diff options
| -rw-r--r-- | driver/ForwardSimulationBlock.v | 111 | ||||
| -rw-r--r-- | mppa_k1c/Machblock.v | 44 | ||||
| -rw-r--r-- | mppa_k1c/Machblockgen.v | 176 | ||||
| -rw-r--r-- | mppa_k1c/Machblockgenproof.v | 416 |
4 files changed, 395 insertions, 352 deletions
diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v index 8c1fcb08..a9569e08 100644 --- a/driver/ForwardSimulationBlock.v +++ b/driver/ForwardSimulationBlock.v @@ -1,6 +1,7 @@ (*** -Variante de Forward Simulation pour les blocks. +Auxiliary lemmas on starN and forward_simulation +in order to prove the forward simulation of Mach -> Machblock. ***) @@ -15,16 +16,36 @@ Require Import Smallstep. Local Open Scope nat_scope. -Section ForwardSimuBlock. +(** Auxiliary lemma on starN *) +Section starN_lemma. -Variable L1 L2: semantics. +Variable L: semantics. -Local Hint Resolve starN_refl starN_step. +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. Lemma starN_last_step n s t1 s': - starN (step L1) (globalenv L1) n s t1 s' -> + starN (step L) (globalenv L) n s t1 s' -> forall (t t2:trace) s'', - Step L1 s' t2 s'' -> t = t1 ** t2 -> starN (step L1) (globalenv L1) (S n) s t s''. + Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. Proof. induction 1; simpl. + intros t t1 s0; autorewrite with trace_rewrite. @@ -34,6 +55,17 @@ Proof. intros; subst; autorewrite with trace_rewrite; auto. Qed. +End starN_lemma. + + + +(** General scheme from a "match_states" relation *) + +Section ForwardSimuBlock_REL. + +Variable L1 L2: semantics. + + (** Hypothèses de la preuve *) Variable dist_end_block: state L1 -> nat. @@ -61,6 +93,8 @@ Hypothesis simu_end_block: (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) +Local Hint Resolve starN_refl starN_step. + Definition star_in_block (head current: state L1): Prop := dist_end_block head >= dist_end_block current /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. @@ -216,7 +250,7 @@ Proof. * unfold head; rewrite H2; simpl. intuition eauto. Qed. -Lemma forward_simulation_block: forward_simulation L1 L2. +Lemma forward_simulation_block_rel: forward_simulation L1 L2. Proof. eapply compose_forward_simulations. eapply forward_memo_simulation_1. @@ -224,4 +258,65 @@ Proof. Qed. -End ForwardSimuBlock.
\ No newline at end of file +End ForwardSimuBlock_REL. + + + +(* An instance of the previous scheme, when there is a translation from L1 states to L2 states + +Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state. +This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label). + +However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below... + +*) + +Section ForwardSimuBlock_TRANS. + +Variable L1 L2: semantics. + +Variable trans_state: state L1 -> state L2. + +Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := + (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))). + +Definition match_states s1 s2: Prop := + equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1). + +Lemma match_states_trans_state s1: match_states s1 (trans_state s1). +Proof. + unfold match_states, equiv_on_next_step. intuition. +Qed. + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. + +Hypothesis match_final_states: + forall s1 r, final_state L1 s1 r -> final_state L2 (trans_state s1) r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'. + +Lemma forward_simulation_block_trans: forward_simulation L1 L2. +Proof. + eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto. + + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto. + + (* simu_end_block *) + intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto. + intros (s2' & H3 & H4); econstructor 1; intuition eauto. + rewrite H2a; auto. + inversion_clear H1. eauto. +Qed. + +End ForwardSimuBlock_TRANS.
\ No newline at end of file diff --git a/mppa_k1c/Machblock.v b/mppa_k1c/Machblock.v index 6d28844b..44cec642 100644 --- a/mppa_k1c/Machblock.v +++ b/mppa_k1c/Machblock.v @@ -38,7 +38,7 @@ Inductive control_flow_inst: Type := . Record bblock := mk_bblock { - header: option label; + header: list label; body: bblock_body; exit: option control_flow_inst }. @@ -60,15 +60,15 @@ Definition length_opt {A} (o: option A) : nat := | None => 0 end. -Definition size (b:bblock): nat := (length_opt (header b))+(length (body b))+(length_opt (exit b)). +Definition size (b:bblock): nat := (length (header b))+(length (body b))+(length_opt (exit b)). Lemma size_null b: size b = 0%nat -> - header b = None /\ body b = nil /\ exit b = None. + header b = nil /\ body b = nil /\ exit b = None. Proof. destruct b as [h b e]. simpl. unfold size. simpl. intros H. - assert (length_opt h = 0%nat) as Hh; [ omega |]. + assert (length h = 0%nat) as Hh; [ omega |]. assert (length b = 0%nat) as Hb; [ omega |]. assert (length_opt e = 0%nat) as He; [ omega|]. repeat split. @@ -94,34 +94,34 @@ Definition genv := Genv.t fundef unit. (*** sémantique ***) +Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. +Proof. + apply List.in_dec. + apply Pos.eq_dec. +Qed. + Definition is_label (lbl: label) (bb: bblock) : bool := - match header bb with - | Some lbl' => if peq lbl lbl' then true else false - | _ => false - end. + if in_dec lbl (header bb) then true else false. -Lemma is_label_correct: - forall lbl bb, - if is_label lbl bb then (header bb) = Some lbl else (header bb) <> Some lbl. +Lemma is_label_correct_true lbl bb: + List.In lbl (header bb) <-> is_label lbl bb = true. Proof. - intros. unfold is_label. destruct (header bb) as [lbl'|]; simpl; try discriminate. - case (peq lbl lbl'); intro; congruence. + unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. Qed. +Lemma is_label_correct_false lbl bb: + ~(List.In lbl (header bb)) <-> is_label lbl bb = false. +Proof. + unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. +Qed. + + Local Open Scope nat_scope. -(* FIXME - avoir une définition un peu plus simple, au prix de la preuve Mach -> Machblock ? *) Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := match c with | nil => None - | bb1 :: bbl => if is_label lbl bb1 - then let bb' := {| header := None ; body := body bb1 ; exit := exit bb1 |} in ( - Some (match size bb' with - | O => bbl - | Datatypes.S _ => bb' :: bbl - end) - ) - else find_label lbl bbl + | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl end. Section RELSEM. diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 039e6c6e..0601f5b9 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -15,6 +15,15 @@ Require Import Mach. Require Import Linking. Require Import Machblock. + +Fixpoint to_bblock_header (c: Mach.code): list label * Mach.code := + match c with + | (Mlabel l)::c' => + let (h, c'') := to_bblock_header c' in + (l::h, c'') + | _ => (nil, c) + end. + Definition to_basic_inst(i: Mach.instruction): option basic_inst := match i with | Mgetstack ofs ty dst => Some (MBgetstack ofs ty dst) @@ -38,12 +47,6 @@ Fixpoint to_bblock_body(c: Mach.code): bblock_body * Mach.code := end end. -Definition to_bblock_header (c: Mach.code): option label * Mach.code := - match c with - | (Mlabel l)::c' => (Some l, c') - | _ => (None, c) - end. - Definition to_cfi (i: Mach.instruction): option control_flow_inst := match i with @@ -105,10 +108,10 @@ Proof. intros H1 H2. destruct a; discriminate || contradict H2; subst; simpl; discriminate. Qed. -Lemma to_bblock_header_not_IsLabel c b c0: +Lemma to_bblock_header_not_IsLabel c h c0: get_code_nature c <> IsLabel -> - to_bblock_header c = (b, c0) -> - c = c0 /\ b=None. + to_bblock_header c = (h, c0) -> + c = c0 /\ h=nil. Proof. intros H1 H2. destruct c. - simpl in H2; inversion H2; auto. @@ -116,14 +119,15 @@ Proof. simpl in H1; contradict H1; auto. Qed. -Lemma to_bblock_header_eq c b c0: +Lemma to_bblock_header_eq c h c0: get_code_nature c <> IsLabel -> - to_bblock_header c = (b, c0) -> + to_bblock_header c = (h, c0) -> c = c0. Proof. intros H1 H2; exploit to_bblock_header_not_IsLabel; intuition eauto. Qed. +(* Lemma to_bblock_header_IsLabel c c0 b: get_code_nature c = IsLabel -> to_bblock_header c = (b, c0) -> @@ -133,23 +137,33 @@ Proof. destruct i; try discriminate. unfold to_bblock_header in H2; inversion H2; eauto. Qed. +*) -Lemma to_bblock_header_wf c b c0: - get_code_nature c = IsLabel -> - to_bblock_header c = (b, c0) -> - (length c > length c0)%nat. +Lemma to_bblock_header_wfe c: + forall h c0, + to_bblock_header c = (h, c0) -> + (length c >= length c0)%nat. Proof. - intros H1 H2; exploit to_bblock_header_IsLabel; eauto. - intros [l X]; subst; simpl; auto. + induction c as [ |i c]; simpl; intros h c' H. + - inversion H; subst; clear H; simpl; auto. + - destruct i; try (inversion H; subst; simpl; auto; fail). + remember (to_bblock_header c) as bhc; destruct bhc as [h0 c0]. + inversion H; subst. + lapply (IHc h0 c'); auto. Qed. -Lemma to_bblock_header_wfe c b c0: +Lemma to_bblock_header_wf c b c0: + get_code_nature c = IsLabel -> to_bblock_header c = (b, c0) -> - (length c >= length c0)%nat. + (length c > length c0)%nat. Proof. - destruct (cn_eqdec (get_code_nature c) IsLabel). - - intros; exploit to_bblock_header_wf; eauto; omega. - - intros; exploit to_bblock_header_eq; eauto. intros; subst; auto. + intros H1 H2; destruct c; [ contradict H1; simpl; discriminate | ]. + destruct i; try discriminate. + simpl in H2. + remember (to_bblock_header c) as bh; destruct bh as [h c'']. + inversion H2; subst. + exploit to_bblock_header_wfe; eauto. + simpl; omega. Qed. Lemma to_bblock_body_eq c b c0: @@ -176,6 +190,7 @@ Proof. + inversion H; subst; auto. Qed. +(* pas vraiment utile: à éliminer *) Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop := Cons_to_bbloc_body i bi c' b': to_basic_inst i = Some bi @@ -244,21 +259,22 @@ Definition to_bblock(c: Mach.code): bblock * Mach.code := ({| header := h; body := bdy; exit := ext |}, c2) . -Lemma to_bblock_double_label c l: - get_code_nature c = IsLabel -> - to_bblock (Mlabel l :: c) = ({| header := Some l; body := nil; exit := None |}, c). +Lemma to_bblock_acc_label c l b c': + to_bblock c = (b, c') -> + to_bblock (Mlabel l :: c) = ({| header := l::(header b); body := (body b); exit := (exit b) |}, c'). Proof. - intros H. - destruct c as [|i c]; try (contradict H; simpl; discriminate). - destruct i; try (contradict H; simpl; discriminate). - auto. + unfold to_bblock; simpl. + remember (to_bblock_header c) as bhc; destruct bhc as [h c0]. + remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1]. + remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2]. + intros H; inversion H; subst; clear H; simpl; auto. Qed. Lemma to_bblock_basic_inst_then_label i c bi: get_code_nature (i::c) = IsBasicInst -> get_code_nature c = IsLabel -> to_basic_inst i = Some bi -> - fst (to_bblock (i::c)) = {| header := None; body := bi::nil; exit := None |}. + fst (to_bblock (i::c)) = {| header := nil; body := bi::nil; exit := None |}. Proof. intros H1 H2 H3. destruct c as [|i' c]; try (contradict H1; simpl; discriminate). @@ -270,7 +286,7 @@ Lemma to_bblock_cf_inst_then_label i c cfi: get_code_nature (i::c) = IsCFI -> get_code_nature c = IsLabel -> to_cfi i = Some cfi -> - fst (to_bblock (i::c)) = {| header := None; body := nil; exit := Some cfi |}. + fst (to_bblock (i::c)) = {| header := nil; body := nil; exit := Some cfi |}. Proof. intros H1 H2 H3. destruct c as [|i' c]; try (contradict H1; simpl; discriminate). @@ -278,55 +294,10 @@ Proof. destruct i; simpl in *; inversion H3; subst; auto. Qed. -Lemma to_bblock_single_label c l: - get_code_nature c <> IsLabel -> - fst (to_bblock (Mlabel l :: c)) = {| - header := Some l; - body := body (fst (to_bblock c)); - exit := exit (fst (to_bblock c)) - |}. -Proof. - intros H. - destruct c as [|i c]; simpl; auto. - apply bblock_eq; simpl. -(* header *) - + destruct i; try ( - remember (to_bblock _) as bb; - unfold to_bblock in *; - remember (to_bblock_header _) as tbh; - destruct tbh; - destruct (to_bblock_body _); - destruct (to_bblock_exit _); - subst; simpl; inversion Heqtbh; auto; fail - ). -(* body *) - + remember i as i0; destruct i0; try ( - remember (to_bblock _) as bb; - unfold to_bblock in *; - remember (to_bblock_header _) as tbh; rewrite Heqi0; - remember (to_bblock_header (i :: _)) as tbh'; rewrite <- Heqi0 in *; - destruct tbh; destruct tbh'; - inversion Heqtbh; inversion Heqtbh'; subst; - destruct (to_bblock_body _); - destruct (to_bblock_exit _); auto; fail - ). contradict H; simpl; auto. -(* exit (same proof as body) *) - + remember i as i0; destruct i0; try ( - remember (to_bblock _) as bb; - unfold to_bblock in *; - remember (to_bblock_header _) as tbh; rewrite Heqi0; - remember (to_bblock_header (i :: _)) as tbh'; rewrite <- Heqi0 in *; - destruct tbh; destruct tbh'; - inversion Heqtbh; inversion Heqtbh'; subst; - destruct (to_bblock_body _); - destruct (to_bblock_exit _); auto; fail - ). contradict H; simpl; auto. -Qed. - Lemma to_bblock_no_label c: get_code_nature c <> IsLabel -> fst (to_bblock c) = {| - header := None; + header := nil; body := body (fst (to_bblock c)); exit := exit (fst (to_bblock c)) |}. @@ -369,18 +340,16 @@ Qed. Lemma to_bblock_label b l c c': to_bblock (Mlabel l :: c) = (b, c') -> - exists bdy c1, to_bblock_body c = (bdy, c1) /\ - header b = Some l /\ body b = bdy /\ exit b = fst (to_bblock_exit c1). + (header b) = l::(tail (header b)) /\ to_bblock c = ({| header:=tail (header b); body := body b; exit := exit b |}, c'). Proof. - intros H. - unfold to_bblock in H; simpl in H. - remember (to_bblock_body c) as tbbc; destruct tbbc as [bdy' c1']. - remember (to_bblock_exit c1') as tbbe; destruct tbbe as [ext c2]. - esplit; eauto. esplit; eauto. esplit; eauto. - inversion H; subst; clear H. simpl. - apply (f_equal fst) in Heqtbbe. simpl in Heqtbbe. auto. + unfold to_bblock; simpl. + remember (to_bblock_header c) as bhc; destruct bhc as [h c0]. + remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1]. + remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2]. + intros H; inversion H; subst; clear H; simpl; auto. Qed. +(* Lemma to_bblock_label_then_nil b l c c': to_bblock (Mlabel l :: c) = (b, c') -> body b = nil -> @@ -397,13 +366,14 @@ Proof. exploit to_bblock_body_nil; eauto. intros; subst. clear Heqtbb. exploit to_bblock_exit_nil; eauto. Qed. +*) Lemma to_bblock_basic_inst c i bi: get_code_nature (i::c) = IsBasicInst -> to_basic_inst i = Some bi -> get_code_nature c <> IsLabel -> fst (to_bblock (i::c)) = {| - header := None; + header := nil; body := bi :: body (fst (to_bblock c)); exit := exit (fst (to_bblock c)) |}. @@ -451,30 +421,22 @@ Qed. Lemma to_bblock_size_single_label c i: get_code_nature (i::c) = IsLabel -> - get_code_nature c <> IsLabel -> size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))). Proof. - intros. - destruct i; try (contradict H; simpl; discriminate). - destruct c; simpl; auto. - destruct i; try ( - exploit to_bblock_single_label; eauto; intro; rewrite H1; - exploit to_bblock_no_label; eauto; intro; rewrite H2; - simpl; auto; fail ). - Unshelve. all: auto. + intros H. + destruct i; try discriminate. + remember (to_bblock c) as bl. destruct bl as [b c']. + erewrite to_bblock_acc_label; eauto. + unfold size; simpl. + auto. Qed. Lemma to_bblock_size_label_neqz c: get_code_nature c = IsLabel -> size (fst (to_bblock c)) <> 0%nat. Proof. - intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate). - destruct i; try (contradict H; simpl; discriminate). - destruct (get_code_nature c) eqn:gcnc. - (* Case gcnc is not IsLabel *) - all: try (rewrite to_bblock_size_single_label; auto; rewrite gcnc; discriminate). - (* Case gcnc is IsLabel *) - rewrite to_bblock_double_label; auto; unfold size; simpl; auto. + destruct c as [ |i c]; try discriminate. + intros; rewrite to_bblock_size_single_label; auto. Qed. Lemma to_bblock_size_basicinst_neqz c: @@ -516,7 +478,7 @@ Proof. (exploit to_bblock_basic_inst; eauto); [remember (to_basic_inst _) as tbi; destruct tbi; eauto |]; intro; rewrite H1; unfold size; simpl; - assert ((length_opt (header (fst (to_bblock c)))) = 0%nat); + assert ((length (header (fst (to_bblock c)))) = 0%nat); exploit to_bblock_no_label; eauto; intro; rewrite H2; simpl; auto; rewrite H2; auto ). @@ -575,6 +537,7 @@ Proof. - eapply to_bblock_size_cfi_neqz; auto. Qed. +(* Lemma to_bblock_islabel c l: is_label l (fst (to_bblock (Mlabel l :: c))) = true. Proof. @@ -621,6 +584,7 @@ Proof. inversion Heqtbc; subst. clear Heqtbh Heqtbc. unfold to_bblock_exit in Heqtbe. apply (f_equal fst) in Heqtbe; auto. Qed. +*) Function trans_code (c: Mach.code) { measure length c }: code := match c with @@ -633,8 +597,6 @@ Proof. intros; eapply to_bblock_wf; eauto. discriminate. Qed. -Definition hd_code (bc: code) := (hd {| header := None; body := nil; exit := None |} bc). - Lemma trans_code_nonil c: c <> nil -> trans_code c <> nil. Proof. @@ -665,7 +627,7 @@ Qed. Lemma trans_code_cfi i c cfi: to_cfi i = Some cfi -> - trans_code (i :: c) = {| header := None ; body := nil ; exit := Some cfi |} :: trans_code c. + trans_code (i :: c) = {| header := nil ; body := nil ; exit := Some cfi |} :: trans_code c. Proof. intros. rewrite trans_code_equation. remember (to_bblock _) as tb; destruct tb as [b c0]. destruct i; try (contradict H; discriminate). diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index b53af131..0efd4586 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -17,45 +17,6 @@ Require Import Machblock. Require Import Machblockgen. Require Import ForwardSimulationBlock. -(** FIXME: put this section somewhere else. - * In "Smallstep" ? - * - * 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). @@ -87,12 +48,27 @@ Definition trans_state (ms: Mach.state) : state := Section PRESERVATION. +Local Open Scope nat_scope. + Variable prog: Mach.program. Variable tprog: Machblock.program. Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. + +Variable rao: function -> code -> ptrofs -> Prop. + +Definition match_states: Mach.state -> state -> Prop + := ForwardSimulationBlock.match_states (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog) trans_state. + +Lemma match_states_trans_state s1: match_states s1 (trans_state s1). +Proof. + apply match_states_trans_state. +Qed. + +Local Hint Resolve match_states_trans_state. + Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_match TRANSF). @@ -187,95 +163,91 @@ Proof. + 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'). +Definition concat (h: list label) (c: code): code := + match c with + | nil => {| header := h; body := nil; exit := None |}::nil + | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c' + end. + +Lemma to_bblock_start_label i c l b c0: + (b, c0) = to_bblock (i :: c) + -> In l (header b) + -> i <> Mlabel l + -> exists l2, i=Mlabel l2. 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. + 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 H; inversion H; subst; clear H; simpl. + destruct i; try (simpl in Heqbh; inversion Heqbh; subst; clear Heqbh; simpl; intuition eauto). 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)). +Lemma find_label_stop c: + forall l b c0 c', + (b, c0) = to_bblock c + -> Mach.find_label l c = Some c' + -> In l (header b) + -> exists h, In l h /\ Some (b :: trans_code c0) = Some (concat h (trans_code c')). Proof. - destruct i; simpl; intros H; inversion H; try (constructor 2; intuition auto; discriminate). - constructor 1; eapply ex_intro; intuition eauto. + induction c as [ |i c]. + - simpl; intros; discriminate. + - intros l b c0 c' H H1 H2. + exploit Mach_find_label_split; eauto; clear H1. + intros [(X1 & X2) | (X1 & X2)]. + * subst. exploit to_bblock_label; eauto. clear H. + intros (H3 & H4). constructor 1 with (x:=l::nil); simpl; intuition auto. + symmetry. + rewrite trans_code_equation. + destruct c as [ |i c]. + + unfold to_bblock in H4; simpl in H4. + injection H4. clear H4; intros H4 H H0 H1; subst. simpl. + rewrite trans_code_equation; simpl. + rewrite <- H1 in H3; clear H1. + destruct b as [h b e]; simpl in * |- *; subst; auto. + + rewrite H4; clear H4; simpl. rewrite <- H3; clear H3. + destruct b; simpl; auto. + * exploit to_bblock_start_label; eauto. + intros (l' & H'). subst. + assert (X: l' <> l). { intro Z; subst; destruct X1; auto. } + clear X1. + exploit to_bblock_label; eauto. clear H. + intros (H3 & H4). + exploit IHc; eauto. { simpl. rewrite H3 in H2; simpl in H2. destruct H2; subst; tauto. } + intros (h' & H5 & H6). + constructor 1 with (x:=l'::h'); simpl; intuition auto. + destruct b as [h b e]; simpl in * |- *; subst. + remember (tl h) as th. subst h. + remember (trans_code c') as tcc'. + rewrite trans_code_equation in Heqtcc'. + destruct c'; subst; simpl in * |- *. + + inversion H6; subst; auto. + + destruct (to_bblock (i :: c')) as [b1 c1]. simpl in * |- *. + inversion H6; subst; auto. 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. +Lemma to_bblock_header_find_label c l: forall c1 h c', + to_bblock_header c = (h, c1) + -> Mach.find_label l c = Some c' + -> ~ In l h + -> 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. + induction c as [|i c]; simpl; auto. + - intros; discriminate. + - destruct i; + try (simpl; intros c1 h c' H1 H2; inversion H1; subst; clear H1; intros; apply refl_equal). + remember (to_bblock_header c) as tbhc. destruct tbhc as [h2 c2]. + intros h c1 c' H1; inversion H1; subst; clear H1. + simpl. destruct (peq _ _). + + subst; tauto. + + intros H1 H2; erewrite IHc; eauto. Qed. -Lemma to_bblock_body_find_label c2 bdy l c1: +Lemma to_bblock_body_find_label c1 l: forall c2 bdy, (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 ( @@ -283,7 +255,7 @@ Proof. inversion H; subst; clear H; simpl; erewrite IHc1; eauto; fail). Qed. -Lemma to_bblock_exit_find_label c2 ext l c1: +Lemma to_bblock_exit_find_label c1 l c2 ext: (ext, c2) = to_bblock_exit c1 -> Mach.find_label l c1 = Mach.find_label l c2. Proof. @@ -293,43 +265,37 @@ Proof. 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'). + exists h, In l h /\ find_label l (trans_code c) = Some (concat h (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. + 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]. + simpl; injection e0; intros; subst; clear e0. + unfold is_label; simpl; destruct (in_dec l h) as [Y|Y]. + + clear IHc0. + eapply find_label_stop; eauto. + unfold to_bblock. + rewrite <- Heqbh, <- Heqbb, <- Heqbe. + auto. + + exploit IHc0; eauto. clear IHc0. + rewrite <- H. + erewrite (to_bblock_header_find_label (i::c) l c1); eauto. + erewrite (to_bblock_body_find_label c1 l c2); eauto. + erewrite (to_bblock_exit_find_label c2 l c0); 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). + exists h, In l h /\ find_label l (fn_code (trans_function f)) = Some (concat h (trans_code c)). Proof. intros. cutrewrite ((fn_code (trans_function f)) = trans_code (Mach.fn_code f)); eauto. apply find_label_transcode_preserved; auto. @@ -357,15 +323,6 @@ Definition dist_end_block (s: Mach.state): nat := 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 |- _ ] => @@ -384,13 +341,13 @@ Ltac totologize H := (* 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. + dist_end_block_code (i::c) <> 0 -> + (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)). Proof. - intros. + intros H. 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. + - 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; @@ -408,16 +365,19 @@ Proof. | 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. + unfold dist_end_block_code in * |- *. subst i0. + rewrite (to_bblock_size_single_label c (Mlabel l)) in * |- *; simpl in * |- *; auto. omega. (* 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. +*) +Admitted. Local Hint Resolve dist_end_block_code_simu_mid_block. @@ -468,12 +428,33 @@ Proof. intros X; inversion_clear X. intuition eauto. Qed. +Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit. +Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same. + +Lemma match_states_concat_trans_code st f sp c rs m h: + match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m). +Proof. + constructor 1; simpl. + + intros (t0 & s1' & H0) t s'. + rewrite! trans_code_equation. + destruct c as [| i c]. { inversion H0. } + remember (to_bblock (i :: c)) as bic. destruct bic as [b c0]. + simpl. + constructor 1; intros H; inversion H; subst; simpl in * |- *; + eapply exec_bblock; eauto. + - inversion H11; subst; eauto. + inversion H2; subst; eauto. + - inversion H11; subst; simpl; eauto. + inversion H2; subst; simpl; eauto. + + intros H r; constructor 1; intro X; inversion X. +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'). + exists s2, cfi_step rao tge e (State (trans_stack stk) f sp (b::lb') rs m) t s2 /\ match_states s' s2. Proof. intros c e c' stk f sp rs m t s' b lb'. intros Hexit Htc Hstep. @@ -482,38 +463,66 @@ Proof. inversion Hexit; subst; inversion Hstep; subst; simpl ). * unfold inv_trans_rao in H11. + eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. 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. + * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. + 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. + * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. + eapply exec_MBbuiltin; eauto. + * exploit find_label_transcode_preserved; eauto. intros (h & X1 & X2). + eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. + * exploit find_label_transcode_preserved; eauto. intros (h & X1 & X2). + eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. + * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. + eapply exec_MBcond_false; eauto. + * exploit find_label_transcode_preserved; eauto. intros (h & X1 & X2). + eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. + * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. + eapply exec_MBreturn; 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 step_simu_exit_step c e c' stk f sp rs m t s' b: + to_bblock_exit c = (e, c') -> + starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt e) (Mach.State stk f sp c rs m) t s' -> + exists s2, exit_step rao tge e (State (trans_stack stk) f sp (b::trans_code c') rs m) t s2 /\ match_states s' s2. +Proof. + intros H1 H2; destruct e as [ e |]; inversion_clear H2. + + (* Some *) inversion H0; clear H0; subst. autorewrite with trace_rewrite. + exploit step_simu_cfi_step; eauto. + intros (s2' & H2 & H3); eapply ex_intro; intuition eauto. + + (* None *) + destruct c as [ |i c]; simpl in H1; inversion H1. + - eapply ex_intro; intuition eauto; try eapply match_states_trans_state. + - remember to_cfi as o. destruct o; try discriminate. + inversion_clear H1. + eapply ex_intro; intuition eauto; try eapply match_states_trans_state. +Qed. + +Lemma step_simu_header st f sp rs m s c: forall h c' t, + (h, c') = to_bblock_header c -> + starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> s = Mach.State st f sp c' rs m /\ t = E0. +Proof. + induction c as [ | i c]; simpl; intros h c' t H. + - inversion_clear H. simpl; intros H; inversion H; auto. + - destruct i; try (injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst; auto). + remember (to_bblock_header c) as bhc. destruct bhc as [h0 c0]. + injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst. + inversion H1; clear H1; subst; auto. autorewrite with trace_rewrite. + exploit IHc; eauto. +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'). + exists s2', step rao tge (trans_state s1) t s2' /\ match_states s1' s2'. Proof. destruct s1; simpl. + (* State *) @@ -545,10 +554,6 @@ Proof. 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]. @@ -560,49 +565,27 @@ Proof. 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. + exploit step_simu_header; eauto. + intros [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. - + subst tc0. + exploit step_simu_exit_step; eauto. clear H3. + intros (s2' & H3 & H4). + eapply ex_intro; intuition eauto. + eapply exec_bblock; eauto. + (* Callstate *) intros t s1' H; inversion_clear H. + eapply ex_intro; constructor 1; eauto. 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 *) @@ -610,9 +593,9 @@ Proof. 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. + eapply ex_intro; constructor 1; eauto. inversion H1; subst; clear H1. inversion_clear H0; simpl. eapply exec_return. @@ -620,14 +603,17 @@ 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). + apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := 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. + - intros. simpl. + eapply ex_intro; constructor 1. + eapply match_states_trans_state. + destruct H. split. apply init_mem_preserved; auto. rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. (* match_final_states *) |