# SymCC MPI 并行符号执行 — 工作进展报告（三）

## 上期回顾

上一阶段（报告二）完成了全量 Benchmark（10 个目标 × 300s × np=2/8/32），建立了双指标体系，得出核心结论：SymCC 有效性高度依赖目标特征，覆盖率不随并行度线性增长是 concolic execution 的固有限制。

**本期目标**：突破 SymCC 的约束求解限制，从求解层面提升覆盖率。

---

## 背景知识

### SymCC 的工作原理（简述）

SymCC 是一种**编译时 concolic execution 工具**。它在编译时通过 LLVM Pass 在程序的每条指令上插入"影子计算"代码。程序运行时，除了正常执行（具体值），还同时构建一棵**符号表达式树**——记录每个变量如何依赖输入字节。

当程序执行到一个分支（如 `if (buf[0] == 'P')`），SymCC 会：
1. 记录当前走了哪个方向（比如 `taken=true`，即 `buf[0]` 确实等于 `'P'`）
2. 将分支条件取反（`buf[0] != 'P'`），交给 Z3 求解器
3. Z3 找到一个满足取反条件的输入值（如 `buf[0] = 0x00`）
4. 将这个新输入写入输出目录，作为新的测试用例

这个过程每次只处理**一条路径**上的分支——程序按具体输入执行一遍，沿途对每个 interesting 分支做一次"取反求解"。

### AFL 的工作原理（简述）

AFL 是一种**覆盖引导的模糊测试器**。它维护一个种子队列，对每个种子进行随机变异（翻转比特、插入字节、使用字典 token 等），然后执行目标程序检查是否触发新的代码路径（用一个 65536 字节的 bitmap 记录边覆盖情况）。发现新路径的变异结果被保存为新种子，加入队列继续变异。

### 覆盖率指标

本报告使用两种覆盖率指标：

- **ShowmapCov**：用 `afl-showmap -C` 工具在实验结束后，将所有保存的测试用例重新执行一遍，统计触发了多少条程序边（edge）。分母是 `afl-showmap` 报告的程序中编译时插桩的**全部边数**（包括从未触发的边）。例如 SQLite 有 31,680 条插桩边。
- **FstatsCov**：从 AFL 运行时自动记录的 `fuzzer_stats` 文件中读取 `bitmap_cvg`（= `edges_found / total_edges`）。它反映 AFL **在整个运行过程中所有执行**（包括未保存的变异）的累积覆盖。分母 `total_edges` 是 AFL bitmap 中实际使用的槽位数，受 hash 碰撞影响通常**小于**插桩边数。例如 SQLite 的 `total_edges` 为 20,509（vs ShowmapCov 的 31,680）。

**为什么两个指标的分母不同**：`afl-showmap` 通过分析插桩二进制的代码段直接统计所有注入的边（包括从未被执行到的死代码中的边）；而 AFL 的 `total_edges` 只统计 bitmap 中被使用的 hash 槽位。由于 AFL 使用 `(prev_block ^ cur_block) % MAP_SIZE` 做边 hash，不同的边可能映射到同一个槽位（碰撞），所以 `total_edges` < 实际插桩边数。**本报告所有对比均在同一指标内进行，不跨指标比较百分比值。**

---

## 一、问题分析：为什么单纯种子共享不够高效

### 1.1 问题现象

上期实验中一个反复出现的模式是：SymCC 生成大量测试用例（如 SQLite np=8 生成 4,000+），但覆盖率仅比 AFL-only 高 0.3pp（FstatsCov 维度）。SymCC 的产出量与覆盖率贡献严重不成比例。

### 1.2 根因定位

通过代码分析（`solver.cpp` 的 `addJcc` → `negatePath` → `syncConstraints` 完整调用链），定位到 4 个层面的效率损失：

#### 损失 1：单步约束翻转的固有限制

**含义**：SymCC 沿一条执行路径走到底，途中遇到的每个分支条件，都**单独取反求解一次**。每次求解只改变**一个**分支的方向，因此输出的新测试用例通常只有 1-3 个字节与原始输入不同。

