Map2Check 9.0.0: AFL++ engine, smart seeds, engine alternation, sound TRUE verdicts

[GuilhermeBn198]

The full 9.0 campaign (the v15 corpora, paired task by task) is complete, and the assume-pruning defect it found is fixed and re-measured: see Full 9.0 campaign below.

Summary

This PR merges the whole TACAS line into one branch and sets the version to Map2Check 9.0.0. It covers:

• smart seeds;
• slicing optimizations;
• engine alternation;
• the fixes that made TRUE sound again;
• a study of --add-invariants.

Nine stacked branches are merged, plus the release and default commits on top of develop:

branch	scope
feat/tacas-smart-seeds	3a: seed store and typed seed exchange, plus the verdict fixes
feat/tacas-2d-slicing	2d: slice once per run, faster criteria, experiment knobs
feat/tacas-3b-alternation	3b: --alternate-engines, AFL++ build cache, fixes from review
feat/tacas-memtrack-intrinsics	memset/memcpy/memmove checked under LLVM 16
feat/tacas-3c-seed-ranking	3c v1: new-edge entries first
feat/tacas-memtrack-strings	%s/puts string checks (off by default)
feat/tacas-fuzzer-suite	the fuzzer corpus as Cover-Branches cases (off by default)
feat/tacas-klee-vector-replay	KLEE vectors replayed natively; harness and input fixes
feat/tacas-invariants	Clam profiles, invariant count, MAP2CHECK_PREOPT=ssa

New defaults (measured in R26)

• The hybrid is the alternation (--alternate-engines, with seed exchange) whenever --timeout is given.
  • On Cover-Error it ties the seed-exchange hybrid (157/213 each).
  • On Cover-Branches it leads (53.5% vs 46.5%, partial).
  • --fixed-hybrid keeps the 8.x schedule.
• The fuzzer's corpus joins Cover-Branches suites (MAP2CHECK_FUZZER_SUITE=0 drops it).
• Everything else stays off, and each knob is documented in the README with what it was measured to do:
  • --add-invariants (optional and under study, see docs/backlog.md);
  • MAP2CHECK_PREOPT=ssa;
  • MAP2CHECK_CHECK_CSTRINGS;
  • the slice knobs.

Why 9.0.0 and not 8.2

• The engine changed, from LibFuzzer to AFL++ 4.40c. --nondet-generator fuzzer is now --nondet-generator afl.
• Several verdicts change meaning, so the same program can get a different answer than under 8.x:
  • a KLEE run that did not explore every path is no longer TRUE;
  • the program's own abort() prunes the path instead of ending KLEE's search.

Changes

Verdict soundness (these fixes affect every mode)

• The program's abort() prunes the path. NonDetPass rewrites the program's abort() into map2check_assume(0). SV-COMP benchmarks use abort() as an assumption, both inline and through assume_abort_if_not. With --exit-on-error-type=Abort, KLEE used to end its whole search on the first such path and answer TRUE. This was the cause of every wrong TRUE of the control arm in R15: the pals_* family and sin_interpolated_index-1.
• KLEE's exit 0 is not a proof unless it explored every path. The following now make the run incomplete, and so UNKNOWN:
  • the HaltTimer;
  • a concretized input ("silently concretizing", for example a symbolic double pinned to 0);
  • any *.err or *.early state;
  • the memory cap ("skipping fork", "over memory cap");
  • a KLEE run with no done lines, meaning it crashed.
• Assumptions under KLEE prune with klee_silent_exit. A failed klee_assume(0) is a KLEE user error, and it counted as a dropped path. An intermediate version of this PR had that bug: it read partially completed paths and could not prove any program that contains an assumption. Fixed and covered by a test.

Engines and seeds

• Seed store <hash>.seeds/ (3a). The store lives beside the scratch directory, so it survives the phases. Exchange works in both directions:
  • the AFL++ queue is replayed through the witness binary into typed .ktest seeds for KLEE;
  • KLEE's vectors go back to the fuzzer, all of them, uncapped.
