LLVM AArch64后端的翻译验证

《Proceedings of the ACM on Programming Languages》：Translation Validation for LLVM’s AArch64 Backend

LLVM的arm-tv项目通过形式化验证确保AArch64架构下LLVM中间表示与机器码的转换正确性，验证过程中发现并修复45个误编译问题，扩展了Alive2工具支持复杂汇编数据流分析，同时对比手工编写与机械推导的ARM语义差异。

　　

摘要

LLVM的后端将其中间表示（IR）转换为汇编代码或目标代码。除了寄存器分配和指令选择之外，这些后端还包含许多与编译器中间代码阶段相关的组件：数据流分析、公共子表达式消除、循环不变量代码移动以及一种称为“机器IR”（MIR）的一级中间表示。实际上，这种类型的编译器后端本身就是一个高度优化的编译器，它涉及数百万行复杂C++代码所带来的所有正确性风险。为了增强对LLVM后端工作正确性的信心，我们开发了arm-tv工具，该工具可以正式验证LLVM IR与AArch64（64位ARM）代码之间的转换。虽然这不是针对LLVM的首个转换验证项目，但我们在多个方面推动了技术的发展：arm-tv是一个能够强制执行众多ABI规则的检查验证工具；我们扩展了Alive2（我们将其作为验证后端重新使用）以处理汇编代码中常见的指针和整数的混合结构；我们研究了手动编写的AArch64语义与从ARM官方形式化语义中机械推导出的语义之间的权衡；此外，我们还利用arm-tv发现了该LLVM后端中45个此前未知的编译错误，其中大部分已在上游的LLVM版本中得到修复。