[Bug][Relax] Constant folding of an int64 Div goes through float64 and is off by one above 2^53

[lackjava-creator]

Environment

• TVM version: 0.26.0 (release wheel) and main @ 48242ec33403f2b6e4fac6e763ca7a683fb9d5df (2026-09-03 21:20:55 -0400, reports 0.26.dev0). Both verified 2026-09-06.

• Build / install: 0.26.0 from a venv wheel; main built from source (/home/lxx/tvm-main/build/lib), LLVM 15.0.7

• OS / Python: Ubuntu 24.04.3 LTS, x86_64 (Xeon E5-2698 v4), Python 3.10

• Reference implementation: onnxruntime 1.23.2 with ORT_DISABLE_ALL, cross-checked against Python's own integer division

• Target: llvm (CPU). opt_level=0 and opt_level=3 give the identical wrong answer, so this is the frontend/constant-fold path, not an optimisation pass.

• Pipeline coverage (relax.get_pipeline("default_build") performs no operator fusion, so all three are reported separately). Verified 2026-09-06 on 0.26.0, llvm:

  • get_pipeline("default_build") (no FuseOps/FuseTIR) — wrong, returns 9007199254740992
  • get_pipeline("zero") (fuses) — wrong, identical value
  • forced FuseOps + FuseTIR — wrong, identical value
    All three agreeing places the defect in constant folding, not in fusion.

Minimal reproducer

Two-node ONNX graph: a Div of two int64 initialisers, plus an Identity so the graph has a real input. model_div_i64_9007199254740993_1.onnx + matching .npz attached, with run.py.

import numpy as np, onnx, onnxruntime as ort, tvm
from onnx import numpy_helper as nh
from tvm import relax
from tvm.relax.frontend.onnx import from_onnx
m = onnx.load("model_div_i64_9007199254740993_1.onnx")           # y = Div(A, B), A = 2**53 + 1, B = 1
feed = dict(np.load("feed_div_i64_9007199254740993_1.npz"))
A, B = (int(nh.to_array(i)[0]) for i in m.graph.initializer)
sd = {i.name: [d.dim_value for d in i.type.tensor_type.shape.dim] for i in m.graph.input}
so = ort.SessionOptions(); so.graph_optimization_level = ort.GraphOptimizationLevel.ORT_DISABLE_ALL
print("python A // B :", A // B)
print("onnxruntime   :", ort.InferenceSession(m.SerializeToString(), so, providers=["CPUExecutionProvider"]).run(None, feed)[0].tolist())
for lvl, pipe in ((0, "zero"), (3, "default_build")):
    with tvm.transform.PassContext(opt_level=lvl):
        ex = tvm.compile(relax.get_pipeline(pipe)(from_onnx(m, shape_dict=sd, keep_params_in_input=False)), target="llvm")
    out = relax.VirtualMachine(ex, tvm.cpu())["main"](*[tvm.runtime.tensor(np.ascontiguousarray(feed[n]), tvm.cpu()) for n in sd])
    print(f"TVM opt{lvl}     :", np.asarray((out if hasattr(out, "numpy") else list(out)[0]).numpy()).tolist())

Expected vs actual

Full precision, on both 0.26.0 and main @ 48242ec, at opt_level 0 and 3 alike:

A	B	expected (A // B, onnxruntime)	TVM
9007199254740993 (2⁵³ + 1)	1	9007199254740993	9007199254740992
9007199254740995 (2⁵³ + 3)	1	9007199254740995	9007199254740996
72057594037927937 (2⁵⁶ + 1)	1	72057594037927937	72057594037927936
344313375098422616	1	344313375098422616	344313375098422612

• Difference: off by 1 in the first three rows and by 4 in the fourth — exactly the spacing of representable float64 values at those magnitudes. Note the second row rounds up and the first rounds down, which is round-to-nearest-even, not truncation.
• B = 1, so the division is the identity: the wrong answer appears with no division actually taking place.
• Coverage: in the campaign family that found this, 108 of 120 states failed.

Root cause (if known)

The constant folding of an int64 Div is performed in float64. Every operand above 2**53 therefore loses its low bits before the division. opt_level=0 (get_pipeline("zero")) and opt_level=3 (get_pipeline("default_build")) agree, which places the fold in the frontend/FoldConstant path rather than in a later optimisation pass.

Present on main @ 48242ec — never fixed.

Why this is a bug (not tolerance / not undefined behaviour)

1. Integer division has no tolerance. ONNX Div-14 on tensor(int64) is exact integer division; there is no rounding mode.
2. This is not integer overflow. 2**53 + 1 is nowhere near int64 range; nothing wraps. The value is rounded, which int64 arithmetic cannot do.
3. Constant folding must be value-preserving. The uncompiled semantics and the folded result differ, so the transformation is unsound regardless of what one thinks of the input magnitudes.
4. The oracle used to find this carries a reliability certificate: over 1560 lowered states in the same family, seed ORT == spec held with unsound = 0 (validate_cf2.log available on request).

How found

Found by EquiAutomaton (equivalence-graph differential testing against onnxruntime at ORT_DISABLE_ALL, with the expected value recomputed from the ONNX operator spec in Python integers rather than taken from another runtime). Depth-0 — the seed graph itself fails.

Reproducer archive

TVM-DIVCF-reproducer.zip

Triage

• Needs triage