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 Zwf.
Require Import Axioms.
Require Import Coqlib.
Require Intv.
Require Import Maps.
Require Archi.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Export Memtype.
Require Import IntFacts.
Require Import Normalise.
Require Import NormaliseSpec.
Require Export Memdata.
Require Import Alloc.
Require Import Permutation.
Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.
Local Notation "
a #
b" := (
PMap.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:
PMap.t (
ZMap.t memval);
(* block -> offset -> memval *)
mem_access:
PMap.t (
Z ->
perm_kind ->
option permission);
mem_blocksize:
PMap.t (
option (
Z*
Z));
mem_mask:
PMap.t (
option nat);
(* block -> option mask; the number of 0-trailing-bits *)
nextblock:
block;
access_max:
forall b ofs,
perm_order'' (
mem_access#
b ofs Max) (
mem_access#
b ofs Cur);
nextblock_noaccess:
forall b ofs k, ~(
Plt b nextblock) ->
mem_access#
b ofs k =
None;
contents_wt_memval:
forall b ofs,
wt_memval (
ZMap.get ofs (
mem_contents #
b));
access_bounds_ok:
(* permissions and bounds agree *)
forall b ofs k,
(
mem_access#
b ofs k) <>
None
->
in_bound ofs (
get_bounds mem_blocksize b);
bs_valid:
(* only valid blocks have non-empty bounds *)
forall b, ~ (
Plt b nextblock) ->
mem_blocksize#
b =
None;
msk_valid:
(* only valid blocks have non-empty masks *)
forall b, ~ (
Plt b nextblock) ->
mem_mask#
b =
None;
wfm_alloc_ok:
(* the allocation algorithm succeeds on this memory *)
alloc_blocks
(
mk_block_list_aux (
get_size ((
mem_blocksize)))
(
pred (
Pos.to_nat nextblock))) <>
None;
alignment_ok:
(* the alignment agrees with the bounds of blocks *)
forall b al,
mem_mask#
b =
Some al ->
al =
alignment_of_size (
get_size (
mem_blocksize)
b);
bounds_mask_consistency:
(* bounds and masks information are present together, or not at all *)
forall b,
(
mem_mask#
b =
None /\
mem_blocksize#
b =
None) \/
(
mem_mask#
b <>
None /\
mem_blocksize#
b <>
None);
bounds_lo_inf0:
(* the lower bound of a block is 0 *)
forall b lo hi,
mem_blocksize#
b =
Some (
lo,
hi) ->
lo = 0
}.
Definition mem :=
mem'.
Definition size_block (
m:
mem) (
b:
block) :
Z :=
get_size (
m.(
mem_blocksize))
b.
Definition size_of_block (
m:
mem) (
b:
block) :=
match PMap.get b m.(
mem_blocksize)
with
|
Some (
lo,
hi) => (
Int.repr (
hi-
lo))
|
None => (
Int.repr 0)
end.
Definition bounds_of_block (
m:
mem) (
b:
block) :
Z*
Z :=
match PMap.get b m.(
mem_blocksize)
with
|
Some (
lo,
hi) => (
lo,
hi)
|
None => (0,0)
end.
Definition mask (
m:
mem) (
b:
block) :=
match PMap.get b m.(
mem_mask)
with
|
Some mask =>
mask
|
None =>
O
end.
The mask of a block is
Definition nat_mask (
m:
mem) (
b:
block) :=
Int.not (
Int.repr (
two_power_nat (
mask m b) - 1)).
Definition mk_block_list (
m:
mem) : (
list (
block *
Z)) :=
mk_block_list_aux (
size_block m) (
pred (
Pos.to_nat (
Mem.nextblock m))).
alloc_mem computes a concrete memory for memory m. size_mem is the
first available address after the allocation of m.
Definition size_mem (
m:
mem) :
Z :=
size_mem_aux (
mk_block_list m).
Definition alloc_mem (
m:
mem) :
option (
block ->
int) :=
alloc_blocks (
mk_block_list m).
Normalisation in a given memory. This is what is called normalise in the
paper.
Definition mem_norm (
m:
mem) (
e:
expr_sym) (
r:
result) :
val :=
Normalise.normalise (
bounds_of_block m) (
nat_mask m)
e r.
Lemma mkmem_ext:
forall cont1 cont2 acc1 acc2 next1 next2
a1 a2 b1 b2 c1 c2 bs1 bs2
mask1 mask2 Pabo1 Pabo2 comp2 comp1 vbs1 vbs2 vm1 vm2
const1 const2 bb1 bb2
bli1 bli2,
cont1=
cont2 ->
acc1=
acc2 ->
next1=
next2 ->
bs1=
bs2 ->
mask1=
mask2 ->
mkmem cont1 acc1 bs1 mask1 next1
a1 b1 c1 Pabo1 vbs1 vm1
comp1 bb1 const1 bli1 =
mkmem cont2 acc2 bs2 mask2 next2
a2 b2 c2 Pabo2 vbs2 vm2
comp2 bb2 const2 bli2.
Proof.
Lemma alloc_compat:
forall m,
exists al,
alloc_mem m =
Some al /\
compat al (
bounds_of_block m) (
nat_mask m).
Proof.
Lemma concrete_mem:
forall m,
exists al,
compat al (
bounds_of_block m) (
nat_mask m).
Proof.
intros.
destruct (
alloc_compat m)
as [
al [
A B]];
exists al;
auto.
Qed.
Lemma alloc_permut:
forall l l',
Permutation l l' ->
(
alloc_blocks l =
None <->
alloc_blocks l' =
None).
Proof.
Lemma norm_ptr_same_eval:
forall m l b o
(
MN :
Mem.mem_norm m (
Eval (
Eptr l Int.zero))
Ptr =
Vptr b o)
(
NIB : ~
NormaliseSpec.in_bound 0 (
Mem.bounds_of_block m l)),
False.
Proof.
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) :=
Plt b (
nextblock m).
Definition valid_block_dec (
m:
mem) (
b:
block) : {
valid_block m b} + {~
valid_block m b}.
Proof.
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).
Defined.
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.
Defined.
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.
Defined.
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.
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.
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.
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.
induction lo using (
well_founded_induction_type (
Zwf_up_well_founded hi)).
destruct (
zlt lo hi).
destruct (
perm_dec m b lo k p).
destruct (
H (
lo + 1)).
red.
omega.
left;
red;
intros.
destruct (
zeq lo ofs).
congruence.
apply r.
omega.
right;
red;
intros.
elim n.
red;
intros;
apply H0;
omega.
right;
red;
intros.
elim n.
apply H0.
omega.
left;
red;
intros.
omegaContradiction.
Defined.
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 ->
align_chunk chunk2 <=
align_chunk chunk1 ->
valid_access m chunk1 b ofs p->
valid_access m chunk2 b ofs p.
Proof.
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 m b ofs returns true if the address b, ofs
is nonempty in m and false if it is empty.
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.
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.
C allows pointers one past the last element of an array. These are not
valid according to the previously defined valid_pointer. The property
weak_valid_pointer m b ofs holds if address b, ofs is a valid pointer
in m, or a pointer one past a valid block in m.
Definition weak_valid_pointer (
m:
mem) (
b:
block) (
ofs:
Z) :=
valid_pointer m b ofs ||
valid_pointer m b (
ofs - 1).
Lemma weak_valid_pointer_spec:
forall m b ofs,
weak_valid_pointer m b ofs =
true <->
valid_pointer m b ofs =
true \/
valid_pointer m b (
ofs - 1) =
true.
Proof.
Lemma valid_pointer_implies:
forall m b ofs,
valid_pointer m b ofs =
true ->
weak_valid_pointer m b ofs =
true.
Proof.
Operations over memory stores
The initial store
Program Definition empty:
mem :=
mkmem (
PMap.init (
ZMap.init (
Symbolic (
Eval (
Eint Int.zero))
O)))
(
PMap.init (
fun ofs k =>
None))
(
PMap.init (
None))
(
PMap.init None)
2%
positive _ _ _ _ _ _ _ _ _ _.
Next Obligation.
repeat rewrite PMap.gi.
red;
auto.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
repeat rewrite PMap.gi in H.
congruence.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
rewrite PMap.gi in H.
congruence.
Qed.
Next Obligation.
left.
rewrite !
PMap.gi.
tauto.
Qed.
Next Obligation.
rewrite PMap.gi in H.
congruence.
Qed.
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' =>
ZMap.get p c ::
getN n' (
p + 1)
c
end.
Lemma getN_Nlist :
forall n p c,
length (
getN n p c) =
n.
Proof.
induction n.
intros; reflexivity.
intros.
simpl.
rewrite IHn.
reflexivity.
Qed.
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) ->
ZMap.get q (
setN vl p c) =
ZMap.get q c.
Proof.
Remark setN_outside:
forall vl c p q,
q <
p \/
q >=
p +
Z_of_nat (
length vl) ->
ZMap.get q (
setN vl p c) =
ZMap.get q c.
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 ->
ZMap.get i c1 =
ZMap.get i c2) ->
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_disjoint:
forall vl q c n p,
Intv.disjoint (
p,
p +
Z_of_nat n) (
q,
q +
Z_of_nat (
length vl)) ->
getN n p (
setN vl q c) =
getN n p c.
Proof.
intros.
apply getN_exten.
intros.
apply setN_other.
intros;
red;
intros;
subst r.
eelim H;
eauto.
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.
Remark setN_default:
forall vl q c,
fst (
setN vl q c) =
fst c.
Proof.
induction vl; simpl; intros. auto. rewrite IHvl. auto.
Qed.
We initialise the memory of allocated blocks with the appropriate Eundef values.
Fixpoint init_block' (
n:
nat) (
b:
block) (
cur:
int) :
list memval :=
match n with
O =>
Symbolic (
Eval (
Eundef b cur))
O ::
nil
|
S m =>
Symbolic (
Eval (
Eundef b cur))
O :: (
init_block'
m b (
Int.add cur (
Int.repr 1)))
end.
Definition init_block (
lo hi:
Z) (
b:
block) :
memval *
PTree.t memval :=
let sz :=
hi -
lo in
if zlt sz 0
then (
ZMap.init (
Symbolic (
Eval (
Eint Int.zero))
O))
else setN (
init_block' (
Z.to_nat sz)
b (
Int.repr lo))
lo (
ZMap.init (
Symbolic (
Eval (
Eint Int.zero))
O)).
Lemma init_block'
_wt_memval:
forall n b cur,
Forall wt_memval (
init_block'
n b cur).
Proof.
induction n; simpl; intuition try congruence.
constructor; try constructor.
simpl; eexists; intuition try constructor.
constructor.
simpl; eexists; intuition try constructor.
apply IHn.
Qed.
Lemma init_block_wt_memval:
forall lo hi cur ofs,
wt_memval (
ZMap.get ofs ( (
init_block lo hi cur))).
Proof.
Lemma pos_ex_index:
forall p,
exists z,
ZIndexed.index z =
p.
Proof.
Lemma init_block_wt_memval':
forall lo hi cur ofs,
wt_memval ((
init_block lo hi cur) #
ofs).
Proof.
Lemma zle_zlt:
forall a b c,
zle a b &&
zlt b c =
true <->
a <=
b <
c.
Proof.
unfold zle,
zlt.
intros.
destruct (
Z_le_gt_dec a b).
destruct (
Z_lt_dec b c).
intuition omega.
split;
try discriminate;
try omega.
split;
try discriminate;
try omega.
Qed.
Run the allocation algorithm on m plus an hypothetical new block.
Definition conc_mem_alloc (
m:
mem) (
lo hi :
Z) (
alignment:
nat) :
option (
block ->
int) :=
alloc_blocks
(
mk_block_list_aux
(
get_size
(
PMap.set (
nextblock m) (
Some (0,
hi)) (
mem_blocksize m)))
(
Pos.to_nat (
nextblock m))).
Definition alloc_mem_dec:
forall l ,
{
alloc_blocks l <>
None} + {
alloc_blocks l =
None}.
Proof.
Definition conc_mem_alloc_dec (
m:
mem) (
lo hi:
Z) (
alignment:
nat) :
{
conc_mem_alloc m lo hi alignment <>
None} +
{
conc_mem_alloc m lo hi alignment =
None}.
Proof.
The allocation is now guarded by the success of conc_mem_alloc.
Program Definition low_alloc (
m:
mem) (
lo hi:
Z) :
option (
mem *
block) :=
let lo := 0
in
let al :=
alignment_of_size (
hi-
lo)
in
if conc_mem_alloc_dec m lo hi al
then
Some (
mkmem (
PMap.set m.(
nextblock)
(
init_block lo hi m.(
nextblock))
m.(
mem_contents))
(
PMap.set m.(
nextblock)
(
fun ofs k =>
if zle lo ofs &&
zlt ofs hi then Some Freeable else None)
m.(
mem_access))
(
PMap.set m.(
nextblock)
(
Some (0,
hi))
m.(
mem_blocksize))
(
PMap.set m.(
nextblock)
(
Some al)
m.(
mem_mask))
(
Psucc m.(
nextblock))
_ _ _ _ _ _ _ _ _ _,
m.(
nextblock))
else None.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Definition alloc (
m:
mem) (
lo hi:
Z) :=
low_alloc m lo hi.
Lemma alloc_nat_mask:
forall m lo hi m'
b,
Mem.alloc m lo hi =
Some (
m',
b) ->
Mem.nat_mask m'
b =
Int.not (
Int.repr (
two_power_nat (
alignment_of_size hi) - 1)).
Proof.
Lemma alloc_contents:
forall m lo hi m'
b,
alloc m lo hi =
Some (
m',
b) ->
forall b',
b <>
b' ->
(
mem_contents m') !!
b' = (
mem_contents m) !!
b'.
Proof.
Freeing a block between the given bounds.
We only free the block when lo and hi corresponds to the exact bounds of b.
Opaque zeq.
Program Definition unchecked_free (
m:
mem) (
b:
block) (
lo hi:
Z):
mem :=
mkmem m.(
mem_contents)
(
PMap.set b
(
fun ofs k =>
if zle lo ofs &&
zlt ofs hi then None else m.(
mem_access)#
b ofs k)
m.(
mem_access))
(
PMap.set b (
match m.(
mem_blocksize)#
b with
Some (
l,
h) =>
if zeq l lo &&
zeq h hi then
None
else m.(
mem_blocksize)#
b
|
None =>
None
end)
m.(
mem_blocksize))
(
PMap.set b (
match m.(
mem_blocksize)#
b with
Some (
l,
h) =>
if zeq l lo &&
zeq h hi
then None
else m.(
mem_mask)#
b
|
None =>
None
end)
m.(
mem_mask))
m.(
nextblock)
_ _ _ _ _ _ _ _ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
unfold get_bounds in *.
repeat rewrite PMap.gsspec in *.
destruct (
peq b0 b).
subst.
destruct (
zle lo ofs &&
zlt ofs hi)
eqn:?;
try intuition congruence.
-
generalize H;
intro H1.
apply access_bounds_ok in H;
auto.
revert H;
destr.
des p.
revert Heqo;
destr.
des p.
revert Heqo0;
destr.
inv Heqo0.
unfold in_bound,
get_bounds in *.
simpl in *.
rewrite Heqo in H.
simpl in *.
auto.
revert Heqo;
destr.
des p.
revert Heqo0;
destr.
inv Heqo0.
unfold in_bound,
get_bounds in *.
simpl in *.
rewrite Heqo in H.
simpl in *.
auto.
cut (
z =
lo /\
z0 =
hi).
intros [
A B];
subst.
apply zle_zlt in H.
congruence.
apply andb_true_iff in Heqb1.
destruct Heqb1;
split.
destruct (
zeq z lo);
intuition try congruence.
discriminate.
destruct (
zeq z0 hi);
intuition try congruence.
discriminate.
unfold get_bounds,
in_bound in H.
rewrite Heqo in H.
simpl in H;
omega.
-
eapply access_bounds_ok;
eauto.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Lemma unchecked_free_mask:
forall m b lo hi b',
mask (
unchecked_free m b lo hi)
b' =
if eq_block b'
b
then match bounds_of_block m b with
(
lo',
hi') =>
(
if zeq lo'
lo &&
zeq hi'
hi
then O
else mask m b')
end
else mask m b'.
Proof.
Lemma unchecked_free_nat_mask:
forall m b lo hi b',
nat_mask (
unchecked_free m b lo hi)
b' =
if eq_block b'
b
then match bounds_of_block m b with
(
lo',
hi') =>
if zeq lo'
lo &&
zeq hi'
hi
then Int.mone
else nat_mask m b'
end
else nat_mask m b'.
Proof.
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.
Lemma bounds_of_block_valid:
forall m b lo hi,
bounds_of_block m b = (
lo,
hi) ->
lo <>
hi ->
valid_block m b.
Proof.
Lemma size_mem_aux_sup1:
forall m,
Alloc.size_mem_aux m >= 8.
Proof.
Lemma size_mem_sup1:
forall m,
Mem.size_mem m >= 8.
Proof.
Memory reads.
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 expr_sym :=
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.
We normalise the address beforehand.
Definition loadv (
chunk:
memory_chunk) (
m:
mem) (
addr:
expr_sym) :
option expr_sym :=
let v :=
mem_norm m addr Values_symbolictype.Ptr
in match v 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.
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 optForall {
A}
P (
l:
option (
list A)) :=
match l with
Some ll =>
Forall P ll
|
None =>
True
end.
Lemma encode_val_wt':
forall c v,
optForall wt_memval (
encode_val c v).
Proof.
Lemma wt_memval_setN:
forall l t ofs ofs0,
Forall wt_memval l ->
(
forall o,
wt_memval (
ZMap.get o t)) ->
wt_memval (
ZMap.get ofs0 (
setN l ofs t)).
Proof.
induction l;
simpl;
intuition try congruence.
-
apply H0.
-
apply IHl.
inv H;
auto.
intros.
rewrite ZMap.gsspec.
destr;
subst.
inv H;
auto.
apply H0.
Qed.
Definition is_encodable chunk v :=
match encode_val chunk v with
Some enc =>
true
|
None =>
false
end.
Definition encode_val_tot chunk v :=
match encode_val chunk v with
Some enc =>
enc
|
_ =>
nil
end.
Program Definition store (
chunk:
memory_chunk) (
m:
mem) (
b:
block) (
ofs:
Z) (
v:
expr_sym):
option mem :=
if valid_access_dec m chunk b ofs Writable then
if is_encodable chunk v then
Some (
mkmem (
PMap.set b
(
setN (
encode_val_tot chunk v)
ofs (
m.(
mem_contents)#
b))
m.(
mem_contents))
m.(
mem_access)
m.(
mem_blocksize)
m.(
mem_mask)
m.(
nextblock)
_ _ _ _ _ _ _ _ _ _)
else None
else
None.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. eauto.
Qed.
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. We normalise the address beforehand.
Definition storev (
chunk:
memory_chunk) (
m:
mem) (
addr v:
expr_sym) :
option mem :=
match mem_norm m addr Values_symbolictype.Ptr with
Vptr b ofs =>
store chunk m b (
Int.unsigned ofs)
v
|
_ =>
None
end.
Lemma check_bytes_correct:
forall l,
check_bytes l =
true ->
Forall wt_memval l.
Proof.
induction l;
simpl;
intuition try congruence.
-
constructor.
-
constructor.
destruct a;
simpl;
auto.
apply andb_true_iff in H.
destruct (
tcheck_expr e)
eqn:?;
simpl in *;
intuition try congruence.
apply mk_lexpr with (
l_styp:=
s);
auto.
des s;
constructor.
des a.
apply andb_true_iff in H.
intuition eauto.
Qed.
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.
Program Definition storebytes (
m:
mem) (
b:
block) (
ofs:
Z) (
bytes:
list memval) :
option mem :=
if bool_dec (
check_bytes bytes)
true then
if range_perm_dec m b ofs (
ofs +
Z_of_nat (
length bytes))
Cur Writable then
Some (
mkmem
(
PMap.set b (
setN bytes ofs (
m.(
mem_contents)#
b))
m.(
mem_contents))
m.(
mem_access)
m.(
mem_blocksize)
m.(
mem_mask)
m.(
nextblock)
_ _ _ _ _ _ _ _ _ _)
else None
else
None.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl in *. eauto.
Qed.
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)
(
PMap.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.(
mem_blocksize)
m.(
mem_mask)
m.(
nextblock)
_ _ _ _ _ _ _ _ _ _)
else None.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl. auto.
Qed.
Next Obligation.
destruct m. simpl in *. eauto.
Qed.
Properties of the memory operations
Properties of the empty store.
Theorem nextblock_empty:
nextblock empty = 2%
positive.
Proof.
reflexivity. Qed.
Theorem perm_empty:
forall b ofs k p, ~
perm empty b ofs k p.
Proof.
Theorem valid_access_empty:
forall chunk b ofs p, ~
valid_access empty chunk b ofs p.
Proof.
Properties related to load
Lemma Forall_rib:
forall {
A} (
P :
A ->
Prop)
l,
Forall P l ->
Forall P (
rev_if_be l).
Proof.
Lemma wt_memval_getN:
forall n b ofs,
(
forall o,
wt_memval (
ZMap.get o b) ) ->
Forall wt_memval (
getN n ofs b).
Proof.
induction n; simpl; auto.
Qed.
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.
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
|
_ =>
True
end.
Proof.
Lemma ps_int8_signed_unsigned:
forall l,
proj_symbolic_le l Mint8signed =
proj_symbolic_le l Mint8unsigned.
Proof.
unfold proj_symbolic_le.
intros;
repeat destr_cond_match;
intuition try congruence.
Qed.
Lemma ps_int16_signed_unsigned:
forall l,
proj_symbolic_le l Mint16signed =
proj_symbolic_le l Mint16unsigned.
Proof.
unfold proj_symbolic_le.
intros;
repeat destr_cond_match;
intuition try congruence.
Qed.
Theorem load_int8_signed_unsigned:
forall m b ofs v1 v2,
load Mint8signed m b ofs =
Some v1 ->
option_map (
Val.sign_ext 8) (
load Mint8unsigned m b ofs) =
Some v2 ->
v1 ==
v2.
Proof.
Theorem load_int8_signed_unsigned_none:
forall m b ofs,
load Mint8signed m b ofs =
None ->
load Mint8unsigned m b ofs =
None.
Proof.
Theorem load_int16_signed_unsigned:
forall m b ofs v1 v2,
load Mint16signed m b ofs =
Some v1 ->
option_map (
Val.sign_ext 16) (
load Mint16unsigned m b ofs) =
Some v2 ->
v1 ==
v2.
Proof.
Theorem load_int16_signed_unsigned_none:
forall m b ofs,
load Mint16signed m b ofs =
None ->
load Mint16unsigned m b ofs =
None.
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.
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.
Lemma Forall_dec:
forall {
A} (
P:
A ->
Prop)
(
Pdec:
forall a,
P a \/ ~
P a)
l,
Forall P l \/ ~
Forall P l.
Proof.
induction l; simpl; intros.
left; constructor.
destruct (Pdec a); destruct IHl; intuition try congruence.
left; constructor; auto.
right; intro C; inv C; congruence.
right; intro C; inv C; congruence.
right; intro C; inv C; congruence.
Qed.
Lemma wt_memval_dec:
forall a,
wt_memval a \/ ~
wt_memval a.
Proof.
intros.
des a.
des (
tcheck_expr e).
des (
is_lval_typ_dec s).
left;
econstructor;
eauto.
right;
intro A;
inv A;
destr.
right;
intro A;
inv A;
destr.
Qed.
Lemma Forall_app_l:
forall {
A} (
P:
A ->
Prop)
l1 l2,
Forall P (
l1 ++
l2) ->
Forall P l1.
Proof.
induction l1; try constructor.
change ((a::l1)++ l2) with (a:: (l1 ++ l2)) in H.
inv H; auto.
change ((a::l1)++ l2) with (a:: (l1 ++ l2)) in H.
inv H; auto.
apply IHl1 with (l2:=l2); auto.
Qed.
Lemma Forall_rev':
forall {
A} (
P:
A ->
Prop)
l,
Forall P l ->
Forall P (
rev l).
Proof.
Lemma Forall_app_r:
forall {
A} (
P:
A ->
Prop)
l1 l2,
Forall P (
l1 ++
l2) ->
Forall P l2.
Proof.
Lemma loadbytes_wt_memval:
forall m b ofs n bytes,
loadbytes m b ofs n =
Some bytes ->
Forall wt_memval bytes.
Proof.
unfold loadbytes.
intros.
revert H.
destr_no_dep.
inv H.
generalize (
contents_wt_memval m b ).
generalize ((
mem_contents m)#
b).
generalize ofs.
generalize (
nat_of_Z n).
clear;
induction n;
simpl;
intros.
constructor.
constructor;
eauto.
Qed.
Theorem load_int64_split:
forall m b ofs v,
load Mint64 m b ofs =
Some v ->
exists v1 v2,
load Mint32 m b ofs =
Some (
if Archi.big_endian then v1 else v2)
/\
load Mint32 m b (
ofs + 4) =
Some (
if Archi.big_endian then v2 else v1)
/\
v ==
Val.longofwords v1 v2.
Proof.
Properties related to store
Theorem valid_access_store:
forall m1 chunk b ofs v,
valid_access m1 chunk b ofs Writable ->
tcheck_expr v =
Some ((
type_of_chunk chunk)) ->
{
m2:
mem |
store chunk m1 b ofs v =
Some m2 }.
Proof.
intros.
unfold store.
destruct (
valid_access_dec m1 chunk b ofs Writable); [|
contradiction].
destruct ( (
is_encodable chunk v) )
eqn:?.
eauto.
unfold is_encodable in Heqb0.
revert Heqb0;
destr_cond_match;
try congruence.
unfold encode_val in Heqo.
rewrite H0 in Heqo.
rewrite styp_eq_refl in Heqo.
destruct v;
destruct s;
destruct chunk;
simpl in *;
intuition try congruence.
Defined.
Hint Local Resolve valid_access_store:
mem.
Section STORE.
Variable chunk:
memory_chunk.
Variable m1:
mem.
Variable b:
block.
Variable ofs:
Z.
Variable v:
expr_sym.
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 =
PMap.set b (
setN (
encode_val_tot chunk v)
ofs m1.(
mem_contents)#
b)
m1.(
mem_contents).
Proof.
Lemma store_encode_some:
encode_val chunk v <>
None.
Proof.
unfold store in STORE;
revert STORE.
repeat destr_cond_match;
try congruence.
intro A;
inv A.
revert Heqb0;
unfold is_encodable;
destr_cond_match;
intuition congruence.
Qed.
Lemma encode_val_tot_length:
length (
encode_val_tot chunk v) =
size_chunk_nat chunk.
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.
Local Hint Resolve perm_store_1 perm_store_2:
mem.
Theorem size_of_block_store:
forall b',
size_of_block m1 b' =
size_of_block m2 b'.
Proof.
intros.
revert STORE.
unfold store.
destr_cond_match;
try congruence.
destr_cond_match;
try congruence.
intro A;
inv A.
unfold size_of_block;
simpl.
reflexivity.
destr_cond_match;
congruence.
Qed.
Theorem mask_store:
forall b',
mask m1 b' =
mask m2 b'.
Proof.
intros.
revert STORE.
unfold store.
destr_cond_match;
try congruence.
destr_cond_match;
try congruence.
intro A;
inv A;
unfold mask;
reflexivity.
destr_cond_match;
congruence.
Qed.
Theorem bounds_of_block_store:
forall b',
bounds_of_block m1 b' =
bounds_of_block m2 b'.
Proof.
intros;
revert STORE;
unfold store;
repeat (
destr_cond_match;
try congruence).
intro A;
inv A;
reflexivity.
Qed.
Theorem nat_mask_store:
forall b',
nat_mask m1 b' =
nat_mask m2 b'.
Proof.
intros;
revert STORE;
unfold store;
repeat destr_cond_match;
try congruence.
intro A;
inv A;
reflexivity.
Qed.
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.
Lemma tcheck_expr_store_chunk:
tcheck_expr v =
Some ((
type_of_chunk chunk)).
Proof.
Theorem load_store_similar:
forall chunk',
size_chunk chunk' =
size_chunk chunk ->
align_chunk chunk' <=
align_chunk chunk ->
exists v',
load chunk'
m2 b ofs =
Some v' /\
decode_encode_expr_sym v chunk chunk'
v'.
Proof.
Lemma store_some_type:
tcheck_expr v =
Some (
type_of_chunk chunk).
Proof.
Theorem load_store_similar_2:
forall chunk'
v1,
size_chunk chunk' =
size_chunk chunk ->
align_chunk chunk' <=
align_chunk chunk ->
type_of_chunk chunk' =
type_of_chunk chunk ->
load chunk'
m2 b ofs =
Some v1 ->
chunk' <>
Many32 /\
chunk' <>
Many64 ->
v1 ==
Val.load_result_expr chunk'
v.
Proof.
intros.
destruct (
load_store_similar chunk')
as [
v' [
A B]];
auto.
rewrite A in H2;
inv H2.
assert (
WT:=
store_some_type).
unfold Val.load_result_expr.
des chunk;
des chunk';
try (
rewrite Val.sign_ext_norm;
auto;
fail);
try (
rewrite Val.zero_ext_norm;
auto;
fail).
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
try rewrite WT;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
rewrite Int.sign_ext_above by (
vm_compute;
intuition congruence);
auto.
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
try rewrite WT;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
rewrite Int64.sign_ext_above by (
vm_compute;
intuition congruence);
auto.
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
try rewrite WT;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
simpl.
generalize (
eSexpr_wt alloc0 em eb eu v Tsingle _ eq_refl).
des (
eSexpr alloc0 em eb eu Tsingle v).
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
try rewrite WT;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
simpl.
inv_expr_type (
eSexpr alloc0 em eb eu Tfloat v).
-
rewrite WT in B;
auto.
symmetry;
auto.
-
omega.
Qed.
Theorem load_store_same:
exists v1,
load chunk m2 b ofs =
Some v1 /\
v1 == (
Val.load_result chunk v).
Proof.
intros.
assert (
Val.has_type v (
styp_of_typ (
AST.type_of_chunk chunk))).
unfold Val.has_type.
apply tcheck_expr_correct.
rewrite tcheck_expr_store_chunk.
des chunk.
exploit load_store_similar;
eauto.
omega.
intros [
v' [
A B]].
rewrite A.
exists v';
split;
auto.
rewrite Val.load_result_eq_expr';
auto.
assert (
Val.has_type v' (
type_of_chunk chunk)).
eapply load_type;
eauto.
unfold Val.has_type in *.
solve_wt.
des chunk.
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
auto;
try rewrite H0;
try rewrite H;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
rewrite Int.sign_ext_above by (
vm_compute;
intuition congruence);
auto.
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
auto;
try rewrite H0;
try rewrite H;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
rewrite Int64.sign_ext_above by (
vm_compute;
intuition congruence);
auto.
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
auto;
try rewrite H0;
try rewrite H;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
simpl.
generalize (
eSexpr_wt alloc0 em eb eu v Tsingle _ eq_refl).
des (
eSexpr alloc0 em eb eu Tsingle v).
-
intro;
intros.
specialize (
B resType sz msk);
rewrite B.
apply norm_eq';
simpl;
auto;
try rewrite H0;
try rewrite H;
simpl;
auto;
try tauto.
intros;
simpl_eval'.
simpl.
inv_expr_type (
eSexpr alloc0 em eb eu Tfloat v).
-
rewrite H in B;
auto.
symmetry;
auto.
Qed.
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) =
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(
ZMap.get q (
setN vl p c)).
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 (
ZMap.get q c) (
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(
Eval (
Eptr v_b v_o)) ->
(
chunk =
Mint32 /\
v =
Eval (
Eptr v_b v_o) /\
chunk' =
Mint32 /\
b' =
b /\
ofs' =
ofs)
\/ (
b' <>
b \/
ofs' +
size_chunk chunk' <=
ofs \/
ofs +
size_chunk chunk <=
ofs').
Proof.
intros.
assert (
True)
by (
destruct m1;
auto).
contradict H.
unfold load.
destr_cond_match;
try congruence.
Transparent decode_val.
des chunk'.
Qed.
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.
Lemma is_encodable_eq:
forall v1 v2 chunk1 chunk2 ,
encode_val chunk1 v1 =
encode_val chunk2 v2 ->
align_chunk chunk1 =
align_chunk chunk2 ->
size_chunk chunk1 =
size_chunk chunk2 ->
is_encodable chunk1 v1 =
is_encodable chunk2 v2.
Proof.
intros;
unfold is_encodable.
rewrite H.
destr_cond_match;
auto.
Qed.
Lemma store_similar_chunks:
forall chunk1 chunk2 v1 v2 m b ofs,
encode_val chunk1 v1 =
encode_val chunk2 v2 ->
align_chunk chunk1 =
align_chunk chunk2 ->
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.
Definition memval_equiv_typ (
e1 e2:
memval) :=
match tcheck_memval e1,
tcheck_memval e2 with
Some t1,
Some t2 =>
if styp_eq t1 t2
then forall alloc em,
eSexpr alloc em eb eu t1 (
expr_of_memval e1 (
ltyp_of_typ t1)) =
eSexpr alloc em eb eu t2 (
expr_of_memval e2 (
ltyp_of_typ t2))
else False
|
_,
_ =>
False
end.
Record mem_equiv (
m1 m2:
mem) :
Prop :=
mk_mem_equiv {
mem_contents_eq:
forall b ofs,
memval_equiv_typ (
ZMap.get ofs ((
mem_contents m1) #
b))
(
ZMap.get ofs ((
mem_contents m2) #
b));
mem_access_eq:
(
mem_access m1) = (
mem_access m2);
mem_blocksize_eq:
(
mem_blocksize m1) = (
mem_blocksize m2);
mem_mask_eq:
(
mem_mask m1) = (
mem_mask m2);
nextblock_eq:
(
nextblock m1) = (
nextblock m2) }.
Definition opt_mem_equiv (
m1 m2:
option mem) :
Prop :=
match m1,
m2 with
None,
None =>
True
|
Some mm1 ,
Some mm2 =>
mem_equiv mm1 mm2
|
_ ,
_ =>
False
end.
Lemma memval_equiv_typ_refl:
forall ofs0 m b,
memval_equiv_typ (
ZMap.get ofs0 (
mem_contents m) #
b)
(
ZMap.get ofs0 (
mem_contents m) #
b).
Proof.
Lemma get_setN_not_last:
forall al ofs0 ofs o a t,
ofs0 <>
ofs ->
(
ZMap.get ofs0 (
setN al o (
ZMap.set ofs a t))) =
ZMap.get ofs0 (
setN al o t).
Proof.
Lemma met_eq:
forall i1 i2,
list_forall2 memval_equiv_typ i1 i2 ->
forall m b ofs b0 ofs0,
memval_equiv_typ
(
ZMap.get ofs0 ((
PMap.set b (
setN i1 ofs (
mem_contents m) #
b) (
mem_contents m)) #
b0))
(
ZMap.get ofs0 ((
PMap.set b (
setN i2 ofs (
mem_contents m) #
b) (
mem_contents m)) #
b0)).
Proof.
Lemma memval_equiv_tint_typ:
forall i1 i2,
Forall (
fun x =>
tcheck_memval x =
Some Tint)
i1 ->
Forall (
fun x =>
tcheck_memval x =
Some Tint)
i2 ->
(
list_forall2 memval_equiv_tint i1 i2 <->
list_forall2 memval_equiv_typ i1 i2).
Proof.
split;
induction 1;
simpl;
intros;
try constructor;
auto.
inv H;
inv H0.
unfold memval_equiv_typ.
unfold memval_equiv_tint in H1.
rewrite H5.
rewrite H4.
simpl.
auto.
apply IHlist_forall2;
eauto.
inv H;
inv H0;
auto.
inv H;
inv H0;
auto.
unfold memval_equiv_typ in H1.
unfold memval_equiv_tint.
inv H;
inv H0.
rewrite H5 in H1.
rewrite H4 in H1.
simpl in H1.
auto.
apply IHlist_forall2;
eauto.
inv H;
inv H0;
auto.
inv H;
inv H0;
auto.
Qed.
Theorem store_int8_zero_ext:
forall m b ofs n,
opt_mem_equiv
(
store Mint8unsigned m b ofs (
Eval (
Eint (
Int.zero_ext 8
n))))
(
store Mint8unsigned m b ofs (
Eval (
Eint n))).
Proof.
Theorem store_int8_sign_ext:
forall m b ofs n,
opt_mem_equiv
(
store Mint8signed m b ofs (
Eval (
Eint (
Int.sign_ext 8
n))))
(
store Mint8signed m b ofs (
Eval (
Eint n))).
Proof.
Theorem store_int16_zero_ext:
forall m b ofs n,
opt_mem_equiv
(
store Mint16unsigned m b ofs (
Eval (
Eint (
Int.zero_ext 16
n))))
(
store Mint16unsigned m b ofs (
Eval (
Eint n))).
Proof.
Theorem store_int16_sign_ext:
forall m b ofs n,
opt_mem_equiv
(
store Mint16signed m b ofs (
Eval (
Eint (
Int.sign_ext 16
n))))
(
store Mint16signed m b ofs (
Eval (
Eint 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 ->
check_bytes bytes =
true ->
{
m2 :
mem |
storebytes m1 b ofs bytes =
Some m2 }.
Proof.
Lemma check_bytes_complete:
forall l :
list memval,
Forall wt_memval l ->
check_bytes l =
true.
Proof.
induction l; simpl; intuition try congruence.
inv H.
specialize (IHl H3).
rewrite IHl.
destruct a; simpl in *; intuition try congruence.
destruct H2 as [s TE IT].
rewrite TE.
inv IT; ring.
Qed.
Theorem storebytes_store:
forall m1 b ofs chunk v m2 enc,
encode_val chunk v =
Some enc ->
storebytes m1 b ofs enc =
Some m2 ->
(
align_chunk chunk |
ofs) ->
store chunk m1 b ofs v =
Some m2.
Proof.
Lemma check_bytes_encode:
forall chunk v l,
encode_val chunk v =
Some l ->
check_bytes l =
true.
Proof.
Theorem store_storebytes:
forall m1 b ofs chunk v m2 enc,
store chunk m1 b ofs v =
Some m2 ->
encode_val chunk v =
Some enc ->
storebytes m1 b ofs enc =
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 =
PMap.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 size_of_block_storebytes:
forall b',
size_of_block m1 b' =
size_of_block m2 b'.
Proof.
intros;
revert STORE.
unfold storebytes;
repeat destr_cond_match;
try congruence.
intro A;
inv A;
unfold size_of_block;
reflexivity.
Qed.
Theorem mask_storebytes:
forall b',
mask m1 b' =
mask m2 b'.
Proof.
intros;
revert STORE.
unfold storebytes;
repeat destr_cond_match;
try congruence.
intro A;
inv A;
unfold mask;
reflexivity.
Qed.
Theorem bounds_of_block_storebytes:
forall b',
bounds_of_block m1 b' =
bounds_of_block m2 b'.
Proof.
intros;
revert STORE;
unfold storebytes;
repeat destr_cond_match;
try congruence.
intro A;
inv A;
reflexivity.
Qed.
Theorem nat_mask_storebytes:
forall b',
nat_mask m1 b' =
nat_mask m2 b'.
Proof.
intros;
revert STORE;
unfold storebytes;
repeat destr_cond_match;
try congruence.
intro A;
inv A;
reflexivity.
Qed.
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_disjoint:
forall b'
ofs'
len,
len >= 0 ->
b' <>
b \/
Intv.disjoint (
ofs',
ofs' +
len) (
ofs,
ofs +
Z_of_nat (
length bytes)) ->
loadbytes m2 b'
ofs'
len =
loadbytes m1 b'
ofs'
len.
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.
Lemma check_bytes_Forall:
forall b,
check_bytes b =
true <->
Forall wt_memval b.
Proof.
Lemma check_bytes_false_Forall:
forall b,
check_bytes b =
false <-> ~
Forall wt_memval b.
Proof.
Lemma Forall_app_not:
forall {
A}
P (
a b:
list A),
(~
Forall P a) \/ (~
Forall P b) ->
~
Forall P (
a++
b).
Proof.
Lemma check_bytes_append:
forall a b,
check_bytes (
a ++
b) =
check_bytes a &&
check_bytes b.
Proof.
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_check_bytes:
forall m b ofs bytes m2,
storebytes m b ofs bytes =
Some m2 ->
check_bytes bytes =
true.
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.
Definition mem_eq_modulo_normalise (
m1 m2:
mem) :=
forall chunk b ofs v1 v2,
load chunk m1 b ofs =
Some v1 ->
load chunk m2 b ofs =
Some v2 ->
v1 ==
v2.
Notation "
a ==
m b" := (
mem_eq_modulo_normalise a b) (
at level 80).
Lemma load_align_chunk:
forall m b ofs chunk v,
load chunk m b ofs =
Some v ->
(
align_chunk chunk |
ofs).
Proof.
intros until v.
unfold load.
destr_cond_match;
try congruence.
destruct v0.
intros;
auto.
Qed.
Lemma loadbytes_one:
forall m b o n bytes,
loadbytes m b o n =
Some bytes ->
n > 0 ->
exists b1 b2,
loadbytes m b o 1 =
Some b1 /\
loadbytes m b (
o+1) (
n-1) =
Some b2 /\
bytes =
b1 ++
b2.
Proof.
Lemma expr_of_memval_zero_ext_eq:
forall a1 a2 alloc0 i i0 em,
wt_memval a1 ->
wt_memval a2 ->
tcheck_expr (
expr_of_memval a2 Lint) =
Some Tint ->
tcheck_expr (
expr_of_memval a1 Lint) =
Some Tint ->
eSexpr alloc0 em eb eu Tint (
expr_of_memval a1 Lint) =
Vi i ->
eSexpr alloc0 em eb eu Tint (
expr_of_memval a2 Lint) =
Vi i0 ->
Int.zero_ext 8
i =
Int.zero_ext 8
i0 ->
i =
i0.
Proof.
Lemma decode_val_spec':
forall l l',
Forall wt_memval l ->
Forall wt_memval l' ->
list_forall2 memval_equiv_tint l l' ->
forall c alloc em,
eSexpr alloc em eb eu ((
type_of_chunk c)) (
decode_val c l) =
eSexpr alloc em eb eu ((
type_of_chunk c)) (
decode_val c l').
Proof.
Transparent decode_val.
Lemma mem_normalise_byte :
forall m1 m2,
(
forall b ofs v1 v2,
load Mint8unsigned m1 b ofs =
Some v1 ->
load Mint8unsigned m2 b ofs =
Some v2 ->
forall alloc em t,
eSexpr alloc em eb eu t v1 =
eSexpr alloc em eb eu t v2) ->
(
forall chunk b ofs v1 v2,
load chunk m1 b ofs =
Some v1 ->
load chunk m2 b ofs =
Some v2 ->
forall alloc em,
eSexpr alloc em eb eu ((
type_of_chunk chunk))
v1 =
eSexpr alloc em eb eu ((
type_of_chunk chunk))
v2).
Proof.
Lemma bytewise_eq_all :
forall m1 m2
,
(
forall b ofs v1 v2,
load Mint8unsigned m1 b ofs =
Some v1 ->
load Mint8unsigned m2 b ofs =
Some v2 ->
forall alloc em t,
eSexpr alloc em eb eu t v1 =
eSexpr alloc em eb eu t v2) ->
m1 ==
m m2.
Proof.
intros.
-
intro;
intros.
intro;
intros.
generalize (
mem_normalise_byte m1 m2 H _ _ _ _ _ H0 H1).
generalize (
load_type _ _ _ _ _ H0).
generalize (
load_type _ _ _ _ _ H1).
unfold Val.has_type in *.
intros.
destr_wt;
solve_wt.
apply norm_eq'.
intuition try congruence.
rewrite e.
intros;
auto.
rewrite e in H3;
inv H3.
rewrite H7 in *.
auto.
apply norm_eq_not_wt;
auto.
intro;
solve_wt.
contradict n;
solve_wt.
congruence.
Qed.
Lemma eSexpr_eq_int_eq_all:
forall x1 x2 alloc em,
memval_equiv x1 x2 ->
eSexpr alloc em eb eu Tint (
decode_val Mint8unsigned (
x1::
nil)) =
eSexpr alloc em eb eu Tint (
decode_val Mint8unsigned (
x2::
nil)) ->
forall t,
eSexpr alloc em eb eu t (
decode_val Mint8unsigned (
x1::
nil)) =
eSexpr alloc em eb eu t (
decode_val Mint8unsigned (
x2::
nil)).
Proof.
Require Import Fappli_IEEE_bits.
Require Import Psatz.
Lemma int_range_int64:
forall i,
0 <=
Int.unsigned i <=
Int64.max_unsigned.
Proof.
Lemma int_inf_two_p_32:
forall i,
0 <=
Int.unsigned i <
two_power_nat 32.
Proof.
Lemma decode_val_eq_memval_equiv:
forall l l'
(
FWMl:
Forall wt_memval l)
(
FWMl':
Forall wt_memval l')
(
EVAL:
forall alloc em ,
eSexpr alloc em eb eu Tlong (
decode_val Mint64 l) =
eSexpr alloc em eb eu Tlong (
decode_val Mint64 l')),
length l =
length l' ->
(
length l <= 8)%
nat ->
list_forall2 memval_equiv_tint l l'.
Proof.
intros.
assert (
forall (
alloc0 :
NormaliseSpec.mem) (
em :
block ->
int ->
byte),
eSexpr alloc0 em eb eu Tlong
(
proj_symbolic_aux_le (
rev_if_be l)
Llong) =
eSexpr alloc0 em eb eu Tlong
(
proj_symbolic_aux_le (
rev_if_be l')
Llong)).
{
intros.
specialize (
EVAL alloc0 em).
repeat rewrite decode_val_info with (
c:=
Mint64)
in EVAL.
simpl in EVAL.
simpl_eval'.
apply proof_irr_int64 in H4.
repeat rewrite Int64.sign_ext_above with (
n:=64)
in H4 by (
vm_compute;
congruence).
subst;
auto.
}
clear EVAL.
apply list_forall2_rib_inv.
revert H H0 H1.
rewrite <- (
rev_if_be_length _ l).
rewrite <- (
rev_if_be_length _ l').
apply Forall_rib in FWMl.
apply Forall_rib in FWMl'.
revert FWMl FWMl'.
generalize (
rev_if_be l).
generalize (
rev_if_be l').
clear l l'.
induction l;
simpl;
intros.
-
des l.
constructor.
-
des l0.
Opaque expr_of_memval.
assert (
length l1 <= 7)%
nat by omega.
inv FWMl;
inv FWMl'.
inv H.
clear H0.
specialize (
IHl _ H6 H8 H4).
assert (
eom_il:
forall alloc em a i1,
wt_memval a ->
eSexpr alloc em eb eu Tlong (
expr_of_memval a Llong) =
Vl i1 ->
eSexpr alloc em eb eu Tint (
expr_of_memval a Lint) =
Vi (
Int64.loword i1)).
{
clear;
intros.
generalize (
eSexpr_wt alloc0 em eb eu (
expr_of_memval a Lint)
Tint _ eq_refl).
des (
eSexpr alloc0 em eb eu Tint (
expr_of_memval a Lint)).
f_equal.
eapply eom_int_long_same;
eauto.
}
assert (
forall alloc0 em,
exists i i0 i1 i2,
eSexpr alloc0 em eb eu Tlong (
cast Llong (
expr_of_memval m Llong)) =
Vl i /\
eSexpr alloc0 em eb eu Tlong (
proj_symbolic_aux_le l1 Llong) =
Vl i0 /\
eSexpr alloc0 em eb eu Tlong (
cast Llong (
expr_of_memval a Llong)) =
Vl i1 /\
eSexpr alloc0 em eb eu Tlong (
proj_symbolic_aux_le l Llong) =
Vl i2 /\
Int64.add i (
Int64.shl'
i0 (
Int.repr 8)) =
Int64.add i1 (
Int64.shl'
i2 (
Int.repr 8))).
{
intros.
specialize (
H1 alloc0 em).
simpl_eval'.
apply proof_irr_int64 in H11.
repeat eexists;
repeat split;
eauto.
}
clear H1.
assert (
forall alloc0 em i i0 i1 i2 i3,
eSexpr alloc0 em eb eu Tlong (
cast Llong (
expr_of_memval m Llong)) =
Vl i ->
eSexpr alloc0 em eb eu Tlong (
proj_symbolic_aux_le l1 Llong) =
Vl i0 ->
eSexpr alloc0 em eb eu Tlong (
cast Llong (
expr_of_memval a Llong)) =
Vl i1 ->
eSexpr alloc0 em eb eu Tlong (
proj_symbolic_aux_le l Llong) =
Vl i2 ->
Int64.add i (
Int64.shl'
i0 (
Int.repr 8)) =
Int64.add i1 (
Int64.shl'
i2 (
Int.repr 8)) ->
0 <=
i3 <
Int64.zwordsize ->
Int64.testbit i i3 =
Int64.testbit i1 i3 /\
Int64.testbit i0 i3 =
Int64.testbit i2 i3).
{
revert H5 H6 H7 H8 H2 H4 eom_il.
clear.
intros WTm WTl1 WTa WTl l7 len_l1_l eom_il alloc0 em i i0 i1 i2 i3 EOMm PSAl1 EOMa PSAl i64eq i3val.
generalize (
eSexpr_wt alloc0 em eb eu (
expr_of_memval m Llong)
Tint _ eq_refl).
destruct (
eSexpr alloc0 em eb eu Tint (
expr_of_memval m Llong))
eqn:?;
simpl;
intro A;
try (
exfalso;
auto;
fail);
clear A.
generalize (
eSexpr_wt alloc0 em eb eu (
expr_of_memval a Llong)
Tint _ eq_refl).
destruct (
eSexpr alloc0 em eb eu Tint (
expr_of_memval a Llong))
eqn:?;
simpl;
intro A;
try (
exfalso;
auto;
fail);
clear A.
unfold cast in EOMm,
EOMa.
rewrite expr_of_memval_wt in *;
simpl;
auto.
generalize (
expr_of_memval_bound_int_long _ _ _ _ WTm Heql0).
generalize (
expr_of_memval_bound_int_long _ _ _ _ WTa Heql1).
intros EOM_bnd_a EOM_bnd_m.
generalize (
psa_le_n_bnds _ WTl1 7
l7 _ _ _ PSAl1).
rewrite len_l1_l in l7.
generalize (
psa_le_n_bnds _ WTl 7
l7 _ _ _ PSAl).
intros PSA_bnd_l PSA_bnd_l1.
simpl in *.
unfold eunop in *.
rewrite Heql0 in EOMm.
rewrite Heql1 in EOMa.
unfold unop,
fun_of_unop,
fun_of_unop'
in *;
simpl in *.
inv EOMm.
inv EOMa.
clear Heql1 PSAl1 Heql0 PSAl.
generalize i64eq;
intro i64eq'.
repeat rewrite Int64.testbit_repr;
auto.
assert (
forall ii, 0 <=
ii <
Int64.zwordsize ->
Z.testbit (
Int.unsigned i4)
ii =
Z.testbit (
Int.unsigned i5)
ii).
{
intros.
des (
zlt ii Int.zwordsize).
repeat rewrite <-
Int.testbit_repr;
auto.
repeat rewrite Int.repr_unsigned.
apply (
f_equal (
fun x =>
Int64.testbit x ii))
in i64eq.
rewrite Int64_add_is_or_lt_256 in i64eq.
rewrite Int64_add_is_or_lt_256 in i64eq.
repeat rewrite Int64.bits_or in i64eq by omega.
repeat rewrite shl'
_shl in i64eq by (
vm_compute;
intuition congruence).
change (
Int.unsigned (
Int.repr 8))
with 8
in i64eq.
repeat rewrite Int64.bits_shl in i64eq by omega.
change (
Int64.unsigned (
Int64.repr 8))
with 8
in i64eq.
des (
zlt ii 8).
repeat rewrite orb_false_r in i64eq;
auto.
repeat rewrite Int64.testbit_repr in i64eq by auto.
auto.
rewrite (
int_testbit_lt_256 i4);
auto.
rewrite (
int_testbit_lt_256 i5);
auto.
destr.
rewrite Int64.unsigned_repr;
auto.
apply int_range_int64.
rewrite Int64.unsigned_repr;
auto.
apply int_range_int64.
repeat rewrite Int.Ztestbit_above with (
n:=32%
nat);
auto.
apply int_inf_two_p_32.
apply int_inf_two_p_32.
}
assert (
forall ii, 0 <=
ii <
Int64.zwordsize ->
Int64.testbit i0 ii =
Int64.testbit i2 ii).
{
intros.
apply (
f_equal (
fun x =>
Int64.testbit x (
ii+8)))
in i64eq.
rewrite Int64_add_is_or_lt_256 in i64eq.
rewrite Int64_add_is_or_lt_256 in i64eq.
des (
zlt (
ii+8)
Int64.zwordsize).
repeat rewrite Int64.bits_or in i64eq by omega.
repeat rewrite shl'
_shl in i64eq by (
vm_compute;
intuition congruence).
change (
Int.unsigned (
Int.repr 8))
with 8
in i64eq.
repeat rewrite Int64.bits_shl in i64eq by omega.
change (
Int64.unsigned (
Int64.repr 8))
with 8
in i64eq.
repeat rewrite Int64.testbit_repr in i64eq by omega.
rewrite H in i64eq;
auto;
try omega.
rewrite Int.Ztestbit_above with (
n:=8%
nat)
in i64eq;
simpl;
auto;
try omega.
simpl in i64eq.
des (
zlt (
ii + 8) 8);
try omega.
replace (
ii + 8 - 8)
with ii in i64eq by omega.
auto.
change (
two_power_nat 8)
with 256;
split;
try omega.
generalize (
Int.unsigned_range i5);
omega.
rewrite (
int64_testbit_lt_256_7 i0) ;
auto.
rewrite (
int64_testbit_lt_256_7 i2) ;
auto.
rewrite Heqs;
auto.
rewrite Int64.unsigned_repr;
auto.
apply int_range_int64.
rewrite Int64.unsigned_repr;
auto.
apply int_range_int64.
}
split.
apply H;
auto.
apply H0;
auto.
}
assert (
forall (
alloc0 :
NormaliseSpec.mem) (
em :
block ->
int ->
byte),
exists i i0 i1 i2 :
int64,
eSexpr alloc0 em eb eu Tlong (
cast Llong (
expr_of_memval m Llong)) =
Vl i /\
eSexpr alloc0 em eb eu Tlong (
proj_symbolic_aux_le l1 Llong) =
Vl i0 /\
eSexpr alloc0 em eb eu Tlong (
cast Llong (
expr_of_memval a Llong)) =
Vl i1 /\
eSexpr alloc0 em eb eu Tlong (
proj_symbolic_aux_le l Llong) =
Vl i2 /\
Int64.add i (
Int64.shl'
i0 (
Int.repr 8)) =
Int64.add i1 (
Int64.shl'
i2 (
Int.repr 8)) /\
forall i3, 0 <=
i3 <
Int64.zwordsize ->
Int64.testbit i i3 =
Int64.testbit i1 i3 /\
Int64.testbit i0 i3 =
Int64.testbit i2 i3).
{
intros.
destruct (
H alloc0 em)
as (
i &
i0 &
i1 &
i2 &
A &
B &
C &
D &
E).
rewrite A;
rewrite B;
rewrite C;
rewrite D.
do 4
eexists.
do 4
split;
eauto.
}
clear H H0.
constructor.
+
unfold memval_equiv_tint.
intros.
destruct (
H1 alloc0 em)
as (
i &
i0 &
i1 &
i2 &
A &
B &
C &
D &
E &
F).
rewrite eom_il with (
i1:=
i);
auto.
rewrite eom_il with (
i1:=
i1);
auto.
f_equal;
f_equal.
solve_long.
destruct (
F _ (
conj H0 H3));
auto.
clear -
C H7.
inv_expr_type (
eSexpr alloc0 em eb eu Tint (
expr_of_memval a Llong)).
inv_expr_type (
eSexpr alloc0 em eb eu Tlong (
expr_of_memval a Llong)).
unfold cast in C.
rewrite expr_of_memval_wt in C;
auto.
destr.
repeat (
simpl_eval';
simpl).
rewrite <-
eom_int_long_same'
in Heql1;
auto.
generalize (
eom_int_long_same _ _ _ _ _ H7 Heql1 Heql0) ;
eauto.
intro;
subst.
generalize (
expr_of_memval_bound_long _ _ _ _ H7 Heql0).
intros.
f_equal.
unfold Int64.loword.
rewrite Int.unsigned_repr.
rewrite Int64.repr_unsigned;
auto.
generalize (
Int64.unsigned_range i0).
split.
omega.
transitivity 256.
omega.
vm_compute.
congruence.
clear -
A H5.
inv_expr_type (
eSexpr alloc0 em eb eu Tint (
expr_of_memval m Llong)).
inv_expr_type (
eSexpr alloc0 em eb eu Tlong (
expr_of_memval m Llong)).
unfold cast in A.
rewrite expr_of_memval_wt in A;
auto.
destr.
repeat (
simpl_eval';
simpl).
rewrite <-
eom_int_long_same'
in Heql1;
auto.
generalize (
eom_int_long_same _ _ _ _ _ H5 Heql1 Heql0) ;
eauto.
intro;
subst.
generalize (
expr_of_memval_bound_long _ _ _ _ H5 Heql0).
intros.
f_equal.
unfold Int64.loword.
rewrite Int.unsigned_repr.
rewrite Int64.repr_unsigned;
auto.
generalize (
Int64.unsigned_range i1).
split.
omega.
transitivity 256.
omega.
vm_compute.
congruence.
+
apply IHl.
omega.
intros.
destruct (
H1 alloc0 em)
as (
i &
i0 &
i1 &
i2 &
A &
B &
C &
D &
E &
F).
rewrite B;
rewrite D.
f_equal.
solve_long.
destruct (
F _ (
conj H0 H3));
auto.
Qed.
Lemma memval_equiv_tint_sym:
forall a b,
memval_equiv_tint a b ->
memval_equiv_tint b a.
Proof.
Lemma eSexpr_eq_int_eq_all_int:
forall v1 v2 x1 x2 alloc em,
wt_memval x1 ->
wt_memval x2 ->
decode_val Mint8unsigned (
x1::
nil) =
v1 ->
decode_val Mint8unsigned (
x2::
nil) =
v2 ->
memval_equiv_tint x1 x2 ->
eSexpr alloc em eb eu Tint v1 =
eSexpr alloc em eb eu Tint v2 ->
forall t,
eSexpr alloc em eb eu t v1 =
eSexpr alloc em eb eu t v2.
Proof.
Require Import Setoid.
Theorem storebytes_int64_split:
forall m b ofs v m'
x x0 enc64 encLoword encHiword
(
Hwt:
tcheck_expr v =
Some Tlong)
(
H :
store Mint64 m b ofs v =
Some m')
(
Enc64:
encode_val Mint64 v =
Some enc64)
(
EncLoword:
encode_val Mint32 (
if big_endian then Val.hiword v else Val.loword v) =
Some encLoword)
(
EncHiword:
encode_val Mint32 (
if big_endian then Val.loword v else Val.hiword v) =
Some encHiword)
(
SB :
storebytes m b ofs enc64 =
Some m')
(
e :
storebytes m b ofs encLoword =
Some x)
(
e0 :
storebytes x b (
ofs + 4)
encHiword =
Some x0),
m' ==
m x0.
Proof.
Lemma encode_val_wt'':
forall c v,
tcheck_expr v =
Some ((
type_of_chunk c)) ->
encode_val c v <>
None.
Proof.
Lemma ex_enc32_64:
forall (
b:
bool)
v enc64,
encode_val Mint64 v =
Some enc64 ->
(
exists enc32_1,
encode_val Mint32 (
if b then Val.hiword v else Val.loword v) =
Some enc32_1).
Proof.
Theorem store_int64_split:
forall m b ofs v m',
store Mint64 m b ofs v =
Some m' ->
exists m1 m2,
store Mint32 m b ofs (
if Archi.big_endian then Val.hiword v else Val.loword v) =
Some m1
/\
store Mint32 m1 b (
ofs + 4) (
if Archi.big_endian then Val.loword v else Val.hiword v) =
Some m2
/\
m' ==
m m2.
Proof.
Lemma store_int64_eq_add:
forall m b i v m',
store Mint64 m b (
Int.unsigned i)
v =
Some m' ->
Int.unsigned (
Int.add i (
Int.repr 4)) =
Int.unsigned i + 4.
Proof.
Properties related to alloc.
Section ALLOC.
Variable m1:
Mem.mem.
Variables lo hi:
Z.
Variable m2:
Mem.mem.
Variable b:
block.
Hypothesis ALLOC:
alloc m1 lo hi =
Some (
m2,
b).
Theorem mask_alloc_other:
forall b',
b <>
b' ->
mask m1 b' =
mask m2 b'.
Proof.
Theorem size_of_block_alloc_other:
forall b',
b <>
b' ->
size_of_block m1 b' =
size_of_block m2 b'.
Proof.
Theorem bounds_of_block_alloc_other:
forall b',
b <>
b' ->
bounds_of_block m1 b' =
bounds_of_block m2 b'.
Proof.
Theorem nat_mask_alloc_other:
forall b',
b <>
b' ->
nat_mask m1 b' =
nat_mask m2 b'.
Proof.
Theorem nextblock_alloc:
nextblock m2 =
Psucc (
nextblock m1).
Proof.
Theorem alloc_result:
b =
nextblock m1.
Proof.
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, 0 <=
ofs <
hi ->
perm m2 b ofs k Freeable.
Proof.
Theorem perm_alloc_inv:
forall b'
ofs k p,
perm m2 b'
ofs k p ->
if eq_block b'
b then 0 <=
ofs <
hi else perm m1 b'
ofs k p.
Proof.
Theorem perm_alloc_3:
forall ofs k p,
perm m2 b ofs k p -> 0 <=
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,
0 <=
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 0 <=
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.
Require Import Classical.
Lemma init_block'
_eundef:
forall n b cur o,
(0 <=
o <=
n)%
nat ->
nth_error (
init_block'
n b cur)
o =
Some (
Symbolic
(
Eval (
Eundef b (
Int.add cur (
Int.repr (
Z.of_nat o)))))
O).
Proof.
induction n;
simpl;
intros.
assert (
o=
O)
by omega.
subst.
simpl.
rewrite Int.add_zero.
auto.
destruct H.
destruct o.
simpl.
rewrite Int.add_zero;
auto.
simpl.
rewrite IHn;
auto.
rewrite Int.add_assoc.
f_equal.
f_equal.
f_equal.
f_equal.
f_equal.
rewrite Val.int_add_repr.
f_equal.
xomega.
omega.
Qed.
Lemma in_nth_error:
forall (
A:
Type) (
vl:
list A) (
x:
A),
In x vl ->
exists n,
nth_error vl n =
Some x.
Proof.
induction vl;
simpl;
intros.
exfalso;
auto.
destruct H;
subst;
auto.
exists O;
auto.
destruct (
IHvl _ H).
exists (
S x0);
auto.
Qed.
Lemma nth_error_length:
forall (
A:
Type) (
l:
list A)
x v,
nth_error l x =
Some v ->
(
length l >
x)%
nat.
Proof.
induction l;
simpl;
intros.
rewrite nth_error_nil in H;
congruence.
destruct x.
omega.
simpl in H.
apply IHl in H.
omega.
Qed.
Lemma init_block'
_length:
forall n b c,
length (
init_block'
n b c) =
S n.
Proof.
induction n; simpl; intros; eauto.
Qed.
Lemma init_block_eundef:
forall n o lo hi c,
lo <=
o ->
o +
Z.of_nat n <=
hi ->
Forall (
fun x =>
exists y z,
x =
Symbolic (
Eval (
Eundef y z))
O) (
getN n o (
init_block lo hi c)).
Proof.
induction n;
simpl;
intros.
constructor.
constructor;
auto.
-
unfold init_block.
zify.
destr;
try omega.
set (
P:=
fun mv =>
exists y z,
mv =
Symbolic (
Eval (
Eundef y z))
O).
refine (
setN_property P _ _ _ _ _ _).
intros.
apply in_nth_error in H2.
destruct H2.
rewrite init_block'
_eundef in H2.
inv H2.
unfold P;
simpl.
eauto.
split.
omega.
apply nth_error_length in H2.
rewrite init_block'
_length in H2.
omega.
rewrite init_block'
_length.
split.
omega.
rewrite <-
Z2Nat.inj_succ;
try omega.
rewrite Z2Nat.id;
try omega.
-
apply IHn.
omega.
rewrite Zpos_P_of_succ_nat in H0.
omega.
Qed.
Lemma decode_list_undef_is_undef:
forall l chunk,
length l =
size_chunk_nat chunk ->
Forall
(
fun x =>
exists y z,
x =
Symbolic (
Eval (
Eundef y z)) 0)
l ->
is_undef (
decode_val chunk (
rev_if_be l)).
Proof.
Theorem load_alloc_same:
forall chunk ofs v,
load chunk m2 b ofs =
Some v ->
is_undef v.
Proof.
Theorem load_alloc_same':
forall chunk ofs,
0 <=
ofs ->
ofs +
size_chunk chunk <=
hi -> (
align_chunk chunk |
ofs) ->
exists v,
load chunk m2 b ofs =
Some v /\
is_undef v.
Proof.
Theorem loadbytes_alloc_unchanged:
forall b'
ofs n,
valid_block m1 b' ->
loadbytes m2 b'
ofs n =
loadbytes m1 b'
ofs n.
Proof.
Theorem loadbytes_alloc_same:
forall n ofs bytes byte,
loadbytes m2 b ofs n =
Some bytes ->
In byte bytes ->
exists y z,
byte =
Symbolic (
Eval (
Eundef y z))
O.
Proof.
End ALLOC.
Lemma bounds_of_block_alloc:
forall m1 lo hi m1'
b1,
alloc m1 lo hi =
Some (
m1',
b1) ->
bounds_of_block m1'
b1 = (0,
hi).
Proof.
Lemma bounds_of_block_alloc_old:
forall m1 lo hi m1'
b1,
alloc m1 lo hi =
Some (
m1',
b1) ->
bounds_of_block m1 b1 = (0,0).
Proof.
Lemma alloc_mask:
forall m1 lo hi m1'
b1,
alloc m1 lo hi =
Some (
m1',
b1) ->
mask m1'
b1 =
alignment_of_size (
hi).
Proof.
Lemma pos2nat_id:
forall p,
Pos.of_nat (
S (
pred (
Pos.to_nat p))) =
p.
Proof.
Lemma size_mem_al_aligned:
forall l z,
z =
align z 8 ->
size_mem_al 8
l z =
align (
size_mem_al 8
l z) 8.
Proof.
induction l;
simpl;
intros;
auto.
apply IHl.
destruct a.
rewrite <- !
align_distr.
rewrite align_align;
omega.
Qed.
Lemma size_mem_aux_aligned:
forall l,
size_mem_aux l =
align (
size_mem_aux l) 8.
Proof.
Opaque Pos.of_nat.
Lemma alloc_size_mem':
forall m1 lo hi m1'
b1
(
ALLOC:
alloc m1 lo hi =
Some (
m1',
b1)),
size_mem m1' =
size_mem m1 +
align (
Z.max 0
hi) 8.
Proof.
Lemma size_mem_alloc_0:
forall tm1 tm2 sp
(
ALLOC:
alloc tm1 0 0 =
Some (
tm2,
sp)),
size_mem tm1 =
size_mem tm2.
Proof.
intros.
apply alloc_size_mem'
in ALLOC.
rewrite Z.max_id in ALLOC.
rewrite ALLOC.
change (
align 0 8)
with 0.
omega.
Qed.
Lemma size_mem_aligned:
forall m z,
Mem.size_mem m =
z ->
align z 8 =
z.
Proof.
Lemma alloc_lo_0:
forall m lo hi,
alloc m lo hi =
alloc m 0
hi.
Proof.
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.
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 mask_free:
forall b',
bf <>
b' ->
mask m1 b' =
mask m2 b'.
Proof.
Theorem size_of_block_free:
forall b',
bf <>
b' ->
size_of_block m1 b' =
size_of_block m2 b'.
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.
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.
Theorem load_free_2:
forall chunk b ofs v,
load chunk m2 b ofs =
Some v ->
load chunk m1 b ofs =
Some v.
Proof.
Theorem loadbytes_free:
forall b ofs n,
b <>
bf \/
lo >=
hi \/
ofs +
n <=
lo \/
hi <=
ofs ->
loadbytes m2 b ofs n =
loadbytes m1 b ofs n.
Proof.
Theorem loadbytes_free_2:
forall b ofs n bytes,
loadbytes m2 b ofs n =
Some bytes ->
loadbytes m1 b ofs n =
Some bytes.
Proof.
End FREE.
Lemma unchecked_free_bounds_of_block:
forall m b lo hi,
bounds_of_block (
unchecked_free m b lo hi)
b =
match (
bounds_of_block m b)
with
(
lo',
hi') =>
if zeq lo'
lo &&
zeq hi'
hi then (0,0)
else (
lo',
hi')
end.
Proof.
Lemma unchecked_free_bounds_of_block_other:
forall m b lo hi b',
b <>
b' ->
bounds_of_block (
unchecked_free m b lo hi)
b' =
bounds_of_block m b'.
Proof.
Lemma unchecked_free_bounds:
forall m b lo hi b',
bounds_of_block (
unchecked_free m b lo hi)
b' =
if eq_block b'
b
then match bounds_of_block m b with
(
lo',
hi') => (
if zeq lo'
lo &&
zeq hi'
hi
then (0,0)
else (
lo',
hi'))
end
else bounds_of_block m b'.
Proof.
Lemma bounds_free:
forall m m'
b b'
lo hi ,
Mem.free m b lo hi =
Some m' ->
b <>
b' ->
Mem.bounds_of_block m'
b' =
Mem.bounds_of_block m b'.
Proof.
Lemma bounds_freelist:
forall fbl m m'
b ,
Mem.free_list m fbl =
Some m' ->
~
In b (
map (
fun a =>
fst (
fst a))
fbl) ->
Mem.bounds_of_block m'
b =
Mem.bounds_of_block m b.
Proof.
induction fbl;
simpl;
intros.
inv H.
auto.
destruct a as [[
b'
lo]
hi].
destruct (
Mem.free m b'
lo hi)
eqn:?;
try congruence.
intros.
intuition try congruence.
simpl in *.
generalize (
IHfbl _ _ _ H H2).
intro A;
rewrite A.
erewrite bounds_free;
eauto.
Qed.
Lemma range_perm_freelist:
forall fbl m m'
b,
Mem.free_list m fbl =
Some m' ->
~
In b (
map (
fun a =>
fst (
fst a))
fbl) ->
forall lo hi k p,
Mem.range_perm m'
b lo hi k p ->
Mem.range_perm m b lo hi k p.
Proof.
induction fbl;
simpl;
intros.
inv H.
auto.
destruct a as [[
b'
lo']
hi'].
destruct (
Mem.free m b'
lo'
hi')
eqn:?;
try congruence.
intros.
intuition try congruence.
simpl in *.
generalize (
IHfbl _ _ _ H H3 _ _ _ _ H1).
unfold Mem.range_perm.
intros.
specialize (
H0 ofs H4).
eapply Mem.perm_free_3;
eauto.
Qed.
Lemma mask_freelist:
forall fbl m m'
b ,
Mem.free_list m fbl =
Some m' ->
~
In b (
map (
fun a =>
fst (
fst a))
fbl) ->
Mem.mask m'
b =
Mem.mask m b.
Proof.
induction fbl;
simpl;
intros.
inv H.
auto.
destruct a as [[
b'
lo]
hi].
destruct (
Mem.free m b'
lo hi)
eqn:?;
try congruence.
intros.
intuition try congruence.
simpl in *.
generalize (
IHfbl _ _ _ H H2).
intro A;
rewrite A.
erewrite <-
Mem.mask_free;
eauto.
Qed.
Lemma contents_free:
forall m b lo hi m'
b',
Mem.free m b lo hi =
Some m' ->
b <>
b' ->
(
Mem.mem_contents m) !!
b' = (
Mem.mem_contents m') !!
b'.
Proof.
Lemma contents_freelist:
forall fbl m m'
b',
Mem.free_list m fbl =
Some m' ->
~
In b' (
map (
fun a =>
fst (
fst a))
fbl) ->
(
Mem.mem_contents m) !!
b' = (
Mem.mem_contents m') !!
b'.
Proof.
induction fbl;
simpl;
intros.
inv H;
auto.
destruct a as [[
b lo']
hi'].
destruct (
Mem.free m b lo'
hi')
eqn:?;
intuition try congruence.
simpl in *.
rewrite (
contents_free _ _ _ _ _ _ Heqo H1).
eauto.
Qed.
Lemma freelist_valid:
forall fbl m m'
b,
Mem.free_list m fbl =
Some m' ->
~
Mem.valid_block m'
b ->
~
Mem.valid_block m b.
Proof.
induction fbl;
simpl;
intros.
inv H;
auto.
destruct a as [[
b0 lo]
hi].
destruct (
Mem.free m b0 lo hi)
eqn:?;
try congruence.
generalize (
IHfbl _ _ _ H H0).
intros.
intro.
generalize (
Mem.valid_block_free_1 _ _ _ _ _ Heqo _ H2);
auto.
Qed.
Lemma free_size_mem:
forall m1 lo hi m1'
b1
(
FREE:
free m1 b1 lo hi =
Some m1')
(
bnds:
bounds_of_block m1 b1 = (
lo,
hi)),
size_mem m1 =
size_mem m1' +
align (
Z.max 0 (
hi-
lo)) 8.
Proof.
Definition size_mem_blocks (
bl:
list (
block *
Z *
Z)) (
z:
Z) :
Z :=
fold_left
(
fun acc x =>
align acc 8 +
Z.max 0 (
snd x -
snd (
fst x)))
bl z.
Definition list_of_blocks (
bl:
list (
block*
Z*
Z)) :
list (
block*
Z) :=
map (
fun a :
ident *
Z *
Z => (
fst (
fst a),
snd a -
snd (
fst a)))
bl.
Lemma size_mem_blocks_al:
forall l z,
size_mem_al 8 (
list_of_blocks l) (
align z 8) =
align (
size_mem_blocks l z) 8.
Proof.
induction l;
simpl;
intros.
auto.
rewrite IHl.
rewrite Alloc.align_align.
auto.
omega.
Qed.
Lemma size_mem_al_rev:
forall l z,
size_mem_al 8
l z =
size_mem_al 8 (
rev l)
z.
Proof.
Lemma size_mem_app:
forall a b c,
size_mem_al 8 (
a++
b)
c =
size_mem_al 8
b (
size_mem_al 8
a c).
Proof.
Lemma freelist_size_mem:
forall bl m m'
(
bnds:
Forall (
fun bbnds :
ident*
Z*
Z =>
Mem.bounds_of_block m (
fst (
fst bbnds))
= (
snd (
fst bbnds),
snd (
bbnds)) )
bl)
(
FL:
Mem.free_list m bl =
Some m')
(
NR:
list_norepet (
map fst (
map fst bl))),
size_mem m =
align (
size_mem_blocks bl (
size_mem m')) 8.
Proof.
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 mask_drop_perm:
forall b',
mask m b' =
mask m'
b'.
Proof.
revert DROP;
unfold drop_perm;
destr_cond_match;
try congruence.
intro A;
inv A.
intros.
unfold mask;
reflexivity.
Qed.
Theorem size_of_block_drop_perm:
forall b',
size_of_block m b' =
size_of_block m'
b'.
Proof.
revert DROP;
unfold drop_perm;
destr_cond_match;
try congruence.
intro A;
inv A.
intros.
unfold size_of_block;
reflexivity.
Qed.
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.
Theorem loadbytes_drop:
forall b'
ofs n,
b' <>
b \/
ofs +
n <=
lo \/
hi <=
ofs \/
perm_order p Readable ->
loadbytes m'
b'
ofs n =
loadbytes m b'
ofs n.
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.
Record mem_inj (
map_undef:
Val.partial_undef_allocation) (
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_bounds:
(* we mimic mi_perm with bounds instead of permissions. *)
forall b1 b2 delta ofs,
f b1 =
Some(
b2,
delta) ->
in_bound ofs (
bounds_of_block m1 b1) ->
in_bound (
ofs+
delta) (
bounds_of_block m2 b2);
mi_align':
forall b b0 z,
(* we can now talk of the alignment of blocks *)
f b =
Some (
b0,
z) ->
(
mask m2 b0 >=
mask m1 b)%
nat /\
Z.divide (
two_p (
Z.of_nat (
mask m1 b)))
z;
mi_memval:
forall b1 ofs b2 delta,
f b1 =
Some(
b2,
delta) ->
perm m1 b1 ofs Cur Readable ->
memval_inject map_undef f
(
ZMap.get ofs m1.(
mem_contents)#
b1)
(
ZMap.get (
ofs+
delta)
m2.(
mem_contents)#
b2);
mi_size_mem:
(* m2 must be ``smaller'' than m1. *)
(
size_mem m2) <= (
size_mem m1)
}.
Lemma perm_bounds:
forall m b ofs p k,
Mem.perm m b ofs k p ->
in_bound ofs (
Mem.bounds_of_block m b).
Proof.
Lemma load_in_bound:
forall chunk b ofs m v,
load chunk m b ofs =
Some v ->
in_bound ofs (
Mem.bounds_of_block m b).
Proof.
Lemma mi_align:
forall f um m1 m2,
mem_inj um f m1 m2 ->
forall (
b1 b2:
block)
delta,
f b1 =
Some (
b2,
delta) ->
forall chunk ofs p,
range_perm m1 b1 ofs (
ofs +
size_chunk chunk)
Max p ->
(
align_chunk chunk |
delta).
Proof.
Preservation of permissions
Lemma perm_inj:
forall m f m1 m2 b1 ofs k p b2 delta,
mem_inj m 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 m f m1 m2 b1 lo hi k p b2 delta,
mem_inj m 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.
Lemma valid_access_inj:
forall m f m1 m2 b1 b2 delta chunk ofs p,
mem_inj m f m1 m2 ->
f b1 =
Some(
b2,
delta) ->
valid_access m1 chunk b1 ofs p ->
valid_access m2 chunk b2 (
ofs +
delta)
p.
Proof.
Preservation of loads.
Lemma getN_inj:
forall m f m1 m2 b1 b2 delta,
mem_inj m 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 m 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 m f m1 m2 chunk b1 ofs b2 delta v1,
mem_inj m 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.expr_inject m f v1 v2.
Proof.
Lemma loadbytes_inj:
forall m f m1 m2 len b1 ofs b2 delta bytes1,
mem_inj m 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 m f)
bytes1 bytes2.
Proof.
Preservation of stores.
Lemma setN_inj:
forall (
access:
Z ->
Prop)
delta m f vl1 vl2,
list_forall2 (
memval_inject m f)
vl1 vl2 ->
forall p c1 c2,
(
forall q,
access q ->
memval_inject m f (
ZMap.get q c1) (
ZMap.get (
q +
delta)
c2)) ->
(
forall q,
access q ->
memval_inject m f (
ZMap.get q (
setN vl1 p c1))
(
ZMap.get (
q +
delta) (
setN vl2 (
p +
delta)
c2))).
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.
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) ->
in_bound ofs1 (
bounds_of_block m b1) ->
in_bound ofs2 (
bounds_of_block m b2) ->
b1' <>
b2' \/
ofs1 +
delta1 <>
ofs2 +
delta2.
Lemma encode_val_tot_inject :
forall (
m :
Val.partial_undef_allocation) (
f :
meminj)
(
v1 v2 :
expr_sym) (
chunk :
memory_chunk),
Val.expr_inject m f v1 v2 ->
list_forall2 (
memval_inject m f) (
encode_val_tot chunk v1)
(
encode_val_tot chunk v2).
Proof.
Lemma store_size_block:
forall chunk m b o v m',
store chunk m b o v =
Some m' ->
size_block m' =
size_block m.
Proof.
unfold store;
intros.
repeat (
revert H;
destr).
inv H;
simpl.
unfold size_block.
simpl.
auto.
Qed.
Lemma store_mask:
forall chunk m b o v m',
store chunk m b o v =
Some m' ->
mask m' =
mask m.
Proof.
unfold store;
intros.
repeat (
revert H;
destr).
inv H;
simpl.
unfold mask.
simpl.
auto.
Qed.
Lemma store_mk_block_list:
forall chunk m b o v m',
store chunk m b o v =
Some m' ->
mk_block_list m' =
mk_block_list m.
Proof.
Lemma store_size_mem:
forall chunk m b o v m',
store chunk m b o v =
Some m' ->
size_mem m' =
size_mem m.
Proof.
Lemma size_block_store:
forall chunk m1 b1 ofs v1 n1,
store chunk m1 b1 ofs v1 =
Some n1 ->
forall b',
size_block n1 b' =
size_block m1 b'.
Proof.
intros.
unfold size_block,
get_size.
unfold store in H.
repeat (
revert H;
destr).
inv H;
simpl in *.
congruence.
inv H;
simpl in *;
congruence.
inv H.
simpl in *.
congruence.
Qed.
Lemma store_mapped_inj:
forall m f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
mem_inj m f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
meminj_no_overlap f m1 ->
f b1 =
Some (
b2,
delta) ->
Val.expr_inject m f v1 v2 ->
exists n2,
store chunk m2 b2 (
ofs +
delta)
v2 =
Some n2
/\
mem_inj m f n1 n2.
Proof.
Lemma store_unmapped_inj:
forall m f chunk m1 b1 ofs v1 n1 m2,
mem_inj m f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
f b1 =
None ->
mem_inj m f n1 m2.
Proof.
Lemma store_outside_inj:
forall m f m1 m2 chunk b ofs v m2',
mem_inj m 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 m f m1 m2'.
Proof.
Lemma storebytes_size_block:
forall m b o v m',
storebytes m b o v =
Some m' ->
size_block m' =
size_block m.
Proof.
unfold storebytes;
intros.
repeat (
revert H;
destr).
inv H;
simpl.
unfold size_block.
simpl.
auto.
Qed.
Lemma storebytes_mask:
forall m b o v m',
storebytes m b o v =
Some m' ->
mask m' =
mask m.
Proof.
unfold storebytes;
intros.
repeat (
revert H;
destr).
inv H;
simpl.
unfold mask.
simpl.
auto.
Qed.
Lemma storebytes_mk_block_list:
forall m b o v m',
storebytes m b o v =
Some m' ->
mk_block_list m' =
mk_block_list m.
Proof.
Lemma storebytes_size_mem:
forall m b o v m',
storebytes m b o v =
Some m' ->
size_mem m' =
size_mem m.
Proof.
Lemma size_block_storebytes:
forall m1 b1 ofs lv1 n1,
storebytes m1 b1 ofs lv1 =
Some n1 ->
forall b',
size_block n1 b' =
size_block m1 b'.
Proof.
intros.
unfold size_block,
get_size.
unfold storebytes in H.
repeat (
revert H;
destr).
inv H;
simpl in *.
congruence.
inv H;
simpl in *;
congruence.
inv H.
simpl in *.
congruence.
Qed.
Lemma storebytes_mapped_inj:
forall m f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
mem_inj m f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
meminj_no_overlap f m1 ->
f b1 =
Some (
b2,
delta) ->
list_forall2 (
memval_inject m f)
bytes1 bytes2 ->
Forall wt_memval bytes2 ->
exists n2,
storebytes m2 b2 (
ofs +
delta)
bytes2 =
Some n2
/\
mem_inj m f n1 n2.
Proof.
Lemma storebytes_unmapped_inj:
forall m f m1 b1 ofs bytes1 n1 m2,
mem_inj m f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
f b1 =
None ->
mem_inj m f n1 m2.
Proof.
Lemma storebytes_outside_inj:
forall m f m1 m2 b ofs bytes2 m2',
mem_inj m 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 m f m1 m2'.
Proof.
Lemma storebytes_empty_inj:
forall m f m1 b1 ofs1 m1'
m2 b2 ofs2 m2',
mem_inj m f m1 m2 ->
storebytes m1 b1 ofs1 nil =
Some m1' ->
storebytes m2 b2 ofs2 nil =
Some m2' ->
mem_inj m f m1'
m2'.
Proof.
Preservation of allocations
Lemma alloc_size_mem:
forall m1 lo hi m1'
b1
(
ALLOC:
alloc m1 lo hi =
Some (
m1',
b1)),
(
size_mem m1) <= (
size_mem m1').
Proof.
intros.
rewrite (
alloc_size_mem'
_ _ _ _ _ ALLOC).
generalize (
Zmax_bound_l 0 0
hi).
generalize (
align_le (
Z.max 0
hi) 8).
omega.
Qed.
Lemma alloc_left_unmapped_inj:
forall m f m1 m2 lo hi m1'
b1,
mem_inj m f m1 m2 ->
alloc m1 lo hi =
Some (
m1',
b1) ->
f b1 =
None ->
mem_inj m f m1'
m2.
Proof.
Definition inj_offset_aligned (
delta:
Z) (
size:
Z) :
Prop :=
forall chunk,
size_chunk chunk <=
size -> (
align_chunk chunk |
delta).
Lemma get_setN_inside:
forall vl ofs lo t,
lo <=
ofs <
lo +
Z.of_nat (
length vl) ->
Some (
ZMap.get ofs (
setN vl lo t)) =
nth_error vl (
Z.to_nat (
ofs -
lo)).
Proof.
induction vl;
simpl;
intros.
-
omega.
-
des (
zlt lo ofs).
rewrite IHvl by (
zify;
omega).
replace (
Z.to_nat (
ofs -
lo))
with (
S (
Z.to_nat (
ofs - (
lo + 1)))).
simpl.
auto.
zify.
repeat rewrite Z2Nat.id by omega.
omega.
replace lo with ofs by omega.
rewrite setN_outside by omega.
rewrite ZMap.gss.
replace (
ofs -
ofs)
with 0
by omega.
simpl.
reflexivity.
Qed.
Lemma nth_error_init_block':
forall n b cur ofs,
(
ofs <
n)%
nat ->
nth_error (
init_block'
n b cur)
ofs =
Some (
Symbolic (
Eval (
Eundef b (
Int.add cur (
Int.repr (
Z.of_nat ofs)))))
O).
Proof.
Lemma init_block_length:
forall n b i,
length (
init_block'
n b i) =
S n.
Proof.
induction n; simpl; intros; try omega.
rewrite IHn; omega.
Qed.
Lemma get_init_block:
forall ofs lo hi b,
lo <=
ofs <
hi ->
ZMap.get ofs (
init_block lo hi b) =
Symbolic (
Eval (
Eundef b (
Int.repr ofs)))
O.
Proof.
Lemma free_size_mem_wrong_bounds:
forall m1 lo hi m1'
b1
(
FREE:
free m1 b1 lo hi =
Some m1')
(
bnds:
bounds_of_block m1 b1 <> (
lo,
hi)),
size_mem m1 =
size_mem m1'.
Proof.
Lemma bounds_dec:
forall m b lo hi,
{
bounds_of_block m b = (
lo,
hi)} + {
bounds_of_block m b <> (
lo,
hi)}.
Proof.
decide equality.
Qed.
Preservation of drop_perm operations.
Lemma drop_perm_bounds:
forall m b lo hi p m',
drop_perm m b lo hi p =
Some m' ->
forall b',
bounds_of_block m b' =
bounds_of_block m'
b'.
Proof.
Lemma nat_mask_drop_perm:
forall m b lo hi p m'
b',
drop_perm m b lo hi p =
Some m' ->
nat_mask m b' =
nat_mask m'
b'.
Proof.
unfold drop_perm;
intros m b lo hi p m'
b'.
destr.
inv H.
unfold nat_mask.
f_equal.
Qed.
Lemma drop_perm_size_block:
forall m b o v p m',
drop_perm m b o v p =
Some m' ->
size_block m' =
size_block m.
Proof.
unfold drop_perm;
intros.
repeat (
revert H;
destr).
inv H;
simpl.
unfold size_block.
simpl.
auto.
Qed.
Lemma drop_perm_mask:
forall m b o v m'
p,
drop_perm m b o v p =
Some m' ->
mask m' =
mask m.
Proof.
unfold drop_perm;
intros.
repeat (
revert H;
destr).
inv H;
simpl.
unfold mask.
simpl.
auto.
Qed.
Lemma drop_perm_nextblock:
forall m b o v m'
p,
drop_perm m b o v p =
Some m' ->
nextblock m' =
nextblock m.
Proof.
unfold drop_perm;
intros.
repeat (
revert H;
destr).
inv H;
simpl.
unfold nextblock.
simpl.
auto.
Qed.
Lemma drop_perm_mk_block_list:
forall (
m m' :
mem) (
b :
block) (
lo hi :
Z) (
p :
permission),
drop_perm m b lo hi p =
Some m' ->
mk_block_list m =
mk_block_list m'.
Proof.
Lemma drop_perm_size_mem:
forall m m'
b lo hi p,
drop_perm m b lo hi p =
Some m' ->
(
size_mem m) = (
size_mem m').
Proof.
Lemma size_block_drop:
forall m b lo hi p m',
drop_perm m b lo hi p =
Some m' ->
forall b',
size_block m'
b' =
size_block m b'.
Proof.
Lemma drop_unmapped_inj:
forall m f m1 m2 b lo hi p m1',
mem_inj m f m1 m2 ->
drop_perm m1 b lo hi p =
Some m1' ->
f b =
None ->
mem_inj m f m1'
m2.
Proof.
Lemma drop_mapped_inj:
forall m f m1 m2 b1 b2 delta lo hi p m1',
mem_inj m 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 m f m1'
m2'.
Proof.
Lemma drop_outside_inj:
forall m f m1 m2 b lo hi p m2',
mem_inj m 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 m f m1 m2'.
Proof.
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' (
m:
Val.partial_undef_allocation) (
m1 m2:
mem) :
Prop :=
mk_extends {
mext_next:
nextblock m1 =
nextblock m2;
mext_inj:
mem_inj m inject_id m1 m2
}.
Definition extends :=
extends'.
Theorem extends_refl:
forall m,
extends (
fun _ _ =>
None)
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.
split.
omega.
apply Z.divide_0_r.
-
intros.
unfold inject_id in H;
inv H.
replace (
ofs + 0)
with ofs by omega.
generalize (
contents_wt_memval m b2 ofs).
unfold wt_memval.
destr.
inv H.
econstructor;
eauto.
apply Val.ei_id.
-
omega.
Qed.
Lemma expr_inject_lessdef:
forall v1 v2 m,
Val.expr_inject m inject_id v1 v2 <->
Val.lessdef m v1 v2.
Proof.
Theorem load_extends:
forall m chunk m1 m2 b ofs v1,
extends m m1 m2 ->
load chunk m1 b ofs =
Some v1 ->
exists v2,
load chunk m2 b ofs =
Some v2 /\
Val.lessdef m v1 v2.
Proof.
intros.
inv H.
exploit load_inj;
eauto.
reflexivity.
intros [
v2 [
A B]].
exists v2;
split.
replace (
ofs + 0)
with ofs in A by omega.
auto.
auto.
Qed.
Theorem loadbytes_extends:
forall m m1 m2 b ofs len bytes1,
extends m m1 m2 ->
loadbytes m1 b ofs len =
Some bytes1 ->
exists bytes2,
loadbytes m2 b ofs len =
Some bytes2
/\
list_forall2 (
memval_lessdef m)
bytes1 bytes2.
Proof.
intros.
inv H.
replace ofs with (
ofs + 0)
by omega.
eapply loadbytes_inj;
eauto.
Qed.
Theorem store_within_extends:
forall m chunk m1 m2 b ofs v1 m1'
v2,
extends m m1 m2 ->
store chunk m1 b ofs v1 =
Some m1' ->
Val.lessdef m v1 v2 ->
exists m2',
store chunk m2 b ofs v2 =
Some m2'
/\
extends m 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.
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 m chunk m1 m2 b ofs v m2',
extends m 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 m m1 m2'.
Proof.
Theorem storebytes_within_extends:
forall m m1 m2 b ofs bytes1 m1'
bytes2,
extends m m1 m2 ->
storebytes m1 b ofs bytes1 =
Some m1' ->
list_forall2 (
memval_lessdef m)
bytes1 bytes2 ->
Forall wt_memval bytes2 ->
exists m2',
storebytes m2 b ofs bytes2 =
Some m2'
/\
extends m m1'
m2'.
Proof.
Theorem storebytes_outside_extends:
forall m m1 m2 b ofs bytes2 m2',
extends m 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 m m1 m2'.
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 unsigned machine integers;
-
pointers that could be represented using unsigned machine integers remain
representable after the injection.
Opaque Z.add.
Lemma size_sup_one_block:
forall m bs b z0
(
BS:
bs #
b =
Some (0,
z0))
(
PLE: ((
Pos.to_nat b) <=
m)%
nat)
,
z0 <=
size_mem_aux
(
mk_block_list_aux (
get_size bs)
m).
Proof.
Lemma in_bound_rep:
forall m b o,
in_bound o (
bounds_of_block m b) ->
0 <=
o <
Int.max_unsigned.
Proof.
This is now provable and not needed as an invariant.
Lemma mi_representable':
forall m f m1 m2
(
MI:
mem_inj m f m1 m2),
forall b b'
delta ofs
(
FB:
f b =
Some(
b',
delta))
(
PERM:
in_bound (
Int.unsigned ofs) (
bounds_of_block m1 b) \/
in_bound (
Int.unsigned ofs - 1) (
bounds_of_block m1 b))
(
delta_pos:
delta >= 0),
0 <=
Int.unsigned ofs +
delta <=
Int.max_unsigned.
Proof.
Lemma mi_representable:
forall m f m1 m2
(
MI:
mem_inj m f m1 m2),
forall b b'
delta ofs
(
FB:
f b =
Some(
b',
delta))
(
PERM:
perm m1 b (
Int.unsigned ofs)
Max Nonempty \/
perm m1 b (
Int.unsigned ofs - 1)
Max Nonempty)
(
delta_pos:
delta >= 0),
0 <=
Int.unsigned ofs +
delta <=
Int.max_unsigned.
Proof.
intros.
eapply mi_representable';
eauto.
destruct PERM as [
PERM|
PERM]; [
left|
right];
apply perm_bounds in PERM;
auto.
Qed.
Record inject' (
m:
Val.partial_undef_allocation) (
f:
meminj) (
m1 m2:
mem) :
Prop :=
mk_inject {
mi_inj:
mem_inj m 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_freeblocks_undef:
(* freeblocks may not be specialized *)
forall b o,
~
valid_block m1 b ->
m b o =
None;
mi_no_overlap':
meminj_no_overlap'
f m1;
mi_delta_pos:
(* the mi_representable is derivable from mi_delta_pos and mi_inj *)
forall b b'
delta,
f b =
Some(
b',
delta) ->
delta >= 0
}.
Definition inject :=
inject'.
Local Hint Resolve mi_mappedblocks:
mem.
Lemma meminj_no_overlap_impl:
forall f m,
Mem.meminj_no_overlap'
f m ->
Mem.meminj_no_overlap f m.
Proof.
intros f m MNO.
red in MNO;
red.
intros b1 b1'
delta1 b2 b2'
delta2 ofs1 ofs2 diff FB1 FB2 P1 P2.
apply Mem.perm_bounds in P1.
apply Mem.perm_bounds in P2.
specialize (
MNO b1 b1'
delta1 b2 b2'
delta2 ofs1 ofs2 diff FB1 FB2 P1 P2).
auto.
Qed.
Lemma inject_meminj_no_overlap:
forall p f m1 m2,
inject p f m1 m2 ->
meminj_no_overlap f m1.
Proof.
Preservation of access validity and pointer validity
Theorem valid_block_inject_1:
forall m f m1 m2 b1 b2 delta,
f b1 =
Some(
b2,
delta) ->
inject m f m1 m2 ->
valid_block m1 b1.
Proof.
Theorem valid_block_inject_2:
forall m f m1 m2 b1 b2 delta,
f b1 =
Some(
b2,
delta) ->
inject m f m1 m2 ->
valid_block m2 b2.
Proof.
Local Hint Resolve valid_block_inject_1 valid_block_inject_2:
mem.
Theorem perm_inject:
forall m f m1 m2 b1 b2 delta ofs k p,
f b1 =
Some(
b2,
delta) ->
inject m 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 m f m1 m2 b1 b2 delta lo hi k p,
f b1 =
Some(
b2,
delta) ->
inject m 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 m f m1 m2 chunk b1 ofs b2 delta p,
f b1 =
Some(
b2,
delta) ->
inject m f m1 m2 ->
valid_access m1 chunk b1 ofs p ->
valid_access m2 chunk b2 (
ofs +
delta)
p.
Proof.
Theorem valid_pointer_inject:
forall m f m1 m2 b1 ofs b2 delta,
f b1 =
Some(
b2,
delta) ->
inject m f m1 m2 ->
valid_pointer m1 b1 ofs =
true ->
valid_pointer m2 b2 (
ofs +
delta) =
true.
Proof.
Theorem weak_valid_pointer_inject:
forall m f m1 m2 b1 ofs b2 delta,
f b1 =
Some(
b2,
delta) ->
inject m f m1 m2 ->
weak_valid_pointer m1 b1 ofs =
true ->
weak_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 m f m1 m2 b1 ofs1 b2 delta p,
inject m f m1 m2 ->
perm m1 b1 (
Int.unsigned ofs1)
Cur p ->
f b1 =
Some (
b2,
delta) ->
Int.unsigned (
Int.add ofs1 (
Int.repr delta)) =
Int.unsigned ofs1 +
delta.
Proof.
Lemma address_inject':
forall m f m1 m2 chunk b1 ofs1 b2 delta,
inject m 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 weak_valid_pointer_inject_no_overflow:
forall m f m1 m2 b ofs b'
delta,
inject m f m1 m2 ->
weak_valid_pointer m1 b (
Int.unsigned ofs) =
true ->
f b =
Some(
b',
delta) ->
0 <=
Int.unsigned ofs +
Int.unsigned (
Int.repr delta) <=
Int.max_unsigned.
Proof.
Theorem valid_pointer_inject_no_overflow:
forall m f m1 m2 b ofs b'
delta,
inject m f m1 m2 ->
valid_pointer m1 b (
Int.unsigned ofs) =
true ->
f b =
Some(
b',
delta) ->
0 <=
Int.unsigned ofs +
Int.unsigned (
Int.repr delta) <=
Int.max_unsigned.
Proof.
Theorem valid_pointer_inject_val:
forall m f m1 m2 b ofs b'
ofs',
inject m f m1 m2 ->
valid_pointer m1 b (
Int.unsigned ofs) =
true ->
Val.expr_inject m f (
Eval (
Eptr b ofs)) (
Eval (
Eptr b'
ofs')) ->
valid_pointer m2 b' (
Int.unsigned ofs') =
true.
Proof.
Theorem weak_valid_pointer_inject_val:
forall m f m1 m2 b ofs b'
ofs',
inject m f m1 m2 ->
weak_valid_pointer m1 b (
Int.unsigned ofs) =
true ->
Val.expr_inject m f (
Eval (
Eptr b ofs)) (
Eval (
Eptr b'
ofs')) ->
weak_valid_pointer m2 b' (
Int.unsigned ofs') =
true.
Proof.
Theorem inject_no_overlap:
forall m f m1 m2 b1 b2 b1'
b2'
delta1 delta2 ofs1 ofs2,
inject m 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.
Theorem different_pointers_inject:
forall p f m m'
b1 ofs1 b2 ofs2 b1'
delta1 b2'
delta2,
inject p 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 p f m m'
b1 b1'
delta1 b2 b2'
delta2 ofs1 ofs2 sz,
inject p 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 inject_meminj_no_overlap;
eauto.
instantiate (1 :=
x -
delta1).
apply H2.
omega.
instantiate (1 :=
x -
delta2).
apply H3.
omega.
intuition.
Qed.
Theorem aligned_area_inject:
forall p f m m'
b ofs al sz b'
delta,
inject p f m m' ->
al = 1 \/
al = 2 \/
al = 4 \/
al = 8 ->
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 p f m1 m2 chunk b1 ofs b2 delta v1,
inject p 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.expr_inject p f v1 v2.
Proof.
intros.
inv H.
eapply load_inj;
eauto.
Qed.
Definition id_pua :
Val.partial_undef_allocation :=
fun _ _ =>
None.
Lemma bounds_of_block_alloc_eq:
forall m lo hi b m',
alloc m lo hi =
Some (
m',
b) ->
forall b',
bounds_of_block m'
b' =
if eq_block b'
b
then (0,
hi)
else if plt b' (
nextblock m')
then bounds_of_block m b'
else (0,0).
Proof.
Lemma alloc_0_inject:
forall tm1 tm2 sp f1 m2,
alloc tm1 0 0 =
Some (
tm2,
sp) ->
inject id_pua f1 m2 tm1 ->
inject id_pua f1 m2 tm2.
Proof.
Lemma alignment_inj:
forall i i0 i1 i2
(
A :
Int.and i (
Int.not (
Int.repr (
two_power_nat i0 - 1))) =
i)
(
B :
Int.and (
Int.not (
Int.repr (
two_power_nat i0 - 1)))
(
Int.not (
Int.repr (
two_power_nat i1 - 1))) =
Int.not (
Int.repr (
two_power_nat i0 - 1)))
(
C :
Int.and i2 (
Int.not (
Int.repr (
two_power_nat i1 - 1))) =
i2),
Int.and (
Int.add i i2) (
Int.not (
Int.repr (
two_power_nat i1 - 1))) =
Int.add i i2.
Proof.
Lemma int_add_rew:
forall a b,
Int.repr (
Int.unsigned a +
Int.unsigned b) =
Int.add a b.
Proof.
Lemma two_p_abs:
forall n n0,
(
n >=
n0)%
nat ->
Int.and (
Int.not (
Int.repr (
two_power_nat n - 1)))
(
Int.not (
Int.repr (
two_power_nat n0 - 1))) =
Int.not (
Int.repr (
two_power_nat n - 1)).
Proof.
Definition all_blocks_injected (
f:
meminj) (
m:
mem) :
Prop :=
forall b lo hi,
bounds_of_block m b = (
lo,
hi) ->
hi -
lo <> 0 ->
f b <>
None.
Lemma abi_in_bound:
forall f m b o
(
ABI :
all_blocks_injected f m)
(
IB :
in_bound (
Int.unsigned o) (
bounds_of_block m b))
(
Fnone :
f b =
None),
False.
Proof.
intros.
destruct (
bounds_of_block m b)
eqn:?.
specialize (
ABI b _ _ Heqp ).
destruct (
zeq (
z0 -
z) 0).
unfold in_bound in IB.
simpl in IB.
omega.
apply ABI;
auto.
Qed.
Lemma int_add_diff_range_plus:
forall o z o'
z0 i,
o +
z <>
o' +
z0 ->
z0 >= 0 ->
z >= 0 ->
0 <=
o' +
z0 <=
Int.modulus - 1 ->
0 <=
o +
z <=
Int.modulus - 1 ->
((
i +
z)
mod Int.modulus +
o)
mod Int.modulus <>
((
i +
z0)
mod Int.modulus +
o')
mod Int.modulus.
Proof.
intros.
rewrite !
Zplus_mod_idemp_l.
revert H.
revert H2 H3.
replace (
i+
z+
o)
with (
i + (
o +
z))
by omega.
replace (
i+
z0+
o')
with (
i + (
o' +
z0))
by omega.
generalize (
o +
z) (
o' +
z0).
clear.
intros.
intro.
unf_modulus.
elim_div.
lia.
Qed.
Lemma compat_inject:
forall p f m m'
(
ABI:
all_blocks_injected f m)
(
INJ :
inject p f m m')
al
(
COMP:
compat al (
bounds_of_block m') (
nat_mask m')),
compat (
Val.inj_alloc al f) (
bounds_of_block m) (
nat_mask m).
Proof.
Lemma norm_inject:
forall p f m m'
e1 v1 e1'
(
ABI:
all_blocks_injected f m)
(
INJ:
inject p f m m')
(
EI:
Val.expr_inject p f e1 e1')
(
NU:
v1 <>
Vundef),
forall r (
MN:
mem_norm m e1 r =
v1),
mem_norm m'
e1'
r <>
Vundef /\
Val.expr_inject p f (
Eval (
sval_of_val v1)) (
Eval (
sval_of_val (
mem_norm m'
e1'
r))).
Proof.
Lemma expr_val_inject:
forall p f v1 v2,
Val.expr_inject p f (
Eval (
sval_of_val v1))
(
Eval (
sval_of_val v2)) ->
val_inject f v1 v2.
Proof.
intros p f v1 v2 EI.
destruct v1;
destruct v2;
inv EI;
simpl in *;
try constructor;
inv inj_ok;
try constructor;
unfold Val.inj_ptr in *;
destruct (
f b)
as [[
b'
delta]|]
eqn:?;
simpl in *;
inv H0.
econstructor;
eauto.
Qed.
Lemma norm_inject_val':
forall p f m m'
e1 e1'
r
(
ABI:
all_blocks_injected f m)
(
INJ:
inject p f m m')
(
EI:
Val.expr_inject p f e1 e1'),
val_inject f (
mem_norm m e1 r) (
mem_norm m'
e1'
r).
Proof.
Theorem loadv_inject:
forall p f m1 m2 chunk a1 a2 v1
(
ABI:
all_blocks_injected f m1),
inject p f m1 m2 ->
loadv chunk m1 a1 =
Some v1 ->
Val.expr_inject p f a1 a2 ->
exists v2,
loadv chunk m2 a2 =
Some v2 /\
Val.expr_inject p f v1 v2.
Proof.
Theorem loadbytes_inject:
forall p f m1 m2 b1 ofs len b2 delta bytes1,
inject p 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 p f)
bytes1 bytes2.
Proof.
Preservation of stores
Theorem store_mapped_inject:
forall p f chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
inject p f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
f b1 =
Some (
b2,
delta) ->
Val.expr_inject p f v1 v2 ->
exists n2,
store chunk m2 b2 (
ofs +
delta)
v2 =
Some n2
/\
inject p f n1 n2.
Proof.
Theorem storev_inject:
forall p f m1 m2 chunk a1 a2 b1 b2 v1
(
ABI:
all_blocks_injected f m1),
inject p f m1 m2 ->
storev chunk m1 a1 b1 =
Some v1 ->
Val.expr_inject p f a1 a2 ->
Val.expr_inject p f b1 b2 ->
exists v2,
storev chunk m2 a2 b2 =
Some v2 /\
inject p f v1 v2.
Proof.
Theorem store_unmapped_inject:
forall p f chunk m1 b1 ofs v1 n1 m2,
inject p f m1 m2 ->
store chunk m1 b1 ofs v1 =
Some n1 ->
f b1 =
None ->
inject p f n1 m2.
Proof.
Theorem store_outside_inject:
forall p f m1 m2 chunk b ofs v m2',
inject p 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 p f m1 m2'.
Proof.
intros.
inversion H.
constructor;
eauto with mem.
eapply store_outside_inj;
eauto.
Qed.
Theorem storev_mapped_inject:
forall p f chunk m1 a1 v1 n1 m2 a2 v2
(
ABI:
all_blocks_injected f m1),
inject p f m1 m2 ->
storev chunk m1 a1 v1 =
Some n1 ->
Val.expr_inject p f a1 a2 ->
Val.expr_inject p f v1 v2 ->
exists n2,
storev chunk m2 a2 v2 =
Some n2 /\
inject p f n1 n2.
Proof.
Theorem storebytes_mapped_inject:
forall p f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
inject p f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
f b1 =
Some (
b2,
delta) ->
list_forall2 (
memval_inject p f)
bytes1 bytes2 ->
Forall wt_memval bytes2 ->
exists n2,
storebytes m2 b2 (
ofs +
delta)
bytes2 =
Some n2
/\
inject p f n1 n2.
Proof.
Theorem storebytes_unmapped_inject:
forall p f m1 b1 ofs bytes1 n1 m2,
inject p f m1 m2 ->
storebytes m1 b1 ofs bytes1 =
Some n1 ->
f b1 =
None ->
inject p f n1 m2.
Proof.
Theorem storebytes_outside_inject:
forall p f m1 m2 b ofs bytes2 m2',
inject p 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 p f m1 m2'.
Proof.
Theorem storebytes_empty_inject:
forall p f m1 b1 ofs1 m1'
m2 b2 ofs2 m2',
inject p f m1 m2 ->
storebytes m1 b1 ofs1 nil =
Some m1' ->
storebytes m2 b2 ofs2 nil =
Some m2' ->
inject p f m1'
m2'.
Proof.
Theorem alloc_left_unmapped_inject:
forall p f m1 m2 lo hi m1'
b1,
inject p f m1 m2 ->
alloc m1 lo hi =
Some (
m1',
b1) ->
exists f',
inject p 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 eq_block b b1 then None else f b).
assert (
inject_incr f f').
{
red;
unfold f';
intros.
destruct (
eq_block b b1).
subst b.
assert (
f b1 =
None).
eauto with mem.
congruence.
auto.
}
assert (
mem_inj p f'
m1 m2).
{
inversion mi_inj0;
constructor;
eauto with mem.
-
unfold f';
intros.
destruct (
eq_block b0 b1).
congruence.
eauto.
-
unfold f';
intros.
destruct (
eq_block b0 b1).
congruence.
eauto.
-
unfold f';
intros.
destruct (
eq_block b b1).
congruence.
eauto.
-
unfold f';
intros.
destruct (
eq_block b0 b1).
congruence.
apply memval_inject_incr with f;
auto.
}
exists f';
split.
constructor;
eauto.
-
eapply alloc_left_unmapped_inj;
eauto.
unfold f';
apply dec_eq_true.
-
intros.
unfold f'.
destruct (
eq_block b b1).
auto.
apply mi_freeblocks0.
red;
intro;
elim H3.
eauto with mem.
-
unfold f';
intros.
destruct (
eq_block b b1).
congruence.
eauto.
-
intros.
apply mi_freeblocks_undef0.
intro A.
eapply valid_block_alloc in A;
eauto.
-
unfold f';
red;
intros.
destruct (
eq_block b0 b1);
destruct (
eq_block b2 b1);
try congruence.
eapply mi_no_overlap'0.
eexact H3.
eauto.
eauto.
erewrite <-
bounds_of_block_alloc_other in H6;
eauto.
erewrite <-
bounds_of_block_alloc_other in H7;
eauto.
-
unfold f';
intros.
destruct (
eq_block b b1);
try discriminate.
eauto.
-
split;
auto.
split.
unfold f';
apply dec_eq_true.
intros;
unfold f';
apply dec_eq_false;
auto.
Qed.
Lemma alignment_of_size_inj:
forall n n0,
Z.max 0
n >=
Z.max 0
n0 ->
(
alignment_of_size n >=
alignment_of_size n0)%
nat.
Proof.
Lemma ioa_div:
forall sz delta,
inj_offset_aligned delta sz ->
(
two_p (
Z.of_nat (
alignment_of_size sz)) |
delta).
Proof.
Lemma alloc_left_mapped_inj:
forall m f m1 m2 lo hi m1'
b1 b2 delta
(
Hmi:
forall ofs b2 delta,
lo <=
ofs <
hi ->
f (
nextblock m1) =
Some (
b2,
delta) ->
memval_inject
m f
(
Symbolic (
Eval (
Eundef (
nextblock m1) (
Int.repr ofs))) 0)
(
ZMap.get (
ofs +
delta) (
mem_contents m2) #
b2))
(
msk_b2: (
mem_mask m2) #
b2 <>
None),
mem_inj m f m1 m2 ->
lo = 0 ->
alloc m1 lo hi =
Some (
m1',
b1) ->
valid_block m2 b2 ->
inj_offset_aligned delta 8 ->
(
forall ofs k p,
lo <=
ofs <
hi ->
perm m2 b2 (
ofs +
delta)
k p) ->
(
forall ofs,
lo <=
ofs <
hi ->
in_bound (
ofs+
delta) (
bounds_of_block m2 b2)) ->
f b1 =
Some(
b2,
delta) ->
mem_inj m f m1'
m2.
Proof.
Theorem memval_inject_alloc_left_mapped:
forall p f m1 m2 lo hi m1'
b1 b2 delta
(
ALLOC:
alloc m1 lo hi =
Some (
m1',
b1))
(
VB:
valid_block m2 b2)
(
RANGE: 0 <=
delta <=
Int.max_unsigned)
(
INJ:
mem_inj p f m1 m2)
(
VB_none:
forall b :
block, ~
valid_block m1 b ->
f b =
None)
(
vb_none:
forall b o, ~
valid_block m1 b ->
p b o =
None)
(
INJ':
mem_inj p (
fun b :
positive =>
if eq_block b b1 then Some (
b2,
delta)
else f b)
m1 m2)
(
ofs :
Z) (
b0 :
block) (
delta0 :
Z)
(
RANGE':
lo <=
ofs <
hi)
(
f'
eq: (
if eq_block (
nextblock m1)
b1 then Some (
b2,
delta)
else f (
nextblock m1)) =
Some (
b0,
delta0))
(
contents:
forall ofs,
lo <=
ofs <
hi ->
ZMap.get (
ofs +
delta) (
mem_contents m2) #
b0 =
Symbolic (
Eval (
Eundef b0 (
Int.repr (
ofs+
delta))))
O),
memval_inject p
(
fun b :
block =>
if eq_block b b1 then Some (
b2,
delta)
else f b)
(
Symbolic (
Eval (
Eundef (
nextblock m1) (
Int.repr ofs))) 0)
(
ZMap.get (
ofs +
delta0) (
mem_contents m2) #
b0).
Proof.
Lemma mask_alloc_old:
forall m1 lo hi m1'
b1,
alloc m1 lo hi =
Some (
m1',
b1) ->
mask m1 b1 =
O.
Proof.
Lemma nat_mask_alloc_old:
forall m1 lo hi m1'
b1,
alloc m1 lo hi =
Some (
m1',
b1) ->
nat_mask m1 b1 =
Int.mone.
Proof.
Theorem alloc_left_mapped_inject_aux_mem_inj:
forall p f m1 m2 lo hi m1'
b1 b2 delta
(
INJ:
inject p f m1 m2)
(
lo0:
lo = 0)
(
ALLOC:
alloc m1 lo hi =
Some (
m1',
b1))
(
VB:
valid_block m2 b2)
(
MSKb2: (
mem_mask m2) #
b2 <>
None)
(
DMU: 0 <=
delta <=
Int.max_unsigned)
(
PERM_MU:
forall ofs k p,
perm m2 b2 ofs k p ->
delta = 0 \/ 0 <=
ofs <
Int.max_unsigned)
(
BND_PERM:
forall ofs k p,
lo <=
ofs <
hi ->
perm m2 b2 (
ofs +
delta)
k p)
(
IOA:
inj_offset_aligned delta 8)
(
space_free:
forall b delta'
ofs k p,
f b =
Some (
b2,
delta') ->
perm m1 b ofs k p ->
lo +
delta <=
ofs +
delta' <
hi +
delta ->
False)
(
Hmi:
forall ofs,
lo <=
ofs <
hi ->
ZMap.get (
ofs +
delta) (
mem_contents m2) #
b2 =
Symbolic (
Eval (
Eundef b2 (
Int.repr (
ofs+
delta))))
O),
mem_inj p (
fun b =>
if eq_block b b1 then Some(
b2,
delta)
else f b)
m1'
m2.
Proof.
Theorem alloc_left_mapped_inject_aux:
forall p f m1 m2 lo hi m1'
b1 b2 delta
(
INJ:
inject p f m1 m2)
(
lo0:
lo = 0)
(
ALLOC:
alloc m1 lo hi =
Some (
m1',
b1))
(
VB:
valid_block m2 b2)
(
MSKb2: (
mem_mask m2) #
b2 <>
None)
(
DMU: 0 <=
delta <=
Int.max_unsigned)
(
PERM_MU:
forall ofs k p,
perm m2 b2 ofs k p ->
delta = 0 \/ 0 <=
ofs <
Int.max_unsigned)
(
BND_PERM:
forall ofs k p,
lo <=
ofs <
hi ->
perm m2 b2 (
ofs +
delta)
k p)
(
IOA:
inj_offset_aligned delta 8)
(
space_free_perm:
forall b delta'
ofs k p,
f b =
Some (
b2,
delta') ->
perm m1 b ofs k p ->
lo +
delta <=
ofs +
delta' <
hi +
delta ->
False)
(
space_free_bnd:
forall b delta'
ofs,
f b =
Some (
b2,
delta') ->
in_bound ofs (
bounds_of_block m1 b) ->
lo +
delta <=
ofs +
delta' <
hi +
delta ->
False)
(
Hmi:
forall ofs :
Z,
lo <=
ofs <
hi ->
ZMap.get (
ofs +
delta) (
mem_contents m2) #
b2 =
Symbolic (
Eval (
Eundef b2 (
Int.repr (
ofs +
delta)))) 0)
(
BND_MU:
forall ofs,
in_bound ofs (
bounds_of_block m2 b2) ->
delta = 0 \/ 0 <=
ofs <
Int.max_unsigned)
(
BND_bound:
forall ofs,
lo <=
ofs <
hi ->
in_bound (
ofs+
delta) (
bounds_of_block m2 b2)),
inject p (
fun b =>
if eq_block b b1 then Some(
b2,
delta)
else f b)
m1'
m2.
Proof.
intros.
inversion INJ.
set (
f' := (
fun b =>
if eq_block b b1 then Some(
b2,
delta)
else f b)).
constructor;
auto.
-
eapply alloc_left_mapped_inject_aux_mem_inj;
eauto.
-
unfold f';
intros b NVB.
destruct (
eq_block b b1).
subst b.
elim NVB.
eauto with mem.
eauto with mem.
-
unfold f';
intros.
destruct (
eq_block b b1).
congruence.
eauto.
-
intros.
apply mi_freeblocks_undef0.
intro A;
eapply valid_block_alloc in A;
eauto.
-
unfold f';
red.
intros b0 b1'
delta1 b3 b2'
delta2 ofs1 ofs2 b03 INJ1 INJ2 PERM1 PERM2.
erewrite bounds_of_block_alloc_eq in PERM1;
eauto.
erewrite bounds_of_block_alloc_eq in PERM2;
eauto.
destruct (
eq_block b0 b1);
destruct (
eq_block b3 b1).
+
congruence.
+
inv INJ1.
destruct (
plt b3 (
nextblock m1')).
destruct (
eq_block b1'
b2');
auto.
subst b2'.
right;
red;
intros.
eapply space_free_bnd;
eauto.
rewrite <-
H.
unfold in_bound in PERM1.
revert PERM1.
simpl.
intros;
omega.
unfold in_bound in PERM2.
revert PERM2.
simpl.
intros;
omega.
+
inv INJ2.
destruct (
plt b0 (
nextblock m1')).
destruct (
eq_block b1'
b2');
auto.
subst b2'.
right;
red;
intros.
eapply space_free_bnd;
eauto.
rewrite H.
unfold in_bound in PERM2.
revert PERM2.
simpl.
intros;
omega.
unfold in_bound in PERM1.
simpl in PERM1;
omega.
+
destruct (
plt b0 (
nextblock m1')).
destruct (
plt b3 (
nextblock m1')).
eauto.
unfold in_bound in PERM2.
simpl in PERM2;
omega.
unfold in_bound in PERM1.
simpl in PERM1;
omega.
-
intros b b'
delta0 INJ'.
destruct (
eq_block b b1).
subst.
injection INJ';
intros;
subst b'
delta0.
omega.
eauto.
Qed.
Definition block_undefs lo hi delta m2 b2 :=
forall ofs :
Z,
lo <=
ofs <
hi ->
ZMap.get (
ofs +
delta) (
mem_contents m2) #
b2 =
Symbolic (
Eval (
Eundef b2 (
Int.repr (
ofs +
delta)))) 0.
Theorem alloc_left_mapped_inject:
forall p f m1 m2 lo hi m1'
b1 b2 delta,
inject p f m1 m2 ->
lo = 0 ->
alloc m1 lo hi =
Some (
m1',
b1) ->
valid_block m2 b2 ->
(
mem_mask m2) #
b2 <>
None ->
0 <=
delta <=
Int.max_unsigned ->
(
forall ofs,
in_bound ofs (
bounds_of_block m2 b2) ->
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 8 ->
(
forall b delta'
ofs,
f b =
Some (
b2,
delta') ->
in_bound ofs (
bounds_of_block m1 b) ->
lo +
delta <=
ofs +
delta' <
hi +
delta ->
False) ->
block_undefs lo (
Z.max 0
hi)
delta m2 b2 ->
exists f',
inject p f'
m1'
m2
/\
inject_incr f f'
/\
f'
b1 =
Some(
b2,
delta)
/\ (
forall b,
b <>
b1 ->
f'
b =
f b).
Proof.
intros p f m1 m2 lo hi m1'
b1 b2 delta INJ lo0 ALLOC VB MSK_m2 delta_rep bnd_rep bnd_perm
ioa bnd_inj bu.
inversion INJ.
set (
f' :=
fun b =>
if eq_block b b1 then Some(
b2,
delta)
else f b).
assert (
inject_incr f f').
{
red;
unfold f';
intros.
destruct (
eq_block b b1).
subst b.
assert (
f b1 =
None).
eauto with mem.
congruence.
auto.
}
exists f'.
split.
eapply alloc_left_mapped_inject_aux;
eauto.
-
intros;
apply bnd_rep.
apply perm_bounds in H0.
auto.
-
intros.
eapply bnd_inj in H0;
eauto.
apply perm_bounds in H1;
auto.
-
intros.
eapply bu;
eauto.
split;
try omega.
cut (
hi <=
Z.max 0
hi).
omega.
apply Zmax_bound_r.
omega.
-
intros.
eapply bnd_perm with (
k:=
Cur) (
p:=
Freeable)
in H0;
eauto.
apply perm_bounds in H0.
auto.
-
unfold f'.
split;
auto.
split;
auto.
rewrite dec_eq_true;
auto.
intros;
rewrite dec_eq_false;
auto.
Qed.
Lemma mem_alloc_block_undefs:
forall m lo hi m'
b,
alloc m lo hi =
Some (
m',
b) ->
block_undefs 0
hi 0
m'
b.
Proof.
Lemma alloc_contents_old:
forall m1 lo hi m2 b
(
ALLOC:
alloc m1 lo hi =
Some (
m2,
b))
b'
(
DIFF:
b' <>
b),
(
mem_contents m2) #
b' = (
mem_contents m1) #
b'.
Proof.
Lemma align_distr:
forall z z1,
align z 8 +
align z1 8 =
align (
align z 8 +
z1) 8.
Proof.
Opaque align.
Lemma mk_block_list_aux_eq:
forall lo hi b'
bs ,
mk_block_list_aux
(
fun b0 :
block =>
get_size
(
PMap.set b' (
Some (
lo,
hi))
bs)
b0)
(
pred (
Pos.to_nat (
Pos.succ b'))) =
(
b',
hi-
lo)::
mk_block_list_aux
(
fun b0 =>
get_size bs b0)
(
pred (
Pos.to_nat b')).
Proof.
Lemma size_mem_inf_add_larger:
forall (
m1 m2 :
mem) (
p1 p2:
block) (
lo hi lo'
hi':
Z),
hi >= 0 ->
hi' >= 0 ->
hi >=
lo ->
hi' -
lo' >=
hi -
lo ->
size_mem_aux
(
mk_block_list_aux (
size_block m2)
(
pred (
Pos.to_nat p2))) <=
size_mem_aux
(
mk_block_list_aux (
size_block m1)
(
pred (
Pos.to_nat p1))) ->
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p2) (
Some (
lo,
hi)) (
mem_blocksize m2)))
(
Pos.to_nat p2)) <=
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p1) (
Some (
lo',
hi')) (
mem_blocksize m1)))
(
Pos.to_nat p1)).
Proof.
Lemma alloc_less_ok:
forall m z z0,
Mem.alloc m 0
z =
None ->
Mem.alloc m 0
z0 <>
None ->
0 <=
z <=
z0 ->
False.
Proof.
Lemma size_mem_inf_add':
forall (
m1 m2 :
mem) (
p1 p2:
block) (
lo hi :
Z),
hi >= 0 ->
lo <=
hi ->
size_mem_aux
(
mk_block_list_aux (
size_block m2)
(
pred (
Pos.to_nat p2))) <=
size_mem_aux
(
mk_block_list_aux (
size_block m1)
(
pred (
Pos.to_nat p1))) ->
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p2) (
Some (
lo,
hi)) (
mem_blocksize m2)))
(
Pos.to_nat (
p2))) <=
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p1) (
Some (
lo,
hi)) (
mem_blocksize m1)))
(
Pos.to_nat (
p1))).
Proof.
Lemma alloc_same_inj_inf:
forall m1 m2 lo hi m1'
b1
(
ALLOC :
alloc m1 lo hi =
Some (
m1',
b1))
m b
(
ALLOC2 :
alloc m2 lo hi =
Some (
m,
b))
(
inf :
size_mem m2 <=
size_mem m1)
(
Hpos:
hi >= 0),
size_mem m <=
size_mem m1'.
Proof.
intros.
apply alloc_size_mem' in ALLOC; auto.
apply alloc_size_mem' in ALLOC2; auto.
rewrite ALLOC. rewrite ALLOC2.
omega.
Qed.
Lemma alloc_parallel_inj:
forall p f m1 m2 lo hi m1'
b1 m b
(
INJ:
inject p f m1 m2)
(
ALLOC:
alloc m1 lo hi =
Some (
m1',
b1))
(
HIpos :
hi >= 0)
(
ALLOC2 :
alloc m2 lo hi =
Some (
m,
b)),
mem_inj p (
fun b0 :
positive =>
if peq b0 b1 then Some (
b, 0)
else f b0)
m1'
m.
Proof.
Lemma less_alloc_less:
forall m1 m2 hi
(
ALLOC :
alloc m1 0
hi <>
None)
(
HIpos :
hi >= 0)
(
NALLOC :
alloc m2 0
hi =
None)
(
sizes:
size_mem m2 <=
size_mem m1),
False.
Proof.
intros m1 m2 hi.
unfold alloc,
low_alloc.
destr.
revert NALLOC;
destr.
clear ALLOC.
clear Heqs Heqs0 NALLOC.
unfold conc_mem_alloc in n,
e.
unfold alloc_blocks in n,
e.
repeat (
revert n;
destr).
repeat (
revert e;
destr).
clear e Heqs0 n Heqs.
apply alloc_size_mem_aux in Heqp;
apply alloc_size_mem_aux in Heqp0.
cut (
z1 <=
z);
try omega.
subst.
clear g l.
apply size_mem_inf_add';
auto;
try omega;
try xomega.
Qed.
Theorem alloc_parallel_inject:
forall p f m1 m2 lo1 hi1 m1'
b1 (
ORD:
lo1 <=
hi1)
(
INJ:
inject p f m1 m2)
(
ALLOC:
alloc m1 lo1 hi1 =
Some (
m1',
b1))
(
HIpos:
hi1 >= 0),
exists f',
exists m2',
exists b2,
alloc m2 lo1 hi1 =
Some (
m2',
b2)
/\
inject p f'
m1'
m2'
/\
inject_incr f f'
/\
f'
b1 =
Some(
b2, 0)
/\ (
forall b,
b <>
b1 ->
f'
b =
f b).
Proof.
intros.
destruct (
alloc m2 lo1 hi1)
eqn:?.
-
destruct p0.
exists (
fun b0 =>
if peq b0 b1 then Some (
b,0)
else f b0).
exists m.
exists b.
intuition.
+
constructor;
simpl;
intros;
eauto.
*
eapply alloc_parallel_inj;
eauto.
*
destr.
subst.
contradict H.
eapply valid_new_block;
eauto.
inv INJ;
auto.
apply mi_freeblocks0;
auto.
intro A.
apply (
valid_block_alloc _ _ _ _ _ ALLOC)
in A.
congruence.
*
inv INJ;
eauto.
revert H;
destr;
subst.
inv H.
apply valid_new_block in Heqo;
auto.
apply mi_mappedblocks0 in H;
auto.
eapply valid_block_alloc in H;
eauto.
*
inv INJ.
apply mi_freeblocks_undef0.
intro A.
eapply valid_block_alloc in A;
eauto.
*
inv INJ.
red.
intros b0 b1'
delta1 b2 b2'
delta2 ofs1 ofs2 diff F0 F2 i0 i2.
{
des (
peq b0 b1).
des (
peq b2 b1).
-
left.
inv F0.
intro;
subst.
apply mi_mappedblocks0 in F2.
apply (
fresh_block_alloc _ _ _ _ _ Heqo)
in F2;
auto.
-
des (
peq b2 b1).
inv F2.
+
left.
intro;
subst.
apply mi_mappedblocks0 in F0.
apply (
fresh_block_alloc _ _ _ _ _ Heqo)
in F0;
auto.
+
red in mi_no_overlap'0.
apply (
mi_no_overlap'0
_ _ _ _ _ _ _ _ diff);
eauto.
rewrite <- (
bounds_of_block_alloc_other _ _ _ _ _ ALLOC)
in i0;
auto.
rewrite <-(
bounds_of_block_alloc_other _ _ _ _ _ ALLOC)
in i2;
auto.
}
*
inv INJ.
destruct (
peq b0 b1);
subst;
auto.
inv H.
omega.
eauto.
+
unfold inject_incr.
intros.
des (
peq b0 b1).
rewrite mi_freeblocks with (
m:=
p) (
m1:=
m1) (
m2:=
m2)
in H;
auto.
congruence.
eapply fresh_block_alloc;
eauto.
+
rewrite peq_true.
auto.
+
rewrite peq_false;
auto.
-
exfalso.
subst.
rewrite alloc_lo_0 in *.
generalize (
mi_size_mem _ _ _ _ (
mi_inj _ _ _ _ INJ)).
refine (
less_alloc_less m1 m2 hi1 _ HIpos Heqo).
rewrite ALLOC;
congruence.
Qed.
Preservation of free operations
Lemma free_bounds:
forall m b lo hi m'
b',
free m b lo hi =
Some m' ->
bounds_of_block m'
b' =
bounds_of_block m b' \/
bounds_of_block m'
b' = (0,0).
Proof.
Lemma free_mask:
forall m b lo hi m'
b',
free m b lo hi =
Some m' ->
mask m'
b' =
mask m b' \/ (
mask m'
b' =
O /\
bounds_of_block m b' = (
lo,
hi)).
Proof.
intros m b lo hi m'
b'.
unfold free.
destr.
inv H.
rewrite unchecked_free_mask.
destr.
destr.
destr.
subst.
rewrite Heqp.
des (
zeq z lo);
des (
zeq z0 hi).
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;
simpl;
intros.
inv H.
auto.
destruct a as [[
b1 lo1]
hi1].
destruct (
free m b1 lo1 hi1)
as [
m1|]
eqn:
E;
try discriminate.
exploit IHl;
eauto.
intros [
A B].
split.
eauto with mem.
intros.
destruct H1.
inv H1.
elim (
perm_free_2 _ _ _ _ _ E ofs k p).
auto.
auto.
eauto.
Qed.
Lemma drop_outside_inject:
forall m f m1 m2 b lo hi p m2',
inject m 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 m f m1 m2'.
Proof.
Composing two memory injections.
Lemma mem_inj_compose:
forall p p'
f f'
m1 m2 m3
(
Ffree:
forall b, ~
valid_block m1 b ->
match f b with
|
None =>
True
|
Some (
b',
delta) => ~
valid_block m2 b'
end),
mem_inj p f m1 m2 ->
mem_inj p'
f'
m2 m3 ->
mem_inj (
Val.inj_m f p p') (
compose_meminj f f')
m1 m3.
Proof.
intros.
unfold compose_meminj.
inv H;
inv H0;
constructor;
intros;
eauto.
-
destruct (
f b1)
as [[
b'
delta'] |]
eqn:?;
try discriminate.
destruct (
f'
b')
as [[
b''
delta''] |]
eqn:?;
inv H.
replace (
ofs + (
delta' +
delta''))
with ((
ofs +
delta') +
delta'')
by omega.
eauto.
-
destruct (
f b1)
as [[
b'
delta'] |]
eqn:?;
try discriminate.
destruct (
f'
b')
as [[
b''
delta''] |]
eqn:?;
inv H.
replace (
ofs + (
delta' +
delta''))
with ((
ofs +
delta') +
delta'')
by omega.
eauto.
-
destruct (
f b)
as [[
b'
delta'] |]
eqn:?;
try discriminate.
destruct (
f'
b')
as [[
b''
delta''] |]
eqn:?;
inv H.
clear -
mi_align'0
mi_align'1
Heqo Heqo0 Ffree.
unfold nat_mask in *.
specialize (
mi_align'0
_ _ _ Heqo).
specialize (
mi_align'1
_ _ _ Heqo0).
destruct mi_align'1;
destruct mi_align'0.
split;
try omega.
apply Z.divide_add_r;
auto.
apply Z.divide_trans with (
two_p (
Z.of_nat (
mask m2 b')));
auto.
red.
exists (
two_p (
Z.of_nat (
mask m2 b') -
Z.of_nat (
mask m1 b))).
rewrite <-
two_p_is_exp by omega.
replace (
Z.of_nat (
mask m2 b') -
Z.of_nat (
mask m1 b) +
Z.of_nat (
mask m1 b))
with (
Z.of_nat (
mask m2 b'))
by omega.
auto.
-
destruct (
f b1)
as [[
b'
delta'] |]
eqn:?;
try discriminate.
destruct (
f'
b')
as [[
b''
delta''] |]
eqn:?;
inv H.
replace (
ofs + (
delta' +
delta''))
with ((
ofs +
delta') +
delta'')
by omega.
eapply memval_inject_compose;
eauto.
-
omega.
Qed.
Theorem inject_compose:
forall p p'
f f'
m1 m2 m3,
inject p f m1 m2 ->
inject p'
f'
m2 m3 ->
inject (
Val.inj_m f p p') (
compose_meminj f f')
m1 m3.
Proof.
unfold compose_meminj;
intros.
inv H;
inv H0.
constructor.
-
eapply mem_inj_compose;
eauto.
intros;
destr.
des p0.
rewrite mi_freeblocks0 in Heqo;
auto.
congruence.
-
intros.
erewrite mi_freeblocks0;
eauto.
-
intros.
destruct (
f b)
as [[
b1 delta1] |]
eqn:?;
try discriminate.
destruct (
f'
b1)
as [[
b2 delta2] |]
eqn:?;
inv H.
eauto.
-
intros.
unfold Val.inj_m.
rewrite mi_freeblocks_undef0;
auto.
rewrite mi_freeblocks0;
eauto.
-
red;
intros.
destruct (
f b1)
as [[
b1x delta1x] |]
eqn:?;
try discriminate.
destruct (
f'
b1x)
as [[
b1y delta1y] |]
eqn:?;
inv H0.
destruct (
f b2)
as [[
b2x delta2x] |]
eqn:?;
try discriminate.
destruct (
f'
b2x)
as [[
b2y delta2y] |]
eqn:?;
inv H1.
exploit mi_no_overlap'0;
eauto.
intros A.
destruct (
eq_block b1x b2x).
subst b1x.
destruct A.
congruence.
assert (
delta1y =
delta2y)
by congruence.
right;
omega.
exploit mi_no_overlap'1.
eauto.
eauto.
eauto.
eapply mi_bounds.
eauto.
eauto.
eauto.
eapply mi_bounds.
eauto.
eauto.
eauto.
intuition omega.
-
intros.
destruct (
f b)
as [[
b1 delta1] |]
eqn:?;
try discriminate.
destruct (
f'
b1)
as [[
b2 delta2] |]
eqn:?;
inv H.
specialize (
mi_delta_pos0 _ _ _ Heqo).
specialize (
mi_delta_pos1 _ _ _ Heqo0).
omega.
Qed.
Lemma val_lessdef_inject_compose:
forall p p'
f v1 v2 v3,
Val.lessdef p v1 v2 ->
Val.expr_inject p'
f v2 v3 ->
Val.expr_inject (
Val.inj_m inject_id p p')
f v1 v3.
Proof.
Lemma val_inject_lessdef_compose:
forall p p'
f v1 v2 v3,
Val.expr_inject p f v1 v2 ->
Val.lessdef p'
v2 v3 ->
Val.expr_inject (
Val.inj_m f p p')
f v1 v3.
Proof.
Injecting a memory into itself.
Definition flat_inj (
thr:
block) :
meminj :=
fun (
b:
block) =>
if plt b thr then Some(
b, 0)
else None.
Definition inject_neutral (
thr:
block) (
m:
mem) :=
mem_inj id_pua (
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 (
plt b1 thr);
inversion H0;
subst.
destruct (
plt b2 thr);
inversion H1;
subst.
auto.
Qed.
Theorem neutral_inject:
forall m,
inject_neutral (
nextblock m)
m ->
inject id_pua (
flat_inj (
nextblock m))
m m.
Proof.
Theorem empty_inject_neutral:
forall thr,
inject_neutral thr empty.
Proof.
intros thr;
red;
constructor;
eauto.
-
unfold flat_inj;
intros.
destruct (
plt b1 thr);
inv H.
replace (
ofs + 0)
with ofs by omega;
auto.
-
unfold flat_inj;
intros.
destruct (
plt b1 thr);
inv H.
replace (
ofs + 0)
with ofs by omega;
auto.
-
unfold flat_inj;
intros.
destruct (
plt b thr);
inv H.
split;
try omega.
unfold mask;
simpl.
rewrite PMap.gi.
simpl.
apply Z.divide_1_l.
-
intros.
apply perm_empty in H0.
exfalso;
auto.
-
omega.
Qed.
Theorem alloc_inject_neutral:
forall thr m lo hi b m'
(
ALLOC:
alloc m lo hi =
Some (
m',
b))
(
LO:
lo <= 0)
(
INJ:
inject_neutral thr m)
(
LT:
Plt (
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 ->
Plt b thr ->
Val.expr_inject id_pua (
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 ->
Plt b thr ->
inject_neutral thr m'.
Proof.
Invariance properties between two memory states
Section UNCHANGED_ON.
Variable P:
block ->
Z ->
Prop.
Record unchanged_on (
m_before m_after:
mem) :
Prop :=
mk_unchanged_on {
unchanged_on_perm:
forall b ofs k p,
P b ofs ->
valid_block m_before b ->
(
perm m_before b ofs k p <->
perm m_after b ofs k p);
unchanged_on_contents:
forall b ofs,
P b ofs ->
perm m_before b ofs Cur Readable ->
ZMap.get ofs (
PMap.get b m_after.(
mem_contents)) =
ZMap.get ofs (
PMap.get b m_before.(
mem_contents))
}.
Lemma unchanged_on_refl:
forall m,
unchanged_on m m.
Proof.
intros; constructor; tauto.
Qed.
Lemma perm_unchanged_on:
forall m m'
b ofs k p,
unchanged_on m m' ->
P b ofs ->
valid_block m b ->
perm m b ofs k p ->
perm m'
b ofs k p.
Proof.
intros. destruct H. apply unchanged_on_perm0; auto.
Qed.
Lemma perm_unchanged_on_2:
forall m m'
b ofs k p,
unchanged_on m m' ->
P b ofs ->
valid_block m b ->
perm m'
b ofs k p ->
perm m b ofs k p.
Proof.
intros. destruct H. apply unchanged_on_perm0; auto.
Qed.
Lemma loadbytes_unchanged_on_1:
forall m m'
b ofs n,
unchanged_on m m' ->
valid_block m b ->
(
forall i,
ofs <=
i <
ofs +
n ->
P b i) ->
loadbytes m'
b ofs n =
loadbytes m b ofs n.
Proof.
Lemma loadbytes_unchanged_on:
forall m m'
b ofs n bytes,
unchanged_on m m' ->
(
forall i,
ofs <=
i <
ofs +
n ->
P b i) ->
loadbytes m b ofs n =
Some bytes ->
loadbytes m'
b ofs n =
Some bytes.
Proof.
Lemma load_unchanged_on_1:
forall m m'
chunk b ofs,
unchanged_on m m' ->
valid_block m b ->
(
forall i,
ofs <=
i <
ofs +
size_chunk chunk ->
P b i) ->
load chunk m'
b ofs =
load chunk m b ofs.
Proof.
Lemma load_unchanged_on:
forall m m'
chunk b ofs v,
unchanged_on m m' ->
(
forall i,
ofs <=
i <
ofs +
size_chunk chunk ->
P b i) ->
load chunk m b ofs =
Some v ->
load chunk m'
b ofs =
Some v.
Proof.
Lemma store_unchanged_on:
forall chunk m b ofs v m',
store chunk m b ofs v =
Some m' ->
(
forall i,
ofs <=
i <
ofs +
size_chunk chunk -> ~
P b i) ->
unchanged_on m m'.
Proof.
Lemma storebytes_unchanged_on:
forall m b ofs bytes m',
storebytes m b ofs bytes =
Some m' ->
(
forall i,
ofs <=
i <
ofs +
Z_of_nat (
length bytes) -> ~
P b i) ->
unchanged_on m m'.
Proof.
Lemma alloc_unchanged_on:
forall m lo hi m'
b,
alloc m lo hi =
Some (
m',
b) ->
unchanged_on m m'.
Proof.
Lemma free_unchanged_on:
forall m b lo hi m',
free m b lo hi =
Some m' ->
(
forall i,
lo <=
i <
hi -> ~
P b i) ->
unchanged_on m m'.
Proof.
End UNCHANGED_ON.
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.unchanged_on_refl
:
mem.