Machblock: Mach language with basic blocks

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.