FAILURE MAP
← Case archive

FA-89891 / Bytecode virtual machines / Open access

JVM int32 opcodes: iushr sign-extends · case 01

Unsigned right shifts of negative ints stay negative.

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

ROOT CAUSE

The shift is applied to the signed value, so ones are shifted in.

VERIFIED REPAIR

Reinterpret the operand as unsigned 32-bit before shifting by the masked count.

Unsuccessful approach: Reinterpreting as unsigned but shifting by the unmasked count breaks counts of 32 and above.

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(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 >> (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[-1, -1][15, 134217727]Failed
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 / 197d135088d4d21adbc671252c90a97e47635f8ff9ab32645cf7336967fa85ab

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(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))
        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, 0][15, 134217727]Failed
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 / f576eed36a9bc0dda1d37b18ad75277c5e639e5bcf2f7761967f19c84ef35046

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.583196+00:00.

Case digest / fb47f6d15cafd04eba0fc2a09120825ea97b39581261d8d358d7eb3cfb55acb9