tacasv2b: --slice for memtrack/memcleanup, and two correctness fixes - #70

Merged

hbgit merged 42 commits into

feat/tacas-slicing-mem

Sep 28, 2026

Commits on Sep 26, 2026

docs(tacasv1): design spec — replace LibFuzzer with AFL++
GuilhermeBn198
committed
b72835b
docs(tacasv1): implementation plan — LibFuzzer to AFL++
GuilhermeBn198
committed
e98397d
feat(tacasv1): install AFL++ 4.40c (PCGUARD) in the dev image
GuilhermeBn198
committed
fdd1fb4
feat(tacasv1): resolve afl-clang-fast/afl-fuzz paths
GuilhermeBn198
committed
0031130
feat(tacasv1): replace FindLibFuzzer with FindAFLPlusPlus
GuilhermeBn198
committed
1455be8
feat(tacasv1): AFL++ persistent nondet generator
GuilhermeBn198
committed
208c6dc
feat(tacasv1): drive AFL++ from the Caller
GuilhermeBn198
committed
d9ab6d0
feat(tacasv1): --nondet-generator afl replaces fuzzer
GuilhermeBn198
committed
c18cd77
chore(tacasv1): rename SKIP_LIB_FUZZER→SKIP_AFL_PLUS_PLUS and update docs
GuilhermeBn198
committed
abae549
fix(tacasv1): make the AFL++ arm build and confirm violations

GuilhermeBn198
and
claude
committed
87f9aaa
fix(tacasv1): address the review of the AFL++ fix commit

GuilhermeBn198
and
claude
committed
d089c90
feat(tacasv1): CmpLog companion binary, and rewind the AFL++ read index

GuilhermeBn198
and
claude
committed
1a49aa5
fix(tacasv1): bound afl-fuzz by timeout alone, not also by -V

GuilhermeBn198
and
claude
committed
a6068c6
fix(verdict): an empty vector is a witness when the program reads no input

GuilhermeBn198
and
claude
committed
6c7b0f2

Commits on Sep 27, 2026

docs(tacasv2a): design spec — slicing for reach/assert that keeps the suite valid

GuilhermeBn198
and
claude
committed
a12ac9b
docs(tacasv2a): implementation plan

GuilhermeBn198
and
claude
committed
83ec67c
feat(tacasv2a): pure slicing helpers -- criteria, stub, statistics

GuilhermeBn198
and
claude
committed
74ecf4a
fix(tacasv2a): slice without cutoff and keep every nondet read

GuilhermeBn198
and
claude
committed
336a26d
feat(tacasv2a): --slice in assert mode

GuilhermeBn198
and
claude
committed
c36a532
docs(tacasv2a): diagnostic sample re-run on the implementation

GuilhermeBn198
and
claude
committed
75bdefd
fix(tacasv2a): take the nondet names from the program as well

GuilhermeBn198
and
claude
committed
ffad3e5
ci: run the PR gates on PRs stacked on tacas/** branches

GuilhermeBn198
and
claude
committed
0b0e855
Revert "ci: run the PR gates on PRs stacked on tacas/** branches"

GuilhermeBn198
and
claude
committed
8eb66b3
test(tacasv1): the evaluation runner's fuzzer arm is GENERATOR=afl

GuilhermeBn198
and
claude
committed
5a4e2fb
Merge branch 'feat/tacas-aflpp' into feat/tacas-slicing
GuilhermeBn198
committed
d182b20
docs(tacas): experiment log -- one entry per mini-round (R1-R6)

GuilhermeBn198
and
claude
committed
2d6bf1a
docs(tacasv2b): design spec — slicing for memtrack/memcleanup after instrumentation

GuilhermeBn198
and
claude
committed
bb0afa3
docs(tacasv2b): implementation plan

GuilhermeBn198
and
claude
committed
e8e244e
feat(tacasv2b): runtime names as slicing criteria

GuilhermeBn198
and
claude
committed
e4ac339
feat(tacasv2b): --slice for memtrack and memcleanup, after instrumentation

GuilhermeBn198
and
claude
committed
8864d7c
test(tacasv2b): SV-COMP MemSafety evaluation harness

GuilhermeBn198
and
claude
committed
9632286
test(tacasv2b): opt-in flags for the CASTLE and Juliet runners

GuilhermeBn198
and
claude
committed
2cddf6b
docs(tacas): R7 -- overflow slicing probe

GuilhermeBn198
and
claude
committed
e29e45d
docs(tacasv2c): study and draft spec -- slicing for overflow

GuilhermeBn198
and
claude
committed
5836a44
docs(tacas): R8-R9 -- memory slicing rounds, wrong TRUE found

GuilhermeBn198
and
claude
committed
aa76cee
fix(tacasv2b): external calls are slicing criteria after instrumentation

GuilhermeBn198
and
claude
committed
96e078f
fix(verdict): KLEE halting on its timer is a timeout, not a proof

GuilhermeBn198
and
claude
committed
30f2215
docs(tacas): R9b-R13 and the two correctness defects they exposed

GuilhermeBn198
and
claude
committed
e6b9296
docs(tacas): sleep-3 is a pre-existing memtrack false positive, not slicing

GuilhermeBn198
and
claude
committed
4d1954f

Commits on Sep 28, 2026

fix(tacasv2b): intrinsics as criteria, refuse a slice without runtime calls

GuilhermeBn198
and
claude
committed
a9bfeff
docs(tacas): R14 -- consolidated control x slice with both fixes

GuilhermeBn198
and
claude
committed
69d8104
docs(tacas): R14b -- memory slice arm on the final build

GuilhermeBn198
and
claude
committed
f92095e