reharness: 基于AST分析的C设备驱动
形式化寄存器交互规约提取

1. 引言

设备驱动是操作系统内核中最庞大、最易出错的组件[1,2]。单个Linux版本包含数万个驱动源文件，每个都通过内存映射I/O（MMIO）读写、中断处理和框架回调注册编码了复杂的硬件协议。尽管数十年来对驱动可靠性的研究不断推进[3,4,5]，驱动的寄存器级行为仍然在很大程度上是隐式的——通过宏、指针运算和抵抗自动推理的临时数据结构在C源码中表达。

核心挑战在于提取：将原始C源码转化为机器可读的规约，描述驱动对硬件寄存器做什么、以什么顺序、在什么条件下。这一规约是验证[6]、测试[7]、安全语言翻译[8]和AI辅助驱动合成[9]的基础。

然而，现有提取工具运行在表层。它们使用正则表达式匹配MMIO函数调用（例如 readl、writel），但在四种常见模式上失败：(1)通过 #define 宏定义的寄存器偏移，在正则匹配下解析为零；(2)隐藏在从驱动入口点调用的包装函数中的MMIO访问；(3)控制寄存器访问路径的分支条件；(4)涉及基指针和偏移算术组合的地址表达式。

本文提出 reharness，一个通过AST级分析解决这些局限的管线。reharness使用libclang以完整预处理上下文解析C翻译单元，使其能够解析宏展开的寄存器偏移（例如 GPIO_INT_EN → 0x20），而这些对基于正则表达式的工具是不可见的。它通过受控深度的过程间调用图分析内联包装函数，以暴露隐藏在辅助函数中的MMIO操作。它通过路径不敏感的谓词堆栈追踪分支条件，将保护表达式附到每个寄存器操作。关键的是，它执行流敏感数据流与污点追踪：识别 ioremap 调用为MMIO基指针源，追踪 readl 返回值为读-污点数据，并检测读-修改-写（RMW）模式——即读出的值被修改后写回同一地址。

reharness的输出是一种形式化寄存器交互序列（RIS）规约语言，设计为既人类可读又机器可解析。每个RIS模块记录一个驱动函数的寄存器操作序列，带有符号化寄存器名称、分支条件和语义意图标注。

在原始提取之上，reharness执行语义推断：将RIS模块提升为后端无关的函数规约（FunctionSpec），捕获函数的角色（例如 interrupt_ack）、执行上下文、状态绑定、效果以及Hoare式前后条件。函数规约被组合为设备级规约（DeviceSpec），建模设备的状态、资源、寄存器映射和不变量。这些形式化规约可与后端特定的绑定文件（.bind）配对，为多个目标生成驱动代码：用于测试的用户态存根、用于嵌入式系统的裸机C以及Linux内核骨架。

最后，reharness包含一个闭环LLM辅助合成模块：当确定性代码生成不足时（例如复杂的Linux子系统胶水代码），管线组装结构化输入包（RIS、设备规约、后端绑定、源事实、脚手架），并利用编译、静态和追踪验证反馈迭代修复LLM生成的候选代码。

本文做出以下贡献：

1. 一种形式化寄存器交互序列（RIS）语言，捕获带有符号化寄存器解析、分支条件和RMW检测的MMIO操作，作为驱动行为提取的规范中间表示。
2. 一个基于libclang的提取管线，具有流敏感数据流和污点追踪，克服了基于正则表达式方法的四个根本局限。
3. 从RIS模块到函数级和设备级形式化规约的后端无关语义推断，包括回调角色推断、状态绑定和效果建模。
4. 一个多后端代码生成框架，带有确定性测试存根、裸机和Linux后端，以及一个具有结构化验证反馈的闭环LLM辅助合成模块。
5. 对17个Linux设备驱动的评估，展示了100%符号化地址解析率和0.92的平均RIS质量得分。

2. 动机

2.1 正则表达式提取的局限

为激发reharness的动机，我们考察业界实践中的基于正则表达式的提取工具 driver-harness[10] 的失败模式。其方法使用正则表达式扫描C源码文本来检测MMIO调用。虽然轻量，但这一策略在真实驱动代码中无处不在的四种模式上系统性失败。

模式1：宏定义的寄存器偏移。Linux驱动通过预处理器宏定义寄存器布局：

#define GPIO_INT_EN   0x20
#define GPIO_INT_CLR  0x30
writel(0, base + GPIO_INT_EN);