**具体示例**：假设输入是 SQL 语句 `"SELECT * FROM t"`，程序的词法分析器逐字符比较关键字。执行路径上有 6 个分支：`input[0]=='S'?` → `input[1]=='E'?` → ... → `input[5]=='T'?`。SymCC 对每个分支独立求解，产出 6 个新输入，每个只改了 1 个字节：

```
原始输入: "SELECT * FROM t"
SymCC 输出 1: "·ELECT * FROM t"  （byte[0] 被 Z3 改为某个 != 'S' 的值）
SymCC 输出 2: "S·LECT * FROM t"  （byte[1] 被改为 != 'E' 的值）
...
SymCC 输出 6: "SELEC· * FROM t"  （byte[5] 被改）
```

这 6 个输出都不是合法的 SQL 关键字——它们不会让程序进入 `INSERT`、`UPDATE` 等不同的处理分支。要生成 `"INSERT"` 需要**同时**改变 6 个字节（`S→I, E→N, L→S, E→E, C→R, T→T`），但 SymCC 的"单步翻转"机制每次只改一个。

**这是 concolic execution 的根本局限**：它只探索当前路径的"邻域"（相邻路径），无法跳到距离较远的路径。

#### 损失 2：盲目种子选择

Master 从 AFL queue 中按先进先出（FIFO）顺序取种子给 SymCC 处理。AFL queue 中大量种子已被 AFL 充分变异，SymCC 重复分析这些种子只会产出 AFL 已覆盖过的路径。没有优先级机制区分"高价值种子"和"已饱和种子"。

#### 损失 3：约束信息丢失

**含义**：SymCC 在求解过程中获得了宝贵的**结构化知识**——例如"输入的第 257 个字节必须等于 0x75 才能匹配 tar 格式的 magic number 'ustar'"。但这些知识仅以**文件中的具体字节值**的形式传递给 AFL。AFL 收到这个文件后，不知道"第 257 字节是关键的"——它仍然用盲目的 bitflip/havoc 变异整个文件，无法针对性地在**其他文件的第 257 字节**也尝试 0x75。

**类比**：SymCC 像一个解题专家，解出了"密码的第 3 位是 7"。但它只把带着正确第 3 位的完整密码交给 AFL，而没有告诉 AFL"第 3 位是 7 很重要"。AFL 拿到密码后可能会随机改第 3 位，又把 7 改没了。

#### 损失 4：约束膨胀

**含义**：SymCC 在运行时为输入的**每一个字节**创建一个 Z3 符号变量。但是，一个具体的分支条件可能只依赖输入的 3 个字节（比如 `buf[0]=='P' && buf[1]=='K' && buf[2]==0x03`）。当 SymCC 把这个分支的取反条件交给 Z3 求解时，Z3 的上下文中包含了**整条执行路径上所有分支**的约束——这些约束可能涉及 1024 个符号变量中的大部分。

**SymCC 求解的是什么**：不是"从入口到执行点"的完整路径约束，而是通过**依赖森林**（DependencyForest）筛选出的**与目标分支共享输入字节的所有约束**。具体来说：如果目标分支依赖 byte[3] 和 byte[7]，SymCC 会找出所有同样涉及 byte[3] 或 byte[7] 的历史约束，作为 Z3 的上下文。这比加载全部路径约束高效，但当某个字节被大量分支共享时（如循环计数器），依赖树可以非常大，导致 Z3 收到大量约束而超时（默认 10 秒限制）。

### 1.3 文献调研

对 2021-2026 年的最新研究进行了系统调研，识别出 6 个改进方向：

| 来源 | 方向 | 解决的问题 |
|------|------|-----------|
| CONFETTI (ICSE 2022) | 约束 hint 传递给 fuzzer | 损失 3 |
| LeanSym (RAID 2021) | 选择性符号化 | 损失 4 |
| MEUZZ / K-Scheduler | 智能种子调度 | 损失 2 |
| FUZZOLIC (2021) | Fuzzy-Sat 近似求解 | 损失 4 |
| Cottontail / ConcoLLMic (S&P 2026) | LLM 约束求解 | 损失 1 |
| Backsolver (TOSEM 2025) | 反向路径适配 | 损失 1 |

