JumpTableResolver reads a jump table over an index range VSA narrowed incorrectly

THIS MESSAGE WAS GENERATED BY AN AUTOMATED PROCESS

Description

JumpTableResolver takes the jump table's read window from the strided interval it computed for the index expression: _try_resolve_targets_load uses state.solver.min/max of the load address as the first entry and cardinality as the number of entries (angr/analyses/cfg/indirect_jump_resolvers/jumptable.py, around lines 1878-1912 and 2054-2066). When a switch is guarded by two chained modular range comparisons on the same variable, that interval is wrong in a way that is neither conservative nor detectable downstream, and the resolver reads a window that starts past the real table and runs off its end.

Two defects compound:

1. Balancer._balance_add (angr/utils/balancer.py, around 453-471) rewrites X + k ⋈ K as X ⋈ K - k without accounting for modular wrap, and a single strided interval cannot hold the wrapped result. For (c - 0x4c) & 0xff >u 0x2e the true solution set is [0, 0x4b] ∪ [0x7b, 0xff]; the balancer keeps only [0x7b, 0xff], dropping the real values and keeping a disjoint bogus range.
2. Because of (1), the next comparison -- the one that actually bounds the table -- is definitely false under the bogus interval, so SimSolver.add (angr/state_plugins/solver.py, around 702-740) returns at its if self.is_false(arg): return guard without narrowing anything and without marking the state infeasible. The stale interval survives as if the second guard did not exist.

Nothing catches the result afterwards. _is_jumptarget_legal only asks whether VEX decodes something at the address, never whether the address is an instruction boundary, and it is applied only when the target count is 1, 0x100 or 0x10000. jumptable_entries_guessed stays False, so the entries are reported as certain.

What it produces

On an x86-64 -O2 build of a coreutils-family program, a format-character switch:

0x40c1c0  lea   eax, [rbp - 0x4c]
0x40c1c3  cmp   al, 0x2e
0x40c1c5  ja    0x40c1d8
...
0x40c1d8  lea   eax, [rbp - 0x25]
0x40c1db  cmp   al, 0x53
0x40c1dd  ja    0x40c640
0x40c1e3  lea   rcx, [rip + 0x4216]        ; rcx = 0x410400, the table
0x40c1ea  movzx eax, al
0x40c1ed  movsxd rax, dword ptr [rcx + rax*4]
0x40c1f1  add   rax, rcx
0x40c1f4  notrack jmp rax

The table is at 0x410400 with at most 0x54 = 84 four-byte entries. angr resolves jumptable@0x410558 with 133 entries, jumptable_entry_size=4, entries_guessed=False: the window starts 86 entries past the base and runs into .rodata and .eh_frame. Index range believed: [0x56, 0xda]; correct: at most [0, 0x53], and [0, 0x26] once both guards are applied.

Of the 133 targets, 25 land on a real instruction boundary, 35 land strictly inside an instruction of a function whose linear disassembly consumes its symbol size exactly, and 73 are not code at all. CFGFast gives the jump 58 successors, builds blocks at 33 addresses that are not instruction boundaries, and creates a spurious function. Examples:

• 0x403d40 -- 2 bytes into the 5-byte jmp 0x403950 at 0x403d3e
• 0x403e40 -- inside the 7-byte lea rsi, [rip + 0xb857] at 0x403e3a
• 0x404000 -- inside the 7-byte lea rax, [rip + 0x110ff] at 0x403ffc
• 0x4046f0 -- inside the 5-byte mov eax, 0x80000293 at 0x4046ed
• 0x4104a3, 0x410958, 0x412148 -- .rodata and .eh_frame

The notrack prefix is not involved: pyvex lifts 3e ff e0 and ff e0 to the same IR, and the other 12 resolved tables in the same binary are all exact, their entry counts matching their guard bounds. The <= side of the very first guard in this same function narrows correctly (c ∈ [0x4c, 0x7a], 47 entries); only the > side wraps.

Reproducing without the object

The binary is from a private corpus. A maintainer can rebuild the shape with gcc or clang at -O2 from a switch on a char reached through two chained range tests, for example a printf format walker that first rejects c < '%'-relative values and then switches over a 0x54-wide window, so that the emitted code performs two lea/cmp al/ja pairs on the same value before the table load. The two guards must be modular subtractions of different constants from the same byte.

Options

The three plausible repairs are independent and a maintainer should pick:

1. Make Balancer._balance_add refuse to move a constant across a comparison when the result wraps, leaving the value unconstrained instead of narrowing it to the wrong half.
2. Make SimSolver.add treat a constraint that is definitely false under the current intervals as a signal that the intervals are wrong, rather than dropping it silently.
3. Give JumpTableResolver a sanity check the wrong window cannot pass: the address expression carries the table's base as a literal, so a window that does not start at that base is suspect, and a target that is not an instruction boundary of a symbol-sized function should not be accepted.

Environment

angr, cle, pyvex, archinfo, claripy at master as of 2026-08-13 (angr 0c293dc0, archinfo da171ca0, claripy c0b78b21, cle b58ea02a, pypcode 559aacdc, pyvex 90e9094c).