diff options
Diffstat (limited to 'common/Memory.v')
-rw-r--r-- | common/Memory.v | 129 |
1 files changed, 122 insertions, 7 deletions
diff --git a/common/Memory.v b/common/Memory.v index 0ea9e3b0..f32d21c7 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -2823,7 +2823,10 @@ Qed. Record extends' (m1 m2: mem) : Prop := mk_extends { mext_next: nextblock m1 = nextblock m2; - mext_inj: mem_inj inject_id m1 m2 + mext_inj: mem_inj inject_id m1 m2; + mext_perm_inv: forall b ofs k p, + perm m2 b ofs k p -> + perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty }. Definition extends := extends'. @@ -2836,6 +2839,7 @@ Proof. intros. unfold inject_id in H; inv H. apply Z.divide_0_r. intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. apply memval_lessdef_refl. + tauto. Qed. Theorem load_extends: @@ -2890,10 +2894,11 @@ Proof. intros [m2' [A B]]. exists m2'; split. replace (ofs + 0) with ofs in A by omega. auto. - split; auto. + constructor; auto. rewrite (nextblock_store _ _ _ _ _ _ H0). rewrite (nextblock_store _ _ _ _ _ _ A). auto. + intros. exploit mext_perm_inv0; intuition eauto using perm_store_1, perm_store_2. Qed. Theorem store_outside_extends: @@ -2907,6 +2912,7 @@ Proof. rewrite (nextblock_store _ _ _ _ _ _ H0). auto. eapply store_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + intros. eauto using perm_store_2. Qed. Theorem storev_extends: @@ -2940,10 +2946,11 @@ Proof. intros [m2' [A B]]. exists m2'; split. replace (ofs + 0) with ofs in A by omega. auto. - split; auto. + constructor; auto. rewrite (nextblock_storebytes _ _ _ _ _ H0). rewrite (nextblock_storebytes _ _ _ _ _ A). auto. + intros. exploit mext_perm_inv0; intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. Theorem storebytes_outside_extends: @@ -2957,6 +2964,7 @@ Proof. rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. eapply storebytes_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + intros. eauto using perm_storebytes_2. Qed. Theorem alloc_extends: @@ -2988,6 +2996,15 @@ Proof. eapply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. + intros. eapply perm_alloc_inv in H; eauto. + generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM. + destruct (eq_block b0 b). + subst b0. + assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega. + destruct EITHER. + left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. + right; tauto. + exploit mext_perm_inv0; intuition eauto using perm_alloc_1, perm_alloc_4. Qed. Theorem free_left_extends: @@ -2999,6 +3016,10 @@ Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_left_inj; eauto. + intros. exploit mext_perm_inv0; eauto. intros [A|A]. + eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. + subst b0. right; eapply perm_free_2; eauto. + intuition eauto using perm_free_3. Qed. Theorem free_right_extends: @@ -3012,6 +3033,7 @@ Proof. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_right_inj; eauto. unfold inject_id; intros. inv H. eapply H1; eauto. omega. + intros. eauto using perm_free_3. Qed. Theorem free_parallel_extends: @@ -3029,13 +3051,17 @@ Proof. eapply perm_inj with (b1 := b); eauto. eapply free_range_perm; eauto. destruct X as [m2' FREE]. exists m2'; split; auto. - inv H. constructor. + constructor. rewrite (nextblock_free _ _ _ _ _ H0). rewrite (nextblock_free _ _ _ _ _ FREE). auto. eapply free_right_inj with (m1 := m1'); eauto. eapply free_left_inj; eauto. - unfold inject_id; intros. inv H. + unfold inject_id; intros. inv H1. eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. + intros. exploit mext_perm_inv0; eauto using perm_free_3. intros [A|A]. + eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. + subst b0. right; eapply perm_free_2; eauto. + right; intuition eauto using perm_free_3. Qed. Theorem valid_block_extends: @@ -3054,6 +3080,13 @@ Proof. eapply perm_inj; eauto. Qed. +Theorem perm_extends_inv: + forall m1 m2 b ofs k p, + extends m1 m2 -> perm m2 b ofs k p -> perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty. +Proof. + intros. inv H; eauto. +Qed. + Theorem valid_access_extends: forall m1 m2 chunk b ofs p, extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p. @@ -3110,7 +3143,12 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop := forall b b' delta ofs, f b = Some(b', delta) -> perm m1 b (Int.unsigned ofs) Max Nonempty \/ perm m1 b (Int.unsigned ofs - 1) Max Nonempty -> - delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned + delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned; + mi_perm_inv: + forall b1 ofs b2 delta k p, + f b1 = Some(b2, delta) -> + perm m2 b2 (ofs + delta) k p -> + perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty }. Definition inject := inject'. @@ -3148,6 +3186,16 @@ Proof. intros. inv H0. eapply perm_inj; eauto. Qed. +Theorem perm_inject_inv: + forall f m1 m2 b1 ofs b2 delta k p, + inject f m1 m2 -> + f b1 = Some(b2, delta) -> + perm m2 b2 (ofs + delta) k p -> + perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty. +Proof. + intros. eapply mi_perm_inv; eauto. +Qed. + Theorem range_perm_inject: forall f m1 m2 b1 b2 delta lo hi k p, f b1 = Some(b2, delta) -> @@ -3433,6 +3481,9 @@ Proof. (* representable *) intros. eapply mi_representable; try eassumption. destruct H4; eauto with mem. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_store_2. + intuition eauto using perm_store_1, perm_store_2. Qed. Theorem store_unmapped_inject: @@ -3455,6 +3506,9 @@ Proof. (* representable *) intros. eapply mi_representable; try eassumption. destruct H3; eauto with mem. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_store_2. + intuition eauto using perm_store_1, perm_store_2. Qed. Theorem store_outside_inject: @@ -3478,6 +3532,8 @@ Proof. auto. (* representable *) eauto with mem. +(* perm inv *) + intros. eauto using perm_store_2. Qed. Theorem storev_mapped_inject: @@ -3521,6 +3577,9 @@ Proof. (* representable *) intros. eapply mi_representable0; eauto. destruct H4; eauto using perm_storebytes_2. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. Theorem storebytes_unmapped_inject: @@ -3543,6 +3602,9 @@ Proof. (* representable *) intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto. + intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. Theorem storebytes_outside_inject: @@ -3566,6 +3628,8 @@ Proof. auto. (* representable *) auto. +(* perm inv *) + intros. eapply mi_perm_inv0; eauto using perm_storebytes_2. Qed. Theorem storebytes_empty_inject: @@ -3587,6 +3651,9 @@ Proof. (* representable *) intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. (* Preservation of allocations *) @@ -3609,6 +3676,10 @@ Proof. auto. (* representable *) auto. +(* perm inv *) + intros. eapply perm_alloc_inv in H2; eauto. destruct (eq_block b0 b2). + subst b0. eelim fresh_block_alloc; eauto. + eapply mi_perm_inv0; eauto. Qed. Theorem alloc_left_unmapped_inject: @@ -3652,6 +3723,10 @@ Proof. destruct (eq_block b b1); try discriminate. eapply mi_representable0; try eassumption. destruct H4; eauto using perm_alloc_4. +(* perm inv *) + intros. unfold f' in H3; destruct (eq_block b0 b1); try discriminate. + exploit mi_perm_inv0; eauto. + intuition eauto using perm_alloc_1, perm_alloc_4. (* incr *) split. auto. (* image *) @@ -3734,6 +3809,14 @@ Proof. generalize (Int.unsigned_range_2 ofs). omega. eapply mi_representable0; try eassumption. destruct H10; eauto using perm_alloc_4. +(* perm inv *) + intros. unfold f' in H9; destruct (eq_block b0 b1). + inversion H9; clear H9; subst b0 b3 delta0. + assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by omega. + destruct EITHER. + left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. + right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto. + exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4. (* incr *) split. auto. (* image of b1 *) @@ -3790,6 +3873,10 @@ Proof. (* representable *) intros. eapply mi_representable0; try eassumption. destruct H2; eauto with mem. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto. intuition eauto using perm_free_3. + eapply perm_free_inv in H4; eauto. destruct H4 as [[A B] | A]; auto. + subst b1. right; eapply perm_free_2; eauto. Qed. Lemma free_list_left_inject: @@ -3825,6 +3912,8 @@ Proof. auto. (* representable *) auto. +(* perm inv *) + intros. eauto using perm_free_3. Qed. Lemma perm_free_list: @@ -3900,6 +3989,7 @@ Proof. intros. destruct H. constructor; eauto. eapply drop_outside_inj; eauto. intros. unfold valid_block in *. erewrite nextblock_drop; eauto. + intros. eapply mi_perm_inv0; eauto using perm_drop_4. Qed. (** Composing two memory injections. *) @@ -3973,6 +4063,15 @@ Proof. ((Int.unsigned ofs - 1) + delta1) by omega. destruct H0; eauto using perm_inj. rewrite H. omega. +(* perm inv *) + intros. + destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. + destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate. + inversion H; clear H; subst b'' delta. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by omega. + exploit mi_perm_inv1; eauto. intros [A|A]. + eapply mi_perm_inv0; eauto. + right; red; intros. elim A. eapply perm_inj; eauto. Qed. Lemma val_lessdef_inject_compose: @@ -4007,6 +4106,10 @@ Proof. (* representable *) eapply mi_representable0; eauto. destruct H1; eauto using perm_extends. +(* perm inv *) + exploit mi_perm_inv0; eauto. intros [A|A]. + eapply mext_perm_inv0; eauto. + right; red; intros; elim A. eapply perm_extends; eauto. Qed. Lemma inject_extends_compose: @@ -4026,19 +4129,27 @@ Proof. red; intros. eapply mi_no_overlap0; eauto. (* representable *) eapply mi_representable0; eauto. +(* perm inv *) + exploit mext_perm_inv0; eauto. intros [A|A]. + eapply mi_perm_inv0; eauto. + right; red; intros; elim A. eapply perm_inj; eauto. Qed. Lemma extends_extends_compose: forall m1 m2 m3, extends m1 m2 -> extends m2 m3 -> extends m1 m3. Proof. - intros. inv H; inv H0; constructor; intros. + intros. inversion H; subst; inv H0; constructor; intros. (* nextblock *) congruence. (* meminj *) replace inject_id with (compose_meminj inject_id inject_id). eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. auto. + (* perm inv *) + exploit mext_perm_inv1; eauto. intros [A|A]. + eapply mext_perm_inv0; eauto. + right; red; intros; elim A. eapply perm_extends; eauto. Qed. (** Injecting a memory into itself. *) @@ -4075,6 +4186,10 @@ Proof. (* range *) unfold flat_inj; intros. destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega. +(* perm inv *) + unfold flat_inj; intros. + destruct (plt b1 (nextblock m)); inv H0. + rewrite Zplus_0_r in H1; auto. Qed. Theorem empty_inject_neutral: |