diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-10-29 18:10:16 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-11-06 18:30:21 +0100 |
| commit | acaabc6c481cc70e5597ccb74052a7f6d330b0f1 (patch) | |
| tree | 38e7b9f6a25282ffc089261a8400bd646125192a /aarch64 | |
| parent | c3c7d3a417b37bf7268562c20a27916ae0c51adf (diff) | |
| download | compcert-kvx-acaabc6c481cc70e5597ccb74052a7f6d330b0f1.tar.gz compcert-kvx-acaabc6c481cc70e5597ccb74052a7f6d330b0f1.zip | |
Added implementation for fmin/fmax for aarch64.
The two built-in function map to the fmax and fmin instruction.
Bug 30035
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asm.v | 4 | ||||
| -rw-r--r-- | aarch64/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | aarch64/TargetPrinter.ml | 4 |
3 files changed, 12 insertions, 0 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 79232783..5ac577b1 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -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 _ => diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index ea2ee703..1ba754dd 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -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 diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index fec05cc6..78b9eb2a 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -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) |