• --alternate-engines (3b). AFL++ and KLEE take turns:
  • a turn ends when its engine stagnates: AFL_EXIT_ON_TIME for AFL++, and for KLEE the covered instructions read from run.stats (SQLite is optional at build time; SIGINT goes to the KLEE pid);
  • windows (0.1T for the fuzzer, 0.3T for KLEE) and the stagnation patience double every round;
  • each phase measures its own setup time and deducts it from the budget.
• KLEE's vectors replayed natively. After a KLEE phase that found nothing, KLEE's vectors are completed with zeros past their end and run through the witness binary. KLEE's partial paths often go on to the error. The seed-exchange hybrid used to find these only by accident, in its last fuzzer dry run.
• AFL++ binaries built once per run (<hash>.build/), and the three builds share one budget.
• 3c v1: AFL++ queue entries marked +cov are sent to KLEE first.

Slicing

• Slice once per run (<hash>.slice/, keyed by content). A slicer failure is cached too.
• Criteria collected by a plain scan instead of std::regex: on the eca-* programs the regex took about 45 s.
• Experiment knobs: MAP2CHECK_SLICE_CLEANUP=light|o2 and MAP2CHECK_SLICER_FLAGS. None was promoted: every variant stayed within ±3 tasks.

Memory safety

• Memory intrinsics are checked. MemoryTrackPass matched llvm.memset/memcpy by their LLVM 6 names, so under LLVM 16 no intrinsic was checked and memmove never was. It now dispatches on MemSetInst / MemTransferInst.
• MAP2CHECK_CHECK_CSTRINGS=1, off by default. Under KLEE, printf runs as an external call, so a %s read of an unterminated buffer was never checked.
  • It fixes a wrong TRUE in Juliet CWE121 CWE193 cpy bad.
  • It creates a wrong FALSE in the matching good task. There the terminator is an uninitialized byte, which SV-COMP counts as zero.
  • It stays off until a larger Juliet sample decides between the two.

Test suites

• The Cover-Branches cap of 50 and the deduplication apply across phases, and every run starts from an empty suite.
• MAP2CHECK_FUZZER_SUITE=1, off by default: the fuzzer corpus becomes Cover-Branches test cases, up to half of the suite.

--add-invariants (INV-1 in the log)

• The history of the old engine:
  • The SV-COMP 2019/2020 builds (v7.3.x) ran crab-llvm with --crab-promote-assume. That flag emits llvm.assume, which NonDetPass does not map and which KLEE ignores. I tested this on the release's KLEE 2.1 and on KLEE 3.1, with and without --optimize. In those builds the invariants had no effect.
  • Before October 2018 the configuration was --crab-track=arr --crab-add-invariants=after-load, and the invariants did reach KLEE.
• Where the gain actually came from. On a probe loop program, a safe variant and a buggy one, compiling through Clam decided both even with no invariant inserted. The gain came from the SSA preprocessing, not from the invariants.
• What this PR adds:
  • MAP2CHECK_CLAM_PROFILE=default|memory|none;
  • the number of invariants inserted, in the log;
  • a fallback when Clam fails;
  • MAP2CHECK_PREOPT=ssa (mem2reg + simplifycfg), for reachability and assert only. With it on, the memory modes produced FALSE-FREE on safe programs.

