54 lines
2.5 KiB
Markdown
54 lines
2.5 KiB
Markdown
# 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.
|