fix: the fuzzer's corpus reaches Cover-Branches suites on reactive programs

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

CHANGELOG.md

@@ -7,6 +7,19 @@ 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 before the
+  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
   (`memory.max`; `MAP2CHECK_MEMORY_LIMIT_MB` overrides it):

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.

modules/backend/library/lib/NonDetGeneratorAFL.c

@@ -9,6 +9,7 @@
 #include "../header/NonDetGenerator.h"
 #include "../header/NonDetLog.h"
 
+#include <stdio.h>
 #include <stdlib.h>
 #include <stdint.h>
 #include <setjmp.h>
@@ -28,7 +29,31 @@ 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 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.
+ *
+ * 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;
+  if (replay) {
+    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);
+}
 
 void nondet_assume(int expr) {
   if (!expr) {

modules/frontend/caller.cpp

@@ -667,8 +667,13 @@ std::string environmentKnob(const char *name) {
 }  // namespace
 
 std::vector<std::vector<std::string>> Caller::fuzzerCorpusVectors(
-    size_t cap) {
+    size_t cap, std::vector<bool> *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<std::vector<std::string>> vectors;
+  std::vector<std::vector<std::string>> prefixes;
   std::error_code error;
   const std::string queue = "afl-out/default/queue";
   const std::string replay =
@@ -702,9 +707,18 @@ std::vector<std::vector<std::string>> Caller::fuzzerCorpusVectors(
     std::vector<std::string> 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;
 }
 

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<std::vector<std::string>> fuzzerCorpusVectors(size_t cap);
+  std::vector<std::vector<std::string>> fuzzerCorpusVectors(
+      size_t cap, std::vector<bool> *pruned = nullptr);
 
 
   /** Instrument and execute nondeterministic generator */

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<std::vector<std::string>> &fuzzerVectors) {
+                   const std::vector<std::vector<std::string>> &fuzzerVectors,
+                   const std::vector<bool> &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<std::string> &inputs : fuzzerVectors) {
+    for (size_t i = 0; i < fuzzerVectors.size(); ++i) {
+      const std::vector<std::string> &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<std::vector<std::string>> fuzzerVectors;
+    std::vector<bool> 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)

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 ]