# Z3-backed complexity analysis feasibility and SAST lane map

> Date: 2026-06-10
> Scope: research/planning pass for adding complexity/resource analysis to Fold's source code-analysis lane while avoiding duplicated scanner and security/SAST work.

## Executive takeaways

1. **Feasible, but not as "ask Z3 for Big-O".** Z3 is useful for proving loop bounds, ranking functions, path feasibility, transition implications, and bounded cost obligations. It should sit under a small resource-bound model, not become the whole complexity analyzer.
2. **Start with security-relevant complexity, not general asymptotic inference.** The most Fold-aligned MVP is a `complexity`/`resource-bound` source detector that reports likely algorithmic-complexity DoS, nested input-dependent loops, unbounded loop/call costs, and complexity regressions under a conservative confidence model.
3. **Reuse the existing security walk.** Fold already has a composite source security walker and observer hook model. Complexity should either be another observer over that walk for statement/event counting or a sibling walk that consumes the same `SourcePathState`, range facts, `Octagon`, and loop facts. Do **not** create another ad hoc AST traversal with its own path/range model.
4. **Refactor detector registration first.** Adding another detector by extending the current boolean-heavy `SourceDetectorPlan` and large `scan_runner.cpp` if-chain will increase duplicated work. Move toward descriptor-driven detector registration before or during the complexity MVP.
5. **Library strategy: borrow ideas, not embed a big tool.** LLVM ScalarEvolution, Infer Cost, KoAT/AProVE/CoFloCo/LoAT, CiaoPP-style Horn/cost relations, CRAB/Clam, and Z3 muZ are the right references. Direct embedding is likely too heavy or mismatched for Fold's Clang-AST lane.

## Literature and tool evidence

| Source/tool | What it does | Lesson for Fold |
|---|---|---|
| **Infer Cost** (`infer --cost`) | Computes asymptotic execution cost and supports complexity diffing/regression reporting. Docs state Java is primary; C/C++ support is limited. It reports degree increases such as `O(n)` -> `O(n^2)` through `reportdiff`. | Fold should separate **cost summaries** from **findings**, and support baseline/regression workflows rather than only per-scan warnings. |
| **LLVM ScalarEvolution (SCEV)** | Models induction variables, add recurrences, exit/backedge counts, and trip counts in LLVM IR. | Best practical library idea for loop trip-count recognition. Since Fold is AST-first, use SCEV as design vocabulary or optional LLVM-lane later, not as the first dependency. |
| **KoAT / AProVE** | Automatic complexity/termination for integer programs, including C integer programs via translation, with upper runtime and size bounds. | Mature approach: translate loops/procedures to integer transition systems, infer size bounds and runtime bounds modularly. Good long-term export/backend model. |
| **CoFloCo / COSTA/PUBS family** | Infers symbolic upper/lower bounds from cost equations independent of source language. Often uses recurrence/cost-relation generation plus solving. | Fold can generate a small internal `CostRelation` IR and only later export to CoFloCo-like formats. |
| **LoAT** | Lower-bound/nontermination analysis over transition systems and linear CHCs; parses CHC SMT-LIB. | Useful for proving worst-case lower-bound hazards (`at least n^2`) and nontermination candidates, but not MVP. |
| **Difference-constraint resource bound analysis** | Literature shows scalable imperative-program bounds by modeling transitions like `x' <= y + c`, and mutually inferring transition and variable bounds. | Fold already has intervals/octagons; first MVP should target difference constraints and affine loop updates. |
| **CHC/Horn resource verification / CiaoPP** | Translates resource usage specifications and inferred resource functions into Horn clauses, often with interval preconditions. Z3's muZ supports CHCs. | Good fit for future `--complexity-chc` experimental backend. Use CHCs for summaries/procedures once intra-procedural loop bounds work. |
| **Ranking-function synthesis** | Linear ranking functions prove termination and bound simple loop progress using SMT obligations. | Fold can use Z3 to prove candidate ranking/variant functions for loops and turn them into bounded trip counts. |
| **pymwp** | Static analyzer for C programs that certifies polynomial growth bounds, compositional and automated, but not a Z3-centric security scanner. | Useful alternate target: classify polynomial vs unknown/exponential-ish growth before trying exact Big-O. |

