Correctness proof for Cminor generation.
Require Import Coq.Program.Equality.
Require Import FSets.
Require Import Permutation.
Require Import Coqlib.
Require Intv.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import NormaliseSpec.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Switch.
Require Import Csharpminor.
Require Import Cminor.
Require Import Cminorgen.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import IntFacts.
Open Local Scope error_monad_scope.
Section TRANSLATION.
Variable prog:
Csharpminor.program.
Variable tprog:
program.
Hypothesis TRANSL:
transl_program prog =
OK tprog.
Let ge :
Csharpminor.genv :=
Genv.globalenv prog.
Let tge:
genv :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_transf_partial transl_fundef _ TRANSL).
Lemma function_ptr_translated:
forall (
b:
block) (
f:
Csharpminor.fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
transl_fundef f =
OK tf.
Proof (
Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).
Lemma functions_translated:
forall m (
v:
expr_sym) (
f:
Csharpminor.fundef),
Genv.find_funct m ge v =
Some f ->
exists tf,
Genv.find_funct m tge v =
Some tf /\
transl_fundef f =
OK tf.
Proof (
Genv.find_funct_transf_partial transl_fundef _ TRANSL).
Lemma varinfo_preserved:
forall b,
Genv.find_var_info tge b =
Genv.find_var_info ge b.
Proof (
Genv.find_var_info_transf_partial transl_fundef _ TRANSL).
Lemma sig_preserved_body:
forall f tf cenv size,
transl_funbody cenv size f =
OK tf ->
tf.(
fn_sig) =
Csharpminor.fn_sig f.
Proof.
Lemma sig_preserved:
forall f tf,
transl_fundef f =
OK tf ->
Cminor.funsig tf =
Csharpminor.funsig f.
Proof.
Derived properties of memory operations
Lemma perm_freelist:
forall fbl m m'
b ofs k p,
Mem.free_list m fbl =
Some m' ->
Mem.perm m'
b ofs k p ->
Mem.perm m b ofs k p.
Proof.
induction fbl;
simpl;
intros until p.
congruence.
destruct a as [[
b'
lo]
hi].
case_eq (
Mem.free m b'
lo hi);
try congruence.
intros.
eauto with mem.
Qed.
Lemma nextblock_freelist:
forall fbl m m',
Mem.free_list m fbl =
Some m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
induction fbl;
intros until m';
simpl.
congruence.
destruct a as [[
b lo]
hi].
case_eq (
Mem.free m b lo hi);
intros;
try congruence.
transitivity (
Mem.nextblock m0).
eauto.
eapply Mem.nextblock_free;
eauto.
Qed.
Lemma free_list_freeable:
forall l m m',
Mem.free_list m l =
Some m' ->
forall b lo hi,
In (
b,
lo,
hi)
l ->
Mem.range_perm m b lo hi Cur Freeable.
Proof.
induction l;
simpl;
intros.
contradiction.
revert H.
destruct a as [[
b'
lo']
hi'].
caseEq (
Mem.free m b'
lo'
hi');
try congruence.
intros m1 FREE1 FREE2.
destruct H0.
inv H.
eauto with mem.
red;
intros.
eapply Mem.perm_free_3;
eauto.
exploit IHl;
eauto.
Qed.
Lemma nextblock_storev:
forall chunk m addr v m',
Mem.storev chunk m addr v =
Some m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
Correspondence between C#minor's and Cminor's environments and memory states
In C#minor, every variable is stored in a separate memory block.
In the corresponding Cminor code, these variables become sub-blocks
of the stack data block. We capture these changes in memory via a
memory injection f:
f b = Some(b', ofs) means that C#minor block b corresponds
to a sub-block of Cminor block b at offset ofs.
A memory injection f defines a relation val_inject f between
values and a relation Mem.inject f between memory states. These
relations will be used intensively in our proof of simulation
between C#minor and Cminor executions.
Matching between Cshaprminor's temporaries and Cminor's variables
Definition match_temps (
f:
meminj) (
le:
Csharpminor.temp_env) (
te:
env) :
Prop :=
forall id v,
le!
id =
Some v ->
exists v',
te!(
id) =
Some v' /\
Val.expr_inject Mem.id_pua f v v'.
Lemma match_temps_invariant:
forall f f'
le te,
match_temps f le te ->
inject_incr f f' ->
match_temps f'
le te.
Proof.
intros;
red;
intros.
destruct (
H _ _ H1)
as [
v' [
A B]].
exists v';
split;
eauto.
eapply Val.expr_inject_incr;
eauto.
Qed.
Lemma match_temps_assign:
forall f le te id v tv,
match_temps f le te ->
Val.expr_inject Mem.id_pua f v tv ->
match_temps f (
PTree.set id v le) (
PTree.set id tv te).
Proof.
intros;
red;
intros.
rewrite PTree.gsspec in *.
destruct (
peq id0 id).
inv H1.
exists tv;
auto.
auto.
Qed.
Matching between C#minor's variable environment and Cminor's stack pointer
Inductive match_var (
f:
meminj) (
sp:
block):
option (
block *
Z) ->
option Z ->
Prop :=
|
match_var_local:
forall b sz ofs,
Val.expr_inject Mem.id_pua f (
Eval (
Eptr b Int.zero)) (
Eval (
Eptr sp (
Int.repr ofs))) ->
match_var f sp (
Some(
b,
sz)) (
Some ofs)
|
match_var_global:
match_var f sp None None.
Matching between a C#minor environment e and a Cminor
stack pointer sp. The lo and hi parameters delimit the range
of addresses for the blocks referenced from te.
Record match_env (
f:
meminj) (
cenv:
compilenv)
(
e:
Csharpminor.env) (
sp:
block)
(
lo hi:
block) :
Prop :=
mk_match_env {
C#minor local variables match sub-blocks of the Cminor stack data block.
me_vars:
forall id,
match_var f sp (
e!
id) (
cenv!
id);
lo, hi is a proper interval.
me_low_high:
Ple lo hi;
Every block appearing in the C#minor environment e must be
in the range lo, hi.
me_bounded:
forall id b sz,
PTree.get id e =
Some(
b,
sz) ->
Ple lo b /\
Plt b hi;
All blocks mapped to sub-blocks of the Cminor stack data must be
images of variables from the C#minor environment e
me_inv:
forall b delta,
f b =
Some(
sp,
delta) ->
exists id,
exists sz,
PTree.get id e =
Some(
b,
sz);
All C#minor blocks below lo (i.e. allocated before the blocks
referenced from e) must map to blocks that are below sp
(i.e. allocated before the stack data for the current Cminor function).
me_incr:
forall b tb delta,
f b =
Some(
tb,
delta) ->
Plt b lo ->
Plt tb sp
}.
Ltac geninv x :=
let H :=
fresh in (
generalize x;
intro H;
inv H).
Lemma match_env_invariant:
forall f1 cenv e sp lo hi f2,
match_env f1 cenv e sp lo hi ->
inject_incr f1 f2 ->
(
forall b delta,
f2 b =
Some(
sp,
delta) ->
f1 b =
Some(
sp,
delta)) ->
(
forall b,
Plt b lo ->
f2 b =
f1 b) ->
match_env f2 cenv e sp lo hi.
Proof.
intros.
destruct H.
constructor;
auto.
-
intros.
geninv (
me_vars0 id);
econstructor;
eauto.
eapply Val.expr_inject_incr;
eauto.
-
intros.
eauto.
-
intros.
rewrite H2 in H;
eauto.
Qed.
match_env and external calls
Remark inject_incr_separated_same:
forall f1 f2 m1 m1',
inject_incr f1 f2 ->
inject_separated f1 f2 m1 m1' ->
forall b,
Mem.valid_block m1 b ->
f2 b =
f1 b.
Proof.
intros. case_eq (f1 b).
intros [b' delta] EQ. apply H; auto.
intros EQ. case_eq (f2 b).
intros [b'1 delta1] EQ1. exploit H0; eauto. intros [C D]. contradiction.
auto.
Qed.
Remark inject_incr_separated_same':
forall f1 f2 m1 m1',
inject_incr f1 f2 ->
inject_separated f1 f2 m1 m1' ->
forall b b'
delta,
f2 b =
Some(
b',
delta) ->
Mem.valid_block m1'
b' ->
f1 b =
Some(
b',
delta).
Proof.
intros. case_eq (f1 b).
intros [b'1 delta1] EQ. exploit H; eauto. congruence.
intros. exploit H0; eauto. intros [C D]. contradiction.
Qed.
Lemma match_env_external_call:
forall f1 cenv e sp lo hi f2 m1 m1',
match_env f1 cenv e sp lo hi ->
inject_incr f1 f2 ->
inject_separated f1 f2 m1 m1' ->
Ple hi (
Mem.nextblock m1) ->
Plt sp (
Mem.nextblock m1') ->
match_env f2 cenv e sp lo hi.
Proof.
match_env and allocations
The sizes of blocks appearing in e are respected.
Definition match_bounds (
e:
Csharpminor.env) (
m:
mem) :
Prop :=
forall id b sz ofs p,
PTree.get id e =
Some(
b,
sz) ->
Mem.perm m b ofs Max p -> 0 <=
ofs <
sz.
Definition match_bounds' (
e:
Csharpminor.env) (
m:
mem) :
Prop :=
forall id b sz,
PTree.get id e =
Some(
b,
sz) ->
Mem.bounds_of_block m b = (0,
sz).
Lemma match_bounds_invariant:
forall e m1 m2,
match_bounds e m1 ->
(
forall id b sz ofs p,
PTree.get id e =
Some(
b,
sz) ->
Mem.perm m2 b ofs Max p ->
Mem.perm m1 b ofs Max p) ->
match_bounds e m2.
Proof.
intros; red; intros. eapply H; eauto.
Qed.
Lemma match_bounds'
_invariant:
forall e m1 m2,
match_bounds'
e m1 ->
(
forall id b sz,
PTree.get id e =
Some(
b,
sz) ->
Mem.bounds_of_block m1 b =
Mem.bounds_of_block m2 b) ->
match_bounds'
e m2.
Proof.
intros; red; intros. erewrite <- H0; eauto.
Qed.
Permissions on the Cminor stack block
The parts of the Cminor stack data block that are not images of
C#minor local variable blocks remain freeable at all times.
Inductive is_reachable_from_env (
f:
meminj) (
e:
Csharpminor.env) (
sp:
block) (
ofs:
Z) :
Prop :=
|
is_reachable_intro:
forall id b sz delta,
e!
id =
Some(
b,
sz) ->
f b =
Some(
sp,
delta) ->
delta <=
ofs <
delta +
sz ->
is_reachable_from_env f e sp ofs.
Definition padding_freeable (
f:
meminj) (
e:
Csharpminor.env) (
tm:
mem) (
sp:
block) (
sz:
Z) :
Prop :=
forall ofs,
0 <=
ofs <
sz ->
Mem.perm tm sp ofs Cur Freeable \/
is_reachable_from_env f e sp ofs.
Lemma padding_freeable_invariant:
forall f1 e tm1 sp sz cenv lo hi f2 tm2,
padding_freeable f1 e tm1 sp sz ->
match_env f1 cenv e sp lo hi ->
(
forall ofs,
Mem.perm tm1 sp ofs Cur Freeable ->
Mem.perm tm2 sp ofs Cur Freeable) ->
(
forall b,
Plt b hi ->
f2 b =
f1 b) ->
padding_freeable f2 e tm2 sp sz.
Proof.
intros;
red;
intros.
exploit H;
eauto.
intros [
A |
A].
left;
auto.
right.
inv A.
exploit me_bounded;
eauto.
intros [
D E].
econstructor;
eauto.
rewrite H2;
auto.
Qed.
Decidability of the is_reachable_from_env predicate.
Lemma is_reachable_from_env_dec:
forall f e sp ofs,
is_reachable_from_env f e sp ofs \/ ~
is_reachable_from_env f e sp ofs.
Proof.
Correspondence between global environments
Global environments match if the memory injection f leaves unchanged
the references to global symbols and functions.
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).
Remark inj_preserves_globals:
forall f hi,
match_globalenvs f hi ->
meminj_preserves_globals ge f.
Proof.
intros. inv H.
split. intros. apply DOMAIN. eapply SYMBOLS. eauto.
split. intros. apply DOMAIN. eapply VARINFOS. eauto.
intros. symmetry. eapply IMAGE; eauto.
Qed.
Invariant on abstract call stacks
Call stacks represent abstractly the execution state of the current
C#minor and Cminor functions, as well as the states of the
calling functions. A call stack is a list of frames, each frame
collecting information on the current execution state of a C#minor
function and its Cminor translation.
Inductive frame :
Type :=
Frame(
cenv:
compilenv)
(
tf:
Cminor.function)
(
e:
Csharpminor.env)
(
le:
Csharpminor.temp_env)
(
te:
Cminor.env)
(
sp:
block)
(
lo hi:
block).
Definition callstack :
Type :=
list frame.
Matching of call stacks imply:
-
matching of environments for each of the frames
-
matching of the global environments
-
separation conditions over the memory blocks allocated for C#minor local variables;
-
separation conditions over the memory blocks allocated for Cminor stack data;
-
freeable permissions on the parts of the Cminor stack data blocks
that are not images of C#minor local variable blocks.
:=
list_norepet (
map fst (
map fst (
blocks_of_env e))).
Definition small_var_space (
vars:
list (
ident*
Z))
start :=
fold_right (
fun y x =>
align x (
block_alignment (
snd y)) +
Z.max 0 (
snd y))
start vars.
Lemma align_plus:
forall z sz,
align (
align z (
block_alignment sz)) 8 =
align z 8.
Proof.
Lemma block_alignment_pos:
forall sz,
block_alignment sz > 0.
Proof.
Lemma fr_align_pos:
forall vars z,
z >= 0 ->
small_var_space vars z >=
z.
Proof.
Definition big_var_space (
vars:
list (
ident*
Z))
start :=
fold_right (
fun y x =>
align x 8 +
Z.max 0 (
snd y))
start vars.
Lemma fr_align_pos8:
forall vars z,
z >= 0 ->
big_var_space vars z >=
z.
Proof.
Lemma sp_le_vars_right:
forall vars ,
small_var_space vars 0 <=
big_var_space vars 0.
Proof.
Definition big_vars_block_space (
vars:
list (
block*
Z*
Z))
start :=
fold_right
(
fun (
y :
block *
Z *
Z) (
x :
Z) =>
align x 8 +
Z.max 0 (
snd y -
snd (
fst y)))
start vars.
Lemma bvbs_rew:
forall vars start,
big_vars_block_space vars start =
big_var_space (
map (
fun a => (
fst (
fst a),
snd a -
snd (
fst a)))
vars)
start.
Proof.
induction vars; simpl; intros;
congruence.
Qed.
Lemma fr_permut:
forall l l'
z,
Permutation l l' ->
align (
big_vars_block_space l z) 8 =
align (
big_vars_block_space l'
z) 8.
Proof.
induction 1;
simpl;
intros.
-
auto.
-
rewrite IHPermutation.
auto.
-
rewrite <- !
Mem.align_distr.
omega.
-
congruence.
Qed.
Lemma fr_permut':
forall (
l l':
list (
ident*
Z))
z,
Permutation l l' ->
align (
big_var_space l z) 8 =
align (
big_var_space l'
z) 8.
Proof.
induction 1;
simpl;
intros.
-
auto.
-
rewrite IHPermutation.
auto.
-
rewrite <- !
Mem.align_distr.
omega.
-
congruence.
Qed.
Lemma big_vars_block_space_left:
forall vars z,
align (
fold_left
(
fun (
x :
Z) (
y :
block *
Z *
Z) =>
align x 8 +
Z.max 0 (
snd y -
snd (
fst y)))
vars z) 8
=
align (
big_vars_block_space vars z) 8.
Proof.
Inductive match_callstack (
f:
meminj) (
m:
mem) (
tm:
mem):
callstack ->
block ->
block ->
Prop :=
|
mcs_nil:
forall hi bound tbound,
match_globalenvs f hi ->
Mem.all_blocks_injected f m ->
Ple hi bound ->
Ple hi tbound ->
match_callstack f m tm nil bound tbound
|
mcs_cons:
forall cenv tf e le te sp lo hi cs bound tbound
(
BOUND:
Ple hi bound)
(
TBOUND:
Plt sp tbound)
(
MTMP:
match_temps f le te)
(
MENV:
match_env f cenv e sp lo hi)
(
BOUND:
match_bounds e m)
(
BOUND':
match_bounds'
e m)
(
NRP:
norepet_env e)
(
hi_pos:
Forall (
fun bnds :
ident *
Z *
Z =>
snd bnds >= 0) (
blocks_of_env e))
(
sz_stack:
align (
fn_stackspace tf) 8 =
align
(
big_vars_block_space (
rev (
blocks_of_env e)) 0) 8)
(
ss_pos:
fn_stackspace tf >= 0)
(
PERM:
padding_freeable f e tm sp (
align (
fn_stackspace tf) 8))
(
bnd_sp:
Mem.bounds_of_block tm sp = (0,
align (
fn_stackspace tf) 8))
(
MCS:
match_callstack f m tm cs lo sp),
match_callstack f m tm (
Frame cenv tf e le te sp lo hi ::
cs)
bound tbound.
match_callstack implies match_globalenvs.
Lemma match_callstack_match_globalenvs:
forall f m tm cs bound tbound,
match_callstack f m tm cs bound tbound ->
exists hi,
match_globalenvs f hi.
Proof.
induction 1; eauto.
Qed.
Lemma match_callstack_all_blocks_injected:
forall f m tm cs mm sp,
match_callstack f m tm cs mm sp ->
Mem.all_blocks_injected f m.
Proof.
induction 1; auto.
Qed.
Invariance properties for match_callstack.
Lemma match_callstack_invariant:
forall f1 m1 tm1 f2 m2 tm2 cs bound tbound
(
MCS:
match_callstack f1 m1 tm1 cs bound tbound)
(
INCR:
inject_incr f1 f2)
(
PRM:
forall b ofs p,
Plt b bound ->
Mem.perm m2 b ofs Max p ->
Mem.perm m1 b ofs Max p)
(
BND:
forall b,
Plt b bound ->
Mem.bounds_of_block m2 b =
Mem.bounds_of_block m1 b)
(
BND':
forall b,
Plt b tbound ->
Mem.bounds_of_block tm2 b =
Mem.bounds_of_block tm1 b)
(
PRM':
forall sp ofs,
Plt sp tbound ->
Mem.perm tm1 sp ofs Cur Freeable ->
Mem.perm tm2 sp ofs Cur Freeable)
(
Fsame:
forall b,
Plt b bound ->
f2 b =
f1 b)
(
Fsame':
forall b b'
delta,
f2 b =
Some(
b',
delta) ->
Plt b'
tbound ->
f1 b =
Some(
b',
delta))
(
ABI:
Mem.all_blocks_injected f2 m2),
match_callstack f2 m2 tm2 cs bound tbound.
Proof.
induction 1;
intros.
-
apply (
mcs_nil _ _ _ hi bound tbound);
auto.
+
inv H.
constructor;
intros;
eauto.
eapply IMAGE;
eauto.
eapply Fsame';
eauto.
xomega.
-
assert (
Ple lo hi)
by (
eapply me_low_high;
eauto).
econstructor;
eauto.
+
eapply match_temps_invariant;
eauto.
+
eapply match_env_invariant;
eauto.
intros.
apply Fsame.
xomega.
+
eapply match_bounds_invariant;
eauto.
intros.
eapply PRM;
eauto.
exploit me_bounded;
eauto.
xomega.
+
eapply match_bounds'
_invariant;
eauto.
intros.
erewrite <-
BND;
eauto.
exploit me_bounded;
eauto.
xomega.
+
eapply padding_freeable_invariant;
eauto.
intros.
apply Fsame.
xomega.
+
rewrite <-
bnd_sp.
apply BND'.
xomega.
+
eapply IHMCS;
eauto.
*
intros.
eapply PRM;
eauto.
xomega.
*
intros.
eapply BND;
eauto.
xomega.
*
intros.
eapply BND';
eauto.
xomega.
*
intros.
eapply PRM';
eauto.
xomega.
*
intros.
eapply Fsame;
eauto.
xomega.
*
intros.
eapply Fsame';
eauto.
xomega.
Qed.
Lemma match_callstack_incr_bound:
forall f m tm cs bound tbound bound'
tbound',
match_callstack f m tm cs bound tbound ->
Ple bound bound' ->
Ple tbound tbound' ->
match_callstack f m tm cs bound'
tbound'.
Proof.
intros. inv H.
econstructor; eauto. xomega. xomega.
econstructor; auto. xomega. xomega.
Qed.
Assigning a temporary variable.
Lemma match_callstack_set_temp:
forall f cenv e le te sp lo hi cs bound tbound m tm tf id v tv,
Val.expr_inject Mem.id_pua f v tv ->
match_callstack f m tm (
Frame cenv tf e le te sp lo hi ::
cs)
bound tbound ->
match_callstack f m tm (
Frame cenv tf e (
PTree.set id v le) (
PTree.set id tv te)
sp lo hi ::
cs)
bound tbound.
Proof.
Preservation of match_callstack by freeing all blocks allocated
for local variables at function entry (on the C#minor side)
and simultaneously freeing the Cminor stack data block.
Lemma in_blocks_of_env:
forall e id b sz,
e!
id =
Some(
b,
sz) ->
In (
b, 0,
sz) (
blocks_of_env e).
Proof.
Lemma in_blocks_of_env_inv:
forall b lo hi e,
In (
b,
lo,
hi) (
blocks_of_env e) ->
exists id,
e!
id =
Some(
b,
hi) /\
lo = 0.
Proof.
Lemma alloc_variables_alloc_sp:
forall fn tf,
transl_function fn =
OK tf ->
fn_stackspace tf =
big_var_space (
rev (
VarSort.sort (
Csharpminor.fn_vars fn))) 0.
Proof.
Ltac trim H :=
match type of H with
?
A -> ?
B =>
let x:=
fresh in
assert (
x:
A); [
clear H|
specialize (
H x);
clear x]
end.
Lemma size_mem_blocks_rew:
forall l z,
align (
Mem.size_mem_blocks l z) 8 =
align z 8 +
align (
Mem.size_mem_blocks l 0) 8.
Proof.
induction l;
simpl;
intros;
auto.
change (
align 0 8)
with 0.
omega.
rewrite IHl at 1.
rewrite <-
Mem.align_distr.
rewrite <-
Z.add_assoc.
f_equal.
rewrite <-
IHl.
auto.
Qed.
Lemma size_mem_blocks_big_vars:
forall vars z,
Mem.size_mem_blocks vars z =
big_vars_block_space (
rev vars)
z.
Proof.
Lemma freelist_free_size_mem:
forall m m'
tm tm'
sp e tf
(
vars_norepet:
list_norepet (
map fst (
map fst (
blocks_of_env e))))
(
exact_bounds:
Forall
(
fun bbnds :
ident *
Z *
Z =>
Mem.bounds_of_block m (
fst (
fst bbnds)) =
(
snd (
fst bbnds),
snd bbnds)) (
blocks_of_env e))
(
FREELIST :
Mem.free_list m (
blocks_of_env e) =
Some m')
(
SP_bnds :
Mem.bounds_of_block tm sp = (0,
align (
fn_stackspace tf) 8))
(
FREE :
Mem.free tm sp 0 (
align (
fn_stackspace tf) 8) =
Some tm')
(
ss_eq:
align (
fn_stackspace tf) 8 =
align (
big_vars_block_space (
rev (
blocks_of_env e)) 0) 8)
(
ss_pos:
fn_stackspace tf >= 0)
(
hi_pos:
Forall (
fun bnds:
ident *
Z *
Z =>
snd bnds >= 0) (
blocks_of_env e))
(
mi_size_mem :
Mem.size_mem tm <=
Mem.size_mem m),
Mem.size_mem tm' <=
Mem.size_mem m'.
Proof.
Lemma freelist_inject:
forall f m tm e m'
sp tf tm'
(
MI:
Mem.inject Mem.id_pua f m tm)
(
nr:
list_norepet (
map fst (
map fst (
blocks_of_env e))))
(
exact_bounds:
Forall
(
fun bbnds :
ident *
Z *
Z =>
Mem.bounds_of_block m (
fst (
fst bbnds)) = (
snd (
fst bbnds),
snd bbnds))
(
blocks_of_env e))
(
ss_eq:
align (
fn_stackspace tf) 8 =
align (
big_vars_block_space (
rev (
blocks_of_env e)) 0) 8)
(
ss_pos:
fn_stackspace tf >= 0)
(
hi_pos:
Forall (
fun bnds :
ident *
Z *
Z =>
snd bnds >= 0) (
blocks_of_env e))
(
INJ_not_in_sp:
forall b b'
delta,
~
In b (
map (
fun a =>
fst (
fst a)) (
blocks_of_env e)) ->
f b =
Some (
b',
delta) ->
b' <>
sp)
(
NOPERM:
forall b,
In b (
map (
fun a =>
fst (
fst a)) (
blocks_of_env e)) ->
forall k p ofs,
~
Mem.perm m'
b ofs k p)
(
NOBOUND:
forall b,
In b (
map (
fun a =>
fst (
fst a)) (
blocks_of_env e)) ->
Mem.bounds_of_block m'
b = (0,0))
(
NOMASK:
forall b,
In b (
map (
fun a =>
fst (
fst a)) (
blocks_of_env e)) ->
Mem.mask m'
b =
O)
(
FREELIST:
Mem.free_list m (
blocks_of_env e) =
Some m')
(
SP_bnds:
Mem.bounds_of_block tm sp = (0,
align (
fn_stackspace tf) 8))
(
FREE:
Mem.free tm sp 0 (
align (
fn_stackspace tf) 8) =
Some tm'),
Mem.inject Mem.id_pua f m'
tm'.
Proof.
Lemma exact_bounds_perm_free_list:
forall e m m'
(
BOUNDS:
forall b lo hi,
In (
b,
lo,
hi)
e ->
Mem.bounds_of_block m b = (
lo,
hi))
(
LNR:
list_norepet (
map (
fun a =>
fst (
fst a))
e))
(
FREELIST:
Mem.free_list m e =
Some m'),
forall b,
In b (
map (
fun a =>
fst (
fst a))
e) ->
Mem.bounds_of_block m'
b = (0,0)
/\
Mem.mask m'
b =
O.
Proof.
Lemma exact_bounds_free_list:
forall e m m'
(
BOUNDS:
forall b lo hi,
In (
b,
lo,
hi)
e ->
Mem.bounds_of_block m b = (
lo,
hi))
(
LNR:
list_norepet (
map (
fun a =>
fst (
fst a))
e))
(
FREELIST:
Mem.free_list m e =
Some m'),
forall b,
In b (
map (
fun a =>
fst (
fst a))
e) ->
Mem.bounds_of_block m'
b = (0,0) /\
(
forall k p ofs,
~
Mem.perm m'
b ofs k p) /\
Mem.mask m'
b =
O.
Proof.
Lemma match_callstack_freelist_aux:
forall f cenv tf e le te sp lo hi cs m m'
tm
(
NOBOUND:
forall b,
In b (
map (
fun a =>
fst (
fst a)) (
blocks_of_env e)) ->
Mem.bounds_of_block m'
b = (0,0))
(
NOPERM:
forall b,
In b (
map (
fun a =>
fst (
fst a)) (
blocks_of_env e)) ->
forall k p ofs,
~
Mem.perm m'
b ofs k p) ,
Mem.inject Mem.id_pua f m tm ->
Mem.free_list m (
blocks_of_env e) =
Some m' ->
Mem.bounds_of_block tm sp = (0,
align (
fn_stackspace tf) 8) ->
match_callstack f m tm (
Frame cenv tf e le te sp lo hi ::
cs) (
Mem.nextblock m) (
Mem.nextblock tm) ->
exists tm',
Mem.free tm sp 0 (
align (
tf.(
fn_stackspace)) 8) =
Some tm'
/\
match_callstack f m'
tm'
cs (
Mem.nextblock m') (
Mem.nextblock tm')
/\
Mem.inject Mem.id_pua f m'
tm'.
Proof.
Lemma mcs_norepet_env:
forall f m tm cenv tf le te sp lo hi cs e
(
MCS:
match_callstack f m tm (
Frame cenv tf e le te sp lo hi ::
cs) (
Mem.nextblock m) (
Mem.nextblock tm)),
list_norepet (
map (
fun a =>
fst (
fst a)) (
blocks_of_env e)).
Proof.
Lemma match_callstack_freelist:
forall f cenv tf e le te sp lo hi cs m m'
tm
(
BOUNDS:
forall b lo hi,
In (
b,
lo,
hi) (
blocks_of_env e) ->
Mem.bounds_of_block m b = (
lo,
hi))
(
BOUNDSsp:
Mem.bounds_of_block tm sp = (0,
align (
fn_stackspace tf) 8)),
Mem.inject Mem.id_pua f m tm ->
Mem.free_list m (
blocks_of_env e) =
Some m' ->
match_callstack f m tm (
Frame cenv tf e le te sp lo hi ::
cs) (
Mem.nextblock m) (
Mem.nextblock tm) ->
exists tm',
Mem.free tm sp 0 (
align (
tf.(
fn_stackspace)) 8) =
Some tm'
/\
match_callstack f m'
tm'
cs (
Mem.nextblock m') (
Mem.nextblock tm')
/\
Mem.inject Mem.id_pua f m'
tm'.
Proof.
Correctness of stack allocation of local variables
This section shows the correctness of the translation of
Csharpminor local variables as sub-blocks of the Cminor stack data.
This is the most difficult part of the proof.
Definition cenv_compat (
cenv:
compilenv) (
vars:
list (
ident *
Z)) (
tsz:
Z) :
Prop :=
forall id sz,
In (
id,
sz)
vars ->
exists ofs,
PTree.get id cenv =
Some ofs
/\
Mem.inj_offset_aligned ofs sz
/\ 0 <=
ofs
/\
ofs +
Zmax 0
sz <=
tsz.
Definition cenv_separated (
cenv:
compilenv) (
vars:
list (
ident *
Z)) :
Prop :=
forall id1 sz1 ofs1 id2 sz2 ofs2,
In (
id1,
sz1)
vars ->
In (
id2,
sz2)
vars ->
PTree.get id1 cenv =
Some ofs1 ->
PTree.get id2 cenv =
Some ofs2 ->
id1 <>
id2 ->
ofs1 +
sz1 <=
ofs2 \/
ofs2 +
sz2 <=
ofs1.
Definition cenv_mem_separated (
cenv:
compilenv) (
vars:
list (
ident *
Z)) (
f:
meminj) (
sp:
block) (
m:
mem) :
Prop :=
forall id sz ofs b delta ofs'
k p,
In (
id,
sz)
vars ->
PTree.get id cenv =
Some ofs ->
f b =
Some (
sp,
delta) ->
Mem.perm m b ofs'
k p ->
ofs <=
ofs' +
delta <
sz +
ofs ->
False.
Inductive alloc_variables_right :
Csharpminor.env ->
mem ->
list (
ident *
Z)
->
Csharpminor.env ->
mem ->
Prop :=
alloc_variables_right_nil :
forall (
e :
Csharpminor.env) (
m :
mem),
alloc_variables_right e m nil e m
|
alloc_variables_right_cons :
forall (
e :
PTree.t (
block *
Z))
(
m :
mem) (
id :
positive)
(
sz :
Z) (
vars :
list (
ident *
Z))
(
m1 :
mem) (
b1 :
block)
(
m2 :
mem) (
e2 :
Csharpminor.env),
Mem.alloc m1 0 (
Z.max 0
sz) =
Some (
m2,
b1) ->
alloc_variables_right (
PTree.set id (
b1, (
Z.max 0
sz))
e)
m vars
e2 m1 ->
alloc_variables_right e m ((
id,
sz) ::
vars)
e2 m2.
Lemma alloc_one_more_sizes':
forall tm1 tm2 tm2'
m0 m2 b1 sp sp'
size_vars
sz
(
Hofs:
sz +
align size_vars 8 <=
Int.max_unsigned)
(
Zsizepos:
size_vars >= 0)
(
ALLOC_vars:
Mem.alloc tm1 0 (
align size_vars 8) =
Some (
tm2,
sp))
(
ALLOC_new_var:
Mem.alloc m0 0
sz =
Some (
m2,
b1))
(
ALLOC_all:
Mem.alloc tm1 0 (
align size_vars 8 +
align (
Z.max 0
sz) 8) =
Some (
tm2',
sp'))
(
sizes:
Mem.size_mem tm2 <=
Mem.size_mem m0),
Mem.size_mem tm2' <=
Mem.size_mem m2.
Proof.
intros.
apply Mem.alloc_size_mem'
in ALLOC_new_var.
apply Mem.alloc_size_mem'
in ALLOC_vars.
apply Mem.alloc_size_mem'
in ALLOC_all.
rewrite ALLOC_all in *.
rewrite ALLOC_new_var in *.
rewrite ALLOC_vars in *.
rewrite Zmax_r.
rewrite (
Z.add_comm (
align _ _)).
rewrite <-
Mem.align_distr.
rewrite Zmax_r in sizes.
subst.
omega.
transitivity size_vars;
try omega.
apply align_le;
omega.
subst.
generalize (
Zmax_bound_l 0 0
sz)
(
align_le (
Z.max 0
sz) 8)
(
align_le size_vars 8).
omega.
Qed.
Lemma nat_ge_le:
forall n m,
(
m >=
n)%
nat ->
(
n <=
m)%
nat.
Proof.
intros; omega.
Qed.
Lemma alloc_one_more:
forall tm1 tm2 tm2'
m0 m2 b1 sp sp'
f2 ofs
size_vars
sz
(
Hofs:
align (
Z.max 0
sz) 8 +
align size_vars 8 <=
Int.max_unsigned)
(
Zsizepos:
size_vars >= 0)
(
ALLOC_vars:
Mem.alloc tm1 0 (
align size_vars 8) =
Some (
tm2,
sp))
(
ALLOC_new_var:
Mem.alloc m0 0 (
Z.max 0
sz) =
Some (
m2,
b1))
(
MI:
Mem.inject Mem.id_pua f2 m0 tm2)
(
ALLOC_all:
Mem.alloc tm1 0 (
align size_vars 8 +
align (
Z.max 0
sz) 8)
=
Some (
tm2',
sp'))
(
overlap:
forall b delta,
f2 b =
Some (
sp,
delta) ->
delta +
Mem.size_block m0 b <=
ofs
)
(
ofsInf: 0 <=
ofs <=
size_vars),
Mem.inject Mem.id_pua
(
fun bb :
positive =>
if peq bb b1
then Some (
sp',
align ofs (
block_alignment sz))
else f2 bb)
m2 tm2'.
Proof.
Lemma alloc_variables_nextblock:
forall vars e1 m1 e m2,
alloc_variables_right e1 m1 vars e m2 ->
Ple (
Mem.nextblock m1) (
Mem.nextblock m2).
Proof.
induction vars;
simpl;
intros e1 m1 e m2 AVR.
inv AVR;
xomega.
inv AVR.
apply IHvars in H6.
apply Mem.nextblock_alloc in H3.
rewrite H3.
xomega.
Qed.
Lemma alloc_in_vars'':
forall vars e1 e m1 m2
(
AVR:
alloc_variables_right e1 m1 vars e m2),
forall id p,
e1!
id =
Some p ->
e!
id <>
None.
Proof.
induction vars;
simpl;
intros;
inv AVR.
-
congruence.
-
specialize (
IHvars _ _ _ _ H7 id).
revert IHvars.
rewrite PTree.gsspec.
destruct (
peq id id0);
subst;
auto.
intro A;
apply (
A _ eq_refl).
intro A;
apply (
A _ H).
Qed.
Lemma alloc_in_vars':
forall vars e1 e m1 m2
(
AVR:
alloc_variables_right e1 m1 vars e m2)
(
LNR:
list_norepet (
map fst vars))
(
He1:
forall id,
In id (
map fst vars) ->
e1 !
id =
None),
forall id p,
e1!
id =
Some p ->
e!
id =
Some p.
Proof.
induction vars;
simpl;
intros;
inv AVR.
-
congruence.
-
eapply IHvars;
eauto.
inv LNR;
auto.
intros.
specialize (
He1 id1 (
or_intror H0)).
inv LNR.
rewrite PTree.gso;
auto.
congruence.
inv LNR.
rewrite PTree.gsspec.
destruct (
peq id id0);
subst;
auto.
specialize (
He1 id0 (
or_introl eq_refl)).
congruence.
Qed.
Lemma alloc_in_vars_domain:
forall vars e1 e m1 m2
(
AVR:
alloc_variables_right e1 m1 vars e m2)
(
LNT:
list_norepet (
map fst vars))
(
He1:
forall id,
In id (
map fst vars) ->
e1 !
id =
None),
forall id b z,
e1!
id =
None ->
e!
id =
Some (
b,
z) ->
exists z',
Z.max 0
z' =
z /\
In (
id,
z')
vars.
Proof.
induction vars;
simpl;
intros;
inv AVR.
-
congruence.
-
inv LNT.
assert (
forall id1 :
ident,
In id1 (
map fst vars) -> (
PTree.set id0 (
b1,
Z.max 0
sz)
e1) !
id1 =
None).
intros;
rewrite PTree.gso by congruence;
auto.
specialize (
IHvars _ _ _ _ H8 H4 H1 id b z ).
rewrite PTree.gsspec in IHvars.
destruct (
peq id id0);
simpl;
subst;
auto.
apply (
alloc_in_vars')
with (
id:=
id0) (
p:=(
b1,
Z.max 0
sz))
in H8;
auto.
rewrite H8 in H0;
inv H0;
auto.
exists sz.
split;
auto.
apply PTree.gss.
destruct IHvars as [
z' [
A B]];
auto.
exists z';
auto.
Qed.
Record inject_incr_cs (
f1 f2:
meminj) (
sp:
block) (
m1:
mem) (
e:
Csharpminor.env) (
cenv:
compilenv) :
Prop :=
{
inj_incr:
inject_incr f1 f2;
inj_same_thr:
forall b :
positive,
Plt b (
Mem.nextblock m1) ->
f2 b =
f1 b;
inj_above_thr_tm:
forall (
b b' :
block) (
delta :
Z),
f2 b =
Some (
b',
delta) ->
Plt b'
sp ->
f1 b =
Some (
b',
delta);
inj_env:
forall id b z ofs,
e!
id =
Some (
b,
z) ->
cenv!
id =
Some ofs ->
f2 b =
Some (
sp,
ofs);
inj_env_ex:
forall (
b :
block) (
delta :
Z),
f2 b =
Some (
sp,
delta) ->
exists (
id :
positive) (
sz :
Z),
e !
id =
Some (
b,
sz)
}.
Definition nodbl (
e:
Csharpminor.env) :=
forall id b sz,
e !
id =
Some (
b,
sz) ->
~ (
exists id'
p,
id' <>
id /\
e!
id' =
Some p /\
fst p =
b).
Lemma assign_variables_not_in:
forall l t z id0,
~
In id0 (
map fst l) ->
(
fst (
assign_variables (
t,
z)
l)) !
id0 =
t !
id0.
Proof.
Lemma assign_variables_fold_left:
forall l t z id0 sz,
(
fst (
assign_variables (
t,
z) (
l ++ (
id0,
sz) ::
nil))) !
id0 =
Some (
align
(
small_var_space (
rev l)
z)
(
block_alignment sz)).
Proof.
Lemma alloc_variables_right_bounds:
forall vars e1 e m1 m2 id b sz
(
AVR:
alloc_variables_right e1 m1 vars e m2)
(
Iv:
In id (
map fst vars))
(
Heid:
e !
id =
Some (
b,
sz))
(
LNR:
list_norepet (
map fst vars))
(
Hnodbl:
forall id id0 b b'
sz sz',
In id (
map fst vars) ->
In id0 (
map fst vars) ->
id <>
id0 ->
e!
id =
Some (
b,
sz) ->
e!
id0 =
Some (
b',
sz') ->
b <>
b')
(
He1:
forall id,
In id (
map fst vars) ->
e1 !
id =
None
),
Mem.bounds_of_block m2 b = (0,
sz).
Proof.
induction vars;
simpl;
intros;
try
intuition congruence.
inv AVR.
destruct (
peq id0 id);
subst.
-
generalize H6;
intros.
inv LNR.
apply alloc_in_vars'
with (
id:=
id) (
p:=(
b1,
Z.max 0
sz0))
in H6;
auto.
+
rewrite Heid in H6;
inv H6.
erewrite Mem.bounds_of_block_alloc;
eauto.
+
intros.
rewrite PTree.gso by congruence.
apply He1;
auto.
+
rewrite PTree.gss;
auto.
-
destruct Iv;
subst;
simpl in *;
try congruence.
destruct (
peq b b1).
+
subst.
generalize (
He1 id0 (
or_introl eq_refl)).
generalize (
He1 id (
or_intror H)).
intros e1id e1id0.
inv LNR.
generalize Heid.
assert (
forall id1 :
ident,
In id1 (
map fst vars) ->
(
PTree.set id0 (
b1,
Z.max 0
sz0)
e1) !
id1 =
None).
{
intros.
rewrite PTree.gso.
apply He1;
auto.
congruence.
}
generalize (
alloc_in_vars'
_ _ _ _ _ H6 H4 H0) .
intro AIV.
intros.
generalize (
AIV id0 (
b1,
Z.max 0
sz0)).
rewrite PTree.gss.
destruct (
e!
id0)
eqn:?;
intuition try congruence.
inv H5.
specialize (
Hnodbl id0 id _ _ _ _ (
or_introl eq_refl) (
or_intror H)
n
Heqo Heid0).
congruence.
+
erewrite <-
Mem.bounds_of_block_alloc_other;
eauto.
eapply IHvars in H6;
eauto.
inv LNR;
auto.
intros.
rewrite PTree.gso;
auto.
inv LNR.
congruence.
Qed.
Lemma list_norepet_rev:
forall A (
l:
list A),
list_norepet l ->
list_norepet (
rev l).
Proof.
Lemma alloc_variables_right_nodbl:
forall vars e1 e m1 m2
(
AVR:
alloc_variables_right e1 m1 vars e m2)
(
LNR:
list_norepet (
map fst vars))
(
INe1:
forall id :
ident,
In id (
map fst vars) ->
e1 !
id =
None)
(
NDBL:
nodbl e1)
(
VB:
forall id b z,
e1!
id =
Some (
b,
z) -> ~
Mem.valid_block m2 b),
nodbl e.
Proof.
induction vars;
simpl;
intros;
inv AVR;
auto.
inv LNR.
specialize (
IHvars _ _ _ _ H6 H2).
apply IHvars.
-
intros.
rewrite PTree.gso by congruence.
apply INe1;
auto.
-
red;
intros.
intros [
id' [[
i j] [
A [
B C]]]];
simpl in *.
subst.
red in NDBL.
revert H B.
rewrite !
PTree.gsspec.
repeat destruct peq;
subst;
intuition try congruence.
+
inv H.
generalize (
Mem.valid_new_block _ _ _ _ _ H3).
intro.
apply VB in B;
auto.
+
inv B.
generalize (
Mem.valid_new_block _ _ _ _ _ H3).
intro.
apply VB in H;
auto.
+
apply (
NDBL _ _ _ H).
exists id' ;
exists (
b,
j);
repeat split;
auto.
-
intros.
rewrite PTree.gsspec in H.
destruct (
peq id0 id);
subst;
auto.
inv H.
eapply Mem.fresh_block_alloc;
eauto.
intro.
generalize (
Mem.valid_block_alloc _ _ _ _ _ H3).
intro.
apply H4 in H0.
eapply VB;
eauto.
Qed.
Lemma assign_variables_in:
forall vars t o id,
In id (
map fst vars) ->
list_norepet (
map fst vars) ->
(
fst (
assign_variables (
t,
o)
vars)) !
id =
None ->
False.
Proof.
induction vars;
simpl;
intros.
auto.
unfold assign_variable in H0.
destruct a.
simpl in *.
destruct H.
subst.
rewrite assign_variables_not_in in H1.
rewrite PTree.gss in H1;
congruence.
inv H0;
auto.
apply IHvars in H1;
auto.
inv H0;
auto.
Qed.
Lemma fl_align_add:
forall l z1,
0 <=
z1 ->
z1 <=
fold_left
(
fun (
x :
Z) (
y :
positive *
Z) =>
align x (
block_alignment (
snd y)) +
Z.max 0 (
snd y))
l
z1.
Proof.
Lemma alloc_in_vars_same:
forall vars e1 e m1 m2
(
AVR:
alloc_variables_right e1 m1 vars e m2)
id
(
LNR: ~
In id (
map fst vars)),
e1!
id =
e !
id.
Proof.
induction vars;
simpl;
intros;
inv AVR;
auto.
eapply IHvars in H6;
eauto.
revert H6.
rewrite PTree.gso;
auto.
Qed.
Lemma avr_valid_before:
forall vars e1 m1 e m0
(
AVR:
alloc_variables_right e1 m1 vars e m0)
b
(
LNR:
list_norepet (
map fst vars))
(
VB:
Mem.valid_block m0 b),
Mem.valid_block m1 b \/
(
exists i z,
e !
i =
Some (
b,
z) /\
In i (
map fst vars)).
Proof.
induction 1;
simpl;
intros;
auto.
generalize H;
intro ALLOC.
apply Mem.valid_block_alloc_inv with (
b':=
b)
in ALLOC;
auto.
destruct ALLOC;
subst.
-
right;
exists id;
exists (
Z.max 0
sz);
split;
auto.
inv LNR.
generalize (
alloc_in_vars_same _ _ _ _ _ AVR _ H2).
rewrite PTree.gss;
auto.
-
inv LNR.
destruct (
IHAVR _ H4 H0);
auto.
destruct H1 as [
i [
z [
A B]]].
right;
exists i;
exists z;
split;
auto.
Qed.
Lemma match_callstack_alloc_variables_inject:
forall vars tm1 sp tm2 m1 e m2 f1 e1 size cenv
(
AVS:
alloc_variables_right e1 m1 vars e m2)
(
NODBL:
nodbl e)
(
LNR:
list_norepet (
map fst vars))
(
He1:
forall id,
In id (
map fst vars) ->
e1 !
id =
None)
(
VB:
forall (
id :
positive) (
b :
block) (
z :
Z),
e !
id =
Some (
b,
z) -> ~
Mem.valid_block m1 b)
(
ALLOC:
Mem.alloc tm1 0 (
align size 8) =
Some (
tm2,
sp))
(
INJ:
Mem.inject Mem.id_pua f1 m1 tm1)
(
SSTF:
align size 8 =
align (
big_var_space vars 0) 8)
(
size_int: 0 <=
align size 8 <=
Int.max_unsigned)
(
cenv_spec:
fst (
assign_variables (
PTree.empty Z,0) (
rev vars)) =
cenv),
exists f2,
Mem.inject Mem.id_pua f2 m2 tm2 /\
inject_incr_cs f1 f2 sp m1 e cenv.
Proof.
induction vars.
-
simpl;
intros;
subst.
rewrite SSTF in ALLOC.
repeat change (
align 0 8)
with 0
in ALLOC.
generalize (
Mem.alloc_0_inject _ _ _ _ _ ALLOC INJ).
intro;
exists f1;
simpl;
auto.
inv AVS.
split;
auto.
constructor;
auto.
intros id b z ofs;
rewrite PTree.gempty;
congruence.
intros b delta FB.
clear H;
eapply Mem.mi_mappedblocks in FB;
eauto.
erewrite Mem.alloc_result in FB;
eauto.
unfold Mem.valid_block in FB;
xomega.
-
simpl in *;
intros;
subst.
inv AVS.
simpl in *.
destruct (
Mem.alloc tm1 0 (
align (
big_var_space vars 0) 8))
eqn:?.
+
destruct p.
generalize Heqo;
intro ALLOC'.
generalize (
fr_align_pos8 vars 0).
intro H;
trim H.
omega.
eapply IHvars with (
m2:=
m0)
in Heqo;
eauto.
*
destruct Heqo as [
f2 [
MI IICS]].
exists (
fun bb =>
if peq bb b1
then Some (
sp,
align
(
small_var_space vars 0)
(
block_alignment sz))
else f2 bb).
split.
{
eapply alloc_one_more;
eauto.
-
revert size_int.
generalize (
align_le (
Z.max 0
sz) 8).
intros.
rewrite SSTF in size_int.
rewrite <-
Mem.align_distr in size_int.
omega.
-
rewrite <-
ALLOC.
rewrite SSTF.
rewrite <- !
Mem.align_distr.
reflexivity.
-
clear IHvars H SSTF size_int.
intros.
inv IICS.
generalize H;
intro FB.
apply inj_env_ex0 in H.
destruct H as [
id0 [
sz0 Heid]].
des (
peq b0 b1).
erewrite Mem.mi_freeblocks in FB;
eauto.
congruence.
eapply Mem.fresh_block_alloc;
eauto.
des (
peq id id0).
erewrite (
alloc_in_vars'
_ _ _ _ _ H6)
with (
p:=(
b1,
Z.max 0
sz))
in Heid;
eauto.
inv Heid;
congruence.
inv LNR;
auto.
inv LNR;
intros;
rewrite PTree.gso.
apply He1;
auto.
congruence.
apply PTree.gss.
inv LNR.
destruct (
in_dec peq id0 (
map fst vars)).
+
generalize (
alloc_in_vars_domain _ _ _ _ _ H6 H2).
intro A.
trim A.
{
intros.
rewrite PTree.gso by congruence.
apply He1;
auto.
}
specialize (
A id0 b0 sz0).
trim A.
{
rewrite PTree.gso by congruence.
apply He1;
auto.
}
specialize (
A Heid).
destruct A as [
s' [
Zspec I]].
assert (
Mem.bounds_of_block m0 b0 = (0,
sz0)).
{
refine (
alloc_variables_right_bounds
_ _ _ _ _ _ _ _
H6 i Heid H2
_ _
).
*
intros.
red in NODBL.
apply NODBL in H5.
intro.
subst.
apply H5.
exists id2.
rewrite H7.
eexists;
repeat split;
eauto.
*
intros.
rewrite PTree.gso by congruence.
apply He1.
auto.
}
assert (
Mem.size_block m0 b0 =
sz0).
{
revert H;
unfold Mem.bounds_of_block,
Mem.size_block,
Alloc.get_size.
destr;
try des p;
inv H;
omega.
}
rewrite H0.
clear H0.
subst.
revert I inj_env0 Heid FB H2.
clear.
destruct ((
fst (
assign_variables (
PTree.empty Z, 0) (
rev vars)))!
id0)
eqn:?.
*
intros.
generalize Heid;
intro Heid'.
eapply inj_env0 with (
ofs:=
z)
in Heid;
auto.
rewrite Heid in FB.
inv FB.
clear inj_env0.
rewrite <- (
rev_involutive vars).
unfold small_var_space.
rewrite fold_left_rev_right.
apply in_rev in I.
apply list_norepet_rev in H2.
rewrite <-
map_rev in H2.
revert I Heqo H2.
unfold ident in *.
generalize (
rev vars).
clear Heid'
Heid.
intro l;
revert id0 s'
delta.
assert (0 <= 0)
by omega.
revert H.
generalize 0
at 2 3 6.
generalize (
PTree.empty Z).
clear.
{
induction l;
simpl;
intros.
exfalso;
auto.
unfold assign_variable in Heqo.
destruct a.
destruct I.
-
inv H0.
inv H2.
rewrite assign_variables_not_in in Heqo;
auto.
rewrite PTree.gss in Heqo.
inv Heqo.
simpl.
apply fl_align_add.
generalize (
Zmax_bound_l 0 0
s').
generalize (
align_le z _ (
block_alignment_pos s')).
omega.
-
apply IHl with (
s':=
s')
in Heqo;
auto.
generalize (
Zmax_bound_l 0 0
z0).
generalize (
align_le z _ (
block_alignment_pos z0)).
omega.
inv H2;
auto.
}
*
intros.
apply assign_variables_in in Heqo.
exfalso;
auto.
apply in_map with (
f:=
fst)
in I;
simpl in *;
auto.
rewrite map_rev.
apply ->
in_rev;
auto.
rewrite map_rev.
apply list_norepet_rev;
auto.
+
clear Heqs Heqs0.
exfalso.
apply VB with (
id:=
id0) (
b:=
b0) (
z:=
sz0);
auto.
generalize (
alloc_in_vars_same _ _ _ _ _ H6 _ n1).
rewrite PTree.gso by congruence.
rewrite Heid.
intro A.
destruct (
avr_valid_before _ _ _ _ _ H6 b0 H2);
auto.
destruct (
Mem.valid_block_dec m0 b0);
auto.
erewrite Mem.mi_freeblocks in FB;
eauto.
congruence.
destruct H as [
i [
z [
C B]]].
exfalso.
destruct (
peq i id0);
try congruence.
generalize (
NODBL _ _ _ Heid).
intro D;
apply D.
exists i;
exists (
b0,
z);
repeat split;
auto.
-
split.
+
apply Zge_le.
apply fr_align_pos.
omega.
+
apply sp_le_vars_right.
}
{
inv IICS.
constructor;
simpl;
intros;
eauto.
-
red;
intros.
destruct (
peq b0 b1);
subst;
auto.
erewrite Mem.mi_freeblocks with (
m1:=
m1)
in H0;
eauto.
congruence.
generalize (
alloc_variables_nextblock _ _ _ _ _ H6).
rewrite (
Mem.alloc_result _ _ _ _ _ H3).
unfold Mem.valid_block.
xomega.
-
destruct (
peq b0 b1);
subst;
auto.
generalize (
alloc_variables_nextblock _ _ _ _ _ H6).
rewrite (
Mem.alloc_result _ _ _ _ _ H3)
in H0.
xomega.
-
destruct (
peq b0 b1);
subst;
auto.
+
inv H0.
xomega.
+
eapply inj_above_thr_tm0 in H0;
eauto.
rewrite (
Mem.alloc_result _ _ _ _ _ ALLOC').
rewrite (
Mem.alloc_result _ _ _ _ _ ALLOC)
in H1.
auto.
-
destruct (
peq b0 b1);
subst;
auto.
inv LNR.
generalize (
alloc_in_vars'
_ _ _ _ _ H6 H7).
intro A.
assert (
e!
id =
Some (
b1,
Z.max 0
sz)).
{
apply A;
auto.
intros;
rewrite PTree.gso by congruence.
apply He1;
auto.
apply PTree.gss.
}
clear A.
assert (
id =
id0).
{
destruct (
peq id id0);
subst;
auto.
destruct (
NODBL id b1 _ H2).
exists id0.
exists (
b1,
z).
repeat split;
auto.
}
subst.
rewrite H0 in H2;
inv H2.
f_equal.
f_equal.
{
revert H1.
clear.
rewrite assign_variables_fold_left.
intro A;
inv A.
rewrite rev_involutive;
auto.
}
apply inj_env0 with (
ofs:=
ofs)
in H0.
rewrite (
Mem.alloc_result _ _ _ _ _ ALLOC')
in H0.
rewrite (
Mem.alloc_result _ _ _ _ _ ALLOC).
auto.
assert (
id0 <>
id).
{
intro;
subst.
erewrite (
alloc_in_vars'
_ _ _ _ _ H6)
with (
p:=(
b1,
Z.max 0
sz))
in H0;
eauto.
-
inv H0.
congruence.
-
inv LNR.
auto.
-
intros.
rewrite PTree.gso.
apply He1;
auto.
inv LNR;
intuition congruence.
-
apply PTree.gss.
}
clear -
H1 H2.
revert H1.
generalize (
PTree.empty Z).
generalize 0.
intros z t.
assert (~
In id0 (
map fst ((
id,
sz) ::
nil))).
{
simpl;
intuition congruence.
}
revert H.
unfold ident in *.
generalize ((
id,
sz)::
nil).
generalize (
rev vars).
clear H2.
intros l l0.
revert l l0 id0 ofs z t.
clear.
induction l;
simpl;
intros.
rewrite assign_variables_not_in in H1;
auto.
unfold ident in *.
destruct (
assign_variable (
t,
z)
a)
eqn:?.
apply IHl in H1;
auto.
-
destruct (
peq b0 b1);
subst;
intros;
eauto.
+
inv H0.
clear inj_env_ex0 inj_env0 inj_above_thr_tm0 inj_same_thr0 inj_incr0.
exists id;
exists (
Z.max 0
sz).
apply (
alloc_in_vars'
_ _ _ _ _ H6);
auto.
inv LNR;
auto.
intros.
inv LNR.
rewrite PTree.gso;
auto.
congruence.
apply PTree.gss.
+
assert (
b=
sp).
rewrite (
Mem.alloc_result _ _ _ _ _ ALLOC').
rewrite (
Mem.alloc_result _ _ _ _ _ ALLOC).
auto.
subst.
apply inj_env_ex0 in H0.
auto.
}
*
inv LNR;
auto.
*
intros.
generalize (
He1 _ (
or_intror H0)).
rewrite PTree.gso;
auto.
inv LNR;
auto.
congruence.
*
split;
try omega.
refine (
Zle_trans _ _ _ _ (
align_le _ 8
_)).
omega.
omega.
revert size_int.
rewrite SSTF.
rewrite <-
Mem.align_distr.
intro;
destruct size_int as [
_ size_int].
etransitivity;
eauto.
generalize (
align_le (
Z.max 0
sz) 8).
generalize (
Zmax_bound_l 0 0
sz).
omega.
+
generalize (
fr_align_pos8 vars 0).
intro H;
trim H.
omega.
revert size_int;
simpl.
revert ALLOC Heqo H.
rewrite SSTF.
clear;
intros.
exfalso.
eapply Mem.alloc_less_ok with (
z0:=(
align (
align (
big_var_space vars 0) 8 +
Z.max 0
sz) 8));
eauto.
congruence.
rewrite <-
Mem.align_distr.
generalize (
align_le (
Z.max 0
sz) 8).
generalize (
Zmax_bound_l 0 0
sz).
generalize (
align_le (
big_var_space vars 0) 8).
omega.
Qed.
Lemma alloc_variables_right_bounds_old:
forall vars e1 e m1 m2 b
(
AVR:
alloc_variables_right e1 m1 vars e m2)
(
MNB:
Plt b (
Mem.nextblock m1)),
Mem.bounds_of_block m2 b =
Mem.bounds_of_block m1 b.
Proof.
Lemma alloc_variables_right_perm:
forall vars e1 e2 m1 m2 b ofs p
(
AVR:
alloc_variables_right e1 m1 vars e2 m2)
(
LT:
Plt b (
Mem.nextblock m1))
(
PERM:
Mem.perm m2 b ofs Max p),
Mem.perm m1 b ofs Max p.
Proof.
Lemma avr_valid_ex:
forall vars e1 m1 e m2 b,
alloc_variables_right e1 m1 vars e m2 ->
(
forall id :
ident,
In id (
map fst vars) ->
e1 !
id =
None) ->
list_norepet (
map fst vars) ->
~
Mem.valid_block m1 b ->
Mem.valid_block m2 b ->
exists id z,
e !
id =
Some (
b,
z).
Proof.
induction vars;
simpl;
intros.
inv H.
congruence.
inv H.
destruct (
peq b b1);
subst;
auto.
-
exists id;
exists (
Z.max 0
sz).
inv H1.
rewrite (
alloc_in_vars'
_ _ _ _ _ H11 H6)
with (
p:=(
b1,
Z.max 0
sz));
auto.
intros;
eauto.
rewrite PTree.gso by congruence.
apply H0.
auto.
apply PTree.gss.
-
inv H1.
generalize (
IHvars _ _ _ _ b H11);
eauto.
intro A;
apply A;
auto.
intros.
rewrite PTree.gso by congruence.
apply H0;
auto.
destruct (
Mem.valid_block_alloc_inv _ _ _ _ _ H8 b H3);
auto.
congruence.
Qed.
Lemma avr_norepet:
forall e (
NDBL:
nodbl e),
list_norepet (
map fst (
map fst (
blocks_of_env e))).
Proof.
unfold nodbl,
blocks_of_env,
block_of_binding;
intros.
rewrite !
map_map.
rewrite map_ext with (
g:=
fun a =>
fst (
snd a))
by (
intros;
destruct a;
destruct p;
simpl;
auto).
assert (
forall id b sz,
In (
id,(
b,
sz)) (
PTree.elements e) ->
~
exists id'
p,
id' <>
id /\
e!
id' =
Some p /\
fst p =
b).
intros.
apply PTree.elements_complete in H.
eapply NDBL;
eauto.
assert (
forall id b sz,
In (
id,(
b,
sz)) (
PTree.elements e) ->
~
exists id'
z,
In (
id',(
b,
z)) (
PTree.elements e) /\
id' <>
id).
intros.
apply H in H0.
intro.
apply H0.
destruct H1 as [
id' [
z [
A B]]].
apply PTree.elements_complete in A.
exists id'.
exists (
b,
z).
auto.
clear H NDBL.
apply list_map_norepet;
auto.
generalize (
PTree.elements_keys_norepet e).
apply (
PTree_Properties.list_norepet_map).
intros.
destruct x as [
a [
b c]].
destruct y as [
d [
f g]].
generalize (
H0 _ _ _ H).
generalize (
H0 _ _ _ H1).
intros.
simpl in *.
intro;
subst.
apply H4.
exists d.
exists g.
split;
auto.
intro;
subst.
generalize (
PTree.elements_complete _ _ _ H1)
(
PTree.elements_complete _ _ _ H).
intros A B;
rewrite A in B;
inv B.
congruence.
Qed.
Lemma avr_hi_pos:
forall vars e1 m1 e m2
(
init:
Forall (
fun bnds :
ident *
Z *
Z =>
snd bnds >= 0) (
blocks_of_env e1))
(
AVS :
alloc_variables_right e1 m1 vars e m2),
Forall (
fun bnds :
ident *
Z *
Z =>
snd bnds >= 0) (
blocks_of_env e).
Proof.
Lemma list_norepet_NoDup:
forall A (
l:
list A),
NoDup l <->
list_norepet l.
Proof.
induction l; simpl; intros. split; constructor.
split; intro B; inv B; constructor; eauto.
apply IHl; auto.
apply IHl; auto.
Qed.
Lemma avr_in_vars:
forall vars e1 m1 e m2 i z'
(
LNR :
list_norepet (
map fst vars))
(
AVR :
alloc_variables_right e1 m1 vars e m2)
(
B :
In (
i,
z')
vars),
exists b :
block,
e !
i =
Some (
b,
Z.max 0
z').
Proof.
induction vars;
simpl;
intros;
auto.
exfalso;
auto.
inv AVR;
inv LNR.
destruct B.
-
inv H.
exists b1.
apply alloc_in_vars_same with (
id:=
i)
in H6;
auto.
rewrite <-
H6.
apply PTree.gss.
-
apply IHvars with (
i:=
i) (
z':=
z')
in H6;
auto.
Qed.
Lemma frmap:
forall A B C l f (
g:
A ->
B) (
c:
C),
fold_right f c (
map g l) =
fold_right (
fun y x =>
f (
g y)
x)
c l.
Proof.
induction l; simpl; intros. auto.
rewrite IHl. auto.
Qed.
Lemma frext:
forall A C f g
(
ext:
forall x y,
f x y =
g x y)
(
l:
list A) (
c:
C),
fold_right f c l =
fold_right g c l.
Proof.
induction l; simpl; intros; auto.
rewrite ext; auto.
rewrite IHl; auto.
Qed.
Lemma bvs_map_sup:
forall vars z,
big_var_space
(
map (
fun id_sz :
ident *
Z => (
fst id_sz,
Z.max 0 (
snd id_sz)))
vars)
z =
big_var_space vars z.
Proof.
induction vars;
simpl;
intros;
auto.
rewrite IHvars.
rewrite !
Zmax_spec;
repeat destr;
omega.
Qed.
Lemma avr_size_vars:
forall vars m1 e m2
(
LNR:
list_norepet (
map fst vars))
(
AVR:
alloc_variables_right empty_env m1 vars e m2)
(
He1:
forall id :
ident,
In id (
map fst vars) ->
empty_env !
id =
None)
(
Hnodbl:
nodbl empty_env)
(
He1vb:
forall (
id :
positive) (
b :
block) (
z :
Z),
empty_env !
id =
Some (
b,
z) -> ~
Mem.valid_block m2 b),
align
(
big_var_space vars 0) 8 =
align
(
big_vars_block_space ( (
blocks_of_env e)) 0) 8.
Proof.
Lemma match_callstack_alloc_variables_cs:
forall vars tm1 sp tm2 m1 e m2 cenv f1 cs le te e1 size size'
fns fnp fnv fnb f2
(
ALLOC:
Mem.alloc tm1 0 (
align size 8) =
Some (
tm2,
sp))
(
SSMU:
size' <=
Int.max_unsigned)
(
AVS:
alloc_variables_right e1 m1 vars e m2)
(
envs:
forall id p,
e1!
id =
Some p ->
e!
id =
Some p)
(
NODBL:
nodbl e1)
(
VB:
forall (
id :
positive) (
b :
block) (
z :
Z),
e1 !
id =
Some (
b,
z) -> ~
Mem.valid_block m2 b)
(
init:
Forall (
fun bnds :
ident *
Z *
Z =>
snd bnds >= 0) (
blocks_of_env e1))
(
LNR:
list_norepet (
map fst vars))
(
size_sup:
size' >=
align size 8)
(
Ccompat:
cenv_compat cenv vars size')
(
Csep:
cenv_separated cenv vars)
(
Csome_in: (
forall id ofs,
cenv!
id =
Some ofs ->
In id (
map fst vars)))
(
Esome_in: (
forall id b z,
e!
id =
Some (
b,
z) ->
exists z',
Z.max 0
z' =
z /\
In (
id,
z')
vars))
(
in_vars:
forall id,
In id (
map fst vars) ->
e1!
id =
None)
(
INJ:
Mem.inject Mem.id_pua f1 m1 tm1)
(
INJ':
Mem.inject Mem.id_pua f2 m2 tm2)
(
inj_spec:
inject_incr_cs f1 f2 sp m1 e cenv)
(
e_cenv:
forall id,
e !
id =
None <->
cenv !
id =
None)
(
MCS:
match_callstack f1 m1 tm1 cs (
Mem.nextblock m1) (
Mem.nextblock tm1))
(
MTmps:
match_temps f1 le te)
(
SSTF:
align size 8 =
align (
big_var_space vars 0) 8)
(
ss_blocks:
align size 8 =
align (
big_vars_block_space (
rev (
blocks_of_env e)) 0) 8)
(
ss_pos:
size >= 0),
match_callstack f2 m2 tm2 (
Frame cenv (
mkfunction fns fnp fnv size fnb)
e le te sp (
Mem.nextblock m1) (
Mem.nextblock m2) ::
cs)
(
Mem.nextblock m2) (
Mem.nextblock tm2).
Proof.
Lemma avr_in_not_none:
forall vars e1 m1 e m2 id
(
AVS :
alloc_variables_right e1 m1 vars e m2)
(
IN:
In id (
map fst vars)),
e !
id <>
None.
Proof.
induction 1;
simpl;
intros.
intuition.
destruct IN;
subst;
auto.
apply alloc_in_vars''
with (
id:=
id) (
p:=(
b1,
Z.max 0
sz))
in AVS;
auto.
apply PTree.gss.
Qed.
Properties of the compilation environment produced by build_compilenv
Remark assign_variable_incr:
forall id sz cenv stksz cenv'
stksz',
assign_variable (
cenv,
stksz) (
id,
sz) = (
cenv',
stksz') ->
stksz <=
stksz'.
Proof.
Remark assign_variables_incr:
forall vars cenv sz cenv'
sz',
assign_variables (
cenv,
sz)
vars = (
cenv',
sz') ->
sz <=
sz'.
Proof.
Remark inj_offset_aligned_block:
forall stacksize sz,
Mem.inj_offset_aligned (
align stacksize (
block_alignment sz))
sz.
Proof.
Lemma assign_variable_sound:
forall cenv1 sz1 id sz cenv2 sz2 vars,
assign_variable (
cenv1,
sz1) (
id,
sz) = (
cenv2,
sz2) ->
~
In id (
map fst vars) ->
0 <=
sz1 ->
cenv_compat cenv1 vars sz1 ->
cenv_separated cenv1 vars ->
cenv_compat cenv2 (
vars ++ (
id,
sz) ::
nil)
sz2
/\
cenv_separated cenv2 (
vars ++ (
id,
sz) ::
nil).
Proof.
unfold assign_variable;
intros until vars;
intros ASV NOREPET POS COMPAT SEP.
inv ASV.
assert (
LE:
sz1 <=
align sz1 8).
apply align_le.
omega.
assert (
EITHER:
forall id'
sz',
In (
id',
sz') (
vars ++ (
id,
sz) ::
nil) ->
In (
id',
sz')
vars /\
id' <>
id \/ (
id',
sz') = (
id,
sz)).
{
intros.
rewrite in_app in H.
destruct H.
left;
split;
auto.
red;
intros;
subst id'.
elim NOREPET.
change id with (
fst (
id,
sz')).
apply in_map;
auto.
simpl in H.
destruct H.
auto.
contradiction.
}
split;
red;
intros.
-
apply EITHER in H.
destruct H as [[
P Q] |
P].
+
exploit COMPAT;
eauto.
intros [
ofs [
A [
B [
C D]]]].
exists ofs.
split.
rewrite PTree.gso;
auto.
split.
auto.
split.
auto.
transitivity sz1.
auto.
rewrite Zmax_spec.
generalize (
align_le sz1 _ (
block_alignment_pos sz)).
destr;
omega.
+
inv P.
exists (
align sz1 (
block_alignment sz)).
split.
apply PTree.gss.
split.
unfold Mem.inj_offset_aligned.
intros.
apply Zdivides_trans with (
y:=(
block_alignment sz)).
unfold block_alignment;
repeat destruct zlt;
des chunk;
try (
exists 8;
auto;
fail);
try (
exists 4;
auto;
fail);
try (
exists 2;
auto;
fail);
try (
exists 1;
auto;
fail);
try omega.
apply align_divides.
apply block_alignment_pos.
split.
transitivity sz1;
auto.
apply (
align_le _ _ (
block_alignment_pos sz)).
omega.
-
apply EITHER in H;
apply EITHER in H0.
destruct H as [[
P Q] |
P];
destruct H0 as [[
R S] |
R].
+
rewrite PTree.gso in *;
auto.
eapply SEP;
eauto.
+
inv R.
rewrite PTree.gso in H1;
auto.
rewrite PTree.gss in H2;
inv H2.
exploit COMPAT;
eauto.
intros [
ofs [
A [
B [
C D]]]].
assert (
ofs =
ofs1)
by congruence.
subst ofs.
left.
transitivity (
ofs1 +
Z.max 0
sz0).
generalize (
Zmax_bound_r sz0 0
sz0).
omega.
transitivity sz1;
auto.
apply (
align_le _ _ (
block_alignment_pos sz)).
+
inv P.
rewrite PTree.gso in H2;
auto.
rewrite PTree.gss in H1;
inv H1.
exploit COMPAT;
eauto.
intros [
ofs [
A [
B [
C D]]]].
assert (
ofs =
ofs2)
by congruence.
subst ofs.
right.
transitivity (
ofs2 +
Z.max 0
sz2).
generalize (
Zmax_bound_r sz2 0
sz2).
omega.
transitivity sz1;
auto.
apply (
align_le _ _ (
block_alignment_pos sz)).
+
congruence.
Qed.
Lemma assign_variables_sound:
forall vars'
cenv1 sz1 cenv2 sz2 vars,
assign_variables (
cenv1,
sz1)
vars' = (
cenv2,
sz2) ->
list_norepet (
map fst vars' ++
map fst vars) ->
0 <=
sz1 ->
cenv_compat cenv1 vars sz1 ->
cenv_separated cenv1 vars ->
cenv_compat cenv2 (
vars ++
vars')
sz2 /\
cenv_separated cenv2 (
vars ++
vars').
Proof.
induction vars';
simpl;
intros.
rewrite app_nil_r.
inv H;
auto.
destruct a as [
id sz].
simpl in H0.
inv H0.
rewrite in_app in H6.
rewrite list_norepet_app in H7.
destruct H7 as [
P [
Q R]].
destruct (
assign_variable (
cenv1,
sz1) (
id,
sz))
as [
cenv'
sz']
eqn:?.
exploit assign_variable_sound.
eauto.
instantiate (1 :=
vars).
tauto.
auto.
auto.
auto.
intros [
A B].
exploit IHvars'.
eauto.
instantiate (1 :=
vars ++ ((
id,
sz) ::
nil)).
rewrite list_norepet_app.
split.
auto.
split.
rewrite map_app.
apply list_norepet_append_commut.
simpl.
constructor;
auto.
rewrite map_app.
simpl.
red;
intros.
rewrite in_app in H4.
destruct H4.
eauto.
simpl in H4.
destruct H4.
subst y.
red;
intros;
subst x.
tauto.
tauto.
generalize (
assign_variable_incr _ _ _ _ _ _ Heqp).
omega.
auto.
auto.
rewrite app_ass.
auto.
Qed.
Remark permutation_norepet:
forall (
A:
Type) (
l l':
list A),
Permutation l l' ->
list_norepet l ->
list_norepet l'.
Proof.
induction 1;
intros.
constructor.
inv H0.
constructor;
auto.
red;
intros;
elim H3.
apply Permutation_in with l';
auto.
apply Permutation_sym;
auto.
inv H.
simpl in H2.
inv H3.
constructor.
simpl;
intuition.
constructor.
intuition.
auto.
eauto.
Qed.
Lemma build_compilenv_sound:
forall f cenv sz,
build_compilenv f = (
cenv,
sz) ->
list_norepet (
map fst (
Csharpminor.fn_vars f)) ->
cenv_compat cenv (
Csharpminor.fn_vars f)
sz /\
cenv_separated cenv (
Csharpminor.fn_vars f).
Proof.
Lemma assign_variables_domain:
forall id vars cesz,
(
fst (
assign_variables cesz vars))!
id <>
None ->
(
fst cesz)!
id <>
None \/
In id (
map fst vars).
Proof.
induction vars;
simpl;
intros.
auto.
exploit IHvars;
eauto.
unfold assign_variable.
destruct a as [
id1 sz1].
destruct cesz as [
cenv stksz].
simpl.
rewrite PTree.gsspec.
destruct (
peq id id1).
auto.
tauto.
Qed.
Lemma build_compilenv_domain:
forall f cenv sz id ofs,
build_compilenv f = (
cenv,
sz) ->
cenv!
id =
Some ofs ->
In id (
map fst (
Csharpminor.fn_vars f)).
Proof.
Lemma match_callstack_alloc_variables:
forall vars tm1 sp tm2 m1 e m2 cenv f1 cs le te e1 size size'
fns fnp fnv fnb
(
ALLOC:
Mem.alloc tm1 0 (
align size 8) =
Some (
tm2,
sp))
(
SSMU:
size' <=
Int.max_unsigned)
(
AVS:
alloc_variables_right e1 m1 vars e m2)
(
init:
Forall (
fun bnds :
ident *
Z *
Z =>
snd bnds >= 0) (
blocks_of_env e1))
(
vars_fresh:
forall v b ofs,
e!
v =
Some (
b,
ofs) ->
~
Mem.valid_block m1 b
)
(
vars_fresh':
forall id b z,
e1!
id =
Some (
b,
z) ->
~
Mem.valid_block m2 b
)
(
NDBL:
nodbl e1)
(
LNR:
list_norepet (
map fst vars))
(
size_sup:
size' >=
align size 8)
(
Ccompat:
cenv_compat cenv vars size')
(
Csep:
cenv_separated cenv vars)
(
cenv_spec:
True ->
fst (
assign_variables (
PTree.empty Z, 0) (
rev vars)) =
cenv)
(
Csome_in: (
forall id ofs,
cenv!
id =
Some ofs ->
In id (
map fst vars)))
(
Esome_in: (
forall id b z,
e!
id =
Some (
b,
z) ->
exists z',
Z.max 0
z' =
z /\
In (
id,
z')
vars))
(
in_vars:
forall id,
In id (
map fst vars) ->
e1!
id =
None)
(
INJ:
Mem.inject Mem.id_pua f1 m1 tm1)
(
MCS:
match_callstack f1 m1 tm1 cs (
Mem.nextblock m1) (
Mem.nextblock tm1))
(
MTmps:
match_temps f1 le te)
(
SSTF:
align size 8 =
align (
big_var_space vars 0) 8)
(
ss_blocks:
align size 8 =
align
(
big_vars_block_space (
rev (
blocks_of_env e)) 0) 8)
(
ss_pos:
size >= 0),
exists f2,
match_callstack f2 m2 tm2 (
Frame cenv (
mkfunction fns fnp fnv size fnb)
e le te sp (
Mem.nextblock m1) (
Mem.nextblock m2) ::
cs)
(
Mem.nextblock m2) (
Mem.nextblock tm2)
/\
Mem.inject Mem.id_pua f2 m2 tm2.
Proof.
intros.
destruct (
match_callstack_alloc_variables_inject
_ _ _ _ _ _ _ _ _ _ cenv
AVS
(
alloc_variables_right_nodbl _ _ _ _ _ AVS LNR
in_vars NDBL vars_fresh')
LNR
in_vars
vars_fresh ALLOC INJ SSTF )
as [
f2 [
MI'
INJ_incr']];
auto.
-
split;
try omega.
refine (
Zle_trans _ size _ _ (
align_le _ _ _));
omega.
- (
exists f2;
split;
auto).
eapply match_callstack_alloc_variables_cs;
eauto.
+
intros id p H.
erewrite (
alloc_in_vars'
_ _ _ _ _ AVS)
with (
p:=
p);
eauto.
+
intros.
destruct (
in_dec peq id (
map fst vars)).
*
assert (
exists z,
In (
id,
z)
vars).
apply in_map_iff in i.
destruct i as [[
i z0] [
I J]].
exists z0;
auto.
simpl in *;
subst.
auto.
destruct H as [
z0 K].
destruct (
Ccompat _ _ K)
as [
ofs [
A [
B [
C D]]]].
rewrite A.
generalize (
avr_in_not_none _ _ _ _ _ id AVS i).
intuition congruence.
*
destruct (
e!
id)
eqn:?.
destruct p.
apply Esome_in in Heqo;
intuition try congruence.
destruct Heqo as [
z' [
ZM I]].
apply in_map with (
f:=
fst)
in I;
auto.
simpl in *;
intuition congruence.
destruct (
cenv!
id)
eqn:?.
apply Csome_in in Heqo0;
intuition try congruence.
tauto.
Qed.
Initialization of C#minor temporaries and Cminor local variables.
Lemma create_undef_temps_val:
forall id temps v,
(
create_undef_temps temps)!
id =
Some v ->
In id temps.
Proof.
induction temps;
simpl;
intros.
rewrite PTree.gempty in H.
congruence.
rewrite PTree.gsspec in H.
destruct (
peq id a).
auto.
exploit IHtemps;
eauto.
Qed.
Fixpoint set_params' (
vl:
list expr_sym) (
il:
list ident) (
te:
Cminor.env) :
Cminor.env :=
match il,
vl with
|
i1 ::
is,
v1 ::
vs =>
set_params'
vs is (
PTree.set i1 v1 te)
|
i1 ::
is,
nil =>
set_params'
nil is
(
PTree.set i1
(
Eval (
Eint Int.zero))
te)
|
_,
_ =>
te
end.
Lemma bind_parameters_agree_rec:
forall f vars vals tvals le1 le2 te,
bind_parameters vars vals le1 =
Some le2 ->
Val.expr_list_inject Mem.id_pua f vals tvals ->
match_temps f le1 te ->
match_temps f le2 (
set_params'
tvals vars te).
Proof.
Opaque PTree.set.
induction vars;
simpl;
intros.
destruct vals;
try discriminate.
inv H.
auto.
destruct vals;
try discriminate.
inv H0.
simpl.
eapply IHvars;
eauto.
red;
intros.
rewrite PTree.gsspec in *.
destruct (
peq id a).
inv H0.
exists v';
auto.
apply H1;
auto.
Qed.
Lemma set_params'
_outside:
forall id il vl te, ~
In id il -> (
set_params'
vl il te)!
id =
te!
id.
Proof.
induction il;
simpl;
intros.
auto.
destruct vl;
rewrite IHil.
apply PTree.gso.
intuition.
intuition.
apply PTree.gso.
intuition.
intuition.
Qed.
Lemma set_params'
_inside:
forall id il vl te1 te2,
In id il ->
(
set_params'
vl il te1)!
id = (
set_params'
vl il te2)!
id.
Proof.
induction il;
simpl;
intros.
contradiction.
destruct vl;
destruct (
List.in_dec peq id il);
auto;
repeat rewrite set_params'
_outside;
auto;
assert (
a =
id)
by intuition;
subst a;
repeat rewrite PTree.gss;
auto.
Qed.
Lemma set_params_set_params':
forall il vl id,
list_norepet il ->
(
set_params vl il)!
id = (
set_params'
vl il (
PTree.empty expr_sym))!
id.
Proof.
induction il;
simpl;
intros.
auto.
inv H.
destruct vl.
rewrite PTree.gsspec.
destruct (
peq id a).
subst a.
rewrite set_params'
_outside;
auto.
rewrite PTree.gss;
auto.
rewrite IHil;
auto.
destruct (
List.in_dec peq id il).
apply set_params'
_inside;
auto.
repeat rewrite set_params'
_outside;
auto.
rewrite PTree.gso;
auto.
rewrite PTree.gsspec.
destruct (
peq id a).
subst a.
rewrite set_params'
_outside;
auto.
rewrite PTree.gss;
auto.
rewrite IHil;
auto.
destruct (
List.in_dec peq id il).
apply set_params'
_inside;
auto.
repeat rewrite set_params'
_outside;
auto.
rewrite PTree.gso;
auto.
Qed.
Lemma set_locals_outside:
forall e id il,
~
In id il -> (
set_locals il e)!
id =
e!
id.
Proof.
induction il;
simpl;
intros.
auto.
rewrite PTree.gso.
apply IHil.
tauto.
intuition.
Qed.
Lemma set_locals_inside:
forall e id il,
In id il ->
(
set_locals il e)!
id =
Some (
Eval (
Eint Int.zero)).
Proof.
induction il;
simpl;
intros.
contradiction.
destruct H.
subst a.
rewrite PTree.gss.
eexists;
split;
eauto.
rewrite PTree.gsspec.
destruct (
peq id a).
eexists;
split;
eauto.
subst;
auto.
Qed.
Lemma set_locals_set_params':
forall vars vals params id,
list_norepet params ->
list_disjoint params vars ->
(
set_locals vars (
set_params vals params)) !
id =
(
set_params'
vals params (
set_locals vars (
PTree.empty expr_sym) )) !
id.
Proof.
Lemma create_undef_temps_init:
forall temps id0 v,
(
create_undef_temps temps) !
id0 =
Some v ->
v =
Eval (
Eint Int.zero).
Proof.
induction temps;
simpl;
intuition try congruence.
rewrite PTree.gempty in H.
congruence.
rewrite PTree.gsspec in H.
destruct (
peq id0 a);
subst.
inv H;
auto.
eapply IHtemps;
eauto.
Qed.
Lemma bind_parameters_agree:
forall f params temps vals tvals le,
bind_parameters params vals (
create_undef_temps temps) =
Some le ->
Val.expr_list_inject Mem.id_pua f vals tvals ->
list_norepet params ->
list_disjoint params temps ->
match_temps f le (
set_locals temps (
set_params tvals params)).
Proof.
The main result in this section.
Theorem match_callstack_function_entry:
forall fn cenv tf m e m'
tm tm'
sp f cs args targs le sz
(
TRF:
transl_function fn =
OK tf)
(
SSle:
sz <=
tf.(
fn_stackspace))
(
BCE:
build_compilenv fn = (
cenv,
sz))
(
SSMU:
align (
tf.(
fn_stackspace)) 8 <=
Int.max_unsigned)
(
LNR:
list_norepet (
map fst (
Csharpminor.fn_vars fn)))
(
LNRparam:
list_norepet (
Csharpminor.fn_params fn))
(
PAR_TMP:
list_disjoint (
Csharpminor.fn_params fn) (
Csharpminor.fn_temps fn))
(
AVR:
alloc_variables_right Csharpminor.empty_env m (
rev (
VarSort.sort (
Csharpminor.fn_vars fn)))
e m')
(
BP:
bind_parameters (
Csharpminor.fn_params fn)
args
(
create_undef_temps fn.(
fn_temps)) =
Some le)
(
ELI:
Val.expr_list_inject Mem.id_pua f args targs)
(
ALLOC:
Mem.alloc tm 0 (
align (
tf.(
fn_stackspace)) 8) =
Some (
tm',
sp))
(
MCS:
match_callstack f m tm cs (
Mem.nextblock m) (
Mem.nextblock tm))
(
MI:
Mem.inject Mem.id_pua f m tm)
,
let te :=
set_locals (
Csharpminor.fn_temps fn) (
set_params targs (
Csharpminor.fn_params fn))
in
exists f',
match_callstack f'
m'
tm'
(
Frame cenv tf e le te sp (
Mem.nextblock m) (
Mem.nextblock m') ::
cs)
(
Mem.nextblock m') (
Mem.nextblock tm')
/\
Mem.inject Mem.id_pua f'
m'
tm'.
Proof.
intros.
generalize (
build_compilenv_sound _ _ _ BCE LNR).
intros [
C1 C2].
destruct tf;
simpl in *.
eapply match_callstack_alloc_variables with (
size':=
align fn_stackspace 8);
eauto.
-
unfold blocks_of_env.
unfold empty_env.
simpl.
constructor.
-
clear -
AVR.
revert AVR.
assert (
forall v b z,
empty_env !
v =
Some (
b,
z) -> ~
Mem.valid_block m b).
{
intros v b z;
rewrite PTree.gempty.
intuition congruence.
}
generalize (
rev (
VarSort.sort (
Csharpminor.fn_vars fn)))
m e m'
empty_env H .
clear.
induction l;
simpl;
intros.
inv AVR.
apply H in H0;
auto.
inv AVR.
assert (
(
forall (
v :
positive) (
b :
block) (
z :
Z),
(
PTree.set id (
b1,
Z.max 0
sz)
e0) !
v =
Some (
b,
z) -> ~
Mem.valid_block m b) ->
forall (
v :
positive) (
b :
block) (
ofs :
Z),
e !
v =
Some (
b,
ofs) -> ~
Mem.valid_block m b).
{
intros.
eapply IHl in H8;
eauto.
}
clear IHl.
assert ((
forall (
v :
positive) (
b0 :
block) (
z :
Z),
(
PTree.set id (
b1,
Z.max 0
sz)
e0) !
v =
Some (
b0,
z) ->
~
Mem.valid_block m b0)).
{
intros.
rewrite PTree.gsspec in H2.
destruct (
peq v0 id);
subst;
auto.
inv H2.
rewrite (
Mem.alloc_result _ _ _ _ _ H5).
generalize (
alloc_variables_nextblock _ _ _ _ _ H8).
unfold Mem.valid_block.
xomega.
apply H in H2;
auto.
}
specialize (
H1 H2).
apply H1 in H0;
auto.
-
intros id b z.
rewrite PTree.gempty;
intuition congruence.
-
red.
intros id b sz'.
rewrite PTree.gempty;
intuition congruence.
-
rewrite map_rev.
apply list_norepet_rev.
generalize (
VarSort.Permuted_sort (
Csharpminor.fn_vars fn)).
intro.
apply Permutation_map with (
f:=
fst)
in H.
eapply permutation_norepet;
eauto.
-
omega.
-
red;
intros.
apply in_rev in H.
generalize (
VarSort.Permuted_sort (
Csharpminor.fn_vars fn)).
intro.
apply Permutation_sym in H0.
eapply Permutation_in in H;
eauto.
red in C1.
apply C1 in H.
destruct H;
intuition.
exists x;
repeat split;
auto.
etransitivity;
eauto.
etransitivity;
eauto.
apply align_le;
omega.
-
red;
intros.
generalize (
VarSort.Permuted_sort (
Csharpminor.fn_vars fn)).
intro.
symmetry in H4.
apply in_rev in H.
apply in_rev in H0.
eapply Permutation_in in H;
eauto.
eapply Permutation_in in H0;
eauto.
-
revert BCE.
unfold build_compilenv.
rewrite rev_involutive.
auto.
intro A;
rewrite A.
simpl;
auto.
-
intros.
generalize (
build_compilenv_domain _ _ _ _ _ BCE H).
intro.
rewrite map_rev.
rewrite in_rev.
rewrite rev_involutive.
generalize (
VarSort.Permuted_sort (
Csharpminor.fn_vars fn)).
intro.
apply Permutation_map with (
f:=
fst)
in H1.
eapply Permutation_in;
eauto.
-
intros.
generalize AVR.
apply avr_hi_pos in AVR.
rewrite Forall_forall in AVR.
generalize H.
apply in_blocks_of_env in H.
apply AVR in H.
simpl in H.
intros.
eapply (
alloc_in_vars_domain _ _ _ _ _ AVR0)
in H0;
eauto.
clear -
LNR.
rewrite map_rev.
apply list_norepet_rev.
generalize (
VarSort.Permuted_sort (
Csharpminor.fn_vars fn)).
intro.
apply Permutation_map with (
f:=
fst)
in H.
eapply permutation_norepet;
eauto.
intros;
rewrite PTree.gempty;
auto.
intros;
rewrite PTree.gempty;
auto.
unfold blocks_of_env,
empty_env;
simpl.
constructor.
-
intros;
rewrite PTree.gempty;
auto.
-
eapply bind_parameters_agree;
eauto.
-
generalize (
alloc_variables_alloc_sp _ _ TRF).
simpl.
intro;
subst;
auto.
-
generalize (
alloc_variables_alloc_sp _ _ TRF).
simpl.
intro;
subst.
rewrite bvbs_rew.
rewrite (
fr_permut'
_ _ _ (
Permutation_rev (
map _ _))).
rewrite map_rev.
rewrite rev_involutive.
rewrite <-
bvbs_rew.
eapply (
avr_size_vars);
eauto.
+
rewrite map_rev.
apply list_norepet_rev.
generalize (
VarSort.Permuted_sort (
Csharpminor.fn_vars fn)).
intro.
apply Permutation_map with (
f:=
fst)
in H.
eapply permutation_norepet;
eauto.
+
intros;
rewrite PTree.gempty;
auto.
+
red;
intros id b sz'.
rewrite PTree.gempty;
auto.
congruence.
+
red;
intros id b sz'.
rewrite PTree.gempty;
auto.
congruence.
-
generalize (
alloc_variables_alloc_sp _ _ TRF).
simpl.
intro;
subst.
apply fr_align_pos8;
omega.
Qed.
Definition fold_alloc_fn (
v:
ident*
Z) (
m:
Csharpminor.env*
mem) :=
match Mem.alloc (
snd m) 0 (
Z.max 0 (
snd v))
with
Some (
m',
b') =>
(
PTree.set (
fst v) (
b',
Z.max 0 (
snd v)) (
fst m),
m')
|
None =>
m
end.
Lemma env_independent:
forall vars (
e e':
Csharpminor.env)
m,
snd (
fold_right fold_alloc_fn (
e,
m)
vars) =
snd (
fold_right fold_alloc_fn (
e',
m)
vars).
Proof.
induction vars;
simpl;
intros;
auto.
unfold fold_alloc_fn at 1 3;
simpl.
rewrite IHvars with (
e':=
e').
auto.
destr_cond_match;
auto.
destruct p;
simpl;
auto.
Qed.
Lemma alloc_variables_fold_right_mem:
forall vars e m e2 m2 e3 m3,
alloc_variables_right e m vars e2 m2 ->
fold_right fold_alloc_fn (
e,
m)
vars = (
e3,
m3) ->
m2 =
m3.
Proof.
Lemma fold_alloc_fn_old:
forall vars e m e1 m0 id,
~
In id (
map fst vars) ->
fold_right fold_alloc_fn (
e,
m)
vars = (
e1,
m0) ->
e1 !
id =
e !
id.
Proof.
induction vars;
simpl;
intros.
inv H0;
auto.
destruct (
fold_right fold_alloc_fn (
e,
m)
vars)
eqn:?;
simpl in *.
eapply IHvars with (
id:=
id)
in Heqp;
auto.
rewrite <-
Heqp.
unfold fold_alloc_fn in H0.
simpl in H0.
revert H0;
destr.
destruct p.
inv H0.
rewrite PTree.gso;
auto.
Qed.
Lemma fold_alloc_fn_diff:
forall vars e m p e0 e1 m0 id
(
FAF:
fold_right fold_alloc_fn (
e,
m)
vars = (
e0,
m0))
(
FAF':
fold_right fold_alloc_fn (
PTree.set id p e,
m)
vars = (
e1,
m0))
id0
(
DIFF:
id0 <>
id),
e0 !
id0 =
e1 !
id0.
Proof.
Lemma alloc_variables_fold_right_env:
forall vars e m e2 m2,
list_norepet (
map fst vars) ->
alloc_variables_right e m vars e2 m2 ->
forall e3 m3,
fold_right fold_alloc_fn (
e,
m)
vars = (
e3,
m3) ->
forall id,
e3!
id =
e2!
id.
Proof.
Lemma alloc_variables_fold_right:
forall vars e m e2 m2,
list_norepet (
map fst vars) ->
alloc_variables_right e m vars e2 m2 ->
forall e3 m3,
fold_right fold_alloc_fn (
e,
m)
vars = (
e3,
m3) ->
m2 =
m3 /\
forall id,
e3!
id =
e2!
id.
Proof.
Lemma alloc_variables_right_just_mem:
forall l m e e1 e'
m',
alloc_variables_right e1 m l e'
m' ->
exists (
e'0 :
Csharpminor.env),
alloc_variables_right e m l e'0
m'.
Proof.
induction l;
simpl;
intros;
auto.
inv H.
exists e;
constructor.
inv H.
eapply IHl with (
e:=(
PTree.set id (
b1,
Z.max 0
sz)
e))
in H7;
eauto.
destruct H7 as [
e'0
H7].
eexists.
econstructor;
eauto.
Qed.
Lemma alloc_variables_right_decompose:
forall vars e m l ee mm,
alloc_variables_right e m (
vars ++
l)
ee mm ->
exists e'
m',
alloc_variables_right e m l e'
m'.
Proof.
induction vars;
simpl;
intros.
exists ee;
exists mm;
auto.
inv H.
apply IHvars in H7.
destruct H7 as [
e' [
m'
H7]].
eapply alloc_variables_right_just_mem in H7;
eauto.
destruct H7.
exists x;
exists m';
eauto.
Qed.
Lemma alloc_variables_right_determ:
forall l e m ee mm e'
m'
(
AVR :
alloc_variables_right e m l ee mm)
(
AVR' :
alloc_variables_right e m l e'
m'),
ee =
e' /\
mm =
m'.
Proof.
Lemma alloc_variables_right_decompose':
forall vars l e m ee mm,
alloc_variables_right e m (
vars ++
l)
ee mm ->
forall e'
m',
alloc_variables_right e m l e'
m' ->
exists ee',
alloc_variables_right e'
m'
vars ee'
mm.
Proof.
Lemma alloc_variables_right_decompose'':
forall vars l e m ee mm,
alloc_variables_right e m (
vars ++
l)
ee mm ->
exists e'
m'
ee',
alloc_variables_right e m l e'
m' /\
alloc_variables_right e'
m'
vars ee'
mm.
Proof.
intros.
destruct (
alloc_variables_right_decompose _ _ _ _ _ _ H)
as [
e' [
m'
A]].
destruct (
alloc_variables_right_decompose'
_ _ _ _ _ _ H _ _ A)
as [
ee'
B].
exists e';
exists m';
exists ee';
split;
auto.
Qed.
Lemma fold_alloc_fn_in_vars:
forall vars (
e'
e1:
Csharpminor.env)
m1 e2 e0 m2
(
INIT:
forall id,
e'!
id =
e1!
id)
(
FR1:
fold_right fold_alloc_fn (
e',
m1)
vars = (
e2,
m2))
(
FR2:
fold_right fold_alloc_fn (
e1,
m1)
vars = (
e0,
m2))
id
(
LNR:
list_norepet (
map fst vars))
(
i :
In id (
map fst vars)),
e2 !
id =
e0 !
id.
Proof.
induction vars;
simpl;
intros.
exfalso;
auto.
destruct (
fold_right fold_alloc_fn (
e',
m1)
vars)
eqn:?.
destruct (
fold_right fold_alloc_fn (
e1,
m1)
vars)
eqn:?.
generalize (
env_independent vars e'
e1 m1).
rewrite Heqp.
rewrite Heqp0.
simpl;
intro;
subst.
revert FR1 FR2;
unfold fold_alloc_fn;
simpl;
destr_cond_match.
destruct p.
intros A B;
inv A;
inv B.
rewrite !
PTree.gsspec.
destruct i;
subst.
rewrite !
peq_true.
auto.
inv LNR.
rewrite (
IHvars _ _ _ _ _ _ INIT Heqp Heqp0 _ H3 H).
auto.
intros A B;
inv A;
inv B.
destruct i;
subst.
inv LNR.
generalize (
fold_alloc_fn_old _ _ _ _ _ _ H1 Heqp).
generalize (
fold_alloc_fn_old _ _ _ _ _ _ H1 Heqp0).
clear -
INIT.
intros A B.
rewrite A.
rewrite B.
auto.
inv LNR.
rewrite (
IHvars _ _ _ _ _ _ INIT Heqp Heqp0 _ H3 H).
auto.
Qed.
Lemma fold_alloc_fn_in_vars':
forall vars (
e'
e1:
Csharpminor.env)
m1 e2 e0 m2
(
INIT:
forall id,
In id (
map fst vars) ->
e'!
id =
e1!
id)
(
FR1:
fold_right fold_alloc_fn (
e',
m1)
vars = (
e2,
m2))
(
FR2:
fold_right fold_alloc_fn (
e1,
m1)
vars = (
e0,
m2))
id
(
LNR:
list_norepet (
map fst vars))
(
i :
In id (
map fst vars)),
e2 !
id =
e0 !
id.
Proof.
induction vars;
simpl;
intros.
exfalso;
auto.
destruct (
fold_right fold_alloc_fn (
e',
m1)
vars)
eqn:?.
destruct (
fold_right fold_alloc_fn (
e1,
m1)
vars)
eqn:?.
generalize (
env_independent vars e'
e1 m1).
rewrite Heqp.
rewrite Heqp0.
simpl;
intro;
subst.
revert FR1 FR2;
unfold fold_alloc_fn;
simpl;
destr_cond_match.
destruct p.
intros A B;
inv A;
inv B.
rewrite !
PTree.gsspec.
destruct i;
subst.
rewrite !
peq_true.
auto.
inv LNR.
assert (
init:
forall id,
In id (
map fst vars) ->
e'!
id =
e1!
id).
intros;
auto.
rewrite (
IHvars _ _ _ _ _ _ init Heqp Heqp0 _ H3 H).
auto.
intros A B;
inv A;
inv B.
destruct i;
subst.
inv LNR.
generalize (
fold_alloc_fn_old _ _ _ _ _ _ H1 Heqp).
generalize (
fold_alloc_fn_old _ _ _ _ _ _ H1 Heqp0).
clear -
INIT.
intros A B.
rewrite A.
rewrite B.
auto.
inv LNR.
assert (
init:
forall id,
In id (
map fst vars) ->
e'!
id =
e1!
id).
intros;
auto.
rewrite (
IHvars _ _ _ _ _ _ init Heqp Heqp0 _ H3 H).
auto.
Qed.
Lemma alloc_variables_right_app:
forall vars l e m ee mm,
list_norepet (
map fst (
vars ++
l)) ->
alloc_variables_right e m (
vars ++
l)
ee mm ->
exists ee'
mm'
e2,
alloc_variables_right e m l ee'
mm' /\
alloc_variables_right ee'
mm'
vars e2 mm /\
forall id,
e2 !
id =
ee !
id.
Proof.
Lemma alloc_variables_right_env:
forall vars e e'
m ef ef'
mf
(
LNR:
list_norepet (
map fst vars))
(
AVR:
alloc_variables_right e m vars ef mf)
(
AVR':
alloc_variables_right e'
m vars ef'
mf)
(
INIT:
forall id,
In id (
map fst vars) ->
e!
id=
e'!
id)
id,
ef!
id =
if in_dec peq id (
map fst vars)
then ef'!
id
else e!
id.
Proof.
Lemma avr_old
:
forall (
vars :
list (
ident *
Z)) (
e :
Csharpminor.env)
(
m :
mem) (
e1 :
Csharpminor.env) (
m0 :
mem)
(
id :
ident),
~
In id (
map fst vars) ->
list_norepet (
map fst vars) ->
alloc_variables_right e m vars e1 m0 ->
e1 !
id =
e !
id.
Proof.
Lemma alloc_variables_right_app':
forall vars l e m mm ee'
mm'
e2,
list_norepet (
map fst (
vars ++
l)) ->
alloc_variables_right e m l ee'
mm' ->
alloc_variables_right ee'
mm'
vars e2 mm ->
exists e2',
alloc_variables_right e m (
vars ++
l)
e2'
mm /\
forall id,
e2!
id =
e2'!
id.
Proof.
Lemma alloc_variables_left_right:
forall (
vars :
list (
ident *
Z)) (
e :
Csharpminor.env)
(
m :
mem) (
e2 :
Csharpminor.env) (
m2 :
mem)
(
LNR:
list_norepet (
map fst vars)),
alloc_variables e m vars e2 m2 ->
exists e2',
alloc_variables_right e m (
rev vars)
e2'
m2 /\
forall id,
e2!
id=
e2'!
id.
Proof.
induction vars;
simpl;
intros.
inv H.
exists e2;
split;
constructor.
inv H.
inv LNR.
apply IHvars in H7;
auto.
destruct H7 as [
e2' [
A B]].
exploit (
alloc_variables_right_app' (
rev vars) ((
id,
sz)::
nil)
e m m2 (
PTree.set id (
b1,
Z.max 0
sz)
e)
m1 e2').
replace (
rev vars ++ (
id,
sz) ::
nil)
with (
rev ((
id,
sz)::
vars));
auto.
rewrite map_rev.
apply list_norepet_rev.
simpl.
constructor;
auto.
econstructor;
eauto.
constructor.
auto.
intros [
e2'0 [
C D]].
exists e2'0;
split;
auto.
intros.
rewrite B.
apply D.
Qed.
Compatibility of evaluation functions with respect to memory injections.
Remark val_inject_val_of_bool:
forall f b,
Val.expr_inject Mem.id_pua f (
Val.of_bool b) (
Val.of_bool b).
Proof.
unfold Val.of_bool.
destruct b;
econstructor;
simpl;
eauto;
simpl;
tauto.
Qed.
Ltac TrivialExists :=
match goal with
| [ |-
exists y,
Some ?
x =
Some y /\
val_inject _ _ _ ] =>
exists x;
split; [
auto |
try(
econstructor;
eauto)]
| [ |-
exists y,
_ /\
val_inject _ (
Vint ?
x)
_ ] =>
exists (
Vint x);
split; [
eauto with evalexpr |
constructor]
| [ |-
exists y,
_ /\
val_inject _ (
Vfloat ?
x)
_ ] =>
exists (
Vfloat x);
split; [
eauto with evalexpr |
constructor]
| [ |-
exists y,
_ /\
val_inject _ (
Vlong ?
x)
_ ] =>
exists (
Vlong x);
split; [
eauto with evalexpr |
constructor]
|
_ =>
idtac
end.
Compatibility of eval_unop with respect to val_inject.
Lemma eval_unop_compat:
forall f op v1 tv1 v,
eval_unop op v1 =
Some v ->
Val.expr_inject Mem.id_pua f v1 tv1 ->
exists tv,
eval_unop op tv1 =
Some tv
/\
Val.expr_inject Mem.id_pua f v tv.
Proof.
intros.
destruct op;
simpl;
intros;
inv H;
eexists;
split;
eauto;
try (
apply Val.expr_inject_unop;
auto).
Qed.
Compatibility of eval_binop with respect to val_inject.
Lemma eval_binop_compat:
forall f op v1 tv1 v2 tv2 v m tm,
eval_binop op v1 v2 m =
Some v ->
Val.expr_inject Mem.id_pua f v1 tv1 ->
Val.expr_inject Mem.id_pua f v2 tv2 ->
Mem.inject Mem.id_pua f m tm ->
exists tv,
eval_binop op tv1 tv2 tm =
Some tv
/\
Val.expr_inject Mem.id_pua f v tv.
Proof.
Correctness of Cminor construction functions
Correctness of the variable accessor var_addr
Lemma var_addr_correct:
forall cenv id f tf e le te sp lo hi m cs tm b,
match_callstack f m tm (
Frame cenv tf e le te sp lo hi ::
cs) (
Mem.nextblock m) (
Mem.nextblock tm) ->
eval_var_addr ge e id b ->
exists tv,
eval_expr tge sp te tm (
var_addr cenv id)
tv
/\
Val.expr_inject Mem.id_pua f (
Eval (
Eptr b Int.zero))
tv.
Proof.
unfold var_addr;
intros.
assert (
match_var f sp e!
id cenv!
id).
inv H.
inv MENV.
auto.
inv H1;
inv H0;
try congruence.
-
(
exists (
Eval (
Eptr sp (
Int.repr ofs))));
split.
constructor.
simpl.
auto.
rewrite <-
H2 in H1;
inv H1.
auto.
-
exploit match_callstack_match_globalenvs;
eauto.
intros [
bnd MG].
inv MG.
(
exists (
Eval (
Eptr b (
Int.zero))));
split.
constructor.
simpl.
rewrite symbols_preserved.
rewrite H2.
auto.
econstructor;
simpl;
eauto.
unfold Val.inj_ptr;
rewrite DOMAIN;
auto.
eapply SYMBOLS;
eauto.
Qed.
Semantic preservation for the translation
The proof of semantic preservation uses simulation diagrams of the
following form:
e, m1, s ----------------- sp, te1, tm1, ts
| |
t| |t
v v
e, m2, out --------------- sp, te2, tm2, tout
where
ts is the Cminor statement obtained by translating the
C#minor statement
s. The left vertical arrow is an execution
of a C#minor statement. The right vertical arrow is an execution
of a Cminor statement. The precondition (top vertical bar)
includes a
mem_inject relation between the memory states
m1 and
tm1,
and a
match_callstack relation for any callstack having
e,
te1,
sp as top frame. The postcondition (bottom vertical bar)
is the existence of a memory injection
f2 that extends the injection
f1 we started with, preserves the
match_callstack relation for
the transformed callstack at the final state, and validates a
outcome_inject relation between the outcomes
out and
tout.
Semantic preservation for expressions
Remark bool_of_val_inject:
forall f v tv b,
Val.bool_of_val v b ->
Val.expr_inject Mem.id_pua f v tv ->
Val.bool_of_val tv b.
Proof.
Lemma transl_constant_correct:
forall f sp cst v,
Csharpminor.eval_constant cst =
Some v ->
exists tv,
eval_constant tge sp (
transl_constant cst) =
Some tv
/\
Val.expr_inject Mem.id_pua f v tv.
Proof.
destruct cst; simpl; intros; inv H; eexists; split; eauto;
econstructor; simpl; eauto; simpl; tauto.
Qed.
Lemma transl_expr_correct:
forall f m tm cenv tf e le te sp lo hi cs
(
MINJ:
Mem.inject Mem.id_pua f m tm)
(
MATCH:
match_callstack f m tm
(
Frame cenv tf e le te sp lo hi ::
cs)
(
Mem.nextblock m) (
Mem.nextblock tm)),
forall a v,
Csharpminor.eval_expr ge e le m a v ->
forall ta
(
TR:
transl_expr cenv a =
OK ta),
exists tv,
eval_expr tge sp te tm ta tv
/\
Val.expr_inject Mem.id_pua f v tv.
Proof.
induction 3;
intros;
simpl in TR;
try (
monadInv TR).
-
inv MATCH.
exploit MTMP;
eauto.
intros [
tv [
A B]].
exists tv;
split.
constructor;
auto.
auto.
-
exploit var_addr_correct;
eauto.
-
exploit transl_constant_correct;
eauto.
intros [
tv [
A B]].
exists tv;
split;
eauto.
constructor;
eauto.
-
exploit IHeval_expr;
eauto.
intros [
tv1 [
EVAL1 INJ1 ]].
exploit eval_unop_compat;
eauto.
intros [
tv2 [
EVAL INJ]].
exists tv2.
split;
auto.
econstructor;
eauto.
-
exploit IHeval_expr1;
eauto.
intros [
tv1 [
EVAL1 INJ1]].
exploit IHeval_expr2;
eauto.
intros [
tv2 [
EVAL2 INJ2]].
exploit eval_binop_compat;
eauto.
intros [
tv [
EVAL INJ]].
exists tv;
split.
econstructor;
eauto.
auto.
-
exploit IHeval_expr;
eauto.
intros [
tv1 [
EVAL1 INJ1]].
exploit Mem.loadv_inject;
eauto.
apply match_callstack_all_blocks_injected in MATCH;
auto.
intros [
tv [
LOAD INJ]].
exists tv;
split.
econstructor;
eauto.
auto.
Qed.
Lemma transl_exprlist_correct:
forall f m tm cenv tf e le te sp lo hi cs
(
MINJ:
Mem.inject Mem.id_pua f m tm)
(
MATCH:
match_callstack f m tm
(
Frame cenv tf e le te sp lo hi ::
cs)
(
Mem.nextblock m) (
Mem.nextblock tm)),
forall a v,
Csharpminor.eval_exprlist ge e le m a v ->
forall ta
(
TR:
transl_exprlist cenv a =
OK ta),
exists tv,
eval_exprlist tge sp te tm ta tv
/\
Val.expr_list_inject Mem.id_pua f v tv.
Proof.
induction 3;
intros;
monadInv TR.
exists (@
nil expr_sym);
split.
constructor.
constructor.
exploit transl_expr_correct;
eauto.
intros [
tv1 [
EVAL1 VINJ1]].
exploit IHeval_exprlist;
eauto.
intros [
tv2 [
EVAL2 VINJ2]].
exists (
tv1 ::
tv2);
split.
constructor;
auto.
constructor;
auto.
Qed.
Semantic preservation for statements and functions
Inductive match_cont:
Csharpminor.cont ->
Cminor.cont ->
compilenv ->
exit_env ->
callstack ->
Prop :=
|
match_Kstop:
forall cenv xenv,
match_cont Csharpminor.Kstop Kstop cenv xenv nil
|
match_Kseq:
forall s k ts tk cenv xenv cs,
transl_stmt cenv xenv s =
OK ts ->
match_cont k tk cenv xenv cs ->
match_cont (
Csharpminor.Kseq s k) (
Kseq ts tk)
cenv xenv cs
|
match_Kseq2:
forall s1 s2 k ts1 tk cenv xenv cs,
transl_stmt cenv xenv s1 =
OK ts1 ->
match_cont (
Csharpminor.Kseq s2 k)
tk cenv xenv cs ->
match_cont (
Csharpminor.Kseq (
Csharpminor.Sseq s1 s2)
k)
(
Kseq ts1 tk)
cenv xenv cs
|
match_Kblock:
forall k tk cenv xenv cs,
match_cont k tk cenv xenv cs ->
match_cont (
Csharpminor.Kblock k) (
Kblock tk)
cenv (
true ::
xenv)
cs
|
match_Kblock2:
forall k tk cenv xenv cs,
match_cont k tk cenv xenv cs ->
match_cont k (
Kblock tk)
cenv (
false ::
xenv)
cs
|
match_Kcall:
forall optid fn e le k tfn sp te tk cenv xenv lo hi cs sz cenv',
transl_funbody cenv sz fn =
OK tfn ->
match_cont k tk cenv xenv cs ->
match_cont (
Csharpminor.Kcall optid fn e le k)
(
Kcall optid tfn sp te tk)
cenv'
nil
(
Frame cenv tfn e le te sp lo hi ::
cs).
Inductive match_states:
Csharpminor.state ->
Cminor.state ->
Prop :=
|
match_state:
forall fn s k e le m tfn ts tk sp te tm cenv xenv f lo hi cs sz
(
TRF:
transl_funbody cenv sz fn =
OK tfn)
(
TR:
transl_stmt cenv xenv s =
OK ts)
(
MINJ:
Mem.inject Mem.id_pua f m tm)
(
MCS:
match_callstack f m tm
(
Frame cenv tfn e le te sp lo hi ::
cs)
(
Mem.nextblock m) (
Mem.nextblock tm))
(
MK:
match_cont k tk cenv xenv cs),
match_states (
Csharpminor.State fn s k e le m)
(
State tfn ts tk sp te tm)
|
match_state_seq:
forall fn s1 s2 k e le m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz
(
TRF:
transl_funbody cenv sz fn =
OK tfn)
(
TR:
transl_stmt cenv xenv s1 =
OK ts1)
(
MINJ:
Mem.inject Mem.id_pua f m tm)
(
MCS:
match_callstack f m tm
(
Frame cenv tfn e le te sp lo hi ::
cs)
(
Mem.nextblock m) (
Mem.nextblock tm))
(
MK:
match_cont (
Csharpminor.Kseq s2 k)
tk cenv xenv cs),
match_states (
Csharpminor.State fn (
Csharpminor.Sseq s1 s2)
k e le m)
(
State tfn ts1 tk sp te tm)
|
match_callstate:
forall fd args k m tfd targs tk tm f cs cenv
(
TR:
transl_fundef fd =
OK tfd)
(
MINJ:
Mem.inject Mem.id_pua f m tm)
(
MCS:
match_callstack f m tm cs (
Mem.nextblock m) (
Mem.nextblock tm))
(
MK:
match_cont k tk cenv nil cs)
(
ISCC:
Csharpminor.is_call_cont k)
(
ARGSINJ:
Val.expr_list_inject Mem.id_pua f args targs),
match_states (
Csharpminor.Callstate fd args k m)
(
Callstate tfd targs tk tm)
|
match_returnstate:
forall v k m tv tk tm f cs cenv
(
MINJ:
Mem.inject Mem.id_pua f m tm)
(
MCS:
match_callstack f m tm cs (
Mem.nextblock m) (
Mem.nextblock tm))
(
MK:
match_cont k tk cenv nil cs)
(
RESINJ:
Val.expr_inject Mem.id_pua f v tv),
match_states (
Csharpminor.Returnstate v k m)
(
Returnstate tv tk tm).
Remark val_inject_function_pointer:
forall m'
m bound v fd f tv
(
MI:
Mem.inject Mem.id_pua f m m')
(
FF:
Genv.find_funct m ge v =
Some fd)
(
MGE:
match_globalenvs f bound)
(
ABI:
Mem.all_blocks_injected f m)
(
EI:
Val.expr_inject Mem.id_pua f v tv),
Mem.mem_norm m'
tv Ptr =
Mem.mem_norm m v Ptr.
Proof.
Lemma match_call_cont:
forall k tk cenv xenv cs,
match_cont k tk cenv xenv cs ->
match_cont (
Csharpminor.call_cont k) (
call_cont tk)
cenv nil cs.
Proof.
induction 1; simpl; auto; econstructor; eauto.
Qed.
Lemma match_is_call_cont:
forall tfn te sp tm k tk cenv xenv cs,
match_cont k tk cenv xenv cs ->
Csharpminor.is_call_cont k ->
exists tk',
star step tge (
State tfn Sskip tk sp te tm)
E0 (
State tfn Sskip tk'
sp te tm)
/\
is_call_cont tk'
/\
match_cont k tk'
cenv nil cs.
Proof.
induction 1;
simpl;
intros;
try contradiction.
econstructor;
split.
apply star_refl.
split.
exact I.
econstructor;
eauto.
exploit IHmatch_cont;
eauto.
intros [
tk' [
A B]].
exists tk';
split.
eapply star_left;
eauto.
constructor.
traceEq.
auto.
econstructor;
split.
apply star_refl.
split.
exact I.
econstructor;
eauto.
Qed.
Properties of switch compilation
Inductive lbl_stmt_tail:
lbl_stmt ->
nat ->
lbl_stmt ->
Prop :=
|
lstail_O:
forall sl,
lbl_stmt_tail sl O sl
|
lstail_S:
forall c s sl n sl',
lbl_stmt_tail sl n sl' ->
lbl_stmt_tail (
LScons c s sl) (
S n)
sl'.
Lemma switch_table_default:
forall sl base,
exists n,
lbl_stmt_tail sl n (
select_switch_default sl)
/\
snd (
switch_table sl base) = (
n +
base)%
nat.
Proof.
induction sl;
simpl;
intros.
-
exists O;
split.
constructor.
omega.
-
destruct o.
+
destruct (
IHsl (
S base))
as (
n &
P &
Q).
exists (
S n);
split.
constructor;
auto.
destruct (
switch_table sl (
S base))
as [
tbl dfl];
simpl in *.
omega.
+
exists O;
split.
constructor.
destruct (
switch_table sl (
S base))
as [
tbl dfl];
simpl in *.
auto.
Qed.
Lemma switch_table_case:
forall i sl base dfl,
match select_switch_case i sl with
|
None =>
switch_target i dfl (
fst (
switch_table sl base)) =
dfl
|
Some sl' =>
exists n,
lbl_stmt_tail sl n sl'
/\
switch_target i dfl (
fst (
switch_table sl base)) = (
n +
base)%
nat
end.
Proof.
induction sl;
simpl;
intros.
-
auto.
-
destruct (
switch_table sl (
S base))
as [
tbl1 dfl1]
eqn:
ST.
destruct o;
simpl.
rewrite dec_eq_sym.
destruct (
zeq i z).
exists O;
split;
auto.
constructor.
specialize (
IHsl (
S base)
dfl).
rewrite ST in IHsl.
simpl in *.
destruct (
select_switch_case i sl).
destruct IHsl as (
x &
P &
Q).
exists (
S x);
split.
constructor;
auto.
omega.
auto.
specialize (
IHsl (
S base)
dfl).
rewrite ST in IHsl.
simpl in *.
destruct (
select_switch_case i sl).
destruct IHsl as (
x &
P &
Q).
exists (
S x);
split.
constructor;
auto.
omega.
auto.
Qed.
Lemma switch_table_select:
forall i sl,
lbl_stmt_tail sl
(
switch_target i (
snd (
switch_table sl O)) (
fst (
switch_table sl O)))
(
select_switch i sl).
Proof.
Inductive transl_lblstmt_cont(
cenv:
compilenv) (
xenv:
exit_env):
lbl_stmt ->
cont ->
cont ->
Prop :=
|
tlsc_default:
forall k,
transl_lblstmt_cont cenv xenv LSnil k (
Kblock (
Kseq Sskip k))
|
tlsc_case:
forall i s ls k ts k',
transl_stmt cenv (
switch_env (
LScons i s ls)
xenv)
s =
OK ts ->
transl_lblstmt_cont cenv xenv ls k k' ->
transl_lblstmt_cont cenv xenv (
LScons i s ls)
k (
Kblock (
Kseq ts k')).
Lemma switch_descent:
forall cenv xenv k ls body s,
transl_lblstmt cenv (
switch_env ls xenv)
ls body =
OK s ->
exists k',
transl_lblstmt_cont cenv xenv ls k k'
/\ (
forall f sp e m,
plus step tge (
State f s k sp e m)
E0 (
State f body k'
sp e m)).
Proof.
induction ls;
intros.
-
monadInv H.
econstructor;
split.
econstructor.
intros.
eapply plus_two.
constructor.
constructor.
auto.
-
monadInv H.
exploit IHls;
eauto.
intros [
k' [
A B]].
econstructor;
split.
econstructor;
eauto.
intros.
eapply plus_star_trans.
eauto.
eapply star_left.
constructor.
apply star_one.
constructor.
reflexivity.
traceEq.
Qed.
Lemma switch_ascent:
forall f sp e m cenv xenv ls n ls',
lbl_stmt_tail ls n ls' ->
forall k k1,
transl_lblstmt_cont cenv xenv ls k k1 ->
exists k2,
star step tge (
State f (
Sexit n)
k1 sp e m)
E0 (
State f (
Sexit O)
k2 sp e m)
/\
transl_lblstmt_cont cenv xenv ls'
k k2.
Proof.
induction 1;
intros.
-
exists k1;
split;
auto.
apply star_refl.
-
inv H0.
exploit IHlbl_stmt_tail;
eauto.
intros (
k2 &
P &
Q).
exists k2;
split;
auto.
eapply star_left.
constructor.
eapply star_left.
constructor.
eexact P.
eauto.
auto.
Qed.
Lemma switch_match_cont:
forall cenv xenv k cs tk ls tk',
match_cont k tk cenv xenv cs ->
transl_lblstmt_cont cenv xenv ls tk tk' ->
match_cont (
Csharpminor.Kseq (
seq_of_lbl_stmt ls)
k)
tk'
cenv (
false ::
switch_env ls xenv)
cs.
Proof.
Lemma switch_match_states:
forall fn k e le m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk'
(
TRF:
transl_funbody cenv sz fn =
OK tfn)
(
TR:
transl_lblstmt cenv (
switch_env ls xenv)
ls body =
OK ts)
(
MINJ:
Mem.inject Mem.id_pua f m tm)
(
MCS:
match_callstack f m tm
(
Frame cenv tfn e le te sp lo hi ::
cs)
(
Mem.nextblock m) (
Mem.nextblock tm))
(
MK:
match_cont k tk cenv xenv cs)
(
TK:
transl_lblstmt_cont cenv xenv ls tk tk'),
exists S,
plus step tge (
State tfn (
Sexit O)
tk'
sp te tm)
E0 S
/\
match_states (
Csharpminor.State fn (
seq_of_lbl_stmt ls)
k e le m)
S.
Proof.
Lemma transl_lblstmt_suffix:
forall cenv xenv ls n ls',
lbl_stmt_tail ls n ls' ->
forall body ts,
transl_lblstmt cenv (
switch_env ls xenv)
ls body =
OK ts ->
exists body',
exists ts',
transl_lblstmt cenv (
switch_env ls'
xenv)
ls'
body' =
OK ts'.
Proof.
induction 1; intros.
- exists body, ts; auto.
- monadInv H0. eauto.
Qed.
Commutation between find_label and compilation
Section FIND_LABEL.
Variable lbl:
label.
Variable cenv:
compilenv.
Variable cs:
callstack.
Lemma transl_lblstmt_find_label_context:
forall xenv ls body ts tk1 tk2 ts'
tk',
transl_lblstmt cenv (
switch_env ls xenv)
ls body =
OK ts ->
transl_lblstmt_cont cenv xenv ls tk1 tk2 ->
find_label lbl body tk2 =
Some (
ts',
tk') ->
find_label lbl ts tk1 =
Some (
ts',
tk').
Proof.
induction ls; intros.
- monadInv H. inv H0. simpl. rewrite H1. auto.
- monadInv H. inv H0. simpl in H6. eapply IHls; eauto.
replace x with ts0 by congruence. simpl. rewrite H1. auto.
Qed.
Lemma transl_find_label:
forall s k xenv ts tk,
transl_stmt cenv xenv s =
OK ts ->
match_cont k tk cenv xenv cs ->
match Csharpminor.find_label lbl s k with
|
None =>
find_label lbl ts tk =
None
|
Some(
s',
k') =>
exists ts',
exists tk',
exists xenv',
find_label lbl ts tk =
Some(
ts',
tk')
/\
transl_stmt cenv xenv'
s' =
OK ts'
/\
match_cont k'
tk'
cenv xenv'
cs
end
with transl_lblstmt_find_label:
forall ls xenv body k ts tk tk1,
transl_lblstmt cenv (
switch_env ls xenv)
ls body =
OK ts ->
match_cont k tk cenv xenv cs ->
transl_lblstmt_cont cenv xenv ls tk tk1 ->
find_label lbl body tk1 =
None ->
match Csharpminor.find_label_ls lbl ls k with
|
None =>
find_label lbl ts tk =
None
|
Some(
s',
k') =>
exists ts',
exists tk',
exists xenv',
find_label lbl ts tk =
Some(
ts',
tk')
/\
transl_stmt cenv xenv'
s' =
OK ts'
/\
match_cont k'
tk'
cenv xenv'
cs
end.
Proof.
intros.
destruct s;
try (
monadInv H);
simpl;
auto.
exploit (
transl_find_label s1).
eauto.
eapply match_Kseq.
eexact EQ1.
eauto.
destruct (
Csharpminor.find_label lbl s1 (
Csharpminor.Kseq s2 k))
as [[
s'
k'] | ].
intros [
ts' [
tk' [
xenv' [
A [
B C]]]]].
exists ts';
exists tk';
exists xenv'.
intuition.
rewrite A;
auto.
intro.
rewrite H.
apply transl_find_label with xenv;
auto.
exploit (
transl_find_label s1).
eauto.
eauto.
destruct (
Csharpminor.find_label lbl s1 k)
as [[
s'
k'] | ].
intros [
ts' [
tk' [
xenv' [
A [
B C]]]]].
exists ts';
exists tk';
exists xenv'.
intuition.
rewrite A;
auto.
intro.
rewrite H.
apply transl_find_label with xenv;
auto.
apply transl_find_label with xenv.
auto.
econstructor;
eauto.
simpl.
rewrite EQ;
auto.
apply transl_find_label with (
true ::
xenv).
auto.
constructor;
auto.
simpl in H.
destruct (
switch_table l O)
as [
tbl dfl].
monadInv H.
exploit switch_descent;
eauto.
intros [
k' [
A B]].
eapply transl_lblstmt_find_label.
eauto.
eauto.
eauto.
reflexivity.
destruct o;
monadInv H;
auto.
destruct (
ident_eq lbl l).
exists x;
exists tk;
exists xenv;
auto.
apply transl_find_label with xenv;
auto.
intros.
destruct ls;
monadInv H;
simpl.
inv H1.
rewrite H2.
auto.
inv H1.
simpl in H7.
exploit (
transl_find_label s).
eauto.
eapply switch_match_cont;
eauto.
destruct (
Csharpminor.find_label lbl s (
Csharpminor.Kseq (
seq_of_lbl_stmt ls)
k))
as [[
s'
k''] | ].
intros [
ts' [
tk' [
xenv' [
A [
B C]]]]].
exists ts';
exists tk';
exists xenv';
intuition.
eapply transl_lblstmt_find_label_context;
eauto.
simpl.
replace x with ts0 by congruence.
rewrite H2.
auto.
intro.
eapply transl_lblstmt_find_label.
eauto.
auto.
eauto.
simpl.
replace x with ts0 by congruence.
rewrite H2.
auto.
Qed.
End FIND_LABEL.
Lemma transl_find_label_body:
forall cenv xenv size f tf k tk cs lbl s'
k',
transl_funbody cenv size f =
OK tf ->
match_cont k tk cenv xenv cs ->
Csharpminor.find_label lbl f.(
Csharpminor.fn_body) (
Csharpminor.call_cont k) =
Some (
s',
k') ->
exists ts',
exists tk',
exists xenv',
find_label lbl tf.(
fn_body) (
call_cont tk) =
Some(
ts',
tk')
/\
transl_stmt cenv xenv'
s' =
OK ts'
/\
match_cont k'
tk'
cenv xenv'
cs.
Proof.
The simulation diagram.
Fixpoint seq_left_depth (
s:
Csharpminor.stmt) :
nat :=
match s with
|
Csharpminor.Sseq s1 s2 =>
S (
seq_left_depth s1)
|
_ =>
O
end.
Definition measure (
S:
Csharpminor.state) :
nat :=
match S with
|
Csharpminor.State fn s k e le m =>
seq_left_depth s
|
_ =>
O
end.
Lemma alloc_variables_size:
forall l e m e'
m'
(
AVR :
alloc_variables_right e m l e'
m'),
Mem.size_mem m' =
align (
big_var_space l (
Mem.size_mem m)) 8.
Proof.
induction l;
simpl;
intros.
-
inv AVR.
symmetry;
eapply Mem.size_mem_aligned;
eauto.
-
inv AVR.
rewrite (
Mem.alloc_size_mem'
_ _ _ _ _ H3).
specialize (
IHl _ _ _ _ H6).
rewrite IHl.
rewrite <-!
Mem.align_distr.
rewrite !
Zmax_spec;
repeat destr;
omega.
Qed.
Lemma alloc_variables_size':
forall m,
align (
Mem.size_mem m) 8 <
Int.max_unsigned.
Proof.
Lemma alloc_none_size:
forall m lo hi,
Mem.alloc m lo hi =
None ->
Mem.conc_mem_alloc m lo hi 3%
nat =
None.
Proof.
Lemma conc_mem_alloc_size:
forall m lo hi ,
Alloc.size_mem_aux
(
Alloc.mk_block_list_aux
(
Alloc.get_size
(
PMap.set (
Mem.nextblock m) (
Some (
lo,
hi)) (
Mem.mem_blocksize m)))
(
Pos.to_nat (
Mem.nextblock m)))
=
align (
align (
Alloc.size_mem_aux
(
Alloc.mk_block_list_aux
(
Alloc.get_size (
Mem.mem_blocksize m))
(
pred (
Pos.to_nat ((
Mem.nextblock m)))))) 8 +
Z.max 0 (
hi -
lo)) 8.
Proof.
Lemma fr_rew:
forall l x
(
ALIGNED:
x =
align x 8),
align (
big_var_space l x) 8 =
align x 8 +
align (
big_var_space l 0) 8.
Proof.
induction l.
-
simpl.
intros;
simpl.
Transparent align.
unfold align at 3.
simpl.
intros;
omega.
-
simpl.
intros.
rewrite IHl;
auto.
rewrite IHl;
auto.
rewrite <-
Z.add_assoc.
rewrite <-
Mem.align_distr.
auto.
Qed.
Lemma alloc_variables_right_app'':
forall vars l e m mm ee'
mm'
e2,
alloc_variables_right e m l ee'
mm' ->
alloc_variables_right ee'
mm'
vars e2 mm ->
exists e2',
alloc_variables_right e m (
vars ++
l)
e2'
mm.
Proof.
Lemma alloc_variables_left_right':
forall (
vars :
list (
ident *
Z)) (
e :
Csharpminor.env)
(
m :
mem) (
e2 :
Csharpminor.env) (
m2 :
mem),
alloc_variables e m vars e2 m2 ->
exists e2',
alloc_variables_right e m (
rev vars)
e2'
m2.
Proof.
induction vars;
simpl;
intros.
inv H.
exists e2;
constructor.
inv H.
apply IHvars in H7;
auto.
destruct H7 as [
e2'
A].
destruct (
alloc_variables_right_app'' (
rev vars) ((
id,
sz)::
nil)
e m m2 (
PTree.set id (
b1,
Z.max 0
sz)
e)
m1 e2').
econstructor.
eauto.
constructor.
auto.
eexists;
eauto.
Qed.
Lemma odd_not_2_divides:
forall z,
Z.odd z =
true ->
~ (2 |
z).
Proof.
intros.
destruct 1.
subst.
unfold Z.odd in H.
destruct x;
simpl in *;
try congruence;
destruct p;
simpl in *;
try congruence.
Qed.
Lemma conc_mem_alloc_none_mu:
forall tm sz
(
ALLOC :
Mem.conc_mem_alloc tm 0
sz 3 =
None),
Mem.size_mem tm +
align (
Z.max 0
sz) 8 >=
Int.max_unsigned.
Proof.
Lemma alloc_variables_alloc_sp_ok:
forall p f m fn e m1 tf tm
(
INJ:
Mem.inject p f m tm)
(
AV:
alloc_variables empty_env m
(
VarSort.sort (
Csharpminor.fn_vars fn))
e m1)
(
TF:
transl_function fn =
OK tf)
(
ALLOC:
Mem.alloc tm 0 (
align
(
big_var_space
(
rev (
VarSort.sort (
Csharpminor.fn_vars fn)))
0)
8) =
None),
False.
Proof.
Lemma mcs_frame_env_ext:
forall f m tm ce tf x e le te sp lo hi cs b tb,
match_callstack f m tm (
Frame ce tf x le te sp lo hi ::
cs)
b tb ->
(
forall id,
x!
id =
e!
id) ->
match_callstack f m tm (
Frame ce tf e le te sp lo hi ::
cs)
b tb.
Proof.
Lemma fl_align_add':
forall l z1 z2,
0 <=
z1 <=
z2 ->
big_var_space l z1 <=
big_var_space l z2.
Proof.
Lemma big_var_space_app:
forall a b z,
big_var_space (
a ++
b)
z =
big_var_space a (
big_var_space b z).
Proof.
Lemma build_compilenv_le8:
forall ce sz f,
build_compilenv f = (
ce,
sz) ->
sz <=
big_var_space (
rev (
VarSort.sort (
Csharpminor.fn_vars f))) 0.
Proof.
Lemma external_call_bounds:
forall ef vargs m t vres m'
(
EC :
external_call ef ge vargs m t vres m'),
forall b,
Mem.bounds_of_block m'
b =
Mem.bounds_of_block m b.
Proof.
Lemma external_block_valid:
forall ef vargs m t vres m'
(
EC :
external_call ef ge vargs m t vres m')
b
(
VB:
Mem.valid_block m'
b),
Mem.valid_block m b.
Proof.
Lemma external_call_match_callstack:
forall f0 m tm cs
(
MCS :
match_callstack f0 m tm cs
(
Mem.nextblock m) (
Mem.nextblock tm))
ef vargs tvargs t vres vres'
m'
tm'
(
EC :
external_call ef ge vargs m t vres m')
(
EC' :
external_call ef ge tvargs tm t vres'
tm')
(
OUTOFREACH :
Mem.unchanged_on (
loc_out_of_reach f0 m)
tm tm'),
match_callstack f0 m'
tm'
cs
(
Mem.nextblock m) (
Mem.nextblock tm).
Proof.
Lemma transl_step_correct:
forall S1 t S2,
Csharpminor.step ge S1 t S2 ->
forall T1,
match_states S1 T1 ->
(
exists T2,
plus step tge T1 t T2 /\
match_states S2 T2)
\/ (
measure S2 <
measure S1 /\
t =
E0 /\
match_states S2 T1)%
nat.
Proof.
Lemma match_globalenvs_init:
forall m,
Genv.init_mem prog =
Some m ->
match_globalenvs (
Mem.flat_inj (
Mem.nextblock m)) (
Mem.nextblock m).
Proof.
Lemma transl_initial_states:
forall S,
Csharpminor.initial_state prog S ->
exists R,
Cminor.initial_state tprog R /\
match_states S R.
Proof.
Lemma transl_final_states:
forall S R r,
match_states S R ->
Csharpminor.final_state S r ->
Cminor.final_state R r.
Proof.
Theorem transl_program_correct:
forward_simulation (
Csharpminor.semantics prog) (
Cminor.semantics tprog).
Proof.
End TRANSLATION.