Module AsmExtra
Require
Import
Skeleton
ModSem
.
Require
Import
Integers
.
Require
Import
CoqlibC
ValuesC
MemoryC
.
Require
Import
LocationsC
Conventions
AsmregsC
.
Require
Import
AsmC
StoreArguments
StoreArgumentsProps
.
Set
Implicit
Arguments
.
Lemma
loc_external_result_one
sg
:
is_one
(
loc_external_result
sg
)
.
Proof.
unfold
loc_external_result
.
generalize
(
loc_result_one
sg
);
i
.
destruct
(
loc_result
sg
)
eqn
:
T
;
ss
.
des
;
clarify
.
Qed.
Lemma
asm_initial_frame_succeed
(
asm
:
Asm.program
)
args
fptr
vs
m
skenv_link
fd
sg
(
ARGS
:
args
=
Args.Cstyle
fptr
vs
m
)
(
LEN
:
Datatypes.length
vs
=
Datatypes.length
(
sig_args
sg
))
(
SIZE
: 4 *
size_arguments
sg
<=
Ptrofs.max_unsigned
)
(
FPTR
:
Genv.find_funct
(
SkEnv.revive
(
SkEnv.project
skenv_link
(
Sk.of_program
fn_sig
asm
))
asm
)
fptr
=
Some
(
Internal
fd
))
(
SIG
:
fd
.(
fn_sig
) =
sg
)
(
CSTYLE
:
sg
.(
sig_cstyle
) =
true
)
:
exists
st_init
,
initial_frame
skenv_link
asm
args
st_init
.
Proof.
rewrite
<-
SIG
in
*.
exploit
store_arguments_progress
.
{
eapply
typify_has_type_list
;
eauto
. }
{
eauto
. }
i
.
des
.
instantiate
(1:=
m
)
in
STR
.
instantiate
(1:=0%
nat
)
in
PTRFREE
.
eexists
(
mkstate
_
(
Asm.State
_
_
)).
econs
;
try
apply
ARGS
;
ss
;
eauto
.
-
instantiate
(1:= ((
to_pregset
rs
) #
PC
<-
fptr
#
RSP
<- (
Vptr
(
Mem.nextblock
m
)
Ptrofs.zero
) #
RA
<-
Vnullptr
)).
ss
.
-
rewrite
Pregmap.gss
.
ii
.
clarify
.
-
repeat
(
rewrite
Pregmap.gso
; [|
clarify
;
fail
]).
eapply
Pregmap.gss
.
-
econs
;
eauto
.
-
econs
.
+
inv
STR
.
econs
;
eauto
.
eapply
extcall_arguments_same
;
eauto
.
i
.
unfold
to_mregset
,
to_pregset
,
Pregmap.set
,
to_preg
,
preg_of
.
des_ifs
;
ss
;
clarify
.
+
des_ifs
.
-
instantiate
(1:=0%
nat
).
i
.
unfold
Pregmap.set
,
to_pregset
in
PTR
.
des_ifs
;
eauto
.
+
exfalso
.
apply
PTR
.
ss
.
+
left
.
esplits
;
eauto
.
apply
NNPP
.
eauto
.
+
exfalso
.
apply
PTR
.
ss
.
Qed.
Lemma
asm_initial_frame_succeed_asmstyle
(
asm
:
Asm.program
)
args
rs
m
skenv_link
fd
(
ARGS
:
args
=
Args.Asmstyle
rs
m
)
(
FPTR
:
Genv.find_funct
(
SkEnv.revive
(
SkEnv.project
skenv_link
(
Sk.of_program
fn_sig
asm
))
asm
) (
rs
PC
) =
Some
(
Internal
fd
))
(
ASMSTYLE
:
fd
.(
fn_sig
).(
sig_cstyle
) =
false
)
:
exists
st_init
,
initial_frame
skenv_link
asm
args
st_init
.
Proof.
exists
(
AsmC.mkstate
(
rs
#
RA
<-
Vnullptr
) (
Asm.State
(
rs
#
RA
<-
Vnullptr
) (
JunkBlock.assign_junk_blocks
m
0%
nat
))).
econs
2;
eauto
;
ss
.
Qed.
Definition
set_regset
(
rs0
rs1
:
Mach.regset
) (
sg
:
signature
) (
mr
:
mreg
) :
val
:=
if
Loc.notin_dec
(
R
mr
) (
regs_of_rpairs
(
loc_arguments
sg
))
then
rs1
mr
else
rs0
mr
.
Definition
set_regset_undef
(
rs
:
Mach.regset
) (
sg
:
signature
) (
mr
:
mreg
) :
val
:=
if
Loc.notin_dec
(
R
mr
) (
regs_of_rpairs
(
loc_arguments
sg
))
then
Vundef
else
rs
mr
.