Semantic preservation for the SimplLocals pass.
Require Import FSets.
Require Import Coqlib Errors Ordered Maps Integers Floats.
Require Import AST Linking.
Require Import Values Memory Globalenvs Events Smallstep.
Require Import Ctypes Cop Clight SimplLocals.
Module VSF :=
FSetFacts.Facts(
VSet).
Module VSP :=
FSetProperties.Properties(
VSet).
Definition match_prog (
p tp:
program) :
Prop :=
match_program (
fun ctx f tf =>
transf_fundef f =
OK tf)
eq p tp
/\
prog_types tp =
prog_types p.
Lemma match_transf_program:
forall p tp,
transf_program p =
OK tp ->
match_prog p tp.
Proof.
Section PRESERVATION.
Existing Instance inject_perm_all.
Context `{
external_calls_prf:
ExternalCalls}.
Variable fn_stack_requirements:
ident ->
Z.
Variable prog:
program.
Variable tprog:
program.
Hypothesis TRANSF:
match_prog prog tprog.
Let ge :=
globalenv prog.
Let tge :=
globalenv tprog.
Lemma comp_env_preserved:
genv_cenv tge =
genv_cenv ge.
Proof.
unfold tge,
ge.
destruct prog,
tprog;
simpl.
destruct TRANSF as [
_ EQ].
simpl in EQ.
congruence.
Qed.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_match (
proj1 TRANSF)).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_match (
proj1 TRANSF)).
Lemma functions_translated:
forall (
v:
val) (
f:
fundef),
Genv.find_funct ge v =
Some f ->
exists tf,
Genv.find_funct tge v =
Some tf /\
transf_fundef f =
OK tf.
Proof (
Genv.find_funct_transf_partial (
proj1 TRANSF)).
Lemma function_ptr_translated:
forall (
b:
block) (
f:
fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
transf_fundef f =
OK tf.
Proof (
Genv.find_funct_ptr_transf_partial (
proj1 TRANSF)).
Lemma type_of_fundef_preserved:
forall fd tfd,
transf_fundef fd =
OK tfd ->
type_of_fundef tfd =
type_of_fundef fd.
Proof.
intros.
destruct fd;
monadInv H;
auto.
monadInv EQ.
simpl;
unfold type_of_function;
simpl.
auto.
Qed.
Matching between environments before and after
Inductive match_var (
f:
meminj) (
cenv:
compilenv) (
e:
env) (
m:
mem) (
te:
env) (
tle:
temp_env) (
id:
ident) :
Prop :=
|
match_var_lifted:
forall b ty chunk v tv
(
ENV:
e!
id =
Some(
b,
ty))
(
TENV:
te!
id =
None)
(
LIFTED:
VSet.mem id cenv =
true)
(
MAPPED:
f b =
None)
(
MODE:
access_mode ty =
By_value chunk)
(
LOAD:
Mem.load chunk m b 0 =
Some v)
(
TLENV:
tle!(
id) =
Some tv)
(
VINJ:
Val.inject f v tv),
match_var f cenv e m te tle id
|
match_var_not_lifted:
forall b ty b'
(
ENV:
e!
id =
Some(
b,
ty))
(
TENV:
te!
id =
Some(
b',
ty))
(
LIFTED:
VSet.mem id cenv =
false)
(
MAPPED:
f b =
Some(
b', 0)),
match_var f cenv e m te tle id
|
match_var_not_local:
forall
(
ENV:
e!
id =
None)
(
TENV:
te!
id =
None)
(
LIFTED:
VSet.mem id cenv =
false),
match_var f cenv e m te tle id.
Record match_envs (
f:
meminj) (
cenv:
compilenv)
(
e:
env) (
le:
temp_env) (
m:
mem) (
lo hi:
block)
(
te:
env) (
tle:
temp_env) (
tlo thi:
block) :
Prop :=
mk_match_envs {
me_vars:
forall id,
match_var f cenv e m te tle id;
me_temps:
forall id v,
le!
id =
Some v ->
(
exists tv,
tle!
id =
Some tv /\
Val.inject f v tv)
/\ (
VSet.mem id cenv =
true ->
v =
Vundef);
me_inj:
forall id1 b1 ty1 id2 b2 ty2,
e!
id1 =
Some(
b1,
ty1) ->
e!
id2 =
Some(
b2,
ty2) ->
id1 <>
id2 ->
b1 <>
b2;
me_tinj:
forall id1 b1 ty1 id2 b2 ty2,
te!
id1 =
Some(
b1,
ty1) ->
te!
id2 =
Some(
b2,
ty2) ->
id1 <>
id2 ->
b1 <>
b2;
me_range:
forall id b ty,
e!
id =
Some(
b,
ty) ->
Ple lo b /\
Plt b hi;
me_trange:
forall id b ty,
te!
id =
Some(
b,
ty) ->
Ple tlo b /\
Plt b thi;
me_mapped:
forall id b'
ty,
te!
id =
Some(
b',
ty) ->
exists b,
f b =
Some(
b', 0) /\
e!
id =
Some(
b,
ty);
me_flat:
forall id b'
ty b delta,
te!
id =
Some(
b',
ty) ->
f b =
Some(
b',
delta) ->
e!
id =
Some(
b,
ty) /\
delta = 0;
me_incr:
Ple lo hi;
me_tincr:
Ple tlo thi
}.
Invariance by change of memory and injection
Lemma match_envs_invariant:
forall f cenv e le m lo hi te tle tlo thi f'
m',
match_envs f cenv e le m lo hi te tle tlo thi ->
(
forall b chunk v,
f b =
None ->
Ple lo b /\
Plt b hi ->
Mem.load chunk m b 0 =
Some v ->
Mem.load chunk m'
b 0 =
Some v) ->
inject_incr f f' ->
(
forall b,
Ple lo b /\
Plt b hi ->
f'
b =
f b) ->
(
forall b b'
delta,
f'
b =
Some(
b',
delta) ->
Ple tlo b' /\
Plt b'
thi ->
f'
b =
f b) ->
match_envs f'
cenv e le m'
lo hi te tle tlo thi.
Proof.
intros until m';
intros ME LD INCR INV1 INV2.
destruct ME;
constructor;
eauto.
vars *)
intros.
generalize (
me_vars0 id);
intros MV;
inv MV.
eapply match_var_lifted;
eauto.
rewrite <-
MAPPED;
eauto.
eapply match_var_not_lifted;
eauto.
eapply match_var_not_local;
eauto.
temps *)
intros.
exploit me_temps0;
eauto.
intros [[
v' [
A B]]
C].
split;
auto.
exists v';
eauto.
mapped *)
intros.
exploit me_mapped0;
eauto.
intros [
b [
A B]].
exists b;
split;
auto.
flat *)
intros.
eapply me_flat0;
eauto.
rewrite <-
H0.
symmetry.
eapply INV2;
eauto.
Qed.
Invariance by external call
Lemma match_envs_extcall:
forall f cenv e le m lo hi te tle tlo thi tm f'
m',
match_envs f cenv e le m lo hi te tle tlo thi ->
Mem.unchanged_on (
loc_unmapped f)
m m' ->
inject_incr f f' ->
inject_separated f f'
m tm ->
Ple hi (
Mem.nextblock m) ->
Ple thi (
Mem.nextblock tm) ->
match_envs f'
cenv e le m'
lo hi te tle tlo thi.
Proof.
intros.
eapply match_envs_invariant;
eauto.
intros.
eapply Mem.load_unchanged_on;
eauto.
red in H2.
intros.
destruct (
f b)
as [[
b'
delta]|]
eqn:?.
eapply H1;
eauto.
destruct (
f'
b)
as [[
b'
delta]|]
eqn:?;
auto.
exploit H2;
eauto.
unfold Mem.valid_block.
intros [
A B].
xomegaContradiction.
intros.
destruct (
f b)
as [[
b''
delta']|]
eqn:?.
eauto.
exploit H2;
eauto.
unfold Mem.valid_block.
intros [
A B].
xomegaContradiction.
Qed.
Properties of values resulting from a cast
Lemma val_casted_load_result:
forall v ty chunk,
val_casted v ty ->
access_mode ty =
By_value chunk ->
Val.load_result chunk v =
v.
Proof.
intros.
inversion H;
clear H;
subst v ty;
simpl in H0.
-
destruct sz.
destruct si;
inversion H0;
clear H0;
subst chunk;
simpl in *;
congruence.
destruct si;
inversion H0;
clear H0;
subst chunk;
simpl in *;
congruence.
clear H1.
inv H0.
auto.
inversion H0;
clear H0;
subst chunk.
simpl in *.
destruct (
Int.eq n Int.zero);
subst n;
reflexivity.
-
inv H0;
auto.
-
inv H0;
auto.
-
inv H0;
auto.
-
inv H0.
unfold Mptr,
Val.load_result;
destruct Archi.ptr64;
auto.
-
inv H0.
unfold Mptr,
Val.load_result;
rewrite H1;
auto.
-
inv H0.
unfold Val.load_result;
rewrite H1;
auto.
-
inv H0.
unfold Mptr,
Val.load_result;
rewrite H1;
auto.
-
inv H0.
unfold Val.load_result;
rewrite H1;
auto.
-
discriminate.
-
discriminate.
-
discriminate.
Qed.
Lemma val_casted_inject:
forall f v v'
ty,
Val.inject f v v' ->
val_casted v ty ->
val_casted v'
ty.
Proof.
intros. inv H; auto.
inv H0; constructor; auto.
inv H0; constructor.
Qed.
Lemma forall2_val_casted_inject:
forall f vl vl',
Val.inject_list f vl vl' ->
forall tyl,
list_forall2 val_casted vl tyl ->
list_forall2 val_casted vl'
tyl.
Proof.
induction 1;
intros tyl F;
inv F;
constructor;
eauto.
eapply val_casted_inject;
eauto.
Qed.
Inductive val_casted_list:
list val ->
typelist ->
Prop :=
|
vcl_nil:
val_casted_list nil Tnil
|
vcl_cons:
forall v1 vl ty1 tyl,
val_casted v1 ty1 ->
val_casted_list vl tyl ->
val_casted_list (
v1 ::
vl) (
Tcons ty1 tyl).
Lemma val_casted_list_params:
forall params vl,
val_casted_list vl (
type_of_params params) ->
list_forall2 val_casted vl (
map snd params).
Proof.
induction params; simpl; intros.
inv H. constructor.
destruct a as [id ty]. inv H. constructor; auto.
Qed.
Correctness of make_cast
Lemma make_cast_correct:
forall e le m a v1 tto v2,
eval_expr tge e le m a v1 ->
sem_cast v1 (
typeof a)
tto m =
Some v2 ->
eval_expr tge e le m (
make_cast a tto)
v2.
Proof.
intros.
assert (
DFL:
eval_expr tge e le m (
Ecast a tto)
v2).
econstructor;
eauto.
unfold sem_cast,
make_cast in *.
destruct (
classify_cast (
typeof a)
tto);
auto.
destruct v1;
destruct Archi.ptr64;
inv H0;
auto.
destruct sz2;
auto.
destruct v1;
inv H0;
auto.
destruct v1;
inv H0;
auto.
destruct v1;
inv H0;
auto.
destruct v1;
inv H0;
auto.
destruct v1;
try discriminate.
destruct (
ident_eq id1 id2);
inv H0;
auto.
destruct v1;
try discriminate.
destruct (
ident_eq id1 id2);
inv H0;
auto.
inv H0;
auto.
Qed.
Debug annotations.
Lemma cast_typeconv:
forall v ty m,
val_casted v ty ->
sem_cast v ty (
typeconv ty)
m =
Some v.
Proof.
Lemma step_Sdebug_temp:
forall f id ty k e le m v,
le!
id =
Some v ->
val_casted v ty ->
step2 fn_stack_requirements tge (
State f (
Sdebug_temp id ty)
k e le m)
E0 (
State f Sskip k e le m).
Proof.
Lemma step_Sdebug_var:
forall f id ty k e le m b,
e!
id =
Some(
b,
ty) ->
(
step2 fn_stack_requirements)
tge (
State f (
Sdebug_var id ty)
k e le m)
E0 (
State f Sskip k e le m).
Proof.
Lemma step_Sset_debug:
forall f id ty a k e le m v v',
eval_expr tge e le m a v ->
sem_cast v (
typeof a)
ty m =
Some v' ->
plus (
step2 fn_stack_requirements)
tge (
State f (
Sset_debug id ty a)
k e le m)
E0 (
State f Sskip k e (
PTree.set id v'
le)
m).
Proof.
Lemma step_add_debug_vars:
forall f s e le m vars k,
(
forall id ty,
In (
id,
ty)
vars ->
exists b,
e!
id =
Some (
b,
ty)) ->
star (
step2 fn_stack_requirements)
tge (
State f (
add_debug_vars vars s)
k e le m)
E0 (
State f s k e le m).
Proof.
Remark bind_parameter_temps_inv:
forall id params args le le',
bind_parameter_temps params args le =
Some le' ->
~
In id (
var_names params) ->
le'!
id =
le!
id.
Proof.
induction params;
simpl;
intros.
destruct args;
inv H.
auto.
destruct a as [
id1 ty1].
destruct args;
try discriminate.
transitivity ((
PTree.set id1 v le)!
id).
eapply IHparams;
eauto.
apply PTree.gso.
intuition.
Qed.
Lemma step_add_debug_params:
forall f s k e le m params vl le1,
list_norepet (
var_names params) ->
list_forall2 val_casted vl (
map snd params) ->
bind_parameter_temps params vl le1 =
Some le ->
star (
step2 fn_stack_requirements)
tge (
State f (
add_debug_params params s)
k e le m)
E0 (
State f s k e le m).
Proof.
Preservation by assignment to lifted variable.
Lemma match_envs_assign_lifted:
forall f cenv e le m lo hi te tle tlo thi b ty v m'
id tv,
match_envs f cenv e le m lo hi te tle tlo thi ->
e!
id =
Some(
b,
ty) ->
val_casted v ty ->
Val.inject f v tv ->
assign_loc ge ty m b Ptrofs.zero v m' ->
VSet.mem id cenv =
true ->
match_envs f cenv e le m'
lo hi te (
PTree.set id tv tle)
tlo thi.
Proof.
Preservation by assignment to a temporary
Lemma match_envs_set_temp:
forall f cenv e le m lo hi te tle tlo thi id v tv x,
match_envs f cenv e le m lo hi te tle tlo thi ->
Val.inject f v tv ->
check_temp cenv id =
OK x ->
match_envs f cenv e (
PTree.set id v le)
m lo hi te (
PTree.set id tv tle)
tlo thi.
Proof.
Lemma match_envs_set_opttemp:
forall f cenv e le m lo hi te tle tlo thi optid v tv x,
match_envs f cenv e le m lo hi te tle tlo thi ->
Val.inject f v tv ->
check_opttemp cenv optid =
OK x ->
match_envs f cenv e (
set_opttemp optid v le)
m lo hi te (
set_opttemp optid tv tle)
tlo thi.
Proof.
Extensionality with respect to temporaries
Lemma match_envs_temps_exten:
forall f cenv e le m lo hi te tle tlo thi tle',
match_envs f cenv e le m lo hi te tle tlo thi ->
(
forall id,
tle'!
id =
tle!
id) ->
match_envs f cenv e le m lo hi te tle'
tlo thi.
Proof.
Invariance by assignment to an irrelevant temporary
Lemma match_envs_change_temp:
forall f cenv e le m lo hi te tle tlo thi id v,
match_envs f cenv e le m lo hi te tle tlo thi ->
le!
id =
None ->
VSet.mem id cenv =
false ->
match_envs f cenv e le m lo hi te (
PTree.set id v tle)
tlo thi.
Proof.
Properties of cenv_for.
Definition cenv_for_gen (
atk:
VSet.t) (
vars:
list (
ident *
type)) :
compilenv :=
List.fold_right (
add_local_variable atk)
VSet.empty vars.
Remark add_local_variable_charact:
forall id ty atk cenv id1,
VSet.In id1 (
add_local_variable atk (
id,
ty)
cenv) <->
VSet.In id1 cenv \/
exists chunk,
access_mode ty =
By_value chunk /\
id =
id1 /\
VSet.mem id atk =
false.
Proof.
Lemma cenv_for_gen_domain:
forall atk id vars,
VSet.In id (
cenv_for_gen atk vars) ->
In id (
var_names vars).
Proof.
Lemma cenv_for_gen_by_value:
forall atk id ty vars,
In (
id,
ty)
vars ->
list_norepet (
var_names vars) ->
VSet.In id (
cenv_for_gen atk vars) ->
exists chunk,
access_mode ty =
By_value chunk.
Proof.
induction vars;
simpl;
intros.
contradiction.
destruct a as [
id1 ty1].
simpl in H0.
inv H0.
rewrite add_local_variable_charact in H1.
destruct H;
destruct H1 as [
A | [
chunk [
A [
B C]]]].
inv H.
elim H4.
eapply cenv_for_gen_domain;
eauto.
inv H.
exists chunk;
auto.
eauto.
subst id1.
elim H4.
change id with (
fst (
id,
ty)).
apply in_map;
auto.
Qed.
Lemma cenv_for_gen_compat:
forall atk id vars,
VSet.In id (
cenv_for_gen atk vars) ->
VSet.mem id atk =
false.
Proof.
induction vars;
simpl;
intros.
rewrite VSF.empty_iff in H.
contradiction.
destruct a as [
id1 ty1].
rewrite add_local_variable_charact in H.
destruct H as [
A | [
chunk [
A [
B C]]]].
auto.
congruence.
Qed.
Compatibility between a compilation environment and an address-taken set.
Definition compat_cenv (
atk:
VSet.t) (
cenv:
compilenv) :
Prop :=
forall id,
VSet.In id atk ->
VSet.In id cenv ->
False.
Lemma compat_cenv_for:
forall f,
compat_cenv (
addr_taken_stmt f.(
fn_body)) (
cenv_for f).
Proof.
Lemma compat_cenv_union_l:
forall atk1 atk2 cenv,
compat_cenv (
VSet.union atk1 atk2)
cenv ->
compat_cenv atk1 cenv.
Proof.
intros;
red;
intros.
eapply H;
eauto.
apply VSet.union_2;
auto.
Qed.
Lemma compat_cenv_union_r:
forall atk1 atk2 cenv,
compat_cenv (
VSet.union atk1 atk2)
cenv ->
compat_cenv atk2 cenv.
Proof.
intros;
red;
intros.
eapply H;
eauto.
apply VSet.union_3;
auto.
Qed.
Lemma compat_cenv_empty:
forall cenv,
compat_cenv VSet.empty cenv.
Proof.
Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty:
compat.
Allocation and initialization of parameters
Lemma alloc_variables_nextblock:
forall ge e m vars e'
m',
alloc_variables ge e m vars e'
m' ->
Ple (
Mem.nextblock m) (
Mem.nextblock m').
Proof.
Lemma alloc_variables_range:
forall ge id b ty e m vars e'
m',
alloc_variables ge e m vars e'
m' ->
e'!
id =
Some(
b,
ty) ->
e!
id =
Some(
b,
ty) \/
Ple (
Mem.nextblock m)
b /\
Plt b (
Mem.nextblock m').
Proof.
Lemma alloc_variables_injective:
forall ge id1 b1 ty1 id2 b2 ty2 e m vars e'
m',
alloc_variables ge e m vars e'
m' ->
(
e!
id1 =
Some(
b1,
ty1) ->
e!
id2 =
Some(
b2,
ty2) ->
id1 <>
id2 ->
b1 <>
b2) ->
(
forall id b ty,
e!
id =
Some(
b,
ty) ->
Plt b (
Mem.nextblock m)) ->
(
e'!
id1 =
Some(
b1,
ty1) ->
e'!
id2 =
Some(
b2,
ty2) ->
id1 <>
id2 ->
b1 <>
b2).
Proof.
Lemma match_alloc_variables:
forall cenv e m vars e'
m',
alloc_variables ge e m vars e'
m' ->
forall j g tm te,
list_norepet (
var_names vars) ->
Mem.inject j g m tm ->
exists j',
exists te',
exists tm',
alloc_variables tge te tm (
remove_lifted cenv vars)
te'
tm'
/\
Mem.inject j'
g m'
tm'
/\
inject_incr j j'
/\ (
forall b,
Mem.valid_block m b ->
j'
b =
j b)
/\ (
forall b b'
delta,
j'
b =
Some(
b',
delta) ->
Mem.valid_block tm b' ->
j'
b =
j b)
/\ (
forall b b'
delta,
j'
b =
Some(
b',
delta) -> ~
Mem.valid_block tm b' ->
exists id,
exists ty,
e'!
id =
Some(
b,
ty) /\
te'!
id =
Some(
b',
ty) /\
delta = 0)
/\ (
forall id ty,
In (
id,
ty)
vars ->
exists b,
e'!
id =
Some(
b,
ty)
/\
if VSet.mem id cenv
then te'!
id =
te!
id /\
j'
b =
None
else exists tb,
te'!
id =
Some(
tb,
ty) /\
j'
b =
Some(
tb, 0))
/\ (
forall id, ~
In id (
var_names vars) ->
e'!
id =
e!
id /\
te'!
id =
te!
id)
.
Proof.
induction 1;
intros j g tm te LNR MINJ .
-
exists j;
exists te;
exists tm.
simpl.
split.
constructor.
split.
auto.
split.
auto.
split.
auto.
split.
auto.
split.
intros.
elim H0.
eapply Mem.valid_block_inject_2;
eauto.
split.
tauto.
split.
auto.
congruence.
-
simpl in LNR.
inv LNR.
simpl.
destruct (
VSet.mem id cenv)
eqn:?.
simpl.
+
exploit Mem.alloc_left_unmapped_inject;
eauto.
intros [
j1 [
A [
B [
C D]]]].
exploit IHalloc_variables;
eauto.
intros id1 b0 ty1 id2 b2 ty2 b t1 t2. *) { *) rewrite ! PTree.gsspec. repeat destr. *) intros. eapply INJUNIQUE. *) apply H1. apply H2. eauto. eauto. rewrite <- D. eauto. intro; subst. congruence. *) rewrite <- D. eauto. intro; subst. congruence. *) } *)
instantiate (1 :=
te).
intros [
j' [
te' [
tm' [
J [
K [
L [
M [
N [
Q [
O P]]]]]]]]]].
exists j';
exists te';
exists tm'.
split.
auto.
split.
auto.
split.
eapply inject_incr_trans;
eauto.
split.
intros.
transitivity (
j1 b).
apply M.
eapply Mem.valid_block_alloc;
eauto.
apply D.
apply Mem.valid_not_valid_diff with m;
auto.
eapply Mem.fresh_block_alloc;
eauto.
split.
intros.
transitivity (
j1 b).
eapply N;
eauto.
destruct (
eq_block b b1);
auto.
subst.
assert (
j'
b1 =
j1 b1).
apply M.
eapply Mem.valid_new_block;
eauto.
congruence.
split.
exact Q.
split.
intros.
destruct (
ident_eq id0 id).
same var *)
subst id0.
assert (
ty0 =
ty).
destruct H1.
congruence.
elim H3.
unfold var_names.
change id with (
fst (
id,
ty0)).
apply in_map;
auto.
subst ty0.
exploit P;
eauto.
intros [
X Y].
rewrite Heqb.
rewrite X.
rewrite Y.
exists b1.
split.
apply PTree.gss.
split.
auto.
rewrite M.
auto.
eapply Mem.valid_new_block;
eauto.
other vars *)
eapply O;
eauto.
destruct H1.
congruence.
auto.
intros.
exploit (
P id0).
tauto.
intros [
X Y].
rewrite X;
rewrite Y.
split;
auto.
apply PTree.gso.
intuition.
{ *) intros id1 b0 ty1 id2 b2 ty2 b t1 t2 NIN1 NIN2 IN1 IN2 INJ1 INJ2. *) destruct (peq id1 id2). congruence. *)
*) *) *) *) *) *) *)
*)
destruct (peq id1 id). *) - subst. *) edestruct P as (AA & BB). apply H3. *) rewrite AA in IN1. rewrite PTree.gss in IN1. inv IN1. *)
destruct (in_dec peq id1 (map fst vars)). *) - rewrite in_map_iff in i. destruct i as (x & EQ & i). subst. destruct x; simpl in *. *) destruct (O _ _ i) as (bb & E2 & EQ). *) rewrite IN1 in E2. inv E2. rewrite INJ1 in EQ. destr_in EQ. *) destruct EQ as (tb & TE1 & HH); inv HH. *) destruct (in_dec peq id2 (map fst vars)). *) + rewrite in_map_iff in i1. destruct i1 as (x & EQ & i1). subst. destruct x; simpl in *. *) destruct (O _ _ i1) as (bb2 & E2 & EQ). *) rewrite IN2 in E2. inv E2. rewrite INJ2 in EQ. destr_in EQ. *) destruct EQ as (tb2 & TE2 & HH); inv HH. *) eapply INJ. rewrite PTree.gso. apply NIN1. *) intro; subst. apply H3. unfold var_names. *) rewrite in_map_iff. exists (id,t); split ; eauto. *) rewrite PTree.gso. apply NIN2. *) intro; subst. apply H3. unfold var_names. *) rewrite in_map_iff. exists (id,t0); split ; eauto. *) eauto. eauto. eauto. eauto. *) + destruct (P _ n) as (AA & BB). *) rewrite AA in IN2. rewrite PTree.gsspec in IN2. destr_in IN2. inv IN2. *)
+
exploit Mem.alloc_parallel_inject.
eauto.
eauto.
apply Zle_refl.
apply Zle_refl.
intros [
j1 [
tm1 [
tb1 [
A [
B [
C [
D E]]]]]]].
exploit IHalloc_variables;
eauto.
instantiate (1 :=
PTree.set id (
tb1,
ty)
te).
intros [
j' [
te' [
tm' [
J [
K [
L [
M [
N [
Q [
O P]]]]]]]]]].
exists j';
exists te';
exists tm'.
split.
simpl.
econstructor;
eauto.
rewrite comp_env_preserved;
auto.
split.
auto.
split.
eapply inject_incr_trans;
eauto.
split.
intros.
transitivity (
j1 b).
apply M.
eapply Mem.valid_block_alloc;
eauto.
apply E.
apply Mem.valid_not_valid_diff with m;
auto.
eapply Mem.fresh_block_alloc;
eauto.
split.
intros.
transitivity (
j1 b).
eapply N;
eauto.
eapply Mem.valid_block_alloc;
eauto.
destruct (
eq_block b b1);
auto.
subst.
assert (
j'
b1 =
j1 b1).
apply M.
eapply Mem.valid_new_block;
eauto.
rewrite H5 in H1.
rewrite D in H1.
inv H1.
eelim Mem.fresh_block_alloc;
eauto.
split.
intros.
destruct (
eq_block b'
tb1).
subst b'.
rewrite (
N _ _ _ H1)
in H1.
destruct (
eq_block b b1).
subst b.
rewrite D in H1;
inv H1.
exploit (
P id);
auto.
intros [
X Y].
exists id;
exists ty.
rewrite X;
rewrite Y.
repeat rewrite PTree.gss.
auto.
rewrite E in H1;
auto.
elim H2.
eapply Mem.valid_block_inject_2;
eauto.
eapply Mem.valid_new_block;
eauto.
eapply Q;
eauto.
unfold Mem.valid_block in *.
exploit Mem.nextblock_alloc.
eexact A.
exploit Mem.alloc_result.
eexact A.
unfold block;
xomega.
split.
intros.
destruct (
ident_eq id0 id).
same var *)
subst id0.
assert (
ty0 =
ty).
destruct H1.
congruence.
elim H3.
unfold var_names.
change id with (
fst (
id,
ty0)).
apply in_map;
auto.
subst ty0.
exploit P;
eauto.
intros [
X Y].
rewrite Heqb.
rewrite X.
rewrite Y.
exists b1.
split.
apply PTree.gss.
exists tb1;
split.
apply PTree.gss.
rewrite M.
auto.
eapply Mem.valid_new_block;
eauto.
other vars *)
exploit (
O id0 ty0).
destruct H1.
congruence.
auto.
rewrite PTree.gso;
auto.
intros.
exploit (
P id0).
tauto.
intros [
X Y].
rewrite X;
rewrite Y.
split;
apply PTree.gso;
intuition.
Qed.
Lemma alloc_variables_load:
forall e m vars e'
m',
alloc_variables ge e m vars e'
m' ->
forall chunk b ofs v,
Mem.load chunk m b ofs =
Some v ->
Mem.load chunk m'
b ofs =
Some v.
Proof.
Lemma sizeof_by_value:
forall ty chunk,
access_mode ty =
By_value chunk ->
size_chunk chunk <=
sizeof ge ty.
Proof.
Definition env_initial_value (
e:
env) (
m:
mem) :=
forall id b ty chunk,
e!
id =
Some(
b,
ty) ->
access_mode ty =
By_value chunk ->
Mem.load chunk m b 0 =
Some Vundef.
Lemma alloc_variables_initial_value:
forall e m vars e'
m',
alloc_variables ge e m vars e'
m' ->
env_initial_value e m ->
env_initial_value e'
m'.
Proof.
Lemma create_undef_temps_charact:
forall id ty vars,
In (
id,
ty)
vars -> (
create_undef_temps vars)!
id =
Some Vundef.
Proof.
induction vars;
simpl;
intros.
contradiction.
destruct H.
subst a.
apply PTree.gss.
destruct a as [
id1 ty1].
rewrite PTree.gsspec.
destruct (
peq id id1);
auto.
Qed.
Lemma create_undef_temps_inv:
forall vars id v, (
create_undef_temps vars)!
id =
Some v ->
v =
Vundef /\
In id (
var_names vars).
Proof.
induction vars;
simpl;
intros.
rewrite PTree.gempty in H;
congruence.
destruct a as [
id1 ty1].
rewrite PTree.gsspec in H.
destruct (
peq id id1).
inv H.
auto.
exploit IHvars;
eauto.
tauto.
Qed.
Lemma create_undef_temps_exten:
forall id l1 l2,
(
In id (
var_names l1) <->
In id (
var_names l2)) ->
(
create_undef_temps l1)!
id = (
create_undef_temps l2)!
id.
Proof.
Remark var_names_app:
forall vars1 vars2,
var_names (
vars1 ++
vars2) =
var_names vars1 ++
var_names vars2.
Proof.
Remark filter_app:
forall (
A:
Type) (
f:
A ->
bool)
l1 l2,
List.filter f (
l1 ++
l2) =
List.filter f l1 ++
List.filter f l2.
Proof.
induction l1; simpl; intros.
auto.
destruct (f a). simpl. decEq; auto. auto.
Qed.
Remark filter_charact:
forall (
A:
Type) (
f:
A ->
bool)
x l,
In x (
List.filter f l) <->
In x l /\
f x =
true.
Proof.
induction l; simpl. tauto.
destruct (f a) eqn:?.
simpl. rewrite IHl. intuition congruence.
intuition congruence.
Qed.
Remark filter_norepet:
forall (
A:
Type) (
f:
A ->
bool)
l,
list_norepet l ->
list_norepet (
List.filter f l).
Proof.
induction 1;
simpl.
constructor.
destruct (
f hd);
auto.
constructor;
auto.
rewrite filter_charact.
tauto.
Qed.
Remark filter_map:
forall (
A B:
Type) (
f:
A ->
B) (
pa:
A ->
bool) (
pb:
B ->
bool),
(
forall a,
pb (
f a) =
pa a) ->
forall l,
List.map f (
List.filter pa l) =
List.filter pb (
List.map f l).
Proof.
induction l; simpl.
auto.
rewrite H. destruct (pa a); simpl; congruence.
Qed.
Lemma create_undef_temps_lifted:
forall id f,
~
In id (
var_names (
fn_params f)) ->
(
create_undef_temps (
add_lifted (
cenv_for f) (
fn_vars f) (
fn_temps f))) !
id =
(
create_undef_temps (
add_lifted (
cenv_for f) (
fn_params f ++
fn_vars f) (
fn_temps f))) !
id.
Proof.
Lemma vars_and_temps_properties:
forall cenv params vars temps,
list_norepet (
var_names params ++
var_names vars) ->
list_disjoint (
var_names params) (
var_names temps) ->
list_norepet (
var_names params)
/\
list_norepet (
var_names (
remove_lifted cenv (
params ++
vars)))
/\
list_disjoint (
var_names params) (
var_names (
add_lifted cenv vars temps)).
Proof.
Theorem match_envs_alloc_variables:
forall cenv m vars e m'
temps j g tm,
alloc_variables ge empty_env m vars e m' ->
list_norepet (
var_names vars) ->
Mem.inject j g m tm ->
(
forall id ty,
In (
id,
ty)
vars ->
VSet.mem id cenv =
true ->
exists chunk,
access_mode ty =
By_value chunk) ->
(
forall id,
VSet.mem id cenv =
true ->
In id (
var_names vars)) ->
exists j',
exists te,
exists tm',
alloc_variables tge empty_env tm (
remove_lifted cenv vars)
te tm'
/\
match_envs j'
cenv e (
create_undef_temps temps)
m' (
Mem.nextblock m) (
Mem.nextblock m')
te (
create_undef_temps (
add_lifted cenv vars temps)) (
Mem.nextblock tm) (
Mem.nextblock tm')
/\
Mem.inject j'
g m'
tm'
/\
inject_incr j j'
/\ (
forall b,
Mem.valid_block m b ->
j'
b =
j b)
/\ (
forall b b'
delta,
j'
b =
Some(
b',
delta) ->
Mem.valid_block tm b' ->
j'
b =
j b)
/\ (
forall id ty,
In (
id,
ty)
vars ->
VSet.mem id cenv =
false ->
exists b,
te!
id =
Some(
b,
ty))
.
Proof.
Lemma assign_loc_inject:
forall f g ty m loc ofs v m'
tm loc'
ofs'
v',
assign_loc ge ty m loc ofs v m' ->
Val.inject f (
Vptr loc ofs) (
Vptr loc'
ofs') ->
Val.inject f v v' ->
Mem.inject f g m tm ->
exists tm',
assign_loc tge ty tm loc'
ofs'
v'
tm'
/\
Mem.inject f g m'
tm'
/\ (
forall b chunk v,
f b =
None ->
Mem.load chunk m b 0 =
Some v ->
Mem.load chunk m'
b 0 =
Some v).
Proof.
Lemma assign_loc_nextblock:
forall ge ty m b ofs v m',
assign_loc ge ty m b ofs v m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
Lemma assign_loc_stack:
forall ge ty m b ofs v m',
assign_loc ge ty m b ofs v m' ->
Mem.stack m' =
Mem.stack m.
Proof.
Theorem store_params_correct:
forall j g f k cenv le lo hi te tlo thi e m params args m',
bind_parameters ge e m params args m' ->
forall s tm tle1 tle2 targs,
list_norepet (
var_names params) ->
list_forall2 val_casted args (
map snd params) ->
Val.inject_list j args targs ->
match_envs j cenv e le m lo hi te tle1 tlo thi ->
Mem.inject j g m tm ->
(
forall id, ~
In id (
var_names params) ->
tle2!
id =
tle1!
id) ->
(
forall id,
In id (
var_names params) ->
le!
id =
None) ->
exists tle,
exists tm',
star (
step2 fn_stack_requirements)
tge (
State f (
store_params cenv params s)
k te tle tm)
E0 (
State f s k te tle tm')
/\
bind_parameter_temps params targs tle2 =
Some tle
/\
Mem.inject j g m'
tm'
/\
match_envs j cenv e le m'
lo hi te tle tlo thi
/\
Mem.nextblock tm' =
Mem.nextblock tm
/\
Mem.stack tm' =
Mem.stack tm.
Proof.
Lemma bind_parameters_nextblock:
forall ge e m params args m',
bind_parameters ge e m params args m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
Lemma bind_parameters_load:
forall ge e chunk b ofs,
(
forall id b'
ty,
e!
id =
Some(
b',
ty) ->
b <>
b') ->
forall m params args m',
bind_parameters ge e m params args m' ->
Mem.load chunk m'
b ofs =
Mem.load chunk m b ofs.
Proof.
Freeing of local variables
Lemma free_blocks_of_env_perm_1:
forall ce m e m'
id b ty ofs k p,
Mem.free_list m (
blocks_of_env ce e) =
Some m' ->
e!
id =
Some(
b,
ty) ->
Mem.perm m'
b ofs k p ->
0 <=
ofs <
sizeof ce ty ->
False.
Proof.
Lemma free_list_perm':
forall b lo hi l m m',
Mem.free_list m l =
Some m' ->
In (
b,
lo,
hi)
l ->
Mem.range_perm m b lo hi Cur Freeable.
Proof.
induction l;
simpl;
intros.
contradiction.
destruct a as [[
b1 lo1]
hi1].
destruct (
Mem.free m b1 lo1 hi1)
as [
m1|]
eqn:?;
try discriminate.
destruct H0.
inv H0.
eapply Mem.free_range_perm;
eauto.
red;
intros.
eapply Mem.perm_free_3;
eauto.
eapply IHl;
eauto.
Qed.
Lemma free_blocks_of_env_perm_2:
forall ce m e m'
id b ty,
Mem.free_list m (
blocks_of_env ce e) =
Some m' ->
e!
id =
Some(
b,
ty) ->
Mem.range_perm m b 0 (
sizeof ce ty)
Cur Freeable.
Proof.
Fixpoint freelist_no_overlap (
l:
list (
block *
Z *
Z)) :
Prop :=
match l with
|
nil =>
True
| (
b,
lo,
hi) ::
l' =>
freelist_no_overlap l' /\
(
forall b'
lo'
hi',
In (
b',
lo',
hi')
l' ->
b' <>
b \/
hi' <=
lo \/
hi <=
lo')
end.
Lemma can_free_list:
forall l m,
(
forall b lo hi,
In (
b,
lo,
hi)
l ->
Mem.range_perm m b lo hi Cur Freeable) ->
freelist_no_overlap l ->
exists m',
Mem.free_list m l =
Some m'.
Proof.
induction l;
simpl;
intros.
-
exists m;
auto.
-
destruct a as [[
b lo]
hi].
destruct H0.
destruct (
Mem.range_perm_free m b lo hi)
as [
m1 A];
auto.
rewrite A.
apply IHl;
auto.
intros.
red;
intros.
eapply Mem.perm_free_1;
eauto.
exploit H1;
eauto.
intros [
B|
B].
auto.
right;
omega.
eapply H;
eauto.
Qed.
Lemma blocks_of_env_no_overlap:
forall (
ge:
genv)
j g cenv e le m lo hi te tle tlo thi tm,
match_envs j cenv e le m lo hi te tle tlo thi ->
Mem.inject j g m tm ->
(
forall id b ty,
e!
id =
Some(
b,
ty) ->
Mem.range_perm m b 0 (
sizeof ge ty)
Cur Freeable) ->
forall l,
list_norepet (
List.map fst l) ->
(
forall id bty,
In (
id,
bty)
l ->
te!
id =
Some bty) ->
freelist_no_overlap (
List.map (
block_of_binding ge)
l).
Proof.
Lemma free_list_right_inject:
forall j g m1 l m2 m2',
Mem.inject j g m1 m2 ->
Mem.free_list m2 l =
Some m2' ->
(
forall b1 b2 delta lo hi ofs k p,
j b1 =
Some(
b2,
delta) ->
In (
b2,
lo,
hi)
l ->
Mem.perm m1 b1 ofs k p ->
lo <=
ofs +
delta <
hi ->
False) ->
Mem.inject j g m1 m2'.
Proof.
induction l;
simpl;
intros.
congruence.
destruct a as [[
b lo]
hi].
destruct (
Mem.free m2 b lo hi)
as [
m21|]
eqn:?;
try discriminate.
eapply IHl with (
m2 :=
m21);
eauto.
eapply Mem.free_right_inject;
eauto.
Qed.
Lemma blocks_of_env_translated:
forall e,
blocks_of_env tge e =
blocks_of_env ge e.
Proof.
Theorem match_envs_free_blocks:
forall j g cenv e le m lo hi te tle tlo thi m'
tm,
match_envs j cenv e le m lo hi te tle tlo thi ->
Mem.inject j g m tm ->
Mem.free_list m (
blocks_of_env ge e) =
Some m' ->
exists tm',
Mem.free_list tm (
blocks_of_env tge te) =
Some tm'
/\
Mem.inject j g m'
tm'.
Proof.
Matching global environments
Inductive match_globalenvs (
f:
meminj) (
bound:
block):
Prop :=
|
mk_match_globalenvs
(
DOMAIN:
forall b,
Plt b bound ->
f b =
Some(
b, 0))
(
IMAGE:
forall b1 b2 delta,
f b1 =
Some(
b2,
delta) ->
Plt b2 bound ->
b1 =
b2)
(
SYMBOLS:
forall id b,
Genv.find_symbol ge id =
Some b ->
Plt b bound)
(
FUNCTIONS:
forall b fd,
Genv.find_funct_ptr ge b =
Some fd ->
Plt b bound)
(
VARINFOS:
forall b gv,
Genv.find_var_info ge b =
Some gv ->
Plt b bound).
Lemma match_globalenvs_preserves_globals:
forall f,
(
exists bound,
match_globalenvs f bound) ->
meminj_preserves_globals ge f.
Proof.
intros. destruct H as [bound MG]. inv MG.
split; intros. eauto. split; intros. eauto. symmetry. eapply IMAGE; eauto.
Qed.
Evaluation of expressions
Section EVAL_EXPR.
Variables e te:
env.
Variables le tle:
temp_env.
Variables m tm:
mem.
Variable f:
meminj.
Variable g:
frameinj.
Variable cenv:
compilenv.
Variables lo hi tlo thi:
block.
Hypothesis MATCH:
match_envs f cenv e le m lo hi te tle tlo thi.
Hypothesis MEMINJ:
Mem.inject f g m tm.
Hypothesis GLOB:
exists bound,
match_globalenvs f bound.
Lemma typeof_simpl_expr:
forall a,
typeof (
simpl_expr cenv a) =
typeof a.
Proof.
destruct a;
simpl;
auto.
destruct (
VSet.mem i cenv);
auto.
Qed.
Lemma deref_loc_inject:
forall ty loc ofs v loc'
ofs',
deref_loc ty m loc ofs v ->
Val.inject f (
Vptr loc ofs) (
Vptr loc'
ofs') ->
exists tv,
deref_loc ty tm loc'
ofs'
tv /\
Val.inject f v tv.
Proof.
Lemma eval_simpl_expr:
forall a v,
eval_expr ge e le m a v ->
compat_cenv (
addr_taken_expr a)
cenv ->
exists tv,
eval_expr tge te tle tm (
simpl_expr cenv a)
tv /\
Val.inject f v tv
with eval_simpl_lvalue:
forall a b ofs,
eval_lvalue ge e le m a b ofs ->
compat_cenv (
addr_taken_expr a)
cenv ->
match a with Evar id ty =>
VSet.mem id cenv =
false |
_ =>
True end ->
exists b',
exists ofs',
eval_lvalue tge te tle tm (
simpl_expr cenv a)
b'
ofs' /\
Val.inject f (
Vptr b ofs) (
Vptr b'
ofs').
Proof.
destruct 1;
simpl;
intros.
const *)
exists (
Vint i);
split;
auto.
constructor.
exists (
Vfloat f0);
split;
auto.
constructor.
exists (
Vsingle f0);
split;
auto.
constructor.
exists (
Vlong i);
split;
auto.
constructor.
tempvar *)
exploit me_temps;
eauto.
intros [[
tv [
A B]]
C].
exists tv;
split;
auto.
constructor;
auto.
addrof *)
exploit eval_simpl_lvalue;
eauto.
destruct a;
auto with compat.
destruct a;
auto.
destruct (
VSet.mem i cenv)
eqn:?;
auto.
elim (
H0 i).
apply VSet.singleton_2.
auto.
apply VSet.mem_2.
auto.
intros [
b' [
ofs' [
A B]]].
exists (
Vptr b'
ofs');
split;
auto.
constructor;
auto.
unop *)
exploit eval_simpl_expr;
eauto.
intros [
tv1 [
A B]].
exploit sem_unary_operation_inject;
eauto.
intros [
tv [
C D]].
exists tv;
split;
auto.
econstructor;
eauto.
rewrite typeof_simpl_expr;
auto.
binop *)
exploit eval_simpl_expr.
eexact H.
eauto with compat.
intros [
tv1 [
A B]].
exploit eval_simpl_expr.
eexact H0.
eauto with compat.
intros [
tv2 [
C D]].
exploit sem_binary_operation_inject;
eauto.
intros [
tv [
E F]].
exists tv;
split;
auto.
econstructor;
eauto.
repeat rewrite typeof_simpl_expr;
rewrite comp_env_preserved;
auto.
cast *)
exploit eval_simpl_expr;
eauto.
intros [
tv1 [
A B]].
exploit sem_cast_inject;
eauto.
intros [
tv2 [
C D]].
exists tv2;
split;
auto.
econstructor.
eauto.
rewrite typeof_simpl_expr;
auto.
sizeof *)
econstructor;
split.
constructor.
rewrite comp_env_preserved;
auto.
alignof *)
econstructor;
split.
constructor.
rewrite comp_env_preserved;
auto.
rval *)
assert (
EITHER: (
exists id,
exists ty,
a =
Evar id ty /\
VSet.mem id cenv =
true)
\/ (
match a with Evar id _ =>
VSet.mem id cenv =
false |
_ =>
True end)).
destruct a;
auto.
destruct (
VSet.mem i cenv)
eqn:?;
auto.
left;
exists i;
exists t;
auto.
destruct EITHER as [ [
id [
ty [
EQ OPT]]] |
NONOPT ].
a variable pulled out of memory *)
subst a.
simpl.
rewrite OPT.
exploit me_vars;
eauto.
instantiate (1 :=
id).
intros MV.
inv H;
inv MV;
try congruence.
rewrite ENV in H6;
inv H6.
inv H0;
try congruence.
assert (
chunk0 =
chunk).
simpl in H.
congruence.
subst chunk0.
assert (
v0 =
v).
unfold Mem.loadv in H2.
rewrite Ptrofs.unsigned_zero in H2.
congruence.
subst v0.
exists tv;
split;
auto.
constructor;
auto.
simpl in H;
congruence.
simpl in H;
congruence.
any other l-value *)
exploit eval_simpl_lvalue;
eauto.
intros [
loc' [
ofs' [
A B]]].
exploit deref_loc_inject;
eauto.
intros [
tv [
C D]].
exists tv;
split;
auto.
econstructor.
eexact A.
rewrite typeof_simpl_expr;
auto.
lvalues *)
destruct 1;
simpl;
intros.
local var *)
rewrite H1.
exploit me_vars;
eauto.
instantiate (1 :=
id).
intros MV.
inv MV;
try congruence.
rewrite ENV in H;
inv H.
exists b';
exists Ptrofs.zero;
split.
apply eval_Evar_local;
auto.
econstructor;
eauto.
global var *)
rewrite H2.
exploit me_vars;
eauto.
instantiate (1 :=
id).
intros MV.
inv MV;
try congruence.
exists l;
exists Ptrofs.zero;
split.
apply eval_Evar_global.
auto.
rewrite <-
H0.
apply symbols_preserved.
destruct GLOB as [
bound GLOB1].
inv GLOB1.
econstructor;
eauto.
deref *)
exploit eval_simpl_expr;
eauto.
intros [
tv [
A B]].
inversion B.
subst.
econstructor;
econstructor;
split;
eauto.
econstructor;
eauto.
field struct *)
rewrite <-
comp_env_preserved in *.
exploit eval_simpl_expr;
eauto.
intros [
tv [
A B]].
inversion B.
subst.
econstructor;
econstructor;
split.
eapply eval_Efield_struct;
eauto.
rewrite typeof_simpl_expr;
eauto.
econstructor;
eauto.
repeat rewrite Ptrofs.add_assoc.
decEq.
apply Ptrofs.add_commut.
field union *)
rewrite <-
comp_env_preserved in *.
exploit eval_simpl_expr;
eauto.
intros [
tv [
A B]].
inversion B.
subst.
econstructor;
econstructor;
split.
eapply eval_Efield_union;
eauto.
rewrite typeof_simpl_expr;
eauto.
auto.
Qed.
Lemma eval_simpl_exprlist:
forall al tyl vl,
eval_exprlist ge e le m al tyl vl ->
compat_cenv (
addr_taken_exprlist al)
cenv ->
val_casted_list vl tyl /\
exists tvl,
eval_exprlist tge te tle tm (
simpl_exprlist cenv al)
tyl tvl
/\
Val.inject_list f vl tvl.
Proof.
induction 1;
simpl;
intros.
split.
constructor.
econstructor;
split.
constructor.
auto.
exploit eval_simpl_expr;
eauto with compat.
intros [
tv1 [
A B]].
exploit sem_cast_inject;
eauto.
intros [
tv2 [
C D]].
exploit IHeval_exprlist;
eauto with compat.
intros [
E [
tvl [
F G]]].
split.
constructor;
auto.
eapply cast_val_is_casted;
eauto.
exists (
tv2 ::
tvl);
split.
econstructor;
eauto.
rewrite typeof_simpl_expr;
auto.
econstructor;
eauto.
Qed.
End EVAL_EXPR.
Matching continuations
Inductive match_cont (
f:
meminj):
compilenv ->
cont ->
cont ->
mem ->
block ->
block ->
Prop :=
|
match_Kstop:
forall cenv m bound tbound hi,
match_globalenvs f hi ->
Ple hi bound ->
Ple hi tbound ->
match_cont f cenv Kstop Kstop m bound tbound
|
match_Kseq:
forall cenv s k ts tk m bound tbound,
simpl_stmt cenv s =
OK ts ->
match_cont f cenv k tk m bound tbound ->
compat_cenv (
addr_taken_stmt s)
cenv ->
match_cont f cenv (
Kseq s k) (
Kseq ts tk)
m bound tbound
|
match_Kloop1:
forall cenv s1 s2 k ts1 ts2 tk m bound tbound,
simpl_stmt cenv s1 =
OK ts1 ->
simpl_stmt cenv s2 =
OK ts2 ->
match_cont f cenv k tk m bound tbound ->
compat_cenv (
VSet.union (
addr_taken_stmt s1) (
addr_taken_stmt s2))
cenv ->
match_cont f cenv (
Kloop1 s1 s2 k) (
Kloop1 ts1 ts2 tk)
m bound tbound
|
match_Kloop2:
forall cenv s1 s2 k ts1 ts2 tk m bound tbound,
simpl_stmt cenv s1 =
OK ts1 ->
simpl_stmt cenv s2 =
OK ts2 ->
match_cont f cenv k tk m bound tbound ->
compat_cenv (
VSet.union (
addr_taken_stmt s1) (
addr_taken_stmt s2))
cenv ->
match_cont f cenv (
Kloop2 s1 s2 k) (
Kloop2 ts1 ts2 tk)
m bound tbound
|
match_Kswitch:
forall cenv k tk m bound tbound,
match_cont f cenv k tk m bound tbound ->
match_cont f cenv (
Kswitch k) (
Kswitch tk)
m bound tbound
|
match_Kcall:
forall cenv optid fn e le k tfn te tle tk m hi thi lo tlo bound tbound x,
transf_function fn =
OK tfn ->
match_envs f (
cenv_for fn)
e le m lo hi te tle tlo thi ->
match_cont f (
cenv_for fn)
k tk m lo tlo ->
check_opttemp (
cenv_for fn)
optid =
OK x ->
Ple hi bound ->
Ple thi tbound ->
match_cont f cenv (
Kcall optid fn e le k)
(
Kcall optid tfn te tle tk)
m bound tbound.
Invariance property by change of memory and injection
Lemma match_cont_invariant:
forall f'
m'
f cenv k tk m bound tbound,
match_cont f cenv k tk m bound tbound ->
(
forall b chunk v,
f b =
None ->
Plt b bound ->
Mem.load chunk m b 0 =
Some v ->
Mem.load chunk m'
b 0 =
Some v) ->
inject_incr f f' ->
(
forall b,
Plt b bound ->
f'
b =
f b) ->
(
forall b b'
delta,
f'
b =
Some(
b',
delta) ->
Plt b'
tbound ->
f'
b =
f b) ->
match_cont f'
cenv k tk m'
bound tbound.
Proof.
induction 1;
intros LOAD INCR INJ1 INJ2;
econstructor;
eauto.
globalenvs *)
inv H.
constructor;
intros;
eauto.
assert (
f b1 =
Some (
b2,
delta)).
rewrite <-
H;
symmetry;
eapply INJ2;
eauto.
xomega.
eapply IMAGE;
eauto.
call *)
eapply match_envs_invariant;
eauto.
intros.
apply LOAD;
auto.
xomega.
intros.
apply INJ1;
auto;
xomega.
intros.
eapply INJ2;
eauto;
xomega.
eapply IHmatch_cont;
eauto.
intros;
apply LOAD;
auto.
inv H0;
xomega.
intros;
apply INJ1.
inv H0;
xomega.
intros;
eapply INJ2;
eauto.
inv H0;
xomega.
Qed.
Invariance by assignment to location "above"
Lemma match_cont_assign_loc:
forall f cenv k tk m bound tbound ty loc ofs v m',
match_cont f cenv k tk m bound tbound ->
assign_loc ge ty m loc ofs v m' ->
Ple bound loc ->
match_cont f cenv k tk m'
bound tbound.
Proof.
Invariance by external calls
Lemma match_cont_extcall:
forall f cenv k tk m bound tbound tm f'
m',
match_cont f cenv k tk m bound tbound ->
Mem.unchanged_on (
loc_unmapped f)
m m' ->
inject_incr f f' ->
inject_separated f f'
m tm ->
Ple bound (
Mem.nextblock m) ->
Ple tbound (
Mem.nextblock tm) ->
match_cont f'
cenv k tk m'
bound tbound.
Proof.
intros.
eapply match_cont_invariant;
eauto.
intros.
eapply Mem.load_unchanged_on;
eauto.
red in H2.
intros.
destruct (
f b)
as [[
b'
delta] | ]
eqn:?.
auto.
destruct (
f'
b)
as [[
b'
delta] | ]
eqn:?;
auto.
exploit H2;
eauto.
unfold Mem.valid_block.
intros [
A B].
xomegaContradiction.
red in H2.
intros.
destruct (
f b)
as [[
b''
delta''] | ]
eqn:?.
auto.
exploit H2;
eauto.
unfold Mem.valid_block.
intros [
A B].
xomegaContradiction.
Qed.
Invariance by change of bounds
Lemma match_cont_incr_bounds:
forall f cenv k tk m bound tbound,
match_cont f cenv k tk m bound tbound ->
forall bound'
tbound',
Ple bound bound' ->
Ple tbound tbound' ->
match_cont f cenv k tk m bound'
tbound'.
Proof.
induction 1; intros; econstructor; eauto; xomega.
Qed.
match_cont and call continuations.
Lemma match_cont_change_cenv:
forall f cenv k tk m bound tbound cenv',
match_cont f cenv k tk m bound tbound ->
is_call_cont k ->
match_cont f cenv'
k tk m bound tbound.
Proof.
intros. inv H; simpl in H0; try contradiction; econstructor; eauto.
Qed.
Lemma match_cont_is_call_cont:
forall f cenv k tk m bound tbound,
match_cont f cenv k tk m bound tbound ->
is_call_cont k ->
is_call_cont tk.
Proof.
intros. inv H; auto.
Qed.
Lemma match_cont_call_cont:
forall f cenv k tk m bound tbound,
match_cont f cenv k tk m bound tbound ->
forall cenv',
match_cont f cenv' (
call_cont k) (
call_cont tk)
m bound tbound.
Proof.
induction 1; simpl; auto; intros; econstructor; eauto.
Qed.
match_cont and freeing of environment blocks
Remark free_list_nextblock:
forall l m m',
Mem.free_list m l =
Some m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
induction l;
simpl;
intros.
congruence.
destruct a.
destruct p.
destruct (
Mem.free m b z0 z)
as [
m1|]
eqn:?;
try discriminate.
transitivity (
Mem.nextblock m1).
eauto.
eapply Mem.nextblock_free;
eauto.
Qed.
Remark free_list_load:
forall chunk b'
l m m',
Mem.free_list m l =
Some m' ->
(
forall b lo hi,
In (
b,
lo,
hi)
l ->
Plt b'
b) ->
Mem.load chunk m'
b' 0 =
Mem.load chunk m b' 0.
Proof.
induction l;
simpl;
intros.
inv H;
auto.
destruct a.
destruct p.
destruct (
Mem.free m b z0 z)
as [
m1|]
eqn:?;
try discriminate.
transitivity (
Mem.load chunk m1 b' 0).
eauto.
eapply Mem.load_free.
eauto.
left.
assert (
Plt b'
b)
by eauto.
unfold block;
xomega.
Qed.
Lemma match_cont_free_env:
forall f cenv e le m lo hi te tle tm tlo thi k tk m'
tm',
match_envs f cenv e le m lo hi te tle tlo thi ->
match_cont f cenv k tk m lo tlo ->
Ple hi (
Mem.nextblock m) ->
Ple thi (
Mem.nextblock tm) ->
Mem.free_list m (
blocks_of_env ge e) =
Some m' ->
Mem.free_list tm (
blocks_of_env tge te) =
Some tm' ->
match_cont f cenv k tk m' (
Mem.nextblock m') (
Mem.nextblock tm').
Proof.
Lemma match_cont_free_env':
forall f cenv e le m lo hi te tle tm tlo thi k tk m'
tm'
m''
tm'',
match_envs f cenv e le m lo hi te tle tlo thi ->
match_cont f cenv k tk m lo tlo ->
Ple hi (
Mem.nextblock m) ->
Ple thi (
Mem.nextblock tm) ->
Mem.free_list m (
blocks_of_env ge e) =
Some m' ->
Mem.free_list tm (
blocks_of_env tge te) =
Some tm' ->
Mem.unrecord_stack_block m' =
Some m'' ->
Mem.unrecord_stack_block tm' =
Some tm'' ->
match_cont f cenv k tk m'' (
Mem.nextblock m'') (
Mem.nextblock tm'').
Proof.
Matching of global environments
Lemma match_cont_globalenv:
forall f cenv k tk m bound tbound,
match_cont f cenv k tk m bound tbound ->
exists bound,
match_globalenvs f bound.
Proof.
induction 1; auto. exists hi; auto.
Qed.
Hint Resolve match_cont_globalenv:
compat.
Lemma match_cont_find_funct:
forall f cenv k tk m bound tbound vf fd tvf,
match_cont f cenv k tk m bound tbound ->
Genv.find_funct ge vf =
Some fd ->
Val.inject f vf tvf ->
exists tfd,
Genv.find_funct tge tvf =
Some tfd /\
transf_fundef fd =
OK tfd.
Proof.
Relating execution states
Inductive match_states:
state ->
state ->
Prop :=
|
match_regular_states:
forall f s k e le m tf ts tk te tle tm j lo hi tlo thi
(
TRF:
transf_function f =
OK tf)
(
TRS:
simpl_stmt (
cenv_for f)
s =
OK ts)
(
MENV:
match_envs j (
cenv_for f)
e le m lo hi te tle tlo thi)
(
MCONT:
match_cont j (
cenv_for f)
k tk m lo tlo)
(
MINJ:
Mem.inject j (
flat_frameinj (
length (
Mem.stack m)))
m tm)
(
COMPAT:
compat_cenv (
addr_taken_stmt s) (
cenv_for f))
(
BOUND:
Ple hi (
Mem.nextblock m))
(
TBOUND:
Ple thi (
Mem.nextblock tm))
(
SE:
stack_equiv (
Mem.stack m) (
Mem.stack tm)),
match_states (
State f s k e le m)
(
State tf ts tk te tle tm)
|
match_call_state:
forall fd vargs k m tfd tvargs tk tm j targs tres cconv sz
(
TRFD:
transf_fundef fd =
OK tfd)
(
MCONT:
forall cenv,
match_cont j cenv k tk m (
Mem.nextblock m) (
Mem.nextblock tm))
(
MINJ:
Mem.inject j (
flat_frameinj (
length (
Mem.stack m)))
m tm)
(
AINJ:
Val.inject_list j vargs tvargs)
(
FUNTY:
type_of_fundef fd =
Tfunction targs tres cconv)
(
ANORM:
val_casted_list vargs targs)
(
SE:
stack_equiv (
Mem.stack m) (
Mem.stack tm))
(
TOPNPERM:
top_tframe_tc (
Mem.stack tm)),
match_states (
Callstate fd vargs k m sz)
(
Callstate tfd tvargs tk tm sz)
|
match_return_state:
forall v k m tv tk tm j
(
MCONT:
forall cenv,
match_cont j cenv k tk m (
Mem.nextblock m) (
Mem.nextblock tm))
(
MINJ:
Mem.inject j (
flat_frameinj (
length (
Mem.stack m)))
m tm)
(
RINJ:
Val.inject j v tv)
(
SE:
stack_equiv (
Mem.stack m) (
Mem.stack tm)),
match_states (
Returnstate v k m)
(
Returnstate tv tk tm).
Lemma bind_parameters_stack:
forall ge e m vars args m'
(
BP:
bind_parameters ge e m vars args m'),
Mem.stack m' =
Mem.stack m.
Proof.
induction 1;
simpl;
intros;
eauto.
rewrite IHBP.
eapply assign_loc_stack;
eauto.
Qed.
Lemma alloc_variables_stack:
forall ge e m vars e'
m',
alloc_variables ge e m vars e'
m' ->
Mem.stack m' =
Mem.stack m.
Proof.
The simulation diagrams
Remark is_liftable_var_charact:
forall cenv a,
match is_liftable_var cenv a with
|
Some id =>
exists ty,
a =
Evar id ty /\
VSet.mem id cenv =
true
|
None =>
match a with Evar id ty =>
VSet.mem id cenv =
false |
_ =>
True end
end.
Proof.
intros.
destruct a;
simpl;
auto.
destruct (
VSet.mem i cenv)
eqn:?.
exists t;
auto.
auto.
Qed.
Remark simpl_select_switch:
forall cenv n ls tls,
simpl_lblstmt cenv ls =
OK tls ->
simpl_lblstmt cenv (
select_switch n ls) =
OK (
select_switch n tls).
Proof.
Remark simpl_seq_of_labeled_statement:
forall cenv ls tls,
simpl_lblstmt cenv ls =
OK tls ->
simpl_stmt cenv (
seq_of_labeled_statement ls) =
OK (
seq_of_labeled_statement tls).
Proof.
induction ls; simpl; intros; monadInv H; simpl.
auto.
rewrite EQ; simpl. erewrite IHls; eauto. simpl. auto.
Qed.
Remark compat_cenv_select_switch:
forall cenv n ls,
compat_cenv (
addr_taken_lblstmt ls)
cenv ->
compat_cenv (
addr_taken_lblstmt (
select_switch n ls))
cenv.
Proof.
Remark addr_taken_seq_of_labeled_statement:
forall ls,
addr_taken_stmt (
seq_of_labeled_statement ls) =
addr_taken_lblstmt ls.
Proof.
induction ls; simpl; congruence.
Qed.
Section FIND_LABEL.
Variable f:
meminj.
Variable cenv:
compilenv.
Variable m:
mem.
Variables bound tbound:
block.
Variable lbl:
ident.
Lemma simpl_find_label:
forall s k ts tk,
simpl_stmt cenv s =
OK ts ->
match_cont f cenv k tk m bound tbound ->
compat_cenv (
addr_taken_stmt s)
cenv ->
match find_label lbl s k with
|
None =>
find_label lbl ts tk =
None
|
Some(
s',
k') =>
exists ts',
exists tk',
find_label lbl ts tk =
Some(
ts',
tk')
/\
compat_cenv (
addr_taken_stmt s')
cenv
/\
simpl_stmt cenv s' =
OK ts'
/\
match_cont f cenv k'
tk'
m bound tbound
end
with simpl_find_label_ls:
forall ls k tls tk,
simpl_lblstmt cenv ls =
OK tls ->
match_cont f cenv k tk m bound tbound ->
compat_cenv (
addr_taken_lblstmt ls)
cenv ->
match find_label_ls lbl ls k with
|
None =>
find_label_ls lbl tls tk =
None
|
Some(
s',
k') =>
exists ts',
exists tk',
find_label_ls lbl tls tk =
Some(
ts',
tk')
/\
compat_cenv (
addr_taken_stmt s')
cenv
/\
simpl_stmt cenv s' =
OK ts'
/\
match_cont f cenv k'
tk'
m bound tbound
end.
Proof.
induction s;
simpl;
intros until tk;
intros TS MC COMPAT;
auto.
skip *)
monadInv TS;
auto.
var *)
destruct (
is_liftable_var cenv e);
monadInv TS;
auto.
unfold Sset_debug.
destruct (
Compopts.debug tt);
auto.
set *)
monadInv TS;
auto.
call *)
monadInv TS;
auto.
builtin *)
monadInv TS;
auto.
seq *)
monadInv TS.
exploit (
IHs1 (
Kseq s2 k)
x (
Kseq x0 tk));
eauto with compat.
constructor;
eauto with compat.
destruct (
find_label lbl s1 (
Kseq s2 k))
as [[
s'
k']|].
intros [
ts' [
tk' [
P [
Q [
R S]]]]].
exists ts';
exists tk'.
simpl.
rewrite P.
auto.
intros E.
simpl.
rewrite E.
eapply IHs2;
eauto with compat.
ifthenelse *)
monadInv TS.
exploit (
IHs1 k x tk);
eauto with compat.
destruct (
find_label lbl s1 k)
as [[
s'
k']|].
intros [
ts' [
tk' [
P [
Q [
R S]]]]].
exists ts';
exists tk'.
simpl.
rewrite P.
auto.
intros E.
simpl.
rewrite E.
eapply IHs2;
eauto with compat.
loop *)
monadInv TS.
exploit (
IHs1 (
Kloop1 s1 s2 k)
x (
Kloop1 x x0 tk));
eauto with compat.
constructor;
eauto with compat.
destruct (
find_label lbl s1 (
Kloop1 s1 s2 k))
as [[
s'
k']|].
intros [
ts' [
tk' [
P [
Q [
R S]]]]].
exists ts';
exists tk'.
simpl;
rewrite P.
auto.
intros E.
simpl;
rewrite E.
eapply IHs2;
eauto with compat.
econstructor;
eauto with compat.
break *)
monadInv TS;
auto.
continue *)
monadInv TS;
auto.
return *)
monadInv TS;
auto.
switch *)
monadInv TS.
simpl.
eapply simpl_find_label_ls;
eauto with compat.
constructor;
auto.
label *)
monadInv TS.
simpl.
destruct (
ident_eq lbl l).
exists x;
exists tk;
auto.
eapply IHs;
eauto.
goto *)
monadInv TS;
auto.
induction ls;
simpl;
intros.
nil *)
monadInv H.
auto.
cons *)
monadInv H.
exploit (
simpl_find_label s (
Kseq (
seq_of_labeled_statement ls)
k)).
eauto.
constructor.
eapply simpl_seq_of_labeled_statement;
eauto.
eauto.
rewrite addr_taken_seq_of_labeled_statement.
eauto with compat.
eauto with compat.
destruct (
find_label lbl s (
Kseq (
seq_of_labeled_statement ls)
k))
as [[
s'
k']|].
intros [
ts' [
tk' [
P [
Q [
R S]]]]].
exists ts';
exists tk';
split.
simpl;
rewrite P.
auto.
auto.
intros E.
simpl;
rewrite E.
eapply IHls;
eauto with compat.
Qed.
Lemma find_label_store_params:
forall s k params,
find_label lbl (
store_params cenv params s)
k =
find_label lbl s k.
Proof.
induction params;
simpl.
auto.
destruct a as [
id ty].
destruct (
VSet.mem id cenv);
auto.
Qed.
Lemma find_label_add_debug_vars:
forall s k vars,
find_label lbl (
add_debug_vars vars s)
k =
find_label lbl s k.
Proof.
Lemma find_label_add_debug_params:
forall s k vars,
find_label lbl (
add_debug_params vars s)
k =
find_label lbl s k.
Proof.
End FIND_LABEL.
Lemma match_envs_norepet_blocks_with_info:
forall j cenv e tenv m0 lo hi te tenv'
lo'
hi',
match_envs j cenv e tenv m0 lo hi te tenv'
lo'
hi' ->
list_norepet (
map fst (
blocks_with_info tge te)).
Proof.
Lemma alloc_variables_perm_1:
forall (
ge:
genv)
e1 m1 vars e2 m2,
alloc_variables ge e1 m1 vars e2 m2 ->
forall b o k p,
Mem.perm m1 b o k p ->
Mem.perm m2 b o k p.
Proof.
induction 1;
simpl;
intros b o k p P.
auto.
eapply IHalloc_variables.
eapply Mem.perm_alloc_1;
eauto.
Qed.
Lemma alloc_variables_perm_2:
forall (
ge:
genv)
e1 m1 vars e2 m2,
alloc_variables ge e1 m1 vars e2 m2 ->
forall b o k p,
Mem.valid_block m1 b ->
Mem.perm m2 b o k p ->
Mem.perm m1 b o k p.
Proof.
Lemma alloc_variables_not_in_vars:
forall ge e1 m1 vars e2 m2,
alloc_variables ge e1 m1 vars e2 m2 ->
forall id,
~
In id (
map fst vars) ->
e1 !
id =
e2 !
id.
Proof.
induction 1;
simpl;
intros id0 NIN.
auto.
destruct (
peq id0 id).
subst.
intuition congruence.
erewrite <-
IHalloc_variables;
auto.
rewrite PTree.gso.
auto.
auto.
Qed.
Lemma alloc_variables_perm:
forall ge e1 m1 vars e2 m2,
alloc_variables ge e1 m1 vars e2 m2 ->
list_norepet (
map fst vars) ->
forall id b ty o k p,
e1 !
id =
None ->
e2 !
id =
Some (
b,
ty) ->
Mem.perm m2 b o k p ->
0 <=
o <
sizeof ge ty.
Proof.
Lemma match_cont_push_new_stage:
forall j cenv k1 k2 m a b,
match_cont j cenv k1 k2 m a b ->
match_cont j cenv k1 k2 (
Mem.push_new_stage m)
a b.
Proof.
Ltac rewrite_stack_blocks :=
match goal with
|
H:
Mem.alloc _ _ _ = (?
m,
_) |-
context [
Mem.stack ?
m ] =>
rewrite (
Mem.alloc_stack_blocks _ _ _ _ _ H)
|
H:
Mem.store _ _ _ _ _ =
Some ?
m |-
context [
Mem.stack ?
m ] =>
rewrite (
Mem.store_stack_blocks _ _ _ _ _ _ H)
|
H:
Mem.storev _ _ _ _ =
Some ?
m |-
context [
Mem.stack ?
m ] =>
rewrite (
Mem.storev_stack _ _ _ _ _ H)
|
H:
external_call _ _ _ _ _ _ ?
m |-
context [
Mem.stack ?
m ] =>
rewrite <- (
external_call_stack_blocks _ _ _ _ _ _ _ H)
|
H:
Mem.free_list _ _ =
Some ?
m |-
context [
Mem.stack ?
m ] =>
rewrite (
Mem.free_list_stack_blocks _ _ _ H)
|
H:
Mem.free _ _ _ _ =
Some ?
m |-
context [
Mem.stack ?
m ] =>
rewrite (
Mem.free_stack_blocks _ _ _ _ _ H)
|
H:
context[
Mem.stack (
Mem.push_new_stage ?
m)] |-
_ =>
rewrite Mem.push_new_stage_stack in H;
inv H
| |-
context[
Mem.stack (
Mem.push_new_stage ?
m)] =>
rewrite Mem.push_new_stage_stack
|
H:
Mem.record_stack_blocks _ _ =
Some ?
m |-
context [
Mem.stack ?
m ] =>
let f :=
fresh "
f"
in
let r :=
fresh "
r"
in
let EQ1 :=
fresh "
EQ1"
in
let EQ2 :=
fresh "
EQ2"
in
destruct (
Mem.record_stack_blocks_stack_eq _ _ _ H)
as (
f &
r &
EQ1 &
EQ2);
rewrite EQ2
|
H:
Mem.unrecord_stack_block ?
m1 =
Some ?
m
|-
context [
Mem.stack ?
m ] =>
let f :=
fresh "
f"
in
let EQ :=
fresh "
EQ"
in
destruct (
Mem.unrecord_stack _ _ H)
as (
f,
EQ);
replace (
Mem.stack m)
with (
tl (
Mem.stack m1))
by (
rewrite EQ;
reflexivity)
|
H:
alloc_variables _ _ _ _ _ ?
m |-
context [
Mem.stack ?
m ] =>
rewrite (
alloc_variables_stack _ _ _ _ _ _ H)
|
H:
bind_parameters _ _ _ _ _ ?
m |-
context [
Mem.stack ?
m ] =>
rewrite (
bind_parameters_stack _ _ _ _ _ _ H)
|
H:
assign_loc _ _ _ _ _ _ ?
m |-
context [
Mem.stack ?
m ] =>
rewrite (
assign_loc_stack _ _ _ _ _ _ _ H)
end.
Lemma step_simulation:
forall S1 t S2,
step1 fn_stack_requirements ge S1 t S2 ->
forall S1' (
MS:
match_states S1 S1'),
exists S2',
plus (
step2 fn_stack_requirements)
tge S1'
t S2' /\
match_states S2 S2'.
Proof.
induction 1;
simpl;
intros;
inv MS;
simpl in *;
try (
monadInv TRS).
-
generalize (
is_liftable_var_charact (
cenv_for f)
a1);
destruct (
is_liftable_var (
cenv_for f)
a1)
as [
id|];
monadInv TRS.
+
intros [
ty [
P Q]];
subst a1;
simpl in *.
exploit eval_simpl_expr;
eauto with compat.
intros [
tv2 [
A B]].
exploit sem_cast_inject;
eauto.
intros [
tv [
C D]].
exploit me_vars;
eauto.
instantiate (1 :=
id).
intros MV.
inv H.
*
econstructor;
split.
eapply step_Sset_debug.
eauto.
rewrite typeof_simpl_expr.
eauto.
econstructor;
eauto with compat.
eapply match_envs_assign_lifted;
eauto.
eapply cast_val_is_casted;
eauto.
eapply match_cont_assign_loc;
eauto.
exploit me_range;
eauto.
xomega.
inv MV;
try congruence.
inv H2;
try congruence.
unfold Mem.storev in H3.
eapply Mem.store_unmapped_inject;
eauto.
rewrite_stack_blocks.
eauto.
congruence.
erewrite assign_loc_nextblock;
eauto.
repeat rewrite_stack_blocks;
eauto.
*
inv MV;
congruence.
+
intros P.
exploit eval_simpl_lvalue;
eauto with compat.
intros [
tb [
tofs [
E F]]].
exploit eval_simpl_expr;
eauto with compat.
intros [
tv2 [
A B]].
exploit sem_cast_inject;
eauto.
intros [
tv [
C D]].
exploit assign_loc_inject;
eauto.
intros [
tm' [
X [
Y Z]]].
econstructor;
split.
apply plus_one.
econstructor.
eexact E.
eexact A.
repeat rewrite typeof_simpl_expr.
eexact C.
rewrite typeof_simpl_expr;
auto.
eexact X.
econstructor;
eauto with compat.
eapply match_envs_invariant;
eauto.
eapply match_cont_invariant;
eauto.
erewrite assign_loc_stack;
eauto.
erewrite assign_loc_nextblock;
eauto.
erewrite assign_loc_nextblock;
eauto.
repeat rewrite_stack_blocks;
eauto.
-
exploit eval_simpl_expr;
eauto with compat.
intros [
tv [
A B]].
econstructor;
split.
apply plus_one.
econstructor.
eauto.
econstructor;
eauto with compat.
eapply match_envs_set_temp;
eauto.
-
exploit eval_simpl_expr;
eauto with compat.
intros [
tvf [
A B]].
exploit eval_simpl_exprlist;
eauto with compat.
intros [
CASTED [
tvargs [
C D]]].
exploit match_cont_find_funct;
eauto.
intros [
tfd [
P Q]].
destruct IFI as (
bb &
oo &
EQ3 &
EQ2).
econstructor;
split.
apply plus_one.
eapply step_call with (
fd0 :=
tfd) (
vf0:=
tvf).
{
subst.
inv B.
eexists;
eexists;
split;
eauto.
rewrite symbols_preserved.
rewrite EQ2.
f_equal.
edestruct match_cont_globalenv as (
bnd &
MG);
eauto.
inv MG.
rewrite DOMAIN in H6.
inv H6.
auto.
eapply SYMBOLS;
eauto.
}
rewrite typeof_simpl_expr.
eauto.
apply A.
eauto.
eauto.
erewrite type_of_fundef_preserved;
eauto.
econstructor;
eauto.
intros;
eapply match_cont_push_new_stage.
rewrite !
Mem.push_new_stage_nextblock.
econstructor;
eauto.
apply Mem.push_new_stage_inject_flat.
eauto.
repeat rewrite_stack_blocks.
repeat constructor;
auto.
rewrite_stack_blocks.
constructor.
reflexivity.
-
exploit eval_simpl_exprlist;
eauto with compat.
intros [
CASTED [
tvargs [
C D]]].
exploit Mem.push_new_stage_inject_flat.
eauto.
intro MINJ'.
exploit external_call_mem_inject;
eauto.
apply match_globalenvs_preserves_globals;
eauto with compat.
intros [
j' [
tvres [
tm' [
P [
Q [
R [
S [
T [
U V]]]]]]]]].
exploit Mem.unrecord_stack_block_inject_parallel_flat.
erewrite (
external_call_stack_blocks)
in R. 2:
eauto.
apply R.
eauto.
intros (
m2' &
USB &
MINJ'').
econstructor;
split.
apply plus_one.
econstructor.
eauto.
eapply external_call_symbols_preserved;
eauto.
apply senv_preserved.
eauto.
auto.
assert (
UNCH:
Mem.unchanged_on (
loc_unmapped j)
m m'').
{
eapply Mem.unchanged_on_trans.
eapply Mem.strong_unchanged_on_weak,
Mem.push_new_stage_unchanged_on.
eapply Mem.unchanged_on_trans.
eauto.
eapply Mem.strong_unchanged_on_weak,
Mem.unrecord_stack_block_unchanged_on.
eauto.
}
assert (
SEP:
inject_separated j j'
m tm).
{
red;
intros.
specialize (
V _ _ _ H2 H3).
revert V.
unfold Mem.valid_block.
rewrite !
Mem.push_new_stage_nextblock;
tauto.
}
econstructor;
eauto with compat.
eapply match_envs_set_opttemp;
eauto.
eapply match_envs_extcall;
eauto.
eapply match_cont_extcall;
eauto.
inv MENV;
xomega.
inv MENV;
xomega.
erewrite Mem.unrecord_stack_block_nextblock by eauto.
eapply Ple_trans;
eauto.
eapply Ple_trans. 2:
eapply external_call_nextblock;
eauto.
rewrite Mem.push_new_stage_nextblock;
xomega.
erewrite Mem.unrecord_stack_block_nextblock by eauto.
eapply Ple_trans;
eauto.
eapply Ple_trans. 2:
eapply external_call_nextblock;
eauto.
rewrite Mem.push_new_stage_nextblock;
xomega.
repeat rewrite_stack_blocks;
eauto.
-
econstructor;
split.
apply plus_one.
econstructor.
econstructor;
eauto with compat.
econstructor;
eauto with compat.
-
inv MCONT.
econstructor;
split.
apply plus_one.
econstructor.
econstructor;
eauto.
-
inv MCONT.
econstructor;
split.
apply plus_one.
econstructor.
econstructor;
eauto.
-
inv MCONT.
econstructor;
split.
apply plus_one.
econstructor.
econstructor;
eauto.
-
exploit eval_simpl_expr;
eauto with compat.
intros [
tv [
A B]].
econstructor;
split.
apply plus_one.
apply step_ifthenelse with (
v2 :=
tv) (
b0 :=
b).
auto.
rewrite typeof_simpl_expr.
eapply bool_val_inject;
eauto.
destruct b;
econstructor;
eauto with compat.
-
econstructor;
split.
apply plus_one.
econstructor.
econstructor;
eauto with compat.
econstructor;
eauto with compat.
-
inv MCONT.
econstructor;
split.
apply plus_one.
econstructor.
destruct H;
subst x;
simpl in *;
intuition congruence.
econstructor;
eauto with compat.
econstructor;
eauto with compat.
-
inv MCONT.
econstructor;
split.
apply plus_one.
eapply step_break_loop1.
econstructor;
eauto.
-
inv MCONT.
econstructor;
split.
apply plus_one.
eapply step_skip_loop2.
econstructor;
eauto with compat.
simpl;
rewrite H2;
rewrite H4;
auto.
-
inv MCONT.
econstructor;
split.
apply plus_one.
eapply step_break_loop2.
econstructor;
eauto.
-
exploit match_envs_free_blocks;
eauto.
intros [
tm' [
P Q]].
econstructor;
split.
apply plus_one.
econstructor;
eauto.
econstructor;
eauto.
intros.
eapply match_cont_call_cont.
eapply match_cont_free_env;
eauto.
rewrite_stack_blocks.
eauto.
repeat rewrite_stack_blocks;
eauto using stack_equiv_tail.
-
exploit eval_simpl_expr;
eauto with compat.
intros [
tv [
A B]].
exploit sem_cast_inject;
eauto.
intros [
tv' [
C D]].
exploit match_envs_free_blocks;
eauto.
intros [
tm' [
P Q]].
econstructor;
split.
apply plus_one.
econstructor;
eauto.
rewrite typeof_simpl_expr.
monadInv TRF;
simpl.
eauto.
econstructor;
eauto.
intros.
eapply match_cont_call_cont.
eapply match_cont_free_env;
eauto.
rewrite_stack_blocks;
eauto.
repeat rewrite_stack_blocks;
eauto using stack_equiv_tail.
-
exploit match_envs_free_blocks;
eauto.
intros [
tm' [
P Q]].
econstructor;
split.
apply plus_one.
econstructor;
eauto.
eapply match_cont_is_call_cont;
eauto.
monadInv TRF;
auto.
econstructor;
eauto.
intros.
apply match_cont_change_cenv with (
cenv_for f);
auto.
eapply match_cont_free_env;
eauto.
rewrite_stack_blocks;
eauto.
repeat rewrite_stack_blocks;
eauto using stack_equiv_tail.
-
exploit eval_simpl_expr;
eauto with compat.
intros [
tv [
A B]].
econstructor;
split.
apply plus_one.
econstructor;
eauto.
rewrite typeof_simpl_expr.
instantiate (1 :=
n).
unfold sem_switch_arg in *;
destruct (
classify_switch (
typeof a));
try discriminate;
inv B;
inv H0;
auto.
econstructor;
eauto.
erewrite simpl_seq_of_labeled_statement.
reflexivity.
eapply simpl_select_switch;
eauto.
econstructor;
eauto.
rewrite addr_taken_seq_of_labeled_statement.
apply compat_cenv_select_switch.
eauto with compat.
-
inv MCONT.
econstructor;
split.
apply plus_one.
eapply step_skip_break_switch.
destruct H;
subst x;
simpl in *;
intuition congruence.
econstructor;
eauto with compat.
-
inv MCONT.
econstructor;
split.
apply plus_one.
eapply step_continue_switch.
econstructor;
eauto with compat.
-
econstructor;
split.
apply plus_one.
econstructor.
econstructor;
eauto.
-
generalize TRF;
intros TRF'.
monadInv TRF'.
exploit (
simpl_find_label j (
cenv_for f)
m lo tlo lbl (
fn_body f) (
call_cont k)
x (
call_cont tk)).
eauto.
eapply match_cont_call_cont.
eauto.
apply compat_cenv_for.
rewrite H.
intros [
ts' [
tk' [
A [
B [
C D]]]]].
econstructor;
split.
apply plus_one.
econstructor;
eauto.
simpl.
rewrite find_label_add_debug_params.
rewrite find_label_store_params.
rewrite find_label_add_debug_vars.
eexact A.
econstructor;
eauto.
-
monadInv TRFD.
inv H.
generalize EQ;
intro EQ';
monadInv EQ'.
assert (
list_norepet (
var_names (
fn_params f ++
fn_vars f))).
unfold var_names.
rewrite map_app.
auto.
exploit match_envs_alloc_variables;
eauto.
instantiate (1 :=
cenv_for_gen (
addr_taken_stmt f.(
fn_body)) (
fn_params f ++
fn_vars f)).
intros.
eapply cenv_for_gen_by_value;
eauto.
rewrite VSF.mem_iff.
eexact H6.
intros.
eapply cenv_for_gen_domain.
rewrite VSF.mem_iff.
eexact H3.
intros [
j' [
te [
tm0 [
A [
B [
C [
D [
E [
F G]]]]]]]]].
assert (
K:
list_forall2 val_casted vargs (
map snd (
fn_params f))).
{
apply val_casted_list_params.
unfold type_of_function in FUNTY.
congruence. }
exploit match_envs_norepet_blocks_with_info.
eauto.
intro LNR.
exploit Mem.record_push_inject_flat. 8:
simpl;
eauto.
rewrite (
alloc_variables_stack _ _ _ _ _ _ H1).
eauto.
instantiate (1 := {|
frame_adt_blocks :=
blocks_with_info tge te;
frame_adt_size :=
frame_adt_size fa;
frame_adt_blocks_norepet :=
LNR |}).
{
red.
setoid_rewrite Forall_forall.
simpl.
rewrite H2.
intros (
b0&
fi);
simpl;
intros IN b'
delta J'
B.
assert (
exists i t,
e !
i =
Some (
b0,
t) /\
fi =
public_frame_info (
sizeof ge t)).
{
unfold blocks_with_info in IN.
unfold blocks_of_env in IN.
rewrite !
map_map,
in_map_iff in IN.
destruct IN as [[
id0 [
bb ty]] [
EQ'
IN]].
repeat destr_in EQ'.
apply PTree.elements_complete in IN.
simpl in Heqp.
inv Heqp.
eauto.
}
destruct H3 as (
i &
t &
EI &
EQfi).
inv B.
edestruct (
me_vars0 i);
try congruence.
rewrite EI in ENV.
inv ENV.
rewrite J'
B in MAPPED;
inv MAPPED.
apply PTree.elements_correct in TENV.
eexists.
split. 2:
apply inject_frame_info_id.
eapply in_map with (
f :=
fun x =>
let '(
b,
_,
hi) :=
block_of_binding ge x in (
b,
public_frame_info hi))
in TENV.
unfold blocks_with_info,
blocks_of_env.
rewrite map_map.
simpl in TENV.
erewrite list_map_exten.
apply TENV.
simpl.
intros.
unfold block_of_binding.
repeat destr.
destruct x.
destruct p1.
inv Heqp;
inv Heqp1.
f_equal.
f_equal.
replace ge with (
globalenv prog)
by reflexivity.
replace tge with (
globalenv tprog)
by reflexivity.
simpl.
assert (
prog_comp_env prog =
prog_comp_env tprog).
{
clear -
TRANSF.
destruct prog,
tprog.
simpl.
destruct TRANSF.
simpl in *.
subst.
congruence.
}
rewrite H6.
auto.
}
{
intros b0 INS INF.
red in INF.
unfold get_frame_blocks in INF.
simpl in INF.
rewrite (
alloc_variables_stack _ _ _ _ _ _ A)
in INS.
apply Mem.in_frames_valid in INS.
unfold blocks_with_info,
blocks_of_env in INF.
rewrite !
map_map,
in_map_iff in INF.
destruct INF as [[
id0 [
bb ty]] [
EQ'
IN]].
apply PTree.elements_complete in IN.
simpl in EQ';
subst.
eapply me_trange in IN;
eauto.
clear -
IN INS.
destruct IN;
red in INS.
xomega.
}
{
intros b'
IN.
red in IN.
unfold get_frame_blocks in IN.
unfold blocks_with_info,
blocks_of_env in IN.
simpl in IN.
rewrite !
map_map,
in_map_iff in IN.
destruct IN as [[
id0 [
bb ty]] [
EQ'
IN]].
apply PTree.elements_complete in IN.
simpl in EQ';
subst.
inv B.
destruct (
me_vars0 id0);
try congruence.
eapply me_trange0;
eauto.
}
{
simpl;
intros b fi o k0 p IN.
unfold blocks_with_info,
blocks_of_env in IN.
simpl in IN.
rewrite !
map_map,
in_map_iff in IN.
destruct IN as [[
id0 [
bb ty]] [
EQ'
IN]].
apply PTree.elements_complete in IN.
simpl in EQ';
inv EQ'.
simpl.
intros PERM;
eapply alloc_variables_perm in PERM;
eauto.
rewrite Z.max_r by omega.
auto.
edestruct vars_and_temps_properties as (
_ &
AA &
_);
eauto.
apply PTree.gempty.
}
{
unfold in_frame.
unfold get_frame_blocks.
simpl.
rewrite H2.
inv B.
unfold blocks_with_info,
blocks_of_env.
intros;
rewrite !
map_map, !
in_map_iff.
split; [
intros [[
id0 [
bb ty]] [
EQ'
IN]]|
intros [[
id0 [
bb ty]] [
EQ'
IN]]];
apply PTree.elements_complete in IN;
simpl in EQ';
subst.
-
destruct (
me_vars0 id0);
try congruence.
rewrite IN in ENV.
inv ENV.
rewrite H3 in MAPPED;
inv MAPPED.
repeat eexists. 2:
apply PTree.elements_correct;
eauto.
reflexivity.
-
exploit me_flat0;
eauto.
intros (
X &
Y).
subst.
repeat eexists. 2:
apply PTree.elements_correct;
eauto.
reflexivity.
}
reflexivity.
erewrite alloc_variables_stack by eauto.
inv TOPNPERM;
constructor.
auto.
simpl.
repeat rewrite_stack_blocks.
apply Z.eq_le_incl.
eauto using stack_equiv_fsize,
stack_equiv_tail.
intros (
m2' &
RSB &
INJ).
exploit store_params_correct.
eauto.
eapply list_norepet_append_left;
eauto.
eexact K.
apply val_inject_list_incr with j';
eauto.
{
eapply match_envs_invariant.
eexact B.
all:
eauto.
intros.
eapply (
Mem.load_unchanged_on (
fun _ _ =>
True)).
eapply Mem.strong_unchanged_on_weak.
eapply Mem.record_stack_block_unchanged_on;
eauto.
auto.
auto.
}
eexact INJ.
intros.
apply (
create_undef_temps_lifted id f).
auto.
intros.
destruct (
create_undef_temps (
fn_temps f))!
id as [
v|]
eqn:?;
auto.
exploit create_undef_temps_inv;
eauto.
intros [
P Q].
elim (
l id id);
auto.
intros [
tel [
tm1 [
P [
Q [
R [
S [
T TT]]]]]]].
change (
cenv_for_gen (
addr_taken_stmt (
fn_body f)) (
fn_params f ++
fn_vars f))
with (
cenv_for f)
in *.
generalize (
vars_and_temps_properties (
cenv_for f) (
fn_params f) (
fn_vars f) (
fn_temps f)).
intros [
X [
Y Z]].
auto.
auto.
econstructor;
split.
eapply plus_left.
econstructor.
econstructor.
exact Y.
exact X.
exact Z.
simpl.
eexact A. 3:
eauto.
reflexivity.
reflexivity.
eexact Q.
simpl.
eapply star_trans.
eapply step_add_debug_params.
auto.
eapply forall2_val_casted_inject;
eauto.
eexact Q.
eapply star_trans.
eexact P.
eapply step_add_debug_vars.
unfold remove_lifted;
intros id ty IN.
rewrite List.filter_In in IN.
destruct IN as [
IN FILT].
apply negb_true_iff in FILT.
eauto.
reflexivity.
reflexivity.
traceEq.
econstructor;
eauto.
eapply match_cont_invariant;
eauto.
{
intros b chunk v JB PLT LOAD.
transitivity (
Mem.load chunk m1'
b 0).
-
eapply bind_parameters_load;
eauto.
intros id b'
ty EID.
exploit alloc_variables_range.
eexact H1.
eauto.
unfold empty_env.
rewrite PTree.gempty.
intros [?|?].
congruence.
red;
intros;
subst b'.
xomega.
-
eapply alloc_variables_load in LOAD. 2:
eauto.
eapply (
Mem.load_unchanged_on (
fun _ _ =>
True)).
eapply Mem.strong_unchanged_on_weak.
eapply Mem.record_stack_block_unchanged_on;
eauto.
auto.
auto.
}
rewrite (
bind_parameters_stack _ _ _ _ _ _ H5).
auto.
apply compat_cenv_for.
rewrite (
bind_parameters_nextblock _ _ _ _ _ _ H5).
rewrite (
Mem.record_stack_block_nextblock _ _ _ H4).
xomega.
rewrite T.
rewrite (
Mem.record_stack_block_nextblock _ _ _ RSB).
xomega.
rewrite TT.
repeat rewrite_stack_blocks.
erewrite alloc_variables_stack in EQ1 by eauto.
erewrite alloc_variables_stack in EQ3 by eauto.
rewrite EQ1,
EQ3 in SE.
inv SE.
repeat constructor;
eauto.
simpl.
destruct LF2.
simpl in *.
auto.
-
monadInv TRFD.
inv FUNTY.
exploit external_call_mem_inject;
eauto.
apply match_globalenvs_preserves_globals.
eapply match_cont_globalenv.
eexact (
MCONT VSet.empty).
intros [
j' [
tvres [
tm' [
P [
Q [
R [
S [
T [
U V]]]]]]]]].
econstructor;
split.
apply plus_one.
econstructor;
eauto.
eapply external_call_symbols_preserved;
eauto.
apply senv_preserved.
econstructor;
eauto.
intros.
apply match_cont_incr_bounds with (
Mem.nextblock m) (
Mem.nextblock tm).
eapply match_cont_extcall;
eauto.
xomega.
xomega.
eapply external_call_nextblock;
eauto.
eapply external_call_nextblock;
eauto.
rewrite_stack_blocks;
eauto.
repeat rewrite_stack_blocks;
eauto.
-
specialize (
MCONT (
cenv_for f)).
inv MCONT.
exploit Mem.unrecord_stack_block_inject_parallel_flat.
apply MINJ.
eauto.
intros (
m2' &
USB &
MINJ'').
econstructor;
split.
apply plus_one.
econstructor.
eauto.
econstructor;
eauto with compat.
eapply match_envs_set_opttemp;
eauto.
eapply match_envs_extcall;
eauto.
eapply Mem.strong_unchanged_on_weak,
Mem.unrecord_stack_block_unchanged_on;
eauto.
red;
congruence.
eapply match_cont_extcall;
eauto.
eapply Mem.strong_unchanged_on_weak,
Mem.unrecord_stack_block_unchanged_on;
eauto.
red;
congruence.
inv H7;
xomega.
instantiate(1:=
tm).
inv H7;
xomega.
erewrite Mem.unrecord_stack_block_nextblock by eauto.
eauto.
erewrite Mem.unrecord_stack_block_nextblock by eauto.
eauto.
repeat rewrite_stack_blocks;
eauto using stack_equiv_tail.
Unshelve.
destruct fa;
auto.
Qed.
Lemma initial_states_simulation:
forall S,
initial_state fn_stack_requirements prog S ->
exists R,
initial_state fn_stack_requirements tprog R /\
match_states S R.
Proof.
Lemma final_states_simulation:
forall S R r,
match_states S R ->
final_state S r ->
final_state R r.
Proof.
intros.
inv H0.
inv H.
specialize (
MCONT VSet.empty).
inv MCONT.
inv RINJ.
constructor.
Qed.
Theorem transf_program_correct:
forward_simulation (
semantics1 fn_stack_requirements prog) (
semantics2 fn_stack_requirements tprog).
Proof.
End PRESERVATION.
Commutation with linking
Instance TransfSimplLocalsLink :
TransfLink match_prog.
Proof.