Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-IntrinSec
Commits
acaabc6c
Commit
acaabc6c
authored
Oct 29, 2020
by
Bernhard Schommer
Committed by
Xavier Leroy
Nov 06, 2020
Browse files
Added implementation for fmin/fmax for aarch64.
The two built-in function map to the fmax and fmin instruction. Bug 30035
parent
c3c7d3a4
Changes
3
Hide whitespace changes
Inline
Side-by-side
aarch64/Asm.v
View file @
acaabc6c
...
...
@@ -283,6 +283,8 @@ Inductive instruction: Type :=
|
Pfmsub
(
sz
:
fsize
)
(
rd
r1
r2
r3
:
freg
)
(
**
r
[
rd
=
r3
-
r1
*
r2
]
*
)
|
Pfnmadd
(
sz
:
fsize
)
(
rd
r1
r2
r3
:
freg
)
(
**
r
[
rd
=
-
r3
-
r1
*
r2
]
*
)
|
Pfnmsub
(
sz
:
fsize
)
(
rd
r1
r2
r3
:
freg
)
(
**
r
[
rd
=
-
r3
+
r1
*
r2
]
*
)
|
Pfmax
(
sz
:
fsize
)
(
rd
r1
r2
:
freg
)
(
**
r
maximum
*
)
|
Pfmin
(
sz
:
fsize
)
(
rd
r1
r2
:
freg
)
(
**
r
minimum
*
)
(
**
Floating
-
point
comparison
*
)
|
Pfcmp
(
sz
:
fsize
)
(
r1
r2
:
freg
)
(
**
r
compare
[
r1
]
and
[
r2
]
*
)
|
Pfcmp0
(
sz
:
fsize
)
(
r1
:
freg
)
(
**
r
compare
[
r1
]
and
[
+
0.0
]
*
)
...
...
@@ -1114,6 +1116,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
|
Pfmsub
_
_
_
_
_
|
Pfnmadd
_
_
_
_
_
|
Pfnmsub
_
_
_
_
_
|
Pfmax
_
_
_
_
|
Pfmin
_
_
_
_
|
Pnop
|
Pcfi_adjust
_
|
Pcfi_rel_offset
_
=>
...
...
aarch64/Asmexpand.ml
View file @
acaabc6c
...
...
@@ -363,6 +363,10 @@ let expand_builtin_inline name args res =
emit
(
Pfnmadd
(
D
,
res
,
a1
,
a2
,
a3
))
|
"__builtin_fnmsub"
,
[
BA
(
FR
a1
);
BA
(
FR
a2
);
BA
(
FR
a3
)]
,
BR
(
FR
res
)
->
emit
(
Pfnmsub
(
D
,
res
,
a1
,
a2
,
a3
))
|
"__builtin_fmax"
,
[
BA
(
FR
a1
);
BA
(
FR
a2
)]
,
BR
(
FR
res
)
->
emit
(
Pfmax
(
D
,
res
,
a1
,
a2
))
|
"__builtin_fmin"
,
[
BA
(
FR
a1
);
BA
(
FR
a2
)]
,
BR
(
FR
res
)
->
emit
(
Pfmin
(
D
,
res
,
a1
,
a2
))
(* Vararg *)
|
"__builtin_va_start"
,
[
BA
(
IR
a
)]
,
_
->
expand_builtin_va_start
a
...
...
aarch64/TargetPrinter.ml
View file @
acaabc6c
...
...
@@ -467,6 +467,10 @@ module Target : TARGET =
fprintf
oc
" fnmadd %a, %a, %a, %a
\n
"
freg
(
sz
,
rd
)
freg
(
sz
,
r1
)
freg
(
sz
,
r2
)
freg
(
sz
,
r3
)
|
Pfnmsub
(
sz
,
rd
,
r1
,
r2
,
r3
)
->
fprintf
oc
" fnmsub %a, %a, %a, %a
\n
"
freg
(
sz
,
rd
)
freg
(
sz
,
r1
)
freg
(
sz
,
r2
)
freg
(
sz
,
r3
)
|
Pfmax
(
sz
,
rd
,
r1
,
r2
)
->
fprintf
oc
" fmax %a, %a, %a
\n
"
freg
(
sz
,
rd
)
freg
(
sz
,
r1
)
freg
(
sz
,
r2
)
|
Pfmin
(
sz
,
rd
,
r1
,
r2
)
->
fprintf
oc
" fmin %a, %a, %a
\n
"
freg
(
sz
,
rd
)
freg
(
sz
,
r1
)
freg
(
sz
,
r2
)
(* Floating-point comparison *)
|
Pfcmp
(
sz
,
r1
,
r2
)
->
fprintf
oc
" fcmp %a, %a
\n
"
freg
(
sz
,
r1
)
freg
(
sz
,
r2
)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment