# 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.