Require Import Coqlib.
Require Import Maps.
Require Import Compopts.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import ExprEval Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Lattice.
Require Import Kildall.
Require Import Registers.
Require Import Op.
Require Import RTL.
Require Import ValueDomain.
Require Import ValueAOp.
Require Import Liveness.
The dataflow analysis
Definition areg (
ae:
aenv) (
r:
reg) :
aval :=
AE.get r ae.
Definition aregs (
ae:
aenv) (
rl:
list reg) :
list aval :=
List.map (
areg ae)
rl.
Definition mafter_public_call :
amem :=
mtop.
Definition mafter_private_call (
am_before:
amem) :
amem :=
{|
am_stack :=
am_before.(
am_stack);
am_glob :=
PTree.empty _;
am_nonstack :=
Nonstack;
am_top :=
eplub (
ab_summary (
am_stack am_before))
Nonstack |}.
Axiom trace_calls :
bool ->
unit.
Definition print (
printer:
bool ->
unit) (
b:
bool) (
v:
VA.t') :
VA.t' :=
let unused :=
printer b in v.
Definition transfer_call (
ae:
aenv) (
am:
amem) (
args:
list reg) (
res:
reg) :=
if epincl am.(
am_nonstack)
Nonstack
&&
forallb (
fun r =>
epincl (
provenance (
areg ae r))
Nonstack)
args
then
print trace_calls true
(
VA.State (
AE.set res (
Ptr Nonstack)
ae) (
mafter_private_call am))
else
print trace_calls false
(
VA.State (
AE.set res Vtop ae)
mafter_public_call).
Inductive builtin_kind :
Type :=
|
Builtin_vload (
chunk:
memory_chunk) (
aaddr:
aval)
|
Builtin_vstore (
chunk:
memory_chunk) (
aaddr av:
aval)
|
Builtin_memcpy (
sz al:
Z) (
adst asrc:
aval)
|
Builtin_annot
|
Builtin_annot_val (
av:
aval)
|
Builtin_default
.
Definition classify_builtin (
ef:
external_function) (
args:
list reg) (
ae:
aenv) :=
match ef,
args with
|
EF_vload chunk,
a1::
nil =>
Builtin_vload chunk (
areg ae a1)
|
EF_vload_global chunk id ofs,
nil =>
Builtin_vload chunk (
Ptr (
Gl id ofs))
|
EF_vstore chunk,
a1::
a2::
nil =>
Builtin_vstore chunk (
areg ae a1) (
areg ae a2)
|
EF_vstore_global chunk id ofs,
a1::
nil =>
Builtin_vstore chunk (
Ptr (
Gl id ofs)) (
areg ae a1)
|
EF_memcpy sz al,
a1::
a2::
nil =>
Builtin_memcpy sz al (
areg ae a1) (
areg ae a2)
|
EF_annot _ _,
_ =>
Builtin_annot
|
EF_annot_val _ _,
a1::
nil =>
Builtin_annot_val (
areg ae a1)
|
_,
_ =>
Builtin_default
end.
Definition transfer_builtin (
ae:
aenv) (
am:
amem) (
rm:
romem) (
ef:
external_function) (
args:
list reg) (
res:
reg) :=
match classify_builtin ef args ae with
|
Builtin_vload chunk aaddr =>
let a :=
if va_strict tt
then evlub (
loadv chunk rm am aaddr) (
vnormalize chunk (
Ptr Glob))
else vnormalize chunk Vtop in
VA.State (
AE.set res a ae)
am
|
Builtin_vstore chunk aaddr av =>
let am' :=
storev chunk am aaddr av in
VA.State (
AE.set res Vtop ae) (
mlub am am')
|
Builtin_memcpy sz al adst asrc =>
if zlt 0
sz
then
let p :=
loadbytes am rm (
aptr_of_aval asrc)
in
let am' :=
storebytes am (
aptr_of_aval adst)
sz p in
VA.State (
AE.set res Vtop ae)
am'
else VA.State (
AE.set res Vtop ae)
am
|
Builtin_annot =>
VA.State (
AE.set res Vtop ae)
am
|
Builtin_annot_val av =>
VA.State (
AE.set res av ae)
am
|
Builtin_default =>
transfer_call ae am args res
end.
Definition transfer (
f:
function) (
rm:
romem) (
pc:
node) (
ae:
aenv) (
am:
amem) :
VA.t :=
match f.(
fn_code)!
pc with
|
None =>
VA.Bot
|
Some(
Inop s) =>
VA.State ae am
|
Some(
Iop op args res s) =>
let a :=
eval_static_operation op (
aregs ae args)
in
VA.State (
AE.set res a ae)
am
|
Some(
Iload chunk addr args dst s) =>
let a :=
loadv chunk rm am (
eval_static_addressing addr (
aregs ae args))
in
VA.State (
AE.set dst a ae)
am
|
Some(
Istore chunk addr args src s) =>
let am' :=
storev chunk am (
eval_static_addressing addr (
aregs ae args)) (
areg ae src)
in
VA.State ae am'
|
Some(
Icall sig ros args res s) =>
transfer_call ae am args res
|
Some(
Itailcall sig ros args) =>
VA.Bot
|
Some(
Ibuiltin ef args res s) =>
transfer_builtin ae am rm ef args res
|
Some(
Icond cond args s1 s2) =>
VA.State ae am
|
Some(
Ijumptable arg tbl) =>
VA.State ae am
|
Some(
Ireturn arg) =>
VA.Bot
end.
Definition transfer' (
f:
function) (
lastuses:
PTree.t (
list reg)) (
rm:
romem)
(
pc:
node) (
before:
VA.t) :
VA.t :=
match before with
|
VA.Bot =>
VA.Bot
|
VA.State ae am =>
match transfer f rm pc ae am with
|
VA.Bot =>
VA.Bot
|
VA.State ae'
am' =>
let ae'' :=
match lastuses!
pc with
|
None =>
ae'
|
Some regs =>
eforget regs ae'
end in
VA.State ae''
am'
end
end.
Module DS :=
Dataflow_Solver(
VA)(
NodeSetForward).
Definition mfunction_entry :=
{|
am_stack :=
ablock_init Pcst;
am_glob :=
PTree.empty _;
am_nonstack :=
Nonstack;
am_top :=
Nonstack |}.
Definition set_print (
v:
unit ->
VA.t) (
p:
PMap.t VA.t) :=
let _ :=
v tt in p.
Definition analyze (
rm:
romem) (
f:
function):
PMap.t VA.t :=
let lu :=
Liveness.last_uses f in
let entry :=
VA.State (
einit_regs f.(
fn_params))
mfunction_entry in
match DS.fixpoint f.(
fn_code)
successors_instr (
transfer'
f lu rm)
f.(
fn_entrypoint)
entry with
|
None =>
PMap.init (
VA.State AE.top mtop)
|
Some res =>
set_print (
fun (
_:
unit) =>
PTree.fold (
fun (
acc:
VA.t) (
pc:
positive) (
va:
VA.t) =>
(
transfer'
f lu rm pc va))
(
snd res)
VA.Bot)
res
end.
Constructing the approximation of read-only globals
Definition store_init_data (
ab:
ablock) (
p:
Z) (
id:
init_data) :
ablock :=
match id with
|
Init_int8 n =>
ablock_store Mint8unsigned ab p (
I n)
|
Init_int16 n =>
ablock_store Mint16unsigned ab p (
I n)
|
Init_int32 n =>
ablock_store Mint32 ab p (
I n)
|
Init_int64 n =>
ablock_store Mint64 ab p (
L n)
|
Init_float32 n =>
ablock_store Mfloat32 ab p (
FS n)
|
Init_float64 n =>
ablock_store Mfloat64 ab p (
F n)
|
Init_addrof symb ofs =>
ablock_store Mint32 ab p (
Ptr (
Gl symb ofs))
|
Init_space n _ =>
ab
end.
Fixpoint store_init_data_list (
ab:
ablock) (
p:
Z) (
idl:
list init_data)
{
struct idl}:
ablock :=
match idl with
|
nil =>
ab
|
id ::
idl' =>
store_init_data_list (
store_init_data ab p id) (
p +
Genv.init_data_size id)
idl'
end.
Definition alloc_global (
rm:
romem) (
idg:
ident *
globdef fundef unit):
romem :=
match idg with
| (
id,
Gfun f) =>
PTree.remove id rm
| (
id,
Gvar v) =>
if v.(
gvar_readonly) &&
negb v.(
gvar_volatile)
then PTree.set id (
store_init_data_list (
ablock_init Pcst) 0
v.(
gvar_init))
rm
else PTree.remove id rm
end.
Definition romem_for_program (
p:
program) :
romem :=
List.fold_left alloc_global p.(
prog_defs) (
PTree.empty _).
Soundness proof
Properties of the dataflow solution.
Lemma analyze_entrypoint:
forall rm f vl m bc
,
(
forall v,
In v vl ->
evmatch bc v (
Ptr Nonstack)) ->
mmatch bc m mfunction_entry ->
exists ae am,
(
analyze rm f)!!(
fn_entrypoint f) =
VA.State ae am
/\
ematch bc (
init_regs vl (
fn_params f))
ae
/\
mmatch bc m am.
Proof.
Lemma analyze_successor:
forall f n ae am instr s rm ae'
am',
(
analyze rm f)!!
n =
VA.State ae am ->
f.(
fn_code)!
n =
Some instr ->
In s (
successors_instr instr) ->
transfer f rm n ae am =
VA.State ae'
am' ->
VA.ge (
analyze rm f)!!
s (
transfer f rm n ae am).
Proof.
Lemma analyze_succ:
forall e m rm f n ae am instr s ae'
am'
bc
,
(
analyze rm f)!!
n =
VA.State ae am ->
f.(
fn_code)!
n =
Some instr ->
In s (
successors_instr instr) ->
transfer f rm n ae am =
VA.State ae'
am' ->
ematch bc e ae' ->
mmatch bc m am' ->
exists ae''
am'',
(
analyze rm f)!!
s =
VA.State ae''
am''
/\
ematch bc e ae''
/\
mmatch bc m am''.
Proof.
intros.
exploit analyze_successor;
eauto.
rewrite H2.
destruct (
analyze rm f)#
s as [ |
ae''
am''];
simpl;
try tauto.
intros [
A B].
exists ae'',
am''.
split.
auto.
split.
eapply ematch_ge;
eauto.
eauto.
Qed.
Classification of builtin functions
Lemma classify_builtin_sound:
forall bc e ae ef (
ge:
genv)
args m t res m',
ematch bc e ae ->
genv_match bc ge ->
external_call ef ge e##
args m t res m' ->
match classify_builtin ef args ae with
|
Builtin_vload chunk aaddr =>
exists addr,
volatile_load_sem chunk ge (
addr::
nil)
m t res m' /\
evmatch bc addr aaddr
|
Builtin_vstore chunk aaddr av =>
exists addr v,
volatile_store_sem chunk ge (
addr::
v::
nil)
m t res m'
/\
evmatch bc addr aaddr /\
evmatch bc v av
|
Builtin_memcpy sz al adst asrc =>
exists dst,
exists src,
extcall_memcpy_sem sz al ge (
dst::
src::
nil)
m t res m'
/\
evmatch bc dst adst /\
evmatch bc src asrc
|
Builtin_annot =>
m' =
m /\
is_constant Vundef res
|
Builtin_annot_val av =>
m' =
m /\
evmatch bc res av
|
Builtin_default =>
True
end.
Proof.
intros.
unfold classify_builtin;
destruct ef;
auto.
-
destruct args;
auto.
destruct args;
auto.
exists (
e#
p);
split;
eauto.
-
destruct args;
auto.
destruct args;
auto.
destruct args;
auto.
exists (
e#
p), (
e#
p0);
eauto.
-
destruct args;
auto.
simpl in H1.
rewrite volatile_load_global_charact in H1.
destruct H1 as (
b &
A &
B).
exists (
Values_symbolictype.Eval(
Vptr b ofs));
split;
auto.
econstructor ;
eauto.
econstructor.
eapply H0;
eauto.
repeat intro ;
reflexivity.
-
destruct args;
auto.
destruct args;
auto.
simpl in H1.
rewrite volatile_store_global_charact in H1.
destruct H1 as (
b &
A &
B).
exists (
Values_symbolictype.Eval(
Vptr b ofs)), (
e#
p);
split;
auto.
split;
eauto.
constructor.
econstructor.
eapply H0;
eauto.
repeat intro ;
reflexivity.
-
destruct args;
auto.
destruct args;
auto.
destruct args;
auto.
exists (
e#
p), (
e#
p0);
eauto.
-
simpl in H1.
inv H1.
split.
auto.
red.
reflexivity.
-
destruct args;
auto.
destruct args;
auto.
simpl in H1.
inv H1.
split;
eauto.
Qed.
Constructing block classifications
Definition bc_nostack (
bc:
block_classification) :
Prop :=
forall b,
bc b <>
BCstack.
Section NOSTACK.
Variable bc:
block_classification.
Hypothesis NOSTACK:
bc_nostack bc.
Lemma pmatch_no_stack:
forall e p,
epmatch bc e p ->
epmatch bc e Nonstack.
Proof.
Lemma vmatch_no_stack:
forall v x ,
evmatch bc v x ->
evmatch bc v (
Ptr Nonstack).
Proof.
Lemma smatch_no_stack:
forall m b p,
smatch bc m b p ->
smatch bc m b Nonstack.
Proof.
intros.
destruct H as [
A B].
split;
intros.
-
reflexivity.
-
exploit B ;
eauto.
destruct mv ;
simpl in *.
eapply pmatch_no_stack;
eauto.
Qed.
Lemma mmatch_no_stack:
forall m am astk,
mmatch bc m am ->
mmatch bc m {|
am_stack :=
astk;
am_glob :=
PTree.empty _;
am_nonstack :=
Nonstack;
am_top :=
Nonstack |}.
Proof.
End NOSTACK.
Construction 1: allocating the stack frame at function entry
Ltac splitall :=
repeat (
match goal with |-
_ /\
_ =>
split end).
Theorem allocate_stack:
forall m sz m'
sp bc ge rm am,
Mem.alloc m 0
sz Normal =
Some (
m',
sp) ->
genv_match bc ge ->
romatch bc m rm ->
mmatch bc m am ->
bc_nostack bc ->
exists bc',
bc_incr bc bc'
/\
bc'
sp =
BCstack
/\
genv_match bc'
ge
/\
romatch bc'
m'
rm
/\
mmatch bc'
m'
mfunction_entry
/\ (
forall b,
Plt b sp ->
bc'
b =
bc b)
/\ (
forall v x,
evmatch bc v x ->
evmatch bc'
v (
Ptr Nonstack)).
Proof.
Theorem loadbytes_allocbytes_unchanged:
forall m1 n m2 (
AB:
MemReserve.reserve_boxes m1 n =
Some m2)
b'
ofs n0
(
VB:
Mem.valid_block m1 b'),
Mem.loadbytes m2 b'
ofs n0 =
Mem.loadbytes m1 b'
ofs n0.
Proof.
Lemma romatch_allocbytes
:
forall (
bc :
block_classification) (
m :
mem)
(
n :
nat) (
m' :
mem) (
rm :
romem),
MemReserve.reserve_boxes m n =
Some m' ->
bc_below bc (
Mem.nextblock m) ->
romatch bc m rm ->
romatch bc m'
rm.
Proof.
red;
intros.
exploit H1;
eauto.
intros [
A [
B C]].
repSplit;
auto.
inv B.
constructor.
inv BMS.
constructor;
auto.
intros;
eapply SMLD;
eauto.
rewrite <-
H5.
symmetry.
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply H0.
congruence.
intros;
eapply BML;
eauto.
eapply loadbytes_load_ext with (
m':=
m');
eauto.
intros.
rewrite <-
H5.
symmetry.
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply H0.
congruence.
intros ofs PERM.
unfold MemReserve.reserve_boxes in H;
destr_in H.
inv H.
eapply C.
apply PERM.
Qed.
Lemma match_allocbytes
:
forall (
bc :
block_classification) (
m :
mem)
(
n :
nat) (
m' :
mem) (
am :
amem)
(
AB:
MemReserve.reserve_boxes m n =
Some m')
(
MM:
mmatch bc m am),
mmatch bc m'
am.
Proof.
intros.
inv MM;
constructor;
auto.
-
intros.
exploit mmatch_stack;
eauto.
intro A;
inv A.
constructor.
inv BMS;
constructor;
auto.
intros;
eapply SMLD;
eauto.
rewrite <-
H1.
symmetry.
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply mmatch_below.
congruence.
intros;
eapply BML;
eauto.
eapply loadbytes_load_ext with (
m':=
m');
eauto.
intros.
rewrite <-
H1.
symmetry.
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply mmatch_below.
congruence.
-
intros.
exploit mmatch_glob;
eauto.
intro A;
inv A.
constructor.
inv BMS;
constructor;
auto.
intros;
eapply SMLD;
eauto.
rewrite <-
H2.
symmetry.
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply mmatch_below.
congruence.
intros;
eapply BML;
eauto.
eapply loadbytes_load_ext with (
m':=
m');
eauto.
intros.
rewrite <-
H2.
symmetry.
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply mmatch_below.
congruence.
-
intros.
exploit mmatch_nonstack;
eauto.
intro A;
inv A.
constructor.
auto.
intros;
eapply SMLD;
eauto.
rewrite <-
H2.
symmetry.
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply mmatch_below.
congruence.
-
intros.
exploit mmatch_top;
eauto.
intro A;
inv A.
constructor;
auto.
intros;
eapply SMLD;
eauto.
rewrite <-
H1;
symmetry;
eapply loadbytes_allocbytes_unchanged;
eauto.
red.
apply mmatch_below.
congruence.
-
red.
intros.
exploit mmatch_below;
eauto.
rewrite (
MemReserve.reserve_nextblock _ _ _ AB).
xomega.
Qed.
Theorem allocate_stack':
forall m n m'
bc ge rm am,
MemReserve.reserve_boxes m n =
Some m' ->
genv_match bc ge ->
romatch bc m rm ->
mmatch bc m am ->
romatch bc m'
rm
/\
mmatch bc m'
am
.
Proof.
Construction 2: turn the stack into an "other" block, at public calls or function returns
Theorem anonymize_stack:
forall m sp bc ge rm am
,
genv_match bc ge ->
romatch bc m rm ->
mmatch bc m am ->
bc sp =
BCstack ->
exists bc',
bc_nostack bc'
/\
bc'
sp =
BCother
/\ (
forall b,
b <>
sp ->
bc'
b =
bc b)
/\ (
forall v x,
evmatch bc v x ->
evmatch bc'
v Vtop)
/\
genv_match bc'
ge
/\
romatch bc'
m rm
/\
mmatch bc'
m mtop.
Proof.
Construction 3: turn the stack into an invalid block, at private calls
Theorem hide_stack:
forall m sp bc ge rm am
,
genv_match bc ge ->
romatch bc m rm ->
mmatch bc m am ->
bc sp =
BCstack ->
epge Nonstack am.(
am_nonstack) ->
exists bc',
bc_nostack bc'
/\
bc'
sp =
BCinvalid
/\ (
forall b,
b <>
sp ->
bc'
b =
bc b)
/\ (
forall v x,
evge (
Ptr Nonstack)
x ->
evmatch bc v x ->
evmatch bc'
v Vtop)
/\
genv_match bc'
ge
/\
romatch bc'
m rm
/\
mmatch bc'
m mtop.
Proof.
Construction 4: restore the stack after a public call
Theorem return_from_public_call:
forall (
caller callee:
block_classification)
bound sp ge e ae v m rm
,
bc_below caller bound ->
callee sp =
BCother ->
caller sp =
BCstack ->
(
forall b,
Plt b bound ->
b <>
sp ->
caller b =
callee b) ->
genv_match caller ge ->
ematch caller e ae ->
Ple bound (
Mem.nextblock m) ->
evmatch callee v Vtop ->
romatch callee m rm ->
mmatch callee m mtop ->
genv_match callee ge ->
bc_nostack callee ->
exists bc,
evmatch bc v Vtop
/\
ematch bc e ae
/\
romatch bc m rm
/\
mmatch bc m mafter_public_call
/\
genv_match bc ge
/\
bc sp =
BCstack
/\ (
forall b,
Plt b sp ->
bc b =
caller b).
Proof.
intros until rm;
intros BELOW SP1 SP2 SAME GE1 EM BOUND RESM RM MM GE2 NOSTACK.
set (
f :=
fun b =>
if eq_block b sp then BCstack else callee b).
assert (
F_stack:
forall b1 b2,
f b1 =
BCstack ->
f b2 =
BCstack ->
b1 =
b2).
{
assert (
forall b,
f b =
BCstack ->
b =
sp).
{
unfold f;
intros.
destruct (
eq_block b sp);
auto.
eelim NOSTACK;
eauto. }
intros.
transitivity sp;
auto.
symmetry;
auto.
}
assert (
F_glob:
forall b1 b2 id,
f b1 =
BCglob id ->
f b2 =
BCglob id ->
b1 =
b2).
{
assert (
forall b id,
f b =
BCglob id ->
callee b =
BCglob id).
{
unfold f;
intros.
destruct (
eq_block b sp).
congruence.
auto. }
intros.
eapply (
bc_glob callee);
eauto.
}
set (
bc :=
BC f F_stack F_glob).
unfold f in bc.
assert (
INCR:
bc_incr caller bc).
{
red;
simpl;
intros.
destruct (
eq_block b sp).
congruence.
symmetry;
apply SAME;
auto.
}
assert (
PM:
forall ex p,
epmatch callee ex p ->
epmatch bc ex Ptop).
{
intros.
assert (
epmatch callee ex Ptop)
by (
eapply epmatch_top';
eauto).
inv H0.
constructor;
simpl.
eapply depends_on_blocks_le ;
eauto.
simpl.
intros.
destruct (
eq_block b sp);
congruence.
}
assert (
VM:
forall v x,
evmatch callee v x ->
evmatch bc v Vtop).
{
intros.
assert (
evmatch callee v0 Vtop)
by (
eapply evmatch_top;
eauto).
inv H0;
constructor;
eauto.
}
assert (
SM:
forall b p,
smatch callee m b p ->
smatch bc m b Ptop).
{
intros.
destruct H;
split;
intros.
reflexivity.
exploit SMLD ;
eauto.
destruct mv ;
simpl.
eapply PM ;
eauto.
}
exists bc;
splitall.
-
eapply VM;
eauto.
-
eapply ematch_incr;
eauto.
-
apply romatch_exten with callee;
auto.
intros;
simpl.
destruct (
eq_block b sp);
intuition.
-
constructor;
simpl;
intros.
+
apply ablock_init_sound.
destruct (
eq_block b sp).
subst b.
eapply SM.
eapply mmatch_nonstack;
eauto.
congruence.
elim (
NOSTACK b);
auto.
+
rewrite PTree.gempty in H0;
discriminate.
+
destruct (
eq_block b sp).
congruence.
eapply SM;
auto.
eapply mmatch_nonstack;
eauto.
+
eapply SM.
eapply mmatch_top;
eauto.
destruct (
eq_block b sp);
congruence.
+
red;
simpl;
intros.
destruct (
eq_block b sp).
subst b.
eapply mmatch_below;
eauto.
congruence.
eapply mmatch_below;
eauto.
-
eapply genv_match_exten with caller;
eauto.
simpl;
intros.
destruct (
eq_block b sp).
intuition congruence.
split;
intros.
rewrite SAME in H by eauto with va.
auto.
apply <- (
proj1 GE2)
in H.
apply (
proj1 GE1)
in H.
auto.
simpl;
intros.
destruct (
eq_block b sp).
congruence.
rewrite <-
SAME;
eauto with va.
-
simpl.
apply dec_eq_true.
-
simpl;
intros.
destruct (
eq_block b sp).
congruence.
symmetry.
apply SAME;
auto.
eapply Plt_trans.
eauto.
apply BELOW.
congruence.
Qed.
Construction 5: restore the stack after a private call
Theorem return_from_private_call:
forall (
caller callee:
block_classification)
bound sp ge e ae v m rm am
,
bc_below caller bound ->
callee sp =
BCinvalid ->
caller sp =
BCstack ->
(
forall b,
Plt b bound ->
b <>
sp ->
caller b =
callee b) ->
genv_match caller ge ->
ematch caller e ae ->
bmatch caller m sp am.(
am_stack) ->
Ple bound (
Mem.nextblock m) ->
evmatch callee v Vtop ->
romatch callee m rm ->
mmatch callee m mtop ->
genv_match callee ge ->
bc_nostack callee ->
exists bc,
evmatch bc v (
Ptr Nonstack)
/\
ematch bc e ae
/\
romatch bc m rm
/\
mmatch bc m (
mafter_private_call am)
/\
genv_match bc ge
/\
bc sp =
BCstack
/\ (
forall b,
Plt b sp ->
bc b =
caller b).
Proof.
Construction 6: external call
Lemma eventval_match_dep:
forall (
ge:
genv)
bc
(
ME:
genv_match bc ge)
t ev v chunk
(
EVM :
eventval_match ge ev t v),
depends_on_blocks (
fun b0 :
block =>
bc b0 <>
BCinvalid)
(
Values_symbolic.Val.load_result chunk (
Values_symbolictype.Eval v)).
Proof.
intros.
inv EVM; try now (des chunk; destr).
red; intros.
destruct ME as [ME ME']. rewrite ME in FS.
trim (H b). congruence.
des chunk; destr; rewrite H; auto.
Qed.
Theorem external_call_match:
forall ef (
ge:
genv)
vargs m t vres m'
bc rm am,
external_call ef ge vargs m t vres m' ->
genv_match bc ge ->
(
forall v,
In v vargs ->
evmatch bc v Vtop) ->
romatch bc m rm ->
mmatch bc m am ->
bc_nostack bc ->
exists bc',
bc_incr bc bc'
/\ (
forall b,
Plt b (
Mem.nextblock m) ->
bc'
b =
bc b)
/\
evmatch bc'
vres Vtop
/\
genv_match bc'
ge
/\
romatch bc'
m'
rm
/\
mmatch bc'
m'
mtop
/\
bc_nostack bc'
/\ (
forall b ofs n,
Mem.valid_block m b ->
bc b =
BCinvalid ->
Mem.loadbytes m'
b ofs n =
Mem.loadbytes m b ofs n).
Proof.
intros until am;
intros EC GENV ARGS RO MM NOSTACK.
generalize (
ec_dep (
external_call_spec ef)
ge t vres m'
EC).
intro DEP.
specialize (
DEP (
fun b =>
match bc b with BCinvalid =>
true |
_ =>
false end)).
trim DEP.
{
intros.
erewrite bc_below_invalid;
eauto.
eapply mmatch_below;
eauto.
}
trim DEP.
{
intros.
des GENV.
rewrite i in H.
destr.
}
trim DEP.
{
apply Forall_forall.
intros x IN;
apply ARGS in IN.
inv IN.
inv H1.
red.
eapply depends_on_blocks_le;
eauto.
simpl.
intros;
destr.
}
assert (
SMTOP1:
forall b,
match bc b with BCinvalid =>
true |
_ =>
false end =
false ->
smatch bc m b Ptop).
{
intros.
des MM.
split.
constructor.
intros.
des mv.
eapply epmatch_top_def.
destruct (
mmatch_top b).
des (
bc b).
specialize (
SMLD _ _ _ H0 H1 _ H2).
simpl in SMLD.
eauto.
}
trim DEP.
{
intros.
red;
intros.
specialize (
SMTOP1 _ NS).
des SMTOP1.
rewrite Forall_forall.
intros.
specialize (
SMLD _ _ _ POS LB _ H).
des x.
inv SMLD.
red.
eapply depends_on_blocks_le;
eauto.
simpl;
intros.
destr.
}
destruct DEP as (
unreachable &
INCR &
SAME &
NODEP &
DEP_valid &
ReachSpec).
set (
f :=
fun b =>
if plt b (
Mem.nextblock m)
then bc b
else if unreachable b
then BCinvalid else BCother).
assert (
F_stack:
forall b1 b2,
f b1 =
BCstack ->
f b2 =
BCstack ->
b1 =
b2).
{
assert (
forall b,
f b =
BCstack ->
bc b =
BCstack).
{
unfold f;
intros.
destruct (
plt b (
Mem.nextblock m));
auto.
destr_in H. }
intros.
apply (
bc_stack bc);
auto.
}
assert (
F_glob:
forall b1 b2 id,
f b1 =
BCglob id ->
f b2 =
BCglob id ->
b1 =
b2).
{
assert (
forall b id,
f b =
BCglob id ->
bc b =
BCglob id).
{
unfold f;
intros.
destruct (
plt b (
Mem.nextblock m));
auto.
destr_in H. }
intros.
eapply (
bc_glob bc);
eauto.
}
set (
bc' :=
BC f F_stack F_glob).
unfold f in bc'.
assert (
INCR':
bc_incr bc bc').
{
red;
simpl;
intros.
apply pred_dec_true.
eapply mmatch_below;
eauto.
}
assert (
BELOW:
forall b,
Plt b (
Mem.nextblock m) ->
bc'
b =
bc b).
{
simpl;
intros;
apply pred_dec_true;
auto.
}
assert (
SMTOP:
forall b,
unreachable b =
false ->
smatch bc'
m'
b Ptop).
{
intros;
split;
intros.
-
constructor.
-
generalize (
NODEP _ H _ _ _ H0 H1);
intro.
rewrite Forall_forall in H3;
apply H3 in H2.
des mv.
constructor.
eapply depends_on_blocks_le. 2:
eauto.
simpl.
intros.
Require Import Tactics.
destr.
apply ReachSpec in H4.
des H4.
destr_in e0.
xomega.
rewrite H4.
destr.
}
exists bc';
repSplit;
auto.
-
constructor.
constructor.
red in DEP_valid.
eapply depends_on_blocks_le. 2:
eauto.
simpl.
intros.
destr.
apply ReachSpec in H.
des H.
destr_in e.
xomega.
rewrite H.
destr.
-
apply genv_match_exten with bc;
auto.
simpl;
intros;
split;
intros.
rewrite pred_dec_true by (
eapply mmatch_below;
eauto with va).
auto.
destruct (
plt b (
Mem.nextblock m)).
auto.
destr_in H.
simpl;
intros.
rewrite pred_dec_true by (
eapply mmatch_below;
eauto with va).
auto.
-
red;
simpl;
intros.
destruct (
plt b (
Mem.nextblock m)).
+
exploit RO;
eauto.
intros (
R &
P &
Q).
split;
auto.
split.
*
apply bmatch_incr with bc;
auto.
apply bmatch_inv with m;
auto.
intros.
eapply Mem.loadbytes_unchanged_on_1.
eapply external_call_readonly;
eauto.
auto.
intros;
red.
apply Q.
*
intros;
red;
intros;
elim (
Q ofs).
eapply external_call_max_perm with (
m2 :=
m');
eauto.
+
destr_in H.
-
constructor;
simpl;
intros.
+
repeat destr_in H.
+
rewrite PTree.gempty in H0;
discriminate.
+
apply SMTOP;
auto.
des (
unreachable b).
rename Heqb0 into UR.
generalize UR;
intro.
apply INCR in UR.
destr_in H0.
destr_in UR.
+
apply SMTOP;
auto.
des (
unreachable b).
rename Heqb0 into UR.
generalize UR;
intro.
apply INCR in UR.
destr_in H.
destr_in UR.
+
red;
simpl;
intros.
destruct (
plt b (
Mem.nextblock m)).
eapply Plt_le_trans.
eauto.
eapply external_call_nextblock;
eauto.
destr_in H.
eapply ReachSpec in Heqb0.
des Heqb0.
replace (
bc b)
with BCinvalid in e.
destr.
symmetry;
eapply bc_below_invalid;
eauto.
eapply mmatch_below;
eauto.
-
red;
intros.
unfold bc'.
simpl.
destr.
destr.
-
intros.
rewrite SAME;
auto.
rewrite H0;
auto.
Qed.
Semantic invariant
Section SOUNDNESS.
Variable prog:
program.
Let ge :
genv :=
Genv.globalenv prog.
Let rm :=
romem_for_program prog.
Inductive sound_stack:
block_classification ->
list stackframe ->
mem ->
block ->
Prop :=
|
sound_stack_nil:
forall bc m bound,
sound_stack bc nil m bound
|
sound_stack_public_call:
forall (
bc:
block_classification)
res f sp pc e stk m bound bc'
bound'
ae
(
STK:
sound_stack bc'
stk m sp)
(
INCR:
Ple bound'
bound)
(
BELOW:
bc_below bc'
bound')
(
SP:
bc sp =
BCother)
(
SP':
bc'
sp =
BCstack)
(
SAME:
forall b,
Plt b bound' ->
b <>
sp ->
bc b =
bc'
b)
(
GE:
genv_match bc'
ge)
(
AN:
VA.ge (
analyze rm f)!!
pc (
VA.State (
AE.set res Vtop ae)
mafter_public_call))
(
EM:
ematch bc'
e ae),
sound_stack bc (
Stackframe res f sp pc e ::
stk)
m bound
|
sound_stack_private_call:
forall (
bc:
block_classification)
res f sp pc e stk m bound bc'
bound'
ae am
(
STK:
sound_stack bc'
stk m sp)
(
INCR:
Ple bound'
bound)
(
BELOW:
bc_below bc'
bound')
(
SP:
bc sp =
BCinvalid)
(
SP':
bc'
sp =
BCstack)
(
SAME:
forall b,
Plt b bound' ->
b <>
sp ->
bc b =
bc'
b)
(
GE:
genv_match bc'
ge)
(
AN:
VA.ge (
analyze rm f)!!
pc (
VA.State (
AE.set res (
Ptr Nonstack)
ae) (
mafter_private_call am)))
(
EM:
ematch bc'
e ae)
(
CONTENTS:
bmatch bc'
m sp am.(
am_stack)),
sound_stack bc (
Stackframe res f sp pc e ::
stk)
m bound.
Inductive sound_state:
state ->
Prop :=
|
sound_regular_state:
forall s f sp pc e m ae am bc
(
STK:
sound_stack bc s m sp)
(
AN: (
analyze rm f)!!
pc =
VA.State ae am)
(
EM:
ematch bc e ae)
(
RO:
romatch bc m rm)
(
MM:
mmatch bc m am)
(
GE:
genv_match bc ge)
(
SP:
bc sp =
BCstack),
sound_state (
State s f sp pc e m)
|
sound_call_state:
forall s fd args m bc
(
STK:
sound_stack bc s m (
Mem.nextblock m))
(
ARGS:
forall v,
In v args ->
evmatch bc v Vtop)
(
RO:
romatch bc m rm)
(
MM:
mmatch bc m mtop)
(
GE:
genv_match bc ge)
(
NOSTK:
bc_nostack bc),
sound_state (
Callstate s fd args m)
|
sound_return_state:
forall s v m bc
(
STK:
sound_stack bc s m (
Mem.nextblock m))
(
RES:
evmatch bc v Vtop)
(
RO:
romatch bc m rm)
(
MM:
mmatch bc m mtop)
(
GE:
genv_match bc ge)
(
NOSTK:
bc_nostack bc),
sound_state (
Returnstate s v m).
Properties of the sound_stack invariant on call stacks.
Lemma sound_stack_ext:
forall m' (
bc:
block_classification)
stk m bound
,
sound_stack bc stk m bound ->
(
forall b ofs n bytes,
Plt b bound ->
bc b =
BCinvalid ->
n >= 0 ->
Mem.loadbytes m'
b ofs n =
Some bytes ->
Mem.loadbytes m b ofs n =
Some bytes) ->
sound_stack bc stk m'
bound.
Proof.
intros until 0.
induction 1;
intros INV.
-
constructor.
-
assert (
Plt sp bound')
by eauto with va.
subst.
eapply sound_stack_public_call;
eauto.
apply IHsound_stack;
intros;
auto.
apply INV.
xomega.
rewrite SAME;
auto.
xomega.
auto.
auto.
-
assert (
Plt sp bound')
by eauto with va.
eapply sound_stack_private_call;
eauto.
apply IHsound_stack;
intros;
auto.
apply INV.
xomega.
rewrite SAME;
auto.
xomega.
auto.
auto.
apply bmatch_ext with m;
auto.
intros.
apply INV.
xomega.
auto.
auto.
auto.
Qed.
Lemma sound_stack_inv:
forall m'
bc stk m bound,
sound_stack bc stk m bound ->
(
forall b ofs n,
Plt b bound ->
bc b =
BCinvalid ->
n >= 0 ->
Mem.loadbytes m'
b ofs n =
Mem.loadbytes m b ofs n) ->
sound_stack bc stk m'
bound.
Proof.
Lemma sound_stack_storev:
forall chunk m addr v m'
bc aaddr stk bound
,
Mem.storev chunk m addr v =
Some m' ->
evmatch bc addr aaddr ->
sound_stack bc stk m bound ->
sound_stack bc stk m'
bound.
Proof.
Lemma sound_stack_storebytes:
forall m b ofs bytes m'
bc aaddr stk bound dst,
Mem.mem_norm m dst =
Vptr b ofs ->
Mem.storebytes m b (
Int.unsigned ofs)
bytes =
Some m' ->
pmatch bc b ofs aaddr ->
sound_stack bc stk m bound ->
sound_stack bc stk m'
bound.
Proof.
Import NormaliseSpec.
Lemma sound_stack_free:
forall m b lo hi m'
bc stk bound,
Mem.free m b lo hi =
Some m' ->
sound_stack bc stk m bound ->
sound_stack bc stk m'
bound.
Proof.
Lemma loadbytes_free_list_2:
forall l (
m1 m2 :
mem),
MemReserve.release_boxes m1 l =
Some m2 ->
forall (
b :
block) (
ofs n :
Z) (
bytes :
list memval),
Mem.loadbytes m2 b ofs n =
Some bytes ->
Mem.loadbytes m1 b ofs n =
Some bytes.
Proof.
Lemma sound_stack_free_list:
forall m l m'
bc stk bound,
MemReserve.release_boxes m l =
Some m' ->
sound_stack bc stk m bound ->
sound_stack bc stk m'
bound.
Proof.
Lemma sound_stack_new_bound:
forall bc stk m bound bound',
sound_stack bc stk m bound ->
Ple bound bound' ->
sound_stack bc stk m bound'.
Proof.
Lemma sound_stack_exten:
forall bc stk m bound (
bc1:
block_classification),
sound_stack bc stk m bound ->
(
forall b,
Plt b bound ->
bc1 b =
bc b) ->
sound_stack bc1 stk m bound.
Proof.
intros.
inv H.
-
constructor.
-
assert (
Plt sp bound')
by eauto with va.
eapply sound_stack_public_call;
eauto.
rewrite H0;
auto.
xomega.
intros.
rewrite H0;
auto.
xomega.
-
assert (
Plt sp bound')
by eauto with va.
eapply sound_stack_private_call;
eauto.
rewrite H0;
auto.
xomega.
intros.
rewrite H0;
auto.
xomega.
Qed.
Preservation of the semantic invariant by one step of execution
Lemma sound_succ_state:
forall bc pc ae am instr ae'
am'
s f sp pc'
e'
m',
(
analyze rm f)!!
pc =
VA.State ae am ->
f.(
fn_code)!
pc =
Some instr ->
In pc' (
successors_instr instr) ->
transfer f rm pc ae am =
VA.State ae'
am' ->
ematch bc e'
ae' ->
mmatch bc m'
am' ->
romatch bc m'
rm ->
genv_match bc ge ->
bc sp =
BCstack ->
sound_stack bc s m'
sp ->
sound_state (
State s f sp pc'
e'
m').
Proof.
intros.
exploit analyze_succ;
eauto.
intros (
ae'' &
am'' &
AN &
EM &
MM).
econstructor;
eauto.
Qed.
Lemma areg_sound:
forall bc e ae r,
ematch bc e ae ->
evmatch bc (
e#
r) (
areg ae r).
Proof.
intros. apply H.
Qed.
Lemma aregs_sound:
forall bc e ae rl,
ematch bc e ae ->
list_forall2 (
evmatch bc) (
e##
rl) (
aregs ae rl).
Proof.
induction rl;
simpl;
intros.
constructor.
constructor;
auto.
apply areg_sound;
auto.
Qed.
Hint Resolve areg_sound aregs_sound:
va.
Lemma epge_evge :
forall v,
epge Nonstack (
provenance v) ->
evge (
Ptr Nonstack)
v.
Proof.
intros.
unfold provenance in H.
simpl in H.
destruct v ;
simpl in H ;
try constructor ;
simpl;
auto.
destruct p ;
simpl in * ;
auto.
destruct p ;
simpl in * ;
auto.
destruct p ;
simpl in * ;
auto.
Qed.
Lemma romatch_free_list:
forall l bc m m'
rm,
MemReserve.release_boxes m l =
Some m' ->
romatch bc m rm ->
romatch bc m'
rm.
Proof.
Lemma mmatch_free_list :
forall l (
bc :
block_classification) (
m :
mem)
(
m' :
mem) (
am :
amem),
MemReserve.release_boxes m l =
Some m' ->
mmatch bc m am ->
mmatch bc m'
am.
Proof.
Lemma match_aptr_of_aval :
forall bc dst adst m bdst odst,
evmatch bc dst adst->
Mem.mem_norm m dst =
Vptr bdst odst ->
pmatch bc bdst odst (
aptr_of_aval adst).
Proof.
Theorem sound_step:
forall st sz t st',
RTL.step ge sz st t st' ->
sound_state st ->
sound_state st'.
Proof.
End SOUNDNESS.
Soundness of the initial memory abstraction
Section INITIAL.
Variable prog:
program.
Let ge :=
Genv.globalenv prog.
Lemma initial_block_classification:
forall m fid sz,
Genv.init_mem fid sz prog =
Some m ->
exists bc,
genv_match bc ge
/\
bc_below bc (
Mem.nextblock m)
/\
bc_nostack bc
/\ (
forall b id,
bc b =
BCglob id ->
Genv.find_symbol ge id =
Some b)
/\ (
forall b,
Mem.valid_block m b ->
bc b <>
BCinvalid).
Proof.
Section INIT.
Variable bc:
block_classification.
Hypothesis GMATCH:
genv_match bc ge.
Lemma store_init_data_summary:
forall ab p id,
is_romem (
ab_summary ab) ->
is_romem (
ab_summary (
store_init_data ab p id)).
Proof.
Lemma store_init_data_is_romem_block:
forall ab p id,
is_romem_block ab ->
is_romem_block (
store_init_data ab p id).
Proof.
Lemma store_init_data_list_summary:
forall idl ab p,
is_romem_block ab ->
is_romem_block (
store_init_data_list ab p idl).
Proof.
Lemma store_init_data_sound:
forall m b p id m'
ab,
Genv.store_init_data ge m b p id =
Some m' ->
bmatch bc m b ab ->
bmatch bc m'
b (
store_init_data ab p id).
Proof.
intros.
destruct id;
try (
eapply ablock_store_sound;
eauto;
repeat constructor;
fail).
simpl in H.
inv H.
auto.
simpl in H.
destruct (
Genv.find_symbol ge i)
as [
b'|]
eqn:
FS;
try discriminate.
eapply ablock_store_sound;
eauto.
constructor.
econstructor.
apply GMATCH;
eauto.
repeat intro ;
reflexivity.
Qed.
Lemma store_init_data_list_sound:
forall idl m b p m'
ab,
Genv.store_init_data_list ge m b p idl =
Some m' ->
bmatch bc m b ab ->
bmatch bc m'
b (
store_init_data_list ab p idl).
Proof.
Lemma store_init_data_other:
forall m b p id m'
ab b',
Genv.store_init_data ge m b p id =
Some m' ->
b' <>
b ->
bmatch bc m b'
ab ->
bmatch bc m'
b'
ab.
Proof.
Lemma store_init_data_list_other:
forall b b'
ab idl m p m',
Genv.store_init_data_list ge m b p idl =
Some m' ->
b' <>
b ->
bmatch bc m b'
ab ->
bmatch bc m'
b'
ab.
Proof.
Lemma store_zeros_same:
forall p m b pos n m',
store_zeros m b pos n =
Some m' ->
smatch bc m b p ->
smatch bc m'
b p.
Proof.
intros until n.
functional induction (
store_zeros m b pos n);
intros.
-
inv H.
auto.
-
eapply IHo;
eauto.
replace p with (
evplub (
I Int.zero)
p).
eapply smatch_store;
eauto.
simpl ;
auto.
constructor.
repeat intro ;
reflexivity.
inv H0.
destruct p ;
simpl in * ;
tauto.
-
discriminate.
Qed.
Lemma store_zeros_other:
forall b'
ab m b p n m',
store_zeros m b p n =
Some m' ->
b' <>
b ->
bmatch bc m b'
ab ->
bmatch bc m'
b'
ab.
Proof.
Definition initial_mem_match (
bc:
block_classification) (
m:
mem) (
g:
genv) :=
forall b v,
Genv.find_var_info g b =
Some v ->
v.(
gvar_volatile) =
false ->
v.(
gvar_readonly) =
true ->
bmatch bc m b (
store_init_data_list (
ablock_init Pcst) 0
v.(
gvar_init)).
Lemma alloc_global_match:
forall m g idg m'
fsz fid,
Genv.genv_next g =
Mem.nextblock m ->
initial_mem_match bc m g ->
Genv.alloc_global fid fsz ge m idg =
Some m' ->
initial_mem_match bc m' (
Genv.add_global g idg).
Proof.
Lemma alloc_globals_match:
forall gl m g m'
fsz ,
Genv.genv_next g =
Mem.nextblock m ->
initial_mem_match bc m g ->
Genv.alloc_globals fid fsz ge m gl =
Some m' ->
initial_mem_match bc m' (
Genv.add_globals g gl).
Proof.
Definition romem_consistent (
g:
genv) (
rm:
romem) :=
forall id b ab,
Genv.find_symbol g id =
Some b ->
rm!
id =
Some ab ->
exists v,
Genv.find_var_info g b =
Some v
/\
v.(
gvar_readonly) =
true
/\
v.(
gvar_volatile) =
false
/\
ab =
store_init_data_list (
ablock_init Pcst) 0
v.(
gvar_init).
Lemma alloc_global_consistent:
forall g rm idg,
romem_consistent g rm ->
romem_consistent (
Genv.add_global g idg) (
alloc_global rm idg).
Proof.
Lemma alloc_globals_consistent:
forall gl g rm,
romem_consistent g rm ->
romem_consistent (
Genv.add_globals g gl) (
List.fold_left alloc_global gl rm).
Proof.
End INIT.
Theorem initial_mem_matches:
forall fsz m (
Fsz_spec:
forall i,
fsz i > 0),
Genv.init_mem RTL.fid fsz prog =
Some m ->
exists bc,
genv_match bc ge
/\
bc_below bc (
Mem.nextblock m)
/\
bc_nostack bc
/\
romatch bc m (
romem_for_program prog)
/\ (
forall b,
Mem.valid_block m b ->
bc b <>
BCinvalid).
Proof.
End INITIAL.
Lemma genv_store_init_data_smatch_top :
forall (
ge:
Genv.t fundef unit)
bc m m'
b p a
(
MENV :
genv_match bc ge)
(
SI :
Genv.store_init_data ge m b p a =
Some m')
(
SMATCH :
forall b :
positive,
Plt b (
Mem.nextblock m) ->
smatch bc m b Ptop),
forall b :
positive,
Plt b (
Mem.nextblock m') ->
smatch bc m'
b Ptop.
Proof.
intros.
assert (
NEXT :
Mem.nextblock m' =
Mem.nextblock m).
{
unfold Genv.store_init_data in SI.
destruct a;
try (
eapply Mem.nextblock_store ;
eauto;
fail).
congruence.
destruct (
Genv.find_symbol ge i) ;
try congruence.
eapply Mem.nextblock_store ;
eauto;
fail.
}
rewrite NEXT in H.
apply SMATCH in H.
clear NEXT.
destruct a ;
simpl in SI.
-
apply smatch_store with (2:=
H) (
av:=
Pcst)
in SI;
simpl ;
auto.
repeat constructor ;
repeat intro ;
reflexivity.
-
apply smatch_store with (2:=
H) (
av:=
Pcst)
in SI;
simpl ;
auto.
repeat constructor ;
repeat intro ;
reflexivity.
-
apply smatch_store with (2:=
H) (
av:=
Pcst)
in SI;
simpl ;
auto.
repeat constructor ;
repeat intro ;
reflexivity.
-
apply smatch_store with (2:=
H) (
av:=
Pcst)
in SI;
simpl ;
auto.
repeat constructor ;
repeat intro ;
reflexivity.
-
apply smatch_store with (2:=
H) (
av:=
Pcst)
in SI;
simpl ;
auto.
repeat constructor ;
repeat intro ;
reflexivity.
-
apply smatch_store with (2:=
H) (
av:=
Pcst)
in SI;
simpl ;
auto.
repeat constructor ;
repeat intro ;
reflexivity.
-
inv SI ;
congruence.
-
destruct (
Genv.find_symbol ge i)
eqn:
SYMB ;
try congruence.
apply smatch_store with (2:=
H) (
av:=
Glob)
in SI;
simpl ;
auto.
apply epmatch_ge with (
q:=
Gl i i0).
simpl ;
auto.
destruct MENV.
rewrite H0 in SYMB.
econstructor;
eauto.
repeat intro ;
reflexivity.
Qed.
Lemma genv_store_init_data_list_smatch_top :
forall (
ge:
Genv.t fundef unit)
bc idl m m'
b p
(
ENV :
genv_match bc ge)
(
SIDL :
Genv.store_init_data_list ge m b p idl =
Some m')
(
SMATCH :
forall b :
positive,
Plt b (
Mem.nextblock m) ->
smatch bc m b Ptop),
forall b :
positive,
Plt b (
Mem.nextblock m') ->
smatch bc m'
b Ptop.
Proof.
Lemma alloc_smatch_top :
forall bc m j m'
b'
(
ALLOC :
Mem.alloc m 0
j Normal =
Some (
m',
b'))
(
SMATCH :
forall b :
positive,
Plt b (
Mem.nextblock m) ->
smatch bc m b Ptop),
forall b,
Plt b (
Mem.nextblock m') ->
smatch bc m'
b Ptop.
Proof.
Lemma drop_perm_loadbytes :
forall m b sz p m'
n ofs b'
l
(
ALLOCG :
Mem.drop_perm m b 0
sz p =
Some m')
(
LOAD :
Mem.loadbytes m'
b'
ofs n =
Some l),
Mem.loadbytes m b'
ofs n =
Some l.
Proof.
Lemma low_alloc_smatch_top :
forall bc m j m'
b'
al
(
ALLOC :
Mem.low_alloc m 0
j al Normal =
Some (
m',
b'))
(
SMATCH :
forall b :
positive,
Plt b (
Mem.nextblock m) ->
smatch bc m b Ptop),
forall b,
Plt b (
Mem.nextblock m') ->
smatch bc m'
b Ptop.
Proof.
Lemma alloc_global_smatch_top :
forall (
ge:
Genv.t fundef unit)
bc m idg m'
fsz
(
MENV :
genv_match bc ge)
(
ALLOCG :
Genv.alloc_global fid fsz ge m idg =
Some m')
(
SMATCH :
forall b,
Plt b (
Mem.nextblock m) ->
smatch bc m b Ptop),
(
forall b',
Plt b' (
Mem.nextblock m') ->
smatch bc m'
b'
Ptop).
Proof.
Lemma alloc_globals_smatch_top :
forall (
ge:
Genv.t fundef unit)
bc idg m m'
fsz
(
MENV :
genv_match bc ge)
(
ALLOCG :
Genv.alloc_globals fid fsz ge m idg =
Some m')
(
SMATCH :
forall b',
Plt b' (
Mem.nextblock m) ->
smatch bc m b'
Ptop),
(
forall b',
Plt b' (
Mem.nextblock m') ->
smatch bc m'
b'
Ptop).
Proof.
Lemma mmatch_init_top :
forall m prog fsz bc
(
INIT :
Genv.init_mem fid fsz prog =
Some m)
(
GE :
genv_match bc (
Genv.globalenv prog))
(
BELOW :
bc_below bc (
Mem.nextblock m))
(
NOSTACK :
bc_nostack bc)
(
RM :
romatch bc m (
romem_for_program prog))
(
VALID :
forall b :
block,
Mem.valid_block m b ->
bc b <>
BCinvalid),
mmatch bc m mtop.
Proof.
Theorem sound_initial:
forall prog fsz (
Fszspec:
forall i,
fsz i > 0)
st,
initial_state prog fsz st ->
sound_state prog st.
Proof.
Hint Resolve areg_sound aregs_sound:
va.
Interface with other optimizations
Definition avalue (
a:
VA.t) (
r:
reg) :
aval :=
match a with
|
VA.Bot =>
Vbot
|
VA.State ae am =>
AE.get r ae
end.
Lemma avalue_sound:
forall prog s f sp pc e m r,
sound_state prog (
State s f sp pc e m) ->
exists bc,
evmatch bc e#
r (
avalue (
analyze (
romem_for_program prog)
f)!!
pc r)
/\
genv_match bc (
Genv.globalenv prog)
/\
bc sp =
BCstack.
Proof.
intros. inv H. exists bc; split; auto. rewrite AN. apply EM.
Qed.
Definition aaddr (
a:
VA.t) (
r:
reg) :
aptr :=
match a with
|
VA.Bot =>
Pbot
|
VA.State ae am =>
aptr_of_aval (
AE.get r ae)
end.
Definition aaddressing (
a:
VA.t) (
addr:
addressing) (
args:
list reg) :
aptr :=
match a with
|
VA.Bot =>
Pbot
|
VA.State ae am =>
aptr_of_aval (
eval_static_addressing addr (
aregs ae args))
end.