From 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 21 May 2021 21:18:59 +0200 Subject: Now supporting Bnop insertion in conditions --- scheduling/RTLtoBTLproof.v | 151 ++++++++++++++++++--------------------------- 1 file changed, 59 insertions(+), 92 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 7ad1472b..f3e258ae 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -242,11 +242,20 @@ Proof. Qed. Lemma expand_entry_isnt_goto dupmap f pc ib: - match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None -> - is_goto (expand (entry ib) None) = false. + match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None -> + is_goto (expand (entry ib) (Bnop None)) = false. Proof. - destruct (is_goto (expand (entry ib) None))eqn:EQG; - destruct (expand (entry ib) None); + destruct (is_goto (expand (entry ib) (Bnop None))) eqn:EQG; + destruct (expand (entry ib) (Bnop None)); + try destruct fi; try discriminate; trivial. + intros; inv H; inv H5. +Qed. + +Lemma expand_entry_isnt_bnop dupmap f pc ib: + match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None -> + expand (entry ib) (Bnop None) <> Bnop None. +Proof. + destruct (expand (entry ib) (Bnop None)) eqn:EQG; try destruct fi; try discriminate; trivial. intros; inv H; inv H5. Qed. @@ -268,38 +277,23 @@ Proof. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. +Local Hint Constructors iblock_istep: core. Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1: forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1) k ofin2 rs2 m2 (CONT: match ofin1 with - | None => - (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) - \/ (exists rem, k = Some rem - /\ iblock_istep tge sp rs1 m1 rem rs2 m2 ofin2) + | None => iblock_istep tge sp rs1 m1 k rs2 m2 ofin2 | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 end), iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2. Proof. - induction 1; simpl. - { (* BF *) - intros ? ? ? ? (HRS & HM & HOF); subst. - constructor. } - (*destruct k; intros. try inv CONT.*) - 1-4: (* Bnop, Bop, Bload, Bstore *) - destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; - subst; try (inv HK; fail); try (inv HR; fail); try (econstructor; eauto; fail); - inversion HR; subst; clear HR; - eapply exec_seq_continue; [ econstructor; eauto | assumption]. - - (* Bseq_stop *) - destruct k; intros; apply IHISTEP; eauto. - - (* Bseq_continue *) - destruct ofin; intros. - + destruct CONT as [HRS [HM HOF]]; subst. - eapply IHISTEP1; right. eexists; repeat split; eauto. - + destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; subst. - * eapply IHISTEP1; right. eexists; repeat split; eauto. - eapply IHISTEP2; left; simpl; auto. - * eapply IHISTEP1; right. eexists; repeat split; eauto. + induction 1; simpl; intros; intuition subst; eauto. + { (* Bnop *) + autodestruct; intros OI; inv OI; destruct (Bnop_dec k); subst; + try (inv CONT; constructor; fail); repeat econstructor; eauto. } + 1-3: (* Bop, Bload, Bstore *) + intros; destruct (Bnop_dec k); subst; repeat econstructor; eauto; + inv CONT; econstructor; eauto. - (* Bcond *) destruct ofin; intros; econstructor; eauto; @@ -308,47 +302,19 @@ Qed. Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin -> - iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 ofin. + iblock_istep tge sp rs0 m0 (expand ib (Bnop None)) rs1 m1 ofin. Proof. intros; eapply expand_iblock_istep_rec_correct; eauto. destruct ofin; simpl; auto. Qed. -(* TODO gourdinl useless? *) -Lemma expand_iblock_istep_run_Some_rec sp ib rs0 m0 rs1 m1 ofin1: - forall (ISTEP: iblock_istep_run tge sp ib rs0 m0 = - Some {| _rs := rs1; _m := m1; _fin := ofin1 |}) - k ofin2 rs2 m2 - (CONT: match ofin1 with - | None => - (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) - \/ (exists rem, k = Some rem - /\ iblock_istep_run tge sp rem rs1 m1 = - Some {| _rs := rs2; _m := m2; _fin := ofin2 |}) - | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 - end), - iblock_istep_run tge sp (expand ib k) rs0 m0 = - Some {| _rs := rs2; _m := m2; _fin := ofin2 |}. -Proof. - intros. destruct ofin1; - rewrite <- iblock_istep_run_equiv in *. - - destruct CONT as [HRS [HM HO]]; subst. - eapply expand_iblock_istep_rec_correct; eauto. - simpl; auto. - - eapply expand_iblock_istep_rec_correct; eauto. - simpl. destruct CONT as [HL | [rem [HR ISTEP']]]. - left; auto. rewrite <- iblock_istep_run_equiv in ISTEP'. - right; eexists; split; eauto. -Qed. - Lemma expand_iblock_istep_run_None_rec sp ib: forall rs0 m0 o k (ISTEP: iblock_istep_run tge sp ib rs0 m0 = o) (CONT: match o with | Some (out rs1 m1 ofin) => - exists rem, - k = Some rem /\ ofin = None /\ - iblock_istep_run tge sp rem rs1 m1 = None + ofin = None /\ + iblock_istep_run tge sp k rs1 m1 = None | _ => True end), iblock_istep_run tge sp (expand ib k) rs0 m0 = None. @@ -357,35 +323,34 @@ Proof. try discriminate. - (* BF *) intros; destruct o; try discriminate; simpl in *. - inv ISTEP. destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO. + inv ISTEP. destruct CONT as [HO ISTEP]; inv HO. - (* Bnop *) - intros; destruct o; inv ISTEP; destruct k; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + intros; destruct o; inv ISTEP; destruct oiinfo, CONT; auto. + destruct (Bnop_dec k); subst; repeat econstructor; eauto. - (* Bop *) - intros; destruct o; - destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; destruct k; - simpl; rewrite EVAL; auto; destruct CONT as [rem [HR [HO ISTEP]]]; - inv HR; inv HO; trivial. + intros; destruct o; destruct (Bnop_dec k); + destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; + simpl; rewrite EVAL; auto; destruct CONT as [HO ISTEP]; + trivial. - (* Bload *) - intros; destruct o; + intros; destruct o; destruct (Bnop_dec k); destruct (trap) eqn:TRAP; try destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; destruct k; + try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + destruct CONT as [HO ISTEP]; trivial. - (* Bstore *) - intros; destruct o; + intros; destruct o; destruct (Bnop_dec k); destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; destruct k; + try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + destruct CONT as [HO ISTEP]; inv HO; trivial. - (* Bseq *) intros. eapply IHib1; eauto. destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto. - destruct o0. eexists; split; eauto. simpl in *. - destruct _fin; inv ISTEP. - + destruct CONT as [rem [_ [CONTRA _]]]; inv CONTRA. + destruct o0; simpl in *. destruct _fin; inv ISTEP. + + destruct CONT as [CONTRA _]; inv CONTRA. + split; auto. eapply IHib2; eauto. - (* Bcond *) intros; destruct (eval_condition _ _ _); trivial. @@ -396,7 +361,7 @@ Qed. Lemma expand_preserves_iblock_istep_run_None sp ib: forall rs m, iblock_istep_run tge sp ib rs m = None - -> iblock_istep_run tge sp (expand ib None) rs m = None. + -> iblock_istep_run tge sp (expand ib (Bnop None)) rs m = None. Proof. intros; eapply expand_iblock_istep_run_None_rec; eauto. simpl; auto. @@ -404,7 +369,7 @@ Qed. Lemma expand_preserves_iblock_istep_run sp ib: forall rs m, iblock_istep_run tge sp ib rs m = - iblock_istep_run tge sp (expand ib None) rs m. + iblock_istep_run tge sp (expand ib (Bnop None)) rs m. Proof. intros. destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP. @@ -415,28 +380,24 @@ Proof. apply expand_preserves_iblock_istep_run_None; auto. Qed. +Local Hint Constructors match_iblock: core. Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst: forall opc1 (MIB: match_iblock dupmap cfg isfst pc ib opc1) k opc2 (CONT: match opc1 with | Some pc' => - k = None /\ opc2 = opc1 \/ - (exists rem, k = Some rem - /\ match_iblock dupmap cfg false pc' rem opc2) + match_iblock dupmap cfg false pc' k opc2 | None => opc2=opc1 end), match_iblock dupmap cfg isfst pc (expand ib k) opc2. Proof. - induction 1; simpl. + induction 1; simpl; intros; eauto. { (* BF *) - intros; inv CONT; econstructor; eauto. } - 1-4: (* Bnop *) - destruct k; intros; destruct CONT as [[HK HO] | [rem [HR MIB]]]; - try inv HK; try inv HO; try inv HR; repeat econstructor; eauto. + inv CONT; econstructor; eauto. } + 1-4: (* Bnop, Bop, Bload, Bstore *) + destruct (Bnop_dec k); subst; eauto; inv CONT; econstructor; eauto. { (* Bgoto *) intros; inv CONT; apply mib_exit; auto. } - { (* Bseq *) - intros. eapply IHMIB1. right. eexists; split; eauto. } { (* Bcond *) intros. inv H0; econstructor; eauto; try econstructor. @@ -445,7 +406,7 @@ Qed. Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc: match_iblock dupmap cfg isfst pc ib opc -> - match_iblock dupmap cfg isfst pc (expand ib None) opc. + match_iblock dupmap cfg isfst pc (expand ib (Bnop None)) opc. Proof. intros. eapply expand_matchiblock_rec_correct; eauto. @@ -508,6 +469,7 @@ Proof. apply iblock_istep_run_equiv in BTL_RUN; eauto. + econstructor; apply expand_matchiblock_correct in MI. econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. econstructor. apply expand_preserves_iblock_istep_run. eapply expand_entry_isnt_goto; eauto. - (* Others *) @@ -575,7 +537,8 @@ Proof. eapply eval_builtin_args_preserved; eauto. eapply external_call_symbols_preserved; eauto. eapply senv_preserved. * econstructor; eauto; apply expand_matchiblock_correct in MI. - { econstructor; eauto. apply expand_correct; trivial. + { econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. apply star_refl. apply expand_preserves_iblock_istep_run. } eapply expand_entry_isnt_goto; eauto. + (* Bjumptable *) @@ -591,6 +554,7 @@ Proof. eapply BTL_RUN. econstructor; eauto. * econstructor; eauto; apply expand_matchiblock_correct in MI. { econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. apply star_refl. apply expand_preserves_iblock_istep_run. } eapply expand_entry_isnt_goto; eauto. - (* mib_exit *) @@ -599,7 +563,7 @@ Proof. inversion H; subst; try (inv IS_EXPD; try inv H5; discriminate; fail); inversion STEP; subst; try_simplify_someHyps; intros. - + (* Bnop *) + + (* Bnop is_rtl *) eapply match_strong_state_simu. 1,2: do 2 (econstructor; eauto). econstructor; eauto. @@ -637,7 +601,8 @@ Proof. intros; rewrite H12 in BTL_RUN. destruct b; eapply match_strong_state_simu; eauto. 1,3: inv H2; econstructor; eauto. - 1,3,5,7: inv IS_EXPD; auto; discriminate. + 1,3: inv IS_EXPD; [ inv H3; auto; inv H0 | inv H ]. + 3,5: inv IS_EXPD; [ inv H7; auto; inv H1 | inv H ]. 1-4: eapply star_right; eauto. assert (measure bnot > 0) by apply measure_pos; lia. assert (measure bso > 0) by apply measure_pos; lia. @@ -698,6 +663,7 @@ Proof. * apply expand_matchiblock_correct in MI. econstructor. econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. 3: eapply expand_entry_isnt_goto; eauto. all: erewrite preserv_fnparams; eauto. constructor. @@ -719,7 +685,8 @@ Proof. + apply expand_matchiblock_correct in MI. econstructor. econstructor; eauto. apply expand_correct; trivial. - constructor. apply expand_preserves_iblock_istep_run. + constructor. congruence. eapply expand_entry_isnt_bnop; eauto. + econstructor. apply expand_preserves_iblock_istep_run. eapply expand_entry_isnt_goto; eauto. Qed. -- cgit