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/Renumberproof.v | 68 ++++++++++++++++++++++++------------------------- 1 file changed, 34 insertions(+), 34 deletions(-) (limited to 'backend/Renumberproof.v') diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 33d6aafa..f4d9cca3 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -67,7 +67,7 @@ Lemma find_function_translated: find_function ge ros rs = Some fd -> find_function tge ros rs = Some (transf_fundef fd). Proof. - unfold find_function; intros. destruct ros as [r|id]. + unfold find_function; intros. destruct ros as [r|id]. eapply functions_translated; eauto. rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence. eapply function_ptr_translated; eauto. @@ -87,18 +87,18 @@ Lemma renum_cfg_nodes: Proof. set (P := fun (c c': code) => forall x y i, c!x = Some i -> f!x = Some y -> c'!y = Some(renum_instr f i)). - intros c0. change (P c0 (renum_cfg f c0)). unfold renum_cfg. + intros c0. change (P c0 (renum_cfg f c0)). unfold renum_cfg. apply PTree_Properties.fold_rec; unfold P; intros. (* extensionality *) - eapply H0; eauto. rewrite H; auto. + eapply H0; eauto. rewrite H; auto. (* base *) rewrite PTree.gempty in H; congruence. (* induction *) - rewrite PTree.gsspec in H2. unfold renum_node. destruct (peq x k). - inv H2. rewrite H3. apply PTree.gss. - destruct f!k as [y'|] eqn:?. - rewrite PTree.gso. eauto. red; intros; subst y'. elim n. eapply f_inj; eauto. - eauto. + rewrite PTree.gsspec in H2. unfold renum_node. destruct (peq x k). + inv H2. rewrite H3. apply PTree.gss. + destruct f!k as [y'|] eqn:?. + rewrite PTree.gso. eauto. red; intros; subst y'. elim n. eapply f_inj; eauto. + eauto. Qed. End RENUMBER. @@ -113,9 +113,9 @@ Lemma transf_function_at: reach f pc -> (transf_function f).(fn_code)!(renum_pc (pnum f) pc) = Some(renum_instr (pnum f) i). Proof. - intros. + intros. destruct (postorder_correct (successors_map f) f.(fn_entrypoint)) as [A B]. - fold (pnum f) in *. + fold (pnum f) in *. unfold renum_pc. destruct (pnum f)! pc as [pc'|] eqn:?. simpl. eapply renum_cfg_nodes; eauto. elim (B pc); auto. unfold successors_map. rewrite PTree.gmap1. rewrite H. simpl. congruence. @@ -132,10 +132,10 @@ Lemma reach_succ: f.(fn_code)!pc = Some i -> In s (successors_instr i) -> reach f pc -> reach f s. Proof. - unfold reach; intros. econstructor; eauto. - unfold successors_map. rewrite PTree.gmap1. rewrite H. auto. + unfold reach; intros. econstructor; eauto. + unfold successors_map. rewrite PTree.gmap1. rewrite H. auto. Qed. - + Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := | match_frames_intro: forall res f sp pc rs (REACH: reach f pc), @@ -164,23 +164,23 @@ Lemma step_simulation: Proof. induction 1; intros S1' MS; inv MS; try TR_AT. (* nop *) - econstructor; split. eapply exec_Inop; eauto. - constructor; auto. eapply reach_succ; eauto. simpl; auto. + econstructor; split. eapply exec_Inop; eauto. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* op *) econstructor; split. eapply exec_Iop; eauto. - instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* load *) econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Iload; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* store *) econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* call *) @@ -204,23 +204,23 @@ Proof. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* cond *) econstructor; split. - eapply exec_Icond; eauto. + eapply exec_Icond; eauto. replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot) with (renum_pc (pnum f) (if b then ifso else ifnot)). - constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto. + constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto. destruct b; auto. (* jumptbl *) econstructor; split. - eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto. - constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto. + eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto. + constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto. (* return *) econstructor; split. - eapply exec_Ireturn; eauto. + eapply exec_Ireturn; eauto. constructor; auto. (* internal function *) simpl. econstructor; split. - eapply exec_function_internal; eauto. - constructor; auto. unfold reach. constructor. + eapply exec_function_internal; eauto. + constructor; auto. unfold reach. constructor. (* external function *) econstructor; split. eapply exec_function_external; eauto. @@ -229,8 +229,8 @@ Proof. constructor; auto. (* return *) inv STACKS. inv H1. - econstructor; split. - eapply exec_return; eauto. + econstructor; split. + eapply exec_return; eauto. constructor; auto. Qed. @@ -239,10 +239,10 @@ Lemma transf_initial_states: exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. Proof. intros. inv H. econstructor; split. - econstructor. - eapply Genv.init_mem_transf; eauto. - simpl. rewrite symbols_preserved. eauto. - eapply function_ptr_translated; eauto. + econstructor. + eapply Genv.init_mem_transf; eauto. + simpl. rewrite symbols_preserved. eauto. + eapply function_ptr_translated; eauto. rewrite <- H3; apply sig_preserved. constructor. constructor. Qed. @@ -260,14 +260,14 @@ Proof. eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. - exact step_simulation. + exact step_simulation. Qed. End PRESERVATION. - - + + -- cgit