Module CsemC
Require
Import
CoqlibC
Maps
.
Require
Import
ASTC
Integers
ValuesC
Events
Memory
Globalenvs
.
Require
Import
Op
Registers
.
Require
Import
sflib
.
Require
Import
SmallstepC
.
newly added *
Require
Export
Simulation
Csem
CopC
Ctypes
Ctyping
Csyntax
.
Require
Import
Skeleton
Mod
ModSem
.
Require
Import
AsmregsC
CtypesC
.
Require
Import
Conventions
.
Require
Import
CtypingC
.
Set
Implicit
Arguments
.
Local
Obligation
Tactic
:=
ii
;
ss
;
des
;
do
2
inv_all_once
;
ss
;
clarify
.
Definition
is_call_cont_strong
(
k0
:
cont
):
Prop
:=
match
k0
with
|
Kcall
_
_
_
_
_
=>
True
|
_
=>
False
end
.
Definition
signature_of_function
(
fd
:
function
) :=
{|
sig_args
:=
map
typ_of_type
(
map
snd
(
fn_params
fd
));
sig_res
:=
opttyp_of_type
(
fn_return
fd
);
sig_cc
:=
fn_callconv
fd
;
sig_cstyle
:=
true
|}.
Definition
get_mem
(
st
:
state
):
option
mem
:=
match
st
with
|
State
_
_
_
_
m0
=>
Some
m0
|
ExprState
_
_
_
_
m0
=>
Some
m0
|
Callstate
_
_
_
_
m0
=>
Some
m0
|
Returnstate
_
_
m0
=>
Some
m0
|
Stuckstate
=>
None
end
.
Section
MODSEM
.
Variable
skenv_link
:
SkEnv.t
.
Variable
p
:
program
.
Let
skenv
:
SkEnv.t
:=
skenv_link
.(
SkEnv.project
)
p
.(
CSk.of_program
signature_of_function
).
Let
ce_ge
:
composite_env
:=
prog_comp_env
p
.
Let
ge_ge
:
Genv.t
fundef
type
:=
SkEnv.revive
skenv
p
.
Let
ge
:
genv
:=
Build_genv
ge_ge
ce_ge
.
Inductive
at_external
:
state
->
Args.t
->
Prop
:=
|
at_external_intro
fptr_arg
vs_arg
targs
tres
cconv
k0
m0
(
EXTERNAL
:
ge
.(
Genv.find_funct
)
fptr_arg
=
None
)
(
SIG
:
exists
skd
,
skenv_link
.(
Genv.find_funct
)
fptr_arg
=
Some
skd
/\
Some
(
signature_of_type
targs
tres
cconv
) =
Sk.get_csig
skd
)
(
CALL
:
is_call_cont_strong
k0
):
at_external
(
Callstate
fptr_arg
(
Tfunction
targs
tres
cconv
)
vs_arg
k0
m0
) (
Args.mk
fptr_arg
vs_arg
m0
).
Inductive
initial_frame
(
args
:
Args.t
):
state
->
Prop
:=
|
initial_frame_intro
fd
tyf
(
CSTYLE
:
Args.is_cstyle
args
)
(
FINDF
:
Genv.find_funct
ge
args
.(
Args.fptr
) =
Some
(
Internal
fd
))
(
TYPE
:
type_of_fundef
(
Internal
fd
) =
tyf
)
(
TYP
:
typecheck
args
.(
Args.vs
) (
type_of_params
(
fn_params
fd
))):
initial_frame
args
(
Callstate
args
.(
Args.fptr
)
tyf
args
.(
Args.vs
)
Kstop
args
.(
Args.m
)).
Inductive
final_frame
:
state
->
Retv.t
->
Prop
:=
|
final_frame_intro
v_ret
m_ret
:
final_frame
(
Returnstate
v_ret
Kstop
m_ret
) (
Retv.mk
v_ret
m_ret
).
Inductive
after_external
:
state
->
Retv.t
->
state
->
Prop
:=
|
after_external_intro
fptr_arg
vs_arg
m_arg
k
retv
tv
targs
tres
cconv
(
CSTYLE
:
Retv.is_cstyle
retv
)
(
TYP
:
typify_c
retv
.(
Retv.v
)
tres
tv
):
after_external
(
Callstate
fptr_arg
(
Tfunction
targs
tres
cconv
)
vs_arg
k
m_arg
)
retv
(
Returnstate
tv
k
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
;
|}.
Ltac
inv_single_events
:=
repeat
match
goal
with
| [
H
:
_
|-
_
] =>
try
(
exploit
external_call_trace_length
;
eauto
;
check_safe
;
intro
T
;
des
);
inv
H
;
ss
;
try
xomega
end
.
Lemma
single_events_at
:
forall
st
,
single_events_at
modsem
st
.
Proof.
ii
.
inv
H
.
-
inv
H0
;
ss
;
try
xomega
.
clear
-
H
.
inv_single_events
.
-
inv_single_events
.
Qed.
End
MODSEM
.
Section
MODULE
.
Variable
p
:
program
.
Program
Definition
module
:
Mod.t
:=
{|
Mod.data
:=
p
;
Mod.get_sk
:=
CSk.of_program
signature_of_function
;
Mod.get_modsem
:=
modsem
; |}.
End
MODULE
.
Inductive
typechecked
(
builtins
:
list
(
ident
*
globdef
(
Ctypes.fundef
function
)
type
)) (
p
:
program
):
Prop
:=
|
typechecked_intro
(
TYPCHECK
:
typecheck_program
p
=
Errors.OK
p
)
(
WT_EXTERNAL
:
forall
se
id
ef
args
res
cc
vargs
m
t
vres
m
',
In
(
id
,
Gfun
(
External
ef
args
res
cc
))
p
.(
prog_defs
) ->
external_call
ef
se
vargs
m
t
vres
m
' ->
wt_retval
vres
res
)
(
WF
:
Sk.wf
(
module
p
))
(
CSTYLE
:
forall
id
ef
tyargs
ty
cc
(
IN
:
In
(
id
, (
Gfun
(
Ctypes.External
ef
tyargs
ty
cc
)))
p
.(
prog_defs
)),
ef
.(
ef_sig
).(
sig_cstyle
))
(
BINCL
:
incl
builtins
p
.(
prog_defs
))
(
BCOMPLETE
:
forall
id
fd
(
IN
:
In
(
id
, (
Gfun
fd
))
p
.(
prog_defs
))
(
BUILTIN
: ~
is_external_fd
fd
),
In
(
id
,
Gfun
fd
)
builtins
)
.