diff --git a/benchmarks/repsel_census/baseline.json b/benchmarks/repsel_census/baseline.json index f9d3fb3609..50ad8d908d 100644 --- a/benchmarks/repsel_census/baseline.json +++ b/benchmarks/repsel_census/baseline.json @@ -94,7 +94,7 @@ "ptr-shape": 0, "ptr-shape-consumed": 0, "ptr-numarray": 0, - "canonical-i32": 2, + "canonical-i32": 3, "canonical-u32": 1, "canonical-str": 1, "int-valued-ta": 0, @@ -161,6 +161,30 @@ "unconsumed_mechanisms": {}, "consumption_sites": {} }, + { + "name": "fixture_loop_bounded_i32", + "role": "liveness", + "source": "benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts", + "floors": { + "ptr-shape": 0, + "ptr-shape-consumed": 0, + "ptr-numarray": 0, + "canonical-i32": 3, + "canonical-u32": 0, + "canonical-str": 0, + "int-valued-ta": 0, + "spec-abi-entry": 1, + "spec-abi-taptr-slot": 0 + }, + "candidates": { + "ptr-shape": 0, + "ptr-numarray": 0, + "canonical-slot": 5, + "int-valued-ta": 0, + "spec-abi": 4 + }, + "unconsumed_mechanisms": {} + }, { "name": "batch", "role": "corpus", @@ -620,7 +644,7 @@ "candidates": { "ptr-shape": 0, "ptr-numarray": 1, - "canonical-slot": 5, + "canonical-slot": 4, "int-valued-ta": 0, "spec-abi": 0 }, @@ -628,5 +652,5 @@ "consumption_sites": {} } ], - "generated_at": "2026-07-31T05:15:37.361861Z" + "generated_at": "2026-07-31T05:53:44.935156Z" } diff --git a/benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts b/benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts new file mode 100644 index 0000000000..ea61a8f77c --- /dev/null +++ b/benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts @@ -0,0 +1,79 @@ +// Liveness fixture for the monotone loop-induction i32 range proof (#7110). +// +// `fixture_canonical_slots.ts` proves canonical-i32 on STRAIGHT-LINE bitwise +// locals and says so in its own comment — it deliberately avoids loops, because +// before #7110 a loop counter could not select the canonical rep at all. This +// fixture is the complement: every canonical-i32 promotion in it comes from the +// loop-induction rule and from nothing else. There is no bitwise mixing, no +// `| 0`, no `>>> 0`, and no array indexing anywhere, so if +// `collect_loop_bounded_i32_locals` returns the empty set this file's +// canonical-i32 count is zero and the census goes red. +// +// The two locals it must NOT promote are here on purpose: an unadmitted +// counter and an unbounded accumulator keep the fixture from being satisfied by +// any rule that simply says yes to proven-integer locals. +// +// Requirements shared with the other canonical-slot fixtures: plain synchronous +// function bodies (async/generator bodies are context-excluded), and no closure +// capture of the candidate locals. + +const ROUNDS = 4096; + +// PROMOTES. A bare `for` counter with a module-level `const` bound: not +// index-used, and `i++` keeps it out of `strictly_i32_bounded_locals`. +// Interval [0, 4095]. +function countUp(): number { + let last = 0.5; + for (let i = 0; i < ROUNDS; i++) { + last = last + 0.25; + } + return last; +} + +// PROMOTES. A `while` whose guard is a CONJUNCTION and whose step is a +// `LocalSet` Add rather than `++` — the 15_mandelbrot `iter` shape. +// Interval [0, 100]. +function iterate(seed: number): number { + let iter = 0; + let x = seed; + while (x < 1000.0 && iter < 100) { + x = x * 1.5; + iter = iter + 1; + } + return iter; +} + +// DOES NOT PROMOTE. `i <= 2147483647` lets the counter reach 2147483648, one +// past INT32_MAX. Node prints 2147483648 here; an i32 slot would print +// -2147483648. `break` keeps the fixture fast without weakening the proof +// obligation, which is a property of the loop text, not of the trip count. +function overshoot(): number { + let i = 2147483640; + for (; i <= 2147483647; i++) { + if (i > 2147483642) { + break; + } + } + return i; +} + +// DOES NOT PROMOTE. A bare accumulator: `sum` has no guard bounding it, and +// 13_factorial's version of this really does reach 4.995e10. +function accumulate(): number { + let sum = 0; + for (let i = 0; i < ROUNDS; i++) { + sum = sum + 1000000; + } + return sum; +} + +console.log( + "loopBounded:" + + countUp() + + ":" + + iterate(1.0) + + ":" + + overshoot() + + ":" + + accumulate(), +); diff --git a/changelog.d/7122-canonical-i32-loop-induction.md b/changelog.d/7122-canonical-i32-loop-induction.md new file mode 100644 index 0000000000..b8c67447ec --- /dev/null +++ b/changelog.d/7122-canonical-i32-loop-induction.md @@ -0,0 +1,112 @@ +A bare loop counter never took canonical unboxed storage. Not in a function +body, not anywhere: `canonical_safe_local` in `stmt/let_stmt.rs` required the +local to be used as an **array index** or to sit in +`strictly_i32_bounded_locals`, and a counter is neither — `i++` disqualifies a +local from the latter outright (#6072), and nothing about `i` in + +```ts +for (let i = 0; i < 1000000; i++) { sum = sum + 1; } +``` + +involves an array. Add one `a[i]` read and it promoted immediately. The +promotion turned on the presence of an array, not on any property of `i`. + +## The proof that admits it + +`collectors/loop_bounded_i32.rs` proves a **closed interval** the local can +never leave, from the guard that dominates every write to it: + +* one declaration, initialiser an i32-range integer literal `I`; +* every write anywhere in the function is a step (`v++`, `v = v + k`, and the + decrement mirror) with `k` a non-negative integer constant; +* every step sits directly in the body or update of a loop whose condition has + a top-level `&&`-spine conjunct `v < B` / `v <= B` / `v > B` / `v >= B`, `B` an + i32-range constant — a literal, a `const` local, or a module-level `const` + from `compile_time_constants`; +* no intervening loop and no intervening closure between the step and that + guard, so each step site runs at most once per iteration; +* the step direction agrees with the guard. + +With `S` the sum of the steps at that level, an increment counter is confined to +`[I, B - 1 + S]` (`[I, B + S]` for `<=`), a decrement counter to the mirror, and +the local is admitted only when **both endpoints fit i32**. + +This is a range argument, not a compatibility bound. The existing +`integer_locals ∩ index_used_locals` term is sound only because the pre-phase +shadow model already read the i32 slot for that exact set (the range-soundness +audit in `expr/slot_rep.rs` says so); this one adds no overflow surface, because +there is no reachable state in which the value leaves i32. The same argument is +already trusted one layer down — `stmt/loops.rs` allocates a *parallel* i32 +shadow for a constant-bounded counter on exactly this reasoning. What is new is +lifting it to a Let-site fact, so the counter's i32 slot becomes its **only** +storage instead of a shadow kept in sync with a boxed double. + +Consumed only by the canonical-i32 gate, never by the parallel-shadow +`needs_i32_slot` gate, so `PERRY_CANONICAL_I32_LOCALS=0` still reproduces the +pre-phase model bit-for-bit — the containment `int_valued_ta_locals` already +uses. No new env knob. + +## The half that stays denied, and why + +A bare **accumulator** is not admitted and must not be. +`benchmarks/suite/13_factorial.ts` — one of the three workloads #7110 names — +computes `sum = sum + (i % 1000)` over 1e8 iterations. That reaches +**49,950,000,000**, twenty-three times `INT32_MAX`. Node prints it exactly; an +i32 slot would print a wrapped negative. "Every write is `sum = sum + `" +is not an i32 proof, and a rule that treated it as one would be a silent wrong +answer rather than a missed optimization. Bounding an accumulator needs the +loop's trip count multiplied by a magnitude bound on the step expression — +strictly more analysis, and filed as #7123. + +The `not_index_used_or_bounded` denial reason now says this, so the report +distinguishes "not implemented yet" from "must not be promoted". + +## Evidence + +`--opt-report=json --no-link`, macOS arm64, oracle Node 26.5.1. + +```ts +function run(): number { let sum = 0; for (let i = 0; i < 1000000; i++) { sum = sum + 1; } return sum; } +``` + +| | `i` | `sum` | +|---|---|---| +| before | denied `not_index_used_or_bounded` | denied `not_index_used_or_bounded` | +| after | **selected `I32`** | denied `not_index_used_or_bounded` | + +Emitted IR for that function, before → after: the counter's `alloca double` +becomes `alloca i32`, the condition's `load double` becomes `load i32`, and the +update's `fadd double %r11, 1.0` becomes `add i32 %r12, 1`. Selecting +canonical-i32 *moves the storage*, so unlike `Ptr` there is no slot left +for an unconsumed selection to fall back to: every read and write of the local +is forced through the i32 slot or it does not compile. + +**Census** (`compiler_output_regression.py census`): corpus-wide `canonical-i32` +**13 → 17**. No floor dropped; `fixture_canonical_slots` rises 2 → 3 (its +`u32Mixer` counter now promotes). The new liveness fixture +`fixture_loop_bounded_i32` has no bitwise mixing, no `| 0` and no array +indexing, so its three `canonical-i32` promotions can only come from this rule; +its `LIVENESS_FLOORS` minimum is pinned at 3 in code, where `--update` cannot +reach it. + +**Wider sweep** (201 parsed files: 200 `test_gap_*.ts` + the app-pattern +kernels), canonical-slot verdicts before → after: + +| | before | after | +|---|---|---| +| selected `I32` | 24 | **28** | +| denied `not_index_used_or_bounded` | 77 | **51** | +| denied `module_init_context` | 127 | **145** | +| denied `closure_referenced` / `declared_bigint` | 7 / 5 | 7 / 5 | + +The 26 locals that leave `not_index_used_or_bounded` split 4 promoted / 18 now +blocked *only* by the module-init context gate (#7109) / 4 that were being +reported twice and are now one selection. So the rule proves **22** more locals +than it promotes today; the other 18 land the moment #7109 is fixed. + +**gc-ratchet** (`--repeats 7`, `shared_ci`): OK. The gated retention and +evacuation counters are **bit-identical** between `PERRY_CANONICAL_I32_LOCALS` +on and off — the representation change moves nothing the collector counts. The +ungated `wall_ms` column moves on 7 of 8 probes (+1.2% to +8.2% slower with the +canonical model off), which is what proves the two arms were different binaries +rather than one stale archive measured twice. diff --git a/crates/perry-codegen/src/collectors/hir_facts.rs b/crates/perry-codegen/src/collectors/hir_facts.rs index e001b1f017..7b0f1b8c3d 100644 --- a/crates/perry-codegen/src/collectors/hir_facts.rs +++ b/crates/perry-codegen/src/collectors/hir_facts.rs @@ -47,6 +47,14 @@ pub(crate) struct RepresentationFacts { /// strictly-i32-bounded — the box `slot.ts` mix shape (`let l = P[0]` from /// an Int32Array PARAM, bitwise-only updates and observations). pub int_valued_ta_locals: HashSet, + /// Locals proven to stay inside i32 range by the monotone loop-induction + /// argument (#7110): single literal initialiser, every write a step whose + /// direction agrees with a constant-bounded guard on the immediately + /// enclosing loop, both interval endpoints inside i32. Like + /// `int_valued_ta_locals` this is a canonical-storage-only admission term + /// — it never widens the parallel-shadow `needs_i32_slot` gate. See + /// `collectors/loop_bounded_i32.rs`. + pub loop_bounded_i32_locals: HashSet, } #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -155,6 +163,10 @@ impl TypeFacts { &self.representation.int_valued_ta_locals } + pub(crate) fn loop_bounded_i32_locals(&self) -> &HashSet { + &self.representation.loop_bounded_i32_locals + } + pub(crate) fn not_bigint_locals(&self) -> &HashSet { &self.representation.not_bigint_locals } @@ -414,6 +426,14 @@ pub(crate) fn collect_type_facts( } } let unsigned_i32_locals = super::i32_locals::collect_unsigned_i32_locals(stmts); + // #7110: the monotone loop-induction i32 range proof. Skipped entirely when + // canonical selection is off, so the `PERRY_CANONICAL_I32_LOCALS=0` + // bisection arm reproduces the pre-phase model with no analysis run at all. + let loop_bounded_i32_locals = if crate::expr::canonical_i32_locals_enabled() { + super::loop_bounded_i32::collect_loop_bounded_i32_locals(stmts, compile_time_constants) + } else { + HashSet::new() + }; let not_bigint_locals = super::not_bigint_locals::collect_not_bigint_locals(stmts, params, binding_types); let (array_facts, effect_facts, materialization_hazards) = @@ -504,6 +524,7 @@ pub(crate) fn collect_type_facts( unsigned_i32_locals, not_bigint_locals, int_valued_ta_locals, + loop_bounded_i32_locals, }, arrays: array_facts, effect: effect_facts, diff --git a/crates/perry-codegen/src/collectors/loop_bounded_i32.rs b/crates/perry-codegen/src/collectors/loop_bounded_i32.rs new file mode 100644 index 0000000000..d3afed3b83 --- /dev/null +++ b/crates/perry-codegen/src/collectors/loop_bounded_i32.rs @@ -0,0 +1,873 @@ +//! Repsel Phase 1 widening (#7110): the **monotone loop-induction** i32 range +//! proof. +//! +//! ## The hole this fills +//! +//! `stmt/let_stmt.rs`'s canonical-i32 gate admits a proven-integer local only +//! when it is *index-used*, *strictly-i32-bounded*, `>>> 0`-written, or an +//! int-typed-array accumulator. A loop counter satisfies none of those: +//! +//! ```text +//! for (let i = 0; i < 1000000; i++) { sum = sum + 1; } +//! ``` +//! +//! `i` is not index-used (nothing is indexed), and it is not +//! `strictly_i32_bounded` because `i++` unconditionally disqualifies a local +//! there (#6072 — `x++` is `x = x + 1` with full f64 semantics, so an +//! *unbounded* `++` really can leave i32 range). Add one `a[i]` read and `i` +//! promotes; the promotion turned on the presence of an array, not on any +//! property of `i`. +//! +//! ## The proof +//! +//! For a local `v` this analysis proves a **closed interval** that `v` can +//! never leave, from the loop guard that dominates every write to it: +//! +//! 1. `v` has exactly one declaration, whose initialiser is an integer literal +//! `I` inside i32 range. +//! 2. Every write to `v` anywhere in the function is a **step** — `v++`, +//! `v += k`, `v = v + k` (or the `--`/`-=`/`v = v - k` mirror) with `k` a +//! non-negative integer constant — and every such step sits **directly in +//! the body or update of a loop whose condition guards `v`**, with no +//! intervening loop and no intervening closure. +//! 3. That loop's condition has a top-level `&&`-spine conjunct `v < B`, +//! `v <= B`, `v > B` or `v >= B` (either operand order) with `B` an +//! integer constant in i32 range. +//! 4. The step direction agrees with the guard: `<`/`<=` admits only +//! increments, `>`/`>=` only decrements. (`for (let i = 0; i < 10; i--)` +//! runs away downwards and must not be admitted.) +//! +//! Then, writing `S` for the sum of the `k`s of all step sites at that loop +//! level (each executes at most once per iteration — that is what "no +//! intervening loop" buys): +//! +//! * increments: every step is reached only after the guard `v < B` was +//! observed true this iteration, so `v <= B - 1` before it and +//! `v <= B - 1 + S` after; `v` never decreases, so `v >= I`. The interval is +//! `[I, B - 1 + S]` (`[I, B + S]` for `<=`). +//! * decrements: the mirror, `[B + 1 - S, I]` (`[B - S, I]` for `>=`). +//! +//! Both endpoints are compile-time integers; the local is admitted only when +//! **both fit i32**. That is a genuine range argument, not the compatibility +//! bound that `integer_locals ∩ index_used_locals` rests on (see the range +//! soundness audit in `expr/slot_rep.rs`): it introduces no new overflow +//! surface, because there is no reachable state in which the value leaves i32. +//! +//! The same argument is already trusted elsewhere in codegen — `stmt/loops.rs` +//! allocates a *parallel* i32 shadow for a constant-bounded counter on exactly +//! this reasoning ("with a CONSTANT bound the counter provably stays in i32 +//! range"). This module lifts it to a Let-site fact so the counter can take +//! canonical storage (i32 slot only, no double slot, no dual writes) instead of +//! a shadow that has to be kept in sync with a boxed double. +//! +//! ## What it deliberately does NOT prove +//! +//! A bare **accumulator** — `let sum = 0; for (…) sum = sum + x;` — is not +//! admitted, and must not be. `benchmarks/suite/13_factorial.ts` is the live +//! counterexample: `sum = sum + (i % 1000)` over 1e8 iterations reaches +//! 49,950,000,000, twenty-three times `INT32_MAX`. Node prints it exactly; an +//! i32 slot would print a wrapped negative. Admitting "every write is +//! `sum = sum + `" as an i32 proof is a silent wrong answer, not a +//! missed optimization. Bounding an accumulator needs the loop's *trip count* +//! multiplied by a magnitude bound on the step expression — strictly more +//! analysis than this module does; #7123 specifies it. +//! +//! Consumed only by the canonical-i32 gate (`canonical_safe_local` in +//! `stmt/let_stmt.rs`), never by the parallel-shadow `needs_i32_slot` gate, so +//! `PERRY_CANONICAL_I32_LOCALS=0` still reproduces the pre-phase model +//! bit-for-bit — the same containment `int_valued_ta_locals` uses. + +use std::collections::{HashMap, HashSet}; + +use perry_hir::{BinaryOp, CompareOp, Expr, LogicalOp, Stmt, UpdateOp}; + +/// Direction a local's induction moves in. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +enum Dir { + Inc, + Dec, +} + +/// The bound a single guarded loop level derives for one local. +#[derive(Clone, Copy, Debug)] +struct GuardedLevel { + dir: Dir, + /// The extreme the local can reach at this level: an upper bound for + /// [`Dir::Inc`], a lower bound for [`Dir::Dec`]. Always inside i32. + extreme: i64, +} + +/// Analysis state, accumulated over one whole function body. +#[derive(Default)] +struct State { + /// `id → I`, the single literal initialiser. Absent when the local has no + /// declaration with an i32-range integer literal init. + declared_init: HashMap, + /// Locals declared more than once, or whose declaration carries a + /// non-literal / out-of-range init. Never admissible. + bad_decl: HashSet, + /// `id → value` for immutable integer-literal bindings never written + /// anywhere. Used to resolve a symbolic loop bound (`i < LIMIT`). + const_ints: HashMap, + /// Module-level `const NAME = ` bindings + /// (`codegen/mod.rs`'s `compile_time_constants`). A `const` reassignment + /// is a parse-time error in ECMAScript, so these are constants by the + /// language rather than by analysis — the same map the Phase 2 in-bounds + /// proof already trusts. Carries the `for (let i = 0; i < ITERATIONS; i++)` + /// shape where `ITERATIONS` is declared at module scope. + module_consts: HashMap, + /// A write that was not a guarded step. Never admissible. + disqualified: HashSet, + /// Merged bound across every guarded loop level that stepped this local. + bounds: HashMap, +} + +/// Locals proven to stay inside i32 range by the monotone loop-induction +/// argument documented at the top of this module. +pub fn collect_loop_bounded_i32_locals( + stmts: &[Stmt], + compile_time_constants: &HashMap, +) -> HashSet { + let mut st = State::default(); + st.module_consts = compile_time_constants + .iter() + .filter_map(|(&id, &v)| { + (v.is_finite() && v.fract() == 0.0 && v.abs() <= i32::MAX as f64) + .then_some((id, v as i64)) + }) + .collect(); + collect_declarations(stmts, &mut st); + collect_const_ints(stmts, &mut st); + + let empty: HashMap = HashMap::new(); + walk_stmts(stmts, &empty, &mut st); + + let mut out = HashSet::new(); + for (&id, bound) in &st.bounds { + if st.disqualified.contains(&id) || st.bad_decl.contains(&id) { + continue; + } + let Some(&init) = st.declared_init.get(&id) else { + continue; + }; + // The interval is [min(init, extreme), max(init, extreme)] — for `Inc` + // the local never goes below `init` and never above `extreme`; for + // `Dec` the mirror. Both endpoints must fit i32; `extreme` already + // does by construction, and `init` was range-checked at declaration, + // but assert it here so the admission rule reads as the interval it is. + let (lo, hi) = match bound.dir { + Dir::Inc => (init, bound.extreme), + Dir::Dec => (bound.extreme, init), + }; + if fits_i32(lo) && fits_i32(hi) { + out.insert(id); + } + } + out +} + +fn fits_i32(n: i64) -> bool { + i32::try_from(n).is_ok() +} + +/// An integer-literal expression, if `e` is one (`Expr::Number` included so a +/// bound written `1e6` is not silently a different rule from `1000000`). +fn integer_literal(e: &Expr) -> Option { + match e { + Expr::Integer(n) => Some(*n), + Expr::Number(f) + if f.is_finite() && f.fract() == 0.0 && f.abs() <= 9.007_199_254_740_992e15 => + { + Some(*f as i64) + } + _ => None, + } +} + +/// An i32-range integer constant: a literal, or a `const` local bound to one. +fn const_i32_value(e: &Expr, st: &State) -> Option { + let v = match e { + Expr::LocalGet(id) => *st.const_ints.get(id).or_else(|| st.module_consts.get(id))?, + _ => integer_literal(e)?, + }; + fits_i32(v).then_some(v) +} + +// --------------------------------------------------------------------------- +// Pass 1: declarations and constants +// --------------------------------------------------------------------------- + +/// Record each local's single literal initialiser. A local declared twice (a +/// hoisted `var`, a `let` in two switch arms sharing an id) loses the +/// single-entry-value premise the interval rests on, so it is rejected +/// outright. +fn collect_declarations(stmts: &[Stmt], st: &mut State) { + for_each_let(stmts, &mut |id, init, _mutable| { + if st.declared_init.contains_key(&id) { + st.bad_decl.insert(id); + return; + } + match init.and_then(integer_literal) { + Some(v) if fits_i32(v) => { + st.declared_init.insert(id, v); + } + _ => { + st.bad_decl.insert(id); + } + } + }); +} + +/// Immutable integer-literal bindings that are never written. These are the +/// only symbolic loop bounds this analysis will resolve (`const LIMIT = 1000`). +fn collect_const_ints(stmts: &[Stmt], st: &mut State) { + let mut candidates: HashMap = HashMap::new(); + for_each_let(stmts, &mut |id, init, mutable| { + if mutable { + return; + } + if let Some(v) = init.and_then(integer_literal) { + if fits_i32(v) { + candidates.insert(id, v); + } + } + }); + if candidates.is_empty() { + return; + } + let mut written: HashSet = HashSet::new(); + collect_written_locals(stmts, &mut written); + candidates.retain(|id, _| !written.contains(id)); + st.const_ints = candidates; +} + +/// Every local that is assigned anywhere in the body — `LocalSet` *and* +/// `Update`. `collect_localset_ids_in_stmts` deliberately skips `Update` +/// (it preserves integer-ness, which is what that collector asks about); +/// here a `++` is exactly what must disqualify a "constant" bound. +fn collect_written_locals(stmts: &[Stmt], out: &mut HashSet) { + fn in_expr(e: &Expr, out: &mut HashSet) { + match e { + Expr::LocalSet(id, _) | Expr::Update { id, .. } => { + out.insert(*id); + } + Expr::Closure { body, .. } => walk(body, out), + _ => { + if let Some(id) = with_set_fallback_local(e) { + out.insert(id); + } + } + } + perry_hir::walker::walk_expr_children(e, &mut |c| in_expr(c, out)); + } + fn walk(stmts: &[Stmt], out: &mut HashSet) { + for s in stmts { + match s { + Stmt::Let { init, .. } => { + if let Some(e) = init { + in_expr(e, out); + } + } + Stmt::Expr(e) | Stmt::Throw(e) => in_expr(e, out), + Stmt::Return(opt) => { + if let Some(e) = opt { + in_expr(e, out); + } + } + Stmt::If { + condition, + then_branch, + else_branch, + } => { + in_expr(condition, out); + walk(then_branch, out); + if let Some(eb) = else_branch { + walk(eb, out); + } + } + Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => { + in_expr(condition, out); + walk(body, out); + } + Stmt::For { + init, + condition, + update, + body, + } => { + if let Some(i) = init { + walk(std::slice::from_ref(i.as_ref()), out); + } + if let Some(c) = condition { + in_expr(c, out); + } + if let Some(u) = update { + in_expr(u, out); + } + walk(body, out); + } + Stmt::Try { + body, + catch, + finally, + } => { + walk(body, out); + if let Some(c) = catch { + walk(&c.body, out); + } + if let Some(f) = finally { + walk(f, out); + } + } + Stmt::Switch { + discriminant, + cases, + } => { + in_expr(discriminant, out); + for c in cases { + if let Some(t) = &c.test { + in_expr(t, out); + } + walk(&c.body, out); + } + } + Stmt::Labeled { body, .. } => walk(std::slice::from_ref(body.as_ref()), out), + _ => {} + } + } + } + walk(stmts, out); +} + +/// Visit every `Stmt::Let` in the body, including inside closures — a closure's +/// own `let` shares the id space, and missing it would let a second +/// declaration go unnoticed. +fn for_each_let(stmts: &[Stmt], f: &mut dyn FnMut(u32, Option<&Expr>, bool)) { + for s in stmts { + match s { + Stmt::Let { + id, init, mutable, .. + } => { + f(*id, init.as_ref(), *mutable); + if let Some(init) = init { + for_each_let_in_expr(init, f); + } + } + Stmt::Expr(e) | Stmt::Throw(e) => for_each_let_in_expr(e, f), + Stmt::Return(opt) => { + if let Some(e) = opt { + for_each_let_in_expr(e, f); + } + } + Stmt::If { + condition, + then_branch, + else_branch, + } => { + for_each_let_in_expr(condition, f); + for_each_let(then_branch, f); + if let Some(eb) = else_branch { + for_each_let(eb, f); + } + } + Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => { + for_each_let_in_expr(condition, f); + for_each_let(body, f); + } + Stmt::For { + init, + condition, + update, + body, + } => { + if let Some(init) = init { + for_each_let(std::slice::from_ref(init.as_ref()), f); + } + if let Some(c) = condition { + for_each_let_in_expr(c, f); + } + if let Some(u) = update { + for_each_let_in_expr(u, f); + } + for_each_let(body, f); + } + Stmt::Try { + body, + catch, + finally, + } => { + for_each_let(body, f); + if let Some(c) = catch { + for_each_let(&c.body, f); + } + if let Some(fin) = finally { + for_each_let(fin, f); + } + } + Stmt::Switch { + discriminant, + cases, + } => { + for_each_let_in_expr(discriminant, f); + for c in cases { + if let Some(t) = &c.test { + for_each_let_in_expr(t, f); + } + for_each_let(&c.body, f); + } + } + Stmt::Labeled { body, .. } => { + for_each_let(std::slice::from_ref(body.as_ref()), f); + } + _ => {} + } + } +} + +fn for_each_let_in_expr(e: &Expr, f: &mut dyn FnMut(u32, Option<&Expr>, bool)) { + if let Expr::Closure { body, .. } = e { + for_each_let(body, f); + } + perry_hir::walker::walk_expr_children(e, &mut |child| for_each_let_in_expr(child, f)); +} + +// --------------------------------------------------------------------------- +// Pass 2: judge every write against the guard of its immediately-enclosing loop +// --------------------------------------------------------------------------- + +/// A step write: `(direction, magnitude)`. +fn classify_step(id: u32, value: &Expr, st: &State) -> Option<(Dir, i64)> { + let Expr::Binary { op, left, right } = value else { + return None; + }; + let dir = match op { + BinaryOp::Add => Dir::Inc, + BinaryOp::Sub => Dir::Dec, + _ => return None, + }; + // `v = v + k` (and, for Add only, the commuted `v = k + v`). `v = k - v` + // is NOT a step: it flips sign every iteration and is not monotone. + let is_self = |e: &Expr| matches!(e, Expr::LocalGet(other) if *other == id); + let k = if is_self(left) { + const_i32_value(right, st)? + } else if matches!(dir, Dir::Inc) && is_self(right) { + const_i32_value(left, st)? + } else { + return None; + }; + // A negative magnitude reverses the direction and would break monotonicity + // against the guard; reject rather than normalise, so the rule stays the + // one the module doc states. + (k >= 0).then_some((dir, k)) +} + +/// Every step site for `id` at ONE loop level: the loop's `update` plus its +/// body, descending through `if`/`switch`/`try`/labels but never into a nested +/// loop or a closure. Returns `None` when any write at this level is not a +/// step, when the directions disagree, or when there is no step at all. +fn scan_level_steps( + update: Option<&Expr>, + body: &[Stmt], + id: u32, + st: &State, +) -> Option<(Dir, i64)> { + let mut acc: Option<(Dir, i64)> = None; + let mut ok = true; + let mut fold = |step: Option<(Dir, i64)>| match (step, acc) { + (None, _) => ok = false, + (Some((d, k)), None) => acc = Some((d, k)), + (Some((d, k)), Some((d0, total))) => { + if d == d0 { + acc = Some((d0, total.saturating_add(k))); + } else { + ok = false; + } + } + }; + if let Some(u) = update { + scan_level_writes_in_expr(u, id, st, &mut fold); + } + scan_level_writes(body, id, st, &mut fold); + if !ok { + return None; + } + acc +} + +fn scan_level_writes(stmts: &[Stmt], id: u32, st: &State, f: &mut dyn FnMut(Option<(Dir, i64)>)) { + for s in stmts { + match s { + Stmt::Let { init, .. } => { + if let Some(init) = init { + scan_level_writes_in_expr(init, id, st, f); + } + } + Stmt::Expr(e) | Stmt::Throw(e) => scan_level_writes_in_expr(e, id, st, f), + Stmt::Return(opt) => { + if let Some(e) = opt { + scan_level_writes_in_expr(e, id, st, f); + } + } + Stmt::If { + condition, + then_branch, + else_branch, + } => { + scan_level_writes_in_expr(condition, id, st, f); + scan_level_writes(then_branch, id, st, f); + if let Some(eb) = else_branch { + scan_level_writes(eb, id, st, f); + } + } + Stmt::Try { + body, + catch, + finally, + } => { + scan_level_writes(body, id, st, f); + if let Some(c) = catch { + scan_level_writes(&c.body, id, st, f); + } + if let Some(fin) = finally { + scan_level_writes(fin, id, st, f); + } + } + Stmt::Switch { + discriminant, + cases, + } => { + scan_level_writes_in_expr(discriminant, id, st, f); + for c in cases { + if let Some(t) = &c.test { + scan_level_writes_in_expr(t, id, st, f); + } + scan_level_writes(&c.body, id, st, f); + } + } + Stmt::Labeled { body, .. } => { + scan_level_writes(std::slice::from_ref(body.as_ref()), id, st, f); + } + // A nested loop is a different level: its writes are judged against + // its OWN guard by `walk_stmts`, and must not be folded into this + // level's per-iteration total (they can execute many times per + // outer iteration). + Stmt::While { .. } | Stmt::DoWhile { .. } | Stmt::For { .. } => {} + _ => {} + } + } +} + +fn scan_level_writes_in_expr(e: &Expr, id: u32, st: &State, f: &mut dyn FnMut(Option<(Dir, i64)>)) { + match e { + Expr::LocalSet(target, value) => { + if *target == id { + f(classify_step(id, value, st)); + } + scan_level_writes_in_expr(value, id, st, f); + } + Expr::Update { id: target, op, .. } => { + if *target == id { + f(Some((update_dir(*op), 1))); + } + } + // A closure body is not part of this level (and any write it makes is + // disqualifying — `walk_stmts` judges it against an empty guard). + Expr::Closure { .. } => {} + _ => { + if with_set_fallback_local(e) == Some(id) { + f(None); + } + perry_hir::walker::walk_expr_children(e, &mut |child| { + scan_level_writes_in_expr(child, id, st, f) + }); + } + } +} + +/// The local a `with (obj) { name = v }` write falls back to when the object +/// does not bind `name`. That write never appears as a `LocalSet`, so without +/// this arm a `with` block could assign a counter behind the analysis's back. +fn with_set_fallback_local(e: &Expr) -> Option { + let Expr::WithSet { fallback, .. } = e else { + return None; + }; + match fallback { + perry_hir::WithSetFallback::Local(id) | perry_hir::WithSetFallback::SloppyImplicit(id) => { + Some(*id) + } + _ => None, + } +} + +fn update_dir(op: UpdateOp) -> Dir { + match op { + UpdateOp::Increment => Dir::Inc, + UpdateOp::Decrement => Dir::Dec, + } +} + +/// The guards a loop's condition establishes for the locals it steps. +fn derive_guards( + condition: Option<&Expr>, + update: Option<&Expr>, + body: &[Stmt], + st: &State, +) -> HashMap { + let mut out = HashMap::new(); + let Some(condition) = condition else { + return out; + }; + for (id, op, bound) in conjunct_guards(condition, st) { + let Some((dir, total)) = scan_level_steps(update, body, id, st) else { + continue; + }; + let guard_dir = match op { + CompareOp::Lt | CompareOp::Le => Dir::Inc, + CompareOp::Gt | CompareOp::Ge => Dir::Dec, + _ => continue, + }; + if dir != guard_dir { + continue; + } + // The guard is observed true immediately before the iteration that + // contains the steps, so the value entering them is at most `bound - 1` + // (`bound` for the inclusive forms) and the steps add at most `total`. + let extreme = match op { + CompareOp::Lt => bound - 1 + total, + CompareOp::Le => bound + total, + CompareOp::Gt => bound + 1 - total, + CompareOp::Ge => bound - total, + _ => continue, + }; + if !fits_i32(extreme) { + continue; + } + // Two conjuncts can name the same local (`i < A && i < B`); either is a + // valid bound, so keep the tighter one. + match out.entry(id) { + std::collections::hash_map::Entry::Vacant(v) => { + v.insert(GuardedLevel { dir, extreme }); + } + std::collections::hash_map::Entry::Occupied(mut o) => { + let cur: &mut GuardedLevel = o.get_mut(); + if cur.dir == dir { + cur.extreme = match dir { + Dir::Inc => cur.extreme.min(extreme), + Dir::Dec => cur.extreme.max(extreme), + }; + } + } + } + } + out +} + +/// Every `local OP const` comparison on the condition's top-level `&&` spine. +/// A conjunct is guaranteed true whenever the body runs; `||` and `!` give no +/// such guarantee and are not descended into. +fn conjunct_guards(e: &Expr, st: &State) -> Vec<(u32, CompareOp, i64)> { + let mut out = Vec::new(); + collect_conjunct_guards(e, st, &mut out); + out +} + +fn collect_conjunct_guards(e: &Expr, st: &State, out: &mut Vec<(u32, CompareOp, i64)>) { + match e { + Expr::Logical { + op: LogicalOp::And, + left, + right, + } => { + collect_conjunct_guards(left, st, out); + collect_conjunct_guards(right, st, out); + } + Expr::Compare { op, left, right } => { + if let (Expr::LocalGet(id), Some(bound)) = (left.as_ref(), const_i32_value(right, st)) { + out.push((*id, *op, bound)); + } else if let (Some(bound), Expr::LocalGet(id)) = + (const_i32_value(left, st), right.as_ref()) + { + // `B > i` is `i < B`, etc. + if let Some(flipped) = flip_compare(*op) { + out.push((*id, flipped, bound)); + } + } + } + _ => {} + } +} + +fn flip_compare(op: CompareOp) -> Option { + match op { + CompareOp::Lt => Some(CompareOp::Gt), + CompareOp::Le => Some(CompareOp::Ge), + CompareOp::Gt => Some(CompareOp::Lt), + CompareOp::Ge => Some(CompareOp::Le), + _ => None, + } +} + +fn walk_stmts(stmts: &[Stmt], guard: &HashMap, st: &mut State) { + for s in stmts { + match s { + Stmt::Let { init, .. } => { + if let Some(init) = init { + walk_expr(init, guard, st); + } + } + Stmt::Expr(e) | Stmt::Throw(e) => walk_expr(e, guard, st), + Stmt::Return(opt) => { + if let Some(e) = opt { + walk_expr(e, guard, st); + } + } + Stmt::If { + condition, + then_branch, + else_branch, + } => { + walk_expr(condition, guard, st); + walk_stmts(then_branch, guard, st); + if let Some(eb) = else_branch { + walk_stmts(eb, guard, st); + } + } + Stmt::While { condition, body } => { + // The condition is evaluated before each iteration, so a write + // INSIDE it is not covered by the guard it is establishing. + walk_expr(condition, guard, st); + let level = derive_guards(Some(condition), None, body, st); + walk_stmts(body, &level, st); + } + // `do { … } while (c)` runs its body once BEFORE `c` is ever + // evaluated, so no guard dominates the first pass. Judged at the + // enclosing level, which disqualifies any step it contains. + Stmt::DoWhile { body, condition } => { + walk_stmts(body, &HashMap::new(), st); + walk_expr(condition, guard, st); + } + Stmt::For { + init, + condition, + update, + body, + } => { + if let Some(init) = init { + walk_stmts(std::slice::from_ref(init.as_ref()), guard, st); + } + if let Some(c) = condition { + walk_expr(c, guard, st); + } + let level = derive_guards(condition.as_ref(), update.as_ref(), body, st); + if let Some(u) = update { + walk_expr(u, &level, st); + } + walk_stmts(body, &level, st); + } + Stmt::Try { + body, + catch, + finally, + } => { + walk_stmts(body, guard, st); + if let Some(c) = catch { + walk_stmts(&c.body, guard, st); + } + if let Some(fin) = finally { + walk_stmts(fin, guard, st); + } + } + Stmt::Switch { + discriminant, + cases, + } => { + walk_expr(discriminant, guard, st); + for c in cases { + if let Some(t) = &c.test { + walk_expr(t, guard, st); + } + walk_stmts(&c.body, guard, st); + } + } + Stmt::Labeled { body, .. } => { + walk_stmts(std::slice::from_ref(body.as_ref()), guard, st); + } + _ => {} + } + } +} + +fn walk_expr(e: &Expr, guard: &HashMap, st: &mut State) { + match e { + Expr::LocalSet(id, value) => { + let step = classify_step(*id, value, st); + record_write(*id, step, guard, st); + walk_expr(value, guard, st); + } + Expr::Update { id, op, .. } => { + record_write(*id, Some((update_dir(*op), 1)), guard, st); + } + Expr::Closure { body, .. } => { + // No loop guard reaches into a closure body: it can be called any + // number of times, from anywhere. Any write it makes disqualifies. + let empty = HashMap::new(); + walk_stmts(body, &empty, st); + // Param defaults are ordinary expressions evaluated per call. + perry_hir::walker::walk_expr_children(e, &mut |child| walk_expr(child, &empty, st)); + } + _ => { + // A `with (obj) { i = v }` write is not a `LocalSet`; its target + // lives in the `WithSet` fallback and is unconditionally + // disqualifying (the object probe decides at runtime whether the + // local is written at all). + if let Some(id) = with_set_fallback_local(e) { + st.disqualified.insert(id); + } + // `walk_expr_children` is the crate's single source of truth for + // sub-expression descent, so a future variant carrying a + // `LocalSet`/`Update` is judged rather than silently skipped. + perry_hir::walker::walk_expr_children(e, &mut |child| walk_expr(child, guard, st)); + } + } +} + +fn record_write( + id: u32, + step: Option<(Dir, i64)>, + guard: &HashMap, + st: &mut State, +) { + let Some((dir, _)) = step else { + st.disqualified.insert(id); + return; + }; + let Some(level) = guard.get(&id).copied() else { + st.disqualified.insert(id); + return; + }; + if level.dir != dir { + st.disqualified.insert(id); + return; + } + match st.bounds.entry(id) { + std::collections::hash_map::Entry::Vacant(v) => { + v.insert(level); + } + std::collections::hash_map::Entry::Occupied(mut o) => { + let cur: &mut GuardedLevel = o.get_mut(); + if cur.dir != level.dir { + st.disqualified.insert(id); + return; + } + // Widen to the union of every guarded level that steps this local. + cur.extreme = match level.dir { + Dir::Inc => cur.extreme.max(level.extreme), + Dir::Dec => cur.extreme.min(level.extreme), + }; + } + } +} + +#[cfg(test)] +#[path = "loop_bounded_i32/tests.rs"] +mod tests; diff --git a/crates/perry-codegen/src/collectors/loop_bounded_i32/tests.rs b/crates/perry-codegen/src/collectors/loop_bounded_i32/tests.rs new file mode 100644 index 0000000000..63297d4b84 --- /dev/null +++ b/crates/perry-codegen/src/collectors/loop_bounded_i32/tests.rs @@ -0,0 +1,768 @@ +//! Unit tests for the monotone loop-induction i32 range proof (#7110). +//! +//! The interesting assertions are the REJECTIONS. Admitting a value that can +//! leave i32 range is a silent wrong answer (a wrapped negative printed where +//! Node prints the true integer), so every arm of the proof gets a test that +//! removing it would turn green. + +use super::*; +use perry_hir::types::Type as HirType; +use perry_hir::{CatchClause, Param, SwitchCase}; + +fn let_mut(id: u32, init: Option) -> Stmt { + Stmt::Let { + id, + name: format!("v{id}"), + ty: HirType::Number, + mutable: true, + init, + } +} + +fn let_const(id: u32, value: i64) -> Stmt { + Stmt::Let { + id, + name: format!("c{id}"), + ty: HirType::Number, + mutable: false, + init: Some(Expr::Integer(value)), + } +} + +fn inc(id: u32) -> Expr { + Expr::Update { + id, + op: UpdateOp::Increment, + prefix: false, + } +} + +fn dec(id: u32) -> Expr { + Expr::Update { + id, + op: UpdateOp::Decrement, + prefix: false, + } +} + +fn bin(op: BinaryOp, l: Expr, r: Expr) -> Expr { + Expr::Binary { + op, + left: Box::new(l), + right: Box::new(r), + } +} + +fn cmp(op: CompareOp, l: Expr, r: Expr) -> Expr { + Expr::Compare { + op, + left: Box::new(l), + right: Box::new(r), + } +} + +fn and(l: Expr, r: Expr) -> Expr { + Expr::Logical { + op: LogicalOp::And, + left: Box::new(l), + right: Box::new(r), + } +} + +fn or(l: Expr, r: Expr) -> Expr { + Expr::Logical { + op: LogicalOp::Or, + left: Box::new(l), + right: Box::new(r), + } +} + +fn set(id: u32, rhs: Expr) -> Stmt { + Stmt::Expr(Expr::LocalSet(id, Box::new(rhs))) +} + +/// `for (let = ; < ; ++) ` +fn counting_for(id: u32, init: i64, bound: Expr, body: Vec) -> Stmt { + Stmt::For { + init: Some(Box::new(let_mut(id, Some(Expr::Integer(init))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(id), bound)), + update: Some(inc(id)), + body, + } +} + +fn run(stmts: &[Stmt]) -> HashSet { + collect_loop_bounded_i32_locals(stmts, &HashMap::new()) +} + +/// Same, with a module-level `const` map (`compile_time_constants`). +fn run_with_module_consts(stmts: &[Stmt], consts: &[(u32, f64)]) -> HashSet { + let map: HashMap = consts.iter().copied().collect(); + collect_loop_bounded_i32_locals(stmts, &map) +} + +// --------------------------------------------------------------------------- +// The shape the issue is about +// --------------------------------------------------------------------------- + +#[test] +fn bare_loop_counter_with_literal_bound_is_admitted() { + // for (let i = 0; i < 1000000; i++) { sum = sum + 1; } + // + // `i` is not index-used (nothing is indexed) and `i++` keeps it out of + // `strictly_i32_bounded_locals`. This fact is the ONLY thing that can + // admit it. Interval: [0, 999999]. + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(1_000_000), + vec![set( + 1, + bin(BinaryOp::Add, Expr::LocalGet(1), Expr::Integer(1)), + )], + ), + ]; + let got = run(&stmts); + assert!(got.contains(&2), "loop counter must be admitted: {got:?}"); +} + +#[test] +fn bare_accumulator_is_not_admitted() { + // The other half of #7110, and the half that must STAY denied: + // `sum = sum + 1` is a step, but no loop guard constrains `sum`, so + // nothing bounds it. 13_factorial's `sum` really does reach 4.995e10. + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(1_000_000), + vec![set( + 1, + bin(BinaryOp::Add, Expr::LocalGet(1), Expr::Integer(1)), + )], + ), + ]; + let got = run(&stmts); + assert!( + !got.contains(&1), + "bare accumulator must stay denied: {got:?}" + ); +} + +#[test] +fn const_local_bound_resolves() { + // const LIMIT = 100; for (let i = 0; i < LIMIT; i++) {} + let stmts = vec![ + let_const(1, 100), + counting_for(2, 0, Expr::LocalGet(1), vec![]), + ]; + assert!(run(&stmts).contains(&2)); +} + +#[test] +fn while_loop_guard_conjunct_admits_the_counter() { + // The 15_mandelbrot `iter` shape: a `while` whose guard is a CONJUNCTION, + // one arm of which bounds the counter, and whose step is a `LocalSet` Add + // rather than `++`. + // let iter = 0; + // while (flag && iter < 100) { iter = iter + 1; } + let stmts = vec![ + let_mut(3, Some(Expr::Integer(0))), + Stmt::While { + condition: and( + Expr::Bool(true), + cmp(CompareOp::Lt, Expr::LocalGet(3), Expr::Integer(100)), + ), + body: vec![set( + 3, + bin(BinaryOp::Add, Expr::LocalGet(3), Expr::Integer(1)), + )], + }, + ]; + assert!(run(&stmts).contains(&3)); +} + +#[test] +fn disjunctive_guard_is_not_a_guard() { + // `a || i < 100` does NOT imply `i < 100` when the body runs. + let stmts = vec![ + let_mut(3, Some(Expr::Integer(0))), + Stmt::While { + condition: or( + Expr::Bool(true), + cmp(CompareOp::Lt, Expr::LocalGet(3), Expr::Integer(100)), + ), + body: vec![set( + 3, + bin(BinaryOp::Add, Expr::LocalGet(3), Expr::Integer(1)), + )], + }, + ]; + assert!(!run(&stmts).contains(&3)); +} + +#[test] +fn reversed_operand_order_is_the_same_guard() { + // for (let i = 0; 100 > i; i++) {} + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Gt, Expr::Integer(100), Expr::LocalGet(2))), + update: Some(inc(2)), + body: vec![], + }]; + assert!(run(&stmts).contains(&2)); +} + +#[test] +fn descending_counter_is_admitted() { + // for (let i = 100; i > -5; i--) {} → interval [-4, 100] + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(100))))), + condition: Some(cmp(CompareOp::Gt, Expr::LocalGet(2), Expr::Integer(-5))), + update: Some(dec(2)), + body: vec![], + }]; + assert!(run(&stmts).contains(&2)); +} + +// --------------------------------------------------------------------------- +// Overflow-boundary rejections — each one is a wrong answer if admitted +// --------------------------------------------------------------------------- + +#[test] +fn le_bound_at_int32_max_would_overflow_and_is_rejected() { + // for (let i = 0; i <= 2147483647; i++) — the counter tops out at + // 2147483648, one past INT32_MAX. Must NOT be admitted. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp( + CompareOp::Le, + Expr::LocalGet(2), + Expr::Integer(i32::MAX as i64), + )), + update: Some(inc(2)), + body: vec![], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn lt_bound_at_int32_max_tops_out_exactly_at_int32_max() { + // for (let i = 0; i < 2147483647; i++) — tops out at 2147483647. Admitted; + // this is the boundary the previous test sits one past. + let stmts = vec![counting_for(2, 0, Expr::Integer(i32::MAX as i64), vec![])]; + assert!(run(&stmts).contains(&2)); +} + +#[test] +fn two_steps_per_iteration_are_summed_into_the_bound() { + // for (let i = 0; i < 2147483646; i++) { i = i + 1; } + // The body step AND the update both run, so the counter tops out at + // 2147483645 + 2 = 2147483647. Exactly INT32_MAX — admitted. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp( + CompareOp::Lt, + Expr::LocalGet(2), + Expr::Integer(i32::MAX as i64 - 1), + )), + update: Some(inc(2)), + body: vec![set( + 2, + bin(BinaryOp::Add, Expr::LocalGet(2), Expr::Integer(1)), + )], + }]; + assert!(run(&stmts).contains(&2)); + + // One higher and the same two steps overshoot INT32_MAX. Rejected. If the + // per-iteration total were not summed, this would (wrongly) pass. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp( + CompareOp::Lt, + Expr::LocalGet(2), + Expr::Integer(i32::MAX as i64), + )), + update: Some(inc(2)), + body: vec![set( + 2, + bin(BinaryOp::Add, Expr::LocalGet(2), Expr::Integer(1)), + )], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn out_of_range_literal_bound_is_rejected() { + // for (let i = 0; i < 3000000000; i++) — the bound itself is past i32. + let stmts = vec![counting_for(2, 0, Expr::Integer(3_000_000_000), vec![])]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn out_of_range_initialiser_is_rejected() { + // let i = 3000000000; for (; i > 0; i--) — the ENTRY value is past i32 + // even though the guard bounds the other end. + let stmts = vec![ + let_mut(2, Some(Expr::Integer(3_000_000_000))), + Stmt::For { + init: None, + condition: Some(cmp(CompareOp::Gt, Expr::LocalGet(2), Expr::Integer(0))), + update: Some(dec(2)), + body: vec![], + }, + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn runtime_bound_is_not_a_constant() { + // for (let i = 0; i < n; i++) where `n` is a mutable local: #6072's + // runaway shape (`n = 2147483653` wraps the shadow to INT32_MIN). + let stmts = vec![ + let_mut(1, None), + counting_for(2, 0, Expr::LocalGet(1), vec![]), + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_written_bound_is_not_a_constant() { + // `let LIMIT = 100; LIMIT = 4000000000;` — declared with a literal but + // reassigned, so it cannot serve as a compile-time bound. + let stmts = vec![ + Stmt::Let { + id: 1, + name: "LIMIT".into(), + ty: HirType::Number, + mutable: false, + init: Some(Expr::Integer(100)), + }, + set(1, Expr::Integer(4_000_000_000)), + counting_for(2, 0, Expr::LocalGet(1), vec![]), + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn direction_must_agree_with_the_guard() { + // for (let i = 0; i < 10; i--) never terminates upward-bounded: `i` runs + // to -infinity. The guard says Inc, the step says Dec. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(dec(2)), + body: vec![], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn non_step_write_disqualifies() { + // for (let i = 0; i < 10; i++) { i = someCall(); } + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![set(2, Expr::LocalGet(9))], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn multiplicative_step_is_not_a_step() { + // `i = i * 2` grows geometrically; the guard bounds one iteration's ENTRY + // value but not the product. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(1))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(Expr::LocalSet( + 2, + Box::new(bin(BinaryOp::Mul, Expr::LocalGet(2), Expr::Integer(2))), + )), + body: vec![], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn reverse_subtraction_is_not_a_step() { + // `i = 10 - i` flips sign each iteration; it is not monotone, so the + // "guard dominates the step" argument does not apply. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(Expr::LocalSet( + 2, + Box::new(bin(BinaryOp::Sub, Expr::Integer(10), Expr::LocalGet(2))), + )), + body: vec![], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn step_inside_a_nested_loop_is_not_bounded_by_the_outer_guard() { + // for (let i = 0; i < 10; i++) { for (let j = 0; j < 1000000000; j++) { i = i + 1; } } + // + // `i` advances a BILLION times per outer iteration; the outer guard bounds + // it only at the top of each outer iteration. If the "no intervening loop" + // rule were dropped, this would be admitted and `i` would wrap. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![counting_for( + 3, + 0, + Expr::Integer(1_000_000_000), + vec![set( + 2, + bin(BinaryOp::Add, Expr::LocalGet(2), Expr::Integer(1)), + )], + )], + }]; + let got = run(&stmts); + assert!( + !got.contains(&2), + "outer counter must not be admitted: {got:?}" + ); + // The inner counter is still fine — its own guard dominates its own step. + assert!(got.contains(&3)); +} + +#[test] +fn do_while_first_pass_is_unguarded() { + // `let i = 0; do { i++; } while (i < 10);` — the first `i++` runs before + // the condition is ever evaluated, so no guard dominates it. + let stmts = vec![ + let_mut(2, Some(Expr::Integer(0))), + Stmt::DoWhile { + body: vec![Stmt::Expr(inc(2))], + condition: cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10)), + }, + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_write_from_a_closure_disqualifies() { + // The gate excludes closure-referenced locals independently, but the FACT + // must not claim a bound it cannot prove: a closure body can run any + // number of times, from anywhere. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![Stmt::Expr(Expr::Closure { + func_id: 0, + params: Vec::::new(), + return_type: HirType::Void, + body: vec![Stmt::Expr(inc(2))], + captures: vec![2], + mutable_captures: vec![2], + captures_this: false, + captures_new_target: false, + enclosing_class: None, + is_arrow: true, + is_async: false, + is_generator: false, + is_strict: false, + })], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_write_after_the_loop_disqualifies() { + // for (let i = 0; i < 10; i++) {} … then `i = i + 1` outside the loop: + // that step has no guard at all. + let stmts = vec![ + counting_for(2, 0, Expr::Integer(10), vec![]), + set(2, bin(BinaryOp::Add, Expr::LocalGet(2), Expr::Integer(1))), + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_local_declared_twice_is_rejected() { + // A hoisted `var` / two arms sharing an id break the single-entry-value + // premise the interval rests on. + let stmts = vec![ + let_mut(2, Some(Expr::Integer(0))), + Stmt::If { + condition: Expr::Bool(true), + then_branch: vec![let_mut(2, Some(Expr::Integer(5)))], + else_branch: None, + }, + Stmt::For { + init: None, + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![], + }, + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_local_with_no_declaration_is_rejected() { + // A parameter (no `Stmt::Let`) has an unknown entry value. + let stmts = vec![Stmt::For { + init: None, + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(7), Expr::Integer(10))), + update: Some(inc(7)), + body: vec![], + }]; + assert!(!run(&stmts).contains(&7)); +} + +#[test] +fn a_never_stepped_local_is_not_reported() { + // `let i = 0;` with no writes is already handled by + // `strictly_i32_bounded_locals`; this fact only speaks about induction + // variables, so it must not widen its own scope. + let stmts = vec![let_mut(2, Some(Expr::Integer(0)))]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn two_guarded_loops_take_the_union_of_their_intervals() { + // let i = 0; for (; i < 10; i++) {} for (; i < 20; i++) {} + // Both writes are guarded; the interval is [0, 19]. + let stmts = vec![ + let_mut(2, Some(Expr::Integer(0))), + Stmt::For { + init: None, + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![], + }, + Stmt::For { + init: None, + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(20))), + update: Some(inc(2)), + body: vec![], + }, + ]; + assert!(run(&stmts).contains(&2)); + + // …but if the second loop's bound is out of range, the union is not. + let stmts = vec![ + let_mut(2, Some(Expr::Integer(0))), + Stmt::For { + init: None, + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![], + }, + Stmt::For { + init: None, + condition: Some(cmp( + CompareOp::Lt, + Expr::LocalGet(2), + Expr::Integer(3_000_000_000), + )), + update: Some(inc(2)), + body: vec![], + }, + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn step_under_an_if_inside_the_guarded_body_is_still_guarded() { + // A conditional step still executes at most once per iteration, so the + // per-iteration total is exact. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![Stmt::If { + condition: Expr::Bool(true), + then_branch: vec![set( + 2, + bin(BinaryOp::Add, Expr::LocalGet(2), Expr::Integer(1)), + )], + else_branch: None, + }], + }]; + assert!(run(&stmts).contains(&2)); +} + +#[test] +fn step_in_a_switch_case_and_a_finally_are_both_counted() { + // Both are reachable at most once per iteration and both must be summed + // into the per-iteration total, not silently skipped. + let body = vec![ + Stmt::Switch { + discriminant: Expr::LocalGet(2), + cases: vec![SwitchCase { + test: Some(Expr::Integer(0)), + body: vec![Stmt::Expr(inc(2))], + }], + }, + Stmt::Try { + body: vec![], + catch: Some(CatchClause { + param: None, + body: vec![], + }), + finally: Some(vec![Stmt::Expr(inc(2))]), + }, + ]; + // Three steps run per iteration (update + switch case + finally), so the + // counter tops out at `bound - 1 + 3`. At bound == INT32_MAX - 2 that is + // exactly INT32_MAX: admitted. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp( + CompareOp::Lt, + Expr::LocalGet(2), + Expr::Integer(i32::MAX as i64 - 2), + )), + update: Some(inc(2)), + body: body.clone(), + }]; + assert!(run(&stmts).contains(&2)); + + // One higher overshoots by exactly one. Counting only the `update` step + // (total 1 instead of 3) would compute 2147483646 and let this through. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp( + CompareOp::Lt, + Expr::LocalGet(2), + Expr::Integer(i32::MAX as i64 - 1), + )), + update: Some(inc(2)), + body, + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_step_by_a_const_local_amount_is_summed_at_its_value() { + // `for (let i = 0; i < 10; i = i + STEP)` with `const STEP = 4`. + let stmts = vec![ + let_const(1, 4), + Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(Expr::LocalSet( + 2, + Box::new(bin(BinaryOp::Add, Expr::LocalGet(2), Expr::LocalGet(1))), + )), + body: vec![], + }, + ]; + assert!(run(&stmts).contains(&2)); +} + +#[test] +fn a_negative_step_magnitude_is_rejected() { + // `i = i + (-1)` under a `<` guard walks downwards forever. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(Expr::LocalSet( + 2, + Box::new(bin(BinaryOp::Add, Expr::LocalGet(2), Expr::Integer(-1))), + )), + body: vec![], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn commuted_increment_is_a_step() { + // `i = 1 + i` is the same step as `i = i + 1`. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(Expr::LocalSet( + 2, + Box::new(bin(BinaryOp::Add, Expr::Integer(1), Expr::LocalGet(2))), + )), + body: vec![], + }]; + assert!(run(&stmts).contains(&2)); +} + +#[test] +fn a_step_written_in_the_loop_condition_is_not_guarded_by_that_loop() { + // `while (i++ < 10) {}` — the write happens while the guard is being + // EVALUATED, so it is not dominated by it. + let stmts = vec![ + let_mut(2, Some(Expr::Integer(0))), + Stmt::While { + condition: cmp(CompareOp::Lt, inc(2), Expr::Integer(10)), + body: vec![], + }, + ]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_module_level_const_bound_resolves() { + // `const ITERATIONS = 100000000;` at module scope, read from a function + // body: id 1 is not declared in these stmts, only in `hir.init`. + let stmts = vec![counting_for(2, 0, Expr::LocalGet(1), vec![])]; + assert!(!run(&stmts).contains(&2), "no bound without the const map"); + assert!(run_with_module_consts(&stmts, &[(1, 100_000_000.0)]).contains(&2)); +} + +#[test] +fn an_out_of_range_module_const_is_not_a_bound() { + let stmts = vec![counting_for(2, 0, Expr::LocalGet(1), vec![])]; + assert!(!run_with_module_consts(&stmts, &[(1, 3_000_000_000.0)]).contains(&2)); +} + +#[test] +fn a_fractional_module_const_is_not_a_bound() { + // `const LIMIT = 10.5` — `i` stops at 11, but the guard arithmetic + // (`bound - 1 + step`) is integer, so refuse rather than round. + let stmts = vec![counting_for(2, 0, Expr::LocalGet(1), vec![])]; + assert!(!run_with_module_consts(&stmts, &[(1, 10.5)]).contains(&2)); +} + +#[test] +fn a_with_block_fallback_write_disqualifies() { + // `with (obj) { i = 4000000000; }` writes `i` through + // `Expr::WithSet`'s fallback, NOT through a `LocalSet`. Without the + // fallback arm the analysis never sees the write and admits `i`. + let stmts = vec![Stmt::For { + init: Some(Box::new(let_mut(2, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Lt, Expr::LocalGet(2), Expr::Integer(10))), + update: Some(inc(2)), + body: vec![Stmt::Expr(Expr::WithSet { + object: Box::new(Expr::LocalGet(9)), + property: "i".into(), + value: Box::new(Expr::Integer(4_000_000_000)), + fallback: perry_hir::WithSetFallback::Local(2), + strict: false, + })], + }]; + assert!(!run(&stmts).contains(&2)); +} + +#[test] +fn a_with_block_fallback_write_also_kills_a_constant_bound() { + // Same mechanism one level up: a `const`-looking bound that a `with` + // block can reassign is not a compile-time constant. + let stmts = vec![ + let_const(1, 100), + Stmt::Expr(Expr::WithSet { + object: Box::new(Expr::LocalGet(9)), + property: "LIMIT".into(), + value: Box::new(Expr::Integer(4_000_000_000)), + fallback: perry_hir::WithSetFallback::SloppyImplicit(1), + strict: false, + }), + counting_for(2, 0, Expr::LocalGet(1), vec![]), + ]; + assert!(!run(&stmts).contains(&2)); +} diff --git a/crates/perry-codegen/src/collectors/mod.rs b/crates/perry-codegen/src/collectors/mod.rs index e07d6d80f4..90ebd15fd8 100644 --- a/crates/perry-codegen/src/collectors/mod.rs +++ b/crates/perry-codegen/src/collectors/mod.rs @@ -20,6 +20,7 @@ mod index_uses; mod int_valued_ta_locals; mod integer_locals; mod local_refs; +mod loop_bounded_i32; mod mutation; mod not_bigint_locals; mod pointer_locals; diff --git a/crates/perry-codegen/src/expr/slot_rep.rs b/crates/perry-codegen/src/expr/slot_rep.rs index 1dea0b2ec1..9fa0b73fb6 100644 --- a/crates/perry-codegen/src/expr/slot_rep.rs +++ b/crates/perry-codegen/src/expr/slot_rep.rs @@ -53,6 +53,14 @@ //! - `int_valued_ta_locals` (merged into `integer_locals`): every write i32 or //! a possibly-OOB int-TA read whose every observation is ToInt32-coercing; //! NaN-safe entry conversion (`toint32_wrap`) keeps OOB `undefined` → 0. +//! - `loop_bounded_i32_locals` (#7110): a monotone induction variable whose +//! reachable interval is a pair of compile-time i32 constants — single +//! literal init, every write a `+k`/`-k` step dominated by a +//! constant-bounded guard on the immediately enclosing loop, direction +//! agreeing with the guard. A real range argument, not a compatibility +//! bound: there is no reachable state in which the value leaves i32. A bare +//! accumulator is deliberately NOT admitted — see +//! `collectors/loop_bounded_i32.rs`. //! - `integer_locals ∩ index_used_locals`: admission accepts `Add/Sub/Mul` //! chains that can in principle exceed i32 — but under the pre-phase shadow //! model every `LocalGet` of such a local ALREADY reads the i32 slot @@ -317,9 +325,12 @@ impl CanonicalI32Denial { if self.not_index_used_or_bounded { return Some(( "not_index_used_or_bounded", - "proven integer-valued, but never used as an array index and \ - not provably i32-bounded, so nothing pins its range to 32 bits \ - — a bare accumulator or counter lands here", + "proven integer-valued, but never used as an array index, not \ + provably i32-bounded, and not a constant-bounded loop \ + induction variable (#7110), so nothing pins its range to 32 \ + bits. A bare accumulator lands here and must: \ + `sum = sum + (i % 1000)` over 1e8 iterations really does reach \ + 4.995e10, so an i32 slot would print a wrapped negative", Tier::CompilerLimitation, Some(NOT_BOUNDED_ISSUE), )); diff --git a/crates/perry-codegen/src/stmt/let_stmt.rs b/crates/perry-codegen/src/stmt/let_stmt.rs index ad1ed48d48..ff6a1ae6ba 100644 --- a/crates/perry-codegen/src/stmt/let_stmt.rs +++ b/crates/perry-codegen/src/stmt/let_stmt.rs @@ -1256,15 +1256,25 @@ pub(crate) fn lower_let( // (array-valued), and async/generator contexts (gated at FnCtx build). // See `expr/slot_rep.rs` for the mechanism and range-soundness audit. // - // Canonical-only safety term: an `int_valued_ta_locals` member (#6898) is - // eligible even when neither index-used nor strictly-i32-bounded — its - // whole-function proof (every write i32-producing or an int-kind TA read, - // every observation ToInt32-coercing) makes canonical-i32 storage - // output-invariant with the NaN-safe entry conversion. The parallel-shadow - // gate (`needs_i32_slot` below) is deliberately NOT widened, so the - // flag-off model stays exactly the pre-phase one. - let canonical_safe_local = - i32_safe_local || ctx.native_facts.int_valued_ta_locals().contains(&id); + // Canonical-only safety terms. The parallel-shadow gate (`needs_i32_slot` + // above) is deliberately NOT widened by either, so the flag-off model stays + // exactly the pre-phase one. + // + // * `int_valued_ta_locals` (#6898): every write i32-producing or an int-kind + // TA read, every observation ToInt32-coercing — which makes canonical-i32 + // storage output-invariant with the NaN-safe entry conversion. + // * `loop_bounded_i32_locals` (#7110): a monotone induction variable whose + // whole reachable interval is a pair of compile-time i32 constants — + // single literal init, every write a step dominated by a constant-bounded + // guard on the immediately enclosing loop. This is the term that admits a + // plain `for (let i = 0; i < 1000000; i++)` counter, which satisfies + // neither `index_used_locals` (nothing is indexed) nor + // `strictly_i32_bounded_locals` (`i++` disqualifies there, #6072). + // See `collectors/loop_bounded_i32.rs` for the interval argument — and + // for why a bare accumulator is NOT admitted by it. + let canonical_safe_local = i32_safe_local + || ctx.native_facts.int_valued_ta_locals().contains(&id) + || ctx.native_facts.loop_bounded_i32_locals().contains(&id); // Split into the VALUE-level proof and the CONTEXT gate so a context-level // exclusion can be reported (#7106). `canonical_i32` is the conjunction, so // selection behaviour is unchanged. diff --git a/scripts/compiler_output_harness/repsel_census.py b/scripts/compiler_output_harness/repsel_census.py index a628578056..8428370f93 100644 --- a/scripts/compiler_output_harness/repsel_census.py +++ b/scripts/compiler_output_harness/repsel_census.py @@ -198,6 +198,12 @@ "canonical-u32": 1, "canonical-str": 1, }, + # #7110: every canonical-i32 promotion in this fixture comes from the + # loop-induction range proof and from nothing else -- no bitwise mixing, no + # `| 0`, no array indexing. Pinned at the exact count it is written to + # promote (2 counters + 1 in the accumulator loop), so losing any one of the + # three goes red rather than silently degrading to "still nonzero". + "fixture_loop_bounded_i32": {"canonical-i32": 3}, "fixture_int_valued_ta": {"int-valued-ta": 1}, "fixture_spec_abi_taptr": {"spec-abi-entry": 1, "spec-abi-taptr-slot": 1}, } diff --git a/test-files/test_gap_repsel_loop_bounded_i32.ts b/test-files/test_gap_repsel_loop_bounded_i32.ts new file mode 100644 index 0000000000..98d472fd26 --- /dev/null +++ b/test-files/test_gap_repsel_loop_bounded_i32.ts @@ -0,0 +1,167 @@ +// Repsel Phase 1, #7110: canonical unboxed i32 storage for a monotone loop +// induction variable — a counter that is NOT used as an array index and is NOT +// in `strictly_i32_bounded_locals` (`i++` disqualifies a local there, #6072). +// +// Byte-compared against `node --experimental-strip-types`. Every number below +// is chosen so that a WRONG answer is loud rather than plausible: the values +// sit on the i32 boundary, where an unsound admission wraps to a large negative +// instead of drifting by one. +// +// The three functions the analysis must REFUSE (`overshoot`, `runtimeBound`, +// `accumulate`) are the point of this file as much as the ones it admits. An +// i32 slot for any of them prints a wrapped negative here, and Node prints the +// true value. Keep them. + +// --- Admitted: interval endpoints are compile-time i32 constants ------------ + +const ROUNDS = 4096; + +// `i < 2147483647` with a `++` step tops out at exactly INT32_MAX. +function topOut(): number { + let i = 2147483640; + for (; i < 2147483647; i++) {} + return i; +} + +// Descending across zero: interval [-2147483641, 10]. +function descend(): number { + let i = 10; + for (; i > -2147483648; i--) { + if (i < -2147483640) { + break; + } + } + return i; +} + +// A module-level `const` bound, the `for (let i = 0; i < ITERATIONS; i++)` +// shape. Sums into a float so the accumulator is not itself a candidate. +function moduleConstBound(): number { + let acc = 0.5; + for (let i = 0; i < ROUNDS; i++) { + acc = acc + 0.25; + } + return acc; +} + +// A `while` with a CONJUNCTIVE guard and a `LocalSet` Add step rather than +// `++` — the 15_mandelbrot `iter` shape. +function whileConjunct(seed: number): number { + let iter = 0; + let x = seed; + while (x < 1000.0 && iter < 100) { + x = x * 1.5; + iter = iter + 1; + } + return iter; +} + +// Two steps per iteration (update + body) and a step larger than one: the +// counter overshoots the bound by the per-iteration total, which the interval +// has to account for. +function twoSteps(): string { + let a = 0; + for (; a < 10; a++) { + a = a + 1; + } + let b = 0; + for (; b < 10; b = b + 4) {} + return a + "/" + b; +} + +// The counter observed through boxed use sites: value-position `++`/`--`, +// string concat, `typeof`, division, negation, JSON. +function observed(): string { + let out = ""; + let i = 0; + for (; i < 4; i++) { + out = out + i++ + ":" + typeof i + ":" + i / 2 + ":" + JSON.stringify({ k: -i }) + ";"; + } + let j = 3; + for (; j > 0; j--) { + out = out + --j + "|"; + } + return out + "end=" + i + "," + j; +} + +// --- Refused: no compile-time i32 interval exists --------------------------- + +// `i <= 2147483647` lets the counter reach 2147483648, one past INT32_MAX. +// `break` keeps the test fast; the proof obligation is a property of the loop +// text, not of the trip count. +function overshoot(): number { + let i = 2147483640; + for (; i <= 2147483647; i++) { + if (i > 2147483642) { + break; + } + } + return i; +} + +// A runtime bound is not a constant: #6072's runaway shape, where `limit` +// exceeds INT32_MAX and a wrapped i32 counter spins forever. +function runtimeBound(limit: number): number { + let i = 2147483640; + for (; i < limit; i++) { + if (i > 2147483645) { + break; + } + } + return i; +} + +// A bare accumulator has no guard bounding it. `benchmarks/suite/13_factorial.ts` +// is the same shape at 1e8 iterations, where the true total is 49,950,000,000. +function accumulate(): number { + let sum = 0; + for (let i = 0; i < ROUNDS; i++) { + sum = sum + 1000000; + } + return sum; +} + +// The two RUNTIME-OBSERVABLE overflow probes. Every other refusal above is only +// checkable in `--opt-report`; these two print a different number if the +// analysis admits them, in three iterations rather than 2^31. +// +// `i` steps by 2e9 under a `<= INT32_MAX` guard, so it exits at 4e9 — a value an +// i32 slot cannot hold. Dropping the interval's `fits_i32` check admits it, the +// step wraps to -294967296, the guard is true again, and the loop runs until the +// `steps` fuse trips: a different printed value, not a hang. +function bigStepOverflow(): number { + let i = 0; + let steps = 0; + for (; i <= 2147483647; i = i + 2000000000) { + steps = steps + 1; + if (steps > 5) { + break; + } + } + return i; +} + +// The descending mirror: exits at -4e9. +function bigStepUnderflow(): number { + let i = 0; + let steps = 0; + for (; i >= -2147483648; i = i - 2000000000) { + steps = steps + 1; + if (steps > 5) { + break; + } + } + return i; +} + +console.log("topOut:" + topOut()); +console.log("descend:" + descend()); +console.log("moduleConstBound:" + moduleConstBound()); +console.log("whileConjunct:" + whileConjunct(1.0)); +console.log("twoSteps:" + twoSteps()); +console.log("observed:" + observed()); +console.log("overshoot:" + overshoot()); +console.log("runtimeBound:" + runtimeBound(2147483653)); +console.log("accumulate:" + accumulate()); +console.log("bigStepOverflow:" + bigStepOverflow()); +console.log("bigStepUnderflow:" + bigStepUnderflow()); diff --git a/test-parity/gc_repsel_corpus.txt b/test-parity/gc_repsel_corpus.txt index 91ed6f8535..49c1ef7be7 100644 --- a/test-parity/gc_repsel_corpus.txt +++ b/test-parity/gc_repsel_corpus.txt @@ -15,6 +15,15 @@ test_gap_repsel_canonical_i32 test_gap_int_valued_ta_locals +# --- Phase 1 widening: constant-bounded loop induction variables (#7110) ---- +# A counter that is neither index-used nor `strictly_i32_bounded` now takes +# canonical i32 storage when the loop guard pins its whole interval inside i32. +# Three functions in the file are there to be REFUSED (`overshoot`, +# `runtimeBound`, `accumulate`); an i32 slot for any of them prints a wrapped +# negative where Node prints the true value, so this file fails loudly under an +# unsound widening rather than drifting by one. +test_gap_repsel_loop_bounded_i32 + # --- Phase 2: specialized calling convention / spec-ABI raw params (#6905) -- test_gap_specabi_polymorphic_coexist test_gap_specabi_reassign