Correctness proof for the Allocation pass (translation from RTL to LTL).

Properties of allocated locations

We list here various properties of the locations alloc r, where r is an RTL pseudo-register and alloc is the register assignment returned by regalloc.

Semantic agreement between RTL registers and LTL locations

Remember the core of the code transformation performed in module Allocation: every reference to register r is replaced by a reference to location assign r. We will shortly prove the semantic equivalence between the original code and the transformed code. The key tool to do this is the following relation between a register set rs in the original RTL program and a location set ls in the transformed LTL program. The two sets agree if they assign identical values to matching registers and locations, that is, the value of register r in rs is the same as the value of location assign r in ls. However, this equality needs to hold only for live registers r. If r is dead at the current point, its value is never used later, hence the value of assign r can be arbitrary.

What follows is a long list of lemmas expressing properties of the agree_live_regs predicate that are useful for the semantic equivalence proof. First: two register sets that agree on a given set of live registers also agree on a subset of those live registers.

Some useful special cases of agree_increasing.

Agreement over a set of live registers just extended with r implies equality of the values of r and assign r.

Same, for a list of registers.

Agreement is insensitive to the current values of the temporary machine registers.

If a register is dead, assigning it an arbitrary value in rs and leaving ls unchanged preserves agreement. (This corresponds to an operation over a dead register in the original program that is turned into a no-op in the transformed program.)

Setting r to value v in rs and simultaneously setting assign r to value v in ls preserves agreement, provided that all live registers except r are mapped to locations other than that of r.

This is a special case of the previous lemma where the value v being stored is not arbitrary, but is the value of another register arg. (This corresponds to a register-register move instruction.) In this case, the condition can be weakened: it suffices that all live registers except arg and res are mapped to locations other than that of res.

Yet another special case corresponding to the case of a redundant move.

This complicated lemma states agreement between the states after a function call, provided that the states before the call agree and that calling conventions are respected.

Agreement between the initial register set at RTL function entry and the location set at LTL function entry.

Preservation of semantics

We now show that the LTL code reflecting register allocation has the same semantics as the original RTL code. We start with standard properties of translated functions and global environments in the original and translated code.

The proof of semantic preservation is a simulation argument based on diagrams of the following form:

           st1 --------------- st2
            |                   |
           t|                   |t
            |                   |
            v                   v
           st1'--------------- st2'

Hypotheses: the left vertical arrow represents a transition in the original RTL code. The top horizontal bar is the match_states relation defined below. It implies agreement between the RTL register map rs and the LTL location map ls over the pseudo-registers live before the RTL instruction at pc.

Conclusions: the right vertical arrow is an exec_instrs transition in the LTL code generated by translation of the current function. The bottom horizontal bar is the match_states relation.

The simulation proof is by case analysis over the RTL transition taken in the source program.

The semantic equivalence between the original and transformed programs follows easily.