Finished backtracking (cf previous commit) for ARM and PowerPC.

ARM: slightly shorter code generated for indirect memory accesses.


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

1 files changed, 219 insertions, 300 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 6c95744..7699fef 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -86,8 +86,8 @@ Proof.
 Qed.
 
 Lemma exec_straight_exec:
-  forall f c ep tf tc c' rs m rs' m',
-  transl_code_at_pc ge (rs PC) f c ep tf tc ->
+  forall fb f c ep tf tc c' rs m rs' m',
+  transl_code_at_pc ge (rs PC) fb 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.
@@ -98,11 +98,11 @@ Proof.
 Qed.
 
 Lemma exec_straight_at:
-  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 ->
+  forall fb f c ep tf tc c' ep' tc' rs m rs' m',
+  transl_code_at_pc ge (rs PC) fb 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 ge (rs' PC) f c' ep' tf tc'.
+  transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
 Proof.
   intros. inv H. 
   exploit exec_straight_steps_2; eauto. 
@@ -112,39 +112,6 @@ Proof.
   rewrite PC'. constructor; auto.
 Qed.
 
-(** The [find_label] function returns the code tail starting at the
-  given label.  A connection with [code_tail] is then established. *)
-
-Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
-  match c with
-  | nil => None
-  | instr :: c' =>
-      if is_label lbl instr then Some c' else find_label lbl c'
-  end.
-
-Lemma label_pos_code_tail:
-  forall lbl c pos c',
-  find_label lbl c = Some c' ->
-  exists pos',
-  label_pos lbl pos c = Some pos' 
-  /\ code_tail (pos' - pos) c c'
-  /\ pos < pos' <= pos + list_length_z c.
-Proof.
-  induction c. 
-  simpl; intros. discriminate.
-  simpl; intros until c'.
-  case (is_label lbl a).
-  intro EQ; injection EQ; intro; subst c'.
-  exists (pos + 1). split. auto. split.
-  replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. 
-  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. 
-  intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
-  exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
-  constructor. auto. 
-  rewrite list_length_z_cons. omega.
-Qed.
-
 (** The following lemmas show that the translation from Mach to PPC
   preserves labels, in the sense that the following diagram commutes:
 <<
@@ -163,180 +130,169 @@ Qed.
 
 Section TRANSL_LABEL.
 
-Variable lbl: label.
-
 Remark loadimm_label:
-  forall r n k, find_label lbl (loadimm r n k) = find_label lbl k.
+  forall r n k, tail_nolabel k (loadimm r n k).
 Proof.
   intros. unfold loadimm. 
-  case (Int.eq (high_s n) Int.zero). reflexivity. 
-  case (Int.eq (low_s n) Int.zero). reflexivity.
-  reflexivity.
+  case (Int.eq (high_s n) Int.zero). TailNoLabel.
+  case (Int.eq (low_s n) Int.zero); TailNoLabel.
 Qed.
-Hint Rewrite loadimm_label: labels.
+Hint Resolve loadimm_label: labels.
 
 Remark addimm_label:
-  forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
+  forall r1 r2 n k, tail_nolabel k (addimm r1 r2 n k).
 Proof.
   intros; unfold addimm. 
-  case (Int.eq (high_s n) Int.zero). reflexivity.
-  case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity.
+  case (Int.eq (high_s n) Int.zero). TailNoLabel.
+  case (Int.eq (low_s n) Int.zero); TailNoLabel.
 Qed.
-Hint Rewrite addimm_label: labels.
+Hint Resolve addimm_label: labels.
 
 Remark andimm_base_label:
-  forall r1 r2 n k, find_label lbl (andimm_base r1 r2 n k) = find_label lbl k.
+  forall r1 r2 n k, tail_nolabel k (andimm_base r1 r2 n k).
 Proof.
   intros; unfold andimm_base. 
-  case (Int.eq (high_u n) Int.zero). reflexivity.
-  case (Int.eq (low_u n) Int.zero). reflexivity.
-  autorewrite with labels. reflexivity.
+  case (Int.eq (high_u n) Int.zero). TailNoLabel.
+  case (Int.eq (low_u n) Int.zero). TailNoLabel.
+  eapply tail_nolabel_trans; TailNoLabel.
 Qed.
-Hint Rewrite andimm_base_label: labels.
+Hint Resolve andimm_base_label: labels.
 
 Remark andimm_label:
-  forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k.
+  forall r1 r2 n k, tail_nolabel k (andimm r1 r2 n k).
 Proof.
   intros; unfold andimm. 
-  case (is_rlw_mask n). reflexivity.
-  autorewrite with labels. reflexivity.
+  case (is_rlw_mask n); TailNoLabel.
 Qed.
-Hint Rewrite andimm_label: labels.
+Hint Resolve andimm_label: labels.
 
 Remark orimm_label:
-  forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k.
+  forall r1 r2 n k, tail_nolabel k (orimm r1 r2 n k).
 Proof.
   intros; unfold orimm. 
-  case (Int.eq (high_u n) Int.zero). reflexivity.
-  case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity.
+  case (Int.eq (high_u n) Int.zero). TailNoLabel.
+  case (Int.eq (low_u n) Int.zero); TailNoLabel.
 Qed.
-Hint Rewrite orimm_label: labels.
+Hint Resolve orimm_label: labels.
 
 Remark xorimm_label:
-  forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k.
+  forall r1 r2 n k, tail_nolabel k (xorimm r1 r2 n k).
 Proof.
   intros; unfold xorimm. 
-  case (Int.eq (high_u n) Int.zero). reflexivity.
-  case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity.
+  case (Int.eq (high_u n) Int.zero). TailNoLabel.
+  case (Int.eq (low_u n) Int.zero); TailNoLabel.
 Qed.
-Hint Rewrite xorimm_label: labels.
+Hint Resolve xorimm_label: labels.
 
 Remark rolm_label:
-  forall r1 r2 amount mask k, find_label lbl (rolm r1 r2 amount mask k) = find_label lbl k.
+  forall r1 r2 amount mask k, tail_nolabel k (rolm r1 r2 amount mask k).
 Proof.
   intros; unfold rolm. 
-  case (is_rlw_mask mask). reflexivity.
-Opaque Int.eq.
-  simpl. autorewrite with labels. auto.
+  case (is_rlw_mask mask); TailNoLabel.
 Qed.
-Hint Rewrite rolm_label: labels.
+Hint Resolve rolm_label: labels.
 
 Remark loadind_label:
   forall base ofs ty dst k c,
-  loadind base ofs ty dst k = OK c ->
-  find_label lbl c = find_label lbl k.
+  loadind base ofs ty dst k = OK c -> tail_nolabel k c.
 Proof.
   unfold loadind; intros.
-  destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H;
-  autorewrite with labels; auto.
+  destruct ty; destruct (Int.eq (high_s ofs) Int.zero);
+  TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
 Remark storeind_label:
   forall base ofs ty src k c,
-  storeind base src ofs ty k = OK c ->
-  find_label lbl c = find_label lbl k.
+  storeind base src ofs ty k = OK c -> tail_nolabel k c.
 Proof.
   unfold storeind; intros.
-  destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H;
-  autorewrite with labels; auto.
+  destruct ty; destruct (Int.eq (high_s ofs) Int.zero);
+  TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
 Remark floatcomp_label:
-  forall cmp r1 r2 k, find_label lbl (floatcomp cmp r1 r2 k) = find_label lbl k.
+  forall cmp r1 r2 k, tail_nolabel k (floatcomp cmp r1 r2 k).
 Proof.
-  intros; unfold floatcomp. destruct cmp; reflexivity.
+  intros; unfold floatcomp. destruct cmp; TailNoLabel.
 Qed.
-Hint Rewrite floatcomp_label: labels.
+Hint Resolve floatcomp_label: labels.
 
 Remark transl_cond_label:
   forall cond args k c,
-  transl_cond cond args k = OK c -> find_label lbl c = find_label lbl k.
+  transl_cond cond args k = OK c -> tail_nolabel k c.
 Proof.
-  unfold transl_cond; intros; destruct cond; 
-  (destruct args; 
-  [try discriminate | destruct args;
-  [try discriminate | destruct args; try discriminate]]);
-  monadInv H; autorewrite with labels; auto.
-  destruct (Int.eq (high_s i) Int.zero); inv EQ0; autorewrite with labels; auto.
-  destruct (Int.eq (high_u i) Int.zero); inv EQ0; autorewrite with labels; auto.
+  unfold transl_cond; intros; destruct cond; TailNoLabel;
+  eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
 Remark transl_cond_op_label:
   forall cond args r k c,
-  transl_cond_op cond args r k = OK c -> find_label lbl c = find_label lbl k.
+  transl_cond_op cond args r k = OK c -> tail_nolabel k c.
 Proof.
   unfold transl_cond_op; intros; destruct (classify_condition cond args);
-  monadInv H; auto.
-  erewrite transl_cond_label. 2: eauto. 
-  destruct (snd (crbit_for_cond c0)); auto.
+  TailNoLabel.
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto.
+  destruct (snd (crbit_for_cond c0)); TailNoLabel.
 Qed.
 
 Remark transl_op_label:
   forall op args r k c,
-  transl_op op args r k = OK c -> find_label lbl c = find_label lbl k.
+  transl_op op args r k = OK c -> tail_nolabel k c.
 Proof.
-  unfold transl_op; intros; destruct op; try (eapply transl_cond_op_label; eauto; fail);
-  (destruct args; 
-  [try discriminate | destruct args;
-  [try discriminate | destruct args; try discriminate]]);
-  try (monadInv H); autorewrite with labels; auto.
-  destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; auto.
-  destruct (symbol_is_small_data i i0); auto.
-  destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto.
-  destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto.
+Opaque Int.eq.
+  unfold transl_op; intros; destruct op; TailNoLabel.
+  destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
+  destruct (symbol_is_small_data i i0); TailNoLabel.
+  destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
+  destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
+  eapply transl_cond_op_label; eauto.
 Qed.
 
 Remark transl_memory_access_label:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
          addr args temp k c,
   transl_memory_access mk1 mk2 addr args temp k = OK c ->
-  (forall c r, is_label lbl (mk1 c r) = false) ->
-  (forall r1 r2, is_label lbl (mk2 r1 r2) = false) ->
-  find_label lbl c = find_label lbl k.
+  (forall c r, nolabel (mk1 c r)) ->
+  (forall r1 r2, nolabel (mk2 r1 r2)) ->
+  tail_nolabel k c.
 Proof.
-  unfold transl_memory_access; intros; destruct addr; 
-  (destruct args; 
-  [try discriminate | destruct args;
-  [try discriminate | destruct args; try discriminate]]);
-  monadInv H; autorewrite with labels; auto.
-  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto.
-  simpl; rewrite H1; auto.
-  destruct (symbol_is_small_data i i0); simpl; rewrite H0; auto.
-  simpl; rewrite H0; auto.
-  destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto.
+  unfold transl_memory_access; intros; destruct addr; TailNoLabel.
+  destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
+  destruct (symbol_is_small_data i i0); TailNoLabel.
+  destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
 Qed.
 
 Lemma transl_instr_label:
   forall f i ep k c,
   transl_instr f i ep k = OK c ->
-  find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
+  match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end.
 Proof.
-  unfold transl_instr, Mach.is_label; intros; destruct i; try (monadInv H);
-  autorewrite with labels; auto.
+  unfold transl_instr; intros; destruct i; TailNoLabel.
   eapply loadind_label; eauto.
   eapply storeind_label; eauto.
-  destruct ep. eapply loadind_label; eauto.
-  monadInv H. transitivity (find_label lbl x); eapply loadind_label; eauto. 
+  eapply loadind_label; eauto.
+  eapply tail_nolabel_trans; eapply loadind_label; eauto.
   eapply transl_op_label; eauto.
-  destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto.
-  destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto.
-  destruct s0; monadInv H; auto.
-  destruct s0; monadInv H; auto.
-  erewrite transl_cond_label. 2: eauto. destruct (snd (crbit_for_cond c0)); auto.
+  destruct m; monadInv H; (eapply tail_nolabel_trans; [eapply transl_memory_access_label; TailNoLabel|TailNoLabel]).
+  destruct m; monadInv H; eapply transl_memory_access_label; TailNoLabel.
+  destruct s0; monadInv H; TailNoLabel.
+  destruct s0; monadInv H; TailNoLabel.
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto. 
+  destruct (snd (crbit_for_cond c0)); TailNoLabel.
+Qed.
+
+Lemma transl_instr_label':
+  forall lbl f i ep k c,
+  transl_instr f i ep k = OK c ->
+  find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
+Proof.
+  intros. exploit transl_instr_label; eauto.
+  destruct i; try (intros [A B]; apply B). 
+  intros. subst c. simpl. auto.
 Qed.
 
 Lemma transl_code_label:
-  forall f c ep tc,
+  forall lbl f c ep tc,
   transl_code f c ep = OK tc ->
   match Mach.find_label lbl c with
   | None => find_label lbl tc = None
@@ -345,7 +301,7 @@ Lemma transl_code_label:
 Proof.
   induction c; simpl; intros.
   inv H. auto.
-  monadInv H. rewrite (transl_instr_label _ _ _ _ _ EQ0).
+  monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0).
   generalize (Mach.is_label_correct lbl a). 
   destruct (Mach.is_label lbl a); intros.
   subst a. simpl in EQ. exists x; auto.
@@ -353,7 +309,7 @@ Proof.
 Qed.
 
 Lemma transl_find_label:
-  forall f tf,
+  forall lbl f tf,
   transf_function f = OK tf ->
   match Mach.find_label lbl f.(Mach.fn_code) with
   | None => find_label lbl tf = None
@@ -361,8 +317,7 @@ Lemma transl_find_label:
   end.
 Proof.
   intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0.
-  monadInv EQ. simpl.
-  eapply transl_code_label; eauto. 
+  monadInv EQ. simpl. eapply transl_code_label; eauto. 
 Qed.
 
 End TRANSL_LABEL.
@@ -378,7 +333,7 @@ Lemma find_label_goto_label:
   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 ge (rs' PC) f c' false tf tc'
+  /\ 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. 
@@ -394,6 +349,21 @@ Proof.
   intros. apply Pregmap.gso; auto.
 Qed.
 
+(** Existence of return addresses *)
+
+Lemma return_address_exists:
+  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. eapply Asmgenproof0.return_address_exists; eauto. 
+- intros. exploit transl_instr_label; eauto. 
+  destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
+- intros. monadInv H0. 
+  destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. monadInv EQ.
+  exists x; exists false; split; auto. unfold fn_code. repeat constructor.
+- exact transf_function_no_overflow.
+Qed.
+
 (** * Proof of semantic preservation *)
 
 (** Semantic preservation is proved using simulation diagrams
@@ -414,49 +384,49 @@ Qed.
 
 Inductive match_states: Mach.state -> Asm.state -> Prop :=
   | match_states_intro:
-      forall s f sp c ep ms m m' rs tf tc ra
-        (STACKS: match_stack ge s m m' ra sp)
+      forall s fb sp c ep ms m m' rs f tf tc
+        (STACKS: match_stack ge s)
+        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
         (MEXT: Mem.extends m m')
-        (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)
+        (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
+        (AG: agree ms sp rs)
         (DXP: ep = true -> rs#GPR11 = parent_sp s),
-      match_states (Mach.State s f (Vptr sp Int.zero) c ms m)
+      match_states (Mach.State s fb sp c ms m)
                    (Asm.State rs m')
   | match_states_call:
-      forall s fd ms m m' rs fb
-        (STACKS: match_stack ge s m m' (rs LR) (Mem.nextblock m))
+      forall s fb ms m m' rs
+        (STACKS: match_stack ge s)
         (MEXT: Mem.extends m m')
         (AG: agree ms (parent_sp s) rs)
         (ATPC: rs PC = Vptr fb Int.zero)
-        (FUNCT: Genv.find_funct_ptr ge fb = Some fd)
-        (WTRA: Val.has_type (rs LR) Tint),
-      match_states (Mach.Callstate s fd ms m)
+        (ATLR: rs RA = parent_ra s),
+      match_states (Mach.Callstate s fb ms m)
                    (Asm.State rs m')
   | match_states_return:
       forall s ms m m' rs
-        (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m))
+        (STACKS: match_stack ge s)
         (MEXT: Mem.extends m m')
-        (AG: agree ms (parent_sp s) rs),
+        (AG: agree ms (parent_sp s) rs)
+        (ATPC: rs PC = parent_ra s),
       match_states (Mach.Returnstate s ms m)
                    (Asm.State rs m').
 
 Lemma exec_straight_steps:
-  forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra,
-  match_stack ge s m2 m2' ra sp ->
+  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,
+  match_stack ge s ->
   Mem.extends m2 m2' ->
-  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 ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  transl_code_at_pc ge (rs1 PC) fb 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 (Vptr sp Int.zero) rs2
+    /\ agree ms2 sp rs2
     /\ (r11_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
-  match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'.
+  match_states (Mach.State s fb sp 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. 
@@ -464,23 +434,23 @@ Proof.
 Qed.
 
 Lemma exec_straight_steps_goto:
-  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 ->
+  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
+  match_stack ge s ->
   Mem.extends m2 m2' ->
-  retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
   Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc ->
+  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
   r11_is_parent ep i = false ->
   (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 (Vptr sp Int.zero) rs2
+    /\ agree ms2 sp 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 (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'.
+  match_states (Mach.State s fb sp 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.
@@ -524,7 +494,7 @@ Qed.
 (** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
 
 Theorem step_simulation:
-  forall S1 t S2, Mach.step ge S1 t S2 ->
+  forall S1 t S2, Mach.step return_address_offset 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.
@@ -551,8 +521,6 @@ Proof.
   assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m2' [A B]]. 
   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 with asmgen. intros [rs' [P Q]].
   exists rs'; split. eauto.
@@ -560,11 +528,12 @@ Proof.
   simpl; intros. rewrite Q; auto with asmgen.
 
 - (* Mgetparam *)
+  assert (f0 = f) by congruence; subst f0.
   unfold load_stack in *. 
-  exploit Mem.loadv_extends. eauto. eexact H. auto. 
+  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 H0. auto. 
+  exploit Mem.loadv_extends. eauto. eexact H1. auto. 
   intros [v' [C D]].
 Opaque loadind.
   left; eapply exec_straight_steps; eauto; intros.
@@ -591,7 +560,7 @@ Opaque loadind.
   apply preg_of_not_GPR11; auto.
 
 - (* Mop *)
-  assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). 
+  assert (eval_operation tge sp 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. 
@@ -602,7 +571,7 @@ Opaque loadind.
   rewrite R; auto. apply preg_of_not_GPR11; auto.
 
 - (* Mload *)
-  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). 
+  assert (eval_addressing tge sp 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.
@@ -615,95 +584,83 @@ Opaque loadind.
   simpl; congruence.
 
 - (* Mstore *)
-  assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). 
+  assert (eval_addressing tge sp 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 (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.
-  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. intros; auto with asmgen. 
   simpl; congruence.
 
 - (* Mcall *)
+  assert (f0 = f) by congruence.  subst f0.
   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 H3.
+  destruct ros as [rf|fid]; simpl in H; monadInv H5.
 + (* 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 (rs rf = Vptr f' Int.zero).
+    destruct (rs rf); try discriminate.
+    revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
+  assert (rs0 x0 = Vptr f' Int.zero).
+    exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto.
+  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
   generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2.
-  assert (TCA: transl_code_at_pc ge (Vptr b (Int.add (Int.add ofs Int.one) Int.one)) f c false tf x).
-    econstructor; eauto. 
+  assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add (Int.add ofs Int.one) Int.one)) fb f c false tf x).
+    econstructor; eauto.
+  exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
   eapply plus_left. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto.
-  apply star_one. eapply exec_step_internal. Simpl. rewrite <- H0; simpl; eauto.
+  apply star_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
   simpl. eauto.
   traceEq.
   econstructor; eauto. 
-  econstructor; eauto.
-  Simpl. rewrite <- H0; eexact TCA.
-  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  econstructor; eauto. 
+  eapply agree_sp_def; eauto.
   simpl. eapply agree_exten; eauto. intros. Simpl. 
-  Simpl. rewrite <- H0. exact I.
+  Simpl. rewrite <- H2. auto.
 + (* 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).
+  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb 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 FS. eauto.
+  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto.
   econstructor; eauto. 
   econstructor; eauto.
-  rewrite <- H0. eexact TCA.
-  change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. 
+  eapply agree_sp_def; eauto.
   simpl. eapply agree_exten; eauto. intros. Simpl.
-  auto.
-  rewrite <- H0. exact I.
+  Simpl. rewrite <- H2. auto.
 
 - (* Mtailcall *)
+Opaque Int.repr.
+  assert (f0 = f) by congruence.  subst f0.
   inversion AT; subst.
   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]]. 
+    eapply transf_function_no_overflow; eauto.  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
+  exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]].
   exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (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.
+  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 *)
-  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.
-  set (rs2 := nextinstr (rs0#CTR <- (Vptr bf Int.zero))).
-  set (rs3 := nextinstr (rs2#GPR0 <- ra)).
-  set (rs4 := nextinstr (rs3#LR <- ra)).
+  assert (rs rf = Vptr f' Int.zero).
+    destruct (rs rf); try discriminate.
+    revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
+  assert (rs0 x0 = Vptr f' Int.zero).
+    exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto.
+  set (rs2 := nextinstr (rs0#CTR <- (Vptr f' Int.zero))).
+  set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))).
+  set (rs4 := nextinstr (rs3#LR <- (parent_ra s))).
   set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))).
   set (rs6 := rs5#PC <- (rs5 CTR)).
   assert (exec_straight tge tf
@@ -712,21 +669,23 @@ Opaque Int.repr.
             rs0 m'0
             (Pbctr :: x) rs5 m2').
   apply exec_straight_step with rs2 m'0. 
-  simpl. rewrite H6. auto. auto.
+  simpl. rewrite H9. auto. auto.
   apply exec_straight_step with rs3 m'0.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  change (rs2 GPR1) with (rs0 GPR1). rewrite C. auto. congruence. auto.
+  change (rs2 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). 
+  simpl. rewrite C. auto. congruence. auto.
   apply exec_straight_step with rs4 m'0.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
-  simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG).
+  simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). 
+  simpl. rewrite A.
   rewrite E. reflexivity. reflexivity.
   left; exists (State rs6 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
   change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone).
-  rewrite <- H3; simpl. eauto.
+  rewrite <- H4; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
@@ -734,20 +693,17 @@ Opaque Int.repr.
   (* match states *)
   econstructor; eauto.
 Hint Resolve agree_nextinstr agree_set_other: asmgen.
-  assert (AG4: agree rs (Vptr stk Int.zero) rs4).
+  assert (AG4: agree rs (Vptr stk soff) rs4).
     unfold rs4, rs3, rs2; auto 10 with asmgen.
   assert (AG5: agree rs (parent_sp s) rs5).
     unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto. 
     eapply parent_sp_def; eauto. 
   unfold rs6, rs5; auto 10 with asmgen.
-  reflexivity.
-  change (rs6 LR) with ra. eapply retaddr_stored_at_type; eauto. 
 + (* Direct call *)
-  destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate.
-  set (rs2 := nextinstr (rs0#GPR0 <- ra)).
-  set (rs3 := nextinstr (rs2#LR <- ra)).
+  set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))).
+  set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
   set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
-  set (rs5 := rs4#PC <- (Vptr bf Int.zero)).
+  set (rs5 := rs4#PC <- (Vptr f' Int.zero)).
   assert (exec_straight tge tf
             (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0
              :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid :: x)
@@ -755,33 +711,30 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
             (Pbs fid :: x) rs4 m2').
   apply exec_straight_step with rs2 m'0. 
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  rewrite C. auto. congruence. auto.
+  rewrite <- (sp_val _ _ _ AG). simpl. rewrite C. auto. congruence. auto.
   apply exec_straight_step with rs3 m'0.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
-  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG).
+  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). simpl. rewrite A. 
   rewrite E. reflexivity. reflexivity.
   left; exists (State rs5 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone).
-  rewrite <- H3; simpl. eauto.
+  rewrite <- H4; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto. traceEq.
+  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. traceEq.
   (* match states *)
   econstructor; eauto.
-Hint Resolve agree_nextinstr agree_set_other: asmgen.
-  assert (AG3: agree rs (Vptr stk Int.zero) rs3).
+  assert (AG3: agree rs (Vptr stk soff) rs3).
     unfold rs3, rs2; auto 10 with asmgen.
   assert (AG4: agree rs (parent_sp s) rs4).
     unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto. 
     eapply parent_sp_def; eauto. 
   unfold rs5; auto 10 with asmgen.
-  reflexivity.
-  change (rs5 LR) with ra. eapply retaddr_stored_at_type; eauto.
 
 - (* Mbuiltin *)
   inv AT. monadInv H3. 
@@ -795,16 +748,11 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   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).
   Simpl. rewrite <- H0. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
   apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. 
   rewrite Pregmap.gss. auto. 
   intros. Simpl. 
-  eapply retaddr_stored_at_extcall; eauto. 
-  intros; eapply external_call_max_perm; eauto. 
   congruence.
 
 - (* Mannot *)
@@ -820,18 +768,15 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   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.
 
 - (* Mgoto *)
-  inv AT. monadInv H3. 
+  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.
@@ -843,6 +788,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   congruence.
 
 - (* Mcond true *)
+  assert (f0 = f) by congruence. subst f0.
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
   left; eapply exec_straight_steps_goto; eauto.
   intros. simpl in TR.
@@ -873,9 +819,10 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   simpl. congruence.
 
 - (* Mjumptable *)
-  inv AT. monadInv H5. 
+  assert (f0 = f) by congruence. subst f0.
+  inv AT. monadInv H6. 
   exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H4); intro NOOV.
+  generalize (transf_function_no_overflow _ _ H5); intro NOOV.
   exploit find_label_goto_label. eauto. eauto.
   instantiate (2 := rs0#GPR12 <- Vundef #CTR <- Vundef). 
   Simpl. eauto.
@@ -885,36 +832,27 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
   eapply find_instr_tail; eauto. 
-  simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
+  simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
   econstructor; eauto. 
   eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. 
   congruence.
 
 - (* Mreturn *)
-  inversion AT; subst. 
+  assert (f0 = f) by congruence. subst f0.
+  inversion AT; subst.
   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 H. 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.
-  assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (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.
-  set (rs2 := nextinstr (rs0#GPR0 <- ra)).
-  set (rs3 := nextinstr (rs2#LR <- ra)).
+  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.
+  set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))).
+  set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
   set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
-  set (rs5 := rs4#PC <- ra).
+  set (rs5 := rs4#PC <- (parent_ra s)).
   assert (exec_straight tge tf
            (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1
            :: Pmtlr GPR0
@@ -932,7 +870,7 @@ Opaque Int.repr.
   eapply exec_straight_exec; eauto.
   econstructor.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). 
-  rewrite <- H2. simpl. eauto.
+  rewrite <- H3. simpl. eauto.
   eapply functions_transl; eauto.
   eapply find_instr_tail. 
   eapply code_tail_next_int; auto.
@@ -941,7 +879,7 @@ Opaque Int.repr.
   reflexivity. traceEq.
   (* match states *)
   econstructor; eauto. 
-  assert (AG3: agree rs (Vptr stk Int.zero) rs3). 
+  assert (AG3: agree rs (Vptr stk soff) rs3). 
     unfold rs3, rs2; auto 10 with asmgen.
   assert (AG4: agree rs (parent_sp s) rs4).
     unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto. 
@@ -955,12 +893,10 @@ Opaque Int.repr.
   unfold store_stack in *. 
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
   intros [m1' [C D]].
-  assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto).
-  exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. 
+  exploit Mem.storev_extends. eexact D. 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]]].
+  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. 
+  intros [m3' [P Q]].
   (* Execution of function prologue *)
   monadInv EQ0.
   set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)).
@@ -977,23 +913,11 @@ Opaque Int.repr.
   simpl. auto.
   simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
   change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. 
-  rewrite Int.add_zero_l. rewrite P. auto. congruence.
+  rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence.
   auto. auto. auto.
   left; exists (State rs4 m3'); split.
   eapply exec_straight_steps_1; eauto. unfold fn_code; omega. constructor. 
   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.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). 
   rewrite ATPC. simpl. constructor; eauto.
   subst x. unfold fn_code. eapply code_tail_next_int. omega. 
@@ -1019,10 +943,6 @@ Opaque Int.repr.
   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 asmgen. rewrite Pregmap.gss. auto. 
@@ -1030,7 +950,8 @@ Opaque Int.repr.
 
 - (* return *)
   inv STACKS. simpl in *.
-  right. split. omega. split. auto. 
+  right. split. omega. split. auto.
+  rewrite <- ATPC in H5. 
   econstructor; eauto. congruence.
 Qed.
 
@@ -1039,21 +960,19 @@ Lemma transf_initial_states:
   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 b Int.zero).
+     with (Vptr fb Int.zero).
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
-  split. auto. intros. rewrite Regmap.gi. auto. 
-  reflexivity. 
-  exact I.
+  split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. 
   unfold symbol_offset. 
-  rewrite (transform_partial_program_main _ _ TRANSF). 
-  rewrite symbols_preserved. unfold ge; rewrite H1. auto.
+  rewrite (transform_partial_program_main _ _ TRANSF).
+  rewrite symbols_preserved. 
+  unfold ge; rewrite H1. auto.
 Qed.
 
 Lemma transf_final_states:
@@ -1067,7 +986,7 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forward_simulation (Mach.semantics prog) (Asm.semantics tprog).
+  forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
   eapply forward_simulation_star with (measure := measure).
   eexact symbols_preserved.