SymCC-Parallel 当前新增技术全景与实现说明

• 快照日期：2026-07-29
• 覆盖范围：当前工作树相对上游 SymCC 新增或显著扩展的 F00-F274
• 读者对象：第一次接触符号执行的工程人员、系统研究人员、项目汇报与论文写作者
• 权威明细：New_Implementation_Archive.md
• 完整配置：Configuration.txt
• 历史追踪：Development_History_Traceability.md

1. 先给出结论

当前项目已经不再只是“给 SymCC 加一个 MPI master”。它形成了七个彼此连接的 研究层：

1. 编译与语义层：在 LLVM IR 中提取稳定站点、控制依赖、数据依赖、内存状态 和可恢复 continuation，并对难以直接符号化的控制流做有界、证明门控的变换；
2. 运行时观测层：记录路径、求解、数据进展、字符串操作、线程事件和候选来源；
3. 统一表示层：用 PrefixDAG、ECT、Query IR、grammar/SPPF、schedule artifact 和 content-addressed live state 保存可复用的结构；
4. 求解与候选层：组合精确 Z3、QF_BV/String portfolio、Pangolin 式上下文复用、 PSCache 式部分解、Backsolver、乐观/选择性求解和结构化候选生成；
5. 并行探索层：同时支持 seed 级 MPI workers、solver 级 portfolio race、 schedule 级 DPOR 和 continuation state 级 frontier；
6. 反馈闭环层：普通 corpus 由 AFL edge novelty 接纳；data coverage、内容摘要、 结构新颖度和执行成本作为调度、去重与独立证据 campaign 的信号；
7. 科研证据层：把 manifest、seal、独立 replay、随机化配对协议、消融和 claim gate 作为实现的一部分，而不是实验结束后临时补日志。

最重要的系统不变量是：

输入 proposal 不能绕过完整当前约束验证和真实目标程序重放；编译变换不能绕过 proof gate 与未变换基线 replay；进入普通 corpus 的候选最终必须通过全局 AFL edge novelty 仲裁。

这使项目可以激进地引入新技术，同时把不完备方法隔离在正确性可信边界之外。

1.1 阅读路线

• 五分钟了解系统：阅读第 1、3、4、22 节，先建立执行流、bitmap 和可信边界；
• 准备部署或调试：继续阅读第 2、7、20、21 节，重点核对默认开关、产物和测试；
• 理解算法实现：按第 9-18 节的顺序阅读，从 PrefixDAG、Query IR 到 solver、 grammar、schedule、continuation 和 CFG 变换；
• 准备论文或实验：阅读第 19、23-25 节，并回到逐项档案核查 ID、证据和已知边界。

1.2 术语速查

2. 如何理解“已经实现”

2.1 结果等级

项目文档使用两类标记，不能把它们读成一条线性的成熟度阶梯：

I/T/B/R 描述证据成熟度；E 是正交的可执行证据属性，表示有 manifest、 seal、独立 replay 或 claim gate 可重算部分结论。一个功能可以是 I/T/E，但并不 因此达到 B 或 R；E 也不是形式化证明、密码学签名或远程证明。

当前多数功能达到 I/T；后期研究路径大量达到 I/T/E；早期并行、公开 benchmark 和 SymSan 路径包含 B 级历史结果。最新全功能组合尚未整体达到 R，所以本文不会把 “机制已实现”写成“系统已在公开 benchmark 上达到 SOTA”。

2.2 启用方式

功能是否存在与是否默认启用是两件事：

因此“项目实现了 275 个功能 ID”不表示一次 campaign 会同时执行 275 条路径。 超预算、证据不完整、语义不支持或验证失败时，功能应 fail closed 或退回受支持的 精确路径，而不是静默近似程序语义。

Configuration.txt 当前记录 373 个唯一 SYMCC_* 配置名。本文只解释配置族， 具体默认值、上限和产物 schema 以该文件为准。

2.3 学术技术来源与本项目差异

“借鉴某论文”不等于“复现该论文”。下表明确区分原始思想和本项目实际落地：

完整论文链接、论文原始结论和逐项差距见 sota_hybrid_execution_2026.md 与 SOTA_Gap_Audit_2026-07-24.md。

3. 两条执行主线

3.1 Native concolic + AFL++ 闭环

这是当前最成熟的执行主线，单个工作项按以下顺序运行：

1. AFL++ 或 corpus 产生种子；
2. coordinator 扫描队列，结合 PrefixDAG、ECT、目标距离、历史收益和 worker 状态 选择工作项；
3. master 向 worker 下发种子对象、executor/profile、focus set、目标分支、schedule prefix 和 AFL edge-bitmap 版本或增量；
4. instrumented target 真实执行，QSYM/SymCC runtime 构造符号表达式和路径约束；
5. QSYM 的私有 branch-interest bitmap 判断某分支是否值得再次求解；
6. runtime 内的 exact、tailored/Backsolver、sampling 或本地 string backend 可直接 产生候选；QueryStore、grammar、agentic 等异步路径通过各自 artifact/sidecar 产生候选，但最后汇入相同 triage；
7. worker 先用 128-bit BLAKE2b 摘要做有界的实用内容去重，再用 AFL-instrumented target 的 streaming/batched showmap 重放候选；
8. worker 的本地 AFL edge bitmap 做预过滤，只上传本地判新的 sparse edges；
9. master 在自己的会话级 edge bitmap，或多 coordinator coverage-owner shard 上 做最终 novelty claim；只有全局 edge delta 非零的候选才写入普通 SymCC/AFL queue；
10. master 消费 telemetry，更新 PrefixDAG、ECT、data-progress tracker、策略后验、 coverage owner 和下一轮工作优先级。

