Merge of branch value-analysis.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 157 insertions, 68 deletions

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