Alive2 如何对包含循环的 LLVM 优化进行有界验证
文本解读
- 有界翻译验证：将循环展开指定次数（例如 2 次），只检查在这些展开次数内可能触发的错误。如果错误需要更多迭代才能暴露，则可能漏报。这是一种工程权衡。
- 循环分析：使用 Tarjan-Havlak 算法识别循环及其嵌套关系，构建循环嵌套森林。
- 后序遍历：由内向外（先展开最内层循环）处理循环，这样展开次数与循环数量呈线性关系，避免指数爆炸。
- 展开操作：
- 复制循环体达到展开因子。
- 修补操作数：维护一个映射，记录每个原始 SSA 值的各次副本，复制指令时用最新副本替换操作数。
- 修补跳转目标：将回边跳转到下一个副本的对应基本块；最后一次展开的回边重定向到一个特殊的 sink BB。
- 修补 φ 节点：对于循环内定义、循环外使用的值，需要插入新的 φ 节点或使用内存（栈变量）来合并各次迭代的值。
- sink BB：表示展开后无法到达出口的路径。它的可达性条件被取反并加入函数的前置条件，从而限制精化检查只考虑能够正常退出循环的路径。
- 展开因子选择：对于不操作循环的优化，至少为 2（以覆盖 φ 节点的回边入口）；对于操作循环的优化（如向量化），可能需要更大的因子（如 64）。
概述
Alive2 通过有界翻译验证来处理循环：将源和目标函数中的循环按指定因子展开
从而将包含循环的问题转化为无环的等价问题，再使用 SMT 求解器检查精化关系。
具体例子: 循环向量化优化
假设我们有一个简单的循环，计算数组元素之和。源程序（未优化）和目标程序（手动展开一次）都使用 LLVM IR。
源程序 src.ll
define 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 = sum0+val0 i1 = 1, check i1 < n ? if true -> copy1 else -> exit0 copy1: ; 第二次迭代 load arr[1] -> val1, sum2 = sum1+val1 i2 = 2, check i2 < n ? if true -> sink (因为展开结束) else -> exit1 exit0: ; 提前退出（n==1） sum.final = sum1 exit1: ; 正常退出（n>=2） sum.final = sum2 sink: ; 需要更多迭代，不可达（n>=3）Alive2 会为sink块添加不可达约束，即假设n < 3才能验证精化。因此这种有界验证只能覆盖n <= 2的情况。
目标程序展开
目标程序本身已经部分展开，Alive2 只需将loop.remain展开因子 2 次（类似过程），得到无环 IR。
修补操作数、跳转和 φ 节点
在复制过程中，Alive2 维护一个ValueMap，将原始 SSA 值映射到当前副本。
例如，源中%i在第一次副本中变为%i_0，第二次变为%i_1。跳转目标也相应更新。
生成 SMT 公式
Alive2 将展开后的无环 IR 编码为 SMT 公式。以下是对源程序展开后（假设 n=2 的情况）的简化编码。
变量定义
输入：arr（符号化内存），n（整数）
我们假设内存是数组，用select和store建模。这里简化：load(arr, i)返回第 i 个元素的值，记作mem[i]。
第一次迭代（copy0）
i0 = 0 sum0 = 0 val0 = mem[i0] (即 mem[0]) sum1 = sum0 + val0 cond0 = (i0+1) < n 即 1 < n第二次迭代（copy1）
如果cond0为真，则执行：
i1 = 1 val1 = mem[i1] (mem[1]) sum2 = sum1 + val1 cond1 = (i1+1) < 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 公式
目标程序对于n=0,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），结果仍相同。需要更隐蔽的错误，例如忘记累加第二次迭代。
假设目标程序在n=2时错误地返回mem[0]（遗漏了第二次迭代）。那么源输出为5+3=8，目标输出为 5，SMT 求解器会找到反例mem[0]=5, mem[1]=3, n=2，输出SAT，并报告精化失败。
总结
Alive2 通过有界展开将循环转化为无环代码，然后使用 SMT 求解器验证精化。
展开过程需要精心修补操作数、跳转和 φ 节点，并引入 sink BB 来处理超出展开次数的路径。
选择展开因子是精度与效率的权衡。
上述例子展示了从 LLVM IR 到 SMT 公式的转换核心思想：用ite表示控制流，用算术运算表示计算，用数组理论表示内存。