Correctness proof for the Reload pass.

Exploitation of the typing hypothesis

Reloading is applied to LTLin code that is well-typed in the sense of LTLintyping. We exploit this hypothesis to obtain information on the number of temporaries required for reloading the arguments.

Some additional properties of reg_for and regs_for.

Correctness of the Linear constructors

This section proves theorems that establish the correctness of the Linear constructor functions such as add_move. The theorems are of the general form ``the generated Linear instructions execute and modify the location set in the expected way: the result location(s) contain the expected values; other, non-temporary locations keep their values''.

Agreement between values of locations

The predicate agree states that two location maps give compatible values to all acceptable locations, that is, non-temporary registers and Local stack slots. The notion of compatibility used is the Val.lessdef ordering, which enables a Vundef value in the original program to be refined into any value in the transformed program.

A typical situation where this refinement of values occurs is at function entry point. In LTLin, all registers except those belonging to the function parameters are set to Vundef. In Linear, these registers have whatever value they had in the caller function. This difference is harmless: if the original LTLin code does not get stuck, we know that it does not use any of these Vundef values.

Preservation of labels and gotos

Semantic preservation

The match_state predicate relates states in the original LTLin program and the transformed Linear program. The main property it enforces are:

• Agreement between the values of locations in the two programs, according to the agree or agree_arguments predicates.
• Agreement between the memory states of the two programs, according to the Mem.lessdef predicate.
• Lists of LTLin instructions appearing in the source state are always suffixes of the code for the corresponding functions.
• Well-typedness of the source code, which ensures that only acceptable locations are accessed by this code.
• Agreement over return types during calls: the return type of a function is always equal to the return type of the signature of the corresponding call. This invariant is necessary since the conventional location used for passing return values depend on the return type. This invariant is enforced through the third parameter of the match_stackframes predicate, which is the signature of the called function.

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

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

It is possible for the transformed code to take no transition, remaining in the same state; for instance, if the source transition corresponds to a move instruction that was eliminated. To ensure that this cannot occur infinitely often in a row, we use the following measure function that just counts the remaining number of instructions in the source code sequence.