匹配 writel(..., ... + ...) 的正则表达式能捕获调用点，但无法将 GPIO_INT_EN 解析为其数值0x20。基线工具默认将所有此类访问报告为偏移0，丢失了区分不同寄存器的关键信息。在我们的评估中，这导致GPIO和virtio-MMIO驱动中100%的寄存器访问被错误报告为位于偏移0。

模式2：包装函数。驱动通常将MMIO原语包装在辅助函数中：

static void gpio_setbit(u32 val, void __iomem *base, u32 off) {
    u32 r = readl(base + off);
    writel(r | val, base + off);
}

对主回调函数操作的正则表达式会遗漏 gpio_setbit 及类似包装函数内的所有MMIO操作。没有过程间分析，驱动的完整寄存器访问足迹是不完整的。

模式3：条件寄存器访问。寄存器序列通常依赖运行时条件：

if (type & IRQ_TYPE_EDGE_BOTH) {
    writel(val | BIT(line), base + GPIO_INT_BOTH_EDGE);
}

基线工具记录 writel 操作但丢弃保护条件，丢失了该写入仅发生在边沿触发中断这一语义上下文。

模式4：算术地址计算。基指针通常通过字段访问链计算：

struct ftgpio_gpio *g = gpiochip_get_data(gc);
readl(g->base + GPIO_INT_STAT);

解析 g->base 需要追踪初始化它的 ioremap 调用，而这又需要流敏感污点传播——远超正则表达式的能力范围。

2.2 设计目标

reharness旨在克服这些局限，同时保留下游工具链所需的三项基本属性：

1. 精确性：每次寄存器访问必须解析为源自源码级宏定义的具体符号名称和偏移，而非来自硬编码模式匹配。
2. 完整性：从驱动入口点可达的任何MMIO操作都不应被静默丢弃。包装内联和过程间分析必须在有界深度上覆盖完整调用图。
3. 形式化语义：输出必须是形式化规约语言，而非临时JSON格式，从而可直接用作验证、测试和代码生成工具的输入。

3. 系统总览

reharness组织为四个主要阶段的管线，如图1所示。

阶段1：RIS提取。提取阶段使用libclang解析C源码，从预处理记录构建宏偏移表，识别驱动入口点，并执行逐函数流敏感数据流分析。输出是形式化RIS规约，记录每个寄存器读、写和RMW操作，带有符号化寄存器名、分支保护和宽度标注。

阶段2：语义推断。推断阶段以后端无关语义丰富原始RIS模块。它从回调表注册（例如 .irq_ack = ftgpio_ack_irq → interrupt_ack）推断函数角色，将C参数类型抽象为形式化类型（例如 struct irq_data * → LogicalIRQ），将MMIO基绑定到设备状态，并从角色语义推导效果和Hoare式合约。结果是每个驱动函数的 FunctionSpec，组合为包含状态、资源、寄存器映射和不变量得 DeviceSpec。

阶段3：代码生成。生成阶段消费形式化规约和后端特定绑定文件，为三个目标生成驱动代码：(1)带有虚假MMIO内存和追踪日志的用户态测试存根；(2)用于嵌入式系统的便携裸机C；(3)带有平台驱动样板的Linux内核骨架。当确定性生成不足时，管线组装LLM输入包并进入修复循环。

阶段4：LLM辅助合成。当确定性后端无法完整重建复杂子系统胶水代码（例如Linux probe/资源生命周期）时，reharness组装结构化输入包（RIS、设备规约、后端绑定、源事实、脚手架），然后进入闭环：编译/静态/追踪验证产生结构化反馈，反馈被送入LLM作为修复提示，LLM修复候选代码，循环重复直到候选代码通过所有检查或耗尽迭代预算。

4. 形式化 RIS 语言

reharness的核心输出是RIS（寄存器交互序列）规约语言。RIS设计为既人类可读又机器可解析，形式化文法覆盖真实驱动中MMIO操作的完整词汇。

4.1 文法

driver <name> v<version> {
  module <function_name> {
    <var> := R(<width>, <addr>) [-- <intent>]
    W(<width>, <addr>) = <expr> [-- <intent>]
    RMW(<width>, <addr>) = <transform> [-- <intent>]
    IF <guard> { <ops> } [ELSE { <ops> }]
    LOOP <count> { <ops> }
    DELAY(<cycles>)
  }
}

每个 module 对应一个驱动函数（框架回调或辅助函数）。模块内操作按源码顺序排列，保留程序的执行序列。

4.2 操作

