Module range 

Interval range propagation (DF-7).

Build a range-propagation Program:

use weir::range::range_propagate;

let program = range_propagate("defs_in", "edges_in", "ranges_out");

DF-7 - value-range and symbolic-length lattice.

Interval abstract domain over integer-typed variables: ⟨lo, hi⟩ ∈ {−∞, ℤ, +∞}². Overflow tracked as a separate flag so the domain is sound under wrap-around arithmetic.

Extended with symbolic-length expressions: len(buf) + k, where k is a range constant. Critical for C05 (integer trunc → undersized alloc → OOB) and C19 (ioctl size fields that bypass copy_from_user bound checks when the lattice concretizes to a non-trivial range).

Implementation

Each variable occupies two consecutive u32 slots [lo, hi] in the flat buffer. One invocation per variable, indexed by InvocationId axis 0. The edge transfer is an additive shift per variable (lo' = lo + t_lo, hi' = hi + t_hi) - the simplest interval transfer that covers assign, add-const, and symbolic-length-plus-k.

Meet at join points is the caller’s responsibility: join two runs of this primitive with an element-wise min(lo, lo') / max(hi, hi') kernel (built via vyre_primitives::math ops).

Soundness: MayOver in the standard abstract-interpretation sense. Zero-FP rules that consume this lattice must pair with DF-3 + an aliasing filter.

Structs

Range

Marker type for the interval-range dataflow primitive.

RangePropagateScratch

Caller-owned staging for repeated range propagation dispatches.

Functions

range_propagate

Build one forward interval-propagation step.

range_propagate_borrowed_into_result_with_scratch_via

GPU range propagation using caller-owned staging/output scratch and caller-owned decoded result storage.

range_propagate_borrowed_into_via

GPU range propagation using borrowed dispatch inputs and caller-owned output storage.

range_propagate_borrowed_via

GPU range propagation using borrowed dispatch inputs.

range_propagate_borrowed_with_scratch_via

GPU range propagation using borrowed dispatch inputs and caller-owned staging/output scratch.

range_propagate_via

try_range_propagate

Checked version of range_propagate for callers that want uniform fallible construction.

try_range_propagate_with_count

Checked version that takes var_count explicitly.