Module ValueDomainC
Require
Import
FunInd
.
Require
Import
Zwf
CoqlibC
Maps
Integers
Floats
Lattice
.
Require
Import
Compopts
AST
.
Require
Import
Values
MemoryC
Globalenvs
Events
.
Require
Import
Registers
RTL
.
Require
Import
sflib
.
newly added *
Require
Export
ValueDomain
.
Require
Import
Skeleton
.
Require
Import
Sound
UnreachC
.
Require
Import
ModSem
.
Definition
bc2su
(
bc
:
block_classification
) (
ge_nb
:
block
) (
nb
:
block
):
Unreach.t
:=
Unreach.mk
(
fun
blk
=>
if
plt
blk
nb
then
block_class_eq
(
bc
blk
)
BCinvalid
else
false
)
ge_nb
nb
.
Lemma
sound_state_sound_args
bc
m0
p
skenv_link
vs_arg
rm
(
ge
:
genv
)
(
GENV
:
ge
= (
SkEnv.revive
(
SkEnv.project
skenv_link
p
.(
Sk.of_program
fn_sig
))
p
))
(
ARGS
:
forall
v
:
val
,
In
v
vs_arg
->
vmatch
bc
v
Vtop
)
(
RO
:
romatch
bc
m0
rm
)
(
MM
:
mmatch
bc
m0
mtop
)
(
GE
:
genv_match
bc
ge
)
(
NOSTK
:
forall
b
,
bc
b
<>
BCstack
)
fptr_arg
sg_arg
(
SIG
:
exists
skd
,
Genv.find_funct
skenv_link
fptr_arg
=
Some
skd
/\
Sk.get_csig
skd
=
sg_arg
):
args
' (
bc2su
bc
ge
.(
Genv.genv_next
)
m0
.(
Mem.nextblock
)) (
Args.mk
fptr_arg
vs_arg
m0
).
Proof.
{
r
.
s
.
esplits
;
eauto
.
-
des
.
unfold
Genv.find_funct
,
Genv.find_funct_ptr
in
*.
des_ifs
.
ss
.
r
.
ii
;
clarify
.
ss
.
r
in
GE
.
des
.
specialize
(
GE0
blk
).
exploit
GE0
;
eauto
.
{
ss
.
eapply
Genv.genv_defs_range
;
eauto
. }
i
;
des
.
(* exploit sound_stack_unreach_compat; eauto. intro CPT. des. *)
(* inv SU. ss. *)
esplits
;
eauto
.
+
ii
.
des_ifs
.
des_sumbool
.
congruence
.
+
inv
MM
.
eapply
mmatch_below
;
eauto
.
rewrite
H
;
ss
.
-
rewrite
Forall_forall
.
i
.
spcN
1
ARGS
.
spc
ARGS
.
ii
;
clarify
.
assert
(
BCV
:
bc
blk
<>
BCinvalid
).
{
inv
ARGS
;
ss
.
inv
H1
;
ss
. }
esplits
;
eauto
.
+
u
.
ii
.
des_ifs
.
des_sumbool
.
ss
.
+
inv
MM
.
eapply
mmatch_below
;
eauto
.
-
inv
MM
.
econs
;
eauto
.
+
ii
.
clarify
.
assert
(
BCV
:
bc
blk
<>
BCinvalid
).
{
u
in
PUB
.
ii
.
rewrite
H
in
*.
ss
.
exploit
Mem.perm_valid_block
;
eauto
.
i
;
des
.
des_ifs
. }
assert
(
BCV0
:
bc
blk0
<>
BCinvalid
).
{
exploit
mmatch_top
;
eauto
.
(* spcN 0%nat mmatch_top. spc mmatch_top. inv mmatch_top. *)
intro
SM
.
inv
SM
.
specialize
(
H0
ofs
%
Z
blk0
ofs0
q
n
).
exploit
H0
.
{
eapply
Mem_loadbytes_succeeds
;
et
. }
intro
PM
.
inv
PM
.
ss
.
}
esplits
;
eauto
.
{
u
.
des_ifs
.
i
;
des_sumbool
;
ss
. }
s
.
eapply
mmatch_below
;
eauto
.
+
u
.
ii
.
des_ifs
.
+
ss
.
r
in
GE
.
ss
.
des
.
r
in
mmatch_below
.
apply
NNPP
.
ii
.
apply
Pos.lt_nle
in
H
.
exploit
GE0
;
eauto
.
i
;
des
.
exploit
mmatch_below
;
eauto
. {
rewrite
H0
;
ss
. }
i
;
des
.
xomega
.
-
econs
;
ss
;
i
;
des_ifs
.
r
in
GE
.
des
.
ss
.
des_sumbool
.
apply
NNPP
.
ii
.
exploit
(
GE0
x0
);
eauto
. {
xomega
. }
i
;
des
.
congruence
.
}
Qed.
Lemma
sound_state_sound_retv
bc
m_ret
p
skenv_link
v_ret
rm
(
ge
:
genv
)
(
GENV
:
ge
= (
SkEnv.revive
(
SkEnv.project
skenv_link
p
.(
Sk.of_program
fn_sig
))
p
))
(
RES
:
vmatch
bc
v_ret
Vtop
)
(
RO
:
romatch
bc
m_ret
rm
)
(
MM
:
mmatch
bc
m_ret
mtop
)
(
GE
:
genv_match
bc
ge
)
(
NOSTK
:
forall
b
,
bc
b
<>
BCstack
):
Sound.retv
(
bc2su
bc
ge
.(
Genv.genv_next
)
m_ret
.(
Mem.nextblock
)) (
Retv.mk
v_ret
m_ret
).
Proof.
{
r
.
s
.
esplits
;
eauto
.
-
ii
;
clarify
.
assert
(
BCV
:
bc
blk
<>
BCinvalid
).
{
inv
RES
;
ss
.
inv
H0
;
ss
. }
esplits
;
eauto
.
+
u
.
ii
.
des_ifs
.
des_sumbool
.
ss
.
+
inv
MM
.
eapply
mmatch_below
;
eauto
.
-
inv
MM
.
econs
;
eauto
.
+
ii
.
clarify
.
assert
(
BCV
:
bc
blk
<>
BCinvalid
).
{
u
in
PUB
.
ii
.
rewrite
H
in
*.
ss
.
exploit
Mem.perm_valid_block
;
eauto
.
i
;
des
.
des_ifs
. }
assert
(
BCV0
:
bc
blk0
<>
BCinvalid
).
{
exploit
mmatch_top
;
eauto
.
(* spcN 0%nat mmatch_top. spc mmatch_top. inv mmatch_top. *)
intro
SM
.
inv
SM
.
specialize
(
H0
ofs
blk0
ofs0
q
n
).
exploit
H0
.
{
eapply
Mem_loadbytes_succeeds
;
et
. }
intro
PM
.
inv
PM
.
ss
.
}
esplits
;
eauto
.
{
u
.
des_ifs
.
i
;
des_sumbool
;
ss
. }
s
.
eapply
mmatch_below
;
eauto
.
+
u
.
ii
.
des_ifs
.
+
ss
.
r
in
GE
.
ss
.
des
.
r
in
mmatch_below
.
apply
NNPP
.
ii
.
apply
Pos.lt_nle
in
H
.
exploit
GE0
;
eauto
.
i
;
des
.
exploit
mmatch_below
;
eauto
. {
rewrite
H0
;
ss
. }
i
;
des
.
xomega
.
-
econs
;
eauto
;
ss
;
i
;
des_ifs
.
des_sumbool
.
rr
in
GE
.
des
.
apply
NNPP
.
ii
.
exploit
(
GE0
x0
);
eauto
.
{
unfold
fundef
in
*.
xomega
. }
i
;
des
.
congruence
.
}
Qed.