本期选择前 4 个方向进行实施（最后 2 个列入中长期计划），并新增了"多分支联合求解"直接解决损失 1。

---

## 二、实施的改进（5 项）

### 2.1 多分支联合求解（C++ 层，`solver.cpp`）

**目标**：解决损失 1——让 Z3 一次性改变多个字节，生成"跳跃式"变体。

**设计**：在标准的逐分支求解之外，额外收集连续出现的 interesting 分支，检测是否属于"连续字节比较"模式，若是则一次性将所有分支条件取反交给 Z3 联合求解。

**"偏移连续"的含义**：每个分支条件依赖输入的某个字节位置（偏移量）。如果连续几个分支分别依赖 byte[257]、byte[258]、byte[259]、byte[260]、byte[261]，这些偏移量 257、258、259、260、261 是**严格递增且无间隔**的——这就是"偏移连续"。这种模式典型地出现在 `strcmp`/`memcmp` 类的字符串比较中，程序逐字节检查输入是否匹配某个 magic number（如 tar 格式的 `ustar`）。

**具体示例**（libarchive 解析 tar 文件）：

```
tar 文件偏移 257-261 处存储 magic number "ustar"

程序执行：
  if (buf[257] == 'u')   → 分支 1，依赖 byte[257]
  if (buf[258] == 's')   → 分支 2，依赖 byte[258]
  if (buf[259] == 't')   → 分支 3，依赖 byte[259]
  if (buf[260] == 'a')   → 分支 4，依赖 byte[260]
  if (buf[261] == 'r')   → 分支 5，依赖 byte[261]

偏移序列 [257, 258, 259, 260, 261] → 严格连续 → 触发联合求解

标准模式（逐分支）：产出 5 个单字节变体，每个只改 1 字节
联合求解：Z3 同时求解 buf[257]!='u' ∧ buf[258]!='s' ∧ ... ∧ buf[261]!='r'
  → 一次性改变 5 个字节
  → 若路径约束中包含对 zip magic "PK\x03\x04" 的判断，
    Z3 可能在满足路径约束的同时生成 zip 格式的输入
```

**三种检测模式**：

| 模式 | 检测条件 | 典型场景 | 控制级别 |
|------|---------|---------|---------|
| 连续字节比较 | 各分支依赖的输入字节偏移连续（如 257,258,259） | `strcmp`/`memcmp` | `SYMCC_MULTI_SOLVE=1` |
| 同变量 switch-case | 各分支依赖完全相同的字节集合，但比较不同常量 | `switch(type)` | `SYMCC_MULTI_SOLVE=2`（实验性） |
| 邻近结构体字段 | 各分支依赖的字节在 64B 窗口内 | 文件头 magic + version + flags | `SYMCC_MULTI_SOLVE=2`（实验性） |

**迭代过程**：

| 版本 | 策略 | libarchive FstatsCov | 问题 |
|------|------|------:|------|
| v1 盲目联合 | 每 8 个 interesting 分支直接联合求解 | 17.88%（基线 17.94%） | Z3 超时严重，生成量 -30% |
| v2 连续字节 | 仅对连续字节偏移的分支联合求解 | **20.02%**（+2.08pp） | 检测精确，无吞吐量损失 |
| v3 三模式 | 连续字节 + switch + struct | 16.88%（-1.06pp） | 新模式约束过复杂，Z3 超时 |

**结论**：v1 证明盲目联合求解因 Z3 超时而适得其反；v2 精准命中字符串匹配场景（如 libarchive 的 `ustar`/`PK\x03\x04` magic），是唯一有效的模式。最终 v2 设为 `SYMCC_MULTI_SOLVE=1`（推荐），v3 设为 `=2`（实验性）。

