weir/range.rs
1//! DF-7 - value-range and symbolic-length lattice.
2//!
3//! Interval abstract domain over integer-typed variables:
4//! `⟨lo, hi⟩ ∈ {−∞, ℤ, +∞}²`. Overflow tracked as a separate flag
5//! so the domain is sound under wrap-around arithmetic.
6//!
7//! Extended with symbolic-length expressions: `len(buf) + k`, where
8//! `k` is a range constant. Critical for C05 (integer trunc →
9//! undersized alloc → OOB) and C19 (ioctl size fields that bypass
10//! `copy_from_user` bound checks when the lattice concretizes to a
11//! non-trivial range).
12//!
13//! # Implementation
14//!
15//! Each variable occupies two consecutive u32 slots `[lo, hi]`
16//! in the flat buffer. One invocation per variable, indexed by
17//! `InvocationId` axis 0. The edge transfer is an additive shift
18//! per variable (`lo' = lo + t_lo`, `hi' = hi + t_hi`) - the
19//! simplest interval transfer that covers assign, add-const, and
20//! symbolic-length-plus-k.
21//!
22//! Meet at join points is the caller's responsibility: join two
23//! runs of this primitive with an element-wise `min(lo, lo')` /
24//! `max(hi, hi')` kernel (built via `vyre_primitives::math` ops).
25//!
26//! Soundness: [`MayOver`](super::Soundness::MayOver) in the standard
27//! abstract-interpretation sense. Zero-FP rules that consume this
28//! lattice must pair with DF-3 + an aliasing filter.
29
30#[cfg(any(test, feature = "cpu-parity"))]
31mod cpu_oracle;
32mod dispatch;
33mod program;
34mod scratch;
35mod tag;
36
37#[cfg(test)]
38mod tests;
39
40pub(crate) const OP_ID: &str = "weir::range";
41
42#[cfg(any(test, feature = "cpu-parity"))]
43#[allow(deprecated)]
44pub(crate) use cpu_oracle::range_propagate_cpu;
45pub use dispatch::{
46 range_propagate_borrowed_into_result_with_scratch_via, range_propagate_borrowed_into_via,
47 range_propagate_borrowed_via, range_propagate_borrowed_with_scratch_via, range_propagate_via,
48};
49pub use program::{range_propagate, try_range_propagate, try_range_propagate_with_count};
50#[cfg(any(test, feature = "legacy-infallible"))]
51pub use program::range_propagate_with_count;
52pub use scratch::RangePropagateScratch;
53pub use tag::Range;