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..ff411b8a9 100644 --- a/CHANGELOG.md +++ b/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. 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/CMakeLists.txt b/CMakeLists.txt index e5786b19b..a10f305e4 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) @@ -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) diff --git a/Dockerfile.dev b/Dockerfile.dev index e43d5f14e..9a8080ba2 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 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 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 new file mode 100644 index 000000000..ddb75e729 --- /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 +# 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() 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() 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/docs/reports/tacas-experiment-log.md b/docs/reports/tacas-experiment-log.md new file mode 100644 index 000000000..adbed7c00 --- /dev/null +++ b/docs/reports/tacas-experiment-log.md @@ -0,0 +1,288 @@ +# Registro de mini-rodadas — linha TACAS + +Uma entrada por mini-rodada de testes, na ordem em que foram feitas. Cada entrada tem +o que mudou, a configuração, os dados brutos, a comparação com a rodada anterior +relevante e a leitura. Os números aqui são **diagnóstico** (amostras pequenas, uma ou +poucas execuções); a avaliação de cada versão é a execução sequencial completa, feita +depois do merge. + +Ambiente comum: imagem `map2check-dev:aflpp` (Dockerfile.dev com AFL++ 4.40c), host +WSL2. Build da v15 = `develop` em `415032766`, no mesmo container. + +--- + +## R1 — tacasv1: smoke do AFL++ (2026-09-26) + +- **Mudança:** LibFuzzer → AFL++ 4.40c (persistente, PCGUARD), 1 instância. +- **Config:** 4 programas mínimos, `--timeout 30`. +- **Dados:** + +| programa | esperado | resultado | +|---|---|---| +| reach `x != 0` (a semente já causa crash) | FAILED | FAILED 3/3 (1 timeout no dry-run por core dump do WSL em outra execução) | +| reach `1000 **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/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/plans/2026-09-27-tacasv2b-slicing-memsafety.md b/docs/superpowers/plans/2026-09-27-tacasv2b-slicing-memsafety.md new file mode 100644 index 000000000..01002cf3d --- /dev/null +++ b/docs/superpowers/plans/2026-09-27-tacasv2b-slicing-memsafety.md @@ -0,0 +1,377 @@ +# tacasv2b — Slicing for memtrack/memcleanup: 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` work with `--memtrack` and `--memcleanup-property`, by slicing the instrumented module with every runtime call as a criterion. Also add an SV-COMP MemSafety evaluation harness, and let the CASTLE and Juliet runners take extra flags. + +**Architecture:** +- **Shared slicer helper.** The slicer invocation is factored out of `sliceWithRespectToTarget` into a private `Caller::runSlicer` helper. It handles disassembly, criteria, budget, statistics and fallback. +- **New `Caller::sliceInstrumented()`.** It uses the helper on `-output.bc`, between `callPass` and `linkLLVM`. The criteria are every `@map2check_*` symbol plus every nondet function, and the entry is `__map2check_main__`. +- **Harness.** It reuses `build_corpus.py`, with directory-based categories for memory, plus a new runner and a tested classifier. + +**Tech Stack:** C++17, LLVM 16, sbt-slicer, GTest, bash, python3. Build and run everything in `map2check-dev:aflpp`. Build dirs: +- `build_aflpp`, install prefix pinned to `/workspace/build_aflpp/install`; +- `build_aflpp_ut`, with `ENABLE_TEST=ON`. + +**Spec:** `docs/superpowers/specs/2026-09-27-tacasv2b-slicing-memsafety-design.md` + +## Global Constraints + +- Branch `feat/tacas-slicing-mem` (from `feat/tacas-slicing`). Baseline tacasv1; nothing targets LibFuzzer. +- Memory criteria: every `@map2check_*` symbol in the instrumented IR, plus the fixed nondet list, plus the nondet names found in the IR. +- Slicer flags: `--entry=__map2check_main__ -cutoff-diverging=false --statistics`. +- Slicing order: for reach/assert, before `callPass` (unchanged); for memtrack/memcleanup, after `callPass` and before `linkLLVM`. Overflow and cover-branches are still refused. +- Refusal message: `--slice applies to reachability, assert and memory properties only`. +- On any slicer failure, fall back to the unsliced module with a warning. Never abort the run. +- Every mini-round is appended to `docs/reports/tacas-experiment-log.md` and compared with the previous one (standing rule). +- Commits end with `Co-Authored-By: Claude Opus 5.5 (1M context) `. + +## Review Focus + +- **Instrumented modules that call a runtime function only through a declaration never called.** The criterion is harmless (verified in 2a); nothing to pin beyond the unit test. +- **A VLA/`llvm.stacksave` program.** The slicer errors, the run must fall back and keep the unsliced verdict. Pinned in Task 2 (integration test 20). +- **A safe program must never become FALSE because of slicing** (a spurious violation). Pinned in Task 2 (test 19). +- **A FALSE with the wrong subproperty** (e.g. FALSE-FREE on a valid-deref task) must count as `wrong-false`, not correct. Pinned in Task 3 (classifier tests). +- **Rerunning an evaluation with an existing CSV must resume, not duplicate rows.** Pinned in Task 3 (the runner copies the resumable pattern; checked in its smoke step). + +--- + +## File Structure + +- Modify `modules/frontend/utils/slicer.hpp`: add `runtimeNamesInIR()`. +- Modify `tests/unit/frontend/SlicerTest.cpp`: add tests for it. +- Modify `modules/frontend/caller.hpp` / `caller.cpp`: add `runSlicer` (private) and `sliceInstrumented` (public), and refactor `sliceWithRespectToTarget` onto `runSlicer`. +- Modify `modules/frontend/map2check.cpp`: gating, and the post-`callPass` hook. +- Modify `tests/integration/test_testcomp_regressions.sh`: sections 17–21, plus the section-12 refusal moved to overflow. +- Modify `tests/testcomp/build_corpus.py`: add the `memsafety` and `memcleanup` properties, directory categories, and expected verdict/subproperty. +- Create `tests/lib/memsafety_classifier.sh` with `classify_memsafety_result`. +- Create `tests/integration/test_memsafety_classifier.sh` with the classifier table tests. +- Create `tests/memsafety/run_memsafety_evaluation.sh`, the new runner. +- Modify `tests/castle/run_castle_evaluation.sh` and `tests/juliet/run_juliet_evaluation.sh` to accept `EXTRA_FLAGS`. + +--- + +### Task 1: `runtimeNamesInIR` + +**Files:** Modify `modules/frontend/utils/slicer.hpp`, `tests/unit/frontend/SlicerTest.cpp` + +**Interfaces:** Produces `std::vector Map2Check::runtimeNamesInIR(const std::string& ir);`, which returns every `@map2check_[A-Za-z0-9_]+`, in first-appearance order, without duplicates. + +- [ ] **Step 1: Failing test.** Append to `SlicerTest.cpp`: + +```cpp +// After instrumentation the memory property lives in the runtime calls +// MemoryTrackPass inserted; every one of them is a criterion, so nothing that +// records memory is sliced away. +TEST(RuntimeNamesInIR, FindsEveryMap2checkSymbolOnce) { + const std::string ir = + "declare void @map2check_malloc(ptr, i64)\n" + " call void @map2check_check_deref(ptr %3, i64 4), !dbg !7\n" + " call void @map2check_malloc(ptr %1, i64 8)\n" + " call i32 @__VERIFIER_nondet_int()\n"; + const std::vector names = Map2Check::runtimeNamesInIR(ir); + ASSERT_EQ(names.size(), 2u); + EXPECT_EQ(names[0], "map2check_malloc"); + EXPECT_EQ(names[1], "map2check_check_deref"); +} +``` + +- [ ] **Step 2: Run it and confirm it fails** (`ninja SlicerTest` in `build_aflpp_ut`). Expected: `no member named 'runtimeNamesInIR'`. +- [ ] **Step 3: Implement** it in `slicer.hpp`, next to `nondetNamesInIR`: + +```cpp +/** Every map2check_* runtime symbol in a module's textual IR, in order of + * first appearance. Used as the slicing criteria for the memory properties: + * the property is decided by these calls, so none of them may be removed. */ +inline std::vector runtimeNamesInIR(const std::string& ir) { + static const std::regex symbol(R"(@(map2check_[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); + } + } + return names; +} +``` + +- [ ] **Step 4: Run SlicerTest.** Expected: `[ PASSED ] 12 tests.` +- [ ] **Step 5: Commit** `feat(tacasv2b): runtime names as slicing criteria`. + +--- + +### Task 2: Slice the instrumented module in the memory modes + +**Files:** Modify `caller.hpp`, `caller.cpp`, `map2check.cpp`, `tests/integration/test_testcomp_regressions.sh` + +**Interfaces:** +- Consumes: `runtimeNamesInIR`, `nondetNamesInIR`, `slicingCriteria`, `parseSlicerStatistics` and `describeSlice`. +- Produces: + - `bool Caller::sliceInstrumented();` (public); + - `bool Caller::runSlicer(const std::string& input, const std::string& output, std::vector primary, bool addRuntimeNames, const std::string& entry, const std::string& label);` (private). + - Log prefix `Sliced with respect to map2check runtime`. + +- [ ] **Step 1: Failing integration tests.** + - In section 12, change the refusal run from `--memtrack` to `--check-overflow`, and the grep to `"applies to reachability, assert and memory properties only"`. + - Insert before the summary lines the sections below. Each program is written with a `cat > … <<'EOF'` heredoc, as in the existing sections. + +```bash +# --- 17. memtrack slices the instrumented module and keeps the violation ----- +# Memory has no criterion in the user's program: the property is decided by the +# runtime calls MemoryTrackPass inserts, so the slice is taken AFTER +# instrumentation with every map2check_* call as a criterion. +mkdir -p "$WORK/mem" +cat > "$WORK/mem/dfree.c" <<'EOF' +#include +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + int unrelated = 0; + for (int i = 0; i < 4; i++) { unrelated += i; } + int *p = malloc(sizeof(int)); + free(p); + if (n == 11) { free(p); } + return unrelated; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 dfree.c ) > "$WORK/mem/plain.log" 2>&1 +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --nondet-generator symex --timeout 45 dfree.c ) > "$WORK/mem/slice.log" 2>&1 +plain_v=$(grep -oE "FALSE-[A-Z]+" "$WORK/mem/plain.log" | tail -1) +slice_v=$(grep -oE "FALSE-[A-Z]+" "$WORK/mem/slice.log" | tail -1) +if grep -q "Sliced with respect to map2check runtime" "$WORK/mem/slice.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/mem/slice.log" && [ -n "$slice_v" ] && \ + [ "$slice_v" = "$plain_v" ]; then + ok "memtrack slices after instrumentation and keeps the violation ($slice_v)" +else + fail "memtrack slice" "plain=[$plain_v] slice=[$slice_v]" + grep -E "Sliced|slice|VERIFICATION" "$WORK/mem/slice.log" | sed 's/^/ /' +fi + +# --- 18. memcleanup slices too and still sees the leak ---------------------- +cat > "$WORK/mem/leak.c" <<'EOF' +#include +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + int *p = malloc(sizeof(int)); + if (n == 5) { return 0; } + free(p); + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memcleanup-property --slice --nondet-generator symex --timeout 45 leak.c ) \ + > "$WORK/mem/leak.log" 2>&1 +if grep -q "Sliced with respect to map2check runtime" "$WORK/mem/leak.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/mem/leak.log"; then + ok "memcleanup slices and still finds the leak" +else + fail "memcleanup slice" "no slice, or the leak was lost" + grep -E "Sliced|slice|VERIFICATION" "$WORK/mem/leak.log" | sed 's/^/ /' +fi + +# --- 19. slicing must not invent a memory violation -------------------------- +cat > "$WORK/mem/safe.c" <<'EOF' +#include +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + int *p = malloc(sizeof(int)); + if (p == 0) { return 0; } + *p = n; + if (n == 11) { *p = 0; } + free(p); + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --nondet-generator symex --timeout 45 safe.c ) > "$WORK/mem/safe.log" 2>&1 +if grep -q "VERIFICATION FAILED" "$WORK/mem/safe.log"; then + fail "slice soundness" "a safe program was reported FALSE after slicing" +else + ok "slicing does not invent a memory violation" +fi + +# --- 20. a construct the slicer rejects falls back, loudly ------------------- +# sbt-slicer errors on llvm.stacksave (variable-length arrays). The run must +# fall back to the unsliced module and reach the same verdict. +cat > "$WORK/mem/vla.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + if (n > 0 && n < 10) { + int a[n]; + a[n] = 1; + return a[0]; + } + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 vla.c ) > "$WORK/mem/vla-plain.log" 2>&1 +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --nondet-generator symex --timeout 45 vla.c ) > "$WORK/mem/vla.log" 2>&1 +vla_plain=$(grep -oE "VERIFICATION [A-Z]+" "$WORK/mem/vla-plain.log" | tail -1) +vla_slice=$(grep -oE "VERIFICATION [A-Z]+" "$WORK/mem/vla.log" | tail -1) +if { grep -q "Sliced with respect to map2check runtime" "$WORK/mem/vla.log" || \ + grep -q "analysing the unsliced program" "$WORK/mem/vla.log"; } && \ + [ -n "$vla_slice" ] && [ "$vla_slice" = "$vla_plain" ]; then + ok "a slicer failure falls back and keeps the verdict ($vla_slice)" +else + fail "slice fallback" "plain=[$vla_plain] slice=[$vla_slice]" +fi +``` + + Run the suite. Expected FAILs: `slice mode guard` (old message), and `memtrack slice` and `memcleanup slice` (no slice). Test 19 passes before the fix, trivially (the slice is refused); it is a regression guard, not a RED test. Test 20 passes before the fix too (no slice: same verdict), for the same reason. Ledger both. + +- [ ] **Step 2: Implement.** + - **Extract `runSlicer`** from `sliceWithRespectToTarget`. It covers the lines from the `slicer` existence check to the `describeSlice` log, parameterized by `input`, `output`, `primary`, `addRuntimeNames`, `entry` and `label`. It returns `false` on a missing slicer or on no usable output (keeping the existing warnings), and `true` after logging. When `addRuntimeNames` is set, the runtime names are appended to `primary` before `slicingCriteria(primary, programNondets)`. The IR file becomes `input + ".ll"`, so the two call sites do not collide. + - **`sliceWithRespectToTarget`** becomes: `if (!runSlicer(programHash + "-compiled.bc", programHash + "-sliced.bc", criteria, false, "main", joined(criteria))) return false;` followed by the existing stub-and-rename code. + - **`sliceInstrumented()`:** + +```cpp +bool Caller::sliceInstrumented() { + // Memory properties have no criterion in the user's program: the property + // is decided by the runtime calls MemoryTrackPass inserted, so the slice is + // taken after instrumentation with every map2check_* call as a criterion + // (none can be dropped), and __map2check_main__ -- the renamed user main -- + // as the entry. tacasv2b spec, section 2. + const std::string input = programHash + "-output.bc"; + const std::string output = programHash + "-sliced-instrumented.bc"; + if (!std::filesystem::exists(input)) return false; + if (!runSlicer(input, output, {}, true, "__map2check_main__", + "map2check runtime")) { + return false; + } + std::error_code error; + std::filesystem::rename(output, input, error); + return !error; +} +``` + + - **In `map2check.cpp`:** + - In the pre-`callPass` block, the memory modes fall through without a warning. + - The warning text changes to `"--slice applies to reachability, assert and memory properties only: there is no criterion to slice towards when the goal is coverage or overflow. Analysing the whole program."`. + - After `caller->callPass(args.function);` insert: + +```cpp + // Memory properties slice the INSTRUMENTED module (see sliceInstrumented). + if (args.sliceProgram && + (args.mode == Map2Check::Map2CheckMode::MEMTRACK_MODE || + args.mode == Map2Check::Map2CheckMode::MEMCLEANUP_MODE)) { + caller->sliceInstrumented(); + } +``` + + - Update the `--slice` help text to mention `--memtrack` and `--memcleanup-property`. +- [ ] **Step 3: Rebuild and run the integration suite and ctest.** Expected: `Results: 27 passed, 0 failed`, ctest 100%. +- [ ] **Step 4: Commit** `feat(tacasv2b): --slice for memtrack and memcleanup, after instrumentation`. + +--- + +### Task 3: SV-COMP MemSafety harness + +**Files:** +- Modify `tests/testcomp/build_corpus.py`. +- Create `tests/lib/memsafety_classifier.sh`, `tests/integration/test_memsafety_classifier.sh` and `tests/memsafety/run_memsafety_evaluation.sh`. + +**Interfaces:** +- Produces `classify_memsafety_result `, which prints one of `correct-true correct-false wrong-true wrong-false unknown error`. `` is the output of `classify_map2check_verdict`. +- Produces manifests with the columns `category program data_model expected subproperty`. + +- [ ] **Step 1: Failing classifier test.** Create `tests/integration/test_memsafety_classifier.sh`: + +```bash +#!/bin/bash +# Table test for classify_memsafety_result: a FALSE only counts when its kind +# matches the task's subproperty; a TRUE on a false task is the dangerous error. +set -u +. "$(dirname "$0")/../lib/memsafety_classifier.sh" +PASSED=0; FAILED=0 +check() { # expected subproperty verdict want + got=$(classify_memsafety_result "$1" "$2" "$3") + if [ "$got" = "$4" ]; then PASSED=$((PASSED+1)); else FAILED=$((FAILED+1)); echo " FAIL $1/$2/$3: want $4 got $got"; fi +} +check true "" TRUE correct-true +check true "" FALSE-DEREF wrong-false +check false valid-deref FALSE-DEREF correct-false +check false valid-free FALSE-FREE correct-false +check false valid-memtrack FALSE-MEMTRACK correct-false +check false valid-memcleanup FALSE-MEMCLEANUP correct-false +check false valid-deref FALSE-FREE wrong-false +check false valid-deref TRUE wrong-true +check false valid-deref UNKNOWN unknown +check false valid-deref TIMEOUT unknown +check true "" ERROR error +echo " Results: $PASSED passed, $FAILED failed" +[ "$FAILED" -eq 0 ] +``` + + Run `bash tests/integration/test_memsafety_classifier.sh`. Expected: fails, because `memsafety_classifier.sh` does not exist. +- [ ] **Step 2: Implement** `tests/lib/memsafety_classifier.sh`: + +```bash +# shellcheck shell=bash +# classify_memsafety_result +# is classify_map2check_verdict's output. A FALSE counts as correct +# only when its kind matches the subproperty the task declares; FALSE of the +# wrong kind is a wrong answer, not a lucky one. +classify_memsafety_result() { + local expected="$1" sub="$2" verdict="$3" want="" + case "$sub" in + valid-deref) want="FALSE-DEREF" ;; + valid-free) want="FALSE-FREE" ;; + valid-memtrack) want="FALSE-MEMTRACK" ;; + valid-memcleanup) want="FALSE-MEMCLEANUP" ;; + esac + case "$verdict" in + TRUE) [ "$expected" = "true" ] && echo correct-true || echo wrong-true ;; + FALSE*) if [ "$expected" = "false" ] && [ "$verdict" = "$want" ]; then + echo correct-false; else echo wrong-false; fi ;; + ERROR) echo error ;; + *) echo unknown ;; + esac +} +``` + + Run the test. Expected: `Results: 11 passed, 0 failed`. +- [ ] **Step 3: `build_corpus.py`.** + - Add `"memsafety": "valid-memsafety.prp"` and `"memcleanup": "valid-memcleanup.prp"` to `PROPERTY_FILE`. + - Add `MEMORY_CATEGORIES`, a dict from category to directory list. For `memsafety`: Arrays, Heap, LinkedLists, Other and Juliet, exactly as spec §3.4. For `memcleanup`: one category, `MemCleanup`, covering every directory. The `memcleanup` expansion globs `*/*.yml` and filters by property. + - In `main`, when the property is `memsafety` or `memcleanup`, expand categories with `glob(BENCH//*.yml)` instead of `expand_set`. + - Generalize `task_info` so that, for the wanted property, it captures `expected_verdict` and `subproperty` (the lines after the matching `- property_file:`), and returns them as a 4th value. + - For memory properties, write the header `# category\tprogram\tdata_model\texpected\tsubproperty` and 5 columns. The cover-* outputs stay unchanged. + - Smoke: `python3 tests/testcomp/build_corpus.py --property memsafety --per-category 3 --out /tmp/ms.tsv`. Expected: a summary listing Arrays/Heap/LinkedLists/Other/Juliet with non-zero "applicable", and 15 rows. +- [ ] **Step 4: `tests/memsafety/run_memsafety_evaluation.sh`.** + - Copy the structure of `tests/testcomp/run_testcomp_evaluation.sh`: the env vars `MANIFEST PROPERTY RESULTS_DIR SHARD SHARDS BUDGET DEADLINE_S EXTRA_FLAGS MAP2CHECK_PATH`, the resumable CSV, fd 3, and a private work dir per task. + - Differences: + - The mode flag is `--memtrack` for `memsafety` and `--memcleanup-property` for `memcleanup`. There is no TestCov. + - The raw verdict comes from `classify_map2check_verdict "$output" "$rc" "$elapsed" "$BUDGET"` (source `tests/lib/verdict_classifier.sh`). + - The class comes from `classify_memsafety_result "$expected" "$subproperty" "$verdict"` (source `tests/lib/memsafety_classifier.sh`). + - The slice statistics come from the log (`grep -o "Sliced with respect to.*"`). + - The CSV header is `category,program,data_model,expected,subproperty,verdict,class,elapsed_s,slice`. + - Smoke: run it on `/tmp/ms.tsv` with `BUDGET=30`, twice. Expected: 15 rows after the first run, still 15 after the second (resume). +- [ ] **Step 5: Commit** `test(tacasv2b): SV-COMP MemSafety evaluation harness`. + +--- + +### Task 4: `EXTRA_FLAGS` in the CASTLE and Juliet runners + +**Files:** Modify `tests/castle/run_castle_evaluation.sh`, `tests/juliet/run_juliet_evaluation.sh` + +- [ ] **Step 1:** In each runner, next to the other env defaults, add `EXTRA_FLAGS="${EXTRA_FLAGS:-}"`, with a comment that it holds opt-in flags such as `--slice` appended to every run. Append `$EXTRA_FLAGS` to the map2check invocation, right after the mode flags. In CASTLE that is both invocations (lines ~174 and ~199); in Juliet, the equivalent call. +- [ ] **Step 2:** `bash -n` both files. Then run a 2-task CASTLE smoke with `EXTRA_FLAGS=--slice` and `RESULTS_DIR` in the scratchpad (use whatever the runner offers to limit tasks; if nothing, a temporary copy of the dataset list with 2 entries). Expected: the raw logs show `Sliced with respect to`. +- [ ] **Step 3: Commit** `test(tacasv2b): opt-in flags for the CASTLE and Juliet runners`. + +--- + +### Task 5: Mini-rounds R7–R9 and the log + +- [ ] **R7, CASTLE:** the full 250, `EXTRA_FLAGS=""` and `EXTRA_FLAGS=--slice`, same build, separate `RESULTS_DIR` in the scratchpad. Tally TP/TN/FP/FN/UNKNOWN/TIMEOUT per arm, and compare with v15 (`tests/castle/results_v15`: TP 54, FN 14, FP 1). +- [ ] **R8, SV-COMP MemSafety:** 10 per category (`--per-category 10`), both arms, `BUDGET=120`. Tally the classes per arm and per category; report the median time and the slice reduction. +- [ ] **R9, Juliet scope C:** a small per-CWE sample (use the runner's sampling options; if none, 5 per CWE), both arms. +- [ ] **Append R7, R8 and R9** to `docs/reports/tacas-experiment-log.md`. For each: data, comparison with the previous round and with the other arm, and the reading, with **wrong-true and wrong-false called out explicitly**. Commit `docs(tacas): R7-R9 -- memory slicing mini-rounds`. 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..9714d883f --- /dev/null +++ b/docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md @@ -0,0 +1,261 @@ +# 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) + 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) | 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). + +--- + +## 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()`/`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. + +### 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 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. | + +--- + +## 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. 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..73e66b7f0 --- /dev/null +++ b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md @@ -0,0 +1,173 @@ +# 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. + +**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:` + 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 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. + +--- + +## 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 | diff --git a/docs/superpowers/specs/2026-09-27-tacasv2b-slicing-memsafety-design.md b/docs/superpowers/specs/2026-09-27-tacasv2b-slicing-memsafety-design.md new file mode 100644 index 000000000..54640567a --- /dev/null +++ b/docs/superpowers/specs/2026-09-27-tacasv2b-slicing-memsafety-design.md @@ -0,0 +1,150 @@ +# tacasv2b — Slicing para memtrack e memcleanup + +**Data:** 2026-09-27 +**Branch:** `feat/tacas-slicing-mem` (a partir de `feat/tacas-slicing`, PR #68) +**Baseline:** tacasv1 (AFL++ 4.40c + CmpLog), mesmo build com e sem `--slice` +**Status:** rascunho — aguardando revisão +**Registro de rodadas:** `docs/reports/tacas-experiment-log.md` (R6 = sondagem deste design) + +--- + +## 1. Objetivo + +Estender o `--slice` para `--memtrack` e `--memcleanup-property` e medir o efeito em três +corpora: **MemSafety do SV-COMP** (programas grandes, onde o slicing tem o que cortar), +**CASTLE** e **Juliet** (os corpora já medidos na v15, programas pequenos). O critério de +sucesso é o slicing **não introduzir veredito errado** (FALSE espúrio ou TRUE errado) e, +onde houver o que cortar, reduzir o tempo ou aumentar os acertos. + +--- + +## 2. Abordagem escolhida: fatiar depois da instrumentação + +Na tacasv2a, o slicing roda antes da instrumentação porque o critério (`reach_error`, +`__VERIFIER_assert`) existe no programa do usuário. Para memória não há chamada no +programa que sirva de critério: o critério são os próprios acessos à memória, que só +ganham forma de chamada depois do `MemoryTrackPass`. + +Então, em `MEMTRACK_MODE` e `MEMCLEANUP_MODE`: +1. `callPass` instrumenta normalmente, gerando `-output.bc`. +2. **Novo:** o slicer roda sobre `-output.bc` com + - critério = **toda função `map2check_*`** chamada no módulo (as que o runtime do + memtrack recebe: `map2check_malloc`, `map2check_free`, `map2check_check_deref`, + `map2check_alloca`, `map2check_load`, `map2check_add_store_pointer`, …) **mais** as + `__VERIFIER_nondet_*` (lista fixa + IR, como na 2a); + - `--entry=__map2check_main__` (a instrumentação renomeia o `main` do usuário; o `main` + real vem do gerador nondet no link); + - `-cutoff-diverging=false --statistics` (os mesmos motivos da 2a). +3. `linkLLVM` segue igual, sobre o `-output.bc` fatiado. + +**Por que é seguro:** o problema registrado no código (fatiar depois da instrumentação +remove a instrumentação) acontecia com o critério `reach_error`: as chamadas que +**registram** a violação não influenciam o alcance do alvo e eram cortadas. Aqui toda +chamada do runtime é critério, então nenhuma é removida; o que sai é computação que não +alimenta nenhum acesso à memória, alocação ou leitura de entrada. + +**Sondagem (R6):** busybox `basename-2.i` 2985 → 2373 instruções (−20%); +memsafety-cve `admesh.i` −1,5%; o slicer falha em `llvm.stacksave` (VLA) e aí o Caller +já volta ao programa inteiro. + +**Rejeitadas:** marcadores no estilo Symbiotic antes da instrumentação (mais código, ganho +não medido) e A/B das duas (dobra o custo). Ficam como alternativa se a medição mostrar +fatias grandes demais. + +--- + +## 3. Mudanças + +### 3.1 `slicer.hpp` +- `runtimeNamesInIR(ir)`: todo símbolo `@map2check_[A-Za-z0-9_]+` no IR textual, na ordem + da primeira ocorrência, sem repetição (mesma forma de `nondetNamesInIR`). + +### 3.2 `Caller` +- `sliceInstrumented()`: fatia `-output.bc` no lugar. Desmonta com `opt -S`, + junta `runtimeNamesInIR` + `nondetNamesInIR` como critério, roda o slicer com + `--entry=__map2check_main__`, e em sucesso renomeia a fatia por cima do `-output.bc`. + Mesmo orçamento, mesmo fallback (programa inteiro com aviso) e mesma linha de log + (`describeSlice`, rótulo `map2check runtime`) da 2a. +- Sem stub `weak`: nenhuma função do programa é critério. +- Refatoração: o trecho comum com `sliceWithRespectToTarget` (desmontar, ler estatísticas, + orçamento, fallback) vira um helper privado, para as duas usarem o mesmo caminho. + +### 3.3 `map2check.cpp` +- `--slice` em `MEMTRACK_MODE`/`MEMCLEANUP_MODE` chama `sliceInstrumented()` **depois** de + `callPass` e **antes** de `linkLLVM`. Overflow continua recusado (2c); a mensagem passa a + "reachability, assert and memory properties". + +### 3.4 Harness de MemSafety do SV-COMP (novo) +- `build_corpus.py` ganha as propriedades `memsafety` (`valid-memsafety.prp`) e + `memcleanup` (`valid-memcleanup.prp`). Para essas, o manifesto carrega o **veredito + esperado e a subpropriedade** (`valid-deref`/`valid-free`/`valid-memtrack`), lidos do + `.yml`. +- Categorias por diretório, espelhando os `.set` do SV-COMP (os `.set` não vêm no + benchmark local): + +| categoria | diretórios | +|---|---| +| Arrays | `array-memsafety`, `array-memsafety-realloc` | +| Heap | `memsafety`, `memsafety-ext*`, `memsafety-broom`, `ldv-memsafety*`, `forester-heap`, `heap-manipulation` | +| LinkedLists | `list-simple`, `list-ext-properties`, `list-properties`, `ddv-machzwd` | +| Other | `busybox-1.22.0`, `coreutils-v8.31`, `coreutils-v9.5-units`, `memsafety-cve`, `uthash-2.0.2`, `goblint-regression`, `goblint-coreutils` | +| Juliet | `Juliet_Test` | +| MemCleanup | tarefas com `valid-memcleanup.prp` | + + Excluídos: `pthread*`, `weaver`, `termination-*` (o Map2Check não suporta threads nem + terminação; mediria zeros sem significado). +- `run_memsafety_evaluation.sh` (novo, no molde do `run_testcomp_evaluation.sh`: retomável, + por shard, `EXTRA_FLAGS`, `BUDGET`): roda `--memtrack` (ou `--memcleanup-property`) e + classifica cada tarefa em `correct-true`, `correct-false` (FALSE **com a subpropriedade + certa**), `wrong-true`, `wrong-false`, `unknown`, `error`. FALSE com subpropriedade + diferente conta como `wrong-false`. + +### 3.5 CASTLE e Juliet +- `run_castle_evaluation.sh` e `tests/juliet/run_juliet_evaluation.sh` passam a aceitar + `EXTRA_FLAGS` (acrescentado a `mode_flags`) e `RESULTS_DIR` já existente, para o braço + com `--slice`. + +--- + +## 4. Testes + +Integração (`test_testcomp_regressions.sh`): +1. **Memtrack com slice mantém a detecção:** programa com uso depois de `free` e código + irrelevante; `--memtrack --slice --nondet-generator symex` → `Sliced with respect to + map2check runtime` e FALSE-FREE/FALSE-DEREF como sem slice. +2. **Memcleanup com slice mantém o leak:** leak alcançado por leitura nondet → + FALSE-MEMCLEANUP com slice. +3. **Programa seguro não vira FALSE com slice** (mesma forma do 1, sem o bug). +4. **VLA:** programa com array de tamanho variável → aviso de fallback, veredito igual ao + sem slice. +5. A recusa em overflow continua (mensagem nova). + +Unitário: `runtimeNamesInIR` acha todo símbolo `@map2check_*` e deduplica. Não precisa +distinguir função de variável global: um nome sem call site é critério inofensivo (a 2a +verificou isso no código do dg). + +Harness: teste do classificador de veredito (tabela esperado × obtido × subpropriedade → +classe), no estilo de `tests/lib/verdict_classifier.sh`. + +--- + +## 5. Avaliação (mini-rodadas, cada uma registrada no log) + +- **R7:** CASTLE completo (250), tacasv1 com e sem `--slice`, 300 s. +- **R8:** amostra de MemSafety do SV-COMP (por categoria, cota pequena — p.ex. 10 por + categoria), com e sem `--slice`. +- **R9:** Juliet escopo C, amostra por CWE, com e sem `--slice`. +- Em cada uma: acertos, **erros (wrong-true/wrong-false)**, unknown, tempo mediano e + redução de instruções. Comparação explícita com a rodada anterior. +- A avaliação completa fica para a execução sequencial depois do merge. + +--- + +## 6. Riscos + +| Risco | Mitigação | +|---|---| +| Fatia remove algo que o runtime precisava → FALSE espúrio ou violação perdida | Todo `map2check_*` é critério; testes 1–3; wrong-* medido em R7–R9 | +| Slicer não suporta construções (VLA/`stacksave`, threads, `longjmp`) | Fallback já existente para o programa inteiro, com aviso; teste 4 | +| Redução pequena (R6: 1,5%–20%) → efeito nulo | Aceitável: o critério é não piorar; o ganho é medido, não presumido | +| Categorias por diretório divergem dos `.set` oficiais | Mapeamento documentado na §3.4; é amostra de diagnóstico | diff --git a/docs/superpowers/specs/2026-09-27-tacasv2c-slicing-overflow-design.md b/docs/superpowers/specs/2026-09-27-tacasv2c-slicing-overflow-design.md new file mode 100644 index 000000000..d731b99e3 --- /dev/null +++ b/docs/superpowers/specs/2026-09-27-tacasv2c-slicing-overflow-design.md @@ -0,0 +1,65 @@ +# tacasv2c — Slicing para overflow + +**Data:** 2026-09-27 +**Branch prevista:** `feat/tacas-slicing-overflow` (a partir de `feat/tacas-slicing-mem`) +**Baseline:** tacasv1, mesmo build com e sem `--slice` +**Status:** rascunho de estudo — aguardando revisão +**Registro:** `docs/reports/tacas-experiment-log.md` (R7 = sondagem deste design) + +--- + +## 1. Objetivo + +Estender o `--slice` para `--check-overflow`, fechando o slicing por propriedade da +tacasv2 (2a: reach/assert; 2b: memória; 2c: overflow). + +## 2. Estudo + +- **Como o overflow é instrumentado.** O `OverflowPass` troca cada operação aritmética + com sinal (add, sub, mul, sdiv, srem, shl…) por uma chamada de runtime + `map2check_binop_*` (`modules/backend/pass/OperationsFunctions.hpp`). Essas chamadas + recebem os operandos e registram a violação. +- **Consequência:** o critério de overflow é o mesmo do 2b, ou seja, toda chamada + `map2check_*` do módulo instrumentado mais as nondets. `Caller::sliceInstrumented()` + já faz exatamente isso. Nenhuma lógica de slicing nova é necessária. +- **O que o Symbiotic faz** (levantado na 2a): instrumenta as checagens de overflow e + fatia em relação à chamada de erro (`__VERIFIER_error`). O nosso critério é mais + conservador: fatiar em relação às próprias checagens mantém todas elas, e não só as + que já levam a erro. +- **Sondagem (R7):** busybox `chgrp-incomplete-2.i` 927 → 487 instruções (−47%); + bitvector −2%; nla-digbench −14%. Nos programas grandes, a redução é maior que a de + memória (R6: −20%). + +## 3. Mudanças + +1. **Gating** (`map2check.cpp`): `OVERFLOW_MODE` entra no gancho pós-`callPass` junto com + memtrack/memcleanup. A mensagem de recusa passa a citar só coverage. +2. **Harness:** `build_corpus.py` ganha `--property overflow` (`no-overflow.prp`), com + categorias por diretório espelhando o NoOverflows do SV-COMP: + - Main: `bitvector`, `nla-digbench-scaling`, `recursive-simple`, `loop-zilu`, + `signedintegeroverflow-regression`, `goblint-regression`; + - BusyBox: `busybox-1.22.0`; + - Juliet: `Juliet_Test`. + + Ficam excluídos `pthread*`, `weaver` e `termination-*`. + `run_memsafety_evaluation.sh` aceita `PROPERTY=overflow` (modo `--check-overflow`), + e o classificador mapeia a subpropriedade `no-overflow` para `FALSE-OVERFLOW`. +3. **Testes:** + - overflow com slice mantém o FALSE-OVERFLOW; + - programa sem overflow não vira FALSE; + - a recusa em cover-branches continua; + - linhas novas na tabela do classificador (`no-overflow`). + +## 4. Avaliação (mini-rodadas, registradas no log) + +- CASTLE CWE-190 (os 12 casos de overflow) e Juliet CWE-190, com e sem `--slice`. Os + runners já aceitam `EXTRA_FLAGS`. +- NoOverflows do SV-COMP: 10 por categoria, com e sem `--slice`. +- Métricas: acertos, **wrong-true e wrong-false** e redução de instruções. + +## 5. Riscos + +| Risco | Mitigação | +|---|---| +| Operação sem instrumentação (sem sinal, por exemplo) sai da fatia e deixa de alimentar uma checagem | O critério é a checagem; o dg mantém as dependências de dados de cada operando | +| Redução nula em programas pequenos (CASTLE/Juliet) | Critério de sucesso = não piorar; o ganho aparece no SV-COMP (R7) | 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/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..01cefa075 --- /dev/null +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -0,0 +1,184 @@ +/** + * 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; + +/* 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() { + if (map2check_afl_index < map2check_afl_size) { + return map2check_afl_data[map2check_afl_index++]; + } + + map2check_afl_index = 0; + return map2check_afl_data[map2check_afl_index]; +} + +/* 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; +} + +/* 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) 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 + * 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_afl_index = 0; + __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; -} diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index d416a20e1..2c557fb1f 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 @@ -144,7 +146,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++; @@ -176,7 +178,9 @@ std::string Caller::exportFuzzerVectorAsKtest() { return path; } -bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { +bool Caller::runSlicer(const std::string &input, const std::string &output, + std::vector primary, bool addRuntimeNames, + const std::string &entry, const std::string &label) { const std::string slicer = Map2Check::slicerBinary(); if (!std::filesystem::exists(slicer)) { // Announced, not silently skipped. A slicer that is asked for and absent @@ -187,40 +191,63 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { " -- analysing the unsliced program"); return false; } - - // The COMPILED bitcode, not the instrumented one: this runs before callPass - // so that the instrumentation is applied to the slice rather than removed by - // it. Entry is still plain main at this point, for the same reason. - const std::string input = programHash + "-compiled.bc"; - const std::string output = programHash + "-sliced.bc"; if (!std::filesystem::exists(input)) return false; - std::ostringstream command; - // -c is the slicing criterion: keep what the target call depends on. The - // criterion is the whole reason this only serves Cover-Error -- there is no - // criterion to give it when every branch is the goal. - // - // --entry is required. Run after callPass this had to be - // __map2check_main__, because the instrumentation renames the entry and the - // slicer would report "The entry function not found: main" and slice - // nothing. Run before it, as it now is, the program still has its own main. // Bounded, for the reason every other external step here is bounded: the // slicer builds a system dependence graph over the whole module, and on the - // large programs that is not fast. Measured on the v12 corpus: the sliced - // arm recorded 26 ERROR verdicts against the control's 9, every one of them - // at 87 to 89 seconds, and three were tasks the control had ANSWERED -- - // slicing did not fail on them, it just took the run past its deadline. - // - // A slice that does not finish is not a loss: the code below already falls - // back to analysing the whole program, which is exactly what the control - // does. Overrunning the budget loses the verdict instead. + // large programs that is not fast. A slice that does not finish is not a + // loss -- the caller falls back to the whole program; overrunning the budget + // loses the verdict instead. const double sliceBudget = std::max( 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 << " " + + // The program's own names join the criteria: the nondet functions (no fixed + // list knows every name a benchmark declares, and a missing one silently + // shifts the suite), and for the memory properties every map2check_* call + // the instrumentation inserted. Read from the textual IR -- the bitcode + // string table packs names with no separator. If the disassembly fails, the + // fixed nondet list stands. + const std::string inputIR = input + ".ll"; + std::ostringstream disassemble; + disassemble << Map2Check::optBinary << " -S " << input << " -o " << inputIR + << " > /dev/null 2>&1"; + std::vector programNondets; + std::string irText; + if (system(disassemble.str().c_str()) == 0) { + std::ifstream irFile(inputIR); + std::stringstream irStream; + irStream << irFile.rdbuf(); + irText = irStream.str(); + programNondets = Map2Check::nondetNamesInIR(irText); + } + if (addRuntimeNames) { + // The runtime checks decide the property and external calls can commit + // the error themselves: both are criteria. Without the IR there are no + // checks to keep, and a slice would remove them all -- refuse instead of + // falling back to the nondet list, which is only sound for reach/assert. + std::vector runtimeCriteria; + if (!Map2Check::instrumentedSliceCriteria(irText, &runtimeCriteria)) { + Map2Check::Log::Warning( + "could not read the instrumented module's runtime calls -- " + "analysing the unsliced program"); + return false; + } + for (const std::string &name : runtimeCriteria) primary.push_back(name); + } + + // -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). + // --statistics: counts before and after, logged below. + std::ostringstream command; + command << "timeout -k " << Map2Check::killGracePeriod << " " + << static_cast(sliceBudget) << " " << slicer << " -c " + << Map2Check::slicingCriteria(primary, programNondets) + << " --entry=" << entry + << " -cutoff-diverging=false --statistics -o " << output << " " << input << " > slicer.output 2>&1"; Map2Check::Log::Debug(command.str()); const int result = system(command.str().c_str()); @@ -236,27 +263,40 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { } // Reported, because a slice is not a neutral speed-up: it narrows the - // question being answered, and the size difference is the only visible sign - // of how much was dropped. + // question being answered, and this line is the only visible sign 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(); + Map2Check::Log::Info(Map2Check::describeSlice( + label, Map2Check::parseSlicerStatistics(slicerText.str()), before, + after)); + return true; +} + +bool Caller::sliceWithRespectToTarget(const std::string &targetFunction, + const std::vector &criteria) { + // The COMPILED bitcode, not the instrumented one: this runs before callPass + // so that the instrumentation is applied to the slice rather than removed by + // it. Entry is still plain main at this point, for the same reason. + const std::string input = programHash + "-compiled.bc"; + const std::string output = programHash + "-sliced.bc"; + std::string label; + for (const std::string &name : criteria) { + label += (label.empty() ? "" : ",") + name; + } + if (!runSlicer(input, output, criteria, false, "main", label)) return false; + std::error_code error; // 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 // 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. - // - // Measured on rangesum05.i: --nondet-generator fuzzer answers FAILED, and - // the same invocation with --slice answers UNKNOWN with zero crash inputs - // and no fuzzed binary on disk. This is what cost the sliced arm the bulk - // of its 133 lost detections in the v11 factorial. + // is produced, and the fuzzer stage then does nothing at all. // // A WEAK definition restores the link without displacing a real one: where // the slice did keep the body, the strong definition still wins. @@ -266,7 +306,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; @@ -286,13 +326,31 @@ 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); return !error; } +bool Caller::sliceInstrumented() { + // Memory properties have no criterion in the user's program: the property + // is decided by the runtime calls MemoryTrackPass inserted, so the slice is + // taken after instrumentation with every map2check_* call as a criterion + // (none can be dropped), and __map2check_main__ -- the renamed user main -- + // as the entry. tacasv2b spec, section 2. + const std::string input = programHash + "-output.bc"; + const std::string output = programHash + "-sliced-instrumented.bc"; + if (!std::filesystem::exists(input)) return false; + if (!runSlicer(input, output, {}, true, "__map2check_main__", + "map2check runtime")) { + return false; + } + std::error_code error; + std::filesystem::rename(output, input, error); + return !error; +} + void Caller::cleanGarbage() { std::filesystem::current_path(currentPath); std::ostringstream removeCommand; @@ -313,8 +371,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 +398,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,21 +407,41 @@ 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"; 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; 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"); + } else if (!std::filesystem::exists(programHash + "-cmplog.out", + fuzzErr)) { + Map2Check::Log::Warning( + "the AFL++ CmpLog binary did not build -- fuzzing without " + "comparison solving"); } break; } @@ -543,8 +620,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; } } @@ -776,60 +853,155 @@ void Caller::executeAnalysis(std::string solvername) { Map2Check::Log::Warning("Exited klee with " + std::to_string(result)); if (result == 31744) // Timeout gotTimeout = true; + // KLEE stopping on its own --max-time exits 0, like a run that explored + // every path, but it proves nothing. Treated as the timeout it is: a + // violation already recorded is kept, anything else is UNKNOWN -- never + // the TRUE a short path's NONE in the property file would otherwise make + // it (a reachable null dereference came back TRUE). + if (Map2Check::kleeHaltedOnTimer(Map2Check::kleeOutputDir)) { + Map2Check::Log::Warning( + "KLEE halted on its timer with states left -- not a complete " + "exploration"); + gotTimeout = true; + } 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())); - 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; + // 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). + // + // 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; + 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"; + if (!seed.good()) + Map2Check::Log::Warning("could not write the AFL++ placeholder seed"); } - command << "./" + programHash + - "-fuzzed.out -jobs=8 -use_value_profile=1" - << corpus << " > fuzzer.output"; + 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 + // 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 "; + // 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 << " " + << std::max(1u, 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"; + if (hasCmplog) command << " -c ./" << programHash << "-cmplog.out"; + command << " -- ./" << 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()); + // 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. + // 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.is_regular_file(crashErr)) continue; + if (entry.path().filename() == "README.txt") continue; + std::ostringstream commandWitness; + commandWitness << "timeout -k " << Map2Check::killGracePeriod << " " + << replayBudget << " ./" << 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 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 (!entry.is_regular_file(queueErr)) 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"); if (isWitnessFileCreated()) { diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 359252ed6..eba63101d 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 @@ -131,10 +130,24 @@ 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); + + /** Slices the INSTRUMENTED module (-output.bc) in place, for the + * memory properties: every map2check_* runtime call and every nondet read + * is a criterion, and the entry is __map2check_main__. Runs after callPass + * and before linkLLVM. Returns false, leaving the module untouched, if the + * slicer is unavailable or produced nothing usable. */ + bool sliceInstrumented(); /** Turns on the exchange of input vectors between the two engines. * @@ -146,10 +159,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. - * LibFuzzer treats it as its corpus and grows it; 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. */ @@ -190,6 +208,14 @@ class Caller { * artefact lives. Named after the SHA-1 of the input bitcode, so two runs on * the same input share it. */ std::string getScratchDir() { return currentPath + "/" + programHash; } + private: + /** Shared by both slicing entry points: disassembles `input`, adds the + * program's nondet names (and, with addRuntimeNames, its map2check_* calls) + * to `primary`, runs sbt-slicer bounded, and logs the slice under `label`. + * Returns false, with a warning, when there is no usable output. */ + bool runSlicer(const std::string& input, const std::string& output, + std::vector primary, bool addRuntimeNames, + const std::string& entry, const std::string& label); }; } // namespace Map2Check diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index 6fdffc276..34ae97de0 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -514,20 +514,37 @@ 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); + 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."); + if (args.mode != Map2Check::Map2CheckMode::MEMTRACK_MODE && + args.mode != Map2Check::Map2CheckMode::MEMCLEANUP_MODE) { + Map2Check::Log::Warning( + "--slice applies to reachability, assert and memory properties " + "only: there is no criterion to slice towards when the goal is " + "coverage or overflow. Analysing the whole program."); + } } } caller->callPass(args.function); + + // Memory properties slice the INSTRUMENTED module (see sliceInstrumented): + // their criterion is the runtime calls the instrumentation inserted. + if (args.sliceProgram && + (args.mode == Map2Check::Map2CheckMode::MEMTRACK_MODE || + args.mode == Map2Check::Map2CheckMode::MEMCLEANUP_MODE)) { + caller->sliceInstrumented(); + } caller->linkLLVM(); // (3) Apply nondeterministic mode and execute analysis @@ -560,15 +577,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 +597,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 { @@ -608,6 +625,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 +637,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 " @@ -646,7 +668,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 +745,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), @@ -746,8 +768,10 @@ 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), " + "the assertions (--check-asserts) or the memory runtime checks " + "(--memtrack, --memcleanup-property) 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)") @@ -898,7 +922,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 +934,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 +971,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 +997,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; diff --git a/modules/frontend/test_suite/ktest_reader.cpp b/modules/frontend/test_suite/ktest_reader.cpp index 1d9ce4550..9bbf55703 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; @@ -287,6 +287,37 @@ 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; +} + +bool kleeHaltedOnTimer(const std::string& kleeOutDir) { + std::ifstream messages( + (std::filesystem::path(kleeOutDir) / "messages.txt").string()); + std::string line; + while (std::getline(messages, line)) { + if (line.find("HaltTimer invoked") != std::string::npos) 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 214f204e8..f9d18febb 100644 --- a/modules/frontend/test_suite/ktest_reader.hpp +++ b/modules/frontend/test_suite/ktest_reader.hpp @@ -73,6 +73,20 @@ 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); + +/** Whether KLEE stopped on its own --max-time rather than running out of + * paths ("HaltTimer invoked" in messages.txt). Such a run exits 0, exactly + * like a finished one, but it proves nothing: a short path having written + * NONE to the property file made a reachable null dereference read as TRUE. */ +bool kleeHaltedOnTimer(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 @@ -85,7 +99,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/slicer.hpp b/modules/frontend/utils/slicer.hpp new file mode 100644 index 000000000..2fe1880a8 --- /dev/null +++ b/modules/frontend/utils/slicer.hpp @@ -0,0 +1,229 @@ +/** + * 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 +#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; +} + +/** 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); + } + } + return names; +} + +/** Every map2check_* runtime symbol in a module's textual IR, in order of + * first appearance. Used as the slicing criteria for the memory properties: + * the property is decided by these calls, so none of them may be removed. */ +inline std::vector runtimeNamesInIR(const std::string& ir) { + static const std::regex symbol(R"(@(map2check_[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); + } + } + return names; +} + +/** Every function a module DECLARES without defining (`declare ... @f(`), in + * order of first appearance, LLVM intrinsics excluded. In the modes that slice + * the instrumented module these are criteria too: a memory error can happen + * inside an external function (strcpy overflowing a stack buffer), and nothing + * the runtime checks depends on such a call, so without it as a criterion the + * slicer drops the call and the bug with it (CASTLE-787-2: a wrong TRUE). */ +inline std::vector externalNamesInIR(const std::string& ir) { + static const std::regex declaration( + R"((?:^|\n)declare [^\n]*?@([A-Za-z0-9_.$]+)\()"); + std::vector names; + for (std::sregex_iterator it(ir.begin(), ir.end(), declaration), end; + it != end; ++it) { + const std::string name = (*it)[1]; + // Intrinsics are not calls into code the slicer could keep -- except the + // memory ones: clang lowers memcpy/memset/memmove (and struct copies) to + // them, and an overflowing copy into a buffer nothing reads again feeds no + // criterion, so it has to be one (the strcpy case again). + if (name.rfind("llvm.", 0) == 0 && name.rfind("llvm.memcpy.", 0) != 0 && + name.rfind("llvm.memmove.", 0) != 0 && + name.rfind("llvm.memset.", 0) != 0) { + continue; + } + if (std::find(names.begin(), names.end(), name) == names.end()) { + names.push_back(name); + } + } + return names; +} + +/** The primary criteria for slicing the INSTRUMENTED module: every runtime + * check, then every external function (see externalNamesInIR). Returns false + * when the IR holds no runtime call at all -- a failed disassembly, an empty + * file -- because a slice without the checks as criteria removes them all and + * the property silently reads as holding. */ +inline bool instrumentedSliceCriteria(const std::string& ir, + std::vector* criteria) { + criteria->clear(); + for (const std::string& name : runtimeNamesInIR(ir)) { + criteria->push_back(name); + } + if (criteria->empty()) return false; + for (const std::string& name : externalNamesInIR(ir)) { + if (std::find(criteria->begin(), criteria->end(), name) == + criteria->end()) { + criteria->push_back(name); + } + } + return true; +} + +/** 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(); +} + +/** 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/modules/frontend/utils/tools.hpp b/modules/frontend/utils/tools.hpp index 16975283a..19a1e4a4b 100644 --- a/modules/frontend/utils/tools.hpp +++ b/modules/frontend/utils/tools.hpp @@ -59,6 +59,29 @@ 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. + * + * 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("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 with MAP2CHECK_AFL_FUZZ. */ +inline std::string aflFuzzBinary() { + const char* override_path = getenv("MAP2CHECK_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. @@ -73,9 +96,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++ 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/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 diff --git a/tests/castle/run_castle_evaluation.sh b/tests/castle/run_castle_evaluation.sh index 308b29e76..82116596f 100755 --- a/tests/castle/run_castle_evaluation.sh +++ b/tests/castle/run_castle_evaluation.sh @@ -10,6 +10,10 @@ SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" CASTLE_DIR="$SCRIPT_DIR/CASTLE-Benchmark/datasets/CASTLE-C250" JSON_FILE="$SCRIPT_DIR/CASTLE-Benchmark/datasets/CASTLE-C250.min.json" RESULTS_DIR="${RESULTS_DIR:-$SCRIPT_DIR/results}" +# Opt-in flags appended to every map2check run (e.g. "--slice"), for measuring +# a capability against the same corpus without it. Not part of the CWE's mode: +# the CSV's mode column stays the property that was checked. +EXTRA_FLAGS="${EXTRA_FLAGS:-}" TIMEOUT_SEC=360 # CWE → mode mapping (single-pass flags, --add-invariants added on UNKNOWN) @@ -171,7 +175,7 @@ for t in data['tests']: start=$(date +%s%N) rc=0 run_isolated "$raw" "$TIMEOUT_SEC" \ - "$MAP2CHECK" $mode_flags --timeout "$INNER_TIMEOUT" "$bc_file" || rc=$? + "$MAP2CHECK" $mode_flags $EXTRA_FLAGS --timeout "$INNER_TIMEOUT" "$bc_file" || rc=$? end=$(date +%s%N) elapsed=$(python3 -c "print(round(($end - $start) / 1000000000, 1))") output=$(cat "$raw") @@ -196,7 +200,7 @@ for t in data['tests']: start=$(date +%s%N) rc=0 run_isolated "$raw" "$TIMEOUT_SEC" \ - "$MAP2CHECK" $mode_flags --add-invariants --timeout "$INNER_TIMEOUT" "$bc_file" || rc=$? + "$MAP2CHECK" $mode_flags $EXTRA_FLAGS --add-invariants --timeout "$INNER_TIMEOUT" "$bc_file" || rc=$? end=$(date +%s%N) if [ "$rc" -eq 3 ]; then diff --git a/tests/integration/test_memsafety_classifier.sh b/tests/integration/test_memsafety_classifier.sh new file mode 100755 index 000000000..e4f63fde2 --- /dev/null +++ b/tests/integration/test_memsafety_classifier.sh @@ -0,0 +1,28 @@ +#!/bin/bash +# Table test for classify_memsafety_result: a FALSE only counts when its kind +# matches the task's subproperty; a TRUE on a false task is the dangerous error. +set -u +. "$(dirname "$0")/../lib/memsafety_classifier.sh" +PASSED=0; FAILED=0 +check() { # expected subproperty verdict want + got=$(classify_memsafety_result "$1" "$2" "$3") + if [ "$got" = "$4" ]; then PASSED=$((PASSED+1)); else FAILED=$((FAILED+1)); echo " FAIL $1/$2/$3: want $4 got $got"; fi +} +check true "" TRUE correct-true +check true "" FALSE-DEREF wrong-false +check false valid-deref FALSE-DEREF correct-false +check false valid-free FALSE-FREE correct-false +check false valid-memtrack FALSE-MEMTRACK correct-false +check false valid-memcleanup FALSE-MEMCLEANUP correct-false +check false valid-deref FALSE-FREE wrong-false +check false valid-deref TRUE wrong-true +check false valid-deref UNKNOWN unknown +check false valid-deref TIMEOUT unknown +check true "" ERROR error +# sv-benchmarks' Juliet_Test MemSafety tasks declare no subproperty: any +# memory FALSE is the right answer there, but not a leak-at-exit or overflow. +check false any FALSE-DEREF correct-false +check false any FALSE-MEMTRACK correct-false +check false any FALSE-OVERFLOW wrong-false +echo " Results: $PASSED passed, $FAILED failed" +[ "$FAILED" -eq 0 ] diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index 9016c3938..924f00f68 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" @@ -446,12 +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) - -# 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. +# 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, 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 @@ -459,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 @@ -494,14 +514,326 @@ fi # There is no criterion to slice towards when the goal is a memory property or # branch coverage, so asking must be refused rather than quietly ignored. ( cd "$WORK/slice" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ - --memtrack --slice --nondet-generator symex --timeout 45 reach.c ) \ + --check-overflow --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, assert and memory properties 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" 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 + +# --- 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 + +# --- 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 + +# --- 17. memtrack slices the instrumented module and keeps the violation ----- +# Memory has no criterion in the user's program: the property is decided by the +# runtime calls MemoryTrackPass inserts, so the slice is taken AFTER +# instrumentation with every map2check_* call as a criterion. +mkdir -p "$WORK/mem" +cat > "$WORK/mem/dfree.c" <<'EOF' +#include +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + int unrelated = 0; + for (int i = 0; i < 4; i++) { unrelated += i; } + int *p = malloc(sizeof(int)); + free(p); + if (n == 11) { free(p); } + return unrelated; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 dfree.c ) > "$WORK/mem/plain.log" 2>&1 +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --nondet-generator symex --timeout 45 dfree.c ) > "$WORK/mem/slice.log" 2>&1 +plain_v=$(grep -oE "FALSE-[A-Z]+" "$WORK/mem/plain.log" | tail -1) +slice_v=$(grep -oE "FALSE-[A-Z]+" "$WORK/mem/slice.log" | tail -1) +if grep -q "Sliced with respect to map2check runtime" "$WORK/mem/slice.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/mem/slice.log" && [ -n "$slice_v" ] && \ + [ "$slice_v" = "$plain_v" ]; then + ok "memtrack slices after instrumentation and keeps the violation ($slice_v)" +else + fail "memtrack slice" "plain=[$plain_v] slice=[$slice_v]" + grep -E "Sliced|slice|VERIFICATION" "$WORK/mem/slice.log" | sed 's/^/ /' +fi + +# --- 18. memcleanup slices too and still sees the leak ---------------------- +cat > "$WORK/mem/leak.c" <<'EOF' +#include +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + int *p = malloc(sizeof(int)); + if (n == 5) { return 0; } + free(p); + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memcleanup-property --slice --nondet-generator symex --timeout 45 leak.c ) \ + > "$WORK/mem/leak.log" 2>&1 +if grep -q "Sliced with respect to map2check runtime" "$WORK/mem/leak.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/mem/leak.log"; then + ok "memcleanup slices and still finds the leak" +else + fail "memcleanup slice" "no slice, or the leak was lost" + grep -E "Sliced|slice|VERIFICATION" "$WORK/mem/leak.log" | sed 's/^/ /' +fi + +# --- 19. slicing must not invent a memory violation -------------------------- +cat > "$WORK/mem/safe.c" <<'EOF' +#include +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + int *p = malloc(sizeof(int)); + if (p == 0) { return 0; } + *p = n; + if (n == 11) { *p = 0; } + free(p); + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --nondet-generator symex --timeout 45 safe.c ) > "$WORK/mem/safe.log" 2>&1 +if grep -q "VERIFICATION FAILED" "$WORK/mem/safe.log"; then + fail "slice soundness" "a safe program was reported FALSE after slicing" +else + ok "slicing does not invent a memory violation" +fi + +# --- 20. a construct the slicer rejects falls back, loudly ------------------- +# sbt-slicer errors on llvm.stacksave (variable-length arrays). The run must +# fall back to the unsliced module and reach the same verdict. +cat > "$WORK/mem/vla.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +int main(void) { + int n = __VERIFIER_nondet_int(); + if (n > 0 && n < 10) { + int a[n]; + a[n] = 1; + return a[0]; + } + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 45 vla.c ) > "$WORK/mem/vla-plain.log" 2>&1 +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --nondet-generator symex --timeout 45 vla.c ) > "$WORK/mem/vla.log" 2>&1 +vla_plain=$(grep -oE "VERIFICATION [A-Z]+" "$WORK/mem/vla-plain.log" | tail -1) +vla_slice=$(grep -oE "VERIFICATION [A-Z]+" "$WORK/mem/vla.log" | tail -1) +if { grep -q "Sliced with respect to map2check runtime" "$WORK/mem/vla.log" || \ + grep -q "analysing the unsliced program" "$WORK/mem/vla.log"; } && \ + [ -n "$vla_slice" ] && [ "$vla_slice" = "$vla_plain" ]; then + ok "a slicer failure falls back and keeps the verdict ($vla_slice)" +else + fail "slice fallback" "plain=[$vla_plain] slice=[$vla_slice]" +fi + +# --- 21. a memory error inside an external function must not be sliced away -- +# CASTLE-787-2 overflows a stack buffer inside strcpy. No map2check_* call +# depends on that call, and the slicer treats external functions as only +# reading their arguments, so it was dropped -- and the run answered TRUE for a +# program with an out-of-bounds write. Every external call is a criterion now. +cat > "$WORK/mem/strcpy.c" <<'EOF' +#include +#include +int main(void) { + char username[10]; + strcpy(username, "Is_this_too_long_for_this_array_buffer?"); + printf("Hello %s!\n", username); + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --nondet-generator symex --timeout 45 strcpy.c ) > "$WORK/mem/strcpy.log" 2>&1 +if grep -q "VERIFICATION SUCCEEDED" "$WORK/mem/strcpy.log"; then + fail "external call slicing" "the overflowing strcpy was sliced away: TRUE" +else + ok "a memory error inside an external call survives slicing" +fi + +# --- 22. KLEE stopping on its timer is not a proof --------------------------- +# KLEE halting on --max-time exits 0, like a run that explored every path. One +# short path wrote NONE to the property file, and the run answered TRUE for a +# program with a reachable null dereference. Found by slicing (memsafety-cve +# frr.i, pacparser.i: the slice let KLEE reach its own timer), but it is not a +# slicing defect -- this program is not sliced. +mkdir -p "$WORK/halt" +cat > "$WORK/halt/halt.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + if (x == 0) { return 0; } + int n = 0; + while (1) { + int y = __VERIFIER_nondet_int(); + if (y > 3) { n++; } else { n += 2; } + if (n == 200000) { int *p = 0; *p = 1; } + } + return 0; +} +EOF +( cd "$WORK/halt" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --nondet-generator symex --timeout 20 halt.c ) > "$WORK/halt/run.log" 2>&1 +if grep -q "VERIFICATION SUCCEEDED" "$WORK/halt/run.log"; then + fail "halted KLEE verdict" "TRUE after KLEE stopped on its timer" +else + ok "a KLEE run halted on its timer is not reported TRUE" +fi + +# --- 23. an overflowing memcpy into a buffer nothing reads survives slicing -- +# clang lowers memcpy to llvm.memcpy.*; the copy feeds no criterion when the +# destination is never read again, so without the intrinsic as a criterion the +# slicer removed the overflow and the run could answer TRUE (review of 2b). +cat > "$WORK/mem/memcpy.c" <<'EOF' +#include +extern int __VERIFIER_nondet_int(void); +int main(void) { + char src[20]; + char buf[10]; + int n = __VERIFIER_nondet_int(); + memset(src, n, sizeof(src)); + memcpy(buf, src, 20); + return 0; +} +EOF +( cd "$WORK/mem" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --memtrack --slice --debug --nondet-generator symex --timeout 30 memcpy.c ) > "$WORK/mem/memcpy.log" 2>&1 +if grep "sbt-slicer" "$WORK/mem/memcpy.log" | grep -q "llvm.memcpy" && \ + ! grep -q "VERIFICATION SUCCEEDED" "$WORK/mem/memcpy.log"; then + ok "memory intrinsics are slicing criteria and the overflow is not called safe" +else + fail "intrinsic slicing" "llvm.memcpy not among the criteria, or TRUE" +fi + echo " ---" echo " Results: $PASSED passed, $FAILED failed" [ "$FAILED" -eq 0 ] || exit 1 diff --git a/tests/juliet/run_juliet_evaluation.sh b/tests/juliet/run_juliet_evaluation.sh index 6e69f0e4b..010e416ba 100755 --- a/tests/juliet/run_juliet_evaluation.sh +++ b/tests/juliet/run_juliet_evaluation.sh @@ -92,6 +92,7 @@ OUTER_TIMEOUT="${OUTER_TIMEOUT:-300}" INNER_TIMEOUT="${INNER_TIMEOUT:-60}" LIMIT="${LIMIT:-0}" # 0 = unlimited, counted across all CWEs PER_FAMILY="${PER_FAMILY:-3}" # files sampled per family; 0 = all +EXTRA_FLAGS="${EXTRA_FLAGS:-}" # opt-in flags for every run, e.g. --slice # LIMIT_PER_CWE is deliberately gone: it was the alphabetical-prefix cap that # produced the v3 sampling failure documented in the header. A per-CWE ceiling # cannot be expressed without reintroducing that bias, so the knob is @@ -241,7 +242,7 @@ for cwe in "${SCOPE_CWES[@]}"; do start=$(date +%s%N) rc=0 run_isolated "$raw" "$OUTER_TIMEOUT" \ - "$MAP2CHECK" $mode --timeout "$INNER_TIMEOUT" "$combined" || rc=$? + "$MAP2CHECK" $mode $EXTRA_FLAGS --timeout "$INNER_TIMEOUT" "$combined" || rc=$? end=$(date +%s%N) elapsed=$(python3 -c "print(round(($end - $start) / 1000000000, 1))") output=$(cat "$raw") diff --git a/tests/lib/memsafety_classifier.sh b/tests/lib/memsafety_classifier.sh new file mode 100644 index 000000000..52eae5c7e --- /dev/null +++ b/tests/lib/memsafety_classifier.sh @@ -0,0 +1,24 @@ +# shellcheck shell=bash +# classify_memsafety_result +# is classify_map2check_verdict's output. A FALSE counts as correct +# only when its kind matches the subproperty the task declares; FALSE of the +# wrong kind is a wrong answer, not a lucky one. +classify_memsafety_result() { + local expected="$1" sub="$2" verdict="$3" want="" + case "$sub" in + valid-deref) want="FALSE-DEREF" ;; + valid-free) want="FALSE-FREE" ;; + valid-memtrack) want="FALSE-MEMTRACK" ;; + valid-memcleanup) want="FALSE-MEMCLEANUP" ;; + # MemSafety tasks that declare no subproperty (sv-benchmarks' Juliet_Test): + # any memory-safety FALSE answers them, a leak-at-exit or overflow does not. + any) case "$verdict" in FALSE-DEREF|FALSE-FREE|FALSE-MEMTRACK) want="$verdict" ;; esac ;; + esac + case "$verdict" in + TRUE) [ "$expected" = "true" ] && echo correct-true || echo wrong-true ;; + FALSE*) if [ "$expected" = "false" ] && [ "$verdict" = "$want" ]; then + echo correct-false; else echo wrong-false; fi ;; + ERROR) echo error ;; + *) echo unknown ;; + esac +} diff --git a/tests/memsafety/run_memsafety_evaluation.sh b/tests/memsafety/run_memsafety_evaluation.sh new file mode 100755 index 000000000..c8d7ae786 --- /dev/null +++ b/tests/memsafety/run_memsafety_evaluation.sh @@ -0,0 +1,132 @@ +#!/bin/bash +# run_memsafety_evaluation.sh -- Map2Check over a stratified SV-COMP MemSafety +# (or MemCleanup) corpus, scoring each verdict against the task's expected +# verdict AND subproperty. +# +# Built for tacasv2b (slicing for the memory properties): the same corpus is +# run twice, with and without EXTRA_FLAGS=--slice, on the same build. What the +# comparison must show first is that slicing introduces no wrong answer, so +# the classes keep the two kinds of error apart: +# +# correct-true expected true, TRUE +# correct-false expected false, FALSE of the task's subproperty +# wrong-true expected false, TRUE -- the dangerous one +# wrong-false expected true and FALSE, or FALSE of the wrong kind +# unknown UNKNOWN or TIMEOUT +# error the tool failed +# +# Resumable: the CSV is the state, a task already in it is skipped. +# +# Environment: +# MANIFEST from build_corpus.py --property memsafety|memcleanup (required) +# PROPERTY memsafety | memcleanup (required) +# RESULTS_DIR where the CSV and raw logs go (required) +# MAP2CHECK_PATH install to run (required) +# SHARD/SHARDS process every SHARDS-th task starting at SHARD (default 0/1) +# BUDGET seconds given to map2check per task (default 120) +# DEADLINE_S stop starting new tasks after this many seconds (default 18000) +# EXTRA_FLAGS passed verbatim to map2check (e.g. "--slice") +set -u +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +BENCH="$SCRIPT_DIR/../testcomp/bench/sv-benchmarks/c" +. "$SCRIPT_DIR/../lib/verdict_classifier.sh" +. "$SCRIPT_DIR/../lib/memsafety_classifier.sh" + +MANIFEST="${MANIFEST:?set MANIFEST}" +PROPERTY="${PROPERTY:?set PROPERTY to memsafety or memcleanup}" +RESULTS_DIR="${RESULTS_DIR:?set RESULTS_DIR}" +MAP2CHECK_DIR="${MAP2CHECK_PATH:?set MAP2CHECK_PATH}" +MAP2CHECK="$MAP2CHECK_DIR/map2check" +SHARD="${SHARD:-0}" +SHARDS="${SHARDS:-1}" +BUDGET="${BUDGET:-120}" +DEADLINE_S="${DEADLINE_S:-18000}" +EXTRA_FLAGS="${EXTRA_FLAGS:-}" + +case "$PROPERTY" in + memsafety) MODE_FLAGS="--memtrack" ;; + memcleanup) MODE_FLAGS="--memcleanup-property" ;; + *) echo "unknown PROPERTY: $PROPERTY" >&2; exit 2 ;; +esac + +mkdir -p "$RESULTS_DIR/raw" +CSV="$RESULTS_DIR/results.csv" +if [ ! -f "$CSV" ]; then + echo "category,program,data_model,expected,subproperty,verdict,class,elapsed_s,slice" > "$CSV" +fi + +# Already-done set, read once (per-task re-reads make a resume O(n^2)). +declare -A DONE +while IFS=, read -r _cat prog _rest; do + [ -n "$prog" ] && DONE["$prog"]=1 +done < <(tail -n +2 "$CSV") + +started=$(date +%s) +index=-1 +processed=0 +skipped=0 + +# fd 3, not stdin: map2check inherits stdin, and consuming it would eat the +# rest of the manifest. +while IFS=$'\t' read -r category program data_model expected subproperty <&3; do + case "$category" in ''|\#*) continue ;; esac + index=$((index + 1)) + [ $((index % SHARDS)) -eq "$SHARD" ] || continue + + if [ -n "${DONE[$program]:-}" ]; then + skipped=$((skipped + 1)) + continue + fi + + now=$(date +%s) + if [ $((now - started)) -ge "$DEADLINE_S" ]; then + echo "[deadline] stopping after ${processed} tasks ($(( (now-started)/60 )) min)" + break + fi + + src="$BENCH/$program" + if [ ! -f "$src" ]; then + echo "$category,$program,$data_model,$expected,$subproperty,MISSING,error,0," >> "$CSV" + continue + fi + + # A private directory per task: map2check names its scratch by the input's + # hash, and a directory left behind by an aborted run would be reused. + work=$(mktemp -d) + cp "$src" "$work/" 2>/dev/null || { rm -rf "$work"; continue; } + name=$(basename "$src") + arch=$([ "$data_model" = "LP64" ] && echo 64bit || echo 32bit) + + t0=$(date +%s) + rc=0 + # shellcheck disable=SC2086 # the flag strings are word lists on purpose + ( cd "$work" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 $((BUDGET + 30)) \ + "$MAP2CHECK" $MODE_FLAGS $EXTRA_FLAGS --architecture "$arch" \ + --timeout "$BUDGET" "$name" ) > "$work/map2check.log" 2>&1 > "$CSV" + printf '[%s] %-12s %-52s %-17s %-13s %s\n' \ + "$(date +%H:%M:%S)" "$category" "$(basename "$program")" "$verdict" "$class" "${slice:-—}" + + # Raw logs only for the cases worth reading: every wrong answer and error. + case "$class" in + wrong-*|error) + cp "$work/map2check.log" "$RESULTS_DIR/raw/$(echo "$program" | tr '/' '_').m2c.log" 2>/dev/null ;; + esac + + rm -rf "$work" + processed=$((processed + 1)) +done 3< "$MANIFEST" + +echo "==========================================================" +echo "shard $SHARD/$SHARDS: $processed processed, $skipped already done" +echo "CSV: $CSV" +echo "==========================================================" diff --git a/tests/testcomp/build_corpus.py b/tests/testcomp/build_corpus.py index d7e19cada..043239e03 100755 --- a/tests/testcomp/build_corpus.py +++ b/tests/testcomp/build_corpus.py @@ -29,6 +29,12 @@ Usage: build_corpus.py --property cover-error --per-category 40 --out manifest.tsv build_corpus.py --property cover-branches --per-category 40 --out manifest.tsv + build_corpus.py --property memsafety --per-category 10 --out manifest.tsv + build_corpus.py --property memcleanup --per-category 10 --out manifest.tsv + +For the memory properties the manifest carries two more columns, the expected +verdict and the subproperty (valid-deref, valid-free, valid-memtrack, +valid-memcleanup), because a FALSE only counts when its kind matches. """ import argparse @@ -62,8 +68,47 @@ PROPERTY_FILE = { "cover-error": "coverage-error-call.prp", "cover-branches": "coverage-branches.prp", + "memsafety": "valid-memsafety.prp", + "memcleanup": "valid-memcleanup.prp", +} + +# The memory properties have no .set files in the local sv-benchmarks copy, so +# their categories are directory lists mirroring SV-COMP's MemSafety sets +# (tacasv2b spec, section 3.4). Threads and termination are left out: Map2Check +# supports neither, and running them would report zeros that mean nothing. +MEMORY_CATEGORIES = { + "memsafety": { + "Arrays": ["array-memsafety", "array-memsafety-realloc"], + "Heap": ["memsafety", "memsafety-ext", "memsafety-ext2", + "memsafety-ext3", "memsafety-broom", "ldv-memsafety", + "ldv-memsafety-bitfields", "forester-heap", + "heap-manipulation"], + "LinkedLists": ["list-simple", "list-ext-properties", + "list-properties", "ddv-machzwd"], + "Other": ["busybox-1.22.0", "coreutils-v8.31", "coreutils-v9.5-units", + "memsafety-cve", "uthash-2.0.2", "goblint-regression", + "goblint-coreutils"], + "Juliet": ["Juliet_Test"], + }, + "memcleanup": {"MemCleanup": ["*"]}, } +EXCLUDED_DIRS = ("pthread", "weaver", "termination") + + +def expand_dirs(dirs): + """Every task definition in the given directories, in sorted order.""" + import glob + + paths = [] + for directory in dirs: + for path in glob.glob(os.path.join(BENCH, directory, "*.yml")): + top = os.path.relpath(path, BENCH).split(os.sep)[0] + if top.startswith(EXCLUDED_DIRS): + continue + paths.append(path) + return sorted(set(paths)) + def expand_set(name): """Every task definition a .set file names, in sorted order.""" @@ -91,6 +136,7 @@ def task_info(yml_path, wanted_property): data_model = "ILP32" # the sv-benchmarks default when unstated has_property = False expected = "" + subproperty = "" in_properties = False current_property = None @@ -107,9 +153,17 @@ def task_info(yml_path, wanted_property): elif in_properties and stripped.startswith("- property_file:"): current_property = stripped.split(":", 1)[1].strip() elif in_properties and stripped.startswith("expected_verdict:"): - if current_property and current_property.endswith( - "unreach-call.prp"): + # Cover-* tasks report the unreach-call verdict (whether the + # error is reachable); the memory properties report their own. + verdict_of = ("unreach-call.prp" + if wanted_property.startswith("cover") + else PROPERTY_FILE[wanted_property]) + if current_property and current_property.endswith(verdict_of): expected = stripped.split(":", 1)[1].strip() + elif in_properties and stripped.startswith("subproperty:"): + if current_property and current_property.endswith( + PROPERTY_FILE[wanted_property]): + subproperty = stripped.split(":", 1)[1].strip() if current_property and current_property.endswith( PROPERTY_FILE[wanted_property]): has_property = True @@ -122,7 +176,15 @@ def task_info(yml_path, wanted_property): program = os.path.join(os.path.dirname(yml_path), input_file) if not os.path.isfile(program): return None - return program, data_model, expected + # valid-memcleanup is a single-subproperty property: its tasks declare no + # subproperty, but a FALSE of any other kind is still the wrong answer. + if wanted_property == "memcleanup" and expected == "false" and not subproperty: + subproperty = "valid-memcleanup" + # Juliet_Test's MemSafety tasks declare none: any memory-safety FALSE + # answers them (the classifier's "any"). + if wanted_property == "memsafety" and expected == "false" and not subproperty: + subproperty = "any" + return program, data_model, expected, subproperty def spread_order(items): @@ -177,11 +239,17 @@ def main(): sys.exit("sv-benchmarks not found at %s -- run fetch-benchmarks.sh" % BENCH) + memory = args.property in MEMORY_CATEGORIES + categories = (list(MEMORY_CATEGORIES[args.property]) if memory + else CATEGORIES) + per_category = {} summary = [] - for category in CATEGORIES: + for category in categories: applicable = [] - for yml in expand_set(category): + ymls = (expand_dirs(MEMORY_CATEGORIES[args.property][category]) + if memory else expand_set(category)) + for yml in ymls: info = task_info(yml, args.property) if info is not None: applicable.append((yml,) + info) @@ -189,8 +257,8 @@ def main(): summary.append((category, len(applicable), len(chosen))) per_category[category] = [ (category, os.path.relpath(program, BENCH), data_model, - expected or "unknown") - for yml, program, data_model, expected in chosen + expected or "unknown") + ((subproperty,) if memory else ()) + for yml, program, data_model, expected, subproperty in chosen ] # Round-robin, not grouped. A run that stops at its deadline should stop @@ -199,13 +267,17 @@ def main(): rows = [] depth = max((len(v) for v in per_category.values()), default=0) for index in range(depth): - for category in CATEGORIES: + for category in categories: bucket = per_category.get(category, []) if index < len(bucket): rows.append(bucket[index]) with open(args.out, "w") as handle: - handle.write("# category\tprogram\tdata_model\texpected_unreach\n") + if memory: + handle.write( + "# category\tprogram\tdata_model\texpected\tsubproperty\n") + else: + handle.write("# category\tprogram\tdata_model\texpected_unreach\n") for row in rows: handle.write("\t".join(row) + "\n") 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 ;; 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/KtestReaderTest.cpp b/tests/unit/frontend/KtestReaderTest.cpp index f58feed9e..e9c07f76f 100644 --- a/tests/unit/frontend/KtestReaderTest.cpp +++ b/tests/unit/frontend/KtestReaderTest.cpp @@ -255,3 +255,55 @@ 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); +} + +// --- a KLEE run that stopped on its timer did not finish --------------------- + +// KLEE halting on --max-time exits 0, exactly like a run that explored every +// path. With one short path having written NONE to the property file, that +// read as a proof: a reachable null dereference came back TRUE. +TEST(KleeHaltedOnTimer, DetectsTheHaltTimerLine) { + fs::path d = freshDir("halt"); + std::ofstream(d / "messages.txt") + << "KLEE: output directory is \"x\"\nKLEE: HaltTimer invoked\n" + "KLEE: halting execution, dumping remaining states\n"; + EXPECT_TRUE(Map2Check::kleeHaltedOnTimer(d.string())); + fs::remove_all(d); +} + +TEST(KleeHaltedOnTimer, AFinishedRunIsNotHalted) { + fs::path d = freshDir("finished"); + std::ofstream(d / "messages.txt") << "KLEE: output directory is \"x\"\n"; + EXPECT_FALSE(Map2Check::kleeHaltedOnTimer(d.string())); + EXPECT_FALSE(Map2Check::kleeHaltedOnTimer("/nonexistent/klee-last")); + fs::remove_all(d); +} diff --git a/tests/unit/frontend/SlicerTest.cpp b/tests/unit/frontend/SlicerTest.cpp new file mode 100644 index 000000000..12e9babe6 --- /dev/null +++ b/tests/unit/frontend/SlicerTest.cpp @@ -0,0 +1,201 @@ +/** + * 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"); +} + +// 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); +} + +// After instrumentation the memory property lives in the runtime calls +// MemoryTrackPass inserted; every one of them is a criterion, so nothing that +// records memory is sliced away. +TEST(RuntimeNamesInIR, FindsEveryMap2checkSymbolOnce) { + const std::string ir = + "declare void @map2check_malloc(ptr, i64)\n" + " call void @map2check_check_deref(ptr %3, i64 4), !dbg !7\n" + " call void @map2check_malloc(ptr %1, i64 8)\n" + " call i32 @__VERIFIER_nondet_int()\n"; + const std::vector names = Map2Check::runtimeNamesInIR(ir); + ASSERT_EQ(names.size(), 2u); + EXPECT_EQ(names[0], "map2check_malloc"); + EXPECT_EQ(names[1], "map2check_check_deref"); +} + +// A memory error can happen INSIDE an external function (strcpy overflowing a +// stack buffer). No map2check_* call depends on such a call, so without it as +// a criterion the slicer drops it and the bug with it -- measured: CASTLE-787-2 +// went from UNKNOWN to a wrong TRUE. Every declared-but-undefined function is +// a criterion in the post-instrumentation modes; intrinsics are not calls. +TEST(ExternalNamesInIR, FindsDeclaredFunctionsButNotIntrinsicsOrDefinitions) { + const std::string ir = + "define dso_local i32 @__map2check_main__() {\n" + " call ptr @strcpy(ptr %1, ptr @.str)\n" + "}\n" + "declare ptr @strcpy(ptr noundef, ptr noundef) #2\n" + "declare void @llvm.dbg.declare(metadata, metadata, metadata) #1\n" + "declare i32 @printf(ptr noundef, ...) #2\n" + "declare void @map2check_malloc(ptr, i64)\n" + "declare ptr @strcpy(ptr noundef, ptr noundef) #2\n"; + const std::vector names = Map2Check::externalNamesInIR(ir); + ASSERT_EQ(names.size(), 3u); + EXPECT_EQ(names[0], "strcpy"); + EXPECT_EQ(names[1], "printf"); + EXPECT_EQ(names[2], "map2check_malloc"); +} + +// clang lowers memcpy/memset/memmove (and struct copies) to intrinsics, and a +// copy that overflows into a buffer nothing reads again feeds no criterion: +// without its name the slicer drops it, the same wrong-TRUE shape as the +// strcpy of CASTLE-787-2. Other intrinsics (debug info) are not calls. +TEST(ExternalNamesInIR, KeepsTheMemoryIntrinsics) { + const std::string ir = + "declare void @llvm.memcpy.p0.p0.i64(ptr, ptr, i64, i1)\n" + "declare void @llvm.memset.p0.i64(ptr, i8, i64, i1)\n" + "declare void @llvm.memmove.p0.p0.i64(ptr, ptr, i64, i1)\n" + "declare void @llvm.dbg.declare(metadata, metadata, metadata)\n" + "declare void @llvm.lifetime.start.p0(i64, ptr)\n"; + const std::vector names = Map2Check::externalNamesInIR(ir); + ASSERT_EQ(names.size(), 3u); + EXPECT_EQ(names[0], "llvm.memcpy.p0.p0.i64"); + EXPECT_EQ(names[1], "llvm.memset.p0.i64"); + EXPECT_EQ(names[2], "llvm.memmove.p0.p0.i64"); +} + +// Slicing the instrumented module is only sound with the runtime checks as +// criteria. If the IR could not be read (a failed disassembly, an empty file) +// there are none, and the slice would remove every check: refuse instead. +TEST(InstrumentedSliceCriteria, RefusesWithoutRuntimeCalls) { + std::vector criteria; + EXPECT_FALSE(Map2Check::instrumentedSliceCriteria("", &criteria)); + EXPECT_FALSE(Map2Check::instrumentedSliceCriteria( + "declare i32 @__VERIFIER_nondet_int()\n", &criteria)); +} + +TEST(InstrumentedSliceCriteria, CollectsRuntimeThenExternalNames) { + std::vector criteria; + ASSERT_TRUE(Map2Check::instrumentedSliceCriteria( + " call void @map2check_check_deref(ptr %3, i64 4)\n" + "declare ptr @strcpy(ptr, ptr)\n" + "declare void @map2check_check_deref(ptr, i64)\n", + &criteria)); + ASSERT_EQ(criteria.size(), 2u); + EXPECT_EQ(criteria[0], "map2check_check_deref"); + EXPECT_EQ(criteria[1], "strcpy"); +}