FAILURE MAP
← Case archive

FA-89876 / Bytecode virtual machines / Open access

JVM int32 opcodes: MIN_VALUE / -1 escapes the int range · case 01

Dividing MIN_VALUE by -1 yields 2147483648, a value no int slot can hold.

Verified by executionVariant 1 · 8 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The truncated quotient is pushed without re-wrapping to 32 bits.

VERIFIED REPAIR

Wrap the quotient, which maps the single overflow case back to MIN_VALUE.

Unsuccessful approach: Saturating to MAX_VALUE is a different, non-conforming answer for the overflow case.

Case contract

Each op is [name, a, b] over 32-bit two's complement ints: iadd/imul wrap; idiv truncates toward zero and MIN_VALUE / -1 wraps to MIN_VALUE; irem has the sign of the dividend; ishl/ishr/iushr use only the low five bits of the shift count, iushr shifts in zeros; ineg wraps. Division by zero yields "ArithmeticException", an unknown op "VerifyError".

Why this case matters

Bytecode integer opcodes must reproduce fixed-width semantics that host-language integers do not.

1 / The failure

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(ops):
    def wrap(v):
        v &= 0xFFFFFFFF
        return v - 0x100000000 if v >= 0x80000000 else v
    out = []
    for op, a, b in ops:
        if op == 'iadd':
            out.append(wrap(a + b))
        elif op == 'imul':
            out.append(wrap(a * b))
        elif op == 'idiv':
            if b == 0:
                out.append('ArithmeticException')
            else:
                q = abs(a) // abs(b)
                out.append(q if (a < 0) == (b < 0) else -q)
        elif op == 'irem':
            if b == 0:
                out.append('ArithmeticException')
            else:
                r = abs(a) % abs(b)
                out.append(r if a >= 0 else -r)
        elif op == 'ishl':
            out.append(wrap(a << (b & 31)))
        elif op == 'ishr':
            out.append(a >> (b & 31))
        elif op == 'iushr':
            out.append(wrap((a & 0xFFFFFFFF) >> (b & 31)))
        elif op == 'ineg':
            out.append(wrap(-a))
        else:
            out.append('VerifyError')
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483646, 1], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -8, 2], ['idiv', 9, -2]],), [-4, -4]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483647, -1]],),
   [-2147483648, 2147483647]),
  ('irem takes the sign of the dividend', ([['irem', -10, 3], ['irem', 11, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 2, 32], ['ishl', 3, 34]],), [2, 12]),
  ('iushr is a logical shift with masking', ([['iushr', -16, 28], ['iushr', -16, 37]],), [15, 134217727]),
  ('division by zero', ([['idiv', 1, 0], ['irem', 1, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65537], ['ishr', -8, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [65536, -2, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483645, 2], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -9, 2], ['idiv', 11, -2]],), [-4, -5]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483646, -1]],),
   [-2147483648, 2147483646]),
  ('irem takes the sign of the dividend', ([['irem', -13, 3], ['irem', 14, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 3, 32], ['ishl', 3, 35]],), [3, 24]),
  ('iushr is a logical shift with masking', ([['iushr', -32, 28], ['iushr', -16, 38]],), [15, 67108863]),
  ('division by zero', ([['idiv', 2, 0], ['irem', 2, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65538], ['ishr', -16, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [131072, -4, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483644, 3], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -10, 2], ['idiv', 13, -2]],), [-5, -6]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483645, -1]],),
   [-2147483648, 2147483645]),
  ('irem takes the sign of the dividend', ([['irem', -16, 3], ['irem', 17, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 4, 32], ['ishl', 3, 36]],), [4, 48]),
  ('iushr is a logical shift with masking', ([['iushr', -48, 28], ['iushr', -16, 39]],), [15, 33554431]),
  ('division by zero', ([['idiv', 3, 0], ['irem', 3, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65539], ['ishr', -24, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [196608, -6, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483643, 4], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -11, 2], ['idiv', 15, -2]],), [-5, -7]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483644, -1]],),
   [-2147483648, 2147483644]),
  ('irem takes the sign of the dividend', ([['irem', -19, 3], ['irem', 20, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 5, 32], ['ishl', 3, 37]],), [5, 96]),
  ('iushr is a logical shift with masking', ([['iushr', -64, 28], ['iushr', -16, 40]],), [15, 16777215]),
  ('division by zero', ([['idiv', 4, 0], ['irem', 4, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65540], ['ishr', -32, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [262144, -8, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483642, 5], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -12, 2], ['idiv', 17, -2]],), [-6, -8]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483643, -1]],),
   [-2147483648, 2147483643]),
  ('irem takes the sign of the dividend', ([['irem', -22, 3], ['irem', 23, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 6, 32], ['ishl', 3, 38]],), [6, 192]),
  ('iushr is a logical shift with masking', ([['iushr', -80, 28], ['iushr', -16, 41]],), [15, 8388607]),
  ('division by zero', ([['idiv', 5, 0], ['irem', 5, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65541], ['ishr', -40, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [327680, -10, -2147483648, 'VerifyError'])]]
for label, args, expected in cases[N - 1]:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
regression: iadd reaching MAX_VALUE[2147483647, -2147483648][2147483647, -2147483648]Passed
idiv truncates toward zero[-4, -4][-4, -4]Passed
idiv MIN_VALUE by -1 overflows to MIN_VALUE[2147483648, 2147483647][-2147483648, 2147483647]Failed
irem takes the sign of the dividend[-1, 2][-1, 2]Passed
ishl masks the shift count to five bits[2, 12][2, 12]Passed
iushr is a logical shift with masking[15, 134217727][15, 134217727]Passed
division by zero['ArithmeticException', 'ArithmeticException']['ArithmeticException', 'ArithmeticException']Passed
controls: imul wrap, ishr, ineg MIN[65536, -2, -2147483648, 'VerifyError'][65536, -2, -2147483648, 'VerifyError']Passed

SHA-256 / b5dd8ceb3352132564d41d9c45f3bbe1adcb628935211e54a14aa3d32240a1a9

2 / The unsuccessful fix

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(ops):
    def wrap(v):
        v &= 0xFFFFFFFF
        return v - 0x100000000 if v >= 0x80000000 else v
    out = []
    for op, a, b in ops:
        if op == 'iadd':
            out.append(wrap(a + b))
        elif op == 'imul':
            out.append(wrap(a * b))
        elif op == 'idiv':
            if b == 0:
                out.append('ArithmeticException')
            else:
                q = abs(a) // abs(b)
                out.append(min(q, 2147483647) if (a < 0) == (b < 0) else -q)
        elif op == 'irem':
            if b == 0:
                out.append('ArithmeticException')
            else:
                r = abs(a) % abs(b)
                out.append(r if a >= 0 else -r)
        elif op == 'ishl':
            out.append(wrap(a << (b & 31)))
        elif op == 'ishr':
            out.append(a >> (b & 31))
        elif op == 'iushr':
            out.append(wrap((a & 0xFFFFFFFF) >> (b & 31)))
        elif op == 'ineg':
            out.append(wrap(-a))
        else:
            out.append('VerifyError')
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483646, 1], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -8, 2], ['idiv', 9, -2]],), [-4, -4]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483647, -1]],),
   [-2147483648, 2147483647]),
  ('irem takes the sign of the dividend', ([['irem', -10, 3], ['irem', 11, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 2, 32], ['ishl', 3, 34]],), [2, 12]),
  ('iushr is a logical shift with masking', ([['iushr', -16, 28], ['iushr', -16, 37]],), [15, 134217727]),
  ('division by zero', ([['idiv', 1, 0], ['irem', 1, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65537], ['ishr', -8, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [65536, -2, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483645, 2], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -9, 2], ['idiv', 11, -2]],), [-4, -5]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483646, -1]],),
   [-2147483648, 2147483646]),
  ('irem takes the sign of the dividend', ([['irem', -13, 3], ['irem', 14, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 3, 32], ['ishl', 3, 35]],), [3, 24]),
  ('iushr is a logical shift with masking', ([['iushr', -32, 28], ['iushr', -16, 38]],), [15, 67108863]),
  ('division by zero', ([['idiv', 2, 0], ['irem', 2, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65538], ['ishr', -16, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [131072, -4, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483644, 3], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -10, 2], ['idiv', 13, -2]],), [-5, -6]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483645, -1]],),
   [-2147483648, 2147483645]),
  ('irem takes the sign of the dividend', ([['irem', -16, 3], ['irem', 17, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 4, 32], ['ishl', 3, 36]],), [4, 48]),
  ('iushr is a logical shift with masking', ([['iushr', -48, 28], ['iushr', -16, 39]],), [15, 33554431]),
  ('division by zero', ([['idiv', 3, 0], ['irem', 3, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65539], ['ishr', -24, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [196608, -6, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483643, 4], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -11, 2], ['idiv', 15, -2]],), [-5, -7]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483644, -1]],),
   [-2147483648, 2147483644]),
  ('irem takes the sign of the dividend', ([['irem', -19, 3], ['irem', 20, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 5, 32], ['ishl', 3, 37]],), [5, 96]),
  ('iushr is a logical shift with masking', ([['iushr', -64, 28], ['iushr', -16, 40]],), [15, 16777215]),
  ('division by zero', ([['idiv', 4, 0], ['irem', 4, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65540], ['ishr', -32, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [262144, -8, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483642, 5], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -12, 2], ['idiv', 17, -2]],), [-6, -8]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483643, -1]],),
   [-2147483648, 2147483643]),
  ('irem takes the sign of the dividend', ([['irem', -22, 3], ['irem', 23, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 6, 32], ['ishl', 3, 38]],), [6, 192]),
  ('iushr is a logical shift with masking', ([['iushr', -80, 28], ['iushr', -16, 41]],), [15, 8388607]),
  ('division by zero', ([['idiv', 5, 0], ['irem', 5, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65541], ['ishr', -40, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [327680, -10, -2147483648, 'VerifyError'])]]
for label, args, expected in cases[N - 1]:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
regression: iadd reaching MAX_VALUE[2147483647, -2147483648][2147483647, -2147483648]Passed
idiv truncates toward zero[-4, -4][-4, -4]Passed
idiv MIN_VALUE by -1 overflows to MIN_VALUE[2147483647, 2147483647][-2147483648, 2147483647]Failed
irem takes the sign of the dividend[-1, 2][-1, 2]Passed
ishl masks the shift count to five bits[2, 12][2, 12]Passed
iushr is a logical shift with masking[15, 134217727][15, 134217727]Passed
division by zero['ArithmeticException', 'ArithmeticException']['ArithmeticException', 'ArithmeticException']Passed
controls: imul wrap, ishr, ineg MIN[65536, -2, -2147483648, 'VerifyError'][65536, -2, -2147483648, 'VerifyError']Passed

SHA-256 / b1c90ffbdc9e651e920fe0e883ab43f810cbc01f58fd5214c4deeb96601839c9

3 / The verified repair

Exit 0
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(ops):
    def wrap(v):
        v &= 0xFFFFFFFF
        return v - 0x100000000 if v >= 0x80000000 else v
    out = []
    for op, a, b in ops:
        if op == 'iadd':
            out.append(wrap(a + b))
        elif op == 'imul':
            out.append(wrap(a * b))
        elif op == 'idiv':
            if b == 0:
                out.append('ArithmeticException')
            else:
                q = abs(a) // abs(b)
                out.append(wrap(q if (a < 0) == (b < 0) else -q))
        elif op == 'irem':
            if b == 0:
                out.append('ArithmeticException')
            else:
                r = abs(a) % abs(b)
                out.append(r if a >= 0 else -r)
        elif op == 'ishl':
            out.append(wrap(a << (b & 31)))
        elif op == 'ishr':
            out.append(a >> (b & 31))
        elif op == 'iushr':
            out.append(wrap((a & 0xFFFFFFFF) >> (b & 31)))
        elif op == 'ineg':
            out.append(wrap(-a))
        else:
            out.append('VerifyError')
    return out
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483646, 1], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -8, 2], ['idiv', 9, -2]],), [-4, -4]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483647, -1]],),
   [-2147483648, 2147483647]),
  ('irem takes the sign of the dividend', ([['irem', -10, 3], ['irem', 11, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 2, 32], ['ishl', 3, 34]],), [2, 12]),
  ('iushr is a logical shift with masking', ([['iushr', -16, 28], ['iushr', -16, 37]],), [15, 134217727]),
  ('division by zero', ([['idiv', 1, 0], ['irem', 1, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65537], ['ishr', -8, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [65536, -2, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483645, 2], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -9, 2], ['idiv', 11, -2]],), [-4, -5]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483646, -1]],),
   [-2147483648, 2147483646]),
  ('irem takes the sign of the dividend', ([['irem', -13, 3], ['irem', 14, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 3, 32], ['ishl', 3, 35]],), [3, 24]),
  ('iushr is a logical shift with masking', ([['iushr', -32, 28], ['iushr', -16, 38]],), [15, 67108863]),
  ('division by zero', ([['idiv', 2, 0], ['irem', 2, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65538], ['ishr', -16, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [131072, -4, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483644, 3], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -10, 2], ['idiv', 13, -2]],), [-5, -6]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483645, -1]],),
   [-2147483648, 2147483645]),
  ('irem takes the sign of the dividend', ([['irem', -16, 3], ['irem', 17, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 4, 32], ['ishl', 3, 36]],), [4, 48]),
  ('iushr is a logical shift with masking', ([['iushr', -48, 28], ['iushr', -16, 39]],), [15, 33554431]),
  ('division by zero', ([['idiv', 3, 0], ['irem', 3, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65539], ['ishr', -24, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [196608, -6, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483643, 4], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -11, 2], ['idiv', 15, -2]],), [-5, -7]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483644, -1]],),
   [-2147483648, 2147483644]),
  ('irem takes the sign of the dividend', ([['irem', -19, 3], ['irem', 20, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 5, 32], ['ishl', 3, 37]],), [5, 96]),
  ('iushr is a logical shift with masking', ([['iushr', -64, 28], ['iushr', -16, 40]],), [15, 16777215]),
  ('division by zero', ([['idiv', 4, 0], ['irem', 4, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65540], ['ishr', -32, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [262144, -8, -2147483648, 'VerifyError'])],
 [('regression: iadd reaching MAX_VALUE',
   ([['iadd', 2147483642, 5], ['iadd', 2147483647, 1]],),
   [2147483647, -2147483648]),
  ('idiv truncates toward zero', ([['idiv', -12, 2], ['idiv', 17, -2]],), [-6, -8]),
  ('idiv MIN_VALUE by -1 overflows to MIN_VALUE',
   ([['idiv', -2147483648, -1], ['idiv', -2147483643, -1]],),
   [-2147483648, 2147483643]),
  ('irem takes the sign of the dividend', ([['irem', -22, 3], ['irem', 23, -3]],), [-1, 2]),
  ('ishl masks the shift count to five bits', ([['ishl', 6, 32], ['ishl', 3, 38]],), [6, 192]),
  ('iushr is a logical shift with masking', ([['iushr', -80, 28], ['iushr', -16, 41]],), [15, 8388607]),
  ('division by zero', ([['idiv', 5, 0], ['irem', 5, 0]],), ['ArithmeticException', 'ArithmeticException']),
  ('controls: imul wrap, ishr, ineg MIN',
   ([['imul', 65536, 65541], ['ishr', -40, 2], ['ineg', -2147483648, 0], ['bogus', 1, 1]],),
   [327680, -10, -2147483648, 'VerifyError'])]]
for label, args, expected in cases[N - 1]:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
regression: iadd reaching MAX_VALUE[2147483647, -2147483648][2147483647, -2147483648]Passed
idiv truncates toward zero[-4, -4][-4, -4]Passed
idiv MIN_VALUE by -1 overflows to MIN_VALUE[-2147483648, 2147483647][-2147483648, 2147483647]Passed
irem takes the sign of the dividend[-1, 2][-1, 2]Passed
ishl masks the shift count to five bits[2, 12][2, 12]Passed
iushr is a logical shift with masking[15, 134217727][15, 134217727]Passed
division by zero['ArithmeticException', 'ArithmeticException']['ArithmeticException', 'ArithmeticException']Passed
controls: imul wrap, ishr, ineg MIN[65536, -2, -2147483648, 'VerifyError'][65536, -2, -2147483648, 'VerifyError']Passed

SHA-256 / d82463138cabe7da586d4868218a3ec371fb8a5d390b26b71191a945b77e3ddc

Verification & scope

A deterministic, bounded teaching model of one bytecode virtual machine mechanism with a stipulated instruction encoding; it is not a production VM and claims no conformance to any real specification. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.

Observations recorded using Python 3.12.14 at 2026-09-29T14:51:21.367863+00:00.

Case digest / 70125f65e9771c3a0038f633162ed520f60cba213dc97bdeba64e1965b63bf11