diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 601 |
1 files changed, 306 insertions, 295 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index feaac26f..7d83931b 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -6,6 +6,229 @@ 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. + +(** 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 allowing for trailing [Bnop None]. *) +Inductive is_wnormRTL: iblock -> Prop := + | wnorm_Bseq ib1 ib2: + is_RTLbasic ib1 = true -> + (ib2 <> Bnop None -> 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 => 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; intuition subst; eauto. + { (* Bnop *) autodestruct; eauto. } + 1-3: (* Bop, Bload, Bstore *) + intros; repeat econstructor; eauto. + (* Bcond *) + destruct ofin; intuition subst; + 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 k + (CONT: match iblock_istep_run tge sp ib rs0 m0 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; intros; subst; intuition (try discriminate). + - (* Bnop *) + intros. autodestruct; auto. + - (* Bop *) + intros; repeat autodestruct; simpl; intuition congruence. + - (* Bload *) + intros; repeat autodestruct; simpl; intuition congruence. + - (* Bstore *) + intros; repeat autodestruct; simpl; intuition congruence. + - (* Bseq *) + intros. + eapply IHib1; eauto. + autodestruct; simpl in *; destruct o; simpl in *; intuition eauto. + + destruct _fin; intuition eauto. + + destruct _fin; intuition congruence || eauto. + - (* Bcond *) + intros; repeat autodestruct; simpl; intuition congruence || 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. + rewrite H; 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; subst; eauto. + (* 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); @@ -40,11 +263,11 @@ Qed. Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. -Proof. +Proof. Admitted. (* unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. -Qed. + Qed.*) Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. @@ -106,7 +329,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,26 +454,30 @@ Proof. induction ib; simpl; auto; lia. Qed. -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 H4. + intros MIB; inversion MIB as [d1 d2 d3 d4 d5 H H0| | | | | | | |]; subst; simpl; try congruence. + inv H0; congruence. 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. +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 (expand (entry ib) None))eqn:EQG. - - destruct (expand (entry ib) None); - try destruct fi; try discriminate; trivial. - intros; inv H; inv H4. - - destruct (expand (entry ib) None); - try destruct fi; try discriminate; trivial. + 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, @@ -269,189 +496,6 @@ Proof. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. -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) - | 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. - - (* Bcond *) - destruct ofin; intros; - econstructor; eauto; - destruct b; eapply IHISTEP; eauto. -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. -Proof. - intros; eapply expand_iblock_istep_rec_correct; eauto. - destruct ofin; simpl; auto. -Qed. - -(* TODO 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 - | _ => True - end), - iblock_istep_run tge sp (expand ib k) rs0 m0 = None. -Proof. - induction ib; simpl; - try discriminate. - - (* BF *) - intros; destruct o; try discriminate; simpl in *. - inv ISTEP. destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO. - - (* Bnop *) - intros; destruct o; inv ISTEP; destruct k; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. - - (* 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. - - (* Bload *) - intros; destruct o; - destruct (trap) eqn:TRAP; - try destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; destruct k; - simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. - - (* Bstore *) - intros; destruct o; - destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; destruct k; - simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; 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. - + split; auto. eapply IHib2; eauto. - - (* Bcond *) - intros; destruct (eval_condition _ _ _); trivial. - destruct b. - + eapply IHib1; eauto. - + eapply IHib2; eauto. -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. -Proof. - intros; eapply expand_iblock_istep_run_None_rec; eauto. - simpl; auto. -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. -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. - - symmetry. - apply expand_preserves_iblock_istep_run_None; auto. -Qed. - -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) - | None => opc2=opc1 - end), - match_iblock dupmap cfg isfst pc (expand ib k) opc2. -Proof. - induction 1; simpl. - { (* 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. - { (* Bgoto *) - intros; inv CONT; apply mib_exit; auto. } - { (* Bseq *) - intros. eapply IHMIB1. right. eexists; split; eauto. } - { (* Bcond *) - intros. inv H0; - econstructor; eauto; try econstructor. - destruct opc0; econstructor. } -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. -Proof. - intros. - eapply expand_matchiblock_rec_correct; eauto. - destruct opc; simpl; auto. -Qed. (** * Match strong state property @@ -486,31 +530,30 @@ 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 tid 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)). + /\ 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 *) - inv MSS2. inversion MIB; subst; try inv H3. - remember H0 as ODUPLIC; clear HeqODUPLIC. + inv MSS2. inversion MIB; subst; try inv H4. + remember H2 as ODUPLIC; clear HeqODUPLIC. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. - apply DMC in H0 as [ib [FNC MI]]; clear DMC. - 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. - econstructor. apply expand_preserves_iblock_istep_run. - eapply expand_entry_isnt_goto; eauto. + apply DMC in H2 as [ib [FNC MI]]; clear DMC. + 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. @@ -526,7 +569,7 @@ Lemma opt_simu_intro (exists s2', step tid 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. @@ -567,81 +610,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 expand_matchiblock_correct in MI. - { econstructor; eauto. apply expand_correct; trivial. - apply star_refl. apply expand_preserves_iblock_istep_run. } - eapply expand_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 expand_matchiblock_correct in MI. - { econstructor; eauto. apply expand_correct; trivial. - apply star_refl. apply expand_preserves_iblock_istep_run. } - eapply expand_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. - + (* Bnop *) - 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. + inv IS_EXPD; try discriminate. + inv H; simpl in *; try congruence; + inv STEP; try_simplify_someHyps; eauto. + + (* Bnop is_rtl *) + 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; 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 @@ -655,9 +677,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):** @@ -665,8 +687,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 @@ -693,16 +715,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 expand_matchiblock_correct in MI. - econstructor. econstructor; eauto. - apply expand_correct; trivial. - 3: eapply expand_entry_isnt_goto; eauto. - all: erewrite preserv_fnparams; eauto. - constructor. - apply expand_preserves_iblock_istep_run. + * erewrite preserv_fnparams; eauto. + (* External function *) inv TRANSF. eexists; left; eexists; split. @@ -715,13 +731,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 expand_matchiblock_correct in MI. - econstructor. econstructor; eauto. - apply expand_correct; trivial. - constructor. apply expand_preserves_iblock_istep_run. - eapply expand_entry_isnt_goto; eauto. + eexists; left; eexists; split; eauto. + eapply exec_return. Qed. Local Hint Resolve plus_one star_refl: core. |