Module StoreArguments
Require
Import
CoqlibC
.
Require
Import
Maps
.
Require
Import
AST
.
Require
Import
Integers
.
Require
Import
ValuesC
.
Require
Import
MemoryC
.
Require
Import
Globalenvs
.
Require
Import
Events
.
Require
Import
Smallstep
.
Require
Import
Op
.
Require
Import
LocationsC
.
Require
Import
Conventions
.
Require
Stacklayout
.
newly added *
Require
Import
Mach
.
Definition
only_args
(
m
:
mem
) (
blk
:
block
) (
lo
:
ptrofs
) (
locs
:
list
loc
) :=
forall
ofs
,
(<<
UNDEF
:
ZMap.get
ofs
(
Mem.mem_contents
m
) !!
blk
=
Undef
>>) \/
(<<
INARGS
:
exists
ofs0
ty
v
,
(<<
IN
:
In
(
S
Outgoing
ofs0
ty
)
locs
>>) /\
(<<
RANGE
: 4 *
ofs0
<=
ofs
< 4 *
ofs0
+
size_chunk
(
chunk_of_type
ty
)>>) /\
(<<
LOAD
:
Mem.loadv
(
chunk_of_type
ty
)
m
(
Val.offset_ptr
(
Vptr
blk
lo
) (
Ptrofs.repr
(
Stacklayout.fe_ofs_arg
+ 4 *
ofs0
)))
=
Some
v
>>) /\
(<<
VDEF
:
v
<>
Vundef
>>)>>).
Inductive
store_arguments
(
m0
:
mem
) (
rs
:
Mach.regset
) (
vs
:
list
val
) (
sg
:
signature
) (
m2
:
mem
):
Prop
:=
|
store_arguments_intro
m1
blk
(
ALC
:
Mem.alloc
m0
0 (4 *
size_arguments
sg
) = (
m1
,
blk
))
(
VALS
:
extcall_arguments
rs
m2
(
Vptr
blk
Ptrofs.zero
)
sg
vs
)
(
ONLYARGS
:
only_args
m2
blk
Ptrofs.zero
(
regs_of_rpairs
(
loc_arguments
sg
)))
(
UNCH
:
Mem.unchanged_on
(
fun
b
ofs
=>
if
eq_block
b
blk
then
~ (0 <=
ofs
< 4 *
size_arguments
sg
)
else
True
)
m1
m2
)
(
NB
:
m1
.(
Mem.nextblock
) =
m2
.(
Mem.nextblock
))
(
PERM
:
Mem.range_perm
m2
blk
0 (4 *
size_arguments
sg
)
Cur
Freeable
).