fold/docs/internal/library-expansion-matrix.md

Z3 + Clang library-expansion opportunity matrix

A scorecard of Z3 and Clang LibTooling features fold has either adopted, rejected, or left as evidence-gated opportunities. Companion to docs/internal/perf-audit.md; inherits the same "measure before optimising" discipline that audit baked in after nine wrong-hypothesis pivots.

This is now primarily a decision log and routing table. Most rows have already been audited; use the Status column to distinguish shipped work, measured false positives, and genuinely unscheduled capability ideas. Active loose ends live in docs/internal/library-expansion-followups.md.

When a row does ship, update its Status with the measurement artifact link (e.g. docs/internal/perf-audit/runs/matrix/<row>-<target>-YYYY-MM-DD.json).

Current usage snapshot

Z3 (z3++.h)

Surface	Files
BV-64 arithmetic + overflow predicates	src/symbolic/encoder.cpp, include/fold/symbolic/encoder.hpp
Boolean ops + ite	src/symbolic/encoder.cpp
Arrays (select/store/const_array) for buffer + heap	src/symbolic/encoder.cpp, include/fold/symbolic/heap_model.hpp
Quantifiers (forall/exists) — loop-invariant inference only	src/symbolic/loop_invariant.cpp
Uninterpreted functions for heap pointer identity	include/fold/symbolic/heap_model.hpp
Solver portfolio (QF_BV + simplify→bit-blast→SAT, par_or)	src/symbolic/tactics.cpp
Assumption-based solver.check(expr_vector)	src/detect/{null_deref,div_by_zero,sign_conversion}.cpp
Unsat-core caching (per-detector, member unsat_cores_ + path-hash gate)	src/detect/{null_deref,div_by_zero,oob_access,int_overflow,sign_conversion,int_truncation}.cpp
Multi-model sampling + model→bytes for fuzz seeds	src/fuzz/model_to_bytes.cpp, src/detect/null_deref.cpp
z3::fixedpoint for synthesised loop invariants	src/symbolic/loop_invariant.cpp
Statistics aggregation (solver.statistics() → SolverStats)	include/fold/symbolic/theory.hpp
Shared shared_ptr<z3::context> for cheap env clones	include/fold/symbolic/encoder.hpp

Clang LibTooling / AST / Analysis

