diff options
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 2806 |
1 files changed, 1030 insertions, 1776 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index a76fdbba..15953131 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -16,11 +16,13 @@ Require Import Coqlib Errors. Require Import Integers AST Linking. -Require Import Values Memory Events Globalenvs Smallstep. +Require Import Values Memory Separation Events Globalenvs Smallstep. Require Import LTL Op Locations Linear Mach. Require Import Bounds Conventions Stacklayout Lineartyping. Require Import Stacking. +Local Open Scope sep_scope. + Definition match_prog (p: Linear.program) (tp: Mach.program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -30,7 +32,7 @@ Proof. intros. eapply match_transform_partial_program; eauto. Qed. -(** * Properties of frame offsets *) +(** * Basic properties of the translation *) Lemma typesize_typesize: forall ty, AST.typesize ty = 4 * Locations.typesize ty. @@ -44,6 +46,30 @@ Proof. destruct ty; reflexivity. Qed. +Remark align_type_chunk: + forall ty, align_chunk (chunk_of_type ty) = 4 * Locations.typealign ty. +Proof. + destruct ty; reflexivity. +Qed. + +Lemma slot_outgoing_argument_valid: + forall f ofs ty sg, + In (S Outgoing ofs ty) (loc_arguments sg) -> slot_valid f Outgoing ofs ty = true. +Proof. + intros. exploit loc_arguments_acceptable; eauto. intros [A B]. + unfold slot_valid. unfold proj_sumbool. + rewrite zle_true by omega. + rewrite pred_dec_true by auto. + auto. +Qed. + +Lemma load_result_inject: + forall j ty v v', + Val.inject j v v' -> Val.has_type v ty -> Val.inject j v (Val.load_result (chunk_of_type ty) v'). +Proof. + destruct 1; intros; auto; destruct ty; simpl; try contradiction; econstructor; eauto. +Qed. + Section PRESERVATION. Variable return_address_offset: Mach.function -> Mach.code -> int -> Prop. @@ -108,486 +134,417 @@ 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. *) - -Definition index_valid (idx: frame_index) := - match idx with - | FI_link => True - | FI_retaddr => True - | FI_local x ty => ty <> Tlong /\ 0 <= x /\ x + typesize ty <= b.(bound_local) - | FI_arg x ty => ty <> Tlong /\ 0 <= x /\ x + typesize ty <= b.(bound_outgoing) - | FI_saved_int x => 0 <= x < b.(bound_int_callee_save) - | FI_saved_float x => 0 <= x < b.(bound_float_callee_save) - end. - -Definition type_of_index (idx: frame_index) := - match idx with - | FI_link => Tint - | FI_retaddr => Tint - | FI_local x ty => ty - | FI_arg x ty => ty - | FI_saved_int x => Tany32 - | FI_saved_float x => Tany64 - end. - -(** Non-overlap between the memory areas corresponding to two - frame indices. *) - -Definition index_diff (idx1 idx2: frame_index) : Prop := - match idx1, idx2 with - | FI_link, FI_link => False - | FI_retaddr, FI_retaddr => False - | FI_local x1 ty1, FI_local x2 ty2 => - x1 + typesize ty1 <= x2 \/ x2 + typesize ty2 <= x1 - | FI_arg x1 ty1, FI_arg x2 ty2 => - x1 + typesize ty1 <= x2 \/ x2 + typesize ty2 <= x1 - | FI_saved_int x1, FI_saved_int x2 => x1 <> x2 - | FI_saved_float x1, FI_saved_float x2 => x1 <> x2 - | _, _ => 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_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 (bound_stack_data_pos b); intro. - -Lemma size_pos: 0 <= fe.(fe_size). -Proof. - generalize (frame_env_separated b). intuition. - AddPosProps. - unfold fe. omega. -Qed. - -Opaque function_bounds. - -Ltac InvIndexValid := - match goal with - | [ H: ?ty <> Tlong /\ _ |- _ ] => - destruct H; generalize (typesize_pos ty) (typesize_typesize ty); intros - end. - -Lemma offset_of_index_disj: - forall idx1 idx2, - index_valid idx1 -> index_valid idx2 -> - index_diff idx1 idx2 -> - 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. - destruct idx1; destruct idx2; - simpl in V1; simpl in V2; repeat InvIndexValid; simpl in DIFF; - unfold offset_of_index, type_of_index; - change (AST.typesize Tany32) with 4; change (AST.typesize Tany64) with 8; - change (AST.typesize Tint) with 4; - 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; - simpl in V; repeat InvIndexValid; - unfold offset_of_index, type_of_index; - change (AST.typesize Tany32) with 4; change (AST.typesize Tany64) with 8; - change (AST.typesize Tint) with 4; - 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. +(** * Memory assertions used to describe the contents of stack frames *) -Remark aligned_8_4: - forall x, (8 | x) -> (4 | x). -Proof. intros. apply Zdivides_trans with 8; auto. exists 2; auto. Qed. +Local Opaque Z.add Z.mul Z.divide. -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. +(** Accessing the stack frame using [load_stack] and [store_stack]. *) -Lemma offset_of_index_aligned: - forall idx, (4 | offset_of_index fe idx). +Lemma contains_get_stack: + forall spec m ty sp ofs, + m |= contains (chunk_of_type ty) sp ofs spec -> + exists v, load_stack m (Vptr sp Int.zero) ty (Int.repr ofs) = Some v /\ spec v. Proof. - intros. - 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. + intros. unfold load_stack. + replace (Val.add (Vptr sp Int.zero) (Vint (Int.repr ofs))) with (Vptr sp (Int.repr ofs)). + eapply loadv_rule; eauto. + simpl. rewrite Int.add_zero_l; auto. Qed. -Lemma offset_of_index_aligned_2: - forall idx, index_valid idx -> - (align_chunk (chunk_of_type (type_of_index idx)) | offset_of_index fe idx). +Lemma hasvalue_get_stack: + forall ty m sp ofs v, + m |= hasvalue (chunk_of_type ty) sp ofs v -> + load_stack m (Vptr sp Int.zero) ty (Int.repr ofs) = Some v. Proof. - intros. replace (align_chunk (chunk_of_type (type_of_index idx))) with 4. - apply offset_of_index_aligned. - assert (type_of_index idx <> Tlong) by - (destruct idx; simpl; simpl in H; intuition congruence). - destruct (type_of_index idx); auto; congruence. + intros. exploit contains_get_stack; eauto. intros (v' & A & B). congruence. Qed. -Lemma fe_stack_data_aligned: - (8 | fe_stack_data fe). -Proof. - intros. - generalize (frame_env_aligned b). intuition. fold fe in H. intuition. +Lemma contains_set_stack: + forall (spec: val -> Prop) v spec1 m ty sp ofs P, + m |= contains (chunk_of_type ty) sp ofs spec1 ** P -> + spec (Val.load_result (chunk_of_type ty) v) -> + exists m', + store_stack m (Vptr sp Int.zero) ty (Int.repr ofs) v = Some m' + /\ m' |= contains (chunk_of_type ty) sp ofs spec ** P. +Proof. + intros. unfold store_stack. + replace (Val.add (Vptr sp Int.zero) (Vint (Int.repr ofs))) with (Vptr sp (Int.repr ofs)). + eapply storev_rule; eauto. + simpl. rewrite Int.add_zero_l; auto. +Qed. + +(** [contains_locations j sp pos bound sl ls] is a separation logic assertion + that holds if the memory area at block [sp], offset [pos], size [4 * bound], + reflects the values of the stack locations of kind [sl] given by the + location map [ls], up to the memory injection [j]. + + Two such [contains_locations] assertions will be used later, one to + reason about the values of [Local] slots, the other about the values of + [Outgoing] slots. *) + +Program Definition contains_locations (j: meminj) (sp: block) (pos bound: Z) (sl: slot) (ls: locset) : massert := {| + m_pred := fun m => + (8 | pos) /\ 0 <= pos /\ pos + 4 * bound <= Int.modulus /\ + Mem.range_perm m sp pos (pos + 4 * bound) Cur Freeable /\ + forall ofs ty, 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) -> + exists v, Mem.load (chunk_of_type ty) m sp (pos + 4 * ofs) = Some v + /\ Val.inject j (ls (S sl ofs ty)) v; + m_footprint := fun b ofs => + b = sp /\ pos <= ofs < pos + 4 * bound +|}. +Next Obligation. + intuition auto. +- red; intros. eapply Mem.perm_unchanged_on; eauto. simpl; auto. +- exploit H4; eauto. intros (v & A & B). exists v; split; auto. + eapply Mem.load_unchanged_on; eauto. + simpl; intros. rewrite size_type_chunk, typesize_typesize in H8. + split; auto. omega. +Qed. +Next Obligation. + eauto with mem. Qed. -(** The following lemmas give sufficient conditions for indices - of various kinds to be valid. *) +Remark valid_access_location: + forall m sp pos bound ofs ty p, + (8 | pos) -> + Mem.range_perm m sp pos (pos + 4 * bound) Cur Freeable -> + 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) -> + Mem.valid_access m (chunk_of_type ty) sp (pos + 4 * ofs) p. +Proof. + intros; split. +- red; intros. apply Mem.perm_implies with Freeable; auto with mem. + apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega. +- rewrite align_type_chunk. apply Z.divide_add_r. + apply Zdivide_trans with 8; auto. + exists (8 / (4 * typealign ty)); destruct ty; reflexivity. + apply Z.mul_divide_mono_l. auto. +Qed. + +Lemma get_location: + forall m j sp pos bound sl ls ofs ty, + m |= contains_locations j sp pos bound sl ls -> + 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) -> + exists v, + load_stack m (Vptr sp Int.zero) ty (Int.repr (pos + 4 * ofs)) = Some v + /\ Val.inject j (ls (S sl ofs ty)) v. +Proof. + intros. destruct H as (D & E & F & G & H). + exploit H; eauto. intros (v & U & V). exists v; split; auto. + unfold load_stack; simpl. rewrite Int.add_zero_l, Int.unsigned_repr; auto. + unfold Int.max_unsigned. generalize (typesize_pos ty). omega. +Qed. + +Lemma set_location: + forall m j sp pos bound sl ls P ofs ty v v', + m |= contains_locations j sp pos bound sl ls ** P -> + 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) -> + Val.inject j v v' -> + exists m', + store_stack m (Vptr sp Int.zero) ty (Int.repr (pos + 4 * ofs)) v' = Some m' + /\ m' |= contains_locations j sp pos bound sl (Locmap.set (S sl ofs ty) v ls) ** P. +Proof. + intros. destruct H as (A & B & C). destruct A as (D & E & F & G & H). + edestruct Mem.valid_access_store as [m' STORE]. + eapply valid_access_location; eauto. + assert (PERM: Mem.range_perm m' sp pos (pos + 4 * bound) Cur Freeable). + { red; intros; eauto with mem. } + exists m'; split. +- unfold store_stack; simpl. rewrite Int.add_zero_l, Int.unsigned_repr; eauto. + unfold Int.max_unsigned. generalize (typesize_pos ty). omega. +- simpl. intuition auto. ++ unfold Locmap.set. + destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))]. +* (* same location *) + inv e. rename ofs0 into ofs. rename ty0 into ty. + exists (Val.load_result (chunk_of_type ty) v'); split. + eapply Mem.load_store_similar_2; eauto. omega. + inv H3; destruct (chunk_of_type ty); simpl; econstructor; eauto. +* (* different locations *) + exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto. + rewrite <- X; eapply Mem.load_store_other; eauto. + destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. omega. +* (* overlapping locations *) + destruct (Mem.valid_access_load m' (chunk_of_type ty0) sp (pos + 4 * ofs0)) as [v'' LOAD]. + apply Mem.valid_access_implies with Writable; auto with mem. + eapply valid_access_location; eauto. + exists v''; auto. ++ apply (m_invar P) with m; auto. + eapply Mem.store_unchanged_on; eauto. + intros i; rewrite size_type_chunk, typesize_typesize. intros; red; intros. + eelim C; eauto. simpl. split; auto. omega. +Qed. + +Lemma initial_locations: + forall j sp pos bound P sl ls m, + m |= range sp pos (pos + 4 * bound) ** P -> + (8 | pos) -> + (forall ofs ty, ls (S sl ofs ty) = Vundef) -> + m |= contains_locations j sp pos bound sl ls ** P. +Proof. + intros. destruct H as (A & B & C). destruct A as (D & E & F). split. +- simpl; intuition auto. red; intros; eauto with mem. + destruct (Mem.valid_access_load m (chunk_of_type ty) sp (pos + 4 * ofs)) as [v LOAD]. + eapply valid_access_location; eauto. + red; intros; eauto with mem. + exists v; split; auto. rewrite H1; auto. +- split; assumption. +Qed. + +Lemma contains_locations_exten: + forall ls ls' j sp pos bound sl, + (forall ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) -> + massert_imp (contains_locations j sp pos bound sl ls) + (contains_locations j sp pos bound sl ls'). +Proof. + intros; split; simpl; intros; auto. + intuition auto. rewrite H. eauto. +Qed. + +Lemma contains_locations_incr: + forall j j' sp pos bound sl ls, + inject_incr j j' -> + massert_imp (contains_locations j sp pos bound sl ls) + (contains_locations j' sp pos bound sl ls). +Proof. + intros; split; simpl; intros; auto. + intuition auto. exploit H5; eauto. intros (v & A & B). exists v; eauto. +Qed. + +(** [contains_callee_saves j sp pos rl ls] is a memory assertion that holds + if block [sp], starting at offset [pos], contains the values of the + callee-save registers [rl] as given by the location map [ls], + up to the memory injection [j]. The memory layout of the registers in [rl] + is the same as that implemented by [save_callee_save_rec]. *) + +Fixpoint contains_callee_saves (j: meminj) (sp: block) (pos: Z) (rl: list mreg) (ls: locset) : massert := + match rl with + | nil => pure True + | r :: rl => + let ty := mreg_type r in + let sz := AST.typesize ty in + let pos1 := align pos sz in + contains (chunk_of_type ty) sp pos1 (fun v => Val.inject j (ls (R r)) v) + ** contains_callee_saves j sp (pos1 + sz) rl ls + end. -Lemma index_local_valid: - forall ofs ty, +Lemma contains_callee_saves_incr: + forall j j' sp ls, + inject_incr j j' -> + forall rl pos, + massert_imp (contains_callee_saves j sp pos rl ls) + (contains_callee_saves j' sp pos rl ls). +Proof. + induction rl as [ | r1 rl]; simpl; intros. +- reflexivity. +- apply sepconj_morph_1; auto. apply contains_imp. eauto. +Qed. + +Lemma contains_callee_saves_exten: + forall j sp ls ls' rl pos, + (forall r, In r rl -> ls' (R r) = ls (R r)) -> + massert_eqv (contains_callee_saves j sp pos rl ls) + (contains_callee_saves j sp pos rl ls'). +Proof. + induction rl as [ | r1 rl]; simpl; intros. +- reflexivity. +- apply sepconj_morph_2; auto. rewrite H by auto. reflexivity. +Qed. + +(** Separation logic assertions describing the stack frame at [sp]. + It must contain: + - the values of the [Local] stack slots of [ls], as per [contains_locations] + - the values of the [Outgoing] stack slots of [ls], as per [contains_locations] + - the [parent] pointer representing the back link to the caller's frame + - the [retaddr] pointer representing the saved return address + - the initial values of the used callee-save registers as given by [ls0], + as per [contains_callee_saves]. + +In addition, we use a nonseparating conjunction to record the fact that +we have full access rights on the stack frame, except the part that +represents the Linear stack data. *) + +Definition frame_contents_1 (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) := + contains_locations j sp fe.(fe_ofs_local) b.(bound_local) Local ls + ** contains_locations j sp fe_ofs_arg b.(bound_outgoing) Outgoing ls + ** hasvalue Mint32 sp fe.(fe_ofs_link) parent + ** hasvalue Mint32 sp fe.(fe_ofs_retaddr) retaddr + ** contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0. + +Definition frame_contents (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) := + mconj (frame_contents_1 j sp ls ls0 parent retaddr) + (range sp 0 fe.(fe_stack_data) ** + range sp (fe.(fe_stack_data) + b.(bound_stack_data)) fe.(fe_size)). + +(** Accessing components of the frame. *) + +Lemma frame_get_local: + forall ofs ty j sp ls ls0 parent retaddr m P, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> - index_valid (FI_local ofs ty). + exists v, + load_stack m (Vptr sp Int.zero) ty (Int.repr (offset_local fe ofs)) = Some v + /\ Val.inject j (ls (S Local ofs ty)) v. Proof. - unfold slot_within_bounds, slot_valid, index_valid; intros. - InvBooleans. - split. destruct ty; auto || discriminate. auto. + unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans. + apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_proj1 in H. + eapply get_location; eauto. Qed. -Lemma index_arg_valid: - forall ofs ty, +Lemma frame_get_outgoing: + forall ofs ty j sp ls ls0 parent retaddr m P, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> - index_valid (FI_arg ofs ty). + exists v, + load_stack m (Vptr sp Int.zero) ty (Int.repr (offset_arg ofs)) = Some v + /\ Val.inject j (ls (S Outgoing ofs ty)) v. Proof. - unfold slot_within_bounds, slot_valid, index_valid; intros. - InvBooleans. - split. destruct ty; auto || discriminate. auto. + unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans. + apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick2 in H. + eapply get_location; eauto. Qed. -Lemma index_saved_int_valid: - forall r, - In r int_callee_save_regs -> - index_int_callee_save r < b.(bound_int_callee_save) -> - index_valid (FI_saved_int (index_int_callee_save r)). +Lemma frame_get_parent: + forall j sp ls ls0 parent retaddr m P, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + load_stack m (Vptr sp Int.zero) Tint (Int.repr fe.(fe_ofs_link)) = Some parent. Proof. - intros. red. split. - apply Zge_le. apply index_int_callee_save_pos; auto. - auto. + unfold frame_contents, frame_contents_1; intros. + apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick3 in H. + eapply hasvalue_get_stack; eauto. Qed. -Lemma index_saved_float_valid: - forall r, - In r float_callee_save_regs -> - index_float_callee_save r < b.(bound_float_callee_save) -> - index_valid (FI_saved_float (index_float_callee_save r)). +Lemma frame_get_retaddr: + forall j sp ls ls0 parent retaddr m P, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + load_stack m (Vptr sp Int.zero) Tint (Int.repr fe.(fe_ofs_retaddr)) = Some retaddr. Proof. - intros. red. split. - apply Zge_le. apply index_float_callee_save_pos; auto. - auto. + unfold frame_contents, frame_contents_1; intros. + apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick4 in H. + eapply hasvalue_get_stack; eauto. Qed. -Hint Resolve index_local_valid index_arg_valid - index_saved_int_valid index_saved_float_valid: stacking. - -(** The offset of a valid index lies within the bounds of the frame. *) - -Lemma offset_of_index_valid: - forall idx, - index_valid idx -> - 0 <= offset_of_index fe idx /\ - 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; simpl in V; repeat InvIndexValid; - unfold offset_of_index, type_of_index; - change (AST.typesize Tany32) with 4; change (AST.typesize Tany64) with 8; - change (AST.typesize Tint) with 4; - omega. -Qed. +(** Assigning a [Local] or [Outgoing] stack slot. *) -(** 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. - omega. -Qed. - -(** Offsets for valid index are representable as signed machine integers - without loss of precision. *) - -Lemma offset_of_index_no_overflow: - forall idx, - index_valid 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.unsigned_repr. - generalize (AST.typesize_pos (type_of_index idx)). - generalize size_no_overflow. - omega. -Qed. - -(** Likewise, for offsets within the Linear stack slot, after shifting. *) - -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. - -(** * Contents of frame slots *) - -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. +Lemma frame_set_local: + forall ofs ty v v' j sp ls ls0 parent retaddr m P, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> + Val.inject j v v' -> + exists m', + store_stack m (Vptr sp Int.zero) ty (Int.repr (offset_local fe ofs)) v' = Some m' + /\ m' |= frame_contents j sp (Locmap.set (S Local ofs ty) v ls) ls0 parent retaddr ** P. +Proof. + intros. unfold frame_contents in H. + exploit mconj_proj1; eauto. unfold frame_contents_1. + rewrite ! sep_assoc; intros SEP. + unfold slot_valid in H1; InvBooleans. simpl in H0. + exploit set_location; eauto. intros (m' & A & B). + exists m'; split; auto. + assert (forall i k p, Mem.perm m sp i k p -> Mem.perm m' sp i k p). + { intros. unfold store_stack in A; simpl in A. eapply Mem.perm_store_1; eauto. } + eapply frame_mconj. eauto. + unfold frame_contents_1; rewrite ! sep_assoc; exact B. + eapply sep_preserved. + eapply sep_proj1. eapply mconj_proj2. eassumption. + intros; eapply range_preserved; eauto. + intros; eapply range_preserved; eauto. +Qed. + +Lemma frame_set_outgoing: + forall ofs ty v v' j sp ls ls0 parent retaddr m P, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> + Val.inject j v v' -> + exists m', + store_stack m (Vptr sp Int.zero) ty (Int.repr (offset_arg ofs)) v' = Some m' + /\ m' |= frame_contents j sp (Locmap.set (S Outgoing ofs ty) v ls) ls0 parent retaddr ** P. 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. + intros. unfold frame_contents in H. + exploit mconj_proj1; eauto. unfold frame_contents_1. + rewrite ! sep_assoc, sep_swap. intros SEP. + unfold slot_valid in H1; InvBooleans. simpl in H0. + exploit set_location; eauto. intros (m' & A & B). + exists m'; split; auto. + assert (forall i k p, Mem.perm m sp i k p -> Mem.perm m' sp i k p). + { intros. unfold store_stack in A; simpl in A. eapply Mem.perm_store_1; eauto. } + eapply frame_mconj. eauto. + unfold frame_contents_1; rewrite ! sep_assoc, sep_swap; eauto. + eapply sep_preserved. + eapply sep_proj1. eapply mconj_proj2. eassumption. + intros; eapply range_preserved; eauto. + intros; eapply range_preserved; eauto. Qed. -(** Good variable properties for [index_contains] *) +(** Invariance by change of location maps. *) -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. omega. - 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 *; - try contradiction; auto. - 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 Cur 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)) Cur Freeable. +Lemma frame_contents_exten: + forall ls ls0 ls' ls0' j sp parent retaddr P m, + (forall sl ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) -> + (forall r, In r b.(used_callee_save) -> ls0' (R r) = ls0 (R r)) -> + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + m |= frame_contents j sp ls' ls0' parent retaddr ** P. Proof. - intros. - 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. + unfold frame_contents, frame_contents_1; intros. + rewrite <- ! (contains_locations_exten ls ls') by auto. + erewrite <- contains_callee_saves_exten by eauto. + assumption. Qed. -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. - apply offset_of_index_aligned_2; auto. - exists m'; auto. -Qed. +(** Invariance by assignment to registers. *) -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'. +Corollary frame_set_reg: + forall r v j sp ls ls0 parent retaddr m P, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + m |= frame_contents j sp (Locmap.set (R r) v ls) ls0 parent retaddr ** P. Proof. - intros. unfold store_stack, Mem.storev, Val.add. - rewrite Int.add_commut. rewrite Int.add_zero. - rewrite offset_of_index_no_overflow; auto. + intros. apply frame_contents_exten with ls ls0; auto. Qed. -(** A variant of [index_contains], up to a memory injection. *) - -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'. - -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. +Corollary frame_undef_regs: + forall j sp ls ls0 parent retaddr m P rl, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + m |= frame_contents j sp (LTL.undef_regs rl ls) ls0 parent retaddr ** P. 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. - econstructor; eauto. - econstructor; eauto. +Local Opaque sepconj. + induction rl; simpl; intros. +- auto. +- apply frame_set_reg; auto. Qed. -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.inject j v v' -> - index_contains_inj j m' sp idx (Val.load_result (chunk_of_type (type_of_index idx)) v). +Corollary frame_set_regs: + forall j sp ls0 parent retaddr m P rl vl ls, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + m |= frame_contents j sp (Locmap.setlist (map R rl) vl ls) ls0 parent retaddr ** P. Proof. - intros. exploit gss_index_contains_base; eauto. intros [v'' [A B]]. - exists v''; split; auto. - inv H1; destruct (type_of_index idx); simpl in *; try contradiction; subst; auto. - econstructor; eauto. - econstructor; eauto. - econstructor; eauto. + induction rl; destruct vl; simpl; intros; trivial. apply IHrl. apply frame_set_reg; auto. Qed. -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'. +Corollary frame_set_res: + forall j sp ls0 parent retaddr m P res v ls, + m |= frame_contents j sp ls ls0 parent retaddr ** P -> + m |= frame_contents j sp (Locmap.setres res v ls) ls0 parent retaddr ** P. Proof. - intros. destruct H1 as [v'' [A B]]. exists v''; split; auto. - eapply gso_index_contains; eauto. + induction res; simpl; intros. +- apply frame_set_reg; auto. +- auto. +- 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. +(** Invariance by change of memory injection. *) -Lemma index_contains_inj_incr: - forall j m sp idx v j', - index_contains_inj j m sp idx v -> +Lemma frame_contents_incr: + forall j sp ls ls0 parent retaddr m P j', + m |= frame_contents j sp ls ls0 parent retaddr ** P -> 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. + m |= frame_contents j' sp ls ls0 parent retaddr ** P. 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. - apply offset_of_index_aligned_2; auto. - intros [v C]. - exists v; split; auto. constructor; auto. + unfold frame_contents, frame_contents_1; intros. + rewrite <- (contains_locations_incr j j') by auto. + rewrite <- (contains_locations_incr j j') by auto. + erewrite <- contains_callee_saves_incr by eauto. + assumption. 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 *) @@ -595,89 +552,29 @@ Hint Resolve store_other_index_contains_inj index_contains_inj_incr: stacking. 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 *) +(** Agreement over locations *) -Record agree_frame (j: meminj) (ls ls0: locset) - (m: mem) (sp: block) - (m': mem) (sp': block) - (parent retaddr: val) : Prop := - mk_agree_frame { +Record agree_locs (ls ls0: locset) : Prop := + mk_agree_locs { (** Unused registers have the same value as in the caller *) agree_unused_reg: 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 - at the corresponding offsets. *) - agree_locals: - forall ofs ty, - slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> - index_contains_inj j m' sp' (FI_local ofs ty) (ls (S Local ofs ty)); - agree_outgoing: - forall ofs ty, - slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> - index_contains_inj j m' sp' (FI_arg ofs ty) (ls (S Outgoing ofs ty)); - (** 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)) -> - 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 - 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_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_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: - forall ofs p, Mem.perm m sp ofs Max p -> 0 <= ofs < f.(Linear.fn_stacksize); - - (** Permissions on the frame part of the Mach stack block *) - agree_perm: - frame_perm_freeable m' sp' - }. - -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: stacking. + ls (S Incoming ofs ty) = ls0 (S Outgoing ofs ty) +}. (** Auxiliary predicate used at call points *) Definition agree_callee_save (ls ls0: locset) : Prop := forall l, match l with - | R r => ~In r destroyed_at_call + | R r => is_callee_save r = true | S _ _ _ => True end -> ls l = ls0 l. @@ -698,7 +595,7 @@ Lemma agree_reglist: agree_regs j ls rs -> Val.inject_list j (reglist ls rl) (rs##rl). Proof. induction rl; simpl; intros. - auto. constructor. eauto with stacking. auto. + auto. constructor; auto using agree_reg. Qed. Hint Resolve agree_reg agree_reglist: stacking. @@ -795,310 +692,130 @@ Proof. unfold call_regs; intros; red; intros; auto. Qed. -(** ** Properties of [agree_frame] *) +(** ** Properties of [agree_locs] *) (** 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 -> +Lemma agree_locs_set_reg: + forall ls ls0 r v, + agree_locs ls ls0 -> mreg_within_bounds b r -> - agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra. + agree_locs (Locmap.set (R r) v ls) ls0. Proof. intros. inv H; constructor; auto; intros. rewrite Locmap.gso. auto. red. intuition congruence. Qed. -Lemma agree_frame_set_regs: - forall j ls0 m sp m' sp' parent ra rl vl ls, - agree_frame j ls ls0 m sp m' sp' parent ra -> +Lemma agree_locs_set_regs: + forall ls0 rl vl ls, + agree_locs ls ls0 -> (forall r, In r rl -> mreg_within_bounds b r) -> - agree_frame j (Locmap.setlist (map R rl) vl ls) ls0 m sp m' sp' parent ra. + agree_locs (Locmap.setlist (map R rl) vl ls) ls0. Proof. - induction rl; destruct vl; simpl; intros; intuition. - apply IHrl; auto. - eapply agree_frame_set_reg; eauto. + induction rl; destruct vl; simpl; intros; auto. + apply IHrl; auto. apply agree_locs_set_reg; auto. Qed. -Lemma agree_frame_set_res: - forall j ls0 m sp m' sp' parent ra res v ls, - agree_frame j ls ls0 m sp m' sp' parent ra -> +Lemma agree_locs_set_res: + forall ls0 res v ls, + agree_locs ls ls0 -> (forall r, In r (params_of_builtin_res res) -> mreg_within_bounds b r) -> - agree_frame j (Locmap.setres res v ls) ls0 m sp m' sp' parent ra. + agree_locs (Locmap.setres res v ls) ls0. Proof. induction res; simpl; intros. -- eapply agree_frame_set_reg; eauto. +- eapply agree_locs_set_reg; eauto. - auto. - apply IHres2; auto using in_or_app. Qed. -Lemma agree_frame_undef_regs: - forall j ls0 m sp m' sp' parent ra regs ls, - agree_frame j ls ls0 m sp m' sp' parent ra -> +Lemma agree_locs_undef_regs: + forall ls0 regs ls, + agree_locs ls ls0 -> (forall r, In r regs -> mreg_within_bounds b r) -> - agree_frame j (LTL.undef_regs regs ls) ls0 m sp m' sp' parent ra. + agree_locs (LTL.undef_regs regs ls) ls0. Proof. induction regs; simpl; intros. auto. - apply agree_frame_set_reg; auto. + apply agree_locs_set_reg; auto. Qed. Lemma caller_save_reg_within_bounds: forall r, - In r destroyed_at_call -> mreg_within_bounds b r. + is_callee_save r = false -> mreg_within_bounds b r. Proof. - intros. red. - destruct (zlt (index_int_callee_save r) 0). - destruct (zlt (index_float_callee_save r) 0). - generalize (bound_int_callee_save_pos b) (bound_float_callee_save_pos b); omega. - exfalso. eapply float_callee_save_not_destroyed; eauto. eapply index_float_callee_save_pos2; eauto. - exfalso. eapply int_callee_save_not_destroyed; eauto. eapply index_int_callee_save_pos2; eauto. + intros; red; intros. congruence. Qed. -Lemma agree_frame_undef_locs: - forall j ls0 m sp m' sp' parent ra regs ls, - agree_frame j ls ls0 m sp m' sp' parent ra -> - incl regs destroyed_at_call -> - agree_frame j (LTL.undef_regs regs ls) ls0 m sp m' sp' parent ra. +Lemma agree_locs_undef_locs_1: + forall ls0 regs ls, + agree_locs ls ls0 -> + (forall r, In r regs -> is_callee_save r = false) -> + agree_locs (LTL.undef_regs regs ls) ls0. Proof. - intros. eapply agree_frame_undef_regs; eauto. + intros. eapply agree_locs_undef_regs; eauto. intros. apply caller_save_reg_within_bounds. auto. Qed. -(** 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 b Local ofs ty -> slot_valid f Local ofs ty = true -> - Val.inject j v v' -> - 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. +Lemma agree_locs_undef_locs: + forall ls0 regs ls, + agree_locs ls ls0 -> + existsb is_callee_save regs = false -> + agree_locs (LTL.undef_regs regs ls) ls0. Proof. - intros. inv H. - change (chunk_of_type ty) with (chunk_of_type (type_of_index (FI_local ofs ty))) in H3. - constructor; auto; intros. -(* local *) - unfold Locmap.set. - destruct (Loc.eq (S Local ofs ty) (S Local ofs0 ty0)). - inv e. eapply gss_index_contains_inj'; eauto with stacking. - destruct (Loc.diff_dec (S Local ofs ty) (S Local ofs0 ty0)). - eapply gso_index_contains_inj. eauto. eauto with stacking. eauto. - simpl. simpl in d. intuition. - apply index_contains_inj_undef. auto with stacking. - red; intros. eapply Mem.perm_store_1; eauto. -(* outgoing *) - rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. - red; auto. red; left; congruence. -(* 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. -(* perm *) - red; intros. eapply Mem.perm_store_1; eauto. + intros. eapply agree_locs_undef_locs_1; eauto. + intros. destruct (is_callee_save r) eqn:CS; auto. + assert (existsb is_callee_save regs = true). + { apply existsb_exists. exists r; auto. } + congruence. Qed. -(** Preservation by assignment to outgoing slot *) +(** Preservation by assignment to local 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 b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> - Val.inject j v v' -> - 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. +Lemma agree_locs_set_slot: + forall ls ls0 sl ofs ty v, + agree_locs ls ls0 -> + slot_writable sl = true -> + agree_locs (Locmap.set (S sl ofs ty) v ls) ls0. 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. -(* local *) - rewrite Locmap.gso. eapply gso_index_contains_inj; eauto with stacking. red; auto. - red; left; congruence. -(* outgoing *) - unfold Locmap.set. destruct (Loc.eq (S Outgoing ofs ty) (S Outgoing ofs0 ty0)). - inv e. eapply gss_index_contains_inj'; eauto with stacking. - destruct (Loc.diff_dec (S Outgoing ofs ty) (S Outgoing ofs0 ty0)). - eapply gso_index_contains_inj; eauto with stacking. - red. red in d. intuition. - apply index_contains_inj_undef. auto with stacking. - red; intros. eapply Mem.perm_store_1; eauto. -(* 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. -Qed. - -(** 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) -> - (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> - (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> - (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 k p, - ofs < fe.(fe_stack_data) \/ fe.(fe_stack_data) + f.(Linear.fn_stacksize) <= ofs -> - Mem.perm m' sp' ofs k p -> Mem.perm m1' sp' ofs k p) -> - agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. -Proof. - 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. - eauto. - red; intros. apply H4; auto. -Qed. - -(** A variant of the latter, for use with external calls *) - -Lemma agree_frame_extcall_invariant: - forall j ls ls0 m sp m' sp' parent retaddr m1 m1', - agree_frame j ls ls0 m sp m' sp' parent retaddr -> - (Mem.valid_block m sp -> Mem.valid_block m1 sp) -> - (forall ofs p, Mem.perm m1 sp ofs Max p -> Mem.perm m sp ofs Max p) -> - (Mem.valid_block m' sp' -> Mem.valid_block m1' sp') -> - Mem.unchanged_on (loc_out_of_reach j m) m' m1' -> - agree_frame j ls ls0 m1 sp m1' sp' parent retaddr. -Proof. - 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. - red; intros. exploit agree_bounds; eauto. omega. - eapply agree_frame_invariant; eauto. - intros. eapply Mem.load_unchanged_on; eauto. intros. apply REACH. omega. auto. - intros. eapply Mem.perm_unchanged_on; eauto with mem. auto. -Qed. - -(** Preservation by parallel stores in the Linear and Mach codes *) - -Lemma agree_frame_parallel_stores: - forall j ls ls0 m sp m' sp' parent 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. - eauto with mem. - eauto with mem. - intros. rewrite <- H1. eapply Mem.load_store_other; eauto. - destruct (eq_block 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]. - rewrite shifted_stack_offset_no_overflow. - exploit agree_bounds. eauto. apply Mem.perm_cur_max. apply A. - instantiate (1 := Int.unsigned ofs1). generalize (size_chunk_pos chunk). omega. - intros C. - exploit agree_bounds. eauto. apply Mem.perm_cur_max. apply A. - instantiate (1 := Int.unsigned ofs1 + size_chunk chunk - 1). generalize (size_chunk_pos chunk). omega. - intros D. - omega. - eapply agree_bounds. eauto. apply Mem.perm_cur_max. apply A. - generalize (size_chunk_pos chunk). omega. - intros; eauto with mem. -Qed. - -(** Preservation by increasing memory injections (allocations and external calls) *) - -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. + intros. destruct H; constructor; intros. +- rewrite Locmap.gso; auto. red; auto. +- rewrite Locmap.gso; auto. red. left. destruct sl; discriminate. Qed. (** Preservation at return points (when [ls] is changed but not [ls0]). *) -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 -> +Lemma agree_locs_return: + forall ls ls0 ls', + agree_locs ls ls0 -> agree_callee_save ls' ls -> - agree_frame j ls' ls0 m sp m' sp' parent retaddr. + agree_locs ls' ls0. Proof. intros. red in H0. inv H; constructor; auto; intros. - rewrite H0; auto. red; intros; elim H. apply caller_save_reg_within_bounds; auto. - rewrite H0; auto. - rewrite H0; auto. - rewrite H0; auto. +- rewrite H0; auto. unfold mreg_within_bounds in H. tauto. +- 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 -> +Lemma agree_locs_tailcall: + forall ls ls0 ls0', + agree_locs ls ls0 -> agree_callee_save ls0 ls0' -> - agree_frame j ls ls0' m sp m' sp' parent retaddr. + agree_locs ls ls0'. Proof. intros. red in H0. inv H; constructor; auto; intros. - rewrite <- H0; auto. red; intros; elim H. apply caller_save_reg_within_bounds; auto. - rewrite <- H0; auto. - rewrite <- H0. auto. red; intros. eapply int_callee_save_not_destroyed; eauto. - rewrite <- H0. auto. red; intros. eapply float_callee_save_not_destroyed; eauto. +- rewrite <- H0; auto. unfold mreg_within_bounds in H. tauto. +- rewrite <- H0; auto. Qed. -(** Properties of [agree_callee_save]. *) +(** ** Properties of [agree_callee_save]. *) Lemma agree_callee_save_return_regs: forall ls1 ls2, agree_callee_save (return_regs ls1 ls2) ls1. Proof. intros; red; intros. - unfold return_regs. destruct l; auto. - rewrite pred_dec_false; auto. + unfold return_regs. destruct l; auto. rewrite H; auto. Qed. Lemma agree_callee_save_set_result: @@ -1108,74 +825,60 @@ Lemma agree_callee_save_set_result: Proof. intros sg. generalize (loc_result_caller_save sg). generalize (loc_result sg). -Opaque destroyed_at_call. induction l; simpl; intros. auto. destruct vl; auto. apply IHl; auto. red; intros. rewrite Locmap.gso. apply H0; auto. - destruct l0; simpl; auto. + destruct l0; simpl; auto. red; intros; subst a. + assert (is_callee_save r = false) by auto. congruence. Qed. -(** Properties of destroyed registers. *) +(** ** Properties of destroyed registers. *) -Lemma check_mreg_list_incl: - forall l1 l2, - forallb (fun r => In_dec mreg_eq r l2) l1 = true -> - incl l1 l2. -Proof. - intros; red; intros. - rewrite forallb_forall in H. eapply proj_sumbool_true. eauto. -Qed. +Definition no_callee_saves (l: list mreg) : Prop := + existsb is_callee_save l = false. Remark destroyed_by_op_caller_save: - forall op, incl (destroyed_by_op op) destroyed_at_call. + forall op, no_callee_saves (destroyed_by_op op). Proof. - destruct op; apply check_mreg_list_incl; compute; auto. + unfold no_callee_saves; destruct op; reflexivity. Qed. Remark destroyed_by_load_caller_save: - forall chunk addr, incl (destroyed_by_load chunk addr) destroyed_at_call. + forall chunk addr, no_callee_saves (destroyed_by_load chunk addr). Proof. - intros. destruct chunk; apply check_mreg_list_incl; compute; auto. + unfold no_callee_saves; destruct chunk; reflexivity. Qed. Remark destroyed_by_store_caller_save: - forall chunk addr, incl (destroyed_by_store chunk addr) destroyed_at_call. + forall chunk addr, no_callee_saves (destroyed_by_store chunk addr). Proof. - intros. destruct chunk; apply check_mreg_list_incl; compute; auto. + unfold no_callee_saves; destruct chunk; reflexivity. Qed. Remark destroyed_by_cond_caller_save: - forall cond, incl (destroyed_by_cond cond) destroyed_at_call. + forall cond, no_callee_saves (destroyed_by_cond cond). Proof. - destruct cond; apply check_mreg_list_incl; compute; auto. + unfold no_callee_saves; destruct cond; reflexivity. Qed. Remark destroyed_by_jumptable_caller_save: - incl destroyed_by_jumptable destroyed_at_call. + no_callee_saves destroyed_by_jumptable. Proof. - apply check_mreg_list_incl; compute; auto. + red; reflexivity. Qed. Remark destroyed_by_setstack_caller_save: - forall ty, incl (destroyed_by_setstack ty) destroyed_at_call. + forall ty, no_callee_saves (destroyed_by_setstack ty). Proof. - destruct ty; apply check_mreg_list_incl; compute; auto. + unfold no_callee_saves; destruct ty; reflexivity. Qed. Remark destroyed_at_function_entry_caller_save: - incl destroyed_at_function_entry destroyed_at_call. + no_callee_saves destroyed_at_function_entry. Proof. - apply check_mreg_list_incl; compute; auto. -Qed. - -Remark temp_for_parent_frame_caller_save: - In temp_for_parent_frame destroyed_at_call. -Proof. - Transparent temp_for_parent_frame. - Transparent destroyed_at_call. - unfold temp_for_parent_frame; simpl; tauto. + red; reflexivity. Qed. Hint Resolve destroyed_by_op_caller_save destroyed_by_load_caller_save @@ -1186,7 +889,8 @@ Hint Resolve destroyed_by_op_caller_save destroyed_by_load_caller_save Remark destroyed_by_setstack_function_entry: forall ty, incl (destroyed_by_setstack ty) destroyed_at_function_entry. Proof. - destruct ty; apply check_mreg_list_incl; compute; auto. +Local Transparent destroyed_by_setstack destroyed_at_function_entry. + unfold incl; destruct ty; simpl; tauto. Qed. Remark transl_destroyed_by_op: @@ -1216,129 +920,67 @@ Qed. Section SAVE_CALLEE_SAVE. -Variable bound: frame_env -> Z. -Variable number: mreg -> Z. -Variable mkindex: Z -> frame_index. -Variable ty: typ. Variable j: meminj. Variable cs: list stackframe. Variable fb: block. Variable sp: block. -Variable csregs: list mreg. Variable ls: locset. -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_typ: - forall z, type_of_index (mkindex z) = ty. -Hypothesis mkindex_inj: - forall z1 z2, z1 <> z2 -> mkindex z1 <> mkindex z2. -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 ls_temp_undef: - forall r, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef. + forall ty r, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef. Hypothesis wt_ls: forall r, Val.has_type (ls (R r)) (mreg_type r). -Lemma save_callee_save_regs_correct: - forall l k rs m, - incl l csregs -> - list_norepet l -> - frame_perm_freeable m sp -> +Lemma save_callee_save_rec_correct: + forall k l pos rs m P, + (forall r, In r l -> is_callee_save r = true) -> + m |= range sp pos (size_callee_save_area_rec l pos) ** P -> agree_regs j ls rs -> exists rs', exists m', - star step tge - (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_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_contains m sp idx v -> - index_contains m' sp idx v) - /\ stores_in_frame m m' - /\ frame_perm_freeable m' sp + star step tge + (State cs fb (Vptr sp Int.zero) (save_callee_save_rec l pos k) rs m) + E0 (State cs fb (Vptr sp Int.zero) k rs' m') + /\ m' |= contains_callee_saves j sp pos l ls ** P + /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p) /\ agree_regs j ls rs'. Proof. - induction l; intros; simpl save_callee_save_regs. - (* base case *) - exists rs; exists m. split. apply star_refl. - split. intros. elim H3. - split. auto. - split. constructor. + induction l as [ | r l]; simpl; intros until P; intros CS SEP AG. +- exists rs, m. + split. apply star_refl. + split. rewrite sep_pure; split; auto. eapply sep_drop; eauto. + split. auto. auto. - (* inductive case *) - 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 *) - exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. - eauto. instantiate (1 := rs a). intros [m1 ST]. - exploit (IHl k (undef_regs (destroyed_by_setstack ty) rs) m1). auto with coqlib. auto. - red; eauto with mem. - apply agree_regs_exten with ls rs. auto. - intros. destruct (In_dec mreg_eq r (destroyed_by_setstack ty)). - left. apply ls_temp_undef; auto. - right; split. auto. apply undef_regs_other; auto. - intros [rs' [m' [A [B [C [D [E F]]]]]]]. - exists rs'; exists m'. - split. eapply star_left; eauto. econstructor. - rewrite <- (mkindex_typ (number a)). - apply store_stack_succeeds; auto with coqlib. - auto. traceEq. - split; intros. - simpl in H3. 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 H5 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. +- set (ty := mreg_type r) in *. + set (sz := AST.typesize ty) in *. + set (pos1 := align pos sz) in *. + assert (SZPOS: sz > 0) by (apply AST.typesize_pos). + assert (SZREC: pos1 + sz <= size_callee_save_area_rec l (pos1 + sz)) by (apply size_callee_save_area_rec_incr). + assert (POS1: pos <= pos1) by (apply align_le; auto). + assert (AL1: (align_chunk (chunk_of_type ty) | pos1)). + { unfold pos1. apply Zdivide_trans with sz. + unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides. + apply align_divides; auto. } + apply range_drop_left with (mid := pos1) in SEP; [ | omega ]. + apply range_split with (mid := pos1 + sz) in SEP; [ | omega ]. + unfold sz at 1 in SEP. rewrite <- size_type_chunk in SEP. + apply range_contains in SEP; auto. + exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)). + eexact SEP. + apply load_result_inject; auto. apply wt_ls. + clear SEP; intros (m1 & STORE & SEP). + set (rs1 := undef_regs (destroyed_by_setstack ty) rs). + assert (AG1: agree_regs j ls rs1). + { red; intros. unfold rs1. destruct (In_dec mreg_eq r0 (destroyed_by_setstack ty)). + erewrite ls_temp_undef by eauto. auto. + rewrite undef_regs_other by auto. apply AG. } + rewrite sep_swap in SEP. + exploit (IHl (pos1 + sz) rs1 m1); eauto. + intros (rs2 & m2 & A & B & C & D). + exists rs2, m2. + split. eapply star_left; eauto. constructor. exact STORE. auto. traceEq. + split. rewrite sep_assoc, sep_swap. exact B. + split. intros. apply C. unfold store_stack in STORE; simpl in STORE. eapply Mem.perm_store_1; eauto. auto. - (* no store takes place *) - exploit (IHl k rs m); auto with coqlib. - intros [rs' [m' [A [B [C [D [E F]]]]]]]. - exists rs'; exists m'; intuition. - simpl in H3. destruct H3. subst r. omegaContradiction. apply B; auto. - apply C; auto with coqlib. - intros. eapply H4; eauto. auto with coqlib. Qed. End SAVE_CALLEE_SAVE. @@ -1366,127 +1008,7 @@ Proof. rewrite Locmap.gso. apply IHrl. red; auto. Qed. -Lemma save_callee_save_correct: - forall j ls0 rs sp cs fb k m, - let ls := LTL.undef_regs destroyed_at_function_entry ls0 in - agree_regs j ls rs -> - (forall r, Val.has_type (ls (R r)) (mreg_type r)) -> - frame_perm_freeable m sp -> - exists rs', exists m', - star step tge - (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 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 | 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 - /\ agree_regs j ls rs'. -Proof. - intros. - assert (UNDEF: forall r ty, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef). - intros. unfold ls. apply LTL_undef_regs_same. eapply destroyed_by_setstack_function_entry; eauto. - exploit (save_callee_save_regs_correct - fe_num_int_callee_save - index_int_callee_save - FI_saved_int Tany32 - j cs fb sp int_callee_save_regs ls). - intros. apply index_int_callee_save_inj; auto. - intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption. - auto. - intros; congruence. - intros; simpl. destruct idx; auto. congruence. - intros. apply int_callee_save_type. auto. - eauto. - auto. - apply incl_refl. - apply int_callee_save_norepet. - eauto. - eauto. - intros [rs1 [m1 [A [B [C [D [E F]]]]]]]. - exploit (save_callee_save_regs_correct - fe_num_float_callee_save - index_float_callee_save - FI_saved_float Tany64 - j cs fb sp float_callee_save_regs ls). - intros. apply index_float_callee_save_inj; auto. - intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption. - simpl; auto. - intros; congruence. - intros; simpl. destruct idx; auto. congruence. - intros. apply float_callee_save_type. auto. - eauto. - auto. - apply incl_refl. - apply float_callee_save_norepet. - eexact E. - eexact F. - intros [rs2 [m2 [P [Q [R [S [T U]]]]]]]. - exists rs2; 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. - -(** 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)) -> - (forall ofs k p, Mem.perm m sp ofs k p -> 0 <= ofs < f.(Linear.fn_stacksize)) -> - forall m1 m2, stores_in_frame sp' m1 m2 -> Mem.inject j m m1 -> Mem.inject j m m2. -Proof. - induction 3; intros. - auto. - apply IHstores_in_frame. - intros. eapply Mem.store_outside_inject; eauto. - intros. exploit H; eauto. intros [A B]; subst. - exploit H0; eauto. omega. -Qed. - -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 k p sp m m', stores_in_frame sp m m' -> Mem.perm m b ofs k p -> Mem.perm m' b ofs k p. -Proof. - induction 1; intros. auto. apply IHstores_in_frame. eauto with mem. -Qed. - -Lemma stores_in_frame_contents: - forall chunk b ofs sp, Plt 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. apply Plt_ne; auto. -Qed. - -Lemma undef_regs_type: +Remark undef_regs_type: forall ty l rl ls, Val.has_type (ls l) ty -> Val.has_type (LTL.undef_regs rl ls l) ty. Proof. @@ -1496,21 +1018,60 @@ Proof. destruct (Loc.diff_dec (R a) l); auto. red; auto. Qed. +Lemma save_callee_save_correct: + forall j ls ls0 rs sp cs fb k m P, + m |= range sp fe.(fe_ofs_callee_save) (size_callee_save_area b fe.(fe_ofs_callee_save)) ** P -> + (forall r, Val.has_type (ls (R r)) (mreg_type r)) -> + agree_callee_save ls ls0 -> + agree_regs j ls rs -> + let ls1 := LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) in + let rs1 := undef_regs destroyed_at_function_entry rs in + exists rs', exists m', + star step tge + (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs1 m) + E0 (State cs fb (Vptr sp Int.zero) k rs' m') + /\ m' |= contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0 ** P + /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p) + /\ agree_regs j ls1 rs'. +Proof. + intros until P; intros SEP TY AGCS AG; intros ls1 rs1. + exploit (save_callee_save_rec_correct j cs fb sp ls1). +- intros. unfold ls1. apply LTL_undef_regs_same. eapply destroyed_by_setstack_function_entry; eauto. +- intros. unfold ls1. apply undef_regs_type. apply TY. +- exact b.(used_callee_save_prop). +- eexact SEP. +- instantiate (1 := rs1). apply agree_regs_undef_regs. apply agree_regs_call_regs. auto. +- clear SEP. intros (rs' & m' & EXEC & SEP & PERMS & AG'). + exists rs', m'. + split. eexact EXEC. + split. rewrite (contains_callee_saves_exten j sp ls0 ls1). exact SEP. + intros. apply b.(used_callee_save_prop) in H. + unfold ls1. rewrite LTL_undef_regs_others. unfold call_regs. + apply AGCS; auto. + red; intros. + assert (existsb is_callee_save destroyed_at_function_entry = false) + by (apply destroyed_at_function_entry_caller_save). + assert (existsb is_callee_save destroyed_at_function_entry = true). + { apply existsb_exists. exists r; auto. } + congruence. + split. exact PERMS. exact AG'. +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 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k, + forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k P, agree_regs j ls rs -> agree_callee_save ls ls0 -> (forall r, Val.has_type (ls (R r)) (mreg_type r)) -> ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) -> rs1 = undef_regs destroyed_at_function_entry rs -> - 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 -> + m1' |= minjection j m1 ** globalenv_inject ge j ** P -> exists j', exists rs', 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' @@ -1519,143 +1080,97 @@ Lemma function_prologue_correct: (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) rs1 m4') E0 (State cs fb (Vptr sp' Int.zero) k rs' m5') /\ agree_regs j' ls1 rs' - /\ agree_frame j' ls1 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'. + /\ agree_locs ls1 ls0 + /\ m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P + /\ j' sp = Some(sp', fe.(fe_stack_data)) + /\ inject_incr j j'. Proof. - intros until k; intros AGREGS AGCS WTREGS LS1 RS1 INJ1 ALLOC TYPAR TYRA. + intros until P; intros AGREGS AGCS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP. rewrite unfold_transf_function. unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs. + (* Stack layout info *) +Local Opaque b fe. + generalize (frame_env_range b) (frame_env_aligned b). replace (make_env b) with fe by auto. simpl. + intros LAYOUT1 LAYOUT2. (* 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. - intros; right. - exploit Mem.perm_alloc_inv. eexact ALLOC'. eauto. rewrite dec_eq_true. - generalize size_no_overflow. omega. - 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 8. - 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. + destruct (Mem.alloc m1' 0 (fe_size fe)) as [m2' sp'] eqn:ALLOC'. + exploit alloc_parallel_rule_2. + eexact SEP. eexact ALLOC. eexact ALLOC'. + instantiate (1 := fe_stack_data fe). tauto. + reflexivity. + instantiate (1 := fe_stack_data fe + bound_stack_data b). rewrite Z.max_comm. reflexivity. + generalize (bound_stack_data_pos b) size_no_overflow; omega. + tauto. + tauto. + clear SEP. intros (j' & SEP & INCR & SAME). + (* Remember the freeable permissions using a mconj *) + assert (SEPCONJ: + m2' |= mconj (range sp' 0 (fe_stack_data fe) ** range sp' (fe_stack_data fe + bound_stack_data b) (fe_size fe)) + (range sp' 0 (fe_stack_data fe) ** range sp' (fe_stack_data fe + bound_stack_data b) (fe_size fe)) + ** minjection j' m2 ** globalenv_inject ge j' ** P). + { apply mconj_intro; rewrite sep_assoc; assumption. } + (* Dividing up the frame *) + apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto. (* 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]. + rewrite sep_swap3 in SEP. + apply (range_contains Mint32) in SEP; [|tauto]. + exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tint). + eexact SEP. apply Val.load_result_same; auto. + clear SEP; intros (m3' & STORE_PARENT & SEP). + rewrite sep_swap3 in SEP. + (* Store of return address *) + rewrite sep_swap4 in SEP. + apply (range_contains Mint32) in SEP; [|tauto]. + exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tint). + eexact SEP. apply Val.load_result_same; auto. + clear SEP; intros (m4' & STORE_RETADDR & SEP). + rewrite sep_swap4 in SEP. (* Saving callee-save registers *) - assert (PERM4: frame_perm_freeable m4' sp'). - red; intros. eauto with mem. - exploit save_callee_save_correct. - instantiate (1 := rs1). instantiate (1 := call_regs ls). instantiate (1 := j'). - subst rs1. apply agree_regs_undef_regs. - apply agree_regs_call_regs. eapply agree_regs_inject_incr; eauto. - intros. apply undef_regs_type. simpl. apply WTREGS. - eexact PERM4. - rewrite <- LS1. - intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]]. - (* 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 (eq_block b0 sp). - subst b0. rewrite MAP1 in H; inv H; auto. - rewrite MAP2 in H; auto. - assert (Mem.valid_block m1' sp'). eapply Mem.valid_block_inject_2; eauto. - assert (~Mem.valid_block m1' sp') by eauto with mem. - contradiction. - (* Conclusions *) - exists j'; exists rs'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'. + rewrite sep_swap5 in SEP. + exploit (save_callee_save_correct j' ls ls0 rs); eauto. + apply agree_regs_inject_incr with j; auto. + replace (LTL.undef_regs destroyed_at_function_entry (call_regs ls)) with ls1 by auto. + replace (undef_regs destroyed_at_function_entry rs) with rs1 by auto. + clear SEP; intros (rs2 & m5' & SAVE_CS & SEP & PERMS & AGREGS'). + rewrite sep_swap5 in SEP. + (* Materializing the Local and Outgoing locations *) + exploit (initial_locations j'). eexact SEP. tauto. + instantiate (1 := Local). instantiate (1 := ls1). + intros; rewrite LS1. rewrite LTL_undef_regs_slot. reflexivity. + clear SEP; intros SEP. + rewrite sep_swap in SEP. + exploit (initial_locations j'). eexact SEP. tauto. + instantiate (1 := Outgoing). instantiate (1 := ls1). + intros; rewrite LS1. rewrite LTL_undef_regs_slot. reflexivity. + clear SEP; intros SEP. + rewrite sep_swap in SEP. + (* Now we frame this *) + assert (SEPFINAL: m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P). + { eapply frame_mconj. eexact SEPCONJ. + unfold frame_contents_1; rewrite ! sep_assoc. exact SEP. + assert (forall ofs k p, Mem.perm m2' sp' ofs k p -> Mem.perm m5' sp' ofs k p). + { intros. apply PERMS. + unfold store_stack in STORE_PARENT, STORE_RETADDR. + simpl in STORE_PARENT, STORE_RETADDR. + eauto using Mem.perm_store_1. } + eapply sep_preserved. eapply sep_proj1. eapply mconj_proj2. eexact SEPCONJ. + intros; apply range_preserved with m2'; auto. + intros; apply range_preserved with m2'; auto. + } + clear SEP SEPCONJ. +(* Conclusions *) + exists j', rs2, m2', sp', m3', m4', 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. auto. - (* agree frame *) - split. constructor; intros. - (* unused regs *) - assert (~In r destroyed_at_call). - red; intros; elim H; apply caller_save_reg_within_bounds; auto. - rewrite LS1. rewrite LTL_undef_regs_others. unfold call_regs. - apply AGCS; auto. red; intros; elim H0. - apply destroyed_at_function_entry_caller_save; auto. - (* locals *) - rewrite LS1. rewrite LTL_undef_regs_slot. unfold call_regs. - apply index_contains_inj_undef; auto with stacking. - (* outgoing *) - rewrite LS1. rewrite LTL_undef_regs_slot. unfold call_regs. - apply index_contains_inj_undef; auto with stacking. - (* incoming *) - rewrite LS1. rewrite LTL_undef_regs_slot. 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 *) - assert (~In r destroyed_at_call). - red; intros. eapply int_callee_save_not_destroyed; eauto. - exploit ICS; eauto. rewrite LS1. rewrite LTL_undef_regs_others. unfold call_regs. - rewrite AGCS; auto. - red; intros; elim H1. apply destroyed_at_function_entry_caller_save; auto. - (* float callee save *) - assert (~In r destroyed_at_call). - red; intros. eapply float_callee_save_not_destroyed; eauto. - exploit FCS; eauto. rewrite LS1. rewrite LTL_undef_regs_others. unfold call_regs. - rewrite AGCS; auto. - red; intros; elim H1. apply destroyed_at_function_entry_caller_save; 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 *) - exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto. - (* perms *) - auto. - (* incr *) - split. auto. - (* separated *) - split. eapply inject_alloc_separated; eauto with mem. - (* inject *) - split. eapply stores_in_frame_inject; eauto. - intros. exploit Mem.perm_alloc_inv. eexact ALLOC. eauto. rewrite dec_eq_true. auto. - (* stores in frame *) - auto. + split. exact STORE_PARENT. + split. exact STORE_RETADDR. + split. eexact SAVE_CS. + split. exact AGREGS'. + split. rewrite LS1. apply agree_locs_undef_locs; [|reflexivity]. + constructor; intros. unfold call_regs. apply AGCS. + unfold mreg_within_bounds in H; tauto. + unfold call_regs. apply AGCS. auto. + split. exact SEPFINAL. + split. exact SAME. exact INCR. Qed. (** The following lemmas show the correctness of the register reloading @@ -1665,11 +1180,6 @@ Qed. Section RESTORE_CALLEE_SAVE. -Variable bound: frame_env -> Z. -Variable number: mreg -> Z. -Variable mkindex: Z -> frame_index. -Variable ty: typ. -Variable csregs: list mreg. Variable j: meminj. Variable cs: list stackframe. Variable fb: block. @@ -1677,133 +1187,80 @@ 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_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 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 l rs k, - incl l csregs -> - list_norepet l -> +Lemma restore_callee_save_rec_correct: + forall l ofs rs k, + m |= contains_callee_saves j sp ofs l ls0 -> agree_unused ls0 rs -> + (forall r, In r l -> mreg_within_bounds b r) -> exists rs', star step tge - (State cs fb (Vptr sp Int.zero) - (restore_callee_save_regs bound number mkindex ty fe l k) rs m) + (State cs fb (Vptr sp Int.zero) (restore_callee_save_rec l ofs k) rs m) E0 (State cs fb (Vptr sp Int.zero) k rs' m) /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r l) -> rs' r = rs r) /\ agree_unused ls0 rs'. Proof. - induction l; intros; simpl restore_callee_save_regs. - (* base case *) - exists rs. intuition. apply star_refl. - (* inductive case *) - 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)). - 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. - auto. - (* no load takes place *) - 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. - auto. + induction l as [ | r l]; simpl; intros. +- (* base case *) + exists rs. intuition auto. apply star_refl. +- (* inductive case *) + set (ty := mreg_type r) in *. + set (sz := AST.typesize ty) in *. + set (ofs1 := align ofs sz). + assert (SZPOS: sz > 0) by (apply AST.typesize_pos). + assert (OFSLE: ofs <= ofs1) by (apply align_le; auto). + assert (BOUND: mreg_within_bounds b r) by eauto. + exploit contains_get_stack. + eapply sep_proj1; eassumption. + intros (v & LOAD & SPEC). + exploit (IHl (ofs1 + sz) (rs#r <- v)). + eapply sep_proj2; eassumption. + red; intros. rewrite Regmap.gso. auto. intuition congruence. + eauto. + intros (rs' & A & B & C & D). + exists rs'. + split. eapply star_step; eauto. + econstructor. exact LOAD. traceEq. + split. intros. + destruct (In_dec mreg_eq r0 l). auto. + assert (r = r0) by tauto. subst r0. + rewrite C by auto. rewrite Regmap.gss. exact SPEC. + split. intros. + rewrite C by tauto. apply Regmap.gso. intuition auto. + exact D. Qed. End RESTORE_CALLEE_SAVE. Lemma restore_callee_save_correct: - 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 -> + forall m j sp ls ls0 pa ra P rs k cs fb, + m |= frame_contents j sp ls ls0 pa ra ** P -> agree_unused j ls0 rs -> exists rs', 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 rs' m') + (State cs fb (Vptr sp Int.zero) (restore_callee_save fe k) rs m) + E0 (State cs fb (Vptr sp Int.zero) k rs' m) /\ (forall r, - In r int_callee_save_regs \/ In r float_callee_save_regs -> - Val.inject j (ls0 (R r)) (rs' r)) + is_callee_save r = true -> 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). + is_callee_save r = false -> rs' r = rs r). Proof. intros. - exploit (restore_callee_save_regs_correct - fe_num_int_callee_save - index_int_callee_save - FI_saved_int - Tany32 - int_callee_save_regs - j cs fb sp' ls0 m'); auto. - intros. unfold mreg_within_bounds. split; intros. - split; auto. destruct (zlt (index_float_callee_save r) 0). - generalize (bound_float_callee_save_pos b). omega. - eelim int_float_callee_save_disjoint. eauto. - eapply index_float_callee_save_pos2. eauto. auto. - destruct H2; auto. - 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 - Tany64 - float_callee_save_regs - j cs fb sp' ls0 m'); auto. - intros. unfold mreg_within_bounds. split; intros. - split; auto. destruct (zlt (index_int_callee_save r) 0). - generalize (bound_int_callee_save_pos b). omega. - eelim int_float_callee_save_disjoint. - eapply index_int_callee_save_pos2. eauto. eauto. auto. - destruct H2; auto. - 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. + unfold frame_contents, frame_contents_1 in H. + apply mconj_proj1 in H. rewrite ! sep_assoc in H. apply sep_pick5 in H. + exploit restore_callee_save_rec_correct; eauto. + intros; unfold mreg_within_bounds; auto. + intros (rs' & A & B & C & D). + exists rs'. + split. eexact A. + split; intros. + destruct (In_dec mreg_eq r (used_callee_save b)). + apply B; auto. + rewrite C by auto. apply H0. unfold mreg_within_bounds; tauto. + apply C. red; intros. apply (used_callee_save_prop b) in H2. congruence. Qed. (** As a corollary, we obtain the following correctness result for @@ -1812,10 +1269,11 @@ Qed. of the frame). *) Lemma function_epilogue_correct: - forall j ls ls0 m sp m' sp' pa ra cs fb rs k m1, + forall m' j sp' ls ls0 pa ra P m rs sp m1 k cs fb, + m' |= frame_contents j sp' ls ls0 pa ra ** minjection j m ** P -> agree_regs j ls rs -> - agree_frame j ls ls0 m sp m' sp' pa ra -> - Mem.inject j m m' -> + agree_locs ls ls0 -> + j sp = Some(sp', fe.(fe_stack_data)) -> 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 @@ -1826,268 +1284,138 @@ Lemma function_epilogue_correct: 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 - /\ 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. - eapply agree_bounds. eauto. eapply Mem.perm_max. eauto. - (* can execute epilogue *) - exploit restore_callee_save_correct; eauto. - instantiate (1 := rs). red; intros. - rewrite <- (agree_unused_reg _ _ _ _ _ _ _ _ _ H0). auto. auto. - 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 mreg_eq r destroyed_at_call). - rewrite C; auto. - apply B. intuition. - split. apply agree_callee_save_return_regs. - auto. + /\ m1' |= minjection j m1 ** P. +Proof. + intros until fb; intros SEP AGR AGL INJ FREE. + (* Can free *) + exploit free_parallel_rule. + rewrite <- sep_assoc. eapply mconj_proj2. eexact SEP. + eexact FREE. + eexact INJ. + auto. rewrite Z.max_comm; reflexivity. + intros (m1' & FREE' & SEP'). + (* Reloading the callee-save registers *) + exploit restore_callee_save_correct. + eexact SEP. + instantiate (1 := rs). + red; intros. destruct AGL. rewrite <- agree_unused_reg0 by auto. apply AGR. + intros (rs' & LOAD_CS & CS & NCS). + (* Reloading the back link and return address *) + unfold frame_contents in SEP; apply mconj_proj1 in SEP. + unfold frame_contents_1 in SEP; rewrite ! sep_assoc in SEP. + exploit (hasvalue_get_stack Tint). eapply sep_pick3; eexact SEP. intros LOAD_LINK. + exploit (hasvalue_get_stack Tint). eapply sep_pick4; eexact SEP. intros LOAD_RETADDR. + clear SEP. + (* Conclusions *) + rewrite unfold_transf_function; simpl. + exists rs', m1'. + split. assumption. + split. assumption. + split. assumption. + split. eassumption. + split. red; unfold return_regs; intros. + destruct (is_callee_save r) eqn:C. + apply CS; auto. + rewrite NCS by auto. apply AGR. + split. red; unfold return_regs; intros. + destruct l; auto. rewrite H; auto. + assumption. Qed. End FRAME_PROPERTIES. -(** * Call stack invariant *) +(** * Call stack invariants *) -Inductive match_globalenvs (j: meminj) (bound: block) : Prop := - | match_globalenvs_intro - (DOMAIN: forall b, Plt b bound -> j b = Some(b, 0)) - (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> Plt b2 bound -> b1 = b2) - (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> Plt b bound) - (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> Plt b bound) - (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> Plt b bound). +(** This is the memory assertion that captures the contents of the stack frames + mentioned in the call stacks. *) + +Fixpoint stack_contents (j: meminj) (cs: list Linear.stackframe) (cs': list Mach.stackframe) : massert := + match cs, cs' with + | nil, nil => pure True + | Linear.Stackframe f _ ls c :: cs, Mach.Stackframe fb (Vptr sp' _) ra c' :: cs' => + frame_contents f j sp' ls (parent_locset cs) (parent_sp cs') (parent_ra cs') + ** stack_contents j cs cs' + | _, _ => pure False + end. -Inductive match_stacks (j: meminj) (m m': mem): - list Linear.stackframe -> list stackframe -> signature -> block -> block -> Prop := - | match_stacks_empty: forall sg hi bound bound', - Ple hi bound -> Ple hi bound' -> match_globalenvs j hi -> +(** [match_stacks] captures additional properties (not related to memory) + of the Linear and Mach call stacks. *) + +Inductive match_stacks (j: meminj): + list Linear.stackframe -> list stackframe -> signature -> Prop := + | match_stacks_empty: forall sg, 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 + match_stacks j nil nil sg + | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg trf (TAIL: is_tail c (Linear.fn_code 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') + (INJ: j sp = Some(sp', (fe_stack_data (make_env (function_bounds f))))) (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')) + (AGL: agree_locs f ls (parent_locset cs)) (ARGS: forall ofs ty, In (S Outgoing ofs ty) (loc_arguments sg) -> slot_within_bounds (function_bounds f) Outgoing ofs ty) - (STK: match_stacks j m m' cs cs' (Linear.fn_sig f) sp sp') - (BELOW: Plt sp bound) - (BELOW': Plt sp' bound'), - match_stacks j m m' + (STK: match_stacks j cs cs' (Linear.fn_sig f)), + match_stacks j (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs) (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs') - sg bound bound'. + sg. -(** Invariance with respect to change of bounds. *) +(** Invariance with respect to change of memory injection. *) -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', - Ple bound xbound -> Ple bound' xbound' -> - match_stacks j m1 m' cs cs' sg xbound xbound'. +Lemma stack_contents_change_meminj: + forall m j j', inject_incr j j' -> + forall cs cs' P, + m |= stack_contents j cs cs' ** P -> + m |= stack_contents j' cs cs' ** P. Proof. - induction 1; intros. - apply match_stacks_empty with hi; auto. apply Ple_trans with bound; eauto. apply Ple_trans with bound'; eauto. - econstructor; eauto. eapply Plt_le_trans; eauto. eapply Plt_le_trans; eauto. +Local Opaque sepconj. + induction cs as [ | [] cs]; destruct cs' as [ | [] cs']; simpl; intros; auto. + destruct sp0; auto. + rewrite sep_assoc in *. + apply frame_contents_incr with (j := j); auto. + rewrite sep_swap. apply IHcs. rewrite sep_swap. assumption. 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, Plt b bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> - (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - 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. apply Plt_trans with sp; auto. - intros. apply H1. apply Plt_trans with sp; auto. auto. -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, Plt b bound' -> Mem.valid_block m1' b -> Mem.valid_block m2' b) -> - (forall b ofs k p, Plt b bound' -> Mem.perm m1' b ofs k p -> Mem.perm m2' b ofs k p) -> - (forall chunk b ofs v, Plt 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. apply Plt_trans with sp'; auto. - intros; apply H1; auto. apply Plt_trans with sp'; auto. - intros; apply H2; auto. apply Plt_trans with sp'; auto. -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, Plt b bound -> Mem.valid_block m1 b -> Mem.valid_block m2 b) -> - (forall b ofs p, Plt b bound -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p) -> - (forall b, Plt 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. apply Plt_trans with sp; auto. - intros; apply H1. apply Plt_trans with sp; auto. auto. - intros; apply H2; auto. apply Plt_trans with sp'; auto. - 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' -> - Ple 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. - apply Plt_le_trans with hi. auto. apply Ple_trans with bound'; auto. - econstructor; eauto. - eapply agree_frame_inject_incr; eauto. red. eapply Plt_le_trans; eauto. - apply IHmatch_stacks. apply Ple_trans with bound'; auto. apply Plt_Ple; auto. -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'. + forall j j', inject_incr j j' -> + forall cs cs' sg, + match_stacks j cs cs' sg -> + match_stacks j' cs cs' sg. Proof. - intros until m1'. intros MINJ VINJ STORE1 STORE2. - induction 1. - econstructor; eauto. - econstructor; eauto. - eapply agree_frame_parallel_stores; eauto. + induction 2; intros. +- constructor; auto. +- econstructor; 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' -> - Ple bound (Mem.nextblock m1) -> Ple 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_max_perm; eauto. red. eapply Plt_le_trans; eauto. - intros; eapply external_call_valid_block; eauto. -Qed. - -(** Invariance with respect to change of signature *) +(** 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' -> + forall sg1 j cs cs' sg, + match_stacks j cs cs' sg -> tailcall_possible sg1 -> - match_stacks j m m' cs cs' sg1 bound bound'. + match_stacks j cs cs' sg1. 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_type_sp: - forall j m m' cs cs' sg bound bound', - match_stacks j m m' cs cs' sg bound bound' -> + forall j cs cs' sg, + match_stacks j cs cs' sg -> 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' -> + forall j cs cs' sg, + match_stacks j cs cs' sg -> Val.has_type (parent_ra cs') Tint. Proof. induction 1; simpl; auto. @@ -2099,41 +1427,18 @@ Qed. Section LABELS. -Remark find_label_fold_right: - forall (A: Type) (fn: A -> Mach.code -> Mach.code) lbl, - (forall x k, Mach.find_label lbl (fn x k) = Mach.find_label lbl k) -> forall (args: list A) k, - Mach.find_label lbl (List.fold_right fn k args) = Mach.find_label lbl k. -Proof. - induction args; simpl. auto. - intros. rewrite H. auto. -Qed. - Remark find_label_save_callee_save: - forall fe lbl k, - Mach.find_label lbl (save_callee_save fe k) = Mach.find_label lbl k. + forall lbl l ofs k, + Mach.find_label lbl (save_callee_save_rec l ofs k) = Mach.find_label lbl k. Proof. - intros. unfold save_callee_save, save_callee_save_int, save_callee_save_float, save_callee_save_regs. - repeat rewrite find_label_fold_right. reflexivity. - intros. unfold save_callee_save_reg. - case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); - intro; reflexivity. - intros. unfold save_callee_save_reg. - case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); - intro; reflexivity. + induction l; simpl; auto. Qed. Remark find_label_restore_callee_save: - forall fe lbl k, - Mach.find_label lbl (restore_callee_save fe k) = Mach.find_label lbl k. + forall lbl l ofs k, + Mach.find_label lbl (restore_callee_save_rec l ofs k) = Mach.find_label lbl k. Proof. - intros. unfold restore_callee_save, restore_callee_save_int, restore_callee_save_float, restore_callee_save_regs. - repeat rewrite find_label_fold_right. reflexivity. - intros. unfold restore_callee_save_reg. - case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); - intro; reflexivity. - intros. unfold restore_callee_save_reg. - case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); - intro; reflexivity. + induction l; simpl; auto. Qed. Lemma transl_code_eq: @@ -2148,14 +1453,14 @@ Lemma find_label_transl_code: option_map (transl_code fe) (Linear.find_label lbl c). Proof. induction c; simpl; intros. - auto. - rewrite transl_code_eq. +- auto. +- rewrite transl_code_eq. destruct a; unfold transl_instr; auto. destruct s; simpl; auto. destruct s; simpl; auto. - rewrite find_label_restore_callee_save. auto. - simpl. case (peq lbl l); intro. reflexivity. auto. - rewrite find_label_restore_callee_save. auto. + unfold restore_callee_save. rewrite find_label_restore_callee_save. auto. + simpl. destruct (peq lbl l). reflexivity. auto. + unfold restore_callee_save. rewrite find_label_restore_callee_save. auto. Qed. Lemma transl_find_label: @@ -2166,7 +1471,7 @@ Lemma transl_find_label: Some (transl_code (make_env (function_bounds f)) c). Proof. intros. rewrite (unfold_transf_function _ _ H). simpl. - unfold transl_body. rewrite find_label_save_callee_save. + unfold transl_body. unfold save_callee_save. rewrite find_label_save_callee_save. rewrite find_label_transl_code. rewrite H0. reflexivity. Qed. @@ -2187,38 +1492,20 @@ 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). + forall l ofs k, + is_tail k (save_callee_save_rec l ofs k). Proof. - induction csl; intros; simpl. auto with coqlib. - unfold restore_callee_save_reg. destruct (zlt (number a) (bound fe)). - constructor; auto. auto. + induction l; intros; simpl. auto with coqlib. + constructor; auto. Qed. Lemma is_tail_restore_callee_save: - forall fe k, - is_tail k (restore_callee_save fe k). + forall l ofs k, + is_tail k (restore_callee_save_rec l ofs 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. + induction l; intros; simpl. auto with coqlib. + constructor; auto. Qed. Lemma is_tail_transl_instr: @@ -2228,8 +1515,8 @@ 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. + unfold restore_callee_save. eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib. + unfold restore_callee_save. eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib. Qed. Lemma is_tail_transl_code: @@ -2247,7 +1534,8 @@ Lemma is_tail_transf_function: 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. + unfold transl_body, save_callee_save. + eapply is_tail_trans. 2: apply is_tail_save_callee_save. apply is_tail_transl_code; auto. Qed. @@ -2287,25 +1575,24 @@ Proof. Qed. Lemma find_function_translated: - forall j ls rs m m' cs cs' sg bound bound' ros f, + forall j ls rs m ros f, agree_regs j ls rs -> - match_stacks j m m' cs cs' sg bound bound' -> + m |= globalenv_inject ge j -> Linear.find_function ge ros ls = Some f -> exists bf, exists tf, find_function_ptr tge ros rs = Some bf /\ Genv.find_funct_ptr tge bf = Some tf /\ transf_fundef f = OK tf. Proof. - intros until f; intros AG MS FF. - exploit match_stacks_globalenvs; eauto. intros [hi MG]. + intros until f; intros AG [bound [_ []]] FF. destruct ros; simpl in FF. - exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ 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. - inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. - destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate. + rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. +- destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. rewrite symbols_preserved. auto. @@ -2316,16 +1603,17 @@ Qed. Section EXTERNAL_ARGUMENTS. Variable j: meminj. -Variables m m': mem. Variable cs: list Linear.stackframe. Variable cs': list stackframe. Variable sg: signature. Variables bound bound': block. -Hypothesis MS: match_stacks j m m' cs cs' sg bound bound'. +Hypothesis MS: match_stacks j cs cs' sg. Variable ls: locset. Variable rs: regset. Hypothesis AGR: agree_regs j ls rs. Hypothesis AGCS: agree_callee_save ls (parent_locset cs). +Variable m': mem. +Hypothesis SEP: m' |= stack_contents j cs cs'. Lemma transl_external_argument: forall l, @@ -2333,24 +1621,20 @@ Lemma transl_external_argument: 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. + assert (loc_argument_acceptable l) by (apply loc_arguments_acceptable with sg; auto). destruct l; red in H0. - exists (rs r); split. constructor. auto. - destruct sl; try contradiction. +- exists (rs r); split. constructor. auto. +- destruct sl; try contradiction. inv MS. - elim (H4 _ H). - unfold parent_sp. ++ elim (H1 _ H). ++ simpl in SEP. unfold parent_sp. assert (slot_valid f Outgoing pos ty = true). - exploit loc_arguments_acceptable; eauto. intros [A B]. - unfold slot_valid. unfold proj_sumbool. rewrite zle_true by omega. - destruct ty; auto; congruence. - assert (slot_within_bounds (function_bounds f) Outgoing pos ty). - eauto. - exploit agree_outgoing; eauto. intros [v [A B]]. + { destruct H0. unfold slot_valid, proj_sumbool. + rewrite zle_true by omega. rewrite pred_dec_true by auto. reflexivity. } + assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto. + exploit frame_get_outgoing; eauto. intros (v & A & B). exists v; split. - constructor. - eapply index_contains_load_stack with (idx := FI_arg pos ty); eauto. - red in AGCS. rewrite AGCS; auto. + constructor. exact A. red in AGCS. rewrite AGCS; auto. Qed. Lemma transl_external_arguments_rec: @@ -2393,10 +1677,9 @@ Variables ls ls0: locset. Variable rs: regset. Variables sp sp': block. Variables parent retaddr: val. +Hypothesis INJ: j sp = Some(sp', fe.(fe_stack_data)). Hypothesis AGR: agree_regs j ls rs. -Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr. -Hypothesis MINJ: Mem.inject j m m'. -Hypothesis GINJ: meminj_preserves_globals ge j. +Hypothesis SEP: m' |= frame_contents f j sp' ls ls0 parent retaddr ** minjection j m ** globalenv_inject ge j. Lemma transl_builtin_arg_correct: forall a v, @@ -2407,35 +1690,33 @@ Lemma transl_builtin_arg_correct: eval_builtin_arg ge rs (Vptr sp' Int.zero) m' (transl_builtin_arg fe a) v' /\ Val.inject j v v'. Proof. -Local Opaque fe offset_of_index. + assert (SYMB: forall id ofs, Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). + { assert (G: meminj_preserves_globals ge j). + { eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eexact SEP. } + intros; unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) eqn:FS; auto. + destruct G. econstructor. eauto. rewrite Int.add_zero; auto. } +Local Opaque fe. induction 1; simpl; intros VALID BOUNDS. - assert (loc_valid f x = true) by auto. destruct x as [r | [] ofs ty]; try discriminate. + exists (rs r); auto with barg. - + exploit agree_locals; eauto. intros [v [A B]]. inv A. - exists v; split; auto. constructor. simpl. rewrite Int.add_zero_l. -Local Transparent fe. - unfold fe, b. erewrite offset_of_index_no_overflow by eauto. exact H1. + + exploit frame_get_local; eauto. intros (v & A & B). + exists v; split; auto. constructor; auto. - econstructor; eauto with barg. - econstructor; eauto with barg. - econstructor; eauto with barg. - econstructor; eauto with barg. -- simpl in H. exploit Mem.load_inject; eauto. eapply agree_inj; eauto. - intros (v' & A & B). exists v'; split; auto. constructor. - unfold Mem.loadv, Val.add. rewrite <- Int.add_assoc. - unfold fe, b; erewrite shifted_stack_offset_no_overflow; eauto. - eapply agree_bounds; eauto. eapply Mem.valid_access_perm. eapply Mem.load_valid_access; eauto. -- econstructor; split; eauto with barg. - unfold Val.add. rewrite ! Int.add_zero_l. econstructor. eapply agree_inj; eauto. auto. -- assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). - { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. - destruct (Genv.find_symbol ge id) eqn:FS; auto. - econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. } - exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with barg. +- set (ofs' := Int.add ofs (Int.repr (fe_stack_data fe))). + apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto. + instantiate (1 := Val.add (Vptr sp' Int.zero) (Vint ofs')). + simpl. rewrite ! Int.add_zero_l. econstructor; eauto. + intros (v' & A & B). exists v'; split; auto. constructor; auto. - econstructor; split; eauto with barg. - unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. - destruct (Genv.find_symbol ge id) eqn:FS; auto. - econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. + unfold Val.add. rewrite ! Int.add_zero_l. econstructor; eauto. +- apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto. + intros (v' & A & B). exists v'; auto with barg. +- econstructor; split; eauto with barg. - destruct IHeval_builtin_arg1 as (v1 & A1 & B1); auto using in_or_app. destruct IHeval_builtin_arg2 as (v2 & A2 & B2); auto using in_or_app. exists (Val.longofwords v1 v2); split; auto with barg. @@ -2472,44 +1753,56 @@ End BUILTIN_ARGUMENTS. >> Matching between source and target states is defined by [match_states] below. It implies: +- Satisfaction of the separation logic assertions that describe the contents + of memory. This is a separating conjunction of facts about: +-- the current stack frame +-- the frames in the call stack +-- the injection from the Linear memory state into the Mach memory state +-- the preservation of the global environment. - 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] and the contents of - the memory area corresponding to the stack frame. + and on the Mach side the register set [rs]. - 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_states: Linear.state -> Mach.state -> Prop := | match_states_intro: 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') + (STACKS: match_stacks j cs cs' f.(Linear.fn_sig)) (TRANSL: transf_function f = OK tf) (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf)) (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)), + (AGLOCS: agree_locs f ls (parent_locset cs)) + (INJSP: j sp = Some(sp', fe_stack_data (make_env (function_bounds f)))) + (TAIL: is_tail c (Linear.fn_code f)) + (SEP: m' |= frame_contents f j sp' ls (parent_locset cs) (parent_sp cs') (parent_ra cs') + ** stack_contents j cs cs' + ** minjection j m + ** globalenv_inject ge j), match_states (Linear.State cs f (Vptr sp Int.zero) c ls m) - (Mach.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') + (Mach.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') | match_states_call: forall cs f ls m cs' 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')) + (STACKS: match_stacks j cs cs' (Linear.funsig f)) (TRANSL: transf_fundef f = OK tf) (FIND: Genv.find_funct_ptr tge fb = Some tf) (AGREGS: agree_regs j ls rs) - (AGLOCS: agree_callee_save ls (parent_locset cs)), + (AGLOCS: agree_callee_save ls (parent_locset cs)) + (SEP: m' |= stack_contents j cs cs' + ** minjection j m + ** globalenv_inject ge j), match_states (Linear.Callstate cs f ls m) - (Mach.Callstate cs' fb rs m') + (Mach.Callstate cs' fb rs m') | match_states_return: forall cs ls m cs' rs m' j sg - (MINJ: Mem.inject j m m') - (STACKS: match_stacks j m m' cs cs' sg (Mem.nextblock m) (Mem.nextblock m')) + (STACKS: match_stacks j cs cs' sg) (AGREGS: agree_regs j ls rs) - (AGLOCS: agree_callee_save ls (parent_locset cs)), + (AGLOCS: agree_callee_save ls (parent_locset cs)) + (SEP: m' |= stack_contents j cs cs' + ** minjection j m + ** globalenv_inject ge j), match_states (Linear.Returnstate cs ls m) (Mach.Returnstate cs' rs m'). @@ -2518,13 +1811,6 @@ Theorem transf_step_correct: forall (WTS: wt_state s1) s1' (MS: match_states s1 s1'), exists s2', plus step tge s1' t s2' /\ match_states s2 s2'. Proof. -(* - assert (USEWTF: forall f i c, - wt_function f = true -> is_tail (i :: c) (Linear.fn_code f) -> - wt_instr f i = true). - intros. unfold wt_function, wt_code in H. rewrite forallb_forall in H. - apply H. eapply is_tail_in; eauto. -*) induction 1; intros; try inv MS; try rewrite transl_code_eq; @@ -2533,98 +1819,78 @@ Proof. unfold transl_instr. - (* Lgetstack *) - destruct BOUND. + destruct BOUND as [BOUND1 BOUND2]. exploit wt_state_getstack; eauto. intros SV. unfold destroyed_by_getstack; destruct sl. + (* Lgetstack, local *) - exploit agree_locals; eauto. intros [v [A B]]. + exploit frame_get_local; eauto. intros (v & A & B). econstructor; split. - apply plus_one. apply exec_Mgetstack. - eapply index_contains_load_stack; eauto. + apply plus_one. apply exec_Mgetstack. exact A. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. - apply agree_frame_set_reg; auto. + apply agree_locs_set_reg; auto. + (* Lgetstack, incoming *) unfold slot_valid in SV. InvBooleans. exploit incoming_slot_in_parameters; eauto. intros IN_ARGS. inversion STACKS; clear STACKS. - elim (H6 _ IN_ARGS). - subst bound bound' s cs'. - exploit agree_outgoing. eexact FRM. eapply ARGS; eauto. - exploit loc_arguments_acceptable; eauto. intros [A B]. - unfold slot_valid, proj_sumbool. rewrite zle_true. - destruct ty; reflexivity || congruence. omega. - intros [v [A B]]. + elim (H1 _ IN_ARGS). + subst s cs'. + exploit frame_get_outgoing. + apply sep_proj2 in SEP. simpl in SEP. rewrite sep_assoc in SEP. eexact SEP. + eapply ARGS; eauto. + eapply slot_outgoing_argument_valid; eauto. + intros (v & A & B). econstructor; split. - apply plus_one. eapply exec_Mgetparam; eauto. + 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). eapply TRANSL. eapply agree_link; eauto. - simpl parent_sp. - change (offset_of_index (make_env (function_bounds f)) (FI_arg ofs ty)) - with (offset_of_index (make_env (function_bounds f0)) (FI_arg ofs ty)). - eapply index_contains_load_stack with (idx := FI_arg ofs ty). eauto. eauto. - exploit agree_incoming; eauto. intros EQ; simpl in EQ. + eapply frame_get_parent. eexact SEP. 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 caller_save_reg_within_bounds. - apply temp_for_parent_frame_caller_save. + apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. + erewrite agree_incoming by eauto. exact B. + apply agree_locs_set_reg; auto. apply agree_locs_undef_locs; auto. + (* Lgetstack, outgoing *) - exploit agree_outgoing; eauto. intros [v [A B]]. + exploit frame_get_outgoing; eauto. intros (v & A & B). econstructor; split. - apply plus_one. apply exec_Mgetstack. - eapply index_contains_load_stack; eauto. + apply plus_one. apply exec_Mgetstack. exact A. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. - apply agree_frame_set_reg; auto. + apply agree_locs_set_reg; auto. - (* Lsetstack *) exploit wt_state_setstack; eauto. intros (SV & SW). - set (idx := match sl with - | Local => FI_local ofs ty - | Incoming => FI_link (*dummy*) - | Outgoing => 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 src). intros [m1' STORE]. + set (ofs' := match sl with + | Local => offset_local (make_env (function_bounds f)) ofs + | Incoming => 0 (* dummy *) + | Outgoing => offset_arg ofs + end). + eapply frame_undef_regs with (rl := destroyed_by_setstack ty) in SEP. + assert (A: exists m'', + store_stack m' (Vptr sp' Int.zero) ty (Int.repr ofs') (rs0 src) = Some m'' + /\ m'' |= frame_contents f j sp' (Locmap.set (S sl ofs ty) (rs (R src)) + (LTL.undef_regs (destroyed_by_setstack ty) rs)) + (parent_locset s) (parent_sp cs') (parent_ra cs') + ** stack_contents j s cs' ** minjection j m ** globalenv_inject ge j). + { unfold ofs'; destruct sl; try discriminate. + eapply frame_set_local; eauto. + eapply frame_set_outgoing; eauto. } + clear SEP; destruct A as (m'' & STORE & SEP). econstructor; split. - apply plus_one. destruct sl; simpl in SW. - econstructor. eapply store_stack_succeeds with (idx := idx); eauto. eauto. - discriminate. - econstructor. eapply store_stack_succeeds with (idx := idx); eauto. auto. - econstructor. - eapply Mem.store_outside_inject; eauto. - intros. exploit agree_inj_unique; eauto. intros [EQ1 EQ2]; subst b' delta. - rewrite size_type_chunk in H2. - exploit offset_of_index_disj_stack_data_2; eauto. - exploit agree_bounds. eauto. apply Mem.perm_cur_max. eauto. - omega. - apply match_stacks_change_mach_mem with m'; auto. - eauto with mem. eauto with mem. intros. rewrite <- H1; eapply Mem.load_store_other; eauto. left; apply Plt_ne; auto. - eauto. eauto. - apply agree_regs_set_slot. apply agree_regs_undef_regs; auto. - destruct sl. - + eapply agree_frame_set_local. eapply agree_frame_undef_locs; eauto. - apply destroyed_by_setstack_caller_save. auto. auto. auto. - assumption. - + simpl in SW; discriminate. - + eapply agree_frame_set_outgoing. eapply agree_frame_undef_locs; eauto. - apply destroyed_by_setstack_caller_save. auto. auto. auto. - assumption. - + eauto with coqlib. + apply plus_one. destruct sl; try discriminate. + econstructor. eexact STORE. eauto. + econstructor. eexact STORE. eauto. + econstructor. eauto. eauto. eauto. + apply agree_regs_set_slot. apply agree_regs_undef_regs. auto. + apply agree_locs_set_slot. apply agree_locs_undef_locs. auto. apply destroyed_by_setstack_caller_save. auto. + eauto. eauto with coqlib. eauto. - (* Lop *) 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. + eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. + eapply agree_reglist; eauto. + apply sep_proj2 in SEP. apply sep_proj2 in SEP. apply sep_proj1 in SEP. exact SEP. destruct H0 as [v' [A B]]. econstructor; split. apply plus_one. econstructor. @@ -2633,56 +1899,58 @@ Proof. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. rewrite transl_destroyed_by_op. apply agree_regs_undef_regs; auto. - apply agree_frame_set_reg; auto. apply agree_frame_undef_locs; auto. - apply destroyed_by_op_caller_save. + apply agree_locs_set_reg; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_op_caller_save. + apply frame_set_reg. apply frame_undef_regs. exact SEP. - (* Lload *) 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. + eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. + eapply agree_reglist; eauto. destruct H1 as [a' [A B]]. - exploit Mem.loadv_inject; eauto. intros [v' [C D]]. + exploit loadv_parallel_rule. + apply sep_proj2 in SEP. apply sep_proj2 in SEP. apply sep_proj1 in SEP. eexact SEP. + eauto. 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. eauto. econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. - apply agree_frame_set_reg. apply agree_frame_undef_locs; auto. - apply destroyed_by_load_caller_save. auto. + apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. - (* 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. + eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. + eapply agree_reglist; eauto. destruct H1 as [a' [A B]]. - exploit Mem.storev_mapped_inject; eauto. intros [m1' [C D]]. + rewrite sep_swap3 in SEP. + exploit storev_parallel_rule. eexact SEP. eauto. eauto. apply AGREGS. + clear SEP; intros (m1' & C & SEP). + rewrite sep_swap3 in SEP. econstructor; split. apply plus_one. econstructor. instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. eexact C. eauto. - econstructor. eauto. - eapply match_stacks_parallel_stores. eexact MINJ. eexact B. eauto. eauto. auto. - eauto. eauto. - rewrite transl_destroyed_by_store. - apply agree_regs_undef_regs; auto. - apply agree_frame_undef_locs; auto. - eapply agree_frame_parallel_stores; eauto. - apply destroyed_by_store_caller_save. - eauto with coqlib. + econstructor. eauto. eauto. eauto. + rewrite transl_destroyed_by_store. apply agree_regs_undef_regs; auto. + apply agree_locs_undef_locs. auto. apply destroyed_by_store_caller_save. + auto. eauto with coqlib. + eapply frame_undef_regs; eauto. - (* Lcall *) - exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. + exploit find_function_translated; eauto. + eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. + intros [bf [tf' [A [B C]]]]. exploit is_tail_transf_function; eauto. intros IST. rewrite transl_code_eq in IST. simpl in IST. - exploit return_address_offset_exists. eexact IST. - intros [ra D]. + exploit return_address_offset_exists. eexact IST. intros [ra D]. econstructor; split. apply plus_one. econstructor; eauto. econstructor; eauto. @@ -2691,54 +1959,45 @@ Proof. intros; red. 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. simpl; red; auto. + simpl. rewrite sep_assoc. exact SEP. - (* Ltailcall *) + rewrite (sep_swap (stack_contents j s cs')) in SEP. exploit function_epilogue_correct; eauto. - intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]]. - exploit find_function_translated; eauto. intros [bf [tf' [A [B C]]]]. + clear SEP. intros (rs1 & m1' & P & Q & R & S & T & U & SEP). + rewrite sep_swap in SEP. + exploit find_function_translated; eauto. + eapply sep_proj2. eapply sep_proj2. eexact SEP. + intros [bf [tf' [A [B C]]]]. econstructor; split. eapply plus_right. eexact S. econstructor; eauto. traceEq. econstructor; eauto. 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; apply Plt_ne; auto. - intros. rewrite <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. - eauto with mem. intros. eapply Mem.perm_free_3; eauto. - apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. apply zero_size_arguments_tailcall_possible. eapply wt_state_tailcall; eauto. - (* Lbuiltin *) destruct BOUND as [BND1 BND2]. - exploit transl_builtin_args_correct; eauto. - eapply match_stacks_preserves_globals; eauto. - rewrite <- forallb_forall. eapply wt_state_builtin; eauto. + exploit transl_builtin_args_correct. + eauto. eauto. rewrite sep_swap in SEP; apply sep_proj2 in SEP; eexact SEP. + eauto. rewrite <- forallb_forall. eapply wt_state_builtin; eauto. + exact BND2. intros [vargs' [P Q]]. - exploit external_call_mem_inject; eauto. - eapply match_stacks_preserves_globals; eauto. - intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. + rewrite <- sep_assoc, sep_comm, sep_assoc in SEP. + exploit external_call_parallel_rule; eauto. + clear SEP; intros (j' & res' & m1' & EC & RES & SEP & INCR & ISEP). + rewrite <- sep_assoc, sep_comm, sep_assoc in SEP. econstructor; split. apply plus_one. econstructor; eauto. eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved; eauto. apply senv_preserved. - econstructor; eauto with coqlib. - eapply match_stack_change_extcall; eauto. - apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. - apply Plt_Ple. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. + eapply match_states_intro with (j := j'); eauto with coqlib. + eapply match_stacks_change_meminj; eauto. apply agree_regs_set_res; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto. - eapply agree_frame_inject_incr; eauto. - apply agree_frame_set_res; auto. apply agree_frame_undef_regs; auto. - apply agree_frame_extcall_invariant with m m'0; auto. - eapply external_call_valid_block; eauto. - intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. - eapply external_call_valid_block; eauto. - eapply agree_valid_mach; eauto. + apply agree_locs_set_res; auto. apply agree_locs_undef_regs; auto. + apply frame_set_res. apply frame_undef_regs. apply frame_contents_incr with j; auto. + rewrite sep_swap2. apply stack_contents_change_meminj with j; auto. rewrite sep_swap2. + exact SEP. - (* Llabel *) econstructor; split. @@ -2755,21 +2014,24 @@ Proof. - (* Lcond, true *) econstructor; split. apply plus_one. eapply exec_Mcond_true; eauto. - eapply eval_condition_inject; eauto. eapply agree_reglist; eauto. + eapply eval_condition_inject with (m1 := m). eapply agree_reglist; eauto. apply sep_pick3 in SEP; exact SEP. auto. eapply transl_find_label; eauto. - econstructor. eauto. eauto. eauto. eauto. + econstructor. eauto. eauto. eauto. apply agree_regs_undef_regs; auto. - apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. + apply agree_locs_undef_locs. auto. apply destroyed_by_cond_caller_save. + auto. eapply find_label_tail; eauto. + apply frame_undef_regs; auto. - (* Lcond, false *) econstructor; split. apply plus_one. eapply exec_Mcond_false; eauto. - eapply eval_condition_inject; eauto. eapply agree_reglist; eauto. - econstructor. eauto. eauto. eauto. eauto. + eapply eval_condition_inject with (m1 := m). eapply agree_reglist; eauto. apply sep_pick3 in SEP; exact SEP. auto. + econstructor. eauto. eauto. eauto. apply agree_regs_undef_regs; auto. - apply agree_frame_undef_locs; auto. apply destroyed_by_cond_caller_save. - eauto with coqlib. + apply agree_locs_undef_locs. auto. apply destroyed_by_cond_caller_save. + auto. eauto with coqlib. + apply frame_undef_regs; auto. - (* Ljumptable *) assert (rs0 arg = Vint n). @@ -2777,78 +2039,67 @@ Proof. econstructor; split. apply plus_one; eapply exec_Mjumptable; eauto. apply transl_find_label; eauto. - econstructor. eauto. eauto. eauto. eauto. + econstructor. eauto. eauto. eauto. apply agree_regs_undef_regs; auto. - apply agree_frame_undef_locs; auto. apply destroyed_by_jumptable_caller_save. - eapply find_label_tail; eauto. + apply agree_locs_undef_locs. auto. apply destroyed_by_jumptable_caller_save. + auto. eapply find_label_tail; eauto. + apply frame_undef_regs; auto. - (* Lreturn *) + rewrite (sep_swap (stack_contents j s cs')) in SEP. exploit function_epilogue_correct; eauto. - intros [rs1 [m1' [P [Q [R [S [T [U V]]]]]]]]. + intros (rs' & m1' & A & B & C & D & E & F & G). econstructor; split. - eapply plus_right. eexact S. econstructor; eauto. - traceEq. + eapply plus_right. eexact D. econstructor; eauto. traceEq. 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; apply Plt_ne; auto. - intros. rewrite <- H1. eapply Mem.load_free; eauto. left; apply Plt_ne; auto. - eauto with mem. intros. eapply Mem.perm_free_3; eauto. - apply Plt_Ple. change (Mem.valid_block m' stk). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_linear; eauto. - apply Plt_Ple. change (Mem.valid_block m1' sp'). eapply Mem.valid_block_free_1; eauto. eapply agree_valid_mach; eauto. + rewrite sep_swap; exact G. - (* internal function *) 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. - exploit function_prologue_correct; eauto. eapply wt_callstate_wt_regs; eauto. + destruct (transf_function f) as [tfn|] eqn:TRANSL; simpl; try congruence. + intros EQ; inversion EQ; clear EQ; subst tf. + rewrite sep_comm, sep_assoc in SEP. + exploit function_prologue_correct; eauto. + red; intros; eapply wt_callstate_wt_regs; eauto. eapply match_stacks_type_sp; eauto. eapply match_stacks_type_retaddr; eauto. - intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]]. + clear SEP; + intros (j' & rs' & m2' & sp' & m3' & m4' & m5' & A & B & C & D & E & F & SEP & J & K). + rewrite (sep_comm (globalenv_inject ge j')) in SEP. + rewrite (sep_swap (minjection j' m')) in SEP. econstructor; split. 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. apply Ple_refl. - eauto with mem. intros. exploit Mem.perm_alloc_inv. eexact H. eauto. - rewrite dec_eq_false; auto. apply Plt_ne; auto. - 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. + eapply match_states_intro with (j := j'); eauto with coqlib. + eapply match_stacks_change_meminj; eauto. + rewrite sep_swap in SEP. rewrite sep_swap. eapply stack_contents_change_meminj; eauto. - (* external function *) simpl in TRANSL. inversion TRANSL; subst tf. - 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]]]]]]]]]. + exploit transl_external_arguments; eauto. apply sep_proj1 in SEP; eauto. intros [vl [ARGS VINJ]]. + rewrite sep_comm, sep_assoc in SEP. + inv H0. + exploit external_call_parallel_rule; eauto. + eapply decode_longs_inject; eauto. + intros (j' & res' & m1' & A & B & C & D & E). econstructor; split. apply plus_one. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved'; eauto. apply senv_preserved. - econstructor; eauto. - apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0). - inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. - eapply external_call_nextblock'; eauto. - eapply external_call_nextblock'; eauto. - apply agree_regs_set_regs; auto. apply agree_regs_inject_incr with j; auto. + eapply external_call_symbols_preserved'. econstructor; eauto. apply senv_preserved. + eapply match_states_return with (j := j'). + eapply match_stacks_change_meminj; eauto. + apply agree_regs_set_regs. apply agree_regs_inject_incr with j; auto. apply encode_long_inject; auto. apply agree_callee_save_set_result; auto. + apply stack_contents_change_meminj with j; auto. + rewrite sep_comm, sep_assoc; auto. - (* return *) - inv STACKS. simpl in AGLOCS. + inv STACKS. simpl in AGLOCS. simpl in SEP. rewrite sep_assoc in SEP. econstructor; split. apply plus_one. apply exec_return. econstructor; eauto. - apply agree_frame_return with rs0; auto. + apply agree_locs_return with rs0; auto. + apply frame_contents_exten with rs0 (parent_locset s); auto. Qed. Lemma transf_initial_states: @@ -2862,18 +2113,21 @@ Proof. eapply (Genv.init_mem_transf_partial TRANSF); eauto. rewrite (match_program_main TRANSF). rewrite symbols_preserved. eauto. - econstructor; eauto. + set (j := Mem.flat_inj (Mem.nextblock m0)). + eapply match_states_call with (j := j); eauto. + constructor. red; intros. rewrite H3, loc_arguments_main in H. contradiction. + red; simpl; auto. + red; simpl; auto. + simpl. rewrite sep_pure. split; auto. split;[|split]. eapply Genv.initmem_inject; eauto. - apply match_stacks_empty with (Mem.nextblock m0). apply Ple_refl. apply Ple_refl. - constructor. - intros. unfold Mem.flat_inj. apply pred_dec_true; auto. - unfold Mem.flat_inj; intros. destruct (plt 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_funct_ptr_not_fresh; eauto. - intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. - rewrite H3. red; intros. rewrite loc_arguments_main in H. contradiction. - unfold Locmap.init. red; intros; auto. - unfold parent_locset. red; auto. + simpl. exists (Mem.nextblock m0); split. apply Ple_refl. + unfold j, Mem.flat_inj; constructor; intros. + apply pred_dec_true; auto. + destruct (plt b1 (Mem.nextblock m0)); congruence. + change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto. + change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto. + change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. + red; simpl; tauto. Qed. Lemma transf_final_states: |