读（R）：带绑定变量的寄存器读取，供后续使用。宽度为 B1、B2、B4、B8 之一（从MMIO调用的后缀推导：readl → B4，readw → B2 等）。地址解析为三种形式之一：

• 符号化：g->base.GPIO_INT_EN——已知基表达式加已解析的寄存器宏。
• 固定：0x20——无可解析宏的字面偏移。
• 计算：[base + idx]——无法静态解析的动态地址表达式。

写（W）：带表达式值的寄存器写，值可以是常量、变量或Expr代数中的复合表达式。

读-修改-写（RMW）：当 writel 的值是修改同一地址的 readl 返回值的结果时检测到。这是中断mask/unmask操作中的关键模式，其中单个位必须在不干扰其他位的情况下翻转。

条件（IF）：从 if/else 语句提取的分支条件，附到每个分支内的操作。保护条件使用谓词堆栈，是路径不敏感的（记录最内层包围条件）。

循环（LOOP）：来自 for/while 循环的迭代构造，当静态可推导时附有计数表达式。

延迟（DELAY）：时序操作（mdelay、udelay、msleep）转换为纳秒等值计数。

4.3 表达式代数

RIS中的值和保护以代数表达式语言表示：

BinOp 支持14种操作符：算术（Add、Sub、Mul、Div、Mod）、位操作（BitAnd、BitOr、BitXor、Shl、Shr）以及关系/逻辑操作（Eq、Ne、Lt、Gt、Le、Ge、And、Or）。Top 哨兵代表无法静态解析的值。

表达式示例：

• 0x1 << irqd_to_hwirq(d) → BinOp{Shl, Const(1), Var("irqd_to_hwirq(d)")}
• 0x0 ^ 0xffffffff → BinOp{BitXor, Const(0), Const(0xffffffff)}

4.4 示例

清单1展示了为 gpio-ftgpio010 驱动（Faraday FTGPIO010 GPIO控制器）提取的RIS。每个模块对应一个通过Linux irq_chip 和 gpio_chip 框架表注册的回调。

driver gpio-ftgpio010 v0.1.0 {
  module ftgpio_gpio_ack_irq {
    W(B4, g->base.GPIO_INT_CLR) = (0x1 << irqd_to_hwirq(d))  -- Interrupt
  }
  module ftgpio_gpio_mask_irq {
    val := R(B4, g->base.GPIO_INT_EN)   -- Interrupt
    RMW(B4, g->base.GPIO_INT_EN) = val   -- Interrupt
  }
  module ftgpio_gpio_unmask_irq {
    val := R(B4, g->base.GPIO_INT_EN)   -- Interrupt
    RMW(B4, g->base.GPIO_INT_EN) = val   -- Interrupt
  }
  module ftgpio_gpio_set_irq_type {
    reg_type  := R(B4, g->base.GPIO_INT_TYPE)       -- Interrupt
    reg_level := R(B4, g->base.GPIO_INT_LEVEL)      -- Interrupt
    reg_both  := R(B4, g->base.GPIO_INT_BOTH_EDGE)  -- Interrupt
    RMW(B4, g->base.GPIO_INT_TYPE) = reg_type
    RMW(B4, g->base.GPIO_INT_LEVEL) = reg_level
    RMW(B4, g->base.GPIO_INT_BOTH_EDGE) = reg_both
  }
  module ftgpio_gpio_irq_handler {
    stat := R(B4, g->base.GPIO_INT_STAT_RAW) -- Interrupt
  }
  module ftgpio_gpio_set_config {
    val := R(B4, g->base.GPIO_DEBOUNCE_PRESCALE) -- Config
    IF (val == deb_div) {
      val := R(B4, g->base.GPIO_DEBOUNCE_EN) -- Config
      RMW(B4, g->base.GPIO_DEBOUNCE_EN) = val -- Config
    }
    val := R(B4, g->base.GPIO_DEBOUNCE_EN) -- Config
    W(B4, g->base.GPIO_DEBOUNCE_PRESCALE) = deb_div -- Config
    RMW(B4, g->base.GPIO_DEBOUNCE_EN) = val -- Config
  }
  module ftgpio_gpio_probe {
    W(B4, g->base.GPIO_INT_EN)  = 0x0               -- Init
    W(B4, g->base.GPIO_INT_MASK) = 0x0              -- Init
    W(B4, g->base.GPIO_INT_CLR) = (0x0 ^ 0xffffffff) -- Interrupt
    W(B4, g->base.GPIO_DEBOUNCE_EN) = 0x0           -- Init
  }
}

