Type preservation for the Stacking pass.
Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import Integers.
Require Import AST.
Require Import Op.
Require Import Locations.
Require Import Conventions.
Require Import Linear.
Require Import Lineartyping.
Require Import Mach.
Require Import Machtyping.
Require Import Bounds.
Require Import Stacklayout.
Require Import Stacking.
Require Import Stackingproof.
We show that the Mach code generated by the Stacking pass
is well-typed if the original LTLin code is.
Definition wt_instrs (
k:
Mach.code) :
Prop :=
forall i,
In i k ->
wt_instr i.
Lemma wt_instrs_cons:
forall i k,
wt_instr i ->
wt_instrs k ->
wt_instrs (
i ::
k).
Proof.
unfold wt_instrs; intros. elim H1; intro.
subst i0; auto. auto.
Qed.
Section TRANSL_FUNCTION.
Variable f:
Linear.function.
Let fe :=
make_env (
function_bounds f).
Variable tf:
Mach.function.
Hypothesis TRANSF_F:
transf_function f =
OK tf.
Lemma wt_fold_right:
forall (
A:
Type) (
f:
A ->
code ->
code) (
k:
code) (
l:
list A),
(
forall x k',
In x l ->
wt_instrs k' ->
wt_instrs (
f x k')) ->
wt_instrs k ->
wt_instrs (
List.fold_right f k l).
Proof.
induction l;
intros;
simpl.
auto.
apply H.
apply in_eq.
apply IHl.
intros.
apply H.
auto with coqlib.
auto.
auto.
Qed.
Lemma wt_save_callee_save_int:
forall k,
wt_instrs k ->
wt_instrs (
save_callee_save_int fe k).
Proof.
Lemma wt_save_callee_save_float:
forall k,
wt_instrs k ->
wt_instrs (
save_callee_save_float fe k).
Proof.
Lemma wt_restore_callee_save_int:
forall k,
wt_instrs k ->
wt_instrs (
restore_callee_save_int fe k).
Proof.
Lemma wt_restore_callee_save_float:
forall k,
wt_instrs k ->
wt_instrs (
restore_callee_save_float fe k).
Proof.
Lemma wt_save_callee_save:
forall k,
wt_instrs k ->
wt_instrs (
save_callee_save fe k).
Proof.
Lemma wt_restore_callee_save:
forall k,
wt_instrs k ->
wt_instrs (
restore_callee_save fe k).
Proof.
Lemma wt_transl_instr:
forall instr k,
In instr f.(
Linear.fn_code) ->
Lineartyping.wt_instr f instr ->
wt_instrs k ->
wt_instrs (
transl_instr fe instr k).
Proof.
End TRANSL_FUNCTION.
Lemma wt_transf_function:
forall f tf,
transf_function f =
OK tf ->
Lineartyping.wt_function f ->
wt_function tf.
Proof.
Lemma wt_transf_fundef:
forall f tf,
Lineartyping.wt_fundef f ->
transf_fundef f =
OK tf ->
wt_fundef tf.
Proof.
intros f tf WT.
inversion WT;
subst.
simpl;
intros;
inversion H.
constructor.
unfold transf_fundef,
transf_partial_fundef.
caseEq (
transf_function f0);
simpl;
try congruence.
intros tfn TRANSF EQ.
inversion EQ;
subst tf.
constructor;
eapply wt_transf_function;
eauto.
Qed.
Lemma program_typing_preserved:
forall (
p:
Linear.program) (
tp:
Mach.program),
transf_program p =
OK tp ->
Lineartyping.wt_program p ->
Machtyping.wt_program tp.
Proof.