1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
//! 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`](super::Soundness::MayOver) under the standard
//! widening-narrowing correctness argument.
#[cfg(any(test, feature = "cpu-parity"))]
mod cpu_oracle;
mod dispatch;
mod program;
mod scratch;
mod tag;
#[cfg(test)]
mod tests;
pub(crate) const OP_ID: &str = "weir::loop_sum";
#[cfg(any(test, feature = "cpu-parity"))]
#[allow(deprecated)]
pub(crate) use cpu_oracle::loop_summarize_cpu;
pub use dispatch::{
loop_summarize_borrowed_into_result_with_scratch_via, loop_summarize_borrowed_into_via,
loop_summarize_borrowed_via, loop_summarize_borrowed_with_scratch_via, loop_summarize_via,
};
pub use program::{loop_summarize, try_loop_summarize_with_count};
#[cfg(any(test, feature = "legacy-infallible"))]
pub use program::loop_summarize_with_count;
pub use scratch::LoopSummarizeScratch;
pub use tag::LoopSum;