该驱动中全部22个寄存器操作均解析为符号化地址（100%符号化率）。mask/unmask回调正确呈现RMW模式（读取当前中断使能掩码，修改它，写回）。set_config 模块在debounce使能RMW周围保留了条件保护 (val == deb_div)。

5. 基于 AST 分析的 RIS 提取

5.1 翻译单元解析

reharness使用libclang将每个C源文件解析为未保存翻译单元（unsaved TU），从而能够保留宏展开记录。解析器以容错模式运行，跳过那些会终止普通编译器的语法错误（这对于依赖分析环境中不可用内核头文件的驱动至关重要）。解析产生完整的AST游标树加上从预处理记录构建的 MacroTable。

MacroTable 将翻译单元中的每个 #define 映射到其展开值。对于整数值的寄存器宏（例如 #define GPIO_INT_EN 0x20），我们记录其数值偏移。此表是支持符号化地址解析的关键数据结构：当数据流分析器在地址表达式中遇到 GPIO_INT_EN 引用时，可将其解析为0x20并与基指针配对以产生 Symbolic 地址。

5.2 函数识别与回调检测

通过遍历AST查找源位置在目标文件中的函数定义来识别目标函数。每个函数建模为包含名称、参数列表、返回类型和游标的 Func 对象。

回调入口通过源码文本中的指定初始化器模式检测：.field_name = &function_name。我们在经过注释和字符串剥离的源码上使用指定初始化器正则表达式解析这些模式，将每个字段匹配到已知角色表（FIELD_ROLE）。例如 .irq_ack = ftgpio_gpio_ack_irq 被识别为将函数绑定到 irq_chip 回调表中的 interrupt_ack 角色。未出现在任何指定初始化器中的函数被分类为辅助函数，可能会被内联到其调用者中。

5.3 流敏感数据流与污点追踪

提取的核心是逐函数的流敏感数据流分析。对于每个函数，我们按源码顺序遍历其调用点，维护一个将变量名映射到抽象值（AbsVal）的抽象存储，抽象值取自有限域：

污点源：ioremap 及其变体（devm_ioremap、devm_platform_ioremap_resource 等）被识别为MMIO基指针源。赋有 ioremap 调用返回值的LHS变量被绑定为 BasePtr。

地址解析：当遇到MMIO读/写调用时，其地址参数在抽象存储和宏表上被符号化评估。评估通过组合指针变量的 BasePtr 和宏表的 Offset 值解析 base + REG 表达式，产生同时携带设备上下文和寄存器名称的 Symbolic 地址。

读污点：readl 调用的返回值被绑定为 ReadTaint(addr)，记录读取了哪个地址。当后续 writel 使用评估为同一地址的 ReadTaint 的值时，reharness检测到读-修改-写模式，发出 RMW 操作而非分离的读写。

表达式评估：一个递归下降评估器处理抽象值上的算术（+、-、<<、>>）、位操作（|、&、^）和一元（~）操作。当两个操作数均为 Const 时应用常量折叠；否则表达式被捕获为 SymExpr 或 BinOp 用于形式化RIS输出。

5.4 包装函数内联

当调用点引用的是同一翻译单元中非框架原语（不在 FRAMEWORK_FNS 中）的函数时，reharness检查该函数是否已被提取。如果已提取，其操作被内联到调用点，调用点的分支条件应用于每个内联操作。内联深度有界（默认3），防止通过互递归辅助函数无限展开。

这是过程间分析的一种轻量形式：我们不执行完整的上下文敏感摘要计算，但有界深度内联足以暴露隐藏于常见包装模式（如 gpio_setbit、reg_read 和 reg_write）中的MMIO操作。

5.5 Intent 标注

每个操作附有从已解析寄存器宏名推导的意图字符串。我们使用关键词匹配对寄存器名进行分类：含"INT"或"IRQ"的寄存器赋予 Interrupt 意图；"CLK"或"PLL"产生 Clock；"CONFIG"或"CTRL"产生 Config；"STAT"产生 Status；以此类推。这一轻量启发式无需深度语义分析即可提供人类可读上下文。

6. 语义推断

原始RIS捕获了访问哪些寄存器以及如何访问，但未解释为何——每个函数在驱动中扮演什么角色、对设备状态产生什么影响、必须满足什么合约。reharness通过三层推断以后端无关语义丰富RIS模块。

6.1 函数规约（FunctionSpec）

