From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 84 ++++++++++++----------------------- common/Memory.v | 135 ++++++++++++++++++++++++++++++++++++++++++++++++++------ common/Values.v | 6 +++ 3 files changed, 157 insertions(+), 68 deletions(-) (limited to 'common') diff --git a/common/Events.v b/common/Events.v index 74c672e..24c03dc 100644 --- a/common/Events.v +++ b/common/Events.v @@ -557,7 +557,7 @@ Inductive volatile_store (F V: Type) (ge: Genv.t F V): | volatile_store_vol: forall chunk m b ofs id ev v, block_is_volatile ge b = true -> Genv.find_symbol ge id = Some b -> - eventval_match ge ev (type_of_chunk chunk) v -> + eventval_match ge ev (type_of_chunk chunk) (Val.load_result chunk v) -> volatile_store ge chunk m b ofs v (Event_vstore chunk id ofs ev :: nil) m @@ -585,6 +585,9 @@ Definition extcall_sem : Type := Definition loc_out_of_bounds (m: mem) (b: block) (ofs: Z) : Prop := ~Mem.perm m b ofs Max Nonempty. +Definition loc_not_writable (m: mem) (b: block) (ofs: Z) : Prop := + ~Mem.perm m b ofs Max Writable. + Definition loc_unmapped (f: meminj) (b: block) (ofs: Z): Prop := f b = None. @@ -631,12 +634,9 @@ Record extcall_properties (sem: extcall_sem) (** 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, + forall F V (ge: Genv.t F V) vargs m1 t vres m2, sem F V ge vargs m1 t vres 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; + Mem.unchanged_on (loc_not_writable m1) m1 m2; (** External calls must commute with memory extensions, in the following sense. *) @@ -777,7 +777,7 @@ Proof. (* max perms *) inv H; auto. (* readonly *) - inv H; auto. + inv H. apply Mem.unchanged_on_refl. (* mem extends *) inv H. inv H1. inv H6. inv H4. exploit volatile_load_extends; eauto. intros [v' [A B]]. @@ -839,7 +839,7 @@ Proof. (* max perm *) inv H; auto. (* readonly *) - inv H; auto. + inv H. apply Mem.unchanged_on_refl. (* extends *) inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. econstructor; eauto. @@ -885,25 +885,16 @@ Proof. Qed. Lemma volatile_store_readonly: - forall F V (ge: Genv.t F V) chunk1 m1 b1 ofs1 v t m2 chunk ofs b, + forall F V (ge: Genv.t F V) chunk1 m1 b1 ofs1 v t m2, 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. + Mem.unchanged_on (loc_not_writable m1) m1 m2. 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. + apply Mem.unchanged_on_refl. + eapply Mem.store_unchanged_on; eauto. + exploit Mem.store_valid_access_3; eauto. intros [P Q]. + intros. unfold loc_not_writable. red; intros. elim H2. + apply Mem.perm_cur_max. apply P. auto. Qed. Lemma volatile_store_extends: @@ -917,7 +908,8 @@ Lemma volatile_store_extends: /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'. Proof. intros. inv H. -- econstructor; split. econstructor; eauto. eapply eventval_match_lessdef; eauto. +- econstructor; split. econstructor; eauto. + eapply eventval_match_lessdef; eauto. apply Val.load_result_lessdef; auto. auto with mem. - exploit Mem.store_within_extends; eauto. intros [m2' [A B]]. exists m2'; intuition. @@ -946,7 +938,8 @@ Proof. intros. inv H0. - inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ. rewrite Int.add_zero. exists m1'. intuition. - constructor; auto. eapply eventval_match_inject; eauto. + constructor; auto. + eapply eventval_match_inject; eauto. apply val_load_result_inject; auto. - assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. inv H1. exists m2'; intuition. @@ -1105,10 +1098,7 @@ Proof. rewrite dec_eq_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. + inv H. eapply UNCHANGED; eauto. (* mem extends *) inv H. inv H1. inv H5. inv H7. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. @@ -1167,18 +1157,10 @@ Proof. (* 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. + inv H. eapply Mem.free_unchanged_on; eauto. + intros. red; intros. elim H3. + apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.free_range_perm; eauto. (* mem extends *) inv H. inv H1. inv H8. inv H6. exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. @@ -1271,17 +1253,9 @@ Proof. (* 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. + intros. inv H. eapply Mem.storebytes_unchanged_on; eauto. + intros; red; intros. elim H8. + apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto. (* extensions *) intros. inv H. inv H1. inv H13. inv H14. inv H10. inv H11. @@ -1376,7 +1350,7 @@ Proof. (* perms *) inv H; auto. (* readonly *) - inv H; auto. + inv H. apply Mem.unchanged_on_refl. (* mem extends *) inv H. exists Vundef; exists m1'; intuition. @@ -1420,7 +1394,7 @@ Proof. (* perms *) inv H; auto. (* readonly *) - inv H; auto. + inv H. apply Mem.unchanged_on_refl. (* mem extends *) inv H. inv H1. inv H6. exists v2; exists m1'; intuition. diff --git a/common/Memory.v b/common/Memory.v index af06f6f..1115ed7 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1866,6 +1866,34 @@ Proof. eapply load_alloc_same; eauto. Qed. +Theorem loadbytes_alloc_unchanged: + forall b' ofs n, + valid_block m1 b' -> + loadbytes m2 b' ofs n = loadbytes m1 b' ofs n. +Proof. + intros. unfold loadbytes. + destruct (range_perm_dec m1 b' ofs (ofs + n) Cur Readable). + rewrite pred_dec_true. + injection ALLOC; intros A B. rewrite <- B; simpl. + rewrite PMap.gso. auto. rewrite A. eauto with mem. + red; intros. eapply perm_alloc_1; eauto. + rewrite pred_dec_false; auto. + red; intros; elim n0. red; intros. eapply perm_alloc_4; eauto. eauto with mem. +Qed. + +Theorem loadbytes_alloc_same: + forall n ofs bytes byte, + loadbytes m2 b ofs n = Some bytes -> + In byte bytes -> byte = Undef. +Proof. + unfold loadbytes; intros. destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable); inv H. + revert H0. + injection ALLOC; intros A B. rewrite <- A; rewrite <- B; simpl. rewrite PMap.gss. + generalize (nat_of_Z n) ofs. induction n0; simpl; intros. + contradiction. + rewrite ZMap.gi in H0. destruct H0; eauto. +Qed. + End ALLOC. Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. @@ -2033,6 +2061,40 @@ Proof. red; intro; elim n. eapply valid_access_free_1; eauto. Qed. +Theorem load_free_2: + forall chunk b ofs v, + load chunk m2 b ofs = Some v -> load chunk m1 b ofs = Some v. +Proof. + intros. unfold load. rewrite pred_dec_true. + rewrite (load_result _ _ _ _ _ H). rewrite free_result; auto. + apply valid_access_free_inv_1. eauto with mem. +Qed. + +Theorem loadbytes_free: + forall b ofs n, + b <> bf \/ lo >= hi \/ ofs + n <= lo \/ hi <= ofs -> + loadbytes m2 b ofs n = loadbytes m1 b ofs n. +Proof. + intros. unfold loadbytes. + destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable). + rewrite pred_dec_true. + rewrite free_result; auto. + red; intros. eapply perm_free_3; eauto. + rewrite pred_dec_false; auto. + red; intros. elim n0; red; intros. + eapply perm_free_1; eauto. destruct H; auto. right; omega. +Qed. + +Theorem loadbytes_free_2: + forall b ofs n bytes, + loadbytes m2 b ofs n = Some bytes -> loadbytes m1 b ofs n = Some bytes. +Proof. + intros. unfold loadbytes in *. + destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable); inv H. + rewrite pred_dec_true. rewrite free_result; auto. + red; intros. apply perm_free_3; auto. +Qed. + End FREE. Local Hint Resolve valid_block_free_1 valid_block_free_2 @@ -2164,6 +2226,27 @@ Proof. red; intros; elim n. eapply valid_access_drop_2; eauto. Qed. +Theorem loadbytes_drop: + forall b' ofs n, + b' <> b \/ ofs + n <= lo \/ hi <= ofs \/ perm_order p Readable -> + loadbytes m' b' ofs n = loadbytes m b' ofs n. +Proof. + intros. + unfold loadbytes. + destruct (range_perm_dec m b' ofs (ofs + n) Cur Readable). + rewrite pred_dec_true. + unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. simpl. auto. + red; intros. + destruct (eq_block 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. intuition. + eapply perm_drop_3; eauto. + rewrite pred_dec_false; eauto. + red; intros; elim n0; red; intros. + eapply perm_drop_4; eauto. +Qed. + End DROP. (** * Generic injections *) @@ -4061,6 +4144,26 @@ Proof. intros. destruct H. apply unchanged_on_perm0; auto. Qed. +Lemma loadbytes_unchanged_on_1: + forall m m' b ofs n, + unchanged_on m m' -> + valid_block m b -> + (forall i, ofs <= i < ofs + n -> P b i) -> + loadbytes m' b ofs n = loadbytes m b ofs n. +Proof. + intros. + destruct (zle n 0). ++ erewrite ! loadbytes_empty by assumption. auto. ++ unfold loadbytes. destruct H. + destruct (range_perm_dec m b ofs (ofs + n) Cur Readable). + rewrite pred_dec_true. f_equal. + apply getN_exten. intros. rewrite nat_of_Z_eq in H by omega. + apply unchanged_on_contents0; auto. + red; intros. apply unchanged_on_perm0; auto. + rewrite pred_dec_false. auto. + red; intros; elim n0; red; intros. apply <- unchanged_on_perm0; auto. +Qed. + Lemma loadbytes_unchanged_on: forall m m' b ofs n bytes, unchanged_on m m' -> @@ -4071,15 +4174,24 @@ Proof. intros. destruct (zle n 0). + erewrite loadbytes_empty in * by assumption. auto. -+ unfold loadbytes in *. destruct H. - destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); inv H1. - assert (valid_block m b). - { eapply perm_valid_block. apply (r ofs). omega. } - assert (range_perm m' b ofs (ofs + n) Cur Readable). - { red; intros. apply unchanged_on_perm0; auto. } - rewrite pred_dec_true by assumption. f_equal. - apply getN_exten. intros. rewrite nat_of_Z_eq in H2 by omega. - apply unchanged_on_contents0; auto. ++ rewrite <- H1. apply loadbytes_unchanged_on_1; auto. + exploit loadbytes_range_perm; eauto. instantiate (1 := ofs). omega. + intros. eauto with mem. +Qed. + +Lemma load_unchanged_on_1: + forall m m' chunk b ofs, + unchanged_on m m' -> + valid_block m b -> + (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) -> + load chunk m' b ofs = load chunk m b ofs. +Proof. + intros. unfold load. destruct (valid_access_dec m chunk b ofs Readable). + destruct v. rewrite pred_dec_true. f_equal. f_equal. apply getN_exten. intros. + rewrite <- size_chunk_conv in H4. eapply unchanged_on_contents; eauto. + split; auto. red; intros. eapply perm_unchanged_on; eauto. + rewrite pred_dec_false. auto. + red; intros [A B]; elim n; split; auto. red; intros; eapply perm_unchanged_on_2; eauto. Qed. Lemma load_unchanged_on: @@ -4089,10 +4201,7 @@ Lemma load_unchanged_on: load chunk m b ofs = Some v -> load chunk m' b ofs = Some v. Proof. - intros. - exploit load_valid_access; eauto. intros [A B]. - exploit load_loadbytes; eauto. intros [bytes [C D]]. - subst v. apply loadbytes_load; auto. eapply loadbytes_unchanged_on; eauto. + intros. rewrite <- H1. eapply load_unchanged_on_1; eauto with mem. Qed. Lemma store_unchanged_on: diff --git a/common/Values.v b/common/Values.v index b9594fc..99a994b 100644 --- a/common/Values.v +++ b/common/Values.v @@ -655,6 +655,12 @@ Definition cmpl (c: comparison) (v1 v2: val): option val := Definition cmplu (c: comparison) (v1 v2: val): option val := option_map of_bool (cmplu_bool c v1 v2). +Definition maskzero_bool (v: val) (mask: int): option bool := + match v with + | Vint n => Some (Int.eq (Int.and n mask) Int.zero) + | _ => None + end. + End COMPARISONS. (** [load_result] reflects the effect of storing a value with a given -- cgit v1.2.3