From f7270a57205abd7314203eaef9b752a7abd13ed7 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 21 Sep 2010 07:34:06 +0000 Subject: Memory.v: added drop_perm operation Globalenvs.v: used drop_perm to set appropriate permissions on global variables (Notempty if volatile; Readable if readonly; Writable otherwise) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1510 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Globalenvs.v | 86 ++++++++++---- common/Memory.v | 337 ++++++++++++++++++++++++++++++++++++++++++++++++---- common/Memtype.v | 50 ++++++++ 3 files changed, 427 insertions(+), 46 deletions(-) (limited to 'common') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index a29c249..4a57a37 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -523,10 +523,18 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := | i :: il' => init_data_size i + init_data_list_size il' end. +Definition perm_globvar (gv: globvar V) : permission := + if gv.(gvar_volatile) then Nonempty + else if gv.(gvar_readonly) then Readable + else Writable. + Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem := let init := idv#2.(gvar_init) in let (m', b) := Mem.alloc m 0 (init_data_list_size init) in - store_init_data_list m' b 0 init. + match store_init_data_list m' b 0 init with + | None => None + | Some m'' => Mem.drop_perm m'' b 0 (init_data_list_size init) (perm_globvar idv#2) + end. Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) {struct vl} : option mem := @@ -564,8 +572,11 @@ Proof. unfold alloc_variable. set (init := gvar_init a#2). caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC. - rewrite (IHvl _ _ REC). + caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE. + caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. + intros m3 DROP REC. + rewrite (IHvl _ _ REC). + rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. @@ -595,8 +606,12 @@ Proof. intros until m'. simpl. unfold alloc_variable. set (init := gvar_init a#2). caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC PERM. - eapply IHvl; eauto. + caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE. + caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. + intros m3 DROP REC PERM. + 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. eauto with mem. Qed. @@ -685,13 +700,19 @@ Proof. unfold alloc_variable. set (init := gvar_init a#2). caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC. - caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO REC VAL. + caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO. + caseEq (Mem.drop_perm m2 b1 0 (init_data_list_size init) (perm_globvar a#2)); try congruence. + intros m3 DROP RED VALID. + assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem. + transitivity (Mem.load chunk m3 b p). + apply IHvl; auto. red. + rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ STO). + change (Mem.valid_block m1 b). eauto with mem. transitivity (Mem.load chunk m2 b p). - apply IHvl; auto. red. rewrite (store_init_data_list_nextblock _ _ _ _ STO). - change (Mem.valid_block m1 b). eauto with mem. + eapply Mem.load_drop; eauto. transitivity (Mem.load chunk m1 b p). - eapply store_init_data_list_outside; eauto. left. - apply Mem.valid_not_valid_diff with m; eauto with mem. + eapply store_init_data_list_outside; eauto. eapply Mem.load_alloc_unchanged; eauto. Qed. @@ -714,8 +735,8 @@ Lemma alloc_variables_charact: 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)) Writable - /\ load_store_init_data m' b 0 gv.(gvar_init). + /\ 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. @@ -724,7 +745,9 @@ Proof. caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence. intros m1 b ALLOC. caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence. - intros m2 STORE REC NOREPET IN. inv NOREPET. + intros m2 STORE. + caseEq (Mem.drop_perm m2 b 0 (init_data_list_size (gvar_init gv')) (perm_globvar gv')); try congruence. + intros m3 DROP REC NOREPET IN. inv NOREPET. exploit Mem.alloc_result; eauto. intro BEQ. destruct IN. inv H. exists (Mem.nextblock m); split. @@ -733,17 +756,24 @@ Proof. split. rewrite add_variables_same_address. unfold find_var_info; simpl. rewrite NEXT. apply ZMap.gss. simpl. rewrite <- NEXT; omega. - split. red; intros. eapply alloc_variables_perm; eauto. - eapply store_init_data_list_perm; eauto. - apply Mem.perm_implies with Freeable; eauto with mem. + split. red; intros. + eapply alloc_variables_perm; eauto. + eapply Mem.perm_drop_1; eauto. + intros NOVOL. apply load_store_init_data_invariant with m2. - intros. eapply load_alloc_variables; eauto. - red. rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + intros. transitivity (Mem.load chunk m3 (Mem.nextblock m) ofs). + eapply load_alloc_variables; eauto. + red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ STORE). change (Mem.valid_block m1 (Mem.nextblock m)). eauto with mem. + eapply Mem.load_drop; eauto. repeat right. + unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv); auto with mem. eapply store_init_data_list_charact; eauto. - apply IHvl with m2; auto. - simpl. rewrite (store_init_data_list_nextblock _ _ _ _ STORE). + apply IHvl with m3; auto. + simpl. + rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). + rewrite (store_init_data_list_nextblock _ _ _ _ STORE). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega. Qed. @@ -785,8 +815,8 @@ Theorem find_var_exists: 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)) Writable - /\ 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)) (perm_globvar gv) + /\ (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. @@ -839,11 +869,15 @@ Lemma alloc_variable_neutral: Mem.inject_neutral thr m'. Proof. intros until m'. unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b; intros. + caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b ALLOC. + caseEq (store_init_data_list ge m1 b 0 (gvar_init id#2)); try congruence. + intros m2 STORE DROP NEUTRAL NEXT. + eapply Mem.drop_inject_neutral; eauto. eapply store_init_data_list_neutral with (b := b). eapply Mem.alloc_inject_neutral; eauto. - rewrite (Mem.alloc_result _ _ _ _ _ H). auto. + rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. eauto. + rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto. Qed. Lemma alloc_variables_neutral: @@ -1067,6 +1101,10 @@ Proof. destruct (Mem.alloc m 0 (init_data_list_size init)). rewrite store_init_data_list_match. destruct (store_init_data_list (globalenv p) m0 b 0 init); auto. + change (perm_globvar (mkglobvar info2 init ro vo)) + with (perm_globvar (mkglobvar info1 init ro vo)). + destruct (Mem.drop_perm m1 b 0 (init_data_list_size init) + (perm_globvar (mkglobvar info1 init ro vo))); auto. Qed. Theorem init_mem_match: diff --git a/common/Memory.v b/common/Memory.v index 0e9fbfa..6de00e7 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -440,7 +440,6 @@ Next Obligation. Qed. Next Obligation. unfold clearN, update. -(* destruct (noread_undef m b0 ofs); auto.*) destruct (zeq b0 b). subst b0. destruct (zle lo ofs); simpl; auto. destruct (zlt ofs hi); simpl; auto. @@ -546,16 +545,21 @@ Proof. apply IHvl. Qed. +Remark getN_exten: + forall c1 c2 n p, + (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. + apply H. omega. apply IHn. intros. apply H. omega. +Qed. + Remark getN_setN_outside: forall vl q c n p, p + Z_of_nat n <= q \/ q + Z_of_nat (length vl) <= p -> getN n p (setN vl q c) = getN n p c. Proof. - induction n; intros; simpl. - auto. - rewrite inj_S in H. decEq. - apply setN_outside. omega. - apply IHn. omega. + intros. apply getN_exten. intros. apply setN_outside. omega. Qed. Lemma store_noread_undef: @@ -564,20 +568,19 @@ Lemma store_noread_undef: 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 as [? _]. -(*specialize (H ofs').*) -unfold update. -destruct (zeq b' b). -subst b'. -assert (ofs <= ofs' < ofs + size_chunk ch \/ (ofs' < ofs \/ ofs' >= ofs + size_chunk ch)) by omega. -destruct H0. -exploit (H ofs'); auto; intro. -eauto with mem. -rewrite setN_outside. -destruct (noread_undef m b ofs'); auto. -rewrite encode_val_length. rewrite <- size_chunk_conv; auto. -destruct (noread_undef m b' ofs'); auto. + intros. + destruct VA as [? _]. + unfold update. + destruct (zeq b' b). + subst b'. + assert (ofs <= ofs' < ofs + size_chunk ch \/ (ofs' < ofs \/ ofs' >= ofs + size_chunk ch)) by omega. + destruct H0. + exploit (H ofs'); auto; intro. + eauto with mem. + rewrite setN_outside. + destruct (noread_undef m b ofs'); auto. + rewrite encode_val_length. rewrite <- size_chunk_conv; auto. + destruct (noread_undef m b' ofs'); auto. Qed. (** [store chunk m b ofs v] perform a write in memory state [m]. @@ -588,8 +591,8 @@ Qed. 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)) + (setN (encode_val chunk v) ofs (m.(mem_contents) b)) + m.(mem_contents)) m.(mem_access) m.(bounds) m.(nextblock) @@ -609,6 +612,44 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := | _ => 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]. + 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) + m.(mem_access)) + m.(bounds) m.(nextblock) _ _ _ _) + else None. +Next Obligation. + destruct m; auto. +Qed. +Next Obligation. + destruct m; auto. +Qed. +Next Obligation. + unfold update. destruct (zeq 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. +Qed. + (** * Properties of the memory operations *) (** Properties of the empty store. *) @@ -1694,6 +1735,148 @@ Hint Local 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. +Proof. + unfold drop_perm; intros. + destruct (range_perm_dec m b lo hi p). 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' }. +Proof. + unfold drop_perm; intros. + destruct (range_perm_dec m b lo hi p). econstructor. eauto. contradiction. +Qed. + +Section DROP. + +Variable m: mem. +Variable b: block. +Variable lo hi: Z. +Variable p: permission. +Variable m': mem. +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. +Qed. + +Theorem perm_drop_1: + forall ofs, lo <= ofs < hi -> perm m' b ofs 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. + 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'. +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. + 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'. +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 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'. +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). + subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). + simpl. intros. apply perm_implies with p. apply r. tauto. 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' -> + valid_access m chunk b' ofs p' -> valid_access m' chunk b' ofs p'. +Proof. + intros. destruct H0. split; auto. + red; intros. + destruct (zeq b' b). subst b'. + destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. + destruct (zle hi ofs0). eapply perm_drop_3; eauto. + apply perm_implies with p. eapply perm_drop_1; eauto. omega. + generalize (size_chunk_pos chunk); intros. intuition. omegaContradiction. omegaContradiction. + eapply perm_drop_3; eauto. +Qed. + +Lemma valid_access_drop_2: + forall chunk b' ofs p', + valid_access m' chunk b' ofs p' -> valid_access m chunk b' ofs p'. +Proof. + intros. destruct H; split; auto. + red; intros. eapply perm_drop_4; eauto. +Qed. + +(* +Lemma valid_access_drop_3: + forall chunk b' ofs p', + valid_access m' chunk b' ofs p' -> + b' <> b \/ Intv.disjoint (lo, hi) (ofs, ofs + size_chunk chunk) \/ perm_order p p'. +Proof. + intros. destruct H. + destruct (zeq b' b); auto. subst b'. + destruct (Intv.disjoint_dec (lo, hi) (ofs, ofs + size_chunk chunk)); auto. + exploit intv_not_disjoint; eauto. intros [x [A B]]. + right; right. apply perm_drop_2 with x. auto. apply H. auto. +Qed. +*) + +Theorem load_drop: + forall chunk b' ofs, + b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p Readable -> + load chunk m' b' ofs = load chunk m b' ofs. +Proof. + intros. + 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. + eapply valid_access_drop_1; eauto. + rewrite pred_dec_false. auto. + red; intros; elim n. eapply valid_access_drop_2; eauto. +Qed. + +End DROP. + (** * Extensionality properties *) Lemma mem_access_ext: @@ -2109,6 +2292,103 @@ Proof. rewrite (clearN_out _ _ _ _ _ _ H4); auto. Qed. +(** Preservation of [drop_perm] operations. *) + +Lemma drop_unmapped_inj: + forall f m1 m2 b lo hi p m1', + mem_inj f m1 m2 -> + drop_perm m1 b lo hi p = Some m1' -> + f b = None -> + mem_inj f m1' m2. +Proof. + intros. inv H. constructor. + intros. eapply mi_access0. eauto. + eapply valid_access_drop_2; eauto. + intros. replace (mem_contents m1' b1 ofs) with (mem_contents m1 b1 ofs). + apply mi_memval0; auto. + eapply perm_drop_4; eauto. + unfold drop_perm in H0. destruct (range_perm_dec m1 b lo hi p); inv H0. + simpl. rewrite update_o; auto. congruence. +Qed. + +Lemma drop_mapped_inj: + forall f m1 m2 b1 b2 delta lo hi p m1', + mem_inj f m1 m2 -> + drop_perm m1 b1 lo hi p = Some m1' -> + meminj_no_overlap f m1 -> + f b1 = Some(b2, delta) -> + exists m2', + drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2' + /\ mem_inj f m1' m2'. +Proof. + intros. + assert ({ m2' | drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2' }). + apply range_perm_drop_2. red; intros. + replace ofs with ((ofs - delta) + delta) by omega. + eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. omega. + destruct X as [m2' DROP]. exists m2'; split; auto. + inv H. constructor; intros. +(* access *) + 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. +(* 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. +Qed. + (** * Memory extensions *) (** A store [m2] extends a store [m1] if [m2] can be obtained from [m1] @@ -3030,6 +3310,19 @@ Proof. intros [m'' [A B]]. congruence. Qed. +Theorem drop_inject_neutral: + forall m b lo hi p m' thr, + drop_perm m b lo hi p = Some m' -> + inject_neutral thr m -> + b < thr -> + inject_neutral thr m'. +Proof. + unfold inject_neutral; intros. + exploit drop_mapped_inj; eauto. apply flat_inj_no_overlap. + unfold flat_inj. apply zlt_true; eauto. + repeat rewrite Zplus_0_r. intros [m'' [A B]]. congruence. +Qed. + End Mem. Notation mem := Mem.mem. diff --git a/common/Memtype.v b/common/Memtype.v index cbf3ffe..050cc84 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -137,6 +137,13 @@ Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem := end 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]. + Returns updated memory state, or [None] if insufficient permissions. *) + +Parameter drop_perm: forall (m: mem) (b: block) (lo hi: Z) (p: permission), option mem. + (** * Permissions, block validity, access validity, and bounds *) (** The next block of a memory state is the block identifier for the @@ -647,6 +654,42 @@ Axiom load_free: b <> bf \/ lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs -> load chunk m2 b ofs = load chunk m1 b ofs. +(** ** Properties of [drop_perm]. *) + +Axiom nextblock_drop: + forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> + nextblock m' = nextblock m. + +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. +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' }. + +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. +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'. +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'. +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'. + +Axiom load_drop: + forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> + forall chunk b' ofs, + b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p Readable -> + load chunk m' b' ofs = load chunk m b' ofs. + (** * Relating two memory states. *) (** ** Memory extensions *) @@ -973,4 +1016,11 @@ Axiom store_inject_neutral: val_inject (flat_inj thr) v v -> inject_neutral thr m'. +Axiom drop_inject_neutral: + forall m b lo hi p m' thr, + drop_perm m b lo hi p = Some m' -> + inject_neutral thr m -> + b < thr -> + inject_neutral thr m'. + End MEM. -- cgit v1.2.3