fold/docs/internal/loop-summarization-research.md

# Loop Summarization + Frontend-Agnostic Loop IR — Research Synthesis

> Generated 2026-05-30. Design research for replacing per-iteration loop unrolling with
> loop summarization in fold's core, on a frontend-agnostic loop IR. Gates Workstream B of
> the "precision-drift + IR/loop-perf" plan. Pairs with `perf-audit.md` (cost attribution),
> `multi-language-ir-patterns.md` (IR direction), and `interprocedural-buffer-threading.md`.

## 1. Problem recap

fold handles loops by **bounded unrolling**: `SecurityWalker::unrollLoop`
(`src/detect/security_walker.cpp` ~1990) walks the body `loop_unroll` (default 3) times,
encoding statements and firing observer hooks — each hook may issue a Z3 query — then havocs
modified vars and widens ranges. Two consequences:

1. **Query-volume blowup.** On data-dependent `while(1)` scanners (e.g. the dbench JUMBF JPEG
   marker loops, `dbench_jumbf.cpp:279,375`) the body is large and nested, so unroll × nesting
   produces ~170 hard sink queries each burning the per-query budget. Measured: 8+ min uncapped;
   52s even at `--loop-unroll 1 --per-query-ms 300`. The cooperative deadline + flush-deadline +
   non-progress fixpoint (shipped) bound the *fallback* but cannot make a query-bound TU finish
   under budget — it gets watchdog-quarantined. (See `perf-audit.md`: 89% of wall is recursive
   control-flow walking; the cost is symbolic execution ∝ statements × control-nesting depth.)

2. **Clang coupling blocks a core fix.** Loop handling is on `clang::ForStmt`/`WhileStmt`/`DoStmt`
   directly (81 `clang::` sites in `security_walker.cpp`), and `ir/cfg_walker.hpp` still exposes
   `clang::CFG*`/`clang::CFGBlock*`. So any loop summarization written here would be clang-only
   and would have to be re-implemented for the rust (`rust_ir_encoder.cpp`) and binary
   (`binary_bb_encoder.cpp`) frontends. The fix must live on an abstract loop IR.

## 2. Literature synthesis

| Technique | Source | Relevance to fold |
|---|---|---|
| **Loop acceleration → Presburger / recurrence summaries.** Accelerate simple loops into closed constraints; summarize nested loops with recurrence relations derived from the inner loop's acceleration (may over-approximate). | Liu & Wahl 2015, arXiv:1505.02637 | Core lever: replace N unrolled bodies + per-iteration queries with **one** trip-count-parameterized constraint set. Over-approximation is acceptable for fold (refutation, not verification). |
| **Loop-modified variables as closed-form functions of the iteration count**; steer execution by solving a per-loop constraint system. | Obdrzalek & Trtik 2011, arXiv:1107.1398 | Gives the shape of an affine/counted-loop summary: `x_k = x_0 + k·Δ`. Matches fold's existing `widenLoopRange`/octagon value abstractions. |
| **k-induction + invariant inference** for C verification *and refutation*. | Alhawi & Cordeiro 2020, doi:10.1007/s10009-020-00564-1 (ESBMC) | Alternative/complement to acceleration; fold already has `bench/run_esbmc_on_juliet.py` → ESBMC is the natural quantitative comparator for any summarization approach. |
| **Path-explosion taxonomy**: scope reduction vs guidance heuristics. | Bailey & Nicholas 2025, arXiv:2508.06643 | Frames summarization as *scope reduction* — the highest-ROI class for fold's per-function bounded model. |
| **Incorrectness / under-approximate bug-finding.** | Raad et al. 2020 (ISL) | Justifies fold's posture: we may soundly *over*-approximate reachability (never drop a true bug) and *under*-approximate only where we already bail — summaries must not introduce false negatives, but may introduce (bounded) false positives that downstream confidence tags already handle. |
| **Small core-op IR + shared backend** (Infer SIL ~10 ops, Kani MIR→Z3, CodeQL lang-frontends + shared engine). | `multi-language-ir-patterns.md`, `ir-cross-language-research.md` | The encoder should consume a small set of core IR ops (incl. an explicit loop node), not clang `Stmt`; one summarization pass then serves all frontends. |

