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.

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<string, IrLocal>,
+  initial: ReadonlyMap<string, IntegerRange>,
+): ReadonlyMap<string, IntegerRange> {
+  const result = new Map<string, IntegerRange>();
+  const budget = new Map<string, number>(),
+    refused = new Set<string>();
+  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<string>();
+  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<string, number>();
+  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 {

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<typeof run>[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,

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": {

packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5333-integer-guarded-while-counters.ts.json

@@ -0,0 +1,6 @@
+{
+ "order": [
+  "<repo>/tests/corpus/5333-integer-guarded-while-counters.ts"
+ ],
+ "diags": []
+}

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));