Require Import FunInd.
Require Import Coqlib Maps Integers Floats Lattice Kildall.
Require Import Compopts AST Linking.
Require Import Values Memory Globalenvs Events.
Require Import Registers Op RTL.
Require Import ValueDomain ValueAOp Liveness.
Require Unreach.
Require Import sflib.
Coercion Unreach.unreach:
Unreach.t >->
Funclass.
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.
Analysis of function calls. We treat specially the case where
neither the arguments nor the global variables point within the
stack frame of the current function. In this case, no pointer
within the stack frame escapes during the call.
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 :=
plub (
ab_summary (
am_stack am_before))
Nonstack |}.
Definition analyze_call (
am:
amem) (
aargs:
list aval) :=
if pincl am.(
am_nonstack)
Nonstack
&&
forallb (
fun av =>
vpincl av Nonstack)
aargs
then (
Ifptr Nonstack,
mafter_private_call am)
else (
Vtop,
mafter_public_call).
Definition transfer_call (
ae:
aenv) (
am:
amem) (
args:
list reg) (
res:
reg) :=
let (
av,
am') :=
analyze_call am (
aregs ae args)
in
VA.State (
AE.set res av ae)
am'.
Analysis of builtins.
Fixpoint abuiltin_arg (
ae:
aenv) (
am:
amem) (
rm:
romem) (
ba:
builtin_arg reg) :
aval :=
match ba with
|
BA r =>
areg ae r
|
BA_int n =>
I n
|
BA_long n =>
L n
|
BA_float n =>
F n
|
BA_single n =>
FS n
|
BA_loadstack chunk ofs =>
loadv chunk rm am (
Ptr (
Stk ofs))
|
BA_addrstack ofs =>
Ptr (
Stk ofs)
|
BA_loadglobal chunk id ofs =>
loadv chunk rm am (
Ptr (
Gl id ofs))
|
BA_addrglobal id ofs =>
Ptr (
Gl id ofs)
|
BA_splitlong hi lo =>
longofwords (
abuiltin_arg ae am rm hi) (
abuiltin_arg ae am rm lo)
|
BA_addptr ba1 ba2 =>
let v1 :=
abuiltin_arg ae am rm ba1 in
let v2 :=
abuiltin_arg ae am rm ba2 in
if Archi.ptr64 then addl v1 v2 else add v1 v2
end.
Definition set_builtin_res (
br:
builtin_res reg) (
av:
aval) (
ae:
aenv) :
aenv :=
match br with
|
BR r =>
AE.set r av ae
|
_ =>
ae
end.
Definition transfer_builtin_default
(
ae:
aenv) (
am:
amem) (
rm:
romem)
(
args:
list (
builtin_arg reg)) (
res:
builtin_res reg) :=
let (
av,
am') :=
analyze_call am (
map (
abuiltin_arg ae am rm)
args)
in
VA.State (
set_builtin_res res av ae)
am'.
Definition transfer_builtin
(
ae:
aenv) (
am:
amem) (
rm:
romem) (
ef:
external_function)
(
args:
list (
builtin_arg reg)) (
res:
builtin_res reg) :=
match ef,
args with
|
EF_vload chunk,
addr ::
nil =>
let aaddr :=
abuiltin_arg ae am rm addr in
let a :=
if va_strict tt
then vlub (
loadv chunk rm am aaddr) (
vnormalize chunk (
Ifptr Glob))
else vnormalize chunk Vtop in
VA.State (
set_builtin_res res a ae)
am
|
EF_vstore chunk,
addr ::
v ::
nil =>
let aaddr :=
abuiltin_arg ae am rm addr in
let av :=
abuiltin_arg ae am rm v in
let am' :=
storev chunk am aaddr av in
VA.State (
set_builtin_res res ntop ae) (
mlub am am')
|
EF_memcpy sz al,
dst ::
src ::
nil =>
let adst :=
abuiltin_arg ae am rm dst in
let asrc :=
abuiltin_arg ae am rm src in
let p :=
loadbytes am rm (
aptr_of_aval asrc)
in
let am' :=
storebytes am (
aptr_of_aval adst)
sz p in
VA.State (
set_builtin_res res ntop ae)
am'
| (
EF_annot _ _ _ |
EF_debug _ _ _),
_ =>
VA.State (
set_builtin_res res ntop ae)
am
|
EF_annot_val _ _ _,
v ::
nil =>
let av :=
abuiltin_arg ae am rm v in
VA.State (
set_builtin_res res av ae)
am
|
_,
_ =>
transfer_builtin_default ae am rm args res
end.
The transfer function for one instruction. Given the abstract state
"before" the instruction, computes the abstract state "after".
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.
A wrapper on transfer that removes information associated with
dead registers, so as to reduce the sizes of abstract states.
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.
The forward dataflow analysis.
Module DS :=
Dataflow_Solver(
VA)(
NodeSetForward).
Definition mfunction_entry :=
{|
am_stack :=
ablock_init Pbot;
am_glob :=
PTree.empty _;
am_nonstack :=
Nonstack;
am_top :=
Nonstack |}.
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 =>
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
(
if propagate_float_constants tt then FS n else ntop)
|
Init_float64 n =>
ablock_store Mfloat64 ab p
(
if propagate_float_constants tt then F n else ntop)
|
Init_addrof symb ofs =>
ablock_store Mptr 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 +
init_data_size id)
idl'
end.
When CompCert is used in separate compilation mode, the
gvar_init
initializer attached to a readonly global variable may not correspond
to the actual initial value of this global. This occurs in two cases:
-
an extern const variable, which is represented by gvar_init = nil;
-
a const variable without an explicit initializer, which is treated
by the linker as a "common" symbol, and is represented by
gvar_init = Init_space sz :: nil.
In both cases, the variable can be defined and initialized in another
compilation unit which is later linked with the current compilation unit.
Definition definitive_initializer (
init:
list init_data) :
bool :=
match init with
|
nil =>
false
|
Init_space _ ::
nil =>
false
|
_ =>
true
end.
Definition alloc_global {
F V} (
rm:
romem) (
idg:
ident *
globdef F V):
romem :=
match idg with
| (
id,
Gfun f) =>
PTree.remove id rm
| (
id,
Gvar v) =>
if v.(
gvar_readonly) &&
negb v.(
gvar_volatile) &&
definitive_initializer v.(
gvar_init)
then PTree.set id (
store_init_data_list (
ablock_init Pbot) 0
v.(
gvar_init))
rm
else PTree.remove id rm
end.
Definition romem_for {
F V} (
p:
AST.program F V) :
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 ->
vmatch bc v (
Ifptr 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.
Analysis of registers and builtin arguments
Lemma areg_sound:
forall bc e ae r,
ematch bc e ae ->
vmatch 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 (
vmatch 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 abuiltin_arg_sound:
forall bc F V (
ge:
Genv.t F V)
rs sp m ae rm am,
ematch bc rs ae ->
romatch bc m rm ->
mmatch bc m am ->
genv_match bc ge ->
bc sp =
BCstack ->
forall a v,
eval_builtin_arg ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m a v ->
vmatch bc v (
abuiltin_arg ae am rm a).
Proof.
Lemma abuiltin_args_sound:
forall bc F V (
ge:
Genv.t F V)
rs sp m ae rm am,
ematch bc rs ae ->
romatch bc m rm ->
mmatch bc m am ->
genv_match bc ge ->
bc sp =
BCstack ->
forall al vl,
eval_builtin_args ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m al vl ->
list_forall2 (
vmatch bc)
vl (
map (
abuiltin_arg ae am rm)
al).
Proof.
intros until am;
intros EM RM MM GM SP.
induction 1;
simpl.
-
constructor.
-
constructor;
auto.
eapply abuiltin_arg_sound;
eauto.
Qed.
Lemma set_builtin_res_sound:
forall bc rs ae v av res,
ematch bc rs ae ->
vmatch bc v av ->
ematch bc (
regmap_setres res v rs) (
set_builtin_res res av ae).
Proof.
intros.
destruct res;
simpl;
auto.
apply ematch_update;
auto.
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 b ofs p,
pmatch bc b ofs p ->
pmatch bc b ofs Nonstack.
Proof.
intros. inv H; constructor; congruence.
Qed.
Lemma vmatch_no_stack:
forall v x,
vmatch bc v x ->
vmatch bc v (
Ifptr Nonstack).
Proof.
Lemma smatch_no_stack:
forall m b p,
smatch bc m b p ->
smatch bc m b Nonstack.
Proof.
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).
Definition bc2su (
bc:
block_classification) (
ge_nb:
block) (
nb:
block):
Unreach.t :=
Unreach.mk (
fun blk =>
if plt blk nb
then block_class_eq (
bc blk)
BCinvalid else false)
ge_nb nb.
Hint Extern 999 =>
congruence :
congruence.
Hint Extern 1000 =>
xomega :
xomega.
Lemma pos_le_lt_tight
x y
(
LE:
Ple x y)
(
LT:
Plt y (
Pos.succ x)):
x =
y.
Proof.
xomega. Qed.
Theorem allocate_stack:
forall m sz m'
sp bc F V (
ge:
Genv.t F V)
rm am,
Mem.alloc m 0
sz = (
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,
vmatch bc v x ->
vmatch bc'
v (
Ifptr Nonstack))
/\ (<<
HLE:
Unreach.hle (
bc2su bc ge.(
Genv.genv_next)
m.(
Mem.nextblock)) (
bc2su bc'
ge.(
Genv.genv_next)
m'.(
Mem.nextblock))>>).
Proof.
Construction 2: turn the stack into an "other" block, at public calls or function returns
Theorem anonymize_stack:
forall m sp bc F V (
ge:
Genv.t F V)
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,
vmatch bc v x ->
vmatch 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 F V (
ge:
Genv.t F V)
rm am,
genv_match bc ge ->
romatch bc m rm ->
mmatch bc m am ->
bc sp =
BCstack ->
pge Nonstack am.(
am_nonstack) ->
exists bc',
bc_nostack bc'
/\
bc'
sp =
BCinvalid
/\ (
forall b,
b <>
sp ->
bc'
b =
bc b)
/\ (
forall v x,
vge (
Ifptr Nonstack)
x ->
vmatch bc v x ->
vmatch 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 F V (
ge:
Genv.t F V)
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) ->
vmatch callee v Vtop ->
romatch callee m rm ->
mmatch callee m mtop ->
genv_match callee ge ->
bc_nostack callee ->
exists bc,
vmatch 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 (
Some id) ->
f b2 =
BCglob (
Some 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 b ofs p,
pmatch callee b ofs p ->
pmatch bc b ofs Ptop).
{
intros.
assert (
pmatch callee b ofs Ptop)
by (
eapply pmatch_top';
eauto).
inv H0.
constructor;
simpl.
destruct (
eq_block b sp);
congruence.
}
assert (
VM:
forall v x,
vmatch callee v x ->
vmatch bc v Vtop).
{
intros.
assert (
vmatch callee v0 Vtop)
by (
eapply vmatch_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.
eapply VM;
eauto.
eapply PM;
eauto.
}
assert(
GESAME:
forall b id,
caller b =
BCglob id <->
bc b =
BCglob id).
{
i.
s.
des_ifs;
try by intuition.
split;
i.
-
rewrite <-
SAME;
ss.
apply BELOW.
rewrite H;
ss.
-
assert(
caller b =
BCglob id).
{
clear -
GE1 GE2 H n.
rr in GE1.
rr in GE2.
des.
destruct id.
-
apply GE1.
apply GE2.
eauto.
-
exploit GE3;
eauto.
i.
exploit GE4;
eauto.
i;
des.
destruct id;
ss.
apply GE1 in H1.
apply GE2 in H1.
congruence.
}
rewrite SAME;
ss.
apply BELOW.
rewrite H0;
ss.
}
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).
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 F V (
ge:
Genv.t F V)
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) ->
vmatch callee v Vtop ->
romatch callee m rm ->
mmatch callee m mtop ->
genv_match callee ge ->
bc_nostack callee ->
exists bc,
vmatch bc v (
Ifptr 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
Theorem external_call_match:
forall ef F V (
se:
Senv.t) (
ge:
Genv.t F V) (
SEGE:
senv_genv_compat se ge)
vargs m t vres m'
bc rm am,
external_call ef se vargs m t vres m' ->
genv_match bc ge ->
(
forall v,
In v vargs ->
vmatch 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)
/\
vmatch 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)
/\ <<
MLE: (
bc2su bc ge.(
Genv.genv_next)
m'.(
Mem.nextblock)).(
Unreach.mle)
m m'>>.
Proof.
intros until am;
intros EC GENV ARGS RO MM NOSTACK.
exploit (@
external_call_mem_inject_gen ef se se vargs m t vres m' (
inj_of_bc bc)
m vargs).
{
exploit inj_of_bc_preserves_globals;
eauto.
intro GEINJ.
rr in GENV.
rr in GEINJ.
des.
rr.
unfold inj_of_bc.
inv SEGE.
esplits;
eauto;
i;
try by des_ifs.
esplits;
eauto.
des_ifs.
exploit (
GENV0 b1);
eauto. {
rewrite <-
NB.
eapply Senv.find_symbol_below;
eauto. }
i;
des.
congruence.
}
exact EC.
eapply mmatch_inj;
eauto.
eapply mmatch_below;
eauto.
revert ARGS.
generalize vargs.
induction vargs0;
simpl;
intros;
constructor.
eapply vmatch_inj;
eauto.
auto.
intros (
j' &
vres' &
m'' &
EC' &
IRES &
IMEM &
UNCH1 &
UNCH2 &
IINCR &
ISEP).
assert (
JBELOW:
forall b,
Plt b (
Mem.nextblock m) ->
j'
b =
inj_of_bc bc b).
{
intros.
destruct (
inj_of_bc bc b)
as [[
b'
delta] | ]
eqn:
EQ.
eapply IINCR;
eauto.
destruct (
j'
b)
as [[
b''
delta'] | ]
eqn:
EQ';
auto.
exploit ISEP;
eauto.
tauto.
}
set (
f :=
fun b =>
if plt b (
Mem.nextblock m)
then bc b
else match j'
b with None =>
BCinvalid |
Some _ =>
BCother end).
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.
destruct (
j'
b);
discriminate. }
intros.
apply (
bc_stack bc);
auto.
}
assert (
F_glob:
forall b1 b2 id,
f b1 =
BCglob (
Some id) ->
f b2 =
BCglob (
Some 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.
destruct (
j'
b);
discriminate. }
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 (
BC'
INV:
forall b,
bc'
b <>
BCinvalid ->
exists b'
delta,
j'
b =
Some(
b',
delta)).
{
simpl;
intros.
destruct (
plt b (
Mem.nextblock m)).
exists b, 0.
rewrite JBELOW by auto.
apply inj_of_bc_valid;
auto.
destruct (
j'
b)
as [[
b'
delta] | ].
exists b',
delta;
auto.
congruence.
}
assert (
PMTOP:
forall b b'
delta ofs,
j'
b =
Some (
b',
delta) ->
pmatch bc'
b ofs Ptop).
{
intros.
constructor.
simpl;
unfold f.
destruct (
plt b (
Mem.nextblock m)).
rewrite JBELOW in H by auto.
eapply inj_of_bc_inv;
eauto.
rewrite H;
congruence.
}
assert (
VMTOP:
forall v v',
Val.inject j'
v v' ->
vmatch bc'
v Vtop).
{
intros.
inv H;
constructor.
eapply PMTOP;
eauto.
}
assert (
SMTOP:
forall b,
bc'
b <>
BCinvalid ->
smatch bc'
m'
b Ptop).
{
intros;
split;
intros.
-
exploit BC'
INV;
eauto.
intros (
b' &
delta &
J').
exploit Mem.load_inject.
eexact IMEM.
eauto.
eauto.
intros (
v' &
A &
B).
eapply VMTOP;
eauto.
-
exploit BC'
INV;
eauto.
intros (
b'' &
delta &
J').
exploit Mem.loadbytes_inject.
eexact IMEM.
eauto.
eauto.
intros (
bytes &
A &
B).
inv B.
inv H3.
inv H7.
eapply PMTOP;
eauto.
}
exists bc';
splitall.
-
exact INCR.
-
simpl;
intros.
apply pred_dec_true;
auto.
-
eapply VMTOP;
eauto.
-
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.
destruct (
j'
b);
congruence.
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.
destruct (
j'
b);
congruence.
-
constructor;
simpl;
intros.
+
apply ablock_init_sound.
apply SMTOP.
simpl;
congruence.
+
rewrite PTree.gempty in H0;
discriminate.
+
apply SMTOP;
auto.
+
apply SMTOP;
auto.
+
red;
simpl;
intros.
destruct (
plt b (
Mem.nextblock m)).
eapply Pos.lt_le_trans.
eauto.
eapply external_call_nextblock;
eauto.
destruct (
j'
b)
as [[
bx deltax] | ]
eqn:
J'.
eapply Mem.valid_block_inject_1;
eauto.
congruence.
-
red;
simpl;
intros.
destruct (
plt b (
Mem.nextblock m)).
apply NOSTACK;
auto.
destruct (
j'
b);
congruence.
-
intros.
eapply Mem.loadbytes_unchanged_on_1;
auto.
apply UNCH1;
auto.
intros;
red.
unfold inj_of_bc;
rewrite H0;
auto.
-
econs;
eauto.
+
i.
eapply external_call_max_perm;
try apply EC;
eauto.
+
i.
eapply external_call_readonly;
eauto.
+
eapply Mem.unchanged_on_implies;
try apply UNCH1;
eauto.
unfold Basics.flip.
s.
ii.
rr in H.
rr.
unfold inj_of_bc.
unfold bc2su in *.
des_sumbool.
des_ifs.
Qed.
Semantic invariant
Section SOUNDNESS.
Variable prog:
program.
Variable se:
Senv.t.
Variable ge:
genv.
Hypothesis SEGE:
senv_genv_compat se ge.
Let rm :=
romem_for prog.
Inductive sound_stack (
su:
Unreach.t):
block_classification ->
list stackframe ->
mem ->
block ->
Prop :=
|
sound_stack_nil:
forall bc m bound (
SU:
Ple su.(
Unreach.nb)
bound),
sound_stack su 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 su 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)
(
LESU:
Ple sp bound'),
sound_stack su bc (
Stackframe res f (
Vptr sp Ptrofs.zero)
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 su 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 (
Ifptr Nonstack)
ae) (
mafter_private_call am)))
(
EM:
ematch bc'
e ae)
(
CONTENTS:
bmatch bc'
m sp am.(
am_stack))
(
LESU:
Ple sp bound'),
sound_stack su bc (
Stackframe res f (
Vptr sp Ptrofs.zero)
pc e ::
stk)
m bound.
Inductive sound_state_base (
su:
Unreach.t):
state ->
Prop :=
|
sound_regular_state:
forall s f sp pc e m ae am bc
(
STK:
sound_stack su 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)
(
HLE:
Unreach.hle su (
bc2su bc ge.(
Genv.genv_next)
m.(
Mem.nextblock)))
(
WF:
Unreach.wf su),
sound_state_base su (
State s f (
Vptr sp Ptrofs.zero)
pc e m)
|
sound_call_state:
forall s fptr sg args m bc
(
STK:
sound_stack su bc s m (
Mem.nextblock m))
(
ARGS:
forall v,
In v args ->
vmatch bc v Vtop)
(
RO:
romatch bc m rm)
(
MM:
mmatch bc m mtop)
(
GE:
genv_match bc ge)
(
NOSTK:
bc_nostack bc)
(
HLE:
Unreach.hle su (
bc2su bc ge.(
Genv.genv_next)
m.(
Mem.nextblock)))
(
WF:
Unreach.wf su),
sound_state_base su (
Callstate s fptr sg args m)
|
sound_return_state:
forall s v m bc
(
STK:
sound_stack su bc s m (
Mem.nextblock m))
(
RES:
vmatch bc v Vtop)
(
RO:
romatch bc m rm)
(
MM:
mmatch bc m mtop)
(
GE:
genv_match bc ge)
(
NOSTK:
bc_nostack bc)
(
HLE:
Unreach.hle su (
bc2su bc ge.(
Genv.genv_next)
m.(
Mem.nextblock)))
(
WF:
Unreach.wf su),
sound_state_base su (
Returnstate s v m).
Properties of the sound_stack invariant on call stacks.
Lemma sound_stack_ext:
forall m'
bc stk m bound su,
sound_stack su 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 su bc stk m'
bound.
Proof.
induction 1;
intros INV.
-
constructor;
ss.
-
assert (
Plt sp bound')
by eauto with va.
eapply sound_stack_public_call;
eauto.
apply IHsound_stack;
intros.
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.
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 su,
sound_stack su 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 su bc stk m'
bound.
Proof.
Lemma sound_stack_storev:
forall chunk m addr v m'
bc aaddr stk bound su,
Mem.storev chunk m addr v =
Some m' ->
vmatch bc addr aaddr ->
sound_stack su bc stk m bound ->
sound_stack su bc stk m'
bound.
Proof.
Lemma sound_stack_storebytes:
forall m b ofs bytes m'
bc aaddr stk bound su,
Mem.storebytes m b (
Ptrofs.unsigned ofs)
bytes =
Some m' ->
vmatch bc (
Vptr b ofs)
aaddr ->
sound_stack su bc stk m bound ->
sound_stack su bc stk m'
bound.
Proof.
Lemma sound_stack_free:
forall m b lo hi m'
bc stk bound su,
Mem.free m b lo hi =
Some m' ->
sound_stack su bc stk m bound ->
sound_stack su bc stk m'
bound.
Proof.
Lemma sound_stack_new_bound:
forall bc stk m bound bound'
su,
sound_stack su bc stk m bound ->
Ple bound bound' ->
sound_stack su bc stk m bound'.
Proof.
Lemma sound_stack_exten:
forall bc stk m bound (
bc1:
block_classification)
su,
sound_stack su bc stk m bound ->
(
forall b,
Plt b bound ->
bc1 b =
bc b) ->
sound_stack su bc1 stk m bound.
Proof.
intros.
inv H.
-
constructor;
ss.
-
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.
Lemma sound_stack_unreach
su bc stk m bound
(
STK:
sound_stack su bc stk m bound):
<<
LE:
Ple su.(
Unreach.nb)
bound>>.
Proof.
induction STK; i; ss; des; r; etransitivity; eauto; etransitivity; eauto. 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'
su,
(
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 su bc s m'
sp ->
Unreach.hle su (
bc2su bc (
Genv.genv_next ge) (
Mem.nextblock m')) ->
Unreach.wf su ->
sound_state_base su (
State s f (
Vptr sp Ptrofs.zero)
pc'
e'
m').
Proof.
intros.
exploit analyze_succ;
eauto.
intros (
ae'' &
am'' &
AN &
EM &
MM).
econstructor;
eauto.
Qed.
Lemma vmatch_sound
bc blk ofs av
(
VM:
vmatch bc (
Vptr blk ofs)
av):
<<
VALID:
bc blk <>
BCinvalid>>.
Proof.
inv VM; inv H2; try congruence. Qed.
Ltac spl :=
split;
cycle 1; [
r;
ss;
try reflexivity|].
Theorem sound_step_base:
forall su st t st',
RTL.step se ge st t st' ->
sound_state_base su st ->
sound_state_base su st'
/\ <<
MLE:
Unreach.mle su st.(
get_mem)
st'.(
get_mem)>>.
Proof.
End SOUNDNESS.
Extension to separate compilation
Following et al, POPL 2016, we now extend the results above
to the case where only one compilation unit is analyzed, and not the
whole program.
Section LINKING.
Variable prog:
program.
Variable se :
Senv.t.
Variable ge :
genv.
Hypothesis SEGE:
senv_genv_compat se ge.
Inductive sound_state (
su:
Unreach.t):
state ->
Prop :=
|
sound_state_intro:
forall st,
(
forall cunit,
linkorder cunit prog ->
sound_state_base cunit ge su st) ->
sound_state su st.
Theorem sound_step:
forall st t st'
su,
RTL.step se ge st t st' ->
sound_state su st ->
sound_state su st'
/\ <<
MLE:
su.(
Unreach.mle)
st.(
get_mem)
st'.(
get_mem)>>.
Proof.
Remark sound_state_inv:
forall st cunit su,
sound_state su st ->
linkorder cunit prog ->
sound_state_base cunit ge su st.
Proof.
intros. inv H. eauto.
Qed.
End LINKING.
Program Definition ske2bc {
F} (
ske:
Genv.t F unit):
block_classification :=
BC (
fun b =>
if plt b (
Genv.genv_next ske)
then
match Genv.invert_symbol ske b with None =>
BCglob None |
Some id =>
BCglob (
Some id)
end
else BCinvalid)
_ _.
Next Obligation.
des_ifs. Qed.
Next Obligation.
Lemma bc_eta
bc0 bc1
(
IMG:
forall blk,
bc0.(
bc_img)
blk =
bc1.(
bc_img)
blk):
bc0 =
bc1.
Proof.
Soundness of the initial memory abstraction
Section INITIAL.
Context {
F:
Type}.
Variable prog:
AST.program F unit.
Let ge :=
Genv.globalenv prog.
Lemma initial_block_classification:
forall m,
Genv.init_mem prog =
Some m ->
exists bc,
genv_match bc ge
/\
bc_below bc (
Mem.nextblock m)
/\
bc_nostack bc
/\ (
forall b id,
bc b =
BCglob (
Some id) ->
Genv.find_symbol ge id =
Some b)
/\ (
forall b,
Mem.valid_block m b ->
bc b <>
BCinvalid)
/\ <<
BC:
bc =
ske2bc ge>>.
Proof.
Section INIT.
Variable bc:
block_classification.
Hypothesis GMATCH:
genv_match bc ge.
Lemma store_init_data_summary:
forall ab p id,
pge Glob (
ab_summary ab) ->
pge Glob (
ab_summary (
store_init_data ab p id)).
Proof.
Lemma store_init_data_list_summary:
forall idl ab p,
pge Glob (
ab_summary ab) ->
pge Glob (
ab_summary (
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.
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.
change p with (
vplub (
I Int.zero)
p).
eapply smatch_store;
eauto.
constructor.
-
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.t F unit) :=
forall id b v,
Genv.find_symbol g id =
Some b ->
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 Pbot) 0
v.(
gvar_init)).
Lemma alloc_global_match:
forall m g idg m',
Genv.genv_next g =
Mem.nextblock m ->
initial_mem_match bc m g ->
Genv.alloc_global 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',
Genv.genv_next g =
Mem.nextblock m ->
initial_mem_match bc m g ->
Genv.alloc_globals ge m gl =
Some m' ->
initial_mem_match bc m' (
Genv.add_globals g gl).
Proof.
Definition romem_consistent (
defmap:
PTree.t (
globdef F unit)) (
rm:
romem) :=
forall id ab,
rm!
id =
Some ab ->
exists v,
defmap!
id =
Some (
Gvar v)
/\
v.(
gvar_readonly) =
true
/\
v.(
gvar_volatile) =
false
/\
definitive_initializer v.(
gvar_init) =
true
/\
ab =
store_init_data_list (
ablock_init Pbot) 0
v.(
gvar_init).
Lemma alloc_global_consistent:
forall dm rm idg,
romem_consistent dm rm ->
romem_consistent (
PTree.set (
fst idg) (
snd idg)
dm) (
alloc_global rm idg).
Proof.
Lemma romem_for_consistent:
forall cunit,
romem_consistent (
prog_defmap cunit) (
romem_for cunit).
Proof.
Lemma romem_for_consistent_2:
forall `{
LF:
Linker F}
cunit,
linkorder cunit prog ->
romem_consistent (
prog_defmap prog) (
romem_for cunit).
Proof.
intros;
red;
intros.
exploit (
romem_for_consistent cunit);
eauto.
intros (
v &
DM &
RO &
VO &
DEFN &
AB).
destruct (
prog_defmap_linkorder _ _ _ _ H DM)
as (
gd &
P &
Q).
assert (
gd =
Gvar v).
{
inv Q.
inv H2.
simpl in *.
f_equal.
f_equal.
destruct info1,
info2;
auto.
inv H3;
auto;
discriminate. }
subst gd.
exists v;
auto.
Qed.
End INIT.
Theorem initial_mem_matches:
forall `{
LF:
Linker F}
m,
Genv.init_mem prog =
Some m ->
exists bc,
genv_match bc ge
/\
bc_below bc (
Mem.nextblock m)
/\
bc_nostack bc
/\ (
forall cunit,
linkorder cunit prog ->
romatch bc m (
romem_for cunit))
/\ (
forall b,
Mem.valid_block m b ->
bc b <>
BCinvalid)
/\ <<
BC:
bc =
ske2bc ge>>.
Proof.
End INITIAL.
Require Import Axioms.
Theorem sound_initial:
forall prog st,
initial_state prog st ->
exists su_init,
sound_state prog (
Genv.globalenv prog)
su_init st.
Proof.
Hint Resolve areg_sound aregs_sound:
va.
Interface with other optimizations
Ltac InvSoundState :=
match goal with
|
H1:
sound_state ?
prog ?
ge ?
su ?
st,
H2:
linkorder ?
cunit ?
prog |-
_ =>
let S :=
fresh "
S"
in generalize (
sound_state_inv _ _ _ _ _ H1 H2);
intros S;
inv S
end.
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 cunit prog s f sp pc e m r ge su,
sound_state prog ge su (
State s f (
Vptr sp Ptrofs.zero)
pc e m) ->
linkorder cunit prog ->
exists bc,
vmatch bc e#
r (
avalue (
analyze (
romem_for cunit)
f)!!
pc r)
/\
genv_match bc ge
/\
bc sp =
BCstack.
Proof.
intros. InvSoundState. 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.
Lemma aaddr_sound:
forall cunit prog s f sp pc e m r b ofs ge su,
sound_state prog ge su (
State s f (
Vptr sp Ptrofs.zero)
pc e m) ->
linkorder cunit prog ->
e#
r =
Vptr b ofs ->
exists bc,
pmatch bc b ofs (
aaddr (
analyze (
romem_for cunit)
f)!!
pc r)
/\
genv_match bc ge
/\
bc sp =
BCstack.
Proof.
intros.
InvSoundState.
exists bc;
split;
auto.
unfold aaddr;
rewrite AN.
apply match_aptr_of_aval.
rewrite <-
H1.
apply EM.
Qed.
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.
Lemma aaddressing_sound:
forall cunit prog s f sp pc e m addr args b ofs ge su,
sound_state prog ge su (
State s f (
Vptr sp Ptrofs.zero)
pc e m) ->
linkorder cunit prog ->
eval_addressing ge (
Vptr sp Ptrofs.zero)
addr e##
args =
Some (
Vptr b ofs) ->
exists bc,
pmatch bc b ofs (
aaddressing (
analyze (
romem_for cunit)
f)!!
pc addr args)
/\
genv_match bc ge
/\
bc sp =
BCstack.
Proof.
This is a less precise version of abuiltin_arg, where memory
contents are not taken into account.
Definition aaddr_arg (
a:
VA.t) (
ba:
builtin_arg reg) :
aptr :=
match a with
|
VA.Bot =>
Pbot
|
VA.State ae am =>
match ba with
|
BA r =>
aptr_of_aval (
AE.get r ae)
|
BA_addrstack ofs =>
Stk ofs
|
BA_addrglobal id ofs =>
Gl id ofs
|
_ =>
Ptop
end
end.
Lemma aaddr_arg_sound_1:
forall bc rs ae m rm am F V (
ge:
Genv.t F V)
sp a b ofs,
ematch bc rs ae ->
romatch bc m rm ->
mmatch bc m am ->
genv_match bc ge ->
bc sp =
BCstack ->
eval_builtin_arg ge (
fun r :
positive =>
rs #
r) (
Vptr sp Ptrofs.zero)
m a (
Vptr b ofs) ->
pmatch bc b ofs (
aaddr_arg (
VA.State ae am)
a).
Proof.
Lemma aaddr_arg_sound:
forall cunit prog s f sp pc e m a b ofs ge su,
sound_state prog ge su (
State s f (
Vptr sp Ptrofs.zero)
pc e m) ->
linkorder cunit prog ->
eval_builtin_arg ge (
fun r =>
e#
r) (
Vptr sp Ptrofs.zero)
m a (
Vptr b ofs) ->
exists bc,
pmatch bc b ofs (
aaddr_arg (
analyze (
romem_for cunit)
f)!!
pc a)
/\
genv_match bc ge
/\
bc sp =
BCstack.
Proof.
intros.
InvSoundState.
rewrite AN.
exists bc;
split;
auto.
eapply aaddr_arg_sound_1;
eauto.
Qed.