From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 222 +++++-- common/Globalenvs.v | 293 ++++++--- common/Memory.v | 1776 +++++++++++++++++++++------------------------------ common/Memtype.v | 246 ++++--- 4 files changed, 1182 insertions(+), 1355 deletions(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index 3d082a7..93e1827 100644 --- a/common/Events.v +++ b/common/Events.v @@ -560,23 +560,22 @@ Definition extcall_sem : Type := (** We now specify the expected properties of this predicate. *) Definition mem_unchanged_on (P: block -> Z -> Prop) (m_before m_after: mem): Prop := - (forall b ofs p, - P b ofs -> Mem.perm m_before b ofs p -> Mem.perm m_after b ofs p) + (forall b ofs k p, + P b ofs -> Mem.perm m_before b ofs k p -> Mem.perm m_after b ofs k p) /\(forall chunk b ofs v, (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) -> Mem.load chunk m_before b ofs = Some v -> Mem.load chunk m_after b ofs = Some v). Definition loc_out_of_bounds (m: mem) (b: block) (ofs: Z) : Prop := - ofs < Mem.low_bound m b \/ ofs > Mem.high_bound m b. + ~Mem.perm m b ofs Max Nonempty. Definition loc_unmapped (f: meminj) (b: block) (ofs: Z): Prop := f b = None. Definition loc_out_of_reach (f: meminj) (m: mem) (b: block) (ofs: Z): Prop := forall b0 delta, - f b0 = Some(b, delta) -> - ofs < Mem.low_bound m b0 + delta \/ ofs >= Mem.high_bound m b0 + delta. + f b0 = Some(b, delta) -> ~Mem.perm m b0 (ofs - delta) Max Nonempty. Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := forall b1 b2 delta, @@ -613,11 +612,22 @@ Record extcall_properties (sem: extcall_sem) sem F V ge vargs m1 t vres m2 -> Mem.valid_block m1 b -> Mem.valid_block m2 b; -(** External calls preserve the bounds of valid blocks. *) - ec_bounds: - forall F V (ge: Genv.t F V) vargs m1 t vres m2 b, +(** External calls cannot increase the max permissions of a valid block. + They can decrease the max permissions, e.g. by freeing. *) + ec_max_perm: + forall F V (ge: Genv.t F V) vargs m1 t vres m2 b ofs p, + sem F V ge vargs m1 t vres m2 -> + Mem.valid_block m1 b -> Mem.perm m2 b ofs Max p -> Mem.perm m1 b ofs Max p; + +(** External call cannot modify memory unless they have [Max, Writable] + permissions. *) + ec_readonly: + forall F V (ge: Genv.t F V) vargs m1 t vres m2 chunk b ofs, sem F V ge vargs m1 t vres m2 -> - Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b; + Mem.valid_block m1 b -> + (forall ofs', ofs <= ofs' < ofs + size_chunk chunk -> + ~(Mem.perm m1 b ofs' Max Writable)) -> + Mem.load chunk m2 b ofs = Mem.load chunk m1 b ofs; (** External calls must commute with memory extensions, in the following sense. *) @@ -759,7 +769,9 @@ Proof. inv H1. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. -(* bounds *) +(* max perms *) + inv H; auto. +(* readonly *) inv H; auto. (* mem extends *) inv H. inv H1. inv H6. inv H4. @@ -821,7 +833,9 @@ Proof. inv H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. -(* bounds *) +(* max perm *) + inv H; auto. +(* readonly *) inv H; auto. (* extends *) inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. @@ -867,6 +881,28 @@ Proof. rewrite H0; auto. Qed. +Lemma volatile_store_readonly: + forall F V (ge: Genv.t F V) chunk1 m1 b1 ofs1 v t m2 chunk ofs b, + volatile_store ge chunk1 m1 b1 ofs1 v t m2 -> + Mem.valid_block m1 b -> + (forall ofs', ofs <= ofs' < ofs + size_chunk chunk -> + ~(Mem.perm m1 b ofs' Max Writable)) -> + Mem.load chunk m2 b ofs = Mem.load chunk m1 b ofs. +Proof. + intros. inv H. + auto. + eapply Mem.load_store_other; eauto. + destruct (eq_block b b1); auto. subst b1. right. + apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) + (Int.unsigned ofs1, Int.unsigned ofs1 + size_chunk chunk1)). + red; intros; red; intros. + elim (H1 x); auto. + exploit Mem.store_valid_access_3; eauto. intros [A B]. + apply Mem.perm_cur_max. apply A. auto. + simpl. generalize (size_chunk_pos chunk); omega. + simpl. generalize (size_chunk_pos chunk1); omega. +Qed. + Lemma volatile_store_extends: forall F V (ge: Genv.t F V) chunk m1 b ofs v t m2 m1' v', volatile_store ge chunk m1 b ofs v t m2 -> @@ -886,15 +922,14 @@ Proof. eapply Mem.perm_store_1; eauto. rewrite <- H4. eapply Mem.load_store_other; eauto. destruct (eq_block b0 b); auto. subst b0; right. - exploit Mem.valid_access_in_bounds. - eapply Mem.store_valid_access_3. eexact H3. - intros [C D]. - generalize (size_chunk_pos chunk0). intro E. - generalize (size_chunk_pos chunk). intro G. apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) (Int.unsigned ofs, Int.unsigned ofs + size_chunk chunk)). - red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega. - simpl; omega. simpl; omega. + red; intros; red; intros. + exploit (H x H5). exploit Mem.store_valid_access_3. eexact H3. intros [E G]. + apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. + auto. + simpl. generalize (size_chunk_pos chunk0). omega. + simpl. generalize (size_chunk_pos chunk). omega. Qed. Lemma volatile_store_inject: @@ -929,15 +964,15 @@ Proof. assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta). eapply Mem.address_inject; eauto with mem. unfold Mem.storev in A. rewrite EQ in A. rewrite EQ. - exploit Mem.valid_access_in_bounds. - eapply Mem.store_valid_access_3. eexact H0. - intros [C D]. - generalize (size_chunk_pos chunk0). intro E. - generalize (size_chunk_pos chunk). intro G. apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) (Int.unsigned ofs + delta, Int.unsigned ofs + delta + size_chunk chunk)). - red; intros. exploit (H1 x H7). eauto. unfold Intv.In; simpl. omega. - simpl; omega. simpl; omega. + red; intros; red; intros. exploit (H1 x H7). eauto. + exploit Mem.store_valid_access_3. eexact H0. intros [C D]. + apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. + apply C. red in H8; simpl in H8. omega. + auto. + simpl. generalize (size_chunk_pos chunk0). omega. + simpl. generalize (size_chunk_pos chunk). omega. Qed. Lemma volatile_store_receptive: @@ -961,8 +996,10 @@ Proof. inv H1. constructor. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H1. auto. eauto with mem. -(* bounds *) - inv H. inv H1. auto. eapply Mem.bounds_store; eauto. +(* perms *) + inv H. inv H2. auto. eauto with mem. +(* readonly *) + inv H. eapply volatile_store_readonly; eauto. (* mem extends*) inv H. inv H1. inv H6. inv H7. inv H4. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. @@ -1016,8 +1053,10 @@ Proof. inv H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H2. auto. eauto with mem. -(* bounds *) - inv H. inv H2. auto. eapply Mem.bounds_store; eauto. +(* perms *) + inv H. inv H3. auto. eauto with mem. +(* readonly *) + inv H. eapply volatile_store_readonly; eauto. (* mem extends*) rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. exploit ec_mem_extends. eapply volatile_store_ok. eexact Q. eauto. eauto. @@ -1076,11 +1115,15 @@ Proof. inv H1; econstructor; eauto. (* valid block *) inv H. eauto with mem. -(* bounds *) - inv H. transitivity (Mem.bounds m' b). - eapply Mem.bounds_store; eauto. - eapply Mem.bounds_alloc_other; eauto. +(* perms *) + inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto. + rewrite zeq_false. auto. apply Mem.valid_not_valid_diff with m1; eauto with mem. +(* readonly *) + inv H. transitivity (Mem.load chunk m' b ofs). + eapply Mem.load_store_other; eauto. + left. apply Mem.valid_not_valid_diff with m1; eauto with mem. + eapply Mem.load_alloc_unchanged; eauto. (* mem extends *) inv H. inv H1. inv H5. inv H7. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. @@ -1153,8 +1196,21 @@ Proof. inv H1; econstructor; eauto. (* valid block *) inv H. eauto with mem. -(* bounds *) - inv H. eapply Mem.bounds_free; eauto. +(* perms *) + inv H. eapply Mem.perm_free_3; eauto. +(* readonly *) + inv H. eapply Mem.load_free; eauto. + destruct (eq_block b b0); auto. + subst b0. right; right. + apply (Intv.range_disjoint' + (ofs, ofs + size_chunk chunk) + (Int.unsigned lo - 4, Int.unsigned lo + Int.unsigned sz)). + red; intros; red; intros. + elim (H1 x). auto. apply Mem.perm_cur_max. + apply Mem.perm_implies with Freeable; auto with mem. + exploit Mem.free_range_perm; eauto. + simpl. generalize (size_chunk_pos chunk); omega. + simpl. omega. (* mem extends *) inv H. inv H1. inv H8. inv H6. exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. @@ -1163,19 +1219,20 @@ Proof. econstructor; eauto. eapply UNCHANGED; eauto. omega. intros. destruct (eq_block b' b); auto. subst b; right. - red in H. - exploit Mem.range_perm_in_bounds. - eapply Mem.free_range_perm. eexact H4. omega. omega. + assert (~(Int.unsigned lo - 4 <= ofs < Int.unsigned lo + Int.unsigned sz)). + red; intros; elim H. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.free_range_perm. eexact H4. auto. + omega. (* mem inject *) inv H0. inv H2. inv H7. inv H9. exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. - assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Freeable). + assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable). eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. - apply Mem.perm_implies with Freeable; auto with mem. + apply Mem.perm_implies with Freeable; auto with mem. apply Mem.perm_cur_max. apply H0. instantiate (1 := lo). omega. intro EQ. - assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Freeable). + assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Cur Freeable). red; intros. replace ofs with ((ofs - delta) + delta) by omega. eapply Mem.perm_inject; eauto. apply H0. omega. @@ -1194,20 +1251,23 @@ Proof. subst b. assert (delta0 = delta) by congruence. subst delta0. exists (Int.unsigned lo - 4); exists (Int.unsigned lo + Int.unsigned sz); split. simpl; auto. omega. - elimtype False. - exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. - instantiate (1 := ofs + delta0 - delta). - apply Mem.perm_implies with Freeable; auto with mem. - apply H0. omega. eauto with mem. + elimtype False. exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. + instantiate (1 := ofs + delta0 - delta). + apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. + apply H0. omega. + eapply Mem.perm_max. eauto with mem. unfold block; omega. eapply UNCHANGED; eauto. omega. intros. red in H7. left. congruence. eapply UNCHANGED; eauto. omega. intros. - destruct (eq_block b' b2); auto. subst b'. right. - red in H7. generalize (H7 _ _ H6). intros. - exploit Mem.range_perm_in_bounds. eexact H0. omega. intros. omega. + destruct (eq_block b' b2); auto. subst b'. right. + assert (~(Int.unsigned lo + delta - 4 <= ofs < Int.unsigned lo + delta + Int.unsigned sz)). + red; intros. elim (H7 _ _ H6). + apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. + apply H0. omega. + omega. red; intros. congruence. (* trace length *) @@ -1245,8 +1305,20 @@ Proof. intros. inv H1. econstructor; eauto. (* valid blocks *) intros. inv H. eauto with mem. -(* bounds *) - intros. inv H. eapply Mem.bounds_storebytes; eauto. +(* perms *) + intros. inv H. eapply Mem.perm_storebytes_2; eauto. +(* readonly *) + intros. inv H. eapply Mem.load_storebytes_other; eauto. + destruct (eq_block b bdst); auto. subst b. right. + apply (Intv.range_disjoint' + (ofs, ofs + size_chunk chunk) + (Int.unsigned odst, Int.unsigned odst + Z_of_nat (length bytes))). + red; intros; red; intros. elim (H1 x); auto. + apply Mem.perm_cur_max. + eapply Mem.storebytes_range_perm; eauto. + simpl. generalize (size_chunk_pos chunk); omega. + simpl. rewrite (Mem.loadbytes_length _ _ _ _ _ H8). rewrite nat_of_Z_eq. + omega. omega. (* extensions *) intros. inv H. inv H1. inv H13. inv H14. inv H10. inv H11. @@ -1262,30 +1334,31 @@ Proof. exploit Mem.loadbytes_length. eexact H8. intros. rewrite <- H1. eapply Mem.load_storebytes_other; eauto. destruct (eq_block b bdst); auto. subst b; right. - exploit Mem.range_perm_in_bounds. eapply Mem.storebytes_range_perm. eexact H9. - rewrite H10. rewrite nat_of_Z_eq. omega. omega. - intros [P Q]. - exploit list_forall2_length; eauto. intros R. rewrite R in Q. + exploit list_forall2_length; eauto. intros R. apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) (Int.unsigned odst, Int.unsigned odst + Z_of_nat (length bytes2))); simpl. - red; intros. generalize (H x H11). unfold loc_out_of_bounds, Intv.In; simpl. omega. - generalize (size_chunk_pos chunk); omega. - rewrite <- R; rewrite H10. rewrite nat_of_Z_eq. omega. omega. + red; unfold Intv.In; simpl; intros; red; intros. + eapply (H x H11). + apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. + eapply Mem.storebytes_range_perm. eexact H9. + rewrite R. auto. + generalize (size_chunk_pos chunk). omega. + rewrite <- R. rewrite H10. rewrite nat_of_Z_eq. omega. omega. (* injections *) intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. exploit Mem.loadbytes_length; eauto. intros LEN. - assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Nonempty). + assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. - assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Nonempty). + assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Cur Nonempty). replace sz with (Z_of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. - assert (PSRC: Mem.perm m1 bsrc (Int.unsigned osrc) Nonempty). + assert (PSRC: Mem.perm m1 bsrc (Int.unsigned osrc) Cur Nonempty). apply RPSRC. omega. - assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Nonempty). + assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Cur Nonempty). apply RPDST. omega. - exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1. - exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2. + exploit Mem.address_inject. eauto. apply Mem.perm_cur_max. eexact PSRC. eauto. intros EQ1. + exploit Mem.address_inject. eauto. apply Mem.perm_cur_max. eexact PDST. eauto. intros EQ2. exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]]. exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]]. exists f; exists Vundef; exists m2'. @@ -1293,6 +1366,8 @@ Proof. eapply Mem.aligned_area_inject with (m := m1); eauto. eapply Mem.aligned_area_inject with (m := m1); eauto. eapply Mem.disjoint_or_equal_inject with (m := m1); eauto. + apply Mem.range_perm_max with Cur; auto. + apply Mem.range_perm_max with Cur; auto. split. constructor. split. auto. split. red; split; intros. eauto with mem. @@ -1306,10 +1381,8 @@ Proof. rewrite <- (list_forall2_length B). rewrite LEN. rewrite nat_of_Z_eq; try omega. apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) (Int.unsigned odst + delta0, Int.unsigned odst + delta0 + sz)); simpl. - red; intros. generalize (H0 x H12). unfold loc_out_of_reach, Intv.In; simpl. - intros. exploit H14; eauto. - exploit Mem.range_perm_in_bounds. eexact RPDST. omega. - omega. + red; unfold Intv.In; simpl; intros; red; intros. + eapply (H0 x H12). eauto. apply Mem.perm_cur_max. apply RPDST. omega. generalize (size_chunk_pos chunk); omega. omega. split. apply inject_incr_refl. @@ -1348,7 +1421,9 @@ Proof. eapply eventval_match_preserved; eauto. (* valid block *) inv H; auto. -(* bounds *) +(* perms *) + inv H; auto. +(* readonly *) inv H; auto. (* mem extends *) inv H. @@ -1403,7 +1478,9 @@ Proof. eapply eventval_list_match_preserved; eauto. (* valid blocks *) inv H; auto. -(* bounds *) +(* perms *) + inv H; auto. +(* readonly *) inv H; auto. (* mem extends *) inv H. @@ -1453,6 +1530,8 @@ Proof. inv H; auto. + inv H; auto. + inv H. inv H1. inv H6. exists v2; exists m1'; intuition. econstructor; eauto. @@ -1527,7 +1606,8 @@ Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). Definition external_call_arity ef := ec_arity (external_call_spec ef). Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef). Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef). -Definition external_call_bounds ef := ec_bounds (external_call_spec ef). +Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). +Definition external_call_readonly ef := ec_readonly (external_call_spec ef). Definition external_call_mem_extends ef := ec_mem_extends (external_call_spec ef). Definition external_call_mem_inject ef := ec_mem_inject (external_call_spec ef). Definition external_call_trace_length ef := ec_trace_length (external_call_spec ef). diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 539bb77..d7449f9 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -276,6 +276,40 @@ Proof. intros. unfold globalenv; eauto. Qed. +Theorem find_var_exists: + forall p id gv, + list_norepet (prog_var_names p) -> + In (id, gv) (prog_vars p) -> + exists b, + find_symbol (globalenv p) id = Some b + /\ find_var_info (globalenv p) b = Some gv. +Proof. + intros until gv. + assert (forall vl ge, + ~In id (var_names vl) -> + (exists b, find_symbol ge id = Some b /\ find_var_info ge b = Some gv) -> + (exists b, find_symbol (add_variables ge vl) id = Some b + /\ find_var_info (add_variables ge vl) b = Some gv)). + induction vl; simpl; intros. + auto. + apply IHvl. tauto. destruct a as [id1 gv1]. destruct H0 as [b [P Q]]. + unfold add_variable, find_symbol, find_var_info; simpl. + exists b; split. rewrite PTree.gso. auto. intuition. + rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. + unfold ZIndexed.t; omega. + + unfold globalenv, prog_var_names. + generalize (prog_vars p) (add_functions empty_genv (prog_funct p)). + induction l; simpl; intros. + contradiction. + destruct a as [id1 gv1]; simpl in *. inv H0. + destruct H1. inv H0. + apply H; auto. + exists (genv_nextvar t0); split. + unfold find_symbol, add_variable; simpl. apply PTree.gss. + unfold find_var_info, add_variable; simpl. apply ZMap.gss. + apply IHl; auto. +Qed. Remark add_variables_inversion : forall vs e x b, find_symbol (add_variables e vs) x = Some b -> @@ -740,50 +774,63 @@ Qed. Remark store_zeros_perm: - forall prm b' q m b n m', + forall k prm b' q m b n m', store_zeros m b n = Some m' -> - Mem.perm m b' q prm -> Mem.perm m' b' q prm. + (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. intros until n. functional induction (store_zeros m b n); intros. - inv H; auto. - eauto with mem. + inv H; tauto. + destruct (IHo _ H); intros. split; eauto with mem. congruence. Qed. Remark store_init_data_list_perm: - forall prm b' q idl b m p m', + forall k prm b' q idl b m p m', store_init_data_list m b p idl = Some m' -> - Mem.perm m b' q prm -> Mem.perm m' b' q prm. + (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. induction idl; simpl; intros until m'. - intros. congruence. - caseEq (store_init_data m b p a); try congruence. intros. - eapply IHidl; eauto. - destruct a; simpl in H; eauto with mem. - congruence. + intros. inv H. tauto. + caseEq (store_init_data m b p a); try congruence. intros. + rewrite <- (IHidl _ _ _ _ H0). + destruct a; simpl in H; split; eauto with mem. + inv H; auto. inv H; auto. + destruct (find_symbol ge i); try congruence. eauto with mem. destruct (find_symbol ge i); try congruence. eauto with mem. Qed. Remark alloc_variables_perm: - forall prm b' q vl m m', + forall k prm b' q vl m m', alloc_variables m vl = Some m' -> - Mem.perm m b' q prm -> Mem.perm m' b' q prm. + Mem.valid_block m b' -> + (Mem.perm m b' q k prm <-> Mem.perm m' b' q k prm). Proof. induction vl. - simpl; intros. congruence. + simpl; intros. inv H. tauto. intros until m'. simpl. unfold alloc_variable. set (init := gvar_init a#2). set (sz := init_data_list_size init). caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC. caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. - caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC PERM. + caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID. assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem. - eapply IHvl; eauto. - eapply Mem.perm_drop_3; eauto. - eapply store_init_data_list_perm; eauto. - eapply store_zeros_perm; eauto. + assert (VALID': Mem.valid_block m4 b'). + unfold Mem.valid_block. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + rewrite (store_zeros_nextblock _ _ _ STZ). + change (Mem.valid_block m1 b'). eauto with mem. + rewrite <- (IHvl _ _ REC VALID'). + split; intros. + eapply Mem.perm_drop_3; eauto. + rewrite <- store_init_data_list_perm; [idtac|eauto]. + rewrite <- store_zeros_perm; [idtac|eauto]. eauto with mem. + assert (Mem.perm m1 b' q k prm). + rewrite store_zeros_perm; [idtac|eauto]. + rewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. + exploit Mem.perm_alloc_inv; eauto. rewrite zeq_false; auto. Qed. Remark store_zeros_outside: @@ -913,56 +960,93 @@ Proof. repeat rewrite H. destruct a; intuition. Qed. -Lemma alloc_variables_charact: - forall id gv vl g m m', +Definition variables_initialized (g: t) (m: mem) := + forall b gv, + find_var_info g b = Some gv -> + Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv) + /\ (forall ofs k p, Mem.perm m b ofs k p -> + 0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p) + /\ (gv.(gvar_volatile) = false -> load_store_init_data m b 0 gv.(gvar_init)). + +Lemma alloc_variable_initialized: + forall g m id v m', genv_nextvar g = Mem.nextblock m -> - alloc_variables m vl = Some m' -> - list_norepet (map (@fst ident (globvar V)) vl) -> - In (id, gv) vl -> - exists b, find_symbol (add_variables g vl) id = Some b - /\ find_var_info (add_variables g vl) b = Some gv - /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv) - /\ (gv.(gvar_volatile) = false -> load_store_init_data m' b 0 gv.(gvar_init)). -Proof. - induction vl; simpl. - contradiction. - intros until m'; intro NEXT. - unfold alloc_variable. destruct a as [id' gv']. simpl. - set (init := gvar_init gv'). - set (sz := init_data_list_size init). - caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC. - caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ. - caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE. - caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar gv')); try congruence. - intros m4 DROP REC NOREPET IN. inv NOREPET. - exploit Mem.alloc_result; eauto. intro BEQ. - destruct IN. inversion H; subst id gv. - exists (Mem.nextblock m); split. - rewrite add_variables_same_symb; auto. unfold find_symbol; simpl. - rewrite PTree.gss. congruence. - split. rewrite add_variables_same_address. unfold find_var_info; simpl. - rewrite NEXT. apply ZMap.gss. - simpl. rewrite <- NEXT; omega. - split. red; intros. - rewrite <- BEQ. eapply alloc_variables_perm; eauto. eapply Mem.perm_drop_1; eauto. - intros NOVOL. + alloc_variable m (id, v) = Some m' -> + variables_initialized g m -> + variables_initialized (add_variable g (id, v)) m' + /\ genv_nextvar (add_variable g (id,v)) = Mem.nextblock m'. +Proof. + intros. revert H0. unfold alloc_variable. simpl. + set (il := gvar_init v). + set (sz := init_data_list_size il). + caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC. + caseEq (store_zeros m1 b1 sz); try congruence. intros m2 ZEROS. + caseEq (store_init_data_list m2 b1 0 il); try congruence. intros m3 INIT DROP. + exploit Mem.nextblock_alloc; eauto. intros NB1. + assert (Mem.nextblock m' = Mem.nextblock m1). + rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ INIT). + eapply store_zeros_nextblock; eauto. + exploit Mem.alloc_result; eauto. intro RES. + split. + (* var-init *) + red; intros. revert H2. + unfold add_variable, find_var_info; simpl. + rewrite H; rewrite <- RES. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b b1); intros VI. + (* new var *) + injection VI; intro EQ. subst b gv. clear VI. + fold il. fold sz. + split. red; intros. eapply Mem.perm_drop_1; eauto. + split. intros. + assert (0 <= ofs < sz). + eapply Mem.perm_alloc_3; eauto. + rewrite store_zeros_perm; [idtac|eauto]. + rewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. + split; auto. eapply Mem.perm_drop_2; eauto. + intros. apply load_store_init_data_invariant with m3. - intros. transitivity (Mem.load chunk m4 (Mem.nextblock m) ofs). - eapply load_alloc_variables; eauto. - red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - change (Mem.valid_block m1 (Mem.nextblock m)). rewrite <- BEQ. eauto with mem. - eapply Mem.load_drop; eauto. repeat right. - unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv'); auto with mem. - rewrite <- BEQ. eapply store_init_data_list_charact; eauto. + intros. eapply Mem.load_drop; eauto. right; right; right. + unfold perm_globvar. destruct (gvar_volatile v); try discriminate. + destruct (gvar_readonly v); auto with mem. + eapply store_init_data_list_charact; eauto. + (* older vars *) + exploit H1; eauto. intros [A [B C]]. + split. red; intros. eapply Mem.perm_drop_3; eauto. + rewrite <- store_init_data_list_perm; [idtac|eauto]. + rewrite <- store_zeros_perm; [idtac|eauto]. + eapply Mem.perm_alloc_1; eauto. + split. intros. eapply B. + eapply Mem.perm_alloc_4; eauto. + rewrite store_zeros_perm; [idtac|eauto]. + rewrite store_init_data_list_perm; [idtac|eauto]. + eapply Mem.perm_drop_4; eauto. + intros. apply load_store_init_data_invariant with m; auto. + intros. transitivity (Mem.load chunk m3 b ofs). + eapply Mem.load_drop; eauto. + transitivity (Mem.load chunk m2 b ofs). + eapply store_init_data_list_outside; eauto. + transitivity (Mem.load chunk m1 b ofs). + eapply store_zeros_outside; eauto. + eapply Mem.load_alloc_unchanged; eauto. + red. exploit genv_vars_range; eauto. rewrite <- H. omega. + rewrite H0; rewrite NB1; rewrite H; auto. +Qed. - apply IHvl with m4; auto. - simpl. - rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (store_zeros_nextblock _ _ _ STZ). - rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. +Lemma alloc_variables_initialized: + forall vl g m m', + genv_nextvar g = Mem.nextblock m -> + alloc_variables m vl = Some m' -> + variables_initialized g m -> + variables_initialized (add_variables g vl) m'. +Proof. + induction vl; simpl; intros. + inv H0; auto. + destruct (alloc_variable m a) as [m1|]_eqn; try discriminate. + destruct a as [id gv]. + exploit alloc_variable_initialized; eauto. intros [P Q]. + eapply IHvl; eauto. Qed. End INITMEM. @@ -1007,19 +1091,19 @@ Proof. red. rewrite H1. rewrite <- H3. intuition. Qed. -Theorem find_var_exists: - forall p id gv m, - list_norepet (prog_var_names p) -> - In (id, gv) (prog_vars p) -> +Theorem init_mem_characterization: + forall p b gv m, + find_var_info (globalenv p) b = Some gv -> init_mem p = Some m -> - exists b, find_symbol (globalenv p) id = Some b - /\ find_var_info (globalenv p) b = Some gv - /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv) - /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)). + Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Cur (perm_globvar gv) + /\ (forall ofs k p, Mem.perm m b ofs k p -> + 0 <= ofs < init_data_list_size gv.(gvar_init) /\ perm_order (perm_globvar gv) p) + /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p) m b 0 gv.(gvar_init)). Proof. - intros. exploit alloc_variables_charact; eauto. - instantiate (1 := Mem.empty). rewrite add_functions_nextvar. rewrite Mem.nextblock_empty; auto. - assumption. + intros. eapply alloc_variables_initialized; eauto. + rewrite add_functions_nextvar; auto. + red; intros. exploit genv_vars_range; eauto. rewrite add_functions_nextvar. + simpl. intros. omegaContradiction. Qed. (** ** Compatibility with memory injections *) @@ -1142,8 +1226,8 @@ Proof. Mem.store chunk m2 b ofs v = Some m2' -> Mem.inject (Mem.flat_inj thr) m1 m2'). intros. eapply Mem.store_outside_inject; eauto. - intros b' ? INJ'. unfold Mem.flat_inj in INJ'. - destruct (zlt b' thr); inversion INJ'; subst. omega. + intros. unfold Mem.flat_inj in H0. + destruct (zlt b' thr); inversion H0; subst. omega. destruct id; simpl in ST; try (eapply P; eauto; fail). inv ST; auto. revert ST. caseEq (find_symbol ge i); try congruence. intros; eapply P; eauto. @@ -1687,31 +1771,40 @@ Proof. rewrite H0; simpl. auto. Qed. - -(* This may not yet be in the ideal form for easy use .*) -Theorem find_new_var_exists: - list_norepet (prog_var_names p ++ var_names new_vars) -> - forall id gv m, In (id, gv) new_vars -> - init_mem p' = Some m -> - exists b, find_symbol (globalenv p') id = Some b - /\ find_var_info (globalenv p') b = Some gv - /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) (perm_globvar gv) - /\ (gv.(gvar_volatile) = false -> load_store_init_data (globalenv p') m b 0 gv.(gvar_init)). +Theorem find_new_var_exists: + forall id gv, + list_norepet (var_names new_vars) -> + In (id, gv) new_vars -> + exists b, find_symbol (globalenv p') id = Some b /\ find_var_info (globalenv p') b = Some gv. Proof. intros. - destruct p. + assert (P: forall b vars (ge: t B W), + ~In id (var_names vars) -> + find_symbol ge id = Some b + /\ find_var_info ge b = Some gv -> + find_symbol (add_variables ge vars) id = Some b + /\ find_var_info (add_variables ge vars) b = Some gv). + induction vars; simpl; intros. auto. apply IHvars. tauto. + destruct a as [id1 gv1]; unfold add_variable, find_symbol, find_var_info; simpl in *. + destruct H2; split. rewrite PTree.gso. auto. intuition. + rewrite ZMap.gso. auto. exploit genv_vars_range; eauto. unfold ZIndexed.t; omega. + + assert (Q: forall vars (ge: t B W), + list_norepet (var_names vars) -> + In (id, gv) vars -> + exists b, find_symbol (add_variables ge vars) id = Some b + /\ find_var_info (add_variables ge vars) b = Some gv). + induction vars; simpl; intros. + contradiction. + destruct a as [id1 gv1]; simpl in *. inv H1. destruct H2. inv H1. + exists (genv_nextvar ge). apply P; auto. + unfold add_variable, find_symbol, find_var_info; simpl in *. + split. apply PTree.gss. apply ZMap.gss. + apply IHvars; auto. + unfold transform_partial_augment_program in transf_OK. monadInv transf_OK. rename x into prog_funct'. rename x0 into prog_vars'. simpl in *. - assert (var_names prog_vars = var_names prog_vars'). - clear - EQ1. generalize dependent prog_vars'. induction prog_vars; intros. - simpl in EQ1. inversion EQ1; subst; auto. - simpl in EQ1. destruct a. destruct (transf_globvar transf_var g); try discriminate. monadInv EQ1. - simpl; f_equal; auto. - apply find_var_exists. - unfold prog_var_names in *; simpl in *. - rewrite var_names_app. rewrite <- H2. auto. - simpl. intuition. - auto. + unfold globalenv; simpl. repeat rewrite add_variables_app. apply Q; auto. Qed. Theorem find_var_info_rev_transf_augment: diff --git a/common/Memory.v b/common/Memory.v index 059a27e..0fc663f 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -25,9 +25,10 @@ - [alloc]: allocate a fresh memory block; - [free]: invalidate a memory block. *) - + Require Import Axioms. Require Import Coqlib. +Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. @@ -35,24 +36,7 @@ Require Import Values. Require Export Memdata. Require Export Memtype. -Definition update (A: Type) (x: Z) (v: A) (f: Z -> A) : Z -> A := - fun y => if zeq y x then v else f y. - -Implicit Arguments update [A]. - -Lemma update_s: - forall (A: Type) (x: Z) (v: A) (f: Z -> A), - update x v f x = v. -Proof. - intros; unfold update. apply zeq_true. -Qed. - -Lemma update_o: - forall (A: Type) (x: Z) (v: A) (f: Z -> A) (y: Z), - x <> y -> update x v f y = f y. -Proof. - intros; unfold update. apply zeq_false; auto. -Qed. +Local Notation "a # b" := (ZMap.get b a) (at level 1). Module Mem <: MEM. @@ -62,25 +46,31 @@ Definition perm_order' (po: option permission) (p: permission) := | None => False end. +Definition perm_order'' (po1 po2: option permission) := + match po1, po2 with + | Some p1, Some p2 => perm_order p1 p2 + | _, None => True + | None, Some _ => False + end. + Record mem' : Type := mkmem { - mem_contents: block -> Z -> memval; - mem_access: block -> Z -> option permission; - bounds: block -> Z * Z; + mem_contents: ZMap.t (ZMap.t memval); (**r [block -> offset -> memval] *) + mem_access: ZMap.t (Z -> perm_kind -> option permission); + (**r [block -> offset -> kind -> option permission] *) nextblock: block; nextblock_pos: nextblock > 0; - nextblock_noaccess: forall b, 0 < b < nextblock \/ bounds b = (0,0) ; - bounds_noaccess: forall b ofs, ofs < fst(bounds b) \/ ofs >= snd(bounds b) -> mem_access b ofs = None; - noread_undef: forall b ofs, perm_order' (mem_access b ofs) Readable \/ mem_contents b ofs = Undef + access_max: + forall b ofs, perm_order'' (mem_access#b ofs Max) (mem_access#b ofs Cur); + nextblock_noaccess: + forall b ofs k, b <= 0 \/ b >= nextblock -> mem_access#b ofs k = None }. Definition mem := mem'. Lemma mkmem_ext: - forall cont1 cont2 acc1 acc2 bound1 bound2 next1 next2 - a1 a2 b1 b2 c1 c2 d1 d2, - cont1=cont2 -> acc1=acc2 -> bound1=bound2 -> next1=next2 -> - mkmem cont1 acc1 bound1 next1 a1 b1 c1 d1 = - mkmem cont2 acc2 bound2 next2 a2 b2 c2 d2. + forall cont1 cont2 acc1 acc2 next1 next2 a1 a2 b1 b2 c1 c2, + cont1=cont2 -> acc1=acc2 -> next1=next2 -> + mkmem cont1 acc1 next1 a1 b1 c1 = mkmem cont2 acc2 next2 a2 b2 c2. Proof. intros. subst. f_equal; apply proof_irr. Qed. @@ -103,29 +93,54 @@ Hint Local Resolve valid_not_valid_diff: mem. (** Permissions *) -Definition perm (m: mem) (b: block) (ofs: Z) (p: permission) : Prop := - perm_order' (mem_access m b ofs) p. +Definition perm (m: mem) (b: block) (ofs: Z) (k: perm_kind) (p: permission) : Prop := + perm_order' (m.(mem_access)#b ofs k) p. Theorem perm_implies: - forall m b ofs p1 p2, perm m b ofs p1 -> perm_order p1 p2 -> perm m b ofs p2. + forall m b ofs k p1 p2, perm m b ofs k p1 -> perm_order p1 p2 -> perm m b ofs k p2. Proof. unfold perm, perm_order'; intros. - destruct (mem_access m b ofs); auto. + destruct (m.(mem_access)#b ofs k); auto. eapply perm_order_trans; eauto. Qed. Hint Local Resolve perm_implies: mem. +Theorem perm_cur_max: + forall m b ofs p, perm m b ofs Cur p -> perm m b ofs Max p. +Proof. + assert (forall po1 po2 p, + perm_order' po2 p -> perm_order'' po1 po2 -> perm_order' po1 p). + unfold perm_order', perm_order''. intros. + destruct po2; try contradiction. + destruct po1; try contradiction. + eapply perm_order_trans; eauto. + unfold perm; intros. + generalize (access_max m b ofs). eauto. +Qed. + +Theorem perm_cur: + forall m b ofs k p, perm m b ofs Cur p -> perm m b ofs k p. +Proof. + intros. destruct k; auto. apply perm_cur_max. auto. +Qed. + +Theorem perm_max: + forall m b ofs k p, perm m b ofs k p -> perm m b ofs Max p. +Proof. + intros. destruct k; auto. apply perm_cur_max. auto. +Qed. + +Hint Local Resolve perm_cur perm_max: mem. + Theorem perm_valid_block: - forall m b ofs p, perm m b ofs p -> valid_block m b. + forall m b ofs k p, perm m b ofs k p -> valid_block m b. Proof. unfold perm; intros. destruct (zlt b m.(nextblock)). auto. - assert (mem_access m b ofs = None). - destruct (nextblock_noaccess m b). - elimtype False; omega. - apply bounds_noaccess. rewrite H0; simpl; omega. + assert (m.(mem_access)#b ofs k = None). + eapply nextblock_noaccess; eauto. rewrite H0 in H. contradiction. Qed. @@ -147,34 +162,48 @@ Proof. Qed. Theorem perm_dec: - forall m b ofs p, {perm m b ofs p} + {~ perm m b ofs p}. + forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}. Proof. unfold perm; intros. apply perm_order'_dec. Qed. - -Definition range_perm (m: mem) (b: block) (lo hi: Z) (p: permission) : Prop := - forall ofs, lo <= ofs < hi -> perm m b ofs p. + +Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop := + forall ofs, lo <= ofs < hi -> perm m b ofs k p. Theorem range_perm_implies: - forall m b lo hi p1 p2, - range_perm m b lo hi p1 -> perm_order p1 p2 -> range_perm m b lo hi p2. + forall m b lo hi k p1 p2, + range_perm m b lo hi k p1 -> perm_order p1 p2 -> range_perm m b lo hi k p2. Proof. unfold range_perm; intros; eauto with mem. Qed. -Hint Local Resolve range_perm_implies: mem. +Theorem range_perm_cur: + forall m b lo hi k p, + range_perm m b lo hi Cur p -> range_perm m b lo hi k p. +Proof. + unfold range_perm; intros; eauto with mem. +Qed. + +Theorem range_perm_max: + forall m b lo hi k p, + range_perm m b lo hi k p -> range_perm m b lo hi Max p. +Proof. + unfold range_perm; intros; eauto with mem. +Qed. + +Hint Local Resolve range_perm_implies range_perm_cur range_perm_max: mem. Lemma range_perm_dec: - forall m b lo hi p, {range_perm m b lo hi p} + {~ range_perm m b lo hi p}. + forall m b lo hi k p, {range_perm m b lo hi k p} + {~ range_perm m b lo hi k p}. Proof. intros. assert (forall n, 0 <= n -> - {range_perm m b lo (lo + n) p} + {~ range_perm m b lo (lo + n) p}). + {range_perm m b lo (lo + n) k p} + {~ range_perm m b lo (lo + n) k p}). apply natlike_rec2. left. red; intros. omegaContradiction. intros. destruct H0. - destruct (perm_dec m b (lo + z) p). + destruct (perm_dec m b (lo + z) k p). left. red; intros. destruct (zeq ofs (lo + z)). congruence. apply r. omega. right; red; intro. elim n. apply H0. omega. right; red; intro. elim n. red; intros. apply H0. omega. @@ -185,14 +214,14 @@ Qed. (** [valid_access m chunk b ofs p] holds if a memory access of the given chunk is possible in [m] at address [b, ofs] - with permissions [p]. + with current permissions [p]. This means: -- The range of bytes accessed all have permission [p]. +- The range of bytes accessed all have current permission [p]. - The offset [ofs] is aligned. *) Definition valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) (p: permission): Prop := - range_perm m b ofs (ofs + size_chunk chunk) p + range_perm m b ofs (ofs + size_chunk chunk) Cur p /\ (align_chunk chunk | ofs). Theorem valid_access_implies: @@ -220,7 +249,7 @@ Theorem valid_access_valid_block: valid_block m b. Proof. intros. destruct H. - assert (perm m b ofs Nonempty). + assert (perm m b ofs Cur Nonempty). apply H. generalize (size_chunk_pos chunk). omega. eauto with mem. Qed. @@ -228,11 +257,11 @@ Qed. Hint Local Resolve valid_access_valid_block: mem. Lemma valid_access_perm: - forall m chunk b ofs p, + forall m chunk b ofs k p, valid_access m chunk b ofs p -> - perm m b ofs p. + perm m b ofs k p. Proof. - intros. destruct H. apply H. generalize (size_chunk_pos chunk). omega. + intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). omega. Qed. Lemma valid_access_compat: @@ -250,7 +279,7 @@ Lemma valid_access_dec: {valid_access m chunk b ofs p} + {~ valid_access m chunk b ofs p}. Proof. intros. - destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) p). + destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p). destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)). left; constructor; auto. right; red; intro V; inv V; contradiction. @@ -261,14 +290,14 @@ Qed. the byte at the given location is nonempty. *) Definition valid_pointer (m: mem) (b: block) (ofs: Z): bool := - perm_dec m b ofs Nonempty. + perm_dec m b ofs Cur Nonempty. Theorem valid_pointer_nonempty_perm: forall m b ofs, - valid_pointer m b ofs = true <-> perm m b ofs Nonempty. + valid_pointer m b ofs = true <-> perm m b ofs Cur Nonempty. Proof. intros. unfold valid_pointer. - destruct (perm_dec m b ofs Nonempty); simpl; + destruct (perm_dec m b ofs Cur Nonempty); simpl; intuition congruence. Qed. @@ -283,62 +312,23 @@ Proof. destruct H. apply H. simpl. omega. Qed. -(** Bounds *) - -(** Each block has a low bound and a high bound, determined at allocation time - and invariant afterward. The crucial properties of bounds is - that any offset below the low bound or above the high bound is - empty. *) - -Notation low_bound m b := (fst(bounds m b)). -Notation high_bound m b := (snd(bounds m b)). - -Theorem perm_in_bounds: - forall m b ofs p, perm m b ofs p -> low_bound m b <= ofs < high_bound m b. -Proof. - unfold perm. intros. - destruct (zlt ofs (fst (bounds m b))). - exploit bounds_noaccess. left; eauto. - intros. - rewrite H0 in H. contradiction. - destruct (zlt ofs (snd (bounds m b))). - omega. - exploit bounds_noaccess. right; eauto. - intro; rewrite H0 in H. contradiction. -Qed. - -Theorem range_perm_in_bounds: - forall m b lo hi p, - range_perm m b lo hi p -> lo < hi -> low_bound m b <= lo /\ hi <= high_bound m b. -Proof. - intros. split. - exploit (perm_in_bounds m b lo p). apply H. omega. omega. - exploit (perm_in_bounds m b (hi-1) p). apply H. omega. omega. -Qed. - -Theorem valid_access_in_bounds: - forall m chunk b ofs p, - valid_access m chunk b ofs p -> - low_bound m b <= ofs /\ ofs + size_chunk chunk <= high_bound m b. -Proof. - intros. inv H. apply range_perm_in_bounds with p; auto. - generalize (size_chunk_pos chunk). omega. -Qed. - -Hint Local Resolve perm_in_bounds range_perm_in_bounds valid_access_in_bounds. - -(** * Store operations *) +(** * Operations over memory stores *) (** The initial store *) Program Definition empty: mem := - mkmem (fun b ofs => Undef) - (fun b ofs => None) - (fun b => (0,0)) - 1 _ _ _ _. + mkmem (ZMap.init (ZMap.init Undef)) + (ZMap.init (fun ofs k => None)) + 1 _ _ _. Next Obligation. omega. Qed. +Next Obligation. + repeat rewrite ZMap.gi. red; auto. +Qed. +Next Obligation. + rewrite ZMap.gi. auto. +Qed. Definition nullptr: block := 0. @@ -348,108 +338,56 @@ Definition nullptr: block := 0. infinite memory. *) Program Definition alloc (m: mem) (lo hi: Z) := - (mkmem (update m.(nextblock) - (fun ofs => Undef) - m.(mem_contents)) - (update m.(nextblock) - (fun ofs => if zle lo ofs && zlt ofs hi then Some Freeable else None) - m.(mem_access)) - (update m.(nextblock) (lo, hi) m.(bounds)) + (mkmem (ZMap.set m.(nextblock) + (ZMap.init Undef) + m.(mem_contents)) + (ZMap.set m.(nextblock) + (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None) + m.(mem_access)) (Zsucc m.(nextblock)) - _ _ _ _, + _ _ _, m.(nextblock)). Next Obligation. generalize (nextblock_pos m). omega. Qed. Next Obligation. - assert (0 < b < Zsucc (nextblock m) \/ b <= 0 \/ b > nextblock m) by omega. - destruct H as [?|[?|?]]. left; omega. - right. - rewrite update_o. - destruct (nextblock_noaccess m b); auto. elimtype False; omega. - generalize (nextblock_pos m); omega. -(* generalize (bounds_noaccess m b 0).*) - destruct (nextblock_noaccess m b); auto. left; omega. - rewrite update_o. right; auto. omega. -Qed. -Next Obligation. - unfold update in *. destruct (zeq b (nextblock m)). - simpl in H. destruct H. - unfold proj_sumbool. rewrite zle_false. auto. omega. - unfold proj_sumbool. rewrite zlt_false; auto. rewrite andb_false_r. auto. - apply bounds_noaccess. auto. + repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). + subst b. destruct (zle lo ofs && zlt ofs hi); red; auto with mem. + apply access_max. Qed. Next Obligation. -unfold update. -destruct (zeq b (nextblock m)); auto. -apply noread_undef. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextblock m)). + subst b. generalize (nextblock_pos m). intros. omegaContradiction. + apply nextblock_noaccess. omega. Qed. - (** Freeing a block between the given bounds. Return the updated memory state where the given range of the given block has been invalidated: future reads and writes to this - range will fail. Requires write permission on the given range. *) - -Definition clearN (m: block -> Z -> memval) (b: block) (lo hi: Z) : - block -> Z -> memval := - fun b' ofs => if zeq b' b - then if zle lo ofs && zlt ofs hi then Undef else m b' ofs - else m b' ofs. - -Lemma clearN_in: - forall m b lo hi ofs, lo <= ofs < hi -> clearN m b lo hi b ofs = Undef. -Proof. -intros. unfold clearN. rewrite zeq_true. -destruct H; unfold andb, proj_sumbool. -rewrite zle_true; auto. rewrite zlt_true; auto. -Qed. - -Lemma clearN_out: - forall m b lo hi b' ofs, (b<>b' \/ ofs < lo \/ hi <= ofs) -> clearN m b lo hi b' ofs = m b' ofs. -Proof. -intros. unfold clearN. destruct (zeq b' b); auto. -subst b'. -destruct H. contradiction H; auto. -destruct (zle lo ofs); auto. -destruct (zlt ofs hi); auto. -elimtype False; omega. -Qed. - + range will fail. Requires freeable permission on the given range. *) Program Definition unchecked_free (m: mem) (b: block) (lo hi: Z): mem := - mkmem (clearN m.(mem_contents) b lo hi) - (update b - (fun ofs => if zle lo ofs && zlt ofs hi then None else m.(mem_access) b ofs) + mkmem m.(mem_contents) + (ZMap.set b + (fun ofs k => if zle lo ofs && zlt ofs hi then None else m.(mem_access)#b ofs k) m.(mem_access)) - m.(bounds) - m.(nextblock) _ _ _ _. + m.(nextblock) _ _ _. Next Obligation. apply nextblock_pos. Qed. Next Obligation. -apply (nextblock_noaccess m b0). + repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). + destruct (zle lo ofs && zlt ofs hi). red; auto. apply access_max. + apply access_max. Qed. Next Obligation. - unfold update. destruct (zeq b0 b). subst b0. - destruct (zle lo ofs); simpl; auto. - destruct (zlt ofs hi); simpl; auto. - apply bounds_noaccess; auto. - apply bounds_noaccess; auto. - apply bounds_noaccess; auto. -Qed. -Next Obligation. - unfold clearN, update. - destruct (zeq b0 b). subst b0. - destruct (zle lo ofs); simpl; auto. - destruct (zlt ofs hi); simpl; auto. - apply noread_undef. - apply noread_undef. - apply noread_undef. + repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst. + destruct (zle lo ofs && zlt ofs hi). auto. apply nextblock_noaccess; auto. + apply nextblock_noaccess; auto. Qed. Definition free (m: mem) (b: block) (lo hi: Z): option mem := - if range_perm_dec m b lo hi Freeable + if range_perm_dec m b lo hi Cur Freeable then Some(unchecked_free m b lo hi) else None. @@ -467,10 +405,10 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem := (** Reading N adjacent bytes in a block content. *) -Fixpoint getN (n: nat) (p: Z) (c: Z -> memval) {struct n}: list memval := +Fixpoint getN (n: nat) (p: Z) (c: ZMap.t memval) {struct n}: list memval := match n with | O => nil - | S n' => c p :: getN n' (p + 1) c + | S n' => c#p :: getN n' (p + 1) c end. (** [load chunk m b ofs] perform a read in memory state [m], at address @@ -480,7 +418,7 @@ Fixpoint getN (n: nat) (p: Z) (c: Z -> memval) {struct n}: list memval := Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val := if valid_access_dec m chunk b ofs Readable - then Some(decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents) b))) + then Some(decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b))) else None. (** [loadv chunk m addr] is similar, but the address and offset are given @@ -497,38 +435,37 @@ Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val := not readable. *) Definition loadbytes (m: mem) (b: block) (ofs n: Z): option (list memval) := - if range_perm_dec m b ofs (ofs + n) Readable - then Some (getN (nat_of_Z n) ofs (m.(mem_contents) b)) + if range_perm_dec m b ofs (ofs + n) Cur Readable + then Some (getN (nat_of_Z n) ofs (m.(mem_contents)#b)) else None. (** Memory stores. *) (** Writing N adjacent bytes in a block content. *) -Fixpoint setN (vl: list memval) (p: Z) (c: Z -> memval) {struct vl}: Z -> memval := +Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t memval := match vl with | nil => c - | v :: vl' => setN vl' (p + 1) (update p v c) + | v :: vl' => setN vl' (p + 1) (ZMap.set p v c) end. - Remark setN_other: forall vl c p q, (forall r, p <= r < p + Z_of_nat (length vl) -> r <> q) -> - setN vl p c q = c q. + (setN vl p c)#q = c#q. Proof. induction vl; intros; simpl. auto. simpl length in H. rewrite inj_S in H. - transitivity (update p a c q). - apply IHvl. intros. apply H. omega. - apply update_o. apply H. omega. + transitivity ((ZMap.set p a c)#q). + apply IHvl. intros. apply H. omega. + apply ZMap.gso. apply not_eq_sym. apply H. omega. Qed. Remark setN_outside: forall vl c p q, q < p \/ q >= p + Z_of_nat (length vl) -> - setN vl p c q = c q. + (setN vl p c)#q = c#q. Proof. intros. apply setN_other. intros. omega. @@ -541,13 +478,13 @@ Proof. induction vl; intros; simpl. auto. decEq. - rewrite setN_outside. apply update_s. omega. + rewrite setN_outside. apply ZMap.gss. omega. apply IHvl. Qed. Remark getN_exten: forall c1 c2 n p, - (forall i, p <= i < p + Z_of_nat n -> c1 i = c2 i) -> + (forall i, p <= i < p + Z_of_nat n -> c1#i = c2#i) -> getN n p c1 = getN n p c2. Proof. induction n; intros. auto. rewrite inj_S in H. simpl. decEq. @@ -562,50 +499,23 @@ Proof. intros. apply getN_exten. intros. apply setN_outside. omega. Qed. -Lemma setN_noread_undef: - forall m b ofs bytes (RP: range_perm m b ofs (ofs + Z_of_nat (length bytes)) Writable), - forall b' ofs', - perm m b' ofs' Readable \/ - update b (setN bytes ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef. -Proof. - intros. unfold update. destruct (zeq b' b). subst b'. - assert (ofs <= ofs' < ofs + Z_of_nat (length bytes) - \/ ofs' < ofs - \/ ofs' >= ofs + Z_of_nat (length bytes)) by omega. - destruct H. left. apply perm_implies with Writable; auto with mem. - rewrite setN_outside; auto. apply noread_undef; auto. - apply noread_undef; auto. -Qed. - -Lemma store_noread_undef: - forall m ch b ofs (VA: valid_access m ch b ofs Writable) v, - forall b' ofs', - perm m b' ofs' Readable \/ - update b (setN (encode_val ch v) ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef. -Proof. - intros. destruct VA. apply setN_noread_undef. - rewrite encode_val_length. rewrite <- size_chunk_conv. auto. -Qed. - (** [store chunk m b ofs v] perform a write in memory state [m]. Value [v] is stored at address [b] and offset [ofs]. Return the updated memory store, or [None] if the accessed bytes are not writable. *) Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem := - match valid_access_dec m chunk b ofs Writable with - | left VA => Some (mkmem (update b - (setN (encode_val chunk v) ofs (m.(mem_contents) b)) - m.(mem_contents)) - m.(mem_access) - m.(bounds) - m.(nextblock) - m.(nextblock_pos) - m.(nextblock_noaccess) - m.(bounds_noaccess) - (store_noread_undef m chunk b ofs VA v)) - | right _ => None - end. + if valid_access_dec m chunk b ofs Writable then + Some (mkmem (ZMap.set b + (setN (encode_val chunk v) ofs (m.(mem_contents)#b)) + m.(mem_contents)) + m.(mem_access) + m.(nextblock) + m.(nextblock_pos) + m.(access_max) + m.(nextblock_noaccess)) + else + None. (** [storev chunk m addr v] is similar, but the address and offset are given as a single value [addr], which must be a pointer value. *) @@ -621,57 +531,45 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := or [None] if the accessed locations are not writable. *) Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem := - match range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Writable with - | left RP => - Some (mkmem - (update b (setN bytes ofs (m.(mem_contents) b)) m.(mem_contents)) + if range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Cur Writable then + Some (mkmem + (ZMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents)) m.(mem_access) - m.(bounds) m.(nextblock) m.(nextblock_pos) - m.(nextblock_noaccess) - m.(bounds_noaccess) - (setN_noread_undef m b ofs bytes RP)) - | right _ => - None - end. - -(** [drop_perm m b lo hi p] sets the permissions of the byte range - [(b, lo) ... (b, hi - 1)] to [p]. These bytes must have permissions - at least [p] in the initial memory state [m]. + m.(access_max) + m.(nextblock_noaccess)) + else + None. + +(** [drop_perm m b lo hi p] sets the max permissions of the byte range + [(b, lo) ... (b, hi - 1)] to [p]. These bytes must have current permissions + [Freeable] in the initial memory state [m]. Returns updated memory state, or [None] if insufficient permissions. *) Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem := - if range_perm_dec m b lo hi p then - Some (mkmem (update b - (fun ofs => if zle lo ofs && zlt ofs hi && negb (perm_order_dec p Readable) - then Undef else m.(mem_contents) b ofs) - m.(mem_contents)) - (update b - (fun ofs => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access) b ofs) + if range_perm_dec m b lo hi Cur Freeable then + Some (mkmem m.(mem_contents) + (ZMap.set b + (fun ofs k => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access)#b ofs k) m.(mem_access)) - m.(bounds) m.(nextblock) _ _ _ _) + m.(nextblock) _ _ _) else None. Next Obligation. - destruct m; auto. + apply nextblock_pos. Qed. Next Obligation. - destruct m; auto. + repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0. + destruct (zle lo ofs && zlt ofs hi). red; auto with mem. apply access_max. + apply access_max. Qed. Next Obligation. - unfold update. destruct (zeq b0 b). subst b0. + specialize (nextblock_noaccess m b0 ofs k H0). intros. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b). subst b0. destruct (zle lo ofs). destruct (zlt ofs hi). - exploit range_perm_in_bounds; eauto. omega. intros. omegaContradiction. - simpl. eapply bounds_noaccess; eauto. - simpl. eapply bounds_noaccess; eauto. - eapply bounds_noaccess; eauto. -Qed. -Next Obligation. - unfold update. destruct (zeq b0 b). subst b0. - destruct (zle lo ofs && zlt ofs hi). - destruct (perm_order_dec p Readable); simpl; auto. - eapply noread_undef; eauto. - eapply noread_undef; eauto. + assert (perm m b ofs k Freeable). apply perm_cur. apply H; auto. + unfold perm in H2. rewrite H1 in H2. contradiction. + auto. auto. auto. Qed. (** * Properties of the memory operations *) @@ -681,14 +579,14 @@ Qed. Theorem nextblock_empty: nextblock empty = 1. Proof. reflexivity. Qed. -Theorem perm_empty: forall b ofs p, ~perm empty b ofs p. +Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p. Proof. - intros. unfold perm, empty; simpl. congruence. + intros. unfold perm, empty; simpl. rewrite ZMap.gi. simpl. tauto. Qed. Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. Proof. - intros. red; intros. elim (perm_empty b ofs p). apply H. + intros. red; intros. elim (perm_empty b ofs Cur p). apply H. generalize (size_chunk_pos chunk); omega. Qed. @@ -716,7 +614,7 @@ Qed. Lemma load_result: forall chunk m b ofs v, load chunk m b ofs = Some v -> - v = decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents) b)). + v = decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b)). Proof. intros until v. unfold load. destruct (valid_access_dec m chunk b ofs Readable); intros. @@ -748,7 +646,7 @@ Theorem load_cast: end. Proof. intros. exploit load_result; eauto. - set (l := getN (size_chunk_nat chunk) ofs (mem_contents m b)). + set (l := getN (size_chunk_nat chunk) ofs m.(mem_contents)#b). intros. subst v. apply decode_val_cast. Qed. @@ -758,7 +656,7 @@ Theorem load_int8_signed_unsigned: Proof. intros. unfold load. change (size_chunk_nat Mint8signed) with (size_chunk_nat Mint8unsigned). - set (cl := getN (size_chunk_nat Mint8unsigned) ofs (mem_contents m b)). + set (cl := getN (size_chunk_nat Mint8unsigned) ofs m.(mem_contents)#b). destruct (valid_access_dec m Mint8signed b ofs Readable). rewrite pred_dec_true; auto. unfold decode_val. destruct (proj_bytes cl); auto. rewrite decode_int8_signed_unsigned. auto. @@ -771,7 +669,7 @@ Theorem load_int16_signed_unsigned: Proof. intros. unfold load. change (size_chunk_nat Mint16signed) with (size_chunk_nat Mint16unsigned). - set (cl := getN (size_chunk_nat Mint16unsigned) ofs (mem_contents m b)). + set (cl := getN (size_chunk_nat Mint16unsigned) ofs m.(mem_contents)#b). destruct (valid_access_dec m Mint16signed b ofs Readable). rewrite pred_dec_true; auto. unfold decode_val. destruct (proj_bytes cl); auto. rewrite decode_int16_signed_unsigned. auto. @@ -782,7 +680,7 @@ Qed. Theorem range_perm_loadbytes: forall m b ofs len, - range_perm m b ofs (ofs + len) Readable -> + range_perm m b ofs (ofs + len) Cur Readable -> exists bytes, loadbytes m b ofs len = Some bytes. Proof. intros. econstructor. unfold loadbytes. rewrite pred_dec_true; eauto. @@ -791,10 +689,10 @@ Qed. Theorem loadbytes_range_perm: forall m b ofs len bytes, loadbytes m b ofs len = Some bytes -> - range_perm m b ofs (ofs + len) Readable. + range_perm m b ofs (ofs + len) Cur Readable. Proof. intros until bytes. unfold loadbytes. - destruct (range_perm_dec m b ofs (ofs + len) Readable). auto. congruence. + destruct (range_perm_dec m b ofs (ofs + len) Cur Readable). auto. congruence. Qed. Theorem loadbytes_load: @@ -804,7 +702,7 @@ Theorem loadbytes_load: load chunk m b ofs = Some(decode_val chunk bytes). Proof. unfold loadbytes, load; intros. - destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Readable); + destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur Readable); try congruence. inv H. rewrite pred_dec_true. auto. split; auto. @@ -818,7 +716,7 @@ Theorem load_loadbytes: Proof. intros. exploit load_valid_access; eauto. intros [A B]. exploit load_result; eauto. intros. - exists (getN (size_chunk_nat chunk) ofs (mem_contents m b)); split. + exists (getN (size_chunk_nat chunk) ofs m.(mem_contents)#b); split. unfold loadbytes. rewrite pred_dec_true; auto. auto. Qed. @@ -835,7 +733,7 @@ Theorem loadbytes_length: length bytes = nat_of_Z n. Proof. unfold loadbytes; intros. - destruct (range_perm_dec m b ofs (ofs + n) Readable); try congruence. + destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); try congruence. inv H. apply getN_length. Qed. @@ -866,8 +764,8 @@ Theorem loadbytes_concat: loadbytes m b ofs (n1 + n2) = Some(bytes1 ++ bytes2). Proof. unfold loadbytes; intros. - destruct (range_perm_dec m b ofs (ofs + n1) Readable); try congruence. - destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Readable); try congruence. + destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence. + destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence. rewrite pred_dec_true. rewrite nat_of_Z_plus; auto. rewrite getN_concat. rewrite nat_of_Z_eq; auto. congruence. @@ -886,7 +784,7 @@ Theorem loadbytes_split: /\ bytes = bytes1 ++ bytes2. Proof. unfold loadbytes; intros. - destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Readable); + destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable); try congruence. rewrite nat_of_Z_plus in H; auto. rewrite getN_concat in H. rewrite nat_of_Z_eq in H; auto. @@ -899,28 +797,28 @@ Qed. Theorem load_rep: forall ch m1 m2 b ofs v1 v2, - (forall z, 0 <= z < size_chunk ch -> mem_contents m1 b (ofs+z) = mem_contents m2 b (ofs+z)) -> + (forall z, 0 <= z < size_chunk ch -> m1.(mem_contents)#b#(ofs+z) = m2.(mem_contents)#b#(ofs+z)) -> load ch m1 b ofs = Some v1 -> load ch m2 b ofs = Some v2 -> v1 = v2. Proof. -intros. -apply load_result in H0. -apply load_result in H1. -subst. -f_equal. -rewrite size_chunk_conv in H. -remember (size_chunk_nat ch) as n; clear Heqn. -revert ofs H; induction n; intros; simpl; auto. -f_equal. -rewrite inj_S in H. -replace ofs with (ofs+0) by omega. -apply H; omega. -apply IHn. -intros. -rewrite <- Zplus_assoc. -apply H. -rewrite inj_S. omega. + intros. + apply load_result in H0. + apply load_result in H1. + subst. + f_equal. + rewrite size_chunk_conv in H. + remember (size_chunk_nat ch) as n; clear Heqn. + revert ofs H; induction n; intros; simpl; auto. + f_equal. + rewrite inj_S in H. + replace ofs with (ofs+0) by omega. + apply H; omega. + apply IHn. + intros. + rewrite <- Zplus_assoc. + apply H. + rewrite inj_S. omega. Qed. (** ** Properties related to [store] *) @@ -954,27 +852,27 @@ Proof. auto. Qed. -Lemma store_mem_contents: mem_contents m2 = - update b (setN (encode_val chunk v) ofs (m1.(mem_contents) b)) m1.(mem_contents). +Lemma store_mem_contents: + mem_contents m2 = ZMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents). Proof. unfold store in STORE. destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE. auto. Qed. Theorem perm_store_1: - forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p. + forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p. Proof. intros. unfold perm in *. rewrite store_access; auto. Qed. Theorem perm_store_2: - forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p. + forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p. Proof. intros. unfold perm in *. rewrite store_access in H; auto. Qed. -Hint Local Resolve perm_store_1 perm_store_2: mem. +Local Hint Resolve perm_store_1 perm_store_2: mem. Theorem nextblock_store: nextblock m2 = nextblock m1. @@ -996,7 +894,7 @@ Proof. unfold valid_block; intros. rewrite nextblock_store in H; auto. Qed. -Hint Local Resolve store_valid_block_1 store_valid_block_2: mem. +Local Hint Resolve store_valid_block_1 store_valid_block_2: mem. Theorem store_valid_access_1: forall chunk' b' ofs' p, @@ -1020,16 +918,7 @@ Proof. congruence. Qed. -Hint Local Resolve store_valid_access_1 store_valid_access_2 - store_valid_access_3: mem. - -Theorem bounds_store: - forall b', bounds m2 b' = bounds m1 b'. -Proof. - intros. - unfold store in STORE. - destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE. simpl. auto. -Qed. +Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem. Theorem load_store_similar: forall chunk', @@ -1043,7 +932,7 @@ Proof. exists v'; split; auto. exploit load_result; eauto. intros B. rewrite B. rewrite store_mem_contents; simpl. - rewrite update_s. + rewrite ZMap.gss. replace (size_chunk_nat chunk') with (length (encode_val chunk v)). rewrite getN_setN_same. apply decode_encode_val_general. rewrite encode_val_length. repeat rewrite size_chunk_conv in H. @@ -1070,7 +959,7 @@ Proof. destruct (valid_access_dec m1 chunk' b' ofs' Readable). rewrite pred_dec_true. decEq. decEq. rewrite store_mem_contents; simpl. - unfold update. destruct (zeq b' b). subst b'. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. apply getN_setN_outside. rewrite encode_val_length. repeat rewrite <- size_chunk_conv. intuition. auto. @@ -1085,9 +974,8 @@ Proof. intros. assert (valid_access m2 chunk b ofs Readable) by eauto with mem. unfold loadbytes. rewrite pred_dec_true. rewrite store_mem_contents; simpl. - rewrite update_s. - replace (nat_of_Z (size_chunk chunk)) - with (length (encode_val chunk v)). + rewrite ZMap.gss. + replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)). rewrite getN_setN_same. auto. rewrite encode_val_length. auto. apply H. @@ -1102,10 +990,10 @@ Theorem loadbytes_store_other: loadbytes m2 b' ofs' n = loadbytes m1 b' ofs' n. Proof. intros. unfold loadbytes. - destruct (range_perm_dec m1 b' ofs' (ofs' + n) Readable). + destruct (range_perm_dec m1 b' ofs' (ofs' + n) Cur Readable). rewrite pred_dec_true. decEq. rewrite store_mem_contents; simpl. - unfold update. destruct (zeq b' b). subst b'. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. destruct H. congruence. destruct (zle n 0). rewrite (nat_of_Z_neg _ z). auto. @@ -1122,12 +1010,12 @@ Lemma setN_property: forall (P: memval -> Prop) vl p q c, (forall v, In v vl -> P v) -> p <= q < p + Z_of_nat (length vl) -> - P(setN vl p c q). + P((setN vl p c)#q). Proof. induction vl; intros. simpl in H0. omegaContradiction. simpl length in H0. rewrite inj_S in H0. simpl. - destruct (zeq p q). subst q. rewrite setN_outside. rewrite update_s. + destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss. auto with coqlib. omega. apply IHvl. auto with coqlib. omega. Qed. @@ -1135,7 +1023,7 @@ Qed. Lemma getN_in: forall c q n p, p <= q < p + Z_of_nat n -> - In (c q) (getN n p c). + In (c#q) (getN n p c). Proof. induction n; intros. simpl in H; omegaContradiction. @@ -1151,14 +1039,14 @@ Theorem load_pointer_store: \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs'). Proof. intros. exploit load_result; eauto. rewrite store_mem_contents; simpl. - unfold update. destruct (zeq b' b); auto. subst b'. intro DEC. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b); auto. subst b'. intro DEC. destruct (zle (ofs' + size_chunk chunk') ofs); auto. destruct (zle (ofs + size_chunk chunk) ofs'); auto. destruct (size_chunk_nat_pos chunk) as [sz SZ]. destruct (size_chunk_nat_pos chunk') as [sz' SZ']. exploit decode_pointer_shape; eauto. intros [CHUNK' PSHAPE]. clear CHUNK'. generalize (encode_val_shape chunk v). intro VSHAPE. - set (c := mem_contents m1 b) in *. + set (c := m1.(mem_contents)#b) in *. set (c' := setN (encode_val chunk v) ofs c) in *. destruct (zeq ofs ofs'). @@ -1167,7 +1055,7 @@ Proof. exploit decode_val_pointer_inv; eauto. intros [A B]. subst chunk'. simpl in B. inv B. generalize H4. unfold c'. rewrite <- H0. simpl. - rewrite setN_outside; try omega. rewrite update_s. intros. + rewrite setN_outside; try omega. rewrite ZMap.gss. intros. exploit (encode_val_pointer_inv chunk v v_b v_o). rewrite <- H0. subst mv1. eauto. intros [C [D E]]. left; auto. @@ -1184,9 +1072,9 @@ Proof. For the read to return a pointer, it must satisfy ~memval_valid_cont. *) elimtype False. - assert (~memval_valid_cont (c' ofs')). + assert (~memval_valid_cont (c'#ofs')). rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. auto. - assert (memval_valid_cont (c' ofs')). + assert (memval_valid_cont (c'#ofs')). inv VSHAPE. unfold c'. rewrite <- H1. simpl. apply setN_property. auto. assert (length mvl = sz). @@ -1205,10 +1093,10 @@ Proof. For the read to return a pointer, it must satisfy ~memval_valid_first. *) elimtype False. - assert (memval_valid_first (c' ofs)). + assert (memval_valid_first (c'#ofs)). inv VSHAPE. unfold c'. rewrite <- H0. simpl. - rewrite setN_outside. rewrite update_s. auto. omega. - assert (~memval_valid_first (c' ofs)). + rewrite setN_outside. rewrite ZMap.gss. auto. omega. + assert (~memval_valid_first (c'#ofs)). rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. apply H4. apply getN_in. rewrite size_chunk_conv in z. rewrite SZ' in z. rewrite inj_S in z. omega. @@ -1217,9 +1105,9 @@ Qed. End STORE. -Hint Local Resolve perm_store_1 perm_store_2: mem. -Hint Local Resolve store_valid_block_1 store_valid_block_2: mem. -Hint Local Resolve store_valid_access_1 store_valid_access_2 +Local Hint Resolve perm_store_1 perm_store_2: mem. +Local Hint Resolve store_valid_block_1 store_valid_block_2: mem. +Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem. Theorem load_store_pointer_overlap: @@ -1237,8 +1125,8 @@ Proof. rewrite LD; clear LD. Opaque encode_val. rewrite ST; simpl. - rewrite update_s. - set (c := mem_contents m1 b). + rewrite ZMap.gss. + set (c := m1.(mem_contents)#b). set (c' := setN (encode_val chunk (Vptr v_b v_o)) ofs c). destruct (decode_val_shape chunk' (getN (size_chunk_nat chunk') ofs' c')) as [OK | VSHAPE]. @@ -1265,9 +1153,9 @@ Opaque encode_val. The byte at ofs' is Undef or not memval_valid_first (because write of pointer). The byte at ofs' must be memval_valid_first and not Undef (otherwise load returns Vundef). *) - assert (memval_valid_first (c' ofs') /\ c' ofs' <> Undef). + assert (memval_valid_first (c'#ofs') /\ c'#ofs' <> Undef). rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. auto. - assert (~memval_valid_first (c' ofs') \/ c' ofs' = Undef). + assert (~memval_valid_first (c'#ofs') \/ c'#ofs' = Undef). unfold c'. destruct ENC. right. apply setN_property. rewrite H5. intros. eapply in_list_repeat; eauto. rewrite encode_val_length. rewrite <- size_chunk_conv. omega. @@ -1285,11 +1173,11 @@ Opaque encode_val. The byte at ofs is Undef or not memval_valid_cont (because write of pointer). The byte at ofs must be memval_valid_cont and not Undef (otherwise load returns Vundef). *) - assert (memval_valid_cont (c' ofs) /\ c' ofs <> Undef). + assert (memval_valid_cont (c'#ofs) /\ c'#ofs <> Undef). rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. apply H8. apply getN_in. rewrite size_chunk_conv in H2. rewrite SZ' in H2. rewrite inj_S in H2. omega. - assert (~memval_valid_cont (c' ofs) \/ c' ofs = Undef). + assert (~memval_valid_cont (c'#ofs) \/ c'#ofs = Undef). elim ENC. rewrite <- GET. rewrite SZ. simpl. intros. right; congruence. rewrite <- GET. rewrite SZ. simpl. intros. inv H5. auto. @@ -1309,8 +1197,8 @@ Proof. rewrite LD; clear LD. Opaque encode_val. rewrite ST; simpl. - rewrite update_s. - set (c1 := mem_contents m1 b). + rewrite ZMap.gss. + set (c1 := m1.(mem_contents)#b). set (e := encode_val chunk (Vptr v_b v_o)). destruct (size_chunk_nat_pos chunk) as [sz SZ]. destruct (size_chunk_nat_pos chunk') as [sz' SZ']. @@ -1322,7 +1210,7 @@ Opaque encode_val. Transparent encode_val. unfold e, encode_val. rewrite SZ. destruct chunk; simpl; auto. destruct e as [ | e1 el]. contradiction. - rewrite SZ'. simpl. rewrite setN_outside. rewrite update_s. + rewrite SZ'. simpl. rewrite setN_outside. rewrite ZMap.gss. destruct e1; try contradiction. destruct chunk'; auto. destruct chunk'; auto. intuition. @@ -1350,7 +1238,6 @@ Proof. destruct chunk1; destruct chunk2; inv H0; unfold valid_access, align_chunk in *; try contradiction. Qed. - Theorem store_signed_unsigned_8: forall m b ofs v, store Mint8signed m b ofs v = store Mint8unsigned m b ofs v. @@ -1395,22 +1282,12 @@ Proof. intros. apply store_similar_chunks. simpl. decEq. apply encode_float32_ca Theorem range_perm_storebytes: forall m1 b ofs bytes, - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable -> + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable -> { m2 : mem | storebytes m1 b ofs bytes = Some m2 }. Proof. - intros. - exists (mkmem - (update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents)) - m1.(mem_access) - m1.(bounds) - m1.(nextblock) - m1.(nextblock_pos) - m1.(nextblock_noaccess) - m1.(bounds_noaccess) - (setN_noread_undef m1 b ofs bytes H)). - unfold storebytes. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable). - decEq. decEq. apply proof_irr. + intros. econstructor. unfold storebytes. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable). + reflexivity. contradiction. Qed. @@ -1421,9 +1298,9 @@ Theorem storebytes_store: store chunk m1 b ofs v = Some m2. Proof. unfold storebytes, store. intros. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable); inv H. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable); inv H. destruct (valid_access_dec m1 chunk b ofs Writable). - decEq. decEq. apply proof_irr. + auto. elim n. constructor; auto. rewrite encode_val_length in r. rewrite size_chunk_conv. auto. Qed. @@ -1435,21 +1312,11 @@ Theorem store_storebytes: Proof. unfold storebytes, store. intros. destruct (valid_access_dec m1 chunk b ofs Writable); inv H. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable). - decEq. decEq. apply proof_irr. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable). + auto. destruct v0. elim n. rewrite encode_val_length. rewrite <- size_chunk_conv. auto. Qed. - -Theorem storebytes_empty: - forall m b ofs, storebytes m b ofs nil = Some m. -Proof. - intros. unfold storebytes. simpl. - destruct (range_perm_dec m b ofs (ofs + 0) Writable). - decEq. destruct m; simpl; apply mkmem_ext; auto. - apply extensionality. unfold update; intros. destruct (zeq x b); congruence. - elim n. red; intros; omegaContradiction. -Qed. Section STOREBYTES. Variable m1: mem. @@ -1462,33 +1329,33 @@ Hypothesis STORE: storebytes m1 b ofs bytes = Some m2. Lemma storebytes_access: mem_access m2 = mem_access m1. Proof. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. Lemma storebytes_mem_contents: - mem_contents m2 = update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents). + mem_contents m2 = ZMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents). Proof. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. Theorem perm_storebytes_1: - forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p. + forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p. Proof. intros. unfold perm in *. rewrite storebytes_access; auto. Qed. Theorem perm_storebytes_2: - forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p. + forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p. Proof. intros. unfold perm in *. rewrite storebytes_access in H; auto. Qed. -Hint Local Resolve perm_storebytes_1 perm_storebytes_2: mem. +Local Hint Resolve perm_storebytes_1 perm_storebytes_2: mem. Theorem storebytes_valid_access_1: forall chunk' b' ofs' p, @@ -1504,14 +1371,14 @@ Proof. intros. inv H. constructor; try red; auto with mem. Qed. -Hint Local Resolve storebytes_valid_access_1 storebytes_valid_access_2: mem. +Local Hint Resolve storebytes_valid_access_1 storebytes_valid_access_2: mem. Theorem nextblock_storebytes: nextblock m2 = nextblock m1. Proof. intros. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. @@ -1528,24 +1395,14 @@ Proof. unfold valid_block; intros. rewrite nextblock_storebytes in H; auto. Qed. -Hint Local Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem. +Local Hint Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem. Theorem storebytes_range_perm: - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable. + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable. Proof. intros. unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); - inv STORE. - auto. -Qed. - -Theorem bounds_storebytes: - forall b', bounds m2 b' = bounds m1 b'. -Proof. - intros. - unfold storebytes in STORE. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); inv STORE. auto. Qed. @@ -1554,10 +1411,10 @@ Theorem loadbytes_storebytes_same: loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. Proof. intros. unfold storebytes in STORE. unfold loadbytes. - destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); try discriminate. rewrite pred_dec_true. - decEq. inv STORE; simpl. rewrite update_s. rewrite nat_of_Z_of_nat. + decEq. inv STORE; simpl. rewrite ZMap.gss. rewrite nat_of_Z_of_nat. apply getN_setN_same. red; eauto with mem. Qed. @@ -1571,10 +1428,10 @@ Theorem loadbytes_storebytes_other: loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. Proof. intros. unfold loadbytes. - destruct (range_perm_dec m1 b' ofs' (ofs' + len) Readable). + destruct (range_perm_dec m1 b' ofs' (ofs' + len) Cur Readable). rewrite pred_dec_true. rewrite storebytes_mem_contents. decEq. - unfold update. destruct (zeq b' b). subst b'. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. apply getN_setN_outside. rewrite nat_of_Z_eq; auto. intuition congruence. auto. red; auto with mem. @@ -1592,8 +1449,8 @@ Proof. intros. unfold load. destruct (valid_access_dec m1 chunk b' ofs' Readable). rewrite pred_dec_true. - rewrite storebytes_mem_contents. decEq. - unfold update. destruct (zeq b' b). subst b'. + rewrite storebytes_mem_contents. decEq. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence. auto. destruct v; split; auto. red; auto with mem. @@ -1620,12 +1477,11 @@ Theorem storebytes_concat: Proof. intros. generalize H; intro ST1. generalize H0; intro ST2. unfold storebytes; unfold storebytes in ST1; unfold storebytes in ST2. - destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Writable); try congruence. - destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Writable); try congruence. - destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Writable). + destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Cur Writable); try congruence. + destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Cur Writable); try congruence. + destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Cur Writable). inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto. - apply extensionality; intros. unfold update. destruct (zeq x b); auto. - subst x. rewrite zeq_true. apply setN_concat. + rewrite ZMap.gss. rewrite setN_concat. symmetry. apply ZMap.set2. elim n. rewrite app_length. rewrite inj_plus. red; intros. destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))). @@ -1694,7 +1550,7 @@ Proof. unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. omega. Qed. -Hint Local Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. +Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. Theorem valid_block_alloc_inv: forall b', valid_block m2 b' -> b' = b \/ valid_block m1 b'. @@ -1705,49 +1561,47 @@ Proof. Qed. Theorem perm_alloc_1: - forall b' ofs p, perm m1 b' ofs p -> perm m2 b' ofs p. + forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p. Proof. unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl. - subst b. unfold update. destruct (zeq b' (nextblock m1)); auto. - elimtype False. - destruct (nextblock_noaccess m1 b'). - omega. - rewrite bounds_noaccess in H. contradiction. rewrite H0. simpl; omega. + subst b. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' (nextblock m1)); auto. + rewrite nextblock_noaccess in H. contradiction. omega. Qed. Theorem perm_alloc_2: - forall ofs, lo <= ofs < hi -> perm m2 b ofs Freeable. + forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable. Proof. unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl. - subst b. rewrite update_s. unfold proj_sumbool. rewrite zle_true. + subst b. rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. auto with mem. omega. omega. Qed. -Theorem perm_alloc_3: - forall ofs p, ofs < lo \/ hi <= ofs -> ~perm m2 b ofs p. -Proof. - unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl. - subst b. rewrite update_s. unfold proj_sumbool. - destruct H. rewrite zle_false. simpl. congruence. omega. - rewrite zlt_false. rewrite andb_false_r. - intro; contradiction. - omega. -Qed. - -Hint Local Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3: mem. - Theorem perm_alloc_inv: - forall b' ofs p, - perm m2 b' ofs p -> - if zeq b' b then lo <= ofs < hi else perm m1 b' ofs p. + forall b' ofs k p, + perm m2 b' ofs k p -> + if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p. Proof. intros until p; unfold perm. inv ALLOC. simpl. - unfold update. destruct (zeq b' (nextblock m1)); intros. + rewrite ZMap.gsspec. unfold ZIndexed.eq. destruct (zeq b' (nextblock m1)); intros. destruct (zle lo ofs); try contradiction. destruct (zlt ofs hi); try contradiction. split; auto. auto. Qed. +Theorem perm_alloc_3: + forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi. +Proof. + intros. exploit perm_alloc_inv; eauto. rewrite zeq_true; auto. +Qed. + +Theorem perm_alloc_4: + forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p. +Proof. + intros. exploit perm_alloc_inv; eauto. rewrite zeq_false; auto. +Qed. + +Local Hint Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3 perm_alloc_4: mem. + Theorem valid_access_alloc_other: forall chunk b' ofs p, valid_access m1 chunk b' ofs p -> @@ -1766,7 +1620,7 @@ Proof. red; intros. apply perm_alloc_2. omega. Qed. -Hint Local Resolve valid_access_alloc_other valid_access_alloc_same: mem. +Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. Theorem valid_access_alloc_inv: forall chunk b' ofs p, @@ -1778,8 +1632,8 @@ Proof. intros. inv H. generalize (size_chunk_pos chunk); intro. unfold eq_block. destruct (zeq b' b). subst b'. - assert (perm m2 b ofs p). apply H0. omega. - assert (perm m2 b (ofs + size_chunk chunk - 1) p). apply H0. omega. + assert (perm m2 b ofs Cur p). apply H0. omega. + assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. omega. exploit perm_alloc_inv. eexact H2. rewrite zeq_true. intro. exploit perm_alloc_inv. eexact H3. rewrite zeq_true. intro. intuition omega. @@ -1787,25 +1641,6 @@ Proof. exploit perm_alloc_inv. apply H0. eauto. rewrite zeq_false; auto. Qed. -Theorem bounds_alloc: - forall b', bounds m2 b' = if eq_block b' b then (lo, hi) else bounds m1 b'. -Proof. - injection ALLOC; intros. rewrite <- H; rewrite <- H0; simpl. - unfold update. auto. -Qed. - -Theorem bounds_alloc_same: - bounds m2 b = (lo, hi). -Proof. - rewrite bounds_alloc. apply dec_eq_true. -Qed. - -Theorem bounds_alloc_other: - forall b', b' <> b -> bounds m2 b' = bounds m1 b'. -Proof. - intros. rewrite bounds_alloc. apply dec_eq_false. auto. -Qed. - Theorem load_alloc_unchanged: forall chunk b' ofs, valid_block m1 b' -> @@ -1817,7 +1652,7 @@ Proof. subst b'. elimtype False. eauto with mem. rewrite pred_dec_true; auto. injection ALLOC; intros. rewrite <- H2; simpl. - rewrite update_o. auto. rewrite H1. apply sym_not_equal; eauto with mem. + rewrite ZMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem. rewrite pred_dec_false. auto. eauto with mem. Qed. @@ -1837,7 +1672,7 @@ Theorem load_alloc_same: Proof. intros. exploit load_result; eauto. intro. rewrite H0. injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1. - rewrite update_s. destruct chunk; reflexivity. + rewrite ZMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity. Qed. Theorem load_alloc_same': @@ -1854,14 +1689,14 @@ Qed. End ALLOC. -Hint Local Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. -Hint Local Resolve valid_access_alloc_other valid_access_alloc_same: mem. +Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. +Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. (** ** Properties related to [free]. *) Theorem range_perm_free: forall m1 b lo hi, - range_perm m1 b lo hi Freeable -> + range_perm m1 b lo hi Cur Freeable -> { m2: mem | free m1 b lo hi = Some m2 }. Proof. intros; unfold free. rewrite pred_dec_true; auto. econstructor; eauto. @@ -1876,16 +1711,16 @@ Variable m2: mem. Hypothesis FREE: free m1 bf lo hi = Some m2. Theorem free_range_perm: - range_perm m1 bf lo hi Freeable. + range_perm m1 bf lo hi Cur Freeable. Proof. - unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Freeable); auto. + unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Cur Freeable); auto. congruence. Qed. Lemma free_result: m2 = unchecked_free m1 bf lo hi. Proof. - unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Freeable). + unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Cur Freeable). congruence. congruence. Qed. @@ -1907,16 +1742,16 @@ Proof. intros. rewrite free_result in H. assumption. Qed. -Hint Local Resolve valid_block_free_1 valid_block_free_2: mem. +Local Hint Resolve valid_block_free_1 valid_block_free_2: mem. Theorem perm_free_1: - forall b ofs p, + forall b ofs k p, b <> bf \/ ofs < lo \/ hi <= ofs -> - perm m1 b ofs p -> - perm m2 b ofs p. + perm m1 b ofs k p -> + perm m2 b ofs k p. Proof. intros. rewrite free_result. unfold perm, unchecked_free; simpl. - unfold update. destruct (zeq b bf). subst b. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b. destruct (zle lo ofs); simpl. destruct (zlt ofs hi); simpl. elimtype False; intuition. @@ -1925,22 +1760,33 @@ Proof. Qed. Theorem perm_free_2: - forall ofs p, lo <= ofs < hi -> ~ perm m2 bf ofs p. + forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p. Proof. intros. rewrite free_result. unfold perm, unchecked_free; simpl. - rewrite update_s. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. - simpl. congruence. omega. omega. + rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. + simpl. tauto. omega. omega. Qed. Theorem perm_free_3: - forall b ofs p, - perm m2 b ofs p -> perm m1 b ofs p. + forall b ofs k p, + perm m2 b ofs k p -> perm m1 b ofs k p. Proof. intros until p. rewrite free_result. unfold perm, unchecked_free; simpl. - unfold update. destruct (zeq b bf). subst b. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b. destruct (zle lo ofs); simpl. - destruct (zlt ofs hi); simpl. intro; contradiction. - congruence. auto. auto. + destruct (zlt ofs hi); simpl. tauto. + auto. auto. auto. +Qed. + +Theorem perm_free_inv: + forall b ofs k p, + perm m1 b ofs k p -> + (b = bf /\ lo <= ofs < hi) \/ perm m2 b ofs k p. +Proof. + intros. rewrite free_result. unfold perm, unchecked_free; simpl. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf); auto. subst b. + destruct (zle lo ofs); simpl; auto. + destruct (zlt ofs hi); simpl; auto. Qed. Theorem valid_access_free_1: @@ -1962,9 +1808,9 @@ Proof. intros; red; intros. inv H2. generalize (size_chunk_pos chunk); intros. destruct (zlt ofs lo). - elim (perm_free_2 lo p). + elim (perm_free_2 lo Cur p). omega. apply H3. omega. - elim (perm_free_2 ofs p). + elim (perm_free_2 ofs Cur p). omega. apply H3. omega. Qed. @@ -1976,10 +1822,10 @@ Proof. intros. destruct H. split; auto. red; intros. generalize (H ofs0 H1). rewrite free_result. unfold perm, unchecked_free; simpl. - unfold update. destruct (zeq b bf). subst b. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b bf). subst b. destruct (zle lo ofs0); simpl. - destruct (zlt ofs0 hi); simpl. - intro; contradiction. congruence. auto. auto. + destruct (zlt ofs0 hi); simpl. + tauto. auto. auto. auto. Qed. Theorem valid_access_free_inv_2: @@ -1994,12 +1840,6 @@ Proof. elim (valid_access_free_2 chunk ofs p); auto. omega. Qed. -Theorem bounds_free: - forall b, bounds m2 b = bounds m1 b. -Proof. - intros. rewrite free_result; simpl. auto. -Qed. - Theorem load_free: forall chunk b ofs, b <> bf \/ lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs -> @@ -2009,51 +1849,32 @@ Proof. destruct (valid_access_dec m2 chunk b ofs Readable). rewrite pred_dec_true. rewrite free_result; auto. - simpl. f_equal. f_equal. - unfold clearN. - rewrite size_chunk_conv in H. - remember (size_chunk_nat chunk) as n; clear Heqn. - clear v FREE. - revert lo hi ofs H; induction n; intros; simpl; auto. - f_equal. - destruct (zeq b bf); auto. subst bf. - destruct (zle lo ofs); auto. destruct (zlt ofs hi); auto. - elimtype False. - destruct H as [? | [? | [? | ?]]]; try omega. - contradict H; auto. - rewrite inj_S in H; omega. - apply IHn. - rewrite inj_S in H. - destruct H as [? | [? | [? | ?]]]; auto. - unfold block in *; omega. - unfold block in *; omega. - - apply valid_access_free_inv_1; auto. + eapply valid_access_free_inv_1; eauto. rewrite pred_dec_false; auto. red; intro; elim n. eapply valid_access_free_1; eauto. Qed. End FREE. -Hint Local Resolve valid_block_free_1 valid_block_free_2 +Local Hint Resolve valid_block_free_1 valid_block_free_2 perm_free_1 perm_free_2 perm_free_3 valid_access_free_1 valid_access_free_inv_1: mem. (** ** Properties related to [drop_perm] *) Theorem range_perm_drop_1: - forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> range_perm m b lo hi p. + forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> range_perm m b lo hi Cur Freeable. Proof. unfold drop_perm; intros. - destruct (range_perm_dec m b lo hi p). auto. discriminate. + destruct (range_perm_dec m b lo hi Cur Freeable). auto. discriminate. Qed. Theorem range_perm_drop_2: forall m b lo hi p, - range_perm m b lo hi p -> {m' | drop_perm m b lo hi p = Some m' }. + range_perm m b lo hi Cur Freeable -> {m' | drop_perm m b lo hi p = Some m' }. Proof. unfold drop_perm; intros. - destruct (range_perm_dec m b lo hi p). econstructor. eauto. contradiction. + destruct (range_perm_dec m b lo hi Cur Freeable). econstructor. eauto. contradiction. Qed. Section DROP. @@ -2068,59 +1889,64 @@ Hypothesis DROP: drop_perm m b lo hi p = Some m'. Theorem nextblock_drop: nextblock m' = nextblock m. Proof. - unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP; auto. + unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP; auto. +Qed. + +Theorem drop_perm_valid_block_1: + forall b', valid_block m b' -> valid_block m' b'. +Proof. + unfold valid_block; rewrite nextblock_drop; auto. +Qed. + +Theorem drop_perm_valid_block_2: + forall b', valid_block m' b' -> valid_block m b'. +Proof. + unfold valid_block; rewrite nextblock_drop; auto. Qed. Theorem perm_drop_1: - forall ofs, lo <= ofs < hi -> perm m' b ofs p. + forall ofs k, lo <= ofs < hi -> perm m' b ofs k p. Proof. intros. - unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. - unfold perm. simpl. rewrite update_s. unfold proj_sumbool. + unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. + unfold perm. simpl. rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. constructor. omega. omega. Qed. Theorem perm_drop_2: - forall ofs p', lo <= ofs < hi -> perm m' b ofs p' -> perm_order p p'. + forall ofs k p', lo <= ofs < hi -> perm m' b ofs k p' -> perm_order p p'. Proof. intros. - unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. - revert H0. unfold perm; simpl. rewrite update_s. unfold proj_sumbool. + unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. + revert H0. unfold perm; simpl. rewrite ZMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. auto. omega. omega. Qed. Theorem perm_drop_3: - forall b' ofs p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs p' -> perm m' b' ofs p'. + forall b' ofs k p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs k p' -> perm m' b' ofs k p'. Proof. intros. - unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. - unfold perm; simpl. unfold update. destruct (zeq b' b). subst b'. + unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. + unfold perm; simpl. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). byContradiction. intuition omega. auto. auto. auto. Qed. Theorem perm_drop_4: - forall b' ofs p', perm m' b' ofs p' -> perm m b' ofs p'. + forall b' ofs k p', perm m' b' ofs k p' -> perm m b' ofs k p'. Proof. intros. - unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. - revert H. unfold perm; simpl. unfold update. destruct (zeq b' b). + unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. + revert H. unfold perm; simpl. rewrite ZMap.gsspec. destruct (ZIndexed.eq b' b). subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). - simpl. intros. apply perm_implies with p. apply r. tauto. auto. + simpl. intros. apply perm_implies with p. apply perm_implies with Freeable. apply perm_cur. + apply r. tauto. auto with mem. auto. auto. auto. auto. Qed. -Theorem bounds_drop: - forall b', bounds m' b' = bounds m b'. -Proof. - intros. - unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. - unfold bounds; simpl. auto. -Qed. - Lemma valid_access_drop_1: forall chunk b' ofs p', b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p p' -> @@ -2167,13 +1993,7 @@ Proof. unfold load. destruct (valid_access_dec m chunk b' ofs Readable). rewrite pred_dec_true. - unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi p); inv DROP. simpl. - unfold update. destruct (zeq b' b). subst b'. decEq. decEq. - apply getN_exten. rewrite <- size_chunk_conv. intros. - unfold proj_sumbool. destruct (zle lo i). destruct (zlt i hi). destruct (perm_order_dec p Readable). - auto. - elimtype False. intuition. - auto. auto. auto. + unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. simpl. auto. eapply valid_access_drop_1; eauto. rewrite pred_dec_false. auto. red; intros; elim n. eapply valid_access_drop_2; eauto. @@ -2181,85 +2001,6 @@ Qed. End DROP. -(** * Extensionality properties *) - -Lemma mem_access_ext: - forall m1 m2, perm m1 = perm m2 -> mem_access m1 = mem_access m2. -Proof. - intros. - apply extensionality; intro b. - apply extensionality; intro ofs. - case_eq (mem_access m1 b ofs); case_eq (mem_access m2 b ofs); intros; auto. - assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). - assert (perm m1 b ofs p0 <-> perm m2 b ofs p0) by (rewrite H; intuition). - unfold perm, perm_order' in H2,H3. - rewrite H0 in H2,H3; rewrite H1 in H2,H3. - f_equal. - assert (perm_order p p0 -> perm_order p0 p -> p0=p) by - (clear; intros; inv H; inv H0; auto). - intuition. - assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). - unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. - assert (perm_order p p) by auto with mem. - intuition. - assert (perm m1 b ofs p <-> perm m2 b ofs p) by (rewrite H; intuition). - unfold perm, perm_order' in H2; rewrite H0 in H2; rewrite H1 in H2. - assert (perm_order p p) by auto with mem. - intuition. -Qed. - -Lemma mem_ext': - forall m1 m2, - mem_access m1 = mem_access m2 -> - nextblock m1 = nextblock m2 -> - (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> - (forall b ofs, perm_order' (mem_access m1 b ofs) Readable -> - mem_contents m1 b ofs = mem_contents m2 b ofs) -> - m1 = m2. -Proof. - intros. - destruct m1; destruct m2; simpl in *. - destruct H; subst. - apply mkmem_ext; auto. - apply extensionality; intro b. - apply extensionality; intro ofs. - destruct (perm_order'_dec (mem_access0 b ofs) Readable). - auto. - destruct (noread_undef0 b ofs); try contradiction. - destruct (noread_undef1 b ofs); try contradiction. - congruence. - apply extensionality; intro b. - destruct (nextblock_noaccess0 b); auto. - destruct (nextblock_noaccess1 b); auto. - congruence. -Qed. - -Theorem mem_ext: - forall m1 m2, - perm m1 = perm m2 -> - nextblock m1 = nextblock m2 -> - (forall b, 0 < b < nextblock m1 -> bounds m1 b = bounds m2 b) -> - (forall b ofs, loadbytes m1 b ofs 1 = loadbytes m2 b ofs 1) -> - m1 = m2. -Proof. - intros. - generalize (mem_access_ext _ _ H); clear H; intro. - apply mem_ext'; auto. - intros. - specialize (H2 b ofs). - unfold loadbytes in H2; simpl in H2. - destruct (range_perm_dec m1 b ofs (ofs+1)). - destruct (range_perm_dec m2 b ofs (ofs+1)). - inv H2; auto. - contradict n. - intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. - unfold perm, perm_order'. - rewrite <- H; destruct (mem_access m1 b ofs); try destruct p; intuition. - contradict n. - intros ofs' ?; assert (ofs'=ofs) by omega; subst ofs'. - unfold perm. destruct (mem_access m1 b ofs); try destruct p; intuition. -Qed. - (** * Generic injections *) (** A memory state [m1] generically injects into another memory state [m2] via the @@ -2272,6 +2013,11 @@ Qed. Record mem_inj (f: meminj) (m1 m2: mem) : Prop := mk_mem_inj { + mi_perm: + forall b1 b2 delta ofs k p, + f b1 = Some(b2, delta) -> + perm m1 b1 ofs k p -> + perm m2 b2 (ofs + delta) k p; mi_access: forall b1 b2 delta chunk ofs p, f b1 = Some(b2, delta) -> @@ -2280,33 +2026,28 @@ Record mem_inj (f: meminj) (m1 m2: mem) : Prop := mi_memval: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - perm m1 b1 ofs Nonempty -> - memval_inject f (m1.(mem_contents) b1 ofs) (m2.(mem_contents) b2 (ofs + delta)) + perm m1 b1 ofs Cur Readable -> + memval_inject f (m1.(mem_contents)#b1#ofs) (m2.(mem_contents)#b2#(ofs + delta)) }. (** Preservation of permissions *) Lemma perm_inj: - forall f m1 m2 b1 ofs p b2 delta, + forall f m1 m2 b1 ofs k p b2 delta, mem_inj f m1 m2 -> - perm m1 b1 ofs p -> + perm m1 b1 ofs k p -> f b1 = Some(b2, delta) -> - perm m2 b2 (ofs + delta) p. + perm m2 b2 (ofs + delta) k p. Proof. - intros. - assert (valid_access m1 Mint8unsigned b1 ofs p). - split. red; intros. simpl in H2. replace ofs0 with ofs by omega. auto. - simpl. apply Zone_divide. - exploit mi_access; eauto. intros [A B]. - apply A. simpl; omega. + intros. eapply mi_perm; eauto. Qed. Lemma range_perm_inj: - forall f m1 m2 b1 lo hi p b2 delta, + forall f m1 m2 b1 lo hi k p b2 delta, mem_inj f m1 m2 -> - range_perm m1 b1 lo hi p -> + range_perm m1 b1 lo hi k p -> f b1 = Some(b2, delta) -> - range_perm m2 b2 (lo + delta) (hi + delta) p. + range_perm m2 b2 (lo + delta) (hi + delta) k p. Proof. intros; red; intros. replace ofs with ((ofs - delta) + delta) by omega. @@ -2320,18 +2061,17 @@ Lemma getN_inj: mem_inj f m1 m2 -> f b1 = Some(b2, delta) -> forall n ofs, - range_perm m1 b1 ofs (ofs + Z_of_nat n) Readable -> + range_perm m1 b1 ofs (ofs + Z_of_nat n) Cur Readable -> list_forall2 (memval_inject f) - (getN n ofs (m1.(mem_contents) b1)) - (getN n (ofs + delta) (m2.(mem_contents) b2)). + (getN n ofs (m1.(mem_contents)#b1)) + (getN n (ofs + delta) (m2.(mem_contents)#b2)). Proof. induction n; intros; simpl. constructor. rewrite inj_S in H1. constructor. eapply mi_memval; eauto. - apply perm_implies with Readable. - apply H1. omega. constructor. + apply H1. omega. replace (ofs + delta + 1) with ((ofs + 1) + delta) by omega. apply IHn. red; intros; apply H1; omega. Qed. @@ -2344,7 +2084,7 @@ Lemma load_inj: exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ val_inject f v1 v2. Proof. intros. - exists (decode_val chunk (getN (size_chunk_nat chunk) (ofs + delta) (m2.(mem_contents) b2))). + exists (decode_val chunk (getN (size_chunk_nat chunk) (ofs + delta) (m2.(mem_contents)#b2))). split. unfold load. apply pred_dec_true. eapply mi_access; eauto with mem. exploit load_result; eauto. intro. rewrite H2. @@ -2361,8 +2101,8 @@ Lemma loadbytes_inj: /\ list_forall2 (memval_inject f) bytes1 bytes2. Proof. intros. unfold loadbytes in *. - destruct (range_perm_dec m1 b1 ofs (ofs + len) Readable); inv H0. - exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents) b2)). + destruct (range_perm_dec m1 b1 ofs (ofs + len) Cur Readable); inv H0. + exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents)#b2)). split. apply pred_dec_true. replace (ofs + delta + len) with ((ofs + len) + delta) by omega. eapply range_perm_inj; eauto with mem. @@ -2377,46 +2117,27 @@ Lemma setN_inj: forall (access: Z -> Prop) delta f vl1 vl2, list_forall2 (memval_inject f) vl1 vl2 -> forall p c1 c2, - (forall q, access q -> memval_inject f (c1 q) (c2 (q + delta))) -> - (forall q, access q -> memval_inject f ((setN vl1 p c1) q) - ((setN vl2 (p + delta) c2) (q + delta))). + (forall q, access q -> memval_inject f (c1#q) (c2#(q + delta))) -> + (forall q, access q -> memval_inject f ((setN vl1 p c1)#q) + ((setN vl2 (p + delta) c2)#(q + delta))). Proof. induction 1; intros; simpl. auto. replace (p + delta + 1) with ((p + 1) + delta) by omega. apply IHlist_forall2; auto. - intros. unfold update at 1. destruct (zeq q0 p). subst q0. - rewrite update_s. auto. - rewrite update_o. auto. omega. + intros. rewrite ZMap.gsspec at 1. destruct (ZIndexed.eq q0 p). subst q0. + rewrite ZMap.gss. auto. + rewrite ZMap.gso. auto. unfold ZIndexed.t in *. omega. Qed. Definition meminj_no_overlap (f: meminj) (m: mem) : Prop := - forall b1 b1' delta1 b2 b2' delta2, - b1 <> b2 -> - f b1 = Some (b1', delta1) -> - f b2 = Some (b2', delta2) -> - b1' <> b2' -(* - \/ low_bound m b1 >= high_bound m b1 - \/ low_bound m b2 >= high_bound m b2 *) - \/ high_bound m b1 + delta1 <= low_bound m b2 + delta2 - \/ high_bound m b2 + delta2 <= low_bound m b1 + delta1. - -Lemma meminj_no_overlap_perm: - forall f m b1 b1' delta1 b2 b2' delta2 ofs1 ofs2, - meminj_no_overlap f m -> + forall b1 b1' delta1 b2 b2' delta2 ofs1 ofs2, b1 <> b2 -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> - perm m b1 ofs1 Nonempty -> - perm m b2 ofs2 Nonempty -> + perm m b1 ofs1 Max Nonempty -> + perm m b2 ofs2 Max Nonempty -> b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2. -Proof. - intros. exploit H; eauto. intro. - exploit perm_in_bounds. eexact H3. intro. - exploit perm_in_bounds. eexact H4. intro. - destruct H5. auto. right. omega. -Qed. Lemma store_mapped_inj: forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2, @@ -2429,41 +2150,43 @@ Lemma store_mapped_inj: store chunk m2 b2 (ofs + delta) v2 = Some n2 /\ mem_inj f n1 n2. Proof. - intros. inversion H. + intros. assert (valid_access m2 chunk b2 (ofs + delta) Writable). - eapply mi_access0; eauto with mem. + eapply mi_access; eauto with mem. destruct (valid_access_store _ _ _ _ v2 H4) as [n2 STORE]. - exists n2; split. eauto. + exists n2; split. auto. constructor. +(* perm *) + intros. eapply perm_store_1; [eexact STORE|]. + eapply mi_perm; eauto. + eapply perm_store_2; eauto. (* access *) - intros. - eapply store_valid_access_1; [apply STORE |]. - eapply mi_access0; eauto. - eapply store_valid_access_2; [apply H0 |]. auto. + intros. eapply store_valid_access_1; [apply STORE |]. + eapply mi_access; eauto. + eapply store_valid_access_2; eauto. (* mem_contents *) intros. - assert (perm m1 b0 ofs0 Nonempty). eapply perm_store_2; eauto. rewrite (store_mem_contents _ _ _ _ _ _ H0). rewrite (store_mem_contents _ _ _ _ _ _ STORE). - unfold update. - destruct (zeq b0 b1). subst b0. + repeat rewrite ZMap.gsspec. + destruct (ZIndexed.eq b0 b1). subst b0. (* block = b1, block = b2 *) assert (b3 = b2) by congruence. subst b3. assert (delta0 = delta) by congruence. subst delta0. rewrite zeq_true. - apply setN_inj with (access := fun ofs => perm m1 b1 ofs Nonempty). - apply encode_val_inject; auto. auto. auto. - destruct (zeq b3 b2). subst b3. + apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable). + apply encode_val_inject; auto. intros. eapply mi_memval; eauto. eauto with mem. + destruct (ZIndexed.eq b3 b2). subst b3. (* block <> b1, block = b2 *) - rewrite setN_other. auto. + rewrite setN_other. eapply mi_memval; eauto. eauto with mem. rewrite encode_val_length. rewrite <- size_chunk_conv. intros. assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta). - eapply meminj_no_overlap_perm; eauto. + eapply H1; eauto. eauto 6 with mem. exploit store_valid_access_3. eexact H0. intros [A B]. - eapply perm_implies. apply A. omega. auto with mem. - destruct H9. congruence. omega. + eapply perm_implies. apply perm_cur_max. apply A. omega. auto with mem. + destruct H8. congruence. omega. (* block <> b1, block <> b2 *) - eauto. + eapply mi_memval; eauto. eauto with mem. Qed. Lemma store_unmapped_inj: @@ -2473,14 +2196,15 @@ Lemma store_unmapped_inj: f b1 = None -> mem_inj f n1 m2. Proof. - intros. inversion H. - constructor. + intros. constructor. +(* perm *) + intros. eapply mi_perm; eauto with mem. (* access *) - eauto with mem. + intros. eapply mi_access; eauto with mem. (* mem_contents *) intros. rewrite (store_mem_contents _ _ _ _ _ _ H0). - rewrite update_o. eauto with mem. + rewrite ZMap.gso. eapply mi_memval; eauto with mem. congruence. Qed. @@ -2489,21 +2213,25 @@ Lemma store_outside_inj: mem_inj f m1 m2 -> (forall b' delta ofs', f b' = Some(b, delta) -> - perm m1 b' ofs' Nonempty -> - ofs' + delta < ofs \/ ofs' + delta >= ofs + size_chunk chunk) -> + perm m1 b' ofs' Cur Readable -> + ofs <= ofs' + delta < ofs + size_chunk chunk -> False) -> store chunk m2 b ofs v = Some m2' -> mem_inj f m1 m2'. Proof. - intros. inversion H. constructor. + intros. inv H. constructor. +(* perm *) + eauto with mem. (* access *) eauto with mem. (* mem_contents *) intros. rewrite (store_mem_contents _ _ _ _ _ _ H1). - unfold update. destruct (zeq b2 b). subst b2. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2. rewrite setN_outside. auto. rewrite encode_val_length. rewrite <- size_chunk_conv. - eapply H0; eauto. + destruct (zlt (ofs0 + delta) ofs); auto. + destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). omega. + byContradiction. eapply H0; eauto. omega. eauto with mem. Qed. @@ -2519,7 +2247,7 @@ Lemma storebytes_mapped_inj: /\ mem_inj f n1 n2. Proof. intros. inversion H. - assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Writable). + assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Cur Writable). replace (ofs + delta + Z_of_nat (length bytes2)) with ((ofs + Z_of_nat (length bytes1)) + delta). eapply range_perm_inj; eauto with mem. @@ -2528,33 +2256,37 @@ Proof. destruct (range_perm_storebytes _ _ _ _ H4) as [n2 STORE]. exists n2; split. eauto. constructor. +(* perm *) + intros. + eapply perm_storebytes_1; [apply STORE |]. + eapply mi_perm0; eauto. + eapply perm_storebytes_2; eauto. (* access *) intros. eapply storebytes_valid_access_1; [apply STORE |]. eapply mi_access0; eauto. - eapply storebytes_valid_access_2; [apply H0 |]. auto. + eapply storebytes_valid_access_2; eauto. (* mem_contents *) intros. - assert (perm m1 b0 ofs0 Nonempty). eapply perm_storebytes_2; eauto. + assert (perm m1 b0 ofs0 Cur Readable). eapply perm_storebytes_2; eauto. rewrite (storebytes_mem_contents _ _ _ _ _ H0). rewrite (storebytes_mem_contents _ _ _ _ _ STORE). - unfold update. - destruct (zeq b0 b1). subst b0. + repeat rewrite ZMap.gsspec. destruct (ZIndexed.eq b0 b1). subst b0. (* block = b1, block = b2 *) assert (b3 = b2) by congruence. subst b3. assert (delta0 = delta) by congruence. subst delta0. rewrite zeq_true. - apply setN_inj with (access := fun ofs => perm m1 b1 ofs Nonempty); auto. - destruct (zeq b3 b2). subst b3. + apply setN_inj with (access := fun ofs => perm m1 b1 ofs Cur Readable); auto. + destruct (ZIndexed.eq b3 b2). subst b3. (* block <> b1, block = b2 *) rewrite setN_other. auto. intros. assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta). - eapply meminj_no_overlap_perm; eauto. + eapply H1; eauto 6 with mem. exploit storebytes_range_perm. eexact H0. instantiate (1 := r - delta). rewrite (list_forall2_length H3). omega. - eauto with mem. + eauto 6 with mem. destruct H9. congruence. omega. (* block <> b1, block <> b2 *) eauto. @@ -2569,12 +2301,14 @@ Lemma storebytes_unmapped_inj: Proof. intros. inversion H. constructor. +(* perm *) + intros. eapply mi_perm0; eauto. eapply perm_storebytes_2; eauto. (* access *) intros. eapply mi_access0; eauto. eapply storebytes_valid_access_2; eauto. (* mem_contents *) intros. rewrite (storebytes_mem_contents _ _ _ _ _ H0). - rewrite update_o. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto. + rewrite ZMap.gso. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto. congruence. Qed. @@ -2583,20 +2317,24 @@ Lemma storebytes_outside_inj: mem_inj f m1 m2 -> (forall b' delta ofs', f b' = Some(b, delta) -> - perm m1 b' ofs' Nonempty -> - ofs' + delta < ofs \/ ofs' + delta >= ofs + Z_of_nat (length bytes2)) -> + perm m1 b' ofs' Cur Readable -> + ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) -> storebytes m2 b ofs bytes2 = Some m2' -> mem_inj f m1 m2'. Proof. intros. inversion H. constructor. +(* perm *) + intros. eapply perm_storebytes_1; eauto with mem. (* access *) intros. eapply storebytes_valid_access_1; eauto with mem. (* mem_contents *) intros. rewrite (storebytes_mem_contents _ _ _ _ _ H1). - unfold update. destruct (zeq b2 b). subst b2. + rewrite ZMap.gsspec. destruct (ZIndexed.eq b2 b). subst b2. rewrite setN_outside. auto. - eapply H0; eauto. + destruct (zlt (ofs0 + delta) ofs); auto. + destruct (zle (ofs + Z_of_nat (length bytes2)) (ofs0 + delta)). omega. + byContradiction. eapply H0; eauto. omega. eauto with mem. Qed. @@ -2610,17 +2348,17 @@ Lemma alloc_right_inj: Proof. intros. injection H0. intros NEXT MEM. inversion H. constructor. +(* perm *) + intros. eapply perm_alloc_1; eauto. (* access *) - intros. eauto with mem. + intros. eapply valid_access_alloc_other; eauto. (* mem_contents *) intros. - assert (valid_access m2 Mint8unsigned b0 (ofs + delta) Nonempty). - eapply mi_access0; eauto. - split. simpl. red; intros. assert (ofs0 = ofs) by omega. congruence. - simpl. apply Zone_divide. + assert (perm m2 b0 (ofs + delta) Cur Readable). + eapply mi_perm0; eauto. assert (valid_block m2 b0) by eauto with mem. - rewrite <- MEM; simpl. rewrite update_o. eauto with mem. - rewrite NEXT. apply sym_not_equal. eauto with mem. + rewrite <- MEM; simpl. rewrite ZMap.gso. eauto with mem. + rewrite NEXT. eauto with mem. Qed. Lemma alloc_left_unmapped_inj: @@ -2631,15 +2369,18 @@ Lemma alloc_left_unmapped_inj: mem_inj f m1' m2. Proof. intros. inversion H. constructor. +(* perm *) + intros. exploit perm_alloc_inv; eauto. intros. + destruct (zeq b0 b1). congruence. eauto. (* access *) - unfold update; intros. - exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. + intros. exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. destruct (zeq b0 b1). congruence. eauto. (* mem_contents *) injection H0; intros NEXT MEM. intros. - rewrite <- MEM; simpl. rewrite NEXT. unfold update. - exploit perm_alloc_inv; eauto. intros. - destruct (zeq b0 b1). constructor. eauto. + rewrite <- MEM; simpl. rewrite NEXT. + exploit perm_alloc_inv; eauto. intros. + rewrite ZMap.gsspec. unfold ZIndexed.eq. destruct (zeq b0 b1). + rewrite ZMap.gi. constructor. eauto. Qed. Definition inj_offset_aligned (delta: Z) (size: Z) : Prop := @@ -2651,25 +2392,30 @@ Lemma alloc_left_mapped_inj: alloc m1 lo hi = (m1', b1) -> valid_block m2 b2 -> inj_offset_aligned delta (hi-lo) -> - (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) -> + (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) -> f b1 = Some(b2, delta) -> mem_inj f m1' m2. Proof. intros. inversion H. constructor. +(* perm *) + intros. + exploit perm_alloc_inv; eauto. intros. destruct (zeq b0 b1). subst b0. + rewrite H4 in H5; inv H5. eauto. eauto. (* access *) intros. exploit valid_access_alloc_inv; eauto. unfold eq_block. intros. - destruct (zeq b0 b1). subst b0. rewrite H4 in H5. inversion H5; clear H5; subst b3 delta0. + destruct (zeq b0 b1). subst b0. rewrite H4 in H5. inv H5. split. red; intros. - replace ofs0 with ((ofs0 - delta) + delta) by omega. + replace ofs0 with ((ofs0 - delta0) + delta0) by omega. apply H3. omega. destruct H6. apply Zdivide_plus_r. auto. apply H2. omega. eauto. (* mem_contents *) injection H0; intros NEXT MEM. - intros. rewrite <- MEM; simpl. rewrite NEXT. unfold update. - exploit perm_alloc_inv; eauto. intros. - destruct (zeq b0 b1). constructor. eauto. + intros. rewrite <- MEM; simpl. rewrite NEXT. + exploit perm_alloc_inv; eauto. intros. + rewrite ZMap.gsspec. unfold ZIndexed.eq. + destruct (zeq b0 b1). rewrite ZMap.gi. constructor. eauto. Qed. Lemma free_left_inj: @@ -2679,45 +2425,42 @@ Lemma free_left_inj: mem_inj f m1' m2. Proof. intros. exploit free_result; eauto. intro FREE. inversion H. constructor. +(* perm *) + intros. eauto with mem. (* access *) intros. eauto with mem. (* mem_contents *) - intros. rewrite FREE; simpl. - assert (b=b1 /\ lo <= ofs < hi \/ (b<>b1 \/ ofs free m2 b lo hi = Some m2' -> - (forall b1 delta ofs p, - f b1 = Some(b, delta) -> perm m1 b1 ofs p -> - lo <= ofs + delta < hi -> False) -> + (forall b' delta ofs k p, + f b' = Some(b, delta) -> + perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) -> mem_inj f m1 m2'. Proof. - intros. exploit free_result; eauto. intro FREE. inversion H. constructor. + intros. exploit free_result; eauto. intro FREE. inversion H. + assert (PERM: + forall b1 b2 delta ofs k p, + f b1 = Some (b2, delta) -> + perm m1 b1 ofs k p -> perm m2' b2 (ofs + delta) k p). + intros. + intros. eapply perm_free_1; eauto. + destruct (zeq b2 b); auto. subst b. right. + assert (~ (lo <= ofs + delta < hi)). red; intros; eapply H1; eauto. + omega. + constructor. +(* perm *) + auto. (* access *) intros. exploit mi_access0; eauto. intros [RG AL]. split; auto. - red; intros. eapply perm_free_1; eauto. - destruct (zeq b2 b); auto. subst b. right. - destruct (zlt ofs0 lo); auto. destruct (zle hi ofs0); auto. - elimtype False. eapply H1 with (ofs := ofs0 - delta). eauto. - apply H3. omega. omega. + red; intros. replace ofs0 with ((ofs0 - delta) + delta) by omega. + eapply PERM. eauto. apply H3. omega. (* mem_contents *) - intros. rewrite FREE; simpl. - specialize (mi_memval0 _ _ _ _ H2 H3). - assert (b=b2 /\ lo <= ofs+delta < hi \/ (b<>b2 \/ ofs+delta + perm m1' b0 ofs k p0 -> perm m2' b3 (ofs + delta0) k p0). + intros. + assert (perm m2 b3 (ofs + delta0) k p0). + eapply mi_perm0; eauto. eapply perm_drop_4; eauto. + destruct (zeq b1 b0). + (* b1 = b0 *) + subst b0. rewrite H2 in H; inv H. + destruct (zlt (ofs + delta0) (lo + delta0)). eapply perm_drop_3; eauto. + destruct (zle (hi + delta0) (ofs + delta0)). eapply perm_drop_3; eauto. + assert (perm_order p p0). + eapply perm_drop_2. eexact H0. instantiate (1 := ofs). omega. eauto. + apply perm_implies with p; auto. + eapply perm_drop_1. eauto. omega. + (* b1 <> b0 *) + eapply perm_drop_3; eauto. + destruct (zeq b3 b2); auto. + destruct (zlt (ofs + delta0) (lo + delta)); auto. + destruct (zle (hi + delta) (ofs + delta0)); auto. + exploit H1; eauto. + instantiate (1 := ofs + delta0 - delta). + apply perm_cur_max. apply perm_implies with Freeable. + eapply range_perm_drop_1; eauto. omega. auto with mem. + eapply perm_drop_4; eauto. eapply perm_max. apply perm_implies with p0. eauto. + eauto with mem. + unfold block. omega. + constructor. +(* perm *) + auto. (* access *) - exploit mi_access0; eauto. eapply valid_access_drop_2; eauto. + intros. exploit mi_access0; eauto. eapply valid_access_drop_2; eauto. intros [A B]. split; auto. red; intros. - destruct (eq_block b1 b0). subst b0. rewrite H2 in H; inv H. - (* b1 = b0 *) - destruct (zlt ofs0 (lo + delta0)). eapply perm_drop_3; eauto. - destruct (zle (hi + delta0) ofs0). eapply perm_drop_3; eauto. - destruct H3 as [C D]. - assert (perm_order p p0). - eapply perm_drop_2. eexact H0. instantiate (1 := ofs0 - delta0). omega. - apply C. omega. - apply perm_implies with p; auto. - eapply perm_drop_1. eauto. omega. - (* b1 <> b0 *) - eapply perm_drop_3; eauto. - exploit H1; eauto. intros [P | P]. auto. right. - destruct (zlt lo hi). - exploit range_perm_in_bounds. eapply range_perm_drop_1. eexact H0. auto. - intros [U V]. - exploit valid_access_drop_2. eexact H0. eauto. - intros [C D]. - exploit range_perm_in_bounds. eexact C. generalize (size_chunk_pos chunk); omega. - intros [X Y]. - generalize (size_chunk_pos chunk). omega. - omega. + replace ofs0 with ((ofs0 - delta0) + delta0) by omega. + eapply PERM; eauto. apply H3. omega. (* memval *) - assert (A: perm m1 b0 ofs Nonempty). eapply perm_drop_4; eauto. - exploit mi_memval0; eauto. intros B. - unfold drop_perm in *. - destruct (range_perm_dec m1 b1 lo hi p); inversion H0; clear H0. clear H5. - destruct (range_perm_dec m2 b2 (lo + delta) (hi + delta) p); inversion DROP; clear DROP. clear H4. - simpl. unfold update. destruct (zeq b0 b1). - (* b1 = b0 *) - subst b0. rewrite H2 in H; inv H. rewrite zeq_true. unfold proj_sumbool. - destruct (zle lo ofs). - rewrite zle_true. - destruct (zlt ofs hi). - rewrite zlt_true. - destruct (perm_order_dec p Readable). - simpl. auto. - simpl. constructor. - omega. - rewrite zlt_false. simpl. auto. omega. - omega. - rewrite zle_false. simpl. auto. omega. - (* b1 <> b0 *) - destruct (zeq b3 b2). - (* b2 = b3 *) - subst b3. exploit H1. eauto. eauto. eauto. intros [P | P]. congruence. - exploit perm_in_bounds; eauto. intros X. - destruct (zle (lo + delta) (ofs + delta0)). - destruct (zlt (ofs + delta0) (hi + delta)). - destruct (zlt lo hi). - exploit range_perm_in_bounds. eexact r. auto. intros [Y Z]. - omegaContradiction. - omegaContradiction. - simpl. auto. - simpl. auto. - auto. + intros. + replace (m1'.(mem_contents)#b0) with (m1.(mem_contents)#b0). + replace (m2'.(mem_contents)#b3) with (m2.(mem_contents)#b3). + apply mi_memval0; auto. eapply perm_drop_4; eauto. + unfold drop_perm in DROP; destruct (range_perm_dec m2 b2 (lo + delta) (hi + delta) Cur Freeable); inv DROP; auto. + unfold drop_perm in H0; destruct (range_perm_dec m1 b1 lo hi Cur Freeable); inv H0; auto. Qed. Lemma drop_outside_inj: forall f m1 m2 b lo hi p m2', mem_inj f m1 m2 -> drop_perm m2 b lo hi p = Some m2' -> - (forall b' delta, + (forall b' delta ofs' k p, f b' = Some(b, delta) -> - high_bound m1 b' + delta <= lo - \/ hi <= low_bound m1 b' + delta) -> + perm m1 b' ofs' k p -> + lo <= ofs' + delta < hi -> False) -> mem_inj f m1 m2'. -Proof. - intros. destruct H. constructor; intros. - +Proof. + intros. inv H. + assert (PERM: forall b0 b3 delta0 ofs k p0, + f b0 = Some (b3, delta0) -> + perm m1 b0 ofs k p0 -> perm m2' b3 (ofs + delta0) k p0). + intros. eapply perm_drop_3; eauto. + destruct (zeq b3 b); auto. subst b3. right. + destruct (zlt (ofs + delta0) lo); auto. + destruct (zle hi (ofs + delta0)); auto. + byContradiction. exploit H1; eauto. omega. + constructor. + (* perm *) + auto. (* access *) - inversion H2. - destruct (range_perm_in_bounds _ _ _ _ _ H3). - pose proof (size_chunk_pos chunk). omega. - pose proof (mi_access0 b1 b2 delta chunk ofs p0 H H2). clear mi_access0 H2 H3. - unfold valid_access in *. intuition. clear H3. - unfold range_perm in *. intros. - eapply perm_drop_3; eauto. - destruct (eq_block b2 b); subst; try (intuition; fail). - destruct (H1 b1 delta H); intuition omega. - - (* memval *) - pose proof (mi_memval0 _ _ _ _ H H2). clear mi_memval0. - unfold Mem.drop_perm in H0. - destruct (Mem.range_perm_dec m2 b lo hi p); inversion H0; subst; clear H0. - simpl. unfold update. destruct (zeq b2 b); subst; auto. - pose proof (perm_in_bounds _ _ _ _ H2). - destruct (H1 b1 delta H). - destruct (zle lo (ofs + delta)); simpl; auto. exfalso; omega. - destruct (zle lo (ofs + delta)); destruct (zlt (ofs + delta) hi); simpl; auto. - exfalso; omega. + intros. exploit mi_access0; eauto. intros [A B]. split; auto. + red; intros. + replace ofs0 with ((ofs0 - delta) + delta) by omega. + eapply PERM; eauto. apply H2. omega. + (* contents *) + intros. + replace (m2'.(mem_contents)#b2) with (m2.(mem_contents)#b2). + apply mi_memval0; auto. + unfold drop_perm in H0; destruct (range_perm_dec m2 b lo hi Cur Freeable); inv H0; auto. Qed. - (** * Memory extensions *) (** A store [m2] extends a store [m1] if [m2] can be obtained from [m1] @@ -2864,9 +2591,6 @@ Record extends' (m1 m2: mem) : Prop := mk_extends { mext_next: nextblock m1 = nextblock m2; mext_inj: mem_inj inject_id m1 m2 -(* - mext_bounds: forall b, low_bound m2 b <= low_bound m1 b /\ high_bound m1 b <= high_bound m2 b -*) }. Definition extends := extends'. @@ -2876,6 +2600,7 @@ Theorem extends_refl: Proof. intros. constructor. auto. constructor. intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto. + intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto. intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. apply memval_lessdef_refl. Qed. @@ -2936,30 +2661,19 @@ Proof. rewrite (nextblock_store _ _ _ _ _ _ H0). rewrite (nextblock_store _ _ _ _ _ _ A). auto. -(* - intros. - rewrite (bounds_store _ _ _ _ _ _ H0). - rewrite (bounds_store _ _ _ _ _ _ A). - auto. -*) Qed. Theorem store_outside_extends: forall chunk m1 m2 b ofs v m2', extends m1 m2 -> store chunk m2 b ofs v = Some m2' -> - ofs + size_chunk chunk <= low_bound m1 b \/ high_bound m1 b <= ofs -> + (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + size_chunk chunk -> False) -> extends m1 m2'. Proof. intros. inversion H. constructor. rewrite (nextblock_store _ _ _ _ _ _ H0). auto. eapply store_outside_inj; eauto. - unfold inject_id; intros. inv H2. - exploit perm_in_bounds; eauto. omega. -(* - intros. - rewrite (bounds_store _ _ _ _ _ _ H0). auto. -*) + unfold inject_id; intros. inv H2. eapply H1; eauto. omega. Qed. Theorem storev_extends: @@ -2997,30 +2711,19 @@ Proof. rewrite (nextblock_storebytes _ _ _ _ _ H0). rewrite (nextblock_storebytes _ _ _ _ _ A). auto. -(* - intros. - rewrite (bounds_store _ _ _ _ _ _ H0). - rewrite (bounds_store _ _ _ _ _ _ A). - auto. -*) Qed. Theorem storebytes_outside_extends: forall m1 m2 b ofs bytes2 m2', extends m1 m2 -> storebytes m2 b ofs bytes2 = Some m2' -> - ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs -> + (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) -> extends m1 m2'. Proof. intros. inversion H. constructor. rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. eapply storebytes_outside_inj; eauto. - unfold inject_id; intros. inv H2. - exploit perm_in_bounds; eauto. omega. -(* - intros. - rewrite (bounds_store _ _ _ _ _ _ H0). auto. -*) + unfold inject_id; intros. inv H2. eapply H1; eauto. omega. Qed. Theorem alloc_extends: @@ -3063,26 +2766,19 @@ Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_left_inj; eauto. -(* - intros. rewrite (bounds_free _ _ _ _ _ H0). auto. -*) Qed. Theorem free_right_extends: forall m1 m2 b lo hi m2', extends m1 m2 -> free m2 b lo hi = Some m2' -> - (forall ofs p, lo <= ofs < hi -> ~perm m1 b ofs p) -> + (forall ofs k p, perm m1 b ofs k p -> lo <= ofs < hi -> False) -> extends m1 m2'. Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_right_inj; eauto. - unfold inject_id; intros. inv H. - elim (H1 ofs p); auto. omega. -(* - intros. rewrite (bounds_free _ _ _ _ _ H0). auto. -*) + unfold inject_id; intros. inv H. eapply H1; eauto. omega. Qed. Theorem free_parallel_extends: @@ -3105,15 +2801,8 @@ Proof. rewrite (nextblock_free _ _ _ _ _ FREE). auto. eapply free_right_inj with (m1 := m1'); eauto. eapply free_left_inj; eauto. - unfold inject_id; intros. inv H. - assert (~perm m1' b ofs p). eapply perm_free_2; eauto. omega. - contradiction. -(* - intros. - rewrite (bounds_free _ _ _ _ _ H0). - rewrite (bounds_free _ _ _ _ _ FREE). - auto. -*) + unfold inject_id; intros. inv H. + eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. Qed. Theorem valid_block_extends: @@ -3125,8 +2814,8 @@ Proof. Qed. Theorem perm_extends: - forall m1 m2 b ofs p, - extends m1 m2 -> perm m1 b ofs p -> perm m2 b ofs p. + forall m1 m2 b ofs k p, + extends m1 m2 -> perm m1 b ofs k p -> perm m2 b ofs k p. Proof. intros. inv H. replace ofs with (ofs + 0) by omega. eapply perm_inj; eauto. @@ -3149,15 +2838,6 @@ Proof. eapply valid_access_extends; eauto. Qed. -(* -Theorem bounds_extends: - forall m1 m2 b, - extends m1 m2 -> low_bound m2 b <= low_bound m1 b /\ high_bound m1 b <= high_bound m2 b. -Proof. - intros. inv H. auto. -Qed. -*) - (** * Memory injections *) (** A memory state [m1] injects into another memory state [m2] via the @@ -3188,15 +2868,15 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop := f b = Some(b', delta) -> 0 <= delta <= Int.max_unsigned; mi_range_block: - forall b b' delta, + forall b b' delta ofs k p, f b = Some(b', delta) -> - delta = 0 \/ - (0 <= low_bound m2 b' /\ high_bound m2 b' <= Int.max_unsigned) + perm m2 b' ofs k p -> + delta = 0 \/ 0 <= ofs <= Int.max_unsigned }. Definition inject := inject'. -Hint Local Resolve mi_mappedblocks mi_range_offset: mem. +Local Hint Resolve mi_mappedblocks mi_range_offset: mem. (** Preservation of access validity and pointer validity *) @@ -3219,22 +2899,22 @@ Proof. intros. eapply mi_mappedblocks; eauto. Qed. -Hint Local Resolve valid_block_inject_1 valid_block_inject_2: mem. +Local Hint Resolve valid_block_inject_1 valid_block_inject_2: mem. Theorem perm_inject: - forall f m1 m2 b1 b2 delta ofs p, + forall f m1 m2 b1 b2 delta ofs k p, f b1 = Some(b2, delta) -> inject f m1 m2 -> - perm m1 b1 ofs p -> perm m2 b2 (ofs + delta) p. + perm m1 b1 ofs k p -> perm m2 b2 (ofs + delta) k p. Proof. intros. inv H0. eapply perm_inj; eauto. Qed. Theorem range_perm_inject: - forall f m1 m2 b1 b2 delta lo hi p, + forall f m1 m2 b1 b2 delta lo hi k p, f b1 = Some(b2, delta) -> inject f m1 m2 -> - range_perm m1 b1 lo hi p -> range_perm m2 b2 (lo + delta) (hi + delta) p. + range_perm m1 b1 lo hi k p -> range_perm m2 b2 (lo + delta) (hi + delta) k p. Proof. intros. inv H0. eapply range_perm_inj; eauto. Qed. @@ -3268,19 +2948,18 @@ Qed. Lemma address_inject: forall f m1 m2 b1 ofs1 b2 delta, inject f m1 m2 -> - perm m1 b1 (Int.unsigned ofs1) Nonempty -> + perm m1 b1 (Int.unsigned ofs1) Max Nonempty -> f b1 = Some (b2, delta) -> Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. Proof. intros. exploit perm_inject; eauto. intro A. - exploit perm_in_bounds. eexact A. intros [B C]. - exploit mi_range_block; eauto. intros [D | [E F]]. + exploit mi_range_block; eauto. intros [D | E]. subst delta. rewrite Int.add_zero. omega. unfold Int.add. repeat rewrite Int.unsigned_repr. auto. eapply mi_range_offset; eauto. - omega. + auto. eapply mi_range_offset; eauto. Qed. @@ -3292,7 +2971,7 @@ Lemma address_inject': Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. Proof. intros. destruct H0. eapply address_inject; eauto. - apply H0. generalize (size_chunk_pos chunk). omega. + apply perm_cur_max. apply H0. generalize (size_chunk_pos chunk). omega. Qed. Theorem valid_pointer_inject_no_overflow: @@ -3330,11 +3009,11 @@ Theorem inject_no_overlap: b1 <> b2 -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> - perm m1 b1 ofs1 Nonempty -> - perm m1 b2 ofs2 Nonempty -> + perm m1 b1 ofs1 Max Nonempty -> + perm m1 b2 ofs2 Max Nonempty -> b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2. Proof. - intros. inv H. eapply meminj_no_overlap_perm; eauto. + intros. inv H. eapply mi_no_overlap0; eauto. Qed. Theorem different_pointers_inject: @@ -3355,19 +3034,20 @@ Proof. rewrite (address_inject' _ _ _ _ _ _ _ _ H H1 H3). rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4). inv H1. simpl in H5. inv H2. simpl in H1. - eapply meminj_no_overlap_perm. - eapply mi_no_overlap; eauto. eauto. eauto. eauto. - apply (H5 (Int.unsigned ofs1)). omega. - apply (H1 (Int.unsigned ofs2)). omega. + eapply mi_no_overlap; eauto. + apply perm_cur_max. apply (H5 (Int.unsigned ofs1)). omega. + apply perm_cur_max. apply (H1 (Int.unsigned ofs2)). omega. Qed. +Require Intv. + Theorem disjoint_or_equal_inject: forall f m m' b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz, inject f m m' -> f b1 = Some(b1', delta1) -> f b2 = Some(b2', delta2) -> - range_perm m b1 ofs1 (ofs1 + sz) Nonempty -> - range_perm m b2 ofs2 (ofs2 + sz) Nonempty -> + range_perm m b1 ofs1 (ofs1 + sz) Max Nonempty -> + range_perm m b2 ofs2 (ofs2 + sz) Max Nonempty -> sz > 0 -> b1 <> b2 \/ ofs1 = ofs2 \/ ofs1 + sz <= ofs2 \/ ofs2 + sz <= ofs1 -> b1' <> b2' \/ ofs1 + delta1 = ofs2 + delta2 @@ -3375,12 +3055,19 @@ Theorem disjoint_or_equal_inject: \/ ofs2 + delta2 + sz <= ofs1 + delta1. Proof. intros. - exploit range_perm_in_bounds. eexact H2. omega. intros [LO1 HI1]. - exploit range_perm_in_bounds. eexact H3. omega. intros [LO2 HI2]. destruct (eq_block b1 b2). assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst. destruct H5. congruence. right. destruct H5. left; congruence. right. omega. - exploit mi_no_overlap; eauto. intros [P | P]. auto. right. omega. + destruct (eq_block b1' b2'); auto. subst. right. right. + set (i1 := (ofs1 + delta1, ofs1 + delta1 + sz)). + set (i2 := (ofs2 + delta2, ofs2 + delta2 + sz)). + change (snd i1 <= fst i2 \/ snd i2 <= fst i1). + apply Intv.range_disjoint'; simpl; try omega. + unfold Intv.disjoint, Intv.In; simpl; intros. red; intros. + exploit mi_no_overlap; eauto. + instantiate (1 := x - delta1). apply H2. omega. + instantiate (1 := x - delta2). apply H3. omega. + unfold block; omega. Qed. Theorem aligned_area_inject: @@ -3388,7 +3075,7 @@ Theorem aligned_area_inject: inject f m m' -> al = 1 \/ al = 2 \/ al = 4 -> sz > 0 -> (al | sz) -> - range_perm m b ofs (ofs + sz) Nonempty -> + range_perm m b ofs (ofs + sz) Cur Nonempty -> (al | ofs) -> f b = Some(b', delta) -> (al | ofs + delta). @@ -3468,13 +3155,11 @@ Proof. (* mappedblocks *) eauto with mem. (* no overlap *) - red; intros. - repeat rewrite (bounds_store _ _ _ _ _ _ H0). - eauto. + red; intros. eauto with mem. (* range offset *) eauto. (* range blocks *) - intros. rewrite (bounds_store _ _ _ _ _ _ STORE). eauto. + eauto with mem. Qed. Theorem store_unmapped_inject: @@ -3493,9 +3178,7 @@ Proof. (* mappedblocks *) eauto with mem. (* no overlap *) - red; intros. - repeat rewrite (bounds_store _ _ _ _ _ _ H0). - eauto. + red; intros. eauto with mem. (* range offset *) eauto. (* range blocks *) @@ -3505,18 +3188,16 @@ Qed. Theorem store_outside_inject: forall f m1 m2 chunk b ofs v m2', inject f m1 m2 -> - (forall b' delta, + (forall b' delta ofs', f b' = Some(b, delta) -> - high_bound m1 b' + delta <= ofs - \/ ofs + size_chunk chunk <= low_bound m1 b' + delta) -> + perm m1 b' ofs' Cur Readable -> + ofs <= ofs' + delta < ofs + size_chunk chunk -> False) -> store chunk m2 b ofs v = Some m2' -> inject f m1 m2'. Proof. intros. inversion H. constructor. (* inj *) eapply store_outside_inj; eauto. - intros. exploit perm_in_bounds; eauto. intro. - exploit H0; eauto. intro. omega. (* freeblocks *) auto. (* mappedblocks *) @@ -3525,8 +3206,8 @@ Proof. auto. (* range offset *) auto. -(* rang blocks *) - intros. rewrite (bounds_store _ _ _ _ _ _ H1). eauto. +(* range blocks *) + intros. eauto with mem. Qed. Theorem storev_mapped_inject: @@ -3566,13 +3247,11 @@ Proof. (* mappedblocks *) intros. eapply storebytes_valid_block_1; eauto. (* no overlap *) - red; intros. - repeat rewrite (bounds_storebytes _ _ _ _ _ H0). - eauto. + red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. (* range offset *) eauto. (* range blocks *) - intros. rewrite (bounds_storebytes _ _ _ _ _ STORE). eauto. + intros. eapply mi_range_block0; eauto. eapply perm_storebytes_2; eauto. Qed. Theorem storebytes_unmapped_inject: @@ -3591,30 +3270,26 @@ Proof. (* mappedblocks *) eauto with mem. (* no overlap *) - red; intros. - repeat rewrite (bounds_storebytes _ _ _ _ _ H0). - eauto. + red; intros. eapply mi_no_overlap0; eauto; eapply perm_storebytes_2; eauto. (* range offset *) eauto. (* range blocks *) - auto. + eauto. Qed. Theorem storebytes_outside_inject: forall f m1 m2 b ofs bytes2 m2', inject f m1 m2 -> - (forall b' delta, + (forall b' delta ofs', f b' = Some(b, delta) -> - high_bound m1 b' + delta <= ofs - \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) -> + perm m1 b' ofs' Cur Readable -> + ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) -> storebytes m2 b ofs bytes2 = Some m2' -> inject f m1 m2'. Proof. intros. inversion H. constructor. (* inj *) eapply storebytes_outside_inj; eauto. - intros. exploit perm_in_bounds; eauto. intro. - exploit H0; eauto. omega. (* freeblocks *) auto. (* mappedblocks *) @@ -3624,7 +3299,7 @@ Proof. (* range offset *) auto. (* range blocks *) - intros. rewrite (bounds_storebytes _ _ _ _ _ H1). eauto. + intros. eapply mi_range_block0; eauto. eapply perm_storebytes_2; eauto. Qed. (* Preservation of allocations *) @@ -3648,7 +3323,7 @@ Proof. (* range offset *) auto. (* range block *) - intros. rewrite (bounds_alloc_other _ _ _ _ _ H0). eauto. + intros. exploit perm_alloc_inv; eauto. rewrite zeq_false. eauto. eapply valid_not_valid_diff; eauto with mem. Qed. @@ -3663,39 +3338,43 @@ Theorem alloc_left_unmapped_inject: /\ (forall b, b <> b1 -> f' b = f b). Proof. intros. inversion H. - assert (inject_incr f (update b1 None f)). - red; unfold update; intros. destruct (zeq b b1). subst b. + set (f' := fun b => if zeq b b1 then None else f b). + assert (inject_incr f f'). + red; unfold f'; intros. destruct (zeq b b1). subst b. assert (f b1 = None). eauto with mem. congruence. auto. - assert (mem_inj (update b1 None f) m1 m2). + assert (mem_inj f' m1 m2). inversion mi_inj0; constructor; eauto with mem. - unfold update; intros. destruct (zeq b0 b1). congruence. eauto. - unfold update; intros. destruct (zeq b0 b1). congruence. + unfold f'; intros. destruct (zeq b0 b1). congruence. eauto. + unfold f'; intros. destruct (zeq b0 b1). congruence. eauto. + unfold f'; intros. destruct (zeq b0 b1). congruence. apply memval_inject_incr with f; auto. - exists (update b1 None f); split. constructor. + exists f'; split. constructor. (* inj *) - eapply alloc_left_unmapped_inj; eauto. apply update_s. + eapply alloc_left_unmapped_inj; eauto. unfold f'; apply zeq_true. (* freeblocks *) - intros. unfold update. destruct (zeq b b1). auto. + intros. unfold f'. destruct (zeq b b1). auto. apply mi_freeblocks0. red; intro; elim H3. eauto with mem. (* mappedblocks *) - unfold update; intros. destruct (zeq b b1). congruence. eauto. + unfold f'; intros. destruct (zeq b b1). congruence. eauto. (* no overlap *) - unfold update; red; intros. + unfold f'; red; intros. destruct (zeq b0 b1); destruct (zeq b2 b1); try congruence. - repeat rewrite (bounds_alloc_other _ _ _ _ _ H0); eauto. + eapply mi_no_overlap0. eexact H3. eauto. eauto. + exploit perm_alloc_inv. eauto. eexact H6. rewrite zeq_false; auto. + exploit perm_alloc_inv. eauto. eexact H7. rewrite zeq_false; auto. (* range offset *) - unfold update; intros. + unfold f'; intros. destruct (zeq b b1). congruence. eauto. (* range block *) - unfold update; intros. + unfold f'; intros. destruct (zeq b b1). congruence. eauto. (* incr *) split. auto. (* image *) - split. apply update_s. + split. unfold f'; apply zeq_true. (* incr *) - intros; apply update_o; auto. + intros; unfold f'; apply zeq_false; auto. Qed. Theorem alloc_left_mapped_inject: @@ -3704,13 +3383,13 @@ Theorem alloc_left_mapped_inject: alloc m1 lo hi = (m1', b1) -> valid_block m2 b2 -> 0 <= delta <= Int.max_unsigned -> - delta = 0 \/ 0 <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_unsigned -> - (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) -> + (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) -> + (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) -> inj_offset_aligned delta (hi-lo) -> - (forall b ofs, - f b = Some (b2, ofs) -> - high_bound m1 b + ofs <= lo + delta \/ - hi + delta <= low_bound m1 b + ofs) -> + (forall b delta' ofs k p, + f b = Some (b2, delta') -> + perm m1 b ofs k p -> + lo + delta <= ofs + delta' < hi + delta -> False) -> exists f', inject f' m1' m2 /\ inject_incr f f' @@ -3718,48 +3397,57 @@ Theorem alloc_left_mapped_inject: /\ (forall b, b <> b1 -> f' b = f b). Proof. intros. inversion H. - assert (inject_incr f (update b1 (Some(b2, delta)) f)). - red; unfold update; intros. destruct (zeq b b1). subst b. + set (f' := fun b => if zeq b b1 then Some(b2, delta) else f b). + assert (inject_incr f f'). + red; unfold f'; intros. destruct (zeq b b1). subst b. assert (f b1 = None). eauto with mem. congruence. auto. - assert (mem_inj (update b1 (Some(b2, delta)) f) m1 m2). + assert (mem_inj f' m1 m2). inversion mi_inj0; constructor; eauto with mem. - unfold update; intros. destruct (zeq b0 b1). - inv H8. elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. + unfold f'; intros. destruct (zeq b0 b1). + inversion H8. subst b0 b3 delta0. + elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. + eauto. + unfold f'; intros. destruct (zeq b0 b1). + inversion H8. subst b0 b3 delta0. + elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. eauto. - unfold update; intros. destruct (zeq b0 b1). - inv H8. elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. + unfold f'; intros. destruct (zeq b0 b1). + inversion H8. subst b0 b3 delta0. + elim (fresh_block_alloc _ _ _ _ _ H0). eauto with mem. apply memval_inject_incr with f; auto. - exists (update b1 (Some(b2, delta)) f). split. constructor. + exists f'. split. constructor. (* inj *) - eapply alloc_left_mapped_inj; eauto. apply update_s. + eapply alloc_left_mapped_inj; eauto. unfold f'; apply zeq_true. (* freeblocks *) - unfold update; intros. destruct (zeq b b1). subst b. + unfold f'; intros. destruct (zeq b b1). subst b. elim H9. eauto with mem. eauto with mem. (* mappedblocks *) - unfold update; intros. destruct (zeq b b1). inv H9. auto. - eauto. + unfold f'; intros. destruct (zeq b b1). congruence. eauto. (* overlap *) - unfold update; red; intros. - repeat rewrite (bounds_alloc _ _ _ _ _ H0). unfold eq_block. - destruct (zeq b0 b1); destruct (zeq b3 b1); simpl. - inv H10; inv H11. congruence. - inv H10. destruct (zeq b1' b2'); auto. subst b2'. - right. generalize (H6 _ _ H11). tauto. - inv H11. destruct (zeq b1' b2'); auto. subst b2'. - right. eapply H6; eauto. + unfold f'; red; intros. + exploit perm_alloc_inv. eauto. eexact H12. intros P1. + exploit perm_alloc_inv. eauto. eexact H13. intros P2. + destruct (zeq b0 b1); destruct (zeq b3 b1). + congruence. + inversion H10; subst b0 b1' delta1. + destruct (zeq b2 b2'); auto. subst b2'. right; red; intros. + eapply H6; eauto. omega. + inversion H11; subst b3 b2' delta2. + destruct (zeq b1' b2); auto. subst b1'. right; red; intros. + eapply H6; eauto. omega. eauto. (* range offset *) - unfold update; intros. destruct (zeq b b1). inv H9. auto. eauto. + unfold f'; intros. destruct (zeq b b1). congruence. eauto. (* range block *) - unfold update; intros. destruct (zeq b b1). inv H9. auto. eauto. + unfold f'; intros. destruct (zeq b b1). inversion H9; subst b b' delta0. eauto. eauto. (* incr *) split. auto. (* image of b1 *) - split. apply update_s. + split. unfold f'; apply zeq_true. (* image of others *) - intros. apply update_o; auto. + intros. unfold f'; apply zeq_false; auto. Qed. Theorem alloc_parallel_inject: @@ -3782,11 +3470,10 @@ Proof. instantiate (1 := b2). eauto with mem. instantiate (1 := 0). unfold Int.max_unsigned. generalize Int.modulus_pos; omega. auto. - intros. - apply perm_implies with Freeable; auto with mem. + intros. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. red; intros. apply Zdivide_0. - intros. elimtype False. apply (valid_not_valid_diff m2 b2 b2); eauto with mem. + intros. apply (valid_not_valid_diff m2 b2 b2); eauto with mem. intros [f' [A [B [C D]]]]. exists f'; exists m2'; exists b2; auto. Qed. @@ -3807,7 +3494,7 @@ Proof. (* mappedblocks *) auto. (* no overlap *) - red; intros. repeat rewrite (bounds_free _ _ _ _ _ H0). eauto. + red; intros. eauto with mem. (* range offset *) auto. (* range block *) @@ -3831,8 +3518,8 @@ Lemma free_right_inject: forall f m1 m2 b lo hi m2', inject f m1 m2 -> free m2 b lo hi = Some m2' -> - (forall b1 delta ofs p, - f b1 = Some(b, delta) -> perm m1 b1 ofs p -> + (forall b1 delta ofs k p, + f b1 = Some(b, delta) -> perm m1 b1 ofs k p -> lo <= ofs + delta < hi -> False) -> inject f m1 m2'. Proof. @@ -3848,14 +3535,14 @@ Proof. (* range offset *) auto. (* range blocks *) - intros. rewrite (bounds_free _ _ _ _ _ H0). eauto. + intros. eauto with mem. Qed. Lemma perm_free_list: - forall l m m' b ofs p, + forall l m m' b ofs k p, free_list m l = Some m' -> - perm m' b ofs p -> - perm m b ofs p /\ + perm m' b ofs k p -> + perm m b ofs k p /\ (forall lo hi, In (b, lo, hi) l -> lo <= ofs < hi -> False). Proof. induction l; intros until p; simpl. @@ -3865,7 +3552,7 @@ Proof. exploit IHl; eauto. intros [A B]. split. eauto with mem. intros. destruct H2. inv H2. - elim (perm_free_2 _ _ _ _ _ H ofs p). auto. auto. + elim (perm_free_2 _ _ _ _ _ H ofs k p). auto. auto. eauto. Qed. @@ -3874,9 +3561,9 @@ Theorem free_inject: inject f m1 m2 -> free_list m1 l = Some m1' -> free m2 b lo hi = Some m2' -> - (forall b1 delta ofs p, + (forall b1 delta ofs k p, f b1 = Some(b, delta) -> - perm m1 b1 ofs p -> lo <= ofs + delta < hi -> + perm m1 b1 ofs k p -> lo <= ofs + delta < hi -> exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) -> inject f m1' m2'. Proof. @@ -3887,37 +3574,18 @@ Proof. exploit H2; eauto. intros [lo1 [hi1 [C D]]]. eauto. Qed. -(* -Theorem free_inject': - forall f m1 l m1' m2 b lo hi m2', - inject f m1 m2 -> - free_list m1 l = Some m1' -> - free m2 b lo hi = Some m2' -> - (forall b1 delta, - f b1 = Some(b, delta) -> In (b1, low_bound m1 b1, high_bound m1 b1) l) -> - inject f m1' m2'. -Proof. - intros. eapply free_inject; eauto. - intros. exists (low_bound m1 b1); exists (high_bound m1 b1). - split. eauto. apply perm_in_bounds with p. auto. -Qed. -*) - Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2', inject f m1 m2 -> drop_perm m2 b lo hi p = Some m2' -> - (forall b' delta, + (forall b' delta ofs k p, f b' = Some(b, delta) -> - high_bound m1 b' + delta <= lo - \/ hi <= low_bound m1 b' + delta) -> + perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) -> inject f m1 m2'. Proof. intros. destruct H. constructor; eauto. eapply drop_outside_inj; eauto. - - intros. unfold valid_block in *. erewrite nextblock_drop; eauto. - - intros. erewrite bounds_drop; eauto. + intros. unfold valid_block in *. erewrite nextblock_drop; eauto. + intros. eapply mi_range_block0; eauto. eapply perm_drop_4; eauto. Qed. (** Injecting a memory into itself. *) @@ -3964,11 +3632,14 @@ Theorem empty_inject_neutral: forall thr, inject_neutral thr empty. Proof. intros; red; constructor. +(* perm *) + unfold flat_inj; intros. destruct (zlt b1 thr); inv H. + replace (ofs + 0) with ofs by omega; auto. (* access *) unfold flat_inj; intros. destruct (zlt b1 thr); inv H. replace (ofs + 0) with ofs by omega; auto. (* mem_contents *) - intros; simpl; constructor. + intros; simpl. repeat rewrite ZMap.gi. constructor. Qed. Theorem alloc_inject_neutral: @@ -4026,8 +3697,12 @@ Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes Hint Resolve Mem.valid_not_valid_diff Mem.perm_implies + Mem.perm_cur + Mem.perm_max Mem.perm_valid_block Mem.range_perm_implies + Mem.range_perm_cur + Mem.range_perm_max Mem.valid_access_implies Mem.valid_access_valid_block Mem.valid_access_perm @@ -4059,6 +3734,7 @@ Hint Resolve Mem.perm_alloc_1 Mem.perm_alloc_2 Mem.perm_alloc_3 + Mem.perm_alloc_4 Mem.perm_alloc_inv Mem.valid_access_alloc_other Mem.valid_access_alloc_same diff --git a/common/Memtype.v b/common/Memtype.v index 2e44331..a13e861 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -32,7 +32,8 @@ Require Import Memdata. (** Memory states are accessed by addresses [b, ofs]: pairs of a block identifier [b] and a byte offset [ofs] within that block. - Each address is in one of the following five states: + Each address is associated to permissions, also known as access rights. + The following permissions are expressible: - Freeable (exclusive access): all operations permitted - Writable: load, store and pointer comparison operations are permitted, but freeing is not. @@ -67,6 +68,21 @@ Proof. intros. inv H; inv H0; constructor. Qed. +(** Each address has not one, but two permissions associated + with it. The first is the current permission. It governs whether + operations (load, store, free, etc) over this address succeed or + not. The other is the maximal permission. It is always at least as + strong as the current permission. Once a block is allocated, the + maximal permission of an address within this block can only + decrease, as a result of [free] or [drop_perm] operations, or of + external calls. In contrast, the current permission of an address + can be temporarily lowered by an external call, then raised again by + another external call. *) + +Inductive perm_kind: Type := + | Max: perm_kind + | Cur: perm_kind. + Module Type MEM. (** The abstract type of memory states. *) @@ -143,8 +159,8 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem := end. (** [drop_perm m b lo hi p] sets the permissions of the byte range - [(b, lo) ... (b, hi - 1)] to [p]. These bytes must have permissions - at least [p] in the initial memory state [m]. + [(b, lo) ... (b, hi - 1)] to [p]. These bytes must have [Freeable] permissions + in the initial memory state [m]. Returns updated memory state, or [None] if insufficient permissions. *) Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), option mem. @@ -168,41 +184,52 @@ Definition valid_block (m: mem) (b: block) := Axiom valid_not_valid_diff: forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'. -(** [perm m b ofs p] holds if the address [b, ofs] in memory state [m] - has permission [p]: one of writable, readable, and nonempty. - If the address is empty, [perm m b ofs p] is false for all values of [p]. *) -Parameter perm: forall (m: mem) (b: block) (ofs: Z) (p: permission), Prop. +(** [perm m b ofs k p] holds if the address [b, ofs] in memory state [m] + has permission [p]: one of freeable, writable, readable, and nonempty. + If the address is empty, [perm m b ofs p] is false for all values of [p]. + [k] is the kind of permission we are interested in: either the current + permissions or the maximal permissions. *) +Parameter perm: forall (m: mem) (b: block) (ofs: Z) (k: perm_kind) (p: permission), Prop. (** Logical implications between permissions *) Axiom perm_implies: - forall m b ofs p1 p2, perm m b ofs p1 -> perm_order p1 p2 -> perm m b ofs p2. + forall m b ofs k p1 p2, perm m b ofs k p1 -> perm_order p1 p2 -> perm m b ofs k p2. + +(** The current permission is always less than or equal to the maximal permission. *) + +Axiom perm_cur_max: + forall m b ofs p, perm m b ofs Cur p -> perm m b ofs Max p. +Axiom perm_cur: + forall m b ofs k p, perm m b ofs Cur p -> perm m b ofs k p. +Axiom perm_max: + forall m b ofs k p, perm m b ofs k p -> perm m b ofs Max p. (** Having a (nonempty) permission implies that the block is valid. In other words, invalid blocks, not yet allocated, are all empty. *) Axiom perm_valid_block: - forall m b ofs p, perm m b ofs p -> valid_block m b. + forall m b ofs k p, perm m b ofs k p -> valid_block m b. (* Unused? (** The [Mem.perm] predicate is decidable. *) Axiom perm_dec: - forall m b ofs p, {perm m b ofs p} + {~ perm m b ofs p}. + forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}. *) (** [range_perm m b lo hi p] holds iff the addresses [b, lo] to [b, hi-1] - all have permission [p]. *) -Definition range_perm (m: mem) (b: block) (lo hi: Z) (p: permission) : Prop := - forall ofs, lo <= ofs < hi -> perm m b ofs p. + all have permission [p] of kind [k]. *) +Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop := + forall ofs, lo <= ofs < hi -> perm m b ofs k p. Axiom range_perm_implies: - forall m b lo hi p1 p2, - range_perm m b lo hi p1 -> perm_order p1 p2 -> range_perm m b lo hi p2. + forall m b lo hi k p1 p2, + range_perm m b lo hi k p1 -> perm_order p1 p2 -> range_perm m b lo hi k p2. (** An access to a memory quantity [chunk] at address [b, ofs] with permission [p] is valid in [m] if the accessed addresses all have - permission [p] and moreover the offset is properly aligned. *) + current permission [p] and moreover the offset is properly aligned. *) Definition valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) (p: permission): Prop := - range_perm m b ofs (ofs + size_chunk chunk) p + range_perm m b ofs (ofs + size_chunk chunk) Cur p /\ (align_chunk chunk | ofs). Axiom valid_access_implies: @@ -216,9 +243,9 @@ Axiom valid_access_valid_block: valid_block m b. Axiom valid_access_perm: - forall m chunk b ofs p, + forall m chunk b ofs k p, valid_access m chunk b ofs p -> - perm m b ofs p. + perm m b ofs k p. (** [valid_pointer m b ofs] returns [true] if the address [b, ofs] is nonempty in [m] and [false] if it is empty. *) @@ -227,41 +254,17 @@ Parameter valid_pointer: forall (m: mem) (b: block) (ofs: Z), bool. Axiom valid_pointer_nonempty_perm: forall m b ofs, - valid_pointer m b ofs = true <-> perm m b ofs Nonempty. + valid_pointer m b ofs = true <-> perm m b ofs Cur Nonempty. Axiom valid_pointer_valid_access: forall m b ofs, valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty. -(** Each block has associated low and high bounds. These are the bounds - that were given when the block was allocated. *) - -Parameter bounds: forall (m: mem) (b: block), Z*Z. - -Notation low_bound m b := (fst(bounds m b)). -Notation high_bound m b := (snd(bounds m b)). - -(** The crucial properties of bounds is that any offset below the low - bound or above the high bound is empty. *) - -Axiom perm_in_bounds: - forall m b ofs p, perm m b ofs p -> low_bound m b <= ofs < high_bound m b. - -Axiom range_perm_in_bounds: - forall m b lo hi p, - range_perm m b lo hi p -> lo < hi -> - low_bound m b <= lo /\ hi <= high_bound m b. - -Axiom valid_access_in_bounds: - forall m chunk b ofs p, - valid_access m chunk b ofs p -> - low_bound m b <= ofs /\ ofs + size_chunk chunk <= high_bound m b. - (** * Properties of the memory operations *) (** ** Properties of the initial memory state. *) Axiom nextblock_empty: nextblock empty = 1. -Axiom perm_empty: forall b ofs p, ~perm empty b ofs p. +Axiom perm_empty: forall b ofs k p, ~perm empty b ofs k p. Axiom valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. @@ -315,12 +318,12 @@ Axiom load_int16_signed_unsigned: Axiom range_perm_loadbytes: forall m b ofs len, - range_perm m b ofs (ofs + len) Readable -> + range_perm m b ofs (ofs + len) Cur Readable -> exists bytes, loadbytes m b ofs len = Some bytes. Axiom loadbytes_range_perm: forall m b ofs len bytes, loadbytes m b ofs len = Some bytes -> - range_perm m b ofs (ofs + len) Readable. + range_perm m b ofs (ofs + len) Cur Readable. (** If [loadbytes] succeeds, the corresponding [load] succeeds and returns a value that is determined by the @@ -384,10 +387,10 @@ Axiom store_valid_block_2: Axiom perm_store_1: forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> - forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p. + forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p. Axiom perm_store_2: forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> - forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p. + forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p. Axiom valid_access_store: forall m1 chunk b ofs v, @@ -405,10 +408,6 @@ Axiom store_valid_access_3: forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> valid_access m1 chunk b ofs Writable. -Axiom bounds_store: - forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> - forall b', bounds m2 b' = bounds m1 b'. - (** Load-store properties. *) Axiom load_store_similar: @@ -502,17 +501,17 @@ Axiom store_float32_truncate: Axiom range_perm_storebytes: forall m1 b ofs bytes, - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable -> + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable -> { m2 : mem | storebytes m1 b ofs bytes = Some m2 }. Axiom storebytes_range_perm: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> - range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable. + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable. Axiom perm_storebytes_1: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> - forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p. + forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p. Axiom perm_storebytes_2: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> - forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p. + forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p. Axiom storebytes_valid_access_1: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> forall chunk' b' ofs' p, @@ -530,9 +529,6 @@ Axiom storebytes_valid_block_1: Axiom storebytes_valid_block_2: forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> forall b', valid_block m2 b' -> valid_block m1 b'. -Axiom bounds_storebytes: - forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> - forall b', bounds m2 b' = bounds m1 b'. (** Connections between [store] and [storebytes]. *) @@ -581,8 +577,6 @@ Axiom storebytes_split: exists m1, storebytes m b ofs bytes1 = Some m1 /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2. -Axiom storebytes_empty: - forall m b ofs, storebytes m b ofs nil = Some m. (** ** Properties of [alloc]. *) @@ -616,18 +610,21 @@ Axiom valid_block_alloc_inv: Axiom perm_alloc_1: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - forall b' ofs p, perm m1 b' ofs p -> perm m2 b' ofs p. + forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p. Axiom perm_alloc_2: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - forall ofs, lo <= ofs < hi -> perm m2 b ofs Freeable. + forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable. Axiom perm_alloc_3: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - forall ofs p, ofs < lo \/ hi <= ofs -> ~perm m2 b ofs p. + forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi. +Axiom perm_alloc_4: + forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> + forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p. Axiom perm_alloc_inv: forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - forall b' ofs p, - perm m2 b' ofs p -> - if zeq b' b then lo <= ofs < hi else perm m1 b' ofs p. + forall b' ofs k p, + perm m2 b' ofs k p -> + if zeq b' b then lo <= ofs < hi else perm m1 b' ofs k p. (** Effect of [alloc] on access validity. *) @@ -649,20 +646,6 @@ Axiom valid_access_alloc_inv: then lo <= ofs /\ ofs + size_chunk chunk <= hi /\ (align_chunk chunk | ofs) else valid_access m1 chunk b' ofs p. -(** Effect of [alloc] on bounds. *) - -Axiom bounds_alloc: - forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - forall b', bounds m2 b' = if eq_block b' b then (lo, hi) else bounds m1 b'. - -Axiom bounds_alloc_same: - forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - bounds m2 b = (lo, hi). - -Axiom bounds_alloc_other: - forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) -> - forall b', b' <> b -> bounds m2 b' = bounds m1 b'. - (** Load-alloc properties. *) Axiom load_alloc_unchanged: @@ -689,15 +672,15 @@ Axiom load_alloc_same': (** ** Properties of [free]. *) (** [free] succeeds if and only if the correspond range of addresses - has [Freeable] permission. *) + has [Freeable] current permission. *) Axiom range_perm_free: forall m1 b lo hi, - range_perm m1 b lo hi Freeable -> + range_perm m1 b lo hi Cur Freeable -> { m2: mem | free m1 b lo hi = Some m2 }. Axiom free_range_perm: forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 -> - range_perm m1 bf lo hi Freeable. + range_perm m1 bf lo hi Cur Freeable. (** Block validity is preserved by [free]. *) @@ -715,17 +698,17 @@ Axiom valid_block_free_2: Axiom perm_free_1: forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 -> - forall b ofs p, + forall b ofs k p, b <> bf \/ ofs < lo \/ hi <= ofs -> - perm m1 b ofs p -> - perm m2 b ofs p. + perm m1 b ofs k p -> + perm m2 b ofs k p. Axiom perm_free_2: forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 -> - forall ofs p, lo <= ofs < hi -> ~ perm m2 bf ofs p. + forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p. Axiom perm_free_3: forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 -> - forall b ofs p, - perm m2 b ofs p -> perm m1 b ofs p. + forall b ofs k p, + perm m2 b ofs k p -> perm m1 b ofs k p. (** Effect of [free] on access validity. *) @@ -751,12 +734,6 @@ Axiom valid_access_free_inv_2: valid_access m2 chunk bf ofs p -> lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs. -(** [free] preserves bounds. *) - -Axiom bounds_free: - forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 -> - forall b, bounds m2 b = bounds m1 b. - (** Load-free properties *) Axiom load_free: @@ -770,30 +747,32 @@ Axiom load_free: Axiom nextblock_drop: forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> nextblock m' = nextblock m. +Axiom drop_perm_valid_block_1: + forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> + forall b', valid_block m b' -> valid_block m' b'. +Axiom drop_perm_valid_block_2: + forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> + forall b', valid_block m' b' -> valid_block m b'. Axiom range_perm_drop_1: forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> - range_perm m b lo hi p. + range_perm m b lo hi Cur Freeable. Axiom range_perm_drop_2: forall m b lo hi p, - range_perm m b lo hi p -> { m' | drop_perm m b lo hi p = Some m' }. + range_perm m b lo hi Cur Freeable -> { m' | drop_perm m b lo hi p = Some m' }. Axiom perm_drop_1: forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> - forall ofs, lo <= ofs < hi -> perm m' b ofs p. + forall ofs k, lo <= ofs < hi -> perm m' b ofs k p. Axiom perm_drop_2: forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> - forall ofs p', lo <= ofs < hi -> perm m' b ofs p' -> perm_order p p'. + forall ofs k p', lo <= ofs < hi -> perm m' b ofs k p' -> perm_order p p'. Axiom perm_drop_3: forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> - forall b' ofs p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs p' -> perm m' b' ofs p'. + forall b' ofs k p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs k p' -> perm m' b' ofs k p'. Axiom perm_drop_4: forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> - forall b' ofs p', perm m' b' ofs p' -> perm m b' ofs p'. - -Axiom bounds_drop: - forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> - forall b', bounds m' b' = bounds m b'. + forall b' ofs k p', perm m' b' ofs k p' -> perm m b' ofs k p'. Axiom load_drop: forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> @@ -848,7 +827,7 @@ Axiom store_outside_extends: forall chunk m1 m2 b ofs v m2', extends m1 m2 -> store chunk m2 b ofs v = Some m2' -> - ofs + size_chunk chunk <= low_bound m1 b \/ high_bound m1 b <= ofs -> + (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + size_chunk chunk -> False) -> extends m1 m2'. Axiom storev_extends: @@ -874,7 +853,7 @@ Axiom storebytes_outside_extends: forall m1 m2 b ofs bytes2 m2', extends m1 m2 -> storebytes m2 b ofs bytes2 = Some m2' -> - ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs -> + (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) -> extends m1 m2'. Axiom alloc_extends: @@ -896,7 +875,7 @@ Axiom free_right_extends: forall m1 m2 b lo hi m2', extends m1 m2 -> free m2 b lo hi = Some m2' -> - (forall ofs p, lo <= ofs < hi -> ~perm m1 b ofs p) -> + (forall ofs k p, perm m1 b ofs k p -> lo <= ofs < hi -> False) -> extends m1 m2'. Axiom free_parallel_extends: @@ -912,8 +891,8 @@ Axiom valid_block_extends: extends m1 m2 -> (valid_block m1 b <-> valid_block m2 b). Axiom perm_extends: - forall m1 m2 b ofs p, - extends m1 m2 -> perm m1 b ofs p -> perm m2 b ofs p. + forall m1 m2 b ofs k p, + extends m1 m2 -> perm m1 b ofs k p -> perm m2 b ofs k p. Axiom valid_access_extends: forall m1 m2 chunk b ofs p, extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p. @@ -952,10 +931,10 @@ Axiom valid_block_inject_2: valid_block m2 b2. Axiom perm_inject: - forall f m1 m2 b1 b2 delta ofs p, + forall f m1 m2 b1 b2 delta ofs k p, f b1 = Some(b2, delta) -> inject f m1 m2 -> - perm m1 b1 ofs p -> perm m2 b2 (ofs + delta) p. + perm m1 b1 ofs k p -> perm m2 b2 (ofs + delta) k p. Axiom valid_access_inject: forall f m1 m2 chunk b1 ofs b2 delta p, @@ -974,7 +953,7 @@ Axiom valid_pointer_inject: Axiom address_inject: forall f m1 m2 b1 ofs1 b2 delta, inject f m1 m2 -> - perm m1 b1 (Int.unsigned ofs1) Nonempty -> + perm m1 b1 (Int.unsigned ofs1) Max Nonempty -> f b1 = Some (b2, delta) -> Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. @@ -998,8 +977,8 @@ Axiom inject_no_overlap: b1 <> b2 -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> - perm m1 b1 ofs1 Nonempty -> - perm m1 b2 ofs2 Nonempty -> + perm m1 b1 ofs1 Max Nonempty -> + perm m1 b2 ofs2 Max Nonempty -> b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2. Axiom different_pointers_inject: @@ -1056,10 +1035,10 @@ Axiom store_unmapped_inject: Axiom store_outside_inject: forall f m1 m2 chunk b ofs v m2', inject f m1 m2 -> - (forall b' delta, + (forall b' delta ofs', f b' = Some(b, delta) -> - high_bound m1 b' + delta <= ofs - \/ ofs + size_chunk chunk <= low_bound m1 b' + delta) -> + perm m1 b' ofs' Cur Readable -> + ofs <= ofs' + delta < ofs + size_chunk chunk -> False) -> store chunk m2 b ofs v = Some m2' -> inject f m1 m2'. @@ -1092,10 +1071,10 @@ Axiom storebytes_unmapped_inject: Axiom storebytes_outside_inject: forall f m1 m2 b ofs bytes2 m2', inject f m1 m2 -> - (forall b' delta, + (forall b' delta ofs', f b' = Some(b, delta) -> - high_bound m1 b' + delta <= ofs - \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) -> + perm m1 b' ofs' Cur Readable -> + ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) -> storebytes m2 b ofs bytes2 = Some m2' -> inject f m1 m2'. @@ -1124,13 +1103,13 @@ Axiom alloc_left_mapped_inject: alloc m1 lo hi = (m1', b1) -> valid_block m2 b2 -> 0 <= delta <= Int.max_unsigned -> - delta = 0 \/ 0 <= low_bound m2 b2 /\ high_bound m2 b2 <= Int.max_unsigned -> - (forall ofs p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) p) -> + (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs <= Int.max_unsigned) -> + (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) -> inj_offset_aligned delta (hi-lo) -> - (forall b ofs, - f b = Some (b2, ofs) -> - high_bound m1 b + ofs <= lo + delta \/ - hi + delta <= low_bound m1 b + ofs) -> + (forall b delta' ofs k p, + f b = Some (b2, delta') -> + perm m1 b ofs k p -> + lo + delta <= ofs + delta' < hi + delta -> False) -> exists f', inject f' m1' m2 /\ inject_incr f f' @@ -1154,8 +1133,8 @@ Axiom free_inject: inject f m1 m2 -> free_list m1 l = Some m1' -> free m2 b lo hi = Some m2' -> - (forall b1 delta ofs p, - f b1 = Some(b, delta) -> perm m1 b1 ofs p -> lo <= ofs + delta < hi -> + (forall b1 delta ofs k p, + f b1 = Some(b, delta) -> perm m1 b1 ofs k p -> lo <= ofs + delta < hi -> exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) -> inject f m1' m2'. @@ -1163,10 +1142,9 @@ Axiom drop_outside_inject: forall f m1 m2 b lo hi p m2', inject f m1 m2 -> drop_perm m2 b lo hi p = Some m2' -> - (forall b' delta, + (forall b' delta ofs k p, f b' = Some(b, delta) -> - high_bound m1 b' + delta <= lo - \/ hi <= low_bound m1 b' + delta) -> + perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) -> inject f m1 m2'. (** Memory states that inject into themselves. *) -- cgit v1.2.3