### 2.2 智能种子调度（Python 层，`mpi_fuzzing_helper.py`）

**目标**：解决损失 2——优先处理高价值种子，减少无效 SymCC 执行。

**设计**：重写 `best_new_testcases()` 方法，从 FIFO 改为多因子打分：

| 因子 | 权重 | 原理 |
|------|-----:|------|
| `+cov` 标记 | +100 | AFL 文件名中带 `+cov` 表示该种子发现了新覆盖，最可能位于探索前沿 |
| SymCC 产出（`symcc_` 前缀） | +20 | 对 SymCC 输出再做一轮符号执行（迭代深化）可探索更深路径 |
| AFL ID 新颖度 | +0~50 | AFL 文件名中的 ID 越大越新，越可能在覆盖前沿 |
| 大文件惩罚 | -30 max | >10KB 文件 SymCC 执行慢且约束多 |

此外，维护 `processed_content_hashes` 集合（SHA-256 哈希），跳过与已分析种子内容完全相同的文件（不同文件名但相同内容）。

### 2.3 约束 hint 传递（C++ + Python 层）

**目标**：解决损失 3——将 SymCC 发现的约束知识传递给 AFL 的变异策略。

**设计**（参考 CONFETTI 论文的 global hinting 机制）：

1. **C++ 层**：SymCC 生成输出文件时，同时写入 `.hints` 文件，记录**哪些字节被修改了、从什么值改到什么值**。格式：每行 `offset:old_hex:new_hex`（例如 `257:75:00` 表示第 257 字节从 0x75 改为 0x00）。

2. **Worker 层**：收集 `.hints` 文件，将 hint 信息通过 MPI 传回 Master。

3. **Master 层**：将 hint 中的字节值写入 AFL 的 `extras/` 目录。AFL 自动将 `extras/` 中的文件作为**字典 token**，在变异时以一定概率在输入的**任意位置**插入这些字节。这样 SymCC 发现的"byte 257 应为 0x75"就变成了 AFL 的字典词条，AFL 会在其他输入的不同位置也尝试插入 0x75。

### 2.4 选择性符号化（C++ + Python 层）

**目标**：解决损失 4——减少 Z3 需要处理的约束数量。

**什么是选择性符号化**：标准 SymCC 为输入的**每一个字节**创建一个 Z3 符号变量。"选择性符号化"是只对**特定范围的字节**创建符号变量，其余字节保持为具体值（concrete）——它们在运行时仍参与计算，但不产生 Z3 约束。

**怎么选择**：通过环境变量 `SYMCC_FOCUS_BYTES="start-end"` 指定范围。例如 `"100-200"` 表示只对输入的第 100~200 字节进行符号化。范围外的字节在 `_sym_get_input_byte()` 函数中直接返回 NULL（concrete），不创建符号表达式，从源头消除无关约束。

**自适应机制**：Master 根据之前的 hint 偏移信息自动计算关注范围——如果 SymCC 之前发现第 50、55、60 字节是"interesting"的（产出了新覆盖的测试用例），Master 会计算范围为 [50-32, 60+32] = [18, 92]，并通过 dispatch 消息传递给 Worker。初始无限制（全字节符号化）；积累 ≥5 个 interesting 偏移后自动收窄。

### 2.5 Fuzzy-Sat 近似约束求解（C++ 层，`solver.cpp`）

**目标**：进一步解决损失 4——对简单约束跳过 Z3，直接计算结果。

**设计**：在 `negatePath()` 开头新增 `fastSolve()` 快速路径。对形如 `input_byte[i] == constant` 的简单约束（单个输入字节与一个常数的比较），直接通过位运算计算满足取反条件的值，跳过 Z3 调用。

```
示例：分支条件 buf[5] == 0x50, taken=true（程序走了 true 分支）
  → 取反：buf[5] != 0x50
  → fast-solve：设 buf[5] = 0x50 ^ 0x01 = 0x51
  → 直接写入输出文件（标记 "-fast"），耗时 μs 级
  → Z3 仍然被调用做完整求解（可能发现依赖多个字节的解）
```

