tacasv1: replace LibFuzzer with AFL++ 4.40c (persistent mode + CmpLog) - #69
Merged
Merged
Conversation
Found by the final whole-branch review and confirmed by the Task 7 smoke test in the rebuilt dev image. - NonDetGeneratorAFL.c: define the persistent-mode macros exactly as afl-cc 4.40c injects them. The library is compiled to bitcode by plain clang, so without them every build (including KLEE-only and CI) failed, and afl-clang-fast never re-preprocesses the linked -result.bc, so the ##SIG_AFL_PERSISTENT## marker must already be in the bitcode. - Caller: replay crashes from afl-out/default/crashes (the single instance's directory), feeding each over stdin (a standalone persistent binary ignores argv), bounded by timeout, and stop at the first confirmed one so a non-reproducing replay cannot overwrite it. - Caller: set the headless AFL_* flags on the command line rather than relying on the image ENV; record crashing seeds as crashes and stop at the first crash, as the previous fuzzer did. - Caller: use a private afl-in/ unless --seed-exchange, and copy the AFL++ queue back into seeds/ under it (afl-fuzz never writes into -i). - tools.hpp: MAP2CHECK_AFL_CC / MAP2CHECK_AFL_FUZZ overrides; AFL_CC is AFL++'s own variable and reusing it recursed or disabled instrumentation. - Regression test: --nondet-generator afl; stale comments updated. Verified in map2check-dev:aflpp: persistent + shared-memory mode detected, VERIFICATION FAILED on the plan's smoke program and on a non-trivial one, test_testcomp_regressions.sh 19/19, ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
- Cap each crash replay at max(5s, 10% of the budget): a crash that does not reproduce from a fresh process may loop, and must not eat KLEE's share. - Select crash/queue files by type (regular, not README.txt) rather than by AFL++'s "id:" naming, which AFL_SHA1_FILENAMES changes. - Warn when the AFL++ input dir or placeholder seed cannot be prepared. - Document that seeds/ does not yet survive into the next hybrid phase: each Caller recreates the scratch directory. Inherited unchanged from v15; fixing it changes what the hybrid measures, so it belongs to the smart-seeds work. - Regression test: count only the fuzzer's copied discoveries (afl-*), since the placeholder seed made the old file count pass trivially. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19 (4 afl-* discoveries copied), ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The v15 LibFuzzer runs with -use_value_profile=1, which solves comparison guards such as `x == 123456`. AFL++ with PCGUARD alone does not, so the tacasv1 comparison measured an unarmed AFL++ against an armed LibFuzzer. CmpLog (input-to-state) is AFL++'s counterpart. - Caller compiles a third binary, <hash>-cmplog.out, from the same -result.bc with AFL_LLVM_CMPLOG=1 and passes it to afl-fuzz with -c. Optional: if it does not build, the fuzzer runs without it and says so. - NonDetGeneratorAFL.c rewinds its read position for every __AFL_LOOP iteration. The position was function-static and carried over between inputs, so the same input read different values on every persistent run. That nondeterminism defeats CmpLog's byte-to-operand mapping. This reverses the earlier choice to preserve the index for v15 parity; without the reset CmpLog has no effect. Fuzzer-only smoke, 3 runs x 8 seeded bugs, same image: v15 LibFuzzer 17/24 | AFL++ + CmpLog, index kept 4/24 | AFL++ + CmpLog, index rewound 17/24. - Regression test: the KLEE -> fuzzer export check retries when the (now stronger) fuzzer phase solves seed.c first and KLEE never runs. - Spec: addendum §2.1 with the decision and the numbers. Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19 (twice), ctest 9/9. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
afl-fuzz -V compares gettimeofday() readings. A wall clock stepped
backwards -- measured at 1.1s within 20s under WSL2 -- underflows the
elapsed time, and afl-fuzz stops after a few hundred executions
("Time limit was reached", run_time ~2^64). `timeout` uses a relative
timer, and it is how the previous fuzzer was bounded. The budget is
also clamped to at least 1s, since `timeout 0` means no limit.
Spec §2.1 updated with the final fuzzer-only smoke (3 runs x 8 bugs):
v15 LibFuzzer 20/24, AFL++ + CmpLog with the rewound index 17/24,
without it 8/24. Hybrid verdicts identical to v15 on all 11 programs.
Verified in map2check-dev:aflpp: test_testcomp_regressions.sh 19/19,
ctest 9/9.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…input 621db93 downgrades a KLEE violation to UNKNOWN when no input vector can be recovered, to stop FAILED verdicts that nothing reproduces. It asked readViolatingKtest for a non-empty vector, so a program that reads no nondeterministic input -- whose aborting path has a .ktest with zero objects -- was downgraded too, and its suite came out with no test case. That is tests/testcomp/programs/no_input.c, and it has failed the TestCov CI gate on develop since that commit landed (run 33523637266). hasViolatingKtest counts an .abort.err whose .ktest exists, empty or not; the downgrade now uses it. The halted-KLEE case 621db93 guards against still has no .abort.err at all, so it is still downgraded. Verified in both the current CI image (ghcr map2check-dev:latest) and map2check-dev:aflpp: run_testcov_suite.sh 6/6 (no_input.c COVERED), test_cover_branches.sh 5/5, test_benchexec_toolinfo.py 16/16, test_testcomp_regressions.sh 19/19, ctest 9/9 (3 new KtestReader tests). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Sep 27, 2026
GENERATOR=fuzzer still passed --nondet-generator fuzzer, which the CLI no longer accepts. It now names AFL++, and the old value is refused with a pointer to the new one rather than silently measuring nothing. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Sep 28, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This is the first step of the TACAS line (tacasv1). AFL++ 4.40c replaces LibFuzzer completely as Map2Check's fuzzing engine. It runs in persistent mode, with PCGUARD coverage and a CmpLog companion binary, as a single
afl-fuzzinstance. Nothing else in the pipeline changes (KLEE, the hybrid schedule, smart seeding, slicing), so an evaluation against baseline v15 (=develop) measures the fuzzing engine and nothing else.docs/superpowers/specs/2026-09-25-tacasv1-aflpp-migration-design.md. §2 lists the decisions, and the §2.1 addendum covers CmpLog, the index reset and the removal of-V.docs/superpowers/plans/2026-09-25-tacasv1-aflpp-migration.mdWhy AFL++ 4.40c
afl-clang-fastbuilds its passes against the image's LLVM 16, and PCGUARD needs LLVM ≥ 14.-b v4.40c) inDockerfile.dev§7. The image build fails ifafl-showmapdoes not see instrumentation.Why CmpLog (and why the read index is now rewound)
The v15 LibFuzzer runs with
-use_value_profile=1, which solves comparison guards such asx == 123456. With PCGUARD alone, AFL++ cannot do that: in an early smoke run it found 3 of 9 seeded bugs, where LibFuzzer found 7 of 9. Measuring that setup would compare an unarmed AFL++ against an armed LibFuzzer and misattribute the result to the engine. CmpLog (input-to-state, RedQueen) is AFL++'s standard counterpart:<hash>-cmplog.out, from the same-result.bcwithAFL_LLVM_CMPLOG=1, and passes it toafl-fuzzwith-c.CmpLog only worked once the generator's read index was rewound on every
__AFL_LOOPiteration. The index was function-static, so in persistent mode each input was read from wherever the previous one stopped. The same input then produced different values on every run, which breaks CmpLog's byte-to-operand mapping and lowers stability. This reverses the earlier decision to keep the index unchanged for v15 parity: without the reset, CmpLog has no effect (see the table below). The change is three lines and only touches the AFL++ driver.Why
afl-fuzz -Vwas dropped-Vcomparesgettimeofday()readings. If the wall clock steps backwards, the elapsed-time difference underflows and afl-fuzz stops after a few hundred executions ("Time limit was reached",run_time≈ 2^64). We measured a 1.1 s backward step within 20 s under WSL2. The fuzzer is now bounded only bytimeout(a relative timer), the same way LibFuzzer was in v15, and the limit is clamped to at least 1 s becausetimeout 0means no limit.Minimal tests (Docker dev image, v15 and tacasv1 built in the same image)
Eleven small programs with seeded bugs and safe variants covering every property. The budget is
--timeout 30, so the fuzzer slice is 6 s.Fuzzer only (
--nondet-generator fuzzervsafl): 3 runs × 8 buggy programs.All 11 programs, last round (FAILED is expected for the bugs; SUCCEEDED or UNKNOWN for the safe variants):
1000<x<11005000<x<5100x==1234565000<x<51005000<x<5100, index 51..59). CmpLog proposes the exact comparison operands, which are the range bounds and fall just outside the range. Tuning CmpLog (-l) is left to a later round.Other checks:
AFL++ instruments: OKafl-fuzz: "Persistent mode binary detected", "Using SHARED MEMORY FUZZING", "CMPLOG forkserver successfully started"; no "no instrumentation"witness.graphmlis generatedsymex): no regressiontests/integration/test_testcomp_regressions.sh: 19/19 (several runs)ctestwith-DENABLE_TEST=ON: 9/9ghcr.io/hbgit/map2check-dev:latestand in the AFL++ image: 16/16, 5/5, 6/6Known limitations (documented, out of scope for tacasv1)
afl-fuzzinstance, against v15's-jobs=8.-M/-Sis planned as a follow-up.Callerrecreates the scratch directory, andseeds/lives inside it. Fixing that changes what the hybrid measures, so it belongs to the smart-seeds work (tacasv2/v3). The code now says so explicitly, and the regression test counts only the fuzzer's own copied discoveries.core_patternpipe (/wsl-capture-crash) can make a seed that crashes exceed afl-fuzz's 1000 ms dry-run timeout. This happened intermittently, and-tstays at its default so hang handling is unchanged.Commits after the first review round
87f9aaa91: AFL++ macros for the plain-clang build, crash dirafl-out/default, stdin replay that stops at the first confirmed crash, AFL settings passed on the command line, crashing seeds recorded as crashes,afl-in/unless--seed-exchange,MAP2CHECK_AFL_CC/FUZZoverrides.d089c900b: per-replay budget cap, file-type filtering, warnings, honest seed-exchange test.1a49aa585: CmpLog companion binary and per-iteration index reset.a6068c6dc: dropped-Vin favour oftimeoutalone.6c7b0f2d9: fixes a bug already ondevelop, not caused by tacasv1. The TestCov CI gate (no_input.c) has failed on develop since 621db93 (run 33523637266). That commit downgrades a KLEE violation to UNKNOWN when no input vector can be recovered, and it also treated the legitimately empty vector of a program that reads no input as "nothing recovered". The newhasViolatingKtestcounts an aborting path whose.ktestexists, even with zero objects. The halted-KLEE case that 621db93 guards against still has no.abort.err, so it is still downgraded. Three unit tests were added. TestCov passes 6/6 both in the current CI image and in the AFL++ image.🤖 Generated with Claude Code