Key URLs reviewed:

- Infer Cost: https://fbinfer.com/docs/checker-cost/
- Infer repo/manpage: https://github.com/facebook/infer
- LLVM SCEV header/docs: https://github.com/llvm/llvm-project/blob/main/llvm/include/llvm/Analysis/ScalarEvolution.h
- SCEV explainer: https://www.npopov.com/2023/10/03/LLVM-Scalar-evolution.html
- KoAT: https://koat.verify.rwth-aachen.de/
- AProVE KoAT C integer programs: https://aprove.informatik.rwth-aachen.de/interface/v-koat/c
- CoFloCo: https://github.com/aeflores/CoFloCo
- LoAT: https://loat-developers.github.io/LoAT/
- Z3 fixedpoints/muZ: https://microsoft.github.io/z3guide/docs/fixedpoints/intro/
- Difference-constraint resource bounds: https://link.springer.com/article/10.1007/s10817-016-9402-4

## Feasibility assessment

### What Z3 can do well for Fold

- Prove **path feasibility** for loop-entry/exit guards, reusing `SourcePathState`.
- Prove candidate **linear ranking functions** and monotone progress facts.
- Prove/refute simple **trip-count upper bounds** such as `0 <= i < n`, `i += c`, `n - i` decreases.
- Prove **nested-loop multiplication conditions** when inner bounds depend on outer/input variables.
- Check **threshold obligations**: `cost > limit`, `cost grows with tainted input`, `cost_after > cost_before` for baseline comparison.
- Validate detector claims under current path/guarded facts, keeping `unknown` as precision loss.

### What Z3 should not be expected to do alone

- Infer closed-form Big-O for arbitrary C++ control flow, heap containers, iterators, recursion, virtual calls, callbacks, or data-dependent loops.
- Solve nonlinear recurrences robustly under scanner budgets.
- Replace abstract interpretation/polyhedral/SCEV-style loop recognition.
- Produce useful complexity reports without a separate cost model and summary format.

### Practical MVP confidence levels

| Confidence | Meaning for complexity |
|---|---|
| `proved` | Bound/regression/hazard proved under Fold's bounded/inferred model and current path facts. |
| `latent` | Complexity hazard depends on caller/input size precondition or tainted input range not discharged locally. |
| `heuristic` | Structural pattern indicates risk, but loop bound/cost is partial or unsupported. |
| `syntactic` | Pattern only, e.g. nested loops over same container with no bound proof. |

A general complexity detector should use the same bounded-proof humility as security detectors: proved within model, not universal program complexity.

## Fold scan/SAST lane map

### Current source detector selection

`SourceDetectorPlan` is a hand-maintained boolean struct: `include/fold/cli/detector_plan.hpp:14-44`. Profiles and aliases are duplicated manually in `src/cli/detector_plan.cpp:45-77` and `src/cli/detector_plan.cpp:85-117`.

Implication: adding `complexity` by just appending more booleans will work but increase maintenance duplication. A detector descriptor table should own:

```text
name, aliases, category, backend/lane, profile name, default group, factory/run mode,
proof mode, summary-backed?, cross-tu?, report kind
```

### Current source security scan path

- `src/cli/scan_runner.cpp:1990-1992` runs composite security detectors when enabled.
- Fallback individual detector paths duplicate boilerplate for each detector, e.g. div/null/int/oob at `src/cli/scan_runner.cpp:1995-2065`.
- Composite registration happens in `src/cli/scan_runner.cpp:2352-2419`, building observers for div, null, overflow, truncation, sign conversion, OOB, taint, SQL injection, and double-free.
- `src/cli/scan_runner.cpp:2423-2431` multiplexes observers through one `walkContextWithObserver(...)` call.
- Results/profile attribution are split back out at `src/cli/scan_runner.cpp:2436-2455`.

Implication: complexity analysis should not add another full TU walk if it only needs AST/control-flow facts already seen by `SecurityWalker`. Prefer a new observer or a shared `AnalysisWalker` facade.

### Current security walker/state path

