wpfacts: interval rule results are not widened, and a counter write on a leaving path keeps the narrowed reads (R1 range tightening)

changelog.d/wpfacts-range-tightening.md

@@ -0,0 +1 @@
+Performance: two integer-interval looseness causes in the whole-program facts are gone. The result of an interval rule (`a + b`, `r * 16 + f`, a loop test's clip) is now the rule over its operands' intervals and is no longer widened on its own: only copy targets (a loop counter, a `let`) climb the widening ladder and the loop test clips them back, so `r * 16 + f` over two counters in `[0, 7]` is `[0, 119]` instead of `[0, 255]`, and `r + f` is `[0, 14]` instead of `[0, 127]`. A write of a narrowed counter in a branch that always leaves (`if ((sq & 0x88) !== 0) { sq += 7; continue; }`) no longer ends the counter's narrowed reads after the branch, when every way out of the branch lands outside the narrowed code: an unlabeled `break` or `continue` with no loop or `switch` in between, a `return` or `throw` with no `try` in between; a labeled jump, or a write that falls through to a read, keeps the read wide. Field read calls such as `this.at(r * 16 + f)` and `this.at(sq)` on a 0x88 board are then in the board's floor. `PERRY_FACTS_EXACT_RULES=0` and `PERRY_FACTS_LEAVING_WRITES=0` turn each off; `PERRY_FACTS_SABOTAGE=exactrule` and `leavingwrite` are the negative controls.

crates/perry-wpfacts/src/gen.rs

@@ -368,6 +368,20 @@ pub struct Gen<'a> {
     /// Guards narrow locals by presence: a truthy or non-nullish test
     /// filters out `null`/`undefined` (`FactsConfig::no_guard_presence`).
     pub guard_presence: bool,
+    /// R1: a write of a narrowed local in a branch that always leaves past
+    /// the narrowing's code does not end its narrowed reads after the branch
+    /// (`gen::narrow`, "Writes on a leaving path";
+    /// `FactsConfig::no_leaving_writes`).
+    pub leaving_writes: bool,
+    /// Negative control (`PERRY_FACTS_SABOTAGE=leavingwrite`): every
+    /// branch's writes are dropped from the reads after it, also a branch
+    /// that falls through to them.
+    pub leaving_write_sabotage: bool,
+    /// The loops and `switch`es (`jumps`) and `try` statements (`tries`)
+    /// the walk is inside: where an unlabeled `break`/`continue` lands, and
+    /// whether a `throw` or a `finally` stays inside a narrowing's code.
+    pub jumps: u32,
+    pub tries: u32,
     /// The `import()` / `require(expr)` specifiers of the bodies walked, by
     /// module (`live_dynamic_imports`): in the activation pass, the sites a
     /// body that can run holds.
@@ -694,6 +708,10 @@ impl<'a> Gen<'a> {
             new_array_site: None,
             guard_ranges: true,
             guard_presence: true,
+            leaving_writes: true,
+            leaving_write_sabotage: false,
+            jumps: 0,
+            tries: 0,
             dynimport_seen: Default::default(),
             dynamic_only: Default::default(),
             roots: Vec::new(),

crates/perry-wpfacts/src/gen/narrow.rs

@@ -35,6 +35,27 @@
 //! The bound is a literal, a local, or a local's `length` (an Array's
 //! carries its length interval, `solve::arr_len`).
 //!
+//! ## Writes on a leaving path
+//!
+//! A write ends the start reads for the code it can reach, not for the
+//! program text after it. A branch of an `if` that always leaves
+//! (`always_exits`) reaches the code after the `if` only through its jumps,
+//! so after the branch each narrowing's `written` is what it was before it
+//! when every way out of the branch lands outside the narrowing's code
+//! (`jumps_leave`):
+//! - an unlabeled `break`/`continue` out of the branch, with no loop or
+//!   `switch` between the `if` and the narrowing (`Gen::jumps`): it lands at
+//!   the narrowed loop's update (which reads the end node) or past the
+//!   guarded code;
+//! - a `return` or `throw`, and any exception, with no `try` between them
+//!   (`Gen::tries`): no `catch` or `finally` of the narrowing's code runs
+//!   after it;
+//! - no labeled jump (where it lands is not followed).
+//!
+//! The write still reaches the end node and the local, so the update and
+//! every read the jump reaches see it. `PERRY_FACTS_LEAVING_WRITES=0` ends
+//! the start reads at the first write in the text again.
+//!
 //! The rule only applies where no other code can write `i` during the loop:
 //! `i` is declared by the loop's `init` and no closure appears in the loop.
 //! A nested loop that writes `i` ends the start reads before it (its body
@@ -55,6 +76,10 @@ pub(crate) struct Narrow {
     /// The update is walked: it reads the end node, and its write (which
     /// runs after the body) reaches only the counter.
     in_update: bool,
+    /// `Gen::jumps` and `Gen::tries` where the narrowed code starts (for a
+    /// loop, inside it): "Writes on a leaving path".
+    jumps: u32,
+    tries: u32,
 }
 
 fn expr_has(e: &Expr, p: &mut impl FnMut(&Expr) -> bool) -> bool {
@@ -160,6 +185,8 @@ impl<'a> Gen<'a> {
             end,
             written: false,
             in_update: false,
+            jumps: self.jumps,
+            tries: self.tries,
         });
         true
     }
@@ -205,6 +232,34 @@ impl<'a> Gen<'a> {
         }
     }
 
