Module MachC
Require
Import
CoqlibC
.
Require
Import
Maps
.
Require
Import
AST
.
Require
Import
Integers
.
Require
Import
ValuesC
.
Require
Import
MemoryC
.
Require
Import
Globalenvs
.
Require
Import
EventsC
.
Require
Import
Smallstep
.
Require
Import
Op
.
Require
Import
LocationsC
.
Require
Import
Conventions
.
Require
Stacklayout
.
newly added *
Require
Export
Mach
.
Require
Import
StoreArguments
.
Require
Import
Skeleton
Mod
ModSem
.
Require
Import
Simulation
Integers
.
Require
Import
JunkBlock
.
Set
Implicit
Arguments
.
Local
Obligation
Tactic
:=
ii
;
ss
;
des
;
inv_all_once
;
des
;
ss
;
clarify
;
eauto
with
congruence
.
Section
NEWSTEP
.
Variable
return_address_offset
:
function
->
code
->
ptrofs
->
Prop
.
Variable
se
:
Senv.t
.
Variable
ge
:
genv
.
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
:
Mach.step
return_address_offset
se
ge
st0
tr
st1
>> /\ <<
NOTDUMMY
:
st1
.(
get_stack
) <> []>>.
End
NEWSTEP
.
Hint
Unfold
step
.
Definition
locset_copy
(
diff
:
Z
) (
rs
:
Mach.regset
):
locset
:=
fun
loc
=>
match
loc
with
|
S
_
_
_
=>
Vundef
|
R
r
=>
match
rs
r
with
|
Vptr
blk
ofs
=>
Vptr
(
blk
.(
Zpos
) +
diff
).(
Z.to_pos
)
ofs
|
_
=>
rs
r
end
end
.
Hint
Unfold
locset_copy
.
Definition
get_mem
(
st
:
state
):
mem
:=
match
st
with
|
State
_
_
_
_
_
m0
=>
m0
|
Callstate
_
_
_
m0
=>
m0
|
Returnstate
_
_
m0
=>
m0
end
.
Section
MODSEM
.
Variable
rao
:
function
->
code
->
ptrofs
->
Prop
.
Hypothesis
rao_dtm
:
forall
f
c
ofs
ofs
',
rao
f
c
ofs
->
rao
f
c
ofs
' ->
ofs
=
ofs
'.
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
.
Record
state
:=
mkstate
{
init_rs
:
Mach.regset
;
init_sg
:
signature
;
st
:
Mach.state
;
}.
Inductive
at_external
:
state
->
Args.t
->
Prop
:=
|
at_external_intro
stack
rs
m0
m1
fptr
sg
vs
blk
ofs
init_rs
init_sg
(
EXTERNAL
:
Genv.find_funct
ge
fptr
=
None
)
(
SIG
:
exists
skd
,
skenv_link
.(
Genv.find_funct
)
fptr
=
Some
skd
/\
Sk.get_csig
skd
=
Some
sg
)
(
VALS
:
Mach.extcall_arguments
rs
m0
(
parent_sp
stack
)
sg
vs
)
(
ARGSRANGE
:
Ptrofs.unsigned
ofs
+ 4 *
size_arguments
sg
<=
Ptrofs.max_unsigned
)
(
RSP
: (
parent_sp
stack
) =
Vptr
blk
ofs
)
(
ALIGN
:
forall
chunk
(
CHUNK
:
size_chunk
chunk
<= 4 * (
size_arguments
sg
)),
(
align_chunk
chunk
|
ofs
.(
Ptrofs.unsigned
)))
(
FREE
:
Mem.free
m0
blk
ofs
.(
Ptrofs.unsigned
) (
ofs
.(
Ptrofs.unsigned
) + 4 * (
size_arguments
sg
)) =
Some
m1
):
at_external
(
mkstate
init_rs
init_sg
(
Callstate
stack
fptr
rs
m0
)) (
Args.mk
fptr
vs
m1
).
Inductive
initial_frame
(
args
:
Args.t
) :
state
->
Prop
:=
|
initial_frame_intro
fd
m0
rs
sg
ra
targs
n
m1
(
CSTYLE
:
Args.is_cstyle
args
/\
fd
.(
fn_sig
).(
sig_cstyle
) =
true
)
(
RAPTR
:
Val.has_type
ra
Tptr
)
(
SIG
:
sg
=
fd
.(
fn_sig
))
(
FINDF
:
Genv.find_funct
ge
args
.(
Args.fptr
) =
Some
(
Internal
fd
))
(
TYP
:
typecheck
args
.(
Args.vs
)
sg
targs
)
(
STORE
:
store_arguments
args
.(
Args.m
)
rs
targs
sg
m0
)
(
JUNK
:
assign_junk_blocks
m0
n
=
m1
)
(
PTRFREE
:
forall
mr
(
NOTIN
: ~
In
(
R
mr
) (
regs_of_rpairs
(
loc_arguments
sg
))),
<<
PTRFREE
:
is_junk_value
m0
m1
(
rs
mr
)>>):
initial_frame
args
(
mkstate
rs
sg
(
Callstate
[
dummy_stack
(
Vptr
args
.(
Args.m
).(
Mem.nextblock
)
Ptrofs.zero
)
ra
]
args
.(
Args.fptr
)
rs
m1
)).
Inductive
final_frame
:
state
->
Retv.t
->
Prop
:=
|
final_frame_intro
(
init_rs
rs
:
regset
)
init_sp
m0
m1
blk
init_sg
mr
ra
(
CALLEESAVE
:
forall
mr
,
Conventions1.is_callee_save
mr
->
Val.lessdef
(
init_rs
mr
) (
rs
mr
))
(
INITRSP
:
init_sp
=
Vptr
blk
Ptrofs.zero
)
(
FREE
:
Mem.free
m0
blk
0 (4 *
size_arguments
init_sg
) =
Some
m1
)
(
RETV
:
loc_result
init_sg
=
One
mr
):
final_frame
(
mkstate
init_rs
init_sg
(
Returnstate
[
dummy_stack
init_sp
ra
]
rs
m0
)) (
Retv.mk
(
rs
mr
)
m1
).
Inductive
after_external
:
state
->
Retv.t
->
state
->
Prop
:=
|
after_external_intro
init_rs
init_sg
stack
fptr
ls0
m0
ls1
m1
retv
sg
blk
ofs
(
CSTYLE
:
Retv.is_cstyle
retv
)
(
SIG
:
exists
skd
,
skenv_link
.(
Genv.find_funct
)
fptr
=
Some
skd
/\
Sk.get_csig
skd
=
Some
sg
)
(
REGSET
:
ls1
= (
set_pair
(
loc_result
sg
)
retv
.(
Retv.v
) (
regset_after_external
ls0
)))
(
RSP
: (
parent_sp
stack
) =
Vptr
blk
ofs
)
(
MEMWF
:
Ple
(
Senv.nextblock
skenv_link
)
retv
.(
Retv.m
).(
Mem.nextblock
))
(
UNFREE
:
Mem_unfree
retv
.(
Retv.m
)
blk
ofs
.(
Ptrofs.unsigned
) (
ofs
.(
Ptrofs.unsigned
) + 4 * (
size_arguments
sg
)) =
Some
m1
):
after_external
(
mkstate
init_rs
init_sg
(
Callstate
stack
fptr
ls0
m0
))
retv
(
mkstate
init_rs
init_sg
(
Returnstate
stack
ls1
m1
)).
Inductive
step
' (
se
:
Senv.t
) (
ge
:
genv
) (
st0
:
state
) (
tr
:
trace
) (
st1
:
state
):
Prop
:=
|
step
'
_intro
(
STEP
:
Mach.step
rao
se
ge
st0
.(
st
)
tr
st1
.(
st
))
(
INITRS
:
st0
.(
init_rs
) =
st1
.(
init_rs
))
(
INITFPTR
:
st0
.(
init_sg
) =
st1
.(
init_sg
))
(
NOTDUMMY
:
st1
.(
st
).(
get_stack
) <> []).
Lemma
extcall_arguments_dtm
rs
m
rsp
sg
vs0
vs1
(
ARGS0
:
Mach.extcall_arguments
rs
m
rsp
sg
vs0
)
(
ARGS1
:
Mach.extcall_arguments
rs
m
rsp
sg
vs1
):
vs0
=
vs1
.
Proof.
generalize
dependent
vs1
.
generalize
dependent
vs0
.
generalize
dependent
sg
.
assert
(
A
:
forall
l
v1
v2
,
Mach.extcall_arg
rs
m
rsp
l
v1
->
Mach.extcall_arg
rs
m
rsp
l
v2
->
v1
=
v2
).
{
intros
.
inv
H
;
inv
H0
;
congruence
. }
assert
(
B
:
forall
p
v1
v2
,
Mach.extcall_arg_pair
rs
m
rsp
p
v1
->
Mach.extcall_arg_pair
rs
m
rsp
p
v2
->
v1
=
v2
).
{
intros
.
inv
H
;
inv
H0
.
eapply
A
;
eauto
.
f_equal
;
eapply
A
;
eauto
. }
assert
(
C
:
forall
ll
vl1
,
list_forall2
(
Mach.extcall_arg_pair
rs
m
rsp
)
ll
vl1
->
forall
vl2
,
list_forall2
(
Mach.extcall_arg_pair
rs
m
rsp
)
ll
vl2
->
vl1
=
vl2
).
{
induction
1;
intros
vl2
EA
;
inv
EA
.
auto
.
f_equal
;
eauto
. }
intros
.
eapply
C
;
eauto
.
Qed.
Lemma
extcall_arguments_length
rs
m
rsp
sg
vs
(
ARGS
:
extcall_arguments
rs
m
rsp
sg
vs
):
length
(
loc_arguments
sg
) =
length
vs
.
Proof.
unfold
extcall_arguments
in
*.
abstr
(
loc_arguments
sg
)
locs
.
ginduction
vs
;
ii
;
inv
ARGS
;
ss
.
f_equal
.
erewrite
IHvs
;
eauto
.
Qed.
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
;
|}.
Next Obligation.
rewrite
RSP
in
*.
clarify
.
determ_tac
extcall_arguments_dtm
.
Qed.
Next Obligation.
inv
STEP
;
clarify
.
unfold
Genv.find_funct
in
*.
des_ifs_safe
ss
.
clarify
.
Qed.
Next Obligation.
inv
STEP
;
clarify
.
destruct
st1
;
ss
.
destruct
st0
;
ss
.
clarify
.
Qed.
Lemma
modsem_receptive
:
forall
st
,
receptive_at
modsem
st
.
Proof.
econs
;
eauto
.
-
ii
;
ss
.
inv
H
.
destruct
st0
;
ss
.
destruct
s1
;
ss
.
clarify
.
inv
STEP
;
try
(
exploit
external_call_receptive
;
eauto
;
check_safe
;
intro
T
;
des
);
try
by
(
inv_match_traces
; (
eexists
(
mkstate
_
_
_
);
econs
; [
econs
| | |];
eauto
)).
-
ii
.
inv
H
.
inv
STEP
;
try
(
exploit
external_call_trace_length
;
eauto
;
check_safe
;
intro
T
;
des
);
ss
;
try
xomega
.
Qed.
Lemma
modsem_determinate
:
forall
st
,
determinate_at
modsem
st
.
Proof.
econs
;
eauto
.
-
ii
;
ss
.
inv
H
;
inv
H0
.
destruct
st0
;
ss
.
destruct
s1
;
ss
.
destruct
s2
;
ss
.
clarify
.
inv
STEP
;
inv
STEP0
;
clarify_meq
;
try
(
determ_tac
rao_dtm
;
check_safe
);
try
(
determ_tac
extcall_arguments_dtm
;
check_safe
);
try
(
determ_tac
eval_builtin_args_determ
;
check_safe
);
try
(
determ_tac
external_call_determ
;
check_safe
);
esplits
;
eauto
;
try
(
econs
;
eauto
);
try
(
by
rewrite
Genv.find_funct_find_funct_ptr
in
*;
congruence
);
ii
;
eq_closure_tac
;
clarify_meq
.
-
ii
.
inv
H
.
inv
STEP
;
try
(
exploit
external_call_trace_length
;
eauto
;
check_safe
;
intro
T
;
des
);
ss
;
try
xomega
.
Qed.
End
MODSEM
.
Section
PROPS
.
Variable
rao
:
function
->
code
->
ptrofs
->
Prop
.
Lemma
lift_star
se
ge
st0
tr
st1
init_sg
init_rs
(
STAR
:
star
(
step
rao
)
se
ge
st0
tr
st1
):
star
(
step
'
rao
)
se
ge
(
mkstate
init_rs
init_sg
st0
)
tr
(
mkstate
init_rs
init_sg
st1
).
Proof.
ginduction
STAR
;
ii
;
ss
.
{
econs
;
et
. }
inv
H
.
econs
;
et
.
econs
;
et
.
Qed.
Lemma
lift_plus
se
ge
st0
tr
st1
init_sg
init_rs
(
PLUS
:
plus
(
step
rao
)
se
ge
st0
tr
st1
):
plus
(
step
'
rao
)
se
ge
(
mkstate
init_rs
init_sg
st0
)
tr
(
mkstate
init_rs
init_sg
st1
).
Proof.
inv
PLUS
.
inv
H
.
econs
;
et
.
{
instantiate
(1:=
mkstate
init_rs
init_sg
s2
).
econs
;
ss
;
et
. }
eapply
lift_star
;
et
.
Qed.
End
PROPS
.
Program
Definition
module
(
p
:
program
) (
rao
:
function
->
code
->
ptrofs
->
Prop
):
Mod.t
:=
{|
Mod.data
:=
p
;
Mod.get_sk
:=
Sk.of_program
fn_sig
;
Mod.get_modsem
:=
modsem
rao
; |}.