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