编译器会进行很多的代码转换和优化的操作，如何保证这些操作的正确性尤为重要。这时候就需要翻译验证(translation validation) 工具了，本文简单介绍下发现了 LLVM 转换中 10 多个 bug 的 Alive2。

1、Alive2

我们可以看到很多 LLVM 的 .ll 文件里的 LIT 测试套件，这个是用来跑 LLVM 单元/回归测试的测试套件，但这些测试更多是验证结果是否一致。这种测试，对于格式转换、文本处理、语义结构化都很有帮助。不过对于识别 LLVM 转换中的问题还不够。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

; RUN: opt < %s -instcombine -S -o - | FileCheck %s
target triple = "x86_64-unknown-linux" 
define i32 @foo(i32 %c) { 
entry:   
    ; CHECK: [[RET:%.+]] = add nsw i32 %c, 3   
    ; CHECK: ret i32 [[RET]]   
    %add1 = add nsw i32 %c, 1
    %add2 = add nsw i32 %add1, 2   
    ret i32 %add2 
}

Alive2 主要服务于 LLVM，可以发现各种形式的未定义行为(UB、undefined behavior)，它检查函数在 LLVM IR(intermediate representation) 上的 refinement 关系。

Alive2 还提供了独立的工具 alive-tv 来判断转换是否正确：https://alive2.llvm.org/ 。

2、refinement

refinement 关系不代表等价，它代表目标函数在所有可能的输入状态下，是否表现为源函数行为的子集。即目标函数的行为，都包含在源函数的行为当中了。

例如，在 C/C++ 中，两个 int 类型变量相加，只要在 -32767..32767 之间就行，当它降级(lower) 到 LLVM IR 时，这个有效值范围被 refine 成 -2147483648..2147483647，然后当 LLVM IR 降级到具体的平台时(ARM 或 x86-64)，结果超出范围的加法会从 undefined 被 refine 成 two’s complement wraparound(二进制补码的操作)。这里面的 refinement 都是合法的，但如果反过来转换(递升、raise) 就是不正确的。

3、LLVM UB

LLVM 中主要有这几种 UB：

  • Undef。IR 中显式声明的值、未初始化的变量等导致的出现不固定值。
1

%cmp = icmp sgt i32 undef, %INT_MAX
  • Poison。支持特定操作执行的可能 overflow 的指令、违背运算规则的指令等。poison 值不会立即发生 UB，但可能会一直传递。
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

entry:
  %poison = sub nuw i32 0, 1           ; Results in a poison value.
  %poison2 = sub i32 poison, 1         ; Also results in a poison value.
  %still_poison = and i32 %poison, 0   ; 0, but also poison.
  %poison_yet_again = getelementptr i32, ptr @h, i32 %still_poison
  store i32 0, ptr %poison_yet_again   ; Undefined behavior due to
                                       ; store to poison.

  store i32 %poison, ptr @g            ; Poison value stored to memory.
  %poison3 = load i32, ptr @g          ; Poison value loaded back from memory.

  %poison4 = load i16, ptr @g          ; Returns a poison value.
  %poison5 = load i64, ptr @g          ; Returns a poison value.

  %cmp = icmp slt i32 %poison, 0       ; Returns a poison value.
  br i1 %cmp, label %end, label %end   ; undefined behavior
  • True undefined behavior。比较直接的 UB，如除 0 操作、非法内存访问等。

4、SMT

SMT(Satisfiability Modulo Theories、基于模理论的可满足性)，用来判定数学公式是否是可满足的。在 Alive2 中，用来判断 LLVM IR 的转换的合法性。它可以验证 LLVM 中所有过程内的内存优化操作。

Z3 是高性能的 SMT solver 解析器，这里采用的是 BTV(bounded translation validation)，即证明对特定的输入程序(特定函数) 的优化是否为正确的(即使是循环，也是有限次数的循环)，而非验证所有输入程序的正确性。

这里通过一个案例去说明 SMT 编码，下图为一个函数转换的案例，优化了堆内存分配的操作，直接返回结果：

这里的转换是合法且正确的，因为 LLVM IR 使用的是抽象的虚拟内存模型，不提供直接的内存访问操作，需要通过 load 和 store 去对内存读写。而根据 LLVM IR 的设定，新分配内存都会指向新的内存块。这里 q 指向了新的内存块，而 r 并没有去拿 q 的地址，所以不会有错误优化这种风险。

我们人工可以判断出这是没问题的，那么怎么去自动化验证呢？就需要把这些状态进行编码操作了。

编码会涉及到指针、范围内内存块的数量、别名规则、内存访问等，然后尝试给源函数和目标函数建立 refinement 关系，证明转换是否合法正确。(这部分涉及比较多的数学定义和运算，不做展开，尝试用一张图说明对这个案例的 refinement 判断)

5、扩展

Alive2 也是可以用于其他编译器的转换验证的，不过最近看到一个使用 python z3 库对 GCC 进行验证的案例，可以看下系列文章了解下：GCC Translation Validation。

它会获取 GCC 中的 GIMPLE IR 进行验证 refinement 关系，跟上述证明一样，主要是：

  • 对于没有 UB 的所有输入，两个函数的返回值是一致的。
  • 目标函数不存在源函数所没有的 UB。
  • 对于没有 UB 的输入，全局内存在触发函数之后行为一致。

参考