diff options
Diffstat (limited to 'backend/Reloadtyping.v')
| -rw-r--r-- | backend/Reloadtyping.v | 353 |
1 files changed, 0 insertions, 353 deletions
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v deleted file mode 100644 index 70d79bc..0000000 --- a/backend/Reloadtyping.v +++ /dev/null @@ -1,353 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Proof of type preservation for Reload and of - correctness of computation of stack bounds for Linear. *) - -Require Import Coqlib. -Require Import AST. -Require Import Op. -Require Import Locations. -Require Import LTLin. -Require Import LTLintyping. -Require Import Linear. -Require Import Lineartyping. -Require Import Conventions. -Require Import Parallelmove. -Require Import Reload. -Require Import Reloadproof. - -(** * Typing Linear constructors *) - -(** We show that the Linear constructor functions defined in [Reload] - generate well-typed instruction sequences, - given sufficient typing and well-formedness hypotheses over the locations involved. *) - -Hint Constructors wt_instr: reloadty. - -Remark wt_code_cons: - forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c). -Proof. - intros; red; simpl; intros. elim H1; intro. - subst i; auto. auto. -Qed. - -Hint Resolve wt_code_cons: reloadty. - -Definition loc_valid (f: function) (l: loc) := - match l with R _ => True | S s => slot_valid f s end. - -Lemma loc_acceptable_valid: - forall f l, loc_acceptable l -> loc_valid f l. -Proof. - destruct l; simpl; intro. auto. - destruct s; simpl. omega. tauto. tauto. -Qed. - -Definition loc_writable (l: loc) := - match l with R _ => True | S s => slot_writable s end. - -Lemma loc_acceptable_writable: - forall l, loc_acceptable l -> loc_writable l. -Proof. - destruct l; simpl; intro. auto. - destruct s; simpl; tauto. -Qed. - -Hint Resolve loc_acceptable_valid loc_acceptable_writable: reloadty. - -Definition locs_valid (f: function) (ll: list loc) := - forall l, In l ll -> loc_valid f l. -Definition locs_writable (ll: list loc) := - forall l, In l ll -> loc_writable l. - -Lemma locs_acceptable_valid: - forall f ll, locs_acceptable ll -> locs_valid f ll. -Proof. - unfold locs_acceptable, locs_valid. auto with reloadty. -Qed. - -Lemma locs_acceptable_writable: - forall ll, locs_acceptable ll -> locs_writable ll. -Proof. - unfold locs_acceptable, locs_writable. auto with reloadty. -Qed. - -Hint Resolve locs_acceptable_valid locs_acceptable_writable: reloadty. - -Lemma wt_add_reload: - forall f src dst k, - loc_valid f src -> Loc.type src = mreg_type dst -> - wt_code f k -> wt_code f (add_reload src dst k). -Proof. - intros; unfold add_reload. - destruct src; eauto with reloadty. - destruct (mreg_eq m dst); eauto with reloadty. -Qed. - -Hint Resolve wt_add_reload: reloadty. - -Lemma wt_add_reloads: - forall f srcs dsts k, - locs_valid f srcs -> map Loc.type srcs = map mreg_type dsts -> - wt_code f k -> wt_code f (add_reloads srcs dsts k). -Proof. - induction srcs; destruct dsts; simpl; intros; try congruence. - auto. inv H0. apply wt_add_reload; auto with coqlib reloadty. - apply IHsrcs; auto. red; intros; auto with coqlib. -Qed. - -Hint Resolve wt_add_reloads: reloadty. - -Lemma wt_add_spill: - forall f src dst k, - loc_valid f dst -> loc_writable dst -> Loc.type dst = mreg_type src -> - wt_code f k -> wt_code f (add_spill src dst k). -Proof. - intros; unfold add_spill. - destruct dst; eauto with reloadty. - destruct (mreg_eq src m); eauto with reloadty. -Qed. - -Hint Resolve wt_add_spill: reloadty. - -Lemma wt_add_move: - forall f src dst k, - loc_valid f src -> loc_valid f dst -> loc_writable dst -> - Loc.type dst = Loc.type src -> - wt_code f k -> wt_code f (add_move src dst k). -Proof. - intros. unfold add_move. - destruct (Loc.eq src dst); auto. - destruct src; auto with reloadty. - destruct dst; auto with reloadty. - set (tmp := match slot_type s with - | Tint => IT1 - | Tfloat => FT1 - end). - assert (mreg_type tmp = Loc.type (S s)). - simpl. destruct (slot_type s); reflexivity. - apply wt_add_reload; auto with reloadty. - apply wt_add_spill; auto. congruence. -Qed. - -Hint Resolve wt_add_move: reloadty. - -Lemma wt_add_moves: - forall f b moves, - (forall s d, In (s, d) moves -> - loc_valid f s /\ loc_valid f d /\ loc_writable d /\ Loc.type s = Loc.type d) -> - wt_code f b -> - wt_code f - (List.fold_right (fun p k => add_move (fst p) (snd p) k) b moves). -Proof. - induction moves; simpl; intros. - auto. - destruct a as [s d]. simpl. - destruct (H s d) as [A [B [C D]]]. auto. - auto with reloadty. -Qed. - -Theorem wt_parallel_move: - forall f srcs dsts b, - List.map Loc.type srcs = List.map Loc.type dsts -> - locs_valid f srcs -> locs_valid f dsts -> locs_writable dsts -> - wt_code f b -> wt_code f (parallel_move srcs dsts b). -Proof. - intros. unfold parallel_move. apply wt_add_moves; auto. - intros. - elim (parmove_prop_2 _ _ _ _ H4); intros A B. - split. destruct A as [C|[C|C]]; auto; subst s; exact I. - split. destruct B as [C|[C|C]]; auto; subst d; exact I. - split. destruct B as [C|[C|C]]; auto; subst d; exact I. - eapply parmove_prop_3; eauto. -Qed. -Hint Resolve wt_parallel_move: reloadty. - -Lemma wt_reg_for: - forall l, mreg_type (reg_for l) = Loc.type l. -Proof. - intros. destruct l; simpl. auto. - case (slot_type s); reflexivity. -Qed. -Hint Resolve wt_reg_for: reloadty. - -Lemma wt_regs_for_rec: - forall locs itmps ftmps, - enough_temporaries_rec locs itmps ftmps = true -> - (forall r, In r itmps -> mreg_type r = Tint) -> - (forall r, In r ftmps -> mreg_type r = Tfloat) -> - List.map mreg_type (regs_for_rec locs itmps ftmps) = List.map Loc.type locs. -Proof. - induction locs; intros. - simpl. auto. - simpl in H. simpl. - destruct a. - simpl. decEq. eauto. - caseEq (slot_type s); intro SLOTTYPE; rewrite SLOTTYPE in H. - destruct itmps. discriminate. - simpl. decEq. - rewrite SLOTTYPE. auto with coqlib. - apply IHlocs; auto with coqlib. - destruct ftmps. discriminate. simpl. decEq. - rewrite SLOTTYPE. auto with coqlib. - apply IHlocs; auto with coqlib. -Qed. - -Lemma wt_regs_for: - forall locs, - enough_temporaries locs = true -> - List.map mreg_type (regs_for locs) = List.map Loc.type locs. -Proof. - intros. unfold regs_for. apply wt_regs_for_rec. - auto. - simpl; intros; intuition; subst r; reflexivity. - simpl; intros; intuition; subst r; reflexivity. -Qed. -Hint Resolve wt_regs_for: reloadty. - -Hint Resolve enough_temporaries_op_args enough_temporaries_cond enough_temporaries_addr: reloadty. - -Hint Extern 4 (_ = _) => congruence : reloadty. - -Lemma wt_transf_instr: - forall f instr k, - LTLintyping.wt_instr (LTLin.fn_sig f) instr -> - wt_code (transf_function f) k -> - wt_code (transf_function f) (transf_instr f instr k). -Proof. - Opaque reg_for regs_for. - intros. inv H; simpl; auto with reloadty. - caseEq (is_move_operation op args); intros. - destruct (is_move_operation_correct _ _ H). congruence. - assert (map mreg_type (regs_for args) = map Loc.type args). - eauto with reloadty. - assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty. - auto with reloadty. - - assert (map mreg_type (regs_for args) = map Loc.type args). - eauto with reloadty. - assert (mreg_type (reg_for dst) = Loc.type dst). eauto with reloadty. - auto with reloadty. - - caseEq (enough_temporaries (src :: args)); intro ENOUGH. - caseEq (regs_for (src :: args)); intros. auto. - assert (map mreg_type (regs_for (src :: args)) = map Loc.type (src :: args)). - apply wt_regs_for. auto. - rewrite H in H5. injection H5; intros. - auto with reloadty. - apply wt_add_reloads; auto with reloadty. - symmetry. apply wt_regs_for. eauto with reloadty. - assert (op_for_binary_addressing addr <> Omove). - unfold op_for_binary_addressing; destruct addr; congruence. - assert (type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint)). - apply type_op_for_binary_addressing. - rewrite <- H1. rewrite list_length_map. - eapply not_enough_temporaries_length; eauto. - apply wt_code_cons. - constructor; auto. rewrite H5. decEq. rewrite <- H1. eauto with reloadty. - apply wt_add_reload; auto with reloadty. - apply wt_code_cons; auto. constructor. reflexivity. - rewrite <- H2. eauto with reloadty. - - assert (locs_valid (transf_function f) (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H). - destruct l; simpl; auto. destruct s; simpl; intuition. - assert (locs_writable (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H6). - destruct l; simpl; auto. destruct s; simpl; intuition. - assert (map Loc.type args = map Loc.type (loc_arguments sig)). - rewrite loc_arguments_type; auto. - assert (Loc.type res = mreg_type (loc_result sig)). - rewrite H2. unfold loc_result. unfold proj_sig_res. - destruct (sig_res sig); auto. destruct t; auto. - destruct ros. - destruct H3 as [A [B C]]. - apply wt_parallel_move; eauto with reloadty. - apply wt_add_reload; eauto with reloadty. - apply wt_code_cons; eauto with reloadty. - constructor. rewrite <- A. auto with reloadty. - auto with reloadty. - - assert (locs_valid (transf_function f) (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H). - destruct l; simpl; auto. destruct s; simpl; intuition. - assert (locs_writable (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H6). - destruct l; simpl; auto. destruct s; simpl; intuition. - assert (map Loc.type args = map Loc.type (loc_arguments sig)). - rewrite loc_arguments_type; auto. - destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. - auto 10 with reloadty. - destruct (ef_reloads ef) eqn:?. - assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence. - assert (map mreg_type (regs_for args) = map Loc.type args). - apply wt_regs_for. apply arity_ok_enough. congruence. - assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty. - auto 10 with reloadty. - auto with reloadty. - - assert (map mreg_type (regs_for args) = map Loc.type args). - eauto with reloadty. - auto with reloadty. - - assert (mreg_type (reg_for arg) = Loc.type arg). - eauto with reloadty. - auto with reloadty. - - destruct optres; simpl in *; auto with reloadty. - apply wt_add_reload; auto with reloadty. - unfold loc_result. rewrite <- H1. - destruct (Loc.type l); reflexivity. -Qed. - -Lemma wt_transf_code: - forall f c, - LTLintyping.wt_code (LTLin.fn_sig f) c -> - Lineartyping.wt_code (transf_function f) (transf_code f c). -Proof. - induction c; simpl; intros. - red; simpl; tauto. - rewrite transf_code_cons. - apply wt_transf_instr; auto with coqlib. - apply IHc. red; auto with coqlib. -Qed. - -Lemma wt_transf_fundef: - forall fd, - LTLintyping.wt_fundef fd -> - Lineartyping.wt_fundef (transf_fundef fd). -Proof. - intros. destruct fd; simpl. - inv H. inv H1. constructor. unfold wt_function. simpl. - apply wt_parallel_move; auto with reloadty. - rewrite loc_parameters_type. auto. - red; intros. - destruct (list_in_map_inv _ _ _ H) as [r [A B]]. - generalize (loc_arguments_acceptable _ _ B). - destruct r; intro. - rewrite A. simpl. auto. - red in H0. destruct s; try tauto. - simpl in A. subst l. simpl. auto. - apply wt_transf_code; auto. - constructor. -Qed. - -Lemma program_typing_preserved: - forall p, - LTLintyping.wt_program p -> - Lineartyping.wt_program (transf_program p). -Proof. - intros; red; intros. - destruct (transform_program_function _ _ _ _ H0) as [f0 [A B]]. - subst f; apply wt_transf_fundef. eauto. -Qed. |