reharness 源码教程 · 总览

C 驱动分析libclang AST数据流 / 污点确定性生成Linux / 裸机 / 用户态

reharness 是 DRI 翻译论文（~/Code/dri-trans-paper/reharness）的核心系统：从 Linux C 设备驱动中提取形式化的寄存器交互序列（RIS），推断后端无关的设备语义，并确定性生成 userspace harness、bare-metal C 和 Linux 内核模块三种目标。

一句话定位：把「驱动做了什么」变成机器可验证的形式化契约（.ris），再按契约生成不同运行环境下的等价 C 代码 —— 全程不依赖 LLM 的「手感」，LLM 只是可选的外挂合成器。

核心设计思想

完整流水线

C 驱动源码→ libclang AST→ 宏表 + 目标函数→ 调用图有界内联→ 数据流 / 污点提取→ FormalRIS (.ris)
.ris→ 语义推断 .dspec→ 后端绑定 .bind→ harness / baremetal / linux C→ 编译 + trace + QEMU 验证
① 解析（src/extractor/tu.py · compile_context.py）

libclang 解析 TU，自动读取 Kbuild .o.cmd 或 compile_commands.json 还原编译参数（include 路径、宏定义），保证 AST 与真实内核构建一致。

② 宏表（macros.py）

收集驱动源码里的寄存器偏移宏（如 #define GPIOIE 0x410），常量求值（_eval_int_expr），供地址解析使用。

③ 目标函数（ast_model.py）

找出本文件定义的函数、回调入口（probe/irq_handler/ops 表成员…）、MMIO 全局变量。

④ 调用图 + 内联（call_graph.py）

按源码顺序遍历调用，把包装函数（如 pl061_write 调 writeb）过程间内联，深度上限 max_inline_depth=3；间接调用目标（callback 表）静态解析。

⑤ 数据流 / 污点（dataflow.py · taint.py）

维护抽象存储 var → AbsVal，把 MMIO 调用的地址参数解析成 RegAddr（Fixed/Symbolic/Computed），检测 read-modify-write 模式，记录分支条件栈。

⑥ 形式化（formalize.py）

把扁平 Op 流嵌套成 Cond 块、把值字符串解析进 Expr 代数、打上 op_id / evidence / precision / reliability，输出 .ris 与 FormalRIS JSON。

⑦ 语义推断（spec_infer.py · subsystem.py）

推断寄存器表、状态、资源、callback 绑定、effect/ensure 契约，输出后端无关的 .dspec。

⑧ 生成（generator/）

按 .bind 的类型/函数映射，把 FormalRIS lowering 成 harness / baremetal / linux C；每个访问带 lowering receipt。

⑨ 验证（qa/ · experiment_runner.py）

编译、generation contract 校验、原生 trace、QEMU 运行时比对、strict readiness 评分。

仓库布局

目录内容规模
src/extractor/分析管线：AST 模型、宏、调用图、数据流、污点、MMIO 分类、事务、控制流、SVF 别名、形式化、语义推断~15,600 行
src/generator/三后端生成器 + 共享 lowering~4,900 行
src/experiment_*.py / synthesis.py / trace_protocol.py实验编排（manifest → runner）、LLM 合成桥、trace 协议~2,000 行
qa/测试套件 + 独立 oracle（AST、registration、clock、mutation、trace）+ 矩阵运行器205 项测试
benchmarks/19 个 baseline 单源驱动 + 多源 manifest + zero-shot holdout19 + 3 多源 + 12 holdout
docs/架构文档、里程碑（C10–C27）、复盘40+ 篇
tools/pi/Pi coding-agent 合成器及本地 Node 依赖—
platform/固定内核 submodule 构建 + 测试 rootfs—
research/论文、版本化实验结果、known-good artifacts—

当前权威数字（research/experiments/results/matrix.json）

指标值
驱动数 / 总 ops19 驱动 / 485 个 RIS MMIO 操作
地址分类Symbolic 366 · Fixed 64 · Computed 41
RMW / 条件 / 循环 / 寄存器73 / 123 / 25 / 157
三后端编译harness 19/19 · bare-metal 19/19 · Linux 18/19
QEMU 运行时edu 值级 oracle ✅ · gpio-ftgpio010 结构化 Formal RIS ✅

快速开始

git submodule update --init
./tools/build/prepare_kernel.sh build

./run.sh test                                          # 全量测试
./run.sh extract benchmarks/drivers/baseline/edu.c artifacts/output/edu.ris
./run.sh spec     benchmarks/drivers/baseline/edu.c artifacts/output/edu.dspec
./run.sh gen      benchmarks/drivers/baseline/edu.c linux artifacts/output/edu_drv.c
./run.sh driver   benchmarks/drivers/baseline/edu.c artifacts/output/edu
./run.sh experiment benchmarks/experiments/edu.json    # manifest 驱动的闭环实验

教程导航

章节内容
① RIS 形式语言.ris 语法、表达式代数、地址分类、操作类型、reliability 体系 —— 用 edu / pl061 真实产物逐行讲解
② 提取器实现AST 模型 → 宏表 → 调用图内联 → 数据流/污点 → MMIO 分类 → 形式化，逐模块讲代码
③ 语义推断DeviceSpec / FactsSpec / callback 绑定 / 子系统摘要 / 多源合并
④ 三后端生成器.bind 绑定、generation contract、lowering receipt、harness / baremetal / linux 发射细节
⑤ 验证与实验体系实验 manifest/runner、trace 协议、oracle 家族、QEMU、strict readiness、复现流程