Revu gestion retaddr et link dans Stacking

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

17 files changed, 1032 insertions, 934 deletions

diff --git a/backend/Bounds.v b/backend/Bounds.v
index 0e8b9faf..415a85f0 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -63,7 +63,7 @@ Definition slot_within_bounds (s: slot) :=
   | Local ofs Tint => 0 <= ofs < bound_int_local b
   | Local ofs Tfloat => 0 <= ofs < bound_float_local b
   | Outgoing ofs ty => 14 <= ofs /\ ofs + typesize ty <= bound_outgoing b
-  | Incoming ofs ty => 14 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig)
+  | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig))
   end.
 
 Definition instr_within_bounds (i: instruction) :=
diff --git a/backend/Conventions.v b/backend/Conventions.v
index ea7d448e..2ab2ca91 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -710,28 +710,25 @@ Proof.
   destruct s; try tauto. destruct s0; tauto.
 Qed.
 
-(** A tailcall is possible if and only if the size of arguments is 14. *)
-
-Lemma tailcall_possible_size:
-  forall s, tailcall_possible s <-> size_arguments s = 14.
-Proof.
-  intro; split; intro.
-  assert (forall tyl iregl fregl ofs,
-    (forall l, In l (loc_arguments_rec tyl iregl fregl ofs) ->
-               match l with R _ => True | S _ => False end) ->
-    size_arguments_rec tyl iregl fregl ofs = ofs).
-  induction tyl; simpl; intros.
-  auto.
-  destruct a. destruct iregl. elim (H0 _ (in_eq _ _)).
-  apply IHtyl; intros. apply H0. auto with coqlib.
-  destruct fregl. elim (H0 _ (in_eq _ _)).
-  apply IHtyl; intros. apply H0. auto with coqlib.
-  unfold size_arguments. apply H0. assumption.
-  red; intros.
-  generalize (loc_arguments_acceptable s l H0). 
-  destruct l; simpl. auto. destruct s0; intro; auto.
-  generalize (loc_arguments_bounded _ _ _ H0). 
-  generalize (typesize_pos t). omega.
+(** Decide whether a tailcall is possible. *)
+
+Definition tailcall_is_possible (sg: signature) : bool :=
+  let fix tcisp (l: list loc) :=
+    match l with
+    | nil => true
+    | R _ :: l' => tcisp l'
+    | S _ :: l' => false
+    end
+  in tcisp (loc_arguments sg).
+
+Lemma tailcall_is_possible_correct:
+  forall s, tailcall_is_possible s = true -> tailcall_possible s.
+Proof.
+  intro s. unfold tailcall_is_possible, tailcall_possible.
+  generalize (loc_arguments s). induction l; simpl; intros.
+  elim H0.
+  destruct a. 
+  destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate.
 Qed.
 
 (** ** Location of function parameters *)
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 0f5a1ec9..551462c8 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -36,7 +36,7 @@ Definition slot_valid (s: slot) :=
   match s with
   | Local ofs ty => 0 <= ofs
   | Outgoing ofs ty => 14 <= ofs
-  | Incoming ofs ty => 14 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig)
+  | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig))
   end.
 
 Definition slot_writable (s: slot) :=
diff --git a/backend/Mach.v b/backend/Mach.v
index f7275041..c64903b8 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -70,7 +70,9 @@ Record function: Set := mkfunction
   { fn_sig: signature;
     fn_code: code;
     fn_stacksize: Z;
-    fn_framesize: Z }.
+    fn_framesize: Z;
+    fn_link_ofs: int;
+    fn_retaddr_ofs: int }.
 
 Definition fundef := AST.fundef function.
 
@@ -137,6 +139,3 @@ Definition find_function_ptr
       Genv.find_symbol ge symb
   end.
 
-Definition align_16_top (lo hi: Z) :=
-  Zmax 0 (((hi - lo + 15) / 16) * 16 + lo).
-
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index 32a316ae..76e37e8e 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -46,54 +46,87 @@ Require Import Mach.
 
 (** * Structure of abstract stack frames *)
 
-(** An abstract stack frame comprises a low bound [fr_low] (the high bound
-  is implicitly 0) and a mapping from (type, offset) pairs to values. *)
+(** An abstract stack frame is a mapping from (type, offset) pairs to
+    values.  Like location sets (see module [Locations]), overlap
+    can occur. *)
 
-Record frame : Set := mkframe {
-  fr_low: Z;
-  fr_contents: typ -> Z -> val
-}.
+Definition frame : Set := typ -> Z -> val.
 
 Definition typ_eq: forall (ty1 ty2: typ), {ty1=ty2} + {ty1<>ty2}.
 Proof. decide equality. Defined.
 
 Definition update (ty: typ) (ofs: Z) (v: val) (f: frame) : frame :=
-  mkframe f.(fr_low)
-   (fun ty' ofs' => 
-     if zeq ofs ofs' then
-       if typ_eq ty ty' then v else Vundef
-     else
-       if zle (ofs' + AST.typesize ty') ofs then f.(fr_contents) ty' ofs'
-       else if zle (ofs + AST.typesize ty) ofs' then f.(fr_contents) ty' ofs'
-       else Vundef).
-
-Definition empty_frame := mkframe 0 (fun ty ofs => Vundef).
-
-(** [get_slot fr ty ofs v] holds if the frame [fr] contains value [v]
+  fun ty' ofs' => 
+    if zeq ofs ofs' then
+      if typ_eq ty ty' then v else Vundef
+    else
+      if zle (ofs' + AST.typesize ty') ofs then f ty' ofs'
+      else if zle (ofs + AST.typesize ty) ofs' then f ty' ofs'
+      else Vundef.
+
+Lemma update_same:
+  forall ty ofs v fr,
+  update ty ofs v fr ty ofs = v.
+Proof.
+  unfold update; intros. 
+  rewrite zeq_true. rewrite dec_eq_true. auto.
+Qed. 
+
+Lemma update_other:
+  forall ty ofs v fr ty' ofs',
+  ofs + AST.typesize ty <= ofs' \/ ofs' + AST.typesize ty' <= ofs ->
+  update ty ofs v fr ty' ofs' = fr ty' ofs'.
+Proof.
+  unfold update; intros.
+  generalize (AST.typesize_pos ty). 
+  generalize (AST.typesize_pos ty'). intros.
+  rewrite zeq_false.
+  destruct H. rewrite zle_false. apply zle_true. auto. omega.
+  apply zle_true. auto. 
+  omega.
+Qed.
+
+Definition empty_frame : frame := fun ty ofs => Vundef.
+
+Section FRAME_ACCESSES.
+
+Variable f: function.
+
+(** A slot [(ty, ofs)] within a frame is valid in function [f] if it lies
+  within the bounds of [f]'s frame, and it does not overlap with
+  the slots reserved for the return address and the back link. *)
+
+Inductive slot_valid: typ -> Z -> Prop :=
+  slot_valid_intro:
+    forall ty ofs,
+    0 <= ofs ->
+    ofs + AST.typesize ty <= f.(fn_framesize) ->
+    (ofs + AST.typesize ty <= Int.signed f.(fn_link_ofs)
+       \/ Int.signed f.(fn_link_ofs) + 4 <= ofs) ->
+    (ofs + AST.typesize ty <= Int.signed f.(fn_retaddr_ofs)
+       \/ Int.signed f.(fn_retaddr_ofs) + 4 <= ofs) ->
+    slot_valid ty ofs.
+
+(** [get_slot f fr ty ofs v] holds if the frame [fr] contains value [v]
   with type [ty] at word offset [ofs]. *)
 
 Inductive get_slot: frame -> typ -> Z -> val -> Prop :=
   | get_slot_intro:
       forall fr ty ofs v,
-      24 <= ofs ->
-      fr.(fr_low) + ofs + AST.typesize ty <= 0 ->
-      v = fr.(fr_contents) ty (fr.(fr_low) + ofs) -> 
+      slot_valid ty ofs ->
+      v = fr ty (ofs - f.(fn_framesize)) ->
       get_slot fr ty ofs v.
 
-(** [set_slot fr ty ofs v fr'] holds if frame [fr'] is obtained from
+(** [set_slot f fr ty ofs v fr'] holds if frame [fr'] is obtained from
   frame [fr] by storing value [v] with type [ty] at word offset [ofs]. *)
 
 Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop :=
   | set_slot_intro:
       forall fr ty ofs v fr',
-      24 <= ofs ->
-      fr.(fr_low) + ofs + AST.typesize ty <= 0 ->
-      fr' = update ty (fr.(fr_low) + ofs) v fr ->
+      slot_valid ty ofs ->
+      fr' = update ty (ofs - f.(fn_framesize)) v fr ->
       set_slot fr ty ofs v fr'.
 
-Definition init_frame (f: function) :=
-  mkframe (- f.(fn_framesize)) (fun ty ofs => Vundef).
-
 (** Extract the values of the arguments of an external call. *)
 
 Inductive extcall_arg: regset -> frame -> loc -> val -> Prop :=
@@ -114,6 +147,8 @@ Definition extcall_arguments
    (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop :=
   extcall_args rs fr (Conventions.loc_arguments sg) args.
     
+End FRAME_ACCESSES.
+
 (** Mach execution states. *)
 
 Inductive stackframe: Set :=
@@ -148,7 +183,9 @@ Inductive state: Set :=
 
 (** [parent_frame s] returns the frame of the calling function.
   It is used to access function parameters that are passed on the stack
-  (the [Mgetparent] instruction). *)
+  (the [Mgetparent] instruction).
+  [parent_function s] returns the calling function itself.
+  Suitable defaults are used if there are no calling function. *)
 
 Definition parent_frame (s: list stackframe) : frame :=
   match s with
@@ -156,6 +193,15 @@ Definition parent_frame (s: list stackframe) : frame :=
   | Stackframe f sp c fr :: s => fr
   end.
 
+Definition empty_function := 
+  mkfunction (mksignature nil None) nil 0 0 Int.zero Int.zero.
+
+Definition parent_function (s: list stackframe) : function :=
+  match s with
+  | nil => empty_function
+  | Stackframe f sp c fr :: s => f
+  end.
+
 Section RELSEM.
 
 Variable ge: genv.
@@ -177,17 +223,17 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp c rs fr m)
   | exec_Mgetstack:
       forall s f sp ofs ty dst c rs fr m v,
-      get_slot fr ty (Int.signed ofs) v ->
+      get_slot f fr ty (Int.signed ofs) v ->
       step (State s f sp (Mgetstack ofs ty dst :: c) rs fr m)
         E0 (State s f sp c (rs#dst <- v) fr m)
   | exec_Msetstack:
      forall s f sp src ofs ty c rs fr m fr',
-      set_slot fr ty (Int.signed ofs) (rs src) fr' ->
+      set_slot f fr ty (Int.signed ofs) (rs src) fr' ->
       step (State s f sp (Msetstack src ofs ty :: c) rs fr m)
         E0 (State s f sp c rs fr' m)
   | exec_Mgetparam:
       forall s f sp ofs ty dst c rs fr m v,
-      get_slot (parent_frame s) ty (Int.signed ofs) v ->
+      get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v ->
       step (State s f sp (Mgetparam ofs ty dst :: c) rs fr m)
         E0 (State s f sp c (rs#dst <- v) fr m)
   | exec_Mop:
@@ -251,11 +297,11 @@ Inductive step: state -> trace -> state -> Prop :=
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
       step (Callstate s (Internal f) rs m)
         E0 (State s f (Vptr stk (Int.repr (-f.(fn_framesize))))
-                  f.(fn_code) rs (init_frame f) m')
+                  f.(fn_code) rs empty_frame m')
   | exec_function_external:
       forall s ef args res rs1 rs2 m t,
       event_match ef args t res ->
-      extcall_arguments rs1 (parent_frame s) ef.(ef_sig) args ->
+      extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args ->
       rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       step (Callstate s (External ef) rs1 m)
          t (Returnstate s rs2 m)
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index ffdfb336..2dd3134f 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -27,7 +27,6 @@ Require Import Mach.
 Require Import Machtyping.
 Require Import Machabstr.
 Require Import Machconcr.
-Require Import Stackingproof.
 Require Import PPCgenretaddr.
 
 (** Two semantics were defined for the Mach intermediate language:
@@ -48,27 +47,6 @@ Require Import PPCgenretaddr.
   Mach semantics as input).
 *)
 
-Remark align_16_top_ge:
-  forall lo hi,
-  hi <= align_16_top lo hi.
-Proof.
-  intros. unfold align_16_top. apply Zmax_bound_r. 
-  assert (forall x, x <= (x + 15) / 16 * 16).
-  intro. assert (16 > 0). omega.
-  generalize (Z_div_mod_eq (x + 15) 16 H). intro.
-  replace ((x + 15) / 16 * 16) with ((x + 15) - (x + 15) mod 16).
-  generalize (Z_mod_lt (x + 15) 16 H). omega. 
-  rewrite Zmult_comm. omega.
-  generalize (H (hi - lo)). omega. 
-Qed.
-
-Remark align_16_top_pos:
-  forall lo hi,
-  0 <= align_16_top lo hi.
-Proof.
-  intros. unfold align_16_top. apply Zmax_bound_l. omega.
-Qed.
-
 Remark size_type_chunk:
   forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty.
 Proof.
@@ -79,11 +57,16 @@ Qed.
 
 (** ** Agreement for one frame *)
 
+Section FRAME_MATCH.
+
+Variable f: function.
+Hypothesis wt_f: wt_function f.
+
 (** The core idea of the simulation proof is that for all active
   functions, the memory-allocated activation record, in the concrete 
   semantics, contains the same data as the Cminor stack block
   (at positive offsets) and the frame of the function (at negative
-  offsets) in the abstract semantics.
+  offsets) in the abstract semantics
 
   This intuition (activation record = Cminor stack data + frame)
   is formalized by the following predicate [frame_match fr sp base mm ms].
@@ -91,19 +74,18 @@ Qed.
   semantics. [ms] is the current memory state in the concrete semantics.
   The stack pointer is [Vptr sp base] in both semantics. *)
 
-Inductive frame_match (fr: frame) (sp: block) (base: int) 
+Inductive frame_match (fr: frame)
+                      (sp: block) (base: int) 
                       (mm ms: mem) : Prop :=
   frame_match_intro:
     valid_block ms sp ->
     low_bound mm sp = 0 ->
-    low_bound ms sp = fr.(fr_low) ->
+    low_bound ms sp = -f.(fn_framesize) ->
     high_bound ms sp >= 0 ->
-    fr.(fr_low) <= -24 ->
-    Int.min_signed <= fr.(fr_low) ->
-    base = Int.repr fr.(fr_low) ->
+    base = Int.repr (-f.(fn_framesize)) ->
     (forall ty ofs,
-       fr.(fr_low) + 24 <= ofs -> ofs + AST.typesize ty <= 0 ->
-       load (chunk_of_type ty) ms sp ofs = Some(fr.(fr_contents) ty ofs)) ->
+       -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 ->
+       load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) ->
     frame_match fr sp base mm ms.
 
 (** The following two innocuous-looking lemmas are the key results
@@ -140,22 +122,36 @@ Qed.
   to reading the corresponding slot from the frame
   (in the abstract semantics).  *)
 
+Lemma frame_match_load_stack:
+  forall fr sp base mm ms ty ofs,
+  frame_match fr sp base mm ms ->
+  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
+  load_stack ms (Vptr sp base) ty ofs = 
+  Some (fr ty (Int.signed ofs - f.(fn_framesize))).
+Proof.
+  intros. inv H.
+  unfold load_stack, Val.add, loadv.
+  replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs))
+     with (Int.signed ofs - fn_framesize f).
+  apply H6. omega. omega.
+  inv wt_f.
+  assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
+    apply Int.signed_repr.
+    assert (0 <= Int.max_signed). compute; congruence. omega.
+  rewrite int_add_no_overflow. rewrite H. omega.
+  rewrite H. split. omega.
+  apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. 
+  compute; congruence.
+Qed.
+
 Lemma frame_match_get_slot:
   forall fr sp base mm ms ty ofs v,
   frame_match fr sp base mm ms ->
-  get_slot fr ty (Int.signed ofs) v ->
+  get_slot f fr ty (Int.signed ofs) v ->
   load_stack ms (Vptr sp base) ty ofs = Some v.
 Proof.
-  intros. inv H. inv H0. 
-  unfold load_stack, Val.add, loadv. 
-  assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr).
-    apply Int.signed_repr.
-    split. auto. apply Zle_trans with (-24). auto. compute; congruence.
-  assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs).
-    rewrite int_add_no_overflow. rewrite H0. auto.
-    rewrite H0. split. omega. apply Zle_trans with 0.
-    generalize (AST.typesize_pos ty). omega. compute; congruence.
-  rewrite H9. apply H8. omega. auto.
+  intros. inversion H. inv H0. eapply frame_match_load_stack; eauto.
+  inv H7. auto.
 Qed.
 
 (** Assigning a value to a frame slot (in the abstract semantics)
@@ -163,41 +159,42 @@ Qed.
   (in the concrete semantics).  Moreover, agreement between frames
   and activation records is preserved. *)
 
-Lemma frame_match_set_slot:
-  forall fr sp base mm ms ty ofs v fr',
+Lemma frame_match_store_stack:
+  forall fr sp base mm ms ty ofs v,
   frame_match fr sp base mm ms ->
-  set_slot fr ty (Int.signed ofs) v fr' ->
+  0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) ->
   Val.has_type v ty ->
   Mem.extends mm ms ->
   exists ms',
     store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
-    frame_match fr' sp base mm ms' /\
-    Mem.extends mm ms' /\
-    Int.signed base + 24 <= Int.signed (Int.add base ofs).
+    frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\
+    Mem.extends mm ms'.
 Proof.
-  intros. inv H. inv H0.
+  intros. inv H. inv wt_f.
   unfold store_stack, Val.add, storev.
-  assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr).
-    apply Int.signed_repr.
-    split. auto. apply Zle_trans with (-24). auto. compute; congruence.
-  assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs).
-    rewrite int_add_no_overflow. congruence. 
-    rewrite H0. split. omega. apply Zle_trans with 0.
-    generalize (AST.typesize_pos ty). omega. compute; congruence.
-  rewrite H11.
-  assert (exists ms', store (chunk_of_type ty) ms sp (fr_low fr + Int.signed ofs) v = Some ms').
+  assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) =
+          Int.signed ofs - fn_framesize f).
+  assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f).
+    apply Int.signed_repr. 
+    assert (0 <= Int.max_signed). compute; congruence. omega.
+  rewrite int_add_no_overflow. rewrite H. omega.
+  rewrite H. split. omega.
+  apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. 
+  compute; congruence.
+  rewrite H.
+  assert (exists ms', store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v = Some ms').
     apply valid_access_store. 
     constructor. auto. omega.
     rewrite size_type_chunk. omega.
-  destruct H12 as [ms' STORE]. 
+  destruct H7 as [ms' STORE]. 
   generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB.
   generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB.
   exists ms'. 
   split. exact STORE.
   (* frame match *)
-  split. constructor; simpl fr_low; try congruence.
-    eauto with mem. intros. simpl.
-    destruct (zeq (fr_low fr + Int.signed ofs) ofs0). subst ofs0.
+  split. constructor; try congruence.
+    eauto with mem. intros. unfold update.
+    destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0.
     destruct (typ_eq ty ty0). subst ty0.
     (* same *)
     transitivity (Some (Val.load_result (chunk_of_type ty) v)).
@@ -206,33 +203,45 @@ Proof.
     (* mismatch *)
     eapply load_store_mismatch'; eauto with mem.
     destruct ty; destruct ty0; simpl; congruence.
-    destruct (zle (ofs0 + AST.typesize ty0) (fr_low fr + Int.signed ofs)).
+    destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)).
     (* disjoint *)
