From 51ec982b84851ac3526a0cb3f22e41f974b2d592 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 24 May 2021 22:41:35 +0200 Subject: tiny simplifications in RTLtoBTLproof --- scheduling/RTLtoBTLproof.v | 599 ++++++++++++++++++++++++++------------------- 1 file changed, 341 insertions(+), 258 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index cd6c4dae..7cd8e47d 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -6,6 +6,269 @@ Require Import Errors Linking RTLtoBTL. Require Import Linking. +(** * Normalization of BTL iblock for simulation of RTL + +Below [normRTL] normalizes the representation of BTL blocks, +in order to represent as sequences of RTL instructions. + +This eases the + +*) + +Definition is_RTLatom (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false + | _ => true + end. + +Definition is_RTLbasic (ib: iblock): bool := + match ib with + | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None | BF _ _ => false + | _ => true + end. + + +Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }. +Proof. + destruct k; simpl; try destruct oiinfo; + intuition congruence. +Defined. + +(** The strict [is_normRTL] property specifying the ouput of [normRTL] below *) +Inductive is_normRTL: iblock -> Prop := + | norm_Bseq ib1 ib2: + is_RTLbasic ib1 = true -> + is_normRTL ib2 -> + is_normRTL (Bseq ib1 ib2) + | norm_Bcond cond args ib1 ib2 i: + is_normRTL ib1 -> + is_normRTL ib2 -> + is_normRTL (Bcond cond args ib1 ib2 i) + | norm_others ib: + is_RTLatom ib = true -> + is_normRTL ib + . +Local Hint Constructors is_normRTL: core. + +(** Weaker version with less restrictive hypothesis for conditions *) +Inductive is_wnormRTL: iblock -> Prop := + | wnorm_Bseq ib1 ib2: + is_RTLbasic ib1 = true -> + is_wnormRTL ib2 -> + is_wnormRTL (Bseq ib1 ib2) + | wnorm_Bcond cond args ib1 ib2 iinfo: + (ib1 <> Bnop None -> is_wnormRTL ib1) -> + (ib2 <> Bnop None -> is_wnormRTL ib2) -> + is_wnormRTL (Bcond cond args ib1 ib2 iinfo) + | wnorm_others ib: + is_RTLatom ib = true -> + is_wnormRTL ib + . +Local Hint Constructors is_wnormRTL: core. + +(* NB: [k] is a "continuation" (e.g. semantically [normRTLrec ib k] is like [BSeq ib k]) *) +Fixpoint normRTLrec (ib: iblock) (k: iblock): iblock := + match ib with + | Bseq ib1 ib2 => normRTLrec ib1 (normRTLrec ib2 k) + | Bcond cond args ib1 ib2 iinfo => + Bcond cond args (normRTLrec ib1 k) (normRTLrec ib2 k) iinfo + | BF fin iinfo => BF fin iinfo + | Bnop None => k + | ib => + if Bnop_dec k then ib else Bseq ib k + end. + +Definition normRTL ib := normRTLrec ib (Bnop None). + +Lemma normRTLrec_wcorrect ib: forall k, + (k <> (Bnop None) -> is_wnormRTL k) -> + (normRTLrec ib k) <> Bnop None -> + is_wnormRTL (normRTLrec ib k). +Proof. + induction ib; simpl; intros; repeat autodestruct; auto. +Qed. + +Lemma normRTL_wcorrect ib: + (normRTL ib) <> Bnop None -> + is_wnormRTL (normRTL ib). +Proof. + intros; eapply normRTLrec_wcorrect; eauto. +Qed. + +Lemma is_join_opt_None {A} (opc1 opc2: option A): + is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None. +Proof. + intros X. inv X; auto. +Qed. + +Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: + match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None. +Proof. + intros X; inv X; try congruence. +Qed. +Local Hint Resolve match_iblock_None_not_Bnop: core. + +Lemma is_wnormRTL_normRTL dupmap cfg ib: + is_wnormRTL ib -> + forall isfst pc + (MIB: match_iblock dupmap cfg isfst pc ib None), + is_normRTL ib. +Proof. + induction 1; simpl; intros; auto; try (inv MIB); eauto. + (* Bcond *) + destruct (is_join_opt_None opc1 opc2); subst; eauto. + econstructor; eauto. +Qed. + +Local Hint Constructors iblock_istep: core. +Lemma normRTLrec_iblock_istep_correct tge 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 (normRTLrec ib k) rs2 m2 ofin2. +Proof. + 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; + destruct b; eapply IHISTEP; eauto. +Qed. + +Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin: + iblock_istep tge sp rs0 m0 ib rs1 m1 ofin -> + iblock_istep tge sp rs0 m0 (normRTL ib) rs1 m1 ofin. +Proof. + intros; eapply normRTLrec_iblock_istep_correct; eauto. + destruct ofin; simpl; auto. +Qed. + +Lemma normRTLrec_iblock_istep_run_None tge 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) => + ofin = None /\ + iblock_istep_run tge sp k rs1 m1 = None + | _ => True + end), + iblock_istep_run tge sp (normRTLrec ib k) rs0 m0 = None. +Proof. + induction ib; simpl; + try discriminate. + - (* BF *) + intros; destruct o; try discriminate; simpl in *. + inv ISTEP. destruct CONT as [HO ISTEP]; inv HO. + - (* Bnop *) + intros; destruct o; inv ISTEP; destruct oiinfo, CONT; auto. + destruct (Bnop_dec k); subst; repeat econstructor; eauto. + - (* Bop *) + 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; destruct (Bnop_dec k); + destruct (trap) eqn:TRAP; + try destruct (eval_addressing _ _ _ _) eqn:EVAL; + try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; + simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; + destruct CONT as [HO ISTEP]; trivial. + - (* Bstore *) + intros; destruct o; destruct (Bnop_dec k); + destruct (eval_addressing _ _ _ _) eqn:EVAL; + try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; + simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; + 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; simpl in *. destruct _fin; inv ISTEP. + + destruct CONT as [CONTRA _]; inv CONTRA. + + split; auto. eapply IHib2; eauto. + - (* Bcond *) + intros; destruct (eval_condition _ _ _); trivial. + destruct b. + + eapply IHib1; eauto. + + eapply IHib2; eauto. +Qed. + +Lemma normRTL_preserves_iblock_istep_run_None tge sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = None + -> iblock_istep_run tge sp (normRTL ib) rs m = None. +Proof. + intros; eapply normRTLrec_iblock_istep_run_None; eauto. + simpl; auto. +Qed. + +Lemma normRTL_preserves_iblock_istep_run tge sp ib: + forall rs m, iblock_istep_run tge sp ib rs m = + iblock_istep_run tge sp (normRTL ib) 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 normRTL_iblock_istep_correct; auto. + - symmetry. + apply normRTL_preserves_iblock_istep_run_None; auto. +Qed. + +Local Hint Constructors match_iblock: core. +Lemma normRTLrec_matchiblock_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' => + match_iblock dupmap cfg false pc' k opc2 + | None => opc2=opc1 + end), + match_iblock dupmap cfg isfst pc (normRTLrec ib k) opc2. +Proof. + induction 1; simpl; intros; eauto. + { (* BF *) + 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. } + { (* Bcond *) + intros. inv H0; + econstructor; eauto; try econstructor. + destruct opc0; econstructor. } +Qed. + +Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc: + match_iblock dupmap cfg isfst pc ib opc -> + match_iblock dupmap cfg isfst pc (normRTL ib) opc. +Proof. + intros. + eapply normRTLrec_matchiblock_correct; eauto. + destruct opc; simpl; auto. +Qed. + +Lemma is_normRTL_correct dupmap cfg ib pc + (MI : match_iblock dupmap cfg true pc ib None): + is_normRTL (normRTL ib). +Proof. + exploit normRTL_matchiblock_correct; eauto. + intros MI2. + eapply is_wnormRTL_normRTL; eauto. + apply normRTL_wcorrect; try congruence. + inv MI2; discriminate. +Qed. + +(** * Matching relation on functions *) + Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f); dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f); @@ -106,7 +369,7 @@ Inductive match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 (ATpc0: (fn_code f')!pcB0 = Some ib0) (DUPLIC: dupmap!pcB0 = Some pcR0) (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None) - (IS_EXPD: is_expand ib) + (IS_EXPD: is_normRTL ib) (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs1 m1)) (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs1 m1) : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst @@ -231,43 +494,30 @@ Proof. induction ib; simpl; auto; lia. Qed. -(* TODO gourdinl remove useless lemma? *) -Lemma entry_isnt_goto dupmap f pc ib: - match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None -> - is_goto (entry ib) = false. +Lemma match_iblock_true_isnt_goto dupmap cfg pc ib opc: + match_iblock dupmap cfg true pc ib opc -> + is_goto ib = false. Proof. - intros. - destruct (entry ib); trivial. - destruct fi; trivial. inv H. inv H5. + intros MIB; inversion MIB as [d1 d2 d3 d4 d5 H H0| | | | | | | |]; subst; simpl; try congruence. + inv H0; congruence. Qed. -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. +Local Hint Resolve match_iblock_true_isnt_goto normRTL_preserves_iblock_istep_run star_refl star_right: core. +Local Hint Constructors match_strong_state RTL.step: core. + +(** At entry in a block: we init [match_states] on [normRTL] to normalize the block *) +Lemma match_states_entry dupmap st f sp pc ib rs m st' f' pc' + (STACKS : list_forall2 match_stackframes st st') + (TRANSF : match_function dupmap f f') + (FN : (fn_code f') ! pc' = Some ib) + (MI : match_iblock dupmap (RTL.fn_code f) true pc (entry ib) None) + (DUP : dupmap ! pc' = Some pc): + match_states (Some (normRTL (entry ib))) (RTL.State st f sp pc rs m) (State st' f' sp pc' rs m). Proof. - 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 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 (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. + exploit is_normRTL_correct; eauto. + econstructor; eauto; apply normRTL_matchiblock_correct in MI; eauto. Qed. +Local Hint Resolve match_states_entry: core. Lemma list_nth_z_rev_dupmap: forall dupmap ln ln' (pc pc': node) val, @@ -286,141 +536,6 @@ Proof. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. -Local Hint Constructors iblock_istep: core. -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 (normRTL ib k) rs2 m2 ofin2. -Proof. - 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; - destruct b; eapply IHISTEP; eauto. -Qed. - -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 (normRTL ib (Bnop None)) rs1 m1 ofin. -Proof. - intros; eapply normRTL_iblock_istep_rec_correct; eauto. - destruct ofin; simpl; auto. -Qed. - -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 - | Some (out rs1 m1 ofin) => - ofin = None /\ - iblock_istep_run tge sp k rs1 m1 = None - | _ => True - end), - iblock_istep_run tge sp (normRTL ib k) rs0 m0 = None. -Proof. - induction ib; simpl; - try discriminate. - - (* BF *) - intros; destruct o; try discriminate; simpl in *. - inv ISTEP. destruct CONT as [HO ISTEP]; inv HO. - - (* Bnop *) - intros; destruct o; inv ISTEP; destruct oiinfo, CONT; auto. - destruct (Bnop_dec k); subst; repeat econstructor; eauto. - - (* Bop *) - 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; destruct (Bnop_dec k); - destruct (trap) eqn:TRAP; - try destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; - simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - destruct CONT as [HO ISTEP]; trivial. - - (* Bstore *) - intros; destruct o; destruct (Bnop_dec k); - destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; - simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - 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; simpl in *. destruct _fin; inv ISTEP. - + destruct CONT as [CONTRA _]; inv CONTRA. - + split; auto. eapply IHib2; eauto. - - (* Bcond *) - intros; destruct (eval_condition _ _ _); trivial. - destruct b. - + eapply IHib1; eauto. - + eapply IHib2; eauto. -Qed. - -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 (normRTL ib (Bnop None)) rs m = None. -Proof. - intros; eapply normRTL_iblock_istep_run_None_rec; eauto. - simpl; auto. -Qed. - -Lemma normRTL_preserves_iblock_istep_run sp ib: - forall rs m, iblock_istep_run tge sp ib 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 normRTL_iblock_istep_correct; auto. - - symmetry. - apply normRTL_preserves_iblock_istep_run_None; auto. -Qed. - -Local Hint Constructors match_iblock: core. -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 - | Some pc' => - match_iblock dupmap cfg false pc' k opc2 - | None => opc2=opc1 - end), - match_iblock dupmap cfg isfst pc (normRTL ib k) opc2. -Proof. - induction 1; simpl; intros; eauto. - { (* BF *) - 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. } - { (* Bcond *) - intros. inv H0; - econstructor; eauto; try econstructor. - destruct opc0; econstructor. } -Qed. - -Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc: - match_iblock dupmap cfg isfst pc ib opc -> - match_iblock dupmap cfg isfst pc (normRTL ib (Bnop None)) opc. -Proof. - intros. - eapply normRTL_matchiblock_rec_correct; eauto. - destruct opc; simpl; auto. -Qed. (** * Match strong state property @@ -455,17 +570,20 @@ See explanations of opt_simu below. *) Lemma match_strong_state_simu - dupmap st st' f f' sp rs2 m2 rs1 m1 rs0 m0 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n - (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) E0 (RTL.State st f sp pcR2 rs2 m2)) + dupmap st st' f f' sp rs2 m2 rs1 m1 rs0 m0 pcB0 pcR0 pcR1 pcR2 isfst ib1 ib2 ib0 n t s1' + (EQt: t=E0) + (EQs1': s1'=(RTL.State st f sp pcR2 rs2 m2)) + (STEP : RTL.step ge (RTL.State st f sp pcR1 rs1 m1) t s1') (MSS1 : match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib1 ib0 isfst) (MSS2 : match_strong_state dupmap st st' f f' sp rs2 m2 rs0 m0 pcB0 pcR0 pcR2 ib2 ib0 false) (MES : measure ib2 < n) : exists (oib' : option iblock), - (exists s2', step tge (State st' f' sp pcB0 rs0 m0) E0 s2' - /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) s2') - \/ (omeasure oib' < n /\ E0=E0 - /\ match_states oib' (RTL.State st f sp pcR2 rs2 m2) (State st' f' sp pcB0 rs0 m0)). + (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' + /\ match_states oib' s1' s2') + \/ (omeasure oib' < n /\ t=E0 + /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). Proof. + subst. destruct (is_goto ib2) eqn:GT. destruct ib2; try destruct fi; try discriminate. - (* Bgoto *) @@ -473,13 +591,9 @@ Proof. remember H2 as ODUPLIC; clear HeqODUPLIC. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. apply DMC in H2 as [ib [FNC MI]]; clear DMC. - eexists; left; eexists; split. - + repeat econstructor; eauto. - apply iblock_istep_run_equiv in BTL_RUN; 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. + eexists; left; eexists; split; eauto. + repeat econstructor; eauto. + apply iblock_istep_run_equiv in BTL_RUN; eauto. - (* Others *) exists (Some ib2); right; split. simpl; auto. @@ -495,7 +609,7 @@ Lemma opt_simu_intro (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2') \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). Proof. - inversion MSTRONG; subst. inv MIB. + inv MSTRONG; subst. inv MIB. - (* mib_BF *) inv H0; inversion STEP; subst; try_simplify_someHyps; intros. @@ -536,81 +650,60 @@ Proof. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. remember H1 as ODUPLIC; clear HeqODUPLIC. apply DMC in H1 as [ib [FNC MI]]; clear DMC. - eexists; left; eexists; split. - * econstructor; eauto. econstructor. - eexists; eexists; split. - eapply iblock_istep_run_equiv in BTL_RUN. - eapply BTL_RUN. econstructor; eauto. - pose symbols_preserved as SYMPRES. - eapply eval_builtin_args_preserved; eauto. - eapply external_call_symbols_preserved; eauto. eapply senv_preserved. - * 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. + exists (Some (normRTL (entry ib))); left; eexists; split; eauto. + econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. + pose symbols_preserved as SYMPRES. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + (* Bjumptable *) exploit list_nth_z_rev_dupmap; eauto. intros (pc'0 & LNZ & DM). eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. remember DM as ODUPLIC; clear HeqODUPLIC. apply DMC in DM as [ib [FNC MI]]; clear DMC. - eexists; left; eexists; split. - * econstructor; eauto. econstructor. - eexists; eexists; split. - eapply iblock_istep_run_equiv in BTL_RUN. - eapply BTL_RUN. econstructor; 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. + exists (Some (normRTL (entry ib))); left; eexists; split; eauto. + econstructor; eauto. econstructor. + eexists; eexists; split. + eapply iblock_istep_run_equiv in BTL_RUN. + eapply BTL_RUN. econstructor; eauto. - (* mib_exit *) discriminate. - (* mib_seq *) - inversion H; subst; - try (inv IS_EXPD; try inv H5; discriminate; fail); - inversion STEP; subst; try_simplify_someHyps; intros. + inv IS_EXPD; try discriminate. + inv H; simpl in *; try congruence; + inv STEP; try_simplify_someHyps; eauto. + (* Bnop is_rtl *) - eapply match_strong_state_simu. - 1,2: do 2 (econstructor; eauto). - econstructor; eauto. - inv IS_EXPD; eauto. simpl in *; discriminate. - eapply star_right; eauto. lia. + intros; eapply match_strong_state_simu; eauto. + (* Bop *) - eapply match_strong_state_simu. - 1,2: do 2 (econstructor; eauto). + intros; eapply match_strong_state_simu; eauto. econstructor; eauto. - inv IS_EXPD; eauto. simpl in *; discriminate. - eapply star_right; eauto. - erewrite eval_operation_preserved in H11. - erewrite H11 in BTL_RUN; simpl in BTL_RUN; auto. - intros; rewrite <- symbols_preserved; trivial. lia. + erewrite eval_operation_preserved in H12. + erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + (* Bload *) - eapply match_strong_state_simu. - 1,2: do 2 (econstructor; eauto). + intros; eapply match_strong_state_simu; eauto. econstructor; eauto. - inv IS_EXPD; eauto. simpl in *; discriminate. - eapply star_right; eauto. - erewrite eval_addressing_preserved in H11. - erewrite H11, H12 in BTL_RUN; simpl in BTL_RUN; auto. - intros; rewrite <- symbols_preserved; trivial. lia. + erewrite eval_addressing_preserved in H12. + erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. + (* Bstore *) - eapply match_strong_state_simu. - 1,2: do 2 (econstructor; eauto). + intros; eapply match_strong_state_simu; eauto. econstructor; eauto. - inv IS_EXPD; eauto. simpl in *; discriminate. - eapply star_right; eauto. - erewrite eval_addressing_preserved in H11. - erewrite H11, H12 in BTL_RUN; simpl in BTL_RUN; auto. - intros; rewrite <- symbols_preserved; trivial. lia. + erewrite eval_addressing_preserved in H12. + erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. - (* mib_cond *) + inv IS_EXPD; try discriminate. inversion STEP; subst; try_simplify_someHyps; intros. - 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; 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. + destruct (is_join_opt_None opc1 opc2); eauto. subst. + eapply match_strong_state_simu with (ib1:=Bcond c lr bso bnot iinfo) (ib2:=(if b then bso else bnot)); eauto. + + intros; rewrite H14 in BTL_RUN; destruct b; econstructor; eauto. + + assert (measure (if b then bnot else bso) > 0) by apply measure_pos; destruct b; simpl; lia. + Unshelve. + all: eauto. Qed. (** * Main RTL to BTL simulation theorem @@ -624,9 +717,9 @@ Two possible executions: RTL state match_states BTL state s1 ------------------------------------ s2 | | - STEP | Classical lockstep simu | - | | - s1' ----------------------------------- s2' + STEP | Classical lockstep simu | + | | + s1' ----------------------------------- s2' **Middle instruction (right side):** @@ -634,8 +727,8 @@ Two possible executions: RTL state match_states [oib] BTL state s1 ------------------------------------ s2 | _______/ - STEP | *E0 ___________________/ - | / match_states [oib'] + STEP | *E0 ___________________/ + | / match_states [oib'] s1' ______/ Where omeasure oib' < omeasure oib @@ -662,15 +755,10 @@ Proof. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. apply DMC in ENTRY as DMC'. destruct DMC' as [ib [CENTRY MI]]; clear DMC. - eexists; left; eexists; split. + exists (Some (normRTL (entry ib))); left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. - * apply normRTL_matchiblock_correct in MI. - econstructor. econstructor; eauto. - eapply is_expand_normRTL_entry; eauto. - 3: eapply normRTL_entry_isnt_goto; eauto. - all: erewrite preserv_fnparams; eauto. - constructor. apply normRTL_preserves_iblock_istep_run. + * erewrite preserv_fnparams; eauto. + (* External function *) inv TRANSF. eexists; left; eexists; split. @@ -683,13 +771,8 @@ Proof. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. remember DUPLIC as ODUPLIC; clear HeqODUPLIC. apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. - eexists; left; eexists; split. - + eapply exec_return. - + apply normRTL_matchiblock_correct in MI. - econstructor. econstructor; eauto. - eapply is_expand_normRTL_entry; eauto. - econstructor. apply normRTL_preserves_iblock_istep_run. - eapply normRTL_entry_isnt_goto; eauto. + eexists; left; eexists; split; eauto. + eapply exec_return. Qed. Local Hint Resolve plus_one star_refl: core. -- cgit