+    /// Before walking a branch of an `if`: each narrowing's `written`.
+    pub(crate) fn narrow_snapshot(&self) -> Vec<bool> {
+        if !self.leaving_writes {
+            return Vec::new();
+        }
+        self.narrow.iter().map(|n| n.written).collect()
+    }
+
+    /// After walking `branch` (`pre` from `narrow_snapshot` before it): a
+    /// write in a branch that always leaves past a narrowing's code does
+    /// not reach the reads after the `if` (module docs, "Writes on a
+    /// leaving path").
+    pub(crate) fn narrow_leave(&mut self, branch: &[Stmt], pre: Vec<bool>) {
+        if pre.is_empty() {
+            return;
+        }
+        let sabotage = self.leaving_write_sabotage;
+        if !sabotage && !(always_exits(branch) && jumps_leave(branch)) {
+            return;
+        }
+        let (f, jumps, tries) = (self.m.cur_fn, self.jumps, self.tries);
+        for (n, w) in self.narrow.iter_mut().zip(pre) {
+            if n.f == f && (sabotage || (n.jumps == jumps && n.tries == tries)) {
+                n.written = w;
+            }
+        }
+    }
+
     /// Before walking a nested loop: a narrowed counter it writes is read
     /// through the end node inside it (a read there may follow the write).
     pub(crate) fn narrow_enter_loop(&mut self, s: &Stmt) {
@@ -437,6 +492,37 @@ pub(crate) fn always_exits(ss: &[Stmt]) -> bool {
     )
 }
 
+/// Whether every jump out of `ss` lands where an unlabeled jump at the
+/// statement around `ss` lands, or leaves the function: no labeled `break`
+/// or `continue` (where it lands is not followed). A `break` inside a loop
+/// or `switch` of `ss`, and a `continue` inside a loop of it, stay in `ss`.
+/// Nested function bodies are expressions: not walked.
+pub(crate) fn jumps_leave(ss: &[Stmt]) -> bool {
+    ss.iter().all(|s| match s {
+        Stmt::LabeledBreak(_) | Stmt::LabeledContinue(_) => false,
+        Stmt::If {
+            then_branch,
+            else_branch,
+            ..
+        } => jumps_leave(then_branch) && else_branch.as_deref().is_none_or(jumps_leave),
+        Stmt::While { body, .. } | Stmt::DoWhile { body, .. } | Stmt::For { body, .. } => {
+            jumps_leave(body)
+        }
+        Stmt::Switch { cases, .. } => cases.iter().all(|c| jumps_leave(&c.body)),
+        Stmt::Try {
+            body,
+            catch,
+            finally,
+        } => {
+            jumps_leave(body)
+                && catch.as_ref().is_none_or(|c| jumps_leave(&c.body))
+                && finally.as_deref().is_none_or(jumps_leave)
+        }
+        Stmt::Labeled { body, .. } => jumps_leave(std::slice::from_ref(body)),
+        _ => true,
+    })
+}
+
 /// Whether running `ss` may reach its end: a function body that does
 /// returns `undefined` there. Conservative: a `return` or `throw` on every
 /// path (through `if`/`else`, `try`, a `switch` with a `default` and an
@@ -929,6 +1015,8 @@ impl<'a> Gen<'a> {
                 end,
                 written: false,
                 in_update: false,
+                jumps: self.jumps,
+                tries: self.tries,
             });
             pushed += 1;
         }

crates/perry-wpfacts/src/gen/walk.rs

@@ -1213,34 +1213,44 @@ impl<'a> Gen<'a> {
                     guard: Some((t, then_test)),
                     ..fx.clone()
                 };
