From 0e943fedb074ce03ab496fb0fe8e032e59831785 Mon Sep 17 00:00:00 2001 From: Malte Ubl Date: Thu, 15 Oct 2026 06:34:13 -0700 Subject: [PATCH] Bound while counters by their loop condition While loops discarded every loop-carried fact, so the escape-time counter in `while (x * x + y * y <= 4 && it < MAX) { ...; it++ }` stayed a double: its increment, its bound compare and the `it === MAX` test after the loop all ran in floating point. guardedLoopCounterFacts bounds a counter that the loop changes only by increments of positive integer literals outside nested loops, switch and exception regions, when a conjunct of the condition compares it below a literal or a binding the loop never writes, and the condition itself never writes it. The body runs only after that conjunct held, so every pass starts at most at the bound and climbs by at most the sum of the body's increments; the counter starts at its entry fact and only grows. The range holds at every read inside and after the loop, so it also feeds the loop-carried closure as an invariant. The mandelbrot counter becomes an i32 slot. Corpus 5333 pins escape-time, reversed, inclusive, multi-increment, early-exit and module-level counters, and every case that must stay double (counters written by their condition, decrements, fractional and unknown steps, nested increments, written bounds, disjunctions, fractional, -0, NaN and infinite starts, limits past 2^31, 2^32 and 2^53) against Node. --- .../compiler/src/ir/integer-loop-facts.ts | 106 +++++++++++++++ .../compiler/src/ir/integer-ranges.test.ts | 95 ++++++++++++++ packages/compiler/src/ir/integer-ranges.ts | 16 ++- ...333-integer-guarded-while-counters.ts.json | 6 + .../5333-integer-guarded-while-counters.ts | 122 ++++++++++++++++++ 5 files changed, 342 insertions(+), 3 deletions(-) create mode 100644 packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json create mode 100644 tests/corpus/5333-integer-guarded-while-counters.ts diff --git a/packages/compiler/src/ir/integer-loop-facts.ts b/packages/compiler/src/ir/integer-loop-facts.ts index d18f42297..0017a152c 100644 --- a/packages/compiler/src/ir/integer-loop-facts.ts +++ b/packages/compiler/src/ir/integer-loop-facts.ts @@ -154,6 +154,112 @@ export function boundedIntegerLoopFacts( return result; } +/** Bound counters of a while loop by its condition. A counter qualifies when + * the loop (condition and body) changes it only by increments of positive + * integer literals outside nested loops, switch and exception regions, and a + * conjunct of the condition compares it below a literal or a binding the loop + * never writes (`while (x * x + y * y <= 4 && it < MAX) it++`). The body runs + * only after that conjunct held, and the condition never writes the counter, + * so every pass starts at most at the conjunct's bound and climbs by at most + * the sum of the body's increments. The counter starts at its entry fact and + * only grows, so the range holds at every read inside and after the loop. */ +export function guardedLoopCounterFacts( + loop: IrStmt & { kind: "while" }, + locals: ReadonlyMap, + initial: ReadonlyMap, +): ReadonlyMap { + const result = new Map(); + const budget = new Map(), + refused = new Set(); + let opaque = 0; + const write = (id: string, delta: number | null): void => { + if (opaque || delta === null || delta <= 0 || delta > 2147483647) refused.add(id); + else budget.set(id, (budget.get(id) ?? 0) + delta); + }; + const expr = (e: IrExpr): boolean => { + if (e.kind === "assignExpr") write(e.localId, increment(e.localId, e.value)); + if (e.kind === "incDec") write(e.localId, e.op === "+" ? 1 : null); + return everyExprChild(e, expr, stmt); + }; + const stmt = (s: IrStmt): boolean => { + const region = + s.kind === "for" || + s.kind === "while" || + s.kind === "doWhile" || + s.kind === "forOf" || + s.kind === "tryCatch" || + s.kind === "switch"; + if (region) opaque++; + if (s.kind === "assign") write(s.localId, increment(s.localId, s.value)); + if (s.kind === "varDecl" || s.kind === "forOf") write(s.localId, null); + if (s.kind === "tryCatch" && s.catchLocalId) write(s.catchLocalId, null); + const completed = everyStmtChild(s, expr, stmt); + if (region) opaque--; + return completed; + }; + // The condition is evaluated before every pass; a write there would + // separate the compared value from the one the body sees. + const condition = new Set(); + const conditionWrites = (e: IrExpr): boolean => { + if (e.kind === "assignExpr" || e.kind === "incDec") condition.add(e.localId); + return everyExprChild(e, conditionWrites, (s) => { + opaque++; + stmt(s); + opaque--; + return true; + }); + }; + conditionWrites(loop.cond); + for (const id of condition) refused.add(id); + loop.body.every(stmt); + const stable = (id: string): boolean => { + const local = locals.get(id); + return local !== undefined && !local.boxed && !local.tdz && !budget.has(id) && !refused.has(id); + }; + const limit = (e: IrExpr): IntegerRange | null => { + if (e.kind === "numLit" && Number.isSafeInteger(e.value) && !Object.is(e.value, -0)) + return { min: e.value, max: e.value }; + if (e.kind === "varRef" && stable(e.localId)) return initial.get(e.localId) ?? null; + return null; + }; + // Conjuncts that hold whenever the body runs. + const conjuncts: IrExpr[] = []; + const collect = (e: IrExpr): void => { + if (e.kind === "toBool") collect(e.operand); + else if (e.kind === "logical" && e.op === "&&") { + collect(e.left); + collect(e.right); + } else conjuncts.push(e); + }; + collect(loop.cond); + const ceiling = new Map(); + for (const c of conjuncts) { + if (c.kind !== "bin") continue; + // `counter < bound` or `bound > counter` (and the inclusive forms). + const below = c.op === "<" || c.op === "<=", + above = c.op === ">" || c.op === ">="; + const counter = below ? c.left : above ? c.right : null, + other = below ? c.right : c.left; + if (counter?.kind !== "varRef") continue; + const bound = limit(other); + if (!bound) continue; + const hi = c.op === "<" || c.op === ">" ? bound.max - 1 : bound.max; + const previous = ceiling.get(counter.localId); + ceiling.set(counter.localId, previous === undefined ? hi : Math.min(previous, hi)); + } + for (const [id, step] of budget) { + const local = locals.get(id), + start = initial.get(id), + hi = ceiling.get(id); + if (refused.has(id) || !local || local.boxed || local.tdz || !start || hi === undefined) + continue; + const max = Math.max(start.max, hi + step); + if (Number.isSafeInteger(start.min) && Number.isSafeInteger(max)) + result.set(id, { min: start.min, max }); + } + return result; +} + /** Recognize only exits whose target cannot be inside this statement list. * Labeled blocks, loops, switch and exception regions retain the join. */ export function integerPathFallsThrough(body: readonly IrStmt[]): boolean { diff --git a/packages/compiler/src/ir/integer-ranges.test.ts b/packages/compiler/src/ir/integer-ranges.test.ts index 9ee1d55ff..ac9e4a98a 100644 --- a/packages/compiler/src/ir/integer-ranges.test.ts +++ b/packages/compiler/src/ir/integer-ranges.test.ts @@ -611,6 +611,101 @@ test("a loop-invariant positive step bounds the counter of a limited loop", () = expect(loop(step, update, body).inside, label).toBeNull(); }); +test("a while condition bounds a counter the loop only increments", () => { + // it = start; while (unknown <= 4 && it < MAX) { observe(it); it++ } observe(it) + const set = (localId: string, value: IrExpr): IrStmt => ({ loc, kind: "assign", localId, value }); + const bump = (op: "+" | "-" = "+"): IrStmt => ({ + loc, + kind: "exprStmt", + expr: { loc, kind: "incDec", op, prefix: false, localId: "it", type: F64 }, + }); + const and = (left: IrExpr, right: IrExpr): IrExpr => ({ + loc, + kind: "logical", + op: "&&", + left, + right, + type: BOOL, + }); + const run = ( + options: { + start?: IrExpr; + cond?: IrExpr; + body?: IrStmt[]; + before?: IrStmt[]; + } = {}, + ) => { + const inside = ref("it"), + after = ref("it"); + const f = fn([ + set("max", num(300)), + set("it", options.start ?? num(0)), + ...(options.before ?? []), + { + loc, + kind: "while", + cond: + options.cond ?? + and(condition("<=", ref("unknown"), num(4)), condition("<", ref("it"), ref("max"))), + body: options.body ?? [observe(inside), bump()], + }, + observe(after), + ]); + for (const id of ["it", "max"]) f.locals.push({ id, name: id, type: F64, mutable: true }); + const ranges = analyzeIntegerRanges(f); + return { inside: ranges.get(inside), after: ranges.get(after) }; + }; + expect(run()).toEqual({ inside: { min: 0, max: 299 }, after: { min: 0, max: 300 } }); + // `MAX > it`, an inclusive bound, two increments per pass and an early exit. + expect(run({ cond: condition(">", ref("max"), ref("it")) }).after).toEqual({ min: 0, max: 300 }); + expect(run({ cond: condition("<=", ref("it"), num(10)) }).after).toEqual({ min: 0, max: 11 }); + const twice = [observe(ref("it")), bump(), set("it", bin("+", ref("it"), num(2)))]; + expect(run({ body: twice }).after).toEqual({ min: 0, max: 302 }); + const exit: IrStmt = { + loc, + kind: "if", + cond: condition("===", ref("unknown"), num(0)), + then: [{ loc, kind: "break" }], + else_: null, + }; + expect(run({ body: [exit, bump()] }).after).toEqual({ min: 0, max: 300 }); + // A start above the bound stays the entry value. + expect(run({ start: num(500) }).after).toEqual({ min: 500, max: 500 }); + // Decrements, fractional or variable steps, increments in a nested loop, + // writes in the condition, a bound the loop writes, a disjunction, and an + // unknown start prove nothing. + const nested: IrStmt = { + loc, + kind: "while", + cond: condition("<", ref("unknown"), num(3)), + body: [bump()], + }; + const counted: IrExpr = { loc, kind: "incDec", op: "+", prefix: false, localId: "it", type: F64 }; + const open: [string, Parameters[0]][] = [ + ["decrement", { body: [bump("-")] }], + ["fraction step", { body: [set("it", bin("+", ref("it"), num(0.5)))] }], + ["variable step", { body: [set("it", bin("+", ref("it"), ref("unknown")))] }], + ["nested increment", { body: [nested] }], + ["condition write", { cond: condition("<", counted, ref("max")), body: [] }], + ["written bound", { body: [bump(), set("max", num(1e12))] }], + [ + "disjunction", + { + cond: { + loc, + kind: "logical", + op: "||", + left: condition("<=", ref("unknown"), num(4)), + right: condition("<", ref("it"), ref("max")), + type: BOOL, + }, + }, + ], + ["unknown start", { start: ref("unknown") }], + ]; + for (const [label, options] of open) expect(run(options).after, label).toBeNull(); +}); + test("whole-program slot facts seed parameters, field reads and call results", () => { const field: IrExpr = { loc, diff --git a/packages/compiler/src/ir/integer-ranges.ts b/packages/compiler/src/ir/integer-ranges.ts index 25afcdfee..2277b632c 100644 --- a/packages/compiler/src/ir/integer-ranges.ts +++ b/packages/compiler/src/ir/integer-ranges.ts @@ -1,7 +1,11 @@ import type { IrExpr, IrFunction, IrStmt } from "./ir.js"; import { everyExprChild, everyStmtChild, everyStmtList } from "./traverse.js"; import { byteNumberAccess, byteNumberRange } from "./byte-numbers.js"; -import { boundedIntegerLoopFacts, integerPathFallsThrough } from "./integer-loop-facts.js"; +import { + boundedIntegerLoopFacts, + guardedLoopCounterFacts, + integerPathFallsThrough, +} from "./integer-loop-facts.js"; /** Exactly representable integers, excluding negative zero. Facts describe * the evaluated value, never a later read of the same local binding. */ @@ -846,15 +850,21 @@ export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = { } case "while": case "doWhile": { + // Counters the condition bounds keep their range at every read + // inside and after the loop. + const guarded = + s.kind === "while" ? guardedLoopCounterFacts(s, loopLocals, facts) : noInvariants; const loop = new Map(facts); - havoc(loop, [s], loop); + havocWith(loop, [s], loop, guarded); + for (const [id, range] of guarded) set(loop, id, range); const header = new Map(loop); expr(s.cond, header); if (s.kind === "while") { refine(s.cond, true, header); body(s.body, header); } else body(s.body, new Map(loop)); - havoc(facts, [s], facts); + havocWith(facts, [s], facts, guarded); + for (const [id, range] of guarded) set(facts, id, range); break; } case "forOf": { diff --git a/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json b/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json new file mode 100644 index 000000000..113a84867 --- /dev/null +++ b/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json @@ -0,0 +1,6 @@ +{ + "order": [ + "/tests/corpus/5333-integer-guarded-while-counters.ts" + ], + "diags": [] +} diff --git a/tests/corpus/5333-integer-guarded-while-counters.ts b/tests/corpus/5333-integer-guarded-while-counters.ts new file mode 100644 index 000000000..cd43cc5dc --- /dev/null +++ b/tests/corpus/5333-integer-guarded-while-counters.ts @@ -0,0 +1,122 @@ +// While-loop counters that the loop only increments by integer literals and +// that a conjunct of the condition bounds (`it < MAX` in an escape-time +// loop) stay exact integers. Counters written in the condition, decremented, +// stepped by fractions or unknown values, or incremented inside nested +// loops, bounds the loop writes, disjunctions, and limits near 2^31, 2^32 +// and 2^53 keep ordinary double behavior. + +const MAX: number = 300; + +function escape(cx: number, cy: number): number { + let x: number = 0; + let y: number = 0; + let it: number = 0; + while (x * x + y * y <= 4 && it < MAX) { + const xt: number = x * x - y * y + cx; + y = 2 * x * y + cy; + x = xt; + it++; + } + return it; +} +let inside: number = 0; +let total: number = 0; +for (let py: number = 0; py < 24; py++) { + for (let px: number = 0; px < 32; px++) { + const it: number = escape((px / 32) * 3 - 2, (py / 24) * 2 - 1); + total += it; + if (it === MAX) inside++; + } +} +console.log("escape", inside, total, escape(0, 0), escape(2, 2)); + +// Reversed and inclusive bounds, two increments per pass, early exits and +// continue, a counter used as an index and a remainder operand. +function shapes(limit: number): string { + const table: Int32Array = new Int32Array(64); + let a: number = 0; + while (limit > a) a += 3; + let b: number = 1; + while (b <= 40) { + b++; + if (b % 7 === 0) continue; + b += 2; + } + let c: number = 0; + while (c < 63) { + table[c] = c % 5; + if (table[c] === 4 && c > 50) break; + c++; + } + let sum: number = 0; + for (let i: number = 0; i < 64; i++) sum += table[i]; + return `${a} ${b} ${c} ${sum}`; +} +console.log("shapes", shapes(10), shapes(0), shapes(-5), shapes(64)); + +// A module-level counter in the initializer. +let steps: number = 0; +while (steps < 1000 && (steps * 7) % 11 !== 10) steps++; +console.log("module", steps); + +// Entries outside the proof: fractions, -0, NaN and Infinity starts. +function starts(start: number): string { + let i: number = start; + while (i < 5) i++; + return `${i} ${Object.is(i, -0)}`; +} +console.log("starts", starts(0.5), starts(-0), starts(NaN), starts(Infinity), starts(-2), starts(9)); + +// Counters that cross 2^31, 2^32 and 2^53 under their bound. +function wide(): string { + let i: number = 0; + while (i < 3000000000) i += 1000000000; + let j: number = 2147483600; + while (j < 2147483647) j += 13; + let k: number = 9007199254740980; + while (k < 9007199254740991) k += 4; + let u: number = 4294967290; + while (u <= 4294967295) u++; + return `${i} ${j} ${k} ${u} ${j | 0} ${u >>> 0}`; +} +console.log("wide", wide()); + +// Forms the proof refuses: a counter written by its condition, decrements, +// unknown and fractional steps, nested increments, written bounds and +// disjunctions. (The first counter stays bounded: its condition writes only +// `budget`, which is not the counter.) +function refused(n: number): string { + let a: number = 0; + let budget: number = n; + while (budget-- > 0 && a < 10) a++; + let b: number = 0; + while (b++ < 5) b += 0; + let c: number = 10; + while (c < 20) { + c++; + c--; + c += 2; + } + let d: number = 0; + while (d < 3) d += 0.75; + let e: number = 0; + while (e < 20) e += n; + let f: number = 0; + while (f < 6) { + let g: number = 0; + while (g < 3) { + f++; + g++; + } + } + let h: number = 0; + let cap: number = 4; + while (h < cap) { + h++; + if (h === 3) cap = 4.5; + } + let k: number = 0; + while (k < 3 || k === 3) k++; + return `${a} ${budget} ${b} ${c} ${d} ${e} ${f} ${h} ${cap} ${k}`; +} +console.log("refused", refused(3), refused(25));