Module CleanupLabelsproofC
Require
Import
FSets
.
Require
Import
CoqlibC
Ordered
Integers
.
Require
Import
AST
Linking
.
Require
Import
ValuesC
Memory
Events
Globalenvs
Smallstep
.
Require
Import
Op
Locations
LinearC
.
Require
Import
CleanupLabels
.
Require
Import
sflib
.
newly added *
Require
Export
CleanupLabelsproof
.
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
AsmregsC
MatchSimModSem
ModSemProps
.
Require
SimMemId
.
Require
SoundTop
.
Require
Import
LiftDummy
.
Require
Import
JunkBlock
.
Set
Implicit
Arguments
.
Definition
strong_wf_tgt
(
st_tgt0
:
Linear.state
):
Prop
:=
exists
sg_init
ls_init
,
last_option
st_tgt0
.(
LinearC.get_stack
) =
Some
(
Linear.dummy_stack
sg_init
ls_init
).
Section
SIMMODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variable
prog
tprog
:
Linear.program
.
Let
md_src
:
Mod.t
:= (
LinearC.module
prog
).
Let
md_tgt
:
Mod.t
:= (
LinearC.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
:= (
SkEnv.revive
(
SkEnv.project
skenv_link
md_src
.(
Mod.sk
))
prog
).
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
st_tgt0
:
Linear.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
CleanupLabelsproof.match_states
st_src0
st_tgt0
)
(
MCOMPATSRC
:
st_src0
.(
LinearC.get_mem
) =
sm0
.(
SimMem.src
))
(
MCOMPATTGT
:
st_tgt0
.(
LinearC.get_mem
) =
sm0
.(
SimMem.tgt
))
(
DUMMYTGT
:
strong_wf_tgt
st_tgt0
)
(
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
f
tf
=>
tf
=
transf_fundef
f
)
eq
prog
)
ge
tge
.
Proof.
subst_locals
.
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 *)
inv
INITTGT
.
destruct
sm_arg
;
ss
.
clarify
.
inv
SIMARGS
;
ss
.
clarify
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
folder
.
exploit
(
bsim_internal_funct_id
SIMGE
);
et
.
i
;
des
.
destruct
fd_src
;
ss
.
eexists
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
cycle
2;
ss
.
+
econs
;
eauto
;
ss
.
*
inv
TYP
.
rpapply
match_states_call
;
try
eapply
Val.lessdef_refl
.
{
instantiate
(1:= [
Linear.dummy_stack
(
fn_sig
fd
)
ls_init
]).
econs
;
eauto
;
econs
;
et
.
econs
.
inv
H
.
}
*
rr
.
ss
.
esplits
;
et
.
(* * ss. esplits; et. *)
+
assert
(
SGEQ
:
fn_sig
fd
=
fn_sig
f
). {
inv
MATCH
;
et
. }
rewrite
SGEQ
.
rpapply
LinearC.initial_frame_intro
;
revgoals
; [
f_equal
;
et
| .. ];
eauto
with
congruence
.
*
folder
.
rewrite
<-
SGEQ
.
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
.
folder
.
des_ifs
.
inv
TYP
.
unfold
transf_function
in
*.
des_ifs
.
destruct
sm_arg
;
ss
.
clarify
.
assert
(
SGEQ
:
fn_sig
fd
=
fn_sig
(
transf_function
fd
)). {
et
. }
esplits
;
eauto
.
econs
;
swap
1 3;
eauto
;
ss
.
-
(* call wf *)
inv
MATCH
;
ss
.
destruct
sm0
;
ss
.
clarify
.
u
in
CALLSRC
.
des
.
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
.
r
in
TRANSL
.
exploit
(
SimSymbId.sim_skenv_revive
TRANSL
);
eauto
.
{
apply
SIMSKENV
. }
intro
GE
.
apply
(
fsim_external_funct_id
GE
);
ss
.
folder
.
inv
H6
;
ss
.
*
des
.
esplits
;
eauto
.
eapply
SimSymb.simskenv_func_fsim
;
eauto
;
ss
.
inv
H6
;
et
.
inv
SIG
.
+
econs
;
ss
;
eauto
.
*
inv
H6
;
et
.
des
.
inv
SIG
.
*
instantiate
(1:=
SimMemId.mk
_
_
).
ss
.
*
ss
.
+
ss
.
-
(* after fsim *)
inv
AFTERSRC
.
inv
SIMRET
;
ss
.
exists
sm_ret
.
destruct
sm_ret
;
ss
.
clarify
.
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
esplits
;
eauto
.
+
econs
;
eauto
.
+
econs
;
ss
;
eauto
.
*
econs
;
eauto
.
{
clear
-
H5
.
inv
H5
.
{
econs
;
et
. }
ss
.
des_ifs
.
econs
;
et
.
inv
H
;
econs
;
et
.
}
*
clear
-
DUMMYTGT
.
unfold
strong_wf_tgt
in
*.
des
.
destruct
ts
;
ss
.
unfold
dummy_stack
,
dummy_function
in
*.
des_ifs
;
ss
;
clarify
;
esplits
;
et
.
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
;
inv
MATCHST
;
ss
.
inv
H3
;
ss
.
inv
H4
;
ss
.
destruct
sm0
;
ss
.
clarify
.
eexists
(
SimMemId.mk
_
_
).
esplits
;
ss
;
eauto
;
try
econs
;
eauto
;
ss
.
rr
in
DUMMYTGT
.
des
.
ss
.
clarify
.
assert
(
sg_init
=
sg_init0
).
{
inv
H1
;
ss
. }
clarify
.
(* repeat f_equal; et. *)
-
left
;
i
.
esplits
;
eauto
.
{
apply
LinearC.modsem_receptive
;
et
. }
inv
MATCH
.
ii
.
r
in
STEPSRC
;
des
.
hexploit
(@
transf_step_correct
prog
skenv_link
skenv_link
);
eauto
.
{
inv
SIMSKENV
.
inv
SIMSKELINK
.
ss
. }
{
apply
make_match_genvs
;
eauto
.
apply
SIMSKENV
. }
i
;
des
.
+
assert
(
PLUS
:
plus
Linear.step
skenv_link
tge
st_tgt0
tr
s2
').
{
econs
.
eapply
H
.
econs
.
rewrite
E0_right
.
et
. }
exploit
(
lift_plus
Linear.step
(
fun
st
=>
get_stack
st
<> [])
strong_wf_tgt
);
ss
;
et
.
{
intros
st
X
Y
.
rr
in
X
.
des
.
rewrite
Y
in
*.
ss
. }
{
i
.
folder
.
unfold
strong_wf_tgt
in
*.
des
.
inv
HSTEP
;
ss
;
eauto
.
-
des_ifs
;
ss
;
eauto
.
-
des_ifs
;
ss
;
eauto
.
right
.
ii
.
inv
HSTEP0
;
ss
. }
{
ii
.
unfold
strong_wf_tgt
in
*;
des
.
inv
HSTEP
;
try
inv
STACKS
;
ss
;
clarify
;
et
;
des_ifs
;
et
. }
{
intro
T
.
inv
H0
;
ss
;
clarify
;
try
inv
STACKS
;
ss
;
try
inv
H1
;
ss
. }
intro
TT
;
des
.
esplits
;
eauto
.
*
left
.
eapply
spread_dplus
;
eauto
.
{
eapply
modsem_determinate
;
eauto
. }
*
instantiate
(1:=
SimMemId.mk
_
_
).
econs
;
ss
.
+
clarify
.
esplits
;
et
.
*
right
.
esplits
;
et
.
{
eapply
star_refl
. }
*
instantiate
(1:=
SimMemId.mk
_
_
).
econs
;
ss
.
Unshelve
.
all
:
ss
;
try
(
by
econs
).
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variable
prog
tprog
:
Linear.program
.
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
LinearC.module
prog
) (
LinearC.module
tprog
)
tt
.
Theorem
sim_mod
:
ModPair.sim
mp
.
Proof.
econs
;
ss
.
-
r
.
eapply
Sk.match_program_eq
;
eauto
.
ii
.
destruct
f1
;
ss
.
+
clarify
.
right
.
esplits
;
eauto
.
+
clarify
.
left
.
esplits
;
eauto
.
-
ii
.
inv
SIMSKENVLINK
.
eapply
sim_modsem
;
eauto
.
Unshelve
.
all
:
ss
.
Qed.
End
SIMMOD
.