diff options
Diffstat (limited to 'backend/Stackingtyping.v')
| -rw-r--r-- | backend/Stackingtyping.v | 121 |
1 files changed, 59 insertions, 62 deletions
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index beb28e2..fa8a3e2 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Errors. Require Import Integers. Require Import AST. Require Import Op. @@ -11,11 +12,12 @@ Require Import Linear. Require Import Lineartyping. Require Import Mach. Require Import Machtyping. +Require Import Bounds. Require Import Stacking. Require Import Stackingproof. (** We show that the Mach code generated by the [Stacking] pass - is well-typed if the original Linear code is. *) + is well-typed if the original LTLin code is. *) Definition wt_instrs (k: Mach.code) : Prop := forall i, In i k -> wt_instr i. @@ -33,17 +35,7 @@ Section TRANSL_FUNCTION. Variable f: Linear.function. Let fe := make_env (function_bounds f). Variable tf: Mach.function. -Hypothesis TRANSF_F: transf_function f = Some tf. - -Lemma wt_Msetstack': - forall idx ty r, - mreg_type r = ty -> index_valid f idx -> - wt_instr (Msetstack r (Int.repr (offset_of_index fe idx)) ty). -Proof. - intros. constructor. auto. - unfold fe. rewrite (offset_of_index_no_overflow f tf TRANSF_F); auto. - generalize (offset_of_index_valid f idx H0). tauto. -Qed. +Hypothesis TRANSF_F: transf_function f = OK tf. Lemma wt_fold_right: forall (A: Set) (f: A -> code -> code) (k: code) (l: list A), @@ -58,51 +50,57 @@ Proof. auto. Qed. -Lemma wt_save_int_callee_save: - forall cs k, - In cs int_callee_save_regs -> wt_instrs k -> - wt_instrs (save_int_callee_save fe cs k). +Lemma wt_save_callee_save_int: + forall k, + wt_instrs k -> + wt_instrs (save_callee_save_int fe k). Proof. - intros. unfold save_int_callee_save. - case (zlt (index_int_callee_save cs) (fe_num_int_callee_save fe)); intro. + intros. unfold save_callee_save_int, save_callee_save_regs. + apply wt_fold_right; auto. + intros. unfold save_callee_save_reg. + case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro. apply wt_instrs_cons; auto. - apply wt_Msetstack'. apply int_callee_save_type; auto. - apply index_saved_int_valid. auto. exact z. + apply wt_Msetstack. apply int_callee_save_type; auto. auto. Qed. -Lemma wt_save_float_callee_save: - forall cs k, - In cs float_callee_save_regs -> wt_instrs k -> - wt_instrs (save_float_callee_save fe cs k). +Lemma wt_save_callee_save_float: + forall k, + wt_instrs k -> + wt_instrs (save_callee_save_float fe k). Proof. - intros. unfold save_float_callee_save. - case (zlt (index_float_callee_save cs) (fe_num_float_callee_save fe)); intro. + intros. unfold save_callee_save_float, save_callee_save_regs. + apply wt_fold_right; auto. + intros. unfold save_callee_save_reg. + case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro. apply wt_instrs_cons; auto. - apply wt_Msetstack'. apply float_callee_save_type; auto. - apply index_saved_float_valid. auto. exact z. + apply wt_Msetstack. apply float_callee_save_type; auto. auto. Qed. -Lemma wt_restore_int_callee_save: - forall cs k, - In cs int_callee_save_regs -> wt_instrs k -> - wt_instrs (restore_int_callee_save fe cs k). +Lemma wt_restore_callee_save_int: + forall k, + wt_instrs k -> + wt_instrs (restore_callee_save_int fe k). Proof. - intros. unfold restore_int_callee_save. - case (zlt (index_int_callee_save cs) (fe_num_int_callee_save fe)); intro. + intros. unfold restore_callee_save_int, restore_callee_save_regs. + apply wt_fold_right; auto. + intros. unfold restore_callee_save_reg. + case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro. apply wt_instrs_cons; auto. constructor. apply int_callee_save_type; auto. auto. Qed. -Lemma wt_restore_float_callee_save: - forall cs k, - In cs float_callee_save_regs -> wt_instrs k -> - wt_instrs (restore_float_callee_save fe cs k). +Lemma wt_restore_callee_save_float: + forall k, + wt_instrs k -> + wt_instrs (restore_callee_save_float fe k). Proof. - intros. unfold restore_float_callee_save. - case (zlt (index_float_callee_save cs) (fe_num_float_callee_save fe)); intro. + intros. unfold restore_callee_save_float, restore_callee_save_regs. + apply wt_fold_right; auto. + intros. unfold restore_callee_save_reg. + case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro. apply wt_instrs_cons; auto. constructor. apply float_callee_save_type; auto. auto. @@ -113,9 +111,7 @@ Lemma wt_save_callee_save: wt_instrs k -> wt_instrs (save_callee_save fe k). Proof. intros. unfold save_callee_save. - apply wt_fold_right. exact wt_save_int_callee_save. - apply wt_fold_right. exact wt_save_float_callee_save. - auto. + apply wt_save_callee_save_int. apply wt_save_callee_save_float. auto. Qed. Lemma wt_restore_callee_save: @@ -123,37 +119,34 @@ Lemma wt_restore_callee_save: wt_instrs k -> wt_instrs (restore_callee_save fe k). Proof. intros. unfold restore_callee_save. - apply wt_fold_right. exact wt_restore_int_callee_save. - apply wt_fold_right. exact wt_restore_float_callee_save. - auto. + apply wt_restore_callee_save_int. apply wt_restore_callee_save_float. auto. Qed. 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. - intros. destruct instr; unfold transl_instr; inversion H. + intros. + generalize (instr_is_within_bounds f instr H H0); intro BND. + destruct instr; unfold transl_instr; inv H0; simpl in BND. (* getstack *) - destruct s; simpl in H3; apply wt_instrs_cons; auto; + destruct BND. + destruct s; simpl in *; apply wt_instrs_cons; auto; constructor; auto. (* setstack *) - destruct s; simpl in H3; simpl in H4. - apply wt_instrs_cons; auto. apply wt_Msetstack'. auto. - apply index_local_valid. auto. + destruct s. + apply wt_instrs_cons; auto. apply wt_Msetstack. auto. auto. - apply wt_instrs_cons; auto. apply wt_Msetstack'. auto. - apply index_arg_valid. auto. + apply wt_instrs_cons; auto. apply wt_Msetstack. auto. (* op, move *) simpl. apply wt_instrs_cons. constructor; auto. auto. - (* op, undef *) - simpl. apply wt_instrs_cons. constructor. auto. (* op, others *) apply wt_instrs_cons; auto. constructor. destruct o; simpl; congruence. - destruct o; simpl; congruence. rewrite H6. destruct o; reflexivity || congruence. (* load *) apply wt_instrs_cons; auto. @@ -162,10 +155,14 @@ Proof. (* store *) apply wt_instrs_cons; auto. constructor; auto. - rewrite H3. destruct a; reflexivity. + rewrite H4. destruct a; reflexivity. (* call *) apply wt_instrs_cons; auto. constructor; auto. + (* tailcall *) + apply wt_restore_callee_save. apply wt_instrs_cons; auto. + constructor; auto. + destruct s0; auto. rewrite H5; auto. (* alloc *) apply wt_instrs_cons; auto. constructor. (* label *) @@ -185,7 +182,7 @@ End TRANSL_FUNCTION. Lemma wt_transf_function: forall f tf, - transf_function f = Some tf -> + transf_function f = OK tf -> Lineartyping.wt_function f -> wt_function tf. Proof. @@ -201,7 +198,7 @@ Proof. constructor. change (wt_instrs (fn_code tf)). rewrite H1; simpl; unfold transl_body. - apply wt_save_callee_save with tf; auto. + apply wt_save_callee_save; auto. unfold transl_code. apply wt_fold_right. intros. eapply wt_transl_instr; eauto. red; intros. elim H3. @@ -213,20 +210,20 @@ Qed. Lemma wt_transf_fundef: forall f tf, Lineartyping.wt_fundef f -> - transf_fundef f = Some tf -> + 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); try congruence. + 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 = Some tp -> + transf_program p = OK tp -> Lineartyping.wt_program p -> Machtyping.wt_program tp. Proof. |