② 提取器实现（extractor/）

提取器把 C 驱动变成 FormalRIS，约 15,600 行 Python。主编排在 extractor.py，模块 docstring 一句话概括全流程：

parse TU → collect macros → find target functions
→ dataflow extraction (with wrapper inlining)
→ intent annotation → build FormalRIS

2.1 入口与配置（extractor.py · cli.py）

ExtractorConfig 是贯穿全管的配置对象，关键字段：

多源入口 _extract_multi 逐 TU 解析 → 合并宏表 → 可选 SVF 链接分析 → 交给 extract_multi_with_inlining。模块名消歧（_assign_multi_module_names）：同名 static 函数重命名为 {源文件stub}__{函数名}[__N]，外部符号冲突直接 ValueError —— 绝不静默合并 C 符号。

2.2 编译上下文（compile_context.py）

要得到与真实内核一致的 AST，必须知道驱动实际是怎么编译的。优先级：

1. compile_commands.json（如果提供）
2. Kbuild 的 .o.cmd 文件（kbuild_cmd_path 自动发现）—— 记录真实 include 路径、-D 宏、优化选项

_sanitize_arguments 清洗 token（去 -o/-c 输出项等），CompileContext.display() 输出审计信息，来源与 SHA 写进 analysis metadata —— 这是「可复现」的地基。

2.3 AST 模型（ast_model.py）

• Func / CallSite：函数与调用点的轻量封装（名称、static 性、参数、位置、module_name）。
• target_functions(tu, file)：筛出本文件定义的目标函数；target_mmio_globals 收集 MMIO 全局（BASE_FIELDS 集合里的 base/ioaddr/virtbase… 字段名）。
• walk_with_conditions：深度遍历，产出 (cursor, cond_stack) —— 每个 AST 节点携带其所在的分支谓词栈（数据流用它记录条件 op）。
• walk_with_control：产出 (cursor, control_stack) —— 结构化 Cond/Loop 帧（formalize 时用它）。
• continuation_guards：把「简单参数型 early return / 可界定的前向 goto」转成 continuation guard（负条件），后向 goto 与未证明循环交给 control accounting 显式阻塞。
• callback_entry_functions / callback_entry_symbols：从 struct xxx_ops 初始化器反向找出回调入口 —— 回调也是提取目标。

2.4 宏表（macros.py）

内核驱动大量用宏定义寄存器偏移（#define GPIODIR 0x400）。MacroTable.build(tu, source, source_text) 收集驱动自身与头文件里的宏，_eval_int_expr 做常量求值，支持 BIT(n)、算术折叠。地址解析时：pl061->base + GPIODIR → 宏值 0x400 → Symbolic{device, GPIODIR} 并登记 register_map（dspec 里就是 register GPIODIR: B1 at base + 0x400）。多源时 combined_macros.merge 检测同名宏冲突。

2.5 调用图与有界内联（call_graph.py）

驱动里的寄存器访问常藏在包装函数里（如 pl061_write 内部才调 writeb）。方案是过程间有限深度内联：

• extract_with_inlining(funcs, macros, tu, source_lines)：按调用序提取；_eligible_call_edges 决定哪些边可内联（本文件函数、非黑名单、深度 ≤ max_inline_depth）。
• _selective_frontier_call_closure / _direct_evidence_frontier：只内联能贡献访问证据的调用，保留每个 helper 未覆盖的 definition-owned evidence frontier —— 访问不会因为内联而消失。
• _coverage_aware_inlined_names：被 dedup 的 helper 名追踪，用于 C15 的 coverage-aware callee rescue。
• build_inline_cache：函数级提取缓存，多源/多入口复用。
• 间接调用（函数指针表）通过 indirect.py 的 indirect_targets 静态解析（从 .ops = { .get = pl061_get_value } 这类初始化器推导）。

2.6 流敏感数据流（dataflow.py，1,487 行）

模块 docstring：

"Walks each function's calls in source order, maintaining an abstract store
(var -> AbsVal). At each MMIO call it resolves the address argument to a
RegAddr via the store + macro table, records branch conditions, and detects
read-modify-write patterns (readl→modify→writel on the same address)."

核心数据结构 Op（后续所有阶段的传输对象）：

@dataclass
class Op:
    kind: str                 # Read/Write/ReadModifyWrite/Transaction*/State*/...
    addr: dict                # RegAddr: Fixed|Symbolic|Computed
    width: int
    value: Optional[str]      # 写值/变换的原始 C 文本
    condition: Optional[str]
    intent: str = "Unknown"
    source_loc / line         # 源码位置
    reg_name: Optional[str]   # 解析出的寄存器宏名
    var: Optional[str]        # Read 的 LHS 变量
    cond_stack: list          # 分支谓词栈（formalize 用）
    control_stack: list       # 结构化 Cond/Loop 帧
    evidence: dict            # 可审计来源证据
    state_field / transaction # State 与事务扩展