-    rewrite <- H10; auto. eapply load_store_other; eauto.
+    rewrite <- H8; auto. eapply load_store_other; eauto.
     right; left. rewrite size_type_chunk; auto.
-    destruct (zle (fr_low fr + Int.signed ofs + AST.typesize ty)).
-    rewrite <- H10; auto. eapply load_store_other; eauto.
+    destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)).
+    rewrite <- H8; auto. eapply load_store_other; eauto.
     right; right. rewrite size_type_chunk; auto.
     (* overlap *)
     eapply load_store_overlap'; eauto with mem.
     rewrite size_type_chunk; auto. 
     rewrite size_type_chunk; auto.
   (* extends *)
-  split. eapply store_outside_extends; eauto.
+  eapply store_outside_extends; eauto.
   left. rewrite size_type_chunk. omega.
-  (* bound *)
-  omega.
+Qed.
+
+Lemma frame_match_set_slot:
+  forall fr sp base mm ms ty ofs v fr',
+  frame_match fr sp base mm ms ->
+  set_slot f fr ty (Int.signed ofs) v fr' ->
+  Val.has_type v ty ->
+  Mem.extends mm ms ->
+  exists ms',
+    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
+    frame_match fr' sp base mm ms' /\
+    Mem.extends mm ms'.
+Proof.
+  intros. inv H0. eapply frame_match_store_stack; eauto. 
+  inv H3. auto.
 Qed.
 
 (** Agreement is preserved by stores within blocks other than the
-  one pointed to by [sp], or to the low 24 bytes
-  of the [sp] block. *)
+  one pointed to by [sp]. *)
 
 Lemma frame_match_store_other:
   forall fr sp base mm ms chunk b ofs v ms',
   frame_match fr sp base mm ms ->
   store chunk ms b ofs v = Some ms' ->
-  sp <> b \/ ofs + size_chunk chunk <= fr_low fr + 24 ->
+  sp <> b ->
   frame_match fr sp base mm ms'.
 Proof.
   intros. inv H. 
@@ -242,11 +251,13 @@ Proof.
   eauto with mem. 
   congruence.
   congruence.
-  intros. rewrite <- H9; auto. 
+  intros. rewrite <- H7; auto. 
   eapply load_store_other; eauto.
-  elim H1; intro. auto. right. rewrite size_type_chunk. omega. 
 Qed.
 
+(** Agreement is preserved by parallel stores in the Machabstr
+  and the Machconcr semantics. *)
+
 Lemma frame_match_store:
   forall fr sp base mm ms chunk b ofs v mm' ms',
   frame_match fr sp base mm ms ->
@@ -262,31 +273,11 @@ Proof.
   apply frame_match_intro; auto.
   eauto with mem.
   congruence. congruence. congruence.
-  intros. rewrite <- H9; auto. eapply load_store_other; eauto.
+  intros. rewrite <- H7; auto. eapply load_store_other; eauto.
   destruct (zeq sp b). subst b. right. 
   rewrite size_type_chunk. 
   assert (valid_access mm chunk sp ofs) by eauto with mem.
-  inv H10. left. omega.
-  auto.
-Qed.
-
-(** The low 24 bytes of a frame are preserved by a parallel
-    store in the two memory states. *)
-
-Lemma frame_match_store_link_invariant:
-  forall fr sp base mm ms chunk b ofs v mm' ms' ofs',
-  frame_match fr sp base mm ms ->
-  store chunk mm b ofs v = Some mm' ->
-  store chunk ms b ofs v = Some ms' ->
-  ofs' <= fr_low fr + 20 -> 
-  load Mint32 ms' sp ofs' = load Mint32 ms sp ofs'.
-Proof.
-  intros. inv H.
-  eapply load_store_other; eauto.
-  destruct (eq_block sp b). subst b.
-  right; left. change (size_chunk Mint32) with 4. 
-  assert (valid_access mm chunk sp ofs) by eauto with mem.
-  inv H. omega. 
+  inv H8. left. omega.
   auto.
 Qed.
 
@@ -297,14 +288,12 @@ Qed.
   remain true. *)
 
 Lemma frame_match_new:
-  forall mm ms mm' ms' sp sp' f,
+  forall mm ms mm' ms' sp sp',
   mm.(nextblock) = ms.(nextblock) ->
   alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
-  alloc ms (- f.(fn_framesize)) (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) = (ms', sp') ->
-  f.(fn_framesize) >= 24 ->
-  f.(fn_framesize) <= -Int.min_signed ->
+  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') ->
   sp = sp' /\
-  frame_match (init_frame f) sp (Int.repr (-f.(fn_framesize))) mm' ms'.
+  frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'.
 Proof.
   intros. 
   assert (sp = sp').
@@ -315,13 +304,12 @@ Proof.
   generalize (low_bound_alloc_same _ _ _ _ _ H1). intro LBs.
   generalize (high_bound_alloc_same _ _ _ _ _ H0). intro HBm.
   generalize (high_bound_alloc_same _ _ _ _ _ H1). intro HBs.
+  inv wt_f.
   constructor; simpl; eauto with mem.
-  rewrite HBs. apply Zle_ge. apply align_16_top_pos.
-  omega. omega.
+  rewrite HBs. auto.
   intros.
-  eapply load_alloc_same'; eauto. omega. 
-  rewrite size_type_chunk. apply Zle_trans with 0. auto.
-  apply align_16_top_pos.
+  eapply load_alloc_same'; eauto.  
+  rewrite size_type_chunk. omega.
 Qed.
 
 Lemma frame_match_alloc:
@@ -334,13 +322,13 @@ Lemma frame_match_alloc:
 Proof.
   intros. inversion H0.
   assert (valid_block mm sp). red. rewrite H. auto.
-  exploit low_bound_alloc_other. eexact H1. eexact H11. intro LBm.
-  exploit high_bound_alloc_other. eexact H1. eexact H11. intro HBm.
+  exploit low_bound_alloc_other. eexact H1. eexact H9. intro LBm.
+  exploit high_bound_alloc_other. eexact H1. eexact H9. intro HBm.
   exploit low_bound_alloc_other. eexact H2. eexact H3. intro LBs.
   exploit high_bound_alloc_other. eexact H2. eexact H3. intro HBs.
   apply frame_match_intro.
   eapply valid_block_alloc; eauto.
-  congruence. congruence. congruence. auto. auto. auto. 
+  congruence. congruence. congruence. auto. auto.
   intros. eapply load_alloc_other; eauto. 
 Qed.
 
@@ -360,9 +348,138 @@ Proof.
   generalize (high_bound_free ms _ _ H0); intro HBs.
   apply frame_match_intro; auto.
   congruence. congruence. congruence.
-  intros. rewrite <- H8; auto. apply load_free. auto.
+  intros. rewrite <- H6; auto. apply load_free. auto.
+Qed.
+
+End FRAME_MATCH.
+
+(** ** Accounting for the return address and back link *)
+
+Section EXTEND_FRAME.
+
+Variable f: function.
+Hypothesis wt_f: wt_function f.
+Variable cs: list Machconcr.stackframe.
+
+Definition extend_frame (fr: frame) : frame :=
+  update Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize)) (parent_ra cs)
+    (update Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize)) (parent_sp cs)
+      fr).
+
+Lemma get_slot_extends:
+  forall fr ty ofs v,
+  get_slot f fr ty ofs v ->
+  get_slot f (extend_frame fr) ty ofs v.
+Proof.
+  intros. inv H. constructor. auto.
+  inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro.
+  unfold extend_frame. rewrite update_other. rewrite update_other. auto.
+  simpl; omega. simpl; omega.
+Qed.
+
+Lemma update_commut:
+  forall ty1 ofs1 v1 ty2 ofs2 v2 fr,
+  ofs1 + AST.typesize ty1 <= ofs2 \/
+  ofs2 + AST.typesize ty2 <= ofs1 ->
+  update ty1 ofs1 v1 (update ty2 ofs2 v2 fr) =
+  update ty2 ofs2 v2 (update ty1 ofs1 v1 fr).
+Proof.
+  intros. unfold frame.
+  apply extensionality. intro ty. apply extensionality. intro ofs.
+  generalize (AST.typesize_pos ty1).
+  generalize (AST.typesize_pos ty2).
+  generalize (AST.typesize_pos ty); intros.
+  unfold update.
+  set (sz1 := AST.typesize ty1) in *.
+  set (sz2 := AST.typesize ty2) in *.
+  set (sz := AST.typesize ty) in *.
+  destruct (zeq ofs1 ofs).
+  rewrite zeq_false. 
+  destruct (zle (ofs + sz) ofs2). auto.
+  destruct (zle (ofs2 + sz2) ofs). auto.
+  destruct (typ_eq ty1 ty); auto.
+  replace sz with sz1 in z. omegaContradiction. unfold sz1, sz; congruence.
+  omega.
+
+  destruct (zle (ofs + sz) ofs1).
+  auto.
+  destruct (zle (ofs1 + sz1) ofs).
+  auto.
+
+  destruct (zeq ofs2 ofs).
+  destruct (typ_eq ty2 ty); auto.
+  replace sz with sz2 in z. omegaContradiction. unfold sz2, sz; congruence.
+  destruct (zle (ofs + sz) ofs2); auto.
+  destruct (zle (ofs2 + sz2) ofs); auto.
+Qed.
+
+Lemma set_slot_extends:
+  forall fr ty ofs v fr',
+  set_slot f fr ty ofs v fr' ->
+  set_slot f (extend_frame fr) ty ofs v (extend_frame fr').
+Proof.
+  intros. inv H. constructor. auto.
+  inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro.
+  unfold extend_frame. 
+  rewrite (update_commut ty). rewrite (update_commut ty). auto.
+  simpl. omega. 
+  simpl. omega.
+Qed.
+
+Lemma frame_match_load_link:
+  forall fr sp base mm ms,
+  frame_match f (extend_frame fr) sp base mm ms ->
+  load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs).
+Proof.
+  intros. inversion wt_f.
+  replace (parent_sp cs) with
+   (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))).
+  eapply frame_match_load_stack; eauto.
+  unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. 
+Qed.
+
+Lemma frame_match_load_retaddr:
+  forall fr sp base mm ms,
+  frame_match f (extend_frame fr) sp base mm ms ->
+  load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs).
+Proof.
+  intros. inversion wt_f.
+  replace (parent_ra cs) with
+   (extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))).
+  eapply frame_match_load_stack; eauto.
+  unfold extend_frame. apply update_same.
+Qed.
+
+Lemma frame_match_function_entry:
+  forall mm ms mm' ms1 sp sp',
+  extends mm ms ->
+  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
+  alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') ->
+  Val.has_type (parent_sp cs) Tint ->
+  Val.has_type (parent_ra cs) Tint ->
+  let base := Int.repr (-f.(fn_framesize)) in
+  exists ms2, exists ms3,
+  sp = sp' /\
+  store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\
+  store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\
+  frame_match f (extend_frame empty_frame) sp base mm' ms3 /\
+  extends mm' ms3.
+Proof.
+  intros. inversion wt_f.
+  exploit alloc_extends; eauto. omega. omega. intros [A EXT0].
+  exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto.
+  fold base. intros [C FM0].
+  destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
+              FM0 wt_function_link H2 EXT0)
+  as [ms2 [STORE1 [FM1 EXT1]]].
+  destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _
+              FM1 wt_function_retaddr H3 EXT1)
+  as [ms3 [STORE2 [FM3 EXT3]]].
+  exists ms2; exists ms3; auto.
 Qed.
 
+End EXTEND_FRAME.
+
 (** ** Invariant for stacks *)
 
 Section SIMULATION.
@@ -380,31 +497,27 @@ Let ge := Genv.globalenv p.
   their addresses increase strictly from caller to callee.
 *)
 
+Definition stack_below (ts: list Machconcr.stackframe) (b: block) : Prop :=
+  match parent_sp ts with
+  | Vptr sp base' => sp < b
+  | _ => False
+  end.
+
 Inductive match_stacks: 
       list Machabstr.stackframe -> list Machconcr.stackframe ->
-      block -> int -> mem -> mem -> Prop :=
-  | match_stacks_nil: forall sp base mm ms,
-      load Mint32 ms sp (Int.signed base) = Some (Vptr Mem.nullptr Int.zero) ->
-      load Mint32 ms sp (Int.signed base + 12) = Some Vzero ->
-      match_stacks nil nil sp base mm ms
-  | match_stacks_cons: forall f sp' base' c fr s fb ra ts sp base mm ms,
-      frame_match fr sp' base' mm ms ->
-      sp' < sp ->
-      load Mint32 ms sp (Int.signed base) = Some (Vptr sp' base') ->
-      load Mint32 ms sp (Int.signed base + 12) = Some ra ->
+      mem -> mem -> Prop :=
+  | match_stacks_nil: forall mm ms,
+      match_stacks nil nil mm ms
+  | match_stacks_cons: forall fb sp base c fr s f ra ts mm ms,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      match_stacks s ts sp' base' mm ms ->
-      match_stacks (Machabstr.Stackframe f (Vptr sp' base') c fr :: s)
-                   (Machconcr.Stackframe fb (Vptr sp' base') ra c :: ts)
-                   sp base mm ms.
-
-Remark frame_match_base_eq:
-  forall fr sp base mm ms,
-  frame_match fr sp base mm ms -> Int.signed base = fr_low fr.
-Proof.
-  intros. inv H. apply Int.signed_repr. split; auto.
-  apply Zle_trans with (-24); auto. compute; congruence.
-Qed.
+      wt_function f ->
+      frame_match f (extend_frame f ts fr) sp base mm ms ->
+      stack_below ts sp ->
+      Val.has_type ra Tint ->
+      match_stacks s ts mm ms ->
+      match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s)
+                   (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts)
+                   mm ms.
 
 (** If [match_stacks] holds, a lookup in the parent frame in the
   Machabstr semantics corresponds to two memory loads in the
@@ -412,230 +525,128 @@ Qed.
   activation record, the second to read within this record. *)
 
 Lemma match_stacks_get_parent:
-  forall s ts sp base mm ms ty ofs v,
-  match_stacks s ts sp base mm ms ->
-  get_slot (parent_frame s) ty (Int.signed ofs) v ->
-  exists parent,
-     load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some parent
-  /\ load_stack ms parent ty ofs = Some v.
+  forall s ts mm ms ty ofs v,
+  match_stacks s ts mm ms ->
+  get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v ->
+  load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v.
 Proof.
   intros. inv H; simpl in H0. 
-  inv H0. simpl in H3. elimtype False. generalize (AST.typesize_pos ty). omega.
-  exists (Vptr sp' base'); split.
-  unfold load_stack. simpl. rewrite Int.add_zero. auto.
-  eapply frame_match_get_slot; eauto.
+  inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega.
+  simpl. eapply frame_match_get_slot; eauto.
+  eapply get_slot_extends; eauto. 
 Qed.
 
-(** If [match_stacks] holds, reading memory at offsets 0 and 12
-  from the stack pointer returns the stack pointer and return
-  address of the caller, respectively. *)
+(** Preservation of the [match_stacks] invariant
+    by various kinds of memory stores. *)
 
-Lemma match_stacks_load_links:
-  forall fr s ts sp base mm ms,
-  frame_match fr sp base mm ms ->
-  match_stacks s ts sp base mm ms ->
-  load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some (parent_sp ts) /\
-  load_stack ms (Vptr sp base) Tint (Int.repr 12) = Some (parent_ra ts).
-Proof.
-  intros. unfold load_stack. simpl. rewrite Int.add_zero.
-  replace (Int.signed (Int.add base (Int.repr 12)))
-     with (Int.signed base + 12).
-  inv H0; simpl; auto.
-  inv H. rewrite Int.add_signed. 
-  change (Int.signed (Int.repr 12)) with 12.
-  repeat rewrite Int.signed_repr. auto.
-  split. omega. apply Zle_trans with (-12). omega. compute; congruence.
-  split. auto. apply Zle_trans with (-24). auto. compute; congruence.
-Qed.
-
-(** The [match_stacks] invariant is preserved by memory stores
-  outside the 24-byte reserved area at the bottom of activation records.
-*)
+Remark stack_below_trans:
+  forall ts b b', 
+  stack_below ts b -> b <= b' -> stack_below ts b'.
+Proof.
+  unfold stack_below; intros. 
+  destruct (parent_sp ts); auto. omega.
+Qed.
 
 Lemma match_stacks_store_other:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
   forall chunk b ofs v ms',
   store chunk ms b ofs v = Some ms' ->
-  sp < b ->
-  match_stacks s ts sp base mm ms'.
+  stack_below ts b ->
+  match_stacks s ts mm ms'.
 Proof.
   induction 1; intros.
-  assert (sp <> b). unfold block; omega.
   constructor.
-  rewrite <- H. eapply load_store_other; eauto.
-  rewrite <- H0. eapply load_store_other; eauto.
-  assert (sp <> b). unfold block; omega.
+  red in H6; simpl in H6. 
   econstructor; eauto.
   eapply frame_match_store_other; eauto.
-  left. unfold block; omega.
-  rewrite <- H1. eapply load_store_other; eauto.
-  rewrite <- H2. eapply load_store_other; eauto.
-  eapply IHmatch_stacks; eauto. omega.
+  unfold block; omega.
+  eapply IHmatch_stacks; eauto.
+  eapply stack_below_trans; eauto. omega.
 Qed.
 
 Lemma match_stacks_store_slot:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
-  forall ty ofs v ms',
-  store_stack ms (Vptr sp base) ty ofs v = Some ms' ->
-  Int.signed base + 24 <= Int.signed (Int.add base ofs) ->
-  match_stacks s ts sp base mm ms'.
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
+  forall ty ofs v ms' b i,
+  stack_below ts b ->
+  store_stack ms (Vptr b i) ty ofs v = Some ms' ->
+  match_stacks s ts mm ms'.
 Proof.
   intros.
