Pass：SimplExpr

1. 目标与位置

• 位置：cfrontend/SimplExpr.v
• 输入/输出：Csyntax.program → Clight.program
• 目标：把 CompCert C（Csyntax）中带副作用的表达式规范化为 Clight 的“表达式无副作用”形式，保证后续前端/后端更易分析与证明。

2. 核心思想

• 将表达式求值中的副作用提取为显式语句序列。
• 使用 gensym 单子生成临时变量，保证表达式拆解后语义等价。
• 对 volatile 访问、bitfield、取址/解引用等做语义保持的重写。

3. 关键数据结构与函数

• generator：记录 gen_next 与 gen_trail，用于生成新临时变量。
• result / mon：依赖型单子，保证 gensym 的单调性。
• 关键构造器：
  • makeif：对常量条件做折叠（若可判定）。
  • Ederef' / Eaddrof'：消除 *& / &* 的组合。
  • transl_valof / make_assign：处理 volatile 读写与 bitfield 访问。
  • transl_expr / transl_stmt：表达式与语句翻译主入口。
• 程序入口：transl_program。

4. 具体变换要点

• 副作用拆分：
  • 对赋值、逻辑短路、条件表达式等生成显式语句序列，保证 Clight 的表达式纯度。
• volatile 语义：
  • 对 volatile 读写生成 Sbuiltin EF_vload/EF_vstore 或临时变量读写。
• bitfield 语义：
  • 区分全字段与 bitfield，避免对 bitfield 取地址等非法语义。
• 临时变量：
  • 统一使用 gensym 分配，保持变量唯一性。

5. 与前后 pass 的接口

• 前：Csyntax（来自 C2C）
• 后：Clight（供 SimplLocals 与 Cshmgen 使用）

6. 常见边界与约束

• volatile/bitfield 与复合类型访问必须通过特定 builtin 或语句序列实现。
• 变换使用的临时变量需要在 Clight 层面声明与作用域维护。