FunctionSpec 是一个元组：

角色推断是关键步骤。reharness优先使用回调表绑定而非函数名启发式。当识别到回调表字段（例如 irq_chip 结构中的 .irq_ack），对应的角色（interrupt_ack）和执行上下文（irq）被确定性地赋予。我们的 FIELD_ROLE 表覆盖35+个标准Linux回调字段，横跨 irq_chip、platform_driver、virtio_config_ops、gpio_chip 和 dev_pm_ops。对于未出现在任何回调表中的函数，降级启发式将函数名字符串子串匹配到角色（例如 *_ack_irq → interrupt_ack）。

签名抽象化将C参数类型映射为抽象形式类型：struct irq_data * → LogicalIRQ，struct platform_device * → DeviceState，整数类型 → UInt，void → Void。这一抽象对后端独立性至关重要：同一 DeviceSpec 可面向Linux、裸机和测试存根后端，而无需引用Linux特有类型。

状态绑定识别函数使用的MMIO基表达式（例如 g->base）并将其绑定到形式化 dev.base 路径。绑定通过扫描函数RIS操作的地址表达式中的成员访问模式来发现。

效果从两个来源推导：(1)对函数写入的每个符号化寄存器发出 writes_register(REG) 效果；(2)从函数角色推导语义事件效果（例如 interrupt_ack → clears_interrupt(line)）。

Requires/Ensures是从角色语义推导的Hoare式前后条件。例如 interrupt_ack 函数不需要前置条件，确保 interrupt_pending[line] == false；probe 函数要求 resources_available 并确保 device_state == READY。

6.2 设备规约（DeviceSpec）

DeviceSpec 将多个 FunctionSpec 实例组合为设备级模型：

设备类别从驱动名推断（例如 gpio-ftgpio010 → gpio_controller，virtio_mmio → virtio_mmio）。

状态从函数的需求推断：每个设备获得一个 MmioBase 状态字段；如果任何函数具有时钟相关角色或源码提及 clk，则添加 Clock 字段；如果任何函数具有中断相关角色，则添加 num_irqs: UInt 字段。

资源从状态字段推导：绑定到 base 的 MmioResource，加上按需的 ClockResource 和 IrqResource。

寄存器从RIS的 register_map 收集，其中包含驱动实际访问的每个符号化寄存器（不是硬件定义的每个寄存器，仅是驱动接触的那些）。

不变量生成为最小安全属性：对于支持中断的设备，断言不变量 forall line: UInt. line < num_irqs → valid_interrupt_line(line)。

6.3 后端绑定（.bind）

BindSpec 将 DeviceSpec 中的抽象概念映射到具体后端API：

• 类型映射：DeviceState → "struct ftgpio_gpio"，MmioBase → "void __iomem *"（Linux）或 uintptr_t（裸机）。
• 回调映射：irq_chip.irq_ack = ftgpio_gpio_ack_irq。
• 原语映射：MmioRead(B4) → "readl"（Linux）或 mmio_read32（裸机）。
• 状态映射：dev.base → "g->base"。
• 导出映射：interrupt_ack as "ftgpio_ack_irq"（裸机）。

默认绑定为每个后端生成，但可自定义以支持非标准API或命名约定。

6.4 源事实（.facts）

对于LLM辅助合成，reharness提取源事实——有助于重建但不应用于后端无关形式化规约的信息：

• Include列表：<linux/gpio/driver.h>、<linux/platform_device.h>。
• 结构体定义：ftgpio_gpio 含字段 base: void __iomem *、clk: struct clk *。
• 常量：具有整数值的非寄存器宏（标志、状态码、位掩码）。
• 回调表：irq_chip.irq_ack = ftgpio_gpio_ack_irq 等。
• 资源：获取调用（devm_platform_ioremap_resource）及绑定目标。
• 错误路径：源码中找到的返回码（-ENOMEM、-ENODEV、PTR_ERR）。
• 辅助调用：显著的子系统函数（devm_gpiochip_add_data、bgpio_init）。

7. 代码生成

reharness包含一个多后端代码生成器，消费 (RIS, DeviceSpec, BindSpec) 来生成可编译驱动代码。提供三个确定性后端；第四个后端对复杂目标使用LLM辅助合成。

7.1 用户态 Harness 后端

Harness后端生成一个自包含C程序，通过固定大小的内存缓冲区（uint32_t mmio_mem[4096]）模拟MMIO。读写通过包装函数（harness_read32、harness_write32）路由，每次访问记录一行追踪：

