RTL function inlining: semantic preservation
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import Inlining.
Require Import Inliningspec.
Require Import RTL.
Section INLINING.
Variable prog:
program.
Variable tprog:
program.
Hypothesis TRANSF:
transf_program prog =
OK tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Let fenv :=
funenv_program prog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
Lemma public_preserved:
forall (
s:
ident),
Genv.public_symbol tge s =
Genv.public_symbol ge s.
Proof.
Lemma varinfo_preserved:
forall b,
Genv.find_var_info tge b =
Genv.find_var_info ge b.
Proof.
Lemma functions_translated:
forall (
v:
val) (
f:
fundef),
Genv.find_funct ge v =
Some f ->
exists f',
Genv.find_funct tge v =
Some f' /\
transf_fundef fenv f =
OK f'.
Proof (
Genv.find_funct_transf_partial (
transf_fundef fenv)
_ TRANSF).
Lemma function_ptr_translated:
forall (
b:
block) (
f:
fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists f',
Genv.find_funct_ptr tge b =
Some f' /\
transf_fundef fenv f =
OK f'.
Proof (
Genv.find_funct_ptr_transf_partial (
transf_fundef fenv)
_ TRANSF).
Lemma sig_function_translated:
forall f f',
transf_fundef fenv 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 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. 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 +
Zmax sz 0)
hi.
Proof.
intros;
red;
intros.
exploit (
H ofs).
generalize (
Zmax2 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 +
Zmax 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 fd',
find_function tge (
sros ctx ros)
rs' =
Some fd' /\
transf_fundef fenv fd =
OK fd'.
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 Int.zero)
m a v ->
exists v',
eval_builtin_arg tge (
fun r =>
rs'#
r) (
Vptr sp'
Int.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 Int.zero)
m al vl ->
exists vl',
eval_builtin_args tge (
fun r =>
rs'#
r) (
Vptr sp'
Int.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 ctx
(
MS:
match_stacks_inside F m m'
stk stk'
f'
ctx sp'
rs')
(
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) <
Int.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 Int.zero)
pc rs ::
stk)
(
Stackframe (
sreg ctx res)
f' (
Vptr sp'
Int.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) <
Int.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'
Int.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'
ctx sp'
rs'
ctx'
(
MS:
match_stacks_inside F m m'
stk stk'
f'
ctx'
sp'
rs')
(
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 Int.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.
nil *)
apply match_stacks_nil with (
bound1 :=
bound1).
inv MG.
constructor;
auto.
intros.
apply IMAGE with delta.
eapply INJ;
eauto.
eapply Plt_le_trans;
eauto.
auto.
auto.
cons *)
apply match_stacks_cons 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 agree_regs_incr;
eauto.
eapply range_private_invariant;
eauto.
untailcall *)
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.
base *)
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.
inlined *)
apply match_stacks_inside_inlined with (
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,
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).
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 Zone_divide.
apply Zone_divide.
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,
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).
omega.
omega.
Qed.
Lemma match_stacks_inside_inlined_tailcall:
forall 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:
state ->
state ->
Prop :=
|
match_regular_states:
forall stk f sp pc rs m stk'
f'
sp'
rs'
m'
F ctx
(
MS:
match_stacks_inside F m m'
stk stk'
f'
ctx sp'
rs')
(
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) <
Int.max_unsigned)
(
SSZ2:
forall ofs,
Mem.perm m'
sp'
ofs Max Nonempty -> 0 <=
ofs <=
f'.(
fn_stacksize)),
match_states (
State stk f (
Vptr sp Int.zero)
pc rs m)
(
State stk'
f' (
Vptr sp'
Int.zero) (
spc ctx pc)
rs'
m')
|
match_call_states:
forall stk fd args m stk'
fd'
args'
m'
F
(
MS:
match_stacks F m m'
stk stk' (
Mem.nextblock m'))
(
FD:
transf_fundef fenv 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 ctx ctx'
pc'
pc1'
rargs
(
MS:
match_stacks_inside F m m'
stk stk'
f'
ctx sp'
rs')
(
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) <
Int.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'
Int.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) <
Int.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'
Int.zero)
pc'
rs'
m').
Forward simulation
Definition measure (
S:
state) :
nat :=
match S with
|
State _ _ _ _ _ _ => 1%
nat
|
Callstate _ _ _ _ => 0%
nat
|
Returnstate _ _ _ => 0%
nat
end.
Lemma tr_funbody_inv:
forall 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.