3.1.1 一个最小端到端例子

假设输入 A0 到达 if (x == 0x42)，当前走 false 分支：

1. runtime 用稳定 site ID 和 taken=false 更新 QSYM branch-interest map，并构造 x != 0x42 的已走路径与 x == 0x42 的翻转目标；
2. direct fast solve 可能直接把依赖字节改成 0x42；复杂情况再进入当前 prefix context、Backsolver 或 Z3；
3. 候选 B0 先在 worker 内按内容摘要去重，然后由 AFL target 重放得到 [(edge_17, count_1), (edge_31, count_1)]；
4. 若 worker 本地 bitmap 已有两条边，候选在 worker 被丢弃；否则 sparse edges 随候选上传；
5. 若 master 全局 bitmap 仍缺 edge_31，master 原子接纳 B0 并广播 coverage delta；若另一 worker 已先声明该边，B0 不进入普通 queue；
6. 无论最终是否接纳，solver 状态、候选数、data progress 和耗时都会进入反馈， 但调度奖励不能代替全局 edge novelty。

3.2 Continuation/CAS 状态级执行

该路径不是“多启动几个相同进程”，而是把可恢复符号状态作为工作：

1. LLVM 子集被降低为 executable continuation IR；
2. checkpoint 保存 program counter、symbolic store、path-condition root、 page-COW memory、对象生命周期和动态选择计数器；
3. 状态内容以 CAS 哈希寻址，coordinator 只租约分发状态描述符；
4. worker 恢复 continuation，在有界步数内执行并在符号分支处 fork；
5. child 的 path condition 追加一个 solver-frame delta；symbolic store 重新内容 寻址，未改 memory page 通过 page-COW root 共享；
6. halted candidate、frontier checkpoint 和失败原因一起提交；
7. master 通过 fencing token 和内容哈希拒绝过期、重复或被篡改提交；
8. 可具体化的输入仍进入与 native 路径相同的目标重放和 AFL 仲裁。

Continuation 路径当前覆盖的是明确有界的 LLVM 语义子集，并不是任意 C/C++ 程序 的完整 GenSym 复刻。遇到异常处理、无法证明的别名、超预算 pointer domain、 不支持的 intrinsic 或复杂循环时会保守拒绝 lowering。

4. 位图、集合与哈希空间

项目中“bitmap”不是一个对象的多个名字。混淆它们会直接导致重复求解判断错误。 下表的 B1-B6 是本文和 Architecture_QA3.md 为讲解定义的标签，不是源码类型名。

B3 与 B1/B2 使用不同 ID 空间：B3 关注符号分支及其上下文，B1/B2 关注 AFL instrumented binary 的覆盖边。SYMCC_AFL_COVERAGE_MAP 在 worker 中实际指向 131072-byte 的 QSYM qsym_bitmap，不能拿 AFL edge ID 去索引它。B5 是兼容 AFL 的有限 namespace，仍可能发生哈希碰撞；scheduler 的 data tracker 则用显式结构键 记录最佳 matched bits。F247 是独立研究流程：在同一 instrumentation identity 下 分别用 edge-only 与 edge+data showmap 重放相同 candidate/witness，封存 sparse map、 重复稳定性和 feature calibration；它不改变普通 MPI queue 的 edge-only 接纳条件。

5. 技术族总表

技术族是多对多视图，同一 ID 可以同时服务调度、solver 和 evidence。第 24 节为避免 重复只给每个 ID 分配一个“主层”；表中范围重叠不表示重复实现。

下面按执行链解释每个技术族。

6. 编译器与运行时正确性基础

6.1 位宽、线程和站点身份

F00 修复并扩展了符号表达式的基础语义：

• inttoptr、ptrtoint 按 LLVM DataLayout 做扩展或截断，而不是假定 64 位；
• runtime 参数表达式槽和返回表达式改为 thread_local，避免多线程目标互相污染；
• test-case handler 可显式保存已经验证的 concrete values；
• QSYM 专属测试按 backend capability gate 运行。

F26 是一次跨层 correctness hardening：

• bit-vector 线性化只有在证明无回绕时才进入整数/polyhedral reasoning；
• poly cache key 绑定完整前缀和表达式上下文；
• fast solve、cache model 和外来 poly sample 都重新验证当前目标；
• LLVM site ID 由稳定模块/位置身份产生，避免 ASLR 和构建顺序污染；
• UCSan shadow copy、multi-master fencing 和 benchmark 字段一致性被重新审计。

这些工作不直接增加覆盖率，却决定所有后续优化是否有可信基础。尤其是“把位向量 当整数”和“跨前缀复用 UNSAT”都可能产生静默漏解，因此项目只允许经过证明的 线性子域，并禁止跨前缀传播 UNSAT。

7. MPI 并行与 AFL++ 混合闭环

7.1 从串行 seed 到分布式工作

F17 建立 master/worker 协议：worker 声明就绪，master 分发内容寻址的种子与策略， worker 返回稀疏覆盖和小型 telemetry。协议包含原子文件、非阻塞消息资源回收、 终止握手、超时区分和大规模多 coordinator 路径。

