Repository navigation

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

Merged

hbgit merged 98 commits into

developfrom

feat/map2check-9.0

Oct 23, 2026

Merged

Map2Check 9.0.0: AFL++ engine, smart seeds, engine alternation, sound TRUE verdicts#73
hbgit merged 98 commits into
developfrom
feat/map2check-9.0

Commits on Sep 28, 2026
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
Commits on Oct 1, 2026
- docs(tacas): R26 complete and the first batches of the 9.0 campaign
  
  GuilhermeBn198
  and
  claude
  committed
  b1f1870
Commits on Oct 2, 2026
- docs(tacas): handoff -- resuming the 9.0 campaign after a power loss
  
  GuilhermeBn198
  and
  claude
  committed
  a65377e
Commits on Oct 3, 2026
- fix(hybrid): link the fuzzer with libm, and kill a KLEE an interrupt cannot stop
  
  GuilhermeBn198
  and
  claude
  committed
  76eedfc
- docs(tacas): the two defects of the 9.0 campaign and the build swap
  
  GuilhermeBn198
  and
  claude
  committed
  43ee04e
- docs(tacas): 9.0 campaign -- Cover-Error, CASTLE and Juliet a/b/d complete
  
  GuilhermeBn198
  and
  claude
  committed
  c8a4f6a
Commits on Oct 4, 2026
- docs(tacas): handoff -- Cover-Branches shard 5 split in four
  
  GuilhermeBn198
  and
  claude
  committed
  60597d7
- docs(backlog): campaign sample vs the official Test-Comp 2026 set; assume-pruned KLEE paths
  
  GuilhermeBn198
  and
  claude
  committed
  b51ee3d
Commits on Oct 5, 2026
- docs(tacas): 9.0 campaign -- Cover-Branches complete
  
  GuilhermeBn198
  and
  claude
  committed
  7c08270
- fix(klee): end an assumption-pruned path with _exit, so KLEE writes its test
  
  GuilhermeBn198
  and
  claude
  committed
  e4e0b74
- fix(suite): assumption-pruned paths give way to deeper ones in a capped suite
  
  GuilhermeBn198
  and
  claude
  committed
  6848d23
Commits on Oct 6, 2026
- docs(tacas): assume-pruned paths fix and its rerun
  
  GuilhermeBn198
  and
  claude
  committed
  53a43e8
- chore: untrack local documents committed by mistake in 53a43e821
  
  GuilhermeBn198
  and
  claude
  committed
  5d57fff
Commits on Oct 7, 2026
Commits on Oct 12, 2026
- fix(testcomp): drop each validator's scratch so a full corpus fits on disk
  
  GuilhermeBn198
  and
  claude
  committed
  4a2dcca
- test(testcomp): let TESTCOV_S=0 skip the internal TestCov
  
  GuilhermeBn198
  and
  claude
  committed
  14766fd
- test(testcomp): official corpora with proportional stratification
  
  GuilhermeBn198
  and
  claude
  committed
  0149e22
- docs(tacas): official Test-Comp environment and the V99 campaign handoff
  
  GuilhermeBn198
  and
  claude
  committed
  3e0dcef
- fix(nondet): model float, longlong, ulonglong, u8/u16/u32 and nondet_memory
  
  GuilhermeBn198
  and
  claude
  committed
  05a1573
- docs(tacas): issue #74 fix, probe and the V99 re-run of the affected categories
  
  GuilhermeBn198
  and
  claude
  committed
  5146272
- docs(tacas): issue #74 re-run report and the KLEE log explosion (#75)
  
  GuilhermeBn198
  and
  claude
  committed
  a2a164a
Commits on Oct 13, 2026
- docs(changelog): unmodeled nondet types (#74) and the official Test-Comp validation
  
  GuilhermeBn198
  and
  claude
  committed
  4855cbb
- fix(runtime): stop the KLEE nondet log from exploding the error path
  
  GuilhermeBn198
  and
  claude
  committed
  8da5794
- feat(klee): MAP2CHECK_KLEE_MAX_MEMORY knob; changelog for #75
  
  GuilhermeBn198
  and
  claude
  committed
  b4bda90
- docs(tacas): issue #75 probes and the 40-task CE sample on install_v99c
  
  GuilhermeBn198
  and
  claude
  committed
  a2fbc56
Commits on Oct 15, 2026
- test(testcomp): loop_reads.c is COVERED since #75
  
  GuilhermeBn198
  and
  claude
  committed
  0b149ce
Commits on Oct 22, 2026
- fix(frontend): read every nondet type of klee_log.csv
  
  Guilherme Bernardo
  and
  claude
  committed
  7db6dd5
- fix(nondet): redirect calls to an existing runtime name instead of renaming
  
  Guilherme Bernardo
  and
  claude
  committed
  9c14229
- fix(counterexample): the C testcase falls back to the violating .ktest
  
  Guilherme Bernardo
  and
  claude
  committed
  c2bcc6c
- fix(memtrack): GNU %m consumes no printf argument
  
  Guilherme Bernardo
  and
  claude
  committed
  223194e
- fix(tests): a tool crash after the fuzzer phase is ERROR
  
  Guilherme Bernardo
  and
  claude
  committed
  b25e6af
- fix(testcomp): make-archive.sh resolves its paths before changing directory
  
  Guilherme Bernardo
  and
  claude
  committed
  deea32a
- docs(testcomp): the test-suite format and how each corpus manifest was built
  
  Guilherme Bernardo
  and
  claude
  committed
  fb2423b

Commits

Commits on Sep 28, 2026

Commits on Sep 29, 2026

Commits on Sep 30, 2026

Commits on Oct 1, 2026

Commits on Oct 2, 2026

Commits on Oct 3, 2026

Commits on Oct 4, 2026

Commits on Oct 5, 2026

Commits on Oct 6, 2026

Commits on Oct 7, 2026

Commits on Oct 12, 2026

Commits on Oct 13, 2026

Commits on Oct 15, 2026

Commits on Oct 22, 2026