Revised Stacking and Asmgen passes and Mach semantics:

- no more prediction of return addresses (Asmgenretaddr is gone)
- instead, punch a hole for the retaddr in Mach stack frame and
  fill this hole with the return address in the Asmgen proof.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 280 insertions, 653 deletions

diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index d618d44..e43552e 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -25,12 +25,10 @@ Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import Mach.
-Require Import Machsem.
-Require Import Machtyping.
 Require Import Conventions.
 Require Import Asm.
 Require Import Asmgen.
-Require Import Asmgenretaddr.
+Require Import Asmgenproof0.
 Require Import Asmgenproof1.
 
 Section PRESERVATION.
@@ -77,65 +75,6 @@ Qed.
 
 (** * Properties of control flow *)
 
-Lemma find_instr_in:
-  forall c pos i,
-  find_instr pos c = Some i -> In i c.
-Proof.
-  induction c; simpl. intros; discriminate.
-  intros until i. case (zeq pos 0); intros.
-  left; congruence. right; eauto.
-Qed.
-
-Lemma find_instr_tail:
-  forall c1 i c2 pos,
-  code_tail pos c1 (i :: c2) ->
-  find_instr pos c1 = Some i.
-Proof.
-  induction c1; simpl; intros.
-  inv H.
-  destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction.
-  inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega.
-  eauto.
-Qed.
-
-Remark code_tail_bounds:
-  forall fn ofs i c,
-  code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
-Proof.
-  assert (forall ofs fn c, code_tail ofs fn c ->
-          forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
-  induction 1; intros; simpl. 
-  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
-  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
-  eauto.
-Qed.
-
-Lemma code_tail_next:
-  forall fn ofs i c,
-  code_tail ofs fn (i :: c) ->
-  code_tail (ofs + 1) fn c.
-Proof.
-  assert (forall ofs fn c, code_tail ofs fn c ->
-          forall i c', c = i :: c' -> code_tail (ofs + 1) fn c').
-  induction 1; intros.
-  subst c. constructor. constructor.
-  constructor. eauto.
-  eauto.
-Qed.
-
-Lemma code_tail_next_int:
-  forall fn ofs i c,
-  list_length_z fn <= Int.max_unsigned ->
-  code_tail (Int.unsigned ofs) fn (i :: c) ->
-  code_tail (Int.unsigned (Int.add ofs Int.one)) fn c.
-Proof.
-  intros. rewrite Int.add_unsigned.
-  change (Int.unsigned Int.one) with 1.
-  rewrite Int.unsigned_repr. apply code_tail_next with i; auto.
-  generalize (code_tail_bounds _ _ _ _ H0). omega. 
-Qed.
-
 Lemma transf_function_no_overflow:
   forall f tf,
   transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned.
@@ -144,73 +83,9 @@ Proof.
   rewrite list_length_z_cons. omega. 
 Qed.
 
-(** [transl_code_at_pc pc fn c] holds if the code pointer [pc] points
-  within the IA32 code generated by translating Mach function [fn],
-  and [c] is the tail of the generated code at the position corresponding
-  to the code pointer [pc]. *)
-
-Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> bool ->
-                                             Asm.code -> Asm.code -> Prop :=
-  transl_code_at_pc_intro:
-    forall b ofs f c ep tf tc,
-    Genv.find_funct_ptr ge b = Some (Internal f) ->
-    transf_function f = OK tf ->
-    transl_code f c ep = OK tc ->
-    code_tail (Int.unsigned ofs) tf tc ->
-    transl_code_at_pc (Vptr b ofs) b f c ep tf tc.
-
-(** The following lemmas show that straight-line executions
-  (predicate [exec_straight]) correspond to correct PPC executions
-  (predicate [exec_steps]) under adequate [transl_code_at_pc] hypotheses. *)
-
-Lemma exec_straight_steps_1:
-  forall fn c rs m c' rs' m',
-  exec_straight tge fn c rs m c' rs' m' ->
-  list_length_z fn <= Int.max_unsigned ->
-  forall b ofs,
-  rs#PC = Vptr b ofs ->
-  Genv.find_funct_ptr tge b = Some (Internal fn) ->
-  code_tail (Int.unsigned ofs) fn c ->
-  plus step tge (State rs m) E0 (State rs' m').
-Proof.
-  induction 1; intros.
-  apply plus_one.
-  econstructor; eauto. 
-  eapply find_instr_tail. eauto.
-  eapply plus_left'.
-  econstructor; eauto. 
-  eapply find_instr_tail. eauto.
-  apply IHexec_straight with b (Int.add ofs Int.one). 
-  auto. rewrite H0. rewrite H3. reflexivity.
-  auto. 
-  apply code_tail_next_int with i; auto.
-  traceEq.
-Qed.
-    
-Lemma exec_straight_steps_2:
-  forall fn c rs m c' rs' m',
-  exec_straight tge fn c rs m c' rs' m' ->
-  list_length_z fn <= Int.max_unsigned ->
-  forall b ofs,
-  rs#PC = Vptr b ofs ->
-  Genv.find_funct_ptr tge b = Some (Internal fn) ->
-  code_tail (Int.unsigned ofs) fn c ->
-  exists ofs',
-     rs'#PC = Vptr b ofs'
-  /\ code_tail (Int.unsigned ofs') fn c'.
-Proof.
-  induction 1; intros.
-  exists (Int.add ofs Int.one). split.
-  rewrite H0. rewrite H2. auto.
-  apply code_tail_next_int with i1; auto.
-  apply IHexec_straight with (Int.add ofs Int.one).
-  auto. rewrite H0. rewrite H3. reflexivity. auto. 
-  apply code_tail_next_int with i; auto.
-Qed.
-
 Lemma exec_straight_exec:
-  forall fb f c ep tf tc c' rs m rs' m',
-  transl_code_at_pc (rs PC) fb f c ep tf tc ->
+  forall f c ep tf tc c' rs m rs' m',
+  transl_code_at_pc ge (rs PC) f c ep tf tc ->
   exec_straight tge tf tc rs m c' rs' m' ->
   plus step tge (State rs m) E0 (State rs' m').
 Proof.
@@ -221,11 +96,11 @@ Proof.
 Qed.
 
 Lemma exec_straight_at:
-  forall fb f c ep tf tc c' ep' tc' rs m rs' m',
-  transl_code_at_pc (rs PC) fb f c ep tf tc ->
+  forall f c ep tf tc c' ep' tc' rs m rs' m',
+  transl_code_at_pc ge (rs PC) f c ep tf tc ->
   transl_code f c' ep' = OK tc' ->
   exec_straight tge tf tc rs m tc' rs' m' ->
-  transl_code_at_pc (rs' PC) fb f c' ep' tf tc'.
+  transl_code_at_pc ge (rs' PC) f c' ep' tf tc'.
 Proof.
   intros. inv H. 
   exploit exec_straight_steps_2; eauto. 
@@ -235,36 +110,6 @@ Proof.
   rewrite PC'. constructor; auto.
 Qed.
 
-(** Correctness of the return addresses predicted by
-    [Asmgen.return_address_offset]. *)
-
-Remark code_tail_no_bigger:
-  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
-Proof.
-  induction 1; simpl; omega.
-Qed.
-
-Remark code_tail_unique:
-  forall fn c pos pos',
-  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
-Proof.
-  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  f_equal. eauto.
-Qed.
-
-Lemma return_address_offset_correct:
-  forall b ofs fb f c tf tc ofs',
-  transl_code_at_pc (Vptr b ofs) fb f c false tf tc ->
-  return_address_offset f c ofs' ->
-  ofs' = ofs.
-Proof.
-  intros. inv H0. inv H. 
-  exploit code_tail_unique. eexact H12. eapply H1; eauto. intro.
-  subst ofs0. apply Int.repr_unsigned.
-Qed.
-
 (** The [find_label] function returns the code tail starting at the
   given label.  A connection with [code_tail] is then established. *)
 
@@ -446,7 +291,6 @@ Proof.
   destruct c0; auto.
 Qed.
 
-
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c ->
@@ -534,7 +378,7 @@ Qed.
 Lemma transl_find_label:
   forall f tf,
   transf_function f = OK tf ->
-  match Mach.find_label lbl f.(fn_code) with
+  match Mach.find_label lbl f.(Mach.fn_code) with
   | None => find_label lbl tf = None
   | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc
   end.
@@ -553,10 +397,10 @@ Lemma find_label_goto_label:
   Genv.find_funct_ptr ge b = Some (Internal f) ->
   transf_function f = OK tf ->
   rs PC = Vptr b ofs ->
-  Mach.find_label lbl f.(fn_code) = Some c' ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
   exists tc', exists rs',
     goto_label tf lbl rs m = Next rs' m  
-  /\ transl_code_at_pc (rs' PC) b f c' false tf tc'
+  /\ transl_code_at_pc ge (rs' PC) 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. 
@@ -590,61 +434,51 @@ Qed.
 - Mach register values and PPC register values agree.
 *)
 
-Inductive match_stack: list Machsem.stackframe -> Prop :=
-  | match_stack_nil:
-      match_stack nil
-  | match_stack_cons: forall fb sp ra c s f tf tc,
-      Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      transl_code_at_pc ra fb f c false tf tc ->
-      sp <> Vundef -> ra <> Vundef ->
-      match_stack s ->
-      match_stack (Stackframe fb sp ra c :: s).
-
-Inductive match_states: Machsem.state -> Asm.state -> Prop :=
+Inductive match_states: Mach.state -> Asm.state -> Prop :=
   | match_states_intro:
-      forall s fb sp c ep ms m m' rs f tf tc
-        (STACKS: match_stack s)
-        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
+      forall s f sp c ep ms m m' rs tf tc ra
+        (STACKS: match_stack ge s m m' ra sp)
         (MEXT: Mem.extends m m')
-        (AT: transl_code_at_pc (rs PC) fb f c ep tf tc)
-        (AG: agree ms sp rs)
+        (AT: transl_code_at_pc ge (rs PC) f c ep tf tc)
+        (AG: agree ms (Vptr sp Int.zero) rs)
+        (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra)
         (DXP: ep = true -> rs#EDX = parent_sp s),
-      match_states (Machsem.State s fb sp c ms m)
+      match_states (Mach.State s f (Vptr sp Int.zero) c ms m)
                    (Asm.State rs m')
   | match_states_call:
-      forall s fb ms m m' rs
-        (STACKS: match_stack s)
+      forall s fd ms m m' rs fb
+        (STACKS: match_stack ge s m m' (rs RA) (Mem.nextblock m))
         (MEXT: Mem.extends m m')
         (AG: agree ms (parent_sp s) rs)
         (ATPC: rs PC = Vptr fb Int.zero)
-        (ATLR: rs RA = parent_ra s),
-      match_states (Machsem.Callstate s fb ms m)
+        (FUNCT: Genv.find_funct_ptr ge fb = Some fd)
+        (WTRA: Val.has_type (rs RA) Tint),
+      match_states (Mach.Callstate s fd ms m)
                    (Asm.State rs m')
   | match_states_return:
       forall s ms m m' rs
-        (STACKS: match_stack s)
+        (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m))
         (MEXT: Mem.extends m m')
-        (AG: agree ms (parent_sp s) rs)
-        (ATPC: rs PC = parent_ra s),
-      match_states (Machsem.Returnstate s ms m)
+        (AG: agree ms (parent_sp s) rs),
+      match_states (Mach.Returnstate s ms m)
                    (Asm.State rs m').
 
 Lemma exec_straight_steps:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,
-  match_stack s ->
+  forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra,
+  match_stack ge s m2 m2' ra sp ->
   Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc ->
-  (forall k c, transl_instr f i ep k = OK c ->
+  retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra ->
+  transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
    exists rs2,
        exec_straight tge tf c rs1 m1' k rs2 m2'
-    /\ agree ms2 sp rs2
+    /\ agree ms2 (Vptr sp Int.zero) rs2
     /\ (edx_preserved ep i = true -> rs2#EDX = parent_sp s)) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machsem.State s fb sp c ms2 m2) st'.
+  match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'.
 Proof.
-  intros. inversion H2. subst. monadInv H7. 
+  intros. inversion H2; subst. monadInv H7. 
   exploit H3; eauto. intros [rs2 [A [B C]]]. 
   exists (State rs2 m2'); split.
   eapply exec_straight_exec; eauto. 
@@ -652,23 +486,23 @@ Proof.
 Qed.
 
 Lemma exec_straight_steps_goto:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
-  match_stack s ->
+  forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra,
+  match_stack ge s m2 m2' ra sp ->
   Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl f.(fn_code) = Some c' ->
-  transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc ->
+  retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
+  transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc ->
   edx_preserved ep i = false ->
-  (forall k c, transl_instr f i ep k = OK c ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
    exists jmp, exists k', exists rs2,
        exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
-    /\ agree ms2 sp rs2
+    /\ agree ms2 (Vptr sp Int.zero) rs2
     /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Machsem.State s fb sp c' ms2 m2) st'.
+  match_states (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'.
 Proof.
-  intros. inversion H3. subst. monadInv H9.
+  intros. inversion H3; subst. monadInv H9.
   exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
   generalize (functions_transl _ _ _ H7 H8); intro FN.
   generalize (transf_function_no_overflow _ _ H8); intro NOOV.
@@ -684,164 +518,99 @@ Proof.
   rewrite C. eexact GOTO.
   traceEq.
   econstructor; eauto.
-  apply agree_exten with rs2; auto with ppcgen.
+  apply agree_exten with rs2; auto with asmgen.
   congruence.
 Qed.
 
-Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
-Proof. induction 1; simpl. congruence. auto. Qed.
-
-Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
-Proof. induction 1; simpl. unfold Vzero. congruence. auto. Qed.
-
-Lemma lessdef_parent_sp:
-  forall s v,
-  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
-Proof.
-  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
-Qed.
-
-Lemma lessdef_parent_ra:
-  forall s v,
-  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
-Proof.
-  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
-Qed.
-
 (** We need to show that, in the simulation diagram, we cannot
   take infinitely many Mach transitions that correspond to zero
   transitions on the PPC side.  Actually, all Mach transitions
   correspond to at least one Asm transition, except the
-  transition from [Machsem.Returnstate] to [Machsem.State].
+  transition from [Mach.Returnstate] to [Mach.State].
   So, the following integer measure will suffice to rule out
   the unwanted behaviour. *)
 
-Definition measure (s: Machsem.state) : nat :=
+Definition measure (s: Mach.state) : nat :=
   match s with
-  | Machsem.State _ _ _ _ _ _ => 0%nat
-  | Machsem.Callstate _ _ _ _ => 0%nat
-  | Machsem.Returnstate _ _ _ => 1%nat
+  | Mach.State _ _ _ _ _ _ => 0%nat
+  | Mach.Callstate _ _ _ _ => 0%nat
+  | Mach.Returnstate _ _ _ => 1%nat
   end.
 
-(** We show the simulation diagram by case analysis on the Mach transition
-  on the left.  Since the proof is large, we break it into one lemma
-  per transition. *)
-
-Definition exec_instr_prop (s1: Machsem.state) (t: trace) (s2: Machsem.state) : Prop :=
-  forall s1' (MS: match_states s1 s1'),
-  (exists s2', plus step tge s1' t s2' /\ match_states s2 s2')
-  \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
-
+(** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
 
-Lemma exec_Mlabel_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
-         (m : mem),
-  exec_instr_prop (Machsem.State s fb sp (Mlabel lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c ms m).
+Theorem step_simulation:
+  forall S1 t S2, Mach.step ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
-  intros; red; intros; inv MS.
+  induction 1; intros; inv MS.
+
+- (* Mlabel *)
   left; eapply exec_straight_steps; eauto; intros. 
-  monadInv H. econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
+  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. 
   split. apply agree_nextinstr; auto. simpl; congruence.
-Qed.
 
-Lemma exec_Mgetstack_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (ofs : int)
-         (ty : typ) (dst : mreg) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (v : val),
-  load_stack m sp ty ofs = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mgetstack ofs ty dst :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set dst v ms) m).
-Proof.
-  intros; red; intros; inv MS.
+- (* Mgetstack *)
   unfold load_stack in H.
   exploit Mem.loadv_extends; eauto. intros [v' [A B]].
   rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto. intros. simpl in H0. 
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
   exploit loadind_correct; eauto. intros [rs' [P [Q R]]].
   exists rs'; split. eauto.
   split. eapply agree_set_mreg; eauto. congruence.
   simpl; congruence.
-Qed.
 
-Lemma exec_Msetstack_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (src : mreg)
-         (ofs : int) (ty : typ) (c : list Mach.instruction)
-         (ms : mreg -> val) (m m' : mem),
-  store_stack m sp ty ofs (ms src) = Some m' ->
-  exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_setstack ms) m').
-Proof.
-  intros; red; intros; inv MS.
+- (* Msetstack *)
   unfold store_stack in H.
-  assert (Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m2' [A B]]. 
-  rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto. intros. simpl in H1.
+  left; eapply exec_straight_steps; eauto.
+  eapply match_stack_storev; eauto. 
+  eapply retaddr_stored_at_storev; eauto. 
+  rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
   exploit storeind_correct; eauto. intros [rs' [P Q]].
   exists rs'; split. eauto.
   split. unfold undef_setstack. eapply agree_undef_move; eauto.
-  simpl; intros. rewrite Q; auto with ppcgen.
-Qed.
+  simpl; intros. rewrite Q; auto with asmgen.
 
-Lemma exec_Mgetparam_prop:
-  forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : val)
-         (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (v : val),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (parent_sp s) ty ofs = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mgetparam *)
   unfold load_stack in *. 
-  exploit Mem.loadv_extends. eauto. eexact H0. auto. 
+  exploit Mem.loadv_extends. eauto. eexact H. auto. 
   intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  assert (parent' = parent_sp s). inv B. auto. rewrite <- H3 in H1. simpl in H1. congruence.
-  subst parent'.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. 
+  exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
+  exploit Mem.loadv_extends. eauto. eexact H0. auto. 
   intros [v' [C D]].
 Opaque loadind.
   left; eapply exec_straight_steps; eauto; intros. 
   assert (DIFF: negb (mreg_eq dst IT1) = true -> IR EDX <> preg_of dst).
-    intros. change (IR EDX) with (preg_of IT1). red; intros.
-    exploit preg_of_injective; eauto. intros. subst dst. 
-    unfold proj_sumbool in H3. rewrite dec_eq_true in H3. simpl in H3. congruence.
-  destruct ep; simpl in H2.
+    intros. change (IR EDX) with (preg_of IT1). red; intros. 
+    unfold proj_sumbool in H1. destruct (mreg_eq dst IT1); try discriminate.
+    elim n. eapply preg_of_injective; eauto.
+  destruct ep; simpl in TR.
 (* EDX contains parent *)
-  exploit loadind_correct. eexact H2.
-  instantiate (2 := rs). rewrite DXP; eauto.  
+  exploit loadind_correct. eexact TR.
+  instantiate (2 := rs0). rewrite DXP; eauto.  
   intros [rs1 [P [Q R]]].
   exists rs1; split. eauto. 
   split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto.
   simpl; intros. rewrite R; auto.
 (* EDX does not contain parent *)
-  monadInv H2.
+  monadInv TR.
   exploit loadind_correct. eexact EQ0. eauto. intros [rs1 [P [Q R]]]. simpl in Q.
   exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto.
   intros [rs2 [S [T U]]]. 
   exists rs2; split. eapply exec_straight_trans; eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto.
-  simpl; intros. rewrite U; auto. 
-Qed.
+  simpl; intros. rewrite U; auto.
 
-Lemma exec_Mop_prop:
-  forall (s : list stackframe) (fb : block) (sp : val) (op : operation)
-         (args : list mreg) (res : mreg) (c : list Mach.instruction)
-         (ms : mreg -> val) (m : mem) (v : val),
-  eval_operation ge sp op ms ## args m = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mop op args res :: c) ms m) E0
-                  (Machsem.State s fb sp c (Regmap.set res v (undef_op op ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (eval_operation tge sp op ms##args m = Some v). 
+- (* Mop *)
+  assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). 
     rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
   exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
   intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. 
-  left; eapply exec_straight_steps; eauto; intros. simpl in H1. 
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
   exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. 
   assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto).
   exists rs2; split. eauto.
@@ -850,209 +619,135 @@ Proof.
   destruct op; try (eapply agree_set_undef_mreg; eauto).
   eapply agree_set_undef_move_mreg; eauto. 
   simpl; congruence.
-Qed.
 
-Lemma exec_Mload_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (chunk : memory_chunk) (addr : addressing) (args : list mreg)
-         (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val)
-         (m : mem) (a v : val),
-  eval_addressing ge sp addr ms ## args = Some a ->
-  Mem.loadv chunk m a = Some v ->
-  exec_instr_prop (Machsem.State s fb sp (Mload chunk addr args dst :: c) ms m)
-               E0 (Machsem.State s fb sp c (Regmap.set dst v (undef_temps ms)) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (eval_addressing tge sp addr ms##args = Some a). 
+- (* Mload *)
+  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##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]].
-  left; eapply exec_straight_steps; eauto; intros. simpl in H2. 
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
   exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. 
   exists rs2; split. eauto.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   simpl; congruence.
-Qed.
 
-Lemma exec_Mstore_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (chunk : memory_chunk) (addr : addressing) (args : list mreg)
-         (src : mreg) (c : list Mach.instruction) (ms : mreg -> val)
-         (m m' : mem) (a : val),
-  eval_addressing ge sp addr ms ## args = Some a ->
-  Mem.storev chunk m a (ms src) = Some m' ->
-  exec_instr_prop (Machsem.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_temps ms) m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (eval_addressing tge sp addr ms##args = Some a). 
+- (* Mstore *)
+  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##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) (rs (preg_of src))). eapply preg_val; eauto.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m2' [C D]].
-  left; eapply exec_straight_steps; eauto; intros. simpl in H3. 
+  left; eapply exec_straight_steps; eauto.
+  eapply match_stack_storev; eauto.
+  eapply retaddr_stored_at_storev; eauto.
+  intros. simpl in TR. 
   exploit transl_store_correct; eauto. intros [rs2 [P Q]]. 
   exists rs2; split. eauto.
   split. eapply agree_exten_temps; eauto. 
   simpl; congruence.
-Qed.
 
-Lemma exec_Mcall_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (sig : signature) (ros : mreg + ident) (c : Mach.code)
-         (ms : Mach.regset) (m : mem) (f : function) (f' : block)
-         (ra : int),
-  find_function_ptr ge ros ms = Some f' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  return_address_offset f c ra ->
-  exec_instr_prop (Machsem.State s fb sp (Mcall sig ros :: c) ms m) E0
-                  (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' ms m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mcall *)
   inv AT. 
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
-  destruct ros as [rf|fid]; simpl in H; monadInv H5.
-  (* Indirect call *)
-  assert (DEST: ms rf = Vptr f' Int.zero).
-    destruct (ms rf); try discriminate.
-    generalize (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero); congruence.
-  clear H.
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
+  destruct ros as [rf|fid]; simpl in H; monadInv H3.
++ (* Indirect call *)
+  exploit Genv.find_funct_inv; eauto. intros [bf EQ2].
+  rewrite EQ2 in H; rewrite  Genv.find_funct_find_funct_ptr in H. 
+  assert (rs0 x0 = Vptr bf Int.zero).
+    exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto.
+  generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x).
     econstructor; eauto. 
-  exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. 
-  constructor; auto. 
-  econstructor; eauto. eapply agree_sp_def; eauto. congruence.
-  simpl. eapply agree_exten; eauto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-  exploit ireg_val; eauto. rewrite DEST. intros LD. inv LD. auto.
-  rewrite <- H2. auto. 
-  (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
+  econstructor; eauto. 
+  econstructor; eauto.
+  rewrite <- H0. eexact TCA. 
+  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  simpl. eapply agree_exten; eauto. intros. Simplifs. 
+  rewrite <- H0. exact I.
++ (* Direct call *)
+  destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate.
+  generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x).
     econstructor; eauto. 
-  exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto.
-  constructor; auto. 
-  econstructor; eauto. eapply agree_sp_def; eauto. congruence.
-  simpl. eapply agree_exten; eauto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-  rewrite <- H2. auto.
-Qed.
-
-Lemma agree_change_sp:
-  forall ms sp rs sp',
-  agree ms sp rs -> sp' <> Vundef ->
-  agree ms sp' (rs#ESP <- sp').
-Proof.
-  intros. inv H. split. apply Pregmap.gss. auto. 
-  intros. rewrite Pregmap.gso; auto with ppcgen.
-Qed.
+  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. eauto.
+  econstructor; eauto. 
+  econstructor; eauto.
+  rewrite <- H0. eexact TCA.
+  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  simpl. eapply agree_exten; eauto. intros. Simplifs.
+  auto.
+  rewrite <- H0. exact I.
 
-Lemma exec_Mtailcall_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m',
-  find_function_ptr ge ros ms = Some f' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop
-          (Machsem.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
-          (Callstate s f' ms m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mtailcall *)
   inv AT. 
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. 
+  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. 
   exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]].
-  exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
-  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. 
-  destruct ros as [rf|fid]; simpl in H; monadInv H7.
-  (* Indirect call *)
-  assert (DEST: ms rf = Vptr f' Int.zero).
-    destruct (ms rf); try discriminate.
-    generalize (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero); congruence.
-  clear H.
-  generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1.
+  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 ESP) (Vint (fn_retaddr_ofs f))) = Some ra).
+Opaque Int.repr.
+    erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l.
+    eapply rsa_contains; eauto.
+  exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]].
+  assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')).
+    apply match_stack_change_bound with stk.
+    eapply match_stack_free_left; eauto. 
+    eapply match_stack_free_left; eauto. 
+    eapply match_stack_free_right; eauto.
+    omega.
+    apply Z.lt_le_incl. change (Mem.valid_block m'' stk).
+    eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. 
+    eapply retaddr_stored_at_valid; eauto.
+  destruct ros as [rf|fid]; simpl in H; monadInv H6.
++ (* Indirect call *)
+  exploit Genv.find_funct_inv; eauto. intros [bf EQ2].
+  rewrite EQ2 in H; rewrite  Genv.find_funct_find_funct_ptr in H. 
+  assert (rs0 x0 = Vptr bf Int.zero).
+    exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto.
+  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
   apply star_one. eapply exec_step_internal. 
-  transitivity (Val.add rs#PC Vone). auto. rewrite <- H4. simpl. eauto.
+  transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. traceEq.
-  constructor; auto.
+  econstructor; eauto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-  rewrite Pregmap.gss. rewrite nextinstr_inv; auto with ppcgen.
-  repeat rewrite Pregmap.gso; auto with ppcgen. 
-  exploit ireg_val; eauto. rewrite DEST. intros LD. inv LD. auto.
-  generalize (preg_of_not_ESP rf). rewrite (ireg_of_eq _ _ EQ1). congruence.
-  (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1.
+  Simplifs. rewrite Pregmap.gso; auto. 
+  generalize (preg_of_not_SP rf). rewrite (ireg_of_eq _ _ EQ1). congruence.
+  change (Val.has_type ra Tint). eapply retaddr_stored_at_type; eauto.
++ (* Direct call *)
+  destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate.
+  generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
   apply star_one. eapply exec_step_internal. 
-  transitivity (Val.add rs#PC Vone). auto. rewrite <- H4. simpl. eauto.
+  transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. traceEq.
-  constructor; auto.
+  econstructor; eauto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-  rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto.
-Qed.
+  rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto.
+  change (Val.has_type ra Tint). eapply retaddr_stored_at_type; eauto.
 
-Lemma exec_Mgoto_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
-         (m : mem) (c' : Mach.code),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machsem.State s fb sp (Mgoto lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c' ms m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H4. 
-  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
-  left; exists (State rs' m'); split.
-  apply plus_one. econstructor; eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail; eauto.
-  simpl; eauto.
-  econstructor; eauto.
-  eapply agree_exten; eauto with ppcgen.
-  congruence.
-Qed.
-
-Lemma exec_Mbuiltin_prop:
-  forall (s : list stackframe) (f : block) (sp : val)
-         (ms : Mach.regset) (m : mem) (ef : external_function)
-         (args : list mreg) (res : mreg) (b : list Mach.instruction)
-         (t : trace) (v : val) (m' : mem),
-  external_call ef ge ms ## args m t v m' ->
-  exec_instr_prop (Machsem.State s f sp (Mbuiltin ef args res :: b) ms m) t
-                  (Machsem.State s f sp b (Regmap.set res v (undef_temps ms)) m').
-Proof.
-  intros; red; intros; inv MS.
+- (* Mbuiltin *)
   inv AT. monadInv H3. 
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H2); intro NOOV.
@@ -1064,28 +759,21 @@ Proof.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
+  eapply match_stack_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   instantiate (2 := tf); instantiate (1 := x).
   unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss.
-  simpl undef_regs. repeat rewrite Pregmap.gso; auto with ppcgen. 
+  simpl undef_regs. repeat rewrite Pregmap.gso; auto with asmgen. 
   rewrite <- H0. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
   apply agree_nextinstr_nf. eapply agree_set_undef_mreg; eauto. 
   rewrite Pregmap.gss. auto. 
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+  intros. Simplifs. 
+  eapply retaddr_stored_at_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   congruence.
-Qed.
 
-Lemma exec_Mannot_prop:
-  forall (s : list stackframe) (f : block) (sp : val)
-         (ms : Mach.regset) (m : mem) (ef : external_function)
-         (args : list Mach.annot_param) (b : list Mach.instruction)
-         (vargs: list val) (t : trace) (v : val) (m' : mem),
-  Machsem.annot_arguments ms m sp args vargs ->
-  external_call ef ge vargs m t v m' ->
-  exec_instr_prop (Machsem.State s f sp (Mannot ef args :: b) ms m) t
-                  (Machsem.State s f sp b ms m').
-Proof.
-  intros; red; intros; inv MS.
+- (* Mannot *)
   inv AT. monadInv H4. 
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H3); intro NOOV.
@@ -1098,32 +786,35 @@ Proof.
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_states_intro with (ep := false); eauto with coqlib.
+  eapply match_stack_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   unfold nextinstr. rewrite Pregmap.gss. 
   rewrite <- H1; simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto. 
   apply agree_nextinstr. auto.
+  eapply retaddr_stored_at_extcall; eauto. 
+  intros; eapply external_call_max_perm; eauto. 
   congruence.
-Qed.
 
-Lemma exec_Mcond_true_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (cond : condition) (args : list mreg) (lbl : Mach.label)
-         (c : list Mach.instruction) (ms : mreg -> val) (m : mem)
-         (c' : Mach.code),
-  eval_condition cond ms ## args m = Some true ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c' (undef_temps ms) m).
-Proof.
-  intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0.
+- (* Mgoto *)
+  inv AT. monadInv H3. 
+  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
+  left; exists (State rs' m'); split.
+  apply plus_one. econstructor; eauto.
+  eapply functions_transl; eauto.
+  eapply find_instr_tail; eauto.
+  simpl; eauto.
+  econstructor; eauto.
+  eapply agree_exten; eauto with asmgen.
+  congruence.
+
+- (* Mcond true *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
   left; eapply exec_straight_steps_goto; eauto.
-  intros. simpl in H2.
-  destruct (transl_cond_correct tge tf cond args _ _ rs m' H2)
+  intros. simpl in TR.
+  destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]]. 
-  rewrite EC in B (* 8.4 *)
-   || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *).
+  rewrite EC in B.
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   exists (Pjcc c1 lbl); exists k; exists rs'.
@@ -1131,47 +822,37 @@ Proof.
   split. eapply agree_exten_temps; eauto. 
   simpl. rewrite B. auto.
 (* jcc; jcc *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
   destruct b1.   
   (* first jcc jumps *)
   exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'.
   split. eexact A.
   split. eapply agree_exten_temps; eauto. 
-  simpl. rewrite Heqo. auto.
+  simpl. rewrite TC1. auto.
   (* second jcc jumps *)
   exists (Pjcc c2 lbl); exists k; exists (nextinstr rs').
   split. eapply exec_straight_trans. eexact A. 
-  eapply exec_straight_one. simpl. rewrite Heqo. auto. auto.
-  split. eapply agree_exten_temps; eauto. 
-  intros. rewrite nextinstr_inv; auto with ppcgen.
-  simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0.
+  eapply exec_straight_one. simpl. rewrite TC1. auto. auto.
+  split. eapply agree_exten_temps; eauto.
+  intros; Simplifs.
+  simpl. rewrite eval_testcond_nextinstr. rewrite TC2.
   destruct b2; auto || discriminate.
 (* jcc2 *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
-  destruct (andb_prop _ _ H4). subst. 
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
+  destruct (andb_prop _ _ H2). subst. 
   exists (Pjcc2 c1 c2 lbl); exists k; exists rs'.
   split. eexact A.
   split. eapply agree_exten_temps; eauto. 
-  simpl. rewrite Heqo; rewrite Heqo0; auto. 
-Qed.
+  simpl. rewrite TC1; rewrite TC2; auto.
 
-Lemma exec_Mcond_false_prop:
-  forall (s : list stackframe) (fb : block) (sp : val)
-         (cond : condition) (args : list mreg) (lbl : Mach.label)
-         (c : list Mach.instruction) (ms : mreg -> val) (m : mem),
-  eval_condition cond ms ## args m = Some false ->
-  exec_instr_prop (Machsem.State s fb sp (Mcond cond args lbl :: c) ms m) E0
-                  (Machsem.State s fb sp c (undef_temps ms) m).
-Proof.
-  intros; red; intros; inv MS.
+- (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_steps; eauto. intros. simpl in H0. 
-  destruct (transl_cond_correct tge tf cond args _ _ rs m' H0)
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR. 
+  destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR)
   as [rs' [A [B C]]]. 
-  rewrite EC in B (* 8.4 *)
-   || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *).
+  rewrite EC in B.
   destruct (testcond_for_condition cond); simpl in *.
 (* simple jcc *)
   econstructor; split.
@@ -1180,149 +861,119 @@ Proof.
   split. apply agree_nextinstr. eapply agree_exten_temps; eauto.
   simpl; congruence.
 (* jcc ; jcc *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
-  destruct (orb_false_elim _ _ H2); subst.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
+  destruct (orb_false_elim _ _ H1); subst.
   econstructor; split.
   eapply exec_straight_trans. eexact A. 
-  eapply exec_straight_two. simpl. rewrite Heqo. eauto. auto. 
-  simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. eauto. auto. auto.
+  eapply exec_straight_two. simpl. rewrite TC1. eauto. auto. 
+  simpl. rewrite eval_testcond_nextinstr. rewrite TC2. eauto. auto. auto.
   split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten_temps; eauto.
   simpl; congruence.
 (* jcc2 *)
-  destruct (eval_testcond c1 rs') as [b1|] eqn:?;
-  destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B.
+  destruct (eval_testcond c1 rs') as [b1|] eqn:TC1;
+  destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B.
   exists (nextinstr rs'); split.
   eapply exec_straight_trans. eexact A. 
   apply exec_straight_one. simpl. 
-  rewrite Heqo; rewrite Heqo0. 
+  rewrite TC1; rewrite TC2. 
   destruct b1. simpl in *. subst b2. auto. auto.
   auto.
   split. apply agree_nextinstr. eapply agree_exten_temps; eauto.
-  rewrite H2; congruence.
-Qed.
+  rewrite H1; congruence.
 
-Lemma exec_Mjumptable_prop:
-  forall (s : list stackframe) (fb : block) (f : function) (sp : val)
-         (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction)
-         (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
-         (c' : Mach.code),
-  rs arg = Vint n ->
-  list_nth_z tbl (Int.unsigned n) = Some lbl ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl (fn_code f) = Some c' ->
-  exec_instr_prop
-    (Machsem.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
-    (Machsem.State s fb sp c' (undef_temps rs) m).
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H6. 
+- (* Mjumptable *)
+  inv AT. monadInv H5. 
   exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H5); intro NOOV.
+  generalize (transf_function_no_overflow _ _ H4); intro NOOV.
   exploit find_label_goto_label. eauto. eauto. instantiate (2 := rs0#ECX <- Vundef #EDX <- Vundef). 
-  rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. eauto. eauto. 
+  repeat (rewrite Pregmap.gso by auto with asmgen). eauto. eauto. 
   intros [tc' [rs' [A [B C]]]].
   exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
   eapply find_instr_tail; eauto. 
-  simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eauto.
+  simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eauto.
   econstructor; eauto. 
-  eapply agree_exten_temps; eauto. intros. rewrite C; auto with ppcgen. 
-  repeat rewrite Pregmap.gso; auto with ppcgen. 
+  eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simplifs. 
   congruence.
-Qed.
 
-Lemma exec_Mreturn_prop:
-  forall (s : list stackframe) (fb stk : block) (soff : int)
-         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m',
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
-  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-  exec_instr_prop (Machsem.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
-                  (Returnstate s ms m').
-Proof.
-  intros; red; intros; inv MS.
-  assert (f0 = f) by congruence. subst f0.
+- (* Mreturn *)
   inv AT. 
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. 
+  exploit Mem.loadv_extends. eauto. eexact H. auto. simpl. intros [parent' [A B]]. 
   exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]].
-  exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
-  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. 
-  monadInv H6.
+  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 ESP) (Vint (fn_retaddr_ofs f))) = Some ra).
+Opaque Int.repr.
+    erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l.
+    eapply rsa_contains; eauto.
+  exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]].
+  assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')).
+    apply match_stack_change_bound with stk.
+    eapply match_stack_free_left; eauto.
+    eapply match_stack_free_left; eauto.
+    eapply match_stack_free_right; eauto. omega.
+    apply Z.lt_le_incl. change (Mem.valid_block m'' stk).
+    eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. 
+    eapply retaddr_stored_at_valid; eauto.
+  monadInv H5.
   exploit code_tail_next_int; eauto. intro CT1.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto.
   apply star_one. eapply exec_step_internal. 
-  transitivity (Val.add rs#PC Vone). auto. rewrite <- H3. simpl. eauto.
+  transitivity (Val.add rs0#PC Vone). auto. rewrite <- H2. simpl. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto. traceEq.
   constructor; auto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-Qed.
 
-Lemma exec_function_internal_prop:
-  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
-         (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mem.alloc m 0 (fn_stacksize f) = (m1, stk) ->
-  let sp := Vptr stk Int.zero in
-  store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
-  store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
-  exec_instr_prop (Machsem.Callstate s fb ms m) E0
-                  (Machsem.State s fb sp (fn_code f) (undef_temps ms) m3).
-Proof.
-  intros; red; intros; inv MS.
+- (* internal function *)
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
   generalize EQ; intros EQ'. monadInv EQ'. 
   destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1.
   unfold store_stack in *. 
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
   intros [m1' [C D]].
-  exploit Mem.storev_extends. eauto. eexact H1. eauto. eauto. 
-  intros [m2' [E F]].
-  exploit Mem.storev_extends. eexact F. eauto. eauto. eauto. 
-  intros [m3' [P Q]].
+  assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto).
+  exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. 
+  intros [m2' [F G]].
+  exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. 
+  auto. auto. auto. auto. eauto. 
+  intros [m3' [P [Q R]]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
-  rewrite <- H4; simpl. eauto. 
-  simpl. rewrite C. simpl in E. rewrite (sp_val _ _ _ AG) in E. rewrite E.
-  rewrite ATLR. simpl in P. rewrite P. eauto. 
-  econstructor; eauto. 
-  unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with ppcgen. 
+  subst x; simpl. rewrite Int.unsigned_zero. simpl. eauto. 
+  simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F.
+  rewrite Int.add_zero_l. rewrite P. eauto. 
+  econstructor; eauto.
+  assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto).
+  rewrite <- STK in STACKS. simpl in F. simpl in H1.
+  eapply match_stack_invariant; eauto.
+  intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. 
+  eapply Mem.perm_store_2; eauto. unfold block; omega.
+  intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. 
+  eapply Mem.perm_alloc_1; eauto. 
+  intros. erewrite Mem.load_store_other. 2: eauto.
+  erewrite Mem.load_store_other. 2: eauto. 
+  eapply Mem.load_alloc_other; eauto.
+  left; unfold block; omega.
+  left; unfold block; omega.
+  unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. 
   rewrite ATPC. simpl. constructor; eauto.
-  subst x. eapply code_tail_next_int. rewrite list_length_z_cons. omega. 
+  subst x. unfold fn_code. eapply code_tail_next_int. rewrite list_length_z_cons. omega. 
   constructor. 
   apply agree_nextinstr. eapply agree_change_sp; eauto.
-  apply agree_exten_temps with rs; eauto.
-  intros. apply Pregmap.gso; auto with ppcgen.
+  apply agree_exten_temps with rs0; eauto.
+  intros; Simplifs.
   congruence. 
-  intros. rewrite nextinstr_inv; auto with ppcgen. 
-  rewrite Pregmap.gso; auto with ppcgen. 
-  rewrite Pregmap.gss. eapply agree_sp; eauto. 
-Qed.
+  intros. Simplifs. eapply agree_sp; eauto.
 
-Lemma exec_function_external_prop:
-  forall (s : list stackframe) (fb : block) (ms : Mach.regset)
-         (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
-         (ef : external_function) (args : list val) (res : val) (m': mem),
-  Genv.find_funct_ptr ge fb = Some (External ef) ->
-  external_call ef ge args m t0 res m' ->
-  Machsem.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
-  ms' = Regmap.set (loc_result (ef_sig ef)) res ms ->
-  exec_instr_prop (Machsem.Callstate s fb ms m)
-               t0 (Machsem.Returnstate s ms' m').
-Proof.
-  intros; red; intros; inv MS.
+- (* external function *)
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B.
   exploit extcall_arguments_match; eauto. 
@@ -1334,63 +985,38 @@ Proof.
   eapply external_call_symbols_preserved; eauto. 
   exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
+  rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). 
+  eapply match_stack_extcall; eauto.
+  intros. eapply external_call_max_perm; eauto.
+  eapply external_call_nextblock; eauto.
   unfold loc_external_result.
   eapply agree_set_mreg; eauto. 
-  rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss. auto. 
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-Qed.
+  rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. 
+  intros; Simplifs.
 
-Lemma exec_return_prop:
-  forall (s : list stackframe) (fb : block) (sp ra : val)
-         (c : Mach.code) (ms : Mach.regset) (m : mem),
-  exec_instr_prop (Machsem.Returnstate (Stackframe fb sp ra c :: s) ms m) E0
-                  (Machsem.State s fb sp c ms m).
-Proof.
-  intros; red; intros; inv MS. inv STACKS. simpl in *.
+- (* return *)
+  inv STACKS. simpl in *.
   right. split. omega. split. auto. 
-  econstructor; eauto. rewrite ATPC; eauto.  
-  congruence.
+  econstructor; eauto. congruence.
 Qed.
 
-Theorem transf_instr_correct:
-  forall s1 t s2, Machsem.step ge s1 t s2 ->
-  exec_instr_prop s1 t s2.
-Proof
-  (Machsem.step_ind ge exec_instr_prop
-           exec_Mlabel_prop
-           exec_Mgetstack_prop
-           exec_Msetstack_prop
-           exec_Mgetparam_prop
-           exec_Mop_prop
-           exec_Mload_prop
-           exec_Mstore_prop
-           exec_Mcall_prop
-           exec_Mtailcall_prop
-           exec_Mbuiltin_prop
-           exec_Mannot_prop
-           exec_Mgoto_prop
-           exec_Mcond_true_prop
-           exec_Mcond_false_prop
-           exec_Mjumptable_prop
-           exec_Mreturn_prop
-           exec_function_internal_prop
-           exec_function_external_prop
-           exec_return_prop).
-
 Lemma transf_initial_states:
-  forall st1, Machsem.initial_state prog st1 ->
+  forall st1, Mach.initial_state prog st1 ->
   exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. unfold ge0 in *.
+  exploit functions_translated; eauto. intros [tf [A B]]. 
   econstructor; split.
   econstructor.
   eapply Genv.init_mem_transf_partial; eauto.
   replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
-     with (Vptr fb Int.zero).
-  econstructor; eauto. constructor. apply Mem.extends_refl.
-  split. auto. unfold parent_sp; congruence.
-  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
-  destruct r; simpl; congruence.
+     with (Vptr b Int.zero).
+  econstructor; eauto.
+  constructor.
+  apply Mem.extends_refl.
+  split. auto. intros. rewrite Regmap.gi. auto. 
+  reflexivity. 
+  exact I.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. unfold ge; rewrite H1. auto.
@@ -1398,21 +1024,22 @@ Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
-  match_states st1 st2 -> Machsem.final_state st1 r -> Asm.final_state st2 r.
+  match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. constructor. auto. 
+  intros. inv H0. inv H. inv STACKS. constructor.
+  auto. 
   compute in H1. 
   generalize (preg_val _ _ _ AX AG). rewrite H1. intros LD; inv LD. auto.
 Qed.
 
 Theorem transf_program_correct:
-  forward_simulation (Machsem.semantics prog) (Asm.semantics tprog).
+  forward_simulation (Mach.semantics prog) (Asm.semantics tprog).
 Proof.
   eapply forward_simulation_star with (measure := measure).
   eexact symbols_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
-  exact transf_instr_correct. 
+  exact step_simulation.
 Qed.
 
 End PRESERVATION.