Gia*_*bue 3 compiler-construction formal-verification formal-methods compilation llvm
假设我有这样的函数:
int foo(int a, int b, int d, int x){
if (c) {a = 1; b = 1; d = a;}
else {a = 2; b = 2; d = 1;}
if (a == b) {x = d;} else {x = 0;}
return x;
}
Run Code Online (Sandbox Code Playgroud)
这个简单的函数总是返回1.使用clang -O2选项进行编译并查看反汇编代码LLVM正确编译此函数return 1;.
我的问题是:llvm如何进行静态值分析?最弱的前提技术?价值传播?霍尔的技术?
LLVM做各种各样的事情:见这里.
您可以在每次优化传递后获得中间表示的转储,如下所示:
clang -c -mllvm -print-after-all -O2 foo.c
Run Code Online (Sandbox Code Playgroud)
确定哪个阶段正在做什么.
事实上,这个特殊的例子并不是非常神奇!
如果将其转换为SSA格式,它看起来像这样:
// block 1
if (c == 0) goto L1;
// block 2
a_0 = 1;
b_0 = 1;
d_0 = a_0;
goto L2;
L1:
// block 3
a_1 = 2;
b_1 = 2;
d_1 = 1;
goto L2;
L2:
// block 4 (has two possible predecessors: block 2 or block 3)
a_2 = PHI(a_0, a_1); // i.e. a_0 if we came from block 2, a_1 if we came from block 3
b_2 = PHI(b_0, b_1); // i.e. b_0 if we came from block 2, b_1 if we came from block 3
d_2 = PHI(d_0, d_1); // i.e. d_0 if we came from block 2, d_1 if we came from block 3
if (a_2 != b_2) goto L3;
// block 5
x_0 = d_2;
goto L4:
L3:
// block 6
x_1 = 0;
goto L4;
L4:
// block 7 (has two possible predecessors: block 5 or block 6)
return PHI(x_0, x_1); // i.e. x_0 if we came from block 5, x_1 if we came from block 6
Run Code Online (Sandbox Code Playgroud)
简单地传播常数值会导致:
// block 1
if (c == 0) goto L1;
// block 2
a_0 = 1;
b_0 = 1;
d_0 = 1;
goto L2;
L1:
// block 3
a_1 = 2;
b_1 = 2;
d_1 = 1;
goto L2;
L2:
// block 4
a_2 = PHI(1, 2); // i.e. 1 if we came from block 2, 2 if we came from block 3
b_2 = PHI(1, 2); // i.e. 1 if we came from block 2, 2 if we came from block 3
d_2 = 1; // PHI(d_0, d_1) == PHI(1, 1) i.e. 1 regardless of where we came from
if (a_2 != b_2) goto L3;
// block 5
x_0 = 1; // (we've deduced that d_2 == 1 regardless of control flow)
goto L4:
L3:
// block 6
x_1 = 0;
goto L4;
L4:
// block 7
return PHI(1, 0); // i.e. 1 if we came from block 5, 0 if we came from block 6
Run Code Online (Sandbox Code Playgroud)
简化删除不再用于其他任何内容的赋值给出了:
// block 1
if (c == 0) goto L1;
// block 2
goto L2;
L1:
// block 3
goto L2;
L2:
// block 4
a_2 = PHI(1, 2); // i.e. 1 if we came from block 2, 2 if we came from block 3
b_2 = PHI(1, 2); // i.e. 1 if we came from block 2, 2 if we came from block 3
if (a_2 != b_2) goto L3;
// block 5
goto L4:
L3:
// block 6
goto L4;
L4:
// block 7
return PHI(1, 0); // i.e. 1 if we came from block 5, 0 if we came from block 6
Run Code Online (Sandbox Code Playgroud)
......现在第一个条件显然是无操作; 并且第二个必须始终为真(块5路径)因为a_2并且b_2是相同的表达式.结果是
return 1;
Run Code Online (Sandbox Code Playgroud)