Library Memory
Coq development accompanying the paper
"Formal verification of a C-like memory model
and its uses for verifying program transformations"
by Xavier Leroy and Sandrine Blazy.
Require Import List.
Require Import ZArith.
Require Import Znumtheory.
Open Scope Z_scope.
Ltac inv H := inversion H; clear H; subst.
Definition zeq: forall (z1 z2: Z), {z1=z2} + {z1<>z2} := Z_eq_dec.
Definition zle: forall (z1 z2: Z), {z1<=z2} + {z1>z2} := Z_le_gt_dec.
Definition zlt: forall (z1 z2: Z), {z1<z2} + {z1>=z2} := Z_lt_ge_dec.
Parameter val: Set.
Parameter vundef : val.
Parameter memtype: Set.
Parameter compat: memtype -> memtype -> Prop.
Parameter sizeof: memtype -> Z.
Parameter alignof: memtype -> Z.
Parameter convert: memtype -> val -> val.
Axiom compat_dec: forall ty1 ty2, {compat ty1 ty2} + {~compat ty1 ty2}.
Axiom sizeof_pos: forall ty, sizeof ty > 0.
Axiom compat_sizeof:
forall ty ty', compat ty ty' -> sizeof ty' = sizeof ty.
Axiom alignof_pos: forall ty, alignof ty > 0.
Parameter max_alignment: Z.
Axiom alignof_div: forall ty, (alignof ty | max_alignment).
Axiom compat_alignof:
forall ty ty', compat ty ty' -> alignof ty' = alignof ty.
Module Type GEN_MEM.
Variable block: Set.
Hypothesis eq_block: forall (b1 b2: block), {b1=b2} + {b1<>b2}.
Variable mem: Set.
Variable empty: mem.
Variable alloc: mem -> Z -> Z -> option (block * mem).
Variable load: memtype -> mem -> block -> Z -> option val.
Variable store: memtype -> mem -> block -> Z -> val -> option mem.
Variable free: mem -> block -> option mem.
Hypothesis load_alloc_other:
forall m lo hi b m' ty b' ofs,
alloc m lo hi = Some (b, m') ->
b' <> b ->
load ty m' b' ofs = load ty m b' ofs.
Hypothesis load_store_same:
forall ty m b ofs v m' ty',
store ty m b ofs v = Some m' ->
compat ty ty' ->
load ty' m' b ofs = Some (convert ty' v).
Hypothesis load_store_disjoint:
forall ty m b ofs v m' ty' b' ofs',
store ty m b ofs v = Some m' ->
b' <> b \/ ofs' + sizeof ty' <= ofs \/ ofs + sizeof ty <= ofs' ->
load ty' m' b' ofs' = load ty' m b' ofs'.
Hypothesis load_free_other:
forall m b m' ty b' ofs,
free m b = Some m' ->
b' <> b ->
load ty m' b' ofs = load ty m b' ofs.
Variable valid_block: mem -> block -> Prop.
Hypothesis alloc_valid_block:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') ->
(valid_block m' b' <-> b' = b \/ valid_block m b').
Hypothesis alloc_not_valid_block:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> ~(valid_block m b).
Hypothesis load_valid_block:
forall ty m b ofs v,
load ty m b ofs = Some v -> valid_block m b.
Hypothesis store_valid_block:
forall ty m b ofs v m',
store ty m b ofs v = Some m' -> valid_block m b.
Hypothesis store_valid_block_inv:
forall ty m b ofs v m' b',
store ty m b ofs v = Some m' -> (valid_block m' b' <-> valid_block m b').
Hypothesis free_valid_block:
forall m b m' b',
free m b = Some m' -> b' <> b -> (valid_block m' b' <-> valid_block m b').
Hypothesis valid_block_free:
forall m b,
valid_block m b -> exists m', free m b = Some m'.
Variable bounds: mem -> block -> Z*Z.
Hypothesis alloc_result_bounds:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> bounds m' b = (lo, hi).
Hypothesis alloc_bounds_inv:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') -> b' <> b -> bounds m' b' = bounds m b'.
Hypothesis store_bounds_inv:
forall ty m b ofs v m' b',
store ty m b ofs v = Some m' -> bounds m' b' = bounds m b'.
Hypothesis free_bounds_inv:
forall m b m' b',
free m b = Some m' -> b' <> b -> bounds m' b' = bounds m b'.
Definition valid_pointer (ty: memtype) (m: mem) (b: block) (ofs: Z) : Prop :=
valid_block m b
/\ (alignof ty | ofs)
/\ fst (bounds m b) <= ofs
/\ ofs + sizeof ty <= snd (bounds m b).
Hypothesis valid_pointer_store:
forall ty m b ofs v,
valid_pointer ty m b ofs ->
exists m', store ty m b ofs v = Some m'.
End GEN_MEM.
Derived properties of the abstract memory model.
Module Gen_Mem_Facts(M: GEN_MEM).
Import M.
Lemma alloc_valid_block_inv:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') -> valid_block m b' -> valid_block m' b'.
Proof.
intros. rewrite (alloc_valid_block _ _ _ _ _ b' H). auto.
Qed.
Lemma alloc_not_valid_block_2:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') -> valid_block m b' -> b' <> b.
Proof.
intros. red; intros; subst b'.
elim (alloc_not_valid_block _ _ _ _ _ H). auto.
Qed.
Lemma load_alloc_other_2:
forall m lo hi b m' b' ty ofs v,
alloc m lo hi = Some(b, m') ->
load ty m b' ofs = Some v ->
load ty m' b' ofs = Some v.
Proof.
intros. rewrite <- H0. eapply load_alloc_other; eauto.
red; intro. subst b'.
elim (alloc_not_valid_block _ _ _ _ _ H).
eapply load_valid_block; eauto.
Qed.
Lemma alloc_result_valid_pointer:
forall m lo hi b m' ty ofs,
alloc m lo hi = Some(b, m') ->
(alignof ty | ofs) -> lo <= ofs -> ofs + sizeof ty <= hi ->
valid_pointer ty m' b ofs.
Proof.
intros; red.
split. rewrite (alloc_valid_block _ _ _ _ _ b H). tauto.
split. auto.
rewrite (alloc_result_bounds _ _ _ _ _ H). simpl. tauto.
Qed.
Lemma alloc_valid_pointer_inv:
forall m lo hi b m' ty b' ofs,
alloc m lo hi = Some(b, m') ->
valid_pointer ty m b' ofs -> valid_pointer ty m' b' ofs.
Proof.
intros. destruct H0 as [A [B [C D]]].
assert (b' <> b). eapply alloc_not_valid_block_2; eauto.
split. rewrite (alloc_valid_block _ _ _ _ _ b' H). auto.
split. auto.
rewrite (alloc_bounds_inv _ _ _ _ _ _ H H0). tauto.
Qed.
Lemma store_valid_pointer_inv:
forall ty m b ofs v m' ty' b' ofs',
store ty m b ofs v = Some m' ->
(valid_pointer ty' m' b' ofs' <-> valid_pointer ty' m b' ofs').
Proof.
intros. unfold valid_pointer.
rewrite (store_bounds_inv _ _ _ _ _ _ b' H).
rewrite (store_valid_block_inv _ _ _ _ _ _ b' H).
tauto.
Qed.
Lemma free_valid_pointer_inv:
forall m b m' ty b' ofs,
free m b = Some m' -> b' <> b ->
(valid_pointer ty m' b' ofs <-> valid_pointer ty m b' ofs).
Proof.
intros. unfold valid_pointer.
rewrite (free_bounds_inv _ _ _ _ H H0).
rewrite (free_valid_block _ _ _ _ H H0).
tauto.
Qed.
Section LOADV.
Variable proj_pointer: val -> option (block * Z).
Definition loadv (ty: memtype) (m: mem) (v: val) : option val :=
match proj_pointer v with
| Some(b, ofs) => load ty m b ofs
| None => None
end.
Definition storev (ty: memtype) (m: mem) (addr v: val) : option mem :=
match proj_pointer addr with
| Some(b, ofs) => store ty m b ofs v
| None => None
end.
End LOADV.
End Gen_Mem_Facts.
The concrete memory model is first specified by the properties it
satisfies.
Module Type REF_GEN_MEM.
Variable block: Set.
Hypothesis eq_block: forall (b1 b2: block), {b1=b2} + {b1<>b2}.
Variable mem: Set.
Variable empty: mem.
Variable alloc: mem -> Z -> Z -> option (block * mem).
Variable load: memtype -> mem -> block -> Z -> option val.
Variable store: memtype -> mem -> block -> Z -> val -> option mem.
Variable free: mem -> block -> option mem.
Properties inherited from the abstract memory model.
Hypothesis load_alloc_other:
forall m lo hi b m' ty b' ofs,
alloc m lo hi = Some (b, m') ->
b' <> b ->
load ty m' b' ofs = load ty m b' ofs.
Hypothesis load_store_same:
forall ty m b ofs v m' ty',
store ty m b ofs v = Some m' ->
compat ty ty' ->
load ty' m' b ofs = Some (convert ty' v).
Hypothesis load_store_disjoint:
forall ty m b ofs v m' ty' b' ofs',
store ty m b ofs v = Some m' ->
b' <> b \/ ofs' + sizeof ty' <= ofs \/ ofs + sizeof ty <= ofs' ->
load ty' m' b' ofs' = load ty' m b' ofs'.
Hypothesis load_free_other:
forall m b m' ty b' ofs,
free m b = Some m' ->
b' <> b ->
load ty m' b' ofs = load ty m b' ofs.
Variable valid_block: mem -> block -> Prop.
Hypothesis alloc_valid_block:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') ->
(valid_block m' b' <-> b' = b \/ valid_block m b').
Hypothesis alloc_not_valid_block:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> ~(valid_block m b).
Hypothesis load_valid_block:
forall ty m b ofs v,
load ty m b ofs = Some v -> valid_block m b.
Hypothesis store_valid_block:
forall ty m b ofs v m',
store ty m b ofs v = Some m' -> valid_block m b.
Hypothesis store_valid_block_inv:
forall ty m b ofs v m' b',
store ty m b ofs v = Some m' -> (valid_block m' b' <-> valid_block m b').
Hypothesis free_valid_block:
forall m b m' b',
free m b = Some m' -> b' <> b -> (valid_block m' b' <-> valid_block m b').
Hypothesis valid_block_free:
forall m b,
valid_block m b -> exists m', free m b = Some m'.
Variable bounds: mem -> block -> Z*Z.
Hypothesis alloc_result_bounds:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> bounds m' b = (lo, hi).
Hypothesis alloc_bounds_inv:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') -> b' <> b -> bounds m' b' = bounds m b'.
Hypothesis store_bounds_inv:
forall ty m b ofs v m' b',
store ty m b ofs v = Some m' -> bounds m' b' = bounds m b'.
Hypothesis free_bounds_inv:
forall m b m' b',
free m b = Some m' -> b' <> b -> bounds m' b' = bounds m b'.
Definition valid_pointer (ty: memtype) (m: mem) (b: block) (ofs: Z) : Prop :=
valid_block m b
/\ (alignof ty | ofs)
/\ fst (bounds m b) <= ofs
/\ ofs + sizeof ty <= snd (bounds m b).
Hypothesis valid_pointer_store:
forall ty m b ofs v,
valid_pointer ty m b ofs ->
exists m', store ty m b ofs v = Some m'.
Additional properties specific to the concrete memory model.
Hypothesis valid_pointer_load:
forall ty m b ofs,
valid_pointer ty m b ofs ->
exists v, load ty m b ofs = Some v.
Hypothesis store_valid_pointer:
forall ty m b ofs v m',
store ty m b ofs v = Some m' -> valid_pointer ty m b ofs.
Hypothesis load_valid_pointer:
forall ty m b ofs v,
load ty m b ofs = Some v -> valid_pointer ty m b ofs.
Hypothesis load_alloc_same:
forall m lo hi b m' ty ofs v,
alloc m lo hi = Some (b, m') ->
load ty m' b ofs = Some v ->
v = vundef.
Hypothesis load_store_mismatch:
forall ty m b ofs v m' ty' v',
store ty m b ofs v = Some m' ->
~(compat ty ty') ->
load ty' m' b ofs = Some v' ->
v' = vundef.
Hypothesis load_store_overlap:
forall ty m b ofs v m' ty' ofs' v',
store ty m b ofs v = Some m' ->
ofs' <> ofs -> ofs' + sizeof ty' > ofs -> ofs + sizeof ty > ofs' ->
load ty' m' b ofs' = Some v' ->
v' = vundef.
Variable fresh_block: mem -> block -> Prop.
Hypothesis fresh_valid_block_exclusive:
forall m b,
fresh_block m b -> valid_block m b -> False.
Hypothesis alloc_fresh_block:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') ->
(fresh_block m' b' <-> b <> b' /\ fresh_block m b').
Hypothesis alloc_fresh_block_2:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> fresh_block m b.
Hypothesis store_fresh_block:
forall m chunk b ofs v m' b',
store chunk m b ofs v = Some m' ->
(fresh_block m' b' <-> fresh_block m b').
Hypothesis free_fresh_block:
forall m b m' b',
free m b = Some m' ->
(fresh_block m' b' <-> fresh_block m b').
Definition same_domain (m1 m2: mem) : Prop :=
forall b, fresh_block m1 b <-> fresh_block m2 b.
Hypothesis alloc_same_domain:
forall m1 lo1 hi1 b1 m1' m2 lo2 hi2 b2 m2',
alloc m1 lo1 hi1 = Some(b1, m1') ->
alloc m2 lo2 hi2 = Some(b2, m2') ->
same_domain m1 m2 ->
b1 = b2 /\ same_domain m1' m2'.
Hypothesis free_not_valid_block:
forall m b m',
free m b = Some m' -> ~(valid_block m' b).
Hypothesis free_same_bounds:
forall m b m',
free m b = Some m' ->
fst(bounds m' b) = snd(bounds m' b).
End REF_GEN_MEM.
Derived properties of the concrete memory model.
Module Ref_Gen_Mem_Facts(M: REF_GEN_MEM).
Import M.
Module MF := Gen_Mem_Facts(M).
Import MF.
Lemma store_valid_pointer_2:
forall ty m b ofs v m',
store ty m b ofs v = Some m' -> valid_pointer ty m' b ofs.
Proof.
intros. rewrite (store_valid_pointer_inv _ _ _ _ _ _ ty b ofs H).
eapply store_valid_pointer; eauto.
Qed.
Lemma load_alloc_same_2:
forall m lo hi b m' ty ofs,
alloc m lo hi = Some (b, m') ->
(alignof ty | ofs) -> lo <= ofs -> ofs + sizeof ty <= hi ->
load ty m' b ofs = Some vundef.
Proof.
intros.
assert (valid_pointer ty m' b ofs).
split. rewrite (alloc_valid_block _ _ _ _ _ b H). auto.
rewrite (alloc_result_bounds _ _ _ _ _ H). simpl; tauto.
destruct (valid_pointer_load _ _ _ _ H3) as [v LOAD].
assert (v = vundef).
eapply load_alloc_same; eauto.
congruence.
Qed.
Lemma load_store_mismatch_2:
forall ty m b ofs v m' ty',
store ty m b ofs v = Some m' ->
~(compat ty ty') ->
valid_pointer ty' m b ofs ->
load ty' m' b ofs = Some vundef.
Proof.
intros.
assert (valid_pointer ty' m' b ofs).
rewrite (MF.store_valid_pointer_inv _ _ _ _ _ _ ty' b ofs H). auto.
destruct (valid_pointer_load _ _ _ _ H2) as [v' LOAD].
assert (v' = vundef).
eapply load_store_mismatch; eauto.
congruence.
Qed.
Lemma load_store_overlap_2:
forall ty m b ofs v m' ty' ofs',
store ty m b ofs v = Some m' ->
ofs' <> ofs -> ofs' + sizeof ty' > ofs -> ofs + sizeof ty > ofs' ->
valid_pointer ty' m b ofs' ->
load ty' m' b ofs' = Some vundef.
Proof.
intros.
assert (valid_pointer ty' m' b ofs').
rewrite (MF.store_valid_pointer_inv _ _ _ _ _ _ ty' b ofs' H). auto.
destruct (valid_pointer_load _ _ _ _ H4) as [v' LOAD].
assert (v' = vundef).
eapply load_store_overlap; eauto.
congruence.
Qed.
Inductive load_store_cases
(ty1: memtype) (b1: block) (ofs1: Z)
(ty2: memtype) (b2: block) (ofs2: Z) : Set :=
| lsc_similar:
b1 = b2 -> ofs1 = ofs2 -> compat ty1 ty2 ->
load_store_cases ty1 b1 ofs1 ty2 b2 ofs2
| lsc_other:
b1 <> b2 \/ ofs2 + sizeof ty2 <= ofs1 \/ ofs1 + sizeof ty1 <= ofs2 ->
load_store_cases ty1 b1 ofs1 ty2 b2 ofs2
| lsc_overlap:
b1 = b2 -> ofs1 <> ofs2 -> ofs2 + sizeof ty2 > ofs1 -> ofs1 + sizeof ty1 > ofs2 ->
load_store_cases ty1 b1 ofs1 ty2 b2 ofs2
| lsc_mismatch:
b1 = b2 -> ofs1 = ofs2 -> ~compat ty1 ty2 ->
load_store_cases ty1 b1 ofs1 ty2 b2 ofs2.
Definition load_store_classification:
forall (ty1: memtype) (b1: block) (ofs1: Z)
(ty2: memtype) (b2: block) (ofs2: Z),
load_store_cases ty1 b1 ofs1 ty2 b2 ofs2.
Proof.
intros. destruct (eq_block b1 b2).
destruct (zeq ofs1 ofs2).
destruct (compat_dec ty1 ty2).
apply lsc_similar; auto.
apply lsc_mismatch; auto.
destruct (zle (ofs2 + sizeof ty2) ofs1).
apply lsc_other. tauto.
destruct (zle (ofs1 + sizeof ty1) ofs2).
apply lsc_other. tauto.
apply lsc_overlap; auto.
apply lsc_other; tauto.
Qed.
Lemma load_store_characterization:
forall ty m1 b ofs v m2 ty' b' ofs',
store ty m1 b ofs v = Some m2 ->
valid_pointer ty' m1 b' ofs' ->
load ty' m2 b' ofs' =
match load_store_classification ty b ofs ty' b' ofs' with
| lsc_similar _ _ _ => Some (convert ty' v)
| lsc_other _ => load ty' m1 b' ofs'
| lsc_overlap _ _ _ _ => Some vundef
| lsc_mismatch _ _ _ => Some vundef
end.
Proof.
intros.
assert (valid_pointer ty' m2 b' ofs').
rewrite (MF.store_valid_pointer_inv _ _ _ _ _ _ ty' b' ofs' H). auto.
destruct (valid_pointer_load _ _ _ _ H1) as [v' LOAD].
destruct (load_store_classification ty b ofs ty' b' ofs').
subst b' ofs'. eapply load_store_same; eauto.
eapply load_store_disjoint; eauto. intuition.
subst b'. rewrite LOAD. f_equal.
eapply load_store_overlap; eauto.
subst b' ofs'. rewrite LOAD. f_equal.
eapply load_store_mismatch; eauto.
Qed.
Lemma store_same_domain:
forall ty1 m1 b1 ofs1 v1 m1' ty2 m2 b2 ofs2 v2 m2',
store ty1 m1 b1 ofs1 v1 = Some m1' ->
store ty2 m2 b2 ofs2 v2 = Some m2' ->
same_domain m1 m2 ->
same_domain m1' m2'.
Proof.
intros; red; intros.
rewrite (store_fresh_block _ _ _ _ _ _ b H).
rewrite (store_fresh_block _ _ _ _ _ _ b H0).
apply H1.
Qed.
Lemma free_same_domain:
forall m1 b m1' m2 m2',
free m1 b = Some m1' ->
free m2 b = Some m2' ->
same_domain m1 m2 ->
same_domain m1' m2'.
Proof.
unfold same_domain; intros.
rewrite (free_fresh_block _ _ _ b0 H).
rewrite (free_fresh_block _ _ _ b0 H0).
auto.
Qed.
Lemma free_not_valid_pointer:
forall m b m',
free m b = Some m' ->
forall ty ofs, ~(valid_pointer ty m' b ofs).
Proof.
intros; red; intros. destruct H0 as [A [B [C D]]].
rewrite (free_same_bounds _ _ _ H) in C; simpl in C.
generalize (sizeof_pos ty). omega.
Qed.
End Ref_Gen_Mem_Facts.
An implementation of the concrete memory model
Definition update (A: Set) (x: Z) (v: A) (f: Z -> A): Z -> A :=
fun y => if zeq y x then v else f y.
Implicit Arguments update [A].
Lemma update_s:
forall (A: Set) (x: Z) (v: A) (f: Z -> A),
update x v f x = v.
Proof.
intros; unfold update; destruct (zeq x x); congruence.
Qed.
Lemma update_o:
forall (A: Set) (x: Z) (v: A) (f: Z -> A) (y: Z),
y <> x -> update x v f y = f y.
Proof.
intros; unfold update; destruct (zeq y x); congruence.
Qed.
Module Concrete_Mem <: REF_GEN_MEM.
Definition block := Z.
Lemma eq_block: forall (b1 b2: block), {b1=b2} + {b1<>b2}.
Proof zeq.
Definition content := option (memtype * val).
Record mem_ : Set := mkmem {
nextblock: Z;
bounds: block -> Z*Z;
freed: block -> bool;
contents: block -> Z -> content
}.
Definition mem := mem_.
Definition empty: mem :=
mkmem 1
(fun (b: block) => (0, 0))
(fun (b: block) => false)
(fun (b: block) (ofs: Z) => None).
Definition fresh_block (m: mem) (b: block) : Prop :=
b >= nextblock m.
Definition valid_block (m: mem) (b: block) : Prop :=
b < nextblock m /\ freed m b = false.
Lemma valid_block_dec:
forall m b, {valid_block m b} + {~valid_block m b}.
Proof.
intros; unfold valid_block. destruct (zlt b (nextblock m)).
destruct (freed m b).
right; red; intros [A B]; congruence.
left; auto.
right; red; intros [A B]; omega.
Qed.
Definition valid_pointer (ty: memtype) (m: mem) (b: block) (ofs: Z) : Prop :=
valid_block m b
/\ (alignof ty | ofs)
/\ fst (bounds m b) <= ofs
/\ ofs + sizeof ty <= snd (bounds m b).
Remark Zdivide_Zmod:
forall a b, b > 0 -> ((b | a) <-> Zmod a b = 0).
Proof.
intros; split; intros.
apply Z_div_exact_1. auto. inv H0. rewrite Z_div_mult; auto. ring.
exists (a / b).
transitivity (b * (a / b) + (a mod b)). apply Z_div_mod_eq; auto.
transitivity (b * (a / b)). omega.
ring.
Qed.
Lemma aligned_dec:
forall ty ofs, {(alignof ty | ofs)} + {~(alignof ty | ofs)}.
Proof.
intros. generalize (Zdivide_Zmod ofs (alignof ty) (alignof_pos ty)); intro.
destruct (zeq (Zmod ofs (alignof ty)) 0).
left. rewrite H. auto.
right. rewrite H. auto.
Qed.
Lemma valid_pointer_dec:
forall ty m b ofs, {valid_pointer ty m b ofs} + {~valid_pointer ty m b ofs}.
Proof.
intros. unfold valid_pointer.
destruct (valid_block_dec m b).
destruct (aligned_dec ty ofs).
destruct (zle (fst (bounds m b)) ofs).
destruct (zle (ofs + sizeof ty) (snd (bounds m b))).
left; auto.
right. red. intros [A [B [C D]]]. omega.
right. red. intros [A [B [C D]]]. omega.
right. tauto.
right. tauto.
Qed.
Definition nat_of_Z (z: Z) : nat :=
match z with
| Z0 => O
| Zpos p => nat_of_P p
| Zneg p => O
end.
Lemma nat_of_Z_eq:
forall z, z >= 0 -> Z_of_nat (nat_of_Z z) = z.
Proof.
intros. destruct z; simpl.
auto.
symmetry. apply Zpos_eq_Z_of_nat_o_nat_of_P.
compute in H. congruence.
Qed.
Fixpoint check_cont (f: Z -> content) (ofs: Z) (n: nat) {struct n} : bool :=
match n with
| O => true
| S n' =>
match f ofs with
| None => check_cont f (ofs + 1) n'
| _ => false
end
end.
Lemma check_cont_charact:
forall f n ofs,
if check_cont f ofs n
then (forall i, ofs <= i < ofs + Z_of_nat n -> f i = None)
else (exists i, ofs <= i < ofs + Z_of_nat n /\ f i <> None).
Proof.
induction n; intros.
simpl. intros. elimtype False; omega.
rewrite inj_S. simpl.
case_eq (f ofs); intros.
exists ofs. split. omega. congruence.
generalize (IHn (ofs + 1)). destruct (check_cont f (ofs + 1)).
intros. assert (i = ofs \/ ofs + 1 <= i < (ofs + 1) + (Z_of_nat n)) by omega.
destruct H2. congruence.
apply H0. auto.
intros [i [A B]]. exists i; split. omega. auto.
Qed.
Lemma check_cont_exten:
forall f1 f2 n ofs,
(forall i, ofs <= i < ofs + Z_of_nat n -> f2 i = f1 i) ->
check_cont f2 ofs n = check_cont f1 ofs n.
Proof.
induction n; intros; simpl.
auto.
rewrite inj_S in H.
rewrite H. destruct (f1 ofs); auto. apply IHn.
intros. apply H. omega. omega.
Qed.
Definition load_contents (ty: memtype) (f: Z -> content) (ofs: Z) : val :=
match f ofs with
| Some(ty', v) =>
if compat_dec ty' ty then
if check_cont f (ofs + 1) (nat_of_Z (sizeof ty - 1))
then convert ty v
else vundef
else vundef
| _ => vundef
end.
Lemma load_contents_exten:
forall f1 f2 ty ofs,
(forall i, ofs <= i < ofs + sizeof ty -> f2 i = f1 i) ->
load_contents ty f2 ofs = load_contents ty f1 ofs.
Proof.
intros. unfold load_contents.
rewrite H. destruct (f1 ofs).
destruct p as [ty' v].
destruct (compat_dec ty' ty); auto.
rewrite (check_cont_exten f1 f2).
destruct (check_cont f1 (ofs + 1) (nat_of_Z (sizeof ty - 1))); auto.
intros. apply H. rewrite nat_of_Z_eq in H0. omega.
generalize (sizeof_pos ty); omega.
auto.
generalize (sizeof_pos ty); omega.
Qed.
Lemma load_contents_1:
forall ty f ofs ty' v,
f ofs = Some(ty', v) ->
compat ty' ty ->
(forall i, ofs + 1 <= i < ofs + sizeof ty -> f i = None) ->
load_contents ty f ofs = convert ty v.
Proof.
intros. unfold load_contents.
rewrite H. destruct (compat_dec ty' ty). 2:contradiction.
generalize (check_cont_charact f (nat_of_Z (sizeof ty - 1)) (ofs + 1)).
destruct (check_cont f (ofs + 1) (nat_of_Z (sizeof ty - 1))).
auto.
intros [i [A B]]. elim B. apply H1.
rewrite nat_of_Z_eq in A. omega.
generalize (sizeof_pos ty). omega.
Qed.
Lemma load_contents_2:
forall ty f ofs,
f ofs = None ->
load_contents ty f ofs = vundef.
Proof.
intros. unfold load_contents. rewrite H. auto.
Qed.
Lemma load_contents_3:
forall ty f ofs ty' v,
f ofs = Some(ty', v) ->
~compat ty' ty ->
load_contents ty f ofs = vundef.
Proof.
intros; unfold load_contents. rewrite H.
destruct (compat_dec ty' ty). contradiction. auto.
Qed.
Lemma load_contents_4:
forall ty f ofs i,
ofs + 1 <= i < ofs + sizeof ty -> f i <> None ->
load_contents ty f ofs = vundef.
Proof.
intros. unfold load_contents.
destruct (f ofs). destruct p as [ty' v].
destruct (compat_dec ty' ty); auto.
generalize (check_cont_charact f (nat_of_Z (sizeof ty - 1)) (ofs + 1)).
destruct (check_cont f (ofs + 1) (nat_of_Z (sizeof ty - 1))).
intro. elim H0. apply H1. rewrite nat_of_Z_eq. omega.
generalize (sizeof_pos ty). omega.
auto.
auto.
Qed.
Fixpoint set_cont (f: Z -> content) (ofs: Z) (n: nat) {struct n} : Z -> content :=
match n with
| O => f
| S n' => set_cont (update ofs None f) (ofs + 1) n'
end.
Lemma set_cont_outside:
forall n f ofs i,
i < ofs \/ i >= ofs + Z_of_nat n -> set_cont f ofs n i = f i.
Proof.
induction n; intros; simpl.
auto.
rewrite inj_S in H. rewrite IHn. apply update_o. omega. omega.
Qed.
Lemma set_cont_inside:
forall n f ofs i,
ofs <= i < ofs + Z_of_nat n -> set_cont f ofs n i = None.
Proof.
induction n; intros; simpl.
simpl in H. elimtype False; omega.
rewrite inj_S in H.
assert (i = ofs \/ ofs + 1 <= i < (ofs + 1) + Z_of_nat n) by omega.
destruct H0. subst i. rewrite set_cont_outside. apply update_s. omega.
apply IHn. omega.
Qed.
Definition store_contents (f: Z -> content) (ty: memtype) (ofs: Z) (v: val): Z -> content :=
set_cont (update ofs (Some (ty, v)) f) (ofs + 1) (nat_of_Z (sizeof ty - 1)).
Lemma store_contents_at:
forall f ty ofs v,
store_contents f ty ofs v ofs = Some (ty, v).
Proof.
intros; unfold store_contents.
rewrite set_cont_outside. apply update_s. omega.
Qed.
Lemma store_contents_cont:
forall f ty ofs v i,
ofs < i < ofs + sizeof ty ->
store_contents f ty ofs v i = None.
Proof.
intros; unfold store_contents.
apply set_cont_inside. rewrite nat_of_Z_eq. omega.
generalize (sizeof_pos ty); omega.
Qed.
Lemma store_contents_outside:
forall f ty ofs v i,
i < ofs \/ i >= ofs + sizeof ty ->
store_contents f ty ofs v i = f i.
Proof.
intros; unfold store_contents.
rewrite set_cont_outside. apply update_o.
generalize (sizeof_pos ty). omega.
rewrite nat_of_Z_eq. omega.
generalize (sizeof_pos ty); omega.
Qed.
Lemma load_store_contents_same:
forall f ty ty' ofs v,
compat ty ty' ->
load_contents ty' (store_contents f ty ofs v) ofs = convert ty' v.
Proof.
intros. apply load_contents_1 with ty.
apply store_contents_at. auto.
intros. apply store_contents_cont.
rewrite <- (compat_sizeof _ _ H). omega.
Qed.
Lemma load_store_contents_disjoint:
forall f ty ty' ofs ofs' v,
ofs' + sizeof ty' <= ofs \/ ofs + sizeof ty <= ofs' ->
load_contents ty' (store_contents f ty ofs v) ofs' =
load_contents ty' f ofs'.
Proof.
intros. apply load_contents_exten.
intros. apply store_contents_outside. omega.
Qed.
Lemma load_store_contents_mismatch:
forall f ty ty' ofs v,
~compat ty ty' ->
load_contents ty' (store_contents f ty ofs v) ofs = vundef.
Proof.
intros. eapply load_contents_3; eauto.
apply store_contents_at.
Qed.
Lemma load_store_contents_overlap:
forall f ty ty' ofs ofs' v,
ofs' <> ofs -> ofs' + sizeof ty' > ofs -> ofs + sizeof ty > ofs' ->
load_contents ty' (store_contents f ty ofs v) ofs' = vundef.
Proof.
intros. generalize (sizeof_pos ty); generalize (sizeof_pos ty'); intros.
assert (ofs < ofs' < ofs + sizeof ty
\/ ofs' < ofs < ofs' + sizeof ty') by omega.
destruct H4.
apply load_contents_2.
rewrite store_contents_cont. auto. auto.
apply load_contents_4 with ofs. omega.
rewrite store_contents_at. congruence.
Qed.
Parameter enough_free_memory: mem -> Z -> bool.
Definition alloc (m: mem) (lo hi: Z) : option (block * mem) :=
if enough_free_memory m (hi - lo)
then Some(nextblock m,
mkmem (nextblock m + 1)
(update (nextblock m) (lo, hi) (bounds m))
(update (nextblock m) false (freed m))
(update (nextblock m) (fun (ofs: Z) => None) (contents m)))
else None.
Definition load (ty: memtype) (m: mem) (b: block) (ofs: Z) : option val :=
if valid_pointer_dec ty m b ofs
then Some (load_contents ty (contents m b) ofs)
else None.
Definition store (ty: memtype) (m: mem) (b: block) (ofs: Z) (v: val) : option mem :=
if valid_pointer_dec ty m b ofs
then Some(mkmem (nextblock m)
(bounds m)
(freed m)
(update b (store_contents (contents m b) ty ofs v) (contents m)))
else None.
Definition free (m: mem) (b: block) : option mem :=
if freed m b
then None
else Some(mkmem (nextblock m)
(update b (0,0) (bounds m))
(update b true (freed m))
(contents m)).
Lemma alloc_result_bounds:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> bounds m' b = (lo, hi).
Proof.
unfold alloc; intros.
destruct (enough_free_memory m (hi-lo)); inv H; simpl.
apply update_s.
Qed.
Lemma alloc_bounds_inv:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') -> b' <> b -> bounds m' b' = bounds m b'.
Proof.
unfold alloc; intros.
destruct (enough_free_memory m (hi-lo)); inv H; simpl.
apply update_o. auto.
Qed.
Lemma store_bounds_inv:
forall ty m b ofs v m' b',
store ty m b ofs v = Some m' -> bounds m' b' = bounds m b'.
Proof.
unfold store; intros.
destruct (valid_pointer_dec ty m b ofs); inv H; simpl.
auto.
Qed.
Lemma free_bounds_inv:
forall m b m' b',
free m b = Some m' -> b' <> b -> bounds m' b' = bounds m b'.
Proof.
unfold free; intros. destruct (freed m b); inv H; simpl. apply update_o. auto.
Qed.
Lemma fresh_valid_block_exclusive:
forall m b,
fresh_block m b -> valid_block m b -> False.
Proof.
unfold fresh_block, valid_block; intros.
destruct H0. omega.
Qed.
Lemma alloc_fresh_block:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') ->
(fresh_block m' b' <-> b <> b' /\ fresh_block m b').
Proof.
unfold alloc, fresh_block; intros.
destruct (enough_free_memory m (hi-lo)); inv H; simpl.
unfold block. split; intros; omega.
Qed.
Lemma alloc_fresh_block_2:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> fresh_block m b.
Proof.
unfold alloc, fresh_block; intros.
destruct (enough_free_memory m (hi-lo)); inv H; simpl.
omega.
Qed.
Lemma store_inversion:
forall ty m b ofs v m',
store ty m b ofs v = Some m' ->
valid_pointer ty m b ofs /\
m' = mkmem (nextblock m)
(bounds m)
(freed m)
(update b (store_contents (contents m b) ty ofs v) (contents m)).
Proof.
unfold store; intros.
destruct (valid_pointer_dec ty m b ofs); inv H. auto.
Qed.
Lemma store_fresh_block:
forall m chunk b ofs v m' b',
store chunk m b ofs v = Some m' ->
(fresh_block m' b' <-> fresh_block m b').
Proof.
intros. destruct (store_inversion _ _ _ _ _ _ H) as [A B].
unfold fresh_block; rewrite B; simpl. tauto.
Qed.
Lemma free_fresh_block:
forall m b m' b',
free m b = Some m' ->
(fresh_block m' b' <-> fresh_block m b').
Proof.
unfold free. intros. destruct (freed m b); inv H; unfold fresh_block; simpl. tauto.
Qed.
Lemma alloc_valid_block:
forall m lo hi b m' b',
alloc m lo hi = Some(b, m') ->
(valid_block m' b' <-> b' = b \/ valid_block m b').
Proof.
unfold alloc, valid_block; intros.
destruct (enough_free_memory m (hi-lo)); inv H; simpl.
unfold update. destruct (zeq b' (nextblock m)).
subst b'; intuition.
intuition.
Qed.
Lemma alloc_not_valid_block:
forall m lo hi b m',
alloc m lo hi = Some(b, m') -> ~(valid_block m b).
Proof.
intros; red; intros. eapply fresh_valid_block_exclusive; eauto.
eapply alloc_fresh_block_2; eauto.
Qed.
Lemma load_valid_block:
forall ty m b ofs v,
load ty m b ofs = Some v -> valid_block m b.
Proof.
unfold load; intros. destruct (valid_pointer_dec ty m b); inv H.
inv v0; auto.
Qed.
Lemma store_valid_block:
forall ty m b ofs v m',
store ty m b ofs v = Some m' -> valid_block m b.
Proof.
unfold store; intros. destruct (valid_pointer_dec ty m b); inv H.
inv v0; auto.
Qed.
Lemma store_valid_block_inv:
forall ty m b ofs v m' b',
store ty m b ofs v = Some m' -> (valid_block m' b' <-> valid_block m b').
Proof.
unfold store, valid_block; intros.
destruct (valid_pointer_dec ty m b); inv H; simpl.
tauto.
Qed.
Lemma free_valid_block:
forall m b m' b',
free m b = Some m' -> b' <> b -> (valid_block m' b' <-> valid_block m b').
Proof.
unfold free; intros. destruct (freed m b); inv H; unfold valid_block; simpl.
rewrite update_o. tauto. auto.
Qed.
Lemma store_valid_pointer_inv:
forall ty m b ofs v m' ty' b' ofs',
store ty m b ofs v = Some m' ->
(valid_pointer ty' m' b' ofs' <-> valid_pointer ty' m b' ofs').
Proof.
intros. unfold valid_pointer.
rewrite (store_bounds_inv _ _ _ _ _ _ b' H).
rewrite (store_valid_block_inv _ _ _ _ _ _ b' H).
tauto.
Qed.
Lemma alloc_valid_pointer_inv:
forall m lo hi b m' ty b' ofs,
alloc m lo hi = Some(b, m') -> b' <> b ->
(valid_pointer ty m b' ofs <-> valid_pointer ty m' b' ofs).
Proof.
intros. unfold valid_pointer.
rewrite (alloc_valid_block _ _ _ _ _ b' H).
rewrite (alloc_bounds_inv _ _ _ _ _ _ H H0). tauto.
Qed.
Lemma free_valid_pointer_inv:
forall m b m' ty b' ofs,
free m b = Some m' -> b' <> b ->
(valid_pointer ty m' b' ofs <-> valid_pointer ty m b' ofs).
Proof.
intros. unfold valid_pointer.
rewrite (free_bounds_inv _ _ _ _ H H0).
rewrite (free_valid_block _ _ _ _ H H0).
tauto.
Qed.
Lemma load_alloc_other:
forall m lo hi b m' ty b' ofs,
alloc m lo hi = Some (b, m') ->
b' <> b ->
load ty m' b' ofs = load ty m b' ofs.
Proof.
intros. unfold load.
destruct (valid_pointer_dec ty m b' ofs).
rewrite (alloc_valid_pointer_inv _ _ _ _ _ ty _ ofs H H0) in v.
destruct (valid_pointer_dec ty m' b' ofs); try contradiction.
f_equal. f_equal.
unfold alloc in H; destruct (enough_free_memory m (hi-lo)); inv H; simpl.
apply update_o; auto.
rewrite (alloc_valid_pointer_inv _ _ _ _ _ ty _ ofs H H0) in n.
destruct (valid_pointer_dec ty m' b' ofs); try contradiction. auto.
Qed.
Lemma valid_pointer_compat:
forall ty m b ofs ty',
compat ty ty' ->
(valid_pointer ty m b ofs <-> valid_pointer ty' m b ofs).
Proof.
unfold valid_pointer; intros.
rewrite (compat_sizeof _ _ H). rewrite (compat_alignof _ _ H).
tauto.
Qed.
Lemma load_store_same:
forall ty m b ofs v m' ty',
store ty m b ofs v = Some m' ->
compat ty ty' ->
load ty' m' b ofs = Some (convert ty' v).
Proof.
intros. destruct (store_inversion _ _ _ _ _ _ H).
unfold load. destruct (valid_pointer_dec ty' m' b ofs).
f_equal. rewrite H2; simpl. rewrite update_s. apply load_store_contents_same; auto.
elim n.
rewrite <- (valid_pointer_compat ty m' b ofs ty' H0).
rewrite (store_valid_pointer_inv _ _ _ _ _ _ ty b ofs H). auto.
Qed.
Lemma load_store_disjoint:
forall ty m b ofs v m' ty' b' ofs',
store ty m b ofs v = Some m' ->
b' <> b \/ ofs' + sizeof ty' <= ofs \/ ofs + sizeof ty <= ofs' ->
load ty' m' b' ofs' = load ty' m b' ofs'.
Proof.
intros. destruct (store_inversion _ _ _ _ _ _ H).
unfold load.
destruct (valid_pointer_dec ty' m' b' ofs').
rewrite (store_valid_pointer_inv _ _ _ _ _ _ ty' b' ofs' H) in v0.
destruct (valid_pointer_dec ty' m b' ofs'); try contradiction.
f_equal. rewrite H2; simpl; unfold update. destruct (zeq b' b).
subst b'. apply load_store_contents_disjoint. destruct H0. congruence. auto.
auto.
rewrite (store_valid_pointer_inv _ _ _ _ _ _ ty' b' ofs' H) in n.
destruct (valid_pointer_dec ty' m b' ofs'); try contradiction. auto.
Qed.
Lemma load_free_other:
forall m b m' ty b' ofs,
free m b = Some m' ->
b' <> b ->
load ty m' b' ofs = load ty m b' ofs.
Proof.
intros. unfold load. destruct (valid_pointer_dec ty m' b' ofs).
rewrite (free_valid_pointer_inv _ _ _ ty b' ofs H H0) in v.
destruct (valid_pointer_dec ty m b' ofs); try contradiction.
f_equal. f_equal.
unfold free in H; destruct (freed m b); inv H; simpl. auto.
rewrite (free_valid_pointer_inv _ _ _ ty b' ofs H H0) in n.
destruct (valid_pointer_dec ty m b' ofs); try contradiction. auto.
Qed.
Lemma load_alloc_same:
forall m lo hi b m' ty ofs v,
alloc m lo hi = Some (b, m') ->
load ty m' b ofs = Some v ->
v = vundef.
Proof.
unfold alloc, load; intros.
destruct (valid_pointer_dec ty m' b ofs); inv H0.
destruct (enough_free_memory m (hi-lo)); inv H; simpl.
rewrite update_s. apply load_contents_2. auto.
Qed.
Lemma load_store_mismatch:
forall ty m b ofs v m' ty' v',
store ty m b ofs v = Some m' ->
~(compat ty ty') ->
load ty' m' b ofs = Some v' ->
v' = vundef.
Proof.
unfold load, store; intros.
destruct (valid_pointer_dec ty' m' b ofs); inv H1.
destruct (valid_pointer_dec ty m b ofs); inversion H.
simpl. rewrite update_s.
apply load_store_contents_mismatch; auto.
Qed.
Lemma load_store_overlap:
forall ty m b ofs v m' ty' ofs' v',
store ty m b ofs v = Some m' ->
ofs' <> ofs -> ofs' + sizeof ty' > ofs -> ofs + sizeof ty > ofs' ->
load ty' m' b ofs' = Some v' ->
v' = vundef.
Proof.
unfold load, store; intros.
destruct (valid_pointer_dec ty' m' b ofs'); inv H3.
destruct (valid_pointer_dec ty m b ofs); inversion H.
simpl. rewrite update_s.
apply load_store_contents_overlap; auto.
Qed.
Definition same_domain (m1 m2: mem) : Prop :=
forall b, fresh_block m1 b <-> fresh_block m2 b.
Lemma same_domain_same_nextblock:
forall m1 m2, same_domain m1 m2 -> nextblock m2 = nextblock m1.
Proof.
unfold same_domain, fresh_block; intros.
assert (nextblock m2 >= nextblock m1).
rewrite H. omega.
assert (nextblock m1 >= nextblock m2).
rewrite <- H. omega.
unfold block. omega.
Qed.
Lemma alloc_same_domain:
forall m1 lo1 hi1 b1 m1' m2 lo2 hi2 b2 m2',
alloc m1 lo1 hi1 = Some(b1, m1') ->
alloc m2 lo2 hi2 = Some(b2, m2') ->
same_domain m1 m2 ->
b1 = b2 /\ same_domain m1' m2'.
Proof.
unfold alloc; intros.
destruct (enough_free_memory m1 (hi1-lo1)); inv H; simpl.
destruct (enough_free_memory m2 (hi2-lo2)); inv H0; simpl.
unfold same_domain, fresh_block; simpl.
rewrite (same_domain_same_nextblock _ _ H1).
split. auto. intros. tauto.
Qed.
Lemma valid_block_free:
forall m b,
valid_block m b -> exists m', free m b = Some m'.
Proof.
intros. destruct H. unfold free. rewrite H0.
econstructor. reflexivity.
Qed.
Lemma valid_pointer_store:
forall ty m b ofs v,
valid_pointer ty m b ofs ->
exists m', store ty m b ofs v = Some m'.
Proof.
intros. unfold store.
destruct (valid_pointer_dec ty m b ofs).
econstructor; reflexivity.
contradiction.
Qed.
Lemma store_valid_pointer:
forall ty m b ofs v m',
store ty m b ofs v = Some m' -> valid_pointer ty m b ofs.
Proof.
intros. destruct (store_inversion _ _ _ _ _ _ H). auto.
Qed.
Lemma valid_pointer_load:
forall ty m b ofs,
valid_pointer ty m b ofs ->
exists v, load ty m b ofs = Some v.
Proof.
intros. unfold load. destruct (valid_pointer_dec ty m b ofs).
econstructor. reflexivity.
contradiction.
Qed.
Lemma load_valid_pointer:
forall ty m b ofs v,
load ty m b ofs = Some v -> valid_pointer ty m b ofs.
Proof.
unfold load; intros. destruct (valid_pointer_dec ty m b ofs).
auto. discriminate.
Qed.
Lemma free_not_valid_block:
forall m b m',
free m b = Some m' ->
~(valid_block m' b).
Proof.
unfold free, valid_block; intros. destruct (freed m b); inv H; simpl.
rewrite update_s. red; intros [A B]; congruence.
Qed.
Lemma free_same_bounds:
forall m b m',
free m b = Some m' ->
fst(bounds m' b) = snd(bounds m' b).
Proof.
unfold free; intros. destruct (freed m b); inv H; simpl.
rewrite update_s. auto.
Qed.
End Concrete_Mem.
Module Rel_Mem(M: REF_GEN_MEM).
Module MF := Gen_Mem_Facts(M).
Module RMF := Ref_Gen_Mem_Facts(M).
Import M.
Import MF.
Import RMF.
Section GENERIC_EMBEDDING.
Definition embedding : Set := block -> option (block * Z).
Variable val_emb: embedding -> val -> val -> Prop.
Definition mem_emb (emb: embedding) (m1 m2: mem) :=
forall ty b1 ofs v1 b2 delta,
emb b1 = Some(b2, delta) ->
load ty m1 b1 ofs = Some v1 ->
exists v2, load ty m2 b2 (ofs + delta) = Some v2 /\ val_emb emb v1 v2.
Lemma valid_pointer_emb:
forall emb m1 m2 ty b1 ofs b2 delta,
emb b1 = Some(b2, delta) ->
mem_emb emb m1 m2 ->
valid_pointer ty m1 b1 ofs ->
valid_pointer ty m2 b2 (ofs + delta).
Proof.
intros.
destruct (valid_pointer_load _ _ _ _ H1) as [v1 LOAD1].
destruct (H0 _ _ _ _ _ _ H LOAD1) as [v2 [LOAD2 VEMB]].
eapply load_valid_pointer; eauto.
Qed.
Lemma store_unmapped_emb:
forall emb m1 m2 b ofs v ty m1',
mem_emb emb m1 m2 ->
emb b = None ->
store ty m1 b ofs v = Some m1' ->
mem_emb emb m1' m2.
Proof.
intros; red; intros.
assert (load ty0 m1 b1 ofs0 = Some v1).
rewrite <- H3. symmetry. eapply load_store_disjoint; eauto.
left. congruence.
eapply H; eauto.
Qed.
Lemma store_outside_emb:
forall emb m1 m2 ty b ofs v m2',
mem_emb emb m1 m2 ->
(forall b' delta,
emb b' = Some(b, delta) ->
snd(bounds m1 b') + delta <= ofs \/ ofs + sizeof ty <= fst(bounds m1 b') + delta) ->
store ty m2 b ofs v = Some m2' ->
mem_emb emb m1 m2'.
Proof.
intros; red; intros.
destruct (H _ _ _ _ _ _ H2 H3) as [v2 [LOAD2 VEMB]].
exists v2; split.
rewrite <- LOAD2. eapply load_store_disjoint; eauto.
destruct (eq_block b2 b).
subst b2. generalize (H0 _ _ H2); intro.
destruct (load_valid_pointer _ _ _ _ _ H3) as [A [B [C D]]].
right. omega.
auto.
auto.
Qed.
Definition embedding_no_overlap (emb: embedding) (m: mem) : Prop :=
forall b1 b1' delta1 b2 b2' delta2,
b1 <> b2 ->
emb b1 = Some (b1', delta1) ->
emb b2 = Some (b2', delta2) ->
b1' <> b2'
\/ fst(bounds m b1) >= snd(bounds m b1)
\/ fst(bounds m b2) >= snd(bounds m b2)
\/ snd(bounds m b1) + delta1 <= fst(bounds m b2) + delta2
\/ snd(bounds m b2) + delta2 <= fst(bounds m b1) + delta1.
Lemma store_mapped_emb:
forall emb m1 m2 b1 ofs b2 delta v1 v2 ty m1',
mem_emb emb m1 m2 ->
embedding_no_overlap emb m1 ->
val_emb emb vundef vundef ->
emb b1 = Some(b2, delta) ->
store ty m1 b1 ofs v1 = Some m1' ->
(forall ty', compat ty ty' ->
val_emb emb (convert ty' v1) (convert ty' v2)) ->
exists m2',
store ty m2 b2 (ofs + delta) v2 = Some m2' /\ mem_emb emb m1' m2'.
Proof.
intros.
assert (valid_pointer ty m1 b1 ofs).
eapply store_valid_pointer; eauto.
assert (valid_pointer ty m2 b2 (ofs + delta)).
eapply valid_pointer_emb; eauto.
destruct (valid_pointer_store _ _ _ _ v2 H6) as [m2' STORE2].
exists m2'; split. auto.
red. intros ty' b1' ofs' v b2' delta' CP LOAD1.
assert (valid_pointer ty' m1 b1' ofs').
rewrite <- (store_valid_pointer_inv _ _ _ _ _ _ ty' b1' ofs' H3).
eapply load_valid_pointer; eauto.
generalize (load_store_characterization _ _ _ _ _ _ _ _ _ H3 H7).
destruct (load_store_classification ty b1 ofs ty' b1' ofs');
intro.
subst b1' ofs'.
rewrite CP in H2. inversion H2. subst b2' delta'.
rewrite LOAD1 in H8. inversion H8. subst v.
exists (convert ty' v2). split.
eapply load_store_same; eauto.
auto.
rewrite LOAD1 in H8.
destruct (H _ _ _ _ _ _ CP (sym_equal H8)) as [v2' [LOAD2 VCP]].
exists v2'. split; auto.
rewrite <- LOAD2. eapply load_store_disjoint; eauto.
destruct (eq_block b1 b1'). subst b1'.
rewrite CP in H2; inversion H2.
right. elim o; [congruence | omega].
assert (valid_pointer ty m1 b1 ofs).
eapply store_valid_pointer; eauto.
generalize (H0 _ _ _ _ _ _ n H2 CP). intros [A | [A | [A | A]]].
left. apply sym_not_equal; auto.
destruct H9 as [B [C [D E]]].
generalize (sizeof_pos ty); intro. elimtype False. omega.
destruct H7 as [B [C [D E]]].
generalize (sizeof_pos ty'); intro. elimtype False. omega.
destruct H9 as [B [C [D E]]]. destruct H7 as [U [V [W X]]].
right. omega.
subst b1'. rewrite CP in H2; inversion H2; subst.
assert (exists v2', load ty' m2' b2 (ofs' + delta) = Some v2').
apply valid_pointer_load.
rewrite (store_valid_pointer_inv _ _ _ _ _ _ ty' b2 (ofs' + delta) STORE2).
eapply valid_pointer_emb. eexact CP. eauto.
rewrite <- (store_valid_pointer_inv _ _ _ _ _ _ ty' b1 ofs' H3).
eapply load_valid_pointer; eauto.
destruct H9 as [v2' LOAD2'].
assert (v2' = vundef). eapply load_store_overlap; eauto.
omega. omega. omega.
exists v2'; split. auto.
replace v with vundef by congruence. subst v2'. auto.
subst b1' ofs'. rewrite CP in H2; inversion H2; subst.
assert (exists v2', load ty' m2' b2 (ofs + delta) = Some v2').
apply valid_pointer_load.
rewrite (store_valid_pointer_inv _ _ _ _ _ _ ty' b2 (ofs + delta) STORE2).
eapply valid_pointer_emb. eexact CP. eauto.
rewrite <- (store_valid_pointer_inv _ _ _ _ _ _ ty' b1 ofs H3).
eapply load_valid_pointer; eauto.
destruct H9 as [v2' LOAD2'].
assert (v2' = vundef). eapply load_store_mismatch; eauto.
exists v2'; split. auto.
replace v with vundef by congruence. subst v2'. auto.
Qed.
Remark alignment_shift:
forall ty ofs delta,
(alignof ty | ofs) -> (max_alignment | delta) ->
(alignof ty | ofs + delta).
Proof.
assert (forall a b c, (a|b) -> (b|c) -> (a|c)).
intros. inv H; inv H0. exists (q0 * q); ring.
intros. apply Zdivide_plus_r. auto.
apply H with max_alignment. apply alignof_div. auto.
Qed.
Lemma alloc_parallel_emb:
forall emb m1 m2 lo1 hi1 m1' b1 lo2 hi2 m2' b2 delta,
mem_emb emb m1 m2 ->
alloc m1 lo1 hi1 = Some(b1, m1') ->
alloc m2 lo2 hi2 = Some(b2, m2') ->
emb b1 = Some(b2, delta) ->
lo2 <= lo1 + delta -> hi1 + delta <= hi2 ->
(max_alignment | delta) ->
val_emb emb vundef vundef ->
mem_emb emb m1' m2'.
Proof.
intros; red. intros ty b ofs v b' delta'. intros.
assert (valid_pointer ty m1' b ofs). eapply load_valid_pointer; eauto.
destruct H9 as [A [B [C D]]].
destruct (eq_block b1 b).
subst b.
assert (v = vundef). eapply load_alloc_same with (m := m1); eauto. subst v.
rewrite H2 in H7; inv H7.
exists vundef. split.
eapply load_alloc_same_2; eauto.
apply alignment_shift; auto.
rewrite (alloc_result_bounds _ _ _ _ _ H0) in C. simpl in C. omega.
rewrite (alloc_result_bounds _ _ _ _ _ H0) in D. simpl in D. omega.
auto.
assert (load ty m1 b ofs = Some v).
rewrite <- H8. symmetry. eapply load_alloc_other; eauto.
destruct (H _ _ _ _ _ _ H7 H9) as [v2 [LOAD2 VEMB]].
exists v2; split.
eapply load_alloc_other_2; eauto.
auto.
Qed.
Lemma alloc_right_emb:
forall emb m1 m2 lo hi b2 m2',
mem_emb emb m1 m2 ->
alloc m2 lo hi = Some(b2, m2') ->
mem_emb emb m1 m2'.
Proof.
intros; red; intros.
destruct (H _ _ _ _ _ _ H1 H2) as [v2 [LOAD2 VEMB]].
exists v2; split.
eapply load_alloc_other_2; eauto.
auto.
Qed.
Lemma alloc_left_unmapped_emb:
forall emb m1 m2 lo hi b1 m1',
mem_emb emb m1 m2 ->
alloc m1 lo hi = Some(b1, m1') ->
emb b1 = None ->
mem_emb emb m1' m2.
Proof.
intros; red; intros.
destruct (eq_block b1 b0).
subst b0. congruence.
red in H. eapply H; eauto.
rewrite <- H3. symmetry. eapply load_alloc_other; eauto.
Qed.
Lemma alloc_left_mapped_emb:
forall emb m1 m2 lo hi b1 m1' b2 delta,
mem_emb emb m1 m2 ->
alloc m1 lo hi = Some(b1, m1') ->
emb b1 = Some(b2, delta) ->
valid_block m2 b2 ->
fst(bounds m2 b2) <= lo + delta -> hi + delta <= snd(bounds m2 b2) ->
(max_alignment | delta) ->
(forall v, val_emb emb vundef v) ->
mem_emb emb m1' m2.
Proof.
intros; red; intros.
destruct (eq_block b1 b0).
subst b0. rewrite H1 in H7; inv H7.
assert (v1 = vundef). eapply load_alloc_same; eauto. subst v1.
assert (valid_pointer ty m1' b1 ofs). eapply load_valid_pointer; eauto.
destruct H7 as [A [B [C D]]].
assert (valid_pointer ty m2 b3 (ofs + delta0)).
split. auto.
split. apply alignment_shift; auto.
split. rewrite (alloc_result_bounds _ _ _ _ _ H0) in C; simpl in C. omega.
rewrite (alloc_result_bounds _ _ _ _ _ H0) in D; simpl in D. omega.
destruct (valid_pointer_load _ _ _ _ H7) as [v2 LOAD2].
exists v2; split. auto. auto.
red in H. eapply H; eauto.
rewrite <- H8. symmetry. eapply load_alloc_other; eauto.
Qed.
Lemma free_left_emb:
forall emb m1 m2 b1 m1',
mem_emb emb m1 m2 ->
free m1 b1 = Some m1' ->
mem_emb emb m1' m2.
Proof.
intros; red; intros.
destruct (eq_block b0 b1).
subst b0. elim (free_not_valid_pointer _ _ _ H0 ty ofs).
eapply load_valid_pointer; eauto.
red in H; eapply H; eauto.
rewrite <- H2. symmetry. eapply load_free_other; eauto.
Qed.
Lemma free_right_emb:
forall emb m1 m2 b2 m2',
mem_emb emb m1 m2 ->
(forall b1 delta,
emb b1 = Some(b2, delta) -> ~(valid_block m1 b1)) ->
free m2 b2 = Some m2' ->
mem_emb emb m1 m2'.
Proof.
intros; red; intros.
destruct (H _ _ _ _ _ _ H2 H3) as [v2 [LOAD2 VEMB]].
exists v2; split.
rewrite <- LOAD2. eapply load_free_other; eauto.
red; intro; subst b0.
elim (H0 b1 delta); auto.
generalize (load_valid_pointer _ _ _ _ _ H3). intro. inv H4; auto.
auto.
Qed.
Fixpoint free_list (m: mem) (bl: list block) {struct bl} : option mem :=
match bl with
| nil => Some m
| b :: bs =>
match free_list m bs with
| None => None
| Some m1 => free m1 b
end
end.
Lemma free_list_left_emb:
forall emb m2 l m1 m1',
mem_emb emb m1 m2 ->
free_list m1 l = Some m1' ->
mem_emb emb m1' m2.
Proof.
induction l; simpl.
intros; inv H0; auto.
intros m1 m1' EMB. case_eq (free_list m1 l). 2:congruence. intros.
apply free_left_emb with m a; eauto.
Qed.
Remark free_list_not_valid_block:
forall m bl m',
free_list m bl = Some m' ->
forall b, In b bl -> ~(valid_block m' b).
Proof.
induction bl; simpl.
intros. contradiction.
intro m'. case_eq (free_list m bl). 2: congruence. intros.
destruct (eq_block b a).
subst b. eapply free_not_valid_block; eauto.
rewrite (free_valid_block _ _ _ b H0 n).
eapply IHbl; eauto. intuition congruence.
Qed.
Lemma free_list_free_parallel_emb:
forall emb m1 m2 bl b2 m1' m2',
mem_emb emb m1 m2 ->
free_list m1 bl = Some m1' ->
free m2 b2 = Some m2' ->
(forall b delta', emb b = Some(b2, delta') -> In b bl) ->
mem_emb emb m1' m2'.
Proof.
intros. eapply free_right_emb; eauto.
eapply free_list_left_emb; eauto.
intros. eapply free_list_not_valid_block; eauto.
Qed.
Lemma free_parallel_emb:
forall emb m1 m2 b1 b2 m1' m2',
mem_emb emb m1 m2 ->
free m1 b1 = Some m1' ->
free m2 b2 = Some m2' ->
(forall b delta', emb b = Some(b2, delta') -> b = b1) ->
mem_emb emb m1' m2'.
Proof.
intros.
eapply free_right_emb; eauto.
eapply free_left_emb; eauto.
intros. assert (b0 = b1) by eauto. subst b0.
eapply free_not_valid_block; eauto.
Qed.
End GENERIC_EMBEDDING.
Section MEM_EXTENDS.
Definition emb_id : embedding := fun b => Some(b, 0).
Definition val_emb_id (emb: embedding) (v1 v2: val) := v1 = v2.
Definition mem_extends (m1 m2: mem) :=
same_domain m1 m2 /\ mem_emb val_emb_id emb_id m1 m2.
Lemma mem_extends_refl:
forall m, mem_extends m m.
Proof.
intros. split. red; intros; tauto.
red; intros. exists v1; split.
unfold emb_id in H. inv H. replace (ofs + 0) with ofs by omega. auto.
red; auto.
Qed.
Lemma mem_extends_trans:
forall m1 m2 m3, mem_extends m1 m2 -> mem_extends m2 m3 -> mem_extends m1 m3.
Proof.
intros. destruct H; destruct H0. split.
red; intros. rewrite (H b). apply H0.
red; intros. destruct (H1 _ _ _ _ _ _ H3 H4) as [v2 [LOAD2 VEMB2]].
generalize H3. unfold emb_id; intro EQ; inv EQ.
replace (ofs + 0) with ofs in LOAD2 by omega.
destruct (H2 _ _ _ _ _ _ H3 LOAD2) as [v3 [LOAD3 VEMB3]].
exists v3; split. auto.
red. transitivity v2. auto. auto.
Qed.
Lemma alloc_extends:
forall m1 m2 lo1 hi1 b1 m1' lo2 hi2 b2 m2',
mem_extends m1 m2 ->
alloc m1 lo1 hi1 = Some(b1, m1') ->
alloc m2 lo2 hi2 = Some(b2, m2') ->
lo2 <= lo1 -> hi1 <= hi2 ->
b1 = b2 /\ mem_extends m1' m2'.
Proof.
intros. destruct H.
assert (b1 = b2 /\ same_domain m1' m2').
eapply alloc_same_domain; eauto.
destruct H5. subst b2. split. auto. split. auto.
eapply alloc_parallel_emb; eauto.
unfold emb_id; reflexivity. omega. omega.
apply Zdivide_0.
red; auto.
Qed.
Lemma load_extends:
forall m1 m2 ty b ofs v,
mem_extends m1 m2 ->
load ty m1 b ofs = Some v ->
load ty m2 b ofs = Some v.
Proof.
intros. destruct H.
assert (emb_id b = Some(b, 0)). unfold emb_id; auto.
destruct (H1 _ _ _ _ _ _ H2 H0) as [v2 [LOAD VEMB]].
red in VEMB. replace ofs with (ofs + 0) by omega. congruence.
Qed.
Lemma store_within_extends:
forall m1 m2 ty b ofs v m1',
mem_extends m1 m2 ->
store ty m1 b ofs v = Some m1' ->
exists m2', store ty m2 b ofs v = Some m2' /\ mem_extends m1' m2'.
Proof.
intros. destruct H.
assert (exists m2', store ty m2 b (ofs + 0) v = Some m2' /\ mem_emb val_emb_id emb_id m1' m2').
eapply store_mapped_emb; eauto.
red; unfold emb_id; intros. inv H3. inv H4. auto.
red; auto.
reflexivity.
intros; red; auto.
destruct H2 as [m2' [STORE MEMB]].
replace (ofs + 0) with ofs in STORE by omega.
exists m2'; split. auto. split. eapply store_same_domain; eauto. auto.
Qed.
Lemma store_outside_extends:
forall m1 m2 ty b ofs v m2',
mem_extends m1 m2 ->
ofs + sizeof ty <= fst(bounds m1 b) \/ snd(bounds m1 b) <= ofs ->
store ty m2 b ofs v = Some m2' ->
mem_extends m1 m2'.
Proof.
intros. destruct H.
split. red; intros. rewrite (store_fresh_block _ _ _ _ _ _ b0 H1). auto.
eapply store_outside_emb; eauto.
unfold emb_id; intros. inv H3. omega.
Qed.
Lemma free_extends:
forall m1 m2 b m1' m2',
mem_extends m1 m2 ->
free m1 b = Some m1' ->
free m2 b = Some m2' ->
mem_extends m1' m2'.
Proof.
intros. destruct H. split.
eapply free_same_domain; eauto.
eapply free_parallel_emb; eauto.
unfold emb_id; intros. congruence.
Qed.
End MEM_EXTENDS.
Section MEM_LESSDEF.
Definition val_lessdef (v1 v2: val) := v1 = vundef \/ v1 = v2.
Definition val_emb_lessdef (emb: embedding) (v1 v2: val) :=
val_lessdef v1 v2.
Definition mem_lessdef (m1 m2: mem) :=
same_domain m1 m2 /\ mem_emb val_emb_lessdef emb_id m1 m2.
Lemma mem_lessdef_refl:
forall m, mem_lessdef m m.
Proof.
intros. split. red; intros; tauto.
red; intros. exists v1; split.
unfold emb_id in H. inv H. replace (ofs + 0) with ofs by omega. auto.
hnf; auto.
Qed.
Lemma mem_lessdef_trans:
forall m1 m2 m3, mem_lessdef m1 m2 -> mem_lessdef m2 m3 -> mem_lessdef m1 m3.
Proof.
intros. destruct H; destruct H0. split.
red; intros. rewrite (H b). apply H0.
red; intros. destruct (H1 _ _ _ _ _ _ H3 H4) as [v2 [LOAD2 VEMB2]].
generalize H3. unfold emb_id; intro EQ; inv EQ.
replace (ofs + 0) with ofs in LOAD2 by omega.
destruct (H2 _ _ _ _ _ _ H3 LOAD2) as [v3 [LOAD3 VEMB3]].
exists v3; split. auto.
hnf. hnf in VEMB2. hnf in VEMB3. intuition congruence.
Qed.
Lemma alloc_lessdef:
forall m1 m2 lo1 hi1 b1 m1' lo2 hi2 b2 m2',
mem_lessdef m1 m2 ->
alloc m1 lo1 hi1 = Some(b1, m1') ->
alloc m2 lo2 hi2 = Some(b2, m2') ->
lo2 <= lo1 -> hi1 <= hi2 ->
b1 = b2 /\ mem_lessdef m1' m2'.
Proof.
intros. destruct H.
assert (b1 = b2 /\ same_domain m1' m2').
eapply alloc_same_domain; eauto.
destruct H5. subst b2. split. auto. split. auto.
eapply alloc_parallel_emb; eauto.
unfold emb_id; reflexivity. omega. omega.
apply Zdivide_0.
hnf; auto.
Qed.
Lemma load_lessdef:
forall m1 m2 ty b ofs v1,
mem_lessdef m1 m2 ->
load ty m1 b ofs = Some v1 ->
exists v2, load ty m2 b ofs = Some v2 /\ val_lessdef v1 v2.
Proof.
intros. destruct H.
replace ofs with (ofs + 0) by omega.
apply (H1 ty b ofs v1); auto.
Qed.
Hypothesis convert_monotone:
forall ty v1 v2, val_lessdef v1 v2 -> val_lessdef (convert ty v1) (convert ty v2).
Lemma store_lessdef:
forall m1 m2 ty b ofs v1 m1' v2,
mem_lessdef m1 m2 ->
store ty m1 b ofs v1 = Some m1' ->
val_lessdef v1 v2 ->
exists m2', store ty m2 b ofs v2 = Some m2' /\ mem_lessdef m1' m2'.
Proof.
intros. destruct H.
assert (exists m2', store ty m2 b (ofs + 0) v2 = Some m2' /\ mem_emb val_emb_lessdef emb_id m1' m2').
eapply store_mapped_emb; eauto.
red; unfold emb_id; intros. inv H4. inv H5. auto.
red; auto.
red; auto.
reflexivity.
intros. red. apply convert_monotone; auto.
destruct H3 as [m2' [STORE MEMB]].
replace (ofs + 0) with ofs in STORE by omega.
exists m2'; split. auto. split. eapply store_same_domain; eauto. auto.
Qed.
Lemma free_lessdef:
forall m1 m2 b m1' m2',
mem_lessdef m1 m2 ->
free m1 b = Some m1' ->
free m2 b = Some m2' ->
mem_lessdef m1' m2'.
Proof.
intros. destruct H. split.
eapply free_same_domain; eauto.
eapply free_parallel_emb; eauto.
unfold emb_id; intros. congruence.
Qed.
End MEM_LESSDEF.
Section MEM_INJECT.
Variable val_inject: embedding -> val -> val -> Prop.
Record mem_inject (f: embedding) (m1 m2: mem) : Prop :=
mk_mem_inject {
mi_emb:
mem_emb val_inject f m1 m2;
mi_freeblocks:
forall b, fresh_block m1 b -> f b = None;
mi_mappedblocks:
forall b b' delta, f b = Some(b', delta) -> ~(fresh_block m2 b');
mi_no_overlap:
embedding_no_overlap f m1
}.
Lemma load_inject:
forall emb m1 m2 ty b1 ofs v1 b2 delta,
mem_inject emb m1 m2 ->
load ty m1 b1 ofs = Some v1 ->
emb b1 = Some(b2, delta) ->
exists v2, load ty m2 b2 (ofs + delta) = Some v2 /\ val_inject emb v1 v2.
Proof.
intros. destruct H. apply (mi_emb0 ty b1 ofs v1); auto.
Qed.
Hypothesis val_inject_undef:
forall emb v, val_inject emb vundef v.
Hypothesis convert_inject:
forall emb ty v1 v2,
val_inject emb v1 v2 ->
val_inject emb (convert ty v1) (convert ty v2).
Lemma store_mapped_inject:
forall emb m1 m2 ty b1 ofs v1 m1' b2 delta v2,
mem_inject emb m1 m2 ->
store ty m1 b1 ofs v1 = Some m1' ->
val_inject emb v1 v2 ->
emb b1 = Some(b2, delta) ->
exists m2', store ty m2 b2 (ofs + delta) v2 = Some m2' /\ mem_inject emb m1' m2'.
Proof.
intros. destruct H.
assert (exists m2', store ty m2 b2 (ofs + delta) v2 = Some m2' /\ mem_emb val_inject emb m1' m2').
eapply store_mapped_emb; eauto.
destruct H as [m2' [STORE MEMB]].
exists m2'; split. auto.
constructor.
auto.
intros. rewrite (store_fresh_block _ _ _ _ _ _ b H0) in H. auto.
intros. rewrite (store_fresh_block _ _ _ _ _ _ b' STORE). eauto.
red; intros.
rewrite (store_bounds_inv _ _ _ _ _ _ b0 H0).
rewrite (store_bounds_inv _ _ _ _ _ _ b3 H0).
auto.
Qed.
Lemma store_unmapped_inject:
forall emb m1 m2 ty b1 ofs v1 m1',
mem_inject emb m1 m2 ->
store ty m1 b1 ofs v1 = Some m1' ->
emb b1 = None ->
mem_inject emb m1' m2.
Proof.
intros. destruct H.
constructor.
eapply store_unmapped_emb; eauto.
intros. rewrite (store_fresh_block _ _ _ _ _ _ b H0) in H. auto.
auto.
red; intros.
rewrite (store_bounds_inv _ _ _ _ _ _ b0 H0).
rewrite (store_bounds_inv _ _ _ _ _ _ b2 H0).
auto.
Qed.
Section LOADV.
Variable proj_pointer: val -> option (block * Z).
Hypothesis val_inject_proj_pointer:
forall v1 v2 b1 ofs1 emb,
proj_pointer v1 = Some(b1, ofs1) ->
val_inject emb v1 v2 ->
exists b2, exists ofs2, exists delta,
proj_pointer v2 = Some(b2, ofs2) /\
emb b1 = Some(b2, delta) /\
ofs2 = ofs1 + delta.
Lemma loadv_inject:
forall ty m1 addr1 v1 emb addr2 m2,
loadv proj_pointer ty m1 addr1 = Some v1 ->
val_inject emb addr1 addr2 ->
mem_inject emb m1 m2 ->
exists v2, loadv proj_pointer ty m2 addr2 = Some v2 /\ val_inject emb v1 v2.
Proof.
intros until m2. unfold loadv. case_eq (proj_pointer addr1). 2: congruence.
intros [b1 ofs1]. intros.
destruct (val_inject_proj_pointer _ _ _ _ _ H H1) as [b2 [ofs2 [delta [A [B C]]]]].
rewrite A. rewrite C. eapply load_inject; eauto.
Qed.
Lemma storev_inject:
forall ty m1 addr1 v1 m1' emb addr2 v2 m2,
storev proj_pointer ty m1 addr1 v1 = Some m1' ->
val_inject emb addr1 addr2 ->
val_inject emb v1 v2 ->
mem_inject emb m1 m2 ->
exists m2', storev proj_pointer ty m2 addr2 v2 = Some m2' /\ mem_inject emb m1' m2'.
Proof.
intros until m2. unfold storev. case_eq (proj_pointer addr1). 2: congruence.
intros [b1 ofs1]. intros.
destruct (val_inject_proj_pointer _ _ _ _ _ H H1) as [b2 [ofs2 [delta [A [B C]]]]].
rewrite A. rewrite C. eapply store_mapped_inject; eauto.
Qed.
End LOADV.
Lemma embedding_no_overlap_free:
forall emb m b m',
free m b = Some m' ->
embedding_no_overlap emb m ->
embedding_no_overlap emb m'.
Proof.
intros; red; intros.
assert (fst (bounds m' b) >= snd (bounds m' b)).
rewrite (free_same_bounds _ _ _ H). omega.
destruct (eq_block b1 b); destruct (eq_block b2 b); subst; auto.
rewrite (free_bounds_inv _ _ _ _ H n).
rewrite (free_bounds_inv _ _ _ _ H n0).
auto.
Qed.
Lemma embedding_no_overlap_free_list:
forall emb m bl m',
free_list m bl = Some m' ->
embedding_no_overlap emb m ->
embedding_no_overlap emb m'.
Proof.
induction bl; simpl; intros.
inv H; auto.
generalize H; clear H. case_eq (free_list m bl).
intros m1 F1 F2. eapply embedding_no_overlap_free; eauto.
congruence.
Qed.
Remark free_list_fresh_block:
forall m l m' b,
free_list m l = Some m' ->
(fresh_block m' b <-> fresh_block m b).
Proof.
induction l; simpl.
intros. inv H. tauto.
case_eq (free_list m l); intros. 2: congruence.
rewrite (free_fresh_block _ _ _ b H0).
eapply IHl; eauto.
Qed.
Lemma free_inject:
forall emb m1 m2 l b m1' m2',
(forall b1 delta, emb b1 = Some(b, delta) -> In b1 l) ->
free_list m1 l = Some m1' ->
free m2 b = Some m2' ->
mem_inject emb m1 m2 ->
mem_inject emb m1' m2'.
Proof.
intros. inv H2. constructor.
eapply free_list_free_parallel_emb; eauto.
intros. apply mi_freeblocks0.
rewrite <- (free_list_fresh_block _ _ _ b0 H0). auto.
intros. rewrite (free_fresh_block _ _ _ b' H1). eauto.
eapply embedding_no_overlap_free_list; eauto.
Qed.
Definition embedding_incr (emb1 emb2: embedding) : Prop :=
forall b, emb2 b = emb1 b \/ emb1 b = None.
Hypothesis val_inject_incr:
forall emb1 emb2 v1 v2,
embedding_incr emb1 emb2 ->
val_inject emb1 v1 v2 ->
val_inject emb2 v1 v2.
Definition extend_embedding (b: block) (x: option (block * Z))
(emb: embedding): embedding :=
fun (b': block) => if eq_block b' b then x else emb b'.
Lemma extend_embedding_incr:
forall emb b x,
emb b = None -> embedding_incr emb (extend_embedding b x emb).
Proof.
intros; red; intros. unfold extend_embedding.
destruct (eq_block b0 b). subst b0; auto. auto.
Qed.
Lemma alloc_right_inject:
forall emb m1 m2 lo hi b2 m2',
mem_inject emb m1 m2 ->
alloc m2 lo hi = Some(b2, m2') ->
mem_inject emb m1 m2'.
Proof.
intros. inv H. constructor.
eapply alloc_right_emb; eauto.
auto.
intros. rewrite (alloc_fresh_block _ _ _ _ _ b' H0).
generalize (mi_mappedblocks0 _ _ _ H). tauto.
auto.
Qed.
Lemma alloc_left_unmapped_inject:
forall emb m1 m2 lo hi b1 m1',
mem_inject emb m1 m2 ->
alloc m1 lo hi = Some(b1, m1') ->
mem_inject (extend_embedding b1 None emb) m1' m2
/\ embedding_incr emb (extend_embedding b1 None emb).
Proof.
intros. inv H.
assert (INCR: embedding_incr emb (extend_embedding b1 None emb)).
red. intro. unfold extend_embedding. destruct (eq_block b b1).
subst b1. right. apply mi_freeblocks0.
eapply alloc_fresh_block_2; eauto.
auto.
split; auto. constructor.
eapply alloc_left_unmapped_emb; eauto.
red; intros. unfold extend_embedding in H.
destruct (eq_block b0 b1). discriminate.
destruct (mi_emb0 _ _ _ _ _ _ H H1) as [v2 [A B]].
exists v2; split. auto. eapply val_inject_incr; eauto.
unfold extend_embedding. destruct (eq_block b1 b1); congruence.
intros. unfold extend_embedding. destruct (eq_block b b1). auto.
apply mi_freeblocks0.
generalize (alloc_fresh_block _ _ _ _ _ b H0). tauto.
unfold extend_embedding. intros. destruct (eq_block b b1).
discriminate. eauto.
unfold extend_embedding; red; intros.
destruct (eq_block b0 b1). discriminate.
destruct (eq_block b2 b1). discriminate.
rewrite (alloc_bounds_inv _ _ _ _ _ _ H0 n).
rewrite (alloc_bounds_inv _ _ _ _ _ _ H0 n0).
apply mi_no_overlap0; auto.
Qed.
Lemma alloc_left_mapped_inject:
forall emb m1 m2 lo hi b1 m1' b2 ofs,
mem_inject emb m1 m2 ->
alloc m1 lo hi = Some(b1, m1') ->
valid_block m2 b2 ->
fst (bounds m2 b2) <= lo + ofs ->
hi + ofs <= snd(bounds m2 b2) ->
(max_alignment | ofs) ->
(forall b' ofs',
emb b' = Some(b2, ofs') ->
snd (bounds m1 b') + ofs' <= lo + ofs \/
hi + ofs <= fst (bounds m1 b') + ofs') ->
mem_inject (extend_embedding b1 (Some(b2, ofs)) emb) m1' m2
/\ embedding_incr emb (extend_embedding b1 (Some(b2, ofs)) emb).
Proof.
intros. inv H.
assert (INCR: embedding_incr emb (extend_embedding b1 (Some(b2, ofs)) emb)).
red. intro. unfold extend_embedding. destruct (eq_block b b1).
subst b1. right. apply mi_freeblocks0. eapply alloc_fresh_block_2; eauto.
auto.
split; auto. constructor.
eapply alloc_left_mapped_emb; eauto.
red; intros. unfold extend_embedding in H.
destruct (eq_block b0 b1). subst b0.
destruct (load_valid_pointer _ _ _ _ _ H6) as [A [B [C D]]].
elim (alloc_not_valid_block _ _ _ _ _ H0 A).
destruct (mi_emb0 _ _ _ _ _ _ H H6) as [v2 [A B]].
exists v2; split. auto. eapply val_inject_incr; eauto.
unfold extend_embedding. destruct (eq_block b1 b1); congruence.
intros. unfold extend_embedding. destruct (eq_block b b1).
subst b. rewrite (alloc_fresh_block _ _ _ _ _ b1 H0) in H.
intuition congruence.
apply mi_freeblocks0.
generalize (alloc_fresh_block _ _ _ _ _ b H0). tauto.
unfold extend_embedding. intros. destruct (eq_block b b1).
inv H. red; intro. eapply fresh_valid_block_exclusive; eauto.
eauto.
unfold extend_embedding; red; intros.
assert (forall b, bounds m1' b = if eq_block b b1 then (lo, hi) else bounds m1 b).
intros. destruct (eq_block b b1).
subst b. eapply alloc_result_bounds; eauto.
eapply alloc_bounds_inv; eauto.
repeat rewrite H8. clear H8.
destruct (eq_block b0 b1); destruct (eq_block b3 b1); simpl.
subst b0 b3. congruence.
subst b0. injection H6; clear H6; intros; subst b1' delta1.
destruct (eq_block b2 b2').
right. subst b2'. generalize (H5 _ _ H7). omega.
left. auto.
subst b3. injection H7; clear H7; intros; subst b2' delta2.
destruct (eq_block b1' b2).
right. subst b1'. generalize (H5 _ _ H6). omega.
left. auto.
eapply mi_no_overlap0; eauto.
Qed.
Fixpoint alloc_list (m: mem) (req: list (Z * Z)) {struct req} : option (list block * mem) :=
match req with
| nil => Some(nil, m)
| (lo, hi) :: req' =>
match alloc m lo hi with
| None => None
| Some(b1, m1) =>
match alloc_list m1 req' with
| None => None
| Some(bl, m2) => Some(b1 :: bl, m2)
end
end
end.
Inductive list_forall2 (A B: Set) (P: A -> B -> Prop): list A -> list B -> Prop :=
| list_forall2_nil:
list_forall2 A B P nil nil
| list_forall2_cons: forall hd1 tl1 hd2 tl2,
P hd1 hd2 -> list_forall2 A B P tl1 tl2 ->
list_forall2 A B P (hd1 :: tl1) (hd2 :: tl2).
Implicit Arguments list_forall2 [A B].
Inductive disjoint_req (lo hi: Z): list (Z*Z) -> list(option Z) -> Prop :=
| disjoint_req_nil:
disjoint_req lo hi nil nil
| disjoint_req_cons: forall lo' hi' optdelta req map,
match optdelta with
| None => True
| Some delta => hi' + delta <= lo \/ hi <= lo' + delta
end ->
disjoint_req lo hi req map ->
disjoint_req lo hi ((lo', hi') :: req) (optdelta :: map).
Inductive wf_req (lob hib: Z): list (Z*Z) -> list(option Z) -> Prop :=
| wf_req_nil:
wf_req lob hib nil nil
| wf_req_cons: forall lo hi optdelta req map,
match optdelta with
| None => True
| Some delta =>
lob <= lo + delta /\ hi + delta <= hib /\
(max_alignment | delta) /\
disjoint_req (lo + delta) (hi + delta) req map
end ->
wf_req lob hib req map ->
wf_req lob hib ((lo, hi) :: req) (optdelta :: map).
Lemma alloc_list_left_inject:
forall m2 b2, valid_block m2 b2 ->
forall req map, wf_req (fst (bounds m2 b2)) (snd (bounds m2 b2)) req map ->
forall emb m1 bl m1',
mem_inject emb m1 m2 ->
alloc_list m1 req = Some(bl, m1') ->
(forall b' ofs',
emb b' = Some(b2, ofs') ->
disjoint_req (fst(bounds m1 b') + ofs') (snd(bounds m1 b') + ofs') req map) ->
exists emb',
mem_inject emb' m1' m2
/\ list_forall2
(fun (mp: option Z) (b: block) =>
emb' b = match mp with None => None | Some ofs => Some(b2, ofs) end)
map bl
/\ (forall b, ~fresh_block m1 b -> emb' b = emb b).
Proof.
intros m2 b2 VB2. induction 1; intros until m1'; simpl.
intros MINJ ALLOC DISJ. inversion ALLOC; clear ALLOC; subst bl m1'.
exists emb; split. auto. split. constructor. auto.
case_eq (alloc m1 lo hi). 2:congruence. intros [b1 m] ALLOC MINJ.
case_eq (alloc_list m req). 2:congruence. intros [bl1 m1''] ALLOCLIST EQ DISJ.
inversion EQ; clear EQ; subst bl m1''.
pose (img := match optdelta with None => None | Some delta => Some(b2, delta) end).
pose (emb' := extend_embedding b1 img emb).
assert (mem_inject emb' m m2 /\ embedding_incr emb emb').
unfold emb', img. destruct optdelta as [delta | ].
eapply alloc_left_mapped_inject; eauto. tauto. tauto. tauto.
intros. generalize (DISJ _ _ H1); intro. inv H2. tauto.
eapply alloc_left_unmapped_inject; eauto.
destruct H1 as [MINJ' INCR].
assert (DISJ': forall b' ofs', emb' b' = Some(b2, ofs') ->
disjoint_req (fst (bounds m b') + ofs') (snd (bounds m b') + ofs') req map).
intros until ofs'. unfold emb', extend_embedding. destruct (eq_block b' b1).
unfold img. destruct optdelta as [delta|]; intro EQ; simplify_eq EQ; clear EQ.
intro; subst ofs' b'.
rewrite (alloc_result_bounds _ _ _ _ _ ALLOC). simpl. tauto.
intros. rewrite (alloc_bounds_inv _ _ _ _ _ _ ALLOC n).
generalize (DISJ _ _ H1); intro. inv H2; auto.
destruct (IHwf_req _ _ _ _ MINJ' ALLOCLIST DISJ') as [emb'' [A [B C]]].
exists emb''; split. auto.
split. constructor; auto. rewrite C. unfold emb', extend_embedding.
destruct (eq_block b1 b1). 2: congruence. reflexivity.
red; intro. eapply fresh_valid_block_exclusive. eauto.
rewrite (alloc_valid_block _ _ _ _ _ b1 ALLOC). auto.
intros. rewrite C. unfold emb', extend_embedding.
destruct (eq_block b b1). subst b.
elim H1. eapply alloc_fresh_block_2; eauto. auto.
rewrite (alloc_fresh_block _ _ _ _ _ b ALLOC). tauto.
Qed.
Lemma alloc_list_alloc_inject:
forall req map emb m1 m2 bl m1' b2 m2' lo hi,
mem_inject emb m1 m2 ->
alloc_list m1 req = Some(bl, m1') ->
alloc m2 lo hi = Some(b2, m2') ->
wf_req lo hi req map ->
exists emb',
mem_inject emb' m1' m2'
/\ list_forall2
(fun (rq: option Z) (b: block) =>
emb' b = match rq with None => None | Some delta => Some(b2, delta) end)
map bl
/\ embedding_incr emb emb'.
Proof.
intros.
assert (VALB: valid_block m2' b2).
rewrite (alloc_valid_block _ _ _ _ _ b2 H1). auto.
assert (MINJ: mem_inject emb m1 m2').
eapply alloc_right_inject; eauto.
assert (DISJ: forall b' ofs', emb b' = Some(b2, ofs') ->
disjoint_req (fst (bounds m1 b') + ofs') (snd (bounds m1 b') + ofs') req map).
intros. inversion H. elim (mi_mappedblocks0 _ _ _ H3).
eapply alloc_fresh_block_2; eauto.
assert (WFREQ: wf_req (fst (bounds m2' b2)) (snd (bounds m2' b2)) req map).
rewrite (alloc_result_bounds _ _ _ _ _ H1). simpl; auto.
destruct (alloc_list_left_inject _ _ VALB _ _ WFREQ _ _ _ _ MINJ H0 DISJ)
as [emb' [A [B C]]].
exists emb'; split. auto. split. auto.
red; intros. inv H. case_eq (emb b); intros.
left. rewrite <- H. apply C. red; intro. generalize (mi_freeblocks0 _ H3); intro. congruence.
right. auto.
Qed.
End MEM_INJECT.
End Rel_Mem.