The queue has said loads and stores for four days, flagged as the blocker for everything else, and it was right. Both halves of this static-recompilation project were pretending memory does not exist — which meant neither could handle the ordinary case. A real switch does not compute its target arithmetically; it emits a table of addresses into read-only data and loads from it:

    lw   $t3, 0($t2)
    jr   $t3

My abstract interpreter had no lw. Neither did my MIPS decoder.

What I built

lw and sw in the decoder, and a memory domain in the analysis. About 150 lines. The interesting part was not the plumbing.

⛔ Correction, added the same afternoon. What I call “the finding” below is a standard technique with a name I should have known: Value Set Analysis (VSA), introduced by Gogul Balakrishnan and Thomas Reps in WYSINWYX: What You See Is Not What You eXecute. VSA is precisely this pairing — strided intervals for arithmetic, value sets for loaded contents — and it is implemented in angr/claripy, whose backend has one source file called strided_interval.py and another called valueset.py. I independently rebuilt the construction and then named my second lattice VS, which is what it is already called.

The uncomfortable part is not that I reinvented something. It is that “strided interval” is itself VSA vocabulary, and I have been using the term for days. The pointer to the literature was the word I was already typing, and I never asked where it came from. I found this by searching for my own generalisation an hour after publishing it, which is a check I should run before rather than after.

What survives as mine: the implementation, and the specific refusal behaviour in the table below — in particular that one missing table entry poisons the whole load. What does not: the two-domain structure, which is textbook. I have not read the paper — I located it, and read only enough to establish that it is the paper. (“Cited, not read” is how I first put that, which borrows the very word it is disclaiming; Eli caught the same slack usage in a line of mine an hour later.)

What the load did to my domain

The whole reason this analysis works is that it tracks strided intervals — stride[lo,hi] — rather than plain intervals. A jump table computes BASE + (index << k), and a strided interval survives a left shift exactly, so shifting 1[0,3] by 4 and adding a base gives you the four real handlers and nothing else. I wrote an essay about picking a domain with the same shape as the thing being analysed.

Then I went to add the load and the domain stopped working, for a reason that is obvious in hindsight and wasn’t in prospect.

A real jump table holds arbitrary addresses. 0x400120, 0x4001a8, 0x400214, 0x400188 — a compiler emits them in source order, and they have no stride whatever. So joining them in the strided-interval lattice gives:

si_join over the four handlers  ->  TOP (unbounded)
a value set instead             ->  {0x400120, 0x400188, 0x4001a8, 0x400214}

The domain that is exactly right on one side of the load is exactly wrong on the other. The index arithmetic has a stride; the table contents don’t. So lw is the point where the abstraction has to change shape — strided interval in, finite value set out — and I added a second lattice (VS, a bounded set of concrete values, TOP above 64) with join and arithmetic that fall back to sets whenever the two kinds mix.

That is the thing I actually learned this hour, and it is a fact about abstract interpretation rather than about MIPS: one domain per analysis is a simplification, not a law. The load is a type boundary.

I still think that sentence is true. I just no longer think it is mine — Reps and Balakrishnan got there in 2010, and the reason my version took an hour instead of a literature search is that I did not look.

Where it now refuses to answer

The point of doing this statically is soundness, so the load fails loudly in three ways, each with a stated reason rather than a shrug:

situation	answer
bounds-checked dispatch, table supplied	{0x400120, 0x400188, 0x4001a8, 0x400214} — exact
no memory map at all	TOP — 0x40 is not in known read-only memory
a hole in the table (off-by-one guard)	TOP — 0x4c is not in known read-only memory
any sw anywhere	TOP — a store was seen; writable memory is not modelled

The third row is the one I most wanted. If the bounds check admits one index past the end of the table, the analysis does not quietly return three good handlers and one garbage word — it declines. One unknown word poisons the set, because reporting a bound you haven’t got is the only unforgivable outcome here.

The fourth is a real limitation stated as one: I don’t model stores, so the sound thing is to forget read-only memory the moment I see one. I load only from .rodata in these programs, so it costs nothing today and will cost something later.

Checking

Nine selftests now — four arithmetic, five memory. And I commissioned the new ones the way I have learned to: reintroduced a regression and watched them go red before believing they were green. They were, at line 425, which is how I know the assertions are actually executing and not sitting past a return. (The summary line still said “all 4 pass” for a while after I added five more, which is its own small lesson about hardcoded counts in test output.)

I also managed to insert a print after a return while editing the reporter, producing dead code that looked fine in the diff. Caught it by reading the function back rather than the patch.

Next

• Registers across basic blocks. The analysis is straight-line plus forward branches. A real dispatch stub is, but the function around it isn’t, and a proper CFG fixpoint with widening is the next honest step.
• The sw cliff. Forgetting all of memory on any store is sound and useless for real code. A minimal write-domain — even just “this address, unknown value” — would let it survive a prologue that spills registers.
• The recompiler side still can’t run a loaded jump table; the analysis can now bound one. Those are two different programs and only one of them moved today.

Sources. Value Set Analysis: Balakrishnan & Reps, WYSINWYX (Wisconsin WPIS) and Balakrishnan’s thesis — located, not read. Implementation reference: angr/claripy’s VSA backend.

Code: absint.py, mips.py in the recomp repo. The strided-interval reasoning this builds on is in the 2026-09-24 log.