CompCert 源码总体分析（总览）

1. 仓库定位与总体结构

• 这是 CompCert 的源码与证明组合仓库，包含：
  • 形式化定义与证明（Coq，.v）
  • 由 Coq 抽取或与抽取代码协同的 OCaml 实现（.ml/.mli）
  • 目标架构相关模块（arm/, aarch64/, powerpc/, riscV/, x86/ 等）
  • 运行时支持库（runtime/）
  • 工具与测试（tools/, test/）
• 顶层核心目录：
  • cparser/：C 语法解析 + 语义化/消歧 + 语法规范化
  • cfrontend/：CompCert C 语义（Csyntax）到 Clight/Cminor 等前端 IR
  • backend/：后端优化与代码生成（Cminor/RTL/LTL/Mach/Asm 等）
  • common/ + lib/：共享数据结构、内存模型、事件与语义框架
  • driver/：编译器驱动与命令行
  • export/：clightgen 导出 Coq AST
  • debug/：DWARF/debug 信息生成
  • runtime/：补充运行时函数
  • flocq/：浮点运算形式化库
  • MenhirLib/：Menhir 解析器验证相关库

2. 编译流水线（高层）

该流水线的精确组合定义在 driver/Compiler.v，驱动入口在 driver/Driver.ml。

2.1 源码到 AST

1. 预处理：driver/Frontend.ml 调用外部预处理器（Configuration.prepro）并设置宏
2. 解析 + 语义化：cparser/Parse.ml
   • Lexer + Menhir parser 生成 Cabs
   • Elab 将 Cabs 变换为简化/类型化的 C AST
   • transform_program：Unblock、SwitchNorm、PackedStructs、StructPassing、Rename
3. 生成 CompCert C：cfrontend/C2C.ml 将前端 AST 转为 Csyntax

2.2 语义与 IR 变换

流水线由 Compiler.transf_*_program 定义（driver/Compiler.v）： - Csyntax → SimplExpr → Clight - Clight → SimplLocals → Csharpminor - Csharpminor → Cminorgen → Cminor - Cminor → Selection → CminorSel - CminorSel → RTLgen → RTL - RTL 级优化与后端： - Tailcall → Inlining → Renumber - Constprop → Renumber - CSE → Deadcode → Unusedglob - Allocation（寄存器分配） - Tunneling → Linearize → CleanupLabels - Debugvar（可选） - Stacking → Mach - Asmgen → Asm - 驱动层随后调用 Asmexpand.expand_program（架构相关）做汇编级扩展

3. 驱动层执行路径（ccomp）

• driver/Driver.ml 是 ccomp 的主入口：
  • 解析命令行
  • 预处理/编译/汇编/链接阶段调度
  • 通过 Compiler.transf_c_program 构建完整编译流水线
• driver/Frontend.ml 负责宏与 ABI 相关设置，并初始化 Machine.config

4. 形式化证明与抽取

• 大部分语义与变换核心在 .v 文件中定义
• extraction/ 目录负责抽取配置
• 后端的核心算法多数在 Coq 中实现，OCaml 中的 .ml 多用于：
  • 驱动/工具
  • 打印/序列化/调试
  • 与外部工具链的集成

5. 目标架构抽象

• 架构相关目录提供：
  • 指令集/寄存器描述（Asm.v, Machregs.v, Op.v）
  • 选择/组合/常量传播等特定规则（SelectOp, CombineOp, ConstpropOp, NeedOp）
  • ABI/调用约定（Conventions1.v）
  • 汇编生成和扩展（Asmgen.v, Asmexpand.ml）

6. 文档与可执行工具

• doc/：man page 与网页
• export/：clightgen 工具生成 Coq 版 AST
• tools/：构建辅助脚本

7. 子报告索引

• docs-llm/module-common.md
• docs-llm/module-lib.md
• docs-llm/module-cparser.md
• docs-llm/module-cfrontend.md
• docs-llm/module-backend.md
• docs-llm/module-driver.md
• docs-llm/module-export.md
• docs-llm/module-debug.md
• docs-llm/module-arch.md
• docs-llm/module-runtime.md
• docs-llm/module-flocq.md
• docs-llm/module-menhirlib.md
• docs-llm/module-tools-tests.md
• docs-llm/module-coq-extraction.md