From ca281a5ff122f136db761581f95110465b5eea31 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 18 Oct 2013 06:55:06 +0000 Subject: Revised renumbering of nodes and registers so that main function is not shifted by 1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Inliningspec.v | 116 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 84 insertions(+), 32 deletions(-) (limited to 'backend/Inliningspec.v') diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index f41f376..0fc4613 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -127,6 +127,55 @@ Proof. eapply Ple_trans. 2: eapply Pmax_r. eauto. Qed. +(** ** Properties of shifting *) + +Lemma shiftpos_eq: forall x y, Zpos (shiftpos x y) = (Zpos x + Zpos y) - 1. +Proof. + intros. unfold shiftpos. zify. rewrite Pos2Z.inj_sub. auto. + zify. omega. +Qed. + +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. + assert (Z.pos x = Z.pos y) by omega. + congruence. +Qed. + +Lemma shiftpos_diff: + forall x y n, x <> y -> shiftpos x n <> shiftpos y n. +Proof. + intros; red; intros. elim H. eapply shiftpos_inj; eauto. +Qed. + +Lemma shiftpos_above: + forall x n, Ple n (shiftpos x n). +Proof. + 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. +Qed. + +Lemma shiftpos_below: + forall x n, Plt (shiftpos x n) (Pplus x n). +Proof. + 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. +Qed. + + (** ** Working with the state monad *) Remark bind_inversion: @@ -223,7 +272,7 @@ Inductive tr_moves (c: code) : node -> list reg -> list reg -> node -> Prop := Lemma add_moves_unchanged: forall srcs dsts pc2 s pc1 s' i pc, add_moves srcs dsts pc2 s = R pc1 s' i -> - Ple pc s.(st_nextnode) \/ Plt s'.(st_nextnode) pc -> + Plt pc s.(st_nextnode) \/ Ple s'.(st_nextnode) pc -> s'.(st_code)!pc = s.(st_code)!pc. Proof. induction srcs; simpl; intros. @@ -237,7 +286,7 @@ Qed. Lemma add_moves_spec: forall srcs dsts pc2 s pc1 s' i c, add_moves srcs dsts pc2 s = R pc1 s' i -> - (forall pc, Plt s.(st_nextnode) pc -> Ple pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) -> + (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. @@ -360,7 +409,7 @@ Hypothesis rec_unchanged: forall fe' (L: (size_fenv fe' < size_fenv fe)%nat) ctx f s x s' i pc, rec fe' L ctx f s = R x s' i -> Ple ctx.(dpc) s.(st_nextnode) -> - Ple pc ctx.(dpc) -> + Plt pc ctx.(dpc) -> s'.(st_code)!pc = s.(st_code)!pc. Remark set_instr_other: @@ -385,7 +434,7 @@ Lemma expand_instr_unchanged: forall ctx pc instr s x s' i pc', expand_instr fe rec ctx pc instr s = R x s' i -> Ple ctx.(dpc) s.(st_nextnode) -> - Ple pc' s.(st_nextnode) -> + Plt pc' s.(st_nextnode) -> pc' <> spc ctx pc -> s'.(st_code)!pc' = s.(st_code)!pc'. Proof. @@ -420,7 +469,7 @@ Lemma iter_expand_instr_unchanged: forall ctx pc l s x s' i, mlist_iter2 (expand_instr fe rec ctx) l s = R x s' i -> Ple ctx.(dpc) s.(st_nextnode) -> - Ple pc s.(st_nextnode) -> + Plt pc s.(st_nextnode) -> ~In pc (List.map (spc ctx) (List.map (@fst _ _) l)) -> list_norepet (List.map (@fst _ _) l) -> s'.(st_code)!pc = s.(st_code)!pc. @@ -440,7 +489,7 @@ Lemma expand_cfg_rec_unchanged: forall ctx f s x s' i pc, expand_cfg_rec fe rec ctx f s = R x s' i -> Ple ctx.(dpc) s.(st_nextnode) -> - Ple pc ctx.(dpc) -> + Plt pc ctx.(dpc) -> s'.(st_code)!pc = s.(st_code)!pc. Proof. intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. @@ -450,7 +499,7 @@ Proof. 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. xomega. + subst pc. unfold spc in H1. eapply shiftpos_not_below; eauto. apply PTree.elements_keys_norepet. subst s0; auto. Qed. @@ -461,13 +510,13 @@ Hypothesis rec_spec: fenv_agree fe' -> Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) -> ctx.(mreg) = max_def_function f -> - Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> + Ple (Pplus ctx.(dreg) ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> ctx.(mstk) = Zmax (fn_stacksize f) 0 -> (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> - (forall pc, Plt ctx.(dpc) pc -> Ple pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) -> + (forall pc, Ple ctx.(dpc) pc -> Plt pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) -> tr_funbody ctx f c. Remark min_alignment_pos: @@ -487,11 +536,11 @@ Lemma expand_instr_spec: forall ctx pc instr s x s' i c, expand_instr fe rec ctx pc instr s = R x s' i -> Ple (max_def_instr instr) ctx.(mreg) -> - Ple (spc ctx pc) s.(st_nextnode) -> + Plt (spc ctx pc) s.(st_nextnode) -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> - (forall pc', Plt s.(st_nextnode) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> + (forall pc', Ple s.(st_nextnode) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> c!(spc ctx pc) = s'.(st_code)!(spc ctx pc) -> tr_instr ctx pc instr c. Proof. @@ -511,7 +560,8 @@ Proof. apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto. eapply BASE; eauto. eapply add_moves_spec; eauto. - intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega. + intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. + xomega. xomega. eapply rec_spec; eauto. red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto. simpl. subst s2; simpl in *; xomega. @@ -523,7 +573,7 @@ Proof. 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. + 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]. @@ -544,7 +594,7 @@ Proof. intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega. eapply rec_spec; eauto. red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto. - simpl. subst s2; simpl in *; xomega. + simpl. subst s3; simpl in *. subst s2; simpl in *. xomega. simpl. subst s3; simpl in *; xomega. simpl. xomega. simpl. apply align_divides. apply min_alignment_pos. @@ -553,7 +603,8 @@ Proof. 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. + red; simpl. +subst s2; simpl in *; xomega. red; auto. (* return *) destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. @@ -568,11 +619,11 @@ Lemma iter_expand_instr_spec: mlist_iter2 (expand_instr fe rec ctx) l s = R x s' i -> list_norepet (List.map (@fst _ _) l) -> (forall pc instr, In (pc, instr) l -> Ple (max_def_instr instr) ctx.(mreg)) -> - (forall pc instr, In (pc, instr) l -> Ple (spc ctx pc) s.(st_nextnode)) -> + (forall pc instr, In (pc, instr) l -> Plt (spc ctx pc) s.(st_nextnode)) -> Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) -> ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> - (forall pc', Plt s.(st_nextnode) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> + (forall pc', Ple s.(st_nextnode) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> (forall pc instr, In (pc, instr) l -> c!(spc ctx pc) = s'.(st_code)!(spc ctx pc)) -> forall pc instr, In (pc, instr) l -> tr_instr ctx pc instr c. Proof. @@ -582,7 +633,8 @@ 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: Ple (spc ctx pc) (st_nextnode s)) by eauto. unfold spc in B; xomega. + 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. @@ -593,18 +645,18 @@ Proof. 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 (Ple (spc ctx pc0) (st_nextnode s)) by eauto. xomega. + 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. - assert (Ple (spc ctx pc) (st_nextnode s)) by eauto. xomega. + 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. - intros [[pc0 instr0] [P Q]]. simpl in P. unfold spc in P. - assert (pc = pc0) by (unfold node; xomega). subst pc0. + 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. - intros. eapply Ple_trans; eauto. + intros. eapply Plt_le_trans. eapply H2. right; eauto. xomega. intros; eapply Ple_trans; eauto. intros. apply H7; auto. xomega. Qed. @@ -620,7 +672,7 @@ Lemma expand_cfg_rec_spec: (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> - (forall pc', Plt ctx.(dpc) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> + (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. @@ -633,14 +685,14 @@ Proof. eapply PTree.elements_complete; eauto. intros. assert (Ple pc0 (max_pc_function f)). - eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - unfold spc. subst s0; simpl; xomega. + eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. + 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. unfold spc; xomega. - assert (Ple pc0 (max_pc_function f)). - eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - unfold spc. inversion i; xomega. + 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. apply PTree.elements_correct; auto. auto. auto. auto. inversion INCR0. subst s0; simpl in STKSIZE; xomega. @@ -652,7 +704,7 @@ Lemma expand_cfg_unchanged: forall fe ctx f s x s' i pc, expand_cfg fe ctx f s = R x s' i -> Ple ctx.(dpc) s.(st_nextnode) -> - Ple pc ctx.(dpc) -> + Plt pc ctx.(dpc) -> s'.(st_code)!pc = s.(st_code)!pc. Proof. intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv). @@ -673,7 +725,7 @@ Lemma expand_cfg_spec: (min_alignment (fn_stacksize f) | ctx.(dstk)) -> ctx.(dstk) >= 0 -> s'.(st_stksize) <= stacksize -> - (forall pc', Plt ctx.(dpc) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> + (forall pc', Ple ctx.(dpc) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') -> tr_funbody ctx f c. Proof. intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv). -- cgit v1.2.3