Module loop_sum 

Loop summarization with widening+narrowing (DF-10).

Build a loop-summary Program:

use weir::loop_sum::loop_summarize;

let program = loop_summarize("prev", "next", "out");

DF-10 - loop summarization (stratified fixpoint acceleration).

Widening + narrowing over loops so range / taint analyses terminate in finitely many iterations on unbounded loops. Required for decode-chain detection (C10 decompression bomb, C11 parser differential, C15 path traversal decode chain) where the vuln only manifests after N iterations of a loop that reads a length-prefixed field.

Implementation

Standard Cousot widening on the interval lattice: at a loop header, the new summary is widen(prev, new) where widen(⟨a, b⟩, ⟨c, d⟩) keeps a if it was finite and reduced else jumps to -∞, and keeps b if it was finite and grew else jumps to +∞. The u32 lattice uses 0 as -∞ sentinel and u32::MAX as +∞ sentinel.

Each invocation handles one variable’s [lo, hi] pair, identical buffer layout to DF-7 range.

Soundness: MayOver under the standard widening-narrowing correctness argument.

Structs

LoopSum

Marker type for the loop-summarization dataflow primitive.

LoopSummarizeScratch

Caller-owned staging for repeated loop-summary dispatches.

Functions

loop_summarize

One widening step. cfg_in holds the previous-iteration intervals [prev_lo_v, prev_hi_v, …]; ranges_in holds the new iteration’s intervals; summary_out receives the widened result per variable.

loop_summarize_borrowed_into_result_with_scratch_via

GPU loop summarization using caller-owned staging/output scratch and caller-owned decoded result storage.

loop_summarize_borrowed_into_via

GPU loop summarization using borrowed dispatch inputs and caller-owned output storage.

loop_summarize_borrowed_via

GPU loop summarization using borrowed dispatch inputs.

loop_summarize_borrowed_with_scratch_via

GPU loop summarization using borrowed dispatch inputs and caller-owned staging/output scratch.

loop_summarize_via

try_loop_summarize_with_count

Checked version of [loop_summarize_with_count] for production GPU wrappers.