① RIS 形式语言与数据模型

RIS（Register Interaction Sequence，寄存器交互序列）是 reharness 的核心产物。实现位于 src/extractor/formal.py（表达式代数 + Display 语法）与 src/extractor/formalize.py（扁平 Op 流 → 嵌套 FormalRIS）。

1.1 形式文法

直接引用 formal.py 模块 docstring 中的定义：

Expr   = Const | Var | BinOp{op,left,right} | Ite{guard,then,else}
       | Bits{hi,lo,expr} | Top
RegAddr= Fixed{base,offset} | Symbolic{device,register} | Computed(Expr)
RISOp  = Read | Write | ReadModifyWrite | TransactionRead
       | TransactionWrite | TransactionUpdate | StateRead | StateWrite
       | OutputWrite | Return | Delay | Cond | Seq | Loop
FormalRIS = {driver, version, modules[], register_map[], metadata}

设计要点：表达式域刻意很小（Const/Var/BinOp/Ite/Bits/Top），Top 表示「无法静态解析」，是 strict readiness 的显式阻塞器 —— 系统宁可拒绝也不猜。

1.2 表达式代数的实现（formal.py）

parse_expr —— 尽力而为的 C 表达式解析

把提取器拿到的值/条件字符串解析成 Expr dict。关键实现决策（按优先级从低到高逐层切分）：

BINOPS = ["==", "!=", "<=", ">=", "&&", "||", "<<", ">>", "<", ">",
          "|", "^", "&", "+", "-", "*", "/", "%"]

三元表达式：_split_ternary 用括号深度计数找顶层 ?/:，支持嵌套 Ite，产出 {"Ite": {guard, then, else}}。
二元运算：按上表顺序用 _split_top 在括号深度 0 处切分（正确处理 ->、<<、>> 不误切），左结合折叠成嵌套 BinOp。
一元运算：!x → Eq(x, 0)；~x → BitXor(x, 0xFFFFFFFF) —— 用现有 BinOp 代数表达，不新增节点类型。
BIT(n)：常量参数直接折叠成 1 << n 的数值；变量参数保留为 Shl(1, arg)。
字面量：十六进制/十进制 → Const；其余标识符/成员/调用 → Var（原样保留字符串）。

simplify_expr —— 常量折叠

对 BinOp 双常量的 19 种运算就地求值（& 0xFFFFFFFFFFFFFFFF 防溢出）；Ite 守卫为常量时直接选边，then/else 相同则合并；Bits 常量切片折叠。符号项（Var）永不触碰 —— 保证「不改变符号语义的折叠」。

expr_display —— 回写成人类可读

Formal Expr → 文本（⊤ 表示 Top），用于 .ris 文件输出。

1.3 地址分类：不伪装的精度哲学

分类	含义	示例（edu）
Symbolic	可静态命名的寄存器访问	`priv->mmio.IO_IRQ_STATUS`（宏解析后归入 register_map）
Fixed	常量偏移地址	`priv->mmio + 0x0`
Computed	运行时计算地址，保留完整动态 offset 表达式	`priv->mmio + *off[0x0]`（edu_read 的 file offset 寻址）

对应 formalize.py 中 _common_fields：address_precision = symbolic | fixed | computed | unknown（Computed 内含 Top 时降级为 unknown）。矩阵里 366 symbolic / 64 fixed / 41 computed 的统计就是这么来的，绝不把运行时索引伪造成「100% symbolic」。

1.4 操作类型与精度字段

Op	语义
`Read`	`var := R(width, addr)`，记录 LHS 变量名（`op.var`）
`Write`	`W(width, addr) = expr`
`ReadModifyWrite`	`RMW(width, addr) = transform`，保留 `read_var` —— 由 readl→modify→writel 数据流模式合成
`Transaction*`	regmap / I2C/SMBus / MFD 事务，显式区分 target、selector、scalar/buffer payload，不伪装成 MMIO
`StateRead/Write`	驱动私有状态字段（如 `pl061->csave_regs.*`）
`Cond / Loop / Seq`	结构化控制流：`Cond{guard, then_ops, else_ops}`、`Loop{guard, body}`

每个叶子 op 都带五个审计字段（formalize.py: _common_fields）：

{
  "op_id": "op_12",                    # 全局唯一，生成契约的锚点
  "evidence": {...},                   # 源码位置/调用栈/访问域
  "reliability": "Exact|Conservative|Unknown|Unsupported",
  "address_precision": "symbolic",     # symbolic|fixed|computed|unknown
  "value_precision": "exact|unknown",  # 值表达式含 Top 则 unknown
  "path_precision": "unconditional|syntactic",  # 是否有 cond_stack
  "access_domain": "mmio|regmap|i2c|mfd|source_state|unsupported_*"
}