-  unfold store_stack in H0. simpl in H0. 
-  assert (load Mint32 ms' sp (Int.signed base) = load Mint32 ms sp (Int.signed base)).
-  eapply load_store_other; eauto.
-  right; left. change (size_chunk Mint32) with 4; omega.
-  assert (load Mint32 ms' sp (Int.signed base + 12) = load Mint32 ms sp (Int.signed base + 12)).
-  eapply load_store_other; eauto.
-  right; left. change (size_chunk Mint32) with 4; omega.
+  unfold store_stack in H1. simpl in H1.
   inv H.
-  constructor; congruence.
-  constructor; auto.
+  constructor.
+  red in H0; simpl in H0.
+  econstructor; eauto.
   eapply frame_match_store_other; eauto.
-  left; unfold block; omega.
-  congruence. congruence.
+  unfold block; omega.
   eapply match_stacks_store_other; eauto. 
+  eapply stack_below_trans; eauto. omega.
 Qed.
 
 Lemma match_stacks_store:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
-  forall fr chunk b ofs v mm' ms',
-  frame_match fr sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
+  forall chunk b ofs v mm' ms',
   store chunk mm b ofs v = Some mm' ->
   store chunk ms b ofs v = Some ms' ->
-  match_stacks s ts sp base mm' ms'.
+  match_stacks s ts mm' ms'.
 Proof.
   induction 1; intros.
-  assert (Int.signed base = fr_low fr) by (eapply frame_match_base_eq; eauto).
   constructor.
-  rewrite <- H. eapply frame_match_store_link_invariant; eauto. omega.
-  rewrite <- H0. eapply frame_match_store_link_invariant; eauto. omega.
-  assert (Int.signed base = fr_low fr0) by (eapply frame_match_base_eq; eauto).
   econstructor; eauto.
-  eapply frame_match_store; eauto. 
-  rewrite <- H1. eapply frame_match_store_link_invariant; eauto. omega.
-  rewrite <- H2. eapply frame_match_store_link_invariant; eauto. omega.
+  eapply frame_match_store; eauto.
 Qed.
 
 Lemma match_stacks_alloc:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
   forall lom him mm' bm los his ms' bs,
   mm.(nextblock) = ms.(nextblock) ->
   alloc mm lom him = (mm', bm) ->
   alloc ms los his = (ms', bs) ->
-  match_stacks s ts sp base mm' ms'.
+  match_stacks s ts mm' ms'.
 Proof.
   induction 1; intros.
   constructor.
-  rewrite <- H; eapply load_alloc_unchanged; eauto with mem.
-  rewrite <- H0; eapply load_alloc_unchanged; eauto with mem.
   econstructor; eauto.
   eapply frame_match_alloc; eauto.
-  rewrite <- H1; eapply load_alloc_unchanged; eauto with mem.
-  rewrite <- H2; eapply load_alloc_unchanged; eauto with mem.
 Qed.
 
 Lemma match_stacks_free:
-  forall s ts sp base ms mm,
-  match_stacks s ts sp base mm ms ->
+  forall s ts ms mm,
+  match_stacks s ts mm ms ->
   forall b,
-  sp < b ->
-  match_stacks s ts sp base (Mem.free mm b) (Mem.free ms b).
+  stack_below ts b ->
+  match_stacks s ts (Mem.free mm b) (Mem.free ms b).
 Proof.
   induction 1; intros.
-  assert (sp <> b). unfold block; omega.
   constructor.
-  rewrite <- H. apply load_free; auto.
-  rewrite <- H0. apply load_free; auto.
-  assert (sp <> b). unfold block; omega.
+  red in H5; simpl in H5.
   econstructor; eauto.
   eapply frame_match_free; eauto. unfold block; omega.
-  rewrite <- H1. apply load_free; auto.
-  rewrite <- H2. apply load_free; auto.
-  eapply IHmatch_stacks; eauto. omega.
-Qed.
-
-(** Invocation of a function temporarily violates the [mach_stacks]
-  invariant: the return address and back link are not yet stored
-  in the appropriate parts of the activation record.  
-  The following [match_stacks_partial] predicate is a weaker version
-  of [match_stacks] that captures this situation. *)
-
-Inductive match_stacks_partial: 
-      list Machabstr.stackframe -> list Machconcr.stackframe ->
-      mem -> mem -> Prop :=
-  | match_stacks_partial_nil: forall mm ms,
-      match_stacks_partial nil nil mm ms
-  | match_stacks_partial_cons: forall f sp base c fr s fb ra ts mm ms,
-      frame_match fr sp base mm ms ->
-      sp < ms.(nextblock) ->
-      Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      match_stacks s ts sp base mm ms ->
-      Val.has_type ra Tint ->
-      match_stacks_partial (Machabstr.Stackframe f (Vptr sp base) c fr :: s)
-                           (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts)
-                           mm ms.
-
-Lemma match_stacks_match_stacks_partial:
-  forall s ts sp base mm ms,
-  match_stacks s ts sp base mm ms ->
-  match_stacks_partial s ts (free mm sp) (free ms sp).
-Proof.
-  intros. inv H. constructor.
-  econstructor. 
-  eapply frame_match_free; eauto. unfold block; omega.
-  simpl. inv H0; auto.
-  auto.
-  apply match_stacks_free; auto.
-  generalize (Mem.load_inv _ _ _ _ _ H3). intros [A B].
-  rewrite B.
-  destruct (getN (pred_size_chunk Mint32) (Int.signed base + 12)
-                 (contents (blocks ms sp))); exact I.
+  eapply IHmatch_stacks; eauto.
+  eapply stack_below_trans; eauto. omega.
 Qed.
 
 Lemma match_stacks_function_entry:
-  forall s ts mm ms lom him mm' los his ms' stk ms'' ms''' base,
-  match_stacks_partial s ts mm ms ->
+  forall s ts mm ms lom him mm' los his ms' stk,
+  match_stacks s ts mm ms ->
   alloc mm lom him = (mm', stk) ->
   alloc ms los his = (ms', stk) ->
-  store Mint32 ms' stk (Int.signed base) (parent_sp ts) = Some ms'' ->
-  store Mint32 ms'' stk (Int.signed base + 12) (parent_ra ts) = Some ms''' ->
-  match_stacks s ts stk base mm' ms'''.
+  match_stacks s ts mm' ms' /\ stack_below ts stk.
 Proof.
-  intros. 
-  assert (WT_SP: Val.has_type (parent_sp ts) Tint).
-    inv H; simpl; auto.
-  assert (WT_RA: Val.has_type (parent_ra ts) Tint).
-    inv H; simpl; auto.
-  assert (load Mint32 ms''' stk (Int.signed base) = Some (parent_sp ts)).
-    transitivity (load Mint32 ms'' stk (Int.signed base)).
-    eapply load_store_other; eauto. right; left. simpl. omega.
-    transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_sp ts))).
-    simpl chunk_of_type. eapply load_store_same; eauto. 
-    decEq. apply load_result_ty. auto.
-  assert (load Mint32 ms''' stk (Int.signed base + 12) = Some (parent_ra ts)).
-    transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_ra ts))).
-    simpl chunk_of_type. eapply load_store_same; eauto. 
-    decEq. apply load_result_ty. auto.
-  inv H; simpl in *.
-  constructor; auto.
-  assert (sp < stk). rewrite (alloc_result _ _ _ _ _ H1). auto.
-  assert (sp <> stk). unfold block; omega.
-  assert (nextblock mm = nextblock ms).
-  rewrite <- (alloc_result _ _ _ _ _ H0). 
-  rewrite <- (alloc_result _ _ _ _ _ H1). auto.
-  econstructor; eauto.
-  eapply frame_match_store_other; eauto. 
-  eapply frame_match_store_other; eauto.
-  eapply frame_match_alloc with (mm := mm) (ms := ms); eauto.
-  eapply match_stacks_store_other; eauto. 
-  eapply match_stacks_store_other; eauto.
-  eapply match_stacks_alloc with (mm := mm) (ms := ms); eauto.
- Qed.
+  intros.
+  assert (stk = nextblock mm). eapply Mem.alloc_result; eauto.
+  assert (stk = nextblock ms). eapply Mem.alloc_result; eauto.
+  split.
+  eapply match_stacks_alloc; eauto. congruence.
+  red. 
+  inv H; simpl.
+  unfold nullptr. apply Zgt_lt. apply nextblock_pos. 
+  inv H6. red in H. rewrite H3. auto. 
+Qed.
 
 (** ** Invariant between states. *)
 
@@ -651,27 +662,27 @@ Inductive match_states:
             Machabstr.state -> Machconcr.state -> Prop :=
   | match_states_intro:
       forall s f sp base c rs fr mm ts fb ms
-        (STACKS: match_stacks s ts sp base mm ms)
-        (FM: frame_match fr sp base mm ms)
+        (STACKS: match_stacks s ts mm ms)
+        (FM: frame_match f (extend_frame f ts fr) sp base mm ms)
+        (BELOW: stack_below ts sp)
         (MEXT: Mem.extends mm ms)
         (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)),
       match_states (Machabstr.State s f (Vptr sp base) c rs fr mm)
                    (Machconcr.State ts fb (Vptr sp base) c rs ms)
   | match_states_call:
       forall s f rs mm ts fb ms
-        (STACKS: match_stacks_partial s ts mm ms)
+        (STACKS: match_stacks s ts mm ms)
         (MEXT: Mem.extends mm ms)
         (FIND: Genv.find_funct_ptr ge fb = Some f),
       match_states (Machabstr.Callstate s f rs mm)
                    (Machconcr.Callstate ts fb rs ms)
   | match_states_return:
       forall s rs mm ts ms
-        (STACKS: match_stacks_partial s ts mm ms)
+        (STACKS: match_stacks s ts mm ms)
         (MEXT: Mem.extends mm ms),
       match_states (Machabstr.Returnstate s rs mm)
                    (Machconcr.Returnstate ts rs ms).
 