+                // A branch that always leaves: its writes reach only where
+                // it jumps to (`narrow_leave`).
+                let pre = self.narrow_snapshot();
                 let k = self.narrow_guard(fx, condition, true);
                 self.stmts(&then_fx, then_branch);
                 self.narrow_pop(k);
+                self.narrow_leave(then_branch, pre);
                 self.own_guard_done(own);
                 if let Some(e) = else_branch {
                     let else_fx = Fx {
                         guard: Some((t, else_test)),
                         ..fx.clone()
                     };
+                    let pre = self.narrow_snapshot();
                     let k = self.narrow_guard(fx, condition, false);
                     self.stmts(&else_fx, e);
                     self.narrow_pop(k);
+                    self.narrow_leave(e, pre);
                 }
             }
             Stmt::While { condition, body } => {
                 self.narrow_enter_loop(s);
                 self.loop_depth += 1;
+                self.jumps += 1;
                 let _ = self.expr(fx, condition);
                 let k = self.narrow_guard(fx, condition, true);
                 self.stmts(fx, body);
                 self.narrow_pop(k);
+                self.jumps -= 1;
                 self.loop_depth -= 1;
             }
             Stmt::DoWhile { body, condition } => {
                 self.narrow_enter_loop(s);
                 self.loop_depth += 1;
+                self.jumps += 1;
                 let _ = self.expr(fx, condition);
                 self.stmts(fx, body);
+                self.jumps -= 1;
                 self.loop_depth -= 1;
             }
             Stmt::For {
@@ -1254,6 +1264,7 @@ impl<'a> Gen<'a> {
                     self.stmt(fx, i);
                 }
                 self.loop_depth += 1;
+                self.jumps += 1;
                 if let Some(c) = condition {
                     let _ = self.expr(fx, c);
                 }
@@ -1281,6 +1292,7 @@ impl<'a> Gen<'a> {
                 if narrowed {
                     self.narrow_end();
                 }
+                self.jumps -= 1;
                 self.loop_depth -= 1;
             }
             Stmt::Labeled { body, .. } => self.stmt(fx, body),
@@ -1310,6 +1322,7 @@ impl<'a> Gen<'a> {
                 // finally run in the enclosing one.
                 let rt = self.m.node_l("RAISE-try");
                 let outer = std::mem::replace(&mut self.m.gen_region, Some(rt));
+                self.tries += 1;
                 self.stmts(fx, body);
                 self.m.gen_region = outer;
                 if let Some(c) = catch {
@@ -1326,13 +1339,15 @@ impl<'a> Gen<'a> {
                 if let Some(f) = finally {
                     self.stmts(fx, f);
                 }
+                self.tries -= 1;
             }
             Stmt::Switch {
                 discriminant,
                 cases,
             } => {
                 let d = self.expr(fx, discriminant);
                 // `===` against case values: no coercion.
+                self.jumps += 1;
                 for c in cases {
                     if let Some(t) = &c.test {
                         let tv = self.expr(fx, t);
@@ -1341,6 +1356,7 @@ impl<'a> Gen<'a> {
                     }
                     self.stmts(fx, &c.body);
                 }
+                self.jumps -= 1;
             }
         }
     }

crates/perry-wpfacts/src/lib.rs

@@ -94,6 +94,14 @@ pub struct FactsConfig {
     /// No `Rep::Arr` for a field and no in-floor field read call
     /// (`PERRY_FACTS_ARRAY_FIELDS=0`, DESIGN-p4l1 PR-C3).
     pub no_array_fields: bool,
+    /// R1: a `Cons::Range` result widens like any node again, after
+    /// `WIDEN_STEPS` growths (`PERRY_FACTS_EXACT_RULES=0`;
+    /// `solve::grow_rule_range`).
+    pub no_exact_rules: bool,
+    /// R1: a write of a narrowed local in a branch that always leaves ends
+    /// the narrowed reads after the branch again (`PERRY_FACTS_LEAVING_WRITES=0`;
+    /// `gen::narrow`, "Writes on a leaving path").
+    pub no_leaving_writes: bool,
     /// An element read's past-the-end `undefined` is unconditional again
     /// (`PERRY_FACTS_ELEM_UNDEF=0`, PR-C1: `Cons::ElemUndef`).
     pub no_elem_undef: bool,
@@ -497,6 +505,10 @@ fn generate<'a>(
     g.m.arr_const_sabotage = cfg.sabotage.as_deref() == Some("arrconst");
     g.m.array_fields = !cfg.no_array_fields;
     g.m.arr_field_sabotage = cfg.sabotage.as_deref() == Some("arrfield");
+    g.m.exact_rules = !cfg.no_exact_rules;
+    g.m.exact_rule_sabotage = cfg.sabotage.as_deref() == Some("exactrule");
+    g.leaving_writes = !cfg.no_leaving_writes;
+    g.leaving_write_sabotage = cfg.sabotage.as_deref() == Some("leavingwrite");
     g.int_ranges = !cfg.no_int_ranges;
     g.arr_lengths = g.int_ranges && !cfg.no_array_lengths;
     g.guard_ranges = g.int_ranges && !cfg.no_guard_ranges;

crates/perry-wpfacts/src/model.rs

@@ -1261,6 +1261,14 @@ pub struct Model {
     /// `+` interval rule drops its right operand, a wrong transfer the
     /// int32 witnesses must catch.
     pub range_sabotage: bool,
+    /// R1: a `Cons::Range` result takes the join of its rule's evaluations
+    /// without widening (`solve::grow_rule_range`); only copy targets widen.
+    /// `PERRY_FACTS_EXACT_RULES=0` widens a result like any node.
+    pub exact_rules: bool,
+    /// Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): with the exact
+    /// rule results, a sum is the hull of its operands instead of their
+    /// sum, a claim too narrow that the witnesses must catch.
+    pub exact_rule_sabotage: bool,
     /// Negative control (`PERRY_FACTS_SABOTAGE=arrlen`): every index store
     /// counts as one inside its array's birth length (`arr_len_index`).
     pub arr_len_sabotage: bool,

crates/perry-wpfacts/src/solve.rs

@@ -1975,3 +1975,36 @@ pub(crate) fn grow_range(node: &mut Node, iv: Iv) -> bool {
     node.drange = true;
     true
 }
+
+/// Join `iv` into the result of a [`Cons::Range`] rule (R1, sum widening).
+///
+/// The rule's result is `op` over its operands' intervals at each
+/// evaluation, and every operand only grows, so the join is the rule over
+/// the operands' last intervals: a rule result needs no widening of its own.
+/// The operands are what widen: a loop counter (a copy target, `grow_range`)
+/// climbs the ladder and the loop test clips it back (`gen::narrow`), so
+/// `r * 16 + f` over `r, f` in `[0, 7]` is `[0, 119]`, where widening the
+/// sum after `WIDEN_STEPS` of its operands' growths jumped to a rung (127,
+/// then 255).
+///
+/// Termination: the rule results form no cycle among themselves (each
+/// rule's operands exist before its result node is ruled, and a result has
+/// one rule), so every cycle passes a copy target, which widens, and a
+/// result grows at most once per operand growth. Past `WIDEN_LIMIT` growths
+/// it still climbs the ladder (a backstop that bounds even a cycle the
+/// argument missed).
+pub(crate) fn grow_rule_range(node: &mut Node, iv: Iv) -> bool {
+    use crate::model::range::{widen, WIDEN_LIMIT};
+    let joined = node.range.join(iv);
+    if joined == node.range {
+        return false;
+    }
+    node.rsteps = node.rsteps.saturating_add(1);
+    node.range = if node.rsteps > WIDEN_LIMIT {
+        widen(node.range, joined)
+    } else {
+        joined
+    };
+    node.drange = true;
+    true
+}

crates/perry-wpfacts/src/solve/apply.rs

@@ -1511,14 +1511,24 @@ impl Model {
                     let (l, r) = if right { (ot, me) } else { (me, ot) };
                     if self.range_sabotage && op == RangeOp::Add {
                         l
+                    } else if self.exact_rule_sabotage && op == RangeOp::Add {
+                        // Negative control (`exactrule`): a sum is the hull
+                        // of its operands, not their sum.
+                        l.join(r)
                     } else {
                         self.const_numbers
                             .then(|| crate::model::range::eval_exact(op, l, r))
                             .flatten()
                             .unwrap_or_else(|| crate::model::range::eval(op, l, r))
                     }
                 };
-                if crate::solve::grow_range(&mut self.nodes[dst as usize], iv) {
+                let d = &mut self.nodes[dst as usize];
+                let grew = if self.exact_rules {
+                    crate::solve::grow_rule_range(d, iv)
+                } else {
+                    crate::solve::grow_range(d, iv)
+                };
+                if grew {
                     let d = &mut self.nodes[dst as usize];
                     if !d.in_wl {
                         d.in_wl = true;

crates/perry-wpfacts/src/tests.rs

@@ -148,6 +148,7 @@ mod proto_lock_keys;
 mod proto_value;
 mod protocol_calls;
 mod protocol_keys;
+mod range_tightening;
 mod reach_accessor;
 mod receiver_slots;
 mod receiver_this;