This file develops the memory model that is used in the dynamic
semantics of all the languages used in the compiler.
It defines a type
mem of memory states, the following 4 basic
operations over memory states, and their properties:
-
load: read a memory chunk at a given address;
-
store: store a memory chunk at a given address;
-
alloc: allocate a fresh memory block;
-
free: invalidate a memory block.
.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Export Memdata.
Require Export Memtype.
Local Notation "
a #
b" := (
ZMap.get b a) (
at level 1).
Module Mem <:
MEM.
Definition perm_order' (
po:
option permission) (
p:
permission) :=
match po with
|
Some p' =>
perm_order p'
p
|
None =>
False
end.
Definition perm_order'' (
po1 po2:
option permission) :=
match po1,
po2 with
|
Some p1,
Some p2 =>
perm_order p1 p2
|
_,
None =>
True
|
None,
Some _ =>
False
end.
Record mem' :
Type :=
mkmem {
mem_contents:
ZMap.t (
ZMap.t memval);
(* block -> offset -> memval *)
mem_access:
ZMap.t (
Z ->
perm_kind ->
option permission);
nextblock:
block;
nextblock_pos:
nextblock > 0;
access_max:
forall b ofs,
perm_order'' (
mem_access#
b ofs Max) (
mem_access#
b ofs Cur);
nextblock_noaccess:
forall b ofs k,
b <= 0 \/
b >=
nextblock ->
mem_access#
b ofs k =
None
}.
Definition mem :=
mem'.
Lemma mkmem_ext:
forall cont1 cont2 acc1 acc2 next1 next2 a1 a2 b1 b2 c1 c2,
cont1=
cont2 ->
acc1=
acc2 ->
next1=
next2 ->
mkmem cont1 acc1 next1 a1 b1 c1 =
mkmem cont2 acc2 next2 a2 b2 c2.
Proof.
intros.
subst.
f_equal;
apply proof_irr.
Qed.
Validity of blocks and accesses
A block address is valid if it was previously allocated. It remains valid
even after being freed.
Definition valid_block (
m:
mem) (
b:
block) :=
b <
nextblock m.
Theorem valid_not_valid_diff:
forall m b b',
valid_block m b -> ~(
valid_block m b') ->
b <>
b'.
Proof.
intros; red; intros. subst b'. contradiction.
Qed.
Hint Local Resolve valid_not_valid_diff:
mem.
Permissions
Definition perm (
m:
mem) (
b:
block) (
ofs:
Z) (
k:
perm_kind) (
p:
permission) :
Prop :=
perm_order' (
m.(
mem_access)#
b ofs k)
p.
Theorem perm_implies:
forall m b ofs k p1 p2,
perm m b ofs k p1 ->
perm_order p1 p2 ->
perm m b ofs k p2.
Proof.
Hint Local Resolve perm_implies:
mem.
Theorem perm_cur_max:
forall m b ofs p,
perm m b ofs Cur p ->
perm m b ofs Max p.
Proof.
assert (
forall po1 po2 p,
perm_order'
po2 p ->
perm_order''
po1 po2 ->
perm_order'
po1 p).
unfold perm_order',
perm_order''.
intros.
destruct po2;
try contradiction.
destruct po1;
try contradiction.
eapply perm_order_trans;
eauto.
unfold perm;
intros.
generalize (
access_max m b ofs).
eauto.
Qed.
Theorem perm_cur:
forall m b ofs k p,
perm m b ofs Cur p ->
perm m b ofs k p.
Proof.
Theorem perm_max:
forall m b ofs k p,
perm m b ofs k p ->
perm m b ofs Max p.
Proof.
Hint Local Resolve perm_cur perm_max:
mem.
Theorem perm_valid_block:
forall m b ofs k p,
perm m b ofs k p ->
valid_block m b.
Proof.
Hint Local Resolve perm_valid_block:
mem.
Remark perm_order_dec:
forall p1 p2, {
perm_order p1 p2} + {~
perm_order p1 p2}.
Proof.
intros. destruct p1; destruct p2; (left; constructor) || (right; intro PO; inversion PO).
Qed.
Remark perm_order'
_dec:
forall op p, {
perm_order'
op p} + {~
perm_order'
op p}.
Proof.
intros.
destruct op;
unfold perm_order'.
apply perm_order_dec.
right;
tauto.
Qed.
Theorem perm_dec:
forall m b ofs k p, {
perm m b ofs k p} + {~
perm m b ofs k p}.
Proof.
unfold perm; intros.
apply perm_order'_dec.
Qed.
Definition range_perm (
m:
mem) (
b:
block) (
lo hi:
Z) (
k:
perm_kind) (
p:
permission) :
Prop :=
forall ofs,
lo <=
ofs <
hi ->
perm m b ofs k p.
Theorem range_perm_implies:
forall m b lo hi k p1 p2,
range_perm m b lo hi k p1 ->
perm_order p1 p2 ->
range_perm m b lo hi k p2.
Proof.
unfold range_perm; intros; eauto with mem.
Qed.
Theorem range_perm_cur:
forall m b lo hi k p,
range_perm m b lo hi Cur p ->
range_perm m b lo hi k p.
Proof.
unfold range_perm; intros; eauto with mem.
Qed.
Theorem range_perm_max:
forall m b lo hi k p,
range_perm m b lo hi k p ->
range_perm m b lo hi Max p.
Proof.
unfold range_perm; intros; eauto with mem.
Qed.
Hint Local Resolve range_perm_implies range_perm_cur range_perm_max:
mem.
Lemma range_perm_dec:
forall m b lo hi k p, {
range_perm m b lo hi k p} + {~
range_perm m b lo hi k p}.
Proof.
intros.
assert (
forall n, 0 <=
n ->
{
range_perm m b lo (
lo +
n)
k p} + {~
range_perm m b lo (
lo +
n)
k p}).
apply natlike_rec2.
left.
red;
intros.
omegaContradiction.
intros.
destruct H0.
destruct (
perm_dec m b (
lo +
z)
k p).
left.
red;
intros.
destruct (
zeq ofs (
lo +
z)).
congruence.
apply r.
omega.
right;
red;
intro.
elim n.
apply H0.
omega.
right;
red;
intro.
elim n.
red;
intros.
apply H0.
omega.
destruct (
zlt lo hi).
replace hi with (
lo + (
hi -
lo))
by omega.
apply H.
omega.
left;
red;
intros.
omegaContradiction.
Qed.
valid_access m chunk b ofs p holds if a memory access
of the given chunk is possible in
m at address
b, ofs
with current permissions
p.
This means:
-
The range of bytes accessed all have current permission p.
-
The offset ofs is aligned.
Definition valid_access (
m:
mem) (
chunk:
memory_chunk) (
b:
block) (
ofs:
Z) (
p:
permission):
Prop :=
range_perm m b ofs (
ofs +
size_chunk chunk)
Cur p
/\ (
align_chunk chunk |
ofs).
Theorem valid_access_implies:
forall m chunk b ofs p1 p2,
valid_access m chunk b ofs p1 ->
perm_order p1 p2 ->
valid_access m chunk b ofs p2.
Proof.
intros. inv H. constructor; eauto with mem.
Qed.
Theorem valid_access_freeable_any:
forall m chunk b ofs p,
valid_access m chunk b ofs Freeable ->
valid_access m chunk b ofs p.
Proof.
Hint Local Resolve valid_access_implies:
mem.
Theorem valid_access_valid_block:
forall m chunk b ofs,
valid_access m chunk b ofs Nonempty ->
valid_block m b.
Proof.
Hint Local Resolve valid_access_valid_block:
mem.
Lemma valid_access_perm:
forall m chunk b ofs k p,
valid_access m chunk b ofs p ->
perm m b ofs k p.
Proof.
Lemma valid_access_compat:
forall m chunk1 chunk2 b ofs p,
size_chunk chunk1 =
size_chunk chunk2 ->
valid_access m chunk1 b ofs p->
valid_access m chunk2 b ofs p.
Proof.
intros.
inv H0.
rewrite H in H1.
constructor;
auto.
rewrite <- (
align_chunk_compat _ _ H).
auto.
Qed.
Lemma valid_access_dec:
forall m chunk b ofs p,
{
valid_access m chunk b ofs p} + {~
valid_access m chunk b ofs p}.
Proof.
valid_pointer is a boolean-valued function that says whether
the byte at the given location is nonempty.
Definition valid_pointer (
m:
mem) (
b:
block) (
ofs:
Z):
bool :=
perm_dec m b ofs Cur Nonempty.
Theorem valid_pointer_nonempty_perm:
forall m b ofs,
valid_pointer m b ofs =
true <->
perm m b ofs Cur Nonempty.
Proof.
intros.
unfold valid_pointer.
destruct (
perm_dec m b ofs Cur Nonempty);
simpl;
intuition congruence.
Qed.
Theorem valid_pointer_valid_access:
forall m b ofs,
valid_pointer m b ofs =
true <->
valid_access m Mint8unsigned b ofs Nonempty.
Proof.
intros.
rewrite valid_pointer_nonempty_perm.
split;
intros.
split.
simpl;
red;
intros.
replace ofs0 with ofs by omega.
auto.
simpl.
apply Zone_divide.
destruct H.
apply H.
simpl.
omega.
Qed.
Operations over memory stores
The initial store
Program Definition empty:
mem :=
mkmem (
ZMap.init (
ZMap.init Undef))
(
ZMap.init (
fun ofs k =>
None))
1
_ _ _.
Next Obligation.
omega.
Qed.
Next Obligation.
repeat rewrite ZMap.gi.
red;
auto.
Qed.
Next Obligation.
Definition nullptr:
block := 0.
Allocation of a fresh block with the given bounds. Return an updated
memory state and the address of the fresh block, which initially contains
undefined cells. Note that allocation never fails: we model an
infinite memory.
Program Definition alloc (
m:
mem) (
lo hi:
Z) :=
(
mkmem (
ZMap.set m.(
nextblock)
(
ZMap.init Undef)
m.(
mem_contents))
(
ZMap.set m.(
nextblock)
(
fun ofs k =>
if zle lo ofs &&
zlt ofs hi then Some Freeable else None)
m.(
mem_access))
(
Zsucc m.(
nextblock))
_ _ _,
m.(
nextblock)).
Next Obligation.
Next Obligation.
Next Obligation.
Freeing a block between the given bounds.
Return the updated memory state where the given range of the given block
has been invalidated: future reads and writes to this
range will fail. Requires freeable permission on the given range.
Program Definition unchecked_free (
m:
mem) (
b:
block) (
lo hi:
Z):
mem :=
mkmem m.(
mem_contents)
(
ZMap.set b
(
fun ofs k =>
if zle lo ofs &&
zlt ofs hi then None else m.(
mem_access)#
b ofs k)
m.(
mem_access))
m.(
nextblock)
_ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
Definition free (
m:
mem) (
b:
block) (
lo hi:
Z):
option mem :=
if range_perm_dec m b lo hi Cur Freeable
then Some(
unchecked_free m b lo hi)
else None.
Fixpoint free_list (
m:
mem) (
l:
list (
block *
Z *
Z)) {
struct l}:
option mem :=
match l with
|
nil =>
Some m
| (
b,
lo,
hi) ::
l' =>
match free m b lo hi with
|
None =>
None
|
Some m' =>
free_list m'
l'
end
end.
Memory reads.
Reading N adjacent bytes in a block content.
Fixpoint getN (
n:
nat) (
p:
Z) (
c:
ZMap.t memval) {
struct n}:
list memval :=
match n with
|
O =>
nil
|
S n' =>
c#
p ::
getN n' (
p + 1)
c
end.
load chunk m b ofs perform a read in memory state m, at address
b and offset ofs. It returns the value of the memory chunk
at that address. None is returned if the accessed bytes
are not readable.
Definition load (
chunk:
memory_chunk) (
m:
mem) (
b:
block) (
ofs:
Z):
option val :=
if valid_access_dec m chunk b ofs Readable
then Some(
decode_val chunk (
getN (
size_chunk_nat chunk)
ofs (
m.(
mem_contents)#
b)))
else None.
loadv chunk m addr is similar, but the address and offset are given
as a single value addr, which must be a pointer value.
Definition loadv (
chunk:
memory_chunk) (
m:
mem) (
addr:
val) :
option val :=
match addr with
|
Vptr b ofs =>
load chunk m b (
Int.unsigned ofs)
|
_ =>
None
end.
loadbytes m b ofs n reads n consecutive bytes starting at
location (b, ofs). Returns None if the accessed locations are
not readable.
Definition loadbytes (
m:
mem) (
b:
block) (
ofs n:
Z):
option (
list memval) :=
if range_perm_dec m b ofs (
ofs +
n)
Cur Readable
then Some (
getN (
nat_of_Z n)
ofs (
m.(
mem_contents)#
b))
else None.
Memory stores.
Writing N adjacent bytes in a block content.
Fixpoint setN (
vl:
list memval) (
p:
Z) (
c:
ZMap.t memval) {
struct vl}:
ZMap.t memval :=
match vl with
|
nil =>
c
|
v ::
vl' =>
setN vl' (
p + 1) (
ZMap.set p v c)
end.
Remark setN_other:
forall vl c p q,
(
forall r,
p <=
r <
p +
Z_of_nat (
length vl) ->
r <>
q) ->
(
setN vl p c)#
q =
c#
q.
Proof.
induction vl;
intros;
simpl.
auto.
simpl length in H.
rewrite inj_S in H.
transitivity ((
ZMap.set p a c)#
q).
apply IHvl.
intros.
apply H.
omega.
apply ZMap.gso.
apply not_eq_sym.
apply H.
omega.
Qed.
Remark setN_outside:
forall vl c p q,
q <
p \/
q >=
p +
Z_of_nat (
length vl) ->
(
setN vl p c)#
q =
c#
q.
Proof.
Remark getN_setN_same:
forall vl p c,
getN (
length vl)
p (
setN vl p c) =
vl.
Proof.
induction vl;
intros;
simpl.
auto.
decEq.
rewrite setN_outside.
apply ZMap.gss.
omega.
apply IHvl.
Qed.
Remark getN_exten:
forall c1 c2 n p,
(
forall i,
p <=
i <
p +
Z_of_nat n ->
c1#
i =
c2#
i) ->
getN n p c1 =
getN n p c2.
Proof.
induction n;
intros.
auto.
rewrite inj_S in H.
simpl.
decEq.
apply H.
omega.
apply IHn.
intros.
apply H.
omega.
Qed.
Remark getN_setN_outside:
forall vl q c n p,
p +
Z_of_nat n <=
q \/
q +
Z_of_nat (
length vl) <=
p ->
getN n p (
setN vl q c) =
getN n p c.
Proof.
store chunk m b ofs v perform a write in memory state m.
Value v is stored at address b and offset ofs.
Return the updated memory store, or None if the accessed bytes
are not writable.
Definition store (
chunk:
memory_chunk) (
m:
mem) (
b:
block) (
ofs:
Z) (
v:
val):
option mem :=
if valid_access_dec m chunk b ofs Writable then
Some (
mkmem (
ZMap.set b
(
setN (
encode_val chunk v)
ofs (
m.(
mem_contents)#
b))
m.(
mem_contents))
m.(
mem_access)
m.(
nextblock)
m.(
nextblock_pos)
m.(
access_max)
m.(
nextblock_noaccess))
else
None.
storev chunk m addr v is similar, but the address and offset are given
as a single value addr, which must be a pointer value.
Definition storev (
chunk:
memory_chunk) (
m:
mem) (
addr v:
val) :
option mem :=
match addr with
|
Vptr b ofs =>
store chunk m b (
Int.unsigned ofs)
v
|
_ =>
None
end.
storebytes m b ofs bytes stores the given list of bytes bytes
starting at location (b, ofs). Returns updated memory state
or None if the accessed locations are not writable.
Definition storebytes (
m:
mem) (
b:
block) (
ofs:
Z) (
bytes:
list memval) :
option mem :=
if range_perm_dec m b ofs (
ofs +
Z_of_nat (
length bytes))
Cur Writable then
Some (
mkmem
(
ZMap.set b (
setN bytes ofs (
m.(
mem_contents)#
b))
m.(
mem_contents))
m.(
mem_access)
m.(
nextblock)
m.(
nextblock_pos)
m.(
access_max)
m.(
nextblock_noaccess))
else
None.
drop_perm m b lo hi p sets the max permissions of the byte range
(b, lo) ... (b, hi - 1) to p. These bytes must have current permissions
Freeable in the initial memory state m.
Returns updated memory state, or None if insufficient permissions.
Program Definition drop_perm (
m:
mem) (
b:
block) (
lo hi:
Z) (
p:
permission):
option mem :=
if range_perm_dec m b lo hi Cur Freeable then
Some (
mkmem m.(
mem_contents)
(
ZMap.set b
(
fun ofs k =>
if zle lo ofs &&
zlt ofs hi then Some p else m.(
mem_access)#
b ofs k)
m.(
mem_access))
m.(
nextblock)
_ _ _)
else None.
Next Obligation.
Next Obligation.
Next Obligation.
Properties of the memory operations
Properties of the empty store.
Theorem nextblock_empty:
nextblock empty = 1.
Proof.
reflexivity. Qed.
Theorem perm_empty:
forall b ofs k p, ~
perm empty b ofs k p.
Proof.
intros.
unfold perm,
empty;
simpl.
rewrite ZMap.gi.
simpl.
tauto.
Qed.
Theorem valid_access_empty:
forall chunk b ofs p, ~
valid_access empty chunk b ofs p.
Proof.
Properties related to load
Theorem valid_access_load:
forall m chunk b ofs,
valid_access m chunk b ofs Readable ->
exists v,
load chunk m b ofs =
Some v.
Proof.
intros.
econstructor.
unfold load.
rewrite pred_dec_true;
eauto.
Qed.
Theorem load_valid_access:
forall m chunk b ofs v,
load chunk m b ofs =
Some v ->
valid_access m chunk b ofs Readable.
Proof.
Lemma load_result:
forall chunk m b ofs v,
load chunk m b ofs =
Some v ->
v =
decode_val chunk (
getN (
size_chunk_nat chunk)
ofs (
m.(
mem_contents)#
b)).
Proof.
Hint Local Resolve load_valid_access valid_access_load:
mem.
Theorem load_type:
forall m chunk b ofs v,
load chunk m b ofs =
Some v ->
Val.has_type v (
type_of_chunk chunk).
Proof.
Theorem load_cast:
forall m chunk b ofs v,
load chunk m b ofs =
Some v ->
match chunk with
|
Mint8signed =>
v =
Val.sign_ext 8
v
|
Mint8unsigned =>
v =
Val.zero_ext 8
v
|
Mint16signed =>
v =
Val.sign_ext 16
v
|
Mint16unsigned =>
v =
Val.zero_ext 16
v
|
Mfloat32 =>
v =
Val.singleoffloat v
|
_ =>
True
end.
Proof.
Theorem load_int8_signed_unsigned:
forall m b ofs,
load Mint8signed m b ofs =
option_map (
Val.sign_ext 8) (
load Mint8unsigned m b ofs).
Proof.
Theorem load_int16_signed_unsigned:
forall m b ofs,
load Mint16signed m b ofs =
option_map (
Val.sign_ext 16) (
load Mint16unsigned m b ofs).
Proof.
Properties related to loadbytes
Theorem range_perm_loadbytes:
forall m b ofs len,
range_perm m b ofs (
ofs +
len)
Cur Readable ->
exists bytes,
loadbytes m b ofs len =
Some bytes.
Proof.
intros.
econstructor.
unfold loadbytes.
rewrite pred_dec_true;
eauto.
Qed.
Theorem loadbytes_range_perm:
forall m b ofs len bytes,
loadbytes m b ofs len =
Some bytes ->
range_perm m b ofs (
ofs +
len)
Cur Readable.
Proof.
Theorem loadbytes_load:
forall chunk m b ofs bytes,
loadbytes m b ofs (
size_chunk chunk) =
Some bytes ->
(
align_chunk chunk |
ofs) ->
load chunk m b ofs =
Some(
decode_val chunk bytes).
Proof.
Theorem load_loadbytes:
forall chunk m b ofs v,
load chunk m b ofs =
Some v ->
exists bytes,
loadbytes m b ofs (
size_chunk chunk) =
Some bytes
/\
v =
decode_val chunk bytes.
Proof.
Lemma getN_length:
forall c n p,
length (
getN n p c) =
n.
Proof.
induction n; simpl; intros. auto. decEq; auto.
Qed.
Theorem loadbytes_length:
forall m b ofs n bytes,
loadbytes m b ofs n =
Some bytes ->
length bytes =
nat_of_Z n.
Proof.
Theorem loadbytes_empty:
forall m b ofs n,
n <= 0 ->
loadbytes m b ofs n =
Some nil.
Proof.
Lemma getN_concat:
forall c n1 n2 p,
getN (
n1 +
n2)%
nat p c =
getN n1 p c ++
getN n2 (
p +
Z_of_nat n1)
c.
Proof.
induction n1;
intros.
simpl.
decEq.
omega.
rewrite inj_S.
simpl.
decEq.
replace (
p +
Zsucc (
Z_of_nat n1))
with ((
p + 1) +
Z_of_nat n1)
by omega.
auto.
Qed.
Theorem loadbytes_concat:
forall m b ofs n1 n2 bytes1 bytes2,
loadbytes m b ofs n1 =
Some bytes1 ->
loadbytes m b (
ofs +
n1)
n2 =
Some bytes2 ->
n1 >= 0 ->
n2 >= 0 ->
loadbytes m b ofs (
n1 +
n2) =
Some(
bytes1 ++
bytes2).
Proof.
Theorem loadbytes_split:
forall m b ofs n1 n2 bytes,
loadbytes m b ofs (
n1 +
n2) =
Some bytes ->
n1 >= 0 ->
n2 >= 0 ->
exists bytes1,
exists bytes2,
loadbytes m b ofs n1 =
Some bytes1
/\
loadbytes m b (
ofs +
n1)
n2 =
Some bytes2
/\
bytes =
bytes1 ++
bytes2.
Proof.
unfold loadbytes;
intros.
destruct (
range_perm_dec m b ofs (
ofs + (
n1 +
n2))
Cur Readable);
try congruence.
rewrite nat_of_Z_plus in H;
auto.
rewrite getN_concat in H.
rewrite nat_of_Z_eq in H;
auto.
repeat rewrite pred_dec_true.
econstructor;
econstructor.
split.
reflexivity.
split.
reflexivity.
congruence.
red;
intros;
apply r;
omega.
red;
intros;
apply r;
omega.
Qed.
Theorem load_rep:
forall ch m1 m2 b ofs v1 v2,
(
forall z, 0 <=
z <
size_chunk ch ->
m1.(
mem_contents)#
b#(
ofs+
z) =
m2.(
mem_contents)#
b#(
ofs+
z)) ->
load ch m1 b ofs =
Some v1 ->
load ch m2 b ofs =
Some v2 ->
v1 =
v2.
Proof.
Properties related to store
Theorem valid_access_store:
forall m1 chunk b ofs v,
valid_access m1 chunk b ofs Writable ->
{
m2:
mem |
store chunk m1 b ofs v =
Some m2 }.
Proof.
Hint Local Resolve valid_access_store:
mem.
Section STORE.
Variable chunk:
memory_chunk.
Variable m1:
mem.
Variable b:
block.
Variable ofs:
Z.
Variable v:
val.
Variable m2:
mem.
Hypothesis STORE:
store chunk m1 b ofs v =
Some m2.
Lemma store_access:
mem_access m2 =
mem_access m1.
Proof.
Lemma store_mem_contents:
mem_contents m2 =
ZMap.set b (
setN (
encode_val chunk v)
ofs m1.(
mem_contents)#
b)
m1.(
mem_contents).
Proof.
Theorem perm_store_1:
forall b'
ofs'
k p,
perm m1 b'
ofs'
k p ->
perm m2 b'
ofs'
k p.
Proof.
Theorem perm_store_2:
forall b'
ofs'
k p,
perm m2 b'
ofs'
k p ->
perm m1 b'
ofs'
k p.
Proof.
intros.
unfold perm in *.
rewrite store_access in H;
auto.
Qed.
Local Hint Resolve perm_store_1 perm_store_2:
mem.
Theorem nextblock_store:
nextblock m2 =
nextblock m1.
Proof.
Theorem store_valid_block_1:
forall b',
valid_block m1 b' ->
valid_block m2 b'.
Proof.
Theorem store_valid_block_2:
forall b',
valid_block m2 b' ->
valid_block m1 b'.
Proof.
Local Hint Resolve store_valid_block_1 store_valid_block_2:
mem.
Theorem store_valid_access_1:
forall chunk'
b'
ofs'
p,
valid_access m1 chunk'
b'
ofs'
p ->
valid_access m2 chunk'
b'
ofs'
p.
Proof.
intros. inv H. constructor; try red; auto with mem.
Qed.
Theorem store_valid_access_2:
forall chunk'
b'
ofs'
p,
valid_access m2 chunk'
b'
ofs'
p ->
valid_access m1 chunk'
b'
ofs'
p.
Proof.
intros. inv H. constructor; try red; auto with mem.
Qed.
Theorem store_valid_access_3:
valid_access m1 chunk b ofs Writable.
Proof.
Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3:
mem.
Theorem load_store_similar:
forall chunk',
size_chunk chunk' =
size_chunk chunk ->
exists v',
load chunk'
m2 b ofs =
Some v' /\
decode_encode_val v chunk chunk'
v'.
Proof.
Theorem load_store_similar_2:
forall chunk',
size_chunk chunk' =
size_chunk chunk ->
type_of_chunk chunk' =
type_of_chunk chunk ->
load chunk'
m2 b ofs =
Some (
Val.load_result chunk'
v).
Proof.
Theorem load_store_same:
load chunk m2 b ofs =
Some (
Val.load_result chunk v).
Proof.
Theorem load_store_other:
forall chunk'
b'
ofs',
b' <>
b
\/
ofs' +
size_chunk chunk' <=
ofs
\/
ofs +
size_chunk chunk <=
ofs' ->
load chunk'
m2 b'
ofs' =
load chunk'
m1 b'
ofs'.
Proof.
Theorem loadbytes_store_same:
loadbytes m2 b ofs (
size_chunk chunk) =
Some(
encode_val chunk v).
Proof.
Theorem loadbytes_store_other:
forall b'
ofs'
n,
b' <>
b
\/
n <= 0
\/
ofs' +
n <=
ofs
\/
ofs +
size_chunk chunk <=
ofs' ->
loadbytes m2 b'
ofs'
n =
loadbytes m1 b'
ofs'
n.
Proof.
Lemma setN_property:
forall (
P:
memval ->
Prop)
vl p q c,
(
forall v,
In v vl ->
P v) ->
p <=
q <
p +
Z_of_nat (
length vl) ->
P((
setN vl p c)#
q).
Proof.
induction vl;
intros.
simpl in H0.
omegaContradiction.
simpl length in H0.
rewrite inj_S in H0.
simpl.
destruct (
zeq p q).
subst q.
rewrite setN_outside.
rewrite ZMap.gss.
auto with coqlib.
omega.
apply IHvl.
auto with coqlib.
omega.
Qed.
Lemma getN_in:
forall c q n p,
p <=
q <
p +
Z_of_nat n ->
In (
c#
q) (
getN n p c).
Proof.
induction n;
intros.
simpl in H;
omegaContradiction.
rewrite inj_S in H.
simpl.
destruct (
zeq p q).
subst q.
auto.
right.
apply IHn.
omega.
Qed.
Theorem load_pointer_store:
forall chunk'
b'
ofs'
v_b v_o,
load chunk'
m2 b'
ofs' =
Some(
Vptr v_b v_o) ->
(
chunk =
Mint32 /\
v =
Vptr v_b v_o /\
chunk' =
Mint32 /\
b' =
b /\
ofs' =
ofs)
\/ (
b' <>
b \/
ofs' +
size_chunk chunk' <=
ofs \/
ofs +
size_chunk chunk <=
ofs').
Proof.
End STORE.
Local Hint Resolve perm_store_1 perm_store_2:
mem.
Local Hint Resolve store_valid_block_1 store_valid_block_2:
mem.
Local Hint Resolve store_valid_access_1 store_valid_access_2
store_valid_access_3:
mem.
Theorem load_store_pointer_overlap:
forall chunk m1 b ofs v_b v_o m2 chunk'
ofs'
v,
store chunk m1 b ofs (
Vptr v_b v_o) =
Some m2 ->
load chunk'
m2 b ofs' =
Some v ->
ofs' <>
ofs ->
ofs' +
size_chunk chunk' >
ofs ->
ofs +
size_chunk chunk >
ofs' ->
v =
Vundef.
Proof.
Theorem load_store_pointer_mismatch:
forall chunk m1 b ofs v_b v_o m2 chunk'
v,
store chunk m1 b ofs (
Vptr v_b v_o) =
Some m2 ->
load chunk'
m2 b ofs =
Some v ->
chunk <>
Mint32 \/
chunk' <>
Mint32 ->
v =
Vundef.
Proof.
Lemma store_similar_chunks:
forall chunk1 chunk2 v1 v2 m b ofs,
encode_val chunk1 v1 =
encode_val chunk2 v2 ->
store chunk1 m b ofs v1 =
store chunk2 m b ofs v2.
Proof.
Theorem store_signed_unsigned_8:
forall m b ofs v,
store Mint8signed m b ofs v =
store Mint8unsigned m b ofs v.
Proof.
Theorem store_signed_unsigned_16:
forall m b ofs v,
store Mint16signed m b ofs v =
store Mint16unsigned m b ofs v.
Proof.
Theorem store_int8_zero_ext:
forall m b ofs n,
store Mint8unsigned m b ofs (
Vint (
Int.zero_ext 8
n)) =
store Mint8unsigned m b ofs (
Vint n).
Proof.
Theorem store_int8_sign_ext:
forall m b ofs n,
store Mint8signed m b ofs (
Vint (
Int.sign_ext 8
n)) =
store Mint8signed m b ofs (
Vint n).
Proof.
Theorem store_int16_zero_ext:
forall m b ofs n,
store Mint16unsigned m b ofs (
Vint (
Int.zero_ext 16
n)) =
store Mint16unsigned m b ofs (
Vint n).
Proof.
Theorem store_int16_sign_ext:
forall m b ofs n,
store Mint16signed m b ofs (
Vint (
Int.sign_ext 16
n)) =
store Mint16signed m b ofs (
Vint n).
Proof.
Theorem store_float32_truncate:
forall m b ofs n,
store Mfloat32 m b ofs (
Vfloat (
Float.singleoffloat n)) =
store Mfloat32 m b ofs (
Vfloat n).
Proof.
Properties related to storebytes.
Theorem range_perm_storebytes:
forall m1 b ofs bytes,
range_perm m1 b ofs (
ofs +
Z_of_nat (
length bytes))
Cur Writable ->
{
m2 :
mem |
storebytes m1 b ofs bytes =
Some m2 }.
Proof.
Theorem storebytes_store:
forall m1 b ofs chunk v m2,
storebytes m1 b ofs (
encode_val chunk v) =
Some m2 ->
(
align_chunk chunk |
ofs) ->
store chunk m1 b ofs v =
Some m2.
Proof.
Theorem store_storebytes:
forall m1 b ofs chunk v m2,
store chunk m1 b ofs v =
Some m2 ->
storebytes m1 b ofs (
encode_val chunk v) =
Some m2.
Proof.
Section STOREBYTES.
Variable m1:
mem.
Variable b:
block.
Variable ofs:
Z.
Variable bytes:
list memval.
Variable m2:
mem.
Hypothesis STORE:
storebytes m1 b ofs bytes =
Some m2.
Lemma storebytes_access:
mem_access m2 =
mem_access m1.
Proof.
Lemma storebytes_mem_contents:
mem_contents m2 =
ZMap.set b (
setN bytes ofs m1.(
mem_contents)#
b)
m1.(
mem_contents).
Proof.
Theorem perm_storebytes_1:
forall b'
ofs'
k p,
perm m1 b'
ofs'
k p ->
perm m2 b'
ofs'
k p.
Proof.
Theorem perm_storebytes_2:
forall b'
ofs'
k p,
perm m2 b'
ofs'
k p ->
perm m1 b'
ofs'
k p.
Proof.
Local Hint Resolve perm_storebytes_1 perm_storebytes_2:
mem.
Theorem storebytes_valid_access_1:
forall chunk'
b'
ofs'
p,
valid_access m1 chunk'
b'
ofs'
p ->
valid_access m2 chunk'
b'
ofs'
p.
Proof.
intros. inv H. constructor; try red; auto with mem.
Qed.
Theorem storebytes_valid_access_2:
forall chunk'
b'
ofs'
p,
valid_access m2 chunk'
b'
ofs'
p ->
valid_access m1 chunk'
b'
ofs'
p.
Proof.
intros. inv H. constructor; try red; auto with mem.
Qed.
Local Hint Resolve storebytes_valid_access_1 storebytes_valid_access_2:
mem.
Theorem nextblock_storebytes:
nextblock m2 =
nextblock m1.
Proof.
Theorem storebytes_valid_block_1:
forall b',
valid_block m1 b' ->
valid_block m2 b'.
Proof.
Theorem storebytes_valid_block_2:
forall b',
valid_block m2 b' ->
valid_block m1 b'.
Proof.
Local Hint Resolve storebytes_valid_block_1 storebytes_valid_block_2:
mem.
Theorem storebytes_range_perm:
range_perm m1 b ofs (
ofs +
Z_of_nat (
length bytes))
Cur Writable.
Proof.
Theorem loadbytes_storebytes_same:
loadbytes m2 b ofs (
Z_of_nat (
length bytes)) =
Some bytes.
Proof.
Theorem loadbytes_storebytes_other:
forall b'
ofs'
len,
len >= 0 ->
b' <>
b
\/
ofs' +
len <=
ofs
\/
ofs +
Z_of_nat (
length bytes) <=
ofs' ->
loadbytes m2 b'
ofs'
len =
loadbytes m1 b'
ofs'
len.
Proof.
Theorem load_storebytes_other:
forall chunk b'
ofs',
b' <>
b
\/
ofs' +
size_chunk chunk <=
ofs
\/
ofs +
Z_of_nat (
length bytes) <=
ofs' ->
load chunk m2 b'
ofs' =
load chunk m1 b'
ofs'.
Proof.
End STOREBYTES.
Lemma setN_concat:
forall bytes1 bytes2 ofs c,
setN (
bytes1 ++
bytes2)
ofs c =
setN bytes2 (
ofs +
Z_of_nat (
length bytes1)) (
setN bytes1 ofs c).
Proof.
induction bytes1;
intros.
simpl.
decEq.
omega.
simpl length.
rewrite inj_S.
simpl.
rewrite IHbytes1.
decEq.
omega.
Qed.
Theorem storebytes_concat:
forall m b ofs bytes1 m1 bytes2 m2,
storebytes m b ofs bytes1 =
Some m1 ->
storebytes m1 b (
ofs +
Z_of_nat(
length bytes1))
bytes2 =
Some m2 ->
storebytes m b ofs (
bytes1 ++
bytes2) =
Some m2.
Proof.
Theorem storebytes_split:
forall m b ofs bytes1 bytes2 m2,
storebytes m b ofs (
bytes1 ++
bytes2) =
Some m2 ->
exists m1,
storebytes m b ofs bytes1 =
Some m1
/\
storebytes m1 b (
ofs +
Z_of_nat(
length bytes1))
bytes2 =
Some m2.
Proof.
Properties related to alloc.
Section ALLOC.
Variable m1:
mem.
Variables lo hi:
Z.
Variable m2:
mem.
Variable b:
block.
Hypothesis ALLOC:
alloc m1 lo hi = (
m2,
b).
Theorem nextblock_alloc:
nextblock m2 =
Zsucc (
nextblock m1).
Proof.
injection ALLOC; intros. rewrite <- H0; auto.
Qed.
Theorem alloc_result:
b =
nextblock m1.
Proof.
injection ALLOC; auto.
Qed.
Theorem valid_block_alloc:
forall b',
valid_block m1 b' ->
valid_block m2 b'.
Proof.
Theorem fresh_block_alloc:
~(
valid_block m1 b).
Proof.
Theorem valid_new_block:
valid_block m2 b.
Proof.
Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block:
mem.
Theorem valid_block_alloc_inv:
forall b',
valid_block m2 b' ->
b' =
b \/
valid_block m1 b'.
Proof.
Theorem perm_alloc_1:
forall b'
ofs k p,
perm m1 b'
ofs k p ->
perm m2 b'
ofs k p.
Proof.
Theorem perm_alloc_2:
forall ofs k,
lo <=
ofs <
hi ->
perm m2 b ofs k Freeable.
Proof.
unfold perm;
intros.
injection ALLOC;
intros.
rewrite <-
H1;
simpl.
subst b.
rewrite ZMap.gss.
unfold proj_sumbool.
rewrite zle_true.
rewrite zlt_true.
simpl.
auto with mem.
omega.
omega.
Qed.
Theorem perm_alloc_inv:
forall b'
ofs k p,
perm m2 b'
ofs k p ->
if zeq b'
b then lo <=
ofs <
hi else perm m1 b'
ofs k p.
Proof.
intros until p;
unfold perm.
inv ALLOC.
simpl.
rewrite ZMap.gsspec.
unfold ZIndexed.eq.
destruct (
zeq b' (
nextblock m1));
intros.
destruct (
zle lo ofs);
try contradiction.
destruct (
zlt ofs hi);
try contradiction.
split;
auto.
auto.
Qed.
Theorem perm_alloc_3:
forall ofs k p,
perm m2 b ofs k p ->
lo <=
ofs <
hi.
Proof.
Theorem perm_alloc_4:
forall b'
ofs k p,
perm m2 b'
ofs k p ->
b' <>
b ->
perm m1 b'
ofs k p.
Proof.
Local Hint Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3 perm_alloc_4:
mem.
Theorem valid_access_alloc_other:
forall chunk b'
ofs p,
valid_access m1 chunk b'
ofs p ->
valid_access m2 chunk b'
ofs p.
Proof.
intros. inv H. constructor; auto with mem.
red; auto with mem.
Qed.
Theorem valid_access_alloc_same:
forall chunk ofs,
lo <=
ofs ->
ofs +
size_chunk chunk <=
hi -> (
align_chunk chunk |
ofs) ->
valid_access m2 chunk b ofs Freeable.
Proof.
intros.
constructor;
auto with mem.
red;
intros.
apply perm_alloc_2.
omega.
Qed.
Local Hint Resolve valid_access_alloc_other valid_access_alloc_same:
mem.
Theorem valid_access_alloc_inv:
forall chunk b'
ofs p,
valid_access m2 chunk b'
ofs p ->
if eq_block b'
b
then lo <=
ofs /\
ofs +
size_chunk chunk <=
hi /\ (
align_chunk chunk |
ofs)
else valid_access m1 chunk b'
ofs p.
Proof.
Theorem load_alloc_unchanged:
forall chunk b'
ofs,
valid_block m1 b' ->
load chunk m2 b'
ofs =
load chunk m1 b'
ofs.
Proof.
Theorem load_alloc_other:
forall chunk b'
ofs v,
load chunk m1 b'
ofs =
Some v ->
load chunk m2 b'
ofs =
Some v.
Proof.
Theorem load_alloc_same:
forall chunk ofs v,
load chunk m2 b ofs =
Some v ->
v =
Vundef.
Proof.
intros.
exploit load_result;
eauto.
intro.
rewrite H0.
injection ALLOC;
intros.
rewrite <-
H2;
simpl.
rewrite <-
H1.
rewrite ZMap.gss.
destruct chunk;
simpl;
repeat rewrite ZMap.gi;
reflexivity.
Qed.
Theorem load_alloc_same':
forall chunk ofs,
lo <=
ofs ->
ofs +
size_chunk chunk <=
hi -> (
align_chunk chunk |
ofs) ->
load chunk m2 b ofs =
Some Vundef.
Proof.
End ALLOC.
Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block:
mem.
Local Hint Resolve valid_access_alloc_other valid_access_alloc_same:
mem.
Properties related to free.
Theorem range_perm_free:
forall m1 b lo hi,
range_perm m1 b lo hi Cur Freeable ->
{
m2:
mem |
free m1 b lo hi =
Some m2 }.
Proof.
intros;
unfold free.
rewrite pred_dec_true;
auto.
econstructor;
eauto.
Qed.
Section FREE.
Variable m1:
mem.
Variable bf:
block.
Variables lo hi:
Z.
Variable m2:
mem.
Hypothesis FREE:
free m1 bf lo hi =
Some m2.
Theorem free_range_perm:
range_perm m1 bf lo hi Cur Freeable.
Proof.
Lemma free_result:
m2 =
unchecked_free m1 bf lo hi.
Proof.
Theorem nextblock_free:
nextblock m2 =
nextblock m1.
Proof.
Theorem valid_block_free_1:
forall b,
valid_block m1 b ->
valid_block m2 b.
Proof.
Theorem valid_block_free_2:
forall b,
valid_block m2 b ->
valid_block m1 b.
Proof.
Local Hint Resolve valid_block_free_1 valid_block_free_2:
mem.
Theorem perm_free_1:
forall b ofs k p,
b <>
bf \/
ofs <
lo \/
hi <=
ofs ->
perm m1 b ofs k p ->
perm m2 b ofs k p.
Proof.
Theorem perm_free_2:
forall ofs k p,
lo <=
ofs <
hi -> ~
perm m2 bf ofs k p.
Proof.
Theorem perm_free_3:
forall b ofs k p,
perm m2 b ofs k p ->
perm m1 b ofs k p.
Proof.
Theorem perm_free_inv:
forall b ofs k p,
perm m1 b ofs k p ->
(
b =
bf /\
lo <=
ofs <
hi) \/
perm m2 b ofs k p.
Proof.
Theorem valid_access_free_1:
forall chunk b ofs p,
valid_access m1 chunk b ofs p ->
b <>
bf \/
lo >=
hi \/
ofs +
size_chunk chunk <=
lo \/
hi <=
ofs ->
valid_access m2 chunk b ofs p.
Proof.
intros.
inv H.
constructor;
auto with mem.
red;
intros.
eapply perm_free_1;
eauto.
destruct (
zlt lo hi).
intuition.
right.
omega.
Qed.
Theorem valid_access_free_2:
forall chunk ofs p,
lo <
hi ->
ofs +
size_chunk chunk >
lo ->
ofs <
hi ->
~(
valid_access m2 chunk bf ofs p).
Proof.
Theorem valid_access_free_inv_1:
forall chunk b ofs p,
valid_access m2 chunk b ofs p ->
valid_access m1 chunk b ofs p.
Proof.
intros.
destruct H.
split;
auto.
red;
intros.
generalize (
H ofs0 H1).
rewrite free_result.
unfold perm,
unchecked_free;
simpl.
rewrite ZMap.gsspec.
destruct (
ZIndexed.eq b bf).
subst b.
destruct (
zle lo ofs0);
simpl.
destruct (
zlt ofs0 hi);
simpl.
tauto.
auto.
auto.
auto.
Qed.
Theorem valid_access_free_inv_2:
forall chunk ofs p,
valid_access m2 chunk bf ofs p ->
lo >=
hi \/
ofs +
size_chunk chunk <=
lo \/
hi <=
ofs.
Proof.
Theorem load_free:
forall chunk b ofs,
b <>
bf \/
lo >=
hi \/
ofs +
size_chunk chunk <=
lo \/
hi <=
ofs ->
load chunk m2 b ofs =
load chunk m1 b ofs.
Proof.
End FREE.
Local Hint Resolve valid_block_free_1 valid_block_free_2
perm_free_1 perm_free_2 perm_free_3
valid_access_free_1 valid_access_free_inv_1:
mem.
Properties related to drop_perm
Theorem range_perm_drop_1:
forall m b lo hi p m',
drop_perm m b lo hi p =
Some m' ->
range_perm m b lo hi Cur Freeable.
Proof.
Theorem range_perm_drop_2:
forall m b lo hi p,
range_perm m b lo hi Cur Freeable -> {
m' |
drop_perm m b lo hi p =
Some m' }.
Proof.
Section DROP.
Variable m:
mem.
Variable b:
block.
Variable lo hi:
Z.
Variable p:
permission.
Variable m':
mem.
Hypothesis DROP:
drop_perm m b lo hi p =
Some m'.
Theorem nextblock_drop:
nextblock m' =
nextblock m.
Proof.
Theorem drop_perm_valid_block_1:
forall b',
valid_block m b' ->
valid_block m'
b'.
Proof.
Theorem drop_perm_valid_block_2:
forall b',
valid_block m'
b' ->
valid_block m b'.
Proof.
Theorem perm_drop_1:
forall ofs k,
lo <=
ofs <
hi ->
perm m'
b ofs k p.
Proof.
Theorem perm_drop_2:
forall ofs k p',
lo <=
ofs <
hi ->
perm m'
b ofs k p' ->
perm_order p p'.
Proof.
Theorem perm_drop_3:
forall b'
ofs k p',
b' <>
b \/
ofs <
lo \/
hi <=
ofs ->
perm m b'
ofs k p' ->
perm m'
b'
ofs k p'.
Proof.
Theorem perm_drop_4:
forall b'
ofs k p',
perm m'
b'
ofs k p' ->
perm m b'
ofs k p'.
Proof.
Lemma valid_access_drop_1:
forall chunk b'
ofs p',
b' <>
b \/
ofs +
size_chunk chunk <=
lo \/
hi <=
ofs \/
perm_order p p' ->
valid_access m chunk b'
ofs p' ->
valid_access m'
chunk b'
ofs p'.
Proof.
Lemma valid_access_drop_2:
forall chunk b'
ofs p',
valid_access m'
chunk b'
ofs p' ->
valid_access m chunk b'
ofs p'.
Proof.
intros.
destruct H;
split;
auto.
red;
intros.
eapply perm_drop_4;
eauto.
Qed.
Theorem load_drop:
forall chunk b'
ofs,
b' <>
b \/
ofs +
size_chunk chunk <=
lo \/
hi <=
ofs \/
perm_order p Readable ->
load chunk m'
b'
ofs =
load chunk m b'
ofs.
Proof.
End DROP.
Generic injections
A memory state
m1 generically injects into another memory state
m2 via the
memory injection
f if the following conditions hold:
-
each access in m2 that corresponds to a valid access in m1
is itself valid;
-
the memory value associated in m1 to an accessible address
must inject into m2's memory value at the corersponding address.
(
f:
meminj) (
m1 m2:
mem) :
Prop :=
mk_mem_inj {
mi_perm:
forall b1 b2 delta ofs k p,
f b1 =
Some(
b2,
delta) ->
perm m1 b1 ofs k p ->
perm m2 b2 (
ofs +
delta)
k p;
mi_access:
forall b1 b2 delta chunk ofs p,
f b1 =
Some(
b2,
delta) ->
valid_access m1 chunk b1 ofs p ->
valid_access m2 chunk b2 (
ofs +
delta)
p;
mi_memval:
forall b1 ofs b2 delta,
f b1 =
Some(
b2,
delta) ->
perm m1 b1 ofs Cur Readable ->
memval_inject f (
m1.(
mem_contents)#
b1#
ofs) (
m2.(
mem_contents)#
b2#(
ofs +
delta))
}.
Preservation of permissions
Lemma perm_inj:
forall f m1 m2 b1 ofs k p b2 delta,
mem_inj f m1 m2 ->
perm m1 b1 ofs k p ->
f b1 =
Some(
b2,
delta) ->
perm m2 b2 (
ofs +
delta)
k p.
Proof.
intros.
eapply mi_perm;
eauto.
Qed.
Lemma range_perm_inj:
forall f m1 m2 b1 lo hi k p b2 delta,
mem_inj f m1 m2 ->
range_perm m1 b1 lo hi k p ->
f b1 =
Some(
b2,
delta) ->
range_perm m2 b2 (
lo +
delta) (
hi +
delta)
k p.
Proof.
intros;
red;
intros.
replace ofs with ((
ofs -
delta) +
delta)
by omega.
eapply perm_inj;
eauto.
apply H0.
omega.
Qed.
Preservation of loads.
Lemma getN_inj:
forall f m1 m2 b1 b2 delta,
mem_inj f m1 m2 ->
f b1 =
Some(
b2,
delta) ->
forall n ofs,
range_perm m1 b1 ofs (
ofs +
Z_of_nat n)
Cur Readable ->
list_forall2 (
memval_inject f)
(
getN n ofs (
m1.(
mem_contents)#
b1))
(
getN n (
ofs +
delta) (
m2.(
mem_contents)#
b2)).
Proof.
induction n;
intros;
simpl.
constructor.
rewrite inj_S in H1.
constructor.
eapply mi_memval;
eauto.
apply H1.
omega.
replace (
ofs +
delta + 1)
with ((
ofs + 1) +
delta)
by omega.
apply IHn.
red;
intros;
apply H1;
omega.
Qed.
Lemma load_inj:
forall f m1 m2 chunk b1 ofs b2 delta v1,
mem_inj f m1 m2 ->
load chunk m1 b1 ofs =
Some v1 ->
f b1 =
Some (
b2,
delta) ->
exists v2,
load chunk m2 b2 (
ofs +
delta) =
Some v2 /\
val_inject f v1 v2.
Proof.
Lemma loadbytes_inj:
forall f m1 m2 len b1 ofs b2 delta bytes1,
mem_inj f m1 m2 ->
loadbytes m1 b1 ofs len =
Some bytes1 ->
f b1 =
Some (
b2,
delta) ->
exists bytes2,
loadbytes m2 b2 (
ofs +
delta)
len =
Some bytes2
/\
list_forall2 (
memval_inject f)
bytes1 bytes2.
Proof.
Preservation of stores.
Lemma setN_inj:
forall (
access:
Z ->
Prop)
delta f vl1 vl2,
list_forall2 (
memval_inject f)
vl1 vl2 ->
forall p c1 c2,
(
forall q,
access q ->
memval_inject f (
c1#
q) (
c2#(
q +
delta))) ->
(
forall q,
access q ->
memval_inject f ((
setN vl1 p c1)#
q)
((
setN vl2 (
p +
delta)
c2)#(
q +
delta))).
Proof.
induction 1;
intros;
simpl.
auto.
replace (
p +
delta + 1)
with ((
p + 1) +
delta)
by omega.
apply IHlist_forall2;
auto.
intros.
rewrite ZMap.gsspec at 1.
destruct (
ZIndexed.eq q0 p).
subst q0.
rewrite ZMap.gss.
auto.
rewrite ZMap.gso.
auto.
unfold ZIndexed.t in *.
omega.
Qed.
Definition meminj_no_overlap (
f:
meminj) (
m:
mem) :
Prop :=
forall b1 b1'
delta1 b2 b2'
delta2 ofs1 ofs2,
b1 <>
b2 ->
f b1 =
Some (
b1',
delta1) ->
f b2 =
Some (
b2',
delta2) ->
perm m b1 ofs1 Max Nonempty ->
perm m b2 ofs2 Max Nonempty ->
b1' <>
b2' \/
ofs1 +
delta1 <>
ofs2 +
delta2.
Lemma store_mapped_inj:
forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
mem_inj f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
meminj_no_overlap f m1 ->
f b1 =
Some (
b2,
delta) ->
val_inject f v1 v2 ->
exists n2,
store chunk m2 b2 (
ofs +
delta)
v2 =
Some n2
/\
mem_inj f n1 n2.
Proof.
Lemma store_unmapped_inj:
forall f chunk m1 b1 ofs v1 n1 m2,
mem_inj f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
f b1 =
None ->
mem_inj f n1 m2.
Proof.
Lemma store_outside_inj:
forall f m1 m2 chunk b ofs v m2',
mem_inj f m1 m2 ->
(
forall b'
delta ofs',
f b' =
Some(
b,
delta) ->
perm m1 b'
ofs'
Cur Readable ->
ofs <=
ofs' +
delta <
ofs +
size_chunk chunk ->
False) ->
store chunk m2 b ofs v =
Some m2' ->
mem_inj f m1 m2'.
Proof.
Lemma storebytes_mapped_inj:
forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
mem_inj f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
meminj_no_overlap f m1 ->
f b1 =
Some (
b2,
delta) ->
list_forall2 (
memval_inject f)
bytes1 bytes2 ->
exists n2,
storebytes m2 b2 (
ofs +
delta)
bytes2 =
Some n2
/\
mem_inj f n1 n2.
Proof.
Lemma storebytes_unmapped_inj:
forall f m1 b1 ofs bytes1 n1 m2,
mem_inj f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
f b1 =
None ->
mem_inj f n1 m2.
Proof.
Lemma storebytes_outside_inj:
forall f m1 m2 b ofs bytes2 m2',
mem_inj f m1 m2 ->
(
forall b'
delta ofs',
f b' =
Some(
b,
delta) ->
perm m1 b'
ofs'
Cur Readable ->
ofs <=
ofs' +
delta <
ofs +
Z_of_nat (
length bytes2) ->
False) ->
storebytes m2 b ofs bytes2 =
Some m2' ->
mem_inj f m1 m2'.
Proof.
Preservation of allocations
Lemma alloc_right_inj:
forall f m1 m2 lo hi b2 m2',
mem_inj f m1 m2 ->
alloc m2 lo hi = (
m2',
b2) ->
mem_inj f m1 m2'.
Proof.
intros.
injection H0.
intros NEXT MEM.
inversion H.
constructor.
intros.
eapply perm_alloc_1;
eauto.
intros.
eapply valid_access_alloc_other;
eauto.
intros.
assert (
perm m2 b0 (
ofs +
delta)
Cur Readable).
eapply mi_perm0;
eauto.
assert (
valid_block m2 b0)
by eauto with mem.
rewrite <-
MEM;
simpl.
rewrite ZMap.gso.
eauto with mem.
rewrite NEXT.
eauto with mem.
Qed.
Lemma alloc_left_unmapped_inj:
forall f m1 m2 lo hi m1'
b1,
mem_inj f m1 m2 ->
alloc m1 lo hi = (
m1',
b1) ->
f b1 =
None ->
mem_inj f m1'
m2.
Proof.
intros.
inversion H.
constructor.
intros.
exploit perm_alloc_inv;
eauto.
intros.
destruct (
zeq b0 b1).
congruence.
eauto.
intros.
exploit valid_access_alloc_inv;
eauto.
unfold eq_block.
intros.
destruct (
zeq b0 b1).
congruence.
eauto.
injection H0;
intros NEXT MEM.
intros.
rewrite <-
MEM;
simpl.
rewrite NEXT.
exploit perm_alloc_inv;
eauto.
intros.
rewrite ZMap.gsspec.
unfold ZIndexed.eq.
destruct (
zeq b0 b1).
rewrite ZMap.gi.
constructor.
eauto.
Qed.
Definition inj_offset_aligned (
delta:
Z) (
size:
Z) :
Prop :=
forall chunk,
size_chunk chunk <=
size -> (
align_chunk chunk |
delta).
Lemma alloc_left_mapped_inj:
forall f m1 m2 lo hi m1'
b1 b2 delta,
mem_inj f m1 m2 ->
alloc m1 lo hi = (
m1',
b1) ->
valid_block m2 b2 ->
inj_offset_aligned delta (
hi-
lo) ->
(
forall ofs k p,
lo <=
ofs <
hi ->
perm m2 b2 (
ofs +
delta)
k p) ->
f b1 =
Some(
b2,
delta) ->
mem_inj f m1'
m2.
Proof.
intros.
inversion H.
constructor.
intros.
exploit perm_alloc_inv;
eauto.
intros.
destruct (
zeq b0 b1).
subst b0.
rewrite H4 in H5;
inv H5.
eauto.
eauto.
intros.
exploit valid_access_alloc_inv;
eauto.
unfold eq_block.
intros.
destruct (
zeq b0 b1).
subst b0.
rewrite H4 in H5.
inv H5.
split.
red;
intros.
replace ofs0 with ((
ofs0 -
delta0) +
delta0)
by omega.
apply H3.
omega.
destruct H6.
apply Zdivide_plus_r.
auto.
apply H2.
omega.
eauto.
injection H0;
intros NEXT MEM.
intros.
rewrite <-
MEM;
simpl.
rewrite NEXT.
exploit perm_alloc_inv;
eauto.
intros.
rewrite ZMap.gsspec.
unfold ZIndexed.eq.
destruct (
zeq b0 b1).
rewrite ZMap.gi.
constructor.
eauto.
Qed.
Lemma free_left_inj:
forall f m1 m2 b lo hi m1',
mem_inj f m1 m2 ->
free m1 b lo hi =
Some m1' ->
mem_inj f m1'
m2.
Proof.
intros.
exploit free_result;
eauto.
intro FREE.
inversion H.
constructor.
intros.
eauto with mem.
intros.
eauto with mem.
intros.
rewrite FREE;
simpl.
eauto with mem.
Qed.
Lemma free_right_inj:
forall f m1 m2 b lo hi m2',
mem_inj f m1 m2 ->
free m2 b lo hi =
Some m2' ->
(
forall b'
delta ofs k p,
f b' =
Some(
b,
delta) ->
perm m1 b'
ofs k p ->
lo <=
ofs +
delta <
hi ->
False) ->
mem_inj f m1 m2'.
Proof.
intros.
exploit free_result;
eauto.
intro FREE.
inversion H.
assert (
PERM:
forall b1 b2 delta ofs k p,
f b1 =
Some (
b2,
delta) ->
perm m1 b1 ofs k p ->
perm m2'
b2 (
ofs +
delta)
k p).
intros.
intros.
eapply perm_free_1;
eauto.
destruct (
zeq b2 b);
auto.
subst b.
right.
assert (~ (
lo <=
ofs +
delta <
hi)).
red;
intros;
eapply H1;
eauto.
omega.
constructor.
auto.
intros.
exploit mi_access0;
eauto.
intros [
RG AL].
split;
auto.
red;
intros.
replace ofs0 with ((
ofs0 -
delta) +
delta)
by omega.
eapply PERM.
eauto.
apply H3.
omega.
intros.
rewrite FREE;
simpl.
eauto.
Qed.
Preservation of drop_perm operations.
Lemma drop_unmapped_inj:
forall f m1 m2 b lo hi p m1',
mem_inj f m1 m2 ->
drop_perm m1 b lo hi p =
Some m1' ->
f b =
None ->
mem_inj f m1'
m2.
Proof.
Lemma drop_mapped_inj:
forall f m1 m2 b1 b2 delta lo hi p m1',
mem_inj f m1 m2 ->
drop_perm m1 b1 lo hi p =
Some m1' ->
meminj_no_overlap f m1 ->
f b1 =
Some(
b2,
delta) ->
exists m2',
drop_perm m2 b2 (
lo +
delta) (
hi +
delta)
p =
Some m2'
/\
mem_inj f m1'
m2'.
Proof.
intros.
assert ({
m2' |
drop_perm m2 b2 (
lo +
delta) (
hi +
delta)
p =
Some m2' }).
apply range_perm_drop_2.
red;
intros.
replace ofs with ((
ofs -
delta) +
delta)
by omega.
eapply perm_inj;
eauto.
eapply range_perm_drop_1;
eauto.
omega.
destruct X as [
m2'
DROP].
exists m2';
split;
auto.
inv H.
assert (
PERM:
forall b0 b3 delta0 ofs k p0,
f b0 =
Some (
b3,
delta0) ->
perm m1'
b0 ofs k p0 ->
perm m2'
b3 (
ofs +
delta0)
k p0).
intros.
assert (
perm m2 b3 (
ofs +
delta0)
k p0).
eapply mi_perm0;
eauto.
eapply perm_drop_4;
eauto.
destruct (
zeq b1 b0).
subst b0.
rewrite H2 in H;
inv H.
destruct (
zlt (
ofs +
delta0) (
lo +
delta0)).
eapply perm_drop_3;
eauto.
destruct (
zle (
hi +
delta0) (
ofs +
delta0)).
eapply perm_drop_3;
eauto.
assert (
perm_order p p0).
eapply perm_drop_2.
eexact H0.
instantiate (1 :=
ofs).
omega.
eauto.
apply perm_implies with p;
auto.
eapply perm_drop_1.
eauto.
omega.
eapply perm_drop_3;
eauto.
destruct (
zeq b3 b2);
auto.
destruct (
zlt (
ofs +
delta0) (
lo +
delta));
auto.
destruct (
zle (
hi +
delta) (
ofs +
delta0));
auto.
exploit H1;
eauto.
instantiate (1 :=
ofs +
delta0 -
delta).
apply perm_cur_max.
apply perm_implies with Freeable.
eapply range_perm_drop_1;
eauto.
omega.
auto with mem.
eapply perm_drop_4;
eauto.
eapply perm_max.
apply perm_implies with p0.
eauto.
eauto with mem.
unfold block.
omega.
constructor.
auto.
intros.
exploit mi_access0;
eauto.
eapply valid_access_drop_2;
eauto.
intros [
A B].
split;
auto.
red;
intros.
replace ofs0 with ((
ofs0 -
delta0) +
delta0)
by omega.
eapply PERM;
eauto.
apply H3.
omega.
intros.
replace (
m1'.(
mem_contents)#
b0)
with (
m1.(
mem_contents)#
b0).
replace (
m2'.(
mem_contents)#
b3)
with (
m2.(
mem_contents)#
b3).
apply mi_memval0;
auto.
eapply perm_drop_4;
eauto.
unfold drop_perm in DROP;
destruct (
range_perm_dec m2 b2 (
lo +
delta) (
hi +
delta)
Cur Freeable);
inv DROP;
auto.
unfold drop_perm in H0;
destruct (
range_perm_dec m1 b1 lo hi Cur Freeable);
inv H0;
auto.
Qed.
Lemma drop_outside_inj:
forall f m1 m2 b lo hi p m2',
mem_inj f m1 m2 ->
drop_perm m2 b lo hi p =
Some m2' ->
(
forall b'
delta ofs'
k p,
f b' =
Some(
b,
delta) ->
perm m1 b'
ofs'
k p ->
lo <=
ofs' +
delta <
hi ->
False) ->
mem_inj f m1 m2'.
Proof.
intros.
inv H.
assert (
PERM:
forall b0 b3 delta0 ofs k p0,
f b0 =
Some (
b3,
delta0) ->
perm m1 b0 ofs k p0 ->
perm m2'
b3 (
ofs +
delta0)
k p0).
intros.
eapply perm_drop_3;
eauto.
destruct (
zeq b3 b);
auto.
subst b3.
right.
destruct (
zlt (
ofs +
delta0)
lo);
auto.
destruct (
zle hi (
ofs +
delta0));
auto.
byContradiction.
exploit H1;
eauto.
omega.
constructor.
auto.
intros.
exploit mi_access0;
eauto.
intros [
A B].
split;
auto.
red;
intros.
replace ofs0 with ((
ofs0 -
delta) +
delta)
by omega.
eapply PERM;
eauto.
apply H2.
omega.
intros.
replace (
m2'.(
mem_contents)#
b2)
with (
m2.(
mem_contents)#
b2).
apply mi_memval0;
auto.
unfold drop_perm in H0;
destruct (
range_perm_dec m2 b lo hi Cur Freeable);
inv H0;
auto.
Qed.
Memory extensions
A store m2 extends a store m1 if m2 can be obtained from m1
by increasing the sizes of the memory blocks of m1 (decreasing
the low bounds, increasing the high bounds), and replacing some of
the Vundef values stored in m1 by more defined values stored
in m2 at the same locations.
Record extends' (
m1 m2:
mem) :
Prop :=
mk_extends {
mext_next:
nextblock m1 =
nextblock m2;
mext_inj:
mem_inj inject_id m1 m2
}.
Definition extends :=
extends'.
Theorem extends_refl:
forall m,
extends m m.
Proof.
intros.
constructor.
auto.
constructor.
intros.
unfold inject_id in H;
inv H.
replace (
ofs + 0)
with ofs by omega.
auto.
intros.
unfold inject_id in H;
inv H.
replace (
ofs + 0)
with ofs by omega.
auto.
intros.
unfold inject_id in H;
inv H.
replace (
ofs + 0)
with ofs by omega.
apply memval_lessdef_refl.
Qed.
Theorem load_extends:
forall chunk m1 m2 b ofs v1,
extends m1 m2 ->
load chunk m1 b ofs =
Some v1 ->
exists v2,
load chunk m2 b ofs =
Some v2 /\
Val.lessdef v1 v2.
Proof.
intros.
inv H.
exploit load_inj;
eauto.
unfold inject_id;
reflexivity.
intros [
v2 [
A B]].
exists v2;
split.
replace (
ofs + 0)
with ofs in A by omega.
auto.
rewrite val_inject_id in B.
auto.
Qed.
Theorem loadv_extends:
forall chunk m1 m2 addr1 addr2 v1,
extends m1 m2 ->
loadv chunk m1 addr1 =
Some v1 ->
Val.lessdef addr1 addr2 ->
exists v2,
loadv chunk m2 addr2 =
Some v2 /\
Val.lessdef v1 v2.
Proof.
unfold loadv;
intros.
inv H1.
destruct addr2;
try congruence.
eapply load_extends;
eauto.
congruence.
Qed.
Theorem loadbytes_extends:
forall m1 m2 b ofs len bytes1,
extends m1 m2 ->
loadbytes m1 b ofs len =
Some bytes1 ->
exists bytes2,
loadbytes m2 b ofs len =
Some bytes2
/\
list_forall2 memval_lessdef bytes1 bytes2.
Proof.
intros.
inv H.
replace ofs with (
ofs + 0)
by omega.
eapply loadbytes_inj;
eauto.
Qed.
Theorem store_within_extends:
forall chunk m1 m2 b ofs v1 m1'
v2,
extends m1 m2 ->
store chunk m1 b ofs v1 =
Some m1' ->
Val.lessdef v1 v2 ->
exists m2',
store chunk m2 b ofs v2 =
Some m2'
/\
extends m1'
m2'.
Proof.
intros.
inversion H.
exploit store_mapped_inj;
eauto.
unfold inject_id;
red;
intros.
inv H3;
inv H4.
auto.
unfold inject_id;
reflexivity.
rewrite val_inject_id.
eauto.
intros [
m2' [
A B]].
exists m2';
split.
replace (
ofs + 0)
with ofs in A by omega.
auto.
split;
auto.
rewrite (
nextblock_store _ _ _ _ _ _ H0).
rewrite (
nextblock_store _ _ _ _ _ _ A).
auto.
Qed.
Theorem store_outside_extends:
forall chunk m1 m2 b ofs v m2',
extends m1 m2 ->
store chunk m2 b ofs v =
Some m2' ->
(
forall ofs',
perm m1 b ofs'
Cur Readable ->
ofs <=
ofs' <
ofs +
size_chunk chunk ->
False) ->
extends m1 m2'.
Proof.
intros.
inversion H.
constructor.
rewrite (
nextblock_store _ _ _ _ _ _ H0).
auto.
eapply store_outside_inj;
eauto.
unfold inject_id;
intros.
inv H2.
eapply H1;
eauto.
omega.
Qed.
Theorem storev_extends:
forall chunk m1 m2 addr1 v1 m1'
addr2 v2,
extends m1 m2 ->
storev chunk m1 addr1 v1 =
Some m1' ->
Val.lessdef addr1 addr2 ->
Val.lessdef v1 v2 ->
exists m2',
storev chunk m2 addr2 v2 =
Some m2'
/\
extends m1'
m2'.
Proof.
unfold storev;
intros.
inv H1.
destruct addr2;
try congruence.
eapply store_within_extends;
eauto.
congruence.
Qed.
Theorem storebytes_within_extends:
forall m1 m2 b ofs bytes1 m1'
bytes2,
extends m1 m2 ->
storebytes m1 b ofs bytes1 =
Some m1' ->
list_forall2 memval_lessdef bytes1 bytes2 ->
exists m2',
storebytes m2 b ofs bytes2 =
Some m2'
/\
extends m1'
m2'.
Proof.
intros.
inversion H.
exploit storebytes_mapped_inj;
eauto.
unfold inject_id;
red;
intros.
inv H3;
inv H4.
auto.
unfold inject_id;
reflexivity.
intros [
m2' [
A B]].
exists m2';
split.
replace (
ofs + 0)
with ofs in A by omega.
auto.
split;
auto.
rewrite (
nextblock_storebytes _ _ _ _ _ H0).
rewrite (
nextblock_storebytes _ _ _ _ _ A).
auto.
Qed.
Theorem storebytes_outside_extends:
forall m1 m2 b ofs bytes2 m2',
extends m1 m2 ->
storebytes m2 b ofs bytes2 =
Some m2' ->
(
forall ofs',
perm m1 b ofs'
Cur Readable ->
ofs <=
ofs' <
ofs +
Z_of_nat (
length bytes2) ->
False) ->
extends m1 m2'.
Proof.
Theorem alloc_extends:
forall m1 m2 lo1 hi1 b m1'
lo2 hi2,
extends m1 m2 ->
alloc m1 lo1 hi1 = (
m1',
b) ->
lo2 <=
lo1 ->
hi1 <=
hi2 ->
exists m2',
alloc m2 lo2 hi2 = (
m2',
b)
/\
extends m1'
m2'.
Proof.
Theorem free_left_extends:
forall m1 m2 b lo hi m1',
extends m1 m2 ->
free m1 b lo hi =
Some m1' ->
extends m1'
m2.
Proof.
Theorem free_right_extends:
forall m1 m2 b lo hi m2',
extends m1 m2 ->
free m2 b lo hi =
Some m2' ->
(
forall ofs k p,
perm m1 b ofs k p ->
lo <=
ofs <
hi ->
False) ->
extends m1 m2'.
Proof.
intros.
inv H.
constructor.
rewrite (
nextblock_free _ _ _ _ _ H0).
auto.
eapply free_right_inj;
eauto.
unfold inject_id;
intros.
inv H.
eapply H1;
eauto.
omega.
Qed.
Theorem free_parallel_extends:
forall m1 m2 b lo hi m1',
extends m1 m2 ->
free m1 b lo hi =
Some m1' ->
exists m2',
free m2 b lo hi =
Some m2'
/\
extends m1'
m2'.
Proof.
Theorem valid_block_extends:
forall m1 m2 b,
extends m1 m2 ->
(
valid_block m1 b <->
valid_block m2 b).
Proof.
intros. inv H. unfold valid_block. rewrite mext_next0. omega.
Qed.
Theorem perm_extends:
forall m1 m2 b ofs k p,
extends m1 m2 ->
perm m1 b ofs k p ->
perm m2 b ofs k p.
Proof.
intros.
inv H.
replace ofs with (
ofs + 0)
by omega.
eapply perm_inj;
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.
Proof.
intros.
inv H.
replace ofs with (
ofs + 0)
by omega.
eapply mi_access;
eauto.
auto.
Qed.
Theorem valid_pointer_extends:
forall m1 m2 b ofs,
extends m1 m2 ->
valid_pointer m1 b ofs =
true ->
valid_pointer m2 b ofs =
true.
Proof.
Memory injections
A memory state
m1 injects into another memory state
m2 via the
memory injection
f if the following conditions hold:
-
each access in m2 that corresponds to a valid access in m1
is itself valid;
-
the memory value associated in m1 to an accessible address
must inject into m2's memory value at the corersponding address;
-
unallocated blocks in m1 must be mapped to None by f;
-
if f b = Some(b', delta), b' must be valid in m2;
-
distinct blocks in m1 are mapped to non-overlapping sub-blocks in m2;
-
the sizes of m2's blocks are representable with signed machine integers;
-
the offsets delta are representable with signed machine integers.
' (
f:
meminj) (
m1 m2:
mem) :
Prop :=
mk_inject {
mi_inj:
mem_inj f m1 m2;
mi_freeblocks:
forall b, ~(
valid_block m1 b) ->
f b =
None;
mi_mappedblocks:
forall b b'
delta,
f b =
Some(
b',
delta) ->
valid_block m2 b';
mi_no_overlap:
meminj_no_overlap f m1;
mi_range_offset:
forall b b'
delta,
f b =
Some(
b',
delta) ->
0 <=
delta <=
Int.max_unsigned;
mi_range_block:
forall b b'
delta ofs k p,
f b =
Some(
b',
delta) ->
perm m2 b'
ofs k p ->
delta = 0 \/ 0 <=
ofs <=
Int.max_unsigned
}.
Definition inject :=
inject'.
Local Hint Resolve mi_mappedblocks mi_range_offset:
mem.
Preservation of access validity and pointer validity
Theorem valid_block_inject_1:
forall f m1 m2 b1 b2 delta,
f b1 =
Some(
b2,
delta) ->
inject f m1 m2 ->
valid_block m1 b1.
Proof.
Theorem valid_block_inject_2:
forall f m1 m2 b1 b2 delta,
f b1 =
Some(
b2,
delta) ->
inject f m1 m2 ->
valid_block m2 b2.
Proof.
Local Hint Resolve valid_block_inject_1 valid_block_inject_2:
mem.
Theorem perm_inject:
forall f m1 m2 b1 b2 delta ofs k p,
f b1 =
Some(
b2,
delta) ->
inject f m1 m2 ->
perm m1 b1 ofs k p ->
perm m2 b2 (
ofs +
delta)
k p.
Proof.
intros.
inv H0.
eapply perm_inj;
eauto.
Qed.
Theorem range_perm_inject:
forall f m1 m2 b1 b2 delta lo hi k p,
f b1 =
Some(
b2,
delta) ->
inject f m1 m2 ->
range_perm m1 b1 lo hi k p ->
range_perm m2 b2 (
lo +
delta) (
hi +
delta)
k p.
Proof.
Theorem valid_access_inject:
forall f m1 m2 chunk b1 ofs b2 delta p,
f b1 =
Some(
b2,
delta) ->
inject f m1 m2 ->
valid_access m1 chunk b1 ofs p ->
valid_access m2 chunk b2 (
ofs +
delta)
p.
Proof.
Theorem valid_pointer_inject:
forall f m1 m2 b1 ofs b2 delta,
f b1 =
Some(
b2,
delta) ->
inject f m1 m2 ->
valid_pointer m1 b1 ofs =
true ->
valid_pointer m2 b2 (
ofs +
delta) =
true.
Proof.
The following lemmas establish the absence of machine integer overflow
during address computations.
Lemma address_inject:
forall f m1 m2 b1 ofs1 b2 delta,
inject f m1 m2 ->
perm m1 b1 (
Int.unsigned ofs1)
Max Nonempty ->
f b1 =
Some (
b2,
delta) ->
Int.unsigned (
Int.add ofs1 (
Int.repr delta)) =
Int.unsigned ofs1 +
delta.
Proof.
Lemma address_inject':
forall f m1 m2 chunk b1 ofs1 b2 delta,
inject f m1 m2 ->
valid_access m1 chunk b1 (
Int.unsigned ofs1)
Nonempty ->
f b1 =
Some (
b2,
delta) ->
Int.unsigned (
Int.add ofs1 (
Int.repr delta)) =
Int.unsigned ofs1 +
delta.
Proof.
Theorem valid_pointer_inject_no_overflow:
forall f m1 m2 b ofs b'
x,
inject f m1 m2 ->
valid_pointer m1 b (
Int.unsigned ofs) =
true ->
f b =
Some(
b',
x) ->
0 <=
Int.unsigned ofs +
Int.unsigned (
Int.repr x) <=
Int.max_unsigned.
Proof.
Theorem valid_pointer_inject_val:
forall f m1 m2 b ofs b'
ofs',
inject f m1 m2 ->
valid_pointer m1 b (
Int.unsigned ofs) =
true ->
val_inject f (
Vptr b ofs) (
Vptr b'
ofs') ->
valid_pointer m2 b' (
Int.unsigned ofs') =
true.
Proof.
Theorem inject_no_overlap:
forall f m1 m2 b1 b2 b1'
b2'
delta1 delta2 ofs1 ofs2,
inject f m1 m2 ->
b1 <>
b2 ->
f b1 =
Some (
b1',
delta1) ->
f b2 =
Some (
b2',
delta2) ->
perm m1 b1 ofs1 Max Nonempty ->
perm m1 b2 ofs2 Max Nonempty ->
b1' <>
b2' \/
ofs1 +
delta1 <>
ofs2 +
delta2.
Proof.
intros. inv H. eapply mi_no_overlap0; eauto.
Qed.
Theorem different_pointers_inject:
forall f m m'
b1 ofs1 b2 ofs2 b1'
delta1 b2'
delta2,
inject f m m' ->
b1 <>
b2 ->
valid_pointer m b1 (
Int.unsigned ofs1) =
true ->
valid_pointer m b2 (
Int.unsigned ofs2) =
true ->
f b1 =
Some (
b1',
delta1) ->
f b2 =
Some (
b2',
delta2) ->
b1' <>
b2' \/
Int.unsigned (
Int.add ofs1 (
Int.repr delta1)) <>
Int.unsigned (
Int.add ofs2 (
Int.repr delta2)).
Proof.
Require Intv.
Theorem disjoint_or_equal_inject:
forall f m m'
b1 b1'
delta1 b2 b2'
delta2 ofs1 ofs2 sz,
inject f m m' ->
f b1 =
Some(
b1',
delta1) ->
f b2 =
Some(
b2',
delta2) ->
range_perm m b1 ofs1 (
ofs1 +
sz)
Max Nonempty ->
range_perm m b2 ofs2 (
ofs2 +
sz)
Max Nonempty ->
sz > 0 ->
b1 <>
b2 \/
ofs1 =
ofs2 \/
ofs1 +
sz <=
ofs2 \/
ofs2 +
sz <=
ofs1 ->
b1' <>
b2' \/
ofs1 +
delta1 =
ofs2 +
delta2
\/
ofs1 +
delta1 +
sz <=
ofs2 +
delta2
\/
ofs2 +
delta2 +
sz <=
ofs1 +
delta1.
Proof.
intros.
destruct (
eq_block b1 b2).
assert (
b1' =
b2')
by congruence.
assert (
delta1 =
delta2)
by congruence.
subst.
destruct H5.
congruence.
right.
destruct H5.
left;
congruence.
right.
omega.
destruct (
eq_block b1'
b2');
auto.
subst.
right.
right.
set (
i1 := (
ofs1 +
delta1,
ofs1 +
delta1 +
sz)).
set (
i2 := (
ofs2 +
delta2,
ofs2 +
delta2 +
sz)).
change (
snd i1 <=
fst i2 \/
snd i2 <=
fst i1).
apply Intv.range_disjoint';
simpl;
try omega.
unfold Intv.disjoint,
Intv.In;
simpl;
intros.
red;
intros.
exploit mi_no_overlap;
eauto.
instantiate (1 :=
x -
delta1).
apply H2.
omega.
instantiate (1 :=
x -
delta2).
apply H3.
omega.
unfold block;
omega.
Qed.
Theorem aligned_area_inject:
forall f m m'
b ofs al sz b'
delta,
inject f m m' ->
al = 1 \/
al = 2 \/
al = 4 ->
sz > 0 ->
(
al |
sz) ->
range_perm m b ofs (
ofs +
sz)
Cur Nonempty ->
(
al |
ofs) ->
f b =
Some(
b',
delta) ->
(
al |
ofs +
delta).
Proof.
Preservation of loads
Theorem load_inject:
forall f m1 m2 chunk b1 ofs b2 delta v1,
inject f m1 m2 ->
load chunk m1 b1 ofs =
Some v1 ->
f b1 =
Some (
b2,
delta) ->
exists v2,
load chunk m2 b2 (
ofs +
delta) =
Some v2 /\
val_inject f v1 v2.
Proof.
intros.
inv H.
eapply load_inj;
eauto.
Qed.
Theorem loadv_inject:
forall f m1 m2 chunk a1 a2 v1,
inject f m1 m2 ->
loadv chunk m1 a1 =
Some v1 ->
val_inject f a1 a2 ->
exists v2,
loadv chunk m2 a2 =
Some v2 /\
val_inject f v1 v2.
Proof.
intros.
inv H1;
simpl in H0;
try discriminate.
exploit load_inject;
eauto.
intros [
v2 [
LOAD INJ]].
exists v2;
split;
auto.
unfold loadv.
replace (
Int.unsigned (
Int.add ofs1 (
Int.repr delta)))
with (
Int.unsigned ofs1 +
delta).
auto.
symmetry.
eapply address_inject';
eauto with mem.
Qed.
Theorem loadbytes_inject:
forall f m1 m2 b1 ofs len b2 delta bytes1,
inject f m1 m2 ->
loadbytes m1 b1 ofs len =
Some bytes1 ->
f b1 =
Some (
b2,
delta) ->
exists bytes2,
loadbytes m2 b2 (
ofs +
delta)
len =
Some bytes2
/\
list_forall2 (
memval_inject f)
bytes1 bytes2.
Proof.
Preservation of stores
Theorem store_mapped_inject:
forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
inject f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
f b1 =
Some (
b2,
delta) ->
val_inject f v1 v2 ->
exists n2,
store chunk m2 b2 (
ofs +
delta)
v2 =
Some n2
/\
inject f n1 n2.
Proof.
intros.
inversion H.
exploit store_mapped_inj;
eauto.
intros [
n2 [
STORE MI]].
exists n2;
split.
eauto.
constructor.
auto.
eauto with mem.
eauto with mem.
red;
intros.
eauto with mem.
eauto.
eauto with mem.
Qed.
Theorem store_unmapped_inject:
forall f chunk m1 b1 ofs v1 n1 m2,
inject f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
f b1 =
None ->
inject f n1 m2.
Proof.
intros.
inversion H.
constructor.
eapply store_unmapped_inj;
eauto.
eauto with mem.
eauto with mem.
red;
intros.
eauto with mem.
eauto.
auto.
Qed.
Theorem store_outside_inject:
forall f m1 m2 chunk b ofs v m2',
inject f m1 m2 ->
(
forall b'
delta ofs',
f b' =
Some(
b,
delta) ->
perm m1 b'
ofs'
Cur Readable ->
ofs <=
ofs' +
delta <
ofs +
size_chunk chunk ->
False) ->
store chunk m2 b ofs v =
Some m2' ->
inject f m1 m2'.
Proof.
intros.
inversion H.
constructor.
eapply store_outside_inj;
eauto.
auto.
eauto with mem.
auto.
auto.
intros.
eauto with mem.
Qed.
Theorem storev_mapped_inject:
forall f chunk m1 a1 v1 n1 m2 a2 v2,
inject f m1 m2 ->
storev chunk m1 a1 v1 =
Some n1 ->
val_inject f a1 a2 ->
val_inject f v1 v2 ->
exists n2,
storev chunk m2 a2 v2 =
Some n2 /\
inject f n1 n2.
Proof.
Theorem storebytes_mapped_inject:
forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
inject f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
f b1 =
Some (
b2,
delta) ->
list_forall2 (
memval_inject f)
bytes1 bytes2 ->
exists n2,
storebytes m2 b2 (
ofs +
delta)
bytes2 =
Some n2
/\
inject f n1 n2.
Proof.
Theorem storebytes_unmapped_inject:
forall f m1 b1 ofs bytes1 n1 m2,
inject f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
f b1 =
None ->
inject f n1 m2.
Proof.
Theorem storebytes_outside_inject:
forall f m1 m2 b ofs bytes2 m2',
inject f m1 m2 ->
(
forall b'
delta ofs',
f b' =
Some(
b,
delta) ->
perm m1 b'
ofs'
Cur Readable ->
ofs <=
ofs' +
delta <
ofs +
Z_of_nat (
length bytes2) ->
False) ->
storebytes m2 b ofs bytes2 =
Some m2' ->
inject f m1 m2'.
Proof.
Theorem alloc_right_inject:
forall f m1 m2 lo hi b2 m2',
inject f m1 m2 ->
alloc m2 lo hi = (
m2',
b2) ->
inject f m1 m2'.
Proof.
Theorem alloc_left_unmapped_inject:
forall f m1 m2 lo hi m1'
b1,
inject f m1 m2 ->
alloc m1 lo hi = (
m1',
b1) ->
exists f',
inject f'
m1'
m2
/\
inject_incr f f'
/\
f'
b1 =
None
/\ (
forall b,
b <>
b1 ->
f'
b =
f b).
Proof.
intros.
inversion H.
set (
f' :=
fun b =>
if zeq b b1 then None else f b).
assert (
inject_incr f f').
red;
unfold f';
intros.
destruct (
zeq b b1).
subst b.
assert (
f b1 =
None).
eauto with mem.
congruence.
auto.
assert (
mem_inj f'
m1 m2).
inversion mi_inj0;
constructor;
eauto with mem.
unfold f';
intros.
destruct (
zeq b0 b1).
congruence.
eauto.
unfold f';
intros.
destruct (
zeq b0 b1).
congruence.
eauto.
unfold f';
intros.
destruct (
zeq b0 b1).
congruence.
apply memval_inject_incr with f;
auto.
exists f';
split.
constructor.
eapply alloc_left_unmapped_inj;
eauto.
unfold f';
apply zeq_true.
intros.
unfold f'.
destruct (
zeq b b1).
auto.
apply mi_freeblocks0.
red;
intro;
elim H3.
eauto with mem.
unfold f';
intros.
destruct (
zeq b b1).
congruence.
eauto.
unfold f';
red;
intros.
destruct (
zeq b0 b1);
destruct (
zeq b2 b1);
try congruence.
eapply mi_no_overlap0.
eexact H3.
eauto.
eauto.
exploit perm_alloc_inv.
eauto.
eexact H6.
rewrite zeq_false;
auto.
exploit perm_alloc_inv.
eauto.
eexact H7.
rewrite zeq_false;
auto.
unfold f';
intros.
destruct (
zeq b b1).
congruence.
eauto.
unfold f';
intros.
destruct (
zeq b b1).
congruence.
eauto.
split.
auto.
split.
unfold f';
apply zeq_true.
intros;
unfold f';
apply zeq_false;
auto.
Qed.
Theorem alloc_left_mapped_inject:
forall f m1 m2 lo hi m1'
b1 b2 delta,
inject f m1 m2 ->
alloc m1 lo hi = (
m1',
b1) ->
valid_block m2 b2 ->
0 <=
delta <=
Int.max_unsigned ->
(
forall ofs k p,
perm m2 b2 ofs k p ->
delta = 0 \/ 0 <=
ofs <=
Int.max_unsigned) ->
(
forall ofs k p,
lo <=
ofs <
hi ->
perm m2 b2 (
ofs +
delta)
k p) ->
inj_offset_aligned delta (
hi-
lo) ->
(
forall b delta'
ofs k p,
f b =
Some (
b2,
delta') ->
perm m1 b ofs k p ->
lo +
delta <=
ofs +
delta' <
hi +
delta ->
False) ->
exists f',
inject f'
m1'
m2
/\
inject_incr f f'
/\
f'
b1 =
Some(
b2,
delta)
/\ (
forall b,
b <>
b1 ->
f'
b =
f b).
Proof.
intros.
inversion H.
set (
f' :=
fun b =>
if zeq b b1 then Some(
b2,
delta)
else f b).
assert (
inject_incr f f').
red;
unfold f';
intros.
destruct (
zeq b b1).
subst b.
assert (
f b1 =
None).
eauto with mem.
congruence.
auto.
assert (
mem_inj f'
m1 m2).
inversion mi_inj0;
constructor;
eauto with mem.
unfold f';
intros.
destruct (
zeq b0 b1).
inversion H8.
subst b0 b3 delta0.
elim (
fresh_block_alloc _ _ _ _ _ H0).
eauto with mem.
eauto.
unfold f';
intros.
destruct (
zeq b0 b1).
inversion H8.
subst b0 b3 delta0.
elim (
fresh_block_alloc _ _ _ _ _ H0).
eauto with mem.
eauto.
unfold f';
intros.
destruct (
zeq b0 b1).
inversion H8.
subst b0 b3 delta0.
elim (
fresh_block_alloc _ _ _ _ _ H0).
eauto with mem.
apply memval_inject_incr with f;
auto.
exists f'.
split.
constructor.
eapply alloc_left_mapped_inj;
eauto.
unfold f';
apply zeq_true.
unfold f';
intros.
destruct (
zeq b b1).
subst b.
elim H9.
eauto with mem.
eauto with mem.
unfold f';
intros.
destruct (
zeq b b1).
congruence.
eauto.
unfold f';
red;
intros.
exploit perm_alloc_inv.
eauto.
eexact H12.
intros P1.
exploit perm_alloc_inv.
eauto.
eexact H13.
intros P2.
destruct (
zeq b0 b1);
destruct (
zeq b3 b1).
congruence.
inversion H10;
subst b0 b1'
delta1.
destruct (
zeq b2 b2');
auto.
subst b2'.
right;
red;
intros.
eapply H6;
eauto.
omega.
inversion H11;
subst b3 b2'
delta2.
destruct (
zeq b1'
b2);
auto.
subst b1'.
right;
red;
intros.
eapply H6;
eauto.
omega.
eauto.
unfold f';
intros.
destruct (
zeq b b1).
congruence.
eauto.
unfold f';
intros.
destruct (
zeq b b1).
inversion H9;
subst b b'
delta0.
eauto.
eauto.
split.
auto.
split.
unfold f';
apply zeq_true.
intros.
unfold f';
apply zeq_false;
auto.
Qed.
Theorem alloc_parallel_inject:
forall f m1 m2 lo1 hi1 m1'
b1 lo2 hi2,
inject f m1 m2 ->
alloc m1 lo1 hi1 = (
m1',
b1) ->
lo2 <=
lo1 ->
hi1 <=
hi2 ->
exists f',
exists m2',
exists b2,
alloc m2 lo2 hi2 = (
m2',
b2)
/\
inject f'
m1'
m2'
/\
inject_incr f f'
/\
f'
b1 =
Some(
b2, 0)
/\ (
forall b,
b <>
b1 ->
f'
b =
f b).
Proof.
Preservation of free operations
Lemma free_left_inject:
forall f m1 m2 b lo hi m1',
inject f m1 m2 ->
free m1 b lo hi =
Some m1' ->
inject f m1'
m2.
Proof.
intros.
inversion H.
constructor.
eapply free_left_inj;
eauto.
eauto with mem.
auto.
red;
intros.
eauto with mem.
auto.
auto.
Qed.
Lemma free_list_left_inject:
forall f m2 l m1 m1',
inject f m1 m2 ->
free_list m1 l =
Some m1' ->
inject f m1'
m2.
Proof.
induction l;
simpl;
intros.
inv H0.
auto.
destruct a as [[
b lo]
hi].
generalize H0.
case_eq (
free m1 b lo hi);
intros.
apply IHl with m;
auto.
eapply free_left_inject;
eauto.
congruence.
Qed.
Lemma free_right_inject:
forall f m1 m2 b lo hi m2',
inject f m1 m2 ->
free m2 b lo hi =
Some m2' ->
(
forall b1 delta ofs k p,
f b1 =
Some(
b,
delta) ->
perm m1 b1 ofs k p ->
lo <=
ofs +
delta <
hi ->
False) ->
inject f m1 m2'.
Proof.
intros.
inversion H.
constructor.
eapply free_right_inj;
eauto.
auto.
eauto with mem.
auto.
auto.
intros.
eauto with mem.
Qed.
Lemma perm_free_list:
forall l m m'
b ofs k p,
free_list m l =
Some m' ->
perm m'
b ofs k p ->
perm m b ofs k p /\
(
forall lo hi,
In (
b,
lo,
hi)
l ->
lo <=
ofs <
hi ->
False).
Proof.
induction l;
intros until p;
simpl.
intros.
inv H.
split;
auto.
destruct a as [[
b1 lo1]
hi1].
case_eq (
free m b1 lo1 hi1);
intros;
try congruence.
exploit IHl;
eauto.
intros [
A B].
split.
eauto with mem.
intros.
destruct H2.
inv H2.
elim (
perm_free_2 _ _ _ _ _ H ofs k p).
auto.
auto.
eauto.
Qed.
Theorem free_inject:
forall f m1 l m1'
m2 b lo hi m2',
inject f m1 m2 ->
free_list m1 l =
Some m1' ->
free m2 b lo hi =
Some m2' ->
(
forall b1 delta ofs k p,
f b1 =
Some(
b,
delta) ->
perm m1 b1 ofs k p ->
lo <=
ofs +
delta <
hi ->
exists lo1,
exists hi1,
In (
b1,
lo1,
hi1)
l /\
lo1 <=
ofs <
hi1) ->
inject f m1'
m2'.
Proof.
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' ->
(
forall b'
delta ofs k p,
f b' =
Some(
b,
delta) ->
perm m1 b'
ofs k p ->
lo <=
ofs +
delta <
hi ->
False) ->
inject f m1 m2'.
Proof.
intros.
destruct H.
constructor;
eauto.
eapply drop_outside_inj;
eauto.
intros.
unfold valid_block in *.
erewrite nextblock_drop;
eauto.
intros.
eapply mi_range_block0;
eauto.
eapply perm_drop_4;
eauto.
Qed.
Injecting a memory into itself.
Definition flat_inj (
thr:
block) :
meminj :=
fun (
b:
block) =>
if zlt b thr then Some(
b, 0)
else None.
Definition inject_neutral (
thr:
block) (
m:
mem) :=
mem_inj (
flat_inj thr)
m m.
Remark flat_inj_no_overlap:
forall thr m,
meminj_no_overlap (
flat_inj thr)
m.
Proof.
unfold flat_inj;
intros;
red;
intros.
destruct (
zlt b1 thr);
inversion H0;
subst.
destruct (
zlt b2 thr);
inversion H1;
subst.
auto.
Qed.
Theorem neutral_inject:
forall m,
inject_neutral (
nextblock m)
m ->
inject (
flat_inj (
nextblock m))
m m.
Proof.
intros.
constructor.
auto.
unfold flat_inj,
valid_block;
intros.
apply zlt_false.
omega.
unfold flat_inj,
valid_block;
intros.
destruct (
zlt b (
nextblock m));
inversion H0;
subst.
auto.
apply flat_inj_no_overlap.
unfold flat_inj;
intros.
destruct (
zlt b (
nextblock m));
inv H0.
unfold Int.max_unsigned.
generalize Int.modulus_pos;
omega.
unfold flat_inj;
intros.
destruct (
zlt b (
nextblock m));
inv H0.
auto.
Qed.
Theorem empty_inject_neutral:
forall thr,
inject_neutral thr empty.
Proof.
intros;
red;
constructor.
unfold flat_inj;
intros.
destruct (
zlt b1 thr);
inv H.
replace (
ofs + 0)
with ofs by omega;
auto.
unfold flat_inj;
intros.
destruct (
zlt b1 thr);
inv H.
replace (
ofs + 0)
with ofs by omega;
auto.
intros;
simpl.
repeat rewrite ZMap.gi.
constructor.
Qed.
Theorem alloc_inject_neutral:
forall thr m lo hi b m',
alloc m lo hi = (
m',
b) ->
inject_neutral thr m ->
nextblock m <
thr ->
inject_neutral thr m'.
Proof.
Theorem store_inject_neutral:
forall chunk m b ofs v m'
thr,
store chunk m b ofs v =
Some m' ->
inject_neutral thr m ->
b <
thr ->
val_inject (
flat_inj thr)
v v ->
inject_neutral thr m'.
Proof.
Theorem drop_inject_neutral:
forall m b lo hi p m'
thr,
drop_perm m b lo hi p =
Some m' ->
inject_neutral thr m ->
b <
thr ->
inject_neutral thr m'.
Proof.
End Mem.
Notation mem :=
Mem.mem.
Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes.
Hint Resolve
Mem.valid_not_valid_diff
Mem.perm_implies
Mem.perm_cur
Mem.perm_max
Mem.perm_valid_block
Mem.range_perm_implies
Mem.range_perm_cur
Mem.range_perm_max
Mem.valid_access_implies
Mem.valid_access_valid_block
Mem.valid_access_perm
Mem.valid_access_load
Mem.load_valid_access
Mem.loadbytes_range_perm
Mem.valid_access_store
Mem.perm_store_1
Mem.perm_store_2
Mem.nextblock_store
Mem.store_valid_block_1
Mem.store_valid_block_2
Mem.store_valid_access_1
Mem.store_valid_access_2
Mem.store_valid_access_3
Mem.storebytes_range_perm
Mem.perm_storebytes_1
Mem.perm_storebytes_2
Mem.storebytes_valid_access_1
Mem.storebytes_valid_access_2
Mem.nextblock_storebytes
Mem.storebytes_valid_block_1
Mem.storebytes_valid_block_2
Mem.nextblock_alloc
Mem.alloc_result
Mem.valid_block_alloc
Mem.fresh_block_alloc
Mem.valid_new_block
Mem.perm_alloc_1
Mem.perm_alloc_2
Mem.perm_alloc_3
Mem.perm_alloc_4
Mem.perm_alloc_inv
Mem.valid_access_alloc_other
Mem.valid_access_alloc_same
Mem.valid_access_alloc_inv
Mem.range_perm_free
Mem.free_range_perm
Mem.nextblock_free
Mem.valid_block_free_1
Mem.valid_block_free_2
Mem.perm_free_1
Mem.perm_free_2
Mem.perm_free_3
Mem.valid_access_free_1
Mem.valid_access_free_2
Mem.valid_access_free_inv_1
Mem.valid_access_free_inv_2
:
mem.