-
 (** * The proof of simulation *)
 
 (** The proof of simulation relies on diagrams of the following form:
@@ -710,29 +721,23 @@ Qed.
 
 Lemma transl_extcall_arguments:
   forall rs s sg args ts m ms,
-  Machabstr.extcall_arguments rs (parent_frame s) sg args ->
-  match_stacks_partial s ts m ms ->
+  Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args ->
+  match_stacks s ts m ms ->
   extcall_arguments rs ms (parent_sp ts) sg args.
 Proof.
   unfold Machabstr.extcall_arguments, extcall_arguments; intros.
-  assert (forall ty ofs v,
-    get_slot (parent_frame s) ty (Int.signed ofs) v ->
-    load_stack ms (parent_sp ts) ty ofs = Some v).
-  inv H0; simpl; intros.
-  inv H0. simpl in H2. elimtype False. generalize (AST.typesize_pos ty). omega.
-  eapply frame_match_get_slot; eauto.
   assert (forall locs vals,
-    Machabstr.extcall_args rs (parent_frame s) locs vals ->
+    Machabstr.extcall_args (parent_function s) rs (parent_frame s) locs vals ->
     extcall_args rs ms (parent_sp ts) locs vals).
-  induction locs; intros; inversion H2; subst; clear H2.
+  induction locs; intros; inv H1.
   constructor.
   constructor; auto.
-  inversion H7; subst; clear H7. 
-  constructor.
-  constructor. auto.  
+  inv H6. constructor. constructor. eapply match_stacks_get_parent; eauto.
   auto.
 Qed.
 
+Hypothesis wt_prog: wt_program p.
+
 Theorem step_equiv:
   forall s1 t s2, Machabstr.step ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1') (WTS: wt_state s1),
@@ -746,27 +751,33 @@ Proof.
   econstructor; eauto with coqlib.
 
   (* Mgetstack *)
+  assert (WTF: wt_function f) by (inv WTS; auto).
   exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split.
-  apply exec_Mgetstack; auto. eapply frame_match_get_slot; eauto.
+  constructor; auto.
+  eapply frame_match_get_slot; eauto.
+  eapply get_slot_extends; eauto.
   econstructor; eauto with coqlib.
 
   (* Msetstack *)
+  assert (WTF: wt_function f) by (inv WTS; auto).
   assert (Val.has_type (rs src) ty).
     inv WTS. 
     generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI.
     inv WTI. apply WTRS.
-  exploit frame_match_set_slot; eauto. 
-  intros [ms' [STORE [FM' [EXT' BOUND]]]].
+  exploit frame_match_set_slot; eauto.
+    eapply set_slot_extends; eauto.
+  intros [ms' [STORE [FM' EXT']]].
   exists (State ts fb (Vptr sp0 base) c rs ms'); split.
   apply exec_Msetstack; auto.
   econstructor; eauto.
   eapply match_stacks_store_slot; eauto.
 
   (* Mgetparam *)
-  exploit match_stacks_get_parent; eauto. 
-  intros [parent [LOAD1 LOAD2]].
+  assert (WTF: wt_function f) by (inv WTS; auto).
   exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split.
-  eapply exec_Mgetparam; eauto. 
+  eapply exec_Mgetparam; eauto.
+    eapply frame_match_load_link; eauto.
+    eapply match_stacks_get_parent; eauto.
   econstructor; eauto with coqlib. 
  
   (* Mop *)
@@ -802,16 +813,17 @@ Proof.
   econstructor; split.
   eapply exec_Mcall; eauto. 
   econstructor; eauto. 
-  econstructor; eauto. inv FM; auto. exact I.  
+  econstructor; eauto. inv WTS; auto. exact I.
 
   (* Mtailcall *)
+  assert (WTF: wt_function f) by (inv WTS; auto).
   exploit find_function_find_function_ptr; eauto. 
   intros [fb' [FIND' FINDFUNCT]].
-  exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2].
   econstructor; split.
   eapply exec_Mtailcall; eauto.
-  econstructor; eauto.
-  eapply match_stacks_match_stacks_partial; eauto. 
+    eapply frame_match_load_link; eauto.
+    eapply frame_match_load_retaddr; eauto.
+  econstructor; eauto. eapply match_stacks_free; auto.
   apply free_extends; auto.
 
   (* Malloc *)
@@ -841,67 +853,32 @@ Proof.
   econstructor; eauto.
 
   (* Mreturn *)
-  exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2].
+  assert (WTF: wt_function f) by (inv WTS; auto).
   econstructor; split.
   eapply exec_Mreturn; eauto.
-  econstructor; eauto.  
-  eapply match_stacks_match_stacks_partial; eauto. 
+    eapply frame_match_load_link; eauto.
+    eapply frame_match_load_retaddr; eauto.
+  econstructor; eauto. eapply match_stacks_free; eauto.   
   apply free_extends; auto.
 
   (* internal function *)
-  assert (WTF: wt_function f). inv WTS. inv H5. auto. inv WTF.
-  caseEq (alloc ms (- f.(fn_framesize))
-                   (align_16_top (- f.(fn_framesize)) f.(fn_stacksize))).
+  assert (WTF: wt_function f). inv WTS. inv H5. auto.
+  caseEq (alloc ms (- f.(fn_framesize)) f.(fn_stacksize)).
   intros ms' stk' ALLOC.
-  exploit (alloc_extends m ms m' ms' 0 (fn_stacksize f)
-               (- fn_framesize f)
-               (align_16_top (- fn_framesize f) (fn_stacksize f))); eauto.
-  omega. apply align_16_top_ge. 
-  intros [EQ EXT']. subst stk'.
-  exploit (frame_match_new m ms); eauto. inv MEXT; auto.
-  intros [EQ FM]. clear EQ.
-  set (sp := Vptr stk (Int.repr (- fn_framesize f))).
-  assert (exists ms'', store Mint32 ms' stk (- fn_framesize f) (parent_sp ts) = Some ms'').
-    apply valid_access_store. constructor. 
-    eauto with mem.
-    rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega.
-    rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC).
-    change (size_chunk Mint32) with 4. 
-    apply Zle_trans with 0. omega. apply align_16_top_pos.
-  destruct H0 as [ms'' STORE1].
-  assert (exists ms''', store Mint32 ms'' stk (- fn_framesize f + 12) (parent_ra ts) = Some ms''').
-    apply valid_access_store. constructor. 
-    eauto with mem.
-    rewrite (low_bound_store _ _ _ _ _ _ STORE1 stk). 
-    rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega.
-    rewrite (high_bound_store _ _ _ _ _ _ STORE1 stk). 
-    rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC).
-    change (size_chunk Mint32) with 4. 
-    apply Zle_trans with 0. omega. apply align_16_top_pos.
-  destruct H0 as [ms''' STORE2].
-  assert (RANGE1: Int.min_signed <= - fn_framesize f <= Int.max_signed).
-  split. omega. apply Zle_trans with (-24). omega. compute;congruence.
-  assert (RANGE2: Int.min_signed <= - fn_framesize f + 12 <= Int.max_signed).
-  split. omega. apply Zle_trans with (-12). omega. compute;congruence.
+  assert (Val.has_type (parent_sp ts) Tint).
+    inv STACKS; simpl; auto.
+  assert (Val.has_type (parent_ra ts) Tint).
+    inv STACKS; simpl; auto.
+  destruct (frame_match_function_entry _ WTF _ _ _ _ _ _ _
+              MEXT H ALLOC H0 H1)
+  as [ms2 [ms3 [EQ [STORE1 [STORE2 [FM MEXT']]]]]].
+  subst stk'.
   econstructor; split.
   eapply exec_function_internal; eauto.
-  unfold store_stack. simpl. rewrite Int.add_zero. 
-  rewrite Int.signed_repr. eauto. auto.
-  unfold store_stack. simpl. rewrite Int.add_signed.
-  change (Int.signed (Int.repr 12)) with 12.
-  repeat rewrite Int.signed_repr; eauto.
-  (* match states *)
-  unfold sp; econstructor; eauto.
-  eapply match_stacks_function_entry; eauto.
-  rewrite Int.signed_repr; eauto.
-  rewrite Int.signed_repr; eauto.
-  eapply frame_match_store_other with (ms := ms''); eauto.
-  eapply frame_match_store_other with (ms := ms'); eauto. 
-  simpl. right; omega. simpl. right; omega.
-  eapply store_outside_extends with (m2 := ms''); eauto.
-  eapply store_outside_extends with (m2 := ms'); eauto.
-  rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega.
-  rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega.
+  exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW].
+  econstructor; eauto.
+  eapply match_stacks_store_slot with (ms := ms2); eauto.
+  eapply match_stacks_store_slot with (ms := ms'); eauto.
 
   (* external function *)
   econstructor; split.
@@ -916,8 +893,6 @@ Proof.
   econstructor; eauto.
 Qed.
 
-Hypothesis wt_prog: wt_program p.
-
 Lemma equiv_initial_states:
   forall st1, Machabstr.initial_state p st1 ->
   exists st2, Machconcr.initial_state p st2 /\ match_states st1 st2 /\ wt_state st1.
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 2eb3d478..0cfd8f11 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -41,17 +41,17 @@ Require PPCgenretaddr.
   caller function at offset 0.
 
 In addition to this linking of activation records, the concrete
-semantics also make provisions for storing a return address
-at offset 12 from the stack pointer.  This stack location will
-be used by the PPC code generated by [PPCgen] 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.  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] predicate
-from module [PPCgenretaddr] is used to guess the value of the return
-address that the PPC code generated later will store in the
-reserved location.
+semantics also make provisions for storing a back link at offset
+[f.(fn_link_ofs)] from the stack pointer, and a return address at
+offset [f.(fn_retaddr_ofs)].  The latter stack location will be used
+by the PPC code generated by [PPCgen] 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.  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] predicate from module
+[PPCgenretaddr] is used to guess the value of the return address that
+the PPC code generated later will store in the reserved location.
 *)
 
 Definition chunk_of_type (ty: typ) :=
@@ -146,11 +146,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 rs m')
   | exec_Mgetparam:
-      forall s f sp parent ofs ty dst c rs m v,
-      load_stack m sp Tint (Int.repr 0) = Some parent ->
+      forall s fb f sp parent 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 ->
       load_stack m parent ty ofs = Some v ->
-      step (State s f sp (Mgetparam ofs ty dst :: c) rs m)
-        E0 (State s f sp c (rs#dst <- v) m)
+      step (State s fb sp (Mgetparam ofs ty dst :: c) rs m)
+        E0 (State s fb sp c (rs#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 ->
@@ -177,10 +178,11 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s)
                        f' rs m)
   | exec_Mtailcall:
-      forall s fb stk soff sig ros c rs m f',
+      forall s fb stk soff sig ros c rs m f f',
       find_function_ptr ge ros rs = Some f' ->
-      load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) ->
-      load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) ->
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
       step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
         E0 (Callstate s f' rs (Mem.free m stk))
   | exec_Malloc:
@@ -210,20 +212,19 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Mcond cond args lbl :: c) rs m)
         E0 (State s f sp c rs m)
   | exec_Mreturn:
-      forall s f stk soff c rs m,
-      load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) ->
-      load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) ->
-      step (State s f (Vptr stk soff) (Mreturn :: c) rs m)
+      forall s fb stk soff c rs m f,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
+      step (State s fb (Vptr stk soff) (Mreturn :: c) rs m)
         E0 (Returnstate s rs (Mem.free m stk))
   | exec_function_internal:
       forall s fb rs m f m1 m2 m3 stk,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
-      Mem.alloc m (- f.(fn_framesize))
-                  (align_16_top (- f.(fn_framesize)) f.(fn_stacksize))
-                                                        = (m1, stk) ->
+      Mem.alloc m (- f.(fn_framesize)) f.(fn_stacksize) = (m1, stk) ->
       let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in
-      store_stack m1 sp Tint (Int.repr 0) (parent_sp s) = Some m2 ->
-      store_stack m2 sp Tint (Int.repr 12) (parent_ra s) = Some 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) rs m3)
   | exec_function_external:
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 5e5f03c4..f9f76d82 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -90,9 +90,16 @@ Record wt_function (f: function) : Prop := mk_wt_function {
   wt_function_stacksize:
     f.(fn_stacksize) >= 0;
   wt_function_framesize:
-    f.(fn_framesize) >= 24;
-  wt_function_no_overflow:
-    f.(fn_framesize) <= -Int.min_signed
+    0 <= f.(fn_framesize) <= -Int.min_signed;
+  wt_function_link:
+    0 <= Int.signed f.(fn_link_ofs)
+    /\ Int.signed f.(fn_link_ofs) + 4 <= f.(fn_framesize);
+  wt_function_retaddr:
+    0 <= Int.signed f.(fn_retaddr_ofs)
+    /\ Int.signed f.(fn_retaddr_ofs) + 4 <= f.(fn_framesize);
+  wt_function_link_retaddr:
+    Int.signed f.(fn_retaddr_ofs) + 4 <= Int.signed f.(fn_link_ofs)
+    \/ Int.signed f.(fn_link_ofs) + 4 <= Int.signed f.(fn_retaddr_ofs)
 }.
 
 Inductive wt_fundef: fundef -> Prop :=
@@ -122,7 +129,7 @@ Definition wt_regset (rs: regset) : Prop :=
   forall r, Val.has_type (rs r) (mreg_type r).
 
 Definition wt_frame (fr: frame) : Prop :=
-  forall ty ofs, Val.has_type (fr.(fr_contents) ty ofs) ty.
+  forall ty ofs, Val.has_type (fr ty ofs) ty.
 
 Lemma wt_setreg:
   forall (rs: regset) (r: mreg) (v: val),
@@ -136,28 +143,28 @@ Proof.
 Qed.
 
 Lemma wt_get_slot:
-  forall fr ty ofs v,
-  get_slot fr ty ofs v ->
+  forall f fr ty ofs v,
+  get_slot f fr ty ofs v ->
   wt_frame fr ->
   Val.has_type v ty. 
 Proof.
   induction 1; intros.
-  subst v. apply H2.
+  subst v. apply H1.
 Qed.
 
 Lemma wt_set_slot:
-  forall fr ty ofs v fr',
-  set_slot fr ty ofs v fr' ->
+  forall f fr ty ofs v fr',
+  set_slot f fr ty ofs v fr' ->
   wt_frame fr ->
   Val.has_type v ty ->
   wt_frame fr'.
 Proof.
-  intros. induction H. subst fr'; red; intros; simpl.
-  destruct (zeq (fr_low fr + ofs) ofs0).
+  intros. induction H. subst fr'; red; intros. unfold update.
+  destruct (zeq (ofs - f.(fn_framesize)) ofs0).
   destruct (typ_eq ty ty0). congruence. exact I.
-  destruct (zle (ofs0 + AST.typesize ty0) (fr_low fr + ofs)).
+  destruct (zle (ofs0 + AST.typesize ty0) (ofs - f.(fn_framesize))).
   apply H0.
-  destruct (zle (fr_low fr + ofs + AST.typesize ty) ofs0).
+  destruct (zle (ofs - f.(fn_framesize) + AST.typesize ty) ofs0).
   apply H0.
   exact I.
 Qed.
@@ -168,13 +175,6 @@ Proof.
   intros; red; intros; exact I.
 Qed.
 
-Lemma wt_init_frame:
-  forall f,
-  wt_frame (init_frame f).
-Proof.
-  intros; red; intros; exact I.
-Qed.
-
 Lemma is_tail_find_label:
   forall lbl c c', find_label lbl c = Some c' -> is_tail c' c.
 Proof.
@@ -235,7 +235,7 @@ Proof.
        eapply wt_state_intro; eauto with coqlib).
 
   apply wt_setreg; auto. 
-  inversion H0. rewrite H2. apply wt_get_slot with fr (Int.signed ofs); auto.
+  inversion H0. rewrite H2. eapply wt_get_slot; eauto.
 
   inversion H0. eapply wt_set_slot; eauto. 
   rewrite <- H2. apply WTRS.
@@ -244,7 +244,7 @@ Proof.
     destruct s; simpl. apply wt_empty_frame. 
     generalize (STK s (in_eq _ _)); intro. inv H1. auto. 
   inversion H0. apply wt_setreg; auto.
-  rewrite H3. apply wt_get_slot with (parent_frame s) (Int.signed ofs); auto.
+  rewrite H3. eapply wt_get_slot; eauto.
 
   apply wt_setreg; auto. inv H0.
     simpl in H. 
@@ -280,7 +280,7 @@ Proof.
   econstructor; eauto.
 
   econstructor; eauto with coqlib. inv H5; auto. exact I. 
-  apply wt_init_frame.
+  apply wt_empty_frame.
 
   econstructor; eauto. apply wt_setreg; auto.
   generalize (wt_event_match _ _ _ _ H). 
diff --git a/backend/PPC.v b/backend/PPC.v
index 8af2c9be..7a330639 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -98,7 +98,7 @@ Inductive instruction : Set :=
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
   | Paddze: ireg -> ireg -> instruction                       (**r add Carry bit *)
   | Pallocblock: instruction                                  (**r allocate new heap block *)
-  | Pallocframe: Z -> Z -> instruction                        (**r allocate new stack frame *)
+  | Pallocframe: Z -> Z -> int -> instruction                 (**r allocate new stack frame *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
   | Pandi_: ireg -> ireg -> constant -> instruction           (**r and immediate and set conditions *)
@@ -121,7 +121,7 @@ Inductive instruction : Set :=
   | Peqv: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-xor *)
   | Pextsb: ireg -> ireg -> instruction                       (**r 8-bit sign extension *)
   | Pextsh: ireg -> ireg -> instruction                       (**r 16-bit sign extension *)
-  | Pfreeframe: instruction                                   (**r deallocate stack frame and restore previous frame *)
+  | Pfreeframe: int -> instruction                            (**r deallocate stack frame and restore previous frame *)
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
@@ -243,25 +243,25 @@ lbl:    .long   0x43300000, 0x80000000
 lbl:    .long   0x43300000, 0x00000000
         .text
 >>
-- [Pallocframe lo hi]: in the formal semantics, this pseudo-instruction
+- [Pallocframe lo hi ofs]: in the formal semantics, this pseudo-instruction
   allocates a memory block with bounds [lo] and [hi], stores the value
-  of register [r1] (the stack pointer, by convention) at the bottom
-  of this block, and sets [r1] to a pointer to the bottom of this
+  of register [r1] (the stack pointer, by convention) at offset [ofs]
+  in this block, and sets [r1] to a pointer to the bottom of this
   block.  In the printed PowerPC assembly code, this allocation
-  is just a store-decrement of register [r1]:
+  is just a store-decrement of register [r1], assuming that [ofs = 0]:
 <<
         stwu    r1, (lo - hi)(r1)
 >>
   This cannot be expressed in our memory model, which does not reflect
   the fact that stack frames are adjacent and allocated/freed
   following a stack discipline.
-- [Pfreeframe]: in the formal semantics, this pseudo-instruction
-  reads the bottom word of the block pointed by [r1] (the stack pointer),
-  frees this block, and sets [r1] to the value of the bottom word.
-  In the printed PowerPC assembly code, this freeing
-  is just a load of register [r1] relative to [r1] itself:
+- [Pfreeframe ofs]: in the formal semantics, this pseudo-instruction
+  reads the word at offset [ofs] in the block pointed by [r1] (the
+  stack pointer), frees this block, and sets [r1] to the value of the
+  word at offset [ofs].  In the printed PowerPC assembly code, this
+  freeing is just a load of register [r1] relative to [r1] itself:
 <<
-        lwz     r1, 0(r1)
+        lwz     r1, ofs(r1)
 >>
   Again, our memory model cannot comprehend that this operation
   frees (logically) the current stack frame.
@@ -534,10 +534,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
                            #LR <- (Val.add rs#PC Vone))) m'
       | _ => Error
       end
-  | Pallocframe lo hi =>
+  | Pallocframe lo hi ofs =>
       let (m1, stk) := Mem.alloc m lo hi in
       let sp := Vptr stk (Int.repr lo) in
-      match Mem.storev Mint32 m1 sp rs#GPR1 with
+      match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with
       | None => Error
       | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR2 <- Vundef)) m2
       end
@@ -594,8 +594,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#rd <- (Val.cast8signed rs#r1))) m
   | Pextsh rd r1 =>
       OK (nextinstr (rs#rd <- (Val.cast16signed rs#r1))) m
-  | Pfreeframe =>
-      match Mem.loadv Mint32 m rs#GPR1 with
+  | Pfreeframe ofs =>
+      match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with
       | None => Error
       | Some v =>
           match rs#GPR1 with
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index 805d039b..1789fb13 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -419,14 +419,14 @@ Definition transl_load_store
 
 (** Translation of a Mach instruction. *)
 
-Definition transl_instr (i: Mach.instruction) (k: code) :=
+Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
   match i with
   | Mgetstack ofs ty dst =>
       loadind GPR1 ofs ty dst k
   | Msetstack src ofs ty =>
       storeind src GPR1 ofs ty k
   | Mgetparam ofs ty dst =>
-      Plwz GPR2 (Cint (Int.repr 0)) GPR1 :: loadind GPR2 ofs ty dst k
+      Plwz GPR2 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR2 ofs ty dst k
   | Mop op args res =>
       transl_op op args res k
   | Mload chunk addr args dst =>
@@ -484,14 +484,14 @@ Definition transl_instr (i: Mach.instruction) (k: code) :=
       Pbl symb :: k
   | Mtailcall sig (inl r) =>
       Pmtctr (ireg_of r) :: 
-      Plwz GPR2 (Cint (Int.repr 12)) GPR1 ::
+      Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR2 ::
-      Pfreeframe :: 
+      Pfreeframe f.(fn_link_ofs) :: 
       Pbctr :: k
   | Mtailcall sig (inr symb) =>
-      Plwz GPR2 (Cint (Int.repr 12)) GPR1 ::
+      Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
       Pmtlr GPR2 ::
-      Pfreeframe :: 
+      Pfreeframe f.(fn_link_ofs) :: 
       Pbs symb :: k
   | Malloc =>
       Pallocblock :: k
@@ -504,12 +504,14 @@ Definition transl_instr (i: Mach.instruction) (k: code) :=
       transl_cond cond args
         (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k)
   | Mreturn =>
-      Plwz GPR2 (Cint (Int.repr 12)) GPR1 ::
-      Pmtlr GPR2 :: Pfreeframe :: Pblr :: k
+      Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+      Pmtlr GPR2 ::
+      Pfreeframe f.(fn_link_ofs) ::
+      Pblr :: k
   end.
 
-Definition transl_code (il: list Mach.instruction) :=
-  List.fold_right transl_instr nil il.
+Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
+  List.fold_right (transl_instr f) nil il.
 
 (** Translation of a whole function.  Note that we must check
   that the generated code contains less than [2^32] instructions,
@@ -517,11 +519,10 @@ Definition transl_code (il: list Mach.instruction) :=
   around, leading to incorrect executions. *)
 
 Definition transl_function (f: Mach.function) :=
-  Pallocframe (- f.(fn_framesize))
-              (align_16_top (-f.(fn_framesize)) f.(fn_stacksize)) ::
+  Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
   Pmflr GPR2 ::
-  Pstw GPR2 (Cint (Int.repr 12)) GPR1 ::
-  transl_code f.(fn_code).
+  Pstw GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+  transl_code f f.(fn_code).
 
 Fixpoint code_size (c: code) : Z :=
   match c with
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index 2b00cfc0..932f7dea 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -157,7 +157,7 @@ Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> Prop
   transl_code_at_pc_intro:
     forall b ofs f c,
     Genv.find_funct_ptr ge b = Some (Internal f) ->
-    code_tail (Int.unsigned ofs) (transl_function f) (transl_code c) ->
+    code_tail (Int.unsigned ofs) (transl_function f) (transl_code f c) ->
     transl_code_at_pc (Vptr b ofs) b f c.
 
 (** The following lemmas show that straight-line executions
@@ -213,7 +213,7 @@ Lemma exec_straight_exec:
   forall fb f c c' rs m rs' m',
   transl_code_at_pc (rs PC) fb f c ->
   exec_straight tge (transl_function f)
-                (transl_code c) rs m c' rs' m' ->
+                (transl_code f c) rs m c' rs' m' ->
   plus step tge (State rs m) E0 (State rs' m').
 Proof.
   intros. inversion H. subst.
@@ -226,7 +226,7 @@ Lemma exec_straight_at:
   forall fb f c c' rs m rs' m',
   transl_code_at_pc (rs PC) fb f c ->
   exec_straight tge (transl_function f)
-                (transl_code c) rs m (transl_code c') rs' m' ->
+                (transl_code f c) rs m (transl_code f c') rs' m' ->
   transl_code_at_pc (rs' PC) fb f c'.
 Proof.
   intros. inversion H. subst. 
@@ -471,8 +471,8 @@ Qed.
 Hint Rewrite transl_load_store_label: labels.
 
 Lemma transl_instr_label:
-  forall i k,
-  find_label lbl (transl_instr i k) = 
+  forall f i k,
+  find_label lbl (transl_instr f i k) = 
     if Mach.is_label lbl i then Some k else find_label lbl k.
 Proof.
   intros. generalize (Mach.is_label_correct lbl i). 
@@ -488,9 +488,9 @@ Proof.
 Qed.
 
 Lemma transl_code_label:
-  forall c,
-  find_label lbl (transl_code c) = 
-    option_map transl_code (Mach.find_label lbl c).
+  forall f c,
+  find_label lbl (transl_code f c) = 
+    option_map (transl_code f) (Mach.find_label lbl c).
 Proof.
   induction c; simpl; intros.
   auto. rewrite transl_instr_label.
@@ -501,7 +501,7 @@ Qed.
 Lemma transl_find_label:
   forall f,
   find_label lbl (transl_function f) = 
-    option_map transl_code (Mach.find_label lbl f.(fn_code)).
+    option_map (transl_code f) (Mach.find_label lbl f.(fn_code)).
 Proof.
   intros. unfold transl_function. simpl. apply transl_code_label.
 Qed.
@@ -525,7 +525,7 @@ Proof.
   generalize (transl_find_label lbl f).
   rewrite H1; simpl. intro.
   generalize (label_pos_code_tail lbl (transl_function f) 0 
-                 (transl_code c') H2).
+                 (transl_code f c') H2).
   intros [pos' [A [B C]]].
   exists (rs#PC <- (Vptr b (Int.repr pos'))).
   split. unfold goto_label. rewrite A. rewrite H0. auto.
@@ -663,7 +663,7 @@ Lemma exec_straight_steps:
   incl c2 f.(fn_code) ->
   transl_code_at_pc (rs1 PC) fb f c1 ->
   (exists rs2,
-     exec_straight tge (transl_function f) (transl_code c1) rs1 m1 (transl_code c2) rs2 m2
+     exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2
      /\ agree ms2 sp rs2) ->
   exists st',
   plus step tge (State rs1 m1) E0 st' /\
@@ -729,7 +729,7 @@ Proof.
   rewrite (sp_val _ _ _ AG) in H.
   assert (NOTE: GPR1 <> GPR0). congruence.
   generalize (loadind_correct tge (transl_function f) GPR1 ofs ty
-                dst (transl_code c) rs m v H H1 NOTE).
+                dst (transl_code f c) rs m v H H1 NOTE).
   intros [rs2 [EX [RES OTH]]].
   left; eapply exec_straight_steps; eauto with coqlib.
   simpl. exists rs2; split. auto. 
@@ -756,7 +756,7 @@ Proof.
   rewrite (preg_val ms sp rs) in H; auto.
   assert (NOTE: GPR1 <> GPR0). congruence.
   generalize (storeind_correct tge (transl_function f) GPR1 ofs ty
-                src (transl_code c) rs m m' H H1 NOTE).
+                src (transl_code f c) rs m m' H H1 NOTE).
   intros [rs2 [EX OTH]].
   left; eapply exec_straight_steps; eauto with coqlib.
   exists rs2; split; auto.
@@ -764,30 +764,32 @@ Proof.
 Qed.
 
 Lemma exec_Mgetparam_prop:
-  forall (s : list stackframe) (fb : block) (sp parent : val)
+  forall (s : list stackframe) (fb : block) (f: Mach.function) (sp parent : val)
          (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction)
          (ms : Mach.regset) (m : mem) (v : val),
-  load_stack m sp Tint (Int.repr 0) = Some parent ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  load_stack m sp Tint f.(fn_link_ofs) = Some parent ->
   load_stack m parent ty ofs = Some v ->
   exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0
                   (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
 Proof.
   intros; red; intros; inv MS.
+  assert (f0 = f) by congruence. subst f0.
   set (rs2 := nextinstr (rs#GPR2 <- parent)).
   assert (EX1: exec_straight tge (transl_function f)
-                 (transl_code (Mgetparam ofs ty dst :: c)) rs m
-                 (loadind GPR2 ofs ty dst (transl_code c)) rs2 m).
+                 (transl_code f (Mgetparam ofs ty dst :: c)) rs m
+                 (loadind GPR2 ofs ty dst (transl_code f c)) rs2 m).
   simpl. apply exec_straight_one.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen.
   unfold const_low. rewrite <- (sp_val ms sp rs); auto.
-  unfold load_stack in H. simpl chunk_of_type in H. 
-  rewrite H. reflexivity. reflexivity.
+  unfold load_stack in H0. simpl chunk_of_type in H0. 
+  rewrite H0. reflexivity. reflexivity.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inversion WTI.
-  unfold load_stack in H0. change parent with rs2#GPR2 in H0.
+  unfold load_stack in H1. change parent with rs2#GPR2 in H1.
   assert (NOTE: GPR2 <> GPR0). congruence.
   generalize (loadind_correct tge (transl_function f) GPR2 ofs ty
-                dst (transl_code c) rs2 m v H0 H2 NOTE).
+                dst (transl_code f c) rs2 m v H1 H3 NOTE).
   intros [rs3 [EX2 [RES OTH]]].
   left; eapply exec_straight_steps; eauto with coqlib.
   exists rs3; split; simpl.
@@ -852,7 +854,7 @@ Proof.
   generalize (transl_load_correct tge (transl_function f)
                 (Plbz (ireg_of dst)) (Plbzx (ireg_of dst))
                 Mint8unsigned addr args 
-                (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code c) 
+                (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code f c) 
                 ms sp rs m dst a v'
                 X1 X2 AG H3 H7 LOAD').
   intros [rs2 [EX1 AG1]].
@@ -965,21 +967,23 @@ Qed.
 Lemma exec_Mtailcall_prop:
   forall (s : list stackframe) (fb stk : block) (soff : int)
          (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
-         (ms : Mach.regset) (m : mem) (f' : block),
+         (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block),
   find_function_ptr ge ros ms = Some f' ->
-  load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
   exec_instr_prop
           (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
           (Callstate s f' ms (free m stk)).
 Proof.
   intros; red; intros; inv MS.
+  assert (f0 = f) by congruence. subst f0.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inversion WTI.
   inversion AT. subst b f0 c0.
   assert (NOOV: code_size (transl_function f) <= Int.max_unsigned).
     eapply functions_transl_no_overflow; eauto.
-  destruct ros; simpl in H; simpl in H8.
+  destruct ros; simpl in H; simpl in H9.
   (* Indirect call *)
   set (rs2 := nextinstr (rs#CTR <- (ms m0))).
   set (rs3 := nextinstr (rs2#GPR2 <- (parent_ra s))).
@@ -987,27 +991,27 @@ Proof.
   set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))).
   set (rs6 := rs5#PC <- (rs5 CTR)).
   assert (exec_straight tge (transl_function f)
-            (transl_code (Mtailcall sig (inl ident m0) :: c)) rs m 
-            (Pbctr :: transl_code c) rs5 (free m stk)).
+            (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m 
+            (Pbctr :: transl_code f c) rs5 (free m stk)).
   simpl. apply exec_straight_step with rs2 m. 
-  simpl. rewrite <- (ireg_val _ _ _ _ AG H5). reflexivity. reflexivity.
+  simpl. rewrite <- (ireg_val _ _ _ _ AG H6). reflexivity. reflexivity.
   apply exec_straight_step with rs3 m.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). 
-  simpl. unfold load_stack in H1. simpl in H1. rewrite H1.
+  simpl. unfold load_stack in H2. simpl in H2. rewrite H2.
   reflexivity. discriminate. reflexivity.
   apply exec_straight_step with rs4 m.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
   simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
-  unfold load_stack in H0; simpl in H0. rewrite Int.add_zero in H0.
-  simpl. rewrite H0. reflexivity. reflexivity.
+  unfold load_stack in H1; simpl in H1. 
+  simpl. rewrite H1. reflexivity. reflexivity.
   left; exists (State rs6 (free m stk)); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
   change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone) Vone).
-  rewrite <- H6; simpl. eauto.
+  rewrite <- H7; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
@@ -1018,7 +1022,7 @@ Proof.
     unfold rs4, rs3, rs2; auto 10 with ppcgen.
   assert (AG5: agree ms (parent_sp s) rs5).
     unfold rs5. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG4. rewrite H11. 
+    split. reflexivity. intros. inv AG4. rewrite H12. 
     rewrite Pregmap.gso; auto with ppcgen.
   unfold rs6; auto with ppcgen.
   change (rs6 PC) with (ms m0). 
@@ -1030,25 +1034,25 @@ Proof.
   set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
   set (rs5 := rs4#PC <- (Vptr f' Int.zero)).
   assert (exec_straight tge (transl_function f)
-            (transl_code (Mtailcall sig (inr mreg i) :: c)) rs m 
-            (Pbs i :: transl_code c) rs4 (free m stk)).
+            (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m 
+            (Pbs i :: transl_code f c) rs4 (free m stk)).
   simpl. apply exec_straight_step with rs2 m. 
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   rewrite <- (sp_val _ _ _ AG). 
-  simpl. unfold load_stack in H1. simpl in H1. rewrite H1.
+  simpl. unfold load_stack in H2. simpl in H2. rewrite H2.
   reflexivity. discriminate. reflexivity.
   apply exec_straight_step with rs3 m.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
   simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
-  unfold load_stack in H0; simpl in H0. rewrite Int.add_zero in H0.
-  simpl. rewrite H0. reflexivity. reflexivity.
+  unfold load_stack in H1; simpl in H1.
+  simpl. rewrite H1. reflexivity. reflexivity.
   left; exists (State rs5 (free m stk)); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
   econstructor.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone).
-  rewrite <- H6; simpl. eauto.
+  rewrite <- H7; simpl. eauto.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
@@ -1060,7 +1064,7 @@ Proof.
     unfold rs3, rs2; auto 10 with ppcgen.
   assert (AG4: agree ms (parent_sp s) rs4).
     unfold rs4. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG3. rewrite H11. 
+    split. reflexivity. intros. inv AG3. rewrite H12. 
     rewrite Pregmap.gso; auto with ppcgen.
   unfold rs5; auto with ppcgen.
 Qed.
@@ -1120,8 +1124,8 @@ Proof.
   intro WTI. inv WTI.
   pose (k1 := 
          if snd (crbit_for_cond cond)
-         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code c
-         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c).
+         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c
+         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c).
   generalize (transl_cond_correct tge (transl_function f)
                 cond args k1 ms sp rs m true H3 AG H).
   simpl. intros [rs2 [EX [RES AG2]]].
@@ -1161,8 +1165,8 @@ Proof.
   intro WTI. inversion WTI.
   pose (k1 := 
          if snd (crbit_for_cond cond)
-         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code c
-         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code c).
+         then Pbt (fst (crbit_for_cond cond)) lbl :: transl_code f c
+         else Pbf (fst (crbit_for_cond cond)) lbl :: transl_code f c).
   generalize (transl_cond_correct tge (transl_function f)
                 cond args k1 ms sp rs m false H1 AG H).
   simpl. intros [rs2 [EX [RES AG2]]].
@@ -1181,30 +1185,32 @@ Qed.
 
 Lemma exec_Mreturn_prop:
   forall (s : list stackframe) (fb stk : block) (soff : int)
-         (c : list Mach.instruction) (ms : Mach.regset) (m : mem),
-  load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) ->
-  load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) ->
+         (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function),
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+  load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
   exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
                   (Returnstate s ms (free m stk)).
 Proof.
   intros; red; intros; inv MS.
+  assert (f0 = f) by congruence. subst f0.
   set (rs2 := nextinstr (rs#GPR2 <- (parent_ra s))).
   set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
   set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
   set (rs5 := rs4#PC <- (parent_ra s)).
   assert (exec_straight tge (transl_function f)
-            (transl_code (Mreturn :: c)) rs m 
-            (Pblr :: transl_code c) rs4 (free m stk)).
+            (transl_code f (Mreturn :: c)) rs m 
+            (Pblr :: transl_code f c) rs4 (free m stk)).
   simpl. apply exec_straight_three with rs2 m rs3 m.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  unfold load_stack in H0. simpl in H0. 
-  rewrite <- (sp_val _ _ _ AG). simpl. rewrite H0.
+  unfold load_stack in H1. simpl in H1. 
+  rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1.
   reflexivity. discriminate.
   unfold rs3. change (parent_ra s) with rs2#GPR2. reflexivity.
   simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
   simpl. 
-  unfold load_stack in H. simpl in H. rewrite Int.add_zero in H.  
-  rewrite H. reflexivity.
+  unfold load_stack in H0. simpl in H0.
+  rewrite H0. reflexivity.
   reflexivity. reflexivity. reflexivity.
   left; exists (State rs5 (free m stk)); split.
   (* execution *)
@@ -1212,10 +1218,10 @@ Proof.
   eapply exec_straight_exec; eauto.
   inv AT. econstructor.
   change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). 
-  rewrite <- H2. simpl. eauto.
+  rewrite <- H3. simpl. eauto.
   apply functions_transl; eauto.
-  generalize (functions_transl_no_overflow _ _ H3); intro NOOV.
-  simpl in H4. eapply find_instr_tail. 
+  generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
+  simpl in H5. eapply find_instr_tail. 
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; auto.
   eapply code_tail_next_int; eauto.
@@ -1237,11 +1243,10 @@ Lemma exec_function_internal_prop:
   forall (s : list stackframe) (fb : block) (ms : Mach.regset)
          (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  alloc m (- fn_framesize f)
-          (align_16_top (- fn_framesize f) (fn_stacksize f)) = (m1, stk) ->
+  alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
   let sp := Vptr stk (Int.repr (- fn_framesize f)) in
-  store_stack m1 sp Tint (Int.repr 0) (parent_sp s) = Some m2 ->
-  store_stack m2 sp Tint (Int.repr 12) (parent_ra s) = Some 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 ->
   exec_instr_prop (Machconcr.Callstate s fb ms m) E0
                   (Machconcr.State s fb sp (fn_code f) ms m3).
 Proof.
@@ -1258,14 +1263,12 @@ Proof.
   assert (EXEC_PROLOGUE:
             exec_straight tge (transl_function f)
               (transl_function f) rs m
-              (transl_code (fn_code f)) rs4 m3).
+              (transl_code f (fn_code f)) rs4 m3).
   unfold transl_function at 2. 
   apply exec_straight_three with rs2 m2 rs3 m2.
-  unfold exec_instr. rewrite H0. fold sp. 
-  generalize H1. unfold store_stack. change (Vint (Int.repr 0)) with Vzero.
-  replace (Val.add sp Vzero) with sp. simpl chunk_of_type. 
-  rewrite (sp_val _ _ _ AG). intro EQ; rewrite EQ; clear EQ.
-  reflexivity. unfold sp. simpl. rewrite Int.add_zero. reflexivity.
+  unfold exec_instr. rewrite H0. fold sp.
+  unfold store_stack in H1. simpl chunk_of_type in H1. 
+  rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity.
   simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity.
   simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
   unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR2) with (parent_ra s).
diff --git a/backend/PPCgenretaddr.v b/backend/PPCgenretaddr.v
index 3526865e..eab8599e 100644
--- a/backend/PPCgenretaddr.v
+++ b/backend/PPCgenretaddr.v
@@ -68,7 +68,7 @@ Qed.
 Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop :=
   | return_address_offset_intro:
       forall c f ofs,
-      code_tail ofs (transl_function f) (transl_code c) ->
+      code_tail ofs (transl_function f) (transl_code f c) ->
       return_address_offset f c (Int.repr ofs).
 
 (** We now show that such an offset always exists if the Mach code [c]
@@ -159,7 +159,7 @@ Proof. unfold transl_load_store; intros; destruct addr; IsTail. Qed.
 Hint Resolve transl_load_store_tail: ppcretaddr.
 
 Lemma transl_instr_tail:
-  forall i k, is_tail k (transl_instr i k).
+  forall f i k, is_tail k (transl_instr f i k).
 Proof.
   unfold transl_instr; intros; destruct i; IsTail.
   destruct m; IsTail.
@@ -170,7 +170,7 @@ Qed.
 Hint Resolve transl_instr_tail: ppcretaddr.
 
 Lemma transl_code_tail: 
-  forall c1 c2, is_tail c1 c2 -> is_tail (transl_code c1) (transl_code c2).
+  forall f c1 c2, is_tail c1 c2 -> is_tail (transl_code f c1) (transl_code f c2).
 Proof.
   induction 1; simpl. constructor. eapply is_tail_trans; eauto with ppcretaddr.
 Qed.
@@ -179,7 +179,7 @@ Lemma return_address_exists:
   forall f c, is_tail c f.(fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
-  intros. assert (is_tail (transl_code c) (transl_function f)).
+  intros. assert (is_tail (transl_code f c) (transl_function f)).
   unfold transl_function. IsTail. apply transl_code_tail; auto.
   destruct (is_tail_code_tail _ _ H0) as [ofs A].
   exists (Int.repr ofs). constructor. auto.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index a30f9e50..fa9dd210 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -224,7 +224,7 @@ Definition check_instr (i: instruction) : bool :=
       match ros with inl r => check_reg r Tint | inr s => true end
       && check_regs args sig.(sig_args)
       && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res)
-      && zeq (Conventions.size_arguments sig) 14
+      && Conventions.tailcall_is_possible sig
   | Ialloc arg res s =>
       check_reg arg Tint 
       && check_reg res Tint
@@ -330,8 +330,7 @@ Proof.
   destruct s0; auto. apply check_reg_correct; auto.
   eapply proj_sumbool_true; eauto.
   apply check_regs_correct; auto.
-  rewrite Conventions.tailcall_possible_size. 
-  eapply proj_sumbool_true; eauto.
+  apply Conventions.tailcall_is_possible_correct; auto.
   (* alloc *)
   constructor. 
   apply check_reg_correct; auto.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 3f0ff1ee..2edb4827 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -300,12 +300,13 @@ Proof.
   inv H. inv H1. constructor. unfold wt_function. simpl. 
   apply wt_parallel_move; auto with reloadty.
     rewrite loc_parameters_type. auto.
-    unfold loc_parameters; red; intros.
-    destruct (list_in_map_inv _ _ _ H) as [r [A B]]. rewrite A.
-    generalize (loc_arguments_acceptable _ _ B). 
-    destruct r; simpl; auto. destruct s; try tauto.
-    intros; simpl. split. omega. 
-    apply loc_arguments_bounded; auto.
+    red; intros.
+    destruct (list_in_map_inv _ _ _ H) as [r [A B]].
+    generalize (loc_arguments_acceptable _ _ B).
+    destruct r; intro.
+    rewrite A. simpl. auto.
+    red in H0. destruct s; try tauto.
+    simpl in A. subst l. simpl. auto.
   apply wt_transf_code; auto.
   constructor.
 Qed.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 16595e54..a1310aa1 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -45,9 +45,8 @@ Require Import Conventions.
 To facilitate some of the proofs, the Cminor stack-allocated data
 starts at offset 0; the preceding areas in the activation record
 therefore have negative offsets.  This part (with negative offsets)
-is called the ``frame'' (see the [Machabstr] semantics for the Mach
-language), by opposition with the ``Cminor stack data'' which is the part
-with positive offsets.
+is called the ``frame'', by opposition with the ``Cminor stack data''
+which is the part with positive offsets.
 
 The [frame_env] compilation environment records the positions of
 the boundaries between areas in the frame part.
@@ -55,6 +54,8 @@ the boundaries between areas in the frame part.
 
 Record frame_env : Set := mk_frame_env {
   fe_size: Z;
+  fe_ofs_link: Z;
+  fe_ofs_retaddr: Z;
   fe_ofs_int_local: Z;
   fe_ofs_int_callee_save: Z;
   fe_num_int_callee_save: Z;
@@ -67,19 +68,22 @@ Record frame_env : Set := mk_frame_env {
   function. *)
 
 Definition make_env (b: bounds) :=
-  let oil := 4 * b.(bound_outgoing) in              (* integer locals *)
+  let oil := 4 * b.(bound_outgoing) in    (* integer locals *)
   let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *)
   let oendi := oics + 4 * b.(bound_int_callee_save) in
   let ofl := align oendi 8 in       (* float locals *)
   let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
   let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *)
-  mk_frame_env sz oil oics b.(bound_int_callee_save)
+  mk_frame_env sz 0 12
+                  oil oics b.(bound_int_callee_save)
                   ofl ofcs b.(bound_float_callee_save).
 
 (** Computation the frame offset for the given component of the frame.
   The component is expressed by the following [frame_index] sum type. *)
 
 Inductive frame_index: Set :=
+  | FI_link: frame_index
+  | FI_retaddr: frame_index
   | FI_local: Z -> typ -> frame_index
   | FI_arg: Z -> typ -> frame_index
   | FI_saved_int: Z -> frame_index
@@ -87,6 +91,8 @@ Inductive frame_index: Set :=
 
 Definition offset_of_index (fe: frame_env) (idx: frame_index) :=
   match idx with
+  | FI_link => fe.(fe_ofs_link)
+  | FI_retaddr => fe.(fe_ofs_retaddr)
   | FI_local x Tint => fe.(fe_ofs_int_local) + 4 * x
   | FI_local x Tfloat => fe.(fe_ofs_float_local) + 8 * x
   | FI_arg x ty => 4 * x
@@ -218,7 +224,8 @@ Definition transl_instr
   | Lcall sig ros =>
       Mcall sig ros :: k
   | Ltailcall sig ros =>
-      restore_callee_save fe (Mtailcall sig ros :: k)
+      restore_callee_save fe
+        (Mtailcall sig ros :: k)
   | Lalloc =>
       Malloc :: k
   | Llabel lbl =>
@@ -228,7 +235,8 @@ Definition transl_instr
   | Lcond cond args lbl =>
       Mcond cond args lbl :: k
   | Lreturn =>
-      restore_callee_save fe (Mreturn :: k)
+      restore_callee_save fe
+        (Mreturn :: k)
   end.
 
 (** Translation of a function.  Code that saves the values of used
@@ -260,7 +268,9 @@ Definition transf_function (f: Linear.function) : res Mach.function :=
          f.(Linear.fn_sig)
          (transl_body f fe)
          f.(Linear.fn_stacksize)
-         fe.(fe_size)).
+         fe.(fe_size)
+         (Int.repr fe.(fe_ofs_link))
+         (Int.repr fe.(fe_ofs_retaddr))).
 
 Definition transf_fundef (f: Linear.fundef) : res Mach.fundef :=
   AST.transf_partial_fundef transf_function f.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 46e19ca9..fc2b63a1 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -50,6 +50,7 @@ Proof.
   destruct ty; auto.
 Qed.
 
+(*
 Lemma get_slot_ok:
   forall fr ty ofs,
   24 <= ofs -> fr.(fr_low) + ofs + 4 * typesize ty <= 0 ->
@@ -133,6 +134,7 @@ Lemma slot_gi:
 Proof.
   intros. rewrite <- typesize_typesize in H0. constructor; auto.
 Qed.
+*)
 
 Section PRESERVATION.
 
@@ -157,7 +159,9 @@ Lemma unfold_transf_function:
          f.(Linear.fn_sig)
          (transl_body f fe)
          f.(Linear.fn_stacksize)
-         fe.(fe_size).
+         fe.(fe_size)
+         (Int.repr fe.(fe_ofs_link))
+         (Int.repr fe.(fe_ofs_retaddr)).
 Proof.
   generalize TRANSF_F. unfold transf_function.
   case (zlt (Linear.fn_stacksize f) 0). intros; discriminate.
@@ -180,6 +184,8 @@ Qed.
 
 Definition index_valid (idx: frame_index) :=
   match idx with
+  | FI_link => True
+  | FI_retaddr => True
   | FI_local x Tint => 0 <= x < b.(bound_int_local)
   | FI_local x Tfloat => 0 <= x < b.(bound_float_local)
   | FI_arg x ty => 14 <= x /\ x + typesize ty <= b.(bound_outgoing)
@@ -189,6 +195,8 @@ Definition index_valid (idx: frame_index) :=
 
 Definition type_of_index (idx: frame_index) :=
   match idx with
+  | FI_link => Tint
+  | FI_retaddr => Tint
   | FI_local x ty => ty
   | FI_arg x ty => ty
   | FI_saved_int x => Tint
@@ -200,6 +208,8 @@ Definition type_of_index (idx: frame_index) :=
 
 Definition index_diff (idx1 idx2: frame_index) : Prop :=
   match idx1, idx2 with
+  | FI_link, FI_link => False
+  | FI_retaddr, FI_retaddr => False
   | FI_local x1 ty1, FI_local x2 ty2 =>
       x1 <> x2 \/ ty1 <> ty2
   | FI_arg x1 ty1, FI_arg x2 ty2 =>
@@ -224,7 +234,7 @@ Ltac AddPosProps :=
   generalize (bound_outgoing_pos b); intro;
   generalize align_float_part; intro.
 
-Lemma size_pos: fe.(fe_size) >= 24.
+Lemma size_pos: fe.(fe_size) >= 0.
 Proof.
   AddPosProps.
   unfold fe, make_env, fe_size. omega.
@@ -246,6 +256,7 @@ Proof.
   unfold offset_of_index, fe, make_env,
     fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
     fe_ofs_float_local, fe_ofs_float_callee_save,
+    fe_ofs_link, fe_ofs_retaddr,
     type_of_index, typesize;
   simpl in H5; simpl in H6; simpl in H7;
   try omega.
@@ -302,7 +313,7 @@ Hint Resolve index_local_valid index_arg_valid
 Lemma offset_of_index_valid:
   forall idx,
   index_valid idx ->
-  24 <= offset_of_index fe idx /\
+  0 <= offset_of_index fe idx /\
   offset_of_index fe idx + 4 * typesize (type_of_index idx) <= fe.(fe_size).
 Proof.
   AddPosProps.
@@ -311,6 +322,7 @@ Proof.
   unfold offset_of_index, fe, make_env,
     fe_size, fe_ofs_int_local, fe_ofs_int_callee_save,
     fe_ofs_float_local, fe_ofs_float_callee_save,
+    fe_ofs_link, fe_ofs_retaddr,
     type_of_index, typesize;
   simpl in H5;
   omega.
@@ -327,7 +339,7 @@ Proof.
   intros.
   generalize (offset_of_index_valid idx H). intros [A B].
   apply Int.signed_repr.
-  split. apply Zle_trans with 24; auto. compute; intro; discriminate.
+  split. apply Zle_trans with 0; auto. compute; intro; discriminate.
   assert (offset_of_index fe idx < fe_size fe).
     generalize (typesize_pos (type_of_index idx)); intro. omega.
   apply Zlt_succ_le. 
@@ -335,102 +347,111 @@ Proof.
   generalize size_no_overflow. omega. 
 Qed.
 
-(** Admissible evaluation rules for the [Mgetstack] and [Msetstack]
-  instructions, in case the offset is computed with [offset_of_index]. *)
+(** Characterization of the [get_slot] and [set_slot]
+  operations in terms of the following [index_val] and [set_index_val]
+  frame access functions. *)
 
-Lemma exec_Mgetstack':
-  forall sp idx ty c rs fr dst m v,
-  index_valid idx ->
-  get_slot fr ty (offset_of_index fe idx) v ->
-  step tge 
-     (State stack tf sp
-            (Mgetstack (Int.repr (offset_of_index fe idx)) ty dst :: c)
-            rs fr m)
-  E0 (State stack tf sp c (rs#dst <- v) fr m).
-Proof.
-  intros. apply exec_Mgetstack.
-  rewrite offset_of_index_no_overflow. auto. auto.
-Qed.
+Definition index_val (idx: frame_index) (fr: frame) :=
+  fr (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)).
 
-Lemma exec_Msetstack':
-  forall sp idx ty c rs fr src m fr',
-  index_valid idx ->
-  set_slot fr ty (offset_of_index fe idx) (rs src) fr' ->
-  step tge
-     (State stack tf sp
-           (Msetstack src (Int.repr (offset_of_index fe idx)) ty :: c) 
-           rs fr m)
-  E0 (State stack tf sp c rs fr' m).
+Definition set_index_val (idx: frame_index) (v: val) (fr: frame) :=
+  update (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)) v fr.
+
+Lemma slot_valid_index:
+  forall idx,
+  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->
+  slot_valid tf (type_of_index idx) (offset_of_index fe idx).
 Proof.
-  intros. apply exec_Msetstack.
-  rewrite offset_of_index_no_overflow. auto. auto.
+  intros.
+  destruct (offset_of_index_valid idx H) as [A B].
+  rewrite <- typesize_typesize in B.
+  rewrite unfold_transf_function; constructor.
+  auto. unfold fn_framesize. auto.
+  unfold fn_link_ofs. change (fe_ofs_link fe) with (offset_of_index fe FI_link).
+  rewrite offset_of_index_no_overflow.
+  exploit (offset_of_index_disj idx FI_link).
+    auto. exact I. red. destruct idx; auto || congruence.
+  intro. rewrite typesize_typesize. assumption.
+  exact I.
+  unfold fn_retaddr_ofs. change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr).
+  rewrite offset_of_index_no_overflow.
+  exploit (offset_of_index_disj idx FI_retaddr).
+    auto. exact I. red. destruct idx; auto || congruence.
+  intro. rewrite typesize_typesize. assumption.
+  exact I.
 Qed.
 
-(** An alternate characterization of the [get_slot] and [set_slot]
-  operations in terms of the following [index_val] frame access
-  function. *)
-
-Definition index_val (idx: frame_index) (fr: frame) :=
-  fr.(fr_contents) (type_of_index idx) (fr.(fr_low) + offset_of_index fe idx).
-
 Lemma get_slot_index:
   forall fr idx ty v,
-  index_valid idx ->
-  fr.(fr_low) = -fe.(fe_size) ->
+  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->
   ty = type_of_index idx ->
   v = index_val idx fr ->
-  get_slot fr ty (offset_of_index fe idx) v.
+  get_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe idx))) v.
 Proof.
-  intros. subst v; subst ty.
-  generalize (offset_of_index_valid idx H); intros [A B].
-  rewrite <- typesize_typesize in B. 
+  intros. subst v; subst ty. rewrite offset_of_index_no_overflow; auto.
   unfold index_val. apply get_slot_intro; auto.
-  rewrite H0. omega.
+  apply slot_valid_index; auto.
 Qed.
 
 Lemma set_slot_index:
   forall fr idx v,
-  index_valid idx ->
-  fr.(fr_low) = -fe.(fe_size) ->
-  exists fr', set_slot fr (type_of_index idx) (offset_of_index fe idx) v fr'.
-Proof.
-  intros. 
-  generalize (offset_of_index_valid idx H); intros [A B].
-  apply set_slot_ok; auto. rewrite H0. omega.
+  index_valid idx -> idx <> FI_link -> idx <> FI_retaddr ->
+  set_slot tf fr (type_of_index idx) (Int.signed (Int.repr (offset_of_index fe idx)))
+                 v (set_index_val idx v fr).
+Proof.
+  intros.  rewrite offset_of_index_no_overflow; auto.
+  apply set_slot_intro. 
+  apply slot_valid_index; auto.
+  unfold set_index_val. auto.
 Qed.
 
-(** Alternate ``good variable'' properties for [get_slot] and [set_slot]. *)
+(** ``Good variable'' properties for [index_val] and [set_index_val]. *)
 
-Lemma slot_iss:
-  forall fr idx v fr',
-  set_slot fr (type_of_index idx) (offset_of_index fe idx) v fr' ->
-  index_val idx fr' = v.
+Lemma get_set_index_val_same:
+  forall fr idx v,
+  index_val idx (set_index_val idx v fr) = v.
 Proof.
-  intros. exploit slot_gss; eauto. intro. inv H0. auto.
+  intros. unfold index_val, set_index_val. apply update_same. 
 Qed.
 
-Lemma slot_iso:
-  forall fr idx v fr' idx',
-  set_slot fr (type_of_index idx) (offset_of_index fe idx) v fr' ->
-  index_diff idx idx' ->
-  index_valid idx -> index_valid idx' ->
-  index_val idx' fr' = index_val idx' fr.
+Lemma get_set_index_val_other:
+  forall fr idx idx' v,
+  index_valid idx -> index_valid idx' -> index_diff idx idx' ->
+  index_val idx' (set_index_val idx v fr) = index_val idx' fr.
 Proof.
-  intros. generalize (offset_of_index_disj idx idx' H1 H2 H0). intro.
-  inv H. unfold index_val. simpl fr_low. apply frame_update_gso.
-  omega.
+  intros. unfold index_val, set_index_val. apply update_other.
+  repeat rewrite typesize_typesize. 
+  exploit (offset_of_index_disj idx idx'); auto. omega.
+Qed.
+
+Lemma get_set_index_val_overlap:
+  forall ofs1 ty1 ofs2 ty2 v fr,
+  S (Outgoing ofs1 ty1) <> S (Outgoing ofs2 ty2) ->
+  Loc.overlap (S (Outgoing ofs1 ty1)) (S (Outgoing ofs2 ty2)) = true ->
+  index_val (FI_arg ofs2 ty2) (set_index_val (FI_arg ofs1 ty1) v fr) = Vundef.
+Proof.
+  intros. unfold index_val, set_index_val, offset_of_index, type_of_index.
+  assert (~(ofs1 + typesize ty1 <= ofs2 \/ ofs2 + typesize ty2 <= ofs1)).
+  destruct (orb_prop _ _ H0). apply Loc.overlap_aux_true_1. auto. 
+  apply Loc.overlap_aux_true_2. auto.
+  unfold update. 
+  destruct (zeq (4 * ofs1 - fn_framesize tf) (4 * ofs2 - fn_framesize tf)).
+  destruct (typ_eq ty1 ty2). 
+  elim H. decEq. decEq. omega. auto.
+  auto.
+  repeat rewrite typesize_typesize.
+  rewrite zle_false. apply zle_false. omega. omega.
 Qed.
 
 (** * Agreement between location sets and Mach environments *)
 
 (** The following [agree] predicate expresses semantic agreement between:
 - on the Linear side, the current location set [ls] and the location
-  set at function entry [ls0];
-- on the Mach side, a register set [rs] plus the current and parent frames
-  [fr] and [parent]. 
+  set of the caller [ls0];
+- on the Mach side, a register set [rs], a frame [fr] and a call stack [cs].
 *)
 
-Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop :=
+Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Prop :=
   mk_agree {
     (** Machine registers have the same values on the Linear and Mach sides. *)
     agree_reg:
@@ -442,10 +463,6 @@ Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop :
     agree_unused_reg:
       forall r, ~(mreg_within_bounds b r) -> rs r = ls0 (R r);
 
-    (** The low bound of the current frame is [- fe.(fe_size)]. *)
-    agree_size:
-      fr.(fr_low) = -fe.(fe_size);
-
     (** Local and outgoing stack slots (on the Linear side) have
         the same values as the one loaded from the current Mach frame 
         at the corresponding offsets. *)
@@ -463,8 +480,9 @@ Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop :
         at the corresponding offsets. *)
     agree_incoming:
       forall ofs ty,
-      slot_within_bounds f b (Incoming ofs ty) ->
-      get_slot parent ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Incoming ofs ty)));
+      In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) ->
+      get_slot (parent_function cs) (parent_frame cs)
+               ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Incoming ofs ty)));
 
     (** The areas of the frame reserved for saving used callee-save
         registers always contain the values that those registers had
@@ -481,22 +499,22 @@ Record agree (ls: locset) (rs: regset) (fr parent: frame) (ls0: locset) : Prop :
       index_val (FI_saved_float (index_float_callee_save r)) fr = ls0 (R r)
   }.
 
-Hint Resolve agree_reg agree_unused_reg agree_size 
+Hint Resolve agree_reg agree_unused_reg 
              agree_locals agree_outgoing agree_incoming
              agree_saved_int agree_saved_float: stacking.
 
 (** Values of registers and register lists. *)
 
 Lemma agree_eval_reg:
-  forall ls rs fr parent ls0 r,
-  agree ls rs fr parent ls0 -> rs r = ls (R r).
+  forall ls ls0 rs fr cs r,
+  agree ls ls0 rs fr cs -> rs r = ls (R r).
 Proof.
   intros. symmetry. eauto with stacking.
 Qed.
 
 Lemma agree_eval_regs:
-  forall ls rs fr parent ls0 rl,
-  agree ls rs fr parent ls0 -> rs##rl = reglist ls rl.
+  forall ls ls0 rs fr cs rl,
+  agree ls ls0 rs cs fr -> rs##rl = reglist ls rl.
 Proof.
   induction rl; simpl; intros.
   auto. f_equal. eapply agree_eval_reg; eauto. auto.
@@ -508,10 +526,10 @@ Hint Resolve agree_eval_reg agree_eval_regs: stacking.
   of machine registers, of local slots, of outgoing slots. *)
 
 Lemma agree_set_reg:
-  forall ls rs fr parent ls0 r v,
-  agree ls rs fr parent ls0 ->
+  forall ls ls0 rs fr cs r v,
+  agree ls ls0 rs fr cs ->
   mreg_within_bounds b r ->
-  agree (Locmap.set (R r) v ls) (Regmap.set r v rs) fr parent ls0.
+  agree (Locmap.set (R r) v ls) ls0 (Regmap.set r v rs) fr cs.
 Proof.
   intros. constructor; eauto with stacking.
   intros. case (mreg_eq r r0); intro.
@@ -526,131 +544,176 @@ Proof.
 Qed.
 
 Lemma agree_set_local:
-  forall ls rs fr parent ls0 v ofs ty,
-  agree ls rs fr parent ls0 ->
+  forall ls ls0 rs fr cs v ofs ty,
+  agree ls ls0 rs fr cs ->
   slot_within_bounds f b (Local ofs ty) ->
   exists fr',
-    set_slot fr ty (offset_of_index fe (FI_local ofs ty)) v fr' /\
-    agree (Locmap.set (S (Local ofs ty)) v ls) rs fr' parent ls0.
+    set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_local ofs ty)))) v fr' /\
+    agree (Locmap.set (S (Local ofs ty)) v ls) ls0 rs fr' cs.
 Proof.
   intros.
-  generalize (set_slot_index fr _ v (index_local_valid _ _ H0) 
-                (agree_size _ _ _ _ _ H)).
-  intros [fr' SET].
-  exists fr'. split. auto. constructor; eauto with stacking.
+  exists (set_index_val (FI_local ofs ty) v fr); split.
+  set (idx := FI_local ofs ty). 
+  change ty with (type_of_index idx).
+  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
+  constructor; eauto with stacking.
   (* agree_reg *)
   intros. rewrite Locmap.gso. eauto with stacking. red; auto.
-  (* agree_size *)
-  inversion SET. rewrite H3; simpl fr_low. eauto with stacking.
   (* agree_local *)
   intros. case (slot_eq (Local ofs ty) (Local ofs0 ty0)); intro.
   rewrite <- e. rewrite Locmap.gss. 
   replace (FI_local ofs0 ty0) with (FI_local ofs ty).
-  symmetry. eapply slot_iss; eauto. congruence.
+  symmetry. apply get_set_index_val_same. congruence.
   assert (ofs <> ofs0 \/ ty <> ty0).
     case (zeq ofs ofs0); intro. compare ty ty0; intro.
     congruence. tauto.  tauto. 
-  rewrite Locmap.gso. transitivity (index_val (FI_local ofs0 ty0) fr).
-  eauto with stacking. symmetry. eapply slot_iso; eauto.
-  simpl. auto.
+  rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
+  red. auto.
   (* agree_outgoing *)
-  intros. rewrite Locmap.gso. transitivity (index_val (FI_arg ofs0 ty0) fr).
-  eauto with stacking. symmetry. eapply slot_iso; eauto.
-  red; auto. red; auto. 
+  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
+  red; auto. red; auto.
   (* agree_incoming *)
   intros. rewrite Locmap.gso. eauto with stacking. red. auto.
   (* agree_saved_int *)
-  intros. rewrite <- (agree_saved_int _ _ _ _ _ H r H1 H2). 
-  eapply slot_iso; eauto with stacking. red; auto.
+  intros. rewrite get_set_index_val_other; eauto with stacking.
+  red; auto.
   (* agree_saved_float *)
-  intros. rewrite <- (agree_saved_float _ _ _ _ _ H r H1 H2). 
-  eapply slot_iso; eauto with stacking. red; auto.
+  intros. rewrite get_set_index_val_other; eauto with stacking.
+  red; auto.
 Qed.
 
 Lemma agree_set_outgoing:
-  forall ls rs fr parent ls0 v ofs ty,
-  agree ls rs fr parent ls0 ->
+  forall ls ls0 rs fr cs v ofs ty,
+  agree ls ls0 rs fr cs ->
   slot_within_bounds f b (Outgoing ofs ty) ->
   exists fr',
-    set_slot fr ty (offset_of_index fe (FI_arg ofs ty)) v fr' /\
-    agree (Locmap.set (S (Outgoing ofs ty)) v ls) rs fr' parent ls0.
-Proof.
-  intros. 
-  generalize (set_slot_index fr _ v (index_arg_valid _ _ H0)
-                (agree_size _ _ _ _ _ H)).
-  intros [fr' SET].
-  exists fr'. split. exact SET. constructor; eauto with stacking.
+    set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_arg ofs ty)))) v fr' /\
+    agree (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 rs fr' cs.
+Proof.
+  intros.
+  exists (set_index_val (FI_arg ofs ty) v fr); split.
+  set (idx := FI_arg ofs ty). 
+  change ty with (type_of_index idx).
+  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
+  constructor; eauto with stacking.
   (* agree_reg *)
   intros. rewrite Locmap.gso. eauto with stacking. red; auto.
-  (* agree_size *)
-  inversion SET. subst fr'; simpl fr_low. eauto with stacking.
   (* agree_local *)
-  intros. rewrite Locmap.gso. 
-  transitivity (index_val (FI_local ofs0 ty0) fr).
-  eauto with stacking. symmetry. eapply slot_iso; eauto.
-  red; auto. red; auto. 
+  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
+  red; auto. red; auto.
   (* agree_outgoing *)
   intros. unfold Locmap.set. 
   case (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intro.
   (* same location *)
-  replace ofs0 with ofs. replace ty0 with ty. 
-  symmetry. eapply slot_iss; eauto.
-  congruence. congruence.
+  replace ofs0 with ofs by congruence. replace ty0 with ty by congruence.
+  symmetry. apply get_set_index_val_same.
   (* overlapping locations *)
   caseEq (Loc.overlap (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intros.
-  inv SET. unfold index_val, type_of_index, offset_of_index.
-  destruct (zeq ofs ofs0).
-  subst ofs0. symmetry. apply frame_update_mismatch. 
-  destruct ty; destruct ty0; simpl; congruence.
-  generalize (Loc.overlap_not_diff _ _ H2). intro. simpl in H5.
-  simpl fr_low. symmetry. apply frame_update_overlap. omega. omega. omega.
-  (* different locations *)
-  transitivity (index_val (FI_arg ofs0 ty0) fr).
-  eauto with stacking.
-  symmetry. eapply slot_iso; eauto. 
-  simpl. eapply Loc.overlap_aux_false_1; eauto.
+  symmetry. apply get_set_index_val_overlap; auto.
+  (* disjoint locations *)
+  rewrite get_set_index_val_other; eauto with stacking.
+  red. eapply Loc.overlap_aux_false_1; eauto.
   (* agree_incoming *)
   intros. rewrite Locmap.gso. eauto with stacking. red. auto.
   (* saved ints *)
-  intros. rewrite <- (agree_saved_int _ _ _ _ _ H r H1 H2). 
-  eapply slot_iso; eauto with stacking. red; auto.
+  intros. rewrite get_set_index_val_other; eauto with stacking. red; auto.
   (* saved floats *)
-  intros. rewrite <- (agree_saved_float _ _ _ _ _ H r H1 H2). 
-  eapply slot_iso; eauto with stacking. red; auto.
+  intros. rewrite get_set_index_val_other; eauto with stacking. red; auto.
 Qed.
+
 (*
-Lemma agree_return_regs:
-  forall ls rs fr parent ls0 ls' rs',
-  agree ls rs fr parent ls0 ->
-  (forall r,
-    In (R r) temporaries \/ In (R r) destroyed_at_call ->
-    rs' r = ls' (R r)) ->
-  (forall r,
-    In r int_callee_save_regs \/ In r float_callee_save_regs ->
-    rs' r = rs r) ->
-  agree (LTL.return_regs ls ls') rs' fr parent ls0.
+Lemma agree_set_int_callee_save:
+  forall ls ls0 rs fr r v,
+  agree ls ls0 rs fr ->
+  In r int_callee_save_regs ->
+  index_int_callee_save r < fe.(fe_num_int_callee_save) ->
+  exists fr',
+    set_slot tf fr Tint 
+             (Int.signed (Int.repr
+               (offset_of_index fe (FI_saved_int (index_int_callee_save r)))))
+             v fr' /\
+    agree ls (Locmap.set (R r) v ls0) rs fr'.
 Proof.
-  intros. constructor; unfold LTL.return_regs; eauto with stacking.
-  (* agree_reg *)
-  intros. case (In_dec Loc.eq (R r) temporaries); intro.
-  symmetry. apply H0. tauto.
-  case (In_dec Loc.eq (R r) destroyed_at_call); intro.
-  symmetry. apply H0. tauto.
-  rewrite H1. eauto with stacking. 
-  generalize (register_classification r); tauto.
+  intros.
+  set (idx := FI_saved_int (index_int_callee_save r)).
+  exists (set_index_val idx v fr); split.
+  change Tint with (type_of_index idx).
+  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
+  constructor; eauto with stacking.
   (* agree_unused_reg *)
-  intros. rewrite H1. eauto with stacking.
-  generalize H2; unfold mreg_within_bounds; case (mreg_type r); intro.
-  left. apply index_int_callee_save_pos2. 
-  generalize (bound_int_callee_save_pos b); intro. omega.
-  right. apply index_float_callee_save_pos2. 
-  generalize (bound_float_callee_save_pos b); intro. omega.
-Qed. 
+  intros. rewrite Locmap.gso. eauto with stacking.
+  red; red; intro. subst r0. elim H2. red. 
+  rewrite (int_callee_save_type r H0). auto.
+  (* agree_local *)
+  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
+  red; auto.
+  (* agree_outgoing *)
+  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
+  red; auto.
+  (* agree_incoming *)
+  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
+  (* saved ints *)
+  intros. destruct (mreg_eq r r0). 
+  subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. 
+  rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking.
+  unfold idx. auto with stacking. auto with stacking.
+  unfold idx; red. apply index_int_callee_save_inj; auto.
+  red; auto.
+  (* saved floats *)
+  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
+  unfold idx. auto with stacking. 
+  unfold idx; red; auto.
+  red. apply int_float_callee_save_disjoint; auto.
+Qed.
+
+Lemma agree_set_float_callee_save:
+  forall ls ls0 rs fr r v,
+  agree ls ls0 rs fr ->
+  In r float_callee_save_regs ->
+  index_float_callee_save r < fe.(fe_num_float_callee_save) ->
+  exists fr',
+    set_slot tf fr Tfloat
+             (Int.signed (Int.repr
+               (offset_of_index fe (FI_saved_float (index_float_callee_save r)))))
+             v fr' /\
+    agree ls (Locmap.set (R r) v ls0) rs fr'.
+Proof.
+  intros.
+  set (idx := FI_saved_float (index_float_callee_save r)).
+  exists (set_index_val idx v fr); split.
+  change Tfloat with (type_of_index idx).
+  apply set_slot_index; unfold idx. auto with stacking. congruence. congruence.
+  constructor; eauto with stacking.
+  (* agree_unused_reg *)
+  intros. rewrite Locmap.gso. eauto with stacking.
+  red; red; intro. subst r0. elim H2. red. 
+  rewrite (float_callee_save_type r H0). auto.
+  (* agree_local *)
+  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
+  red; auto.
+  (* agree_outgoing *)
+  intros. unfold idx; rewrite get_set_index_val_other; eauto with stacking.
+  red; auto.
+  (* agree_incoming *)
+  intros. rewrite Locmap.gso. eauto with stacking. red. auto.
+  (* saved ints *)
+  intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking.
+  unfold idx. auto with stacking. 
+  unfold idx; red; auto.
+  red. apply sym_not_equal. apply int_float_callee_save_disjoint; auto.
+  (* saved floats *)
+  intros. destruct (mreg_eq r r0). 
+  subst r0. rewrite Locmap.gss. unfold idx. apply get_set_index_val_same. 
+  rewrite Locmap.gso. rewrite get_set_index_val_other. eauto with stacking.
+  unfold idx. auto with stacking. auto with stacking.
+  unfold idx; red. apply index_float_callee_save_inj; auto.
+  red; auto.
+Qed.
 *)
 
 Lemma agree_return_regs:
-  forall ls rs fr parent ls0 rs',
-  agree ls rs fr parent ls0 ->
+  forall ls ls0 rs fr cs rs',
+  agree ls ls0 rs fr cs ->
   (forall r,
     ~In r int_callee_save_regs -> ~In r float_callee_save_regs ->
     rs' r = rs r) ->
@@ -695,10 +758,10 @@ Proof.
 Qed.
 
 Lemma agree_callee_save_agree:
-  forall ls rs fr parent ls1 ls2,
-  agree ls rs fr parent ls1 ->
+  forall ls ls1 ls2 rs fr cs,
+  agree ls ls1 rs fr cs ->
   agree_callee_save ls1 ls2 ->
-  agree ls rs fr parent ls2.
+  agree ls ls2 rs fr cs.
 Proof.
   intros. inv H. constructor; auto.
   intros. rewrite agree_unused_reg0; auto.
@@ -732,15 +795,15 @@ Qed.
 
 (** A variant of [agree] used for return frames. *)
 
-Definition agree_frame (ls: locset) (fr parent: frame) (ls0: locset) : Prop :=
-  exists rs, agree ls rs fr parent ls0.
+Definition agree_frame (ls ls0: locset) (fr: frame) (cs: list stackframe): Prop :=
+  exists rs, agree ls ls0 rs fr cs.
 
 Lemma agree_frame_agree:
-  forall ls1 ls2 rs fr parent ls0,
-  agree_frame ls1 fr parent ls0 ->
+  forall ls1 ls2 rs fr cs ls0,
+  agree_frame ls1 ls0 fr cs ->
   agree_callee_save ls2 ls1 ->
   (forall r, rs r = ls2 (R r)) ->
-  agree ls2 rs fr parent ls0.
+  agree ls2 ls0 rs fr cs.
 Proof.
   intros. destruct H as [rs' AG]. inv AG.
   constructor; auto.
@@ -767,10 +830,15 @@ Variable mkindex: Z -> frame_index.
 Variable ty: typ.
 Variable sp: val.
 Variable csregs: list mreg.
+
 Hypothesis number_inj: 
   forall r1 r2, In r1 csregs -> In r2 csregs -> r1 <> r2 -> number r1 <> number r2.
 Hypothesis mkindex_valid:
   forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)).
+Hypothesis mkindex_not_link:
+  forall z, mkindex z <> FI_link.
+Hypothesis mkindex_not_retaddr:
+  forall z, mkindex z <> FI_retaddr.
 Hypothesis mkindex_typ:
   forall z, type_of_index (mkindex z) = ty.
 Hypothesis mkindex_inj:
@@ -783,13 +851,11 @@ Lemma save_callee_save_regs_correct:
   forall l k rs fr m,
   incl l csregs ->
   list_norepet l ->
-  fr.(fr_low) = -fe.(fe_size) ->
   exists fr',
     star step tge 
        (State stack tf sp
          (save_callee_save_regs bound number mkindex ty fe l k) rs fr m)
     E0 (State stack tf sp k rs fr' m)
-  /\ fr'.(fr_low) = - fe.(fe_size)
   /\ (forall r,
        In r l -> number r < bound fe ->
        index_val (mkindex (number r)) fr' = rs r)
@@ -801,8 +867,9 @@ Lemma save_callee_save_regs_correct:
 Proof.
   induction l; intros; simpl save_callee_save_regs.
   (* base case *)
-  exists fr. split. apply star_refl. split. auto. 
-  split. intros. elim H2. auto.
+  exists fr. split. apply star_refl.
+  split. intros. elim H1.
+  auto.
   (* inductive case *)
   set (k1 := save_callee_save_regs bound number mkindex ty fe l k).
   assert (R1: incl l csregs). eauto with coqlib.
@@ -810,49 +877,42 @@ Proof.
   unfold save_callee_save_reg.
   destruct (zlt (number a) (bound fe)).
   (* a store takes place *)
-  assert (VALID: index_valid (mkindex (number a))).
-    apply mkindex_valid. auto with coqlib. auto.
-  exploit set_slot_index; eauto.
-  intros [fr1 SET].
-  exploit (IHl k rs fr1 m); auto. inv SET; auto. 
-  fold k1. intros [fr' [A [B [C D]]]].
+  set (fr1 := set_index_val (mkindex (number a)) (rs a) fr).
+  exploit (IHl k rs fr1 m); auto. 
+  fold k1. intros [fr' [A [B C]]].
   exists fr'.
-  split. eapply star_left.
-  apply exec_Msetstack'; eauto with stacking. rewrite <- (mkindex_typ (number a)). eauto.
-  eexact A. traceEq.
-  split. auto. 
-  split. intros. elim H2; intros. subst r. 
-    rewrite D. eapply slot_iss; eauto.  
-    apply mkindex_valid; auto.
+  split. eapply star_left. 
+  apply exec_Msetstack. instantiate (1 := fr1). 
+  unfold fr1. rewrite <- (mkindex_typ (number a)).
+  eapply set_slot_index; eauto with coqlib.
+  eexact A.
+  traceEq.
+  split. intros. simpl in H1. destruct H1. subst r.
+    rewrite C. unfold fr1. apply get_set_index_val_same.
+    apply mkindex_valid; auto with coqlib.
     intros. apply mkindex_inj. apply number_inj; auto with coqlib.
-    inversion H0. red; intro; subst r; contradiction.
-    apply C; auto.
-  intros. transitivity (index_val idx fr1).
-    apply D; auto. 
-    intros. apply H3; eauto with coqlib.
-    eapply slot_iso; eauto.
-    apply mkindex_diff. apply H3. auto with coqlib.
-    auto.
+    inversion H0. congruence.
+    apply B; auto.
+  intros. rewrite C; auto with coqlib. 
+    unfold fr1. apply get_set_index_val_other; auto with coqlib. 
   (* no store takes place *)
-  exploit (IHl k rs fr m); auto. intros [fr' [A [B [C D]]]].
-  exists fr'. split. exact A. split. exact B.
-  split. intros. elim H2; intros. subst r. omegaContradiction.
-    apply C; auto. 
-  intros. apply D; auto.
-    intros. apply H3; auto with coqlib.
+  exploit (IHl k rs fr m); auto. intros [fr' [A [B C]]].
+  exists fr'.
+  split. exact A.
+  split. intros. simpl in H1; destruct H1. subst r. omegaContradiction.
+    apply B; auto. 
+  intros. apply C; auto with coqlib.
 Qed.
 
 End SAVE_CALLEE_SAVE. 
 
 Lemma save_callee_save_int_correct:
   forall k sp rs fr m,
-  fr.(fr_low) = - fe.(fe_size) ->
   exists fr',
     star step tge 
        (State stack tf sp
          (save_callee_save_int fe k) rs fr m)
     E0 (State stack tf sp k rs fr' m)
-  /\ fr'.(fr_low) = - fe.(fe_size)
   /\ (forall r,
        In r int_callee_save_regs ->
        index_int_callee_save r < bound_int_callee_save b ->
@@ -866,26 +926,26 @@ Proof.
   exploit (save_callee_save_regs_correct fe_num_int_callee_save index_int_callee_save FI_saved_int
                                          Tint sp int_callee_save_regs).
   exact index_int_callee_save_inj.
-  intros. red. split; auto. generalize (index_int_callee_save_pos r H0). omega.
+  intros. red. split; auto. generalize (index_int_callee_save_pos r H). omega.
+  intro; congruence.
+  intro; congruence.
   auto.
   intros; congruence.
   intros until idx. destruct idx; simpl; auto. congruence.
   apply incl_refl.
-  apply int_callee_save_norepet. eauto.
-  intros [fr' [A [B [C D]]]]. 
+  apply int_callee_save_norepet.
+  intros [fr' [A [B C]]]. 
   exists fr'; intuition. unfold save_callee_save_int; eauto. 
-  apply D. auto. intros; subst idx. auto.
+  apply C. auto. intros; subst idx. auto.
 Qed.
 
 Lemma save_callee_save_float_correct:
   forall k sp rs fr m,
-  fr.(fr_low) = - fe.(fe_size) ->
   exists fr',
     star step tge 
        (State stack tf sp
          (save_callee_save_float fe k) rs fr m)
     E0 (State stack tf sp k rs fr' m)
-  /\ fr'.(fr_low) = - fe.(fe_size)
   /\ (forall r,
        In r float_callee_save_regs ->
        index_float_callee_save r < bound_float_callee_save b ->
@@ -899,55 +959,57 @@ Proof.
   exploit (save_callee_save_regs_correct fe_num_float_callee_save index_float_callee_save FI_saved_float
                                          Tfloat sp float_callee_save_regs).
   exact index_float_callee_save_inj.
-  intros. red. split; auto. generalize (index_float_callee_save_pos r H0). omega.
+  intros. red. split; auto. generalize (index_float_callee_save_pos r H). omega.
+  intro; congruence.
+  intro; congruence.
   auto.
   intros; congruence.
   intros until idx. destruct idx; simpl; auto. congruence.
   apply incl_refl.
   apply float_callee_save_norepet. eauto.
-  intros [fr' [A [B [C D]]]]. 
+  intros [fr' [A [B C]]]. 
   exists fr'; intuition. unfold save_callee_save_float; eauto. 
-  apply D. auto. intros; subst idx. auto.
+  apply C. auto. intros; subst idx. auto.
 Qed.
 
 Lemma save_callee_save_correct:
-  forall sp k rs fr m ls,
+  forall sp k rs m ls cs,
   (forall r, rs r = ls (R r)) ->
-  (forall ofs ty, 
-     14 <= ofs -> 
-     ofs + typesize ty <= size_arguments f.(Linear.fn_sig) ->
-     get_slot (parent_frame stack) ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) ->
-  fr.(fr_low) = - fe.(fe_size) ->
-  (forall idx, index_valid idx -> index_val idx fr = Vundef) ->
+  (forall ofs ty,
+     In (S (Outgoing ofs ty)) (loc_arguments f.(Linear.fn_sig)) ->
+     get_slot (parent_function cs) (parent_frame cs)
+              ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) ->
   exists fr',
     star step tge
-       (State stack tf sp (save_callee_save fe k) rs fr m)
+       (State stack tf sp (save_callee_save fe k) rs empty_frame m)
     E0 (State stack tf sp k rs fr' m)
-  /\ agree (LTL.call_regs ls) rs fr' (parent_frame stack) ls.
+  /\ agree (LTL.call_regs ls) ls rs fr' cs.
 Proof.
   intros. unfold save_callee_save.
   exploit save_callee_save_int_correct; eauto. 
-  intros [fr1 [A1 [B1 [C1 D1]]]].
-  exploit save_callee_save_float_correct. eexact B1. 
-  intros [fr2 [A2 [B2 [C2 D2]]]].
+  intros [fr1 [A1 [B1 C1]]].
+  exploit save_callee_save_float_correct. 
+  intros [fr2 [A2 [B2 C2]]].
   exists fr2.
   split. eapply star_trans. eexact A1. eexact A2. traceEq.
   constructor; unfold LTL.call_regs; auto.
   (* agree_local *)
-  intros. rewrite D2; auto with stacking. 
-  rewrite D1; auto with stacking. 
-  symmetry. auto with stacking.
+  intros. rewrite C2; auto with stacking. 
+  rewrite C1; auto with stacking. 
   (* agree_outgoing *)
-  intros. rewrite D2; auto with stacking. 
-  rewrite D1; auto with stacking. 
-  symmetry. auto with stacking. 
+  intros. rewrite C2; auto with stacking. 
+  rewrite C1; auto with stacking.
   (* agree_incoming *)
-  intros. simpl in H3. apply H0. tauto. tauto.
+  intros. apply H0. unfold loc_parameters in H1.
+  exploit list_in_map_inv; eauto. intros [l [A B]].
+  exploit loc_arguments_acceptable; eauto. intro C.
+  destruct l; simpl in A. discriminate.
+  simpl in C. destruct s; try contradiction. inv A. auto.
   (* agree_saved_int *)
-  intros. rewrite D2; auto with stacking.
-  rewrite C1; auto with stacking. 
+  intros. rewrite C2; auto with stacking.
+  rewrite B1; auto with stacking. 
   (* agree_saved_float *)
-  intros. rewrite C2; auto with stacking. 
+  intros. rewrite B2; auto with stacking. 
 Qed.
 
 (** The following lemmas show the correctness of the register reloading
@@ -965,21 +1027,25 @@ Variable sp: val.
 Variable csregs: list mreg.
 Hypothesis mkindex_valid:
   forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)).
+Hypothesis mkindex_not_link:
+  forall z, mkindex z <> FI_link.
+Hypothesis mkindex_not_retaddr:
+  forall z, mkindex z <> FI_retaddr.
 Hypothesis mkindex_typ:
   forall z, type_of_index (mkindex z) = ty.
 Hypothesis number_within_bounds:
   forall r, In r csregs ->
   (number r < bound fe <-> mreg_within_bounds b r).
 Hypothesis mkindex_val:
-  forall ls rs fr ls0 r, 
-  agree ls rs fr (parent_frame stack) ls0 -> In r csregs -> number r < bound fe ->
+  forall ls ls0 rs fr cs r, 
+  agree ls ls0 rs fr cs -> In r csregs -> number r < bound fe ->
   index_val (mkindex (number r)) fr = ls0 (R r).
 
 Lemma restore_callee_save_regs_correct:
-  forall k fr m ls0 l ls rs,
+  forall k fr m ls0 l ls rs cs,
   incl l csregs ->
   list_norepet l -> 
-  agree ls rs fr (parent_frame stack) ls0 ->
+  agree ls ls0 rs fr cs ->
   exists ls', exists rs',
     star step tge
       (State stack tf sp
@@ -987,7 +1053,7 @@ Lemma restore_callee_save_regs_correct:
    E0 (State stack tf sp k rs' fr m)
   /\ (forall r, In r l -> rs' r = ls0 (R r))
   /\ (forall r, ~(In r l) -> rs' r = rs r)
-  /\ agree ls' rs' fr (parent_frame stack) ls0.
+  /\ agree ls' ls0 rs' fr cs.
 Proof.
   induction l; intros; simpl restore_callee_save_regs.
   (* base case *)
@@ -1004,15 +1070,14 @@ Proof.
   destruct (zlt (number a) (bound fe)).
   set (ls1 := Locmap.set (R a) (ls0 (R a)) ls).
   set (rs1 := Regmap.set a (ls0 (R a)) rs).
-  assert (R3: agree ls1 rs1 fr (parent_frame stack) ls0). 
+  assert (R3: agree ls1 ls0 rs1 fr cs). 
     unfold ls1, rs1. apply agree_set_reg. auto. 
     rewrite <- number_within_bounds; auto. 
-  generalize (IHl ls1 rs1 R1 R2 R3). 
+  generalize (IHl ls1 rs1 cs R1 R2 R3). 
   intros [ls' [rs' [A [B [C D]]]]].
   exists ls'. exists rs'. split. 
   apply star_left with E0 (State stack tf sp k1 rs1 fr m) E0.
-  unfold rs1; apply exec_Mgetstack'; eauto with stacking.
-  apply get_slot_index; eauto with stacking.
+  unfold rs1; apply exec_Mgetstack. apply get_slot_index; auto. 
   symmetry. eapply mkindex_val; eauto.  
   auto. traceEq.
   split. intros. elim H2; intros.
@@ -1022,7 +1087,7 @@ Proof.
   apply sym_not_eq; tauto. tauto.
   assumption.
   (* no load takes place *)
-  generalize (IHl ls rs R1 R2 H1).  
+  generalize (IHl ls rs cs R1 R2 H1).  
   intros [ls' [rs' [A [B [C D]]]]].
   exists ls'; exists rs'. split. assumption.
   split. intros. elim H2; intros. 
@@ -1035,8 +1100,8 @@ Qed.
 End RESTORE_CALLEE_SAVE.
 
 Lemma restore_int_callee_save_correct:
-  forall sp k fr m ls0 ls rs,
-  agree ls rs fr (parent_frame stack) ls0 ->
+  forall sp k fr m ls0 ls rs cs,
+  agree ls ls0 rs fr cs ->
   exists ls', exists rs',
     star step tge
        (State stack tf sp
@@ -1044,11 +1109,13 @@ Lemma restore_int_callee_save_correct:
     E0 (State stack tf sp k rs' fr m)
   /\ (forall r, In r int_callee_save_regs -> rs' r = ls0 (R r))
   /\ (forall r, ~(In r int_callee_save_regs) -> rs' r = rs r)
-  /\ agree ls' rs' fr (parent_frame stack) ls0.
+  /\ agree ls' ls0 rs' fr cs.
 Proof.
   intros. unfold restore_callee_save_int.
   apply restore_callee_save_regs_correct with int_callee_save_regs ls.
   intros; simpl. split; auto. generalize (index_int_callee_save_pos r H0). omega.
+  intros; congruence.
+  intros; congruence.
   auto.
   intros. unfold mreg_within_bounds. 
   rewrite (int_callee_save_type r H0). tauto. 
@@ -1059,8 +1126,8 @@ Proof.
 Qed.
 
 Lemma restore_float_callee_save_correct:
-  forall sp k fr m ls0 ls rs,
-  agree ls rs fr (parent_frame stack) ls0 ->
+  forall sp k fr m ls0 ls rs cs,
+  agree ls ls0 rs fr cs ->
   exists ls', exists rs',
     star step tge
        (State stack tf sp
@@ -1068,11 +1135,13 @@ Lemma restore_float_callee_save_correct:
     E0 (State stack tf sp k rs' fr m)
   /\ (forall r, In r float_callee_save_regs -> rs' r = ls0 (R r))
   /\ (forall r, ~(In r float_callee_save_regs) -> rs' r = rs r)
-  /\ agree ls' rs' fr (parent_frame stack) ls0.
+  /\ agree ls' ls0 rs' fr cs.
 Proof.
   intros. unfold restore_callee_save_float.
   apply restore_callee_save_regs_correct with float_callee_save_regs ls.
   intros; simpl. split; auto. generalize (index_float_callee_save_pos r H0). omega.
+  intros; congruence.
+  intros; congruence.
   auto.
   intros. unfold mreg_within_bounds. 
   rewrite (float_callee_save_type r H0). tauto. 
@@ -1083,8 +1152,8 @@ Proof.
 Qed.
 
 Lemma restore_callee_save_correct:
-  forall sp k fr m ls0 ls rs,
-  agree ls rs fr (parent_frame stack) ls0 ->
+  forall sp k fr m ls0 ls rs cs,
+  agree ls ls0 rs fr cs ->
   exists rs',
     star step tge
        (State stack tf sp (restore_callee_save fe k) rs fr m)
@@ -1235,15 +1304,15 @@ Proof.
 Qed.
 
 Lemma find_function_translated:
-  forall f0 ls rs fr parent ls0 ros f,
-  agree f0 ls rs fr parent ls0 ->
+  forall f0 tf0 ls ls0 rs fr cs ros f,
+  agree f0 tf0 ls ls0 rs fr cs ->
   Linear.find_function ge ros ls = Some f ->
   exists tf,
   find_function tge ros rs = Some tf /\ transf_fundef f = OK tf.
 Proof.
   intros until f; intro AG.
   destruct ros; simpl.
-  rewrite (agree_eval_reg _ _ _ _ _ _ m AG). intro.
+  rewrite (agree_eval_reg _ _ _ _ _ _ _ m AG). intro.
   apply functions_translated; auto.
   rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence.
   intro. apply function_ptr_translated; auto.
@@ -1321,42 +1390,40 @@ Qed.
 
 Section EXTERNAL_ARGUMENTS.
 
+Variable f: function.
 Variable ls: locset.
 Variable fr: frame.
 Variable rs: regset.
 Variable sg: signature.
 Hypothesis AG1: forall r, rs r = ls (R r).
 Hypothesis AG2: forall (ofs : Z) (ty : typ),
-      14 <= ofs ->
-      ofs + typesize ty <= size_arguments sg ->
-      get_slot fr ty (Int.signed (Int.repr (4 * ofs)))
-                     (ls (S (Outgoing ofs ty))).
+      In (S (Outgoing ofs ty)) (loc_arguments sg) ->
+      get_slot f fr ty (Int.signed (Int.repr (4 * ofs)))
+                       (ls (S (Outgoing ofs ty))).
 
 Lemma transl_external_arguments_rec:
   forall locs,
-  (forall l, In l locs -> loc_argument_acceptable l) ->
-  (forall ofs ty, In (S (Outgoing ofs ty)) locs ->
-                  ofs + typesize ty <= size_arguments sg) ->
-  extcall_args rs fr locs ls##locs.
+  incl locs (loc_arguments sg) ->
+  extcall_args f rs fr locs ls##locs.
 Proof.
   induction locs; simpl; intros.
   constructor.
   constructor. 
-  assert (loc_argument_acceptable a). apply H; auto.
-  destruct a; red in H1.
+  assert (loc_argument_acceptable a). 
+    apply loc_arguments_acceptable with sg; auto with coqlib.
+  destruct a; red in H0.
   rewrite <- AG1. constructor. 
   destruct s; try contradiction.
-  constructor. apply AG2. omega. apply H0. auto.
-  apply IHlocs; auto.
+  constructor. apply AG2. auto with coqlib. 
+  apply IHlocs; eauto with coqlib.
 Qed.
 
 Lemma transl_external_arguments:
-  extcall_arguments rs fr sg (ls ## (loc_arguments sg)).
+  extcall_arguments f rs fr sg (ls ## (loc_arguments sg)).
 Proof.
   unfold extcall_arguments. 
-  apply transl_external_arguments_rec. 
-  exact (Conventions.loc_arguments_acceptable sg).
-  exact (Conventions.loc_arguments_bounded sg).
+  apply transl_external_arguments_rec.
+  auto with coqlib.
 Qed.
 
 End EXTERNAL_ARGUMENTS.
@@ -1390,7 +1457,7 @@ Inductive match_stacks: list Linear.stackframe -> list Machabstr.stackframe -> P
       match_stacks s ts ->
       transf_function f = OK tf ->
       wt_function f ->
-      agree_frame f ls fr (parent_frame ts) (parent_locset s) ->
+      agree_frame f tf ls (parent_locset s) fr ts ->
       incl c (Linear.fn_code f) ->
       match_stacks
        (Linear.Stackframe f sp ls c :: s)
@@ -1402,7 +1469,7 @@ Inductive match_states: Linear.state -> Machabstr.state -> Prop :=
         (STACKS: match_stacks s ts)
         (TRANSL: transf_function f = OK tf)
         (WTF: wt_function f)
-        (AG: agree f ls rs fr (parent_frame ts) (parent_locset s))
+        (AG: agree f tf ls (parent_locset s) rs fr ts)
         (INCL: incl c (Linear.fn_code f)),
       match_states (Linear.State s f sp c ls m)
                    (Machabstr.State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) rs fr m)
@@ -1413,9 +1480,8 @@ Inductive match_states: Linear.state -> Machabstr.state -> Prop :=
         (WTF: wt_fundef f)
         (AG1: forall r, rs r = ls (R r))
         (AG2: forall ofs ty, 
-                14 <= ofs -> 
-                ofs + typesize ty <= size_arguments (Linear.funsig f) ->
-                get_slot (parent_frame ts) ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty))))
+                In (S (Outgoing ofs ty)) (loc_arguments (Linear.funsig f)) ->
+                get_slot (parent_function ts) (parent_frame ts) ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty))))
         (AG3: agree_callee_save ls (parent_locset s)),
       match_states (Linear.Callstate s f ls m)
                    (Machabstr.Callstate ts tf rs m)
@@ -1450,17 +1516,15 @@ Proof.
              (rs0#r <- (rs (S sl))) fr m).
   split. destruct sl. 
   (* Lgetstack, local *)
-  apply plus_one. eapply exec_Mgetstack'; eauto.
-  apply get_slot_index. apply index_local_valid. auto. 
-  eapply agree_size; eauto. reflexivity. 
+  apply plus_one. apply exec_Mgetstack.
+  apply get_slot_index. auto. apply index_local_valid. auto. congruence. congruence. auto.
   eapply agree_locals; eauto.
   (* Lgetstack, incoming *)
   apply plus_one; apply exec_Mgetparam.
   unfold offset_of_index. eapply agree_incoming; eauto.
   (* Lgetstack, outgoing *)
-  apply plus_one; apply exec_Mgetstack'; eauto.
-  apply get_slot_index. apply index_arg_valid. auto. 
-  eapply agree_size; eauto. reflexivity. 
+  apply plus_one; apply exec_Mgetstack.
+  apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. 
   eapply agree_outgoing; eauto.
   (* Lgetstack, common *)
   econstructor; eauto with coqlib. 
@@ -1470,20 +1534,20 @@ Proof.
   inv WTI. destruct sl.
 
   (* Lsetstack, local *)
-  generalize (agree_set_local _ _ _ _ _ _ (rs0 r) _ _ AG BOUND).
+  generalize (agree_set_local _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND).
   intros [fr' [SET AG']].
   econstructor; split.
-  apply plus_one. eapply exec_Msetstack'; eauto.
+  apply plus_one. eapply exec_Msetstack; eauto.
   econstructor; eauto with coqlib.
   replace (rs (R r)) with (rs0 r). auto.
   symmetry. eapply agree_reg; eauto.
   (* Lsetstack, incoming *)
   contradiction.
   (* Lsetstack, outgoing *)
-  generalize (agree_set_outgoing _ _ _ _ _ _ (rs0 r) _ _ AG BOUND).
+  generalize (agree_set_outgoing _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND).
   intros [fr' [SET AG']].
   econstructor; split.
-  apply plus_one. eapply exec_Msetstack'; eauto.
+  apply plus_one. eapply exec_Msetstack; eauto.
   econstructor; eauto with coqlib.
   replace (rs (R r)) with (rs0 r). auto.
   symmetry. eapply agree_reg; eauto.
@@ -1493,7 +1557,7 @@ Proof.
   apply plus_one. apply exec_Mop. 
   apply shift_eval_operation. auto. 
   change mreg with RegEq.t.
-  rewrite (agree_eval_regs _ _ _ _ _ _ args AG). auto.
+  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). auto.
   econstructor; eauto with coqlib.
   apply agree_set_reg; auto.
 
@@ -1502,7 +1566,7 @@ Proof.
   apply plus_one; eapply exec_Mload; eauto.
   apply shift_eval_addressing; auto. 
   change mreg with RegEq.t.
-  rewrite (agree_eval_regs _ _ _ _ _ _ args AG). eauto.
+  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto.
   econstructor; eauto with coqlib.
   apply agree_set_reg; auto.
 
@@ -1511,8 +1575,8 @@ Proof.
   apply plus_one; eapply exec_Mstore; eauto.
   apply shift_eval_addressing; eauto. 
   change mreg with RegEq.t.
-  rewrite (agree_eval_regs _ _ _ _ _ _ args AG). eauto.
-  rewrite (agree_eval_reg _ _ _ _ _ _ src AG). eauto.
+  rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto.
+  rewrite (agree_eval_reg _ _ _ _ _ _ _ src AG). eauto.
   econstructor; eauto with coqlib.
 
   (* Lcall *) 
@@ -1525,24 +1589,24 @@ Proof.
   econstructor; eauto with coqlib.
   exists rs0; auto.
   intro. symmetry. eapply agree_reg; eauto.
-  intros. 
+  intros. unfold parent_function, parent_frame. 
   assert (slot_within_bounds f (function_bounds f) (Outgoing ofs ty)).
-  red. simpl. omega. 
+  red. simpl. generalize (loc_arguments_bounded _ _ _ H0). 
+  generalize (loc_arguments_acceptable _ _ H0). unfold loc_argument_acceptable. 
+  omega. 
   change (4 * ofs) with (offset_of_index (make_env (function_bounds f)) (FI_arg ofs ty)).
-  rewrite (offset_of_index_no_overflow f tf); auto. 
-  apply get_slot_index. apply index_arg_valid. auto. 
-  eapply agree_size; eauto. reflexivity. 
+  apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto.
   eapply agree_outgoing; eauto.
   simpl. red; auto.
 
   (* Ltailcall *) 
   assert (WTF': wt_fundef f'). eapply find_function_well_typed; eauto.
-  generalize (find_function_translated _ _ _ _ _ _ _ _ AG H). 
+  exploit find_function_translated; eauto. 
   intros [tf' [FIND' TRANSL']].
   generalize (restore_callee_save_correct ts _ _ TRANSL
                (shift_sp tf (Vptr stk Int.zero)) 
                (Mtailcall (Linear.funsig f') ros :: transl_code (make_env (function_bounds f)) b)
-               _ m _ _ _ AG).
+               _ m _ _ _ _ AG).
   intros [rs2 [A [B C]]].
   assert (FIND'': find_function tge ros rs2 = Some tf').
     rewrite <- FIND'. destruct ros; simpl; auto.
@@ -1553,15 +1617,14 @@ Proof.
   simpl shift_sp. eapply exec_Mtailcall; eauto. traceEq.
   econstructor; eauto. 
   intros; symmetry; eapply agree_return_regs; eauto.
-  intros. inv WTI. rewrite tailcall_possible_size in H4.
-  rewrite H4 in H1. elimtype False. generalize (typesize_pos ty). omega.
+  intros. inv WTI. generalize (H3 _ H0). tauto.
   apply agree_callee_save_return_regs. 
  
   (* Lalloc *)
   exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b)
                           (rs0#loc_alloc_result <- (Vptr blk Int.zero)) fr m'); split.
   apply plus_one; eapply exec_Malloc; eauto.
-  rewrite (agree_eval_reg _ _ _ _ _ _ loc_alloc_argument AG). auto.
+  rewrite (agree_eval_reg _ _ _ _ _ _ _ loc_alloc_argument AG). auto.
   econstructor; eauto with coqlib.
   apply agree_set_reg; auto.
   red. simpl. generalize (max_over_regs_of_funct_pos f int_callee_save). omega.
@@ -1581,7 +1644,7 @@ Proof.
   (* Lcond, true *)
   econstructor; split.
   apply plus_one; apply exec_Mcond_true.
-  rewrite <- (agree_eval_regs _ _ _ _ _ _ args AG) in H; eauto.
+  rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; eauto.
   apply transl_find_label; eauto.
   econstructor; eauto.
   eapply find_label_incl; eauto.
@@ -1589,7 +1652,7 @@ Proof.
   (* Lcond, false *)
   econstructor; split.
   apply plus_one; apply exec_Mcond_false.
-  rewrite <- (agree_eval_regs _ _ _ _ _ _ args AG) in H; auto.
+  rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; auto.
   econstructor; eauto with coqlib.
 
   (* Lreturn *)
@@ -1611,15 +1674,6 @@ Proof.
   set (sp := Vptr stk Int.zero) in *.
   set (tsp := shift_sp tfn sp).
   set (fe := make_env (function_bounds f)).
-  assert (fr_low (init_frame tfn) = - fe.(fe_size)).
-    simpl fr_low. rewrite (unfold_transf_function _ _ TRANSL).
-    reflexivity.
-  assert (UNDEF: forall idx, index_valid f idx -> index_val f idx (init_frame tfn) = Vundef).
-    intros.
-    assert (get_slot (init_frame tfn) (type_of_index idx) (offset_of_index fe idx) Vundef).
-    generalize (offset_of_index_valid _ _ H1). fold fe. intros [XX YY].
-    apply slot_gi; auto. omega. 
-    inv H2; auto.
   exploit save_callee_save_correct; eauto. 
   intros [fr [EXP AG]].
   econstructor; split.
@@ -1671,10 +1725,7 @@ Proof.
   rewrite (Genv.init_mem_transf_partial _ _ TRANSF).
   econstructor; eauto. constructor. 
   eapply Genv.find_funct_ptr_prop; eauto.
-  intros. 
-  replace (size_arguments (Linear.funsig f)) with 14 in H5.
-  elimtype False. generalize (typesize_pos ty). omega.
-  rewrite H2; auto.
+  intros. rewrite H2 in H4. simpl in H4. contradiction.
   simpl; red; auto.
 Qed.
 
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index aa534ff0..f3fe24f2 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -205,18 +205,33 @@ Proof.
   case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))); intro.
   intros; discriminate. intro EQ.
   generalize (unfold_transf_function f tf H); intro.
-  assert (fn_framesize tf = fe_size (make_env (function_bounds f))).
+  set (b := function_bounds f) in *.
+  set (fe := make_env b) in *.
+  assert (fn_framesize tf = fe_size fe).
     subst tf; reflexivity.
+  assert (Int.signed tf.(fn_link_ofs) = offset_of_index fe FI_link).
+    rewrite H1; unfold fn_link_ofs. 
+    change (fe_ofs_link fe) with (offset_of_index fe FI_link).
+    unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto. 
+  assert (Int.signed tf.(fn_retaddr_ofs) = offset_of_index fe FI_retaddr).
+    rewrite H1; unfold fn_retaddr_ofs. 
+    change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr).
+    unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto. 
   constructor.
   change (wt_instrs (fn_code tf)).
   rewrite H1; simpl; unfold transl_body. 
-  apply wt_save_callee_save; auto. 
+  unfold fe, b; apply wt_save_callee_save; auto. 
   unfold transl_code. apply wt_fold_right. 
   intros. eapply wt_transl_instr; eauto. 
-  red; intros. elim H3.
+  red; intros. elim H5.
   subst tf; simpl; auto.
-  rewrite H2. eapply size_pos; eauto.
-  rewrite H2. eapply size_no_overflow; eauto.
+  rewrite H2. generalize (size_pos f). fold b; fold fe; omega.
+  rewrite H3; rewrite H2. change 4 with (4 * typesize (type_of_index FI_link)).
+  unfold fe, b; apply offset_of_index_valid. red; auto.
+  rewrite H4; rewrite H2. change 4 with (4 * typesize (type_of_index FI_retaddr)).
+  unfold fe, b; apply offset_of_index_valid. red; auto.
+  rewrite H3; rewrite H4.
+  apply (offset_of_index_disj f FI_retaddr FI_link); red; auto.
 Qed.
 
 Lemma wt_transf_fundef: