diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-03 21:35:23 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-03 21:35:23 +0000 |
| commit | 6acc8ded7cd7e6605fcf27bdbd209d94571f45f4 (patch) | |
| tree | c8a6cfbb481adaab445988e5df223dbca751456a | |
| parent | d2ab3d934a3ae059422b12849fc1ca02d54ba7b8 (diff) | |
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
| -rw-r--r-- | Changelog | 1 | ||||
| -rw-r--r-- | backend/Asmgenproof0.v | 514 | ||||
| -rw-r--r-- | backend/Mach.v | 137 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 445 | ||||
| -rw-r--r-- | driver/Compiler.v | 3 | ||||
| -rw-r--r-- | ia32/Asm.v | 2 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 512 |
7 files changed, 757 insertions, 857 deletions
@@ -13,7 +13,6 @@ Development version - Arguments to __builtin_annot() that are compile-time constants are now replaced by their (integer or float) value in the annotation generated in the assembly file. -- Revised handling of return addresses in the Stacking and Asmgen passes. - ARM and PowerPC ports: more efficient access to function parameters that are passed on the call stack. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 06b5407..324e1f7 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -139,6 +139,7 @@ Qed. Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { agree_sp: rs#SP = sp; + agree_sp_def: sp <> Vundef; agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) }. @@ -185,7 +186,7 @@ Lemma agree_exten: (forall r, data_preg r = true -> rs'#r = rs#r) -> agree ms sp rs'. Proof. - intros. destruct H. split. + intros. destruct H. split; auto. rewrite H0; auto. auto. intros. rewrite H0; auto. apply preg_of_data. Qed. @@ -199,9 +200,8 @@ Lemma agree_set_mreg: (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> agree (Regmap.set r v ms) sp rs'. Proof. - intros. destruct H. split. + intros. destruct H. split; auto. rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP. - auto. intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. rewrite H1. auto. apply preg_of_data. red; intros; elim n. eapply preg_of_injective; eauto. @@ -243,7 +243,7 @@ Lemma agree_exten_temps: (forall r, nontemp_preg r = true -> rs'#r = rs#r) -> agree (undef_temps ms) sp rs'. Proof. - intros. destruct H. split. + intros. destruct H. split; auto. rewrite H0; auto. auto. intros. unfold undef_temps. destruct (In_dec mreg_eq r temporary_regs). @@ -271,7 +271,7 @@ Lemma agree_change_sp: agree ms sp rs -> sp' <> Vundef -> agree ms sp' (rs#SP <- sp'). Proof. - intros. inv H. split. apply Pregmap.gss. auto. + intros. inv H. split; auto. intros. rewrite Pregmap.gso; auto with asmgen. Qed. @@ -391,7 +391,16 @@ Proof. eauto. Qed. -Remark code_tail_bounds: +Remark code_tail_bounds_1: + forall fn ofs c, + code_tail ofs fn c -> 0 <= ofs <= list_length_z fn. +Proof. + induction 1; intros; simpl. + generalize (list_length_z_pos c). omega. + rewrite list_length_z_cons. omega. +Qed. + +Remark code_tail_bounds_2: forall fn ofs i c, code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn. Proof. @@ -425,23 +434,218 @@ Proof. intros. rewrite Int.add_unsigned. change (Int.unsigned Int.one) with 1. rewrite Int.unsigned_repr. apply code_tail_next with i; auto. - generalize (code_tail_bounds _ _ _ _ H0). omega. + generalize (code_tail_bounds_2 _ _ _ _ H0). omega. Qed. -(** [transl_code_at_pc pc f c ep tf tc] holds if the code pointer [pc] points +(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points within the Asm code generated by translating Mach function [f], and [tc] is the tail of the generated code at the position corresponding to the code pointer [pc]. *) Inductive transl_code_at_pc (ge: Mach.genv): - val -> Mach.function -> Mach.code -> bool -> Asm.function -> Asm.code -> Prop := + val -> block -> Mach.function -> Mach.code -> bool -> Asm.function -> Asm.code -> Prop := transl_code_at_pc_intro: forall b ofs f c ep tf tc, Genv.find_funct_ptr ge b = Some(Internal f) -> transf_function f = Errors.OK tf -> transl_code f c ep = OK tc -> code_tail (Int.unsigned ofs) (fn_code tf) tc -> - transl_code_at_pc ge (Vptr b ofs) f c ep tf tc. + transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. + +(** Predictor for return addresses in generated Asm code. + + The [return_address_offset] predicate defined here is used in the + semantics for Mach to determine the return addresses that are + stored in activation records. *) + +(** Consider a Mach function [f] and a sequence [c] of Mach instructions + representing the Mach code that remains to be executed after a + function call returns. The predicate [return_address_offset f c ofs] + holds if [ofs] is the integer offset of the PPC instruction + following the call in the Asm code obtained by translating the + code of [f]. Graphically: +<< + Mach function f |--------- Mcall ---------| + Mach code c | |--------| + | \ \ + | \ \ + | \ \ + Asm code | |--------| + Asm function |------------- Pcall ---------| + + <-------- ofs -------> +>> +*) + +Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: int) : Prop := + forall tf tc, + transf_function f = OK tf -> + transl_code f c false = OK tc -> + code_tail (Int.unsigned ofs) (fn_code tf) tc. + +(** We now show that such an offset always exists if the Mach code [c] + is a suffix of [f.(fn_code)]. This holds because the translation + from Mach to PPC is compositional: each Mach instruction becomes + zero, one or several PPC instructions, but the order of instructions + is preserved. *) + +Lemma is_tail_code_tail: + forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1. +Proof. + induction 1. exists 0; constructor. + destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto. +Qed. + +Section RETADDR_EXISTS. + +Hypothesis transl_instr_tail: + forall f i ep k c, transl_instr f i ep k = OK c -> is_tail k c. +Hypothesis transf_function_inv: + forall f tf, transf_function f = OK tf -> + exists tc, exists ep, transl_code f (Mach.fn_code f) ep = OK tc /\ is_tail tc (fn_code tf). +Hypothesis transf_function_len: + forall f tf, transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned. + +Lemma transl_code_tail: + forall f c1 c2, is_tail c1 c2 -> + forall tc2 ep2, transl_code f c2 ep2 = OK tc2 -> + exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2. +Proof. + induction 1; simpl; intros. + exists tc2; exists ep2; split; auto with coqlib. + monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]]. + exists tc1; exists ep1; split. auto. + apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto. +Qed. + +Lemma return_address_exists: + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, return_address_offset f c ra. +Proof. + intros. destruct (transf_function f) as [tf|] eqn:TF. ++ exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1). + exploit transl_code_tail; eauto. intros (tc2 & ep2 & TR2 & TL2). +Opaque transl_instr. + monadInv TR2. + assert (TL3: is_tail x (fn_code tf)). + { apply is_tail_trans with tc1; auto. + apply is_tail_trans with tc2; auto. + eapply transl_instr_tail; eauto. } + exploit is_tail_code_tail. eexact TL3. intros [ofs CT]. + exists (Int.repr ofs). red; intros. + rewrite Int.unsigned_repr. congruence. + exploit code_tail_bounds_1; eauto. + apply transf_function_len in TF. omega. ++ exists Int.zero; red; intros. congruence. +Qed. + +End RETADDR_EXISTS. + +Remark code_tail_no_bigger: + forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. +Proof. + induction 1; simpl; omega. +Qed. + +Remark code_tail_unique: + forall fn c pos pos', + code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. +Proof. + induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + f_equal. eauto. +Qed. + +Lemma return_address_offset_correct: + forall ge b ofs fb f c tf tc ofs', + transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc -> + return_address_offset f c ofs' -> + ofs' = ofs. +Proof. + intros. inv H. red in H0. + exploit code_tail_unique. eexact H12. eapply H0; eauto. intro. + rewrite <- (Int.repr_unsigned ofs). + rewrite <- (Int.repr_unsigned ofs'). + congruence. +Qed. + +(** The [find_label] function returns the code tail starting at the + given label. A connection with [code_tail] is then established. *) + +Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := + match c with + | nil => None + | instr :: c' => + if is_label lbl instr then Some c' else find_label lbl c' + end. + +Lemma label_pos_code_tail: + forall lbl c pos c', + find_label lbl c = Some c' -> + exists pos', + label_pos lbl pos c = Some pos' + /\ code_tail (pos' - pos) c c' + /\ pos < pos' <= pos + list_length_z c. +Proof. + induction c. + simpl; intros. discriminate. + simpl; intros until c'. + case (is_label lbl a). + intro EQ; injection EQ; intro; subst c'. + exists (pos + 1). split. auto. split. + replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. + rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. + intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. + exists pos'. split. auto. split. + replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. + constructor. auto. + rewrite list_length_z_cons. omega. +Qed. + +(** Helper lemmas to reason about +- the "code is tail of" property +- correct translation of labels. *) + +Definition tail_nolabel (k c: code) : Prop := is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k. + +Lemma tail_nolabel_refl: + forall c, tail_nolabel c c. +Proof. + intros; split. apply is_tail_refl. auto. +Qed. + +Lemma tail_nolabel_trans: + forall c1 c2 c3, tail_nolabel c1 c2 -> tail_nolabel c2 c3 -> tail_nolabel c1 c3. +Proof. + intros. destruct H; destruct H0; split. + eapply is_tail_trans; eauto. + intros. rewrite H2; auto. +Qed. + +Lemma tail_nolabel_cons: + forall i c k, + match i with Plabel _ => False | _ => True end -> + tail_nolabel k c -> tail_nolabel k (i :: c). +Proof. + intros. destruct H0. split. + constructor; auto. + intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction. +Qed. + +Hint Resolve tail_nolabel_refl: labels. + +Ltac TailNoLabels := + eauto with labels; + match goal with + | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [exact I | TailNoLabels] + | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabels + | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabels + | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabels + | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabels + | _ => idtac + end. (** * Execution of straight-line code *) @@ -558,287 +762,41 @@ Qed. End STRAIGHTLINE. -(** * Stack invariants *) - -(** ** Stored return addresses *) - -(** [retaddr_stored_at m m' sp pos ra] holds if Asm memory [m'] - contains value [ra] (a return address) at offset [pos] in block [sp]. *) - -Record retaddr_stored_at (m m': mem) (sp: block) (pos: Z) (ra: val) : Prop := { - rsa_noperm: - forall ofs k p, pos <= ofs < pos + 4 -> ~Mem.perm m sp ofs k p; - rsa_allperm: - forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p; - rsa_contains: - Mem.load Mint32 m' sp pos = Some ra -}. - -Lemma retaddr_stored_at_invariant: - forall m m' sp pos ra m1 m1', - retaddr_stored_at m m' sp pos ra -> - (forall ofs p, pos <= ofs < pos + 4 -> Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> - (forall ofs k p, pos <= ofs < pos + 4 -> Mem.perm m' sp ofs k p -> Mem.perm m1' sp ofs k p) -> - (Mem.load Mint32 m' sp pos = Some ra -> Mem.load Mint32 m1' sp pos = Some ra) -> - retaddr_stored_at m1 m1' sp pos ra. -Proof. - intros. inv H. constructor; intros. - red; intros. eelim rsa_noperm0. eauto. apply H0. auto. eapply Mem.perm_max; eauto. - eauto. - eauto. -Qed. - -Lemma retaddr_stored_at_store: - forall chunk m m' b ofs v v' m1 m1' sp pos ra, - retaddr_stored_at m m' sp pos ra -> - Mem.store chunk m b ofs v = Some m1 -> - Mem.store chunk m' b ofs v' = Some m1' -> - retaddr_stored_at m1 m1' sp pos ra. -Proof. - intros. eapply retaddr_stored_at_invariant; eauto; intros. -- eapply Mem.perm_store_2; eauto. -- eapply Mem.perm_store_1; eauto. -- rewrite <- H2. eapply Mem.load_store_other; eauto. - destruct (eq_block sp b); auto. subst b. - right. exploit Mem.store_valid_access_3. eexact H0. intros [A B]. - apply (Intv.range_disjoint' (pos, pos + size_chunk Mint32) (ofs, ofs + size_chunk chunk)). - red; intros; red; intros. - elim (rsa_noperm _ _ _ _ _ H x Cur Writable). assumption. apply A. assumption. - simpl; omega. - simpl; generalize (size_chunk_pos chunk); omega. -Qed. - -Lemma retaddr_stored_at_storev: - forall chunk m m' a a' v v' m1 m1' sp pos ra, - retaddr_stored_at m m' sp pos ra -> - Mem.storev chunk m a v = Some m1 -> - Mem.storev chunk m' a' v' = Some m1' -> - Val.lessdef a a' -> - retaddr_stored_at m1 m1' sp pos ra. -Proof. - intros. destruct a; simpl in H0; try discriminate. inv H2. simpl in H1. - eapply retaddr_stored_at_store; eauto. -Qed. - -Lemma retaddr_stored_at_valid': - forall m m' sp pos ra, - retaddr_stored_at m m' sp pos ra -> - Mem.valid_block m' sp. -Proof. - intros. - eapply Mem.valid_access_valid_block. - apply Mem.valid_access_implies with Readable; auto with mem. - eapply Mem.load_valid_access. - eapply rsa_contains; eauto. -Qed. - -Lemma retaddr_stored_at_valid: - forall m m' sp pos ra, - retaddr_stored_at m m' sp pos ra -> - Mem.extends m m' -> - Mem.valid_block m sp. -Proof. - intros. - erewrite Mem.valid_block_extends; eauto. - eapply retaddr_stored_at_valid'; eauto. -Qed. - -Lemma retaddr_stored_at_extcall: - forall m1 m1' sp pos ra m2 m2', - retaddr_stored_at m1 m1' sp pos ra -> - (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - mem_unchanged_on (loc_out_of_bounds m1) m1' m2' -> - Mem.extends m1 m1' -> - retaddr_stored_at m2 m2' sp pos ra. -Proof. - intros. - assert (B: forall ofs, pos <= ofs < pos + 4 -> loc_out_of_bounds m1 sp ofs). - intros; red; intros. eapply rsa_noperm; eauto. - eapply retaddr_stored_at_invariant; eauto. -- intros. apply H0; auto. eapply retaddr_stored_at_valid; eauto. -- intros. destruct H1. eauto. -- intros. destruct H1. apply H4; auto. -Qed. - -Lemma retaddr_stored_at_can_alloc: - forall m lo hi m1 sp pos m2 a v m3 m' m1' a' v' m2' ra, - Mem.alloc m lo hi = (m1, sp) -> - Mem.free m1 sp pos (pos + 4) = Some m2 -> - Mem.storev Mint32 m2 a v = Some m3 -> - Mem.alloc m' lo hi = (m1', sp) -> - Mem.storev Mint32 m1' a' v' = Some m2' -> - (4 | pos) -> - Mem.extends m3 m2' -> - Val.has_type ra Tint -> - exists m3', - Mem.store Mint32 m2' sp pos ra = Some m3' - /\ retaddr_stored_at m3 m3' sp pos ra - /\ Mem.extends m3 m3'. -Proof. - intros. destruct a; simpl in H1; try discriminate. destruct a'; simpl in H3; try discriminate. - assert (POS: forall ofs, pos <= ofs < pos + 4 -> lo <= ofs < hi). - intros. eapply Mem.perm_alloc_3. eexact H. eapply Mem.free_range_perm; eauto. - assert (ST: { m3' | Mem.store Mint32 m2' sp pos ra = Some m3' }). - { - apply Mem.valid_access_store. split. - red; intros. eapply Mem.perm_store_1; eauto. - apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. - assumption. - } - destruct ST as [m3' ST]. exists m3'; split; auto. - split. constructor. - intros; red; intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto. - intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. - apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. - replace ra with (Val.load_result Mint32 ra). eapply Mem.load_store_same; eauto. - destruct ra; reflexivity || contradiction. - eapply Mem.store_outside_extends; eauto. - intros. eelim Mem.perm_free_2; eauto. eapply Mem.perm_store_2; eauto. -Qed. - -Lemma retaddr_stored_at_can_free: - forall m m' sp pos ra lo m1 hi m2, - retaddr_stored_at m m' sp pos ra -> - Mem.free m sp lo pos = Some m1 -> - Mem.free m1 sp (pos + 4) hi = Some m2 -> - Mem.extends m m' -> - exists m1', Mem.free m' sp lo hi = Some m1' /\ Mem.extends m2 m1'. -Proof. - intros. inv H. - assert (F: { m1' | Mem.free m' sp lo hi = Some m1' }). - { - apply Mem.range_perm_free. red; intros. - assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega. - destruct EITHER as [A | [A | A]]. - eapply Mem.perm_extends; eauto. eapply Mem.free_range_perm; eauto. - auto. - eapply Mem.perm_extends; eauto. - eapply Mem.perm_free_3; eauto. eapply Mem.free_range_perm; eauto. - } - destruct F as [m1' F]. exists m1'; split; auto. - eapply Mem.free_right_extends; eauto. - eapply Mem.free_left_extends. eapply Mem.free_left_extends. eauto. eauto. eauto. - intros. - exploit Mem.perm_free_3. eexact H1. eauto. intros P1. - exploit Mem.perm_free_3. eexact H0. eauto. intros P0. - assert (EITHER: lo <= ofs < pos \/ pos <= ofs < pos + 4 \/ pos + 4 <= ofs < hi) by omega. - destruct EITHER as [A | [A | A]]. - eelim Mem.perm_free_2. eexact H0. eexact A. eauto. - eelim rsa_noperm0; eauto. - eelim Mem.perm_free_2. eexact H1. eexact A. eauto. -Qed. - -Lemma retaddr_stored_at_type: - forall m m' sp pos ra, retaddr_stored_at m m' sp pos ra -> Val.has_type ra Tint. -Proof. - intros. change Tint with (type_of_chunk Mint32). - eapply Mem.load_type. eapply rsa_contains; eauto. -Qed. - -(** Matching a Mach stack against an Asm memory state. *) +(** * Properties of the Mach call stack *) Section MATCH_STACK. Variable ge: Mach.genv. -Inductive match_stack: - list Mach.stackframe -> mem -> mem -> val -> block -> Prop := - | match_stack_nil: forall m m' bound, - match_stack nil m m' Vzero bound - | match_stack_cons: forall f sp c s m m' ra tf tc ra' bound - (AT: transl_code_at_pc ge ra f c false tf tc) - (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra') - (BELOW: sp < bound), - match_stack s m m' ra' sp -> - match_stack (Stackframe f (Vptr sp Int.zero) c :: s) m m' ra bound. +Inductive match_stack: list Mach.stackframe -> Prop := + | match_stack_nil: + match_stack nil + | match_stack_cons: forall fb sp ra c s f tf tc, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ge ra fb f c false tf tc -> + sp <> Vundef -> + match_stack s -> + match_stack (Stackframe fb sp ra c :: s). -Lemma match_stack_invariant: - forall m2 m2' s m1 m1' ra bound, - match_stack s m1 m1' ra bound -> - (forall b ofs p, b < bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - (forall b ofs k p, b < bound -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) -> - (forall b ofs v, b < bound -> Mem.load Mint32 m1' b ofs = Some v -> Mem.load Mint32 m2' b ofs = Some v) -> - match_stack s m2 m2' ra bound. -Proof. - induction 1; intros; econstructor; eauto. - eapply retaddr_stored_at_invariant; eauto. - apply IHmatch_stack; intros. - eapply H0; eauto. omega. - eapply H1; eauto. omega. - eapply H2; eauto. omega. -Qed. +Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. +Proof. induction 1; simpl. congruence. auto. Qed. -Lemma match_stack_change_bound: - forall s m m' ra bound1 bound2, - match_stack s m m' ra bound1 -> - bound1 <= bound2 -> - match_stack s m m' ra bound2. -Proof. - intros. inv H; econstructor; eauto. omega. -Qed. +Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. +Proof. induction 1; simpl. unfold Vzero. congruence. inv H0. congruence. Qed. -Lemma match_stack_storev: - forall chunk a v m1 a' v' m1' s m m' ra bound, - match_stack s m m' ra bound -> - Mem.storev chunk m a v = Some m1 -> - Mem.storev chunk m' a' v' = Some m1' -> - Val.lessdef a a' -> - match_stack s m1 m1' ra bound. -Proof. - induction 1; intros; econstructor; eauto. - eapply retaddr_stored_at_storev; eauto. -Qed. - -Lemma match_stack_extcall: - forall m2 m2' s m1 m1' ra bound, - match_stack s m1 m1' ra bound -> - (forall b ofs p, Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - mem_unchanged_on (loc_out_of_bounds m1) m1' m2' -> - Mem.extends m1 m1' -> - match_stack s m2 m2' ra bound. -Proof. - induction 1; intros; econstructor; eauto. - eapply retaddr_stored_at_extcall; eauto. -Qed. - -Lemma match_stack_free_left: - forall s m m' ra bound b lo hi m1, - match_stack s m m' ra bound -> - Mem.free m b lo hi = Some m1 -> - match_stack s m1 m' ra bound. -Proof. - intros. eapply match_stack_invariant; eauto. - intros. eapply Mem.perm_free_3; eauto. -Qed. - -Lemma match_stack_free_right: - forall s m m' ra bound b lo hi m1', - match_stack s m m' ra bound -> - Mem.free m' b lo hi = Some m1' -> - bound <= b -> - match_stack s m m1' ra bound. -Proof. - intros. eapply match_stack_invariant; eauto. - intros. eapply Mem.perm_free_1; eauto. left. unfold block; omega. - intros. rewrite <- H3. eapply Mem.load_free; eauto. left. unfold block; omega. -Qed. - -Lemma parent_sp_def: - forall s m m' ra bound, - match_stack s m m' ra bound -> parent_sp s <> Vundef. +Lemma lessdef_parent_sp: + forall s v, + match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. Proof. - intros. inv H; simpl; congruence. + intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. Qed. -Lemma lessdef_parent_sp: - forall s m m' ra bound v, - match_stack s m m' ra bound -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Lemma lessdef_parent_ra: + forall s v, + match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. Proof. - intros. inv H0; auto. exfalso. eelim parent_sp_def; eauto. + intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. Qed. End MATCH_STACK. - diff --git a/backend/Mach.v b/backend/Mach.v index 12c6c9d..0728c4d 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -115,7 +115,13 @@ semantics also make provisions for storing a back link at offset offset [f.(fn_retaddr_ofs)]. The latter stack location will be used by the Asm code generated by [Asmgen] to save the return address into the caller at the beginning of a function, then restore it and jump to -it at the end of a function. *) +it at the end of a function. The Mach concrete semantics does not +attach any particular meaning to the pointer stored in this reserved +location, but makes sure that it is preserved during execution of a +function. The [return_address_offset] parameter is used to guess the +value of the return address that the Asm code generated later will +store in the reserved location. +*) Definition chunk_of_type (ty: typ) := match ty with Tint => Mint32 | Tfloat => Mfloat64al32 end. @@ -202,16 +208,20 @@ Qed. Section RELSEM. +Variable return_address_offset: function -> code -> int -> Prop. + Variable ge: genv. -Definition find_function (ros: mreg + ident) (rs: regset) : option fundef := +Definition find_function_ptr + (ge: genv) (ros: mreg + ident) (rs: regset) : option block := match ros with - | inl r => Genv.find_funct ge (rs r) - | inr symb => - match Genv.find_symbol ge symb with - | None => None - | Some b => Genv.find_funct_ptr ge b + | inl r => + match rs r with + | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None + | _ => None end + | inr symb => + Genv.find_symbol ge symb end. (** Extract the values of the arguments to an external call. *) @@ -242,17 +252,20 @@ Definition annot_arguments (** Mach execution states. *) +(** Mach execution states. *) + Inductive stackframe: Type := | Stackframe: - forall (f: function) (**r calling function *) + forall (f: block) (**r pointer to calling function *) (sp: val) (**r stack pointer in calling function *) + (retaddr: val) (**r Asm return address in calling function *) (c: code), (**r program point in calling function *) stackframe. Inductive state: Type := | State: forall (stack: list stackframe) (**r call stack *) - (f: function) (**r current function *) + (f: block) (**r pointer to current function *) (sp: val) (**r stack pointer *) (c: code) (**r current program point *) (rs: regset) (**r register state *) @@ -260,7 +273,7 @@ Inductive state: Type := state | Callstate: forall (stack: list stackframe) (**r call stack *) - (fd: fundef) (**r function to call *) + (f: block) (**r pointer to function to call *) (rs: regset) (**r register state *) (m: mem), (**r memory state *) state @@ -273,7 +286,13 @@ Inductive state: Type := Definition parent_sp (s: list stackframe) : val := match s with | nil => Vptr Mem.nullptr Int.zero - | Stackframe f sp c :: s' => sp + | Stackframe f sp ra c :: s' => sp + end. + +Definition parent_ra (s: list stackframe) : val := + match s with + | nil => Vzero + | Stackframe f sp ra c :: s' => ra end. Inductive step: state -> trace -> state -> Prop := @@ -292,11 +311,12 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Msetstack src ofs ty :: c) rs m) E0 (State s f sp c (undef_setstack rs) m') | exec_Mgetparam: - forall s f sp ofs ty dst c rs m v, + forall s fb f sp ofs ty dst c rs m v, + Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (parent_sp s) ty ofs = Some v -> - step (State s f sp (Mgetparam ofs ty dst :: c) rs m) - E0 (State s f sp c (rs # IT1 <- Vundef # dst <- v) m) + step (State s fb sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m) | exec_Mop: forall s f sp op args res c rs m v, eval_operation ge sp op rs##args m = Some v -> @@ -315,19 +335,22 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mstore chunk addr args src :: c) rs m) E0 (State s f sp c (undef_temps rs) m') | exec_Mcall: - forall s f sp sig ros c rs m fd, - find_function ros rs = Some fd -> - step (State s f sp (Mcall sig ros :: c) rs m) - E0 (Callstate (Stackframe f sp c :: s) - fd rs m) + forall s fb sp sig ros c rs m f f' ra, + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + return_address_offset f c ra -> + step (State s fb sp (Mcall sig ros :: c) rs m) + E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) + f' rs m) | exec_Mtailcall: - forall s f stk soff sig ros c rs m fd m' m'', - find_function ros rs = Some fd -> + forall s fb stk soff sig ros c rs m f f' m', + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> - Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> - step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs m) - E0 (Callstate s fd rs m'') + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) + E0 (Callstate s f' rs m') | exec_Mbuiltin: forall s f sp rs m ef args res b t v m', external_call ef ge rs##args m t v m' -> @@ -340,70 +363,74 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mannot ef args :: b) rs m) t (State s f sp b rs m') | exec_Mgoto: - forall s f sp lbl c rs m c', + forall s fb f sp lbl c rs m c', + Genv.find_funct_ptr ge fb = Some (Internal f) -> find_label lbl f.(fn_code) = Some c' -> - step (State s f sp (Mgoto lbl :: c) rs m) - E0 (State s f sp c' rs m) + step (State s fb sp (Mgoto lbl :: c) rs m) + E0 (State s fb sp c' rs m) | exec_Mcond_true: - forall s f sp cond args lbl c rs m c', + forall s fb f sp cond args lbl c rs m c', eval_condition cond rs##args m = Some true -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> find_label lbl f.(fn_code) = Some c' -> - step (State s f sp (Mcond cond args lbl :: c) rs m) - E0 (State s f sp c' (undef_temps rs) m) + step (State s fb sp (Mcond cond args lbl :: c) rs m) + E0 (State s fb sp c' (undef_temps rs) m) | exec_Mcond_false: forall s f sp cond args lbl c rs m, eval_condition cond rs##args m = Some false -> step (State s f sp (Mcond cond args lbl :: c) rs m) E0 (State s f sp c (undef_temps rs) m) | exec_Mjumptable: - forall s f sp arg tbl c rs m n lbl c', + forall s fb f sp arg tbl c rs m n lbl c', rs arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some lbl -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> find_label lbl f.(fn_code) = Some c' -> - step (State s f sp (Mjumptable arg tbl :: c) rs m) - E0 (State s f sp c' (undef_temps rs) m) + step (State s fb sp (Mjumptable arg tbl :: c) rs m) + E0 (State s fb sp c' (undef_temps rs) m) | exec_Mreturn: - forall s f stk soff c rs m m' m'', + forall s fb stk soff c rs m f m', + Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> - Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' -> - Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' -> - step (State s f (Vptr stk soff) (Mreturn :: c) rs m) - E0 (Returnstate s rs m'') + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) + E0 (Returnstate s rs m') | exec_function_internal: - forall s f rs m m1 m2 m3 stk, + forall s fb rs m f m1 m2 m3 stk, + Genv.find_funct_ptr ge fb = Some (Internal f) -> Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> - Mem.free m1 stk (Int.unsigned f.(fn_retaddr_ofs)) (Int.unsigned f.(fn_retaddr_ofs) + 4) = Some m2 -> let sp := Vptr stk Int.zero in - store_stack m2 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m3 -> - (4 | Int.unsigned f.(fn_retaddr_ofs)) -> - step (Callstate s (Internal f) rs m) - E0 (State s f sp f.(fn_code) (undef_temps rs) m3) + store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 -> + store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> + step (Callstate s fb rs m) + E0 (State s fb sp f.(fn_code) (undef_temps rs) m3) | exec_function_external: - forall s ef rs m t rs' args res m', + forall s fb rs m t rs' ef args res m', + Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t res m' -> extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> rs' = (rs#(loc_result (ef_sig ef)) <- res) -> - step (Callstate s (External ef) rs m) + step (Callstate s fb rs m) t (Returnstate s rs' m') | exec_return: - forall s f sp c rs m, - step (Returnstate (Stackframe f sp c :: s) rs m) + forall s f sp ra c rs m, + step (Returnstate (Stackframe f sp ra c :: s) rs m) E0 (State s f sp c rs m). End RELSEM. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b fd m0, + | initial_state_intro: forall fb m0, let ge := Genv.globalenv p in Genv.init_mem p = Some m0 -> - Genv.find_symbol ge p.(prog_main) = Some b -> - Genv.find_funct_ptr ge b = Some fd -> - initial_state p (Callstate nil fd (Regmap.init Vundef) m0). + Genv.find_symbol ge p.(prog_main) = Some fb -> + initial_state p (Callstate nil fb (Regmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, rs (loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. -Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). +Definition semantics (rao: function -> code -> int -> Prop) (p: program) := + Semantics (step rao) (initial_state p) final_state (Genv.globalenv p). diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index cd01beb..4ce8c25 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -50,6 +50,15 @@ Qed. Section PRESERVATION. +Variable return_address_offset: Mach.function -> Mach.code -> int -> Prop. + +Hypothesis return_address_offset_exists: + forall f sg ros c, + is_tail (Mcall sg ros :: c) (fn_code f) -> + exists ofs, return_address_offset f c ofs. + +Let step := Mach.step return_address_offset. + Variable prog: Linear.program. Variable tprog: Mach.program. Hypothesis TRANSF: transf_program prog = OK tprog. @@ -421,31 +430,23 @@ Definition frame_perm_freeable (m: mem) (sp: block): Prop := forall ofs, 0 <= ofs < fe.(fe_size) -> ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> - ofs < fe.(fe_ofs_retaddr) \/ fe.(fe_ofs_retaddr) + 4 <= ofs -> Mem.perm m sp ofs Cur Freeable. Lemma offset_of_index_perm: forall m sp idx, - index_valid idx -> idx <> FI_retaddr -> + index_valid idx -> frame_perm_freeable m sp -> Mem.range_perm m sp (offset_of_index fe idx) (offset_of_index fe idx + AST.typesize (type_of_index idx)) Cur Freeable. Proof. intros. exploit offset_of_index_valid; eauto. intros [A B]. - exploit offset_of_index_disj. - instantiate (1 := FI_retaddr); exact I. - eexact H. - red. destruct idx; auto || congruence. - change (AST.typesize (type_of_index FI_retaddr)) with 4. - change (offset_of_index fe FI_retaddr) with fe.(fe_ofs_retaddr). - intros C. - exploit offset_of_index_disj_stack_data_2; eauto. intros D. - red; intros. apply H1. omega. omega. omega. + exploit offset_of_index_disj_stack_data_2; eauto. intros. + red; intros. apply H0. omega. omega. Qed. Lemma store_index_succeeds: forall m sp idx v, - index_valid idx -> idx <> FI_retaddr -> + index_valid idx -> frame_perm_freeable m sp -> exists m', Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m'. @@ -527,7 +528,7 @@ Qed. Lemma index_contains_inj_undef: forall j m sp idx, - index_valid idx -> idx <> FI_retaddr -> + index_valid idx -> frame_perm_freeable m sp -> index_contains_inj j m sp idx Vundef. Proof. @@ -557,7 +558,7 @@ Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop := Record agree_frame (j: meminj) (ls ls0: locset) (m: mem) (sp: block) (m': mem) (sp': block) - (parent: val) : Prop := + (parent retaddr: val) : Prop := mk_agree_frame { (** Unused registers have the same value as in the caller *) @@ -583,9 +584,12 @@ Record agree_frame (j: meminj) (ls ls0: locset) In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) -> ls (S (Incoming ofs ty)) = ls0 (S (Outgoing ofs ty)); - (** The back link contains the [parent] value. *) + (** The back link and return address slots of the Mach frame contain + the [parent] and [retaddr] values, respectively. *) agree_link: index_contains m' sp' FI_link parent; + agree_retaddr: + index_contains m' sp' FI_retaddr retaddr; (** The areas of the frame reserved for saving used callee-save registers always contain the values that those registers had @@ -627,7 +631,7 @@ Record agree_frame (j: meminj) (ls ls0: locset) }. Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming - agree_link agree_saved_int agree_saved_float + agree_link agree_retaddr agree_saved_int agree_saved_float agree_valid_linear agree_valid_mach agree_perm agree_wt_ls: stacking. @@ -767,11 +771,11 @@ Qed. (** Preservation under assignment of machine register. *) Lemma agree_frame_set_reg: - forall j ls ls0 m sp m' sp' parent r v, - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent ra r v, + agree_frame j ls ls0 m sp m' sp' parent ra -> mreg_within_bounds b r -> Val.has_type v (Loc.type (R r)) -> - agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent. + agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra. Proof. intros. inv H; constructor; auto; intros. rewrite Locmap.gso. auto. red. intuition congruence. @@ -798,10 +802,10 @@ Proof. Qed. Lemma agree_frame_undef_locs: - forall j ls0 m sp m' sp' parent regs ls, - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls0 m sp m' sp' parent ra regs ls, + agree_frame j ls ls0 m sp m' sp' parent ra -> incl (List.map R regs) temporaries -> - agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent. + agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra. Proof. induction regs; simpl; intros. auto. @@ -812,17 +816,17 @@ Proof. Qed. Lemma agree_frame_undef_temps: - forall j ls ls0 m sp m' sp' parent, - agree_frame j ls ls0 m sp m' sp' parent -> - agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent. + forall j ls ls0 m sp m' sp' parent ra, + agree_frame j ls ls0 m sp m' sp' parent ra -> + agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra. Proof. intros. unfold temporaries. apply agree_frame_undef_locs; auto. apply incl_refl. Qed. Lemma agree_frame_undef_setstack: - forall j ls ls0 m sp m' sp' parent, - agree_frame j ls ls0 m sp m' sp' parent -> - agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent. + forall j ls ls0 m sp m' sp' parent ra, + agree_frame j ls ls0 m sp m' sp' parent ra -> + agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent ra. Proof. intros. unfold Linear.undef_setstack, destroyed_at_move. apply agree_frame_undef_locs; auto. @@ -830,9 +834,9 @@ Proof. Qed. Lemma agree_frame_undef_op: - forall j ls ls0 m sp m' sp' parent op, - agree_frame j ls ls0 m sp m' sp' parent -> - agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent. + forall j ls ls0 m sp m' sp' parent ra op, + agree_frame j ls ls0 m sp m' sp' parent ra -> + agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent ra. Proof. intros. exploit agree_frame_undef_temps; eauto. @@ -842,13 +846,13 @@ Qed. (** Preservation by assignment to local slot *) Lemma agree_frame_set_local: - forall j ls ls0 m sp m' sp' parent ofs ty v v' m'', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds f b (Local ofs ty) -> val_inject j v v' -> Val.has_type v ty -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_local ofs ty)) v' = Some m'' -> - agree_frame j (Locmap.set (S (Local ofs ty)) v ls) ls0 m sp m'' sp' parent. + agree_frame j (Locmap.set (S (Local ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr. Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3. @@ -867,6 +871,8 @@ Proof. rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto. red; auto. +(* retaddr *) + eapply gso_index_contains; eauto. red; auto. (* int callee save *) eapply gso_index_contains_inj; eauto. simpl; auto. (* float callee save *) @@ -882,13 +888,13 @@ Qed. (** Preservation by assignment to outgoing slot *) Lemma agree_frame_set_outgoing: - forall j ls ls0 m sp m' sp' parent ofs ty v v' m'', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr ofs ty v v' m'', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> slot_within_bounds f b (Outgoing ofs ty) -> val_inject j v v' -> Val.has_type v ty -> Mem.store (chunk_of_type ty) m' sp' (offset_of_index fe (FI_arg ofs ty)) v' = Some m'' -> - agree_frame j (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 m sp m'' sp' parent. + agree_frame j (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 m sp m'' sp' parent retaddr. Proof. intros. inv H. change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3. @@ -901,7 +907,7 @@ Proof. unfold Locmap.set. simpl. destruct (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))). inv e. eapply gss_index_contains_inj; eauto. case_eq (Loc.overlap_aux ty ofs ofs0 || Loc.overlap_aux ty0 ofs0 ofs); intros. - apply index_contains_inj_undef. auto. congruence. + apply index_contains_inj_undef. auto. red; intros. eapply Mem.perm_store_1; eauto. eapply gso_index_contains_inj; eauto. red. eapply Loc.overlap_aux_false_1; eauto. @@ -909,6 +915,8 @@ Proof. rewrite Locmap.gso; auto. red; auto. (* parent *) eapply gso_index_contains; eauto with stacking. red; auto. +(* retaddr *) + eapply gso_index_contains; eauto with stacking. red; auto. (* int callee save *) eapply gso_index_contains_inj; eauto with stacking. simpl; auto. (* float callee save *) @@ -924,8 +932,8 @@ Qed. (** General invariance property with respect to memory changes. *) Lemma agree_frame_invariant: - forall j ls ls0 m sp m' sp' parent m1 m1', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr m1 m1', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> @@ -937,7 +945,7 @@ Lemma agree_frame_invariant: (forall ofs k p, ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> Mem.perm m' sp' ofs k p -> Mem.perm m1' sp' ofs k p) -> - agree_frame j ls ls0 m1 sp m1' sp' parent. + agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. Proof. intros. assert (IC: forall idx v, @@ -956,13 +964,13 @@ Qed. (** A variant of the latter, for use with external calls *) Lemma agree_frame_extcall_invariant: - forall j ls ls0 m sp m' sp' parent m1 m1', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr m1 m1', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> mem_unchanged_on (loc_out_of_reach j m) m' m1' -> - agree_frame j ls ls0 m1 sp m1' sp' parent. + agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. Proof. intros. assert (REACH: forall ofs, @@ -978,13 +986,13 @@ Qed. (** Preservation by parallel stores in the Linear and Mach codes *) Lemma agree_frame_parallel_stores: - forall j ls ls0 m sp m' sp' parent chunk addr addr' v v' m1 m1', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr chunk addr addr' v v' m1 m1', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> Mem.inject j m m' -> val_inject j addr addr' -> Mem.storev chunk m addr v = Some m1 -> Mem.storev chunk m' addr' v' = Some m1' -> - agree_frame j ls ls0 m1 sp m1' sp' parent. + agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. Proof. Opaque Int.add. intros until m1'. intros AG MINJ VINJ STORE1 STORE2. @@ -1014,11 +1022,11 @@ Qed. (** Preservation by increasing memory injections (allocations and external calls) *) Lemma agree_frame_inject_incr: - forall j ls ls0 m sp m' sp' parent m1 m1' j', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr m1 m1' j', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> inject_incr j j' -> inject_separated j j' m1 m1' -> Mem.valid_block m1' sp' -> - agree_frame j' ls ls0 m sp m' sp' parent. + agree_frame j' ls ls0 m sp m' sp' parent retaddr. Proof. intros. inv H. constructor; auto; intros; eauto with stacking. case_eq (j b0). @@ -1054,11 +1062,11 @@ Proof. Qed. Lemma agree_frame_return: - forall j ls ls0 m sp m' sp' parent ls', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr ls', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> agree_callee_save ls' ls -> wt_locset ls' -> - agree_frame j ls' ls0 m sp m' sp' parent. + agree_frame j ls' ls0 m sp m' sp' parent retaddr. Proof. intros. red in H0. inv H; constructor; auto; intros. rewrite H0; auto. apply mreg_not_within_bounds_callee_save; auto. @@ -1070,10 +1078,10 @@ Qed. (** Preservation at tailcalls (when [ls0] is changed but not [ls]). *) Lemma agree_frame_tailcall: - forall j ls ls0 m sp m' sp' parent ls0', - agree_frame j ls ls0 m sp m' sp' parent -> + forall j ls ls0 m sp m' sp' parent retaddr ls0', + agree_frame j ls ls0 m sp m' sp' parent retaddr -> agree_callee_save ls0 ls0' -> - agree_frame j ls ls0' m sp m' sp' parent. + agree_frame j ls ls0' m sp m' sp' parent retaddr. Proof. intros. red in H0. inv H; constructor; auto; intros. rewrite <- H0; auto. apply mreg_not_within_bounds_callee_save; auto. @@ -1082,6 +1090,7 @@ Proof. rewrite <- H0; auto. Qed. + (** Properties of [agree_callee_save]. *) Lemma agree_callee_save_return_regs: @@ -1122,6 +1131,7 @@ Variable mkindex: Z -> frame_index. Variable ty: typ. Variable j: meminj. Variable cs: list stackframe. +Variable fb: block. Variable sp: block. Variable csregs: list mreg. Variable ls: locset. @@ -1154,8 +1164,6 @@ Hypothesis mkindex_inj: Hypothesis mkindex_diff: forall r idx, idx <> mkindex (number r) -> index_diff (mkindex (number r)) idx. -Hypothesis mkindex_not_retaddr: - forall r, mkindex (number r) <> FI_retaddr. Hypothesis csregs_typ: forall r, In r csregs -> mreg_type r = ty. @@ -1172,9 +1180,9 @@ Lemma save_callee_save_regs_correct: agree_regs j ls rs -> exists rs', exists m', star step tge - (State cs tf (Vptr sp Int.zero) + (State cs fb (Vptr sp Int.zero) (save_callee_save_regs bound number mkindex ty fe l k) rs m) - E0 (State cs tf (Vptr sp Int.zero) k rs' m') + E0 (State cs fb (Vptr sp Int.zero) k rs' m') /\ (forall r, In r l -> number r < bound fe -> index_contains_inj j m' sp (mkindex (number r)) (ls (R r))) @@ -1201,7 +1209,7 @@ Proof. unfold save_callee_save_reg. destruct (zlt (number a) (bound fe)). (* a store takes place *) - exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. auto. + exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. eauto. instantiate (1 := rs a). intros [m1 ST]. exploit (IHl k (undef_setstack rs) m1). auto with coqlib. auto. red; eauto with mem. @@ -1244,13 +1252,13 @@ Qed. End SAVE_CALLEE_SAVE. Lemma save_callee_save_correct: - forall j ls rs sp cs k m, + forall j ls rs sp cs fb k m, agree_regs j (call_regs ls) rs -> wt_locset (call_regs ls) -> frame_perm_freeable m sp -> exists rs', exists m', star step tge - (State cs tf (Vptr sp Int.zero) (save_callee_save fe k) rs m) - E0 (State cs tf (Vptr sp Int.zero) k rs' m') + (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs m) + E0 (State cs fb (Vptr sp Int.zero) k rs' m') /\ (forall r, In r int_callee_save_regs -> index_int_callee_save r < b.(bound_int_callee_save) -> index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (call_regs ls (R r))) @@ -1275,13 +1283,12 @@ Transparent destroyed_at_move_regs. fe_num_int_callee_save index_int_callee_save FI_saved_int Tint - j cs sp int_callee_save_regs (call_regs ls)). + j cs fb sp int_callee_save_regs (call_regs ls)). intros. apply index_int_callee_save_inj; auto. intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption. auto. intros; congruence. intros; simpl. destruct idx; auto. congruence. - intros; congruence. intros. apply int_callee_save_type. auto. auto. auto. @@ -1294,13 +1301,12 @@ Transparent destroyed_at_move_regs. fe_num_float_callee_save index_float_callee_save FI_saved_float Tfloat - j cs sp float_callee_save_regs (call_regs ls)). + j cs fb sp float_callee_save_regs (call_regs ls)). intros. apply index_float_callee_save_inj; auto. intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption. simpl; auto. intros; congruence. intros; simpl. destruct idx; auto. congruence. - intros; congruence. intros. apply float_callee_save_type. auto. auto. auto. @@ -1371,28 +1377,28 @@ Qed. saving of the used callee-save registers). *) Lemma function_prologue_correct: - forall j ls ls0 rs m1 m1' m2 sp parent cs k, + forall j ls ls0 rs m1 m1' m2 sp parent ra cs fb k, agree_regs j ls rs -> agree_callee_save ls ls0 -> wt_locset ls -> Mem.inject j m1 m1' -> Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) -> - Val.has_type parent Tint -> + Val.has_type parent Tint -> Val.has_type ra Tint -> exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5', Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp') - /\ Mem.free m2' sp' (Int.unsigned tf.(fn_retaddr_ofs)) (Int.unsigned tf.(fn_retaddr_ofs) + 4) = Some m3' - /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m4' + /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3' + /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4' /\ star step tge - (State cs tf (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4') - E0 (State cs tf (Vptr sp' Int.zero) k rs' m5') + (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4') + E0 (State cs fb (Vptr sp' Int.zero) k rs' m5') /\ agree_regs j' (call_regs ls) rs' - /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent + /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent ra /\ inject_incr j j' /\ inject_separated j j' m1 m1' /\ Mem.inject j' m2 m5' - /\ stores_in_frame sp' m3' m5'. + /\ stores_in_frame sp' m2' m5'. Proof. - intros until k; intros AGREGS AGCS WTREGS INJ1 ALLOC TYPAR. + intros until k; intros AGREGS AGCS WTREGS INJ1 ALLOC TYPAR TYRA. rewrite unfold_transf_function. unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs. (* Allocation step *) @@ -1417,37 +1423,14 @@ Proof. assert (~Mem.valid_block m1' sp') by eauto with mem. contradiction. intros [j' [INJ2 [INCR [MAP1 MAP2]]]]. - (* separation *) - assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe). - intros. destruct (zeq b0 sp). - subst b0. rewrite MAP1 in H; inv H; auto. - rewrite MAP2 in H; auto. - assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto. - assert (~Mem.valid_block m1' sp') by eauto with mem. - contradiction. - (* Freeing step *) - assert (OFSRA: Int.unsigned (Int.repr (fe_ofs_retaddr fe)) = fe_ofs_retaddr fe). - apply (offset_of_index_no_overflow FI_retaddr). exact I. - rewrite OFSRA. - assert (FREE: { m3' | Mem.free m2' sp' (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) = Some m3'}). - apply Mem.range_perm_free. - exploit (offset_of_index_valid FI_retaddr). exact I. - unfold offset_of_index. simpl AST.typesize. intros [A B]. - red; intros. eapply Mem.perm_alloc_2; eauto. omega. - destruct FREE as [m3' FREE]. - assert (INJ3: Mem.inject j' m2 m3'). - eapply Mem.free_right_inject; eauto. - intros. exploit SEP; eauto. intros [A B]. subst b1 delta. - exploit (offset_of_index_disj_stack_data_1 FI_retaddr). exact I. - unfold offset_of_index. simpl AST.typesize. intros. - exploit Mem.perm_alloc_3. eexact ALLOC. eauto. intros. - generalize bound_stack_data_stacksize; intros. - omega. - assert (PERM: frame_perm_freeable m3' sp'). - red; intros. eapply Mem.perm_free_1; eauto. eapply Mem.perm_alloc_2; eauto. + assert (PERM: frame_perm_freeable m2' sp'). + red; intros. eapply Mem.perm_alloc_2; eauto. (* Store of parent *) - exploit (store_index_succeeds m3' sp' FI_link parent). red; auto. congruence. auto. - intros [m4' STORE]. + exploit (store_index_succeeds m2' sp' FI_link parent). red; auto. auto. + intros [m3' STORE2]. + (* Store of retaddr *) + exploit (store_index_succeeds m3' sp' FI_retaddr ra). red; auto. red; eauto with mem. + intros [m4' STORE3]. (* Saving callee-save registers *) assert (PERM4: frame_perm_freeable m4' sp'). red; intros. eauto with mem. @@ -1457,21 +1440,32 @@ Proof. eexact PERM4. intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]]. (* stores in frames *) - assert (SIF: stores_in_frame sp' m3' m5'). + assert (SIF: stores_in_frame sp' m2' m5'). econstructor; eauto. rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto. + econstructor; eauto. + rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; auto. red; auto. + (* separation *) + assert (SEP: forall b0 delta, j' b0 = Some(sp', delta) -> b0 = sp /\ delta = fe_stack_data fe). + intros. destruct (zeq b0 sp). + subst b0. rewrite MAP1 in H; inv H; auto. + rewrite MAP2 in H; auto. + assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto. + assert (~Mem.valid_block m1' sp') by eauto with mem. + contradiction. (* Conclusions *) exists j'; exists rs'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'. - (* alloc *) - split. auto. - (* free *) split. auto. (* store parent *) split. change Tint with (type_of_index FI_link). change (fe_ofs_link fe) with (offset_of_index fe FI_link). apply store_stack_succeeds; auto. red; auto. + (* store retaddr *) + split. change Tint with (type_of_index FI_retaddr). + change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr). + apply store_stack_succeeds; auto. red; auto. (* saving of registers *) - split. rewrite <- unfold_transf_function. eexact STEPS. + split. eexact STEPS. (* agree_regs *) split. auto. (* agree frame *) @@ -1481,13 +1475,18 @@ Proof. elim H. apply temporary_within_bounds; auto. apply AGCS. apply mreg_not_within_bounds_callee_save; auto. (* locals *) - simpl. apply index_contains_inj_undef; auto. congruence. + simpl. apply index_contains_inj_undef; auto. (* outgoing *) - simpl. apply index_contains_inj_undef; auto. congruence. + simpl. apply index_contains_inj_undef; auto. (* incoming *) unfold call_regs. apply AGCS. auto. (* parent *) apply OTHERS; auto. red; auto. + eapply gso_index_contains; eauto. red; auto. + eapply gss_index_contains; eauto. red; auto. + red; auto. + (* retaddr *) + apply OTHERS; auto. red; auto. eapply gss_index_contains; eauto. red; auto. (* int callee save *) rewrite <- AGCS. replace (ls (R r)) with (call_regs ls (R r)). @@ -1508,7 +1507,7 @@ Proof. (* valid sp *) eauto with mem. (* valid sp' *) - eapply stores_in_frame_valid with (m := m3'); eauto with mem. + eapply stores_in_frame_valid with (m := m2'); eauto with mem. (* bounds *) exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite zeq_true. auto. (* perms *) @@ -1540,6 +1539,7 @@ Variable ty: typ. Variable csregs: list mreg. Variable j: meminj. Variable cs: list stackframe. +Variable fb: block. Variable sp: block. Variable ls0: locset. Variable m: mem. @@ -1566,9 +1566,9 @@ Lemma restore_callee_save_regs_correct: agree_unused ls0 rs -> exists rs', star step tge - (State cs tf (Vptr sp Int.zero) + (State cs fb (Vptr sp Int.zero) (restore_callee_save_regs bound number mkindex ty fe l k) rs m) - E0 (State cs tf (Vptr sp Int.zero) k rs' m) + E0 (State cs fb (Vptr sp Int.zero) k rs' m) /\ (forall r, In r l -> val_inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r l) -> rs' r = rs r) /\ agree_unused ls0 rs'. @@ -1613,13 +1613,13 @@ Qed. End RESTORE_CALLEE_SAVE. Lemma restore_callee_save_correct: - forall j ls ls0 m sp m' sp' pa cs rs k, - agree_frame j ls ls0 m sp m' sp' pa -> + forall j ls ls0 m sp m' sp' pa ra cs fb rs k, + agree_frame j ls ls0 m sp m' sp' pa ra -> agree_unused j ls0 rs -> exists rs', star step tge - (State cs tf (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') - E0 (State cs tf (Vptr sp' Int.zero) k rs' m') + (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') + E0 (State cs fb (Vptr sp' Int.zero) k rs' m') /\ (forall r, In r int_callee_save_regs \/ In r float_callee_save_regs -> val_inject j (ls0 (R r)) (rs' r)) @@ -1635,7 +1635,7 @@ Proof. FI_saved_int Tint int_callee_save_regs - j cs sp' ls0 m'); auto. + j cs fb sp' ls0 m'); auto. intros. unfold mreg_within_bounds. rewrite (int_callee_save_type r H1). tauto. eapply agree_saved_int; eauto. apply incl_refl. @@ -1648,7 +1648,7 @@ Proof. FI_saved_float Tfloat float_callee_save_regs - j cs sp' ls0 m'); auto. + j cs fb sp' ls0 m'); auto. intros. unfold mreg_within_bounds. rewrite (float_callee_save_type r H1). tauto. eapply agree_saved_float; eauto. apply incl_refl. @@ -1668,94 +1668,57 @@ Qed. registers + reloading of the link and return address + freeing of the frame). *) -Remark mem_range_perm_free_twice: - forall m blk lo1 hi1 lo2 hi2, - (forall ofs, lo1 <= ofs < hi2 -> ofs < hi1 \/ lo2 <= ofs -> Mem.perm m blk ofs Cur Freeable) -> - lo1 <= hi1 /\ lo2 <= hi2 -> hi1 < lo2 -> - exists m', exists m'', - Mem.free m blk lo1 hi1 = Some m' /\ Mem.free m' blk lo2 hi2 = Some m''. -Proof. - intros. - destruct (Mem.range_perm_free m blk lo1 hi1) as [m' FREE1]. - red; intros. apply H. omega. omega. - destruct (Mem.range_perm_free m' blk lo2 hi2) as [m'' FREE2]. - red; intros. eapply Mem.perm_free_1; eauto. right. omega. - apply H. omega. omega. - exists m'; exists m''; auto. -Qed. - Lemma function_epilogue_correct: - forall j ls ls0 m sp m' sp' pa cs rs k m1, + forall j ls ls0 m sp m' sp' pa ra cs fb rs k m1, agree_regs j ls rs -> - agree_frame j ls ls0 m sp m' sp' pa -> + agree_frame j ls ls0 m sp m' sp' pa ra -> Mem.inject j m m' -> Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 -> - exists rs1, exists m1', exists m2', + exists rs1, exists m1', load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) = Some pa - /\ Mem.free m' sp' 0 (Int.unsigned tf.(fn_retaddr_ofs)) = Some m1' - /\ Mem.free m1' sp' (Int.unsigned tf.(fn_retaddr_ofs) + 4) tf.(fn_stacksize) = Some m2' + /\ load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) = Some ra + /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1' /\ star step tge - (State cs tf (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') - E0 (State cs tf (Vptr sp' Int.zero) k rs1 m') + (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') + E0 (State cs fb (Vptr sp' Int.zero) k rs1 m') /\ agree_regs j (return_regs ls0 ls) rs1 /\ agree_callee_save (return_regs ls0 ls) ls0 /\ rs1 IT1 = rs IT1 - /\ Mem.inject j m1 m2'. + /\ Mem.inject j m1 m1'. Proof. intros. - assert (RETADDR: Int.unsigned tf.(fn_retaddr_ofs) = fe.(fe_ofs_retaddr)). - rewrite unfold_transf_function. unfold fn_retaddr_ofs. - apply (offset_of_index_no_overflow FI_retaddr). exact I. - rewrite RETADDR. (* can free *) - destruct (mem_range_perm_free_twice m' sp' - 0 (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) (fe_size fe)) - as [m1' [m2' [FREE1 FREE2]]]. - intros. + destruct (Mem.range_perm_free m' sp' 0 (fn_stacksize tf)) as [m1' FREE]. + rewrite unfold_transf_function; unfold fn_stacksize. red; intros. assert (EITHER: fe_stack_data fe <= ofs < fe_stack_data fe + Linear.fn_stacksize f - \/ (ofs < fe_stack_data fe \/ fe_stack_data fe + Linear.fn_stacksize f <= ofs)) + \/ (ofs < fe_stack_data fe \/ fe_stack_data fe + Linear.fn_stacksize f <= ofs)) by omega. destruct EITHER. replace ofs with ((ofs - fe_stack_data fe) + fe_stack_data fe) by omega. eapply Mem.perm_inject with (f := j). eapply agree_inj; eauto. eauto. eapply Mem.free_range_perm; eauto. omega. - eapply agree_perm; eauto. - apply (offset_of_index_valid FI_retaddr). exact I. - omega. + eapply agree_perm; eauto. (* inject after free *) - assert (UNMAPPED: forall b1 delta ofs k0 p, - j b1 = Some (sp', delta) -> - Mem.perm m1 b1 ofs k0 p -> - False). - { - intros. - exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta. - eelim Mem.perm_free_2. eexact H2. eapply agree_bounds; eauto. - eapply Mem.perm_free_3; eauto. apply Mem.perm_max with k0. eauto. eauto. - } - assert (INJ1: Mem.inject j m1 m2'). - { - eapply Mem.free_right_inject. - eapply Mem.free_right_inject. - eapply Mem.free_left_inject. eauto. eauto. - eauto. - intros; eapply UNMAPPED; eauto. - eauto. - intros; eapply UNMAPPED; eauto. - } + assert (INJ1: Mem.inject j m1 m1'). + eapply Mem.free_inject with (l := (sp, 0, f.(Linear.fn_stacksize)) :: nil); eauto. + simpl. rewrite H2. auto. + intros. exploit agree_inj_unique; eauto. intros [P Q]; subst b1 delta. + exists 0; exists (Linear.fn_stacksize f); split. auto with coqlib. + eapply agree_bounds. eauto. eapply Mem.perm_max. eauto. (* can execute epilogue *) exploit restore_callee_save_correct; eauto. instantiate (1 := rs). red; intros. - rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ H0). auto. auto. + rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ _ H0). auto. auto. intros [rs1 [A [B C]]]. (* conclusions *) - exists rs1; exists m1'; exists m2'. + exists rs1; exists m1'. split. rewrite unfold_transf_function; unfold fn_link_ofs. eapply index_contains_load_stack with (idx := FI_link); eauto with stacking. - split. exact FREE1. - split. rewrite unfold_transf_function; unfold fn_stacksize. exact FREE2. + split. rewrite unfold_transf_function; unfold fn_retaddr_ofs. + eapply index_contains_load_stack with (idx := FI_retaddr); eauto with stacking. + split. auto. split. eexact A. - split. red; intros. unfold return_regs. + split. red;intros. unfold return_regs. generalize (register_classification r) (int_callee_save_not_destroyed r) (float_callee_save_not_destroyed r); intros. destruct (in_dec Loc.eq (R r) temporaries). rewrite C; auto. @@ -1787,12 +1750,14 @@ Inductive match_stacks (j: meminj) (m m': mem): hi <= bound -> hi <= bound' -> match_globalenvs j hi -> tailcall_possible sg -> match_stacks j m m' nil nil sg bound bound' - | match_stacks_cons: forall f sp ls c cs sp' c' cs' sg bound bound' tf + | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg bound bound' trf (TAIL: is_tail c (Linear.fn_code f)) (WTF: wt_function f) - (TRF: transf_function f = OK tf) + (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf)) + (TRF: transf_function f = OK trf) (TRC: transl_code (make_env (function_bounds f)) c = c') - (FRM: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs')) + (TY_RA: Val.has_type ra Tint) + (FRM: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs')) (ARGS: forall ofs ty, In (S (Outgoing ofs ty)) (loc_arguments sg) -> slot_within_bounds f (function_bounds f) (Outgoing ofs ty)) @@ -1801,7 +1766,7 @@ Inductive match_stacks (j: meminj) (m m': mem): (BELOW': sp' < bound'), match_stacks j m m' (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs) - (Stackframe tf (Vptr sp' Int.zero) c' :: cs') + (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs') sg bound bound'. (** Invariance with respect to change of bounds. *) @@ -1992,6 +1957,14 @@ Proof. induction 1; simpl; auto. Qed. +Lemma match_stacks_type_retaddr: + forall j m m' cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + Val.has_type (parent_ra cs') Tint. +Proof. + induction 1; simpl; auto. +Qed. + (** * Syntactic properties of the translation *) (** Preservation of code labels through the translation. *) @@ -2192,8 +2165,9 @@ Lemma find_function_translated: agree_regs j ls rs -> match_stacks j m m' cs cs' sg bound bound' -> Linear.find_function ge ros ls = Some f -> - exists tf, - find_function tge ros rs = Some tf + exists bf, exists tf, + find_function_ptr tge ros rs = Some bf + /\ Genv.find_funct_ptr tge bf = Some tf /\ transf_fundef f = OK tf. Proof. intros until f; intros AG MS FF. @@ -2202,14 +2176,13 @@ Proof. exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF. rewrite Genv.find_funct_find_funct_ptr in FF. exploit function_ptr_translated; eauto. intros [tf [A B]]. - exists tf; split; auto. simpl. + exists b; exists tf; split; auto. simpl. generalize (AG m0). rewrite EQ. intro INJ. inv INJ. - rewrite Int.add_zero_l. - inv MG. rewrite DOMAIN in H2. inv H2. simpl. rewrite A. apply dec_eq_true. - eapply FUNCTIONS; eauto. - destruct (Genv.find_symbol ge i) as [b|] eqn:FS; try discriminate. + inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. + destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate. exploit function_ptr_translated; eauto. intros [tf [A B]]. - exists tf; split; auto. simpl. rewrite symbols_preserved. rewrite FS. auto. + exists b; exists tf; split; auto. simpl. + rewrite symbols_preserved. auto. Qed. Hypothesis wt_prog: wt_program prog. @@ -2297,9 +2270,9 @@ Variables m m': mem. Variables ls ls0: locset. Variable rs: regset. Variables sp sp': block. -Variables parent: val. +Variables parent retaddr: val. Hypothesis AGR: agree_regs j ls rs. -Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent. +Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr. Lemma transl_annot_param_correct: forall l, @@ -2364,27 +2337,29 @@ End ANNOT_ARGUMENTS. Inductive match_states: Linear.state -> Mach.state -> Prop := | match_states_intro: - forall cs f sp c ls m cs' sp' rs m' j tf + forall cs f sp c ls m cs' fb sp' rs m' j tf (MINJ: Mem.inject j m m') (STACKS: match_stacks j m m' cs cs' f.(Linear.fn_sig) sp sp') (TRANSL: transf_function f = OK tf) + (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf)) (WTF: wt_function f) (AGREGS: agree_regs j ls rs) - (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs')) + (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs')) (TAIL: is_tail c (Linear.fn_code f)), match_states (Linear.State cs f (Vptr sp Int.zero) c ls m) - (Mach.State cs' tf (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') + (Mach.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') | match_states_call: - forall cs f ls m cs' rs m' j tf + forall cs f ls m cs' fb rs m' j tf (MINJ: Mem.inject j m m') (STACKS: match_stacks j m m' cs cs' (Linear.funsig f) (Mem.nextblock m) (Mem.nextblock m')) (TRANSL: transf_fundef f = OK tf) + (FIND: Genv.find_funct_ptr tge fb = Some tf) (WTF: wt_fundef f) (WTLS: wt_locset ls) (AGREGS: agree_regs j ls rs) (AGLOCS: agree_callee_save ls (parent_locset cs)), match_states (Linear.Callstate cs f ls m) - (Mach.Callstate cs' tf rs m') + (Mach.Callstate cs' fb rs m') | match_states_return: forall cs ls m cs' rs m' j sg (MINJ: Mem.inject j m m') @@ -2398,7 +2373,7 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := Theorem transf_step_correct: forall s1 t s2, Linear.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), - exists s2', plus Mach.step tge s1' t s2' /\ match_states s2 s2'. + exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. Proof. assert (RED: forall f i c, transl_code (make_env (function_bounds f)) (i :: c) = @@ -2463,7 +2438,6 @@ Proof. apply index_local_valid; auto. red; auto. apply index_arg_valid; auto. - assert (idx <> FI_retaddr) by (unfold idx; destruct sl; congruence). exploit store_index_succeeds; eauto. eapply agree_perm; eauto. instantiate (1 := rs0 r). intros [m1' STORE]. econstructor; split. @@ -2474,12 +2448,12 @@ Proof. econstructor; eauto with coqlib. eapply Mem.store_outside_inject; eauto. intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta. - rewrite size_type_chunk in H6. + rewrite size_type_chunk in H5. exploit offset_of_index_disj_stack_data_2; eauto. exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. omega. apply match_stacks_change_mach_mem with m'; auto. - eauto with mem. eauto with mem. intros. rewrite <- H5; eapply Mem.load_store_other; eauto. left; unfold block; omega. + eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega. apply agree_regs_set_slot. apply agree_regs_undef_setstack; auto. destruct sl. eapply agree_frame_set_local. eapply agree_frame_undef_setstack; eauto. auto. auto. @@ -2548,11 +2522,15 @@ Proof. eapply agree_frame_parallel_stores; eauto. (* Lcall *) - exploit find_function_translated; eauto. intros [tf' [A B]]. + exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. + exploit is_tail_transf_function; eauto. intros IST. simpl in IST. + exploit return_address_offset_exists. eexact IST. + intros [ra D]. econstructor; split. apply plus_one. econstructor; eauto. econstructor; eauto. econstructor; eauto with coqlib. + simpl; auto. intros; red. split. generalize (loc_arguments_acceptable _ _ H0). simpl. omega. apply Zle_trans with (size_arguments (Linear.funsig f')); auto. @@ -2564,13 +2542,13 @@ Proof. simpl; red; auto. (* Ltailcall *) - exploit find_function_translated; eauto. intros [tf' [A B]]. + exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. exploit function_epilogue_correct; eauto. - intros [rs1 [m1' [m2' [P [Q [R [S [T [U [V W ]]]]]]]]]]. + intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]]. econstructor; split. eapply plus_right. eexact S. econstructor; eauto. - replace (find_function tge ros rs1) - with (find_function tge ros rs0). eauto. + replace (find_function_ptr tge ros rs1) + with (find_function_ptr tge ros rs0). eauto. destruct ros; simpl; auto. inv WTI. rewrite V; auto. traceEq. econstructor; eauto. @@ -2579,15 +2557,11 @@ Proof. apply match_stacks_change_linear_mem with m. apply match_stacks_change_mach_mem with m'0. auto. - eauto with mem. - intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. - eapply Mem.perm_free_1; eauto. left; unfold block; omega. - intros. erewrite Mem.load_free. erewrite Mem.load_free; eauto. - left; unfold block; omega. eauto. left; unfold block; omega. - eauto with mem. - intros. eapply Mem.perm_free_3; eauto. + eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. + intros. rewrite <- H2. eapply Mem.load_free; eauto. left; unfold block; omega. + eauto with mem. intros. eapply Mem.perm_free_3; eauto. apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m2' sp'). eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. eapply find_function_well_typed; eauto. apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. @@ -2680,7 +2654,7 @@ Proof. (* Lreturn *) exploit function_epilogue_correct; eauto. - intros [rs1 [m1' [m2' [P [Q [R [S [T [U [V W]]]]]]]]]]. + intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]]. econstructor; split. eapply plus_right. eexact S. econstructor; eauto. traceEq. @@ -2689,15 +2663,11 @@ Proof. apply match_stacks_change_linear_mem with m. apply match_stacks_change_mach_mem with m'0. eauto. - eauto with mem. - intros. eapply Mem.perm_free_1. eauto. left; unfold block; omega. - eapply Mem.perm_free_1; eauto. left; unfold block; omega. - intros. erewrite Mem.load_free. erewrite Mem.load_free; eauto. - left; unfold block; omega. eauto. left; unfold block; omega. - eauto with mem. - intros. eapply Mem.perm_free_3; eauto. + eauto with mem. intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. + intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega. + eauto with mem. intros. eapply Mem.perm_free_3; eauto. apply Zlt_le_weak. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Zlt_le_weak. change (Mem.valid_block m2' sp'). eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + apply Zlt_le_weak. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. apply wt_return_regs; auto. eapply match_stacks_wt_locset; eauto. eapply agree_wt_ls; eauto. (* internal function *) @@ -2707,14 +2677,11 @@ Proof. inversion WTF as [|f' WTFN]. subst f'. exploit function_prologue_correct; eauto. eapply match_stacks_type_sp; eauto. + eapply match_stacks_type_retaddr; eauto. intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]]. econstructor; split. - eapply plus_left. econstructor; eauto. - rewrite (unfold_transf_function _ _ TRANSL). unfold fn_retaddr_ofs. - generalize (offset_of_index_no_overflow _ _ TRANSL FI_retaddr I). - unfold offset_of_index. intros EQ; rewrite EQ. - apply (offset_of_index_aligned f FI_retaddr). - rewrite (unfold_transf_function _ _ TRANSL) at 2. unfold fn_code. unfold transl_body. + eapply plus_left. econstructor; eauto. + rewrite (unfold_transf_function _ _ TRANSL). unfold fn_code. unfold transl_body. eexact D. traceEq. generalize (Mem.alloc_result _ _ _ _ _ H). intro SP_EQ. generalize (Mem.alloc_result _ _ _ _ _ A). intro SP'_EQ. @@ -2727,10 +2694,7 @@ Proof. rewrite zeq_false. auto. omega. intros. eapply stores_in_frame_valid; eauto with mem. intros. eapply stores_in_frame_perm; eauto with mem. - eapply Mem.perm_free_1; eauto. left; unfold block; omega. eauto with mem. - intros. rewrite <- H1. - transitivity (Mem.load chunk m3' b ofs). eapply stores_in_frame_contents; eauto. - transitivity (Mem.load chunk m2' b ofs). eapply Mem.load_free; eauto. left; unfold block; omega. + intros. rewrite <- H1. transitivity (Mem.load chunk m2' b ofs). eapply stores_in_frame_contents; eauto. eapply Mem.load_alloc_unchanged; eauto. red. congruence. auto with coqlib. @@ -2777,7 +2741,6 @@ Proof. eapply Genv.init_mem_transf_partial; eauto. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. eauto. - eexact FIND. econstructor; eauto. eapply Genv.initmem_inject; eauto. apply match_stacks_empty with (Mem.nextblock m0). omega. omega. @@ -2807,7 +2770,7 @@ Proof. Qed. Theorem transf_program_correct: - forward_simulation (Linear.semantics prog) (Mach.semantics tprog). + forward_simulation (Linear.semantics prog) (Mach.semantics return_address_offset tprog). Proof. eapply forward_simulation_plus. eexact symbols_preserved. diff --git a/driver/Compiler.v b/driver/Compiler.v index c8fb8c5..ea277ac 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -249,7 +249,8 @@ Proof. eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply RREproof.transf_program_correct. eauto. - eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto. + eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. + eexact Asmgenproof.return_address_exists. eassumption. eauto. apply Asmgenproof.transf_program_correct; eauto. split. auto. apply forward_to_backward_simulation. auto. @@ -70,7 +70,7 @@ Coercion CR: crbit >-> preg. (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) -Notation "'SP'" := ESP (only parsing). +Notation SP := ESP (only parsing). (** ** Instruction set. *) diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index e43552e..83918f4 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -84,8 +84,8 @@ Proof. Qed. Lemma exec_straight_exec: - forall f c ep tf tc c' rs m rs' m', - transl_code_at_pc ge (rs PC) f c ep tf tc -> + forall fb f c ep tf tc c' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> exec_straight tge tf tc rs m c' rs' m' -> plus step tge (State rs m) E0 (State rs' m'). Proof. @@ -96,11 +96,11 @@ Proof. Qed. Lemma exec_straight_at: - forall f c ep tf tc c' ep' tc' rs m rs' m', - transl_code_at_pc ge (rs PC) f c ep tf tc -> + forall fb f c ep tf tc c' ep' tc' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> transl_code f c' ep' = OK tc' -> exec_straight tge tf tc rs m tc' rs' m' -> - transl_code_at_pc ge (rs' PC) f c' ep' tf tc'. + transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'. Proof. intros. inv H. exploit exec_straight_steps_2; eauto. @@ -110,39 +110,6 @@ Proof. rewrite PC'. constructor; auto. 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. - (** The following lemmas show that the translation from Mach to Asm preserves labels, in the sense that the following diagram commutes: << @@ -157,120 +124,148 @@ Qed. >> The proof demands many boring lemmas showing that Asm constructor functions do not introduce new labels. + + In passing, we also prove a "is tail" property of the generated Asm code. *) Section TRANSL_LABEL. -Variable lbl: label. +Definition nolabel (i: instruction) := + match i with Plabel _ => False | _ => True end. + +Hint Extern 1 (nolabel _) => exact I : labels. + +Lemma tail_nolabel_cons: + forall i c k, + nolabel i -> 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. + + +Ltac TailNoLabel := + eauto with labels; + match goal with + | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel] + | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel + | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabel + | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel + | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel + | _ => idtac + end. Remark mk_mov_label: - forall rd rs k c, mk_mov rd rs k = OK c -> find_label lbl c = find_label lbl k. + forall rd rs k c, mk_mov rd rs k = OK c -> tail_nolabel k c. Proof. unfold mk_mov; intros. - destruct rd; try discriminate; destruct rs; inv H; auto. + destruct rd; try discriminate; destruct rs; TailNoLabel. Qed. +Hint Resolve mk_mov_label: labels. Remark mk_shift_label: forall f r1 r2 k c, mk_shift f r1 r2 k = OK c -> - (forall r, is_label lbl (f r) = false) -> - find_label lbl c = find_label lbl k. + (forall r, nolabel (f r)) -> + tail_nolabel k c. Proof. - unfold mk_shift; intros. - destruct (ireg_eq r2 ECX). monadInv H; simpl; rewrite H0; auto. - destruct (ireg_eq r1 ECX); monadInv H; simpl; rewrite H0; auto. + unfold mk_shift; intros. TailNoLabel. Qed. +Hint Resolve mk_shift_label: labels. Remark mk_mov2_label: forall r1 r2 r3 r4 k, - find_label lbl (mk_mov2 r1 r2 r3 r4 k) = find_label lbl k. + tail_nolabel k (mk_mov2 r1 r2 r3 r4 k). Proof. intros; unfold mk_mov2. - destruct (ireg_eq r1 r2); auto. - destruct (ireg_eq r3 r4); auto. - destruct (ireg_eq r3 r2); auto. - destruct (ireg_eq r1 r4); auto. + destruct (ireg_eq r1 r2); TailNoLabel. + destruct (ireg_eq r3 r4); TailNoLabel. + destruct (ireg_eq r3 r2); TailNoLabel. + destruct (ireg_eq r1 r4); TailNoLabel. Qed. +Hint Resolve mk_mov2_label: labels. Remark mk_div_label: forall f r1 r2 k c, mk_div f r1 r2 k = OK c -> - (forall r, is_label lbl (f r) = false) -> - find_label lbl c = find_label lbl k. + (forall r, nolabel (f r)) -> + tail_nolabel k c. Proof. - unfold mk_div; intros. - destruct (ireg_eq r1 EAX). - destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. - monadInv H; simpl. rewrite mk_mov2_label. simpl; rewrite H0; auto. + unfold mk_div; intros. TailNoLabel. + eapply tail_nolabel_trans. 2: apply mk_mov2_label. TailNoLabel. Qed. +Hint Resolve mk_div_label: labels. Remark mk_mod_label: forall f r1 r2 k c, mk_mod f r1 r2 k = OK c -> - (forall r, is_label lbl (f r) = false) -> - find_label lbl c = find_label lbl k. + (forall r, nolabel (f r)) -> + tail_nolabel k c. Proof. - unfold mk_mod; intros. - destruct (ireg_eq r1 EAX). - destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. - monadInv H; simpl. rewrite mk_mov2_label. simpl; rewrite H0; auto. + unfold mk_mod; intros. TailNoLabel. + eapply tail_nolabel_trans. 2: apply mk_mov2_label. TailNoLabel. Qed. +Hint Resolve mk_mod_label: labels. Remark mk_shrximm_label: - forall r n k c, mk_shrximm r n k = OK c -> find_label lbl c = find_label lbl k. + forall r n k c, mk_shrximm r n k = OK c -> tail_nolabel k c. Proof. - intros. monadInv H; auto. + intros. monadInv H; TailNoLabel. Qed. +Hint Resolve mk_shrximm_label: labels. Remark mk_intconv_label: forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> - (forall r r', is_label lbl (f r r') = false) -> - find_label lbl c = find_label lbl k. + (forall r r', nolabel (f r r')) -> + tail_nolabel k c. Proof. - unfold mk_intconv; intros. destruct (low_ireg r2); inv H; simpl; rewrite H0; auto. + unfold mk_intconv; intros. TailNoLabel. Qed. +Hint Resolve mk_intconv_label: labels. Remark mk_smallstore_label: forall f addr r k c, mk_smallstore f addr r k = OK c -> - (forall r addr, is_label lbl (f r addr) = false) -> - find_label lbl c = find_label lbl k. + (forall r addr, nolabel (f r addr)) -> + tail_nolabel k c. Proof. - unfold mk_smallstore; intros. destruct (low_ireg r). - monadInv H; simpl; rewrite H0; auto. - destruct (addressing_mentions addr ECX); monadInv H; simpl; rewrite H0; auto. + unfold mk_smallstore; intros. TailNoLabel. Qed. +Hint Resolve mk_smallstore_label: labels. Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> - find_label lbl c = find_label lbl k. + tail_nolabel k c. Proof. - unfold loadind; intros. destruct ty. - monadInv H; auto. - destruct (preg_of dst); inv H; auto. + unfold loadind; intros. destruct ty. + TailNoLabel. + destruct (preg_of dst); TailNoLabel. Qed. Remark storeind_label: forall base ofs ty src k c, storeind src base ofs ty k = OK c -> - find_label lbl c = find_label lbl k. + tail_nolabel k c. Proof. - unfold storeind; intros. destruct ty. - monadInv H; auto. - destruct (preg_of src); inv H; auto. + unfold storeind; intros. destruct ty. + TailNoLabel. + destruct (preg_of src); TailNoLabel. Qed. Remark mk_setcc_label: forall xc rd k, - find_label lbl (mk_setcc xc rd k) = find_label lbl k. + tail_nolabel k (mk_setcc xc rd k). Proof. - intros. destruct xc; simpl; auto; destruct (ireg_eq rd EDX); auto. + intros. destruct xc; simpl; destruct (ireg_eq rd EDX); TailNoLabel. Qed. Remark mk_jcc_label: forall xc lbl' k, - find_label lbl (mk_jcc xc lbl' k) = find_label lbl k. + tail_nolabel k (mk_jcc xc lbl' k). Proof. - intros. destruct xc; auto. + intros. destruct xc; simpl; TailNoLabel. Qed. +(* Ltac ArgsInv := match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -278,88 +273,78 @@ Ltac ArgsInv := | [ H: bind _ _ = OK _ |- _ ] => monadInv H; ArgsInv | _ => idtac end. +*) Remark transl_cond_label: forall cond args k c, transl_cond cond args k = OK c -> - find_label lbl c = find_label lbl k. + tail_nolabel k c. Proof. - unfold transl_cond; intros. - destruct cond; ArgsInv; auto. - destruct (Int.eq_dec i Int.zero); auto. - destruct c0; auto. - destruct c0; auto. + unfold transl_cond; intros. + destruct cond; TailNoLabel. + destruct (Int.eq_dec i Int.zero); TailNoLabel. + destruct c0; simpl; TailNoLabel. + destruct c0; simpl; TailNoLabel. Qed. Remark transl_op_label: forall op args r k c, transl_op op args r k = OK c -> - find_label lbl c = find_label lbl k. + tail_nolabel k c. Proof. - unfold transl_op; intros. destruct op; ArgsInv; auto. - eapply mk_mov_label; eauto. - destruct (Int.eq_dec i Int.zero); auto. - destruct (Float.eq_dec f Float.zero); auto. - eapply mk_intconv_label; eauto. - eapply mk_intconv_label; eauto. - eapply mk_intconv_label; eauto. - eapply mk_intconv_label; eauto. - eapply mk_div_label; eauto. - eapply mk_div_label; eauto. - eapply mk_mod_label; eauto. - eapply mk_mod_label; eauto. - eapply mk_shift_label; eauto. - eapply mk_shift_label; eauto. - eapply mk_shrximm_label; eauto. - eapply mk_shift_label; eauto. - eapply trans_eq. eapply transl_cond_label; eauto. apply mk_setcc_label. + unfold transl_op; intros. destruct op; TailNoLabel. + destruct (Int.eq_dec i Int.zero); TailNoLabel. + destruct (Float.eq_dec f Float.zero); TailNoLabel. + eapply tail_nolabel_trans. eapply mk_setcc_label. eapply transl_cond_label. eauto. Qed. Remark transl_load_label: forall chunk addr args dest k c, transl_load chunk addr args dest k = OK c -> - find_label lbl c = find_label lbl k. + tail_nolabel k c. Proof. - intros. monadInv H. destruct chunk; monadInv EQ0; auto. + intros. monadInv H. destruct chunk; TailNoLabel. Qed. Remark transl_store_label: forall chunk addr args src k c, transl_store chunk addr args src k = OK c -> - find_label lbl c = find_label lbl k. + tail_nolabel k c. Proof. - intros. monadInv H. destruct chunk; monadInv EQ0; auto; eapply mk_smallstore_label; eauto. + intros. monadInv H. destruct chunk; TailNoLabel. Qed. Lemma transl_instr_label: forall f i ep k c, transl_instr f i ep k = OK c -> - find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. + match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end. Proof. - intros. generalize (Mach.is_label_correct lbl i). - case (Mach.is_label lbl i); intro. - subst i. monadInv H. simpl. rewrite peq_true. auto. Opaque loadind. - destruct i; simpl in H. + unfold transl_instr; intros; destruct i; TailNoLabel. eapply loadind_label; eauto. eapply storeind_label; eauto. - destruct ep. eapply loadind_label; eauto. monadInv H. eapply trans_eq; eapply loadind_label; eauto. + eapply loadind_label; eauto. + eapply tail_nolabel_trans; eapply loadind_label; eauto. eapply transl_op_label; eauto. eapply transl_load_label; eauto. eapply transl_store_label; eauto. - destruct s0; monadInv H; auto. - destruct s0; monadInv H; auto. - monadInv H; auto. - monadInv H; auto. - inv H; simpl. destruct (peq lbl l). congruence. auto. - monadInv H; auto. - eapply trans_eq. eapply transl_cond_label; eauto. apply mk_jcc_label. - monadInv H; auto. - monadInv H; auto. + destruct s0; TailNoLabel. + destruct s0; TailNoLabel. + eapply tail_nolabel_trans. eapply mk_jcc_label. eapply transl_cond_label; eauto. +Qed. + +Lemma transl_instr_label': + forall lbl f i ep k c, + transl_instr f i ep k = OK c -> + find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. +Proof. + intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply B). + intros. subst c. simpl. auto. Qed. Lemma transl_code_label: - forall f c ep tc, + forall lbl f c ep tc, transl_code f c ep = OK tc -> match Mach.find_label lbl c with | None => find_label lbl tc = None @@ -368,7 +353,7 @@ Lemma transl_code_label: Proof. induction c; simpl; intros. inv H. auto. - monadInv H. rewrite (transl_instr_label _ _ _ _ _ EQ0). + monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0). generalize (Mach.is_label_correct lbl a). destruct (Mach.is_label lbl a); intros. subst a. simpl in EQ. exists x; auto. @@ -376,7 +361,7 @@ Proof. Qed. Lemma transl_find_label: - forall f tf, + forall lbl f tf, transf_function f = OK tf -> match Mach.find_label lbl f.(Mach.fn_code) with | None => find_label lbl tf = None @@ -400,7 +385,7 @@ Lemma find_label_goto_label: Mach.find_label lbl f.(Mach.fn_code) = Some c' -> exists tc', exists rs', goto_label tf lbl rs m = Next rs' m - /\ transl_code_at_pc ge (rs' PC) f c' false tf tc' + /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' /\ forall r, r <> PC -> rs'#r = rs#r. Proof. intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. @@ -416,6 +401,21 @@ Proof. intros. apply Pregmap.gso; auto. Qed. +(** Existence of return addresses *) + +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. eapply Asmgenproof0.return_address_exists; eauto. +- intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. +- intros. monadInv H0. + destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. + exists x; exists true; split; auto. unfold fn_code. repeat constructor. +- exact transf_function_no_overflow. +Qed. + (** * Proof of semantic preservation *) (** Semantic preservation is proved using simulation diagrams @@ -436,49 +436,49 @@ Qed. Inductive match_states: Mach.state -> Asm.state -> Prop := | match_states_intro: - forall s f sp c ep ms m m' rs tf tc ra - (STACKS: match_stack ge s m m' ra sp) + forall s fb sp c ep ms m m' rs f tf tc + (STACKS: match_stack ge s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (MEXT: Mem.extends m m') - (AT: transl_code_at_pc ge (rs PC) f c ep tf tc) - (AG: agree ms (Vptr sp Int.zero) rs) - (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra) + (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) + (AG: agree ms sp rs) (DXP: ep = true -> rs#EDX = parent_sp s), - match_states (Mach.State s f (Vptr sp Int.zero) c ms m) + match_states (Mach.State s fb sp c ms m) (Asm.State rs m') | match_states_call: - forall s fd ms m m' rs fb - (STACKS: match_stack ge s m m' (rs RA) (Mem.nextblock m)) + forall s fb ms m m' rs + (STACKS: match_stack ge s) (MEXT: Mem.extends m m') (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (FUNCT: Genv.find_funct_ptr ge fb = Some fd) - (WTRA: Val.has_type (rs RA) Tint), - match_states (Mach.Callstate s fd ms m) + (ATLR: rs RA = parent_ra s), + match_states (Mach.Callstate s fb ms m) (Asm.State rs m') | match_states_return: forall s ms m m' rs - (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m)) + (STACKS: match_stack ge s) (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs), + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = parent_ra s), match_states (Mach.Returnstate s ms m) (Asm.State rs m'). Lemma exec_straight_steps: - forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra, - match_stack ge s m2 m2' ra sp -> + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, + match_stack ge s -> Mem.extends m2 m2' -> - retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> - transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> (forall k c (TR: transl_instr f i ep k = OK c), exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' - /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ agree ms2 sp rs2 /\ (edx_preserved ep i = true -> rs2#EDX = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'. + match_states (Mach.State s fb sp c ms2 m2) st'. Proof. - intros. inversion H2; subst. monadInv H7. + intros. inversion H2. subst. monadInv H7. exploit H3; eauto. intros [rs2 [A [B C]]]. exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. @@ -486,23 +486,23 @@ Proof. Qed. Lemma exec_straight_steps_goto: - forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra, - match_stack ge s m2 m2' ra sp -> + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', + match_stack ge s -> Mem.extends m2 m2' -> - retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> edx_preserved ep i = false -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ agree ms2 sp rs2 /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'. + match_states (Mach.State s fb sp c' ms2 m2) st'. Proof. - intros. inversion H3; subst. monadInv H9. + intros. inversion H3. subst. monadInv H9. exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. generalize (functions_transl _ _ _ H7 H8); intro FN. generalize (transf_function_no_overflow _ _ H8); intro NOOV. @@ -540,7 +540,7 @@ Definition measure (s: Mach.state) : nat := (** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) Theorem step_simulation: - forall S1 t S2, Mach.step ge S1 t S2 -> + forall S1 t S2, Mach.step return_address_offset ge S1 t S2 -> forall S1' (MS: match_states S1 S1'), (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. @@ -567,8 +567,6 @@ Proof. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [A B]]. left; eapply exec_straight_steps; eauto. - eapply match_stack_storev; eauto. - eapply retaddr_stored_at_storev; eauto. rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. exploit storeind_correct; eauto. intros [rs' [P Q]]. exists rs'; split. eauto. @@ -576,11 +574,12 @@ Proof. simpl; intros. rewrite Q; auto with asmgen. - (* Mgetparam *) + assert (f0 = f) by congruence; subst f0. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H. auto. + exploit Mem.loadv_extends. eauto. eexact H0. auto. intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. - exploit Mem.loadv_extends. eauto. eexact H0. auto. + exploit Mem.loadv_extends. eauto. eexact H1. auto. intros [v' [C D]]. Opaque loadind. left; eapply exec_straight_steps; eauto; intros. @@ -606,7 +605,7 @@ Opaque loadind. simpl; intros. rewrite U; auto. - (* Mop *) - assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). + assert (eval_operation tge sp op rs##args m = Some v). rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. @@ -621,7 +620,7 @@ Opaque loadind. simpl; congruence. - (* Mload *) - assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. @@ -633,15 +632,13 @@ Opaque loadind. simpl; congruence. - (* Mstore *) - assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [C D]]. left; eapply exec_straight_steps; eauto. - eapply match_stack_storev; eauto. - eapply retaddr_stored_at_storev; eauto. intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. @@ -649,79 +646,70 @@ Opaque loadind. simpl; congruence. - (* Mcall *) + assert (f0 = f) by congruence. subst f0. inv AT. assert (NOOV: list_length_z tf <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. - destruct ros as [rf|fid]; simpl in H; monadInv H3. + destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) - exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. - rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. - assert (rs0 x0 = Vptr bf Int.zero). - exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. - generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x). - econstructor; eauto. + assert (rs rf = Vptr f' Int.zero). + destruct (rs rf); try discriminate. + revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Int.zero). + exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). + econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. econstructor; eauto. econstructor; eauto. - rewrite <- H0. eexact TCA. - change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. - simpl. eapply agree_exten; eauto. intros. Simplifs. - rewrite <- H0. exact I. + eapply agree_sp_def; eauto. + simpl. eapply agree_exten; eauto. intros. Simplifs. + Simplifs. rewrite <- H2. auto. + (* Direct call *) - destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. - generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x). - econstructor; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). + econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. eauto. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto. econstructor; eauto. econstructor; eauto. - rewrite <- H0. eexact TCA. - change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simplifs. - auto. - rewrite <- H0. exact I. + Simplifs. rewrite <- H2. auto. - (* Mtailcall *) + assert (f0 = f) by congruence. subst f0. inv AT. assert (NOOV: list_length_z tf <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. - assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 ESP) (Vint (fn_retaddr_ofs f))) = Some ra). -Opaque Int.repr. - erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. - eapply rsa_contains; eauto. - exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. - assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). - apply match_stack_change_bound with stk. - eapply match_stack_free_left; eauto. - eapply match_stack_free_left; eauto. - eapply match_stack_free_right; eauto. - omega. - apply Z.lt_le_incl. change (Mem.valid_block m'' stk). - eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. - eapply retaddr_stored_at_valid; eauto. - destruct ros as [rf|fid]; simpl in H; monadInv H6. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) - exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. - rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. - assert (rs0 x0 = Vptr bf Int.zero). - exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. - generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. + assert (rs rf = Vptr f' Int.zero). + destruct (rs rf); try discriminate. + revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Int.zero). + exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. + generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1. left; econstructor; split. eapply plus_left. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. apply star_one. eapply exec_step_internal. - transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto. + transitivity (Val.add rs0#PC Vone). auto. rewrite <- H4. simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. traceEq. econstructor; eauto. @@ -729,23 +717,20 @@ Opaque Int.repr. eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. Simplifs. rewrite Pregmap.gso; auto. generalize (preg_of_not_SP rf). rewrite (ireg_of_eq _ _ EQ1). congruence. - change (Val.has_type ra Tint). eapply retaddr_stored_at_type; eauto. + (* Direct call *) - destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. - generalize (code_tail_next_int _ _ _ _ NOOV H7). intro CT1. + generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1. left; econstructor; split. eapply plus_left. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. apply star_one. eapply exec_step_internal. - transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto. + transitivity (Val.add rs0#PC Vone). auto. rewrite <- H4. simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. traceEq. econstructor; eauto. apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. - rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto. - change (Val.has_type ra Tint). eapply retaddr_stored_at_type; eauto. + rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. - (* Mbuiltin *) inv AT. monadInv H3. @@ -759,8 +744,6 @@ Opaque Int.repr. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - eapply match_stack_extcall; eauto. - intros; eapply external_call_max_perm; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss. simpl undef_regs. repeat rewrite Pregmap.gso; auto with asmgen. @@ -769,8 +752,6 @@ Opaque Int.repr. apply agree_nextinstr_nf. eapply agree_set_undef_mreg; eauto. rewrite Pregmap.gss. auto. intros. Simplifs. - eapply retaddr_stored_at_extcall; eauto. - intros; eapply external_call_max_perm; eauto. congruence. - (* Mannot *) @@ -786,18 +767,15 @@ Opaque Int.repr. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. - eapply match_stack_extcall; eauto. - intros; eapply external_call_max_perm; eauto. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr. auto. - eapply retaddr_stored_at_extcall; eauto. - intros; eapply external_call_max_perm; eauto. congruence. - (* Mgoto *) - inv AT. monadInv H3. + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H4. exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. @@ -809,6 +787,7 @@ Opaque Int.repr. congruence. - (* Mcond true *) + assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps_goto; eauto. intros. simpl in TR. @@ -841,7 +820,7 @@ Opaque Int.repr. (* jcc2 *) destruct (eval_testcond c1 rs') as [b1|] eqn:TC1; destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B. - destruct (andb_prop _ _ H2). subst. + destruct (andb_prop _ _ H3). subst. exists (Pjcc2 c1 c2 lbl); exists k; exists rs'. split. eexact A. split. eapply agree_exten_temps; eauto. @@ -883,9 +862,10 @@ Opaque Int.repr. rewrite H1; congruence. - (* Mjumptable *) - inv AT. monadInv H5. + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H6. exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H4); intro NOOV. + generalize (transf_function_no_overflow _ _ H5); intro NOOV. exploit find_label_goto_label. eauto. eauto. instantiate (2 := rs0#ECX <- Vundef #EDX <- Vundef). repeat (rewrite Pregmap.gso by auto with asmgen). eauto. eauto. intros [tc' [rs' [A [B C]]]]. @@ -893,39 +873,30 @@ Opaque Int.repr. left; econstructor; split. apply plus_one. econstructor; eauto. eapply find_instr_tail; eauto. - simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eauto. + simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eauto. econstructor; eauto. eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simplifs. congruence. - (* Mreturn *) + assert (f0 = f) by congruence. subst f0. inv AT. assert (NOOV: list_length_z tf <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. - assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 ESP) (Vint (fn_retaddr_ofs f))) = Some ra). -Opaque Int.repr. - erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. - eapply rsa_contains; eauto. - exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. - assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). - apply match_stack_change_bound with stk. - eapply match_stack_free_left; eauto. - eapply match_stack_free_left; eauto. - eapply match_stack_free_right; eauto. omega. - apply Z.lt_le_incl. change (Mem.valid_block m'' stk). - eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. - eapply retaddr_stored_at_valid; eauto. - monadInv H5. + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + monadInv H6. exploit code_tail_next_int; eauto. intro CT1. left; econstructor; split. eapply plus_left. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. apply star_one. eapply exec_step_internal. - transitivity (Val.add rs0#PC Vone). auto. rewrite <- H2. simpl. eauto. + transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. traceEq. constructor; auto. @@ -939,30 +910,17 @@ Opaque Int.repr. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. - assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto). - exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. + exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. - exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. - auto. auto. auto. auto. eauto. - intros [m3' [P [Q R]]]. + exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. + intros [m3' [P Q]]. left; econstructor; split. apply plus_one. econstructor; eauto. - subst x; simpl. rewrite Int.unsigned_zero. simpl. eauto. + subst x; simpl. eauto. +Opaque Int.repr. simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F. - rewrite Int.add_zero_l. rewrite P. eauto. + simpl in P. rewrite ATLR. rewrite P. eauto. econstructor; eauto. - assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). - rewrite <- STK in STACKS. simpl in F. simpl in H1. - eapply match_stack_invariant; eauto. - intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. - eapply Mem.perm_store_2; eauto. unfold block; omega. - intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. - eapply Mem.perm_alloc_1; eauto. - intros. erewrite Mem.load_store_other. 2: eauto. - erewrite Mem.load_store_other. 2: eauto. - eapply Mem.load_alloc_other; eauto. - left; unfold block; omega. - left; unfold block; omega. unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. rewrite ATPC. simpl. constructor; eauto. subst x. unfold fn_code. eapply code_tail_next_int. rewrite list_length_z_cons. omega. @@ -985,10 +943,6 @@ Opaque Int.repr. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). - eapply match_stack_extcall; eauto. - intros. eapply external_call_max_perm; eauto. - eapply external_call_nextblock; eauto. unfold loc_external_result. eapply agree_set_mreg; eauto. rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. @@ -996,8 +950,8 @@ Opaque Int.repr. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. - econstructor; eauto. congruence. + right. split. omega. split. auto. + econstructor; eauto. rewrite ATPC; eauto. congruence. Qed. Lemma transf_initial_states: @@ -1005,21 +959,19 @@ Lemma transf_initial_states: exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. unfold ge0 in *. - exploit functions_translated; eauto. intros [tf [A B]]. econstructor; split. econstructor. eapply Genv.init_mem_transf_partial; eauto. replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) - with (Vptr b Int.zero). + with (Vptr fb Int.zero). econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. intros. rewrite Regmap.gi. auto. - reflexivity. - exact I. + split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. unfold symbol_offset. - rewrite (transform_partial_program_main _ _ TRANSF). - rewrite symbols_preserved. unfold ge; rewrite H1. auto. + rewrite (transform_partial_program_main _ _ TRANSF). + rewrite symbols_preserved. + unfold ge; rewrite H1. auto. Qed. Lemma transf_final_states: @@ -1033,7 +985,7 @@ Proof. Qed. Theorem transf_program_correct: - forward_simulation (Mach.semantics prog) (Asm.semantics tprog). + forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). eexact symbols_preserved. |