Module SimplExprproofC
Require
Import
FunInd
.
Require
Import
CoqlibC
Maps
Errors
IntegersC
.
Require
Import
ASTC
LinkingC
.
Require
Import
ValuesC
MemoryC
EventsC
GlobalenvsC
Smallstep
.
Require
Import
Ctypes
Cop
Csyntax
Csem
CstrategyC
ClightC
.
Require
Import
SimplExpr
SimplExprspec
.
newly added *
Require
Export
SimplExprproof
.
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSemSR
SimSymb
SimMem
MatchSimModSemSR
.
Require
Import
ModSemProps
.
Require
Import
CtypesC
.
Require
Import
CtypingC
.
Require
SimMemId
.
Require
SoundTop
.
Require
Import
sflib
.
Set
Implicit
Arguments
.
Section
SIMMODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variable
prog
:
Csyntax.program
.
Variable
tprog
:
Clight.program
.
Let
md_src
:
Mod.t
:= (
CstrategyC.module
prog
).
Let
md_tgt
:
Mod.t
:= (
ClightC.module1
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
:
Csem.genv
:=
Csem.Build_genv
(
SkEnv.revive
(
SkEnv.project
skenv_link
md_src
.(
Mod.sk
))
prog
)
prog
.(
prog_comp_env
).
Let
tge
:
genv
:=
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
:
Csem.state
) (
st_tgt0
:
Clight.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
SimplExprproof.match_states
tge
st_src0
st_tgt0
)
(
MWF
:
SimMem.wf
sm0
)
(
MEASURE
:
measure
st_src0
=
idx
).
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
Csyntax.fundef
type
)
f
tf
=>
tr_fundef
f
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.
Theorem
sim_modsem
:
ModSemPair.simSR
msp
.
Proof.
eapply
match_states_sim
with
(
match_states
:=
match_states
) (
match_states_at
:=
top4
) (
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
.
inv
SIMARGS
;
ss
.
clarify
.
inv
INITTGT
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
eexists
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
eauto
.
+
econs
;
eauto
;
ss
.
*
inv
TYP
.
rpapply
match_callstates
;
eauto
.
{
econs
;
eauto
. }
inv
SAFESRC
.
folder
.
inv
TYP
.
exploit
(
Genv.find_funct_match_genv
SIMGE
);
eauto
.
intro
TFPTR
;
des
.
ss
.
f_equal
;
ss
.
inv
TFPTR0
;
ss
.
inv
H0
;
ss
.
unfold
Csyntax.type_of_function
.
unfold
type_of_function
.
f_equal
;
try
congruence
.
+
des
.
inv
SAFESRC
.
ss
.
-
(* init progress *)
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
exploit
(
Genv.find_funct_match_genv
SIMGE
);
eauto
.
i
;
des
.
ss
.
clarify
.
folder
.
inv
TYP
.
inv
H0
.
esplits
;
eauto
.
econs
;
eauto
.
folder
.
inv
H3
.
ss
.
econs
;
try
rewrite
H5
;
eauto
.
-
(* call wf *)
inv
MATCH
;
ss
.
-
(* call fsim *)
inv
MATCH
;
ss
.
destruct
sm0
;
ss
.
clarify
.
inv
CALLSRC
.
inv
MATCHST
;
ss
.
folder
.
esplits
;
eauto
.
+
econs
;
eauto
.
*
ss
.
folder
.
des
.
destruct
TRANSL
as
[
TRANSL0
_
].
exploit
(
SimSymbId.sim_skenv_revive
TRANSL0
);
eauto
.
{
apply
SIMSKENV
. }
intro
GE
;
des
.
apply
(
fsim_external_funct_id
GE
);
ss
.
+
econs
;
ss
;
eauto
.
*
instantiate
(1:=
SimMemId.mk
_
_
).
ss
.
*
ss
.
+
ss
.
-
(* after fsim *)
inv
AFTERSRC
.
inv
SIMRET
;
cycle
1.
{
inv
CSTYLE
. }
ss
.
exists
sm_ret
.
destruct
sm_ret
;
ss
.
clarify
.
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
esplits
;
eauto
;
econs
;
ss
;
eauto
.
clarify
.
econs
;
eauto
.
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
;
inv
MATCHST
;
ss
.
inv
H3
.
destruct
sm0
;
ss
.
clarify
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
ss
;
eauto
.
econs
;
ss
;
eauto
.
-
left
;
i
.
esplits
;
eauto
.
{
apply
modsem_strongly_receptive
;
et
. }
inv
MATCH
.
ii
.
hexploit
(@
simulation
prog
skenv_link
skenv_link
);
eauto
.
{
inv
SIMSKENV
.
ss
. }
{
exploit
make_match_genvs
;
eauto
. {
eapply
SIMSKENV
. }
intro
T
;
des
.
esplits
;
eauto
. }
i
.
des_safe
.
esplits
;
eauto
.
+
des
.
*
left
.
eapply
spread_dplus
;
eauto
.
{
eapply
modsem1_determinate
;
eauto
. }
*
right
.
esplits
;
eauto
.
eapply
spread_dstar
;
eauto
.
{
eapply
modsem1_determinate
;
eauto
. }
+
econs
;
eauto
.
Unshelve
.
all
:
ss
;
try
(
by
econs
);
try
eapply
Mem.empty
.
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variable
prog
:
Csyntax.program
.
Variable
tprog
:
Clight.program
.
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
CstrategyC.module
prog
).(
Mod.Atomic.trans
) (
ClightC.module1
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
.
esplits
;
eauto
.
inv
H2
.
unfold
CsemC.signature_of_function
,
signature_of_function
.
f_equal
;
congruence
.
+
clarify
.
left
.
inv
MATCH
.
esplits
;
eauto
.
-
ii
.
inv
SIMSKENVLINK
.
eapply
factor_simmodsem_source
;
eauto
.
{
ii
.
ss
.
hexploit
(@
modsem_strongly_receptive
skenv_link_tgt
prog
s
);
eauto
.
intro
SR
.
inv
SR
.
exploit
ssr_traces_at
;
eauto
.
}
{
ii
.
ss
.
eapply
modsem1_receptive
;
ss
;
eauto
. }
ss
.
eapply
sim_modsem
;
eauto
.
Qed.
End
SIMMOD
.