RTL function inlining: semantic preservation
Require Import Coqlib Wfsimpl Maps Errors Integers.
Require Import AST Linking Values Memory Globalenvs Events Smallstep.
Require Import Op Registers RTL.
Require Import Inlining Inliningspec.
Require Import sflib.
Require SimMemInj.
Definition match_prog (
prog tprog:
program) :=
match_program (
fun cunit f tf =>
transf_fundef (
funenv_program cunit)
f =
OK tf)
eq prog tprog.
Lemma transf_program_match:
forall prog tprog,
transf_program prog =
OK tprog ->
match_prog prog tprog.
Proof.
Section INLINING.
Variable prog tprog:
program.
Hypothesis TRANSF:
match_prog prog tprog.
Section CORELEMMA.
Variable se tse:
Senv.t.
Hypothesis (
MATCH_SENV:
Senv.equiv se tse).
Variable ge tge:
genv.
Hypothesis SECOMPATSRC:
senv_genv_compat se ge.
Hypothesis SECOMPATTGT:
senv_genv_compat tse tge.
Hypothesis (
GENV_COMPAT:
genv_compat ge prog).
Hypothesis (
MATCH_GENV:
Genv.match_genvs (
match_globdef (
fun cunit f tf =>
transf_fundef (
funenv_program cunit)
f =
OK tf)
eq prog)
ge tge).
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_match_genv MATCH_GENV).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_match_genv MATCH_GENV).
Lemma functions_translated:
forall (
v:
val) (
f:
fundef),
Genv.find_funct ge v =
Some f ->
exists cu f',
Genv.find_funct tge v =
Some f' /\
transf_fundef (
funenv_program cu)
f =
OK f' /\
linkorder cu prog.
Proof (
Genv.find_funct_match_genv MATCH_GENV).
Lemma function_ptr_translated:
forall (
b:
block) (
f:
fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists cu f',
Genv.find_funct_ptr tge b =
Some f' /\
transf_fundef (
funenv_program cu)
f =
OK f' /\
linkorder cu prog.
Proof (
Genv.find_funct_ptr_match_genv MATCH_GENV).
Lemma sig_function_translated:
forall cu f f',
transf_fundef (
funenv_program cu)
f =
OK f' ->
funsig f' =
funsig f.
Proof.
intros.
destruct f;
Errors.monadInv H.
exploit transf_function_spec;
eauto.
intros SP;
inv SP.
auto.
auto.
Qed.
Properties of contexts and relocations
Remark sreg_below_diff:
forall ctx r r',
Plt r'
ctx.(
dreg) ->
sreg ctx r <>
r'.
Proof.
Remark context_below_diff:
forall ctx1 ctx2 r1 r2,
context_below ctx1 ctx2 ->
Ple r1 ctx1.(
mreg) ->
sreg ctx1 r1 <>
sreg ctx2 r2.
Proof.
Remark context_below_lt:
forall ctx1 ctx2 r,
context_below ctx1 ctx2 ->
Ple r ctx1.(
mreg) ->
Plt (
sreg ctx1 r)
ctx2.(
dreg).
Proof.
Agreement between register sets before and after inlining.
Definition agree_regs (
F:
meminj) (
ctx:
context) (
rs rs':
regset) :=
(
forall r,
Ple r ctx.(
mreg) ->
Val.inject F rs#
r rs'#(
sreg ctx r))
/\(
forall r,
Plt ctx.(
mreg)
r ->
rs#
r =
Vundef).
Definition val_reg_charact (
F:
meminj) (
ctx:
context) (
rs':
regset) (
v:
val) (
r:
reg) :=
(
Plt ctx.(
mreg)
r /\
v =
Vundef) \/ (
Ple r ctx.(
mreg) /\
Val.inject F v rs'#(
sreg ctx r)).
Remark Plt_Ple_dec:
forall p q, {
Plt p q} + {
Ple q p}.
Proof.
intros.
destruct (
plt p q).
left;
auto.
right;
xomega.
Qed.
Lemma agree_val_reg_gen:
forall F ctx rs rs'
r,
agree_regs F ctx rs rs' ->
val_reg_charact F ctx rs'
rs#
r r.
Proof.
intros.
destruct H as [
A B].
destruct (
Plt_Ple_dec (
mreg ctx)
r).
left.
rewrite B;
auto.
right.
auto.
Qed.
Lemma agree_val_regs_gen:
forall F ctx rs rs'
rl,
agree_regs F ctx rs rs' ->
list_forall2 (
val_reg_charact F ctx rs')
rs##
rl rl.
Proof.
Lemma agree_val_reg:
forall F ctx rs rs'
r,
agree_regs F ctx rs rs' ->
Val.inject F rs#
r rs'#(
sreg ctx r).
Proof.
intros.
exploit agree_val_reg_gen;
eauto.
instantiate (1 :=
r).
intros [[
A B] | [
A B]].
rewrite B;
auto.
auto.
Qed.
Lemma agree_val_regs:
forall F ctx rs rs'
rl,
agree_regs F ctx rs rs' ->
Val.inject_list F rs##
rl rs'##(
sregs ctx rl).
Proof.
induction rl;
intros;
simpl.
constructor.
constructor;
auto.
apply agree_val_reg;
auto.
Qed.
Lemma agree_set_reg:
forall F ctx rs rs'
r v v',
agree_regs F ctx rs rs' ->
Val.inject F v v' ->
Ple r ctx.(
mreg) ->
agree_regs F ctx (
rs#
r <-
v) (
rs'#(
sreg ctx r) <-
v').
Proof.
Lemma agree_set_reg_undef:
forall F ctx rs rs'
r v',
agree_regs F ctx rs rs' ->
agree_regs F ctx (
rs#
r <-
Vundef) (
rs'#(
sreg ctx r) <-
v').
Proof.
Lemma agree_set_reg_undef':
forall F ctx rs rs'
r,
agree_regs F ctx rs rs' ->
agree_regs F ctx (
rs#
r <-
Vundef)
rs'.
Proof.
Lemma agree_regs_invariant:
forall F ctx rs rs1 rs2,
agree_regs F ctx rs rs1 ->
(
forall r,
Ple ctx.(
dreg)
r ->
Plt r (
ctx.(
dreg) +
ctx.(
mreg)) ->
rs2#
r =
rs1#
r) ->
agree_regs F ctx rs rs2.
Proof.
Lemma agree_regs_incr:
forall F ctx rs1 rs2 F',
agree_regs F ctx rs1 rs2 ->
inject_incr F F' ->
agree_regs F'
ctx rs1 rs2.
Proof.
intros. destruct H. split; intros. eauto. auto.
Qed.
Remark agree_regs_init:
forall F ctx rs,
agree_regs F ctx (
Regmap.init Vundef)
rs.
Proof.
Lemma agree_regs_init_regs:
forall F ctx rl vl vl',
Val.inject_list F vl vl' ->
(
forall r,
In r rl ->
Ple r ctx.(
mreg)) ->
agree_regs F ctx (
init_regs vl rl) (
init_regs vl' (
sregs ctx rl)).
Proof.
Executing sequences of moves
Lemma tr_moves_init_regs:
forall F stk f sp m ctx1 ctx2,
context_below ctx1 ctx2 ->
forall rdsts rsrcs vl pc1 pc2 rs1,
tr_moves f.(
fn_code)
pc1 (
sregs ctx1 rsrcs) (
sregs ctx2 rdsts)
pc2 ->
(
forall r,
In r rdsts ->
Ple r ctx2.(
mreg)) ->
list_forall2 (
val_reg_charact F ctx1 rs1)
vl rsrcs ->
exists rs2,
star step tse tge (
State stk f sp pc1 rs1 m)
E0 (
State stk f sp pc2 rs2 m)
/\
agree_regs F ctx2 (
init_regs vl rdsts)
rs2
/\
forall r,
Plt r ctx2.(
dreg) ->
rs2#
r =
rs1#
r.
Proof.
Memory invariants
A stack location is private if it is not the image of a valid
location and we have full rights on it.
Definition loc_private (
F:
meminj) (
m m':
mem) (
sp:
block) (
ofs:
Z) :
Prop :=
Mem.perm m'
sp ofs Cur Freeable /\
(
forall b delta,
F b =
Some(
sp,
delta) -> ~
Mem.perm m b (
ofs -
delta)
Max Nonempty).
Likewise, for a range of locations.
Definition range_private (
F:
meminj) (
m m':
mem) (
sp:
block) (
lo hi:
Z) :
Prop :=
forall ofs,
lo <=
ofs <
hi ->
loc_private F m m'
sp ofs.
Lemma range_private_tgt_private
sm blk lo hi
(
MWF:
SimMemInj.wf'
sm)
(
PRIVTGT:
range_private sm.(
SimMemInj.inj)
sm.(
SimMemInj.src)
sm.(
SimMemInj.tgt)
blk lo hi):
forall ofs (
BDD:
lo <=
ofs <
hi), <<
PRIVTGT:
sm.(
SimMemInj.tgt_private)
blk ofs>>.
Proof.
ii. repeat red. specialize (PRIVTGT ofs BDD). red in PRIVTGT. des.
esplits; eauto. red. eauto with mem.
Qed.
Lemma range_private_invariant:
forall F m m'
sp lo hi F1 m1 m1',
range_private F m m'
sp lo hi ->
(
forall b delta ofs,
F1 b =
Some(
sp,
delta) ->
Mem.perm m1 b ofs Max Nonempty ->
lo <=
ofs +
delta <
hi ->
F b =
Some(
sp,
delta) /\
Mem.perm m b ofs Max Nonempty) ->
(
forall ofs,
Mem.perm m'
sp ofs Cur Freeable ->
Mem.perm m1'
sp ofs Cur Freeable) ->
range_private F1 m1 m1'
sp lo hi.
Proof.
intros; red; intros. exploit H; eauto. intros [A B]. split; auto.
intros; red; intros. exploit H0; eauto. omega. intros [P Q].
eelim B; eauto.
Qed.
Lemma range_private_perms:
forall F m m'
sp lo hi,
range_private F m m'
sp lo hi ->
Mem.range_perm m'
sp lo hi Cur Freeable.
Proof.
intros; red; intros. eapply H; eauto.
Qed.
Lemma range_private_alloc_left:
forall F m m'
sp'
base hi sz m1 sp F1,
range_private F m m'
sp'
base hi ->
Mem.alloc m 0
sz = (
m1,
sp) ->
F1 sp =
Some(
sp',
base) ->
(
forall b,
b <>
sp ->
F1 b =
F b) ->
range_private F1 m1 m'
sp' (
base +
Z.max sz 0)
hi.
Proof.
intros;
red;
intros.
exploit (
H ofs).
generalize (
Z.le_max_r sz 0).
omega.
intros [
A B].
split;
auto.
intros;
red;
intros.
exploit Mem.perm_alloc_inv;
eauto.
destruct (
eq_block b sp);
intros.
subst b.
rewrite H1 in H4;
inv H4.
rewrite Zmax_spec in H3.
destruct (
zlt 0
sz);
omega.
rewrite H2 in H4;
auto.
eelim B;
eauto.
Qed.
Lemma range_private_free_left:
forall F m m'
sp base sz hi b m1,
range_private F m m'
sp (
base +
Z.max sz 0)
hi ->
Mem.free m b 0
sz =
Some m1 ->
F b =
Some(
sp,
base) ->
Mem.inject F m m' ->
range_private F m1 m'
sp base hi.
Proof.
Lemma range_private_extcall:
forall F F'
m1 m2 m1'
m2'
sp base hi,
range_private F m1 m1'
sp base hi ->
(
forall b ofs p,
Mem.valid_block m1 b ->
Mem.perm m2 b ofs Max p ->
Mem.perm m1 b ofs Max p) ->
Mem.unchanged_on (
loc_out_of_reach F m1)
m1'
m2' ->
Mem.inject F m1 m1' ->
inject_incr F F' ->
inject_separated F F'
m1 m1' ->
Mem.valid_block m1'
sp ->
range_private F'
m2 m2'
sp base hi.
Proof.
intros until hi;
intros RP PERM UNCH INJ INCR SEP VB.
red;
intros.
exploit RP;
eauto.
intros [
A B].
split.
eapply Mem.perm_unchanged_on;
eauto.
intros.
red in SEP.
destruct (
F b)
as [[
sp1 delta1] |]
eqn:?.
exploit INCR;
eauto.
intros EQ;
rewrite H0 in EQ;
inv EQ.
red;
intros;
eelim B;
eauto.
eapply PERM;
eauto.
red.
destruct (
plt b (
Mem.nextblock m1));
auto.
exploit Mem.mi_freeblocks;
eauto.
congruence.
exploit SEP;
eauto.
tauto.
Qed.
Relating global environments
Inductive match_globalenvs (
F:
meminj) (
bound:
block):
Prop :=
|
mk_match_globalenvs
(
DOMAIN:
forall b,
Plt b bound ->
F b =
Some(
b, 0))
(
IMAGE:
forall b1 b2 delta,
F b1 =
Some(
b2,
delta) ->
Plt b2 bound ->
b1 =
b2)
(
SYMBOLS:
forall id b,
Genv.find_symbol ge id =
Some b ->
Plt b bound)
(
FUNCTIONS:
forall b fd,
Genv.find_funct_ptr ge b =
Some fd ->
Plt b bound)
(
VARINFOS:
forall b gv,
Genv.find_var_info ge b =
Some gv ->
Plt b bound).
Lemma find_function_ptr_agree:
forall ros rs fptr F ctx rs'
bound,
find_function_ptr ge ros rs =
fptr ->
agree_regs F ctx rs rs' ->
match_globalenvs F bound ->
exists tfptr,
find_function_ptr tge (
sros ctx ros)
rs' =
tfptr /\
Val.inject F fptr tfptr.
Proof.
Lemma find_inlined_function:
forall fenv id rs f fptr,
fenv_compat prog fenv ->
find_function_ptr ge (
inr id)
rs =
fptr ->
fenv!
id =
Some f ->
<<
FPTR:
Genv.find_funct ge fptr =
Some (
Internal f)>>.
Proof.
intros.
apply H in H1.
apply GENV_COMPAT in H1.
destruct H1 as (
b &
A &
B).
simpl in H0.
unfold fundef in *.
rewrite A in H0.
clarify.
ss.
des_ifs.
unfold Genv.find_funct_ptr.
des_ifs.
Qed.
Lemma functions_injected
j v tv f
(
SRC:
Genv.find_funct ge v =
Some f)
(
INJ:
Val.inject j v tv)
(
MATCH:
exists bound,
match_globalenvs j bound):
exists cunit tf, <<
TGT:
Genv.find_funct tge tv =
Some tf>> /\
<<
TRANSF:
transf_fundef (
funenv_program cunit)
f =
OK tf>> /\
<<
LINK:
linkorder cunit prog>>.
Proof.
Translation of builtin arguments.
Lemma tr_builtin_arg:
forall F bound ctx rs rs'
sp sp'
m m',
match_globalenvs F bound ->
agree_regs F ctx rs rs' ->
F sp =
Some(
sp',
ctx.(
dstk)) ->
Mem.inject F m m' ->
forall a v,
eval_builtin_arg ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m a v ->
exists v',
eval_builtin_arg tge (
fun r =>
rs'#
r) (
Vptr sp'
Ptrofs.zero)
m' (
sbuiltinarg ctx a)
v'
/\
Val.inject F v v'.
Proof.
Lemma tr_builtin_args:
forall F bound ctx rs rs'
sp sp'
m m',
match_globalenvs F bound ->
agree_regs F ctx rs rs' ->
F sp =
Some(
sp',
ctx.(
dstk)) ->
Mem.inject F m m' ->
forall al vl,
eval_builtin_args ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m al vl ->
exists vl',
eval_builtin_args tge (
fun r =>
rs'#
r) (
Vptr sp'
Ptrofs.zero)
m' (
map (
sbuiltinarg ctx)
al)
vl'
/\
Val.inject_list F vl vl'.
Proof.
induction 5;
simpl.
-
exists (@
nil val);
split;
constructor.
-
exploit tr_builtin_arg;
eauto.
intros (
v1' &
A &
B).
destruct IHlist_forall2 as (
vl' &
C &
D).
exists (
v1' ::
vl');
split;
constructor;
auto.
Qed.
Relating stacks
Inductive match_stacks (
F:
meminj) (
m m':
mem) (
sm0:
SimMemInj.t') :
list stackframe ->
list stackframe ->
block ->
Prop :=
|
match_stacks_nil:
forall bound1 bound
(
SYMBINJ:
symbols_inject F se tse)
(
HI:
bound1 =
ge.(
Genv.genv_next))
(
MG:
match_globalenvs F bound1)
(
BELOW:
Ple bound1 bound),
match_stacks F m m'
sm0 nil nil bound
|
match_stacks_cons:
forall res f sp pc rs stk f'
sp'
rs'
stk'
bound fenv ctx
(
MS:
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs')
(
DISJ:
sm0.(
SimMemInj.tgt_external) /2\ (
fun blk _ =>
sp' =
blk) <2=
bot2)
(
COMPAT:
fenv_compat prog fenv)
(
FB:
tr_funbody fenv f'.(
fn_stacksize)
ctx f f'.(
fn_code))
(
AG:
agree_regs F ctx rs rs')
(
SP:
F sp =
Some(
sp',
ctx.(
dstk)))
(
PRIV:
range_private F m m'
sp' (
ctx.(
dstk) +
ctx.(
mstk))
f'.(
fn_stacksize))
(
SSZ1: 0 <=
f'.(
fn_stacksize) <
Ptrofs.max_unsigned)
(
SSZ2:
forall ofs,
Mem.perm m'
sp'
ofs Max Nonempty -> 0 <=
ofs <=
f'.(
fn_stacksize))
(
RES:
Ple res ctx.(
mreg))
(
BELOW:
Plt sp'
bound),
match_stacks F m m'
sm0
(
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
(
Stackframe (
sreg ctx res)
f' (
Vptr sp'
Ptrofs.zero) (
spc ctx pc)
rs' ::
stk')
bound
|
match_stacks_untailcall:
forall stk res f'
sp'
rpc rs'
stk'
bound ctx
(
MS:
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs')
(
DISJ:
sm0.(
SimMemInj.tgt_external) /2\ (
fun blk _ =>
sp' =
blk) <2=
bot2)
(
PRIV:
range_private F m m'
sp'
ctx.(
dstk)
f'.(
fn_stacksize))
(
SSZ1: 0 <=
f'.(
fn_stacksize) <
Ptrofs.max_unsigned)
(
SSZ2:
forall ofs,
Mem.perm m'
sp'
ofs Max Nonempty -> 0 <=
ofs <=
f'.(
fn_stacksize))
(
RET:
ctx.(
retinfo) =
Some (
rpc,
res))
(
BELOW:
Plt sp'
bound),
match_stacks F m m'
sm0
stk
(
Stackframe res f' (
Vptr sp'
Ptrofs.zero)
rpc rs' ::
stk')
bound
with match_stacks_inside (
F:
meminj) (
m m':
mem) (
sm0:
SimMemInj.t') :
list stackframe ->
list stackframe ->
function ->
context ->
block ->
regset ->
Prop :=
|
match_stacks_inside_base:
forall stk stk'
f'
ctx sp'
rs'
(
MS:
match_stacks F m m'
sm0 stk stk'
sp')
(
DISJ:
sm0.(
SimMemInj.tgt_external) /2\ (
fun blk _ =>
sp' =
blk) <2=
bot2)
(
BB: (
SimMemInj.tgt_parent_nb sm0 <=
sp')%
positive)
(
RET:
ctx.(
retinfo) =
None)
(
DSTK:
ctx.(
dstk) = 0),
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs'
|
match_stacks_inside_inlined:
forall res f sp pc rs stk stk'
f'
fenv ctx sp'
rs'
ctx'
(
MS:
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx'
sp'
rs')
(
DISJ:
sm0.(
SimMemInj.tgt_external) /2\ (
fun blk _ =>
sp' =
blk) <2=
bot2)
(
BB: (
SimMemInj.tgt_parent_nb sm0 <=
sp')%
positive)
(
COMPAT:
fenv_compat prog fenv)
(
FB:
tr_funbody fenv f'.(
fn_stacksize)
ctx'
f f'.(
fn_code))
(
AG:
agree_regs F ctx'
rs rs')
(
SP:
F sp =
Some(
sp',
ctx'.(
dstk)))
(
PAD:
range_private F m m'
sp' (
ctx'.(
dstk) +
ctx'.(
mstk))
ctx.(
dstk))
(
RES:
Ple res ctx'.(
mreg))
(
RET:
ctx.(
retinfo) =
Some (
spc ctx'
pc,
sreg ctx'
res))
(
BELOW:
context_below ctx'
ctx)
(
SBELOW:
context_stack_call ctx'
ctx),
match_stacks_inside F m m'
sm0 (
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
stk'
f'
ctx sp'
rs'.
Properties of match_stacks
Section MATCH_STACKS.
Variable F:
meminj.
Variables m m':
mem.
Lemma match_stacks_symbols_inject:
forall stk stk'
bound sm0,
match_stacks F m m'
sm0 stk stk'
bound ->
symbols_inject F se tse
with match_stacks_inside_symbols_inject:
forall stk stk'
f ctx sp rs'
sm0,
match_stacks_inside F m m'
sm0 stk stk'
f ctx sp rs' ->
symbols_inject F se tse.
Proof.
induction 1; eauto. induction 1; eauto. Qed.
Lemma match_stacks_globalenvs:
forall stk stk'
bound sm0,
match_stacks F m m'
sm0 stk stk'
bound ->
exists b,
match_globalenvs F b
with match_stacks_inside_globalenvs:
forall stk stk'
f ctx sp rs'
sm0,
match_stacks_inside F m m'
sm0 stk stk'
f ctx sp rs' ->
exists b,
match_globalenvs F b.
Proof.
induction 1; eauto.
induction 1; eauto.
Qed.
Lemma match_globalenvs_preserves_globals:
forall b,
match_globalenvs F b ->
meminj_preserves_globals ge F.
Proof.
intros. inv H. red. split. eauto. split. eauto.
intros. symmetry. eapply IMAGE; eauto.
Qed.
Lemma match_stacks_inside_globals:
forall stk stk'
f ctx sp rs'
sm0,
match_stacks_inside F m m'
sm0 stk stk'
f ctx sp rs' ->
meminj_preserves_globals ge F.
Proof.
Lemma match_stacks_bound:
forall stk stk'
bound bound1 sm0,
match_stacks F m m'
sm0 stk stk'
bound ->
Ple bound bound1 ->
match_stacks F m m'
sm0 stk stk'
bound1.
Proof.
Variable F1:
meminj.
Variables m1 m1':
mem.
Hypothesis INCR:
inject_incr F F1.
Lemma match_stacks_invariant:
forall stk stk'
bound sm0,
match_stacks F m m'
sm0 stk stk'
bound ->
forall (
INJ:
forall b1 b2 delta,
F1 b1 =
Some(
b2,
delta) ->
Plt b2 bound ->
F b1 =
Some(
b2,
delta))
(
PERM1:
forall b1 b2 delta ofs,
F1 b1 =
Some(
b2,
delta) ->
Plt b2 bound ->
Mem.perm m1 b1 ofs Max Nonempty ->
Mem.perm m b1 ofs Max Nonempty)
(
PERM2:
forall b ofs,
Plt b bound ->
Mem.perm m'
b ofs Cur Freeable ->
Mem.perm m1'
b ofs Cur Freeable)
(
PERM3:
forall b ofs k p,
Plt b bound ->
Mem.perm m1'
b ofs k p ->
Mem.perm m'
b ofs k p),
match_stacks F1 m1 m1'
sm0 stk stk'
bound
with match_stacks_inside_invariant:
forall stk stk'
f'
ctx sp'
rs1 sm0,
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs1 ->
forall rs2
(
RS:
forall r,
Plt r ctx.(
dreg) ->
rs2#
r =
rs1#
r)
(
INJ:
forall b1 b2 delta,
F1 b1 =
Some(
b2,
delta) ->
Ple b2 sp' ->
F b1 =
Some(
b2,
delta))
(
PERM1:
forall b1 b2 delta ofs,
F1 b1 =
Some(
b2,
delta) ->
Ple b2 sp' ->
Mem.perm m1 b1 ofs Max Nonempty ->
Mem.perm m b1 ofs Max Nonempty)
(
PERM2:
forall b ofs,
Ple b sp' ->
Mem.perm m'
b ofs Cur Freeable ->
Mem.perm m1'
b ofs Cur Freeable)
(
PERM3:
forall b ofs k p,
Ple b sp' ->
Mem.perm m1'
b ofs k p ->
Mem.perm m'
b ofs k p),
match_stacks_inside F1 m1 m1'
sm0 stk stk'
f'
ctx sp'
rs2.
Proof.
induction 1;
intros.
apply match_stacks_nil with (
bound1 :=
bound1).
{
eapply symbols_inject_incr;
eauto.
-
i.
inv SECOMPATSRC.
rewrite NB in *.
inv MG.
exploit DOMAIN;
eauto.
i;
clarify.
exploit INCR;
eauto.
i;
clarify.
-
i.
inv SECOMPATTGT.
rewrite NB in *.
erewrite INJ;
eauto.
inv MATCH_GENV.
rewrite mge_next in *.
xomega.
}
{
ss. }
inv MG.
constructor;
auto.
intros.
apply IMAGE with delta.
eapply INJ;
eauto.
eapply Pos.lt_le_trans;
eauto.
auto.
auto.
apply match_stacks_cons with (
fenv :=
fenv) (
ctx :=
ctx);
auto.
eapply match_stacks_inside_invariant;
eauto.
intros;
eapply INJ;
eauto;
xomega.
intros;
eapply PERM1;
eauto;
xomega.
intros;
eapply PERM2;
eauto;
xomega.
intros;
eapply PERM3;
eauto;
xomega.
eapply agree_regs_incr;
eauto.
eapply range_private_invariant;
eauto.
apply match_stacks_untailcall with (
ctx :=
ctx);
auto.
eapply match_stacks_inside_invariant;
eauto.
intros;
eapply INJ;
eauto;
xomega.
intros;
eapply PERM1;
eauto;
xomega.
intros;
eapply PERM2;
eauto;
xomega.
intros;
eapply PERM3;
eauto;
xomega.
eapply range_private_invariant;
eauto.
induction 1;
intros.
eapply match_stacks_inside_base;
eauto.
eapply match_stacks_invariant;
eauto.
intros;
eapply INJ;
eauto;
xomega.
intros;
eapply PERM1;
eauto;
xomega.
intros;
eapply PERM2;
eauto;
xomega.
intros;
eapply PERM3;
eauto;
xomega.
apply match_stacks_inside_inlined with (
fenv :=
fenv) (
ctx' :=
ctx');
auto.
apply IHmatch_stacks_inside;
auto.
intros.
apply RS.
red in BELOW.
xomega.
apply agree_regs_incr with F;
auto.
apply agree_regs_invariant with rs';
auto.
intros.
apply RS.
red in BELOW.
xomega.
eapply range_private_invariant;
eauto.
intros.
split.
eapply INJ;
eauto.
xomega.
eapply PERM1;
eauto.
xomega.
intros.
eapply PERM2;
eauto.
xomega.
Qed.
Lemma match_stacks_empty:
forall stk stk'
bound sm0,
match_stacks F m m'
sm0 stk stk'
bound ->
stk =
nil ->
stk' =
nil
with match_stacks_inside_empty:
forall stk stk'
f ctx sp rs sm0,
match_stacks_inside F m m'
sm0 stk stk'
f ctx sp rs ->
stk =
nil ->
stk' =
nil /\
ctx.(
retinfo) =
None.
Proof.
induction 1; intros.
auto.
discriminate.
exploit match_stacks_inside_empty; eauto. intros [A B]. congruence.
induction 1; intros.
split. eapply match_stacks_empty; eauto. auto.
discriminate.
Qed.
Lemma match_stacks_le:
forall
sm0 sm1 F m m'
stk stk'
bound
(
MS:
match_stacks F m m'
sm0 stk stk'
bound)
(
LE:
SimMemInj.le'
sm0 sm1),
<<
MS:
match_stacks F m m'
sm1 stk stk'
bound>>
with match_stacks_inside_le:
forall
sm0 sm1 F m m'
stk stk'
f'
ctx sp'
rs'
(
MS:
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs')
(
LE:
SimMemInj.le'
sm0 sm1),
<<
MS:
match_stacks_inside F m m'
sm1 stk stk'
f'
ctx sp'
rs'>>.
Proof.
- induction 1; ii; ss; econs; eauto; try (eapply match_stacks_inside_le; eauto).
all: ii; des; eapply DISJ; eauto; esplits; eauto; inv LE; congruence.
- induction 1; ii; ss.
+ econs; eauto; try (eapply match_stacks_le; eauto); inv LE; try congruence.
ii; des; eapply DISJ; eauto; esplits; eauto; congruence.
+ econs 2; eauto; try (eapply match_stacks_inside_le; eauto); inv LE; try congruence.
ii; des; eapply DISJ; eauto; esplits; eauto; congruence.
Qed.
End MATCH_STACKS.
Preservation by assignment to a register
Lemma match_stacks_inside_set_reg:
forall F m m'
stk stk'
f'
ctx sp'
rs'
r v sm0,
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs' ->
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp' (
rs'#(
sreg ctx r) <-
v).
Proof.
Lemma match_stacks_inside_set_res:
forall F m m'
stk stk'
f'
ctx sp'
rs'
res v sm0,
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs' ->
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp' (
regmap_setres (
sbuiltinres ctx res)
v rs').
Proof.
Preservation by a memory store
Lemma match_stacks_inside_store:
forall F m m'
stk stk'
f'
ctx sp'
rs'
chunk b ofs v m1 chunk'
b'
ofs'
v'
m1'
sm0,
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs' ->
Mem.store chunk m b ofs v =
Some m1 ->
Mem.store chunk'
m'
b'
ofs'
v' =
Some m1' ->
match_stacks_inside F m1 m1'
sm0 stk stk'
f'
ctx sp'
rs'.
Proof.
Preservation by an allocation
Lemma match_stacks_inside_alloc_left:
forall F m m'
stk stk'
f'
ctx sp'
rs'
sm0,
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs' ->
forall sz m1 b F1 delta,
Mem.alloc m 0
sz = (
m1,
b) ->
inject_incr F F1 ->
F1 b =
Some(
sp',
delta) ->
(
forall b1,
b1 <>
b ->
F1 b1 =
F b1) ->
delta >=
ctx.(
dstk) ->
match_stacks_inside F1 m1 m'
sm0 stk stk'
f'
ctx sp'
rs'.
Proof.
Preservation by freeing
Lemma match_stacks_free_left:
forall F m m'
stk stk'
sp b lo hi m1 sm0,
match_stacks F m m'
sm0 stk stk'
sp ->
Mem.free m b lo hi =
Some m1 ->
match_stacks F m1 m'
sm0 stk stk'
sp.
Proof.
Lemma match_stacks_free_right:
forall F m m'
stk stk'
sp lo hi m1'
sm0,
match_stacks F m m'
sm0 stk stk'
sp ->
Mem.free m'
sp lo hi =
Some m1' ->
match_stacks F m m1'
sm0 stk stk'
sp.
Proof.
Lemma min_alignment_sound:
forall sz n, (
min_alignment sz |
n) ->
Mem.inj_offset_aligned n sz.
Proof.
intros;
red;
intros.
unfold min_alignment in H.
assert (2 <=
sz -> (2 |
n)).
intros.
destruct (
zle sz 1).
omegaContradiction.
destruct (
zle sz 2).
auto.
destruct (
zle sz 4).
apply Zdivides_trans with 4;
auto.
exists 2;
auto.
apply Zdivides_trans with 8;
auto.
exists 4;
auto.
assert (4 <=
sz -> (4 |
n)).
intros.
destruct (
zle sz 1).
omegaContradiction.
destruct (
zle sz 2).
omegaContradiction.
destruct (
zle sz 4).
auto.
apply Zdivides_trans with 8;
auto.
exists 2;
auto.
assert (8 <=
sz -> (8 |
n)).
intros.
destruct (
zle sz 1).
omegaContradiction.
destruct (
zle sz 2).
omegaContradiction.
destruct (
zle sz 4).
omegaContradiction.
auto.
destruct chunk;
simpl in *;
auto.
apply Z.divide_1_l.
apply Z.divide_1_l.
apply H2;
omega.
apply H2;
omega.
Qed.
Preservation by external calls
Section EXTCALL.
Variables F1 F2:
meminj.
Variables m1 m2 m1'
m2':
mem.
Hypothesis MAXPERM:
forall b ofs p,
Mem.valid_block m1 b ->
Mem.perm m2 b ofs Max p ->
Mem.perm m1 b ofs Max p.
Hypothesis MAXPERM':
forall b ofs p,
Mem.valid_block m1'
b ->
Mem.perm m2'
b ofs Max p ->
Mem.perm m1'
b ofs Max p.
Hypothesis UNCHANGED:
Mem.unchanged_on (
loc_out_of_reach F1 m1)
m1'
m2'.
Hypothesis INJ:
Mem.inject F1 m1 m1'.
Hypothesis INCR:
inject_incr F1 F2.
Hypothesis SEP:
inject_separated F1 F2 m1 m1'.
Lemma match_stacks_extcall:
forall stk stk'
bound sm0,
match_stacks F1 m1 m1'
sm0 stk stk'
bound ->
Ple bound (
Mem.nextblock m1') ->
match_stacks F2 m2 m2'
sm0 stk stk'
bound
with match_stacks_inside_extcall:
forall stk stk'
f'
ctx sp'
rs'
sm0,
match_stacks_inside F1 m1 m1'
sm0 stk stk'
f'
ctx sp'
rs' ->
Plt sp' (
Mem.nextblock m1') ->
match_stacks_inside F2 m2 m2'
sm0 stk stk'
f'
ctx sp'
rs'.
Proof.
End EXTCALL.
Change of context corresponding to an inlined tailcall
Lemma align_unchanged:
forall n amount,
amount > 0 -> (
amount |
n) ->
align n amount =
n.
Proof.
intros.
destruct H0 as [
p EQ].
subst n.
unfold align.
decEq.
apply Zdiv_unique with (
b :=
amount - 1).
omega.
omega.
Qed.
Lemma match_stacks_inside_inlined_tailcall:
forall fenv F m m'
stk stk'
f'
ctx sp'
rs'
ctx'
f sm0,
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs' ->
context_below ctx ctx' ->
context_stack_tailcall ctx f ctx' ->
ctx'.(
retinfo) =
ctx.(
retinfo) ->
range_private F m m'
sp'
ctx.(
dstk)
f'.(
fn_stacksize) ->
forall (
MYDISJ:
sm0.(
SimMemInj.tgt_external) /2\ (
fun blk _ =>
sp' =
blk) <2=
bot2),
tr_funbody fenv f'.(
fn_stacksize)
ctx'
f f'.(
fn_code) ->
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx'
sp'
rs'.
Proof.
Relating states
Inductive match_states:
RTL.state ->
RTL.state ->
SimMemInj.t' ->
Prop :=
|
match_regular_states:
forall stk f sp pc rs m stk'
f'
sp'
rs'
m'
F fenv ctx
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
F)
(
MWF:
SimMemInj.wf'
sm0)
(
MS:
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs')
(
COMPAT:
fenv_compat prog fenv)
(
FB:
tr_funbody fenv f'.(
fn_stacksize)
ctx f f'.(
fn_code))
(
AG:
agree_regs F ctx rs rs')
(
SP:
F sp =
Some(
sp',
ctx.(
dstk)))
(
MINJ:
Mem.inject F m m')
(
VB:
Mem.valid_block m'
sp')
(
PRIV:
range_private F m m'
sp' (
ctx.(
dstk) +
ctx.(
mstk))
f'.(
fn_stacksize))
(
SSZ1: 0 <=
f'.(
fn_stacksize) <
Ptrofs.max_unsigned)
(
SSZ2:
forall ofs,
Mem.perm m'
sp'
ofs Max Nonempty -> 0 <=
ofs <=
f'.(
fn_stacksize)),
match_states (
State stk f (
Vptr sp Ptrofs.zero)
pc rs m)
(
State stk'
f' (
Vptr sp'
Ptrofs.zero) (
spc ctx pc)
rs'
m')
sm0
|
match_call_states:
forall stk fptr sg tfptr args m stk'
args'
m'
F
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
F)
(
MWF:
SimMemInj.wf'
sm0)
(
MS:
match_stacks F m m'
sm0 stk stk' (
Mem.nextblock m'))
(
FPTR:
Val.inject F fptr tfptr)
(
VINJ:
Val.inject_list F args args')
(
MINJ:
Mem.inject F m m'),
match_states (
Callstate stk fptr sg args m)
(
Callstate stk'
tfptr sg args'
m')
sm0
|
match_call_regular_states:
forall stk fptr sg f vargs m stk'
f'
sp'
rs'
m'
F fenv ctx ctx'
pc'
pc1'
rargs
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
F)
(
MWF:
SimMemInj.wf'
sm0)
(
MS:
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs')
(
FPTR:
Genv.find_funct ge fptr =
Some (
Internal f))
(
COMPAT:
fenv_compat prog fenv)
(
FB:
tr_funbody fenv f'.(
fn_stacksize)
ctx f f'.(
fn_code))
(
BELOW:
context_below ctx'
ctx)
(
NOP:
f'.(
fn_code)!
pc' =
Some(
Inop pc1'))
(
MOVES:
tr_moves f'.(
fn_code)
pc1' (
sregs ctx'
rargs) (
sregs ctx f.(
fn_params)) (
spc ctx f.(
fn_entrypoint)))
(
VINJ:
list_forall2 (
val_reg_charact F ctx'
rs')
vargs rargs)
(
MINJ:
Mem.inject F m m')
(
VB:
Mem.valid_block m'
sp')
(
PRIV:
range_private F m m'
sp'
ctx.(
dstk)
f'.(
fn_stacksize))
(
SSZ1: 0 <=
f'.(
fn_stacksize) <
Ptrofs.max_unsigned)
(
SSZ2:
forall ofs,
Mem.perm m'
sp'
ofs Max Nonempty -> 0 <=
ofs <=
f'.(
fn_stacksize)),
match_states (
Callstate stk fptr sg vargs m)
(
State stk'
f' (
Vptr sp'
Ptrofs.zero)
pc'
rs'
m')
sm0
|
match_return_states:
forall stk v m stk'
v'
m'
F
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
F)
(
MWF:
SimMemInj.wf'
sm0)
(
MS:
match_stacks F m m'
sm0 stk stk' (
Mem.nextblock m'))
(
VINJ:
Val.inject F v v')
(
MINJ:
Mem.inject F m m'),
match_states (
Returnstate stk v m)
(
Returnstate stk'
v'
m')
sm0
|
match_return_regular_states:
forall stk v m stk'
f'
sp'
rs'
m'
F ctx pc'
or rinfo
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
F)
(
MWF:
SimMemInj.wf'
sm0)
(
MS:
match_stacks_inside F m m'
sm0 stk stk'
f'
ctx sp'
rs')
(
RET:
ctx.(
retinfo) =
Some rinfo)
(
AT:
f'.(
fn_code)!
pc' =
Some(
inline_return ctx or rinfo))
(
VINJ:
match or with None =>
v =
Vundef |
Some r =>
Val.inject F v rs'#(
sreg ctx r)
end)
(
MINJ:
Mem.inject F m m')
(
VB:
Mem.valid_block m'
sp')
(
PRIV:
range_private F m m'
sp'
ctx.(
dstk)
f'.(
fn_stacksize))
(
SSZ1: 0 <=
f'.(
fn_stacksize) <
Ptrofs.max_unsigned)
(
SSZ2:
forall ofs,
Mem.perm m'
sp'
ofs Max Nonempty -> 0 <=
ofs <=
f'.(
fn_stacksize)),
match_states (
Returnstate stk v m)
(
State stk'
f' (
Vptr sp'
Ptrofs.zero)
pc'
rs'
m')
sm0.
Forward simulation
Definition measure (
S:
RTL.state) :
nat :=
match S with
|
State _ _ _ _ _ _ => 1%
nat
|
Callstate _ _ _ _ _ => 0%
nat
|
Returnstate _ _ _ => 0%
nat
end.
Lemma tr_funbody_inv:
forall fenv sz cts f c pc i,
tr_funbody fenv sz cts f c ->
f.(
fn_code)!
pc =
Some i ->
tr_instr fenv sz cts pc i c.
Proof.
intros. inv H. eauto.
Qed.
Theorem step_simulation:
forall S1 t S2,
step se ge S1 t S2 ->
forall S1'
sm0 (
MS:
match_states S1 S1'
sm0),
(
exists S2',
plus step tse tge S1'
t S2' /\
exists sm1,
match_states S2 S2'
sm1 /\ <<
MLE:
SimMemInj.le'
sm0 sm1>>)
\/ (
measure S2 <
measure S1 /\
t =
E0 /\
exists sm1,
match_states S2 S1'
sm1 /\ <<
MLE:
SimMemInj.le'
sm0 sm1>>)%
nat.
Proof.
End CORELEMMA.
Section WHOLE.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Let MATCH_GENV:
Genv.match_genvs (
match_globdef (
fun cunit f tf =>
transf_fundef (
funenv_program cunit)
f =
OK tf)
eq prog)
ge tge.
Proof.
Let GENV_COMPAT:
genv_compat ge prog.
Proof.
Let match_states :=
match_states ge tge.
Lemma transf_initial_states:
forall st1,
initial_state prog st1 ->
exists st2,
initial_state tprog st2 /\
exists sm,
match_states ge st1 st2 sm.
Proof.
Lemma transf_final_states:
forall st1 st2 r,
(
exists sm,
match_states ge st1 st2 sm) ->
final_state st1 r ->
final_state st2 r.
Proof.
Theorem transf_program_correct:
forward_simulation (
semantics prog) (
semantics tprog).
Proof.
End WHOLE.
End INLINING.