基于 LLVM 和 Z3 的数组访问越界检查
这是一篇水文。
日语课论文还没写完，开题答辩 PPT 刚刚做完第三稿等着导师回复，忙里偷闲来水篇文章。
编译原理的最后一个课程实验有两个选题，其中一个是基于 LLVM 中间表示配合 Z3 一起进行数组访问越界检查。由于另一个题目是手写垃圾回收，给了份 Go 语言代码作为编程范本和性能对照，我实在是懒得研究 Go 的语言特性、内存分配机制、垃圾回收机制这些东西，于是毅然决然的选了 LLVM + Z3 这个实验。
这个实验给我的感受就是有无数的坑。
实验内容
有一份 LLVM 代码，其中没有循环也没有递归。它定义了一堆函数和一个全局数组。其中有一些加了 inbounds 选项的 getelementptr 语句，这些语句的作用是根据数组指针（即这个全局数组）和传入的下标计算访存地址。inbounds 选项使得一旦出现数组越界（即，假如我只有一个长为 1024 的数组 arr，我却要计算 arr[1024] 的地址），这条语句就会返回一个 poisoned value，从而导致运行时错误。
实验任务是通过 Z3 来推断，对于每个函数，是否存在某个传入的参数组合，使得在 getelementptr 时发生越界。
第一眼看上去还是比较简单的。
控制流敏感分析
控制流敏感本来是非常麻烦的一个玩意儿，但是通过 opt -mem2reg 我们可以把代码变成 SSA（Single Static Assignment，静态单赋值）的，这就让代码中自带了控制流信息，分析也就好做多了。实际上我们要处理的也就是这么个东西。
每个 LLVM 寄存器都对应到 Z3 中的一个 bv_const 上，之所以用位向量而不是 int 是因为 LLVM 里每个整型都是有位宽的，我们要把位宽信息也带入 Z3 中。
由于我之前没有用过 Z3，我天真地认为对 Z3 Context 实例的每一次 bv_const 调用都会产生一个新的位向量实例。于是我想到在分析每个函数前，先扫描这个函数的符号表，找出其中所有的变量，创建对应的 bv_const 实例加入一个 map 中，以供后面取用。在这里，我立即踩到了第一个坑：
坑 #1：
z3::expr没有默认构造函数，不能使用map的取下标运算符（operator[]）。
这是因为 map::operator[] 在对应的键值不存在的时候，会用默认构造函数构造一个新的键值对。跳出这个坑也比较简单，用 insert 和 find 就行了。
坑 #2： 使用这种方式存储
z3::expr会导致谜之上下文不匹配问题，导致 Z3 抛异常，或者让推理结果变成不知道什么玩意。
惊不惊喜意不意外，这就又踩了一个坑。Z3 在做每一个操作的时候会检查两个操作数是否同属一个 Z3 Context 实例：
1 | inline void check_context(object const & a, object const & b) { (void)a; (void)b; assert(a.m_ctx == b.m_ctx); } |
明明是用同一个 context 实例创建出来的，怎么就不一样了呢？我并没有找到原因，但是在不断尝试后，我发现，只要传入名称和位宽都相同，那么 bv_const 函数的返回值就对应这个上下文中的同一个位向量实例！想一想这也是显然的，而用这个方法我就成功地规避了上下文不匹配的问题。
坑 #3： 不是所有的变量和基本块都在函数的符号表中。
这个坑本来是存在的，但是假如每个位向量实例都在使用它的地方用 bv_const 现场取得，这个问题也就不存在了。至于如何得到临时变量的一个名字，可以通过 LLVM 的 raw_string_ostream 把它打印到字符串来解决。
从这三个坑跳出来之后，接下来的流程比较顺利，只需要实现 visit 各个指令类型的函数，然后在每个函数中把对应的断言加入到一个 Z3 Solver 里面。我们需要考虑的指令限制在一小部分二元算术和位运算指令、比较指令和一元位扩展指令中。Z3 重载了表达式的各种算术和位运算符，提供了 ite 表示 if-then-else 结构，提供了有符号和无符号比较功能（有符号比较直接使用运算符），提供了位扩展函数，全都套用进去就可以了。
分支分析
为了做好控制流敏感分析，我们还必须做到分支敏感。
分支敏感意味着我们要处理 br 指令，以及烦人的 phi 指令。我们来看看 LLVM 是怎么说的。下面这段文字原封不动地摘抄自 llvm/IR/Instructions.h 中 PHINode 类前面的注释，其中重点部分加粗：
PHINode - The PHINode class is used to represent the magical mystical PHI node, that can not exist in nature, but can be synthesized in a computer scientist’s overactive imagination.
这个评价可以说是十分准确地代表了我的想法。
由于代码是 SSA 的，并且各个基本块也构成一个 DAG（没有循环），我们可以通过拓扑序扫描每个基本块，确定性地给出到达每条基本块所需的逻辑条件。具体来说，初始时除了入口基本块的进入条件为 true，其他基本块的进入条件全部初始化为 false。假设当前基本块的进入条件为 cond，如果我们在其中遇到了一条 br 指令（这也一定是它的最后一条指令）：
- 如果是无条件跳转，那么对应的后继的进入条件要和
cond取逻辑或； - 如果是有条件跳转，设这个
br检查的寄存器为r，那么两个对应的后继的进入条件分别和(cond && r == 0)、(cond && r == 1)取逻辑或。
坑 #4： 有条件的
br指令中，排在前面的操作数代表的是r == 0跳到的基本块，也就是 else 的情况。
这其实很好理解，因为 1 前面是 0；但是它稍微有点违反直觉，因为我们总是先写 if 语句成立时的代码，再写它不成立时的代码。
回到正题，我们不仅要保存每个基本块的进入条件，同时还要分开保存走每条边（基本块到基本块之间的有向边）的条件。这是为了方便 phi 语句的处理。显然，一个基本块的进入条件等于它所有前驱到它的边上的条件的逻辑或。
LLVM 保证 phi 指令一定在基本块的最前面。通过 Z3 的 implies 函数，我们可以表示出 phi 函数中的蕴涵关系（实际上这是一个等价关系，但是这里无所谓）。
getelementptr 分析
通过以上一通操作，我们获得了关于函数中所有变量的断言集合 F。当我们遇到一个 getelementptr，我们可以知道它不越界的条件。比方说，假如要访问的数组是一个长度为 1024 的一维数组，传入的下标是 i，那么这个条件（记作 A）就是 0 <= i && i < 1024。
我们要检查的就是 F && !A 是否可满足，如果是，那么这里就可能产生数组越界。在分析的时候我们利用 Solver 的 push 函数构造一个新的 scope，然后再向其中加入 !A，分析完可满足性之后再 pop 出去，防止数组越界条件污染原本的断言集合。
做完这部分之后，第一阶段——也就是整个实验的大部分内容就都完成了。
上下文敏感分析
这一部分要考虑函数之间的互相调用，处理 call 和 ret 指令，完善第一阶段的数组越界检测模型。
函数表达的求解
为了表示 LLVM 中的函数，我们同样需要利用 Z3 中的函数。假如说有这么一个函数：define i32 @foo(i32 %i, i32 %j)，其中有一条指令 %c = add i32 %a, %b。原本我们生成的是类似这样的断言（为了阅读方便，以下全部用 Z3 Python API 风格）：
1 | c == a + b |
现在，为了表现函数关系，我们把函数中使用的寄存器，连带着这个函数（LLVM）本身一起，表示为关于函数（LLVM）参数的一个函数（Z3）：
1 | ForAll((i, j), c(i, j) == a(i, j) + b(i, j)) |
这个代换非常简单明了，不过它只适用于纯函数。为了简化问题，我们不需要考虑函数返回值与访存相关的情况。这看起来不难，我们本来并没有针对 load 指令做任何处理；纯函数自然没有问题，非纯函数和 load 指令相关的寄存器对应的函数在 Z3 中就是没有任何约束，Z3 自然会把它当做一个任意值来看待，岂不美哉？
坑 #5： 在这种时候，Z3 很大概率无法在可接受的时间内得出解。
可能看起来很不可思议，Z3 作为一个成熟的推理引擎，在面对这类断言时推理能力低得令人发指。考虑如下绝对值函数：
1 | define i32 @abs(i32 %i) { |
这个绝对值函数通过一个 if-else 结构判断返回值应该等于传入的参数，还是它的相反数。这段程序理应生成如下 Z3 断言集合：
1 | ForAll(i, cmp(i) == If(i < 0, 1, 0)) |
把它交给 Z3 分析，Z3 会很快判定模型可解，并且得到一个并不十分好看的结果：
1 | If(i == 2147483648, |
但是这毕竟是有一个结果。我们看到，这五个断言实际上非常啰嗦，它为了表达一个绝对值用了许多中间表示，我们完全可以把它压缩为一个：
1 | ForAll(i, abs(i) == If(i < 0, 0 - i, i)) |
任何人都会觉得这一个断言比上面那五个直白得多，并且这个断言天然就表示了模型是可满足的，Z3 根本不需要求解 abs(i) 的表示，直接用我们给它的就行了。
但结果呢? 我们发现 Z3 无法在规定时间内出解。
这很匪夷所思。不过现在 i 是 32 位的位向量，如果说是搜索空间太大也勉强算是情有可原。把位宽改成一个小点的数，比如说 2 试试？这回马上就出解了：
1 | If(If(ULE(1, i), If(ULE(2, i), If(i == 3, 3, 2), 1), 0) == 3, |
这个解真的是无比丑陋和冗长，其中充斥着一些小学生也能看出来的严重问题。例如，最外面的 if 语句的条件中：
1 | If(ULE(1, i), If(ULE(2, i), If(i == 3, 3, 2), 1), 0) |
ULE 是无符号比较，在无符号的意义下 i 只有 0、1、2、3 这 4 个取值；所以这个表达式写了一堆 if，实际上最后返回的结果就是 i 本身。可以想象当位宽是 32 的时候 Z3 将会得出多么大一坨屎。
见识了 Z3 软弱的推理能力，我们只能选择不处理返回值与访存有关的函数。然而，这里又有一个新坑：
坑 #6： 判断返回值是否与访存有关需要求解一个前向数据流模型。
虽然这是前两次实验做过的东西，但要移植这玩意儿到 C++ 工作量就太大了。于是大手一挥，凡是含有 load 的函数都不予考虑。这下六根清净。
使用求解出的函数表达
求解出 model 后，实验文档要求我们求出函数的表达，存下来备用。但这是非常麻烦的，如果我们在求解 model 后立即取得函数的表达，我们使用的将是函数的形式参数；到了函数调用点，我们需要把其中所有的形式参数换成实际参数。要做这个代换不知得花费多大的力气，我们不如就存下一个 model，然后等到了调用点再用实际参数取得函数返回值的表达。
实验文档还要求我们全程使用带 ForAll 的 Z3 的函数表达。然而，见识了 Z3 的垃圾之处后，我是实在不再敢用这个东西了；反正用回之前的 bv_const 也没有任何问题，不如就直接复用第一阶段的代码。
至此，这个作业终于完结。
总结
踩坑真 TM 快乐啊。