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 取地址等非法语义。
- 临时变量:
5. 与前后 pass 的接口
- 前:
Csyntax(来自 C2C)
- 后:
Clight(供 SimplLocals 与
Cshmgen 使用)
6. 常见边界与约束
- volatile/bitfield 与复合类型访问必须通过特定 builtin
或语句序列实现。
- 变换使用的临时变量需要在 Clight 层面声明与作用域维护。