[trace 0] W 0x20 = 0x00000000  ; GPIO_INT_EN
[trace 1] W 0x30 = 0xffffffff  ; GPIO_INT_CLR

harness包含设备状态结构体、从寄存器映射推导的寄存器常量、RIS支持的函数体（使用后端绑定的原语和状态映射）和单元测试脚手架。整个harness使用标准C编译器（cc -Wall）编译，产生可执行和追踪的二进制文件。

7.2 裸机后端

裸机后端生成面向自由运行环境的便携C代码。不使用Linux内核类型，而是使用标准整数类型（uintptr_t、uint32_t）和便携MMIO原语（mmio_read32、mmio_write32）。生成的代码包含设备状态结构体、初始化/复位/IRQ辅助函数，不含框架胶水代码。使用 cc -ffreestanding -c 编译。

7.3 Linux 后端

Linux后端生成内核驱动骨架：struct device_state、probe/remove 函数、of_device_id 表、框架操作表和RIS支持的回调体，使用恰当的Linux MMIO原语（readl、writel）。此后端仅在设备规约具有足够框架数据时才激活；不支持的语义产生明确诊断而非错误的代码。

7.4 LLM 辅助合成循环

当确定性生成不足时——例如Linux后端无法完整重建probe/资源生命周期或子系统特有注册胶水代码——reharness进入闭环LLM辅助合成模式（图1虚线路径）。

合成模块组装结构化输入包：device.ris、device.dspec、device.{backend}.bind、device.facts、device.scaffold.c 以及两份指导文档（constraints.md 和 verification.md）。脚手架是确定性生成器的输出。

修复循环操作如下：

1. 编译：以严格警告为目标后端编译候选代码。
2. 静态检查：每个RIS引用解析到模块；每个符号化寄存器在寄存器映射中；每个回调入口有表绑定；无遗留TODO。
3. 追踪检查（仅harness）：执行生成的harness并将其MMIO追踪与从RIS规约推导的预期追踪比较。
4. 修复：如果任何检查失败，结构化反馈被格式化并与当前候选代码一同送至LLM。LLM被指示生成满足所有约束的修复后C候选代码。
5. 重复：步骤1–4迭代直至候选代码被接受或耗尽迭代预算（默认3）。

LLM是可插拔客户端：默认情况下，一个空操作存根报告脚手架和验证反馈而不调用API。当设置 REHARNESS_LLM_CMD 环境变量时，完整提示被管道传输到外部命令，修复后的候选代码从标准输出读取。

8. 评估

我们在来自CRUST-Bench测试套件[11]和Linux内核源码树的17个Linux设备驱动上评估reharness。评估回答四个研究问题：

• RQ1（精确性）：多大比例的寄存器访问被解析为符号化地址？
• RQ2（完整性）：检测到多少RMW模式和分支条件？
• RQ3（质量）：每个驱动的生成就绪度得分是多少？
• RQ4（对比）：reharness与基于正则表达式的基线相比如何？

8.1 实验设置

所有实验在配备AMD 9950X处理器和64 GB RAM的Linux机器上运行，使用libclang 18和Python 3。reharness除 clang.cindex 外无外部Python包依赖。

8.2 提取覆盖率（RQ1、RQ2）

表1总结了全部17个测试驱动的提取统计。

核心发现：横跨全部17个驱动，reharness达到100%符号化地址解析——每次寄存器访问均被映射到具有已解析偏移的命名寄存器。这与基于正则表达式的基线形成鲜明对比，后者将所有宏定义寄存器访问报告为偏移0，在相同驱动上达到0%符号化率。

77个检测到的RMW模式集中于中断mask/unmask回调（mask_irq、unmask_irq）和配置函数（set_config、set_irq_type），正是区分纯写与读-修改-写对安全语言翻译至关重要的操作。

62个记录的分支条件主要出现在修改寄存器前检查设备状态的配置函数中（例如 gpio-ftgpio010 的 set_config 中的debounce预分频器比较）。

8.3 生成就绪度（RQ3）

表2展示了四个最复杂驱动的生成就绪度得分。

所有四个驱动均超过 llm_synthesis_ready 所需的0.7 RIS质量阈值和0.5 FuncSpec质量阈值。全部达到 bare_metal_ready。由于推断阶段缺少回调表绑定（在第10节讨论的已知局限），Linux后端就绪度尚未满足任何驱动。

8.4 与正则基线的对比（RQ4）

