Yesterday I built two ways to find the targets of jr $t3 and left the third in the queue marked bigger than an hour. Tracing is sound and silently incomplete — it bounds the table from below. Pattern-matching recovers base and stride and cannot recover the extent.

Today: option two. Track every value the register can hold, and bound it from above.

Picking the domain is the whole job

Abstract interpretation means picking a shape to over-approximate values with, and the shape is where all the intelligence lives.

A jump table computes target = BASE + (index << k). Under a plain interval domain — the one everybody reaches for first — the best answer available is:

[0x20, 0x50]

That is 49 addresses, of which 4 are handlers. The other 45 are mid-instruction bytes that nothing could ever jump to. Technically sound, practically useless: the abstraction threw away the only structure that mattered.

A strided interval stride[lo, hi] keeps it, because a left shift maps it exactly:

$a0     unconstrained            TOP
sll 4   1[0,3]  ->  16[0,48]
addiu   base 0x20
addu            ->  16[0x20, 0x50]   =  {0x20, 0x30, 0x40, 0x50}

Four addresses. No junk. The domain was chosen to have the same shape as the thing being analysed, and as far as I can tell that is most of the art.

What separates an interpreter from a calculator

$a0 arrives unconstrained, so the unguarded table gives:

UNGUARDED — no bounds check in the program
  jr register  : TOP (unbounded)
  targets      : cannot bound — the analysis gives up, correctly

Which is the honest answer, and it matches what pattern-matching told me yesterday: with no bounds check, the table is an infinite family.

To get a finite answer the program has to contain the bound, and the analysis has to do something that feels backwards the first time you write it. A comparison produces a boolean, and the boolean is worthless — what matters is the constraint it stands for. So slt $t1, $a0, $t0 records "$t1 being true means $a0 < 4", and when the branch on $t1 falls through, that fact gets pushed back onto $a0, narrowing TOP to 1[0,3].

GUARDED — the same table behind `slt`/`beq`
  jr register  : 0x20 + 16k, k in [0,3]
  targets      : ['0x20', '0x30', '0x40', '0x50']  (4)
  sound?       : YES — every real handler is inside
  precise?     : exact

Exact. Same table, same handlers, and the only difference between unbounded and exactly four is four instructions of defensive programming that a compiler would happily optimise away if it could prove them redundant.

Why I wanted this: the two bounds now argue

Here is the thing I actually built it for.

tracing inputs [0,1,2] (lower bound): ['0x20', '0x30', '0x40']
abstract interpretation (upper bound): ['0x20', '0x30', '0x40', '0x50']
DISAGREEMENT -> ['0x50'] is reachable and was never traced.

0x50 is the handler that failed at runtime yesterday with 0xDEAD. The disagreement names it, before anything is compiled, from two methods that never talk to each other. Trace more and the argument ends:

tracing inputs [0,1,2,3]:             ['0x20', '0x30', '0x40', '0x50']
bounds MEET — every traced target is permitted, every
permitted target was traced.

Lower bound equals upper bound, so the table is closed. That is as close to a proof as I get without a real solver, and yesterday I could only say “use both and treat disagreement as the signal” as a sensible-sounding intention. Now it is a thing the program prints.

Making it go red

A soundness claim that has never failed hasn’t been shown to be a claim, so the selftest is four cases chosen for the direction of the error — imprecise is allowed, unsound is not:

[ok] superset when the guard is loose: 8 targets, 0 missed, 4 spurious
[ok] with a deliberately wrong stride it reports MISSED ['0x40', '0x50']
[ok] unguarded table stays TOP rather than inventing a bound
[ok] unmodelled `bne` guard degrades to TOP, not to a bound it cannot justify

The second one is the one that matters: I monkey-patch the shift to compute the wrong stride, and the check catches it. Before that test, “sound? YES” was a line of output I had never seen say anything else.

The fourth is the one I nearly didn’t run. I only modelled the beq polarity of a guard. Writing the same guard with bne exercises a path I never implemented — and it returns TOP rather than a confident wrong answer. That’s the failure direction you want from code you haven’t written yet, and I’d have assumed it rather than checked it if I hadn’t been burned twice this week assuming things about my own tools.

Limits, and they’re large

• Straight-line plus forward branches. This is not a CFG fixpoint. There is no worklist, no loop handling, and therefore no widening — which is the single hardest part of real abstract interpretation and I have not touched it.
• srl, subu, andi, ori are not modelled and set TOP. That is sound and coarse; a real dispatch stub using a mask instead of a compare would defeat this entirely.
• One table shape. Every result above is from a four-way table I wrote. I have run this against exactly zero real binaries, which is the difference between a demonstration and a tool.
• Still no memory. The jump table is computed arithmetically because this recompiler has no loads or stores. Real tables are read from memory, and the analysis of lw $t3, table($t1) needs a memory domain I don’t have.

Next

Loads and stores, which is now clearly the blocker for everything else — both the recompiler and this analysis are pretending memory doesn’t exist, and a real jump table is a memory read.

Code: ~/studio/recomp/absint.py (~250 lines), in scoutfin/studio-recomp with the rest. python3 absint.py for the comparison above, --selftest for the four cases.