Unmodeled nondet types (#74)

• The fix. NonDetPass instrumented only 16 __VERIFIER_nondet_* types. A call to float, longlong, ulonglong, u8/u16/u32 or __VERIFIER_nondet_memory was an external call: KLEE killed every state and the task was UNKNOWN by construction.
• What each type now has:
  • a KLEE and an AFL++ generator of the right width;
  • a full-width log entry: 64-bit and float values no longer pass through the int logger, and floats print as %.9g so they round-trip;
  • decoding in the ktest reader.
• nondet_memory gives one uchar input per byte, which is how the validators' harness reads it.
• Tests: 8 new unit tests, and synthetic programs for each type: UNKNOWN before the fix, FAILED after, Result: TRUE on TestCov 3.11.
• What the fix uncovered: the KLEE nondet-log explosion (KLEE: gravar o klee_log.csv com valores simbólicos explode os estados no fim de cada caminho #75), fixed below.

KLEE nondet-log explosion (#75)

• Cause. At the end of each violating path, the KLEE runtime wrote klee_log.csv with fprintf, and the values were still symbolic. uClibc's vfprintf forks on every digit it converts. KLEE reached the target, then multiplied states while writing the log and never finished.

• The fix, each part driven by run.istats:

  • the logged values are pinned to one model before printing (klee_get_value + klee_assume, in order, so the row stays one consistent vector);
  • the rows are formatted without printf. Even with concrete values, vfprintf was 93% of a 1,000-read path. The file is byte for byte the same (NonDetLogTest);
  • a log past 1,024 rows is not written. The violating .ktest carries the same vector, and the frontend already falls back to it;
  • the log container grows geometrically, and the heap copy that leaked one row per read is gone.

• Measured on a straight-line program with N nondet reads and the target at the end, KLEE only:

  N	before	after
  5	FAILED, 28 s	FAILED, 1 s
  10	UNKNOWN	FAILED, 1 s
  1,000	UNKNOWN	FAILED, 6 s
  10,000	UNKNOWN	FAILED, 31 s

• Intel-TDX is still 0/8 on the 300 s probe, with KLEE's default cap and with MAP2CHECK_KLEE_MAX_MEMORY=6000 (new knob, default unchanged). The log no longer blocks KLEE: it now completes about 850 paths per task, where it completed 0 before. What remains is the programs' own path explosion: thousands of havoc reads followed by a long validity precondition.

• Tests: integration 51/51; section 38 checks KLEE alone behind 12 nondet reads.

Official Test-Comp 2026 validation

• tests/testcomp/official/run.sh generate|validate runs the competition's own validators under BenchExec: TestCov gcc/clang unformatted and TestCoCa clang formatted. Each task gets its own property files, and each validator's scratch is dropped so a full corpus fits on disk.
• Official corpora (build_corpus_official.py), drawn from the Test-Comp 2026 task set with proportional stratification:
  • Cover-Error;
  • Cover-Branches, 3,500 tasks.
• The AFL++ toolchain ships as a self-contained archive for the validation image.

Smaller fixes

• AFL++ input past its end reads as zeros. Before, it wrapped around, so a while (nondet()) loop never ended and afl-fuzz aborted in its dry run.
• A fuzzer link error is reported with its cause, and an unreadable input program is reported clearly.
• Evaluation harnesses:
  • children no longer inherit the manifest descriptor (the program under test was moving the loop's file offset);
  • a crash replayed from the fuzzer is no longer classified as a tool failure.

Results

Full 9.0 campaign, paired with v15 (2026-10-05)

Setup. Both versions ran on the same tasks under the same conditions: the corpora of the v15 campaign, 300 s and 4 GB per task, compared task by task. 9.0 ran with its defaults: alternating hybrid, seed exchange, and the fuzzer corpus in Cover-Branches suites. The campaign build is 76eedfc75. The assume fix (e4e0b74c7, 6848d2395) came after the campaign; its rerun is reported separately below.

At a glance

corpus	what it measures	v15	9.0	change
Test-Comp Cover-Error (1,087 tasks)	tasks whose suite reaches the error, confirmed by TestCov (1 point each)	470	722	+252 (+54%)
Test-Comp Cover-Branches (2,765 tasks)	mean branch coverage of the suite, measured by TestCov	41.4%	45.1% (≈47.0% with the fix)	+3.7 p.p. (≈+5.6)
Juliet C (8,060 cases)	bugs found in the vulnerable variants (4,030 cases)	1,154 (28.6%)	1,808 (44.9%)	+654
	false alarms on the fixed variants (4,030 cases)	120 (3.0%)	120 (3.0%)	=
CASTLE (119 cases in scope)	bugs found / false alarms	54 / 1	54 / 1	=

Cover-Error: finding the error and proving its absence

A task counts only when TestCov runs the suite and confirms the error is reached. A wrong TRUE means the tool claimed the error unreachable on a task where it is reachable. The competition penalises that heavily, and it is what this line set out to remove.

	v15	9.0
covered (TestCov confirms the error)	470	722	+265 gained, −13 lost
wrong TRUE	175	0	soundness: a TRUE now needs an exhaustive KLEE run
ERROR (tool crash)	9	0
median time per task	176 s	72 s	the alternation stops early once it finds the error

By category (covered): ECA 58 → 146, ProductLines 111 → 169, Sequentialized 9 → 78, XCSP 22 → 38, Arrays 84 → 92, Loops 102 → 109. No category loses.

Cover-Branches: how much of the program the suite exercises

Score: the branch coverage TestCov measures when it runs the suite. A task with no validated suite counts as 0%.

	v15	9.0 (campaign)	9.0 + assume fix
mean coverage	41.4%	45.1%	≈47.0% (projected)
median coverage	38.5%	47.6%
tasks better / worse / equal vs v15	—	932 / 381 / 1,452
XCSP mean	77.6%	54.6% ⚠️	96.6%
TestCov failed to validate (TESTCOV_ERROR)	110	140	109 of them fail on v15 too; almost all ECA, where TestCov exceeds 300 s
median time per task	114 s	274 s	the alternation keeps working while the suite still grows

By category (mean coverage, v15 → 9.0): Arrays 60.7 → 76.2, BitVectors 60.6 → 70.0, ControlFlow 44.9 → 53.1, Recursive 57.8 → 65.3, Heap 40.6 → 47.3, Loops 70.5 → 73.8, LinkedLists 75.8 → 78.5, Sequentialized 56.0 → 58.7, Floats 5.4 → 6.7, ProductLines 20.3 → 20.7, ECA 10.5 → 10.6. XCSP was the only category that lost, and the fix below recovers it.

The assume fix. In the campaign build, a path that a failed assumption pruned under KLEE wrote no test. 50 tasks (43 XCSP, 7 Floats) ended with an empty suite. The fix has two parts:

• the pruned path ends normally (_exit), so KLEE writes its test;
• the test is marked, and when the suite reaches its cap of 50 a deeper path replaces it, even in a later phase. Without that, on xcsp/AllInterval the shallow pruned tests filled the suite first, and coverage fell from 95% to 9%.

Rerun with the fix (mean coverage, same conditions):

set	tasks	v15	9.0 (campaign)	9.0 + fix
tasks left with no test	50	88.8%	0%	88.8%
XCSP tasks that already had tests	76	64.9%	85.5%	94.7%
random control	100	46.9%	54.4%	55.0%
Cover-Error random sample (tasks covered)	100	—	63	63, still 0 wrong TRUE

The projected ≈47.0% replaces these 226 tasks in the campaign result; the other tasks were not rerun.

Re-run of the categories #74 affected (official corpus, 2026-10-12)

Same conditions as the V99 campaign on the official corpus: 900 s, 8 GB, 4 cores. All suites were validated by the three official validators.

category	tasks	before the fix	with the fix	official score
Floats	33	11	33	33.0 (22 UNKNOWN → FAILED, from ~830 s to 0–92 s)
regression guard (ProductLines, Loops, Sequentialized, Hardware, Arrays, Heap)	15	15	15	15.0
Intel-TDX (sample)	12	0	0	— (#75)

Report: docs/reports/2026-10-12-issue74-rerodada.md.

Juliet C and CASTLE: memory-safety and overflow bugs

Each Juliet test comes in a bad variant, which has the bug, and a good variant, which has it fixed. Finding the bug in a bad variant is a TP. Saying it is safe is an FN. Reporting a bug in a good variant is an FP.

	v15	9.0
bad variants: bug found (TP)	1,154	1,808	+654
bad variants: claimed safe (FN)	1,145	1,084	−61
bad variants: no answer (UNKNOWN / TIMEOUT)	1,351	1,138
bad variants: tool crash (ERROR)	380	0
good variants: confirmed safe (TN)	3,290	3,262	−28, moved to UNKNOWN / TIMEOUT
good variants: false alarm (FP)	120	120	=
good variants: tool crash (ERROR)	0	4	KLEE core dumps

CASTLE is unchanged: TP 54, TN 44, FN 14, FP 1 on the 119 cases in scope.

Caveats

• The corpora are the v15 sample, not the Test-Comp 2026 task set. The official set has 1,895 Cover-Error and 14,322 Cover-Branches tasks, including Hardware and Intel-TDX subcategories the sample lacks, and it normalises scores per subcategory. These numbers compare 9.0 with v15. They do not predict a competition score (docs/backlog.md).
• Per-task data and every round are in docs/reports/tacas-experiment-log.md.

Development rounds (samples)

All rounds use the Test-Comp samples r15-ce.tsv (Cover-Error, 213 tasks) and r15-cb.tsv (Cover-Branches, 120 tasks), which are nested inside the v15 campaign, with 300 s per task. The per-round data is in docs/reports/tacas-experiment-log.md.

v15 baseline (full campaign, before this line)

Cover-Error, 1,087 tasks	control 470 covered, slice 412
Cover-Branches	53.0%
Juliet	TP 1154, FP 120
CASTLE	TP 54, FN 14, FP 1

Cover-Error, 213-task sample

round	build / arm	covered	wrong TRUE	median time
R15	v15 control	111	27	43 s
R15	develop after #68–#71	129	5	5 s
R16	+ smart seeds, before the verdict fixes	148	7	6 s
R19	control, with all verdict fixes	128	0	3 s
R19	--seed-exchange	151 (+23 −0 vs control)	0	5 s
R19	--alternate-engines, before its fix	148 (+20 −0)	0	9 s
R19	--slice and its 4 variants	127–128 (±3)	0	4–5 s
R24	control + KLEE vector replay	146 (+20 −2 vs R19 control)	0	4 s
R20	seeds + 3c ranking	150 (+2 −3 vs R19 seeds)	0	4 s
R23	seeds, intermediate build	154	0	4 s
R24	seeds + KLEE vector replay	155	0	5 s
R26	--seed-exchange, this branch	157 (+29 −0 vs R19 control)	0	3 s
R26	--alternate-engines (the new default), this branch	157 (+30 −1)	0	9 s

• v15 → this branch, same 213 tasks: 111 → 157 covered (+41%), wrong TRUE 27 → 0.
• Wrong TRUE is 0 in every arm since R19, confirmed at scale.
• Seed exchange gives +23 −0 over the fixed control. The KLEE-vector replay gives most of that gain to the plain hybrid as well: 146 against 151.

Cover-Branches, 120-task sample

round	arm	mean coverage
R15	v15 / develop	48.0% / 47.7%
R16	seeds	49.7% (26 better, 9 worse)
R19	control / seeds / alternate	44.7% / 46.1% / 50.3% (alternate: 43 better, 5 worse)
R22	control + fuzzer corpus in the suite	49.7% vs 44.7% (40 better, 3 worse)
R26 (partial, 107)	alternate + fuzzer corpus (the new default), this branch	52.9% vs 46.0% (40 better, 7 worse)
R26 (partial, 97)	seeds + fuzzer corpus, this branch	49.0% vs 44.5% (30 better, 11 worse)

R19 ran under heavier machine load than R15: 11 containers at once, and memory ran out at the end. That is why the R19 control scored lower on the same sample.

--add-invariants and SSA (R25, 71 Cover-Error + 50 MemSafety tasks)

arm	Cover-Error covered	ERROR	MemSafety correct / wrong-true / wrong-false
off	51	0	28 / 2 / 2
MAP2CHECK_PREOPT=ssa	50	0	—
Clam, no invariants	50	2	25 / 1 / 4
Clam, default profile	49	4	27 / 1 / 4
Clam, memory profile	44	7	25 / 2 / 4

• No gain in the hybrid, and more wrong FALSE on MemSafety.
• The ERRORs came from Clam running unbounded; it is now bounded at 0.2T and falls back to the plain compile.
• The option stays optional. A dedicated study is in the backlog.
• The history of the old engine is in the "--add-invariants" section above.

SV-COMP (R17 and R21, 120 s per task)

	control	seeds	alternate
MemSafety (50): correct	29	30	29
MemSafety: wrong TRUE	2	1	1
MemCleanup (10): correct	6	6	6
NoOverflows (20): correct / unknown	2 / 17	2 / 17	2 / 17

• The 6 MemSafety error results in R17 came from the harness classifier, not from Map2Check (fixed).
• The %s check (R21) fixes one wrong TRUE and introduces one wrong FALSE. On CASTLE it raised FP from 1 to 4 (a scanf buffer, argv[0]). It is off by default.
• CASTLE (R21, %s check on): TP 54, TN 44, FN 12, FP 4. Baseline R14: TP 53, FN 14, FP 1.

Tests

• Unit tests: 12/12 (ctest). New: AlternationTest, plus new cases in KtestReaderTest, SlicerTest, SeedStoreTest and TestSuiteTest.
• Integration (tests/integration/test_testcomp_regressions.sh): 50/50 with the new defaults; section 11 now checks the 8.x behaviour through --fixed-hybrid. Also 50/50 with MAP2CHECK_PREOPT=ssa. New sections 29–37 cover the abort rewrite, dropped paths, the slice cache, the AFL++ nondet loop, alternation, intrinsics, %s, the fuzzer suite and the link error.
• Verdict classifier: 21/21 (tests/integration/test_verdict_classifier.sh).

Documentation

• README: a new section on the engines, the options and the verdict semantics, plus a table of the environment knobs with what each was measured to do.
• CLAUDE.md: the hybrid, and the state kept beside the scratch directory.
• docs/backlog.md:
  • the --add-invariants study;
  • the KLEE memory limit for parallel rounds;
  • the pitfalls of the campaign harness.
• Addendum to docs/reports/2026-08-16-crabllvm-review.md.
• docs/reports/tacas-experiment-log.md: every round, R1–R26, plus the official-environment rounds and NonDetPass: tipos __VERIFIER_nondet_* não modelados zeram tarefas (Intel-TDX, Floats) para UNKNOWN #74.
• docs/reports/2026-10-06-ambiente-testcomp-oficial.md and docs/reports/2026-10-12-issue74-rerodada.md.

🤖 Generated with Claude Code

[GuilhermeBn198]

R26 complete. On SV-COMP the alternating hybrid, the new default, loses no correct TRUE: MemSafety correct-true is 10 vs 10, and wrong TRUE goes from 2 to 1. MemCleanup and NoOverflows are identical across arms. CASTLE matches v15 exactly (TP 54, FN 14, FP 1), and v15's 4 TIMEOUTs are now UNKNOWN.

9.0 campaign, first batches, paired with v15 on the same tasks:

• Cover-Error (532 of 1087 tasks): 394 covered vs 288 (+112 −6); wrong TRUE 0 vs 57; median time 19 s vs 59 s.
• Juliet groups a+b (2,271 tasks): TP 776 vs 340, FN 90 vs 118, FP 20 vs 20, ERROR 0 vs 114.

Still running: Cover-Error (the rest), Juliet groups c and d, then Cover-Branches (2,765 tasks).

[GuilhermeBn198]

The 9.0 campaign found two defects on Juliet's CWE190/191 group. Both are fixed in 76eedfc:

1. The AFL++ binaries were linked without -lm. A program calling sqrt or pow lost its fuzzer phase, and the harness counted those 55 tasks as ERROR.
2. A KLEE blocked in a native external call ignored the stagnation stop. The Juliet fscanf variants hand __isoc99_fscanf a uClibc FILE*, and KLEE then ignores both the interrupt and its own --max-time. It held the rest of its window until the final SIGKILL. It is now killed 10 s after the interrupt, and the time goes to the next phase.

Neither defect changes a verdict; the second one only wasted time.

The campaign continues on the fixed build, which is now this branch's head.

• Rerun with it: Juliet group c in full, the 2 Cover-Error tasks that call libm, and Cover-Branches (it had barely started).
• Kept from the previous build: CASTLE, the rest of Cover-Error, and Juliet groups a, b and d. None of these had a libm error.

[GuilhermeBn198]

9.0 campaign: Cover-Error complete, 1,087 tasks paired with v15:

	v15	9.0
covered	470	722 (+265 −13, +54%)
wrong TRUE	175	0
ERROR	9	0
median time	176 s	72 s

No category loses. The largest gains: ECA 58 → 146, ProductLines 111 → 169, Sequentialized 9 → 78.

Juliet, complete groups:

• a: TP 214 → 611, ERROR 269 → 0;
• b: TP 216 → 473, FP 30 → 30;
• d: unchanged TP; 11 TN → UNKNOWN (to investigate).

Group c is being rerun on the fixed build.

CASTLE is identical to v15. Cover-Branches has just started: 48.3% vs 42.1% on the first 111 of 2,765 tasks.