CompCert 是目前唯一经过机器检验的优化 C 编译器，也是规模最大的 Coq 工程之一（约 10 万行 Coq + 6 万行 OCaml）。本篇不试图覆盖 CompCert 全貌，而是以 Constprop（常量传播）pass 为切入点，解剖一个工业级 Coq 项目在模块组织、证明策略、仿真关系、提取边界上的工程选择。

CompCert 的编译管线

CompCert 把 C 程序从 Clight（C 的形式化子集）经过约 20 个 pass 编译到 PowerPC / ARM / x86 / RISC-V 汇编。每个 pass 都有一个仿真定理（simulation theorem），保证源程序的可观测行为在变换后保持不变。

1
2
Clight → Csharpminor → Cminor → CminorSel → RTL
  → (各种 RTL 优化 pass) → LTL → Linear → Mach → Asm

RTL（Register Transfer Language）是大部分优化 pass 的载体。Constprop、CSE（公共子表达式消除）、Deadcode（死代码删除）都工作在 RTL 上。

源码目录结构

CompCert 的目录按编译阶段和目标架构组织：

1
2
3
4
5
6
7
8
9
compcert/
├── common/          # 共享定义：内存模型、值、事件、全局环境
├── lib/             # 通用数据结构：映射、lattice、Kildall 不动点
├── cfrontend/       # Clight → Csharpminor → Cminor
├── backend/         # Cminor → Asm 的所有 pass
├── x86/             # x86 目标相关定义
├── arm/             # ARM 目标相关定义
├── driver/          # 编译器入口、pass 组合、整体正确性定理
└── extraction/      # 提取配置和 OCaml 胶水代码

backend/Constprop.v 和 backend/Constpropproof.v 分别是常量传播的实现和证明。这种"实现与证明分离"的文件命名约定贯穿整个项目。

Constprop pass 解剖

抽象域：ValueDomain

常量传播的核心数据结构定义在 backend/ValueDomain.v 中。抽象值用一个 lattice 表示：

1
2
3
4
5
6
7
8
9
Inductive aval : Type :=
  | Vbot                       (* 不可达 *)
  | I    (n: int)              (* 确定的 32 位整数 *)
  | L    (n: int64)            (* 确定的 64 位整数 *)
  | F    (f: float)            (* 确定的双精度浮点 *)
  | FS   (f: float32)          (* 确定的单精度浮点 *)
  | Ptr  (p: aptr)             (* 指针的抽象：全局符号 + 偏移量 *)
  | Ifptr (p: aptr)            (* 可能是整数也可能是指针 *)
  | Vtop.                      (* 任意值 *)

aval 构成一个有限高度的 lattice，Vbot 是底、Vtop 是顶。lub（最小上界）和 ble（偏序判定）是布尔函数，不是 Prop——可判定性在提取后直接变成 OCaml 的 if 分支。

1
2
3
4
5
6
7
8
Definition vlub (v w: aval) : aval :=
  match v, w with
  | Vbot, x | x, Vbot => x
  | I n1, I n2 => if Int.eq_dec n1 n2 then I n1 else Vtop
  | F f1, F f2 => if Float.eq_dec f1 f2 then F f1 else Vtop
  (* ... 其余组合 ... *)
  | _, _ => Vtop
  end.

抽象语义

eval_static_operation 把 RTL 的每个操作符在抽象域上求值。例如加法：

1
2
3
4
5
6
7
8
Definition eval_static_operation (op: operation)
    (vl: list aval) : aval :=
  match op, vl with
  | Oadd, v1 :: v2 :: nil => add v1 v2
  | Osub, v1 :: v2 :: nil => sub v1 v2
  (* ... 几十个 case ... *)
  | _, _ => Vtop
  end.

add 在抽象值上的定义：如果两侧都是确定的整数 I n1 和 I n2，结果是 I (Int.add n1 n2)；否则返回 Vtop。每个这样的抽象操作都附带一个 soundness 引理，保证抽象求值的结果"包含"了具体求值的结果。

1
2
3
4
Lemma add_sound:
  forall v w x y,
  vmatch v x -> vmatch w y ->
  vmatch (Val.add v w) (add x y).

vmatch v x 表示具体值 v 被抽象值 x 覆盖。这个关系是整个 pass 正确性的核心不变量。

不动点计算：Kildall 算法

常量传播需要在 RTL 的控制流图上求不动点。CompCert 使用的是 Kildall 算法的变体，实现在 lib/Kildall.v 中。

