Global environments are a component of the dynamic semantics of
all languages involved in the compiler. A global environment
maps symbol names (names of functions and of global variables)
to the corresponding memory addresses. It also maps memory addresses
of functions to the corresponding function descriptions.
Global environments, along with the initial memory state at the beginning
of program execution, are built from the program of interest, as follows:
-
A distinct memory address is assigned to each function of the program.
These function addresses use negative numbers to distinguish them from
addresses of memory blocks. The associations of function name to function
address and function address to function description are recorded in
the global environment.
-
For each global variable, a memory block is allocated and associated to
the name of the variable.
These operations reflect (at a high level of abstraction) what takes
place during program linking and program loading in a real operating
system.
.
Require Import Zwf.
Require Import Axioms Coqlib Errors Maps AST Linking.
Require Import Integers Floats Values Memory.
Declare Scope pair_scope.
Notation "
s #1" := (
fst s) (
at level 9,
format "
s '#1'") :
pair_scope.
Notation "
s #2" := (
snd s) (
at level 9,
format "
s '#2'") :
pair_scope.
Local Open Scope pair_scope.
Local Open Scope error_monad_scope.
Set Implicit Arguments.
Auxiliary function for initialization of global variables.
Function store_zeros (
m:
mem) (
b:
block) (
p:
Z) (
n:
Z) {
wf (
Zwf 0)
n}:
option mem :=
if zle n 0
then Some m else
match Mem.store Mint8unsigned m b p Vzero with
|
Some m' =>
store_zeros m'
b (
p + 1) (
n - 1)
|
None =>
None
end.
Proof.
Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.
Symbol environments
Symbol environments are a restricted view of global environments,
focusing on symbol names and their associated blocks. They do not
contain mappings from blocks to function or variable definitions.
Module Senv.
Record t:
Type :=
mksenv {
Operations
find_symbol:
ident ->
option block;
public_symbol:
ident ->
bool;
invert_symbol:
block ->
option ident;
block_is_volatile:
block ->
bool;
nextblock:
block;
Properties
find_symbol_injective:
forall id1 id2 b,
find_symbol id1 =
Some b ->
find_symbol id2 =
Some b ->
id1 =
id2;
invert_find_symbol:
forall id b,
invert_symbol b =
Some id ->
find_symbol id =
Some b;
find_invert_symbol:
forall id b,
find_symbol id =
Some b ->
invert_symbol b =
Some id;
public_symbol_exists:
forall id,
public_symbol id =
true ->
exists b,
find_symbol id =
Some b;
find_symbol_below:
forall id b,
find_symbol id =
Some b ->
Plt b nextblock;
block_is_volatile_below:
forall b,
block_is_volatile b =
true ->
Plt b nextblock
}.
Definition symbol_address (
ge:
t) (
id:
ident) (
ofs:
ptrofs) :
val :=
match find_symbol ge id with
|
Some b =>
Vptr b ofs
|
None =>
Vundef
end.
Theorem shift_symbol_address:
forall ge id ofs delta,
symbol_address ge id (
Ptrofs.add ofs delta) =
Val.offset_ptr (
symbol_address ge id ofs)
delta.
Proof.
Theorem shift_symbol_address_32:
forall ge id ofs n,
Archi.ptr64 =
false ->
symbol_address ge id (
Ptrofs.add ofs (
Ptrofs.of_int n)) =
Val.add (
symbol_address ge id ofs) (
Vint n).
Proof.
Theorem shift_symbol_address_64:
forall ge id ofs n,
Archi.ptr64 =
true ->
symbol_address ge id (
Ptrofs.add ofs (
Ptrofs.of_int64 n)) =
Val.addl (
symbol_address ge id ofs) (
Vlong n).
Proof.
Definition equiv (
se1 se2:
t) :
Prop :=
(
forall id,
find_symbol se2 id =
find_symbol se1 id)
/\ (
forall id,
public_symbol se2 id =
public_symbol se1 id)
/\ (
forall b,
block_is_volatile se2 b =
block_is_volatile se1 b).
End Senv.
Module Genv.
Global environments
Section GENV.
Variable F:
Type.
(* The type of function descriptions *)
Variable V:
Type.
(* The type of information attached to variables *)
The type of global environments.
Record t:
Type :=
mkgenv {
genv_public:
list ident;
(* which symbol names are public *)
genv_symb:
PTree.t block;
(* mapping symbol -> block *)
genv_defs:
PTree.t (
globdef F V);
(* mapping block -> definition *)
genv_next:
block;
(* next symbol pointer *)
genv_symb_range:
forall id b,
PTree.get id genv_symb =
Some b ->
Plt b genv_next;
genv_defs_range:
forall b g,
PTree.get b genv_defs =
Some g ->
Plt b genv_next;
genv_vars_inj:
forall id1 id2 b,
PTree.get id1 genv_symb =
Some b ->
PTree.get id2 genv_symb =
Some b ->
id1 =
id2
}.
Lookup functions
find_symbol ge id returns the block associated with the given name, if any
Definition find_symbol (
ge:
t) (
id:
ident) :
option block :=
PTree.get id ge.(
genv_symb).
symbol_address ge id ofs returns a pointer into the block associated
with id, at byte offset ofs. Vundef is returned if no block is associated
to id.
Definition symbol_address (
ge:
t) (
id:
ident) (
ofs:
ptrofs) :
val :=
match find_symbol ge id with
|
Some b =>
Vptr b ofs
|
None =>
Vundef
end.
public_symbol ge id says whether the name id is public and defined.
Definition public_symbol (
ge:
t) (
id:
ident) :
bool :=
match find_symbol ge id with
|
None =>
false
|
Some _ =>
In_dec ident_eq id ge.(
genv_public)
end.
find_def ge b returns the global definition associated with the given address.
Definition find_def (
ge:
t) (
b:
block) :
option (
globdef F V) :=
PTree.get b ge.(
genv_defs).
find_funct_ptr ge b returns the function description associated with
the given address.
Definition find_funct_ptr (
ge:
t) (
b:
block) :
option F :=
match find_def ge b with Some (
Gfun f) =>
Some f |
_ =>
None end.
find_funct is similar to find_funct_ptr, but the function address
is given as a value, which must be a pointer with offset 0.
Definition find_funct (
ge:
t) (
v:
val) :
option F :=
match v with
|
Vptr b ofs =>
if Ptrofs.eq_dec ofs Ptrofs.zero then find_funct_ptr ge b else None
|
_ =>
None
end.
invert_symbol ge b returns the name associated with the given block, if any
Definition invert_symbol (
ge:
t) (
b:
block) :
option ident :=
PTree.fold
(
fun res id b' =>
if eq_block b b'
then Some id else res)
ge.(
genv_symb)
None.
find_var_info ge b returns the information attached to the variable
at address b.
Definition find_var_info (
ge:
t) (
b:
block) :
option (
globvar V) :=
match find_def ge b with Some (
Gvar v) =>
Some v |
_ =>
None end.
block_is_volatile ge b returns true if b points to a global variable
of volatile type, false otherwise.
Definition block_is_volatile (
ge:
t) (
b:
block) :
bool :=
match find_var_info ge b with
|
None =>
false
|
Some gv =>
gv.(
gvar_volatile)
end.
Constructing the global environment
Program Definition add_global (
ge:
t) (
idg:
ident *
globdef F V) :
t :=
@
mkgenv
ge.(
genv_public)
(
PTree.set idg#1
ge.(
genv_next)
ge.(
genv_symb))
(
PTree.set ge.(
genv_next)
idg#2
ge.(
genv_defs))
(
Pos.succ ge.(
genv_next))
_ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
destruct ge;
simpl in *.
rewrite PTree.gsspec in H.
rewrite PTree.gsspec in H0.
destruct (
peq id1 i);
destruct (
peq id2 i).
congruence.
inv H.
eelim Plt_strict.
eapply genv_symb_range0;
eauto.
inv H0.
eelim Plt_strict.
eapply genv_symb_range0;
eauto.
eauto.
Qed.
Definition add_globals (
ge:
t) (
gl:
list (
ident *
globdef F V)) :
t :=
List.fold_left add_global gl ge.
Lemma add_globals_app:
forall gl2 gl1 ge,
add_globals ge (
gl1 ++
gl2) =
add_globals (
add_globals ge gl1)
gl2.
Proof.
Program Definition empty_genv (
pub:
list ident):
t :=
@
mkgenv pub (
PTree.empty _) (
PTree.empty _) 1%
positive _ _ _.
Definition globalenv (
p:
program F V) :=
add_globals (
empty_genv p.(
prog_public))
p.(
prog_defs).
Proof principles
Section GLOBALENV_PRINCIPLES.
Variable P:
t ->
Prop.
Lemma add_globals_preserves:
forall gl ge,
(
forall ge id g,
P ge ->
In (
id,
g)
gl ->
P (
add_global ge (
id,
g))) ->
P ge ->
P (
add_globals ge gl).
Proof.
induction gl; simpl; intros.
auto.
destruct a. apply IHgl; auto.
Qed.
Lemma add_globals_ensures:
forall id g gl ge,
(
forall ge id g,
P ge ->
In (
id,
g)
gl ->
P (
add_global ge (
id,
g))) ->
(
forall ge,
P (
add_global ge (
id,
g))) ->
In (
id,
g)
gl ->
P (
add_globals ge gl).
Proof.
induction gl;
simpl;
intros.
contradiction.
destruct H1.
subst a.
apply add_globals_preserves;
auto.
apply IHgl;
auto.
Qed.
Lemma add_globals_unique_preserves:
forall id gl ge,
(
forall ge id1 g,
P ge ->
In (
id1,
g)
gl ->
id1 <>
id ->
P (
add_global ge (
id1,
g))) ->
~
In id (
map fst gl) ->
P ge ->
P (
add_globals ge gl).
Proof.
induction gl; simpl; intros.
auto.
destruct a. apply IHgl; auto.
Qed.
Lemma add_globals_unique_ensures:
forall gl1 id g gl2 ge,
(
forall ge id1 g1,
P ge ->
In (
id1,
g1)
gl2 ->
id1 <>
id ->
P (
add_global ge (
id1,
g1))) ->
(
forall ge,
P (
add_global ge (
id,
g))) ->
~
In id (
map fst gl2) ->
P (
add_globals ge (
gl1 ++ (
id,
g) ::
gl2)).
Proof.
Remark in_norepet_unique:
forall id g (
gl:
list (
ident *
globdef F V)),
In (
id,
g)
gl ->
list_norepet (
map fst gl) ->
exists gl1 gl2,
gl =
gl1 ++ (
id,
g) ::
gl2 /\ ~
In id (
map fst gl2).
Proof.
induction gl as [|[
id1 g1]
gl];
simpl;
intros.
contradiction.
inv H0.
destruct H.
inv H.
exists nil,
gl.
auto.
exploit IHgl;
eauto.
intros (
gl1 &
gl2 &
X &
Y).
exists ((
id1,
g1) ::
gl1),
gl2;
split;
auto.
rewrite X;
auto.
Qed.
Lemma add_globals_norepet_ensures:
forall id g gl ge,
(
forall ge id1 g1,
P ge ->
In (
id1,
g1)
gl ->
id1 <>
id ->
P (
add_global ge (
id1,
g1))) ->
(
forall ge,
P (
add_global ge (
id,
g))) ->
In (
id,
g)
gl ->
list_norepet (
map fst gl) ->
P (
add_globals ge gl).
Proof.
End GLOBALENV_PRINCIPLES.
Properties of the operations over global environments
Theorem public_symbol_exists:
forall ge id,
public_symbol ge id =
true ->
exists b,
find_symbol ge id =
Some b.
Proof.
Theorem shift_symbol_address:
forall ge id ofs delta,
symbol_address ge id (
Ptrofs.add ofs delta) =
Val.offset_ptr (
symbol_address ge id ofs)
delta.
Proof.
Theorem shift_symbol_address_32:
forall ge id ofs n,
Archi.ptr64 =
false ->
symbol_address ge id (
Ptrofs.add ofs (
Ptrofs.of_int n)) =
Val.add (
symbol_address ge id ofs) (
Vint n).
Proof.
Theorem shift_symbol_address_64:
forall ge id ofs n,
Archi.ptr64 =
true ->
symbol_address ge id (
Ptrofs.add ofs (
Ptrofs.of_int64 n)) =
Val.addl (
symbol_address ge id ofs) (
Vlong n).
Proof.
Theorem find_funct_inv:
forall ge v f,
find_funct ge v =
Some f ->
exists b,
v =
Vptr b Ptrofs.zero.
Proof.
Theorem find_funct_find_funct_ptr:
forall ge b,
find_funct ge (
Vptr b Ptrofs.zero) =
find_funct_ptr ge b.
Proof.
Theorem find_funct_ptr_iff:
forall ge b f,
find_funct_ptr ge b =
Some f <->
find_def ge b =
Some (
Gfun f).
Proof.
Theorem find_var_info_iff:
forall ge b v,
find_var_info ge b =
Some v <->
find_def ge b =
Some (
Gvar v).
Proof.
Theorem find_def_symbol:
forall p id g,
(
prog_defmap p)!
id =
Some g <->
exists b,
find_symbol (
globalenv p)
id =
Some b /\
find_def (
globalenv p)
b =
Some g.
Proof.
Theorem find_symbol_exists:
forall p id g,
In (
id,
g) (
prog_defs p) ->
exists b,
find_symbol (
globalenv p)
id =
Some b.
Proof.
Theorem find_symbol_inversion :
forall p x b,
find_symbol (
globalenv p)
x =
Some b ->
In x (
prog_defs_names p).
Proof.
Theorem find_def_inversion:
forall p b g,
find_def (
globalenv p)
b =
Some g ->
exists id,
In (
id,
g) (
prog_defs p).
Proof.
Corollary find_funct_ptr_inversion:
forall p b f,
find_funct_ptr (
globalenv p)
b =
Some f ->
exists id,
In (
id,
Gfun f) (
prog_defs p).
Proof.
Corollary find_funct_inversion:
forall p v f,
find_funct (
globalenv p)
v =
Some f ->
exists id,
In (
id,
Gfun f) (
prog_defs p).
Proof.
Theorem find_funct_ptr_prop:
forall (
P:
F ->
Prop)
p b f,
(
forall id f,
In (
id,
Gfun f) (
prog_defs p) ->
P f) ->
find_funct_ptr (
globalenv p)
b =
Some f ->
P f.
Proof.
Theorem find_funct_prop:
forall (
P:
F ->
Prop)
p v f,
(
forall id f,
In (
id,
Gfun f) (
prog_defs p) ->
P f) ->
find_funct (
globalenv p)
v =
Some f ->
P f.
Proof.
Theorem global_addresses_distinct:
forall ge id1 id2 b1 b2,
id1 <>
id2 ->
find_symbol ge id1 =
Some b1 ->
find_symbol ge id2 =
Some b2 ->
b1 <>
b2.
Proof.
intros. red; intros; subst. elim H. destruct ge. eauto.
Qed.
Theorem invert_find_symbol:
forall ge id b,
invert_symbol ge b =
Some id ->
find_symbol ge id =
Some b.
Proof.
Theorem find_invert_symbol:
forall ge id b,
find_symbol ge id =
Some b ->
invert_symbol ge b =
Some id.
Proof.
Definition advance_next (
gl:
list (
ident *
globdef F V)) (
x:
positive) :=
List.fold_left (
fun n g =>
Pos.succ n)
gl x.
Remark genv_next_add_globals:
forall gl ge,
genv_next (
add_globals ge gl) =
advance_next gl (
genv_next ge).
Proof.
induction gl; simpl; intros.
auto.
rewrite IHgl. auto.
Qed.
Remark genv_public_add_globals:
forall gl ge,
genv_public (
add_globals ge gl) =
genv_public ge.
Proof.
induction gl; simpl; intros.
auto.
rewrite IHgl; auto.
Qed.
Theorem globalenv_public:
forall p,
genv_public (
globalenv p) =
prog_public p.
Proof.
Theorem block_is_volatile_below:
forall ge b,
block_is_volatile ge b =
true ->
Plt b ge.(
genv_next).
Proof.
Coercing a global environment into a symbol environment
Definition to_senv (
ge:
t) :
Senv.t :=
@
Senv.mksenv
(
find_symbol ge)
(
public_symbol ge)
(
invert_symbol ge)
(
block_is_volatile ge)
ge.(
genv_next)
ge.(
genv_vars_inj)
(
invert_find_symbol ge)
(
find_invert_symbol ge)
(
public_symbol_exists ge)
ge.(
genv_symb_range)
(
block_is_volatile_below ge).
Construction of the initial memory state
Section INITMEM.
Variable ge:
t.
Definition store_init_data (
m:
mem) (
b:
block) (
p:
Z) (
id:
init_data) :
option mem :=
match id with
|
Init_int8 n =>
Mem.store Mint8unsigned m b p (
Vint n)
|
Init_int16 n =>
Mem.store Mint16unsigned m b p (
Vint n)
|
Init_int32 n =>
Mem.store Mint32 m b p (
Vint n)
|
Init_int64 n =>
Mem.store Mint64 m b p (
Vlong n)
|
Init_float32 n =>
Mem.store Mfloat32 m b p (
Vsingle n)
|
Init_float64 n =>
Mem.store Mfloat64 m b p (
Vfloat n)
|
Init_addrof symb ofs =>
match find_symbol ge symb with
|
None =>
None
|
Some b' =>
Mem.store Mptr m b p (
Vptr b'
ofs)
end
|
Init_space n =>
Some m
end.
Fixpoint store_init_data_list (
m:
mem) (
b:
block) (
p:
Z) (
idl:
list init_data)
{
struct idl}:
option mem :=
match idl with
|
nil =>
Some m
|
id ::
idl' =>
match store_init_data m b p id with
|
None =>
None
|
Some m' =>
store_init_data_list m'
b (
p +
init_data_size id)
idl'
end
end.
Definition perm_globvar (
gv:
globvar V) :
permission :=
if gv.(
gvar_volatile)
then Nonempty
else if gv.(
gvar_readonly)
then Readable
else Writable.
Definition alloc_global (
m:
mem) (
idg:
ident *
globdef F V):
option mem :=
match idg with
| (
id,
Gfun f) =>
let (
m1,
b) :=
Mem.alloc m 0 1
in
Mem.drop_perm m1 b 0 1
Nonempty
| (
id,
Gvar v) =>
let init :=
v.(
gvar_init)
in
let sz :=
init_data_list_size init in
let (
m1,
b) :=
Mem.alloc m 0
sz in
match store_zeros m1 b 0
sz with
|
None =>
None
|
Some m2 =>
match store_init_data_list m2 b 0
init with
|
None =>
None
|
Some m3 =>
Mem.drop_perm m3 b 0
sz (
perm_globvar v)
end
end
end.
Fixpoint alloc_globals (
m:
mem) (
gl:
list (
ident *
globdef F V))
{
struct gl} :
option mem :=
match gl with
|
nil =>
Some m
|
g ::
gl' =>
match alloc_global m g with
|
None =>
None
|
Some m' =>
alloc_globals m'
gl'
end
end.
Lemma alloc_globals_app :
forall gl1 gl2 m m1,
alloc_globals m gl1 =
Some m1 ->
alloc_globals m1 gl2 =
alloc_globals m (
gl1 ++
gl2).
Proof.
induction gl1.
simpl.
intros.
inversion H;
subst.
auto.
simpl.
intros.
destruct (
alloc_global m a);
eauto.
inversion H.
Qed.
Next-block properties
Remark store_zeros_nextblock:
forall m b p n m',
store_zeros m b p n =
Some m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
intros until n.
functional induction (
store_zeros m b p n);
intros.
inv H;
auto.
rewrite IHo;
eauto with mem.
congruence.
Qed.
Remark store_init_data_list_nextblock:
forall idl b m p m',
store_init_data_list m b p idl =
Some m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
Remark alloc_global_nextblock:
forall g m m',
alloc_global m g =
Some m' ->
Mem.nextblock m' =
Pos.succ(
Mem.nextblock m).
Proof.
Remark alloc_globals_nextblock:
forall gl m m',
alloc_globals m gl =
Some m' ->
Mem.nextblock m' =
advance_next gl (
Mem.nextblock m).
Proof.
Permissions
Remark store_zeros_perm:
forall k prm b'
q m b p n m',
store_zeros m b p n =
Some m' ->
(
Mem.perm m b'
q k prm <->
Mem.perm m'
b'
q k prm).
Proof.
intros until n.
functional induction (
store_zeros m b p n);
intros.
inv H;
tauto.
destruct (
IHo _ H);
intros.
split;
eauto with mem.
congruence.
Qed.
Remark store_init_data_perm:
forall k prm b'
q i b m p m',
store_init_data m b p i =
Some m' ->
(
Mem.perm m b'
q k prm <->
Mem.perm m'
b'
q k prm).
Proof.
intros.
assert (
forall chunk v,
Mem.store chunk m b p v =
Some m' ->
(
Mem.perm m b'
q k prm <->
Mem.perm m'
b'
q k prm)).
intros;
split;
eauto with mem.
destruct i;
simpl in H;
eauto.
inv H;
tauto.
destruct (
find_symbol ge i);
try discriminate.
eauto.
Qed.
Remark store_init_data_list_perm:
forall k prm b'
q idl b m p m',
store_init_data_list m b p idl =
Some m' ->
(
Mem.perm m b'
q k prm <->
Mem.perm m'
b'
q k prm).
Proof.
induction idl as [ |
i1 idl];
simpl;
intros.
-
inv H;
tauto.
-
destruct (
store_init_data m b p i1)
as [
m1|]
eqn:
S1;
try discriminate.
transitivity (
Mem.perm m1 b'
q k prm).
eapply store_init_data_perm;
eauto.
eapply IHidl;
eauto.
Qed.
Remark alloc_global_perm:
forall k prm b'
q idg m m',
alloc_global m idg =
Some m' ->
Mem.valid_block m b' ->
(
Mem.perm m b'
q k prm <->
Mem.perm m'
b'
q k prm).
Proof.
Remark alloc_globals_perm:
forall k prm b'
q gl m m',
alloc_globals m gl =
Some m' ->
Mem.valid_block m b' ->
(
Mem.perm m b'
q k prm <->
Mem.perm m'
b'
q k prm).
Proof.
Data preservation properties
Remark store_zeros_unchanged:
forall (
P:
block ->
Z ->
Prop)
m b p n m',
store_zeros m b p n =
Some m' ->
(
forall i,
p <=
i <
p +
n -> ~
P b i) ->
Mem.unchanged_on P m m'.
Proof.
Remark store_init_data_unchanged:
forall (
P:
block ->
Z ->
Prop)
b i m p m',
store_init_data m b p i =
Some m' ->
(
forall ofs,
p <=
ofs <
p +
init_data_size i -> ~
P b ofs) ->
Mem.unchanged_on P m m'.
Proof.
Remark store_init_data_list_unchanged:
forall (
P:
block ->
Z ->
Prop)
b il m p m',
store_init_data_list m b p il =
Some m' ->
(
forall ofs,
p <=
ofs -> ~
P b ofs) ->
Mem.unchanged_on P m m'.
Proof.
Properties related to loadbytes
Definition readbytes_as_zero (
m:
mem) (
b:
block) (
ofs len:
Z) :
Prop :=
forall p n,
ofs <=
p ->
p +
Z.of_nat n <=
ofs +
len ->
Mem.loadbytes m b p (
Z.of_nat n) =
Some (
List.repeat (
Byte Byte.zero)
n).
Lemma store_zeros_loadbytes:
forall m b p n m',
store_zeros m b p n =
Some m' ->
readbytes_as_zero m'
b p n.
Proof.
Definition bytes_of_init_data (
i:
init_data):
list memval :=
match i with
|
Init_int8 n =>
inj_bytes (
encode_int 1%
nat (
Int.unsigned n))
|
Init_int16 n =>
inj_bytes (
encode_int 2%
nat (
Int.unsigned n))
|
Init_int32 n =>
inj_bytes (
encode_int 4%
nat (
Int.unsigned n))
|
Init_int64 n =>
inj_bytes (
encode_int 8%
nat (
Int64.unsigned n))
|
Init_float32 n =>
inj_bytes (
encode_int 4%
nat (
Int.unsigned (
Float32.to_bits n)))
|
Init_float64 n =>
inj_bytes (
encode_int 8%
nat (
Int64.unsigned (
Float.to_bits n)))
|
Init_space n =>
List.repeat (
Byte Byte.zero) (
Z.to_nat n)
|
Init_addrof id ofs =>
match find_symbol ge id with
|
Some b =>
inj_value (
if Archi.ptr64 then Q64 else Q32) (
Vptr b ofs)
|
None =>
List.repeat Undef (
if Archi.ptr64 then 8%
nat else 4%
nat)
end
end.
Remark init_data_size_addrof:
forall id ofs,
init_data_size (
Init_addrof id ofs) =
size_chunk Mptr.
Proof.
Lemma store_init_data_loadbytes:
forall m b p i m',
store_init_data m b p i =
Some m' ->
readbytes_as_zero m b p (
init_data_size i) ->
Mem.loadbytes m'
b p (
init_data_size i) =
Some (
bytes_of_init_data i).
Proof.
Fixpoint bytes_of_init_data_list (
il:
list init_data):
list memval :=
match il with
|
nil =>
nil
|
i ::
il =>
bytes_of_init_data i ++
bytes_of_init_data_list il
end.
Lemma store_init_data_list_loadbytes:
forall b il m p m',
store_init_data_list m b p il =
Some m' ->
readbytes_as_zero m b p (
init_data_list_size il) ->
Mem.loadbytes m'
b p (
init_data_list_size il) =
Some (
bytes_of_init_data_list il).
Proof.
Properties related to load
Definition read_as_zero (
m:
mem) (
b:
block) (
ofs len:
Z) :
Prop :=
forall chunk p,
ofs <=
p ->
p +
size_chunk chunk <=
ofs +
len ->
(
align_chunk chunk |
p) ->
Mem.load chunk m b p =
Some (
match chunk with
|
Mint8unsigned |
Mint8signed |
Mint16unsigned |
Mint16signed |
Mint32 =>
Vint Int.zero
|
Mint64 =>
Vlong Int64.zero
|
Mfloat32 =>
Vsingle Float32.zero
|
Mfloat64 =>
Vfloat Float.zero
|
Many32 |
Many64 =>
Vundef
end).
Remark read_as_zero_unchanged:
forall (
P:
block ->
Z ->
Prop)
m b ofs len m',
read_as_zero m b ofs len ->
Mem.unchanged_on P m m' ->
(
forall i,
ofs <=
i <
ofs +
len ->
P b i) ->
read_as_zero m'
b ofs len.
Proof.
Lemma store_zeros_read_as_zero:
forall m b p n m',
store_zeros m b p n =
Some m' ->
read_as_zero m'
b p n.
Proof.
Fixpoint load_store_init_data (
m:
mem) (
b:
block) (
p:
Z) (
il:
list init_data) {
struct il} :
Prop :=
match il with
|
nil =>
True
|
Init_int8 n ::
il' =>
Mem.load Mint8unsigned m b p =
Some(
Vint(
Int.zero_ext 8
n))
/\
load_store_init_data m b (
p + 1)
il'
|
Init_int16 n ::
il' =>
Mem.load Mint16unsigned m b p =
Some(
Vint(
Int.zero_ext 16
n))
/\
load_store_init_data m b (
p + 2)
il'
|
Init_int32 n ::
il' =>
Mem.load Mint32 m b p =
Some(
Vint n)
/\
load_store_init_data m b (
p + 4)
il'
|
Init_int64 n ::
il' =>
Mem.load Mint64 m b p =
Some(
Vlong n)
/\
load_store_init_data m b (
p + 8)
il'
|
Init_float32 n ::
il' =>
Mem.load Mfloat32 m b p =
Some(
Vsingle n)
/\
load_store_init_data m b (
p + 4)
il'
|
Init_float64 n ::
il' =>
Mem.load Mfloat64 m b p =
Some(
Vfloat n)
/\
load_store_init_data m b (
p + 8)
il'
|
Init_addrof symb ofs ::
il' =>
(
exists b',
find_symbol ge symb =
Some b' /\
Mem.load Mptr m b p =
Some(
Vptr b'
ofs))
/\
load_store_init_data m b (
p +
size_chunk Mptr)
il'
|
Init_space n ::
il' =>
read_as_zero m b p n
/\
load_store_init_data m b (
p +
Z.max n 0)
il'
end.
Lemma store_init_data_list_charact:
forall b il m p m',
store_init_data_list m b p il =
Some m' ->
read_as_zero m b p (
init_data_list_size il) ->
load_store_init_data m'
b p il.
Proof.
Remark alloc_global_unchanged:
forall (
P:
block ->
Z ->
Prop)
m id g m',
alloc_global m (
id,
g) =
Some m' ->
Mem.unchanged_on P m m'.
Proof.
Remark alloc_globals_unchanged:
forall (
P:
block ->
Z ->
Prop)
gl m m',
alloc_globals m gl =
Some m' ->
Mem.unchanged_on P m m'.
Proof.
Remark load_store_init_data_invariant:
forall m m'
b,
(
forall chunk ofs,
Mem.load chunk m'
b ofs =
Mem.load chunk m b ofs) ->
forall il p,
load_store_init_data m b p il ->
load_store_init_data m'
b p il.
Proof.
induction il; intro p; simpl.
auto.
rewrite ! H. destruct a; intuition. red; intros; rewrite H; auto.
Qed.
Definition globals_initialized (
g:
t) (
m:
mem) :=
forall b gd,
find_def g b =
Some gd ->
match gd with
|
Gfun f =>
Mem.perm m b 0
Cur Nonempty
/\ (
forall ofs k p,
Mem.perm m b ofs k p ->
ofs = 0 /\
p =
Nonempty)
|
Gvar v =>
Mem.range_perm m b 0 (
init_data_list_size v.(
gvar_init))
Cur (
perm_globvar v)
/\ (
forall ofs k p,
Mem.perm m b ofs k p ->
0 <=
ofs <
init_data_list_size v.(
gvar_init) /\
perm_order (
perm_globvar v)
p)
/\ (
v.(
gvar_volatile) =
false ->
load_store_init_data m b 0
v.(
gvar_init))
/\ (
v.(
gvar_volatile) =
false ->
Mem.loadbytes m b 0 (
init_data_list_size v.(
gvar_init)) =
Some (
bytes_of_init_data_list v.(
gvar_init)))
end.
Lemma alloc_global_initialized:
forall g m id gd m',
genv_next g =
Mem.nextblock m ->
alloc_global m (
id,
gd) =
Some m' ->
globals_initialized g m ->
globals_initialized (
add_global g (
id,
gd))
m'
/\
genv_next (
add_global g (
id,
gd)) =
Mem.nextblock m'.
Proof.
Lemma alloc_globals_initialized:
forall gl ge m m',
alloc_globals m gl =
Some m' ->
genv_next ge =
Mem.nextblock m ->
globals_initialized ge m ->
globals_initialized (
add_globals ge gl)
m'.
Proof.
induction gl;
simpl;
intros.
-
inv H;
auto.
-
destruct a as [
id g].
destruct (
alloc_global m (
id,
g))
as [
m1|]
eqn:?;
try discriminate.
exploit alloc_global_initialized;
eauto.
intros [
P Q].
eapply IHgl;
eauto.
Qed.
End INITMEM.
Definition init_mem (
p:
program F V) :=
alloc_globals (
globalenv p)
Mem.empty p.(
prog_defs).
Lemma init_mem_genv_next:
forall p m,
init_mem p =
Some m ->
genv_next (
globalenv p) =
Mem.nextblock m.
Proof.
Theorem find_symbol_not_fresh:
forall p id b m,
init_mem p =
Some m ->
find_symbol (
globalenv p)
id =
Some b ->
Mem.valid_block m b.
Proof.
Theorem find_def_not_fresh:
forall p b g m,
init_mem p =
Some m ->
find_def (
globalenv p)
b =
Some g ->
Mem.valid_block m b.
Proof.
Theorem find_funct_ptr_not_fresh:
forall p b f m,
init_mem p =
Some m ->
find_funct_ptr (
globalenv p)
b =
Some f ->
Mem.valid_block m b.
Proof.
Theorem find_var_info_not_fresh:
forall p b gv m,
init_mem p =
Some m ->
find_var_info (
globalenv p)
b =
Some gv ->
Mem.valid_block m b.
Proof.
Lemma init_mem_characterization_gen:
forall p m,
init_mem p =
Some m ->
globals_initialized (
globalenv p) (
globalenv p)
m.
Proof.
Theorem init_mem_characterization:
forall p b gv m,
find_var_info (
globalenv p)
b =
Some gv ->
init_mem p =
Some m ->
Mem.range_perm m b 0 (
init_data_list_size gv.(
gvar_init))
Cur (
perm_globvar gv)
/\ (
forall ofs k p,
Mem.perm m b ofs k p ->
0 <=
ofs <
init_data_list_size gv.(
gvar_init) /\
perm_order (
perm_globvar gv)
p)
/\ (
gv.(
gvar_volatile) =
false ->
load_store_init_data (
globalenv p)
m b 0
gv.(
gvar_init))
/\ (
gv.(
gvar_volatile) =
false ->
Mem.loadbytes m b 0 (
init_data_list_size gv.(
gvar_init)) =
Some (
bytes_of_init_data_list (
globalenv p)
gv.(
gvar_init))).
Proof.
Theorem init_mem_characterization_2:
forall p b fd m,
find_funct_ptr (
globalenv p)
b =
Some fd ->
init_mem p =
Some m ->
Mem.perm m b 0
Cur Nonempty
/\ (
forall ofs k p,
Mem.perm m b ofs k p ->
ofs = 0 /\
p =
Nonempty).
Proof.
Compatibility with memory injections
Section INITMEM_INJ.
Variable ge:
t.
Variable thr:
block.
Hypothesis symb_inject:
forall id b,
find_symbol ge id =
Some b ->
Plt b thr.
Lemma store_zeros_neutral:
forall m b p n m',
Mem.inject_neutral thr m ->
Plt b thr ->
store_zeros m b p n =
Some m' ->
Mem.inject_neutral thr m'.
Proof.
Lemma store_init_data_neutral:
forall m b p id m',
Mem.inject_neutral thr m ->
Plt b thr ->
store_init_data ge m b p id =
Some m' ->
Mem.inject_neutral thr m'.
Proof.
Lemma store_init_data_list_neutral:
forall b idl m p m',
Mem.inject_neutral thr m ->
Plt b thr ->
store_init_data_list ge m b p idl =
Some m' ->
Mem.inject_neutral thr m'.
Proof.
Lemma alloc_global_neutral:
forall idg m m',
alloc_global ge m idg =
Some m' ->
Mem.inject_neutral thr m ->
Plt (
Mem.nextblock m)
thr ->
Mem.inject_neutral thr m'.
Proof.
Remark advance_next_le:
forall gl x,
Ple x (
advance_next gl x).
Proof.
Lemma alloc_globals_neutral:
forall gl m m',
alloc_globals ge m gl =
Some m' ->
Mem.inject_neutral thr m ->
Ple (
Mem.nextblock m')
thr ->
Mem.inject_neutral thr m'.
Proof.
End INITMEM_INJ.
Theorem initmem_inject:
forall p m,
init_mem p =
Some m ->
Mem.inject (
Mem.flat_inj (
Mem.nextblock m))
m m.
Proof.
Sufficient and necessary conditions for the initial memory to exist.
Alignment properties
Definition init_data_alignment (
i:
init_data) :
Z :=
match i with
|
Init_int8 n => 1
|
Init_int16 n => 2
|
Init_int32 n => 4
|
Init_int64 n => 8
|
Init_float32 n => 4
|
Init_float64 n => 4
|
Init_addrof symb ofs =>
if Archi.ptr64 then 8
else 4
|
Init_space n => 1
end.
Fixpoint init_data_list_aligned (
p:
Z) (
il:
list init_data) {
struct il} :
Prop :=
match il with
|
nil =>
True
|
i1 ::
il => (
init_data_alignment i1 |
p) /\
init_data_list_aligned (
p +
init_data_size i1)
il
end.
Section INITMEM_INVERSION.
Variable ge:
t.
Lemma store_init_data_aligned:
forall m b p i m',
store_init_data ge m b p i =
Some m' ->
(
init_data_alignment i |
p).
Proof.
Lemma store_init_data_list_aligned:
forall b il m p m',
store_init_data_list ge m b p il =
Some m' ->
init_data_list_aligned p il.
Proof.
Lemma store_init_data_list_free_idents:
forall b i o il m p m',
store_init_data_list ge m b p il =
Some m' ->
In (
Init_addrof i o)
il ->
exists b',
find_symbol ge i =
Some b'.
Proof.
induction il as [ |
i1 il];
simpl;
intros.
-
contradiction.
-
destruct (
store_init_data ge m b p i1)
as [
m1|]
eqn:
S1;
try discriminate.
destruct H0.
+
subst i1.
simpl in S1.
destruct (
find_symbol ge i)
as [
b'|].
exists b';
auto.
discriminate.
+
eapply IHil;
eauto.
Qed.
End INITMEM_INVERSION.
Theorem init_mem_inversion:
forall p m id v,
init_mem p =
Some m ->
In (
id,
Gvar v)
p.(
prog_defs) ->
init_data_list_aligned 0
v.(
gvar_init)
/\
forall i o,
In (
Init_addrof i o)
v.(
gvar_init) ->
exists b,
find_symbol (
globalenv p)
i =
Some b.
Proof.
Section INITMEM_EXISTS.
Variable ge:
t.
Lemma store_zeros_exists:
forall m b p n,
Mem.range_perm m b p (
p +
n)
Cur Writable ->
exists m',
store_zeros m b p n =
Some m'.
Proof.
Lemma store_init_data_exists:
forall m b p i,
Mem.range_perm m b p (
p +
init_data_size i)
Cur Writable ->
(
init_data_alignment i |
p) ->
(
forall id ofs,
i =
Init_addrof id ofs ->
exists b,
find_symbol ge id =
Some b) ->
exists m',
store_init_data ge m b p i =
Some m'.
Proof.
Lemma store_init_data_list_exists:
forall b il m p,
Mem.range_perm m b p (
p +
init_data_list_size il)
Cur Writable ->
init_data_list_aligned p il ->
(
forall id ofs,
In (
Init_addrof id ofs)
il ->
exists b,
find_symbol ge id =
Some b) ->
exists m',
store_init_data_list ge m b p il =
Some m'.
Proof.
Lemma alloc_global_exists:
forall m idg,
match idg with
| (
id,
Gfun f) =>
True
| (
id,
Gvar v) =>
init_data_list_aligned 0
v.(
gvar_init)
/\
forall i o,
In (
Init_addrof i o)
v.(
gvar_init) ->
exists b,
find_symbol ge i =
Some b
end ->
exists m',
alloc_global ge m idg =
Some m'.
Proof.
End INITMEM_EXISTS.
Theorem init_mem_exists:
forall p,
(
forall id v,
In (
id,
Gvar v) (
prog_defs p) ->
init_data_list_aligned 0
v.(
gvar_init)
/\
forall i o,
In (
Init_addrof i o)
v.(
gvar_init) ->
exists b,
find_symbol (
globalenv p)
i =
Some b) ->
exists m,
init_mem p =
Some m.
Proof.
intros.
set (
ge :=
globalenv p)
in *.
unfold init_mem.
revert H.
generalize (
prog_defs p)
Mem.empty.
induction l as [ |
idg l];
simpl;
intros.
-
exists m;
auto.
-
destruct (@
alloc_global_exists ge m idg)
as [
m1 A1].
destruct idg as [
id [
f|
v]];
eauto.
fold ge.
rewrite A1.
eapply IHl;
eauto.
Qed.
End GENV.
Commutation with program transformations
Section MATCH_GENVS.
Context {
A B V W:
Type} (
R:
globdef A V ->
globdef B W ->
Prop).
Record match_genvs (
ge1:
t A V) (
ge2:
t B W):
Prop := {
mge_next:
genv_next ge2 =
genv_next ge1;
mge_symb:
forall id,
PTree.get id (
genv_symb ge2) =
PTree.get id (
genv_symb ge1);
mge_defs:
forall b,
option_rel R (
PTree.get b (
genv_defs ge1)) (
PTree.get b (
genv_defs ge2))
}.
Lemma add_global_match:
forall ge1 ge2 id g1 g2,
match_genvs ge1 ge2 ->
R g1 g2 ->
match_genvs (
add_global ge1 (
id,
g1)) (
add_global ge2 (
id,
g2)).
Proof.
intros.
destruct H.
constructor;
simpl;
intros.
-
congruence.
-
rewrite mge_next0, !
PTree.gsspec.
destruct (
peq id0 id);
auto.
-
rewrite mge_next0, !
PTree.gsspec.
destruct (
peq b (
genv_next ge1)).
constructor;
auto.
auto.
Qed.
Lemma add_globals_match:
forall gl1 gl2,
list_forall2 (
fun idg1 idg2 =>
fst idg1 =
fst idg2 /\
R (
snd idg1) (
snd idg2))
gl1 gl2 ->
forall ge1 ge2,
match_genvs ge1 ge2 ->
match_genvs (
add_globals ge1 gl1) (
add_globals ge2 gl2).
Proof.
induction 1;
intros;
simpl.
auto.
destruct a1 as [
id1 g1];
destruct b1 as [
id2 g2];
simpl in *;
destruct H;
subst id2.
apply IHlist_forall2.
apply add_global_match;
auto.
Qed.
End MATCH_GENVS.
Section MATCH_PROGRAMS.
Context {
C F1 V1 F2 V2:
Type} {
LC:
Linker C} {
LF:
Linker F1} {
LV:
Linker V1}.
Variable match_fundef:
C ->
F1 ->
F2 ->
Prop.
Variable match_varinfo:
V1 ->
V2 ->
Prop.
Variable ctx:
C.
Variable p:
program F1 V1.
Variable tp:
program F2 V2.
Hypothesis progmatch:
match_program_gen match_fundef match_varinfo ctx p tp.
Lemma globalenvs_match:
match_genvs (
match_globdef match_fundef match_varinfo ctx) (
globalenv p) (
globalenv tp).
Proof.
Theorem find_def_match_2:
forall b,
option_rel (
match_globdef match_fundef match_varinfo ctx)
(
find_def (
globalenv p)
b) (
find_def (
globalenv tp)
b).
Proof (
mge_defs globalenvs_match).
Theorem find_def_match:
forall b g,
find_def (
globalenv p)
b =
Some g ->
exists tg,
find_def (
globalenv tp)
b =
Some tg /\
match_globdef match_fundef match_varinfo ctx g tg.
Proof.
intros.
generalize (
find_def_match_2 b).
rewrite H;
intros R;
inv R.
exists y;
auto.
Qed.
Theorem find_funct_ptr_match:
forall b f,
find_funct_ptr (
globalenv p)
b =
Some f ->
exists cunit tf,
find_funct_ptr (
globalenv tp)
b =
Some tf /\
match_fundef cunit f tf /\
linkorder cunit ctx.
Proof.
Theorem find_funct_match:
forall v f,
find_funct (
globalenv p)
v =
Some f ->
exists cunit tf,
find_funct (
globalenv tp)
v =
Some tf /\
match_fundef cunit f tf /\
linkorder cunit ctx.
Proof.
Theorem find_var_info_match:
forall b v,
find_var_info (
globalenv p)
b =
Some v ->
exists tv,
find_var_info (
globalenv tp)
b =
Some tv /\
match_globvar match_varinfo v tv.
Proof.
Theorem find_symbol_match:
forall (
s :
ident),
find_symbol (
globalenv tp)
s =
find_symbol (
globalenv p)
s.
Proof.
Theorem senv_match:
Senv.equiv (
to_senv (
globalenv p)) (
to_senv (
globalenv tp)).
Proof.
Lemma store_init_data_list_match:
forall idl m b ofs m',
store_init_data_list (
globalenv p)
m b ofs idl =
Some m' ->
store_init_data_list (
globalenv tp)
m b ofs idl =
Some m'.
Proof.
Lemma alloc_globals_match:
forall gl1 gl2,
list_forall2 (
match_ident_globdef match_fundef match_varinfo ctx)
gl1 gl2 ->
forall m m',
alloc_globals (
globalenv p)
m gl1 =
Some m' ->
alloc_globals (
globalenv tp)
m gl2 =
Some m'.
Proof.
Theorem init_mem_match:
forall m,
init_mem p =
Some m ->
init_mem tp =
Some m.
Proof.
End MATCH_PROGRAMS.
Special case for partial transformations that do not depend on the compilation unit
Section TRANSFORM_PARTIAL.
Context {
A B V:
Type} {
LA:
Linker A} {
LV:
Linker V}.
Context {
transf:
A ->
res B} {
p:
program A V} {
tp:
program B V}.
Hypothesis progmatch:
match_program (
fun cu f tf =>
transf f =
OK tf)
eq p tp.
Theorem find_funct_ptr_transf_partial:
forall b f,
find_funct_ptr (
globalenv p)
b =
Some f ->
exists tf,
find_funct_ptr (
globalenv tp)
b =
Some tf /\
transf f =
OK tf.
Proof.
Theorem find_funct_transf_partial:
forall v f,
find_funct (
globalenv p)
v =
Some f ->
exists tf,
find_funct (
globalenv tp)
v =
Some tf /\
transf f =
OK tf.
Proof.
Theorem find_symbol_transf_partial:
forall (
s :
ident),
find_symbol (
globalenv tp)
s =
find_symbol (
globalenv p)
s.
Proof.
Theorem senv_transf_partial:
Senv.equiv (
to_senv (
globalenv p)) (
to_senv (
globalenv tp)).
Proof.
Theorem init_mem_transf_partial:
forall m,
init_mem p =
Some m ->
init_mem tp =
Some m.
Proof.
End TRANSFORM_PARTIAL.
Special case for total transformations that do not depend on the compilation unit
Section TRANSFORM_TOTAL.
Context {
A B V:
Type} {
LA:
Linker A} {
LV:
Linker V}.
Context {
transf:
A ->
B} {
p:
program A V} {
tp:
program B V}.
Hypothesis progmatch:
match_program (
fun cu f tf =>
tf =
transf f)
eq p tp.
Theorem find_funct_ptr_transf:
forall b f,
find_funct_ptr (
globalenv p)
b =
Some f ->
find_funct_ptr (
globalenv tp)
b =
Some (
transf f).
Proof.
Theorem find_funct_transf:
forall v f,
find_funct (
globalenv p)
v =
Some f ->
find_funct (
globalenv tp)
v =
Some (
transf f).
Proof.
Theorem find_symbol_transf:
forall (
s :
ident),
find_symbol (
globalenv tp)
s =
find_symbol (
globalenv p)
s.
Proof.
Theorem senv_transf:
Senv.equiv (
to_senv (
globalenv p)) (
to_senv (
globalenv tp)).
Proof.
Theorem init_mem_transf:
forall m,
init_mem p =
Some m ->
init_mem tp =
Some m.
Proof.
End TRANSFORM_TOTAL.
End Genv.
Coercion Genv.to_senv:
Genv.t >->
Senv.t.