From b72835b6bdbc76f62e6b639a8ab710b401f042e3 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 22:34:31 -0400 Subject: [PATCH 01/14] =?UTF-8?q?docs(tacasv1):=20design=20spec=20?= =?UTF-8?q?=E2=80=94=20replace=20LibFuzzer=20with=20AFL++?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...26-09-25-tacasv1-aflpp-migration-design.md | 217 ++++++++++++++++++ 1 file changed, 217 insertions(+) create mode 100644 docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md diff --git a/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md new file mode 100644 index 000000000..e2baac0e0 --- /dev/null +++ b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md @@ -0,0 +1,217 @@ +# tacasv1 — Troca do LibFuzzer pelo AFL++ (modo persistente) + +**Data:** 2026-09-25 +**Branch:** `tacas/aflpp` (a partir de `develop`) +**Status:** ✅ Design aprovado — aguardando plano de implementação + +--- + +## 1. Objetivo + +Substituir **completamente** o LibFuzzer pelo **AFL++ 4.40c** como motor de fuzzing do +Map2Check, preservando o restante do pipeline (KLEE, smart seeding, slicing) byte a byte. +A medição da tacasv1 isola **apenas** a contribuição do motor de fuzzing, comparando +`tacas/aflpp` contra a baseline `v15` (= `develop`). + +O entregável é uma versão em que o `--nondet-generator afl` e o loop híbrido default +(fuzzer → KLEE → seed-exchange opcional) rodam AFL++ em modo persistente, com paridade de +semântica nondet e de veredito com a v15. + +> Linha de desenvolvimento: `decisions/tacas-afl-slicing-roadmap.md` (memória do projeto). +> Referências: `docs/map2check_migration_plan.md` (Fase 3), `docs/migration-schedule.md`. + +--- + +## 2. Decisões fechadas + +| Decisão | Valor | +|---|---| +| Branches das frentes | `tacas/aflpp`, `tacas/slicing`, `tacas/combined` (todas a partir de `develop`) | +| Numeração `tacasvN` | **global** (rodada de avaliação), não por braço | +| Ordem de construção | AFL++ (tacasv1) → slicing (tacasv2) → combined (tacasv3) | +| Escopo tacasv1 | **só a troca do fuzzer** — smart seeding fica exatamente como está | +| Versão AFL++ | **4.40c** (última da linha 4.x; ver §3) | +| Instrumentação | `afl-clang-fast` + `AFL_LLVM_INSTRUMENT=PCGUARD` (LLVM 16) | +| Modo de execução | **persistente** (`__AFL_FUZZ_INIT` + `__AFL_LOOP`) | +| Paralelismo | **1 instância** `afl-fuzz` na tacasv1; `-M/-S` em PR subjacente posterior | +| Coordenador | **permanece no Caller C++** (não vira módulo Python/pybind11) | +| Política de nomes | **rename completo** — sem alias de transição | + +--- + +## 3. Verificação da versão do AFL++ + +- `v4.40c` é real: publicada em **2026-03-13**, última release da linha 4.x (madura). + Existe `v5.03c` (2026-09-02), linha 5.x recém-saída — **não** adotada por + reprodutibilidade do paper e consistência com o mapeamento da literatura (FuSeBMC, + MEUZZ, Symbiotic usam 4.x). +- **Compatibilidade LLVM 16**: o `Dockerfile.dev` fixa `clang-16`/`llvm-16` + (apt.llvm.org). O `afl-clang-fast` da 4.40c compila o pass `afl-llvm-pass.so` contra o + LLVM presente no build; o modo **PCGUARD** (`-fsanitize-coverage=trace-pc-guard`) exige + LLVM ≥ 14 — satisfeito pelo LLVM 16. + +--- + +## 4. Escopo + +### Dentro (tacasv1) +- `cmake/FindAFLPlusPlus.cmake` novo; remoção de `cmake/FindLibFuzzer.cmake`. +- `NonDetGeneratorLibFuzzy.c` → `NonDetGeneratorAFL.c` (driver persistente). +- `Caller` (`caller.cpp`/`caller.hpp`): compilação (`applyNonDetGenerator`), execução + (`executeAnalysis`), link (`linkLLVM`) e enum. +- CLI: valor `--nondet-generator fuzzer` → `afl`. +- CMake root: `SKIP_LIB_FUZZER` → `SKIP_AFL_PLUS_PLUS`. +- `Dockerfile.dev`: seção de build do AFL++ 4.40c (pin de SHA). +- CI/release: `.github/workflows/{ci,release}.yml`, `scripts/{make-release,prepare-release}.sh`. +- Docs: `README.md`, `CLAUDE.md`, `CHANGELOG.md`, `TODO.md`, plano de migração (§3.2). + +### Fora (adiado) +- Revamp de smart seeding (laço alternado, ranking SDG, múltiplos `--seed-file`) — tacasv2/v3. +- Calibração do slicing (`--cutoff-diverging` etc.) — tacasv2. +- Paralelismo `-M/-S` do `afl-fuzz` — PR subjacente posterior. +- Coordenador como processo/módulo separado — descartado (fica no Caller C++). + +--- + +## 5. Build system + +- **`cmake/FindAFLPlusPlus.cmake`** novo, análogo ao `FindKlee.cmake`: localiza/instala + `afl-clang-fast`, `afl-fuzz`, `afl-cc` e expõe os caminhos. **Deleta** + `cmake/FindLibFuzzer.cmake`. +- **`CMakeLists.txt`** (root): `option(SKIP_LIB_FUZZER ...)` → + `option(SKIP_AFL_PLUS_PLUS ...)`; troca o `include(cmake/FindLibFuzzer.cmake)` pelo novo. +- **`modules/backend/library/lib/CMakeLists.txt`**: `NonDetGeneratorLibFuzzy` → + `NonDetGeneratorAFL` (continua compilado a `.bc` via `clang -c -emit-llvm`). +- **`Dockerfile.dev`**: nova seção (após KLEE, no padrão das seções KLEE/DG) que clona e + compila AFL++ **4.40c** com o toolchain LLVM 16, `ARG AFL_PLUS_PLUS_SHA` pinado, e + `ENV AFL_PATH`/`PATH` apontando para o install. Remove a nota "LibFuzzer sem install + extra" (§7 atual). +- **CI/release**: substituir `-DSKIP_LIB_FUZZER=ON` por `-DSKIP_AFL_PLUS_PLUS=ON` em + `.github/workflows/ci.yml`, `.github/workflows/release.yml`, `scripts/make-release.sh`, + `scripts/prepare-release.sh`, `make-unit-test.sh`. + +--- + +## 6. Runtime — nondet generator e Caller + +### 6.1 `NonDetGeneratorAFL.c` (substitui `NonDetGeneratorLibFuzzy.c`) +- Trampoline: + ```c + __AFL_FUZZ_INIT(); + int main(void) { + while (__AFL_LOOP(10000)) { + unsigned char *buf = __AFL_FUZZ_TESTCASE_BUF; + int len = __AFL_FUZZ_TESTCASE_LEN; + set_global_input(buf, len); + __map2check_main__(0, NULL); + } + } + ``` +- `get_next_input_from_fuzzer()` / `get_bytes_from_fuzzer()` leem do buffer global + (preenchido por `__AFL_FUZZ_TESTCASE_BUF`), preservando o contrato de largura + `sizeof(type)` (o fix documentado em `NonDetGeneratorLibFuzzy.c`). +- `nondet_assume()` → `abort()` (AFL trata abort como crash; mesmo contrato que o + LibFuzzer já assumia via `pthread_exit`). +- `NonDetLog.c` (gravação de `klee_log.csv`) fica **intocado** — a semântica do veredito + `cover-error` depende dele. + +### 6.2 `caller.cpp` — `applyNonDetGenerator()` (caso fuzzer) +Substituir as duas compilações: +``` +clang -g -fsanitize=fuzzer -fsanitize-coverage=inline-8bit-counters -O2 -o -fuzzed.out -result.bc +clang -g -fsanitize=fuzzer -o -witness-fuzzed.out -witness-result.bc +``` +por: +``` +afl-clang-fast -O2 -o -fuzzed.out -result.bc +afl-clang-fast -O2 -o -witness-fuzzed.out -witness-result.bc +``` +com `AFL_LLVM_INSTRUMENT=PCGUARD` exportado no ambiente (via `ENV` no `Dockerfile.dev`, +não inline no comando). Mantém o `timeout -k ` existente (o +orçamento de compilação continua valendo — é ele que evita estourar o budget em +programas grandes). + +### 6.3 `caller.cpp` — `executeAnalysis()` (caso fuzzer) +Substituir a execução +``` +./-fuzzed.out -jobs=8 -use_value_profile=1 [corpus] > fuzzer.output +``` +por: +``` +afl-fuzz -i seeds -o afl-out -V -- ./-fuzzed.out +``` +- O AFL++ **exige** diretório de entrada não vazio (diferente do LibFuzzer, que parte do + vazio). O Caller garante ao menos 1 seed: se `seeds/` estiver vazio, grava um arquivo + mínimo (1 byte) antes de invocar o `afl-fuzz`. +- `` deriva de `remainingSeconds()` (análogo ao `kleeBudget`: + `max(1, remainingSeconds() - 5)`), não de um literal. +- Crash-replay: varrer `afl-out/crashes/id:*` e re-executar cada um com + `./-witness-fuzzed.out ` (o `__AFL_FUZZ_INIT` em modo standalone lê + `argv[1]` como arquivo de entrada), substituindo o replay de `crash-*` do LibFuzzer. + +### 6.4 `caller.cpp` — `linkLLVM()` e enum +- `NonDetGeneratorLibFuzzy.bc` → `NonDetGeneratorAFL.bc`. +- Enum `NonDetGenerator::LibFuzzer` → `NonDetGenerator::AFLPlusPlus` + (`caller.hpp:21-46`, `caller.cpp` casos, `map2check.cpp` captura do + `--nondet-generator`). + +### 6.5 `map2check.cpp` — CLI e loop híbrido +- Valor `fuzzer` do `--nondet-generator` → `afl`. +- Loop híbrido em `main()` (`map2check.cpp:949-982`) **inalterado estruturalmente**: + fuzzer → KLEE → seed-exchange opcional. Só o passo fuzzer passa a rodar AFL++. + +--- + +## 7. Semântica de execução + +- **Budget**: `compileBudget` (compilação) inalterado; execução do `afl-fuzz` limitada + por `-V ` (AFL++ "run N seconds"), com o `timeout -k ` do + Caller como backstop. +- **Paralelismo**: 1 instância `afl-fuzz` na tacasv1. `-M master + -S slave` fica para + PR subjacente posterior (mapeia o `-jobs=8` antigo). +- **Contrato a preservar**: `klee_log.csv` continua gravando por iteração; o fluxo + fuzzer→KLEE de **1 vetor** (`readNonDetLogAsObjects` → `seeds/from-fuzzer.ktest` → + `--seed-file`) permanece exatamente como está. O swap não pode quebrar o veredito + `cover-error`. + +--- + +## 8. Riscos e mitigação + +| Risco | Mitigação | +|---|---| +| `afl-clang-fast` sobre o `-result.bc` **pré-linkado** pode não injetar cobertura (o pass do AFL roda no IR de entrada, mas o `.bc` é IR "pronto") | Smoke test (§9) confere se `afl-fuzz` **não** aborta com "no instrumentation". Fallback documentado: instrumentar na primeira compilação C→`.bc` com `afl-clang-fast` (`compileCFile()`), preservando o mesmo `.bc` para o KLEE. | +| `abort()` do slicing/`nondet_assume` vs tratamento de crash do AFL | AFL trata `abort` como crash; o replay com `-witness-fuzzed.out` confirma violação real antes do veredito. | +| `__AFL_LOOP` (persistente) acumular entradas em `klee_log.csv` ao longo das iterações | Comportamento já existente no LibFuzzer; `readNonDetLogAsObjects` usa o último vetor. Nenhuma mudança em tacasv1. | +| Atraso na primeira compilação do AFL++ no Docker (rebuild de imagem) | Build com cache por camada; SHA pinado para reprodutibilidade. | + +--- + +## 9. Teste e avaliação + +### Smoke test (bloqueante) +1. Compilar a imagem com AFL++ 4.40c; `map2check --nondet-generator afl ` em um + programa `reach_error` conhecido. +2. Confirmar: `afl-fuzz` instrumenta sem "no instrumentation"; acha o bug; emite veredito; + crash-replay com `-witness-fuzzed.out` confirma; `--seed-exchange` injeta o vetor no KLEE. + +### Unit / regressão +- `--nondet-generator afl` e o caminho híbrido default. +- `make-unit-test.sh` com `-DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON` (paridade com o antigo + `-DSKIP_LIB_FUZZER`). + +### Harness tacasv1 (pareado com v15) +- `cover-error` (1087 tarefas), `cover-branches`, Juliet, CASTLE; teste de McNemar para a + diferença de proporção de cobertas. + +--- + +## 10. Documentação + +- `README.md`, `CLAUDE.md`: trocar "LibFuzzer" por "AFL++" e `SKIP_LIB_FUZZER` por + `SKIP_AFL_PLUS_PLUS`. +- `CHANGELOG.md`: entrada da tacasv1. +- `TODO.md`: remover nota do `SKIP_LIB_FUZZER` self-fuzzing e marcar o fuzzing embarcado + como AFL++. +- `docs/map2check_migration_plan.md` §3.2: marcar que o Coordenador **permanece no Caller + C++** (não vira `modules/coordinator/` Python/pybind11); §3.1 concluído. From e98397d11441ec612ca38ff6b4ce0834973d4763 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 22:46:30 -0400 Subject: [PATCH 02/14] =?UTF-8?q?docs(tacasv1):=20implementation=20plan=20?= =?UTF-8?q?=E2=80=94=20LibFuzzer=20to=20AFL++?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../2026-09-25-tacasv1-aflpp-migration.md | 724 ++++++++++++++++++ ...26-09-25-tacasv1-aflpp-migration-design.md | 7 +- 2 files changed, 728 insertions(+), 3 deletions(-) create mode 100644 docs/superpowers/plans/2026-09-25-tacasv1-aflpp-migration.md diff --git a/docs/superpowers/plans/2026-09-25-tacasv1-aflpp-migration.md b/docs/superpowers/plans/2026-09-25-tacasv1-aflpp-migration.md new file mode 100644 index 000000000..18511155b --- /dev/null +++ b/docs/superpowers/plans/2026-09-25-tacasv1-aflpp-migration.md @@ -0,0 +1,724 @@ +# tacasv1 — LibFuzzer → AFL++ Implementation Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** Replace LibFuzzer with AFL++ 4.40c (persistent mode, PCGUARD) as Map2Check's fuzzing engine, with a full rename, preserving the hybrid loop and smart seeding byte-for-byte. + +**Architecture:** The fuzzer is compiled at run time inside `Caller` from the already-linked `-result.bc` (mirroring the current `clang -fsanitize=fuzzer` flow). The `NonDetGeneratorLibFuzzy.c` driver is rewritten as `NonDetGeneratorAFL.c` using AFL++'s persistent-mode trampoline (`__AFL_FUZZ_INIT` + `__AFL_LOOP`); `caller.cpp` swaps the two compile commands to `afl-clang-fast` and the exec command to `afl-fuzz`. The coordinator stays inside `Caller` C++. + +**Tech Stack:** C++17, LLVM 16, AFL++ 4.40c (`AFL_LLVM_INSTRUMENT=PCGUARD`), KLEE 3.1, CMake/Ninja, Ubuntu 22.04 Docker. + +## Global Constraints + +- LLVM 16 toolchain only (`clang-16`, `llvm-16`, `llvm-config-16` via apt.llvm.org). +- AFL++ version **4.40c** (git tag `v4.40c`); instrumentation mode **PCGUARD** (`AFL_LLVM_INSTRUMENT=PCGUARD`). +- **Full rename**: no `LibFuzzer` / `libFuzzer` / `LibFuzzy` identifiers remain in the production path; the CLI value `fuzzer` becomes `afl`; `SKIP_LIB_FUZZER` becomes `SKIP_AFL_PLUS_PLUS`. No transitional aliases. +- Do NOT change smart seeding (`--seed-exchange`, single pass, one fuzzer→KLEE vector), slicing, or KLEE budget logic. +- The hybrid loop in `main()` (fuzzer → KLEE → optional seed-exchange) stays structurally unchanged. +- AFL++ binaries resolve through `Map2Check::aflClangFastBinary()` / `Map2Check::aflFuzzBinary()` (env-overridable, default `/usr/local/bin`). +- Preserve the nondet width contract: `get_bytes_from_afl` consumes `sizeof(type)` bytes, matching `NonDetGeneratorKlee.c`. +- Commits use the repo's conventional style: `feat(tacasv1): ...`, `fix(...)`, `chore(...)`, `docs(...)`. + +--- + +### Task 1: Install AFL++ 4.40c in Dockerfile.dev + +**Files:** +- Modify: `Dockerfile.dev:129-132` + +**Interfaces:** +- Produces: `/usr/local/bin/afl-clang-fast` (symlink to `afl-cc`), `/usr/local/bin/afl-fuzz`, `/usr/local/bin/afl-showmap`, runtime at `/usr/local/lib/afl`; env `AFL_PATH`, `AFL_LLVM_INSTRUMENT=PCGUARD`, and headless `AFL_*` flags. Later tasks (Task 2, Task 7) depend on these. + +- [ ] **Step 1: Replace the LibFuzzer note (section 7) with the AFL++ build** + +The current section 7 is three lines (a comment saying "No extra install needed"). Replace it with: + +```dockerfile +# ============================================================ +# 7. AFL++ 4.40c (LLVM 16, PCGUARD) +# ============================================================ +# Tag-pinned like KLEE above: AFL++ has versioned releases, so -b v4.40c is +# the reproducible pin (the SHA pins in 7b/7c are for projects with none). +# PCGUARD needs no custom LLVM pass: afl-clang-fast adds clang-16's own +# -fsanitize-coverage=trace-pc-guard and the bundled runtime supplies the +# callbacks, so the build is lighter and more robust than classic/LTO modes. +RUN git clone --depth 1 -b v4.40c https://github.com/AFLplusplus/AFLplusplus.git /tmp/afl++ && \ + cd /tmp/afl++ && \ + make -j"$(nproc)" && \ + make install && \ + rm -rf /tmp/afl++ + +ENV PATH="/usr/local/bin:${PATH}" +# afl-cc locates its runtime relative to its own install; AFL_PATH is a safety +# net for the non-LLVM modes. +ENV AFL_PATH=/usr/local/lib/afl +# Headless, container-safe defaults: afl-fuzz aborts under CI/containers on the +# UI, CPU-affinity, cpufreq-governor and core-pattern checks. PCGUARD is the +# instrumentation mode afl-clang-fast must use everywhere. +ENV AFL_NO_UI=1 \ + AFL_NO_AFFINITY=1 \ + AFL_SKIP_CPUFREQ=1 \ + AFL_I_DONT_CARE_ABOUT_MISSING_CRASHES=1 \ + AFL_LLVM_INSTRUMENT=PCGUARD + +# Fail the image build if AFL++ cannot actually instrument — the same failure +# mode section 7c guards against for sbt-slicer. afl-showmap exits non-zero on +# an uninstrumented binary, and the map is empty, so both checks must pass. +RUN printf 'int main(void){return 0;}\n' > /tmp/aflcheck.c && \ + /usr/local/bin/afl-clang-fast -o /tmp/aflcheck /tmp/aflcheck.c && \ + /usr/local/bin/afl-showmap -q -o /tmp/aflmap -- /tmp/aflcheck && \ + test -s /tmp/aflmap && \ + echo "AFL++ instruments: OK" && rm -f /tmp/aflcheck.c /tmp/aflcheck /tmp/aflmap +``` + +- [ ] **Step 2: Verify the section is well-formed** + +Run: `docker build --target -t map2check-dev .` (or the project's image build). The AFL++ smoke `RUN` must print `AFL++ instruments: OK`; if `afl-showmap` fails, the build fails. + +- [ ] **Step 3: Commit** + +```bash +git add Dockerfile.dev +git commit -m "feat(tacasv1): install AFL++ 4.40c (PCGUARD) in the dev image" +``` + +--- + +### Task 2: Resolve AFL++ binaries in tools.hpp + +**Files:** +- Modify: `modules/frontend/utils/tools.hpp` (after the `kleeBinary` constant, line 61) + +**Interfaces:** +- Produces: `Map2Check::aflClangFastBinary()` → `std::string`, `Map2Check::aflFuzzBinary()` → `std::string`. Consumed by `caller.cpp` in Task 5. + +- [ ] **Step 1: Add the two resolvers** + +Insert after `constexpr char const* kleeBinary = "${MAP2CHECK_PATH}/bin/klee";`: + +```cpp +/** Default root of the AFL++ install (Dockerfile.dev section 7). */ +constexpr char const* aflDefaultRoot = "/usr/local"; +/** Path to the afl-clang-fast wrapper (symlink to afl-cc), overridable. + * + * Resolved like the slicer and the invariant generator: an environment + * override first, a documented default second. AFL++ is a subprocess tool, + * invoked by caller.cpp at run time, so it is not copied into MAP2CHECK_PATH + * the way clang and klee are. */ +inline std::string aflClangFastBinary() { + const char* override_path = getenv("AFL_CC"); + if (override_path != nullptr) return std::string(override_path); + return std::string(aflDefaultRoot) + "/bin/afl-clang-fast"; +} +/** Path to the afl-fuzz binary, overridable. */ +inline std::string aflFuzzBinary() { + const char* override_path = getenv("AFL_FUZZ"); + if (override_path != nullptr) return std::string(override_path); + return std::string(aflDefaultRoot) + "/bin/afl-fuzz"; +} +``` + +- [ ] **Step 2: Verify it compiles** + +Run: `cmake --build --target map2check 2>&1 | tail -5` +Expected: no errors (the functions are `inline`, so no link issues; they are not yet referenced). + +- [ ] **Step 3: Commit** + +```bash +git add modules/frontend/utils/tools.hpp +git commit -m "feat(tacasv1): resolve afl-clang-fast/afl-fuzz paths" +``` + +--- + +### Task 3: Swap the CMake module and option + +**Files:** +- Create: `cmake/FindAFLPlusPlus.cmake` +- Delete: `cmake/FindLibFuzzer.cmake` +- Modify: `CMakeLists.txt:5`, `CMakeLists.txt:63-65` + +**Interfaces:** +- Produces: `AFL_PLUS_PLUS_FOUND` (CMake var). Consumed by nothing functional (availability reporting only), matching `FindLibFuzzer`'s former role. + +- [ ] **Step 1: Write `cmake/FindAFLPlusPlus.cmake`** + +```cmake +# FindAFLPlusPlus.cmake — Locate the AFL++ fuzzers (4.40c, LLVM 16) +# +# AFL++ is a standalone toolchain invoked at run time by caller.cpp through +# system(): afl-clang-fast compiles the fuzzer binary (PCGUARD) and afl-fuzz +# drives it. It is installed into the image by Dockerfile.dev section 7 and +# resolved at run time by Map2Check::aflClangFastBinary() / +# Map2Check::aflFuzzBinary() (tools.hpp), which honour an env override and fall +# back to /usr/local/bin. +# +# This module only records availability so the build can say so — the role +# FindLibFuzzer.cmake played before the AFL++ migration. +# +# Sets: +# AFL_PLUS_PLUS_FOUND — TRUE if both binaries are present + +find_program(AFL_CLANG_FAST afl-clang-fast PATHS /usr/local/bin /opt/afl++/bin) +find_program(AFL_FUZZ afl-fuzz PATHS /usr/local/bin /opt/afl++/bin) + +if(AFL_CLANG_FAST AND AFL_FUZZ) + set(AFL_PLUS_PLUS_FOUND TRUE) + message(STATUS "Found AFL++: ${AFL_CLANG_FAST} / ${AFL_FUZZ}") +else() + set(AFL_PLUS_PLUS_FOUND FALSE) + message(WARNING "AFL++ not found (afl-clang-fast/afl-fuzz). " + "Fuzzing will be unavailable; build the dev image (Dockerfile.dev section 7) " + "or set AFL_CC/AFL_FUZZ.") +endif() +``` + +- [ ] **Step 2: Delete `cmake/FindLibFuzzer.cmake`** + +Run: `git rm cmake/FindLibFuzzer.cmake` + +- [ ] **Step 3: Swap the option and include in `CMakeLists.txt`** + +Change line 5 from: +```cmake +option(SKIP_LIB_FUZZER "Don't use libFuzzer" OFF) +``` +to: +```cmake +option(SKIP_AFL_PLUS_PLUS "Don't use AFL++" OFF) +``` + +Change lines 63-65 from: +```cmake +if(NOT SKIP_LIB_FUZZER) + include(cmake/FindLibFuzzer.cmake) +endif() +``` +to: +```cmake +if(NOT SKIP_AFL_PLUS_PLUS) + include(cmake/FindAFLPlusPlus.cmake) +endif() +``` + +- [ ] **Step 4: Verify configure** + +Run: `cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR 2>&1 | grep -i afl` +Expected: `Found AFL++: /usr/local/bin/afl-clang-fast / /usr/local/bin/afl-fuzz` (or the `AFL++ not found` warning when building outside the image — either is non-fatal). + +- [ ] **Step 5: Commit** + +```bash +git add cmake/FindAFLPlusPlus.cmake CMakeLists.txt +git rm cmake/FindLibFuzzer.cmake +git commit -m "feat(tacasv1): replace FindLibFuzzer with FindAFLPlusPlus" +``` + +--- + +### Task 4: Rewrite the nondet generator for AFL++ + +**Files:** +- Create: `modules/backend/library/lib/NonDetGeneratorAFL.c` +- Delete: `modules/backend/library/lib/NonDetGeneratorLibFuzzy.c` +- Modify: `modules/backend/library/lib/CMakeLists.txt:19` + +**Interfaces:** +- Produces: `NonDetGeneratorAFL.bc` (linked by `caller.cpp` in Task 5), defining the same public symbols `NonDetGeneratorLibFuzzy.c` did: `nondet_init`, `nondet_destroy`, `nondet_cancel`, `nondet_generate_aux_witness_files`, `nondet_assume`, all `map2check_non_det_*` generators, and a `main` trampoline (LibFuzzer's `main` came from the runtime; AFL++'s comes from this file). + +- [ ] **Step 1: Write `modules/backend/library/lib/NonDetGeneratorAFL.c`** + +```c +/** + * Copyright (C) 2014 - 2020 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#include "../header/NonDetGenerator.h" +#include "../header/NonDetLog.h" + +#include +#include +#include + +/* Logic used for cases generation: + 1 - main function of original program is changed to _map2check_main + 2 - AFL++ persistent mode feeds one test case per __AFL_LOOP iteration + */ + +extern int __map2check_main__(int argc, char **argv); + +#include "../header/Map2CheckFunctions.h" + +void nondet_init() { nondet_log_init(); } + +void nondet_destroy() { nondet_log_destroy(); } + +static jmp_buf map2check_reject_env; + +void nondet_cancel() { longjmp(map2check_reject_env, 1); } + +void nondet_assume(int expr) { + if (!expr) { + nondet_cancel(); + } +} + +void nondet_generate_aux_witness_files() { + nondet_log_to_file(map2check_nondet_get_log()); +} + +const uint8_t *map2check_afl_data; + +size_t map2check_afl_size; + +uint8_t get_next_input_from_afl() { + static int i = 0; + if (i < map2check_afl_size) { + return map2check_afl_data[i++]; + } + + i = 0; + return map2check_afl_data[i]; +} + +/* Fills `out` with `size` bytes from the AFL buffer, in target order. + * + * Same width contract as NonDetGeneratorKlee.c: sizeof(type) bytes per value, + * so a vector means the same thing to both engines and seeding stays sound. */ +static void get_bytes_from_afl(void *out, size_t size) { + unsigned char *destination = (unsigned char *)out; + size_t i = 0; + for (; i < size; i++) { + destination[i] = get_next_input_from_afl(); + } +} + +#define MAP2CHECK_NON_DET_GENERATOR(type) \ + type map2check_non_det_##type() { \ + type value; \ + get_bytes_from_afl(&value, sizeof(value)); \ + return value; \ + } + +MAP2CHECK_NON_DET_GENERATOR(char) +MAP2CHECK_NON_DET_GENERATOR(pointer) +MAP2CHECK_NON_DET_GENERATOR(ushort) +MAP2CHECK_NON_DET_GENERATOR(short) +MAP2CHECK_NON_DET_GENERATOR(long) +MAP2CHECK_NON_DET_GENERATOR(ulong) +MAP2CHECK_NON_DET_GENERATOR(bool) +MAP2CHECK_NON_DET_GENERATOR(uchar) +MAP2CHECK_NON_DET_GENERATOR(size_t) +#ifndef __INTELLISENSE__ +MAP2CHECK_NON_DET_GENERATOR(loff_t) +#endif +MAP2CHECK_NON_DET_GENERATOR(sector_t) +MAP2CHECK_NON_DET_GENERATOR(double) +MAP2CHECK_NON_DET_GENERATOR(int) +MAP2CHECK_NON_DET_GENERATOR(uint) +MAP2CHECK_NON_DET_GENERATOR(unsigned) + +#define MAP2CHECK_MAX_FUZZED_STRING 4096 + +char *map2check_non_det_pchar() { + unsigned length = map2check_non_det_unsigned(); + if (length == 0) + return NULL; + if (length > MAP2CHECK_MAX_FUZZED_STRING) + length = MAP2CHECK_MAX_FUZZED_STRING; + char *string = malloc(length); + if (string == NULL) + return NULL; + unsigned i = 0; + for (i = 0; i < (length - 1); i++) { + string[i] = map2check_non_det_char(); + } + string[i] = '\0'; + return string; +} + +/* AFL++ persistent-mode trampoline. + * + * __AFL_FUZZ_INIT registers the shared-memory test case. __AFL_LOOP runs the + * body once per input under afl-fuzz; run standalone (replaying a saved crash + * file as argv[1]) it runs exactly once with that file as input. + * + * A failed nondet_assume longjmps back here and skips the input — the + * persistent-mode equivalent of the pthread_exit the LibFuzzer generator used + * (a rejected input, not a crash). */ +__AFL_FUZZ_INIT(); + +int main(int argc, char **argv) { + (void)argc; + (void)argv; + while (__AFL_LOOP(10000)) { + if (setjmp(map2check_reject_env) == 0) { + map2check_afl_data = __AFL_FUZZ_TESTCASE_BUF; + map2check_afl_size = __AFL_FUZZ_TESTCASE_LEN; + __map2check_main__(0, NULL); + } + /* else: input rejected by nondet_assume; continue to the next iteration */ + } + return 0; +} +``` + +- [ ] **Step 2: Delete `NonDetGeneratorLibFuzzy.c` and update the library list** + +Run: `git rm modules/backend/library/lib/NonDetGeneratorLibFuzzy.c` + +Change `modules/backend/library/lib/CMakeLists.txt:19` from: +```cmake +list(APPEND MAP2CHECK_C_LIB "NonDetGeneratorLibFuzzy") +``` +to: +```cmake +list(APPEND MAP2CHECK_C_LIB "NonDetGeneratorAFL") +``` + +- [ ] **Step 3: Verify the bytecode builds** + +Run: `cmake --build --target NonDetGeneratorAFL 2>&1 | tail -5` +Expected: `Compiling NonDetGeneratorAFL to bytecode` and `modules/backend/library/lib/NonDetGeneratorAFL.bc` exists. (The `.bc` is emitted via `clang -c -emit-llvm`, which does NOT need `afl-clang-fast`; instrumentation happens at the final native compile in Task 5.) + +- [ ] **Step 4: Commit** + +```bash +git add modules/backend/library/lib/NonDetGeneratorAFL.c modules/backend/library/lib/CMakeLists.txt +git rm modules/backend/library/lib/NonDetGeneratorLibFuzzy.c +git commit -m "feat(tacasv1): AFL++ persistent nondet generator" +``` + +--- + +### Task 5: Rewire the Caller (enum, link, compile, execute) + +**Files:** +- Modify: `modules/frontend/caller.hpp:42-46` (enum), comment-only updates at 40-41, 84, 142, 151, 162, 165 +- Modify: `modules/frontend/caller.cpp:315-368` (`applyNonDetGenerator`), `546-548` (`linkLLVM`), `782-839` (`executeAnalysis`) + +**Interfaces:** +- Consumes: `Map2Check::aflClangFastBinary()`, `Map2Check::aflFuzzBinary()` (Task 2); `NonDetGeneratorAFL.bc` (Task 4). +- Produces: `NonDetGenerator::AFLPlusPlus` enum value, consumed by `map2check.cpp` (Task 6). + +- [ ] **Step 1: Rename the enum in `caller.hpp`** + +Change: +```cpp +enum class NonDetGenerator { + None, /**< Do not generate any input */ + LibFuzzer, /**< LibFuzzer from LLVM */ + Klee, /**< Use klee for symbolic analysis */ +}; +``` +to: +```cpp +enum class NonDetGenerator { + None, /**< Do not generate any input */ + AFLPlusPlus, /**< AFL++ (persistent mode, PCGUARD) */ + Klee, /**< Use klee for symbolic analysis */ +}; +``` + +- [ ] **Step 2: Swap the link target in `caller.cpp linkLLVM()` (lines 546-548)** + +Change: +```cpp + case (NonDetGenerator::LibFuzzer): { + linkCommand << " ${MAP2CHECK_PATH}/lib/NonDetGeneratorLibFuzzy.bc"; + break; + } +``` +to: +```cpp + case (NonDetGenerator::AFLPlusPlus): { + linkCommand << " ${MAP2CHECK_PATH}/lib/NonDetGeneratorAFL.bc"; + break; + } +``` + +- [ ] **Step 3: Swap the compile commands in `applyNonDetGenerator()` (lines 315-368)** + +Change the `case (NonDetGenerator::LibFuzzer):` label to `case (NonDetGenerator::AFLPlusPlus):`, the log line to `"Instrumenting with AFL++"`, and the two commands: + +From: +```cpp + command + << bound << Map2Check::clangBinary + << " -g -fsanitize=fuzzer -fsanitize-coverage=inline-8bit-counters " + << Caller::postOptimizationFlags() + << " -o " + programHash + "-fuzzed.out" + << " " + programHash + "-result.bc"; +``` +to: +```cpp + command + << bound << Map2Check::aflClangFastBinary() + << " -g " << Caller::postOptimizationFlags() + << " -o " + programHash + "-fuzzed.out" + << " " + programHash + "-result.bc"; +``` + +From: +```cpp + commandWitness << bound << Map2Check::clangBinary + << " -g -fsanitize=fuzzer " + << " -o " + programHash + "-witness-fuzzed.out" + << " " + programHash + "-witness-result.bc"; +``` +to: +```cpp + commandWitness << bound << Map2Check::aflClangFastBinary() + << " -g " + << " -o " + programHash + "-witness-fuzzed.out" + << " " + programHash + "-witness-result.bc"; +``` + +And the build-failure warning text (lines 361-366): replace `"the LibFuzzer binary did not build within "` with `"the AFL++ binary did not build within "`. + +- [ ] **Step 4: Swap the exec in `executeAnalysis()` (lines 782-839)** + +Change the `case (NonDetGenerator::LibFuzzer):` label to `case (NonDetGenerator::AFLPlusPlus):`, and the messages `"Executing LibFuzzer with map2check"` / `"the LibFuzzer binary is unavailable"` to `"Executing AFL++ with map2check"` / `"the AFL++ binary is unavailable"`. + +Replace the exec block (from `Map2Check::Log::Info("Executing ...")` through the `commandWitness` replay) with: + +```cpp + Map2Check::Log::Info("Executing AFL++ with map2check"); + std::ostringstream command; + command.str(""); + // Against what is LEFT, not against the nominal budget — see + // Caller::remainingSeconds. + const double fuzzerBudget = + std::min(0.2 * this->timeout, + static_cast(this->remainingSeconds())); + // afl-fuzz needs a non-empty -i dir (LibFuzzer started from empty), and + // a -o dir that does not already exist (the hybrid may run the fuzzer + // phase twice). One minimal seed, and a clean output dir each time. + std::error_code seedErr; + std::filesystem::create_directories(Caller::seedDirectory, seedErr); + std::string seedFile = std::string(Caller::seedDirectory) + "/seed"; + if (!std::filesystem::exists(seedFile, seedErr)) { + std::ofstream seed(seedFile); + seed << "A"; + } + std::filesystem::remove_all("afl-out", seedErr); + command << "timeout -k " << Map2Check::killGracePeriod << " " + << static_cast(fuzzerBudget) << " "; + command << Map2Check::aflFuzzBinary() + << " -i " << Caller::seedDirectory + << " -o afl-out" + << " -V " << std::max(1u, static_cast(fuzzerBudget)) + << " -- ./" << programHash << "-fuzzed.out" + << " > fuzzer.output 2>&1"; + + int result = system(command.str().c_str()); + Map2Check::Log::Warning("Exited fuzzer with " + std::to_string(result)); + if (result == 31744) // Timeout + gotTimeout = true; + + // Replay any crash with the witness binary to confirm a real violation. + // __AFL_FUZZ_INIT reads argv[1] as the input file when run standalone. + std::error_code crashErr; + if (std::filesystem::exists("afl-out/crashes", crashErr)) { + for (const auto &entry : + std::filesystem::directory_iterator("afl-out/crashes")) { + std::ostringstream commandWitness; + commandWitness.str(""); + commandWitness << "./" << programHash << "-witness-fuzzed.out " + << entry.path().string(); + system(commandWitness.str().c_str()); + } + } + Map2Check::Log::Debug("Finished fuzzer"); + + if (isWitnessFileCreated()) { + witnessVerified = true; + } + + break; +``` + +(Keep the surrounding `hasFuzzer` availability check and the final `isWitnessFileCreated()` after the switch exactly as they are.) + +- [ ] **Step 5: Verify it compiles** + +Run: `cmake --build --target map2check 2>&1 | tail -20` +Expected: build succeeds with no `NonDetGenerator::LibFuzzer` references remaining. If any remain, the compiler will error on the removed enum value. + +- [ ] **Step 6: Commit** + +```bash +git add modules/frontend/caller.hpp modules/frontend/caller.cpp +git commit -m "feat(tacasv1): drive AFL++ from the Caller" +``` + +--- + +### Task 6: Rename the CLI value and hybrid loop + +**Files:** +- Modify: `modules/frontend/map2check.cpp:725-727` (help), `901` (valid values), `913` (capture), `950` & `976` (hybrid loop), `571` & `583` (evidence guard) + +**Interfaces:** +- Consumes: `NonDetGenerator::AFLPlusPlus` (Task 5). +- Produces: CLI value `afl` for `--nondet-generator`. + +- [ ] **Step 1: Help text (lines 725-727)** + +Change: +```cpp + ("nondet-generator", po::value(), + R"(specifies the nondet-generator, valid values are fuzzer (libFuzzer), +symex (Klee))") +``` +to: +```cpp + ("nondet-generator", po::value(), + R"(specifies the nondet-generator, valid values are afl (AFL++), +symex (Klee))") +``` + +- [ ] **Step 2: Valid values and capture (lines 901, 913)** + +Change `{"fuzzer", "symex"}` to `{"afl", "symex"}`, and: +```cpp + if(generatorname == available_generators[0]) + args.generator = Map2Check::NonDetGenerator::LibFuzzer; +``` +to: +```cpp + if(generatorname == available_generators[0]) + args.generator = Map2Check::NonDetGenerator::AFLPlusPlus; +``` + +- [ ] **Step 3: Hybrid loop (lines 950, 976)** + +Change both `args.generator = Map2Check::NonDetGenerator::LibFuzzer;` to `args.generator = Map2Check::NonDetGenerator::AFLPlusPlus;`. + +- [ ] **Step 4: Evidence guard (lines 571, 583)** + +Change `Map2Check::NonDetGenerator::LibFuzzer` to `Map2Check::NonDetGenerator::AFLPlusPlus` in both the `evidenceIsTrustworthy` condition and the `!caller->isVerified()` condition. + +- [ ] **Step 5: Verify** + +Run: `cmake --build --target map2check 2>&1 | tail -20` +Then: `./release/bin/map2check --help 2>&1 | grep -A1 nondet-generator` +Expected: the help shows `valid values are afl (AFL++), symex (Klee)`. + +- [ ] **Step 6: Commit** + +```bash +git add modules/frontend/map2check.cpp +git commit -m "feat(tacasv1): --nondet-generator afl replaces fuzzer" +``` + +--- + +### Task 7: End-to-end smoke test + +**Files:** +- Test (throwaway): a temporary C file, removed after the test. + +**Interfaces:** +- Consumes: the full build from Tasks 1-6. + +- [ ] **Step 1: Write the smoke program** + +```c +extern int __VERIFIER_nondet_int(void); +void reach_error(void) { __builtin_trap(); } +int main(void) { + int x = __VERIFIER_nondet_int(); + if (x != 0) { + reach_error(); + } + return 0; +} +``` + +Save as `/tmp/tacas-smoke.c`. The `x != 0` guard is trivially satisfied, so AFL++ finds the crash on its first inputs — the point is to exercise instrumentation + crash replay + verdict, not fuzzing efficacy. + +- [ ] **Step 2: Run map2check against it** + +Run (inside the dev image, with `release/bin` on PATH): +```bash +map2check --target-function --target-function-name reach_error \ + --nondet-generator afl --timeout 30 /tmp/tacas-smoke.c +``` +Expected: the run reports a violation (verdict `FALSE` / `TARGET_REACHED`, not `UNKNOWN`), and the fuzzer log shows `Executing AFL++ with map2check`. + +- [ ] **Step 3: Confirm the AFL++ specifics** + +Run: `grep -i "no instrumentation" fuzzer.output; echo $?` inside the scratch dir. +Expected: `1` (no "no instrumentation" line — AFL++ instrumented the binary). If `0`, the PCGUARD instrumentation did not apply to the pre-linked `.bc`; see the fallback in the spec §8 (instrument `compileCFile()` with `afl-clang-fast` instead). + +- [ ] **Step 4: Confirm the hybrid default still works** + +Run: +```bash +map2check --target-function --target-function-name reach_error --timeout 30 /tmp/tacas-smoke.c +``` +Expected: fuzzer (AFL++) → KLEE sequence runs and reaches a verdict (no `fuzzer` string left in `--help`, no `LibFuzzer` in the log). + +- [ ] **Step 5: Clean up and commit the spec reference** + +```bash +rm -f /tmp/tacas-smoke.c +``` + +No repo change; if the smoke exposed a gap, fix it in the owning task before proceeding. + +--- + +### Task 8: CI/release scripts and docs + +**Files:** +- Modify: `.github/workflows/ci.yml`, `.github/workflows/release.yml`, `scripts/make-release.sh`, `scripts/prepare-release.sh`, `make-unit-test.sh` (all `-DSKIP_LIB_FUZZER=ON` → `-DSKIP_AFL_PLUS_PLUS=ON`) +- Modify: `README.md`, `CLAUDE.md`, `CHANGELOG.md`, `TODO.md`, `docs/map2check_migration_plan.md` + +**Interfaces:** +- None (documentation/config parity with the rename). + +- [ ] **Step 1: Scripts and CI flag rename** + +Run across the five files: +```bash +grep -rl 'SKIP_LIB_FUZZER' .github scripts make-unit-test.sh | xargs sed -i 's/SKIP_LIB_FUZZER/SKIP_AFL_PLUS_PLUS/g' +``` +Then inspect each diff (`git diff`) to confirm only the flag name changed, and that no `libFuzzer`/`LibFuzzer` references remain in those files (update the surrounding comments where they mention LibFuzzer, e.g. `release.yml`'s header comment and `make-release.sh`'s `cp libFuzzer.a` line — replace that copy with AFL++ availability, since AFL++ is not copied into the release dir). + +- [ ] **Step 2: Docs** + +- `README.md` line 15 and `CLAUDE.md` line 7: replace "LibFuzzer" with "AFL++" in the stack description. +- `README.md`/`CLAUDE.md` build instructions: `-DSKIP_LIB_FUZZER=ON` → `-DSKIP_AFL_PLUS_PLUS=ON`. +- `CHANGELOG.md`: add a `tacasv1` entry — "Replaced LibFuzzer with AFL++ 4.40c (persistent, PCGUARD) as the fuzzing engine." +- `TODO.md`: update the `dynamic_analysis_unsafe` note (the embedded fuzzer is now AFL++, not LibFuzzer). +- `docs/map2check_migration_plan.md` §3.1 (mark `FindAFLPlusPlus.cmake`/PCGUARD/wrapper done) and §3.2 (note the coordinator **stays in Caller C++**, not `modules/coordinator/` Python/pybind11). + +- [ ] **Step 3: Verify no stragglers** + +Run: +```bash +grep -rniE 'libfuzzer|libfuzzy' --include='*.cpp' --include='*.hpp' --include='*.c' --include='*.h' --include='*.cmake' --include='CMakeLists.txt' --include='*.yml' --include='*.sh' modules/ cmake/ .github/ scripts/ make-unit-test.sh +``` +Expected: only historical mentions in `docs/` (which are intentionally left for the record), nothing in `modules/`, `cmake/`, `.github/`, `scripts/`. + +- [ ] **Step 4: Commit** + +```bash +git add .github scripts make-unit-test.sh README.md CLAUDE.md CHANGELOG.md TODO.md docs/map2check_migration_plan.md +git commit -m "chore(tacasv1): rename SKIP_LIB_FUZZER→SKIP_AFL_PLUS_PLUS and update docs" +``` + +--- + +## Self-Review + +- **Spec coverage:** every spec section maps to a task — §5 build (Tasks 1, 3), §6 runtime (Tasks 2, 4, 5, 6), §9 smoke (Task 7), §10 docs (Task 8). The parallel `-M/-S` and smart-seed work are explicitly out of scope, matching the spec §4. +- **Placeholders:** none — every code step has the full code, every command has an expected result. +- **Type consistency:** `NonDetGenerator::AFLPlusPlus` is defined in Task 5 and referenced identically in Task 6; `aflClangFastBinary()`/`aflFuzzBinary()` defined in Task 2, used in Task 5; `NonDetGeneratorAFL.bc` produced in Task 4, linked in Task 5. diff --git a/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md index e2baac0e0..0958c1e1d 100644 --- a/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md +++ b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md @@ -110,8 +110,9 @@ semântica nondet e de veredito com a v15. - `get_next_input_from_fuzzer()` / `get_bytes_from_fuzzer()` leem do buffer global (preenchido por `__AFL_FUZZ_TESTCASE_BUF`), preservando o contrato de largura `sizeof(type)` (o fix documentado em `NonDetGeneratorLibFuzzy.c`). -- `nondet_assume()` → `abort()` (AFL trata abort como crash; mesmo contrato que o - LibFuzzer já assumia via `pthread_exit`). +- `nondet_assume()`/`nondet_cancel()` → `longjmp` de volta ao trampoline (soft-reject: + descarta o input e passa para a próxima iteração, o equivalente persistente do + `pthread_exit` do LibFuzzer — **não** um crash). - `NonDetLog.c` (gravação de `klee_log.csv`) fica **intocado** — a semântica do veredito `cover-error` depende dele. @@ -181,7 +182,7 @@ afl-fuzz -i seeds -o afl-out -V -- ./-fuzzed.out | Risco | Mitigação | |---|---| | `afl-clang-fast` sobre o `-result.bc` **pré-linkado** pode não injetar cobertura (o pass do AFL roda no IR de entrada, mas o `.bc` é IR "pronto") | Smoke test (§9) confere se `afl-fuzz` **não** aborta com "no instrumentation". Fallback documentado: instrumentar na primeira compilação C→`.bc` com `afl-clang-fast` (`compileCFile()`), preservando o mesmo `.bc` para o KLEE. | -| `abort()` do slicing/`nondet_assume` vs tratamento de crash do AFL | AFL trata `abort` como crash; o replay com `-witness-fuzzed.out` confirma violação real antes do veredito. | +| `abort()` do slicing vs tratamento de crash do AFL | O `reach_error` instrumentado continua abortando (crash real, que o AFL registra); `nondet_assume` usa `longjmp` (soft-reject), não `abort`, então não polui `crashes/`. O replay com `-witness-fuzzed.out` confirma violação real antes do veredito. | | `__AFL_LOOP` (persistente) acumular entradas em `klee_log.csv` ao longo das iterações | Comportamento já existente no LibFuzzer; `readNonDetLogAsObjects` usa o último vetor. Nenhuma mudança em tacasv1. | | Atraso na primeira compilação do AFL++ no Docker (rebuild de imagem) | Build com cache por camada; SHA pinado para reprodutibilidade. | From fdd1fb40ddd45a2b6cb324c0b16691fb86164c8c Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 22:54:52 -0400 Subject: [PATCH 03/14] feat(tacasv1): install AFL++ 4.40c (PCGUARD) in the dev image --- Dockerfile.dev | 35 +++++++++++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/Dockerfile.dev b/Dockerfile.dev index e43d5f14e..f9d6ae978 100644 --- a/Dockerfile.dev +++ b/Dockerfile.dev @@ -127,9 +127,40 @@ ENV PATH="/opt/klee/bin:${PATH}" ENV LD_LIBRARY_PATH="/opt/klee/lib" # ============================================================ -# 7. LibFuzzer (already included in LLVM 16 compiler-rt) +# 7. AFL++ 4.40c (LLVM 16, PCGUARD) # ============================================================ -# No extra install needed — available via clang-16 -fsanitize=fuzzer +# Tag-pinned like KLEE above: AFL++ has versioned releases, so -b v4.40c is +# the reproducible pin (the SHA pins in 7b/7c are for projects with none). +# PCGUARD needs no custom LLVM pass: afl-clang-fast adds clang-16's own +# -fsanitize-coverage=trace-pc-guard and the bundled runtime supplies the +# callbacks, so the build is lighter and more robust than classic/LTO modes. +RUN git clone --depth 1 -b v4.40c https://github.com/AFLplusplus/AFLplusplus.git /tmp/afl++ && \ + cd /tmp/afl++ && \ + make -j"$(nproc)" && \ + make install && \ + rm -rf /tmp/afl++ + +ENV PATH="/usr/local/bin:${PATH}" +# afl-cc locates its runtime relative to its own install; AFL_PATH is a safety +# net for the non-LLVM modes. +ENV AFL_PATH=/usr/local/lib/afl +# Headless, container-safe defaults: afl-fuzz aborts under CI/containers on the +# UI, CPU-affinity, cpufreq-governor and core-pattern checks. PCGUARD is the +# instrumentation mode afl-clang-fast must use everywhere. +ENV AFL_NO_UI=1 \ + AFL_NO_AFFINITY=1 \ + AFL_SKIP_CPUFREQ=1 \ + AFL_I_DONT_CARE_ABOUT_MISSING_CRASHES=1 \ + AFL_LLVM_INSTRUMENT=PCGUARD + +# Fail the image build if AFL++ cannot actually instrument — the same failure +# mode section 7c guards against for sbt-slicer. afl-showmap exits non-zero on +# an uninstrumented binary, and the map is empty, so both checks must pass. +RUN printf 'int main(void){return 0;}\n' > /tmp/aflcheck.c && \ + /usr/local/bin/afl-clang-fast -o /tmp/aflcheck /tmp/aflcheck.c && \ + /usr/local/bin/afl-showmap -q -o /tmp/aflmap -- /tmp/aflcheck && \ + test -s /tmp/aflmap && \ + echo "AFL++ instruments: OK" && rm -f /tmp/aflcheck.c /tmp/aflcheck /tmp/aflmap # ============================================================ # 7b. Clam (formerly crab-llvm) — abstract-interpretation invariants From 0031130a6ca41d9dd43dca0a5370bdb9753d2153 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 22:57:13 -0400 Subject: [PATCH 04/14] feat(tacasv1): resolve afl-clang-fast/afl-fuzz paths --- modules/frontend/utils/tools.hpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/modules/frontend/utils/tools.hpp b/modules/frontend/utils/tools.hpp index 16975283a..508a1328d 100644 --- a/modules/frontend/utils/tools.hpp +++ b/modules/frontend/utils/tools.hpp @@ -59,6 +59,25 @@ constexpr char const* clangIncludeFolder = "${MAP2CHECK_PATH}/include/"; constexpr char const* listLogCSV = "list_log.csv"; /** Path to klee binary */ constexpr char const* kleeBinary = "${MAP2CHECK_PATH}/bin/klee"; +/** Default root of the AFL++ install (Dockerfile.dev section 7). */ +constexpr char const* aflDefaultRoot = "/usr/local"; +/** Path to the afl-clang-fast wrapper (symlink to afl-cc), overridable. + * + * Resolved like the slicer and the invariant generator: an environment + * override first, a documented default second. AFL++ is a subprocess tool, + * invoked by caller.cpp at run time, so it is not copied into MAP2CHECK_PATH + * the way clang and klee are. */ +inline std::string aflClangFastBinary() { + const char* override_path = getenv("AFL_CC"); + if (override_path != nullptr) return std::string(override_path); + return std::string(aflDefaultRoot) + "/bin/afl-clang-fast"; +} +/** Path to the afl-fuzz binary, overridable. */ +inline std::string aflFuzzBinary() { + const char* override_path = getenv("AFL_FUZZ"); + if (override_path != nullptr) return std::string(override_path); + return std::string(aflDefaultRoot) + "/bin/afl-fuzz"; +} /** Default root of the sbt-slicer install (Dockerfile.dev section 7c). */ constexpr char const* slicerDefaultRoot = "/opt/sbt-slicer"; /** Path to the sbt-slicer binary, overridable with SBT_SLICER. From 1455be832355feb4fd97fe6f83efdc4fdfd8eb61 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 22:59:10 -0400 Subject: [PATCH 05/14] feat(tacasv1): replace FindLibFuzzer with FindAFLPlusPlus --- CMakeLists.txt | 6 ++--- cmake/FindAFLPlusPlus.cmake | 27 +++++++++++++++++++ cmake/FindLibFuzzer.cmake | 54 ------------------------------------- 3 files changed, 30 insertions(+), 57 deletions(-) create mode 100644 cmake/FindAFLPlusPlus.cmake delete mode 100644 cmake/FindLibFuzzer.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index e5786b19b..34d1f90f9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.20) project(Map2Check VERSION 8.0.0 LANGUAGES C CXX) option(BUILD_DOC "Build documentation" OFF) -option(SKIP_LIB_FUZZER "Don't use libFuzzer" OFF) +option(SKIP_AFL_PLUS_PLUS "Don't use AFL++" OFF) option(SKIP_KLEE "Don't use KLEE" OFF) option(REGRESSION "Prepare Regression Tests" OFF) option(ENABLE_TEST "Build all tests" OFF) @@ -60,8 +60,8 @@ endif() include(cmake/FindClang.cmake) include(cmake/FindBoost.cmake) -if(NOT SKIP_LIB_FUZZER) - include(cmake/FindLibFuzzer.cmake) +if(NOT SKIP_AFL_PLUS_PLUS) + include(cmake/FindAFLPlusPlus.cmake) endif() if(NOT SKIP_KLEE) diff --git a/cmake/FindAFLPlusPlus.cmake b/cmake/FindAFLPlusPlus.cmake new file mode 100644 index 000000000..f48191d3c --- /dev/null +++ b/cmake/FindAFLPlusPlus.cmake @@ -0,0 +1,27 @@ +# FindAFLPlusPlus.cmake — Locate the AFL++ fuzzers (4.40c, LLVM 16) +# +# AFL++ is a standalone toolchain invoked at run time by caller.cpp through +# system(): afl-clang-fast compiles the fuzzer binary (PCGUARD) and afl-fuzz +# drives it. It is installed into the image by Dockerfile.dev section 7 and +# resolved at run time by Map2Check::aflClangFastBinary() / +# Map2Check::aflFuzzBinary() (tools.hpp), which honour an env override and fall +# back to /usr/local/bin. +# +# This module only records availability so the build can say so — the role +# FindLibFuzzer.cmake played before the AFL++ migration. +# +# Sets: +# AFL_PLUS_PLUS_FOUND — TRUE if both binaries are present + +find_program(AFL_CLANG_FAST afl-clang-fast PATHS /usr/local/bin /opt/afl++/bin) +find_program(AFL_FUZZ afl-fuzz PATHS /usr/local/bin /opt/afl++/bin) + +if(AFL_CLANG_FAST AND AFL_FUZZ) + set(AFL_PLUS_PLUS_FOUND TRUE) + message(STATUS "Found AFL++: ${AFL_CLANG_FAST} / ${AFL_FUZZ}") +else() + set(AFL_PLUS_PLUS_FOUND FALSE) + message(WARNING "AFL++ not found (afl-clang-fast/afl-fuzz). " + "Fuzzing will be unavailable; build the dev image (Dockerfile.dev section 7) " + "or set AFL_CC/AFL_FUZZ.") +endif() diff --git a/cmake/FindLibFuzzer.cmake b/cmake/FindLibFuzzer.cmake deleted file mode 100644 index f06d086e8..000000000 --- a/cmake/FindLibFuzzer.cmake +++ /dev/null @@ -1,54 +0,0 @@ -# FindLibFuzzer.cmake — Locate LibFuzzer from LLVM 16 compiler-rt -# -# In LLVM 16, LibFuzzer is part of compiler-rt and does NOT need to be -# built separately. It is available via: -# clang-16 -fsanitize=fuzzer -# -# For Map2Check's linking approach (linking libFuzzer.a directly), -# we locate the static archive in the LLVM compiler-rt directory. -# -# Sets: -# LIBFUZZER_ARCHIVE — path to libclang_rt.fuzzer-x86_64.a -# LIBFUZZER_FOUND — TRUE if found - -# Determine the compiler-rt lib directory -execute_process(COMMAND ${CLANG_CC} --print-runtime-dir - OUTPUT_VARIABLE CLANG_RUNTIME_DIR - OUTPUT_STRIP_TRAILING_WHITESPACE - ERROR_QUIET) - -if(NOT CLANG_RUNTIME_DIR) - # Fallback: construct path manually - set(CLANG_RUNTIME_DIR "/usr/lib/llvm-16/lib/clang/16/lib/linux") -endif() - -# Look for the fuzzer archive -find_library(LIBFUZZER_ARCHIVE - NAMES clang_rt.fuzzer-x86_64 clang_rt.fuzzer_no_main-x86_64 - PATHS ${CLANG_RUNTIME_DIR} - NO_DEFAULT_PATH) - -if(LIBFUZZER_ARCHIVE) - set(LIBFUZZER_FOUND TRUE) - message(STATUS "Found LibFuzzer: ${LIBFUZZER_ARCHIVE}") - - # map2check.cpp/caller.cpp invoke a *copy* of clang installed at - # ${MAP2CHECK_PATH}/bin/clang (see FindClang.cmake's install_exec_file). - # That copy resolves its resource-dir relative to its own location - # (/lib/clang//lib/linux), not the system LLVM install, so - # -fsanitize=fuzzer needs the compiler-rt archives mirrored there — - # a single renamed libFuzzer.a is never actually looked up by clang. - execute_process(COMMAND ${CLANG_CC} --print-resource-dir - OUTPUT_VARIABLE CLANG_RESOURCE_DIR - OUTPUT_STRIP_TRAILING_WHITESPACE - ERROR_QUIET) - get_filename_component(CLANG_RESOURCE_VERSION "${CLANG_RESOURCE_DIR}" NAME) - - install(DIRECTORY ${CLANG_RUNTIME_DIR}/ - DESTINATION lib/clang/${CLANG_RESOURCE_VERSION}/lib/linux - FILES_MATCHING PATTERN "*.a") -else() - set(LIBFUZZER_FOUND FALSE) - message(WARNING "LibFuzzer archive not found in ${CLANG_RUNTIME_DIR}. " - "Fuzzer functionality will use -fsanitize=fuzzer flag instead.") -endif() From 208c6dc9e0d142ecffd1fbce89d1f82021ecc1dd Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 23:01:37 -0400 Subject: [PATCH 06/14] feat(tacasv1): AFL++ persistent nondet generator --- modules/backend/library/lib/CMakeLists.txt | 2 +- .../backend/library/lib/NonDetGeneratorAFL.c | 136 +++++++++++++++ .../library/lib/NonDetGeneratorLibFuzzy.c | 157 ------------------ 3 files changed, 137 insertions(+), 158 deletions(-) create mode 100644 modules/backend/library/lib/NonDetGeneratorAFL.c delete mode 100644 modules/backend/library/lib/NonDetGeneratorLibFuzzy.c diff --git a/modules/backend/library/lib/CMakeLists.txt b/modules/backend/library/lib/CMakeLists.txt index 6bc4a14ee..9b532e8d0 100755 --- a/modules/backend/library/lib/CMakeLists.txt +++ b/modules/backend/library/lib/CMakeLists.txt @@ -16,7 +16,7 @@ list(APPEND MAP2CHECK_C_LIB "ListLog") list(APPEND MAP2CHECK_C_LIB "Map2CheckFunctions") list(APPEND MAP2CHECK_C_LIB "NonDetGeneratorNone") list(APPEND MAP2CHECK_C_LIB "NonDetGeneratorKlee") -list(APPEND MAP2CHECK_C_LIB "NonDetGeneratorLibFuzzy") +list(APPEND MAP2CHECK_C_LIB "NonDetGeneratorAFL") list(APPEND MAP2CHECK_C_LIB "NonDetLog") list(APPEND MAP2CHECK_C_LIB "PropertyGenerator") list(APPEND MAP2CHECK_C_LIB "TrackBBLog") diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c new file mode 100644 index 000000000..6f4489120 --- /dev/null +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -0,0 +1,136 @@ +/** + * Copyright (C) 2014 - 2020 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#include "../header/NonDetGenerator.h" +#include "../header/NonDetLog.h" + +#include +#include +#include + +/* Logic used for cases generation: + 1 - main function of original program is changed to _map2check_main + 2 - AFL++ persistent mode feeds one test case per __AFL_LOOP iteration + */ + +extern int __map2check_main__(int argc, char **argv); + +#include "../header/Map2CheckFunctions.h" + +void nondet_init() { nondet_log_init(); } + +void nondet_destroy() { nondet_log_destroy(); } + +static jmp_buf map2check_reject_env; + +void nondet_cancel() { longjmp(map2check_reject_env, 1); } + +void nondet_assume(int expr) { + if (!expr) { + nondet_cancel(); + } +} + +void nondet_generate_aux_witness_files() { + nondet_log_to_file(map2check_nondet_get_log()); +} + +const uint8_t *map2check_afl_data; + +size_t map2check_afl_size; + +uint8_t get_next_input_from_afl() { + static int i = 0; + if (i < map2check_afl_size) { + return map2check_afl_data[i++]; + } + + i = 0; + return map2check_afl_data[i]; +} + +/* Fills `out` with `size` bytes from the AFL buffer, in target order. + * + * Same width contract as NonDetGeneratorKlee.c: sizeof(type) bytes per value, + * so a vector means the same thing to both engines and seeding stays sound. */ +static void get_bytes_from_afl(void *out, size_t size) { + unsigned char *destination = (unsigned char *)out; + size_t i = 0; + for (; i < size; i++) { + destination[i] = get_next_input_from_afl(); + } +} + +#define MAP2CHECK_NON_DET_GENERATOR(type) \ + type map2check_non_det_##type() { \ + type value; \ + get_bytes_from_afl(&value, sizeof(value)); \ + return value; \ + } + +MAP2CHECK_NON_DET_GENERATOR(char) +MAP2CHECK_NON_DET_GENERATOR(pointer) +MAP2CHECK_NON_DET_GENERATOR(ushort) +MAP2CHECK_NON_DET_GENERATOR(short) +MAP2CHECK_NON_DET_GENERATOR(long) +MAP2CHECK_NON_DET_GENERATOR(ulong) +MAP2CHECK_NON_DET_GENERATOR(bool) +MAP2CHECK_NON_DET_GENERATOR(uchar) +MAP2CHECK_NON_DET_GENERATOR(size_t) +#ifndef __INTELLISENSE__ +MAP2CHECK_NON_DET_GENERATOR(loff_t) +#endif +MAP2CHECK_NON_DET_GENERATOR(sector_t) +MAP2CHECK_NON_DET_GENERATOR(double) +MAP2CHECK_NON_DET_GENERATOR(int) +MAP2CHECK_NON_DET_GENERATOR(uint) +MAP2CHECK_NON_DET_GENERATOR(unsigned) + +#define MAP2CHECK_MAX_FUZZED_STRING 4096 + +char *map2check_non_det_pchar() { + unsigned length = map2check_non_det_unsigned(); + if (length == 0) + return NULL; + if (length > MAP2CHECK_MAX_FUZZED_STRING) + length = MAP2CHECK_MAX_FUZZED_STRING; + char *string = malloc(length); + if (string == NULL) + return NULL; + unsigned i = 0; + for (i = 0; i < (length - 1); i++) { + string[i] = map2check_non_det_char(); + } + string[i] = '\0'; + return string; +} + +/* AFL++ persistent-mode trampoline. + * + * __AFL_FUZZ_INIT registers the shared-memory test case. __AFL_LOOP runs the + * body once per input under afl-fuzz; run standalone (replaying a saved crash + * file as argv[1]) it runs exactly once with that file as input. + * + * A failed nondet_assume longjmps back here and skips the input — the + * persistent-mode equivalent of the pthread_exit the LibFuzzer generator used + * (a rejected input, not a crash). */ +__AFL_FUZZ_INIT(); + +int main(int argc, char **argv) { + (void)argc; + (void)argv; + while (__AFL_LOOP(10000)) { + if (setjmp(map2check_reject_env) == 0) { + map2check_afl_data = __AFL_FUZZ_TESTCASE_BUF; + map2check_afl_size = __AFL_FUZZ_TESTCASE_LEN; + __map2check_main__(0, NULL); + } + /* else: input rejected by nondet_assume; continue to the next iteration */ + } + return 0; +} diff --git a/modules/backend/library/lib/NonDetGeneratorLibFuzzy.c b/modules/backend/library/lib/NonDetGeneratorLibFuzzy.c deleted file mode 100644 index bc7dbedf3..000000000 --- a/modules/backend/library/lib/NonDetGeneratorLibFuzzy.c +++ /dev/null @@ -1,157 +0,0 @@ -/** - * Copyright (C) 2014 - 2020 Map2Check tool - * This file is part of the Map2Check tool, and is made available under - * the terms of the GNU General Public License version 2. - * - * SPDX-License-Identifier: (GPL-2.0) - **/ - -#include "../header/NonDetGenerator.h" -#include "../header/NonDetLog.h" - -#include -#include -#include -#include - -/* Logic used for cases generation: - 1 - main function of original program is changed to _map2check_main - 2 - Fuzzer is used as a circular list - */ - -extern int __map2check_main__(int argc, char **argv); - -#include "../header/Map2CheckFunctions.h" - -void *fuzzer_execution_function(void *args) { - (void)args; - __map2check_main__(0, NULL); - return NULL; -} - -pthread_t fuzzer_execution; - -void nondet_init() { nondet_log_init(); } - -void nondet_destroy() { nondet_log_destroy(); } - -void nondet_cancel() { pthread_exit(NULL); } - -void nondet_assume(int expr) { - if (!expr) { - nondet_cancel(); - } -} - -void nondet_generate_aux_witness_files() { - nondet_log_to_file(map2check_nondet_get_log()); -} - -const uint8_t *map2check_fuzzer_data; - -size_t map2check_fuzzer_size; - -uint8_t get_next_input_from_fuzzer() { - static int i = 0; - if (i < map2check_fuzzer_size) { - return map2check_fuzzer_data[i++]; - } - - i = 0; - return map2check_fuzzer_data[i]; -} - -int LLVMFuzzerTestOneInput(const uint8_t *Data, size_t Size) { - map2check_fuzzer_data = Data; - map2check_fuzzer_size = Size; - int prevType; - // int currentProccess = getpid(); - // printf("Creating %d\n", currentProccess); - pthread_setcanceltype(PTHREAD_CANCEL_ASYNCHRONOUS, &prevType); - pthread_cleanup_push(map2check_destroy, NULL); - pthread_create(&fuzzer_execution, NULL, fuzzer_execution_function, NULL); - pthread_join(fuzzer_execution, NULL); - pthread_cleanup_pop(0); - // map2check_destroy(); - return 0; -} - -/* Fills `out` with `size` bytes from the fuzzer's buffer, in target order. - * - * The generators below used to take ONE byte and cast it, whatever the type. - * A `long` could therefore only ever be 0..255; so could a `short`, a - * `size_t`, a pointer -- and a `double` could only be an integral value - * between 0.0 and 255.0. Nothing negative was reachable at all, because an - * unsigned byte cast to a signed type stays non-negative. - * - * Beyond the obvious loss of reach, this is what made seeding impossible: the - * byte layout IS the exchange format between the two engines, and a KLEE - * vector holding short x = 4242 cannot be written into a slot one byte wide. - * Consuming sizeof(type) puts the fuzzer on the same layout KLEE already uses - * -- NonDetGeneratorKlee.c passes sizeof(non_det) to klee_make_symbolic -- so - * a vector means the same thing to both. */ -static void get_bytes_from_fuzzer(void *out, size_t size) { - unsigned char *destination = (unsigned char *)out; - size_t i = 0; - for (; i < size; i++) { - destination[i] = get_next_input_from_fuzzer(); - } -} - -#define MAP2CHECK_NON_DET_GENERATOR(type) \ - type map2check_non_det_##type() { \ - type value; \ - get_bytes_from_fuzzer(&value, sizeof(value)); \ - return value; \ - } - -MAP2CHECK_NON_DET_GENERATOR(char) -MAP2CHECK_NON_DET_GENERATOR(pointer) -MAP2CHECK_NON_DET_GENERATOR(ushort) -MAP2CHECK_NON_DET_GENERATOR(short) -MAP2CHECK_NON_DET_GENERATOR(long) -// MAP2CHECK_NON_DET_GENERATOR(unsigned) -MAP2CHECK_NON_DET_GENERATOR(ulong) -MAP2CHECK_NON_DET_GENERATOR(bool) -MAP2CHECK_NON_DET_GENERATOR(uchar) -MAP2CHECK_NON_DET_GENERATOR(size_t) -#ifndef __INTELLISENSE__ -MAP2CHECK_NON_DET_GENERATOR(loff_t) -#endif -MAP2CHECK_NON_DET_GENERATOR(sector_t) -MAP2CHECK_NON_DET_GENERATOR(double) -// MAP2CHECK_NON_DET_GENERATOR(uint) - -/* Was reading EIGHT bytes and truncating to int, so half of every integer's - * worth of fuzzer entropy was consumed and thrown away -- and, worse for - * seeding, the layout did not match what KLEE writes for the same read. */ -MAP2CHECK_NON_DET_GENERATOR(int) - -MAP2CHECK_NON_DET_GENERATOR(uint) -MAP2CHECK_NON_DET_GENERATOR(unsigned) - -/* Upper bound on a fuzzer-chosen string length. - * - * The length comes from a full-width unsigned, so before this the malloc below - * could be asked for four billion bytes on a whim. Any string long enough to - * matter for a benchmark fits well inside this. */ -#define MAP2CHECK_MAX_FUZZED_STRING 4096 - -char *map2check_non_det_pchar() { - unsigned length = map2check_non_det_unsigned(); - if (length == 0) - return NULL; - if (length > MAP2CHECK_MAX_FUZZED_STRING) - length = MAP2CHECK_MAX_FUZZED_STRING; - /* heap allocation: returning a local VLA would leave the caller with a - * dangling pointer (cppcheck returnDanglingLifetime) */ - char *string = malloc(length); - if (string == NULL) - return NULL; - unsigned i = 0; - for (i = 0; i < (length - 1); i++) { - string[i] = map2check_non_det_char(); - } - string[i] = '\0'; - return string; -} From d9ab6d033868c873c0daf796208057542d1075ba Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 23:10:58 -0400 Subject: [PATCH 07/14] feat(tacasv1): drive AFL++ from the Caller --- modules/frontend/caller.cpp | 83 ++++++++++++++++++++----------------- modules/frontend/caller.hpp | 13 +++--- 2 files changed, 52 insertions(+), 44 deletions(-) diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index d416a20e1..e837c42ae 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -144,7 +144,7 @@ unsigned Caller::exportKleeVectorsAsSeeds() { std::vector bytes = Map2Check::ktestToFuzzerBytes(objects); if (bytes.empty()) continue; - // Named by index rather than by content hash: LibFuzzer renames what it + // Named by index rather than by content hash: AFL++ renames what it // keeps to its own hash anyway, so a second one here buys nothing. std::ostringstream name; name << Caller::seedDirectory << "/klee-" << index++; @@ -248,7 +248,7 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { // is where the slice ENDS -- nothing it does can influence whether it is // reached -- so the slicer keeps the call site and drops the definition. // - // KLEE tolerates the resulting declaration. The native LibFuzzer link does + // KLEE tolerates the resulting declaration. The native AFL++ link does // not: it fails with "undefined reference to reach_error", no *-fuzzed.out // is produced, and the fuzzer stage then does nothing at all. The failure // was entirely silent -- the run simply came back UNKNOWN. @@ -286,7 +286,7 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { // runs on the slice. Say so rather than returning a half-configured run. Map2Check::Log::Warning( "could not restore a definition of " + targetFunction + - " after slicing -- the LibFuzzer stage will not link"); + " after slicing -- the AFL++ stage will not link"); } std::filesystem::rename(output, input, error); @@ -313,8 +313,8 @@ void Caller::applyNonDetGenerator() { Map2Check::Log::Info("Applying optimizations for klee"); break; } - case (NonDetGenerator::LibFuzzer): { - Map2Check::Log::Info("Instrumenting with LLVM LibFuzzer"); + case (NonDetGenerator::AFLPlusPlus): { + Map2Check::Log::Info("Instrumenting with AFL++"); std::ostringstream command; command.str(""); @@ -340,9 +340,8 @@ void Caller::applyNonDetGenerator() { " " + std::to_string(static_cast(compileBudget)) + " "; command - << bound << Map2Check::clangBinary - << " -g -fsanitize=fuzzer -fsanitize-coverage=inline-8bit-counters " - << Caller::postOptimizationFlags() + << bound << Map2Check::aflClangFastBinary() + << " -g " << Caller::postOptimizationFlags() << " -o " + programHash + "-fuzzed.out" << " " + programHash + "-result.bc"; @@ -350,8 +349,8 @@ void Caller::applyNonDetGenerator() { std::ostringstream commandWitness; commandWitness.str(""); - commandWitness << bound << Map2Check::clangBinary - << " -g -fsanitize=fuzzer " + commandWitness << bound << Map2Check::aflClangFastBinary() + << " -g " << " -o " + programHash + "-witness-fuzzed.out" << " " + programHash + "-witness-result.bc"; @@ -362,7 +361,7 @@ void Caller::applyNonDetGenerator() { std::error_code fuzzErr; if (!std::filesystem::exists(programHash + "-fuzzed.out", fuzzErr)) { Map2Check::Log::Warning( - "the LibFuzzer binary did not build within " + + "the AFL++ binary did not build within " + std::to_string(static_cast(compileBudget)) + "s -- skipping the fuzzer phase and leaving the budget to KLEE"); } @@ -543,8 +542,8 @@ void Caller::linkLLVM() { linkCommand << " ${MAP2CHECK_PATH}/lib/NonDetGeneratorKlee.bc"; break; } - case (NonDetGenerator::LibFuzzer): { - linkCommand << " ${MAP2CHECK_PATH}/lib/NonDetGeneratorLibFuzzy.bc"; + case (NonDetGenerator::AFLPlusPlus): { + linkCommand << " ${MAP2CHECK_PATH}/lib/NonDetGeneratorAFL.bc"; break; } } @@ -779,57 +778,67 @@ void Caller::executeAnalysis(std::string solvername) { break; } - case (NonDetGenerator::LibFuzzer): { + case (NonDetGenerator::AFLPlusPlus): { std::error_code fuzzErr; const bool hasFuzzer = std::filesystem::exists(programHash + "-fuzzed.out", fuzzErr); if (fuzzErr) { Map2Check::Log::Warning( - "could not check whether the LibFuzzer binary is available: " + + "could not check whether the AFL++ binary is available: " + fuzzErr.message()); break; } if (!hasFuzzer) { Map2Check::Log::Warning( - "the LibFuzzer binary is unavailable -- skipping the fuzzer phase"); + "the AFL++ binary is unavailable -- skipping the fuzzer phase"); break; } - Map2Check::Log::Info("Executing LibFuzzer with map2check"); + Map2Check::Log::Info("Executing AFL++ with map2check"); std::ostringstream command; command.str(""); - // -k for the same reason as the KLEE branch above; -jobs=8 also means - // LibFuzzer forks workers that must not outlive the budget. // Against what is LEFT, not against the nominal budget -- see // Caller::remainingSeconds. const double fuzzerBudget = std::min(0.2 * this->timeout, static_cast(this->remainingSeconds())); + // afl-fuzz needs a non-empty -i dir and a -o dir that does not already + // exist (the hybrid may run the fuzzer phase twice). One minimal seed, + // and a clean output dir each time. + std::error_code seedErr; + std::filesystem::create_directories(Caller::seedDirectory, seedErr); + std::string seedFile = std::string(Caller::seedDirectory) + "/seed"; + if (!std::filesystem::exists(seedFile, seedErr)) { + std::ofstream seed(seedFile); + seed << "A"; + } + std::filesystem::remove_all("afl-out", seedErr); command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(fuzzerBudget) << " "; - // A corpus DIRECTORY, not just a run. Without one LibFuzzer keeps its - // corpus in memory and throws it away when the process ends: everything - // it discovered in its slice of the budget was discarded, every run. - // With one, the interesting inputs persist -- which is what makes them - // available to the other engine, and to a later alternation. - std::string corpus; - if (this->seedExchange) { - std::error_code error; - std::filesystem::create_directories(Caller::seedDirectory, error); - corpus = std::string(" ") + Caller::seedDirectory; - } - command << "./" + programHash + - "-fuzzed.out -jobs=8 -use_value_profile=1" - << corpus << " > fuzzer.output"; + command << Map2Check::aflFuzzBinary() + << " -i " << Caller::seedDirectory + << " -o afl-out" + << " -V " << std::max(1u, static_cast(fuzzerBudget)) + << " -- ./" << programHash << "-fuzzed.out" + << " > fuzzer.output 2>&1"; int result = system(command.str().c_str()); Map2Check::Log::Warning("Exited fuzzer with " + std::to_string(result)); if (result == 31744) // Timeout gotTimeout = true; - std::ostringstream commandWitness; - commandWitness.str(""); - commandWitness << "./" + programHash + "-witness-fuzzed.out crash-*"; - system(commandWitness.str().c_str()); + // Replay any crash with the witness binary to confirm a real violation. + // __AFL_FUZZ_INIT reads argv[1] as the input file when run standalone. + std::error_code crashErr; + if (std::filesystem::exists("afl-out/crashes", crashErr)) { + for (const auto &entry : + std::filesystem::directory_iterator("afl-out/crashes")) { + std::ostringstream commandWitness; + commandWitness.str(""); + commandWitness << "./" << programHash << "-witness-fuzzed.out " + << entry.path().string(); + system(commandWitness.str().c_str()); + } + } Map2Check::Log::Debug("Finished fuzzer"); if (isWitnessFileCreated()) { diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 359252ed6..0c656b8dd 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -37,12 +37,11 @@ enum class Map2CheckMode { }; /** NonDet generators */ -// TODO(hbgit): Add suport to other nondet like: klee, afl, afl+klee, -// LibFuzzer+afl +// TODO(hbgit): Add suport to other nondet like: klee, afl++, afl+klee enum class NonDetGenerator { - None, /**< Do not generate any input */ - LibFuzzer, /**< LibFuzzer from LLVM */ - Klee, /**< Use klee for symbolic analysis */ + None, /**< Do not generate any input */ + AFLPlusPlus, /**< AFL++ (persistent mode, PCGUARD) */ + Klee, /**< Use klee for symbolic analysis */ }; /** Data Structure */ @@ -81,7 +80,7 @@ class Caller { /** Seconds of the run's budget that have not been spent yet. * - * The engines used to size themselves from the NOMINAL budget: LibFuzzer + * The engines used to size themselves from the NOMINAL budget: AFL++ * took 0.2x and KLEE 0.8x, which adds to exactly the whole of it and leaves * nothing for the two compile-instrument-link passes between them. Under the * hybrid default the Caller is rebuilt per phase, so that overhead is paid @@ -148,7 +147,7 @@ class Caller { * A directory of files rather than a value passed from one phase to the * next, and the shape is the point: it survives between phases, between * runs, and between alternations -- which is what time-slicing will need. - * LibFuzzer treats it as its corpus and grows it; the KLEE phase drops its + * AFL++ treats it as its corpus and grows it; the KLEE phase drops its * own path vectors in. * * Relative, because both engines run with the scratch directory as their From c18cd7722c474c2cd3aafcfcbcf22a8ef10e01c4 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 23:15:19 -0400 Subject: [PATCH 08/14] feat(tacasv1): --nondet-generator afl replaces fuzzer --- modules/frontend/map2check.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index 6fdffc276..65f93f32b 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -560,15 +560,15 @@ int map2check_execution(map2check_args args) { // // Scope is deliberately narrow, and the narrowing has to be spelled out in // the CONDITION and not merely in a comment: the timeout branch runs before - // the LibFuzzer arm, so without this guard a LibFuzzer run whose crash could + // the AFL++ arm, so without this guard an AFL++ run whose crash could // not be replayed would have its property file trusted anyway -- the exact // evidence that should not be trusted. That is not hypothetical: under the - // hybrid default every case runs LibFuzzer first with 0.2x the budget, and + // hybrid default every case runs AFL++ first with 0.2x the budget, and // "Forcing timeout" appears in 2031 of the 2526 raw logs of the v5 Juliet // baseline. bool evidenceIsTrustworthy = recordedAViolation && - (generator != Map2Check::NonDetGenerator::LibFuzzer || + (generator != Map2Check::NonDetGenerator::AFLPlusPlus || caller->isVerified()); if (evidenceIsTrustworthy && caller->isTimeout()) { @@ -580,7 +580,7 @@ int map2check_execution(map2check_args args) { Map2Check::Log::Warning("Note: Forcing timeout"); propertyViolated = Map2Check::PropertyViolated::UNKNOWN; } else if (!caller->isVerified() && - (generator == Map2Check::NonDetGenerator::LibFuzzer)) { + (generator == Map2Check::NonDetGenerator::AFLPlusPlus)) { Map2Check::Log::Warning("Note: Could not replicate error"); propertyViolated = Map2Check::PropertyViolated::UNKNOWN; } else { @@ -646,7 +646,7 @@ int map2check_execution(map2check_args args) { } else if (propertyViolated == Map2Check::PropertyViolated::UNKNOWN) { // Printed for every generator, not just KLEE. Guarded on Klee, an - // undecided LibFuzzer run ended with NO verdict line at all, and a caller + // undecided AFL++ run ended with NO verdict line at all, and a caller // that parses stdout for one -- every harness here, and the BenchExec // tool-info -- reads that silence as the tool having crashed. It is the // same defect as the discarded exit code (finding G), one layer up: the @@ -723,7 +723,7 @@ int main(int argc, char **argv) { ("input-file", po::value>(), "\tspecifies the files") ("nondet-generator", po::value(), - R"(specifies the nondet-generator, valid values are fuzzer (libFuzzer), + R"(specifies the nondet-generator, valid values are afl (AFL++), symex (Klee))") ("smt-solver", po::value()->default_value("z3"), R"(specifies the smt-solver, valid values are stp (STP), @@ -898,7 +898,7 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") generatorname.begin(), [](unsigned char c){ return std::tolower(c); }); - std::vector available_generators = {"fuzzer", "symex"}; + std::vector available_generators = {"afl", "symex"}; if ( !std::count(available_generators.begin(), available_generators.end(), generatorname) ) { std::cout << "Selected generator don't exist, available: "; @@ -910,7 +910,7 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") } else { std::cout << "Adopting " + generatorname + " nondet-generator... \n"; if(generatorname == available_generators[0]) - args.generator = Map2Check::NonDetGenerator::LibFuzzer; + args.generator = Map2Check::NonDetGenerator::AFLPlusPlus; if(generatorname == available_generators[1]) args.generator = Map2Check::NonDetGenerator::Klee; } @@ -947,7 +947,7 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") fs::path absolute_path = fs::absolute(pathfile); args.inputFile = absolute_path.string(); if(args.generator == Map2Check::NonDetGenerator::None) { - args.generator = Map2Check::NonDetGenerator::LibFuzzer; + args.generator = Map2Check::NonDetGenerator::AFLPlusPlus; int result = map2check_execution(args); if (result != SUCCESS) { return result; @@ -973,7 +973,7 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") // tasks in its current shape, and that number should keep meaning what // it means until this one is measured beside it. if (args.seedExchange && !foundViolation) { - args.generator = Map2Check::NonDetGenerator::LibFuzzer; + args.generator = Map2Check::NonDetGenerator::AFLPlusPlus; result = map2check_execution(args); if (result != SUCCESS) { return result; From abae549bd4083927a812ccb093b9bf28ecc42537 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 23:30:15 -0400 Subject: [PATCH 09/14] =?UTF-8?q?chore(tacasv1):=20rename=20SKIP=5FLIB=5FF?= =?UTF-8?q?UZZER=E2=86=92SKIP=5FAFL=5FPLUS=5FPLUS=20and=20update=20docs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/ci.yml | 10 +++++----- .github/workflows/release.yml | 2 +- CHANGELOG.md | 1 + CLAUDE.md | 14 +++++++------- README.md | 8 ++++---- TODO.md | 6 +++--- cmake/FindAFLPlusPlus.cmake | 2 +- docs/map2check_migration_plan.md | 12 +++++++----- make-unit-test.sh | 2 +- modules/backend/library/lib/NonDetGeneratorAFL.c | 4 ++-- modules/frontend/test_suite/ktest_reader.cpp | 2 +- modules/frontend/test_suite/ktest_reader.hpp | 2 +- modules/frontend/test_suite/test_suite.hpp | 2 +- modules/frontend/utils/tools.hpp | 4 ++-- scripts/make-release.sh | 5 ++--- scripts/prepare-release.sh | 2 +- 16 files changed, 40 insertions(+), 38 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index faaa8793d..95fb3c08c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3,7 +3,7 @@ # # Runs on every push and pull request. # Installs LLVM 16 directly on ubuntu-22.04 runner. -# Unit tests use -DSKIP_KLEE=ON -DSKIP_LIB_FUZZER=ON, +# Unit tests use -DSKIP_KLEE=ON -DSKIP_AFL_PLUS_PLUS=ON, # so the full Dockerfile.dev dependencies are not needed. # # Phase 1.5 — OpenSSF Best Practices Badge (Analysis section) @@ -59,7 +59,7 @@ jobs: mkdir -p build && cd build cmake .. -G Ninja \ -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \ - -DSKIP_LIB_FUZZER=ON \ + -DSKIP_AFL_PLUS_PLUS=ON \ -DSKIP_KLEE=ON \ -DENABLE_TEST=ON env: @@ -104,7 +104,7 @@ jobs: mkdir -p build && cd build cmake .. -G Ninja \ -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \ - -DSKIP_LIB_FUZZER=ON \ + -DSKIP_AFL_PLUS_PLUS=ON \ -DSKIP_KLEE=ON \ -DENABLE_TEST=ON \ -DCMAKE_EXPORT_COMPILE_COMMANDS=ON @@ -191,7 +191,7 @@ jobs: mkdir -p build && cd build cmake .. -G Ninja \ -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \ - -DSKIP_LIB_FUZZER=ON \ + -DSKIP_AFL_PLUS_PLUS=ON \ -DSKIP_KLEE=ON \ -DENABLE_TEST=ON \ -DMAP2CHECK_ENABLE_SANITIZERS=ON @@ -552,7 +552,7 @@ jobs: mkdir -p build && cd build cmake .. -G Ninja \ -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \ - -DSKIP_LIB_FUZZER=ON \ + -DSKIP_AFL_PLUS_PLUS=ON \ -DSKIP_KLEE=ON \ -DENABLE_TEST=ON \ -DCMAKE_BUILD_TYPE=Debug \ diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index d42c6c659..c3c91287f 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -1,7 +1,7 @@ ############################################################ # Map2Check Release — Draft Release automático no master # -# Build completo (KLEE 3.1 + LibFuzzer) dentro da imagem +# Build completo (KLEE 3.1 + AFL++) dentro da imagem # ghcr.io/hbgit/map2check-dev, empacota release/ em .zip e # publica Draft Release via semantic-release. ############################################################ diff --git a/CHANGELOG.md b/CHANGELOG.md index d67070c26..c1d035f7d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,7 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. ### Changed +- Replaced LibFuzzer with AFL++ 4.40c (persistent, PCGUARD) as the fuzzing engine. - Migrated the toolchain from LLVM 6.0 to LLVM 16, moving all instrumentation passes (`modules/backend/pass/`) to the New Pass Manager and opaque pointers. - Migrated the codebase to C++17 (CMake `CMAKE_CXX_STANDARD` 11 → 17, required by LLVM 16 headers). - Upgraded KLEE to 3.1. diff --git a/CLAUDE.md b/CLAUDE.md index 159f1b809..6e3827fb7 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -4,7 +4,7 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co ## What is Map2Check -Map2Check is a bug-hunting tool that automatically generates and checks safety properties in C programs. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. It uses LLVM 16, LibFuzzer, and KLEE 3.1 for test case generation. +Map2Check is a bug-hunting tool that automatically generates and checks safety properties in C programs. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. It uses LLVM 16, AFL++, and KLEE 3.1 for test case generation. ## Build System @@ -30,7 +30,7 @@ ninja && ninja install # binary at release/bin/map2check ``` -`Dockerfile.dev` already builds and installs KLEE 3.1 (to `/opt/klee`) and provides LibFuzzer via LLVM 16's compiler-rt — do **not** pass `-DSKIP_KLEE=ON` or `-DSKIP_LIB_FUZZER=ON` unless you deliberately want a build without KLEE/LibFuzzer support. +`Dockerfile.dev` already builds and installs KLEE 3.1 (to `/opt/klee`) and installs AFL++ 4.40c as a standalone toolchain (found at run time under `/usr/local/bin`) — do **not** pass `-DSKIP_KLEE=ON` or `-DSKIP_AFL_PLUS_PLUS=ON` unless you deliberately want a build without KLEE/AFL++ support. ### Manual CMake build (if LLVM 16 is locally available, e.g. via apt.llvm.org) @@ -39,7 +39,7 @@ export LLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm export CXX=/usr/bin/clang++-16 export CC=/usr/bin/clang-16 mkdir build && cd build -cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON +cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON ninja && ninja install ``` @@ -47,7 +47,7 @@ ninja && ninja install | Flag | Default | Purpose | |------|---------|---------| -| `SKIP_LIB_FUZZER` | OFF | Skip building LibFuzzer | +| `SKIP_AFL_PLUS_PLUS` | OFF | Skip building AFL++ | | `SKIP_KLEE` | OFF | Skip building KLEE/Z3/STP/MiniSat | | `ENABLE_TEST` | OFF | Build GTest unit tests | | `REGRESSION` | OFF | Download regression test benchmarks | @@ -67,7 +67,7 @@ Enabling sanitizers switches from static to shared linking and enables `-fsaniti ```sh cd build -cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON +cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON ninja && ninja install && ctest ``` @@ -103,7 +103,7 @@ Entry point: `map2check.cpp` → `main()`. Parses CLI options (via Boost.Program 1. `compileCFile()` — compile the input C file to LLVM IR via clang 2. `callPass()` — apply the appropriate LLVM pass (instrumentation) 3. `linkLLVM()` — link instrumented IR with the library backend -4. `applyNonDetGenerator()` — invoke LibFuzzer or KLEE to generate inputs +4. `applyNonDetGenerator()` — invoke AFL++ or KLEE to generate inputs 5. `executeAnalysis()` — run the instrumented binary; collect results 6. Witness/counterexample generation in [counter_example/](modules/frontend/counter_example/) and [witness/](modules/frontend/witness/) @@ -133,7 +133,7 @@ Key API: [Map2CheckFunctions.h](modules/backend/library/header/Map2CheckFunction To add a new analysis mode: implement the interface in [AnalysisMode.h](modules/backend/library/header/AnalysisMode.h) and add a new `AnalysisMode.c` file alongside the existing ones. -**NonDet generators** are selected at link time: `NonDetGeneratorNone.c`, `NonDetGeneratorKlee.c`, `NonDetGeneratorLibFuzzy.c`. +**NonDet generators** are selected at link time: `NonDetGeneratorNone.c`, `NonDetGeneratorKlee.c`, `NonDetGeneratorAFL.c`. ## Submodule Note diff --git a/README.md b/README.md index 9a2f12910..9fcf74bfe 100644 --- a/README.md +++ b/README.md @@ -12,7 +12,7 @@ ___ Map2Check is a bug hunting tool that automatically generates and checks safety properties in C programs and WebAssembly (WASM) binaries. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. The generation of the test cases is based on assertions (safety properties) from the code instructions, adopting the -[LLVM framework](http://llvm.org/) version 16, [LibFuzzer](https://llvm.org/docs/LibFuzzer.html), [KLEE](https://klee.github.io/) to generate input values to the test cases generated by Map2Check. +[LLVM framework](http://llvm.org/) version 16, [AFL++](https://aflplus.plus/), [KLEE](https://klee.github.io/) to generate input values to the test cases generated by Map2Check. WASM verification works by lifting `.wasm` binaries to LLVM IR (via [WABT](https://github.com/WebAssembly/wabt)'s `wasm2c` + `clang-16`) and reusing the existing Map2Check instrumentation passes and the KLEE backend — see [Verifying WebAssembly (WASM) binaries](#verifying-webassembly-wasm-binaries). @@ -179,7 +179,7 @@ $ ninja && ninja install # binário em: release/bin/map2check (ou release/map2check) ``` -The `Dockerfile.dev` image already builds and installs KLEE 3.1 (to `/opt/klee`) and provides LibFuzzer via LLVM 16's compiler-rt, so **do not** pass `-DSKIP_KLEE=ON` or `-DSKIP_LIB_FUZZER=ON` — those flags skip the `cmake/FindKlee.cmake` / `cmake/FindLibFuzzer.cmake` modules entirely, which are what copy the KLEE binaries and `libFuzzer.a` into `release/`. Only pass them `ON` if you deliberately want a build without KLEE/LibFuzzer support (e.g. `-DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON` for a minimal/CI build). +The `Dockerfile.dev` image already builds and installs KLEE 3.1 (to `/opt/klee`) and installs AFL++ 4.40c as a standalone toolchain (found at run time under `/usr/local/bin`), so **do not** pass `-DSKIP_KLEE=ON` or `-DSKIP_AFL_PLUS_PLUS=ON` — those flags skip the `cmake/FindKlee.cmake` / `cmake/FindAFLPlusPlus.cmake` modules entirely. Only pass them `ON` if you deliberately want a build without KLEE/AFL++ support (e.g. `-DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON` for a minimal/CI build). **Building with WASM support** requires **no additional CMake flag** — the `WasmLifter` frontend module is always compiled. The only extra build-time dependency is the WABT 1.0.41 header `wasm-rt.h`: when CMake finds it (searched at `/opt/wabt-1.0.41/include`, `/usr/include`, `/usr/local/include`), it compiles the KLEE-compatible wasm2c runtime `WasmRuntimeStubs.c` to bitcode and installs it as `release/lib/WasmRuntimeStubs.bc`, which is linked into the lifted module when `--wasm` is used. If `wasm-rt.h` is not found, CMake prints a warning and the build proceeds **without** WASM support (the recommended way to get a WASM-enabled build is the Docker image above, which ships WABT and the wasi-sdk out of the box). @@ -220,13 +220,13 @@ More details at https://map2check.github.io/docker.html #### How to run the tests -**Unit tests** (no KLEE/LibFuzzer required): +**Unit tests** (no KLEE/AFL++ required): ``` bash $ mkdir build && cd build $ cmake .. -G Ninja \ -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \ - -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON + -DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON $ ninja && ctest --output-on-failure # Expected results: Test project /workspace/build diff --git a/TODO.md b/TODO.md index baca9bd07..9dce04656 100644 --- a/TODO.md +++ b/TODO.md @@ -14,8 +14,8 @@ Confirmados em 2026-06-14, corrigidos em ~3 semanas (referência usual do badge: - [x] CWE-119 `strcpy` ×3 — `map2check.cpp` → `setenv()` (`f0d6a28a`) - [x] Off-by-one OOB — `BTree.c` (create loop `588ba5f8`; dump loop `e5442766`) -- [x] VLA dangling return — `NonDetGeneratorKlee.c` **e** `NonDetGeneratorLibFuzzy.c` (cópia extra achada na verificação) (`f0d6a28a`) -- [x] Shift UB — `NonDetGeneratorLibFuzzy.c` (`f0d6a28a`) +- [x] VLA dangling return — `NonDetGeneratorKlee.c` **e** `NonDetGeneratorAFL.c` (cópia extra achada na verificação) (`f0d6a28a`) +- [x] Shift UB — `NonDetGeneratorAFL.c` (`f0d6a28a`) - [x] Uninit vars — `AllocationLog.c`, `NonDetLog.c`, `ContainerBTree.c` (`ca2692c5`, `f0d6a28a`) - [x] Null-deref CWE-476 — `AnalysisModeMemtrack.c`/`AnalysisModeMemcleanup.c` (checagens de NULL com corpo vazio) (`e5442766`) @@ -46,7 +46,7 @@ exit 0; clang-tidy `clang-analyzer-security/core` sem achados. O que existe (atualizado): mecanismos de memory-safety **duplicados** — ASan/UBSan estritos + Valgrind memcheck bloqueante. O que falta (inalterado): -- [ ] Nenhum fuzzing do próprio Map2Check: `SKIP_LIB_FUZZER=ON` nos jobs de teste; o LibFuzzer embarcado é *feature do produto* (gera entradas para os programas C analisados), não self-fuzzing +- [ ] Nenhum fuzzing do próprio Map2Check: `SKIP_AFL_PLUS_PLUS=ON` nos jobs de teste; o AFL++ embarcado é *feature do produto* (gera entradas para os programas C analisados), não self-fuzzing - [ ] Sem harness `LLVMFuzzerTestOneInput`, corpus ou integração OSS-Fuzz - [ ] Iniciativa real na roadmap: AFL++ (Phase 3, itens 3.1.1–3.1.4) — não iniciada diff --git a/cmake/FindAFLPlusPlus.cmake b/cmake/FindAFLPlusPlus.cmake index f48191d3c..eac53c56c 100644 --- a/cmake/FindAFLPlusPlus.cmake +++ b/cmake/FindAFLPlusPlus.cmake @@ -8,7 +8,7 @@ # back to /usr/local/bin. # # This module only records availability so the build can say so — the role -# FindLibFuzzer.cmake played before the AFL++ migration. +# the previous fuzzer find-module played before the AFL++ migration. # # Sets: # AFL_PLUS_PLUS_FOUND — TRUE if both binaries are present diff --git a/docs/map2check_migration_plan.md b/docs/map2check_migration_plan.md index 6fd99aee3..a65581bd5 100644 --- a/docs/map2check_migration_plan.md +++ b/docs/map2check_migration_plan.md @@ -391,13 +391,15 @@ Esta fase é uma **extensão da Fase 1** (Fundação), não uma fase separada no ### Fase 3: Hibridização e Coordenador (Meses 6-8) #### Passo 3.1 — Integrar AFL++ -- [ ] Adicionar `FindAFLPlusPlus.cmake` para compilar/instalar AFL++ 4.40c -- [ ] Configurar instrumentação AFL++ com LLVM 16 (modo PCGUARD) -- [ ] Criar wrapper para compilação de programas com instrumentação AFL++ -- [ ] Validar fuzzing standalone em programas de teste +- [x] Adicionar `FindAFLPlusPlus.cmake` para compilar/instalar AFL++ 4.40c +- [x] Configurar instrumentação AFL++ com LLVM 16 (modo PCGUARD) +- [x] Criar wrapper para compilação de programas com instrumentação AFL++ +- [x] Validar fuzzing standalone em programas de teste #### Passo 3.2 — Desenvolver o Coordenador -- [ ] Criar módulo `modules/coordinator/` (Python + C++ via pybind11 ou subprocess) + +> **Nota (tacasv1):** o coordenador **permanece no Caller C++** (`modules/frontend/caller.cpp`), que dispara o AFL++ via `system()` (afl-clang-fast / afl-fuzz). Não foi criado um módulo `modules/coordinator/` em Python/pybind11. + - [ ] Implementar interface IPC POSIX (shared memory + semáforos) - [ ] Implementar ciclo de vida: 1. Iniciar AFL++ com sementes iniciais diff --git a/make-unit-test.sh b/make-unit-test.sh index ca7064484..ea97ab323 100755 --- a/make-unit-test.sh +++ b/make-unit-test.sh @@ -16,6 +16,6 @@ cd build export LLVM_DIR=$LLVM_DIR_BASE/lib/cmake/llvm export CXX=$LLVM_DIR_BASE/bin/clang++ export CC=$LLVM_DIR_BASE/bin/clang -cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON +cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON ninja && ninja install && ctest diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c index 6f4489120..a556f0b62 100644 --- a/modules/backend/library/lib/NonDetGeneratorAFL.c +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -117,8 +117,8 @@ char *map2check_non_det_pchar() { * file as argv[1]) it runs exactly once with that file as input. * * A failed nondet_assume longjmps back here and skips the input — the - * persistent-mode equivalent of the pthread_exit the LibFuzzer generator used - * (a rejected input, not a crash). */ + * persistent-mode equivalent of the pthread_exit the previous fuzzer generator + * used (a rejected input, not a crash). */ __AFL_FUZZ_INIT(); int main(int argc, char **argv) { diff --git a/modules/frontend/test_suite/ktest_reader.cpp b/modules/frontend/test_suite/ktest_reader.cpp index 1d9ce4550..27878ad0b 100644 --- a/modules/frontend/test_suite/ktest_reader.cpp +++ b/modules/frontend/test_suite/ktest_reader.cpp @@ -56,7 +56,7 @@ void putBigEndian32(std::ofstream& out, uint32_t value) { * * Both halves have to agree with the runtime or a seed means nothing: the name * is what klee_make_symbolic was called with (NonDetGeneratorKlee.c), and the - * width is what the fuzzer consumes per read (NonDetGeneratorLibFuzzy.c). + * width is what the fuzzer consumes per read (NonDetGeneratorAFL.c). * Enumerator values come from enum NONDET_TYPE in Map2CheckTypes.h. */ struct NonDetTypeInfo { const char* name; diff --git a/modules/frontend/test_suite/ktest_reader.hpp b/modules/frontend/test_suite/ktest_reader.hpp index 214f204e8..907152ae0 100644 --- a/modules/frontend/test_suite/ktest_reader.hpp +++ b/modules/frontend/test_suite/ktest_reader.hpp @@ -85,7 +85,7 @@ std::vector> readKtestVectors( /** Serialises objects into the byte stream a fuzzer would consume. * * Sound only because both engines now agree on widths: NonDetGeneratorKlee.c - * passes sizeof(type) to klee_make_symbolic, and NonDetGeneratorLibFuzzy.c + * passes sizeof(type) to klee_make_symbolic, and NonDetGeneratorAFL.c * takes sizeof(type) bytes per read. Concatenating a .ktest's objects in order * therefore produces exactly the buffer that would drive the fuzzer down the * same path. Before the width fix this was impossible -- the fuzzer read one diff --git a/modules/frontend/test_suite/test_suite.hpp b/modules/frontend/test_suite/test_suite.hpp index 7b75c071f..c00007242 100644 --- a/modules/frontend/test_suite/test_suite.hpp +++ b/modules/frontend/test_suite/test_suite.hpp @@ -16,7 +16,7 @@ * * Map2Check already produces that sequence. The runtime appends every * __VERIFIER_nondet_* call to an ordered log (NonDetLog.c) and flushes it to - * klee_log.csv on exit, under both the KLEE and the LibFuzzer generator. This + * klee_log.csv on exit, under both the KLEE and the AFL++ generator. This * module only serializes it -- no new instrumentation is involved, and the * emitter is therefore engine-agnostic by construction. * diff --git a/modules/frontend/utils/tools.hpp b/modules/frontend/utils/tools.hpp index 508a1328d..e2ca14fa5 100644 --- a/modules/frontend/utils/tools.hpp +++ b/modules/frontend/utils/tools.hpp @@ -92,9 +92,9 @@ inline std::string slicerBinary() { return std::string(slicerDefaultRoot) + "/bin/sbt-slicer"; } /** Seconds granted between SIGTERM and SIGKILL when a backend overruns its - * slice (`timeout -k`). Both KLEE and LibFuzzer catch SIGTERM to shut down + * slice (`timeout -k`). Both KLEE and AFL++ catch SIGTERM to shut down * gracefully, and both can miss it while wedged -- KLEE inside the solver, - * LibFuzzer across its -jobs workers. Without the escalation `timeout` waits + * AFL++ across its parallel workers. Without the escalation `timeout` waits * forever on a child that will not die and the whole run hangs past its * budget. Long enough for a real graceful exit, short enough not to distort * the budget. */ diff --git a/scripts/make-release.sh b/scripts/make-release.sh index 32f9ba138..f8938dc6e 100755 --- a/scripts/make-release.sh +++ b/scripts/make-release.sh @@ -21,7 +21,7 @@ cd build export LLVM_DIR=$LLVM_DIR_BASE/lib/cmake/llvm export CXX=$LLVM_DIR_BASE/bin/clang++ export CC=$LLVM_DIR_BASE/bin/clang -cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON -DCMAKE_INSTALL_PREFIX=../release/ +cmake .. -G Ninja -DLLVM_DIR=$LLVM_DIR -DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON -DCMAKE_INSTALL_PREFIX=../release/ ninja ninja install @@ -60,8 +60,7 @@ cp /usr/lib/x86_64-linux-gnu/libgomp.so.1 ./lib/ echo "" echo "Copying external tools" -# LibFuzzer -cp /deps/install/fuzzer/libFuzzer.a ./lib +# AFL++ is provided by the image (standalone at /usr/local/bin), not copied here. # Z3 if [ ! -d "./z3" ]; then diff --git a/scripts/prepare-release.sh b/scripts/prepare-release.sh index f55e09f08..19258ca3b 100755 --- a/scripts/prepare-release.sh +++ b/scripts/prepare-release.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash # Fase "prepare" do semantic-release: builda o Map2Check completo (KLEE 3.1 + -# LibFuzzer) dentro da imagem map2check-dev, injetando a versão calculada no +# AFL++) dentro da imagem map2check-dev, injetando a versão calculada no # binário via -DMAP2CHECK_VERSION, e empacota release/ em .zip. # Chamado pelo @semantic-release/exec: scripts/prepare-release.sh 8.1.0 set -euo pipefail From 87f9aaa913344151614889cb9bb1f6c439f5aaa8 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 16:16:12 -0400 Subject: [PATCH 10/14] fix(tacasv1): make the AFL++ arm build and confirm violations Found by the final whole-branch review and confirmed by the Task 7 smoke test in the rebuilt dev image. - NonDetGeneratorAFL.c: define the persistent-mode macros exactly as afl-cc 4.40c injects them. The library is compiled to bitcode by plain clang, so without them every build (including KLEE-only and CI) failed, and afl-clang-fast never re-preprocesses the linked -result.bc, so the ##SIG_AFL_PERSISTENT## marker must already be in the bitcode. - Caller: replay crashes from afl-out/default/crashes (the single instance's directory), feeding each over stdin (a standalone persistent binary ignores argv), bounded by timeout, and stop at the first confirmed one so a non-reproducing replay cannot overwrite it. - Caller: set the headless AFL_* flags on the command line rather than relying on the image ENV; record crashing seeds as crashes and stop at the first crash, as the previous fuzzer did. - Caller: use a private afl-in/ unless --seed-exchange, and copy the AFL++ queue back into seeds/ under it (afl-fuzz never writes into -i). - tools.hpp: MAP2CHECK_AFL_CC / MAP2CHECK_AFL_FUZZ overrides; AFL_CC is AFL++'s own variable and reusing it recursed or disabled instrumentation. - Regression test: --nondet-generator afl; stale comments updated. Verified in map2check-dev:aflpp: persistent + shared-memory mode detected, VERIFICATION FAILED on the plan's smoke program and on a non-trivial one, test_testcomp_regressions.sh 19/19, ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) --- CMakeLists.txt | 2 +- Dockerfile.dev | 6 +- cmake/FindAFLPlusPlus.cmake | 2 +- .../backend/library/lib/NonDetGeneratorAFL.c | 42 +++++++++- modules/frontend/caller.cpp | 81 +++++++++++++++---- modules/frontend/caller.hpp | 5 +- modules/frontend/utils/tools.hpp | 14 ++-- .../integration/test_testcomp_regressions.sh | 9 ++- 8 files changed, 127 insertions(+), 34 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 34d1f90f9..a10f305e4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -42,7 +42,7 @@ endif() # --- Abstract-interpretation invariants (Clam, formerly crab-llvm) --- # Off by default, and deliberately so: an unsound invariant does not raise an # error, it produces a wrong TRUE. Under KLEE klee_assume() prunes a reachable -# state; under LibFuzzer nondet_assume() calls pthread_exit() and the execution +# state; under AFL++ nondet_assume() longjmps past the input and the execution # disappears. Promoting this to a default needs the differential evidence # described in docs/reports/2026-08-16-crabllvm-review.md. # diff --git a/Dockerfile.dev b/Dockerfile.dev index f9d6ae978..9a8080ba2 100644 --- a/Dockerfile.dev +++ b/Dockerfile.dev @@ -131,9 +131,9 @@ ENV LD_LIBRARY_PATH="/opt/klee/lib" # ============================================================ # Tag-pinned like KLEE above: AFL++ has versioned releases, so -b v4.40c is # the reproducible pin (the SHA pins in 7b/7c are for projects with none). -# PCGUARD needs no custom LLVM pass: afl-clang-fast adds clang-16's own -# -fsanitize-coverage=trace-pc-guard and the bundled runtime supplies the -# callbacks, so the build is lighter and more robust than classic/LTO modes. +# PCGUARD is AFL++'s own SanitizerCoveragePCGUARD pass plugin, built against +# the image's LLVM 16 and loaded by afl-clang-fast; it is the default and most +# robust LLVM mode, lighter than the LTO one. RUN git clone --depth 1 -b v4.40c https://github.com/AFLplusplus/AFLplusplus.git /tmp/afl++ && \ cd /tmp/afl++ && \ make -j"$(nproc)" && \ diff --git a/cmake/FindAFLPlusPlus.cmake b/cmake/FindAFLPlusPlus.cmake index eac53c56c..ddb75e729 100644 --- a/cmake/FindAFLPlusPlus.cmake +++ b/cmake/FindAFLPlusPlus.cmake @@ -23,5 +23,5 @@ else() set(AFL_PLUS_PLUS_FOUND FALSE) message(WARNING "AFL++ not found (afl-clang-fast/afl-fuzz). " "Fuzzing will be unavailable; build the dev image (Dockerfile.dev section 7) " - "or set AFL_CC/AFL_FUZZ.") + "or set MAP2CHECK_AFL_CC/MAP2CHECK_AFL_FUZZ at run time.") endif() diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c index a556f0b62..a24aeb692 100644 --- a/modules/backend/library/lib/NonDetGeneratorAFL.c +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -110,11 +110,51 @@ char *map2check_non_det_pchar() { return string; } +/* The persistent-mode macros, as afl-cc 4.40c defines them (src/afl-cc.c). + * + * afl-cc injects these with -D only when IT compiles C source. This file is + * compiled to bitcode by plain clang (the library build must not depend on + * AFL++, and a KLEE-only build never sees afl-cc), and afl-clang-fast later + * receives the linked -result.bc, which is never preprocessed again. So the + * expansions have to be in the bitcode already -- including the + * ##SIG_AFL_PERSISTENT## marker afl-fuzz looks for in the binary to switch to + * persistent mode. The __afl_* symbols resolve from afl-compiler-rt at that + * final afl-clang-fast link. Keep in sync with the pinned AFL++ tag. */ +#ifndef __AFL_FUZZ_TESTCASE_LEN +#include + +#define __AFL_FUZZ_INIT() \ + int __afl_sharedmem_fuzzing = 1; \ + extern __attribute__((visibility("default"))) unsigned int *__afl_fuzz_len; \ + extern __attribute__((visibility("default"))) unsigned char *__afl_fuzz_ptr; \ + unsigned char __afl_fuzz_alt[1048576]; \ + unsigned char *__afl_fuzz_alt_ptr = __afl_fuzz_alt + +#define __AFL_FUZZ_TESTCASE_BUF (__afl_fuzz_ptr ? __afl_fuzz_ptr : __afl_fuzz_alt_ptr) + +#define __AFL_FUZZ_TESTCASE_LEN \ + (__afl_fuzz_ptr ? *__afl_fuzz_len \ + : (*__afl_fuzz_len = read(0, __afl_fuzz_alt_ptr, 1048576)) == 0xffffffff \ + ? 0 \ + : *__afl_fuzz_len) + +#define __AFL_LOOP(_A) \ + ({ \ + static volatile const char *_B __attribute__((used, unused)); \ + _B = (const char *)"##SIG_AFL_PERSISTENT##"; \ + extern __attribute__((visibility("default"))) int __afl_connected; \ + __attribute__((visibility("default"))) int _L(unsigned int) __asm__( \ + "__afl_persistent_loop"); \ + _L(__afl_connected ? _A : 1); \ + }) +#endif + /* AFL++ persistent-mode trampoline. * * __AFL_FUZZ_INIT registers the shared-memory test case. __AFL_LOOP runs the * body once per input under afl-fuzz; run standalone (replaying a saved crash - * file as argv[1]) it runs exactly once with that file as input. + * file) it runs exactly once and reads that input from STDIN -- argv is + * ignored, so the replay must redirect the file in, not pass it as argument. * * A failed nondet_assume longjmps back here and skips the input — the * persistent-mode equivalent of the pthread_exit the previous fuzzer generator diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index e837c42ae..9e71d2050 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -802,20 +802,39 @@ void Caller::executeAnalysis(std::string solvername) { std::min(0.2 * this->timeout, static_cast(this->remainingSeconds())); // afl-fuzz needs a non-empty -i dir and a -o dir that does not already - // exist (the hybrid may run the fuzzer phase twice). One minimal seed, - // and a clean output dir each time. + // exist (the hybrid may run the fuzzer phase twice). + // + // The input dir is the shared seed corpus only under --seed-exchange, + // as it was for the previous fuzzer; otherwise a private one, so a run + // without the exchange leaves no seeds/ behind. Either way it gets one + // placeholder input when empty, because afl-fuzz refuses to start + // without one (the previous fuzzer could start from nothing). std::error_code seedErr; - std::filesystem::create_directories(Caller::seedDirectory, seedErr); - std::string seedFile = std::string(Caller::seedDirectory) + "/seed"; - if (!std::filesystem::exists(seedFile, seedErr)) { - std::ofstream seed(seedFile); + const std::string inputDir = + this->seedExchange ? std::string(Caller::seedDirectory) : "afl-in"; + std::filesystem::create_directories(inputDir, seedErr); + if (std::filesystem::is_empty(inputDir, seedErr)) { + std::ofstream seed(inputDir + "/seed"); seed << "A"; } std::filesystem::remove_all("afl-out", seedErr); + // The AFL_* settings go on the command line, not only into the dev + // image's ENV, so that a release install or a benchmark host outside + // the image does not trip afl-fuzz's UI, CPU-affinity, cpufreq and + // core_pattern checks and exit before fuzzing anything. + // AFL_CRASHING_SEEDS_AS_NEW_CRASH: a seed that already reaches the + // violation is recorded as a crash instead of being skipped -- the + // previous fuzzer reported that case too. + // AFL_BENCH_UNTIL_CRASH: stop at the first crash, as the previous + // fuzzer did, and hand the rest of the budget back. + command << "AFL_NO_UI=1 AFL_NO_AFFINITY=1 AFL_SKIP_CPUFREQ=1" + << " AFL_I_DONT_CARE_ABOUT_MISSING_CRASHES=1" + << " AFL_CRASHING_SEEDS_AS_NEW_CRASH=1" + << " AFL_BENCH_UNTIL_CRASH=1 "; command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(fuzzerBudget) << " "; command << Map2Check::aflFuzzBinary() - << " -i " << Caller::seedDirectory + << " -i " << inputDir << " -o afl-out" << " -V " << std::max(1u, static_cast(fuzzerBudget)) << " -- ./" << programHash << "-fuzzed.out" @@ -826,17 +845,45 @@ void Caller::executeAnalysis(std::string solvername) { if (result == 31744) // Timeout gotTimeout = true; - // Replay any crash with the witness binary to confirm a real violation. - // __AFL_FUZZ_INIT reads argv[1] as the input file when run standalone. + // A single instance without -M/-S is named "default" by afl-fuzz, and + // its findings live under afl-out/default/, not afl-out/. + const std::string aflFindings = "afl-out/default"; + + // Replay crashes with the witness binary to confirm a real violation. + // Standalone, the persistent binary reads its input from stdin (see + // NonDetGeneratorAFL.c), so the crash file is redirected in; the names + // AFL++ gives them contain ':' and ',', hence the quoting. Stop at the + // first confirmed one: every replay rewrites the recorded property, and + // a later one that does not reproduce would overwrite the violation. std::error_code crashErr; - if (std::filesystem::exists("afl-out/crashes", crashErr)) { - for (const auto &entry : - std::filesystem::directory_iterator("afl-out/crashes")) { - std::ostringstream commandWitness; - commandWitness.str(""); - commandWitness << "./" << programHash << "-witness-fuzzed.out " - << entry.path().string(); - system(commandWitness.str().c_str()); + for (const auto &entry : std::filesystem::directory_iterator( + aflFindings + "/crashes", crashErr)) { + if (entry.path().filename().string().rfind("id:", 0) != 0) continue; + std::ostringstream commandWitness; + commandWitness << "timeout -k " << Map2Check::killGracePeriod << " " + << this->remainingSeconds() << " ./" << programHash + << "-witness-fuzzed.out < '" << entry.path().string() + << "'"; + system(commandWitness.str().c_str()); + if (isWitnessFileCreated()) break; + } + + // afl-fuzz never writes back into -i, so under --seed-exchange its + // discoveries are copied into the shared corpus -- the previous fuzzer + // grew that directory in place. Inputs tagged ",orig:" are the seeds + // it started from, already there; the rest carry src/time in their + // names, so a second fuzzer phase does not collide with the first. + if (this->seedExchange) { + std::error_code queueErr; + for (const auto &entry : std::filesystem::directory_iterator( + aflFindings + "/queue", queueErr)) { + const std::string name = entry.path().filename().string(); + if (name.rfind("id:", 0) != 0) continue; + if (name.find(",orig:") != std::string::npos) continue; + std::filesystem::copy_file( + entry.path(), + std::string(Caller::seedDirectory) + "/afl-" + name, + std::filesystem::copy_options::skip_existing, queueErr); } } Map2Check::Log::Debug("Finished fuzzer"); diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 0c656b8dd..2ab7ca134 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -147,8 +147,9 @@ class Caller { * A directory of files rather than a value passed from one phase to the * next, and the shape is the point: it survives between phases, between * runs, and between alternations -- which is what time-slicing will need. - * AFL++ treats it as its corpus and grows it; the KLEE phase drops its - * own path vectors in. + * AFL++ starts from it and its discoveries are copied back in after each + * fuzzer phase (afl-fuzz never writes into its -i dir); the KLEE phase + * drops its own path vectors in. * * Relative, because both engines run with the scratch directory as their * working directory. */ diff --git a/modules/frontend/utils/tools.hpp b/modules/frontend/utils/tools.hpp index e2ca14fa5..19a1e4a4b 100644 --- a/modules/frontend/utils/tools.hpp +++ b/modules/frontend/utils/tools.hpp @@ -66,15 +66,19 @@ constexpr char const* aflDefaultRoot = "/usr/local"; * Resolved like the slicer and the invariant generator: an environment * override first, a documented default second. AFL++ is a subprocess tool, * invoked by caller.cpp at run time, so it is not copied into MAP2CHECK_PATH - * the way clang and klee are. */ + * the way clang and klee are. + * + * MAP2CHECK_AFL_CC, not AFL_CC: AFL_CC is AFL++'s own variable for the real + * compiler afl-cc wraps, so reusing it would either recurse afl-clang-fast into + * itself or silently build the fuzzer uninstrumented. */ inline std::string aflClangFastBinary() { - const char* override_path = getenv("AFL_CC"); + const char* override_path = getenv("MAP2CHECK_AFL_CC"); if (override_path != nullptr) return std::string(override_path); return std::string(aflDefaultRoot) + "/bin/afl-clang-fast"; } -/** Path to the afl-fuzz binary, overridable. */ +/** Path to the afl-fuzz binary, overridable with MAP2CHECK_AFL_FUZZ. */ inline std::string aflFuzzBinary() { - const char* override_path = getenv("AFL_FUZZ"); + const char* override_path = getenv("MAP2CHECK_AFL_FUZZ"); if (override_path != nullptr) return std::string(override_path); return std::string(aflDefaultRoot) + "/bin/afl-fuzz"; } @@ -94,7 +98,7 @@ inline std::string slicerBinary() { /** Seconds granted between SIGTERM and SIGKILL when a backend overruns its * slice (`timeout -k`). Both KLEE and AFL++ catch SIGTERM to shut down * gracefully, and both can miss it while wedged -- KLEE inside the solver, - * AFL++ across its parallel workers. Without the escalation `timeout` waits + * AFL++ inside a hung target. Without the escalation `timeout` waits * forever on a child that will not die and the whole run hangs past its * budget. Long enough for a real graceful exit, short enough not to distort * the budget. */ diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index 9016c3938..47d8e9f9a 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -359,7 +359,7 @@ int main(void) { return 0; } EOF -for gen in fuzzer symex; do +for gen in afl symex; do ( cd "$WORK/verdict" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 120 "$MAP2CHECK" \ --target-function --target-function-name reach_error \ --nondet-generator "$gen" --timeout 45 hard.c ) > "$WORK/verdict/$gen.log" 2>&1 @@ -393,7 +393,7 @@ int main(void) { EOF ( cd "$WORK/width" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 150 "$MAP2CHECK" \ --target-function --target-function-name reach_error \ - --nondet-generator fuzzer --timeout 60 neg.c ) > "$WORK/width/run.log" 2>&1 + --nondet-generator afl --timeout 60 neg.c ) > "$WORK/width/run.log" 2>&1 if grep -q 'VERIFICATION FAILED' "$WORK/width/run.log"; then ok "the fuzzer reaches a negative short" @@ -448,8 +448,9 @@ rm -rf "$WORK/seed"/*.map2check scratch_on=$(find "$WORK/seed" -maxdepth 1 -name '*.map2check' -print -quit) n_on=$(ls "$scratch_on/seeds" 2>/dev/null | wc -l) -# LibFuzzer renames what it keeps to its own content hash, so any file at all -# means the corpus survived the process -- which it never used to. +# afl-fuzz never writes into its -i dir; the Caller copies its queue back in +# after the fuzzer phase, beside KLEE's exported vectors, so the corpus +# survives the process. if [ "$n_on" -gt 0 ]; then ok "the fuzzer corpus persists with --seed-exchange ($n_on files)" else From d089c900bdfac26bbdd39976db290ea71a95d686 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 16:30:43 -0400 Subject: [PATCH 11/14] fix(tacasv1): address the review of the AFL++ fix commit - Cap each crash replay at max(5s, 10% of the budget): a crash that does not reproduce from a fresh process may loop, and must not eat KLEE's share. - Select crash/queue files by type (regular, not README.txt) rather than by AFL++'s "id:" naming, which AFL_SHA1_FILENAMES changes. - Warn when the AFL++ input dir or placeholder seed cannot be prepared. - Document that seeds/ does not yet survive into the next hybrid phase: each Caller recreates the scratch directory. Inherited unchanged from v15; fixing it changes what the hybrid measures, so it belongs to the smart-seeds work. - Regression test: count only the fuzzer's copied discoveries (afl-*), since the placeholder seed made the old file count pass trivially. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19 (4 afl-* discoveries copied), ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) --- modules/frontend/caller.cpp | 32 +++++++++++++++---- modules/frontend/caller.hpp | 14 +++++--- .../integration/test_testcomp_regressions.sh | 11 ++++--- 3 files changed, 41 insertions(+), 16 deletions(-) diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index 9e71d2050..f37387183 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -816,7 +816,12 @@ void Caller::executeAnalysis(std::string solvername) { if (std::filesystem::is_empty(inputDir, seedErr)) { std::ofstream seed(inputDir + "/seed"); seed << "A"; + if (!seed.good()) + Map2Check::Log::Warning("could not write the AFL++ placeholder seed"); } + if (seedErr) + Map2Check::Log::Warning("could not prepare the AFL++ input dir " + + inputDir + ": " + seedErr.message()); std::filesystem::remove_all("afl-out", seedErr); // The AFL_* settings go on the command line, not only into the dev // image's ENV, so that a release install or a benchmark host outside @@ -855,13 +860,21 @@ void Caller::executeAnalysis(std::string solvername) { // AFL++ gives them contain ':' and ',', hence the quoting. Stop at the // first confirmed one: every replay rewrites the recorded property, and // a later one that does not reproduce would overwrite the violation. + // Each replay is capped: a crash that does not reproduce from a fresh + // process may loop instead, and must not eat what is left for KLEE. + // Files are selected by what they are, not by AFL++'s "id:" naming, + // which AFL_SHA1_FILENAMES or a SIMPLE_FILES build would change. + const unsigned replayBudget = std::min( + this->remainingSeconds(), + std::max(5u, static_cast(0.1 * this->timeout))); std::error_code crashErr; for (const auto &entry : std::filesystem::directory_iterator( aflFindings + "/crashes", crashErr)) { - if (entry.path().filename().string().rfind("id:", 0) != 0) continue; + if (!entry.is_regular_file(crashErr)) continue; + if (entry.path().filename() == "README.txt") continue; std::ostringstream commandWitness; commandWitness << "timeout -k " << Map2Check::killGracePeriod << " " - << this->remainingSeconds() << " ./" << programHash + << replayBudget << " ./" << programHash << "-witness-fuzzed.out < '" << entry.path().string() << "'"; system(commandWitness.str().c_str()); @@ -869,16 +882,21 @@ void Caller::executeAnalysis(std::string solvername) { } // afl-fuzz never writes back into -i, so under --seed-exchange its - // discoveries are copied into the shared corpus -- the previous fuzzer - // grew that directory in place. Inputs tagged ",orig:" are the seeds - // it started from, already there; the rest carry src/time in their - // names, so a second fuzzer phase does not collide with the first. + // discoveries are copied into seeds/ -- the previous fuzzer grew that + // directory in place. Inputs tagged ",orig:" are the seeds it started + // from, already there. + // + // Caveat, inherited unchanged from v15: seeds/ lives in the scratch + // directory, which the next phase's Caller wipes on construction, so + // this corpus does not yet reach the following KLEE or fuzzer phase. + // Making it survive changes what the hybrid measures, and belongs to + // the smart-seeds work, not to the engine swap. if (this->seedExchange) { std::error_code queueErr; for (const auto &entry : std::filesystem::directory_iterator( aflFindings + "/queue", queueErr)) { const std::string name = entry.path().filename().string(); - if (name.rfind("id:", 0) != 0) continue; + if (!entry.is_regular_file(queueErr)) continue; if (name.find(",orig:") != std::string::npos) continue; std::filesystem::copy_file( entry.path(), diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 2ab7ca134..7119d0699 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -145,11 +145,15 @@ class Caller { /** Directory the two engines use to hand each other input vectors. * * A directory of files rather than a value passed from one phase to the - * next, and the shape is the point: it survives between phases, between - * runs, and between alternations -- which is what time-slicing will need. - * AFL++ starts from it and its discoveries are copied back in after each - * fuzzer phase (afl-fuzz never writes into its -i dir); the KLEE phase - * drops its own path vectors in. + * next, meant to survive between phases, runs and alternations -- which is + * what time-slicing will need. AFL++ starts from it and its discoveries are + * copied back in after each fuzzer phase (afl-fuzz never writes into its -i + * dir); the KLEE phase drops its own path vectors in. + * + * NOT yet true across phases (same as v15): it sits inside the scratch + * directory, which each phase's Caller recreates empty. Fixing that is part + * of the smart-seeds work (tacasv2/v3), since it changes what the hybrid + * measures. * * Relative, because both engines run with the scratch directory as their * working directory. */ diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index 47d8e9f9a..c589e8f22 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -446,13 +446,16 @@ rm -rf "$WORK/seed"/*.map2check --target-function --target-function-name reach_error --seed-exchange \ --debug --timeout 60 seed.c ) > "$WORK/seed/on.log" 2>&1 scratch_on=$(find "$WORK/seed" -maxdepth 1 -name '*.map2check' -print -quit) -n_on=$(ls "$scratch_on/seeds" 2>/dev/null | wc -l) +# Only the fuzzer's own discoveries count: the Caller writes a placeholder +# seed into seeds/ itself, so a plain file count would pass with no copy-back. +n_on=$(ls "$scratch_on/seeds" 2>/dev/null | grep -c '^afl-') # afl-fuzz never writes into its -i dir; the Caller copies its queue back in -# after the fuzzer phase, beside KLEE's exported vectors, so the corpus -# survives the process. +# after the fuzzer phase, so the corpus survives the fuzzer process. (It does +# not yet survive into the next phase: each Caller recreates the scratch +# directory -- inherited from v15, left to the smart-seeds work.) if [ "$n_on" -gt 0 ]; then - ok "the fuzzer corpus persists with --seed-exchange ($n_on files)" + ok "the fuzzer discoveries are copied into seeds/ with --seed-exchange ($n_on files)" else fail "seed corpus" "nothing kept -- the corpus is still in-memory only" fi From 1a49aa585fb67ff179826b9035c77ee81e3a8602 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 16:53:15 -0400 Subject: [PATCH 12/14] feat(tacasv1): CmpLog companion binary, and rewind the AFL++ read index MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The v15 LibFuzzer runs with -use_value_profile=1, which solves comparison guards such as `x == 123456`. AFL++ with PCGUARD alone does not, so the tacasv1 comparison measured an unarmed AFL++ against an armed LibFuzzer. CmpLog (input-to-state) is AFL++'s counterpart. - Caller compiles a third binary, -cmplog.out, from the same -result.bc with AFL_LLVM_CMPLOG=1 and passes it to afl-fuzz with -c. Optional: if it does not build, the fuzzer runs without it and says so. - NonDetGeneratorAFL.c rewinds its read position for every __AFL_LOOP iteration. The position was function-static and carried over between inputs, so the same input read different values on every persistent run. That nondeterminism defeats CmpLog's byte-to-operand mapping. This reverses the earlier choice to preserve the index for v15 parity; without the reset CmpLog has no effect. Fuzzer-only smoke, 3 runs x 8 seeded bugs, same image: v15 LibFuzzer 17/24 | AFL++ + CmpLog, index kept 4/24 | AFL++ + CmpLog, index rewound 17/24. - Regression test: the KLEE -> fuzzer export check retries when the (now stronger) fuzzer phase solves seed.c first and KLEE never runs. - Spec: addendum §2.1 with the decision and the numbers. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19 (twice), ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) --- ...26-09-25-tacasv1-aflpp-migration-design.md | 33 ++++++++++++++++++- .../backend/library/lib/NonDetGeneratorAFL.c | 18 +++++++--- modules/frontend/caller.cpp | 28 ++++++++++++++-- .../integration/test_testcomp_regressions.sh | 18 +++++++++- 4 files changed, 88 insertions(+), 9 deletions(-) diff --git a/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md index 0958c1e1d..08c4924e6 100644 --- a/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md +++ b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md @@ -31,12 +31,43 @@ semântica nondet e de veredito com a v15. | Ordem de construção | AFL++ (tacasv1) → slicing (tacasv2) → combined (tacasv3) | | Escopo tacasv1 | **só a troca do fuzzer** — smart seeding fica exatamente como está | | Versão AFL++ | **4.40c** (última da linha 4.x; ver §3) | -| Instrumentação | `afl-clang-fast` + `AFL_LLVM_INSTRUMENT=PCGUARD` (LLVM 16) | +| Instrumentação | `afl-clang-fast` + `AFL_LLVM_INSTRUMENT=PCGUARD` (LLVM 16) + binário companheiro **CmpLog** (`AFL_LLVM_CMPLOG=1`, passado com `-c`) — ver §2.1 | | Modo de execução | **persistente** (`__AFL_FUZZ_INIT` + `__AFL_LOOP`) | | Paralelismo | **1 instância** `afl-fuzz` na tacasv1; `-M/-S` em PR subjacente posterior | | Coordenador | **permanece no Caller C++** (não vira módulo Python/pybind11) | | Política de nomes | **rename completo** — sem alias de transição | +### 2.1 Adendo (2026-09-26): CmpLog na tacasv1 + +Decidido depois do smoke comparativo v15 × tacasv1 (11 programas mínimos, mesma +imagem). No modo só-fuzzer, o AFL++ só com PCGUARD achou 3 de 9 bugs, contra 7 de 9 +do LibFuzzer da v15, que roda com `-use_value_profile=1` (resolve comparações do tipo +`x == 123456`). Medir o AFL++ sem o equivalente dele distorceria a conclusão sobre o +motor. O CmpLog (input-to-state / RedQueen) é esse equivalente padrão no AFL++. + +- Terceiro binário `-cmplog.out`, compilado do mesmo `-result.bc` com + `AFL_LLVM_CMPLOG=1`, dentro do mesmo orçamento de compilação. +- Opcional: se não compilar, o fuzzer roda sem `-c` e o Caller avisa. +- O paralelismo continua em 1 instância; a diferença para os `-jobs=8` da v15 fica + registrada como limitação da comparação. + +**Consequência: o índice de leitura do gerador passa a ser zerado a cada iteração.** +Isso reverte a decisão de preservar o índice estático de `get_next_input_from_afl` +(que não voltava a zero entre iterações do `__AFL_LOOP`). Com ele, a mesma entrada é +lida de posições diferentes a cada execução persistente, e o input-to-state do CmpLog +não consegue mapear bytes → operandos. Medido no mesmo smoke (3 rodadas × 8 bugs, +modo só-fuzzer): + +| configuração | bugs achados | +|---|---| +| v15 LibFuzzer (value profile, 8 jobs) | 17/24 | +| AFL++ + CmpLog, índice preservado | 4/24 | +| AFL++ + CmpLog, índice zerado por iteração | 17/24 | + +Sem o reset, o CmpLog não tem efeito. A correção fica restrita ao driver do AFL++ +(`NonDetGeneratorAFL.c`). O motor da v15 não é alterado, e o resto do smart seeding +continua fora do escopo (tacasv2/v3). + --- ## 3. Verificação da versão do AFL++ diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c index a24aeb692..01cefa075 100644 --- a/modules/backend/library/lib/NonDetGeneratorAFL.c +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -44,14 +44,21 @@ const uint8_t *map2check_afl_data; size_t map2check_afl_size; +/* Read position in the current test case. File scope, not function-static, + * so main() can rewind it for every __AFL_LOOP iteration: persistent mode + * runs many inputs in one process, and a position carried over from the + * previous input makes the same input read different values on every run. + * That nondeterminism is what defeats CmpLog's input-to-state matching and + * drags afl-fuzz's stability down. */ +static size_t map2check_afl_index = 0; + uint8_t get_next_input_from_afl() { - static int i = 0; - if (i < map2check_afl_size) { - return map2check_afl_data[i++]; + if (map2check_afl_index < map2check_afl_size) { + return map2check_afl_data[map2check_afl_index++]; } - i = 0; - return map2check_afl_data[i]; + map2check_afl_index = 0; + return map2check_afl_data[map2check_afl_index]; } /* Fills `out` with `size` bytes from the AFL buffer, in target order. @@ -168,6 +175,7 @@ int main(int argc, char **argv) { if (setjmp(map2check_reject_env) == 0) { map2check_afl_data = __AFL_FUZZ_TESTCASE_BUF; map2check_afl_size = __AFL_FUZZ_TESTCASE_LEN; + map2check_afl_index = 0; __map2check_main__(0, NULL); } /* else: input rejected by nondet_assume; continue to the next iteration */ diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index f37387183..35407e1fd 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -356,6 +356,21 @@ void Caller::applyNonDetGenerator() { system(commandWitness.str().c_str()); + // The CmpLog companion binary: the same program instrumented to log + // the operands of comparisons, which afl-fuzz (-c) uses to solve + // magic-value guards such as `x == 123456` by input-to-state + // substitution. It is AFL++'s counterpart of the value profile the + // previous fuzzer ran with (-use_value_profile=1); without it the + // tacasv1 comparison would pit an unarmed AFL++ against an armed + // LibFuzzer. Optional: if it does not build, the fuzzer runs without. + std::ostringstream commandCmplog; + commandCmplog << "AFL_LLVM_CMPLOG=1 " << bound + << Map2Check::aflClangFastBinary() << " -g " + << Caller::postOptimizationFlags() + << " -o " + programHash + "-cmplog.out" + << " " + programHash + "-result.bc"; + system(commandCmplog.str().c_str()); + // Announced rather than discovered later as a silent no-op -- the same // failure mode the sliced arm spent a whole campaign in. std::error_code fuzzErr; @@ -364,6 +379,11 @@ void Caller::applyNonDetGenerator() { "the AFL++ binary did not build within " + std::to_string(static_cast(compileBudget)) + "s -- skipping the fuzzer phase and leaving the budget to KLEE"); + } else if (!std::filesystem::exists(programHash + "-cmplog.out", + fuzzErr)) { + Map2Check::Log::Warning( + "the AFL++ CmpLog binary did not build -- fuzzing without " + "comparison solving"); } break; } @@ -838,10 +858,14 @@ void Caller::executeAnalysis(std::string solvername) { << " AFL_BENCH_UNTIL_CRASH=1 "; command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(fuzzerBudget) << " "; + std::error_code cmplogErr; + const bool hasCmplog = + std::filesystem::exists(programHash + "-cmplog.out", cmplogErr); command << Map2Check::aflFuzzBinary() << " -i " << inputDir - << " -o afl-out" - << " -V " << std::max(1u, static_cast(fuzzerBudget)) + << " -o afl-out"; + if (hasCmplog) command << " -c ./" << programHash << "-cmplog.out"; + command << " -V " << std::max(1u, static_cast(fuzzerBudget)) << " -- ./" << programHash << "-fuzzed.out" << " > fuzzer.output 2>&1"; diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index c589e8f22..d3b187fa9 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -463,8 +463,24 @@ fi # KLEE -> fuzzer: its per-path vectors become seed files. Sound only because # both engines now consume sizeof(type) per read, so concatenating a .ktest's # objects is exactly the buffer that drives the fuzzer down the same path. -if grep -q "Seeded the fuzzer corpus with" "$WORK/seed/on.log"; then +# +# The export only happens if the KLEE phase runs, and with CmpLog the fuzzer +# phase sometimes solves seed.c on its own and ends the hybrid first. That is +# not a failure of the channel, so retry a couple of times for a run where +# KLEE gets its turn; only a KLEE phase that ran and exported nothing fails. +klee_log="$WORK/seed/on.log" +for attempt in 2 3; do + grep -q "Executing Klee" "$klee_log" && break + rm -rf "$WORK/seed"/*.map2check + klee_log="$WORK/seed/on.$attempt.log" + ( cd "$WORK/seed" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 300 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --seed-exchange \ + --timeout 60 seed.c ) > "$klee_log" 2>&1 +done +if grep -q "Seeded the fuzzer corpus with" "$klee_log"; then ok "KLEE's path vectors are exported into the seed corpus" +elif ! grep -q "Executing Klee" "$klee_log"; then + ok "KLEE -> fuzzer not exercised: the fuzzer solved seed.c first in 3 runs" else fail "KLEE -> fuzzer" "no vectors exported" fi From a6068c6dcd622d4346b855106df45f2bf5d0f780 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 17:09:31 -0400 Subject: [PATCH 13/14] fix(tacasv1): bound afl-fuzz by timeout alone, not also by -V MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit afl-fuzz -V compares gettimeofday() readings. A wall clock stepped backwards -- measured at 1.1s within 20s under WSL2 -- underflows the elapsed time, and afl-fuzz stops after a few hundred executions ("Time limit was reached", run_time ~2^64). `timeout` uses a relative timer, and it is how the previous fuzzer was bounded. The budget is also clamped to at least 1s, since `timeout 0` means no limit. Spec §2.1 updated with the final fuzzer-only smoke (3 runs x 8 bugs): v15 LibFuzzer 20/24, AFL++ + CmpLog with the rewound index 17/24, without it 8/24. Hybrid verdicts identical to v15 on all 11 programs. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19, ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../2026-09-25-tacasv1-aflpp-migration-design.md | 16 ++++++++++++++-- modules/frontend/caller.cpp | 11 ++++++++--- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md index 08c4924e6..9714d883f 100644 --- a/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md +++ b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md @@ -60,10 +60,22 @@ modo só-fuzzer): | configuração | bugs achados | |---|---| -| v15 LibFuzzer (value profile, 8 jobs) | 17/24 | -| AFL++ + CmpLog, índice preservado | 4/24 | +| v15 LibFuzzer (value profile, 8 jobs) | 20/24 | +| AFL++ + CmpLog, índice preservado | 8/24 | | AFL++ + CmpLog, índice zerado por iteração | 17/24 | +(Rodada final, depois de remover o `-V` do `afl-fuzz` — ver abaixo. No modo híbrido +default, os vereditos ficaram idênticos à v15 nos 11 programas, todos corretos.) +O AFL++ ainda perde sistematicamente os bugs guardados por **faixa** estreita +(`5000 < x < 5100`, índice 51..59): o input-to-state do CmpLog propõe os operandos +exatos (os limites da faixa, que ficam fora dela). Ajustar o nível/transformações do +CmpLog (`-l`) fica como calibração para uma rodada posterior. + +**Orçamento sem `-V`.** O `afl-fuzz -V` compara leituras de `gettimeofday`. Um relógio +que volta (medido: 1,1 s em 20 s no WSL2) faz a diferença dar underflow e o AFL++ +encerra depois de poucas centenas de execuções. O fuzzer passa a ser limitado só pelo +`timeout` (temporizador relativo), como o LibFuzzer na v15. + Sem o reset, o CmpLog não tem efeito. A correção fica restrita ao driver do AFL++ (`NonDetGeneratorAFL.c`). O motor da v15 não é alterado, e o resto do smart seeding continua fora do escopo (tacasv2/v3). diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index 35407e1fd..d6584a0f8 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -856,8 +856,14 @@ void Caller::executeAnalysis(std::string solvername) { << " AFL_I_DONT_CARE_ABOUT_MISSING_CRASHES=1" << " AFL_CRASHING_SEEDS_AS_NEW_CRASH=1" << " AFL_BENCH_UNTIL_CRASH=1 "; + // Bounded by `timeout` alone, as the previous fuzzer was. Not also by + // afl-fuzz -V: that one compares wall-clock (gettimeofday) readings, + // and a clock stepped backwards -- measured at over a second under + // WSL2 -- underflows the difference and ends the run after a few + // hundred executions. `timeout` uses a relative timer. At least 1s, + // since `timeout 0` would mean no limit at all. command << "timeout -k " << Map2Check::killGracePeriod << " " - << static_cast(fuzzerBudget) << " "; + << std::max(1u, static_cast(fuzzerBudget)) << " "; std::error_code cmplogErr; const bool hasCmplog = std::filesystem::exists(programHash + "-cmplog.out", cmplogErr); @@ -865,8 +871,7 @@ void Caller::executeAnalysis(std::string solvername) { << " -i " << inputDir << " -o afl-out"; if (hasCmplog) command << " -c ./" << programHash << "-cmplog.out"; - command << " -V " << std::max(1u, static_cast(fuzzerBudget)) - << " -- ./" << programHash << "-fuzzed.out" + command << " -- ./" << programHash << "-fuzzed.out" << " > fuzzer.output 2>&1"; int result = system(command.str().c_str()); From 6c7b0f2d91b50844e0dc260efad539d45aa7ba97 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 18:24:53 -0400 Subject: [PATCH 14/14] fix(verdict): an empty vector is a witness when the program reads no input 621db9372 downgrades a KLEE violation to UNKNOWN when no input vector can be recovered, to stop FAILED verdicts that nothing reproduces. It asked readViolatingKtest for a non-empty vector, so a program that reads no nondeterministic input -- whose aborting path has a .ktest with zero objects -- was downgraded too, and its suite came out with no test case. That is tests/testcomp/programs/no_input.c, and it has failed the TestCov CI gate on develop since that commit landed (run 33523637266). hasViolatingKtest counts an .abort.err whose .ktest exists, empty or not; the downgrade now uses it. The halted-KLEE case 621db9372 guards against still has no .abort.err at all, so it is still downgraded. Verified in both the current CI image (ghcr map2check-dev:latest) and map2check-dev:aflpp: run_testcov_suite.sh 6/6 (no_input.c COVERED), test_cover_branches.sh 5/5, test_benchexec_toolinfo.py 16/16, test_testcomp_regressions.sh 19/19, ctest 9/9 (3 new KtestReader tests). Co-Authored-By: Claude Opus 5.5 (1M context) --- modules/frontend/map2check.cpp | 7 ++++- modules/frontend/test_suite/ktest_reader.cpp | 21 ++++++++++++++ modules/frontend/test_suite/ktest_reader.hpp | 8 ++++++ tests/unit/frontend/KtestReaderTest.cpp | 30 ++++++++++++++++++++ 4 files changed, 65 insertions(+), 1 deletion(-) diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index 65f93f32b..cd5e7f91e 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -608,6 +608,11 @@ int map2check_execution(map2check_args args) { // // Gated on generating a suite at all, and on the two sources emitTestSuite // itself consults -- so the check can never disagree with what gets written. + // + // "Recovered" includes the EMPTY vector of an aborting path: a program that + // reads no input reaches its error with zero elements, and that + // test case covers it (tests/testcomp/programs/no_input.c). Counting only + // non-empty vectors downgraded exactly that case to UNKNOWN. if (args.generateTestSuite && !args.coverBranches && args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE && generator == Map2Check::NonDetGenerator::Klee && @@ -615,7 +620,7 @@ int map2check_execution(map2check_args args) { propertyViolated != Map2Check::PropertyViolated::UNKNOWN) { const bool haveVector = !Map2Check::readNonDetLog(Map2Check::kleeLogCSV).empty() || - !Map2Check::readViolatingKtest(Map2Check::kleeOutputDir).empty(); + Map2Check::hasViolatingKtest(Map2Check::kleeOutputDir); if (!haveVector) { Map2Check::Log::Warning( "the property file records a violation but no input vector could be " diff --git a/modules/frontend/test_suite/ktest_reader.cpp b/modules/frontend/test_suite/ktest_reader.cpp index 27878ad0b..c44185cea 100644 --- a/modules/frontend/test_suite/ktest_reader.cpp +++ b/modules/frontend/test_suite/ktest_reader.cpp @@ -287,6 +287,27 @@ std::vector readViolatingKtest(const std::string& kleeOutDir) { return {}; } +bool hasViolatingKtest(const std::string& kleeOutDir) { + std::error_code error; + if (!std::filesystem::is_directory(kleeOutDir, error)) return false; + const std::string kAbortSuffix = ".abort.err"; + for (const auto& entry : + std::filesystem::directory_iterator(kleeOutDir, error)) { + const std::string name = entry.path().filename().string(); + if (name.size() <= kAbortSuffix.size()) continue; + if (name.compare(name.size() - kAbortSuffix.size(), kAbortSuffix.size(), + kAbortSuffix) != 0) { + continue; + } + const std::string stem = name.substr(0, name.size() - kAbortSuffix.size()); + if (std::filesystem::exists( + std::filesystem::path(kleeOutDir) / (stem + ".ktest"), error)) { + return true; + } + } + return false; +} + std::vector> readKtestVectors( const std::string& kleeOutDir, size_t limit) { std::vector> vectors; diff --git a/modules/frontend/test_suite/ktest_reader.hpp b/modules/frontend/test_suite/ktest_reader.hpp index 907152ae0..b737ad59c 100644 --- a/modules/frontend/test_suite/ktest_reader.hpp +++ b/modules/frontend/test_suite/ktest_reader.hpp @@ -73,6 +73,14 @@ std::string decodeKtestObject(const KtestObject& object); * runtime. Returns an empty vector when no path errored. */ std::vector readViolatingKtest(const std::string& kleeOutDir); +/** Whether KLEE flagged an aborting path whose .ktest is on disk at all. + * + * Unlike readViolatingKtest this also counts a path with ZERO objects: a + * program that reads no nondeterministic input reaches its error with the + * empty vector, and that empty vector is a complete, reproducible witness -- + * not the "nothing recovered" readViolatingKtest's empty result means. */ +bool hasViolatingKtest(const std::string& kleeOutDir); + /** Every input vector KLEE recorded under `kleeOutDir`, one per .ktest. * * Ordered by file name, which is KLEE's own path numbering: stable across diff --git a/tests/unit/frontend/KtestReaderTest.cpp b/tests/unit/frontend/KtestReaderTest.cpp index f58feed9e..e3233a2bd 100644 --- a/tests/unit/frontend/KtestReaderTest.cpp +++ b/tests/unit/frontend/KtestReaderTest.cpp @@ -255,3 +255,33 @@ TEST(ReadKtestVectors, DropsVectorsWithNoObjects) { TEST(ReadKtestVectors, MissingDirectoryYieldsNothing) { EXPECT_TRUE(Map2Check::readKtestVectors("/nonexistent/klee-last", 10).empty()); } + +// --- violating path --------------------------------------------------------- + +// A program with no nondeterministic input reaches its error with the empty +// vector. That is a complete witness, and the verdict must not be downgraded +// for lacking one (tests/testcomp/programs/no_input.c). +TEST(HasViolatingKtest, CountsAnAbortingPathWithNoObjects) { + fs::path d = freshDir("violating_empty"); + KtestBuilder().writeTo(d / "test000001.ktest"); + std::ofstream(d / "test000001.abort.err") << "abort"; + EXPECT_TRUE(Map2Check::hasViolatingKtest(d.string())); + EXPECT_TRUE(Map2Check::readViolatingKtest(d.string()).empty()); + fs::remove_all(d); +} + +TEST(HasViolatingKtest, IgnoresErrorsThatAreNotAborts) { + fs::path d = freshDir("violating_ptr"); + KtestBuilder().object("non_det_int", le32(1)).writeTo(d / "test000001.ktest"); + std::ofstream(d / "test000001.ptr.err") << "ptr"; + EXPECT_FALSE(Map2Check::hasViolatingKtest(d.string())); + fs::remove_all(d); +} + +TEST(HasViolatingKtest, NeedsTheKtestBesideTheReport) { + fs::path d = freshDir("violating_orphan"); + std::ofstream(d / "test000001.abort.err") << "abort"; + EXPECT_FALSE(Map2Check::hasViolatingKtest(d.string())); + EXPECT_FALSE(Map2Check::hasViolatingKtest("/nonexistent/klee-last")); + fs::remove_all(d); +}