Files
scriptc/tests
Malte Ubl ea8cd32016 Close loop-carried locals under exact integer arithmetic
analyzeIntegerRanges discarded loop-carried facts except for closed locals,
whose writes only qualified syntactically (bitwise results, literals,
imul/clz32). A local like `v = (v * 31 + n) % 1000003` stayed a double, so
every iteration paid fmul/fadd plus the checked floating remainder
(fptosi, exactness and 2^53 range checks, srem, -0 select, sitofp).

The closure now evaluates each write by the same interval rules as
`expr` (exact safe integers, never -0: `*` refuses a zero times a
negative, `%` needs a non-negative dividend and positive divisor, unary
minus refuses ranges containing 0) while every candidate is assumed
inside a fixed bound: int32, uint32, or the new non-negative int32 bound
that `%` closes under. The greatest fixpoint keeps candidates whose every
write lands inside the bound; their range then narrows to the entry fact
joined with the writes' values (sound by induction over the region), and
the closures intersect. A for loop's counter, which only the update
writes, contributes its header range to reads inside the region, so
`h = (h * 131 + i) % 65521` closes too.

The kernel's v becomes an i32 slot with mul/add nsw i32 and urem i32.
Corpus 5321 pins the closed forms and every case that must stay double
(negative dividends and -0, products above 2^53, NaN/Infinity/fraction
entries, zero and fractional divisors) against Node.
2026-10-15 04:46:12 -07:00
..
2026-07-22 18:08:04 -05:00