intermediatet commit before builtins

1 files changed, 1009 insertions, 40 deletions

diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 33acc110..55f50b7a 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -1,12 +1,24 @@
-(** Correctness proof for aarch64/Asmblock generation: main proof. 
-CURRENTLY A STUB !
-*)
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
 
 Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock IterList.
-Require Import Asmblockgen Asmblockgenproof0.
+Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
 
 Module MB := Machblock.
 Module AB := Asmblock.
@@ -44,13 +56,16 @@ Lemma functions_translated:
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
 Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
-Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
-  Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
-
-(*Lemma functions_bound_max_pos: forall fb f,
+Lemma functions_transl:
+  forall fb f tf,
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  (max_pos next f) <= Ptrofs.max_unsigned.
-Admitted.*)
+  transf_function f = OK tf ->
+  Genv.find_funct_ptr tge fb = Some (Internal tf).
+Proof.
+  intros. exploit functions_translated; eauto. intros [tf' [A B]].
+  monadInv B. unfold transf_function in H0. monadInv H0.
+  destruct zlt; try discriminate. rewrite EQ in EQ0. inv EQ0; inv EQ1; auto.
+Qed.
 
 Lemma transf_function_no_overflow:
   forall f tf,
@@ -60,6 +75,14 @@ Proof.
   omega.
 Qed.
 
+Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
+  Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
+
+(*Lemma functions_bound_max_pos: forall fb f,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  (max_pos next f) <= Ptrofs.max_unsigned.
+Admitted.*)
+
 (** * Proof of semantic preservation *)
 
 (** Semantic preservation is proved using a complex simulation diagram
@@ -118,6 +141,183 @@ Inductive match_states: Machblock.state -> Asm.state -> Prop :=
       match_states (Machblock.Returnstate s ms m)
                    (Asm.State rs m').
 
+Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *)
+
+Lemma cons_bblocks_label:
+  forall hd bdy ex tbb tc,
+  cons_bblocks hd bdy ex = tbb::tc ->
+  header tbb = hd.
+Proof.
+  intros until tc. intros CONSB. unfold cons_bblocks in CONSB.
+  destruct ex; try destruct bdy; try destruct c; try destruct i.
+  all: inv CONSB; simpl; auto.
+Qed.
+
+Lemma cons_bblocks_label2:
+  forall hd bdy ex tbb1 tbb2,
+  cons_bblocks hd bdy ex = tbb1::tbb2::nil ->
+  header tbb2 = nil.
+Proof.
+  intros until tbb2. intros CONSB. unfold cons_bblocks in CONSB.
+  destruct ex; try destruct bdy; try destruct c; try destruct i.
+  all: inv CONSB; simpl; auto.
+Qed.
+
+Remark in_dec_transl:
+  forall lbl hd,
+  (if in_dec lbl hd then true else false) = (if MB.in_dec lbl hd then true else false).
+Proof.
+  intros. destruct (in_dec lbl hd), (MB.in_dec lbl hd). all: tauto.
+Qed.
+
+Lemma transl_is_label:
+  forall lbl bb tbb f ep tc,
+  transl_block f bb ep = OK (tbb::tc) ->
+  is_label lbl tbb = MB.is_label lbl bb.
+Proof.
+  intros until tc. intros TLB.
+  destruct tbb as [thd tbdy tex]; simpl in *.
+  monadInv TLB.
+  unfold is_label. simpl.
+  apply cons_bblocks_label in H0. simpl in H0. subst.
+  rewrite in_dec_transl. auto.
+Qed.
+
+Lemma transl_is_label_false2:
+  forall lbl bb f ep tbb1 tbb2,
+  transl_block f bb ep = OK (tbb1::tbb2::nil) ->
+  is_label lbl tbb2 = false.
+Proof.
+  intros until tbb2. intros TLB.
+  destruct tbb2 as [thd tbdy tex]; simpl in *.
+  monadInv TLB. apply cons_bblocks_label2 in H0. simpl in H0. subst.
+  apply is_label_correct_false. simpl. auto.
+Qed.
+
+(*
+Lemma transl_is_label2:
+  forall f bb ep tbb1 tbb2 lbl,
+  transl_block f bb ep = OK (tbb1::tbb2::nil) ->
+     is_label lbl tbb1 = MB.is_label lbl bb
+  /\ is_label lbl tbb2 = false.
+Proof.
+  intros. split. eapply transl_is_label; eauto. eapply transl_is_label_false2; eauto.
+Qed. *)
+
+Lemma transl_block_nonil:
+  forall f c ep tc,
+  transl_block f c ep = OK tc ->
+  tc <> nil.
+Proof.
+  intros. monadInv H. unfold cons_bblocks.
+  destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i.
+  all: discriminate.
+Qed.
+
+Lemma transl_block_limit: forall f bb ep tbb1 tbb2 tbb3 tc,
+  ~transl_block f bb ep = OK (tbb1 :: tbb2 :: tbb3 :: tc).
+Proof.
+  intros. intro. monadInv H.
+  unfold cons_bblocks in H0.
+  destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i.
+  all: discriminate.
+Qed.
+
+Lemma find_label_transl_false:
+  forall x f lbl bb ep x',
+  transl_block f bb ep = OK x ->
+  MB.is_label lbl bb = false ->
+  find_label lbl (x++x') = find_label lbl x'.
+Proof.
+  intros until x'. intros TLB MBis; simpl; auto.
+  destruct x as [|x0 x1]; simpl; auto.
+  destruct x1 as [|x1 x2]; simpl; auto.
+  - erewrite <- transl_is_label in MBis; eauto. rewrite MBis. auto.
+  - destruct x2 as [|x2 x3]; simpl; auto.
+    + erewrite <- transl_is_label in MBis; eauto. rewrite MBis.
+      erewrite transl_is_label_false2; eauto.
+    + apply transl_block_limit in TLB. destruct TLB.
+Qed.
+
+Lemma transl_blocks_label:
+  forall lbl f c tc ep,
+  transl_blocks f c ep = OK tc ->
+  match MB.find_label lbl c with
+  | None => find_label lbl tc = None
+  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_blocks f c' false = OK tc'
+  end.
+Proof.
+  induction c; simpl; intros.
+  inv H. auto.
+  monadInv H.
+  destruct (MB.is_label lbl a) eqn:MBis.
+  - destruct x as [|tbb tc]. { apply transl_block_nonil in EQ. contradiction. }
+    simpl find_label. exploit transl_is_label; eauto. intros ABis. rewrite MBis in ABis.
+    rewrite ABis.
+    eexists. eexists. split; eauto. simpl transl_blocks.
+    assert (MB.header a <> nil).
+    { apply MB.is_label_correct_true in MBis.
+      destruct (MB.header a). contradiction. discriminate. }
+    destruct (MB.header a); try contradiction.
+    rewrite EQ. simpl. rewrite EQ1. simpl. auto.
+  - apply IHc in EQ1. destruct (MB.find_label lbl c).
+    + destruct EQ1 as (tc' & FIND & TLBS). exists tc'; eexists; auto.
+      erewrite find_label_transl_false; eauto.
+    + erewrite find_label_transl_false; eauto.
+Qed.
+
+Lemma find_label_nil:
+  forall bb lbl c,
+  header bb = nil ->
+  find_label lbl (bb::c) = find_label lbl c.
+Proof.
+  intros. destruct bb as [hd bdy ex]; simpl in *. subst.
+  assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false).
+  { erewrite <- is_label_correct_false. simpl. auto. }
+  rewrite H. auto.
+Qed.
+
+Theorem transl_find_label:
+  forall lbl f tf,
+  transf_function f = OK tf ->
+  match MB.find_label lbl f.(MB.fn_code) with
+  | None => find_label lbl tf.(fn_blocks) = None
+  | Some c => exists tc, find_label lbl tf.(fn_blocks) = Some tc /\ transl_blocks f c false = OK tc
+  end.
+Proof.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); inv EQ0. clear g.
+  monadInv EQ. unfold make_prologue. simpl fn_blocks. repeat (rewrite find_label_nil); simpl; auto.
+  eapply transl_blocks_label; eauto.
+Qed.
+
+End TRANSL_LABEL.
+(** A valid branch in a piece of Machblock code translates to a valid ``go to''
+  transition in the generated Asmblock code. *)
+
+Lemma find_label_goto_label:
+  forall f tf lbl rs m c' b ofs,
+  Genv.find_funct_ptr ge b = Some (Internal f) ->
+  transf_function f = OK tf ->
+  rs PC = Vptr b ofs ->
+  MB.find_label lbl f.(MB.fn_code) = Some c' ->
+  exists tc', exists rs',
+    goto_label tf lbl rs m = Next rs' m
+  /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc'
+  /\ forall r, r <> PC -> rs'#r = rs#r.
+Proof.
+  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2.
+  intros (tc & A & B).
+  exploit label_pos_code_tail; eauto. instantiate (1 := 0).
+  intros [pos' [P [Q R]]].
+  exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
+  split. unfold goto_label. rewrite P. rewrite H1. auto.
+  split. rewrite Pregmap.gss. constructor; auto.
+  rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
+  auto. omega.
+  generalize (transf_function_no_overflow _ _ H0). omega.
+  intros. apply Pregmap.gso; auto.
+Qed.
+
 (** Existence of return addresses *)
 
 Lemma return_address_exists:
@@ -144,11 +344,6 @@ Ltac exploreInst :=
   | [ H : bind _ _ = OK _ |- _ ] => monadInv H
   | [ H : Error _ = OK _ |- _ ] => inversion H
   end.
-  
-Ltac desif :=
-  repeat match goal with
-  | [ |- context[if ?f then _ else _ ] ] => destruct f
-  end.
 
 (** Some translation properties *)
 
@@ -488,6 +683,688 @@ Proof.
   all: simpl; auto.
 Qed.
 
+Lemma exec_straight_body:
+  forall c c' rs1 m1 rs2 m2,
+  exec_straight tge lk c rs1 m1 c' rs2 m2 ->
+  exists l,
+     c = l ++ c'
+  /\ exec_body lk tge l rs1 m1 = Next rs2 m2.
+Proof.
+  induction c; try (intros; inv H; fail).
+  intros until m2. intros EXES. inv EXES.
+  - exists (a :: nil). repeat (split; simpl; auto). rewrite H6. auto.
+  - eapply IHc in H7; eauto. destruct H7 as (l' & Hc & EXECB). subst.
+    exists (a :: l'). repeat (split; simpl; auto).
+    rewrite H1. auto.
+Qed.
+
+Lemma exec_straight_body2:
+  forall c rs1 m1 c' rs2 m2,
+  exec_straight tge lk c rs1 m1 c' rs2 m2 ->
+  exists body,
+     exec_body lk tge body rs1 m1 = Next rs2 m2
+  /\ body ++ c' = c.
+Proof.
+  intros until m2. induction 1.
+  - exists (i1::nil). split; auto. simpl. rewrite H. auto.
+  - destruct IHexec_straight as (bdy & EXEB & BTC).
+    exists (i:: bdy). split; simpl.
+    + rewrite H. auto.
+    + congruence.
+Qed.
+
+Lemma exec_straight_opt_body2:
+  forall c rs1 m1 c' rs2 m2,
+  exec_straight_opt tge lk c rs1 m1 c' rs2 m2 ->
+  exists body,
+     exec_body lk tge body rs1 m1 = Next rs2 m2
+  /\ body ++ c' = c.
+Proof.
+  intros until m2. intros EXES.
+  inv EXES.
+  - exists nil. split; auto.
+  - eapply exec_straight_body2. auto.
+Qed.
+
+Lemma PC_not_data_preg: forall r ,
+  data_preg r = true ->
+  r <> PC.
+Proof.
+  intros. destruct (PregEq.eq r PC); [ rewrite e in H; simpl in H; discriminate | auto ].
+Qed.
+
+Lemma X30_not_data_preg: forall r ,
+  data_preg r = true ->
+  r <> X30.
+Proof.
+  intros. destruct (PregEq.eq r X30); [ rewrite e in H; simpl in H; discriminate | auto ].
+Qed.
+
+Ltac Simpl :=
+  rewrite Pregmap.gso; try apply PC_not_data_preg; try apply X30_not_data_preg.
+  
+Ltac ArgsInv :=
+  repeat (match goal with
+  | [ H: Error _ = OK _ |- _ ] => discriminate
+  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
+  | [ H: bind _ _ = OK _ |- _ ] => monadInv H
+  | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
+  | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
+  end);
+  subst;
+  repeat (match goal with
+  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *
+  | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
+  end).
+  
+(* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are
+   unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by
+   yourself the steps *)
+Theorem step_simu_control:
+  forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2,
+  MB.body bb' = nil ->
+  (forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) ->
+  Genv.find_funct_ptr tge fb = Some (Internal fn) ->
+  pstate cs2 = (State rs2 m2) ->
+  pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->
+  cur cs2 = tbb ->
+  match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->
+  match_asmstate fb cs2 (State rs1 m1) ->
+  exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') t S'' ->
+  (exists rs3 m3 rs4 m4,
+      exec_body lk tge tbdy2 rs2 m2 = Next rs3 m3
+  /\  exec_exit tge fn (Ptrofs.repr (size tbb)) rs3 m3 tex t rs4 m4
+  /\  match_states S'' (State rs4 m4)).
+Proof. Admitted. (*
+  intros until cs2. intros Hbody Hbuiltin FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP.
+  inv ESTEP.
+  - inv MCS. inv MAS. simpl in *.
+    inv Hpstate.
+    destruct ctl.
+    + (* MBcall *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+        eapply transf_function_no_overflow; eauto.
+      destruct s1 as [rf|fid]; simpl in H1.
+      * (* Indirect call *)
+        monadInv H1. monadInv EQ.
+        assert (ms' rf = Vptr f' Ptrofs.zero).
+        { unfold find_function_ptr in H12. destruct (ms' rf); try discriminate.
+          revert H12; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
+        assert (rs2 x = Vptr f' Ptrofs.zero).
+        { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. }
+        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
+        remember (Ptrofs.add _ _) as ofs'.
+        assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
+        { econstructor; eauto. }
+        assert (f1 = f) by congruence. subst f1.
+        exploit return_address_offset_correct; eauto. intros; subst ra.
+
+        repeat eexists.
+        econstructor; eauto. econstructor.
+          econstructor; eauto. econstructor; eauto.
+          eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros.
+          unfold incrPC; repeat Simpl; auto.
+          simpl. unfold incrPC; rewrite Pregmap.gso; auto; try discriminate.
+          rewrite !Pregmap.gss. rewrite PCeq. rewrite Heqofs'. simpl. auto.
+
+      * (* Direct call *)
+        monadInv H1.
+        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
+        remember (Ptrofs.add _ _) as ofs'.
+        assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
+          econstructor; eauto.
+        assert (f1 = f) by congruence. subst f1.
+        exploit return_address_offset_correct; eauto. intros; subst ra.
+        repeat eexists.
+        econstructor; eauto. econstructor.
+          econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros.
+        unfold incrPC; repeat Simpl; auto. unfold Genv.symbol_address. rewrite symbols_preserved. simpl in H12. rewrite H12. auto.
+        unfold incrPC; simpl; rewrite Pregmap.gso; try discriminate. rewrite !Pregmap.gss.
+        subst. unfold Val.offset_ptr. rewrite PCeq. auto.
+    + (* MBtailcall *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence.  subst f0.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+        eapply transf_function_no_overflow; eauto.
+      exploit Mem.loadv_extends. eauto. eexact H13. auto. simpl. intros [parent' [A B]].
+      destruct s1 as [rf|fid]; simpl in H11. 
+      * monadInv H1. monadInv EQ.
+        assert (ms' rf = Vptr f' Ptrofs.zero).
+          { destruct (ms' rf); try discriminate. revert H11. predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
+        assert (rs2 x = Vptr f' Ptrofs.zero).
+          { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. }
+
+        assert (f = f1) by congruence. subst f1. clear FIND1. clear H12.
+        exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
+        exploit exec_straight_body; eauto.
+        intros (l & MKEPI & EXEB).
+        repeat eexists. rewrite app_nil_r in MKEPI.
+        rewrite <- MKEPI in EXEB.
+        eauto. econstructor. simpl. unfold incrPC.
+        rewrite !Pregmap.gso; try discriminate. eauto.
+        econstructor; eauto.
+          { apply agree_set_other.
+            - econstructor; auto with asmgen.
+              + apply V.
+              + intro r. destruct r; apply V; auto.
+            - eauto with asmgen. }
+        rewrite Pregmap.gss. rewrite Z; auto; try discriminate.
+        eapply ireg_of_not_X30''; eauto.
+        eapply ireg_of_not_X16''; eauto.
+      * monadInv H1. assert (f = f1) by congruence. subst f1. clear FIND1. clear H12.
+        exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
+        exploit exec_straight_body; eauto.
+        intros (l & MKEPI & EXEB).
+        repeat eexists. inv EQ. rewrite app_nil_r in MKEPI.
+        rewrite <- MKEPI in EXEB.
+        eauto. inv EQ. econstructor. simpl. unfold incrPC.
+        eauto.
+        econstructor; eauto.
+        { apply agree_set_other.
+          - econstructor; auto with asmgen.
+            + apply V.
+            + intro r. destruct r; apply V; auto.
+          - eauto with asmgen. }
+        { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. }
+    + (* MBbuiltin (contradiction) *)
+      assert (MB.exit bb' <> Some (MBbuiltin e l b)) by (apply Hbuiltin).
+      rewrite <- H in H1. contradict H1; auto.
+    + (* MBgoto *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0. assert (f1 = f) by congruence. subst f1. clear H9.
+      remember (incrPC (Ptrofs.repr (size tbb)) rs2) as rs2'.
+      exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND'.
+      assert (tf = fn) by congruence. subst tf.
+      exploit find_label_goto_label.
+        eauto. eauto.
+        instantiate (2 := rs2').
+        { subst. unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. eauto. }
+        eauto.
+      intros (tc' & rs' & GOTO & AT2 & INV).
+
+      eexists. eexists. repeat eexists. repeat split.
+      econstructor; eauto.
+        rewrite Heqrs2' in INV. unfold incrPC in INV.
+        rewrite Heqrs2' in GOTO; simpl; eauto.
+        econstructor; eauto.
+        eapply agree_exten; eauto with asmgen.
+        assert (forall r : preg, r <> PC -> rs' r = rs2 r).
+        { intros. rewrite Heqrs2' in INV.
+          rewrite INV; unfold incrPC; try rewrite Pregmap.gso; auto. }
+        eauto with asmgen.
+        congruence.
+    + (* MBcond *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      * (* MBcond true *)
+        assert (f0 = f) by congruence. subst f0.
+        exploit eval_condition_lessdef.
+          eapply preg_vals; eauto.
+          all: eauto.
+        intros EC. monadInv H1.
+        unfold transl_cond_branch in EQ. ArgsInv.
+        { unfold transl_cond_branch_default in EQ. monadInv EQ. unfold transl_cond in EQ0.
+          destruct c0; try discriminate. }
+        { destruct c0; ArgsInv;
+          try (unfold transl_cond_branch_default, transl_cond in EQ; try monadInv EQ; discriminate).
+          - destruct c0.
+            3:{ unfold transl_cond_branch_default, transl_cond in EQ. monadInv EQ. monadInv EQ0.
+            repeat eexists. destruct is_arith_imm32.
+            - simpl. eauto.
+            - destruct is_arith_imm32; simpl; eauto.
+            
+            discriminate.
+          destruct c0; ArgsInv. unfold transl_cond_branch_default in EQ; try monadInv EQ; try unfold transl_cond in EQ0;
+          try discriminate.
+        { destruct c0; try discriminate. }
+        
+        
+        { monadInv EQ. unfold transl_cond in EQ0. destruct c0; try discriminate. }
+        { apply IHl. discriminate.
+          { destruct l, c0; simpl in *; try congruence.
+        destruct c0; simpl. simpl in EQ. monadInv EQ.
+        
+        exploit (transl_cbranch_correct); eauto. intros (rsX & mX & rsY & mY & A & B & C).
+        
+        exists rsX. exists mX. exists rsY. exists mY. split. eauto. eauto.
+
+        assert (PCeq': rs2 PC = rs' PC). { admit. (* inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. *) }
+        rewrite PCeq' in PCeq.
+        assert (f1 = f) by congruence. subst f1.
+        exploit find_label_goto_label.
+          4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')). unfold incrPC.
+          rewrite Pregmap.gss.
+          unfold Val.offset_ptr. rewrite PCeq. eauto.
+        intros (tc' & rs3 & GOTOL & TLPC & Hrs3).
+        exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
+        assert (tf = fn) by congruence. subst tf.
+
+        repeat eexists.
+          rewrite <- BTC. simpl. rewrite app_nil_r. eauto.
+          eapply (cfi_step tge fn (Ptrofs.repr (size tbb)) rs' m2 (Some x0) E0 _ _). rewrite <- BTC. simpl. econstructor. rewrite B. eauto.
+
+        econstructor; eauto.
+          eapply agree_exten with rs2; eauto with asmgen.
+          { intros. destruct r; try destruct g; try discriminate.
+            all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. }
+        intros. discriminate.
+
+      * (* MBcond false *)
+        assert (f0 = f) by congruence. subst f0.
+        exploit eval_condition_lessdef.
+          eapply preg_vals; eauto.
+          all: eauto.
+        intros EC.
+
+        exploit transl_cbranch_correct_false; eauto. intros (rs' & jmp & A & B & C).
+        exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
+        assert (PCeq': rs2 PC = rs' PC). { inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. }
+        rewrite PCeq' in PCeq.
+        exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
+        assert (tf = fn) by congruence. subst tf.
+
+        assert (NOOV: size_blocks fn.(fn_blocks) <= Ptrofs.max_unsigned).
+          eapply transf_function_no_overflow; eauto.
+        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
+
+        repeat eexists.
+          rewrite H6. rewrite <- BTC. rewrite extract_basics_to_code. simpl. rewrite app_nil_r. eauto.
+          rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto.
+
+        econstructor; eauto.
+          unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.
+          eapply agree_exten with rs2; eauto with asmgen.
+          { intros. destruct r; try destruct g; try discriminate.
+            all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. }
+        intros. discriminate.
+    + (* MBjumptable *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0.
+      monadInv H1.
+      generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.
+      assert (f1 = f) by congruence. subst f1.
+      exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).
+        unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.
+      exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.
+
+      intros [tc' [rs' [A [B C]]]].
+      exploit ireg_val; eauto. rewrite H13. intros LD; inv LD.
+      
+      repeat eexists.
+        rewrite H6. simpl extract_basic. simpl. eauto.
+        rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A.
+      econstructor; eauto.
+        eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.
+        { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0.
+          destruct (preg_eq r' GPR63). subst. contradiction.
+          destruct (preg_eq r' GPR62). subst. contradiction.
+          destruct r'; Simpl. }
+        discriminate.
+    + (* MBreturn *)
+      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+        eapply transf_function_no_overflow; eauto.
+      exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
+      exploit exec_straight_body; eauto.
+        simpl. eauto.
+      intros EXEB.
+      assert (f1 = f) by congruence. subst f1.
+      
+      repeat eexists.
+        rewrite H6. simpl extract_basic. eauto.
+        rewrite H7. simpl extract_ctl. simpl. reflexivity.
+      econstructor; eauto.
+        unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen.
+
+  - inv MCS. inv MAS. simpl in *. subst. inv Hpstate.
+    destruct bb' as [hd' bdy' ex']; simpl in *. subst.
+    monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6.
+    simpl. repeat eexists.
+    econstructor. 4: instantiate (3 := false). all:eauto.
+      unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq.
+      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+        eapply transf_function_no_overflow; eauto.
+      assert (f = f0) by congruence. subst f0. econstructor; eauto.
+      generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto.
+    eapply agree_exten; eauto. intros. Simpl.
+    discriminate.
+Qed.*)
+
+(* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *)
+Theorem step_simu_basic:
+  forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy,
+  MB.header bb = nil -> MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
+  bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} ->
+  basic_step ge s fb sp ms m bi ms' m' ->
+  pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy ->
+  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
+  (exists rs2 m2 l cs2 tbdy',
+       cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := tbdy'; pbody2 := pbody2 cs1;
+                pctl := pctl cs1; ep := it1_is_parent (ep cs1) bi; rem := rem cs1; cur := cur cs1 |}
+    /\ tbdy = l ++ tbdy'
+    /\ exec_body lk tge l rs1 m1 = Next rs2 m2
+    /\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2).
+Proof.
+  intros until bdy. intros Hheader Hbody Hnobuiltin (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS.
+  simpl in *. inv Hpstate.
+  rewrite Hbody in TBC. monadInv TBC.
+  inv BSTEP.
+
+  - (* MBgetstack *)
+    simpl in EQ0.
+    unfold Mach.load_stack in H.
+    exploit Mem.loadv_extends; eauto. intros [v' [A B]].
+    rewrite (sp_val _ _ _ AG) in A.
+    exploit loadind_correct; eauto with asmgen.
+    intros (rs2 & EXECS & Hrs'1 & Hrs'2).
+    eapply exec_straight_body in EXECS.
+    destruct EXECS as (l & Hlbi & EXECB).
+    exists rs2, m1, l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }
+    subst. simpl in Hheadereq.
+
+    eapply match_codestate_intro; eauto.
+    eapply agree_set_mreg; eauto with asmgen.
+    intro Hep. simpl in Hep. discriminate.
+  - (* MBsetstack *)
+    simpl in EQ0.
+    unfold Mach.store_stack in H.
+    assert (Val.lessdef (ms src) (rs1 (preg_of src))). { eapply preg_val; eauto. }
+    exploit Mem.storev_extends; eauto. intros [m2' [A B]].
+    exploit storeind_correct; eauto with asmgen.
+    rewrite (sp_val _ _ _ AG) in A. eauto. intros [rs' [P Q]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs', m2', l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    subst.
+    eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
+    eapply agree_undef_regs; eauto with asmgen.
+    simpl; intros. rewrite Q; auto with asmgen. rewrite Hheader in DXP. auto.
+  - (* MBgetparam *)
+    simpl in EQ0.
+
+    assert (f0 = f) by congruence; subst f0.
+    unfold Mach.load_stack in *.
+    exploit Mem.loadv_extends. eauto. eexact H0. auto.
+    intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+    exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
+    exploit Mem.loadv_extends. eauto. eexact H1. auto.
+    intros [v' [C D]].
+
+    monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP.
+    destruct ep0 eqn:EPeq.
+
+  (* X29 contains parent *)
+    + exploit loadind_correct. eexact EQ1.
+      instantiate (2 := rs1). rewrite DXP; eauto. discriminate.
+      intros [rs2 [P [Q R]]].
+
+      eapply exec_straight_body in P.
+      destruct P as (l & ll & EXECB).
+      exists rs2, m1, l. eexists.
+      eexists. split. instantiate (1 := x). eauto.
+      repeat (split; auto).
+      remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+      assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }
+      subst.
+      eapply match_codestate_intro; eauto.
+
+      eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
+      simpl; intros. rewrite R; auto with asmgen. unfold preg_of.
+      apply preg_of_not_X29; auto.
+
+  (* X29 does not contain parent *)
+    + rewrite chunk_of_Tptr in A. 
+      exploit loadptr_correct. eexact A. discriminate. intros [rs2 [P [Q R]]].
+      exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto.
+      discriminate.
+      intros [rs3 [S [T U]]].
+
+      exploit exec_straight_trans.
+        eapply P.
+        eapply S.
+      intros EXES.
+
+      eapply exec_straight_body in EXES.
+      destruct EXES as (l & ll & EXECB).
+      exists rs3, m1, l.
+      eexists. eexists. split. instantiate (1 := x). eauto.
+      repeat (split; auto).
+      remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+      assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+      subst.
+      eapply match_codestate_intro; eauto.
+      eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
+      instantiate (1 := rs2#X29 <- (rs3#X29)). intros.
+      rewrite Pregmap.gso; auto with asmgen.
+      congruence.
+      intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
+      simpl; intros. rewrite U; auto with asmgen.
+      apply preg_of_not_X29; auto.
+  - (* MBop *)
+    simpl in EQ0. rewrite Hheader in DXP.
+    
+    assert (eval_operation tge sp op (map ms args) m' = Some v).
+      rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
+    exploit eval_operation_lessdef.
+      eapply preg_vals; eauto.
+      2: eexact H0.
+      all: eauto.
+    intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+    exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs2, m1, l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    subst.
+    eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
+    apply agree_set_undef_mreg with rs1; auto. 
+    apply Val.lessdef_trans with v'; auto.
+    simpl; intros. destruct (andb_prop _ _ H1); clear H1.
+    rewrite R; auto. apply preg_of_not_X29; auto.
+Local Transparent destroyed_by_op.
+    destruct op; simpl; auto; try discriminate.
+  - (* MBload *)
+    simpl in EQ0. rewrite Hheader in DXP.
+
+    assert (Op.eval_addressing tge sp addr (map ms args) = Some a).
+      rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+    exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+    intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+    exploit Mem.loadv_extends; eauto. intros [v' [C D]]. destruct trap; try discriminate.
+    exploit transl_load_correct; eauto.
+    intros [rs2 [P [Q R]]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs2, m1, l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+    subst.
+    eapply match_codestate_intro; eauto.
+    eapply agree_set_mreg; eauto with asmgen.
+    intro Hep. simpl in Hep. discriminate.
+  - (* MBload notrap1 *)
+    simpl in EQ0. unfold transl_load in EQ0. discriminate.
+    (*destruct addr; simpl in H; destruct chunk; monadInv EQ0.
+    all:
+    destruct args as [|h0 t0]; try discriminate;
+    destruct t0 as [|h1 t1]; try discriminate;
+    destruct t1 as [|h2 t2]; try discriminate.*)
+    
+  - (* MBload notrap2 *)
+    simpl in EQ0. unfold transl_load in EQ0. discriminate.
+    (*simpl in EQ0. rewrite Hheader in DXP.
+
+    assert (Op.eval_addressing tge sp addr (map ms args) = Some a).
+      rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+    exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+    intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+    exploit transl_load_correct; eauto.
+    intros [rs2 [P [Q R]]].
+    
+    destruct (Mem.loadv chunk m1 a') as [v' | ] eqn:Hload.
+    {
+    exploit transl_load_correct; eauto.
+    intros [rs2 [P [Q R]]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs2, m1, l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    eapply match_codestate_intro; eauto.
+
+    eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
+
+    simpl in *. discriminate.
+    }
+    {
+    exploit transl_load_correct_notrap2; eauto.
+    intros [rs2 [P [Q R]]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs2, m1, l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+(*     assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+    rewrite <- Hheadereq. *) subst.
+    eapply match_codestate_intro; eauto.
+
+    eapply agree_set_undef_mreg; eauto. intros; auto with asmgen.
+    simpl in *. discriminate.
+    }*)
+  - (* MBstore *)
+    simpl in EQ0. rewrite Hheader in DXP.
+
+    assert (Op.eval_addressing tge sp addr (map ms args) = Some a).
+      rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+    exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+    intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+    assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto.
+    exploit Mem.storev_extends; eauto. intros [m2' [C D]].
+    exploit transl_store_correct; eauto. intros [rs2 [P Q]].
+
+    eapply exec_straight_body in P.
+    destruct P as (l & ll & EXECB).
+    exists rs2, m2', l.
+    eexists. eexists. split. instantiate (1 := x). eauto.
+    repeat (split; auto).
+    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+    subst.
+    eapply match_codestate_intro; eauto.
+    eapply agree_undef_regs; eauto with asmgen.
+    intro Hep. simpl in Hep. discriminate.
+Qed.
+
+Lemma exec_body_trans:
+  forall l l' rs0 m0 rs1 m1 rs2 m2,
+  exec_body lk tge l rs0 m0 = Next rs1 m1 ->
+  exec_body lk tge l' rs1 m1 = Next rs2 m2 ->
+  exec_body lk tge (l++l') rs0 m0 = Next rs2 m2.
+Proof.
+  induction l.
+  - simpl. induction l'. intros.
+    + simpl in *. congruence.
+    + intros. inv H. auto.
+  - intros until m2. intros EXEB1 EXEB2.
+    inv EXEB1. destruct (exec_basic _) eqn:EBI; try discriminate.
+    simpl. rewrite EBI. eapply IHl; eauto.
+Qed.
+
+Lemma exec_body_control:
+  forall b t rs1 m1 rs2 m2 rs3 m3 fn,
+  exec_body lk tge (body b) rs1 m1 = Next rs2 m2 ->
+  exec_exit tge fn (Ptrofs.repr (size b)) rs2 m2 (exit b) t rs3 m3 ->
+  exec_bblock lk tge fn b rs1 m1 t rs3 m3.
+Proof.
+  intros until fn. intros EXEB EXECTL.
+  econstructor; eauto.
+Qed.
+
+Inductive exec_header: codestate -> codestate -> Prop :=
+  | exec_header_cons: forall cs1,
+      exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1;
+                          pctl := pctl cs1; ep := (if pheader cs1 then ep cs1 else false); rem := rem cs1;
+                          cur := cur cs1 |}.
+
+(* Theorem (A) in the diagram, the easiest of all *)
+Theorem step_simu_header:
+  forall bb s fb sp c ms m rs1 m1 cs1,
+  pstate cs1 = (State rs1 m1) ->
+  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
+  (exists cs1',
+       exec_header cs1 cs1'
+    /\ match_codestate fb (MB.State s fb sp (mb_remove_header bb::c) ms m) cs1').
+Proof.
+  intros until cs1. intros Hpstate MCS.
+  eexists. split; eauto.
+  econstructor; eauto.
+  inv MCS. simpl in *. inv Hpstate.
+  econstructor; eauto.
+Qed.
+
+(* Theorem (B) in the diagram, using step_simu_basic + induction on the Machblock body *)
+Theorem step_simu_body:
+  forall bb s fb sp c ms m rs1 m1 ms' cs1 m',
+  MB.header bb = nil ->
+  (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
+  body_step ge s fb sp (MB.body bb) ms m ms' m' ->
+  pstate cs1 = (State rs1 m1) ->
+  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
+  (exists rs2 m2 cs2 ep,
+       cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := nil; pbody2 := pbody2 cs1;
+                pctl := pctl cs1; ep := ep; rem := rem cs1; cur := cur cs1 |}
+    /\ exec_body lk tge (pbody1 cs1) rs1 m1 = Next rs2 m2
+    /\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2).
+Proof.
+  intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy].
+  - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS.
+    inv BSTEP.
+    exists rs1, m1, cs1, (ep cs1).
+    inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto).
+    econstructor; eauto.
+  - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. inv BSTEP.
+    rename ms' into ms''. rename m' into m''. rename rs' into ms'. rename m'0 into m'.
+    exploit (step_simu_basic); eauto. simpl. eauto. simpl; auto. simpl; auto.
+    intros (rs2 & m2 & l & cs2 & tbdy' & Hcs2 & Happ & EXEB & MCS').
+    simpl in *.
+    exploit IHbdy. auto. 2: eapply H6. 3: eapply MCS'. all: eauto. subst; eauto. simpl; auto.
+    intros (rs3 & m3 & cs3 & ep & Hcs3 & EXEB' & MCS'').
+    exists rs3, m3, cs3, ep.
+    repeat (split; simpl; auto). subst. simpl in *. auto.
+    rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.
+Qed.
+
 (* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *)
 (* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *)
 Lemma step_simulation_bblock':
@@ -543,8 +1420,7 @@ Proof.
     assert (exists rs1 m1, pstate cs1 = State rs1 m1). { inv MAS. simpl. eauto. }
     destruct H as (rs1 & m1 & Hpstate2). subst.
     assert (f = fb). { inv MCS. auto. } subst fb.
-    all: admit.
-    (*exploit step_simu_header.
+    exploit step_simu_header.
       2: eapply MCS.
       all: eauto.
     intros (cs1' & EXEH & MCS2).
@@ -561,15 +1437,11 @@ Proof.
     assert (exists tf, Genv.find_funct_ptr tge f = Some (Internal tf)).
     { exploit functions_translated; eauto. intros (tf & FIND' & TRANSF'). monadInv TRANSF'. eauto. }
     destruct H as (tf & FIND').
-    assert (exists tex, pbody2 cs1 = extract_basic tex /\ pctl cs1 = extract_ctl tex).
-    { inv MAS. simpl in *. eauto. }
-    destruct H as (tex & Hpbody2 & Hpctl).
     inv EXEH. simpl in *.
     subst. exploit step_simu_control.
       9: eapply MCS'. all: simpl.
       10: eapply ESTEP.
       all: simpl; eauto.
-      rewrite Hpbody2. rewrite Hpctl.
       { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto.
         erewrite exec_body_pc; eauto. }
     intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS').
@@ -580,14 +1452,14 @@ Proof.
       eauto.
     intros EXEB2.
     exploit exec_body_control; eauto.
-    rewrite <- Hpbody2 in EXEB2. rewrite <- Hbody in EXEB2. eauto.
-    rewrite Hexit. rewrite Hpctl. eauto.
-    intros EXECB. inv EXECB.
+    rewrite <- Hbody in EXEB2. eauto.
+    rewrite Hexit. eauto.
+    intros EXECB. (* inv EXECB. *)
     exists (State rs4 m4).
     split; auto. eapply plus_one. rewrite Hpstate2.
     assert (exists ofs, rs1 PC = Vptr f ofs).
     { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. }
-    destruct H0 as (ofs & Hrs1pc).
+    destruct H as (ofs & Hrs1pc).
     eapply exec_step_internal; eauto.
 
     (* proving the initial find_bblock *)
@@ -595,10 +1467,10 @@ Proof.
     assert (f1 = f0) by congruence. subst f0.
     rewrite PCeq in Hrs1pc. inv Hrs1pc.
     exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''.
-    inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ.
+    inv FIND''. monadInv TRANS''. unfold transf_function in TRANSF0. monadInv TRANSF0.
+    destruct (zlt _ _) in EQ1; try discriminate. rewrite EQ in EQ0. inv EQ0. inv EQ1.
     eapply find_bblock_tail; eauto.
-Qed.*)
-Admitted.
+Qed.
 
 Theorem step_simulation_bblock:
   forall sf f sp bb ms m ms' m' S2 c,
@@ -616,6 +1488,106 @@ Proof.
   - econstructor.
 Qed.
 
+(* Definition split (c: MB.code) :=
+  match c with
+  | nil => nil
+  | bb::c => {| MB.header := MB.header bb; MB.body := MB.body bb; MB.exit := None |}
+              :: {| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |} :: c
+  end.
+  
+Lemma cons_ok_eq3 {A: Type} :
+  forall (x:A) y z x' y' z',
+  x = x' -> y = y' -> z = z' ->
+  OK (x::y::z) = OK (x'::y'::z').
+Proof.
+  intros. subst. auto.
+Qed.
+
+Lemma transl_blocks_split_builtin:
+  forall bb c ep f ef args res,
+  MB.exit bb = Some (MBbuiltin ef args res) -> MB.body bb <> nil ->
+  transl_blocks f (split (bb::c)) ep = transl_blocks f (bb::c) ep.
+Proof.
+  intros until res. intros Hexit Hbody. simpl split.
+  unfold transl_blocks. fold transl_blocks. unfold transl_block.
+  simpl. remember (transl_basic_code _ _ _) as tbc. remember (transl_exit _ _) as tbi.
+  remember (transl_blocks _ _ _) as tlbs.
+  destruct tbc; destruct tbi; destruct tlbs.
+  - unfold cons_bblocks; try destruct p; try simpl; rewrite app_nil_r. 
+  destruct l; destruct o; destruct b; simpl. auto.
+  
+  auto.
+  all: unfold cons_bblocks; try destruct p; try simpl; auto.
+  - simpl. rewrite Hexit in Heqtbi. simpl in Heqtbi. monadInv Heqtbi. simpl.
+    unfold cons_bblocks. simpl. destruct l.
+    + exploit transl_basic_code_nonil; eauto. intro. destruct H.
+    + simpl. rewrite app_nil_r. simpl. apply cons_ok_eq3. all: try eapply bblock_equality. all: simpl; auto.
+Qed.
+
+Lemma transl_code_at_pc_split_builtin:
+  forall rs f f0 bb c ep tf tc ef args res,
+  MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) ->
+  transl_code_at_pc ge (rs PC) f f0 (bb :: c) ep tf tc ->
+  transl_code_at_pc ge (rs PC) f f0 (split (bb :: c)) ep tf tc.
+Proof.
+  intros until res. intros Hbody Hexit AT. inv AT.
+  econstructor; eauto. erewrite transl_blocks_split_builtin; eauto.
+Qed.
+
+
+Theorem match_states_split_builtin:
+  forall sf f sp bb c rs m ef args res S1,
+  MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) ->
+  match_states (Machblock.State sf f sp (bb :: c) rs m) S1 ->
+  match_states (Machblock.State sf f sp (split (bb::c)) rs m) S1.
+Proof.
+  intros until S1. intros Hbody Hexit MS.
+  inv MS.
+  econstructor; eauto.
+  eapply transl_code_at_pc_split_builtin; eauto.
+Qed. *)
+
+Theorem step_simulation_builtin:
+  forall ef args res bb sf f sp c ms m t S2,
+  MB.body bb = nil -> MB.exit bb = Some (MBbuiltin ef args res) ->
+  exit_step return_address_offset ge (MB.exit bb) (Machblock.State sf f sp (bb :: c) ms m) t S2 ->
+  forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' ->
+  exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'.
+Proof.
+  intros until S2. intros Hbody Hexit ESTEP S1' MS.
+  inv MS. inv AT. monadInv H2. monadInv EQ.
+  rewrite Hbody in EQ. monadInv EQ.
+  rewrite Hexit in EQ0. monadInv EQ0.
+  rewrite Hexit in ESTEP. inv ESTEP. inv H4.
+
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H1); intro NOOV.
+  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
+  exploit external_call_mem_extends; eauto.
+  intros [vres' [m2' [A [B [C D]]]]].
+  econstructor; split. apply plus_one.
+  simpl in H3.
+  eapply exec_step_internal. eauto. eauto.
+    eapply find_bblock_tail; eauto.
+    simpl. econstructor. eexists. simpl. split; eauto.
+    econstructor.
+    erewrite <- sp_val by eauto.
+    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+    eauto.
+  econstructor; eauto.
+    instantiate (2 := tf); instantiate (1 := x0).
+    unfold incrPC. rewrite Pregmap.gss.
+    rewrite set_res_other. rewrite undef_regs_other_2.
+    rewrite <- H. simpl. econstructor; eauto.
+    eapply code_tail_next_int; eauto.
+    rewrite preg_notin_charact. intros. auto with asmgen.
+    auto with asmgen.
+    apply agree_nextblock. eapply agree_set_res; auto.
+    eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
+    congruence.
+Qed.
+
 (* Measure to prove finite stuttering, see the other backends *)
 Definition measure (s: MB.state) : nat :=
   match s with
@@ -631,26 +1603,23 @@ Theorem step_simulation:
   forall S1' (MS: match_states S1 S1'),
   (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2')
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
-Proof.
-  induction 1; intros.
+Proof. Admitted.
+(*  induction 1; intros.
 
 - (* bblock *)
   left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0.
-  all: admit.
-all: admit.
-Admitted.
-  (*all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; 
+  all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; 
             try (rewrite MBE; try discriminate); eauto).
   + (* MBbuiltin *)
     destruct (MB.body bb) eqn:MBB.
     * inv H. eapply step_simulation_builtin; eauto. rewrite MBE. eauto.
-    * eapply match_states_split_builtin in MS; eauto.
-        2: rewrite MBB; discriminate.
-      simpl split in MS.
+    * (* eapply match_states_split_builtin in MS; eauto.
+        2: rewrite MBB; discriminate. *)
+      (* simpl split in MS. *)
       rewrite <- MBB in H.
-      remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1.
-      assert (MB.body bb = MB.body bb1). { subst. simpl. auto. }
-      rewrite H1 in H. subst.
+(*       remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1. *)
+(*       assert (MB.body bb = MB.body bb1). { subst. simpl. auto. } *)
+(*       rewrite H1 in H. subst. *)
       exploit step_simulation_bblock. eapply H.
         discriminate.
         simpl. constructor.