Type checking and preservation proof for LTL

[gergo-]

The main reason for the patches in this branch is to strengthen the Locmap.gss_reg lemma, which used to claim that any value can be written to and recovered from any register:

Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v.

This statement is not true if v is a 64-bit value and r is a 32-bit register. (This does not seem to allow miscompilations in practice, as there are plenty of type checks both above and below the LTL level.) The new version enforces correct typing, as for stack slots:

Lemma gss_reg: forall r v m, Val.has_type v (mreg_type r) -> (set (R r) v m)

[xavierleroy]

Some general comments. (We'll go over the code when you're back.)

• I support the new "typed" semantics for registers in LTL. It is more realistic and unifies the treatment of registers with that of stack locations.
• At first I thought the Allocation checker could be strengthened to guarantee the well-typedness of the generated LTL, without a need for an additional LTL type-checking pass. Maybe it's not true, and probably it's simpler to have the additional LTL type-checking pass. But then, are there opportunities to simplify the Allocation checker? E.g. the well_typed_move business.
• I'm on the edge concerning the non-recursive BR_splitlong. This makes it impossible to describe an int64 builtin result that would be split between a 32-bit register and a 32-bit stack location. Apparently we never need this, otherwise this PR would break. On the other hand, on the side of builtin arguments we do need this kind of description (for debugging info and for annotation builtins) and so BA_splitlong must be recursive. So we're losing some symmetry between builtin results and builtin arguments. Probably it doesn't matter.

[gergo-]

Thanks for your comments.

At first I thought the Allocation checker could be strengthened to guarantee the well-typedness of the generated LTL, without a need for an additional LTL type-checking pass.

That may be possible, I didn't try to approach it that way. The type-checking pass is convenient for reasoning of the form "if f is well-typed, then any instruction in f is well-typed". But there might be enough information in the Allocation checker to replace this.

I do use the Allocation checker where the information from the type checker is not precise enough, i.e., in the case we discussed of spills from a general register (e.g., Tany32) to a stack slot of a concrete type (e.g., Tsingle). Maybe we could generalize this and do away with the type checker completely.

I'm on the edge concerning the non-recursive BR_splitlong. This makes it impossible to describe an int64 builtin result that would be split between a 32-bit register and a 32-bit stack location.

I'm not sure this is true. BR_splitlong takes a type argument A, so a value of type BR_splitlong Locations.loc should be able to hold a register in one part and a stack slot in the other. On the other hand, on a quick skim I didn't find any occurrences of this type in the diffs, so maybe this was never actually supported? Most occurrences use mreg or preg for A, only allowing pairs of registers, excluding pairs of a register and a stack slot.