From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- backend/Inliningspec.v | 172 ++++++++++++++++++++++++------------------------- 1 file changed, 86 insertions(+), 86 deletions(-) (limited to 'backend/Inliningspec.v') diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 161e2a6e..ba62313f 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -40,24 +40,24 @@ Remark add_globdef_compat: fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg). Proof. intros. destruct idg as [id gd]. red; simpl; intros. - unfold Genv.find_symbol in H1; simpl in H1. + unfold Genv.find_symbol in H1; simpl in H1. unfold Genv.find_funct_ptr; simpl. rewrite PTree.gsspec in H1. destruct (peq id0 id). (* same *) - subst id0. inv H1. destruct gd. destruct f0. + subst id0. inv H1. destruct gd. destruct f0. destruct (should_inline id f0). rewrite PTree.gss in H0. rewrite PTree.gss. inv H0; auto. rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. rewrite PTree.grs in H0; discriminate. (* different *) - destruct gd. rewrite PTree.gso. eapply H; eauto. + destruct gd. rewrite PTree.gso. eapply H; eauto. destruct f0. destruct (should_inline id f0). rewrite PTree.gso in H0; auto. rewrite PTree.gro in H0; auto. rewrite PTree.gro in H0; auto. red; intros; subst b. eelim Plt_strict. eapply Genv.genv_symb_range; eauto. - rewrite PTree.gro in H0; auto. eapply H; eauto. + rewrite PTree.gro in H0; auto. eapply H; eauto. Qed. Lemma funenv_program_compat: @@ -68,7 +68,7 @@ Proof. assert (forall gl ge fenv, fenv_compat ge fenv -> fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)). - induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto. + induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto. apply H. red; intros. rewrite PTree.gempty in H0; discriminate. Qed. @@ -80,12 +80,12 @@ Proof. zify. omega. Qed. -Lemma shiftpos_inj: +Lemma shiftpos_inj: forall x y n, shiftpos x n = shiftpos y n -> x = y. Proof. intros. assert (Zpos (shiftpos x n) = Zpos (shiftpos y n)) by congruence. - rewrite ! shiftpos_eq in H0. + rewrite ! shiftpos_eq in H0. assert (Z.pos x = Z.pos y) by omega. congruence. Qed. @@ -99,32 +99,32 @@ Qed. Lemma shiftpos_above: forall x n, Ple n (shiftpos x n). Proof. - intros. unfold Ple; zify. rewrite shiftpos_eq. xomega. + intros. unfold Ple; zify. rewrite shiftpos_eq. xomega. Qed. Lemma shiftpos_not_below: forall x n, Plt (shiftpos x n) n -> False. Proof. - intros. generalize (shiftpos_above x n). xomega. + intros. generalize (shiftpos_above x n). xomega. Qed. Lemma shiftpos_below: forall x n, Plt (shiftpos x n) (Pplus x n). Proof. - intros. unfold Plt; zify. rewrite shiftpos_eq. omega. + intros. unfold Plt; zify. rewrite shiftpos_eq. omega. Qed. Lemma shiftpos_le: forall x y n, Ple x y -> Ple (shiftpos x n) (shiftpos y n). Proof. - intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. omega. + intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. omega. Qed. (** ** Working with the state monad *) Remark bind_inversion: - forall (A B: Type) (f: mon A) (g: A -> mon B) + forall (A B: Type) (f: mon A) (g: A -> mon B) (y: B) (s1 s3: state) (i: sincr s1 s3), bind f g s1 = R y s3 i -> exists x, exists s2, exists i1, exists i2, @@ -156,7 +156,7 @@ Ltac monadInv H := match type of H with | (ret _ _ = R _ _ _) => monadInv1 H | (bind ?F ?G ?S = R ?X ?S' ?I) => monadInv1 H - | (?F _ _ _ _ _ _ _ _ = R _ _ _) => + | (?F _ _ _ _ _ _ _ _ = R _ _ _) => ((progress simpl in H) || unfold F in H); monadInv1 H | (?F _ _ _ _ _ _ _ = R _ _ _) => ((progress simpl in H) || unfold F in H); monadInv1 H @@ -189,7 +189,7 @@ Proof. induction l; simpl; intros. exists (sincr_refl s); auto. destruct a as [x y]. unfold bind. simpl. destruct (f x y s) as [xx s1 i1]. - destruct (IHl s1) as [i2 EQ]. rewrite EQ. econstructor; eauto. + destruct (IHl s1) as [i2 EQ]. rewrite EQ. econstructor; eauto. Qed. Lemma ptree_mfold_spec: @@ -197,7 +197,7 @@ Lemma ptree_mfold_spec: ptree_mfold f t s = R x s' i -> exists i', mlist_iter2 f (PTree.elements t) s = R tt s' i'. Proof. - intros. + intros. destruct (mlist_iter2_fold _ _ f (PTree.elements t) s) as [i' EQ]. unfold ptree_mfold in H. inv H. rewrite PTree.fold_spec. econstructor. eexact EQ. @@ -220,12 +220,12 @@ Lemma add_moves_unchanged: Plt pc s.(st_nextnode) \/ Ple s'.(st_nextnode) pc -> s'.(st_code)!pc = s.(st_code)!pc. Proof. - induction srcs; simpl; intros. + induction srcs; simpl; intros. monadInv H. auto. destruct dsts; monadInv H. auto. - transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. xomega. + transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. xomega. monadInv EQ; simpl. apply PTree.gso. - inversion INCR0; simpl in *. xomega. + inversion INCR0; simpl in *. xomega. Qed. Lemma add_moves_spec: @@ -234,15 +234,15 @@ Lemma add_moves_spec: (forall pc, Ple s.(st_nextnode) pc -> Plt pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) -> tr_moves c pc1 srcs dsts pc2. Proof. - induction srcs; simpl; intros. + induction srcs; simpl; intros. monadInv H. apply tr_moves_nil; auto. - destruct dsts; monadInv H. apply tr_moves_nil; auto. - apply tr_moves_cons with x. eapply IHsrcs; eauto. + destruct dsts; monadInv H. apply tr_moves_nil; auto. + apply tr_moves_cons with x. eapply IHsrcs; eauto. intros. inversion INCR. apply H0; xomega. monadInv EQ. - rewrite H0. erewrite add_moves_unchanged; eauto. - simpl. apply PTree.gss. - simpl. xomega. + rewrite H0. erewrite add_moves_unchanged; eauto. + simpl. apply PTree.gss. + simpl. xomega. xomega. inversion INCR; inversion INCR0; simpl in *; xomega. Qed. @@ -386,25 +386,25 @@ Proof. generalize set_instr_other; intros A. intros. unfold expand_instr in H; destruct instr; eauto. (* call *) - destruct (can_inline fe s1). eauto. + destruct (can_inline fe s1). eauto. monadInv H. unfold inline_function in EQ. monadInv EQ. - transitivity (s2.(st_code)!pc'). eauto. + transitivity (s2.(st_code)!pc'). eauto. transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto. - left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. - transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. + left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. + transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega. - simpl. monadInv EQ1; simpl. auto. + simpl. monadInv EQ1; simpl. auto. monadInv EQ; simpl. monadInv EQ1; simpl. auto. (* tailcall *) destruct (can_inline fe s1). destruct (retinfo ctx) as [[rpc rreg]|]; eauto. monadInv H. unfold inline_tail_function in EQ. monadInv EQ. - transitivity (s2.(st_code)!pc'). eauto. + transitivity (s2.(st_code)!pc'). eauto. transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto. - left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. - transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. + left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. + transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega. - simpl. monadInv EQ1; simpl. auto. + simpl. monadInv EQ1; simpl. auto. monadInv EQ; simpl. monadInv EQ1; simpl. auto. (* return *) destruct (retinfo ctx) as [[rpc rreg]|]; eauto. @@ -425,8 +425,8 @@ Proof. (* inductive case *) destruct a as [pc1 instr1]; simpl in *. monadInv H. inv H3. - transitivity ((st_code s0)!pc). - eapply IHl; eauto. destruct INCR; xomega. destruct INCR; xomega. + transitivity ((st_code s0)!pc). + eapply IHl; eauto. destruct INCR; xomega. destruct INCR; xomega. eapply expand_instr_unchanged; eauto. Qed. @@ -439,12 +439,12 @@ Lemma expand_cfg_rec_unchanged: Proof. intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. transitivity ((st_code s0)!pc). - exploit ptree_mfold_spec; eauto. intros [INCR' ITER]. - eapply iter_expand_instr_unchanged; eauto. - subst s0; auto. + exploit ptree_mfold_spec; eauto. intros [INCR' ITER]. + eapply iter_expand_instr_unchanged; eauto. + subst s0; auto. subst s0; simpl. xomega. - red; intros. exploit list_in_map_inv; eauto. intros [pc1 [A B]]. - subst pc. unfold spc in H1. eapply shiftpos_not_below; eauto. + red; intros. exploit list_in_map_inv; eauto. intros [pc1 [A B]]. + subst pc. unfold spc in H1. eapply shiftpos_not_below; eauto. apply PTree.elements_keys_norepet. subst s0; auto. Qed. @@ -456,7 +456,7 @@ Hypothesis rec_spec: Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) -> ctx.(mreg) = max_reg_function f -> Ple (Pplus ctx.(dreg) ctx.(mreg)) s.(st_nextreg) -> - ctx.(mstk) >= 0 -> + ctx.(mstk) >= 0 -> ctx.(mstk) = Zmax (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> @@ -496,14 +496,14 @@ Proof. (* call *) destruct (can_inline fe s1) as [|id f P Q]. (* not inlined *) - eapply tr_call; eauto. + eapply tr_call; eauto. (* inlined *) subst s1. monadInv EXP. unfold inline_function in EQ; monadInv EQ. set (ctx' := callcontext ctx x1 x2 (max_reg_function f) (fn_stacksize f) n r). - inversion EQ0; inversion EQ1; inversion EQ. inv_incr. + inversion EQ0; inversion EQ1; inversion EQ. inv_incr. apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto. - eapply BASE; eauto. + eapply BASE; eauto. eapply add_moves_spec; eauto. intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega. @@ -517,24 +517,24 @@ Proof. omega. intros. simpl in H. rewrite S1. transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. - eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. - red; simpl. subst s2; simpl in *. xomega. + eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. + red; simpl. subst s2; simpl in *. xomega. red; simpl. split. auto. apply align_le. apply min_alignment_pos. (* tailcall *) destruct (can_inline fe s1) as [|id f P Q]. (* not inlined *) - destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. + destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. (* turned into a call *) - eapply tr_tailcall_call; eauto. + eapply tr_tailcall_call; eauto. (* preserved *) - eapply tr_tailcall; eauto. + eapply tr_tailcall; eauto. (* inlined *) subst s1. monadInv EXP. unfold inline_function in EQ; monadInv EQ. set (ctx' := tailcontext ctx x1 x2 (max_reg_function f) (fn_stacksize f)) in *. - inversion EQ0; inversion EQ1; inversion EQ. inv_incr. + inversion EQ0; inversion EQ1; inversion EQ. inv_incr. apply tr_tailcall_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto. - eapply BASE; eauto. + eapply BASE; eauto. eapply add_moves_spec; eauto. intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega. eapply rec_spec; eauto. @@ -547,18 +547,18 @@ Proof. omega. intros. simpl in H. rewrite S1. transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. - eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. - red; simpl. + eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. + red; simpl. subst s2; simpl in *; xomega. red; auto. (* builtin *) - eapply tr_builtin; eauto. destruct b; eauto. + eapply tr_builtin; eauto. destruct b; eauto. (* return *) - destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. + destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. (* inlined *) - eapply tr_return_inlined; eauto. + eapply tr_return_inlined; eauto. (* unchanged *) - eapply tr_return; eauto. + eapply tr_return; eauto. Qed. Lemma iter_expand_instr_spec: @@ -580,29 +580,29 @@ Proof. (* inductive case *) destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. assert (A: Ple ctx.(dpc) s0.(st_nextnode)). - assert (B: Plt (spc ctx pc) (st_nextnode s)) by eauto. + assert (B: Plt (spc ctx pc) (st_nextnode s)) by eauto. unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). xomega. destruct H9. inv H. (* same pc *) eapply expand_instr_spec; eauto. omega. intros. - transitivity ((st_code s')!pc'). - apply H7. auto. xomega. - eapply iter_expand_instr_unchanged; eauto. - red; intros. rewrite list_map_compose in H9. exploit list_in_map_inv; eauto. - intros [[pc0 instr0] [P Q]]. simpl in P. + transitivity ((st_code s')!pc'). + apply H7. auto. xomega. + eapply iter_expand_instr_unchanged; eauto. + red; intros. rewrite list_map_compose in H9. exploit list_in_map_inv; eauto. + intros [[pc0 instr0] [P Q]]. simpl in P. assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. xomega. - transitivity ((st_code s')!(spc ctx pc)). - eapply H8; eauto. - eapply iter_expand_instr_unchanged; eauto. + transitivity ((st_code s')!(spc ctx pc)). + eapply H8; eauto. + eapply iter_expand_instr_unchanged; eauto. assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. xomega. - red; intros. rewrite list_map_compose in H. exploit list_in_map_inv; eauto. + red; intros. rewrite list_map_compose in H. exploit list_in_map_inv; eauto. intros [[pc0 instr0] [P Q]]. simpl in P. assert (pc = pc0) by (eapply shiftpos_inj; eauto). subst pc0. elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto. (* older pc *) - inv_incr. eapply IHl; eauto. + inv_incr. eapply IHl; eauto. intros. eapply Plt_le_trans. eapply H2. right; eauto. xomega. intros; eapply Ple_trans; eauto. intros. apply H7; auto. xomega. @@ -614,7 +614,7 @@ Lemma expand_cfg_rec_spec: Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) -> ctx.(mreg) = max_reg_function f -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> - ctx.(mstk) >= 0 -> + ctx.(mstk) >= 0 -> ctx.(mstk) = Zmax (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> @@ -622,13 +622,13 @@ Lemma expand_cfg_rec_spec: (forall pc', Ple ctx.(dpc) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> tr_funbody ctx f c. Proof. - intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. - constructor. - intros. rewrite H1. eapply max_reg_function_params; eauto. + intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. + constructor. + intros. rewrite H1. eapply max_reg_function_params; eauto. intros. exploit ptree_mfold_spec; eauto. intros [INCR' ITER]. - eapply iter_expand_instr_spec; eauto. - apply PTree.elements_keys_norepet. - intros. rewrite H1. eapply max_reg_function_def with (i := instr); eauto. + eapply iter_expand_instr_spec; eauto. + apply PTree.elements_keys_norepet. + intros. rewrite H1. eapply max_reg_function_def with (i := instr); eauto. eapply PTree.elements_complete; eauto. intros. assert (Ple pc0 (max_pc_function f)). @@ -636,10 +636,10 @@ Proof. eapply Plt_le_trans. apply shiftpos_below. subst s0; simpl; xomega. subst s0; simpl; auto. intros. apply H8; auto. subst s0; simpl in H11; xomega. - intros. apply H8. apply shiftpos_above. + intros. apply H8. apply shiftpos_above. assert (Ple pc0 (max_pc_function f)). - eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Plt_le_trans. apply shiftpos_below. inversion i; xomega. + eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. + eapply Plt_le_trans. apply shiftpos_below. inversion i; xomega. apply PTree.elements_correct; auto. auto. auto. auto. inversion INCR0. subst s0; simpl in STKSIZE; xomega. @@ -657,17 +657,17 @@ Proof. intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv). apply well_founded_ltof. intros. unfold expand_cfg in H0. rewrite unroll_Fixm in H0. - eapply expand_cfg_rec_unchanged; eauto. assumption. + eapply expand_cfg_rec_unchanged; eauto. assumption. Qed. Lemma expand_cfg_spec: forall fe ctx f s x s' i c, expand_cfg fe ctx f s = R x s' i -> - fenv_agree fe -> + fenv_agree fe -> Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) -> ctx.(mreg) = max_reg_function f -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> - ctx.(mstk) >= 0 -> + ctx.(mstk) >= 0 -> ctx.(mstk) = Zmax (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> @@ -678,7 +678,7 @@ Proof. intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv). apply well_founded_ltof. intros. unfold expand_cfg in H0. rewrite unroll_Fixm in H0. - eapply expand_cfg_rec_spec; eauto. + eapply expand_cfg_rec_spec; eauto. simpl. intros. eapply expand_cfg_unchanged; eauto. assumption. Qed. @@ -701,7 +701,7 @@ Lemma transf_function_spec: forall f f', transf_function fenv f = OK f' -> tr_function f f'. Proof. intros. unfold transf_function in H. - destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. + destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. destruct (zlt (st_stksize s) Int.max_unsigned); inv H. monadInv Heqr. set (ctx := initcontext x x0 (max_reg_function f) (fn_stacksize f)) in *. Opaque initstate. @@ -712,11 +712,11 @@ Opaque initstate. unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega. unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega. simpl. xomega. - simpl. apply Zdivide_0. + simpl. apply Zdivide_0. simpl. omega. simpl. omega. - simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. - simpl. change 0 with (st_stksize initstate). omega. + simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. + simpl. change 0 with (st_stksize initstate). omega. Qed. End INLINING_SPEC. -- cgit