Phase 5: detect stack buffer overflows in binaries through the P-Code
pipeline, value-aware against recovered buffer capacities.
- ir::pcode::PcodeOp gains in_buffer_sizes (parallel to in): per-pointer-arg
recovered stack-buffer capacity, SSA-only (-1 = unknown).
- ghidra_lifter: inject locked prototypes for known copy/input sinks at their
call-target addresses BEFORE the SSA action pipeline, so parameter recovery
attaches the destination pointer; resolveStackBufferBytes traces the
PTRSUB/PTRADD/INT_ADD spacebase+const def chain to a stack address and reads
the recovered local's type size via getScopeLocal()->findOverlap().
- pcode_encoder: recognize copy/input sinks (unbounded: gets/strcpy/strcat/
sprintf/...; bounded: fgets/read/memcpy/strncpy/snprintf/...) and fire
onBufferCopy with the write length when the dst capacity was recovered.
- BinaryBBObserver::onBufferCopy: ugt(size, cap) bounds check -> OOBAccess
finding (binary-buffer-overflow). Unbounded sinks -> Heuristic; bounded with
provable len>cap -> Proved (checkAndEmit gains a confidence parameter).
- router: SSA rewrites CALL targets to synthesized addresses, so resolve callee
names from the raw stream by target address and carry them to the SSA stream
by call-site instruction address (annotateByTarget / annotateBySite).
- r2_backend: extractCallTargetNames maps stub/func addresses -> normalized
callee names; scan_runner activates the lane for oob/oob-access detectors.
Validated on bench/corpora/ctf-challenges: 3 TPs in libbof_overflow
(gets->32B, strcpy->64B, sprintf->128B), genuine TPs in libcmd_injection
(sprintf->256B) and libvuln_demo (strcpy->16B), zero false positives across
the corpus; safe_version and the bounded __strncpy_chk path are not flagged.
Unit tests cover unbounded/bounded/safe/no-size/non-sink cases.
meson test: 74/74. div-by-zero and null-deref P-Code findings unchanged.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds a second hazard to the P-Code encoder. LOAD/STORE now fire onPointerDerefIr
when the dereferenced address provably folds to 0, backed by a small stack-slot
memory model (address-value -> stored value) so a `store 0,[slot]; load r,[slot];
deref r` chain proves r==0. Gated on a provably-zero address (no path forking
yet) → zero-FP: ordinary stack accesses (sp+const) and heap pointers don't fold
to 0. The value map keys on (space,offset) so sub-register reads alias the
full-register write the lifter emits.
Validated end-to-end (ghidra-enabled) on the CTF corpus: libnull_deref.dylib ->
2 null-deref TPs (sym._null_deref_direct AND sym._null_deref_conditional — the
const-0 pointer flows linearly so the conditional case is caught without path
forking), matching the source detector's 2 proved null-derefs; div-by-zero still
2 on libdiv_by_zero; zero null/div FP across the other corpus dylibs. Unit tests
(test_pcode_encoder): store-0->load->deref fires; ordinary stack-slot deref does
not. Full suite 71 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Follow-up to 3fa6d0f56 (dead-encoder removal): test_binary_bb_observer.cpp had
a stale `#include "fold/symbolic/binary_bb_encoder.hpp"` and three TEST_CASEs
exercising the deleted encodeBinaryBBs. The earlier commit's targeted build did
not compile this test, so the break only surfaced in the full suite. Remove the
stale include and the obsolete encodeBinaryBBs cases; the direct
BinaryBBObserver hook tests (null-deref / div-by-zero / overflow) remain and
pass. Full suite 71 Ok / 0 Fail / 1 timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Wires the whole pipeline together: binary bytes -> raw+SSA lift -> P-Code
encoder -> Z3 -> BinaryBBObserver -> merged finding.
- include/fold/binary/pcode_router.{hpp} + src/binary/pcode_router.cpp:
routeFunctionToFindings() lifts a function both ways (liftRaw + liftSSA),
encodes each into a fresh Z3 context/observer, tags findings with the lift
level (evidence.backend = binary-pcode-raw|ssa), and merges + dedups by
(kind, line, detector) — raw wins on collision (more direct hazard evidence).
- meson: gated `fold-ghidra` static lib (ghidra_lifter + pcode_router) linking
fold_core_dep + ghidra_decompiler_dep (first fold_core <-> Ghidra link), and
the `pcode_scan` smoke driver. Defined after fold_core so both deps are in
scope; built only when -Dghidra=enabled.
- pcode_encoder fix: value map now keys on (space, offset) without size and
coerces on read, so a sub-register divisor read (w9, size 4) sees the
full-register zero write (x9, size 8) the lifter emits for `mov w9,#0`
(ARM64 zero-extend). New unit test locks this aliasing.
Validated end-to-end: pcode_scan on arm64 sym._div_by_zero_direct emits exactly
one finding — `[binary-pcode-raw] division by zero proven by Z3` — with the SSA
stream correctly contributing nothing (it folds x/0 -> 0) and the router
merging. Full suite 71 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
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>
`if ((p != 0) && (p->m))` and `if (p == 0 || p->m)` false-positived: the
walker's encodeConditionWithShortCircuit added the LHS to the Z3 solver for
the RHS encode but never updated the env's non-null marks — and the deref
gate checks `env.isDefinitelyNonNull`, not the solver. So only a fragile
same-line text heuristic (sourceLineShortCircuitProvesNonNull) suppressed the
canonical `p && p->m`; parenthesized / `!=0` forms slipped through.
Fix: in the &&/|| short-circuit handling, extract the LHS null-check
(extractNullCheckedVar) and mark its pointer definitely-non-null for the RHS
encode only, then clear it — short-circuit guarantees the LHS holds when the
RHS runs, and clearing prevents the fact leaking into the else-arm (where the
pointer may be null). Path-sensitive, shape-independent, and the bitwise `&`
case stays flagged (both operands really evaluate).
Drift gate: no per-detector change (null-deref 0.792/0.494/0.609 held) — the
fix removes a real FP class without moving the capped-corpus numbers and is
more robust than the text heuristic it supersedes.
Tests: 3 cases in test_null_deref (parenthesized && safe, || safe, bitwise &
still flagged).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Extend ir::Loop classification: a monotone single-induction-variable for-loop
with a symbolic bound (e.g. `for (i=0; i<n; ++i)`) is now Affine (was General).
The walker summarizes Affine loops like Counted ones — bind the induction
variable to a fresh symbolic, assert its start bound plus the loop condition
(encoded to a Z3 bool) as path constraints, walk the body once — exposing
high-index OOB that bounded unroll misses. Findings are over-approximations
(LoopHavoc/heuristic), never proved.
Net effect on the gate: oob recall 0.531 -> 0.559, F1 0.637 -> 0.652 (precision
dips 0.796 -> 0.782) — a contract-sanctioned over-approximation tradeoff.
Also regenerate bench/fp-baseline.json deterministically from a clean run: the
prior committed oob numbers (0.574) were not reproducible (transient warm-state
artifact); fresh runs are now bit-identical, so the gate is reliable.
Tests: test_ir_loop (affine classification), test_loop_summary (symbolic-bound
OOB exposed, not proved). Suite green.
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>
- Verified seedInterproceduralContext() pipeline: SecurityWalker calls it
before TraverseDecl, OOBObserver scans all call sites for ConstantArrayType
- OOB observer consumes param_buffer_sizes_ for ParmVarDecl base variables
- Test added for interprocedural buffer-bound detection
- encoder.cpp: extract VarDecl from ArraySubscriptExpr base when
trackedArrayVar returns null (covers ParmVarDecls like 'output')
- test_oob_access.cpp: test interprocedural buffer propagation
(decode_base64 receiving decoded[256] via pointer parameter)
- Root cause: validate_auth is summarized, preventing inline walk.
Mitigation tracked in docs/internal/interprocedural-notes.md
- SizeInfo struct: buffer_name, capacity, index_expr for OOB findings
- path_trace: vector of branch/call events from SafetyObserver
- counterexample: Z3 model key=value pairs for SAT findings
- variable_name, sink_function: named context for LLM steering
- Serialized in FindingEvidence + SARIF properties
- BinaryBBObserver extends SafetyObserver for binary BB analysis
- Detects null-deref, div-by-zero, int-overflow via Z3 on binary paths
- Wired into BinaryDetectorRunner in scan pipeline
- 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
- Language enum: Unknown, Rust, Cpp, Swift on RustExprNode
- 4 new Clang node kinds: ThrowExpr, CXXConstructExpr, LambdaExpr, StmtExpr
- Updated json_keys namespace with new constants
- 42 roundtrip test assertions pass
- All 3 frontends now share the same IR representation
- 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>
Fold-on-fold pass surfaced 152 dead-statement findings against
fold's own source. Spot-checks revealed every flagged statement
was inside a range-for body. Minimal isolation fixture:
for (const auto& [k, v] : src)
dst[k] = v; // flagged FP: "unreachable from entry"
Plain `for (int x : v)` does NOT trip the bug. The trigger is the
structured binding inside the range-for. Clang's CFG for that
shape leaves the body block without an incoming edge from the
loop's condition check, so the reachability walk in
DeadStatementVisitor marks every body statement unreachable.
Filter: walk up the parent map from the candidate anchor (capped
at 16 hops); if any ancestor is a CXXForRangeStmt, suppress the
finding. Narrow, behaviour-preserving for real dead code,
contained to the same defensive-filter block that already handles
macro-expanded anchors.
Result on fold's own 134-TU compile DB:
before: 152 dead-statement findings
after: 16 (90% reduction)
The remaining 16 likely have other root causes; future audit work.
Added regression test exercising the exact failing fixture; 5/5
test_dead_statement cases pass. Full 44/44 suite still green.
Note: this is itself a fold-on-fold success — the perf-audit's
fold-on-fold pass surfaced a detector bug that had been silently
shipping FPs on every C++ codebase with structured-binding range
loops.
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>
