使用Z3+LLVM实现定义可达分析

最近在研究的一个功能：使用LLVM IR配合Z3求解器为C语言程序实现一个基于约束的数据可达性静态分析。通过这个技术可以高效的实现代码静态分析功能，也可以作为IDE的数据源提供给其它功能使用。

实现思路：程序作为一个编译器插件，在LLVM所生成的IR基础上执行分析，根据不同指令对数据访问的特点去生成关系，在查找时，Z3根据预先定义的约束规则和生成的关系则可以解析出结果。

以下面这段C代码及相应的IR代码为例：

变量x, y在函数的最开始定义，直到if.then和if.else两个条件分支中被重新赋值之前，x，y的定义都是没有发生改变的，即可以认为x，y的定义是可以到达分支之前的任何一个指令处的。

而在分支内部，变量x，y都被重新赋值，而这个新的值都被if表达式之后的语句所接收，也就是说，在if语句的两个分支中产生的两个新数据，是可以到达if语句之后的。

参考IR，数据X被%x = alloca i32, align 4所定义，而这个定义可以一直到达分支指令br，当然也包含其之前的任何一条指令（同样，数据Y和Z也可以到达这些指令的位置）。然后，数据X在IR的第23行被重新定义，从这里开始，这个新的定义可以到达IR的23~26行这些指令之后，又跟随26行的br指令可以到达if.end分支，直到函数结尾。由于if.then分支中没有任何可能跳转到if.else分支的指令，所以23行所定义的数据无法到达28~33行指令中的任何位置。

有了这些信息，就能知道数据X在哪些位置被改变，每处改变的影响范围以及整个函数中数据X的引用情况都被标记出来。这样在进行一些优化时，就能获取到更丰富的条件。比如可以评估出某一处的指令改变，对之后分支的影响范围等等。

人工搞清楚这个定义可达分析的结果之后，就要考虑如何使用Z3求解器自动推算出这样的分析结果了。

定义以下几个函数：

Out(X, Y)：表示定义Y在指令X之后是可达的，即指令X之后，定义Y有效（这可能是由于X指令新定义了Y，也可能是之前定义的Y在流过指令X之后仍然保持有效状态）。

Def(X, Y)：表示数据X在Y指令处定义。这里也就是数据X新的定义起始点。

In(X, Y)：表示数据X可以到达指令Y。和Out(X, Y)不同的是，Out表示数据在指令Y之后是有效的，而In只表示数据在指令Y及其之前是有效的。

Next(X, Y)：代表指令Y是指令X的直接后继，即指令X之后会到达指令Y，对于分支来说，可能会出现一个指令具有多个后继，或是多个指令的后继是同一条指令。

Kill((X, Y)：代表在指令Y处，定义X被改变了，也就是说，定义X的可达性到Y为止，不再向后传播了。

根据可达性的定义，结合上面的函数，可以制定以下的Z3规则：

Out(X, Y) :- Def(Y, X)：如果X定义了Y,则Y在X之后是可达的，这个很好理解，因为Y是从X处产生的，当然也是从此有效的。

In(X, Y) :- Out(X, Z), Next(Z, Y)：如果定义Z在指令X之后有效，而指令Z的后继指令是Y,那么定义Z在指令Y之前也是有效的。这个规则使得指令可以“继承”来自之前指令的定义，也是真正实现可达性传递的地方。

Kill(Y, Z) :- Def(X, Y), Def(X, Z)：如果数据X被指令Y定义后，又被指令Z定义，则认为指令Z的重新定义行为结束了指令Y之前的定义行为，即数据X从指令Y流出后，在指令Z处终结了。这条规则指出了可达性结束的条件。

有了这3条规则，就指明了一个定义从哪里开始流出（Out），如何流入下一条指令（In），以及在哪里结束（Kill）。那只剩下一个问题：流入的这些定义，在什么情况下可以通过当前指令继续向后流出：

Out(X, Y) :- In(X, Y), !Kill(X, Y)：如果X可以到达Y,而Y又没有重新定义X,那就代表X保持了之前的定义，自然定义X可以继续从Y处流出，再利用第2条规则向后传递。

以下是利用Z3得到的部分Out的结果，指明了定义在哪些指令之后是有效的：

以下是利用Z3得到的部分In的结果，指明了定义在哪些指令之前是有效的：