F18 把 AFL queue 增量送入 SymCC，把经过真实 showmap 判新的候选送回 AFL。关键优化 包括 worker-side triage、streaming/batched showmap、增量目录扫描、内容哈希预去重、 coverage delta 和各阶段交错执行。历史固定配置测量曾记录明显的 I/O 与通信下降， 但这些数字是 B 级机制结果，不是跨目标平均加速。

F19 继续解决扩展性：

• focus bytes/focus set 对输入依赖域分区；
• branch-density-balanced partition 避免等长切分造成难度偏斜；
• work stealing 和 adaptive granularity 消化 worker 空闲；
• persistent mode 与 shared-memory testcase 减少启动/I/O；
• 报告 active worker 和总 CPU，而不是只报 -np。

7.2 异构执行引擎

F20 把 LAF、CTX/NGRAM、CmpLog、MOpt、GRIMOIRE 和 honggfuzz 作为互补候选来源； F23 用 ConcolicEngine 契约统一 SymCC 与 SymSan；F24 把选择性符号化、dictionary、 multi-field hints 和 RGD 的 I2S/JIGSAW/Z3 级联接入 SymSan。所有引擎仍共享 coverage triage、调度和冗余统计，避免评测逻辑因 backend 不同而漂移。

F25 提供可重复安装、离线 bundle、相对 RPATH 和 bare-machine/debootstrap 验证。 它解决“代码能跑”和“别人能重建同一实验环境”之间的工程缺口。

8. 遥测、覆盖与结构反馈

8.1 统一 SolverTelemetry

F01 把每次执行归一为 engine-neutral telemetry：

• 进程状态：signed return code、timeout、killed、elapsed；
• 路径状态：path hash、open branches、bounded branch trace；
• 求解状态：SAT/UNSAT/unknown/timeout、算法、成本、cache hit；
• 依赖状态：comparison taint、input offsets、结构 context；
• 结果状态：generated、validated、accepted 和拒绝原因；
• capability/missing fields：避免把 backend 缺失字段误当作零。

这使 scheduler 能同时比较 SymCC、SymSan、exact、sampling 和 semantic proposal， 又不会依赖某个求解器的进程内对象。

8.2 Data Coverage

F04/F28 将“距离常量还有多远”变成独立反馈：

• 整数 equality 使用相等 bit 数；
• ordered comparison 使用相等高位前缀；
• switch 只探测相邻 case 或范围端点；
• memcmp/bcmp/strcmp/strncmp 记录有界字节区域进展；
• 编译期常量全局对象用稳定 module/object ID 注册；
• 未插桩 DSO 的只读 PT_LOAD 可在启动时注册；
• runtime 地址归一化为 (object_id, byte_offset, width, kind)。

显式结构键 novelty set 负责逐 feature 的精确 dominance；有限的 AFL data namespace 负责与 AFL 生态兼容。只有 matched bits 严格提升时才替换 scheduler 中的 feature winner，而且该 tracker 不会删除 AFL 自有 queue 文件。

8.3 结构覆盖和目标引导

F06 组合 directed coloration、静态依赖、并发提示和结构任务图：

• ColorGo 风格的静态/动态 coloration 从 target 反向计算 CFG/call distance；
• DynamiQ 风格的结构任务把递归 call-graph SCC 压缩成稳定 region，再按收益、成本、 停滞和 queue pressure 分配 ownership/work stealing；
• 静态 branch-to-byte 摘要可在不额外执行目标的情况下生成 replay focus；
• 并发图标记 thread lifecycle、lock/condition/barrier/semaphore、atomic 和 fence。

F07 用 Expressive Coverage Tree 表示 observed/open outcome、上下文、重复形状和结构 稀有度；Empc 风格 multiple minimum path cover 先折叠 loop SCC，再用不同 maximum matching 产生多组路径覆盖，并依据真实 trace 缩小 seed 的活动 cover。目标不可行时 退回 predecessor/dependence，而不是持续选择同一条最短路径。

F22 把总耗时拆为取任务、concolic、扫描、去重、showmap、发送等 phase，并建立 redundancy funnel：同 worker 重复、跨 item 重复、跨 worker 重复、coverage 已见和 最终 accepted。没有这些字段，学习型 scheduler 很容易把 I/O 拥塞误认为求解无效。

9. PrefixDAG、目标任务与自适应调度

F05 用 PrefixDAG 保存跨 seed 的路径前缀，而不是把一次 execution 当作孤立事件：

• S2F 式 actionseed 把同一 seed 的多个高价值 open branch 批量化；
• exact executor 优先处理明确目标，tailored executor 处理 ITE/隐式流；
• sampling 只分给困难但曾产生收益的前缀；
• TACO 风格目标路径关注 under-explored near-target prefixes；
• MultiGo 风格评分联合目标距离、路径频率、难度和探索保留。

F08 把选择扩展到 seed、worker、executor、strategy 和 parameter；F09 学习 SMT algorithm sequence；F10 提供确定性的 semantic fallback、内置 route、异步 provider 接口和 verifier-gated proposal。当前仓库实现的是 inverse/exemplar/token/ object-partition 等有界数据候选，不包含 Gordian 完整 ghost-code 编译迭代，也没有 把 NeuroSCA 训练模型作为 solver backend。所有外部输出都经过 schema 检查、 Query IR 或 concrete evaluator 验证和目标重放。

