tacasv2c: --slice for overflow by GuilhermeBn198 · Pull Request #71 · hbgit/Map2Check

GuilhermeBn198 · 2026-09-28T02:05:26Z

Summary

tacasv2c extends --slice to --check-overflow, which completes per-property slicing for tacasv2 (reach, assert, memory, overflow). Only --cover-branches still refuses --slice, because it has no criterion.

This PR builds on #70 (tacasv2b), and through it on #68 and #69. The base is develop so the CI runs. Merge it last.

Spec: docs/superpowers/specs/2026-09-27-tacasv2c-slicing-overflow-design.md
Plan: docs/superpowers/plans/2026-09-27-tacasv2c-slicing-overflow.md
Log: docs/reports/tacas-experiment-log.md (R7 probe, R11, R13, R14)

Why this is small

The OverflowPass checks are runtime calls (map2check_binop_add/sub/mul/sdiv/srem…). The post-instrumentation slice from tacasv2b therefore already keeps them. The only code change is adding OVERFLOW_MODE to the hook after callPass.

What changed

map2check.cpp: overflow slices the instrumented module. The refusal message now names only branch coverage.
Harness:
- build_corpus.py gains --property overflow (NoOverflows). The categories are Main (bitvector, nla-digbench, recursive-simple, loop-zilu, signedintegeroverflow-regression, goblint-regression) and BusyBox.
- No Juliet category: sv-benchmarks' Juliet_Test declares no no-overflow task, and Juliet CWE-190/191 are measured through tests/juliet instead.
- The runner accepts PROPERTY=overflow, and the classifier maps no-overflow to FALSE-OVERFLOW.

Results

R7 (probe): on busybox chgrp-incomplete-2.i the slice drops from 927 to 487 instructions (−47%). The reduction on large programs is bigger than for memory.
R13 / R14, NoOverflows (20 tasks): control and slice give identical classes in R14 (4 correct, 16 unknown), with 0 wrong answers in both arms. Median reduction is 10%, max 37%.
R14, CASTLE overflow cases and Juliet CWE-190/191/369: control and slice are identical.

Test plan

Integration, 32/32 on an idle machine. Sections 24–25 are new here: the violation is kept with slice, and no overflow is invented.
Classifier 17/17 (adds no-overflow and any rows).
R11, R13 and R14 recorded in the log.
CI

🤖 Generated with Claude Code

…docs

Found by the final whole-branch review and confirmed by the Task 7 smoke test in the rebuilt dev image. - NonDetGeneratorAFL.c: define the persistent-mode macros exactly as afl-cc 4.40c injects them. The library is compiled to bitcode by plain clang, so without them every build (including KLEE-only and CI) failed, and afl-clang-fast never re-preprocesses the linked -result.bc, so the ##SIG_AFL_PERSISTENT## marker must already be in the bitcode. - Caller: replay crashes from afl-out/default/crashes (the single instance's directory), feeding each over stdin (a standalone persistent binary ignores argv), bounded by timeout, and stop at the first confirmed one so a non-reproducing replay cannot overwrite it. - Caller: set the headless AFL_* flags on the command line rather than relying on the image ENV; record crashing seeds as crashes and stop at the first crash, as the previous fuzzer did. - Caller: use a private afl-in/ unless --seed-exchange, and copy the AFL++ queue back into seeds/ under it (afl-fuzz never writes into -i). - tools.hpp: MAP2CHECK_AFL_CC / MAP2CHECK_AFL_FUZZ overrides; AFL_CC is AFL++'s own variable and reusing it recursed or disabled instrumentation. - Regression test: --nondet-generator afl; stale comments updated. Verified in map2check-dev:aflpp: persistent + shared-memory mode detected, VERIFICATION FAILED on the plan's smoke program and on a non-trivial one, test_testcomp_regressions.sh 19/19, ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

