weir/
loop_sum.rs

1//! DF-10  -  loop summarization (stratified fixpoint acceleration).
2//!
3//! Widening + narrowing over loops so range / taint analyses
4//! terminate in finitely many iterations on unbounded loops.
5//! Required for decode-chain detection (C10 decompression bomb, C11
6//! parser differential, C15 path traversal decode chain) where the
7//! vuln only manifests after N iterations of a loop that reads a
8//! length-prefixed field.
9//!
10//! # Implementation
11//!
12//! Standard Cousot widening on the interval lattice: at a loop
13//! header, the new summary is `widen(prev, new)` where
14//! `widen(⟨a, b⟩, ⟨c, d⟩)` keeps `a` if it was finite and reduced
15//! else jumps to `-∞`, and keeps `b` if it was finite and grew
16//! else jumps to `+∞`. The u32 lattice uses `0` as `-∞` sentinel
17//! and `u32::MAX` as `+∞` sentinel.
18//!
19//! Each invocation handles one variable's `[lo, hi]` pair,
20//! identical buffer layout to DF-7 `range`.
21//!
22//! Soundness: [`MayOver`](super::Soundness::MayOver) under the standard
23//! widening-narrowing correctness argument.
24
25#[cfg(any(test, feature = "cpu-parity"))]
26mod cpu_oracle;
27mod dispatch;
28mod program;
29mod scratch;
30mod tag;
31
32#[cfg(test)]
33mod tests;
34
35pub(crate) const OP_ID: &str = "weir::loop_sum";
36
37#[cfg(any(test, feature = "cpu-parity"))]
38#[allow(deprecated)]
39pub(crate) use cpu_oracle::loop_summarize_cpu;
40pub use dispatch::{
41    loop_summarize_borrowed_into_result_with_scratch_via, loop_summarize_borrowed_into_via,
42    loop_summarize_borrowed_via, loop_summarize_borrowed_with_scratch_via, loop_summarize_via,
43};
44pub use program::{loop_summarize, try_loop_summarize_with_count};
45#[cfg(any(test, feature = "legacy-infallible"))]
46pub use program::loop_summarize_with_count;
47pub use scratch::LoopSummarizeScratch;
48pub use tag::LoopSum;
weir/loop_sum.rs

weir/
loop_sum.rs