`fastSolve` 成功后**不跳过** Z3——Z3 仍被调用，因此 fast-solve 是**纯增量**产出。由 `SYMCC_FAST_SOLVE=1` 控制。

---

## 三、实验结果

### 3.1 实验设计

所有实验使用相同条件：Hybrid np=8（1 个 AFL + 1 个 Master + 6 个 SymCC Worker），timeout=300s，单轮运行。目标：SQLite（SQL 数据库引擎，文本解析器）和 libarchive（归档解析库，支持 tar/zip/cpio 等多种格式）。

**`SYMCC_TIMEOUT=30` 的含义**：每个 SymCC Worker 执行一个输入文件的最大时间限制。原始默认值为 10 秒，改为 30 秒。这不是通过实验调参得到的最优值，而是一个**工程判断**：10 秒对于含大量分支的程序（如 SQLite 解析复杂 SQL）过短，SymCC 还没来得及遍历路径上的所有分支就被 kill；30 秒给予充分的探索时间，同时不至于让单个 Worker 长时间占用。理想值取决于目标程序的路径长度，但缺少系统调参实验。

**重要说明**：v1/v2/v3 不是同一代码的不同配置，而是 `solver.cpp` 的三次代码迭代。各版本的代码差异见第二章迭代过程表。

| 组别 | 代码版本 | 环境变量 | 与基线的代码差异 |
|------|---------|---------|----------------|
| **基线** | 原始代码 | `SYMCC_TIMEOUT=10`（默认） | 无 |
| **v1** | solver.cpp 第 1 版 | `SYMCC_MULTI_SOLVE=1` | 盲目联合求解（每 8 个分支触发） |
| **v2** | solver.cpp 第 2 版 | `SYMCC_MULTI_SOLVE=1` | 仅连续字节模式触发联合求解 |
| **v3** | solver.cpp 第 3 版 | `SYMCC_MULTI_SOLVE=1` | 三模式检测 |
| **全部增强** | 最终版（含 Python 层改动） | `SYMCC_MULTI_SOLVE=1 SYMCC_EMIT_HINTS=1 SYMCC_TIMEOUT=30` | v2 联合求解 + 智能调度 + hint + 选择性符号化 + 迭代深化 |
| **全部增强+fast** | 最终版 | 上述 + `SYMCC_FAST_SOLVE=1` | 上述 + Fuzzy-Sat |

**控制变量的已知缺陷**：
- 基线 `SYMCC_TIMEOUT=10`，全部增强 `=30`。无法排除覆盖率差异中有多少来自超时增加本身。
- 智能种子调度是代码层面改动，无法通过环境变量禁用。全部增强组与基线组**代码不同**。
- 各组实验为不同时间的独立运行，AFL-only 基线也在波动（见 3.5 节）。

### 3.2 libarchive 结果

为消除 AFL-only 基线波动的影响，增加"Hybrid 相对同次 AFL-only 的增益"列（差值 = 同一次实验中 Hybrid 覆盖率 - AFL-only 覆盖率）：

| 版本 | ShowmapCov | 同次 AFL-only | **差值** | FstatsCov | 同次 AFL-only | **差值** | 生成量 |
|------|------:|------:|------:|------:|------:|------:|------:|
| 基线 | 23.19% | 16.49% | **+6.70pp** | 17.94% | 16.56% | **+1.38pp** | 7,274 |
| v1 盲目 | 20.33% | 16.93% | +3.40pp | 17.88% | 17.00% | +0.88pp | 5,107 |
| v2 连续 | 22.87% | 16.63% | **+6.24pp** | 20.02% | 16.70% | **+3.32pp** | 7,118 |
| v3 三模式 | 20.45% | 17.04% | +3.41pp | 16.88% | 17.11% | -0.23pp | 5,494 |
| **全增强** | **26.70%** | 17.12% | **+9.58pp** | **21.75%** | 17.19% | **+4.56pp** | 7,142 |
| 全增强+fast | 22.57% | 16.91% | +5.66pp | 18.43% | 16.98% | +1.45pp | 7,026 |

