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

1 files changed, 204 insertions, 241 deletions

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.