fixed CSE2 for mppa_k1c

Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2

3 files changed, 85 insertions, 27 deletions

diff --git a/common/Events.v b/common/Events.v
index 10e0c232..28bb992a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -649,9 +649,12 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
 (** External call cannot modify memory unless they have [Max, Writable]
    permissions. *)
   ec_readonly:
-    forall ge vargs m1 t vres m2,
+    forall ge vargs m1 t vres m2 b ofs n bytes,
     sem ge vargs m1 t vres m2 ->
-    Mem.unchanged_on (loc_not_writable m1) m1 m2;
+    Mem.valid_block m1 b ->
+    Mem.loadbytes m2 b ofs n = Some bytes ->
+    (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) ->
+    Mem.loadbytes m1 b ofs n = Some bytes;
 
 (** External calls must commute with memory extensions, in the
   following sense. *)
@@ -784,7 +787,7 @@ Proof.
 (* max perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H. inv H1. inv H6. inv H4.
   exploit volatile_load_extends; eauto. intros [v' [A B]].
@@ -833,14 +836,27 @@ Proof.
   rewrite C; auto.
 Qed.
 
+Lemma unchanged_on_readonly:
+  forall m1 m2 b ofs n bytes,
+  Mem.unchanged_on (loc_not_writable m1) m1 m2 ->
+  Mem.valid_block m1 b ->
+  Mem.loadbytes m2 b ofs n = Some bytes ->
+  (forall i, ofs <= i < ofs + n -> ~Mem.perm m1 b i Max Writable) ->
+  Mem.loadbytes m1 b ofs n = Some bytes.
+Proof.
+  intros.
+  rewrite <- H1. symmetry.
+  apply Mem.loadbytes_unchanged_on_1 with (P := loc_not_writable m1); auto.
+Qed.
+
 Lemma volatile_store_readonly:
   forall ge chunk1 m1 b1 ofs1 v t m2,
   volatile_store ge chunk1 m1 b1 ofs1 v t m2 ->
   Mem.unchanged_on (loc_not_writable m1) m1 m2.
 Proof.
   intros. inv H.
-  apply Mem.unchanged_on_refl.
-  eapply Mem.store_unchanged_on; eauto.
+- 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.
@@ -934,7 +950,7 @@ Proof.
 (* perms *)
 - inv H. inv H2. auto. eauto with mem.
 (* readonly *)
-- inv H. eapply volatile_store_readonly; eauto.
+- inv H. eapply unchanged_on_readonly; eauto. 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]]].
@@ -994,7 +1010,7 @@ Proof.
   rewrite dec_eq_false. auto.
   apply Mem.valid_not_valid_diff with m1; eauto with mem.
 (* readonly *)
-- inv H. eapply UNCHANGED; eauto.
+- inv H. eapply unchanged_on_readonly; eauto. 
 (* mem extends *)
 - inv H. inv H1. inv H7.
   assert (SZ: v2 = Vptrofs sz).
@@ -1045,11 +1061,13 @@ Qed.
 
 Inductive extcall_free_sem (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
-  | extcall_free_sem_intro: forall b lo sz m m',
+  | extcall_free_sem_ptr: forall b lo sz m m',
       Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) ->
       Ptrofs.unsigned sz > 0 ->
       Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' ->
-      extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'.
+      extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'
+  | extcall_free_sem_null: forall m,
+      extcall_free_sem ge (Vnullptr :: nil) m E0 Vundef m.
 
 Lemma extcall_free_ok:
   extcall_properties extcall_free_sem
@@ -1057,26 +1075,29 @@ Lemma extcall_free_ok:
 Proof.
   constructor; intros.
 (* well typed *)
-- inv H. simpl. auto.
+- inv H; simpl; auto.
 (* symbols preserved *)
 - inv H0; econstructor; eauto.
 (* valid block *)
-- inv H. eauto with mem.
+- inv H; eauto with mem.
 (* perms *)
-- inv H. eapply Mem.perm_free_3; eauto.
+- inv H; eauto using Mem.perm_free_3.
 (* readonly *)
-- inv H. eapply Mem.free_unchanged_on; eauto.
-  intros. red; intros. elim H3.
+- eapply unchanged_on_readonly; eauto. inv H.
++ eapply Mem.free_unchanged_on; eauto.
+  intros. red; intros. elim H6.
   apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.free_range_perm; eauto.
++ apply Mem.unchanged_on_refl.
 (* mem extends *)
