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 shift instr k,
In instr f.(
Linear.fn_code) ->
Lineartyping.wt_instr f instr ->
wt_instrs k ->
wt_instrs (
transl_instr fe shift instr k).
Proof.
End TRANSL_FUNCTION.
Lemma unsigned_nneg:
forall i, 0 <=
Int.unsigned i.
Proof.
Lemma align_size_16_div:
forall sz, (
Mem.align_size sz | 16).
Proof.
intro.
unfold Mem.align_size.
repeat destruct zlt;
by apply Zmod_divide.
Qed.
Lemma wt_transf_function:
forall f tf,
transf_function f =
OK tf ->
Lineartyping.wt_function f ->
wt_function tf.
Proof.
intros.
generalize H;
unfold transf_function,
Int.lt.
case zle;
try done;
intros LT.
case zle;
try done;
intros LT'
_.
assert (
EQ :=
unfold_transf_function f tf H).
assert (
FRMPOS : 0 <=
fn_framesize tf) .
by subst tf;
eapply Zle_trans,
align_framesize_le;
pose proof (
size_pos f);
omega.
assert (
STKPOS : 0 <=
fn_paddedstacksize tf).
subst.
unfold fn_paddedstacksize,
align_stacksize.
pose proof (
align_le (
Int.unsigned (
Linear.fn_stacksize f) +
fe_retaddrsize)
(
Mem.align_size (
Int.unsigned (
Linear.fn_stacksize f)))
(
Mem.align_size_pos _)).
pose proof (
Int.unsigned_range (
Linear.fn_stacksize f)).
omega.
assert (
DIV16: (16 |
fn_paddedstacksize tf +
fn_framesize tf +
fe_retaddrsize)).
subst tf;
unfold fn_framesize,
fn_paddedstacksize in *.
set (
ssz :=
align_stacksize (
Int.unsigned (
Linear.fn_stacksize f))
fe_retaddrsize);
set (
rsz :=
fe_retaddrsize);
set (
fsz :=
fe_size (
make_env (
function_bounds f))).
unfold align_framesize.
replace (
ssz + (
align (
ssz +
rsz +
fsz) 16 -
ssz -
rsz) +
rsz)
with
(
align (
ssz +
rsz +
fsz) 16); [|
omega].
by apply align_divides.
constructor;
try done.
-
change (
wt_instrs (
fn_code tf)).
rewrite EQ;
simpl;
unfold transl_body.
apply wt_save_callee_save;
auto.
unfold transl_code.
apply wt_fold_right;
try done.
intros;
eapply wt_transl_instr;
eauto.
-
subst tf;
unfold fn_paddedstacksize,
fn_stacksize,
align_stacksize.
pose proof (
align_le (
Int.unsigned (
Linear.fn_stacksize f) +
fe_retaddrsize)
(
Mem.align_size (
Int.unsigned (
Linear.fn_stacksize f)))
(
Mem.align_size_pos _));
omega.
-
split.
pose proof (
Int.unsigned_range (
fn_stacksize tf)).
unfold fe_retaddrsize.
omega.
subst tf.
unfold fn_framesize,
fn_paddedstacksize in *.
unfold Int.min_signed in LT.
omega.
-
pose proof (
Zdivide_trans _ _ _ (
align_size_16_div
(
Int.unsigned (
fn_stacksize tf)))
DIV16)
as ASD.
assert (
STRA: (
Mem.align_size (
Int.unsigned (
fn_stacksize tf)) |
fn_paddedstacksize tf +
fe_retaddrsize)).
rewrite EQ;
unfold fn_paddedstacksize,
fn_stacksize,
align_stacksize.
rewrite Zplus_minus_l.
apply align_divides,
Mem.align_size_pos.
replace (
fn_framesize tf)
with (
fn_paddedstacksize tf +
fn_framesize tf +
fe_retaddrsize - (
fn_paddedstacksize tf +
fe_retaddrsize)); [|
omega].
eby eapply (
Zdivide_minus_l _ _ _ ASD STRA).
-
by apply Zmod_divide.
-
subst.
simpl.
unfold Int.min_signed in LT'.
omega.
Qed.
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.