Surface	Files
RecursiveASTVisitor (detectors + frontend)	src/detect/*.cpp, src/frontend/{ast_visitor,clang_backend}.cpp
ParentMapContext	src/detect/{security_walker,null_deref,div_by_zero}.cpp
clang::CFG::buildCFG + CFGBlock	src/ir/cfg_walker.cpp, src/detect/dead_statement.cpp
ASTFrontendAction + ASTConsumer	src/frontend/{clang_backend,ast_visitor}.cpp
tooling::CompilationDatabase + ClangTool	src/cli/scan_runner.cpp, src/frontend/comp_db.cpp
Type queries (getTypeSizeInChars, Linkage)	src/symbolic/encoder_type_queries.cpp, src/detect/oob_access.cpp
SourceManager / SourceLocation (ubiquitous)	every detector
Hand-built call graph (Tarjan SCC) — not clang::CallGraph	src/ir/call_graph.cpp
Hand-built CTU cache + persistence — not clang::CrossTranslationUnitContext	src/detect/{cross_tu_cache,cross_tu_cache_io}.cpp
Custom def-use chains — not clang::dataflow	include/fold/ir/def_use.hpp

Opportunity matrix

Columns:

• Feature — the Z3/Clang API
• Insertion site — file (path verified at write time)
• Affects — detectors / encoder / frontend / infra
• Payoff — precision / perf / capability / UX
• Sizing — qualitative S/M/L + the measurement that would confirm it. The audit's lesson is to ALWAYS name that measurement before writing code.
• Risk — semantic-drift / perf-regression / build-fragility
• Deps — other matrix rows or upstream features needed first
• Status — shipped, unscheduled, or retired with a named false-positive reason plus links to artifacts where available.

Z3 rows

#	Feature	Insertion site	Affects	Payoff	Sizing	Complexity	Risk	Deps	Status
Z1	Quantifiers + patterns (forall :pattern) for function-summary preconditions	src/symbolic/encoder_summary_instantiate.cpp	encoder, all summary-backed detectors	precision	hypothesis-FP — measured curl scan: 3,052 instantiate calls, 238 ms total = 0.042% of analyze_ms (570 s). Not a hot path.	M	semantic-drift (matching heuristics fire differently), z3 quantifier e-matching typically slower than direct substitution	none	unscheduled — measured FP. Z1 (matrix author's original hypothesis: summary_lookup_ms reduction) was based on the wrong timer — summary_lookup_ms measures SummaryStore::lookup() (hash-map), NOT the parse_string+substitute path that Z1 would replace. Instrumented the parse_string path directly on curl 2026-05-25: 0.042 % of total scan time. No room for a measurable win, and quantifier encoding would add semantic-drift risk. Skip.
Z2	Datatypes / tuples for structured pointer metadata (base, size, freed)	include/fold/symbolic/heap_model.hpp	oob-access, null-deref	perf, precision	design-FP — HeapRegion is a C++ struct whose only z3-typed fields (base, size) are already z3 BV exprs; freed/in_loop/alloc_id are C++ scalars. The struct never crosses TUs (cross-TU cache serialises body_smt only), so a z3 tuple sort saves zero bytes. mergeFrom is hashmap union with freed = lhs.freed || rhs.freed — no z3 queries fired, so "alias-query count" is not a real timer.	L	semantic-drift, build-fragility (Z3 datatypes need careful sort setup)	none	unscheduled — design FP. The real opportunity at this site is path-sensitive freed merge (currently a crude bool-or that loses path-sensitivity), which is a heap-model correctness fix, not a library-expansion row. Carved out as future work in docs/internal/perf-audit/optimization-backlog.md rather than wedged into Z2's framing.
Z3	String / sequence theory for strcpy/strlen and taint flow	src/symbolic/encoder.cpp:259, 541, 549, 559	oob-access, taint-track	capability, precision	hypothesis-FP for the "byte-unroll elimination" framing — encoder doesn't unroll strcpy/strlen byte-by-byte; concrete-length cases use recordKnownStringDestinationLength and symbolic cases bail (clear_dst()). Real opportunity is new capability (symbolic-length string reasoning), not eliminating existing unrolls.	L	semantic-drift (Z3 strings theory is heavier than BV)	none	unscheduled — current-state FP. Reframable as pure capability addition (symbolic strlen/strcpy) but payoff is speculative findings on string-content patterns; deferred until there's a concrete missed-finding driving it.
Z4	Array lambda for symbolic-length memcpy/memmove modelling	src/symbolic/encoder.cpp:688 (modelMemcpyLikeCall)	encoder, oob-access	capability, perf	M (shipped) — replaced per-byte store(store(...)) chain with z3::lambda(i, ite(dst_off ≤ i < dst_off + copy_bytes, select(src, ...), select(orig, i))). Dropped the !arg_values[2].is_numeral() bail; symbolic copy_bytes now modelled. Kept kMaxModeledCopyBytes=4096 cap on CONCRETE bounds. z3 simplifies the lambda away at concrete-index selects so QF_BV stays viable — no logic-change cascade. Curl baseline post-Z4: analyze_ms=565020, null-deref wall_ms=344675 with 2,533 queries (see baseline JSON).	M	none observed — full unit suite (57/57) green; downstream detectors handle the lambda transparently	none	shipped — docs/internal/perf-audit/runs/matrix/Z4-curl-2026-05-26.json, tests/unit/test_memcpy_lambda.cpp
Z5	z3::optimize for minimal counterexample selection	src/fuzz/minimal_witness.{hpp,cpp} (new), src/detect/null_deref.cpp:1023	fuzz seed quality	UX	S (shipped) — measured on synthetic access_at_offset(int *p, int offset) { if (0 < offset && offset < 100) return p[offset]; }: primary witness drops to the path minimum (current direct artifact: offset 64 → 1, 98.4% smaller). divide_by_count(int *p, int count) { if (count > 0) return *p / count; } unchanged (path-min was already 1). Buffer-size framing in the original row was wrong — buffer_bytes is a C++ constant in param_schema.cpp:84, not a z3 var. The real measurable is integer-witness magnitude.	S	semantic-drift — only the primary witness is refined; recordAlternateWitnesses keeps the original model so the corpus still covers the equivalence class	none	shipped — opt-in via active recorder presence; no flag needed. Per-finding cost = one z3::optimize.check(). Synthetic primitive artifact: docs/internal/perf-audit/runs/matrix/Z5-synthetic-2026-05-26.json. Curl-scale validation deferred: fuzz-prep on curl crashes with SIGSEGV (pre-existing — verified Z5-OFF baseline also exit 139).
Z6	Fixedpoint engine extension beyond loop invariants (mutual recursion, linear-arithmetic invariants)	src/symbolic/loop_invariant.cpp, src/detect/security_walker.cpp:1604	encoder	capability	infrastructure-FP — inferCountedLoopInvariant already runs; its result is only used for spdlog::debug at security_walker.cpp:1607. refineRange/recordRangeInOctagon run unconditionally and do NOT consume the invariant. Extending fixedpoint to mutual recursion before wiring the existing single-loop result back into analysis state would add capability nothing reads.	L	semantic-drift, perf-regression	Z1 (deferred — measured FP)	unscheduled — infrastructure FP. Reframable as: (a) first wire the existing loop invariant into octagon/range refinement (small fix), then (b) extend to mutual recursion. (a) is a precision-bug fix, not a library-expansion row. (b) without (a) ships dead code.
Z7	Solver push/pop for incremental walkIf paths	src/detect/security_walker.cpp::walkIf (~L1500)	encoder, all walker-driven detectors	perf	S — env_clone_count reduction (already measured as <1µs each; bar is low)	M	semantic-drift (incremental solver state must match cloned-env semantics exactly)	none	unscheduled — env_clone wasn't the bottleneck (0ms / 770K clones)
Z8	Generalise unsat-core caching to remaining detectors	src/detect/sign_conversion.cpp, src/detect/int_truncation.cpp	sign-conversion, int-truncation	perf	S — per-detector wall_ms in --profile	S	none — pattern is proven across four detectors	none	shipped — applied to sign-conversion + int-truncation; taint-track skipped (uses no solver, dataflow only)
Z9	Proof + Craig interpolant generation for finding witnesses	finding emission in detectors; src/witness/graphml.cpp	capability, UX	infrastructure-absent FP — 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 are not in the linked headers. Even if available, existing buildCounterexample already emits concrete model values ((e.g., when ptr=0)) which are easier to read than formula slices.	L	perf-regression (proof generation is expensive)	upstream z3 reintroducing interpolants	unscheduled — infrastructure absent. Reconsider if z3 reintroduces the API; until then concrete-model counterexamples cover the same UX surface.
Z10	let-bindings / macros for serialised-summary compaction	src/symbolic/serialize.cpp:73	encoder, summary-store size	perf	M — measured smaller serialised bodies on encoder-shaped n=100 corpora via z3::set_param("pp.min-alias-size", 2); current direct artifact: 320.4 KB → 113.7 KB (64.5% smaller). Earlier corpus cited 94.9 KB → 57.0 KB (39.9% smaller).	S	none	none	shipped — src/symbolic/serialize.cpp, tests/unit/test_serialize_letbindings.cpp, docs/internal/perf-audit/runs/matrix/Z10-serialize-corpus-2026-05-26.json

Clang rows

#	Feature	Insertion site	Affects	Payoff	Sizing	Complexity	Risk	Deps	Status
C1	AST matchers (clang/ASTMatchers) for targeted patterns	src/detect/dead_branch.cpp, src/detect/security_walker.cpp	detectors	UX (code clarity); some perf	no-forcing-function — surveyed sites: dead_branch has 7 dyn_cast uses, all single-line type-tag dispatch (dyn_cast<CompoundStmt>(stmt)); security_walker has 48 of the same shape. ASTMatchers would be MORE verbose for type-tag dispatch (require MatchFinder + bind + callback). They win only for pattern-structure queries (regex name + nth arg shape + …), which the existing detectors don't need.	S–M per call site	none for isolated replacements	none	unscheduled — no measurable benefit-bearing site. Reconsider when a concrete pattern-structure detector lands that would actually benefit (e.g. a "specific calling-convention misuse" check that's awkward to write with dyn_cast).
C2	clang::CallGraph for built-in call resolution	src/cli/scan_runner.cpp → ir::ProjectCallGraph	infra	perf, capability (constructor/new/default-init/block edges)	M — virtual-call resolution count; CTU cache hit-rate stability	M	semantic-drift (clang's call graph has different node identity than ir::ProjectCallGraph); breaks cross-TU cache invariants	careful migration plan	shipped selective adapter — fold's ProjectCallGraph remains canonical; Clang TU-local edges are merged additively and persisted through the existing cross-TU cache contribution format
C3	clang::dataflow::Analysis framework for pre-pass typestate	src/symbolic/encoder.cpp (env initialisation)	encoder, null-deref	precision, perf	L (not M as originally sized) — clang ships the framework but NO ready-made pointer-nullability analyzer. Bundled UncheckedOptionalAccessModel is for std::optional, not raw pointers. C3 would require writing a custom DataflowAnalysis<NullPtrLattice> with transfer functions for every pointer-touching expression — comparable cost to a new detector. Original "M — functions_prechecked_safe" sizing was wrong-tracked: that counter measures syntactic sink-absence (precheckSecuritySinks), not nullability.	L	wrong lattice = silent missed bugs (false-negatives). additive-pre-pass framing only holds if the lattice is genuinely sound.	none	unscheduled — sized wrong + no forcing function. 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.
C4	clang::consumed::ConsumedAnalysis for RAII	src/detect/security_walker.cpp	use-after-free path (future detector)	capability	wrong-tool-FP — ConsumedAnalysis is intra-procedural typestate for linear types with states (Unconsumed/Consumed/Unknown). It only activates on classes marked [[clang::consumable]] + member functions marked [[clang::callable_when(state)]] + [[clang::return_typestate(state)]]. Real-world C code (curl, yams, kernel-style) has none of these attributes; without auto-injection the analysis is silent.	M	none — but no useful signal on unannotated code	source annotations or attribute auto-injection	unscheduled — wrong-tool FP. A native UAF detector remains a real opportunity, but it's a CFG-walker shape (track malloc/free on tracked pointers + flag derefs after free), not ConsumedAnalysis. Carved out as a future detector row rather than wedged into C4's framing.
C5	UninitializedValues analyzer → uninit-local-read detector	src/detect/uninit_local_read.{hpp,cpp} (new), src/symbolic/uninit_pre_pass.{hpp,cpp} (measurement)	new detector --detectors uninit-local-read	capability	S (shipped) — measurement wrapper + 5 unit tests on the detector entry point + end-to-end smoke on a synthetic fixture (int x; int y = x; → finding @ line 3; int p; int y = p; → no finding). Original "null-deref FP triage" framing was wrong-hypothesis (clang's analyzer flags LOCAL read-before-write, NOT parameter nullability) — C5 now ships as the local-uninit detector that calibration revealed. Curl baseline: 0 SARIF findings after report filtering, 68 ms detector wall.	S	none	none	shipped — library function + detector + registry + scan-runner dispatch + SARIF rule id; baseline docs/internal/perf-audit/runs/matrix/C5-curl-2026-05-26.json
C6	clang::Preprocessor macro-expansion hook	src/frontend/clang_backend.cpp	dead-statement, dead-branch	precision	current-state-FP — dead_statement.cpp:140 already filters anchor->getBeginLoc().isMacroID() (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" is not a live failure mode. dead-branch lacks the macro-ID filter but no documented FP drives the need.	M	build-fragility (Preprocessor hooks fire during parse; lifetime is delicate)	none	unscheduled — current-state FP. If a real dead-branch FP under macros surfaces, the fix is one-line (add the same isMacroID() filter to dead_branch.cpp), not a Preprocessor-hook row.
C7	AvailabilityAttr / deprecation detection	src/detect/deprecated_api.{hpp,cpp} (new)	new detector (--detectors deprecated-api)	UX, capability	S (shipped) — 7 unit tests pin [[deprecated]], __attribute__((deprecated)), message-payload propagation, decl-only-not-flagged, multi-callsite, method-call. Curl baseline: 52 real findings with replacement guidance carried through ("Use curl_mime_init()", "first deprecated in macOS 10.11 — use OpenDirectory Framework"). Per-call rather than per-decl so refactors show monotone progress.	S	none	none	shipped — baseline docs/internal/perf-audit/runs/matrix/C7-curl-2026-05-26.json
C8	RawCommentList for /*@ requires */ user contracts	src/symbolic/function_contracts.{hpp,cpp} (new), src/detect/security_walker.cpp (apply hook), src/frontend/comp_db.cpp (-fparse-all-comments)	encoder, all detectors that consult isDefinitelyNonNull	capability	S (shipped) — 8 unit tests pin: != null / != NULL / != nullptr shapes, multi-line, unknown-param reject, twin-flag negative. v1 grammar = /*@ requires <param> != <null> */. Suppresses within-function derefs on contracted params; synthetic twin baseline dropped null-deref findings 6 → 1 (5 contracted derefs suppressed; unannotated residual still fires). Does not suppress call-site findings (callers still need to prove non-null at the call). The call-site suppression is the "callee-standalone-context" gap from docs/internal/perf-audit/fold-on-fold.md, separate from C8.	S	none	none — but requires -fparse-all-comments (added to applyHostToolchain)	shipped (within-function suppression) — baseline docs/internal/perf-audit/runs/matrix/C8-contracts-synthetic-2026-05-26.json
C9	FixIts for fold --fix-output (unified-diff patch)	include/fold/report/{fix_it,patch_writer}.hpp (new), src/report/patch_writer.cpp (new), src/detect/{uninit_local_read,deprecated_api}.cpp (consumers), src/cli/main.cpp (--fix-output flag)	UX (new capability — autopatch)	S (shipped) — 4 patch_writer tests + 4 FixIt-emission tests + end-to-end smoke on synthetic fixture (int x; → int x = 0; patch applies cleanly with git apply --check). Consumers: UninitLocalRead (scalar integer locals only — int x; → int x = 0;; non-scalar deferred); DeprecatedApi (regex on the message for [Uu]se foo() pattern; emits no FixIt when no replacement is parseable, rather than hallucinating). Patch writer now emits one coherent hunk per file so multiple same-file FixIts apply cleanly. Patch-only mode — no in-place rewrites — keeps the safety blast radius small.	M	semantic-drift mitigated by emitting only when transform is provably sound and never auto-applying	C8 contracts (deferred — could prove additional patch safety later)	shipped — unified-diff output via fold scan --fix-output <path>; baseline docs/internal/perf-audit/runs/matrix/C9-synthetic-2026-05-26.json. Multi-line replacements + non-scalar uninit + non-call-form deprecation replacements remain unscheduled.
C10	clang::CrossTranslationUnitContext	src/detect/cross_tu_cache.cpp	infra	perf, precision	architectural-mismatch FP — clang CTU is an on-demand callee-AST importer (ASTImporter); fold's CrossTuCache is a property-summary cache (CalleeProperties { derefed_params, divisor_params, ... }). Different paradigms: clang CTU exists for analyses that walk callee STATEMENTS; 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.	L	semantic-drift (would invalidate cross_tu_cache.v2 parity)	full analysis-paradigm redesign	unscheduled — architectural-mismatch FP. The matrix's original "selective adoption" framing implied a real selective use case; on inspection there isn't one. fold's summary-property approach is architecturally superior for its design (smaller serialised footprint, O(1) lookup, no per-call AST parse).

