Library memory
To support modular verification, we use a non-deterministic C memory model
defined in this file, including basic operations and useful properties over
the memory model.
Definitions and lemmas for instantiating the memory
Theorem addr_eq_dec : forall a b : addr, {a = b} + {a <> b}.
Fixpoint blt_pos (p q : positive) {struct p} : bool :=
match (Pcompare p q Eq) with
| Lt => true
| _ => false
end.
Fixpoint blt_Z (n m : Z) {struct n} : bool :=
match n, m with
| Z0, Zpos p => true
| Zneg p, Z0 => true
| Zneg p, Zpos q => true
| Zneg p, Zneg q => blt_pos q p
| Zpos p, Zpos q => blt_pos p q
| _, _ => false
end.
Fixpoint beq_pos (p p´ : positive) {struct p} : bool :=
match p, p´ with
| x~0, x´~0 => andb true (beq_pos x x´)
| p~1, p´~1 => andb true (beq_pos p p´)
| 1, 1 => true
| _, _ => false
end %positive.
Fixpoint beq_Z (z z´ : Z) {struct z} : bool :=
match z, z´ with
| Z0, Z0 => true
| Zpos p, Zpos p´ => beq_pos p p´
| Zneg p, Zneg p´ => beq_pos p p´
| _, _ => false
end.
Definition beq_addr (n m : addr) : bool :=
match n, m with
| (b, i), (b´, i´) => andb (beq_pos b b´) (beq_Z i i´)
end.
Definition blt_addr (n m : addr) : bool :=
match n, m with
| (b, i), (b´, i´) => if blt_pos b b´
then true
else if beq_pos b b´
then blt_Z i i´
else false
end.
Lemma beq_pos_Pos_eqb_eq :
forall b1 b2,
beq_pos b1 b2 = Pos.eqb b1 b2.
Lemma beq_Z_Z_eqb_eq :
forall z1 z2,
beq_Z z1 z2 = Z.eqb z1 z2.
Lemma beq_addr_true_eq_iff : forall z z´ : addr,
beq_addr z z´ = true <-> z = z´.
Lemma beq_addr_false_neq_iff :
forall z z´ : addr,
beq_addr z z´ = false <-> z <> z´.
Lemma blt_pos_Pos_ltb_eq :
forall b1 b2,
blt_pos b1 b2 = Pos.ltb b1 b2.
Lemma blt_Z_Z_ltb_eq :
forall z1 z2,
blt_Z z1 z2 = Z.ltb z1 z2.
Module addrspec.
Definition A := addr.
Definition B := addr.
Definition beq : A -> A -> bool := beq_addr.
Definition blt : A -> A -> bool := blt_addr.
Lemma beq_true_eq : forall a a´ : A,
beq a a´ = true -> a = a´.
Lemma beq_false_neq : forall a a´ : A,
beq a a´ = false -> a <> a´.
Lemma eq_beq_true : forall a a´ : A,
a = a´ -> beq a a´ = true.
Lemma neq_beq_false : forall a a´ : A,
a <> a´ -> beq a a´ = false.
Lemma blt_trans : forall a a´ a´´ : A,
blt a a´ = true -> blt a´ a´´ = true -> blt a a´´ = true.
Lemma blt_irrefl : forall a : A,
blt a a = false.
Lemma blt_asym : forall a b : A,
blt a b = true -> blt b a = false.
Lemma blt_beq_dec : forall a b : A,
{blt a b = true} + {beq a b = true} + {blt b a = true}.
End addrspec.
Module valspec.
Definition B := memval.
End valspec.
Fixpoint blt_pos (p q : positive) {struct p} : bool :=
match (Pcompare p q Eq) with
| Lt => true
| _ => false
end.
Fixpoint blt_Z (n m : Z) {struct n} : bool :=
match n, m with
| Z0, Zpos p => true
| Zneg p, Z0 => true
| Zneg p, Zpos q => true
| Zneg p, Zneg q => blt_pos q p
| Zpos p, Zpos q => blt_pos p q
| _, _ => false
end.
Fixpoint beq_pos (p p´ : positive) {struct p} : bool :=
match p, p´ with
| x~0, x´~0 => andb true (beq_pos x x´)
| p~1, p´~1 => andb true (beq_pos p p´)
| 1, 1 => true
| _, _ => false
end %positive.
Fixpoint beq_Z (z z´ : Z) {struct z} : bool :=
match z, z´ with
| Z0, Z0 => true
| Zpos p, Zpos p´ => beq_pos p p´
| Zneg p, Zneg p´ => beq_pos p p´
| _, _ => false
end.
Definition beq_addr (n m : addr) : bool :=
match n, m with
| (b, i), (b´, i´) => andb (beq_pos b b´) (beq_Z i i´)
end.
Definition blt_addr (n m : addr) : bool :=
match n, m with
| (b, i), (b´, i´) => if blt_pos b b´
then true
else if beq_pos b b´
then blt_Z i i´
else false
end.
Lemma beq_pos_Pos_eqb_eq :
forall b1 b2,
beq_pos b1 b2 = Pos.eqb b1 b2.
Lemma beq_Z_Z_eqb_eq :
forall z1 z2,
beq_Z z1 z2 = Z.eqb z1 z2.
Lemma beq_addr_true_eq_iff : forall z z´ : addr,
beq_addr z z´ = true <-> z = z´.
Lemma beq_addr_false_neq_iff :
forall z z´ : addr,
beq_addr z z´ = false <-> z <> z´.
Lemma blt_pos_Pos_ltb_eq :
forall b1 b2,
blt_pos b1 b2 = Pos.ltb b1 b2.
Lemma blt_Z_Z_ltb_eq :
forall z1 z2,
blt_Z z1 z2 = Z.ltb z1 z2.
Module addrspec.
Definition A := addr.
Definition B := addr.
Definition beq : A -> A -> bool := beq_addr.
Definition blt : A -> A -> bool := blt_addr.
Lemma beq_true_eq : forall a a´ : A,
beq a a´ = true -> a = a´.
Lemma beq_false_neq : forall a a´ : A,
beq a a´ = false -> a <> a´.
Lemma eq_beq_true : forall a a´ : A,
a = a´ -> beq a a´ = true.
Lemma neq_beq_false : forall a a´ : A,
a <> a´ -> beq a a´ = false.
Lemma blt_trans : forall a a´ a´´ : A,
blt a a´ = true -> blt a´ a´´ = true -> blt a a´´ = true.
Lemma blt_irrefl : forall a : A,
blt a a = false.
Lemma blt_asym : forall a b : A,
blt a b = true -> blt b a = false.
Lemma blt_beq_dec : forall a b : A,
{blt a b = true} + {beq a b = true} + {blt b a = true}.
End addrspec.
Module valspec.
Definition B := memval.
End valspec.
memory definition
"fresh M b" means the memory block b is a fresh block with respect to M .
"allocb M b i k" recursively allocates k bytes over M from the beginning
address (b, i) to the ending point (b, i+k−1).
Fixpoint allocb (m : mem) (b: block) (i : Z) (n : nat) {struct n} : mem :=
match n with
| O => m
| S n´ => MemMod.set (allocb m b (i+1) n´) (b, i) Undef
end.
"freeb M b i k" recursively frees k bytes from (b, i). It requires that
each freed memory location should be allocated before.
Fixpoint freeb (m : mem) (b: block) (i : Z) (n : nat) {struct n} : option mem :=
match n with
| O => Some m
| S n´ => match MemMod.get m (b, i), freeb m b (i+1) n´ with
| Some v, Some m´ => Some (MemMod.minus m´ (MemMod.sig (b, i) v))
| _, _ => None
end
end.
storebytes M l V updates the memory M with the list of memory values V
from the beginning address l.
Fixpoint storebytes (m : mem) (l : addr) (bl :list memval) {struct bl}: option mem :=
match bl with
| nil => Some m
| u :: bl´ => match l with
(b , i) =>
match MemMod.get m l, storebytes m (b, (i+1)) bl´ with
| Some _, Some m´ => Some (MemMod.set m´ l u)
| _, _ => None
end
end
end.
"loadbytes M l k" reads k bytes from the address l and return the
corresponding value list if the address l is valid.
Fixpoint loadbytes (m : mem) (l : addr) (n : nat) {struct n}: option (list memval) :=
match n with
| O => Some nil
| S n´ => match l with
(b , i) =>
match MemMod.get m l, loadbytes m (b, (i+1)) n´ with
| Some u, Some bl => Some (u :: bl)
| _, _ => None
end
end
end.
Module identspec.
Definition A := ident.
Definition beq := Zeq_bool.
Definition blt := Zlt_bool.
Lemma beq_true_eq : forall a a´ : A,
beq a a´ = true -> a = a´.
Lemma beq_false_neq : forall a a´ : A,
beq a a´ = false -> a <> a´.
Lemma eq_beq_true : forall a a´ : A,
a = a´ -> beq a a´ = true.
Lemma neq_beq_false : forall a a´ : A,
a <> a´ -> beq a a´ = false.
Lemma blt_trans :
forall a a´ a´´ : A,
blt a a´ = true -> blt a´ a´´ = true -> blt a a´´ = true.
Lemma blt_irrefl :
forall a : A,
blt a a = false.
Lemma blt_asym :
forall a b : A,
blt a b = true -> blt b a = false.
Lemma blt_beq_dec :
forall a b : A,
{blt a b = true} + {beq a b = true} + {blt b a = true}.
End identspec.
Fixpoint ftype (id : ident) (dls : decllist) : option type :=
match dls with
| dnil => None
| dcons id´ t dls´ => if Zeq_bool id id´ then Some t else ftype id dls´
end.
Module addrtypespec.
Definition B:=prod addr type.
End addrtypespec.
Module blocktypespec.
Definition B:=prod block type.
End blocktypespec.
Module EnvMod := MapLib.MapFun identspec blocktypespec.
Definition env := EnvMod.map.
Definition var := Z.
memory allocation
Definition alloc (x : var) (t : type) (e : env) (m : mem) (e´ : env) (m´:mem) : Prop :=
exists b, fresh m b /\ m´ = allocb m b 0 (typelen t) /\~ EnvMod.indom e x /\
e´ = EnvMod.set e x (b, t).
memory deallocation
memory write
Definition store (t : type) (m : mem) (l : addr) (v : val) : option mem :=
match l with
(b, i) => storebytes m l (encode_val t v)
end.
memory read
Definition loadm (t : type) (m : mem) (l : addr) : option val :=
match l with
(b, i) => match loadbytes m l (typelen t) with
| Some bls => Some (decode_val t bls)
| _ => None
end
end.
"FullMemory M" specifies the memory that contains all the memory blocks. It
means that we could not allocate a fresh memory block over the full memory.
The framework assumes that the memory is infinite by the axiom “∀M.¬FullMemory M”,
which means that it is impossible to reach the full memory. This guarantees that
the memory allocation operation never fail. This is the only axiom introduced in
the framework.
Definition FullMemory m := forall b, exists i, MemMod.indom m (b,i).
Axiom MemoryNotFull : forall m,~FullMemory m.
Some useful properties of the memory model.
Lemma allocb_get_some :
forall m b n i off,
(off<n)%nat->
exists v,
MemMod.get (allocb m b i n) (b, (i + Z_of_nat off)) = Some v.
Lemma allocb_get_none :
forall m b i off n,
(off>0)->
fresh m b ->
MemMod.get (allocb m b (BinInt.Z.add i off) n) (b, i) = None.
Lemma freeb_get_same :
forall m m´ b i off n,
(off>0)%Z->
freeb m b (BinInt.Z.add i off) n = Some m´ ->
MemMod.get m´ (b, i) = MemMod.get m (b, i).
Lemma storebytes_get_same :
forall m m´ b i off vl,
(off>0)->
storebytes m (b, (BinInt.Z.add i off)) vl = Some m´ ->
MemMod.get m´ (b, i) = MemMod.get m (b, i).
Lemma allocb_storebytes_mem_ex :
forall vl n m b i,
((length vl) + i = n)%nat ->
(exists m´, storebytes (allocb m b 0 n) (b, Z_of_nat i) vl = Some m´).
Lemma allocb_store_mem_ex :
forall t m b v,
(exists m´, store t (allocb m b 0 (typelen t)) (b, BinNums.Z0) v = Some m´).
Lemma join_allocb :
forall m1 M m2 m1´ m2´ b i n, MemMod.join m1 M m2 ->
m1´ = allocb m1 b i n ->
m2´ = allocb m2 b i n ->
fresh m2 b ->
MemMod.join m1´ M m2´.
Lemma join_freeb :
forall m1 M m2 m1´ m2´ b i n, MemMod.join m1 M m2 ->
freeb m1 b i n = Some m1´ ->
freeb m2 b i n = Some m2´ ->
MemMod.join m1´ M m2´.
Lemma join_free :
forall m1 M m2 m1´ m2´ t b, MemMod.join m1 M m2 ->
free t b m1 = Some m1´ ->
free t b m2 = Some m2´ ->
MemMod.join m1´ M m2´.
Lemma join_storebytes :
forall m1 M m2 m1´ m2´ b o vl, MemMod.join m1 M m2 ->
storebytes m1 (b, o) vl = Some m1´ ->
storebytes m2 (b, o) vl = Some m2´ ->
MemMod.join m1´ M m2´.
Lemma join_store :
forall m1 M m2 m1´ m2´ t a v, MemMod.join m1 M m2 ->
store t m1 a v = Some m1´ ->
store t m2 a v = Some m2´ ->
MemMod.join m1´ M m2´.
Lemma join_allocb_emp :
forall M b i n,
fresh M b ->
MemMod.join M (allocb MemMod.emp b i n) (allocb M b i n).
Lemma join_allocb´ :
forall M1 M2 M b i n,
MemMod.join M2 M (allocb M2 b i n) ->
fresh M2 b ->
fresh M1 b ->
MemMod.join M1 M (allocb M1 b i n).
Lemma join_store_allocb :
forall M1 M2 M M´´ M1´ M2´ b t v,
MemMod.join M1 M M2 ->
MemMod.join M2 M´´ M2´ ->
fresh M2 b ->
store t (allocb M1 b 0 (typelen t)) (b, 0%Z) v = Some M1´ ->
store t (allocb M2 b 0 (typelen t)) (b, 0%Z) v = Some M2´ ->
MemMod.join M1 M´´ M1´.
Lemma fresh_mono :
forall m1 M m2 b, MemMod.join m1 M m2 ->
fresh m2 b -> fresh m1 b.
Lemma fresh_exist : forall m, (exists b,fresh m b).
Require Import Coq.Logic.Classical_Pred_Type.
Lemma alloc_false : forall x t le M M´, ~alloc x t le M le M´.
Lemma free_false : forall t b M,(typelen t <> 0)%nat -> ~free t b M = Some M.
Lemma storebytes_mono´ :
forall M1 M1´ M M2 M2´ a l,
storebytes M1 a l = Some M1´ ->
MemMod.join M1 M M2 ->
MemMod.join M1´ M M2´ ->
storebytes M2 a l = Some M2´.
Lemma store_mono´ :
forall t M1 M1´ M M2 M2´ a v,
store t M1 a v = Some M1´ ->
MemMod.join M1 M M2 ->
MemMod.join M1´ M M2´ ->
store t M2 a v = Some M2´.
Lemma store_same_mono :
forall t M M1 M2 a v,
MemMod.join M M1 M2 ->
store t M a v = Some M ->
store t M2 a v = Some M2.