Partial backtracking on previous commit: the "hole in Mach stack frame"

trick prevents a future mapping of the Mach/Asm call stack as a single
block.  IA32 is fixed, PowerPC and ARM remains to be done.


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

3 files changed, 522 insertions, 574 deletions

diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 06b5407..324e1f7 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -139,6 +139,7 @@ Qed.
 
 Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree {
   agree_sp: rs#SP = sp;
+  agree_sp_def: sp <> Vundef;
   agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
 }.
 
@@ -185,7 +186,7 @@ Lemma agree_exten:
   (forall r, data_preg r = true -> rs'#r = rs#r) ->
   agree ms sp rs'.
 Proof.
-  intros. destruct H. split. 
+  intros. destruct H. split; auto.
   rewrite H0; auto. auto.
   intros. rewrite H0; auto. apply preg_of_data.
 Qed.
@@ -199,9 +200,8 @@ Lemma agree_set_mreg:
   (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
   agree (Regmap.set r v ms) sp rs'.
 Proof.
-  intros. destruct H. split.
+  intros. destruct H. split; auto.
   rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP.
-  auto.
   intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. 
   rewrite H1. auto. apply preg_of_data.
   red; intros; elim n. eapply preg_of_injective; eauto.
@@ -243,7 +243,7 @@ Lemma agree_exten_temps:
   (forall r, nontemp_preg r = true -> rs'#r = rs#r) ->
   agree (undef_temps ms) sp rs'.
 Proof.
-  intros. destruct H. split. 
+  intros. destruct H. split; auto.
   rewrite H0; auto. auto. 
   intros. unfold undef_temps. 
   destruct (In_dec mreg_eq r temporary_regs).
@@ -271,7 +271,7 @@ Lemma agree_change_sp:
   agree ms sp rs -> sp' <> Vundef ->
   agree ms sp' (rs#SP <- sp').
 Proof.
-  intros. inv H. split. apply Pregmap.gss. auto. 
+  intros. inv H. split; auto.
   intros. rewrite Pregmap.gso; auto with asmgen.
 Qed.
 
@@ -391,7 +391,16 @@ Proof.
   eauto.
 Qed.
 
-Remark code_tail_bounds:
+Remark code_tail_bounds_1:
+  forall fn ofs c,
+  code_tail ofs fn c -> 0 <= ofs <= list_length_z fn.
+Proof.
+  induction 1; intros; simpl.
+  generalize (list_length_z_pos c). omega. 
+  rewrite list_length_z_cons. omega.
+Qed.
+
+Remark code_tail_bounds_2:
   forall fn ofs i c,
   code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
 Proof.
@@ -425,23 +434,218 @@ 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. 
+  generalize (code_tail_bounds_2 _ _ _ _ H0). omega. 
 Qed.
 
-(** [transl_code_at_pc pc f c ep tf tc] holds if the code pointer [pc] points
+(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
   within the Asm code generated by translating Mach function [f],
   and [tc] is the tail of the generated code at the position corresponding
   to the code pointer [pc]. *)
 
 Inductive transl_code_at_pc (ge: Mach.genv):
-    val -> Mach.function -> Mach.code -> bool -> Asm.function -> Asm.code -> Prop :=
+    val -> block -> Mach.function -> Mach.code -> bool -> Asm.function -> 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 = Errors.OK tf ->
     transl_code f c ep = OK tc ->
     code_tail (Int.unsigned ofs) (fn_code tf) tc ->
-    transl_code_at_pc ge (Vptr b ofs) f c ep tf tc.
+    transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc.
+
+(** Predictor for return addresses in generated Asm code.
+
+  The [return_address_offset] predicate defined here is used in the
+  semantics for Mach to determine the return addresses that are
+  stored in activation records. *)
+
+(** Consider a Mach function [f] and a sequence [c] of Mach instructions
+  representing the Mach code that remains to be executed after a
+  function call returns.  The predicate [return_address_offset f c ofs]
+  holds if [ofs] is the integer offset of the PPC instruction
+  following the call in the Asm code obtained by translating the
+  code of [f]. Graphically:
+<<
+     Mach function f    |--------- Mcall ---------|
+         Mach code c    |                |--------|
+                        |                 \        \
+                        |                  \        \
+                        |                   \        \
+     Asm code           |                    |--------|
+     Asm function       |------------- Pcall ---------|
+
+                        <-------- ofs ------->
+>>
+*)
+
+Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: int) : Prop :=
+  forall tf tc,
+  transf_function f = OK tf ->
+  transl_code f c false = OK tc ->
+  code_tail (Int.unsigned ofs) (fn_code tf) tc.
+
+(** We now show that such an offset always exists if the Mach code [c]
+  is a suffix of [f.(fn_code)].  This holds because the translation
+  from Mach to PPC is compositional: each Mach instruction becomes
+  zero, one or several PPC instructions, but the order of instructions
+  is preserved. *)
+
+Lemma is_tail_code_tail:
+  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
+Proof.
+  induction 1. exists 0; constructor.
+  destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto.
+Qed.
+
+Section RETADDR_EXISTS.
+
+Hypothesis transl_instr_tail:
+  forall f i ep k c, transl_instr f i ep k = OK c -> is_tail k c.
+Hypothesis transf_function_inv:
+  forall f tf, transf_function f = OK tf ->
+  exists tc, exists ep, transl_code f (Mach.fn_code f) ep = OK tc /\ is_tail tc (fn_code tf).
+Hypothesis transf_function_len:
+  forall f tf, transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned.
+
+Lemma transl_code_tail: 
+  forall f c1 c2, is_tail c1 c2 ->
+  forall tc2 ep2, transl_code f c2 ep2 = OK tc2 ->
+  exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2.
+Proof.
+  induction 1; simpl; intros.
+  exists tc2; exists ep2; split; auto with coqlib.
+  monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]].
+  exists tc1; exists ep1; split. auto. 
+  apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto.
+Qed.
+
+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. destruct (transf_function f) as [tf|] eqn:TF.
++ exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1).
+  exploit transl_code_tail; eauto. intros (tc2 & ep2 & TR2 & TL2).
+Opaque transl_instr.
+  monadInv TR2. 
+  assert (TL3: is_tail x (fn_code tf)).
+  { apply is_tail_trans with tc1; auto. 
+    apply is_tail_trans with tc2; auto.
+    eapply transl_instr_tail; eauto. }
+  exploit is_tail_code_tail. eexact TL3. intros [ofs CT].
+  exists (Int.repr ofs). red; intros. 
+  rewrite Int.unsigned_repr. congruence. 
+  exploit code_tail_bounds_1; eauto.
+  apply transf_function_len in TF. omega. 
++ exists Int.zero; red; intros. congruence. 
+Qed.
+
+End RETADDR_EXISTS.
+
+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 ge b ofs fb f c tf tc ofs',
+  transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc ->
+  return_address_offset f c ofs' ->
+  ofs' = ofs.
+Proof.
+  intros. inv H. red in H0.  
+  exploit code_tail_unique. eexact H12. eapply H0; eauto. intro.
+  rewrite <- (Int.repr_unsigned ofs). 
+  rewrite <- (Int.repr_unsigned ofs').
+  congruence.
+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.
+
+(** Helper lemmas to reason about 
+- the "code is tail of" property
+- correct translation of labels. *)
+
+Definition tail_nolabel (k c: code) : Prop := is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k.
+
+Lemma tail_nolabel_refl:
+  forall c, tail_nolabel c c.
+Proof.
+  intros; split. apply is_tail_refl. auto.
+Qed.
+
+Lemma tail_nolabel_trans:
+  forall c1 c2 c3, tail_nolabel c1 c2 -> tail_nolabel c2 c3 -> tail_nolabel c1 c3.
+Proof.
+  intros. destruct H; destruct H0; split. 
+  eapply is_tail_trans; eauto.
+  intros. rewrite H2; auto.
+Qed.
+
+Lemma tail_nolabel_cons:
+  forall i c k,
+  match i with Plabel _ => False | _ => True end ->
+  tail_nolabel k c -> tail_nolabel k (i :: c).
+Proof.
+  intros. destruct H0. split. 
+  constructor; auto.
+  intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
+Qed.
+
+Hint Resolve tail_nolabel_refl: labels.
+
+Ltac TailNoLabels :=
+  eauto with labels;
+  match goal with
+  | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [exact I | TailNoLabels]
+  | [ H: Error _ = OK _ |- _ ] => discriminate
+  | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabels
+  | [ H: bind _ _ = OK _ |- _ ] => monadInv H;  TailNoLabels
+  | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabels
+  | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabels
+  | _ => idtac
+  end.
 
 (** * Execution of straight-line code *)
 
@@ -558,287 +762,41 @@ Qed.
 
 End STRAIGHTLINE.
 
-(** * Stack invariants *)
-
-(** ** Stored return addresses *)
-
-(** [retaddr_stored_at m m' sp pos ra] holds if Asm memory [m']
-  contains value [ra] (a return address) at offset [pos] in block [sp]. *)
-
-Record retaddr_stored_at (m m': mem) (sp: block) (pos: Z) (ra: val) : Prop := {
-  rsa_noperm:
-    forall ofs k p, pos <= ofs < pos + 4 -> ~Mem.perm m sp ofs k p;
-  rsa_allperm:
-    forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p;
-  rsa_contains:
-    Mem.load Mint32 m' sp pos = Some ra
-}.
-
-Lemma retaddr_stored_at_invariant:
-  forall m m' sp pos ra m1 m1',
-  retaddr_stored_at m m' sp pos ra ->
-  (forall ofs p, pos <= ofs < pos + 4 -> Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) ->
-  (forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p -> Mem.perm m1' sp ofs k p) ->
-  (Mem.load Mint32 m' sp pos = Some ra -> Mem.load Mint32 m1' sp pos = Some ra) ->
-  retaddr_stored_at m1 m1' sp pos ra.
-Proof.
-  intros. inv H. constructor; intros.
-  red; intros. eelim rsa_noperm0. eauto. apply H0. auto. eapply Mem.perm_max; eauto.  
-  eauto.
-  eauto.
-Qed.
-
-Lemma retaddr_stored_at_store:
-  forall chunk m m' b ofs v v' m1 m1' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.store chunk m b ofs v = Some m1 ->
-  Mem.store chunk m' b ofs v' = Some m1' ->
-  retaddr_stored_at m1 m1' sp pos ra.
-Proof.
-  intros. eapply retaddr_stored_at_invariant; eauto; intros.
-- eapply Mem.perm_store_2; eauto.
-- eapply Mem.perm_store_1; eauto.
-- rewrite <- H2. eapply Mem.load_store_other; eauto.
-  destruct (eq_block sp b); auto. subst b.
-  right. exploit Mem.store_valid_access_3. eexact H0. intros [A B].
-  apply (Intv.range_disjoint' (pos, pos + size_chunk Mint32) (ofs, ofs + size_chunk chunk)).
-  red; intros; red; intros. 
-  elim (rsa_noperm _ _ _ _ _ H x Cur Writable). assumption. apply A. assumption.
-  simpl; omega.
-  simpl; generalize (size_chunk_pos chunk); omega.
-Qed.
-
-Lemma retaddr_stored_at_storev:
-  forall chunk m m' a a' v v' m1 m1' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.storev chunk m a v = Some m1 ->
-  Mem.storev chunk m' a' v' = Some m1' ->
-  Val.lessdef a a' ->
-  retaddr_stored_at m1 m1' sp pos ra.
-Proof.
-  intros. destruct a; simpl in H0; try discriminate. inv H2. simpl in H1.
-  eapply retaddr_stored_at_store; eauto.
-Qed.
-
-Lemma retaddr_stored_at_valid':
-  forall m m' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.valid_block m' sp.
-Proof.
-  intros.
-  eapply Mem.valid_access_valid_block. 
-  apply Mem.valid_access_implies with Readable; auto with mem.
-  eapply Mem.load_valid_access.
-  eapply rsa_contains; eauto.
-Qed.
-
-Lemma retaddr_stored_at_valid:
-  forall m m' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.extends m m' ->
-  Mem.valid_block m sp.
-Proof.
-  intros.
-  erewrite Mem.valid_block_extends; eauto.
-  eapply retaddr_stored_at_valid'; eauto.
-Qed.
-
-Lemma retaddr_stored_at_extcall:
-  forall m1 m1' sp pos ra m2 m2',
-  retaddr_stored_at m1 m1' sp pos ra ->
-  (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  mem_unchanged_on (loc_out_of_bounds m1) m1' m2' ->
-  Mem.extends m1 m1' ->
-  retaddr_stored_at m2 m2' sp pos ra.
-Proof.
-  intros.
-  assert (B: forall ofs, pos <= ofs < pos + 4 -> loc_out_of_bounds m1 sp ofs).
-    intros; red; intros. eapply rsa_noperm; eauto.
-  eapply retaddr_stored_at_invariant; eauto. 
-- intros. apply H0; auto. eapply retaddr_stored_at_valid; eauto. 
-- intros. destruct H1. eauto. 
-- intros. destruct H1. apply H4; auto. 
-Qed.
-
-Lemma retaddr_stored_at_can_alloc:
-  forall m lo hi m1 sp pos m2 a v m3 m' m1' a' v' m2' ra,
-  Mem.alloc m lo hi = (m1, sp) ->
-  Mem.free m1 sp pos (pos + 4) = Some m2 ->
-  Mem.storev Mint32 m2 a v = Some m3 ->
-  Mem.alloc m' lo hi = (m1', sp) ->
-  Mem.storev Mint32 m1' a' v' = Some m2' ->
-  (4 | pos) ->
-  Mem.extends m3 m2' ->
-  Val.has_type ra Tint ->
-  exists m3',
-     Mem.store Mint32 m2' sp pos ra = Some m3'
-  /\ retaddr_stored_at m3 m3' sp pos ra
-  /\ Mem.extends m3 m3'.
-Proof.
-  intros. destruct a; simpl in H1; try discriminate. destruct a'; simpl in H3; try discriminate.
-  assert (POS: forall ofs, pos <= ofs < pos + 4 -> lo <= ofs < hi).
-    intros. eapply Mem.perm_alloc_3. eexact H. eapply Mem.free_range_perm; eauto.
-  assert (ST: { m3' | Mem.store Mint32 m2' sp pos ra = Some m3' }).
-  {
-    apply Mem.valid_access_store. split.
-    red; intros. eapply Mem.perm_store_1; eauto.
-    apply Mem.perm_implies with Freeable; auto with mem.
-    eapply Mem.perm_alloc_2; eauto.
-    assumption.
-  }
-  destruct ST as [m3' ST]. exists m3'; split; auto.
-  split. constructor.
-  intros; red; intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto.
-  intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. 
-  apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.perm_alloc_2; eauto.
-  replace ra with (Val.load_result Mint32 ra). eapply Mem.load_store_same; eauto.
-  destruct ra; reflexivity || contradiction.
-  eapply Mem.store_outside_extends; eauto. 
-  intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto.  
-Qed.
-
-Lemma retaddr_stored_at_can_free:
-  forall m m' sp pos ra lo m1 hi m2,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.free m sp lo pos = Some m1 ->
-  Mem.free m1 sp (pos + 4) hi = Some m2 ->
-  Mem.extends m m' ->
-  exists m1', Mem.free m' sp lo hi = Some m1' /\ Mem.extends m2 m1'.
-Proof.
-  intros. inv H.
-  assert (F: { m1' | Mem.free m' sp lo hi = Some m1' }).
-  {
-    apply Mem.range_perm_free. red; intros. 
-    assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega.
-    destruct EITHER as [A | [A | A]].
-    eapply Mem.perm_extends; eauto. eapply Mem.free_range_perm; eauto.
-    auto.
-    eapply Mem.perm_extends; eauto.
-    eapply Mem.perm_free_3; eauto. eapply Mem.free_range_perm; eauto.
-  }
-  destruct F as [m1' F]. exists m1'; split; auto.
-  eapply Mem.free_right_extends; eauto.
-  eapply Mem.free_left_extends. eapply Mem.free_left_extends. eauto. eauto. eauto. 
-  intros. 
-  exploit Mem.perm_free_3. eexact H1. eauto. intros P1.
-  exploit Mem.perm_free_3. eexact H0. eauto. intros P0.
-  assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega.
-  destruct EITHER as [A | [A | A]].
-  eelim Mem.perm_free_2. eexact H0. eexact A. eauto. 
-  eelim rsa_noperm0; eauto.
-  eelim Mem.perm_free_2. eexact H1. eexact A. eauto. 
-Qed.
-
-Lemma retaddr_stored_at_type:
-  forall m m' sp pos ra, retaddr_stored_at m m' sp pos ra -> Val.has_type ra Tint.
-Proof.
-  intros. change Tint with (type_of_chunk Mint32). 
-  eapply Mem.load_type. eapply rsa_contains; eauto.
-Qed.
-
-(** Matching a Mach stack against an Asm memory state. *)
+(** * Properties of the Mach call stack *)
 
 Section MATCH_STACK.
 
 Variable ge: Mach.genv.
 
-Inductive match_stack:
-           list Mach.stackframe -> mem -> mem -> val -> block -> Prop :=
-  | match_stack_nil: forall m m' bound,
-      match_stack nil m m' Vzero bound
-  | match_stack_cons: forall f sp c s m m' ra tf tc ra' bound
-      (AT: transl_code_at_pc ge ra f c false tf tc)
-      (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra')
-      (BELOW: sp < bound),
-      match_stack s m m' ra' sp ->
-      match_stack (Stackframe f (Vptr sp Int.zero) c :: s) m m' ra bound.
+Inductive match_stack: list Mach.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 ge ra fb f c false tf tc ->
+      sp <> Vundef ->
+      match_stack s ->
+      match_stack (Stackframe fb sp ra c :: s).
 
-Lemma match_stack_invariant:
-  forall m2 m2' s m1 m1' ra bound,
-  match_stack s m1 m1' ra bound ->
-  (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  (forall b ofs k p, b < bound -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) ->
-  (forall b ofs v, b < bound -> Mem.load Mint32 m1' b ofs = Some v -> Mem.load Mint32 m2' b ofs = Some v) ->
-  match_stack s m2 m2' ra bound.
-Proof.
-  induction 1; intros; econstructor; eauto.
-  eapply retaddr_stored_at_invariant; eauto.
-  apply IHmatch_stack; intros. 
-  eapply H0; eauto. omega.
-  eapply H1; eauto. omega.
-  eapply H2; eauto. omega.
-Qed.
+Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
+Proof. induction 1; simpl. congruence. auto. Qed.
 
-Lemma match_stack_change_bound:
-  forall s m m' ra bound1 bound2,
-  match_stack s m m' ra bound1 ->
-  bound1 <= bound2 ->
-  match_stack s m m' ra bound2.
-Proof.
-  intros. inv H; econstructor; eauto. omega. 
-Qed.
+Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
+Proof. induction 1; simpl. unfold Vzero. congruence. inv H0. congruence. Qed.
 
-Lemma match_stack_storev:
-  forall chunk a v m1 a' v' m1' s m m' ra bound,
-  match_stack s m m' ra bound ->
-  Mem.storev chunk m a v = Some m1 ->
-  Mem.storev chunk m' a' v' = Some m1' ->
-  Val.lessdef a a' ->
-  match_stack s m1 m1' ra bound.
-Proof.
-  induction 1; intros; econstructor; eauto. 
-  eapply retaddr_stored_at_storev; eauto.
-Qed.
-
-Lemma match_stack_extcall:
-  forall m2 m2' s m1 m1' ra bound,
-  match_stack s m1 m1' ra bound ->
-  (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  mem_unchanged_on (loc_out_of_bounds m1) m1' m2' ->
-  Mem.extends m1 m1' ->
-  match_stack s m2 m2' ra bound.
-Proof.
-  induction 1; intros; econstructor; eauto.
-  eapply retaddr_stored_at_extcall; eauto. 
-Qed.
-
-Lemma match_stack_free_left:
-  forall s m m' ra bound b lo hi m1,
-  match_stack s m m' ra bound ->
-  Mem.free m b lo hi = Some m1 ->
-  match_stack s m1 m' ra bound.
-Proof.
-  intros. eapply match_stack_invariant; eauto.
-  intros. eapply Mem.perm_free_3; eauto. 
-Qed.
-
-Lemma match_stack_free_right:
-  forall s m m' ra bound b lo hi m1',
-  match_stack s m m' ra bound ->
-  Mem.free m' b lo hi = Some m1' ->
-  bound <= b ->
-  match_stack s m m1' ra bound.
-Proof.
-  intros. eapply match_stack_invariant; eauto.
-  intros. eapply Mem.perm_free_1; eauto. left. unfold block; omega. 
-  intros. rewrite <- H3. eapply Mem.load_free; eauto. left. unfold block; omega.
-Qed.
-
-Lemma parent_sp_def:
-  forall s m m' ra bound,
-  match_stack s m m' ra bound -> parent_sp s <> Vundef.
+Lemma lessdef_parent_sp:
+  forall s v,
+  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
 Proof.
-  intros. inv H; simpl; congruence.
+  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
 Qed.
 
-Lemma lessdef_parent_sp:
-  forall s m m' ra bound v,
-  match_stack s m m' ra bound -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
+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. exfalso. eelim parent_sp_def; eauto.
+  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
 Qed.
 
 End MATCH_STACK.
 
-
diff --git a/backend/Mach.v b/backend/Mach.v
index 12c6c9d..0728c4d 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -115,7 +115,13 @@ semantics also make provisions for storing a back link at offset
 offset [f.(fn_retaddr_ofs)].  The latter stack location will be used
 by the Asm code generated by [Asmgen] to save the return address into
 the caller at the beginning of a function, then restore it and jump to
-it at the end of a function. *)
+it at the end of a function.  The Mach concrete semantics does not
+attach any particular meaning to the pointer stored in this reserved
+location, but makes sure that it is preserved during execution of a
+function.  The [return_address_offset] parameter is used to guess the
+value of the return address that the Asm code generated later will
+store in the reserved location.
+*)
 
 Definition chunk_of_type (ty: typ) :=
   match ty with Tint => Mint32 | Tfloat => Mfloat64al32 end.
@@ -202,16 +208,20 @@ Qed.
 
 Section RELSEM.
 
+Variable return_address_offset: function -> code -> int -> Prop.
+
 Variable ge: genv.
 
-Definition find_function (ros: mreg + ident) (rs: regset) : option fundef :=
+Definition find_function_ptr
+        (ge: genv) (ros: mreg + ident) (rs: regset) : option block :=
   match ros with
-  | inl r => Genv.find_funct ge (rs r)
-  | inr symb =>
-      match Genv.find_symbol ge symb with
-      | None => None
-      | Some b => Genv.find_funct_ptr ge b
+  | inl r =>
+      match rs r with
+      | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None
+      | _ => None
       end
+  | inr symb =>
+      Genv.find_symbol ge symb
   end.
 
 (** Extract the values of the arguments to an external call. *)
@@ -242,17 +252,20 @@ Definition annot_arguments
 
 (** Mach execution states. *)
 
+(** Mach execution states. *)
+
 Inductive stackframe: Type :=
   | Stackframe:
-      forall (f: function)    (**r calling function *)
+      forall (f: block)       (**r pointer to calling function *)
              (sp: val)        (**r stack pointer in calling function *)
+             (retaddr: val)   (**r Asm return address in calling function *)
              (c: code),       (**r program point in calling function *)
       stackframe.
 
 Inductive state: Type :=
   | State:
       forall (stack: list stackframe)  (**r call stack *)
-             (f: function)             (**r current function *)
+             (f: block)                (**r pointer to current function *)
              (sp: val)                 (**r stack pointer *)
              (c: code)                 (**r current program point *)
              (rs: regset)              (**r register state *)
@@ -260,7 +273,7 @@ Inductive state: Type :=
       state
   | Callstate:
       forall (stack: list stackframe)  (**r call stack *)
-             (fd: fundef)              (**r function to call *)
+             (f: block)                (**r pointer to function to call *)
              (rs: regset)              (**r register state *)
              (m: mem),                 (**r memory state *)
       state
@@ -273,7 +286,13 @@ Inductive state: Type :=
 Definition parent_sp (s: list stackframe) : val :=
   match s with
   | nil => Vptr Mem.nullptr Int.zero
-  | Stackframe f sp c :: s' => sp
+  | Stackframe f sp ra c :: s' => sp
+  end.
+
+Definition parent_ra (s: list stackframe) : val :=
+  match s with
+  | nil => Vzero
+  | Stackframe f sp ra c :: s' => ra
   end.
 
 Inductive step: state -> trace -> state -> Prop :=
@@ -292,11 +311,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Msetstack src ofs ty :: c) rs m)
         E0 (State s f sp c (undef_setstack rs) m')
   | exec_Mgetparam:
-      forall s f sp ofs ty dst c rs m v,
+      forall s fb f sp ofs ty dst c rs m v,
+      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 ->
-      step (State s f sp (Mgetparam ofs ty dst :: c) rs m)
-        E0 (State s f sp c (rs # IT1 <- Vundef # dst <- v) m)
+      step (State s fb sp (Mgetparam ofs ty dst :: c) rs m)
+        E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m)
   | exec_Mop:
       forall s f sp op args res c rs m v,
       eval_operation ge sp op rs##args m = Some v ->
@@ -315,19 +335,22 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mstore chunk addr args src :: c) rs m)
         E0 (State s f sp c (undef_temps rs) m')
   | exec_Mcall:
-      forall s f sp sig ros c rs m fd,
-      find_function ros rs = Some fd ->
-      step (State s f sp (Mcall sig ros :: c) rs m)
-        E0 (Callstate (Stackframe f sp c :: s)
-                       fd rs m)
+      forall s fb sp sig ros c rs m f f' ra,
+      find_function_ptr ge ros rs = Some f' ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      return_address_offset f c ra ->
+      step (State s fb sp (Mcall sig ros :: c) rs m)
+        E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s)
+                       f' rs m)
   | exec_Mtailcall:
-      forall s f stk soff sig ros c rs m fd m' m'',
-      find_function ros rs = Some fd ->
+      forall s fb stk soff sig ros c rs m f f' m',
+      find_function_ptr ge ros rs = 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) ->
-      Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' ->
-      Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' ->
-      step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
-        E0 (Callstate s fd rs m'')
+      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' ->
+      step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
+        E0 (Callstate s f' rs m')
   | exec_Mbuiltin:
       forall s f sp rs m ef args res b t v m',
       external_call ef ge rs##args m t v m' ->
@@ -340,70 +363,74 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mannot ef args :: b) rs m)
          t (State s f sp b rs m')
   | exec_Mgoto:
-      forall s f sp lbl c rs m c',
+      forall s fb f sp lbl c rs m c',
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mgoto lbl :: c) rs m)
-        E0 (State s f sp c' rs m)
+      step (State s fb sp (Mgoto lbl :: c) rs m)
+        E0 (State s fb sp c' rs m)
   | exec_Mcond_true:
-      forall s f sp cond args lbl c rs m c',
+      forall s fb f sp cond args lbl c rs m c',
       eval_condition cond rs##args m = Some true ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mcond cond args lbl :: c) rs m)
-        E0 (State s f sp c' (undef_temps rs) m)
+      step (State s fb sp (Mcond cond args lbl :: c) rs m)
+        E0 (State s fb sp c' (undef_temps rs) m)
   | exec_Mcond_false:
       forall s f sp cond args lbl c rs m,
       eval_condition cond rs##args m = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs m)
         E0 (State s f sp c (undef_temps rs) m)
   | exec_Mjumptable:
-      forall s f sp arg tbl c rs m n lbl c',
+      forall s fb f sp arg tbl c rs m n lbl c',
       rs arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some lbl ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       find_label lbl f.(fn_code) = Some c' ->
-      step (State s f sp (Mjumptable arg tbl :: c) rs m)
-        E0 (State s f sp c' (undef_temps rs) m)
+      step (State s fb sp (Mjumptable arg tbl :: c) rs m)
+        E0 (State s fb sp c' (undef_temps rs) m)
   | exec_Mreturn:
-      forall s f stk soff c rs m m' m'',
+      forall s fb stk soff c rs m f 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) ->
-      Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' ->
-      Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' ->
-      step (State s f (Vptr stk soff) (Mreturn :: c) rs m)
-        E0 (Returnstate s rs m'')
+      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' ->
+      step (State s fb (Vptr stk soff) (Mreturn :: c) rs m)
+        E0 (Returnstate s rs m')
   | exec_function_internal:
-      forall s f rs m m1 m2 m3 stk,
+      forall s fb rs m f m1 m2 m3 stk,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
       Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
-      Mem.free m1 stk (Int.unsigned f.(fn_retaddr_ofs)) (Int.unsigned f.(fn_retaddr_ofs) + 4) = Some m2 ->
       let sp := Vptr stk Int.zero in
-      store_stack m2 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m3 ->
-      (4 | Int.unsigned f.(fn_retaddr_ofs)) ->
-      step (Callstate s (Internal f) rs m)
-        E0 (State s f sp f.(fn_code) (undef_temps rs) m3)
+      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 ->
+      step (Callstate s fb rs m)
+        E0 (State s fb sp f.(fn_code) (undef_temps rs) m3)
   | exec_function_external:
-      forall s ef rs m t rs' args res m',
+      forall s fb rs m t rs' ef args res m',
+      Genv.find_funct_ptr ge fb = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
       rs' = (rs#(loc_result (ef_sig ef)) <- res) ->
-      step (Callstate s (External ef) rs m)
+      step (Callstate s fb rs m)
          t (Returnstate s rs' m')
   | exec_return:
-      forall s f sp c rs m,
-      step (Returnstate (Stackframe f sp c :: s) rs m)
+      forall s f sp ra c rs m,
+      step (Returnstate (Stackframe f sp ra c :: s) rs m)
         E0 (State s f sp c rs m).
 
 End RELSEM.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b fd m0,
+  | initial_state_intro: forall fb m0,
       let ge := Genv.globalenv p in
       Genv.init_mem p = Some m0 ->
-      Genv.find_symbol ge p.(prog_main) = Some b ->
-      Genv.find_funct_ptr ge b = Some fd ->
-      initial_state p (Callstate nil fd (Regmap.init Vundef) m0).
+      Genv.find_symbol ge p.(prog_main) = Some fb ->
+      initial_state p (Callstate nil fb (Regmap.init Vundef) m0).
 
 Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall rs m r,
       rs (loc_result (mksignature nil (Some Tint))) = Vint r ->
       final_state (Returnstate nil rs m) r.
 
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+Definition semantics (rao: function -> code -> int -> Prop) (p: program) :=
+  Semantics (step rao) (initial_state p) final_state (Genv.globalenv p).
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index cd01beb..4ce8c25 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -50,6 +50,15 @@ Qed.
 
 Section PRESERVATION.
 
+Variable return_address_offset: Mach.function -> Mach.code -> int -> Prop.
+
+Hypothesis return_address_offset_exists:
+  forall f sg ros c,
+  is_tail (Mcall sg ros :: c) (fn_code f) ->
+  exists ofs, return_address_offset f c ofs.
+
+Let step := Mach.step return_address_offset.
+
 Variable prog: Linear.program.
 Variable tprog: Mach.program.
 Hypothesis TRANSF: transf_program prog = OK tprog.
@@ -421,31 +430,23 @@ Definition frame_perm_freeable (m: mem) (sp: block): Prop :=
   forall ofs,
   0 <= ofs < fe.(fe_size) ->
   ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
-  ofs < fe.(fe_ofs_retaddr) \/ fe.(fe_ofs_retaddr) + 4 <= ofs ->
   Mem.perm m sp ofs Cur Freeable.
 
 Lemma offset_of_index_perm:
   forall m sp idx,
-  index_valid idx -> idx <> FI_retaddr ->
+  index_valid idx ->
   frame_perm_freeable m sp ->
   Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Cur Freeable.
 Proof.
   intros.
   exploit offset_of_index_valid; eauto. intros [A B].
-  exploit offset_of_index_disj.
-    instantiate (1 := FI_retaddr); exact I.
-    eexact H.
-    red. destruct idx; auto || congruence.
-  change (AST.typesize (type_of_index FI_retaddr)) with 4.
-  change (offset_of_index fe FI_retaddr) with fe.(fe_ofs_retaddr).
-  intros C.
-  exploit offset_of_index_disj_stack_data_2; eauto. intros D.
-  red; intros. apply H1. omega. omega. omega.
+  exploit offset_of_index_disj_stack_data_2; eauto. intros.
+  red; intros. apply H0. omega. omega.
 Qed.
 
 Lemma store_index_succeeds:
   forall m sp idx v,
-  index_valid idx -> idx <> FI_retaddr ->
+  index_valid idx ->
   frame_perm_freeable m sp ->
   exists m',
   Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m'.
@@ -527,7 +528,7 @@ Qed.
 
 Lemma index_contains_inj_undef:
   forall j m sp idx,
-  index_valid idx -> idx <> FI_retaddr ->
+  index_valid idx ->
   frame_perm_freeable m sp ->
   index_contains_inj j m sp idx Vundef.
 Proof.
@@ -557,7 +558,7 @@ Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop :=
 Record agree_frame (j: meminj) (ls ls0: locset)
                    (m: mem) (sp: block)
                    (m': mem) (sp': block)
-                   (parent: val) : Prop :=
+                   (parent retaddr: val) : Prop :=
   mk_agree_frame {
 
     (** Unused registers have the same value as in the caller *)
@@ -583,9 +584,12 @@ Record agree_frame (j: meminj) (ls ls0: locset)
        In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) ->
        ls (S (Incoming ofs ty)) = ls0 (S (Outgoing ofs ty));
 
-    (** The back link contains the [parent] value. *)
+    (** The back link and return address slots of the Mach frame contain
+        the [parent] and [retaddr] values, respectively. *)
     agree_link:
       index_contains m' sp' FI_link parent;
+    agree_retaddr:
+      index_contains m' sp' FI_retaddr retaddr;
 
     (** The areas of the frame reserved for saving used callee-save
         registers always contain the values that those registers had
@@ -627,7 +631,7 @@ Record agree_frame (j: meminj) (ls ls0: locset)
   }.
 
 Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming
-             agree_link agree_saved_int agree_saved_float
+             agree_link agree_retaddr agree_saved_int agree_saved_float
              agree_valid_linear agree_valid_mach agree_perm
              agree_wt_ls: stacking.
 
@@ -767,11 +771,11 @@ Qed.
 (** Preservation under assignment of machine register. *)
 
 Lemma agree_frame_set_reg:
-  forall j ls ls0 m sp m' sp' parent r v,
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent ra r v,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
   mreg_within_bounds b r ->
    Val.has_type v (Loc.type (R r)) ->
-  agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent.
+  agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. inv H; constructor; auto; intros.
   rewrite Locmap.gso. auto. red. intuition congruence.
@@ -798,10 +802,10 @@ Proof.
 Qed.
 
 Lemma agree_frame_undef_locs:
-  forall j ls0 m sp m' sp' parent regs ls,
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls0 m sp m' sp' parent ra regs ls,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
   incl (List.map R regs) temporaries ->
-  agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent.
+  agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra.
 Proof.
   induction regs; simpl; intros.
   auto.
@@ -812,17 +816,17 @@ Proof.
 Qed.
 
 Lemma agree_frame_undef_temps:
-  forall j ls ls0 m sp m' sp' parent,
-  agree_frame j ls ls0 m sp m' sp' parent ->
-  agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent.
+  forall j ls ls0 m sp m' sp' parent ra,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. unfold temporaries. apply agree_frame_undef_locs; auto. apply incl_refl. 
 Qed.
 
 Lemma agree_frame_undef_setstack:
-  forall j ls ls0 m sp m' sp' parent,
-  agree_frame j ls ls0 m sp m' sp' parent ->
-  agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent.
+  forall j ls ls0 m sp m' sp' parent ra,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. unfold Linear.undef_setstack, destroyed_at_move. 
   apply agree_frame_undef_locs; auto.
@@ -830,9 +834,9 @@ Proof.
 Qed.
 
 Lemma agree_frame_undef_op:
-  forall j ls ls0 m sp m' sp' parent op,
-  agree_frame j ls ls0 m sp m' sp' parent ->
-  agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent.
+  forall j ls ls0 m sp m' sp' parent ra op,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. 
   exploit agree_frame_undef_temps; eauto.
@@ -842,13 +846,13 @@ Qed.
 (** Preservation by assignment to local slot *)
 
 Lemma agree_frame_set_local:
-  forall j ls ls0 m sp m' sp' parent ofs ty v v' m'',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds f b (Local ofs ty) ->
   val_inject j v v' ->
   Val.has_type v ty ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' ->
-  agree_frame j (Locmap.set (S (Local ofs ty)) v ls) ls0 m sp m'' sp' parent.
+  agree_frame j (Locmap.set (S (Local ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
   intros. inv H. 
   change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3.
@@ -867,6 +871,8 @@ Proof.
   rewrite Locmap.gso; auto. red; auto.
 (* parent *)
   eapply gso_index_contains; eauto. red; auto.
+(* retaddr *)
+  eapply gso_index_contains; eauto. red; auto.
 (* int callee save *)
   eapply gso_index_contains_inj; eauto. simpl; auto. 
 (* float callee save *)
@@ -882,13 +888,13 @@ Qed.
 (** Preservation by assignment to outgoing slot *)
 
 Lemma agree_frame_set_outgoing:
-  forall j ls ls0 m sp m' sp' parent ofs ty v v' m'',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   slot_within_bounds f b (Outgoing ofs ty) ->
   val_inject j v v' ->
   Val.has_type v ty ->
   Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' ->
-  agree_frame j (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 m sp m'' sp' parent.
+  agree_frame j (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr.
 Proof.
   intros. inv H. 
   change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3.
@@ -901,7 +907,7 @@ Proof.
   unfold Locmap.set. simpl. destruct (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))).
   inv e. eapply gss_index_contains_inj; eauto.
   case_eq (Loc.overlap_aux ty ofs ofs0 || Loc.overlap_aux ty0 ofs0 ofs); intros.
-  apply index_contains_inj_undef. auto. congruence.
+  apply index_contains_inj_undef. auto.
   red; intros. eapply Mem.perm_store_1; eauto.
   eapply gso_index_contains_inj; eauto.
   red. eapply Loc.overlap_aux_false_1; eauto.
@@ -909,6 +915,8 @@ Proof.
   rewrite Locmap.gso; auto. red; auto.
 (* parent *)
   eapply gso_index_contains; eauto with stacking. red; auto.
+(* retaddr *)
+  eapply gso_index_contains; eauto with stacking. red; auto.
 (* int callee save *)
   eapply gso_index_contains_inj; eauto with stacking. simpl; auto. 
 (* float callee save *)
@@ -924,8 +932,8 @@ Qed.
 (** General invariance property with respect to memory changes. *)
 
 Lemma agree_frame_invariant:
-  forall j ls ls0 m sp m' sp' parent m1 m1',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr m1 m1',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   (Mem.valid_block m sp -> Mem.valid_block m1 sp) ->
   (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) ->
   (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') ->
@@ -937,7 +945,7 @@ Lemma agree_frame_invariant:
   (forall ofs k p,
      ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs ->
      Mem.perm m' sp' ofs k p -> Mem.perm m1' sp' ofs k p) ->
-  agree_frame j ls ls0 m1 sp m1' sp' parent.
+  agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
 Proof.
   intros.
   assert (IC: forall idx v,
@@ -956,13 +964,13 @@ Qed.
 (** A variant of the latter, for use with external calls *)
 
 Lemma agree_frame_extcall_invariant:
-  forall j ls ls0 m sp m' sp' parent m1 m1',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr m1 m1',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   (Mem.valid_block m sp -> Mem.valid_block m1 sp) ->
   (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) ->
   (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') ->
   mem_unchanged_on (loc_out_of_reach j m) m' m1' ->
-  agree_frame j ls ls0 m1 sp m1' sp' parent.
+  agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
 Proof.
   intros.
   assert (REACH: forall ofs,
@@ -978,13 +986,13 @@ Qed.
 (** Preservation by parallel stores in the Linear and Mach codes *)
 
 Lemma agree_frame_parallel_stores:
-  forall j ls ls0 m sp m' sp' parent chunk addr addr' v v' m1 m1',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr chunk addr addr' v v' m1 m1',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   Mem.inject j m m' ->
   val_inject j addr addr' ->
   Mem.storev chunk m addr v = Some m1 ->
   Mem.storev chunk m' addr' v' = Some m1' ->
-  agree_frame j ls ls0 m1 sp m1' sp' parent.
+  agree_frame j ls ls0 m1 sp m1' sp' parent retaddr.
 Proof.
 Opaque Int.add.
   intros until m1'. intros AG MINJ VINJ STORE1 STORE2.
@@ -1014,11 +1022,11 @@ Qed.
 (** Preservation by increasing memory injections (allocations and external calls) *)
 
 Lemma agree_frame_inject_incr:
-  forall j ls ls0 m sp m' sp' parent m1 m1' j',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr m1 m1' j',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   inject_incr j j' -> inject_separated j j' m1 m1' ->
   Mem.valid_block m1' sp' ->
-  agree_frame j' ls ls0 m sp m' sp' parent.
+  agree_frame j' ls ls0 m sp m' sp' parent retaddr.
 Proof.
   intros. inv H. constructor; auto; intros; eauto with stacking.
   case_eq (j b0). 
@@ -1054,11 +1062,11 @@ Proof.
 Qed.
 
 Lemma agree_frame_return:
-  forall j ls ls0 m sp m' sp' parent ls',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr ls',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   agree_callee_save ls' ls ->
   wt_locset ls' ->
-  agree_frame j ls' ls0 m sp m' sp' parent.
+  agree_frame j ls' ls0 m sp m' sp' parent retaddr.
 Proof.
   intros. red in H0. inv H; constructor; auto; intros.
   rewrite H0; auto. apply mreg_not_within_bounds_callee_save; auto. 
@@ -1070,10 +1078,10 @@ Qed.
 (** Preservation at tailcalls (when [ls0] is changed but not [ls]). *)
 
 Lemma agree_frame_tailcall:
-  forall j ls ls0 m sp m' sp' parent ls0',
-  agree_frame j ls ls0 m sp m' sp' parent ->
+  forall j ls ls0 m sp m' sp' parent retaddr ls0',
+  agree_frame j ls ls0 m sp m' sp' parent retaddr ->
   agree_callee_save ls0 ls0' ->
-  agree_frame j ls ls0' m sp m' sp' parent.
+  agree_frame j ls ls0' m sp m' sp' parent retaddr.
 Proof.
   intros. red in H0. inv H; constructor; auto; intros.
   rewrite <- H0; auto. apply mreg_not_within_bounds_callee_save; auto. 
@@ -1082,6 +1090,7 @@ Proof.
   rewrite <- H0; auto.
 Qed.
 
+
 (** Properties of [agree_callee_save]. *)
 
 Lemma agree_callee_save_return_regs:
@@ -1122,6 +1131,7 @@ Variable mkindex: Z -> frame_index.
 Variable ty: typ.
 Variable j: meminj.
 Variable cs: list stackframe.
+Variable fb: block.
 Variable sp: block.
 Variable csregs: list mreg.
 Variable ls: locset.
@@ -1154,8 +1164,6 @@ Hypothesis mkindex_inj:
 Hypothesis mkindex_diff:
   forall r idx,
   idx <> mkindex (number r) -> index_diff (mkindex (number r)) idx.
-Hypothesis mkindex_not_retaddr:
-  forall r, mkindex (number r) <> FI_retaddr.
 Hypothesis csregs_typ:
   forall r, In r csregs -> mreg_type r = ty.
 
@@ -1172,9 +1180,9 @@ Lemma save_callee_save_regs_correct:
   agree_regs j ls rs ->
   exists rs', exists m',
     star step tge 
-       (State cs tf (Vptr sp Int.zero)
+       (State cs fb (Vptr sp Int.zero)
          (save_callee_save_regs bound number mkindex ty fe l k) rs m)
-    E0 (State cs tf (Vptr sp Int.zero) k rs' m')
+    E0 (State cs fb (Vptr sp Int.zero) k rs' m')
   /\ (forall r,
        In r l -> number r < bound fe ->
        index_contains_inj j m' sp (mkindex (number r)) (ls (R r)))
@@ -1201,7 +1209,7 @@ Proof.
   unfold save_callee_save_reg.
   destruct (zlt (number a) (bound fe)).
   (* a store takes place *)
-  exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. auto. 
+  exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. 
   eauto. instantiate (1 := rs a). intros [m1 ST].
   exploit (IHl k (undef_setstack rs) m1).  auto with coqlib. auto. 
   red; eauto with mem.
@@ -1244,13 +1252,13 @@ Qed.
 End SAVE_CALLEE_SAVE.
 
 Lemma save_callee_save_correct:
-  forall j ls rs sp cs k m,
+  forall j ls rs sp cs fb k m,
   agree_regs j (call_regs ls) rs -> wt_locset (call_regs ls) ->
   frame_perm_freeable m sp ->
   exists rs', exists m',
     star step tge 
-       (State cs tf (Vptr sp Int.zero) (save_callee_save fe k) rs m)
-    E0 (State cs tf (Vptr sp Int.zero) k rs' m')
+       (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs m)
+    E0 (State cs fb (Vptr sp Int.zero) k rs' m')
   /\ (forall r,
        In r int_callee_save_regs -> index_int_callee_save r < b.(bound_int_callee_save) ->
        index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (call_regs ls (R r)))
@@ -1275,13 +1283,12 @@ Transparent destroyed_at_move_regs.
              fe_num_int_callee_save
              index_int_callee_save
              FI_saved_int Tint
-             j cs sp int_callee_save_regs (call_regs ls)).
+             j cs fb sp int_callee_save_regs (call_regs ls)).
   intros. apply index_int_callee_save_inj; auto. 
   intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption.
   auto.
   intros; congruence.
   intros; simpl. destruct idx; auto. congruence.
-  intros; congruence.
   intros. apply int_callee_save_type. auto.
   auto.
   auto.
@@ -1294,13 +1301,12 @@ Transparent destroyed_at_move_regs.
              fe_num_float_callee_save
              index_float_callee_save
              FI_saved_float Tfloat
-             j cs sp float_callee_save_regs (call_regs ls)).
+             j cs fb sp float_callee_save_regs (call_regs ls)).
   intros. apply index_float_callee_save_inj; auto. 
   intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption.
   simpl; auto.
   intros; congruence.
   intros; simpl. destruct idx; auto. congruence.
-  intros; congruence.
   intros. apply float_callee_save_type. auto.
   auto. 
   auto.
@@ -1371,28 +1377,28 @@ Qed.
   saving of the used callee-save registers). *)
 
 Lemma function_prologue_correct:
-  forall j ls ls0 rs m1 m1' m2 sp parent cs k,
+  forall j ls ls0 rs m1 m1' m2 sp parent ra cs fb k,
   agree_regs j ls rs ->
   agree_callee_save ls ls0 ->
   wt_locset ls ->
   Mem.inject j m1 m1' ->
   Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) ->
-  Val.has_type parent Tint ->
+  Val.has_type parent Tint -> Val.has_type ra Tint ->
   exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5',
      Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp')
-  /\ Mem.free m2' sp' (Int.unsigned tf.(fn_retaddr_ofs)) (Int.unsigned tf.(fn_retaddr_ofs) + 4) = Some m3'
-  /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m4'
+  /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3'
+  /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4'
   /\ star step tge 
-         (State cs tf (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4')
-      E0 (State cs tf (Vptr sp' Int.zero) k rs' m5')
+         (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4')
+      E0 (State cs fb (Vptr sp' Int.zero) k rs' m5')
   /\ agree_regs j' (call_regs ls) rs'
-  /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent
+  /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent ra
   /\ inject_incr j j'
   /\ inject_separated j j' m1 m1'
   /\ Mem.inject j' m2 m5'
-  /\ stores_in_frame sp' m3' m5'.
+  /\ stores_in_frame sp' m2' m5'.
 Proof.
-  intros until k; intros AGREGS AGCS WTREGS INJ1 ALLOC TYPAR.
+  intros until k; intros AGREGS AGCS WTREGS INJ1 ALLOC TYPAR TYRA.
   rewrite unfold_transf_function.
   unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs.
   (* Allocation step *)
@@ -1417,37 +1423,14 @@ Proof.
       assert (~Mem.valid_block m1' sp') by eauto with mem.
       contradiction.
   intros [j' [INJ2 [INCR [MAP1 MAP2]]]].
-  (* separation *)
-  assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe).
-    intros. destruct (zeq b0 sp). 
-    subst b0. rewrite MAP1 in H; inv H; auto.
-    rewrite MAP2 in H; auto. 
-    assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto.
-    assert (~Mem.valid_block m1' sp') by eauto with mem.
-    contradiction.
-  (* Freeing step *)
-  assert (OFSRA: Int.unsigned (Int.repr (fe_ofs_retaddr fe)) = fe_ofs_retaddr fe).
-    apply (offset_of_index_no_overflow FI_retaddr). exact I.
-  rewrite OFSRA.
-  assert (FREE: { m3' | Mem.free m2' sp' (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) = Some m3'}).
-    apply Mem.range_perm_free. 
-    exploit (offset_of_index_valid FI_retaddr). exact I.
-    unfold offset_of_index. simpl AST.typesize. intros [A B].
-    red; intros. eapply Mem.perm_alloc_2; eauto. omega. 
-  destruct FREE as [m3' FREE].
-  assert (INJ3: Mem.inject j' m2 m3').
-    eapply Mem.free_right_inject; eauto. 
-    intros. exploit SEP; eauto. intros [A B]. subst b1 delta. 
-    exploit (offset_of_index_disj_stack_data_1 FI_retaddr). exact I.
-    unfold offset_of_index. simpl AST.typesize. intros. 
-    exploit Mem.perm_alloc_3. eexact ALLOC. eauto. intros. 
-    generalize bound_stack_data_stacksize; intros.
-    omega. 
-  assert (PERM: frame_perm_freeable m3' sp').
-    red; intros. eapply Mem.perm_free_1; eauto. eapply Mem.perm_alloc_2; eauto.
+  assert (PERM: frame_perm_freeable m2' sp').
+    red; intros. eapply Mem.perm_alloc_2; eauto.
   (* Store of parent *)
-  exploit (store_index_succeeds m3' sp' FI_link parent). red; auto. congruence. auto. 
-  intros [m4' STORE].
+  exploit (store_index_succeeds m2' sp' FI_link parent). red; auto. auto. 
+  intros [m3' STORE2].
+  (* Store of retaddr *)
+  exploit (store_index_succeeds m3' sp' FI_retaddr ra). red; auto. red; eauto with mem.
+  intros [m4' STORE3].
   (* Saving callee-save registers *)
   assert (PERM4: frame_perm_freeable m4' sp').
     red; intros. eauto with mem. 
@@ -1457,21 +1440,32 @@ Proof.
     eexact PERM4.
   intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]].
   (* stores in frames *)
-  assert (SIF: stores_in_frame sp' m3' m5').
+  assert (SIF: stores_in_frame sp' m2' m5').
     econstructor; eauto. 
     rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto.
+    econstructor; eauto.
+    rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto.
+  (* separation *)
+  assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe).
+    intros. destruct (zeq b0 sp). 
+    subst b0. rewrite MAP1 in H; inv H; auto.
+    rewrite MAP2 in H; auto. 
+    assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto.
+    assert (~Mem.valid_block m1' sp') by eauto with mem.
+    contradiction.
   (* Conclusions *)
   exists j'; exists rs'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'.
-  (* alloc *)
-  split. auto.
-  (* free *)
   split. auto.
   (* store parent *)
   split. change Tint with (type_of_index FI_link). 
   change (fe_ofs_link fe) with (offset_of_index fe FI_link).
   apply store_stack_succeeds; auto. red; auto.
+  (* store retaddr *)
+  split. change Tint with (type_of_index FI_retaddr). 
+  change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr).
+  apply store_stack_succeeds; auto. red; auto.
   (* saving of registers *)
-  split. rewrite <- unfold_transf_function. eexact STEPS.
+  split. eexact STEPS.
   (* agree_regs *)
   split. auto.
   (* agree frame *)
@@ -1481,13 +1475,18 @@ Proof.
     elim H. apply temporary_within_bounds; auto.
     apply AGCS. apply mreg_not_within_bounds_callee_save; auto.
     (* locals *)
-    simpl. apply index_contains_inj_undef; auto. congruence.
+    simpl. apply index_contains_inj_undef; auto.
     (* outgoing *)
-    simpl. apply index_contains_inj_undef; auto. congruence.
+    simpl. apply index_contains_inj_undef; auto.
     (* incoming *)
     unfold call_regs. apply AGCS. auto.
     (* parent *)
     apply OTHERS; auto. red; auto.
+    eapply gso_index_contains; eauto. red; auto.
+    eapply gss_index_contains; eauto. red; auto.
+    red; auto.
+    (* retaddr *)
+    apply OTHERS; auto. red; auto.
     eapply gss_index_contains; eauto. red; auto.
     (* int callee save *)
     rewrite <- AGCS. replace (ls (R r)) with (call_regs ls (R r)).
@@ -1508,7 +1507,7 @@ Proof.
     (* valid sp *)
     eauto with mem.
     (* valid sp' *)
-    eapply stores_in_frame_valid with (m := m3'); eauto with mem.
+    eapply stores_in_frame_valid with (m := m2'); eauto with mem.
     (* bounds *)
     exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto.
     (* perms *)
@@ -1540,6 +1539,7 @@ Variable ty: typ.
 Variable csregs: list mreg.
 Variable j: meminj.
 Variable cs: list stackframe.
+Variable fb: block.
 Variable sp: block.
 Variable ls0: locset.
 Variable m: mem.
@@ -1566,9 +1566,9 @@ Lemma restore_callee_save_regs_correct:
   agree_unused ls0 rs ->
   exists rs',
     star step tge
-      (State cs tf (Vptr sp Int.zero)
+      (State cs fb (Vptr sp Int.zero)
         (restore_callee_save_regs bound number mkindex ty fe l k) rs m)
-   E0 (State cs tf (Vptr sp Int.zero) k rs' m)
+   E0 (State cs fb (Vptr sp Int.zero) k rs' m)
   /\ (forall r, In r l -> val_inject j (ls0 (R r)) (rs' r))
   /\ (forall r, ~(In r l) -> rs' r = rs r)
   /\ agree_unused ls0 rs'.
@@ -1613,13 +1613,13 @@ Qed.
 End RESTORE_CALLEE_SAVE.
 
 Lemma restore_callee_save_correct:
-  forall j ls ls0 m sp m' sp' pa cs rs k,
-  agree_frame j ls ls0 m sp m' sp' pa ->
+  forall j ls ls0 m sp m' sp' pa ra cs fb rs k,
+  agree_frame j ls ls0 m sp m' sp' pa ra ->
   agree_unused j ls0 rs ->
   exists rs',
     star step tge
-       (State cs tf (Vptr sp' Int.zero) (restore_callee_save fe k) rs m')
-    E0 (State cs tf (Vptr sp' Int.zero) k rs' m')
+       (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m')
+    E0 (State cs fb (Vptr sp' Int.zero) k rs' m')
   /\ (forall r, 
         In r int_callee_save_regs \/ In r float_callee_save_regs -> 
         val_inject j (ls0 (R r)) (rs' r))
@@ -1635,7 +1635,7 @@ Proof.
              FI_saved_int
              Tint
              int_callee_save_regs
-             j cs sp' ls0 m'); auto.
+             j cs fb sp' ls0 m'); auto.
   intros. unfold mreg_within_bounds. rewrite (int_callee_save_type r H1). tauto.
   eapply agree_saved_int; eauto. 
   apply incl_refl.
@@ -1648,7 +1648,7 @@ Proof.
              FI_saved_float
              Tfloat
              float_callee_save_regs
-             j cs sp' ls0 m'); auto.
+             j cs fb sp' ls0 m'); auto.
   intros. unfold mreg_within_bounds. rewrite (float_callee_save_type r H1). tauto.
   eapply agree_saved_float; eauto. 
   apply incl_refl.
@@ -1668,94 +1668,57 @@ Qed.
   registers + reloading of the link and return address + freeing
   of the frame). *)
 
-Remark mem_range_perm_free_twice:
-  forall m blk lo1 hi1 lo2 hi2,
-  (forall ofs, lo1 <= ofs < hi2 -> ofs < hi1 \/ lo2 <= ofs -> Mem.perm m blk ofs Cur Freeable) ->
-  lo1 <= hi1 /\ lo2 <= hi2 -> hi1 < lo2 ->
-  exists m', exists m'',
-  Mem.free m blk lo1 hi1 = Some m' /\ Mem.free m' blk lo2 hi2 = Some m''.
-Proof.
-  intros. 
-  destruct (Mem.range_perm_free m blk lo1 hi1) as [m' FREE1].
-  red; intros. apply H. omega. omega. 
-  destruct (Mem.range_perm_free m' blk lo2 hi2) as [m'' FREE2].
-  red; intros. eapply Mem.perm_free_1; eauto. right. omega. 
-  apply H. omega. omega. 
-  exists m'; exists m''; auto.
-Qed.
-
 Lemma function_epilogue_correct:
-  forall j ls ls0 m sp m' sp' pa cs rs k m1,
+  forall j ls ls0 m sp m' sp' pa ra cs fb rs k m1,
   agree_regs j ls rs ->
-  agree_frame j ls ls0 m sp m' sp' pa ->
+  agree_frame j ls ls0 m sp m' sp' pa ra ->
   Mem.inject j m m' ->
   Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 ->
-  exists rs1, exists m1', exists m2',
+  exists rs1, exists m1',
      load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) = Some pa
-  /\ Mem.free m' sp' 0 (Int.unsigned tf.(fn_retaddr_ofs)) = Some m1'
-  /\ Mem.free m1' sp' (Int.unsigned tf.(fn_retaddr_ofs) + 4) tf.(fn_stacksize) = Some m2'
+  /\ load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) = Some ra
+  /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1'
   /\ star step tge
-       (State cs tf (Vptr sp' Int.zero) (restore_callee_save fe k) rs m')
-    E0 (State cs tf (Vptr sp' Int.zero) k rs1 m')
+       (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m')
+    E0 (State cs fb (Vptr sp' Int.zero) k rs1 m')
   /\ agree_regs j (return_regs ls0 ls) rs1
   /\ agree_callee_save (return_regs ls0 ls) ls0
   /\ rs1 IT1 = rs IT1
-  /\ Mem.inject j m1 m2'.
+  /\ Mem.inject j m1 m1'.
 Proof.
   intros.
-  assert (RETADDR: Int.unsigned tf.(fn_retaddr_ofs) = fe.(fe_ofs_retaddr)).
-    rewrite unfold_transf_function. unfold fn_retaddr_ofs. 
-    apply (offset_of_index_no_overflow FI_retaddr). exact I.
-  rewrite RETADDR.
   (* can free *)
-  destruct (mem_range_perm_free_twice m' sp'
-              0 (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) (fe_size fe))
-  as [m1' [m2' [FREE1 FREE2]]].
-  intros. 
+  destruct (Mem.range_perm_free m' sp' 0 (fn_stacksize tf)) as [m1' FREE].
+  rewrite unfold_transf_function; unfold fn_stacksize. red; intros.
   assert (EITHER: fe_stack_data fe <= ofs < fe_stack_data fe + Linear.fn_stacksize f
-              \/  (ofs < fe_stack_data fe \/ fe_stack_data fe + Linear.fn_stacksize f <= ofs))
+              \/ (ofs < fe_stack_data fe \/ fe_stack_data fe + Linear.fn_stacksize f <= ofs))
   by omega.
   destruct EITHER.
   replace ofs with ((ofs - fe_stack_data fe) + fe_stack_data fe) by omega.
   eapply Mem.perm_inject with (f := j). eapply agree_inj; eauto. eauto. 
   eapply Mem.free_range_perm; eauto. omega.
-  eapply agree_perm; eauto.
-  apply (offset_of_index_valid FI_retaddr). exact I.
-  omega.
+  eapply agree_perm; eauto. 
   (* inject after free *)
-  assert (UNMAPPED: forall b1 delta ofs k0 p,
-          j b1 = Some (sp', delta) ->
-          Mem.perm m1 b1 ofs k0 p ->
-          False).
-  {
-    intros. 
-    exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta.
-    eelim Mem.perm_free_2. eexact H2. eapply agree_bounds; eauto. 
-    eapply Mem.perm_free_3; eauto. apply Mem.perm_max with k0. eauto. eauto. 
-  }
-  assert (INJ1: Mem.inject j m1 m2').
-  {
-    eapply Mem.free_right_inject.
-    eapply Mem.free_right_inject.
-    eapply Mem.free_left_inject. eauto. eauto. 
-    eauto.
-    intros; eapply UNMAPPED; eauto.
-    eauto.
-    intros; eapply UNMAPPED; eauto.
-  }
+  assert (INJ1: Mem.inject j m1 m1').
+  eapply Mem.free_inject with (l := (sp, 0, f.(Linear.fn_stacksize)) :: nil); eauto.
+  simpl. rewrite H2. auto.
+  intros. exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta.
+  exists 0; exists (Linear.fn_stacksize f); split. auto with coqlib.
+  eapply agree_bounds. eauto. eapply Mem.perm_max. eauto.  
   (* can execute epilogue *)
   exploit restore_callee_save_correct; eauto.
     instantiate (1 := rs). red; intros. 
-    rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ H0). auto. auto. 
+    rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ _ H0). auto. auto. 
   intros [rs1 [A [B C]]].
   (* conclusions *)
-  exists rs1; exists m1'; exists m2'.
+  exists rs1; exists m1'.
   split. rewrite unfold_transf_function; unfold fn_link_ofs. 
     eapply index_contains_load_stack with (idx := FI_link); eauto with stacking.
-  split. exact FREE1. 
-  split. rewrite unfold_transf_function; unfold fn_stacksize. exact FREE2.
+  split. rewrite unfold_transf_function; unfold fn_retaddr_ofs. 
+    eapply index_contains_load_stack with (idx := FI_retaddr); eauto with stacking.
+  split. auto.
   split. eexact A.
-  split. red; intros. unfold return_regs. 
+  split. red;intros. unfold return_regs. 
     generalize (register_classification r) (int_callee_save_not_destroyed r) (float_callee_save_not_destroyed r); intros.
     destruct (in_dec Loc.eq (R r) temporaries).
     rewrite C; auto. 
@@ -1787,12 +1750,14 @@ Inductive match_stacks (j: meminj) (m m': mem):
       hi <= bound -> hi <= bound' -> match_globalenvs j hi ->
       tailcall_possible sg ->
       match_stacks j m m' nil nil sg bound bound'
-  | match_stacks_cons: forall f sp ls c cs sp' c' cs' sg bound bound' tf
+  | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf
         (TAIL: is_tail c (Linear.fn_code f))
         (WTF: wt_function f)
-        (TRF: transf_function f = OK tf)
+        (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf))
+        (TRF: transf_function f = OK trf)
         (TRC: transl_code (make_env (function_bounds f)) c = c')
-        (FRM: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs'))
+        (TY_RA: Val.has_type ra Tint)
+        (FRM: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs'))
         (ARGS: forall ofs ty,
              In (S (Outgoing ofs ty)) (loc_arguments sg) ->
              slot_within_bounds f (function_bounds f) (Outgoing ofs ty))
@@ -1801,7 +1766,7 @@ Inductive match_stacks (j: meminj) (m m': mem):
         (BELOW': sp' < bound'),
       match_stacks j m m'
                    (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs)
-                   (Stackframe tf (Vptr sp' Int.zero) c' :: cs')
+                   (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs')
                    sg bound bound'.
 
 (** Invariance with respect to change of bounds. *)
@@ -1992,6 +1957,14 @@ Proof.
   induction 1; simpl; auto.
 Qed.
 
+Lemma match_stacks_type_retaddr:
+  forall j m m' cs cs' sg bound bound',
+  match_stacks j m m' cs cs' sg bound bound' ->
+  Val.has_type (parent_ra cs') Tint.
+Proof.
+  induction 1; simpl; auto.
+Qed.
+
 (** * Syntactic properties of the translation *)
 
 (** Preservation of code labels through the translation. *)
@@ -2192,8 +2165,9 @@ Lemma find_function_translated:
   agree_regs j ls rs ->
   match_stacks j m m' cs cs' sg bound bound' ->
   Linear.find_function ge ros ls = Some f ->
-  exists tf,
-     find_function tge ros rs = Some tf
+  exists bf, exists tf,
+     find_function_ptr tge ros rs = Some bf
+  /\ Genv.find_funct_ptr tge bf = Some tf
   /\ transf_fundef f = OK tf.
 Proof.
   intros until f; intros AG MS FF.
@@ -2202,14 +2176,13 @@ Proof.
   exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF. 
   rewrite Genv.find_funct_find_funct_ptr in FF. 
   exploit function_ptr_translated; eauto. intros [tf [A B]].
-  exists tf; split; auto. simpl.
+  exists b; exists tf; split; auto. simpl.
   generalize (AG m0). rewrite EQ. intro INJ. inv INJ.
-  rewrite Int.add_zero_l. 
-  inv MG. rewrite DOMAIN in H2. inv H2. simpl. rewrite A. apply dec_eq_true. 
-  eapply FUNCTIONS; eauto. 
-  destruct (Genv.find_symbol ge i) as [b|] eqn:FS; try discriminate. 
+  inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. 
+  destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate. 
   exploit function_ptr_translated; eauto. intros [tf [A B]].
-  exists tf; split; auto. simpl. rewrite symbols_preserved. rewrite FS. auto.
+  exists b; exists tf; split; auto. simpl. 
+  rewrite symbols_preserved. auto.
 Qed.
 
 Hypothesis wt_prog: wt_program prog.
@@ -2297,9 +2270,9 @@ Variables m m': mem.
 Variables ls ls0: locset.
 Variable rs: regset.
 Variables sp sp': block.
-Variables parent: val.
+Variables parent retaddr: val.
 Hypothesis AGR: agree_regs j ls rs.
-Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent.
+Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr.
 
 Lemma transl_annot_param_correct:
   forall l,
@@ -2364,27 +2337,29 @@ End ANNOT_ARGUMENTS.
 
 Inductive match_states: Linear.state -> Mach.state -> Prop :=
   | match_states_intro:
-      forall cs f sp c ls m cs' sp' rs m' j tf
+      forall cs f sp c ls m cs' fb sp' rs m' j tf
         (MINJ: Mem.inject j m m')
         (STACKS: match_stacks j m m' cs cs' f.(Linear.fn_sig) sp sp')
         (TRANSL: transf_function f = OK tf)
+        (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf))
         (WTF: wt_function f)
         (AGREGS: agree_regs j ls rs)
-        (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs'))
+        (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs'))
         (TAIL: is_tail c (Linear.fn_code f)),
       match_states (Linear.State cs f (Vptr sp Int.zero) c ls m)
-                  (Mach.State cs' tf (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m')
+                  (Mach.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m')
   | match_states_call:
-      forall cs f ls m cs' rs m' j tf
+      forall cs f ls m cs' fb rs m' j tf
         (MINJ: Mem.inject j m m')
         (STACKS: match_stacks j m m' cs cs' (Linear.funsig f) (Mem.nextblock m) (Mem.nextblock m'))
         (TRANSL: transf_fundef f = OK tf)
+        (FIND: Genv.find_funct_ptr tge fb = Some tf)
         (WTF: wt_fundef f)
         (WTLS: wt_locset ls)
         (AGREGS: agree_regs j ls rs)
         (AGLOCS: agree_callee_save ls (parent_locset cs)),
       match_states (Linear.Callstate cs f ls m)
-                  (Mach.Callstate cs' tf rs m')
+                  (Mach.Callstate cs' fb rs m')
   | match_states_return:
       forall cs ls m cs' rs m' j sg 
         (MINJ: Mem.inject j m m')
@@ -2398,7 +2373,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
 Theorem transf_step_correct:
   forall s1 t s2, Linear.step ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1'),
-  exists s2', plus Mach.step tge s1' t s2' /\ match_states s2 s2'.
+  exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
 Proof.
   assert (RED: forall f i c,
           transl_code (make_env (function_bounds f)) (i :: c) = 
@@ -2463,7 +2438,6 @@ Proof.
     apply index_local_valid; auto.
     red; auto.
     apply index_arg_valid; auto.
-  assert (idx <> FI_retaddr) by (unfold idx; destruct sl; congruence).
   exploit store_index_succeeds; eauto. eapply agree_perm; eauto.
   instantiate (1 := rs0 r). intros [m1' STORE].
   econstructor; split.
@@ -2474,12 +2448,12 @@ Proof.
   econstructor; eauto with coqlib.
   eapply Mem.store_outside_inject; eauto. 
     intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta.
-    rewrite size_type_chunk in H6.
+    rewrite size_type_chunk in H5.
     exploit offset_of_index_disj_stack_data_2; eauto.
     exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. 
     omega.
   apply match_stacks_change_mach_mem with m'; auto.
-  eauto with mem. eauto with mem. intros. rewrite <- H5; eapply Mem.load_store_other; eauto. left; unfold block; omega.
+  eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega.
   apply agree_regs_set_slot. apply agree_regs_undef_setstack; auto. 
   destruct sl.
     eapply agree_frame_set_local. eapply agree_frame_undef_setstack; eauto. auto. auto.
@@ -2548,11 +2522,15 @@ Proof.
   eapply agree_frame_parallel_stores; eauto.
 
   (* Lcall *)
-  exploit find_function_translated; eauto. intros [tf' [A B]].
+  exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
+  exploit is_tail_transf_function; eauto. intros IST. simpl in IST.
+  exploit return_address_offset_exists. eexact IST.
+  intros [ra D].
   econstructor; split.
   apply plus_one. econstructor; eauto.
   econstructor; eauto.
   econstructor; eauto with coqlib.
+  simpl; auto.
   intros; red. split.
     generalize (loc_arguments_acceptable _ _ H0). simpl. omega.
     apply Zle_trans with (size_arguments (Linear.funsig f')); auto.
@@ -2564,13 +2542,13 @@ Proof.
   simpl; red; auto.
 
   (* Ltailcall *)
-  exploit find_function_translated; eauto. intros [tf' [A B]].
+  exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]].
   exploit function_epilogue_correct; eauto.
-  intros [rs1 [m1' [m2' [P [Q [R [S [T [U [V W ]]]]]]]]]].
+  intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]].
   econstructor; split.
   eapply plus_right. eexact S. econstructor; eauto.
-  replace (find_function tge ros rs1)
-     with (find_function tge ros rs0). eauto.
+  replace (find_function_ptr tge ros rs1)
+     with (find_function_ptr tge ros rs0). eauto.
   destruct ros; simpl; auto. inv WTI. rewrite V; auto. 
   traceEq.
   econstructor; eauto.
@@ -2579,15 +2557,11 @@ Proof.
   apply match_stacks_change_linear_mem with m. 
   apply match_stacks_change_mach_mem with m'0.
   auto. 
-  eauto with mem.
-  intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega.
-    eapply Mem.perm_free_1; eauto. left; unfold block; omega.
-  intros. erewrite Mem.load_free. erewrite Mem.load_free; eauto. 
-    left; unfold block; omega. eauto. left; unfold block; omega.
-  eauto with mem.
-  intros. eapply Mem.perm_free_3; eauto. 
+  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
+  intros. rewrite <- H2. eapply Mem.load_free; eauto. left; unfold block; omega.
+  eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
-  apply Zlt_le_weak. change (Mem.valid_block m2' sp'). eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto.  eapply agree_valid_mach; eauto. 
+  apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
   eapply find_function_well_typed; eauto.
   apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
@@ -2680,7 +2654,7 @@ Proof.
 
   (* Lreturn *)
   exploit function_epilogue_correct; eauto.
-  intros [rs1 [m1' [m2' [P [Q [R [S [T [U [V W]]]]]]]]]].
+  intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]].
   econstructor; split.
   eapply plus_right. eexact S. econstructor; eauto.
   traceEq.
@@ -2689,15 +2663,11 @@ Proof.
   apply match_stacks_change_linear_mem with m. 
   apply match_stacks_change_mach_mem with m'0.
   eauto. 
-  eauto with mem. 
-  intros. eapply Mem.perm_free_1. eauto. left; unfold block; omega.
-    eapply Mem.perm_free_1; eauto. left; unfold block; omega.
-  intros. erewrite Mem.load_free. erewrite Mem.load_free; eauto. 
-    left; unfold block; omega. eauto. left; unfold block; omega.
-  eauto with mem.
-  intros. eapply Mem.perm_free_3; eauto. 
+  eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. 
+  intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega.
+  eauto with mem. intros. eapply Mem.perm_free_3; eauto. 
   apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. 
-  apply Zlt_le_weak. change (Mem.valid_block m2' sp'). eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
+  apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. 
   apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto.
 
   (* internal function *)
@@ -2707,14 +2677,11 @@ Proof.
   inversion WTF as [|f' WTFN]. subst f'.
   exploit function_prologue_correct; eauto.
   eapply match_stacks_type_sp; eauto. 
+  eapply match_stacks_type_retaddr; eauto.
   intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]].
   econstructor; split.
-  eapply plus_left. econstructor; eauto.
-  rewrite (unfold_transf_function _ _ TRANSL). unfold fn_retaddr_ofs. 
-  generalize (offset_of_index_no_overflow  _ _ TRANSL FI_retaddr I).
-  unfold offset_of_index. intros EQ; rewrite EQ. 
-  apply (offset_of_index_aligned f FI_retaddr).
-  rewrite (unfold_transf_function _ _ TRANSL) at 2. unfold fn_code. unfold transl_body. 
+  eapply plus_left. econstructor; eauto. 
+  rewrite (unfold_transf_function _ _ TRANSL). unfold fn_code. unfold transl_body. 
   eexact D. traceEq.
   generalize (Mem.alloc_result _ _ _ _ _ H). intro SP_EQ. 
   generalize (Mem.alloc_result _ _ _ _ _ A). intro SP'_EQ.
@@ -2727,10 +2694,7 @@ Proof.
   rewrite zeq_false. auto. omega. 
   intros. eapply stores_in_frame_valid; eauto with mem. 
   intros. eapply stores_in_frame_perm; eauto with mem.
-    eapply Mem.perm_free_1; eauto. left; unfold block; omega. eauto with mem. 
-  intros. rewrite <- H1.
-  transitivity (Mem.load chunk m3' b ofs). eapply stores_in_frame_contents; eauto.
-  transitivity (Mem.load chunk m2' b ofs). eapply Mem.load_free; eauto. left; unfold block; omega.
+  intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto.
   eapply Mem.load_alloc_unchanged; eauto. red. congruence.
   auto with coqlib.
 
@@ -2777,7 +2741,6 @@ Proof.
   eapply Genv.init_mem_transf_partial; eauto.
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. eauto.
-  eexact FIND.
   econstructor; eauto.
   eapply Genv.initmem_inject; eauto.
   apply match_stacks_empty with (Mem.nextblock m0). omega. omega.
@@ -2807,7 +2770,7 @@ Proof.
 Qed.
 
 Theorem transf_program_correct:
-  forward_simulation (Linear.semantics prog) (Mach.semantics tprog).
+  forward_simulation (Linear.semantics prog) (Mach.semantics return_address_offset tprog).
 Proof.
   eapply forward_simulation_plus.
   eexact symbols_preserved.