具体调度器不是单一 bandit：

• SimiFuzz 风格 LinUCB 对 seed-worker pair 建模，并按固定 time slice 聚合反馈；
• K-Scheduler 风格 frontier score 使用 showmap cache 的稀有边权重；
• TACE 两阶段先执行 bounded no-solve dependency profile，再只符号化 sparse focus；
• Strategy/Component portfolio 分开学习 exact/tailored/sampling、solver、focus 和 sampling 组件，避免把组合收益错误归给每个开关；
• AdaptiveParallelismController 用带迟滞的 hill climbing 调整 active symbolic workers，防止并行度频繁抖动；
• SYMCTS 风格 prefix/edge-dependence 状态为 under-explored branch pair 保留 replay 机会，而不是只依赖 AFL 的粗粒度边图。

F14 将上述能力组织成 xFUZZ/KRAKEN 风格 AFL profile，组合 LAF/CompCov、CTX、 Ngram、CmpLog、MOpt 和 power schedule；F15 保存 propensity、并行干扰和离线 trajectory，用 clipped IPS、SNIPS、doubly robust、ESS 和 lower confidence bound 做保守 off-policy 评估。F186 又将 ParaSuit 式参数空间升级为带 active_when 依赖的机器 schema、上下文后验和只读 transfer prior。失活参数不会被错误归因， exact profile 也会显式下发关闭近似路径的 hard guard。

这里的“学习”是资源分配，不是把神经网络放进 correctness oracle。预测错误最多浪费 预算，不能让非法候选进入 corpus。

10. Query IR 与持久化查询服务

10.1 为什么需要 Query IR

直接保存一段 solver 日志很难跨进程、跨 backend 或跨实验复用。F27 建立内容寻址、 版本化的 Query IR：

• 节点、位宽、输入 offset、prefix roots 和 target root 都有规范表示；
• query trie 共享共同前缀；
• QueryStore 以 digest 管理提交、lease、结果、候选和证据；
• async query service 可在 worker 之外消费查询；
• prefix-keyed incremental solver 避免重复翻译同一断言向量。

F29 从 Query IR 中提取可逆 equality、模型和 polyhedral domain，生成多个候选； F181 把 converter recipe 持久化并逐步/累积重放。未知 operation、冲突 assignment、 越界 offset 或关闭 full-validation obligation 都会被拒绝。

Query IR 已成为多个技术之间的“公共语言”：Pangolin reuse、PSCache、string solver、 grammar hole、schedule joint solving、QF_BV portfolio 和研究证据都可以引用同一查询 身份，而不是各自发明不可比较的日志格式。

11. Pangolin 式 polyhedral/Z3 context 复用

11.1 同前缀复用

F03 在 QSYM 内保存：

• SAT/UNSAT/timeout 结果；
• Z3 model 修改的输入字节；
• 依赖字节的可行区间 box；
• 规范化线性约束；
• prefix assertion vector 和可重用 Z3 translation context；
• 小 UNSAT core 及其结构 fingerprint。

同一完整 key 下可重放 SAT model、跳过已知 UNSAT、从 polytope 采样或复用 assertion vector。UNSAT core 只有在当前约束包含被证明的 core 时才能使用。

11.2 跨前缀与跨布局 SAT 候选

F176-F185 将复用扩展为一条逐步加固的链：

1. F176：比较不同前缀的规范线性系统，只召回 SAT 候选；
2. F179：对缺失字节做 [0,255] 区间消元，得到保守投影 envelope；
3. F180：搜索保持系数/约束结构的字段 byte bijection；
4. F182：用有界整数 Z3 公式精确检查双向蕴含和交集；
5. F183：通过系数结构证明跨长度、跨 offset、跨 endian 对齐；
6. F184/F185：widening/narrowing 必须经过 exact existential projection；
7. F176/F179 的 interval/polytope 只负责排序和采样，完整当前表达式仍负责接纳。

采样器可构造完整 A x <= b，使用 John/Dikin/coordinate walk；每个取整后的 byte assignment 都重新检查整数约束。奇异、边界或超维情况退回 hit-and-run/coordinate 或普通 Z3。

不能跨前缀复用 UNSAT。 即使两个线性抽象看起来等价，未抽象的非线性、数组、 字符串或控制依赖也可能不同。跨前缀路径只把外来 SAT model 当 proposal。

12. 多层求解、Backsolver 与 Solver Portfolio

12.1 概念上的决策层，而非固定调用栈

一次目标翻转并不总是直接调用完整 Z3。下面是理解成本层次的概念顺序，实际代码会 根据 executor profile、query shape、cache 命中和异步 ownership 跳过、交换或并发 执行其中若干层：

1. branch-interest、依赖和 prefix policy 判断是否值得求解；
2. exact cache、prefix context、PSCache 或已验证 generator model；
3. direct/optimistic generator 和 Backsolver 的有界候选；
4. selective concolic partition 或 string/grammar 专用 backend；
5. 单 solver exact 求解；
6. bounded parallel portfolio race；
7. timeout/unknown 时保留证据并回退或延后。

