Module LinearC
Require
Import
CoqlibC
.
Require
Import
ASTC
Integers
ValuesC
MemoryC
EventsC
GlobalenvsC
Smallstep
.
Require
Import
Op
LocationsC
LTL
Conventions
.
newly added *
Require
Export
Linear
.
Require
Import
Skeleton
Mod
ModSem
.
Require
Import
Simulation
AsmregsC
.
Require
Import
JunkBlock
.
Set
Implicit
Arguments
.
Local
Obligation
Tactic
:=
ii
;
ss
;
des
;
do
2
inv_all_once
;
ss
;
clarify
.
Section
NEWSTEP
.
Variable
se
:
Senv.t
.
Variable
ge
:
genv
.
Let
find_function_ptr
:=
find_function_ptr
ge
.
Definition
get_stack
(
st
:
state
):
list
stackframe
:=
match
st
with
|
State
stk
_
_
_
_
_
=>
stk
|
Callstate
stk
_
_
_
_
=>
stk
|
Returnstate
stk
_
_
=>
stk
end
.
Definition
step
:
state
->
trace
->
state
->
Prop
:=
fun
st0
tr
st1
=>
<<
STEP
:
Linear.step
se
ge
st0
tr
st1
>> /\ <<
NOTDUMMY
:
st1
.(
get_stack
) <> []>>.
End
NEWSTEP
.
Hint
Unfold
step
.
Definition
get_mem
(
st
:
state
):
mem
:=
match
st
with
|
State
_
_
_
_
_
m0
=>
m0
|
Callstate
_
_
_
_
m0
=>
m0
|
Returnstate
_
_
m0
=>
m0
end
.
Definition
get_locset
(
st
:
state
):
locset
:=
match
st
with
|
State
_
_
_
_
ls
_
=>
ls
|
Callstate
_
_
_
ls
_
=>
ls
|
Returnstate
_
ls
_
=>
ls
end
.
Definition
current_locset
(
stk
:
stackframe
):
locset
:=
match
stk
with
|
Stackframe
_
_
ls
_
=>
ls
end
.
Definition
current_function
(
stk
:
Linear.stackframe
):
Linear.function
:=
match
stk
with
|
Linear.Stackframe
f
_
_
_
=>
f
end
.
Definition
undef_outgoing_slots
(
ls
:
locset
):
locset
:=
fun
l
=>
match
l
with
|
S
Outgoing
_
_
=>
Vundef
|
_
=>
ls
l
end
.
Definition
stackframes_after_external
(
stack
:
list
stackframe
):
list
stackframe
:=
match
stack
with
|
nil
=>
nil
|
Stackframe
f
sp
ls
bb
::
tl
=>
Stackframe
f
sp
ls
.(
undef_outgoing_slots
)
bb
::
tl
end
.
Lemma
parent_locset_after_external
:
forall
stack
,
<<
SPURRIOUS
:
parent_locset
stack
.(
stackframes_after_external
) =
parent_locset
stack
/\
stack
= []>>
\/ <<
AFTER
:
parent_locset
stack
.(
stackframes_after_external
) = (
parent_locset
stack
).(
undef_outgoing_slots
)>>.
Proof.
destruct
stack
;
ss
.
{
left
;
ss
. }
des_ifs
;
ss
.
right
.
ss
.
Qed.
Section
MODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
p
:
program
.
Let
skenv
:
SkEnv.t
:=
skenv_link
.(
SkEnv.project
)
p
.(
Sk.of_program
fn_sig
).
Let
ge
:
genv
:=
skenv
.(
SkEnv.revive
)
p
.
Inductive
at_external
:
state
->
Args.t
->
Prop
:=
|
at_external_intro
stack
fptr_arg
sg
ls
vs_arg
m0
(
EXTERNAL
:
ge
.(
Genv.find_funct
)
fptr_arg
=
None
)
(
SIG
:
exists
skd
,
skenv_link
.(
Genv.find_funct
)
fptr_arg
=
Some
skd
/\
Sk.get_csig
skd
=
Some
sg
)
(
VALS
:
vs_arg
=
map
(
fun
p
=>
Locmap.getpair
p
ls
) (
loc_arguments
sg
)):
at_external
(
Callstate
stack
fptr_arg
sg
ls
m0
) (
Args.Cstyle
fptr_arg
vs_arg
m0
).
Inductive
initial_frame
(
args
:
Args.t
):
state
->
Prop
:=
|
initial_frame_intro
fd
ls_init
sg
tvs
n
m0
(
CSTYLE
:
Args.is_cstyle
args
/\
fd
.(
fn_sig
).(
sig_cstyle
) =
true
)
(
SIG
:
sg
=
fd
.(
fn_sig
))
(
FINDF
:
Genv.find_funct
ge
args
.(
Args.fptr
) =
Some
(
Internal
fd
))
(
TYP
:
typecheck
args
.(
Args.vs
)
sg
tvs
)
(
LOCSET
:
tvs
=
map
(
fun
p
=>
Locmap.getpair
p
ls_init
) (
loc_arguments
sg
))
(
JUNK
:
assign_junk_blocks
args
.(
Args.m
)
n
=
m0
)
(
PTRFREE
:
forall
loc
(
NOTIN
: ~
In
loc
(
regs_of_rpairs
(
loc_arguments
sg
))),
<<
PTRFREE
:
is_junk_value
args
.(
Args.m
)
m0
(
ls_init
loc
)>>)
(
SLOT
:
forall
sl
ty
ofs
(
NOTIN
: ~
In
(
S
sl
ty
ofs
) (
regs_of_rpairs
(
loc_arguments
sg
))),
<<
UNDEF
:
ls_init
(
S
sl
ty
ofs
) =
Vundef
>>):
initial_frame
args
(
Callstate
[
dummy_stack
sg
ls_init
]
args
.(
Args.fptr
)
sg
ls_init
m0
).
Inductive
final_frame
:
state
->
Retv.t
->
Prop
:=
|
final_frame_intro
ls0
m0
sg_init
ls_init
v0
(
VAL
:
Locmap.getpair
(
map_rpair
R
(
loc_result
sg_init
))
ls0
=
v0
):
final_frame
(
Returnstate
[
dummy_stack
sg_init
ls_init
]
ls0
m0
) (
Retv.mk
v0
m0
).
Inductive
after_external
:
state
->
Retv.t
->
state
->
Prop
:=
|
after_external_intro
stack
fptr_arg
sg_arg
ls_arg
m_arg
retv
ls_after
(
CSTYLE
:
Retv.is_cstyle
retv
)
(
LSAFTER
:
ls_after
=
Locmap.setpair
(
loc_result
sg_arg
)
(
typify
retv
.(
Retv.v
)
sg_arg
.(
proj_sig_res
))
(
undef_caller_save_regs
ls_arg
)):
after_external
(
Callstate
stack
fptr_arg
sg_arg
ls_arg
m_arg
)
retv
(
Returnstate
stack
.(
stackframes_after_external
)
ls_after
retv
.(
Retv.m
)).
Program
Definition
modsem
:
ModSem.t
:=
{|
ModSem.step
:=
step
;
ModSem.at_external
:=
at_external
;
ModSem.initial_frame
:=
initial_frame
;
ModSem.final_frame
:=
final_frame
;
ModSem.after_external
:=
after_external
;
ModSem.globalenv
:=
ge
;
ModSem.skenv
:=
skenv
;
ModSem.skenv_link
:=
skenv_link
;
|}.
Lemma
modsem_determinate
:
forall
st
,
determinate_at
modsem
st
.
Proof.
econs
;
eauto
.
-
ii
;
ss
.
inv
H
;
inv
H0
.
inv
H1
;
inv
H
;
clarify_meq
;
try
(
determ_tac
eval_builtin_args_determ
;
check_safe
);
try
(
determ_tac
external_call_determ
;
check_safe
);
esplits
;
eauto
;
try
(
econs
;
eauto
);
ii
;
eq_closure_tac
;
clarify_meq
.
-
ii
.
inv
H
.
inv
H0
;
try
(
exploit
external_call_trace_length
;
eauto
;
check_safe
;
intro
T
;
des
);
ss
;
try
xomega
.
Qed.
Lemma
modsem_receptive
:
forall
st
,
receptive_at
modsem
st
.
Proof.
econs
;
eauto
.
-
ii
;
ss
.
inv
H
.
inv
H1
;
try
(
exploit
external_call_receptive
;
eauto
;
check_safe
;
intro
T
;
des
);
inv_match_traces
;
try
(
by
esplits
;
eauto
;
econs
; [
econs
;
eauto
|];
eauto
).
-
ii
.
inv
H
.
inv
H0
;
try
(
exploit
external_call_trace_length
;
eauto
;
check_safe
;
intro
T
;
des
);
ss
;
try
xomega
.
Qed.
End
MODSEM
.
Section
PROPS
.
Lemma
step_preserves_last_option
se
ge
st0
tr
st1
dummy_stack
(
STEP
:
step
se
ge
st0
tr
st1
)
(
LAST
:
last_option
(
get_stack
st0
) =
Some
dummy_stack
):
<<
LAST
:
last_option
(
get_stack
st1
) =
Some
dummy_stack
>>.
Proof.
r
in
STEP
.
des
.
inv
STEP0
;
ss
;
des_ifs
. Qed.
End
PROPS
.
Program
Definition
module
(
p
:
program
):
Mod.t
:=
{|
Mod.data
:=
p
;
Mod.get_sk
:=
Sk.of_program
fn_sig
;
Mod.get_modsem
:=
modsem
; |}.