我们将reharness与 driver-harness 对比，后者是reharness的前身和基线。对比聚焦于第2节识别的四种失败模式。

正则基线解析0%的宏定义寄存器偏移，因其无法评估预处理器常量。它遗漏所有包装函数内部的MMIO操作，为所有分支条件报告 None，无法计算 base + offset 算术表达式。reharness通过AST级分析解决全部四种模式，在整个评估集上实现100%符号化解析。

8.5 案例研究：gpio-ftgpio010

我们详细考察FTGPIO010 GPIO控制器驱动。该驱动在两个Linux框架表（irq_chip 和 gpio_chip）中注册7个回调函数。驱动通过 #define 定义了13个寄存器宏，其中9个被驱动代码实际访问。

reharness正确提取了跨7个模块的全部22个寄存器操作，将所有9个被访问的寄存器解析为其宏名和数值偏移，检测到8个RMW模式（在 mask_irq、unmask_irq、set_irq_type、set_config 中），记录了1个分支条件（在 set_config 中），并推断出7个函数中6个的角色（剩余函数 set_config 没有直接的回调表绑定，降级为 helper 角色）。

生成的用户态harness以 cc -Wall 编译无错误，其执行追踪与probe模块的预期RIS操作序列匹配（对GPIO_INT_EN、GPIO_INT_MASK、GPIO_INT_CLR和GPIO_DEBOUNCE_EN的4次写入）。生成的裸机C以 cc -ffreestanding -c 编译通过。

9. 相关工作

9.1 驱动分析与提取

C-to-Rust翻译。C2Rust项目[8]执行从C到不安全Rust的语法翻译，将安全所有权和借用标注的插入留给后续工具。&inator[17]通过将Rust类型选择建模为类型片段、指针变换图和NLL借用约束上的SMT约束满足问题来解决接口翻译问题。reharness是互补的：它提取可指导C2Rust风格翻译器中语义保持约束的形式化寄存器级行为。

静态驱动分析。SDV[3]、Dingo[4]和Termite[12]等工具对驱动源码执行静态分析以验证协议合规性并生成样板代码。这些工具在框架API级别操作（例如验证 probe 分配资源而 remove 释放它们）。reharness在更低级别操作：它提取实际的寄存器交互序列，捕获的是硬件协议而非OS框架协议。

符号执行。KLEE[7]和S2E[15]对驱动代码执行符号执行以生成测试输入。reharness的提取是静态而非动态的，使其适用于无法在测试环境中执行的驱动（例如由于缺少硬件或内核基础设施）。

9.2 形式化规约与代码生成

设备驱动合成。Termite-2[13]从设备和OS接口的形式化规约合成驱动。规约必须以领域特定语言手动编写。reharness自动化了规约提取步骤，从已有C源码自动生成 DeviceSpec 和 BindSpec。

基于LLM的代码生成。近期研究探索使用大语言模型进行驱动合成[9]。这些方法通常在自然语言描述或源码片段上操作。reharness的LLM辅助合成模块的独特之处在于提供结构化形式化规约和验证反馈作为输入约束，实现修复循环而非一次性生成。

9.3 驱动的中间表示

设备树与ACPI。设备树和ACPI等硬件描述标准描述硬件拓扑（寄存器基地址、中断线、时钟），但不描述寄存器交互协议。reharness的RIS和 DeviceSpec 通过捕获行为协议补充这些标准。

Haiku和Barrelfish驱动模型。Haiku[16]和Barrelfish[14]操作系统使用将设备逻辑与OS框架代码分离的驱动模型，类似于reharness将 DeviceSpec（设备做什么）与 BindSpec（它如何连接到OS）分离的设计。reharness提供了从现有Linux驱动中提取这些规约的工具。

10. 讨论与局限

10.1 当前局限

Linux子系统覆盖。reharness当前识别 irq_chip、platform_driver、virtio_config_ops、gpio_chip 和 dev_pm_ops 的回调表。使用其他子系统（例如 i2c_driver、spi_driver、pci_driver）的驱动需要额外的回调字段模式。

数据流精度。流敏感数据流分析在函数内是路径不敏感的：它不追踪不同分支上的不同状态，也不执行超出简单成员访问链的别名分析。不支持通过函数指针数组的间接调用和位域访问等复杂模式。

Linux后端完整度。确定性Linux后端是三个后端中最不成熟的一个。它为简单平台GPIO驱动生成正确骨架，但尚无法在没有LLM辅助的情况下重建完整资源生命周期（时钟使能/禁用顺序、PM运行时集成、devres回退）。

