From d69f1a99d8225d714d26ed3a2507b4155e84610b Mon Sep 17 00:00:00 2001 From: BREW <81044362+b-re-w@users.noreply.github.com> Date: Sat, 17 Oct 2026 17:41:15 +0900 Subject: [PATCH 1/3] Feat: Interval proofs from guards and locals drop provably safe integer checks (#148) --- .../src/main/python/typedpython/cgen.py | 45 +- .../src/main/python/typedpython/frontend.py | 233 ++++++- .../src/main/python/typedpython/ir.py | 13 +- .../main/python/typedpython/runtime/API.md | 10 + .../python/typedpython/runtime/tp_runtime.h | 32 + .../src/main/python/typedpython/verify.py | 305 ++++++++- .../src/test/python/test_cgen.py | 25 +- .../src/test/python/test_frontend.py | 7 +- .../src/test/python/test_frontend_classes.py | 7 +- .../src/test/python/test_interval_proofs.py | 586 ++++++++++++++++++ .../src/test/python/test_verify.py | 27 +- 11 files changed, 1200 insertions(+), 90 deletions(-) create mode 100644 python-multiplatform-ksp/src/test/python/test_interval_proofs.py diff --git a/python-multiplatform-ksp/src/main/python/typedpython/cgen.py b/python-multiplatform-ksp/src/main/python/typedpython/cgen.py index cb99f79d0..0f9b39768 100644 --- a/python-multiplatform-ksp/src/main/python/typedpython/cgen.py +++ b/python-multiplatform-ksp/src/main/python/typedpython/cgen.py @@ -169,6 +169,18 @@ class CGenError(Exception): _I64_DEOPT = {ir.BinOpKind.ADD, ir.BinOpKind.SUB, ir.BinOpKind.MUL, ir.BinOpKind.FLOORDIV, ir.BinOpKind.TRUEDIV} _INT64_MIN, _INT64_MAX = -(2 ** 63), 2 ** 63 - 1 +# `proven` on an I64 op (ir.BinOp.proven): ADD/SUB/MUL cannot overflow; FLOORDIV/MOD by a Const +# power of two of a value >= 0 become a shift / mask. +_SHIFT_OPS = {ir.BinOpKind.FLOORDIV, ir.BinOpKind.MOD} +_PROVEN_OPS = {ir.BinOpKind.ADD, ir.BinOpKind.SUB, ir.BinOpKind.MUL} | _SHIFT_OPS + + +def _pow2_shift(divisor: ir.Expr) -> int | None: + """k when `divisor` is the Const 2**k (k >= 0), else None.""" + v = divisor.value if isinstance(divisor, ir.Const) and divisor.type is Type.I64 else None + if type(v) is int and v >= 1 and v & (v - 1) == 0: + return v.bit_length() - 1 + return None # --- C literals and identifiers ------------------------------------------------------------------ @@ -287,7 +299,7 @@ def _all_exprs(f: ir.Function): def _can_deopt(e: ir.Expr, functions: dict[str, ir.Function]) -> bool: if isinstance(e, ir.BinOp) and e.left.type is Type.I64 and e.op in _I64_DEOPT: - return not e.proven # a proven op cannot deopt (overflow = SystemError) + return not e.proven # a proven op cannot deopt (no overflow, or a shift / mask) if isinstance(e, ir.UnaryOp) and e.op is ir.UnaryOpKind.NEG and e.operand.type is Type.I64: return not e.proven if isinstance(e, (ir.Unbox, ir.CheckExact)): @@ -632,12 +644,16 @@ def _check_function(f: ir.Function, functions: dict[str, ir.Function]) -> None: raise CGenError(f"{f.name}: marked pure but contains an effect ({what})") for e in _all_exprs(f): if isinstance(e, (ir.BinOp, ir.UnaryOp)) and e.proven: - checked = (e.op in (ir.BinOpKind.ADD, ir.BinOpKind.SUB, ir.BinOpKind.MUL) - if isinstance(e, ir.BinOp) else e.op is ir.UnaryOpKind.NEG) + checked = (e.op in _PROVEN_OPS if isinstance(e, ir.BinOp) + else e.op is ir.UnaryOpKind.NEG) operand = e.left if isinstance(e, ir.BinOp) else e.operand if not checked or operand.type is not Type.I64: raise CGenError(f"{f.name}: proven is set on {e.op.name} of {operand.type} " - "(ir.py: I64 ADD/SUB/MUL and NEG only)") + "(ir.py: I64 ADD/SUB/MUL, FLOORDIV/MOD by a power of two, and NEG " + "only)") + if isinstance(e, ir.BinOp) and e.op in _SHIFT_OPS and _pow2_shift(e.right) is None: + raise CGenError(f"{f.name}: proven {e.op.name} needs a Const power-of-two divisor " + f"(ir.py), got {e.right!r}") if isinstance(e, ir.Call): callee = functions.get(e.function) if callee is None: @@ -788,14 +804,6 @@ def check(self, call: str) -> None: self.emit(f"tp_s = {call};") self.emit("if (tp_s != 0) { tp_rc = tp_s; goto tp_exit; }") - def check_proven(self, call: str) -> None: - """A checked I64 helper on a `proven` op (ir.BinOp.proven): it can only return 0 or 1, and - 1 means the front end's and the verifier's proof was wrong, an internal error, never a - deopt (a proven op may sit after an effect).""" - self.emit(f"tp_s = {call};") - self.emit("if (tp_s != 0) { PyErr_SetString(PyExc_SystemError, " - "\"typedpython: proven operation overflowed\"); tp_rc = -1; goto tp_exit; }") - def fail(self) -> None: self.emit("{ tp_rc = -1; goto tp_exit; }") @@ -877,8 +885,15 @@ def ev_BinOp(self, e: ir.BinOp) -> str: a, b = self.ev(e.left), self.ev(e.right) if lt is Type.I64: t = self.tmp("double" if e.op is ir.BinOpKind.TRUEDIV else "int64_t") - if e.proven: - self.check_proven(f"{_I64_OP[e.op]}({a}, {b}, &{t})") + if e.proven and e.op in _SHIFT_OPS: + # a >= 0 and the divisor is 2**k (verifier): Python's // and % equal >> and & + k = _pow2_shift(e.right) + if e.op is ir.BinOpKind.FLOORDIV: + self.emit(f"{t} = {a} >> {k};") + else: + self.emit(f"{t} = {a} & {_i64_lit((1 << k) - 1)};") + elif e.proven: + self.emit(f"tp_proven({e.op.name.lower()}, {a}, {b}, {t});") else: self.check(f"{_I64_OP[e.op]}({a}, {b}, &{t})") return t @@ -909,7 +924,7 @@ def ev_UnaryOp(self, e: ir.UnaryOp) -> str: if ot is Type.I64 and e.op is ir.UnaryOpKind.NEG: t = self.tmp("int64_t") if e.proven: - self.check_proven(f"tp_neg_i64({v}, &{t})") + self.emit(f"tp_proven_neg({v}, {t});") else: self.check(f"tp_neg_i64({v}, &{t})") return t diff --git a/python-multiplatform-ksp/src/main/python/typedpython/frontend.py b/python-multiplatform-ksp/src/main/python/typedpython/frontend.py index 83e707fd2..8dfbc2099 100644 --- a/python-multiplatform-ksp/src/main/python/typedpython/frontend.py +++ b/python-multiplatform-ksp/src/main/python/typedpython/frontend.py @@ -18,10 +18,15 @@ free of overflow is a CPython int object (OBJ, `PyNumber_*`), a call to a compiled function that may deopt goes through the module global (`CallObject(Global)`), and only `for ... in range()` targets whose every binding is such a loop stay I64. The proof is a small interval analysis: -constants, range targets (between their bounds), `len()` and the i64 range of a guarded parameter. -It is recorded in the IR: an I64 ADD/SUB/MUL/NEG it proves cannot overflow is `proven=True` (the -verifier re-proves it; a proven op does not deopt). Division and modulo of ints cannot be recorded, -so they count as deopting. An impure caller of a pure callee that may deopt and returns F64, BOOL +constants, range targets (between their bounds), `len()` (at most 2**62), the i64 range of a guarded +parameter, the join of what a plain local is assigned (a fixpoint over lowering rounds, widened +when it keeps growing), and the comparisons around a use (`if n > 0:` narrows `n` inside, `while +lo < hi:` narrows both at the top of each iteration, a returning guard narrows the code after it; +a narrowing ends at the next assignment; verify.py "Local variables and guards" is the contract and +the verifier recomputes all of it). It is recorded in the IR: an I64 ADD/SUB/MUL/NEG it proves cannot +overflow is `proven=True` (the verifier re-proves it; a proven op does not deopt), and so is an I64 +`//` or `%` by a Const power of two of a value it proves >= 0 (the back end emits a shift / mask). +Any other division or modulo of ints cannot be recorded, so it counts as deopting. An impure caller of a pure callee that may deopt and returns F64, BOOL or NONE emits `Call(redo=True)`: only the callee is redone on a deopt. Fixed-layout classes (SPEC N-11, `ir.ClassDecl`). A module-level class (in a marked module, or @@ -61,6 +66,8 @@ TOP = (I64_MIN, I64_MAX) EXACT_INT_FLOAT = 2**53 # |n| <= this: int/int true division is exact-rounded in C (ir.BinOp) +LEN_MAX = 2**62 # a native array is never longer (the verifier's Len interval is [0, 2**62]) + Interval = tuple[int, int] | None # None: no value at all (not yet known to be reached) TYPE_NAME = { @@ -608,13 +615,20 @@ def _lower_in_mode(sig, env, info, inferred, impure: bool) -> ir.Function: def _lower_with_bounds(sig, env, info, inferred, impure: bool, candidates: dict[str, Type]) -> ir.Function: # Range-target intervals: least fixpoint by iteration, widened to TOP if it does not settle. + # A local that keeps growing (a counter) is widened to the i64 limit from round 3 on, as the + # verifier's own fixpoint does (verify._prove). bounds: dict[str, Interval] = {} - for _ in range(8): + for rnd in range(16): lowerer = _Lowerer(sig, env, info, inferred, impure, bounds, candidates) fn = lowerer.run() joined = {**bounds} for var, iv in lowerer.found_bounds.items(): - joined[var] = _join(joined.get(var), iv) + new = _join(joined.get(var), iv) + old = joined.get(var) + if rnd >= 3 and var in lowerer.acc_vars and old is not None and new != old: + new = (old[0] if new[0] >= old[0] else I64_MIN, + old[1] if new[1] <= old[1] else I64_MAX) + joined[var] = new if joined == bounds: return fn bounds = joined @@ -664,6 +678,17 @@ def __init__(self, sig: _Signature, env: dict[str, ir.Function], info: _ModuleIn if n not in self.params and any(b.how == "range" for b in bs) and all(b.how in ("range", "annotation") for b in bs) } + # Locals only ever assigned by plain `=` / `+=` statements (never a loop target): their + # interval is the join of what is assigned to them (found_bounds, widened across rounds). + self.acc_vars = { + n for n, bs in self.bindings.items() + if n not in self.params and n not in self.local_arrays + and any(b.how == "assign" for b in bs) + and all(b.how in ("assign", "annotation") for b in bs) + } + # Guard facts at this point (verify.py "Local variables and guards"): local -> interval. + self.refined: dict[str, tuple[int, int]] = {} + self.dead = 0 # >0: in code whose guard read a local with no interval yet in this round self.all_names = {n.id for n in ast.walk(self.fn) if isinstance(n, ast.Name)} \ | set(self.params) @@ -878,13 +903,41 @@ def stmt(self, node: ast.stmt) -> list[ir.Stmt]: if isinstance(node, ast.If): cond = self.condition(node.test) pre = self.take() - return pre + [ir.If(cond, self.block(node.body), self.block(node.orelse))] + entry = self.refined + self.refined, dead = self.narrowed(cond, True, entry) + self.dead += dead + then = self.block(node.body) + self.dead -= dead + then_refined = self.refined + self.refined, dead = self.narrowed(cond, False, entry) + self.dead += dead + orelse = self.block(node.orelse) + self.dead -= dead + else_refined = self.refined + then_ends, else_ends = _diverges(then), _diverges(orelse) + if then_ends and else_ends: + self.refined = entry + elif then_ends: + self.refined = else_refined + elif else_ends: + self.refined = then_refined + else: + self.refined = {k: (min(v[0], else_refined[k][0]), max(v[1], else_refined[k][1])) + for k, v in then_refined.items() if k in else_refined} + return pre + [ir.If(cond, then, orelse)] if isinstance(node, ast.While): if node.orelse: raise Skip(line, "`while ... else` is not supported") + killed = _stored_names(node.body) + head = {k: v for k, v in self.refined.items() if k not in killed} + self.refined = head cond = self.condition(node.test) pre = self.take() + self.refined, dead = self.narrowed(cond, True, head) + self.dead += dead body = self.block(node.body) + self.dead -= dead + self.refined = dict(head) if not pre: return [ir.While(cond, body)] # The condition needs statements (a chain's temporary): run them on every iteration. @@ -906,8 +959,9 @@ def assign(self, target: ast.expr, value_node: ast.expr, node: ast.stmt) -> list raise Skip(line, f"array parameter `{name}` is rebound") value = self.value(value_node) t = self.local_type(name, line) - return self.take() + [ir.Assign(name, self.coerce(value, t, value_node, - f"local `{name}`"))] + value = self.coerce(value, t, value_node, f"local `{name}`") + self.note_assign(name, value) + return self.take() + [ir.Assign(name, value)] if isinstance(target, ast.Subscript): array, elem = self.array_of(target) # CPython evaluates the value first, then the index. @@ -1096,7 +1150,9 @@ def aug_assign(self, node: ast.AugAssign) -> list[ir.Stmt]: t = self.local_type(name, line) current = ir.Local(t, name) result = self.arith(op, current, self.sub(node.value), node) - return self.take() + [ir.Assign(name, self.coerce(result, t, node, f"local `{name}`"))] + result = self.coerce(result, t, node, f"local `{name}`") + self.note_assign(name, result) + return self.take() + [ir.Assign(name, result)] if isinstance(target, ast.Subscript): array, elem = self.array_of(target) index = self.index(target.slice) @@ -1152,14 +1208,18 @@ def for_range(self, node: ast.For) -> list[ir.Stmt]: pre = self.take() s, e = self.interval(start), self.interval(stop) - if s is not None and e is not None: + if s is not None and e is not None and not self.dead: if step > 0: iv = (s[0], max(s[0], e[1] - 1)) else: iv = (min(s[1], e[0] + 1), s[1]) self.found_bounds[var] = _join(self.found_bounds.get(var), iv) + killed = _stored_names(node.body) | {var} + head = {k: v for k, v in self.refined.items() if k not in killed} + self.refined = head body = self.block(node.body) + self.refined = dict(head) return pre + [ir.ForRange(var, start, stop, ir.Const(Type.I64, step), body)] def range_bound(self, node: ast.expr) -> ir.Expr: @@ -1591,18 +1651,75 @@ def coerce(self, value: ir.Expr, target: Type, node: ast.AST, what: str) -> ir.E def interval(self, e: ir.Expr) -> Interval: if isinstance(e, ir.Const) and e.type == Type.I64: return (e.value, e.value) # type: ignore[return-value] - if isinstance(e, ir.Local) and e.type == Type.I64 and e.name in self.range_vars: - return self.bounds.get(e.name) + if isinstance(e, ir.Local) and e.type == Type.I64: + base = (self.bounds.get(e.name) if e.name in self.range_vars or e.name in self.acc_vars + else TOP) + if base is None: + return None + return _meet(base, self.refined.get(e.name)) if isinstance(e, ir.Len): - return (0, I64_MAX) - if isinstance(e, (ir.BinOp, ir.UnaryOp)) and e.type == Type.I64 and self.proved(e): - return self._result_interval(e) + return (0, LEN_MAX) + if isinstance(e, (ir.BinOp, ir.UnaryOp)) and e.type == Type.I64: + if isinstance(e, ir.BinOp) and e.op in (ir.BinOpKind.FLOORDIV, ir.BinOpKind.MOD): + a, b = self.interval(e.left), self.interval(e.right) + if a is None or b is None: + return None + return _clamp(_div_interval(e.op, a, b)) + if isinstance(e, ir.BinOp) and e.op == ir.BinOpKind.TRUEDIV: + return TOP + # ADD/SUB/MUL/NEG/POS: an op that overflows deopts, so only in-range results flow on + r = self._result_interval(e) + return None if r is None else _clamp(r) return TOP - @staticmethod - def recordable(e: ir.BinOp) -> bool: - """`proven` exists for ADD/SUB/MUL only; the verifier cannot re-prove the others.""" - return e.op in (ir.BinOpKind.ADD, ir.BinOpKind.SUB, ir.BinOpKind.MUL) + def note_assign(self, name: str, value: ir.Expr) -> None: + """`name = value` was lowered: record the value's interval for the local (acc_vars) and end + any guard on it.""" + if name in self.acc_vars and not self.dead and value.type == Type.I64: + iv = self.interval(value) + if iv is not None: + self.found_bounds[name] = _join(self.found_bounds.get(name), iv) + self.refined.pop(name, None) + + def narrowed(self, cond: ir.Expr, truth: bool, base: dict[str, tuple[int, int]] + ) -> tuple[dict[str, tuple[int, int]], bool]: + """(`base` narrowed by `cond` being `truth`, whether a bound read a local with no interval + yet). Same rules as verify._Checker.refinements.""" + self.refined = base + found, bottom = {}, False + stack = [(cond, truth)] + while stack: + c, t = stack.pop() + if isinstance(c, ir.UnaryOp) and c.op == ir.UnaryOpKind.NOT: + stack.append((c.operand, not t)) + elif isinstance(c, (ir.And, ir.Or)) and (isinstance(c, ir.And) == t): + stack += [(c.left, t), (c.right, t)] + elif isinstance(c, ir.Compare) and c.left.type == Type.I64 and c.right.type == Type.I64: + kind = c.op if t else _NEGATE[c.op] + for local, other, k in ((c.left, c.right, kind), (c.right, c.left, _SWAP[kind])): + if isinstance(local, ir.Local): + iv = self.interval(other) + if iv is None: + bottom = True + else: + _narrow(found, local.name, _bound(k, iv)) + out = dict(base) + for name, iv in found.items(): + _narrow(out, name, iv) + return out, bottom + + def recordable(self, e: ir.BinOp) -> bool: + """`proven` exists for ADD/SUB/MUL, and for FLOORDIV/MOD by a Const power of two >= 1 of a + value known to be >= 0 (the back end then emits a shift / mask); the verifier re-proves + both and cannot re-prove anything else.""" + if e.op in (ir.BinOpKind.ADD, ir.BinOpKind.SUB, ir.BinOpKind.MUL): + return True + if e.op in (ir.BinOpKind.FLOORDIV, ir.BinOpKind.MOD): + d = e.right.value if isinstance(e.right, ir.Const) else None + a = self.interval(e.left) + return (type(d) is int and d >= 1 and d & (d - 1) == 0 + and a is not None and a[0] >= 0) + return False def proved(self, e: ir.BinOp | ir.UnaryOp) -> bool: """The i64 operation provably does not deopt (no overflow, exact division).""" @@ -1639,17 +1756,81 @@ def _result_interval(self, e: ir.BinOp | ir.UnaryOp) -> Interval: if e.op == ir.BinOpKind.MUL: products = [x * y for x in a for y in b] return (min(products), max(products)) - if e.op == ir.BinOpKind.FLOORDIV: - m = max(abs(a[0]), abs(a[1])) - return (max(-m, I64_MIN), min(m, I64_MAX)) - if e.op == ir.BinOpKind.MOD: - d = max(abs(b[0]), abs(b[1]), 1) - return (-(d - 1), d - 1) return TOP # --- helpers ------------------------------------------------------------------------------------- +_NEGATE = {ir.CompareKind.EQ: ir.CompareKind.NE, ir.CompareKind.NE: ir.CompareKind.EQ, + ir.CompareKind.LT: ir.CompareKind.GE, ir.CompareKind.GE: ir.CompareKind.LT, + ir.CompareKind.LE: ir.CompareKind.GT, ir.CompareKind.GT: ir.CompareKind.LE} +_SWAP = {ir.CompareKind.EQ: ir.CompareKind.EQ, ir.CompareKind.NE: ir.CompareKind.NE, + ir.CompareKind.LT: ir.CompareKind.GT, ir.CompareKind.GT: ir.CompareKind.LT, + ir.CompareKind.LE: ir.CompareKind.GE, ir.CompareKind.GE: ir.CompareKind.LE} + + +def _clamp(iv: tuple[int, int]) -> tuple[int, int]: + return (max(iv[0], I64_MIN), min(iv[1], I64_MAX)) + + +def _meet(a: tuple[int, int], b: tuple[int, int] | None) -> tuple[int, int]: + """`a` narrowed by `b`; an empty meet (unreachable code) leaves `a`, which is still sound.""" + if b is None: + return a + lo, hi = max(a[0], b[0]), min(a[1], b[1]) + return (lo, hi) if lo <= hi else a + + +def _narrow(facts: dict[str, tuple[int, int]], name: str, iv: tuple[int, int] | None) -> None: + if iv is not None: + cur = facts.get(name) + facts[name] = iv if cur is None else _meet(cur, iv) + + +def _bound(kind: ir.CompareKind, other: tuple[int, int]) -> tuple[int, int] | None: + """The interval of `x` when `x e` is true and `e` lies in `other` (verify._bound).""" + lo, hi = other + K = ir.CompareKind + out = {K.LT: (I64_MIN, hi - 1), K.LE: (I64_MIN, hi), K.GT: (lo + 1, I64_MAX), + K.GE: (lo, I64_MAX), K.EQ: (lo, hi)}.get(kind) + return out if out is not None and out[0] <= out[1] else None + + +def _div_interval(op: ir.BinOpKind, a: tuple[int, int], b: tuple[int, int]) -> tuple[int, int]: + """Result interval of I64 FLOORDIV / MOD (verify._div_interval).""" + if op == ir.BinOpKind.MOD: + if b[0] > 0: + return (0, b[1] - 1) + if b[1] < 0: + return (b[0] + 1, 0) + d = max(abs(b[0]), abs(b[1]), 1) + return (-(d - 1), d - 1) + if b[0] > 0 or b[1] < 0: + corners = [x // y for x in a for y in b] + return (min(corners), max(corners)) + m = max(abs(a[0]), abs(a[1])) + return (-m, m) + + +def _stored_names(stmts: Iterable[ast.stmt]) -> set[str]: + """Every name stored (assigned, augmented, loop target) anywhere in `stmts`.""" + return {n.id for st in stmts for n in ast.walk(st) + if isinstance(n, ast.Name) and isinstance(n.ctx, ast.Store)} + + +def _diverges(body: tuple[ir.Stmt, ...]) -> bool: + """Control never reaches the end of `body`: it ends in a return, break or continue, or in an + `if` whose branches both do (verify.py reads these as unreachable states too).""" + if not body: + return False + last = body[-1] + if isinstance(last, (ir.Return, ir.Break, ir.Continue)): + return True + if isinstance(last, ir.If): + return _diverges(last.then) and _diverges(last.orelse) + return False + + def _walk(x): if isinstance(x, (tuple, list)): for y in x: diff --git a/python-multiplatform-ksp/src/main/python/typedpython/ir.py b/python-multiplatform-ksp/src/main/python/typedpython/ir.py index 4660df44f..642eade65 100644 --- a/python-multiplatform-ksp/src/main/python/typedpython/ir.py +++ b/python-multiplatform-ksp/src/main/python/typedpython/ir.py @@ -130,10 +130,15 @@ class BinOp(Expr): op: BinOpKind left: Expr right: Expr - # I64 ADD/SUB/MUL only: set by the front end when an interval proof shows the result cannot - # leave the i64 range; the verifier re-proves it (never trusts it) and a proven op cannot - # deopt, so it is allowed in an impure function. The back end still uses the checked helper - # and treats an overflow there as an internal error (SystemError), never as a deopt. + # I64 only, set by the front end when an interval proof shows the op cannot deopt; the + # verifier re-proves it (never trusts it) and a proven op cannot deopt, so it is allowed in an + # impure function. + # ADD/SUB/MUL: the result cannot leave the i64 range. The back end does plain arithmetic, with + # no check (#148); built with -DTP_CHECK_PROVEN it uses the checked helper and treats an + # overflow as an internal error (SystemError), never as a deopt. + # FLOORDIV/MOD: the divisor is a Const power of two >= 1 and the dividend lies in + # [0, 2**63-1] (Python's floor semantics and C's agree there); the back end emits `>>` / `&`. + # Any other op, or an op the verifier cannot prove, is rejected (verify/proven-overflow). proven: bool = False diff --git a/python-multiplatform-ksp/src/main/python/typedpython/runtime/API.md b/python-multiplatform-ksp/src/main/python/typedpython/runtime/API.md index 37295a6df..8e342894c 100644 --- a/python-multiplatform-ksp/src/main/python/typedpython/runtime/API.md +++ b/python-multiplatform-ksp/src/main/python/typedpython/runtime/API.md @@ -10,6 +10,16 @@ Python error set, nothing to undo), `-1` Python error set (CPython's exception t int tp_sub_i64(int64_t a, int64_t b, int64_t *out); int tp_mul_i64(int64_t a, int64_t b, int64_t *out); int tp_neg_i64(int64_t a, int64_t *out); /* 1 for INT64_MIN */ + /* Proven operations (ir.BinOp.proven, #148): the verifier showed the result fits in i64, so the + generated code calls these (function-like macros; no check, no status). With + -DTP_CHECK_PROVEN they are the checked helpers above and a wrong proof is a SystemError. A + proven // or % by a power of two is emitted inline as `>>` / `&`, not through a helper. */ + tp_proven(add|sub|mul, a, b, t); /* t = a op b, no overflow check */ + tp_proven_neg(a, t); /* t = -a */ + int64_t tp_padd_i64(int64_t a, int64_t b); /* the unchecked forms behind them */ + int64_t tp_psub_i64(int64_t a, int64_t b); + int64_t tp_pmul_i64(int64_t a, int64_t b); + int64_t tp_pneg_i64(int64_t a); int tp_floordiv_i64(int64_t a, int64_t b, int64_t *out); /* -1 ZeroDivisionError; 1 for MIN // -1 */ int tp_mod_i64(int64_t a, int64_t b, int64_t *out); /* -1 ZeroDivisionError; sign of b */ int tp_truediv_i64(int64_t a, int64_t b, double *out); /* -1 ZeroDivisionError; 1 if |a| or |b| > 2**53 */ diff --git a/python-multiplatform-ksp/src/main/python/typedpython/runtime/tp_runtime.h b/python-multiplatform-ksp/src/main/python/typedpython/runtime/tp_runtime.h index b80a36963..14c00bf31 100644 --- a/python-multiplatform-ksp/src/main/python/typedpython/runtime/tp_runtime.h +++ b/python-multiplatform-ksp/src/main/python/typedpython/runtime/tp_runtime.h @@ -218,6 +218,38 @@ static inline int tp_neg_i64(int64_t a, int64_t *out) return 0; } +/* Proven i64 operations (ir.BinOp.proven / UnaryOp.proven): the verifier showed the result fits in + * i64, so the generated code does the arithmetic with no check (unsigned wrap-around, which is plain + * machine arithmetic and has no undefined behaviour). Built with -DTP_CHECK_PROVEN, each of them is + * the checked helper again and a wrong proof is a SystemError, never a deopt: that is for the tests + * and for debugging a verifier change. The macros use the generated function's `tp_s`, `tp_rc` and + * `tp_exit`. */ +static inline int64_t tp_padd_i64(int64_t a, int64_t b) { return (int64_t)((uint64_t)a + (uint64_t)b); } +static inline int64_t tp_psub_i64(int64_t a, int64_t b) { return (int64_t)((uint64_t)a - (uint64_t)b); } +static inline int64_t tp_pmul_i64(int64_t a, int64_t b) { return (int64_t)((uint64_t)a * (uint64_t)b); } +static inline int64_t tp_pneg_i64(int64_t a) { return (int64_t)(0 - (uint64_t)a); } +#ifdef TP_CHECK_PROVEN +#define tp_proven_fail() \ + do { \ + PyErr_SetString(PyExc_SystemError, "typedpython: proven operation overflowed"); \ + tp_rc = -1; \ + goto tp_exit; \ + } while (0) +#define tp_proven(op, a, b, t) \ + do { \ + tp_s = tp_##op##_i64((a), (b), &(t)); \ + if (tp_s != 0) tp_proven_fail(); \ + } while (0) +#define tp_proven_neg(a, t) \ + do { \ + tp_s = tp_neg_i64((a), &(t)); \ + if (tp_s != 0) tp_proven_fail(); \ + } while (0) +#else +#define tp_proven(op, a, b, t) ((t) = tp_p##op##_i64((a), (b))) +#define tp_proven_neg(a, t) ((t) = tp_pneg_i64(a)) +#endif + /* Python floor division: the quotient rounds toward negative infinity. */ static inline int tp_floordiv_i64(int64_t a, int64_t b, int64_t *out) { diff --git a/python-multiplatform-ksp/src/main/python/typedpython/verify.py b/python-multiplatform-ksp/src/main/python/typedpython/verify.py index b42711114..9854a0f42 100644 --- a/python-multiplatform-ksp/src/main/python/typedpython/verify.py +++ b/python-multiplatform-ksp/src/main/python/typedpython/verify.py @@ -94,9 +94,11 @@ Proven i64 operations. The verifier never trusts `BinOp.proven` / `UnaryOp.proven`: for every I64 expression it computes an interval [lo, hi] (exact Python ints) and accepts `proven=True` only on an -I64 ADD/SUB/MUL (BinOp) or NEG (UnaryOp) whose exact result interval lies inside [-2**63, 2**63-1]; -anything else (a different op, a non-I64 node, a result that may leave i64, a non-bool flag) is -rejected, and so is the whole function. A proven op is not a deopting node (an impure function may +I64 ADD/SUB/MUL (BinOp) or NEG (UnaryOp) whose exact result interval lies inside [-2**63, 2**63-1], +or on an I64 FLOORDIV/MOD whose divisor is a Const power of two >= 1 and whose dividend interval lies +inside [0, 2**63-1] (the back end then emits a shift / mask, #148); +anything else (a different op, a non-I64 node, a result that may leave i64, a dividend that may be +negative, another divisor, a non-bool flag) is rejected, and so is the whole function. A proven op is not a deopting node (an impure function may contain it; a pure one does not count it toward `may_deopt`); every unproven I64 ADD/SUB/MUL/NEG still deopts. The interval rules, exactly: @@ -106,17 +108,45 @@ step < 0 [min(hi(start), lo(stop) + 1), hi(start)] (the bounds are the intervals of the start/stop expressions, both evaluated before the loop; then intersected with the i64 range) + Local, any other I64 local see "Local variables and guards" below Len(array) [0, 2**62] ADD / SUB / MUL interval arithmetic on the operand intervals (for MUL the min/max of the four endpoint products); a proven op must fit i64 exactly, an unproven one is clamped to i64 (a result outside it deopts, so only in-range values flow on) NEG / POS [-hi, -lo] / [lo, hi] - everything else the full i64 range: I64 params and entry globals, every local that is - not the ForRange var of an enclosing loop (the verifier does no flow - analysis, so a local assigned a constant is still "any i64"), a loop - var after its loop, Index elements, Unbox, Call results, FLOORDIV, - MOD, TRUEDIV + MOD divisor interval > 0: [0, hi(b) - 1]; < 0: [lo(b) + 1, 0]; else + [-(d - 1), d - 1] with d = max |b| + FLOORDIV divisor interval that keeps its sign: the min/max of the four + corner quotients; else [-m, m] with m = max |a| (all clamped to i64: + -2**63 // -1 deopts, so it yields no value) + everything else the full i64 range: I64 params and entry globals, a loop var after + its loop, Index elements, Unbox, Call results, TRUEDIV + +Local variables and guards (#148). Two flow facts narrow what a read of an I64 local can be; both +are computed here, never taken from the front end. + + * Assigned values. A local that is not a parameter, entry global, array or ForRange var of the + function, and is assigned by Assign statements, has the join of the intervals of every value + assigned to it (an unproven op counts clamped to i64, as above). The intervals are a fixed point: + `_prove` walks the body again and again, each walk reading the intervals the previous one found, + until no interval grows; from the fourth walk a bound that still grows jumps to the i64 limit, + and after 16 walks every such local is full range. The fixed point means each assigned value + lies inside its local's interval, whichever path ran. An assignment that reads a local with no + interval yet (the first walks) adds nothing that walk. So `x = 1; x + 1` is proven, and a counter + that starts at 0 and only grows (`k = 0 ... k = k + 1`) is in [0, 2**63-1], not "any i64". + * Guards. Inside the then-branch of `If(c)` (the else-branch for `c` false), the body of + `While(c)`, and after an `If` one branch of which cannot complete (return, break, continue), a + Local that is a side of an I64 comparison with the other side's interval [lo, hi] is narrowed: + `x < e` gives x <= hi - 1, `x <= e` x <= hi, `x > e` x >= lo + 1, `x >= e` x >= lo, `x == e` + [lo, hi]; the Local may be either side; And (true) and Or (false) apply both links, Not flips, + the negation of a comparison is the opposite comparison, `!=` and anything else give nothing. + A guard on `x` ends at the next Assign to `x`; entering a loop drops the guards on every local + the loop body assigns (the back edge brings other values); a While's condition is re-read at + each iteration, so it narrows the top of every iteration. A read is the assigned-values interval + narrowed by the guard (and a ForRange var's interval is narrowed by it too). + So `if n > 0: return n - 1` and `while lo < hi: lo += 1; hi -= 1` need no check, `n <= 0` early + return then `n - 1` likewise. Local arrays (NewArray / CopyArray, ir.Function "Local arrays"). A local of an array type holds a native array the function owns. The verifier proves, never trusting the front end: @@ -146,12 +176,12 @@ Tuple. `Tuple(OBJ, elements)`: a tuple of OBJ expressions (a scalar needs Box), result OBJ, a reference creator in the ownership rule. Building one is not an effect. -What this cannot prove: anything that needs knowing a value through assignments (accumulators, -`x = 1; x + 1`), relations between variables (`i < n` does not bound `i + n`), bounds that come from -guards or conditions (`if n < 100`), values through array elements, calls or Unbox, the result of -`//` and `%` (even by a constant), a loop var after the loop, or `range` bounds that are themselves -full-range (`range(n)` bounds the var only by i64). A function needing such a proof keeps its -checked, deopting ops (and is then legal only if pure). +What this cannot prove: relations between variables (`i < n` bounds `i`, not `i + n`, and says +nothing about `j` when `j` is not compared), the range of a counter that is bounded only by how +often a loop runs (`k += 1` in `while c`), values through array elements, calls or Unbox, a loop var +after the loop, a guard on a local the guarded code assigns before the use, or `range` bounds that +are themselves full-range (`range(n)` bounds the var only by i64). A function needing such a proof +keeps its checked, deopting ops (and is then legal only if pure). Call.redo. Legal only if the caller is impure, the callee is pure and may_deopt, and the callee returns F64, BOOL or NONE (`verify/redo` otherwise). A redo call is not a deopting node in the @@ -235,6 +265,15 @@ class Diagnostic: _FULL = (_I64_MIN, _I64_MAX) _LEN_MAX = 2 ** 62 _PROVABLE_OPS = frozenset({BinOpKind.ADD, BinOpKind.SUB, BinOpKind.MUL}) +_POW2_OPS = frozenset({BinOpKind.FLOORDIV, BinOpKind.MOD}) # `proven` means shift / mask +_NEGATE = {CompareKind.EQ: CompareKind.NE, CompareKind.NE: CompareKind.EQ, + CompareKind.LT: CompareKind.GE, CompareKind.GE: CompareKind.LT, + CompareKind.LE: CompareKind.GT, CompareKind.GT: CompareKind.LE} +_SWAP = {CompareKind.EQ: CompareKind.EQ, CompareKind.NE: CompareKind.NE, + CompareKind.LT: CompareKind.GT, CompareKind.GT: CompareKind.LT, + CompareKind.LE: CompareKind.GE, CompareKind.GE: CompareKind.LE} +_ROUNDS = 16 # rounds of the local-interval fixpoint before every local is full range +_WIDEN_FROM = 3 # from this round on a bound that still grows jumps to the i64 limit # Definite assignment uses `None` for "unreachable" (bottom: every name counts as assigned). _State = frozenset[str] | None @@ -253,6 +292,7 @@ def __init__(self, var: str | None, bounds_array: str | None): self.var = var # ForRange var (None for While) self.bounds_array = bounds_array # array whose indices by `var` are in bounds self.interval = _FULL # the values `var` takes inside the body + self.bottom = False # fixpoint round: start/stop not known yet self.breaks: list[_State] = [] @@ -261,8 +301,19 @@ class _Checker: body with proven bounds.""" def __init__(self, function: Function, signatures: dict[str, Function], - classes: dict[str, ClassDecl] | None = None): + classes: dict[str, ClassDecl] | None = None, + var_ivs: dict[str, tuple[int, int]] | None = None, fixing: bool = False): self.fn = function + # Local intervals (module docstring "Local variables and guards"): `var_ivs` is the interval + # of every eligible local; `fixing` says this walk is a round of the fixpoint that computes + # them (a local without an interval yet is then "bottom": `bottom` is set when one is read). + self.var_ivs = dict(var_ivs or {}) + self.fixing = fixing + self.eligible: frozenset[str] = frozenset() + self.contrib: dict[str, tuple[int, int]] = {} + self.bottom = False + self.dead = 0 # >0: inside code that is bottom in this round + self.refine: dict[str, tuple[int, int]] = {} # guard facts at this point self.sigs = signatures self.classes = classes or {} self.facts: dict[str, str] = {} # local -> class it is proved exactly (see docstring) @@ -551,19 +602,68 @@ def interval(self, e: ir.Expr) -> tuple[int, int]: if cls is Local: for loop in reversed(self.loops): if loop.var == e.name: - return loop.interval - return _FULL + if loop.bottom: + self.bottom = True + return _meet_interval(loop.interval, self.refine.get(e.name)) + base = _FULL + if e.name in self.eligible: + known = self.var_ivs.get(e.name) + if known is not None: + base = known + elif self.fixing: + self.bottom = True + return _meet_interval(base, self.refine.get(e.name)) if cls is Len: return self.lens.get(e.array, (0, _LEN_MAX)) if cls is BinOp and e.op in _PROVABLE_OPS: lo, hi = _exact(e.op, self.interval(e.left), self.interval(e.right)) return (max(lo, _I64_MIN), min(hi, _I64_MAX)) + if cls is BinOp and e.op in _POW2_OPS: + lo, hi = _div_interval(e.op, self.interval(e.left), self.interval(e.right)) + return (max(lo, _I64_MIN), min(hi, _I64_MAX)) if cls is UnaryOp and e.op in (UnaryOpKind.NEG, UnaryOpKind.POS): lo, hi = self.interval(e.operand) lo, hi = (-hi, -lo) if e.op is UnaryOpKind.NEG else (lo, hi) return (max(lo, _I64_MIN), min(hi, _I64_MAX)) return _FULL + def refinements(self, c: ir.Expr, truth: bool) -> dict[str, tuple[int, int]]: + """The intervals that hold of locals when condition `c` evaluated to `truth` (module + docstring "Local variables and guards"). A comparison of two I64 operands one of which is a + `Local` bounds that local by the interval of the other; And (true) / Or (false) combine + both links; Not flips; anything else gives nothing.""" + cls = type(c) + if cls is Compare and type(c.op) is CompareKind: + l, r = c.left, c.right + if getattr(l, "type", None) is not Type.I64 or getattr(r, "type", None) is not Type.I64: + return {} + kind = c.op if truth else _NEGATE[c.op] + out: dict[str, tuple[int, int]] = {} + if type(l) is Local: + _narrow(out, l.name, _bound(kind, self.interval(r))) + if type(r) is Local: + _narrow(out, r.name, _bound(_SWAP[kind], self.interval(l))) + return out + if cls is UnaryOp and c.op is UnaryOpKind.NOT: + return self.refinements(c.operand, not truth) + if (cls is And and truth) or (cls is Or and not truth): + out = self.refinements(c.left, truth) + for name, iv in self.refinements(c.right, truth).items(): + _narrow(out, name, iv) + return out + return {} + + def narrowed(self, c: ir.Expr, truth: bool) -> tuple[dict[str, tuple[int, int]], bool]: + """(the current guard facts narrowed by `c` being `truth`, whether the narrowing read a local + whose interval is not known yet in this fixpoint round).""" + self.bottom = False + found = self.refinements(c, truth) + bottom, self.bottom = self.bottom, False + out = dict(self.refine) + for name, iv in found.items(): + _narrow(out, name, iv) + return out, bottom + def check_proven(self, shape_ok: bool, interval: tuple[int, int], what: str) -> bool: """`proven=True` (already known to be a bool) is accepted only if re-proved. Returns whether the node counts as non-deopting.""" @@ -576,6 +676,21 @@ def check_proven(self, shape_ok: bool, interval: tuple[int, int], what: str) -> return True return False + def check_shift(self, op: BinOpKind, left: ir.Expr, right: ir.Expr) -> bool: + """`proven` on an I64 FLOORDIV / MOD: the divisor is a Const power of two >= 1 and the + dividend lies in [0, 2**63-1], so the back end may emit a shift / mask (Python's floor + semantics and C's agree there). Returns whether the node counts as non-deopting.""" + d = right.value if type(right) is Const and type(right.value) is int else None + if d is None or d < 1 or d & (d - 1) != 0: + self.error(PROVEN, f"`proven` is set on i64 {op.value} but the divisor is not a " + f"Const power of two >= 1") + elif self.interval(left)[0] < 0: + self.error(PROVEN, f"`proven` is set on i64 {op.value} by {d} but the dividend may be " + f"negative (its interval starts at {self.interval(left)[0]})") + else: + return True + return False + def e_BinOp(self, e: BinOp, state: _State) -> ir.Expr: if type(e.op) is not BinOpKind: self.error(UNKNOWN, f"BinOp op {e.op!r} is not a BinOpKind") @@ -586,10 +701,14 @@ def e_BinOp(self, e: BinOp, state: _State) -> ir.Expr: if type(e.proven) is not bool: self.error(TYPE, f"BinOp `proven` {e.proven!r} is not a bool") elif e.proven: - shape = (e.type is Type.I64 and lt is Type.I64 and rt is Type.I64 - and e.op in _PROVABLE_OPS) - exact = _exact(e.op, self.interval(left), self.interval(right)) if shape else _FULL - proven = self.check_proven(shape, exact, f"{e.type.value} {e.op.value}") + both = e.type is Type.I64 and lt is Type.I64 and rt is Type.I64 + if both and e.op in _POW2_OPS: + proven = self.check_shift(e.op, left, right) + else: + shape = both and e.op in _PROVABLE_OPS + exact = (_exact(e.op, self.interval(left), self.interval(right)) + if shape else _FULL) + proven = self.check_proven(shape, exact, f"{e.type.value} {e.op.value}") if lt not in (Type.I64, Type.F64, Type.OBJ): self.error(TYPE if lt is not Type.OBJ else OWNERSHIP, f"BinOp {e.op.value} on {getattr(lt, 'value', lt)} operands") @@ -1067,6 +1186,14 @@ def s_Assign(self, s: Assign, state: _State): self.error(TYPE, f"None assigned to '{target}'") if target in self.entry: self.error(STRUCTURE, f"entry global '{target}' is assigned in the body") + if (target in self.eligible and not alloc and not self.dead + and getattr(value, "type", None) is Type.I64): + self.bottom = False + iv = self.interval(value) + if not self.bottom: + self.contrib[target] = _join_interval(self.contrib.get(target), iv) + self.bottom = False + self.refine.pop(target, None) # a guard on `target` ends at its assignment proved = None if alloc else self.exact_of(value) if proved is not None: self.facts[target] = proved @@ -1108,12 +1235,29 @@ def s_FieldSet(self, s: FieldSet, state: _State): def s_If(self, s: If, state: _State): cond = self.cond(s.cond, state, "if") base = self.facts + entry = self.refine self.facts = {**base, **self.facts_if(cond, True)} + self.refine, dead = self.narrowed(cond, True) + self.dead += dead then, st = self.block(s.then, state) - then_facts = self.facts + self.dead -= dead + then_facts, then_refine = self.facts, self.refine self.facts = {**base, **self.facts_if(cond, False)} + self.refine = entry + self.refine, dead = self.narrowed(cond, False) + self.dead += dead orelse, se = self.block(s.orelse, state) - else_facts = self.facts + self.dead -= dead + else_facts, else_refine = self.facts, self.refine + if st is None and se is None: + self.refine = entry + elif st is None: + self.refine = else_refine + elif se is None: + self.refine = then_refine + else: + self.refine = {k: (min(v[0], else_refine[k][0]), max(v[1], else_refine[k][1])) + for k, v in then_refine.items() if k in else_refine} if st is None and se is None: self.facts = base elif st is None: @@ -1133,14 +1277,21 @@ def loop_facts(self, body: object, extra: tuple[str, ...] = ()) -> dict[str, str def s_While(self, s: While, state: _State): head = self.loop_facts(s.body) self.facts = head + killed = _assigned_names(s.body) + head_refine = {k: v for k, v in self.refine.items() if k not in killed} + self.refine = head_refine cond = self.cond(s.cond, state, "while") loop = _Loop(None, None) self.facts = {**head, **self.facts_if(cond, True)} + self.refine, dead = self.narrowed(cond, True) + self.dead += dead self.loops.append(loop) # Assignments only add names, so the loop-head state is the entry state (the meet of the # entry, end-of-body and continue states equals the entry state). body, _ = self.block(s.body, state) self.loops.pop() + self.dead -= dead + self.refine = dict(head_refine) self.facts = dict(head) # leaving by the condition or a break: no more than the head's facts forever = type(s.cond) is Const and s.cond.type is Type.BOOL and s.cond.value is True after: _State = None if forever else state @@ -1179,7 +1330,9 @@ def s_ForRange(self, s: ForRange, state: _State): loop = _Loop(var, bounds) if (step_ok and getattr(start, "type", None) is Type.I64 and getattr(stop, "type", None) is Type.I64): + self.bottom = False (slo, shi), (elo, ehi) = self.interval(start), self.interval(stop) + loop.bottom, self.bottom = self.bottom, False if step.value > 0: lo = slo hi = max(lo, ehi - 1) @@ -1190,8 +1343,12 @@ def s_ForRange(self, s: ForRange, state: _State): self.loops.append(loop) head = self.loop_facts(s.body, (var,)) self.facts = dict(head) + killed = _assigned_names(s.body) | {var} + head_refine = {k: v for k, v in self.refine.items() if k not in killed} + self.refine = head_refine body, _ = self.block(s.body, None if state is None else state | {var}) self.loops.pop() + self.refine = dict(head_refine) self.facts = dict(head) # Zero iterations leave `var` (and everything the body assigns) as it was: the state after # the loop is the entry state, met with every break state (each a superset of it). @@ -1228,6 +1385,13 @@ def run(self) -> Function: fn = self.fn params = self.declarations() self.reassigned = frozenset(_assigned_names(fn.body)) + assigned: dict[str, list[object]] = {} + _assigned_values(fn.body, assigned) + loop_vars = _loop_vars(fn.body) + self.eligible = frozenset( + n for n in assigned + if self.scalars.get(n) is Type.I64 and n not in params and n not in loop_vars + and n not in self.arrays and n not in self.larrays) self.new_only = self.new_only_locals(params) if self.larrays: counts: dict[str, int] = {} @@ -1321,6 +1485,62 @@ def _assigned_names(body: object) -> set[str]: return out +def _meet_interval(a: tuple[int, int], b: tuple[int, int] | None) -> tuple[int, int]: + """`a` narrowed by `b`; an empty meet (unreachable code) leaves `a`, which is still sound.""" + if b is None: + return a + lo, hi = max(a[0], b[0]), min(a[1], b[1]) + return (lo, hi) if lo <= hi else a + + +def _narrow(facts: dict[str, tuple[int, int]], name: str, iv: tuple[int, int] | None) -> None: + if iv is None: + return + cur = facts.get(name) + facts[name] = iv if cur is None else _meet_interval(cur, iv) + + +def _bound(kind: CompareKind, other: tuple[int, int]) -> tuple[int, int] | None: + """The interval of `x` when `x e` is true and `e` lies in `other`.""" + lo, hi = other + if kind is CompareKind.LT: + out = (_I64_MIN, hi - 1) + elif kind is CompareKind.LE: + out = (_I64_MIN, hi) + elif kind is CompareKind.GT: + out = (lo + 1, _I64_MAX) + elif kind is CompareKind.GE: + out = (lo, _I64_MAX) + elif kind is CompareKind.EQ: + out = (lo, hi) + else: + return None + return out if out[0] <= out[1] else None + + +def _div_interval(op: BinOpKind, a: tuple[int, int], b: tuple[int, int]) -> tuple[int, int]: + """The result interval of I64 FLOORDIV / MOD (an operation that completes: a zero divisor + raises and -2**63 // -1 deopts, so neither yields a value). MOD: [0, hi(b) - 1] for a positive + divisor, [lo(b) + 1, 0] for a negative one, else |result| < max |b|. FLOORDIV: for a divisor + that keeps its sign the extremes are at the corners; else |result| <= max |a|.""" + if op is BinOpKind.MOD: + if b[0] > 0: + return (0, b[1] - 1) + if b[1] < 0: + return (b[0] + 1, 0) + d = max(abs(b[0]), abs(b[1]), 1) + return (-(d - 1), d - 1) + if b[0] > 0 or b[1] < 0: + corners = [x // y for x in a for y in b] + return (min(corners), max(corners)) + m = max(abs(a[0]), abs(a[1])) + return (-m, m) + + +def _join_interval(a: tuple[int, int] | None, b: tuple[int, int]) -> tuple[int, int]: + return b if a is None else (min(a[0], b[0]), max(a[1], b[1])) + + def _exact(op: BinOpKind, a: tuple[int, int], b: tuple[int, int]) -> tuple[int, int]: """The exact (unbounded) result interval of ADD/SUB/MUL on operand intervals.""" if op is BinOpKind.ADD: @@ -1331,6 +1551,42 @@ def _exact(op: BinOpKind, a: tuple[int, int], b: tuple[int, int]) -> tuple[int, return min(products), max(products) +def _prove(g: Function, sigs: dict[str, Function], classes: dict[str, ClassDecl] + ) -> tuple[_Checker, Function]: + """Check `g`, first computing the interval of every eligible local (Local variables and + guards): walks of the body repeat, each reading the intervals found by the one before, until + they stop growing (a bound still growing from round `_WIDEN_FROM` jumps to the i64 limit). The + result is a fixed point, so every assigned value lies inside its local's interval. If it does + not settle in `_ROUNDS` walks, every eligible local is full range.""" + known: dict[str, tuple[int, int]] = {} + for rnd in range(_ROUNDS): + c = _Checker(g, sigs, classes, known, True) + rebuilt = c.run() + if not c.eligible: + return c, rebuilt + grown = dict(known) + for name in c.eligible: + iv = c.contrib.get(name) + if iv is None: + continue + old = known.get(name) + if old is None: + grown[name] = iv + continue + lo = old[0] if iv[0] >= old[0] else (_I64_MIN if rnd >= _WIDEN_FROM else iv[0]) + hi = old[1] if iv[1] <= old[1] else (_I64_MAX if rnd >= _WIDEN_FROM else iv[1]) + grown[name] = (lo, hi) + if grown == known: + absent = c.eligible - set(known) + if not absent: + return c, rebuilt + for name in absent: # never given an interval: nothing is known about it + grown[name] = _FULL + known = grown + c = _Checker(g, sigs, classes, {}, False) + return c, c.run() + + def verify(module: Module) -> tuple[Module, list[Diagnostic]]: """Prove each function of `module`; return the module of proved functions (with proven bounds marked) and every diagnostic. Rejected functions move to `skipped` with the reason.""" @@ -1364,8 +1620,7 @@ def reject(fn_name: str, line: int, rule: str, message: str) -> None: open_why: dict[str, str] = {} # a function that runs user code -> why slow_why: dict[str, str] = {} # a function whose slow paths can run user code -> why for name, g in sigs.items(): - c = _Checker(g, sigs, classes) - rebuilt = c.run() + c, rebuilt = _prove(g, sigs, classes) for d in c.diags: reject(d.function, d.source_line, d.rule, d.message) checked[name] = rebuilt diff --git a/python-multiplatform-ksp/src/test/python/test_cgen.py b/python-multiplatform-ksp/src/test/python/test_cgen.py index 8fd8c3704..d7afecef8 100644 --- a/python-multiplatform-ksp/src/test/python/test_cgen.py +++ b/python-multiplatform-ksp/src/test/python/test_cgen.py @@ -936,14 +936,16 @@ def test_gen_accepts_proven_ops_in_an_impure_function(): proven=True))], pure=False, may_deopt=False) text = cgen.generate(Module("tp_proven_gen", (ok,)), source_file("tp_proven_gen")) - assert "typedpython: proven operation overflowed" in text + # #148: a proven op is plain arithmetic (TP_PROVEN*, tp_runtime.h), not the checked helper + assert "tp_proven(sub," in text and "tp_proven_neg(" in text + assert "tp_sub_i64(" not in text and "tp_neg_i64(" not in text def test_gen_rejects_proven_on_an_op_that_is_not_checked_i64_arithmetic(): from typedpython import cgen bad = fn("badproven", [Param("a", I64)], I64, {}, - [Return(BinOp(I64, BinOpKind.FLOORDIV, L("a", I64), c(2), proven=True))], + [Return(BinOp(I64, BinOpKind.FLOORDIV, L("a", I64), c(3), proven=True))], # 3: no shift pure=True, may_deopt=True) with pytest.raises(cgen.CGenError, match="proven"): cgen.generate(Module("tp_bad4", (bad,)), source_file("tp_bad4")) @@ -975,9 +977,24 @@ def test_proven_op_in_an_impure_function_computes_the_interpreted_result(mod): before = deopts(mod) assert mod.proven_eff(5) == interp(mod, "proven_eff")(5) == 6 assert mod.calls == [5, 5] and deopts(mod) == before + + +@pytest.fixture(scope="module") +def checked_mod(): + from typedpython import cbuild + return build_module("tp_cgen_proven_checked", (f_proven_eff,), + flags=list(cbuild.DEFAULT_FLAGS) + ["-DTP_CHECK_PROVEN"]) + + +def test_proven_op_with_a_wrong_proof_is_an_internal_error_when_proofs_are_checked(checked_mod): + # #148: a proven op is unchecked by default; -DTP_CHECK_PROVEN checks every one again. A proof + # the IR producer got wrong is then an internal error, never a deopt (the effect has happened + # already, so a redo would run it twice). + mod = checked_mod + mod.calls.clear() + before = deopts(mod) + assert mod.proven_eff(5) == 6 mod.calls.clear() - # A proof the IR producer got wrong: the overflow is an internal error, never a deopt (the - # effect has happened already, so a redo would run it twice). with pytest.raises(SystemError, match="typedpython: proven operation overflowed"): mod.proven_eff(2 ** 63 - 1) assert mod.calls == [2 ** 63 - 1] and deopts(mod) == before diff --git a/python-multiplatform-ksp/src/test/python/test_frontend.py b/python-multiplatform-ksp/src/test/python/test_frontend.py index dc06deaec..03217ece2 100644 --- a/python-multiplatform-ksp/src/test/python/test_frontend.py +++ b/python-multiplatform-ksp/src/test/python/test_frontend.py @@ -185,10 +185,11 @@ def f(x: float) -> float: assert not any(n.proven for n in nodes(f, BinOp) + nodes(f, UnaryOp)) -@pytest.mark.parametrize("expr", ["i // 2", "i / 2"]) +@pytest.mark.parametrize("expr", ["i // 3", "i / 2"]) def test_int_division_cannot_be_recorded_as_proven_so_it_deopts(tmp_path, expr): - # ir.BinOp.proven exists for ADD/SUB/MUL only; the verifier cannot re-prove // and / on i64, - # so they count as deopting: in a pure function may_deopt, in an impure one a CPython int. + # ir.BinOp.proven exists for ADD/SUB/MUL and for // and % by a power of two of a value >= 0 + # (#148, test_interval_proofs.py); the verifier cannot re-prove // by 3 or / on i64, so they + # count as deopting: in a pure function may_deopt, in an impure one a CPython int. m = lower(tmp_path, f""" @compiled def f(n: int) -> float: diff --git a/python-multiplatform-ksp/src/test/python/test_frontend_classes.py b/python-multiplatform-ksp/src/test/python/test_frontend_classes.py index 4def4ed49..33c0473cc 100644 --- a/python-multiplatform-ksp/src/test/python/test_frontend_classes.py +++ b/python-multiplatform-ksp/src/test/python/test_frontend_classes.py @@ -587,10 +587,11 @@ def test_binary_trees_with_slots_lowers_make_and_check(tmp_path): FieldGet(OBJ, Local(OBJ, "node"), "Node", "right")] assert nodes(check, Is) assert nodes(check, CallObject) == [] and nodes(check, GetAttr) == [] - # report: make() and check() both may deopt (i64 arithmetic, and `check(left)` passes an - # `Node | None` local to a parameter guarded `type(x) is Node`) + # report: check() may deopt (i64 arithmetic, and `check(left)` passes an `Node | None` local to + # a parameter guarded `type(x) is Node`); make() no longer does (#148: `depth - 1` sits under + # `if depth > 0`, so it cannot overflow) print(f"make.may_deopt={make.may_deopt} check.may_deopt={check.may_deopt}") - assert make.may_deopt and check.may_deopt + assert check.may_deopt and not make.may_deopt def test_binary_trees_without_slots_stays_object_code(tmp_path): diff --git a/python-multiplatform-ksp/src/test/python/test_interval_proofs.py b/python-multiplatform-ksp/src/test/python/test_interval_proofs.py new file mode 100644 index 000000000..045a593e3 --- /dev/null +++ b/python-multiplatform-ksp/src/test/python/test_interval_proofs.py @@ -0,0 +1,586 @@ +"""Interval proofs that drop provably safe checked i64 operations (issue #148, SPEC N-8 / N-9). + +New facts, all re-proved by the verifier (the front end only proposes `proven`): + + * guards: inside `if x < e:` / `while lo < hi:` (and after a guard that returns) a local's + interval is narrowed by the comparison, until the local is assigned; + * locals: a local assigned only i64 values has the join of their intervals (a flow-insensitive + fixpoint with widening), so `x = 1; x + 1` and non-negative accumulators are known; + * `//` and `%` by a constant have bounded results; + * `//` and `%` by a positive power-of-two Const of a value in [0, 2**63-1] carry `proven` and + are emitted as a shift / mask (no tp_floordiv_i64 / tp_mod_i64); + * the front end's `len()` bound is 2**62, as the verifier's. + +Section 1 builds IR by hand (no front end): each fact is accepted when sound and rejected with the +PROVEN rule when the IR claims it without the fact. Section 2 runs source through the front end, +verifier, C back end and the C compiler, and compares the compiled function with CPython at the +boundary values. Builds go to pytest's basetemp inside the worktree's `.tmp/`. +""" +from __future__ import annotations + +import dataclasses +import importlib.machinery +import importlib.util +import re +from pathlib import Path + +import pytest + +from typedpython import cbuild, cgen, frontend, verify +from typedpython.ir import ( + And, ArrayParam, Assign, BinOp, BinOpKind, Compare, CompareKind, Const, ForRange, If, Index, + Local, Or, Param, Return, Type, UnaryOp, UnaryOpKind, While, +) +from test_verify import ( + IMPURE, PROVEN, FLAG_DEOPT, assert_accepted, assert_rejected, fn, i, kept, lb, li, padd, pmul, + psub, run, +) + +I64, BOOL = Type.I64, Type.BOOL +MAX, MIN = 2 ** 63 - 1, -2 ** 63 +A = [ArrayParam("a", Type.I64_ARRAY, stored=False)] +N = [Param("n", I64)] + + +def cmp(kind, l, r): return Compare(BOOL, kind, l, r) +def lt(l, r): return cmp(CompareKind.LT, l, r) +def le(l, r): return cmp(CompareKind.LE, l, r) +def gt(l, r): return cmp(CompareKind.GT, l, r) +def ge(l, r): return cmp(CompareKind.GE, l, r) +def eq(l, r): return cmp(CompareKind.EQ, l, r) +def pdiv(l, r): return BinOp(I64, BinOpKind.FLOORDIV, l, r, proven=True) +def pmod(l, r): return BinOp(I64, BinOpKind.MOD, l, r, proven=True) +def div(l, r): return BinOp(I64, BinOpKind.FLOORDIV, l, r) +def mod(l, r): return BinOp(I64, BinOpKind.MOD, l, r) +def elem(k=0): return Index(I64, "a", i(k)) + + +def pure_fn(body, params=N, locals_=None, may_deopt=False, **kw): + return fn(params=params, locals_=locals_, returns=I64, pure=True, may_deopt=may_deopt, + body=body, **kw) + + +# --- 1a. guards ---------------------------------------------------------------------------------- + +def test_a_less_than_guard_bounds_the_local_from_above(): + ok = pure_fn([If(lt(li("n"), i(MAX)), (Return(padd(li("n"), i(1))),)), Return(i(0))]) + assert_accepted(ok) + # `<=` leaves n == MAX possible + assert_rejected(PROVEN, pure_fn([If(le(li("n"), i(MAX)), (Return(padd(li("n"), i(1))),)), + Return(i(0))])) + # no guard at all + assert_rejected(PROVEN, pure_fn([Return(padd(li("n"), i(1)))])) + + +def test_a_greater_than_guard_bounds_the_local_from_below(): + assert_accepted(pure_fn([If(gt(li("n"), i(MIN)), (Return(psub(li("n"), i(1))),)), Return(i(0))])) + assert_rejected(PROVEN, pure_fn([If(ge(li("n"), i(MIN)), + (Return(psub(li("n"), i(1))),)), Return(i(0))])) + + +def test_the_local_may_be_on_the_right_of_the_comparison(): + assert_accepted(pure_fn([If(gt(i(MAX), li("n")), (Return(padd(li("n"), i(1))),)), + Return(i(0))])) + + +def test_the_other_side_may_be_any_expression_with_a_known_interval(): + # n < m, and m <= 2**63 - 1: n <= 2**63 - 2 + ps = [Param("n", I64), Param("m", I64)] + assert_accepted(pure_fn([If(lt(li("n"), li("m")), (Return(padd(li("n"), i(1))),)), + Return(i(0))], params=ps)) + # but n <= m only gives n <= 2**63 - 1 + assert_rejected(PROVEN, pure_fn([If(le(li("n"), li("m")), (Return(padd(li("n"), i(1))),)), + Return(i(0))], params=ps)) + + +def test_a_conjunction_applies_every_link_and_a_disjunction_none(): + both = And(BOOL, lt(li("n"), i(MAX)), gt(li("n"), i(MIN))) + assert_accepted(pure_fn([If(both, (Return(padd(psub(li("n"), i(1)), i(1))),)), Return(i(0))])) + either = Or(BOOL, lt(li("n"), i(MAX)), lt(li("n"), i(5))) + assert_rejected(PROVEN, pure_fn([If(either, (Return(padd(li("n"), i(1))),)), Return(i(0))])) + # the else branch of a disjunction has both links false + neither = Or(BOOL, ge(li("n"), i(MAX)), lt(li("n"), i(MIN + 1))) + assert_accepted(pure_fn([If(neither, (Return(i(0)),), (Return(padd(li("n"), i(1))),))])) + + +def test_not_and_the_else_branch_negate_the_condition(): + assert_accepted(pure_fn([If(UnaryOp(BOOL, UnaryOpKind.NOT, ge(li("n"), i(MAX))), + (Return(padd(li("n"), i(1))),)), Return(i(0))])) + assert_accepted(pure_fn([If(ge(li("n"), i(MAX)), (Return(i(0)),), + (Return(padd(li("n"), i(1))),))])) + + +def test_a_guard_that_returns_narrows_the_code_after_it(): + assert_accepted(pure_fn([If(ge(li("n"), i(MAX)), (Return(i(0)),)), + Return(padd(li("n"), i(1)))])) + # the branch falls through: the code after the If is reachable with n == MAX + assert_rejected(PROVEN, pure_fn([If(ge(li("n"), i(MAX)), (Assign("x", i(1)),)), + Return(padd(li("n"), i(1)))], locals_={"x": I64})) + + +def test_an_equality_guard_pins_the_local(): + assert_accepted(pure_fn([If(eq(li("n"), i(5)), (Return(padd(li("n"), i(MAX - 5))),)), + Return(i(0))])) + assert_rejected(PROVEN, pure_fn([If(eq(li("n"), i(5)), (Return(padd(li("n"), i(MAX - 4))),)), + Return(i(0))])) + + +def test_assigning_the_local_ends_the_guard(): + ps = N + A + ok = pure_fn([Assign("x", li("n")), + If(lt(li("x"), i(MAX)), (Return(padd(li("x"), i(1))),)), Return(i(0))], + params=ps, locals_={"x": I64}) + assert_accepted(ok) + killed = pure_fn([Assign("x", li("n")), + If(lt(li("x"), i(MAX)), (Assign("x", elem()), Return(padd(li("x"), i(1))))), + Return(i(0))], params=ps, locals_={"x": I64}) + assert_rejected(PROVEN, killed) + + +def test_a_while_condition_holds_at_the_top_of_each_iteration_until_the_local_is_assigned(): + # while lo < hi: lo += 1; hi -= 1 (the fannkuch reversal) + loop = While(lt(li("lo"), li("hi")), (Assign("lo", padd(li("lo"), i(1))), + Assign("hi", psub(li("hi"), i(1))))) + body = [Assign("lo", elem(0)), Assign("hi", elem(1)), loop, Return(i(0))] + assert_accepted(pure_fn(body, params=A, locals_={"lo": I64, "hi": I64})) + # lo <= hi lets lo be MAX (and hi be MIN): neither step is safe + weak = While(le(li("lo"), li("hi")), (Assign("lo", padd(li("lo"), i(1))),)) + assert_rejected(PROVEN, pure_fn([Assign("lo", elem(0)), Assign("hi", elem(1)), weak, Return(i(0))], + params=A, locals_={"lo": I64, "hi": I64})) + weak2 = While(le(li("lo"), li("hi")), (Assign("hi", psub(li("hi"), i(1))),)) + assert_rejected(PROVEN, pure_fn([Assign("lo", elem(0)), Assign("hi", elem(1)), weak2, Return(i(0))], + params=A, locals_={"lo": I64, "hi": I64})) + + +def test_a_guard_does_not_survive_the_back_edge_of_a_loop_that_assigns_the_local(): + # if x < MAX: while c: y = x + 1; x = a[0] second iteration: x is any i64 + inner = While(lb("c"), (Assign("y", padd(li("x"), i(1))), Assign("x", elem()))) + body = [Assign("x", li("n")), If(lt(li("x"), i(MAX)), (inner,)), Return(i(0))] + ps = N + A + [Param("c", BOOL)] + assert_rejected(PROVEN, pure_fn(body, params=ps, locals_={"x": I64, "y": I64})) + # the same loop with the guard as its own condition re-checks it every iteration + again = While(lt(li("x"), i(MAX)), (Assign("y", padd(li("x"), i(1))), Assign("x", elem()))) + assert_accepted(pure_fn([Assign("x", li("n")), again, Return(i(0))], params=N + A, + locals_={"x": I64, "y": I64})) + + +def test_a_guard_does_not_outlive_a_loop_that_assigns_the_local(): + inner = While(lb("c"), (Assign("x", elem()),)) + body = [Assign("x", li("n")), + If(lt(li("x"), i(MAX)), (inner, Return(padd(li("x"), i(1))))), Return(i(0))] + ps = N + A + [Param("c", BOOL)] + assert_rejected(PROVEN, pure_fn(body, params=ps, locals_={"x": I64})) + + +def test_a_guard_on_a_float_comparison_proves_nothing(): + ps = [Param("n", I64), Param("x", Type.F64)] + body = [If(lt(Const(Type.F64, 0.0), Local(Type.F64, "x")), (Return(padd(li("n"), i(1))),)), Return(i(0))] + assert_rejected(PROVEN, pure_fn(body, params=ps)) + + +# --- 1b. locals ---------------------------------------------------------------------------------- + +def test_a_local_assigned_a_constant_has_that_interval(): + body = [Assign("x", i(1)), Return(padd(li("x"), i(1)))] + assert_accepted(pure_fn(body, params=(), locals_={"x": I64})) + + +def test_a_local_has_the_join_of_all_its_assignments(): + ps = [Param("c", BOOL)] + def f(extra): + return pure_fn([If(lb("c"), (Assign("x", i(5)),), (Assign("x", i(7)),)), + Return(padd(li("x"), i(extra)))], params=ps, locals_={"x": I64}) + assert_accepted(f(MAX - 7)) + assert_rejected(PROVEN, f(MAX - 6)) + + +def test_a_local_assigned_from_an_unknown_value_is_full_range(): + body = [Assign("x", li("n")), Return(padd(li("x"), i(1)))] + assert_rejected(PROVEN, pure_fn(body, locals_={"x": I64})) + body = [Assign("x", i(0)), If(gt(li("n"), i(0)), (Assign("x", elem()),)), + Return(padd(li("x"), i(1)))] + assert_rejected(PROVEN, pure_fn(body, params=N + A, locals_={"x": I64})) + + +def test_a_counter_that_only_grows_is_non_negative(): + # x = 0; while c: x = x + 1 (checked) x in [0, MAX] + loop = While(lb("c"), (Assign("x", BinOp(I64, BinOpKind.ADD, li("x"), i(1))),)) + ps = [Param("c", BOOL)] + base = [Assign("x", i(0)), loop] + assert_accepted(pure_fn(base + [Return(pdiv(li("x"), i(4)))], params=ps, locals_={"x": I64}, + may_deopt=True)) + # a proven +1 on it is not provable: x can be MAX + assert_rejected(PROVEN, pure_fn(base + [Return(padd(li("x"), i(1)))], params=ps, + locals_={"x": I64}, may_deopt=True)) + + +def test_a_counter_that_only_shrinks_is_not_non_negative(): + loop = While(lb("c"), (Assign("x", BinOp(I64, BinOpKind.SUB, li("x"), i(1))),)) + ps = [Param("c", BOOL)] + assert_rejected(PROVEN, pure_fn([Assign("x", i(0)), loop, Return(pdiv(li("x"), i(4)))], + params=ps, locals_={"x": I64}, may_deopt=True)) + + +def test_the_fixpoint_terminates_and_stays_sound_for_mutually_dependent_locals(): + # x = y + 1 and y = x + 1 (checked): both start at 0 and grow without bound + loop = While(lb("c"), (Assign("x", BinOp(I64, BinOpKind.ADD, li("y"), i(1))), + Assign("y", BinOp(I64, BinOpKind.ADD, li("x"), i(1))))) + ps = [Param("c", BOOL)] + base = [Assign("x", i(0)), Assign("y", i(0)), loop] + loc = {"x": I64, "y": I64} + assert_accepted(pure_fn(base + [Return(pdiv(li("y"), i(2)))], params=ps, locals_=loc, + may_deopt=True)) + assert_rejected(PROVEN, pure_fn(base + [Return(padd(li("y"), i(1)))], params=ps, locals_=loc, + may_deopt=True)) + + +def test_a_for_range_variable_is_still_only_known_inside_its_loop(): + body = [Assign("k", i(0)), ForRange("k", i(0), i(5), i(1), ()), Return(padd(li("k"), i(1)))] + assert_rejected(PROVEN, pure_fn(body, params=(), locals_={"k": I64})) + + +def test_a_parameter_that_is_reassigned_is_still_unknown(): + body = [Assign("n", i(0)), Return(padd(li("n"), i(1)))] + assert_rejected(PROVEN, pure_fn(body)) + + +# --- 1c. // and % --------------------------------------------------------------------------------- + +def test_mod_by_a_positive_constant_is_between_zero_and_the_divisor_minus_one(): + ok = lambda extra: pure_fn([Return(padd(mod(li("n"), i(7)), i(extra)))], may_deopt=True) + assert_accepted(ok(MAX - 6)) + assert_rejected(PROVEN, ok(MAX - 5)) + + +def test_mod_by_a_negative_constant_is_between_the_divisor_plus_one_and_zero(): + assert_accepted(pure_fn([Return(padd(mod(li("n"), i(-7)), i(MAX)))], may_deopt=True)) + assert_rejected(PROVEN, pure_fn([Return(padd(mod(li("n"), i(7)), i(MAX)))], may_deopt=True)) + + +def test_mod_by_an_unknown_divisor_is_full_range(): + ps = [Param("n", I64), Param("m", I64)] + assert_rejected(PROVEN, pure_fn([Return(padd(mod(li("n"), li("m")), i(1)))], params=ps, + may_deopt=True)) + + +def test_floordiv_by_a_positive_constant_halves_the_range(): + two = lambda e: pure_fn([Return(e(div(li("n"), i(2))))], may_deopt=True) + assert_accepted(two(lambda d: padd(d, d))) # [-2**63, 2**63 - 2] + assert_accepted(two(lambda d: pmul(d, i(2)))) + assert_rejected(PROVEN, two(lambda d: pmul(d, i(3)))) + + +def test_floordiv_by_minus_one_is_full_range(): + assert_rejected(PROVEN, pure_fn([Return(padd(div(li("n"), i(-1)), i(1)))], may_deopt=True)) + + +# --- 1d. floor division / modulo by a power of two ------------------------------------------------- + +def _loop(op, start=0, stop=5, params=()): + return fn(params=params, locals_={"k": I64, "t": I64}, pure=True, may_deopt=False, + body=(ForRange("k", i(start), i(stop), i(1), (Assign("t", op(li("k"))),)), Return())) + + +@pytest.mark.parametrize("d", [1, 2, 8, 1024, 2 ** 62]) +def test_proven_floordiv_and_mod_by_a_power_of_two_of_a_non_negative_value_are_accepted(d): + assert_accepted(_loop(lambda k: pdiv(k, i(d)))) + assert_accepted(_loop(lambda k: pmod(k, i(d)))) + + +def test_a_proven_div_is_not_a_deopting_node(): + ok = _loop(lambda k: pdiv(k, i(4))) + assert_accepted(ok) + assert_rejected(FLAG_DEOPT, dataclasses.replace(ok, may_deopt=True)) + + +@pytest.mark.parametrize("op", [pdiv, pmod]) +def test_proven_div_or_mod_needs_a_non_negative_dividend(op): + assert_rejected(PROVEN, _loop(lambda k: op(k, i(4)), start=-1)) + assert_rejected(PROVEN, pure_fn([Return(op(li("n"), i(4)))])) + + +@pytest.mark.parametrize("op", [pdiv, pmod]) +@pytest.mark.parametrize("d", [0, -8, 3, 6, 12]) +def test_proven_div_or_mod_needs_a_positive_power_of_two_constant(op, d): + assert_rejected(PROVEN, _loop(lambda k: op(k, i(d)))) + + +@pytest.mark.parametrize("op", [pdiv, pmod]) +def test_proven_div_or_mod_needs_a_constant_divisor(op): + assert_rejected(PROVEN, _loop(lambda k: op(k, li("k")))) + assert_rejected(PROVEN, _loop(lambda k: op(k, padd(i(2), i(2))))) + + +def test_proven_truediv_is_still_rejected(): + assert_rejected(PROVEN, _loop(lambda k: BinOp(Type.F64, BinOpKind.TRUEDIV, k, i(2), proven=True))) + + +def test_a_guarded_dividend_is_non_negative(): + assert_accepted(pure_fn([If(ge(li("n"), i(0)), (Return(pdiv(li("n"), i(16))),)), Return(i(0))])) + assert_rejected(PROVEN, pure_fn([If(ge(li("n"), i(-1)), (Return(pdiv(li("n"), i(16))),)), + Return(i(0))])) + + +def test_a_mod_result_can_feed_a_proof(): + # (k % 8) + (MAX - 7) fits + assert_accepted(_loop(lambda k: padd(pmod(k, i(8)), i(MAX - 7)))) + assert_rejected(PROVEN, _loop(lambda k: padd(pmod(k, i(8)), i(MAX - 6)))) + + +# --- 2. end to end --------------------------------------------------------------------------------- + +SOURCE = '''\ +# typedpython: compiled + + +def dec_if_positive(n: int) -> int: + if n > 0: + return n - 1 + return -1 + + +def dec_after_guard(n: int) -> int: + if n <= 0: + return 0 + return n - 1 + + +def inc_below_max(n: int) -> int: + if n < 9223372036854775807: + return n + 1 + return 0 + + +def inc_below_100(n: int) -> int: + if n < 100: + return n + 1 + return 0 + + +def inc_if_positive(n: int) -> int: + if n > 0: + return n + 1 + return 0 + + +def reverse_gap(a: int, b: int) -> int: + lo: int = a + hi: int = b + steps: int = 0 + while lo < hi: + lo += 1 + hi -= 1 + steps += 1 + return hi - lo + steps + + +def killed_guard(n: int, a: list[int]) -> int: + if n < 100: + n = a[0] + return n + 1 + return 0 + + +def killed_in_loop(c: int, a: list[int]) -> int: + n: int = a[0] + t: int = 0 + if n < 100: + for i in range(c): + t = n + 1 + n = a[1] + return t + + +def parity(n: int) -> int: + k: int = 0 + s: int = 0 + for i in range(n): + if k % 2 == 0: + s += 1 + k += 1 + return s + + +def const_local() -> int: + x: int = 41 + return x + 1 + + +def range_shifts(a: int, b: int) -> int: + if a < 0: + return 0 + t: int = 0 + for i in range(a, b): + t += i // 4 + i % 8 + i // 1 + return t + + +def guarded_shift(n: int) -> int: + if n >= 0: + return n // 16 + n % 16 + return 0 + + +def negative_shift(n: int) -> int: + return n // 4 + n % 8 + + +def odd_divisor(n: int) -> int: + if n >= 0: + return n // 3 + n % 6 + return 0 + + +def mod_then_add(n: int) -> int: + return n % 10 + 1 + + +def pair_sums(a: list[int]) -> int: + best: int = 0 + for i in range(len(a)): + for j in range(len(a)): + if i + j > best: + best = i + j + return best +''' + +CASES = { + "dec_if_positive": [(n,) for n in (MIN, -1, 0, 1, 2, MAX - 1, MAX)], + "dec_after_guard": [(n,) for n in (MIN, -1, 0, 1, 2, MAX - 1, MAX)], + "inc_below_max": [(n,) for n in (MIN, -1, 0, MAX - 2, MAX - 1, MAX)], + "inc_below_100": [(n,) for n in (MIN, 98, 99, 100, MAX)], + "inc_if_positive": [(n,) for n in (MIN, 0, 1, MAX - 1, MAX)], + "reverse_gap": [(0, 0), (0, 1), (0, 7), (5, 2), (-3, 4), (MAX - 3, MAX), (MIN, MIN + 3), + (MAX - 1, MAX), (MIN, MIN + 1)], + "killed_guard": [(5, [3]), (5, [MAX]), (500, [MAX]), (5, [MIN])], + "killed_in_loop": [(0, [5, MAX]), (1, [5, MAX]), (3, [5, MAX]), (3, [5, 6]), (3, [500, MAX])], + "parity": [(0,), (1,), (2,), (7,), (100,)], + "const_local": [()], + "range_shifts": [(0, 0), (0, 40), (-20, 20), (-3, 0), (3, 3), (5, 2), (MAX - 5, MAX), (MIN, MIN + 6), + (MIN + 3, MIN + 4)], + "guarded_shift": [(n,) for n in (MIN, -1, 0, 1, 15, 16, 17, 1023, MAX)], + "negative_shift": [(n,) for n in (MIN, -9, -8, -1, 0, 1, 7, 8, MAX)], + "odd_divisor": [(n,) for n in (MIN, -1, 0, 1, 5, 6, 7, MAX)], + "mod_then_add": [(n,) for n in (MIN, -11, -1, 0, 9, 10, MAX)], + "pair_sums": [([],), ([5],), ([1, 2, 3],), (list(range(9)),)], +} + + +@pytest.fixture(scope="module") +def built(tmp_path_factory): + d = tmp_path_factory.mktemp("interval_proofs") + path = d / "ivmod.py" + path.write_text(SOURCE) + lowered = frontend.lower(path) + proved, diags = verify.verify(lowered) + c = cgen.generate(proved, path, path.name) + so = cbuild.build(c, path.stem, d / "out") + loader = importlib.machinery.ExtensionFileLoader(path.stem, str(so)) + spec = importlib.util.spec_from_file_location(path.stem, str(so), loader=loader) + module = importlib.util.module_from_spec(spec) + loader.exec_module(module) + return dataclasses.make_dataclass("Built", ["lowered", "proved", "diags", "c", "module"])( + lowered, proved, diags, c, module) + + +def impl_text(c: str, name: str) -> str: + """The C text of the normal implementation of `name`.""" + start = c.index(f"static int tp_impl_{name}(", c.index("static const char tp_source")) + while not c[c.index(")", start) + 1:].startswith("\n{"): + start = c.index(f"static int tp_impl_{name}(", start + 1) + return c[start:c.index("\n}\n", start)] + + +def helpers(c: str, name: str) -> dict[str, int]: + text = impl_text(c, name) + out: dict[str, int] = {} + for h in re.findall(r"tp_(add|sub|mul|floordiv|mod|neg)_i64\(", text): + out[h] = out.get(h, 0) + 1 + return out + + +def test_every_function_is_compiled(built): + assert {f.name for f in built.proved.functions} == set(CASES), (built.proved.skipped, built.diags) + + +@pytest.mark.parametrize("name", sorted(CASES)) +def test_compiled_equals_cpython_at_the_boundaries(built, name): + comp = getattr(built.module, name) + plain = built.module.__typedpython_interpreted__[name] + for args in CASES[name]: + want = plain(*[list(a) if isinstance(a, list) else a for a in args]) + got = comp(*[list(a) if isinstance(a, list) else a for a in args]) + assert got == want and type(got) is type(want), (name, args, got, want) + + +# which helpers must be gone from each function's C, and which must stay +GONE = { + "dec_if_positive": ["sub"], + "dec_after_guard": ["sub"], + "inc_below_max": ["add"], + "inc_below_100": ["add"], + "const_local": ["add"], + "guarded_shift": ["floordiv", "mod", "add"], + "mod_then_add": ["add"], + "pair_sums": ["add"], +} +STAY = { + "inc_if_positive": ["add"], + "killed_guard": ["add"], + "killed_in_loop": ["add"], + "negative_shift": ["floordiv", "mod"], + "odd_divisor": ["floordiv", "mod"], + "mod_then_add": ["mod"], +} + + +@pytest.mark.parametrize("name", sorted(GONE)) +def test_a_proved_operation_has_no_checked_helper_in_the_c(built, name): + found = helpers(built.c, name) + for h in GONE[name]: + assert h not in found, (name, found) + + +@pytest.mark.parametrize("name", sorted(STAY)) +def test_an_unprovable_operation_keeps_its_checked_helper(built, name): + found = helpers(built.c, name) + for h in STAY[name]: + assert h in found, (name, found) + + +def test_reverse_gap_drops_exactly_the_two_guarded_steps(built): + # lo += 1 and hi -= 1 are proved by `lo < hi`; `steps += 1` and `hi - lo + steps` are not + assert helpers(built.c, "reverse_gap") == {"add": 2, "sub": 1} + + +def test_parity_masks_the_accumulator_and_keeps_its_increments_checked(built): + found = helpers(built.c, "parity") + assert "mod" not in found and found.get("add", 0) >= 2 + assert "& " in impl_text(built.c, "parity") + + +def test_range_shifts_use_shifts_and_masks(built): + text = impl_text(built.c, "range_shifts") + found = helpers(built.c, "range_shifts") + assert "floordiv" not in found and "mod" not in found + assert ">> 2" in text and "& INT64_C(7)" in text + + +def test_the_front_end_marks_the_new_facts_and_the_verifier_agrees(built): + f = {g.name: g for g in built.lowered.functions} + def ops(fn_name): + found, stack = [], [f[fn_name]] + while stack: + x = stack.pop() + if isinstance(x, (tuple, list)): + stack.extend(x) + elif dataclasses.is_dataclass(x) and not isinstance(x, type): + if isinstance(x, BinOp): + found.append(x) + stack.extend(getattr(x, fl.name) for fl in dataclasses.fields(x)) + return found + + assert all(b.proven for b in ops("dec_if_positive")) + assert all(b.proven for b in ops("guarded_shift")) + assert not any(b.proven for b in ops("inc_if_positive")) + assert built.diags == [] diff --git a/python-multiplatform-ksp/src/test/python/test_verify.py b/python-multiplatform-ksp/src/test/python/test_verify.py index ec31224d1..6a2d8155d 100644 --- a/python-multiplatform-ksp/src/test/python/test_verify.py +++ b/python-multiplatform-ksp/src/test/python/test_verify.py @@ -743,10 +743,11 @@ def test_duplicate_function_names_are_rejected(): # The verifier never trusts `proven`: it computes an interval for every I64 expression and accepts # a proven op only when the exact result interval fits in i64. Intervals (verify.py documents them): # Const [v, v]; a ForRange var inside its own loop [lo(start), hi(stop)-1] (step > 0) or -# [lo(stop)+1, hi(start)] (step < 0); Len [0, 2**60-1]; ADD/SUB/MUL/NEG/POS by interval arithmetic; +# [lo(stop)+1, hi(start)] (step < 0); Len [0, 2**62]; ADD/SUB/MUL/NEG/POS by interval arithmetic; # MOD by a divisor whose interval is positive [0, hi(divisor)-1]; FLOORDIV by a positive divisor -# interval by its endpoints; everything else (params, entry globals, other locals, Index, Unbox, -# Call) the full i64 range. +# interval by its endpoints; a local assigned only i64 values (not a loop var) the join of their +# intervals, narrowed by the guards around the read (#148, test_interval_proofs.py); everything else +# (params, entry globals, Index, Unbox, Call) the full i64 range. def _ranged(op, start=0, stop=5, step=1, impure=True, pure=False, may_deopt=False, params=()): """for k in range(start, stop, step): t = in an (impure) function""" @@ -855,17 +856,23 @@ def test_len_bound_is_zero_to_two_to_the_62(): assert_rejected(PROVEN, fn(params=a, returns=I64, body=[W, Return(pmul(L, i(-3)))])) -def test_mod_and_floordiv_are_full_range_so_nothing_is_provable_from_them(): +def test_mod_and_floordiv_by_a_constant_have_bounded_results(): + # #148: n % 7 is in [0, 6] (it was full range before) ps = [Param("n", I64)] m = BinOp(I64, BinOpKind.MOD, li("n"), i(7)) - assert_rejected(PROVEN, fn(params=ps, returns=I64, pure=True, may_deopt=True, - body=[Return(padd(m, i(1)))])) + assert_accepted(fn(params=ps, returns=I64, pure=True, may_deopt=True, + body=[Return(padd(m, i(1)))])) + # ... and by an unknown divisor it is still full range + ps2 = [Param("n", I64), Param("d", I64)] + full = BinOp(I64, BinOpKind.MOD, li("n"), li("d")) + assert_rejected(PROVEN, fn(params=ps2, returns=I64, pure=True, may_deopt=True, + body=[Return(padd(full, i(1)))])) def test_what_the_intervals_cannot_prove(): - # a local assigned a constant is still full range (locals other than loop vars are not tracked) - assert_rejected(PROVEN, fn(locals_={"x": I64}, returns=I64, - body=[IMPURE, Assign("x", i(1)), Return(padd(li("x"), i(1)))])) + # a local assigned an unknown value is full range (#148: a local assigned a constant is not) + assert_rejected(PROVEN, fn(params=[Param("n", I64)], locals_={"x": I64}, returns=I64, + body=[IMPURE, Assign("x", li("n")), Return(padd(li("x"), i(1)))])) # the loop var after its loop is full range assert_rejected(PROVEN, fn(locals_={"k": I64}, returns=I64, body=[ IMPURE, Assign("k", i(0)), ForRange("k", i(0), i(5), i(1), ()), Return(padd(li("k"), i(1)))])) @@ -1304,7 +1311,7 @@ def _proof_mutations(rng, base): return "proven on param add", b, "q", {PROVEN} if kind == 2: # proven set on a node that has no i64 overflow node = rng.choice([BinOp(F64, BinOpKind.ADD, f(1.0), f(2.0), proven=True), - BinOp(I64, BinOpKind.FLOORDIV, i(4), i(2), proven=True), + BinOp(I64, BinOpKind.FLOORDIV, i(-4), i(2), proven=True), # negative dividend UnaryOp(I64, UnaryOpKind.POS, i(1), proven=True), BinOp(I64, BinOpKind.ADD, i(1), i(2), proven=1)]) t = Type.F64 if node.type is F64 else Type.I64 From de73628c7719143b233404e33d77097d4c05af2c Mon Sep 17 00:00:00 2001 From: BREW <81044362+b-re-w@users.noreply.github.com> Date: Sat, 17 Oct 2026 17:45:02 +0900 Subject: [PATCH 2/3] Test: The sanitizer run checks every proven op (TP_CHECK_PROVEN); SPEC N-9 row (#148) --- .github/workflows/typedpython.yml | 2 +- docs/SPEC.md | 1 + python-multiplatform-ksp/src/test/python/conftest.py | 6 ++++-- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/.github/workflows/typedpython.yml b/.github/workflows/typedpython.yml index d8b53d42b..8b26b70db 100644 --- a/.github/workflows/typedpython.yml +++ b/.github/workflows/typedpython.yml @@ -78,7 +78,7 @@ jobs: run: | env $(.venv/bin/python tools/sanitizers.py env) \ .venv/bin/python -m pytest -q -m "not measurement and not race_mutant" \ - src/test/python/test_cgen.py src/test/python/test_runtime.py src/test/python/test_pipeline.py + src/test/python/test_cgen.py src/test/python/test_runtime.py src/test/python/test_pipeline.py src/test/python/test_interval_proofs.py app-fixture: # #45: a TypedPython-compiled module calling Kotlin through the upcall table, in the app diff --git a/docs/SPEC.md b/docs/SPEC.md index 4bde73d18..310421966 100644 --- a/docs/SPEC.md +++ b/docs/SPEC.md @@ -577,6 +577,7 @@ All in `PM/commonTest`, so they run wherever the interpreter loads. | No deopting node in an impure function | not compiled; diagnostic | | Array access in bounds, or a runtime bounds check kept | the check stays (never an unchecked access) | | Array parameters only indexed, stored, `len`-ed; no aliasing (entry guard) | not compiled; diagnostic | + | Integer ops proven safe by the verifier's intervals (constants, `len`, `range` variables, guards such as `if x < e` / `while lo < hi`, joined local assignments, `//` and `%` by constants) | emitted unchecked (a shift/mask for `//`/`%` by a power of two of a non-negative value); the sanitizer CI run builds with `TP_CHECK_PROVEN` and turns a wrong proof into a SystemError (#148) | | A function holding an array parameter runs no user code: closed, and no slot read or `C(args)` whose slow path runs user code, in its whole call tree (#203) | not compiled; diagnostic | | OBJ references follow one ownership rule; no IR form for free, borrowed alias or NULL read | not compiled; diagnostic | | Integer overflow checked and promoted (deopt); an op marked `proven` must re-prove its interval fits i64 | not compiled; diagnostic `verify/proven-overflow` | diff --git a/python-multiplatform-ksp/src/test/python/conftest.py b/python-multiplatform-ksp/src/test/python/conftest.py index f04ff2974..139f2064e 100644 --- a/python-multiplatform-ksp/src/test/python/conftest.py +++ b/python-multiplatform-ksp/src/test/python/conftest.py @@ -28,7 +28,9 @@ def errors(diagnostics): # TP_SANITIZE=1 (tools/sanitizers.py): every extension TypedPython builds gets ASan + UBSan, and a -# sanitizer report fails the run (-fno-sanitize-recover=undefined; ASan halts). Nothing else changes. +# sanitizer report fails the run (-fno-sanitize-recover=undefined; ASan halts). It also defines +# TP_CHECK_PROVEN: an op the verifier proved runs the checked helper and raises SystemError if the +# proof was wrong (#148), so this run catches a wrong proof that the default build would let wrap. import os # noqa: E402 if os.environ.get("TP_SANITIZE") == "1": @@ -36,7 +38,7 @@ def errors(diagnostics): from typedpython import cbuild as _cbuild _SAN = ["-fsanitize=address,undefined", "-fno-sanitize-recover=undefined", "-g", - "-fno-omit-frame-pointer"] + "-fno-omit-frame-pointer", "-DTP_CHECK_PROVEN"] _orig_compiler = _cbuild.compiler def _sanitized_compiler(): From 8011a608b879afe63e441143aa121f9fa8cffab8 Mon Sep 17 00:00:00 2001 From: BREW <81044362+b-re-w@users.noreply.github.com> Date: Sat, 17 Oct 2026 18:01:44 +0900 Subject: [PATCH 3/3] Bench: Record the interval-proofs A/B (#148) --- .../2026-10-17-interval-proofs-ab.json | 308 ++++++++++++++++++ 1 file changed, 308 insertions(+) create mode 100644 benchmarks/typedpython/results/2026-10-17-interval-proofs-ab.json diff --git a/benchmarks/typedpython/results/2026-10-17-interval-proofs-ab.json b/benchmarks/typedpython/results/2026-10-17-interval-proofs-ab.json new file mode 100644 index 000000000..790a0ccda --- /dev/null +++ b/benchmarks/typedpython/results/2026-10-17-interval-proofs-ab.json @@ -0,0 +1,308 @@ +{ + "fannkuch-redux": { + "size": "10", + "pairs": [ + { + "before_s": 1.0887560830451548, + "after_s": 0.6829974167048931, + "cpython_s": 5.911647166591138, + "after_over_before": 0.627319036229501, + "speedup_before": 5.429725958505584, + "speedup_after": 8.655445865537468, + "load": [ + 2.66748046875, + 2.986328125, + 3.36767578125 + ] + }, + { + "after_s": 0.27054166700690985, + "before_s": 0.2709987089037895, + "cpython_s": 5.913880208041519, + "after_over_before": 0.9983134905006432, + "speedup_before": 21.822540158820743, + "speedup_after": 21.8594062551203, + "load": [ + 2.49072265625, + 2.93701171875, + 3.34521484375 + ] + }, + { + "before_s": 0.2726931250654161, + "after_s": 0.27129745902493596, + "cpython_s": 5.907416833098978, + "after_over_before": 0.9948819170261615, + "speedup_before": 21.663240801108767, + "speedup_after": 21.774685447960664, + "load": [ + 2.37109375, + 2.90478515625, + 3.3310546875 + ] + }, + { + "after_s": 0.270517417229712, + "before_s": 0.2704989998601377, + "cpython_s": 5.924571041949093, + "after_over_before": 1.0000680866457319, + "speedup_before": 21.90237688498815, + "speedup_after": 21.900885727140434, + "load": [ + 2.16015625, + 2.841796875, + 3.3037109375 + ] + }, + { + "before_s": 0.27097137505188584, + "after_s": 0.27024612482637167, + "cpython_s": 5.908709957730025, + "after_over_before": 0.9973235171966954, + "speedup_before": 21.805661046664504, + "speedup_after": 21.864180148841232, + "load": [ + 2.14697265625, + 2.82763671875, + 3.2958984375 + ] + }, + { + "after_s": 0.27170295920223, + "before_s": 0.2769245416857302, + "cpython_s": 6.009743249975145, + "after_over_before": 0.9811443852115281, + "speedup_before": 21.701735835299655, + "speedup_after": 22.118799396299767, + "load": [ + 2.0546875, + 2.796875, + 3.2822265625 + ] + }, + { + "before_s": 0.2953220000490546, + "after_s": 0.2890004999935627, + "cpython_s": 6.02235220791772, + "after_over_before": 0.9785945508480849, + "speedup_before": 20.3924943177866, + "speedup_after": 20.83855290233707, + "load": [ + 2.21044921875, + 2.81640625, + 3.2861328125 + ] + }, + { + "after_s": 0.27058391692116857, + "before_s": 0.2701001246459782, + "cpython_s": 6.634010416921228, + "after_over_before": 1.0017911590223236, + "speedup_before": 24.561300834705143, + "speedup_after": 24.51738629703542, + "load": [ + 2.3251953125, + 2.82177734375, + 3.2822265625 + ] + }, + { + "before_s": 0.3240792923606932, + "after_s": 0.3907488747499883, + "cpython_s": 6.6358414171263576, + "after_over_before": 1.205719970269169, + "speedup_before": 20.475980951417316, + "speedup_after": 16.982368589985445, + "load": [ + 2.69921875, + 2.89111328125, + 3.3037109375 + ] + }, + { + "after_s": 0.2735611251555383, + "before_s": 0.2766624162904918, + "cpython_s": 6.041726541239768, + "after_over_before": 0.9887903417582489, + "speedup_before": 21.83790130313919, + "speedup_after": 22.085471895192093, + "load": [ + 2.95947265625, + 2.94287109375, + 3.3173828125 + ] + }, + { + "before_s": 0.2883912082761526, + "after_s": 0.28800000017508864, + "cpython_s": 7.008296665735543, + "after_over_before": 0.9986434811816823, + "speedup_before": 24.301353386004266, + "speedup_after": 24.334363407898863, + "load": [ + 2.88232421875, + 2.9267578125, + 3.3095703125 + ] + } + ], + "median_after_over_before": 0.9973235171966954, + "min_after_over_before": 0.627319036229501, + "max_after_over_before": 1.205719970269169, + "median_speedup_before": 21.805661046664504, + "median_speedup_after": 21.864180148841232 + }, + "binary-trees": { + "size": "16", + "pairs": [ + { + "before_s": 3.155360875185579, + "after_s": 3.0856687501072884, + "cpython_s": 3.590506291948259, + "after_over_before": 0.9779131047651747, + "speedup_before": 1.1379067035358, + "speedup_after": 1.1636071732662223, + "load": [ + 2.7314453125, + 2.89453125, + 3.2958984375 + ] + }, + { + "after_s": 2.393941333051771, + "before_s": 2.388220750261098, + "cpython_s": 3.54007404204458, + "after_over_before": 1.0023953325043538, + "speedup_before": 1.4823060396144505, + "speedup_after": 1.478763908358494, + "load": [ + 2.8525390625, + 2.9140625, + 3.2978515625 + ] + }, + { + "before_s": 2.403391916770488, + "after_s": 2.392654124647379, + "cpython_s": 3.593896792270243, + "after_over_before": 0.9955322342360468, + "speedup_before": 1.4953436296396774, + "speedup_after": 1.5020544571187862, + "load": [ + 2.88134765625, + 2.91650390625, + 3.2939453125 + ] + }, + { + "after_s": 2.379018457606435, + "before_s": 2.754461499862373, + "cpython_s": 3.6588334999978542, + "after_over_before": 0.8636963913727975, + "speedup_before": 1.3283298750701973, + "speedup_after": 1.5379592740440777, + "load": [ + 3.04638671875, + 2.951171875, + 3.3017578125 + ] + }, + { + "before_s": 2.3003429169766605, + "after_s": 2.309331167023629, + "cpython_s": 3.513636375311762, + "after_over_before": 1.0039073522389357, + "speedup_before": 1.5274402565725864, + "speedup_after": 1.5214952387449465, + "load": [ + 3.580078125, + 3.0673828125, + 3.3388671875 + ] + }, + { + "after_s": 2.2887648749165237, + "before_s": 2.2567570419050753, + "cpython_s": 3.2699287086725235, + "after_over_before": 1.0141831098417349, + "speedup_before": 1.4489502626796564, + "speedup_after": 1.4286870374973686, + "load": [ + 3.693359375, + 3.09912109375, + 3.34814453125 + ] + }, + { + "before_s": 2.160762708168477, + "after_s": 2.1336489161476493, + "cpython_s": 3.3091259165666997, + "after_over_before": 0.987451749366866, + "speedup_before": 1.5314619713016095, + "speedup_after": 1.5509233461620295, + "load": [ + 3.740234375, + 3.12841796875, + 3.35498046875 + ] + }, + { + "after_s": 2.1829029163345695, + "before_s": 2.155100916977972, + "cpython_s": 3.1836033752188087, + "after_over_before": 1.012900555671232, + "speedup_before": 1.4772409728650073, + "speedup_after": 1.4584264611110465, + "load": [ + 3.5205078125, + 3.0927734375, + 3.3408203125 + ] + }, + { + "before_s": 2.9248738340102136, + "after_s": 2.181852374691516, + "cpython_s": 3.206505249720067, + "after_over_before": 0.7459646119846608, + "speedup_before": 1.0962883979592775, + "speedup_after": 1.4696252078802639, + "load": [ + 3.2060546875, + 3.03955078125, + 3.31884765625 + ] + }, + { + "after_s": 2.146172667387873, + "before_s": 2.1432514172047377, + "cpython_s": 3.184945832937956, + "after_over_before": 1.0013629993008217, + "speedup_before": 1.4860346328812009, + "speedup_after": 1.4840119256641096, + "load": [ + 3.669921875, + 3.13818359375, + 3.35205078125 + ] + }, + { + "before_s": 2.1659594592638314, + "after_s": 2.5923933750018477, + "cpython_s": 3.8596382504329085, + "after_over_before": 1.196879915694707, + "speedup_before": 1.7819531357917135, + "speedup_after": 1.4888320143273617, + "load": [ + 3.56640625, + 3.13330078125, + 3.34716796875 + ] + } + ], + "median_after_over_before": 1.0013629993008217, + "min_after_over_before": 0.7459646119846608, + "max_after_over_before": 1.196879915694707, + "median_speedup_before": 1.4823060396144505, + "median_speedup_after": 1.4840119256641096 + } +}