Module UnusedglobproofC
Require
Import
FSets
CoqlibC
Maps
Ordered
Iteration
Errors
.
Require
Import
AST
Linking
.
Require
Import
IntegersC
ValuesC
Memory
Globalenvs
Events
Smallstep
.
Require
Import
Op
Registers
RTLC
.
Require
Import
Unusedglob
.
Require
Import
sflib
.
Require
SimMemInj
.
newly added *
Require
Export
Unusedglobproof
.
Require
Import
Simulation
.
Require
Import
Skeleton
Mod
ModSem
SimMod
SimModSem
SimSymb
SimMem
AsmregsC
MatchSimModSem
.
Require
SimMemInjC
.
Require
SimSymbDrop
.
Require
SoundTop
.
Require
Import
CtypingC
.
Require
Import
ModSemProps
.
Require
Import
JunkBlock
.
Set
Implicit
Arguments
.
Section
SIMMODSEM
.
Variable
skenv_link_src
skenv_link_tgt
:
SkEnv.t
.
Variable
sm_link
:
SimMem.t
.
Variable
prog
tprog
:
RTL.program
.
Let
md_src
:
Mod.t
:= (
RTLC.module
prog
).
Let
md_tgt
:
Mod.t
:= (
RTLC.module2
tprog
).
Hypothesis
(
INCLSRC
:
SkEnv.includes
skenv_link_src
md_src
.(
Mod.sk
)).
Hypothesis
(
INCLTGT
:
SkEnv.includes
skenv_link_tgt
md_tgt
.(
Mod.sk
)).
Hypothesis
(
WFSRC
:
SkEnv.wf
skenv_link_src
).
Hypothesis
(
WFTGT
:
SkEnv.wf
skenv_link_tgt
).
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Let
ge
:= (
SkEnv.revive
(
SkEnv.project
skenv_link_src
md_src
.(
Mod.sk
))
prog
).
Let
tge
:= (
SkEnv.revive
(
SkEnv.project
skenv_link_tgt
md_tgt
.(
Mod.sk
))
tprog
).
Definition
msp
:
ModSemPair.t
:=
ModSemPair.mk
(
md_src
.(
Mod.modsem
)
skenv_link_src
) (
md_tgt
.(
Mod.modsem
)
skenv_link_tgt
)
((
prog
.(
defs
) -1
tprog
.(
defs
) -1 (
Pos.eq_dec
tprog
.(
prog_main
))):
ident
->
Prop
)
sm_link
.
Inductive
match_states
(
sm_init
:
SimMem.t
)
(
idx
:
nat
) (
st_src0
:
RTL.state
) (
st_tgt0
:
RTL.state
) (
sm0
:
SimMem.t
):
Prop
:=
|
match_states_intro
(
MATCHST
:
Unusedglobproof.match_states
prog
tprog
(
used_set
tprog
)
skenv_link_src
skenv_link_tgt
ge
tge
st_src0
st_tgt0
sm0
).
Lemma
find_funct_inject
used
fptr
tfptr
fd
j
(
SIMGE
:
meminj_preserves_globals
prog
tprog
used
ge
tge
j
)
(
FINDSRC
:
Genv.find_funct
ge
fptr
=
Some
fd
)
(
INJ
:
Val.inject
j
fptr
tfptr
):
<<
FINDTGT
:
Genv.find_funct
tge
tfptr
=
Some
fd
>>.
Proof.
inv
SIMGE
.
uge0
.
des_ifs_safe
.
inv
INJ
.
exploit
defs_inject
;
et
.
i
;
des
.
clarify
.
psimpl
.
des_ifs
.
Qed.
Theorem
sim_skenv_meminj_preserves_globals
:
forall
sm_arg
(
SIMSKENV
:
SimSymbDrop.sim_skenv
sm_arg
((
prog
.(
defs
) -1
tprog
.(
defs
) -1 (
Pos.eq_dec
tprog
.(
prog_main
))):
ident
->
Prop
)
(
SkEnv.project
skenv_link_src
md_src
.(
Mod.sk
)) (
SkEnv.project
skenv_link_tgt
md_tgt
.(
Mod.sk
))),
<<
SIMGE
:
meminj_preserves_globals
prog
tprog
(
used_set
tprog
)
ge
tge
(
SimMemInj.inj
sm_arg
)>>.
Proof.
i
.
inv
SIMSKENV
.
ss
.
bar
.
destruct
TRANSL
as
[
used0
TRANSL0
].
desH
TRANSL0
.
clarify
.
econs
;
eauto
.
-
i
.
exploit
SIMSYMB1
;
et
.
i
;
des
.
clarify
.
-
i
.
exploit
SIMSYMB2
;
et
.
{
ii
.
des
.
unfold
used_set
,
defs
in
*.
ss
.
des_sumbool
.
align_bool
;
bsimpl
.
des_sumbool
.
des
;
clarify
. }
-
i
.
unfold
ge
in
H0
.
exploit
Genv_map_defs_def
;
et
.
i
;
des
.
exploit
SIMDEF
;
et
.
i
;
des
.
clarify
.
psimpl
.
uo
.
des_ifs_safe
.
exploit
Genv.invert_find_symbol
;
et
.
intro
SYMBSRC
;
des
.
exploit
SIMSYMB1
;
et
.
i
;
des
.
psimpl
.
clear_tac
.
exploit
Genv.find_invert_symbol
;
et
.
intro
SYMBTGT
;
des
.
destruct
(
classic
(
defs
prog
i
));
cycle
1.
{
clear
-
Heq1
H1
.
contradict
H1
.
unfold
defs
in
*.
des_sumbool
.
apply
prog_defmap_spec
;
et
. }
assert
(
KEPT0
: (
defs
tprog
i
\/
Pos.eq_dec
(
prog_main
tprog
)
i
)).
{
tauto
. }
clear
KEPT
.
assert
(
IN
: (
used_set
tprog
)
i
).
{
clarify
.
unfold
used_set
.
repeat
(
des_sumbool
;
des
;
ss
;
eauto
).
right
.
unfold
defs
in
*.
des_sumbool
;
ss
. }
esplits
;
et
.
+
unfold
tge
,
SkEnv.revive
.
erewrite
Genv_map_defs_def_inv
;
et
.
uo
.
des_ifs_safe
.
erewrite
match_prog_def
;
et
.
des_ifs
.
+
i
.
eapply
used_closed
;
et
.
-
unfold
tge
.
i
.
exploit
Genv_map_defs_def
;
et
.
i
;
des
.
uo
.
des_ifs
.
bsimpl
.
exploit
SIMDEFINV
;
et
.
i
;
des
.
clarify
.
psimpl
.
clear_tac
.
exploit
Genv.invert_find_symbol
;
et
.
intro
SYMBTGT
;
des
.
exploit
SIMSYMB3
;
et
.
i
;
des
.
exploit
Genv.find_invert_symbol
;
et
.
intro
SYMBSRC
.
esplits
;
et
.
assert
(
used_set
tprog
i
).
{
hexploit
(
match_prog_def
_
_
_
TRANSL1
i
);
et
.
i
.
des_ifs
. }
exploit
SIMSYMB2
;
et
.
{
unfold
used_set
in
*.
clear
-
H1
.
des_sumbool
.
ii
.
des
.
align_bool
;
bsimpl
.
des_sumbool
.
ss
.
des
;
clarify
.
unfold
defs
in
*.
des_sumbool
.
ss
. }
i
;
des
.
clarify
.
clear_tac
.
assert
(
blk_src
=
b
)
by
(
eapply
DISJ
;
et
).
clarify
.
unfold
ge
.
unfold
SkEnv.revive
.
erewrite
Genv_map_defs_def_inv
;
et
.
uo
.
des_ifs_safe
.
hexploit
(
match_prog_def
_
_
_
TRANSL1
i
);
et
.
intro
DEFMAP
.
des_ifs
.
Qed.
Let
SEGESRC
:
senv_genv_compat
skenv_link_src
ge
.
Proof
.
eapply
SkEnv.senv_genv_compat
;
et
. Qed.
Let
SEGETGT
:
senv_genv_compat
skenv_link_tgt
tge
.
Proof
.
eapply
SkEnv.senv_genv_compat
;
et
. Qed.
Theorem
sim_modsem
:
ModSemPair.sim
msp
.
Proof.
(* rr in TRANSL. destruct TRANSL as [TRANSL0 TRANSL1]. *)
destruct
TRANSL
as
[
used0
TRANSL0
].
des
.
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. *)
inv
INITTGT
.
des
.
inv
SAFESRC
.
destruct
args_src
,
args_tgt
;
ss
.
inv
SIMARGS
;
ss
.
clarify
.
assert
(
SIMGE
:
meminj_preserves_globals
prog
tprog
(
used_set
tprog
)
ge
tge
(
SimMemInj.inj
sm_arg
)).
{
eapply
sim_skenv_meminj_preserves_globals
;
et
.
apply
SIMSKENV
. }
des
.
eexists
.
exploit
SimMemInjC.inject_junk_blocks_tgt
;
et
.
intro
P
;
des
.
exists
sm1
.
esplits
;
eauto
;
econs
;
eauto
;
ss
.
+
inv
TYP
.
folder
.
ss
.
inv
TYP0
.
exploit
find_funct_inject
;
et
.
i
;
des
.
clarify
.
rpapply
match_states_call
;
ss
;
eauto
.
{
econs
;
ss
;
et
.
-
inv
SIMSKENV
.
ss
.
eapply
SimSymbDrop.sim_skenv_symbols_inject
;
et
.
-
inv
SIMSKENV
.
inv
MWF
.
inv
SIMSKELINK
.
ss
.
rewrite
NBSRC
.
xomega
.
-
inv
SIMSKENV
.
inv
MWF
.
inv
SIMSKELINK
.
ss
.
rewrite
assign_junk_blocks_nextblock
.
rewrite
NBTGT
.
des_ifs
;
xomega
.
}
{
eapply
inject_list_typify_list
;
eauto
. }
{
eapply
MWF0
. }
-
des
.
inv
SAFESRC
.
inv
SIMARGS
;
ss
.
assert
(
SIMGE
:
meminj_preserves_globals
prog
tprog
(
used_set
tprog
)
ge
tge
(
SimMemInj.inj
sm_arg
)).
{
eapply
sim_skenv_meminj_preserves_globals
;
et
.
apply
SIMSKENV
. }
exploit
find_funct_inject
;
et
.
i
;
des
.
clarify
.
inv
TYP
.
esplits
;
eauto
.
econs
;
eauto
.
+
econs
;
et
.
etrans
;
try
apply
LEN
;
et
.
symmetry
.
eapply
inject_list_length
;
et
.
(* TODO: add lemma *)
+
etrans
;
try
apply
LEN
;
et
.
symmetry
.
eapply
inject_list_length
;
et
.
-
(* call wf *)
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
-
(* call fsim *)
des
.
clear_tac
.
assert
(
SIMGE
:
meminj_preserves_globals
prog
tprog
(
used_set
tprog
)
ge
tge
(
SimMemInj.inj
sm0
)).
{
eapply
sim_skenv_meminj_preserves_globals
;
et
.
apply
SIMSKENV
. }
inv
MATCH
;
ss
.
inv
CALLSRC
.
inv
MATCHST
;
ss
.
clarify
.
folder
.
inv
MCOMPAT
;
ss
.
clear_tac
.
inv
FPTR
;
try
(
by
des
;
ss
).
ss
.
destruct
(
Ptrofs.eq_dec
ofs1
Ptrofs.zero
);
clarify
;
try
(
by
des
;
ss
).
esplits
;
try
refl
;
eauto
.
+
econs
;
eauto
.
*
folder
.
ss
.
des_ifs_safe
.
inv
SIMGE
.
uge0
.
des_ifs_safe
.
exploit
defs_rev_inject
;
eauto
.
i
;
des
.
clarify
.
des_ifs_safe
.
des_ifs
.
*
clear
EXTERNAL
.
des
.
ss
.
uge0
.
des_ifs_safe
.
psimpl
.
inv
SIMSKENV
.
inv
SIMSKELINK
.
ss
.
exploit
SIMDEF
;
et
.
i
;
des
.
clarify
.
des_ifs
.
esplits
;
et
.
+
econs
;
ss
;
et
.
-
(* after fsim *)
des
.
clear_tac
.
assert
(
SIMGE
:
meminj_preserves_globals
prog
tprog
(
used_set
tprog
)
ge
tge
(
SimMemInj.inj
sm0
)).
{
eapply
sim_skenv_meminj_preserves_globals
;
et
.
apply
SIMSKENV
. }
inv
AFTERSRC
.
inv
SIMRET
;
ss
.
exists
(
SimMemInj.unlift
'
sm_arg
sm_ret
).
inv
MATCH
;
ss
.
inv
MATCHST
;
ss
.
inv
HISTORY
.
ss
.
clear_tac
.
esplits
;
try
refl
;
eauto
.
+
econs
;
eauto
.
+
econs
;
ss
;
eauto
.
inv
MLE0
;
ss
.
inv
MCOMPAT
.
clear_tac
.
rpapply
match_states_return
;
ss
;
eauto
;
ss
.
{
eapply
match_stacks_bound
;
eauto
with
mem
.
eapply
match_stacks_incr
;
et
.
i
.
inv
FROZEN
.
exploit
NEW_IMPLIES_OUTSIDE
;
et
. }
{
eapply
inject_typify
;
et
. }
{
eapply
MWFAFTR
. }
-
(* final fsim *)
inv
MATCH
.
inv
FINALSRC
;
inv
MATCHST
;
ss
.
inv
STACKS
.
inv
MCOMPAT
;
ss
.
eexists
sm0
.
esplits
;
ss
;
eauto
;
try
refl
.
econs
;
eauto
.
-
(* step *)
left
;
i
.
assert
(
SIMGE
:
meminj_preserves_globals
prog
tprog
(
used_set
tprog
)
ge
tge
(
SimMemInj.inj
sm0
)).
{
eapply
sim_skenv_meminj_preserves_globals
;
et
.
apply
SIMSKENV
. }
esplits
;
eauto
.
{
apply
modsem_receptive
;
et
. }
inv
MATCH
.
ii
.
hexploit
(@
step_simulation
prog
tprog
(
used_set
tprog
)
skenv_link_src
skenv_link_tgt
);
eauto
.
i
;
des
.
esplits
;
eauto
.
+
left
.
apply
plus_one
.
econs
;
eauto
.
eapply
modsem2_determinate
;
eauto
.
+
econs
;
ss
;
inv
H0
;
ss
;
inv
MCOMPAT
;
ss
.
Unshelve
.
all
:
ss
;
try
(
by
econs
).
Qed.
End
SIMMODSEM
.
Section
SIMMOD
.
Variable
prog
:
RTL.program
.
Variable
tprog
:
RTL.program
.
Hypothesis
TRANSL
:
match_prog
prog
tprog
.
Definition
mp
:
ModPair.t
:=
ModPair.mk
(
RTLC.module
prog
) (
RTLC.module2
tprog
) ((
prog
.(
defs
) -1
tprog
.(
defs
) -1 (
Pos.eq_dec
tprog
.(
prog_main
))):
ident
->
Prop
).
Theorem
sim_mod
:
ModPair.sim
mp
.
Proof.
econs
;
ss
.
-
destruct
TRANSL
as
[
used0
TRANSL0
].
desH
TRANSL0
.
clarify
.
econs
;
ss
.
+
i
.
ss
.
inv
TRANSL1
.
specialize
(
match_prog_def
id
).
assert
(
REL0
:= (
Sk.of_program_prog_defmap
prog
fn_sig
id
)).
assert
(
REL1
:= (
Sk.of_program_prog_defmap
tprog
fn_sig
id
)).
destruct
(
classic
(
defs
prog
id
));
cycle
1.
{
rewrite
<- (
Sk.of_program_defs
fn_sig
)
in
H
.
inv
REL0
;
align_opt
;
cycle
1.
{
exploit
prog_defmap_image
;
et
.
i
;
des
.
unfold
defs
in
*.
align_bool
;
bsimpl
.
align_bool
.
des_sumbool
.
ss
. }
unfold
fundef
in
*.
rewrite
H1
in
*.
inv
REL1
;
align_opt
;
ss
;
clarify
.
des_ifs
.
}
assert
(
KEPT0
:
defs
tprog
id
\/
Pos.eq_dec
(
prog_main
tprog
)
id
)
by
tauto
.
clear
KEPT
.
assert
(
IN
:
used_set
tprog
id
).
{
unfold
used_set
.
des_sumbool
.
ss
.
des
;
et
;
bsimpl
.
-
right
.
unfold
defs
in
*.
des_sumbool
.
ss
.
-
des_sumbool
.
clarify
.
tauto
. }
des_ifs
.
unfold
fundef
in
*.
rewrite
match_prog_def
in
*.
erewrite
(
Sk.of_program_prog_defmap_eq
fn_sig
prog
tprog
)
in
*;
ss
.
+
i
.
ss
.
inv
TRANSL1
.
specialize
(
match_prog_def
id
).
assert
(
REL0
:= (
Sk.of_program_prog_defmap
prog
fn_sig
id
)).
assert
(
REL1
:= (
Sk.of_program_prog_defmap
tprog
fn_sig
id
)).
des
.
align_bool
;
bsimpl
.
align_bool
.
des_sumbool
.
inv
REL1
;
ss
;
align_opt
.
rewrite
<- (
Sk.of_program_defs
fn_sig
)
in
DROP1
.
exploit
prog_defmap_image
;
et
.
i
;
des
.
unfold
defs
in
*;
ss
.
des_sumbool
.
ss
.
+
ii
.
unfold
privs
.
bsimpl
.
des
.
bsimpl
.
des_sumbool
.
rewrite
(
Sk.of_program_defs
fn_sig
).
split
;
ss
.
unfold
NW
.
align_bool
;
bsimpl
.
des_sumbool
.
ii
.
exploit
used_public
;
et
.
intro
IN
.
unfold
used_set
,
defs
in
*.
des_sumbool
.
ss
.
des
;
clarify
;
ss
.
+
inv
TRANSL1
;
ss
.
+
inv
TRANSL1
;
ss
.
+
ii
.
des
.
inv
TRANSL0
.
assert
(
PROG0
: (
prog_defmap
tprog
) !
id
=
Some
(
Gvar
gv
)).
{
generalize
(
Sk.of_program_prog_defmap
tprog
fn_sig
id
).
intro
REL
.
(* TODO: make lemma!!!!!!!!!!!!!!!!!!! *)
inv
REL
;
try
congruence
.
rewrite
PROG
in
*.
clarify
.
inv
H2
.
inv
H4
.
ss
.
destruct
i1
,
i2
;
ss
.
}
inv
TRANSL1
.
rewrite
match_prog_def
in
*.
des_ifs
.
exploit
(
used_closed
id
);
et
.
ii
.
exploit
used_defined
;
et
.
i
;
des
.
{
exploit
prog_defmap_dom
;
et
.
i
;
des
.
specialize
(
match_prog_def
id_drop
).
des_ifs
.
rewrite
H2
in
*.
unfold
defs
in
DROP1
.
apply
DROP1
.
des_sumbool
.
eapply
prog_defmap_image
;
et
. }
{
clarify
.
apply
DROP0
.
des_sumbool
.
ss
. }
+
inv
TRANSL1
.
eapply
NoDup_norepet
;
et
.
rewrite
Sk.of_program_defs_names
;
ss
.
+
ii
.
des
.
eapply
H0
.
des_sumbool
.
inv
TRANSL1
.
eauto
.
-
ii
.
eapply
sim_modsem
;
eauto
.
Unshelve
.
all
:
ss
.
Qed.
End
SIMMOD
.