fold/docs/internal/perf-audit/optimization-backlog.md

Fold optimization backlog from literature

This backlog maps literature-backed ideas to concrete Fold work. Each item must be benchmarked with bench/run_micro_opt.py and at least yams-wide20-security.

1. Demand-driven sink slicing

• Source: SVF/SUPA demand-driven value-flow; Clang Static Analyzer checker callback discipline.
• Fold shape: find detector-relevant sink statements first, then focus full symbolic walking around only functions/slices that can emit active-detector hooks.
• Implementation stages: function-level sink precheck (landed), then per-sink structural target walks, then sparse backward fact collection.
• Metrics: functions_prechecked_safe, candidate_sink_count, control_walk_ms, finding stability.

2. CFG worklist facts before symbolic execution

• Source: Clang dataflow / abstract interpretation.
• Fold shape: compute must-facts once per function over the CFG: non-null, nonzero, bounded index, positive counters, validated members.
• Metrics: reduced z3_queries, increased abstract_unsat, stable findings.

3. AST-independent condition fact cache

• Source: abstract interpretation transfer functions and Clang SA performance guidance on repeated analysis steps.
• Fold shape: cache condition decomposition by (Expr*, assume_true) and replay into ranges/octagon without re-walking condition ASTs.
• Metrics: range_refine_ms, octagon_refine_ms, condition_fact_ms.

4. Sparse summaries and demand-driven cross-TU

• Source: compositional analysis / Infer-like summaries and value-flow graph reachability.
• Fold shape: store callee preconditions/effects that matter to security: derefed params, divisor params, arithmetic params, bounds params, returned non-null, output length constraints.
• Metrics: cross_tu_prime_ms, summary_lookup_ms, callsite findings.

5. Z3 funnel and query-shape optimization

• Source: Z3 bit-vector and tactics guidance.
• Fold shape: keep constant/interval/octagon checks ahead of QF_BV; track cache hits/misses and only experiment with tactics for repeated hard families.
• Metrics: expr_cache_hits, expr_cache_misses, z3_queries, z3_timeouts.

6. Trace discipline

• Source: Clang Static Analyzer performance investigation.
• Fold shape: profile per function and per detector, then use heavier tools only after profile JSON narrows the hot bucket.
• Metrics: top-N function cost report, median/IQR across real-code runs.