How to use this matrix now

The first sweep has already retired the original top picks (Z8, C5, C8) and several adjacent rows. Treat this file as a compact map of what was learned, not as a fresh backlog ordered by the old hypotheses.

Status meanings

• shipped — implementation exists; prefer follow-up measurement or polish, not another implementation pass.
• unscheduled — measured/design/current-state/etc. FP — the row's original framing was audited and should not be re-opened without new evidence.
• unscheduled — no forcing function / capability gap — still possible, but needs a concrete missed finding, benchmark, or user-facing workflow before it is worth adding complexity.

Active next work

Do not choose from the old Z/C row order by default. The actionable queue is in docs/internal/library-expansion-followups.md:

1. Commit/verify scan-runner wiring for C2 + C5 if those local hunks are still present.
2. Design a native use-after-free detector (the real capability gap found while retiring C4's ConsumedAnalysis framing).
3. Capture missing per-row baselines for shipped rows that predate the per-row artifact convention.

Re-opening a retired row

Only re-open a retired row when the session starts with at least one of:

• a concrete false-positive / false-negative example the row would address;
• a profile artifact showing the cited path is now hot;
• an upstream/library change that removes the reason the row was retired;
• a user-facing workflow that justifies a capability row despite no perf win.

If none of those exists, create a follow-up entry instead of expanding the matrix row. This keeps the matrix from accumulating speculative implementation plans that have already failed the audit discipline.

When to pick differently

The follow-up queue assumes you want the least surprising path to completion. If the next session's goal is instead:

• New source detector capability → start from the native UAF follow-up, not C4's ConsumedAnalysis wording.
• Fuzz-seed quality → Z5 has a direct synthetic primitive baseline; require a fresh fuzz-prep baseline before extending it into curl-scale workflow changes.
• Documentation-quality findings → revisit Z9 only if the pinned Z3 exposes proof/interpolant APIs again, or scope a non-interpolant explanation feature.
• OSS readability → wait for a detector whose pattern structure is actually awkward with dyn_cast before using C1 / AST matchers.

Out of scope

• Implementing any of the 20 rows. Each row is a separate session.
• Bulk replacement of RecursiveASTVisitor with AST matchers (C1 applies to specific isolated sites).
• Wholesale swap of ir::ProjectCallGraph for clang::CallGraph (C2 shipped only as selective additive adoption; clang's graph lacks the cross-TU provenance the persistence layer depends on).
• Z3 features requiring Z3 > 4.13.4 (the Conan pin). Bumping Z3 is its own decision.