**分析**：

1. **全部增强在差值维度最优**。FstatsCov 差值 +4.56pp（基线 +1.38pp），净增 +3.18pp。

2. **v2（连续字节）单独贡献确认**。FstatsCov 差值从 +1.38pp 提升到 +3.32pp（净增 +1.94pp）。连续字节联合求解精准命中 libarchive 的 magic number 匹配。

3. **全增强相对 v2 的增量**（+4.56 - 3.32 = +1.24pp）来自智能调度 + hint + 超时增加的组合，但缺少消融实验**无法分离各项独立贡献**。

4. **v1 和 v3 效果为负**。v1 生成量暴跌 30%，v3 的 FstatsCov 差值为负。Z3 对复杂联合约束频繁超时是主因。

5. **fast-solve 对 libarchive 覆盖率下降**（全增强+fast 22.57% vs 全增强 26.70%，-4.13pp）。fast-solve 产出的大量单字节变体增加了 Worker 输出目录中的文件数，导致后续 showmap dedup 处理时间增长，压缩了单位时间内的有效探索次数。此问题需进一步排查。

### 3.3 SQLite 结果

| 版本 | ShowmapCov | 同次 AFL-only | **差值** | FstatsCov | 同次 AFL-only | **差值** | 生成量 |
|------|------:|------:|------:|------:|------:|------:|------:|
| 基线 | 21.14% | 19.71% | **+1.43pp** | 28.83% | 27.35% | **+1.48pp** | 4,183 |
| v1 盲目 | 20.31% | 20.83% | -0.52pp | 27.91% | 28.40% | -0.49pp | 4,206 |
| v2 连续 | 19.69% | 19.24% | +0.45pp | 26.68% | 26.85% | -0.17pp | 4,542 |
| v3 三模式 | 20.46% | 20.15% | +0.31pp | 27.86% | 27.65% | +0.21pp | 4,315 |
| 全增强 | 20.65% | 20.87% | -0.22pp | 28.29% | 28.82% | -0.53pp | 4,369 |
| **全增强+fast** | **21.21%** | 20.64% | **+0.57pp** | **29.58%** | 28.62% | **+0.96pp** | 3,791 |

**分析**：

1. **SQLite 上所有改进的效果均在噪声范围内**。FstatsCov 差值波动 -0.53pp ~ +1.48pp，基线 +1.48pp 可能本身是噪声上沿。

2. **multi-solve 对 SQLite 不触发**。SQLite 的关键字比较经过词法分析器的多层函数调用和状态机转换，不是简单的逐字节 `strcmp`。`extractInputByteOffset()` 无法从复杂表达式中提取单字节偏移。

3. **fast-solve 有初步正向迹象**（+0.96pp），但处于噪声边缘。需多轮实验确认。

### 3.4 选择性符号化的实际效果说明

在所有实验的日志中 `symcc_interesting=0`（Master 层 triage 中 SymCC 未产出通过全局 bitmap 检查的测试用例）。这导致：hint 偏移集合为空 → `focus_bytes` 未计算 → `SYMCC_FOCUS_BYTES` 环境变量从未被设置 → **选择性符号化实际未生效**。

全部增强的覆盖率提升来自**智能调度 + 超时增加 + multi-solve v2** 的组合，不包含选择性符号化的贡献。该机制需要更长运行时间或更宽松的 interesting 判定标准才能激活。

### 3.5 AFL-only 基线波动

以下为各实验中 AFL-only 的 ShowmapCov 值，反映单轮运行的随机性：

| 目标 | 各次值 | 均值 | 标准差 |
|------|-------|------:|------:|
| libarchive | 16.49, 16.93, 16.63, 17.04, 17.12, 16.91 | 16.85% | ±0.23pp |
| SQLite | 19.71, 20.83, 19.24, 20.15, 20.87, 20.64 | 20.24% | ±0.63pp |

### 3.6 迭代深化改进

