小编Pav*_*kov的帖子

任何或多或少的实用编程语言和编译器都必须处理约束.最常见的约束是类型.通常,类型推导和统一是通过简单的算法(例如Hindley-Milner)完成的,其中最终程序中的所有项都被赋予唯一类型.如果没有发生,则会出现错误指示.

在编译器中可能存在更复杂的约束,其中完全统一是不可能的,并且解决方案仅在某些限制下存在.可能的例子是

• 数据流分析.仿射相等约束的解可以用于循环矢量化.

• 内存管理.如果我们对引用和数据访问模式有一些约束,编译器可以从优化引用计数和垃圾收集中受益.

从另一点来看,约束求解器(如Z3或Yices)在为不同类型的约束寻找可满足的模型方面非常强大.

我正在寻找有关编译器如何从SMT求解器的强大功能以及他们正在解决的任务类型中受益的成功案例.我列出了一些区域,但我没有找到任何具体的例子.你能建议吗？

我有一段需要反混淆的C代码.它包含一堆棘手的宏.我通过C预处理器和缩进运行代码,现在看起来类似于:

switch (9263 + 1505) {
case 1505 + 41131 + 6729 + 2347:
            ...
case 1505 + 41131 + 6729 + 2347 + 1:
            ...
case 1505 + 41131 + 6729 + 2347 + 2:
            ...

为了简化进一步的分析,我正在寻找一些可以折叠代码中所有常量的工具.我知道C预处理器无法做到这一点,并且在编译阶段将执行常量折叠优化.但是源代码怎么样？

Shell脚本也很受欢迎,因为我怀疑这可能是唯一的方法.

我的目标是定义一个内射函数f: Int -> Term，其中Term有一些新的类型。提到内射函数的定义后，我写了以下内容：

(declare-sort Term)
(declare-fun f (Int) Term)
(assert (forall ((x Int) (y Int))
                (=> (= (f x) (f y)) (= x y))))
(check-sat)

这将导致超时。我怀疑这是因为求解程序试图验证Int域中所有值的断言，该值是无限的。

我还检查了上述模型是否适用于某些自定义排序，而不是Int：

(declare-sort Term)
(declare-sort A)
(declare-fun f (A) Term)
(assert (forall ((x A) (y A))
                (=> (= (f x) (f y)) (= x y))))
(declare-const x A)
(declare-const y A)
(assert (and (not (= x y)) (= (f x) (f y))))
(check-sat)
(get-model) …

我正在编写一个Clang工具来静态分析源文件,并匹配和重命名类的所有私有成员.

考虑一个例子:

class AClass { // problem: my matcher modifies AST node here too
private:
    int a; // <- I know how to rename this 'a' using other matcher
public:
    AClass() {
        AClass cl;
        this->a = 1; // <- rename this 'a'
        cl.a = 2; // <- rename this 'a'
    }
};
void bar(AClass);
void foo() {
    //bar(AClass());
}

我使用以下匹配器来访问我想要修改的AST节点.它像我期望的那样工作.

clang-query> match memberExpr(hasDeclaration(namedDecl(isPrivate())))

Match #1:

sum.cpp:7:9: note: "root" binds here
    this->a = 1;
    ^~~~~~~

Match #2:

sum.cpp:8:9: note: "root" binds …