文本解读有界翻译验证将循环展开指定次数例如 2 次只检查在这些展开次数内可能触发的错误。如果错误需要更多迭代才能暴露则可能漏报。这是一种工程权衡。循环分析使用 Tarjan-Havlak 算法识别循环及其嵌套关系构建循环嵌套森林。后序遍历由内向外先展开最内层循环处理循环这样展开次数与循环数量呈线性关系避免指数爆炸。展开操作复制循环体达到展开因子。修补操作数维护一个映射记录每个原始 SSA 值的各次副本复制指令时用最新副本替换操作数。修补跳转目标将回边跳转到下一个副本的对应基本块最后一次展开的回边重定向到一个特殊的 sink BB。修补 φ 节点对于循环内定义、循环外使用的值需要插入新的 φ 节点或使用内存栈变量来合并各次迭代的值。sink BB表示展开后无法到达出口的路径。它的可达性条件被取反并加入函数的前置条件从而限制精化检查只考虑能够正常退出循环的路径。展开因子选择对于不操作循环的优化至少为 2以覆盖 φ 节点的回边入口对于操作循环的优化如向量化可能需要更大的因子如 64。概述Alive2 通过有界翻译验证来处理循环将源和目标函数中的循环按指定因子展开从而将包含循环的问题转化为无环的等价问题再使用 SMT 求解器检查精化关系。具体例子: 循环向量化优化假设我们有一个简单的循环计算数组元素之和。源程序未优化和目标程序手动展开一次都使用 LLVM IR。源程序 src.lldefine i32 sum(i32* %arr, i32 %n) { entry: %cmp icmp sgt i32 %n, 0 br i1 %cmp, label %loop, label %exit loop: %i phi i32 [ 0, %entry ], [ %i.next, %loop ] %sum phi i32 [ 0, %entry ], [ %sum.next, %loop ] %ptr getelementptr i32, i32* %arr, i32 %i %val load i32, i32* %ptr %sum.next add i32 %sum, %val %i.next add i32 %i, 1 %cmp2 icmp slt i32 %i.next, %n br i1 %cmp2, label %loop, label %exit exit: %sum.final phi i32 [ %sum.next, %loop ] ret i32 %sum.final }目标程序 tgt.ll手动展开一次优化将循环的前两次迭代合并减少分支开销。define i32 sum(i32* %arr, i32 %n) { entry: %cmp icmp sgt i32 %n, 0 br i1 %cmp, label %loop.unrolled, label %exit loop.unrolled: ; 第一次迭代 %i0 0 %ptr0 getelementptr i32, i32* %arr, i32 %i0 %val0 load i32, i32* %ptr0 %sum1 add i32 0, %val0 ; 第二次迭代如果 n 2 %i1 1 %ptr1 getelementptr i32, i32* %arr, i32 %i1 %val1 load i32, i32* %ptr1 %sum2 add i32 %sum1, %val1 %i.next 2 %cmp2 icmp slt i32 %i.next, %n br i1 %cmp2, label %loop.remain, label %exit loop.remain: ; 剩余迭代用原始循环 %i phi i32 [ %i.next, %loop.unrolled ], [ %i.next2, %loop.remain ] %sum phi i32 [ %sum2, %loop.unrolled ], [ %sum.next, %loop.remain ] %ptr getelementptr i32, i32* %arr, i32 %i %val load i32, i32* %ptr %sum.next add i32 %sum, %val %i.next2 add i32 %i, 1 %cmp3 icmp slt i32 %i.next2, %n br i1 %cmp3, label %loop.remain, label %exit exit: %sum.final phi i32 [ %sum2, %loop.unrolled ], [ %sum.next, %loop.remain ] ret i32 %sum.final }我们要验证tgt是否精化src。Alive2 的处理过程循环分析源程序只有一个循环头块loop无嵌套。目标程序有loop.unrolled和loop.remain两个基本块但loop.remain构成一个循环头块 loop.remain。实际上loop.unrolled是展开后的部分不是循环。选择展开因子这里优化涉及循环改变了循环结构因此需要较大的展开因子。假设我们选择因子 2覆盖回边。展开循环源程序展开因子 2将loop展开 2 次得到无环的 IR示意entry - copy0 copy0: ; 第一次迭代 i0 0, sum0 0 load arr[0] - val0, sum1 sum0val0 i1 1, check i1 n ? if true - copy1 else - exit0 copy1: ; 第二次迭代 load arr[1] - val1, sum2 sum1val1 i2 2, check i2 n ? if true - sink (因为展开结束) else - exit1 exit0: ; 提前退出n1 sum.final sum1 exit1: ; 正常退出n2 sum.final sum2 sink: ; 需要更多迭代不可达n3Alive2 会为sink块添加不可达约束即假设n 3才能验证精化。因此这种有界验证只能覆盖n 2的情况。目标程序展开目标程序本身已经部分展开Alive2 只需将loop.remain展开因子 2 次类似过程得到无环 IR。修补操作数、跳转和 φ 节点在复制过程中Alive2 维护一个ValueMap将原始 SSA 值映射到当前副本。例如源中%i在第一次副本中变为%i_0第二次变为%i_1。跳转目标也相应更新。生成 SMT 公式Alive2 将展开后的无环 IR 编码为 SMT 公式。以下是对源程序展开后假设 n2 的情况的简化编码。变量定义输入arr符号化内存n整数我们假设内存是数组用select和store建模。这里简化load(arr, i)返回第 i 个元素的值记作mem[i]。第一次迭代copy0i0 0 sum0 0 val0 mem[i0] (即 mem[0]) sum1 sum0 val0 cond0 (i01) n 即 1 n第二次迭代copy1如果cond0为真则执行i1 1 val1 mem[i1] (mem[1]) sum2 sum1 val1 cond1 (i11) n 即 2 n如果cond1为假则退出如果为真则进入 sink不可达。退出条件如果cond0为假即n 1则最终结果为sum1。如果cond0为真且 cond1 为假即n 2则最终结果为sum2。如果cond0为真且 cond1 为真n 3则进入 sink我们强制false约束即认为这种输入不会发生。因此我们只验证n ∈ {0,1,2}的情况。最终 SMT 公式源(declare-fun mem (Int) Int) ; 数组 (declare-fun n () Int) (assert (and ( n 0) ( n 2))) ; 有界假设 (define-fun src_output () Int (ite ( n 1) ( 0 (mem 0)) ( ( 0 (mem 0)) (mem 1)) ) )目标程序展开后的 SMT 公式目标程序对于n0,1,2的行为应该与源相同。我们手动推导如果n 0直接跳到exit返回 0。如果n 1执行loop.unrolled中的第一次迭代然后条件1 n为假跳exit返回sum1 mem[0]。如果n 2执行两次迭代然后条件2 n为假跳exit返回sum2 mem[0] mem[1]。因此目标输出公式与源完全相同。精化检查Alive2 构建如下验证条件∀ mem, n (0 ≤ n ≤ 2) → (src_output tgt_output)这是一个可满足性检查试图找到反例使两边不等。由于我们构造的优化是正确的SMT 求解器会返回 UNSAT无反例从而验证成功。如果优化有错误假设目标程序错误地将第二次迭代的加法顺序颠倒导致sum2 mem[1] mem[0]实际上加法交换律不影响结果但假设有更复杂错误。那么对于某些输入比如mem[0]5, mem[1]3结果仍相同。需要更隐蔽的错误例如忘记累加第二次迭代。假设目标程序在n2时错误地返回mem[0]遗漏了第二次迭代。那么源输出为538目标输出为 5SMT 求解器会找到反例mem[0]5, mem[1]3, n2输出SAT并报告精化失败。总结Alive2 通过有界展开将循环转化为无环代码然后使用 SMT 求解器验证精化。展开过程需要精心修补操作数、跳转和 φ 节点并引入 sink BB 来处理超出展开次数的路径。选择展开因子是精度与效率的权衡。上述例子展示了从 LLVM IR 到 SMT 公式的转换核心思想用ite表示控制流用算术运算表示计算用数组理论表示内存。