QSYM 主路径的关键次序更具体：fast solve 成功会直接返回；否则默认先做带完整 prefix 的 strict solve。strict UNSAT/unknown 后，普通目标可尝试只保留目标的 optimistic solve；含 ITE 的目标进入 Backsolver，后者才可能选择性丢弃与 ITE controller 依赖 重叠的 prefix。只有设置 SYMCC_OPTIMISTIC_FIRST=1 才会先解只含翻转目标的 target-only 公式：结果为 SAT 时保存临时 model 并继续 strict solve；结果为 UNSAT 时，目标本身已经不可满足，可以直接结束；结果为 unknown/timeout 时按当前预算停止。 只有后续 strict solve 未得到 SAT 时，先前的 optimistic model 才作为 Backsolver/保存路径的候选，仍不因此取得 corpus 接纳资格。

求解策略没有静态占比。占比由实际 workload 与 profile 决定，应从 solver_queries、fast_solve_count、backsolver_*、cache/poly/generator hits、 portfolio attempts 和 accepted outputs 等 telemetry 计算；没有 campaign 原始计数时， 不能给出“Z3/乐观/丢前缀各占多少”的百分比。

12.2 Backsolver 与 bounded Veritesting

F02 在 LLVM 中把 canonical select、双前驱 PHI 和有界多臂区域表示为 ITE。 Backsolver 先枚举附近 controller outcome，直接反演并用 lightweight evaluator 验证；若失败，再尝试删除与 ITE controller 依赖重叠的部分前缀并调用 Z3。

丢弃前缀只发生在明确的 tailored/Backsolver fallback，而不是普通 exact solve。 实现只删除与 ITE controller input dependencies 重叠的 prefix constraints，保留其余 约束并把目标翻转加入 Z3 或直接反演候选。副作用是：

• 候选可能满足目标却不满足原始路径；
• 嵌套 ITE 会造成候选组合增长；
• 删除过多会把成本从求解器转移到大量无效 concrete replay；
• 因此前缀被删除后，候选必须对保留约束和目标重新求值，并最终真实执行。它并不 保证满足被删除的原始路径，所以 concrete replay 失败属于预期代价而非 solver bug。

12.3 PSCache 与部分解

F32/F35/F236 用 solver assignment、assumption conflict 和最小化 UNSAT core 构造 部分输入 assignment。命中时必须：

• 重建 signed prefix/off-path literal；
• 证明 assignment 与当前 Query IR 相容；
• 对当前完整 roots 重新求值；
• 把固有 UNSAT、空 core、缺字段和 proof tamper 显式拒绝。

它不是“看到相同几个字节就复制答案”，也不实现论文中所有 bit-blast trail 技术。

12.4 QF_BV portfolio 与 SMTgazer 式调度

F31/F34 建立异步和并行 portfolio，记录每个 backend 的 SAT/UNSAT、模型验证、 disagreement、child CPU、取消和 timeout。F237-F246 继续加入：

• backend-neutral QF_BV lowering 与 capability certificate；
• prefix-keyed persistent SMT-LIB process；
• cvc5/Bitwuzla/Z3 conformance 和模型双验证；
• censored-cost X-means/BIC prior；
• bagging/boosting schedule optimizer；
• expected-improvement SMBO；
• SAT consensus grace 与可取消 process group；
• Query IR feature schema v2；
• sealed paired holdout 与 leakage check。

UNSAT 只有在 backend 具备授权证据时才用于剪枝；SAT 必须有可验证模型。训练集、 holdout、solver binary identity、配置和内部 attempt 都绑定进 evidence，防止 post-hoc 选择最好结果。

F177/F178 的乐观 generator 和 Z3 tactic model converter同样遵守“proposal + full validation”：simplify/solve-eqs 可以消掉变量，但必须通过 model converter 恢复 assignment，并对原始完整公式检查。

13. 字符串与位向量双表示

F30 先从 memcmp/strcmp/strncmp 导出 offset-aware concrete token 和 patch artifact； F33 加入可执行 string solver 和 MPI/CLI materialization。F193-F200 将其扩展为：

• 同一 query context 中同时声明 String 和逐 offset 8-bit BV；
• 字符、first-NUL、长度与输入 byte 精确连接；
• contains/indexof/substr 和 byte predicate 联合求解；
• strlen/strchr/strstr 的有界 operation artifact；
• Z3/cvc5 等 backend 的 validation-first portfolio；
• atoi/strtol/strtoul 在明确子域内的 regex、String integer 和 BV fold 一致编码；
• wrapper 先用 concrete strtol/strtoul 结果、ERANGE、base/endptr、位宽和逐十进制 step bound 判断是否落在精确子域；进入 symbolic 路径后把 digit/range/overflow guard 编码为约束，并由 string query evaluator 再复核候选；
• contextual backend selector 只学习已通过 concrete evaluator 的结果。

这是 SymCC-str 思想的保守可执行子集，不是完整 C 字符串库模型。非空 endptr、 base 0/2-36、Unicode、复杂 alias/lifetime、中间 string object 和域外转换会 fail closed 或回退普通 BV 路径。

14. 在线语法、解析森林与 PCFG

14.1 从 token 到可验证 grammar hole

F36 提供 token grammar proposal；F187 根据 comparison-taint span、分隔符和历史 accepted seed 在线学习稳定 production，并允许有界变长 splice。F190 把 Query IR 中的未约束 input bytes 标记为 grammar hole，候选同时经过 grammar evaluator 和 Query IR evaluator。F191 只在 coverage plateau 后从保留历史中采集结构，F192 用 独立 parser oracle 拒绝错误泛化，并按上下文拆分冲突规则。