1
Module Solver := Dataflow_Solver(AVal)(NodeSetForward).

Dataflow_Solver 是一个参数化模块，接受 lattice 和节点集合策略作为参数。它的正确性定理声明：如果 lattice 满足有限升链条件（ascending chain condition），算法一定终止，且返回值是最小不动点。

终止性证明用了一个精巧的度量函数——lattice 元素到自然数的映射，每次迭代严格递减。这个技巧在前篇（深入 Coq 09）中用过简化版本，CompCert 的版本处理的是产品 lattice（每个程序点一个 lattice 元素）。

变换函数

Constprop.v 中的 transf_function 拿到不动点结果后，逐条指令做常量替换：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Definition transf_instr (approx: D.t) (instr: instruction)
    : instruction :=
  match instr with
  | Iop op args res s =>
      let aargs := aregs approx args in
      match eval_static_operation op aargs with
      | I n =>
          Iop (Ointconst n) nil res s
      | _ =>
          Iop (strength_reduce_op op aargs) args res s
      end
  (* ... Iload, Icond 等 ... *)
  | _ => instr
  end.

如果抽象求值发现某个操作的结果是确定的整数 I n，直接把该指令替换为常量加载 Ointconst n。否则尝试强度削减（strength reduction），例如把 x * 4 替换为 x << 2。

仿真关系与正确性定理

forward simulation

CompCert 的每个 pass 都证明一个前向仿真（forward simulation）定理。Constprop 的核心定理在 Constpropproof.v 中：

1
2
3
4
Theorem transf_program_correct:
  forall prog tprog,
  transf_program prog = OK tprog ->
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).

forward_simulation 是 common/Smallstep.v 中定义的标准关系：源程序每走一步，变换后的程序要么走相同步数的对应步骤，要么走零步（stuttering）。用图来说明：

1
2
3
4
5
6
source state s1 ----step----> source state s2
     |                              |
   match                          match
     |                              |
     v                              v
target state t1 --step(s)--> target state t2

match 是仿真关系（match_states），定义了源状态和目标状态之间的对应。Constprop 的 match_states 核心条件是：在对应的程序点上，目标状态中每个寄存器的具体值都被不动点分析给出的抽象值覆盖。

match_states 的结构

