Module CshmgenproofC
Require
Import
CoqlibC
Errors
Maps
Integers
Floats
.
Require
Import
AST
Linking
.
Require
Import
ValuesC
Events
Memory
Globalenvs
Smallstep
.
Require
Import
CtypesC
Cop
ClightC
Cminor
CsharpminorC
.
Require
Import
Cshmgen
.
Require
Import
sflib
.
newly added *
Require
Export
Cshmgenproof
.
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
AsmregsC
MatchSimModSem
.
Require
SimMemId
.
Require
SoundTop
.
Require
Import
CtypingC
.
Require
Import
ModSemProps
.
Set
Implicit
Arguments
.
Lemma
proj_sig_res_type
targs0
tres0
cconv0
:
proj_sig_res
(
signature_of_type
targs0
tres0
cconv0
) =
typ_of_type
tres0
.
Proof.
destruct
tres0
;
ss
.
Qed.
Section
SIMMODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variable
prog
:
Clight.program
.
Variable
tprog
:
Csharpminor.program
.
Let
md_src
:
Mod.t
:= (
ClightC.module2
prog
).
Let
md_tgt
:
Mod.t
:= (
CsharpminorC.module
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
:= (
SkEnv.revive
(
SkEnv.project
skenv_link
md_tgt
.(
Mod.sk
))
tprog
).
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
:
Csharpminor.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
Cshmgenproof.match_states
prog
ge
st_src0
st_tgt0
)
(
MCOMPATSRC
:
st_src0
.(
ClightC.get_mem
) =
sm0
.(
SimMem.src
))
(
MCOMPATTGT
:
st_tgt0
.(
CsharpminorC.get_mem
) =
sm0
.(
SimMem.tgt
)).
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
match_fundef
match_varinfo
prog
)
ge
tge
.
Proof.
subst_locals
.
ss
.
eapply
SimSymbId.sim_skenv_revive
;
eauto
. Qed.
Theorem
sim_modsem
:
ModSemPair.sim
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
INITTGT
.
inv
SIMARGS
;
ss
.
clarify
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
eexists
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
eauto
.
+
econs
;
eauto
;
ss
.
*
inv
TYP
.
inv
SAFESRC
.
folder
.
rpapply
match_callstate
;
eauto
.
{
econs
;
eauto
. }
{
ss
. }
inv
TYP
.
exploit
(
Genv.find_funct_match_genv
SIMGE
);
eauto
.
intro
FINDFSRC
;
des
.
inv
FINDFSRC0
.
ss
.
clarify
.
monadInv
H0
;
ss
.
f_equal
;
try
congruence
.
{
exploit
(
function_type_implies_sig
fd0
);
et
.
unfold
type_of_function
.
ss
. }
-
(* init progress *)
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
exploit
(
Genv.find_funct_match_genv
SIMGE
);
eauto
.
i
;
des
.
ss
.
clarify
.
folder
.
inv
TYP
.
inv
H0
.
ss
.
assert
(
TYEQ
: (
ClightC.signature_of_function
fd
) =
fn_sig
tf0
).
{
monadInv
H3
.
ss
. }
esplits
;
eauto
.
econs
;
swap
1 2;
ss
;
eauto
.
+
esplits
;
ss
.
unfold
ClightC.signature_of_function
in
*.
rewrite
<-
TYEQ
.
ss
.
+
ss
.
econs
;
ss
.
rewrite
<-
TYEQ
.
ss
.
+
rewrite
<-
TYEQ
.
ss
.
-
(* call wf *)
inv
MATCH
;
ss
.
destruct
sm0
;
ss
.
clarify
.
inv
CALLSRC
.
inv
MATCHST
;
ss
.
-
(* call fsim *)
inv
MATCH
;
ss
.
destruct
sm0
;
ss
.
clarify
.
inv
CALLSRC
.
inv
MATCHST
;
ss
.
folder
.
esplits
;
eauto
.
+
econs
;
eauto
.
*
folder
.
des
.
r
in
TRANSL
.
exploit
(
SimSymbId.sim_skenv_revive
TRANSL
);
eauto
.
{
apply
SIMSKENV
. }
intro
GE
.
apply
(
fsim_external_funct_id
GE
);
ss
.
*
des
.
clarify
.
esplits
;
eauto
.
+
econs
;
ss
;
eauto
.
*
instantiate
(1:=
SimMemId.mk
_
_
).
ss
.
*
ss
.
+
ss
.
-
(* after fsim *)
inv
AFTERSRC
.
inv
SIMRET
;
inv
CSTYLE
.
ss
.
exists
sm_ret
.
destruct
sm_ret
;
ss
.
clarify
.
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
esplits
;
eauto
.
+
econs
;
eauto
.
+
econs
;
ss
;
eauto
.
clarify
.
rpapply
match_returnstate
;
eauto
.
repeat
f_equal
.
rewrite
proj_sig_res_type
.
ss
.
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
;
inv
MATCHST
;
ss
.
inv
MK
;
ss
.
destruct
sm0
;
ss
.
clarify
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
ss
;
eauto
.
econs
;
ss
;
eauto
.
-
left
;
i
.
esplits
;
eauto
.
{
apply
modsem2_receptive
. }
inv
MATCH
.
ii
.
hexploit
(@
transl_step
prog
skenv_link
skenv_link
);
eauto
;
ss
.
{
apply
make_match_genvs
;
eauto
.
apply
SIMSKENV
. }
i
;
des
.
esplits
;
eauto
.
+
left
.
eapply
spread_dplus
;
eauto
.
eapply
modsem_determinate
;
eauto
.
+
instantiate
(1:=
SimMemId.mk
_
_
).
econs
;
ss
.
Unshelve
.
all
:
ss
;
try
(
by
econs
).
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variable
prog
:
Clight.program
.
Variable
tprog
:
Csharpminor.program
.
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
ClightC.module2
prog
) (
CsharpminorC.module
tprog
)
tt
.
Theorem
sim_mod
:
ModPair.sim
mp
.
Proof.
econs
;
ss
.
-
r
.
inv
TRANSL
.
des
.
unfold
CSk.of_program
,
Sk.of_program
.
f_equal
;
ss
.
revert
H
.
generalize
prog
at
1
as
CTX
.
i
.
destruct
prog
,
tprog
;
ss
.
clear
-
H
.
ginduction
prog_defs
;
ii
;
ss
;
inv
H
;
ss
.
erewrite
IHprog_defs
;
et
.
f_equal
;
ss
.
inv
H2
.
destruct
a
,
b1
;
ss
.
clarify
.
inv
H0
;
ss
.
+
unfold
update_snd
.
ss
.
f_equal
.
destruct
f1
;
inv
H1
;
ss
.
unfold
transl_function
in
H2
.
unfold
bind
in
*.
ss
.
des_ifs
.
+
inv
H
.
ss
.
-
ii
.
inv
SIMSKENVLINK
.
eapply
sim_modsem
;
eauto
.
Qed.
End
SIMMOD
.