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 Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
Require Import Clight.
Require Import SimplLocalsDummy.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import NormaliseSpec.
Require Import Memory.
Require Import Equivalences.
Require Import ClightEquivalences.
Section PRESERVATION.
Variable prog:
program.
Variable tprog:
program.
Hypothesis TRANSF:
transf_program prog =
OK tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof.
Lemma varinfo_preserved:
forall b,
Genv.find_var_info tge b =
Genv.find_var_info ge b.
Proof.
Lemma functions_translated:
forall m (
v:
expr_sym) (
f:
fundef),
Genv.find_funct m ge v =
Some f ->
exists tf,
Genv.find_funct m 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
Record match_envs (
e:
env) (
le:
temp_env) (
m:
mem) (
lo hi:
block)
(
tle:
temp_env) :
Prop :=
mk_match_envs {
me_temps:
forall id v,
le!
id =
Some v ->
(
exists tv,
tle!
id =
Some tv /\
same_eval v tv);
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_incr:
Ple lo hi;
me_bounds:
forall id b ty,
e !
id =
Some (
b,
ty) ->
Mem.bounds_of_block m b = (0,
sizeof ty)
}.
Invariance by change of memory and injection
Lemma match_envs_invariant:
forall e le m lo hi tle m',
match_envs e le m lo hi tle ->
(
forall b,
Ple lo b /\
Plt b hi ->
Mem.bounds_of_block m b =
Mem.bounds_of_block m'
b) ->
match_envs e le m'
lo hi tle.
Proof.
intros until m'; intros ME SB.
destruct ME; constructor; eauto.
intros; auto. rewrite <- SB. eauto.
eapply me_range0. eauto.
Qed.
Invariance by external call
Lemma match_envs_extcall:
forall e le m lo hi tle tm m',
match_envs e le m lo hi tle ->
Mem.unchanged_on (
fun b _ =>
Ple lo b /\
Plt b hi)
m m' ->
Ple hi (
Mem.nextblock m) ->
Ple hi (
Mem.nextblock tm) ->
(
forall b,
Mem.bounds_of_block m b =
Mem.bounds_of_block m'
b) ->
match_envs e le m'
lo hi tle.
Proof.
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_expr v1 (
typeof a)
tto =
Some v2 ->
eval_expr tge e le m (
make_cast a tto)
v2.
Proof.
intros.
econstructor; eauto.
Qed.
Preservation by assignment to a temporary
Lemma match_envs_set_temp:
forall e le m lo hi tle id v tv,
match_envs e le m lo hi tle ->
same_eval v tv ->
match_envs e (
PTree.set id v le)
m lo hi (
PTree.set id tv tle).
Proof.
intros.
destruct H.
constructor;
eauto;
intros.
rewrite PTree.gsspec in *.
destruct (
peq id0 id).
inv H.
exists tv;
split;
auto.
eapply me_temps0;
eauto.
Qed.
Lemma match_envs_set_opttemp:
forall e le m lo hi tle optid v tv,
match_envs e le m lo hi tle ->
same_eval v tv ->
match_envs e (
set_opttemp optid v le)
m lo hi (
set_opttemp optid tv tle).
Proof.
Extensionality with respect to temporaries
Lemma match_envs_temps_exten:
forall e le m lo hi tle tle',
match_envs e le m lo hi tle ->
(
forall id,
tle'!
id =
tle!
id) ->
match_envs e le m lo hi tle'.
Proof.
intros. destruct H. constructor; auto; intros.
rewrite H0. eauto.
Qed.
Invariance by assignment to an irrelevant temporary
Lemma match_envs_change_temp:
forall e le m lo hi tle id v,
match_envs e le m lo hi tle ->
le!
id =
None ->
match_envs e le m lo hi (
PTree.set id v tle).
Proof.
intros.
destruct H.
constructor;
auto;
intros.
rewrite PTree.gso.
eauto.
congruence.
Qed.
Allocation and initialization of parameters
Lemma alloc_variables_nextblock:
forall e m vars e'
m',
alloc_variables e m vars e'
m' ->
Ple (
Mem.nextblock m) (
Mem.nextblock m').
Proof.
Lemma alloc_variables_range:
forall id b ty e m vars e'
m',
alloc_variables 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 id1 b1 ty1 id2 b2 ty2 e m vars e'
m',
alloc_variables 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 alloc_variables_bounds:
forall e m vars e'
m',
alloc_variables e m vars e'
m' ->
(
forall id b ty,
e!
id =
Some (
b,
ty) ->
Mem.valid_block m b) ->
(
forall id ty b,
e!
id =
Some (
b,
ty) ->
Mem.bounds_of_block m b = (0,
sizeof ty)) ->
forall id ty b,
e'!
id =
Some (
b,
ty) ->
Mem.bounds_of_block m'
b = (0,
sizeof ty).
Proof.
Lemma match_alloc_variables:
forall e m vars e'
m'
(
AV:
alloc_variables e m vars e'
m')
tm
(
lnr:
list_norepet (
var_names vars))
(
MINJ:
mem_equiv m tm),
exists tm',
alloc_variables e tm vars e'
tm'
/\
mem_equiv m'
tm'
/\ (
forall id ty,
In (
id,
ty)
vars ->
exists b,
e'!
id =
Some(
b,
ty))
/\ (
forall id, ~
In id (
var_names vars) ->
e'!
id =
e!
id).
Proof.
induction 1;
intros.
-
exists tm;
simpl.
repeat (
split;
auto).
constructor.
tauto.
-
simpl in lnr.
inv lnr.
simpl.
destruct (
alloc_mem_equiv _ _ _ _ _ H _ MINJ)
as [
tm' [
A B]].
exploit IHAV;
eauto.
intros [
tm'0 [
C [
D [
E F]]]].
exists tm'0.
repeat (
split;
eauto).
+
econstructor;
eauto.
+
intros.
destruct (
ident_eq id0 id).
*
subst id0.
assert (
ty0 =
ty).
destruct H0.
congruence.
elim H2.
unfold var_names.
change id with (
fst (
id,
ty0)).
apply in_map;
auto.
subst ty0.
exploit F;
eauto.
intros X.
rewrite X.
rewrite PTree.gss;
eexists;
eauto.
*
exploit (
E id0 ty0).
destruct H0.
congruence.
auto.
auto.
+
intros.
exploit (
F id0).
tauto.
intros X.
rewrite X;
apply PTree.gso;
intuition.
Qed.
Lemma alloc_variables_load:
forall e m vars e'
m',
alloc_variables 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 alloc_variables_bound:
forall e m vars e'
m',
alloc_variables e m vars e'
m' ->
forall b,
Plt b (
Mem.nextblock m) ->
Mem.bounds_of_block m b =
Mem.bounds_of_block m'
b.
Proof.
Lemma sizeof_by_value:
forall ty chunk,
access_mode ty =
By_value chunk ->
size_chunk chunk <=
sizeof ty.
Proof.
unfold access_mode;
intros.
assert (
size_chunk chunk =
sizeof ty).
{
destruct ty;
try destruct i;
try destruct s;
try destruct f;
inv H;
auto.
}
omega.
Qed.
Lemma create_undef_temps_charact:
forall id ty vars,
In (
id,
ty)
vars -> (
create_undef_temps vars)!
id =
Some (
Eval (
Eint Int.zero)).
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 =
Eval (
Eint Int.zero) /\
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 vars_and_temps_properties:
forall 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 (
params ++
vars))
/\
list_disjoint (
var_names params) (
var_names temps).
Proof.
Lemma alloc_variables_preserves_bounds:
forall e m vars e'
m'
(
A:
alloc_variables e m vars e'
m')
tm te te'
tm'
(
TA:
alloc_variables te tm vars te'
tm')
(
sb:
forall b :
block,
Mem.bounds_of_block m b =
Mem.bounds_of_block tm b)
(
nb:
Mem.nextblock m =
Mem.nextblock tm),
forall b :
block,
Mem.bounds_of_block m'
b =
Mem.bounds_of_block tm'
b.
Proof.
Theorem match_envs_alloc_variables:
forall m vars e m'
temps tm
(
AV:
alloc_variables empty_env m vars e m')
(
lnr:
list_norepet (
var_names vars))
(
MINK:
mem_equiv m tm),
exists tm',
alloc_variables empty_env tm vars e tm'
/\
match_envs e (
create_undef_temps temps)
m'
(
Mem.nextblock m) (
Mem.nextblock m')
(
create_undef_temps temps)
/\
mem_equiv m'
tm'.
Proof.
Lemma assign_loc_inject:
forall ty m addr addr'
v m'
tm v',
assign_loc ty m addr v m' ->
same_eval addr addr' ->
same_eval v v' ->
mem_equiv m tm ->
exists tm',
assign_loc ty tm addr'
v'
tm'
/\
mem_equiv m'
tm'.
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 e le)!
id).
eapply IHparams;
eauto.
apply PTree.gso.
intuition.
Qed.
Lemma assign_loc_nextblock:
forall ty m addr v m',
assign_loc ty m addr v m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
Lemma assign_loc_bounds:
forall ty m addr v m'
b,
assign_loc ty m addr v m' ->
Mem.bounds_of_block m b =
Mem.bounds_of_block m'
b.
Proof.
Inductive casted_list :
list expr_sym ->
list type ->
Prop :=
casted_list_nil:
casted_list nil nil
|
casted_list_cons:
forall el tl e t e',
sem_cast_expr e t t =
Some e' ->
same_eval e e' ->
casted_list el tl ->
casted_list (
e::
el) (
t::
tl).
Lemma assign_loc_equiv:
forall ty m e1 e2 m'
e2',
assign_loc ty m e1 e2 m' ->
same_eval e2 e2' ->
exists m2',
assign_loc ty m e1 e2'
m2' /\
mem_equiv m'
m2'.
Proof.
Lemma bpt_set_se:
forall bl params t1 t2 tle',
temp_env_equiv t1 t2 ->
bind_parameter_temps params bl t1 =
Some tle' ->
exists tle'0,
bind_parameter_temps params bl t2 =
Some tle'0 /\
temp_env_equiv tle'
tle'0.
Proof.
induction bl;
destruct params;
simpl;
intros;
try destruct p;
try inv H0.
-
eexists;
split;
auto.
-
eapply IHbl;
eauto.
intro.
rewrite !
PTree.gsspec.
destruct (
peq i0 i);
subst;
auto.
reflexivity.
apply H.
Qed.
Lemma set_se:
forall t id b v,
same_eval b v ->
temp_env_equiv (
PTree.set id b t) (
PTree.set id v t).
Proof.
intros t id b v SE i.
rewrite !
PTree.gsspec.
destruct (
peq i id);
subst;
auto.
destr_cond_match;
auto;
reflexivity.
Qed.
Lemma temp_env_equiv_refl:
forall t,
temp_env_equiv t t.
Proof.
red; intros.
destr_cond_match; auto; reflexivity.
Qed.
Lemma bind_parameters_nextblock:
forall e m params args m',
bind_parameters e m params args m' ->
Mem.nextblock m' =
Mem.nextblock m.
Proof.
Lemma norm_ptr_in_bound:
forall m b ofs,
NormaliseSpec.in_bound (
Int.unsigned ofs) (
Mem.bounds_of_block m b) ->
Mem.mem_norm m (
Eval (
Eptr b ofs))
Ptr =
Vptr b ofs.
Proof.
Lemma norm_ptr_zero:
forall m b,
Mem.mem_norm m (
Eval (
Eptr b Int.zero))
Ptr =
Vptr b Int.zero \/
Mem.mem_norm m (
Eval (
Eptr b Int.zero))
Ptr =
Vundef.
Proof.
Lemma bind_parameters_load:
forall e chunk b ofs,
(
forall id b'
ty,
e!
id =
Some(
b',
ty) ->
b <>
b') ->
forall m params args m',
bind_parameters e m params args m' ->
Mem.load chunk m'
b ofs =
Mem.load chunk m b ofs.
Proof.
Lemma bind_parameters_bound:
forall e b,
(
forall id b'
ty,
e!
id =
Some(
b',
ty) ->
b <>
b') ->
forall m params args m',
bind_parameters e m params args m' ->
Mem.bounds_of_block m'
b =
Mem.bounds_of_block m b.
Proof.
induction 2.
auto.
rewrite IHbind_parameters.
assert (
b <>
b0)
by eauto.
symmetry;
eapply assign_loc_bounds;
eauto.
Qed.
Freeing of local variables
Lemma free_blocks_of_env_perm_1:
forall m e m'
id b ty ofs k p,
Mem.free_list m (
blocks_of_env e) =
Some m' ->
e!
id =
Some(
b,
ty) ->
Mem.perm m'
b ofs k p ->
0 <=
ofs <
sizeof 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 m e m'
id b ty,
Mem.free_list m (
blocks_of_env e) =
Some m' ->
e!
id =
Some(
b,
ty) ->
Mem.range_perm m b 0 (
sizeof 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 free_contents:
forall m b lo hi m',
Mem.free m b lo hi =
Some m' ->
Mem.mem_contents m =
Mem.mem_contents m'.
Proof.
intros m b lo hi m'
F.
Transparent Mem.free.
unfold Mem.free in F.
revert F;
destr_cond_match;
try discriminate.
intro A;
inv A.
simpl;
auto.
Qed.
Theorem match_envs_free_blocks:
forall e m m'
tm,
mem_equiv m tm ->
Mem.free_list m (
blocks_of_env e) =
Some m' ->
exists tm',
Mem.free_list tm (
blocks_of_env e) =
Some tm'
/\
mem_equiv m'
tm'.
Proof.
Matching global environments
Inductive match_globalenvs (
bound:
block):
Prop :=
|
mk_match_globalenvs
(
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).
Evaluation of expressions
Section EVAL_EXPR.
Variables e :
env.
Variables le tle:
temp_env.
Variables m tm:
mem.
Variables lo hi :
block.
Hypothesis MATCH:
match_envs e le m lo hi tle.
Hypothesis MEMINJ:
mem_equiv m tm.
Hypothesis GLOB:
exists bound,
match_globalenvs bound.
Lemma deref_loc_se:
forall ty addr v addr',
deref_loc ty m addr v ->
same_eval addr addr' ->
exists tv,
deref_loc ty tm addr'
tv
/\
same_eval v tv.
Proof.
Lemma eval_simpl_expr:
forall a v,
eval_expr ge e le m a v ->
exists tv,
eval_expr tge e tle tm a tv /\
same_eval v tv
with eval_simpl_lvalue:
forall a addr,
eval_lvalue ge e le m a addr ->
exists addr',
eval_lvalue tge e tle tm a addr' /\
same_eval addr addr'.
Proof.
destruct 1;
simpl;
intros.
-
eexists;
split;
eauto;
repeat (
constructor;
simpl;
auto).
-
eexists;
split;
eauto;
repeat (
constructor;
simpl;
auto).
-
eexists;
split;
eauto;
repeat (
constructor;
simpl;
auto).
-
eexists;
split;
eauto;
repeat (
constructor;
simpl;
auto).
-
exploit me_temps;
eauto.
intros [
tv [
A B]].
exists tv;
split;
auto.
constructor;
auto.
-
exploit eval_simpl_lvalue;
eauto.
intros [
addr' [
A B]].
(
exists addr');
split;
auto.
constructor;
auto.
-
exploit eval_simpl_expr;
eauto.
intros [
tv1 [
A B]].
generalize (
sem_unary_operation_expr_se op (
typeof a)
_ _ B).
intro C.
eexists;
split;
eauto.
econstructor;
eauto.
subst;
auto.
-
exploit eval_simpl_expr.
eexact H.
intros [
tv1 [
A B]].
exploit eval_simpl_expr.
eexact H0.
intros [
tv2 [
C D]].
generalize (
sem_binary_operation_expr_se
m op (
typeof a1) (
typeof a2)
_ _ _ _ B D).
rewrite H1.
destr_cond_match;
try tauto.
intro E.
eexists;
split;
eauto.
econstructor;
eauto.
-
exploit eval_simpl_expr;
eauto.
intros [
tv1 [
A B]].
generalize (
sem_cast_expr_se (
typeof a)
ty _ _ B).
rewrite H0.
destr_cond_match;
try tauto;
intro E.
eexists ;
split;
eauto.
econstructor.
eauto.
eauto.
-
exploit eval_simpl_lvalue;
eauto.
intros [
addr' [
A B]].
exploit deref_loc_se;
eauto.
intros [
tv [
C D]].
eexists tv;
split;
eauto.
econstructor.
eexact A.
eauto.
-
destruct 1;
simpl;
intros.
+
eexists;
split;
eauto.
econstructor;
eauto.
reflexivity.
+
eexists;
split;
eauto.
rewrite <-
symbols_preserved in H0.
eapply eval_Evar_global;
eauto.
reflexivity.
+
exploit eval_simpl_expr;
eauto.
intros [
tv [
A B]].
eexists;
split.
econstructor;
simpl;
eauto.
auto.
+
exploit eval_simpl_expr;
eauto.
intros [
tv [
A B]].
eexists;
split.
econstructor;
eauto.
apply binop_same_eval;
auto.
reflexivity.
+
exploit eval_simpl_expr;
eauto.
intros [
tv [
A B]].
eexists;
split.
eapply eval_Efield_union;
eauto.
auto.
Qed.
Lemma eval_simpl_exprlist:
forall al tyl vl,
eval_exprlist ge e le m al tyl vl ->
exists tvl,
eval_exprlist tge e tle tm al tyl tvl
/\
list_forall2 same_eval vl tvl.
Proof.
induction 1;
simpl;
intros.
econstructor;
split.
constructor.
constructor.
exploit eval_simpl_expr;
eauto.
intros [
tv1 [
A B]].
generalize (
sem_cast_expr_se (
typeof a)
ty _ _ B);
rewrite H0.
destr_cond_match;
try tauto;
intro C.
destruct IHeval_exprlist as [
tvl [
E F]].
exists (
e0 ::
tvl);
split.
econstructor;
eauto.
econstructor;
eauto.
Qed.
End EVAL_EXPR.
Matching continuations
Inductive match_cont :
cont ->
cont ->
mem ->
block ->
block ->
Prop :=
|
match_Kstop:
forall m bound tbound hi,
match_globalenvs hi ->
Ple hi bound ->
Ple hi tbound ->
match_cont Kstop Kstop m bound tbound
|
match_Kseq:
forall s k tk m bound tbound,
match_cont k tk m bound tbound ->
match_cont (
Kseq s k) (
Kseq s tk)
m bound tbound
|
match_Kloop1:
forall s1 s2 k tk m bound tbound,
match_cont k tk m bound tbound ->
match_cont (
Kloop1 s1 s2 k) (
Kloop1 s1 s2 tk)
m bound tbound
|
match_Kloop2:
forall s1 s2 k tk m bound tbound,
match_cont k tk m bound tbound ->
match_cont (
Kloop2 s1 s2 k) (
Kloop2 s1 s2 tk)
m bound tbound
|
match_Kswitch:
forall k tk m bound tbound,
match_cont k tk m bound tbound ->
match_cont (
Kswitch k) (
Kswitch tk)
m bound tbound
|
match_Kcall:
forall optid fn e le k tfn tle tk m hi thi lo bound tbound,
transf_function fn =
OK tfn ->
match_envs e le m lo hi tle ->
match_cont k tk m lo lo ->
Ple hi bound ->
Ple thi tbound ->
match_cont (
Kcall optid fn e le k)
(
Kcall optid tfn e tle tk)
m bound tbound.
Invariance property by change of memory and injection
Lemma match_cont_invariant:
forall m'
k tk m bound tbound,
match_cont k tk m bound tbound ->
(
forall b,
Plt b bound ->
Mem.bounds_of_block m b =
Mem.bounds_of_block m'
b) ->
match_cont k tk m'
bound tbound.
Proof.
induction 1;
simpl;
intros ME;
econstructor;
eauto.
eapply match_envs_invariant;
eauto.
intros.
eapply ME;
eauto.
xomega.
eapply IHmatch_cont;
eauto.
intros;
eapply ME;
eauto.
inv H0;
xomega.
Qed.
Invariance by assignment to location "above"
Lemma match_cont_assign_loc:
forall k tk m bound tbound ty addr loc ofs v m',
match_cont k tk m bound tbound ->
assign_loc ty m addr v m' ->
Mem.mem_norm m addr Ptr =
Vptr loc ofs ->
Ple bound loc ->
match_cont k tk m'
bound tbound.
Proof.
Invariance by external calls
Invariance by change of bounds
Lemma match_cont_incr_bounds:
forall k tk m bound tbound,
match_cont k tk m bound tbound ->
forall bound'
tbound',
Ple bound bound' ->
Ple tbound tbound' ->
match_cont k tk m bound'
tbound'.
Proof.
induction 1; intros; econstructor; eauto; xomega.
Qed.
match_cont and call continuations.
Lemma match_cont_is_call_cont:
forall k tk m bound tbound,
match_cont 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 k tk m bound tbound,
match_cont k tk m bound tbound ->
match_cont (
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 e le m lo hi tle tm k tk m'
tm',
match_envs e le m lo hi tle ->
match_cont k tk m lo lo ->
Ple hi (
Mem.nextblock m) ->
Mem.free_list m (
blocks_of_env e) =
Some m' ->
Mem.free_list tm (
blocks_of_env e) =
Some tm' ->
mem_equiv m tm ->
match_cont k tk m' (
Mem.nextblock m') (
Mem.nextblock tm').
Proof.
Matching of global environments
Lemma match_cont_globalenv:
forall k tk m bound tbound,
match_cont k tk m bound tbound ->
exists bound,
match_globalenvs bound.
Proof.
induction 1; auto. exists hi; auto.
Qed.
Hint Resolve match_cont_globalenv:
compat.
Lemma match_cont_find_funct:
forall k tk m tm bound tbound vf fd tvf,
match_cont k tk m bound tbound ->
Genv.find_funct m ge vf =
Some fd ->
same_eval vf tvf ->
mem_equiv m tm ->
exists tfd,
Genv.find_funct tm tge tvf =
Some tfd /\
transf_fundef fd =
OK tfd.
Proof.
Relating execution states
Fixpoint type_list_of_typelist (
tl:
typelist) :
list type :=
match tl with
Tnil =>
nil
|
Tcons a b =>
a::(
type_list_of_typelist b)
end.
Inductive match_states:
state ->
state ->
Prop :=
|
match_regular_states:
forall f s k e le m tf tk tle tm lo hi
(
TRF:
transf_function f =
OK tf)
(
MENV:
match_envs e le m lo hi tle)
(
MCONT:
match_cont k tk m lo lo)
(
MINJ:
mem_equiv m tm)
(
BOUND:
Ple hi (
Mem.nextblock m)),
match_states (
State f s k e le m)
(
State tf s tk e tle tm)
|
match_call_state:
forall fd vargs k m tfd tvargs tk tm targs tres cconv
(
TRFD:
transf_fundef fd =
OK tfd)
(
MCONT:
match_cont k tk m (
Mem.nextblock m) (
Mem.nextblock tm))
(
MINJ:
mem_equiv m tm)
(
AINJ:
casted_list vargs (
type_list_of_typelist targs))
(
SE:
list_forall2 same_eval vargs tvargs)
(
FUNTY:
type_of_fundef fd =
Tfunction targs tres cconv),
match_states (
Callstate fd vargs k m)
(
Callstate tfd tvargs tk tm)
|
match_return_state:
forall v k m tv tk tm
(
MCONT:
match_cont k tk m (
Mem.nextblock m) (
Mem.nextblock tm))
(
MINJ:
mem_equiv m tm)
(
RINJ:
same_eval v tv),
match_states (
Returnstate v k m)
(
Returnstate tv tk tm).
The simulation diagrams
Section FIND_LABEL.
Variable m:
mem.
Variables bound tbound:
block.
Variable lbl:
ident.
Lemma simpl_find_label:
forall s k tk,
match_cont k tk m bound tbound ->
match find_label lbl s k with
|
None =>
find_label lbl s tk =
None
|
Some(
s',
k') =>
exists tk',
find_label lbl s tk =
Some(
s',
tk')
/\
match_cont k'
tk'
m bound tbound
end
with simpl_find_label_ls:
forall ls k tk,
match_cont k tk m bound tbound ->
match find_label_ls lbl ls k with
|
None =>
find_label_ls lbl ls tk =
None
|
Some(
s',
k') =>
exists tk',
find_label_ls lbl ls tk =
Some(
s',
tk')
/\
match_cont k'
tk'
m bound tbound
end.
Proof.
induction s;
simpl;
intros until tk;
intros MC;
auto.
-
exploit (
IHs1 (
Kseq s2 k) (
Kseq s2 tk));
eauto with compat.
constructor;
eauto with compat.
destruct (
find_label lbl s1 (
Kseq s2 k))
as [[
s'
k']|].
intros [
tk' [
P Q]].
exists tk'.
simpl.
rewrite P.
auto.
intros E.
simpl.
rewrite E.
eapply IHs2;
eauto with compat.
-
exploit (
IHs1 k tk);
eauto with compat.
destruct (
find_label lbl s1 k)
as [[
s'
k']|].
intros [
tk' [
P Q]].
exists tk'.
simpl.
rewrite P.
auto.
intros E.
simpl.
rewrite E.
eapply IHs2;
eauto with compat.
-
exploit (
IHs1 (
Kloop1 s1 s2 k) (
Kloop1 s1 s2 tk));
eauto with compat.
constructor;
eauto with compat.
destruct (
find_label lbl s1 (
Kloop1 s1 s2 k))
as [[
s'
k']|].
intros [
tk' [
P Q]].
exists tk'.
simpl.
rewrite P.
auto.
intros E.
simpl.
rewrite E.
eapply IHs2;
eauto with compat.
econstructor;
eauto with compat.
-
eapply simpl_find_label_ls;
eauto with compat.
constructor;
auto.
-
destruct (
ident_eq lbl l).
+ (
exists tk;
auto).
+
eapply IHs;
eauto.
-
induction ls;
simpl;
intros;
auto.
exploit (
simpl_find_label s (
Kseq (
seq_of_labeled_statement ls)
k)).
constructor;
eauto.
destruct (
find_label lbl s (
Kseq (
seq_of_labeled_statement ls)
k))
as [[
s'
k']|].
intros [
tk' [
P Q]].
rewrite P.
eexists;
split;
eauto.
intros E.
simpl;
rewrite E.
eapply IHls;
eauto with compat.
Qed.
Lemma find_label_store_params:
forall lbl s k params,
find_label lbl (
store_params params s)
k =
find_label lbl s k.
Proof.
induction params; simpl. auto.
destruct a as [id ty]. auto.
Qed.
End FIND_LABEL.
Lemma free_list_bounds_after:
forall bl m m',
Mem.free_list m bl =
Some m' ->
forall b lo0 hi0,
Mem.bounds_of_block m'
b = (
lo0,
hi0) ->
hi0 -
lo0 <> 0 ->
Mem.bounds_of_block m b = (
lo0,
hi0).
Proof.
induction bl;
simpl;
intros;
auto.
-
inv H;
auto.
-
destruct a as [[
b'
lo]
hi].
destruct (
Mem.free m b'
lo hi)
eqn:?;
try discriminate.
eapply IHbl in H;
eauto.
destruct (
Mem.free_bounds _ _ _ _ _ b Heqo);
auto.
congruence.
rewrite H in H2;
inv H2;
omega.
Qed.
Lemma bpt_se:
forall vargs tvargs,
list_forall2 same_eval vargs tvargs ->
forall te pars e m0 m1,
bind_parameters e m0 pars vargs m1 ->
exists ee,
bind_parameter_temps pars tvargs te =
Some ee.
Proof.
induction 1; simpl; intros; eauto.
inv H; simpl. eexists; eauto.
inv H1. eapply IHlist_forall2 in H9; eauto.
Qed.
Lemma bpt_se':
forall vargs tyargs,
casted_list vargs tyargs ->
forall te pars e m0 m1,
bind_parameters e m0 pars vargs m1 ->
exists ee,
bind_parameter_temps pars vargs te =
Some ee.
Proof.
induction 1; simpl; intros; eauto.
inv H; simpl. eexists; eauto.
inv H2.
eapply IHcasted_list in H10; eauto.
Qed.
Lemma bpt_se'':
forall vargs tvargs,
list_forall2 same_eval vargs tvargs ->
forall pars te te'
ee,
temp_env_equiv te te' ->
bind_parameter_temps pars vargs te =
Some ee ->
exists ee',
bind_parameter_temps pars tvargs te' =
Some ee' /\
temp_env_equiv ee ee'.
Proof.
induction 1;
simpl;
intros.
-
destruct pars;
simpl in *;
try intuition congruence;
try destruct p;
inv H0.
eexists;
split;
eauto.
inv H0.
auto.
destruct p;
inv H0.
-
destruct pars;
simpl in *;
try intuition congruence;
try destruct p;
inv H0.
destruct p.
eapply IHlist_forall2 in H2;
eauto.
intro;
intros.
rewrite !
PTree.gsspec.
destruct (
peq i0 i);
simpl;
auto.
apply H1.
Qed.
Lemma unop_ext_se:
forall s0 n v1,
0 <
n ->
same_eval
(
Eunop
(
match s0 with
|
Signed =>
OpSignext
|
Unsigned =>
OpZeroext
end n)
Tint v1)
(
Eunop
(
match s0 with
|
Signed =>
OpSignext
|
Unsigned =>
OpZeroext
end n)
Tint
(
Eunop
(
match s0 with
|
Signed =>
OpSignext
|
Unsigned =>
OpZeroext
end n)
Tint v1)).
Proof.
Lemma boolval_idem_se:
forall v1,
same_eval (
Eunop OpBoolval Tint v1)
(
Eunop OpBoolval Tint (
Eunop OpBoolval Tint v1)).
Proof.
Lemma notbool_boolval_se:
forall e,
same_eval (
Eunop OpNotbool Tint e)
(
Eunop OpBoolval Tint (
Eunop OpNotbool Tint e)).
Proof.
Lemma sem_cast_expr_idem:
forall v1 ta ty v2,
sem_cast_expr v1 ta ty =
Some v2 ->
exists v2',
sem_cast_expr v2 ty ty =
Some v2' /\
same_eval v2 v2'.
Proof.
intros.
unfold sem_cast_expr in H.
destruct ta eqn:?;
destruct ty eqn:?;
simpl in *;
inv H;
unfold sem_cast_expr;
simpl;
try (
eexists;
split;
eauto;
reflexivity).
destruct i;
simpl in *;
inv H1.
destruct f;
simpl;
inv H1.
destruct i0;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
reflexivity.
apply boolval_idem_se.
destruct f;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct i;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
reflexivity.
apply notbool_boolval_se.
destruct f;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct i;
simpl in *;
inv H1;
eexists;
split;
eauto;
try destruct f;
inv H0;
try apply unop_ext_se;
try omega;
try reflexivity;
try apply notbool_boolval_se.
destruct f0;
destruct f;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct i;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
reflexivity.
apply notbool_boolval_se.
destruct f;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct i;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
reflexivity.
apply notbool_boolval_se.
destruct f;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct i;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
reflexivity.
apply notbool_boolval_se.
destruct f;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct i0;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
destruct f0;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct (
ident_eq i0 i0);
destruct (
fieldlist_eq f0 f0);
simpl;
try congruence.
eexists;
split;
eauto;
reflexivity.
destruct i0;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
destruct f0;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
destruct (
ident_eq i0 i0);
destruct (
fieldlist_eq f0 f0);
simpl;
try congruence.
eexists;
split;
eauto;
reflexivity.
destruct i0;
simpl in *;
inv H1;
eexists;
split;
eauto;
try apply unop_ext_se;
try omega.
reflexivity.
apply notbool_boolval_se.
destruct f;
simpl;
inv H1;
eexists;
split;
eauto;
reflexivity.
Qed.
Lemma eval_exprlist_casted_list:
forall ge e le m al tyargs vargs,
eval_exprlist ge e le m al tyargs vargs ->
casted_list vargs (
type_list_of_typelist tyargs).
Proof.
induction 1;
simpl;
auto.
constructor.
apply sem_cast_expr_idem in H0.
destruct H0 as [
v2' [
A B]].
econstructor;
eauto.
Qed.
Lemma params_type_list:
forall f,
(
type_list_of_typelist (
type_of_params (
fn_params f))) =
map snd (
fn_params f).
Proof.
intro.
generalize (
fn_params f).
induction l;
simpl;
intros;
eauto.
destruct a;
simpl;
eauto.
congruence.
Qed.
Lemma temp_env_equiv_sym:
forall t1 t2,
temp_env_equiv t1 t2 ->
temp_env_equiv t2 t1.
Proof.
intros t1 t2 A; red; intro i; specialize (A i);
repeat destr_cond_match; try symmetry; auto.
Qed.
Lemma temp_env_equiv_trans:
forall t1 t2 t3,
temp_env_equiv t1 t2 ->
temp_env_equiv t2 t3 ->
temp_env_equiv t1 t3.
Proof.
intros t1 t2 t3 A B; red; intro i;
specialize (A i); specialize (B i);
repeat destr_cond_match; destruct (t2!i) eqn:?; simpl in *; auto;
etransitivity; eauto; try tauto.
Qed.
Instance temp_env_equiv_equi :
RelationClasses.Equivalence temp_env_equiv :=
RelationClasses.Build_Equivalence _ _
(
temp_env_equiv_refl)
(
temp_env_equiv_sym)
(
temp_env_equiv_trans).
Theorem store_params_correct:
forall e m params args m',
bind_parameters e m params args m' ->
casted_list args (
map snd params) ->
forall f k le lo hi ,
forall s tm tle1 targs,
list_norepet (
var_names params) ->
list_forall2 same_eval args targs ->
match_envs e le m lo hi tle1 ->
mem_equiv m tm ->
(
forall id,
In id (
var_names params) ->
le!
id =
None) ->
forall tle ,
bind_parameter_temps params args tle1 =
Some tle ->
exists tm',
star step2 tge (
State f (
store_params params s)
k e tle tm)
E0 (
State f s k e tle tm')
/\
mem_equiv m'
tm'
/\
match_envs e le m'
lo hi tle
/\
Mem.nextblock tm' =
Mem.nextblock tm
/\ (
forall b,
Mem.bounds_of_block tm'
b =
Mem.bounds_of_block tm b).
Proof.
Inductive match_cont_eq :
cont ->
cont ->
Prop :=
|
match_cont_eq_stop:
match_cont_eq Kstop Kstop
|
match_cont_eq_seq:
forall s k k',
match_cont_eq k k' ->
match_cont_eq (
Kseq s k) (
Kseq s k')
|
match_cont_eq_loop1:
forall s t k k',
match_cont_eq k k' ->
match_cont_eq (
Kloop1 s t k) (
Kloop1 s t k')
|
match_cont_eq_loop2:
forall s t k k',
match_cont_eq k k' ->
match_cont_eq (
Kloop2 s t k) (
Kloop2 s t k')
|
match_cont_eq_switch:
forall k k',
match_cont_eq k k' ->
match_cont_eq (
Kswitch k) (
Kswitch k')
|
match_cont_eq_call:
forall k k'
te te'
oi f e,
temp_env_equiv te te' ->
match_cont_eq k k' ->
match_cont_eq (
Kcall oi f e te k) (
Kcall oi f e te'
k').
Inductive match_states_eq :
state ->
state ->
Prop :=
|
match_states_eq_state:
forall f s k k'
e te te'
m m',
temp_env_equiv te te' ->
mem_equiv m m' ->
match_cont_eq k k' ->
match_states_eq (
State f s k e te m) (
State f s k'
e te'
m')
|
match_states_eq_call:
forall f el el'
k k'
m m',
list_forall2 same_eval el el' ->
mem_equiv m m' ->
match_cont_eq k k' ->
match_states_eq (
Callstate f el k m) (
Callstate f el'
k'
m')
|
match_states_eq_ret:
forall e e'
k k'
m m',
match_cont_eq k k' ->
mem_equiv m m' ->
same_eval e e' ->
match_states_eq (
Returnstate e k m) (
Returnstate e'
k'
m').
Lemma mem_temp_equiv_expr_lvalue:
forall ge e le le'
m m',
mem_equiv m m' ->
temp_env_equiv le le' ->
(
forall a v,
Clight.eval_expr ge e le m a v ->
exists v',
Clight.eval_expr ge e le'
m'
a v' /\
same_eval v v')
/\(
forall a v,
Clight.eval_lvalue ge e le m a v ->
exists v',
Clight.eval_lvalue ge e le'
m'
a v' /\
same_eval v v').
Proof.
intros ge0 e le le'
m m'
ME TEE.
apply eval_expr_lvalue_ind;
intros.
-
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
reflexivity.
-
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
reflexivity.
-
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
reflexivity.
-
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
reflexivity.
-
specialize (
TEE id);
rewrite H in TEE.
destruct (
le'!
id)
eqn:?;
try tauto.
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
-
destruct H0 as [
v' [
A B]].
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
-
destruct H0 as [
v' [
A B]].
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
subst.
apply sem_unary_operation_expr_se;
auto.
-
destruct H0 as [
v' [
A B]].
destruct H2 as [
v'' [
C D]].
generalize (
sem_binary_operation_expr_se m op (
typeof a1) (
typeof a2)
_ _ _ _ B D).
rewrite H3.
destr_cond_match;
try tauto.
intro;
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
-
destruct H0 as [
v' [
A B]].
generalize (
sem_cast_expr_se (
typeof a)
ty _ _ B).
rewrite H1.
destr_cond_match;
try tauto.
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
-
destruct H0 as [
v' [
A B]].
eapply deref_loc_se in H1;
eauto.
destruct H1 as [
tv [
C D]].
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
-
eexists;
split;
eauto.
econstructor;
simpl;
eauto.
reflexivity.
-
eexists;
split;
eauto.
eapply eval_Evar_global;
eauto.
reflexivity.
-
destruct H0 as [
v' [
A B]].
eexists;
split;
eauto.
econstructor.
eauto.
-
destruct H0 as [
v' [
A B]].
eexists;
split;
eauto.
econstructor;
eauto.
apply binop_same_eval;
auto.
reflexivity.
-
destruct H0 as [
v' [
A B]].
eexists;
split;
eauto.
econstructor;
eauto.
Qed.
Lemma mem_temp_equiv_expr:
forall ge e le le'
m m',
mem_equiv m m' ->
temp_env_equiv le le' ->
forall a v,
Clight.eval_expr ge e le m a v ->
exists v',
Clight.eval_expr ge e le'
m'
a v' /\
same_eval v v'.
Proof.
Lemma mem_temp_equiv_lvalue:
forall ge e le le'
m m',
mem_equiv m m' ->
temp_env_equiv le le' ->
forall a v,
Clight.eval_lvalue ge e le m a v ->
exists v',
Clight.eval_lvalue ge e le'
m'
a v' /\
same_eval v v'.
Proof.
Lemma mem_temp_equiv_exprlist:
forall ge e le m al tl vl le'
m',
mem_equiv m m' ->
temp_env_equiv le le' ->
eval_exprlist ge e le m al tl vl ->
exists vl',
eval_exprlist ge e le'
m'
al tl vl' /\
list_forall2 same_eval vl vl'.
Proof.
Lemma mem_equiv_same_eval_norm:
forall m m'
e1 e2 r,
mem_equiv m m' ->
same_eval e1 e2 ->
Mem.mem_norm m e1 r =
Mem.mem_norm m'
e2 r.
Proof.
Ltac simpeq :=
repeat match goal with
H:
eval_lvalue ?
tge ?
e ?
le ?
m ?
a1 ?
vptr,
ME:
mem_equiv ?
m ?
m',
TE:
temp_env_equiv ?
le ?
le' |-
_ =>
let vptr' :=
fresh "
vptr"
in
let se :=
fresh "
SE"
in
apply (
mem_temp_equiv_lvalue tge e le le'
m m'
ME TE)
in H;
destruct H as [
vptr' [
H se]]
|
H:
Mem.mem_norm ?
m ?
e ?
r =
_,
ME:
mem_equiv ?
m ?
m',
SE:
same_eval ?
e ?
e' |-
_ =>
rewrite (
mem_equiv_same_eval_norm m m'
e e'
r ME SE)
in H
|
H:
eval_expr ?
tge ?
e ?
le ?
m ?
a1 ?
v,
ME:
mem_equiv ?
m ?
m',
TE:
temp_env_equiv ?
le ?
le' |-
_ =>
let v' :=
fresh "
v"
in
let se :=
fresh "
SE"
in
apply (
mem_temp_equiv_expr tge e le le'
m m'
ME TE)
in H;
destruct H as [
v' [
H se]]
|
H:
eval_exprlist ?
tge ?
e ?
le ?
m ?
al ?
tl ?
vl,
ME:
mem_equiv ?
m ?
m',
TE:
temp_env_equiv ?
le ?
le' |-
_ =>
let vl' :=
fresh "
vl"
in
let se :=
fresh "
SE"
in
apply (
mem_temp_equiv_exprlist tge e le m al tl vl _ _ ME TE)
in H;
destruct H as [
vl' [
H se]]
|
H:
sem_cast_expr ?
v2 ?
ty ?
ty' =
Some ?
v,
SE:
same_eval ?
v2 ?
v3 |-
_ =>
let v :=
fresh "
v"
in
let se :=
fresh "
SE"
in
let sce :=
fresh "
SCE"
in
generalize (
sem_cast_expr_se ty ty'
_ _ SE);
rewrite H;
destruct (
sem_cast_expr v3 ty ty')
as [
v|]
eqn:
SCE;
try tauto;
intro se
|
H:
assign_loc ?
ty ?
m ?
addr ?
v ?
m2,
ME:
mem_equiv ?
m ?
m',
SE1:
same_eval ?
addr ?
addr',
SE2:
same_eval ?
v ?
v' |-
_ =>
let m2 :=
fresh "
m"
in
let me :=
fresh "
ME"
in
let al :=
fresh "
AL"
in
destruct (
assign_loc_inject _ _ _ _ _ _ _ _ H SE1 SE2 ME)
as [
m2 [
al me]];
clear H
|
H:
Genv.find_funct ?
m ?
ge ?
v =
_,
ME:
mem_equiv ?
m ?
m',
SE:
same_eval ?
v ?
v' |-
_ =>
rewrite (
genv_find_funct_equiv ge _ _ _ _ ME SE)
in H
|
H:
match_cont_eq (
Kseq ?
s ?
k) ?
k' |-
_ =>
inv H
|
H:
match_cont_eq (
Kloop1 ?
s ?
t ?
k) ?
k' |-
_ =>
inv H
|
H:
match_cont_eq (
Kloop2 ?
s ?
t ?
k) ?
k' |-
_ =>
inv H
|
H:
match_cont_eq (
Kswitch ?
k) ?
k' |-
_ =>
inv H
|
H:
match_cont_eq (
Kcall ?
oi ?
f ?
e ?
te ?
k) ?
k' |-
_ =>
inv H
|
H:
Mem.free_list ?
m ?
bl =
Some ?
m',
ME:
mem_equiv ?
m ?
m2 |-
_ =>
let m2 :=
fresh "
m2"
in
let me :=
fresh "
ME"
in
apply (
free_list_mem_equiv _ _ _ _ ME)
in H;
destruct H as [
m2 [
H me]]
end.
Lemma match_cont_eq_call_cont:
forall k k',
match_cont_eq k k' ->
match_cont_eq (
call_cont k) (
call_cont k').
Proof.
induction 1; simpl; intros; try constructor; auto.
Qed.
Lemma is_call_cont_match_eq:
forall k k',
match_cont_eq k k' ->
is_call_cont k ->
is_call_cont k'.
Proof.
induction 1; simpl; intros; auto.
Qed.
Lemma find_label_cont:
forall lbl s k tk,
match_cont_eq k tk ->
match find_label lbl s k with
|
None =>
find_label lbl s tk =
None
|
Some(
s',
k') =>
exists tk',
find_label lbl s tk =
Some(
s',
tk')
/\
match_cont_eq k'
tk'
end
with find_label_ls_cont:
forall lbl ls k tk,
match_cont_eq k tk ->
match find_label_ls lbl ls k with
|
None =>
find_label_ls lbl ls tk =
None
|
Some(
s',
k') =>
exists tk',
find_label_ls lbl ls tk =
Some(
s',
tk')
/\
match_cont_eq k'
tk'
end.
Proof.
-
induction s;
simpl;
intros until tk;
intros MC;
auto.
+
assert (
match_cont_eq (
Kseq s2 k) (
Kseq s2 tk))
by (
constructor;
auto).
destruct (
find_label lbl s1 (
Kseq s2 k))
eqn:?.
generalize (
IHs1 _ _ H).
*
destruct p.
rewrite Heqo.
intros [
tk' [
A B]].
rewrite A.
eexists;
split;
eauto.
*
generalize (
IHs1 _ _ H).
rewrite Heqo.
intro A.
rewrite A.
apply IHs2.
auto.
+
destruct (
find_label lbl s1 k)
eqn:?.
generalize (
IHs1 _ _ MC).
*
destruct p.
rewrite Heqo.
intros [
tk' [
A B]].
rewrite A.
eexists;
split;
eauto.
*
generalize (
IHs1 _ _ MC).
rewrite Heqo.
intro A.
rewrite A.
apply IHs2.
auto.
+
assert (
match_cont_eq (
Kloop1 s1 s2 k) (
Kloop1 s1 s2 tk))
by (
constructor;
auto).
destruct (
find_label lbl s1 (
Kloop1 s1 s2 k))
eqn:?.
generalize (
IHs1 _ _ H).
*
destruct p.
rewrite Heqo.
intros [
tk' [
A B]].
rewrite A.
eexists;
split;
eauto.
*
generalize (
IHs1 _ _ H).
rewrite Heqo.
intro A.
rewrite A.
apply IHs2.
constructor;
auto.
+
apply find_label_ls_cont.
constructor;
auto.
+
destruct (
ident_eq lbl l);
subst;
auto.
eexists;
split;
eauto.
apply IHs.
auto.
-
induction ls;
simpl in *.
auto.
intros.
exploit (
find_label_cont lbl s (
Kseq (
seq_of_labeled_statement ls)
k));
eauto.
econstructor;
eauto.
destruct (
find_label lbl s (
Kseq (
seq_of_labeled_statement ls)
k))
eqn:?;
eauto.
destruct p.
intros [
tk' [
A B]].
rewrite A.
eexists;
split;
eauto.
intro A;
rewrite A.
apply IHls.
auto.
Qed.
Lemma find_label_call_cont:
forall lbl f k k'0
s'
k',
find_label lbl (
fn_body f) (
call_cont k) =
Some (
s',
k') ->
match_cont_eq k k'0 ->
exists k2,
find_label lbl (
fn_body f) (
call_cont k'0) =
Some (
s',
k2) /\
match_cont_eq k'
k2.
Proof.
Lemma bpt_mem_equiv_temp_equiv:
forall params el te tte,
bind_parameter_temps params el te =
Some tte ->
forall el'
te',
list_forall2 same_eval el el' ->
temp_env_equiv te te' ->
exists tte',
bind_parameter_temps params el'
te' =
Some tte' /\
temp_env_equiv tte tte'.
Proof.
induction params;
simpl;
intros;
auto.
-
destruct el;
simpl in *;
try discriminate.
inv H.
inv H0.
eexists;
split;
auto.
-
destruct a.
destruct el;
try discriminate.
inv H0.
eapply IHparams in H;
eauto.
apply temp_env_equiv_set;
auto.
Qed.
Lemma step_equiv_builtin:
forall ef e le te'
f m m'
m'0
optid vres vargs vl tyargs t k k'
al,
eval_exprlist tge e te'
m'0
al tyargs vl ->
list_forall2 same_eval vargs vl ->
external_call ef tge vargs m t vres m' ->
temp_env_equiv le te' ->
mem_equiv m m'0 ->
match_cont_eq k k' ->
exists S2' :
state,
step2 tge (
State f (
Sbuiltin optid ef tyargs al)
k'
e te'
m'0)
t S2' /\
match_states_eq (
State f Sskip k e (
set_opttemp optid vres le)
m')
S2'.
Proof.
intros.
eapply external_call_se in H1;
eauto.
destruct H1 as [
vres' [
m2' [
A [
B C]]]].
destruct ef;
intros;
simpl in *;
try (
eexists;
split;
eauto; [
econstructor;
eauto|
constructor;
auto;
destruct optid;
auto;
apply temp_env_equiv_set;
auto]).
Qed.
Lemma step_equiv_external:
forall ef m m'
m'0
vres vargs el'
cconv tres targs t k k' ,
external_call ef tge vargs m t vres m' ->
list_forall2 same_eval vargs el' ->
mem_equiv m m'0 ->
match_cont_eq k k' ->
exists S2' :
state,
step2 tge (
Callstate (
External ef targs tres cconv)
el'
k'
m'0)
t S2' /\
match_states_eq (
Returnstate vres k m')
S2'.
Proof.
intros.
eapply external_call_se in H1;
eauto.
destruct H1 as [
vres' [
m2' [
A [
B C]]]].
destruct ef;
intros;
simpl in *;
try (
eexists;
split;
eauto; [
econstructor;
eauto|
constructor;
auto;
destruct optid;
auto;
apply temp_env_equiv_set;
auto]).
Qed.
Lemma step_equiv:
forall S1 t S2,
step2 tge S1 t S2 ->
forall S1' (
MS:
match_states_eq S1 S1'),
exists S2',
step2 tge S1'
t S2' /\
match_states_eq S2 S2'.
Proof.
Lemma star_step_equiv:
forall S1 t S2,
star step2 tge S1 t S2 ->
forall S1' (
MS:
match_states_eq S1 S1'),
exists S2',
star step2 tge S1'
t S2' /\
match_states_eq S2 S2'.
Proof.
induction 1;
simpl;
intros.
- (
exists S1';
split;
auto).
apply star_refl.
-
eapply step_equiv in H;
eauto.
destruct H as [
s2' [
A B]].
apply IHstar in B.
destruct B as [
S2' [
AA BB]].
eexists;
split;
eauto.
eapply star_left;
eauto.
Qed.
Lemma match_cont_eq_refl:
forall k,
match_cont_eq k k.
Proof.
induction k; simpl; intros; try constructor; auto.
reflexivity.
Qed.
Lemma match_envs_temp_equiv:
forall e le m lo hi tle tle',
match_envs e le m lo hi tle ->
temp_env_equiv tle tle' ->
match_envs e le m lo hi tle'.
Proof.
destruct 1; intros; constructor; auto.
intros.
apply me_temps0 in H0; eauto.
destruct H0 as [tv [A B]].
specialize (H id); rewrite A in H; destruct (tle'!id) eqn:?; try tauto.
eexists; split; eauto.
rewrite B; auto.
Qed.
Lemma match_cont_eq_match_cont:
forall k tk m lo hi,
match_cont k tk m lo hi ->
forall k'
(
MCE:
match_cont_eq tk k'),
match_cont k k'
m lo hi.
Proof.
Lemma menv_ec:
forall ef vargs m t vres m'
le e lo hi tle
(
EC:
external_call ef ge vargs m t vres m')
(
MENV :
match_envs e le m lo hi tle),
match_envs e le m'
lo hi tle.
Proof.
Lemma mcont_ec:
forall ef vargs m t vres m'
k k'
lo hi
(
EC:
external_call ef ge vargs m t vres m')
(
MENV :
match_cont k k'
m lo hi),
match_cont k k'
m'
lo hi.
Proof.
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.
Theorem transf_program_correct:
forward_simulation (
semantics1 prog) (
semantics2 tprog).
Proof.
End PRESERVATION.