From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/Lineartyping.v | 70 +++++++++++++++++++++++++------------------------- 1 file changed, 35 insertions(+), 35 deletions(-) (limited to 'backend/Lineartyping.v') diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 62a0c585..a52e47bb 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -72,7 +72,7 @@ Definition wt_instr (i: instruction) : bool := match is_move_operation op args with | Some arg => subtype (mreg_type arg) (mreg_type res) - | None => + | None => let (targs, tres) := type_of_operation op in subtype tres (mreg_type res) end @@ -105,7 +105,7 @@ Lemma wt_setreg: Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls). Proof. intros; red; intros. - unfold Locmap.set. + unfold Locmap.set. destruct (Loc.eq (R r) l). subst l; auto. destruct (Loc.diff_dec (R r) l). auto. red. auto. @@ -116,10 +116,10 @@ Lemma wt_setstack: wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls). Proof. intros; red; intros. - unfold Locmap.set. + unfold Locmap.set. destruct (Loc.eq (S sl ofs ty) l). - subst l. simpl. - generalize (Val.load_result_type (chunk_of_type ty) v). + subst l. simpl. + generalize (Val.load_result_type (chunk_of_type ty) v). replace (type_of_chunk (chunk_of_type ty)) with ty. auto. destruct ty; reflexivity. destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto. @@ -164,7 +164,7 @@ Lemma wt_setlist: Proof. induction vl; destruct rl; simpl; intros; try contradiction. auto. - destruct H. apply IHvl; auto. apply wt_setreg; auto. + destruct H. apply IHvl; auto. apply wt_setreg; auto. Qed. Lemma wt_setres: @@ -177,7 +177,7 @@ Proof. induction res; simpl; intros. - apply wt_setreg; auto. eapply Val.has_subtype; eauto. - auto. -- InvBooleans. eapply IHres2; eauto. destruct v; exact I. +- InvBooleans. eapply IHres2; eauto. destruct v; exact I. eapply IHres1; eauto. destruct v; exact I. Qed. @@ -189,7 +189,7 @@ Lemma wt_find_label: Proof. unfold wt_function; intros until c. generalize (fn_code f). induction c0; simpl; intros. discriminate. - InvBooleans. destruct (is_label lbl a). + InvBooleans. destruct (is_label lbl a). congruence. auto. Qed. @@ -250,15 +250,15 @@ Hypothesis wt_prog: Lemma wt_find_function: forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f. Proof. - intros. + intros. assert (X: exists i, In (i, Gfun f) prog.(prog_defs)). { destruct ros as [r | s]; simpl in H. - eapply Genv.find_funct_inversion; eauto. + eapply Genv.find_funct_inversion; eauto. destruct (Genv.find_symbol ge s) as [b|]; try discriminate. eapply Genv.find_funct_ptr_inversion; eauto. } - destruct X as [i IN]. eapply wt_prog; eauto. + destruct X as [i IN]. eapply wt_prog; eauto. Qed. Theorem step_type_preservation: @@ -266,38 +266,38 @@ Theorem step_type_preservation: Proof. induction 1; intros WTS; inv WTS. - (* getstack *) - simpl in *; InvBooleans. + simpl in *; InvBooleans. econstructor; eauto. - eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS. + eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS. apply wt_undef_regs; auto. - (* setstack *) - simpl in *; InvBooleans. + simpl in *; InvBooleans. econstructor; eauto. apply wt_setstack. apply wt_undef_regs; auto. - (* op *) simpl in *. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE. + (* move *) - InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. + InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. simpl in H. inv H. - econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS. + econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS. apply wt_undef_regs; auto. - + (* other ops *) + + (* other ops *) destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans. econstructor; eauto. - apply wt_setreg; auto. eapply Val.has_subtype; eauto. - change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. - red; intros; subst op. simpl in ISMOVE. - destruct args; try discriminate. destruct args; discriminate. + apply wt_setreg; auto. eapply Val.has_subtype; eauto. + change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. + red; intros; subst op. simpl in ISMOVE. + destruct args; try discriminate. destruct args; discriminate. apply wt_undef_regs; auto. - (* load *) - simpl in *; InvBooleans. + simpl in *; InvBooleans. econstructor; eauto. - apply wt_setreg. eapply Val.has_subtype; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. apply wt_undef_regs; auto. - (* store *) - simpl in *; InvBooleans. - econstructor. eauto. eauto. eauto. + simpl in *; InvBooleans. + econstructor. eauto. eauto. eauto. apply wt_undef_regs; auto. - (* call *) simpl in *; InvBooleans. @@ -305,35 +305,35 @@ Proof. eapply wt_find_function; eauto. - (* tailcall *) simpl in *; InvBooleans. - econstructor; eauto. + econstructor; eauto. eapply wt_find_function; eauto. - apply wt_return_regs; auto. apply wt_parent_locset; auto. + apply wt_return_regs; auto. apply wt_parent_locset; auto. - (* builtin *) simpl in *; InvBooleans. econstructor; eauto. - eapply wt_setres; eauto. eapply external_call_well_typed; eauto. + eapply wt_setres; eauto. eapply external_call_well_typed; eauto. apply wt_undef_regs; auto. - (* label *) simpl in *. econstructor; eauto. - (* goto *) - simpl in *. econstructor; eauto. eapply wt_find_label; eauto. + simpl in *. econstructor; eauto. eapply wt_find_label; eauto. - (* cond branch, taken *) simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto. apply wt_undef_regs; auto. - (* cond branch, not taken *) - simpl in *. econstructor. auto. auto. auto. + simpl in *. econstructor. auto. auto. auto. apply wt_undef_regs; auto. - (* jumptable *) simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto. apply wt_undef_regs; auto. - (* return *) - simpl in *. InvBooleans. + simpl in *. InvBooleans. econstructor; eauto. apply wt_return_regs; auto. apply wt_parent_locset; auto. - (* internal function *) simpl in WTFD. econstructor. eauto. eauto. eauto. - apply wt_undef_regs. apply wt_call_regs. auto. + apply wt_undef_regs. apply wt_call_regs. auto. - (* external function *) econstructor. auto. apply wt_setlist; auto. eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto. @@ -344,7 +344,7 @@ Qed. Theorem wt_initial_state: forall S, initial_state prog S -> wt_state S. Proof. - induction 1. econstructor. constructor. + induction 1. econstructor. constructor. unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto. intros [id IN]. eapply wt_prog; eauto. apply wt_init. @@ -383,7 +383,7 @@ Lemma wt_state_builtin: wt_state (State s f sp (Lbuiltin ef args res :: c) rs m) -> forallb (loc_valid f) (params_of_builtin_args args) = true. Proof. - intros. inv H. simpl in WTC; InvBooleans. auto. + intros. inv H. simpl in WTC; InvBooleans. auto. Qed. Lemma wt_callstate_wt_regs: @@ -391,5 +391,5 @@ Lemma wt_callstate_wt_regs: wt_state (Callstate s f rs m) -> forall r, Val.has_type (rs (R r)) (mreg_type r). Proof. - intros. inv H. apply WTRS. + intros. inv H. apply WTRS. Qed. -- cgit