③ 语义推断：从 RIS 到 DeviceSpec

RIS 是「这个驱动怎么访问硬件」的序列；DeviceSpec（.dspec）是「这个设备是什么」的后端无关语义模型。实现位于 spec.py（数据结构）、spec_infer.py（推断逻辑，1,079 行）、subsystem.py（子系统摘要，1,487 行）。

3.1 数据结构（spec.py）

结构	内容
`DeviceSpec`	device 头（名称/类/源码）、state 字段、resource、register 表、invariant、function 列表
`FunctionSpec`	函数签名、role（probe/read_config/write_config/interrupt_*…）、source 位置、context（thread/boot/irq）、callback 绑定、bind 映射、RIS 引用、effect 列表、ensure 契约
`FactsSpec`	includes、structs、constants、callbacks、resources、error_paths、helper_calls、source_snippets —— 给 LLM 合成的源码事实

3.2 推断流程（spec_infer.py）

infer_device_spec(extraction)      # 寄存器表/资源/state ← FormalRIS register_map + RIS 操作
infer_function_specs(extraction)   # 每个 module → FunctionSpec（role/context/callback/effect）
infer_facts(extraction)            # 常量、结构体、回调表、资源获取 → FactsSpec
callback_binding_analysis(...)     # 回调字段 ↔ 函数绑定关系分析

register 表：从 FormalRIS 的 Symbolic 访问 + 宏表构建 register NAME: Bn at base + 0x…。
role / context：由函数名与调用上下文推断 —— probe → boot 上下文；irq_handler → irq 上下文；ops.get/set → thread 上下文 + read/write_config role。
effect / ensure：从 RIS 操作归纳 —— writes_register(GPIOIE)、reads_config(offset)；ensure 是意图级契约（如 device_state == READY）。

3.3 真实示例：gpio-pl061.dspec（节选讲解）

产物 artifacts/output/portable-gpio-pl061/gpio-pl061.dspec：

device gpio-pl061 {
  class gpio_controller
  state {
    base: MmioBase
    num_irqs: UInt
  }
  resource mmio0: MmioResource { required true bind base }
  resource irq0: IrqResource { required true }
  register GPIODIR: B1 at base + 0x400   -- 宏 GPIODIR(0x400) 落进寄存器表
  register GPIOIS: B1 at base + 0x404
  register GPIOIBE: B1 at base + 0x408
  register GPIOIEV: B1 at base + 0x40c
  register GPIOIE: B1 at base + 0x410
  register GPIOMIS: B1 at base + 0x418
  register GPIOIC: B1 at base + 0x41c
  invariant forall line: UInt. line < num_irqs -> valid_interrupt_line(line)

state：从 pl061->base 解引用模式推断 base: MmioBase。
resource：devm_platform_ioremap_resource 等 API 识别为 MMIO 资源获取，required true bind base 表达「probe 必须拿到它」。
register 表：B1（字节宽）+ 偏移 —— 生成阶段 readb(GPIODIR) 就对应 base + 0x400。
invariant：从中断线号合法性检查归纳。

函数级契约（同文件节选）：

  function pl061_direction_input(gc: DeviceState, offset: UInt) -> UInt {
    role write_config
    source "gpio-pl061.c:69"
    context thread
    callback gpio_chip.direction_input      -- 挂在 gpio_chip ops 表哪个槽
    bind dev: DeviceState from pl061
    bind base: MmioBase from pl061->base     -- 参数/字段到设备模型的绑定
    ris pl061_direction_input                 -- 指向同名 RIS module
    effect writes_register(GPIODIR)
    effect writes_config(offset)
  }
  function pl061_irq_handler(desc: LogicalIRQ) -> Void {
    role interrupt_handler
    context irq
    callback gpio_irq_chip.parent_handler
    ris pl061_irq_handler
    effect handles_interrupt()
    ensure interrupt_serviced
  }
  function pl061_probe(adev: DeviceState, id: DeviceState) -> UInt {
    role probe
    context boot
    callback amba_driver.probe
    require resources_available
    ris pl061_probe
    effect initializes_device()
    ensure device_state == READY
  }

这段是「后端无关」的关键：callback gpio_chip.direction_input 说的是语义位置（GPIO 子系统的 ops 槽位），而不是具体内核结构体 —— Linux 后端生成时才知道要填 struct gpio_chip 的哪个成员；harness 后端则根本不需要 ops 表。

3.4 子系统摘要（subsystem.py，1,487 行）

不同子系统有各自的回调/访问模式，硬编码在提取器里会破坏泛化。subsystem.py 提供版本化的子系统库摘要：

GPIO：从 typed gpio_generic_chip_config 合成 callback；动态 gpio_irq_chip.init_hw 绑定按字段语义归类。
SDHCI / virtio：accessor/ops table 与 config/virtqueue 分域记录 —— virtio 的 config 空间是 subsystem state，不伪装成 MMIO。
clock provider：保留多套 clk_ops、纯标量 rate 算术、父时钟/provider 注册及 OF 变体。
PCI：Sodaville 案例 —— PCI ID、12-line GPIO generic 行为、mask/unmask/EOI IRQ lifecycle 由版本化源码保守恢复。

效果：冻结矩阵里原本 7 个 no_register_access 驱动降为 0；zero-shot holdout 12 个驱动编译 12/12 —— 摘要让系统能处理「没见过的驱动」。

3.5 地址精度哲学（再次强调）

README 原文：

地址分类是刻意分开的：只有可静态命名的访问记为 Symbolic；
常量偏移和运行时索引分别保留为 Fixed 与 Computed，
不会伪造成 "100% symbolic"。

Computed 地址保留完整动态 offset（如 *off[0x0]）；只有包含不安全调用或未绑定成员的 computed expression 才阻止 readiness。switch/if 的互斥 RMW 路径合成为嵌套 Ite，保留每条路径对原始读值的独立变换；仍无法解析的值保留 Top 并阻止 strict。

3.6 多源合并（extractor.py: _merge_facts）

多 TU 驱动的 facts 合并规则：

includes / structs 去重；常量与 callback 冲突 → 警告并保留首个（不静默覆盖）。
resource 按 (acquisition, binds_to) 去重；error_paths / helper_calls 取并集。
source_snippets 逐条去重。

跨 TU 的 MMIO 摘要传播由 call_graph.py 的 extract_multi_with_inlining 完成：内部调用边 974 条，其中 223 条跨 TU 边全部解析；578 条调用边传播了 MMIO 摘要（README C 阶段数据）。C67X00（4 C）、ASPEED vHub（5 C）、DWC2 dual-role（10 C，19 TU / 27,447 LoC）三后端均 3/3 编译。

下一章：.dspec + .bind 如何驱动三个后端生成 C 代码，以及 generation contract 如何保证每个硬件访问都「有据可查」。