From 9344e5513d2e2a1a82edd5ffe8d76d11cb078b45 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 22:34:30 -0400 Subject: [PATCH 1/4] fix(afl): replay writes the nondet log on assumption-pruned paths A reactive while(1) program ends every execution in a failed assumption; the witness replay longjmp'd out without writing klee_log.csv, so the fuzzer's corpus never reached the Cover-Branches suite (Hardness median: 2 tests in the Test-Comp 2027 pre-run). --- .github/workflows/ci.yml | 1 + CHANGELOG.md | 9 +++ .../backend/library/lib/NonDetGeneratorAFL.c | 12 +++- .../integration/test_fuzzer_pruned_corpus.sh | 56 +++++++++++++++++++ 4 files changed, 77 insertions(+), 1 deletion(-) create mode 100644 tests/integration/test_fuzzer_pruned_corpus.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c5613b70a..5ea2a9078 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -368,6 +368,7 @@ jobs: bash tests/integration/test_ktest_object_names.sh bash tests/integration/test_testcomp_regressions.sh bash tests/integration/test_fuzzer_leftovers.sh + bash tests/integration/test_fuzzer_pruned_corpus.sh bash tests/integration/test_exit_codes.sh bash tests/integration/test_cwe_mode_mapping.sh ' diff --git a/CHANGELOG.md b/CHANGELOG.md index c722917e4..b3e4fc864 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,15 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. ### Fixed +- **Cover-Branches: the fuzzer's corpus reaches the suite on reactive + programs.** In a `while (1)` program that reads its inputs under + `assume_abort_if_not`, every execution ends in a failed assumption. The + witness replay that turns a queue entry into a test case jumped out on it + without writing the nondet log, and every entry was dropped. In the + Test-Comp 2027 pre-run, the median Hardness suite had 2 tests while AFL++ + held hundreds of inputs. The replay now writes the inputs read so far; the + seed exchange (fuzzer → KLEE) gets the same vectors. + - **The run stays below its memory limit** (Test-Comp 2027 pre-run: 1,747 runs ended as OUT OF MEMORY at 3 GB). The limit is read from the run's cgroup (`memory.max`; `MAP2CHECK_MEMORY_LIMIT_MB` overrides it): diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c index 541c32aea..f179194d6 100644 --- a/modules/backend/library/lib/NonDetGeneratorAFL.c +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -28,7 +28,17 @@ void nondet_destroy() { nondet_log_destroy(); } static jmp_buf map2check_reject_env; -void nondet_cancel() { longjmp(map2check_reject_env, 1); } +/* The replay that turns a queue entry into a test case (MAP2CHECK_SEED_REPLAY) + * needs the inputs read so far even when the path ends in a failed + * assumption: a reactive `while (1)` program ends no other way, and without + * the log every one of its entries was dropped. The validator's harness + * aborts at the same assumption, after covering the same branches. */ +void nondet_cancel() { + static int replay = -1; + if (replay < 0) replay = getenv("MAP2CHECK_SEED_REPLAY") != NULL; + if (replay) nondet_generate_aux_witness_files(); + longjmp(map2check_reject_env, 1); +} void nondet_assume(int expr) { if (!expr) { diff --git a/tests/integration/test_fuzzer_pruned_corpus.sh b/tests/integration/test_fuzzer_pruned_corpus.sh new file mode 100644 index 000000000..3a96578c8 --- /dev/null +++ b/tests/integration/test_fuzzer_pruned_corpus.sh @@ -0,0 +1,56 @@ +#!/bin/bash +# test_fuzzer_pruned_corpus.sh -- the fuzzer's corpus reaches the Cover-Branches +# suite even when every path ends in a failed assumption. +# +# A reactive program (`while (1)` reading inputs under assume_abort_if_not, +# the shape of the Hardness tasks) never returns from main: each execution +# ends when an input violates an assumption. The witness replay that turns a +# queue entry into a test case used to longjmp out on that assumption without +# writing the nondet log, so every entry was dropped -- in the Test-Comp 2027 +# pre-run the median Hardness suite had 2 tests while AFL++ held hundreds. + +set -u + +MAP2CHECK_DIR="${MAP2CHECK_PATH:-/workspace/install_e2e}" +WORK=$(mktemp -d) +trap 'rm -rf "$WORK"' EXIT + +PASSED=0 +FAILED=0 +ok() { echo " PASS $1"; PASSED=$((PASSED+1)); } +fail() { echo " FAIL $1: $2"; FAILED=$((FAILED+1)); } + +echo "=== Fuzzer corpus on assumption-pruned paths ===" + +cat > "$WORK/task.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void abort(void); +void assume_abort_if_not(int cond) { if (!cond) abort(); } +int state = 0; +int main(void) { + while (1) { + int x = __VERIFIER_nondet_int(); + assume_abort_if_not(x > 0 && x < 100); + if (x > 50) state++; + else if (x > 25) state += 2; + else state--; + } + return 0; +} +EOF + +(cd "$WORK" && MAP2CHECK_AFL_EXIT_ON_TIME=10 \ + "$MAP2CHECK_DIR/map2check" --cover-branches --generate-test-suite \ + --nondet-generator afl --timeout 40 task.c > map2check.out 2>&1) + +n=$(grep -o 'Test suite: [0-9]* test cases from the fuzzer' "$WORK/map2check.out" \ + | grep -o '[0-9]*' | tail -1) +if [ "${n:-0}" -gt 0 ]; then + ok "the fuzzer's corpus is in the suite ($n test cases)" +else + fail "the fuzzer's corpus is in the suite" "none (see below)" + grep -E 'AFL\+\+ ran|Test suite' "$WORK/map2check.out" +fi + +echo " Results: $PASSED passed, $FAILED failed" +[ "$FAILED" -eq 0 ] From 818ce07058720445bd282a6a9362fe72795c19b4 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 8 Nov 2026 01:27:31 -0400 Subject: [PATCH 2/4] fix(afl): leave the rejected value out of the replayed vector With it, the validator's harness reproduces the abort(), and gcov writes nothing for a test that aborts: 44 such tests measured 2.38% where the 21 KLEE paths ending in exit gave 62.7% (hardness_kloop_100_1loop_file-32). Without it, the harness runs out of inputs at that read and exits. --- CHANGELOG.md | 3 ++- modules/backend/library/lib/NonDetGeneratorAFL.c | 15 ++++++++++++--- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b3e4fc864..7248e1b0a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,7 +13,8 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. witness replay that turns a queue entry into a test case jumped out on it without writing the nondet log, and every entry was dropped. In the Test-Comp 2027 pre-run, the median Hardness suite had 2 tests while AFL++ - held hundreds of inputs. The replay now writes the inputs read so far; the + held hundreds of inputs. The replay now writes the inputs read before the + rejected one (a test ending in `abort()` counts nothing under gcov); the seed exchange (fuzzer → KLEE) gets the same vectors. - **The run stays below its memory limit** (Test-Comp 2027 pre-run: 1,747 runs diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c index f179194d6..35a45b1b8 100644 --- a/modules/backend/library/lib/NonDetGeneratorAFL.c +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -31,12 +31,21 @@ static jmp_buf map2check_reject_env; /* The replay that turns a queue entry into a test case (MAP2CHECK_SEED_REPLAY) * needs the inputs read so far even when the path ends in a failed * assumption: a reactive `while (1)` program ends no other way, and without - * the log every one of its entries was dropped. The validator's harness - * aborts at the same assumption, after covering the same branches. */ + * the log every one of its entries was dropped. + * + * The last value read -- the one the assumption rejected -- is left out. With + * it, the validator's harness reproduces the abort(), and a test that ends in + * abort() counts nothing: gcov writes its data only on a normal exit (TestCov + * measured 2.38% for 44 such tests where 21 ending in exit gave 62.7%). + * Without it, the harness runs out of inputs at that read and exits. */ void nondet_cancel() { static int replay = -1; if (replay < 0) replay = getenv("MAP2CHECK_SEED_REPLAY") != NULL; - if (replay) nondet_generate_aux_witness_files(); + if (replay) { + MAP2CHECK_CONTAINER log = map2check_nondet_get_log(); + if (log.size > 0) log.size--; + nondet_log_to_file(log); + } longjmp(map2check_reject_env, 1); } From 189de2c6a652ffb0e815c0ae44e0eadd049f7956 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 8 Nov 2026 08:13:46 -0400 Subject: [PATCH 3/4] fix(test-suite): fuzzer prefixes of pruned paths give way to full inputs --- CHANGELOG.md | 7 +++++-- .../backend/library/lib/NonDetGeneratorAFL.c | 8 +++++++- modules/frontend/caller.cpp | 18 ++++++++++++++++-- modules/frontend/caller.hpp | 3 ++- modules/frontend/map2check.cpp | 19 +++++++++++++------ 5 files changed, 43 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7248e1b0a..beff739ea 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,8 +14,11 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. without writing the nondet log, and every entry was dropped. In the Test-Comp 2027 pre-run, the median Hardness suite had 2 tests while AFL++ held hundreds of inputs. The replay now writes the inputs read before the - rejected one (a test ending in `abort()` counts nothing under gcov); the - seed exchange (fuzzer → KLEE) gets the same vectors. + rejected one; the seed exchange (fuzzer → KLEE) gets the same vectors. + These prefixes enter the suite as assumption-pruned cases, after the inputs + that ran to the end, and give way to them when the suite is full (otherwise + they took all 50 places: `hardness_kloop_100_1loop_file-32` fell from 62.7% + to 2.4%). - **The run stays below its memory limit** (Test-Comp 2027 pre-run: 1,747 runs ended as OUT OF MEMORY at 3 GB). The limit is read from the run's cgroup diff --git a/modules/backend/library/lib/NonDetGeneratorAFL.c b/modules/backend/library/lib/NonDetGeneratorAFL.c index 35a45b1b8..793178875 100644 --- a/modules/backend/library/lib/NonDetGeneratorAFL.c +++ b/modules/backend/library/lib/NonDetGeneratorAFL.c @@ -9,6 +9,7 @@ #include "../header/NonDetGenerator.h" #include "../header/NonDetLog.h" +#include #include #include #include @@ -37,7 +38,10 @@ static jmp_buf map2check_reject_env; * it, the validator's harness reproduces the abort(), and a test that ends in * abort() counts nothing: gcov writes its data only on a normal exit (TestCov * measured 2.38% for 44 such tests where 21 ending in exit gave 62.7%). - * Without it, the harness runs out of inputs at that read and exits. */ + * Without it, the harness runs out of inputs at that read and exits. + * + * The marker file tells the frontend the vector is a pruned prefix: it may + * fill the suite but must give way to an input that ran to the end. */ void nondet_cancel() { static int replay = -1; if (replay < 0) replay = getenv("MAP2CHECK_SEED_REPLAY") != NULL; @@ -45,6 +49,8 @@ void nondet_cancel() { MAP2CHECK_CONTAINER log = map2check_nondet_get_log(); if (log.size > 0) log.size--; nondet_log_to_file(log); + FILE *marker = fopen("map2check_pruned", "w"); + if (marker != NULL) fclose(marker); } longjmp(map2check_reject_env, 1); } diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index c755f2eb8..1f250b216 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -667,8 +667,13 @@ std::string environmentKnob(const char *name) { } // namespace std::vector> Caller::fuzzerCorpusVectors( - size_t cap) { + size_t cap, std::vector *pruned) { + // Inputs that ran to the end first, then the prefixes of paths a failed + // assumption ended (the replay leaves a marker): a prefix stops before the + // code a full input reaches, and in the suite it must not take the place of + // one (hardness_kloop_100_1loop_file-32: 62.7% -> 2.4% when it did). std::vector> vectors; + std::vector> prefixes; std::error_code error; const std::string queue = "afl-out/default/queue"; const std::string replay = @@ -702,9 +707,18 @@ std::vector> Caller::fuzzerCorpusVectors( std::vector values = Map2Check::readNonDetLog(replay + "/" + Map2Check::kleeLogCSV); if (values.empty() || !seen.insert(values).second) continue; - vectors.push_back(values); + if (std::filesystem::exists(replay + "/map2check_pruned", error)) { + prefixes.push_back(values); + } else { + vectors.push_back(values); + } } std::filesystem::remove_all(replay, error); + if (pruned != nullptr) { + pruned->assign(vectors.size(), false); + pruned->resize(vectors.size() + prefixes.size(), true); + } + vectors.insert(vectors.end(), prefixes.begin(), prefixes.end()); return vectors; } diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 3b2c8e229..dafeb1830 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -221,7 +221,8 @@ class Caller { * queue entries, ranked as for KLEE, each replayed through the witness * binary for the values it actually reads, duplicates dropped. Bounded like * the KLEE export (5% of the budget). Empty when no fuzzer ran. */ - std::vector> fuzzerCorpusVectors(size_t cap); + std::vector> fuzzerCorpusVectors( + size_t cap, std::vector *pruned = nullptr); /** Instrument and execute nondeterministic generator */ diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index bbb990c1f..a81d1ee9c 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -153,7 +153,8 @@ void emitTestSuite(const std::string &outputDir, const std::string &programFile, const std::string &architecture, const std::string &specification, bool foundViolation, bool coverBranches, Map2Check::Map2CheckMode mode, - const std::vector> &fuzzerVectors) { + const std::vector> &fuzzerVectors, + const std::vector &fuzzerPruned) { Map2Check::TestSuiteMetadata metadata; metadata.producer = std::string("Map2Check ") + Map2CheckVersion; metadata.specification = specification; @@ -189,18 +190,22 @@ void emitTestSuite(const std::string &outputDir, const std::string &programFile, // metric rewards by construction (on by default; MAP2CHECK_FUZZER_SUITE=0). // Cases from assumption-pruned paths (see evictPrunedCase) hold no claim // on the suite: they count toward neither share and give way when full. + // The corpus's own pruned prefixes come last (fuzzerCorpusVectors) and + // are written as pruned cases, under the same rule as KLEE's. size_t fromFuzzer = 0; - for (const std::vector &inputs : fuzzerVectors) { + for (size_t i = 0; i < fuzzerVectors.size(); ++i) { + const std::vector &inputs = fuzzerVectors[i]; + const bool isPruned = i < fuzzerPruned.size() && fuzzerPruned[i]; if (writer.caseCount() - writer.prunedCount() >= kMaxBranchTestCases / 2) { break; } if (writer.hasTestCase(inputs)) continue; if (writer.caseCount() >= kMaxBranchTestCases && - !writer.evictPrunedCase()) { + (isPruned || !writer.evictPrunedCase())) { break; } - if (!writer.writeTestCase(inputs, false)) { + if (!writer.writeTestCase(inputs, false, isPruned)) { Map2Check::Log::Warning("could not write test case to " + outputDir); return; } @@ -877,18 +882,20 @@ int map2check_execution(map2check_args args) { // On by default since 9.0 (R22: 49.7% against 44.7% on the fixed hybrid; // R26: 53.5% with the alternation); MAP2CHECK_FUZZER_SUITE=0 turns it off. std::vector> fuzzerVectors; + std::vector fuzzerPruned; const char *fuzzerSuite = std::getenv("MAP2CHECK_FUZZER_SUITE"); if (args.coverBranches && !(fuzzerSuite != nullptr && std::string(fuzzerSuite) == "0") && generator == Map2Check::NonDetGenerator::AFLPlusPlus) { - fuzzerVectors = caller->fuzzerCorpusVectors(kMaxBranchTestCases); + fuzzerVectors = + caller->fuzzerCorpusVectors(kMaxBranchTestCases, &fuzzerPruned); } emitTestSuite(outputDir, caller->c_program_fullpath, args.entryFunction, args.architecture, resolveSpecification(args.propertyFile, caller->getOriginalPath(), args.mode), foundViolation, args.coverBranches, args.mode, - fuzzerVectors); + fuzzerVectors, fuzzerPruned); } // (6) Clean map2check execution (folders and temp files) From 315f7507b6b496f64904f0beda6410b2d3c33b0d Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sun, 8 Nov 2026 15:27:52 -0400 Subject: [PATCH 4/4] docs(tacas): the fuzzer-corpus round (mg4, mg5, mg6) --- docs/reports/tacas-experiment-log.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/docs/reports/tacas-experiment-log.md b/docs/reports/tacas-experiment-log.md index 87442f82c..17a5e780e 100644 --- a/docs/reports/tacas-experiment-log.md +++ b/docs/reports/tacas-experiment-log.md @@ -1465,3 +1465,25 @@ existe, em vez de um `map2check-testcomp.py` à parte. - em relação ao mg2, pelo CRC, só o wrapper muda; - smoke test num `ubuntu:24.04` limpo, com `python3` e `gcc-multilib`: passou; - BenchExec com 120 s: `done`. + +## Rodada CP-corpus (2026-11-08): corpus do fuzzer em caminhos podados (mg4 → mg5 → mg6) + +24 tarefas de Cover-Branches (`tacas-results/MEM/cp.tsv`: 14 Hardness, 6 Floats, 2 Loops, +2 Arrays), 900 s / 3 GB / 1 núcleo, TestCov gcc. Base: Zenodo 24031752. Uma execução por +braço, com a máquina disputada (o BenchExec avisou de swap). + +| Braço | Mudança | Soma | Pior que a base | +|---|---|---|---| +| base | — | 7,81 | — | +| mg4 | o replay grava o log em caminho podado | 13,71 | kloop_100-32: 62,7 → 2,4 | +| mg5 | + tira o valor rejeitado do vetor | 13,14 | kloop_100-32: 2,4 | +| mg6 | + prefixos podados do fuzzer cedem lugar (`189de2c6a`) | 13,56 | nenhuma | + +- **Causa da regressão do mg4:** os prefixos curtos do fuzzer ocupavam as 50 vagas da suíte e + as entradas completas (17 leituras) ficavam de fora. No mg6 eles entram como casos podados, + depois das entradas completas: kloop_100-32 volta a 62,7. +- **A hipótese do mg5** (o `abort()` no fim do teste) estava errada; o mg6 mantém o corte + do valor rejeitado. +- **mg6 em relação ao mg4:** steplocals (74,7 → 4,0) e filler_pr_ci-166 (41,6 → 2,0) caíram + até o nível da base; softmax e cartpole ficaram abaixo do mg4. Com uma execução só, não + dá para separar o efeito do ruído.