From b72835b6bdbc76f62e6b639a8ab710b401f042e3 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Fri, 25 Sep 2026 22:34:31 -0400 Subject: [PATCH 01/24] =?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/24] =?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/24] 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/24] 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/24] 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/24] 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/24] 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/24] 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/24] =?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/24] 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/24] 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/24] 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/24] 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/24] 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); +} From a12ac9b94c0ab9d34d0ce73351cb58c1aa48f990 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 22:59:26 -0400 Subject: [PATCH 15/24] =?UTF-8?q?docs(tacasv2a):=20design=20spec=20?= =?UTF-8?q?=E2=80=94=20slicing=20for=20reach/assert=20that=20keeps=20the?= =?UTF-8?q?=20suite=20valid?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Diagnosis on 12 tasks the v15 slice arm lost, with the tacasv1 build: the slicer's cutoff inserts exit(0) without !dbg and KLEE aborts on a broken module; and nondet calls the slicer drops misalign the suite on the original program. Cutoff off + nondets as criteria: 6/12 -> 10/12. Co-Authored-By: Claude Opus 5.5 (1M context) --- ...26-tacasv2a-slicing-reach-assert-design.md | 164 ++++++++++++++++++ 1 file changed, 164 insertions(+) create mode 100644 docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md diff --git a/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md new file mode 100644 index 000000000..3a0ac37b5 --- /dev/null +++ b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md @@ -0,0 +1,164 @@ +# tacasv2a — Slicing para reachability e assert que preserva a suíte de testes + +**Data:** 2026-09-26 +**Branch:** `tacas/slicing` (a partir de `tacas/aflpp`) +**Baseline:** tacasv1 (AFL++ 4.40c + CmpLog), mesmo motor com e sem `--slice` +**Status:** rascunho — aguardando revisão + +--- + +## 1. Objetivo + +Fazer o `--slice` deixar de **prejudicar** o Cover-Error e, se possível, ajudar. Na v15, o +braço com slice cobriu 412 tarefas contra 470 do controle (McNemar χ² = 36,10), com 57 +das 58 perdas em ECA. Esta etapa corrige a causa dessas perdas e estende o slicing ao +modo assert. É o primeiro sub-projeto da tacasv2 ("slicing por propriedade"); memória e +overflow ficam para 2b e 2c. + +> Linha de desenvolvimento: `decisions/tacas-afl-slicing-roadmap.md` (ai-memory). +> A tacasv2 parte da tacasv1 porque o AFL++ é a evolução decidida: nada é calibrado +> contra o LibFuzzer. + +--- + +## 2. Diagnóstico (medido em 2026-09-26) + +Amostra: 12 tarefas que a v15 cobria sem slice e perdia com slice (9 ECA, 3 de outras +famílias). Build tacasv1, orçamento de 300 s, TestCov 300 s, uma execução por braço. + +| braço | cobertas | +|---|---| +| controle (sem slice) | 11/12 | +| slice como está hoje | 6/12 | +| slice com `-cutoff-diverging=false` | 10/12 | +| slice sem cutoff + nondets como critério | 10/12 (e o único que cobre `floppy.i.cil-1`) | + +As duas tarefas que a última variante não cobriu terminaram perto do orçamento (~258 s). +Com uma execução por braço, não dá para separar isso de variação. + +### Defeito 1 — o KLEE aborta em toda fatia com caminho cortado + +- O `--cutoff-diverging` (default `true` no dg/sbt-slicer) insere um bloco `diverge:` + com `call exit(0)` + `unreachable`. O `--help` diz "abort()", mas o código + (`dg/tools/llvm-slicer-preprocess.cpp`) chama `exit(0)`. +- Essas chamadas não têm localização de debug (`!dbg`), e o programa é compilado com `-g`. +- Quando o KLEE linka a uClibc, `exit` passa a ter corpo e o verificador rejeita o módulo: + `inlinable function call in a function with debug info must have a !dbg location` → + `LLVM ERROR: Broken module found`. O KLEE aborta (status 134) antes de executar. +- Em `eca-rers2012/Problem15_label09.c`, a fatia tem 60 blocos `diverge`. +- **Consequência:** no braço com slice da v15, o KLEE não rodou em nenhuma tarefa com + caminho cortado. Com o LibFuzzer, o `exit(0)` também encerrava a sessão de fuzzing. +- Com `-cutoff-diverging=false`, o KLEE da mesma tarefa roda até o fim (saída 0). + +### Defeito 2 — o vetor da fatia não vale no programa original + +- O slicer remove chamadas `__VERIFIER_nondet_*` cujo valor não afeta o critério. Em + `ntdrivers/floppy.i.cil-1.c`: 29 chamadas no programa, 10 na fatia. +- O vetor de entradas é gerado na fatia, mas o TestCov executa o **programa original**, + que consome mais valores e em outra ordem. O veredito sai FAILED e a suíte não cobre. +- Passar as funções nondet como critério **primário**, junto com o alvo, preserva as + chamadas alcançáveis: `floppy` passa a FAILED + COVERED. + +--- + +## 3. Decisões + +| Decisão | Valor | +|---|---| +| Cutoff | `-cutoff-diverging=false` | +| Critério em reachability | `` + todas as funções `__VERIFIER_nondet_*` conhecidas | +| Critério em assert | `__VERIFIER_assert` + as mesmas funções nondet | +| Onde fatiar | continua **antes** da instrumentação (`sliceWithRespectToTarget`, antes de `callPass`) | +| Stub da função alvo | mantém o stub `weak` atual | +| Visibilidade | `--statistics` no slicer; o Caller registra funções/blocos/instruções antes → depois | +| Outras flags (`--pta`, `--cda`, `--undefined-funs`) | defaults nesta etapa; calibrar só com medição própria | +| Cutoff "consertado" (manter o corte, corrigir `!dbg`, trocar `exit` por poda silenciosa) | fora; experimento condicional se a medição mostrar falta de eficiência de busca | + +A lista de funções nondet é fixa: as 16 que o `NonDetPass` instrumenta (`bool`, `char`, +`uchar`, `short`, `ushort`, `int`, `uint`, `unsigned`, `long`, `ulong`, `size_t`, +`loff_t`, `sector_t`, `pointer`, `pchar`, `double`) mais as do SV-COMP que ele ainda não +cobre (`float`, `longlong`, `ulonglong`, `_Bool`, `u8`, `u16`, `u32`, `charp`). O slicer +aceita nomes que não existem no programa. Isso foi verificado: não dá erro e não muda a +saída. Uma lista fixa dispensa desmontar o bitcode. + +--- + +## 4. Referência comparada: o que o Symbiotic faz + +Levantado no código do Symbiotic (master `4474bb9`), do sbt-slicer (`e350116`, o mesmo +SHA que o nosso Dockerfile fixa) e do dg. + +| Aspecto | Symbiotic | tacasv2a | Por quê | +|---|---|---|---| +| Fatia em Test-Comp (coverage-error/branches) | **Não** no pipeline principal | Sim, em Cover-Error | É onde o Map2Check usa o slicing; exige resolver o Defeito 2, que ele nunca enfrenta | +| `--cutoff-diverging` | Mantém (default) | Desliga | O KLEE dele reconhece violação por `-error-fn` e o módulo dele não quebra; o nosso quebra (Defeito 1) | +| Ponto do pipeline | Depois da instrumentação, com marcadores como critério | Antes da instrumentação | Para reach/assert o critério já existe no programa; os marcadores entram no 2b/2c | +| Contraexemplo | Reexecutado no programa sem slice (`-replay-nondets`) | Nondets preservados na fatia | Replay exigiria nomear cada nondet por call site; preservar é mais simples e resolve para Test-Comp | +| Flags extras | `-pta fi`, `-2c __VERIFIER_assume,klee_assume` (implícito) | Iguais por default | — | + +**O que é contribuição nossa:** slicing que **preserva a ordem de consumo das entradas**, de +modo que a suíte gerada na fatia continua válida no programa original. O Symbiotic não +precisa disso porque não gera suíte a partir da fatia. + +--- + +## 5. Mudanças + +### 5.1 `Caller::sliceWithRespectToTarget` (`modules/frontend/caller.cpp`) +- Recebe a lista de critérios em vez de só o nome da função alvo, e monta + `-c ,`. +- Acrescenta `-cutoff-diverging=false` e `--statistics`. +- Extrai do `slicer.output` as linhas `Statistics before/after` e registra + `Sliced with respect to X: F/B/I functions/blocks/instructions → F'/B'/I'`, mantendo + também os bytes. +- O restante (orçamento, fallback para o programa inteiro, stub `weak`) não muda. + +### 5.2 Gating em `map2check.cpp` +- `--slice` passa a valer também em `ASSERT_MODE`, com o critério `__VERIFIER_assert`. + Os demais modos continuam recusados com aviso, até o 2b e o 2c. + +### 5.3 Constante da lista de nondets +- `Map2Check::nondetFunctionNames()` em `utils/tools.hpp`, documentada como a lista que o + slicing preserva, com um comentário apontando para o `NonDetPass`. + +--- + +## 6. Testes + +Integração (`tests/integration/test_testcomp_regressions.sh`, seção de slicing): +1. **O KLEE sobrevive à fatia.** Um programa com ramos que não alcançam o alvo, rodado com + `--slice --nondet-generator symex`: sem `Broken module`, com FAILED. +2. **O vetor vale no original.** Um programa com um nondet irrelevante antes do relevante + (`int a = nondet(); int b = nondet(); if (b == 42) reach_error();`), rodado com + `--slice --generate-test-suite`: a suíte tem 2 entradas, na ordem do original. +3. **Assert fatia.** `--check-asserts --slice` registra `Sliced with respect to + __VERIFIER_assert` e mantém o veredito. +4. Os testes existentes de slicing ("degrade loudly", recusa em cover-branches) continuam. + +Unitário: se a extração das estatísticas virar função própria, um teste de parser sobre um +`slicer.output` fixo. + +--- + +## 7. Avaliação (tacasv2a) + +- **Quando:** depois do merge do PR #66 e desta branch, na execução sequencial combinada + com o usuário. +- **Como:** corpus de Cover-Error (1087 tarefas pareadas, `cover-error-q400.tsv`), dois + braços com o **mesmo build**: controle (sem slice) e `--slice`. Orçamento de 300 s, + 3 shards, como na v15. +- **Critério de sucesso:** o braço com slice **não perde** para o controle (McNemar sem + diferença significativa contra, ou a favor) e as perdas em ECA desaparecem. +- **Relato:** cobertas por família, perdas/ganhos pareados e estatísticas de redução + (instruções antes/depois). + +--- + +## 8. Riscos + +| Risco | Mitigação | +|---|---| +| Sem o cutoff, a fatia fica maior e o ganho de busca diminui | É o preço da correção. O cutoff "consertado" fica como experimento condicional (§3) | +| Preservar nondets puxa código que a fatia removeria | Medido no `floppy`: 8933 → 9155 linhas de IR (+2,5%). Acompanhar a redução na avaliação | +| Alguma função nondet fora da lista | A lista inclui as do SV-COMP; uma função ausente só reproduz o Defeito 2 naquela tarefa, e o teste 2 detecta o caso comum | +| Amostra de 12 tarefas | É diagnóstico, não avaliação; a conclusão vem da §7 | From 83ec67c7e7ba497149f12b1c774b6e7c0742df95 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 23:35:51 -0400 Subject: [PATCH 16/24] docs(tacasv2a): implementation plan Co-Authored-By: Claude Opus 5.5 (1M context) --- ...026-09-26-tacasv2a-slicing-reach-assert.md | 752 ++++++++++++++++++ ...26-tacasv2a-slicing-reach-assert-design.md | 9 +- 2 files changed, 758 insertions(+), 3 deletions(-) create mode 100644 docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md diff --git a/docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md b/docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md new file mode 100644 index 000000000..d184904bc --- /dev/null +++ b/docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md @@ -0,0 +1,752 @@ +# tacasv2a — Slicing for reach/assert that keeps the suite valid: 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:** Make `--slice` stop crashing KLEE and stop producing test suites that are invalid on the original program. Also extend `--slice` to assert mode. + +**Architecture:** Slicing stays where it is: in `Caller::sliceWithRespectToTarget`, before instrumentation. The pure pieces are: +- the criteria list, built from the target plus every `__VERIFIER_nondet_*` function; +- the weak-stub source; +- the parser for the slicer's `--statistics` output. + +They move into a new header-only unit `modules/frontend/utils/slicer.hpp`, so they can be unit-tested without a build of the whole tool. The Caller then passes `-cutoff-diverging=false --statistics` and logs the counts. `map2check.cpp` enables the assert-mode criterion. + +**Tech Stack:** C++17, LLVM 16, sbt-slicer (dg) pinned in `Dockerfile.dev`, GTest, bash integration tests. Build and run everything inside the dev image (`map2check-dev:aflpp`, built from `Dockerfile.dev`); the host has no clang, cmake or ninja. + +**Spec:** `docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md` + +## Global Constraints + +- Branch `tacas/slicing` (created from `tacas/aflpp`); the baseline is tacasv1. Never target LibFuzzer. +- Cutoff: `-cutoff-diverging=false`. +- Reachability criterion: `` plus every known `__VERIFIER_nondet_*` function. +- Assert criterion: `__VERIFIER_assert,__assert_fail` plus the same nondet functions (AssertPass instruments both). +- Slice before instrumentation (unchanged). Keep the weak stub for the criterion function. +- Other slicer flags (`--pta`, `--cda`, `--undefined-funs`) stay at their defaults in this stage. +- Pass `--statistics` to the slicer, and log globals/functions/blocks/instructions before → after, plus bytes. +- C++: Google style (`.clang-format`), `` (never boost). Commit messages end with `Co-Authored-By: Claude Opus 5.5 (1M context) `. + +## Review Focus + +- **A program that declares no nondet function at all** (`no_input.c`-like). The criteria must still be the target alone plus names that do not exist, and the slicer accepts those silently (verified). Pinned in Task 1. +- **`--slice` in assert mode on a program that only declares `__VERIFIER_assert`.** The weak stub must have the `(int)` signature or `llvm-link` rejects the type. Pinned in Task 3. +- **A slicer build whose `--statistics` prints nothing, or a different format.** The log must fall back to bytes only and never print zeros as if measured. Pinned in Task 1 (parser returns `found=false`). +- **A program with a nondet read that is irrelevant to the target and consumed before the relevant one.** The suite must carry both values, in the original order. Pinned in Task 2. +- **A program whose non-target branch returns early** (the path the cutoff used to rewrite). KLEE must run and report FAILED, not abort on a broken module. Pinned in Task 2. + +--- + +## File Structure + +- Create `modules/frontend/utils/slicer.hpp`, header-only and pure (no I/O). It holds `nondetFunctionNames()`, `slicingCriteria()`, `targetStubSource()`, `SlicerStatistics`, `parseSlicerStatistics()` and `describeSlice()`. +- Create `tests/unit/frontend/SlicerTest.cpp` with the GTest unit tests for `slicer.hpp`. +- Modify `tests/unit/frontend/CMakeLists.txt` to register `SlicerTest`. +- Modify `modules/frontend/caller.cpp` so that `sliceWithRespectToTarget` uses `slicer.hpp` and passes the new flags. +- Modify `modules/frontend/caller.hpp` to update the doc comment of `sliceWithRespectToTarget`; the signature stays the same. +- Modify `modules/frontend/map2check.cpp` for the `--slice` gating (reach + assert) and the help text. +- Modify `tests/integration/test_testcomp_regressions.sh`: new slicing sections, and the refusal-message check updated. +- Modify `CHANGELOG.md` to add a tacasv2a entry. + +--- + +### Task 1: Pure slicing helpers (`slicer.hpp`) with unit tests + +**Files:** +- Create: `modules/frontend/utils/slicer.hpp` +- Create: `tests/unit/frontend/SlicerTest.cpp` +- Modify: `tests/unit/frontend/CMakeLists.txt` (append) + +**Interfaces:** +- Produces (namespace `Map2Check`): + - `const std::vector& nondetFunctionNames();` + - `std::string slicingCriteria(const std::vector& primary);` returns the comma-joined `primary` followed by every nondet name. + - `std::string targetStubSource(const std::string& function);` returns a one-line C weak definition with the right signature. + - `struct SlicerCounts { unsigned globals = 0, functions = 0, blocks = 0, instructions = 0; };` + - `struct SlicerStatistics { bool found = false; SlicerCounts before, after; };` + - `SlicerStatistics parseSlicerStatistics(const std::string& slicerOutput);` + - `std::string describeSlice(const std::string& criterion, const SlicerStatistics& stats, uintmax_t bytesBefore, uintmax_t bytesAfter);` + +- [ ] **Step 1: Write the failing unit tests** + +Create `tests/unit/frontend/SlicerTest.cpp`: + +```cpp +/** + * Copyright (C) 2014 - 2026 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 + +#include +#include +#include + +#include "../../../modules/frontend/utils/slicer.hpp" + +// The suite is generated on the slice and run by TestCov on the ORIGINAL +// program, so every nondet read the original performs must survive slicing. +TEST(SlicingCriteria, AppendsEveryNondetFunctionAfterThePrimary) { + const std::string criteria = Map2Check::slicingCriteria({"reach_error"}); + EXPECT_EQ(criteria.rfind("reach_error,", 0), 0u); + for (const std::string& name : Map2Check::nondetFunctionNames()) { + EXPECT_NE(criteria.find("," + name), std::string::npos) << name; + } +} + +TEST(SlicingCriteria, KeepsSeveralPrimariesInOrder) { + const std::string criteria = + Map2Check::slicingCriteria({"__VERIFIER_assert", "__assert_fail"}); + EXPECT_EQ(criteria.rfind("__VERIFIER_assert,__assert_fail,", 0), 0u); +} + +TEST(NondetFunctionNames, CoversWhatNonDetPassInstruments) { + const auto& names = Map2Check::nondetFunctionNames(); + for (const char* type : {"bool", "char", "uchar", "short", "ushort", "int", + "uint", "unsigned", "long", "ulong", "size_t", + "loff_t", "sector_t", "pointer", "pchar", "double"}) { + const std::string name = std::string("__VERIFIER_nondet_") + type; + EXPECT_NE(std::find(names.begin(), names.end(), name), names.end()) << name; + } +} + +TEST(TargetStubSource, VoidTargetGetsAVoidStub) { + EXPECT_EQ(Map2Check::targetStubSource("reach_error"), + "void __attribute__((weak)) reach_error(void) {}\n"); +} + +// __VERIFIER_assert takes the condition; a (void) stub would not link against +// the program's own declaration. +TEST(TargetStubSource, AssertStubTakesTheCondition) { + EXPECT_EQ(Map2Check::targetStubSource("__VERIFIER_assert"), + "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"); +} + +TEST(ParseSlicerStatistics, ReadsBeforeAndAfter) { + const std::string output = + "Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764\n" + "[llvm-slicer] Sliced away 1454 from 4227 nodes in DG\n" + "Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989\n"; + const Map2Check::SlicerStatistics stats = + Map2Check::parseSlicerStatistics(output); + ASSERT_TRUE(stats.found); + EXPECT_EQ(stats.before.functions, 97u); + EXPECT_EQ(stats.before.blocks, 2215u); + EXPECT_EQ(stats.before.instructions, 10764u); + EXPECT_EQ(stats.after.globals, 37u); + EXPECT_EQ(stats.after.functions, 38u); + EXPECT_EQ(stats.after.instructions, 2989u); +} + +// A slicer that prints no statistics must not be reported as having sliced +// everything away. +TEST(ParseSlicerStatistics, MissingLinesAreNotFound) { + EXPECT_FALSE(Map2Check::parseSlicerStatistics("").found); + EXPECT_FALSE(Map2Check::parseSlicerStatistics( + "Statistics before Globals/Functions/Blocks/Instr.: 1 2 3 4\n") + .found); +} + +TEST(DescribeSlice, ReportsCountsWhenFound) { + Map2Check::SlicerStatistics stats; + stats.found = true; + stats.before = {37, 97, 2215, 10764}; + stats.after = {37, 38, 444, 2989}; + EXPECT_EQ(Map2Check::describeSlice("reach_error", stats, 184164, 171708), + "Sliced with respect to reach_error: 97/2215/10764 -> 38/444/2989 " + "functions/blocks/instructions (184164 -> 171708 bytes of " + "bitcode)"); +} + +TEST(DescribeSlice, FallsBackToBytesWithoutStatistics) { + EXPECT_EQ(Map2Check::describeSlice("reach_error", {}, 10, 8), + "Sliced with respect to reach_error: 10 -> 8 bytes of bitcode"); +} +``` + +Append to `tests/unit/frontend/CMakeLists.txt`: + +```cmake + +add_executable(SlicerTest + SlicerTest.cpp +) +map2check_test(SlicerTest) +``` + +- [ ] **Step 2: Run the tests and confirm they fail to compile** + +Run inside the dev image: +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c \ + 'mkdir -p /workspace/build_ut && cd /workspace/build_ut && cmake .. -G Ninja -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm -DENABLE_TEST=ON >/dev/null && ninja SlicerTest 2>&1 | tail -5' +``` +Expected: FAIL with `fatal error: '../../../modules/frontend/utils/slicer.hpp' file not found`. + +- [ ] **Step 3: Implement `slicer.hpp`** + +Create `modules/frontend/utils/slicer.hpp`: + +```cpp +/** + * Copyright (C) 2014 - 2026 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) + **/ + +#ifndef MODULES_FRONTEND_UTILS_SLICER_HPP_ +#define MODULES_FRONTEND_UTILS_SLICER_HPP_ + +#include +#include +#include +#include +#include + +namespace Map2Check { + +/** Every __VERIFIER_nondet_* function the slice must keep. + * + * The suite is generated on the slice, but TestCov runs it on the ORIGINAL + * program. A nondet call the slicer drops -- its value does not reach the + * criterion -- is still consumed by the original, so the vector shifts and + * the suite stops covering (measured: ntdrivers/floppy.i.cil-1.c, 29 reads in + * the program and 10 in the slice; FAILED, NOT_COVERED). Keeping these calls + * as criteria keeps the consumption order. + * + * The first sixteen are what NonDetPass instruments; the rest are SV-COMP + * names it does not model yet, kept so their order is not lost either. The + * slicer accepts names the program does not use. */ +inline const std::vector& nondetFunctionNames() { + static const std::vector names = { + "__VERIFIER_nondet_bool", "__VERIFIER_nondet_char", + "__VERIFIER_nondet_uchar", "__VERIFIER_nondet_short", + "__VERIFIER_nondet_ushort", "__VERIFIER_nondet_int", + "__VERIFIER_nondet_uint", "__VERIFIER_nondet_unsigned", + "__VERIFIER_nondet_long", "__VERIFIER_nondet_ulong", + "__VERIFIER_nondet_size_t", "__VERIFIER_nondet_loff_t", + "__VERIFIER_nondet_sector_t", "__VERIFIER_nondet_pointer", + "__VERIFIER_nondet_pchar", "__VERIFIER_nondet_double", + "__VERIFIER_nondet_float", "__VERIFIER_nondet_longlong", + "__VERIFIER_nondet_ulonglong", "__VERIFIER_nondet__Bool", + "__VERIFIER_nondet_u8", "__VERIFIER_nondet_u16", + "__VERIFIER_nondet_u32", "__VERIFIER_nondet_charp"}; + return names; +} + +/** The -c argument: the primary criteria, then every nondet function. */ +inline std::string slicingCriteria(const std::vector& primary) { + std::ostringstream criteria; + bool first = true; + for (const std::string& name : primary) { + criteria << (first ? "" : ",") << name; + first = false; + } + for (const std::string& name : nondetFunctionNames()) { + criteria << (first ? "" : ",") << name; + first = false; + } + return criteria.str(); +} + +/** A weak definition of the criterion function, restoring the body the + * slicer removes without displacing a real one. The signature must match + * the program's declaration, or llvm-link rejects the module. */ +inline std::string targetStubSource(const std::string& function) { + if (function == "__VERIFIER_assert") { + return "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"; + } + return "void __attribute__((weak)) " + function + "(void) {}\n"; +} + +struct SlicerCounts { + unsigned globals = 0; + unsigned functions = 0; + unsigned blocks = 0; + unsigned instructions = 0; +}; + +struct SlicerStatistics { + bool found = false; // both the "before" and the "after" line were read + SlicerCounts before; + SlicerCounts after; +}; + +/** Reads sbt-slicer's --statistics lines: + * Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764 + * Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989 */ +inline SlicerStatistics parseSlicerStatistics(const std::string& slicerOutput) { + static const std::regex line( + R"(Statistics (before|after) Globals/Functions/Blocks/Instr\.:\s+)" + R"((\d+)\s+(\d+)\s+(\d+)\s+(\d+))"); + SlicerStatistics stats; + bool sawBefore = false; + bool sawAfter = false; + for (std::sregex_iterator it(slicerOutput.begin(), slicerOutput.end(), line), + end; + it != end; ++it) { + const std::smatch& m = *it; + SlicerCounts counts; + counts.globals = static_cast(std::stoul(m[2])); + counts.functions = static_cast(std::stoul(m[3])); + counts.blocks = static_cast(std::stoul(m[4])); + counts.instructions = static_cast(std::stoul(m[5])); + if (m[1] == "before") { + stats.before = counts; + sawBefore = true; + } else { + stats.after = counts; + sawAfter = true; + } + } + stats.found = sawBefore && sawAfter; + return stats; +} + +/** The one log line a slice produces. Counts when the slicer reported them, + * bytes always -- a slice narrows the question being answered, and this line + * is the only visible sign of how much was dropped. */ +inline std::string describeSlice(const std::string& criterion, + const SlicerStatistics& stats, + uintmax_t bytesBefore, uintmax_t bytesAfter) { + std::ostringstream text; + text << "Sliced with respect to " << criterion << ": "; + if (stats.found) { + text << stats.before.functions << "/" << stats.before.blocks << "/" + << stats.before.instructions << " -> " << stats.after.functions << "/" + << stats.after.blocks << "/" << stats.after.instructions + << " functions/blocks/instructions (" << bytesBefore << " -> " + << bytesAfter << " bytes of bitcode)"; + } else { + text << bytesBefore << " -> " << bytesAfter << " bytes of bitcode"; + } + return text.str(); +} + +} // namespace Map2Check + +#endif // MODULES_FRONTEND_UTILS_SLICER_HPP_ +``` + +- [ ] **Step 4: Run the tests and confirm they pass** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c \ + 'cd /workspace/build_ut && ninja SlicerTest >/dev/null && ./tests/unit/frontend/SlicerTest 2>&1 | tail -3' +``` +Expected: `[ PASSED ] 9 tests.` (If the binary is elsewhere, find it with `find /workspace/build_ut -name SlicerTest -type f`.) + +- [ ] **Step 5: Commit** + +```bash +git add modules/frontend/utils/slicer.hpp tests/unit/frontend/SlicerTest.cpp tests/unit/frontend/CMakeLists.txt +git commit -m "feat(tacasv2a): pure slicing helpers -- criteria, stub, statistics + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` + +--- + +### Task 2: Slice without cutoff, keep the nondets, log the statistics + +**Files:** +- Modify: `modules/frontend/caller.cpp`, in `Caller::sliceWithRespectToTarget` (starts around line 179: the command construction around lines 218-222, the success log around lines 243-245, and the stub around lines 262-268) +- Modify: `modules/frontend/caller.hpp:133-136` (doc comment only) +- Test: `tests/integration/test_testcomp_regressions.sh`, new section 13 inserted **before** the final `echo " ---"` summary lines + +**Interfaces:** +- Consumes: `Map2Check::slicingCriteria`, `Map2Check::targetStubSource`, `Map2Check::parseSlicerStatistics`, `Map2Check::describeSlice` from Task 1. +- Produces: the log line `Sliced with respect to : …` (the integration tests grep the `Sliced with respect to` prefix). `sliceWithRespectToTarget` gains a second parameter, `const std::vector& criteria`, the primary criteria; the first stays `targetFunction`, used for the stub and the log. Task 3 calls it with `{"__VERIFIER_assert", "__assert_fail"}`. + +- [ ] **Step 1: Write the failing integration tests** + +In `tests/integration/test_testcomp_regressions.sh`, insert this block immediately before the lines `echo " ---"` / `echo " Results: ..."` at the end: + +```bash +# --- 13. a slice must leave KLEE something it can run ------------------------- +# sbt-slicer's --cutoff-diverging (default on) rewrites every path that cannot +# reach the criterion into a `diverge:` block calling exit(0) -- with no debug +# location. The program is compiled with -g; once KLEE links uClibc, exit has a +# body, and the verifier rejects the module ("inlinable function call in a +# function with debug info must have a !dbg location"). KLEE aborted before +# executing anything, on every sliced task with a cut path: the slice arm of +# the v15 campaign ran without its symbolic engine. +mkdir -p "$WORK/cut" +cat > "$WORK/cut/cut.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + if (x == 3) { return 1; } + if (x == 7) { reach_error(); } + return 0; +} +EOF +( cd "$WORK/cut" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --timeout 45 cut.c ) > "$WORK/cut/run.log" 2>&1 +if grep -q "Broken module" "$WORK/cut/run.log"; then + fail "slice + KLEE" "KLEE rejected the sliced module (cutoff exit without !dbg)" +elif grep -q "VERIFICATION FAILED" "$WORK/cut/run.log"; then + ok "KLEE runs on the slice and reaches the target" +else + fail "slice + KLEE" "no FAILED verdict on a trivially reachable target" + grep -E "Sliced|Exited klee|VERIFICATION" "$WORK/cut/run.log" | sed 's/^/ /' +fi + +# --- 14. a suite found on the slice must hold on the original ---------------- +# TestCov runs the suite on the ORIGINAL program. A nondet read the slicer +# dropped -- its value does not reach the target -- is still consumed there, +# so the vector shifts: measured on ntdrivers/floppy.i.cil-1.c, FAILED and +# NOT_COVERED. The slice keeps every nondet call, so both values appear, in +# the original order. +mkdir -p "$WORK/order" +cp "$WORK/one/reach.prp" "$WORK/order/" +cat > "$WORK/order/order.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (b == 42) { reach_error(); } + return a; +} +EOF +( cd "$WORK/order" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --generate-test-suite --property-file reach.prp \ + --timeout 60 order.c ) > "$WORK/order/run.log" 2>&1 +order_inputs=$(sed -n 's:.*\(.*\).*:\1:p' \ + "$WORK/order/test-suite/testcase-1.xml" 2>/dev/null | tr '\n' ' ') +if [ "$(echo $order_inputs | wc -w)" -eq 2 ] && \ + [ "$(echo $order_inputs | awk '{print $2}')" = "42" ]; then + ok "the sliced suite keeps the original read order [$order_inputs]" +else + fail "slice read order" "expected 2 inputs ending in 42, got [$order_inputs]" +fi +``` + +- [ ] **Step 2: Build the current code and confirm the new tests fail** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + mkdir -p /workspace/build_aflpp && cd /workspace/build_aflpp && + cmake .. -G Ninja -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm -DCMAKE_INSTALL_PREFIX=/workspace/build_aflpp/install >/dev/null && + ninja >/dev/null && ninja install >/dev/null && + mkdir -p install/lib/klee && ln -sfn /opt/klee/lib/klee/runtime install/lib/klee/runtime && + ln -sfn /usr/lib/llvm-16/lib/clang install/lib/clang && + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|PASS KLEE runs|read order|Results"' +``` +Expected: both `FAIL slice + KLEE: KLEE rejected the sliced module …` and `FAIL slice read order: …`. + +- [ ] **Step 3: Implement the Caller change** + +In `modules/frontend/caller.cpp`, add `#include "utils/slicer.hpp"` next to the other `utils/` includes. + +Change the signature (definition and declaration) to: + +```cpp +bool Caller::sliceWithRespectToTarget(const std::string &targetFunction, + const std::vector &criteria) +``` + +and in `caller.hpp` replace the declaration and its comment with: + +```cpp + /** Runs sbt-slicer over the compiled (not yet instrumented) bitcode. + * + * `criteria` are the primary slicing criteria (the target function, or the + * assert functions); every __VERIFIER_nondet_* function is added to them so + * the suite found on the slice stays valid on the original program. The + * cutoff of diverging paths is off: its exit(0) carries no debug location + * and KLEE rejects the module. `targetFunction` gets its body back through a + * weak stub. Returns false if the slicer is unavailable or produced nothing + * usable, leaving the original bitcode in place. */ + bool sliceWithRespectToTarget(const std::string& targetFunction, + const std::vector& criteria); +``` + +Replace the command construction: + +```cpp + command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(sliceBudget) + << " " << slicer << " -c " << targetFunction + << " --entry=main -o " << output << " " + << input << " > slicer.output 2>&1"; +``` + +with: + +```cpp + // -cutoff-diverging=false: the cutoff rewrites every path that cannot reach + // the criterion into exit(0) with no debug location, and once KLEE links + // uClibc the verifier rejects the module ("Broken module found") -- KLEE + // never ran on a sliced task with a cut path (tacasv2a spec, defect 1). + // + // The nondet functions ride along as criteria so that every read the + // original program performs survives; the suite is generated on the slice + // and replayed on the original (defect 2). + // + // --statistics: counts before and after, logged below. + command << "timeout -k " << Map2Check::killGracePeriod << " " + << static_cast(sliceBudget) << " " << slicer << " -c " + << Map2Check::slicingCriteria(criteria) + << " --entry=main -cutoff-diverging=false --statistics -o " << output + << " " << input << " > slicer.output 2>&1"; +``` + +Replace the success log: + +```cpp + Map2Check::Log::Info("Sliced with respect to " + targetFunction + ": " + + std::to_string(before) + " -> " + + std::to_string(after) + " bytes of bitcode"); +``` + +with: + +```cpp + std::ifstream slicerLog("slicer.output"); + std::stringstream slicerText; + slicerText << slicerLog.rdbuf(); + std::string criterionLabel; + for (const std::string &name : criteria) { + criterionLabel += (criterionLabel.empty() ? "" : ",") + name; + } + Map2Check::Log::Info(Map2Check::describeSlice( + criterionLabel, Map2Check::parseSlicerStatistics(slicerText.str()), + before, after)); +``` + +Replace the stub text: + +```cpp + stub << "void __attribute__((weak)) " << targetFunction << "(void) {}\n"; +``` + +with: + +```cpp + stub << Map2Check::targetStubSource(targetFunction); +``` + +In `modules/frontend/map2check.cpp`, change the one existing call so it still compiles and keeps today's behaviour for reachability: + +```cpp + caller->sliceWithRespectToTarget(args.function, {args.function}); +``` + +Make sure `caller.cpp` includes `` and `` (it already uses `std::ostringstream` and `std::ifstream`; add whichever is missing). + +- [ ] **Step 4: Rebuild and run the integration tests plus the unit tests** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + cd /workspace/build_aflpp && ninja >/dev/null && ninja install >/dev/null && + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|KLEE runs|read order|sliced with respect|Results"' +``` +Expected: `PASS KLEE runs on the slice and reaches the target`, `PASS the sliced suite keeps the original read order [ 42 ]`, `PASS the program was sliced with respect to the target`, and `Results: 21 passed, 0 failed`. + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c 'cd /workspace/build_ut && ninja >/dev/null && ctest 2>&1 | tail -3' +``` +Expected: `100% tests passed`. + +- [ ] **Step 5: Commit** + +```bash +git add modules/frontend/caller.cpp modules/frontend/caller.hpp modules/frontend/map2check.cpp tests/integration/test_testcomp_regressions.sh +git commit -m "fix(tacasv2a): slice without cutoff and keep every nondet read + +The cutoff's exit(0) carries no !dbg and KLEE rejected every sliced +module with a cut path; nondet reads the slicer dropped shifted the +suite on the original program. Both are integration-tested now, and the +slice is logged in functions/blocks/instructions, not only bytes. + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` + +--- + +### Task 3: `--slice` in assert mode + +**Files:** +- Modify: `modules/frontend/map2check.cpp`, the `if (args.sliceProgram)` block (around lines 519-528) and the `("slice", …)` help text (around lines 748-750) +- Test: `tests/integration/test_testcomp_regressions.sh`, section 12's refusal check, plus a new section 15 before the summary +- Modify: `CHANGELOG.md` (top entry) + +**Interfaces:** +- Consumes: `Caller::sliceWithRespectToTarget(const std::string&, const std::vector&)` from Task 2. +- Produces: in assert mode the log line is `Sliced with respect to __VERIFIER_assert,__assert_fail: …`, and the refusal message becomes `--slice applies to reachability and assert only`. + +- [ ] **Step 1: Write the failing tests** + +In section 12 of `tests/integration/test_testcomp_regressions.sh`, change the refusal check's grep from `"applies to reachability only"` to `"applies to reachability and assert only"`. + +Insert before the summary lines (after section 14): + +```bash +# --- 15. assert mode slices towards the assertions ---------------------------- +# AssertPass instruments __VERIFIER_assert and __assert_fail, so those are the +# criteria. The program only DECLARES __VERIFIER_assert: the weak stub must +# take the condition, or llvm-link rejects the (void) definition. +mkdir -p "$WORK/assert" +cat > "$WORK/assert/assert.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void __VERIFIER_assert(int cond); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (a > 0) { a = a - 1; } + __VERIFIER_assert(b != 77); + return a; +} +EOF +( cd "$WORK/assert" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --check-asserts --slice --nondet-generator symex --timeout 45 assert.c ) \ + > "$WORK/assert/run.log" 2>&1 +if grep -q "Sliced with respect to __VERIFIER_assert,__assert_fail" "$WORK/assert/run.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/assert/run.log"; then + ok "assert mode slices towards the assertions and still finds the violation" +else + fail "assert slice" "no assert-criterion slice, or the violation was lost" + grep -E "Sliced|slice|VERIFICATION" "$WORK/assert/run.log" | sed 's/^/ /' +fi +``` + +- [ ] **Step 2: Run them and confirm they fail** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|Results"' +``` +Expected: `FAIL slice mode guard: …` (old message) and `FAIL assert slice: …`. + +- [ ] **Step 3: Implement the gating** + +Replace the block: + +```cpp + if (args.sliceProgram) { + if (args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE) { + caller->sliceWithRespectToTarget(args.function, {args.function}); + } else { + Map2Check::Log::Warning( + "--slice applies to reachability only: there is no criterion to " + "slice towards when the goal is coverage or a memory property. " + "Analysing the whole program."); + } + } +``` + +with: + +```cpp + // Reachability slices towards the target; assert towards the two functions + // AssertPass instruments. Memory properties and overflow need their own + // criteria (tacasv2b/2c); coverage has none -- every branch is the goal. + if (args.sliceProgram) { + if (args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE) { + caller->sliceWithRespectToTarget(args.function, {args.function}); + } else if (args.mode == Map2Check::Map2CheckMode::ASSERT_MODE) { + caller->sliceWithRespectToTarget("__VERIFIER_assert", + {"__VERIFIER_assert", "__assert_fail"}); + } else { + Map2Check::Log::Warning( + "--slice applies to reachability and assert only: there is no " + "criterion to slice towards when the goal is coverage or a memory " + "or overflow property. Analysing the whole program."); + } + } +``` + +Replace the help text: + +```cpp + ("slice", + "\tslice the program with respect to the target before analysing it " + "(reachability only; needs sbt-slicer)") +``` + +with: + +```cpp + ("slice", + "\tslice the program with respect to the target (reachability) or " + "the assertions (--check-asserts) before analysing it; needs " + "sbt-slicer") +``` + +Update the comment block right above `if (args.sliceProgram)` that ends with "Reachability only. Slicing needs a criterion, and Cover-Branches has none -- every branch is the goal. Asking elsewhere is refused, not ignored." so that its last paragraph reads: "Reachability and assert. Slicing needs a criterion, and Cover-Branches has none -- every branch is the goal. Asking elsewhere is refused, not ignored." + +- [ ] **Step 4: Rebuild and run everything** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + cd /workspace/build_aflpp && ninja >/dev/null && ninja install >/dev/null && + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|assert mode|refused|Results"' +``` +Expected: `PASS assert mode slices towards the assertions and still finds the violation`, `PASS --slice is refused where there is no criterion to slice towards`, and `Results: 22 passed, 0 failed`. + +- [ ] **Step 5: CHANGELOG** + +Add at the top of the unreleased section of `CHANGELOG.md`, following its existing format: + +```markdown +- tacasv2a: `--slice` no longer crashes KLEE and its test suites stay valid + on the original program. The slicer runs with `-cutoff-diverging=false` + (the cutoff's `exit(0)` had no debug location and KLEE rejected the + module), and every `__VERIFIER_nondet_*` function is a slicing criterion, + so the read order is preserved. `--slice` now also works with + `--check-asserts`. The slice is logged in functions/blocks/instructions. +``` + +- [ ] **Step 6: Commit** + +```bash +git add modules/frontend/map2check.cpp tests/integration/test_testcomp_regressions.sh CHANGELOG.md +git commit -m "feat(tacasv2a): --slice in assert mode + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` + +--- + +### Task 4: Validation on the diagnostic sample and the CI gates + +**Files:** none changed (verification only). If a check fails, fix it in the task that owns the code and re-run. + +**Interfaces:** +- Consumes: the full build from Tasks 1-3. + +- [ ] **Step 1: Re-run the 12-task diagnostic sample on the finished build** + +The manifest is the one from the spec's §2 (the 12 programs listed there, TSV columns `category program data_model expected_unreach`). Run both arms with the same build, `BUDGET=300 TESTCOV_S=300`, with `tests/testcomp/run_testcomp_evaluation.sh` (`PROPERTY=cover-error`, `EXTRA_FLAGS=""` for control and `EXTRA_FLAGS="--slice"` for the slice arm, `RESULTS_DIR` outside the repository). The container needs `python3-pip zip gcc gcc-multilib lcov` and `pip3 install testcov`. +Expected: the slice arm covers at least 10/12, and `ntdrivers/floppy.i.cil-1.c` is `FAILED,COVERED`. + +- [ ] **Step 2: Run the CI's TestCov step in the dev image** + +```bash +docker run --rm -u root -v $(pwd):/workspace -w /workspace -e MAP2CHECK_PATH=/workspace/build_aflpp/install map2check-dev:aflpp bash -c ' + apt-get update -qq && apt-get install -y -qq python3-pip zip gcc lcov >/dev/null && pip3 install --quiet testcov && + python3 tests/integration/test_benchexec_toolinfo.py 2>&1 | grep Results && + bash tests/integration/test_cover_branches.sh 2>&1 | grep Results && + bash tests/testcomp/run_testcov_suite.sh 2>&1 | grep -E "FAIL|Results"' +``` +Expected: `16 passed`, `5 passed`, `6 passed, 0 failed`. + +- [ ] **Step 3: Record the result** + +Append the sample table to the spec's §2 as "after implementation", then commit: + +```bash +git add docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md +git commit -m "docs(tacasv2a): diagnostic sample re-run on the implementation + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` diff --git a/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md index 3a0ac37b5..5ca6007de 100644 --- a/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md +++ b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md @@ -117,9 +117,12 @@ precisa disso porque não gera suíte a partir da fatia. - `--slice` passa a valer também em `ASSERT_MODE`, com o critério `__VERIFIER_assert`. Os demais modos continuam recusados com aviso, até o 2b e o 2c. -### 5.3 Constante da lista de nondets -- `Map2Check::nondetFunctionNames()` em `utils/tools.hpp`, documentada como a lista que o - slicing preserva, com um comentário apontando para o `NonDetPass`. +### 5.3 Funções puras do slicing +- `modules/frontend/utils/slicer.hpp` (header-only, testável sem build completo): + `nondetFunctionNames()`, `slicingCriteria()`, `targetStubSource()` (o stub de + `__VERIFIER_assert` recebe `int cond`), `parseSlicerStatistics()` e `describeSlice()`. +- Em assert o critério primário é `__VERIFIER_assert,__assert_fail`: o `AssertPass` + instrumenta as duas. --- From 74ecf4a52a3871268cd6f24115744be65e933a73 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 23:47:46 -0400 Subject: [PATCH 17/24] feat(tacasv2a): pure slicing helpers -- criteria, stub, statistics Co-Authored-By: Claude Opus 5.5 (1M context) --- modules/frontend/utils/slicer.hpp | 140 +++++++++++++++++++++++++++++ tests/unit/frontend/CMakeLists.txt | 5 ++ tests/unit/frontend/SlicerTest.cpp | 94 +++++++++++++++++++ 3 files changed, 239 insertions(+) create mode 100644 modules/frontend/utils/slicer.hpp create mode 100644 tests/unit/frontend/SlicerTest.cpp diff --git a/modules/frontend/utils/slicer.hpp b/modules/frontend/utils/slicer.hpp new file mode 100644 index 000000000..271a7c294 --- /dev/null +++ b/modules/frontend/utils/slicer.hpp @@ -0,0 +1,140 @@ +/** + * Copyright (C) 2014 - 2026 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) + **/ + +#ifndef MODULES_FRONTEND_UTILS_SLICER_HPP_ +#define MODULES_FRONTEND_UTILS_SLICER_HPP_ + +#include +#include +#include +#include +#include + +namespace Map2Check { + +/** Every __VERIFIER_nondet_* function the slice must keep. + * + * The suite is generated on the slice, but TestCov runs it on the ORIGINAL + * program. A nondet call the slicer drops -- its value does not reach the + * criterion -- is still consumed by the original, so the vector shifts and + * the suite stops covering (measured: ntdrivers/floppy.i.cil-1.c, 29 reads in + * the program and 10 in the slice; FAILED, NOT_COVERED). Keeping these calls + * as criteria keeps the consumption order. + * + * The first sixteen are what NonDetPass instruments; the rest are SV-COMP + * names it does not model yet, kept so their order is not lost either. The + * slicer accepts names the program does not use. */ +inline const std::vector& nondetFunctionNames() { + static const std::vector names = { + "__VERIFIER_nondet_bool", "__VERIFIER_nondet_char", + "__VERIFIER_nondet_uchar", "__VERIFIER_nondet_short", + "__VERIFIER_nondet_ushort", "__VERIFIER_nondet_int", + "__VERIFIER_nondet_uint", "__VERIFIER_nondet_unsigned", + "__VERIFIER_nondet_long", "__VERIFIER_nondet_ulong", + "__VERIFIER_nondet_size_t", "__VERIFIER_nondet_loff_t", + "__VERIFIER_nondet_sector_t", "__VERIFIER_nondet_pointer", + "__VERIFIER_nondet_pchar", "__VERIFIER_nondet_double", + "__VERIFIER_nondet_float", "__VERIFIER_nondet_longlong", + "__VERIFIER_nondet_ulonglong", "__VERIFIER_nondet__Bool", + "__VERIFIER_nondet_u8", "__VERIFIER_nondet_u16", + "__VERIFIER_nondet_u32", "__VERIFIER_nondet_charp"}; + return names; +} + +/** The -c argument: the primary criteria, then every nondet function. */ +inline std::string slicingCriteria(const std::vector& primary) { + std::ostringstream criteria; + bool first = true; + for (const std::string& name : primary) { + criteria << (first ? "" : ",") << name; + first = false; + } + for (const std::string& name : nondetFunctionNames()) { + criteria << (first ? "" : ",") << name; + first = false; + } + return criteria.str(); +} + +/** A weak definition of the criterion function, restoring the body the + * slicer removes without displacing a real one. The signature must match + * the program's declaration, or llvm-link rejects the module. */ +inline std::string targetStubSource(const std::string& function) { + if (function == "__VERIFIER_assert") { + return "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"; + } + return "void __attribute__((weak)) " + function + "(void) {}\n"; +} + +struct SlicerCounts { + unsigned globals = 0; + unsigned functions = 0; + unsigned blocks = 0; + unsigned instructions = 0; +}; + +struct SlicerStatistics { + bool found = false; // both the "before" and the "after" line were read + SlicerCounts before; + SlicerCounts after; +}; + +/** Reads sbt-slicer's --statistics lines: + * Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764 + * Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989 */ +inline SlicerStatistics parseSlicerStatistics(const std::string& slicerOutput) { + static const std::regex line( + R"(Statistics (before|after) Globals/Functions/Blocks/Instr\.:\s+)" + R"((\d+)\s+(\d+)\s+(\d+)\s+(\d+))"); + SlicerStatistics stats; + bool sawBefore = false; + bool sawAfter = false; + for (std::sregex_iterator it(slicerOutput.begin(), slicerOutput.end(), line), + end; + it != end; ++it) { + const std::smatch& m = *it; + SlicerCounts counts; + counts.globals = static_cast(std::stoul(m[2])); + counts.functions = static_cast(std::stoul(m[3])); + counts.blocks = static_cast(std::stoul(m[4])); + counts.instructions = static_cast(std::stoul(m[5])); + if (m[1] == "before") { + stats.before = counts; + sawBefore = true; + } else { + stats.after = counts; + sawAfter = true; + } + } + stats.found = sawBefore && sawAfter; + return stats; +} + +/** The one log line a slice produces. Counts when the slicer reported them, + * bytes always -- a slice narrows the question being answered, and this line + * is the only visible sign of how much was dropped. */ +inline std::string describeSlice(const std::string& criterion, + const SlicerStatistics& stats, + uintmax_t bytesBefore, uintmax_t bytesAfter) { + std::ostringstream text; + text << "Sliced with respect to " << criterion << ": "; + if (stats.found) { + text << stats.before.functions << "/" << stats.before.blocks << "/" + << stats.before.instructions << " -> " << stats.after.functions << "/" + << stats.after.blocks << "/" << stats.after.instructions + << " functions/blocks/instructions (" << bytesBefore << " -> " + << bytesAfter << " bytes of bitcode)"; + } else { + text << bytesBefore << " -> " << bytesAfter << " bytes of bitcode"; + } + return text.str(); +} + +} // namespace Map2Check + +#endif // MODULES_FRONTEND_UTILS_SLICER_HPP_ diff --git a/tests/unit/frontend/CMakeLists.txt b/tests/unit/frontend/CMakeLists.txt index c4ecc97f0..35d6a0390 100644 --- a/tests/unit/frontend/CMakeLists.txt +++ b/tests/unit/frontend/CMakeLists.txt @@ -15,3 +15,8 @@ add_executable(KtestReaderTest $ ) map2check_test(KtestReaderTest) + +add_executable(SlicerTest + SlicerTest.cpp +) +map2check_test(SlicerTest) diff --git a/tests/unit/frontend/SlicerTest.cpp b/tests/unit/frontend/SlicerTest.cpp new file mode 100644 index 000000000..eceb83718 --- /dev/null +++ b/tests/unit/frontend/SlicerTest.cpp @@ -0,0 +1,94 @@ +/** + * Copyright (C) 2014 - 2026 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 + +#include +#include +#include + +#include "../../../modules/frontend/utils/slicer.hpp" + +// The suite is generated on the slice and run by TestCov on the ORIGINAL +// program, so every nondet read the original performs must survive slicing. +TEST(SlicingCriteria, AppendsEveryNondetFunctionAfterThePrimary) { + const std::string criteria = Map2Check::slicingCriteria({"reach_error"}); + EXPECT_EQ(criteria.rfind("reach_error,", 0), 0u); + for (const std::string& name : Map2Check::nondetFunctionNames()) { + EXPECT_NE(criteria.find("," + name), std::string::npos) << name; + } +} + +TEST(SlicingCriteria, KeepsSeveralPrimariesInOrder) { + const std::string criteria = + Map2Check::slicingCriteria({"__VERIFIER_assert", "__assert_fail"}); + EXPECT_EQ(criteria.rfind("__VERIFIER_assert,__assert_fail,", 0), 0u); +} + +TEST(NondetFunctionNames, CoversWhatNonDetPassInstruments) { + const auto& names = Map2Check::nondetFunctionNames(); + for (const char* type : {"bool", "char", "uchar", "short", "ushort", "int", + "uint", "unsigned", "long", "ulong", "size_t", + "loff_t", "sector_t", "pointer", "pchar", "double"}) { + const std::string name = std::string("__VERIFIER_nondet_") + type; + EXPECT_NE(std::find(names.begin(), names.end(), name), names.end()) << name; + } +} + +TEST(TargetStubSource, VoidTargetGetsAVoidStub) { + EXPECT_EQ(Map2Check::targetStubSource("reach_error"), + "void __attribute__((weak)) reach_error(void) {}\n"); +} + +// __VERIFIER_assert takes the condition; a (void) stub would not link against +// the program's own declaration. +TEST(TargetStubSource, AssertStubTakesTheCondition) { + EXPECT_EQ(Map2Check::targetStubSource("__VERIFIER_assert"), + "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"); +} + +TEST(ParseSlicerStatistics, ReadsBeforeAndAfter) { + const std::string output = + "Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764\n" + "[llvm-slicer] Sliced away 1454 from 4227 nodes in DG\n" + "Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989\n"; + const Map2Check::SlicerStatistics stats = + Map2Check::parseSlicerStatistics(output); + ASSERT_TRUE(stats.found); + EXPECT_EQ(stats.before.functions, 97u); + EXPECT_EQ(stats.before.blocks, 2215u); + EXPECT_EQ(stats.before.instructions, 10764u); + EXPECT_EQ(stats.after.globals, 37u); + EXPECT_EQ(stats.after.functions, 38u); + EXPECT_EQ(stats.after.instructions, 2989u); +} + +// A slicer that prints no statistics must not be reported as having sliced +// everything away. +TEST(ParseSlicerStatistics, MissingLinesAreNotFound) { + EXPECT_FALSE(Map2Check::parseSlicerStatistics("").found); + EXPECT_FALSE(Map2Check::parseSlicerStatistics( + "Statistics before Globals/Functions/Blocks/Instr.: 1 2 3 4\n") + .found); +} + +TEST(DescribeSlice, ReportsCountsWhenFound) { + Map2Check::SlicerStatistics stats; + stats.found = true; + stats.before = {37, 97, 2215, 10764}; + stats.after = {37, 38, 444, 2989}; + EXPECT_EQ(Map2Check::describeSlice("reach_error", stats, 184164, 171708), + "Sliced with respect to reach_error: 97/2215/10764 -> 38/444/2989 " + "functions/blocks/instructions (184164 -> 171708 bytes of " + "bitcode)"); +} + +TEST(DescribeSlice, FallsBackToBytesWithoutStatistics) { + EXPECT_EQ(Map2Check::describeSlice("reach_error", {}, 10, 8), + "Sliced with respect to reach_error: 10 -> 8 bytes of bitcode"); +} From 336a26d1c5984bc634e3aafc925316c413aba485 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 26 Sep 2026 23:57:45 -0400 Subject: [PATCH 18/24] fix(tacasv2a): slice without cutoff and keep every nondet read The cutoff's exit(0) carries no !dbg and KLEE rejected every sliced module with a cut path; nondet reads the slicer dropped shifted the suite on the original program. Both are integration-tested now, and the slice is logged in functions/blocks/instructions, not only bytes. Co-Authored-By: Claude Opus 5.5 (1M context) --- modules/frontend/caller.cpp | 39 +++++++--- modules/frontend/caller.hpp | 15 +++- modules/frontend/map2check.cpp | 2 +- .../integration/test_testcomp_regressions.sh | 74 +++++++++++++++++++ 4 files changed, 116 insertions(+), 14 deletions(-) diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index d6584a0f8..e9f914093 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -22,6 +22,7 @@ #include #include #include +#include #include #include #include @@ -30,6 +31,7 @@ #include "test_suite/ktest_reader.hpp" #include "utils/gen_crypto_hash.hpp" #include "utils/log.hpp" +#include "utils/slicer.hpp" #include "utils/tools.hpp" // namespace fs = boost::filesystem; // } // namespace @@ -176,7 +178,8 @@ std::string Caller::exportFuzzerVectorAsKtest() { return path; } -bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { +bool Caller::sliceWithRespectToTarget(const std::string &targetFunction, + const std::vector &criteria) { const std::string slicer = Map2Check::slicerBinary(); if (!std::filesystem::exists(slicer)) { // Announced, not silently skipped. A slicer that is asked for and absent @@ -218,10 +221,21 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { 1.0, std::min(0.2 * this->timeout, std::max(1.0, static_cast(remainingSeconds()) - 5.0))); - command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(sliceBudget) - << " " << slicer << " -c " << targetFunction - << " --entry=main -o " << output << " " - << input << " > slicer.output 2>&1"; + // -cutoff-diverging=false: the cutoff rewrites every path that cannot reach + // the criterion into exit(0) with no debug location, and once KLEE links + // uClibc the verifier rejects the module ("Broken module found") -- KLEE + // never ran on a sliced task with a cut path (tacasv2a spec, defect 1). + // + // The nondet functions ride along as criteria so that every read the + // original program performs survives; the suite is generated on the slice + // and replayed on the original (defect 2). + // + // --statistics: counts before and after, logged below. + command << "timeout -k " << Map2Check::killGracePeriod << " " + << static_cast(sliceBudget) << " " << slicer << " -c " + << Map2Check::slicingCriteria(criteria) + << " --entry=main -cutoff-diverging=false --statistics -o " << output + << " " << input << " > slicer.output 2>&1"; Map2Check::Log::Debug(command.str()); const int result = system(command.str().c_str()); @@ -240,9 +254,16 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { // of how much was dropped. const auto before = std::filesystem::file_size(input, error); const auto after = std::filesystem::file_size(output, error); - Map2Check::Log::Info("Sliced with respect to " + targetFunction + ": " + - std::to_string(before) + " -> " + - std::to_string(after) + " bytes of bitcode"); + std::ifstream slicerLog("slicer.output"); + std::stringstream slicerText; + slicerText << slicerLog.rdbuf(); + std::string criterionLabel; + for (const std::string &name : criteria) { + criterionLabel += (criterionLabel.empty() ? "" : ",") + name; + } + Map2Check::Log::Info(Map2Check::describeSlice( + criterionLabel, Map2Check::parseSlicerStatistics(slicerText.str()), + before, after)); // sbt-slicer removes the body of the criterion function itself. reach_error // is where the slice ENDS -- nothing it does can influence whether it is @@ -266,7 +287,7 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { { std::ofstream stub(stubSource); if (stub.is_open()) { - stub << "void __attribute__((weak)) " << targetFunction << "(void) {}\n"; + stub << Map2Check::targetStubSource(targetFunction); } } std::ostringstream compileStub; diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 7119d0699..0c8675034 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -130,10 +130,17 @@ class Caller { * decision the caller makes rather than a default. */ bool sliceProgram = false; - /** Runs sbt-slicer over the instrumented bitcode. Returns false if the - * slicer is unavailable or produced nothing usable, leaving the original - * bitcode in place. */ - bool sliceWithRespectToTarget(const std::string& targetFunction); + /** Runs sbt-slicer over the compiled (not yet instrumented) bitcode. + * + * `criteria` are the primary slicing criteria (the target function, or the + * assert functions); every __VERIFIER_nondet_* function is added to them so + * the suite found on the slice stays valid on the original program. The + * cutoff of diverging paths is off: its exit(0) carries no debug location + * and KLEE rejects the module. `targetFunction` gets its body back through a + * weak stub. Returns false if the slicer is unavailable or produced nothing + * usable, leaving the original bitcode in place. */ + bool sliceWithRespectToTarget(const std::string& targetFunction, + const std::vector& criteria); /** Turns on the exchange of input vectors between the two engines. * diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index cd5e7f91e..115f43b3e 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -518,7 +518,7 @@ int map2check_execution(map2check_args args) { // -- every branch is the goal. Asking elsewhere is refused, not ignored. if (args.sliceProgram) { if (args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE) { - caller->sliceWithRespectToTarget(args.function); + caller->sliceWithRespectToTarget(args.function, {args.function}); } else { Map2Check::Log::Warning( "--slice applies to reachability only: there is no criterion to " diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index d3b187fa9..f969222c5 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -522,6 +522,80 @@ else fail "slice mode guard" "--slice was accepted in a mode that has no criterion" fi +# --- 13. a slice must leave KLEE something it can run ------------------------- +# sbt-slicer's --cutoff-diverging (default on) rewrites every path that cannot +# reach the criterion into a `diverge:` block calling exit(0) -- with no debug +# location. The program is compiled with -g; once KLEE links uClibc, exit has a +# body, and the verifier rejects the module ("inlinable function call in a +# function with debug info must have a !dbg location"). KLEE aborted before +# executing anything, on every sliced task with a cut path: the slice arm of +# the v15 campaign ran without its symbolic engine. +mkdir -p "$WORK/cut" +# ECA-shaped on purpose: the slicer turns a plain return from main into a +# `safe_return`, so a straight-line program never gets a `diverge:` block. A +# reactive loop whose step can take a path that never reaches the target does; +# bounded to two steps so that KLEE decides it well inside the budget. +cat > "$WORK/cut/cut.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +extern void exit(int); +int a = 1; +void step(int in) { + if (in == 5) { a = 2; return; } + if (in == 6 && a == 2) { reach_error(); } + if (in == 9) { exit(0); } +} +int main(void) { + for (int i = 0; i < 2; i++) { + int in = __VERIFIER_nondet_int(); + step(in); + } + return 0; +} +EOF +( cd "$WORK/cut" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --timeout 45 cut.c ) > "$WORK/cut/run.log" 2>&1 +if grep -q "Broken module" "$WORK/cut/run.log"; then + fail "slice + KLEE" "KLEE rejected the sliced module (cutoff exit without !dbg)" +elif grep -q "VERIFICATION FAILED" "$WORK/cut/run.log"; then + ok "KLEE runs on the slice and reaches the target" +else + fail "slice + KLEE" "no FAILED verdict on a trivially reachable target" + grep -E "Sliced|Exited klee|VERIFICATION" "$WORK/cut/run.log" | sed 's/^/ /' +fi + +# --- 14. a suite found on the slice must hold on the original ---------------- +# TestCov runs the suite on the ORIGINAL program. A nondet read the slicer +# dropped -- its value does not reach the target -- is still consumed there, +# so the vector shifts: measured on ntdrivers/floppy.i.cil-1.c, FAILED and +# NOT_COVERED. The slice keeps every nondet call, so both values appear, in +# the original order. +mkdir -p "$WORK/order" +cp "$WORK/one/reach.prp" "$WORK/order/" +cat > "$WORK/order/order.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (b == 42) { reach_error(); } + return a; +} +EOF +( cd "$WORK/order" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --generate-test-suite --property-file reach.prp \ + --timeout 60 order.c ) > "$WORK/order/run.log" 2>&1 +order_inputs=$(sed -n 's:.*\(.*\).*:\1:p' \ + "$WORK/order/test-suite/testcase-1.xml" 2>/dev/null | tr '\n' ' ') +if [ "$(echo $order_inputs | wc -w)" -eq 2 ] && \ + [ "$(echo $order_inputs | awk '{print $2}')" = "42" ]; then + ok "the sliced suite keeps the original read order [$order_inputs]" +else + fail "slice read order" "expected 2 inputs ending in 42, got [$order_inputs]" +fi + echo " ---" echo " Results: $PASSED passed, $FAILED failed" [ "$FAILED" -eq 0 ] || exit 1 From c36a532e704be6cbdba445cae21f26d0f6492d9c Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 27 Sep 2026 00:01:15 -0400 Subject: [PATCH 19/24] feat(tacasv2a): --slice in assert mode Co-Authored-By: Claude Opus 5.5 (1M context) --- CHANGELOG.md | 6 ++++ modules/frontend/map2check.cpp | 21 +++++++++----- .../integration/test_testcomp_regressions.sh | 29 ++++++++++++++++++- 3 files changed, 48 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c1d035f7d..ff411b8a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,12 @@ 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. +- tacasv2a: `--slice` no longer crashes KLEE and its test suites stay valid + on the original program. The slicer runs with `-cutoff-diverging=false` + (the cutoff's `exit(0)` had no debug location and KLEE rejected the + module), and every `__VERIFIER_nondet_*` function is a slicing criterion, + so the read order is preserved. `--slice` now also works with + `--check-asserts`. The slice is logged in functions/blocks/instructions. - 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/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index 115f43b3e..48858ecad 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -514,16 +514,22 @@ int map2check_execution(map2check_args args) { // properties: the search space is smaller and the instrumentation is added // to what survives. // - // Reachability only. Slicing needs a criterion, and Cover-Branches has none - // -- every branch is the goal. Asking elsewhere is refused, not ignored. + // Reachability and assert. Slicing needs a criterion, and Cover-Branches has + // none -- every branch is the goal. Asking elsewhere is refused, not ignored. + // Reachability slices towards the target; assert towards the two functions + // AssertPass instruments. Memory properties and overflow need their own + // criteria (tacasv2b/2c). if (args.sliceProgram) { if (args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE) { caller->sliceWithRespectToTarget(args.function, {args.function}); + } else if (args.mode == Map2Check::Map2CheckMode::ASSERT_MODE) { + caller->sliceWithRespectToTarget("__VERIFIER_assert", + {"__VERIFIER_assert", "__assert_fail"}); } else { Map2Check::Log::Warning( - "--slice applies to reachability only: there is no criterion to " - "slice towards when the goal is coverage or a memory property. " - "Analysing the whole program."); + "--slice applies to reachability and assert only: there is no " + "criterion to slice towards when the goal is coverage or a memory " + "or overflow property. Analysing the whole program."); } } @@ -751,8 +757,9 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") ("test-suite-dir", po::value()->default_value("test-suite"), "\tdirectory to write the test suite into") ("slice", - "\tslice the program with respect to the target before analysing it " - "(reachability only; needs sbt-slicer)") + "\tslice the program with respect to the target (reachability) or " + "the assertions (--check-asserts) before analysing it; needs " + "sbt-slicer") ("seed-exchange", "\tlet the two engines hand each other input vectors through a shared " "seed corpus (hybrid runs; off by default)") diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index f969222c5..abcca18c5 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -516,7 +516,7 @@ fi ( cd "$WORK/slice" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ --memtrack --slice --nondet-generator symex --timeout 45 reach.c ) \ > "$WORK/slice/mode.log" 2>&1 -if grep -q "applies to reachability only" "$WORK/slice/mode.log"; then +if grep -q "applies to reachability and assert only" "$WORK/slice/mode.log"; then ok "--slice is refused where there is no criterion to slice towards" else fail "slice mode guard" "--slice was accepted in a mode that has no criterion" @@ -596,6 +596,33 @@ else fail "slice read order" "expected 2 inputs ending in 42, got [$order_inputs]" fi +# --- 15. assert mode slices towards the assertions ---------------------------- +# AssertPass instruments __VERIFIER_assert and __assert_fail, so those are the +# criteria. The program only DECLARES __VERIFIER_assert: the weak stub must +# take the condition, or llvm-link rejects the (void) definition. +mkdir -p "$WORK/assert" +cat > "$WORK/assert/assert.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void __VERIFIER_assert(int cond); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (a > 0) { a = a - 1; } + __VERIFIER_assert(b != 77); + return a; +} +EOF +( cd "$WORK/assert" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --check-asserts --slice --nondet-generator symex --timeout 45 assert.c ) \ + > "$WORK/assert/run.log" 2>&1 +if grep -q "Sliced with respect to __VERIFIER_assert,__assert_fail" "$WORK/assert/run.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/assert/run.log"; then + ok "assert mode slices towards the assertions and still finds the violation" +else + fail "assert slice" "no assert-criterion slice, or the violation was lost" + grep -E "Sliced|slice|VERIFICATION" "$WORK/assert/run.log" | sed 's/^/ /' +fi + echo " ---" echo " Results: $PASSED passed, $FAILED failed" [ "$FAILED" -eq 0 ] || exit 1 From 75bdefd66d68b8512bc6c94d6279b3361ff75649 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 27 Sep 2026 00:19:29 -0400 Subject: [PATCH 20/24] docs(tacasv2a): diagnostic sample re-run on the implementation Control 12/12, slice 12/12 on the 12 tasks the v15 slice arm lost. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../2026-09-26-tacasv2a-slicing-reach-assert-design.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md index 5ca6007de..73e66b7f0 100644 --- a/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md +++ b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md @@ -36,6 +36,12 @@ famílias). Build tacasv1, orçamento de 300 s, TestCov 300 s, uma execução po As duas tarefas que a última variante não cobriu terminaram perto do orçamento (~258 s). Com uma execução por braço, não dá para separar isso de variação. +**Depois da implementação** (2026-09-27, build final da `tacas/slicing`, mesma amostra e +orçamento, uma execução por braço): controle **12/12**, slice **12/12**. `floppy.i.cil-1` +dá FAILED + COVERED com slice. O slice terminou antes do controle em 5 das 9 tarefas ECA +(por exemplo, `Problem17_label55`: FAILED em 51 s, contra UNKNOWN em 137 s no controle). +São 12 tarefas: é validação de que os defeitos sumiram, não avaliação (§7). + ### Defeito 1 — o KLEE aborta em toda fatia com caminho cortado - O `--cutoff-diverging` (default `true` no dg/sbt-slicer) insere um bloco `diverge:` From ffad3e5d0425bc4d43e489c28990c390f2a1bc69 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 27 Sep 2026 00:29:52 -0400 Subject: [PATCH 21/24] fix(tacasv2a): take the nondet names from the program as well The fixed list cannot know every __VERIFIER_nondet_* a benchmark declares (int128, uint128, ...), and a missing name silently brings the shifted suite back. The slicer input is disassembled with opt -S and every nondet symbol joins the criteria; the fixed list is the fallback. Co-Authored-By: Claude Opus 5.5 (1M context) --- modules/frontend/caller.cpp | 18 +++++++- modules/frontend/utils/slicer.hpp | 43 ++++++++++++++----- .../integration/test_testcomp_regressions.sh | 27 ++++++++++++ tests/unit/frontend/SlicerTest.cpp | 30 +++++++++++++ 4 files changed, 107 insertions(+), 11 deletions(-) diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index e9f914093..5e64ec14b 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -231,9 +231,25 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction, // and replayed on the original (defect 2). // // --statistics: counts before and after, logged below. + // The program's own nondet names join the fixed list: no fixed list knows + // every name a benchmark declares, and a missing one silently shifts the + // suite again. Read from the textual IR -- the bitcode string table packs + // names with no separator. If the disassembly fails, the fixed list stands. + const std::string inputIR = programHash + "-slice-input.ll"; + std::ostringstream disassemble; + disassemble << Map2Check::optBinary << " -S " << input << " -o " << inputIR + << " > /dev/null 2>&1"; + std::vector programNondets; + if (system(disassemble.str().c_str()) == 0) { + std::ifstream irFile(inputIR); + std::stringstream irText; + irText << irFile.rdbuf(); + programNondets = Map2Check::nondetNamesInIR(irText.str()); + } + command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(sliceBudget) << " " << slicer << " -c " - << Map2Check::slicingCriteria(criteria) + << Map2Check::slicingCriteria(criteria, programNondets) << " --entry=main -cutoff-diverging=false --statistics -o " << output << " " << input << " > slicer.output 2>&1"; Map2Check::Log::Debug(command.str()); diff --git a/modules/frontend/utils/slicer.hpp b/modules/frontend/utils/slicer.hpp index 271a7c294..c96b91cf6 100644 --- a/modules/frontend/utils/slicer.hpp +++ b/modules/frontend/utils/slicer.hpp @@ -9,6 +9,7 @@ #ifndef MODULES_FRONTEND_UTILS_SLICER_HPP_ #define MODULES_FRONTEND_UTILS_SLICER_HPP_ +#include #include #include #include @@ -46,17 +47,39 @@ inline const std::vector& nondetFunctionNames() { return names; } -/** The -c argument: the primary criteria, then every nondet function. */ -inline std::string slicingCriteria(const std::vector& primary) { - std::ostringstream criteria; - bool first = true; - for (const std::string& name : primary) { - criteria << (first ? "" : ",") << name; - first = false; +/** Every __VERIFIER_nondet_* symbol in a module's textual IR (`opt -S`), + * in order of first appearance. The fixed list above cannot know every name a + * benchmark declares (int128, uint128, ...), and a name missing from the + * criteria silently brings the shifted suite back. */ +inline std::vector nondetNamesInIR(const std::string& ir) { + static const std::regex symbol(R"(@(__VERIFIER_nondet_[A-Za-z0-9_]+))"); + std::vector names; + for (std::sregex_iterator it(ir.begin(), ir.end(), symbol), end; it != end; + ++it) { + const std::string name = (*it)[1]; + if (std::find(names.begin(), names.end(), name) == names.end()) { + names.push_back(name); + } } - for (const std::string& name : nondetFunctionNames()) { - criteria << (first ? "" : ",") << name; - first = false; + return names; +} + +/** The -c argument: the primary criteria, then every nondet function -- the + * fixed list plus `fromProgram` (nondetNamesInIR), each name once. */ +inline std::string slicingCriteria( + const std::vector& primary, + const std::vector& fromProgram = {}) { + std::vector all(primary); + auto add = [&all](const std::string& name) { + if (std::find(all.begin(), all.end(), name) == all.end()) { + all.push_back(name); + } + }; + for (const std::string& name : nondetFunctionNames()) add(name); + for (const std::string& name : fromProgram) add(name); + std::ostringstream criteria; + for (size_t i = 0; i < all.size(); ++i) { + criteria << (i == 0 ? "" : ",") << all[i]; } return criteria.str(); } diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index abcca18c5..74789b97d 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -623,6 +623,33 @@ else grep -E "Sliced|slice|VERIFICATION" "$WORK/assert/run.log" | sed 's/^/ /' fi +# --- 16. nondet names the fixed list does not know are kept too -------------- +# The criteria carry a fixed list of __VERIFIER_nondet_* names, and no fixed +# list knows every name a benchmark declares (int128, uint128, ...). A missing +# one silently brings back the shifted suite of section 14, so the names are +# also read from the program. Checked on the slicer command itself: int128 is +# not in the fixed list, so its presence there proves it came from the program. +mkdir -p "$WORK/names" +cat > "$WORK/names/names.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern __int128 __VERIFIER_nondet_int128(void); +extern void reach_error(void); +int main(void) { + __int128 wide = __VERIFIER_nondet_int128(); + int b = __VERIFIER_nondet_int(); + if (b == 42) { reach_error(); } + return (int)wide; +} +EOF +( cd "$WORK/names" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice --debug \ + --nondet-generator symex --timeout 30 names.c ) > "$WORK/names/run.log" 2>&1 +if grep "sbt-slicer" "$WORK/names/run.log" | grep -q "__VERIFIER_nondet_int128"; then + ok "nondet names declared by the program are slicing criteria too" +else + fail "program nondet names" "__VERIFIER_nondet_int128 is not among the criteria" +fi + echo " ---" echo " Results: $PASSED passed, $FAILED failed" [ "$FAILED" -eq 0 ] || exit 1 diff --git a/tests/unit/frontend/SlicerTest.cpp b/tests/unit/frontend/SlicerTest.cpp index eceb83718..9a312b809 100644 --- a/tests/unit/frontend/SlicerTest.cpp +++ b/tests/unit/frontend/SlicerTest.cpp @@ -92,3 +92,33 @@ TEST(DescribeSlice, FallsBackToBytesWithoutStatistics) { EXPECT_EQ(Map2Check::describeSlice("reach_error", {}, 10, 8), "Sliced with respect to reach_error: 10 -> 8 bytes of bitcode"); } + +// The fixed list cannot know every name a benchmark declares (int128, +// uint128, ...); a name missing from the criteria silently reintroduces the +// shifted suite. The names come from the program itself as well. +TEST(NondetNamesInIR, FindsEveryDeclaredOrCalledNondetFunction) { + const std::string ir = + "declare i32 @__VERIFIER_nondet_int()\n" + "declare i128 @__VERIFIER_nondet_int128()\n" + " %1 = call i128 @__VERIFIER_nondet_int128(), !dbg !19\n" + " call void @reach_error()\n" + "@__VERIFIER_nondet_not_a_call = global i32 0\n"; + const std::vector names = Map2Check::nondetNamesInIR(ir); + ASSERT_EQ(names.size(), 3u); + EXPECT_EQ(names[0], "__VERIFIER_nondet_int"); + EXPECT_EQ(names[1], "__VERIFIER_nondet_int128"); + EXPECT_EQ(names[2], "__VERIFIER_nondet_not_a_call"); +} + +TEST(SlicingCriteria, AddsNamesFromTheProgramOnceEach) { + const std::string criteria = Map2Check::slicingCriteria( + {"reach_error"}, {"__VERIFIER_nondet_int128", "__VERIFIER_nondet_int"}); + EXPECT_NE(criteria.find(",__VERIFIER_nondet_int128"), std::string::npos); + size_t count = 0; + for (size_t at = criteria.find("__VERIFIER_nondet_int,"); + at != std::string::npos; + at = criteria.find("__VERIFIER_nondet_int,", at + 1)) { + ++count; + } + EXPECT_EQ(count, 1u); +} From 0b0e855e76689e3fbec780e3bdeb0d9ad7c1c90d Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 27 Sep 2026 00:31:23 -0400 Subject: [PATCH 22/24] ci: run the PR gates on PRs stacked on tacas/** branches Co-Authored-By: Claude Opus 5.5 (1M context) --- .github/workflows/ci.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 95fb3c08c..ea1dfc1b7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,9 +23,10 @@ on: # Inclui feat/** como ALVO para que PRs empilhadas sejam verificadas. Sem isso # uma PR cuja base é outra branch de feature não dispara nada -- a #56 abriu # com um único check -- e os gates de regressão que ela própria adiciona nunca - # rodariam nela. + # rodariam nela. Idem 'tacas/**': a linha TACAS empilha tacas/slicing sobre + # tacas/aflpp. pull_request: - branches: [develop, main, master, 'feat/**'] + branches: [develop, main, master, 'feat/**', 'tacas/**'] jobs: # =========================================================== From 8eb66b34127bcc61d3938414c2590140682ec504 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 27 Sep 2026 00:39:54 -0400 Subject: [PATCH 23/24] Revert "ci: run the PR gates on PRs stacked on tacas/** branches" Branch naming follows feat/** instead. Co-Authored-By: Claude Opus 5.5 (1M context) --- .github/workflows/ci.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ea1dfc1b7..95fb3c08c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,10 +23,9 @@ on: # Inclui feat/** como ALVO para que PRs empilhadas sejam verificadas. Sem isso # uma PR cuja base é outra branch de feature não dispara nada -- a #56 abriu # com um único check -- e os gates de regressão que ela própria adiciona nunca - # rodariam nela. Idem 'tacas/**': a linha TACAS empilha tacas/slicing sobre - # tacas/aflpp. + # rodariam nela. pull_request: - branches: [develop, main, master, 'feat/**', 'tacas/**'] + branches: [develop, main, master, 'feat/**'] jobs: # =========================================================== From 5a4e2fb8df3f8b8c0854e0b2a60b3d36422a1d7c Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 27 Sep 2026 12:26:12 -0400 Subject: [PATCH 24/24] test(tacasv1): the evaluation runner's fuzzer arm is GENERATOR=afl GENERATOR=fuzzer still passed --nondet-generator fuzzer, which the CLI no longer accepts. It now names AFL++, and the old value is refused with a pointer to the new one rather than silently measuring nothing. Co-Authored-By: Claude Opus 5.5 (1M context) --- tests/testcomp/run_testcomp_evaluation.sh | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/tests/testcomp/run_testcomp_evaluation.sh b/tests/testcomp/run_testcomp_evaluation.sh index c47b969bf..c587bb34b 100755 --- a/tests/testcomp/run_testcomp_evaluation.sh +++ b/tests/testcomp/run_testcomp_evaluation.sh @@ -47,8 +47,10 @@ DEADLINE_S="${DEADLINE_S:-18000}" # compared on the SAME task list: # # symex KLEE only -- every Test-Comp measurement before 2026-08-23 -# fuzzer LibFuzzer only -# hybrid the tool's actual default: LibFuzzer at 0.2x, then KLEE +# afl AFL++ only (tacasv1 onwards; `fuzzer` was LibFuzzer and is +# refused -- the engine is gone, and a result dir named for it +# would mix two engines) +# hybrid the tool's actual default: the fuzzer at 0.2x, then KLEE # hybrid-seed the same, with the two engines exchanging input vectors # # The default is hybrid, which is also the tool's own default when no @@ -67,7 +69,8 @@ GENERATOR="${GENERATOR:-hybrid}" # engine is running. EXTRA_FLAGS="${EXTRA_FLAGS:-}" case "$GENERATOR" in - symex|fuzzer) GENERATOR_FLAG="--nondet-generator $GENERATOR" ;; + symex|afl) GENERATOR_FLAG="--nondet-generator $GENERATOR" ;; + fuzzer) echo "GENERATOR=fuzzer was LibFuzzer, which AFL++ replaced -- use GENERATOR=afl" >&2; exit 2 ;; hybrid) GENERATOR_FLAG="" ;; # absent flag IS the hybrid path hybrid-seed) GENERATOR_FLAG="--seed-exchange" ;; *) echo "unknown GENERATOR: $GENERATOR" >&2; exit 2 ;;