FA-90266 / Bytecode virtual machines / Open access
Switch dispatch: table indexed by key without subtracting low · case 01
Tables with a nonzero low bound select the wrong case or run off the operands.
ROOT CAUSE
The entry index uses key rather than key - low.
VERIFIED REPAIR
Index the offsets with key - low.
Unsuccessful approach: Starting the table one word early reads the high bound as the first offset.
Case contract
code is a method's bytes; at addr is tableswitch (0xAA) or lookupswitch (0xAB). After the opcode, 0-3 padding bytes align the next byte to a multiple of 4 from the method start; then big-endian signed 32-bit words: default, and either low, high and high-low+1 offsets, or npairs followed by sorted (match, offset) pairs. Branch offsets are relative to the switch opcode address. Return the target address, or ["VerifyError", reason] for low > high, negative npairs, keys not strictly increasing, another opcode, or truncated operands.
Why this case matters
Switch opcodes combine alignment, signed decoding and relative targets in one instruction.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, addr, key):
def s32(p):
v = (code[p] << 24) | (code[p + 1] << 16) | (code[p + 2] << 8) | code[p + 3]
return v - (1 << 32) if v & 0x80000000 else v
def dispatch():
op = code[addr]
p = addr + 1
p += (4 - p % 4) % 4
default = s32(p)
if op == 0xAA:
low, high = s32(p + 4), s32(p + 8)
if low > high:
return ['VerifyError', 'low>high']
if low <= key <= high:
return addr + s32(p + 12 + 4 * key)
return addr + default
if op == 0xAB:
npairs = s32(p + 4)
if npairs < 0:
return ['VerifyError', 'npairs']
pairs = [(s32(p + 8 + 8 * i), s32(p + 12 + 8 * i)) for i in range(npairs)]
if any(pairs[i][0] >= pairs[i + 1][0] for i in range(npairs - 1)):
return ['VerifyError', 'unsorted']
lo, hi = 0, npairs - 1
while lo <= hi:
mid = (lo + hi) // 2
if pairs[mid][0] == key:
return addr + pairs[mid][1]
if pairs[mid][0] < key:
lo = mid + 1
else:
hi = mid - 1
return addr + default
return ['VerifyError', 'opcode']
try:
return dispatch()
except IndexError:
return ['VerifyError', 'truncated']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
7,
0),
47),
('tableswitch hit at the high bound',
([0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
1,
1),
51),
('tableswitch hit at the low bound',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
-2),
22),
('tableswitch miss takes the backward default',
([0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
1,
5),
-7),
('lookupswitch hit with negative offset',
([0,
171,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
33,
0,
0,
0,
100,
255,
255,
255,
252,
177],
1,
100),
-3),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
33,
0,
0,
0,
100,
255,
255,
255,
252,
177],
7,
3),
19),
('lookupswitch with duplicate keys is rejected',
([0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 1, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 1, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
11,
0),
51),
('tableswitch hit at the high bound',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
1),
52),
('tableswitch hit at the low bound',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
-2),
23),
('tableswitch miss takes the backward default',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
5),
-6),
('lookupswitch hit with negative offset',
([0,
0,
171,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
34,
0,
0,
0,
100,
255,
255,
255,
252,
177],
2,
100),
-2),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
34,
0,
0,
0,
100,
255,
255,
255,
252,
177],
11,
3),
23),
('lookupswitch with duplicate keys is rejected',
([0, 0, 171, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 2, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 170, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 2, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
15,
0),
55),
('tableswitch hit at the high bound',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
1),
53),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
-2),
24),
('tableswitch miss takes the backward default',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
5),
-5),
('lookupswitch hit with negative offset',
([0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
35,
0,
0,
0,
100,
255,
255,
255,
252,
177],
3,
100),
-1),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
35,
0,
0,
0,
100,
255,
255,
255,
252,
177],
15,
3),
27),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 171, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 3, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 170, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 3, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
19,
0),
59),
('tableswitch hit at the high bound',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
1),
54),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
-2),
25),
('tableswitch miss takes the backward default',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
5),
-4),
('lookupswitch hit with negative offset',
([0,
0,
0,
0,
171,
0,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
36,
0,
0,
0,
100,
255,
255,
255,
252,
177],
4,
100),
0),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
36,
0,
0,
0,
100,
255,
255,
255,
252,
177],
19,
3),
31),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],
4,
1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 4, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
23,
0),
63),
('tableswitch hit at the high bound',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
1),
55),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
6,
-2),
26),
('tableswitch miss takes the backward default',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
5),
-3),
('lookupswitch hit with negative offset',
([0,
0,
0,
0,
0,
171,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
37,
0,
0,
0,
100,
255,
255,
255,
252,
177],
5,
100),
1),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
37,
0,
0,
0,
100,
255,
255,
255,
252,
177],
23,
3),
35),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],
5,
1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 5, 3),
['VerifyError', 'low>high'])]]
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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| regression: tableswitch hit with aligned operands | 27 | 47 | Failed |
| tableswitch hit at the high bound | 32 | 51 | Failed |
| tableswitch hit at the low bound | 0 | 22 | Failed |
| tableswitch miss takes the backward default | -7 | -7 | Passed |
| lookupswitch hit with negative offset | -3 | -3 | Passed |
| lookupswitch miss | 19 | 19 | Passed |
| lookupswitch with duplicate keys is rejected | ['VerifyError', 'unsorted'] | ['VerifyError', 'unsorted'] | Passed |
| control: low greater than high | ['VerifyError', 'low>high'] | ['VerifyError', 'low>high'] | Passed |
SHA-256 / a33dfd44daa5780e56e3458318544c11d418af2bf070982c89733ed67d1ec6a6
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, addr, key):
def s32(p):
v = (code[p] << 24) | (code[p + 1] << 16) | (code[p + 2] << 8) | code[p + 3]
return v - (1 << 32) if v & 0x80000000 else v
def dispatch():
op = code[addr]
p = addr + 1
p += (4 - p % 4) % 4
default = s32(p)
if op == 0xAA:
low, high = s32(p + 4), s32(p + 8)
if low > high:
return ['VerifyError', 'low>high']
if low <= key <= high:
return addr + s32(p + 8 + 4 * (key - low))
return addr + default
if op == 0xAB:
npairs = s32(p + 4)
if npairs < 0:
return ['VerifyError', 'npairs']
pairs = [(s32(p + 8 + 8 * i), s32(p + 12 + 8 * i)) for i in range(npairs)]
if any(pairs[i][0] >= pairs[i + 1][0] for i in range(npairs - 1)):
return ['VerifyError', 'unsorted']
lo, hi = 0, npairs - 1
while lo <= hi:
mid = (lo + hi) // 2
if pairs[mid][0] == key:
return addr + pairs[mid][1]
if pairs[mid][0] < key:
lo = mid + 1
else:
hi = mid - 1
return addr + default
return ['VerifyError', 'opcode']
try:
return dispatch()
except IndexError:
return ['VerifyError', 'truncated']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
7,
0),
47),
('tableswitch hit at the high bound',
([0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
1,
1),
51),
('tableswitch hit at the low bound',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
-2),
22),
('tableswitch miss takes the backward default',
([0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
1,
5),
-7),
('lookupswitch hit with negative offset',
([0,
171,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
33,
0,
0,
0,
100,
255,
255,
255,
252,
177],
1,
100),
-3),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
33,
0,
0,
0,
100,
255,
255,
255,
252,
177],
7,
3),
19),
('lookupswitch with duplicate keys is rejected',
([0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 1, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 1, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
11,
0),
51),
('tableswitch hit at the high bound',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
1),
52),
('tableswitch hit at the low bound',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
-2),
23),
('tableswitch miss takes the backward default',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
5),
-6),
('lookupswitch hit with negative offset',
([0,
0,
171,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
34,
0,
0,
0,
100,
255,
255,
255,
252,
177],
2,
100),
-2),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
34,
0,
0,
0,
100,
255,
255,
255,
252,
177],
11,
3),
23),
('lookupswitch with duplicate keys is rejected',
([0, 0, 171, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 2, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 170, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 2, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
15,
0),
55),
('tableswitch hit at the high bound',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
1),
53),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
-2),
24),
('tableswitch miss takes the backward default',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
5),
-5),
('lookupswitch hit with negative offset',
([0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
35,
0,
0,
0,
100,
255,
255,
255,
252,
177],
3,
100),
-1),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
35,
0,
0,
0,
100,
255,
255,
255,
252,
177],
15,
3),
27),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 171, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 3, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 170, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 3, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
19,
0),
59),
('tableswitch hit at the high bound',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
1),
54),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
-2),
25),
('tableswitch miss takes the backward default',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
5),
-4),
('lookupswitch hit with negative offset',
([0,
0,
0,
0,
171,
0,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
36,
0,
0,
0,
100,
255,
255,
255,
252,
177],
4,
100),
0),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
36,
0,
0,
0,
100,
255,
255,
255,
252,
177],
19,
3),
31),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],
4,
1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 4, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
23,
0),
63),
('tableswitch hit at the high bound',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
1),
55),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
6,
-2),
26),
('tableswitch miss takes the backward default',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
5),
-3),
('lookupswitch hit with negative offset',
([0,
0,
0,
0,
0,
171,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
37,
0,
0,
0,
100,
255,
255,
255,
252,
177],
5,
100),
1),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
37,
0,
0,
0,
100,
255,
255,
255,
252,
177],
23,
3),
35),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],
5,
1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 5, 3),
['VerifyError', 'low>high'])]]
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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| regression: tableswitch hit with aligned operands | 38 | 47 | Failed |
| tableswitch hit at the high bound | 41 | 51 | Failed |
| tableswitch hit at the low bound | 3 | 22 | Failed |
| tableswitch miss takes the backward default | -7 | -7 | Passed |
| lookupswitch hit with negative offset | -3 | -3 | Passed |
| lookupswitch miss | 19 | 19 | Passed |
| lookupswitch with duplicate keys is rejected | ['VerifyError', 'unsorted'] | ['VerifyError', 'unsorted'] | Passed |
| control: low greater than high | ['VerifyError', 'low>high'] | ['VerifyError', 'low>high'] | Passed |
SHA-256 / a75312e8f0c0c97d76f9a3b1f763af8ee04676eafe5470879118f4265c02e3cd
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, addr, key):
def s32(p):
v = (code[p] << 24) | (code[p + 1] << 16) | (code[p + 2] << 8) | code[p + 3]
return v - (1 << 32) if v & 0x80000000 else v
def dispatch():
op = code[addr]
p = addr + 1
p += (4 - p % 4) % 4
default = s32(p)
if op == 0xAA:
low, high = s32(p + 4), s32(p + 8)
if low > high:
return ['VerifyError', 'low>high']
if low <= key <= high:
return addr + s32(p + 12 + 4 * (key - low))
return addr + default
if op == 0xAB:
npairs = s32(p + 4)
if npairs < 0:
return ['VerifyError', 'npairs']
pairs = [(s32(p + 8 + 8 * i), s32(p + 12 + 8 * i)) for i in range(npairs)]
if any(pairs[i][0] >= pairs[i + 1][0] for i in range(npairs - 1)):
return ['VerifyError', 'unsorted']
lo, hi = 0, npairs - 1
while lo <= hi:
mid = (lo + hi) // 2
if pairs[mid][0] == key:
return addr + pairs[mid][1]
if pairs[mid][0] < key:
lo = mid + 1
else:
hi = mid - 1
return addr + default
return ['VerifyError', 'opcode']
try:
return dispatch()
except IndexError:
return ['VerifyError', 'truncated']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
7,
0),
47),
('tableswitch hit at the high bound',
([0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
1,
1),
51),
('tableswitch hit at the low bound',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
-2),
22),
('tableswitch miss takes the backward default',
([0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
31,
0,
0,
0,
40,
0,
0,
0,
50,
177],
1,
5),
-7),
('lookupswitch hit with negative offset',
([0,
171,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
33,
0,
0,
0,
100,
255,
255,
255,
252,
177],
1,
100),
-3),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
33,
0,
0,
0,
100,
255,
255,
255,
252,
177],
7,
3),
19),
('lookupswitch with duplicate keys is rejected',
([0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 1, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 1, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
11,
0),
51),
('tableswitch hit at the high bound',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
1),
52),
('tableswitch hit at the low bound',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
-2),
23),
('tableswitch miss takes the backward default',
([0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
32,
0,
0,
0,
40,
0,
0,
0,
50,
177],
2,
5),
-6),
('lookupswitch hit with negative offset',
([0,
0,
171,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
34,
0,
0,
0,
100,
255,
255,
255,
252,
177],
2,
100),
-2),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
34,
0,
0,
0,
100,
255,
255,
255,
252,
177],
11,
3),
23),
('lookupswitch with duplicate keys is rejected',
([0, 0, 171, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 2, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 170, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 2, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
15,
0),
55),
('tableswitch hit at the high bound',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
1),
53),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
-2),
24),
('tableswitch miss takes the backward default',
([0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
33,
0,
0,
0,
40,
0,
0,
0,
50,
177],
3,
5),
-5),
('lookupswitch hit with negative offset',
([0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
35,
0,
0,
0,
100,
255,
255,
255,
252,
177],
3,
100),
-1),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
35,
0,
0,
0,
100,
255,
255,
255,
252,
177],
15,
3),
27),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 171, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177], 3, 1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 170, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 3, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
19,
0),
59),
('tableswitch hit at the high bound',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
1),
54),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
-2),
25),
('tableswitch miss takes the backward default',
([0,
0,
0,
0,
170,
0,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
34,
0,
0,
0,
40,
0,
0,
0,
50,
177],
4,
5),
-4),
('lookupswitch hit with negative offset',
([0,
0,
0,
0,
171,
0,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
36,
0,
0,
0,
100,
255,
255,
255,
252,
177],
4,
100),
0),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
36,
0,
0,
0,
100,
255,
255,
255,
252,
177],
19,
3),
31),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],
4,
1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 4, 3),
['VerifyError', 'low>high'])],
[('regression: tableswitch hit with aligned operands',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
170,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
23,
0),
63),
('tableswitch hit at the high bound',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
1),
55),
('tableswitch hit at the low bound',
([0,
0,
0,
0,
0,
0,
170,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
6,
-2),
26),
('tableswitch miss takes the backward default',
([0,
0,
0,
0,
0,
170,
0,
0,
255,
255,
255,
248,
255,
255,
255,
254,
0,
0,
0,
1,
0,
0,
0,
20,
0,
0,
0,
35,
0,
0,
0,
40,
0,
0,
0,
50,
177],
5,
5),
-3),
('lookupswitch hit with negative offset',
([0,
0,
0,
0,
0,
171,
0,
0,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
37,
0,
0,
0,
100,
255,
255,
255,
252,
177],
5,
100),
1),
('lookupswitch miss',
([0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
171,
0,
0,
0,
12,
0,
0,
0,
4,
255,
255,
255,
251,
0,
0,
0,
16,
0,
0,
0,
0,
0,
0,
0,
24,
0,
0,
0,
7,
0,
0,
0,
37,
0,
0,
0,
100,
255,
255,
255,
252,
177],
23,
3),
35),
('lookupswitch with duplicate keys is rejected',
([0, 0, 0, 0, 0, 171, 0, 0, 0, 0, 0, 12, 0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 8, 0, 0, 0, 1, 0, 0, 0, 12, 177],
5,
1),
['VerifyError', 'unsorted']),
('control: low greater than high',
([0, 0, 0, 0, 0, 170, 0, 0, 0, 0, 0, 4, 0, 0, 0, 5, 0, 0, 0, 2, 177], 5, 3),
['VerifyError', 'low>high'])]]
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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| regression: tableswitch hit with aligned operands | 47 | 47 | Passed |
| tableswitch hit at the high bound | 51 | 51 | Passed |
| tableswitch hit at the low bound | 22 | 22 | Passed |
| tableswitch miss takes the backward default | -7 | -7 | Passed |
| lookupswitch hit with negative offset | -3 | -3 | Passed |
| lookupswitch miss | 19 | 19 | Passed |
| lookupswitch with duplicate keys is rejected | ['VerifyError', 'unsorted'] | ['VerifyError', 'unsorted'] | Passed |
| control: low greater than high | ['VerifyError', 'low>high'] | ['VerifyError', 'low>high'] | Passed |
SHA-256 / 3ca024a5f888ea848ccc327ce22beb22587cd787a9c9b40136729a35b25f744f
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:25.129107+00:00.
Case digest / b7dcfbf546c103d38294e2cde5f3b2c88b79e39bce47bf07eca7d925e14bca04