From 5c74e1a286d1d2de95995aec41b15d2ff5ed6e14 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 08:45:45 +0100 Subject: [PATCH 01/14] 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 | 1 + crates/perry-wpfacts/src/gen.rs | 18 ++ crates/perry-wpfacts/src/gen/narrow.rs | 88 ++++++++++ crates/perry-wpfacts/src/gen/walk.rs | 16 ++ crates/perry-wpfacts/src/lib.rs | 12 ++ crates/perry-wpfacts/src/model.rs | 8 + crates/perry-wpfacts/src/solve.rs | 38 ++++ crates/perry-wpfacts/src/solve/apply.rs | 8 +- crates/perry-wpfacts/src/tests.rs | 1 + .../src/tests/range_tightening.rs | 160 +++++++++++++++++ .../perry/src/commands/compile/compile_env.rs | 2 + .../src/commands/compile/compile_env/tests.rs | 13 ++ .../src/commands/compile/program_facts.rs | 16 ++ scripts/test-verify-facts-s0.py | 2 + .../verify_facts_s0/leaving-write-negative.ts | 26 +++ scripts/verify_facts_s0/range-sum-negative.ts | 20 +++ .../language/array/test_range_tightening.ts | 165 ++++++++++++++++++ 17 files changed, 593 insertions(+), 1 deletion(-) create mode 100644 changelog.d/wpfacts-range-tightening.md create mode 100644 crates/perry-wpfacts/src/tests/range_tightening.rs create mode 100644 scripts/verify_facts_s0/leaving-write-negative.ts create mode 100644 scripts/verify_facts_s0/range-sum-negative.ts create mode 100644 tests/parity/language/array/test_range_tightening.ts diff --git a/changelog.d/wpfacts-range-tightening.md b/changelog.d/wpfacts-range-tightening.md new file mode 100644 index 00000000000..763146a4a13 --- /dev/null +++ b/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. diff --git a/crates/perry-wpfacts/src/gen.rs b/crates/perry-wpfacts/src/gen.rs index a444310db8b..95d0ef7a8ed 100644 --- a/crates/perry-wpfacts/src/gen.rs +++ b/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(), diff --git a/crates/perry-wpfacts/src/gen/narrow.rs b/crates/perry-wpfacts/src/gen/narrow.rs index fa3a38cd287..178c506f5b1 100644 --- a/crates/perry-wpfacts/src/gen/narrow.rs +++ b/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 { + 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) { + 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; } diff --git a/crates/perry-wpfacts/src/gen/walk.rs b/crates/perry-wpfacts/src/gen/walk.rs index 02fa4444565..b2937576083 100644 --- a/crates/perry-wpfacts/src/gen/walk.rs +++ b/crates/perry-wpfacts/src/gen/walk.rs @@ -1206,34 +1206,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 { @@ -1247,6 +1257,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); } @@ -1274,6 +1285,7 @@ impl<'a> Gen<'a> { if narrowed { self.narrow_end(); } + self.jumps -= 1; self.loop_depth -= 1; } Stmt::Labeled { body, .. } => self.stmt(fx, body), @@ -1303,6 +1315,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 { @@ -1319,6 +1332,7 @@ impl<'a> Gen<'a> { if let Some(f) = finally { self.stmts(fx, f); } + self.tries -= 1; } Stmt::Switch { discriminant, @@ -1327,12 +1341,14 @@ impl<'a> Gen<'a> { let d = self.expr(fx, discriminant); // `===` against case values: no coercion. let _ = d; + self.jumps += 1; for c in cases { if let Some(t) = &c.test { let _ = self.expr(fx, t); } self.stmts(fx, &c.body); } + self.jumps -= 1; } } } diff --git a/crates/perry-wpfacts/src/lib.rs b/crates/perry-wpfacts/src/lib.rs index df839dc2c68..d96d71080b6 100644 --- a/crates/perry-wpfacts/src/lib.rs +++ b/crates/perry-wpfacts/src/lib.rs @@ -90,6 +90,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, @@ -488,6 +496,10 @@ fn generate<'a>( g.m.arr_front_sabotage = cfg.sabotage.as_deref() == Some("arrfront"); 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; diff --git a/crates/perry-wpfacts/src/model.rs b/crates/perry-wpfacts/src/model.rs index ff608963fd4..b87551cee15 100644 --- a/crates/perry-wpfacts/src/model.rs +++ b/crates/perry-wpfacts/src/model.rs @@ -1259,6 +1259,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`): a rule result + /// keeps its first interval, a claim too narrow for the values its + /// operands grow to, which 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, diff --git a/crates/perry-wpfacts/src/solve.rs b/crates/perry-wpfacts/src/solve.rs index 37a7f7a732f..d8f1482999a 100644 --- a/crates/perry-wpfacts/src/solve.rs +++ b/crates/perry-wpfacts/src/solve.rs @@ -1929,3 +1929,41 @@ 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, sabotage: bool) -> bool { + use crate::model::range::{widen, WIDEN_LIMIT}; + // Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): the result keeps + // its first interval, whatever its operands grow to. + if sabotage && !node.range.is_empty() { + return false; + } + 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 +} diff --git a/crates/perry-wpfacts/src/solve/apply.rs b/crates/perry-wpfacts/src/solve/apply.rs index ca8fa1546c5..0595f933230 100644 --- a/crates/perry-wpfacts/src/solve/apply.rs +++ b/crates/perry-wpfacts/src/solve/apply.rs @@ -1487,7 +1487,13 @@ impl Model { .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, self.exact_rule_sabotage) + } 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; diff --git a/crates/perry-wpfacts/src/tests.rs b/crates/perry-wpfacts/src/tests.rs index c667ca327fb..eab85d6f9f7 100644 --- a/crates/perry-wpfacts/src/tests.rs +++ b/crates/perry-wpfacts/src/tests.rs @@ -143,6 +143,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; diff --git a/crates/perry-wpfacts/src/tests/range_tightening.rs b/crates/perry-wpfacts/src/tests/range_tightening.rs new file mode 100644 index 00000000000..0638efdca41 --- /dev/null +++ b/crates/perry-wpfacts/src/tests/range_tightening.rs @@ -0,0 +1,160 @@ +//! R1 (range tightening): a rule's result is not widened past the rule over +//! its operands (`solve::grow_rule_range`), and a counter write in a branch +//! that always leaves does not end the narrowed reads after it +//! (`gen::narrow`, "Writes on a leaving path"). Each verdict is read where it +//! is consumed: the key interval of a field read call (`at(k)` over a board +//! born dense with 128 elements) and whether it is in the floor. + +use super::*; + +/// `(call text, key interval, in floor)` of every field read call of `src`. +fn keys(src: &str, cfg: FactsConfig) -> Vec<(String, Option<(i64, i64)>, bool)> { + let pf = facts_with(src, cfg); + let mut out = Vec::new(); + for mb in &pf.bindings { + for (offset, c) in &mb.field_read_calls { + // Offsets are 1-based. + let rest = &src[*offset as usize - 1..]; + let end = rest.find(';').unwrap_or(rest.len()); + let key = mb + .call_arg_ranges + .binary_search_by_key(offset, |(o, _)| *o) + .ok() + .and_then(|at| mb.call_arg_ranges[at].1.get(c.index_arg as usize).copied()) + .flatten(); + out.push((rest[..end].to_string(), key, c.in_floor)); + } + } + out +} + +fn call(calls: &[(String, Option<(i64, i64)>, bool)], text: &str) -> (Option<(i64, i64)>, bool) { + let c = calls + .iter() + .find(|(t, ..)| t.starts_with(text)) + .unwrap_or_else(|| panic!("no call {text}: {calls:?}")); + (c.1, c.2) +} + +const BOARD: &str = "class B {\n\ + board: number[] = new Array(128).fill(0);\n\ + at(i: number): number { return this.board[i] ?? 0; }\n"; + +fn program(methods: &str, calls: &str) -> String { + format!("{BOARD}{methods}\n}}\nconst b = new B();\nconsole.log({calls});\n") +} + +/// The shapes of the C3 probe (qb9 c3/probe/rg): one method per key. +fn probe() -> String { + program( + " mulOnly(): number { let s = 0; for (let r = 0; r < 8; r++) s += this.at(r * 16); return s; }\n\ + mulAdd(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); return s; }\n\ + addOnly(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r + f); return s; }\n\ + down(): number { let s = 0; for (let r = 7; r >= 0; r--) for (let f = 0; f < 8; f++) s += this.at(r * 16 - f + 7); return s; }\n\ + skip(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 7; continue; } s += this.at(q + 0); } return s; }\n\ + plain(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) continue; s += this.at(q - 0); } return s; }\n\ + elseLeaves(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) === 0) { s += 1; } else { q += 7; continue; } s += this.at(q * 1); } return s; }", + "b.mulOnly(), b.mulAdd(), b.addOnly(), b.down(), b.skip(), b.plain(), b.elseLeaves()", + ) +} + +#[test] +fn a_sum_of_two_counters_is_their_hull() { + let calls = keys(&probe(), FactsConfig::default()); + assert_eq!(call(&calls, "this.at(r * 16)"), (Some((0, 112)), true)); + assert_eq!(call(&calls, "this.at(r * 16 + f)"), (Some((0, 119)), true)); + assert_eq!(call(&calls, "this.at(r + f)"), (Some((0, 14)), true)); + assert_eq!( + call(&calls, "this.at(r * 16 - f + 7)"), + (Some((0, 119)), true) + ); +} + +#[test] +fn a_write_in_a_branch_that_leaves_keeps_the_narrowed_reads() { + let calls = keys(&probe(), FactsConfig::default()); + assert_eq!(call(&calls, "this.at(q + 0)"), (Some((0, 127)), true)); + assert_eq!(call(&calls, "this.at(q - 0)"), (Some((0, 127)), true)); + assert_eq!(call(&calls, "this.at(q * 1)"), (Some((0, 127)), true)); +} + +#[test] +fn the_switches_off_give_the_widened_intervals_back() { + let rules_off = keys( + &probe(), + FactsConfig { + no_exact_rules: true, + ..Default::default() + }, + ); + let (k, _) = call(&rules_off, "this.at(r + f)"); + assert!(k.is_some_and(|(_, hi)| hi > 14), "{k:?}"); + let (k, in_floor) = call(&rules_off, "this.at(r * 16 + f)"); + assert!(k.is_some_and(|(_, hi)| hi > 127) && !in_floor, "{k:?}"); + let writes_off = keys( + &probe(), + FactsConfig { + no_leaving_writes: true, + ..Default::default() + }, + ); + let (k, in_floor) = call(&writes_off, "this.at(q + 0)"); + assert!(k.is_some_and(|(_, hi)| hi > 127) && !in_floor, "{k:?}"); + // A bare `continue` writes nothing: narrowed either way. + assert_eq!(call(&writes_off, "this.at(q - 0)"), (Some((0, 127)), true)); +} + +/// Negative controls: a write that reaches a later read keeps it wide. +fn reaching() -> String { + program( + " falls(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 7; } s += this.at(q + 0); } return s; }\n\ + inSwitch(k: number): number { let s = 0; for (let q = 0; q < 128; q++) { switch (k) { case 1: if (q > 3) { q += 200; break; } s += 1; } s += this.at(q - 0); } return s; }\n\ + inTry(): number { let s = 0; for (let q = 0; q < 128; q++) { try { if (q > 3) { q += 200; continue; } } finally { s += this.at(q * 1); } } return s; }\n\ + labeled(): number { let s = 0; outer: for (let q = 0; q < 128; q++) { if (q > 3) { q += 200; continue outer; } s += this.at(q | 0); } return s; }\n\ + sumPast(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f + 9); return s; }", + "b.falls(), b.inSwitch(1), b.inSwitch(2), b.inTry(), b.labeled(), b.sumPast()", + ) +} + +#[test] +fn a_write_that_reaches_a_later_read_keeps_it_wide() { + let calls = keys(&reaching(), FactsConfig::default()); + for (text, reach) in [ + // `q + 7` falls through to the read. + ("this.at(q + 0)", 134), + // The `break` lands after the `switch`, before the read. + ("this.at(q - 0)", 327), + // The `finally` runs after the `continue`. + ("this.at(q * 1)", 327), + // A labeled jump is not followed (conservative). + ("this.at(q | 0)", 327), + // The sum's hull is past the floor. + ("this.at(r * 16 + f + 9)", 128), + ] { + let (k, in_floor) = call(&calls, text); + assert!( + k.is_none_or(|(_, hi)| hi >= reach) && !in_floor, + "{text}: {k:?} {in_floor}" + ); + } +} + +#[test] +fn the_sabotage_arms_claim_a_read_in_the_floor_that_is_not() { + let leaving = keys( + &reaching(), + FactsConfig { + sabotage: Some("leavingwrite".into()), + ..Default::default() + }, + ); + assert!(call(&leaving, "this.at(q + 0)").1, "{leaving:?}"); + let exact = keys( + &reaching(), + FactsConfig { + sabotage: Some("exactrule".into()), + ..Default::default() + }, + ); + assert!(call(&exact, "this.at(r * 16 + f + 9)").1, "{exact:?}"); +} diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs index dd784b9a12c..5fdc3b42873 100644 --- a/crates/perry/src/commands/compile/compile_env.rs +++ b/crates/perry/src/commands/compile/compile_env.rs @@ -73,10 +73,12 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[ "PERRY_FACTS_CONST_LENGTH", "PERRY_FACTS_CONST_NUMBERS", "PERRY_FACTS_ELEM_UNDEF", + "PERRY_FACTS_EXACT_RULES", "PERRY_FACTS_FIELD_READ_CALLS", "PERRY_FACTS_CANONICAL_NUMBERS", "PERRY_FACTS_GUARD_PRESENCE", "PERRY_FACTS_GUARD_RANGES", + "PERRY_FACTS_LEAVING_WRITES", "PERRY_FACTS_SITE_ARGS", "PERRY_FACTS_SABOTAGE", "PERRY_FACTS_SUPPRESS_BIRTH", diff --git a/crates/perry/src/commands/compile/compile_env/tests.rs b/crates/perry/src/commands/compile/compile_env/tests.rs index ee554d4f850..3645665e5b1 100644 --- a/crates/perry/src/commands/compile/compile_env/tests.rs +++ b/crates/perry/src/commands/compile/compile_env/tests.rs @@ -346,3 +346,16 @@ fn const_number_switch_is_a_cache_input() { "PERRY_FACTS_CONST_NUMBERS must key the compile caches" ); } + +/// R1: the range-tightening switches change the facts' intervals (and with +/// them in-floor reads and int32 locals), so `=0` must never reuse an `=1` +/// object. +#[test] +fn range_tightening_switches_are_cache_inputs() { + for name in ["PERRY_FACTS_EXACT_RULES", "PERRY_FACTS_LEAVING_WRITES"] { + assert!( + COMPILE_ENV_VARS.contains(&name), + "{name} must key the compile caches" + ); + } +} diff --git a/crates/perry/src/commands/compile/program_facts.rs b/crates/perry/src/commands/compile/program_facts.rs index e6e253f60f9..a3262748c2c 100644 --- a/crates/perry/src/commands/compile/program_facts.rs +++ b/crates/perry/src/commands/compile/program_facts.rs @@ -151,6 +151,14 @@ pub(crate) fn run( std::env::var("PERRY_FACTS_ARRAY_FIELDS").as_deref(), Ok("0") | Ok("off") | Ok("false") ), + no_exact_rules: matches!( + std::env::var("PERRY_FACTS_EXACT_RULES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), + no_leaving_writes: matches!( + std::env::var("PERRY_FACTS_LEAVING_WRITES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), no_elem_undef: matches!( std::env::var("PERRY_FACTS_ELEM_UNDEF").as_deref(), Ok("0") | Ok("off") | Ok("false") @@ -896,6 +904,14 @@ pub(crate) fn activation( std::env::var("PERRY_FACTS_ARRAY_FIELDS").as_deref(), Ok("0") | Ok("off") | Ok("false") ), + no_exact_rules: matches!( + std::env::var("PERRY_FACTS_EXACT_RULES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), + no_leaving_writes: matches!( + std::env::var("PERRY_FACTS_LEAVING_WRITES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ), no_elem_undef: matches!( std::env::var("PERRY_FACTS_ELEM_UNDEF").as_deref(), Ok("0") | Ok("off") | Ok("false") diff --git a/scripts/test-verify-facts-s0.py b/scripts/test-verify-facts-s0.py index c925fbb5ad0..0047d8a4ddf 100644 --- a/scripts/test-verify-facts-s0.py +++ b/scripts/test-verify-facts-s0.py @@ -119,6 +119,8 @@ def oracle(source, *argv): ("array-front-negative", "arrfront", "array rep"), ("array-field-negative", "arrfield", "array rep"), ("array-b1-negative", "arrb1", "array rep"), + ("range-sum-negative", "exactrule", "array rep"), + ("leaving-write-negative", "leavingwrite", "array rep"), ("number-call-negative", "numbercall", "numeric result"), ("field-read-call-negative", "fieldreadcall", "field read call"), ("array-undef-negative", "arrundef", "element floor"), diff --git a/scripts/verify_facts_s0/leaving-write-negative.ts b/scripts/verify_facts_s0/leaving-write-negative.ts new file mode 100644 index 00000000000..a28ad65fa2f --- /dev/null +++ b/scripts/verify_facts_s0/leaving-write-negative.ts @@ -0,0 +1,26 @@ +// `at` is a field element read, and `board` is born dense with 16 +// elements. In `walk` the counter write `q += 20` is in a branch that falls +// through to the read, so the read's key reaches past the floor (its value +// is the `?? 0`). Under PERRY_FACTS_SABOTAGE=leavingwrite every branch's +// writes are dropped from the reads after it, so the facts claim the key is +// the loop test's `[0, 15]`, in the floor, and the call loads the slot with +// no bound. The element tier's witness must report the false proof at the +// key. +class Board { + board: number[] = new Array(16).fill(1); + at(sq: number): number { + return this.board[sq] ?? 0; + } + walk(n: number): number { + let s = 0; + for (let q = 0; q < 16; q++) { + if (q === n) { + q += 20; + } + s += this.at(q); + } + return s; + } +} +const b = new Board(); +console.log(b.walk(process.argv.length > 100 ? 99 : 5)); diff --git a/scripts/verify_facts_s0/range-sum-negative.ts b/scripts/verify_facts_s0/range-sum-negative.ts new file mode 100644 index 00000000000..4a5671fa7e3 --- /dev/null +++ b/scripts/verify_facts_s0/range-sum-negative.ts @@ -0,0 +1,20 @@ +// `at` is a field element read, and `board` is born dense with 64 +// elements. `sum` reads the keys `r * 16 + f` for `r, f` in `[0, 7]`: the +// hull `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. +// Under PERRY_FACTS_SABOTAGE=exactrule an interval rule's result keeps its +// first interval, so the facts claim the key is in the floor and the call +// loads the slot with no bound. The element tier's witness must report the +// false proof at the key. +class Board { + board: number[] = new Array(64).fill(1); + at(sq: number): number { + return this.board[sq] ?? 0; + } + sum(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); + return s; + } +} +const b = new Board(); +console.log(b.sum()); diff --git a/tests/parity/language/array/test_range_tightening.ts b/tests/parity/language/array/test_range_tightening.ts new file mode 100644 index 00000000000..dbbd9bcebe2 --- /dev/null +++ b/tests/parity/language/array/test_range_tightening.ts @@ -0,0 +1,165 @@ +// R1 (range tightening): keys whose intervals the facts now prove tighter, +// and the negative controls that must stay wide. Every read goes through +// `at`, a field read call (`this.board[i] ?? -1`) on a board born dense, so +// a key claimed in the floor that is not would read past the elements +// instead of giving -1. + +class Board { + board: number[]; + constructor(n: number) { + this.board = new Array(n).fill(0); + for (let i = 0; i < n; i++) this.board[i] = (i * 7) % 13; + } + at(i: number): number { + return this.board[i] ?? -1; + } + + // (a) sums of two counters: the hull, not the widened sum. + rankFile(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); + return s; + } + diagonal(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r + f); + return s; + } + window(file: number): number { + let s = 0; + for (let r = 1; r >= 0 && r < 8; r++) { + for (let f = Math.max(0, file - 1); f <= Math.min(7, file + 1); f++) s += this.at(r * 16 + f); + } + return s; + } + // Negative control: the hull is past a 128 floor; the last keys are -1. + pastHull(): number { + let s = 0; + for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f + 9); + return s; + } + + // (b) a counter write in a branch that leaves. + skip(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if ((q & 0x88) !== 0) { q += 7; continue; } + s += this.at(q); + } + return s; + } + skipElse(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if ((q & 0x88) === 0) { s += 1; } else { q += 7; continue; } + s += this.at(q); + } + return s; + } + skipReturn(stop: number): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if (q === stop) { q += 500; return s + this.at(q); } + s += this.at(q); + } + return s; + } + skipBreak(stop: number): number { + let s = 0; + let q = 0; + for (q = 0; q < 128; q++) { + if (q === stop) { q += 500; break; } + s += this.at(q); + } + return s * 1000 + this.at(q); + } + guarded(x: number): number { + if (x < 100) { + if (x === 42) { x += 1000; return this.at(x); } + return this.at(x); + } + return -7; + } + + // Negative controls: the write reaches a later read. + falls(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + if ((q & 0x88) !== 0) { q += 7; } + s += this.at(q) + 2; + } + return s; + } + inSwitch(k: number): number { + let s = 0; + for (let q = 0; q < 128; q++) { + switch (k) { + case 1: + if (q > 100) { q += 200; break; } + s += 1; + } + s += this.at(q); + } + return s; + } + inTry(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + try { + if (q > 100) { q += 200; continue; } + } finally { + s += this.at(q); + } + } + return s; + } + inCatch(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + try { + if (q > 100) { q += 200; throw new Error("x"); } + } catch (e) { + s += this.at(q) * 3; + } + } + return s; + } + labeled(): number { + let s = 0; + outer: for (let q = 0; q < 128; q++) { + if (q > 100) { q += 200; continue outer; } + s += this.at(q); + } + return s; + } + innerLoop(): number { + let s = 0; + for (let q = 0; q < 128; q++) { + for (let j = 0; j < 2; j++) { + if (q > 100 && j === 1) { q += 200; continue; } + s += this.at(q); + } + s += this.at(q); + } + return s; + } + guardedLoop(x: number): number { + let s = 0; + if (x < 100) { + for (let j = 0; j < 3; j++) { + if (j === 1) { x += 1000; break; } + } + s += this.at(x); + } + return s; + } +} + +const b = new Board(128); +console.log(b.rankFile(), b.diagonal(), b.window(0), b.window(3), b.window(7), b.pastHull()); +console.log(b.skip(), b.skipElse(), b.skipReturn(40), b.skipReturn(999), b.skipBreak(17), b.skipBreak(999)); +console.log(b.guarded(5), b.guarded(42), b.guarded(150)); +console.log(b.falls(), b.inSwitch(1), b.inSwitch(2), b.inTry(), b.inCatch(), b.labeled(), b.innerLoop()); +console.log(b.guardedLoop(3), b.guardedLoop(120)); +const small = new Board(64); +console.log(small.rankFile(), small.diagonal(), small.skip(), small.falls()); From b6a30cbe80edad0561d82d5b3de3716f5aea7d58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 08:49:32 +0100 Subject: [PATCH 02/14] codegen: a loop that reads a field-held Array on every iteration holds its element base (P4 lever 1, PR-D) --- changelog.d/codegen-array-field-loop-base.md | 1 + crates/perry-codegen/src/collectors/mod.rs | 2 +- .../src/collectors/receiver_regions.rs | 106 +++- crates/perry-codegen/src/expr/index_get.rs | 1 + .../src/expr/index_get/field_base.rs | 316 ++++++++++ .../src/lower_call/field_read_call.rs | 27 +- crates/perry-codegen/src/stmt/field_base.rs | 552 ++++++++++++++++++ .../src/stmt/field_base_tests.rs | 261 +++++++++ crates/perry-codegen/src/stmt/loops.rs | 45 +- crates/perry-codegen/src/stmt/mod.rs | 3 + .../perry/src/commands/compile/compile_env.rs | 1 + .../src/commands/compile/compile_env/tests.rs | 1 + scripts/test-verify-facts-s0.py | 2 + .../array-base-admit-negative.ts | 25 + .../verify_facts_s0/array-base-negative.ts | 24 + .../array/test_array_reps_loop_base.ts | 133 +++++ .../array/test_array_reps_loop_base_gc.ts | 33 ++ 17 files changed, 1517 insertions(+), 16 deletions(-) create mode 100644 changelog.d/codegen-array-field-loop-base.md create mode 100644 crates/perry-codegen/src/expr/index_get/field_base.rs create mode 100644 crates/perry-codegen/src/stmt/field_base.rs create mode 100644 crates/perry-codegen/src/stmt/field_base_tests.rs create mode 100644 scripts/verify_facts_s0/array-base-admit-negative.ts create mode 100644 scripts/verify_facts_s0/array-base-negative.ts create mode 100644 tests/parity/language/array/test_array_reps_loop_base.ts create mode 100644 tests/parity/language/array/test_array_reps_loop_base_gc.ts diff --git a/changelog.d/codegen-array-field-loop-base.md b/changelog.d/codegen-array-field-loop-base.md new file mode 100644 index 00000000000..888936bd4d6 --- /dev/null +++ b/changelog.d/codegen-array-field-loop-base.md @@ -0,0 +1 @@ +Performance: a loop that reads an Array held in a field of `this` on every iteration holds the Array's element base across the loop. When a field read call (`this.at(sq)` = `this.board[sq] ?? 0`) whose field is a dense whole-program `Arr` runs on every path to the loop's back edge, and nothing else in the loop can collect, call, store or allocate (its back-edge poll is the one region ender), the loop's guarded preheader loads `this.board` once, resolves a growth forwarding stub to the live head once, and keeps the head: each read in the loop is then one load at `base + 24 + 8 * i`, with no field reload, no pointer masking and no forwarding test. A read whose key can leave the call's floor tests the key against the dense floor and otherwise keeps its own read, after which the base is re-derived. The poll's slow block re-derives the base from `this`'s root after a collection. There is no second loop body. `PERRY_FACTS_ARRAY_BASE=0` turns it off; `PERRY_VERIFY_FACTS=1` tests the head at the install and at every refresh, and at every read that the held base is the live head; `PERRY_FACTS_SABOTAGE=arrbase` and `arrbaseadm` are the negative controls; `PERRY_ARRAY_BASE_DIAG=1` prints the installer's verdict per loop. diff --git a/crates/perry-codegen/src/collectors/mod.rs b/crates/perry-codegen/src/collectors/mod.rs index 4edabfcc5ff..c0ddf95c622 100644 --- a/crates/perry-codegen/src/collectors/mod.rs +++ b/crates/perry-codegen/src/collectors/mod.rs @@ -148,7 +148,7 @@ pub(crate) use ptr_shape_callbacks::collect_array_callback_shapes; pub(crate) use ptr_shape_returns::collect_exported_return_shapes; pub(crate) use receiver_regions::{region_enders_in_expr, region_enders_in_stmts_classified}; pub(crate) use receiver_regions::{ - region_enders_in_stmts_with_trusted_operations, ByteViewParamAccess, + region_enders_in_stmts_with_trusted_operations, ByteViewParamAccess, FieldBase, ReceiverArrayValidationKind, ReceiverDescriptorTable, RegionEnder, }; pub(crate) use refs::{ diff --git a/crates/perry-codegen/src/collectors/receiver_regions.rs b/crates/perry-codegen/src/collectors/receiver_regions.rs index c31a87373d0..d35470e5fc4 100644 --- a/crates/perry-codegen/src/collectors/receiver_regions.rs +++ b/crates/perry-codegen/src/collectors/receiver_regions.rs @@ -390,6 +390,27 @@ enum ActiveReceiverData { PackedF64Loop(PackedF64LoopFact), MaskedWindowArray(MaskedWindowArrayFact), BufferView(BufferViewSlot), + /// PR-D (DESIGN-p4l1 §4.3): the element base of `this.` held + /// across a loop (`stmt::field_base`). + FieldBase(FieldBase), +} + +/// The element base of the Array in `this.`, held across a loop +/// whose only region ender is its back-edge poll (`stmt::field_base`). +/// +/// `base_slot` is an `i64` slot holding the live (never forwarded) head's +/// handle; element `i` is at `base + 24 + 8 * i`. It is an address, so it +/// is believed only under the poll's refresh recipe: the poll block, and +/// the cold arm of a read that may collect, reload `read` from `this`'s +/// root, resolve forwarding and store the head again. +#[derive(Debug, Clone)] +pub(crate) struct FieldBase { + pub(crate) field: String, + /// The field read the install and every refresh lower: `this.` + /// as the field read call's own read writes it. + pub(crate) read: Expr, + pub(crate) rep: crate::codegen::FactsArrRep, + pub(crate) base_slot: String, } /// Active materialised receiver descriptors for one function lowering. @@ -693,11 +714,94 @@ impl ReceiverDescriptorTable { | ActiveReceiverData::BoundedIndex { .. } | ActiveReceiverData::PackedF64Loop(_) | ActiveReceiverData::MaskedWindowArray(_) - | ActiveReceiverData::BufferView(_) => None, + | ActiveReceiverData::BufferView(_) + | ActiveReceiverData::FieldBase(_) => None, } }) } + /// PR-D: hold the element base of `this.` across a loop. The + /// contract is an address refreshed at the back-edge poll; every other + /// ender is refused by the installer's admission, and a cold arm that + /// may collect re-derives it (`stmt::field_base`). `false` when an + /// outer loop already holds this field's base. + pub(crate) fn materialize_field_base(&mut self, base: FieldBase) -> bool { + if self.field_base(&base.field).is_some() { + return false; + } + let contract = ReceiverDescriptor { + table: "receiver_descriptors[field_base]", + receiver: u32::MAX, + claim: ReceiverClaim::Address, + boundary: FactBoundary::PollRefresh, + excludes_try: false, + }; + boundary_admits(&contract, RegionEnder::BackEdgePoll) + .expect("a field base must survive its back-edge poll"); + self.entries.push(ActiveReceiverDescriptor { + contract, + data: ActiveReceiverData::FieldBase(base), + }); + true + } + + /// Whether every held address is a field base and no byte-view proof is + /// installed: a cold arm that may collect then needs only the field + /// bases' re-derivation. + pub(crate) fn only_field_bases(&self) -> bool { + self.byte_view_params.is_empty() + && self.entries.iter().all(|entry| { + matches!(&entry.data, ActiveReceiverData::FieldBase(_)) + || !matches!( + entry.contract.claim, + ReceiverClaim::Address | ReceiverClaim::NonMovingAddress + ) + }) + } + + /// The active base of `this.`. + pub(crate) fn field_base(&self, field: &str) -> Option<&FieldBase> { + self.entries.iter().find_map(|entry| match &entry.data { + ActiveReceiverData::FieldBase(base) if base.field == field => Some(base), + _ => None, + }) + } + + /// Every active field base, outermost first. + pub(crate) fn field_bases(&self) -> Vec { + self.entries + .iter() + .filter_map(|entry| match &entry.data { + ActiveReceiverData::FieldBase(base) => Some(base.clone()), + _ => None, + }) + .collect() + } + + /// The field bases a back-edge poll re-derives, each checked at the + /// boundary like [`Self::poll_refreshes`]. + pub(crate) fn field_base_refreshes(&self) -> Result, BoundaryViolation> { + let mut out = Vec::new(); + for entry in &self.entries { + if let ActiveReceiverData::FieldBase(base) = &entry.data { + boundary_admits(&entry.contract, RegionEnder::BackEdgePoll)?; + out.push(base.clone()); + } + } + Ok(out) + } + + /// End the loop that holds `field`'s base. + pub(crate) fn dematerialize_field_base(&mut self, field: &str) -> bool { + let Some(index) = self.entries.iter().position(|entry| { + matches!(&entry.data, ActiveReceiverData::FieldBase(base) if base.field == field) + }) else { + return false; + }; + self.entries.remove(index); + true + } + /// Record that `index_local_id` is in bounds for `receiver` throughout a /// lexical loop-proof scope. Scalar relations survive safepoints, while /// reassignment and scope exit invalidate them through the table APIs diff --git a/crates/perry-codegen/src/expr/index_get.rs b/crates/perry-codegen/src/expr/index_get.rs index f7c5ab56425..86df7b394e2 100644 --- a/crates/perry-codegen/src/expr/index_get.rs +++ b/crates/perry-codegen/src/expr/index_get.rs @@ -41,6 +41,7 @@ use super::{ }; pub(crate) mod array_rep; +pub(crate) mod field_base; mod foreign_counter; pub(crate) mod descriptor_read; pub(crate) mod elem_floor; diff --git a/crates/perry-codegen/src/expr/index_get/field_base.rs b/crates/perry-codegen/src/expr/index_get/field_base.rs new file mode 100644 index 00000000000..45cd4e034bc --- /dev/null +++ b/crates/perry-codegen/src/expr/index_get/field_base.rs @@ -0,0 +1,316 @@ +//! The element base of an Array held in a field of `this`, held across a +//! loop (DESIGN-p4l1 rev 2 §4.3, PR-D; REVIEW-p4l1 findings 10 and 11). +//! +//! `stmt::field_base` decides which loop holds which field's base. This +//! module emits what the base needs: the install, the refresh, and the +//! reads of the field read calls (b1, `lower_call::field_read_call`) the +//! loop serves from it. +//! +//! **Install.** Load `this.f` (the field's `FieldProof.array` is `Arr`, +//! dense, with a floor), mask it to its handle, and resolve forwarding +//! once: a header with `GC_FLAG_FORWARDED` is a growth stub, and the +//! runtime's `js_array_live_head` follows the chain to the live head (one +//! cold call, no inline edge). The facts give the kind; forwarding is only +//! an address, so there is no second loop body (finding 10). The live head +//! is stored in the base slot. With `fixed` storage nothing is ever +//! forwarded and the head is the handle. +//! +//! **Refresh.** The base is an address: the back-edge poll's slow block +//! (`stmt::loops`) re-derives it from `this`'s GC-updated root, exactly as +//! at install, and so does the cold arm of a read that may collect. +//! +//! **Reads.** A call in its own floor (wpfacts `FieldReadCall::in_floor`) +//! is `load [base + 24 + 8 * i]`. Any other call is `i `: below the dense floor the slot +//! is a present element, and outside it the cold arm is the read the call +//! has without a base (C3's), after which every held base is re-derived, +//! since that read's generic `Get` may collect. With a `?? L`, the elements +//! must all be Numbers (a stored `null` or `undefined` is a present +//! element), as for C3's in-floor call. +//! +//! **Check mode** (`PERRY_VERIFY_FACTS=1`). At install and at every +//! refresh, the head is tested as a field read's `Arr` claim is, and it +//! must not be forwarded. At every read, the base held must be the live +//! head of a fresh load of the field, and C3's read witness runs on that +//! fresh load. b1's own witness (the real call beside the read) may +//! collect, so the bases are re-derived after it. A miss exits 86 +//! (`Fact::ArrayRep`). +//! +//! `PERRY_FACTS_ARRAY_BASE=0` turns the installer off (C3's build). +//! Negative controls: `PERRY_FACTS_SABOTAGE=arrbase` installs the stub's +//! handle without resolving forwarding; `arrbaseadm` admits a loop whatever +//! else ends its region (`stmt::field_base`). + +use anyhow::Result; +use perry_hir::{Expr, LogicalOp}; + +use super::FnCtx; +use crate::codegen::{FactsArrRep, FactsElemRep}; +use crate::collectors::FieldBase; +use crate::nanbox::{POINTER_MASK_I64, POINTER_TAG_I64}; +use crate::types::{DOUBLE, I32, I64}; + +/// `perry_abi::GC_FLAG_FORWARDED` in the header word's second byte. +const FORWARDED_I32: &str = "32768"; + +/// `PERRY_FACTS_ARRAY_BASE=0` turns the installer off. +pub(crate) fn enabled() -> bool { + static ON: std::sync::OnceLock = std::sync::OnceLock::new(); + *ON.get_or_init(|| { + !matches!( + std::env::var("PERRY_FACTS_ARRAY_BASE").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ) + }) +} + +/// The negative control `PERRY_FACTS_SABOTAGE=`. +pub(crate) fn sabotaged(arm: &str) -> bool { + std::env::var("PERRY_FACTS_SABOTAGE").as_deref() == Ok(arm) +} + +/// A field read call's read (`this.f[k] ?? L`, `field_read_call_at`) that a +/// held base can serve: the field, its representation and the field read +/// `this.f` itself. +pub(crate) struct Servable<'e> { + pub(crate) field: &'e str, + pub(crate) rep: FactsArrRep, + pub(crate) field_read: &'e Expr, + pub(crate) index: &'e Expr, +} + +/// `read` (a field read call's rebuilt read), when a base of `this.f` can +/// serve it: the receiver is `this`, the field read is `Arr`, dense with a +/// floor (`proven_array::in_floor_rep`), and a `?? L` is over Number +/// elements. +pub(crate) fn servable<'e>(ctx: &FnCtx<'_>, read: &'e Expr) -> Option> { + let (element, coalesced) = match read { + Expr::Logical { + op: LogicalOp::Coalesce, + left, + .. + } => (left.as_ref(), true), + e => (e, false), + }; + let Expr::IndexGet { object, index, .. } = element else { + return None; + }; + let Expr::PropertyGet { + object: holder, + property, + .. + } = object.as_ref() + else { + return None; + }; + if !matches!(holder.as_ref(), Expr::This) { + return None; + } + let rep = super::proven_array::in_floor_rep(ctx, object)?; + if coalesced && rep.elem == FactsElemRep::Boxed { + return None; + } + Some(Servable { + field: property, + rep, + field_read: object, + index, + }) +} + +/// Load the field, resolve forwarding and store the live head in the base +/// slot (module docs): the install and every refresh. +pub(crate) fn emit_install(ctx: &mut FnCtx<'_>, base: &FieldBase) -> Result<()> { + let boxed = super::lower_expr(ctx, &base.read)?; + let bits = ctx.block().bitcast_double_to_i64(&boxed); + let handle = ctx.block().and(I64, &bits, POINTER_MASK_I64); + let head = if base.rep.fixed || sabotaged("arrbase") { + handle + } else { + live_head(ctx, &handle) + }; + if crate::verify_facts::enabled() { + let tagged = ctx.block().or(I64, &head, POINTER_TAG_I64); + let word = ctx.block().bitcast_i64_to_double(&tagged); + // The head is never a stub: tested as fixed storage is. + let r = FactsArrRep { + fixed: true, + ..base.rep + }; + super::array_rep::witness_value(ctx, &word, r, &format!("field base this.{}", base.field)); + } + ctx.block().store(I64, &head, &base.base_slot); + Ok(()) +} + +/// The live head of `handle`: itself, or the end of its forwarding chain. +fn live_head(ctx: &mut FnCtx<'_>, handle: &str) -> String { + let word = super::guarded_array::emit_array_guard_word(ctx.block(), handle); + let moved = ctx.block().and(I32, &word, FORWARDED_I32); + let stub = ctx.block().icmp_ne(I32, &moved, "0"); + let follow = ctx.new_block("abase.follow"); + let live = ctx.new_block("abase.live"); + let (follow_l, live_l) = (ctx.block_label(follow), ctx.block_label(live)); + let from = ctx.block().label.clone(); + ctx.block().cond_br(&stub, &follow_l, &live_l); + ctx.current_block = follow; + let followed = ctx + .block() + .call(I64, "js_array_live_head", &[(I64, handle)]); + ctx.block().br(&live_l); + ctx.current_block = live; + ctx.block() + .phi(I64, &[(handle, &from), (&followed, &follow_l)]) +} + +/// Re-derive every held base: after a call that may collect. +pub(crate) fn rederive_all(ctx: &mut FnCtx<'_>) -> Result<()> { + for base in ctx.receiver_descriptors.field_bases() { + emit_install(ctx, &base)?; + } + Ok(()) +} + +/// The back-edge poll's slow block, after `js_gc_loop_safepoint`: every +/// held base, from `this`'s GC-updated root. +pub(crate) fn emit_poll_refresh(ctx: &mut FnCtx<'_>) -> Result<()> { + let bases = ctx + .receiver_descriptors + .field_base_refreshes() + .expect("every held field base must admit a back-edge poll"); + for base in &bases { + emit_install(ctx, base)?; + } + Ok(()) +} + +/// The read of the field read call at `site` (rebuilt as `read`), from the +/// base an enclosing loop holds; `None` when no loop holds that field's +/// base or the read is not one a base serves. +pub(crate) fn try_lower_read( + ctx: &mut FnCtx<'_>, + site: u32, + read: &Expr, +) -> Result> { + let Some(s) = servable(ctx, read) else { + return Ok(None); + }; + let Some(base) = ctx.receiver_descriptors.field_base(s.field).cloned() else { + return Ok(None); + }; + let call_floor = ctx + .wpfacts + .field_read_calls + .get(&site) + .and_then(|f| f.in_floor); + let index = s.index; + crate::verify_facts::consumed( + crate::verify_facts::Fact::ArrayRep, + || serde_json::json!({ "field_base": base.field, "floor": base.rep.floor, "in_floor": call_floor.is_some() }), + ); + crate::facts_consumed::used(); + let idx = crate::expr::lower_expr_as_i32(ctx, index)?; + if crate::verify_facts::enabled() { + witness(ctx, &base, &idx, call_floor)?; + } + if call_floor.is_some() { + return Ok(Some(load(ctx, &base, &idx))); + } + // Outside the call's floor: the slot below the dense floor, else the + // call's own read, after which the bases are re-derived. + let fast = ctx.new_block("abase.slot"); + let slow = ctx.new_block("abase.read"); + let merge = ctx.new_block("abase.merge"); + let (fast_l, slow_l, merge_l) = ( + ctx.block_label(fast), + ctx.block_label(slow), + ctx.block_label(merge), + ); + let inside = ctx.block().icmp_ult(I32, &idx, &base.rep.floor.to_string()); + ctx.block().cond_br(&inside, &fast_l, &slow_l); + ctx.current_block = fast; + let value = load(ctx, &base, &idx); + let fast_end = ctx.block().label.clone(); + ctx.block().br(&merge_l); + ctx.current_block = slow; + let cold = super::lower_expr(ctx, read)?; + rederive_all(ctx)?; + let slow_end = ctx.block().label.clone(); + ctx.block().br(&merge_l); + ctx.current_block = merge; + Ok(Some( + ctx.block() + .phi(DOUBLE, &[(&value, &fast_end), (&cold, &slow_end)]), + )) +} + +/// `load [base + 24 + 8 * idx]`. +fn load(ctx: &mut FnCtx<'_>, base: &FieldBase, idx: &str) -> String { + let blk = ctx.block(); + let head = blk.load(I64, &base.base_slot); + let wide = blk.zext(I32, idx, I64); + let offset = blk.shl(I64, &wide, "3"); + let elements = blk.add( + I64, + &head, + &crate::target_layout::ARRAY_HEADER_SIZE_BYTES.to_string(), + ); + let addr = blk.add(I64, &elements, &offset); + let slot = blk.inttoptr(I64, &addr); + let raw = blk.load(I64, &slot); + blk.bitcast_i64_to_double(&raw) +} + +/// Check mode at a read served from a held base (module docs). +fn witness( + ctx: &mut FnCtx<'_>, + base: &FieldBase, + idx: &str, + call_floor: Option, +) -> Result<()> { + crate::verify_facts::covered( + crate::verify_facts::Fact::ArrayRep, + || serde_json::json!({ "field_base": base.field, "floor": base.rep.floor }), + ); + let fresh = super::lower_expr(ctx, &base.read)?; + let bits = ctx.block().bitcast_double_to_i64(&fresh); + let handle = ctx.block().and(I64, &bits, POINTER_MASK_I64); + let live = ctx + .block() + .call(I64, "js_array_live_head", &[(I64, &handle)]); + let held = ctx.block().load(I64, &base.base_slot); + let same = ctx.block().icmp_eq(I64, &live, &held); + let miss = ctx.new_block("abase.verify_miss"); + let next = ctx.new_block("abase.admitted"); + let (miss_l, next_l) = (ctx.block_label(miss), ctx.block_label(next)); + crate::verify_facts::tick(ctx); + ctx.block().cond_br(&same, &next_l, &miss_l); + ctx.current_block = miss; + let site = crate::verify_facts::site_arg( + ctx, + &format!( + "array rep of field base this.{}: the held base is not the live head", + base.field + ), + crate::verify_facts::Fact::ArrayRep, + &[], + ); + let _ = crate::verify_facts::check( + ctx, + I32, + "perry_wpfacts_check_miss", + &[(DOUBLE, &fresh)], + &site, + ); + ctx.block().unreachable(); + ctx.current_block = next; + let read = super::proven_array::RepRead { + rep: base.rep, + in_floor: call_floor.is_some(), + key_floor: call_floor.unwrap_or(base.rep.floor), + number: base.rep.elem != FactsElemRep::Boxed, + receiver: super::proven_array::Receiver::Field, + }; + super::array_rep::witness_read(ctx, &fresh, idx, read, false); + Ok(()) +} diff --git a/crates/perry-codegen/src/lower_call/field_read_call.rs b/crates/perry-codegen/src/lower_call/field_read_call.rs index 8a2a972526b..0a401d08d5e 100644 --- a/crates/perry-codegen/src/lower_call/field_read_call.rs +++ b/crates/perry-codegen/src/lower_call/field_read_call.rs @@ -115,18 +115,29 @@ pub(crate) fn try_lower( || serde_json::json!({ "call": site }), ); crate::facts_consumed::used(); - let value = match in_floor(ctx, site, &read) { - Some((object, index, rep, floor)) => { - // The index is inert and reaches no ender (the accessor), so no - // collection runs between it and the field load. - let idx = crate::expr::lower_expr_as_i32(ctx, index)?; - let arr = crate::expr::lower_expr(ctx, object)?; - crate::expr::index_get::proven_array::lower_in_floor(ctx, &arr, &idx, rep, floor) + // PR-D: a loop that holds the field's element base serves the read. + let held = crate::expr::index_get::field_base::try_lower_read(ctx, site, &read)?; + let served = held.is_some(); + let value = if let Some(value) = held { + value + } else { + match in_floor(ctx, site, &read) { + Some((object, index, rep, floor)) => { + // The index is inert and reaches no ender (the accessor), so + // no collection runs between it and the field load. + let idx = crate::expr::lower_expr_as_i32(ctx, index)?; + let arr = crate::expr::lower_expr(ctx, object)?; + crate::expr::index_get::proven_array::lower_in_floor(ctx, &arr, &idx, rep, floor) + } + None => crate::expr::lower_expr(ctx, &read)?, } - None => crate::expr::lower_expr(ctx, &read)?, }; if crate::verify_facts::enabled() { witness(ctx, callee, args, &value, site)?; + if served { + // The real call may collect: the held bases are re-derived. + crate::expr::index_get::field_base::rederive_all(ctx)?; + } } Ok(Some(value)) } diff --git a/crates/perry-codegen/src/stmt/field_base.rs b/crates/perry-codegen/src/stmt/field_base.rs new file mode 100644 index 00000000000..a6c34fa9165 --- /dev/null +++ b/crates/perry-codegen/src/stmt/field_base.rs @@ -0,0 +1,552 @@ +//! Which loop holds the element base of `this.f` (DESIGN-p4l1 rev 2 §4.3, +//! PR-D; REVIEW-p4l1 findings 10 and 11). The base's emission (install, +//! refresh, reads) is `expr::index_get::field_base`. +//! +//! A loop L holds the base of field `f` iff: +//! 1. a trusted read of `this.f` **dominates L's back edge** (b3's +//! condition (a)): every path through L's body that reaches the latch, +//! a `continue` included, runs one first. A trusted read is a field read +//! call (b1) on `this` whose read a base can serve +//! (`field_base::servable`): `Arr`, dense, with a floor; +//! 2. L is the outermost such loop: an enclosing loop that holds `f`'s +//! base already serves L, and L installs nothing for `f`; +//! 3. **admission:** every region ender in L (body and controls, nested +//! loops included) is a back-edge poll, with the trusted reads lowered +//! as reads. A read outside its call's floor reports its cold arm +//! (`ColdArmCall`), which re-derives every held base; such a loop is +//! admitted only while no address other than a field base is held. Any +//! other call, any store, allocation, coercion of an unproven operand, +//! `try`, `throw` or suspension refuses L, so L writes no field and +//! grows no Array. +//! +//! **Install point:** L's guarded preheader. A `while` or a `for` with a +//! test lowers the test once more before the loop (it must write nothing +//! and end no region) and installs only when it holds, so every install is +//! followed by at least one iteration and, by rule 1, at least one read. +//! LLVM's loop rotation duplicates the same test into the preheader, and +//! the two fold into one. A `do-while` and a `for` with no test enter their +//! body unconditionally and install unguarded. +//! +//! `PERRY_ARRAY_BASE_DIAG=1` prints one line per loop with a trusted read: +//! the function, the fields and the verdict (the install-rule probe). + +use std::collections::{BTreeMap, HashSet}; + +use anyhow::Result; +use perry_hir::{Expr, Stmt}; + +use crate::codegen::FactsArrRep; +use crate::collectors::{FieldBase, RegionEnder}; +use crate::expr::index_get::field_base as emit; +use crate::expr::FnCtx; +use crate::types::I64; + +/// The fields a loop installed, for [`end`]. +#[must_use] +pub(crate) struct Installed(Vec); + +/// A trusted read found in a loop. +struct Read { + call: usize, + callee: usize, + field: String, + rep: FactsArrRep, + field_read: Expr, + /// The call is in its own floor: its read has no cold arm. + in_floor: bool, +} + +fn diag(ctx: &FnCtx<'_>, fields: &[&str], verdict: &str) { + if std::env::var("PERRY_ARRAY_BASE_DIAG").as_deref() == Ok("1") { + eprintln!( + "[perry array base] fn={} fields={} verdict={verdict}", + ctx.func.name, + fields.join(",") + ); + } +} + +/// Install the bases loop L qualifies for (module docs), before L is +/// lowered. `test`: L's entry test (`while`, `for` with a condition); +/// `controls`: every expression L evaluates outside its body. +pub(crate) fn begin( + ctx: &mut FnCtx<'_>, + test: Option<&Expr>, + controls: &[&Expr], + body: &[Stmt], +) -> Result { + if !emit::enabled() + || ctx.wpfacts_off + || crate::expr::typed_feedback_emission_enabled() + || ctx.block().is_terminated() + { + return Ok(Installed(Vec::new())); + } + let mut reads = Vec::new(); + for s in body { + reads_in_stmt(ctx, s, &mut reads); + } + for c in controls { + reads_in_expr(ctx, c, &mut reads); + } + if reads.is_empty() { + return Ok(Installed(Vec::new())); + } + let mut by_field: BTreeMap<&str, Vec<&Read>> = BTreeMap::new(); + for r in &reads { + by_field.entry(r.field.as_str()).or_default().push(r); + } + let names: Vec<&str> = by_field.keys().copied().collect(); + // Rule 2: a field an enclosing loop holds is served by it. + let held: HashSet<&str> = names + .iter() + .copied() + .filter(|f| ctx.receiver_descriptors.field_base(f).is_some()) + .collect(); + // Rule 1. + let install: Vec<&str> = names + .iter() + .copied() + .filter(|f| !held.contains(f)) + .filter(|f| { + let calls: HashSet = by_field[f].iter().map(|r| r.call).collect(); + stmts_read(body, &|e: &Expr| calls.contains(&addr(e))) == Paths::READ + }) + .collect(); + if install.is_empty() { + diag( + ctx, + &names, + if held.is_empty() { + "refused:no-dominating-read" + } else { + "served-by-outer" + }, + ); + return Ok(Installed(Vec::new())); + } + // Rule 3: the trusted reads are those a base serves, here or outside. + let served: Vec<&Read> = reads + .iter() + .filter(|r| install.contains(&r.field.as_str()) || held.contains(r.field.as_str())) + .collect(); + let classified = |e: &Expr| -> Option> { + let a = addr(e); + served.iter().find_map(|r| { + if r.call == a { + Some((!r.in_floor).then_some(RegionEnder::ColdArmCall)) + } else if r.callee == a { + Some(None) + } else { + None + } + }) + }; + let is_inert = |e: &Expr| crate::rooting::expr_is_inert_primitive(ctx, e); + let enders = crate::collectors::region_enders_in_stmts_classified( + body, + controls, + &is_inert, + &classified, + ); + let other = enders + .iter() + .find(|e| !matches!(e, RegionEnder::BackEdgePoll | RegionEnder::ColdArmCall)); + let cold = enders.contains(&RegionEnder::ColdArmCall); + if !emit::sabotaged("arrbaseadm") { + if let Some(e) = other { + diag(ctx, &install, &format!("refused:ender:{e:?}")); + return Ok(Installed(Vec::new())); + } + if cold && !ctx.receiver_descriptors.only_field_bases() { + diag(ctx, &install, "refused:cold-arm-under-another-address"); + return Ok(Installed(Vec::new())); + } + if test.is_some_and(writes) { + diag(ctx, &install, "refused:test-writes"); + return Ok(Installed(Vec::new())); + } + } + let bases: Vec = install + .iter() + .map(|f| { + let r = by_field[f][0]; + FieldBase { + field: r.field.clone(), + read: r.field_read.clone(), + rep: r.rep, + base_slot: ctx.func.alloca_entry(I64), + } + }) + .collect(); + // The guarded preheader. + let join = test + .map(|t| -> Result { + let holds = crate::lower_conditional::lower_test(ctx, t)?; + let at = ctx.new_block("abase.install"); + let join = ctx.new_block("abase.entered"); + let (at_l, join_l) = (ctx.block_label(at), ctx.block_label(join)); + ctx.block().cond_br(&holds, &at_l, &join_l); + ctx.current_block = at; + Ok(join) + }) + .transpose()?; + for base in &bases { + emit::emit_install(ctx, base)?; + } + if let Some(join) = join { + let join_l = ctx.block_label(join); + ctx.block().br(&join_l); + ctx.current_block = join; + } + let mut fields = Vec::new(); + for base in bases { + let f = base.field.clone(); + if ctx.receiver_descriptors.materialize_field_base(base) { + fields.push(f); + } + } + let shown: Vec<&str> = fields.iter().map(String::as_str).collect(); + diag( + ctx, + &shown, + if cold { + "installed:cold-arm" + } else { + "installed" + }, + ); + Ok(Installed(fields)) +} + +/// End the loop's bases (after the loop is lowered). +pub(crate) fn end(ctx: &mut FnCtx<'_>, installed: Installed) { + for f in installed.0 { + ctx.receiver_descriptors.dematerialize_field_base(&f); + } +} + +fn addr(e: &Expr) -> usize { + e as *const Expr as usize +} + +/// The trusted reads in `e` (not inside closures, which are other frames). +fn reads_in_expr(ctx: &FnCtx<'_>, e: &Expr, out: &mut Vec) { + if matches!(e, Expr::Closure { .. }) { + return; + } + if let Expr::Call { callee, args, .. } = e { + if let Some(read) = + crate::lower_call::field_read_call::field_read_call_at(ctx, callee, args) + { + if let Some(s) = emit::servable(ctx, &read) { + let site = match callee.as_ref() { + Expr::PropertyGet { byte_offset, .. } => *byte_offset, + _ => 0, + }; + let in_floor = ctx + .wpfacts + .field_read_calls + .get(&site) + .is_some_and(|f| f.in_floor.is_some()); + out.push(Read { + call: addr(e), + callee: addr(callee), + field: s.field.to_string(), + rep: s.rep, + field_read: s.field_read.clone(), + in_floor, + }); + } + } + } + perry_hir::walker::walk_expr_children(e, &mut |c| reads_in_expr(ctx, c, out)); +} + +fn reads_in_stmt(ctx: &FnCtx<'_>, s: &Stmt, out: &mut Vec) { + match s { + Stmt::Expr(e) + | Stmt::Throw(e) + | Stmt::Return(Some(e)) + | Stmt::Let { init: Some(e), .. } => reads_in_expr(ctx, e, out), + Stmt::If { + condition, + then_branch, + else_branch, + } => { + reads_in_expr(ctx, condition, out); + for st in then_branch.iter().chain(else_branch.iter().flatten()) { + reads_in_stmt(ctx, st, out); + } + } + Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => { + reads_in_expr(ctx, condition, out); + for st in body { + reads_in_stmt(ctx, st, out); + } + } + Stmt::For { + init, + condition, + update, + body, + } => { + if let Some(i) = init { + reads_in_stmt(ctx, i, out); + } + for e in condition.iter().chain(update.iter()) { + reads_in_expr(ctx, e, out); + } + for st in body { + reads_in_stmt(ctx, st, out); + } + } + Stmt::Labeled { body, .. } => reads_in_stmt(ctx, body, out), + Stmt::Try { + body, + catch, + finally, + } => { + for st in body + .iter() + .chain(catch.iter().flat_map(|c| c.body.iter())) + .chain(finally.iter().flatten()) + { + reads_in_stmt(ctx, st, out); + } + } + Stmt::Switch { + discriminant, + cases, + } => { + reads_in_expr(ctx, discriminant, out); + for c in cases { + if let Some(t) = &c.test { + reads_in_expr(ctx, t, out); + } + for st in &c.body { + reads_in_stmt(ctx, st, out); + } + } + } + _ => {} + } +} + +/// Whether the loop test `e` may write a binding or a property (it is +/// lowered twice: once as the preheader's guard). +fn writes(e: &Expr) -> bool { + let mut found = matches!( + e, + Expr::LocalSet(..) + | Expr::Update { .. } + | Expr::PropertySet { .. } + | Expr::PropertyUpdate { .. } + | Expr::IndexSet { .. } + | Expr::IndexUpdate { .. } + | Expr::GlobalSet(..) + ); + if !found { + perry_hir::walker::walk_expr_children(e, &mut |c| found |= writes(c)); + } + found +} + +/// What the paths through some code do before they reach the loop's latch +/// (rule 1). +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub(crate) struct Paths { + /// Some path leaves the code normally, with no trusted read yet. + pub(crate) unread_falls: bool, + /// Some path reaches the latch (a `continue`) with no trusted read. + pub(crate) unread_latch: bool, +} + +impl Paths { + /// Every path has read, or left the loop. + pub(crate) const READ: Paths = Paths { + unread_falls: false, + unread_latch: false, + }; + const FALLS: Paths = Paths { + unread_falls: true, + unread_latch: false, + }; + const LATCH: Paths = Paths { + unread_falls: false, + unread_latch: true, + }; + fn or(self, o: Paths) -> Paths { + Paths { + unread_falls: self.unread_falls || o.unread_falls, + unread_latch: self.unread_latch || o.unread_latch, + } + } +} + +/// Rule 1 over a loop body: `READ` iff every path to the latch runs a +/// trusted read first (the end of the body is the latch). +pub(crate) fn stmts_read(body: &[Stmt], trusted: &dyn Fn(&Expr) -> bool) -> Paths { + let p = seq(body, trusted); + Paths { + unread_falls: false, + unread_latch: p.unread_latch || p.unread_falls, + } +} + +fn seq(stmts: &[Stmt], trusted: &dyn Fn(&Expr) -> bool) -> Paths { + let mut out = Paths::FALLS; + for s in stmts { + if !out.unread_falls { + break; + } + let p = stmt_read(s, trusted); + out = Paths { + unread_falls: p.unread_falls, + unread_latch: out.unread_latch || p.unread_latch, + }; + } + out +} + +fn stmt_read(s: &Stmt, trusted: &dyn Fn(&Expr) -> bool) -> Paths { + match s { + Stmt::Expr(e) | Stmt::Let { init: Some(e), .. } => { + if expr_reads(e, trusted) { + Paths::READ + } else { + Paths::FALLS + } + } + // Leaves the loop: no latch on this path. + Stmt::Return(_) | Stmt::Throw(_) | Stmt::Break => Paths::READ, + Stmt::Continue => Paths::LATCH, + // A labeled jump may land anywhere, the latch included. + Stmt::LabeledBreak(_) | Stmt::LabeledContinue(_) => Paths::LATCH, + Stmt::If { + condition, + then_branch, + else_branch, + } => { + if expr_reads(condition, trusted) { + return Paths::READ; + } + let t = seq(then_branch, trusted); + let e = else_branch + .as_ref() + .map_or(Paths::FALLS, |b| seq(b, trusted)); + t.or(e) + } + Stmt::Labeled { body, .. } => stmt_read(body, trusted), + // A nested loop may run its body zero times; its own `break` and + // `continue` stay inside it. Only its first test counts. + Stmt::While { condition, body } => { + if expr_reads(condition, trusted) { + Paths::READ + } else { + nested(body) + } + } + Stmt::For { + init, + condition, + body, + .. + } => { + let first = init + .as_deref() + .is_some_and(|i| stmt_read(i, trusted) == Paths::READ) + || condition.as_ref().is_some_and(|c| expr_reads(c, trusted)); + if first { + Paths::READ + } else { + nested(body) + } + } + Stmt::DoWhile { body, .. } => nested(body), + Stmt::Switch { + discriminant, + cases, + } => { + if expr_reads(discriminant, trusted) { + Paths::READ + } else { + Paths { + unread_falls: true, + unread_latch: cases.iter().any(|c| jumps(&c.body, true)), + } + } + } + Stmt::Try { .. } => Paths { + unread_falls: true, + unread_latch: true, + }, + _ => Paths::FALLS, + } +} + +/// A nested loop's body: unread fall-through, and the latch only through a +/// labeled jump. +fn nested(body: &[Stmt]) -> Paths { + Paths { + unread_falls: true, + unread_latch: jumps(body, false), + } +} + +/// Whether `stmts` may jump to the latch: a labeled jump anywhere, and a +/// plain `continue` when `plain` (outside a nested loop). +fn jumps(stmts: &[Stmt], plain: bool) -> bool { + stmts.iter().any(|s| match s { + Stmt::LabeledBreak(_) | Stmt::LabeledContinue(_) => true, + Stmt::Continue => plain, + Stmt::If { + then_branch, + else_branch, + .. + } => jumps(then_branch, plain) || else_branch.as_ref().is_some_and(|b| jumps(b, plain)), + Stmt::Labeled { body, .. } => jumps(std::slice::from_ref(body.as_ref()), plain), + Stmt::While { body, .. } | Stmt::DoWhile { body, .. } | Stmt::For { body, .. } => { + jumps(body, false) + } + Stmt::Switch { cases, .. } => cases.iter().any(|c| jumps(&c.body, plain)), + Stmt::Try { + body, + catch, + finally, + } => { + jumps(body, plain) + || catch.as_ref().is_some_and(|c| jumps(&c.body, plain)) + || finally.as_ref().is_some_and(|f| jumps(f, plain)) + } + _ => false, + }) +} + +/// Whether evaluating `e` always runs a trusted read: the node itself, or +/// a child every evaluation reaches. Only the forms whose children all run +/// are walked (`&&`, `||`, `??` only through their left operand, `?:` +/// through its test); any other form is "no". +fn expr_reads(e: &Expr, trusted: &dyn Fn(&Expr) -> bool) -> bool { + if trusted(e) { + return true; + } + match e { + Expr::Logical { left, .. } => expr_reads(left, trusted), + Expr::Conditional { condition, .. } => expr_reads(condition, trusted), + Expr::Binary { left, right, .. } | Expr::Compare { left, right, .. } => { + expr_reads(left, trusted) || expr_reads(right, trusted) + } + Expr::Unary { operand, .. } => expr_reads(operand, trusted), + Expr::LocalSet(_, value) => expr_reads(value, trusted), + Expr::Sequence(items) => items.iter().any(|x| expr_reads(x, trusted)), + Expr::Call { callee, args, .. } => { + expr_reads(callee, trusted) || args.iter().any(|a| expr_reads(a, trusted)) + } + Expr::IndexGet { object, index, .. } => { + expr_reads(object, trusted) || expr_reads(index, trusted) + } + Expr::PropertyGet { object, .. } => expr_reads(object, trusted), + _ => false, + } +} diff --git a/crates/perry-codegen/src/stmt/field_base_tests.rs b/crates/perry-codegen/src/stmt/field_base_tests.rs new file mode 100644 index 00000000000..ee9de0bc595 --- /dev/null +++ b/crates/perry-codegen/src/stmt/field_base_tests.rs @@ -0,0 +1,261 @@ +//! PR-D (`stmt::field_base`, `expr::index_get::field_base`): rule 1 (a +//! trusted read dominates the back edge) on HIR, and the installed region +//! in the IR on injected facts. Each test has a negative control. + +use std::sync::Arc; + +use perry_hir::{Expr, Module, Stmt}; + +use super::field_base::{stmts_read, Paths}; +use crate::codegen::{ + ElisionFacts, FactsArrRep, FactsClass, FactsElemRep, FactsField, FactsFieldReadCall, FactsRecv, + FactsRep, ProgramFactsView, +}; +use crate::{compile_module, CompileOptions}; + +fn lower(src: &str) -> Module { + let src = src.to_string(); + std::thread::Builder::new() + .stack_size(32 * 1024 * 1024) + .spawn(move || { + let mut cache = perry_diagnostics::SourceCache::new(); + let parsed = perry_parser::parse_typescript_with_cache(&src, "fb.ts", &mut cache) + .expect("parses"); + perry_hir::lower_module(&parsed.module, "fb", "fb.ts").expect("lowers") + }) + .expect("spawn") + .join() + .expect("lowering thread") +} + +/// The first loop body in method `name` of class `B`. +fn loop_body<'m>(m: &'m Module, name: &str) -> &'m [Stmt] { + let class = m.classes.iter().find(|c| c.name == "B").expect("B"); + let f = class + .methods + .iter() + .find(|f| f.name == name) + .unwrap_or_else(|| panic!("method {name}")); + fn find(stmts: &[Stmt]) -> Option<&[Stmt]> { + stmts.iter().find_map(|s| match s { + Stmt::While { body, .. } | Stmt::For { body, .. } | Stmt::DoWhile { body, .. } => { + Some(body.as_slice()) + } + Stmt::Labeled { body, .. } => find(std::slice::from_ref(body.as_ref())), + _ => None, + }) + } + find(&f.body).unwrap_or_else(|| panic!("a loop in {name}")) +} + +/// A call `this.at(...)`. +fn is_at(e: &Expr) -> bool { + matches!(e, Expr::Call { callee, .. } + if matches!(callee.as_ref(), Expr::PropertyGet { property, .. } if property == "at")) +} + +const RULE_SRC: &str = "class B {\n\ + board: number[] = new Array(128).fill(0);\n\ + at(sq: number): number { return this.board[sq] ?? 0; }\n\ + first(n: number): number { let s = 0; let i = 0; while (i < n) { const p = this.at(i); s += p; i++; } return s; }\n\ + test(n: number): number { let s = 0; let i = 0; while (i < n) { if (this.at(i) === 1) s++; i++; } return s; }\n\ + leaves(n: number): number { let s = 0; let i = 0; while (i < n) { if (i > 3) { break; } s += this.at(i); i++; } return s; }\n\ + arms(n: number): number { let s = 0; let i = 0; while (i < n) { if (i > 3) { s += this.at(i); } else { return s; } i++; } return s; }\n\ + skips(n: number): number { let s = 0; for (let i = 0; i < n; i++) { if ((i & 0x88) !== 0) { i += 7; continue; } s += this.at(i); } return s; }\n\ + half(n: number): number { let s = 0; let i = 0; while (i < n) { s += i > 2 ? this.at(i) : 0; i++; } return s; }\n\ + right(n: number): number { let s = 0; let i = 0; while (i < n) { if (i > 2 && this.at(i) === 1) s++; i++; } return s; }\n\ + left(n: number): number { let s = 0; let i = 0; while (i < n) { if (this.at(i) === 1 && i > 2) s++; i++; } return s; }\n\ + inner(n: number): number { let s = 0; for (let r = 0; r < n; r++) { for (let f = 0; f < r; f++) s += this.at(f); } return s; }\n\ + innerTest(n: number): number { let s = 0; for (let r = 0; r < n; r++) { let f = r; while (this.at(f) === 0 && f < 9) f++; s += f; } return s; }\n\ + labeled(n: number): number { let s = 0; outer: for (let r = 0; r < n; r++) { for (let f = 0; f < 3; f++) { if (f === r) continue outer; } s += this.at(r); } return s; }\n\ +}\n"; + +#[test] +fn a_read_that_every_iteration_runs_dominates_the_back_edge() { + let m = lower(RULE_SRC); + for name in ["first", "test", "leaves", "arms", "left", "innerTest"] { + assert_eq!( + stmts_read(loop_body(&m, name), &is_at), + Paths::READ, + "{name}" + ); + } +} + +#[test] +fn a_read_some_iteration_skips_does_not() { + let m = lower(RULE_SRC); + // `continue` before the read (evaluate's square loops), a conditional + // arm, the right operand of `&&`, a nested loop that may run zero + // times, a labeled jump. + for name in ["skips", "half", "right", "inner", "labeled"] { + assert_ne!( + stmts_read(loop_body(&m, name), &is_at), + Paths::READ, + "{name}" + ); + } + // With no trusted read nothing dominates. + assert_ne!(stmts_read(loop_body(&m, "first"), &|_| false), Paths::READ); +} + +const IR_SRC: &str = "export class B {\n\ + board: number[] = [];\n\ + at(sq: number): number { return this.board[sq] ?? 0; }\n\ + ray(n: number): number { let s = 0; let i = 0; while (i < n) { const p = this.at(i & 127); if (p !== 0) break; s += 1; i += 3; } return s; }\n\ + pawn(n: number): number { let s = 0; for (let f = 0; f < n; f++) { if (this.at(f * 16) === 1) s += 1; } return s; }\n\ + some(n: number): number { let s = 0; for (let i = 0; i < n; i++) { if (i > 3) s += this.at(i & 127); } return s; }\n\ + grows(n: number): number { let s = 0; for (let i = 0; i < n; i++) { s += this.at(i & 127); this.board.push(i); } return s; }\n\ +}\n"; + +const GROWABLE: FactsArrRep = FactsArrRep { + elem: FactsElemRep::F64, + floor: 128, + dense: true, + fixed: false, +}; + +/// IR of `IR_SRC` with `this` a `B`, `board` of rep `rep`, every +/// `this.at(...)` a field read call, in its floor except `pawn`'s. +fn ir(rep: FactsRep) -> String { + let m = lower(IR_SRC); + let class = m.classes.iter().find(|c| c.name == "B").expect("B"); + let mut elision = ElisionFacts::default(); + for f in &class.methods { + elision.this_of.insert( + f.id, + FactsRecv { + class_ids: vec![class.id], + nullable: false, + checked: false, + }, + ); + } + elision.classes.insert( + class.id, + FactsClass { + display: class.name.clone(), + fixed_layout: true, + fields: vec![FactsField { + key: "board".into(), + slot: 0, + readonly: true, + kind_mask: 0x80, + ta_stable: false, + ta_kind: None, + declared: false, + reserved: false, + fns: Vec::new(), + classes: Vec::new(), + nullable: false, + rep, + }], + }, + ); + // SWC offsets are 1-based. + let at = |text: &str| IR_SRC.find(text).expect(text) as u32 + 1; + let read = FactsFieldReadCall { + field: "board".into(), + index_arg: 0, + default: Some(0f64.to_bits()), + element_offset: at("this.board[sq]"), + field_offset: at("this.board[sq]"), + in_floor: None, + }; + for (call, key, floor) in [ + ("this.at(i & 127); if", (0, 127), Some(128)), + ("this.at(f * 16)", (0, 255), None), + ("this.at(i & 127); } return", (0, 127), Some(128)), + ("this.at(i & 127); this.board", (0, 127), Some(128)), + ] { + let site = at(call); + elision.field_read_calls.insert( + site, + FactsFieldReadCall { + in_floor: floor, + ..read.clone() + }, + ); + elision.call_arg_ranges.insert(site, vec![Some(key)]); + } + elision.element_keys.insert(at("this.board[sq]"), (0, 255)); + let opts = CompileOptions { + emit_ir_only: true, + program_layouts: Arc::new(crate::layout_families::compute( + [("fb.ts", &m)], + true, + &Default::default(), + )), + program_facts: ProgramFactsView { + elision: Arc::new(elision), + ..Default::default() + }, + ..Default::default() + }; + String::from_utf8(compile_module(&m, opts).expect("fixture compiles")).expect("UTF-8 IR") +} + +/// The IR of the method whose symbol contains `__B__`. +fn method(ir: &str, name: &str) -> String { + let tag = format!("__B__{name}"); + let mut out = Vec::new(); + let mut inside = false; + for line in ir.lines() { + if line.starts_with("define ") { + inside = line.contains(&tag); + } + if inside { + out.push(line); + if line == "}" { + inside = false; + } + } + } + out.join("\n") +} + +#[test] +fn a_loop_whose_every_iteration_reads_the_board_holds_its_base() { + let ir = ir(FactsRep::Arr(GROWABLE)); + let f = method(&ir, "ray"); + assert!(f.contains("abase.install"), "guarded install\n{f}"); + // The install resolves forwarding once; the read inside the loop has + // no forwarding test of its own (C3's `arep.live`). + assert!(f.contains("abase.follow"), "{f}"); + assert!(!f.contains("arep.live"), "no per-read forwarding test\n{f}"); + // The poll re-derives the base: a second resolution after the safepoint. + let after_poll = f + .split("call void @js_gc_loop_safepoint()") + .skip(1) + .any(|tail| tail.contains("js_array_live_head")); + assert!(after_poll, "refresh after the poll\n{f}"); +} + +#[test] +fn a_read_outside_its_floor_takes_the_slot_below_the_floor() { + let ir = ir(FactsRep::Arr(GROWABLE)); + let f = method(&ir, "pawn"); + assert!(f.contains("abase.install"), "{f}"); + assert!(f.contains("abase.slot") && f.contains("abase.read"), "{f}"); + assert!( + f.lines() + .any(|l| l.contains("icmp ult i32") && l.trim_end().ends_with(", 128")), + "the dense floor bounds the slot\n{f}" + ); +} + +#[test] +fn a_loop_that_may_skip_the_read_or_grows_the_board_holds_nothing() { + let ir = ir(FactsRep::Arr(GROWABLE)); + for name in ["some", "grows"] { + let f = method(&ir, name); + assert!(!f.contains("abase."), "{name}\n{f}"); + } + // Without `Arr` no loop holds a base. + let boxed = ir_boxed(); + assert!(!boxed.contains("abase."), "{boxed}"); +} + +fn ir_boxed() -> String { + ir(FactsRep::Boxed) +} diff --git a/crates/perry-codegen/src/stmt/loops.rs b/crates/perry-codegen/src/stmt/loops.rs index d4e50842b70..c34ec2770d1 100644 --- a/crates/perry-codegen/src/stmt/loops.rs +++ b/crates/perry-codegen/src/stmt/loops.rs @@ -6776,7 +6776,21 @@ pub(crate) fn lower_for( if let Some(init_stmt) = init { lower_stmt(ctx, init_stmt)?; } + // PR-D: the element bases this loop holds (`stmt::field_base`). + let controls: Vec<&perry_hir::Expr> = condition.into_iter().chain(update).collect(); + let based = super::field_base::begin(ctx, condition, &controls, body)?; + let lowered = lower_for_after_bases(ctx, init, condition, update, body); + super::field_base::end(ctx, based); + lowered +} +fn lower_for_after_bases( + ctx: &mut FnCtx<'_>, + init: Option<&Stmt>, + condition: Option<&perry_hir::Expr>, + update: Option<&perry_hir::Expr>, + body: &[Stmt], +) -> Result<()> { if iterator_record::lower(ctx, init, condition, update, body)? { return Ok(()); } @@ -8694,6 +8708,9 @@ fn emit_armed_gc_loop_safepoint(ctx: &mut FnCtx<'_>) { blk.store(I64, &handle, &recipe.base_handle_slot); } } + // PR-D: the held element bases, from `this`'s GC-updated root. + crate::expr::index_get::field_base::emit_poll_refresh(ctx) + .expect("a held field base re-derives at the poll"); // Cached element bases of validated windows, from their refreshed handles. let element_refresh: Vec<(String, String)> = ctx .receiver_descriptors @@ -10484,6 +10501,17 @@ pub(crate) fn lower_while( ctx: &mut FnCtx<'_>, condition: &perry_hir::Expr, body: &[Stmt], +) -> Result<()> { + let based = super::field_base::begin(ctx, Some(condition), &[condition], body)?; + let lowered = lower_while_after_bases(ctx, condition, body); + super::field_base::end(ctx, based); + lowered +} + +fn lower_while_after_bases( + ctx: &mut FnCtx<'_>, + condition: &perry_hir::Expr, + body: &[Stmt], ) -> Result<()> { // A while loop is the same Number induction with no init/update clause. if super::number_local_loop::lower(ctx, None, Some(condition), None, body)? { @@ -10578,13 +10606,18 @@ pub(crate) fn lower_do_while( body: &[Stmt], condition: &perry_hir::Expr, ) -> Result<()> { - let region = super::region_loop::begin(ctx, Some(condition), body, None)?; - let lowered = super::region_loop::lower_loop(ctx, region, &mut |ctx| { - super::cold_scoped(ctx, body, &[condition], |c| { - lower_do_while_impl(c, body, condition) - }) + let based = super::field_base::begin(ctx, None, &[condition], body)?; + let region = super::region_loop::begin(ctx, Some(condition), body, None); + let lowered = region.and_then(|region| { + let lowered = super::region_loop::lower_loop(ctx, region, &mut |ctx| { + super::cold_scoped(ctx, body, &[condition], |c| { + lower_do_while_impl(c, body, condition) + }) + }); + super::region_loop::end(ctx, region); + lowered }); - super::region_loop::end(ctx, region); + super::field_base::end(ctx, based); lowered } diff --git a/crates/perry-codegen/src/stmt/mod.rs b/crates/perry-codegen/src/stmt/mod.rs index 0da67095287..116941a51e2 100644 --- a/crates/perry-codegen/src/stmt/mod.rs +++ b/crates/perry-codegen/src/stmt/mod.rs @@ -37,6 +37,9 @@ mod element_shape_loop; #[cfg(test)] mod element_shape_loop_tests; mod element_shape_native; +pub(crate) mod field_base; +#[cfg(test)] +mod field_base_tests; mod if_stmt; pub(crate) mod indexed_owner_loop; mod let_buffer_views; diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs index dd784b9a12c..3bca8eff655 100644 --- a/crates/perry/src/commands/compile/compile_env.rs +++ b/crates/perry/src/commands/compile/compile_env.rs @@ -65,6 +65,7 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[ "PERRY_FACTS_INT32_LOCALS", "PERRY_FACTS_INT_RANGES", "PERRY_FACTS_INT_DEMAND", + "PERRY_FACTS_ARRAY_BASE", "PERRY_FACTS_ARRAY_FIELDS", "PERRY_FACTS_ARRAY_FLOOR", "PERRY_FACTS_ARRAY_REPS", diff --git a/crates/perry/src/commands/compile/compile_env/tests.rs b/crates/perry/src/commands/compile/compile_env/tests.rs index ee554d4f850..7d3c987c661 100644 --- a/crates/perry/src/commands/compile/compile_env/tests.rs +++ b/crates/perry/src/commands/compile/compile_env/tests.rs @@ -323,6 +323,7 @@ fn codegen_env_vars_are_build_cache_inputs() { #[test] fn array_fact_switches_are_cache_inputs() { for name in [ + "PERRY_FACTS_ARRAY_BASE", "PERRY_FACTS_ARRAY_FIELDS", "PERRY_FACTS_ARRAY_FLOOR", "PERRY_FACTS_ARRAY_LENGTHS", diff --git a/scripts/test-verify-facts-s0.py b/scripts/test-verify-facts-s0.py index c925fbb5ad0..e12dc71d016 100644 --- a/scripts/test-verify-facts-s0.py +++ b/scripts/test-verify-facts-s0.py @@ -119,6 +119,8 @@ def oracle(source, *argv): ("array-front-negative", "arrfront", "array rep"), ("array-field-negative", "arrfield", "array rep"), ("array-b1-negative", "arrb1", "array rep"), + ("array-base-negative", "arrbase", "array rep"), + ("array-base-admit-negative", "arrbaseadm", "array rep"), ("number-call-negative", "numbercall", "numeric result"), ("field-read-call-negative", "fieldreadcall", "field read call"), ("array-undef-negative", "arrundef", "element floor"), diff --git a/scripts/verify_facts_s0/array-base-admit-negative.ts b/scripts/verify_facts_s0/array-base-admit-negative.ts new file mode 100644 index 00000000000..1f34ac3632e --- /dev/null +++ b/scripts/verify_facts_s0/array-base-admit-negative.ts @@ -0,0 +1,25 @@ +// `scan`'s loop reads the board through `at` on every iteration, but it +// also calls `grow`, which pushes past the capacity and moves the storage, +// so no loop may hold the board's element base (PR-D admission). Under +// PERRY_FACTS_SABOTAGE=arrbaseadm the loop is admitted anyway; the read +// after the first growth must report that the held base is not the live +// head. +class Board { + board: number[] = new Array(16).fill(1); + at(sq: number): number { + return this.board[sq] ?? 0; + } + grow(n: number): void { + for (let k = 0; k < n; k++) this.board.push(k); + } + scan(): number { + let s = 0; + for (let i = 0; i < 8; i++) { + s += this.at(i); + this.grow(64); + } + return s; + } +} +const b = new Board(); +console.log(b.scan(), b.board.length); diff --git a/scripts/verify_facts_s0/array-base-negative.ts b/scripts/verify_facts_s0/array-base-negative.ts new file mode 100644 index 00000000000..927065339fd --- /dev/null +++ b/scripts/verify_facts_s0/array-base-negative.ts @@ -0,0 +1,24 @@ +// `scan`'s loop reads the board through `at` on every iteration, so it +// holds the board's element base (PR-D). The board grew past its capacity +// first, so the field holds a forwarding stub. Under +// PERRY_FACTS_SABOTAGE=arrbase the install keeps the stub's handle instead +// of resolving it to the live head; the install's witness must report the +// forwarded head. +class Board { + board: number[] = new Array(16).fill(1); + at(sq: number): number { + return this.board[sq] ?? 0; + } + scan(): number { + let s = 0; + let i = 0; + while (i < 16) { + s += this.at(i); + i++; + } + return s; + } +} +const b = new Board(); +b.board[process.argv.length > 100 ? 7 : 40] = 2; +console.log(b.scan(), b.at(40), b.board.length); diff --git a/tests/parity/language/array/test_array_reps_loop_base.ts b/tests/parity/language/array/test_array_reps_loop_base.ts new file mode 100644 index 00000000000..1a75c53e6dd --- /dev/null +++ b/tests/parity/language/array/test_array_reps_loop_base.ts @@ -0,0 +1,133 @@ +// DESIGN-p4l1 §5.4 fixture 15 (PR-D): the element base of a field-held +// board held across a loop. The board grows once (`b[200] = 1`), so its +// header is a forwarding stub; hot loops then read it inside a loop that +// holds the base (every iteration reads first: the install resolves the +// stub) and outside one (the read is conditional). Then the shapes the +// installer must refuse or serve differently: a read outside the call's +// floor (passed-pawn shape), a loop that runs zero times, a `continue` +// before the read, a loop that grows the board, a loop that replaces it, +// a do-while, two fields in one loop, and nested loops. + +class Board { + board: number[] = new Array(128).fill(0); + other: number[] = new Array(16).fill(3); + at(sq: number): number { + return this.board[sq] ?? 0; + } + far(sq: number): number { + return this.other[sq] ?? -1; + } + // In a region: the read dominates the back edge. + ray(from: number, step: number): number { + let sq = from; + let n = 0; + while (sq >= 0 && sq < 128 && (sq & 0x88) === 0) { + const p = this.at(sq); + if (p !== 0) return n * 100 + p; + n++; + sq += step; + } + return n; + } + // Outside a region: some iterations skip the read. + sparse(n: number): number { + let s = 0; + for (let i = 0; i < n; i++) { + if ((i & 3) === 0) s += this.at(5); + } + return s; + } + hot(n: number): number { + let s = 0; + for (let i = 0; i < n; i++) s += this.at(5) + this.at(i & 127); + return s; + } + // The key leaves the floor: the slot below it, the call's read above. + passed(rank: number, file: number): number { + let s = 0; + for (let r = rank; r < 16; r++) { + for (let f = Math.max(0, file - 1); f <= Math.min(7, file + 1); f++) { + s += this.at(r * 16 + f); + } + } + return s; + } + never(): number { + let s = 0; + let i = 10; + while (i < 5) { + s += this.at(i); + i++; + } + return s; + } + skips(): number { + let s = 0; + for (let sq = 0; sq < 128; sq++) { + if ((sq & 0x88) !== 0) { + sq += 7; + continue; + } + s += this.at(sq); + } + return s; + } + grows(n: number): number { + let s = 0; + for (let i = 0; i < n; i++) { + s += this.at(i & 127); + this.board.push(i); + } + return s; + } + replaces(n: number, next: number[]): number { + let s = 0; + for (let i = 0; i < n; i++) { + s += this.at(i & 7); + if (i === 2) this.board = next; + } + return s; + } + once(): number { + let s = 0; + let i = 0; + do { + s += this.at(i); + i += 2; + } while (i < 20); + return s; + } + both(n: number): number { + let s = 0; + for (let i = 0; i < n; i++) s += this.at(i & 127) * 10 + this.far(i & 15); + return s; + } + nested(n: number): number { + let s = 0; + for (let i = 0; i < n; i++) { + s += this.at(i & 127); + for (let j = 0; j < 3; j++) s += this.at((i + j) & 127); + } + return s; + } +} + +const b = new Board(); +for (let i = 0; i < 128; i++) b.board[i] = (i * 7 + 3) % 5; +b.board[0] = 0; +console.log("before", b.ray(0, 1), b.hot(1000), b.sparse(1000), b.passed(6, 3)); +// One store far past the capacity: the storage moves, the header forwards. +b.board[200] = 1; +console.log("length", b.board.length, b.at(200), b.at(199), b.at(5)); +let total = 0; +for (let k = 0; k < 2000; k++) total += b.hot(64) + b.ray(k & 7, 16); +console.log("forwarded", total, b.sparse(4000)); +console.log("passed", b.passed(0, 0), b.passed(6, 7), b.passed(12, 4)); +console.log("never", b.never(), "skips", b.skips(), "once", b.once()); +console.log("both", b.both(500), "nested", b.nested(300)); +const c = new Board(); +for (let i = 0; i < 128; i++) c.board[i] = i & 3; +console.log("grows", c.grows(300), c.board.length, c.at(127), c.at(128)); +const d = new Board(); +const next = new Array(128).fill(9); +console.log("replaces", d.replaces(6, next), d.at(0)); diff --git a/tests/parity/language/array/test_array_reps_loop_base_gc.ts b/tests/parity/language/array/test_array_reps_loop_base_gc.ts new file mode 100644 index 00000000000..c3fe741cfa4 --- /dev/null +++ b/tests/parity/language/array/test_array_reps_loop_base_gc.ts @@ -0,0 +1,33 @@ +// PR-D (DESIGN-p4l1 §4.3): a loop that holds a field-held board's element +// base, called from an allocating loop, so collections run at the held +// loop's poll and between its runs. Run under PERRY_GC_MOVING_LOOP_POLLS=1 +// and a seeded PERRY_GC_STRESS, the poll's refresh must re-derive the base +// from `this`'s root every time a collection moves the board. + +class Board { + board: number[] = new Array(128).fill(0); + at(sq: number): number { + return this.board[sq] ?? 0; + } + scan(from: number): number { + let s = 0; + let i = from; + while (i < 128) { + s += this.at(i); + i += 1; + } + return s; + } +} + +let keep: number[][] = []; +let total = 0; +for (let round = 0; round < 100000; round++) { + const b = new Board(); + b.board[round & 127] = round & 15; + if ((round & 1023) === 0) b.board[300] = 1; + keep.push([round, round + 1]); + if (keep.length > 64) keep = []; + total += b.scan(round & 63); +} +console.log(total, keep.length); From 1231ef360a31c8d3fb1fd11eccb5a884bcbf18ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 08:52:27 +0100 Subject: [PATCH 03/14] wpfacts: R1 test: the labeled control's test implies no clip --- crates/perry-wpfacts/src/tests/range_tightening.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/perry-wpfacts/src/tests/range_tightening.rs b/crates/perry-wpfacts/src/tests/range_tightening.rs index 0638efdca41..5fb773f1f55 100644 --- a/crates/perry-wpfacts/src/tests/range_tightening.rs +++ b/crates/perry-wpfacts/src/tests/range_tightening.rs @@ -110,7 +110,7 @@ fn reaching() -> String { " falls(): number { let s = 0; for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 7; } s += this.at(q + 0); } return s; }\n\ inSwitch(k: number): number { let s = 0; for (let q = 0; q < 128; q++) { switch (k) { case 1: if (q > 3) { q += 200; break; } s += 1; } s += this.at(q - 0); } return s; }\n\ inTry(): number { let s = 0; for (let q = 0; q < 128; q++) { try { if (q > 3) { q += 200; continue; } } finally { s += this.at(q * 1); } } return s; }\n\ - labeled(): number { let s = 0; outer: for (let q = 0; q < 128; q++) { if (q > 3) { q += 200; continue outer; } s += this.at(q | 0); } return s; }\n\ + labeled(): number { let s = 0; outer: for (let q = 0; q < 128; q++) { if ((q & 0x88) !== 0) { q += 200; continue outer; } s += this.at(q | 0); } return s; }\n\ sumPast(): number { let s = 0; for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f + 9); return s; }", "b.falls(), b.inSwitch(1), b.inSwitch(2), b.inTry(), b.labeled(), b.sumPast()", ) From e4933d8d4931cab5f2b1c4eb9a553b5067fd6ab6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 09:22:25 +0100 Subject: [PATCH 04/14] codegen: PR-D admission: an operator over a held read of Number elements is no coercion; the arrbase fixture grows the board by pushes --- crates/perry-codegen/src/stmt/field_base.rs | 45 ++++++++++++++----- .../src/stmt/field_base_tests.rs | 5 +++ .../verify_facts_s0/array-base-negative.ts | 2 +- 3 files changed, 41 insertions(+), 11 deletions(-) diff --git a/crates/perry-codegen/src/stmt/field_base.rs b/crates/perry-codegen/src/stmt/field_base.rs index a6c34fa9165..2f533582da4 100644 --- a/crates/perry-codegen/src/stmt/field_base.rs +++ b/crates/perry-codegen/src/stmt/field_base.rs @@ -130,19 +130,26 @@ pub(crate) fn begin( .iter() .filter(|r| install.contains(&r.field.as_str()) || held.contains(r.field.as_str())) .collect(); + let is_inert = |e: &Expr| crate::rooting::expr_is_inert_primitive(ctx, e); + // A served read over Number elements yields a primitive (an element, + // `undefined` past the length, or a Number default): an operator over + // it and other inert operands runs no user code. + let primitive = |e: &Expr| { + let a = addr(e); + served + .iter() + .any(|r| r.call == a && r.rep.elem != crate::codegen::FactsElemRep::Boxed) + }; let classified = |e: &Expr| -> Option> { let a = addr(e); - served.iter().find_map(|r| { - if r.call == a { - Some((!r.in_floor).then_some(RegionEnder::ColdArmCall)) - } else if r.callee == a { - Some(None) - } else { - None - } - }) + if let Some(r) = served.iter().find(|r| r.call == a) { + return Some((!r.in_floor).then_some(RegionEnder::ColdArmCall)); + } + if served.iter().any(|r| r.callee == a) { + return Some(None); + } + (!is_inert(e) && operator_over(e, &is_inert, &primitive)).then_some(None) }; - let is_inert = |e: &Expr| crate::rooting::expr_is_inert_primitive(ctx, e); let enders = crate::collectors::region_enders_in_stmts_classified( body, controls, @@ -226,6 +233,24 @@ pub(crate) fn end(ctx: &mut FnCtx<'_>, installed: Installed) { } } +/// `e` is a coercing operator (arithmetic, bitwise, relational, unary) +/// whose operands are each inert, a served read of Number elements, or +/// such an operator in turn: ToPrimitive meets no object. +fn operator_over( + e: &Expr, + inert: &dyn Fn(&Expr) -> bool, + primitive: &dyn Fn(&Expr) -> bool, +) -> bool { + let operand = |x: &Expr| inert(x) || primitive(x) || operator_over(x, inert, primitive); + match e { + Expr::Binary { left, right, .. } | Expr::Compare { left, right, .. } => { + operand(left) && operand(right) + } + Expr::Unary { operand: x, .. } => operand(x), + _ => false, + } +} + fn addr(e: &Expr) -> usize { e as *const Expr as usize } diff --git a/crates/perry-codegen/src/stmt/field_base_tests.rs b/crates/perry-codegen/src/stmt/field_base_tests.rs index ee9de0bc595..0b63a5563c4 100644 --- a/crates/perry-codegen/src/stmt/field_base_tests.rs +++ b/crates/perry-codegen/src/stmt/field_base_tests.rs @@ -105,6 +105,7 @@ const IR_SRC: &str = "export class B {\n\ ray(n: number): number { let s = 0; let i = 0; while (i < n) { const p = this.at(i & 127); if (p !== 0) break; s += 1; i += 3; } return s; }\n\ pawn(n: number): number { let s = 0; for (let f = 0; f < n; f++) { if (this.at(f * 16) === 1) s += 1; } return s; }\n\ some(n: number): number { let s = 0; for (let i = 0; i < n; i++) { if (i > 3) s += this.at(i & 127); } return s; }\n\ + sum(n: number): number { let s = 0; for (let i = 0; i < n; i++) { s += this.at(i & 127) * 2; } return s; }\n\ grows(n: number): number { let s = 0; for (let i = 0; i < n; i++) { s += this.at(i & 127); this.board.push(i); } return s; }\n\ }\n"; @@ -167,6 +168,7 @@ fn ir(rep: FactsRep) -> String { ("this.at(f * 16)", (0, 255), None), ("this.at(i & 127); } return", (0, 127), Some(128)), ("this.at(i & 127); this.board", (0, 127), Some(128)), + ("this.at(i & 127) * 2", (0, 127), Some(128)), ] { let site = at(call); elision.field_read_calls.insert( @@ -224,6 +226,9 @@ fn a_loop_whose_every_iteration_reads_the_board_holds_its_base() { assert!(f.contains("abase.follow"), "{f}"); assert!(!f.contains("arep.live"), "no per-read forwarding test\n{f}"); // The poll re-derives the base: a second resolution after the safepoint. + // Arithmetic over the read's Number is no coercion of an object. + let g = method(&ir, "sum"); + assert!(g.contains("abase.install"), "{g}"); let after_poll = f .split("call void @js_gc_loop_safepoint()") .skip(1) diff --git a/scripts/verify_facts_s0/array-base-negative.ts b/scripts/verify_facts_s0/array-base-negative.ts index 927065339fd..66b73c70a97 100644 --- a/scripts/verify_facts_s0/array-base-negative.ts +++ b/scripts/verify_facts_s0/array-base-negative.ts @@ -20,5 +20,5 @@ class Board { } } const b = new Board(); -b.board[process.argv.length > 100 ? 7 : 40] = 2; +for (let k = 0; k < 100; k++) b.board.push(2); console.log(b.scan(), b.at(40), b.board.length); From 503c67c49882ffba192729ba48fb5f971996bf69 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 09:40:46 +0100 Subject: [PATCH 05/14] codegen: PR-D negative control arrbasepoll (the poll does not re-derive the held base) --- changelog.d/codegen-array-field-loop-base.md | 2 +- crates/perry-codegen/src/expr/index_get/field_base.rs | 7 ++++++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/changelog.d/codegen-array-field-loop-base.md b/changelog.d/codegen-array-field-loop-base.md index 888936bd4d6..9dfa2909ceb 100644 --- a/changelog.d/codegen-array-field-loop-base.md +++ b/changelog.d/codegen-array-field-loop-base.md @@ -1 +1 @@ -Performance: a loop that reads an Array held in a field of `this` on every iteration holds the Array's element base across the loop. When a field read call (`this.at(sq)` = `this.board[sq] ?? 0`) whose field is a dense whole-program `Arr` runs on every path to the loop's back edge, and nothing else in the loop can collect, call, store or allocate (its back-edge poll is the one region ender), the loop's guarded preheader loads `this.board` once, resolves a growth forwarding stub to the live head once, and keeps the head: each read in the loop is then one load at `base + 24 + 8 * i`, with no field reload, no pointer masking and no forwarding test. A read whose key can leave the call's floor tests the key against the dense floor and otherwise keeps its own read, after which the base is re-derived. The poll's slow block re-derives the base from `this`'s root after a collection. There is no second loop body. `PERRY_FACTS_ARRAY_BASE=0` turns it off; `PERRY_VERIFY_FACTS=1` tests the head at the install and at every refresh, and at every read that the held base is the live head; `PERRY_FACTS_SABOTAGE=arrbase` and `arrbaseadm` are the negative controls; `PERRY_ARRAY_BASE_DIAG=1` prints the installer's verdict per loop. +Performance: a loop that reads an Array held in a field of `this` on every iteration holds the Array's element base across the loop. When a field read call (`this.at(sq)` = `this.board[sq] ?? 0`) whose field is a dense whole-program `Arr` runs on every path to the loop's back edge, and nothing else in the loop can collect, call, store or allocate (its back-edge poll is the one region ender), the loop's guarded preheader loads `this.board` once, resolves a growth forwarding stub to the live head once, and keeps the head: each read in the loop is then one load at `base + 24 + 8 * i`, with no field reload, no pointer masking and no forwarding test. A read whose key can leave the call's floor tests the key against the dense floor and otherwise keeps its own read, after which the base is re-derived. The poll's slow block re-derives the base from `this`'s root after a collection. There is no second loop body. `PERRY_FACTS_ARRAY_BASE=0` turns it off; `PERRY_VERIFY_FACTS=1` tests the head at the install and at every refresh, and at every read that the held base is the live head; `PERRY_FACTS_SABOTAGE=arrbase`, `arrbaseadm` and `arrbasepoll` are the negative controls; `PERRY_ARRAY_BASE_DIAG=1` prints the installer's verdict per loop. diff --git a/crates/perry-codegen/src/expr/index_get/field_base.rs b/crates/perry-codegen/src/expr/index_get/field_base.rs index 45cd4e034bc..f69fee0e490 100644 --- a/crates/perry-codegen/src/expr/index_get/field_base.rs +++ b/crates/perry-codegen/src/expr/index_get/field_base.rs @@ -39,7 +39,9 @@ //! `PERRY_FACTS_ARRAY_BASE=0` turns the installer off (C3's build). //! Negative controls: `PERRY_FACTS_SABOTAGE=arrbase` installs the stub's //! handle without resolving forwarding; `arrbaseadm` admits a loop whatever -//! else ends its region (`stmt::field_base`). +//! else ends its region (`stmt::field_base`); `arrbasepoll` skips the +//! poll's refresh (exposed only by a moving collection at the poll: +//! `PERRY_GC_SCHEDULE_SEED` with the instrumented runtime). use anyhow::Result; use perry_hir::{Expr, LogicalOp}; @@ -178,6 +180,9 @@ pub(crate) fn emit_poll_refresh(ctx: &mut FnCtx<'_>) -> Result<()> { .receiver_descriptors .field_base_refreshes() .expect("every held field base must admit a back-edge poll"); + if sabotaged("arrbasepoll") { + return Ok(()); + } for base in &bases { emit_install(ctx, base)?; } From 93bb48b2f2db14e49e5dbbc8dd6a54682fe4f790 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 10:18:10 +0100 Subject: [PATCH 06/14] wpfacts: R1 exactrule sabotage is a deterministic wrong sum (the operands' hull) --- crates/perry-wpfacts/src/model.rs | 6 +++--- crates/perry-wpfacts/src/solve.rs | 7 +------ crates/perry-wpfacts/src/solve/apply.rs | 6 +++++- scripts/verify_facts_s0/range-sum-negative.ts | 12 ++++++------ 4 files changed, 15 insertions(+), 16 deletions(-) diff --git a/crates/perry-wpfacts/src/model.rs b/crates/perry-wpfacts/src/model.rs index 988cd36b101..9bc979dff00 100644 --- a/crates/perry-wpfacts/src/model.rs +++ b/crates/perry-wpfacts/src/model.rs @@ -1263,9 +1263,9 @@ pub struct Model { /// 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`): a rule result - /// keeps its first interval, a claim too narrow for the values its - /// operands grow to, which the witnesses must catch. + /// 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`). diff --git a/crates/perry-wpfacts/src/solve.rs b/crates/perry-wpfacts/src/solve.rs index d8f1482999a..8e0a721db1e 100644 --- a/crates/perry-wpfacts/src/solve.rs +++ b/crates/perry-wpfacts/src/solve.rs @@ -1947,13 +1947,8 @@ pub(crate) fn grow_range(node: &mut Node, iv: Iv) -> bool { /// 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, sabotage: bool) -> bool { +pub(crate) fn grow_rule_range(node: &mut Node, iv: Iv) -> bool { use crate::model::range::{widen, WIDEN_LIMIT}; - // Negative control (`PERRY_FACTS_SABOTAGE=exactrule`): the result keeps - // its first interval, whatever its operands grow to. - if sabotage && !node.range.is_empty() { - return false; - } let joined = node.range.join(iv); if joined == node.range { return false; diff --git a/crates/perry-wpfacts/src/solve/apply.rs b/crates/perry-wpfacts/src/solve/apply.rs index 0595f933230..8c5f5c7bbbb 100644 --- a/crates/perry-wpfacts/src/solve/apply.rs +++ b/crates/perry-wpfacts/src/solve/apply.rs @@ -1480,6 +1480,10 @@ 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)) @@ -1489,7 +1493,7 @@ impl Model { }; let d = &mut self.nodes[dst as usize]; let grew = if self.exact_rules { - crate::solve::grow_rule_range(d, iv, self.exact_rule_sabotage) + crate::solve::grow_rule_range(d, iv) } else { crate::solve::grow_range(d, iv) }; diff --git a/scripts/verify_facts_s0/range-sum-negative.ts b/scripts/verify_facts_s0/range-sum-negative.ts index 4a5671fa7e3..ba87632eeea 100644 --- a/scripts/verify_facts_s0/range-sum-negative.ts +++ b/scripts/verify_facts_s0/range-sum-negative.ts @@ -1,12 +1,12 @@ -// `at` is a field element read, and `board` is born dense with 64 +// `at` is a field element read, and `board` is born dense with 116 // elements. `sum` reads the keys `r * 16 + f` for `r, f` in `[0, 7]`: the -// hull `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. -// Under PERRY_FACTS_SABOTAGE=exactrule an interval rule's result keeps its -// first interval, so the facts claim the key is in the floor and the call -// loads the slot with no bound. The element tier's witness must report the +// sum `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. +// Under PERRY_FACTS_SABOTAGE=exactrule a sum's interval is the hull of its +// operands (`r * 16` is `[0, 112]`), so the facts claim the key is in the +// floor and the call loads the slot with no bound. The element tier's witness must report the // false proof at the key. class Board { - board: number[] = new Array(64).fill(1); + board: number[] = new Array(116).fill(1); at(sq: number): number { return this.board[sq] ?? 0; } From 13e81b54c6e4065fc885f66185da9b8111f8cba9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 10:27:59 +0100 Subject: [PATCH 07/14] verify_facts_s0: PR-D fixtures keep the board from growing in place, and the admission fixture's loop is not unrolled --- scripts/verify_facts_s0/array-base-admit-negative.ts | 8 +++++--- scripts/verify_facts_s0/array-base-negative.ts | 8 ++++++-- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/scripts/verify_facts_s0/array-base-admit-negative.ts b/scripts/verify_facts_s0/array-base-admit-negative.ts index 1f34ac3632e..75e73fd7409 100644 --- a/scripts/verify_facts_s0/array-base-admit-negative.ts +++ b/scripts/verify_facts_s0/array-base-admit-negative.ts @@ -12,9 +12,9 @@ class Board { grow(n: number): void { for (let k = 0; k < n; k++) this.board.push(k); } - scan(): number { + scan(n: number): number { let s = 0; - for (let i = 0; i < 8; i++) { + for (let i = 0; i < n; i++) { s += this.at(i); this.grow(64); } @@ -22,4 +22,6 @@ class Board { } } const b = new Board(); -console.log(b.scan(), b.board.length); +// A birth right behind the board keeps it from growing in place. +const blocker = new Board(); +console.log(b.scan(8), b.board.length, blocker.at(3)); diff --git a/scripts/verify_facts_s0/array-base-negative.ts b/scripts/verify_facts_s0/array-base-negative.ts index 66b73c70a97..e310e76201d 100644 --- a/scripts/verify_facts_s0/array-base-negative.ts +++ b/scripts/verify_facts_s0/array-base-negative.ts @@ -20,5 +20,9 @@ class Board { } } const b = new Board(); -for (let k = 0; k < 100; k++) b.board.push(2); -console.log(b.scan(), b.at(40), b.board.length); +// A birth right behind the board keeps it from growing in place +// (the runtime lengthens only the most recent nursery birth). +const blocker = new Board(); +const alias = b.board; +for (let k = 0; k < 100; k++) alias.push(2); +console.log(b.scan(), b.at(40), b.board.length, blocker.at(3)); From f0c5f36bd94a8a2f07731152100d4cb3c9dc9f24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 10:38:04 +0100 Subject: [PATCH 08/14] check_file_size: stmt/loops.rs 8320 (PR-D loop hooks) --- scripts/check_file_size.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/check_file_size.sh b/scripts/check_file_size.sh index 9aea52e1ae7..cb85ec07373 100755 --- a/scripts/check_file_size.sh +++ b/scripts/check_file_size.sh @@ -30,7 +30,7 @@ crates/perry-codegen/src/collectors/hir_facts.rs 2760 # Representation-aware expression dispatch; further decomposition is tracked in #1435. crates/perry-codegen/src/expr/mod.rs 2830 # Loop versioning and representation evidence share lowering state; decomposition is tracked in #1435. -crates/perry-codegen/src/stmt/loops.rs 8290 +crates/perry-codegen/src/stmt/loops.rs 8320 # Representation-aware map core; further decomposition is tracked in #1435. crates/perry-runtime/src/map.rs 3040 # Representation-aware set core; further decomposition is tracked in #1435. From d6f51dcbb0f4cf92dcf3e88ac5290cb4703e228a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 12:34:54 +0100 Subject: [PATCH 09/14] codegen: PR-D IR tests bound their loops by literals (an unproven parameter bound is a coercion ender) --- .../perry-codegen/src/stmt/field_base_tests.rs | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/crates/perry-codegen/src/stmt/field_base_tests.rs b/crates/perry-codegen/src/stmt/field_base_tests.rs index 0b63a5563c4..d1be6228418 100644 --- a/crates/perry-codegen/src/stmt/field_base_tests.rs +++ b/crates/perry-codegen/src/stmt/field_base_tests.rs @@ -42,10 +42,16 @@ fn loop_body<'m>(m: &'m Module, name: &str) -> &'m [Stmt] { Some(body.as_slice()) } Stmt::Labeled { body, .. } => find(std::slice::from_ref(body.as_ref())), + Stmt::If { + then_branch, + else_branch, + .. + } => find(then_branch).or_else(|| else_branch.as_deref().and_then(find)), + Stmt::Try { body, .. } => find(body), _ => None, }) } - find(&f.body).unwrap_or_else(|| panic!("a loop in {name}")) + find(&f.body).unwrap_or_else(|| panic!("a loop in {name}: {:.600?}", f.body)) } /// A call `this.at(...)`. @@ -102,11 +108,11 @@ fn a_read_some_iteration_skips_does_not() { const IR_SRC: &str = "export class B {\n\ board: number[] = [];\n\ at(sq: number): number { return this.board[sq] ?? 0; }\n\ - ray(n: number): number { let s = 0; let i = 0; while (i < n) { const p = this.at(i & 127); if (p !== 0) break; s += 1; i += 3; } return s; }\n\ - pawn(n: number): number { let s = 0; for (let f = 0; f < n; f++) { if (this.at(f * 16) === 1) s += 1; } return s; }\n\ - some(n: number): number { let s = 0; for (let i = 0; i < n; i++) { if (i > 3) s += this.at(i & 127); } return s; }\n\ - sum(n: number): number { let s = 0; for (let i = 0; i < n; i++) { s += this.at(i & 127) * 2; } return s; }\n\ - grows(n: number): number { let s = 0; for (let i = 0; i < n; i++) { s += this.at(i & 127); this.board.push(i); } return s; }\n\ + ray(n: number): number { let s = 0; let i = 0; while (i < 100) { const p = this.at(i & 127); if (p !== 0) break; s += 1; i += 3; } return s; }\n\ + pawn(n: number): number { let s = 0; for (let f = 0; f < 100; f++) { if (this.at(f * 16) === 1) s += 1; } return s; }\n\ + some(n: number): number { let s = 0; for (let i = 0; i < 100; i++) { if (i > 3) s += this.at(i & 127); } return s; }\n\ + sum(n: number): number { let s = 0; for (let i = 0; i < 100; i++) { s += this.at(i & 127) * 2; } return s; }\n\ + grows(n: number): number { let s = 0; for (let i = 0; i < 100; i++) { s += this.at(i & 127); this.board.push(i); } return s; }\n\ }\n"; const GROWABLE: FactsArrRep = FactsArrRep { From a0b546ec527ed51eb9db9bd8d465b7ce377cd23e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 13:14:04 +0100 Subject: [PATCH 10/14] S0: R1 fixtures read through the b1 call with a local key (a loop-counter key goes to the index method clone) --- .../verify_facts_s0/leaving-write-negative.ts | 32 +++++++++++-------- scripts/verify_facts_s0/range-sum-negative.ts | 22 +++++++------ 2 files changed, 30 insertions(+), 24 deletions(-) diff --git a/scripts/verify_facts_s0/leaving-write-negative.ts b/scripts/verify_facts_s0/leaving-write-negative.ts index a28ad65fa2f..13cbcf638d6 100644 --- a/scripts/verify_facts_s0/leaving-write-negative.ts +++ b/scripts/verify_facts_s0/leaving-write-negative.ts @@ -1,26 +1,30 @@ // `at` is a field element read, and `board` is born dense with 16 -// elements. In `walk` the counter write `q += 20` is in a branch that falls -// through to the read, so the read's key reaches past the floor (its value -// is the `?? 0`). Under PERRY_FACTS_SABOTAGE=leavingwrite every branch's -// writes are dropped from the reads after it, so the facts claim the key is -// the loop test's `[0, 15]`, in the floor, and the call loads the slot with -// no bound. The element tier's witness must report the false proof at the -// key. +// elements. In `walk` the guard `q < 16` narrows `q`, and the write +// `q += 20` is in a branch that falls through to the read, so the read's key +// reaches past the floor (its value is the `?? 0`). Under +// PERRY_FACTS_SABOTAGE=leavingwrite every branch's writes are dropped from +// the reads after it, so the facts claim the key is the guard's `[3, 15]`, +// in the floor, and the call loads the slot with no bound. The element +// tier's witness must report the false proof at the key. class Board { board: number[] = new Array(16).fill(1); + ep: number = process.argv.length > 100 ? 3 : 5; + far: boolean = process.argv.length < 100; at(sq: number): number { return this.board[sq] ?? 0; } - walk(n: number): number { - let s = 0; - for (let q = 0; q < 16; q++) { - if (q === n) { + walk(): number { + let q = this.ep; + if (q < 16) { + if (this.far) { q += 20; } - s += this.at(q); + return this.at(q); } - return s; + return -1; } } const b = new Board(); -console.log(b.walk(process.argv.length > 100 ? 99 : 5)); +let s = 0; +for (let i = 0; i < 3; i++) s += b.walk() + 1; +console.log(s); diff --git a/scripts/verify_facts_s0/range-sum-negative.ts b/scripts/verify_facts_s0/range-sum-negative.ts index ba87632eeea..709bdd9e652 100644 --- a/scripts/verify_facts_s0/range-sum-negative.ts +++ b/scripts/verify_facts_s0/range-sum-negative.ts @@ -1,20 +1,22 @@ // `at` is a field element read, and `board` is born dense with 116 -// elements. `sum` reads the keys `r * 16 + f` for `r, f` in `[0, 7]`: the -// sum `[0, 119]` leaves the floor, and the reads past it are the `?? 0`. +// elements. `probe` reads the key `ep + 112` with `ep` in `[3, 5]`: the sum +// `[115, 117]` leaves the floor, and the read past it is the `?? 0`. // Under PERRY_FACTS_SABOTAGE=exactrule a sum's interval is the hull of its -// operands (`r * 16` is `[0, 112]`), so the facts claim the key is in the -// floor and the call loads the slot with no bound. The element tier's witness must report the -// false proof at the key. +// operands (`[3, 112]`), so the facts claim the key is in the floor and the +// call loads the slot with no bound. The element tier's witness must report +// the false proof at the key. class Board { board: number[] = new Array(116).fill(1); + ep: number = process.argv.length > 100 ? 3 : 5; at(sq: number): number { return this.board[sq] ?? 0; } - sum(): number { - let s = 0; - for (let r = 0; r < 8; r++) for (let f = 0; f < 8; f++) s += this.at(r * 16 + f); - return s; + probe(): number { + const ep = this.ep; + return this.at(ep) * 10 + this.at(ep + 112); } } const b = new Board(); -console.log(b.sum()); +let s = 0; +for (let i = 0; i < 3; i++) s += b.probe(); +console.log(s); From b5fd2aa81066ab7132b7e55a15733a0aa126e9e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 13:23:17 +0100 Subject: [PATCH 11/14] codegen: PR-D tests name FactsArrRep's im (merged main) --- crates/perry-codegen/src/stmt/field_base_tests.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/perry-codegen/src/stmt/field_base_tests.rs b/crates/perry-codegen/src/stmt/field_base_tests.rs index d1be6228418..d70ea179d0f 100644 --- a/crates/perry-codegen/src/stmt/field_base_tests.rs +++ b/crates/perry-codegen/src/stmt/field_base_tests.rs @@ -120,6 +120,7 @@ const GROWABLE: FactsArrRep = FactsArrRep { floor: 128, dense: true, fixed: false, + im: false, }; /// IR of `IR_SRC` with `this` a `B`, `board` of rep `rep`, every From 3fe1ade35fa5328713bbb70b52274764c0d79c52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 14:48:26 +0100 Subject: [PATCH 12/14] codegen: an unsigned bound absorbs the element key's sign test (N10) An element read through the canonical key split tested the key's sign and then bounded it with an unsigned compare. The tier's bound already declines a negative key (it is at least 2^31 unsigned), so the sign test moves to the tier's miss arm: a negative key leaves there for the exact property-key arm, a non-negative miss keeps the tier's cold read. A widened native key is no longer mapped to -1 by a select, on reads and on the guarded stores. Reads whose key is proven in range have no bound and keep the split's test. PERRY_UNSIGNED_BOUND=0 turns it off (a compile-cache input). Check mode tests that only non-negative keys reach a tier's cold read (fact "unsigned bound"); PERRY_FACTS_SABOTAGE=unsignedbound drops the exit (S0 unsigned-bound-negative). Parity fixture test_unsigned_bound.ts covers -1, -0, NaN, 2^31, 2^32-1, 1.5, string keys, holes and length 0. --- changelog.d/codegen-unsigned-bound.md | 1 + .../src/expr/index_get/guarded_array.rs | 99 ++++++++++++++++ .../src/expr/index_get/proven_array.rs | 36 +++++- .../src/expr/index_get/runtime_key.rs | 39 +++++-- crates/perry-codegen/src/expr/index_key.rs | 101 +++++++++++++++++ crates/perry-codegen/src/expr/index_set.rs | 5 +- .../src/expr/index_set_guarded.rs | 6 +- .../src/verify_facts/coverage.rs | 2 + .../perry/src/commands/compile/compile_env.rs | 1 + .../src/commands/compile/compile_env/tests.rs | 11 ++ scripts/test-verify-facts-s0.py | 1 + .../unsigned-bound-negative.ts | 23 ++++ .../language/array/test_unsigned_bound.ts | 106 ++++++++++++++++++ 13 files changed, 417 insertions(+), 14 deletions(-) create mode 100644 changelog.d/codegen-unsigned-bound.md create mode 100644 scripts/verify_facts_s0/unsigned-bound-negative.ts create mode 100644 tests/parity/language/array/test_unsigned_bound.ts diff --git a/changelog.d/codegen-unsigned-bound.md b/changelog.d/codegen-unsigned-bound.md new file mode 100644 index 00000000000..39187e21884 --- /dev/null +++ b/changelog.d/codegen-unsigned-bound.md @@ -0,0 +1 @@ +Performance: an element read or store whose key is not proven non-negative no longer tests the key's sign in front of its bound. The element tiers already bound every element arm with one unsigned compare (`idx , + arr_box: &str, + idx_i32: &str, + block_prefix: &str, + require_numeric_layout: bool, + coerce_numeric_fallback: bool, + receiver_slot: Option<&str>, + negative_exit: Option<&str>, +) -> Result { + lower_guarded_array_index_get_with_index( + ctx, + arr_box, + GuardedArrayIndex::Signed(idx_i32), + block_prefix, + require_numeric_layout, + coerce_numeric_fallback, + receiver_slot, + negative_exit, + ) +} + +/// N10 (CENSUS-residual cause i): the element tier a split key enters has +/// an unsigned bound in front of every element arm, so the split's sign +/// test can move to the tier's miss arm. The guarded tier bounds every hit +/// (`idx ) -> bool { + crate::expr::index_key::unsigned_bound() + && match proven { + Some(fact) => super::proven_array::bounds_key(fact), + None => !typed_feedback_emission_enabled(), + } +} + +/// The start of a tier's miss arm under N10: a negative key leaves for +/// `negative_exit` (the split's runtime-key arm, which reads the original +/// key), so only a non-negative key reaches the cold read that follows, +/// exactly as when the split tested the sign first. Check mode +/// (`PERRY_VERIFY_FACTS=1`) tests that claim on the cold read's key; the +/// negative control `PERRY_FACTS_SABOTAGE=unsignedbound` drops the exit. +pub(super) fn emit_negative_exit(ctx: &mut FnCtx<'_>, idx_i32: &str, negative_exit: Option<&str>) { + let Some(exit) = negative_exit else { + return; + }; + crate::verify_facts::consumed( + crate::verify_facts::Fact::UnsignedBound, + || serde_json::json!({ "bound": "unsigned" }), + ); + if !super::field_base::sabotaged("unsignedbound") { + let cold = ctx.new_block("ubound.cold"); + let cold_l = ctx.block_label(cold); + let negative = ctx.block().icmp_slt(I32, idx_i32, "0"); + ctx.block().cond_br(&negative, exit, &cold_l); + ctx.current_block = cold; + } + if !crate::verify_facts::enabled() { + return; + } + crate::verify_facts::covered( + crate::verify_facts::Fact::UnsignedBound, + || serde_json::json!({ "bound": "unsigned" }), + ); + let miss = ctx.new_block("ubound.verify_miss"); + let next = ctx.new_block("ubound.admitted"); + let (miss_l, next_l) = (ctx.block_label(miss), ctx.block_label(next)); + crate::verify_facts::tick(ctx); + let nonnegative = ctx.block().icmp_sge(I32, idx_i32, "0"); + ctx.block().cond_br(&nonnegative, &next_l, &miss_l); + ctx.current_block = miss; + let site = crate::verify_facts::site_arg( + ctx, + "a negative key at an element tier's cold read", + crate::verify_facts::Fact::UnsignedBound, + &[], + ); + let key = ctx.block().sitofp(I32, idx_i32, DOUBLE); + let _ = crate::verify_facts::check( + ctx, + I32, + "perry_wpfacts_check_miss", + &[(DOUBLE, &key)], + &site, + ); + ctx.block().unreachable(); + ctx.current_block = next; +} + /// The same indexed read with a compiler proof of a nonnegative u32 index. /// Retain its original JS number on the cold path, including indices > i32::MAX. pub(super) fn lower_unsigned_array_index_get( @@ -376,6 +471,7 @@ pub(super) fn lower_unsigned_array_index_get( false, false, receiver_slot, + None, ) } @@ -384,6 +480,7 @@ enum GuardedArrayIndex<'a> { Unsigned { i32_value: &'a str, number: &'a str }, } +#[allow(clippy::too_many_arguments)] fn lower_guarded_array_index_get_with_index( ctx: &mut FnCtx<'_>, arr_box: &str, @@ -392,6 +489,7 @@ fn lower_guarded_array_index_get_with_index( require_numeric_layout: bool, coerce_numeric_fallback: bool, receiver_slot: Option<&str>, + negative_exit: Option<&str>, ) -> Result { let canonical = matches!(index, GuardedArrayIndex::Signed(_)); let (idx_i32, unsigned_index) = match index { @@ -577,6 +675,7 @@ fn lower_guarded_array_index_get_with_index( ]; ctx.current_block = fallback_idx; let cold_mode = ctx.block().phi(I64, &cold_inputs); + emit_negative_exit(ctx, idx_i32, negative_exit); crate::expr::store_census::bump(ctx, crate::expr::store_census::ELEM_READ_FALLBACK); let idx_box = unsigned_index .map(str::to_owned) diff --git a/crates/perry-codegen/src/expr/index_get/proven_array.rs b/crates/perry-codegen/src/expr/index_get/proven_array.rs index dbcfa5f96bc..a171db81f12 100644 --- a/crates/perry-codegen/src/expr/index_get/proven_array.rs +++ b/crates/perry-codegen/src/expr/index_get/proven_array.rs @@ -222,7 +222,7 @@ pub(crate) fn lower_in_floor( number: rep.elem != crate::codegen::FactsElemRep::Boxed, receiver: Receiver::Field, }; - lower_rep(ctx, arr_box, idx_i32, read, false) + lower_rep(ctx, arr_box, idx_i32, read, false, None) } /// `e` is an element read the tier loads below a dense floor and whose @@ -287,9 +287,35 @@ pub(super) fn lower( fact: Proven, numeric: bool, ) -> String { + lower_bounded(ctx, arr_box, idx_i32, fact, numeric, None) +} + +/// The read under `fact` has an unsigned bound in front of its load: the +/// key is not proven below the floor (`idx bool { + match fact { + Proven::Rep(read) => !read.in_floor, + Proven::Fixed(fact) => !fact.key_in_bounds, + } +} + +/// [`lower`] whose key is not sign-tested when `negative_exit` is set +/// (`bounds_key` holds): the miss arm sends a negative key there first +/// (`guarded_array::emit_negative_exit`). +pub(super) fn lower_bounded( + ctx: &mut FnCtx<'_>, + arr_box: &str, + idx_i32: &str, + fact: Proven, + numeric: bool, + negative_exit: Option<&str>, +) -> String { + debug_assert!(negative_exit.is_none() || bounds_key(fact)); match fact { - Proven::Rep(read) => lower_rep(ctx, arr_box, idx_i32, read, numeric), - Proven::Fixed(fact) => lower_fixed(ctx, arr_box, idx_i32, fact, numeric), + Proven::Rep(read) => lower_rep(ctx, arr_box, idx_i32, read, numeric, negative_exit), + Proven::Fixed(fact) => lower_fixed(ctx, arr_box, idx_i32, fact, numeric, negative_exit), } } @@ -300,6 +326,7 @@ fn lower_rep( idx_i32: &str, read: RepRead, numeric: bool, + negative_exit: Option<&str>, ) -> String { let r = read.rep; crate::expr::store_census::bump(ctx, crate::expr::store_census::ELEM_READ_OTHER_TIER); @@ -374,6 +401,7 @@ fn lower_rep( ctx.block().br(&merge_label); ctx.current_block = cold_idx; + super::guarded_array::emit_negative_exit(ctx, idx_i32, negative_exit); let idx_box = ctx.block().sitofp(I32, idx_i32, DOUBLE); // Mode 2: the exact arguments, no absence proof (`emit_read_cold`). let cold = super::guarded_array::emit_read_cold( @@ -394,6 +422,7 @@ fn lower_fixed( idx_i32: &str, fact: FactsElementRead, numeric: bool, + negative_exit: Option<&str>, ) -> String { crate::expr::store_census::bump(ctx, crate::expr::store_census::ELEM_READ_OTHER_TIER); crate::verify_facts::consumed( @@ -438,6 +467,7 @@ fn lower_fixed( blk.cond_br(&hit, &merge_label, &cold_label); ctx.current_block = cold_idx; + super::guarded_array::emit_negative_exit(ctx, idx_i32, negative_exit); let idx_box = ctx.block().sitofp(I32, idx_i32, DOUBLE); // Mode 2: the exact arguments, no absence proof (`emit_read_cold`). let cold = super::guarded_array::emit_read_cold( diff --git a/crates/perry-codegen/src/expr/index_get/runtime_key.rs b/crates/perry-codegen/src/expr/index_get/runtime_key.rs index 542b673effd..20b2301ee37 100644 --- a/crates/perry-codegen/src/expr/index_get/runtime_key.rs +++ b/crates/perry-codegen/src/expr/index_get/runtime_key.rs @@ -18,7 +18,7 @@ use anyhow::Result; use crate::types::{DOUBLE, I32}; -use super::{lower_guarded_array_index_get, FnCtx}; +use super::FnCtx; pub(super) fn lower_array_index_get_via_runtime_key( ctx: &mut FnCtx<'_>, @@ -70,19 +70,39 @@ pub(super) fn lower_array_index_get_via_canonical_i32_split( let runtime_label = ctx.block_label(runtime_idx); let merge_label = ctx.block_label(merge_idx); - let idx_i32 = crate::expr::index_key::normalize(ctx, idx_double, Some(index)); - let is_canonical_i32 = ctx.block().icmp_sge(I32, &idx_i32, "0"); - ctx.block() - .cond_br(&is_canonical_i32, &element_label, &runtime_label); + // N10: when every element arm of the tier is behind `idx { - super::proven_array::lower(ctx, arr_box, &idx_i32, fact, coerce_numeric_fallback) - } - None => lower_guarded_array_index_get( + Some(fact) => super::proven_array::lower_bounded( + ctx, + arr_box, + &idx_i32, + fact, + coerce_numeric_fallback, + negative_exit.as_deref(), + ), + None => super::guarded_array::lower_guarded_array_index_get_bounded( ctx, arr_box, &idx_i32, @@ -90,6 +110,7 @@ pub(super) fn lower_array_index_get_via_canonical_i32_split( require_numeric_layout, coerce_numeric_fallback, receiver_slot, + negative_exit.as_deref(), )?, }; let element_end = ctx.block().label.clone(); diff --git a/crates/perry-codegen/src/expr/index_key.rs b/crates/perry-codegen/src/expr/index_key.rs index 4576b050132..e6209123e51 100644 --- a/crates/perry-codegen/src/expr/index_key.rs +++ b/crates/perry-codegen/src/expr/index_key.rs @@ -65,6 +65,35 @@ pub(super) fn is_char_code(ctx: &FnCtx<'_>, expr: &Expr) -> bool { /// another block. The cast's input dominates exactly the same uses as its /// output; signed negatives and unsigned values above i32::MAX decline. pub(super) fn normalize(ctx: &mut FnCtx<'_>, key: &str, expr: Option<&Expr>) -> String { + normalize_keyed(ctx, key, expr, false) +} + +/// [`normalize`] for a consumer whose every element arm is behind an +/// unsigned bound (`idx , key: &str, expr: Option<&Expr>) -> String { + normalize_keyed(ctx, key, expr, unsigned_bound()) +} + +/// `PERRY_UNSIGNED_BOUND=0`: every element read and store keeps its sign +/// test in front of the bound (N10 off). +pub(crate) fn unsigned_bound() -> bool { + static ON: std::sync::OnceLock = std::sync::OnceLock::new(); + *ON.get_or_init(|| { + !matches!( + std::env::var("PERRY_UNSIGNED_BOUND").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ) + }) +} + +fn normalize_keyed(ctx: &mut FnCtx<'_>, key: &str, expr: Option<&Expr>, wrap: bool) -> String { let source = ctx .func .blocks() @@ -72,6 +101,9 @@ pub(super) fn normalize(ctx: &mut FnCtx<'_>, key: &str, expr: Option<&Expr>) -> .rev() .find_map(|b| b.widened_i32_source(key)); if let Some(index) = source { + if wrap { + return index; + } let valid = ctx.block().icmp_sge(I32, &index, "0"); return ctx.block().select(I1, &valid, I32, &index, "-1"); } @@ -516,4 +548,73 @@ mod tests { ); } } + + /// `key | 0`: a native i32 widened to the key's double. + fn int_key() -> Expr { + Expr::Binary { + op: BinaryOp::BitOr, + left: Box::new(Expr::NumberCoerce(Box::new(Expr::LocalGet(2)))), + right: Box::new(Expr::Integer(0)), + } + } + + /// N10: a widened native key enters the bounded tier as it is. No + /// select maps it to -1 and the split does not branch on its sign; the + /// tier's miss arm sends a negative key to the runtime-key arm. + #[test] + fn widened_key_read_has_its_sign_test_on_the_miss_arm_only() { + let ir = read_ir(int_key(), vec![]); + assert!(!ir.contains(", i32 -1"), "the -1 select is gone: {ir}"); + let entry = ir + .split_once("define double @") + .and_then(|(_, f)| f.split("\naidx.canonical.").next()) + .unwrap_or_else(|| panic!("no split: {ir}")); + assert!(!entry.contains("icmp sge i32"), "{entry}"); + let miss = ir + .split_once("\nubound.cold.") + .map(|(head, _)| head.rsplit("\n\n").next().unwrap_or(head)) + .unwrap_or_else(|| panic!("no negative exit: {ir}")); + assert!( + miss.contains("icmp slt i32") && miss.contains("aidx.runtime_key"), + "the miss arm tests the sign and leaves for the runtime key: {miss}" + ); + } + + /// N10, negative controls: a key the normalizer admits still declines + /// NaN, fractions and tags as -1 (now behind the unsigned bound), and + /// the runtime-key arm keeps the original double. + #[test] + fn number_key_keeps_its_normalizer_and_the_exact_runtime_arm() { + let ir = read_ir(Expr::LocalGet(2), vec![]); + assert!( + ir.contains("call i32 @perry_array_index_normalize_i32"), + "{ir}" + ); + assert!(ir.contains("ubound.cold"), "{ir}"); + let runtime_block = ir + .split_once("\naidx.runtime_key.") + .map(|(_, rest)| rest.split("\n\n").next().unwrap_or(rest)) + .unwrap_or_else(|| panic!("no runtime-key block: {ir}")); + assert!( + runtime_block.contains("call double @perry_array_read_cold_shared(double %arg1"), + "{runtime_block}" + ); + } + + /// N10 on the store side: the guarded store's one bound is + /// `idx , idx_double: &str) -> String { - super::index_key::normalize(ctx, idx_double, None) + super::index_key::normalize_unsigned(ctx, idx_double, None) } /// The raw-f64 element-kind bits in `_reserved`: `GC_ARRAY_RAW_F64_LAYOUT` diff --git a/crates/perry-codegen/src/verify_facts/coverage.rs b/crates/perry-codegen/src/verify_facts/coverage.rs index 8a28d859315..a490262ef18 100644 --- a/crates/perry-codegen/src/verify_facts/coverage.rs +++ b/crates/perry-codegen/src/verify_facts/coverage.rs @@ -44,6 +44,7 @@ pub(crate) enum Fact { Signature, ArrayRep, ConstArray, + UnsignedBound, } impl Fact { pub(super) fn name(self) -> &'static str { @@ -87,6 +88,7 @@ impl Fact { Self::Signature => "signature", Self::ArrayRep => "array rep", Self::ConstArray => "constant array", + Self::UnsignedBound => "unsigned bound", } } } diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs index 4bb1479ef16..b7f0a503e67 100644 --- a/crates/perry/src/commands/compile/compile_env.rs +++ b/crates/perry/src/commands/compile/compile_env.rs @@ -240,6 +240,7 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[ "PERRY_TYPED_LOCALS", "PERRY_U8_INLINE_READ", "PERRY_UNBOXED_CLASS_FIELDS", + "PERRY_UNSIGNED_BOUND", "PERRY_VERIFY_FACTS", "PERRY_VERIFY_NATIVE_REGIONS", "PERRY_VISIONOS_SYSROOT", diff --git a/crates/perry/src/commands/compile/compile_env/tests.rs b/crates/perry/src/commands/compile/compile_env/tests.rs index 8bf86dc4b58..d554d166efa 100644 --- a/crates/perry/src/commands/compile/compile_env/tests.rs +++ b/crates/perry/src/commands/compile/compile_env/tests.rs @@ -362,6 +362,17 @@ fn range_tightening_switches_are_cache_inputs() { } } +/// N10: the unsigned-bound switch changes the element reads' and stores' +/// key admission (the sign test in front of the bound), so `=0` must never +/// reuse an `=1` object. +#[test] +fn unsigned_bound_switch_is_a_cache_input() { + assert!( + COMPILE_ENV_VARS.contains(&"PERRY_UNSIGNED_BOUND"), + "PERRY_UNSIGNED_BOUND must key the compile caches" + ); +} + /// N4: the cold-path switch changes helper declarations, call-site /// attributes and branch weights, so `=0` must never reuse an `=1` object. #[test] diff --git a/scripts/test-verify-facts-s0.py b/scripts/test-verify-facts-s0.py index 39fdd16eb89..8e80a6b2d40 100644 --- a/scripts/test-verify-facts-s0.py +++ b/scripts/test-verify-facts-s0.py @@ -124,6 +124,7 @@ def oracle(source, *argv): ("array-base-admit-negative", "arrbaseadm", "array rep"), ("range-sum-negative", "exactrule", "array rep"), ("leaving-write-negative", "leavingwrite", "array rep"), + ("unsigned-bound-negative", "unsignedbound", "unsigned bound"), ("number-call-negative", "numbercall", "numeric result"), ("field-read-call-negative", "fieldreadcall", "field read call"), ("array-undef-negative", "arrundef", "element floor"), diff --git a/scripts/verify_facts_s0/unsigned-bound-negative.ts b/scripts/verify_facts_s0/unsigned-bound-negative.ts new file mode 100644 index 00000000000..e2a07672d81 --- /dev/null +++ b/scripts/verify_facts_s0/unsigned-bound-negative.ts @@ -0,0 +1,23 @@ +// N10: `at` reads `this.board[k | 0]` with no sign test in front of the +// bound. `idx 100 ? 5 : 3; + at(sq: number): number { + return this.board[sq | 0] ?? 0; + } + probe(): number { + const ep = this.ep; + return this.at(ep) * 100 + this.at(ep - 16) * 10 + this.at(ep + 16); + } +} +const b = new Board(); +let s = 0; +for (let i = 0; i < 3; i++) s += b.probe(); +const plain: number[] = [4, 5, 6]; +const k = process.argv.length > 100 ? 1 : -2; +console.log(s, plain[k | 0] ?? 7); diff --git a/tests/parity/language/array/test_unsigned_bound.ts b/tests/parity/language/array/test_unsigned_bound.ts new file mode 100644 index 00000000000..4ff86ffefbd --- /dev/null +++ b/tests/parity/language/array/test_unsigned_bound.ts @@ -0,0 +1,106 @@ +// N10 (unsigned bound): an element read or store whose key is not tested for +// sign before the bound. `idx Date: Tue, 10 Nov 2026 15:43:35 +0100 Subject: [PATCH 13/14] codegen: N10 unit tests assert the exit branch and the runtime arm's mode --- crates/perry-codegen/src/expr/index_key.rs | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/crates/perry-codegen/src/expr/index_key.rs b/crates/perry-codegen/src/expr/index_key.rs index e6209123e51..5b28324ce8b 100644 --- a/crates/perry-codegen/src/expr/index_key.rs +++ b/crates/perry-codegen/src/expr/index_key.rs @@ -570,13 +570,20 @@ mod tests { .and_then(|(_, f)| f.split("\naidx.canonical.").next()) .unwrap_or_else(|| panic!("no split: {ir}")); assert!(!entry.contains("icmp sge i32"), "{entry}"); - let miss = ir - .split_once("\nubound.cold.") - .map(|(head, _)| head.rsplit("\n\n").next().unwrap_or(head)) + // The miss arm's exit: a negative key to the runtime-key arm, the + // rest to the tier's cold read. + let exit = ir + .lines() + .find(|l| l.contains("label %aidx.runtime_key.") && l.contains("label %ubound.cold.")) .unwrap_or_else(|| panic!("no negative exit: {ir}")); + let cond = exit + .split_whitespace() + .nth(2) + .map(|c| c.trim_end_matches(',')) + .unwrap_or_else(|| panic!("{exit}")); assert!( - miss.contains("icmp slt i32") && miss.contains("aidx.runtime_key"), - "the miss arm tests the sign and leaves for the runtime key: {miss}" + ir.contains(&format!("{cond} = icmp slt i32")), + "the exit tests the sign: {ir}" ); } @@ -595,8 +602,10 @@ mod tests { .split_once("\naidx.runtime_key.") .map(|(_, rest)| rest.split("\n\n").next().unwrap_or(rest)) .unwrap_or_else(|| panic!("no runtime-key block: {ir}")); + // Mode 0: the original key, the exact property-key read. assert!( - runtime_block.contains("call double @perry_array_read_cold_shared(double %arg1"), + runtime_block.contains("call double @perry_array_read_cold_shared(") + && runtime_block.contains(", i64 0)"), "{runtime_block}" ); } From 4ba7832307bc2d57bc930f47b3ed5fb9665e9ad8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Tue, 10 Nov 2026 16:04:38 +0100 Subject: [PATCH 14/14] codegen: the any-key claim test expects N10's miss-arm sign test --- crates/perry-codegen/src/expr/index_get_claim_tests.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/crates/perry-codegen/src/expr/index_get_claim_tests.rs b/crates/perry-codegen/src/expr/index_get_claim_tests.rs index 8c2ea0b1481..3ac7d84be41 100644 --- a/crates/perry-codegen/src/expr/index_get_claim_tests.rs +++ b/crates/perry-codegen/src/expr/index_get_claim_tests.rs @@ -830,8 +830,16 @@ fn any_typed_dynamic_key_takes_the_numeric_tiers_when_it_is_an_array_index() { assert!(ir.contains("aidx.canonical") && ir.contains("aidx.runtime_key")); // The "integer-valued double in [0, 2^32)" test is the shared pure // normalizer (`memory(none)`, a GC leaf) and a sign test of its result. + // N10: the tier's unsigned bound declines the normalizer's `-1`, and the + // sign test sits on the tier's miss arm (`icmp slt`, `ubound.cold`); with + // `PERRY_UNSIGNED_BOUND=0` it is the split's `icmp sge` again. + let sign_test = if crate::expr::index_key::unsigned_bound() { + ir.contains("icmp slt i32 %") && ir.contains("ubound.cold") + } else { + ir.contains("icmp sge i32 %") + }; assert!( - ir.contains("call i32 @perry_array_index_normalize_i32(") && ir.contains("icmp sge i32 %"), + ir.contains("call i32 @perry_array_index_normalize_i32(") && sign_test, "the dynamic key must be normalized by the shared index helper:\n{ir}" ); assert!(ir.contains("aidx.dynamic.guard.deref") && ir.contains("aidx.dynamic.fast"));