Add Mem.free_parallel_inject and use it to simplify Events a bit.

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

3 files changed, 50 insertions, 35 deletions

diff --git a/common/Events.v b/common/Events.v
index 5eee93a..8787a14 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1174,47 +1174,27 @@ Proof.
   tauto.
 (* mem inject *)
   inv H0. inv H2. inv H7. inv H9.
-  exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. 
+  exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B.
   assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable).
     eapply Mem.free_range_perm; eauto.
   exploit Mem.address_inject; eauto. 
     apply Mem.perm_implies with Freeable; auto with mem.
     apply H0. instantiate (1 := lo). omega. 
   intro EQ.
-  assert (Mem.range_perm m1' b2 (Int.unsigned lo + delta - 4) (Int.unsigned lo + delta + Int.unsigned sz) Cur Freeable).
-    red; intros. 
-    replace ofs with ((ofs - delta) + delta) by omega.
-    eapply Mem.perm_inject; eauto. apply H0. omega. 
-  destruct (Mem.range_perm_free _ _ _ _ H2) as [m2' FREE].
-  exists f; exists Vundef; exists m2'; intuition.
-
-  econstructor.
-  rewrite EQ. replace (Int.unsigned lo + delta - 4) with (Int.unsigned lo - 4 + delta) by omega.
-  eauto. auto. 
-  rewrite EQ. auto.
-  
-  assert (Mem.free_list m1 ((b, Int.unsigned lo - 4, Int.unsigned lo + Int.unsigned sz) :: nil) = Some m2).
-    simpl. rewrite H5. auto.
-  eapply Mem.free_inject; eauto. 
-  intros. destruct (eq_block b b1).
-  subst b. assert (delta0 = delta) by congruence. subst delta0. 
-  exists (Int.unsigned lo - 4); exists (Int.unsigned lo + Int.unsigned sz); split.
-  simpl; auto. omega.
-  elimtype False. exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. 
-  instantiate (1 := ofs + delta0 - delta).
-  apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-  apply H0. omega.
-  eapply Mem.perm_max. eauto with mem.
-  intuition. 
-
-  eapply Mem.free_unchanged_on; eauto. 
-  unfold loc_unmapped; intros. congruence.
-
-  eapply Mem.free_unchanged_on; eauto. 
-  unfold loc_out_of_reach; intros. red; intros. eelim H8; eauto. 
-  apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
-  apply H0. omega.
-
+  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'). 
+    rewrite EQ. rewrite <- A. f_equal. omega. 
+    auto.
+    rewrite ! EQ. rewrite <- C. f_equal; omega.
+  split. auto. 
+  split. auto.
+  split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence.
+  split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. 
+    intros. red; intros. eelim H7; eauto.
+    apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. 
+    apply H0. omega.
+  split. auto. 
   red; intros. congruence.
 (* trace length *)
   inv H; simpl; omega.
diff --git a/common/Memory.v b/common/Memory.v
index e45df66..45c2497 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -3863,6 +3863,32 @@ Proof.
   exploit H2; eauto. intros [lo1 [hi1 [C D]]]. eauto.
 Qed.
 
+Theorem free_parallel_inject:
+  forall f m1 m2 b lo hi m1' b' delta,
+  inject f m1 m2 ->
+  free m1 b lo hi = Some m1' ->
+  f b = Some(b', delta) ->
+  exists m2',
+     free m2 b' (lo + delta) (hi + delta) = Some m2'
+  /\ inject f m1' m2'.
+Proof.
+  intros. 
+  destruct (range_perm_free m2 b' (lo + delta) (hi + delta)) as [m2' FREE].
+  eapply range_perm_inject; eauto. eapply free_range_perm; eauto.
+  exists m2'; split; auto.
+  eapply free_inject with (m1 := m1) (l := (b,lo,hi)::nil); eauto. 
+  simpl; rewrite H0; auto.
+  intros. destruct (eq_block b1 b).
+  subst b1. rewrite H1 in H2; inv H2. 
+  exists lo, hi; split; auto with coqlib. omega.
+  exploit mi_no_overlap. eexact H. eexact n. eauto. eauto.
+  eapply perm_max. eapply perm_implies. eauto. auto with mem. 
+  instantiate (1 := ofs + delta0 - delta). 
+  apply perm_cur_max. apply perm_implies with Freeable; auto with mem. 
+  eapply free_range_perm; eauto. omega.
+  intros [A|A]. congruence. omega.
+Qed.
+
 Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2',
   inject f m1 m2 -> 
   drop_perm m2 b lo hi p = Some m2' -> 
diff --git a/common/Memtype.v b/common/Memtype.v
index 1ab1cb7..d94c895 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -1177,6 +1177,15 @@ Axiom free_inject:
     exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) ->
   inject f m1' m2'.
 
+Axiom free_parallel_inject:
+  forall f m1 m2 b lo hi m1' b' delta,
+  inject f m1 m2 ->
+  free m1 b lo hi = Some m1' ->
+  f b = Some(b', delta) ->
+  exists m2',
+     free m2 b' (lo + delta) (hi + delta) = Some m2'
+  /\ inject f m1' m2'.
+
 Axiom drop_outside_inject:
   forall f m1 m2 b lo hi p m2',
   inject f m1 m2 ->