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

Draft

GuilhermeBn198 wants to merge 60 commits into

feat/map2check-9.0

Commits on Sep 29, 2026

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

GuilhermeBn198
and
claude
committed
56d11d1
docs(tacasv3a): implementation plan

GuilhermeBn198
and
claude
committed
1f68143
feat(tacasv3a): pure seed-store helpers

GuilhermeBn198
and
claude
committed
fb8248a
feat(tacasv3a): a seed store that survives the hybrid's phases

GuilhermeBn198
and
claude
committed
a560d1e
feat(tacasv3a): the fuzzer corpus reaches KLEE as typed seeds

GuilhermeBn198
and
claude
committed
b662546
fix(tacasv3a): bound and phase-gate the replays, clean store, keep proofs

GuilhermeBn198
and
claude
committed
3a89b46
docs(tacas): R15 -- Cover-Error sample, tacasv2 x v15

GuilhermeBn198
and
claude
committed
3096644
docs(tacas): R15 -- Cover-Branches sample

GuilhermeBn198
and
claude
committed
14c8506
fix(verdict): the program's abort() prunes the path, it does not end the search

GuilhermeBn198
and
claude
committed
1eb8a30
docs(tacas): R18 partial and the 2026-09-29 handoff

GuilhermeBn198
and
claude
committed
3b156aa
docs(tacas): R18 -- the abort fix clears 6 of 8 wrong TRUEs

GuilhermeBn198
and
claude
committed
4206581
docs(tacas): drop the stale R18 partial from the handoff

GuilhermeBn198
and
claude
committed
6fa1b24
fix(verdict): KLEE finishing after dropping paths is not a proof

GuilhermeBn198
and
claude
committed
4c16013
docs(tacas): R16 -- the seed exchange covers 148 vs 129

GuilhermeBn198
and
claude
committed
0e6e015
fix(verdict): a path an assumption pruned is not a dropped path

GuilhermeBn198
and
claude
committed
7c6f892
fix(verdict): a KLEE that died, or hit its memory cap, proved nothing

GuilhermeBn198
and
claude
committed
09d8066
feat(slice): slice once per run, and experiment knobs for the slice

GuilhermeBn198
and
claude
committed
93e8de3
fix(slice): bound the post-slice cleanup like the slicer

GuilhermeBn198
and
claude
committed
be6754d

Commits on Sep 30, 2026

perf(slice): scan the IR for names without std::regex

GuilhermeBn198
and
claude
committed
8cdcb07
fix(afl): the fuzzer's input runs out as zeros, not as a replay of itself

GuilhermeBn198
and
claude
committed
c3d2bbe
feat(hybrid): --alternate-engines, turns that end when an engine stagnates

GuilhermeBn198
and
claude
committed
4d1e91e
docs(schedule): phases 2 and 3 as the TACAS line delivered them

GuilhermeBn198
and
claude
committed
2e931ba
fix(hybrid): the review of --alternate-engines

GuilhermeBn198
and
claude
committed
902eaf5
fix(hybrid): the fuzzer gets all of KLEE's vectors, built once, with growing patience

GuilhermeBn198
and
claude
committed
e247b64
fix(afl): one build budget for the three AFL++ binaries

GuilhermeBn198
and
claude
committed
ca996ba
fix(memtrack): check memset/memcpy/memmove under LLVM 16's opaque pointers

GuilhermeBn198
and
claude
committed
956df7b
docs(tacas): handoff after 2d, 3b and the review fixes

GuilhermeBn198
and
claude
committed
8111145
fix(afl): a fuzzer binary that fails to link says so, and why

GuilhermeBn198
and
claude
committed
56e1cb9
feat(seeds): the fuzzer entries that reached new edges go to KLEE first

GuilhermeBn198
and
claude
committed
b664ae6
docs(tacas): handoff -- 3c v1 and R20

GuilhermeBn198
and
claude
committed
9853308
docs(tacas): R16 -- Cover-Branches, the seed exchange 49.7% vs 47.7%

GuilhermeBn198
and
claude
committed
6e7bfdd
docs(tacas): R17 and a partial R19

GuilhermeBn198
and
claude
committed
caf30b6
fix(eval): a crash replayed from the fuzzer is not a tool failure

GuilhermeBn198
and
claude
committed
e482c3a
fix(memtrack): check the strings a %s or puts will read

GuilhermeBn198
and
claude
committed
e3a2500
fix(memtrack): the %s checks behind MAP2CHECK_CHECK_CSTRINGS=1

GuilhermeBn198
and
claude
committed
f18be77
feat(suite): the fuzzer's corpus in the Cover-Branches suite (knob)

GuilhermeBn198
and
claude
committed
d6da7c5
docs(tacas): handoff -- strings, fuzzer suite, R21/R22

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

GuilhermeBn198
and
claude
committed
fd83c46
docs(tacas): handoff -- R23 and the alternation fix

GuilhermeBn198
and
claude
committed
f1f5237
feat(hybrid): run KLEE's vectors on natively, completed with zeros

GuilhermeBn198
and
claude
committed
7636ec5
docs(tacas): handoff -- vector replay and R24

GuilhermeBn198
and
claude
committed
54c5d58
fix(eval): the programs under test must not inherit the manifest

GuilhermeBn198
and
claude
committed
65a9286
docs(tacas): R19 and R21 results

GuilhermeBn198
and
claude
committed
e972dc4
docs(tacas): handoff -- night state

GuilhermeBn198
and
claude
committed
4f02611
fix(frontend): an unreadable input program is an error that says so

GuilhermeBn198
and
claude
committed
49efa33
docs(tacas): handoff -- R22 rerun

GuilhermeBn198
and
claude
committed
c312c7a
docs(tacas): handoff -- the Crab-LLVM to Clam gap is the next front

GuilhermeBn198
and
claude
committed
e265f5e
docs(tacas): handoff -- first probe of the old crab-llvm engine vs Clam

GuilhermeBn198
and
claude
committed
4fabab4
docs(tacas): INV-1 -- the old crab-llvm vs Clam, and where the gain really was

GuilhermeBn198
and
claude
committed
dff7246
feat(invariants): Clam profiles, an invariant count, and SSA pre-optimization

GuilhermeBn198
and
claude
committed
35f32c9
docs(tacas): handoff -- INV-1 and R25

GuilhermeBn198
and
claude
committed
51dc7f0
docs(tacas): first results of R20, R22, R23 and R24

GuilhermeBn198
and
claude
committed
811fc13
chore(release): Map2Check 9.0.0

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

GuilhermeBn198
and
claude
committed
a17aca5
docs(tacas): R20 and R23 seeds complete

GuilhermeBn198
and
claude
committed
c3ebf40
fix(invariants): bound Clam like the slicer

GuilhermeBn198
and
claude
committed
a1506bc
docs(tacas): overnight results -- R22, R23, R24, R25

GuilhermeBn198
and
claude
committed
e80a478
feat(hybrid): the alternation and the fuzzer suite become the 9.0 defaults

GuilhermeBn198
and
claude
committed
e8fe0da
docs: campaign plan on the 2765-task Cover-Branches set, witness study in the backlog

GuilhermeBn198
and
claude
committed
3476ff7
docs(tacas): handoff -- the 9.0 campaign is chained after R26

GuilhermeBn198
and
claude
committed
529d43a