14.2 解析结构与候选事务

F201-F212 建立结构化 parser trace、rule coverage、递归/互递归 CFG fragment、 incremental ECT subtree correspondence、Pareto corpus、packed forest、nullable SCC fixed point、多 nonterminal 原子 transaction 和 content-addressed parser cache。

这里的关键不是“模型觉得输入像 JSON”，而是每个候选都能指出：

• 来源 production、nonterminal 和 byte span；
• packed forest 中的 alternative 或 nullable proof；
• 与目标 ECT subtree 的 correspondence；
• 修改前后 parser acceptance；
• 被替换 seed 和结构 feature 的 ownership。

14.3 概率语法与漂移控制

F213-F226 在 accepted forest 上建立 PCFG：

• Dirichlet posterior 与 inside/outside mass；
• parent、grandparent、ordered sibling 和 second-order sibling context；
• relation-aware synchronized slots；
• prequential log-loss calibration；
• recency window、stale/OOD detection 和恢复；
• Hoeffding cut、anytime-valid drift certificate、跨 context FWER；
• 五级 context order 的 sealed confirmatory ablation。

概率只改变候选排序。校准变差、证据过期或上下文样本不足时回退到更低阶/global posterior，不会把低概率规则当作不可能。

14.4 多解析器与独立证据

F227-F235 接入 persistent Tree-sitter、generalized Earley/Lark、Parglare GLR/SPPF， 并构造：

• exact edit 与增量 tree reuse proof；
• complete SPPF/selected-tree paired telemetry；
• parser-neutral span/boundary correspondence；
• cross-parser calibration；
• grammar correspondence certificate；
• 小范围 exhaustive language differential。

这些机制用于发现单一 parser adapter 的盲点。不同 parser 同意可提高证据强度， 不同意则进入四象限统计和 fail-closed 路径，而不是多数投票修改程序语义。

15. UCSan 式 Under-Constrained Execution

F11 允许从指定函数入口开始，而不必手写完整应用 harness：

• 编译器建立函数参数、对象和 pointer shadow 操作；
• structured seed 描述 object graph、大小、内容和引用关系；
• runtime 为 pseudo pointer 提供真实 backing object；
• partial shadow、copy、load/store 和 external policy 有明确配置；
• seed 可 inspect、normalize、learn 和 dump。

它适合库函数、深层模块和难以从程序入口到达的代码，但 under-constrained execution 天然可能产生调用环境中不可达的状态。因此生成结果仍需回到真实 harness 或目标 程序验证；对象图大小、外部函数和 pointer scope 也都有上限。

16. 并发调度与内存模型探索

16.1 从 trace 到 schedule constraint

F13/F39-F44 建立线程、锁、条件变量、内存读写和 provenance trace，构造 happens-before、lockset conflict 和 schedule artifact。F45-F55 逐步加入：

• bounded SC replay-prefix SMT；
• mutex/rwlock lifecycle；
• condition wait/signal/broadcast；
• create/start/exit/join/detach/cancel identity；
• partial-order/linear-extension encoding；
• sparse lifecycle anchor；
• constructive topology certificate；
• lazy critical-section refinement；
• 系统 libz3 model extraction 和 runtime replay materialization。

16.2 Source/Optimal-DPOR 与弱内存

F56 保存 Source-DPOR source/sleep sets；F61 建 wakeup tree；F62 构造 bounded ConDPOR execution graph 和 backward revisit；F63/F64 根据 path-dependent event 重新生成 transition 并检查 enabledness；F57 联合 Query IR、schedule 和 read-from 求解；F58/F65 支持有界 SC、TSO、RA 与 native atomic trace。F221 修复 signed integer SMT-LIB 和跨 solver 可移植证据。

当前实现的准确表述是bounded schedule diversification 和可执行证据框架：

• event、thread、memory 和 query 数有硬上限；
• 只覆盖已建模 pthread/atomic 生命周期；
• memory model 是参数化有界编码；
• 尚不能声称任意 C/C++ 并发程序的完备模型检查或论文级 ConDPOR 等价证明。

17. Content-Addressed Live Continuation

17.1 状态数据面

F12 先提供 content-addressed 分布式状态、lease、fencing、coverage gossip 和 multi-coordinator 控制面；F38 定义 canonical continuation descriptor；F59 保存 solver stack、symbolic store 和 page-COW memory；F66 让 continuation IR 可执行并 接入 MPI frontier。

checkpoint descriptor 的内容身份同时绑定 frames/PC、path-condition root、 symbolic-store root、memory root、program root、parent 和 target branch。不同数据面 使用不同持久结构：path condition 是 parent solver frame + assertion delta； symbolic store 是规范化全量映射 root；memory 是 page-level COW root，未修改页共享 摘要。worker 可以从 CAS 完整恢复这些 root。

同一 worker 对相邻 child 复用 prefix-keyed incremental solver 与已物化 SMT fragment；迁移到其他 worker 时从持久 solver-frame chain 重建。进程内 solver-frame、 fragment 和 process cache 不进入 checkpoint identity，丢失它们只影响性能，不改变 checkpoint 语义。

17.2 LLVM 到 continuation 的有界语义

F68-F175 是一条很长但逻辑一致的工程链，可分为四段：

