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

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


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

1 files changed, 236 insertions, 278 deletions

diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 06b54073..324e1f79 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -139,6 +139,7 @@ Qed.
 
 Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree {
   agree_sp: rs#SP = sp;
+  agree_sp_def: sp <> Vundef;
   agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
 }.
 
@@ -185,7 +186,7 @@ Lemma agree_exten:
   (forall r, data_preg r = true -> rs'#r = rs#r) ->
   agree ms sp rs'.
 Proof.
-  intros. destruct H. split. 
+  intros. destruct H. split; auto.
   rewrite H0; auto. auto.
   intros. rewrite H0; auto. apply preg_of_data.
 Qed.
@@ -199,9 +200,8 @@ Lemma agree_set_mreg:
   (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
   agree (Regmap.set r v ms) sp rs'.
 Proof.
-  intros. destruct H. split.
+  intros. destruct H. split; auto.
   rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP.
-  auto.
   intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. 
   rewrite H1. auto. apply preg_of_data.
   red; intros; elim n. eapply preg_of_injective; eauto.
@@ -243,7 +243,7 @@ Lemma agree_exten_temps:
   (forall r, nontemp_preg r = true -> rs'#r = rs#r) ->
   agree (undef_temps ms) sp rs'.
 Proof.
-  intros. destruct H. split. 
+  intros. destruct H. split; auto.
   rewrite H0; auto. auto. 
   intros. unfold undef_temps. 
   destruct (In_dec mreg_eq r temporary_regs).
@@ -271,7 +271,7 @@ Lemma agree_change_sp:
   agree ms sp rs -> sp' <> Vundef ->
   agree ms sp' (rs#SP <- sp').
 Proof.
-  intros. inv H. split. apply Pregmap.gss. auto. 
+  intros. inv H. split; auto.
   intros. rewrite Pregmap.gso; auto with asmgen.
 Qed.
 
@@ -391,7 +391,16 @@ Proof.
   eauto.
 Qed.
 
-Remark code_tail_bounds:
+Remark code_tail_bounds_1:
+  forall fn ofs c,
+  code_tail ofs fn c -> 0 <= ofs <= list_length_z fn.
+Proof.
+  induction 1; intros; simpl.
+  generalize (list_length_z_pos c). omega. 
+  rewrite list_length_z_cons. omega.
+Qed.
+
+Remark code_tail_bounds_2:
   forall fn ofs i c,
   code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
 Proof.
@@ -425,23 +434,218 @@ Proof.
   intros. rewrite Int.add_unsigned.
   change (Int.unsigned Int.one) with 1.
   rewrite Int.unsigned_repr. apply code_tail_next with i; auto.
-  generalize (code_tail_bounds _ _ _ _ H0). omega. 
+  generalize (code_tail_bounds_2 _ _ _ _ H0). omega. 
 Qed.
 
-(** [transl_code_at_pc pc f c ep tf tc] holds if the code pointer [pc] points
+(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
   within the Asm code generated by translating Mach function [f],
   and [tc] is the tail of the generated code at the position corresponding
   to the code pointer [pc]. *)
 
 Inductive transl_code_at_pc (ge: Mach.genv):
-    val -> Mach.function -> Mach.code -> bool -> Asm.function -> Asm.code -> Prop :=
+    val -> block -> Mach.function -> Mach.code -> bool -> Asm.function -> Asm.code -> Prop :=
   transl_code_at_pc_intro:
     forall b ofs f c ep tf tc,
     Genv.find_funct_ptr ge b = Some(Internal f) ->
     transf_function f = Errors.OK tf ->
     transl_code f c ep = OK tc ->
     code_tail (Int.unsigned ofs) (fn_code tf) tc ->
-    transl_code_at_pc ge (Vptr b ofs) f c ep tf tc.
+    transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc.
+
+(** Predictor for return addresses in generated Asm code.
+
+  The [return_address_offset] predicate defined here is used in the
+  semantics for Mach to determine the return addresses that are
+  stored in activation records. *)
+
+(** Consider a Mach function [f] and a sequence [c] of Mach instructions
+  representing the Mach code that remains to be executed after a
+  function call returns.  The predicate [return_address_offset f c ofs]
+  holds if [ofs] is the integer offset of the PPC instruction
+  following the call in the Asm code obtained by translating the
+  code of [f]. Graphically:
+<<
+     Mach function f    |--------- Mcall ---------|
+         Mach code c    |                |--------|
+                        |                 \        \
+                        |                  \        \
+                        |                   \        \
+     Asm code           |                    |--------|
+     Asm function       |------------- Pcall ---------|
+
+                        <-------- ofs ------->
+>>
+*)
+
+Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: int) : Prop :=
+  forall tf tc,
+  transf_function f = OK tf ->
+  transl_code f c false = OK tc ->
+  code_tail (Int.unsigned ofs) (fn_code tf) tc.
+
+(** We now show that such an offset always exists if the Mach code [c]
+  is a suffix of [f.(fn_code)].  This holds because the translation
+  from Mach to PPC is compositional: each Mach instruction becomes
+  zero, one or several PPC instructions, but the order of instructions
+  is preserved. *)
+
+Lemma is_tail_code_tail:
+  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
+Proof.
+  induction 1. exists 0; constructor.
+  destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto.
+Qed.
+
+Section RETADDR_EXISTS.
+
+Hypothesis transl_instr_tail:
+  forall f i ep k c, transl_instr f i ep k = OK c -> is_tail k c.
+Hypothesis transf_function_inv:
+  forall f tf, transf_function f = OK tf ->
+  exists tc, exists ep, transl_code f (Mach.fn_code f) ep = OK tc /\ is_tail tc (fn_code tf).
+Hypothesis transf_function_len:
+  forall f tf, transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned.
+
+Lemma transl_code_tail: 
+  forall f c1 c2, is_tail c1 c2 ->
+  forall tc2 ep2, transl_code f c2 ep2 = OK tc2 ->
+  exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2.
+Proof.
+  induction 1; simpl; intros.
+  exists tc2; exists ep2; split; auto with coqlib.
+  monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]].
+  exists tc1; exists ep1; split. auto. 
+  apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto.
+Qed.
+
+Lemma return_address_exists:
+  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. destruct (transf_function f) as [tf|] eqn:TF.
++ exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1).
+  exploit transl_code_tail; eauto. intros (tc2 & ep2 & TR2 & TL2).
+Opaque transl_instr.
+  monadInv TR2. 
+  assert (TL3: is_tail x (fn_code tf)).
+  { apply is_tail_trans with tc1; auto. 
+    apply is_tail_trans with tc2; auto.
+    eapply transl_instr_tail; eauto. }
+  exploit is_tail_code_tail. eexact TL3. intros [ofs CT].
+  exists (Int.repr ofs). red; intros. 
+  rewrite Int.unsigned_repr. congruence. 
+  exploit code_tail_bounds_1; eauto.
+  apply transf_function_len in TF. omega. 
++ exists Int.zero; red; intros. congruence. 
+Qed.
+
+End RETADDR_EXISTS.
+
+Remark code_tail_no_bigger:
+  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
+Proof.
+  induction 1; simpl; omega.
+Qed.
+
+Remark code_tail_unique:
+  forall fn c pos pos',
+  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
+Proof.
+  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  f_equal. eauto.
+Qed.
+
+Lemma return_address_offset_correct:
+  forall ge b ofs fb f c tf tc ofs',
+  transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc ->
+  return_address_offset f c ofs' ->
+  ofs' = ofs.
+Proof.
+  intros. inv H. red in H0.  
+  exploit code_tail_unique. eexact H12. eapply H0; eauto. intro.
+  rewrite <- (Int.repr_unsigned ofs). 
+  rewrite <- (Int.repr_unsigned ofs').
+  congruence.
+Qed.
+
+(** The [find_label] function returns the code tail starting at the
+  given label.  A connection with [code_tail] is then established. *)
+
+Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
+  match c with
+  | nil => None
+  | instr :: c' =>
+      if is_label lbl instr then Some c' else find_label lbl c'
+  end.
+
+Lemma label_pos_code_tail:
+  forall lbl c pos c',
+  find_label lbl c = Some c' ->
+  exists pos',
+  label_pos lbl pos c = Some pos' 
+  /\ code_tail (pos' - pos) c c'
+  /\ pos < pos' <= pos + list_length_z c.
+Proof.
+  induction c. 
+  simpl; intros. discriminate.
+  simpl; intros until c'.
+  case (is_label lbl a).
+  intro EQ; injection EQ; intro; subst c'.
+  exists (pos + 1). split. auto. split.
+  replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. 
+  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. 
+  intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
+  exists pos'. split. auto. split.
+  replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
+  constructor. auto. 
+  rewrite list_length_z_cons. omega.
+Qed.
+
+(** Helper lemmas to reason about 
+- the "code is tail of" property
+- correct translation of labels. *)
+
+Definition tail_nolabel (k c: code) : Prop := is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k.
+
+Lemma tail_nolabel_refl:
+  forall c, tail_nolabel c c.
+Proof.
+  intros; split. apply is_tail_refl. auto.
+Qed.
+
+Lemma tail_nolabel_trans:
+  forall c1 c2 c3, tail_nolabel c1 c2 -> tail_nolabel c2 c3 -> tail_nolabel c1 c3.
+Proof.
+  intros. destruct H; destruct H0; split. 
+  eapply is_tail_trans; eauto.
+  intros. rewrite H2; auto.
+Qed.
+
+Lemma tail_nolabel_cons:
+  forall i c k,
+  match i with Plabel _ => False | _ => True end ->
+  tail_nolabel k c -> tail_nolabel k (i :: c).
+Proof.
+  intros. destruct H0. split. 
+  constructor; auto.
+  intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
+Qed.
+
+Hint Resolve tail_nolabel_refl: labels.
+
+Ltac TailNoLabels :=
+  eauto with labels;
+  match goal with
+  | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [exact I | TailNoLabels]
+  | [ H: Error _ = OK _ |- _ ] => discriminate
+  | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabels
+  | [ H: bind _ _ = OK _ |- _ ] => monadInv H;  TailNoLabels
+  | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabels
+  | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabels
+  | _ => idtac
+  end.
 
 (** * Execution of straight-line code *)
 
@@ -558,287 +762,41 @@ Qed.
 
 End STRAIGHTLINE.
 
-(** * Stack invariants *)
-
-(** ** Stored return addresses *)
-
-(** [retaddr_stored_at m m' sp pos ra] holds if Asm memory [m']
-  contains value [ra] (a return address) at offset [pos] in block [sp]. *)
-
-Record retaddr_stored_at (m m': mem) (sp: block) (pos: Z) (ra: val) : Prop := {
-  rsa_noperm:
-    forall ofs k p, pos <= ofs < pos + 4 -> ~Mem.perm m sp ofs k p;
-  rsa_allperm:
-    forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p;
-  rsa_contains:
-    Mem.load Mint32 m' sp pos = Some ra
-}.
-
-Lemma retaddr_stored_at_invariant:
-  forall m m' sp pos ra m1 m1',
-  retaddr_stored_at m m' sp pos ra ->
-  (forall ofs p, pos <= ofs < pos + 4 -> Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) ->
-  (forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p -> Mem.perm m1' sp ofs k p) ->
-  (Mem.load Mint32 m' sp pos = Some ra -> Mem.load Mint32 m1' sp pos = Some ra) ->
-  retaddr_stored_at m1 m1' sp pos ra.
-Proof.
-  intros. inv H. constructor; intros.
-  red; intros. eelim rsa_noperm0. eauto. apply H0. auto. eapply Mem.perm_max; eauto.  
-  eauto.
-  eauto.
-Qed.
-
-Lemma retaddr_stored_at_store:
-  forall chunk m m' b ofs v v' m1 m1' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.store chunk m b ofs v = Some m1 ->
-  Mem.store chunk m' b ofs v' = Some m1' ->
-  retaddr_stored_at m1 m1' sp pos ra.
-Proof.
-  intros. eapply retaddr_stored_at_invariant; eauto; intros.
-- eapply Mem.perm_store_2; eauto.
-- eapply Mem.perm_store_1; eauto.
-- rewrite <- H2. eapply Mem.load_store_other; eauto.
-  destruct (eq_block sp b); auto. subst b.
-  right. exploit Mem.store_valid_access_3. eexact H0. intros [A B].
-  apply (Intv.range_disjoint' (pos, pos + size_chunk Mint32) (ofs, ofs + size_chunk chunk)).
-  red; intros; red; intros. 
-  elim (rsa_noperm _ _ _ _ _ H x Cur Writable). assumption. apply A. assumption.
-  simpl; omega.
-  simpl; generalize (size_chunk_pos chunk); omega.
-Qed.
-
-Lemma retaddr_stored_at_storev:
-  forall chunk m m' a a' v v' m1 m1' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.storev chunk m a v = Some m1 ->
-  Mem.storev chunk m' a' v' = Some m1' ->
-  Val.lessdef a a' ->
-  retaddr_stored_at m1 m1' sp pos ra.
-Proof.
-  intros. destruct a; simpl in H0; try discriminate. inv H2. simpl in H1.
-  eapply retaddr_stored_at_store; eauto.
-Qed.
-
-Lemma retaddr_stored_at_valid':
-  forall m m' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.valid_block m' sp.
-Proof.
-  intros.
-  eapply Mem.valid_access_valid_block. 
-  apply Mem.valid_access_implies with Readable; auto with mem.
-  eapply Mem.load_valid_access.
-  eapply rsa_contains; eauto.
-Qed.
-
-Lemma retaddr_stored_at_valid:
-  forall m m' sp pos ra,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.extends m m' ->
-  Mem.valid_block m sp.
-Proof.
-  intros.
-  erewrite Mem.valid_block_extends; eauto.
-  eapply retaddr_stored_at_valid'; eauto.
-Qed.
-
-Lemma retaddr_stored_at_extcall:
-  forall m1 m1' sp pos ra m2 m2',
-  retaddr_stored_at m1 m1' sp pos ra ->
-  (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  mem_unchanged_on (loc_out_of_bounds m1) m1' m2' ->
-  Mem.extends m1 m1' ->
-  retaddr_stored_at m2 m2' sp pos ra.
-Proof.
-  intros.
-  assert (B: forall ofs, pos <= ofs < pos + 4 -> loc_out_of_bounds m1 sp ofs).
-    intros; red; intros. eapply rsa_noperm; eauto.
-  eapply retaddr_stored_at_invariant; eauto. 
-- intros. apply H0; auto. eapply retaddr_stored_at_valid; eauto. 
-- intros. destruct H1. eauto. 
-- intros. destruct H1. apply H4; auto. 
-Qed.
-
-Lemma retaddr_stored_at_can_alloc:
-  forall m lo hi m1 sp pos m2 a v m3 m' m1' a' v' m2' ra,
-  Mem.alloc m lo hi = (m1, sp) ->
-  Mem.free m1 sp pos (pos + 4) = Some m2 ->
-  Mem.storev Mint32 m2 a v = Some m3 ->
-  Mem.alloc m' lo hi = (m1', sp) ->
-  Mem.storev Mint32 m1' a' v' = Some m2' ->
-  (4 | pos) ->
-  Mem.extends m3 m2' ->
-  Val.has_type ra Tint ->
-  exists m3',
-     Mem.store Mint32 m2' sp pos ra = Some m3'
-  /\ retaddr_stored_at m3 m3' sp pos ra
-  /\ Mem.extends m3 m3'.
-Proof.
-  intros. destruct a; simpl in H1; try discriminate. destruct a'; simpl in H3; try discriminate.
-  assert (POS: forall ofs, pos <= ofs < pos + 4 -> lo <= ofs < hi).
-    intros. eapply Mem.perm_alloc_3. eexact H. eapply Mem.free_range_perm; eauto.
-  assert (ST: { m3' | Mem.store Mint32 m2' sp pos ra = Some m3' }).
-  {
-    apply Mem.valid_access_store. split.
-    red; intros. eapply Mem.perm_store_1; eauto.
-    apply Mem.perm_implies with Freeable; auto with mem.
-    eapply Mem.perm_alloc_2; eauto.
-    assumption.
-  }
-  destruct ST as [m3' ST]. exists m3'; split; auto.
-  split. constructor.
-  intros; red; intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto.
-  intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. 
-  apply Mem.perm_implies with Freeable; auto with mem.
-  eapply Mem.perm_alloc_2; eauto.
-  replace ra with (Val.load_result Mint32 ra). eapply Mem.load_store_same; eauto.
-  destruct ra; reflexivity || contradiction.
-  eapply Mem.store_outside_extends; eauto. 
-  intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto.  
-Qed.
-
-Lemma retaddr_stored_at_can_free:
-  forall m m' sp pos ra lo m1 hi m2,
-  retaddr_stored_at m m' sp pos ra ->
-  Mem.free m sp lo pos = Some m1 ->
-  Mem.free m1 sp (pos + 4) hi = Some m2 ->
-  Mem.extends m m' ->
-  exists m1', Mem.free m' sp lo hi = Some m1' /\ Mem.extends m2 m1'.
-Proof.
-  intros. inv H.
-  assert (F: { m1' | Mem.free m' sp lo hi = Some m1' }).
-  {
-    apply Mem.range_perm_free. red; intros. 
-    assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega.
-    destruct EITHER as [A | [A | A]].
-    eapply Mem.perm_extends; eauto. eapply Mem.free_range_perm; eauto.
-    auto.
-    eapply Mem.perm_extends; eauto.
-    eapply Mem.perm_free_3; eauto. eapply Mem.free_range_perm; eauto.
-  }
-  destruct F as [m1' F]. exists m1'; split; auto.
-  eapply Mem.free_right_extends; eauto.
-  eapply Mem.free_left_extends. eapply Mem.free_left_extends. eauto. eauto. eauto. 
-  intros. 
-  exploit Mem.perm_free_3. eexact H1. eauto. intros P1.
-  exploit Mem.perm_free_3. eexact H0. eauto. intros P0.
-  assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega.
-  destruct EITHER as [A | [A | A]].
-  eelim Mem.perm_free_2. eexact H0. eexact A. eauto. 
-  eelim rsa_noperm0; eauto.
-  eelim Mem.perm_free_2. eexact H1. eexact A. eauto. 
-Qed.
-
-Lemma retaddr_stored_at_type:
-  forall m m' sp pos ra, retaddr_stored_at m m' sp pos ra -> Val.has_type ra Tint.
-Proof.
-  intros. change Tint with (type_of_chunk Mint32). 
-  eapply Mem.load_type. eapply rsa_contains; eauto.
-Qed.
-
-(** Matching a Mach stack against an Asm memory state. *)
+(** * Properties of the Mach call stack *)
 
 Section MATCH_STACK.
 
 Variable ge: Mach.genv.
 
-Inductive match_stack:
-           list Mach.stackframe -> mem -> mem -> val -> block -> Prop :=
-  | match_stack_nil: forall m m' bound,
-      match_stack nil m m' Vzero bound
-  | match_stack_cons: forall f sp c s m m' ra tf tc ra' bound
-      (AT: transl_code_at_pc ge ra f c false tf tc)
-      (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra')
-      (BELOW: sp < bound),
-      match_stack s m m' ra' sp ->
-      match_stack (Stackframe f (Vptr sp Int.zero) c :: s) m m' ra bound.
+Inductive match_stack: list Mach.stackframe -> Prop :=
+  | match_stack_nil:
+      match_stack nil
+  | match_stack_cons: forall fb sp ra c s f tf tc,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      transl_code_at_pc ge ra fb f c false tf tc ->
+      sp <> Vundef ->
+      match_stack s ->
+      match_stack (Stackframe fb sp ra c :: s).
 
-Lemma match_stack_invariant:
-  forall m2 m2' s m1 m1' ra bound,
-  match_stack s m1 m1' ra bound ->
-  (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  (forall b ofs k p, b < bound -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) ->
-  (forall b ofs v, b < bound -> Mem.load Mint32 m1' b ofs = Some v -> Mem.load Mint32 m2' b ofs = Some v) ->
-  match_stack s m2 m2' ra bound.
-Proof.
-  induction 1; intros; econstructor; eauto.
-  eapply retaddr_stored_at_invariant; eauto.
-  apply IHmatch_stack; intros. 
-  eapply H0; eauto. omega.
-  eapply H1; eauto. omega.
-  eapply H2; eauto. omega.
-Qed.
+Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
+Proof. induction 1; simpl. congruence. auto. Qed.
 
-Lemma match_stack_change_bound:
-  forall s m m' ra bound1 bound2,
-  match_stack s m m' ra bound1 ->
-  bound1 <= bound2 ->
-  match_stack s m m' ra bound2.
-Proof.
-  intros. inv H; econstructor; eauto. omega. 
-Qed.
+Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
+Proof. induction 1; simpl. unfold Vzero. congruence. inv H0. congruence. Qed.
 
-Lemma match_stack_storev:
-  forall chunk a v m1 a' v' m1' s m m' ra bound,
-  match_stack s m m' ra bound ->
-  Mem.storev chunk m a v = Some m1 ->
-  Mem.storev chunk m' a' v' = Some m1' ->
-  Val.lessdef a a' ->
-  match_stack s m1 m1' ra bound.
-Proof.
-  induction 1; intros; econstructor; eauto. 
-  eapply retaddr_stored_at_storev; eauto.
-Qed.
-
-Lemma match_stack_extcall:
-  forall m2 m2' s m1 m1' ra bound,
-  match_stack s m1 m1' ra bound ->
-  (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) ->
-  mem_unchanged_on (loc_out_of_bounds m1) m1' m2' ->
-  Mem.extends m1 m1' ->
-  match_stack s m2 m2' ra bound.
-Proof.
-  induction 1; intros; econstructor; eauto.
-  eapply retaddr_stored_at_extcall; eauto. 
-Qed.
-
-Lemma match_stack_free_left:
-  forall s m m' ra bound b lo hi m1,
-  match_stack s m m' ra bound ->
-  Mem.free m b lo hi = Some m1 ->
-  match_stack s m1 m' ra bound.
-Proof.
-  intros. eapply match_stack_invariant; eauto.
-  intros. eapply Mem.perm_free_3; eauto. 
-Qed.
-
-Lemma match_stack_free_right:
-  forall s m m' ra bound b lo hi m1',
-  match_stack s m m' ra bound ->
-  Mem.free m' b lo hi = Some m1' ->
-  bound <= b ->
-  match_stack s m m1' ra bound.
-Proof.
-  intros. eapply match_stack_invariant; eauto.
-  intros. eapply Mem.perm_free_1; eauto. left. unfold block; omega. 
-  intros. rewrite <- H3. eapply Mem.load_free; eauto. left. unfold block; omega.
-Qed.
-
-Lemma parent_sp_def:
-  forall s m m' ra bound,
-  match_stack s m m' ra bound -> parent_sp s <> Vundef.
+Lemma lessdef_parent_sp:
+  forall s v,
+  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
 Proof.
-  intros. inv H; simpl; congruence.
+  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
 Qed.
 
-Lemma lessdef_parent_sp:
-  forall s m m' ra bound v,
-  match_stack s m m' ra bound -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
+Lemma lessdef_parent_ra:
+  forall s v,
+  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
 Proof.
-  intros. inv H0; auto. exfalso. eelim parent_sp_def; eauto.
+  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
 Qed.
 
 End MATCH_STACK.
 
-