- `BatchSafetyObserver` queues hook calls and flushes under cooperative deadline: `src/detect/security_walker.cpp:1225-1269`.
- `SecurityWalker` owns per-function CFG/path traversal and budget checks: `src/detect/security_walker.cpp:1496-1525`.
- Per-function setup creates `SymbolicEnv`, Z3 solver, def-use, initial contracts, and then walks CFG/body: `src/detect/security_walker.cpp:2853-2888`.
- Source path API exists: `include/fold/symbolic/source_path_state.hpp:19-47`.
- Existing loop/invariant hooks are minimal but relevant: `include/fold/symbolic/loop_invariant.hpp:10-23`.
- Existing octagon relational facts can support difference constraints: `include/fold/symbolic/octagon.hpp:15-32`.

Implication: complexity should reuse this function setup and enrich it with a `LoopCostAnalyzer` rather than maintain separate path, contract, debug-assert, and def-use logic.

### Current reporting model

`FindingKind` is security/quality oriented and has no complexity/resource kind today: `include/fold/report/finding.hpp:13-72`. Evidence already has backend/proof/path/precondition fields that complexity can reuse: `include/fold/report/finding.hpp:177-214`.

Recommendation: add one or two finding kinds only after the design is stable:

- `ResourceComplexity` / `AlgorithmicComplexity` for security-relevant input-driven cost hazards.
- Optionally `ComplexityRegression` for baseline diff mode, if reports should show it as a finding rather than a profile artifact.

For an MVP, a JSON sidecar (`complexity.summaries.json`) may be safer than immediately expanding SARIF rules.

## Where we may be doing double work

1. **Detector registration/orchestration duplication.** `SourceDetectorPlan` + profile list + alias enablement + scan-runner if-chains are all manually synchronized. Complexity will worsen this unless registration becomes descriptor-driven.
2. **Multiple path/range models.** SecurityWalker, individual detectors, dead/redundant/uninit walkers, intervals, octagon, guarded facts, and loop invariant hooks overlap. Complexity should consume a single `FunctionAnalysisFacts` product rather than clone range/path logic.
3. **Separate structural detectors vs observer detectors.** Some detectors run on the composite observer path; others run custom AST/CFG traversals. A complexity pass will need both structural loops and symbolic facts. This argues for a shared `SourceAnalysisContext` with path facts, loop facts, def-use, summaries, and budget.
4. **Profiles vs findings.** Fold already has rich solver/profile counters in `SolverStats`; complexity may be both a metric and a finding. Keep summary/profile output separate from security findings until the user asks for gating/security warnings.
5. **Source vs binary risk.** Do not route binary P-Code into source complexity IR. Binary can later have separate heuristic cost summaries, but source complexity should remain Clang/AST/CFG grounded.

## Recommended architecture

### New source-lane concepts

```cpp
struct CostSymbol {
    std::string name;          // e.g. n, size(v), len(s), argc
    ir::AccessPath subject;    // canonical source identity where available
};

struct LoopBound {
    enum class Kind { Constant, Linear, Polynomial, Unknown, UnboundedCandidate };
    Kind kind;
    std::string expression;    // textual symbolic bound: n, n*m, n^2
    z3::expr guard;            // path under which bound applies
    Confidence confidence;
};

struct CostSummary {
    std::string function;
    std::string cost_expr;     // O(1), O(n), O(n*m), unknown
    std::vector<LoopBound> loops;
    EncodingPrecisionContext precision;
};
```

### Analysis pipeline

```text
Clang AST/CFG
  -> existing SecurityWalker/SourcePathState setup
  -> LoopCostCollector: loop headers, guards, induction vars, call costs
  -> Bound inference:
       1. cheap syntactic affine recognizer
       2. interval/octagon/difference-constraint facts
       3. Z3 candidate ranking/bound proof
       4. unknown/timeout precision tag
  -> CostSummary sidecar
  -> optional Finding when security-relevant or regression-threshold crossed
```

### Detector shape

Do **not** put complexity fully inside `SafetyObserver` if it needs loop headers before expression encoding. Instead:

- Add a `SourceAnalysisObserver` or `FunctionAnalysisPass` interface.
- Keep existing `SafetyObserver` as hazard-sink observer.
- Let both share `SourceAnalysisContext`:

