Semantic preservation for the SimplLocals pass.
Require Import FSets.
Require FSetAVL.
Require Import Coqlib.
Require Import Errors.
Require Import Ordered.
Require Import AST.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
Require Import Clight.
Require Import SimplLocals.
Module VSF :=
FSetFacts.Facts(
VSet).
Module VSP :=
FSetProperties.Properties(
VSet).
Section PRESERVATION.
Variable prog:
program.
Variable tprog:
program.
Hypothesis TRANSF:
transf_program prog =
OK tprog.
Let ge :=
globalenv prog.
Let tge :=
globalenv tprog.
Lemma comp_env_preserved:
genv_cenv tge =
genv_cenv ge.
Proof.
monadInv TRANSF.
unfold tge;
rewrite <-
H0;
auto.
Qed.
Lemma transf_programs:
AST.transform_partial_program transf_fundef (
program_of_program prog) =
OK (
program_of_program tprog).
Proof.
monadInv TRANSF.
rewrite EQ.
destruct x;
reflexivity.
Qed.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
Lemma public_preserved:
forall (
s:
ident),
Genv.public_symbol tge s =
Genv.public_symbol ge s.
Proof.
Lemma varinfo_preserved:
forall b,
Genv.find_var_info tge b =
Genv.find_var_info ge b.
Proof.
Lemma functions_translated:
forall (
v:
val) (
f:
fundef),
Genv.find_funct ge v =
Some f ->
exists tf,
Genv.find_funct tge v =
Some tf /\
transf_fundef f =
OK tf.
Proof.
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.
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_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 obtained by casting to a given type.
Inductive val_casted:
val ->
type ->
Prop :=
|
val_casted_int:
forall sz si attr n,
cast_int_int sz si n =
n ->
val_casted (
Vint n) (
Tint sz si attr)
|
val_casted_float:
forall attr n,
val_casted (
Vfloat n) (
Tfloat F64 attr)
|
val_casted_single:
forall attr n,
val_casted (
Vsingle n) (
Tfloat F32 attr)
|
val_casted_long:
forall si attr n,
val_casted (
Vlong n) (
Tlong si attr)
|
val_casted_ptr_ptr:
forall b ofs ty attr,
val_casted (
Vptr b ofs) (
Tpointer ty attr)
|
val_casted_int_ptr:
forall n ty attr,
val_casted (
Vint n) (
Tpointer ty attr)
|
val_casted_ptr_int:
forall b ofs si attr,
val_casted (
Vptr b ofs) (
Tint I32 si attr)
|
val_casted_struct:
forall id attr b ofs,
val_casted (
Vptr b ofs) (
Tstruct id attr)
|
val_casted_union:
forall id attr b ofs,
val_casted (
Vptr b ofs) (
Tunion id attr)
|
val_casted_void:
forall v,
val_casted v Tvoid.
Remark cast_int_int_idem:
forall sz sg i,
cast_int_int sz sg (
cast_int_int sz sg i) =
cast_int_int sz sg i.
Proof.
Lemma cast_val_is_casted:
forall v ty ty'
v',
sem_cast v ty ty' =
Some v' ->
val_casted v'
ty'.
Proof.
unfold sem_cast;
intros.
destruct ty';
simpl in *.
void *)
constructor.
int *)
destruct i;
destruct ty;
simpl in H;
try (
destruct f);
try discriminate;
destruct v;
inv H.
constructor.
apply (
cast_int_int_idem I8 s).
constructor.
apply (
cast_int_int_idem I8 s).
destruct (
cast_single_int s f);
inv H1.
constructor.
apply (
cast_int_int_idem I8 s).
destruct (
cast_float_int s f);
inv H1.
constructor.
apply (
cast_int_int_idem I8 s).
constructor.
apply (
cast_int_int_idem I16 s).
constructor.
apply (
cast_int_int_idem I16 s).
destruct (
cast_single_int s f);
inv H1.
constructor.
apply (
cast_int_int_idem I16 s).
destruct (
cast_float_int s f);
inv H1.
constructor.
apply (
cast_int_int_idem I16 s).
constructor.
auto.
constructor.
constructor.
auto.
destruct (
cast_single_int s f);
inv H1.
constructor.
auto.
destruct (
cast_float_int s f);
inv H1.
constructor;
auto.
constructor;
auto.
constructor.
constructor;
auto.
constructor.
constructor;
auto.
constructor.
constructor.
simpl.
destruct (
Int.eq i0 Int.zero);
auto.
constructor.
simpl.
destruct (
Int64.eq i Int64.zero);
auto.
constructor.
simpl.
destruct (
Float32.cmp Ceq f Float32.zero);
auto.
constructor.
simpl.
destruct (
Float.cmp Ceq f Float.zero);
auto.
constructor.
simpl.
destruct (
Int.eq i Int.zero);
auto.
constructor.
simpl.
destruct (
Int.eq i Int.zero);
auto.
constructor.
simpl.
destruct (
Int.eq i Int.zero);
auto.
long *)
destruct ty;
try (
destruct f);
try discriminate.
destruct v;
inv H.
constructor.
destruct v;
inv H.
constructor.
destruct v;
try discriminate.
destruct (
cast_single_long s f);
inv H.
constructor.
destruct v;
try discriminate.
destruct (
cast_float_long s f);
inv H.
constructor.
destruct v;
inv H.
constructor.
destruct v;
inv H.
constructor.
destruct v;
inv H.
constructor.
float *)
destruct f;
destruct ty;
simpl in H;
try (
destruct f);
try discriminate;
destruct v;
inv H;
constructor.
pointer *)
destruct ty;
simpl in H;
try discriminate;
destruct v;
inv H;
try constructor.
impossible cases *)
discriminate.
discriminate.
structs *)
destruct ty;
try discriminate;
destruct v;
try discriminate.
destruct (
ident_eq i0 i);
inv H;
constructor.
unions *)
destruct ty;
try discriminate;
destruct v;
try discriminate.
destruct (
ident_eq i0 i);
inv H;
constructor.
Qed.
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;
auto.
inv H0;
auto.
inv H0;
auto.
discriminate.
discriminate.
discriminate.
Qed.
Lemma cast_val_casted:
forall v ty,
val_casted v ty ->
sem_cast v ty ty =
Some v.
Proof.
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.
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 =
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;
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,
val_casted v ty ->
sem_cast v ty (
typeconv ty) =
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 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 tge (
State f (
Sdebug_var id ty)
k e le m)
E0 (
State f Sskip k e le m).
Proof.
intros.
unfold Sdebug_var.
eapply step_builtin with (
optid :=
None).
econstructor.
constructor.
constructor.
eauto.
simpl.
reflexivity.
constructor.
simpl.
constructor.
Qed.
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 =
Some v' ->
plus step2 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 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 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 Int.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 tm te,
list_norepet (
var_names vars) ->
Mem.inject j m tm ->
exists j',
exists te',
exists tm',
alloc_variables tge te tm (
remove_lifted cenv vars)
te'
tm'
/\
Mem.inject j'
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.
base case *)
exists j;
exists te;
exists tm.
simpl.
split.
constructor.
split.
auto.
split.
auto.
split.
auto.
split.
auto.
split.
intros.
elim H2.
eapply Mem.mi_mappedblocks;
eauto.
split.
tauto.
auto.
inductive case *)
simpl in H1.
inv H1.
simpl.
destruct (
VSet.mem id cenv)
eqn:?.
simpl.
variable is lifted out of memory *)
exploit Mem.alloc_left_unmapped_inject;
eauto.
intros [
j1 [
A [
B [
C D]]]].
exploit IHalloc_variables;
eauto.
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 H5.
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.
variable is not lifted out of memory *)
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 H4 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 H3.
eapply Mem.mi_mappedblocks;
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 H5.
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.
unfold access_mode;
intros.
assert (
size_chunk chunk =
sizeof ge ty).
{
destruct ty;
try destruct i;
try destruct s;
try destruct f;
inv H;
auto.
}
omega.
Qed.
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 tm,
alloc_variables ge empty_env m vars e m' ->
list_norepet (
var_names vars) ->
Mem.inject j 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'
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 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 m tm ->
exists tm',
assign_loc tge ty tm loc'
ofs'
v'
tm'
/\
Mem.inject f 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.
Theorem store_params_correct:
forall j 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 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 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 m'
tm'
/\
match_envs j cenv e le m'
lo hi te tle tlo thi
/\
Mem.nextblock tm' =
Mem.nextblock 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 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 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 m1 l m2 m2',
Mem.inject j 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 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 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 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 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 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 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 Int.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 Int.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 Int.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 Int.add_assoc.
decEq.
apply Int.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.
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 m tm)
(
COMPAT:
compat_cenv (
addr_taken_stmt s) (
cenv_for f))
(
BOUND:
Ple hi (
Mem.nextblock m))
(
TBOUND:
Ple thi (
Mem.nextblock 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
(
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 m tm)
(
AINJ:
Val.inject_list j vargs tvargs)
(
FUNTY:
type_of_fundef fd =
Tfunction targs tres cconv)
(
ANORM:
val_casted_list vargs targs),
match_states (
Callstate fd vargs k m)
(
Callstate tfd tvargs tk tm)
|
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 m tm)
(
RINJ:
Val.inject j v tv),
match_states (
Returnstate v k m)
(
Returnstate tv tk tm).
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 step_simulation:
forall S1 t S2,
step1 ge S1 t S2 ->
forall S1' (
MS:
match_states S1 S1'),
exists S2',
plus step2 tge S1'
t S2' /\
match_states S2 S2'.
Proof.
Lemma initial_states_simulation:
forall S,
initial_state prog S ->
exists R,
initial_state 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 prog) (
semantics2 tprog).
Proof.
End PRESERVATION.