Module AllocproofC
Require
Import
FunInd
.
Require
Import
FSets
.
Require
Import
CoqlibC
Ordered
Maps
Errors
IntegersC
Floats
.
Require
Import
AST
Linking
Lattice
Kildall
.
Require
Import
ValuesC
MemoryC
Globalenvs
Events
Smallstep
.
Require
Archi
.
Require
Import
Op
Registers
RTLC
LocationsC
Conventions
RTLtypingC
LTLC
.
Require
Import
Allocation
.
Require
Import
sflib
.
newly added *
Require
Export
Allocproof
.
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
AsmregsC
MatchSimModSem
.
Require
Import
ModSemProps
.
Require
SimMemExt
.
Require
SoundTop
.
Require
Import
LiftDummy
.
Set
Implicit
Arguments
.
Definition
strong_wf_tgt
(
st_tgt0
:
LTL.state
):
Prop
:=
exists
sg_init
ls_init
,
last_option
st_tgt0
.(
LTLC.get_stack
) =
Some
(
LTL.dummy_stack
sg_init
ls_init
).
Lemma
agree_callee_save_after
tstks
ls
sg
tv
(
NOTNIL
:
tstks
<> [])
(
AG
:
agree_callee_save
(
parent_locset
tstks
)
ls
):
<<
AG
:
agree_callee_save
(
parent_locset
(
stackframes_after_external
tstks
))
(
Locmap.setpair
(
loc_result
sg
)
tv
(
undef_caller_save_regs
ls
))>>.
Proof.
hexploit
(
loc_result_one
sg
);
et
.
intro
ONE
.
unfold
agree_callee_save
in
*.
ii
.
exploit
AG
;
et
.
intro
T
.
destruct
tstks
;
ss
.
des_ifs
.
ss
.
rewrite
locmap_get_set_loc_result
;
ss
;
cycle
1.
{
des_ifs
. }
unfold
undef_outgoing_slots
,
callee_save_loc
in
*.
des_ifs
;
ss
.
des_ifs
.
Qed.
Lemma
match_stackframes_after
tse
tge
stks
tstks
sg
(
STACKS
:
match_stackframes
tse
tge
stks
tstks
sg
):
<<
STACKS
:
match_stackframes
tse
tge
stks
tstks
.(
stackframes_after_external
)
sg
>>.
Proof.
inv
STACKS
;
econs
;
et
.
i
.
exploit
STEPS
;
et
.
clear
-
H1
.
unfold
agree_callee_save
in
*.
ii
.
exploit
H1
;
et
.
intro
T
.
unfold
undef_outgoing_slots
in
*.
des_ifs
.
Qed.
Lemma
match_stackframes_not_nil
skenv_link
tge
stack
ts
sg_arg
(
MATCH
:
match_stackframes
skenv_link
tge
stack
ts
sg_arg
):
ts
<> [].
Proof.
inv
MATCH
;
ss
. Qed.
Lemma
getpair_equal
sg_init
sg
ls
(
SAMERES
:
sig_res
sg_init
=
sig_res
sg
):
Locmap.getpair
(
map_rpair
R
(
loc_result
sg_init
))
ls
=
Locmap.getpair
(
map_rpair
R
(
loc_result
sg
))
ls
.
Proof.
do
2
f_equal
.
unfold
loc_result
.
des_ifs
.
unfold
loc_result_64
.
des_ifs
. Qed.
Section
SIMMODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variable
prog
:
RTL.program
.
Variable
tprog
:
LTL.program
.
Let
md_src
:
Mod.t
:= (
RTLC.module2
prog
).
Let
md_tgt
:
Mod.t
:= (
LTLC.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
:
RTL.state
) (
st_tgt0
:
LTL.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
Allocproof.match_states
skenv_link
tge
st_src0
st_tgt0
)
(
MCOMPATSRC
:
st_src0
.(
RTL.get_mem
) =
sm0
.(
SimMem.src
))
(
MCOMPATTGT
:
st_tgt0
.(
LTLC.get_mem
) =
sm0
.(
SimMem.tgt
))
(
DUMMYTGT
:
strong_wf_tgt
st_tgt0
).
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
_
f
tf
=>
transf_fundef
f
=
OK
tf
)
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
:=
fun
_
_
=>
wt_state
);
eauto
;
ii
;
ss
.
-
instantiate
(1:=
Nat.lt
).
apply
lt_wf
.
-
eapply
wt_state_local_preservation
;
et
.
ii
.
exploit
wt_prog
;
eauto
.
-
(* init bsim *)
destruct
sm_arg
;
ss
.
clarify
.
inv
INITTGT
.
inv
SIMARGS
;
ss
.
clarify
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
des
.
exploit
lessdef_list_length
;
et
.
intro
LEN
;
des
.
exploit
(
bsim_internal_funct_id
SIMGE
);
et
.
i
;
des
.
exploit
(
sig_function_translated
);
eauto
.
intro
SGEQ
.
ss
.
eexists
.
eexists
(
SimMemExt.mk
_
_
).
esplits
;
cycle
2.
+
econs
;
eauto
;
ss
.
*
inv
TYP
.
eapply
match_states_call
;
eauto
;
ss
.
{
econs
;
et
. }
{
rewrite
<-
TYP0
.
eapply
lessdef_list_typify_list
;
try
apply
VALS
;
et
.
xomega
. }
{
eapply
JunkBlock.assign_junk_block_extends
;
eauto
. }
{
eapply
typify_has_type_list
;
et
.
xomega
. }
*
rr
.
ss
.
esplits
;
et
.
+
inv
SAFESRC
.
folder
.
hexploit
(
find_funct_lessdef
ge
FINDF0
FPTR
);
et
.
intro
FEQ
.
rewrite
<-
FEQ
in
*.
clarify
.
rpapply
RTLC.initial_frame2_intro
;
et
.
f_equal
;
ss
.
inv
TYP0
;
ss
.
congruence
.
+
ss
.
-
(* init progress *)
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
inv
FPTR
;
ss
.
exploit
make_match_genvs
;
eauto
. {
apply
SIMSKENV
. }
intro
SIMGE
.
exploit
(
Genv.find_funct_match_genv
SIMGE
);
eauto
.
i
;
des
.
exploit
(
sig_function_translated
);
eauto
.
intro
SGEQ
.
ss
.
ss
.
unfold
bind
in
*.
folder
.
des_ifs
.
ss
.
exploit
(
fill_arguments_progress
(
Locmap.init
Vundef
)
(
typify_list
vs_tgt
(
sig_args
(
fn_sig
f
)))
(
loc_arguments
f
.(
fn_sig
)));
eauto
.
{
rewrite
<-
sig_args_length
.
rewrite
SGEQ
.
unfold
typify_list
.
rewrite
zip_length
.
rewrite
<-
LEN
.
erewrite
<-
lessdef_list_length
;
et
.
eapply
Min.min_idempotent
.
}
i
;
des
.
rename
ls1
into
ls_init
.
exploit
fill_arguments_spec
;
et
.
i
;
des
.
esplits
;
eauto
.
econs
;
eauto
.
+
rewrite
SGEQ
.
ss
.
+
econs
;
eauto
.
erewrite
<-
lessdef_list_length
;
eauto
.
congruence
.
+
ii
.
rewrite
OUT
;
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
FPTR
;
ss
.
*
des
.
esplits
;
eauto
.
eapply
SimSymb.simskenv_func_fsim
;
eauto
;
ss
.
+
econs
;
ss
;
eauto
.
*
instantiate
(1:=
SimMemExt.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
.
*
eapply
match_stackframes_after
;
et
.
*
hexploit
(
loc_result_one
sg_arg
);
et
.
i
.
des
.
rewrite
ONE
.
ss
.
rewrite
Locmap.gss
.
eapply
lessdef_typify
;
et
.
*
eapply
agree_callee_save_after
;
et
.
eapply
match_stackframes_not_nil
;
et
.
*
eapply
typify_has_type
;
et
.
*
rr
.
rr
in
DUMMYTGT
.
des
.
ss
.
destruct
ts
;
ss
.
des_ifs_safe
;
ss
.
destruct
ts
;
ss
;
et
.
unfold
undef_outgoing_slots
.
unfold
dummy_stack
in
*.
clarify
.
esplits
;
et
.
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
;
inv
MATCHST
;
ss
.
inv
STACKS
;
ss
.
destruct
sm0
;
ss
.
clarify
.
eexists
(
SimMemExt.mk
_
_
).
esplits
;
ss
;
eauto
.
econs
;
et
;
ss
.
rpapply
RES
.
eapply
getpair_equal
;
et
.
-
left
;
i
.
esplits
;
eauto
.
{
apply
RTLC.modsem2_receptive
;
et
. }
inv
MATCH
.
ii
.
hexploit
(@
step_simulation
prog
_
skenv_link
skenv_link
);
eauto
.
{
inv
SIMSKENV
.
ss
. }
{
apply
make_match_genvs
;
eauto
.
apply
SIMSKENV
. }
{
ss
.
des
.
ss
. }
i
;
des
.
exploit
(
lift_plus
LTL.step
(
fun
st
=>
get_stack
st
<> [])
strong_wf_tgt
);
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
MAINARGS
;
ss
. }
i
;
des
.
esplits
;
eauto
.
+
left
.
eapply
spread_dplus
;
eauto
.
eapply
modsem_determinate
;
eauto
.
+
instantiate
(1:= (
SimMemExt.mk
_
_
)).
econs
;
ss
.
Unshelve
.
all
:
ss
.
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variable
prog
:
RTL.program
.
Variable
tprog
:
LTL.program
.
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
RTLC.module2
prog
) (
LTLC.module
tprog
)
tt
.
Theorem
sim_mod
:
ModPair.sim
mp
.
Proof.
econs
;
ss
.
-
r
.
eapply
Sk.match_program_eq
;
eauto
.
ii
.
exploit
sig_function_translated
;
et
.
i
.
destruct
f1
;
ss
.
+
clarify
.
right
.
unfold
bind
in
MATCH
.
des_ifs
.
esplits
;
eauto
.
+
clarify
.
left
.
esplits
;
eauto
.
-
ii
.
inv
SIMSKENVLINK
.
eapply
sim_modsem
;
eauto
.
Qed.
End
SIMMOD
.