- Cap each crash replay at max(5s, 10% of the budget): a crash that does not reproduce from a fresh process may loop, and must not eat KLEE's share. - Select crash/queue files by type (regular, not README.txt) rather than by AFL++'s "id:" naming, which AFL_SHA1_FILENAMES changes. - Warn when the AFL++ input dir or placeholder seed cannot be prepared. - Document that seeds/ does not yet survive into the next hybrid phase: each Caller recreates the scratch directory. Inherited unchanged from v15; fixing it changes what the hybrid measures, so it belongs to the smart-seeds work. - Regression test: count only the fuzzer's copied discoveries (afl-*), since the placeholder seed made the old file count pass trivially. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19 (4 afl-* discoveries copied), ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The v15 LibFuzzer runs with -use_value_profile=1, which solves comparison guards such as `x == 123456`. AFL++ with PCGUARD alone does not, so the tacasv1 comparison measured an unarmed AFL++ against an armed LibFuzzer. CmpLog (input-to-state) is AFL++'s counterpart. - Caller compiles a third binary, <hash>-cmplog.out, from the same -result.bc with AFL_LLVM_CMPLOG=1 and passes it to afl-fuzz with -c. Optional: if it does not build, the fuzzer runs without it and says so. - NonDetGeneratorAFL.c rewinds its read position for every __AFL_LOOP iteration. The position was function-static and carried over between inputs, so the same input read different values on every persistent run. That nondeterminism defeats CmpLog's byte-to-operand mapping. This reverses the earlier choice to preserve the index for v15 parity; without the reset CmpLog has no effect. Fuzzer-only smoke, 3 runs x 8 seeded bugs, same image: v15 LibFuzzer 17/24 | AFL++ + CmpLog, index kept 4/24 | AFL++ + CmpLog, index rewound 17/24. - Regression test: the KLEE -> fuzzer export check retries when the (now stronger) fuzzer phase solves seed.c first and KLEE never runs. - Spec: addendum §2.1 with the decision and the numbers. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19 (twice), ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

afl-fuzz -V compares gettimeofday() readings. A wall clock stepped backwards -- measured at 1.1s within 20s under WSL2 -- underflows the elapsed time, and afl-fuzz stops after a few hundred executions ("Time limit was reached", run_time ~2^64). `timeout` uses a relative timer, and it is how the previous fuzzer was bounded. The budget is also clamped to at least 1s, since `timeout 0` means no limit. Spec §2.1 updated with the final fuzzer-only smoke (3 runs x 8 bugs): v15 LibFuzzer 20/24, AFL++ + CmpLog with the rewound index 17/24, without it 8/24. Hybrid verdicts identical to v15 on all 11 programs. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19, ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…input 621db93 downgrades a KLEE violation to UNKNOWN when no input vector can be recovered, to stop FAILED verdicts that nothing reproduces. It asked readViolatingKtest for a non-empty vector, so a program that reads no nondeterministic input -- whose aborting path has a .ktest with zero objects -- was downgraded too, and its suite came out with no test case. That is tests/testcomp/programs/no_input.c, and it has failed the TestCov CI gate on develop since that commit landed (run 33523637266). hasViolatingKtest counts an .abort.err whose .ktest exists, empty or not; the downgrade now uses it. The halted-KLEE case 621db93 guards against still has no .abort.err at all, so it is still downgraded. Verified in both the current CI image (ghcr map2check-dev:latest) and map2check-dev:aflpp: run_testcov_suite.sh 6/6 (no_input.c COVERED), test_cover_branches.sh 5/5, test_benchexec_toolinfo.py 16/16, test_testcomp_regressions.sh 19/19, ctest 9/9 (3 new KtestReader tests). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

… suite valid Diagnosis on 12 tasks the v15 slice arm lost, with the tacasv1 build: the slicer's cutoff inserts exit(0) without !dbg and KLEE aborts on a broken module; and nondet calls the slicer drops misalign the suite on the original program. Cutoff off + nondets as criteria: 6/12 -> 10/12. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>