From f2d0caa5f7594cf936713f3bd6cdc3ab5a6f9626 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 31 Jul 2014 07:33:53 +0000 Subject: 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 --- common/Memory.v | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) (limited to 'common/Memory.v') diff --git a/common/Memory.v b/common/Memory.v index e45df664..45c2497b 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' -> -- cgit