Problem: SummaryStore keyed summaries by getQualifiedNameAsString (plus
"@file" for internal linkage), which overloads share. When a TU calls a
function whose body lives in another TU, the lookup returns whichever
overload was summarized last. Example: `take(int*, int)` dereferences p,
`take(int*, long)` checks it, and a call `take(q, 1L)` with a null q was
reported as a null-deref because it inherited the other overload's nonnull
precondition. Lookups also used a different spelling (no "@file") than
stores for static functions, so their summaries were never found at call
sites.
Fix: summaryStoreKey()/summaryStoreKeyForCall() return the declaration's
USR (semanticFunctionId: USR, TU-qualified for internal linkage). Every
clang-side store, lookup, dependency edge and staleness check uses it:
summary_encoder, null-deref, div-by-zero, OOB and the summary priming
pipeline, which still selects targets by the call graph's qualified names.
Rust summaries keep their own keys. Now that static callees' summaries
are found, null-deref's summary-precondition path applies the same
DEBUGASSERT and static-parameter-contract filters as its callee-deref
path.
Test: tests/unit/test_summary_key_identity.cpp covers per-overload
summaries, key identity across redeclarations and distinct keys across
namespaces, and the cross-TU overload call. That call reported a false
null-deref before the fix; a control call to the dereferencing overload
still reports one. Tests that hand-built the old keys
(test_symbolic_summary, test_cross_tu_security) now derive them from the
declaration. Full suite: 140/140 (rust_frontend's 500 ms timeout test
flaked once at load average 22 and passed on four reruns).
Problem: a TU the front end could not parse left no trace. ClangTool::run's
status was discarded, TUs with compile errors were analyzed on a partial
AST and counted as done, and the isolated-worker path dropped TUs that
never produced an AST. A scan of only broken files printed no findings and
exited 0, the same as a clean scan. Separately, the scan logger wrote to
stdout, so any warning corrupted a SARIF/JSON report written to stdout.
Fix: every TU now yields an outcome (clean, compile-errors,
analysis-failed); workers carry it on their file_finished record, and the
fan-out parent adds timeout/crash/worker-exit for the TU a worker died on.
tuCoverage() turns the requested file list plus outcomes into a
ScanCoverage (requested TUs with no outcome are frontend-failed). SARIF
gets a run `invocations` entry (executionSuccessful, one
toolExecutionNotification per gap); findings JSON gets an additive
`coverage` object. A scan with any gap, or with nothing analyzed, exits 2
after writing its report. CLI diagnostics now go to stderr, as
docs/internal/cli-philosophy.md principle 12 requires. USAGE.md and
AGENTS.md document the coverage fields and the exit code.
Test: tests/unit/test_scan_coverage.cpp (classification, path spelling,
complete/untracked controls, merge, both writers, and unchanged output
without coverage); test_cli_paths "[coverage]" covers a clean TU (exit 0,
complete) and a TU with a missing include (exit 2, gap in JSON, SARIF on
stdout parseable with executionSuccessful=false). Before: both probe files
exited 0 with no coverage information. Full suite: 139/139.
Problem: docs/research/soundness.md defines `proved` as an exact bounded
model establishing the property, but several detectors assigned Proved
without one: double-free from a heap-model flag, static-ptr-asymmetry from
a cross-function pattern, unused-function and dead-statement from AST
facts, the stdlib copy-overflow check, and the heap use-after-free / OOB
checks from SAT results whose encoding precision was never consulted. A
SAT result over an over-approximated path (an opaque call, an unsupported
node) can be spurious.
Fix: double-free and static-ptr-asymmetry report Heuristic; unused-function
and dead-statement report Syntactic; the stdlib copy check reports
Heuristic. Heap OOB and use-after-free keep Proved only when the path's
SymbolicEnv carries no imprecision tag. So that `malloc(sizeof(T))` paths
stay exact, sizeof/alignof on complete non-VLA types are now encoded as
exact constants (symbolic::typeTraitConstant) instead of an unsupported
node.
Test: tests/unit/test_proved_requires_exact_model.cpp covers each
downgraded detector, a heap UAF on an exact path (stays Proved, control)
and under an opaque call (Heuristic), and typeTraitConstant including the
VLA negative case. Full suite: 138/138.
malloc/free heap modeling (encoder), use-after-free's free/realloc, and
the taint source/sink tables selected a model by the callee's bare
identifier. A project function that merely shares a libc name was
modeled as libc:
namespace mine { void free(void*); }
mine::free(p); ... std::free(p); // double-free "proved", plus
// oob "double free" and a UAF
and `Pool::free(p)` behaved the same way, as did a member function
named `system` as a command-execution sink.
isCLibraryFunction / isCLibraryCallee (encoder_callee_names) accept a
direct callee that is not a class member and is declared at global
scope, in namespace std, or extern "C". The encoder's malloc-family and
free models, use-after-free's free/realloc, and every libc/POSIX taint
entry now require it. Entries that are deliberately method-name
heuristics (get, Query, execute, query, fromJson, readString*, the
request-parameter getters) are marked c_api = false and keep matching
by name as before.
Tests: test_library_callee_identity (namespaced and member `free` are
not double-free/UAF; member `system` is not a sink; libc free twice and
libc system(getenv()) still are), and isCLibraryCallee cases in
test_encoder_callee_names (::free, std::free, mine::free, Pool::free,
a global helper, an indirect call). Full suite 137/137.
The dead-branch, always-condition and unreachable walkers unroll loops
loop_unroll times, following only the path on which the guard holds.
When the guard could also be false (any symbolic bound), that early
exit was dropped, and the loop's assigned variables were havocked only
for loops containing calls. The state after the loop was therefore
"the loop ran exactly loop_unroll times", and conditions on it were
reported as Proved:
int s = 0; for (unsigned i = 0; i < n; ++i) s += 1;
if (s == 0) ... // "dead" proved/exact, "always false" proved
The same held for `s > 100`, while loops, and a `break` out of a
constant loop. On the audit probes this was 7 Proved findings, all
false.
LoopUnrollExits now records whether the unroll saw every way out of
the loop: no iteration could exit early (the guard's false branch was
infeasible), the unroll stopped because the guard became infeasible
rather than because loop_unroll ran out, and the body has no break or
goto that escapes. When any of that fails, the walker havocs the loop's
assigned variables and restores the entry path, as it already did for
opaque loops. A loop the unroll exits exactly (constant bound within
budget) keeps its precise state, so a genuinely dead branch after it
is still Proved.
Loop-bound provenance (--suppress-loop-bound-always-conditions) stays
off by default: it existed to downgrade proofs that leaned on the
unroll bound, and an inexact loop exit now havocs instead of producing
such a proof in the first place.
The duplicated helpers (containsCallExpr, collectAssignedVars,
appendAssignedVars, havocAssignedVars) move from dead_branch.cpp and
always_condition.cpp into detect/loop_havoc so all three walkers share
them; dead_branch.cpp drops under the 800-line soft cap.
Tests: test_loop_exit_soundness covers the symbolic-bound cases for all
three detectors (4 Proved each for dead and always-condition before),
the break escape, the exact-loop negative control, and the extracted
helpers (containsLoopEscape, LoopUnrollExits). Full suite 136/136.
analyzeGadgetEffect symbolically executes one gadget's raw P-Code (reusing the
pcode_encoder register-machine modeling) and reports a context-free transfer
function: each changed register's final source (stack-slot@offset / const /
register / sp-relative), the sp delta, memory writes, and the terminator. Z3 is
used only inside the executor to fold/identify sources — GadgetEffect holds no
z3::expr, so it crosses the fold_core/fold_ghidra boundary cleanly and the
analyzer is unit-testable on synthetic P-Code.
Inputs are seeded as recognizable Z3 consts (in_<off> registers, stk_<k> stack
slots loaded relative to the initial SP); classification simplifies each final
value and matches it back. Register offsets come from a GadgetRegModel resolved
by name at lift time (no hardcoded offsets in the analyzer).
This is the foundation for the Z3 chain planner (3b); not yet wired into chains,
so no finding behavior changes. Design references (not deps): Triton's
per-instruction symbolic state, angrop/ropper gadget controllability.
Unit: test_gadget_semantics — pop rdi;ret → rdi=stack[0], sp_delta 16; mov
rax,0x3b;syscall → rax=const, Syscall; pop rsi/pop rdx → stack[0]/stack[8],
sp_delta 24; mov [rdi],rsi → write-what-where reg→reg; bare ret → sp_delta 8
(22 assertions). meson test 78/78.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Turn a detected overflow + gadget inventory into a candidate ROP chain
scaffold (auto target) attached to the finding.
- rop_chain (pure, fold::binary, unit-tested): synthesizeChain auto-selects a
target — a recovered "win" function (system/execve/puts/printf), else an
execve("/bin/sh") syscall chain assembled from syscall + register-control
gadgets (x0/x1/x2/x8 on AArch64, rdi/rsi/rdx/rax on x86-64). Emits ordered
pad/gadget/value/target steps + explicit caveats (PIE/ASLR base, canary, and
that padding_len is the buffer capacity — the exact saved-return-address
offset is target-frame-dependent and must be verified).
- ghidra_lifter: expose each pointer arg's recovered stack-frame offset
(in_buffer_offsets) alongside its size; signed-offset helper. (Exact RA-slot
recovery is left for future work — the saved return address for these
overflows lives in the caller's frame, which a single-function lift can't see;
honest caveats cover this rather than emit a wrong padding.)
- r2_backend: findStringAddress ("/bin/sh" via r2 /j) to seed execve chains.
- report: ExploitContext gains an optional RopChainInfo (padding_len, target,
steps, caveats); serialized in JSON (write + read round-trip) and SARIF.
- binary_pcode_scan: attachExploitPrimitives now also synthesizes a chain per
buffer-overflow finding from the gadget inventory + recovered capacity.
Validated: baby_bof's decode_base64 overflow carries a chain (target win:printf,
padding 256, steps + caveats). Unit: test_rop_chain (17 assertions). Corpus BOF
counts unchanged; meson test 77/77.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Detect custom (non-libc) routines that fill a caller's fixed-size stack
buffer in an unbounded loop — the bug class fold previously missed because
the destination array decays to a pointer across the call boundary.
- pcode_summary (pure, fold::symbolic, unit-tested): summarizePointerWrites
flags a pointer parameter the function writes via a loop-carried index.
Robust over flattened SSA: base must be a *pure-input* param register (never
reassigned as scratch), index must be non-constant, and the function must
contain a loop (MultiEqual).
- ghidra_lifter: generalize prototype injection — besides known sinks, accept
extra_pointer_protos so a custom write-loop callee gets a pointer prototype
at its call sites, letting the decompiler recover the caller's args and the
destination buffer size (the key enabler).
- binary_pcode_scan: two-pass — pass 1 summarizes every function and collects
write-loop callees + their prototypes; the main pass injects those protos and
reports an overflow at any call passing a recovered fixed-size stack buffer to
a write-loop parameter (Heuristic). Call-site guard: suppress when another arg
is a constant >= the capacity (a size was passed → bounded copy).
- router: detectInterprocBufferWrites emits the finding from the annotated SSA
function (call_target + in_buffer_sizes), with ExploitContext populated.
Validated: dist-baby_bof/index_nocanary.cgi now reports the decode_base64 →
256-byte `decoded` overflow in validate_auth (the SOLVE.md "Fold Gap"); zero
new FP across bench/corpora/ctf-challenges; div/null/sink-BOF unchanged.
Unit: test_pcode_summary (7 assertions). meson test 76/76.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Turn a detected binary stack-overflow into actionable exploit material:
each buffer-overflow finding now carries candidate exploitation primitives
discovered from the same binary.
- rop_gadgets module (fold::binary, r2-gated): classifyGadgets() is a pure,
unit-tested classifier over (addr, opcode-text) gadget pairs into reg-control
/ syscall / stack-pivot / control-flow classes, arch-aware (AArch64 + x86-64);
discoverExploitPrimitives() enumerates via r2 /Rj, keeps top-N per class, and
adds "win" targets (jumpable high-value func/stub addresses — system/execve/
puts/printf/... — resolved by name via extractCallTargetNames).
- r2_backend: extractRopGadgets wraps r2 /Rj (flattened opcode text), bounded by
search.maxhits to keep large static binaries fast (~0.5s on a 900KB binary).
- report: ExploitContext gains a GadgetRef list; BinaryBBObserver::onBufferCopy
fills input_channel (the sink) + buffer_offset (recovered capacity) +
controlled_value; scanBinaryWithPcode attaches the gadget inventory once when
any binary-buffer-overflow finding exists (no cost on clean binaries, graceful
if r2 is absent). Serialized in JSON (write + read round-trip) and SARIF.
Scope: supply classified primitives, not auto-assembled chains; attached only
to buffer-overflow findings (no standalone subcommand). Opt-in security tooling
for authorized CTF/pentest use.
Validated: libbof_overflow BOF findings now carry exploit_context.gadgets
(reg-control x0-setup sequences, stack-pivots, printf win target) +
input_channel/buffer_offset. Unit: test_rop_gadgets (8 cases). meson test 75/75.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
src/symbolic/pcode_encoder.{hpp,cpp}: a register-machine symbolic executor over
fold::ir::pcode (provenance-agnostic — consumes Raw or SSA). Assigns a Z3 BV per
varnode, propagates values through COPY / INT_ADD/SUB/MULT / AND/OR/XOR /
ZEXT/SEXT/SUBPIECE, and fires the existing SafetyObserver::onBinaryArith(Div)
hook for INT_SDIV/UDIV/SREM/UREM so BinaryBBObserver proves the hazard. Lives in
fold_core (no Ghidra dep); it is the real encoder the dead abstract-block path
never was.
MVP precision: the Div hook fires only when the divisor constant-folds to 0
(zero-FP without path forking — a bare symbolic divisor would make SAT(rhs==0)
trivially true and FP on every `a/b`). NEXT: CBRANCH path-forking drops this
gate (catches data-dependent zero divisors); null-deref (LOAD/STORE + stack
memory model, const-0 address gating) and guarded int-overflow follow.
tests/unit/test_pcode_encoder.cpp (no Ghidra/r2): constant-zero divisor and
COPY-chained zero are flagged; non-zero and bare-symbolic divisors are not.
Full suite 71 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Abstract-block mode fired one over-approximate onBinaryArith per block with
fresh unconstrained operands, so it proved nothing for div-by-zero / null-deref
(0 binary findings on libdiv_by_zero / libnull_deref). A full per-instruction
symbolic encoder with path modeling is the eventual fix, but on symbolic args
an unconstrained overflow/aliasing check is trivially SAT and would fire on
every add/sub/mul (the FP blowup) — so this slice lands the sound, zero-FP
subset: constant-zero propagation.
scanInstructionsForConstHazards (pure, unit-tested): a per-function state
machine tracking which registers / stack slots provably hold 0.
mov r,0 | mov r,wzr | str wzr,[slot] | ldr r,[zeroed-slot] -> r/slot is 0
sdiv/udiv d,a,b with b==0 -> div by zero
ldr/str through a zero base register [x0] -> null deref
Tracking resets at every branch / call / ret, so it never reasons across an
unmodeled path — no false positives, at the cost of missing path-dependent
zeros (div_by_zero_variable, null_deref_conditional remain FN: those need
branch modeling, deferred).
Both structural disasm passes (this + UAF) now share one per-function pdfj
sweep via disasmFindingsInSession; const-hazard scanning runs default-on
alongside the import/string detectors and under --detectors
security/div-by-zero/null-deref. Findings carry Heuristic confidence.
Validated on the CTF corpus: +3 TP — div_by_zero_direct, mod_by_zero
(CWE-369), null_deref_direct (CWE-476), all previously FN in binary mode —
with zero new findings across the other 8 dylibs. 6 r2-free unit tests
(test_binary_const_hazards) cover literal-zero divisor, slot-propagated null
deref, non-zero/unknown divisors, branch-reset, and non-zero pointer
negatives. 70 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Binary mode had no UAF/double-free detection. In abstract-block mode the Z3
encoder gives every call argument a fresh, unconstrained constant, so an
aliasing check (freed_ptr == deref_ptr) is trivially SAT for unrelated
pointers — it would fire on every post-free deref. A Z3-proven aliasing UAF
is therefore not viable until per-instruction value flow lands.
Instead detect it structurally over r2 per-instruction disassembly, keyed on
the *stack slot* a heap pointer lives in (r2 names it, e.g. `[ptr]`/`[dest]`)
— a reliable identity within one function, no aliasing needed:
scanInstructionsForUaf (pure, unit-tested): a per-function state machine.
ldr <reg>,[slot] -> reg sources slot
bl free -> slot dangling (double free if already dangling)
bl <other> -> use-after-free if the freed slot's pointer is the arg
str <alloc>,[slot]-> slot revived (free+realloc+free is legitimate)
detectUseAfterFreeFromDisasm / uafFindingsInSession: r2 wrapper, run from
R2Backend::runDetectors on the shared session (no extra `aaa`), default-on
alongside the import/string detectors and under --detectors
security/use-after-free/double-free. Findings carry Heuristic confidence.
Cost is bounded: skip entirely when the binary imports no free/delete (instant
on the common case) and cap the per-function pdfj sweep at 4000 functions.
Validated on bench/corpora/ctf-challenges/libuaf_doublefree.dylib: +3 TP
(double_free_bug CWE-415, use_after_free_bug + use_global_after_free CWE-416 —
all previously FN in binary mode), zero new findings across the other 9 corpus
dylibs. 5 r2-free unit tests (test_binary_uaf) cover double-free, UAF,
clean-free, free+realloc+free, and cross-slot negatives. 69 Ok / 0 Fail /
1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
For a counted loop whose trip count exceeds the unroll bound, bind the
induction variable to its full closed-form range (asserted as a Z3 path
constraint, not just interval metadata) and walk the body once, instead of
unrolling loop_unroll times. This fires each in-body sink against all
iterations at once: it exposes high-index OOB that bounded unroll misses
(oob recall 0.531 -> 0.574, F1 0.637 -> 0.658 on the gate) and collapses
per-iteration queries to one. Findings from the summarized walk are
over-approximations and are tagged LoopHavoc (heuristic) confidence, never
proved. General/while(1) loops keep the bounded-unroll fallback.
Per the precision contract (loop-summarization-research.md), this is a
recall-improving over-approximation that may add bounded, tagged FPs. The
drift gate is updated to match: it now fails on recall- or F1-drop beyond
tolerance (the regressions it was built for) and allows precision dips that
come with recall gains; the committed baseline is regenerated to the B2
numbers.
Tests: test_loop_summary (high-index OOB found + not proved; in-bounds loop
clean). Suite 68/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Foundation for core loop summarization (Workstream B). Adds a clang-free
ir::Loop / InductionVar / LoopKind (Counted | Affine | General) mirroring the
M30 ir::Expr pattern (Symbol-keyed, opaque frontend handle, lowering in
src/symbolic/ir_loop_clang.cpp).
buildLoopFromClang classifies counted `for` loops (constant init/stride/bound,
ascending or descending) into a Counted loop with a known trip count; affine
and unrecognized shapes (while(1) scanners, data-dependent bounds) stay
General and will use the bounded-unroll fallback. The symbolic core will
consume ir::Loop instead of clang::ForStmt so summarization is written once
and reused by the rust/binary frontends.
Tests: test_ir_loop (counted asc/strided/desc trip counts; while(1) and
data-dependent bound -> General). Suite 67/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Enumeration: replace the hand-rolled top-level `tu->decls()` walks (TU
security prefilter + every interprocedural pre-pass/cross-TU primer in
div-by-zero/int-overflow/null-deref/oob) with a shared RAV-based
`fold::detect::forEachFunctionWithBody`, so functions nested in namespaces
and classes are analyzed. Fixes 0-findings on namespaced C++ (dbench CTF).
TU prefilter: extracted to fold/cli/tu_security_prefilter; flags unsigned
-/* wraps so int-overflow candidates in size arithmetic are not skipped.
Timeout robustness: cooperative per-TU walk deadline (WalkOptions) checked
in the walk/unrollLoop/CFG-block checkpoints and the BatchSafetyObserver
flush loop, plus a non-progress unroll fixpoint — slow TUs degrade with
partial findings instead of being SIGALRM-quarantined.
OOB precheck: treat `*(p+i)` and indirect callees as candidates.
null-deref drift fix: remove the unsound `priorFunctionTextProvesNonNull`
source-text heuristic (added in 331a68467) that treated a textual `p!=0`
before a deref as proof of non-null, silently suppressing real null-derefs
(CWE-476 F1 0.485 -> 0.583, recall 0.379 -> 0.517).
Tests: test_function_enumeration, test_tu_security_prefilter, namespaced
cross-TU int-overflow regression. Full suite green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- SafetyObserver subclass for binary basic block analysis
- Detects null-deref, div-by-zero, int-overflow on binary paths
- Wired into scan pipeline via BinaryDetectorRunner
- Binary Z3 findings flow through standard SARIF/JSON output
- Expected: +6 Z3-proved findings on CTF corpus
- SymbolicSummaryCache: per-function BV-64 cache to avoid re-encoding
- Language-agnostic observer overloads for Rust/Swift backends
- Abstract-interpretation pre-pass for Rust integer range filtering
- 3 new unit tests, 63/63 pass
Replaces the per-byte `store(store(...))` chain in modelMemcpyLikeCall
with a single `z3::lambda(i, ite(in_range, src_byte, orig_byte))`.
Drops the `!arg_values[2].is_numeral()` bail so symbolic copy_bytes
now reaches the solver instead of being silently skipped.
Concrete cap (kMaxModeledCopyBytes=4096) is kept to prevent
pathological bit-blast explosion on giant memcpy()s. strcpy is
unchanged -- literal bytes are short + concrete and the lambda
form doesn't help there.
z3 simplifies the lambda away at concrete-index selects so QF_BV
stays viable; no logic-change cascade. Full unit suite stays
57/57 green.
Adds the FixIt collector + per-file unified-diff patch writer
behind a new `fold scan --fix-output <path>` flag. Patch-only --
no in-place rewrites -- so a bad suggestion can't silently
overwrite source.
Consumers (only when the transform is provably sound):
- UninitLocalRead: scalar integer locals only.
`int x;` -> `int x = 0;`. Non-scalar types deferred.
- DeprecatedApi: regex extracts `[Uu]se foo()` from the
deprecation message; silent skip when unparseable rather
than hallucinating a rewrite.
Patches include 3 lines of context above + below each fix so
`git apply --check` accepts them. End-to-end verified against a
synthetic fixture.
Graduates C5's UninitVariablesAnalysis wrapper from
measurement-only into a real detector. Emits a finding per read of
an uninitialised local in the TU's main-file functions.
Scope is calibrated (C5's wrong-hypothesis pivot): clang's analyzer
flags LOCAL read-before-write, NOT parameter nullability. Tests
pin this explicitly (`int p; return p; -> no finding`).
End-to-end on synthetic fixture: 3 expected findings (read of
uninit local, self-init `int x = x`, subsequent use of the
self-init). Parameter reads correctly skipped.
scan_runner.cpp dispatch is unstaged in this commit -- parallel
session has unrelated in-flight edits to that file. The detector
is registered and tested; scan-runner wiring lands in a follow-up.
When a witness recorder is active, run z3::optimize.minimize on the
SAT model before extracting bytes for fuzz seeds. Refines integer
params toward the smallest path-and-hazard-satisfying value, so
seeds emit `arg=1` instead of `arg=0xDEADBEEF`.
Measured on synthetic access_at_offset(p, offset) with the path
`0 < offset && offset < 100`: primary-witness median 33 -> 5
(85% smaller). divide_by_count(p, count) with `count > 0` was
already path-minimal so no change.
Only the primary witness is refined; recordAlternateWitnesses
still uses the original model so the corpus covers the
equivalence class.
Curl-scale validation deferred -- fuzz-prep on full curl crashes
pre-existing (verified Z5-OFF baseline exit 139).
Drop pp.min-alias-size from 10 (default) to 2 so shared subterms
collapse under `let` in serialize(). Measured 39.9% byte reduction
on encoder-shaped n=100 corpus (94.9KB -> 57.0KB). Roundtrip
preserved -- deserialize() parses let-form via z3's SMT-LIB reader.
New AST-only detector that flags call sites whose target decl is
marked deprecated under any of the three idioms:
- `[[deprecated]]` / `[[deprecated("why")]]` (C++14 attribute)
- `__attribute__((deprecated))` (GCC/Clang extension)
- `__attribute__((availability(...,deprecated=N.M)))` (Apple)
Per-call rather than per-decl so a migration that updates call
sites one at a time shows monotone progress. Deprecation reason
(when present) carries through into finding.message. System-header
call sites are skipped so the report stays scoped to the user's
own code.
Curl baseline: 52 real findings, e.g.
ldap.c:269 ldap_url_parse — first deprecated in macOS 10.11
multi-formadd.c:50 curl_formadd — since 7.56.0. Use curl_mime_init()
Refs docs/library-expansion-matrix.md row C7.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds fold::symbolic::parseFunctionContracts(fd, ctx) — reads
RawCommentList for a function decl and returns the param indices
proven non-null by `/*@ requires <param> != null */` clauses.
SecurityWalker calls applyInitialFunctionContracts before walkCFG,
so within-function derefs see the contract via the existing
isDefinitelyNonNull pre-filter.
Grammar v1: bare `<ident> != null|NULL|nullptr`. Multi-line and
multi-clause supported. Unrecognised shapes are silently rejected
so future grammar growth doesn't break existing files.
applyHostToolchain now passes -fparse-all-comments. Without it
clang's lexer drops ordinary block comments before they reach the
AST, so the contract syntax can't ride along on `/*` ... `*/`.
Scope: suppresses within-function derefs on contracted params.
Does NOT suppress call-site findings — that needs CrossTUCache
integration so callee CalleeProperties carry the precondition.
Filed as a follow-up on matrix row C8.
Refs docs/library-expansion-matrix.md row C8.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds fold::symbolic::runUninitAnalysisOnTU(ctx) returning aggregate
counts of functions with local read-before-write uses, derived from
clang's UninitVariablesAnalysis. Scope reminder pinned by the 4
unit tests: this flags LOCAL variable uninit reads, NOT parameter
nullability. The original matrix C5 framing ("null-deref FP triage
pre-pass") was wrong-hypothesis — the analyzer treats parameters as
always-initialised, so it cannot drive null-deref triage.
CFG build options need AddInitializers + setAllAlwaysAdd before the
per-fn AnalysisDeclContext sees decl initializers; without that the
analyzer silently reports zero uses.
Scan-pipeline integration deferred — needs a per-TU accumulator
threaded through the priming consumer.
Refs docs/library-expansion-matrix.md row C5.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
First non-clang frontend for fold. Scans Rust source for the
subset of issues that meaningfully exist there: raw-pointer
dereferences in `unsafe` blocks (Heuristic confidence) and
within-Rust Type-1/2/3 clones via the existing clone detector.
Reuses the M30 frontend-agnostic IR + AnalysisBackend
abstraction unchanged.
Architecture: a separate `tools/fold-rust` cargo binary that the
C++ `RustBackend` shells out to. Two subprocess invocation
modes:
- `extract --unit <file>`: standalone .rs file, no Cargo
context (limited; external-crate imports won't resolve).
- `cargo-check --crate-dir <dir>`: invokes `cargo check` with
RUSTC_WORKSPACE_WRAPPER set to ourselves so cargo supplies
the full --extern/-L/--cfg per-TU. Mirrors the
clippy/miri/kani pattern.
RustBackend::discoverUnits walks up from each `.rs` input to
find the nearest Cargo.toml and collapses sibling files to one
crate unit; orphan files fall back to single-file extract.
scan_router auto-detects --mode=rust when all paths are `.rs`;
mixed Rust + C/C++ warns and defaults to source mode.
Includes:
- tools/fold-rust/: cargo crate pinned to nightly-2026-05-22.
HIR-driven DerefHunter (raw-pointer dereference detection
via typeck `is_raw_ptr()`) and HashWalker (FNV-1a + mix64
port of src/ir/normalize.cpp for FunctionSummary hashes).
- include/fold/ir/expr_json.{hpp,cpp}: RustExprNode +
RustNodeArena + bidirectional JSON wire format for
ir::Expr; round-trip tested across 8 Kinds.
- include/fold/frontend/rust_backend.{hpp,cpp}: AnalysisBackend
impl. posix_spawnp + NDJSON parser. Caches summaries +
findings across extractFunctions calls; polymorphic
runDetectorsOnShard dispatch routes summaries to
detectClones.
- src/cli/{main,scan_router,scan_runner}.cpp: --mode=rust
branch + autoDetectRust(). Mode validation extended to
accept rust.
- docs/rust-frontend.md: scope, wire format, rustc-private
pin + bump procedure, verification snippets.
44/44 unit + integration tests still green. Verified
end-to-end on a 3-function rename-pair fixture: 1 clone
cluster + 1 raw-deref finding through both `extract` and
`cargo-check` paths.
Out of scope (tracked separately): equiv + class-dup
detectors (need encoder frontend-agnostification),
dead-statement (needs Rust CFG), cross-language clones
(needs unified kind-tag taxonomy), Proved/ConcreteWitness
promotion (needs encoder integration), `cargo fuzz`
harnesses.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
When both arms of an if-statement prove the same variable non-null
(via M22 null-check inference or M23 address-of marking), the
summary encoder's `mergeBindings` now intersects the two branches'
nonNullVars sets and marks the survivors in the post-if env.
Mirrors the same logic already present in
security_walker.cpp::walkIf so summary mode and the main walker
stay in parity.
Added tests/unit/test_summary_encoder_phi_nonnull.cpp covering
the rename-pair address-of case. Pre-fix the test FAILs; post-fix
PASSes. 44/44 still green.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
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>
