Require Import Coqlib Maps Lia. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad BTL. 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. - (* Bop *) repeat econstructor; eauto. - (* Bload *) inv LOAD. + repeat econstructor; eauto. + do 2 (econstructor; eauto). eapply has_loaded_default; eauto. - (* Bcond *) repeat econstructor; eauto. 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 *) (* we simply switch [f] and [tf] in the usual way *) Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { matchRTL:> BTLmatchRTL.match_function dupmap tf f; liveness_ok: liveness_ok_function tf; }. Local Hint Resolve matchRTL: core. Inductive match_fundef: RTL.fundef -> BTL.fundef -> Prop := | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') | match_External ef: match_fundef (External ef) (External ef). Inductive match_stackframes: RTL.stackframe -> BTL.stackframe -> Prop := | match_stackframe_intro dupmap res f sp pc rs f' pc' (TRANSF: match_function dupmap f f') (DUPLIC: dupmap!pc' = Some pc) : match_stackframes (RTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc' rs). Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. Proof. unfold transf_function; unfold bind. repeat autodestruct. intros LIVE VER _ _ X. inv X. eexists; econstructor. - eapply verify_function_correct; simpl; eauto. - unfold liveness_ok_function; destruct u0; auto. Qed. Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. Proof. intros TRANSF; destruct f; simpl; monadInv TRANSF. + exploit transf_function_correct; eauto. intros (dupmap & MATCH_F). eapply match_Internal; eauto. + eapply match_External. Qed. Definition match_prog (p: RTL.program) (tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. Lemma transf_program_match: forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. Proof. intros. eapply match_transform_partial_program_contextual; eauto. Qed. Section BTL_SIMULATES_RTL. Variable prog: RTL.program. Variable tprog: program. Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Local Open Scope nat_scope. (** * Match relation from a RTL state to a BTL state The "option iblock" parameter represents the current BTL execution state. Thus, each RTL single step is symbolized by a new BTL "option iblock" starting at the equivalent PC. The simulation diagram for match_states_intro is as follows: << RTL state match_states_intro BTL state [pcR0,rs0,m0] --------------------------- [pcB0,rs0,m0] | | | | RTL_RUN | *E0 | BTL_RUN | | | MIB | [pcR1,rs1,m1] ------------------------------- [ib] >> *) Inductive match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst: Prop := | match_strong_state_intro (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_function dupmap f f') (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_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 . Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := | match_states_intro dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst (MSTRONG: match_strong_state dupmap st st' f f' sp rs1 m1 rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) (NGOTO: is_goto ib = false) : match_states (Some ib) (RTL.State st f sp pcR1 rs1 m1) (State st' f' sp pcB0 rs0 m0) | match_states_call st st' f f' args m (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_fundef f f') : match_states None (RTL.Callstate st f args m) (Callstate st' f' args m) | match_states_return st st' v m (STACKS: list_forall2 match_stackframes st st') : match_states None (RTL.Returnstate st v m) (Returnstate st' v m) . Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. Qed. Lemma senv_preserved: Senv.equiv ge tge. Proof. eapply (Genv.senv_match TRANSL). Qed. Lemma functions_translated (v: val) (f: RTL.fundef): Genv.find_funct ge v = Some f -> exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog. Proof. intros. exploit (Genv.find_funct_match TRANSL); eauto. intros (cu & tf & A & B & C). repeat eexists; intuition eauto. + unfold incl; auto. + eapply linkorder_refl. Qed. Lemma function_ptr_translated v f: Genv.find_funct_ptr ge v = Some f -> exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. Proof. intros. exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. Qed. Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.funsig f. Proof. intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto. erewrite preserv_fnsig; eauto. Qed. Lemma transf_initial_states s1: RTL.initial_state prog s1 -> exists ib s2, initial_state tprog s2 /\ match_states ib s1 s2. Proof. intros. inv H. exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). eexists. eexists. split. - econstructor; eauto. + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. symmetry. eapply match_program_main. eauto. + erewrite function_sig_translated; eauto. - constructor; eauto. constructor. apply transf_fundef_correct; auto. Qed. Lemma transf_final_states ib s1 s2 r: match_states ib s1 s2 -> RTL.final_state s1 r -> final_state s2 r. Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. Lemma find_function_preserved ri rs0 fd (FIND : RTL.find_function ge ri rs0 = Some fd) : exists fd', find_function tge ri rs0 = Some fd' /\ transf_fundef fd = OK fd'. Proof. pose symbols_preserved as SYMPRES. destruct ri. + simpl in FIND; apply functions_translated in FIND. destruct FIND as (tf & cunit & TFUN & GFIND & LO). eexists; split. eauto. assumption. + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF). eexists; split. simpl. rewrite symbols_preserved. rewrite GFS. eassumption. assumption. Qed. (** Representing an intermediate BTL state We keep a measure of code that remains to be executed with the omeasure type defined below. Intuitively, each RTL step corresponds to either - a single BTL step if we are on the last instruction of the block - no BTL step (as we use a "big step" semantics) but a change in the measure which represents the new intermediate state of the BTL code *) Fixpoint measure ib: nat := match ib with | Bseq ib1 ib2 | Bcond _ _ ib1 ib2 _ => measure ib1 + measure ib2 | ib => 1 end. Definition omeasure (oib: option iblock): nat := match oib with | None => 0 | Some ib => measure ib end. Remark measure_pos: forall ib, measure ib > 0. Proof. induction ib; simpl; auto; lia. Qed. 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 MIB; inversion MIB as [d1 d2 d3 d4 d5 H H0| | | | | | | |]; subst; simpl; try congruence. inv H0; congruence. Qed. 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. 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, list_nth_z ln val = Some pc -> list_forall2 (fun n' n => dupmap!n' = Some n) ln' ln -> exists (pc': node), list_nth_z ln' val = Some pc' /\ dupmap!pc' = Some pc. Proof. induction ln; intros until val; intros LNZ LFA. - inv LNZ. - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + inv H0. destruct ln'; inv LFA. simpl. exists p. split; auto. + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. (** * Match strong state property Used when executing non-atomic instructions such as Bseq/Bcond(ib1,ib2). Two possible executions: << **ib2 is a Bgoto (left side):** RTL state MSS1 BTL state [pcR1,rs1,m1] -------------------------- [ib1,pcB0,rs0,m0] | | | | | | BTL_STEP | | | | RTL_STEP | *E0 [ib2,pc=(Bgoto succ),rs2,m2] | / | | MSS2 / | | _________________/ | BTL_GOTO | / | | / GOAL: match_states | [pcR2,rs2,m2] ------------------------ [ib?,pc=succ,rs2,m2] **ib2 is any other instruction (right side):** 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 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' 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 H4. remember H2 as ODUPLIC; clear HeqODUPLIC. exploit dupmap_correct; eauto. intros [ib [FNC MI]]. eexists; left; eexists; split; eauto. repeat econstructor; eauto. apply iblock_istep_run_equiv in BTL_RUN; eauto. econstructor. - (* Others *) exists (Some ib2); right; split. simpl; auto. split; auto. econstructor; eauto. Qed. Lemma opt_simu_intro dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst s1' t (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1') (MSTRONG : match_strong_state dupmap st st' f f' sp rs m rs0 m0 pcB0 pcR0 pcR1 ib ib0 isfst) (NGOTO : is_goto ib = false) : exists (oib' : option iblock), (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. inv MSTRONG; subst. inv MIB. - (* mib_BF *) inv H0; inversion STEP; subst; try_simplify_someHyps; intros. + (* Breturn *) eexists; left; eexists; split. * econstructor; eauto. econstructor. eexists; eexists; split. eapply iblock_istep_run_equiv in BTL_RUN. eapply BTL_RUN. econstructor; eauto. erewrite preserv_fnstacksize; eauto. * econstructor; eauto. + (* Bcall *) rename H10 into FIND. eapply find_function_preserved in FIND. destruct FIND as (fd' & FF & TRANSFUN). eexists; left; eexists; split. * econstructor; eauto. econstructor. eexists; eexists; split. eapply iblock_istep_run_equiv in BTL_RUN. eapply BTL_RUN. econstructor; eauto. eapply function_sig_translated; eauto. * repeat (econstructor; eauto). eapply transf_fundef_correct; eauto. + (* Btailcall *) rename H9 into FIND. eapply find_function_preserved in FIND. destruct FIND as (fd' & FF & TRANSFUN). eexists; left; eexists; split. * econstructor; eauto. econstructor. eexists; eexists; split. eapply iblock_istep_run_equiv in BTL_RUN. eapply BTL_RUN. econstructor; eauto. eapply function_sig_translated; eauto. erewrite preserv_fnstacksize; eauto. * repeat (econstructor; eauto). eapply transf_fundef_correct; eauto. + (* Bbuiltin *) exploit dupmap_correct; eauto. intros [ib [FNC MI]]. 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). exploit dupmap_correct; eauto. intros [ib [FNC MI]]. 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 *) inv IS_EXPD; try discriminate. inv H; simpl in *; try congruence; inv STEP; try_simplify_someHyps; intros; eapply match_strong_state_simu; eauto; econstructor; eauto. { (* Bop *) erewrite eval_operation_preserved in H12. erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto. intros; rewrite <- symbols_preserved; trivial. } (* Bload/Bstore *) inv H12; [ idtac | destruct (eval_addressing) eqn:EVAL in LOAD;[ specialize (LOAD v) |] ]; rename LOAD into MEMT. 4: rename H12 into EVAL; rename H13 into MEMT. all: erewrite eval_addressing_preserved in EVAL; try erewrite EVAL in BTL_RUN; try erewrite MEMT in BTL_RUN; simpl in BTL_RUN; try destruct trap; auto; intros; rewrite <- symbols_preserved; trivial. - (* mib_cond *) inv IS_EXPD; try discriminate. inversion STEP; subst; try_simplify_someHyps; intros. 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 Two possible executions: << **Last instruction (left side):** RTL state match_states BTL state s1 ------------------------------------ s2 | | STEP | Classical lockstep simu | | | s1' ----------------------------------- s2' **Middle instruction (right side):** RTL state match_states [oib] BTL state s1 ------------------------------------ s2 | _______/ STEP | *E0 ___________________/ | / match_states [oib'] s1' ______/ Where omeasure oib' < omeasure oib >> *) Theorem opt_simu s1 t s1' oib s2: RTL.step ge s1 t s1' -> match_states oib s1 s2 -> exists (oib' : option iblock), (exists s2', step tid tge s2 t s2' /\ match_states oib' s1' s2') \/ (omeasure oib' < omeasure oib /\ t=E0 /\ match_states oib' s1' s2) . Proof. inversion 2; subst; clear H0. - (* State *) exploit opt_simu_intro; eauto. - (* Callstate *) inv H. + (* Internal function *) inv TRANSF. rename H0 into TRANSF. exploit dupmap_entrypoint; eauto. intros ENTRY. exploit dupmap_correct; eauto. intros [ib [CENTRY MI]]. exists (Some (normRTL (entry ib))); left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. * erewrite preserv_fnparams; eauto. + (* External function *) inv TRANSF. eexists; left; eexists; split. * eapply exec_function_external. eapply external_call_symbols_preserved. eapply senv_preserved. eauto. * econstructor; eauto. - (* Returnstate *) inv H. inv STACKS. inv H1. exploit dupmap_correct; eauto. intros [ib [FNC MI]]. eexists; left; eexists; split; eauto. eapply exec_return. Qed. Local Hint Resolve plus_one star_refl: core. Theorem transf_program_correct_cfg: forward_simulation (RTL.semantics prog) (BTLmatchRTL.cfgsem tprog). Proof. eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states). constructor 1; simpl. - apply well_founded_ltof. - eapply transf_initial_states. - eapply transf_final_states. - intros s1 t s1' STEP i s2 MATCH. exploit opt_simu; eauto. clear MATCH STEP. destruct 1 as (oib' & [ (s2' & STEP & MATCH) | (MEASURE & TRACE & MATCH) ]). + repeat eexists; eauto. + subst. repeat eexists; eauto. - eapply senv_preserved. Qed. Theorem all_fundef_liveness_ok b f: Genv.find_funct_ptr tge b = Some f -> liveness_ok_fundef f. Proof. unfold match_prog, match_program in TRANSL. unfold Genv.find_funct_ptr, tge; simpl; intro X. destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence. destruct y as [tf0|]; try congruence. inversion X as [H1]. subst. clear X. remember (@Gfun fundef unit f) as f2. destruct H as [ctx' f1 f2 H0|]; try congruence. inversion Heqf2 as [H2]. subst; clear Heqf2. exploit transf_fundef_correct; eauto. destruct f; econstructor. inv H1; eapply liveness_ok; eauto. Qed. Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (BTL.fsem tprog). Proof. eapply compose_forward_simulations. - eapply transf_program_correct_cfg. - eapply cfgsem2fsem. apply all_fundef_liveness_ok. Qed. End BTL_SIMULATES_RTL.