编译器本身是可能有 bug 的，会导致引入错误编译问题(miscompilation)，这对于安全要求高、容错率低的任务是很难接受的。

我们会希望编译器生成的代码，其语义与我们所写的源代码语义完全一致，不会被编译器误编译本身所影响，本文简单了解一下通过了形式化验证的编译器 CompCert，其保证了编译的正确性和语义一致性。

1、形式化验证(Formally verified compilation)

形式化验证是在计算机硬件（特别是集成电路）和软件系统的设计过程中，形式验证的含义是根据某个或某些形式规范或属性，使用数学的方法证明其正确性或非正确性。由于软件测试无法证明系统不存在缺陷，也不能证明它符合一定的属性。只有借助形式化验证过程可以证明一个系统不存在某个缺陷或符合某个或某些属性。

由于形式化验证相关的研究在国内较为小众，所以当提到“形式化验证”有什么用？有什么具体行业应用案例？”可能对于非专门研究此方向的业内人士一时也难以举例说明。但其实形式化验证已经在航空航天、军工、电力交通等关键领域可以见其身影。如NASA、空客的一些控制系统，巴黎地铁等等。

编译器引入的错误是很难暴露和追踪的，而一些行业的安全要求特别高，所以也需要高标准的编译可信度。通过限制 C 语言、编译器使用方式、对比编译前后代码、软件测试等还不足以从根本上解决问题，因此引入了对编译器本身进行形式化验证来判断其正确性。

编译器形式化验证是利用严格的数学逻辑体系，对编译过程语义及语言属性的保持和正确进行证明。

其中一个概念是语义保持(Semantic preservation)，从一种语言表示转换到另一种语言表示，而语义行为一致。对于所有源程序 S 和编译器生成的代码 C，如果编译器没报告编译错误，那么代码 C 属于程序 S 所允许的改进行为。(比如表达式求值的顺序可能存在一些不确定性，不同的顺序可能导致不同的行为)。

换句话说，经过形式化验证的编译器要么报告错误，要么生成满足所需正确性属性的代码。

2、CompCert C

CompCert C 是 C 语言的编译器，可以生成高水平保证、行为一致性高的代码，支持生成 PowerPC、ARM、x86 和 RISC-V 架构的机器码。使用 CompCert 是在源代码级别应用形式验证技术（静态分析、程序证明、模型检查）的自然补充。 CompCert 的正确性证明保证了在源代码上验证的所有安全属性也自动适用于生成的代码。

CompCert C 使用数学证明进行了形式验证，以数学确定性证明编译器生成的可执行代码的行为，完全符合源 C 程序的语义所指定的行为，这样就可以避免错误编译问题 (miscompilation)。即通过对编译器本身进行形式化、工具辅助的验证，来解决误编译的问题。

CompCert 的正确性证明是使用 Coq proof assistant 进行的，这是一个软件工具，可以帮助我们与该工具交互构建证明，然后自动重新检查证明的有效性。

编译器通过 CompCert C AST 生成 Asm 代码(汇编语言的抽象语法语言)，经过 8 种中间语言和 15 次编译 pass (lowering 降级或优化)。

CompCert 编译器的源语言称为 Clight，是 C 语言的一个大型子集。后续的几个 pass 都是它的简化版。它支持几乎所有的 C 数据类型，包括指针、数组、结构体和联合类型；所有结构化控制 (if/then、循环、break、continue、Java 风格的开关)、以及函数的全部功能，包括递归函数和函数指针。不支持的是扩展精度算术(long long 和 long double)、goto 语句等。如果有未定义行为会直接报错。

CompCert 的性能比不上 GCC4，不过也会执行一些优化，而且这些优化都通过了形式化验证：

  • 使用图形着色和迭代寄存器合并进行寄存器分配。
  • 具有强度降低的指令选择，以利用目标架构提供的组合指令。
  • 常量传播。
  • 公共子表达式消除。
  • 死代码消除。
  • 函数内联。
  • 尾调用消除。
  • if 转换，用条件移动指令替换条件分支。

3、Coq proof assistant

前面说到，CompCert 的正确性证明是使用 Coq proof assistant 进行的，用来证明其对语义的保持。

用户通过输入一系列构成证明步骤的策略来生成证明，然后由 Coq 提供机器辅助的自动化定理证明。有个线上体验网址，不过需要先理解 Coq 的语法。

Coq 的代码 14% 定义了 CompCert 中实现的编译算法，10% 指定了所涉及语言的语义，剩下的 76% 对应于正确性证明本身。

简单举个操作流程的例子(粗略看看就好，这里只是为了说明要写出通过形式化证明的操作流程)：

比如窥孔优化(Peephole Optimization) 是编译器常见优化，可以替换指令序列为更快、等效的序列。

这里认为转换前的序列处于查找模式，而转换后序列处于替换模式。

上面的指令是当 x 和 y 是 32 位二进制补码时，则从 x = y - x - 1 转换成 x = y + ~x。

在证明窥孔优化的正确性时，需要几个点：

  • Peephole Data。用于定义转换的数据。l 为查找模式的指令序列，r 为替换模式的指令序列，U 为 l 和 r 读取的所有寄存器，D 为 l 和 r 用同样的值更新的所有寄存器(对应上图为 %eax)，T 为 l 和 r 以不同上下文离开的所有寄存器，P 为没出现过在 l 和 r 的所有寄存器。
  • Local Correctness。证明转换满足局部正确性属性。如果 l 和 r 总是结束以相同地更新所有 live location，开始也是所有 live location 所允许的状态，则认为其正确。

  • Side Conditions。建立全局正确性证明中使用的辅助属性。要求 l 和 r 长度一致(可用 nop 填充)、l 的最后一条指令不是 label、还有 l 和 r 不包含任何调用或返回指令，这意味着它们不会通过进行系统调用来修改全局程序跟踪 trace。

当然实际还要结合全局层面来进行分析，数学看晕了，这里就不再展开了。

大致就是要构造数据，然后构造和编写证明，最后通过 Coq 机器辅助证明其正确性。

4、结论

CompCert 是专为安全要求高所制作的编译器，避免了误编译问题，其本身用大量的数学证明来保证了其自身的正确性。

参考