Module MutrecB
Require
Import
AST
Coqlib
.
Require
Import
Asm
.
Require
Import
sflib
.
Require
Import
AsmC
Mod
.
Require
Import
MutrecHeader
Integers
.
Definition
_memoized
:
ident
:= 60%
positive
.
Definition
lb0
:
label
:= 1%
positive
.
Definition
lb1
:
label
:= 2%
positive
.
Definition
lb2
:
label
:= 3%
positive
.
Definition
v_memoized
:= {|
gvar_info
:=
tt
;
gvar_init
:= (
Init_int32
(
Int.zero
) ::
Init_int32
(
Int.zero
) ::
nil
);
gvar_readonly
:=
false
;
gvar_volatile
:=
false
|}.
Definition
code
:
list
instruction
:=
[
Pallocframe
24 (
Ptrofs.repr
16)
Ptrofs.zero
;
Pmov_mr_a
(
Addrmode
(
Some
RSP
)
None
(
inl
8))
RBX
;
Pmov_rr
RBX
RDI
;
Ptestl_rr
RBX
RBX
;
Pjcc
Cond_ne
lb0
;
Pxorl_r
RAX
;
Pjmp_l
lb1
;
Plabel
lb0
;
Pmovl_rm
RAX
(
Addrmode
None
None
(
inr
(
_memoized
,
Ptrofs.zero
)));
Pcmpl_rr
RBX
RAX
;
Pjcc
Cond_e
lb2
;
Pleal
RDI
(
Addrmode
(
Some
RBX
)
None
(
inl
(- 1)));
Pcall_s
f_id
(
mksignature
[
Tint
] (
Some
Tint
)
cc_default
true
);
Pleal
RAX
(
Addrmode
(
Some
RAX
) (
Some
(
RBX
, 1)) (
inl
0));
Pmovl_mr
(
Addrmode
None
None
(
inr
(
_memoized
,
Ptrofs.zero
)))
RBX
;
Pmovl_mr
(
Addrmode
None
None
(
inr
(
_memoized
,
Ptrofs.repr
4)))
RAX
;
Pjmp_l
lb1
;
Plabel
lb2
;
Pmovl_rm
RAX
(
Addrmode
None
None
(
inr
(
_memoized
,
Ptrofs.repr
4)));
Plabel
lb1
;
Pmov_rm_a
RBX
(
Addrmode
(
Some
RSP
)
None
(
inl
8));
Pfreeframe
24 (
Ptrofs.repr
16)
Ptrofs.zero
;
Pret
].
Definition
func_g
:
function
:=
mkfunction
(
mksignature
[
Tint
] (
Some
Tint
)
cc_default
true
)
code
.
Definition
global_definitions
:
list
(
ident
*
globdef
fundef
unit
) :=
((
f_id
,
Gfun
(
External
(
EF_external
"
f
"
(
mksignature
(
AST.Tint
::
nil
) (
Some
AST.Tint
)
cc_default
true
)))) :: (
_memoized
,
Gvar
v_memoized
) ::
(
g_id
,
Gfun
(
Internal
func_g
)) ::
nil
).
Definition
public_idents
:
list
ident
:=
(
f_id
::
g_id
::
nil
).
Definition
prog
:
program
:=
mkprogram
global_definitions
public_idents
main_id
.
Definition
md
:
Mod.t
:=
AsmC.module
prog
.