For every Z3 model fold proved SAT, the concrete byte values it
picked for integer parameters often *are* the magic constants the
path guards on. Promoting them to a libFuzzer dictionary lets the
mutator splice those bytes into nearby inputs that would otherwise
fail the same guard.
Per libFuzzer's docs (https://llvm.org/docs/LibFuzzer.html#dictionaries),
dictionaries are the single largest mutation-quality lever for
formats with magic bytes, fixed headers, or length-prefixed records.
* dict_miner.{hpp,cpp} — mineDictionary(witnesses) -> dict-format
string. One entry per unique non-trivial (Integer|Bool) byte
sequence. Filters trivial values (0/1/all-FF) since S2 boundary
derivatives + libFuzzer's mutator already cover those. Encodes
printable ASCII verbatim, \xNN for non-printable.
* fuzz_prep_runner — emits one .dict per function under
<prep>/dictionaries/<safe>.dict.
* FuzzRunOptions.dict_path + runner.cpp — when set, appends
-dict=<path> to the libFuzzer argv at launch.
* fuzz_run_runner — auto-detects <prep>/dictionaries/<safe>.dict
per function and sets ropts.dict_path. No new CLI flag.
* tests/unit/test_dict_miner.cpp — 10 cases / 12 assertions
covering dedup, trivial filtering, ASCII passthrough, escape
correctness for \" and \\, pointer skip, header counts.
Smoke: leaky(int*, int) with `flag == 0xAB` guard. dict contains
"\xab\x00\x00\x00"; libFuzzer crashes in 0.7s (vs 1s without
dict — gain is modest on a 1-byte guard but the architecture is
in place for the multi-byte magic-value formats where libFuzzer's
own docs cite 5-50x speedups).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
For each integer parameter in a PathWitness, derive boundary
perturbations: 0, 1, -1 (signed only), INT_MAX, INT_MIN (signed).
Classical fuzzing literature shows these catch off-by-one and
overflow bugs that random mutation needs many iterations to reach.
Derivatives share the primary witness's finding_id (so Phase 2's
crash-ingest still correlates by id equality) but are NOT added to
findings.predicted.json — adding them would bloat the prediction
map without changing the correlation key. They land in the same
corpus dir alongside the witness-derived and canonical seeds.
Content-hash filenames in corpus_writer naturally collapse
identical perturbations (e.g. when the primary already has flag=0).
* boundary_seeds.{hpp,cpp} — pure function over PathWitness POD
* fuzz_prep_runner.cpp — emit derivatives after each primary seed
* tests/unit/test_boundary_seeds.cpp — 7 cases / 39 assertions
covering 32-bit signed (5), 32-bit unsigned (3), 8-bit signed,
pointer skip, 2-param independence, bool (2), partial flag.
Smoke: leaky(int*, int) fixture grows from 4 seeds (1 witness +
3 canonical) to 9 seeds (1 witness + 5 boundaries + 3 canonical).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Build the static-analysis-driven fuzzing pipeline alongside the radare2
+ z3 work. fold's symbolic engine already proves sink feasibility; this
adds the path that retains the Z3 model, lowers it to libFuzzer
harnesses + seed corpora, and writes a findings.predicted.json bridge
so a future fold fuzz-run can promote crashes to ConcreteWitness
confidence.
* fold::fuzz value types (PathWitness, ParamWitness) + WitnessRecorder
collector — process-local, lock-free hot-path check
* model_to_bytes — z3::model → little-endian std::byte at source width;
pointer null-vs-nullable disambiguation
* harness_emitter — generates .harness.cc + .schema.json; honors
is_c_linkage via `extern "C"` wrapper for C targets; nested-namespace
emission for C++
* corpus_writer — packs witness bytes per harness layout, FNV-1a hash
for filename, 3 canonical seeds (zeros / 0xFF / single byte)
* param_schema — schemaForFunction + recordSinkWitness +
recordSinkWitnessWithModel; latter looks up each parameter's z3::expr
via env->tryGet() and mines the model for byte payloads
* SafetyObserver: const SymbolicEnv* env added to onPointerDeref,
onDivision, onTruncation, onSignedUnsignedConversion,
onArraySubscript; encoder.cpp passes &env at every call site;
CompositeSafetyObserver in scan_runner fans through
* null_deref, div_by_zero, int_overflow, int_truncation,
sign_conversion now record witnesses with full model bytes;
oob_access records schema-only (sat sites don't capture a model yet)
* fold fuzz-prep subcommand — runs scan in-process (workers can't
ship recorder state), drains the recorder, emits one
{harness,schema,corpus/} bundle per function
Smoke validation: 4 detectors on a 5-line C fixture produce
non-partial witnesses whose bytes are the exact magic values that
trigger each sink (flag=0xAB for null-deref; x=0 for div-by-zero;
a+b that overflows INT_MIN for int-overflow).
Tests: 34 → 37 (add test_model_to_bytes, test_harness_emitter,
test_corpus_writer). All green.
Also folds in a small worker-toolchain optimization that had been
sitting in the working tree: preloadHostToolchainEnv() avoids
repeated popen calls during worker init.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