关键对象包括：

• 对象身份：global、frame-local alloca、heap site/instance、input buffer；
• 生命周期：alloc/free/realloc、frame depth、live/init marker；
• 指针 provenance：有限候选对象、guard、offset domain、caller certificate；
• 内存：page-COW byte memory、pointer sidecar、definedness sidecar；
• 未定义行为：除零、shift、overflow、exact/nuw/nsw、freeze 和 poison；
• 外部语义：只对可证明长度/对象域的 libc/intrinsic 建 summary；
• 恢复身份：program counter、frame、dynamic choice counter 和 path root 均入状态。

后期 byte-lane 技术之所以细分许多 ID，是因为“一个 load 的值是否定义”可能来自 不同路径上的多个部分写入。实现从单 cell PHI 演进到多 cell、循环 carry、递归 condition tree、同源/多源 group 和 forwarded corridor，每次扩展都要求独立的 拓扑与 source-membership 证明。它们不是 30 个互不相关的功能。

18. IFSS、Hydra 与证明携带的 CFG 变换

18.1 为什么在编译期改控制流

复杂分支会产生大量短路径和嵌套 ITE。IFSS/Veritesting 尝试把多个路径合成一个 表达式状态，Hydra 尝试把相似控制流臂合并，从而减少 fork 和重复执行。错误变换会 直接改变程序语义，所以该技术族默认关闭并使用“证明、原程序重放、denylist”三层门。

F37 最初只生成 targeted transformation proposal；F248 将 profile-guided Hydra 接入真实 LLVM pass，并用未变换基线目标/原始 IR 生成的目标作为权威 replay oracle。 只有“变换目标出现失败而基线目标没有”的 site 才形成 spurious-failure 证据并进入 denylist；这符合 Hydra 的 failure-preserving 而非完整 semantics-preserving 边界。

18.2 多臂 IFSS、switch 与 continuation tuple

F249-F259 逐步实现：

• 3-8 臂 region-state worklist；
• MemorySSA/AA 证明的 memory-state merge 和 NoMod def-chain；
• data/memory 共享 partition 与 condition DAG ownership；
• 多 return exit state；
• switch linear、unsigned balanced 和 profile-optimal alphabetic tree；
• shared-destination edge/PHI multiplicity；
• branch-weight import 和可重放 switch manifest。

F260-F270 再将多出口区域表示为 exit-id + live-out tuple：

• scalar 和 MemorySSA-proven memory slot；
• affine natural-loop closed form；
• upper-triangular recurrence；
• post-update break/continue；
• nested acyclic MemoryPhi provenance；
• manifest、SHA-256 seal 和 fresh LLVM process replay。

F271-F274 扩展多 break priority、unequal linear arms、internal-tree Hydra，并把三条 transformation pipeline 统一成 sealed independent replay。seal 绑定 input/lowered IR、compiler、LLVM tool、配置和 ordered proof identities；它能发现本地 artifact 漂移与篡改，但不是数字签名或远程 attestation。

18.3 编译 pass 次序

LLVM new pass manager 把工作拆为 module pipeline start 与 vectorizer start 两段：

Module pipeline start:
IFSSSwitchLowering
  -> IFSSLoopSummary
  -> IFSSExitLowering
  -> IFSSContinuationLowering
  -> IFSSContinuationMemory
  -> HydraTransformation
  -> LiveContinuationExport
  -> SymbolizePass(module)

Function pipeline at vectorizer start:
Scalarizer
  -> LowerAtomic
  -> SymbolizePass(function)

module 版 SymbolizePass 初始化 stable site IDs，插入 UCSan/atomic schedule instrumentation，导出静态依赖/距离图，重命名 wrapper 并建立 runtime constructor； function 版才 lower intrinsic/inline assembly、建立参数表达式、插入 basic-block notification 并逐 instruction 符号化。LLVM 15 及以下的 legacy pipeline 保持相同的 逻辑变换顺序，但把 Scalarizer -> LowerAtomic -> SymbolizeLegacyPass 串在同一注册点。

这个顺序保证 CFG/continuation 变换先完成、atomic/vector 形态先规范化，再由普通 symbolization 看最终 IR。各变换对 proof failure 必须 fail closed；对于先构建再验证的 局部变换，回滚后不能留下孤立 runtime call、不完整 PHI 或残余 metadata。

19. 科研证据、实验协议与可复现性

F16/F21 统一 benchmark schema、公开目标、coverage/crash 口径、AFL stats、抽样和 统计；F60 把 backend oracle、semantic gate、digest 和 claim gate 写成可执行证据； F67 提供 sealed randomized paired protocol。后续各技术族继续把证据内建：

• F198：String/BV cross-solver conformance；
• F221：schedule SMT 跨 solver 可移植性；
• F226：PCFG 五档 confirmatory ablation；
• F228/F230-F235：parser cache/forest/cross-parser calibration；
• F244-F246：固定 solver identity、holdout、leakage check；
• F247：AFL edge/data coverage join；
• F263-F274：compiler transformation manifest、seal 和独立 replay。

一份可用于科研结论的运行至少应保存：

