aboutsummaryrefslogtreecommitdiffstats
path: root/x86/NeedOp.v
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2022-02-07 15:10:54 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-02-07 15:12:20 +0100
commit38b0425d524cd3e7260ac46e13153f007e8bc00d (patch)
tree987d9d3c42c6b0d7873115ec00fcdd99a714d7b5 /x86/NeedOp.v
parent87de3969856cf6a5eb5e1615ec817a015ed90d1c (diff)
downloadcompcert-kvx-38b0425d524cd3e7260ac46e13153f007e8bc00d.tar.gz
compcert-kvx-38b0425d524cd3e7260ac46e13153f007e8bc00d.zip
Add op for float max and min for x86.
The ops `Omaxf` and `Ominf` have the same semantics as `minsd` and `maxsd` instruction, i.e. if both arguments are equal the second argument is returned as well as for NaN. The operations are the used in SelectOp to implement the built-in function `__builtin_fmax` and `__builtin_fmin`. Bug 32640
Diffstat (limited to 'x86/NeedOp.v')
-rw-r--r--x86/NeedOp.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/x86/NeedOp.v b/x86/NeedOp.v
index 775a23db..9c7469e9 100644
--- a/x86/NeedOp.v
+++ b/x86/NeedOp.v
@@ -113,7 +113,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Ororlimm _ => op1 (default nv)
| Oleal addr => needs_of_addressing_64 addr nv
| Onegf | Oabsf => op1 (default nv)
- | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
+ | Oaddf | Osubf | Omulf | Odivf | Omaxf | Ominf => op2 (default nv)
| Onegfs | Oabsfs => op1 (default nv)
| Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
| Osingleoffloat | Ofloatofsingle => op1 (default nv)