Map2Check 9.0.0: AFL++ engine, smart seeds, engine alternation, sound TRUE verdicts by GuilhermeBn198 · Pull Request #73 · hbgit/Map2Check

GuilhermeBn198 · 2026-09-30T04:15:53Z

Draft. No run has yet measured every change of this PR together. The numbers below come from rounds that each ran a subset. Some rounds are still running and are marked partial. The PR stays in draft until a consolidated run on this branch (feat/map2check-9.0) confirms them.

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, 52 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`

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.

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

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 (partial, 178)	seeds + 3c ranking	128 vs 128 (+2 −2)	0
R23 (partial, 177)	seeds, final build	132 vs 128 (+5 −1)	0

Wrong TRUE went from 27 (v15) to 0 in every arm, 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 (partial, 99)	control + fuzzer corpus in the suite	49.2% vs 44.8% (33 better, 2 worse); TestCov validated 97 of 99

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.

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, which is why it is off by default.

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 on the tip, 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).

Still running

These rounds run on frozen installs. I will post each result in this PR as it completes:

R20 (3c ranking), remainder;
R22 seeds (fuzzer corpus in the suite);
R23 seeds and alternate on the final build;
R24 seeds;
R21 CASTLE (false-positive gate for the %s check);
R25 (--add-invariants profiles and MAP2CHECK_PREOPT=ssa against off).

Before leaving draft

A consolidated run of this branch (Cover-Error, Cover-Branches, SV-COMP MemSafety/NoOverflows, CASTLE, Juliet), compared with v15, with wrong TRUE = 0 as the gate.
Decide the defaults:
- which hybrid: fixed, --seed-exchange or --alternate-engines;
- MAP2CHECK_FUZZER_SUITE;
- MAP2CHECK_PREOPT=ssa;
- MAP2CHECK_CHECK_CSTRINGS.
CI green on this branch.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Seeds now live in <cwd>/<hash>.seeds beside the scratch directory, which every phase recreates. KLEE's vectors and the fuzzer's discoveries go to its afl/; the fuzzer phase reads it as -i. With --seed-exchange the KLEE share is 0.6 so the third phase gets real time. The cwd is restored between phases under --debug too (the nesting that broke the store path), and main removes the store after the last phase unless --debug. The single-vector exportFuzzerVectorAsKtest, which read a log that no longer existed, is gone; task 3 replaces it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

At the end of the AFL++ phase (no violation found), up to 64 queue entries are replayed through the witness binary inside the seed store's replay/ directory -- so a replay cannot overwrite a recorded violation -- and the typed nondet log of each becomes a .ktest in ktest/. The witness runtime writes that log only on a violation (to keep KLEE forks from clobbering it), so the replay opts in with MAP2CHECK_SEED_REPLAY. KLEE then runs with --seed-dir, extension/truncation allowed and --seed-time at a quarter of its budget. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…oofs From the final review of the smart-seeds plumbing: - the fuzzer corpus is converted for KLEE only on the hybrid's first phase (a KLEE phase follows), and the replays stop at 5% of the budget; - the seed store is wiped at the start of a run and removed on every way out of main (scope guard), unless --debug keeps it; - a seed ends at the first nondet read the converter cannot express, instead of skipping it and shifting every later value (KLEE matches seeds by position); - the store path is quoted in the KLEE and afl-fuzz commands. Found while tightening the tests: a KLEE proof (SUCCEEDED) was followed by the third fuzzer phase printing UNKNOWN last; a proof now ends the hybrid like a violation does. Under --debug the cwd is restored between phases even without the exchange, so only the last phase's scratch is kept. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…the search In SV-COMP abort() is not an error; programs use it to discard a path, inline as well as through assume_abort_if_not (seq-mthreaded/pals_*: 'if(!(i2)) {abort();}'). KLEE runs with --exit-on-error-type=Abort, so the first path violating such an assumption halted the whole search with exit 0 and the run answered TRUE for a program with a reachable bug. Every wrong TRUE of the tacasv2 control arm in the R15 Cover-Error sample had this shape (pals_* and float-benchs/sin_interpolated_index-1). NonDetPass now rewrites the program's own abort() calls into map2check_assume(0), the same pruning assume_abort_if_not already gets. It runs before the runtime is linked, so the runtime's abort (a recorded violation) is untouched, and TargetPass still records reach_error before a following abort. Pre-existing (v15); unrelated to seeding, shipped with this round. Integration section 29. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

KLEE exits 0 whenever its state queue empties, and the frontend read that as an exhaustive exploration. It is not one when KLEE concretized a symbolic input (a nondet double pinned to 0: float-benchs/sin_interpolated_index-1 answered TRUE) or killed states with its own errors (a VLA of symbolic size: loops/insertion_sort-1-2 under --slice answered TRUE). kleeDroppedPaths() generalizes the HaltTimer check to both; such a run is a timeout. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

kleeDroppedPaths read KLEE's 'partially completed paths', which counts the paths an assumption pruned as well: klee_assume(0) on an already-false path is a KLEE user error, and even klee_silent_exit counts as partial. No program with an assume_abort_if_not or an inline abort could be proved any more -- the section 29 safe program went from TRUE to UNKNOWN. nondet_assume (KLEE) now prunes with klee_silent_exit, which leaves no test behind, and a dropped path is read from what a killed state does leave: any *.err or *.early test, besides the HaltTimer and a concretized input. Section 29 now requires the safe program to be proved. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Two more ways KLEE ends without having explored every path, from the review of the dropped-paths check: a KLEE that crashed (solver, LLVM assertion, the OOM killer) writes no "done" lines and no .err while the paths it did finish may have written NONE; and near --max-memory it stops forking ("skipping fork") or kills states ("over memory cap") and can still exit 0. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Every hybrid phase recreates the scratch directory and used to run sbt-slicer again. On eca-* the slicer timed out (0.2T) in phase 1 and again in phase 2, and the run was killed past its budget with no suite: the 4 ERROR of the R15 slice arm. The slice -- or the slicer's failure -- is now kept beside the scratch (<hash>.slice/), keyed by the input's content and every setting that shapes the slice, for the later phases of the same run. Two environment knobs for the R19 arms, defaults unchanged until measured: MAP2CHECK_SLICE_CLEANUP (none|light|o2, an opt pass over the fresh slice) and MAP2CHECK_SLICER_FLAGS (appended to sbt-slicer, e.g. --cda=ntscd). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

From the review: the MAP2CHECK_SLICE_CLEANUP opt pipeline ran unbounded, outside every engine's window. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

On the eca-* modules (megabytes of IR) the three regex scans that collect the slicing criteria took ~45 s, outside every budget: with the slicer's own 0.2T that was 105 s before the first engine, and the run was killed past its deadline with no verdict (R19: the slice arm's 4 remaining ERROR). A plain scan with the same results (SlicerTest). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…self Past the end of the test case the AFL++ generator started over from its first byte, so 'while (__VERIFIER_nondet_int())' fed by the placeholder seed "A" never ended: afl-fuzz's dry run timed out and the fuzzer aborted before its first execution, on the loop idiom sv-benchmarks is full of. Reads past the end now return zero -- what the witness replay logs, so the suite built from that log stays exact. It also read data[0] of an empty test case. Covered by integration section 32 (next commit). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…nates The fixed 0.2/0.6/0.2 split held an engine that had stopped progressing to the end of its share and cut one that still was. Under --alternate-engines (implies --seed-exchange) the fuzzer and KLEE take turns until a violation, a proof or too little time: each phase is bounded by a window that doubles every round of its engine (0.1T fuzzer, 0.3T KLEE) and ends when its engine goes max(10 s, 0.05T) without new coverage -- AFL_EXIT_ON_TIME for the fuzzer, a watch over KLEE's run.stats (SQLite, optional at build time) that SIGINTs it. A KLEE stopped that way is incomplete, never TRUE. Between turns: KLEE's latest tests seed its next turn (kleeprev/), the fuzzer's own seeds are not replayed back to KLEE, at most 64 KLEE vectors go to a short fuzzer window, and the test suite numbers after the cases an earlier phase wrote instead of overwriting them. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Slicing through sbt-slicer rather than a linked dg, the AFL++/KLEE coordination inside the C++ frontend rather than a Python coordinator with IPC, the verdict fixes the TACAS rounds found, and what is still open (2.4 knobs and 3.2.4 in R19, 3c ranking, the MemoryTrackPass intrinsics). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

- The Cover-Branches cap and duplicates count across phases: every KLEE turn added up to 50 cases, mostly replays of the seeds it was given. The writer knows the cases already in the suite, and a run starts from an empty one (re-running in a directory kept the previous run's cases). - Budget: each phase measures its own setup (compile, instrument, link), which no window covers; a phase starts only if what is left covers it, and its window leaves it out. The fuzzer keeps KLEE's 5 s reserve. - The stagnation SIGINT goes to KLEE itself, not to timeout, which forwarded it to the child and its group: two signals, and the halt dump was lost. - KLEE's stagnation period doubles with its rounds, so it can still finish the paths that make a proof after coverage stops rising. - The fuzzer corpus in the store is capped (256), kleeprev/ is kept only when alternating, the store and slice cache are recorded for cleanup as soon as a phase starts, and the flag warns and stands down without --timeout or with --nondet-generator. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…growing patience R19 lost 5 eca-* tasks to --alternate-engines against the fixed hybrid. The fixed hybrid covers them in its last fuzzer phase: completed with zeros past their end, some of KLEE's partial paths reach the error in afl-fuzz's dry run (sig 06). The alternation sent only the 64 latest KLEE vectors and dropped exactly those. The cap (and the corpus cap) came from a nondet loop whose calibration never ended -- fixed since by the zeros past the end. Two more costs of each fuzzer turn on large programs: the three AFL++ binaries were rebuilt every phase (~24 s on eca-*; now cached per run by the modules' content, <hash>.build/), and the fuzzer's fixed 15 s stagnation cut ended its turns at ~17 s; its patience now doubles per round like KLEE's. Problem06_label05: UNKNOWN -> FAILED at 157 s (the fixed hybrid: 281 s). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The fuzzer, witness and CmpLog builds were each bounded by 0.25T, so in sequence they could take 0.75T; on eca-* they ran the process past its deadline with no verdict (R19). They now share one deadline. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…nters MemoryTrackPass matched the memory intrinsics by name, and the names carried the pointer types (llvm.memset.p0i8.i64) that LLVM 16 no longer writes (llvm.memset.p0.i64): no memset, memcpy or memmove clang emitted was checked, and memmove never was. memset(p, 0, 16) on 8 malloc'd bytes came back UNKNOWN. Dispatched by the intrinsic's kind now (MemSetInst, MemTransferInst), plus the libc names; memset's size is widened to the i64 map2check_load takes. In-bounds copies -- from string constants, struct assignment, memmove -- stay TRUE (integration section 34). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Every missing AFL++ binary was reported as one that 'did not build within Ns' -- the budget's fault -- including a link error (an undefined reach_error) that no budget would fix. The build's status is kept: a timeout is still reported as one, anything else as a failure with the first line of afl-build.log that names the cause. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

KLEE takes at most 64 queue entries, and they were the oldest by id: once the queue outgrew the cap, what the fuzzer found late never reached KLEE. AFL++ marks the entries that hit new edges with ',+cov'; those now come first, each group in id order (tacas 3c, v1). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The Cover-Branches suite came only from KLEE's paths; the fuzzer's queue -- the inputs that reached new edges -- was thrown away with the scratch directory. With MAP2CHECK_FUZZER_SUITE=1 a fuzzer phase replays its ranked queue through the witness binary for the values each entry reads and writes them as test cases, up to half the suite so KLEE's paths keep room, without duplicates. Off by default until measured (R22). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

KLEE's partial paths -- the states it dumped at a halt -- stop where the search stopped. Run natively through the fuzzer's witness binary, completed with zeros past their end, some of them go on to the error: that is how the seed-exchange hybrid covered eca-* tasks KLEE left UNKNOWN, by accident, in its last fuzzer phase's dry run. Now done on purpose right after a KLEE phase that found nothing (not for Cover-Branches), within 10% of the budget, with the witness from the AFL++ build cache -- so the plain hybrid gets it too. A violation's files become the phase's, as a confirmed fuzzer crash's do. eca-rers2012/Problem06_label05, plain hybrid: UNKNOWN -> FAILED at 207 s (1850 vectors replayed in 15 s). Measured in R24. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

The harness reads its manifest on fd 3, and every child inherited it: map2check, KLEE, and through KLEE's native external calls (read, lseek, close on a numeric fd) the program under test itself. The shared offset moved under the loop: a shard ended after 29 of 71 tasks with no deadline reached, and another wrote 38 rows belonging to the next shard (R19, R24). The children now run with fd 3 closed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

GenHash read an unreadable file's size as -1 and std::vector rejected it with a bare 'cannot create std::vector larger than max_size()': all 120 tasks of a Cover-Branches arm came back ERROR with that line during a memory-exhausted spell of the R22 run. The hash now fails, and the Caller reports the file. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…eally was Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

…mization The --add-invariants study (INV-1 in the experiment log) found that the crab-llvm of the SV-COMP 2019/2020 builds emitted llvm.assume, which neither NonDetPass nor KLEE consumes, and that on a loop program the gain of going through Clam came from its preprocessing, not from the invariants: with none inserted it decided a safe and a buggy variant the plain pipeline left UNKNOWN. - MAP2CHECK_CLAM_PROFILE=default|memory|none: the current Clam flags, the 2018 configuration that did reach KLEE (memory tracked, invariants after loads), or Clam's pipeline with no invariant. - The number of invariants Clam inserted is logged, and a Clam failure falls back to the plain compile with a warning instead of leaving no bitcode. - MAP2CHECK_PREOPT=ssa: the module in SSA form (mem2reg, simplifycfg without sinking) for reachability and assert only -- the memory modes track locals through the allocas mem2reg removes (FALSE-FREE on safe programs), overflow lost detections, and fewer branches mean fewer Cover-Branches cases. Integration 50/50 with it off, 50/50 with it on (section 32 flaky: 3/3 on rerun). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

A major version: AFL++ replaces LibFuzzer (--nondet-generator fuzzer is now afl), and TRUE now requires an exhaustive KLEE exploration while the program's abort() prunes a path -- the same program can get another answer than under 8.x. The changelog lists the whole TACAS line. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

GuilhermeBn198 · 2026-09-30T04:51:42Z

Partial update (R21 CASTLE): with the %s check on, CASTLE gives TP 54, TN 44, FN 12, FP 4 (R14 baseline: TP 53, FN 14, FP 1). All 4 FPs are printf("%s") on memory the runtime does not track (a scanf buffer, argv[0]). This independently confirms that MAP2CHECK_CHECK_CSTRINGS stays off by default, as it is in this branch. The R25 SSA arm is being rerun: the scheduler had collapsed its empty flags column into the env column. Details are in the experiment log.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

GuilhermeBn198 · 2026-09-30T05:06:44Z

Partial update, complete rounds on the 213-task Cover-Error sample:

R23, --seed-exchange on the final build: 154 covered (R19 seeds 151: +5 −2; R19 control 128; v15 on the same sample: 111). Wrong TRUE 0, ERROR 0.
R20, seeds + 3c ranking: 150 (+2 −3). Neutral; the ranking only matters when the fuzzer queue exceeds 64 entries.

On the eca-* and product-lines programs Clam's analysis ran past the whole budget and the run was killed with no verdict (R25: 4 to 7 ERROR per --add-invariants arm). Clam now gets at most 0.2T; past it the existing fallback compiles the program without invariants (Problem08_label51: ERROR -> UNKNOWN at 277 s). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

GuilhermeBn198 · 2026-09-30T12:09:26Z

Overnight results, all complete. Numbers are covered tasks out of 213 for Cover-Error and mean coverage over 120 tasks for Cover-Branches.

Cover-Error (reference R19 control: 128; v15 on the same sample: 111)

arm	covered	vs R19 control
control + KLEE vector replay (R24)	146	+20 −2
seeds, final build (R23)	154	+26 −0
seeds, final build + replay (R24)	155	+27 −0
alternate, final build (R23)	153	+26 −1

Cover-Branches (reference R19 control: 44.7%)

arm	mean coverage
seeds	46.1%
alternate	50.6% (44 better, 5 worse)
control + fuzzer corpus in the suite	49.7%
seeds + fuzzer corpus in the suite	49.4%

--add-invariants / SSA (R25): neither helps in the hybrid.

The Clam arms are worse: more wrong FALSE on MemSafety (4 against 2), and ERROR when Clam ran past the budget. The ERROR is fixed in a1506bc: Clam is now bounded at 0.2T.
Both stay off by default.

Consolidated run (R26) now running on this branch (a1506bc):

Cover-Error: seeds and alternate;
Cover-Branches: seeds and alternate, both with the fuzzer corpus in the suite;
SV-COMP MemSafety, MemCleanup and NoOverflows: control, seeds and alternate;
CASTLE.

It will decide the default hybrid.

GuilhermeBn198 · 2026-09-30T14:14:49Z

R26 (consolidated, this branch at a1506bc), first complete arm: Cover-Error with --seed-exchange: 157/213 covered (73.7%). That is +29 −0 against the R19 control, with 0 wrong TRUE, 0 ERROR and a median of 3 s. On the same sample, v15 covered 111 and had 27 wrong TRUE. The other arms are still running.

GuilhermeBn198 · 2026-09-30T15:37:01Z

R26, Cover-Error with --alternate-engines: 157/213. That ties --seed-exchange (157, +4 −4), and is +30 −1 against the R19 control, with 0 wrong TRUE and 0 ERROR. The median time is 9 s against 3 s for seeds. On Cover-Error the two hybrids tie; Cover-Branches (running) will separate them.

GuilhermeBn198 and others added 30 commits September 28, 2026 21:18

docs(tacasv3a): design spec -- smart seeds plumbing (AFL++ <-> KLEE)

56d11d1

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacasv3a): implementation plan

1f68143

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

feat(tacasv3a): pure seed-store helpers

fb8248a

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R15 -- Cover-Error sample, tacasv2 x v15

3096644

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R15 -- Cover-Branches sample

14c8506

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R18 partial and the 2026-09-29 handoff

3b156aa

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R18 -- the abort fix clears 6 of 8 wrong TRUEs

4206581

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): drop the stale R18 partial from the handoff

6fa1b24

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R16 -- the seed exchange covers 148 vs 129

0e6e015

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

fix(slice): bound the post-slice cleanup like the slicer

be6754d

From the review: the MAP2CHECK_SLICE_CLEANUP opt pipeline ran unbounded, outside every engine's window. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff after 2d, 3b and the review fixes

8111145

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- 3c v1 and R20

9853308

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

GuilhermeBn198 and others added 18 commits September 29, 2026 21:17

docs(tacas): handoff -- strings, fuzzer suite, R21/R22

d89ef22

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R17 complete, and why the alternation lost eca-* tasks

fd83c46

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- R23 and the alternation fix

f1f5237

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- vector replay and R24

54c5d58

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R19 and R21 results

e972dc4

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- night state

4f02611

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- R22 rerun

c312c7a

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- the Crab-LLVM to Clam gap is the next front

e265f5e

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- first probe of the old crab-llvm engine vs Clam

4fabab4

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): INV-1 -- the old crab-llvm vs Clam, and where the gain r…

dff7246

…eally was Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): handoff -- INV-1 and R25

51dc7f0

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): first results of R20, R22, R23 and R24

811fc13

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

GuilhermeBn198 self-assigned this Sep 30, 2026

GuilhermeBn198 requested a review from hbgit September 30, 2026 04:26

GuilhermeBn198 added the enhancement label Sep 30, 2026

docs(tacas): R21 CASTLE, and the scheduler's collapsed tab fields

a17aca5

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

docs(tacas): R20 and R23 seeds complete

c3ebf40

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

GuilhermeBn198 and others added 2 commits September 30, 2026 08:08

docs(tacas): overnight results -- R22, R23, R24, R25

e80a478

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Navigation Menu

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

Map2Check 9.0.0: AFL++ engine, smart seeds, engine alternation, sound TRUE verdicts#73
GuilhermeBn198 wants to merge 57 commits into
developfrom
feat/map2check-9.0

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

GuilhermeBn198 commented Sep 30, 2026

Summary

Why 9.0.0 and not 8.2

Changes

Verdict soundness (these fixes affect every mode)

Engines and seeds

Slicing

Memory safety

Test suites

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

Smaller fixes

Results

v15 baseline (full campaign, before this line)

Cover-Error, 213-task sample

Cover-Branches, 120-task sample

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

Tests

Still running

Before leaving draft

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

GuilhermeBn198 commented Sep 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

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