Pass：Allocation

1. 目标与位置

• 位置：backend/Allocation.v（验证器） + backend/Regalloc.ml（寄存器分配器）
• 输入/输出：RTL.program → LTL.program
• 目标：进行寄存器分配，并对外部分配结果进行形式化验证。

2. 核心思想

• 分配器（OCaml）：
  • RTL → XTL → 死代码消除
  • 构建干涉图并着色（IRC）
  • 插入 spill/reload，直到满足约束
• 验证器（Coq）：
  • 检查 LTL 是否正确实现 RTL 语义
  • 通过数据流分析建立 RTL 寄存器与 LTL 位置的等式约束

3. 关键数据结构与函数（Coq 侧）

• equation / eqs：表示 RTL 寄存器与 LTL 位置的等价关系。
• transfer / analyze：后向数据流分析，验证搬运与调用约束。
• check_function：结构检查 + 数据流验证。
• transf_program：程序入口。

4. 关键约束

• 调用约定：函数调用处必须满足 caller/callee-save 规则。
• 类型兼容：寄存器与位置类型必须一致。
• 双字长/拆分：对 64 位值在 32 位架构上的拆分有专门约束。

5. 与前后 pass 的接口

• 前：Unusedglob
• 后：Tunneling

6. 常见边界与约束

• 若外部分配器生成的 LTL 不满足验证器，编译失败。
• 约束严格依赖于 ABI 与架构设定。