# 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.