动态地址。虽然reharness可以在RIS中表示计算地址（如索引寄存器组），但它并不能总是将其解析为具体符号化名称。这是当索引值在运行时确定时静态分析的根本局限。

时间复杂度。libclang解析步骤是主要成本：使用完整内核头文件解析一个典型Linux驱动需要10–30秒。这对于单个驱动的批量分析是可接受的，但对于全内核分析则是禁止的。

10.2 未来工作

额外后端。后端绑定架构设计为可扩展的。我们计划为RTOS目标（FreeRTOS、Zephyr）和验证目标（CBMC、SeaHorn）添加后端，这些后端消费相同的 DeviceSpec 和不同的 BindSpec 文件。

有状态RIS建模。当前RIS捕获操作序列，但不捕获设备状态转换。建模寄存器状态机（例如寄存器值上的有限状态自动机）的有状态扩展将支持更强的验证，如检查驱动从不在初始化前读取寄存器。

全内核分析。扩展到数千个内核驱动需要增量解析、宏表和调用图缓存以及并行执行。reharness的模块化特性（逐驱动、逐函数提取）使这变得可行。

集成安全语言翻译。一个自然的下一步是将reharness集成到C2Rust风格翻译器中：提取的RIS和 DeviceSpec 可为类型选择和所有权标注决策提供信息，特别是对于MMIO指针和中断处理程序上下文。

11. 结论

本文提出了 reharness，一个使用libclang AST分析结合流敏感数据流和污点追踪、从C设备驱动中提取形式化寄存器交互规约的管线。reharness克服了基于正则表达式提取的四个根本局限：宏定义寄存器偏移通过预处理记录解析，包装函数通过过程间调用图分析内联，分支条件通过谓词堆栈记录，算术地址表达式通过符号化抽象解释评估。

在原始提取之上，reharness推断后端无关的函数和设备语义，将其组合为多后端代码生成框架，并为复杂目标提供闭环LLM辅助合成模块。在17个驱动上的评估展示了100%符号化寄存器地址解析、77个检测到的RMW模式和62个记录的分支条件，平均RIS质量得分0.92。

reharness实现了驱动分析工具链中缺失的寄存器级形式化推理能力。通过以形式化语言而非临时格式输出规约，为验证、测试、安全语言翻译和AI辅助驱动合成提供了基础。

致谢

感谢匿名审稿人的建设性反馈。

参考文献

1. A. Chou, J. Yang, B. Chelf, S. Hallem, and D. Engler. "An empirical study of operating systems errors." Proc. SOSP, 2001.
2. M. M. Swift, B. N. Bershad, and H. M. Levy. "Improving the reliability of commodity operating systems." Proc. SOSP, 2003.
3. T. Ball et al. "Thorough static analysis of device drivers." Proc. EuroSys, 2006.
4. L. Ryzhyk, P. Chubb, I. Kuz, and G. Heiser. "Dingo: Taming device drivers." Proc. EuroSys, 2009.
5. A. Kadav, M. J. Renzelmann, and M. M. Swift. "Tolerating hardware device failures in software." Proc. SOSP, 2009.
6. T. Witkowski et al. "Model checking concurrent Linux device drivers." Proc. ASE, 2007.
7. C. Cadar, D. Dunbar, and D. Engler. "KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs." Proc. OSDI, 2008.
8. M. Emrath et al. "C2Rust: Translating C to Rust." https://c2rust.com/, 2021.
9. J. Roelofs, A. Kadav, and A. Cidon. "Large language models as driver synthesizers." Proc. HotOS, 2023.
10. driver-harness: Regex-based driver register extraction. https://github.com/..., 2025.
11. CRUST-Bench: A benchmark suite for C-to-Rust translation. 2024.
12. L. Ryzhyk et al. "Automatic device driver synthesis with Termite." Proc. SOSP, 2009.
13. L. Ryzhyk et al. "User-guided device driver synthesis." Proc. OSDI, 2014.
14. A. Baumann et al. "The multikernel: A new OS architecture for scalable multicore systems." Proc. SOSP, 2009.
15. V. Chipounov, V. Kuznetsov, and G. Candea. "S2E: A platform for in-vivo multi-path analysis of software systems." Proc. ASPLOS, 2011.
16. Haiku operating system. https://www.haiku-os.org/.
17. &inator: Correct, Precise C-to-Rust Interface Translation. Proc. PLDI, 2026.