Expand description
Following every value from the instruction that wrote it to the instructions that read it.
Design: spec/optimizer/39-register-allocation.md section 39.6, which asks for an independent
verifier that every use reads the value its definition produced, and spec/10-backend.md
section 10.4, which says a check like it runs in debug and CI builds.
§Why there are two checkers
crate::check reads the assignment. It asks whether the decision is one the machine can run:
whether two values that are live at once were given the same place, whether anything is sitting
in a register an instruction claims for itself, and so on. Its own module doc says what it
leaves alone, which is the rewrite, on the grounds that the assignment is the decision and the
rewrite is a transcription of it.
This is the other half. A transcription can lose a value while the decision behind it was
right, and the places it can lose one are exactly the places crate::rewrite does something:
handing out scratch registers for a value that lives on the stack, moving a value into the
register an instruction insists on, copying one operand into another for a two address form,
and putting an edge’s moves into an order that can be performed one at a time. Both #350 and
#726 were bugs in that code and neither is a shape the assignment checker can see.
§What it asks
One question. At every instruction, does each register the instruction reads hold the value the operand said it wanted.
That is asked by walking the function with a note of which value is in each place, starting from nothing at the entry block. An instruction writing an operand puts that value in the place the operand ended up naming. A move puts what is in one place into another, or takes the note away when the place it reads from held nothing known. An edge carries the block’s arguments into the block’s parameters, and what arrives is checked and then goes on under the parameter’s name, since from there on that is what the value is called.
A block with two edges into it keeps only what both of them agree about, because a value that is in one place on one path and another place on the other is not in either. That is a fixed point and it is worked out first, before anything is reported, so that a loop is not complained about on the first time round before the back edge has been seen.
§Why it is told the function twice
shape is taken before the rewrite and holds what each operand’s value was called and what
each edge carried. The rewrite is what loses both: afterwards an operand names a physical
register and an edge carries nothing. Checking a transcription means holding on to the thing
that was transcribed, and a snapshot of the operand lists is a cheaper way to do that than a
copy of the function.
§Why it repeats work
It works out where a value lives from the assignment again rather than reading it off the rewritten function, and it sequences nothing. A checker that shares its reasoning with the thing it checks agrees with it about the mistakes as well, and the bug it can never find is the one in the code they share.
It is also allowed to be slow. The state is a map from places to values and it is copied at every edge, because a checker runs in debug builds and the thing it is checking is the thing that has to be fast.
Structs§
- Shape
- What the rewrite is about to lose: what each operand’s value was called, and what each edge carries.
Enums§
- Fault
- One value read out of a place that was not holding it.