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.
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:
program.
Variable tprog:
program.
Hypothesis TRANSF:
match_prog prog tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_match TRANSF).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_match TRANSF).
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 TRANSF).
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 TRANSF).
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;
extlia.
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 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_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. lia. 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).
lia.
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);
lia.
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_agree:
forall ros rs fd F ctx rs'
bound,
find_function ge ros rs =
Some fd ->
agree_regs F ctx rs rs' ->
match_globalenvs F bound ->
exists cu fd',
find_function tge (
sros ctx ros)
rs' =
Some fd' /\
transf_fundef (
funenv_program cu)
fd =
OK fd' /\
linkorder cu prog.
Proof.
Lemma find_inlined_function:
forall fenv id rs fd f,
fenv_compat prog fenv ->
find_function ge (
inr id)
rs =
Some fd ->
fenv!
id =
Some f ->
fd =
Internal f.
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):
list stackframe ->
list stackframe ->
block ->
Prop :=
|
match_stacks_nil:
forall bound1 bound
(
MG:
match_globalenvs F bound1)
(
BELOW:
Ple bound1 bound),
match_stacks F m m'
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'
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)))
(
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'
(
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'
stk stk'
f'
ctx sp'
rs')
(
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'
stk
(
Stackframe res f' (
Vptr sp'
Ptrofs.zero)
rpc rs' ::
stk')
bound
with match_stacks_inside (
F:
meminj) (
m m':
mem):
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'
stk stk'
sp')
(
RET:
ctx.(
retinfo) =
None)
(
DSTK:
ctx.(
dstk) = 0),
match_stacks_inside F m m'
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'
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)))
(
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' (
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_globalenvs:
forall stk stk'
bound,
match_stacks F m m'
stk stk'
bound ->
exists b,
match_globalenvs F b
with match_stacks_inside_globalenvs:
forall stk stk'
f ctx sp rs',
match_stacks_inside F m m'
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',
match_stacks_inside F m m'
stk stk'
f ctx sp rs' ->
meminj_preserves_globals ge F.
Proof.
Lemma match_stacks_bound:
forall stk stk'
bound bound1,
match_stacks F m m'
stk stk'
bound ->
Ple bound bound1 ->
match_stacks F m m'
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,
match_stacks F m m'
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'
stk stk'
bound
with match_stacks_inside_invariant:
forall stk stk'
f'
ctx sp'
rs1,
match_stacks_inside F m m'
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'
stk stk'
f'
ctx sp'
rs2.
Proof.
induction 1;
intros.
apply match_stacks_nil with (
bound1 :=
bound1).
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;
extlia.
intros;
eapply PERM1;
eauto;
extlia.
intros;
eapply PERM2;
eauto;
extlia.
intros;
eapply PERM3;
eauto;
extlia.
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;
extlia.
intros;
eapply PERM1;
eauto;
extlia.
intros;
eapply PERM2;
eauto;
extlia.
intros;
eapply PERM3;
eauto;
extlia.
eapply range_private_invariant;
eauto.
induction 1;
intros.
eapply match_stacks_inside_base;
eauto.
eapply match_stacks_invariant;
eauto.
intros;
eapply INJ;
eauto;
extlia.
intros;
eapply PERM1;
eauto;
extlia.
intros;
eapply PERM2;
eauto;
extlia.
intros;
eapply PERM3;
eauto;
extlia.
apply match_stacks_inside_inlined with (
fenv :=
fenv) (
ctx' :=
ctx');
auto.
apply IHmatch_stacks_inside;
auto.
intros.
apply RS.
red in BELOW.
extlia.
apply agree_regs_incr with F;
auto.
apply agree_regs_invariant with rs';
auto.
intros.
apply RS.
red in BELOW.
extlia.
eapply range_private_invariant;
eauto.
intros.
split.
eapply INJ;
eauto.
extlia.
eapply PERM1;
eauto.
extlia.
intros.
eapply PERM2;
eauto.
extlia.
Qed.
Lemma match_stacks_empty:
forall stk stk'
bound,
match_stacks F m m'
stk stk'
bound ->
stk =
nil ->
stk' =
nil
with match_stacks_inside_empty:
forall stk stk'
f ctx sp rs,
match_stacks_inside F m m'
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.
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,
match_stacks_inside F m m'
stk stk'
f'
ctx sp'
rs' ->
match_stacks_inside F m m'
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,
match_stacks_inside F m m'
stk stk'
f'
ctx sp'
rs' ->
match_stacks_inside F m m'
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',
match_stacks_inside F m m'
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'
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',
match_stacks_inside F m m'
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'
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,
match_stacks F m m'
stk stk'
sp ->
Mem.free m b lo hi =
Some m1 ->
match_stacks F m1 m'
stk stk'
sp.
Proof.
Lemma match_stacks_free_right:
forall F m m'
stk stk'
sp lo hi m1',
match_stacks F m m'
stk stk'
sp ->
Mem.free m'
sp lo hi =
Some m1' ->
match_stacks F m m1'
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).
extlia.
destruct (
zle sz 2).
auto.
destruct (
zle sz 4).
apply Z.divide_trans with 4;
auto.
exists 2;
auto.
apply Z.divide_trans with 8;
auto.
exists 4;
auto.
assert (4 <=
sz -> (4 |
n)).
intros.
destruct (
zle sz 1).
extlia.
destruct (
zle sz 2).
extlia.
destruct (
zle sz 4).
auto.
apply Z.divide_trans with 8;
auto.
exists 2;
auto.
assert (8 <=
sz -> (8 |
n)).
intros.
destruct (
zle sz 1).
extlia.
destruct (
zle sz 2).
extlia.
destruct (
zle sz 4).
extlia.
auto.
destruct chunk;
simpl in *;
auto.
apply Z.divide_1_l.
apply Z.divide_1_l.
apply H2;
lia.
apply H2;
lia.
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,
match_stacks F1 m1 m1'
stk stk'
bound ->
Ple bound (
Mem.nextblock m1') ->
match_stacks F2 m2 m2'
stk stk'
bound
with match_stacks_inside_extcall:
forall stk stk'
f'
ctx sp'
rs',
match_stacks_inside F1 m1 m1'
stk stk'
f'
ctx sp'
rs' ->
Plt sp' (
Mem.nextblock m1') ->
match_stacks_inside F2 m2 m2'
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).
lia.
lia.
Qed.
Lemma match_stacks_inside_inlined_tailcall:
forall fenv F m m'
stk stk'
f'
ctx sp'
rs'
ctx'
f,
match_stacks_inside F m m'
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) ->
tr_funbody fenv f'.(
fn_stacksize)
ctx'
f f'.(
fn_code) ->
match_stacks_inside F m m'
stk stk'
f'
ctx'
sp'
rs'.
Proof.
Relating states
Inductive match_states:
RTL.state ->
RTL.state ->
Prop :=
|
match_regular_states:
forall stk f sp pc rs m stk'
f'
sp'
rs'
m'
F fenv ctx
(
MS:
match_stacks_inside F m m'
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')
|
match_call_states:
forall stk fd args m stk'
fd'
args'
m'
cunit F
(
MS:
match_stacks F m m'
stk stk' (
Mem.nextblock m'))
(
LINK:
linkorder cunit prog)
(
FD:
transf_fundef (
funenv_program cunit)
fd =
OK fd')
(
VINJ:
Val.inject_list F args args')
(
MINJ:
Mem.inject F m m'),
match_states (
Callstate stk fd args m)
(
Callstate stk'
fd'
args'
m')
|
match_call_regular_states:
forall stk f vargs m stk'
f'
sp'
rs'
m'
F fenv ctx ctx'
pc'
pc1'
rargs
(
MS:
match_stacks_inside F m m'
stk stk'
f'
ctx sp'
rs')
(
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 (
Internal f)
vargs m)
(
State stk'
f' (
Vptr sp'
Ptrofs.zero)
pc'
rs'
m')
|
match_return_states:
forall stk v m stk'
v'
m'
F
(
MS:
match_stacks F m m'
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')
|
match_return_regular_states:
forall stk v m stk'
f'
sp'
rs'
m'
F ctx pc'
or rinfo
(
MS:
match_stacks_inside F m m'
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').
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 ge S1 t S2 ->
forall S1' (
MS:
match_states S1 S1'),
(
exists S2',
plus step tge S1'
t S2' /\
match_states S2 S2')
\/ (
measure S2 <
measure S1 /\
t =
E0 /\
match_states S2 S1')%
nat.
Proof.
Lemma transf_initial_states:
forall st1,
initial_state prog st1 ->
exists st2,
initial_state tprog st2 /\
match_states st1 st2.
Proof.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 ->
final_state st1 r ->
final_state st2 r.
Proof.
Theorem transf_program_correct:
forward_simulation (
semantics prog) (
semantics tprog).
Proof.
End INLINING.