模块分析：cfrontend

1. 角色定位

cfrontend/ 负责将 cparser 输出的语义化 AST 转换为 CompCert 形式化前端 IR，并定义 C 语义、类型系统与初始化语义。

2. 核心文件与实现细节

2.1 C2C.ml

• 将 cparser 产出的 C AST 转换为 Csyntax。
• 构建 atom_info 哈希表：记录符号的存储类、大小、对齐、区段、访问模式与 inline 标记。
• atom_is_external / atom_needs_GOT_access 根据 PIC/PIE 与 ELF/Mach-O 规则判断访问方式。
• 初始化全局 composite 环境 comp_env。

2.2 SimplExpr.v（Csyntax → Clight）

• 目标：将副作用从表达式中拆出，生成 Clight。
• 使用 gensym 单子分配临时变量；保证转换过程中变量唯一。
• 关键逻辑：
  • makeif 做常量条件折叠
  • Ederef'/Eaddrof' 消除 *&/&* 组合
  • transl_valof/make_assign 对 volatile 的读写转成 builtin
  • 处理 bitfield 与 volatile 组合时的语义细节

2.3 SimplLocals.v

• 简化局部变量使用方式，标准化存储形式
• 为后续 Csharpminor/Cminor 翻译准备更规整的局部环境

2.4 Initializers.v

• 编译期常量表达式求值：
  • constval 解释常量表达式，指针值以 Vptr id ofs 形式符号化
  • 与运行时语义一致的 sem_* 规则
• 初始化数据构造：
  • state 记录当前写入位置、数据列表与预期大小
  • normalize 将非字节 init 数据拆成字节序列

2.5 语义/类型文件

• Ctypes.v、Csyntax.v、Csem.v、Cstrategy.v、Cexec.v
• 定义 CompCert C 的类型系统、动态语义与执行策略

3. 关键输出

• Csyntax / Clight / Csharpminor / Cminor
• 为 backend/ 提供后端 IR 入口

4. 与后端的接口

• Cminorgen.v 将 Csharpminor 转为 Cminor
• 之后进入 Selection 做目标相关指令选择