翻译验证 | Codeboy's Blog

形式陈述

翻译验证把编译器或优化器视作可能不受信任的产生器。给定源程序 $P$ ，它输出目标 $Q$ ，有时另输出证书 $c$ ；验证器计算

V(P,Q,c)\in\{\operatorname{accept},\operatorname{reject}\}.

关键定理不是“编译器总正确”，而是验证器的可靠性：

\forall P,Q,c.\quad V(P,Q,c)=\operatorname{accept} \Longrightarrow \operatorname{Beh}_T(Q)\subseteq\operatorname{Beh}_S(P).

右侧采用语义保持阶段的行为精化契约：目标的每种观察行为都必须由源语义允许。行为应记录终止或发散，不能只比较终止时的返回值；否则把正常返回的程序编译成死循环也可能漏检。若源语言含未定义行为（UB），还须约定 UB 之后允许哪些行为：可以将其后续按“任意行为”闭合，或改写为显式的行为改进关系。CompCert 手册 §1.2 使用后一种表述，允许消除源程序的运行时错误，但对无错误源程序保留其允许的终止、发散与 I/O 行为。

验证器可以不完备，即对某些其实正确的输出拒绝；流水线此时应回退、重编译或报告失败，绝不能把 reject 当作“可能也没问题”继续发布。若用小步语义检查局部模拟，证书通常给出控制点映射、状态关系、数据流事实或每条目标边的源路径见证。

验证器本身的可信边界必须明示。可在证明助理中证明 $V$ 的 soundness，只信内核、语义定义和提取链；也可信任一个手写 checker，此时编译器虽移出可信基，checker 仍在其中。证书产生器无需可信，因为错误证书只能导致可靠验证器拒绝。

为了让这条蕴含可部署， $V$ 还应终止并对解析后的确切程序对象作判断。证书中的块编号、符号、目标架构和语义选项必须绑定到当前 $P,Q$ ；工程上可把源、目标与配置的规范化摘要写入证书头，再由 checker 重算。若复用另一轮编译的旧证书、验证后又修改目标，soundness 定理就没有作用到最终二进制。

直觉

与其证明一座巨大工厂永远不会装错零件，翻译验证在每件成品出厂时核对它与订单。优化器可以使用复杂启发式甚至外部求解器，只要每次输出都附带足够证据，简单检查器就能确认这一个源—目标对没有新增行为。

这种分工把“找到优化”和“检查优化”分开。前者可不完备、依赖性能技巧，后者力求小、确定且有可靠性证明。它特别适合搜索算法复杂、但候选结果的验证条件清晰的阶段，例如寄存器着色、指令调度或局部等价检查。

例子与边界

源块先执行 $t:=2+3$ ，再执行 $y:=t\times x$ ；目标直接执行 $y:=5\times x$ 。证书把源入口关联到目标入口，并把源完成第一步、满足 $t=5$ 的状态仍关联到目标入口。checker 可计算位向量恒等式 $2+3=5$ ，确认源第一步是静默停顿，再检查双方乘法一步产生相同 $y$ 与内存。对任意 $x$ ，这组局部义务闭合，就得到本次变换的模拟。

若优化器误产出 $y:=6\times x$ ，取 $x=1$ 即破坏关系，可靠 checker 应拒绝。若目标重排了异常边而证书格式只描述正常 CFG，checker 即使验证所有普通块也不能推出完整语义；异常、trap、调用与发散必须在状态关系和边覆盖中出现。

边界还包括算法覆盖率。一个只理解常量折叠的验证器可能拒绝完全正确的循环展开，这是只影响完备性的假阴性。真正危险的是破坏 soundness 的假阳性：checker 接受错误翻译。随机测试源、目标在若干输入相等可以协助筛错，却没有给出对所有输入和路径的可靠性定理。

推论与应用

验证器可采用前向模拟证书、后向模拟证书、SMT 可证等价或专用校验条件。不同方法仍要落到同一观察契约。验证多个阶段时，可以逐阶段检查并组合精化，也可对源与最终目标做全局验证；前者定位清楚，后者可能发现跨阶段对应，但证书更难生成。

逐阶段组合还要求阶段一的目标语义与阶段二当作源语义的版本完全一致，包括整数宽度、外部事件、调用约定和 UB 解释。两个 checker 即使各自可靠，若通过不同解析器理解同一中间文件，集合包含也无法首尾相接。

参考资料

Amir Pnueli, Michael Siegel, and Eli Singerman, “Translation Validation,” in TACAS 1998, LNCS 1384, Springer, pp. 151–166.
George C. Necula, “Translation Validation for an Optimizing Compiler,” PLDI, 2000, pp. 83–94.
Jean-Baptiste Tristan and Xavier Leroy, “Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations,” POPL, 2008, pp. 17–27.
The CompCert project, CompCert C: a trustworthy compiler, §1.2：行为改进契约、未定义行为，以及终止、发散和 I/O 的观察约定。

形式陈述 ​

反向链接

形式陈述