From 34a35d283bf068016a7f309367e9d9c3da82f9fa Mon Sep 17 00:00:00 2001 From: Timothy Bourke Date: Thu, 9 Feb 2017 17:34:16 +0100 Subject: Add range_w for writeable static variables --- common/Separation.v | 191 ++++++++++++++++++++++++++++++++-------------------- x86/Stacklayout.v | 2 +- 2 files changed, 119 insertions(+), 74 deletions(-) diff --git a/common/Separation.v b/common/Separation.v index c4a46b6a..1176edf5 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -338,21 +338,37 @@ Proof. simpl; intros. intuition auto. Qed. -(** A range of bytes, with full permissions and unspecified contents. *) +(** A range of bytes with unspecified contents, and either full permissions + (f = true) or only writable permissions (f = false). *) -Program Definition range (b: block) (lo hi: Z) : massert := {| +Program Definition range' (f: bool) (b: block) (lo hi: Z) : massert := {| m_pred := fun m => 0 <= lo /\ hi <= Ptrofs.modulus - /\ (forall i k p, lo <= i < hi -> Mem.perm m b i k p); + /\ (forall i k, lo <= i < hi -> Mem.perm m b i k + (if f then Freeable else Writable)); m_footprint := fun b' ofs' => b' = b /\ lo <= ofs' < hi |}. Next Obligation. split; auto. split; auto. intros. eapply Mem.perm_unchanged_on; eauto. simpl; auto. Qed. Next Obligation. - apply Mem.perm_valid_block with ofs Cur Freeable; auto. + eapply Mem.perm_valid_block with ofs Cur _; auto. Qed. +Notation range := (range' true). +Notation range_w := (range' false). + +Lemma range_range_w: + forall b lo hi, + massert_imp (range b lo hi) (range_w b lo hi). +Proof. + constructor; auto. + destruct 1 as (Hlo & Hhi & Hperm). + repeat split; auto. + intros i k Hoff. + eapply Mem.perm_implies; eauto using perm_F_any. +Qed. + Lemma alloc_rule: forall m lo hi b m' P, Mem.alloc m lo hi = (m', b) -> @@ -391,10 +407,10 @@ Proof. Qed. Lemma range_split': - forall b lo hi mid, + forall {f} b lo hi mid, lo <= mid <= hi -> - massert_eqv (range b lo hi) - (range b lo mid ** range b mid hi). + massert_eqv (range' f b lo hi) + (range' f b lo mid ** range' f b mid hi). Proof. intros * HR. constructor; constructor. @@ -416,17 +432,17 @@ Proof. constructor; repeat split. + assumption. + assumption. - + intros i k p Hi. + + intros i k Hi. destruct (Z.lt_ge_cases i mid); intuition. - intros * Hfoot. simpl in *. destruct (Z.lt_ge_cases ofs mid); intuition. Qed. Lemma range_split: - forall b lo hi P mid m, + forall {f} b lo hi P mid m, lo <= mid <= hi -> - m |= range b lo hi ** P -> - m |= range b lo mid ** range b mid hi ** P. + m |= range' f b lo hi ** P -> + m |= range' f b lo mid ** range' f b mid hi ** P. Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. split; simpl; intros. @@ -440,29 +456,29 @@ Proof. Qed. Lemma range_drop_left: - forall b lo hi P mid m, + forall {f} b lo hi P mid m, lo <= mid <= hi -> - m |= range b lo hi ** P -> - m |= range b mid hi ** P. + m |= range' f b lo hi ** P -> + m |= range' f b mid hi ** P. Proof. - intros. apply sep_drop with (range b lo mid). apply range_split; auto. + intros. apply sep_drop with (range' f b lo mid). apply range_split; auto. Qed. Lemma range_drop_right: - forall b lo hi P mid m, + forall {f} b lo hi P mid m, lo <= mid <= hi -> - m |= range b lo hi ** P -> - m |= range b lo mid ** P. + m |= range' f b lo hi ** P -> + m |= range' f b lo mid ** P. Proof. - intros. apply sep_drop2 with (range b mid hi). apply range_split; auto. + intros. apply sep_drop2 with (range' f b mid hi). apply range_split; auto. Qed. Lemma range_split_2: - forall b lo hi P mid al m, + forall {f} b lo hi P mid al m, lo <= align mid al <= hi -> al > 0 -> - m |= range b lo hi ** P -> - m |= range b lo mid ** range b (align mid al) hi ** P. + m |= range' f b lo hi ** P -> + m |= range' f b lo mid ** range' f b (align mid al) hi ** P. Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. assert (mid <= align mid al) by (apply align_le; auto). @@ -477,20 +493,22 @@ Proof. Qed. Lemma range_preserved: - forall m m' b lo hi, - m |= range b lo hi -> + forall {f} m m' b lo hi, + m |= range' f b lo hi -> (forall i k p, lo <= i < hi -> Mem.perm m b i k p -> Mem.perm m' b i k p) -> - m' |= range b lo hi. + m' |= range' f b lo hi. Proof. intros. destruct H as (A & B & C). simpl; intuition auto. Qed. -(** A memory area that contains a value sastifying a given predicate *) +(** A memory area that contains a value satisfying a given predicate. + The permissions on the memory are either full (f = true) or only + writable (f = false). *) -Program Definition contains (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| +Program Definition contains' (f: bool) (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| m_pred := fun m => 0 <= ofs /\ ofs + size_chunk chunk <= Ptrofs.modulus - /\ Mem.valid_access m chunk b ofs Freeable + /\ Mem.valid_access m chunk b ofs (if f then Freeable else Writable) /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v; m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk |}. @@ -505,9 +523,23 @@ Next Obligation. eauto with mem. Qed. +Notation contains := (contains' true). +Notation contains_w := (contains' false). + +Lemma contains_contains_w: + forall chunk b ofs spec, + massert_imp (contains chunk b ofs spec) (contains_w chunk b ofs spec). +Proof. + constructor; auto. + inversion 1 as (Hlo & Hhi & Hac & v & Hload & Hspec). + eapply Mem.valid_access_implies with (p2:=Writable) in Hac; + auto using perm_F_any. + repeat (split; eauto). +Qed. + Lemma contains_no_overflow: - forall spec m chunk b ofs, - m |= contains chunk b ofs spec -> + forall {f} spec m chunk b ofs, + m |= contains' f chunk b ofs spec -> 0 <= ofs <= Ptrofs.max_unsigned. Proof. intros. simpl in H. @@ -518,8 +550,8 @@ Proof. Qed. Lemma load_rule: - forall spec m chunk b ofs, - m |= contains chunk b ofs spec -> + forall {f} spec m chunk b ofs, + m |= contains' f chunk b ofs spec -> exists v, Mem.load chunk m b ofs = Some v /\ spec v. Proof. intros. destruct H as (D & E & F & v & G & H). @@ -527,23 +559,23 @@ Proof. Qed. Lemma loadv_rule: - forall spec m chunk b ofs, - m |= contains chunk b ofs spec -> + forall {f} spec m chunk b ofs, + m |= contains' f chunk b ofs spec -> exists v, Mem.loadv chunk m (Vptr b (Ptrofs.repr ofs)) = Some v /\ spec v. Proof. - intros. exploit load_rule; eauto. intros (v & A & B). exists v; split; auto. + intros. exploit (@load_rule f); eauto. intros (v & A & B). exists v; split; auto. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow; eauto. Qed. Lemma store_rule: - forall chunk m b ofs v (spec1 spec: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1 spec: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.store chunk m b ofs v = Some m' /\ m' |= contains chunk b ofs spec ** P. + Mem.store chunk m b ofs v = Some m' /\ m' |= contains' f chunk b ofs spec ** P. Proof. intros. destruct H as (A & B & C). destruct A as (D & E & v0 & F & G). - assert (H: Mem.valid_access m chunk b ofs Writable) by eauto with mem. + assert (H: Mem.valid_access m chunk b ofs Writable) by (destruct f; eauto with mem). destruct (Mem.valid_access_store _ _ _ _ v H) as [m' STORE]. exists m'; split; auto. simpl. intuition auto. - eapply Mem.store_valid_access_1; eauto. @@ -554,22 +586,22 @@ Proof. Qed. Lemma storev_rule: - forall chunk m b ofs v (spec1 spec: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1 spec: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains' f chunk b ofs spec ** P. Proof. - intros. exploit store_rule; eauto. intros (m' & A & B). exists m'; split; auto. + intros. exploit (@store_rule f); eauto. intros (m' & A & B). exists m'; split; auto. simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. Qed. Lemma storev_rule2: - forall chunk m m' b ofs v (spec1 spec: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m m' b ofs v (spec1 spec: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> Memory.Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' -> - m' |= contains chunk b ofs spec ** P. + m' |= contains' f chunk b ofs spec ** P. Proof. intros * Hm Hspec Hstore. apply storev_rule with (1:=Hm) in Hspec. @@ -579,91 +611,104 @@ Proof. Qed. Lemma range_contains': - forall chunk b ofs, + forall {f} chunk b ofs, (align_chunk chunk | ofs) -> - massert_imp (range b ofs (ofs + size_chunk chunk)) - (contains chunk b ofs (fun v => True)). + massert_imp (range' f b ofs (ofs + size_chunk chunk)) + (contains' f chunk b ofs (fun v => True)). Proof. intros. constructor. intros. destruct H0 as (D & E & F). - assert (Mem.valid_access m chunk b ofs Freeable). + assert (Mem.valid_access m chunk b ofs (if f then Freeable else Writable)). { split; auto. red; auto. } split; [|split]. - generalize (size_chunk_pos chunk). omega. - assumption. - split; [assumption|]. destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. - eauto with mem. + destruct f; eauto with mem. exists v; auto. - auto. Qed. Lemma range_contains: - forall chunk b ofs P m, - m |= range b ofs (ofs + size_chunk chunk) ** P -> + forall {f} chunk b ofs P m, + m |= range' f b ofs (ofs + size_chunk chunk) ** P -> (align_chunk chunk | ofs) -> - m |= contains chunk b ofs (fun v => True) ** P. + m |= contains' f chunk b ofs (fun v => True) ** P. Proof. intros. rewrite range_contains' in H; assumption. Qed. Lemma contains_range': - forall chunk b ofs spec, - massert_imp (contains chunk b ofs spec) - (range b ofs (ofs + size_chunk chunk)). + forall {f} chunk b ofs spec, + massert_imp (contains' f chunk b ofs spec) + (range' f b ofs (ofs + size_chunk chunk)). Proof. intros. split. - intros. destruct H as (A & B & C & D). split; [|split]; try assumption. destruct C as (C1 & C2). - intros i k p Hr. + intros i k Hr. specialize (C1 _ Hr). eapply Mem.perm_cur in C1. apply Mem.perm_implies with (1:=C1). - apply perm_F_any. + destruct f; apply perm_refl. - trivial. Qed. Lemma contains_range: - forall chunk b ofs spec P m, - m |= contains chunk b ofs spec ** P -> - m |= range b ofs (ofs + size_chunk chunk) ** P. + forall {f} chunk b ofs spec P m, + m |= contains' f chunk b ofs spec ** P -> + m |= range' f b ofs (ofs + size_chunk chunk) ** P. Proof. intros. rewrite contains_range' in H; assumption. Qed. Lemma contains_imp: - forall (spec1 spec2: val -> Prop) chunk b ofs, + forall {f} (spec1 spec2: val -> Prop) chunk b ofs, (forall v, spec1 v -> spec2 v) -> - massert_imp (contains chunk b ofs spec1) (contains chunk b ofs spec2). + massert_imp (contains' f chunk b ofs spec1) (contains' f chunk b ofs spec2). Proof. intros; split; simpl; intros. - intuition auto. destruct H4 as (v & A & B). exists v; auto. - auto. Qed. -(** A memory area that contains a given value *) +(** A memory area that contains a given value. + The permissions on the underlying memory are either full (f = true) + or only writable (f = false). *) -Definition hasvalue (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert := - contains chunk b ofs (fun v' => v' = v). +Definition hasvalue' (f: bool) (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert := + contains' f chunk b ofs (fun v' => v' = v). + +Notation hasvalue := (hasvalue' true). +Notation hasvalue_w := (hasvalue' false). + +Lemma hasvalue_hasvalue_w: + forall chunk b ofs v, + massert_imp (hasvalue chunk b ofs v) (hasvalue_w chunk b ofs v). +Proof. + constructor; auto. + apply contains_contains_w. +Qed. Lemma store_rule': - forall chunk m b ofs v (spec1: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> exists m', - Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. + Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue' f chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply store_rule; eauto. Qed. Lemma storev_rule': - forall chunk m b ofs v (spec1: val -> Prop) P, - m |= contains chunk b ofs spec1 ** P -> + forall {f} chunk m b ofs v (spec1: val -> Prop) P, + m |= contains' f chunk b ofs spec1 ** P -> exists m', - Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue' f chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply storev_rule; eauto. Qed. diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index d375febf..96b0c8ef 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -58,7 +58,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). -- cgit