From 30e41117b57ab20beb1876e38c26dbddc5a58dfb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 23 May 2021 20:37:22 +0200 Subject: splitting is_expand property with a weak version for conditions --- scheduling/RTLtoBTLproof.v | 114 +++++++++++++++++++++++---------------------- 1 file changed, 58 insertions(+), 56 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index f3e258ae..cd6c4dae 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -241,25 +241,34 @@ Proof. destruct fi; trivial. inv H. inv H5. Qed. -Lemma expand_entry_isnt_goto dupmap f pc ib: - match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None -> - is_goto (expand (entry ib) (Bnop None)) = false. +Lemma normRTL_entry_isnt_goto dupmap f pc ib: + match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None -> + is_goto (normRTL (entry ib) (Bnop None)) = false. Proof. - destruct (is_goto (expand (entry ib) (Bnop None))) eqn:EQG; - destruct (expand (entry ib) (Bnop None)); + destruct (is_goto (normRTL (entry ib) (Bnop None))) eqn:EQG; + destruct (normRTL (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. +Lemma normRTL_entry_isnt_bnop dupmap f pc ib: + match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None -> + normRTL (entry ib) (Bnop None) <> Bnop None. Proof. - destruct (expand (entry ib) (Bnop None)) eqn:EQG; + destruct (normRTL (entry ib) (Bnop None)) eqn:EQG; try destruct fi; try discriminate; trivial. intros; inv H; inv H5. Qed. +Lemma is_expand_normRTL_entry dupmap f ib pc + (MI : match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None): + is_expand (normRTL (entry ib) (Bnop None)). +Proof. + eapply is_wexpand_expand; eauto. + apply normRTL_correct; try congruence. + eapply normRTL_entry_isnt_bnop; eauto. +Qed. + Lemma list_nth_z_rev_dupmap: forall dupmap ln ln' (pc pc': node) val, list_nth_z ln val = Some pc -> @@ -278,14 +287,14 @@ Proof. Qed. Local Hint Constructors iblock_istep: core. -Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1: +Lemma normRTL_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 => 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. + iblock_istep tge sp rs0 m0 (normRTL ib k) rs2 m2 ofin2. Proof. induction 1; simpl; intros; intuition subst; eauto. { (* Bnop *) @@ -300,15 +309,15 @@ Proof. destruct b; eapply IHISTEP; eauto. Qed. -Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin: +Lemma normRTL_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 (Bnop None)) rs1 m1 ofin. + iblock_istep tge sp rs0 m0 (normRTL ib (Bnop None)) rs1 m1 ofin. Proof. - intros; eapply expand_iblock_istep_rec_correct; eauto. + intros; eapply normRTL_iblock_istep_rec_correct; eauto. destruct ofin; simpl; auto. Qed. -Lemma expand_iblock_istep_run_None_rec sp ib: +Lemma normRTL_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 @@ -317,7 +326,7 @@ Lemma expand_iblock_istep_run_None_rec sp ib: iblock_istep_run tge sp k rs1 m1 = None | _ => True end), - iblock_istep_run tge sp (expand ib k) rs0 m0 = None. + iblock_istep_run tge sp (normRTL ib k) rs0 m0 = None. Proof. induction ib; simpl; try discriminate. @@ -359,29 +368,29 @@ Proof. + eapply IHib2; eauto. Qed. -Lemma expand_preserves_iblock_istep_run_None sp ib: +Lemma normRTL_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 (Bnop None)) rs m = None. + -> iblock_istep_run tge sp (normRTL ib (Bnop None)) rs m = None. Proof. - intros; eapply expand_iblock_istep_run_None_rec; eauto. + intros; eapply normRTL_iblock_istep_run_None_rec; eauto. simpl; auto. Qed. -Lemma expand_preserves_iblock_istep_run sp ib: +Lemma normRTL_preserves_iblock_istep_run sp ib: forall rs m, iblock_istep_run tge sp ib rs m = - iblock_istep_run tge sp (expand ib (Bnop None)) rs m. + iblock_istep_run tge sp (normRTL ib (Bnop None)) rs m. Proof. intros. destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP. - destruct o. symmetry. rewrite <- iblock_istep_run_equiv in *. - apply expand_iblock_istep_correct; auto. + apply normRTL_iblock_istep_correct; auto. - symmetry. - apply expand_preserves_iblock_istep_run_None; auto. + apply normRTL_preserves_iblock_istep_run_None; auto. Qed. Local Hint Constructors match_iblock: core. -Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst: +Lemma normRTL_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 @@ -389,7 +398,7 @@ Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst: match_iblock dupmap cfg false pc' k opc2 | None => opc2=opc1 end), - match_iblock dupmap cfg isfst pc (expand ib k) opc2. + match_iblock dupmap cfg isfst pc (normRTL ib k) opc2. Proof. induction 1; simpl; intros; eauto. { (* BF *) @@ -404,12 +413,12 @@ Proof. destruct opc0; econstructor. } Qed. -Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc: +Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc: match_iblock dupmap cfg isfst pc ib opc -> - match_iblock dupmap cfg isfst pc (expand ib (Bnop None)) opc. + match_iblock dupmap cfg isfst pc (normRTL ib (Bnop None)) opc. Proof. intros. - eapply expand_matchiblock_rec_correct; eauto. + eapply normRTL_matchiblock_rec_correct; eauto. destruct opc; simpl; auto. Qed. @@ -467,11 +476,10 @@ Proof. eexists; left; eexists; split. + repeat econstructor; eauto. 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. + + econstructor; apply normRTL_matchiblock_correct in MI. + econstructor; eauto. eapply is_expand_normRTL_entry; eauto. + econstructor. apply normRTL_preserves_iblock_istep_run. + eapply normRTL_entry_isnt_goto; eauto. - (* Others *) exists (Some ib2); right; split. simpl; auto. @@ -536,11 +544,10 @@ Proof. pose symbols_preserved as SYMPRES. 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. - intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. - apply star_refl. apply expand_preserves_iblock_istep_run. } - eapply expand_entry_isnt_goto; eauto. + * econstructor; eauto; apply normRTL_matchiblock_correct in MI. + { econstructor; eauto. eapply is_expand_normRTL_entry; eauto. + apply star_refl. apply normRTL_preserves_iblock_istep_run. } + eapply normRTL_entry_isnt_goto; eauto. + (* Bjumptable *) exploit list_nth_z_rev_dupmap; eauto. intros (pc'0 & LNZ & DM). @@ -552,11 +559,10 @@ Proof. eexists; eexists; split. eapply iblock_istep_run_equiv in BTL_RUN. 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. + * econstructor; eauto; apply normRTL_matchiblock_correct in MI. + { econstructor; eauto. eapply is_expand_normRTL_entry; eauto. + apply star_refl. apply normRTL_preserves_iblock_istep_run. } + eapply normRTL_entry_isnt_goto; eauto. - (* mib_exit *) discriminate. - (* mib_seq *) @@ -601,8 +607,7 @@ Proof. intros; rewrite H12 in BTL_RUN. destruct b; eapply match_strong_state_simu; eauto. 1,3: inv H2; econstructor; eauto. - 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,3,5,7: inv IS_EXPD; auto; try discriminate. 1-4: eapply star_right; eauto. assert (measure bnot > 0) by apply measure_pos; lia. assert (measure bso > 0) by apply measure_pos; lia. @@ -660,14 +665,12 @@ Proof. eexists; left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. - * apply expand_matchiblock_correct in MI. + * apply normRTL_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. + eapply is_expand_normRTL_entry; eauto. + 3: eapply normRTL_entry_isnt_goto; eauto. all: erewrite preserv_fnparams; eauto. - constructor. - apply expand_preserves_iblock_istep_run. + constructor. apply normRTL_preserves_iblock_istep_run. + (* External function *) inv TRANSF. eexists; left; eexists; split. @@ -682,12 +685,11 @@ Proof. apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. eexists; left; eexists; split. + eapply exec_return. - + apply expand_matchiblock_correct in MI. + + apply normRTL_matchiblock_correct in MI. econstructor. econstructor; eauto. - apply expand_correct; trivial. - constructor. congruence. eapply expand_entry_isnt_bnop; eauto. - econstructor. apply expand_preserves_iblock_istep_run. - eapply expand_entry_isnt_goto; eauto. + eapply is_expand_normRTL_entry; eauto. + econstructor. apply normRTL_preserves_iblock_istep_run. + eapply normRTL_entry_isnt_goto; eauto. Qed. Local Hint Resolve plus_one star_refl: core. -- cgit