clang ships the dataflow framework but NO ready-made pointer-
nullability analyzer. Bundled UncheckedOptionalAccessModel is for
std::optional, not raw pointers. C3 would require a custom
DataflowAnalysis<NullPtrLattice> with transfer functions for every
pointer-touching expression -- L, not M as originally sized.
Original sizing column referenced functions_prechecked_safe but
that counter measures syntactic sink-absence, not nullability.
fold already has multiple condition-based non-null pre-passes
(enclosingThenBranchProvesNonNull, ternaryArmProvesNonNull,
priorFunctionTextProvesNonNull, staticParamContractProvesNonNull,
current_debugassert_nonnull_). Reconsider when a concrete null-
deref FP catalog says clang dataflow would catch what these miss.
Surveyed sites: dead_branch.cpp has 7 dyn_cast uses, all
single-line type-tag dispatch. security_walker.cpp has 48 of the
same shape. ASTMatchers would be MORE verbose for type-tag
dispatch (MatchFinder + bind + callback structure).
They win for pattern-structure queries (regex name + nth arg
shape + ...), which fold's existing detectors don't need.
"Apply selectively, not bulk" was correct; on inspection there's
no concrete bulk-replaceable site that benefits.
z3 4.13+ (fold's pinned version) does not export interpolant
APIs; they were a 4.5-era research feature that was removed.
Z3_get_interpolant / mk_interpolant aren't in the linked headers.
Even if available, existing buildCounterexample already emits
concrete model values like `(e.g., when ptr=0)` which are easier
to read than formula slices for the UX-upgrade claim.
Captures curl scan profile after Z4 (lambda memcpy) lands:
analyze_ms=565020, null-deref wall_ms=344675 / 2,533 queries.
Established convention: each shipped row's Status column links
to its baseline JSON under docs/perf-audit/runs/matrix/.
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.
clang::CrossTranslationUnitContext is a callee-AST importer via
ASTImporter; fold's CrossTuCache is a property-summary cache.
Different paradigms.
Clang CTU exists for analyses that walk callee statements (CSA-
style). fold deliberately avoids that -- summary_encoder serialises
bodies to SMT-LIB strings, detectors consume properties not AST.
Adopting clang CTU would mean redesigning the analysis paradigm,
not extending it.
The matrix's "selective adoption" framing implied a real selective
use case; on inspection there isn't one in fold's design.
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.
dead_statement.cpp:140 already filters macro-ID anchors
(battle-tested in 2026-05-15 curl audit: doh.c 9,060 -> 0
findings). Remaining FPs are CFG-construction artifacts
(range-for desugaring, EH stubs), not preprocessor-induced.
fold has no multi-config scan mode, so "variant -D" was a
speculative failure mode. If a real dead-branch macro FP surfaces,
the fix is a one-line isMacroID() filter on dead_branch.cpp, not
a Preprocessor-hook row.
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.
`inferCountedLoopInvariant` already runs in security_walker, but
its result only feeds spdlog::debug -- `refineRange` and
`recordRangeInOctagon` run unconditionally regardless of invariant
proof.
Extending fixedpoint to mutual recursion before wiring the existing
single-loop invariant into analysis state would add capability
nothing reads. The actual fix is precision-bug-shaped (consume the
result), not library-expansion-shaped.
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).
Z3 ("byte-unroll elimination") was wrong-tracked: encoder doesn't
unroll strcpy/strlen byte-by-byte. Concrete cases use
recordKnownStringDestinationLength; symbolic cases bail. The real
Z3 opportunity is a capability addition, not a perf win.
Z4's matrix insertion site (heap_model.cpp::mergeFrom) was wrong --
that path is pure C++ hashmap union with no z3 queries. Real site
is encoder.cpp:688/715 where memcpy/strcpy unroll per-byte
store-chains capped at kMaxModeledCopyBytes and bail on symbolic
copy_bytes. Array lambdas would replace the loop body with one
expression and handle symbolic length.
HeapRegion is a C++ struct, not a serialised z3 value. Its only
z3-typed fields (base, size) are already z3 BV exprs; freed/in_loop
are plain bools. The struct never crosses TUs, so a z3 tuple sort
saves zero bytes in the cross-TU cache. mergeFrom is hashmap union
with no z3 queries -- "alias-query count" was an imaginary timer.
Real opportunity at this site is path-sensitive freed merge, but
that's a heap-model correctness fix, not a library-expansion row.
Instrumented `instantiateSummaryExpr` + `instantiateSummaryPredicate`
+ `instantiateSummaryPredicateInContext` directly: 3,052 calls /
238 ms on a full curl scan = 0.042% of analyze_ms (570 s).
Original `summary_lookup_ms` hypothesis was wrong-tracked; that
timer measures the hash-map lookup, not the parse_string path Z1
would replace. Quantifier e-matching would also add semantic-drift
risk for no measurable win.
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>
Catalogs 10 Z3 + 10 Clang APIs fold doesn't yet use, each with a
file-cited insertion site, scored payoff, and complexity/risk
columns. Top-3 sequencing nominates Z8 (unsat-core caching) →
C5 (UninitializedValues measurement) → C8 (RawCommentList).
Z8 + C5 ship in this same round; matrix rows updated with
"shipped" status. Perf-audit doc gains a single line pointing at
the matrix from its Phase-2 backlog header — the matrix is the
canonical surface for library-expansion picks now.
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>
Mirrors the unsat_cores_ + unsat_core_path_hash_ + buildAssumptions +
rememberUnsatCore pattern that already shipped in null_deref,
div_by_zero, oob_access, and int_overflow. Prunes redundant path
predicates when consecutive queries on the same path return unsat.
Zero semantic risk; cores only narrow assumption vectors.
taint_track skipped: it does not query the solver.
Refs docs/library-expansion-matrix.md row Z8.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Top-level BUILD.md so users see the dependency list (libz3-dev,
libclang-dev, llvm-dev, etc.) without spelunking docs/. Lists apt
package names for Ubuntu/Debian, dnf names for Fedora/RHEL, and
brew names for macOS — kept in sync with docker/Dockerfile.linux-
validate, which is the executable spec.
- README points at BUILD.md instead of docs/BUILDING.md.
- docs/BUILDING.md trimmed to radare2 vendoring notes only (the
topic that didn't belong in a top-level quick-start).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
setup.sh only checked /opt/homebrew/Cellar/llvm/* and exited with
"No Homebrew LLVM installation found" on any non-macOS host. Add
Linux probing for /usr/lib/llvm-N/bin and llvm-config-N on PATH,
plus a brew --prefix llvm@N fallback for Intel/custom-prefix macOS.
Also:
- Symlink z3.pc from the arch-dependent /usr/lib path into the
meson build dir on Linux (libz3-dev installs there but meson
doesn't search it by default).
- Thread the discovered llvm-config path through to meson via
-Dllvm-config-path so the fold meson option picks up the right
binary instead of guessing.
- Default CC/CXX to the discovered clang when unset; necessary on
apt-installed Linux where bare `clang`/`clang++` may not exist.
- Honor caller-provided LLVM_BIN env override.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
libstdc++'s std::unordered_map / std::vector template instantiations
shape their bodies in ways that trip the unreachable-block detection
(structured-binding desugaring inside range-for body blocks).
libc++ on macOS happens to surface a different AST shape; the filter
keeps the signal cross-platform. Surfaced by the Linux validation
container against the M28 dead-statement regression test.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Same fold-on-fold pass that flagged mixHash duplication also caught
supportsParam (7 copies) and collectConjuncts (4 copies) across the
security detectors + class_dup + equiv + dead_branch.
Move both to a new src/symbolic/z3_helpers.{hpp,cpp} sibling of
the existing z3_model_support / expr_hash / tactics. Detectors
add `using fold::symbolic::supportsParam;` (and collectConjuncts
where used) in their anonymous namespaces so call sites stay
unchanged.
Net: -110 lines across 7 detectors. No behavior change.
44/44 tests still green.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
5 copies of the same FNV-1a-style mix function across
div_by_zero / int_overflow / int_truncation / sign_conversion
(security detectors) + incremental_cache. Each was byte-identical
to fold::mix64 in src/ir/normalize.cpp.
Replace with the existing fold::mix64. Net: -30 lines, no
behavior change.
Surfaced by the fold-on-fold pass (commit 57cf9fd) which flagged
this exact duplication as a clone cluster.
44/44 tests still green.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Captured via bench/perf_audit_run.py --label baseline-post-cache
--runs 5. State of the tree: writtenvars cache (52218478) +
dead-statement range-for filter (8895d50) + all phase-timing
instrumentation from this audit session.
5-run summary:
observed_wall_s 436.6s iqr=17.8s range=427.6..452.1
total_wall_ms 436,568 ± 17,837
scan.serial_dispatch_ms 436,498 ± 17,836 (all of it; --profile forces serial)
detector breakdown (medians, ms):
null-deref wall=270,437 walker=267,126 encode=6,109 hook=4,748 z3_queries=5,531
dead wall=8,526
equiv wall=2,173
clone wall=204
The 4% IQR is tight enough to attribute sub-5% optimizations
reliably; bigger changes need fewer samples. Future perf PRs
should `--diff docs/perf-audit/runs/baseline-post-cache.json`
against this snapshot.
Also archives the earlier 2-run smoke output as
docs/perf-audit/runs/smoke.json.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Document the 152 → 16 reduction from the range-for + structured-
binding filter (commit 8895d50). The remaining 16 findings are
all the same idiom: defensive `return "unknown"` after an
exhaustive enum switch. Lays out three resolution options and
recommends documenting it as a known FP idiom rather than
refactoring fold's own source.
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>
The audit's "measurement discipline" section now names the
concrete tool to use for any sub-15% perf claim — the multi-run
harness committed in the previous commit. Includes the
copy-paste invocation pattern for before/after diff.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds bench/perf_audit_run.py which runs fold N times against a
fixed compile DB and reports median + IQR + min/max for every
metric in --profile JSON (scan-level + per-detector). Output
snapshots land under docs/perf-audit/runs/<label>.json so
before/after diffs are git-tracked.
Motivation: the audit's writtenvars-cache commit (5221847)
showed sub-15% perf moves can't be reliably attributed from a
single run — cross-baseline variance was ~15% just from system
load. Future perf PRs need a statistical baseline. This harness
is the single-machine version of that discipline.
Usage:
bench/perf_audit_run.py --label baseline --runs 5
bench/perf_audit_run.py --label after-fix --runs 5 \\
--diff docs/perf-audit/runs/baseline.json
The --diff mode prints a side-by-side with significance flagged
("yes"/"no") when the delta exceeds 1.5×IQR. That's a rough rule
of thumb; for high-confidence claims, run 10+ samples.
Smoke-tested with --runs 2 (15min wall) on the curl baseline:
2-run IQR = 13s on a ~440s scan (~3% band). 5 runs should
tighten that.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
WriteCollector is a RecursiveASTVisitor over a stmt subtree.
5 call sites in security_walker.cpp consulted it per-statement
during the main walk, the buildNonNullAtBlockEntry pre-pass, and
unrollLoop. Same stmt subtrees re-walked across these sites.
Add cachedCollectWrittenVars(stmt) member function with a
per-SecurityWalker std::unordered_map<const clang::Stmt*, set>
cache. WriteCollector's output is a pure function of the stmt
subtree (no SymbolicEnv state, no ctx mutation), so the cache
is always safe. Map lives one function's analysis (SecurityWalker
is per-function-scoped).
Converted all 5 call sites to the cached wrapper.
Perf: ran the curl baseline after the change (4 workers, 306 TUs,
2339 functions). Single-run wall = 451s, vs. 442–465s spread across
prior single-run baselines. Within run-to-run variance; the audit
doc adds a "measurement discipline" section noting that 5+ runs +
median are needed to validate sub-15% wins. Cache is architecturally
sound regardless — pure memoization with no behavior change.
44/44 tests still green.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Add a ScopedHookTimer RAII helper to SolverStats and instrument the
6 hot per-detector hook bodies (onPointerDeref, onDivision,
onBinaryArith, onTruncation, onSignedUnsignedConversion,
onArraySubscript). Each now records its own hook_ms which surfaces
per-detector in --profile JSON.
For null-deref on the curl baseline:
wall_ms: 344,644
walker_ms: 340,329
encode_ms: 24,156 (7.1% of walker)
hook_ms: 11,860 (3.5% of walker)
state_merge_ms: 75
[unaccounted]: 304,238 (89.4% — walker bookkeeping)
Z3 total: ~33ms across the entire scan.
This is the fourth wrong-hypothesis pivot in this audit:
1. Hash-walk fusion: 0.04% of total ← wrong
2. State-merge optimization: <0.1% ← wrong
3. Encoder optimization: 7.1% ← wrong
4. Hook body optimization: 3.5% ← wrong
The 304s lives in the walker's per-stmt bookkeeping:
- M22-M28 non-null marking (6 separate accumulators)
- collectWrittenVars (per-stmt RecursiveASTVisitor)
- refineRanges / refineOctagon (per-branch)
- buildNonNullAtBlockEntry (per-function pre-pass)
- BranchLivenessBuilder / WriteCollector ancillary passes
Phase-level instrumentation can't subdivide further without
O(stmts) timer overhead. Updated docs/perf-audit.md with
flame-graph-based profiling as the next step + 4 specific
remediation candidates ranked by likely payoff.
44/44 tests still green.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
