diff options
Diffstat (limited to 'backend/Machabstr2concr.v')
| -rw-r--r-- | backend/Machabstr2concr.v | 735 |
1 files changed, 355 insertions, 380 deletions
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index ffdfb336..2dd3134f 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -27,7 +27,6 @@ Require Import Mach. Require Import Machtyping. Require Import Machabstr. Require Import Machconcr. -Require Import Stackingproof. Require Import PPCgenretaddr. (** Two semantics were defined for the Mach intermediate language: @@ -48,27 +47,6 @@ Require Import PPCgenretaddr. Mach semantics as input). *) -Remark align_16_top_ge: - forall lo hi, - hi <= align_16_top lo hi. -Proof. - intros. unfold align_16_top. apply Zmax_bound_r. - assert (forall x, x <= (x + 15) / 16 * 16). - intro. assert (16 > 0). omega. - generalize (Z_div_mod_eq (x + 15) 16 H). intro. - replace ((x + 15) / 16 * 16) with ((x + 15) - (x + 15) mod 16). - generalize (Z_mod_lt (x + 15) 16 H). omega. - rewrite Zmult_comm. omega. - generalize (H (hi - lo)). omega. -Qed. - -Remark align_16_top_pos: - forall lo hi, - 0 <= align_16_top lo hi. -Proof. - intros. unfold align_16_top. apply Zmax_bound_l. omega. -Qed. - Remark size_type_chunk: forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty. Proof. @@ -79,11 +57,16 @@ Qed. (** ** Agreement for one frame *) +Section FRAME_MATCH. + +Variable f: function. +Hypothesis wt_f: wt_function f. + (** The core idea of the simulation proof is that for all active functions, the memory-allocated activation record, in the concrete semantics, contains the same data as the Cminor stack block (at positive offsets) and the frame of the function (at negative - offsets) in the abstract semantics. + offsets) in the abstract semantics This intuition (activation record = Cminor stack data + frame) is formalized by the following predicate [frame_match fr sp base mm ms]. @@ -91,19 +74,18 @@ Qed. semantics. [ms] is the current memory state in the concrete semantics. The stack pointer is [Vptr sp base] in both semantics. *) -Inductive frame_match (fr: frame) (sp: block) (base: int) +Inductive frame_match (fr: frame) + (sp: block) (base: int) (mm ms: mem) : Prop := frame_match_intro: valid_block ms sp -> low_bound mm sp = 0 -> - low_bound ms sp = fr.(fr_low) -> + low_bound ms sp = -f.(fn_framesize) -> high_bound ms sp >= 0 -> - fr.(fr_low) <= -24 -> - Int.min_signed <= fr.(fr_low) -> - base = Int.repr fr.(fr_low) -> + base = Int.repr (-f.(fn_framesize)) -> (forall ty ofs, - fr.(fr_low) + 24 <= ofs -> ofs + AST.typesize ty <= 0 -> - load (chunk_of_type ty) ms sp ofs = Some(fr.(fr_contents) ty ofs)) -> + -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> + load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) -> frame_match fr sp base mm ms. (** The following two innocuous-looking lemmas are the key results @@ -140,22 +122,36 @@ Qed. to reading the corresponding slot from the frame (in the abstract semantics). *) +Lemma frame_match_load_stack: + forall fr sp base mm ms ty ofs, + frame_match fr sp base mm ms -> + 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + load_stack ms (Vptr sp base) ty ofs = + Some (fr ty (Int.signed ofs - f.(fn_framesize))). +Proof. + intros. inv H. + unfold load_stack, Val.add, loadv. + replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs)) + with (Int.signed ofs - fn_framesize f). + apply H6. omega. omega. + inv wt_f. + assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). + apply Int.signed_repr. + assert (0 <= Int.max_signed). compute; congruence. omega. + rewrite int_add_no_overflow. rewrite H. omega. + rewrite H. split. omega. + apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. + compute; congruence. +Qed. + Lemma frame_match_get_slot: forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> - get_slot fr ty (Int.signed ofs) v -> + get_slot f fr ty (Int.signed ofs) v -> load_stack ms (Vptr sp base) ty ofs = Some v. Proof. - intros. inv H. inv H0. - unfold load_stack, Val.add, loadv. - assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr). - apply Int.signed_repr. - split. auto. apply Zle_trans with (-24). auto. compute; congruence. - assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs). - rewrite int_add_no_overflow. rewrite H0. auto. - rewrite H0. split. omega. apply Zle_trans with 0. - generalize (AST.typesize_pos ty). omega. compute; congruence. - rewrite H9. apply H8. omega. auto. + intros. inversion H. inv H0. eapply frame_match_load_stack; eauto. + inv H7. auto. Qed. (** Assigning a value to a frame slot (in the abstract semantics) @@ -163,41 +159,42 @@ Qed. (in the concrete semantics). Moreover, agreement between frames and activation records is preserved. *) -Lemma frame_match_set_slot: - forall fr sp base mm ms ty ofs v fr', +Lemma frame_match_store_stack: + forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> - set_slot fr ty (Int.signed ofs) v fr' -> + 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> Val.has_type v ty -> Mem.extends mm ms -> exists ms', store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ - frame_match fr' sp base mm ms' /\ - Mem.extends mm ms' /\ - Int.signed base + 24 <= Int.signed (Int.add base ofs). + frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\ + Mem.extends mm ms'. Proof. - intros. inv H. inv H0. + intros. inv H. inv wt_f. unfold store_stack, Val.add, storev. - assert (Int.signed (Int.repr (fr_low fr)) = fr_low fr). - apply Int.signed_repr. - split. auto. apply Zle_trans with (-24). auto. compute; congruence. - assert (Int.signed (Int.add (Int.repr (fr_low fr)) ofs) = fr_low fr + Int.signed ofs). - rewrite int_add_no_overflow. congruence. - rewrite H0. split. omega. apply Zle_trans with 0. - generalize (AST.typesize_pos ty). omega. compute; congruence. - rewrite H11. - assert (exists ms', store (chunk_of_type ty) ms sp (fr_low fr + Int.signed ofs) v = Some ms'). + assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) = + Int.signed ofs - fn_framesize f). + assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). + apply Int.signed_repr. + assert (0 <= Int.max_signed). compute; congruence. omega. + rewrite int_add_no_overflow. rewrite H. omega. + rewrite H. split. omega. + apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. + compute; congruence. + rewrite H. + assert (exists ms', store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v = Some ms'). apply valid_access_store. constructor. auto. omega. rewrite size_type_chunk. omega. - destruct H12 as [ms' STORE]. + destruct H7 as [ms' STORE]. generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB. generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB. exists ms'. split. exact STORE. (* frame match *) - split. constructor; simpl fr_low; try congruence. - eauto with mem. intros. simpl. - destruct (zeq (fr_low fr + Int.signed ofs) ofs0). subst ofs0. + split. constructor; try congruence. + eauto with mem. intros. unfold update. + destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0. destruct (typ_eq ty ty0). subst ty0. (* same *) transitivity (Some (Val.load_result (chunk_of_type ty) v)). @@ -206,33 +203,45 @@ Proof. (* mismatch *) eapply load_store_mismatch'; eauto with mem. destruct ty; destruct ty0; simpl; congruence. - destruct (zle (ofs0 + AST.typesize ty0) (fr_low fr + Int.signed ofs)). + destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)). (* disjoint *) - rewrite <- H10; auto. eapply load_store_other; eauto. + rewrite <- H8; auto. eapply load_store_other; eauto. right; left. rewrite size_type_chunk; auto. - destruct (zle (fr_low fr + Int.signed ofs + AST.typesize ty)). - rewrite <- H10; auto. eapply load_store_other; eauto. + destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)). + rewrite <- H8; auto. eapply load_store_other; eauto. right; right. rewrite size_type_chunk; auto. (* overlap *) eapply load_store_overlap'; eauto with mem. rewrite size_type_chunk; auto. rewrite size_type_chunk; auto. (* extends *) - split. eapply store_outside_extends; eauto. + eapply store_outside_extends; eauto. left. rewrite size_type_chunk. omega. - (* bound *) - omega. +Qed. + +Lemma frame_match_set_slot: + forall fr sp base mm ms ty ofs v fr', + frame_match fr sp base mm ms -> + set_slot f fr ty (Int.signed ofs) v fr' -> + Val.has_type v ty -> + Mem.extends mm ms -> + exists ms', + store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ + frame_match fr' sp base mm ms' /\ + Mem.extends mm ms'. +Proof. + intros. inv H0. eapply frame_match_store_stack; eauto. + inv H3. auto. Qed. (** Agreement is preserved by stores within blocks other than the - one pointed to by [sp], or to the low 24 bytes - of the [sp] block. *) + one pointed to by [sp]. *) Lemma frame_match_store_other: forall fr sp base mm ms chunk b ofs v ms', frame_match fr sp base mm ms -> store chunk ms b ofs v = Some ms' -> - sp <> b \/ ofs + size_chunk chunk <= fr_low fr + 24 -> + sp <> b -> frame_match fr sp base mm ms'. Proof. intros. inv H. @@ -242,11 +251,13 @@ Proof. eauto with mem. congruence. congruence. - intros. rewrite <- H9; auto. + intros. rewrite <- H7; auto. eapply load_store_other; eauto. - elim H1; intro. auto. right. rewrite size_type_chunk. omega. Qed. +(** Agreement is preserved by parallel stores in the Machabstr + and the Machconcr semantics. *) + Lemma frame_match_store: forall fr sp base mm ms chunk b ofs v mm' ms', frame_match fr sp base mm ms -> @@ -262,31 +273,11 @@ Proof. apply frame_match_intro; auto. eauto with mem. congruence. congruence. congruence. - intros. rewrite <- H9; auto. eapply load_store_other; eauto. + intros. rewrite <- H7; auto. eapply load_store_other; eauto. destruct (zeq sp b). subst b. right. rewrite size_type_chunk. assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H10. left. omega. - auto. -Qed. - -(** The low 24 bytes of a frame are preserved by a parallel - store in the two memory states. *) - -Lemma frame_match_store_link_invariant: - forall fr sp base mm ms chunk b ofs v mm' ms' ofs', - frame_match fr sp base mm ms -> - store chunk mm b ofs v = Some mm' -> - store chunk ms b ofs v = Some ms' -> - ofs' <= fr_low fr + 20 -> - load Mint32 ms' sp ofs' = load Mint32 ms sp ofs'. -Proof. - intros. inv H. - eapply load_store_other; eauto. - destruct (eq_block sp b). subst b. - right; left. change (size_chunk Mint32) with 4. - assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H. omega. + inv H8. left. omega. auto. Qed. @@ -297,14 +288,12 @@ Qed. remain true. *) Lemma frame_match_new: - forall mm ms mm' ms' sp sp' f, + forall mm ms mm' ms' sp sp', mm.(nextblock) = ms.(nextblock) -> alloc mm 0 f.(fn_stacksize) = (mm', sp) -> - alloc ms (- f.(fn_framesize)) (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) = (ms', sp') -> - f.(fn_framesize) >= 24 -> - f.(fn_framesize) <= -Int.min_signed -> + alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') -> sp = sp' /\ - frame_match (init_frame f) sp (Int.repr (-f.(fn_framesize))) mm' ms'. + frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'. Proof. intros. assert (sp = sp'). @@ -315,13 +304,12 @@ Proof. generalize (low_bound_alloc_same _ _ _ _ _ H1). intro LBs. generalize (high_bound_alloc_same _ _ _ _ _ H0). intro HBm. generalize (high_bound_alloc_same _ _ _ _ _ H1). intro HBs. + inv wt_f. constructor; simpl; eauto with mem. - rewrite HBs. apply Zle_ge. apply align_16_top_pos. - omega. omega. + rewrite HBs. auto. intros. - eapply load_alloc_same'; eauto. omega. - rewrite size_type_chunk. apply Zle_trans with 0. auto. - apply align_16_top_pos. + eapply load_alloc_same'; eauto. + rewrite size_type_chunk. omega. Qed. Lemma frame_match_alloc: @@ -334,13 +322,13 @@ Lemma frame_match_alloc: Proof. intros. inversion H0. assert (valid_block mm sp). red. rewrite H. auto. - exploit low_bound_alloc_other. eexact H1. eexact H11. intro LBm. - exploit high_bound_alloc_other. eexact H1. eexact H11. intro HBm. + exploit low_bound_alloc_other. eexact H1. eexact H9. intro LBm. + exploit high_bound_alloc_other. eexact H1. eexact H9. intro HBm. exploit low_bound_alloc_other. eexact H2. eexact H3. intro LBs. exploit high_bound_alloc_other. eexact H2. eexact H3. intro HBs. apply frame_match_intro. eapply valid_block_alloc; eauto. - congruence. congruence. congruence. auto. auto. auto. + congruence. congruence. congruence. auto. auto. intros. eapply load_alloc_other; eauto. Qed. @@ -360,9 +348,138 @@ Proof. generalize (high_bound_free ms _ _ H0); intro HBs. apply frame_match_intro; auto. congruence. congruence. congruence. - intros. rewrite <- H8; auto. apply load_free. auto. + intros. rewrite <- H6; auto. apply load_free. auto. +Qed. + +End FRAME_MATCH. + +(** ** Accounting for the return address and back link *) + +Section EXTEND_FRAME. + +Variable f: function. +Hypothesis wt_f: wt_function f. +Variable cs: list Machconcr.stackframe. + +Definition extend_frame (fr: frame) : frame := + update Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize)) (parent_ra cs) + (update Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize)) (parent_sp cs) + fr). + +Lemma get_slot_extends: + forall fr ty ofs v, + get_slot f fr ty ofs v -> + get_slot f (extend_frame fr) ty ofs v. +Proof. + intros. inv H. constructor. auto. + inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro. + unfold extend_frame. rewrite update_other. rewrite update_other. auto. + simpl; omega. simpl; omega. +Qed. + +Lemma update_commut: + forall ty1 ofs1 v1 ty2 ofs2 v2 fr, + ofs1 + AST.typesize ty1 <= ofs2 \/ + ofs2 + AST.typesize ty2 <= ofs1 -> + update ty1 ofs1 v1 (update ty2 ofs2 v2 fr) = + update ty2 ofs2 v2 (update ty1 ofs1 v1 fr). +Proof. + intros. unfold frame. + apply extensionality. intro ty. apply extensionality. intro ofs. + generalize (AST.typesize_pos ty1). + generalize (AST.typesize_pos ty2). + generalize (AST.typesize_pos ty); intros. + unfold update. + set (sz1 := AST.typesize ty1) in *. + set (sz2 := AST.typesize ty2) in *. + set (sz := AST.typesize ty) in *. + destruct (zeq ofs1 ofs). + rewrite zeq_false. + destruct (zle (ofs + sz) ofs2). auto. + destruct (zle (ofs2 + sz2) ofs). auto. + destruct (typ_eq ty1 ty); auto. + replace sz with sz1 in z. omegaContradiction. unfold sz1, sz; congruence. + omega. + + destruct (zle (ofs + sz) ofs1). + auto. + destruct (zle (ofs1 + sz1) ofs). + auto. + + destruct (zeq ofs2 ofs). + destruct (typ_eq ty2 ty); auto. + replace sz with sz2 in z. omegaContradiction. unfold sz2, sz; congruence. + destruct (zle (ofs + sz) ofs2); auto. + destruct (zle (ofs2 + sz2) ofs); auto. +Qed. + +Lemma set_slot_extends: + forall fr ty ofs v fr', + set_slot f fr ty ofs v fr' -> + set_slot f (extend_frame fr) ty ofs v (extend_frame fr'). +Proof. + intros. inv H. constructor. auto. + inv H0. inv wt_f. generalize (AST.typesize_pos ty); intro. + unfold extend_frame. + rewrite (update_commut ty). rewrite (update_commut ty). auto. + simpl. omega. + simpl. omega. +Qed. + +Lemma frame_match_load_link: + forall fr sp base mm ms, + frame_match f (extend_frame fr) sp base mm ms -> + load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs). +Proof. + intros. inversion wt_f. + replace (parent_sp cs) with + (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). + eapply frame_match_load_stack; eauto. + unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. +Qed. + +Lemma frame_match_load_retaddr: + forall fr sp base mm ms, + frame_match f (extend_frame fr) sp base mm ms -> + load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs). +Proof. + intros. inversion wt_f. + replace (parent_ra cs) with + (extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))). + eapply frame_match_load_stack; eauto. + unfold extend_frame. apply update_same. +Qed. + +Lemma frame_match_function_entry: + forall mm ms mm' ms1 sp sp', + extends mm ms -> + alloc mm 0 f.(fn_stacksize) = (mm', sp) -> + alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') -> + Val.has_type (parent_sp cs) Tint -> + Val.has_type (parent_ra cs) Tint -> + let base := Int.repr (-f.(fn_framesize)) in + exists ms2, exists ms3, + sp = sp' /\ + store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\ + store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\ + frame_match f (extend_frame empty_frame) sp base mm' ms3 /\ + extends mm' ms3. +Proof. + intros. inversion wt_f. + exploit alloc_extends; eauto. omega. omega. intros [A EXT0]. + exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto. + fold base. intros [C FM0]. + destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ + FM0 wt_function_link H2 EXT0) + as [ms2 [STORE1 [FM1 EXT1]]]. + destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ + FM1 wt_function_retaddr H3 EXT1) + as [ms3 [STORE2 [FM3 EXT3]]]. + exists ms2; exists ms3; auto. Qed. +End EXTEND_FRAME. + (** ** Invariant for stacks *) Section SIMULATION. @@ -380,31 +497,27 @@ Let ge := Genv.globalenv p. their addresses increase strictly from caller to callee. *) +Definition stack_below (ts: list Machconcr.stackframe) (b: block) : Prop := + match parent_sp ts with + | Vptr sp base' => sp < b + | _ => False + end. + Inductive match_stacks: list Machabstr.stackframe -> list Machconcr.stackframe -> - block -> int -> mem -> mem -> Prop := - | match_stacks_nil: forall sp base mm ms, - load Mint32 ms sp (Int.signed base) = Some (Vptr Mem.nullptr Int.zero) -> - load Mint32 ms sp (Int.signed base + 12) = Some Vzero -> - match_stacks nil nil sp base mm ms - | match_stacks_cons: forall f sp' base' c fr s fb ra ts sp base mm ms, - frame_match fr sp' base' mm ms -> - sp' < sp -> - load Mint32 ms sp (Int.signed base) = Some (Vptr sp' base') -> - load Mint32 ms sp (Int.signed base + 12) = Some ra -> + mem -> mem -> Prop := + | match_stacks_nil: forall mm ms, + match_stacks nil nil mm ms + | match_stacks_cons: forall fb sp base c fr s f ra ts mm ms, Genv.find_funct_ptr ge fb = Some (Internal f) -> - match_stacks s ts sp' base' mm ms -> - match_stacks (Machabstr.Stackframe f (Vptr sp' base') c fr :: s) - (Machconcr.Stackframe fb (Vptr sp' base') ra c :: ts) - sp base mm ms. - -Remark frame_match_base_eq: - forall fr sp base mm ms, - frame_match fr sp base mm ms -> Int.signed base = fr_low fr. -Proof. - intros. inv H. apply Int.signed_repr. split; auto. - apply Zle_trans with (-24); auto. compute; congruence. -Qed. + wt_function f -> + frame_match f (extend_frame f ts fr) sp base mm ms -> + stack_below ts sp -> + Val.has_type ra Tint -> + match_stacks s ts mm ms -> + match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s) + (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts) + mm ms. (** If [match_stacks] holds, a lookup in the parent frame in the Machabstr semantics corresponds to two memory loads in the @@ -412,230 +525,128 @@ Qed. activation record, the second to read within this record. *) Lemma match_stacks_get_parent: - forall s ts sp base mm ms ty ofs v, - match_stacks s ts sp base mm ms -> - get_slot (parent_frame s) ty (Int.signed ofs) v -> - exists parent, - load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some parent - /\ load_stack ms parent ty ofs = Some v. + forall s ts mm ms ty ofs v, + match_stacks s ts mm ms -> + get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v -> + load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v. Proof. intros. inv H; simpl in H0. - inv H0. simpl in H3. elimtype False. generalize (AST.typesize_pos ty). omega. - exists (Vptr sp' base'); split. - unfold load_stack. simpl. rewrite Int.add_zero. auto. - eapply frame_match_get_slot; eauto. + inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega. + simpl. eapply frame_match_get_slot; eauto. + eapply get_slot_extends; eauto. Qed. -(** If [match_stacks] holds, reading memory at offsets 0 and 12 - from the stack pointer returns the stack pointer and return - address of the caller, respectively. *) +(** Preservation of the [match_stacks] invariant + by various kinds of memory stores. *) -Lemma match_stacks_load_links: - forall fr s ts sp base mm ms, - frame_match fr sp base mm ms -> - match_stacks s ts sp base mm ms -> - load_stack ms (Vptr sp base) Tint (Int.repr 0) = Some (parent_sp ts) /\ - load_stack ms (Vptr sp base) Tint (Int.repr 12) = Some (parent_ra ts). -Proof. - intros. unfold load_stack. simpl. rewrite Int.add_zero. - replace (Int.signed (Int.add base (Int.repr 12))) - with (Int.signed base + 12). - inv H0; simpl; auto. - inv H. rewrite Int.add_signed. - change (Int.signed (Int.repr 12)) with 12. - repeat rewrite Int.signed_repr. auto. - split. omega. apply Zle_trans with (-12). omega. compute; congruence. - split. auto. apply Zle_trans with (-24). auto. compute; congruence. -Qed. - -(** The [match_stacks] invariant is preserved by memory stores - outside the 24-byte reserved area at the bottom of activation records. -*) +Remark stack_below_trans: + forall ts b b', + stack_below ts b -> b <= b' -> stack_below ts b'. +Proof. + unfold stack_below; intros. + destruct (parent_sp ts); auto. omega. +Qed. Lemma match_stacks_store_other: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> forall chunk b ofs v ms', store chunk ms b ofs v = Some ms' -> - sp < b -> - match_stacks s ts sp base mm ms'. + stack_below ts b -> + match_stacks s ts mm ms'. Proof. induction 1; intros. - assert (sp <> b). unfold block; omega. constructor. - rewrite <- H. eapply load_store_other; eauto. - rewrite <- H0. eapply load_store_other; eauto. - assert (sp <> b). unfold block; omega. + red in H6; simpl in H6. econstructor; eauto. eapply frame_match_store_other; eauto. - left. unfold block; omega. - rewrite <- H1. eapply load_store_other; eauto. - rewrite <- H2. eapply load_store_other; eauto. - eapply IHmatch_stacks; eauto. omega. + unfold block; omega. + eapply IHmatch_stacks; eauto. + eapply stack_below_trans; eauto. omega. Qed. Lemma match_stacks_store_slot: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> - forall ty ofs v ms', - store_stack ms (Vptr sp base) ty ofs v = Some ms' -> - Int.signed base + 24 <= Int.signed (Int.add base ofs) -> - match_stacks s ts sp base mm ms'. + forall s ts ms mm, + match_stacks s ts mm ms -> + forall ty ofs v ms' b i, + stack_below ts b -> + store_stack ms (Vptr b i) ty ofs v = Some ms' -> + match_stacks s ts mm ms'. Proof. intros. - unfold store_stack in H0. simpl in H0. - assert (load Mint32 ms' sp (Int.signed base) = load Mint32 ms sp (Int.signed base)). - eapply load_store_other; eauto. - right; left. change (size_chunk Mint32) with 4; omega. - assert (load Mint32 ms' sp (Int.signed base + 12) = load Mint32 ms sp (Int.signed base + 12)). - eapply load_store_other; eauto. - right; left. change (size_chunk Mint32) with 4; omega. + unfold store_stack in H1. simpl in H1. inv H. - constructor; congruence. - constructor; auto. + constructor. + red in H0; simpl in H0. + econstructor; eauto. eapply frame_match_store_other; eauto. - left; unfold block; omega. - congruence. congruence. + unfold block; omega. eapply match_stacks_store_other; eauto. + eapply stack_below_trans; eauto. omega. Qed. Lemma match_stacks_store: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> - forall fr chunk b ofs v mm' ms', - frame_match fr sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> + forall chunk b ofs v mm' ms', store chunk mm b ofs v = Some mm' -> store chunk ms b ofs v = Some ms' -> - match_stacks s ts sp base mm' ms'. + match_stacks s ts mm' ms'. Proof. induction 1; intros. - assert (Int.signed base = fr_low fr) by (eapply frame_match_base_eq; eauto). constructor. - rewrite <- H. eapply frame_match_store_link_invariant; eauto. omega. - rewrite <- H0. eapply frame_match_store_link_invariant; eauto. omega. - assert (Int.signed base = fr_low fr0) by (eapply frame_match_base_eq; eauto). econstructor; eauto. - eapply frame_match_store; eauto. - rewrite <- H1. eapply frame_match_store_link_invariant; eauto. omega. - rewrite <- H2. eapply frame_match_store_link_invariant; eauto. omega. + eapply frame_match_store; eauto. Qed. Lemma match_stacks_alloc: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> forall lom him mm' bm los his ms' bs, mm.(nextblock) = ms.(nextblock) -> alloc mm lom him = (mm', bm) -> alloc ms los his = (ms', bs) -> - match_stacks s ts sp base mm' ms'. + match_stacks s ts mm' ms'. Proof. induction 1; intros. constructor. - rewrite <- H; eapply load_alloc_unchanged; eauto with mem. - rewrite <- H0; eapply load_alloc_unchanged; eauto with mem. econstructor; eauto. eapply frame_match_alloc; eauto. - rewrite <- H1; eapply load_alloc_unchanged; eauto with mem. - rewrite <- H2; eapply load_alloc_unchanged; eauto with mem. Qed. Lemma match_stacks_free: - forall s ts sp base ms mm, - match_stacks s ts sp base mm ms -> + forall s ts ms mm, + match_stacks s ts mm ms -> forall b, - sp < b -> - match_stacks s ts sp base (Mem.free mm b) (Mem.free ms b). + stack_below ts b -> + match_stacks s ts (Mem.free mm b) (Mem.free ms b). Proof. induction 1; intros. - assert (sp <> b). unfold block; omega. constructor. - rewrite <- H. apply load_free; auto. - rewrite <- H0. apply load_free; auto. - assert (sp <> b). unfold block; omega. + red in H5; simpl in H5. econstructor; eauto. eapply frame_match_free; eauto. unfold block; omega. - rewrite <- H1. apply load_free; auto. - rewrite <- H2. apply load_free; auto. - eapply IHmatch_stacks; eauto. omega. -Qed. - -(** Invocation of a function temporarily violates the [mach_stacks] - invariant: the return address and back link are not yet stored - in the appropriate parts of the activation record. - The following [match_stacks_partial] predicate is a weaker version - of [match_stacks] that captures this situation. *) - -Inductive match_stacks_partial: - list Machabstr.stackframe -> list Machconcr.stackframe -> - mem -> mem -> Prop := - | match_stacks_partial_nil: forall mm ms, - match_stacks_partial nil nil mm ms - | match_stacks_partial_cons: forall f sp base c fr s fb ra ts mm ms, - frame_match fr sp base mm ms -> - sp < ms.(nextblock) -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - match_stacks s ts sp base mm ms -> - Val.has_type ra Tint -> - match_stacks_partial (Machabstr.Stackframe f (Vptr sp base) c fr :: s) - (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts) - mm ms. - -Lemma match_stacks_match_stacks_partial: - forall s ts sp base mm ms, - match_stacks s ts sp base mm ms -> - match_stacks_partial s ts (free mm sp) (free ms sp). -Proof. - intros. inv H. constructor. - econstructor. - eapply frame_match_free; eauto. unfold block; omega. - simpl. inv H0; auto. - auto. - apply match_stacks_free; auto. - generalize (Mem.load_inv _ _ _ _ _ H3). intros [A B]. - rewrite B. - destruct (getN (pred_size_chunk Mint32) (Int.signed base + 12) - (contents (blocks ms sp))); exact I. + eapply IHmatch_stacks; eauto. + eapply stack_below_trans; eauto. omega. Qed. Lemma match_stacks_function_entry: - forall s ts mm ms lom him mm' los his ms' stk ms'' ms''' base, - match_stacks_partial s ts mm ms -> + forall s ts mm ms lom him mm' los his ms' stk, + match_stacks s ts mm ms -> alloc mm lom him = (mm', stk) -> alloc ms los his = (ms', stk) -> - store Mint32 ms' stk (Int.signed base) (parent_sp ts) = Some ms'' -> - store Mint32 ms'' stk (Int.signed base + 12) (parent_ra ts) = Some ms''' -> - match_stacks s ts stk base mm' ms'''. + match_stacks s ts mm' ms' /\ stack_below ts stk. Proof. - intros. - assert (WT_SP: Val.has_type (parent_sp ts) Tint). - inv H; simpl; auto. - assert (WT_RA: Val.has_type (parent_ra ts) Tint). - inv H; simpl; auto. - assert (load Mint32 ms''' stk (Int.signed base) = Some (parent_sp ts)). - transitivity (load Mint32 ms'' stk (Int.signed base)). - eapply load_store_other; eauto. right; left. simpl. omega. - transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_sp ts))). - simpl chunk_of_type. eapply load_store_same; eauto. - decEq. apply load_result_ty. auto. - assert (load Mint32 ms''' stk (Int.signed base + 12) = Some (parent_ra ts)). - transitivity (Some (Val.load_result (chunk_of_type Tint) (parent_ra ts))). - simpl chunk_of_type. eapply load_store_same; eauto. - decEq. apply load_result_ty. auto. - inv H; simpl in *. - constructor; auto. - assert (sp < stk). rewrite (alloc_result _ _ _ _ _ H1). auto. - assert (sp <> stk). unfold block; omega. - assert (nextblock mm = nextblock ms). - rewrite <- (alloc_result _ _ _ _ _ H0). - rewrite <- (alloc_result _ _ _ _ _ H1). auto. - econstructor; eauto. - eapply frame_match_store_other; eauto. - eapply frame_match_store_other; eauto. - eapply frame_match_alloc with (mm := mm) (ms := ms); eauto. - eapply match_stacks_store_other; eauto. - eapply match_stacks_store_other; eauto. - eapply match_stacks_alloc with (mm := mm) (ms := ms); eauto. - Qed. + intros. + assert (stk = nextblock mm). eapply Mem.alloc_result; eauto. + assert (stk = nextblock ms). eapply Mem.alloc_result; eauto. + split. + eapply match_stacks_alloc; eauto. congruence. + red. + inv H; simpl. + unfold nullptr. apply Zgt_lt. apply nextblock_pos. + inv H6. red in H. rewrite H3. auto. +Qed. (** ** Invariant between states. *) @@ -651,27 +662,27 @@ Inductive match_states: Machabstr.state -> Machconcr.state -> Prop := | match_states_intro: forall s f sp base c rs fr mm ts fb ms - (STACKS: match_stacks s ts sp base mm ms) - (FM: frame_match fr sp base mm ms) + (STACKS: match_stacks s ts mm ms) + (FM: frame_match f (extend_frame f ts fr) sp base mm ms) + (BELOW: stack_below ts sp) (MEXT: Mem.extends mm ms) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)), match_states (Machabstr.State s f (Vptr sp base) c rs fr mm) (Machconcr.State ts fb (Vptr sp base) c rs ms) | match_states_call: forall s f rs mm ts fb ms - (STACKS: match_stacks_partial s ts mm ms) + (STACKS: match_stacks s ts mm ms) (MEXT: Mem.extends mm ms) (FIND: Genv.find_funct_ptr ge fb = Some f), match_states (Machabstr.Callstate s f rs mm) (Machconcr.Callstate ts fb rs ms) | match_states_return: forall s rs mm ts ms - (STACKS: match_stacks_partial s ts mm ms) + (STACKS: match_stacks s ts mm ms) (MEXT: Mem.extends mm ms), match_states (Machabstr.Returnstate s rs mm) (Machconcr.Returnstate ts rs ms). - (** * The proof of simulation *) (** The proof of simulation relies on diagrams of the following form: @@ -710,29 +721,23 @@ Qed. Lemma transl_extcall_arguments: forall rs s sg args ts m ms, - Machabstr.extcall_arguments rs (parent_frame s) sg args -> - match_stacks_partial s ts m ms -> + Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args -> + match_stacks s ts m ms -> extcall_arguments rs ms (parent_sp ts) sg args. Proof. unfold Machabstr.extcall_arguments, extcall_arguments; intros. - assert (forall ty ofs v, - get_slot (parent_frame s) ty (Int.signed ofs) v -> - load_stack ms (parent_sp ts) ty ofs = Some v). - inv H0; simpl; intros. - inv H0. simpl in H2. elimtype False. generalize (AST.typesize_pos ty). omega. - eapply frame_match_get_slot; eauto. assert (forall locs vals, - Machabstr.extcall_args rs (parent_frame s) locs vals -> + Machabstr.extcall_args (parent_function s) rs (parent_frame s) locs vals -> extcall_args rs ms (parent_sp ts) locs vals). - induction locs; intros; inversion H2; subst; clear H2. + induction locs; intros; inv H1. constructor. constructor; auto. - inversion H7; subst; clear H7. - constructor. - constructor. auto. + inv H6. constructor. constructor. eapply match_stacks_get_parent; eauto. auto. Qed. +Hypothesis wt_prog: wt_program p. + Theorem step_equiv: forall s1 t s2, Machabstr.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1') (WTS: wt_state s1), @@ -746,27 +751,33 @@ Proof. econstructor; eauto with coqlib. (* Mgetstack *) + assert (WTF: wt_function f) by (inv WTS; auto). exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. - apply exec_Mgetstack; auto. eapply frame_match_get_slot; eauto. + constructor; auto. + eapply frame_match_get_slot; eauto. + eapply get_slot_extends; eauto. econstructor; eauto with coqlib. (* Msetstack *) + assert (WTF: wt_function f) by (inv WTS; auto). assert (Val.has_type (rs src) ty). inv WTS. generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI. inv WTI. apply WTRS. - exploit frame_match_set_slot; eauto. - intros [ms' [STORE [FM' [EXT' BOUND]]]]. + exploit frame_match_set_slot; eauto. + eapply set_slot_extends; eauto. + intros [ms' [STORE [FM' EXT']]]. exists (State ts fb (Vptr sp0 base) c rs ms'); split. apply exec_Msetstack; auto. econstructor; eauto. eapply match_stacks_store_slot; eauto. (* Mgetparam *) - exploit match_stacks_get_parent; eauto. - intros [parent [LOAD1 LOAD2]]. + assert (WTF: wt_function f) by (inv WTS; auto). exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. - eapply exec_Mgetparam; eauto. + eapply exec_Mgetparam; eauto. + eapply frame_match_load_link; eauto. + eapply match_stacks_get_parent; eauto. econstructor; eauto with coqlib. (* Mop *) @@ -802,16 +813,17 @@ Proof. econstructor; split. eapply exec_Mcall; eauto. econstructor; eauto. - econstructor; eauto. inv FM; auto. exact I. + econstructor; eauto. inv WTS; auto. exact I. (* Mtailcall *) + assert (WTF: wt_function f) by (inv WTS; auto). exploit find_function_find_function_ptr; eauto. intros [fb' [FIND' FINDFUNCT]]. - exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2]. econstructor; split. eapply exec_Mtailcall; eauto. - econstructor; eauto. - eapply match_stacks_match_stacks_partial; eauto. + eapply frame_match_load_link; eauto. + eapply frame_match_load_retaddr; eauto. + econstructor; eauto. eapply match_stacks_free; auto. apply free_extends; auto. (* Malloc *) @@ -841,67 +853,32 @@ Proof. econstructor; eauto. (* Mreturn *) - exploit match_stacks_load_links; eauto. intros [LOAD1 LOAD2]. + assert (WTF: wt_function f) by (inv WTS; auto). econstructor; split. eapply exec_Mreturn; eauto. - econstructor; eauto. - eapply match_stacks_match_stacks_partial; eauto. + eapply frame_match_load_link; eauto. + eapply frame_match_load_retaddr; eauto. + econstructor; eauto. eapply match_stacks_free; eauto. apply free_extends; auto. (* internal function *) - assert (WTF: wt_function f). inv WTS. inv H5. auto. inv WTF. - caseEq (alloc ms (- f.(fn_framesize)) - (align_16_top (- f.(fn_framesize)) f.(fn_stacksize))). + assert (WTF: wt_function f). inv WTS. inv H5. auto. + caseEq (alloc ms (- f.(fn_framesize)) f.(fn_stacksize)). intros ms' stk' ALLOC. - exploit (alloc_extends m ms m' ms' 0 (fn_stacksize f) - (- fn_framesize f) - (align_16_top (- fn_framesize f) (fn_stacksize f))); eauto. - omega. apply align_16_top_ge. - intros [EQ EXT']. subst stk'. - exploit (frame_match_new m ms); eauto. inv MEXT; auto. - intros [EQ FM]. clear EQ. - set (sp := Vptr stk (Int.repr (- fn_framesize f))). - assert (exists ms'', store Mint32 ms' stk (- fn_framesize f) (parent_sp ts) = Some ms''). - apply valid_access_store. constructor. - eauto with mem. - rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega. - rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC). - change (size_chunk Mint32) with 4. - apply Zle_trans with 0. omega. apply align_16_top_pos. - destruct H0 as [ms'' STORE1]. - assert (exists ms''', store Mint32 ms'' stk (- fn_framesize f + 12) (parent_ra ts) = Some ms'''). - apply valid_access_store. constructor. - eauto with mem. - rewrite (low_bound_store _ _ _ _ _ _ STORE1 stk). - rewrite (low_bound_alloc_same _ _ _ _ _ ALLOC). omega. - rewrite (high_bound_store _ _ _ _ _ _ STORE1 stk). - rewrite (high_bound_alloc_same _ _ _ _ _ ALLOC). - change (size_chunk Mint32) with 4. - apply Zle_trans with 0. omega. apply align_16_top_pos. - destruct H0 as [ms''' STORE2]. - assert (RANGE1: Int.min_signed <= - fn_framesize f <= Int.max_signed). - split. omega. apply Zle_trans with (-24). omega. compute;congruence. - assert (RANGE2: Int.min_signed <= - fn_framesize f + 12 <= Int.max_signed). - split. omega. apply Zle_trans with (-12). omega. compute;congruence. + assert (Val.has_type (parent_sp ts) Tint). + inv STACKS; simpl; auto. + assert (Val.has_type (parent_ra ts) Tint). + inv STACKS; simpl; auto. + destruct (frame_match_function_entry _ WTF _ _ _ _ _ _ _ + MEXT H ALLOC H0 H1) + as [ms2 [ms3 [EQ [STORE1 [STORE2 [FM MEXT']]]]]]. + subst stk'. econstructor; split. eapply exec_function_internal; eauto. - unfold store_stack. simpl. rewrite Int.add_zero. - rewrite Int.signed_repr. eauto. auto. - unfold store_stack. simpl. rewrite Int.add_signed. - change (Int.signed (Int.repr 12)) with 12. - repeat rewrite Int.signed_repr; eauto. - (* match states *) - unfold sp; econstructor; eauto. - eapply match_stacks_function_entry; eauto. - rewrite Int.signed_repr; eauto. - rewrite Int.signed_repr; eauto. - eapply frame_match_store_other with (ms := ms''); eauto. - eapply frame_match_store_other with (ms := ms'); eauto. - simpl. right; omega. simpl. right; omega. - eapply store_outside_extends with (m2 := ms''); eauto. - eapply store_outside_extends with (m2 := ms'); eauto. - rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega. - rewrite (low_bound_alloc_same _ _ _ _ _ H). simpl; omega. + exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW]. + econstructor; eauto. + eapply match_stacks_store_slot with (ms := ms2); eauto. + eapply match_stacks_store_slot with (ms := ms'); eauto. (* external function *) econstructor; split. @@ -916,8 +893,6 @@ Proof. econstructor; eauto. Qed. -Hypothesis wt_prog: wt_program p. - Lemma equiv_initial_states: forall st1, Machabstr.initial_state p st1 -> exists st2, Machconcr.initial_state p st2 /\ match_states st1 st2 /\ wt_state st1. |