Require Import Coqlib Maps Integers Values Memdata AST Globalenvs.
Require Import Blockset Footprint FMemOpFP GMemory FMemory FMemPerm FMemLemmas MemAux CUAST LDSimDefs Localize ValRels MemInterpolant val_casted Ctypes Floats.
Require Import AsmLocalize Clight ClightLang Clight_local ClightWD.
Lemma init_genv_iff:
forall cu ge G,
ClightLang.init_genv cu ge G <->
G = {|
Clight.genv_genv :=
ge;
Clight.genv_cenv :=
cu_comp_env cu |} /\
ge_related ge (
Genv.globalenv (
mkprogram (
cu_defs cu) (
cu_public cu) 1%
positive)).
Proof.
Hint Resolve FPlocalize_emp FPlocalize_union :
fplocalize.
Lemma init_mem_valid_block:
forall ge m,
ClightLang.init_gmem ge m ->
(
forall b,
Bset.belongsto (
valid_block_bset m)
b <->
Plt b (
Genv.genv_next ge)).
Proof.
Definition env_rel (
j:
Bset.inj)(
a b:
block*
type):=
let (
la,
tya):=
a in
let (
lb,
tyb):=
b in
val_related j (
Vptr la Ptrofs.zero)(
Vptr lb Ptrofs.zero) /\
tya =
tyb.
Definition env_related (
j:
Bset.inj)(
e e':
env):
Prop:=
forall id,
option_rel (
fun (
a b:
block*
type)=>
let (
la,
tya):=
a in let (
lb,
tyb):=
b in val_related j (
Vptr la Ptrofs.zero)(
Vptr lb Ptrofs.zero) /\
tya =
tyb) (
e!
id)(
e'!
id).
Definition tenv_related (
j:
Bset.inj)(
e e':
temp_env):
Prop:=
forall id,
option_rel (
val_related j)(
e !
id)(
e' !
id).
Ltac det :=
match goal with
| [
H1:
eval_expr ?
ge ?
sp ?
e ?
m ?
a ?
v1,
H2:
eval_expr ?
ge ?
sp ?
e ?
m ?
a ?
v2
|-
_ ] =>
pose proof (
eval_expr_det _ _ _ _ _ _ H1 _ H2);
subst v1;
clear H1
| [
H1:
eval_expr_fp ?
ge ?
sp ?
e ?
m ?
a ?
v1,
H2:
eval_expr_fp ?
ge ?
sp ?
e ?
m ?
a ?
v2
|-
_ ] =>
pose proof (
eval_expr_fp_det _ _ _ _ _ _ H1 _ H2);
subst v1;
clear H1
| [
H1: ?
x = ?
y1,
H2: ?
x = ?
y2 |-
_] =>
rewrite H1 in H2;
inv H2
end.
Ltac inv_eq:=
repeat match goal with
|
H:?
P ,
H1: ?
P |-
_ =>
clear H
|
H:
context[
match ?
x with _ =>
_ end] |-
_ =>
destruct x eqn:?;
inversion H ;
subst
|
H:?
P = ?
Q,
H1:
context [ ?
P ] |-
_ =>
rewrite H in H1
|
H:?
P = ?
Q |-
context [ ?
P ] =>
rewrite H
|
H:
Some ?
P =
Some ?
Q |-
_ =>
inv H
end;
simpl in *;
subst;
try contradiction;
try discriminate.
Definition trans_c_fundef_ast (
f:
fundef): (
AST.fundef function):=
match f with
Ctypes.Internal x =>
AST.Internal x
|
Ctypes.External x _ _ _ =>
AST.External x
end.
Fixpoint trans_cu_defs_ast_defs (
l:
list (
ident *
globdef fundef Ctypes.type)) :
list (
ident *
globdef (
AST.fundef function)
Ctypes.type):=
match l with
nil =>
nil
| (
id,
x)::
ls =>
cons (
match x with
Gfun y => (
id,
Gfun (
trans_c_fundef_ast y))
|
Gvar y => (
id,
Gvar y)
end) (
trans_cu_defs_ast_defs ls)
end.
Fixpoint ef_name_notin (
name:
String.string)(
ids:
list (
ident*
globdef fundef type)) :
bool :=
match ids with
|
nil =>
true
| (
id,
gd) ::
ids' =>
match gd_ef_fun_name gd with
|
Some name' =>
if String.string_dec name name'
then false
else ef_name_notin name ids'
|
_ =>
ef_name_notin name ids'
end
end.
Lemma ef_name_notin_correct:
forall name defs,
ef_name_notin name defs =
true ->
forall id gd name',
In (
id,
gd)
defs ->
gd_ef_fun_name gd =
Some name' ->
name <>
name'.
Proof.
induction defs;
simpl;
intros.
contradiction.
destruct a.
destruct g.
destruct f.
simpl in *.
inv H0.
inv H2.
discriminate.
eapply IHdefs;
eauto.
destruct gd_ef_fun_name eqn:
NAME.
destruct String.string_dec.
discriminate.
inv H0.
inv H2.
rewrite NAME in H1.
inv H1.
auto.
eapply IHdefs;
eauto.
inv H0.
inv H2.
congruence.
eapply IHdefs;
eauto.
destruct gd_ef_fun_name eqn:
NAME.
destruct String.string_dec;
try congruence.
inv H0.
inv H2.
congruence.
eapply IHdefs;
eauto.
inv H0.
inv H2.
congruence.
eapply IHdefs;
eauto.
Qed.
Fixpoint nodup_ef ids :
bool :=
match ids with
|
nil =>
true
| (
id,
gd) ::
ids' =>
match gd_ef_fun_name gd with
|
Some name =>
ef_name_notin name ids' &&
nodup_ef ids'
|
None =>
nodup_ef ids'
end
end.
Lemma nodup_ef_correct:
forall ids,
nodup_ef ids =
true ->
forall n1 n2 id1 gd1 id2 gd2 name1 name2,
n1 <>
n2 ->
nth_error ids n1 =
Some (
id1,
gd1) ->
nth_error ids n2 =
Some (
id2,
gd2) ->
gd_ef_fun_name gd1 =
Some name1 ->
gd_ef_fun_name gd2 =
Some name2 ->
name1 <>
name2.
Proof.
Definition wdcu (
cu:
clight_comp_unit) :
Prop :=
nodup_ef (
cu_defs cu) =
true /\
nodup_gd_ident (
cu_defs cu) =
true.
Definition transge cu := (
Genv.globalenv {|
AST.prog_defs :=
cu_defs cu;
AST.prog_public :=
cu_public cu;
AST.prog_main := 1%
positive |}).
Lemma norepet_defs_gd_ident_exists:
forall cu,
list_norepet (
map fst (
cu_defs cu)) ->
forall b gd,
PTree.get b (
Genv.genv_defs (
transge cu)) =
Some gd ->
exists id,
PTree.get id (
Genv.genv_symb (
transge cu)) =
Some b.
Proof.
Lemma nodup_gd_ident_exists:
forall cu,
nodup_gd_ident (
cu_defs cu) =
true ->
forall b gd,
PTree.get b (
Genv.genv_defs (
transge cu)) =
Some gd ->
exists id,
PTree.get id (
Genv.genv_symb (
transge cu)) =
Some b.
Proof.
Lemma nodup_gd_ident_exists':
forall cu,
nodup_gd_ident (
cu_defs cu) =
true ->
forall b gd,
PTree.get b (
Genv.genv_defs (
transge cu)) =
Some gd ->
exists id,
In (
id,
gd) (
cu_defs cu) /\
PTree.get id (
Genv.genv_symb (
transge cu)) =
Some b.
Proof.
Lemma wdcu_goodge:
forall cu (
R:
wdcu cu)
b gd, (
Genv.genv_defs (
transge cu)) !
b =
Some gd ->
exists id, (
Genv.genv_symb (
transge cu)) !
id =
Some b.
Proof.
Lemma nodup_ef_ge_norep_ef_name:
forall cu,
wdcu cu->
norep_ef_name (
transge cu).
Proof.
destruct 1.
unfold transge.
unfold norep_ef_name.
intros.
exploit nodup_gd_ident_exists';
try eexact H1;
eauto.
intros [
id1 [
IN1 FIND1]].
exploit nodup_gd_ident_exists';
try eexact H2;
eauto.
intros [
id2 [
IN2 FIND2]].
unfold Genv.find_def,
transge in *.
unfold Genv.globalenv in *.
simpl in *.
assert(
id1 <>
id2).
{
intro.
apply H1.
congruence. }
apply In_nth_error in IN1 as [
n1 IN1].
apply In_nth_error in IN2 as [
n2 IN2].
assert(
n2 <>
n1).
intro;
subst.
apply H1;
congruence.
eapply nodup_ef_correct;
try eassumption.
Qed.
Lemma weak_valid_pointer_related:
forall (
j :
Bset.inj) (
bound :
block) (
fl :
freelist)
(
m :
Memory.Mem.mem) (
m' :
mem) (
b b' :
block) (
ofs :
Z),
mem_related j bound fl (
strip m')
m ->
construct_inj j bound fl b =
Some b' ->
Memory.Mem.weak_valid_pointer m b ofs =
Mem.weak_valid_pointer m'
b'
ofs.
Proof.
Lemma env_related_set:
forall j e e',
env_related j e e'->
forall id b b'
ty,
val_related j (
Vptr b Ptrofs.zero)(
Vptr b'
Ptrofs.zero)->
env_related j (
PTree.set id (
b,
ty)
e)(
PTree.set id (
b',
ty)
e').
Proof.
Section EXPR.
Variable sge tge:
Clight.genv.
Variable j:
Bset.inj.
Hypothesis GEMATCH:
ge_match_strict j (
genv_genv sge)(
genv_genv tge).
Hypothesis GEQ:
genv_cenv sge =
genv_cenv tge.
Definition bound:=(
Genv.genv_next(
genv_genv sge)).
Hypothesis INJECT :
Bset.inject j (
fun b :
block =>
Plt b bound) (
fun b :
block =>
Plt b bound).
Section SEM_EXPR.
Variable e e':
env.
Variable le le':
temp_env.
Variable fm:
FMemory.mem.
Variable m:
Memory.mem.
Definition fl:=
FMemory.Mem.freelist fm.
Hypothesis MEMREL:
mem_related j bound fl (
strip fm)
m.
Definition j' :=
construct_inj j bound fl.
Hypothesis ENVREL:
env_related j'
e'
e.
Hypothesis TENVREL:
tenv_related j'
le'
le.
Hypothesis NOREP:
norep fl.
Hypothesis NOOVERLAP:
no_overlap fl (
fun b=>
Plt b bound).
Lemma injective_j':
forall b b0 b',
j'
b =
Some b' ->
j'
b0 =
Some b' ->
b =
b0.
Proof.
Lemma bool_val_related:
forall v ty b v',
val_related j'
v'
v->
FCop.bool_val v ty fm =
Some b->
Cop.bool_val v'
ty m =
Some b .
Proof.
Lemma bool_val_fp_related:
forall v ty b v',
val_related j'
v'
v->
Cop_fp.bool_val_fp v ty fm =
Some b->
exists b',
Cop_fp_local.bool_val_fp v'
ty m =
Some b'/\
FPlocalize j'
b b'.
Proof.
Lemma sem_unary_operation_localize:
forall v v',
val_related j'
v'
v->
forall op ty resv,
FCop.sem_unary_operation op v ty fm =
Some resv->
exists resv',
Cop.sem_unary_operation op v'
ty m =
Some resv' /\
val_related j'
resv'
resv.
Proof.
Lemma sem_unary_operation_fp_localize:
forall v v',
val_related j'
v'
v->
forall op ty,
option_rel (
FPlocalize j') (
Cop_fp.sem_unary_operation_fp op v ty fm)(
Cop_fp_local.sem_unary_operation_fp op v'
ty m).
Proof.
Lemma sizeof_eq:
forall ty,
Ctypes.sizeof sge ty =
Ctypes.sizeof tge ty.
Proof.
induction ty;
simpl;
auto;
try congruence.
all:
rewrite GEQ;
auto.
Qed.
Lemma alignof_eq:
forall ty,
Ctypes.alignof sge ty =
Ctypes.alignof tge ty.
Proof.
induction ty;
simpl;
auto;
try congruence.
all:
rewrite GEQ;
auto.
Qed.
Definition binary_related_correct
(
sem:
val->
type->
val->
type->
mem->
option val)
(
sem2:
val->
type->
val->
type->
Memory.Mem.mem->
option val) :
Prop:=
forall va tya vb tyb v,
sem va tya vb tyb fm =
Some v->
forall va'
vb',
val_related j'
va'
va ->
val_related j'
vb'
vb ->
exists v',
sem2 va'
tya vb'
tyb m =
Some v' /\
val_related j'
v'
v.
Definition binary_fp_related_correct
(
semfp:
val->
type->
val->
type->
mem->
option FP.t)
(
semfp2:
val->
type->
val->
type->
Memory.Mem.mem->
option FP.t) :
Prop:=
forall va tya vb tyb fp,
semfp va tya vb tyb fm =
Some fp->
forall va'
vb',
val_related j'
va'
va->
val_related j'
vb'
vb->
exists fp',
semfp2 va'
tya vb'
tyb m =
Some fp' /\
FPlocalize j'
fp fp'.
Section MAKE_BIN.
Variable sem_int:
signedness ->
int ->
int ->
option val.
Variable sem_long:
signedness ->
int64 ->
int64 ->
option val.
Variable sem_float:
float ->
float ->
option val.
Variable sem_single:
float32 ->
float32 ->
option val.
Definition notptr v:=
match v with
|
Vptr _ _ =>
false
|
_ =>
true
end =
true.
Hypothesis sem_int_rel:
forall sg a b i,
sem_int sg a b =
Some i->
notptr i.
Hypothesis sem_long_rel:
forall sg a b i,
sem_long sg a b =
Some i->
notptr i.
Hypothesis sem_float_rel:
forall a b i,
sem_float a b =
Some i->
notptr i.
Hypothesis sem_single_rel:
forall a b i,
sem_single a b =
Some i->
notptr i.
Lemma sem_cast_related:
forall va va',
val_related j'
va'
va->
forall tya ty res,
FCop.sem_cast va tya ty fm =
Some res ->
exists res',
Cop.sem_cast va'
tya ty m =
Some res' /\
val_related j'
res'
res.
Proof.
Lemma sem_cast_fp_related:
forall va va',
val_related j'
va'
va->
forall tya ty fp,
Cop_fp.sem_cast_fp va tya ty fm =
Some fp ->
exists fp',
Cop_fp_local.sem_cast_fp va'
tya ty m =
Some fp' /\
FPlocalize j'
fp fp'.
Proof.
Lemma sem_cast_related2:
forall va va',
val_related j'
va'
va->
forall tya ty,
FCop.sem_cast va tya ty fm =
None->
Cop.sem_cast va'
tya ty m =
None.
Proof.
Lemma sem_binarith_correct:
binary_related_correct (
FCop.sem_binarith sem_int sem_long sem_float sem_single)(
Cop.sem_binarith sem_int sem_long sem_float sem_single).
Proof.
Lemma sem_binarith_fp_correct:
binary_fp_related_correct (
Cop_fp.sem_binarith_fp sem_int sem_long sem_float sem_single)(
Cop_fp_local.sem_binarith_fp sem_int sem_long sem_float sem_single).
Proof.
End MAKE_BIN.
Lemma sem_add_correct:
binary_related_correct (
FCop.sem_add sge)(
Cop.sem_add tge).
Proof.
Lemma sem_add_fp_correct:
binary_fp_related_correct (
Cop_fp.sem_add_fp sge)(
Cop_fp_local.sem_add_fp tge).
Proof.
Lemma sem_sub_correct:
binary_related_correct (
FCop.sem_sub sge)(
Cop.sem_sub tge).
Proof.
red.
unfold Cop.sem_sub,
FCop.sem_sub.
intros until v.
intros SEM ? ?
REL1 REL2.
destruct (
Cop.classify_sub tya tyb);
eauto.
{
inv REL1;
inv REL2;
try discriminate.
destruct Archi.ptr64;
try discriminate;
inv SEM;
Esimpl;
eauto;
rewrite sizeof_eq;
constructor.
inv SEM.
Esimpl;
eauto.
rewrite sizeof_eq;
constructor;
auto.
}
{
inv REL1;
inv REL2;
try discriminate.
inv_eq.
eapply injective_j'
in H;
eauto;
subst b0.
destruct (
eq_block b b);
try contradiction.
Esimpl;
eauto.
constructor.
}
{
inv REL1;
inv REL2;
try discriminate;
inv_eq;
Esimpl;
eauto.
}
eapply sem_binarith_correct;
eauto;
intros;
inv_eq;
unfold notptr;
eauto.
Qed.
Lemma sem_sub_fp_correct:
binary_fp_related_correct (
Cop_fp.sem_sub_fp sge)(
Cop_fp_local.sem_sub_fp tge).
Proof.
red.
unfold Cop_fp.sem_sub_fp,
Cop_fp_local.sem_sub_fp.
intros until fp.
intros SEM ? ?
REL1 REL2.
destruct (
Cop.classify_sub tya tyb);
eauto.
{
inv REL1;
inv REL2;
try discriminate.
destruct Archi.ptr64;
try discriminate;
inv SEM;
Esimpl;
eauto with fplocalize.
inv SEM;
Esimpl;
eauto with fplocalize.
}
{
inv REL1;
inv REL2;
try discriminate.
inv_eq.
eapply injective_j'
in H;
eauto;
subst b0.
destruct (
eq_block b b);
try contradiction.
Esimpl;
eauto with fplocalize.
}
{
inv REL1;
inv REL2;
try discriminate;
inv_eq;
Esimpl;
eauto with fplocalize.
}
eapply sem_binarith_fp_correct;
eauto with fplocalize.
Qed.
Lemma sem_mul_correct:
binary_related_correct FCop.sem_mul Cop.sem_mul .
Proof.
Lemma sem_mul_fp_correct:
binary_fp_related_correct Cop_fp.sem_mul_fp Cop_fp_local.sem_mul_fp .
Proof.
Lemma sem_div_correct:
binary_related_correct FCop.sem_div Cop.sem_div.
Proof.
Lemma sem_div_fp_correct:
binary_fp_related_correct Cop_fp.sem_div_fp Cop_fp_local.sem_div_fp .
Proof.
Lemma sem_mod_correct:
binary_related_correct FCop.sem_mod Cop.sem_mod.
Proof.
Lemma sem_mod_fp_correct:
binary_fp_related_correct Cop_fp.sem_mod_fp Cop_fp_local.sem_mod_fp .
Proof.
Lemma sem_and_correct:
binary_related_correct FCop.sem_and Cop.sem_and.
Proof.
Lemma sem_and_fp_correct:
binary_fp_related_correct Cop_fp.sem_and_fp Cop_fp_local.sem_and_fp .
Proof.
Lemma sem_or_correct:
binary_related_correct FCop.sem_or Cop.sem_or.
Proof.
Lemma sem_or_fp_correct:
binary_fp_related_correct Cop_fp.sem_or_fp Cop_fp_local.sem_or_fp .
Proof.
Lemma sem_xor_correct:
binary_related_correct FCop.sem_xor Cop.sem_xor.
Proof.
Lemma sem_xor_fp_correct:
binary_fp_related_correct Cop_fp.sem_xor_fp Cop_fp_local.sem_xor_fp .
Proof.
Lemma cmp_ptr_correct:
forall v1 v1'
v2 v2',
val_related j'
v1'
v1->
val_related j'
v2'
v2->
forall op res,
FCop.cmp_ptr fm op v1 v2 =
Some res->
exists res',
Cop.cmp_ptr m op v1'
v2' =
Some res' /\
val_related j'
res'
res.
Proof.
Lemma cmp_ptr_fp_correct:
forall v1 v1'
v2 v2',
val_related j'
v1'
v1->
val_related j'
v2'
v2->
forall op res,
Cop_fp.cmp_ptr_fp fm op v1 v2 =
Some res->
exists res',
Cop_fp_local.cmp_ptr_fp m op v1'
v2' =
Some res' /\
FPlocalize j'
res res'.
Proof.
Ltac inv_val_rel:=
match goal with
|
H:
val_related _ _ _ |-
_ =>
inv H;
try discriminate
end.
Ltac goal_destruct:=
match goal with
|
H:
_ |-
context[
if ?
x then Vtrue else Vfalse] =>
destruct x
end.
Ltac solv_cmp:=
unfold FCop.sem_cmp,
Cop.sem_cmp in *;
destruct Cop.classify_cmp eqn:?;
try discriminate;
try(
eapply sem_binarith_correct;
eauto;
intros;
inv_eq;
unfold notptr,
Val.of_bool;
goal_destruct;
auto;
fail);
try(
inv_val_rel;
inv_val_rel;
inv_eq;
try(
eapply cmp_ptr_correct;
eauto;
constructor);
fail).
Lemma sem_binary_operation_localize:
forall v1 v2 v1'
v2',
val_related j'
v1'
v1 ->
val_related j'
v2'
v2 ->
forall op res t1 t2,
FCop.sem_binary_operation sge op v1 t1 v2 t2 fm =
Some res ->
exists res',
Cop.sem_binary_operation tge op v1'
t1 v2'
t2 m =
Some res' /\
val_related j'
res'
res.
Proof.
Lemma deref_loc_related:
forall ty loc ofs v,
deref_loc ty fm loc ofs v ->
forall loc'
ofs',
val_related j' (
Vptr loc'
ofs')(
Vptr loc ofs) ->
exists v',
Clight.deref_loc ty m loc'
ofs'
v' /\
val_related j'
v'
v.
Proof.
inversion 1;
subst;
intros.
exploit loadv_related;
eauto;
intro;
simpl in *.
rewrite H1 in H3.
inv H3.
Esimpl;
eauto.
econstructor;
eauto.
Esimpl;
eauto.
econstructor 2;
eauto.
Esimpl;
eauto.
econstructor 3;
eauto.
Qed.
Lemma sem_binary_operation_fp_localize:
forall v1 v2 v1'
v2',
val_related j'
v1'
v1 ->
val_related j'
v2'
v2 ->
forall op res t1 t2,
Cop_fp.sem_binary_operation_fp sge op v1 t1 v2 t2 fm =
Some res ->
exists res',
Cop_fp_local.sem_binary_operation_fp tge op v1'
t1 v2'
t2 m =
Some res' /\
FPlocalize j'
res res'.
Proof.
Lemma eval_expr_lvalue_localize:
(
forall a v,
ClightLang.eval_expr sge e le fm a v ->
exists v',
Clight.eval_expr tge e'
le'
m a v' /\
val_related j'
v'
v) /\
(
forall a b ofs,
ClightLang.eval_lvalue sge e le fm a b ofs ->
exists b'
ofs',
Clight.eval_lvalue tge e'
le'
m a b'
ofs' /\
val_related j' (
Vptr b'
ofs')(
Vptr b ofs)).
Proof.
apply eval_expr_lvalue_ind;
intros.
all:
Hsimpl;
try (
Esimpl;
eauto;
try econstructor;
eauto;
fail).
{
specialize (
TENVREL id).
inv TENVREL;
try congruence.
rewrite H in H1;
inv H1.
Esimpl;
eauto.
econstructor;
eauto.
}
{
eapply sem_unary_operation_localize in H1;
eauto.
Hsimpl;
Esimpl;
eauto.
econstructor;
eauto.
}
{
Hsimpl.
eapply sem_binary_operation_localize in H3;
eauto.
Hsimpl;
Esimpl;
eauto.
econstructor;
eauto.
}
{
eapply sem_cast_related in H1;
eauto.
Hsimpl;
Esimpl;
eauto.
econstructor;
eauto.
}
{
Esimpl.
econstructor;
eauto.
unfold Vptrofs.
destruct Archi.ptr64 eqn:?;
try discriminate.
rewrite sizeof_eq.
constructor.
}
{
Esimpl;
eauto.
econstructor;
eauto.
rewrite alignof_eq.
constructor.
}
{
eapply deref_loc_related in H1 as ?;
eauto.
Hsimpl;
Esimpl;
eauto.
econstructor;
eauto.
}
{
unfold env_related in ENVREL.
specialize (
ENVREL id).
rewrite H in *.
inv ENVREL.
destruct x.
destruct H2.
subst.
Esimpl;
eauto.
econstructor;
eauto.
}
{
unfold env_related in ENVREL.
specialize (
ENVREL id).
rewrite H in *.
inv ENVREL.
eapply Localize.ge_match_strict_senv with(
id0:=
id)
in GEMATCH as ?.
inv H1;
inv_eq.
Esimpl;
eauto.
econstructor 2;
eauto.
econstructor;
eauto.
unfold j'.
unfold construct_inj.
destruct plt;
auto.
eapply INJECT in H6.
unfold Bset.belongsto in H6.
contradiction.
}
{
inv H1.
Esimpl;
eauto.
econstructor;
eauto.
}
{
inv H4.
rewrite GEQ in *.
Esimpl;
eauto.
econstructor;
eauto.
}
{
inv H3.
rewrite GEQ in *.
Esimpl;
econstructor;
eauto.
}
Qed.
Lemma eval_expr_localize:
forall a v,
ClightLang.eval_expr sge e le fm a v ->
exists v',
Clight.eval_expr tge e'
le'
m a v' /\
val_related j'
v'
v.
Proof.
Lemma eval_lvalue_localize:
forall a b ofs,
ClightLang.eval_lvalue sge e le fm a b ofs ->
exists b'
ofs',
Clight.eval_lvalue tge e'
le'
m a b'
ofs' /\
val_related j' (
Vptr b'
ofs')(
Vptr b ofs).
Proof.
Lemma deref_loc_fp_related:
forall ty loc ofs fp,
ClightLang.deref_loc_fp ty loc ofs fp->
forall loc'
ofs',
val_related j' (
Vptr loc'
ofs')(
Vptr loc ofs)->
exists fp',
Clight_local.deref_loc_fp ty loc'
ofs'
fp' /\
FPlocalize j'
fp fp'.
Proof.
assert(
INJ:
Bset.inj_inject j').
unfold Bset.inj_inject.
apply injective_j'.
inversion 1;
subst;
intros.
{
Esimpl;
eauto.
econstructor;
eauto.
eapply loadv_fp_localize;
eauto.
}
{
Esimpl;
eauto with fplocalize.
econstructor 2;
eauto with fplocalize.
}
{
Esimpl;
eauto with fplocalize.
econstructor 3;
eauto.
}
Qed.
Lemma eval_expr_lvalue_fp_localize:
(
forall a fp,
ClightLang.eval_expr_fp sge e le fm a fp ->
forall v (
EX:
ClightLang.eval_expr sge e le fm a v),
exists fp',
Clight_local.eval_expr_fp tge e'
le'
m a fp'/\
FPlocalize j'
fp fp') /\
(
forall a v,
ClightLang.eval_lvalue_fp sge e le fm a v ->
forall b ofs (
EX:
ClightLang.eval_lvalue sge e le fm a b ofs),
exists v',
Clight_local.eval_lvalue_fp tge e'
le'
m a v' /\
FPlocalize j'
v v').
Proof.
Lemma eval_expr_fp_localize:
forall a fp,
ClightLang.eval_expr_fp sge e le fm a fp ->
forall v (
EX:
ClightLang.eval_expr sge e le fm a v),
exists fp',
Clight_local.eval_expr_fp tge e'
le'
m a fp'/\
FPlocalize j'
fp fp'.
Proof.
Lemma eval_lvalue_fp_localize:
forall a v,
ClightLang.eval_lvalue_fp sge e le fm a v ->
forall b ofs (
EX:
ClightLang.eval_lvalue sge e le fm a b ofs),
exists v',
Clight_local.eval_lvalue_fp tge e'
le'
m a v' /\
FPlocalize j'
v v'.
Proof.
Lemma eval_exprlist_localize:
forall la tyl lv,
ClightLang.eval_exprlist sge e le fm la tyl lv ->
exists lv',
Clight.eval_exprlist tge e'
le'
m la tyl lv' /\
list_forall2 (
val_related j')
lv'
lv.
Proof.
induction 1;
intros.
Esimpl;
eauto;
econstructor.
Hsimpl.
eapply eval_expr_localize in H as ?;
eauto.
Hsimpl.
eapply sem_cast_related in H0;
eauto.
Hsimpl.
Esimpl;
eauto;
econstructor;
eauto.
Qed.
Lemma eval_exprlist_fp_localize:
forall la tyl fp,
ClightLang.eval_exprlist_fp sge e le fm la tyl fp->
exists fp',
Clight_local.eval_exprlist_fp tge e'
le'
m la tyl fp' /\
FPlocalize j'
fp fp'.
Proof.
Lemma assign_loc_related:
forall loc ofs loc'
ofs'
v v',
val_related j'
v'
v->
val_related j' (
Vptr loc'
ofs')(
Vptr loc ofs)->
forall ty fm',
ClightLang.assign_loc sge ty fm loc ofs v fm'->
exists m',
Clight.assign_loc tge ty m loc'
ofs'
v'
m' /\
mem_related j bound fl (
strip fm')
m'.
Proof.
intros.
inv H1.
eapply storev_related in H as ?;
eauto.
rewrite H3 in H1.
inv H1.
Esimpl;
eauto.
econstructor;
eauto.
Qed.
Lemma assign_loc_fp_related:
forall loc ofs loc'
ofs'
v v',
val_related j' (
Vptr loc'
ofs')(
Vptr loc ofs)->
forall ty fp,
ClightLang.assign_loc_fp sge ty loc ofs v fp ->
exists fp',
Clight_local.assign_loc_fp tge ty loc'
ofs'
v'
fp' /\
FPlocalize j'
fp fp'.
Proof.
End SEM_EXPR.
Definition binj_to_bofsinj (
f:
block->
option block)(
x y:
block*
Z*
Z):
Prop:=
let (
tx,
hi):=
x in
let (
b,
lo):=
tx in
let (
ty,
hi'):=
y in
let (
b',
lo'):=
ty in
f b =
Some b' /\
lo =
lo' /\
hi =
hi'.
Lemma env_related_l:
forall f e e',
env_related f e e'->
list_forall2
(
fun i_x i_y :
positive * (
block *
type) =>
fst i_x =
fst i_y /\
(
let (
la,
tya) :=
snd i_x in
let (
lb,
tyb) :=
snd i_y in
val_related f (
Vptr la Ptrofs.zero) (
Vptr lb Ptrofs.zero) /\
tya =
tyb))
(
PTree.elements e) (
PTree.elements e').
Proof.
Lemma block_of_binding_mapping:
forall f (
x y:
positive *(
block*
type)),
fst x =
fst y ->
let (
la,
tya) :=
snd x in
let (
lb,
tyb) :=
snd y in
val_related f (
Vptr la Ptrofs.zero) (
Vptr lb Ptrofs.zero) /\
tya =
tyb->
binj_to_bofsinj f (
block_of_binding tge x)(
block_of_binding sge y).
Proof.
intros f [?[]] [?[]];
simpl;
intros ? [];
subst.
inv H0.
Esimpl;
eauto.
rewrite sizeof_eq;
eauto.
Qed.
Lemma env_related_l2:
forall f e e',
env_related f e e'->
list_forall2 (
binj_to_bofsinj f)(
blocks_of_env tge e)(
blocks_of_env sge e').
Proof.
Lemma freelist_related:
forall fm e fm' (
NOREP':
norep (
Mem.freelist fm))(
NOOVERLAP':
no_overlap (
Mem.freelist fm) (
fun b=>
Plt b bound)),
FMemory.Mem.free_list fm (
blocks_of_env sge e) =
Some fm'->
forall e'
m,
mem_related j bound (
Mem.freelist fm)(
strip fm)
m->
env_related (
j'
fm)
e'
e ->
exists m',
Memory.Mem.free_list m (
blocks_of_env tge e') =
Some m' /\
mem_related j bound (
Mem.freelist fm)(
strip fm')
m'.
Proof.
intros.
pose proof env_related_l2 _ _ _ H1.
clear H1.
revert H H2.
generalize dependent fm;
generalize dependent fm';
generalize dependent m.
generalize (
blocks_of_env sge e)(
blocks_of_env tge e').
clear e e'.
induction l;
intros.
{
assert(
l=
nil).
destruct l;
auto.
simpl in *.
inv H2.
subst.
simpl in *.
inv H.
Esimpl;
eauto.
}
{
simpl in H.
destruct a as ((
b,
lo),
hi),
Mem.free eqn:?;
try discriminate.
inv H2.
simpl.
unfold binj_to_bofsinj in H5.
destruct a1 as ((
b__a,
lo__a),
hi__a).
simpl in *.
Hsimpl;
subst.
exploit free_related;
eauto.
rewrite Heqo.
intros R;
inv R.
apply Mem.free_freelist in Heqo as ?.
unfold j',
fl in *.
rewrite <-
H3 in *.
exploit IHl;
eauto.
}
Qed.
Lemma freelist_fp_related:
forall m e1 e2 (
NOREP':
norep (
Mem.freelist m))(
NOOVERLAP':
no_overlap (
Mem.freelist m) (
fun b=>
Plt b bound)),
env_related (
j'
m)
e1 e2 ->
FPlocalize (
j'
m) (
free_list_fp (
blocks_of_env sge e2)) (
free_list_fp (
blocks_of_env tge e1)).
Proof.
Lemma alloc_variables_related:
forall v fm e e'
fm' (
NOREP':
norep (
Mem.freelist fm)),
alloc_variables sge e fm v e'
fm'->
forall m e2,
mem_related j bound (
Mem.freelist fm) (
strip fm)
m->
env_related (
j'
fm)
e2 e->
exists e2'
m',
Clight.alloc_variables tge e2 m v e2'
m' /\
mem_related j bound (
Mem.freelist fm) (
strip fm')
m' /\
env_related (
j'
fm)
e2'
e'.
Proof.
Lemma alloc_variables_fp_related:
forall v fm fp (
NOREP':
norep (
Mem.freelist fm))(
NOOVERLAP':
no_overlap (
Mem.freelist fm) (
fun b=>
Plt b bound)),
ClightLang.alloc_variables_fp sge fm v fp->
forall m,
mem_related j bound (
Mem.freelist fm) (
strip fm)
m->
exists fp',
Clight_local.alloc_variables_fp tge m v fp' /\
FPlocalize (
j'
fm)
fp fp'.
Proof.
Opaque Memory.Mem.alloc.
Lemma tenv_related_setid:
forall j te1 te2,
tenv_related j te1 te2->
forall id v v',
val_related j v v'->
tenv_related j (
PTree.set id v te1)(
PTree.set id v'
te2).
Proof.
Lemma bind_parameter_temps_related:
forall p vargs t le,
bind_parameter_temps p vargs t =
Some le ->
forall j vargs'
t',
list_forall2 (
val_related j)
vargs'
vargs ->
tenv_related j t'
t->
exists le',
bind_parameter_temps p vargs'
t' =
Some le' /\
tenv_related j le'
le.
Proof.
induction p;
intros.
inv H.
inv_eq.
inv H0.
Esimpl;
eauto.
simpl in *.
destruct a.
inv_eq.
inv H0.
exploit IHp;
eauto.
eapply tenv_related_setid;
eauto.
Qed.
Lemma env_related_empty_env:
forall j,
env_related j empty_env empty_env.
Proof.
Lemma tenv_related_temps:
forall j t,
tenv_related j (
create_undef_temps t) (
create_undef_temps t).
Proof.
Lemma function_entry2_related:
forall fm f vargs e le fm' (
NOREP':
norep (
Mem.freelist fm)),
ClightLang.function_entry2 sge f vargs fm e le fm'->
forall vargs'
m,
list_forall2 (
val_related (
j'
fm))
vargs'
vargs->
mem_related j bound (
fl fm) (
strip fm)
m ->
exists e'
m'
le',
Clight_local.function_entry2 tge f vargs'
m e'
le'
m' /\
env_related (
j'
fm)
e'
e /\
tenv_related (
j'
fm)
le'
le /\
mem_related j bound (
fl fm) (
strip fm')
m'.
Proof.
Lemma function_entry2_fp_related:
forall fm f vargs e fp (
NOREP':
norep (
Mem.freelist fm))(
NOOVERLAP':
no_overlap (
Mem.freelist fm) (
fun b=>
Plt b bound)),
ClightLang.function_entry2_fp sge f vargs fm e fp->
forall e'
vargs'
m,
list_forall2 (
val_related (
j'
fm))
vargs'
vargs->
mem_related j bound (
fl fm) (
strip fm)
m ->
exists fp',
Clight_local.function_entry2_fp tge f vargs'
m e'
fp' /\
FPlocalize (
j'
fm)
fp fp'.
Proof.
End EXPR.
Inductive match_cont (
j:
Bset.inj):
cont->
cont->
Prop:=
|
match_stop:
match_cont j Kstop Kstop
|
match_seq:
forall k1 k1'
s,
match_cont j k1 k1'->
match_cont j (
Kseq s k1)(
Kseq s k1')
|
match_loop1:
forall k k'
s1 s2,
match_cont j k k'->
match_cont j (
Kloop1 s1 s2 k)(
Kloop1 s1 s2 k')
|
match_loop2:
forall k k'
s1 s2,
match_cont j k k'->
match_cont j (
Kloop2 s1 s2 k)(
Kloop2 s1 s2 k')
|
match_switch:
forall k k',
match_cont j k k'->
match_cont j (
Kswitch k)(
Kswitch k')
|
match_call:
forall id f v v'
e e'
k k',
match_cont j k k'->
env_related j v v'->
tenv_related j e e'->
match_cont j (
Kcall id f v e k)(
Kcall id f v'
e'
k').
Lemma find_label_match_cont_case1:
forall j s t k k',
match_cont j k k'->
find_label s t k' =
None ->
find_label s t k=
None
with find_label_ls_match_cont_case1:
forall j s t k k',
match_cont j k k'->
find_label_ls s t k' =
None ->
find_label_ls s t k =
None.
Proof.
induction t;intros;auto.
all : simpl in *;ex_match.
all : try (eapply IHt1 in Hx;eauto;try econstructor;eauto;eapply IHt2 in H0;try econstructor;eauto;simpl;rewrite Hx;auto;fail).
eapply find_label_ls_match_cont_case1;eauto. constructor;eauto.
eapply IHt;eauto.
induction t;intros;auto.
all : simpl in *;ex_match.
eapply find_label_match_cont_case1 in Hx;eauto;try econstructor;eauto.
rewrite Hx;eauto.
Qed.
Lemma find_label_match_cont_case2:
forall t j s k k' ,
match_cont j k k'->
match find_label s t k with
|
None =>
find_label s t k' =
None
|
Some (
s2,
k2) =>
exists k3,
find_label s t k' =
Some (
s2,
k3) /\
match_cont j k2 k3
end
with find_label_ls_match_cont_case2:
forall t j s k k' ,
match_cont j k k'->
match find_label_ls s t k with
|
None =>
find_label_ls s t k' =
None
|
Some (
s2,
k2) =>
exists k3,
find_label_ls s t k' =
Some (
s2,
k3) /\
match_cont j k2 k3
end.
Proof.
{
intros t;
case_eq t;
intros.
all:
simpl in *;
eauto.
{
assert(
match_cont j (
Kseq s0 k)(
Kseq s0 k')).
constructor;
auto.
eapply find_label_match_cont_case2 with(
s:=
s1)(
t:=
s)
in H1 as ?.
destruct (
find_label).
destruct p.
Hsimpl.
rewrite H2.
Esimpl;
eauto.
eapply find_label_match_cont_case2 with(
s:=
s1)(
t:=
s0)
in H0.
destruct (
find_label s1 s0 k).
destruct p;
Hsimpl.
rewrite H2.
Esimpl;
eauto.
rewrite H2.
auto.
}
{
eapply find_label_match_cont_case2 with(
s:=
s1)(
t:=
s)
in H0 as ?.
destruct find_label.
destruct p.
Hsimpl.
rewrite H1.
Esimpl;
eauto.
rewrite H1.
eapply find_label_match_cont_case2;
eauto.
}
{
assert(
match_cont j (
Kloop1 s s0 k)(
Kloop1 s s0 k')).
econstructor;
auto.
eapply find_label_match_cont_case2 with(
s:=
s1)(
t:=
s)
in H1 as ?.
destruct (
find_label).
destruct p.
Hsimpl.
rewrite H2.
Esimpl;
eauto.
rewrite H2.
eapply find_label_match_cont_case2.
econstructor;
eauto.
}
{
eapply find_label_ls_match_cont_case2;
eauto.
econstructor;
eauto.
}
{
destruct ident_eq.
{
Esimpl;
eauto.
}
{
eapply find_label_match_cont_case2;
eauto.
}
}
}
{
intros t;
case_eq t;
intros.
all:
simpl in *;
eauto.
destruct find_label eqn:?.
destruct p.
assert(
match_cont j (
Kseq (
seq_of_labeled_statement l)
k)(
Kseq (
seq_of_labeled_statement l)
k')).
econstructor;
eauto.
eapply find_label_match_cont_case2 in H1;
eauto.
rewrite Heqo0 in H1.
Hsimpl.
rewrite H1.
Esimpl;
eauto.
assert(
match_cont j (
Kseq (
seq_of_labeled_statement l)
k)(
Kseq (
seq_of_labeled_statement l)
k')).
econstructor;
eauto.
eapply find_label_match_cont_case2 in H1;
eauto.
rewrite Heqo0 in H1.
rewrite H1.
eapply find_label_ls_match_cont_case2;
eauto.
}
Qed.
:
forall k k'
j,
match_cont j k k'->
match_cont j (
call_cont k)(
call_cont k').
Proof.
induction k;intros;simpl.
inv H;constructor.
inv H. eapply IHk in H3. eauto.
inv H. eapply IHk in H4;eauto.
inv H. eapply IHk in H4;eauto.
inv H. eapply IHk in H1;eauto.
inv H. constructor;auto.
Qed.
Inductive match_core (
j:
Bset.inj) :
core ->
core ->
Prop :=
|
match_state_intro:
forall f s k1 k2 e1 e2 te1 te2,
match_cont j k1 k2 ->
env_related j e1 e2->
tenv_related j te1 te2->
match_core j (
Core_State f s k1 e1 te1)
(
Core_State f s k2 e2 te2)
|
match_state_call:
forall fd args1 args2 k1 k2,
match_cont j k1 k2 ->
list_forall2 (
val_related j)
args1 args2 ->
match_core j (
Core_Callstate fd args1 k1)
(
Core_Callstate fd args2 k2)
|
match_state_return:
forall res1 res2 k1 k2,
match_cont j k1 k2 ->
val_related j res1 res2 ->
match_core j (
Core_Returnstate res1 k1)
(
Core_Returnstate res2 k2).
Lemma freelist_fleq:
forall l m m',
Mem.free_list m l =
Some m'->
Mem.freelist m' =
Mem.freelist m.
Proof.
induction l;
intros;
simpl in *;
inv_eq;
eauto.
apply mem_free_fleq in Heqo.
apply IHl in H1.
congruence.
Qed.
Theorem clight_localize:
LangLocalize clight_comp_unit wdcu Clight_IS_2 Clight_IS_2_local.
Proof.
constructor;
simpl in *.
intros cu WDCU ge G INITGE.
pose proof INITGE as GEBOUND.
rewrite init_genv_iff in GEBOUND.
destruct GEBOUND as [
_ [
_ _ _ _ _ _ _ _ GEBOUND]].
remember (
Genv.genv_next ge)
as bound eqn:
HBOUND.
remember (
ge_extend (
Genv.globalenv (
mkprogram (
cu_defs cu) (
cu_public cu) 1%
positive))
bound GEBOUND)
as ge_local eqn:
HGE.
assert (
INITGE_local:
init_genv cu ge_local {|
genv_genv:=
ge_local;
genv_cenv:=
cu_comp_env cu|}).
{
split; [
auto|
econstructor;
eauto]. }
remember {|
genv_genv:=
ge_local;
genv_cenv:=
cu_comp_env cu|}
as ge_real eqn:
HGE2.
rewrite init_genv_iff in INITGE.
destruct INITGE as [
X INITGE].
subst G.
pose proof INITGE as INITG.
destruct INITGE as [
j DOM INJECTIVE PUBLICEQ SYMBREL DEFSDOM DEFSRANGE DEFSREL _].
exists j,
ge_local,
ge_real.
assert (
GEMATCH:
ge_match_strict j ge ge_local).
{
constructor;
try (
subst;
auto;
fail).
intros.
apply DEFSREL in H.
rewrite <-
H.
subst ge_local;
unfold ge_extend in H;
simpl.
match goal with |-
option_rel _ ?
x ?
x =>
destruct x eqn:?
end.
constructor.
destruct g;
constructor.
destruct v;
constructor.
constructor.
rewrite PUBLICEQ.
subst ge_local;
unfold ge_extend;
simpl.
tauto. }
exists (
fun jfull fl c'
m'
c m =>
exists fm',
strip fm' =
m' /\ (
FMemory.Mem.freelist fm' =
fl) /\
inject_incr (
Bset.inj_to_meminj j) (
Bset.inj_to_meminj jfull) /\
Bset.inject jfull (
fun b =>
Plt b bound) (
fun b =>
Plt b bound) /\
let cj :=
construct_inj jfull bound fl in
match_core cj c c' /\
mem_related jfull bound fl m'
m /\
norep fl /\
no_overlap fl (
fun b =>
Plt b bound)).
do 3 (
split;
auto).
subst.
unfold ge_extend,
Genv.find_def.
simpl.
eauto.
intros jfull INCRJ INJECT.
pose proof GEMATCH as GEMATCH'.
eapply ge_match_strict_incr in GEMATCH;
try exact INCRJ. 2:
inv INJECT;
inv inj_weak;
auto.
constructor;
simpl in *.
ge match & inj wd
split;
auto.
rewrite <-
HBOUND.
auto.
norep freelist
intros.
destruct H.
tauto.
no overlap
intros.
destruct H.
rewrite <-
HBOUND.
tauto.
memrel
intros.
destruct H.
rewrite <-
HBOUND.
tauto.
init
{
intros.
exploit G_args_exists_args_related'.
eauto.
subst ge_local;
simpl in *.
rewrite <-
HBOUND.
eauto.
intros [
args_local INJARGS].
exists args_local.
unfold init_core,
ClightLang.init_core,
type_of_fundef in *.
destruct (
Genv.find_symbol ge id)
eqn:
FINDSYMB;[|
discriminate].
destruct (
Genv.find_funct_ptr ge b)
eqn:
FINDDEF;[|
discriminate].
exploit (
SYMBREL).
instantiate (1:=
id).
rewrite FINDSYMB.
intro.
inv H1.
symmetry in H2.
unfold Genv.find_symbol in H2 |- * .
simpl.
rewrite H2.
clear H2.
exploit DEFSREL.
exact H5.
unfold Genv.find_funct_ptr,
Genv.find_def in *.
destruct ((
Genv.genv_defs ge)!
b)
eqn:
FINDDEF';
try discriminate.
intro.
simpl.
rewrite H1.
clear H1.
rewrite FINDDEF.
destruct g; [|
discriminate].
inversion FINDDEF;
subst f0;
clear FINDDEF.
destruct f; [|
discriminate].
destruct (
type_of_function f)
eqn:
TYPF;
try discriminate.
destruct (
val_casted_list_func args t &&
tys_nonvoid t &&
vals_defined args &&
zlt (4 * (2 *
Zlength args))
Int.max_unsigned)
eqn:
WDARGS;
try discriminate.
assert(
val_casted_list_func args_local t &&
tys_nonvoid t &&
vals_defined args_local &&
zlt (4 * (2 *
Zlength args_local))
Int.max_unsigned =
true).
{
generalize t INJARGS WDARGS.
clear.
intros until 1.
intro.
apply andb_true_iff in WDARGS.
destruct WDARGS.
apply andb_true_iff in H.
destruct H.
apply andb_true_iff in H as [].
repeat (
apply andb_true_iff;
split;
auto).
*)
clear H1 H0 H2.
revert t H .
induction INJARGS;
intros.
destruct t.
auto.
inversion H.
destruct t;
simpl in *;
auto.
apply andb_true_iff in H0.
destruct H0.
apply andb_true_iff;
split;
auto.
inv H;
destruct t;
auto.
*)
clear H H0.
induction INJARGS;
auto.
simpl.
inv H;
auto.
*)
apply list_forall2_length in INJARGS.
rewrite Zlength_correct in H0 |- * .
rewrite INJARGS.
auto.
}
pose proof H1 as H2.
simpl in H2.
rewrite H2.
clear H2.
Esimpl.
apply list_forall2_imply with (
val_related jfull);
auto.
intros.
apply val_related_val_inject_strict;
auto.
eauto.
intros m fl INITMEM NOREP NOOVERLAP RC.
exploit lmem_construction;
eauto.
intros [
lm [
INITMEM_local MEMREL]].
exists lm.
unfold init_mem.
split.
auto.
destruct NOREP as [
NOREP].
assert (
VALIDWD:
forall n b,
get_block fl n =
b ->
In b (
GMem.validblocks m) <-> (
n < 0)%
nat).
{
intros.
split;
intro C; [|
inversion C].
exfalso.
eapply NOOVERLAP;
eauto. }
repeat (
split;
auto).
eexists (
FMemory.Mem.mkmem
(
GMem.mem_contents m) (
GMem.mem_access m) (
GMem.validblocks m)
fl 0
NOREP VALIDWD
(
GMem.access_max m) (
GMem.invalid_noaccess m) (
GMem.contents_default m)).
unfold strip.
simpl.
split.
destruct m;
auto.
repeat (
split;
auto).
match core *)
inv H0.
constructor.
unfold construct_inj.
constructor.
eapply list_forall2_imply.
eauto.
intros.
apply val_related_incr with jfull;
auto.
apply construct_inj_incr;
auto.
eapply Bset.inj_dom'.
inv INJECT;
eauto.
apply bset_eq_no_overlap with (
valid_block_bset m);
auto.
intro.
rewrite <-
init_mem_valid_block;
eauto.
tauto.
}
step
{
set (
ge1:= (
Genv.globalenv {|
AST.prog_defs :=
cu_defs cu;
AST.prog_public :=
cu_public cu;
AST.prog_main := 1%
positive |}))
in *.
intros fl c lc m lm lfp lc'
lm' [
fm [
STRIP [
FL [
_ [
_ [
MS [
MEMREL [
NOREP NOOVERLAP]]]]]]]]
STEP FPG.
set (
sge:= {|
genv_genv :=
ge;
genv_cenv :=
cu_comp_env cu |} )
in *.
set (
tge:= {|
genv_genv :=
ge_local;
genv_cenv :=
cu_comp_env cu |} )
in *.
assert(
GEMATCH0:
ge_match_strict jfull sge tge).
auto.
rewrite HGE in INJECT.
simpl in INJECT.
assert(
FINDFEQ:
forall b b'
f,
construct_inj jfull bound fl b' =
Some b->
(
Genv.genv_defs ge)!
b =
Some f->
(
Genv.genv_defs ge1)!
b' =
Some f).
{
intros.
apply DEFSRANGE in H0 as ?.
Hsimpl.
unfold construct_inj in H.
destruct plt.
exploit INCRJ;
unfold Bset.inj_to_meminj.
rewrite H1.
eauto.
intros.
destruct (
jfull x)
eqn:?;
inv H2.
inv INJECT.
inv inj_weak.
eapply inj_injective in H;
try apply Heqo;
subst x.
eapply DEFSREL in H1;
eauto.
congruence.
{
inversion H.
apply NOOVERLAP in H3.
unfold Bset.belongsto in H3.
apply Genv.genv_defs_range in H0.
rewrite HBOUND in H3.
contradiction.
}
}
Ltac triv:=
Esimpl;
eauto with fplocalize;
try econstructor;
eauto;
try econstructor;
eauto.
inv MS;
inv STEP.
all:
match goal with
|
H:
embed (
strip ?
fm) (
Mem.freelist ?
fm) ?
m |-
_ =>
apply embed_eq in H;
subst fm
end.
{
pose proof H3 as STEPBK.
inv H3.
{
eapply eval_lvalue_localize in H8 as ?;
eauto.
Hsimpl.
eapply eval_expr_localize in H9 as ?;
eauto.
Hsimpl.
eapply sem_cast_related in H10 as ?;
eauto;
unfold bound,
fl;
eauto.
Hsimpl.
eapply assign_loc_related with(
tge:=
tge)
in H11 as ?;
eauto.
Hsimpl.
eapply eval_lvalue_fp_localize in H12 as ?;
eauto.
Hsimpl.
eapply eval_expr_fp_localize in H17 as ?;
eauto.
Hsimpl.
eapply sem_cast_fp_related in H18 as ?;
eauto;
unfold bound,
fl;
eauto.
Hsimpl.
eapply assign_loc_fp_related with(
v':=
x2)
in H19 as ?;
eauto.
Hsimpl.
triv.
inv H11.
eapply mem_storev_fleq in H27;
eauto.
}
{
eapply eval_expr_localize in H12 as ?;
eauto.
Hsimpl.
eapply eval_expr_fp_localize in H13 as ?;
eauto.
Hsimpl.
triv.
eapply tenv_related_setid;
eauto.
}
{
eapply eval_expr_localize in H9 as ?;
eauto;
Hsimpl.
eapply eval_exprlist_localize in H10 as ?;
eauto;
Hsimpl.
eapply eval_expr_fp_localize in H17 as ?;
eauto;
Hsimpl.
eapply eval_exprlist_fp_localize in H18 as ?;
eauto;
Hsimpl.
triv.
unfold Genv.find_funct in *.
inv H3;
auto.
inv_eq.
unfold Genv.find_funct_ptr,
Genv.find_def in *.
unfold ge_extend;
simpl.
inv_eq.
exploit FINDFEQ;
eauto.
intro R;
rewrite R;
auto.
}
{
triv.
}
{
inv H;
triv.
}
{
inv H;
triv.
}
{
inv H;
triv.
}
{
eapply eval_expr_localize in H8 as ?;
eauto;
Hsimpl.
eapply bool_val_related in H13 as ?;
eauto;
Hsimpl;
unfold bound,
fl;
eauto.
eapply eval_expr_fp_localize in H14 as ?;
eauto;
Hsimpl.
eapply bool_val_fp_related in H15 as ?;
unfold bound,
fl;
eauto;
eauto;
Hsimpl.
triv.
}
{
triv.
}
{
inv H;
triv.
}
{
inv H.
Esimpl;
eauto with fplocalize.
eapply Clight_local.step_break_loop1;
eauto with fplocalize.
econstructor;
eauto.
}
{
inv H.
triv.
}
{
inv H.
triv.
}
{
eapply freelist_related in H12 as ?;
eauto.
Hsimpl.
Esimpl;
eauto with fplocalize.
econstructor;
eauto.
exploit freelist_fp_related;
eauto.
eapply freelist_fleq;
eauto.
econstructor;
eauto.
apply call_cont_match;
auto.
}
{
eapply eval_expr_localize in H8 as ?;
eauto;
Hsimpl.
eapply sem_cast_related in H9 as ?;
eauto;
unfold bound,
fl;
eauto;
Hsimpl.
eapply freelist_related in H10 as ?;
eauto;
Hsimpl.
eapply eval_expr_fp_localize in H15 as ?;
eauto;
Hsimpl.
eapply sem_cast_fp_related in H16 as ?;
eauto;
unfold bound,
fl;
eauto;
Hsimpl.
exploit freelist_fp_related;
eauto;
intro.
triv.
eapply freelist_fleq;
eauto.
apply call_cont_match;
auto.
}
{
eapply freelist_related in H13 as ?;
eauto;
Hsimpl.
exploit freelist_fp_related;
eauto;
intro.
triv.
inv H;
inv H12;
constructor.
eapply freelist_fleq;
eauto.
}
{
eapply eval_expr_localize in H12 as ?;
eauto;
Hsimpl.
eapply eval_expr_fp_localize in H13 as ?;
eauto;
Hsimpl.
triv.
inv H3;
simpl in *;
inv_eq;
auto.
}
{
inv H.
triv.
}
{
inv H.
Esimpl;
eauto with fplocalize.
eapply step_continue_switch;
eauto.
econstructor;
eauto.
}
{
triv.
}
{
exploit call_cont_match;
eauto.
intro.
exploit find_label_match_cont_case2;
eauto.
rewrite H12.
intro.
destruct (
find_label lbl (
fn_body f)(
call_cont k1))
eqn:?;
try discriminate.
destruct p as (
s4,
k4).
Hsimpl.
inv H3.
triv.
}
}
{
inv H2.
assert(
genv_cenv sge =
genv_cenv tge).
unfold sge,
tge;
auto.
eapply function_entry2_related in H9 as ?;
eauto.
Hsimpl.
eapply function_entry2_fp_related with(
e':=
x)
in H10 as ?;
eauto.
Hsimpl.
Esimpl;
eauto with fplocalize.
econstructor;
eauto.
inv H9.
eapply alloc_variables_fleq in H13;
eauto.
econstructor;
eauto.
}
{
inv H2.
inv H.
triv.
unfold set_opttemp.
destruct optid eqn:?.
eapply tenv_related_setid;
eauto.
auto.
}
}
{
intros fl c lc m lm f sg args_local [
fm [
STRIP [
FL [
_ [
_ [
MS [
MEMREL [
NOREP NOOVERLAP]]]]]]]]
ATEXT GARGS.
unfold ClightLang.at_external,
at_external in *.
inv MS;
try discriminate.
ef
destruct fd;
try discriminate.
destruct e;
try discriminate.
destruct (
vals_defined args2)
eqn:?;
try discriminate.
assert(
vals_defined args1=
true).
{
revert Heqb H0.
clear.
induction 2;
auto.
simpl in *.
assert(
vals_defined bl =
true).
destruct b1;
try discriminate;
auto.
specialize (
IHlist_forall2 H1).
rewrite IHlist_forall2.
inv H;
try discriminate;
auto.
}
rewrite H1.
destruct (
ClightLang.invert_symbol_from_string _ name)
eqn:
NAME;
try discriminate.
enough(
invert_symbol_from_string
{|
genv_genv :=
ge_extend
(
Genv.globalenv
{|
AST.prog_defs :=
cu_defs cu;
AST.prog_public :=
cu_public cu;
AST.prog_main := 1%
positive |}) (
Genv.genv_next ge)
GEBOUND;
genv_cenv :=
cu_comp_env cu |}
name =
Some i).
rewrite H2.
destruct peq;
try discriminate.
destruct peq;
try discriminate.
simpl in *.
inv ATEXT.
Esimpl;
eauto.
unfold args_related.
{
generalize args_local args1 H0 GARGS NOOVERLAP;
clear.
induction args_local;
intros;
inv H0;
inv GARGS;
constructor;
auto.
inv H3;
econstructor.
unfold Bset.inj_to_meminj,
construct_inj in *.
destruct plt;
try contradiction.
rewrite H.
eauto.
inv H.
exfalso.
eapply NOOVERLAP;
eauto.
rewrite Ptrofs.add_zero.
auto. }
clear GARGS args1 k1 k2 H H0 H1.
set (
ggee:= (
Genv.globalenv (
mkprogram (
cu_defs cu) (
cu_public cu) 1%
positive)))
in *.
set (
ge_local:= (
ge_extend ggee (
Genv.genv_next ge)
GEBOUND))
in *.
unfold invert_symbol_from_string,
ClightLang.invert_symbol_from_string in *.
simpl in *.
destruct (
ClightLang.invert_block_from_string)
eqn:?;
inv NAME.
apply Genv.invert_find_symbol in H0 as ?.
destruct peq;
try discriminate.
destruct peq;
try discriminate.
simpl in *.
inv ATEXT.
specialize (
SYMBREL f)
as R.
rewrite H in R.
inv R.
symmetry in H1.
apply Genv.find_invert_symbol in H1 as ?.
Lemma ge_extend_invert_symbol_eq:
forall F V ge a b x,
Genv.invert_symbol ge x= @
Genv.invert_symbol F V (
ge_extend ge a b)
x.
Proof.
Lemma ge_extend_invert_block_from_string_eq:
forall ge a b x,
invert_block_from_string ge x=
invert_block_from_string (
ge_extend ge a b)
x.
Proof.
unfold ge_local;
rewrite<-
ge_extend_invert_block_from_string_eq.
enough(
invert_block_from_string ggee name =
Some b0).
rewrite H3,<-
ge_extend_invert_symbol_eq;
try congruence.
pose proof invert_block_from_string_eq.
exploit H3;
eauto.
eapply nodup_ef_ge_norep_ef_name;
eauto.
inv WDCU.
eapply nodup_gd_ident_exists;
eauto.
instantiate(1:=
name).
intro.
rewrite Heqo in H5.
inv H5.
Hsimpl.
unfold Genv.find_symbol in *.
specialize (
SYMBREL x)
as ?.
rewrite H5,
H6 in H8.
inv H8.
f_equal.
eapply INJECTIVE;
eauto.
}
{
intros fl c lc m lm ores lc'
lores [
fm [
STRIP [
FL [
_ [
_ [
MS [
MEMREL [
NOREP NOOVERLAP]]]]]]]]
RESREL AFTEXT.
unfold ClightLang.after_external,
after_external in *.
inv MS;
try discriminate.
ef
destruct fd;
try discriminate.
destruct e;
try discriminate.
destruct lores,
ores;
simpl in *;
try contradiction.
{
destruct (
sig_res sg)
as [
ty|];
[
destruct (
val_has_type_func v ty)
eqn:
TYPE, (
val_has_type_func v0 ty)
eqn:
TYPE'
|];
try discriminate.
eexists.
split.
eauto.
exists fm.
repeat (
split;
auto).
inv AFTEXT.
constructor;
auto.
inv RESREL;
auto.
unfold Bset.inj_to_meminj in H1.
ex_match.
inv H1.
rewrite Ptrofs.add_zero.
econstructor;
eauto.
eapply mem_related_inj_construct_inj;
eauto.
exfalso.
inv RESREL;
unfold val_has_type_func in *;
ex_match.
}
{
destruct (
sig_res sg)
as [
ty|];
try discriminate.
eexists.
split.
eauto.
exists fm.
repeat (
split;
auto).
inv AFTEXT.
constructor;
auto.
}
}
{
intros fl c lc m lm [
fm [
STRIP [
FL [
_ [
_ [
MS [
MEMREL [
NOREP NOOVERLAP]]]]]]]]
m'
lm'
UNCHG RELY.
TODO: RELY condition too weak. unchg_freelist required
assert (
MEMREL':
mem_related jfull bound fl m'
lm').
{
subst.
auto. }
assert (
VALIDWD:
forall n b,
get_block fl n =
b ->
In b (
GMem.validblocks m') <-> (
n < (
FMemory.Mem.nextblockid fm))%
nat).
{
intros.
fold (
GMem.valid_block m'
b).
rewrite <-
GMem.unchanged_on_validity;
eauto;
simpl.
unfold GMem.valid_block.
replace (
GMem.validblocks m)
with (
Mem.validblocks fm).
apply (
FMemory.Mem.valid_wd fm);
subst;
auto.
subst m.
unfold strip.
auto.
eexists.
eauto. }
destruct fm.
unfold strip in *.
simpl in *.
subst.
exists (
FMemory.Mem.mkmem
(
GMem.mem_contents m') (
GMem.mem_access m') (
GMem.validblocks m')
fl (
nextblockid) (
freelist_wd)
VALIDWD
(
GMem.access_max m') (
GMem.invalid_noaccess m') (
GMem.contents_default m')).
destruct m'.
subst.
unfold ge_extend in *.
simpl in *.
split;
auto.
split;
auto.
split;
auto.
}
{
unfold ClightLang.halted,
halted,
Vzero;
intros fl c lc m lm lres [
fm [
STRIP [
FL [
_ [
_ [
MS [
MEMREL [
NOREP NOOVERLAP]]]]]]]]
HALT GRES.
inv MS;
try discriminate.
destruct k2 ;
try discriminate.
inv H.
inv HALT.
Esimpl;
eauto.
unfold G_arg in GRES.
inv H0;
auto;
try discriminate;
try constructor.
unfold arg_related.
destruct res2 eqn:?;
inv H1;
inv H0;
try econstructor;
eauto.
unfold Bset.belongsto in GRES.
Focus 2.
instantiate(1:=0).
rewrite Ptrofs.add_zero.
auto.
apply MEMREL in GRES as [].
assert(
construct_inj jfull (
Genv.genv_next ge)(
Mem.freelist fm)
x =
Some b).
eapply mem_related_inj_construct_inj in H;
eauto.
eapply construct_inj_injective in H2;
try apply H0;
eauto.
specialize (
H2 H0).
subst.
unfold Bset.inj_to_meminj.
rewrite H.
auto.
}
Unshelve.
apply 0.
Qed.