Reharness: Hardware Behavior Kernel Extraction Architecture Linux 驱动源码 .c / .h 文件 GPIO / VirtIO / MMC / USB ... 阶段1: RIS 提取 Hardware Behavior Stripping libclang AST tu.py + macros.py 污点分析引擎 taint.py (6种抽象值) 调用图内联 call_graph.py 数据流 + RMW dataflow.py (流敏感) 意图标注 intent.py SVF 别名分析 alias.py (可选增强) RIS: 寄存器交互序列 register_map + 操作序列 + 意图 阶段2: 语义推理 spec_infer.py — RIS → Spec 角色 & 上下文推断 callback 表绑定 + 函数名启发 FunctionSpec + DeviceSpec Effect / Binding / Hoare 前后条件 阶段3: 代码生成 generator/ — RIS + Spec → C harness.py baremetal.py linux.py Pi SDK (.ts) 验证: 动静对齐 Dynamic Trace Alignment QEMU / 真实硬件 运行原始驱动 mmiotrace 录制寄存器轨迹 覆盖引导测试集（初始化/中断/电源/数据传输） trace_match.py instrument_mmio.py 偏序对齐验证 (compare.py) 静态 RIS 输出: 目标平台驱动 裸机 / RTOS Linux 骨架 用户态 Harness Pi SDK 合成 (.ts) 闭环合成 (synthesis.py) — Python 前端 + TypeScript 合成后端 (Pi SDK) Pi Agent SDK (TypeScript) synth.mjs + pi_synth.sh createAgentSession → glm-5.2 编译 + 静态检查 sanitize.py (DMA 去风暴) QEMU Trace 比对 instrument_mmio + trace_match 质量评分 metrics.py (readiness scorer) 反馈修复 repair prompt → LLM 重试 循环直到 accepted 或 blocked 四层形式化规约 .ris — 寄存器交互序列 register_map + 操作序列 + 意图标注 硬件做什么（最小完备集） formalize.py 输出 .dspec — 函数语义规约 FunctionSpec: 角色/签名/前后条件 DeviceSpec: 状态/资源/寄存器 spec.py + spec_infer.py .bind — 目标平台绑定 裸机 / Linux / Zephyr / RTOS 平台 API 映射 + include 依赖 spec.py (default_bind) .facts — 驱动元数据 #define / 结构体 / 配置常量 / 设备树 从 OS 风格提升为硬件通用风格 ast_model.py 提取 数据流 语义 验证 可选