1
2
3
4
5
6
7
8
9
10
Inductive match_states: state -> state -> Prop :=
  | match_regular_states:
      forall s f sp pc rs m s' rs' m' approx
        (MATCH: regs_match_approx approx rs rs')
        (MEM: Mem.extends m m')
        (STACKS: match_stackframes s s'),
      match_states
        (State s f sp pc rs m)
        (State s' (transf_function f) sp pc rs' m')
  (* ... Return_state, Callstate 等 ... *).

regs_match_approx 断言每个寄存器的具体值与分析结果兼容。Mem.extends 断言内存只做了保守的扩展（这里 Constprop 不修改内存布局，所以内存关系比较简单）。match_stackframes 递归地对调用栈做同样的匹配。

证明的规模与策略

Constpropproof.v 约 1500 行。证明的主体是对 RTL 的每种指令（Iop、Iload、Istore、Icall、Icond 等）逐一证明仿真步骤成立。每个 case 的结构相似：

  1. 从 match_states 中拆出寄存器匹配和内存关系
  2. 用抽象求值的 soundness 引理得到变换后指令的具体行为
  3. 构造新的 match_states

这种"逐指令 case analysis"是 CompCert 后端证明的典型模式。Constpropproof.v 在最复杂的 Iop case 中使用了 exploit 和 eauto 的组合来处理几十个操作符的子 case。

整体正确性的组合

pass 的链式组合

driver/Compiler.v 把所有 pass 的 forward simulation 链接成一条从 Clight 到 Asm 的 forward simulation：

1
2
3
4
Theorem transf_c_program_correct:
  forall p tp,
  transf_c_program p = OK tp ->
  backward_simulation (Clight.semantics1 p) (Asm.semantics tp).

注意最终定理是 backward simulation（后向仿真），方向与单个 pass 的 forward simulation 相反。这是因为 CompCert 使用了一个定理：如果源语义是 determinate（确定性的），forward simulation 蕴含 backward simulation。Clight 的确定性在 cfrontend/ClightBigstep.v 中证明。

1
Print Assumptions transf_c_program_correct.

输出会列出若干公理，主要是关于浮点运算的平台假设（Archi.float_of_single_preserves_value 等）和外部函数行为的假设。这些公理对应了 CompCert 的信任基础（Trusted Computing Base, TCB）。

信任基础

CompCert 的 TCB 包括：

  • Coq 本身（内核 + 提取框架）
  • C 的形式化语义（Clight 的定义是否忠实于 ISO C）
  • 汇编语义（目标指令集的行为是否与硬件一致）
  • 链接器和操作系统的行为
  • 浮点运算的平台假设

这些都不在 Coq 内部被验证，而是作为公理或外部假设出现。Print Assumptions 是审计这些边界的标准工具。

工程模式总结

CompCert 的代码组织反映了几个工程决策，可以为中等规模的 Coq 项目提供参考。

实现与证明分离

每个 pass 拆为两个文件：Foo.v（纯实现）和 Fooproof.v（正确性证明）。实现文件可以独立编译和提取，证明文件依赖实现文件但不影响提取产物。好处是修改优化策略时，编译器本身的 OCaml 代码可以快速重新提取，而证明文件可以并行重新检查。

布尔判定优先

类型检查、lattice 比较、指令匹配等操作优先使用布尔函数（bool）而非命题（Prop）。布尔函数提取后直接变成 OCaml 代码中的 if 分支，命题则会被擦除。当需要在证明中使用布尔判定的含义时，附带一个 reflect 或 _spec 引理把 bool 和 Prop 桥接起来。

1
2
Lemma ble_sound:
  forall x y, ble x y = true -> forall v, vmatch v x -> vmatch v y.

Notation 与 Tactic 的克制使用

CompCert 几乎不定义自定义 Notation，也不大量使用 Ltac 宏。复杂的自动化（如 Constpropproof.v 中的 omega/lia 调用）限于局部。这使得代码对新读者更易理解，但代价是某些证明比使用 SSReflect 的项目冗长。

Module System 的实际应用

Kildall.v 用 Coq 的模块系统参数化 lattice 和求解策略。模块签名定义了 lattice 需要满足的接口（bot、lub、ble、wf 等），具体的 lattice 实例（如 ValueDomain 中的 AVal）实现该签名。这种模式在 MathComp 中也有类似物（Canonical Structure），但 CompCert 选择了模块系统因为它与 OCaml 的模块系统对齐得更好，提取后的代码结构更清晰。

动手实验

本地构建 CompCert

1
2
3
4
git clone https://github.com/AbsInt/CompCert.git
cd CompCert
./configure x86_64-linux   # 或 x86_64-macos
make -j4

构建时间约 30–60 分钟（取决于机器性能和 Coq 版本）。构建完成后 ccomp 是可执行的编译器。

阅读 Constprop 的建议路径

  1. 先读 backend/ValueDomain.v 前 200 行，理解 aval 和 vmatch
  2. 跳到 backend/Constprop.v 的 transf_instr，看变换逻辑
  3. 读 lib/Kildall.v 的模块签名（Module Type SEMILATTICE），不需要看证明
  4. 最后读 backend/Constpropproof.v 的 transf_step_correct 引理，看仿真步骤的证明结构
  5. 用 Print Assumptions transf_program_correct. 检查信任边界

替换 pass 实验

尝试写一个极简的 RTL pass：把所有 Iop (Ointconst n) 中 n = 0 的指令替换为 Iop (Oxorimm Int.zero) r r（用 xor 自身实现清零）。这个变换在语义上等价，但需要证明：

1
2
Lemma xor_self_zero: forall r rs,
  rs # r = Vint (Int.xor (rs # r) (rs # r)).

这个练习的目的是体验 CompCert 风格的仿真证明流程，而不需要处理完整的数据流分析。

练习

  1. 在 ValueDomain.v 中找到 vmatch 的定义，解释为什么 vmatch (Vint n) Vtop 成立而 vmatch (Vint n) (I m) 要求 n = m。

  2. Constpropproof.v 中的 match_states 使用了 Mem.extends 而非 Mem.inject。查阅 common/Memory.v 中两者的区别，解释为什么 Constprop 只需要 extends（提示：Constprop 不改变内存布局，不引入新的内存块）。

3.（挑战）阅读 backend/Deadcodeproof.v 的 match_states，与 Constprop 的版本对比。Deadcode 使用了 Mem.magree（memory agreement）而非 Mem.extends。解释这个选择的原因，以及 magree 如何允许死存储被删除。

参考资料