Module SimplLocalsproofC
Require
Import
FSets
.
Require
Import
CoqlibC
Errors
Ordered
Maps
IntegersC
Floats
.
Require
Import
AST
Linking
.
Require
Import
ValuesC
Memory
GlobalenvsC
Events
Smallstep
.
Require
Import
CtypesC
CopC
ClightC
SimplLocals
.
Require
Import
sflib
.
Require
SimMemInj
.
newly added *
Require
Export
SimplLocalsproof
.
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
AsmregsC
MatchSimModSem
.
Require
SimMemInjC
.
Require
SoundTop
.
Require
Import
CtypingC
.
Require
Import
ModSemProps
.
Set
Implicit
Arguments
.
Lemma
val_casted_list_spec
:
forall
vs
tys
,
Forall2
val_casted
vs
(
typelist_to_listtype
tys
) <->
val_casted_list
vs
tys
.
Proof.
split
;
i
.
all
:
ginduction
vs
;
destruct
tys
;
ii
;
ss
;
inv
H
;
clarify
;
econs
;
eauto
.
Qed.
Lemma
typecheck_inject
j
vs0
vs1
tys
(
TYS
:
typecheck
vs0
tys
)
(
INJ
:
Val.inject_list
j
vs0
vs1
):
<<
TYS
:
typecheck
vs1
tys
>>.
Proof.
inv
TYS
.
econs
;
eauto
.
rewrite
<-
forall2_eq
in
*.
eapply
forall2_val_casted_inject
;
eauto
.
Qed.
Lemma
typecheck_typecheck
vs
fd
(
CTYS
:
typecheck
vs
(
type_of_params
(
fn_params
fd
))):
<<
TYS
:
ValuesC.typecheck
vs
(
signature_of_function
fd
)
vs
>>.
Proof.
inv
CTYS
.
econs
;
eauto
.
-
exploit
Forall2_length
;
eauto
.
i
.
ss
.
etrans
;
eauto
.
rewrite
typelist_to_listtype_length
;
ss
.
-
ss
.
eapply
has_type_list_typify
;
eauto
.
rpapply
val_casted_has_type_list
;
eauto
.
rewrite
typlist_of_typelist_eq
;
ss
.
Qed.
Lemma
transf_function_type
f_src
f_tgt
(
TRANSL
:
transf_function
f_src
=
OK
f_tgt
):
(<<
PRMS
: (
fn_params
f_src
) = (
fn_params
f_tgt
)>>) /\
(<<
RET
: (
fn_return
f_src
) = (
fn_return
f_tgt
)>>) /\
(<<
CCONV
: (
fn_callconv
f_src
) = (
fn_callconv
f_tgt
)>>).
Proof.
unfold
transf_function
,
bind
in
*.
des_ifs
. Qed.
Section
SIMMODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variable
prog
tprog
:
Clight.program
.
Let
md_src
:
Mod.t
:= (
ClightC.module1
prog
).
Let
md_tgt
:
Mod.t
:= (
ClightC.module2
tprog
).
Hypothesis
(
INCLSRC
:
SkEnv.includes
skenv_link
md_src
.(
Mod.sk
)).
Hypothesis
(
INCLTGT
:
SkEnv.includes
skenv_link
md_tgt
.(
Mod.sk
)).
Hypothesis
(
WF
:
SkEnv.wf
skenv_link
).
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Let
ge
:=
Build_genv
(
SkEnv.revive
(
SkEnv.project
skenv_link
md_src
.(
Mod.sk
))
prog
)
prog
.(
prog_comp_env
).
Let
tge
:=
Build_genv
(
SkEnv.revive
(
SkEnv.project
skenv_link
md_tgt
.(
Mod.sk
))
tprog
)
tprog
.(
prog_comp_env
).
Definition
msp
:
ModSemPair.t
:=
ModSemPair.mk
(
md_src
skenv_link
) (
md_tgt
skenv_link
)
tt
sm_link
.
Inductive
match_states
(
sm_init
:
SimMem.t
)
(
idx
:
nat
) (
st_src0
:
Clight.state
) (
st_tgt0
:
Clight.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
SimplLocalsproof.match_states
skenv_link
skenv_link
ge
st_src0
st_tgt0
sm0
).
Theorem
make_match_genvs
:
SimSymbId.sim_skenv
(
SkEnv.project
skenv_link
md_src
.(
Mod.sk
)) (
SkEnv.project
skenv_link
md_tgt
.(
Mod.sk
)) ->
Genv.match_genvs
(
match_globdef
(
fun
(
ctx
:
AST.program
fundef
type
)
f
tf
=>
transf_fundef
f
=
OK
tf
)
eq
prog
)
ge
tge
/\
prog_comp_env
prog
=
prog_comp_env
tprog
.
Proof.
subst_locals
.
ss
.
rr
in
TRANSL
.
destruct
TRANSL
.
r
in
H
.
esplits
.
-
eapply
SimSymbId.sim_skenv_revive
;
eauto
.
-
hexploit
(
prog_comp_env_eq
prog
);
eauto
.
i
.
hexploit
(
prog_comp_env_eq
tprog
);
eauto
.
i
.
ss
.
congruence
.
Qed.
Let
SEGESRC
:
senv_genv_compat
skenv_link
ge
.
Proof
.
eapply
CSkEnv.senv_genv_compat
;
et
. Qed.
Let
SEGETGT
:
senv_genv_compat
skenv_link
tge
.
Proof
.
eapply
CSkEnv.senv_genv_compat
;
et
. Qed.
Theorem
sim_modsem
:
ModSemPair.sim
msp
.
Proof.
(* rr in TRANSL. destruct TRANSL as [TRANSL0 TRANSL1]. *)
eapply
match_states_sim
with
(
match_states
:=
match_states
)
(
match_states_at
:=
fun
_
_
=>
eq
)
(
sound_state
:=
SoundTop.sound_state
);
eauto
;
ii
;
ss
.
-
instantiate
(1:=
Nat.lt
).
apply
lt_wf
.
-
eapply
SoundTop.sound_state_local_preservation
.
-
(* init bsim *)
(* destruct sm_arg; ss. clarify. *)
destruct
args_src
,
args_tgt
;
try
(
by
inv
INITTGT
;
des
;
inv
SAFESRC
;
ss
).
inv
SIMARGS
;
ss
.
clarify
.
inv
INITTGT
.
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
eexists
.
exists
sm_arg
.
esplits
;
eauto
;
try
refl
.
+
econs
;
eauto
;
ss
;
cycle
1.
*
inv
TYP
.
inv
SAFESRC
.
folder
.
ss
.
exploit
(
Genv.find_funct_transf_partial_genv
SIMGE
);
eauto
.
intro
FINDFTGT
;
des
.
ss
.
assert
(
MGE
:
match_globalenvs
ge
(
SimMemInj.inj
sm_arg
) (
Genv.genv_next
skenv_link
)).
{
inv
SIMSKENV
.
inv
SIMSKE
.
ss
.
inv
INJECT
.
ss
.
econs
;
eauto
.
+
ii
.
ss
.
eapply
Plt_Ple_trans
. {
genext
. }
ss
.
refl
.
+
ii
.
ss
.
uge
.
des_ifs
.
eapply
Plt_Ple_trans
. {
genext
. }
ss
.
refl
.
+
ii
.
ss
.
uge
.
des_ifs
.
eapply
Plt_Ple_trans
. {
genext
. }
ss
.
refl
.
}
hexploit
fsim_external_inject_eq
;
try
apply
FINDF0
;
et
.
i
;
clarify
.
exploit
typecheck_inject
;
eauto
.
intro
TYPTGT0
;
des
.
exploit
typecheck_typecheck
;
eauto
.
intro
TYPTGT1
;
des
.
rpapply
match_call_state
;
ss
;
eauto
.
{
i
.
inv
SIMSKENV
.
inv
SIMSKE
.
ss
.
inv
INJECT
.
ss
.
econs
;
eauto
.
-
eapply
SimMemInjC.sim_skenv_symbols_inject
;
et
.
-
etrans
;
try
apply
MWF
.
ss
.
etrans
;
try
apply
MWF
.
rewrite
NBSRC
.
xomega
.
-
etrans
;
try
apply
MWF
.
ss
.
etrans
;
try
apply
MWF
.
rewrite
NBTGT
.
xomega
.
}
{
econs
;
et
. }
{
apply
MWF
. }
{
inv
TYP
.
eapply
val_casted_list_spec
;
eauto
. }
f_equal
.
{
unfold
transf_function
in
*.
unfold
bind
in
*.
des_ifs
. }
{
inv
TYPTGT1
.
rewrite
<-
TYP0
at
2.
f_equal
.
ss
.
unfold
transf_function
in
*.
unfold
bind
in
*.
des_ifs
. }
-
(* init progress *)
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
exploit
(
Genv.find_funct_match_genv
SIMGE
);
eauto
.
i
;
des
.
ss
.
clarify
.
folder
.
hexploit
(@
fsim_external_inject_eq
);
try
apply
FINDF
;
eauto
.
clear
FPTR
.
intro
FPTR
.
(* unfold transf_function, bind in *. des_ifs. *)
unfold
bind
in
*.
des_ifs
.
esplits
;
eauto
.
econs
;
eauto
.
+
eapply
typecheck_typecheck
;
et
.
exploit
transf_function_type
;
eauto
.
i
;
des
.
eapply
typecheck_inject
;
et
.
congruence
.
-
(* call wf *)
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
-
(* call fsim *)
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
inv
MATCH
;
ss
.
destruct
sm0
;
ss
.
clarify
.
inv
CALLSRC
.
inv
MATCHST
;
ss
.
folder
.
inv
MCOMPAT
;
ss
.
clear_tac
.
exploit
(
fsim_external_funct_inject
SIMGE
);
eauto
. {
ii
;
clarify
;
ss
.
des
;
ss
. }
intro
EXTTGT
.
esplits
;
eauto
;
try
refl
;
econs
;
eauto
.
+
des
.
clarify
.
esplits
;
eauto
.
(* exploit (sim_internal_funct_inject SIMGE); try apply SIG; et. *)
(* Arguments sim_internal_funct_inject [_]. *)
(* destruct SIMSKENVLINK. inv H. rr in SIMSKENV1. clarify. *)
(* exploit (sim_internal_funct_inject); try apply VAL; try apply SIG; et. *)
(* { erewrite match_globdef_eq. eapply Global_match_genvs_refl. } *)
(* { inv SIMSKENV. ss. } *)
(***************** TODO: Add as a lemma in GlobalenvsC. *******************)
inv
SIMSKENV
.
assert
(
fptr_arg
=
tv
).
{
inv
VAL
;
ss
.
des_ifs_safe
.
apply
Genv.find_funct_ptr_iff
in
SIG
.
unfold
Genv.find_def
in
*.
inv
SIMSKE
.
ss
.
inv
INJECT
;
ss
.
exploit
(
DOMAIN
b1
);
eauto
.
{
eapply
Genv.genv_defs_range
;
et
. }
i
;
clarify
.
}
clarify
.
-
(* after fsim *)
hexploit
(
SimMemInjC.skenv_inject_revive
prog
);
et
. {
apply
SIMSKENV
. }
intro
SIMSKENV0
;
des
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
inv
AFTERSRC
.
inv
SIMRET
;
ss
.
exists
(
SimMemInj.unlift
'
sm_arg
sm_ret
).
destruct
sm_ret
;
ss
.
clarify
.
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
inv
HISTORY
.
ss
.
clear_tac
.
esplits
;
eauto
;
try
refl
;
econs
;
eauto
.
+
destruct
args_src
,
args_tgt
;
try
(
by
inv
CALLSRC
;
inv
CALLTGT
;
ss
).
ss
.
clarify
.
inv
MLE0
;
ss
.
inv
MCOMPAT
.
clear_tac
.
rpapply
match_return_state
;
ss
;
eauto
;
ss
.
{
ss
.
ii
.
eapply
match_cont_incr_bounds
;
eauto
;
swap
2 4.
{
instantiate
(1:=
tge
).
ss
.
esplits
;
eauto
. }
{
eauto
with
mem
. }
{
eauto
with
mem
. }
eapply
match_cont_extcall
with
(
ge
:=
ge
) (
tge
:=
tge
);
eauto
;
try
refl
.
{
eapply
Mem.unchanged_on_implies
;
try
eassumption
.
ii
.
rr
.
esplits
;
eauto
. }
{
eapply
SimMemInj.inject_separated_frozen
;
et
. }
}
{
eapply
MWFAFTR
. }
{
eapply
typify_inject
;
et
. }
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
;
inv
MATCHST
;
ss
.
specialize
(
MCONT
VSet.empty
).
inv
MCONT
.
inv
MCOMPAT
;
ss
.
eexists
sm0
.
esplits
;
ss
;
eauto
;
try
refl
.
econs
;
eauto
.
-
left
;
i
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
inv
MATCH
.
esplits
;
eauto
.
{
apply
modsem1_receptive
. }
ii
.
hexploit
(@
step_simulation
prog
skenv_link
skenv_link
);
eauto
;
ss
.
i
;
des
.
esplits
;
eauto
.
+
left
.
eapply
spread_dplus
;
eauto
.
eapply
modsem2_determinate
;
eauto
.
+
econs
;
ss
.
Unshelve
.
all
:
ss
;
try
(
by
econs
).
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variable
prog
tprog
:
Clight.program
.
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
ClightC.module1
prog
) (
ClightC.module2
tprog
)
tt
.
Theorem
sim_mod
:
ModPair.sim
mp
.
Proof.
econs
;
ss
.
-
r
.
inv
TRANSL
.
eapply
CSk.match_program_eq
;
et
.
ii
.
destruct
f1
;
ss
.
+
clarify
.
right
.
inv
MATCH
.
monadInv
H2
.
esplits
;
eauto
.
unfold
transf_function
in
*.
des_ifs
.
monadInv
EQ
.
ss
.
+
clarify
.
left
.
esplits
;
eauto
.
-
ii
.
inv
SIMSKENVLINK
.
inv
SIMSKENV
.
eapply
sim_modsem
;
eauto
.
Qed.
End
SIMMOD
.