| 改进 | 原值 | 新值 | 原理 |
|------|------|------|------|
| SymCC 超时 | 10s | 30s | 10s 过短，复杂程序路径未充分探索即被 kill |
| 调度策略 | FIFO | 深度优先（最新一代优先） | 优先探索 SymCC 的输出的输出（迭代深化） |
| 代数跟踪 | 无 | `max_generation_reached` | 量化迭代达到的深度 |
| 深度限制 | 无 | `SYMCC_MAX_DEPTH`（可配） | 防止在无效目标上无限迭代 |

超时增加可能贡献了部分覆盖率提升，但缺少"仅改超时"的对照实验。

---

## 四、结论

### 4.1 核心发现

**发现 1：深度集成可显著提升协同效率**

libarchive 上 Hybrid-AFL FstatsCov 差值从 +1.38pp 提升到 +4.56pp（净增 +3.18pp）。使用差值消除了基线波动的干扰。

**发现 2：联合求解的成功取决于模式识别精准度**

盲目联合（v1）生成量下降 30%；连续字节模式（v2）净增 +1.94pp。Z3 的能力边界决定了联合求解的可行范围。

**发现 3：SQLite 上改进效果在噪声范围内**

SQLite 基线波动 ±0.63pp，改进最大值 +0.96pp 处于噪声边缘。需多轮实验确认。

**发现 4：选择性符号化未激活**

因 `symcc_interesting=0`，hint 偏移集合为空，选择性符号化从未生效。

**发现 5：缺少消融实验**

5 项改进同时启用，无法分离各项独立贡献。后续需补充。

### 4.2 代码变更总结

| 文件 | 行数变化 | 主要改动 |
|------|------:|---------|
| `solver.cpp` | +490 行 | `fastSolve()`, `negateGroup()`, `extractInputByteOffset()`, `isConsecutiveByteComparison()`, `isSameVariableComparison()`, `isNearbyFieldComparison()`, `tryNegateGroup()` |
| `solver.h` | +25 行 | `PendingBranch` 结构体、配置字段 |
| `Runtime.cpp` | +30 行 | `SYMCC_FOCUS_BYTES` 选择性符号化 |
| `mpi_fuzzing_helper.py` | +160 行 | 智能调度、hint 收集/注入、选择性符号化传递、迭代深化 |
| **合计** | **~705 行** | |

### 4.3 新增环境变量

| 环境变量 | 默认值 | 功能 |
|---------|-------|------|
| `SYMCC_MULTI_SOLVE` | 未设置（禁用） | `=1` 连续字节联合求解（推荐）；`=2` 含实验性模式 |
| `SYMCC_FAST_SOLVE` | 未设置（禁用） | `=1` 简单约束快速求解 |
| `SYMCC_EMIT_HINTS` | 未设置（禁用） | `=1` 输出约束 hint 文件 |
| `SYMCC_FOCUS_BYTES` | 未设置（全字节） | `="start-end"` 限制符号化范围 |
| `SYMCC_TIMEOUT` | 30 | SymCC 单次执行超时（秒） |
| `SYMCC_MAX_DEPTH` | 0（无限） | 迭代深化最大代数 |

---

## 五、待完成工作

### 5.1 本期遗留

| 事项 | 说明 | 优先级 |
|------|------|:------:|
| 消融实验 | 分别测试仅启用单项改进，分离各项独立贡献 | 高 |
| 多轮统计验证 | libarchive +4.56pp 需 3-5 轮确认 | 高 |
| fast-solve 下降排查 | libarchive 全增强+fast 比全增强低 4.13pp | 高 |
| 选择性符号化激活 | 放宽触发条件或延长运行时间 | 中 |
| 更多目标测试 | 扩展到 10 个目标 | 中 |

### 5.2 中长期研究计划

| 方向 | 来源 | 预期收益 | 工作量 |
|------|------|---------|------:|
| LLM 约束求解 | Cottontail / ConcoLLMic (S&P 2026) | 结构化输入覆盖率 +30% | 1-4 周 |
| 反向路径适配 | Backsolver (TOSEM 2025) | 解决隐式信息流 | 2-3 周 |

