# Research

## Architecture

fold is a bounded symbolic SAST built on a backend-neutral scan shell plus the
source-analysis stack:

1. **Analysis backend**: `AnalysisBackend` discovers analysis units and extracts
   `FunctionIR`. `ClangBackend` wraps the source path; `R2Backend` is the
   prototype binary path using radare2.
2. **Clang frontend**: LibTooling parses C++ into AST. Frontend actions fan out
   to all enabled detectors in a single TU pass.
3. **Symbolic encoder**: translates AST expressions to Z3 BV-64. Path predicate
   accumulates through branches. BV-64 signedness-aware widening (zext unsigned,
   sext signed). SSA renaming per function. Phi symbols at if/else joins.
4. **Observer detectors**: encoder fires hooks (`onBinaryArith`, `onPointerDeref`,
   `onLibraryCall`, `onCallExpr`, `onBufferCopy`) on hazard-relevant IR nodes.
   Detectors implement observers and query Z3 under path constraints.

The backend seam lives in `include/fold/core/analysis_backend.hpp`. Source scans
still delegate to the mature Clang detector pipeline. Binary scans currently
produce heuristic findings directly from radare2-discovered strings, calls, and
pseudocode; they do not yet lift binary functions into the symbolic source IR.
The planned source/binary scan router and hybrid CLI contract are specified in
`docs/research/cli-router.md`.

radare2 integration prefers linked `libr_core` (`-Dradare2=enabled`) and falls
back to invoking `r2` when the development libraries are absent. This gives a
path to pinned/vendored radare2 builds without coupling normal source scans to a
large third-party tree.

Cross-function: `CrossTUCache` shares callee properties (deref params, null-return,
divisor params) across TUs. `SummaryStore` provides leaf-function symbolic return
substitution. `IncrementalCache` fingerprints functions for `--incremental` skip.

Heap model: `HeapModel` tracks per-malloc regions with freed state, byte offsets,
and allocation-site metadata. UaF/double-free through OOB observer.

Key design decisions: QF_BV logic only, assumption-based `check(1, &hazard)`,
push/pop branch scoping, k=3 default loop unroll with post-loop havoc, per-function
solver lifetime, expression canonicalization cache.

**Crash isolation**: non-incremental, non-profile source scans use an OS worker
process even when `--processes 1` is requested. Workers emit a `file_finished`
record after each TU. If a worker exits or receives a fatal signal, the parent
retains findings from completed TUs, quarantines the first unfinished TU, and
restarts the remaining shard in a clean process. Quarantine records use
`<path>\tworker-exit:<status>` or `<path>\tsignal:<number>` so ordinary frontend
failures are not mislabeled as timeouts. The loader remains compatible with the
legacy `<path>:<signal>` form. Incremental and profile scans currently retain
the in-process per-TU `runWithSignalIsolation` fallback because their shared
index/profile state is not worker-mergeable yet. The set of known asserting
Clang APIs and installed precondition gates is catalogued in
`docs/research/clang-quirks.md`.

## Juliet Benchmarks (2026-05-15 final, with all optimizations)

| CWE | Detector | Gold | TP | Precision | Recall | CSA Recall | Queries |
|-----|----------|------|-----|-----------|--------|------------|---------|
| 476 | null-deref | 364 | 184 | 68.7% | 50.5% | 56.0% | 876 |
| 369 | div-by-zero | 938 | 576 | 57.5% | 61.4% | 5.8% | 3222 |
| 190 | int-overflow | 4178 | 1851 | 57.6% | 44.3% | 0.0% | 8849 |
| 121 | oob-access | 5252 | 466 | 61.2% | 8.9% | 6.2% | 5855 |

Total scan time: 741s (12m 21s). Total TP: 3,077.

## Soundness

BV-64 encoding sound for the bounded model (k-unrolled). Every `BailReason`
replaces the expression with an unconstrained fresh symbol — sound but imprecise.

Completeness class: loop-free, integer-only, no-heap, no-call leaf functions.
Within this class, fold has zero false negatives. Proof in `soundness.md`.

## Yams Audits

- **2026-05-13** (baseline, 8 detectors): 55K raw findings, 0 TPs on manual review.
  clone: 6833, equiv: 12, dead: 4, class-dup: 0, dead-statement: 3184, unused-function: 181.
- **2026-05-14**: FP roadmap quick-wins (type filter, per-emission dedup, constant-fold
  literal divisors, null-deref observer rewrite). Findings dropped ~50%.
  Encoder recursion discovered and fixed via RAII depth guard.