1. source revision 与 dirty-worktree 状态；
2. compiler、LLVM、Z3/cvc5/Bitwuzla、AFL++ 和 target binary identity；
3. corpus、dictionary、random seed、CPU affinity 和总 CPU 预算；
4. 完整配置与 capability；
5. 原始 telemetry、coverage maps、query/schedule/parser/transform artifacts；
6. baseline、逐项消融和 full system；
7. 多轮结果、coverage AUC、time-to-target、accepted/CPU-hour、solver CPU；
8. median、bootstrap confidence interval、effect size 和失败运行。

项目现有 B 级历史数字可以说明某优化机制在特定环境可工作，但不能与不同 harness、 CPU 配额或版本的结果直接拼成 SOTA 对比。

20. 配置使用导航

建议从已定义 profile 启用功能，不要一次手工打开数十个开关。profile 会同步设置 依赖、hard guard、预算和输出路径；自定义实验则应保存规范化后的完整环境。

21. 代码与测试导航

当前快照包含：

• compiler/ 顶层 24 个 C++/header 文件；
• util/ 顶层 64 个 Python/C 工具；
• test/ 顶层 154 个 .py/.c/.ll 测试源；
• Configuration.txt 中 373 个唯一 SYMCC_* 配置名；
• New_Implementation_Archive.md 中连续的 275 个功能 ID。

这些数量只能说明覆盖面，不能替代测试结果。常用入口如下：

本快照在 2026-07-29 重新执行了两套全量门禁：

PATH=/usr/lib/llvm-18/bin:$PATH ninja -C build check
  -> 155/155 passed, 114.18 s

python3 -m unittest discover -s test -p 'test_*.py'
  -> 459/459 passed, 109.060 s

文档自身还执行 generate_current_technology_index.py --check、本地 Markdown 链接 检查、Python py_compile 和 git diff --check。这些结果证明当前机制回归通过， 不替代真实目标的等 CPU、多轮覆盖率实验。

22. 当前边界与不应夸大的结论

1. 实现不等于 SOTA 实验结论。 最新 full system 缺少统一版本下的等 CPU、多轮、 全消融 R 级结果。
2. GenSym/ConDPOR/IFSS/SymCC-str 均为有界实现。 项目覆盖论文思想的重要可执行 子集，但不能用论文名称暗示已复刻全部语义或证明。
3. 学习和 agentic 模块不可信。 它们只能排序或提议，不能授权 UNSAT、覆盖或 程序等价。
4. 跨前缀复用不传播 UNSAT。 SAT model、poly sample 和字段重命名始终需要当前 完整约束验证。
5. AFL data namespace 可能碰撞。 scheduler 的显式结构键 tracker 才能区分 (object, offset, width, kind)，但它记录的是观测到的最佳进展，不是程序语义完备性。
6. 多 coordinator 依赖共享存储语义。 当前不是无共享存储的拜占庭一致性系统。
7. proof artifact 有边界。 seal/replay 可检测本地漂移和证据篡改，不等于形式化 验证、密码学签名或远程 attestation。
8. LLVM lowering fail closed 会损失覆盖范围。 保守拒绝是 correctness 选择， 不是“所有输入程序都已经支持”。

23. 可归纳的研究创新

不借用论文名称，仅从当前系统本身看，可以归纳出五个有研究价值的组合创新：

1. 多粒度并行统一闭环：seed、query、schedule 和 continuation state 使用版本化、 可互操作的 telemetry/artifact contract，并在具体化后汇入 coverage ownership 与 可信接纳边界；它们不是一个完全相同的 JSON schema；
2. Query IR 作为跨层证据总线：求解复用、字符串、语法补洞、schedule 和 holdout campaign 共享内容身份和验证语义；
3. 双覆盖平面：AFL 兼容位图保证生态互操作，显式结构键的 data/grammar/structure 状态提高调度与研究测量的可解释性；
4. 激进 proposal、保守 acceptance：polyhedral renaming、optimistic slice、 grammar/PCFG、agentic route 和 Hydra transformation 都可增加召回，但正确性由 独立 validator/replay 保持；
5. 证明携带的系统优化：编译变换、parser forest、solver strategy 和 coverage join 不只输出结果，还输出可重算的结构证据和 sealed experiment identity。

这些是合理的系统设计贡献候选。是否能形成论文主张，仍应由 R 级公开 benchmark、 消融和与最强 baseline 的公平对照决定。

24. 完整功能索引

下表由 New_Implementation_Archive.md 和 Development_History_Traceability.md 自动抽取。每个 F00-F274 必须恰好出现一次； 生成器在缺号、重号、标题缺失或状态缺失时失败。

25. 关联文档

• Architecture_QA3.md：执行次序、位图、约束形态、求解策略、 种子影响、ICSE'23 和 benchmark 的逐问分析；
• Correctness_Review_Fixes_2026-07.md： correctness 审查和修复；
• sota_hybrid_execution_2026.md：学术来源、SOTA 映射和边界；
• SOTA_Gap_Audit_2026-07-24.md：逐论文语义差距；
• Recent_Work_and_Next_Research_Plan.md： 近期实现和后续研究；
• ../benchmark/README.md：benchmark 命令、schema 和产物。

主要技术来源包括 QSYM、 Backsolver、 Pangolin、 GenSlv、 PSCache、 SymCC-str、 Lase、 Data Coverage、 CoFuzz、 GenSym、 ConDPOR、 Hydra、 SMTgazer、 Cottontail 和 UCSan。 论文中的性能数字、证明和适用范围属于原论文；本文只描述本仓库已经实现并有证据 支持的部分。