本文回答 6 个问题：并行框架的执行流程与位图、约束形态与编译方式、求解策略与占比、 输入对 DSE 的影响、ICSE'23 统一再评估、基准目标与 LAVA-M 结果。
证据规则：每个结论都标注来源。
file:line= 当前工作树（分支engine-configurable-symsan）实读； 【实测】 = 为写这份文档当场跑出来的新数据（已脚本化项目见benchmark/qa3_repro/，并非每项都已有 driver）； 【B 级】 = 历史阶段报告中的旧数据，按docs/README.md:41-43的规则不能直接升级为结论； 【论文】 = 取自论文原文（Q5 全节），不在本仓库里，引用时不要写成"仓库记载"； 【缺】 = 仓库里确实没有的数据，明确标出而不是编造。2026-07-29 核验补充：本文把三种容易混淆的数字严格分开： （1）当前仓库已提交 CSV，可证明吞吐与边覆盖； （2）QA3 单次专项短测，可解释机制但不能代表生产分布； （3）历史
/tmp语料重放，可追溯但不是当前仓库内可独立复算的正式结果。 求解“占比”默认指输出文件的策略标签构成，除非明确写成check()次数占比。可复现性边界：本文引用的是一个尚未封存的工作树，分支名和
file:line不是不可变证据。 正式发表或对外复现实验前，必须同时记录主仓库提交、子模块提交、dirty diff 摘要、编译器/ AFL++/Z3 版本，以及脚本、输入语料和结果 CSV 的内容清单。下文的行号用于代码导航， 不能替代这一份实验清单。全文共 22 张图（ASCII，可直接复制进幻灯片）：进程拓扑、五张位图全景、工作项时序、 过滤漏斗、约束形态分流、求解决策树、丢前缀粒度对比、嵌套深度对照、种子长度阶梯等。
本文的审查历史与置信度（如实记录，供读者判断可信度）：
轮次 做法 查出的问题 初稿 读代码 + 当场补测 —— 第 1 轮 3 组 agent 逐条对照代码 5 处真错（含一段我伪造的终端记录）、~40 处引用漂移；顺带查出 mpi_fuzzing_helper.py一个TypeError崩溃 bug 并修复第 2 轮 杜撰审计 + 联网补文献 发现运行中的 AFL 不接收 concolic 产出（§1.10，两个独立实验）；补齐 PCGUARD、 AFL_SYNC_TIME、QSYM/SoK 原文第 3 轮 逐篇核对论文原文 修正 Böhme et al. 的会议（SoK 标为 ASE 2022，实为 ICSE 2022）与建议归属；补 QSYM Table 6 后修正了"AFL 拿 0 个 bug"的口径 结论：每一轮都查出过真错误。 引用本文数据前，优先用
benchmark/qa3_repro/里的脚本自己跑一遍； 论文相关内容一律回原文核对（出处见文末"主要外部原始资料"）。
用户问题里最关键的两句，直接回答：
| 判断 | 用哪个位图 | 在哪个哈希空间 | 存在哪 |
|---|---|---|---|
| worker 判断"这个分支/上下文是否值得再次尝试" | QSYM 自己的 AflTraceMap（qsym_bitmap） |
XXH32(site_id, taken) % 65536，边索引 (prev_loc>>1) ^ h；QSYM 代码沿用变量名 pc，实际入参是编译器生成的稳定 site_id |
每 worker 私有文件，worker_dir/qsym_bitmap，131072 字节（64KB trace + 64KB context） |
| 判断"这个新产出是不是重复" | AFL 边覆盖位图（worker 端 worker_cov → master 端 coverage） |
AFL 插桩的边 ID（本项目 clang-18 走 PCGUARD，链接期顺序分配 guard 下标，非 prev_loc 异或；MAP_SIZE=65536 起步，可增长） |
纯内存 Python bytearray，从不落盘；由 afl-showmap 跑 AFL 插桩二进制产生 |
这两张图属于互不相通的 ID 空间，代码里明确要求分离（严格说全系统有三个 空间，第三个见 §1.8）。B3 是兴趣/尝试状态，不证明目标分支曾经 SAT、模型已落盘， 更不等价于“这个分支已经成功解过”。**
util/mpi_fuzzing_helper.py:4475-4479： ```pythonQSYM 内部剪枝图和 AFL showmap 图属于不同哈希空间，必须分离。前者仅由¶
本 worker 的 QSYM runtime 持久更新；后者通过 MPI delta 播种 worker 去重。¶
solver_bitmap_file = os.path.join(worker_dir, "qsym_bitmap") worker_env = os.environ.copy() worker_env["SYMCC_AFL_COVERAGE_MAP"] = solver_bitmap_file
并且 `util/mpi_fuzzing_helper.py:4687-4688` 再次强调：pythonAFL coverage 只通过 MPI 的完整快照/稀疏 delta 更新 worker 端去重状态。¶
它不会写入 solver_bitmap_file，避免污染 QSYM 自己的分支哈希空间。¶
```
仓库里有两个独立的 MPI 驱动，只有第一个和 AFL/位图有关：
| 工具 | 行数 | 角色 | 是否耦合 AFL | "新不新"的判据 |
|---|---|---|---|---|
util/mpi_fuzzing_helper.py |
5320 | rank 0 = master，rank 1..N-1 = concolic worker | 是（读 AFL 队列、写回） | afl-showmap 边覆盖 |
util/mpi_concolic_execution.py |
826 | 多 master（comm.Split 分组）+ worker |
否 | 仅 SHA-256 内容哈希 |
mpi_concolic_execution.py 全文 0 次 showmap（内容新颖度判据见 :430-440），产出用裸 sha256 十六进制命名，不是 AFL 能 sync 的 id:...,src:... 格式。下文谈位图，一律指 mpi_fuzzing_helper.py。
本文后续的大多数位图与漏斗数据来自经典 native concolic 流，但当前实现还包含一条 opt-in 的可恢复 continuation/CAS 状态流。二者共用 MPI 调度、fenced lease 和最终 AFL 新颖性仲裁，却不是同一种执行语义：
A. 经典 native concolic（默认）
AFL seed → TAG_WORK → 落地输入 → 新起 SymCC/SymSan 目标进程
→ B3 筛分支 → 求解并写候选 → AFL showmap → B2 → TAG_RESULT → B1 → AFL queue
B. continuation/CAS 状态级执行（SYMCC_LIVE_PROGRAM 或 SYMCC_LIVE_LLVM）
seed → master 建初始 CAS checkpoint → fenced state lease → TAG_WORK(continuation_id)
→ worker 恢复 LiveContinuationExecutor → 有界执行/分叉
→ halted states + resumable frontier checkpoints → TAG_RESULT
→ master 校验 fence，恢复 descriptor 并把 frontier 重新入队
→ SAT 输入候选仍回到正常 AFL bitmap triage，不能绕过 B1
util/mpi_fuzzing_helper.py:2511-2555 加载 continuation IR，创建共享
LiveStateStore 和初始执行器；worker 在 :4507-4523 保持一个跨 lease 存活的
LiveContinuationExecutor；continuation_id 的任务在 :4703-4759 先于种子导入恢复 CAS checkpoint，
并按 SYMCC_LIVE_STEPS_PER_LEASE / SYMCC_LIVE_STATES_PER_LEASE 有界推进；:3917-3958 先做 fenced-lease commit，再恢复返回的 frontier descriptor
并重新入队，因此过期 worker 结果不能重复提交；docs/Configuration.txt:1852-1880）；这是状态级路径的 context reuse，不应与
经典 native 路径每次新起目标进程混写；SYMCC_ASYNC_QUERY_WORKERS>0 还可启动持久 query service（helper :1747-1800），
但 SAT 候选仍必须经过目标重放与 AFL 新颖性验证。范围声明：§1.2–§1.10 若未特别注明，描述 A；涉及 continuation 的结论会显式写 B。
┌──────────────────────────── 一台机器（或一个 MPI 通信域）────────────────────────────┐
│ │
benchmark/ │ ┌─── AFL++ 实例群（独立进程，非 MPI）──────────┐ ┌─── MPI 通信域（mpirun -np N）──┐ │
run_benchmark.py ────┼──▶│ fuzzer01 (-M, 带 cmplog -c … -l 2AT) │ │ rank 0 = Master │ │
run_hybrid() │ │ fuzzer02 (-S, explore-cmplog) │ │ rank 1..N-1 = Concolic Worker │ │
│ │ fuzzer03 (-S, mopt-fast) │ └───────────────┬────────────────┘ │
│ │ … （核数 = 总核数 − SymCC 占用） │ │ │
│ └───────────────────┬───────────────────────┘ │ │
│ │ │ │
│ 共享文件系统目录 afl_out/ │ │
│ ┌───────────────────▼───────────────────────────────────────────▼───────────────┐ │
│ │ fuzzer01/queue/ ◀── master 扫描取种子；也被 master 直接写入 id:symcc_* │ │
│ │ fuzzer0N/queue/ │ │
│ │ symcc01/queue/ ◀── master 写入被接受的 concolic 产出（AFL 当兄弟实例 sync） │ │
│ │ symcc01/extras/ ◀── master 写入 hint token（AFL 当字典用） │ │
│ │ symcc01/{hangs,crashes}/ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
└────────────────────────────────────────────────────────────────────────────────────┘
可选伴随进程：honggfuzz、GRIMOIRE 生成器（在 AFL 之前启动）
核数分配：SYMCC_WORKER_CAP=12 → symcc_ranks = max(2, min(np//2, 13))，其余全给 AFL
另外两个容易误认的模块：
- util/hybrid_feedback.py（3939 行）是纯策略库，无进程、无 MPI、无 AFL，只把覆盖增量当标量奖励（:3338, :3506）；
- util/symcc_fuzzing_helper/（Rust）是上游单进程版，单线程轮询 AFL 队列、空则 sleep 5s（src/main.rs:305-323），是 MPI 版的祖先，不在并行路径上。
benchmark/run_benchmark.py:2131 run_hybrid() 用 subprocess.Popen 拉起最多五类进程。次序有硬约束：
afl_out/ 和 work_dir/target_cwd/（:2160-2165）——CWD 隔离，否则 sqlite 之类目标会往仓库里拉屎；:2172-2181）、GRIMOIRE（:2188-2199）——都在 AFL 之前；:2353-2354）。fuzzer01 是 -M，其余 -S 且分配不同调度 profile（:2306-2351）；afl_out/fuzzer01/fuzzer_stats 出现，最多 30s，每 0.5s 轮询（:2364-2397）。只等 master 一个；symcc_all_outputs/（:2404-2405）；mpirun -np <symcc_np> python3 -u util/mpi_fuzzing_helper.py -a fuzzer01 -o <afl_out> -n symcc01 --save-all <dir>（:2412-2427, :2471-2474）；afl_out/symcc01/{queue,hangs,crashes}（:1729-1734）。
⚠ 顺序陷阱：自适应控制器不能预先创建 symcc01/——helper 默认 SYMCC_RESUME=0，见到已存在的目录会拒绝续跑并直接退出（:1712-1725；设 SYMCC_RESUME=1 则相反，会接着跑）；控制器为此要等它 30s（benchmark/run_benchmark.py:2020-2026）；send(TAG_READY) → recv（:4656-4664）。master 读 fuzzer_stats 建 AflConfig（:1924）——AFL 的目标 argv 和 afl-showmap 路径都是从这里解析出来的（:479-511）。核数分配：SYMCC_WORKER_CAP = 12（benchmark/run_benchmark.py:82），symcc_ranks = max(2, min(np//2, CAP+1))，剩下全给 AFL（:3824-3839）。这个上限是实测出来的，见 Q5 §5.3。
MPI 标签 TAG_WORK=1 / TAG_RESULT=2 / TAG_STOP=3 / TAG_READY=4（:104-107）。
TAG_READY 排干进 idle_ranks（:3821-3837），只派给 rank ≤ max_active_workers；更高的 rank 被泊车（阻塞在 recv，~0 CPU），由文件 symcc01/.active_workers 控制（:3087, :3126-3132）；TAG_WORK 载荷含：内容寻址的输入（object_id + 首次才带 object_content，:3699-3709）、策略/参数覆盖、以及位图 delta（:3710-3718）；TAG_RESULT，里面的 new_tests 已经在 worker 端去过重（:5065-5092）。经典 native 流只在内容寻址失败时用文件系统兜底（shutil.copy2，:4790-4791），正常
输入传输走 MPI 字节，因此该流跨节点不要求共享输入 FS。continuation 流例外：当前
SYMCC_LIVE_STATE_STORE 必须对所有 rank 可见，非共享文件系统的 CAS 复制尚未实现
（docs/Configuration.txt:1923-1929）。
┌─────────────────────────────── AFL 边 ID 空间 ────────────────────────────────┐
│ （PCGUARD edge id，MAP_SIZE=65536 起步，afl-showmap 已分桶 1/2/4/…/128） │
│ │
┌────────────┐ │ ┌──────────────┐ ┌──────────────────────────────┐ │
│ AFL 进程 │ │ │ B5 AFL 执行时 │ ◀── afl_data_coverage_rt.c (AFL_PRELOAD) │ │
│ fuzzer01… │───────┼──▶│ 共享位图 │ hook memcmp/strcmp，每匹配 1 个前缀字节点亮 1 槽 │ │
└────────────┘ │ │ __afl_area_ptr│ → 匹配 N→N+1 写散列 feature（可能发生碰撞） │ │
│ └──────────────┘ │ │
│ │ │
┌────────────┐ │ ┌──────────────┐ MPI: BitmapDeltaJournal ┌──────────────┐ │ │
│ Master │ │ │ B1 helper 位图 │ ──── 版本号 + 稀疏 delta ─────────▶ │ B2 worker 位图│ │ │
│ (rank 0) │───────┼──▶│ CoverageBitmap│ （落后超窗口则发全量快照） │ CoverageBitmap│ │ │
└────────────┘ │ │ 内存 bytearray│ │ 内存 bytearray│ │ │
│ │ 【从不落盘】 │ ◀─── TAG_RESULT 里的稀疏边列表 ──── │ 本地预过滤 │ │ │
│ │ helper 内裁决 │ └──────▲───────┘ │ │
│ └──────────────┘ │ │ │
│ afl-showmap 跑 │ │
│ ┌──────────────┐ 【AFL 插桩二进制】 │ │
│ │ B4 gossip 分片│ ◀── 多 master 才启用（opt-in） （绝不是 SymCC 的） │ │
│ │ 磁盘 JSON │ │ │
│ └──────────────┘ │ │
└─────────────────────────────────────────────────────────────────────────────┘
┌──────────────────────── QSYM 自有哈希空间（完全独立！）────────────────────────┐
┌────────────┐ │ ┌────────────────────────────────────────────────────────────────────┐ │
│ Worker │ │ │ B3 qsym_bitmap ── 每 worker 私有【文件】，131072 B │ │
│ (rank k) │───────┼──▶│ = trace_map(64KB) ‖ context_map(64KB) │ │
│ └ concolic │ │ │ 索引 = (prev_loc>>1) ^ XXH32(site_id, taken) % 65536 │ │
│ 子进程 │ │ │ 由 QSYM runtime 自己写（isInterestingBranch 内 commit()） │ │
└────────────┘ │ │ 用途：【这个分支/上下文是否值得再次尝试】 │ │
│ └────────────────────────────────────────────────────────────────────┘ │
└────────────────────────────────────────────────────────────────────────────┘
⚠ B3 与 B1/B2 索引空间不通、绝不互相写入（mpi_fuzzing_helper.py:4475-4479 / :4687-4688）
| # | 名字 | 位置 | 大小 / 空间 | 干什么 |
|---|---|---|---|---|
| B1 | master coverage (CoverageBitmap) |
内存 bytearray + set[int]，:2407 |
惰性 65536，可增长 | helper 已观察到的 AFL edge/hit-count bucket bits；只在本 helper 会话内最终裁决 concolic 候选，不是 AFL campaign 的持久 virgin map |
| B2 | worker worker_cov |
内存，:4580 |
由 B1 经 MPI delta 播种 | 上报 master 前的本地预过滤；在确定性重放、相同目标/环境/map 下保持 coverage |
| B3 | qsym_bitmap |
文件 worker_dir/qsym_bitmap，:4477-4479 |
2×65536 = 131072 B，XXH32 空间 | 分支方向/上下文的兴趣与已尝试状态，在 concolic runtime 内部剪枝；不是 SAT/成功求解记录。⚠ 只存在于 SymCC/QSYM 路径：SymSanEngine 不读 SYMCC_AFL_COVERAGE_MAP |
| B4 | CoverageOwnerShardGossip 分片 |
磁盘 JSON，symcc01/.coverage_owner/state/NNNN.json |
按 bitmap 下标分片 | 跨 master（多节点）全局新颖性仲裁，opt-in |
| B5 | AFL 目标执行时共享图 __afl_area_ptr |
每个 AFL 目标执行绑定的 shm | MAP_SIZE 65536 |
AFL_PRELOAD 写入数据进展 feature；AFL 实例自己的 virgin state 决定是否保留（见 §1.8） |
加一层非位图去重：内容哈希（§1.7）。
还有两处容易漏的：
- B6 语法位图：util/semantic_proposals.py:419 的 GRAMMAR_BITMAP_SIZE = 1 << 16 + grammar_bitmap，在 --adaptive 路径上默认启用（mpi_fuzzing_helper.py:92, 2287），用于结构化提议的新颖性判定——第六张图；
- 分片版 delta journal：SYMCC_BITMAP_SHARDS > 1 时 ShardedBitmapDeltaJournal（distributed_state.py:143）会取代下面讲的 BitmapDeltaJournal（:2997-2999）。
代码在 vendored QSYM 里：runtime/src/backends/qsym/qsym/qsym/pintool/afl_trace_map.cpp。
// :16-34 分支哈希：只哈希传入的 site identity 和方向，和 AFL edge ID 毫无关系
XXH32_hash_t hashPc(ADDRINT pc, bool taken) {
XXH32_state_t state;
XXH32_reset(&state, 0);
XXH32_update(&state, &pc, sizeof(pc));
XXH32_update(&state, &taken, sizeof(taken));
return XXH32_digest(&state) % kMapSize; // kMapSize = 65536, :5
}
// :66-68 边索引：模仿 AFL 的 prev_loc 混合
ADDRINT AflTraceMap::getIndex(ADDRINT h) { return ((prev_loc_ >> 1) ^ h) % kMapSize; }
判定 + 落盘（:130-162）：
bool AflTraceMap::isInterestingBranch(ADDRINT pc, bool taken) {
ADDRINT h = hashPc(pc, taken);
ADDRINT idx = getIndex(h);
bool new_context = isInterestingContext(h, virgin_map_[idx]);
bool ret = true;
virgin_map_[idx]++;
if ((virgin_map_[idx] | trace_map_[idx]) != trace_map_[idx]) {
ADDRINT inv_idx = getIndex(hashPc(pc, !taken));
trace_map_[idx] |= virgin_map_[idx];
// mark the inverse case, because it's already covered by current testcase
virgin_map_[inv_idx]++; // ← 反方向也被标记为已覆盖
trace_map_[inv_idx] |= virgin_map_[inv_idx];
commit(); // ← 立刻写回文件
virgin_map_[inv_idx]--; // ← 只还原本地命中计数;trace_map_ 的标记【不还原】
ret = true;
}
else if (new_context) {
ret = true;
commit();
}
else
ret = false;
prev_loc_ = h;
return ret;
}
文件格式 = trace_map_（64KB）紧跟 context_map_（64KB），commit()/import() 在 :107-117/:51-64。
路径来自 SYMCC_AFL_COVERAGE_MAP（runtime/src/Config.cpp:75-77 → runtime/src/backends/qsym/Runtime.cpp:130）。
调用点在 solver.cpp:4675-4685：
bool Solver::isInterestingJcc(ExprRef rel_expr, bool taken, ADDRINT pc) {
bool interesting = trace_.isInterestingBranch(pc, taken);
last_interested_ = interesting;
return interesting;
}
SEED=benchmark/public/seeds/google-fts/xml_read_fuzzer/seed_01.xml
for i in 1 2 3 4 5; do
mkdir -p out$i # SymCC 不会自己建目录,不建则 exit 255、0 产出
SYMCC_OUTPUT_DIR=out$i SYMCC_INPUT_FILE=$SEED \
SYMCC_AFL_COVERAGE_MAP=./qsym_bitmap SYMCC_TELEMETRY_OUT=tel$i.json \
benchmark/public/bin/google-fts/xml_read_fuzzer $SEED
done
| 轮 | symbolic_branches | interesting_branches | z3_solves | 输出 | solver 耗时 |
|---|---|---|---|---|---|
| 1 | 240 | 225 | 225 | 225 | 64.9 ms |
| 2 | 240 | 0 | 0 | 0 | 0.0 ms |
| 3 | 240 | 0 | 0 | 0 | 0.0 ms |
| 4 | 240 | 0 | 0 | 0 | 0.0 ms |
| 5 | 240 | 0 | 0 | 0 | 0.0 ms |
qsym_bitmap 文件大小：131072 字节（= 2×65536，和代码一致）。
读法：符号分支数恒为 240（程序没变），但第 2 轮起 interesting 归零——B3 记住了
第 1 轮已经尝试过的分支方向/上下文，所以基线策略不再发查询。这里不能推出 225 个查询
全部 SAT，更不能推出其模型都产生了有效测试。编译器在 compiler/Symbolizer.h:352-356
传入 stableSiteId；QSYM 中沿用的参数名 pc 只是历史命名，不是 ASLR 敏感的运行时地址。
此外 B3 不是不可越过的硬门：SYMCC_TARGET_BRANCH 或 S2F solve/sample 可强制设置
is_interesting=true，SYMCC_SKIP_SITES、directed pruning 或 S2F skip 则可在 B3
记账之后阻止求解（solver.cpp:1293-1380）。B3 文件仅为每 worker 私有，当前没有
跨 worker 合并，因此相同 site/context 仍可能被多个 worker 分别尝试。
类定义 util/mpi_fuzzing_helper.py:674-813。核心是重新实现的 AFL has_new_bits（:791-813）：
def _merge_sparse_delta(self, edges: list) -> int:
if self.data is None:
self.data = bytearray(_AFL_MAP_SIZE)
delta = 0
for edge_id, hit in edges:
if edge_id >= len(self.data): # 目标 map 比初值大 → 增长
self.data.extend(b"\x00" * (edge_id + 1 - len(self.data)))
old = self.data[edge_id]
new_bits = hit & ~old # 新观察到的 hit-count bucket bits
delta += new_bits.bit_count()
hit 是 afl-showmap 已经分桶（1,2,4,8,16,32,64,128）后的计数字节（因为三处调用都没传 -r/-s），所以 hit & ~old 是逐桶精确的：同一条边命中次数进了新桶也算"新"。
判定点（worker 侧，:1207-1231） —— 整个框架最关键的一段：
for entry, content in uniq:
if worker_coverage is not None and (use_batch or streaming_showmap is not None):
edges = (batch_edges.get(entry.path) if use_batch
else streaming_showmap.get_edges(content))
if edges is None: # 无 map(超时/崩溃) 或流式进程死亡
redun["showmap_none"] += 1
continue
is_new = worker_coverage.merge(edges) # ← B2 判新
...
if is_new:
tc_entry = {"content": content, "bitmap": edges} # 只有判新的才回传
判定点（master 侧，:1526-1555）：优先直接用 worker 传回的稀疏边列表，退化才自己跑 showmap；然后 coverage.merge_delta(bitmap_data)，coverage_delta > 0 才写进队列。
→ B2 是 worker 的保守预过滤，B1 是 helper 会话内的最终裁决。 在目标确定、输入重放 确定、目标 argv/环境与 map 一致时，B2 只会因状态较旧而多报候选，不会漏掉相对 B1 的新 coverage；但对并发调度、非确定性目标或同字节输入的语义多样性，它可能丢失不同执行结果。 B1 又因为没有从 AFL 队列初始化，不能代表整个 AFL campaign 的全局历史。
前面讲的是"怎么把一次执行读成边集"，这里补上"边 ID 从哪来"——这一层直接决定了 §1.0 的"两个哈希空间"论断成不成立。
本项目用 clang-18 + afl-clang-fast，走的是 PCGUARD（LLVM SanitizerCoverage 的 trace-pc-guard），不是老式的编译期随机 cur_loc。AFL++ 运行时的实现（instrumentation/afl-compiler-rt.o.c）：
/* 每条被插桩的边，执行时只做一次自增；下标【就是 guard 值本身】，没有 prev_loc 异或 */
void __sanitizer_cov_trace_pc_guard(uint32_t *guard) {
__afl_area_ptr[*guard] =
__afl_area_ptr[*guard] + 1 + (__afl_area_ptr[*guard] == 255 ? 1 : 0);
}
/* 加载期一次性分配 guard 值：全局计数器顺序递增 */
if (__afl_final_loc < 4) __afl_final_loc = 4;
*(start++) = ++__afl_final_loc;
while (start < stop) {
if (likely(inst_ratio == 100) || AFL_R(100) < inst_ratio) {
*(start++) = ++__afl_final_loc; // ← 顺序 5, 6, 7, ...
} else {
*(start++) = 0; // 抽样未命中的边禁用
}
}
/* map 大小由实际插桩边数决定，握手时协商给 fuzzer */
if (__afl_final_loc) { __afl_map_size = __afl_final_loc + 1; ... }
三个直接后果：
prev_loc 异或——所以它与 QSYM 的 XXH32(pc,taken) + (prev_loc>>1)^h（§1.4 B3）是根本不同的两套东西，无法互相索引。这就是 §1.0 那条论断的底层依据。MAP_SIZE=65536 不是硬上限，是起步值；__afl_map_size = __afl_final_loc + 1 随目标插桩规模走。这也是为什么 B1/B2 必须可增长（:796-797）——不是边界情况，是常态。__afl_final_loc 可以被外部抬高——本项目的 util/afl_data_coverage_rt.c:63-65 正是这么干的：
c
__attribute__((constructor)) static void data_cov_reserve_namespace(void) {
if (&__afl_final_loc && __afl_final_loc < MAP_SIZE)
__afl_final_loc = MAP_SIZE;
}
LD_PRELOAD 的构造函数先于主程序的 .init_array 执行，于是 guard 从 65537 起分配，低位 64 KB 留给数据覆盖（§1.8）。这就是第三个 ID 空间的来源：同一个二进制，在 AFL_PRELOAD 下的 afl-fuzz 进程里边 ID 从 65537 起，而 helper 自己跑的 afl-showmap（不带 preload）从 5 起。关键前提：跑的永远是 AFL 插桩二进制，从来不是 SymCC/SymSan 二进制。
目标 argv 从 fuzzer_stats 的 command_line 解析（:479-511），worker 复用同一个 AflConfig（:4764-4769）。
| 模式 | 命令行 | 单次成本 | 用在哪 |
|---|---|---|---|
| (c) 批量（默认热路径） | afl-showmap -I <listfile> -o <mapdir> -t 5000 -m none -q -- <afl_bin> [@@]（:1433-1437） |
~25 µs/输入 | worker 去重主路径 |
| (b) 流式 forkserver | afl-showmap -S -t 5000 -m none -- <afl_bin>（:1337-1338） |
~0.6 ms/输入 | 批量不可用时回退 |
| (a) 每输入 fork，二进制 map | afl-showmap [-Q] -t 5000 -m none -b -o <bitmap>（:627-630） |
最慢 | master triage 兜底 + K-Scheduler |
还有第四种，不在 helper 里：
benchmark/run_benchmark.py:810-818的afl-showmap -t T -m none **-C** -i <语料目录> -o <文件>——带-C，一次吃整个语料目录。 全文（尤其 Q3/Q6）引用的 ShowmapCov 覆盖率数字都出自它，不是上面三种。
批量模式不带 -b/-C，afl-showmap 给每个输入写一份文本 map，按 edge_id:count 解析（:1446-1453）：
with open(os.path.join(mapdir, os.path.basename(p))) as mf:
edges = []
for line in mf: # map 每行 "edge_id:count"
eid, _, cnt = line.strip().partition(":")
edges.append((int(eid), int(cnt) if cnt else 0))
流式模式的帧协议（:1369-1391）：[u16 status][u32 edges_count][(u32 eid, u8 count) × N][u32 stdout_len][stdout][u32 stderr_len][stderr]，用 struct.Struct("<IB").iter_unpack 解（:132），上限 _MAX_EDGES = 1<<20。
持久模式检测（决定要不要带 @@）用的是字符串而非符号（:1332-1336）：
self._uses_shmem = b"##SIG_AFL_PERSISTENT##" in _bf.read()
⚠ 这里绝不能改用
__afl_sharedmem_fuzzing符号判断——fork 模式的 cmplog 伴随二进制也定义该符号，误判会让afl-fuzz直接 "Fork server handshake failed"、所有轮次覆盖率归零（benchmark/run_benchmark.py:1438-1450）。
master 侧（:3710-3718）按 worker 的版本号决定发全量快照还是稀疏 delta；版本号只在真有新覆盖时才自增（:4233-4236）。
BitmapDeltaJournal（util/distributed_state.py:84-140）保留有界历史（SYMCC_BITMAP_HISTORY，默认 64）；worker 落后超窗口就发全量（:107-108）。
worker 侧应用（:4689-4694），apply 是按位 OR 合并（distributed_state.py:139）。
【实测】这一步的开销：见 §1.6 的相位计时，显示精度下 bmsync 为约 0.01 s、
0.02 ms/工作项；在这次短测中可忽略，但不能表述成“完全免费”。
init_from_afl 是死代码。 CoverageBitmap.init_from_afl（:691-730）本可用 AFL 现有队列预热 B1，但全仓库只有定义、无调用。master 明确跳过（:2403-2405）：
python
coverage = CoverageBitmap()
# 跳过耗时的 bitmap 初始化 — 前几个 triage 结果会自然建立 bitmap，
# 代价是初期可能有少量假阳性 (interesting)，但不影响正确性
后果：B1 从空开始，头几个 concolic 产出只要带非零 map feature 就会被 helper
判“新”，哪怕 AFL 实例自己的 virgin state 早已见过。AFL 在 sync 时仍会用自己的持久
状态再判一次，因此这是额外 I/O/排队假阳性，而不是对 AFL 保留语义的替代。.shared_bitmap 这个文件已经不存在了。 docs/Parallel_Architecture_Report.md:172、docs/PPT_Material_Complete.md:342、docs/SymCC_Technical_Deep_Dive.md:251 和两处代码注释（:1058, :5292）还在描述它。没有任何代码读写它，现役机制是上面的 MPI BitmapDeltaJournal。_snap 读错了图，而且会直接打死 worker —— 写这份文档时发现并已修复。
原代码 :1057-1068 把 SYMCC_AFL_COVERAGE_MAP 当成"全局 AFL 覆盖快照"读，但 :4479 让该变量指向 B3（qsym_bitmap，XXH32 空间、131072 B）——索引空间根本对不上。
更糟的是 :1218 写的是 any(e >= len(_snap) ... for e in edges)，而 edges 是 [(edge_id, count)] 元组列表 ⇒ tuple >= int ⇒ TypeError，且不被 :1237 的 except (IOError, OSError) 捕获，整个 worker rank 当场死掉。
触发条件：SYMCC_WORKER_PROFILE=1 且已有 qsym_bitmap（即每个 worker 的第 2 个 item 起）。这正是仓库里从来没有可用 redundancy.csv 的根本原因——一开 profiling 就崩。
本文的第一次漏斗实测就撞上了它（mpi.log 里 8 份 TypeError: '>=' not supported between instances of 'tuple' and 'int'）。
已修：快照改取自 worker_coverage.data（AFL 边 ID 空间，语义正确），并按 for eid, _ in edges 取下标。读法：下面是扁平编号，但实际有嵌套和跨进程边界——步骤 10–13 都发生在步骤 9 的
run_symcc_worker（:1022-1241）内部；步骤 16–17 在 master 进程里。相位时钟的边界：exec止于:1104，showmap_dedup起于:1110。图 1-3 的泳道图画的就是这个结构。 另有一条提前返回分支：消息里带continuation_id时，worker 直接恢复检查点并send(TAG_RESULT); continue，跳过步骤 4–15（:4699-4755）。
Master(rank0) Worker(rank k) concolic 子进程 afl-showmap AFL
───────────── ────────────── ────────────── ─────────── ───
│ │ │ │ │
│ ◀── TAG_READY ───────┤ ① │ │ │
│ {rank, bitmap_version}│ │ │ │
│ │ │ │ │
② 扫描 AFL queue + 打分 │ │ │ │
（节流 0.1s / 有空闲才扫） │ │ │ │
│ │ │ │ │
├── TAG_WORK ───────────▶│ ③ bmsync：把 B1 的 delta │ │ │
│ {object_id, 内容(首次),│ 并进 B2（实测 0.000s） │ │ │
│ bitmap delta, │ │ │ │
│ focus_bytes, 策略} │ ④ import：落地输入 │ │ │
│ │ │ │ │
│ ├── exec ─────────────────▶│ ⑤ 跑 concolic │ │
│ │ timeout -k 5 T │ 读 B3 决定哪些分支解│ │
│ │ SYMCC_OUTPUT_DIR=… │ Z3 求解 → 写产出 │ │
│ │ │ 更新 B3 文件 │ │
│ │◀─────────────────────────┤ （已记账活跃相位 31.8%）│ │
│ │ │ │ │
│ │ ⑥ blake2b 内容预去重 │ │ │
│ │ （字节相同直接扔） │ │ │
│ ├── 批量 showmap ──────────────────────────────▶ │ ⑦ 跑 AFL 插桩 │
│ │ afl-showmap -I list … │ 二进制 │
│ │◀────── 每个输入的稀疏边列表 ────────────────────┤ 0.62 ms/个 │
│ │ │ │ │
│ │ ⑧ B2 合并判新 → 只留新的 │ │ │
│ ◀── TAG_RESULT ───────┤ │ │ │
│ {new_tests[], hints, │ │ │ │
│ telemetry, retcode} │ │ │ │
│ │ │ │ │
⑨ B1 合并判新（helper 内最终） │ │ │ │
delta>0 → 原子写： │ │ │ │
(a) symcc01/queue/id:… ╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌▶│ ⑩ 兄弟目录 sync
(b) fuzzer01/queue/ ╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳╳ │ 但要等 10 分钟
id:symcc_* │ 【实测无效】运行中的 AFL 不重扫自己的 queue/ │ (AFL_SYNC_TIME
(c) extras/hint_* ├──────────────────────────────────────────────────▶│ 默认20min,-M减半)
(d) 压回 feedback 队列 │ （AFL 会把 extras/ 当字典用，这条通） │
(代数+1，自反馈环) │ │ │ ⇒ ≤300s 的轮次里
│ │ │ │ (a)(b) 都没送达
│ │ │ │ 详见 §1.10
worker_dir = mkdtemp("symcc_mpi_w{rank}_")（:4473）；置 SYMCC_AFL_COVERAGE_MAP=worker_dir/qsym_bitmap（B3，:4477-4479）；置 SYMCC_TELEMETRY_OUT/SYMSAN_TELEMETRY_OUT（:4483-4484）；建 worker_cov（B2，:4580）和 worker_seen（内容哈希集，:4581）。comm.send({"rank","bitmap_version"}, TAG_READY)（:4658）→ 阻塞 recv ——相位 wait。TAG_WORK；若 bitmap_version 前进，把 B1 的 delta 并进 B2 ——相位 bmsync（:4689-4694）。StreamingShowmap，最多重试 5 次（:4757-4777）。失败则退化为 master 侧全量 showmap。copy2 兜底）——相位 import（:4779-4805）。SYMCC_FOCUS_BYTES/SYMCC_FOCUS_SET（:4810-4820）、策略 profile（:139-157, :4826-4839）、SYMCC_TARGET_BRANCH/SYMCC_S2F_ACTIONS（:4840-4849）、SYMCC_TIMEOUT_OUT（:4915-4921）、DPOR 的 SYMCC_SCHEDULE_*+LD_PRELOAD（:4923-4957）。（SYMCC_SKIP_SITES 不是 per-item，worker 启动时设一次，:4553-4554。）ExecutionRoute（执行器类 → 引擎/命令/超时，:4864-4865）——必须在 TACE 之前，因为 TACE 要读 execution_route.engine。:4866-4902；仅 --engine symcc 生效）；建 run_output = worker_dir/output_{monotonic_ns}（:4907）。run_symcc_worker（:4964-4975）。引擎决定 argv（§1.9）。超时：内层 timeout -k 5 <timeout_sec>，外层 Python timeout_sec + 15 兜底（:1080）；killed = retcode in (124, -9, 137)（:1105）——相位 exec。os.scandir(run_output)，跳过点文件和 .hints；.hints 侧车按 offset:oldhex:newhex 解析进 hint_map（:1136-1164）。worker_seen）→ uniq（:1173-1192）。:1194-1204），退化则逐个流式 get_edges。:1207-1231），只把判新的塞进 new_tests ——相位 showmap_dedup。:4990-5040）。comm.send(result, dest=0, TAG_RESULT)（:5128），rmtree(run_output)（:5114）——相位 send。_batch_triage（:1494-1697）：B1 合并（或 B4 认领）→ 若 coverage_delta > 0：symcc01/queue/id:{queue_id:06d},src:{src_id}（tmp + os.replace，:1560-1574）；MAX_GENERATION_DEPTH 则压回 symcc_feedback_queue（:1576-1584）——这就是 concolic 自反馈环；<afl_out>/fuzzer01/queue/id:symcc_{queue_id:06d},src:{src_id}，并把内容哈希登记进 processed_content_hashes 免得回头再分析（:1585-1603）；symcc01/extras/hint_{n%4096:06d}（:1607-1637），AFL 自动当字典用；recent_byte_offsets → 下一轮的 focus_bytes 窗口（:1639-1645, :4246-4253）。killed 的父输入拷进 hangs/（:1663-1675），把
retcode > 128 && retcode != 137 的父输入拷进 crashes/（:1676-1691）。
--save-all 又位于 for tc in new_tests 内（:1516-1524），只保存已经过 worker
bitmap 的候选，而非原始全部产出。已知正确性缺陷：crash-only/hang-only 候选可能被静默丢失。 默认批量 showmap 对发生 crash/hang 的候选不生成 map 文件（
:1415-1453）；worker 随后把edges is None的候选 记为showmap_none并跳过（:1207-1216），所以 candidate bytes 不进入new_tests。 master 最后的 crash/hang 分支保存的却是本次工作的input_path（父种子），不是触发异常的 candidate。因而“无新 coverage、只触发异常”的候选可能既不进 AFL，也不进正确的crashes//hangs/。本文把它列为待修复项；修复前不能把 helper 的 crash 目录或--save-all当成完整异常语料。
这份数据仓库里此前从未产出过，而且原因不是没人跑——是一开 profiling 就崩。
redun_*.csv/phase_timing_*.csv需要SYMCC_WORKER_PROFILE=1，而该分支上有一个TypeError会在每个 worker 的第 2 个工作项打死整个 rank（详见 §1.4 第 3 条）。 写这份文档时撞到、定位、修好之后才拿到下面的稳态数据。修复前后的差别很直观：
修复前 修复后 8 个 worker 完成的工作项 9 322 反馈代数 max_depth1 3 concolic 产出 799 3,154 复现：
benchmark/qa3_repro/funnel.sh。AFL-M fuzzer01预热 25 s（持久模式，不带@@， 见下方陷阱）攒到 3,149 个队列项；再起mpirun -np 9helper（1 master + 8 worker）跑 180 s，SYMCC_TIMEOUT=10 SYMCC_WORKER_PROFILE=1 SYMCC_MASTER_PROFILE=1，目标 gfts xml。
漏斗（8 个 worker、322 个工作项，redun_rank*.csv 汇总 + redun_master.csv，schema :4638-4640）：
| 阶段 | 计数 | 占产出 |
|---|---|---|
| concolic 产出（generated） | 3,154 | 100 % |
| → 过 worker 位图 B2（reported） | 299 | 9.5 % |
| → 过 master helper 位图 B1（accepted，写入同步目录） | 167 | 5.3 % |
| 冗余成因 | 计数 | 占产出 |
|---|---|---|
| worker 内冗余（gen − reported） | 2,855 | 90.5 % |
├ 字节完全相同，直接跳过 showmap（byte_dup） |
1,098 | 34.8 % |
└ 有新边但本 worker 已自覆盖（worker_fresh） |
403 | 12.8 % |
| worker 间冗余（reported − accepted） | 132 | 4.2 % |
（redun 在代码里有四个桶：byte_dup / showmap_none / infeasible / worker_fresh。本轮
showmap_none 与 infeasible 之外还有一部分产出在 :1184-1185 被内容去重直接跳过而不计桶，
故两项之和 1,501 小于 2,855——这张表不是完全穷尽的，主漏斗 3154 → 299 → 167
才是本轮 helper 日志的总量口径。）
concolic 产出 3,154 ████████████████████████████████████████ 100.0%
│
│ ① 运行时 B3：已覆盖分支根本不求解（发生在产出【之前】，不计入 3,154）
▼
② 内容预去重 blake2b（确定性重放下同字节 ⇒ 同边集） 砍掉 -1,098 █████████████▉ 34.8% ← 连 showmap 都不用跑
│
▼
③ worker 位图 B2（afl-showmap 边集） 砍掉 -1,757 ██████████████████████▎ 55.7%
│ ┈┈┈┈┈┈┈┈┈┈┈┈
▼ 过 B2 → 299 ███▊ 9.5%
④ master helper 位图 B1（会话内最终裁决） 砍掉 -132 █▋ 4.2%
│ ┈┈┈┈┈┈┈┈┈┈┈┈
▼ 过 B1 → 167 ██▏ 5.3% ← 写入 helper/sync 目录
⑤ AFL 在实际导入后再用自身 virgin state 判断（本次 180 s 内未发生，见 §1.10）
反馈代数 max_depth = 3（产出被再次分析、再产出）
读法：
- 两级位图各自都在干实事：worker 侧砍掉 90.5 %；剩下 299 个交给 master，master 又拒掉 44.1 %（132/299）；最终 5.3 % 的 concolic 产出进得了 AFL 队列。
- 字节完全相同的重复产出占 34.8 %——对本次确定性 xml 重放，这一项无需再跑 showmap，
是内容预去重（§1.7）省下的成本；并发调度、时钟/随机数或其他非确定性输入通道会破坏
“同字节即同执行”的前提。
- worker 间冗余只有 4.2 %，比预期低得多。原因是这一轮 AFL 队列有 3,000+ 项，8 个 worker 拿到的种子差异大；种子池小的时候这个数会显著上升（对照 docs/Research_and_Optimization_Report.md:365-395：6 worker 端到端有效率 30.0 %，14 worker 降到 18.6 %——注意那是 interesting/产出 的端到端比率，对应本表的 5.3 %，不是 4.2 % 那一格）。
- max_depth=3 说明反馈环真的在转：concolic 产出被接受 → 回喂 → 再被 concolic 分析，最深迭代到第 3 代。
⚠ 一个我自己踩到、值得写进文档的陷阱：最初两次跑这个实验时我给
afl-fuzz带了@@，而 xml 的 AFL 二进制是持久+shmem 的。结果 AFL 90 秒只攒出 20 个队列项，漏斗退化成1515 → 8 → 1——看上去像"concolic 几乎全是废品"，实际是上游 AFL 被我打瘸了。量化对比见 §6.6。排查"concolic 没用"之前，先确认 AFL 本身是健康的。
── worker 侧（166 s 已记账；总墙钟 8×180 s，记账率仅 12%，见下方说明）──
send 64.96 s ████████████████████████████████████████ 39.1% 201.8 ms/项 ← 阻塞等 master 收
exec 52.82 s ████████████████████████████████▌ 31.8% 164.1 ms/项 ← 跑 concolic
wait 43.09 s ██████████████████████████▌ 25.9% 133.8 ms/项 ← 等 master 派活
showmap_dedup 4.54 s ██▊ 2.7% 14.1 ms/项
import 0.69 s ▍ 0.4% 2.2 ms/项
bmsync 0.01 s · 0.0% 0.02 ms/项 ← 位图同步几乎免费
── master 侧（180 s）──
scan(扫AFL队列) 83.60 s ████████████████████████████████████████ 1213 次 ← 队列 3000-5000 项时的真瓶颈
idle 41.32 s ███████████████████▊
triage 4.65 s ██▏ 229 次
dispatch 2.41 s █▏ 1465 次
recv 0.14 s · 293 次（36 KB）
⇒ 已完成且已记账的活跃相位中：exec 是最大计算项，位图同步可忽略。
⇒ scan 是 master 侧最大的已测相位；低记账率下只能把它视为候选瓶颈。
相位计时（8 个 worker 合计，322 个工作项）：
| 相位 | 合计 | 占已记账时间 | 每工作项 |
|---|---|---|---|
send |
64.96 s | 39.1 % | 201.8 ms |
exec |
52.82 s | 31.8 % | 164.1 ms |
wait |
43.09 s | 25.9 % | 133.8 ms |
showmap_dedup |
4.54 s | 2.7 % | 14.1 ms |
import |
0.69 s | 0.4 % | 2.2 ms |
bmsync |
0.01 s | 0.0 % | 0.02 ms |
| 合计（已记账） | 166.1 s | 100 % | — |
读法：
- bmsync 依然是 0.0 %——位图版本同步 + 稀疏 delta 合并，每工作项 0.02 ms。位图机制本身几乎不花钱，这一条在两轮实测里都成立。
- showmap_dedup 14.1 ms/工作项，平均每个工作项约 10 个产出 ⇒ ~1.4 ms/产出（单产出 showmap 成本与文档记的 0.6 ms 同量级，差异来自批量模式的固定开销摊薄）。
- 真正的大头是 send（39.1 %）和 exec（31.8 %）。send 这么大不是网络慢——MPI 的 send 会阻塞到 master 收走，所以它度量的其实是等 master。同一轮 master 侧：
[PROF] scan=83.60s/1213x dispatch=2.41s/1465x recv=0.14s/293x(36KB) triage=4.65s/229x idle=41.32s
master 把 180 s 里的 83.6 s 花在扫 AFL 队列上（队列已有 3,000–5,000 项），派发/接收/triage 加起来 7.2 s。
- ⚠ 记账率只有 12 %（166 s / 8×180 s）。相位计数器只累加已完成的片段，末次阻塞在 recv 的时间在 teardown 时被丢弃（:4625-4630）。所以上表只能读作"在干活的时候时间花在哪"，不能读成"框架开销占比"。
- 合起来的结论：在已完成且已记账的活跃片段里，exec 是最大计算项，位图同步成本
可忽略；master 的 scan 是最大的已测相位，并与 worker 的 send/wait 堆积一致。
但 12% 的低记账率不足以证明端到端因果瓶颈，下一步需要完整阻塞时间追踪或采样 profiler。
(a) blake2b-128，worker 侧，挡在 showmap 前面（:1166-1192）：
# 内容级预去重(#1,跨 item):SymCC 常吐出【字节完全相同】的重复输出(实测约 23–28%);字节相同
# → 在同目标、同 argv/环境、确定性重放下边集相同，可跳过昂贵的 showmap。
_ckey = hashlib.blake2b(content, digest_size=16).digest()
if _ckey in seen_content:
redun["byte_dup"] += 1
continue
有界集 _WORKER_SEEN_CAP = 300_000（:112），worker 生命周期。
和 showmap 去重的关系：在确定性重放假设下是省钱，放在它前面。 对调度探索、
非确定性目标或文件以外的隐式输入，同一字节串可能产生不同执行；此时内容去重会丢失
语义多样性，不能宣称无条件 coverage-preserving。
【实测】本轮 xml 上 byte_dup = 1,098/3,154 = **34.8 %**，比仓库注释里记的
23–28 % 还高；该节省只在上述确定性条件成立时有效。
(b) SHA-256，master 侧，种子级（:580-585, :591-592）：跳过内容已分析过的 AFL 种子；concolic 自己写回 AFL 队列的产出也登记进去（:1598-1601），避免自己分析自己，并由 PersistentShardLedger 跨重启持久化（:2415-2425）。
util/afl_data_coverage_rt.c 是个 AFL_PRELOAD 库，把数据流进展注入 AFL 自己的 shm 位图：
:110 afl_area_ptr_addr = (unsigned char **)dlsym(RTLD_DEFAULT, "__afl_area_ptr");
:115 const char *shm_id_env = getenv("__AFL_SHM_ID");
:120 void *area = shmat((int)shm_id, NULL, 0);
:168 for (size_t prefix = 0; prefix <= matched; ++prefix) {
:169 uint64_t h = fnv_mix(base, (uint64_t)prefix);
:170 size_t idx = (size_t)(h % afl_data_map_size);
:171 map[idx]++;
它 hook memcmp/strcmp/...，对从 0 到当前匹配长度的每个前缀写一个散列槽。因此
“匹配 N 字节 → 匹配 N+1 字节”会尝试增加一个 data-progress feature；只有该槽/计数桶
相对 AFL 实例的 virgin state 确实新颖时，AFL 才会据此保留输入。FNV 取模会碰撞，计数字节
也会饱和/分桶，所以 N→N+1 不是“必然产生新 bit”的数学保证。源码注释中的 “at least one
genuinely new” 应理解为设计意图，而非无碰撞证明。
⚠ 这引出第三个 ID 空间。
:62-65把__afl_final_loc推到MAP_SIZE之上来预留低位命名空间，所以在AFL_PRELOAD生效的 afl-fuzz 目标进程里，PCGUARD 的边 ID 会从 65536 以上开始；而 helper 自己跑的afl-showmap不带这个 preload，边 ID 从 ~1 开始。 于是 §1.0 说的“两个空间”实际是三个：QSYM 的site_id/XXH32 空间、helperafl-showmap的 PCGUARD 空间、以及 preload 生效时 AFL 目标进程内的 data-feature + 偏移后 PCGUARD 空间。helper 的 showmap 默认不带这个 preload， 所以 B5 feature 不会直接进入 B1/B2，B1/B2 的可增长性只是为 showmap 协商出的更大 map/edge ID 留余量，不能用 B5 来证明它在默认配置下必然增长。 构建与挂载：benchmark/run_benchmark.py:353-368,:2222-2229（仅 hybrid，--adaptive下默认开）。 这张图是 AFL 的，不是 helper 的——它改变的是 AFL 保留什么，从而间接改变 concolic 侧能看到什么种子。
util/concolic_engine.py:27-49 定义接口（3 属性 + wrap_run/build_argv），工厂在 :181-198。
链路：--engine（benchmark/run_benchmark.py:3142-3144）→ os.environ["SYMCC_ENGINE"]（:3231-3234）→ ExecutorPortfolio.from_environment → ExecutionRoute.engine → run_symcc_worker(engine_name=...)（:4968）→ get_engine(...).wrap_run(...)（:1075-1077）。
| SymCC | SymSan | |
|---|---|---|
| 命令 | timeout -k 5 T <目标 argv，@@→输入> |
timeout -k 5 T <fgtest> <二进制> <输入> |
| 输出目录 | SYMCC_OUTPUT_DIR=<out> |
TAINT_OPTIONS="taint_file=<in> output_dir=<out>" |
| 额外环境 | SYMCC_ENABLE_LINEARIZATION=1, SYMCC_EMIT_HINTS, SYMCC_INPUT_FILE |
focus_bytes=s-e 追加进 TAINT_OPTIONS |
| argv[0] 之后的参数 | 保留 | 丢弃（concolic_engine.py:143） |
subprocess.run 返回之后，没有任何一行代码再看 _engine：blake2b 预去重、batch_showmap_edges/StreamingShowmap、worker_coverage.merge、master _batch_triage 完全一致。关键在于 streaming_showmap._target_cmd 是AFL 插桩二进制（:4764-4769），不是 concolic 二进制——所以 showmap 对 *_symsan 的产出照样工作。产出目录的枚举是纯 scandir + 名字过滤（:1136-1141），从不解析文件名，SymCC 的 %06d 和 SymSan 的 id-* 都能直接吃。
⚠ 一处例外：TACE 密度剖析硬绑 SymCC——
engine = get_engine("symcc")（:1296），因为它依赖 SymCC 独有的SYMCC_DENSITY_OUT。不过整个 TACE 块在:4878由execution_route.engine == "symcc"把门，所以--engine symsan下它整个被跳过，那行硬编码不可达。
-M fuzzer01 / -S fuzzerNN 同一个 -o 目录（benchmark/run_benchmark.py:2306-2351），AFL_AUTORESUME=1 AFL_NO_UI=1 AFL_SKIP_CPUFREQ=1（:2214-2217）。AFL_SYNC_TIME 全仓库从未设置，所以用 AFL++ 默认值：
AFL_SYNC_TIME："allows you to specify a different minimal time (in minutes) between fuzzing instances synchronization. Default sync time is 20 minutes, note that time is halved for -M main nodes." —— AFL++docs/env_variables.md即-S每 20 分钟、-M每 10 分钟 才同步一次。
afl_out/symcc01/ 是个兄弟"fuzzer 实例"目录，靠 AFL 的 -M/-S 同步；另外 master 还直接注入 afl_out/fuzzer01/queue/id:symcc_*（:1585-1593）。这是本次审查中发现的、此前没有记录过的问题。两个独立实验：
实验 A（本文 §1.6 那一轮，180 s）——直接查产物：
symcc01/queue 产出 : 167
fuzzer01/queue 里的 id:symcc_* 直注文件 : 167
fuzzer01/.synced/ : 【空】 ← AFL 一次都没同步过 symcc01
fuzzer01 corpus_count : 4885
fuzzer01/queue 里 AFL 自产(id:0*) : 4885 ← 相等 ⇒ 167 个直注文件不在 AFL 队列里
cycles_done = 26，跑了 26 轮仍是这个结果。
实验 B（受控对照）——起一个干净的 -M fuzzer01，稳定后往它自己的 queue/ 里丢 200 个内容各异的 XML，等 120 s 再让 AFL 正常退出刷新最终统计（脚本：benchmark/qa3_repro/inject_test.sh）：
注入前 : corpus_count=2 queue 文件数=1782
注入 200 个后 120s + 正常退出:
corpus_count=2533 queue 文件数=2733 其中 AFL 自产=2533
>>> corpus_count(2533) == AFL 自产数(2533) ⇒ 直注的 200 个【未被采纳】
master 接受一个 concolic 产出后，同时写三个地方：
(a) afl_out/symcc01/queue/id:000123,src:...
│
└─▶ 靠 AFL 的兄弟目录 sync 被别的实例捡走
⏱ AFL_SYNC_TIME 默认 20 min，-M 减半 = 10 min
✗ benchmark 轮次是 120 s / 300 s ⇒ 第一次 sync 都没到就结束了
实测：fuzzer01/.synced/ 【空】，跑满 180 s、26 个 cycle 依然是空
(b) afl_out/fuzzer01/queue/id:symcc_000123,src:...
│
└─▶ 指望正在跑的 fuzzer01 直接看到
✗ 【实测无效】运行中的 afl-fuzz 只在启动/resume 时读一次自己的 queue，
之后队列只在内存里维护，永不重扫自己的目录
实测 A：corpus_count 4885 == AFL 自产 4885，167 个直注文件不在其中
实测 B：受控注入 200 个 → corpus_count 2533 == AFL 自产 2533，一个没吃
(c) afl_out/symcc01/extras/hint_000123
│
└─▶ ✓ 这条【通】：AFL 把 extras/ 当字典 token 用
┌──────────────────────────────────────────────────────────────────────────┐
│ ⇒ 在 ≤300 s 的轮次里，只有 (c) 字典 token 真正到达 AFL； │
│ (a)(b) 携带的【解本身】一个都没送到。 │
│ 所以"hybrid 覆盖率 > afl-only"是 afl-showmap 对【并集语料】的离线测量， │
│ 不是"AFL 用上了 concolic 的解"。数字没错，因果解释要改。 │
└──────────────────────────────────────────────────────────────────────────┘
修复：① 起 AFL 时加 AFL_SYNC_TIME=1
② 把 symcc01 目录加进 -F 的 foreign_dirs（代码已有这条路，只是没接上）
结论（两个实验一致）：
afl-fuzz 不会重扫自己的 queue/ 目录——直接往里丢文件是无效的。AFL 只在启动/resume 时读一次自己的队列，之后队列只在内存里维护；它只会去别的实例目录里 sync。-M 默认）。而本仓库的 benchmark 轮次是 120 s / 300 s（--timeout 默认 60 s）。⇒ 在所有 ≤300 s 的 benchmark 轮次里，concolic 的产出一个都没有真正进到 AFL 手里。
那些"hybrid vs afl-only"的覆盖率差值，来自 afl-showmap 对并集语料的离线测量（把 concolic 产出和 AFL 队列合在一起量），不是"AFL 用上了 concolic 的解之后跑出来的"。这不推翻 §6.7 的覆盖率数字（那些是并集口径，本来就成立），但它推翻了对因果的解释：短轮次里根本没有闭环反馈。
可操作的修复方向（按代价从低到高）： ① 起 AFL 时加
AFL_SYNC_TIME=1（分钟级最小值），让兄弟目录同步真正发生； ② 用 AFL++ 的-F <dir>外部语料导入。代码里已经有这条路，但没接上：run_benchmark.py:2323-2325只把foreign_dirs传给-F，而foreign_dirs的来源是AFL_FOREIGN_DIRS环境变量 + honggfuzz/GRIMOIRE 的输出目录（:2286-2291）——从不包含symcc01/。把它加进去是最小改动； ③ 承认 concolic 产出与 AFL 之间只有"离线并集"关系，并在所有报告口径里写明。这也解释了
docs/SymCC_MPI_Report_QA.md:77记的那个老问题（"AFL 实际上完全不知道 SymCC 生成了哪些输出——双方的反馈循环处于断开状态"）比原文以为的更严重：原文认为只是"不 interesting 的被丢了"，实测是连被接受的那 167 个也没送到。
AflConfig._file_cache 每文件属性缓存，MAX_FILE_CACHE = 200000 FIFO 淘汰（:473-476, :534-538）。注释记着原始代价："实测该扫描是 master 的主要瓶颈，34s/58s @ 15 workers"；SCAN_MIN_INTERVAL = 0.1（:3120）+ 三路条件（:3336-3339）：worker 都忙且刚扫过就跳过；heapq.nlargest 代替全排序（:611-616）；MAX_DEDUP_ENTRIES = 5_000_000（:3206-3220）。
【实测】这些优化确实有效，但还不够：本文实测轮（AFL 队列 3,000–5,000 项）master 是 scan=83.60s/1213次 dispatch=2.41s/1465次 recv=0.14s/293次 triage=4.65s/229次 idle=41.32s——扫描重新占了 180 s 里的 83.6 s。队列规模上千后仍需进一步优化（见 §1.6）。work_dir/target_cwd（benchmark/run_benchmark.py:2164-2165, :2351, :2473），honggfuzz 用 hf_cwd，覆盖率测量用 mkdtemp("showmap_cwd_")，批量 showmap 用独立 _bsm_ 临时目录（:1424）。下表是本文重点分析的三类常见比较场景，不是符号表达式的穷举。最终表达式同时受源码、 LLVM 优化、SymCC 插桩和运行时建模影响，不能只归因于优化器：
| 源码里长什么样 | 在哪里变成约束 | 约束形状 | 谁来加速 |
|---|---|---|---|
宽整数 icmp（4 字节 magic 一次 i32 比较） |
Symbolizer.cpp → _sym_read_memory → QSYM Concat |
一条 Equal(Concat(Read…), Const) |
fastSolveConcat（跳过 Z3） |
幸存的 memcmp/strcmp 调用 |
runtime/src/LibcWrappers.cpp 包装器 |
一条逐字节 Equal 的 And 链 |
无（一次 Z3） |
| 源码里逐字节比较的循环 | N 条独立 icmp 分支 |
N 条单字节分支 | SYMCC_MULTI_SOLVE 的连续字节联合求解 |
QSYM 表达式系统还包含 Extract、ZExt/SExt、Add/Sub/Mul/Div/Rem、位运算、
移位、关系运算和 Ite 等（runtime/.../expr.h:25-77）。真实分支经常是这些节点与
Read/Concat 的组合，例如校验和、长度关系、符号索引和带条件的数据选择。因此，
“宽整数 / libc compare / 字节循环”只能解释比较密集型路径，不能覆盖一般 QF_BV 约束。
还必须把两个正交维度分开：
| 维度 | 研究问题 | 代表机制 |
|---|---|---|
| SymCC 约束来源/形状 | 动态符号执行实际交给 fast path 或 Z3 的表达式是什么 | 宽 icmp、幸存 libc 调用、字节循环、一般算术/位向量/控制表达式 |
| AFL 侧反馈/比较引导 | 随机变异端如何更容易保留或逼近比较 | LAF、CmpLog、B5 data coverage、CTX、NGRAM |
同一个源码位置在第一维只会沿当前编译结果形成一种实际约束，但第二维可同时叠加多个 AFL 机制；laf-intel 并不是第四种 SymCC 约束。
源码： if (memcmp(buf, "SYMC", 4) == 0) { … }
│
┌───────────────┴───────────────┬──────────────────────────┐
│ │ │
-O0/-fno-builtin 常见优化构建（如 -O2） 源码本来就写成循环
│ │ │ for(i=0;i<4;i++)
│ call 指令幸存 │ LLVM 内联成 bswap+icmp │ if(b[i]!=m[i])…
▼ ▼ 或规范化成 bcmp ▼
┌────────────────────┐ ┌────────────────────────┐ ┌────────────────────┐
│ 形态 B：libc 包装器 │ │ 形态 A：宽整数比较 │ │ 形态 C：逐字节分支 │
│ Pass.cpp:964 改名 │ │ Symbolizer 原样透传谓词 │ │ N 条独立 icmp │
│ memcmp_symbolized │ │ _sym_read_memory 拼 Concat│ │ │
└─────────┬──────────┘ └───────────┬────────────┘ └─────────┬──────────┘
│ │ │
▼ ▼ ▼
一条 And 链约束 一条 Equal(Concat,Const) N 条单字节约束
n 个 Equal + n-1 个 And 一次 Z3 解出全部 4 字节 每次只解 1 字节
│ │ │
▼ ▼ ▼
否定 = "存在某字节不等" fastSolveConcat 可完全跳过 Z3 SYMCC_MULTI_SOLVE
Z3 翻 1 个字节即满足 （k∈[2,8] 直连 Concat） 联合翻转连续字节
⇒ 驱动不出逐前缀增长 ⇒ 纯 2–8 字节/常量侧最有利 ⇒ 需反馈迭代逐层解
取值侧：Symbolizer::visitLoadInst（compiler/Symbolizer.cpp:1618）把任何 load 都变成一次运行时调用（:1660-1664）：
auto *data = IRB.CreateCall(
runtime.readMemory,
{IRB.CreatePtrToInt(addr, intPtrType),
ConstantInt::get(intPtrType, dataLayout.getTypeStoreSize(dataType)),
IRB.getInt1(isLittleEndian(dataType) ? 1 : 0)});
Concat 是在运行时拼的，不在编译器里（runtime/src/RuntimeCommon.cpp:136-160）：
SymExpr _sym_read_memory(uint8_t *addr, size_t length, bool little_endian) {
if (isConcrete(addr, length))
return nullptr; // 整段具体 → 根本不建表达式
ReadOnlyShadow shadow(addr, length);
return std::accumulate(shadow.begin_non_null(), shadow.end_non_null(),
static_cast<SymExpr>(nullptr),
[&](SymExpr result, SymExpr byteExpr) {
if (result == nullptr) return byteExpr;
return little_endian ? _sym_concat_helper(byteExpr, result)
: _sym_concat_helper(result, byteExpr);
});
}
一个 8 字节 i64 load ⇒ 7 层嵌套二元 Concat，叶子是 8 个 8-bit ReadExpr。
比较侧：Symbolizer::visitCmpInst（compiler/Symbolizer.cpp:1477）完全不做比较拆分，谓词原样传下去（:1536-1540）：
SymFnT handler = runtime.comparisonHandlers.at(I.getPredicate());
auto runtimeCall = buildRuntimeCall(IRB, handler, {I.getOperand(0), I.getOperand(1)});
对该纯 magic 例子的净结果：一个 4 字节 magic ⇒ 恰好一条路径约束
Equal(Concat(Read3,Read2,Read1,Read0), Const32) ⇒ 一次 Z3 查询可同时解出 4 个字节。
这对 concolic 有利，但不能推广到所有宽比较：混合具体字节、扩展/提取、两侧均符号化、
算术或别名会进入一般求解路径。
uint64_t x; read(0, &x, 8); if (x == 0xaaaabbbbccccdddd) …
_sym_read_memory(&x, 8, little_endian=1)
│
▼ ┌── Concat ──┐
┌─ Concat ─┐ │ │
│ │ Read(7) ┌ Concat ┐
Read(0) ┌ Concat ┐ │ │
│ │ Read(6) … 共 7 层
Read(1) ┌ Concat ┐
│ │
Read(2) … ← 叶子 ReadExpr(i)，i 就是【输入字节偏移】
Z3 编码 = context_.int_symbol(i)，bv_sort(8)
最终约束（一条）： Equal( Concat(Read0..Read7), Const64(0xaaaabbbbccccdddd) )
⇒ 对纯符号字节与常量侧，一次 check-sat 可同时钉住 8 个字节。
⇒ 但 N 字节符号读 = 深度 N 的右倾链，N 很大时递归遍历无上界（kMaxDepth 是死常量）。
声明在 solver.h:304-310，由 SYMCC_FAST_SOLVE=1 开（solver.cpp:555-557，默认关），调用点 solver.cpp:5462-5466：
// Fuzzy-Sat 快速路径：简单约束不走 Z3
if (fast_solve_enabled_ && fastSolve(e, taken)) {
last_branch_solve_status_ = BranchSolveStatus::Sat;
return; // ← 直接 return，Z3 被跳过
}
接受的形状（solver.cpp:4974-5002）：根是关系运算、恰好两个孩子、一侧是 ConstantExpr（≤64 位）、另一侧是纯 Concat of 8 位 ReadExpr，字节数 k ∈ [2, 8]，偏移全部在 inputs_ 范围内。
拒绝的形状（全部落回 Z3，逐条验证过）：
ZExt(Concat(...)) / SExt(Concat(...))、移位-或重建 (b3<<24)|(b2<<16)|…、任何算术（x+1==C、x^k==C、校验和）、Concat 里混了具体字节或 Extract、>8 个符号字节、常量宽于 64 位、两侧都符号化、比较埋在 And/Ite 底下。
因此“宽比较更优”应严格读成：2–8 个纯符号输入字节组成的直接 Concat 与 ≤64-bit 常量
进行关系比较是 fastSolve 的理想输入；一般宽位向量比较仍由 Z3 或其他后端处理。
安全网（这才是它 sound 的原因）（solver.cpp:5062-5089）：
// 安全网：从"实际写入的字节"重建值并核验确实满足 negated 关系——比只核验 target 更稳健，
// 捕获偏移别名 / 分解 / 字节序错误；不满足则不写出（回退 Z3），保证 sound。
uint64_t actual = 0;
for (size_t j = 0; j < k; j++)
actual |= ((uint64_t)values[offs[j]]) << (8 * (k - 1 - j));
再加 validateCandidateAgainstPrefix(e, !taken, values)（:5086-5087），它具体求值目标谓词和每一条前缀路径约束（solver.cpp:5144-5153）。
⚠ 文档过期：
docs/Work_Progress_Report_3.md:201、docs/Parallel_Architecture_v2.md:279、docs/SymCC_Technical_Deep_Dive.md:103都还写着 "fastSolve 成功后不跳过 Z3，因此是纯增量产出"。当前代码是跳过的（solver.cpp:5462-5466）。别再引用"纯增量"这个说法。
拦截方式是改名，不是 dlsym 插桩（compiler/Pass.cpp:964-968）：
for (auto &function : M.functions()) {
auto name = function.getName();
if (isInterceptedFunction(function))
function.setName(name + "_symbolized");
}
白名单 37 个（compiler/Runtime.cpp:218-229；:225 一行放了 7 个，容易数漏）。比较类建模的是：memcmp, strcmp, strncmp, bcmp；另有 strchr, strstr, strlen, atoi, strtol, strtoul。
明显缺席：strcasecmp, strncasecmp, memmem, strrchr, strspn, wcscmp, 以及所有 *_unlocked 变体。
这套机制只在 call 指令活到 pass 时才有效。
-O2下 LLVM 经常 (a) 把memcmp(a,b,4)内联成 bswap+icmp，(b) 把memcmp(...)==0规范化成bcmp（所以白名单里专门加了bcmp，见test/bcopy_bcmp_bzero.c），(c) 常量折叠短strcmp。一旦发生，你悄无声息地拿到的是 §2.1 的宽整数路径，libc 建模一次都没跑。
符号 memcmp 变成什么（runtime/src/LibcWrappers.cpp:393-408）：
void pushMemoryEqualityConstraint(const void *a, const void *b, size_t n,
bool taken, uintptr_t site) {
auto aShadowIt = ReadOnlyShadow(a, n).begin_non_null();
auto bShadowIt = ReadOnlyShadow(b, n).begin_non_null();
auto *allEqual = _sym_build_equal(*aShadowIt, *bShadowIt);
for (size_t i = 1; i < n; i++) {
++aShadowIt; ++bShadowIt;
allEqual = _sym_build_bool_and(allEqual, _sym_build_equal(*aShadowIt, *bShadowIt));
}
_sym_push_path_constraint(allEqual, taken, site);
}
精确地说：逐字节相等链，折成一个表达式，作为一条路径约束推进去。规模线性（n 个 Equal + n−1 个 And），不爆炸；但也没有"部分学分"——它的否定是"存在某字节不等"，Z3 翻一个字节就满足了，驱动不出逐前缀增长。
两个后果值得写进设计文档：
1. _sym_set_return_expression(nullptr)（:1247）——返回值是具体的。memcmp(a,b,n) < 0 这类序关系对求解器不可见，只有相等/不等这一个分支被建模。
2. strcmp 截断到比较前缀（:1261-1279，辅助函数 comparedCStringBytes :410-423）：只约束到第一个不同字节为止——这就是经典的"每轮 concolic 前缀长一个字节"。
唯一会长度爆炸的是 strstr（:944-1008）：真正的二次方析取，护栏在 :977-980（needleLength * (haystackLength - needleLength + 1) > 16384 就放弃），外加 SYMCC_STRING_CONSTRAINT_MAX_BYTES（默认 256，硬上限 4096）。
util/string_*.py 是什么层：全部是运行时之上的纯 Python，一个都不链进插桩二进制。它们消费运行时在 SYMCC_STRING_CONSTRAINT_OUT 下吐的 JSONL（生产者 LibcWrappers.cpp:214-292，schema symcc-string-constraint-v1）。
util/string_constraints.py（1941 行）是唯一被实际使用的库（mpi_fuzzing_helper.py:94 导入）；check_string_constraints.py/check_string_operations.py/string_backend_conformance.py 是 lit 检查器；util/symcc_string_solver.py 是孤儿——全仓库无任何调用。
本项目的编译器/运行时里没有实现，一行都没有。
$ grep -rniE "laf|split[-_]compare|COMPCOV|SplitCompares|cmplog|redqueen" \
compiler/ runtime/src --exclude-dir=backends
(无输出)
（不加 --exclude-dir=backends 会有 32 条 -i 子串误命中，全部落在 vendored 的
runtime/src/backends/qsym/qsym/third_party/ 里，如 instrumentCal**lAf**ter、Index**LAf**ix。）
visitCmpInst（compiler/Symbolizer.cpp:1477-1541）整条谓词透传，不拆分。
最关键的一句（直接回答"laf-intel 的使用场景"）：AFL_LLVM_LAF_ALL 只作用于
单独的 *_afl_laf 二进制（compile_public_benchmarks.sh:1038、run_benchmark.py:108,114），
从不用于任何 SymCC/SymSan 构建。所以 laf-intel 完全不改变 concolic 引擎看到的约束——
它只是让 AFL 那一侧更容易蒙对嵌套比较，属于"另一条腿"，和 §2.0 的三种形态是正交的两件事。
但 laf-intel 是在用的——完全委托给 AFL++ 的编译期 flag：AFL_LLVM_LAF_ALL=1（benchmark/run_benchmark.py:108,112-117；benchmark/compile_public_benchmarks.sh:1038,1041）。所谓"否决"是指"不自己再造一个 pass"，不是"不用"。
现有的只是两个不可比的测量：
| 目标 | 时长 | 指标 | 结果 | 出处 | |
|---|---|---|---|---|---|
| laf | sqlite | 150 s | AFL queue 边数（中立二进制上量） | queue 602→894 边（+48% 多样性），公共覆盖 +1.4% | docs/Research_and_Optimization_Report.md:50-53 【B级】 |
| cmplog | SQLite | 120 s | ShowmapCov | AFL+CmpLog 21.03% > Hybrid 18.84% | docs/PPT_Material.md:213 【B级】 |
两者基线都不一样（cmplog 那行的对照是 SymCC Hybrid，不是 laf），时长不同（150 vs 120 s），指标不同（queue 边数 vs ShowmapCov）。而且 laf 从来没有单独测过——永远和 NGRAM-4 捆在一起。
项目自己也标注了这点（docs/Final_Work_Report.md:375）："CmpLog 数据来自独立的 120s A/B 对比实验……与 v2 全量 benchmark 实验条件不同，数值不可直接对比。此结论仅适用于 SQLite 类文本解析器，不可泛化。"
否决理由的原文（docs/工作小结.md:17）："cmplog 在嵌套/组合比较上完胜，重复建设"，定位是 "concolic 的不可替代价值 = 求解 cmplog 也解不了的校验和 / 哈希类约束"（:20）。
【缺】"嵌套/组合比较上完胜"这句在本仓库内没有任何实测支撑。 写文档时应说成"依据外部调研 + 定位判断"，不能当成本项目的测量结论。
同一份源码，编出 5 类二进制，各自带不同技术：
┌────────────────────────┬───────────────────────────────┬──────────────────────────┐
│ 二进制 │ 编译方式 │ 影响 concolic 看到的约束? │
├────────────────────────┼───────────────────────────────┼──────────────────────────┤
│ *_symcc / *_symsan │ symcc -O2 / ko-clang -O1 │ ✅ 【只有它】 │
│ *_afl（默认） │ afl-clang-fast -O2 │ ❌ 只供 AFL + showmap 用 │
│ *_afl_laf │ + AFL_LLVM_LAF_ALL=1 │ ❌ laf-intel 在这里 │
│ *_afl_ctx / _ngram4 │ + AFL_LLVM_CTX / NGRAM_SIZE │ ❌ │
│ <suite>-cmplog/* │ + AFL_LLVM_CMPLOG=1 │ ❌ 供 afl-fuzz -c 用 │
│ <suite>-cov/* │ gcc --coverage -O0 -g │ ❌ 只供 lcov/gcov 量覆盖率 │
└────────────────────────┴───────────────────────────────┴──────────────────────────┘
⇒ 所以 laf-intel / cmplog / NGRAM / CTX 全都【不改变 concolic 引擎看到的约束】。
它们改的是 AFL 那条腿：把嵌套/组合比较拆开，让随机变异更容易蒙对。
和 §2.0 的"三种约束形态"是【正交的两件事】——形态由优化器决定，与这些 flag 无关。
⇒ 分工：cmplog/laf 负责"能被拆开的比较"，concolic 负责"拆不开的"（校验和、哈希、
宽整数魔数）。仓库对 laf-intel 的"否决"是指不再自己造轮子，不是不用。
AFL_CMPLOG 这个运行期变量）：AFL_LLVM_CMPLOG=1，产出 <suite>-cmplog/ 兄弟目录（compile_public_benchmarks.sh:1042，变体表在 :1037-1043；run_benchmark.py:339-347）；afl-fuzz … -c <cmplog_binary> -l 2AT（run_benchmark.py:2334 hybrid / :2677 afl-only）；master-cmplog，在 run_benchmark.py:2311-2314 内联拼出），另有 explore-cmplog, laf-exploit, laf-seek, ngram-lin（:118-133）；afl-fuzz 直接 "Fork server handshake failed"（README.md:511-514）。检测器必须用 ##SIG_AFL_PERSISTENT## 字符串而非 __afl_sharedmem_fuzzing 符号（原因见 §1.4 引用的 run_benchmark.py:1438-1450）。运行期门禁在 :2332：cmplog_ok = bool(cmplog_binary) and cmplog_persistent == runner_persistent。| 变体 | 命令 | 出处 |
|---|---|---|
| SymCC 微目标 | symcc -O2 <src> -o <name>_symcc |
util/concolic_engine.py:79-81 |
| SymSan 微目标 | 同 argv，编译器换 ko-clang，环境 KO_CC=clang-18 KO_USE_FASTGEN=1 KO_DONT_OPTIMIZE=1 KO_USE_NATIVE_LIBCXX=1 |
concolic_engine.py:169-178 |
| SymCC 公开目标 | CC=build/symcc CFLAGS="-O2 …" SYMCC_OUTPUT_DIR=/tmp/output ./configure --quiet + make -j$(nproc) |
compile_public_benchmarks.sh:240-257, :1148-1155 |
| AFL | CC=afl-clang-fast CFLAGS="-O2" ./configure --quiet --disable-shared + make |
compile_public_benchmarks.sh:883-891, :1008-1011 |
| cmplog 伴随 | 同上 + AFL_LLVM_CMPLOG=1 |
compile_public_benchmarks.sh:1041 |
| 覆盖率 | gcc --coverage -O0 -g → <suite>-cov/ |
run_benchmark.py:425-428; compile_public_benchmarks.sh:625,668,737,766,834 |
symcc wrapper 的真身（compiler/symcc.in:41-47）：
exec "$compiler" @CLANG_LOAD_PASS@"$pass" "$@" \
-L"$runtime_dir" -lsymcc-rt -Wl,-rpath,"$runtime_dir" -Qunused-arguments
插件在 LLVM 13+ 的 pipeline start 注册顺序是
IFSSSwitchLowering → IFSSLoopSummary → IFSSExitLowering → IFSSContinuationLowering
→ IFSSContinuationMemory → HydraTransformation → LiveContinuationExport → Symbolize
（compiler/Main.cpp:117-127）。这些 pass 总会被注册，但各研究特性由环境变量门控；
“正常编译”不能再简化成只运行一个 Symbolize pass。优化级别也不是全项目统一常量：
SymCC 公开目标常见 -O2，SymSan 脚本常见 -O1，覆盖率目标为 -O0 -g，目标自己的
构建系统还可能覆盖 flags。
两个对 §2.2 至关重要的目标特定 hack：
- LAVA-M 的 lib/unlocked-io.h 被改写，把 *_unlocked 映射回标准版（compile_public_benchmarks.sh:212-238）。原注释（在 :205-208）："SymCC 运行时只包装标准版本……不禁用的话，所有输入读取绕过 SymCC，导致 0 个符号约束、0 个测试用例。" AFL 版为保持一致也打同样的补丁（:985-1006）；
- glibc ≥2.28 和 O_SEARCH 兼容补丁（:158-194）。
注意：真实目标构建里从来没有 -fno-builtin。
$ grep -rn "fno-builtin" benchmark/*.sh benchmark/*.py scripts/*.sh
(无输出)
这是"正常编译"和"自测试"之间最重要的一处不对称——见 §2.5 表格最后一行。
驱动只有 8 行有效代码（test/lit.cfg:17-25，此处略去 import）：
config.name = "compiler"
config.test_format = lit.formats.shtest.ShTest()
config.suffixes = [".c", ".cpp", ".ll", ".py"]
config.substitutions += [("%symcc", config.test_exec_root + "/../symcc"), ("%python", "python3")]
唯一全局环境变量是 SYMCC_OUTPUT_DIR（test/lit.site.cfg.in:31）。替换符还有 %filecheck %querysolver %queryservice %schedrt %opt %passlib（:37-46）。
后端相关的 FileCheck 前缀：qsym → QSYM+ANY；simple → SIMPLE+ANY（test/CMakeLists.txt:15-28）。运行入口 make check → lit（:32-38）。
清单（test/ 一级目录 176 个普通文件）：.ll 53（+regression/ 1）、.c 53、.py 48、.test32 17、.cpp 0（尽管后缀声明里有）。
大类：backsolver_* 37（全是 .ll，其中 10 个是 backsolver_*_reject 反例；全库 *reject*.ll 共 11 个）、test_*.py 40、poly_* 10、query_* 7、string* 6、hydra_* 5、directed_* 5，外加约 43 个上游经典（if.c loop.c integers.c strings.c …）。约 25% 上游 / 75% 本项目新增。59 个带 REQUIRES: qsym。
%symcc 不是"编译并运行"的宏，它就是 build/symcc 这个路径，是个 clang drop-in。每个测试都自己写全 编译 → 运行 → 检查。
五种 RUN 行形态：
1. 编译 → 喂 stdin → FileCheck 合并的 stdout+stderr（2>&1 是必须的，后端日志走 stderr）；
2. 冒烟测试，完全没有 CHECK（test/load_store.ll:27-29），退出码就是断言；
3. IR 级 pass 测试——直接喂 opt，绕开 clang（test/backsolver_switch_ifss.ll:2）：
; RUN: env SYMCC_IFSS_SWITCH_STATE=1 %opt -load-pass-plugin=%passlib -passes=ifss-switch-lowering -S %s -o %t.lowered.ll
%opt -passes=verify 作为 IR 良构门禁出现了 66 次；
4. 跑插桩二进制，断言产出的输入字节 + telemetry JSON——现代主力形态。SYMCC_AFL_COVERAGE_MAP 出现在 38 个文件里；
5. 自包含 Python unittest（# RUN: python3 %s，46 次）。
代表性例子 1 —— 这就是宽整数 magic 的情形（test/integers.c，完整）：
// RUN: %symcc -O2 %s -o %t
// RUN: echo -ne "\x05\x00\x00\x00\x00\x00\x00\x00" | %t 2>&1 | %filecheck %s
uint64_t g_value = 0xaaaabbbbccccdddd;
int main(int argc, char *argv[]) {
uint64_t x;
if (read(STDIN_FILENO, &x, sizeof(x)) != sizeof(x)) { ... }
fprintf(stderr, "%s\n", (x == g_value) ? "yes" : "no");
// SIMPLE: Trying to solve
// SIMPLE: Found diverging input
// Make sure that we don't truncate integers.
// SIMPLE-DAG: #xaa
// SIMPLE-DAG: #xbb
// SIMPLE-DAG: #xcc
// SIMPLE-DAG: #xdd
// QSYM-COUNT-2: SMT
// ANY: no
SIMPLE-DAG: #xaa…#xdd 是对 simple 后端打到 stderr 的 SMT-LIB 表达式转储做 FileCheck——字面上在断言"Concat 没被截断"。qsym 后端下这个断言退化成 QSYM-COUNT-2: SMT。
代表性例子 2 —— 强制走 libc 包装器（test/libc_long_compare.c，完整）：
// REQUIRES: qsym
// RUN: %symcc -O0 -fno-builtin-strcmp %s -o %t
// RUN: rm -rf %t-out && mkdir %t-out
// RUN: %python -c "import subprocess; subprocess.run([r'%t'], input=b'A'*80, env={..., 'SYMCC_OUTPUT_DIR':r'%t-out', 'SYMCC_DATA_CMP_BYTES':'64'}, check=True)"
// RUN: %python -c "from pathlib import Path; assert any(p.is_file() for p in Path(r'%t-out').iterdir())"
int main(void) {
char input[81] = {0}; char expected[81];
memset(expected, 'A', 80); expected[80] = '\0';
if (read(STDIN_FILENO, input, 80) != 80) return 1;
return strcmp(input, expected) == 0 ? 0 : 2;
}
.ll 测试确实绕过前端：53 个里 28 个用 %opt + pass 插件，41 个走 %symcc，两组重叠 18 个——所以"完全不经 clang"的只有 10 个；走 %symcc 的那 41 个用的是 clang 的驱动，但 C 前端/parser 仍被绕过（clang 走 LLVM-IR 输入路径）；另有 2 个（live_continuation_*.ll）两者都不用。3 个上游测试额外加 RUN: llc %s -o /dev/null 兜底，因为 clang 对手写 IR 的校验比 codegen 松。
lit 里有没有 AFL？接口层有，campaign 层没有。 SYMCC_AFL_COVERAGE_MAP 出现在 38 个文件，test/test_afl_data_coverage.py:44 甚至自造了一个 unsigned char *__afl_area_ptr = map;（MAP_SIZE=65536）。但没有任何 lit 测试会启动 afl-fuzz。
┌──────────────── 正常编译（真实目标，benchmark）─────────────────┐
│ 源码 ──▶ symcc（公开目标常见 -O2）──▶ *_symcc ─┐ │
│ ──▶ afl-clang-fast -O2 ──▶ *_afl ─┼─▶ afl-fuzz + MPI worker │
│ ──▶ AFL_LLVM_CMPLOG=1 ──▶ *_cmplog ┘ 真实 AFL、真实位图 │
│ ──▶ gcc --coverage -O0 -g ──▶ *_cov 真实 showmap/gcov │
│ ⚠ 从不加 -fno-builtin ⇒ memcmp 常被内联掉 ⇒ 实际走【形态 A】 │
│ ⚠ 目标特定 hack：LAVA-M 的 unlocked-io.h 改写（否则 0 约束） │
└──────────────────────────────────────────────────────────────┘
┌──────────────── 自测试（test/ 176 个文件，lit）────────────────┐
│ .c ──▶ %symcc -O0/-O1/-O2 [-fno-builtin-strcmp] ──▶ 跑一次 │
│ │ │
│ ├─▶ 后端日志(stderr) ──▶ FileCheck（断言表达式转储） │
│ └─▶ %t-out/ 产出 + telemetry JSON ──▶ Python 断言 │
│ .ll ──▶ %opt -load-pass-plugin=%passlib -passes=… （28 个） │
│ └─▶ 其中纯 %opt 测试绕过 clang；其余仍可走 %symcc │
│ .py ──▶ python3 %s（48 个自包含 unittest） │
│ ⚠ 无 afl-fuzz campaign；部分测试会自造 map 或调用接口检查器 │
│ ⚠ 用 -fno-builtin 【强制】触发 libc 包装器 ⇒ 测的是形态 B │
└──────────────────────────────────────────────────────────────┘
⇒ 一句话：自测试验证【机制存在且正确】，benchmark 验证【机制在 -O2 真实目标上是否被触发】。
两者测的常常不是同一条路径——这是读测试结果时最容易误判的地方。
| 维度 | 真实目标 | 自测试 |
|---|---|---|
| 优化级别 | SymCC 微目标/公开目标 -O2；但 SymSan 公开目标是 -O1（scripts/build_public_symsan.sh:27,47,57,70，sqlite 还要 KO_DONT_OPTIMIZE 绕开 ko-clang 强制的 -O3）；gcov 覆盖率版是 -O0 -g |
RUN: %symcc 行里 -O0 占绝大多数（86 处）、-O2 20 处、-O1 6 处；.ll pass 测试 -O0 |
-fno-builtin* |
从不使用 | 4 个 .c 测试显式使用 |
| 后果 | memcmp/strcmp 常被内联/规范化掉 → §2.2 的包装器根本不触发 → 实际拿到的是 §2.1 的宽 icmp 路径 |
包装器被强制触发，测的是 pushMemoryEqualityConstraint 本身，而不是优化器的行为 |
| 输入来源 | 文件（SYMCC_INPUT_FILE / @@）或 AFL 持久模式共享内存 |
printf/echo -ne 喂 stdin |
| 源码 hack | unlocked-io.h 改写、glibc-2.28、O_SEARCH 补丁 |
无 |
| Fuzzer | 真 afl-fuzz，-M/-S、-c cmplog -l 2AT、-p <schedule>、MOpt |
无 |
| 断言对象 | showmap/gcov 覆盖增量、bug 数 | FileCheck 表达式转储 / IR 文本，或 Python 断言产出字节 + telemetry JSON |
SYMCC_FAST_SOLVE / SYMCC_MULTI_SOLVE |
默认 0，仅特定执行器 profile 打开 | 需要时在 RUN 行显式 =1 |
⚠ 潜在 bug：
test/lit.cfg:21把config.suffixes重新绑成list（lit 默认是set），而lit.site.cfg.in:49在其后调用config.suffixes.add(".test32")。list没有.add→TARGET_32BIT=ON时必然AttributeError，17 个.test32实际是死的。lit.cfg是本 fork 改过的（加了.py/%python），所以这是 fork 引入的回归。
-optimistic 标签的输出文件占 49%–84%；这不是生产任务占比，
也不是所有 Z3 check() 调用中乐观查询的固定比例。negatePath 的完整决策树¶入口：runtime/src/backends/qsym/Runtime.cpp:326-332 → Solver::addJcc（solver.cpp:1293）→ 经 isInterestingJcc（B3 过滤，见 §1.4）→ negatePath（solver.cpp:5441-5623）。
negatePath 决策树（默认配置走粗线）¶ 分支 e，具体走向 taken
│
┌────────────▼─────────────┐
│ isInterestingJcc(pc,taken)│ ← 读 B3（qsym_bitmap）
│ = trace_.isInteresting… │
└────────────┬─────────────┘
否 ─────────┴───────── 是
│ ║
不求解 ║ （基线下同时标记反方向；定向/S2F 可覆盖该门）
║
┌─────────────╨──────────────┐
│ ① query spool 导出/延迟 │ 默认关
├────────────────────────────┤
│ ② fastSolve → 命中即 return │ 默认关（SYMCC_FAST_SOLVE）
├────────────────────────────┤
│ ③-⑥ poly / unsat-core 缓存 │ 默认关；命中会【跳过乐观求解】
├────────────────────────────┤
│ ⑦ optimistic-first │ 默认关；开了则不 SAT 就直接放弃
╞════════════════════════════╡
║ ⑧ 严格求解（默认路径） ║
║ reset() ║
║ syncConstraints(e) ← 依赖切片，不是整条路径 ║
║ addToSolver(e, !taken) ║
║ check() [超时 10 s] ║
╘═════════════╤══════════════╝
│
SAT ───────────────────┼─────────────────── UNSAT 或 超时/unknown
║ ║
保存产出（无后缀） ┌────────────╨────────────┐
= nominal │ 表达式里含 Ite ? │
└────┬───────────────┬───┘
含 Ite 不含 Ite
║ ║
┌─────────────╨──────┐ ┌────────╨──────────┐
│ ⑨a tryBacksolve │ │ ⑨b 乐观求解 │
│ 只丢【与 ITE 控制变量│ │ reset() 丢【全部】 │
│ 共享字节】的前缀 │ │ 前缀，只留 ¬branch │
│ 只重验目标+保留前缀 │ │ check() │
│ → 后缀 -backsolve │ │ → 后缀 -optimistic│
└─────────────────────┘ └───────────────────┘
按求值顺序：
| # | 步骤 | 代码 | 默认（不设任何环境变量） |
|---|---|---|---|
| 1 | Query IR 导出 / 延迟求解 | 5455-5459 |
关（SYMCC_QUERY_SPOOL） |
| 2 | fastSolve 绕过 Z3 |
5462-5466 |
关（SYMCC_FAST_SOLVE） |
| 3 | poly-cache 键 + 线性约束 | 5468-5480 |
关（SYMCC_POLY_CACHE） |
| 4 | UNSAT-core 缓存查表 | 5482-5491 |
关（SYMCC_UNSAT_CORE_CACHE） |
| 5 | 线性矛盾包含剪枝 | 5492-5505 |
关 |
| 6 | poly-cache 回放 | 5507-5515 |
关 |
| 7 | 乐观优先查询 | 5535-5570 |
关（SYMCC_OPTIMISTIC_FIRST） |
| 8 | 严格（nominal）查询 | 5572-5588 |
开——这就是默认路径 |
| 9 | UNSAT/超时 → 乐观，或 → backsolve | 5606-5621 |
开 |
// solver.cpp:5572-5588
std::vector<size_t> strict_core;
z3::check_result strict_result;
if (unsat_core_cache_enabled_) {
strict_result = checkTrackedConstraints(unsat_constraints, strict_core);
} else {
reset();
syncConstraintsCached(e); // ← 加载"依赖切片"，不是整条路径
addToSolver(e, !taken); // ← 取反当前分支
strict_result = check();
}
bool sat = strict_result == z3::sat;
SAT → saveConcreteValues(values, "")，无后缀——所以 nominal 产出就是那些不带后缀的文件。
关键澄清：这里的"完整路径约束"不是整条路径。 它是 QSYM 的依赖切片：
syncConstraints（solver.cpp:4546-4581）沿DependencyForest只取与目标分支共享输入字节的那些约束。docs/Work_Progress_Report_3.md:82的权威表述：SymCC 求解的是什么：不是"从入口到执行点"的完整路径约束，而是通过依赖森林（DependencyForest）筛选出的与目标分支共享输入字节的所有约束。……这比加载全部路径约束高效，但当某个字节被大量分支共享时（如循环计数器），依赖树可以非常大，导致 Z3 收到大量约束而超时（默认 10 秒限制）。
// solver.cpp:5606-5621
if (strict_result == z3::unsat)
rememberUnsatCore(unsat_constraints, strict_core);
if (!sat && optimistic_first_enabled_ && optimistic_sat) {
if (!tryBacksolve(e, taken, &optimistic_values))
saveConcreteValues(optimistic_values, "optimistic-first");
} else if (!sat) {
if (!ite_target) {
reset(); // ← 丢掉【全部】前缀断言
// optimistic solving
addToSolver(e, !taken); // ← 只剩 ¬branch
checkAndSave("optimistic");
} else {
tryBacksolve(e, taken);
}
}
要点：
- reset() 把所有前缀断言丢光，只剩取反的当前分支。产出后缀 -optimistic；
- 触发条件是 !sat，同时覆盖 UNSAT 和超时/unknown；
- 如果分支表达式里含 Ite，根本不走乐观求解，改走 tryBacksolve（5617-5619）。SYMCC_BACKSOLVER 默认开（solver.cpp:418）；
- 第 4/5/6 步的缓存/剪枝命中会提前 return，完全跳过乐观求解——这是相对基线 QSYM 的行为差异，开缓存时要注意。
SYMCC_OPTIMISTIC_FIRST=1 会反过来：先跑乐观查询，若不 SAT 就直接放弃，连严格求解都不做（5555-5566）。
路径前缀约束集合（与目标分支共享输入字节的那些）： C1 C2 C3 C4 C5 + ¬branch
依赖切片 syncConstraints ── 在依赖追踪完整、非共享字节保持原值时语义等价
发给 Z3： C1 C2 C3 C4 C5 ∧ ¬branch ✅ 满足已加载切片
backsolve（默认开，仅 Ite 目标）── 只丢与 ITE 控制变量重叠的
发给 Z3： C1 ▓▓ C3 ▓▓ C5 ∧ ¬branch ⚠ 只重验目标与【保留】前缀
↑丢 ↑丢 validateBacksolveCandidate
乐观求解（默认开，作为回退）── 丢光
发给 Z3： ▓▓ ▓▓ ▓▓ ▓▓ ▓▓ ∧ ¬branch ⚠ 解可能根本走不到该分支
靠 afl-showmap 事后筛
✗ 不存在的策略： "保留最后 N 条，丢掉更早的"（窗口式）
| 机制 | 丢什么 | 代码 | 产出后缀 | 默认 |
|---|---|---|---|---|
依赖切片（syncConstraints） |
不加载与目标无共享字节的约束；仅在依赖追踪完整且这些字节保持当前具体值时语义等价 | solver.cpp:4546-4581；dependency.h:54-88 并查集 |
（nominal） | 开 |
| 乐观求解 | 丢全部前缀 | solver.cpp:5611-5616 |
-optimistic |
开（作为回退） |
backsolve（仅当分支表达式含 Ite） |
主要是具体搜索：按与当前赋值的汉明距离枚举 ITE 控制变量真值掩码（:5361-5381）、用 invertPredicate 改字节、具体验证后接受，全程不碰 Z3（上限 SYMCC_BACKSOLVER_CANDIDATES，默认 128）；只有全部失败才回落到 Z3，此时只丢与 ITE 控制变量共享字节的前缀（:5423-5438） |
solver.cpp:5318-5439 |
-backsolve |
开 |
| group-optimistic | 联合翻转多分支，先带前缀，UNSAT 再丢前缀 | solver.cpp:5967-5991 |
-group / -group-optimistic / -group-half |
关（SYMCC_MULTI_SOLVE） |
Z3 回落时的前缀取舍（solver.cpp:5328-5347，简化示意）：
std::vector<ExprRef> retained_constraints;
for (ExprRef constraint : collectPrefixConstraintExprs(e)) {
bool overlaps_controller = false;
DependencySet* dependencies = constraint->getDependencies();
...
if (overlaps_controller) {
backsolver_constraints_dropped_++;
} else {
retained_constraints.push_back(constraint);
backsolver_constraints_kept_++;
}
}
且求解后必须 validateBacksolveCandidate(...) 才写出（:5433-5435）。该函数只具体求值
目标谓词和 retained_constraints（:5155-5170），不会验证已经丢弃的重叠前缀；
因此它防止求解器/改写错误和保留前缀破坏，却不恢复完整路径可达性。最终仍要靠目标重放。
回归测试 test/backsolver_selective_prefix.ll:6 断言两个计数器都非零。
不存在"保留最后 N 条、丢掉其余"的窗口式策略。 依据是通读
negatePath（solver.cpp:5441-5623）、syncConstraints（:4546-4581）和collectPrefixConstraintExprs（:2516-2543）：前缀要么整取（依赖切片）、要么整丢（乐观）、要么按 ITE 依赖选择性丢（backsolve），没有任何按条数的窗口。
solver.cpp:52 const unsigned kSolverTimeout = 10000; // 10 seconds，solver.cpp:546-548 p.set(":timeout", kSolverTimeout)。solver.cpp:5937-5939）。SYMCC_SOLVER_TIMEOUT 这个变量不存在。 SYMCC_TIMEOUT（默认 30 s，mpi_fuzzing_helper.py:110）是每个输入的进程级执行超时，不是求解超时。unknown）（solver.cpp:1273-1277）：
cpp
last_check_timed_out_ = (res == z3::unknown) && (elapsed >= (uint64_t)kSolverTimeout * 900);solver.cpp:5517-5520，就在当年缓存所在的位置：
// 注意：不在此处做约束内容缓存。negatePath 的可满足性依赖于
// 已同步的路径前缀约束（syncConstraints），仅凭分支表达式做缓存
// 会因忽略路径上下文而误跳过可满足的约束、丢失覆盖率。分支级去重
// 已由上游 isInterestingJcc()/trace_.isInterestingBranch(pc,taken) 负责。
删除提交：39f4fa1（在嵌套子模块 runtime/src/backends/qsym/qsym 里，仓库根目录 git rev-parse 解析不到）。现存的缓存（UNSAT-core / prefix-context / poly，默认全关）都按完整 clause 集做键，并对回放的解重新验证。
solver.cpp:1566-1569：
std::string fname = out_dir_ + "/" + toString6digit(num_generated_);
// Add postfix to record where it is genereated
if (!postfix.empty()) fname = fname + "-" + postfix;
完整标签集：""(nominal) / -fast / -optimistic / -optimistic-first / -backsolve / -group / -group-optimistic / -group-half / -polycache / -polycache-cross-prefix / -poly（:4498，多解采样） / -dict。
注意 -optimistic 有两个产出点：negatePath 的回退（:5616）和值枚举路径（:1483），所以数 -optimistic 文件不等于纯粹的 negatePath 统计。
这正是本文能直接把策略占比数出来的原因。
仓库此前没有归档的生产数据。 telemetry 计数器（
solver.cpp:722-745，schema 3） 早就实现了，但没有留下能代表完整 campaign 的策略分布。以下是本文当场补测的 单种子、单次、短时机制实验，适合回答“代码实际走了哪些路径”，不适合回答 “生产运行中各策略的稳定占比”。复现（每个目标一次，各自的第一个种子，默认配置）：
bash SYMCC_OUTPUT_DIR=out SYMCC_INPUT_FILE=$SEED SYMCC_TELEMETRY_OUT=tel.json $SYMCC_BIN $SEED ls out | sed 's/^[0-9]*//; s/^-//' | sort | uniq -c # 策略占比
| 目标 | 种子 | 符号分支 | interesting | Z3 严格查询 | nominal 产出 | optimistic 产出 | optimistic 占比 | 求解耗时 |
|---|---|---|---|---|---|---|---|---|
| lava base64_harness | 5 B | 70 | 53 | 53 | 8 | 41 | 83.7 % | 29.1 ms |
| libarchive | 6 B | 34 | 22 | 22 | 8 | 14 | 63.6 % | 10.6 ms |
| pcre2 | 11 B | 475 | 133 | 133 | 52 | 79 | 60.3 % | 61.0 ms |
| gfts png | 69 B | 144 | 142 | 142 | 51 | 81 | 61.4 % | 194.8 ms |
| sqlite | 34 B | 63 | 45 | 45 | 14 | 31 | 68.9 % | 13.2 ms |
| gfts xml | 52 B | 240 | 225 | 225 | 114 | 111 | 49.3 % | 71.7 ms |
目标 nominal(严格SAT) ▓ + optimistic(丢前缀) ░ 合计 乐观占比
base64_h ▓▓░░░░░░░░ 8+ 41= 49 83.7%
sqlite ▓▓▓░░░░░░ 14+ 31= 45 68.9%
libarchive ▓▓░░░ 8+ 14= 22 63.6%
png ▓▓▓▓▓▓▓▓▓▓░░░░░░░░░░░░░░░░░ 51+ 81=132 61.4%
pcre2 ▓▓▓▓▓▓▓▓▓▓▓░░░░░░░░░░░░░░░░ 52+ 79=131 60.3%
xml ▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓░░░░░░░░░░░░░░░░░░░░░░ 114+111=225 49.3%
（条长按绝对产出数等比，可横向对比目标之间的产量差异）
两条对所有目标都成立的观察：
① z3_solves ≡ interesting_branches ——【严格求解永远先跑，一次不落】
② z3_timeouts = 0（6/6）——仅说明这 6 条单种子 trace 未遇到 Z3 超时
内部一致性自检（以 xml 为例）：solver_queries=336 = 225 严格 + 111 乐观；solver_sat=225 = 114 严格SAT + 111 乐观SAT；solver_unsat=111 = 严格 UNSAT 数 = 触发乐观的次数。
⚠ 但 xml 这条恒等式不普适——另外三个目标的 nominal+optimistic 小于 interesting：
| 目标 | interesting | nominal+optimistic | 缺口 | 解释 |
|---|---|---|---|---|
| base64_h | 53 | 49 | −4 | 这 4 条分支严格 UNSAT 后乐观也 UNSAT（恒真/恒假分支），两次查询都没产出 |
| pcre2 | 133 | 131 | −2 | 同上（变体行独立印证：214 = 133 严格 + 81 乐观，其中 79 SAT ⇒ 2 条乐观 UNSAT ✓） |
| png | 142 | 132 | −10 | 同上（FAST 行：230 = 139 + 91，81 SAT ⇒ 10 条乐观 UNSAT ✓） |
| libarchive / sqlite / xml | — | 相等 | 0 | 乐观全部 SAT |
所以准确说法是：solver_unsat = 严格 UNSAT + 乐观 UNSAT，只有当乐观全 SAT 时才等于"触发乐观的次数"。
另外：六个目标上 -backsolve、-poly、-fast（默认配置下）产出全部为 0。
SYMCC_BACKSOLVER 虽然默认开，但它只在分支表达式含 Ite 时才触发——这批目标一次都没触发。
因此在这套 benchmark 上，"丢前缀"实际就等于"乐观求解"，没有第三种情况。
默认配置没有 fast/poly/cache/optimistic-first，因而可以利用控制流关系反推：
strict_checks = z3_solves = interesting_branches
optimistic_checks = solver_queries - strict_checks
strict_sat_outputs = nominal 文件数
optimistic_outputs = optimistic 文件数
check 结果占比 = solver_{sat,unsat,unknown} / solver_queries
产出策略占比 = 对应后缀文件数 / generated
但在开启 fast solve、poly replay、unsat-core cache、optimistic-first 或 backsolver 后，
solver_queries 仍只记录所有 check() 的总数，z3_solves 则更接近进入主 Z3 路由的
分支数；当前 schema 没有 strict_checks、optimistic_checks、
optimistic_models_saved、optimistic_replay_success 四个独立计数器。因此：
fast_solves / (fast_solves + z3_solves)；solver_queries 计算；constraints_dropped / (constraints_kept + constraints_dropped)；check() 的生产占比目前不能从现有 telemetry 无歧义拆出。结论：
- 严格求解永远先跑——这是代码事实（乐观优先的门 :5535 默认关闭），不是这个计数推出来的。
实测里 z3_solves ≡ interesting_branches（53/53、22/22、133/133、142/142、45/45、225/225）能说明的是：没有任何一条分支走了缓存/剪枝的提前返回，也没有被 skip_solve 跳过（z3_solve_count_++ 在 :5521，位于乐观优先块之前，故它本身不区分先后）；
- 带 -optimistic 标签的文件占保存产出的 49%–84%。这说明该策略在六条 trace 的
保存事件中占比高，但文件可内容重复，也尚未经过 AFL 接受判定，不能称为 campaign 的
“主力覆盖来源”；
- z3_timeouts = 0，六个目标全部为 0。它只证明这六次单种子执行未遇到难查询；
长时间 campaign 会抵达不同路径和更大约束，不能据此断言“该 benchmark 的 Z3 不是瓶颈”。
| 目标 | 配置 | nominal | fast | optimistic | group-opt | Z3 查询 | 求解耗时 |
|---|---|---|---|---|---|---|---|
| xml | 默认 | 114 | — | 111 | — | 336 | 71.7 ms |
| xml | SYMCC_FAST_SOLVE=1 |
23 | 91 | 111 | — | 245 | 50.1 ms（−30 %） |
| xml | SYMCC_OPTIMISTIC_FIRST=1 |
114 | — | 111* | — | 450（+34 %） | 95.6 ms（+33 %） |
| xml | SYMCC_MULTI_SOLVE=1 |
114 | — | 111 | 0 | 336 | 77.0 ms |
| pcre2 | 默认 | 52 | — | 79 | — | 214 | 61.0 ms |
| pcre2 | SYMCC_FAST_SOLVE=1 |
38 | 14 | 79 | — | 200 | 61.9 ms |
| pcre2 | SYMCC_MULTI_SOLVE=1 |
52 | — | 79 | 1 | 216 | 63.5 ms |
| png | SYMCC_FAST_SOLVE=1 |
48 | 3 | 81 | — | 230 | 150.0 ms（−23 %） |
* -optimistic-first 后缀。
读法：
- SYMCC_FAST_SOLVE 在 xml 上很划算：91/225 = 40 % 的分支不用 Z3，Z3 查询 336→245，求解耗时 −30 %，产出数一个不少（225→225）。在 png/sqlite/base64 上几乎不触发（形状不匹配，见 §2.1）；
- SYMCC_OPTIMISTIC_FIRST 在这几个目标上是净亏：产出完全相同（225→225），查询数 +34 %、耗时 +33 %。原因显而易见——它先跑一次乐观查询，而这里绝大多数严格查询本来就 SAT，那次乐观查询纯属浪费。只有在严格查询大量 UNSAT/超时的目标上才值得开；
- SYMCC_MULTI_SOLVE 在这些目标上几乎不产出（pcre2/sqlite 各 +1）。它针对的是"源码里逐字节比较"的形状（见 §2.0），而这些目标的比较早被 -O2 合并成宽比较了。
副作用的机理：乐观解满足 ¬branch 但不满足前缀，具体重放时程序会走上另一条路，根本到不了那个分支，翻转没有兑现。每个这样的产出都要额外付一次目标执行 + 一次 afl-showmap 执行。
【论文】这是 QSYM 论文有意为之的取舍（Yun, Lee, Xu, Jang, Kim, QSYM: A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing, USENIX Security 2018）。原文 §1：
"Additionally, we alleviate the strict soundness requirements of conventional concolic executors … Such incompleteness or unsoundness of constraints is not a problem in a hybrid fuzzer where a co-running fuzzer can quickly validate the newly generated test cases; the fuzzer can quickly discard them if they are invalid."
§3.2 给出具体做法和两条理由：
"Q SYM strives to generate interesting new test cases from the generated constraints by optimistically selecting and solving some portion of the constraints, if not solvable as a whole. … In particular, Q SYM chooses the last constraint of a path for optimistic solving for the two following reasons. First, it typically has a very simple form, making it efficient for constraints solving. … Second, test cases generated from solving the last constraint likely explore the target path as they at least meet the local [constraint]."
以及为什么"不可满足也要解"：
"with the optimistic solving, even if the constraint is unsatisfiable, the solver will solve only the last constraint and generate a potential crash input, which helps fuzzer move forward…"
对上本代码库：solver.cpp:5611-5616 的 reset(); addToSolver(e, !taken); checkAndSave("optimistic") 正是"只留最后一条（取反的当前分支）"，与论文一致。
论文 Figure 12 还做过消融——在最后一条之外再加 1、2 条约束，结果"只用最后一条"找到的 bug 最多且耗时最少。
⇒ 所以判断乐观求解划不划算，唯一正确的口径是"它最终贡献了多少新边"，不是"它的解有多少条真的可达"。这也正是 §1.4 那套 showmap 过滤存在的理由。
系统的预期兜底：nominal / optimistic / fast / backsolve 的内容唯一候选应通过具体
afl-showmap 重放，只有新 feature 才保留（Rust 版 symcc_fuzzing_helper/src/main.rs:337-369；
MPI 版 mpi_fuzzing_helper.py:1207-1231）。但相同内容会在重放前去重，且 §1.5 已记录
batch crash/hang 候选没有 map 时会被丢失；所以“每一个产出都重放”并不准确。
但浪费多少？ 我按策略拆开量了每个产出的边贡献：
复现：benchmark/qa3_repro/landing2.py（对每个产出跑 afl-showmap 于 AFL 插桩二进制，减去种子边集）。
（重放本身有 ±1 条边的抖动：同一份语料复测得到 nominal 独有 85 而非 84，不影响任何结论。）
| 目标 | 策略 | 产出数 | 新边（并集） | 独有新边 | 边/产出 |
|---|---|---|---|---|---|
| xml（宽容文本格式） | nominal | 114 | 444 | 84 | 3.89 |
| optimistic | 111 | 457 | 97 | 4.12 | |
| png（严格二进制 + CRC） | nominal | 51 | 61 | 31 | 1.20 |
| optimistic | 81 | 41 | 11 | 0.51 |
xml（宽容文本格式） png（严格二进制 + CRC）
──────────────────── ─────────────────────
nominal 114 产出 → 独有新边 84 nominal 51 产出 → 独有新边 31
边/产出 3.89 ████████████ 边/产出 1.20 ████████████
optimistic 111 产出 → 独有新边 97 optimistic 81 产出 → 独有新边 11
边/产出 4.12 █████████████ 边/产出 0.51 █████
⇒ 乐观【比严格还高产】 ⇒ 乐观单产出价值低 2.4 倍
破坏前缀仍是合法 XML 变体 破坏前缀常被早期 CRC/魔数拒掉
两边都显示策略互补：png 的 optimistic 集合含 11 条 nominal 集合没有的 edge ID。
这不等价于端到端净收益，因为脚本没有计入求解、进程启动和完整 campaign 成本。
这是一个分目标的、诚实的答案：
landing2.py 只记录 edge ID 集合，固定
AFL_MAP_SIZE=65536，不比较 hit-count bucket，也没有计入求解、进程启动、内容去重、
master 排队和长期 AFL 反馈成本。生成 4 个只有嵌套深度不同的目标：第 i 层检查 b[i] == 'A'+i，第 i 层只有前 i-1 层全部成立才可达（短路嵌套）。用 build/symcc -O0 编，另用 afl-clang-fast 编一份量覆盖率。然后跑迭代式 concolic（产出喂回作为下一代种子），两种前沿策略对照：
fifo：朴素 FIFO，前沿超 64 就截断（没有覆盖率反馈）；cov：覆盖率制导——每个产出跑 afl-showmap，只保留带来新边的（这正是本框架 worker/master 两级位图做的事）。复现：benchmark/qa3_repro/iterate2.py(嵌套目标的生成命令见 benchmark/qa3_repro/README.md)。
| 深度 | 策略 | 结果 | 执行次数 | 产出 | Z3 查询 | 求解耗时 | 墙钟 |
|---|---|---|---|---|---|---|---|
| 16 | fifo |
前沿枯竭，止步深度 10/16 | 298 | 610 | 610 | 161 ms | 4.1 s |
| 16 | cov |
第 16 代解出 ✅ | 16 | 136 | 136 | 36 ms | 0.7 s |
| 32 | fifo |
前沿枯竭，止步深度 10/32 | 298 | 610 | 610 | 161 ms | 4.0 s |
| 32 | cov |
第 32 代解出 ✅ | 32 | 528 | 528 | 135 ms | 2.4 s |
（深度 16 与 32 的两行 fifo 数字完全相同不是笔误：两者都止步于深度 10，此前走过的分支结构一模一样，故执行数 / 查询数 / 耗时都一致。）
每代产出数的演化（fifo，深度 16 与 32 完全一样）：1 → 2 → 4 → 7 → 12 → 20 → 33 → 54 → 88 → 143 → 118 → 82 → 36 → 9 → 1 → 枯竭（合计 610，正是表中的产出数与 Z3 查询数）。
前沿本身受 nxt[:64] 截断：从第 9 代（候选 88 个）起就一直被削到 64，执行=298 就是各代前沿之和。
【无覆盖率反馈】前沿规模随代数演化（fifo，上限 64，深度 16 与 32 完全一样）
代 1 │▏1
2 │▎2
3 │▌4
4 │▉7
5 │██ 12
6 │███ 20
7 │█████ 33
8 │████████ 54
9 │██████████████ 88
10 │███████████████████████ 143 ← 指数膨胀，被上限 64 截断
11 │███████████████████ 118 唯一"前缀正确"的那个种子，
12 │█████████████ 82 在 142 个只差无关字节的兄弟里被挤掉
13 │█████ 36
14 │█ 9
15 │▏1 → 枯竭，止步深度 10
【有覆盖率反馈】cov 策略：前沿【恒为 1】，因为只有走到新一层的那个产出有新边
代 1 │▏1 2 │▏1 3 │▏1 … N │▏1 → 第 N 代恰好解出深度 N
┌──────┬──────────────────┬──────────┬──────┬─────────┬────────┐
│ 深度 │ 策略 │ 结果 │ 执行 │ Z3 查询 │ 墙钟 │
├──────┼──────────────────┼──────────┼──────┼─────────┼────────┤
│ 16 │ fifo（无位图） │ ✗ 卡在 10 │ 298 │ 610 │ 4.1 s │
│ 16 │ cov（位图制导） │ ✓ 第 16 代│ 16 │ 136 │ 0.7 s │
│ 32 │ fifo（无位图） │ ✗ 卡在 10 │ 298 │ 610 │ 4.0 s │
│ 32 │ cov（位图制导） │ ✓ 第 32 代│ 32 │ 528 │ 2.4 s │
└──────┴──────────────────┴──────────┴──────┴─────────┴────────┘
低效：深度 N ⇒ 恰好 N 代，严格串行，加 worker 也快不了；深度 32 时 528 个产出只有 32 个有用（94% 丢弃）。
脆弱：在取头 FIFO 对照中，整条链依赖位图识别"这个产出比兄弟多走了一层"。
没有这个信号，610 次 Z3 查询换不来一层进展。
注：深度 16 与 32 的两行 fifo 数字完全相同不是笔误——两者都止步于深度 10，
此前走过的分支结构一模一样，故执行数 / 查询数 / 耗时都一致。
1）"低效"是结构性的，有三重含义：
cov 策略下前沿恒为 1 个输入——严格串行的链条，无法靠加 worker 缩短。并行只能加宽"同一代里试多少种可能"，加不快"往下走多少层"；2）"脆弱"是字面意义上的——差一点就完全解不出：
fifo 跑了 298 次执行、610 次 Z3 查询，比 cov 多一个数量级，深度 16 和
32 都只到 10 就死了。这里严格证明的是脚本采用的生成顺序取头
nxt[:64] 策略会在该目标上丢失正确前缀，不是“任何有限截断”都会失败；nxt[:64] FIFO，不证明所有深层嵌套都必须依赖 bitmap；
⚠ 范围限定：本实验的 fifo 是取头截断（nxt[:64]，按生成顺序保留前 64 个，没有任何打分）。所以严格成立的结论是"取头截断的 FIFO 会把正确前缀挤掉"；nxt[-64:] 或随机截断未必同样失败。此外前沿最终枯竭（143→118→82→36→9→1→0）还有另一半原因：SHA-256 全局去重把 ≤10 层前缀的空间穷尽了。这两点不影响"有位图 vs 没位图"的对照结论，但不能推广成"任何截断都会失败"；fastSolve 必须重验前缀（solver.cpp:4939）、backsolve 必须重验保留前缀（:5433-5435）。当前 opt-in continuation/CAS 流可从 checkpoint 恢复状态，并在 lease 间保留增量求解上下文， 因此不必把每一层都简化为“新进程从入口重放”。该流仍有有界 state frontier、可行性查询和 状态爆炸问题，但它改变了本节 native N 代链的成本模型；两种执行流需要分别 benchmark。
3）代码层面还有几个放大因素：
| 因素 | 代码 | 后果 |
|---|---|---|
| 依赖森林合并 | dependency.h:70-83 |
两条约束只要共享一个字节就并成一棵树。循环计数器/长度字段/校验累加器会把整片森林塌成一棵——"切片"退化成"整条路径" |
Concat 链深度 ≈ N |
RuntimeCommon.cpp:150-160 |
N 字节符号读 ⇒ 深度 N 的右倾 Concat |
| ExprCache FIFO 淘汰 | expr_cache.h:9-14（kCacheSize = 65536，由 1024 提升而来，SYMCC_EXPR_CACHE_SIZE 可调） |
命中失败会把同一子表达式重建成不同指针，operator==（expr.h:234-252）退化成结构递归比较 |
kMaxDepth 是死常量 |
expr.h:23 定义，全仓库无任何引用 |
Expr::hash() / depth() / getDeps() / toZ3ExprRecursively 的递归没有任何深度上界——多 KB 的符号字段可以把栈冲爆 |
| Query IR 节点上限 65536 | solver.cpp:2630-2646 |
超限直接放弃导出（query_export_failures_++） |
| 反方向在 B3 中同时标记 | afl_trace_map.cpp:144-147 |
基线兴趣门会抑制后续同一 worker 的再次尝试；target/S2F 可强制覆盖，且不同 context 仍可能产生新颖性 |
docs/SymCC_Technical_Deep_Dive.md:156 的原话："两条约束共享一个输入字节就被合并到同一棵树。syncConstraints 加载整棵树——树很大时 Z3 收到大量约束导致超时。"
4）真实目标上的旁证：docs/symsan_ported_techniques.md:173-176 —— 嵌套微目标 deep_branches 在数千次 concolic 执行后也只到 27/64 条边（Z3 fgtest，2821 个输入）。docs/Work_Progress_Report.md:213 的判断："覆盖率不随并行度线性增长，根因是 SymCC 的单步约束翻转只能到达路径树的一步邻居。这不是并行框架的工程缺陷，而是 concolic execution 技术本身的理论边界。"
编译器把"具体走了哪边"和符号表达式一起传给运行时（compiler/Symbolizer.cpp:1582-1586）：
auto runtimeCall = buildRuntimeCall(IRB, runtime.pushPathConstraint,
{{I.getCondition(), true}, // 符号表达式
{I.getCondition(), false}, // ← 本次运行的真实 i1 取值
{getTargetPreferredInt(&I), false}});
运行时断言已走的方向、只对反方向查询一次（simple 后端最直观，runtime/src/backends/simple/Runtime.cpp:463-489）：
Z3_solver_push(g_context, g_solver);
Z3_solver_assert(g_context, g_solver, taken ? not_constraint : constraint);
Z3_lbool feasible = Z3_solver_check(g_context, g_solver);
Z3_solver_pop(g_context, g_solver, 1); // ← 反方向查询是 push/pop 的临时上下文
Z3_ast newConstraint = (taken ? constraint : not_constraint);
Z3_solver_assert(g_context, g_solver, newConstraint); // ← 已走方向被永久断言
● entry
╱ ╲
╱ ╲
┌──────● ○ ● = 本次具体执行走过的（种子决定）
│ ╱ ╲ ○ = 一步邻居：negatePath 能生成输入去够到
│ ╱ ╲ · = 更深的路径：本次执行【完全看不见】
│ ● ○
│ ╱ ╲
│ ╱ ╲ 一次 concolic 执行：
│● ○ • 只沿一条路径记录约束（path_hash_ 是标量，不是树）
│ ╲ • 对每个 interesting 分支解一次反方向
│ ╲ • 产出 = 种子的拷贝 + 模型钉住的那几个字节
│ ● ← 本次执行终点
│ ╱ ╲
│ · · ← 要够到这些，必须先把上面某个 ○ 变成新种子再跑一次
▼
⇒ 深度靠【外层反馈循环】一代一代堆，不是靠单次执行。
⇒ 种子选定了这条线，也就选定了这一整批一步邻居。
对经典 native concolic 流，目标运行时不 fork/快照，也没有进程内 worklist；
path_hash_（solver.cpp:1315）只是当前 trace 的标量摘要，多路径依赖外层候选反馈。
这句话不能推广到整个项目：§1.1.1 的 opt-in continuation/CAS 流确实保存状态 checkpoint、
维护 frontier，并可跨 lease 恢复。
产出是种子的变异（solver.cpp:1531-1548）：
std::vector<UINT8> values = inputs_; // ← 先拷贝种子
for (unsigned i = 0; i < num_constants; i++) {
if (idx >= 0 && (size_t)idx < values.size())
values[idx] = (UINT8)value; // ← 只覆盖模型钉住的字节
}
求解器没约束到的字节，原样保留种子的值。
字节偏移就是变量身份：_sym_make_symbolic（RuntimeCommon.cpp:462-469）按 input_offset++ 逐字节建 ReadExpr(offset)，Z3 编码是 context_.int_symbol(index_)（expr.h:508-535），取模型时再按整数符号反查偏移。
三条结构性后果：
read 返回几字节就符号化几字节。LibcWrappers.cpp:709-713：
cpp
auto result = getc(stream);
if (result == EOF) { _sym_set_return_expression(nullptr); return result; }
所以 while ((c = getc(f)) != EOF) 的循环次数是具体的，求解器永远不能靠翻转循环条件来加长/缩短文件。同理 read() 的返回值 n 是具体的，if (n < 8) 根本不是一个符号分支。util/pure_concolic_execution.sh:15
表述为保持输入长度：
Note that SymCC never changes the length of the input, so be sure that the initial inputs cover all required input lengths.本 fork 的实际输出还取决于 wrapper 如何填充inputs_：有的路径保留整个 seed，有的路径 只序列化已读取窗口并截掉尾部（§4.6）。共同点是求解器无法创造尚未读取/符号化的新字节。
这里的“输入”是已被运行时识别并符号化的字节通道。当前文档和 benchmark 主要覆盖
stdin/文件描述符与 SYMCC_INPUT_FILE；命令行参数、环境变量、网络报文、多文件关系、
时钟/随机数和外部持久状态若未显式建模，仍是具体环境。即使文件 seed 相同，这些通道不同
也会选择不同路径，这也是 DSE 效果依赖 harness 和执行环境的原因。
focus_bytes 会进一步收窄（runtime/src/backends/qsym/Runtime.cpp:401-412）：
SymExpr _sym_get_input_byte(size_t offset, uint8_t value) {
initFocusBytes();
g_enhanced_solver->pushInputByte(offset, value);
// 连续范围模式：范围外具体化
if (g_focus_enabled && (offset < g_focus_start || offset > g_focus_end))
return nullptr;
...
return registerExpression(g_expr_builder->createRead(offset));
}
范围外的字节永远具体，只依赖它的分支对引擎完全不可见。
⚠ SymSan 侧的一个坑（已修，值得记）：DFSan 的 flag parser 把
,当分隔符，focus_bytes=0-3,8-11会让运行时Die()——docs/symsan_ported_techniques.md:81-83："目标当场死掉、一条输出都没有，且不报错，看起来就像'这个目标解不动'"。为此加了三层防御。
目标：4 字节魔数 SYMC → 长度检查 n >= 8 + 长度字段 buf[4]==3 → 校验和 buf[5]+buf[6]+buf[7]==0x42。
8 字节种子 AAAAAAAA——第 6 代解出：
gen 0 input=4141414141414141 AAAAAAAA 过 0 关 -> STAGE1a: bad magic[0] [2 行 SMT 日志 = 1 次查询]
gen 1 input=5341414141414141 SAAAAAAA 过 1 关 -> STAGE1b: bad magic[1] [4 行 SMT 日志 = 2 次查询]
gen 2 input=5359414141414141 SYAAAAAA 过 2 关 -> STAGE1c: bad magic[2] [6 行 SMT 日志 = 3 次查询]
gen 3 input=53594d4141414141 SYMAAAAA 过 3 关 -> STAGE1d: bad magic[3] [8 行 SMT 日志 = 4 次查询]
gen 4 input=53594d4341414141 SYMCAAAA 过 4 关 -> STAGE2b: bad len field [10 行 SMT 日志 = 5 次查询]
gen 5 input=53594d4303414141 SYMC.AAA 过 5 关 -> STAGE3: bad checksum [12 行 SMT 日志 = 6 次查询]
gen 6 input=53594d4303000042 SYMC...B 过 6 关 -> *** 命中深层代码 ***
字节演进：AAAAAAAA → SAAAAAAA → SYAAAAAA → SYMAAAAA → SYMCAAAA → SYMC\x03AAA → SYMC\x03\x00\x00B。
（口径说明：日志里每次 check() 会打两行 [STAT] SMT:（solver.cpp:1248 与 :1278），所以"日志行 2,4,6,…,12"对应 1,2,3,…,6 次 Z3 查询，与 §4.5 中同一种子的 6 个产出一致。）
注意 gen 5→6：3 字节算术校验和被一次 Z3 查询解出（00 00 42）。也注意查询数 1,2,3,4,5,6 逐代 +1——每加深一层，整条前缀都被重走一遍、且多解一个新分支（呼应 §3.5）。
4 字节种子 AAAA——同一个二进制，永远解不出：
gen 0 41414141 AAAA 过 0 关 -> STAGE1a: bad magic[0] [2 行 SMT 日志 = 1 次查询]
gen 1 53414141 SAAA 过 1 关 -> STAGE1b: bad magic[1] [4 行 SMT 日志 = 2 次查询]
gen 2 53594141 SYAA 过 2 关 -> STAGE1c: bad magic[2] [6 行 SMT 日志 = 3 次查询]
gen 3 53594d41 SYMA 过 3 关 -> STAGE1d: bad magic[3] [8 行 SMT 日志 = 4 次查询]
gen 4 53594d43 SYMC 过 4 关 -> STAGE2: input too short (n=4)
[8 次求解 —— 没有增加!]
候选: ac594d43 / 53a64d43 / 5359b243 / 53594dbc 全都退步
-> 不动点，卡死
决定性细节：gen 4 的 Z3 查询数停在 4，不是 5。 if (n < 8) 这个检查一次查询都没贡献——因为 n 是 read() 的具体返回值，那个分支根本不是符号分支，无法被翻转。
不是"解不出长度检查"，而是对 4 字节种子来说这个检查不存在。
目标：magic "SYMC" → 长度 n>=8 且 buf[4]==3 → buf[5]+buf[6]+buf[7]==0x42
8 字节种子 AAAAAAAA 4 字节种子 AAAA
──────────────────── ─────────────
gen0 41414141 41414141 过0关 gen0 41414141 过0关
gen1 53414141 41414141 过1关 S gen1 53414141 过1关 S
gen2 53594141 41414141 过2关 SY gen2 53594141 过2关 SY
gen3 53594d41 41414141 过3关 SYM gen3 53594d41 过3关 SYM
gen4 53594d43 41414141 过4关 SYMC gen4 53594d43 过4关 SYMC
gen5 53594d43 03414141 过5关（长度字段） │ └─▶ "input too short (n=4)"
gen6 53594d43 03000042 ✅ 命中深层代码 │ 查询数停在 4，【没有增加】
│ ⇒ if(n<8) 一次查询都没贡献
Z3 查询: 1,2,3,4,5,6 │ 因为 n 是 read() 的具体返回值
（每加深一层，整条前缀重走一遍） └─▶ ✗ 不动点，31 次执行 / 112 次求解，永不命中
⇒ 不是"解不出长度检查"，而是【对 4 字节种子这个检查根本不是符号分支】。
⇒ 求解器不能创造未建模的新字节；本 fork 可能保留整份 seed，也可能截掉未读尾部。
跑到不动点的完整战报：
| 种子 | concolic 执行次数 | 求解调用 | 唯一输入 | 最深到达 | 墙钟 |
|---|---|---|---|---|---|
4 字节 AAAA |
31 | 112 | 30 | STAGE2: input too short — 永不命中 |
1.37 s |
8 字节 AAAAAAAA |
127 | 492 | 126 | 命中深层代码 | 5.45 s |
空种子则完全惰性：input_bytes=0, symbolic_branches=0, z3_solves=0, generated=0。
开 SYMCC_QUERY_SPOOL（solver.cpp:563-566，导出在 :2808-2810）。以 SYMC\x03AAA 为种子跑一次，导出 6 条查询。
第一条（魔数字节 0），原文：
--- prefix_smt2 (已累积的路径条件) ---
(set-info :status unknown)
(check-sat)
--- target_smt2 (被取反的那个分支) ---
(set-info :status unknown)
(declare-fun k!00 () (_ BitVec 8))
(assert (not (= k!00 (_ bv83 8))))
(check-sat)
k!00 是输入字节 0，bv83 = 'S'。导出格式本身就把 prefix_smt2（已走路径前缀）和 target_smt2（单个取反分支）分开——"一条路径 + 一次翻转"的结构是字面写在文件里的。
最后一条（校验和），原文：
(set-info :status unknown)
(declare-fun k!60 () (_ BitVec 8))
(declare-fun k!50 () (_ BitVec 8))
(declare-fun k!70 () (_ BitVec 8))
(assert (= k!70 (bvadd (_ bv66 8) (bvmul (_ bv255 8) k!50) (bvmul (_ bv255 8) k!60))))
(check-sat)
即 8 位算术下的 buf[7] == 66 - buf[5] - buf[6]，正是 buf[5]+buf[6]+buf[7] == 0x42。变量 k!50/k!60/k!70 = 输入偏移 5/6/7 —— "偏移就是变量"的编码在这里一目了然。
注意这里 prefix 是空的：QSYM 的依赖切片只取与目标共享变量的约束，魔数约束落在偏移 0–4，与 5–7 不相交（呼应 §3.1）。
Query IR 节点（schema: symcc-query-ir-v1），"op": "read" 直接带着输入偏移：
node[1] = {"id":1,"op":"read","bits":8,"children":[],"attrs":{"index":7}}
node[3] = {"id":3,"op":"read","bits":8,"children":[],"attrs":{"index":5}}
node[5] = {"id":5,"op":"read","bits":8,"children":[],"attrs":{"index":6}}
node[7] = {"id":7,"op":"add","bits":32,"children":[4,6],"attrs":{}}
node[9] = {"id":9,"op":"extract","bits":8,"children":[8],"attrs":{"index":0}}
metadata: {"site":10324000135319577099,"branch":0,"desired":false,"dependencies":[5,6,7]}
focus_bytes 的效果：范围外的分支直接消失¶同一个 8 字节种子 SYMC\x03AAA，只改 SYMCC_FOCUS_BYTES：
| 配置 | 产出数 | 产出 |
|---|---|---|
| 无限制（8 字节全符号） | 6 | ac594d43… 53a64d43… 5359b243… 53594dbc… 53594d43fc… 53594d4303000042 |
SYMCC_FOCUS_BYTES=0-3 |
4 | 只有魔数 4 个字节的变体 |
SYMCC_FOCUS_BYTES=5-7 |
1 | 只有 53594d4303000042（校验和解） |
SYMCC_FOCUS_BYTES=0-1 |
2 | 只有 ac594d43… 53a64d43… |
种子文件（8 字节） SYMCC_FOCUS_BYTES=0-3 时
┌──┬──┬──┬──┬──┬──┬──┬──┐
│53│59│4d│43│03│41│41│41│
└──┴──┴──┴──┴──┴──┴──┴──┘
0 1 2 3 4 5 6 7 ← 偏移【就是】Z3 变量身份（k!00 … k!70）
▲ ▲ ▲ ▲ ▲ ▲ ▲ ▲
│ │ │ │ │ │ │ │
符号符号符号符号 │ │ │ │ ← _sym_get_input_byte 返回 ReadExpr(offset)
具体具体具体具体 ← 返回 nullptr，分支【结构性不可见】
实测产出数： 无限制 6 个 │ focus 0-3 → 4 个 │ focus 5-7 → 1 个 │ focus 0-1 → 2 个
⚠ pushInputByte 在门控【之前】执行 ⇒ 去焦不会截短输出。
⚠ SymSan 侧 focus_bytes 只支持单区间；写成 "0-3,8-11" 会让 DFSan 运行时 Die() 且【不报错】，
看起来就像"这个目标解不动"。
范围外字节上的分支不产生查询、不产生输出——结构性不可见，与 Runtime.cpp:401-412 完全吻合。
【B级】但要注意，聚焦并不总是加速（
docs/Research_and_Optimization_Report.md:436-445）：小种子（<200 B）上全符号化 vs 聚焦 = 7.9 s/1354 边 vs 8.0 s/1361 边，0.99×，无加速；12 KB 合成大稀疏输入（1 % 相关）上聚焦反而 0.02× 更慢——因为具体化会改变哪些分支是符号的，非单调地改变探索路径。
| 种子 | 程序读取 | 产出长度 |
|---|---|---|
| 24 字节 | 前 8 字节 | 24 字节（尾部原样保留） |
| 64 字节 | 缓冲区 32 字节 | 32 字节（尾部被丢弃） |
24 字节输入保留尾部，说明“未参与当前约束”不等于“必然删除”；64→32 则说明运行时
inputs_ 只覆盖当前识别/读取的输入窗口时，模型序列化不会凭空补回窗口外尾部。
因此应区分原始 seed 文件长度、目标实际读取长度、运行时 inputs_ 长度和
最终写出的 values 长度，不能用一句“只截不加”概括所有 wrapper/harness。
策略全在 AflConfig.best_new_testcases（mpi_fuzzing_helper.py:514-617）。静态分（:563-576）：
if "+cov" in name: static_score += 100.0
if "+rare" in name: static_score += 60.0
if "symcc_" in name: static_score += 20.0
if fsize > 50*1024: static_score -= 40.0
elif fsize > 10240: static_score -= min(30.0, (fsize-10240)/1024.0)
elif fsize < 256: static_score += 10.0
static_score += min(50.0, math.log1p(afl_id) * 5.0)
动态分叠加 edge_yield（3 类种子的 Beta-Bernoulli Thompson 采样，:2732-2764）和 frontier（K-Scheduler 前沿分，权重 40，:605）；最后 heapq.nlargest 取前 max_active_workers * 4 个（:611-616, :3344）。
K-Scheduler 前沿分（opt-in SYMCC_KSCHED=1，开关在 :3156，打分在 :3162-3188；也可由组件选择器 component_choices["seed"]=="frontier" 激活，:3349-3352）：
score = 0.0
for e, b in enumerate(data):
if b:
f = _edge_freq.get(e, 0)
score += 1.0 / (f + 1) # 稀有边贡献大（前沿）
_edge_freq[e] = f + 1
即 rarity = Σ_{e∈edges(seed)} 1/(freq(e)+1)，用"边命中频率"作为 K-Scheduler 图中心性的 CFG-free 代理。每轮 showmap 预算 16 次（:3159），按内容 SHA-256 缓存。
注意：种子从不被裁剪/最小化。 选择路径里没有 afl-tmin/afl-cmin，也没有任何 minimizer。默认是整份种子发给一个 worker（:381-384）；只有在多样性模式且种子数少于目标工作项数时，_build_work_items（:358-420）才把同一个文件切成 min(focus_parts, …) 份、各自负责不相交的 focus_bytes 区间。
benchmark/benchmark_results_v2/benchmark_data.csv 对照磁盘上的种子数：
| 目标 | 磁盘种子数 | 仅种子覆盖 | MPI 最佳覆盖 | MPI 产出数 |
|---|---|---|---|---|
| lava-md5sum | 1 | 7.14 % | 7.14 % | 0 |
| lava-uniq | 1 | 9.54 % | 9.54 % | 0 |
| lava-who | 1 | 6.73 % | 6.73 % | 8 |
| freetype2 | 2 | 2.22 % | 2.26 % | 689 |
| pcre2 | 8 | 7.16 % | 18.66 % | 140,206 |
| gfts-png | 11 | 10.35 % | 14.94 % | 23,174 |
| lava-base64 | 13 | 11.58 % | 23.25 % | 107,994 |
| libarchive | 13 | 6.45 % | 13.90 % | 75,851 |
| gfts-xml | 20 | 3.08 % | 5.74 % | 36,145 |
| sqlite | 25 | 13.70 % | 14.97 % | 31,747 |
单种子目标的 concolic 增益恰好为零，≥8 种子的目标都有明显增益。
⚠ 诚实说明：这个相关性是混淆的。 仓库把单种子目标的零增益归因于"平坦二进制目标随机翻转即可覆盖、无需约束求解"（
docs/Final_Work_Report.md:414；"目标太浅"那个说法出自docs/SymCC_MPI_Parallel_Effectiveness_Analysis.md:219，且是针对 PNG/XML 而非 LAVA-M）；而后续工作证明 uniq 的零其实是两个 bug（taint_getc丢标签 + 构建时KO_USE_FASTGEN丢失），修完后 0 → 92 个 concolic 产出（docs/symsan_ported_techniques.md:257-277）。"种子少"和"目标浅"这两个因素，仓库里没有任何实验把它们分离开。
更干净的一条种子多样性 A/B（docs/Work_Progress_Report.md:149）：字典引导在 1 个种子时 +50 %（1,802→2,710 边），在 25 个种子时 +0 %（4,832→4,835）。
注意两个基线本身：1,802 vs 4,832 边——同一个目标上 2.7 倍的种子质量效应。原结论（:151）："字典引导是种子多样性的替代品，而非额外提升"。（精确值是 +50.4 % 和 +0.06 %，后者只多 3 条边。）
另一个提醒：配置错误看起来和种子问题一模一样。 lava base64 的 afl-only 基线因为漏了 -d 参数，覆盖率从 23.90 % 掉到 7.81 %（docs/PPT_Material_Supplement.md:169 打 †、:171 给脚注。注意 :23 那行是 hybrid np=8，所以"afl-only 基线掉到 7.81 %"是推断而非直读；另有两份历史文档记的是 7.44 %）。排查"这个目标解不动"时，先查命令行。
base64 程序的约束求解轨迹¶前面的 SYMC 微目标用于隔离机制；这里再用真实的 SymCC 插桩目标
benchmark/public/bin/lava-m/base64 -d <seed> 核验一次。复现脚本：
benchmark/qa3_repro/trace_base64.sh。
关键环境变量如下：
SYMCC_OUTPUT_DIR=out \
SYMCC_INPUT_FILE="$seed" \
SYMCC_AFL_COVERAGE_MAP=qsym_bitmap \
SYMCC_TELEMETRY_OUT=telemetry.json \
SYMCC_DATA_COVERAGE=1 \
benchmark/public/bin/lava-m/base64 -d "$seed"
SYMCC_INPUT_FILE 不是装饰项：若目标通过文件路径读输入但没有设置它，运行时不知道哪个
文件描述符属于符号输入，实测会得到 input_bytes=0、零符号分支、零产出。
| 种子 | 长度 | 退出码 | 符号分支 | interesting | Z3 check() |
SAT/UNSAT | 产出（严格/乐观） | 内容唯一 |
|---|---|---|---|---|---|---|---|---|
rand.b64 |
175 B | 0 | 773 | 233 | 412 | 230/182 | 230（54/176） | 134 |
utmp-fuzzed-100.b64 |
4096 B | 1 | 179 | 101 | 200 | 101/99 | 101（2/99） | 45 |
第一组的 z3_solves=233 等于 interesting 分支数；solver_queries=412 则等于
233 次严格查询再加 179 次乐观回退。总求解耗时约 109 ms、无 unknown/timeout，
只能说明这条 trace 没有 Z3 超时；本次脚本没有把进程执行、重放和筛选完整分相位，
不能据此给出端到端成本排名。
同一个目标换成 4096 字节种子后，程序沿另一条解码/错误退出路径执行： 符号分支从 773 降到 179，严格产出从 54 降到 2，相关输入字节也从 67 降到 8。 这不是“长种子一定更差”，而是种子具体值决定路径，种子长度决定符号变量上界； 两者共同决定本次执行能看见哪些分支和约束。
还有一个容易误读的现象：rand.b64 生成 230 个文件，但 SHA-256 内容只有 134 种，
即 96 个是内容重复。比如最早的一对 nominal/optimistic 文件会对同一 4 字节产生
相同修改。运行时的 generated 因而只能表示求解器保存次数，不能替代 worker 的
内容哈希去重，更不能替代 AFL showmap 的覆盖新颖性判断。这正好闭合了 Q1 的三层漏斗：
求解器保存次数 230
-> 内容唯一候选 134
-> AFL showmap 新 bit 候选（由 hybrid worker/master 再筛）
异常退出还会截断观测：专项扫描中另一个种子以信号结束，只留下少量候选且没有
atexit telemetry；超时种子也没有完整 telemetry。因此真实调试必须同时保留退出码、
stderr、输出目录和 telemetry，不能只看 generated 一个数字。
§4.4 给出了合成目标的一条完整 SMT；§4.9 对真实 base64 目前只有聚合 telemetry， 尚未把某个真实分支从现场一直追到 AFL 结果。科研复现应为至少一个真实 branch 保存以下链：
site_id + parent/path/open_branch_hash
→ prefix_smt2 + target_smt2（或 Query IR 内容哈希）
→ strict/optimistic/backsolve 路由与 check 结果
→ 模型修改的输入 offset/value
→ 候选内容哈希
→ concrete replay 是否重新到达该 site/方向
→ showmap edge + hit-count bucket delta
→ worker B2 / master B1 / AFL virgin-state 的最终保留结论
在这条证据链完成前，本文可以回答“真实程序产生了多少分支/查询/文件”，但不能声称已经 展示了真实 base64 的 branch-by-branch 求解过程。crash/timeout 还必须保存未经过滤候选， 否则会受到 §1.5 crash-only 缺陷影响。
CoFuzz —— Ling Jiang, Hengchen Yuan, Mingyuan Wu, Lingming Zhang, Yuqun Zhang. "Evaluating and Improving Hybrid Fuzzing", ICSE 2023. DOI
10.1109/ICSE48619.2023.00045（南方科技大学 + UIUC；代码 https://github.com/Tricker-z/CoFuzz）
仓库内引用位置：docs/sota_hybrid_execution_2026.md:48；docs/Research_and_Optimization_Report.md:185（小节标题）与 :509（参考文献第 1 条）；代码注释 util/mpi_fuzzing_helper.py:523 和 :2732。全仓库对 cofuzz|cohuzz 共 7 处命中（上列 5 处 + Research_and_Optimization_Report.md:32 + docs/README.md:33）。
排除项：仓库根目录三个 PDF 都不是它——enfuzz.pdf = EnFuzz（PDF 本身只有 arXiv:1807.00182v2 戳，无会议信息；USENIX Sec'19 这个出处来自 µFUZZ 的参考文献）、pafl.pdf = PAFL（ESEC/FSE'18）、ufuzz.pdf = µFUZZ（仓库里那份是匿名投稿版；正式发表为 Yongheng Chen, Rui Zhong, Yupeng Yang, Hong Hu, Dinghao Wu, Wenke Lee, "µFUZZ: Redesign of Parallel Fuzzing using Microservice Architecture", USENIX Security 2023, pp. 1325–1342，代码 https://github.com/s3team/muFuzz）。仓库另引的 ICSE'23 论文是 GenSym，与评估无关。
⚠ 本节的证据来源要分清： §5.2–§5.3 的内容来自论文原文（本次为写文档专门取回并逐条核对），不在本仓库里——仓库只记了两句头条结论。 §5.4 起才是本项目自己的数据。两者不要混引。
这篇论文的定位是对已有 hybrid fuzzer 做统一设置下的再评估，并提出 CoFuzz。它不是 逐个重建并忠实复现每篇原论文的全部 artifact：作者尽可能复用公开源码/运行时，对无法直接 运行的 DigFuzz、Pangolin 等组件进行重新实现或适配。因此本节应称“统一再评估”，而不是 “已有方案的忠实复现”。摘要里的问题意识说得很直白：
"While the existing hybrid fuzzers have shown their superiority over conventional coverage-guided fuzzers, they seldom follow equivalent evaluation setups, e.g., benchmarks and seed corpora."
| 类别 | 系统 | 说明 |
|---|---|---|
| 7 个 hybrid fuzzer | QSYM（基线）、Angora、Eclipser、Intriguer | 各自设计了 concolic executor |
| DigFuzz、MEUZZ、Pangolin | 改进的是协调模式（调度 / 同步） | |
| 3 个传统 CGF 对照 | AFL、FairFuzz、AFL++ | — |
关键的公平性处理（等 CPU）：所有 hybrid fuzzer 都是"1 核跑 fuzzing 策略 + 1 核跑 concolic"，所以论文把传统 CGF 一律实现成双实例版本（同一个 fuzzer 起两个实例、周期性互相同步种子）再来比。这正是本项目后来自己补做的那种等 CPU 对照（§5.4.2）。
| 维度 | 设置 |
|---|---|
| 真实程序 | 15 个：readelf / nm / objdump / strip（binutils-2.37）、tcpdump、libxml2 2.9.12、libjpeg v9c、jhead、libpng 1.7.0、libtiff 4.2.0、file、bento、wavpack、cyclonedds、libming |
| 注入 bug 基准 | LAVA-M（base64 / md5sum / uniq / who，coreutils-8.24） |
| 种子 | JPEG/PNG/TIFF 用 AFL 官方种子集，其余用项目自带；afl-cmin 去重；所有实验共用同一份种子集 |
| 时长 × 重复 | 真实程序 24 小时 × 5 次重复取平均；LAVA-M 5 小时 |
| 指标 | 边覆盖、unique crashes；LAVA-M 上是 bug 数 N + bug 存活时间 Tm（分钟）；另有"冗余边比例"这个自创指标 |
| 统计检验 | Mann-Whitney U 单尾检验，显著性水平 0.01 / 0.05 |
| 硬件 | AMD EPYC ROME 7H12 @2.6 GHz，256 GiB RAM，Ubuntu 18.04 |
15 个程序的平均边覆盖（Table III，24 h × 5 轮），以 AFL 为 0 基准画增幅：
0% +5% +10% +15%
├─────┼─────┼─────┤
H QSYM 5,763 +13.87% ████████████████████████████████████ ← 2018 年的基线
H Pangolin 5,561 +9.88% ██████████████████████████
H Angora 5,517 +9.01% ███████████████████████
H MEUZZ 5,422 +7.13% ███████████████████
H Eclipser 5,323 +5.18% █████████████
H DigFuzz 5,321 +5.14% █████████████
H Intriguer 5,254 +3.81% ██████████ ← 最差的 hybrid
─────────────────────────────────────────────────────────────
C AFL++ 5,180 +2.35% ██████ ← 最好的传统 CGF，只差 1.46pp
C FairFuzz 5,171 +2.17% ██████
C AFL 5,061 +0.00%
H = hybrid fuzzer C = 传统 CGF（双实例版本，等 CPU）
2018 年的 QSYM 平均最高，且在 15 个程序里 7 个夺冠；DigFuzz、MEUZZ、Pangolin 分别比它低 7.67 % / 5.92 % / 3.51 %——三个明确宣称改进 QSYM 协调模式的工作，在统一设置下都没打过它。
原论文自称 vs 本研究复现：
| 系统 | 原论文声称比 QSYM 高 | 本研究实测 |
|---|---|---|
| Intriguer | +12.42 % | QSYM 高 3.75 % |
| MEUZZ | +6.60 % | QSYM 高 9.99 % |
| Pangolin | +21.90 % | QSYM 高 0.17 % |
同一个程序 readelf 上，QSYM 的边覆盖在 Intriguer / MEUZZ / Pangolin 原论文和本研究里分别是 6,012 / 1,244 / 8,402 / 9,512——差了近 8 倍。论文推断原因是硬件平台和初始种子集不同。
Finding 1：hybrid fuzzer 原论文之间的边覆盖对比结果，不一定能推广到其他实验设置。
等 CPU（双实例 CGF）下，最差的 hybrid（Intriguer 5,254）也只是略高于最好的传统 CGF（AFL++ 5,180）。
| 系统 | 原论文声称比 AFL 高 | 本研究实测 |
|---|---|---|
| Angora | +27.08 % | +9.01 % |
| Eclipser | +25.15 % | +5.18 % |
而且 AFL 在 15 个程序里有 4 个胜过 Intriguer、3 个胜过 MEUZZ。
unique crash 上更难看（Table IV，10 个程序有 crash，合计）：
H QSYM 147 ████████████████████████████████████████ ← 唯一有明显优势的 hybrid
H Angora 129 ███████████████████████████████████
C AFL++ 128 ██████████████████████████████████▉
H Pangolin 127 ██████████████████████████████████▋
H MEUZZ 123 █████████████████████████████████▌
H Intriguer 119 ████████████████████████████████▌
C FairFuzz 116 ███████████████████████████████▋
C AFL 109 █████████████████████████████▊
H Eclipser 107 █████████████████████████████ ← 比 AFL 还少
H DigFuzz 105 ████████████████████████████▋ ← 比 AFL 还少
Finding 2：hybrid 相对传统 CGF 的边覆盖优势相当有限，说明 concolic 的能力没有被充分释放。 Finding 4：大多数 hybrid 在真实程序上暴露 unique crash 方面，相对传统 CGF 优势有限甚至没有。
论文把 3 个 fuzzing strategy × 4 个 concolic executor 重新排列组合：QSYM-ce 配 AFL / FairFuzz / AFL++ 得到 5,763 / 5,830 / 5,842 条边——最大差距只有 79 条边。
Finding 3：单独更换 fuzzing strategy 或 concolic executor，对边覆盖的影响很有限。
论文定义"冗余边比例" = fuzzing 策略和 concolic 执行器重复探索到的同一批边的占比。实测 0.47（jhead）到 0.95（libjpeg）；libjpeg 上除 QSYM（0.80）外全部 >0.95。
而且冗余边比例和性能高度相关：QSYM 覆盖最高（5,763）且冗余最低（0.65）；Eclipser / Intriguer 覆盖最低（5,323 / 5,254）且冗余最高（0.92 / 0.91）。
原因论文说得很清楚：fuzzing 策略和 concolic 执行器的覆盖状态是互相不可见的，只能周期性同步，中间存在"覆盖更新间隙"，于是 concolic 大量算力花在 fuzzer 早就覆盖了的边上。
Finding 5：hybrid 的有效性由冗余边比例反映，而它由协调模式决定。 Finding 6：DigFuzz / MEUZZ 的种子级调度没能降低冗余（0.87 / 0.71 vs QSYM 0.65）。 Finding 7：Pangolin 的同步机制改进对边覆盖影响也有限。
论文由此给出的处方：必须做 edge-oriented（边级）而不是 seed-oriented（种子级）的调度。
在完全相同的设置下，CoFuzz（QSYM + 边级在线线性回归调度 + 采样增强同步）：
Table VI，5 小时预算，N = 发现的 bug 数，Tm = bug 存活时间（分钟，越小越快）：
| Fuzzer | base64 N / Tm | md5sum N / Tm | uniq N / Tm | who N / Tm |
|---|---|---|---|---|
| QSYM | 44/44 / 8.48 | 57/57 / 31.77 | 28/28 / 4.55 | 1332/2136 / 300 |
| Angora | 48/44 / 6.75 | 57/57 / 16.37 | 29/28 / 7.15 | 1547/2136 / 300 |
| Eclipser | 46/44 / 128.33 | 57/57 / 147.35 | 29/28 / 155.83 | 1030/2136 / 300 |
| Intriguer | 46/44 / 205.07 | 57/57 / 132.60 | 29/28 / 187.22 | 1350/2136 / 300 |
| DigFuzz | 46/44 / 7.53 | 57/57 / 57.30 | 28/28 / 4.32 | 1146/2136 / 300 |
| MEUZZ | 44/44 / 7.28 | 57/57 / 40.35 | 28/28 / 6.50 | 1205/2136 / 300 |
| Pangolin | 48/44 / 9.37 | 57/57 / 132.75 | 29/28 / 13.27 | 1342/2136 / 300 |
| CoFuzz | 48/44 / 1.07 | 57/57 / 1.75 | 29/28 / 0.50 | 1913/2136 / 300 |
读法（很重要）：
- 在该论文的 5 h protocol 下，base64 / md5sum / uniq 上 7 个 hybrid fuzzer 都覆盖了
validated endpoint（部分还报出列表外 ID），所以这三项主要区分 Tm，不是最终 endpoint。
- 只有 who 还有区分度，而且没有任何一个能在 5 小时内拿满（CoFuzz 1913/2136 最多）。
- 速度差距巨大：CoFuzz 1.07 分钟 vs 第二快的 Angora 6.75 分钟 vs Eclipser 128 分钟。
- 本项目也有一次 /tmp 历史语料在 103 秒预算后重放出 44/44（§6.5），但它与
论文的种子、硬件、CPU 预算、运行方式、重复次数和 Tm 口径均不同，不能据此排序
或声称优于 QSYM/接近 CoFuzz；最多说明 base64 endpoint 很容易在 concolic 路径上饱和。
本项目没有把任何实验命名为"复现 CoFuzz"，但它独立地撞上了同一批问题——有对上的，也有走反的。
util/mpi_fuzzing_helper.py:523 的 docstring 写着 增强种子调度策略（受 CoFuzz ICSE'23 启发），:2732 写着 # 边产出率在线学习（CoFuzz + T-Scheduler 风格）：。但实际实现（:2735-2765）是对 3 类种子（cov / symcc / normal）做 Beta-Bernoulli Thompson 采样，先验 Beta(1,1)。
对照论文：
| CoFuzz 论文 | 本项目实现 | |
|---|---|---|
| 调度粒度 | 边级（edge-oriented） | 种子级（seed-oriented，且只有 3 个类别） |
| 模型 | 在线线性回归（SGD 增量学习），5 个边特征 | Beta-Bernoulli Thompson 采样 |
| 论文对该方向的结论 | 这是它的核心贡献 | Finding 6 明确说：种子级调度降不下冗余边 |
也就是说，本项目照搬的是"在线学习调度"这个形式，但保留了论文诊断为病根的种子级粒度。而且这个调度器从未做过 A/B 验证（docs/ 和 benchmark/ 里找不到它的消融实验）。仓库自己也声明了 -style 标签只表示改编而非忠实复现（docs/sota_hybrid_execution_2026.md:11）。
这是一个应当写进待办的真实差距：论文的处方是让 concolic 面向低效/未覆盖边， 而本项目当前主路径仍是选择种子后沿 trace 尝试多个 interesting 分支。§1.6 当前短测 有 132/299 个 worker 上报在 master 被拒，§5.4.3 的历史实验中 14 worker 有效率降至 18.6%；它们都提示跨执行冗余，但统计定义与论文 0.47–0.95 的“冗余边比例”不同， 不能直接称为同一个指标。
顺带一提：SYMCC_TARGET_BRANCH + telemetry 的 target_reached / target_status 已经把"只解某一条指定分支"的机制做出来了（solver.cpp:714-716，util/hybrid_feedback.py:631-648），差的是把它接到一个边级的效用模型上。
docs/PPT_Material.md:245：
Hybrid 使用的 CPU 核数多于 AFL-only。覆盖率差异中包含 CPU 资源差异的影响——Hybrid 的提升不能完全归功于 SymCC。缺少"多 AFL 实例"的等 CPU 对照组。
核数账（docs/PPT_Material_Complete.md:432-436）：AFL-only = 1 核；Hybrid np=8 = 8 核（1 AFL + 1 MPI master + 6 SymCC worker）。
可靠性说明（:459）：
所有数据为单轮运行（rounds=1），未计算标准差。AFL-only 基线在 6 次独立实验中的 ShowmapCov 标准差：libarchive ±0.23pp，SQLite ±0.63pp。差异 <1pp 的结论应视为初步观察。
被这条削弱的头条结论（:825）：Hybrid 互补性成立 | 10 目标 ShowmapCov 均 ≥ AFL-only——那是 1 核 AFL 对 8 核 hybrid 测出来的。
docs/Research_and_Optimization_Report.md:304-364，三之补 — 并行核心分配实验。
设置（:310）：np=16，timeout=240s，rounds=3，两个代表性目标，扫 AFL 实例数 ∈ {1,4,8,12}，总核数恒为 16，afl-showmap 量并集语料的边覆盖。这就是等 CPU 下的 N×AFL vs SymCC-heavy 对照。
| AFL 实例 | SymCC worker | sqlite | libarchive |
|---|---|---|---|
| 1（旧默认） | 14 | 19.30 % | 23.30 % |
| 4 | 11 | 21.39 % | 23.79 % |
| 8（新默认） | 7 | 22.82 % | 23.92 %（峰值） |
| 12 | 3 | 22.87 % | 21.60 % |
增幅（:326-329）：sqlite 19.30 → 22.82 (+18.2 %)，libarchive 23.30 → 23.92 (+2.7 %)，xml 9.11 → 9.47 (+3.9 %)。
扩展到 np=64、rounds=2、每个配置独占整机（:333-341）：
| 策略 | sqlite | libarchive |
|---|---|---|
| 1 AFL + 63 SymCC（旧默认） | 21.02 % | 23.98 % |
| 均分 32 AFL + 31 SymCC | 24.49 % | 22.88 %（−4.6 % ✗） |
| 封顶 51 AFL + 12 SymCC | 23.12 %（+9.9 %） | 23.95 %（−0.1 % ✓） |
np=16 恒定总核数，扫 AFL 实例数（rounds=3, 240 s）
sqlite libarchive
1 AFL + 14 SymCC (旧默认) 19.30% ████████████████ 23.30% ██████████████████████
4 AFL + 11 SymCC 21.39% █████████████████▌ 23.79% ██████████████████████▌
8 AFL + 7 SymCC (新默认) 22.82% ██████████████████▌23.92% ██████████████████████▊ ← 峰值
12 AFL + 3 SymCC 22.87% ██████████████████▌21.60% ████████████████████▌
np=64 独占整机（rounds=2）
1 AFL + 63 SymCC 21.02% 23.98%
32 AFL + 31 SymCC (均分) 24.49% ▲最高 22.88% ▼-4.6% ← 均分反而伤 libarchive
51 AFL + 12 SymCC (封顶) 23.12% +9.9% 23.95% -0.1% ← 落地为默认
⇒ 把 94% 的核给 concolic 是【严格亏损】。SYMCC_WORKER_CAP = 12。
已作为默认落地：benchmark/run_benchmark.py:82 SYMCC_WORKER_CAP = 12；分配逻辑 :3835。
这一段对设计文档的意义：项目自己的等 CPU 扫描发现，把 ~94 % 的核给 concolic 是严格的亏损，最优点是把 concolic 封顶在 ~12 个 worker、其余全给 AFL。这是一个仓库内部、独立得出的旁证，支持"朴素 hybrid 的优势里有很大一部分是 CPU 预算不公平的假象"。
并行 concolic 的冗余是结构性的（:365-395，同一个 AFL 队列，各 ~95 s）：
| SymCC worker 数 | 产出 TC | interesting | 有效率 |
|---|---|---|---|
| 6 | 1055 | 317 | 30.0 % |
| 14 | 2549 | 474 | 18.6 % |
:375-377：14 worker 时 ~81% 的 concolic 计算浪费在已覆盖边上；哈希去重的重复率为 0 → 冗余是语义层面的，不是重复输出。（本文 §1.6 的漏斗实测与此一致。）
:382-390）：有效率 关 18.0 % vs 开 17.9 %（n=2 噪声内），已回退；:396-420）：np=64，2 轮，sqlite 23.12±0.10 vs 22.97±0.48；libarchive 23.95±2.31 vs 23.61±0.54。保留为 opt-in，默认关；:421+）；:130）：再加引擎的边际增益仅 +5.8% branches / +0.68% bugs（EnFuzz-Q vs QSYM）；:54-58）：GRIMOIRE 式无语法结构重组，sqlite 4339 → 4628 边（+6.7 %），原文称 是所有尝试中唯一实质提升覆盖率的技术。docs/symsan_hybrid_benchmark_6targets.md：6 个真实目标，3 轮 × 20 s，--np-list 8 = 3 AFL 实例 + 2 concolic worker，afl-showmap -C。
| 目标 | AFL 用例 | concolic interesting（均值） | 区间 | 边 | 边% |
|---|---|---|---|---|---|
| base64 | 442 | 28 | 23–33 | 97/192 | 50.5 % |
| uniq | 261 | 8 | 8–8 | 134/1216 | 11.0 % |
| xml | 10681 | 89 | 0–139 | 5019/50880 | 9.9 % |
| png | 832 | 37 | 24–44 | 665/3072 | 21.7 % |
| pcre2 | 23743 | 118 | 99–144 | 4520/9728 | 46.5 % |
| sqlite | 5040 | 86 | 83–89 | 6480/31552 | 20.5 % |
方法学自白（:32-33）：
单轮方差真实。xml 三轮是 139 / 128 / 0（有一轮 concolic worker 20s 内超时未贡献）；均值抹平、范围列显示区间。这正是要跑 3 轮的原因。
benchmark/research_protocol.py:1233-1238：调度校验会拒绝不等 CPU 预算——raise ValueError("schedule does not preserve equal CPU budgets")，通过后返回 "equal_cpu_budget": True（:1261）。配对随机区组（pair_id + 共享 random_seed，:1243-1250）、规范序、摘要封存、强制 git 溯源；benchmark/research_protocol.py:27：MIN_CONFIRMATORY_REPEATS = 20——确认性协议少于 20 次重复直接报 "underpowered confirmatory protocol"；benchmark/analyze_ablation.py：bootstrap_ci / paired_bootstrap_ci（默认 5000 次重采样）、vargha_delaney（A12 效应量）、randomization_p_value（符号翻转）、holm_adjust；docs/Recent_Work_and_Next_Research_Plan.md:397）。落地的是 bootstrap + 符号翻转 + A12/Cliff + Holm；docs/Development_History_Traceability.md:75）：| R | 等 CPU、多轮、置信区间、效应量和逐项消融 |；docs/Recent_Work_and_Next_Research_Plan.md:479-483）：固定 equal CPU budget：1、4、8、16、32 workers；30min、2h、6h 三档；每组至少 20 次随机重复。论文怎么测的：7 个 hybrid fuzzer（QSYM/Angora/Eclipser/Intriguer/DigFuzz/MEUZZ/Pangolin）+ 3 个传统 CGF（跑双实例版本以保证等 CPU），15 个真实程序 + LAVA-M，统一种子集（afl-cmin 去重），24 h × 5 轮取平均，边覆盖 + unique crash + bug 存活时间 + 自创的"冗余边比例"，Mann-Whitney U 单尾检验。
结果如何（对 hybrid fuzzing 相当不客气）：
本项目和它的关系：
0/44 → 39/44；覆盖率层面最有效的杠杆反而是 GRIMOIRE 结构合成（sqlite +6.7 %），不是求解器。微目标：benchmark/run_benchmark.py:63-68 的 TARGETS 只声明 4 个——maze（16 B，指数分支）、parser（32 B，嵌套条件）、deep_branches（8 B，深依赖链）、crypto_check（16 B，逐字节比较）。另有 benchmark/targets/parallel_scaling.c（64 个 MODULE()，id 0–63）只有源码、没有接进 runner（grep -n parallel_scaling benchmark/run_benchmark.py 零命中）。
真实目标（benchmark/public/bin/，版本取自 benchmark/public/gfts_build/）：
| 目标 | 库 / 版本 | 格式 | 驱动 | 种子数 |
|---|---|---|---|---|
gfts-png_read_fuzzer |
libpng 1.2.56 | PNG | compile_public_benchmarks.sh:309-391 内联 harness |
11 |
gfts-xml_read_fuzzer |
libxml2 2.9.2 | XML | :468-545 |
20 |
pcre2-pcre2_fuzzer |
pcre2 10.00 | 正则 | targets/pcre2_harness.c |
8 |
sqlite-sqlite_fuzzer |
sqlite 2016-11-14 | SQL | targets/sqlite_harness.c → sqlite3_exec on :memory: |
25 |
libarchive-archive_fuzzer |
libarchive v3.3.2 | 归档 | targets/libarchive_harness.c |
13 |
freetype2-freetype2_fuzzer |
freetype2（git a6d4860） |
字体 | targets/freetype2_harness.c |
2 |
lava-base64 / _harness |
coreutils 8.24 LAVA-M | base64 | base64 -d @@ |
13 |
lava-md5sum / uniq / who |
coreutils 8.24 LAVA-M | — | md5sum -c / uniq / who |
各 1 |
声明了但从没下载的套件：setup_public_benchmarks.sh:505 的用法行是 --all | --lava-m | --unibench | --symcc-paper | --google-fts | --fuzzbench | --magma（只有 UniBench 在脚本里写明是 20 个程序；FuzzBench/Magma 没写数量）。CGC cb-multios（243 个）在另一个脚本 compile_public_benchmarks.sh:6,32 的 --cgc。实际下载到 benchmark/public/ 的只有 fuzzer-test-suite/ 和 lava_corpus/（该目录另有 bin/、gfts_build/、seeds/ 三个构建产物目录）。tcpdump 和 openjpeg（SymCC 论文的目标）从未构建。
运行配置：默认 --np-list 1,2,4,8 --rounds 3 --timeout 60；归档实验实际用 120 s 或 300 s、rounds=1。主指标是 afl-showmap -C 边覆盖（run_benchmark.py:753-900），lcov/gcov 是次要路径。cmplog 默认开（-c <bin> -l 2AT）。
⚠ 一个容易踩的语义陷阱：
hybrid模式下generated = AFL 队列数 + SymCC 产出数（run_benchmark.py:2583），afl-only下只是 AFL 队列（:2798），mpi下只是 SymCC 产出。hybrid 的generated不是 concolic 产出数。
并行符号执行和并行 fuzzing 的状态单位不同，不能放在同一张“同类系统”表里。前者分发 execution state/path condition，后者并发运行 fuzzer 实例并交换 seed/corpus。
| 系统 | 并行单位 / 目标 | 评估目标 | 关键规模结论 |
|---|---|---|---|
| Cloud9（EuroSys 2011） | KLEE state；中心调度 + worker 间状态迁移 | memcached、Apache httpd、lighttpd、Python、rsync、curl 等真实系统 |
重点证明集群级 state-level symbolic execution 能扩展到服务器和系统程序；与本项目 native seed replay 的执行单位不同 |
| GenSym（ICSE 2023） | 编译成 CPS/continuation 后并行展开路径 | 6 个有限路径算法目标；Coreutils 8.32 的 base32、base64、cat、comm、fold、echo、dirname、expand、paste、cut、join、link、true、pathchk |
4/8/12 线程启用 solver 优化时平均加速 2.08/2.83/3.10×；关闭该优化为 3.63/6.74/9.36×，显示求解器共享/串行成本会限制扩展 |
Cloud9 的目标强调复杂系统与状态迁移；GenSym 的目标强调 continuation 编译和可枚举路径 的并行扩展。当前项目的 continuation/CAS 流在执行单位上更接近 GenSym，但 lowering 覆盖、 内存模型和正式 scaling 证据仍需单独比较，不能因为有 checkpoint 就宣称复现了 GenSym。
| EnFuzz（arXiv:1807.00182v2；据 µFUZZ 参考文献为 USENIX Sec'19） | PAFL（ESEC/FSE'18, pp. 809–814） | µFUZZ（仓库内为匿名投稿版；正式发表 USENIX Sec'23, pp. 1325–1342） | |
|---|---|---|---|
| 套件 | LAVA-M(4) + Google fuzzer-test-suite(24) + 真实项目(15)，共 43 | Google FTS(12) + GitHub(9 有 CVE) | Magma(6)：Poppler / SQLite / openssl / sndfile / libxml2 / PHP |
| 时长 | 24 h | 24 h | 24 h |
| 重复 | 10（FTS）；LAVA-M 未说明 | 10 | 5 |
| 核数 | 1（单）/ 4（并行） | 4 | 40 |
| 基线 | AFL, AFLFast, FairFuzz, libFuzzer, Radamsa, QSYM | AFL, AFLFast, FairFuzz | AFL++, AFLEdge, AFLTeam + 2 消融 |
| 用 LAVA-M 吗 | 用 | 不用（全文 0 次 "LAVA"） | 不用 |
| 指标 | 路径 / 分支 / 唯一 bug | 分支 / 唯一 crash | Magma bug ID + 存活时间（time-to-bug） |
µFUZZ 在引言里说 "including Magma and FuzzBench"，但全文只有引言和参考文献两处提到 FuzzBench，没有任何 FuzzBench 结果表（摘要里并未出现）。
三篇并行 fuzzing 论文各自记录了单机优化在并行下退化的现象：EnFuzz 说 AFLFast/FairFuzz 在 4 核并行下只找到 AFL 的 73.5 %/88.2 % 的 bug；PAFL 说它们只覆盖 AFL 的 97 %/96 % 分支、触发 57 %/89 % 的 crash；µFUZZ 说 QuickJS 上 10 实例 × 1 h 只有 1 实例 × 10 h 的 49 % 路径。这与本项目“增加 worker 后边际收益 下降”的方向一致，但机制不同：它们主要研究 corpus 同步/负载，本项目还叠加了求解冗余。
本仓库从未这样说过。 我对 docs/、benchmark/、README.md 做了 LAVA × {easy, weak, simple, saturat, 简单, 饱和, 局限} 的组合搜索，零命中。仓库的定位反而是正面的（docs/Parallel_Architecture_Report.md:227）："LAVA-M：学术界标准的 bug 注入基准集，可验证 bug 发现能力"。
但文献和现有短测都提示：部分目标在特定 protocol 下对 concolic 的 endpoint 区分度有限：
"The base code of the four applications in LAVA-M are small (2K-4K LOCs) and concolic execution could work well on them. However, real projects have code bases that easily reach 10k LOCs. Concolic execution might perform worse or even get hanged." "While LAVA-M is widely used, Google's fuzzer-test-suite is more practical with many more code lines and containing real-world bugs." 它的小节标题就是 "Preliminary Evaluation on LAVA-M"。
who 还有区分度，且没有一个能在 5 小时内拿满；"Despite its success, LAVA-M is nowadays considered flawed because it artificially injects vulnerabilities into a given target program that are easy for a fuzzer to find but do not correspond to real bugs. More recent works using LAVA-M often do so only for comparability reasons."
同一节还说 CGC "is widely considered outdated and inadequate"，并把结论压成一句："Benchmarks with artificial vulnerabilities are still used."（言下之意：不该再用）。 - 2018 年后的两篇并行 fuzzing 论文（PAFL、µFUZZ）干脆不用 LAVA-M，µFUZZ 改用 Magma + 存活时间分析； - 本项目实测：纯 concolic MPI 在 np=32 时 103 秒拿满 44/44（见 §6.5）。
结论应限定为：在 CoFuzz 的 5 h 设置和本项目的 base64 历史短测中，
base64/md5sum/uniq endpoint 对多种 hybrid/concolic 系统区分度低；who 仍未饱和。
“纯 fuzzer 依然很难”也只由特定 AFL 配置和短预算支持，不能推广到所有 CGF。LAVA-M
适合做通路回归和历史可比性检查，不足以单独支撑真实缺陷发现能力或系统排名。
仓库里唯一的"饱和"措辞是针对自己的 PNG/XML 目标（
docs/SymCC_MPI_Parallel_Effectiveness_Analysis.md:219）："目标太浅：PNG/XML 的 harness 仅调用极少 API，可达路径邻域在 5 分钟内即饱和"。
工具是 scratch_lava_bugcount.py（提交 106cdf2），不是 benchmark 主流程。方法：
benchmark/public/bin/lava-m-cov/<prog>，按 LAVA 规范的选项（base64 -d / md5sum -c / uniq / who），超时 5 s；Successfully triggered bug (\d+)（:36）。LAVA 用 dprintf(1,...) 绕过 stdio 缓冲，所以这行在随后的 SIGSEGV 中仍能幸存；SEGV 退出码被显式忽略（:159）；set（:191）——记的是不同 bug ID 数，不是 crash 次数；validated_bugs 求交，输出两个数：distinct（全部 ID）和 listed hits（∩ validated，即 LAVA 论文口径）。validated_bugs 行数：base64 44、md5sum 57、uniq 28、who 2136。
⚠ benchmark 主流程根本不记 bug 数。 当前
benchmark_results*/benchmark_data.csv共 19 个文件、379 行数据，crashes列无一非零——因为run_benchmark.py:897把"crashes": 0写死了（afl-showmap -C不报 crash）。所有 LAVA-M bug 数都来自 上面的离线重放脚本。
工具自校验（用 LAVA 自带的 ground-truth 触发输入）：base64 44/44 ✅ 完全吻合；md5sum 55/57；uniq 14/28（LAVA 自带 inputs/ 本身只到 14，这是个天花板，引用 uniq 数据时必须说明）；who 1492/2136。用种子语料跑，四个程序全部 0 bug。
当前已提交的 benchmark/benchmark_results_lava/benchmark_data.csv 是 120 s、单轮数据。
它证明并行/混合执行提升了生成吞吐和边覆盖，但其 crashes 全为 0，不能证明 bug 数：
| 模式 | np | generated | unique | tc/s | 边覆盖 | edges |
|---|---|---|---|---|---|---|
| serial | 1 | 0 | 0 | 0.0 | 11.21 % | 122/1088 |
| MPI | 2 | 12,474 | 7,076 | 121.1 | 21.69 % | 236/1088 |
| MPI | 16 | 128,077 | 60,371 | 1,241.1 | 21.88 % | 238/1088 |
| hybrid | 2 | 265 | 265 | 2.19 | 21.51 % | 234/1088 |
| hybrid | 16 | 1,282 | 1,282 | 10.58 | 23.90 % | 260/1088 |
| AFL-only | 1 | 85 | 85 | 0.71 | 7.81 % | 85/1088 |
这些行支持两个有限结论：MPI 把候选生成吞吐扩到 1,241 tc/s；hybrid 虽然保留的输入少， 但覆盖更高，说明 coverage triage 有效。它们不是等 CPU、多轮确认性实验，也没有 LAVA bug ID，所以不能从表中写出“发现了多少漏洞”或 time-to-bug。
提交 106cdf2："Used to measure the afl-only vs hybrid injected-bug counts (base64: 0 -> 39/44)." 底层是 scratchpad 里的 lava_fix.sh + lava_fix.out（2026-07-19，未提交仓库）：
scratchpad/lava_bugs.sh 以 T=240 秒生成；lava_fix.sh 本身不跑 AFL，只消费这份现成语料）/tmp 运行目录重放出的证据¶以下数据可用于解释机制和形成待验证假设，但原始运行目录不在当前仓库内， 不能与 §6.5.0 的已提交 CSV 合并成同一组正式实验。
| 运行 | 配置 | 墙钟 | 语料 | distinct | listed |
|---|---|---|---|---|---|
bench_lava-base64_mpi8_r0_* |
纯 MPI，1 master + 7 worker | 103 s | 4,415 | 43 | 42 / 44 |
bench_lava-base64_mpi32_r0_* |
纯 MPI，31 worker | 103 s | 40,847 | 47 | 44 / 44 |
bench_lava-base64_mpi32_r0_*（第二次） |
同上 | 103 s | 28,588 | 47 | 44 / 44 |
bench_lava-base64_hybrid8_r0_* |
hybrid np=8：4 AFL + 3 SymCC | ~18 s | 707 | 32 | 29 / 44 |
hybrid np=8 的分目录拆解（最有信息量的一片）：
| 子语料 | 文件数 | listed hits |
|---|---|---|
symcc_all_outputs（SymCC 原始产出） |
117 | 26 / 44 |
afl_out/fuzzer02/queue |
89 | 0 / 44 |
afl_out/fuzzer03/queue |
90 | 0 / 44 |
afl_out/fuzzer04/queue |
101 | 1 / 44 |
afl_out/fuzzer04/crashes |
53 | 28 / 44 |
afl_out/fuzzer01/queue（含 helper 直注的 id:symcc_* 文件） |
167 | 26 / 44 |
afl_out/fuzzer03/crashes |
19 | 10 / 44 |
| 全量并集（真实输入文件，不含 extras/.synced/统计文件） | 707 | 29 / 44 |
fuzzer02/03 的队列各为 0，而 fuzzer01 目录中的 helper 直注文件重放得到 26/44，这提示 对应内容来自 SymCC 解；但 §1.10 的受控实验表明运行中的 AFL 不会重扫自己的 queue， 所以这些文件存在于目录不等于已经进入 AFL 内部 corpus。本文也没有做逐 bug-ID/ 内容哈希来源追踪，不能称为 AFL “已 sync” 或闭环生效。
listed bugs / 44 墙钟 ≈CPU·秒
AFL-only，8 实例 0 ░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░ 240 s ~1,920
└ 注：这是 240 s 预算下的 0；QSYM 论文里 AFL 在其预算下拿到 7/44（见"横向校准"）
Hybrid np=8 29 ██████████████████████████░░░░░░░░░░░░░░ 18 s ~144
纯 concolic MPI np=8 42 ██████████████████████████████████████░░ 104 s ~832
纯 concolic MPI np=32 44 ████████████████████████████████████████ 105 s ~3,360 ✅满分
⚠ 四行来自不同历史运行，CPU·秒差 20 倍以上；墙钟是预算，不是 time-to-bug。
只能作为 endpoint 机制观察，不能计算速度提升、显著性或系统排名。
hybrid np=8 拆解：SymCC 原始产出 117 个文件 → 26/44
fuzzer02/03 队列(未 sync) → 0/44
fuzzer01 目录(helper 直注文件) → 26/44 ← 提示内容源自 SymCC
（未做逐 ID 溯源，属一致观察）
机制假设：部分 LAVA 守卫含精确 4 字节比较，适合位向量约束求解；
但实际到达守卫还受前缀、污点传播、harness 和构建配置影响。
⚠ 不可外推：EnFuzz 自述 LAVA-M 只有 2K–4K 行、是 concolic 的舒适区；
同一套方法在 Google FTS(80K–220K 行) 上只找到 60 个 bug（AFL 34）。
⚠ 覆盖率维度上 LAVA-M 早已饱和：base64 边覆盖从 np=8 到 np=190 恒为 23.25%。
| 配置 | 墙钟 | ≈CPU·秒 | base64 listed bugs |
|---|---|---|---|
| AFL-only，8 实例 | 240 s | ~1,920 | 0 / 44 |
| Hybrid np=8（4 AFL + 1 master + 3 SymCC） | ~18 s | ~144 | 29 / 44 |
| 纯 concolic MPI np=8 | 104 s | ~832 | 42 / 44 |
| 纯 concolic MPI np=32 | 105 s | ~3,360 | 44 / 44（满分） |
⚠ 这不是等 CPU、同语料、同机器或多轮对照；"18 s / 103 s"是 campaign 预算， 不是各 bug 的首次触发时间。AFL 0/44 与 concolic 42/44 是有价值的机制观察，但无法 量化"快多少倍"，也不能证明差异不会由配置、种子或运行产物选择造成。
① 【论文】QSYM 自己的 LAVA-M 表（Table 6，USENIX Security 2018；括号内为占官方 bug 总数的比例）：
| 系统 | uniq /28 | base64 /44 | md5sum /57 | who /2136 |
|---|---|---|---|---|
| FUZZER（AFL） | 7 (25 %) | 7 (16 %) | 2 (4 %) | 0 (0 %) |
| SES | 0 (0 %) | 9 (21 %) | 0 (0 %) | 18 (39 %)† |
| VUzzer（论文值） | 27 (96 %) | 17 (39 %) | 0 (0 %) | 50 (2 %) |
| QSYM | 28 (100 %) | 44 (100 %) | 57 (100 %) | 1,238 (58 %) |
† 原表如此（SES 的 who 一列计数与百分比不自洽），属论文原文，非本文转录错误。
⚠ 这条修正本文上面的口径。 实测的"AFL-only 8 实例 240 s → 0/44"是那个预算下的结果， 不能读成"AFL 永远找不到 LAVA-M 的 bug"——QSYM 论文里 AFL 拿到 base64 7/44、uniq 7/28。 正确表述是：在秒级到分钟级预算内，随机变异命中
lava_get(N)==0x6c617564这类精确 4 字节魔数的概率在 2⁻³² 量级， 而约束求解一次即得——这是速度的量级差，不是"能与不能"的绝对差。
② 三个来源在 base64 上高度一致（都拿满 44/44），这反过来说明该目标已无区分度：
| 来源 | 系统 | base64 |
|---|---|---|
| 【论文】QSYM (USENIX'18) Table 6 | QSYM | 44/44 |
| 【论文】CoFuzz (ICSE'23) Table VI | QSYM / Angora / Pangolin / CoFuzz | 均 44/44（或 48，含额外误触发） |
| 【实测】本文 | 纯 concolic MPI np=32 | 44/44 |
可以保留的机制解释：LAVA-M 中部分 guard 是精确宽整数比较，适合一次位向量求解； 随机变异直接命中特定 32-bit 常量的概率很低。但 guard 可达性还依赖路径前缀、输入通道、 污点传播和构建配置，因此不能把每个 LAVA bug 都简化成“一次求解即可”。
CoFuzz Table VI 的 Tm 来自论文自己的 5 h protocol；本项目的 103 s 是另一运行在预算结束
后进行离线 endpoint 重放。二者不是同一 estimand，不能放进同一速度排名。正式横向比较
至少需要同 seed、同硬件/CPU budget、相同版本、逐 bug 首次触发时间和多轮生存分析。
但要立刻加三条限定：
1. 这个优势不能外推。 EnFuzz 的数据里，Google FTS 上 EnFuzz（AFL+AFLFast+libFuzzer+Radamsa）找到 60 个 bug、AFL 34 个；而 LAVA-M 那栏用的是含 QSYM 的 EnFuzz-Q，它在 FTS 上只有 41 个——换个基准就完全不是一个量级。LAVA-M 的 2K–4K 行代码正是 concolic 的舒适区；
2. base64 已经没有区分能力：【论文】里 7 个 hybrid fuzzer 全部拿满 44/44，差别只在速度。用它证明"我们比别人强"是无效的；
3. 覆盖率维度上更是早已饱和：benchmark_results_scaling/benchmark_data.csv 显示 lava base64 的边覆盖从 np=8 到 np=190 恒为 23.25 %——作为 scaling 信号完全无效。
真正还有区分度的是 who：【论文】里没有任何 hybrid 能在 5 小时内拿满（最好的 CoFuzz 1913/2136）。本项目对 who 只有覆盖率数据（hybrid np=32 达 47.26 %），从未做过 bug 计数——这是一个具体可补的实验。
benchmark/benchmark_results_v2/benchmark_data.csv：
| 目标 | 模式 | np | generated | 边覆盖 | 边 |
|---|---|---|---|---|---|
| base64 | afl-only | 1 | 108 | 7.81 %† | 85/1088 |
| base64 | mpi | 32 | 351,574 | 23.16 % | 252/1088 |
| base64 | hybrid | 32 | 2,222 | 23.90 % | 260/1088 |
| md5sum | mpi | 2/8/32 | 0 | 7.14 % | 96/1344 |
| uniq | mpi | 2/8/32 | 0 | 9.54 % | 116/1216 |
| who | hybrid | 32 | 7,150 | 47.26 % | 5051/10688 |
| who | afl-only | 1 | 44 | 44.57 % | 4764/10688 |
† 这个 afl-only 基线漏了 -d 参数（docs/PPT_Material_Supplement.md:168 已标注），不能当作 AFL 的覆盖率基线引用。
关于 uniq 的 "92 个 concolic 产出"（提交 4058446，docs/symsan_ported_techniques.md:264-265）：修掉两个叠加的 bug（taint_getc 逐字符丢标签；构建时 VAR=1 make clean; make ... 的环境作用域错误导致 __taint_trace_cond 链到空 weak stub）后，uniq 在 SymSan 下产出 92 个（fgtest）/ 305 个（fgtest_rgd）。92 是产出数不是 bug 数——SymSan 下从未测过 uniq 的 LAVA bug 数。
仓库多处声称"持久模式 png 18×、xml 7.5×"（benchmark/make_afl_targets_persistent.sh:5、docs/工作小结.md:57、提交 a4b4842），但没有任何数据文件——全树 + 全 git 历史搜索 38668/14894/2118/1991 均无命中。本文补测。
同一个 AFL 二进制，60 s，唯一差别 = 命令行带不带 @@
execs/s AFL 队列 bitmap 覆盖率
xml 带 @@ 15,191 ███████ 20 0.00% ← 跑得飞快，什么都没测到
xml 不带 @@ 40,787 ███████████████████ 4,144 10.51%
png 带 @@ 16,461 ████ 11 0.07% ← 同上
png 不带 @@ 143,718 ████████████████████████ 193 16.80%
检测方法： grep -a '##SIG_AFL_PERSISTENT##' <afl 二进制>
⚠ 绝不能改用 __afl_sharedmem_fuzzing 符号判断——fork 模式的 cmplog 伴随二进制也定义它，
误判会让 afl-fuzz "Fork server handshake failed"、所有轮次覆盖率归零。
复现：benchmark/qa3_repro/persab.sh，每组 60 s，同一个 AFL 二进制，唯一差别是命令行带不带 @@（持久+shmem 二进制带 @@ 会退回文件模式）：
| 配置 | execs/s | 总执行数 | AFL 队列 | bitmap 覆盖率 |
|---|---|---|---|---|
xml 带 @@（退回文件模式） |
15,191 | 911,006 | 20 | 0.00 % |
xml 不带 @@（持久+shmem） |
40,787 | 2,445,979 | 4,144 | 10.51 % |
png 带 @@（退回文件模式） |
16,461 | 987,188 | 11 | 0.07 % |
png 不带 @@（持久+shmem） |
143,718 | 8,621,527 | 193 | 16.80 % |
吞吐比 xml 2.7×、png 8.7×——但这远不是重点。 真正的问题是 带 @@ 时 bitmap 覆盖率是 0.00 % / 0.07 %：模糊测试器在以 1.5 万次/秒的速度跑，却几乎什么都没测到，队列 60 秒只长到 20 / 11 个。这正是 benchmark/run_benchmark.py:821-822 那条注释描述的失效模式（"@@ 会让目标落入文件模式/参数错乱、几乎测不到覆盖率（实测 2 边 vs 正确的 399）"），现在有了直接证据。
⚠ 这次复现和提交信息里的数字对不上，而且方法学是同一套。 提交
a4b4842的原话是 "Measured A/B (identical binary, @@ vs no-@@): png 2.1k→38.7k (18x), xml 2.0k→14.9k (7.5x)"——和本文用的是完全相同的做法（同一二进制、只改带不带@@），所以两组数字本来应当可比。但实测：
提交 a4b4842本文复现 png 带 @@2.1 k 16.5 k png 不带 @@38.7 k 143.7 k xml 带 @@2.0 k 15.2 k xml 不带 @@14.9 k 40.8 k 四个数全部不吻合（本机更快，且"before"侧高出 7–8 倍）。可能来自机器、AFL++ 版本或二进制重编，但原始的 18× / 7.5× 在本仓库内既无数据文件、也无法按其自述方法复现，不应继续引用。 真正稳健、且本文能直接复现的结论是下面这条：带
@@时 bitmap 覆盖率是 0.00 % / 0.07 %——速度比值多少都不重要，因为那一侧根本没在测东西。
benchmark_results_scaling_hybrid）¶ 纯 MPI 吞吐 (tc/s) 纯 MPI 边覆盖 (%)
np=2 128 ▏ 5.67 ██████████████████████▋
np=8 1604 ███ 5.88 ███████████████████████▌
np=32 7683 ███████████████ 6.13 ████████████████████████▌
np=128 15022 ██████████████████████████████ 6.26 █████████████████████████
np=190 13906 ███████████████████████████▊ 6.17 ████████████████████████▋
hybrid 吞吐 (tc/s) hybrid 边覆盖 (%)
np=2 27 · 7.81 ███████████████████████████████▏
np=8 55 ▏ 8.37 █████████████████████████████████▍
np=32 187 ▍ 8.82 ███████████████████████████████████▎
np=128 497 ▉ 8.84 ███████████████████████████████████▎ ← 最高
np=190 590 █ 8.80 ███████████████████████████████████▏
AFL-only np=1（单实例，非等 CPU） 21 · 7.55 ██████████████████████████████▏
⇒ 纯 MPI 吞吐涨 117 倍（128→15022），边覆盖只从 5.67% 挪到 6.26%。
⇒ 生成总量与离线覆盖不单调；但两份大语料的 showmap 都最多抽样 20,000 个文件，
因此不能据此宣称“少 26 倍测试仍覆盖更高”。
gfts-xml 行来自图中同一份 benchmark_results_scaling_hybrid；其余两行来自
benchmark_results_scaling。均为 120 s、1 轮、纯 MPI 吞吐（tc/s）：
| 目标 | np=2 | np=8 | np=32 | np=128 | np=190 |
|---|---|---|---|---|---|
gfts-xml_read_fuzzer |
128.2 | 1,603.9 | 7,682.9 | 15,022.1 | 13,905.9 |
lava-base64_harness |
171.6 | 1,027.3 | 4,117.2 | 12,249.2 | 13,023.5 |
lava-base64 |
104.5 | 652.6 | 2,222.6 | 5,523.1 | 6,471.4 |
base64_harness 是唯一有非零串行基线、因而有真实加速比的目标：np=2 7.30×（100 %）→ np=8 43.68×（85.5 %）→ np=32 175.08×（77.4 %）→ np=128 520.88×（57.1 %）→ np=190 553.80×（41.0 %）。吞吐在 np=128~190 之间掉头。
但覆盖率不随吞吐单调增长：图中同一 CSV 的 xml 纯 MPI np=2→128 只从
5.67 % 到 6.26 %，hybrid 为 7.81 % 到 8.84 %。必须同时注明：
measure_showmap_coverage(..., max_cases=20000) 会对更大语料随机抽样
（run_benchmark.py:752-831）；这些行的候选数远超 20,000，而 CSV schema 没有持久化
sampled、sampled_cases 或 sample digest。故历史覆盖数字是固定上限样本估计，
不能证明完整语料并集，也不能从“generated/unique”反推 corpus efficiency。
benchmark_results_v2（300 s）hybrid vs afl-only：
| 目标 | afl-only execs/s | hybrid np=32 execs/s | afl-only 边 | hybrid np=32 边 |
|---|---|---|---|---|
| png | 4,928 | 4,121 | 14.10 % | 16.96 % |
| xml | 2,880 | 2,362 | 7.60 % | 8.90 % |
| libarchive | 2,277 | 2,138 | 15.07 % | 23.36 % |
| sqlite | 2,694 | 2,885 | 18.55 % | 18.84 % |
| pcre2 | 4,870 | 3,931 | 41.73 % | 43.58 % |
| freetype2 | 3,496 | 3,433 | 5.75 % | 5.59 % |
⚠ 读这张表前必须知道（§1.10 实测）：在 ≤300 s 的轮次里，concolic 产出根本没进到 AFL 手里（直注被忽略、兄弟目录同步要等 10 分钟）。所以 hybrid 那一列不是"AFL 用上了 concolic 的解"的结果，而是
afl-showmap对 AFL 队列 ∪ concolic 产出这个并集语料的离线测量。数字本身没错（并集口径下成立），但不能解释成反馈闭环生效。
hybrid 对 AFL 吞吐的影响实测在 −19 % 到 +7 % 之间（png −16.4 %、xml −18.0 %、pcre2 −19.3 %、libarchive −6.1 %、freetype2 −1.8 %、sqlite +7.1 %）——多数是 CPU 争用带来的损失，但并非一律下降。两条必须一起说的限定：
docs/PPT_Material_Complete.md:432-436 已标注）。等 CPU 下的正确参照是 §5.4.2 那组 16 核/64 核分配扫描。⚠ 一条本仓库无法验证的数据：会上补测据称"libarchive 在 32 实例 afl-only 下达到 27.71 %，与 hybrid np=32 的 26.95 % 持平（净增益 ≈ 0）"。这些数字在本仓库工作树里搜不到（
27.71/26.95均无命中），产物在外部。引用时必须注明出处在仓库之外、无法就地复现。
--timeseries 已实现（run_benchmark.py:1101-1279）但从未在正式实验里启用，全树无 *timeseries* 文件。docs/Final_Work_Report.md:284 明确记录了这一点。µFUZZ 的 Magma 存活时间分析是这块的标杆；np=190 都是单机 190 个 rank；research_protocol.py 的门槛是 20，docs/sota_hybrid_execution_2026.md:2300-2302 承认公开确认性 campaign 尚未运行）；sampled、sampled_cases、随机种子或 sample digest。正式结果必须持久化这些字段，
并同时报告完整语料数；crashes/ 不能作为完备输入；who 从未做过 bug 计数。它是 LAVA-M 四个目标里唯一还有区分度的（【论文】里 7 个 hybrid fuzzer 都拿不满 2136，最好的 CoFuzz 1913）。本项目对 who 只有覆盖率（hybrid np=32 47.26 %），scratch_lava_bugcount.py 也支持它（需用 who_countable 而非仓库预编的 who，后者把 bug printf 编掉了）。这是一个成本极低、区分度极高的可补实验；SYMCC_TARGET_BRANCH 的单分支定向机制已经存在，缺的是接一个边级效用模型。确认性 protocol 的最小交付物应为：equal CPU、同版本/同 seed、≥20 个独立随机重复、 随时间的 edge/bug 首次发现事件、Kaplan-Meier 或同等生存分析、置信区间/效应量、逐 bug 内容溯源，以及 immutable run manifest。只有终点 bug 数而没有 time-to-bug 不能回答速度。
SoK: Prudent Evaluation Practices for Fuzzing（IEEE S&P 2024）统计了 289 篇 fuzzing 论文的评估实践。把本项目摆进去对照：
| 规范维度 | 学界建议（原始出处） | 289 篇论文的现状 | 本项目现状 |
|---|---|---|---|
| 目标数量 | ≥ 10 个有代表性的真实程序（Böhme et al. R1） | — | ✅ 10 个（6 真实 + LAVA-M 4） |
| 单次时长 | Klees et al. 提 24 小时；Böhme et al. R1：≥12 h（最好 24 h） | 只有一部分论文跑满 24 h | ❌ 实测多为 120 / 300 s，最长档也远不够 |
| 重复次数 | Klees et al. 自己用 30 次；Böhme et al. R1：每个 fuzzer×程序组合 ≥10 次（最好 20 次） | 55 %（83 篇）在某个实验里少于 10 次 | ❌ 归档实验多为 rounds=1；SymSan 那组是 3 轮 |
| 显著性检验 | Mann-Whitney U 检验或 bootstrap 方法（SoK Recommendation 5，§3.2.6 统计） | 63 %（94 篇）完全不做统计检验；37 % 做 Mann-Whitney U | ⚠️ 代码里有（bootstrap + 符号翻转），但归档结果没用上 |
| 效应量 | Vargha–Delaney Â12 | 88 %（132 篇）完全不报效应量；只有 10 % 做 Â12 | ⚠️ analyze_ablation.py 实现了 vargha_delaney，同样未用于归档结果 |
| 随时间的曲线 | Klees et al. 建议 plot performance over time | — | ❌ --timeseries 实现了但从未启用（§6.8） |
| 主/次指标 | 主指标应为发现 bug 的能力，覆盖率（基本块或边）作次要指标（Klees et al.） | — | ⚠️ 本项目基本只用边覆盖；bug 计数只有 LAVA-M 的离线脚本 |
| 注入 bug 基准 | LAVA-M 已被视为有缺陷（SoK §3.2.2 Targets under Test） | 21 % 的论文仍在用 | ⚠️ 本项目在用，但§6.3 已按"只验证通路、不比强弱"定位 |
Böhme et al. R1 原文（ICSE 2022 §7.2）：
"R1 If possible, select at least 10 representative programs. For each fuzzer-program combination, conduct at least 10 (better 20) campaigns of at least 12 (better 24) hours. Increasing these values improves generality and statistical power of the results."
按这条尺子，本项目的差距是量级级别的：--timeout 默认 60 s、归档实验 120–300 s、rounds=1，
对照 R1 的"每组 ≥10 次 × ≥12 小时"——单个 fuzzer×程序组合的预算差约 3 个数量级。
两个诚实的观察：
benchmark/analyze_ablation.py 恰恰实现了 bootstrap_ci / paired_bootstrap_ci / vargha_delaney / holm_adjust，research_protocol.py 还强制等 CPU 预算和 ≥20 次重复。工具比 88 % 的论文都齐全。research_protocol.py 契约的确认性 campaign，就能把大量 B 级结论升到 R 级。| 测量 | 位置 | 一句话结论 |
|---|---|---|
| 发现一个此前无记录的架构问题 | §1.10 | 两个独立实验证明：运行中的 AFL 不重扫自己的 queue/（直注无效），兄弟目录同步默认要等 10 分钟（-M）⇒ ≤300 s 的 benchmark 轮次里 concolic 产出一个都没送到 AFL；hybrid 覆盖率只能按"离线并集"解释 |
| 发现并修复一个真 bug | §1.4 | _snap 读错位图 + tuple >= int ⇒ 开 profiling 后每个 worker 第 2 个工作项必崩。这就是仓库从来没有可用 redundancy.csv 的原因；修后工作项 9 → 322 |
| B3 位图过滤效果 | §1.4 | 同一种子第 2 轮起 interesting 225→0、Z3 查询归零；位图文件 131072 B |
| 端到端漏斗 | §1.6 | 3,154 产出 → worker 位图 299（9.5 %）→ master 位图 167（5.3 %）；字节级重复占 34.8 %；反馈迭代到第 3 代 |
| 相位计时 | §1.6 | bmsync 0.02 ms/项，在本轮可忽略；scan 是最大 master 已测相位，但 12% 记账率不足以证明端到端瓶颈 |
| 求解策略构成（6 目标） | §3.3 | -optimistic 文件占保存事件 49–84 %，不是 campaign 覆盖占比；六条单种子 trace 无 Z3 超时；FAST/OPT-FIRST 的收益也只限该短测 |
| 乐观求解的边贡献 | §3.4 | 一次性 edge-ID 重放中 xml/png 都有策略互补；脚本未计 hit-count 和端到端成本，不能证明净收益 |
| 嵌套深度 × 前沿策略 | §3.5 | nxt[:64] 取头 FIFO 在深度 16/32 卡在第 10 层，coverage 前沿可解；结论不外推到其他截断或 continuation 流 |
| 种子长度决定成败 | §4.3 | 同一二进制：8 字节种子第 6 代命中；4 字节种子进不动点，因为 if (n<8) 根本不是符号分支 |
| 真实 SMT 约束转储 | §4.4 | 校验和被单条 bvadd 一次解出；k!50/k!60/k!70 = 输入偏移 5/6/7 |
focus_bytes 效果 |
§4.5 | 范围外分支不产生查询也不产生输出（6 → 4 → 1 → 2 个产出） |
| 真实 base64 求解轨迹 | §4.9 | 175 B 种子 773 符号分支 / 230 产出但内容只有 134 种；4096 B 种子只剩 179 分支——值定路径、长定上界 |
| 持久模式 A/B | §6.6 | 带 @@ 时 bitmap 覆盖率 0.00 % / 0.07 %——跑得飞快但什么都没测到 |
| LAVA-M bug 重放 | §6.5 | 不同历史运行的 endpoint 为 AFL 0/44、纯 concolic 42/44/44；非等 CPU、无首次发现时间，只支持机制假设，不支持速度排名 |
本文已脚本化的实测随文保存：benchmark/qa3_repro/
（measure_strategy.sh、landing.py、landing2.py、iterate.py、iterate2.py、funnel.sh、persab.sh、trace_base64.sh）。
⚠ 尚未脚本化：§4.3–§4.6 的合成 magic/长度/校验和目标（文中给了完整源码与命令，但没有 driver 脚本）。
证据等级声明：本文所有 【实测】 数据均为单次运行，用于说明机制、量级和方向，
按 docs/README.md:41-43 的规则属于 B 级。要升级为 R 级结论，需按
benchmark/research_protocol.py 的契约补等 CPU、多轮（≥20）、置信区间与逐项消融。
论文
ufuzz.pdf 是匿名投稿版）。enfuzz.pdf 是 arXiv:1807.00182v2）。pafl.pdf）。工具文档 / 源码
instrumentation/afl-compiler-rt.o.c —— §1.4 的 PCGUARD 边 ID 分配（__sanitizer_cov_trace_pc_guard / __afl_final_loc）：
https://github.com/AFLplusplus/AFLplusplus/blob/stable/instrumentation/afl-compiler-rt.o.cdocs/env_variables.md —— §1.10 的 AFL_SYNC_TIME 默认值（20 分钟，-M 减半）：
https://github.com/AFLplusplus/AFLplusplus/blob/stable/docs/env_variables.md