Require Import CoqlibC MapsC.
Require Import ASTC Integers Floats Values MemoryC Events Globalenvs Smallstep.
Require Import Locations Stacklayout Conventions Linking.
Require Export Csem Cop Ctypes Ctyping Csyntax Cexec.
Require Import Simulation Memory ValuesC LinkingC2.
Require Import Skeleton ModSem Mod sflib.
Require Import CtypesC CsemC Sem Syntax LinkingC Program SemProps.
Require Import Equality.
Require Import CtypingC.
Set Implicit Arguments.
Ltac Eq :=
match goal with
| [
H1: ?
a = ?
b,
H2: ?
a = ?
c |-
_ ] =>
rewrite H1 in H2;
inv H2;
Eq
| [
H1: ?
a m= ?
b,
H2: ?
a m= ?
c |-
_ ] =>
rewrite H1 in H2;
inv H2;
Eq
|
_ =>
idtac
end.
Fixpoint app_cont (
k0 k1:
cont) {
struct k0}:
cont :=
match k0 with
|
Kstop =>
k1
|
Kdo k =>
Kdo (
app_cont k k1)
|
Kseq s k =>
Kseq s (
app_cont k k1)
|
Kifthenelse s1 s2 k =>
Kifthenelse s1 s2 (
app_cont k k1)
|
Kwhile1 e s k =>
Kwhile1 e s (
app_cont k k1)
|
Kwhile2 e s k =>
Kwhile2 e s (
app_cont k k1)
|
Kdowhile1 e s k =>
Kdowhile1 e s (
app_cont k k1)
|
Kdowhile2 e s k =>
Kdowhile2 e s (
app_cont k k1)
|
Kfor2 e s1 s2 k =>
Kfor2 e s1 s2 (
app_cont k k1)
|
Kfor3 e s1 s2 k =>
Kfor3 e s1 s2 (
app_cont k k1)
|
Kfor4 e s1 s2 k =>
Kfor4 e s1 s2 (
app_cont k k1)
|
Kswitch1 ls k =>
Kswitch1 ls (
app_cont k k1)
|
Kswitch2 k =>
Kswitch2 (
app_cont k k1)
|
Kreturn k =>
Kreturn (
app_cont k k1)
|
Kcall f e em ty k =>
Kcall f e em ty (
app_cont k k1)
end.
Lemma app_cont_stop_right
k0:
<<
EQ:
app_cont k0 Kstop =
k0>>.
Proof.
ginduction k0; ii; ss; des; clarify; ss; r; f_equal; ss.
Qed.
Lemma app_cont_stop_left
k0:
<<
EQ:
app_cont Kstop k0 =
k0>>.
Proof.
ginduction k0; ii; ss; des; clarify; ss; r; f_equal; ss.
Qed.
Lemma app_cont_kstop_inv
k0 k1
(
APP:
app_cont k0 k1 =
Kstop):
k0 =
Kstop /\
k1 =
Kstop.
Proof.
destruct k0; ss. Qed.
Section SIM.
Variable cp_link:
Csyntax.program.
Variable cps:
list Csyntax.program.
Variable ctx:
Syntax.program.
Hypothesis FOCUS:
link_list cps =
Some cp_link.
Let prog_src :=
ctx ++ [
cp_link.(
CsemC.module)].
Let prog_tgt :=
ctx ++
map CsemC.module cps.
Variable sk_link:
Sk.t.
Let skenv_link:
SkEnv.t := (
Sk.load_skenv sk_link).
Hypothesis (
LINKSRC:
link_sk prog_src =
Some sk_link).
Notation " '
geof'
cp" := (
Build_genv (
SkEnv.revive (
SkEnv.project skenv_link cp.(
CSk.of_program signature_of_function))
cp)
cp.(
prog_comp_env))
(
at level 50,
no associativity,
only parsing).
Let ge_cp_link:
genv :=
geof cp_link.
Hypothesis WTPROGLINK:
wt_program cp_link.
Hypothesis WTPROGS:
forall cp (
IN:
In cp cps),
wt_program cp.
Hypothesis CSTYLE_EXTERN_LINK:
forall id ef tyargs ty cc,
In (
id, (
Gfun (
Ctypes.External ef tyargs ty cc)))
cp_link.(
prog_defs) ->
ef.(
ef_sig).(
sig_cstyle).
Definition is_focus (
cp:
Csyntax.program):
Prop :=
In cp cps.
Hypothesis CSTYLE_EXTERN:
forall id ef tyargs ty cc cp,
is_focus cp ->
In (
id, (
Gfun (
Ctypes.External ef tyargs ty cc)))
cp.(
prog_defs) ->
ef.(
ef_sig).(
sig_cstyle).
Lemma link_sk_match:
<<
EQ:
link_sk prog_src =
link_sk prog_tgt>>.
Proof.
Let LINKTGT:
link_sk prog_tgt =
Some sk_link.
Proof.
Let INCL_LINKED:
SkEnv.includes skenv_link (
CSk.of_program signature_of_function cp_link).
Proof.
Let INCL_FOCUS:
forall pgm,
is_focus pgm ->
SkEnv.includes skenv_link (
CSk.of_program signature_of_function pgm).
Proof.
Lemma prog_defmap_func_same_rev
pgm id func
(
FOC:
is_focus pgm)
(
DMAP: (
prog_defmap pgm) !
id =
Some (
Gfun func))
(
INTERNAL:
negb (
is_external_fd func) =
true):
(
prog_defmap cp_link) !
id =
Some (
Gfun func).
Proof.
Inductive sum_cont:
list Frame.t ->
cont ->
Prop :=
|
sum_cont_nil :
sum_cont []
Kstop
|
sum_cont_cons
_fptr _vs k0 _m
_targs _tres _cconv
(
CALL:
is_call_cont_strong k0)
tl k1
(
TL:
sum_cont tl k1)
k2
(
K:
k2 =
app_cont k0 k1)
cp
(
FOCUS:
is_focus cp)
(
K0:
exists _f _e _C _k,
k0 = (
Kcall _f _e _C _tres _k) /\ <<
WTYK:
wtype_cont (
prog_comp_env cp)
_k>>)
(
WTTGT:
wt_state cp (
geof cp) (
Csem.Callstate _fptr (
Tfunction _targs _tres _cconv)
_vs k0 _m)):
sum_cont ((
Frame.mk (
CsemC.modsem skenv_link cp)
(
Csem.Callstate _fptr (
Tfunction _targs _tres _cconv)
_vs k0 _m)) ::
tl)
k2.
Lemma sum_cont_kstop_inv
frs
(
SUM:
sum_cont frs Kstop):
frs = [].
Proof.
Inductive match_focus_state:
Csem.state ->
Csem.state ->
cont ->
Prop :=
|
reg_state_similar
f s k k0 k1 e m
(
CONT:
k =
app_cont k1 k0)
:
match_focus_state (
Csem.State f s k e m) (
Csem.State f s k1 e m)
k0
|
expr_state_similar
f ex k k0 k1 e m
(
CONT:
k =
app_cont k1 k0)
:
match_focus_state (
Csem.ExprState f ex k e m) (
Csem.ExprState f ex k1 e m)
k0
|
call_sate_similar
fptr tyf vargs k k0 k1 m
(
CONT:
k =
app_cont k1 k0)
:
match_focus_state (
Csem.Callstate fptr tyf vargs k m) (
Csem.Callstate fptr tyf vargs k1 m)
k0
|
return_sate_similar
vres k k0 k1 m
(
CONT:
k =
app_cont k1 k0)
:
match_focus_state (
Csem.Returnstate vres k m) (
Csem.Returnstate vres k1 m)
k0
|
stuck_state_similar
k0:
match_focus_state Csem.Stuckstate Csem.Stuckstate k0.
Lemma call_cont_app_cont
k k0
tl_tgt (
SUM:
sum_cont tl_tgt k0):
(
app_cont (
call_cont k)
k0) =
call_cont (
app_cont k k0).
Proof.
clear -
SUM.
assert(
CASE:
k0 =
Kstop \/
is_call_cont_strong k0).
{
inv SUM;
ss;
et.
des.
clarify.
ss.
et. }
clear SUM.
clear_tac.
des.
{
clarify.
repeat rewrite app_cont_stop_right.
ss. }
{
rr in CASE.
des_ifs.
clear_tac.
clear -
c.
ginduction k;
ii;
ss;
des;
repeat rewrite app_cont_stop_right;
ss;
clarify. }
Qed.
Definition matched_state_source (
st_tgt:
Csem.state) (
k0:
cont):
Csem.state :=
match st_tgt with
|
Csem.State f s k1 e m =>
Csem.State f s (
app_cont k1 k0)
e m
|
Csem.ExprState f ex k1 e m =>
Csem.ExprState f ex (
app_cont k1 k0)
e m
|
Csem.Callstate fptr tyf vargs k1 m =>
Csem.Callstate fptr tyf vargs (
app_cont k1 k0)
m
|
Csem.Returnstate vres k1 m =>
Csem.Returnstate vres (
app_cont k1 k0)
m
|
Csem.Stuckstate =>
Csem.Stuckstate
end.
Lemma match_focus_state_iff
st_src0 st_tgt0 k0 :
<<
MATCH:
match_focus_state st_src0 st_tgt0 k0>> <-> <<
MATCH:
st_src0 =
matched_state_source st_tgt0 k0>>.
Proof.
split; i.
- inv H; ss.
- des. clarify. r. destruct st_tgt0; ss; try (by econs; eauto).
Qed.
Same Lemmas
Lemma defmap_with_signature
(
cp:
Csyntax.program)
i g
(
DMAP: (
prog_defmap cp) !
i =
Some g) :
exists gd, (
prog_defmap (
CSk.of_program signature_of_function cp)) !
i =
Some gd.
Proof.
Lemma defmap_with_signature_internal
(
cp:
Csyntax.program)
i if_sig
(
DMAP: (
prog_defmap cp) !
i =
Some (
Gfun (
Internal if_sig))) :
exists if_sig0, (
prog_defmap (
CSk.of_program signature_of_function cp)) !
i =
Some (
Gfun (
AST.Internal if_sig0)).
Proof.
Lemma invert_symbol_lemma1
b i0 i cp
(
FOC:
is_focus cp)
(
SYMBSKENV :
Genv.invert_symbol skenv_link b =
Some i0)
(
DEFS:
defs (
CSk.of_program signature_of_function cp)
i)
(
SYMB :
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp))
b =
Some i) :
i =
i0.
Proof.
Lemma prog_defmap_same_rev
pgm id func
(
FOC:
is_focus pgm)
(
DMAP: (
prog_defmap pgm) !
id =
Some (
Gfun (
Internal func))):
(
prog_defmap cp_link) !
id =
Some (
Gfun (
Internal func)).
Proof.
Lemma prog_defmap_gvar_exists_rev
pgm id var
(
FOC:
is_focus pgm)
(
DMAP: (
prog_defmap pgm) !
id =
Some (
Gvar var)):
exists var', (
prog_defmap cp_link) !
id =
Some (
Gvar var').
Proof.
Lemma prog_defmap_exists_rev
pgm id func
(
FOC:
is_focus pgm)
(
DMAP: (
prog_defmap pgm) !
id =
Some (
Gfun func)):
exists func', (
prog_defmap cp_link) !
id =
Some (
Gfun func').
Proof.
Lemma invert_symbol_lemma2
b i0 i
(
SYMBSKENV :
Genv.invert_symbol skenv_link b =
Some i0)
(
DEFS:
defs (
CSk.of_program signature_of_function cp_link)
i)
(
SYMB :
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
b =
Some i):
i =
i0.
Proof.
Lemma internals_linking
cp i
(
FOC:
is_focus cp)
(
INTERNALS :
internals (
CSk.of_program signature_of_function cp)
i =
true):
internals (
CSk.of_program signature_of_function cp_link)
i =
true.
Proof.
Lemma prog_find_defs_same_rev2
cp b func
(
FOC:
is_focus cp)
(
INTERNAL:
negb (
is_external_fd (
fundef_of_fundef func)) =
true)
(
FIND:
Genv.find_def (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp))
cp)
b =
Some (
Gfun func)):
Genv.find_def (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
cp_link)
b =
Some (
Gfun func).
Proof.
Lemma prog_find_defs_same_rev
cp b if_sig
(
FOC:
is_focus cp)
(
FIND:
Genv.find_def (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp))
cp)
b =
Some (
Gfun (
Internal if_sig))) :
Genv.find_def (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
cp_link)
b =
Some (
Gfun (
Internal if_sig)).
Proof.
Lemma field_offset_same
cp f0 co delta
(
FOC :
linkorder_program cp cp_link)
(
EXTENDS :
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
COMPLETE :
complete_members (
prog_comp_env cp) (
co_members co) =
true) :
field_offset (
prog_comp_env cp)
f0 (
co_members co) =
Errors.OK delta <->
field_offset (
prog_comp_env cp_link)
f0 (
co_members co) =
Errors.OK delta.
Proof.
unfold field_offset in *.
remember 0
as n.
clear Heqn.
revert COMPLETE FOC EXTENDS.
revert cp delta f0 n.
induction (
co_members co)
as [|
mhd mtl];
try (
by ss);
i.
ss.
destruct mhd.
assert (
ALIGN: (
align n (
alignof (
prog_comp_env cp)
t)) = (
align n (
alignof (
prog_comp_env cp_link)
t))).
{
clear -
COMPLETE EXTENDS.
revert t n cp cp_link COMPLETE EXTENDS.
induction t;
ss;
i;
unfold align_attr;
des_ifs;
auto.
-
exploit EXTENDS;
eauto.
i.
Eq.
auto.
-
exploit EXTENDS;
eauto.
i.
Eq.
-
exploit EXTENDS;
eauto.
i.
Eq.
auto.
-
exploit EXTENDS;
eauto.
i.
Eq. }
des_ifs.
-
rewrite ALIGN.
auto.
-
rewrite ALIGN in *.
eapply andb_prop in COMPLETE.
des;
auto.
exploit IHmtl;
eauto.
intros.
erewrite H.
erewrite <-
sizeof_stable;
eauto.
Qed.
Lemma sem_add_ptr_int_same1
cp f v1 ty1 v2 ty2 ty CC k e m'
k1 k2 ty0 si v
(
WTTGT :
wt_state cp (
geof cp) (
ExprState f (
CC (
Ebinop Oadd (
Eval v1 ty1) (
Eval v2 ty2)
ty))
k e m'))
(
EXTENDS :
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
CTX :
context k1 k2 CC)
(
CLASSADD :
classify_add ty1 ty2 =
add_case_pi ty0 si):
sem_add_ptr_int (
prog_comp_env cp)
ty0 si v1 v2 =
Some v
<->
sem_add_ptr_int (
prog_comp_env cp_link)
ty0 si v1 v2 =
Some v.
Proof.
Lemma sem_add_ptr_int_same2
cp f v1 ty1 v2 ty2 ty CC k e m'
k1 k2 ty0 si v
(
WTTGT :
wt_state cp (
geof cp) (
ExprState f (
CC (
Ebinop Oadd (
Eval v1 ty1) (
Eval v2 ty2)
ty))
k e m'))
(
EXTENDS :
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
CTX :
context k1 k2 CC)
(
CLASSADD :
classify_add ty1 ty2 =
add_case_ip si ty0):
sem_add_ptr_int (
prog_comp_env cp)
ty0 si v2 v1 =
Some v
<->
sem_add_ptr_int (
prog_comp_env cp_link)
ty0 si v2 v1 =
Some v.
Proof.
Lemma sem_add_ptr_long_same1
cp f v1 ty1 v2 ty2 ty CC k e m'
k1 k2 ty0 v
(
WTTGT :
wt_state cp (
geof cp) (
ExprState f (
CC (
Ebinop Oadd (
Eval v1 ty1) (
Eval v2 ty2)
ty))
k e m'))
(
EXTENDS :
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
CTX :
context k1 k2 CC)
(
CLASSADD :
classify_add ty1 ty2 =
add_case_pl ty0):
sem_add_ptr_long (
prog_comp_env cp)
ty0 v1 v2 =
Some v
<->
sem_add_ptr_long (
prog_comp_env cp_link)
ty0 v1 v2 =
Some v.
Proof.
Lemma sem_add_ptr_long_same2
cp f v1 ty1 v2 ty2 ty CC k e m'
k1 k2 ty0 v
(
WTTGT :
wt_state cp (
geof cp) (
ExprState f (
CC (
Ebinop Oadd (
Eval v1 ty1) (
Eval v2 ty2)
ty))
k e m'))
(
EXTENDS :
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
CTX :
context k1 k2 CC)
(
CLASSADD :
classify_add ty1 ty2 =
add_case_lp ty0):
sem_add_ptr_long (
prog_comp_env cp)
ty0 v2 v1 =
Some v
<->
sem_add_ptr_long (
prog_comp_env cp_link)
ty0 v2 v1 =
Some v.
Proof.
Lemma sem_sub_same
cp f v1 ty1 v2 ty2 ty CC k e m'
k1 k2 k0 v
(
WTSRC :
wt_state cp_link ge_cp_link (
ExprState f (
CC (
Ebinop Osub (
Eval v1 ty1) (
Eval v2 ty2)
ty)) (
app_cont k k0)
e m'))
(
WTTGT :
wt_state cp (
geof cp) (
ExprState f (
CC (
Ebinop Osub (
Eval v1 ty1) (
Eval v2 ty2)
ty))
k e m'))
(
EXTENDS :
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
CTX :
context k1 k2 CC):
sem_sub (
prog_comp_env cp)
v1 ty1 v2 ty2 m' =
Some v
<->
sem_sub (
prog_comp_env cp_link)
v1 ty1 v2 ty2 m' =
Some v.
Proof.
exploit types_of_context1;
eauto.
intros [
tys [
A B]].
unfold sem_sub.
inv WTTGT;
inv WTSRC;
ss.
destruct (
classify_sub ty1 ty2)
eqn:
ClASSIFY;
unfold classify_sub in *.
all:
try erewrite wt_type_sizeof_stable in *;
eauto.
-
unfold typeconv in *.
des_ifs;
ss;
clarify;
try (
by exploit (
WTYE (
Tpointer ty0 a0));
try eapply B;
ss;
auto;
i;
ss);
try (
by exploit (
WTYE (
Tarray ty0 z a0));
try eapply B;
ss;
auto;
i;
ss).
exploit (
WTYE (
Tpointer ty0 a2));
try eapply B;
ss;
auto;
i;
ss.
exploit (
WTYE (
Tarray ty0 z a2));
try eapply B;
ss;
auto;
i;
ss.
-
des_ifs;
ss;
clarify.
unfold typeconv in *.
des_ifs;
ss;
clarify;
try (
by exploit (
WTYE (
Tpointer ty0 a0));
try eapply B;
ss;
auto;
i;
ss);
try (
by exploit (
WTYE (
Tarray ty0 z0 a0));
try eapply B;
ss;
auto;
i;
ss).
exploit (
WTYE (
Tpointer ty0 a2));
try eapply B;
ss;
auto;
i;
ss.
exploit (
WTYE (
Tarray ty0 z a2));
try eapply B;
ss;
auto;
i;
ss.
exploit (
WTYE (
Tarray ty0 z a0));
try eapply B;
ss;
auto;
i;
ss.
-
des_ifs;
ss;
clarify.
unfold typeconv in *.
des_ifs;
ss;
clarify.
exploit (
WTYE (
Tpointer ty0 a2));
try eapply B;
ss;
auto;
i;
ss.
exploit (
WTYE (
Tarray ty0 z a2));
try eapply B;
ss;
auto;
i;
ss.
Qed.
Lemma sem_add_same
cp f v1 ty1 v2 ty2 ty CC k e m'
k1 k2 v
(
WTTGT :
wt_state cp (
geof cp) (
ExprState f (
CC (
Ebinop Oadd (
Eval v1 ty1) (
Eval v2 ty2)
ty))
k e m'))
(
EXTENDS :
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
CTX :
context k1 k2 CC):
sem_add (
prog_comp_env cp)
v1 ty1 v2 ty2 m' =
Some v
<->
sem_add (
prog_comp_env cp_link)
v1 ty1 v2 ty2 m' =
Some v.
Proof.
Lemma free_list_exists
cp m e m'
(
WTENV:
forall id blk ty,
e !
id =
Some (
blk,
ty) ->
wt_type (
prog_comp_env cp)
ty)
(
EXTENDS :
forall (
id :
positive) (
cmp :
composite),
(
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
FREE :
Mem.free_list m (
blocks_of_env (
geof cp_link)
e) =
Some m') :
Mem.free_list m (
blocks_of_env (
geof cp)
e) =
Some m'.
Proof.
Lemma free_list_same
cp m e m'
(
WTENV:
forall id blk ty,
e !
id =
Some (
blk,
ty) ->
wt_type (
prog_comp_env cp)
ty)
(
EXTENDS :
forall (
id :
positive) (
cmp :
composite),
(
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
FREE :
Mem.free_list m (
blocks_of_env (
geof cp)
e) =
Some m'):
Mem.free_list m (
blocks_of_env ge_cp_link e) =
Some m'.
Proof.
Lemma alignof_blockcopy_wt_stable:
forall t ce ce' (
extends:
forall id co,
ce!
id =
Some co ->
ce'!
id =
Some co),
wt_type ce t =
true ->
alignof_blockcopy ce t =
alignof_blockcopy ce'
t.
Proof.
induction t; simpl; intros; auto.
- destruct (ce!i) as [co|] eqn:E; try discriminate.
erewrite extends by eauto. auto.
- destruct (ce!i) as [co|] eqn:E; try discriminate.
erewrite extends by eauto. auto.
Qed.
Lemma alloc_variables_same
cp f m e m1
(
WT :
Forall (
fun t :
type =>
wt_type (
prog_comp_env cp)
t) (
map snd (
fn_params f ++
fn_vars f)))
(
EXTENDS:
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
ALLOC :
alloc_variables (
geof cp)
empty_env m (
fn_params f ++
fn_vars f)
e m1):
alloc_variables ge_cp_link empty_env m (
fn_params f ++
fn_vars f)
e m1.
Proof.
Lemma bind_parameters_same
cp f vargs m1 e m2
(
WT :
Forall (
fun t :
type =>
wt_type (
prog_comp_env cp)
t) (
map snd (
fn_params f ++
fn_vars f)))
(
EXTENDS:
forall id cmp, (
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
BIND :
bind_parameters skenv_link (
geof cp)
e m1 (
fn_params f)
vargs m2):
bind_parameters skenv_link ge_cp_link e m1 (
fn_params f)
vargs m2.
Proof.
Lemma preservation_alloc
cp_top m1 e l m0
(
FOCUS1 :
is_focus cp_top)
(
ALLOC :
alloc_variables ge_cp_link empty_env m0 l e m1)
(
COMP :
Forall (
fun t :
type =>
wt_type (
prog_comp_env cp_top)
t) (
map snd l)):
alloc_variables (
geof cp_top)
empty_env m0 l e m1.
Proof.
Lemma preservation_bind_param
cp_top m1 e l l'
m2 vs_arg
(
FOCUS1 :
is_focus cp_top)
(
PARAM :
bind_parameters skenv_link ge_cp_link e m1 l vs_arg m2)
(
COMP :
Forall (
fun t :
type =>
wt_type (
prog_comp_env cp_top)
t) (
map snd (
l ++
l'))):
bind_parameters skenv_link (
geof cp_top)
e m1 l vs_arg m2.
Proof.
induction PARAM.
-
econs.
-
ss.
inv COMP.
exploit IHPARAM;
eauto.
i.
econs;
eauto.
inv H0.
*
econs;
eauto.
*
econs 2;
eauto.
*
assert (
forall id co, (
prog_comp_env cp_top) !
id =
Some co -> (
prog_comp_env cp_link) !
id =
Some co).
{
i.
exploit link_list_linkorder;
eauto.
intro ORD.
r in ORD.
rewrite Forall_forall in ORD.
exploit ORD;
et.
intro ORD0.
ss.
rr in ORD0.
des_safe.
et. }
des;
econs 3;
eauto;
ss;
destruct ty;
ss;
des_ifs;
exploit H0;
eauto;
i;
rewrite Heq0 in H10;
inv H10;
eauto.
Qed.
Scheme statement_ind2 :=
Induction for statement Sort Prop
with labeled_statements_ind2 :=
Induction for labeled_statements Sort Prop.
Lemma find_label_same_None
tl_tgt k0 lbl s k
(
SUM :
sum_cont tl_tgt k0)
(
LABEL :
find_label lbl s k =
None) :
find_label lbl s (
app_cont k k0) =
None.
Proof.
Lemma find_label_same_None'
tl_tgt k0 lbl s k k'
(
SUM :
sum_cont tl_tgt k0)
(
LABEL :
find_label lbl s k =
None) :
find_label lbl s k' =
None.
Proof.
Lemma find_label_exists
tl_tgt k0 lbl s k s'
k'
k1
(
SUM :
sum_cont tl_tgt k0)
(
LABEL :
find_label lbl s k =
Some (
s',
k')) :
exists k1',
find_label lbl s k1 =
Some (
s',
k1').
Proof.
revert SUM.
revert_until s.
revert lbl k0 tl_tgt.
clear INCL_FOCUS.
eapply (
statement_ind2 (
fun s =>
forall lbl k0 tl_tgt k s'
k'
k1,
find_label lbl s k =
Some (
s',
k') ->
sum_cont tl_tgt k0 ->
exists k1',
find_label lbl s k1 =
Some (
s',
k1'))
(
fun sl =>
forall lbl k0 tl_tgt k s'
k'
k1,
sum_cont tl_tgt k0 ->
find_label_ls lbl sl k =
Some (
s',
k') ->
exists k1',
find_label_ls lbl sl k1 =
Some (
s',
k1'))
);
ss;
ii;
try (
by (
i;
des_ifs;
eauto));
try (
by (
des_ifs;
exploit H;
eauto)).
-
i.
des_ifs.
+
exploit H;
eauto.
i.
des.
rewrite H1 in Heq.
clarify.
eauto.
+
exploit find_label_same_None';
eauto.
i.
rewrite H3 in Heq.
clarify.
+
exploit find_label_same_None';
eauto.
i.
rewrite H1 in Heq0.
clarify.
+
exploit H0;
eauto.
-
i.
des_ifs.
+
exploit H;
eauto.
i.
des.
rewrite H1 in *.
clarify.
eauto.
+
exploit find_label_same_None';
eauto.
i.
rewrite H3 in Heq.
clarify.
+
exploit find_label_same_None';
eauto.
i.
rewrite H1 in Heq0.
clarify.
+
exploit H0;
eauto.
-
i.
des_ifs.
+
i.
exploit H;
eauto.
ss.
i.
des.
rewrite H2 in *.
eauto.
+
exploit find_label_same_None';
eauto;
ss.
i.
rewrite H2 in *.
clarify.
+
exploit find_label_same_None';
try eapply Heq0;
eauto;
ss.
i.
rewrite H4 in *.
clarify.
+
i.
exploit H;
eauto.
ss.
i.
des.
rewrite H2 in *.
clarify.
+
i.
exploit H1;
eauto.
ss.
i.
des.
rewrite H2 in *.
clarify.
eauto.
+
exploit find_label_same_None';
try eapply Heq2;
eauto;
ss.
i.
rewrite H4 in *.
clarify.
+
i.
exploit H;
eauto.
ss.
i.
des.
rewrite H2 in *.
clarify.
+
i.
exploit H1;
eauto.
ss.
i.
des.
rewrite H2 in *.
clarify.
+
i.
exploit H0;
eauto.
-
i.
des_ifs;
eauto.
+
exploit H;
eauto.
i.
des.
rewrite H2 in *.
clarify.
eauto.
+
exploit find_label_same_None';
eauto.
i.
rewrite H3 in *.
clarify.
+
exploit H;
eauto.
i.
des.
rewrite H2 in *.
clarify.
Qed.
Lemma find_label_same
tl_tgt k0 lbl s k s'
k'
(
SUM :
sum_cont tl_tgt k0)
(
LABEL :
find_label lbl s k =
Some (
s',
k')) :
find_label lbl s (
app_cont k k0) =
Some (
s',
app_cont k'
k0).
Proof.
Hypothesis WFSRC:
forall md :
Mod.t,
In md prog_src ->
Sk.wf md.
Hypothesis WFTGT:
forall md :
Mod.t,
In md prog_tgt ->
Sk.wf md.
Lemma lred_progress
cp f C a k3 k0 e m a'
m'
(
FOC:
is_focus cp)
(
CTX:
context LV RV C)
(
WTSRC:
wt_state cp_link ge_cp_link (
ExprState f (
C a) (
app_cont k3 k0)
e m))
(
WTTGT:
wt_state cp (
geof cp) (
ExprState f (
C a)
k3 e m))
(
EXTENDS:
forall (
id :
positive) (
cmp :
composite),
(
prog_comp_env cp) !
id =
Some cmp -> (
prog_comp_env cp_link) !
id =
Some cmp)
(
LRED:
lred ge_cp_link e a m a'
m'):
exists a1 m1,
lred (
geof cp)
e a m a1 m1.
Proof.
Lemma match_focus_state_bsim
cst_src0 cst_tgt0 cst_tgt1 k0 cp tr
(
ST:
match_focus_state cst_src0 cst_tgt0 k0)
(
ISFOC:
is_focus cp)
(
WTSRC:
wt_state cp_link (
geof cp_link)
cst_src0)
(
WTTGT:
wt_state cp (
geof cp)
cst_tgt0)
(
STEP:
Csem.step skenv_link (
geof cp)
cst_tgt0 tr cst_tgt1)
tl_tgt
(
SUM:
sum_cont tl_tgt k0):
<<
STEP:
Csem.step skenv_link (
geof cp_link)
cst_src0 tr (
matched_state_source cst_tgt1 k0)>>.
Proof.
Lemma match_focus_state_progress
cst_src0 cst_tgt0 cst_src1 k0 cp tr
(
NCALLTGT : ~
exists args,
at_external skenv_link cp cst_tgt0 args)
(
NCALLSRC : ~
exists args,
at_external skenv_link cp_link cst_src0 args)
(
NRETTGT : ~
ModSem.is_return (
modsem skenv_link cp)
cst_tgt0)
(
NRETSRC : ~
ModSem.is_return (
modsem skenv_link cp_link)
cst_src0)
(
ST:
match_focus_state cst_src0 cst_tgt0 k0)
(
ISFOC:
is_focus cp)
(
WTSRC:
wt_state cp_link (
geof cp_link)
cst_src0)
(
WTTGT:
wt_state cp (
geof cp)
cst_tgt0)
(
STEP:
Csem.step skenv_link (
geof cp_link)
cst_src0 tr cst_src1)
tl_tgt
(
SUM:
sum_cont tl_tgt k0):
(<<
STEP:
exists cst_tgt1,
Csem.step skenv_link (
geof cp)
cst_tgt0 tr cst_tgt1>>).
Proof.
assert (
FOC:
linkorder cp cp_link).
{
exploit link_list_linkorder;
eauto.
i.
rr in H.
rewrite Forall_forall in H.
exploit H;
eauto. }
pose cst_src1 as XXX.
assert(
EXTENDS:
forall id cmp (
IN: (
prog_comp_env cp) !
id =
Some cmp),
<<
IN: (
prog_comp_env cp_link) !
id =
Some cmp>>).
{
Local Transparent Linker_program.
ss.
unfold link_program in *.
des_ifs.
Local Transparent Linker_prog.
ss.
unfold linkorder_program in FOC.
inv FOC.
eauto. }
unfold NW in *.
rr in STEP.
des.
-
inv STEP;
inv ST.
+
exploit lred_progress;
eauto.
i.
des.
eexists.
left.
econs;
eauto.
+
rename C into CC.
inversion WTTGT;
subst;
ss.
exploit types_of_context1;
eauto.
intros [
tys [
A B]].
inv H;
try by (
eexists;
econs;
econs 2;
eauto;
econs;
eauto).
*
eexists;
econs;
econs 2;
eauto;
econs;
eauto.
destruct op;
ss;
eauto.
{
erewrite sem_add_same;
eauto. }
{
erewrite sem_sub_same;
eauto. }
*
eexists.
econs.
econs 2;
eauto.
econs;
eauto.
inv H2;
try (
by econs;
eauto).
econs 3;
ss;
eauto.
{
erewrite alignof_blockcopy_wt_stable;
eauto.
exploit (
WTYE);
try eapply B;
ss;
auto;
i;
ss. }
{
erewrite alignof_blockcopy_wt_stable;
eauto.
exploit (
WTYE);
try eapply B;
ss;
auto;
i;
ss. }
{
erewrite wt_type_sizeof_stable;
eauto.
inv WTTGT;
ss.
exploit (
WTYE ty1);
eauto.
eapply B.
ss.
auto. }
{
erewrite wt_type_sizeof_stable;
eauto.
inv WTTGT;
ss.
exploit (
WTYE ty1);
eauto.
eapply B.
ss.
auto. }
+
eexists.
econs.
econs 3;
eauto.
+
eexists.
econs.
econs 4;
eauto.
ii.
eapply H0.
inv H1.
*
econs 1;
eauto.
*
econs 2;
eauto.
*
inv H2.
{
econs 3;
eauto.
instantiate (1:=
m').
instantiate (1:=(
Eloc b Ptrofs.zero ty)).
econs;
eauto. }
{
ss.
econs 3;
eauto.
econs 2;
eauto.
ss.
instantiate (1 :=
b).
unfold Genv.find_symbol in *.
ss.
rewrite PTree_filter_key_spec in *.
des_ifs.
rewrite CSk.of_program_defs in *.
assert (
defs cp x)
by ss.
assert (~
defs cp_link x)
by (
ii;
clarify).
rewrite <-
defs_prog_defmap in *.
des.
exfalso.
eapply H5.
destruct gd.
-
exploit prog_defmap_exists_rev;
eauto.
i.
des.
exists (
Gfun func').
eauto.
-
exploit prog_defmap_gvar_exists_rev;
eauto.
i.
des.
exists (
Gvar var').
eauto. }
{
econs 3;
eauto.
ss.
econs 3;
eauto. }
{
exploit context_compose.
eapply H.
eauto.
i.
exploit types_of_context1;
eauto.
intros [
tys [
A B]].
inv WTTGT.
ss.
exploit (
WTYE (
Tstruct id a)).
eapply B.
ss.
auto.
i.
inv H5.
des_ifs.
econs 3;
eauto.
ss.
econs 4;
eauto;
ss.
erewrite <-
field_offset_same;
eauto.
exploit EXTENDS;
eauto.
i.
Eq.
eauto.
hexploit (
prog_comp_env_eq cp);
et.
intro X.
exploit build_composite_env_consistent;
et.
intro Y.
exploit co_consistent_complete;
et. }
{
exploit context_compose.
eapply H.
eauto.
i.
exploit types_of_context1;
eauto.
intros [
tys [
A B]].
inv WTTGT.
ss.
exploit (
WTYE (
Tunion id a)).
eapply B.
ss.
auto.
i.
inv H4.
des_ifs.
econs 3;
eauto.
ss.
econs 5;
eauto. }
*
inv H2;
try (
by (
econs 4;
eauto;
econs;
eauto)).
{
econs 4;
eauto.
econs 4;
eauto.
ss.
unfold sem_binary_operation in *.
des_ifs;
eauto.
-
exploit context_compose.
eapply H.
eapply H3.
i.
erewrite <-
sem_add_same;
eauto.
ss.
eauto.
-
exploit context_compose.
eapply H.
eapply H3.
i.
erewrite <-
sem_sub_same;
try eapply H2.
eauto.
eapply WTSRC.
eapply WTTGT.
eauto. }
{
exploit context_compose.
eapply H.
eauto.
i.
inversion WTTGT;
subst;
ss.
exploit types_of_context1;
eauto.
intros [
tys [
A B]].
inv H4;
econs 4;
eauto;
econs;
eauto.
-
econs 1;
eauto.
-
econs 2;
eauto.
-
econs 3;
eauto;
ss.
+
erewrite <-
alignof_blockcopy_wt_stable;
eauto.
exploit (
WTYE);
try eapply B;
ss;
auto;
i;
ss.
+
erewrite <-
alignof_blockcopy_wt_stable;
eauto.
exploit (
WTYE);
try eapply B;
ss;
auto;
i;
ss.
+
erewrite <-
wt_type_sizeof_stable;
eauto.
exploit (
WTYE ty1);
eauto.
eapply B.
ss.
auto.
+
erewrite <-
wt_type_sizeof_stable;
eauto.
exploit (
WTYE ty1);
eauto.
eapply B.
ss.
auto. }
*
econs 5;
eauto.
-
ss.
inversion STEP;
subst;
inv ST;
ss;
try (
by eexists;
right;
econs;
eauto);
(
try by (
destruct k3;
destruct k0;
ss;
clarify;
try (
by eexists;
right;
econs;
eauto);
inv SUM;
unfold is_call_cont_strong in CALL;
des_ifs)).
+
eexists.
right.
ss.
rpapply step_return_0;
eauto.
inv WTTGT.
exploit free_list_exists;
eauto.
+
destruct k3;
destruct k0;
ss;
clarify;
eauto;
inv SUM;
unfold is_call_cont_strong in *;
des_ifs.
*
eexists.
right.
ss.
rpapply step_return_2;
eauto.
inv WTTGT.
exploit free_list_exists;
eauto.
*
eexists.
right.
ss.
rpapply step_return_2;
eauto.
inv WTTGT.
exploit free_list_exists;
eauto.
+
eexists.
right.
ss.
eapply step_skip_call;
eauto.
*
exploit Cstrategy.is_call_cont_call_cont;
et.
intro T.
clear -
H T SUM.
unfold is_call_cont in H.
des_ifs.
ss.
destruct k3;
destruct k0;
ss.
inv SUM;
ss.
des;
clarify.
destruct k3;
ss.
destruct k3;
ss.
*
inv WTTGT;
ss.
exploit free_list_exists;
eauto.
+
clear -
H SUM.
erewrite <-
call_cont_app_cont in H;
et.
exploit find_label_exists;
eauto.
i.
des.
eexists.
right.
ss.
eapply step_goto;
et.
+
eexists.
right.
destruct (
lift_option (
Genv.find_funct (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp))
cp)
fptr))
as [[
gd TG] |
TG].
{
assert (
gd =
Internal f).
{
unfold Genv.find_funct in *.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def in *.
ss.
do 2
rewrite MapsC.PTree_filter_map_spec,
o_bind_ignore in *.
des_ifs.
destruct (
Genv.invert_symbol skenv_link b)
eqn:
SKENV;
ss.
unfold o_bind in Heq,
Heq1.
ss.
des_ifs.
destruct (
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
b)
eqn:
LINKSYMB;
ss.
destruct (
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp))
b)
eqn:
PROGSYMB;
ss.
unfold o_bind in FPTR,
TG.
ss.
assert (
i =
i0).
{
destruct ((
prog_defmap cp_link) !
i0)
eqn:
DMAP;
ss;
clarify.
assert (
defs cp_link i0)
by (
rewrite <-
defs_prog_defmap;
eauto).
exploit invert_symbol_lemma2.
eauto.
erewrite CSk.of_program_defs.
eauto.
eauto.
eauto. }
assert (
i =
i1).
{
destruct ((
prog_defmap cp) !
i1)
eqn:
DMAP;
ss;
clarify.
assert (
defs cp i1)
by (
rewrite <-
defs_prog_defmap;
eauto).
exploit invert_symbol_lemma1.
eauto.
eauto.
erewrite CSk.of_program_defs.
eauto.
eauto.
eauto. }
subst.
destruct ((
prog_defmap cp_link) !
i1)
eqn:
DMAP;
ss.
destruct ((
prog_defmap cp) !
i1)
eqn:
DMAP0;
ss.
clarify.
rewrite CSk.of_program_internals in *.
unfold internals in Heq2.
rewrite DMAP0 in Heq2.
ss.
exploit prog_defmap_func_same_rev;
eauto.
i.
Eq.
auto. }
subst.
inv WTTGT;
ss.
eapply step_internal_function;
eauto.
exploit preservation_alloc;
eauto.
exploit preservation_bind_param;
eauto. }
{
exfalso.
eapply NCALLTGT.
eexists.
econs;
eauto.
-
assert (
Genv.find_funct skenv_link fptr =
Some (
AST.Internal (
signature_of_function f))).
{
assert (
SkEnv.wf skenv_link).
{
eapply SkEnv.load_skenv_wf.
eapply link_list_preserves_wf_sk;
eauto. }
dup FPTR.
unfold Genv.find_funct in FPTR.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def in FPTR.
ss.
do 2
rewrite PTree_filter_map_spec,
o_bind_ignore in *.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def.
ss.
exploit SkEnv.project_impl_spec.
eapply INCL_LINKED.
i.
inv H3.
destruct (
Genv.invert_symbol skenv_link b)
eqn:
SKENV;
ss.
unfold o_bind in Heq.
ss.
des_ifs.
assert (
Genv.find_def (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
b =
Some (
Gfun (
AST.Internal (
signature_of_function f)))).
{
unfold Genv.find_def.
ss.
rewrite PTree_filter_map_spec,
o_bind_ignore.
des_ifs.
rewrite SKENV.
unfold o_bind.
ss.
des_ifs.
destruct ((
prog_defmap (
CSk.of_program signature_of_function cp_link)) !
i)
eqn:
DMAP;
ss.
clarify.
destruct (
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
b)
eqn:
CPLINKSYMB;
ss.
unfold o_bind in FPTR.
ss.
destruct ((
prog_defmap cp_link) !
i0)
eqn:
DMAP0;
ss.
clarify.
assert (
i =
i0).
{
assert (
defs cp_link i0)
by (
rewrite <-
defs_prog_defmap;
eauto).
exploit invert_symbol_lemma2.
eauto.
erewrite CSk.of_program_defs.
eauto.
eauto.
eauto. }
subst.
clear -
DMAP DMAP0.
unfold prog_defmap in DMAP.
ss.
unfold prog_defmap in DMAP0.
ss.
unfold skdefs_of_gdefs in DMAP.
ss.
do 2
rewrite prog_defmap_update_snd in DMAP.
rewrite DMAP0 in *.
ss. }
exploit DEFKEPT;
eauto.
i.
des.
inv LO.
inv H6.
eauto. }
esplits;
eauto.
ss.
unfold signature_of_function.
unfold signature_of_type.
ss.
f_equal.
remember (
fn_params f)
as l.
clear Heql.
clear.
induction l.
ss.
ss.
destruct a.
ss.
clarify.
rewrite H0.
ss.
-
inv WTTGT.
ss.
inv WTK;
ss.
exploit WTKS.
{
ii.
unfold fundef in *.
Eq. }
i.
des.
clarify. }
+
eexists.
right.
destruct (
lift_option (
Genv.find_funct (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp))
cp)
fptr))
as [[
gd TG] |
TG].
{
assert (
gd = (
External ef targs tres cc)).
{
unfold Genv.find_funct in *.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def in *.
ss.
do 2
rewrite MapsC.PTree_filter_map_spec,
o_bind_ignore in *.
des_ifs.
destruct (
Genv.invert_symbol skenv_link b)
eqn:
SKENV;
ss.
unfold o_bind in Heq,
Heq1.
ss.
des_ifs.
destruct (
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
b)
eqn:
LINKSYMB;
ss.
destruct (
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp))
b)
eqn:
PROGSYMB;
ss.
unfold o_bind in FPTR,
TG.
ss.
assert (
i =
i0).
{
destruct ((
prog_defmap cp_link) !
i0)
eqn:
DMAP;
ss;
clarify.
assert (
defs cp_link i0)
by (
rewrite <-
defs_prog_defmap;
eauto).
exploit invert_symbol_lemma2.
eauto.
erewrite CSk.of_program_defs.
eauto.
eauto.
eauto. }
assert (
i =
i1).
{
destruct ((
prog_defmap cp) !
i1)
eqn:
DMAP;
ss;
clarify.
assert (
defs cp i1)
by (
rewrite <-
defs_prog_defmap;
eauto).
exploit invert_symbol_lemma1.
eauto.
eauto.
erewrite CSk.of_program_defs.
eauto.
eauto.
eauto. }
subst.
destruct ((
prog_defmap cp_link) !
i1)
eqn:
DMAP;
ss.
destruct ((
prog_defmap cp) !
i1)
eqn:
DMAP0;
ss.
clarify.
rewrite CSk.of_program_internals in *.
unfold internals in Heq2.
rewrite DMAP0 in Heq2.
ss.
exploit prog_defmap_func_same_rev;
eauto.
i.
Eq.
auto. }
subst.
eapply step_external_function;
eauto. }
{
exfalso.
eapply NCALLTGT.
eexists.
dup FPTR.
unfold Genv.find_funct in FPTR.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
unfold Genv.find_def in FPTR.
ss.
do 2
rewrite PTree_filter_map_spec,
o_bind_ignore in *.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
destruct (
Genv.invert_symbol skenv_link b)
eqn:
SKENV;
ss.
unfold o_bind in Heq.
ss.
des_ifs.
destruct ((
prog_defmap (
CSk.of_program signature_of_function cp_link)) !
i)
eqn:
DMAP;
ss.
clarify.
destruct (
Genv.invert_symbol (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
b)
eqn:
CPLINKSYMB;
ss.
unfold o_bind in FPTR.
ss.
destruct ((
prog_defmap cp_link) !
i0)
eqn:
DMAP0;
ss.
clarify.
assert (
i =
i0).
{
assert (
defs cp_link i0)
by (
rewrite <-
defs_prog_defmap;
eauto).
exploit invert_symbol_lemma2.
eauto.
erewrite CSk.of_program_defs.
eauto.
eauto.
eauto. }
subst.
econs;
eauto.
-
assert (
Genv.find_funct skenv_link (
Vptr b Ptrofs.zero) =
Some (
AST.External ef)).
{
assert (
SkEnv.wf skenv_link).
{
eapply SkEnv.load_skenv_wf.
eapply link_list_preserves_wf_sk;
eauto. }
unfold Genv.find_def.
ss.
exploit SkEnv.project_impl_spec.
eapply INCL_LINKED.
i.
inv H1.
assert (
Genv.find_def (
SkEnv.project skenv_link (
CSk.of_program signature_of_function cp_link))
b =
Some (
Gfun (
AST.External ef))).
{
unfold Genv.find_def.
ss.
rewrite PTree_filter_map_spec,
o_bind_ignore.
des_ifs.
rewrite SKENV.
unfold o_bind.
ss.
des_ifs.
clear -
DMAP DMAP0.
rewrite DMAP.
ss.
unfold prog_defmap in DMAP.
ss.
unfold prog_defmap in DMAP0.
ss.
unfold skdefs_of_gdefs in DMAP.
ss.
do 2
rewrite prog_defmap_update_snd in DMAP.
rewrite DMAP0 in *.
ss. }
exploit DEFKEPT;
eauto.
i.
des.
inv LO.
inv H4;
des_ifs;
rewrite Genv.find_funct_ptr_iff;
eauto. }
esplits;
eauto.
inv WTPROGLINK.
unfold prog_defmap in DMAP0.
ss.
eapply PTree_Properties.in_of_list in DMAP0.
exploit H2;
eauto.
i.
exploit CSTYLE_EXTERN_LINK;
eauto.
i.
des_ifs.
congruence.
-
inv WTTGT.
ss.
inv WTK;
ss.
exploit WTKS.
{
ii.
unfold fundef in *.
Eq. }
i.
des.
clarify. }
+
destruct k3;
destruct k0;
ss;
clarify;
try (
by eexists;
right;
econs;
eauto).
inv SUM.
unfold is_call_cont_strong in CALL.
des_ifs.
ss.
exfalso.
eapply NRETTGT.
ss.
econs.
unfold ModSem.final_frame.
ss.
Unshelve.
all:
auto.
Qed.
End SIM.