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.