From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Stackingproof.v | 2816 +++++++++++++++++++++++++++++++---------------- 1 file changed, 1877 insertions(+), 939 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 5b06c71..c32886c 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -12,13 +12,7 @@ (** Correctness proof for the translation from Linear to Mach. *) -(** This file proves semantic preservation for the [Stacking] pass. - For the target language Mach, we use the abstract semantics - given in file [Machabstr], where a part of the activation record - is not resident in memory. Combined with the semantic equivalence - result between the two Mach semantics (see file [Machabstr2concr]), - the proof in this file also shows semantic preservation with - respect to the concrete Mach semantics. *) +(** This file proves semantic preservation for the [Stacking] pass. *) Require Import Coqlib. Require Import Maps. @@ -36,15 +30,13 @@ Require LTL. Require Import Linear. Require Import Lineartyping. Require Import Mach. -Require Import Machabstr. +Require Import Machconcr. Require Import Bounds. Require Import Conventions. Require Import Stacklayout. Require Import Stacking. -(** * Properties of frames and frame accesses *) - -(** ``Good variable'' properties for frame accesses. *) +(** * Properties of frame offsets *) Lemma typesize_typesize: forall ty, AST.typesize ty = 4 * Locations.typesize ty. @@ -52,6 +44,12 @@ Proof. destruct ty; auto. Qed. +Remark size_type_chunk: + forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty. +Proof. + destruct ty; reflexivity. +Qed. + Section PRESERVATION. Variable prog: Linear.program. @@ -63,7 +61,6 @@ Let tge := Genv.globalenv tprog. Section FRAME_PROPERTIES. -Variable stack: list Machabstr.stackframe. Variable f: Linear.function. Let b := function_bounds f. Let fe := make_env b. @@ -74,27 +71,30 @@ Lemma unfold_transf_function: tf = Mach.mkfunction f.(Linear.fn_sig) (transl_body f fe) - f.(Linear.fn_stacksize) fe.(fe_size) (Int.repr fe.(fe_ofs_link)) (Int.repr fe.(fe_ofs_retaddr)). Proof. generalize TRANSF_F. unfold transf_function. - case (zlt (Linear.fn_stacksize f) 0). intros; discriminate. - case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). + destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))). intros; discriminate. intros. unfold fe. unfold b. congruence. Qed. -Lemma size_no_overflow: fe.(fe_size) <= -Int.min_signed. +Lemma size_no_overflow: fe.(fe_size) <= Int.max_unsigned. Proof. generalize TRANSF_F. unfold transf_function. - case (zlt (Linear.fn_stacksize f) 0). intros; discriminate. - case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). + destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))). intros; discriminate. - intros. unfold fe, b. omega. + intros. unfold fe. unfold b. omega. Qed. +Remark bound_stack_data_stacksize: + f.(Linear.fn_stacksize) <= b.(bound_stack_data). +Proof. + unfold b, function_bounds, bound_stack_data. apply Zmax1. +Qed. + (** A frame index is valid if it lies within the resource bounds of the current function. *) @@ -135,18 +135,26 @@ Definition index_diff (idx1 idx2: frame_index) : Prop := | _, _ => True end. +Lemma index_diff_sym: + forall idx1 idx2, index_diff idx1 idx2 -> index_diff idx2 idx1. +Proof. + unfold index_diff; intros. + destruct idx1; destruct idx2; intuition. +Qed. + Ltac AddPosProps := generalize (bound_int_local_pos b); intro; generalize (bound_float_local_pos b); intro; generalize (bound_int_callee_save_pos b); intro; generalize (bound_float_callee_save_pos b); intro; generalize (bound_outgoing_pos b); intro; - generalize (align_float_part b); intro. + generalize (bound_stack_data_pos b); intro. -Lemma size_pos: fe.(fe_size) >= 0. +Lemma size_pos: 0 <= fe.(fe_size). Proof. + generalize (frame_env_separated b). intuition. AddPosProps. - unfold fe, make_env, fe_size. omega. + unfold fe. omega. Qed. Opaque function_bounds. @@ -155,61 +163,79 @@ Lemma offset_of_index_disj: forall idx1 idx2, index_valid idx1 -> index_valid idx2 -> index_diff idx1 idx2 -> - offset_of_index fe idx1 + 4 * typesize (type_of_index idx1) <= offset_of_index fe idx2 \/ - offset_of_index fe idx2 + 4 * typesize (type_of_index idx2) <= offset_of_index fe idx1. + offset_of_index fe idx1 + AST.typesize (type_of_index idx1) <= offset_of_index fe idx2 \/ + offset_of_index fe idx2 + AST.typesize (type_of_index idx2) <= offset_of_index fe idx1. Proof. + intros idx1 idx2 V1 V2 DIFF. + generalize (frame_env_separated b). intuition. fold fe in H. AddPosProps. - intros. destruct idx1; destruct idx2; try (destruct t); try (destruct t0); - unfold offset_of_index, fe, make_env, - fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, - fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg, - type_of_index, typesize; - simpl in H5; simpl in H6; simpl in H7; + unfold offset_of_index, type_of_index, AST.typesize; + simpl in V1; simpl in V2; simpl in DIFF; try omega. assert (z <> z0). intuition auto. omega. assert (z <> z0). intuition auto. omega. Qed. +Lemma offset_of_index_disj_stack_data_1: + forall idx, + index_valid idx -> + offset_of_index fe idx + AST.typesize (type_of_index idx) <= fe.(fe_stack_data) + \/ fe.(fe_stack_data) + b.(bound_stack_data) <= offset_of_index fe idx. +Proof. + intros idx V. + generalize (frame_env_separated b). intuition. fold fe in H. + AddPosProps. + destruct idx; try (destruct t); + unfold offset_of_index, type_of_index, AST.typesize; + simpl in V; + omega. +Qed. + +Lemma offset_of_index_disj_stack_data_2: + forall idx, + index_valid idx -> + offset_of_index fe idx + AST.typesize (type_of_index idx) <= fe.(fe_stack_data) + \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= offset_of_index fe idx. +Proof. + intros. + exploit offset_of_index_disj_stack_data_1; eauto. + generalize bound_stack_data_stacksize. + omega. +Qed. + +(** Alignment properties *) + Remark aligned_4_4x: forall x, (4 | 4 * x). Proof. intro. exists x; ring. Qed. Remark aligned_4_8x: forall x, (4 | 8 * x). Proof. intro. exists (x * 2); ring. Qed. -Remark aligned_4_align8: forall x, (4 | align x 8). -Proof. - intro. apply Zdivides_trans with 8. exists 2; auto. apply align_divides. omega. -Qed. - -Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r - aligned_4_4x aligned_4_8x aligned_4_align8: align_4. +Remark aligned_8_4: + forall x, (8 | x) -> (4 | x). +Proof. intros. apply Zdivides_trans with 8; auto. exists 2; auto. Qed. +Hint Resolve Zdivide_0 Zdivide_refl Zdivide_plus_r + aligned_4_4x aligned_4_8x aligned_8_4: align_4. Hint Extern 4 (?X | ?Y) => (exists (Y/X); reflexivity) : align_4. Lemma offset_of_index_aligned: forall idx, (4 | offset_of_index fe idx). Proof. intros. - destruct idx; - unfold offset_of_index, fe, make_env, - fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, - fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; + generalize (frame_env_aligned b). intuition. fold fe in H. intuition. + destruct idx; try (destruct t); + unfold offset_of_index, type_of_index, AST.typesize; auto with align_4. - destruct t; auto with align_4. Qed. -Lemma frame_size_aligned: - (4 | fe_size fe). +Lemma fe_stack_data_aligned: + (4 | fe_stack_data fe). Proof. - unfold offset_of_index, fe, make_env, - fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, - fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg; - auto with align_4. + intros. + generalize (frame_env_aligned b). intuition. fold fe in H. intuition. Qed. (** The following lemmas give sufficient conditions for indices @@ -262,19 +288,26 @@ Lemma offset_of_index_valid: forall idx, index_valid idx -> 0 <= offset_of_index fe idx /\ - offset_of_index fe idx + 4 * typesize (type_of_index idx) <= fe.(fe_size). + offset_of_index fe idx + AST.typesize (type_of_index idx) <= fe.(fe_size). Proof. + intros idx V. + generalize (frame_env_separated b). intros [A B]. fold fe in A. fold fe in B. + AddPosProps. + destruct idx; try (destruct t); + unfold offset_of_index, type_of_index, AST.typesize; + simpl in V; + omega. +Qed. + +(** The image of the Linear stack data block lies within the bounds of the frame. *) + +Lemma stack_data_offset_valid: + 0 <= fe.(fe_stack_data) /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size). +Proof. + generalize (frame_env_separated b). intros [A B]. fold fe in A. fold fe in B. AddPosProps. - intros. - destruct idx; try destruct t; - unfold offset_of_index, fe, make_env, - fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, - fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg, - type_of_index, typesize; - unfold index_valid in H5; simpl typesize in H5; omega. -Qed. +Qed. (** Offsets for valid index are representable as signed machine integers without loss of precision. *) @@ -282,142 +315,248 @@ Qed. Lemma offset_of_index_no_overflow: forall idx, index_valid idx -> - Int.signed (Int.repr (offset_of_index fe idx)) = offset_of_index fe idx. + Int.unsigned (Int.repr (offset_of_index fe idx)) = offset_of_index fe idx. Proof. intros. generalize (offset_of_index_valid idx H). intros [A B]. - apply Int.signed_repr. - split. apply Zle_trans with 0; auto. compute; intro; discriminate. - assert (offset_of_index fe idx < fe_size fe). - generalize (typesize_pos (type_of_index idx)); intro. omega. - apply Zlt_succ_le. - change (Zsucc Int.max_signed) with (- Int.min_signed). - generalize size_no_overflow. omega. + apply Int.unsigned_repr. + generalize (AST.typesize_pos (type_of_index idx)). + generalize size_no_overflow. + omega. Qed. -(** Characterization of the [get_slot] and [set_slot] - operations in terms of the following [index_val] and [set_index_val] - frame access functions. *) +(** Likewise, for offsets within the Linear stack slot, after shifting. *) -Definition index_val (idx: frame_index) (fr: frame) := - fr (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)). +Lemma shifted_stack_offset_no_overflow: + forall ofs, + 0 <= Int.unsigned ofs < Linear.fn_stacksize f -> + Int.unsigned (Int.add ofs (Int.repr fe.(fe_stack_data))) + = Int.unsigned ofs + fe.(fe_stack_data). +Proof. + intros. unfold Int.add. + generalize size_no_overflow stack_data_offset_valid bound_stack_data_stacksize; intros. + AddPosProps. + replace (Int.unsigned (Int.repr (fe_stack_data fe))) with (fe_stack_data fe). + apply Int.unsigned_repr. omega. + symmetry. apply Int.unsigned_repr. omega. +Qed. -Definition set_index_val (idx: frame_index) (v: val) (fr: frame) := - update (type_of_index idx) (offset_of_index fe idx - tf.(fn_framesize)) v fr. +(** * Contents of frame slots *) -Lemma slot_valid_index: - forall idx, - index_valid idx -> idx <> FI_link -> idx <> FI_retaddr -> - slot_valid tf (type_of_index idx) (offset_of_index fe idx). +Inductive index_contains (m: mem) (sp: block) (idx: frame_index) (v: val) : Prop := + | index_contains_intro: + index_valid idx -> + Mem.load (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) = Some v -> + index_contains m sp idx v. + +Lemma index_contains_load_stack: + forall m sp idx v, + index_contains m sp idx v -> + load_stack m (Vptr sp Int.zero) (type_of_index idx) + (Int.repr (offset_of_index fe idx)) = Some v. +Proof. + intros. inv H. + unfold load_stack, Mem.loadv, Val.add. rewrite Int.add_commut. rewrite Int.add_zero. + rewrite offset_of_index_no_overflow; auto. +Qed. + +(** Good variable properties for [index_contains] *) + +Lemma gss_index_contains_base: + forall idx m m' sp v, + Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' -> + index_valid idx -> + exists v', + index_contains m' sp idx v' + /\ decode_encode_val v (chunk_of_type (type_of_index idx)) (chunk_of_type (type_of_index idx)) v'. +Proof. + intros. + exploit Mem.load_store_similar. eauto. reflexivity. + intros [v' [A B]]. + exists v'; split; auto. constructor; auto. +Qed. + +Lemma gss_index_contains: + forall idx m m' sp v, + Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' -> + index_valid idx -> + Val.has_type v (type_of_index idx) -> + index_contains m' sp idx v. +Proof. + intros. exploit gss_index_contains_base; eauto. intros [v' [A B]]. + assert (v' = v). + destruct v; destruct (type_of_index idx); simpl in *; intuition congruence. + subst v'. auto. +Qed. + +Lemma gso_index_contains: + forall idx m m' sp v idx' v', + Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' -> + index_valid idx -> + index_contains m sp idx' v' -> + index_diff idx idx' -> + index_contains m' sp idx' v'. +Proof. + intros. inv H1. constructor; auto. + rewrite <- H4. eapply Mem.load_store_other; eauto. + right. repeat rewrite size_type_chunk. + apply offset_of_index_disj; auto. apply index_diff_sym; auto. +Qed. + +Lemma store_other_index_contains: + forall chunk m blk ofs v' m' sp idx v, + Mem.store chunk m blk ofs v' = Some m' -> + blk <> sp \/ + (fe.(fe_stack_data) <= ofs /\ ofs + size_chunk chunk <= fe.(fe_stack_data) + f.(Linear.fn_stacksize)) -> + index_contains m sp idx v -> + index_contains m' sp idx v. +Proof. + intros. inv H1. constructor; auto. rewrite <- H3. + eapply Mem.load_store_other; eauto. + destruct H0. auto. right. + exploit offset_of_index_disj_stack_data_2; eauto. intros. + rewrite size_type_chunk. + omega. +Qed. + +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 -> + Mem.perm m sp ofs Freeable. + +Lemma offset_of_index_perm: + forall m sp idx, + 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)) Freeable. Proof. intros. - destruct (offset_of_index_valid idx H) as [A B]. - rewrite <- typesize_typesize in B. - rewrite unfold_transf_function; constructor. - auto. unfold fn_framesize. auto. - unfold fn_link_ofs. change (fe_ofs_link fe) with (offset_of_index fe FI_link). - rewrite offset_of_index_no_overflow. - exploit (offset_of_index_disj idx FI_link). - auto. exact I. red. destruct idx; auto || congruence. - intro. rewrite typesize_typesize. assumption. - exact I. - unfold fn_retaddr_ofs. change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr). - rewrite offset_of_index_no_overflow. - exploit (offset_of_index_disj idx FI_retaddr). - auto. exact I. red. destruct idx; auto || congruence. - intro. rewrite typesize_typesize. assumption. - exact I. - apply offset_of_index_aligned. -Qed. - -Lemma get_slot_index: - forall fr idx ty v, - index_valid idx -> idx <> FI_link -> idx <> FI_retaddr -> - ty = type_of_index idx -> - v = index_val idx fr -> - get_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe idx))) v. -Proof. - intros. subst v; subst ty. rewrite offset_of_index_no_overflow; auto. - unfold index_val. apply get_slot_intro; auto. - apply slot_valid_index; auto. -Qed. - -Lemma set_slot_index: - forall fr idx v, - index_valid idx -> idx <> FI_link -> idx <> FI_retaddr -> - set_slot tf fr (type_of_index idx) (Int.signed (Int.repr (offset_of_index fe idx))) - v (set_index_val idx v fr). -Proof. - intros. rewrite offset_of_index_no_overflow; auto. - apply set_slot_intro. - apply slot_valid_index; auto. - unfold set_index_val. auto. -Qed. - -(** ``Good variable'' properties for [index_val] and [set_index_val]. *) - -Lemma get_set_index_val_same: - forall fr idx v, - index_val idx (set_index_val idx v fr) = v. -Proof. - intros. unfold index_val, set_index_val. apply update_same. -Qed. - -Lemma get_set_index_val_other: - forall fr idx idx' v, - index_valid idx -> index_valid idx' -> index_diff idx idx' -> - index_val idx' (set_index_val idx v fr) = index_val idx' fr. -Proof. - intros. unfold index_val, set_index_val. apply update_other. - repeat rewrite typesize_typesize. - exploit (offset_of_index_disj idx idx'); auto. omega. -Qed. - -Lemma get_set_index_val_overlap: - forall ofs1 ty1 ofs2 ty2 v fr, - S (Outgoing ofs1 ty1) <> S (Outgoing ofs2 ty2) -> - Loc.overlap (S (Outgoing ofs1 ty1)) (S (Outgoing ofs2 ty2)) = true -> - index_val (FI_arg ofs2 ty2) (set_index_val (FI_arg ofs1 ty1) v fr) = Vundef. -Proof. - intros. unfold index_val, set_index_val, offset_of_index, type_of_index. - assert (~(ofs1 + typesize ty1 <= ofs2 \/ ofs2 + typesize ty2 <= ofs1)). - destruct (orb_prop _ _ H0). apply Loc.overlap_aux_true_1. auto. - apply Loc.overlap_aux_true_2. auto. - unfold update. - destruct (zeq (fe_ofs_arg + 4 * ofs1 - fn_framesize tf) - (fe_ofs_arg + 4 * ofs2 - fn_framesize tf)). - destruct (typ_eq ty1 ty2). - elim H. decEq. decEq. omega. auto. - auto. - repeat rewrite typesize_typesize. - rewrite zle_false. apply zle_false. omega. omega. + exploit offset_of_index_valid; eauto. intros [A B]. + exploit offset_of_index_disj_stack_data_2; eauto. intros. + red; intros. apply H0. omega. omega. Qed. -(** Accessing stack-based arguments in the caller's frame. *) +Lemma store_index_succeeds: + forall m sp idx v, + 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'. +Proof. + intros. + destruct (Mem.valid_access_store m (chunk_of_type (type_of_index idx)) sp (offset_of_index fe idx) v) as [m' ST]. + constructor. + rewrite size_type_chunk. + apply Mem.range_perm_implies with Freeable; auto with mem. + apply offset_of_index_perm; auto. + replace (align_chunk (chunk_of_type (type_of_index idx))) with 4. + apply offset_of_index_aligned; auto. + destruct (type_of_index idx); auto. + exists m'; auto. +Qed. -Definition get_parent_slot (cs: list stackframe) (ofs: Z) (ty: typ) (v: val) : Prop := - get_slot (parent_function cs) (parent_frame cs) - ty (Int.signed (Int.repr (fe_ofs_arg + 4 * ofs))) v. +Lemma store_stack_succeeds: + forall m sp idx v m', + index_valid idx -> + Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' -> + store_stack m (Vptr sp Int.zero) (type_of_index idx) (Int.repr (offset_of_index fe idx)) v = Some m'. +Proof. + intros. unfold store_stack, Mem.storev, Val.add. + rewrite Int.add_commut. rewrite Int.add_zero. + rewrite offset_of_index_no_overflow; auto. +Qed. -(** * Agreement between location sets and Mach environments *) +(** A variant of [index_contains], up to a memory injection. *) -(** The following [agree] predicate expresses semantic agreement between: -- on the Linear side, the current location set [ls] and the location - set of the caller [ls0]; -- on the Mach side, a register set [rs], a frame [fr] and a call stack [cs]. -*) +Definition index_contains_inj (j: meminj) (m: mem) (sp: block) (idx: frame_index) (v: val) : Prop := + exists v', index_contains m sp idx v' /\ val_inject j v v'. -Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Prop := - mk_agree { - (** Machine registers have the same values on the Linear and Mach sides. *) - agree_reg: - forall r, ls (R r) = rs r; +Lemma gss_index_contains_inj: + forall j idx m m' sp v v', + Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v' = Some m' -> + index_valid idx -> + Val.has_type v (type_of_index idx) -> + val_inject j v v' -> + index_contains_inj j m' sp idx v. +Proof. + intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]]. + exists v''; split; auto. + inv H2; destruct (type_of_index idx); simpl in *; try contradiction; subst; auto. + econstructor; eauto. +Qed. - (** Machine registers outside the bounds of the current function - have the same values they had at function entry. In other terms, - these registers are never assigned. *) +Lemma gso_index_contains_inj: + forall j idx m m' sp v idx' v', + Mem.store (chunk_of_type (type_of_index idx)) m sp (offset_of_index fe idx) v = Some m' -> + index_valid idx -> + index_contains_inj j m sp idx' v' -> + index_diff idx idx' -> + index_contains_inj j m' sp idx' v'. +Proof. + intros. destruct H1 as [v'' [A B]]. exists v''; split; auto. + eapply gso_index_contains; eauto. +Qed. + +Lemma store_other_index_contains_inj: + forall j chunk m b ofs v' m' sp idx v, + Mem.store chunk m b ofs v' = Some m' -> + b <> sp \/ + (fe.(fe_stack_data) <= ofs /\ ofs + size_chunk chunk <= fe.(fe_stack_data) + f.(Linear.fn_stacksize)) -> + index_contains_inj j m sp idx v -> + index_contains_inj j m' sp idx v. +Proof. + intros. destruct H1 as [v'' [A B]]. exists v''; split; auto. + eapply store_other_index_contains; eauto. +Qed. + +Lemma index_contains_inj_incr: + forall j m sp idx v j', + index_contains_inj j m sp idx v -> + inject_incr j j' -> + index_contains_inj j' m sp idx v. +Proof. + intros. destruct H as [v'' [A B]]. exists v''; split; auto. eauto. +Qed. + +Lemma index_contains_inj_undef: + forall j m sp idx, + index_valid idx -> + frame_perm_freeable m sp -> + index_contains_inj j m sp idx Vundef. +Proof. + intros. + exploit (Mem.valid_access_load m (chunk_of_type (type_of_index idx)) sp (offset_of_index fe idx)). + constructor. + rewrite size_type_chunk. + apply Mem.range_perm_implies with Freeable; auto with mem. + apply offset_of_index_perm; auto. + replace (align_chunk (chunk_of_type (type_of_index idx))) with 4. + apply offset_of_index_aligned. destruct (type_of_index idx); auto. + intros [v C]. + exists v; split; auto. constructor; auto. +Qed. + +Hint Resolve store_other_index_contains_inj index_contains_inj_incr: stacking. + +(** * Agreement between location sets and Mach states *) + +(** Agreement with Mach register states *) + +Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop := + forall r, val_inject j (ls (R r)) (rs r). + +(** Agreement over data stored in memory *) + +Record agree_frame (j: meminj) (ls ls0: locset) + (m: mem) (sp: block) + (m': mem) (sp': block) + (parent retaddr: val) : Prop := + mk_agree_frame { + + (** Unused registers have the same value as in the caller *) agree_unused_reg: - forall r, ~(mreg_within_bounds b r) -> rs r = ls0 (R r); + forall r, ~(mreg_within_bounds b r) -> ls (R r) = ls0 (R r); (** Local and outgoing stack slots (on the Linear side) have the same values as the one loaded from the current Mach frame @@ -425,244 +564,440 @@ Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Pr agree_locals: forall ofs ty, slot_within_bounds f b (Local ofs ty) -> - ls (S (Local ofs ty)) = index_val (FI_local ofs ty) fr; + index_contains_inj j m' sp' (FI_local ofs ty) (ls (S (Local ofs ty))); agree_outgoing: forall ofs ty, slot_within_bounds f b (Outgoing ofs ty) -> - ls (S (Outgoing ofs ty)) = index_val (FI_arg ofs ty) fr; + index_contains_inj j m' sp' (FI_arg ofs ty) (ls (S (Outgoing ofs ty))); - (** Incoming stack slots (on the Linear side) have - the same values as the one loaded from the parent Mach frame - at the corresponding offsets. *) + (** Incoming stack slots have the same value as the + corresponding Outgoing stack slots in the caller *) agree_incoming: - forall ofs ty, - In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) -> - get_parent_slot cs ofs ty (ls (S (Incoming ofs ty))); + forall ofs ty, + In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) -> + ls (S (Incoming ofs ty)) = ls0 (S (Outgoing ofs ty)); + + (** 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 - on function entry. *) + in the caller. *) agree_saved_int: forall r, In r int_callee_save_regs -> index_int_callee_save r < b.(bound_int_callee_save) -> - index_val (FI_saved_int (index_int_callee_save r)) fr = ls0 (R r); + index_contains_inj j m' sp' (FI_saved_int (index_int_callee_save r)) (ls0 (R r)); agree_saved_float: forall r, In r float_callee_save_regs -> index_float_callee_save r < b.(bound_float_callee_save) -> - index_val (FI_saved_float (index_float_callee_save r)) fr = ls0 (R r) + index_contains_inj j m' sp' (FI_saved_float (index_float_callee_save r)) (ls0 (R r)); + + (** Mapping between the Linear stack pointer and the Mach stack pointer *) + agree_inj: + j sp = Some(sp', fe.(fe_stack_data)); + agree_inj_unique: + forall b delta, j b = Some(sp', delta) -> b = sp /\ delta = fe.(fe_stack_data); + + (** The Linear and Mach stack pointers are valid *) + agree_valid_linear: + Mem.valid_block m sp; + agree_valid_mach: + Mem.valid_block m' sp'; + + (** Bounds of the Linear stack data block *) + agree_bounds: + Mem.bounds m sp = (0, f.(Linear.fn_stacksize)); + + (** Permissions on the frame part of the Mach stack block *) + agree_perm: + frame_perm_freeable m' sp'; + + (** Current locset is well-typed *) + agree_wt_ls: + wt_locset ls }. -Hint Resolve agree_reg agree_unused_reg - agree_locals agree_outgoing agree_incoming - agree_saved_int agree_saved_float: stacking. +Hint Resolve agree_unused_reg agree_locals agree_outgoing agree_incoming + agree_link agree_retaddr agree_saved_int agree_saved_float + agree_valid_linear agree_valid_mach agree_perm + agree_wt_ls: stacking. -(** Values of registers and register lists. *) +(** Auxiliary predicate used at call points *) -Lemma agree_eval_reg: - forall ls ls0 rs fr cs r, - agree ls ls0 rs fr cs -> rs r = ls (R r). +Definition agree_callee_save (ls ls0: locset) : Prop := + forall l, + match l with + | R r => In r int_callee_save_regs \/ In r float_callee_save_regs + | S s => True + end -> + ls l = ls0 l. + +(** ** Properties of [agree_regs]. *) + +(** Values of registers *) + +Lemma agree_reg: + forall j ls rs r, + agree_regs j ls rs -> val_inject j (ls (R r)) (rs r). Proof. - intros. symmetry. eauto with stacking. + intros. auto. Qed. -Lemma agree_eval_regs: - forall ls ls0 rs fr cs rl, - agree ls ls0 rs cs fr -> rs##rl = reglist ls rl. +Lemma agree_reglist: + forall j ls rs rl, + agree_regs j ls rs -> val_list_inject j (reglist ls rl) (rs##rl). Proof. induction rl; simpl; intros. - auto. f_equal. eapply agree_eval_reg; eauto. auto. + auto. constructor. eauto with stacking. auto. Qed. -Hint Resolve agree_eval_reg agree_eval_regs: stacking. +Hint Resolve agree_reg agree_reglist: stacking. -(** Preservation of agreement under various assignments: - of machine registers, of local slots, of outgoing slots. *) +(** Preservation under assignments of machine registers. *) -Lemma agree_set_reg: - forall ls ls0 rs fr cs r v, - agree ls ls0 rs fr cs -> - mreg_within_bounds b r -> - agree (Locmap.set (R r) v ls) ls0 (Regmap.set r v rs) fr cs. -Proof. - intros. constructor; eauto with stacking. - intros. case (mreg_eq r r0); intro. - subst r0. rewrite Locmap.gss; rewrite Regmap.gss; auto. - rewrite Locmap.gso. rewrite Regmap.gso. eauto with stacking. - auto. red. auto. - intros. rewrite Regmap.gso. eauto with stacking. - red; intro; subst r0. contradiction. - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - intros. rewrite Locmap.gso. eauto with stacking. red. auto. -Qed. - -Lemma agree_set_local: - forall ls ls0 rs fr cs v ofs ty, - agree ls ls0 rs fr cs -> - slot_within_bounds f b (Local ofs ty) -> - exists fr', - set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_local ofs ty)))) v fr' /\ - agree (Locmap.set (S (Local ofs ty)) v ls) ls0 rs fr' cs. +Lemma agree_regs_set_reg: + forall j ls rs r v v', + agree_regs j ls rs -> + val_inject j v v' -> + agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs). Proof. - intros. - exists (set_index_val (FI_local ofs ty) v fr); split. - set (idx := FI_local ofs ty). - change ty with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_reg *) - intros. rewrite Locmap.gso. eauto with stacking. red; auto. - (* agree_local *) - intros. case (slot_eq (Local ofs ty) (Local ofs0 ty0)); intro. - rewrite <- e. rewrite Locmap.gss. - replace (FI_local ofs0 ty0) with (FI_local ofs ty). - symmetry. apply get_set_index_val_same. congruence. - assert (ofs <> ofs0 \/ ty <> ty0). - case (zeq ofs ofs0); intro. compare ty ty0; intro. - congruence. tauto. tauto. - rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - red. auto. - (* agree_outgoing *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - red; auto. red; auto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* agree_saved_int *) - intros. rewrite get_set_index_val_other; eauto with stacking. - red; auto. - (* agree_saved_float *) - intros. rewrite get_set_index_val_other; eauto with stacking. - red; auto. + intros; red; intros. + unfold Regmap.set. destruct (RegEq.eq r0 r). subst r0. + rewrite Locmap.gss; auto. + rewrite Locmap.gso; auto. red. auto. Qed. -Lemma agree_set_outgoing: - forall ls ls0 rs fr cs v ofs ty, - agree ls ls0 rs fr cs -> - slot_within_bounds f b (Outgoing ofs ty) -> - exists fr', - set_slot tf fr ty (Int.signed (Int.repr (offset_of_index fe (FI_arg ofs ty)))) v fr' /\ - agree (Locmap.set (S (Outgoing ofs ty)) v ls) ls0 rs fr' cs. +Lemma agree_regs_undef_temps: + forall j ls rs, + agree_regs j ls rs -> + agree_regs j (LTL.undef_temps ls) (undef_temps rs). +Proof. + unfold LTL.undef_temps, undef_temps. + change temporaries with (List.map R (int_temporaries ++ float_temporaries)). + generalize (int_temporaries ++ float_temporaries). + induction l; simpl; intros. + auto. + apply IHl. apply agree_regs_set_reg; auto. +Qed. + +Lemma agree_regs_undef_op: + forall op j ls rs, + agree_regs j ls rs -> + agree_regs j (Linear.undef_op op ls) (undef_op (transl_op fe op) rs). Proof. intros. - exists (set_index_val (FI_arg ofs ty) v fr); split. - set (idx := FI_arg ofs ty). - change ty with (type_of_index idx). - apply set_slot_index; unfold idx. auto with stacking. congruence. congruence. - constructor; eauto with stacking. - (* agree_reg *) - intros. rewrite Locmap.gso. eauto with stacking. red; auto. - (* agree_local *) - intros. rewrite Locmap.gso. rewrite get_set_index_val_other; eauto with stacking. - red; auto. red; auto. - (* agree_outgoing *) - intros. unfold Locmap.set. - case (Loc.eq (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intro. - (* same location *) - replace ofs0 with ofs by congruence. replace ty0 with ty by congruence. - symmetry. apply get_set_index_val_same. - (* overlapping locations *) - caseEq (Loc.overlap (S (Outgoing ofs ty)) (S (Outgoing ofs0 ty0))); intros. - symmetry. apply get_set_index_val_overlap; auto. - (* disjoint locations *) - rewrite get_set_index_val_other; eauto with stacking. - red. eapply Loc.overlap_aux_false_1; eauto. - (* agree_incoming *) - intros. rewrite Locmap.gso. eauto with stacking. red. auto. - (* saved ints *) - intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. - (* saved floats *) - intros. rewrite get_set_index_val_other; eauto with stacking. red; auto. + generalize (agree_regs_undef_temps _ _ _ H). + destruct op; simpl; auto. Qed. -Lemma agree_undef_regs: - forall rl ls ls0 rs fr cs, - agree ls ls0 rs fr cs -> - (forall r, In r rl -> In (R r) temporaries) -> - agree (Locmap.undef (List.map R rl) ls) ls0 (undef_regs rl rs) fr cs. +(** Preservation under assignment of stack slot *) + +Lemma agree_regs_set_slot: + forall j ls rs ss v, + agree_regs j ls rs -> + agree_regs j (Locmap.set (S ss) v ls) rs. Proof. - induction rl; intros; simpl. + intros; red; intros. rewrite Locmap.gso; auto. red. destruct ss; auto. +Qed. + +(** Preservation by increasing memory injections *) + +Lemma agree_regs_inject_incr: + forall j ls rs j', + agree_regs j ls rs -> inject_incr j j' -> agree_regs j' ls rs. +Proof. + intros; red; intros; eauto with stacking. +Qed. + +(** Preservation at function entry. *) + +Lemma agree_regs_call_regs: + forall j ls rs, + agree_regs j ls rs -> + agree_regs j (call_regs ls) (undef_temps rs). +Proof. + intros. + assert (agree_regs j (LTL.undef_temps ls) (undef_temps rs)). + apply agree_regs_undef_temps; auto. + unfold call_regs; intros; red; intros. + destruct (in_dec Loc.eq (R r) temporaries). auto. - eapply IHrl; eauto. - apply agree_set_reg; auto with coqlib. - assert (In (R a) temporaries) by auto with coqlib. - red. destruct (mreg_type a). - destruct (zlt (index_int_callee_save a) 0). - generalize (bound_int_callee_save_pos b). omega. - elim (int_callee_save_not_destroyed a). auto. apply index_int_callee_save_pos2; auto. - destruct (zlt (index_float_callee_save a) 0). - generalize (bound_float_callee_save_pos b). omega. - elim (float_callee_save_not_destroyed a). auto. apply index_float_callee_save_pos2; auto. - intros. apply H0. auto with coqlib. -Qed. - -Lemma agree_undef_temps: - forall ls ls0 rs fr cs, - agree ls ls0 rs fr cs -> - agree (LTL.undef_temps ls) ls0 (Mach.undef_temps rs) fr cs. -Proof. - intros. unfold undef_temps, LTL.undef_temps. + generalize (H0 r). unfold LTL.undef_temps. rewrite Locmap.guo. auto. + apply Loc.reg_notin; auto. +Qed. + +(** ** Properties of [agree_frame] *) + +(** Preservation under assignment of machine register. *) + +Lemma agree_frame_set_reg: + 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 ra. +Proof. + intros. inv H; constructor; auto; intros. + rewrite Locmap.gso. auto. red. intuition congruence. + rewrite Locmap.gso; auto. red; auto. + rewrite Locmap.gso; auto. red; auto. + rewrite Locmap.gso; auto. red; auto. + apply wt_setloc; auto. +Qed. + +Remark temporary_within_bounds: + forall r, In (R r) temporaries -> mreg_within_bounds b r. +Proof. + intros; red. destruct (mreg_type r). + destruct (zlt (index_int_callee_save r) 0). + generalize (bound_int_callee_save_pos b). omega. + exploit int_callee_save_not_destroyed. + left. eauto with coqlib. apply index_int_callee_save_pos2; auto. + contradiction. + destruct (zlt (index_float_callee_save r) 0). + generalize (bound_float_callee_save_pos b). omega. + exploit float_callee_save_not_destroyed. + left. eauto with coqlib. apply index_float_callee_save_pos2; auto. + contradiction. +Qed. + +Lemma agree_frame_undef_temps: + 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 until ra. + assert (forall regs ls, + incl (List.map R regs) temporaries -> + agree_frame j ls ls0 m sp m' sp' parent ra -> + agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra). + induction regs; simpl; intros. + auto. + apply IHregs; eauto with coqlib. + apply agree_frame_set_reg; auto. + apply temporary_within_bounds; eauto with coqlib. + red; auto. + intros. unfold LTL.undef_temps. change temporaries with (List.map R (int_temporaries ++ float_temporaries)). - apply agree_undef_regs; auto. + apply H; auto. apply incl_refl. +Qed. + +Lemma agree_frame_undef_op: + 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. - change temporaries with (List.map R (int_temporaries ++ float_temporaries)). - apply List.in_map. auto. + exploit agree_frame_undef_temps; eauto. destruct op; simpl; auto. Qed. -Lemma agree_undef_op: - forall op env ls ls0 rs fr cs, - agree ls ls0 rs fr cs -> - agree (Linear.undef_op op ls) ls0 (Mach.undef_op (transl_op env op) rs) fr cs. +(** Preservation by assignment to local slot *) + +Lemma agree_frame_set_local: + 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 retaddr. Proof. - intros. exploit agree_undef_temps; eauto. intro. - destruct op; simpl; auto. + intros. inv H. + change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3. + constructor; auto; intros. +(* unused *) + rewrite Locmap.gso; auto. red; auto. +(* local *) + unfold Locmap.set. simpl. destruct (Loc.eq (S (Local ofs ty)) (S (Local ofs0 ty0))). + inv e. eapply gss_index_contains_inj; eauto. + eapply gso_index_contains_inj. eauto. simpl; auto. eauto with stacking. + simpl. destruct (zeq ofs ofs0); auto. destruct (typ_eq ty ty0); auto. congruence. +(* outgoing *) + rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. + simpl; auto. red; auto. +(* incoming *) + 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 *) + eapply gso_index_contains_inj; eauto. simpl; auto. +(* valid *) + eauto with mem. +(* perm *) + red; intros. eapply Mem.perm_store_1; eauto. +(* wt *) + apply wt_setloc; auto. +Qed. + +(** Preservation by assignment to outgoing slot *) + +Lemma agree_frame_set_outgoing: + 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 retaddr. +Proof. + intros. inv H. + change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_arg ofs ty))) in H3. + constructor; auto; intros. +(* unused *) + rewrite Locmap.gso; auto. red; auto. +(* local *) + rewrite Locmap.gso. eapply gso_index_contains_inj; eauto. simpl; auto. red; auto. +(* outgoing *) + 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. + red; intros. eapply Mem.perm_store_1; eauto. + eapply gso_index_contains_inj; eauto. + red. eapply Loc.overlap_aux_false_1; eauto. +(* incoming *) + 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 *) + eapply gso_index_contains_inj; eauto with stacking. simpl; auto. +(* valid *) + eauto with mem stacking. +(* perm *) + red; intros. eapply Mem.perm_store_1; eauto. +(* wt *) + apply wt_setloc; auto. Qed. -Lemma agree_undef_getparam: - forall ls ls0 rs fr cs, - agree ls ls0 rs fr cs -> - agree (Locmap.set (R IT1) Vundef ls) ls0 (rs#IT1 <- Vundef) fr cs. +(** General invariance property with respect to memory changes. *) + +Lemma agree_frame_invariant: + 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) -> + (Mem.bounds m1 sp = Mem.bounds m sp) -> + (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> + (forall chunk ofs v, + ofs + size_chunk chunk <= fe.(fe_stack_data) \/ + fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> + Mem.load chunk m' sp' ofs = Some v -> + Mem.load chunk m1' sp' ofs = Some v) -> + (forall ofs p, + ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> + Mem.perm m' sp' ofs p -> Mem.perm m1' sp' ofs p) -> + agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. Proof. - intros. exploit (agree_undef_regs (IT1 :: nil)); eauto. - simpl; intros. intuition congruence. + intros. + assert (IC: forall idx v, + index_contains m' sp' idx v -> index_contains m1' sp' idx v). + intros. inv H5. + exploit offset_of_index_disj_stack_data_2; eauto. intros. + constructor; eauto. apply H3; auto. rewrite size_type_chunk; auto. + assert (ICI: forall idx v, + index_contains_inj j m' sp' idx v -> index_contains_inj j m1' sp' idx v). + intros. destruct H5 as [v' [A B]]. exists v'; split; auto. + inv H; constructor; auto; intros. + rewrite H1; auto. + red; intros. apply H4; auto. Qed. -Lemma agree_return_regs: - forall ls ls0 rs fr cs rs', - agree ls ls0 rs fr cs -> - (forall r, - ~In r int_callee_save_regs -> ~In r float_callee_save_regs -> - rs' r = rs r) -> - (forall r, - In r int_callee_save_regs \/ In r float_callee_save_regs -> - rs' r = ls0 (R r)) -> - (forall r, return_regs ls0 ls (R r) = rs' r). +(** A variant of the latter, for use with external calls *) + +Lemma agree_frame_extcall_invariant: + 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) -> + (Mem.bounds m1 sp = Mem.bounds m sp) -> + (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 retaddr. Proof. - intros; unfold return_regs. - case (In_dec Loc.eq (R r) temporaries); intro. - rewrite H0. eapply agree_reg; eauto. - apply int_callee_save_not_destroyed; auto. - apply float_callee_save_not_destroyed; auto. - case (In_dec Loc.eq (R r) destroyed_at_call); intro. - rewrite H0. eapply agree_reg; eauto. - apply int_callee_save_not_destroyed; auto. - apply float_callee_save_not_destroyed; auto. - symmetry; apply H1. - generalize (register_classification r); tauto. + intros. + assert (REACH: forall ofs, + ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> + loc_out_of_reach j m sp' ofs). + intros; red; intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst. + rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H). unfold fst, snd. omega. + eapply agree_frame_invariant; eauto. + intros. apply H3. intros. apply REACH. omega. auto. + intros. apply H3; auto. Qed. -(** Agreement over callee-save registers and stack locations *) +(** Preservation by parallel stores in the Linear and Mach codes *) -Definition agree_callee_save (ls1 ls2: locset) : Prop := - forall l, - match l with - | R r => In r int_callee_save_regs \/ In r float_callee_save_regs - | S s => True - end -> - ls2 l = ls1 l. +Lemma agree_frame_parallel_stores: + 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 retaddr. +Proof. +Opaque Int.add. + intros until m1'. intros AG MINJ VINJ STORE1 STORE2. + inv VINJ; simpl in *; try discriminate. + eapply agree_frame_invariant; eauto. + eauto with mem. + eapply Mem.bounds_store; eauto. + eauto with mem. + intros. rewrite <- H1. eapply Mem.load_store_other; eauto. + destruct (zeq sp' b2); auto. + subst b2. right. + exploit agree_inj_unique; eauto. intros [P Q]. subst b1 delta. + exploit Mem.store_valid_access_3. eexact STORE1. intros [A B]. + exploit Mem.range_perm_in_bounds. eexact A. generalize (size_chunk_pos chunk); omega. + rewrite (agree_bounds _ _ _ _ _ _ _ _ _ AG). unfold fst,snd. intros [C D]. + rewrite shifted_stack_offset_no_overflow. omega. + generalize (size_chunk_pos chunk); omega. + intros; eauto with mem. +Qed. + +(** Preservation by increasing memory injections (allocations and external calls) *) -Remark mreg_not_within_bounds: +Lemma agree_frame_inject_incr: + 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 retaddr. +Proof. + intros. inv H. constructor; auto; intros; eauto with stacking. + case_eq (j b0). + intros [b' delta'] EQ. rewrite (H0 _ _ _ EQ) in H. inv H. auto. + intros EQ. exploit H1. eauto. eauto. intros [A B]. contradiction. +Qed. + +Remark inject_alloc_separated: + forall j m1 m2 j' b1 b2 delta, + inject_incr j j' -> + j' b1 = Some(b2, delta) -> + (forall b, b <> b1 -> j' b = j b) -> + ~Mem.valid_block m1 b1 -> ~Mem.valid_block m2 b2 -> + inject_separated j j' m1 m2. +Proof. + intros. red. intros. + destruct (eq_block b0 b1). subst b0. rewrite H0 in H5; inv H5. tauto. + rewrite H1 in H5. congruence. auto. +Qed. + +(** Preservation at return points (when [ls] is changed but not [ls0]). *) + +Remark mreg_not_within_bounds_callee_save: forall r, ~mreg_within_bounds b r -> In r int_callee_save_regs \/ In r float_callee_save_regs. Proof. @@ -674,19 +1009,38 @@ Proof. generalize (bound_float_callee_save_pos b). omega. Qed. -Lemma agree_callee_save_agree: - forall ls ls1 ls2 rs fr cs, - agree ls ls1 rs fr cs -> - agree_callee_save ls1 ls2 -> - agree ls ls2 rs fr cs. +Lemma agree_frame_return: + 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 retaddr. Proof. - intros. inv H. constructor; auto. - intros. rewrite agree_unused_reg0; auto. - symmetry. apply H0. apply mreg_not_within_bounds; auto. - intros. rewrite (H0 (R r)); auto. - intros. rewrite (H0 (R r)); auto. + intros. red in H0. inv H; constructor; auto; intros. + rewrite H0; auto. apply mreg_not_within_bounds_callee_save; auto. + rewrite H0; auto. + rewrite H0; auto. + rewrite H0; auto. Qed. +(** Preservation at tailcalls (when [ls0] is changed but not [ls]). *) + +Lemma agree_frame_tailcall: + 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 retaddr. +Proof. + intros. red in H0. inv H; constructor; auto; intros. + rewrite <- H0; auto. apply mreg_not_within_bounds_callee_save; auto. + rewrite <- H0; auto. + rewrite <- H0; auto. + rewrite <- H0; auto. +Qed. + + +(** Properties of [agree_callee_save]. *) + Lemma agree_callee_save_return_regs: forall ls1 ls2, agree_callee_save (return_regs ls1 ls2) ls1. @@ -705,33 +1059,11 @@ Lemma agree_callee_save_set_result: agree_callee_save ls1 ls2 -> agree_callee_save (Locmap.set (R (loc_result sg)) v ls1) ls2. Proof. - intros; red; intros. rewrite H; auto. - symmetry; apply Locmap.gso. destruct l; simpl; auto. + intros; red; intros. rewrite <- H; auto. + apply Locmap.gso. destruct l; simpl; auto. red; intro. subst m. elim (loc_result_not_callee_save _ H0). Qed. -(** A variant of [agree] used for return frames. *) - -Definition agree_frame (ls ls0: locset) (fr: frame) (cs: list stackframe): Prop := - exists rs, agree ls ls0 rs fr cs. - -Lemma agree_frame_agree: - forall ls1 ls2 rs fr cs ls0, - agree_frame ls1 ls0 fr cs -> - agree_callee_save ls2 ls1 -> - (forall r, rs r = ls2 (R r)) -> - agree ls2 ls0 rs fr cs. -Proof. - intros. destruct H as [rs' AG]. inv AG. - constructor; auto. - intros. rewrite <- agree_unused_reg0; auto. - rewrite <- agree_reg0. rewrite H1. symmetry; apply H0. - apply mreg_not_within_bounds; auto. - intros. rewrite <- H0; auto. - intros. rewrite <- H0; auto. - intros. rewrite <- H0; auto. -Qed. - (** * Correctness of saving and restoring of callee-save registers *) (** The following lemmas show the correctness of the register saving @@ -745,17 +1077,35 @@ Variable bound: frame_env -> Z. Variable number: mreg -> Z. Variable mkindex: Z -> frame_index. Variable ty: typ. -Variable sp: val. +Variable j: meminj. +Variable cs: list stackframe. +Variable fb: block. +Variable sp: block. Variable csregs: list mreg. +Variable ls: locset. +Variable rs: regset. + +Inductive stores_in_frame: mem -> mem -> Prop := + | stores_in_frame_refl: forall m, + stores_in_frame m m + | stores_in_frame_step: forall m1 chunk ofs v m2 m3, + ofs + size_chunk chunk <= fe.(fe_stack_data) + \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> + Mem.store chunk m1 sp ofs v = Some m2 -> + stores_in_frame m2 m3 -> + stores_in_frame m1 m3. + +Remark stores_in_frame_trans: + forall m1 m2, stores_in_frame m1 m2 -> + forall m3, stores_in_frame m2 m3 -> stores_in_frame m1 m3. +Proof. + induction 1; intros. auto. econstructor; eauto. +Qed. Hypothesis number_inj: forall r1 r2, In r1 csregs -> In r2 csregs -> r1 <> r2 -> number r1 <> number r2. Hypothesis mkindex_valid: forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)). -Hypothesis mkindex_not_link: - forall z, mkindex z <> FI_link. -Hypothesis mkindex_not_retaddr: - forall z, mkindex z <> FI_retaddr. Hypothesis mkindex_typ: forall z, type_of_index (mkindex z) = ty. Hypothesis mkindex_inj: @@ -763,170 +1113,350 @@ Hypothesis mkindex_inj: Hypothesis mkindex_diff: forall r idx, idx <> mkindex (number r) -> index_diff (mkindex (number r)) idx. +Hypothesis csregs_typ: + forall r, In r csregs -> mreg_type r = ty. + +Hypothesis agree: agree_regs j ls rs. +Hypothesis wt_ls: wt_locset ls. Lemma save_callee_save_regs_correct: - forall l k rs fr m, + forall l k m, incl l csregs -> list_norepet l -> - exists fr', + frame_perm_freeable m sp -> + exists m', star step tge - (State stack tf sp - (save_callee_save_regs bound number mkindex ty fe l k) rs fr m) - E0 (State stack tf sp k rs fr' m) + (State cs fb (Vptr sp Int.zero) + (save_callee_save_regs bound number mkindex ty fe l k) rs m) + E0 (State cs fb (Vptr sp Int.zero) k rs m') /\ (forall r, In r l -> number r < bound fe -> - index_val (mkindex (number r)) fr' = rs r) - /\ (forall idx, + index_contains_inj j m' sp (mkindex (number r)) (ls (R r))) + /\ (forall idx v, index_valid idx -> (forall r, In r l -> number r < bound fe -> idx <> mkindex (number r)) -> - index_val idx fr' = index_val idx fr). + index_contains m sp idx v -> + index_contains m' sp idx v) + /\ stores_in_frame m m' + /\ frame_perm_freeable m' sp. Proof. induction l; intros; simpl save_callee_save_regs. (* base case *) - exists fr. split. apply star_refl. - split. intros. elim H1. + exists m. split. apply star_refl. + split. intros. elim H2. + split. auto. + split. constructor. auto. (* inductive case *) - set (k1 := save_callee_save_regs bound number mkindex ty fe l k). assert (R1: incl l csregs). eauto with coqlib. assert (R2: list_norepet l). inversion H0; auto. unfold save_callee_save_reg. destruct (zlt (number a) (bound fe)). (* a store takes place *) - set (fr1 := set_index_val (mkindex (number a)) (rs a) fr). - exploit (IHl k rs fr1 m); auto. - fold k1. intros [fr' [A [B C]]]. - exists fr'. - split. eapply star_left. - apply exec_Msetstack. instantiate (1 := fr1). - unfold fr1. rewrite <- (mkindex_typ (number a)). - eapply set_slot_index; eauto with coqlib. - eexact A. + exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. + eauto. instantiate (1 := rs a). intros [m1 ST]. + exploit (IHl k m1). auto with coqlib. auto. + red; eauto with mem. + intros [m' [A [B [C [D E]]]]]. + exists m'. + split. eapply star_left; eauto. constructor. + rewrite <- (mkindex_typ (number a)). + apply store_stack_succeeds; auto with coqlib. traceEq. - split. intros. simpl in H1. destruct H1. subst r. - rewrite C. unfold fr1. apply get_set_index_val_same. - apply mkindex_valid; auto with coqlib. - intros. apply mkindex_inj. apply number_inj; auto with coqlib. - inversion H0. congruence. - apply B; auto. - intros. rewrite C; auto with coqlib. - unfold fr1. apply get_set_index_val_other; auto with coqlib. + split; intros. + simpl in H2. destruct (mreg_eq a r). subst r. + assert (index_contains_inj j m1 sp (mkindex (number a)) (ls (R a))). + eapply gss_index_contains_inj; eauto. + rewrite mkindex_typ. rewrite <- (csregs_typ a). apply wt_ls. auto with coqlib. + destruct H4 as [v' [P Q]]. + exists v'; split; auto. apply C; auto. + intros. apply mkindex_inj. apply number_inj; auto with coqlib. + inv H0. intuition congruence. + apply B; auto with coqlib. + intuition congruence. + split. intros. + apply C; auto with coqlib. + eapply gso_index_contains; eauto with coqlib. + split. econstructor; eauto. + rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; eauto with coqlib. + auto. (* no store takes place *) - exploit (IHl k rs fr m); auto. intros [fr' [A [B C]]]. - exists fr'. - split. exact A. - split. intros. simpl in H1; destruct H1. subst r. omegaContradiction. - apply B; auto. - intros. apply C; auto with coqlib. + exploit (IHl k m); auto with coqlib. + intros [m' [A [B [C [D E]]]]]. + exists m'; intuition. + simpl in H2. destruct H2. subst r. omegaContradiction. apply B; auto. + apply C; auto with coqlib. + intros. eapply H3; eauto. auto with coqlib. Qed. -End SAVE_CALLEE_SAVE. +End SAVE_CALLEE_SAVE. -Lemma save_callee_save_int_correct: - forall k sp rs fr m, - exists fr', +Lemma save_callee_save_correct: + forall j ls rs sp cs fb k m, + agree_regs j ls rs -> wt_locset ls -> + frame_perm_freeable m sp -> + exists m', star step tge - (State stack tf sp - (save_callee_save_int fe k) rs fr m) - E0 (State stack tf sp k rs fr' m) + (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)) (ls (R r))) /\ (forall r, - In r int_callee_save_regs -> - index_int_callee_save r < bound_int_callee_save b -> - index_val (FI_saved_int (index_int_callee_save r)) fr' = rs r) - /\ (forall idx, + In r float_callee_save_regs -> index_float_callee_save r < b.(bound_float_callee_save) -> + index_contains_inj j m' sp (FI_saved_float (index_float_callee_save r)) (ls (R r))) + /\ (forall idx v, index_valid idx -> - match idx with FI_saved_int _ => False | _ => True end -> - index_val idx fr' = index_val idx fr). + match idx with FI_saved_int _ => False | FI_saved_float _ => False | _ => True end -> + index_contains m sp idx v -> + index_contains m' sp idx v) + /\ stores_in_frame sp m m' + /\ frame_perm_freeable m' sp. Proof. intros. - exploit (save_callee_save_regs_correct fe_num_int_callee_save index_int_callee_save FI_saved_int - Tint sp int_callee_save_regs). - exact index_int_callee_save_inj. - intros. red. split; auto. generalize (index_int_callee_save_pos r H). omega. - intro; congruence. - intro; congruence. + exploit (save_callee_save_regs_correct + fe_num_int_callee_save + index_int_callee_save + FI_saved_int Tint + j cs fb sp int_callee_save_regs ls rs). + 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 until idx. destruct idx; simpl; auto. congruence. - apply incl_refl. + intros; simpl. destruct idx; auto. congruence. + intros. apply int_callee_save_type. auto. + auto. + auto. + apply incl_refl. apply int_callee_save_norepet. - intros [fr' [A [B C]]]. - exists fr'; intuition. unfold save_callee_save_int; eauto. - apply C. auto. intros; subst idx. auto. + eauto. + intros [m1 [A [B [C [D E]]]]]. + exploit (save_callee_save_regs_correct + fe_num_float_callee_save + index_float_callee_save + FI_saved_float Tfloat + j cs fb sp float_callee_save_regs ls rs). + 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. apply float_callee_save_type. auto. + auto. + auto. + apply incl_refl. + apply float_callee_save_norepet. + eexact E. + intros [m2 [P [Q [R [S T]]]]]. + exists m2. + split. unfold save_callee_save, save_callee_save_int, save_callee_save_float. + eapply star_trans; eauto. + split; intros. + destruct (B r H2 H3) as [v [X Y]]. exists v; split; auto. apply R. + apply index_saved_int_valid; auto. + intros. congruence. + auto. + split. intros. apply Q; auto. + split. intros. apply R. auto. + intros. destruct idx; contradiction||congruence. + apply C. auto. + intros. destruct idx; contradiction||congruence. + auto. + split. eapply stores_in_frame_trans; eauto. + auto. Qed. -Lemma save_callee_save_float_correct: - forall k sp rs fr m, - exists fr', - star step tge - (State stack tf sp - (save_callee_save_float fe k) rs fr m) - E0 (State stack tf sp k rs fr' m) - /\ (forall r, - In r float_callee_save_regs -> - index_float_callee_save r < bound_float_callee_save b -> - index_val (FI_saved_float (index_float_callee_save r)) fr' = rs r) - /\ (forall idx, - index_valid idx -> - match idx with FI_saved_float _ => False | _ => True end -> - index_val idx fr' = index_val idx fr). +(** Properties of sequences of stores in the frame. *) + +Lemma stores_in_frame_inject: + forall j sp sp' m, + (forall b delta, j b = Some(sp', delta) -> b = sp /\ delta = fe.(fe_stack_data)) -> + Mem.bounds m sp = (0, f.(Linear.fn_stacksize)) -> + forall m1 m2, stores_in_frame sp' m1 m2 -> Mem.inject j m m1 -> Mem.inject j m m2. Proof. - intros. - exploit (save_callee_save_regs_correct fe_num_float_callee_save index_float_callee_save FI_saved_float - Tfloat sp float_callee_save_regs). - exact index_float_callee_save_inj. - intros. red. split; auto. generalize (index_float_callee_save_pos r H). omega. - intro; congruence. - intro; congruence. + induction 3; intros. auto. - intros; congruence. - intros until idx. destruct idx; simpl; auto. congruence. - apply incl_refl. - apply float_callee_save_norepet. eauto. - intros [fr' [A [B C]]]. - exists fr'. split. unfold save_callee_save_float; eauto. - split. auto. - intros. apply C. auto. intros; subst. red; intros; subst idx. contradiction. + apply IHstores_in_frame. + intros. eapply Mem.store_outside_inject; eauto. + intros. exploit H; eauto. intros [A B]; subst. + rewrite H0; unfold fst, snd. omega. Qed. -Lemma save_callee_save_correct: - forall sp k rs m ls cs, - (forall r, rs r = ls (R r)) -> - (forall ofs ty, - In (S (Outgoing ofs ty)) (loc_arguments f.(Linear.fn_sig)) -> - get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty)))) -> - exists fr', - star step tge - (State stack tf sp (save_callee_save fe k) rs empty_frame m) - E0 (State stack tf sp k rs fr' m) - /\ agree (call_regs ls) ls rs fr' cs. -Proof. - intros. unfold save_callee_save. - exploit save_callee_save_int_correct; eauto. - intros [fr1 [A1 [B1 C1]]]. - exploit save_callee_save_float_correct. - intros [fr2 [A2 [B2 C2]]]. - exists fr2. - split. eapply star_trans. eexact A1. eexact A2. traceEq. - constructor; unfold call_regs; auto. - (* agree_local *) - intros. rewrite C2; auto with stacking. - rewrite C1; auto with stacking. - (* agree_outgoing *) - intros. rewrite C2; auto with stacking. - rewrite C1; auto with stacking. - (* agree_incoming *) - intros. apply H0. unfold loc_parameters in H1. - exploit list_in_map_inv; eauto. intros [l [A B]]. - exploit loc_arguments_acceptable; eauto. intro C. - destruct l; simpl in A. discriminate. - simpl in C. destruct s; try contradiction. inv A. auto. - (* agree_saved_int *) - intros. rewrite C2; auto with stacking. - rewrite B1; auto with stacking. - (* agree_saved_float *) - intros. rewrite B2; auto with stacking. +Lemma stores_in_frame_valid: + forall b sp m m', stores_in_frame sp m m' -> Mem.valid_block m b -> Mem.valid_block m' b. +Proof. + induction 1; intros. auto. apply IHstores_in_frame. eauto with mem. +Qed. + +Lemma stores_in_frame_perm: + forall b ofs p sp m m', stores_in_frame sp m m' -> Mem.perm m b ofs p -> Mem.perm m' b ofs p. +Proof. + induction 1; intros. auto. apply IHstores_in_frame. eauto with mem. +Qed. + +Lemma stores_in_frame_contents: + forall chunk b ofs sp, b < sp -> + forall m m', stores_in_frame sp m m' -> + Mem.load chunk m' b ofs = Mem.load chunk m b ofs. +Proof. + induction 2. auto. + rewrite IHstores_in_frame. eapply Mem.load_store_other; eauto. + left; unfold block; omega. +Qed. + +(** As a corollary of the previous lemmas, we obtain the following + correctness theorem for the execution of a function prologue + (allocation of the frame + saving of the link and return address + + saving of the used callee-save registers). *) + +Lemma function_prologue_correct: + 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 ra Tint -> + exists j', exists m2', exists sp', exists m3', exists m4', exists m5', + Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp') + /\ 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 fb (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4') + E0 (State cs fb (Vptr sp' Int.zero) k (undef_temps rs) m5') + /\ agree_regs j' (call_regs ls) (undef_temps rs) + /\ 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' m2' m5'. +Proof. + 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 *) + caseEq (Mem.alloc m1' 0 (fe_size fe)). intros m2' sp' ALLOC'. + exploit Mem.alloc_left_mapped_inject. + eapply Mem.alloc_right_inject; eauto. + eauto. + instantiate (1 := sp'). eauto with mem. + instantiate (1 := fe_stack_data fe). + generalize stack_data_offset_valid (bound_stack_data_pos b) size_no_overflow; omega. + right. rewrite (Mem.bounds_alloc_same _ _ _ _ _ ALLOC'). unfold fst, snd. + split. omega. apply size_no_overflow. + intros. apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.perm_alloc_2; eauto. + generalize stack_data_offset_valid bound_stack_data_stacksize; omega. + red. intros. apply Zdivides_trans with 4. + destruct chunk; simpl; auto with align_4. + apply fe_stack_data_aligned. + intros. + assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto. + assert (~Mem.valid_block m1' sp') by eauto with mem. + contradiction. + intros [j' [INJ2 [INCR [MAP1 MAP2]]]]. + assert (PERM: frame_perm_freeable m2' sp'). + red; intros. eapply Mem.perm_alloc_2; eauto. + (* Store of parent *) + 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. + exploit save_callee_save_correct. + apply agree_regs_undef_temps. + eapply agree_regs_inject_incr; eauto. + apply wt_undef_temps. auto. + eexact PERM4. + intros [m5' [STEPS [ICS [FCS [OTHERS [STORES PERM5]]]]]]. + (* stores in frames *) + 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 m2'; exists sp'; exists m3'; exists m4'; exists m5'. + 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. eexact STEPS. + (* agree_regs *) + split. apply agree_regs_call_regs. apply agree_regs_inject_incr with j; auto. + (* agree frame *) + split. constructor; intros. + (* unused regs *) + unfold call_regs. destruct (in_dec Loc.eq (R r) temporaries). + 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. + (* outgoing *) + 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 (LTL.undef_temps ls (R r)). + apply ICS; auto. + unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. + red; intros; exploit int_callee_save_not_destroyed; eauto. + auto. + (* float callee save *) + rewrite <- AGCS. replace (ls (R r)) with (LTL.undef_temps ls (R r)). + apply FCS; auto. + unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. + red; intros; exploit float_callee_save_not_destroyed; eauto. + auto. + (* inj *) + auto. + (* inj_unique *) + auto. + (* valid sp *) + eauto with mem. + (* valid sp' *) + eapply stores_in_frame_valid with (m := m2'); eauto with mem. + (* bounds *) + eapply Mem.bounds_alloc_same; eauto. + (* perms *) + auto. + (* wt *) + apply wt_call_regs; auto. + (* incr *) + split. auto. + (* separated *) + split. eapply inject_alloc_separated; eauto with mem. + (* inject *) + split. eapply stores_in_frame_inject; eauto. + eapply Mem.bounds_alloc_same; eauto. + (* stores in frame *) + auto. Qed. (** The following lemmas show the correctness of the register reloading @@ -940,165 +1470,436 @@ Variable bound: frame_env -> Z. Variable number: mreg -> Z. Variable mkindex: Z -> frame_index. Variable ty: typ. -Variable sp: val. Variable csregs: list mreg. +Variable j: meminj. +Variable cs: list stackframe. +Variable fb: block. +Variable sp: block. +Variable ls0: locset. +Variable m: mem. + Hypothesis mkindex_valid: forall r, In r csregs -> number r < bound fe -> index_valid (mkindex (number r)). -Hypothesis mkindex_not_link: - forall z, mkindex z <> FI_link. -Hypothesis mkindex_not_retaddr: - forall z, mkindex z <> FI_retaddr. Hypothesis mkindex_typ: forall z, type_of_index (mkindex z) = ty. Hypothesis number_within_bounds: forall r, In r csregs -> (number r < bound fe <-> mreg_within_bounds b r). Hypothesis mkindex_val: - forall ls ls0 rs fr cs r, - agree ls ls0 rs fr cs -> In r csregs -> number r < bound fe -> - index_val (mkindex (number r)) fr = ls0 (R r). + forall r, + In r csregs -> number r < bound fe -> + index_contains_inj j m sp (mkindex (number r)) (ls0 (R r)). + +Definition agree_unused (ls0: locset) (rs: regset) : Prop := + forall r, ~(mreg_within_bounds b r) -> val_inject j (ls0 (R r)) (rs r). Lemma restore_callee_save_regs_correct: - forall k fr m ls0 l ls rs cs, + forall l rs k, incl l csregs -> list_norepet l -> - agree ls ls0 rs fr cs -> - exists ls', exists rs', + agree_unused ls0 rs -> + exists rs', star step tge - (State stack tf sp - (restore_callee_save_regs bound number mkindex ty fe l k) rs fr m) - E0 (State stack tf sp k rs' fr m) - /\ (forall r, In r l -> rs' r = ls0 (R r)) + (State cs fb (Vptr sp Int.zero) + (restore_callee_save_regs bound number mkindex ty fe l 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 ls' ls0 rs' fr cs. + /\ agree_unused ls0 rs'. Proof. induction l; intros; simpl restore_callee_save_regs. (* base case *) - exists ls. exists rs. - split. apply star_refl. - split. intros. elim H2. - split. auto. auto. + exists rs. intuition. apply star_refl. (* inductive case *) - set (k1 := restore_callee_save_regs bound number mkindex ty fe l k). assert (R0: In a csregs). apply H; auto with coqlib. assert (R1: incl l csregs). eauto with coqlib. assert (R2: list_norepet l). inversion H0; auto. unfold restore_callee_save_reg. destruct (zlt (number a) (bound fe)). - set (ls1 := Locmap.set (R a) (ls0 (R a)) ls). - set (rs1 := Regmap.set a (ls0 (R a)) rs). - assert (R3: agree ls1 ls0 rs1 fr cs). - unfold ls1, rs1. apply agree_set_reg. auto. - rewrite <- number_within_bounds; auto. - generalize (IHl ls1 rs1 cs R1 R2 R3). - intros [ls' [rs' [A [B [C D]]]]]. - exists ls'. exists rs'. split. - apply star_left with E0 (State stack tf sp k1 rs1 fr m) E0. - unfold rs1; apply exec_Mgetstack. apply get_slot_index; auto. - symmetry. eapply mkindex_val; eauto. - auto. traceEq. - split. intros. elim H2; intros. - subst r. rewrite C. unfold rs1. apply Regmap.gss. inversion H0; auto. + exploit (mkindex_val a); auto. intros [v [X Y]]. + set (rs1 := Regmap.set a v rs). + exploit (IHl rs1 k); eauto. + red; intros. unfold rs1. unfold Regmap.set. destruct (RegEq.eq r a). + subst r. auto. + auto. + intros [rs' [A [B [C D]]]]. + exists rs'. split. + eapply star_left. + constructor. rewrite <- (mkindex_typ (number a)). apply index_contains_load_stack. eauto. + eauto. traceEq. + split. intros. destruct H2. + subst r. rewrite C. unfold rs1. rewrite Regmap.gss. auto. inv H0; auto. auto. split. intros. simpl in H2. rewrite C. unfold rs1. apply Regmap.gso. apply sym_not_eq; tauto. tauto. - assumption. + auto. (* no load takes place *) - generalize (IHl ls rs cs R1 R2 H1). - intros [ls' [rs' [A [B [C D]]]]]. - exists ls'; exists rs'. split. assumption. - split. intros. elim H2; intros. - subst r. apply (agree_unused_reg _ _ _ _ _ D). + exploit (IHl rs k); auto. + intros [rs' [A [B [C D]]]]. + exists rs'. split. assumption. + split. intros. destruct H2. + subst r. apply D. rewrite <- number_within_bounds. auto. auto. auto. split. intros. simpl in H2. apply C. tauto. - assumption. -Qed. - -End RESTORE_CALLEE_SAVE. - -Lemma restore_int_callee_save_correct: - forall sp k fr m ls0 ls rs cs, - agree ls ls0 rs fr cs -> - exists ls', exists rs', - star step tge - (State stack tf sp - (restore_callee_save_int fe k) rs fr m) - E0 (State stack tf sp k rs' fr m) - /\ (forall r, In r int_callee_save_regs -> rs' r = ls0 (R r)) - /\ (forall r, ~(In r int_callee_save_regs) -> rs' r = rs r) - /\ agree ls' ls0 rs' fr cs. -Proof. - intros. unfold restore_callee_save_int. - apply restore_callee_save_regs_correct with int_callee_save_regs ls. - intros; simpl. split; auto. generalize (index_int_callee_save_pos r H0). omega. - intros; congruence. - intros; congruence. - auto. - intros. unfold mreg_within_bounds. - rewrite (int_callee_save_type r H0). tauto. - eauto with stacking. - apply incl_refl. - apply int_callee_save_norepet. auto. Qed. -Lemma restore_float_callee_save_correct: - forall sp k fr m ls0 ls rs cs, - agree ls ls0 rs fr cs -> - exists ls', exists rs', - star step tge - (State stack tf sp - (restore_callee_save_float fe k) rs fr m) - E0 (State stack tf sp k rs' fr m) - /\ (forall r, In r float_callee_save_regs -> rs' r = ls0 (R r)) - /\ (forall r, ~(In r float_callee_save_regs) -> rs' r = rs r) - /\ agree ls' ls0 rs' fr cs. -Proof. - intros. unfold restore_callee_save_float. - apply restore_callee_save_regs_correct with float_callee_save_regs ls. - intros; simpl. split; auto. generalize (index_float_callee_save_pos r H0). omega. - intros; congruence. - intros; congruence. - auto. - intros. unfold mreg_within_bounds. - rewrite (float_callee_save_type r H0). tauto. - eauto with stacking. - apply incl_refl. - apply float_callee_save_norepet. - auto. -Qed. +End RESTORE_CALLEE_SAVE. Lemma restore_callee_save_correct: - forall sp k fr m ls0 ls rs cs, - agree ls ls0 rs fr cs -> + 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 stack tf sp (restore_callee_save fe k) rs fr m) - E0 (State stack tf sp k rs' fr 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 -> - rs' r = ls0 (R r)) + val_inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r int_callee_save_regs) -> ~(In r float_callee_save_regs) -> rs' r = rs r). Proof. - intros. unfold restore_callee_save. - exploit restore_int_callee_save_correct; eauto. - intros [ls1 [rs1 [A [B [C D]]]]]. - exploit restore_float_callee_save_correct. eexact D. - intros [ls2 [rs2 [P [Q [R S]]]]]. - exists rs2. split. eapply star_trans. eexact A. eexact P. traceEq. - split. intros. elim H0; intros. - rewrite R. apply B. auto. apply list_disjoint_notin with int_callee_save_regs. - apply int_float_callee_save_disjoint. auto. - apply Q. auto. - intros. rewrite R. apply C. auto. auto. + intros. + exploit (restore_callee_save_regs_correct + fe_num_int_callee_save + index_int_callee_save + FI_saved_int + Tint + int_callee_save_regs + 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. + apply int_callee_save_norepet. + eauto. + intros [rs1 [A [B [C D]]]]. + exploit (restore_callee_save_regs_correct + fe_num_float_callee_save + index_float_callee_save + FI_saved_float + Tfloat + float_callee_save_regs + 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. + apply float_callee_save_norepet. + eexact D. + intros [rs2 [P [Q [R S]]]]. + exists rs2. + split. unfold restore_callee_save. eapply star_trans; eauto. + split. intros. destruct H1. + rewrite R. apply B; auto. red; intros. exploit int_float_callee_save_disjoint; eauto. + apply Q; auto. + intros. rewrite R; auto. +Qed. + +(** As a corollary, we obtain the following correctness result for + the execution of a function epilogue (reloading of used callee-save + registers + reloading of the link and return address + freeing + of the frame). *) + +Lemma function_epilogue_correct: + 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 ra -> + Mem.inject j m m' -> + Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 -> + exists rs1, exists m1', + load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) = Some pa + /\ 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 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 m1'. +Proof. + intros. + (* can free *) + 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)) + 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. + (* inject after free *) + 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. + exploit Mem.perm_in_bounds; eauto. + rewrite (agree_bounds _ _ _ _ _ _ _ _ _ H0). auto. + (* can execute epilogue *) + exploit restore_callee_save_correct; eauto. + instantiate (1 := rs). red; intros. + rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ _ H0). auto. auto. + intros [rs1 [A [B C]]]. + (* conclusions *) + 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. 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. + 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. + destruct (in_dec Loc.eq (R r) destroyed_at_call). + rewrite C; auto. + intuition. + split. apply agree_callee_save_return_regs. + split. apply C. apply int_callee_save_not_destroyed. left; simpl; auto. + apply float_callee_save_not_destroyed. left; simpl; auto. + auto. Qed. End FRAME_PROPERTIES. -(** * Semantic preservation *) +(** * Call stack invariant *) + +Inductive match_globalenvs (j: meminj) (bound: Z) : Prop := + | match_globalenvs_intro + (POS: bound > 0) + (DOMAIN: forall b, b < bound -> j b = Some(b, 0)) + (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) + (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) + (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + +Inductive match_stacks (j: meminj) (m m': mem): + list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop := + | match_stacks_empty: forall sg hi bound bound', + 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 fb sp' ra c' cs' sg bound bound' trf + (TAIL: is_tail c (Linear.fn_code f)) + (WTF: wt_function f) + (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') + (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)) + (STK: match_stacks j m m' cs cs' (Linear.fn_sig f) sp sp') + (BELOW: sp < bound) + (BELOW': sp' < bound'), + match_stacks j m m' + (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs) + (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs') + sg bound bound'. + +(** Invariance with respect to change of bounds. *) + +Lemma match_stacks_change_bounds: + forall j m1 m' cs cs' sg bound bound', + match_stacks j m1 m' cs cs' sg bound bound' -> + forall xbound xbound', + bound <= xbound -> bound' <= xbound' -> + match_stacks j m1 m' cs cs' sg xbound xbound'. +Proof. + induction 1; intros. + apply match_stacks_empty with hi; auto. omega. omega. + econstructor; eauto. omega. omega. +Qed. + +(** Invariance with respect to change of [m]. *) + +Lemma match_stacks_change_linear_mem: + forall j m1 m2 m' cs cs' sg bound bound', + match_stacks j m1 m' cs cs' sg bound bound' -> + (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> + (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) -> + match_stacks j m2 m' cs cs' sg bound bound'. +Proof. + induction 1; intros. + econstructor; eauto. + econstructor; eauto. + eapply agree_frame_invariant; eauto. + apply IHmatch_stacks. + intros. apply H0; auto. omega. + intros. apply H1. omega. +Qed. + +(** Invariance with respect to change of [m']. *) + +Lemma match_stacks_change_mach_mem: + forall j m m1' m2' cs cs' sg bound bound', + match_stacks j m m1' cs cs' sg bound bound' -> + (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> + (forall b ofs p, b < bound' -> Mem.perm m1' b ofs p -> Mem.perm m2' b ofs p) -> + (forall chunk b ofs v, b < bound' -> Mem.load chunk m1' b ofs = Some v -> Mem.load chunk m2' b ofs = Some v) -> + match_stacks j m m2' cs cs' sg bound bound'. +Proof. + induction 1; intros. + econstructor; eauto. + econstructor; eauto. + eapply agree_frame_invariant; eauto. + apply IHmatch_stacks. + intros; apply H0; auto; omega. + intros; apply H1; auto; omega. + intros; apply H2; auto. omega. +Qed. + +(** A variant of the latter, for use with external calls *) + +Lemma match_stacks_change_mem_extcall: + forall j m1 m2 m1' m2' cs cs' sg bound bound', + match_stacks j m1 m1' cs cs' sg bound bound' -> + (forall b, b < bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> + (forall b, b < bound -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall b, b < bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> + mem_unchanged_on (loc_out_of_reach j m1) m1' m2' -> + match_stacks j m2 m2' cs cs' sg bound bound'. +Proof. + induction 1; intros. + econstructor; eauto. + econstructor; eauto. + eapply agree_frame_extcall_invariant; eauto. + apply IHmatch_stacks. + intros; apply H0; auto; omega. + intros; apply H1; omega. + intros; apply H2; auto; omega. + auto. +Qed. + +(** Invariance with respect to change of [j]. *) + +Lemma match_stacks_change_meminj: + forall j j' m m' m1 m1', + inject_incr j j' -> + inject_separated j j' m1 m1' -> + forall cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + bound' <= Mem.nextblock m1' -> + match_stacks j' m m' cs cs' sg bound bound'. +Proof. + induction 3; intros. + apply match_stacks_empty with hi; auto. + inv H3. constructor; auto. + intros. red in H0. case_eq (j b1). + intros [b' delta'] EQ. rewrite (H _ _ _ EQ) in H3. inv H3. eauto. + intros EQ. exploit H0; eauto. intros [A B]. elim B. red. omega. + econstructor; eauto. + eapply agree_frame_inject_incr; eauto. red; omega. + apply IHmatch_stacks. omega. +Qed. + +(** Preservation by parallel stores in Linear and Mach. *) + +Lemma match_stacks_parallel_stores: + forall j m m' chunk addr addr' v v' m1 m1', + 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' -> + forall cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + match_stacks j m1 m1' cs cs' sg bound bound'. +Proof. + intros until m1'. intros MINJ VINJ STORE1 STORE2. + induction 1. + econstructor; eauto. + econstructor; eauto. + eapply agree_frame_parallel_stores; eauto. +Qed. + +(** Invariance by external calls. *) + +Lemma match_stack_change_extcall: + forall ec args m1 res t m2 args' m1' res' t' m2' j j', + external_call ec ge args m1 t res m2 -> + external_call ec ge args' m1' t' res' m2' -> + inject_incr j j' -> + inject_separated j j' m1 m1' -> + mem_unchanged_on (loc_out_of_reach j m1) m1' m2' -> + forall cs cs' sg bound bound', + match_stacks j m1 m1' cs cs' sg bound bound' -> + bound <= Mem.nextblock m1 -> bound' <= Mem.nextblock m1' -> + match_stacks j' m2 m2' cs cs' sg bound bound'. +Proof. + intros. + eapply match_stacks_change_meminj; eauto. + eapply match_stacks_change_mem_extcall; eauto. + intros; eapply external_call_valid_block; eauto. + intros; eapply external_call_bounds; eauto. red; omega. + intros; eapply external_call_valid_block; eauto. +Qed. + +(** Invariance with respect to change of signature *) + +Lemma match_stacks_change_sig: + forall sg1 j m m' cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + tailcall_possible sg1 -> + match_stacks j m m' cs cs' sg1 bound bound'. +Proof. + induction 1; intros. econstructor; eauto. econstructor; eauto. + intros. elim (H0 _ H1). +Qed. + +(** [match_stacks] implies [match_globalenvs], which implies [meminj_preserves_globals]. *) + +Lemma match_stacks_globalenvs: + forall j m m' cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + exists hi, match_globalenvs j hi. +Proof. + induction 1. exists hi; auto. auto. +Qed. + +Lemma match_stacks_preserves_globals: + forall j m m' cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + meminj_preserves_globals ge j. +Proof. + intros. exploit match_stacks_globalenvs; eauto. intros [hi MG]. inv MG. + split. eauto. split. eauto. intros. symmetry. eauto. +Qed. + +(** Typing properties of [match_stacks]. *) + +Lemma match_stacks_wt_locset: + forall j m m' cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + wt_locset (parent_locset cs). +Proof. + induction 1; simpl. + unfold Locmap.init; red; intros; red; auto. + inv FRM; auto. +Qed. + +Lemma match_stacks_type_sp: + forall j m m' cs cs' sg bound bound', + match_stacks j m m' cs cs' sg bound bound' -> + Val.has_type (parent_sp cs') Tint. +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. *) @@ -1170,19 +1971,86 @@ Qed. End LABELS. -(** Code inclusion property for Linear executions. *) +(** Code tail property for Linear executions. *) -Lemma find_label_incl: +Lemma find_label_tail: forall lbl c c', - Linear.find_label lbl c = Some c' -> incl c' c. + Linear.find_label lbl c = Some c' -> is_tail c' c. Proof. induction c; simpl. intros; discriminate. intro c'. case (Linear.is_label lbl a); intros. - injection H; intro; subst c'. red; intros; auto with coqlib. - apply incl_tl. auto. + injection H; intro; subst c'. auto with coqlib. + auto with coqlib. Qed. +(** Code tail property for translations *) + +Lemma is_tail_save_callee_save_regs: + forall bound number mkindex ty fe csl k, + is_tail k (save_callee_save_regs bound number mkindex ty fe csl k). +Proof. + induction csl; intros; simpl. auto with coqlib. + unfold save_callee_save_reg. destruct (zlt (number a) (bound fe)). + constructor; auto. auto. +Qed. + +Lemma is_tail_save_callee_save: + forall fe k, + is_tail k (save_callee_save fe k). +Proof. + intros. unfold save_callee_save, save_callee_save_int, save_callee_save_float. + eapply is_tail_trans; apply is_tail_save_callee_save_regs. +Qed. + +Lemma is_tail_restore_callee_save_regs: + forall bound number mkindex ty fe csl k, + is_tail k (restore_callee_save_regs bound number mkindex ty fe csl k). +Proof. + induction csl; intros; simpl. auto with coqlib. + unfold restore_callee_save_reg. destruct (zlt (number a) (bound fe)). + constructor; auto. auto. +Qed. + +Lemma is_tail_restore_callee_save: + forall fe k, + is_tail k (restore_callee_save fe k). +Proof. + intros. unfold restore_callee_save, restore_callee_save_int, restore_callee_save_float. + eapply is_tail_trans; apply is_tail_restore_callee_save_regs. +Qed. + +Lemma is_tail_transl_instr: + forall fe i k, + is_tail k (transl_instr fe i k). +Proof. + intros. destruct i; unfold transl_instr; auto with coqlib. + destruct s; auto with coqlib. + destruct s; auto with coqlib. + eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib. + eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib. +Qed. + +Lemma is_tail_transl_code: + forall fe c1 c2, is_tail c1 c2 -> is_tail (transl_code fe c1) (transl_code fe c2). +Proof. + induction 1; simpl. auto with coqlib. + eapply is_tail_trans. eauto. apply is_tail_transl_instr. +Qed. + +Lemma is_tail_transf_function: + forall f tf c, + transf_function f = OK tf -> + is_tail c (Linear.fn_code f) -> + is_tail (transl_code (make_env (function_bounds f)) c) (fn_code tf). +Proof. + intros. rewrite (unfold_transf_function _ _ H). simpl. + unfold transl_body. eapply is_tail_trans. 2: apply is_tail_save_callee_save. + apply is_tail_transl_code; auto. +Qed. + +(** * Semantic preservation *) + (** Preservation / translation of global symbols and functions. *) Lemma symbols_preserved: @@ -1221,35 +2089,35 @@ Lemma sig_preserved: forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f. Proof. intros until tf; unfold transf_fundef, transf_partial_fundef. - destruct f. unfold transf_function. - destruct (zlt (Linear.fn_stacksize f) 0). simpl; congruence. - destruct (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). simpl; congruence. - unfold bind. intros. inversion H; reflexivity. - intro. inversion H. reflexivity. -Qed. - -Lemma stacksize_preserved: - forall f tf, transf_function f = OK tf -> Mach.fn_stacksize tf = Linear.fn_stacksize f. -Proof. - intros until tf; unfold transf_function. - destruct (zlt (Linear.fn_stacksize f) 0). simpl; congruence. - destruct (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). simpl; congruence. - intros. inversion H; reflexivity. + destruct f; intros; monadInv H. + rewrite (unfold_transf_function _ _ EQ). auto. + auto. Qed. Lemma find_function_translated: - forall f0 tf0 ls ls0 rs fr cs ros f, - agree f0 tf0 ls ls0 rs fr cs -> + forall j ls rs m m' cs cs' sg bound bound' ros f, + 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 /\ transf_fundef f = OK 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; intro AG. - destruct ros; simpl. - rewrite (agree_eval_reg _ _ _ _ _ _ _ m AG). intro. - apply functions_translated; auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence. - intro. apply function_ptr_translated; auto. + intros until f; intros AG MS FF. + exploit match_stacks_globalenvs; eauto. intros [hi MG]. + destruct ros; simpl in FF. + 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 b; exists tf; split; auto. simpl. + generalize (AG m0). rewrite EQ. intro INJ. inv INJ. + exploit Genv.find_funct_ptr_negative. unfold ge in FF; eexact FF. intros. + inv MG. rewrite (DOMAIN b) in H2. inv H2. auto. omega. + revert FF. case_eq (Genv.find_symbol ge i); intros; try discriminate. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + exists b; exists tf; split; auto. simpl. + rewrite symbols_preserved. auto. Qed. Hypothesis wt_prog: wt_program prog. @@ -1264,84 +2132,59 @@ Proof. intro. eapply Genv.find_funct_ptr_prop; eauto. Qed. -(** Correctness of stack pointer relocation in operations and - addressing modes. *) - -Definition shift_sp (tf: Mach.function) (sp: val) := - Val.add sp (Vint (Int.repr (-tf.(fn_framesize)))). - -Remark shift_sp_eq: - forall f tf sp, - transf_function f = OK tf -> - shift_sp tf sp = Val.sub sp (Vint (Int.repr (fe_size (make_env (function_bounds f))))). -Proof. - intros. unfold shift_sp. - replace (fe_size (make_env (function_bounds f))) with (fn_framesize tf). - rewrite <- Int.neg_repr. destruct sp; simpl; auto; rewrite Int.sub_add_opp; auto. - rewrite (unfold_transf_function _ _ H). auto. -Qed. - -Lemma shift_eval_operation: - forall f tf sp op args v, - transf_function f = OK tf -> - eval_operation ge sp op args = Some v -> - eval_operation tge (shift_sp tf sp) - (transl_op (make_env (function_bounds f)) op) args = Some v. -Proof. - intros. rewrite <- H0. rewrite (shift_sp_eq f tf sp H). unfold transl_op. - rewrite (eval_operation_preserved ge tge). - apply shift_stack_eval_operation. - exact symbols_preserved. -Qed. - -Lemma shift_eval_addressing: - forall f tf sp addr args v, - transf_function f = OK tf -> - eval_addressing ge sp addr args = Some v -> - eval_addressing tge (shift_sp tf sp) - (transl_addr (make_env (function_bounds f)) addr) args = - Some v. -Proof. - intros. rewrite <- H0. rewrite (shift_sp_eq f tf sp H). unfold transl_addr. - rewrite (eval_addressing_preserved ge tge). - apply shift_stack_eval_addressing. - exact symbols_preserved. -Qed. - (** Preservation of the arguments to an external call. *) Section EXTERNAL_ARGUMENTS. -Variable cs: list Machabstr.stackframe. +Variable j: meminj. +Variables m m': mem. +Variable cs: list Linear.stackframe. +Variable cs': list stackframe. +Variable sg: signature. +Variables bound bound': Z. +Hypothesis MS: match_stacks j m m' cs cs' sg bound bound'. Variable ls: locset. Variable rs: regset. -Variable sg: signature. +Hypothesis AGR: agree_regs j ls rs. +Hypothesis AGCS: agree_callee_save ls (parent_locset cs). -Hypothesis AG1: forall r, rs r = ls (R r). -Hypothesis AG2: forall (ofs : Z) (ty : typ), - In (S (Outgoing ofs ty)) (loc_arguments sg) -> - get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty))). +Lemma transl_external_argument: + forall l, + In l (loc_arguments sg) -> + exists v, extcall_arg rs m' (parent_sp cs') l v /\ val_inject j (ls l) v. +Proof. + intros. + assert (loc_argument_acceptable l). apply loc_arguments_acceptable with sg; auto. + destruct l; red in H0. + exists (rs m0); split. constructor. auto. + destruct s; try contradiction. + inv MS. + elim (H4 _ H). + unfold parent_sp. + exploit agree_outgoing; eauto. intros [v [A B]]. + exists v; split. + constructor. + eapply index_contains_load_stack with (idx := FI_arg z t); eauto. + red in AGCS. rewrite AGCS; auto. +Qed. Lemma transl_external_arguments_rec: forall locs, incl locs (loc_arguments sg) -> - extcall_args (parent_function cs) rs (parent_frame cs) locs ls##locs. + exists vl, + extcall_args rs m' (parent_sp cs') locs vl /\ val_list_inject j ls##locs vl. Proof. induction locs; simpl; intros. - constructor. - constructor. - assert (loc_argument_acceptable a). - apply loc_arguments_acceptable with sg; auto with coqlib. - destruct a; red in H0. - rewrite <- AG1. constructor. - destruct s; try contradiction. - constructor. change (get_parent_slot cs z t (ls (S (Outgoing z t)))). -apply AG2. auto with coqlib. - apply IHlocs; eauto with coqlib. + exists (@nil val); split. constructor. constructor. + exploit transl_external_argument; eauto with coqlib. intros [v [A B]]. + exploit IHlocs; eauto with coqlib. intros [vl [C D]]. + exists (v :: vl); split; constructor; auto. Qed. Lemma transl_external_arguments: - extcall_arguments (parent_function cs) rs (parent_frame cs) sg (ls ## (loc_arguments sg)). + exists vl, + extcall_arguments rs m' (parent_sp cs') sg vl /\ + val_list_inject j (ls ## (loc_arguments sg)) vl. Proof. unfold extcall_arguments. apply transl_external_arguments_rec. @@ -1364,61 +2207,53 @@ End EXTERNAL_ARGUMENTS. below. It implies: - Agreement between, on the Linear side, the location sets [ls] and [parent_locset s] of the current function and its caller, - and on the Mach side the register set [rs], the frame [fr] - and the caller's frame [parent_frame ts]. -- Inclusion between the Linear code [c] and the code of the + and on the Mach side the register set [rs] and the contents of + the memory area corresponding to the stack frame. +- The Linear code [c] is a suffix of the code of the function [f] being executed. +- Memory injection between the Linear and the Mach memory states. - Well-typedness of [f]. *) -Inductive match_stacks: list Linear.stackframe -> list Machabstr.stackframe -> Prop := - | match_stacks_nil: - match_stacks nil nil - | match_stacks_cons: - forall f sp c ls tf fr s ts, - match_stacks s ts -> - transf_function f = OK tf -> - wt_function f -> - agree_frame f tf ls (parent_locset s) fr ts -> - incl c (Linear.fn_code f) -> - match_stacks - (Linear.Stackframe f sp ls c :: s) - (Machabstr.Stackframe tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) fr :: ts). - -Inductive match_states: Linear.state -> Machabstr.state -> Prop := +Inductive match_states: Linear.state -> Machconcr.state -> Prop := | match_states_intro: - forall s f sp c ls m ts tf rs fr - (STACKS: match_stacks s ts) + 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) - (AG: agree f tf ls (parent_locset s) rs fr ts) - (INCL: incl c (Linear.fn_code f)), - match_states (Linear.State s f sp c ls m) - (Machabstr.State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) c) rs fr m) + (AGREGS: agree_regs j ls rs) + (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) + (Machconcr.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') | match_states_call: - forall s f ls m ts tf rs - (STACKS: match_stacks s ts) + 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) - (AG1: forall r, rs r = ls (R r)) - (AG2: forall ofs ty, - In (S (Outgoing ofs ty)) (loc_arguments (Linear.funsig f)) -> - get_parent_slot ts ofs ty (ls (S (Outgoing ofs ty)))) - (AG3: agree_callee_save ls (parent_locset s)), - match_states (Linear.Callstate s f ls m) - (Machabstr.Callstate ts tf rs m) + (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) + (Machconcr.Callstate cs' fb rs m') | match_states_return: - forall s ls m ts rs - (STACKS: match_stacks s ts) - (AG1: forall r, rs r = ls (R r)) - (AG2: agree_callee_save ls (parent_locset s)), - match_states (Linear.Returnstate s ls m) - (Machabstr.Returnstate ts rs m). + forall cs ls m cs' rs m' j sg + (MINJ: Mem.inject j m m') + (STACKS: match_stacks j m m' cs cs' sg (Mem.nextblock m) (Mem.nextblock m')) + (WTLS: wt_locset ls) + (AGREGS: agree_regs j ls rs) + (AGLOCS: agree_callee_save ls (parent_locset cs)), + match_states (Linear.Returnstate cs ls m) + (Machconcr.Returnstate cs' rs m'). Theorem transf_step_correct: forall s1 t s2, Linear.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), - exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. + exists s2', plus Machconcr.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) = @@ -1428,142 +2263,209 @@ Proof. induction 1; intros; try inv MS; try rewrite RED; - try (generalize (WTF _ (INCL _ (in_eq _ _))); intro WTI); - try (generalize (function_is_within_bounds f WTF _ (INCL _ (in_eq _ _))); + try (generalize (WTF _ (is_tail_in TAIL)); intro WTI); + try (generalize (function_is_within_bounds f WTF _ (is_tail_in TAIL)); intro BOUND; simpl in BOUND); unfold transl_instr. + (* Lgetstack *) inv WTI. destruct BOUND. unfold undef_getstack; destruct sl. (* Lgetstack, local *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) - (rs0#r <- (rs (S (Local z t)))) fr m); split. - apply plus_one. apply exec_Mgetstack. - apply get_slot_index. auto. apply index_local_valid. auto. congruence. congruence. auto. - eapply agree_locals; eauto. - econstructor; eauto with coqlib. - apply agree_set_reg; auto. + exploit agree_locals; eauto. intros [v [A B]]. + econstructor; split. + apply plus_one. apply exec_Mgetstack. + eapply index_contains_load_stack; eauto. + econstructor; eauto with coqlib. + apply agree_regs_set_reg; auto. + apply agree_frame_set_reg; auto. simpl; rewrite <- H1. eapply agree_wt_ls; eauto. (* Lgetstack, incoming *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) - (rs0 # IT1 <- Vundef # r <- (rs (S (Incoming z t)))) fr m); split. - apply plus_one. apply exec_Mgetparam. - change (get_parent_slot ts z t (rs (S (Incoming z t)))). - eapply agree_incoming; eauto. - econstructor; eauto with coqlib. - apply agree_set_reg; auto. apply agree_undef_getparam; auto. + red in H2. exploit incoming_slot_in_parameters; eauto. intros IN_ARGS. + inv STACKS. elim (H6 _ IN_ARGS). + exploit agree_outgoing. eexact FRM. eapply ARGS; eauto. + intros [v [A B]]. + econstructor; split. + apply plus_one. eapply exec_Mgetparam; eauto. + rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs. + eapply index_contains_load_stack with (idx := FI_link). eauto. eapply agree_link; eauto. + simpl parent_sp. + change (offset_of_index (make_env (function_bounds f)) (FI_arg z t)) + with (offset_of_index (make_env (function_bounds f0)) (FI_arg z t)). + eapply index_contains_load_stack with (idx := FI_arg z t). eauto. eauto. + exploit agree_incoming; eauto. intros EQ; simpl in EQ. + econstructor; eauto with coqlib. econstructor; eauto. + apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. congruence. + eapply agree_frame_set_reg; eauto. eapply agree_frame_set_reg; eauto. + apply temporary_within_bounds. unfold temporaries; auto with coqlib. + simpl; auto. simpl; rewrite <- H1. eapply agree_wt_ls; eauto. (* Lgetstack, outgoing *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) - (rs0#r <- (rs (S (Outgoing z t)))) fr m); split. - apply plus_one. apply exec_Mgetstack. - apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. - eapply agree_outgoing; eauto. - econstructor; eauto with coqlib. - apply agree_set_reg; auto. - - (* Lsetstack *) - inv WTI. destruct sl. - - (* Lsetstack, local *) - generalize (agree_set_local _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND). - intros [fr' [SET AG']]. + exploit agree_outgoing; eauto. intros [v [A B]]. econstructor; split. - apply plus_one. eapply exec_Msetstack; eauto. + apply plus_one. apply exec_Mgetstack. + eapply index_contains_load_stack; eauto. econstructor; eauto with coqlib. - replace (rs (R r)) with (rs0 r). auto. - symmetry. eapply agree_reg; eauto. - (* Lsetstack, incoming *) - contradiction. - (* Lsetstack, outgoing *) - generalize (agree_set_outgoing _ _ TRANSL _ _ _ _ _ (rs0 r) _ _ AG BOUND). - intros [fr' [SET AG']]. + apply agree_regs_set_reg; auto. + apply agree_frame_set_reg; auto. simpl; rewrite <- H1; eapply agree_wt_ls; eauto. + + (* Lsetstack *) + inv WTI. + set (idx := match sl with + | Local ofs ty => FI_local ofs ty + | Incoming ofs ty => FI_link (*dummy*) + | Outgoing ofs ty => FI_arg ofs ty + end). + assert (index_valid f idx). + unfold idx; destruct sl. + apply index_local_valid; auto. + red; auto. + apply index_arg_valid; auto. + exploit store_index_succeeds; eauto. eapply agree_perm; eauto. + instantiate (1 := rs0 r). intros [m1' STORE]. econstructor; split. - apply plus_one. eapply exec_Msetstack; eauto. + apply plus_one. destruct sl; simpl in H3. + econstructor. eapply store_stack_succeeds with (idx := idx); eauto. + contradiction. + econstructor. eapply store_stack_succeeds with (idx := idx); eauto. econstructor; eauto with coqlib. - replace (rs (R r)) with (rs0 r). auto. - symmetry. eapply agree_reg; eauto. + eapply Mem.store_outside_inject; eauto. + intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta. + rewrite (agree_bounds _ _ _ _ _ _ _ _ _ _ AGFRAME). unfold fst, snd. rewrite Zplus_0_l. + rewrite size_type_chunk. + exploit offset_of_index_disj_stack_data_2; eauto. + omega. + apply match_stacks_change_mach_mem with m'; auto. + eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega. + apply agree_regs_set_slot; auto. + destruct sl. + eapply agree_frame_set_local; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. + simpl in H3; contradiction. + eapply agree_frame_set_outgoing; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. (* Lop *) - set (op' := transl_op (make_env (function_bounds f)) op). - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) ((undef_op op' rs0)#res <- v) fr m); split. - apply plus_one. apply exec_Mop. - apply shift_eval_operation. auto. - change mreg with RegEq.t. - rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). auto. + assert (Val.has_type v (mreg_type res)). + inv WTI. simpl in H. inv H. rewrite <- H1. eapply agree_wt_ls; eauto. + replace (mreg_type res) with (snd (type_of_operation op)). + eapply type_of_operation_sound; eauto. + rewrite <- H4; auto. + assert (exists v', + eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v' + /\ val_inject j v v'). + eapply eval_operation_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + eapply agree_inj; eauto. eapply agree_reglist; eauto. + destruct H1 as [v' [A B]]. + econstructor; split. + apply plus_one. constructor. + instantiate (1 := v'). rewrite <- A. apply eval_operation_preserved. + exact symbols_preserved. econstructor; eauto with coqlib. - apply agree_set_reg; auto. apply agree_undef_op; auto. + apply agree_regs_set_reg; auto. apply agree_regs_undef_op; auto. + apply agree_frame_set_reg; auto. apply agree_frame_undef_op; auto. (* Lload *) - exists (State ts tf (shift_sp tf sp) (transl_code (make_env (function_bounds f)) b) ((undef_temps rs0)#dst <- v) fr m); split. - apply plus_one; eapply exec_Mload; eauto. - apply shift_eval_addressing; auto. - change mreg with RegEq.t. - rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto. + assert (exists a', + eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' + /\ val_inject j a a'). + eapply eval_addressing_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + eapply agree_inj; eauto. eapply agree_reglist; eauto. + destruct H1 as [a' [A B]]. + exploit Mem.loadv_inject; eauto. intros [v' [C D]]. + econstructor; split. + apply plus_one. econstructor. + instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + eexact C. econstructor; eauto with coqlib. - apply agree_set_reg; auto. apply agree_undef_temps; auto. + apply agree_regs_set_reg; auto. apply agree_regs_undef_temps; auto. + apply agree_frame_set_reg; auto. apply agree_frame_undef_temps; auto. + simpl. inv WTI. rewrite H6. + inv B; simpl in H0; try discriminate. eapply Mem.load_type; eauto. (* Lstore *) + assert (exists a', + eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' + /\ val_inject j a a'). + eapply eval_addressing_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + eapply agree_inj; eauto. eapply agree_reglist; eauto. + destruct H1 as [a' [A B]]. + exploit Mem.storev_mapped_inject; eauto. intros [m1' [C D]]. + econstructor; split. + apply plus_one. econstructor. + instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + eexact C. + econstructor; eauto with coqlib. + eapply match_stacks_parallel_stores. eexact MINJ. eexact B. eauto. eauto. auto. + apply agree_regs_undef_temps; auto. + apply agree_frame_undef_temps; auto. + eapply agree_frame_parallel_stores; eauto. + + (* Lcall *) + exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. + exploit is_tail_transf_function; eauto. intros IST. simpl in IST. + exploit Asmgenretaddr.return_address_exists. eexact IST. + intros [ra D]. econstructor; split. - apply plus_one; eapply exec_Mstore; eauto. - apply shift_eval_addressing; eauto. - change mreg with RegEq.t. - rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). eauto. - rewrite (agree_eval_reg _ _ _ _ _ _ _ src AG). eauto. - econstructor; eauto with coqlib. apply agree_undef_temps; auto. - - (* Lcall *) - assert (WTF': wt_fundef f'). eapply find_function_well_typed; eauto. - exploit find_function_translated; eauto. - intros [tf' [FIND' TRANSL']]. - econstructor; split. - apply plus_one; eapply exec_Mcall; eauto. - econstructor; eauto. + apply plus_one. econstructor; eauto. + econstructor; eauto. econstructor; eauto with coqlib. - exists rs0; auto. - intro. symmetry. eapply agree_reg; eauto. - intros. - assert (slot_within_bounds f (function_bounds f) (Outgoing ofs ty)). - red. simpl. generalize (loc_arguments_bounded _ _ _ H0). - generalize (loc_arguments_acceptable _ _ H0). unfold loc_argument_acceptable. - omega. - unfold get_parent_slot, parent_function, parent_frame. - change (fe_ofs_arg + 4 * ofs) - with (offset_of_index (make_env (function_bounds f)) (FI_arg ofs ty)). - apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. - eapply agree_outgoing; eauto. - simpl. red; auto. - - (* Ltailcall *) - assert (WTF': wt_fundef f'). eapply find_function_well_typed; eauto. - exploit find_function_translated; eauto. - intros [tf' [FIND' TRANSL']]. - generalize (restore_callee_save_correct ts _ _ TRANSL - (shift_sp tf (Vptr stk Int.zero)) - (Mtailcall (Linear.funsig f') ros :: transl_code (make_env (function_bounds f)) b) - _ m _ _ _ _ AG). - intros [rs2 [A [B C]]]. - assert (FIND'': find_function tge ros rs2 = Some tf'). - rewrite <- FIND'. destruct ros; simpl; auto. - inv WTI. rewrite C. auto. - simpl. intuition congruence. simpl. intuition congruence. + simpl; auto. + intros; red. split. + generalize (loc_arguments_acceptable _ _ H0). simpl. omega. + apply Zle_trans with (size_arguments (Linear.funsig f')); auto. + apply loc_arguments_bounded; auto. + eapply agree_valid_linear; eauto. + eapply agree_valid_mach; eauto. + eapply find_function_well_typed; eauto. + eapply agree_wt_ls; eauto. + simpl; red; auto. + + (* Ltailcall *) + exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. + exploit function_epilogue_correct; eauto. + intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]]. econstructor; split. - eapply plus_right. eexact A. - simpl shift_sp. eapply exec_Mtailcall; eauto. - rewrite (stacksize_preserved _ _ TRANSL); eauto. + eapply plus_right. eexact S. econstructor; 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. - intros; symmetry; eapply agree_return_regs; eauto. - intros. inv WTI. generalize (H4 _ H0). tauto. - apply agree_callee_save_return_regs. + econstructor; eauto. + inv WTI. apply match_stacks_change_sig with (Linear.fn_sig f); auto. + apply match_stacks_change_bounds with stk sp'. + 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. + intros. rewrite <- H2. eapply Mem.load_free; eauto. left; unfold block; omega. + eauto with mem. intros. eapply Mem.bounds_free; 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 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. (* Lbuiltin *) + exploit external_call_mem_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + eapply agree_reglist; eauto. + intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. econstructor; split. - apply plus_one. apply exec_Mbuiltin. - change mreg with RegEq.t. - rewrite (agree_eval_regs _ _ _ _ _ _ _ args AG). + apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. - apply agree_set_reg; auto. apply agree_undef_temps; auto. - + eapply match_stack_change_extcall; eauto. + apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. + apply Zlt_le_weak. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. + apply agree_regs_set_reg; auto. apply agree_regs_undef_temps; auto. eapply agree_regs_inject_incr; eauto. + apply agree_frame_set_reg; auto. apply agree_frame_undef_temps; auto. + eapply agree_frame_inject_incr; eauto. + apply agree_frame_extcall_invariant with m m'0; auto. + eapply external_call_valid_block; eauto. + eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto. + eapply external_call_valid_block; eauto. + eapply agree_valid_mach; eauto. + inv WTI. simpl; rewrite H4. eapply external_call_well_typed; eauto. + (* Llabel *) econstructor; split. apply plus_one; apply exec_Mlabel. @@ -1571,124 +2473,160 @@ Proof. (* Lgoto *) econstructor; split. - apply plus_one; apply exec_Mgoto. + apply plus_one; eapply exec_Mgoto; eauto. apply transl_find_label; eauto. econstructor; eauto. - eapply find_label_incl; eauto. + eapply find_label_tail; eauto. (* Lcond, true *) econstructor; split. - apply plus_one; apply exec_Mcond_true. - rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; eauto. - apply transl_find_label; eauto. - econstructor; eauto. apply agree_undef_temps; auto. - eapply find_label_incl; eauto. + apply plus_one. eapply exec_Mcond_true; eauto. + eapply eval_condition_inject; eauto. eapply agree_reglist; eauto. + eapply transl_find_label; eauto. + econstructor; eauto with coqlib. + apply agree_regs_undef_temps; auto. + apply agree_frame_undef_temps; auto. + eapply find_label_tail; eauto. (* Lcond, false *) econstructor; split. - apply plus_one; apply exec_Mcond_false. - rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; auto. - econstructor; eauto with coqlib. apply agree_undef_temps; auto. + apply plus_one. eapply exec_Mcond_false; eauto. + eapply eval_condition_inject; eauto. eapply agree_reglist; eauto. + econstructor; eauto with coqlib. + apply agree_regs_undef_temps; auto. + apply agree_frame_undef_temps; auto. (* Ljumptable *) + assert (rs0 arg = Vint n). + generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto. econstructor; split. - apply plus_one; eapply exec_Mjumptable. - rewrite <- (agree_eval_reg _ _ _ _ _ _ _ arg AG) in H; eauto. - eauto. + apply plus_one; eapply exec_Mjumptable; eauto. apply transl_find_label; eauto. - econstructor; eauto. apply agree_undef_temps; auto. - eapply find_label_incl; eauto. + econstructor; eauto. + apply agree_regs_undef_temps; auto. + apply agree_frame_undef_temps; auto. + eapply find_label_tail; eauto. (* Lreturn *) - exploit restore_callee_save_correct; eauto. - intros [ls' [A [B C]]]. + exploit function_epilogue_correct; eauto. + intros [rs1 [m1' [P [Q [R [S [T [U [V W]]]]]]]]]. econstructor; split. - eapply plus_right. eauto. - simpl shift_sp. econstructor; eauto. - rewrite (stacksize_preserved _ _ TRANSL); eauto. + eapply plus_right. eexact S. econstructor; eauto. traceEq. - econstructor; eauto. - intros. symmetry. eapply agree_return_regs; eauto. - apply agree_callee_save_return_regs. + econstructor; eauto. + apply match_stacks_change_bounds with stk sp'. + 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. + intros. rewrite <- H1. eapply Mem.load_free; eauto. left; unfold block; omega. + eauto with mem. intros. eapply Mem.bounds_free; 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 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 *) - generalize TRANSL; clear TRANSL. - unfold transf_fundef, transf_partial_fundef. + revert TRANSL. unfold transf_fundef, transf_partial_fundef. caseEq (transf_function f); simpl; try congruence. intros tfn TRANSL EQ. inversion EQ; clear EQ; subst tf. inversion WTF as [|f' WTFN]. subst f'. - set (sp := Vptr stk Int.zero) in *. - set (tsp := shift_sp tfn sp). - set (fe := make_env (function_bounds f)). - exploit save_callee_save_correct; eauto. - intros [fr [EXP AG]]. + exploit function_prologue_correct; eauto. + eapply match_stacks_type_sp; eauto. + eapply match_stacks_type_retaddr; eauto. + intros [j' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]. econstructor; split. - eapply plus_left. - eapply exec_function_internal; eauto. - rewrite (unfold_transf_function f tfn TRANSL); simpl; eexact H. - replace (Mach.fn_code tfn) with - (transl_body f (make_env (function_bounds f))). - replace (Vptr stk (Int.repr (- fn_framesize tfn))) with tsp. - unfold transl_body. eexact EXP. - unfold tsp, shift_sp, sp. unfold Val.add. - rewrite Int.add_commut. rewrite Int.add_zero. auto. - rewrite (unfold_transf_function f tfn TRANSL). simpl. auto. - traceEq. - unfold tsp. econstructor; eauto with coqlib. - eapply agree_callee_save_agree; eauto. + 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. + econstructor; eauto. + apply match_stacks_change_mach_mem with m'0. + apply match_stacks_change_linear_mem with m. + rewrite SP_EQ; rewrite SP'_EQ. + eapply match_stacks_change_meminj; eauto. omega. + eauto with mem. intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega. + intros. eapply stores_in_frame_valid; eauto with mem. + intros. eapply stores_in_frame_perm; eauto with mem. + 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. (* external function *) simpl in TRANSL. inversion TRANSL; subst tf. inversion WTF. subst ef0. - exploit transl_external_arguments; eauto. intro EXTARGS. + exploit transl_external_arguments; eauto. intros [vl [ARGS VINJ]]. + exploit external_call_mem_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. econstructor; split. apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - intros. unfold Regmap.set. case (RegEq.eq r (loc_result (ef_sig ef))); intro. - rewrite e. rewrite Locmap.gss; auto. rewrite Locmap.gso; auto. - red; auto. - apply agree_callee_save_set_result; auto. + apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0). + eapply match_stack_change_extcall; eauto. omega. omega. + exploit external_call_valid_block. eexact H. + instantiate (1 := (Mem.nextblock m - 1)). red; omega. unfold Mem.valid_block; omega. + exploit external_call_valid_block. eexact A. + instantiate (1 := (Mem.nextblock m'0 - 1)). red; omega. unfold Mem.valid_block; omega. + apply wt_setloc; auto. simpl. rewrite loc_result_type. + change (Val.has_type res (proj_sig_res (ef_sig ef))). + eapply external_call_well_typed; eauto. + apply agree_regs_set_reg; auto. apply agree_regs_inject_incr with j; auto. + apply agree_callee_save_set_result; auto. (* return *) - inv STACKS. + inv STACKS. simpl in AGLOCS. econstructor; split. apply plus_one. apply exec_return. - econstructor; eauto. simpl in AG2. - eapply agree_frame_agree; eauto. + econstructor; eauto. + apply agree_frame_return with rs0; auto. Qed. Lemma transf_initial_states: forall st1, Linear.initial_state prog st1 -> - exists st2, Machabstr.initial_state tprog st2 /\ match_states st1 st2. + exists st2, Machconcr.initial_state tprog st2 /\ match_states st1 st2. Proof. - intros. inversion H. + intros. inv H. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. eapply Genv.init_mem_transf_partial; eauto. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. eauto. - eauto. - econstructor; eauto. constructor. - eapply Genv.find_funct_ptr_prop; eauto. - intros. rewrite H3 in H5. simpl in H5. contradiction. - simpl; red; auto. + econstructor; eauto. + eapply Genv.initmem_inject; eauto. + apply match_stacks_empty with (Mem.nextblock m0). omega. omega. + constructor. + apply Mem.nextblock_pos. + intros. unfold Mem.flat_inj. apply zlt_true; auto. + unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence. + intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto. + intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. + rewrite H3. red; intros. contradiction. + eapply Genv.find_funct_ptr_prop. eexact wt_prog. + fold ge0; eauto. + apply wt_init. + unfold Locmap.init. red; intros; auto. + unfold parent_locset. red; auto. Qed. Lemma transf_final_states: forall st1 st2 r, - match_states st1 st2 -> Linear.final_state st1 r -> Machabstr.final_state st2 r. + match_states st1 st2 -> Linear.final_state st1 r -> Machconcr.final_state st2 r. Proof. - intros. inv H0. inv H. inv STACKS. econstructor. rewrite AG1; auto. + intros. inv H0. inv H. inv STACKS. + constructor. + set (rres := loc_result {| sig_args := nil; sig_res := Some Tint |}) in *. + generalize (AGREGS rres). rewrite H1. intros IJ; inv IJ. auto. Qed. Theorem transf_program_correct: forall (beh: program_behavior), not_wrong beh -> - Linear.exec_program prog beh -> Machabstr.exec_program tprog beh. + Linear.exec_program prog beh -> Machconcr.exec_program tprog beh. Proof. - unfold Linear.exec_program, Machabstr.exec_program; intros. + unfold Linear.exec_program, Machconcr.exec_program; intros. eapply simulation_plus_preservation; eauto. eexact transf_initial_states. eexact transf_final_states. -- cgit v1.2.3