## 3. Chosen approach

**Affine/counted-loop closed-form summarization, recurrence-based nested handling, bounded-unroll
fallback** — implemented once in the core over an abstract loop IR.

- **Classify** each loop: (a) *counted/affine* — single integer induction variable with constant
  stride and a comparison exit condition (`for (i=a; i<b; i+=c)` and the common `while`
  equivalents); (b) *non-affine / irreducible / data-dependent* (`while(1)` with `break`s, pointer
  walks, multiple exits).
- **(a) Summarize:** emit one constraint set parameterized by a symbolic trip count `k` (bounded by
  the exit condition), with induction/derived vars as closed forms `v_k = v_0 + k·Δ` (recurrences
  for nested loops, conservatively widened). Fire each in-body sink **once** against the
  summarized state instead of once per unrolled iteration → collapses the query count from
  O(unroll × nesting × sinks) to O(sinks).
- **(b) Fallback:** keep the existing bounded unroll (and this session's deadline / flush-deadline /
  non-progress-fixpoint guards) for loops we cannot summarize soundly.

Rationale: counted/affine loops are where unrolling wastes the most queries and where closed forms
are cheap and exact; `while(1)` scanners stay on the guarded fallback (correctness over speed).
ESBMC's k-induction is heavier and aimed at proving; acceleration fits fold's bounded refutation
model better and reuses the octagon/range machinery already present.

## 4. Abstract loop/CFG IR shape (target for B1)

Add to `fold::ir` (frontend-agnostic; no `clang::` in headers, builders in `*_clang.cpp` /
rust / binary):

```
ir::FunctionCFG   // owns blocks + edges; NO clang::CFG* in the public type
ir::CFGBlock      // id, successors/predecessors, ordered ir statements
ir::Loop {
    header, latch, exits;            // block ids
    std::vector<InductionVar> ivs;   // { Symbol, init Expr, stride Expr, kind }
    Expr exit_condition;             // normalized guard
    LoopKind kind;                   // Counted | Affine | General
}
```

Induction-variable + stride detection lowers from clang (`ForStmt` analysis already partly exists
as `analyzeForLoopRange`) and from rust MIR / binary BBs into the same `ir::Loop`. The encoder/
walker consumes `ir::Loop`, not `clang::ForStmt`.

## 5. Precision contract (non-negotiable)

1. A summary's **reachability** of any in-body sink must be an **over-approximation** of the real
   loop — i.e. if the real loop can reach a sink, the summary must too. This guarantees **no true
   finding is dropped** (no new false negatives).
2. Value abstractions in the summary may be **widened** (less precise) — this can only add
   heuristic/over-approximated findings, which fold's confidence tags (`proved` vs `heuristic` vs
   `over-approximated`) already communicate.
3. When affine classification is **uncertain**, fall back to bounded unroll. Never summarize a loop
   whose induction/stride/exit we cannot establish.
4. The Workstream-A committed baseline gate is the enforcement mechanism: **zero precision/recall
   regression** on Juliet + security-bugs + interproc, or the change does not land.

## 6. Integration points in fold

- `include/fold/ir/cfg_walker.hpp` + new `include/fold/ir/loop.hpp` — abstract types (B1).
- `src/symbolic/*_clang.cpp` (new builder, mirroring `ir_expr_clang.cpp`) — clang→ir lowering;
  reuse `analyzeForLoopRange`. Rust: `rust_ir_encoder.cpp`; binary: `binary_bb_encoder.cpp`.
