diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-05-24 15:06:18 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:58:30 +0200 |
commit | 0236781c3ff798b60c5c8171a0f9b6cd569f7995 (patch) | |
tree | 117e80f627ac331c066db3140a14040603118424 /mppa_k1c/Machblockgenproof.v | |
parent | 265fdd4f703b0310fbcf5ad448c29dc34f7ff33a (diff) | |
download | compcert-kvx-0236781c3ff798b60c5c8171a0f9b6cd569f7995.tar.gz compcert-kvx-0236781c3ff798b60c5c8171a0f9b6cd569f7995.zip |
Machblock: Mach language with basic blocks
Diffstat (limited to 'mppa_k1c/Machblockgenproof.v')
-rw-r--r-- | mppa_k1c/Machblockgenproof.v | 638 |
1 files changed, 638 insertions, 0 deletions
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v new file mode 100644 index 00000000..838f7977 --- /dev/null +++ b/mppa_k1c/Machblockgenproof.v @@ -0,0 +1,638 @@ +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Stacklayout. +Require Import Mach. +Require Import Linking. +Require Import Machblock. +Require Import Machblockgen. +Require Import ForwardSimulationBlock. + +(* FIXME: put this section somewhere else. + In "Smallstep" ? + +TODO: also move "starN_last_step" in the same section ? + +*) + +Section starN_lemma. +(* Auxiliary Lemma on starN *) + +Import Smallstep. +Local Open Scope nat_scope. + + +Variable L: semantics. + +Local Hint Resolve starN_refl starN_step Eapp_assoc. + +Lemma starN_split n s t s': + starN (step L) (globalenv L) n s t s' -> + forall m k, n=m+k -> + exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. +Proof. + induction 1; simpl. + + intros m k H; assert (X: m=0); try omega. + assert (X0: k=0); try omega. + subst; repeat (eapply ex_intro); intuition eauto. + + intros m; destruct m as [| m']; simpl. + - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. + - intros k H2. inversion H2. + exploit (IHstarN m' k); eauto. intro. + destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7). + repeat (eapply ex_intro). + instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0). + intuition eauto. subst. auto. +Qed. + +End starN_lemma. + + +Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.function) (c: Mach.code) := + rao (trans_function f) (trans_code c). + +Definition match_prog (p: Mach.program) (tp: Machblock.program) := + match_program (fun _ f tf => tf = trans_fundef f) eq p tp. + +Lemma trans_program_match: forall p, match_prog p (trans_prog p). +Proof. + intros. eapply match_transform_program; eauto. +Qed. + +Definition trans_stackframe (msf: Mach.stackframe) : stackframe := + match msf with + | Mach.Stackframe f sp retaddr c => Stackframe f sp retaddr (trans_code c) + end. + +Fixpoint trans_stack (mst: list Mach.stackframe) : list stackframe := + match mst with + | nil => nil + | msf :: mst0 => (trans_stackframe msf) :: (trans_stack mst0) + end. + +Definition trans_state (ms: Mach.state) : state := + match ms with + | Mach.State s f sp c rs m => State (trans_stack s) f sp (trans_code c) rs m + | Mach.Callstate s f rs m => Callstate (trans_stack s) f rs m + | Mach.Returnstate s rs m => Returnstate (trans_stack s) rs m + end. + +Section PRESERVATION. + +Variable prog: Mach.program. +Variable tprog: Machblock.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSF). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). + +Lemma init_mem_preserved: + forall m, + Genv.init_mem prog = Some m -> + Genv.init_mem tprog = Some m. +Proof (Genv.init_mem_transf TRANSF). + +Lemma prog_main_preserved: + prog_main tprog = prog_main prog. +Proof (match_program_main TRANSF). + +Lemma functions_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + exists tf, Genv.find_funct_ptr tge b = Some tf /\ trans_fundef f = tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_match TRANSF); eauto. intro. + destruct H0 as (cunit & tf & A & B & C). + eapply ex_intro. intuition; eauto. subst. eapply A. +Qed. + +Lemma find_function_ptr_same: + forall s rs, + Mach.find_function_ptr ge s rs = find_function_ptr tge s rs. +Proof. + intros. unfold Mach.find_function_ptr. unfold find_function_ptr. + destruct s; auto. + rewrite symbols_preserved; auto. +Qed. + +Lemma find_funct_ptr_same: + forall f f0, + Genv.find_funct_ptr ge f = Some (Internal f0) -> + Genv.find_funct_ptr tge f = Some (Internal (trans_function f0)). +Proof. + intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. +Qed. + +Lemma find_funct_ptr_same_external: + forall f f0, + Genv.find_funct_ptr ge f = Some (External f0) -> + Genv.find_funct_ptr tge f = Some (External f0). +Proof. + intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. +Qed. + +Lemma parent_sp_preserved: + forall s, + Mach.parent_sp s = parent_sp (trans_stack s). +Proof. + unfold parent_sp. unfold Mach.parent_sp. destruct s; simpl; auto. + unfold trans_stackframe. destruct s; simpl; auto. +Qed. + +Lemma parent_ra_preserved: + forall s, + Mach.parent_ra s = parent_ra (trans_stack s). +Proof. + unfold parent_ra. unfold Mach.parent_ra. destruct s; simpl; auto. + unfold trans_stackframe. destruct s; simpl; auto. +Qed. + +Lemma external_call_preserved: + forall ef args m t res m', + external_call ef ge args m t res m' -> + external_call ef tge args m t res m'. +Proof. + intros. eapply external_call_symbols_preserved; eauto. + apply senv_preserved. +Qed. + +Lemma Mach_find_label_split l i c c': + Mach.find_label l (i :: c) = Some c' -> + (i=Mlabel l /\ c' = c) \/ (i <> Mlabel l /\ Mach.find_label l c = Some c'). +Proof. + intros H. + destruct i; try (constructor 2; split; auto; discriminate ). + destruct (peq l0 l) as [P|P]. + - constructor. subst l0; split; auto. + revert H. unfold Mach.find_label. simpl. rewrite peq_true. + intros H; injection H; auto. + - constructor 2. split. + + intro F. injection F. intros. contradict P; auto. + + revert H. unfold Mach.find_label. simpl. rewrite peq_false; auto. +Qed. + +Lemma find_label_stop l b c c0: + to_bblock (Mlabel l :: c) = (b, c0) -> find_label l (b :: trans_code c0) = Some (trans_code c). +Proof. + intros H. + unfold find_label. + assert (X: b=(fst (to_bblock (Mlabel l :: c)))). + { rewrite H; simpl; auto. } + subst b; rewrite to_bblock_islabel. + remember ({| header := None; body := _ ; exit := _ |}) as b'. + remember (fst (to_bblock _)) as b. + destruct (size b') eqn:SIZE. + - destruct (size_null b') as (Hh & Hb & He); auto. + subst b'; simpl in *. clear Hh SIZE. + erewrite <- (to_bblock_label_then_nil b l c c0); eauto. + - assert (X: exists b0 lb0, trans_code c = b0::lb0 /\ c <> nil). + { induction c, (trans_code c) using trans_code_ind. + + subst. simpl in * |-. inversion SIZE. + + (repeat econstructor 1). intro; subst; try tauto. + } + destruct X as (b0 & lb0 & X0 & X1). + unfold to_bblock in * |-. + remember (to_bblock_header _) as bh; destruct bh as [h c1]. + remember (to_bblock_body _) as bb; destruct bb as [bdy c2]. + remember (to_bblock_exit _) as be; destruct be as [ext c3]. + unfold size in SIZE; subst b b'; simpl in * |-. + injection H; clear H; intro; subst c3. + injection Heqbh; clear Heqbh; intros; subst. + cut (to_bblock_header c = (None, c)). + * intros X2; exploit trans_code_step; eauto. + simpl; rewrite X0; clear X0. + intros (Y1 & Y2 & Y3 & Y4). subst. + rewrite Y1; clear X1; destruct b0; simpl; auto. + * destruct (cn_eqdec (get_code_nature c) IsLabel) as [ Y | Y ]. + + destruct c; simpl; try discriminate. + destruct i; simpl; try discriminate. + simpl in * |-. + inversion Heqbb; subst. simpl in * |-. + inversion Heqbe; subst; simpl in * |-. + discriminate. + + destruct c; simpl; discriminate || auto. + destruct i; simpl; auto. + destruct Y. simpl; auto. +Qed. + +Lemma find_label_next l i b c c': + to_bblock (i :: c) = (b, c') -> i <> Mlabel l -> find_label l (b :: trans_code c') = find_label l (trans_code c'). +Proof. + intros H H1. + destruct b as [hd bd ex]. + destruct (cn_eqdec (get_code_nature (i::c)) IsLabel) as [ X | X ]. + - destruct i; try discriminate. + exploit to_bblock_label; eauto. + intros (bdy & c1 & Y1 & Y2 & Y3 & Y4). + simpl in *|-. subst. clear X. + simpl. unfold is_label; simpl. + assert (l0 <> l); [ intro; subst; contradict H1; auto |]. + rewrite peq_false; auto. + - exploit to_bblock_no_label; eauto. + intro Y. apply (f_equal fst) in H as Y1. simpl in Y1. rewrite Y in Y1. clear Y. + inversion Y1; subst; clear Y1. + simpl. auto. +Qed. + +Lemma to_bblock_header_split i c h c1: + to_bblock_header (i::c)=(h, c1) + -> (exists l, i=Mlabel l /\ h=Some l /\ c1=c) \/ (forall l, i<>Mlabel l /\ h=None /\ c1=(i::c)). +Proof. + destruct i; simpl; intros H; inversion H; try (constructor 2; intuition auto; discriminate). + constructor 1; eapply ex_intro; intuition eauto. +Qed. + +Lemma to_bblock_header_find_label i c1 l c h: + i <> Mlabel l + -> to_bblock_header (i :: c) = (h, c1) -> Mach.find_label l c = Mach.find_label l c1. +Proof. + intros H1 H2; exploit to_bblock_header_split; eauto. + intros [ ( l0 & X1 & X2 & X3 ) | X ]. + - subst. auto. + - destruct (X l) as (X1 & X2 & X3). subst. clear X X1. + symmetry. destruct i; try (simpl; auto). + assert (l0 <> l); [ intro; subst; contradict H1; auto |]. + rewrite peq_false; auto. +Qed. + +Lemma to_bblock_body_find_label c2 bdy l c1: + (bdy, c2) = to_bblock_body c1 -> + Mach.find_label l c1 = Mach.find_label l c2. +Proof. + generalize bdy c2. + induction c1 as [|i c1]. + - intros bdy0 c0 H. simpl in H. inversion H; subst; clear H. auto. + - intros bdy' c2' H. simpl in H. destruct i; try ( + simpl in H; remember (to_bblock_body c1) as tbb; destruct tbb as [p c'']; + inversion H; subst; clear H; simpl; erewrite IHc1; eauto; fail). +Qed. + +Lemma to_bblock_exit_find_label c2 ext l c1: + (ext, c2) = to_bblock_exit c1 + -> Mach.find_label l c1 = Mach.find_label l c2. +Proof. + intros H. destruct c1 as [|i c1]. + - simpl in H. inversion H; subst; clear H. auto. + - destruct i; try ( + simpl in H; inversion H; subst; clear H; auto; fail). +Qed. + +Lemma Mach_find_label_to_bblock i c l b c0: + i <> Mlabel l + -> to_bblock (i :: c) = (b, c0) + -> Mach.find_label l c = Mach.find_label l c0. +Proof. + intro H. + unfold to_bblock. + remember (to_bblock_header _) as bh; destruct bh as [h c1]. + remember (to_bblock_body _) as bb; destruct bb as [bdy c2]. + remember (to_bblock_exit _) as be; destruct be as [ext c3]. + intros X; injection X. clear X; intros; subst. + erewrite (to_bblock_header_find_label i c1); eauto. + erewrite (to_bblock_body_find_label c2); eauto. + erewrite to_bblock_exit_find_label; eauto. +Qed. + +Local Hint Resolve find_label_next. + +Lemma find_label_transcode_preserved: + forall l c c', + Mach.find_label l c = Some c' -> + find_label l (trans_code c) = Some (trans_code c'). +Proof. + intros l c; induction c, (trans_code c) using trans_code_ind. + - intros c' H; inversion H. + - intros c' H. subst _x. destruct c as [| i c]; try tauto. + exploit Mach_find_label_split; eauto. clear H. + intros [ [H1 H2] | [H1 H2] ]. + + subst. erewrite find_label_stop; eauto. + + rewrite <- IHc0. eauto. + erewrite <- (Mach_find_label_to_bblock i c); eauto. +Qed. + +Lemma find_label_preserved: + forall l f c, + Mach.find_label l (Mach.fn_code f) = Some c -> + find_label l (fn_code (trans_function f)) = Some (trans_code c). +Proof. + intros. cutrewrite ((fn_code (trans_function f)) = trans_code (Mach.fn_code f)); eauto. + apply find_label_transcode_preserved; auto. +Qed. + +Lemma mem_free_preserved: + forall m stk f, + Mem.free m stk 0 (Mach.fn_stacksize f) = Mem.free m stk 0 (fn_stacksize (trans_function f)). +Proof. + intros. auto. +Qed. + +Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated + parent_sp_preserved. + +Definition dist_end_block_code (c: Mach.code) := (size (fst (to_bblock c))-1)%nat. + + +Definition dist_end_block (s: Mach.state): nat := + match s with + | Mach.State _ _ _ c _ _ => dist_end_block_code c + | _ => 0 + end. + +Local Hint Resolve exec_nil_body exec_cons_body. +Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore. + +Variable rao: function -> code -> ptrofs -> Prop. + +(* +Lemma minus_diff_0 n: (n-1<>0)%nat -> (n >= 2)%nat. +Proof. + omega. +Qed. +*) + +Ltac ExploitDistEndBlockCode := + match goal with + | [ H : dist_end_block_code (Mlabel ?l :: ?c) <> 0%nat |- _ ] => + exploit (to_bblock_size_single_label c (Mlabel l)); eauto + | [ H : dist_end_block_code (?i0 :: ?c) <> 0%nat |- _ ] => + exploit (to_bblock_size_single_basicinst c i0); eauto + | _ => idtac + end. + +(* FIXME - refactoriser avec get_code_nature pour que ce soit plus joli *) +Lemma dist_end_block_code_simu_mid_block i c: + dist_end_block_code (i::c) <> 0%nat -> + (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c))%nat. +Proof. + intros. + remember (get_code_nature c) as gcnc; destruct gcnc. + (* when c is nil *) + - contradict H. rewrite get_code_nature_nil_contra with (c := c); auto. destruct i; simpl; auto. + (* when c is IsLabel *) + - remember i as i0; remember (to_basic_inst i) as sbi; remember (to_cfi i) as scfi; + remember (get_code_nature (i::c)) as gcnic; + destruct i. + (* when i is a basic instruction *) + 1-6: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_basic_inst_then_label; eauto; + [ totologize Heqgcnic; eapply Htoto + | totologize Heqsbi; try eapply Htoto + | intro; subst; rewrite H; simpl; auto + ] ); fail). + (* when i is a control flow instruction *) + 1-8: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_cf_inst_then_label; eauto; + [ totologize Heqgcnic; eapply Htoto + | totologize Heqscfi; try eapply Htoto + | intro; subst; rewrite H; simpl; auto + ] ); fail). + (* when i is a label *) + contradict H. unfold dist_end_block_code. exploit to_bblock_double_label; eauto. + intro. subst. rewrite H. simpl. auto. + (* when c is IsBasicInst or IsCFI *) + - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) + ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | + unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). + - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) + ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | + unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). +Qed. + +Local Hint Resolve dist_end_block_code_simu_mid_block. + +Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) s f sp rs m (t:trace) (s':Mach.state): + to_basic_inst i = Some bi -> + Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> + exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. +Proof. + destruct i; simpl in * |-; + (discriminate + || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). + - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. + destruct H3 as (tf & A & B). subst. eapply A. + all: simpl; rewrite <- parent_sp_preserved; auto. + - eapply exec_MBop; eauto. rewrite <- H. destruct o; simpl; auto. destruct (rs ## l); simpl; auto. + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. +Qed. + + +Lemma star_step_simu_body_step s f sp c: + forall (p:bblock_body) c' rs m t s', + to_bblock_body c = (p, c') -> + starN (Mach.step (inv_trans_rao rao)) ge (length p) (Mach.State s f sp c rs m) t s' -> + exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp p rs m rs' m'. +Proof. + induction c as [ | i0 c0 Hc0]; simpl; intros p c' rs m t s' H. + * (* nil *) + inversion_clear H; simpl; intros X; inversion_clear X. + eapply ex_intro; eapply ex_intro; intuition eauto. + * (* cons *) + remember (to_basic_inst i0) as o eqn:Ho. + destruct o as [bi |]. + + (* to_basic_inst i0 = Some bi *) + remember (to_bblock_body c0) as r eqn:Hr. + destruct r as [p1 c1]; inversion H; simpl; subst; clear H. + intros X; inversion_clear X. + exploit step_simu_basic_step; eauto. + intros [rs' [m' [H2 [H3 H4]]]]; subst. + exploit Hc0; eauto. + intros [rs'' [m'' [H5 [H6 H7]]]]; subst. + refine (ex_intro _ rs'' (ex_intro _ m'' _)); intuition eauto. + + (* to_basic_inst i0 = None *) + inversion_clear H; simpl. + intros X; inversion_clear X. intuition eauto. +Qed. + +Lemma step_simu_cfi_step: + forall c e c' stk f sp rs m t s' b lb', + to_bblock_exit c = (Some e, c') -> + trans_code c' = lb' -> + Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp c rs m) t s' -> + cfi_step rao tge e (State (trans_stack stk) f sp (b::lb') rs m) t (trans_state s'). +Proof. + intros c e c' stk f sp rs m t s' b lb'. + intros Hexit Htc Hstep. + destruct c as [|ei c]; try (contradict Hexit; discriminate). + destruct ei; (contradict Hexit; discriminate) || ( + inversion Hexit; subst; inversion Hstep; subst; simpl + ). + * unfold inv_trans_rao in H11. + apply exec_MBcall with (f := (trans_function f0)); auto. + rewrite find_function_ptr_same in H9; auto. + apply find_funct_ptr_same. auto. + * apply exec_MBtailcall with (f := (trans_function f0)); auto. + rewrite find_function_ptr_same in H9; auto. + apply find_funct_ptr_same; auto. + rewrite parent_sp_preserved in H11; subst; auto. + rewrite parent_ra_preserved in H12; subst; auto. + * eapply exec_MBbuiltin; eauto. + eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. + * eapply exec_MBgoto; eauto. + apply find_funct_ptr_same; eauto. + apply find_label_preserved; auto. + * eapply exec_MBcond_true; eauto. + erewrite find_funct_ptr_same; eauto. + apply find_label_preserved; auto. + * eapply exec_MBcond_false; eauto. + * eapply exec_MBjumptable; eauto. + erewrite find_funct_ptr_same; eauto. + apply find_label_preserved; auto. + * eapply exec_MBreturn; eauto. + apply find_funct_ptr_same; eauto. + rewrite parent_sp_preserved in H8; subst; auto. + rewrite parent_ra_preserved in H9; subst; auto. + rewrite mem_free_preserved in H10; subst; auto. +Qed. + +Lemma simu_end_block: + forall s1 t s1', + starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> + step rao tge (trans_state s1) t (trans_state s1'). +Proof. + destruct s1; simpl. + + (* State *) + (* c cannot be nil *) + destruct c as [|i c]; simpl; try ( (* nil => absurd *) + unfold dist_end_block_code; simpl; + intros t s1' H; inversion_clear H; + inversion_clear H0; fail + ). + + intros t s1' H. + remember (_::_) as c0. remember (trans_code c0) as tc0. + + (* tc0 cannot be nil *) + destruct tc0; try + ( exploit (trans_code_nonil c0); subst; auto; try discriminate; intro H0; contradict H0 ). + + assert (X: Datatypes.S (dist_end_block_code c0) = (size (fst (to_bblock c0)))). + { + unfold dist_end_block_code. remember (size _) as siz. + assert (siz <> 0%nat). rewrite Heqsiz; apply to_bblock_nonil with (c0 := c) (i := i) (c := c0); auto. + omega. + } + + (* decomposition of starN in 3 parts: header + body + exit *) + rewrite X in H; unfold size in H. + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as [t3 [t4 [s1 [H0 [H3 H4]]]]]. + subst t; clear X H. + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as [t1 [t2 [s0 [H [H1 H2]]]]]. + subst t3; clear H0. + + (* Making the hypothesis more readable *) + remember (Smallstep.step _) as Machstep. remember (globalenv _) as mge. + remember (Mach.State _ _ _ _ _ _) as si. + + unfold to_bblock in * |- *. + (* naming parts of block "b" *) + remember (to_bblock_header c0) as hd. destruct hd as [hb c1]. + remember (to_bblock_body c1) as bb. destruct bb as [bb c2]. + remember (to_bblock_exit c2) as exb. destruct exb as [exb c3]. + simpl in * |- *. + + exploit trans_code_step; eauto. intro EQ. destruct EQ as (EQH & EQB & EQE & EQTB0). + subst hb bb exb. + + (* header opt step *) + assert (X: s0 = (Mach.State stack f sp c1 rs m) /\ t1 = E0). + { + destruct (header b) eqn:EQHB. + - inversion_clear H. inversion H2. subst. + destruct i; try (contradict EQHB; inversion Heqhd; fail). + inversion H0. subst. inversion Heqhd. auto. + - simpl in H. inversion H. subst. + destruct i; try (inversion Heqhd; auto; fail). + } + clear H; destruct X as [X1 X2]; subst s0 t1. + autorewrite with trace_rewrite. + + (* body steps *) + subst mge Machstep. + exploit (star_step_simu_body_step); eauto. + clear H1; intros [rs' [m' [H0 [H1 H2]]]]. + subst s1 t2. autorewrite with trace_rewrite. + (* preparing exit step *) + eapply exec_bblock; eauto. + clear H2. + + (* exit step *) + destruct (exit b) as [e|] eqn:EQEB. + - constructor. + simpl in H3. inversion H3. subst. clear H3. + inversion H1. subst. clear H1. + destruct c2 as [|ei c2']; try (contradict Heqexb; discriminate). + rewrite E0_right. + destruct ei; try (contradict Heqexb; discriminate). + all: eapply step_simu_cfi_step; eauto. + - simpl in H3. inversion H3; subst. simpl. + destruct c2 as [|ei c2']; inversion Heqexb; subst; try eapply exec_None_exit. + clear H3. destruct (to_cfi ei) as [cfi|] eqn:TOCFI; inversion H0. + subst. eapply exec_None_exit. + + + (* Callstate *) + intros t s1' H; inversion_clear H. + inversion H1; subst; clear H1. + inversion_clear H0; simpl. + - (* function_internal*) + cutrewrite (trans_code (Mach.fn_code f0) = fn_code (trans_function f0)); eauto. + eapply exec_function_internal; eauto. + apply find_funct_ptr_same; auto. + rewrite <- parent_sp_preserved; eauto. + rewrite <- parent_ra_preserved; eauto. + - (* function_external *) + autorewrite with trace_rewrite. + eapply exec_function_external; eauto. + apply find_funct_ptr_same_external; auto. + rewrite <- parent_sp_preserved; eauto. + apply external_call_preserved; auto. + + (* Returnstate *) + intros t s1' H; inversion_clear H. + inversion H1; subst; clear H1. + inversion_clear H0; simpl. + eapply exec_return. +Qed. + +Theorem simulation: forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog). +Proof. + apply forward_simulation_block with (dist_end_block := dist_end_block) (build_block := trans_state). +(* simu_mid_block *) + - intros s1 t s1' H1. + destruct H1; simpl; omega || (intuition auto). +(* public_preserved *) + - apply senv_preserved. +(* match_initial_states *) + - intros. simpl. destruct H. split. + apply init_mem_preserved; auto. + rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. +(* match_final_states *) + - intros. simpl. destruct H. split with (r := r); auto. +(* final_states_end_block *) + - intros. simpl in H0. inversion H0. + inversion H; simpl; auto. + (* the remaining instructions cannot lead to a Returnstate *) + all: subst; discriminate. +(* simu_end_block *) + - apply simu_end_block. +Qed. + +End PRESERVATION. |