```cpp
struct SourceAnalysisContext {
    clang::ASTContext& ast;
    const clang::FunctionDecl* function;
    SymbolicEnv& env;
    SourcePathState& state;
    const ir::DefUseChains& def_use;
    const symbolic::Octagon& octagon;
    SolverBudget budget;
    SolverStats& stats;
};
```

This is the refactor that prevents complexity from redoing contract setup, path pruning, range facts, and solver accounting.

## MVP roadmap

### Phase 0 — design and dedup before features

- Add a detector descriptor table to replace parallel bool/profile/name wiring for source detectors.
- Add `complexity` as a recognized detector flag but keep it hidden/experimental.
- Add `CostSummary` sidecar schema behind `--profile` or `--complexity-output`.

Validation: detector-plan unit tests should prove every descriptor has one profile/rule alias and every CLI alias maps exactly once.

### Phase 1 — cheap loop inventory and cost sidecar

- Build `LoopCostCollector` over Clang AST/CFG.
- Emit per-function loop count, nesting depth, tainted/input-like variables used in loop guards, and unknown-call-in-loop markers.
- No findings yet unless `--complexity-report-heuristic` is set.

Validation fixtures:

- constant loop -> `O(1)` / bounded
- `for i < n` -> linear symbolic bound
- nested `for i<n; for j<n` -> `n^2` structural estimate
- loop over `argv`/`read`/`size()` input -> latent security relevance

### Phase 2 — Z3-proved affine loop bounds

- Recognize induction var init/update/guard.
- Generate candidate bound obligations and prove with Z3 under `SourcePathState` path facts.
- Reuse `Octagon` for difference constraints and `GuardedFactStore` for guarded range facts.

Examples:

- `for (int i = 0; i < n; ++i)` proves `<= max(n, 0)`.
- `while (i < n) { i += 2; }` proves linear with step.
- Early-return guards constrain latent preconditions, e.g. `if (n > 1000) return;` caps cost.

### Phase 3 — security/SAST findings

Add `AlgorithmicComplexity` finding only for actionable hazards:

- user-controlled/input-sized loop cost exceeds configured degree/threshold;
- nested input-dependent loops in request/parse/crypto/string paths;
- unbounded loop with tainted exit condition;
- complexity regression vs baseline.

Keep general summaries as sidecar/profile data, not warnings.

### Phase 4 — interprocedural cost summaries

- Add function `CostSummary` to existing summary store or a sibling cache.
- Compose call cost inside loops.
- Treat unknown calls with a configurable cost policy (`O(1)`, unknown, summary-only).

### Phase 5 — optional external backend experiments

- Export integer transition systems or cost relations for KoAT/CoFloCo/LoAT experiments.
- Try Z3 muZ CHCs for loop/procedure summaries.
- Consider optional LLVM/SCEV lane only if AST approach hits clear precision limits.

## Security/SAST mapping

Complexity analysis should be in the **source SAST lane** initially:

- It is source semantics sensitive: C++ containers, functions, input APIs, contracts.
- It reuses Clang AST/CFG and existing symbolic facts.
- It can produce security findings when attacker-controlled inputs drive high cost.

It should **not** be in binary mode initially:

- Binary loop bounds from P-Code need separate register/memory/CFG recovery.
- Binary cost evidence would be heuristic and should stay separate if added later.

It should **integrate with confirmation later**:

- Fuzz/DAST can measure slow inputs/timeouts, but runtime timing is noisy.
- Confirmation task schema may need `hazard=algorithmic-complexity`, `resource=time|allocations`, `expected_violation=cost threshold exceeded`.

## Recommended next tasks

1. Refactor source detector registration to descriptor-driven metadata.
2. Add `CostSummary` model and sidecar serialization tests.
3. Implement loop inventory collector with no findings.
4. Add affine Z3-bound proof for simple `for`/`while` loops.
5. Add security-relevance classification using taint/input-source and request/parse/string sink context.
6. Add benchmark fixtures and baseline/regression gate.

## Non-goals for the first implementation

- Full arbitrary C++ Big-O inference.
- Whole-program CHC engine.
- Binary P-Code complexity proof.
- Exact container/allocator modeling.
- Replacing existing security detectors with complexity analysis.