fold/docs/research/z3-complexity-analysis-feasibility-2026-06-10.md

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:

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

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

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:

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.