---

## 附录 A：实验可重现命令

```bash
# 基线
python3 benchmark/run_benchmark.py \
  --targets sqlite-sqlite_fuzzer,libarchive-archive_fuzzer \
  --np-list 8 --timeout 300 --rounds 1 \
  --hybrid --afl-only --no-default --public --skip-build --no-serial --no-mpi \
  --output benchmark/benchmark_results_baseline

# 全部增强（libarchive 最优）
SYMCC_MULTI_SOLVE=1 SYMCC_TIMEOUT=30 SYMCC_EMIT_HINTS=1 \
python3 benchmark/run_benchmark.py \
  --targets libarchive-archive_fuzzer \
  --np-list 8 --timeout 300 --rounds 1 \
  --hybrid --afl-only --no-default --public --skip-build --no-serial --no-mpi \
  --output benchmark/benchmark_results_enhanced

# 全部增强 + fast-solve（SQLite 最优）
SYMCC_MULTI_SOLVE=1 SYMCC_TIMEOUT=30 SYMCC_EMIT_HINTS=1 SYMCC_FAST_SOLVE=1 \
python3 benchmark/run_benchmark.py \
  --targets sqlite-sqlite_fuzzer \
  --np-list 8 --timeout 300 --rounds 1 \
  --hybrid --afl-only --no-default --public --skip-build --no-serial --no-mpi \
  --output benchmark/benchmark_results_fastsol
```

## 附录 B：完整实验数据

### B.1 libarchive（Hybrid np=8, 300s）

| 版本 | Hybrid ShowmapCov | AFL-only ShowmapCov | **差值** | Hybrid FstatsCov | AFL-only FstatsCov | **差值** | 生成量 |
|------|------:|------:|------:|------:|------:|------:|------:|
| 基线 | 23.19% | 16.49% | **+6.70** | 17.94% | 16.56% | **+1.38** | 7,274 |
| v1 盲目 | 20.33% | 16.93% | +3.40 | 17.88% | 17.00% | +0.88 | 5,107 |
| v2 连续 | 22.87% | 16.63% | +6.24 | 20.02% | 16.70% | **+3.32** | 7,118 |
| v3 三模式 | 20.45% | 17.04% | +3.41 | 16.88% | 17.11% | -0.23 | 5,494 |
| **全增强** | **26.70%** | 17.12% | **+9.58** | **21.75%** | 17.19% | **+4.56** | 7,142 |
| 全增强+fast | 22.57% | 16.91% | +5.66 | 18.43% | 16.98% | +1.45 | 7,026 |

ShowmapCov 分母 13,760（插桩边数）；FstatsCov 分母 13,702（AFL bitmap 槽位数）。

### B.2 SQLite（Hybrid np=8, 300s）

| 版本 | Hybrid ShowmapCov | AFL-only ShowmapCov | **差值** | Hybrid FstatsCov | AFL-only FstatsCov | **差值** | 生成量 |
|------|------:|------:|------:|------:|------:|------:|------:|
| 基线 | 21.14% | 19.71% | +1.43 | 28.83% | 27.35% | **+1.48** | 4,183 |
| v1 盲目 | 20.31% | 20.83% | -0.52 | 27.91% | 28.40% | -0.49 | 4,206 |
| v2 连续 | 19.69% | 19.24% | +0.45 | 26.68% | 26.85% | -0.17 | 4,542 |
| v3 三模式 | 20.46% | 20.15% | +0.31 | 27.86% | 27.65% | +0.21 | 4,315 |
| 全增强 | 20.65% | 20.87% | -0.22 | 28.29% | 28.82% | -0.53 | 4,369 |
| **全增强+fast** | **21.21%** | 20.64% | +0.57 | **29.58%** | 28.62% | **+0.96** | 3,791 |

ShowmapCov 分母 31,680；FstatsCov 分母 20,509。分母不同的原因见"背景知识"节。