37 lines
2.1 KiB
Markdown
37 lines
2.1 KiB
Markdown
# 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".
|