Assertions on memory states, in the style of separation logic
This library defines a number of useful logical assertions about
CompCert memory states, such as "block b at offset ofs contains
value v". Assertions can be grouped using a separating conjunction
operator in the style of separation logic.
Currently, this library is used only in module Stackingproof
to reason about the shapes of stack frames generated during the
Stacking pass.
This is not a full-fledged separation logic because there is no
program logic (Hoare triples) to speak of. Also, there is no general
frame rule; instead, a weak form of the frame rule is provided
by the lemmas that help us reason about the logical assertions.
Require Import Setoid Program.Basics.
Require Import Coqlib Decidableplus.
Require Import AST Integers Values Memory Events Globalenvs.
Assertions about memory
An assertion is composed of:
-
a predicate over memory states (of type mem -> Prop)
-
a set of (block, offset) memory locations that represents the memory footprint of the assertion
-
a proof that the predicate is invariant by changes of memory outside of the footprint
-
a proof that the footprint contains only valid memory blocks.
This presentation (where the footprint is part of the assertion) makes
it possible to define separating conjunction without explicitly
defining a separation algebra over CompCert memory states (i.e. the
notion of splitting a memory state into two disjoint halves).
:
Type := {
m_pred :
mem ->
Prop;
m_footprint:
block ->
Z ->
Prop;
m_invar:
forall m m',
m_pred m ->
Mem.unchanged_on m_footprint m m' ->
m_pred m';
m_valid:
forall m b ofs,
m_pred m ->
m_footprint b ofs ->
Mem.valid_block m b
}.
Notation "
m |=
p" := (
m_pred p m) (
at level 74,
no associativity) :
sep_scope.
Implication and logical equivalence between memory predicates
Definition massert_imp (
P Q:
massert) :
Prop :=
(
forall m,
m_pred P m ->
m_pred Q m) /\ (
forall b ofs,
m_footprint Q b ofs ->
m_footprint P b ofs).
Definition massert_eqv (
P Q:
massert) :
Prop :=
massert_imp P Q /\
massert_imp Q P.
Remark massert_imp_refl:
forall p,
massert_imp p p.
Proof.
Remark massert_imp_trans:
forall p q r,
massert_imp p q ->
massert_imp q r ->
massert_imp p r.
Proof.
Remark massert_eqv_refl:
forall p,
massert_eqv p p.
Proof.
Remark massert_eqv_sym:
forall p q,
massert_eqv p q ->
massert_eqv q p.
Proof.
Remark massert_eqv_trans:
forall p q r,
massert_eqv p q ->
massert_eqv q r ->
massert_eqv p r.
Proof.
Record massert_eqv and massert_imp as relations so that they can be used by rewriting tactics.
Add Relation massert massert_imp
reflexivity proved by massert_imp_refl
transitivity proved by massert_imp_trans
as massert_imp_prel.
Add Relation massert massert_eqv
reflexivity proved by massert_eqv_refl
symmetry proved by massert_eqv_sym
transitivity proved by massert_eqv_trans
as massert_eqv_prel.
Add Morphism m_pred
with signature massert_imp ==>
eq ==>
impl
as m_pred_morph_1.
Proof.
intros P Q [A B]. auto.
Qed.
Add Morphism m_pred
with signature massert_eqv ==>
eq ==>
iff
as m_pred_morph_2.
Proof.
intros P Q [[A B] [C D]]. split; auto.
Qed.
Global Hint Resolve massert_imp_refl massert_eqv_refl :
core.
Separating conjunction
Definition disjoint_footprint (
P Q:
massert) :
Prop :=
forall b ofs,
m_footprint P b ofs ->
m_footprint Q b ofs ->
False.
Program Definition sepconj (
P Q:
massert) :
massert := {|
m_pred :=
fun m =>
m_pred P m /\
m_pred Q m /\
disjoint_footprint P Q;
m_footprint :=
fun b ofs =>
m_footprint P b ofs \/
m_footprint Q b ofs
|}.
Next Obligation.
Next Obligation.
Add Morphism sepconj
with signature massert_imp ==>
massert_imp ==>
massert_imp
as sepconj_morph_1.
Proof.
intros P1 P2 [A B] Q1 Q2 [C D].
red; simpl; split; intros.
- intuition auto. red; intros. apply (H2 b ofs); auto.
- intuition auto.
Qed.
Add Morphism sepconj
with signature massert_eqv ==>
massert_eqv ==>
massert_eqv
as sepconj_morph_2.
Proof.
Infix "**" :=
sepconj (
at level 60,
right associativity) :
sep_scope.
Local Open Scope sep_scope.
Lemma sep_imp:
forall P P'
Q Q'
m,
m |=
P **
Q ->
massert_imp P P' ->
massert_imp Q Q' ->
m |=
P' **
Q'.
Proof.
intros. rewrite <- H0, <- H1; auto.
Qed.
Lemma sep_comm_1:
forall P Q,
massert_imp (
P **
Q) (
Q **
P).
Proof.
unfold massert_imp;
simpl;
split;
intros.
-
intuition auto.
red;
intros;
eapply H2;
eauto.
-
intuition auto.
Qed.
Lemma sep_comm:
forall P Q,
massert_eqv (
P **
Q) (
Q **
P).
Proof.
Lemma sep_assoc_1:
forall P Q R,
massert_imp ((
P **
Q) **
R) (
P ** (
Q **
R)).
Proof.
Lemma sep_assoc_2:
forall P Q R,
massert_imp (
P ** (
Q **
R)) ((
P **
Q) **
R).
Proof.
Lemma sep_assoc:
forall P Q R,
massert_eqv ((
P **
Q) **
R) (
P ** (
Q **
R)).
Proof.
Lemma sep_swap:
forall P Q R,
massert_eqv (
P **
Q **
R) (
Q **
P **
R).
Proof.
Definition sep_swap12 :=
sep_swap.
Lemma sep_swap23:
forall P Q R S,
massert_eqv (
P **
Q **
R **
S) (
P **
R **
Q **
S).
Proof.
intros.
rewrite (
sep_swap Q).
reflexivity.
Qed.
Lemma sep_swap34:
forall P Q R S T,
massert_eqv (
P **
Q **
R **
S **
T) (
P **
Q **
S **
R **
T).
Proof.
intros.
rewrite (
sep_swap R).
reflexivity.
Qed.
Lemma sep_swap45:
forall P Q R S T U,
massert_eqv (
P **
Q **
R **
S **
T **
U) (
P **
Q **
R **
T **
S **
U).
Proof.
intros.
rewrite (
sep_swap S).
reflexivity.
Qed.
Definition sep_swap2 :=
sep_swap.
Lemma sep_swap3:
forall P Q R S,
massert_eqv (
P **
Q **
R **
S) (
R **
Q **
P **
S).
Proof.
Lemma sep_swap4:
forall P Q R S T,
massert_eqv (
P **
Q **
R **
S **
T) (
S **
Q **
R **
P **
T).
Proof.
Lemma sep_swap5:
forall P Q R S T U,
massert_eqv (
P **
Q **
R **
S **
T **
U) (
T **
Q **
R **
S **
P **
U).
Proof.
Lemma sep_drop:
forall P Q m,
m |=
P **
Q ->
m |=
Q.
Proof.
simpl; intros. tauto.
Qed.
Lemma sep_drop2:
forall P Q R m,
m |=
P **
Q **
R ->
m |=
P **
R.
Proof.
Lemma sep_proj1:
forall Q P m,
m |=
P **
Q ->
m |=
P.
Proof.
intros. destruct H; auto.
Qed.
Lemma sep_proj2:
forall P Q m,
m |=
P **
Q ->
m |=
Q.
Proof sep_drop.
Definition sep_pick1 :=
sep_proj1.
Lemma sep_pick2:
forall P Q R m,
m |=
P **
Q **
R ->
m |=
Q.
Proof.
Lemma sep_pick3:
forall P Q R S m,
m |=
P **
Q **
R **
S ->
m |=
R.
Proof.
Lemma sep_pick4:
forall P Q R S T m,
m |=
P **
Q **
R **
S **
T ->
m |=
S.
Proof.
Lemma sep_pick5:
forall P Q R S T U m,
m |=
P **
Q **
R **
S **
T **
U ->
m |=
T.
Proof.
Lemma sep_preserved:
forall m m'
P Q,
m |=
P **
Q ->
(
m |=
P ->
m' |=
P) ->
(
m |=
Q ->
m' |=
Q) ->
m' |=
P **
Q.
Proof.
simpl; intros. intuition auto.
Qed.
Basic memory assertions.
Pure logical assertion
Program Definition pure (
P:
Prop) :
massert := {|
m_pred :=
fun m =>
P;
m_footprint :=
fun b ofs =>
False
|}.
Next Obligation.
tauto.
Qed.
Lemma sep_pure:
forall P Q m,
m |=
pure P **
Q <->
P /\
m |=
Q.
Proof.
simpl; intros. intuition auto. red; simpl; tauto.
Qed.
A range of bytes, with full permissions and unspecified contents.
Program Definition range (
b:
block) (
lo hi:
Z) :
massert := {|
m_pred :=
fun m =>
0 <=
lo /\
hi <=
Ptrofs.modulus
/\ (
forall i k p,
lo <=
i <
hi ->
Mem.perm m b i k p);
m_footprint :=
fun b'
ofs' =>
b' =
b /\
lo <=
ofs' <
hi
|}.
Next Obligation.
Next Obligation.
Lemma alloc_rule:
forall m lo hi b m'
P,
Mem.alloc m lo hi = (
m',
b) ->
0 <=
lo ->
hi <=
Ptrofs.modulus ->
m |=
P ->
m' |=
range b lo hi **
P.
Proof.
Lemma range_split:
forall b lo hi P mid m,
lo <=
mid <=
hi ->
m |=
range b lo hi **
P ->
m |=
range b lo mid **
range b mid hi **
P.
Proof.
intros.
rewrite <-
sep_assoc.
eapply sep_imp;
eauto.
split;
simpl;
intros.
-
intuition auto.
+
lia.
+
apply H5;
lia.
+
lia.
+
apply H5;
lia.
+
red;
simpl;
intros;
lia.
-
intuition lia.
Qed.
Lemma range_drop_left:
forall b lo hi P mid m,
lo <=
mid <=
hi ->
m |=
range b lo hi **
P ->
m |=
range b mid hi **
P.
Proof.
Lemma range_drop_right:
forall b lo hi P mid m,
lo <=
mid <=
hi ->
m |=
range b lo hi **
P ->
m |=
range b lo mid **
P.
Proof.
Lemma range_split_2:
forall b lo hi P mid al m,
lo <=
align mid al <=
hi ->
al > 0 ->
m |=
range b lo hi **
P ->
m |=
range b lo mid **
range b (
align mid al)
hi **
P.
Proof.
intros.
rewrite <-
sep_assoc.
eapply sep_imp;
eauto.
assert (
mid <=
align mid al)
by (
apply align_le;
auto).
split;
simpl;
intros.
-
intuition auto.
+
lia.
+
apply H7;
lia.
+
lia.
+
apply H7;
lia.
+
red;
simpl;
intros;
lia.
-
intuition lia.
Qed.
Lemma range_preserved:
forall m m'
b lo hi,
m |=
range b lo hi ->
(
forall i k p,
lo <=
i <
hi ->
Mem.perm m b i k p ->
Mem.perm m'
b i k p) ->
m' |=
range b lo hi.
Proof.
intros. destruct H as (A & B & C). simpl; intuition auto.
Qed.
A memory area that contains a value sastifying a given predicate
Program Definition contains (
chunk:
memory_chunk) (
b:
block) (
ofs:
Z) (
spec:
val ->
Prop) :
massert := {|
m_pred :=
fun m =>
0 <=
ofs <=
Ptrofs.max_unsigned
/\
Mem.valid_access m chunk b ofs Freeable
/\
exists v,
Mem.load chunk m b ofs =
Some v /\
spec v;
m_footprint :=
fun b'
ofs' =>
b' =
b /\
ofs <=
ofs' <
ofs +
size_chunk chunk
|}.
Next Obligation.
rename H2 into v.
split;[|
split].
-
auto.
-
destruct H1;
split;
auto.
red;
intros;
eapply Mem.perm_unchanged_on;
eauto.
simpl;
auto.
-
exists v.
split;
auto.
eapply Mem.load_unchanged_on;
eauto.
simpl;
auto.
Qed.
Next Obligation.
eauto with mem.
Qed.
Lemma contains_no_overflow:
forall spec m chunk b ofs,
m |=
contains chunk b ofs spec ->
0 <=
ofs <=
Ptrofs.max_unsigned.
Proof.
intros. simpl in H. tauto.
Qed.
Lemma load_rule:
forall spec m chunk b ofs,
m |=
contains chunk b ofs spec ->
exists v,
Mem.load chunk m b ofs =
Some v /\
spec v.
Proof.
intros. destruct H as (D & E & v & F & G).
exists v; auto.
Qed.
Lemma loadv_rule:
forall spec m chunk b ofs,
m |=
contains chunk b ofs spec ->
exists v,
Mem.loadv chunk m (
Vptr b (
Ptrofs.repr ofs)) =
Some v /\
spec v.
Proof.
Lemma store_rule:
forall chunk m b ofs v (
spec1 spec:
val ->
Prop)
P,
m |=
contains chunk b ofs spec1 **
P ->
spec (
Val.load_result chunk v) ->
exists m',
Mem.store chunk m b ofs v =
Some m' /\
m' |=
contains chunk b ofs spec **
P.
Proof.
Lemma storev_rule:
forall chunk m b ofs v (
spec1 spec:
val ->
Prop)
P,
m |=
contains chunk b ofs spec1 **
P ->
spec (
Val.load_result chunk v) ->
exists m',
Mem.storev chunk m (
Vptr b (
Ptrofs.repr ofs))
v =
Some m' /\
m' |=
contains chunk b ofs spec **
P.
Proof.
Lemma range_contains:
forall chunk b ofs P m,
m |=
range b ofs (
ofs +
size_chunk chunk) **
P ->
(
align_chunk chunk |
ofs) ->
m |=
contains chunk b ofs (
fun v =>
True) **
P.
Proof.
Lemma contains_imp:
forall (
spec1 spec2:
val ->
Prop)
chunk b ofs,
(
forall v,
spec1 v ->
spec2 v) ->
massert_imp (
contains chunk b ofs spec1) (
contains chunk b ofs spec2).
Proof.
intros; split; simpl; intros.
- intuition auto. destruct H4 as (v & A & B). exists v; auto.
- auto.
Qed.
A memory area that contains a given value
Definition hasvalue (
chunk:
memory_chunk) (
b:
block) (
ofs:
Z) (
v:
val) :
massert :=
contains chunk b ofs (
fun v' =>
v' =
v).
Lemma store_rule':
forall chunk m b ofs v (
spec1:
val ->
Prop)
P,
m |=
contains chunk b ofs spec1 **
P ->
exists m',
Mem.store chunk m b ofs v =
Some m' /\
m' |=
hasvalue chunk b ofs (
Val.load_result chunk v) **
P.
Proof.
Lemma storev_rule':
forall chunk m b ofs v (
spec1:
val ->
Prop)
P,
m |=
contains chunk b ofs spec1 **
P ->
exists m',
Mem.storev chunk m (
Vptr b (
Ptrofs.repr ofs))
v =
Some m' /\
m' |=
hasvalue chunk b ofs (
Val.load_result chunk v) **
P.
Proof.
Non-separating conjunction
Program Definition mconj (
P Q:
massert) :
massert := {|
m_pred :=
fun m =>
m_pred P m /\
m_pred Q m;
m_footprint :=
fun b ofs =>
m_footprint P b ofs \/
m_footprint Q b ofs
|}.
Next Obligation.
Next Obligation.
Lemma mconj_intro:
forall P Q R m,
m |=
P **
R ->
m |=
Q **
R ->
m |=
mconj P Q **
R.
Proof.
intros. destruct H as (A & B & C). destruct H0 as (D & E & F).
split; [|split].
- simpl; auto.
- auto.
- red; simpl; intros. destruct H; [eelim C | eelim F]; eauto.
Qed.
Lemma mconj_proj1:
forall P Q R m,
m |=
mconj P Q **
R ->
m |=
P **
R.
Proof.
intros. destruct H as (A & B & C); simpl in A.
simpl. intuition auto.
red; intros; eapply C; eauto; simpl; auto.
Qed.
Lemma mconj_proj2:
forall P Q R m,
m |=
mconj P Q **
R ->
m |=
Q **
R.
Proof.
intros. destruct H as (A & B & C); simpl in A.
simpl. intuition auto.
red; intros; eapply C; eauto; simpl; auto.
Qed.
Lemma frame_mconj:
forall P P'
Q R m m',
m |=
mconj P Q **
R ->
m' |=
P' **
R ->
m' |=
Q ->
m' |=
mconj P'
Q **
R.
Proof.
intros. destruct H as (A & B & C); simpl in A.
destruct H0 as (D & E & F).
simpl. intuition auto.
red; simpl; intros. destruct H2. eapply F; eauto. eapply C; simpl; eauto.
Qed.
Add Morphism mconj
with signature massert_imp ==>
massert_imp ==>
massert_imp
as mconj_morph_1.
Proof.
intros P1 P2 [A B] Q1 Q2 [C D].
red; simpl; intuition auto.
Qed.
Add Morphism mconj
with signature massert_eqv ==>
massert_eqv ==>
massert_eqv
as mconj_morph_2.
Proof.
The image of a memory injection
Program Definition minjection (
j:
meminj) (
m0:
mem) :
massert := {|
m_pred :=
fun m =>
Mem.inject j m0 m;
m_footprint :=
fun b ofs =>
exists b0 delta,
j b0 =
Some(
b,
delta) /\
Mem.perm m0 b0 (
ofs -
delta)
Max Nonempty
|}.
Next Obligation.
Next Obligation.
Lemma loadv_parallel_rule:
forall j m1 m2 chunk addr1 v1 addr2,
m2 |=
minjection j m1 ->
Mem.loadv chunk m1 addr1 =
Some v1 ->
Val.inject j addr1 addr2 ->
exists v2,
Mem.loadv chunk m2 addr2 =
Some v2 /\
Val.inject j v1 v2.
Proof.
Lemma storev_parallel_rule:
forall j m1 m2 P chunk addr1 v1 m1'
addr2 v2,
m2 |=
minjection j m1 **
P ->
Mem.storev chunk m1 addr1 v1 =
Some m1' ->
Val.inject j addr1 addr2 ->
Val.inject j v1 v2 ->
exists m2',
Mem.storev chunk m2 addr2 v2 =
Some m2' /\
m2' |=
minjection j m1' **
P.
Proof.
Lemma alloc_parallel_rule:
forall m1 sz1 m1'
b1 m2 sz2 m2'
b2 P j lo hi delta,
m2 |=
minjection j m1 **
P ->
Mem.alloc m1 0
sz1 = (
m1',
b1) ->
Mem.alloc m2 0
sz2 = (
m2',
b2) ->
(8 |
delta) ->
lo =
delta ->
hi =
delta +
Z.max 0
sz1 ->
0 <=
sz2 <=
Ptrofs.max_unsigned ->
0 <=
delta ->
hi <=
sz2 ->
exists j',
m2' |=
range b2 0
lo **
range b2 hi sz2 **
minjection j'
m1' **
P
/\
inject_incr j j'
/\
j'
b1 =
Some(
b2,
delta)
/\ (
forall b,
b <>
b1 ->
j'
b =
j b).
Proof.
Lemma free_parallel_rule:
forall j m1 b1 sz1 m1'
m2 b2 sz2 lo hi delta P,
m2 |=
range b2 0
lo **
range b2 hi sz2 **
minjection j m1 **
P ->
Mem.free m1 b1 0
sz1 =
Some m1' ->
j b1 =
Some (
b2,
delta) ->
lo =
delta ->
hi =
delta +
Z.max 0
sz1 ->
exists m2',
Mem.free m2 b2 0
sz2 =
Some m2'
/\
m2' |=
minjection j m1' **
P.
Proof.
Preservation of a global environment by a memory injection
Inductive globalenv_preserved {
F V:
Type} (
ge:
Genv.t F V) (
j:
meminj) (
bound:
block) :
Prop :=
|
globalenv_preserved_intro
(
DOMAIN:
forall b,
Plt b bound ->
j b =
Some(
b, 0))
(
IMAGE:
forall b1 b2 delta,
j b1 =
Some(
b2,
delta) ->
Plt b2 bound ->
b1 =
b2)
(
SYMBOLS:
forall id b,
Genv.find_symbol ge id =
Some b ->
Plt b bound)
(
FUNCTIONS:
forall b fd,
Genv.find_funct_ptr ge b =
Some fd ->
Plt b bound)
(
VARINFOS:
forall b gv,
Genv.find_var_info ge b =
Some gv ->
Plt b bound).
Program Definition globalenv_inject {
F V:
Type} (
ge:
Genv.t F V) (
j:
meminj) :
massert := {|
m_pred :=
fun m =>
exists bound,
Ple bound (
Mem.nextblock m) /\
globalenv_preserved ge j bound;
m_footprint :=
fun b ofs =>
False
|}.
Next Obligation.
Next Obligation.
tauto.
Qed.
Lemma globalenv_inject_preserves_globals:
forall (
F V:
Type) (
ge:
Genv.t F V)
j m,
m |=
globalenv_inject ge j ->
meminj_preserves_globals ge j.
Proof.
intros. destruct H as (bound & A & B). destruct B.
split; [|split]; intros.
- eauto.
- eauto.
- symmetry; eauto.
Qed.
Lemma globalenv_inject_incr:
forall j m0 (
F V:
Type) (
ge:
Genv.t F V)
m j'
P,
inject_incr j j' ->
inject_separated j j'
m0 m ->
m |=
globalenv_inject ge j **
P ->
m |=
globalenv_inject ge j' **
P.
Proof.
intros.
destruct H1 as (
A &
B &
C).
destruct A as (
bound &
D &
E).
split; [|
split];
auto.
exists bound;
split;
auto.
inv E;
constructor;
intros.
-
eauto.
-
destruct (
j b1)
as [[
b0 delta0]|]
eqn:
JB1.
+
erewrite H in H1 by eauto.
inv H1.
eauto.
+
exploit H0;
eauto.
intros (
X &
Y).
elim Y.
apply Pos.lt_le_trans with bound;
auto.
-
eauto.
-
eauto.
-
eauto.
Qed.
Lemma external_call_parallel_rule:
forall (
F V:
Type)
ef (
ge:
Genv.t F V)
vargs1 m1 t vres1 m1'
m2 j P vargs2,
external_call ef ge vargs1 m1 t vres1 m1' ->
m2 |=
minjection j m1 **
globalenv_inject ge j **
P ->
Val.inject_list j vargs1 vargs2 ->
exists j'
vres2 m2',
external_call ef ge vargs2 m2 t vres2 m2'
/\
Val.inject j'
vres1 vres2
/\
m2' |=
minjection j'
m1' **
globalenv_inject ge j' **
P
/\
inject_incr j j'
/\
inject_separated j j'
m1 m2.
Proof.
Lemma alloc_parallel_rule_2:
forall (
F V:
Type) (
ge:
Genv.t F V)
m1 sz1 m1'
b1 m2 sz2 m2'
b2 P j lo hi delta,
m2 |=
minjection j m1 **
globalenv_inject ge j **
P ->
Mem.alloc m1 0
sz1 = (
m1',
b1) ->
Mem.alloc m2 0
sz2 = (
m2',
b2) ->
(8 |
delta) ->
lo =
delta ->
hi =
delta +
Z.max 0
sz1 ->
0 <=
sz2 <=
Ptrofs.max_unsigned ->
0 <=
delta ->
hi <=
sz2 ->
exists j',
m2' |=
range b2 0
lo **
range b2 hi sz2 **
minjection j'
m1' **
globalenv_inject ge j' **
P
/\
inject_incr j j'
/\
j'
b1 =
Some(
b2,
delta).
Proof.