fold/docs/positioning.md

Positioning

Where fold sits relative to existing C/C++ static analyzers and verifiers. This is a sales-free, scope-honest comparison written for engineers evaluating tools, not procurement decks.

One-line summary

fold is a bounded symbolic SAST for C/C++ that ships every flagged sink with a Z3-produced witness, then optionally runs that witness through libFuzzer + ASan to promote findings from "the solver says SAT" to "we observed the crash."

Solver-backed analyzers (for example the Clang Static Analyzer's optional Z3 refutation) use SMT to prune infeasible paths, but their reports stop at a static verdict. Most fuzzers don't know what they're aiming at. fold links the two so the report says which findings are confirmed observable failures, not just satisfiable path predicates.

Confidence tiers fold reports

Findings are not all equal. fold reports five confidence tiers:

Tier	Source	Example
Syntactic	AST pattern match, no solver	"function name matches strcpy"
Heuristic	Solver gave up or path was over-approximated	"interval analysis can't bound len"
Latent	Proved in the callee, modulo a caller obligation not discharged	"p is dereferenced; no caller shown to pass null"
Proved	Z3 returned SAT on (path ∧ hazard) over an exact bounded model (no over-approximated operation on the path; see docs/research/soundness.md); model is the witness	"Z3 finds idx=42, len=10 violating bounds"
ConcreteWitness	Z3 model was packaged as a seed and ASan observed the crash	"libFuzzer crashed on seed_8f3c.bin"

The ordering is explicit in include/fold/report/finding.hpp::confidenceRank() so downstream consumers (CI gates, SARIF parsers, IDE plugins) can sort or filter on it without inventing their own heuristic.

What fold reliably catches vs what's noise

On tight, well-typed codebases (modern C++, careful Rust+FFI), most security findings are false positives. The bounded symbolic model can't carry domain invariants — facts like "this size_t was length-prefixed in our wire format and is always < 1MB" that the codebase enforces elsewhere. Without those invariants, fold has to assume parameters range over their full type domain, which produces many "could overflow / could deref null" findings that are actually unreachable.

The reliable signal is the CLI-input → arithmetic-hole pattern. Where untrusted input (argv, stdin, network bytes, command-line flags) flows into integer math or pointer arithmetic without a bounds check, fold catches it. The fix shape is usually a one-line defensive check at the boundary.

Practical triage heuristic

When working through a fold report:

1. Filter by input reachability. A finding on a function whose only callers are internal helpers in a well-tested module is almost certainly a domain-invariant FP. A finding on a function reachable from an argv parser, an HTTP request handler, or a file-format reader is worth investigating.
2. Trust ConcreteWitness unconditionally. Those are observed crashes under ASan.
3. Triage Proved against the input-reachability filter. The solver found a satisfying assignment; whether it's reachable in practice depends on whether anything in the codebase enforces a tighter constraint than the type system expresses.
4. Heavily filter Heuristic. Over-approximate by design; treat as "worth a quick eyeball" rather than "real bug."

The taint-track detector exists precisely to make the input- reachability check mechanical; running with --detectors security includes it.

Comparison with peer tools

The right comparison set depends on what you're optimizing for. fold's peers fall into four camps.

Linters (clang-tidy, cppcheck, Semgrep)

Pattern matchers over the AST or text. Sub-second per TU. High false- positive rates on anything path-sensitive (null derefs behind guards, overflows that only happen on impossible inputs, dead code after non-obvious assumes). No notion of a counterexample — the finding is the pattern match.

fold differs by: Z3-backed path conditions on the security detectors. A null-deref finding from fold comes with the integer parameter values that exhibit it, not "the AST node has shape X."

When linters are the right tool: style enforcement, name conventions, missing-cast detection, language-spec violations that have nothing to do with runtime values.

Commercial path-sensitive SAST (Coverity, CodeSonar, Veracode)

Mature, well-tuned, expensive. Most use proprietary abstract interpretation domains plus heuristic refinement; some bolt on limited symbolic execution for top-confidence findings. Closed source, closed methodology, opaque false-positive rates.

fold differs by: open source (GPL-3.0 when stable), open methodology (docs/research/soundness.md), and a closed loop with libFuzzer in the same report. fold is also substantially less mature on the heuristic-refinement side — Coverity has had two decades of FP-tuning effort that fold has not.

When commercial SAST is the right tool: large enterprise codebases where the procurement, support, and triage tooling matters more than tool ownership, and where Coverity-grade FP tuning is worth the license cost.

Datalog query engines (CodeQL, Joern)

CodeQL (GitHub, commercial-licensed for non-OSS use) and Joern (open source) phrase analyses as Datalog queries over a code property graph (CPG: AST + CFG + PDG joined). Strong on "interprocedural data flow from source X to sink Y" — taint tracking is a one-line query. Weak on arithmetic reasoning: a CodeQL query can describe "tainted integer flows into array index" but not "the integer is bounded such that the index is in-range."

fold differs by: SMT theory. fold's oob-access detector proves the index is out of bounds via Z3 bitvector arithmetic (QF_BV); a CodeQL query of the same shape can only confirm a flow exists.

When Datalog is the right tool: interprocedural taint and reachability queries on a large codebase where you want to write declarative custom rules, or when GitHub Code Scanning is already your CI surface.

Bounded model checkers (CBMC, ESBMC)

Unroll loops to a configurable depth, encode the bounded program as a SAT/SMT formula (CBMC's default back end is a SAT solver) and ask whether any assertion can fail. Sound for the unrolling depth chosen; report concrete counterexamples; usable as software-verification competitors (SV-COMP). Whole-program BMC cost grows with program size and unwinding depth.

fold differs by: scope and product shape. CBMC verifies one property of one bounded program; fold runs per-sink, mostly intraprocedural queries with a small loop unroll (5 by default), trading verification rigor for breadth. They are complementary: a fold finding worth deep verification can be re-checked under CBMC.

When BMC is the right tool: verifying a specific module or safety-critical kernel routine to a precise unrolling depth, where exhaustive coverage of the bounded program matters more than codebase-wide scan throughput.

Symbolic execution engines (KLEE, SymCC, S2E)

KLEE interprets LLVM IR symbolically with its own constraint solver layer; produces high-quality test inputs for the paths it covers. SymCC instruments at compile time and runs the binary natively with a parallel symbolic shadow store. S2E extends KLEE with whole-system (QEMU) state.

These are full symbolic execution: they explore paths at runtime and produce inputs for every covered path. They do not "scan a codebase for vulnerabilities"; they explore a chosen entry point and report what they found.

fold differs by: direction. fold's scan is bottom-up — every suspicious sink in every function is asked "is this SAT?" without needing an entry point. Symbolic execution is top-down — given an entry point, what paths are reachable?

The two compose well, and fold's Phase 3 (scoped in docs/internal/m31-phase3-concolic.md) brings SymCC-style concolic exploration into fold's loop precisely because the bottom-up scan can miss reachability that top-down execution surfaces.

When pure symbolic execution is the right tool: test generation against a defined harness or entry point, especially for protocol parsers and other constrained-input APIs.

What fold is and is not

Is

• A scan-time tool. Runs per TU, emits SARIF, versioned findings JSON, or Markdown.
• Z3-backed on the security detectors (null-deref, div-by-zero, int-overflow, oob-access, int-truncation, sign-conversion, taint-track).
• Frontend-agnostic at the IR layer (M30 refactor): a future Rust or Swift frontend can produce fold::ir::Expr nodes without touching clang.
• A fuzzer driver as of M31: fold fuzz prep emits libFuzzer harnesses + Z3-derived seed corpora; fold fuzz run ingests crashes and promotes findings to ConcreteWitness.
• Open methodology: every confidence claim is backed by code in src/symbolic/ and src/detect/; correctness reasoning is in docs/research/soundness.md.

Is

• A Rust scanner for the unsafe layer. fold scan <file>.rs auto-dispatches to the Rust frontend (see docs/internal/rust-frontend.md). Detects raw-pointer dereferences in unsafe blocks and within-Rust clone clusters. Not a substitute for clippy / rust-analyzer on safe code — fold's value-add is exactly the layer where the borrow checker is off. Requires a pinned nightly toolchain + rustc-dev component; one-time install via rustup.

Is not

• A formal verifier. fold's encoder is over-approximate in documented ways (docs/research/soundness.md): loops are bounded to one iteration unless invariants are inferred, pointer aliasing is conservative, recursion is bounded. A fold finding is "SAT under our encoding," not "the program has a defect under all behaviors."
• A whole-program analyzer. fold is per-function with summary caching across function boundaries; full interprocedural fixpoint analysis remains future work (docs/research/frontier.md).
• A replacement for runtime sanitizers in production. ASan / UBSan / MSan catch failures fold cannot prove statically; fold helps prioritize which inputs to feed them.
• A managed service. fold is a CLI binary you run in your CI next to clang-tidy. There is no SaaS dashboard.

Where fold's closed scan→fuzz loop matters

The Phase 1+2 work in M31 closes the loop inside one tool (directed fuzzers such as AFLGo and hybrid tools such as SAVIOR explore related ground; see docs/research/prior-art.md): every SAT finding is automatically packaged as a libFuzzer seed, run under ASan, and (if a crash is observed) promoted from Proved to ConcreteWitness in the same JSON report. The user sees one Finding with confidence: "concrete-witness" instead of two separate reports from two separate tools that need to be cross-correlated.

Commercial peers (Coverity, Klocwork) have integrations between SAST and DAST, but they remain conceptually two pipelines glued together. fold is one pipeline.

This matters for triage cost: a developer reviewing confidence: concrete-witness is reviewing an observed crash with a reproducer, not a model output that might still be a false positive against the encoder's over-approximations.

When to choose fold

• You want Z3-grade arithmetic reasoning on C/C++ at scan throughput, not single-function verification throughput.
• You can build with LLVM 22 + Z3 locally and would rather own the toolchain than depend on a SaaS.
• You value witness-quality findings — every flagged sink ships with the inputs that exhibit it.
• You want SAST + fuzzing as one feedback loop, not two artifacts to correlate by hand.

When to choose something else

• You need maximum scan throughput on a 10M-LOC monorepo with no false positives. Coverity or CodeQL with a tuned ruleset will likely beat fold today; fold's FP-tuning maturity is still climbing.
• You need taint queries on a CPG. CodeQL or Joern are better matched to that shape.
• You need to verify a kernel module exhaustively. CBMC or KLEE on the target module, not a codebase-wide scanner.
• You're on Go, Java, or TypeScript. fold has no frontend for those today. Rust has an MVP frontend (see docs/internal/rust-frontend.md) scoped to unsafe-block raw-pointer derefs and within-language clones — not a full Rust analyzer.

Roadmap signal

docs/research/frontier.md tracks what's planned. The two biggest open shapes:

1. Interprocedural fixpoint summaries beyond leaf functions — currently fold's interprocedural reasoning is bounded by the summary cache's depth.
2. Concolic loop closure (M31 Phase 3, scoped in docs/internal/m31-phase3-concolic.md) — bring SymCC-style runtime symbolic execution into the fuzz-run feedback loop.

Neither is shipped. Both are tracked, scoped, and have an opinion in their respective design docs.