diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 758 |
1 files changed, 758 insertions, 0 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v new file mode 100644 index 00000000..0ca93bce --- /dev/null +++ b/scheduling/RTLtoBTLproof.v @@ -0,0 +1,758 @@ +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. } + all: (* Bload / Bstore *) + erewrite eval_addressing_preserved in H12; + try erewrite H12 in BTL_RUN; try erewrite H13 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. |