tacasv2a: --slice that keeps the suite valid (reach + assert)

.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 \

.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.
 ############################################################

CHANGELOG.md

@@ -7,6 +7,13 @@ 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.

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,15 +39,15 @@ 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
 ```
 
 ### Key CMake flags
 
 | 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<Name>.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
 

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)
@@ -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.
 #
@@ -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)

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 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)" && \
+    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

README.md

@@ -12,7 +12,7 @@ ___
 <b>Map2Check</b> is a bug hunting tool that automatically generates and checks safety properties in C programs and <b>WebAssembly (WASM) binaries</b>.
 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 <b>lifting</b> `.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

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
 

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
+# the previous fuzzer find-module 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 MAP2CHECK_AFL_CC/MAP2CHECK_AFL_FUZZ at run time.")
+endif()

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