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 breaks, 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.