模块分析：backend

1. 角色定位

backend/ 负责中后端优化与机器码生成，核心变换基本在 Coq 中实现，并经抽取得到可执行代码；OCaml 侧主要负责打印、寄存器分配辅助与特定算法实现。

2. 主要 IR 与阶段

• Cminor → CminorSel（Selection.v）
• CminorSel → RTL（RTLgen.v）
• RTL → LTL → Linear → Mach → Asm

3. 关键变换与实现细节

3.1 Instruction Selection (Selection.v)

• 目标：利用目标 ISA 的复合操作与地址模式。
• 自底向上重写表达式：
  • sel_unop / sel_binop 映射到目标相关 SelectOp/SelectLong
  • load / store 通过 addressing 识别寻址模式
• 使用 SelectDiv, SplitLong 等辅助模块

3.2 RTL 生成 (RTLgen.v)

• 使用“状态 + 错误”单子构建 CFG：
  • state 包含 st_nextreg, st_nextnode, st_code
  • add_instr 在 CFG 中追加新节点
• 通过 state_incr 维护状态单调性证明（CFG 只增不改）

3.3 Inlining (Inlining.v)

• 维护可内联函数环境 funenv
• 由 OCaml 侧 inlining_analysis 和 should_inline 提供内联启发式
• 内联时构造 context，对 PC、寄存器、栈位置进行统一偏移/重定位

3.4 常量传播、CSE、死代码

• Constprop.v、CSE.v、Deadcode.v 等在 Coq 中实现
• 以 RTL 为载体，配合 ValueAnalysis / ValueDomain

3.5 寄存器分配 (Regalloc.ml + Allocation.v)

• OCaml 侧实现核心算法：
  • RTL → XTL → Deadcode
  • 构建干涉图并调用 IRC 着色
  • 根据 spill 结果插入 spill/reload，循环直到稳定
• 处理 two-address 指令、长整型拆分等架构约束

3.6 CFG 线性化与栈布局

• Linearize.v：CFG → 线性指令序列
• CleanupLabels.v：清理无用标签
• Stacking.v：分配栈帧、保存/恢复寄存器

3.7 Asm 生成

• Asmgen.v 将 Mach 转成 Asm
• 之后驱动层调用架构相关 Asmexpand 完成最终汇编扩展

4. OCaml 辅助与打印

• PrintRTL.ml, PrintLTL.ml, PrintMach.ml, PrintAsm.ml
• JsonAST.ml / Json.ml 提供 JSON 序列化能力
• Asmexpandaux.ml, Linearizeaux.ml 等为 Coq 抽取后的辅助库

5. Debug 支持

• Debugvar.v 在 RTL → Mach 过程中插入局部变量调试信息
• 配合 debug/ 生成 DWARF