# Literature alignment for Fold optimization

Fold's source security backend is closest to a bounded, path-sensitive symbolic
executor over Clang AST/CFG with detector hooks. The next optimization work should
preserve precision by moving work earlier only when it is a sound precheck, or by
caching AST-derived facts whose meaning is independent of the current symbolic
environment.

## Relevant prior art

- **Clang Static Analyzer** uses path-sensitive symbolic execution over an
  exploded graph. Its performance guidance emphasizes measuring path explosion,
  avoiding repeated work, and keeping checker callbacks cheap.
- **Clang dataflow analysis** frames local facts as lattice elements propagated
  by CFG worklists. Fold can borrow this for cheap, must-hold facts before it
  pays for recursive symbolic walks.
- **Z3 / Programming Z3** guidance supports Fold's current ordering: discharge
  constants, intervals, and simple abstract domains before asking QF_BV solvers;
  use solver incrementality carefully and measure tactic overhead.
- **SVF/SUPA demand-driven value-flow** argues for sparse, demand-driven analysis
  near relevant sinks. Fold's detector sink precheck follows that principle by
  skipping full security walks for functions that cannot fire the active detector.
- **Large-scale static analysis reports** reinforce that precision and user trust
  are performance features: faster scans must not simply hide findings unless the
  finding is proven to be a false positive.

## Fold-specific implications

1. Keep Z3 at the end of the funnel: syntactic facts, interval/octagon facts, and
   detector-specific abstract guards should continue to short-circuit queries.
2. Treat `SecurityWalker::control_walk_ms` as the main optimization target; prior
   profiling showed Z3, env cloning, and hook bodies are not dominant.
3. Cache only environment-independent facts by AST identity, such as syntactic
   sink presence, condition shape, written vars, and summary lookup timing.
4. Use real-code medians on Yams/curl for acceptance; micro-benchmarks are fast
   gates, not final proof.
5. Prefer precision-preserving prechecks and pruning over a global "fast mode".