一句话：提出 arm-tv，形式化验证 LLVM IR 到 AArch64 汇编的翻译，并在该后端发现 45 个此前未知的误编译缺陷。
LLVM 后端并不只是寄存器分配与指令选择：它带有数据流分析、公共子表达式消除、循环不变量外提等中端优化，以及一等公民的机器级 IR（MIR），实际上是一个高度优化的编译器，其百万行复杂 C++ 代码蕴含大量正确性风险。本文提出 arm-tv，对 LLVM IR 与 AArch64（64 位 ARM）代码之间的翻译进行形式化验证。作为 checking validator，arm-tv 强制检查多条 ABI 规则；作者扩展 Alive2 作为验证后端，以处理汇编代码中指针与整数非结构化混用的情形；并比较了手写 AArch64 语义与从 ARM 官方形式语义机械导出的语义之间的取舍。在评估中，arm-tv 在该 LLVM 后端发现 45 个此前未知的误编译缺陷，其中大多数已在上游 LLVM 修复。
LLVM’s backends translate its intermediate representation (IR) to assembly or object code. Alongside register allocation and instruction selection, these backends contain many analogues of components traditionally associated with compiler middle ends: dataflow analyses, common subexpression elimination, loop invariant code motion, and a first-class IR—MIR, the “machine IR.” In effect, this kind of compiler backend is a highly optimizing compiler in its own right, with all of the correctness hazards entailed by a million lines of intricate C++. As a step towards gaining confidence in the correctness of work done by LLVM backends, we have created arm-tv, which formally verifies translations between LLVM IR and AArch64 (64-bit ARM) code. Ours is not the first translation validation work for LLVM, but we have advanced the state of the art along multiple fronts: arm-tv is a checking validator that enforces numerous ABI rules; we have extended Alive2 (which we reuse as a verification backend) to deal with unstructured mixes of pointers and integers that are typical of assembly code; we investigate the tradeoffs between hand-written AArch64 semantics and those derived mechanically from ARM’s published formal semantics; and, we have used arm-tv to discover 45 previously unknown miscompilation bugs in this LLVM backend, most of which are now fixed in upstream LLVM.
@article{paperbot2882,
title = {Translation Validation for LLVM’s AArch64 Backend},
author = {Ryan Berger and Mitch Briles and Nader Boushehrinejad Moradi and Nicholas Coughlin and Kait Lam and Nuno P. Lopes and Stefan Mada and Tanmay Tirpankar and John Regehr},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763147}
}