FEAT-042 (v2.6): widening with thresholds

artifacts/roadmap-3.0.yaml

@@ -175,7 +175,7 @@ artifacts:
   - id: FEAT-042
     type: feature
     title: "v2.6 — Widening with thresholds"
-    status: proposed
+    status: accepted
     release: v2.6.0
     description: >
       Replace the fixed iterate-then-widen at LOOP_WIDEN_THRESHOLD with widening

crates/scry-analyze-core/src/lib.rs

@@ -2423,13 +2423,13 @@ const LOOP_ITER_CAP: u32 = 64;
 /// Per-local widening (FEAT-016 slice-2a). `widen(a, b)` over the interval
 /// domain (scry-interval, terminating ascending-chain); region/unknown keep
 /// their value only if unchanged, else degrade to ⊤ (`Unknown`).
-fn widen_abstract(a: &AbstractValue, b: &AbstractValue) -> AbstractValue {
+fn widen_abstract(a: &AbstractValue, b: &AbstractValue, thresholds: &[i64]) -> AbstractValue {
     match (a, b) {
         (AbstractValue::I32Interval(x), AbstractValue::I32Interval(y)) => {
-            AbstractValue::I32Interval(scry_interval::widen(*x, *y))
+            AbstractValue::I32Interval(scry_interval::widen_with_thresholds(*x, *y, thresholds))
         }
         (AbstractValue::I64Interval(x), AbstractValue::I64Interval(y)) => {
-            AbstractValue::I64Interval(scry_interval::widen(*x, *y))
+            AbstractValue::I64Interval(scry_interval::widen_with_thresholds(*x, *y, thresholds))
         }
         _ if a == b => clone_value(a),
         _ => AbstractValue::Unknown,
@@ -2455,8 +2455,15 @@ fn join_locals(a: &[AbstractValue], b: &[AbstractValue]) -> Vec<AbstractValue> {
     a.iter().zip(b).map(|(x, y)| join_abstract(x, y)).collect()
 }
 
-fn widen_locals(a: &[AbstractValue], b: &[AbstractValue]) -> Vec<AbstractValue> {
-    a.iter().zip(b).map(|(x, y)| widen_abstract(x, y)).collect()
+fn widen_locals(
+    a: &[AbstractValue],
+    b: &[AbstractValue],
+    thresholds: &[i64],
+) -> Vec<AbstractValue> {
+    a.iter()
+        .zip(b)
+        .map(|(x, y)| widen_abstract(x, y, thresholds))
+        .collect()
 }
 
 /// Interval NARROWING (FEAT-016 slice-2b-i): replace each INFINITE bound of
@@ -2717,6 +2724,10 @@ struct Interp<'a, 'b> {
     diagnostics: &'a mut Vec<Diagnostic>,
     call_graph: &'a mut Vec<CallEdge>,
     points: Vec<ProgramPoint>,
+    /// FEAT-042: syntactic widening thresholds for this function (its constant
+    /// operands, plus 0), used by the loop-header widening to snap a runaway
+    /// bound to the nearest enclosing constant instead of ±∞.
+    widen_thresholds: Vec<i64>,
 }
 
 impl Interp<'_, '_> {
@@ -3117,7 +3128,7 @@ impl Interp<'_, '_> {
                 None => (entry.clone(), entry_oct.clone()),
             };
             if iter >= LOOP_WIDEN_THRESHOLD {
-                next = widen_locals(&header, &next);
+                next = widen_locals(&header, &next, &self.widen_thresholds);
                 next_oct = scry_octagon::widen(&header_oct, &next_oct);
             }
             if locals_leq(&next, &header) && scry_octagon::leq(&next_oct, &header_oct) {
@@ -3265,6 +3276,24 @@ impl Interp<'_, '_> {
     }
 }
 
+/// FEAT-042: the widening thresholds for a function — its integer constant
+/// operands (the `i32.const` / `i64.const` immediates, where loop bounds and
+/// array sizes live) plus `0`, deduped and sorted. The loop-header widening
+/// snaps a runaway bound to the nearest enclosing threshold instead of ±∞.
+fn collect_widen_thresholds(ops: &[Operator<'_>]) -> Vec<i64> {
+    let mut ts: Vec<i64> = alloc::vec![0];
+    for op in ops {
+        match op {
+            Operator::I32Const { value } => ts.push(*value as i64),
+            Operator::I64Const { value } => ts.push(*value),
+            _ => {}
+        }
+    }
+    ts.sort_unstable();
+    ts.dedup();
+    ts
+}
+
 #[allow(clippy::too_many_arguments)]
 fn run_function_body(
     func: &DefinedFunc<'_>,
@@ -3281,6 +3310,7 @@ fn run_function_body(
     let ops = &func.ops;
     let end_at = build_end_map(ops);
     let want_points = emit_points.is_some();
+    let widen_thresholds = collect_widen_thresholds(ops);
     let mut interp = Interp {
         ops,
         end_at: &end_at,
@@ -3291,6 +3321,7 @@ fn run_function_body(
         diagnostics,
         call_graph,
         points: Vec::new(),
+        widen_thresholds,
     };
     let mut labels: Vec<Label> = Vec::new();
     interp.seq(0, ops.len(), &mut ctx, &mut labels, want_points)?;

crates/scry-interval/src/lib.rs

@@ -131,6 +131,44 @@ pub fn widen(a: Interval, b: Interval) -> Interval {
     Interval { lo, hi }
 }
 
+/// FEAT-042: widening WITH THRESHOLDS. Like [`widen`], but when a bound would
+/// jump to ±∞ it instead snaps to the nearest enclosing `threshold` — the
+/// greatest threshold ≤ `b.lo` for the lower bound, the least threshold ≥ `b.hi`
+/// for the upper — falling back to ±∞ when no threshold encloses. Recovers loop
+/// bounds plain widening over-approximates to ⊤ (a counter that stays `< 16`
+/// snaps to a `16` threshold, not ∞). Sound: the result still ⊒ `a` and ⊒ `b`
+/// (a genuine widening), and termination holds because the threshold set is
+/// finite — each jump moves strictly up the finite ladder `{thresholds} ∪ {±∞}`.
+pub fn widen_with_thresholds(a: Interval, b: Interval, thresholds: &[i64]) -> Interval {
+    if is_bot(a) {
+        return b;
+    }
+    if is_bot(b) {
+        return a;
+    }
+    let lo = if b.lo < a.lo {
+        thresholds
+            .iter()
+            .copied()
+            .filter(|&t| t <= b.lo)
+            .max()
+            .unwrap_or(i64::MIN)
+    } else {
+        a.lo
+    };
+    let hi = if b.hi > a.hi {
+        thresholds
+            .iter()
+            .copied()
+            .filter(|&t| t >= b.hi)
+            .min()
+            .unwrap_or(i64::MAX)
+    } else {
+        a.hi
+    };
+    Interval { lo, hi }
+}
+
 pub fn constant_i32(c: i32) -> Interval {
     Interval {
         lo: c as i64,
@@ -310,6 +348,46 @@ pub fn region_widen(a: Region, b: Region) -> Region {
 mod tests {
     use super::*;
 
+    /// FEAT-042: threshold widening snaps a growing upper bound to the nearest
+    /// enclosing threshold instead of +∞, stays a sound widening (⊒ both inputs),
+    /// and terminates (reaches a fixed point at/within the threshold ladder).
+    #[test]
+    fn widen_with_thresholds_snaps_and_terminates() {
+        let thr = [8i64, 16, 64];
+        // [0,3] ⊔widen [0,5] : hi grew → snap to least threshold ≥ 5 = 8.
+        let w = widen_with_thresholds(Interval { lo: 0, hi: 3 }, Interval { lo: 0, hi: 5 }, &thr);
+        assert_eq!(w, Interval { lo: 0, hi: 8 }, "should snap to 8, not ∞");
+        // soundness: result contains both inputs.
+        for z in 0..=8 {
+            assert!(gamma(w, z));
+        }
+        assert!(gamma(w, 5) && gamma(w, 3));
+        // plain widen would have gone to +∞.
+        assert_eq!(
+            widen(Interval { lo: 0, hi: 3 }, Interval { lo: 0, hi: 5 }).hi,
+            i64::MAX
+        );
+        // termination: widening the snapped value against a still-growing body
+        // climbs the ladder 8 → 16 → 64 → ∞ and stops; never oscillates.
+        let mut acc = Interval { lo: 0, hi: 0 };
+        let mut prev = acc;
+        for step in 1..200 {
+            let body = Interval { lo: 0, hi: step };
+            acc = widen_with_thresholds(acc, body, &thr);
+            assert!(leq(prev, acc), "widening must be ascending");
+            prev = acc;
+        }
+        // After enough growth past the top threshold, it reaches ∞ — finite chain.
+        assert_eq!(acc.hi, i64::MAX);
+        // No threshold encloses → falls back to ±∞ (still sound).
+        let w2 = widen_with_thresholds(
+            Interval { lo: 0, hi: 100 },
+            Interval { lo: 0, hi: 200 },
+            &thr,
+        );
+        assert_eq!(w2.hi, i64::MAX);
+    }
+
     /// γ: does concrete `z` lie in the interval?
     fn gamma(a: Interval, z: i64) -> bool {
         !is_bot(a) && a.lo <= z && z <= a.hi