并行框架 · 约束形态 · 求解策略 · 种子影响 · ICSE'23 复现 · 基准与 LAVA-M
更新于 2026-07-29 分支 engine-configurable-symsan 25 张示意图 + 7 张一手证据截图
| 文件 | 大小 | 说明 |
|---|---|---|
| Architecture_QA3.html | 286 KB | 📖 在线阅读（推荐）——25 张示意图 + 7 张一手证据截图，深/浅色自适应 |
| Architecture_QA3.md | 189 KB | 📝 Markdown 原文 |
| symcc-qa3-docs.tar.gz | 6.2 MB | 📦 全部打包（文档 + HTML + 图集 + DOT 图源 + 证据截图 + 复现脚本） |
| diagrams/ | 64 个文件 | 🖼 25 张示意图（SVG+PNG），src/ 内含 13 个 DOT 图源 |
| evidence/ | 9 个文件 | 🔬 7 张一手证据截图（说明）：objdump / showmap / IR / gdb / fuzzer_stats / 实跑 / 原始报告 |
| qa3_repro/ | 10 个文件 | ⚙️ 10 个复现脚本（README） |
| MANIFEST.txt | 11 KB | 📋 清单：git 版本 + 内容计数 + 逐文件 SHA256 |
| SHA256SUMS.txt | 0 KB | 🔐 主文件校验和 |
| 问题 | 主题 | 要点 |
|---|---|---|
| Q1 | 并行框架的执行流程与位图 | 5 张位图全景、17 步 worker 次序、端到端漏斗；并发现运行中的 AFL 收不到 concolic 产出 |
| Q2 | 三种比较形态 + 正常编译 vs 自测试 | 形态由优化器决定；laf-intel 只作用于 AFL 侧二进制 |
| Q3 | 何时 Z3、何时乐观、何时丢前缀 | 决策树逐步核对；6 目标策略占比实测；嵌套深度对照实验 |
| Q4 | 输入为何决定 DSE 成败 + 真实调试 | IR + gdb 一手证据 · 合成目标逐代演进 · 真实 LAVA-M base64 轨迹 |
| Q5 | ICSE'23（CoFuzz）论文的复现 | 方法学与 7 条 Finding 取自论文原文；本项目等 CPU 对照 |
| Q6 | 基准目标与 LAVA-M | QSYM'18 / CoFuzz'23 / 本文三个独立数据点；对照 IEEE S&P'24 SoK |
qa3_repro/ 的脚本复现，但都是单次短测；
7 张证据截图来自各自当时的一次运行，只用于佐证机制，不提供可比数值。
论文引用已全部回原文逐条核对，出处见文档末尾 17 条参考文献。引用前请优先自行复现。校验：sha256sum -c SHA256SUMS.txt 逐文件哈希见 MANIFEST.txt