reliability 的推导规则：非 MMIO 域 → Unsupported；地址或值 unknown → Unknown；路径是语法级条件 → Conservative；全精确 → Exact。

1.5 真实示例：edu.ris（QEMU 教学设备，全量）

这是 artifacts/output/edu/edu.ris 的完整内容 —— 最小但五脏俱全：

driver edu v0.1.0 {
  module edu_irq_handler {
    status := R(B4, priv->mmio.IO_IRQ_STATUS) -- Interrupt
    W(B4, priv->mmio.IO_IRQ_ACK) = status -- Interrupt
  }
  module edu_read {
    val := R(B4, priv->mmio + *off[0x0]) -- Status
  }
  module edu_write {
    W(B4, priv->mmio + *off[0x0]) = val -- Config
  }
  module edu_pci_probe {
    dev_id := R(B4, priv->mmio.IO_ID) -- Status
  }
}

module = 源码中的一个函数（edu 有 4 个目标函数）。
-- 注释 是提取器标注的 intent（Interrupt/Status/Config/Init），来自 intent.py 的启发式（读状态寄存器→Status，写配置→Config…）。
priv->mmio.IO_IRQ_STATUS：Symbolic 地址 —— IO_IRQ_STATUS 是宏，被解析后进入 register_map（offset 0x24）。
priv->mmio + *off[0x0]：Computed 地址 —— 内核 file_operations 的 off 参数，运行时才知道偏移。
irq_handler 的 readl(STATUS) → writel(ACK, status) 被识别为独立的 Read + Write（不是 RMW —— 写的是另一个寄存器）。

1.6 真实示例：gpio-pl061.ris（丰富语法）

节选 artifacts/output/portable-gpio-pl061/gpio-pl061.ris 讲解三种高级形态：

  module pl061_get_direction {
    IF (readb(pl061->base + GPIODIR) & (0x1 << offset)) {   -- Cond：条件读
      r1 := R(B1, pl061->base.GPIODIR) -- Config
    }
  }
  module pl061_direction_input {
    gpiodir := R(B1, pl061->base.GPIODIR) -- Config
    RMW(B1, pl061->base.GPIODIR) = gpiodir -- Config   -- 读改写合成
  }
  module pl061_irq_type {
    gpioiev := R(B1, pl061->base.GPIOIEV) -- Status
    gpiois  := R(B1, pl061->base.GPIOIS)  -- Status
    RMW(B1, pl061->base.GPIOIS)  = gpiois  -- Config
    RMW(B1, pl061->base.GPIOIBE) = gpioibe -- Config
    RMW(B1, pl061->base.GPIOIEV) = gpioiev -- Config
  }
  module pl061_suspend {
    pl061->csave_regs.gpio_dir := R(B1, pl061->base.GPIODIR) -- Config
    ...
  }
  module pl061_resume {
    W(B1, pl061->base.GPIOIS) = pl061->csave_regs.gpio_is -- Config
    ...
  }

Cond：IF (guard) { ops } —— 路径不敏感：共享同一分支谓词的最大连续 op 运行组成一个 Cond 块（formalize.py 按 op.cond_stack 嵌套）。
RMW：源码 gpiodir = readb(base+GPIODIR); gpiodir |= BIT(offset); writeb(gpiodir, ...) 被数据流识别为 read-modify-write，合成单个 RMW 节点并保留变换表达式。
State 持久化：suspend 把寄存器读到 pl061->csave_regs.*（StateWrite），resume 写回 —— 跨函数的状态流被显式建模。
pl061_irq_type 的三连 RMW：GPIOIS/GPIOIBE/GPIOIEV 三个配置寄存器互不相同的 read-modify-write 被分别保留，每个 RMW 的 transform 只依赖各自的原始读值。

1.7 结构化输出与遍历

formal.py 同时输出 serde 兼容的 FormalRIS JSON（--json-output，产物里叫 *.formal.json）与 .ris 文本 —— 实验聚合全部走 JSON，论文表格机器可读。
walk_leaf_ops / walk_all_ops：递归遍历嵌套结构，生成器与 oracle 都用它做统一遍历；formalize.py 的 save_formal_text 负责文本渲染。
循环：可证明的规范 for 循环（Z3 检查有界性，见 smt.py）生成 Loop；未证明循环由 control accounting 显式阻塞，不伪造 receipt。

下一章预告：这些 .ris 是怎么从 C 源码里挖出来的？下一章深入提取器的 AST 模型、调用图内联、数据流/污点三件套。