- `src/detect/security_walker.cpp` `unrollLoop` → thin dispatcher: summarize (a) or fallback (b).
  Reuse `widenLoopRange`, `octagon_`, `cachedCollectWrittenVars`.
- Carry the shipped fallback guards (`WalkOptions::walk_deadline`, `BatchSafetyObserver` flush
  deadline, non-progress fixpoint).

## 7. Evaluation plan

- **Precision:** Workstream-A committed baseline (Juliet 14 CWEs + security-bugs + interproc) —
  zero regression. Add unit tests: counted loop summarized (query count drops), non-affine falls
  back, a known loop-dependent finding still fires.
- **Perf:** `dbench_jumbf.cpp` cold-cache completes **under budget, no watchdog quarantine**; the 8
  int-overflow findings persist; `--profile` shows reduced `control_walk_ms` + query count.
- **Comparator:** `bench/run_esbmc_on_juliet.py` on the loop-heavy CWEs to sanity-check
  recall/precision of summarization vs a k-induction tool.
- **Cross-frontend reuse:** one rust loop case + one binary loop case exercise the same core
  summarization path (advances loop2-priorities #1 "unify binary + source Z3 paths").

## 8. Risks & open questions

- **False negatives from an unsound summary** — mitigated by the over-approximation contract (§5)
  + baseline gate; default to fallback when unsure.
- **Encoder size** — `encoder.cpp` is 2219 lines (over budget). Per CLAUDE.md, extract the
  summarization pass into its own TU(s); no new monoliths.
- **Nested-loop recurrences** — start with single-level affine; nested recurrence summarization is
  a follow-up once single-level is proven on the gate.
- **context7 not connected this session** — provision via the sage hub for Z3 quantifier/array and
  LLVM `CFG` API specifics before B1 coding; otherwise rely on `clang-analysis-api-research.md`.

## 9. References
- Liu, Wahl. *Unbounded-Thread Reachability via Symbolic Execution and Loop Acceleration.* arXiv:1505.02637 (2015).
- Obdrzalek, Trtik. *Efficient Loop Navigation for Symbolic Execution.* arXiv:1107.1398 (2011).
- Alhawi, Rocha, Gadelha, Cordeiro, Batista. *Verification and refutation of C programs based on k-induction and invariant inference.* STTT, doi:10.1007/s10009-020-00564-1 (2020).
- Bailey, Nicholas. *Symbolic Execution in Practice: A Survey…* arXiv:2508.06643 (2025).
- Raad, Berdine, Dang, Dreyer, O'Hearn, Villard. *Incorrectness Separation Logic.* (2020).
- fold internal: `multi-language-ir-patterns.md`, `ir-cross-language-research.md`, `perf-audit.md`.

---

## Appendix: drift root-cause #1 — null-deref `priorFunctionTextProvesNonNull` (fixed 2026-05-30)

Workstream-A triage of the null-deref CWE-476 recall regression (baseline F1 0.583
→ HEAD 0.485) found the cause was **not** a path-forking bug but a *poor optimization*:
commit `331a68467` ("Optimize security detectors and add quality gates", 2026-05-23)
added `priorFunctionTextProvesNonNull`, a whole-function **source-text** heuristic that
treated the textual presence of `p->`, `*p`, `p!=0`, `p!=NULL`, `p!=nullptr` before a
deref as proof the pointer was non-null, suppressing the finding.

The `!=`-comparison patterns are unsound: a textual `p != 0` is a *test*, not a
guarantee. It suppressed real derefs whenever `p != 0` appeared (textually, after the
last assignment) before the deref — e.g. Juliet's `binary_if` bad case
`if ((p != NULL) & (p->intOne == 5))` (bitwise `&`, both operands evaluated → real
null deref), and any `x = (p != 0); … p->m;` straight-line pattern. Minimal repros in
`/tmp/nd*.c`; the distinguisher is encoding order (a deref *before* the `!=0` text was
still flagged).

**Fix:** removed the heuristic from the suppression chain (`null_deref.cpp` ~883) and
deleted the function. Legitimate non-null facts remain covered by sound mechanisms:
M20 deref-implies-non-null (`markDefinitelyNonNull`/`isDefinitelyNonNull`, encoder),
`enclosingThenBranchProvesNonNull` (`if (p)` then-branch),
`sourceLineShortCircuitProvesNonNull` (`p && p->x`), `staticParamContractProvesNonNull`.

**Result (CWE-476 null-deref):** F1 0.485 → **0.583** (= baseline), recall 0.379 →
**0.517** (above baseline 0.497), precision 0.673 → 0.669 (flat). security-bugs
null-deref stays P1.0/R1.0; full unit suite green (66/0).

**Residual (separate, narrow):** `(p != 0) && p->x` (note `!=0`, and parenthesized)
still FPs because the *sound* same-line `&&` recognizer's text patterns don't handle the
`!=0`/parenthesized form. Right fix is path-sensitive (`&&` fork actually constraining
the null-deref query), not more text patterns — tracked for the IR/encoder work, not
papered over.

**Lesson for Workstream B:** prefer path-sensitive/semantic facts over source-text
heuristics; text-proof shortcuts trade recall for FP-suppression invisibly. The
loop-summarization work must encode guards as constraints, not text patterns.

---

## Appendix: remaining work + architecture finding (2026-05-31)

Status: clang-frontend loop summarization is **done** — `ir::Loop` (Counted | Affine |
General) + `buildLoopFromClang`, wired into `SecurityWalker::unrollLoop`; counted and
affine (symbolic-bound) loops are summarized (sink fired once against the closed-form
range asserted as a Z3 constraint; findings tagged LoopHavoc/heuristic). Gate-validated,
deterministic baseline.

**Key finding that reshapes "cross-frontend reuse":** the rust and binary frontends do
**not** go through `SecurityWalker`/`unrollLoop` and have **no loop handling** today:
- `src/symbolic/rust_ir_encoder.cpp` encodes MIR expression nodes; no loop/unroll/CFG.
- `src/symbolic/binary_bb_encoder.cpp` encodes one basic block at a time (straight-line);
  no back-edge / loop detection.

So lowering `ir::Loop` for rust/binary does **not** by itself enable summarization there —
each frontend would first need loop detection routed through a *shared* loop-walk core.
That means the three "remaining" items are not independent slices; they are one coupled
effort gated on the same foundation:

### Realistic sequencing (each a focused session)
1. **Clang-free CFG + shared loop-walk core (B1-full).** Make `ir::FunctionCFG`/`CFGWalker`
   stop exposing `clang::CFG*`/`CFGBlock*`; move the ~81 `clang::` sites in
   `security_walker.cpp` onto IR; extract the loop dispatch (unroll vs summarize) into a
   frontend-agnostic core that consumes `ir::Loop` + an `ir::CFG`. Prerequisite for the
   other two. Large, mechanical, precision-sensitive — guard every step with the drift gate.
2. **Rust/binary lower into the shared core.** rustc MIR back-edges and r2 BB back-edges →
   `ir::Loop`; route their encoders through the shared loop-walk so counted/affine
   summarization is reused (the multi-frontend payoff). Advances loop2-priorities #1
   ("unify binary + source Z3 paths").
3. **`while(1)` / General acceleration.** The dbench JUMBF blowup. Must be **recall-
   preserving** (additive: keep bounded unroll's concrete-iteration findings AND add a
   summary pass; union, dedup) — a single-walk replacement traded detection in B2's affine
   experiment. Research-grade (recurrence/acceleration); highest precision risk. Today the
   robustness guards (cooperative deadline + flush deadline + non-progress fixpoint) keep
   it bounded (graceful partial findings), which is acceptable until acceleration lands.

No safe small gate-validatable slice exists short of starting (1). Recommend each as a
dedicated session with the drift gate as the guardrail.