From 6acc8ded7cd7e6605fcf27bdbd209d94571f45f4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 3 Mar 2013 21:35:23 +0000 Subject: 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 --- backend/Asmgenproof0.v | 514 +++++++++++++++++++++++-------------------------- 1 file changed, 236 insertions(+), 278 deletions(-) (limited to 'backend/Asmgenproof0.v') 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. - -- cgit