Module Sem
Require
Import
Maps
.
Require
Import
AST
.
Require
Import
Integers
.
Require
Import
Values
.
Require
Import
Memory
.
Require
Import
Events
.
Require
Import
Smallstep
.
Require
Import
GlobalenvsC
.
Require
Import
LinkingC
.
Require
Import
CoqlibC
.
Require
Import
sflib
.
Require
Import
ModSem
Mod
Skeleton
System
.
Require
Export
Syntax
.
Set
Implicit
Arguments
.
Module
Frame
.
Record
t
:
Type
:=
mk
{
ms
:
ModSem.t
;
st
:
ms
.(
ModSem.state
);
}.
Definition
update_st
(
fr0
:
t
) (
st0
:
fr0
.(
ms
).(
ModSem.state
)):
t
:= (
mk
fr0
.(
ms
)
st0
).
End
Frame
.
Module
Ge
.
Definition
t
:
Type
:= (
list
ModSem.t
*
SkEnv.t
).
Inductive
find_fptr_owner
(
ge
:
t
) (
fptr
:
val
) (
ms
:
ModSem.t
):
Prop
:=
|
find_fptr_owner_intro
(
MODSEM
:
In
ms
ge
.(
fst
))
if_sig
(
INTERNAL
:
Genv.find_funct
ms
.(
ModSem.skenv
)
fptr
=
Some
(
Internal
if_sig
)).
Inductive
disjoint
(
ge
:
t
):
Prop
:=
|
disjoint_intro
(
DISJOINT
:
forall
fptr
ms0
ms1
(
FIND0
:
ge
.(
find_fptr_owner
)
fptr
ms0
)
(
FIND1
:
ge
.(
find_fptr_owner
)
fptr
ms1
),
ms0
=
ms1
).
End
Ge
.
Inductive
state
:
Type
:=
|
Callstate
(
args
:
Args.t
)
(
frs
:
list
Frame.t
)
|
State
(
frs
:
list
Frame.t
).
Inductive
step
(
ge
:
Ge.t
):
state
->
trace
->
state
->
Prop
:=
|
step_call
fr0
frs
args
(
AT
:
fr0
.(
Frame.ms
).(
ModSem.at_external
)
fr0
.(
Frame.st
)
args
):
step
ge
(
State
(
fr0
::
frs
))
E0
(
Callstate
args
(
fr0
::
frs
))
|
step_init
args
frs
ms
st_init
(
MSFIND
:
ge
.(
Ge.find_fptr_owner
)
args
.(
Args.get_fptr
)
ms
)
(
INIT
:
ms
.(
ModSem.initial_frame
)
args
st_init
):
step
ge
(
Callstate
args
frs
)
E0
(
State
((
Frame.mk
ms
st_init
) ::
frs
))
|
step_internal
fr0
frs
tr
st0
(
STEP
:
Step
(
fr0
.(
Frame.ms
))
fr0
.(
Frame.st
)
tr
st0
):
step
ge
(
State
(
fr0
::
frs
))
tr
(
State
((
fr0
.(
Frame.update_st
)
st0
) ::
frs
))
|
step_return
fr0
fr1
frs
retv
st0
(
FINAL
:
fr0
.(
Frame.ms
).(
ModSem.final_frame
)
fr0
.(
Frame.st
)
retv
)
(
AFTER
:
fr1
.(
Frame.ms
).(
ModSem.after_external
)
fr1
.(
Frame.st
)
retv
st0
):
step
ge
(
State
(
fr0
::
fr1
::
frs
))
E0
(
State
((
fr1
.(
Frame.update_st
)
st0
) ::
frs
)).
Section
SEMANTICS
.
Variable
p
:
program
.
Definition
link_sk
:
option
Sk.t
:=
link_list
(
List.map
Mod.sk
p
).
Definition
skenv_fill_internals
(
skenv
:
SkEnv.t
):
SkEnv.t
:=
skenv
.(
Genv_map_defs
) (
fun
_
gd
=>
Some
match
gd
with
|
Gfun
(
External
ef
) => (
Gfun
(
Internal
ef
.(
ef_sig
)))
|
Gfun
_
=>
gd
|
Gvar
gv
=>
gd
end
).
Definition
load_system
(
skenv
:
SkEnv.t
): (
ModSem.t
*
SkEnv.t
) :=
(
System.modsem
skenv
,
skenv
.(
skenv_fill_internals
)).
Definition
load_modsems
(
skenv
:
SkEnv.t
):
list
ModSem.t
:=
List.map
((
flip
Mod.modsem
)
skenv
)
p
.
Definition
load_genv
(
init_skenv
:
SkEnv.t
):
Ge.t
:=
let
(
system
,
skenv
) :=
load_system
init_skenv
in
(
system
:: (
load_modsems
init_skenv
),
init_skenv
).
Inductive
initial_state
:
state
->
Prop
:=
|
initial_state_intro
sk_link
skenv_link
m_init
fptr_init
(
INITSK
:
link_sk
=
Some
sk_link
)
(
INITSKENV
:
sk_link
.(
Sk.load_skenv
) =
skenv_link
)
(
INITMEM
:
sk_link
.(
Sk.load_mem
) =
Some
m_init
)
(
FPTR
:
fptr_init
= (
Genv.symbol_address
skenv_link
sk_link
.(
prog_main
)
Ptrofs.zero
))
(
SIG
:
skenv_link
.(
Genv.find_funct
)
fptr_init
=
Some
(
Internal
signature_main
))
(
WF
:
forall
md
(
IN
:
In
md
p
), <<
WF
:
Sk.wf
md
>>):
initial_state
(
Callstate
(
Args.mk
fptr_init
[]
m_init
) []).
Inductive
final_state
:
state
->
int
->
Prop
:=
|
final_state_intro
fr0
retv
i
(
FINAL
:
fr0
.(
Frame.ms
).(
ModSem.final_frame
)
fr0
.(
Frame.st
)
retv
)
(
INT
:
retv
.(
Retv.v
) =
Vint
i
):
final_state
(
State
[
fr0
])
i
.
Definition
sem
:
semantics
:=
(
Semantics_gen
(
fun
_
=>
step
)
initial_state
final_state
(
match
link_sk
with
|
Some
sk_link
=>
load_genv
sk_link
.(
Sk.load_skenv
)
|
None
=> (
nil
,
SkEnv.empty
)
end
)
(
match
link_sk
with
|
Some
sk_link
=>
sk_link
.(
Sk.load_skenv
)
|
None
=>
SkEnv.empty
end
)).
End
SEMANTICS
.
Hint
Unfold
link_sk
load_modsems
load_genv
.