模块分析：common

1. 角色定位

common/ 是所有 IR 与语义的共享基础层，提供： - AST 基础类型、操作与内建语义（AST.v, Values.v, Mem* 等） - 小步语义框架、事件/轨迹、全局环境 - 链接、可分离性与类型相关的通用性质

2. 关键文件与实现细节

2.1 AST.v

• 定义 IR 共用的“弱类型”体系：typ, xtype, signature 等。
• 定义 calling_convention，用于描述变长参数、返回结构体等 ABI 信息。
• memory_chunk 类型定义不同大小/有符号访问方式，是 load/store 语义与后端指令选择的基础。

2.2 Memory.v

• 定义内存模型 mem：
  • mem_contents: block -> offset -> memval
  • mem_access: 权限映射（Cur/Max + 权限等级）
  • nextblock: 线性增长的 block id
• 核心操作：load, store, alloc, free 的语义化封装
• perm/range_perm 的权限推理；在证明中广泛使用
• 采用“块 + 偏移”模型，配合 Memdata/Memtype 描述内存值与权限

2.3 Events.v

• 事件与可观察行为模型：Event_syscall, Event_vload, Event_vstore, Event_annot
• 定义 trace 和 traceinf，用于描述有限/无限执行轨迹
• 用于各语言语义与编译正确性证明中的可观察等价

2.4 其他核心文件

• Values.v：值域（整数/浮点/指针）语义及运算
• Globalenvs.v：全局环境、符号表、函数/全局变量解析
• Smallstep.v：小步语义框架（step/reachability/trace）
• Linking.v：程序链接与组合推理
• Sections.ml/.mli：区段与链接属性（对目标平台重要）
• Switch.v/Switchaux.ml：switch 语句规范化与分析

3. 实现风格与抽象

• 共通层几乎全部用 Coq 定义，可被多个 IR 复用
• OCaml 文件主要用于打印或与外部工具交互（如 Sections.ml, PrintAST.ml）

4. 与其他模块的耦合点

• cfrontend/ 与 backend/ 依赖 AST/Memory/Events/Values
• cparser/ 最终输出的 Csyntax 与 common/ 类型系统一致
• driver/ 与打印模块共享 Sections 与诊断工具