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

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

来源: sbw Blog | 浏览: 40 | 评论: 0 发表时间: 2021-01-30

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



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


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


c source code

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


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


llvm ir code

参考IR,数据X%x = alloca i32, align 4所定义,而这个定义可以一直到达分支指令br,当然也包含其之前的任何一条指令(同样,数据YZ也可以到达这些指令的位置)。然后,数据XIR的第23行被重新定义,从这里开始,这个新的定义可以到达IR23~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):表示数据XY指令处定义。这里也就是数据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,则YX之后是可达的,这个很好理解,因为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的结果,指明了定义在哪些指令之后是有效的:


Out result

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


In result


没有人评论过此文,还不快抢个沙发
  • 昵称: *
  • 邮箱:
  • 网址:
  • 记住我的信息
  • Color
  • Red
  • Blue
  • Code
  • bash
  • cpp
  • css
  • java
  • js
  • perl
  • php
  • python
  • ruby
  • sql
  • xml