• 表达式求值：eval_expr(text, store, macros) → AbsVal。先 _strip_casts 剥类型转换（正则匹配 (u32)/(volatile unsigned long) 等），再 _split_top 顶层切分二元运算，对 base + offset 结构用 _combine_add 合并成 BasePtr + Offset。
• 地址解析：resolve_addr(text, store, macros) 产出 (RegAddr, reg_name) —— 宏表命中 → Symbolic；纯常量 → Fixed；含运行时变量 → Computed（保留完整表达式）。
• RMW 检测：维护「上一个 Read 的地址/变量」，遇到同地址 Write 且值表达式依赖该读变量时，合成 ReadModifyWrite（写入 read_var 与 transform），避免生成阶段重复读硬件。
• 条件跟踪：walk_with_conditions 提供的 cond_stack 原样挂到每个 Op 上。

2.7 污点抽象域（taint.py）

抽象存储的值域设计（对应 Linux 驱动的典型寻址模式）：

AbsVal = BasePtr(变量) | Offset(常量) | ReadTaint(来源读) | Const | SymExpr | Top
addr_fixed(base, off)      # 常量偏移
addr_offset(base, delta)   # 变量偏移
addr_indirect(ptr)         # 指针间接
addr_equal(a, b)           # 地址相等判定（RMW 用）
addr_base_of(a)            # 取基址

它能回答的关键问题：两个地址参数是否指向同一寄存器（RMW 判定）、地址基址是什么（Symbolic 命名）、偏移是否静态可知。

2.8 MMIO 分类与事务（mmio.py · transactions.py）

• mmio.py：识别 MMIO 访问家族 —— readl/readw/readb、writel/writew/writeb、ioread*/iowrite*、ioremap 基址传播；accounting.py 还捕获直接 volatile 解引用与inline asm 访问（_is_volatile_lvalue / _discover_opaque_accesses），全部进入 access accounting —— 无法 lowering 的访问不会静默消失。
• transactions.py：regmap / I2C/SMBus / MFD 事务契约 —— 记录 transport、target、selector、element_width、buffer/count、update_mask/value。这些被建模成 Transaction* op，绝不伪装成 MMIO 地址（README 明确：virtio config/virtqueue 也建模为 subsystem state）。

2.9 控制流（control.py）

_function_cfg 为每个函数构建显式 CFG（block 节点 + pred/succ 边，标注 break/goto/backedge/loop header）；immediate() 计算支配/后支配关系。产物 build_control_accounting 记录哪些控制结构被证明、哪些阻塞了 strict —— 是「未证明循环显式阻塞」的实现者。

2.10 SVF 别名分析（alias.py，可选）

真实驱动的 MMIO 指针常经过多层赋值/别名。SVF 路线：

1. _generate_stubbed_bc：clang 编译成 LLVM IR（对缺失的内核符号打 stub），_assemble_ir 汇编成 bitcode。
2. 多源时 先链接所有 TU 的 bitcode 再跑一次 WPA（find_mmio_aliases_multi），记录 linked-bitcode SHA、工具版本、source provenance。
3. _parse_wpa_aliases：把 WPA 的变量 ID 映射回 C 名（_map_var_to_c_name + 行号定位 LHS），筛选 MMIO lvalue（_accept_mmio_lvalue）。

默认 off（快）；auto 失败降级警告；required 失败即终止。C67X00 required 运行成功链接 4 TU。

2.11 形式化（formalize.py）

把扁平 Op 流变成嵌套 FormalRIS 的三件事：

• Cond 嵌套：按 cond_stack 把共享分支谓词的最大连续 op 运行包成 Cond{guard, then_ops}（路径不敏感、不展开叉积）。
• 表达式解析：F.parse_expr(op.value) 把 C 值字符串解析进 Expr 代数（上一章讲过）；simplify_expr 折叠常量。
• 审计字段：_common_fields 计算 op_id / evidence / reliability / 三种 precision；_semantic_fields（State/Output）、_transaction_fields（事务）各有自己的精度规则。
• register_map：由解析后的宏表构建，写进 FormalRIS 头。

_to_risop 是 Op → RIS op 的分派器：Read 带 var、Write 带 value、RMW 带 transform+read_var、Transaction* 带 endpoint/payload/协议字段。