-- inv H. inv H1. inv H8. inv H6.
+- inv H.
++ inv H1. inv H8. inv H6.
   exploit Mem.load_extends; eauto. intros [v' [A B]].
   assert (v' = Vptrofs sz).
   { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
   subst v'.
   exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]].
-  exists Vundef; exists m2'; intuition.
+  exists Vundef; exists m2'; intuition auto.
   econstructor; eauto.
   eapply Mem.free_unchanged_on; eauto.
   unfold loc_out_of_bounds; intros.
@@ -1084,8 +1105,14 @@ Proof.
   { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
     eapply Mem.free_range_perm. eexact H4. eauto. }
   tauto.
++ inv H1. inv H5. replace v2 with Vnullptr.
+  exists Vundef; exists m1'; intuition auto.
+  constructor.
+  apply Mem.unchanged_on_refl.
+  unfold Vnullptr in *; destruct Archi.ptr64; inv H3; auto.
 (* mem inject *)
-- inv H0. inv H2. inv H7. inv H9.
+- inv H0.
++ inv H2. inv H7. inv H9.
   exploit Mem.load_inject; eauto. intros [v' [A B]].
   assert (v' = Vptrofs sz).
   { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
@@ -1099,7 +1126,7 @@ Proof.
   intro EQ.
   exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
   exists f, Vundef, m2'; split.
-  apply extcall_free_sem_intro with (sz := sz) (m' := m2').
+  apply extcall_free_sem_ptr with (sz := sz) (m' := m2').
     rewrite EQ. rewrite <- A. f_equal. omega.
     auto. auto.
     rewrite ! EQ. rewrite <- C. f_equal; omega.
@@ -1112,14 +1139,19 @@ Proof.
     apply P. omega.
   split. auto.
   red; intros. congruence.
++ inv H2. inv H6. replace v' with Vnullptr.
+  exists f, Vundef, m1'; intuition auto using Mem.unchanged_on_refl.
+  constructor.
+  red; intros; congruence.
+  unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto.
 (* trace length *)
 - inv H; simpl; omega.
 (* receptive *)
-- assert (t1 = t2). inv H; inv H0; auto. subst t2.
+- assert (t1 = t2) by (inv H; inv H0; auto). subst t2.
   exists vres1; exists m1; auto.
 (* determ *)
-- inv H; inv H0.
-  assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
+- inv H; inv H0; try (unfold Vnullptr in *; destruct Archi.ptr64; discriminate).
++ assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
   assert (EQ2: sz0 = sz).
   { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF.
     rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
@@ -1127,6 +1159,7 @@ Proof.
   }
   subst sz0.
   split. constructor. intuition congruence.
++ split. constructor. intuition auto.
 Qed.
 
 (** ** Semantics of [memcpy] operations. *)
@@ -1159,8 +1192,9 @@ Proof.
 - (* perms *)
   intros. inv H. eapply Mem.perm_storebytes_2; eauto.
 - (* readonly *)
-  intros. inv H. eapply Mem.storebytes_unchanged_on; eauto.
-  intros; red; intros. elim H8.
+  intros. inv H. eapply unchanged_on_readonly; eauto. 
+  eapply Mem.storebytes_unchanged_on; eauto.
+  intros; red; intros. elim H11.
   apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto.
 - (* extensions *)
   intros. inv H.
@@ -1271,7 +1305,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H.
   exists Vundef; exists m1'; intuition.
@@ -1316,7 +1350,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H. inv H1. inv H6.
   exists v2; exists m1'; intuition.
@@ -1359,7 +1393,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H.
   exists Vundef; exists m1'; intuition.
@@ -1406,7 +1440,7 @@ Proof.
 (* perms *)
 - inv H; auto.
 (* readonly *)
-- inv H. apply Mem.unchanged_on_refl.
+- inv H; auto.
 (* mem extends *)
 - inv H. fold bsem in H2. apply val_inject_list_lessdef in H1.
   specialize (bs_inject _ bsem _ _ _ H1).
diff --git a/common/Memdata.v b/common/Memdata.v
index f3016efe..a09b90f5 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -44,6 +44,13 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
   | Many64 => 8
   end.
 
+Definition largest_size_chunk := 8.
+
+Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
+Proof.
+  destruct chunk; simpl; omega.
+Qed.
+
 Lemma size_chunk_pos:
   forall chunk, size_chunk chunk > 0.
 Proof.
diff --git a/common/Memory.v b/common/Memory.v
index f21d99af..cd8a2001 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1307,6 +1307,23 @@ Proof.
   }
 Qed.
     
+Section STOREV.
+Variable chunk: memory_chunk.
+Variable m1: mem.
+Variables addr v: val.
+Variable m2: mem.
+Hypothesis STORE: storev chunk m1 addr v = Some m2.
+
+
+Theorem loadv_storev_same:
+  loadv chunk m2 addr = Some (Val.load_result chunk v).
+Proof.
+  destruct addr; simpl in *; try discriminate.
+  eapply load_store_same.
+  eassumption.
+Qed.
+End STOREV.
+
 Lemma load_store_overlap:
   forall chunk m1 b ofs v m2 chunk' ofs' v',
   store chunk m1 b ofs v = Some m2 ->