Module verify 

A static check that a lowered program is well formed.

The machine takes the lowering’s word for a great deal: that a value location fits the frame it is in, that a jump lands on an instruction, that a call passes the layouts the callee declares, and — the one that matters most — that a slot’s Repr is what Function::refs says it is. A collection walks frames using that map, so a lowering that wrote a reference into a slot the map calls an Int would produce a dangling reference at the next collection and a wrong answer some time after that.

A location agrees with its layout, word for word

Every instruction that moves a value names the layout it is moving, and a layout is a run of Reprs. So the check is not “the destination is a reference” but “the destination’s words are the layout’s words, in order”. That is what makes the one-value-many-slots rule checkable: a Copy of a three-word Wrapper into a location whose second word is a Float is a fault here rather than a Float traced as a pointer later.

A width is checked, not assumed

Two of those checks are about how far a run of words reaches, and they are here because nothing downstream can make them. A value location has to fit the frame it is in — slot + width <= frame_size — or a Copy near the top of a frame reads or writes the frame above it, which was the shape of five separate failures while this backend was being built and which Memory::copy_words was left asserting about in a debug build. And a field access has to fit the object it names, which this can say wherever the object’s layout is a static fact; where it is not, the machine’s own bounds check is what answers, from the header.

This is where those assumptions are checked, once, before anything runs. It is not a type checker: cove-sema already did that, and a failure here is a bug in the lowering rather than a fault in the program. It exists so that such a bug is a loud failure at lowering time instead of a quiet one at collection time.

Structs

Invalid

A way in which a lowered program is not well formed.

Functions

verify

Checks every function of program, reporting every fault rather than the first: one lowering bug usually shows up in several places, and seeing all of them is what says which one is the cause.