From 7cdd676d002e33015b496f609538a9e86d77c543 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 8 Aug 2019 11:18:38 +0200 Subject: AArch64 port This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. --- runtime/Makefile | 2 + runtime/aarch64/sysdeps.h | 45 +++++++++++++++++++ runtime/aarch64/vararg.S | 109 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 156 insertions(+) create mode 100644 runtime/aarch64/sysdeps.h create mode 100644 runtime/aarch64/vararg.S (limited to 'runtime') diff --git a/runtime/Makefile b/runtime/Makefile index 8fe00934..6777995d 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -22,6 +22,8 @@ ifeq ($(ARCH),x86_64) OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o else ifeq ($(ARCH),powerpc64) OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o +else ifeq ($(ARCH),aarch64) +OBJS=vararg.o else OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \ i64_shr.o i64_smod.o i64_stod.o i64_stof.o \ diff --git a/runtime/aarch64/sysdeps.h b/runtime/aarch64/sysdeps.h new file mode 100644 index 00000000..0cee9ae3 --- /dev/null +++ b/runtime/aarch64/sysdeps.h @@ -0,0 +1,45 @@ +// ***************************************************************** +// +// The Compcert verified compiler +// +// Xavier Leroy, Collège de France and INRIA Paris +// +// Copyright (c) Institut National de Recherche en Informatique et +// en Automatique. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are met: +// * Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// * Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// * Neither the name of the nor the +// names of its contributors may be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +// +// ********************************************************************* + +// System dependencies + +#define FUNCTION(f) \ + .text; \ + .balign 16; \ + .globl f; \ +f: + +#define ENDFUNCTION(f) \ + .type f, @function; .size f, . - f + diff --git a/runtime/aarch64/vararg.S b/runtime/aarch64/vararg.S new file mode 100644 index 00000000..b7347d65 --- /dev/null +++ b/runtime/aarch64/vararg.S @@ -0,0 +1,109 @@ +// ***************************************************************** +// +// The Compcert verified compiler +// +// Xavier Leroy, Collège de France and INRIA Paris +// +// Copyright (c) Institut National de Recherche en Informatique et +// en Automatique. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are met: +// * Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// * Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// * Neither the name of the nor the +// names of its contributors may be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +// +// ********************************************************************* + +// Helper functions for variadic functions . AArch64 version. + +#include "sysdeps.h" + +// typedef struct __va_list { +// void *__stack; // next stack parameter +// void *__gr_top; // top of the save area for int regs +// void *__vr_top; // top of the save area for float regs +// int__gr_offs; // offset from gr_top to next int reg +// int__vr_offs; // offset from gr_top to next FP reg +// } +// typedef struct __va_list va_list; // struct passed by reference +// unsigned int __compcert_va_int32(va_list * ap); +// unsigned long long __compcert_va_int64(va_list * ap); +// double __compcert_va_float64(va_list * ap); + +FUNCTION(__compcert_va_int32) + ldr w1, [x0, #24] // w1 = gr_offs + cbz w1, 1f + // gr_offs is not zero: load from int save area and update gr_offs + ldr x2, [x0, #8] // x2 = gr_top + ldr w2, [x2, w1, sxtw] // w2 = the next integer + add w1, w1, #8 + str w1, [x0, #24] // update gr_offs + mov w0, w2 + ret + // gr_offs is zero: load from stack save area and update stack pointer +1: ldr x1, [x0, #0] // x1 = stack + ldr w2, [x1, #0] // w2 = the next integer + add x1, x1, #8 + str x1, [x0, #0] // update stack + mov w0, w2 + ret +ENDFUNCTION(__compcert_va_int32) + +FUNCTION(__compcert_va_int64) + ldr w1, [x0, #24] // w1 = gr_offs + cbz w1, 1f + // gr_offs is not zero: load from int save area and update gr_offs + ldr x2, [x0, #8] // x2 = gr_top + ldr x2, [x2, w1, sxtw] // w2 = the next long integer + add w1, w1, #8 + str w1, [x0, #24] // update gr_offs + mov x0, x2 + ret + // gr_offs is zero: load from stack save area and update stack pointer +1: ldr x1, [x0, #0] // x1 = stack + ldr x2, [x1, #0] // w2 = the next long integer + add x1, x1, #8 + str x1, [x0, #0] // update stack + mov x0, x2 + ret +ENDFUNCTION(__compcert_va_int64) + +FUNCTION(__compcert_va_float64) + ldr w1, [x0, #28] // w1 = vr_offs + cbz w1, 1f + // vr_offs is not zero: load from float save area and update vr_offs + ldr x2, [x0, #16] // x2 = vr_top + ldr d0, [x2, w1, sxtw] // d0 = the next float + add w1, w1, #16 + str w1, [x0, #28] // update vr_offs + ret + // gr_offs is zero: load from stack save area and update stack pointer +1: ldr x1, [x0, #0] // x1 = stack + ldr d0, [x1, #0] // d0 = the next float + add x1, x1, #8 + str x1, [x0, #0] // update stack + ret +ENDFUNCTION(__compcert_va_float64) + +// Right now we pass structs by reference. This is not ABI conformant. +FUNCTION(__compcert_va_composite) + b __compcert_va_int64 +ENDFUNCTION(__compcert_va_composite) -- cgit From 4074a67434fc1f1a9bed7a896242faae25cd7fc2 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 9 Jan 2020 16:22:15 +0100 Subject: Fixing issue with and fabs --- runtime/include/math.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'runtime') diff --git a/runtime/include/math.h b/runtime/include/math.h index 060968c8..d6475df1 100644 --- a/runtime/include/math.h +++ b/runtime/include/math.h @@ -3,6 +3,8 @@ #define isfinite(__y) (fpclassify((__y)) >= FP_ZERO) +#include_next + #ifndef COMPCERT_NO_FP_MACROS #define fmin(x, y) __builtin_fmin((x),(y)) #define fmax(x, y) __builtin_fmax((x),(y)) @@ -14,5 +16,4 @@ #define fmaf(x, y, z) __builtin_fmaf((x),(y),(z)) #endif -#include_next #endif -- cgit From 0c25f714e690681c50420a218dad518fbecdb42a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 6 Feb 2020 11:48:30 +0100 Subject: Fixed using ccomp assembly preprocessor --- runtime/mppa_k1c/vararg.S | 54 ----------------------------------------------- runtime/mppa_k1c/vararg.s | 54 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+), 54 deletions(-) delete mode 100644 runtime/mppa_k1c/vararg.S create mode 100644 runtime/mppa_k1c/vararg.s (limited to 'runtime') diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S deleted file mode 100644 index 9e23e0b3..00000000 --- a/runtime/mppa_k1c/vararg.S +++ /dev/null @@ -1,54 +0,0 @@ - -// typedef void * va_list; -// unsigned int __compcert_va_int32(va_list * ap); -// unsigned long long __compcert_va_int64(va_list * ap); - - .text - .balign 2 - .globl __compcert_va_int32 -__compcert_va_int32: - ld $r32 = 0[$r0] # $r32 <- *ap -;; - addd $r32 = $r32, 8 # $r32 <- $r32 + WORDSIZE -;; - sd 0[$r0] = $r32 # *ap <- $r32 -;; - lws $r0 = -8[$r32] # retvalue <- 32-bits at *ap - WORDSIZE - ret -;; - - .text - .balign 2 - .globl __compcert_va_int64 - .globl __compcert_va_float64 - .globl __compcert_va_composite -__compcert_va_int64: -__compcert_va_float64: -# FIXME this assumes pass-by-reference -__compcert_va_composite: -# Prologue - ld $r32 = 0[$r0] # $r32 <- *ap -;; - addd $r32 = $r32, 8 # $r32 <- $r32 + WORDSIZE -;; - sd 0[$r0] = $r32 # *ap <- $r32 -;; - ld $r0 = -8[$r32] # retvalue <- 64-bits at *ap - WORDSIZE - ret -;; - -# FIXME this assumes pass-by-reference - .globl __compcert_acswapd -__compcert_acswapd: - acswapd 0[$r1] = $r2r3 - ;; - sq 0[$r0] = $r2r3 - ret - ;; - .globl __compcert_acswapw -__compcert_acswapw: - acswapw 0[$r1] = $r2r3 - ;; - sq 0[$r0] = $r2r3 - ret - ;; diff --git a/runtime/mppa_k1c/vararg.s b/runtime/mppa_k1c/vararg.s new file mode 100644 index 00000000..65c1eab8 --- /dev/null +++ b/runtime/mppa_k1c/vararg.s @@ -0,0 +1,54 @@ + +# typedef void * va_list; +# unsigned int __compcert_va_int32(va_list * ap); +# unsigned long long __compcert_va_int64(va_list * ap); + + .text + .balign 2 + .globl __compcert_va_int32 +__compcert_va_int32: + ld $r32 = 0[$r0] # $r32 <- *ap +;; + addd $r32 = $r32, 8 # $r32 <- $r32 + WORDSIZE +;; + sd 0[$r0] = $r32 # *ap <- $r32 +;; + lws $r0 = -8[$r32] # retvalue <- 32-bits at *ap - WORDSIZE + ret +;; + + .text + .balign 2 + .globl __compcert_va_int64 + .globl __compcert_va_float64 + .globl __compcert_va_composite +__compcert_va_int64: +__compcert_va_float64: +# FIXME this assumes pass-by-reference +__compcert_va_composite: +# Prologue + ld $r32 = 0[$r0] # $r32 <- *ap +;; + addd $r32 = $r32, 8 # $r32 <- $r32 + WORDSIZE +;; + sd 0[$r0] = $r32 # *ap <- $r32 +;; + ld $r0 = -8[$r32] # retvalue <- 64-bits at *ap - WORDSIZE + ret +;; + +# FIXME this assumes pass-by-reference + .globl __compcert_acswapd +__compcert_acswapd: + acswapd 0[$r1] = $r2r3 + ;; + sq 0[$r0] = $r2r3 + ret + ;; + .globl __compcert_acswapw +__compcert_acswapw: + acswapw 0[$r1] = $r2r3 + ;; + sq 0[$r0] = $r2r3 + ret + ;; -- cgit From 9a58ce92702efdca3cb756c9edd59596e293fba1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 8 Feb 2020 22:07:31 +0100 Subject: why did we remove the ppc runtime ?! --- runtime/powerpc/i64_dtos.s | 100 ++++++++++++++++++ runtime/powerpc/i64_dtou.s | 92 +++++++++++++++++ runtime/powerpc/i64_sar.s | 60 +++++++++++ runtime/powerpc/i64_sdiv.s | 71 +++++++++++++ runtime/powerpc/i64_shl.s | 64 ++++++++++++ runtime/powerpc/i64_shr.s | 65 ++++++++++++ runtime/powerpc/i64_smod.s | 70 +++++++++++++ runtime/powerpc/i64_smulh.s | 80 +++++++++++++++ runtime/powerpc/i64_stod.s | 67 ++++++++++++ runtime/powerpc/i64_stof.s | 68 ++++++++++++ runtime/powerpc/i64_udiv.s | 54 ++++++++++ runtime/powerpc/i64_udivmod.s | 234 ++++++++++++++++++++++++++++++++++++++++++ runtime/powerpc/i64_umod.s | 47 +++++++++ runtime/powerpc/i64_umulh.s | 65 ++++++++++++ runtime/powerpc/i64_utod.s | 66 ++++++++++++ runtime/powerpc/i64_utof.s | 64 ++++++++++++ runtime/powerpc/vararg.s | 163 +++++++++++++++++++++++++++++ 17 files changed, 1430 insertions(+) create mode 100644 runtime/powerpc/i64_dtos.s create mode 100644 runtime/powerpc/i64_dtou.s create mode 100644 runtime/powerpc/i64_sar.s create mode 100644 runtime/powerpc/i64_sdiv.s create mode 100644 runtime/powerpc/i64_shl.s create mode 100644 runtime/powerpc/i64_shr.s create mode 100644 runtime/powerpc/i64_smod.s create mode 100644 runtime/powerpc/i64_smulh.s create mode 100644 runtime/powerpc/i64_stod.s create mode 100644 runtime/powerpc/i64_stof.s create mode 100644 runtime/powerpc/i64_udiv.s create mode 100644 runtime/powerpc/i64_udivmod.s create mode 100644 runtime/powerpc/i64_umod.s create mode 100644 runtime/powerpc/i64_umulh.s create mode 100644 runtime/powerpc/i64_utod.s create mode 100644 runtime/powerpc/i64_utof.s create mode 100644 runtime/powerpc/vararg.s (limited to 'runtime') diff --git a/runtime/powerpc/i64_dtos.s b/runtime/powerpc/i64_dtos.s new file mode 100644 index 00000000..85c60b27 --- /dev/null +++ b/runtime/powerpc/i64_dtos.s @@ -0,0 +1,100 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Conversion from double float to signed long + + .balign 16 + .globl __compcert_i64_dtos +__compcert_i64_dtos: + stfdu f1, -16(r1) # extract LO (r4) and HI (r3) halves of double + lwz r3, 0(r1) + lwz r4, 4(r1) + addi r1, r1, 16 + srawi r10, r3, 31 # save sign of double in r10 + # extract unbiased exponent ((HI & 0x7FF00000) >> 20) - (1023 + 52) + rlwinm r5, r3, 12, 21, 31 + addi r5, r5, -1075 + # check range of exponent + cmpwi r5, -52 # if EXP < -52, abs(double) is < 1.0 + blt 1f + cmpwi r5, 11 # if EXP >= 63 - 52, abs(double) is >= 2^63 + bge 2f + # extract true mantissa + rlwinm r3, r3, 0, 12, 31 # HI &= ~0xFFF00000 + oris r3, r3, 0x10 # HI |= 0x00100000 + # shift it appropriately + cmpwi r5, 0 + blt 3f + # if EXP >= 0, shift left by EXP. Note that EXP < 11. + subfic r6, r5, 32 # r6 = 32 - EXP + slw r3, r3, r5 + srw r0, r4, r6 + or r3, r3, r0 + slw r4, r4, r5 + b 4f + # if EXP < 0, shift right by -EXP. Note that -EXP <= 52 but can be >= 32. +3: subfic r5, r5, 0 # r5 = -EXP = shift amount + subfic r6, r5, 32 # r6 = 32 - amount + addi r7, r5, -32 # r7 = amount - 32 (see i64_shr.s) + srw r4, r4, r5 + slw r0, r3, r6 + or r4, r4, r0 + srw r0, r3, r7 + or r4, r4, r0 + srw r3, r3, r5 + # apply sign to result +4: xor r4, r4, r10 + xor r3, r3, r10 + subfc r4, r10, r4 + subfe r3, r10, r3 + blr + # Special cases +1: li r3, 0 # result is 0 + li r4, 0 + blr +2: li r4, -1 # result is MAX_SINT or MIN_SINT + bge 5f # depending on sign + li r4, -1 # result is MAX_SINT = 0x7FFF_FFFF + srwi r3, r4, 1 + blr +5: lis r3, 0x8000 # result is MIN_SINT = 0x8000_0000 + li r4, 0 + blr + .type __compcert_i64_dtos, @function + .size __compcert_i64_dtos, .-__compcert_i64_dtos + \ No newline at end of file diff --git a/runtime/powerpc/i64_dtou.s b/runtime/powerpc/i64_dtou.s new file mode 100644 index 00000000..67a721d4 --- /dev/null +++ b/runtime/powerpc/i64_dtou.s @@ -0,0 +1,92 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Conversion from double float to unsigned long + + .balign 16 + .globl __compcert_i64_dtou +__compcert_i64_dtou: + stfdu f1, -16(r1) # extract LO (r4) and HI (r3) halves of double + lwz r3, 0(r1) + lwz r4, 4(r1) + addi r1, r1, 16 + cmpwi r3, 0 # is double < 0? + blt 1f # then it converts to 0 + # extract unbiased exponent ((HI & 0x7FF00000) >> 20) - (1023 + 52) + rlwinm r5, r3, 12, 21, 31 + addi r5, r5, -1075 + # check range of exponent + cmpwi r5, -52 # if EXP < -52, double is < 1.0 + blt 1f + cmpwi r5, 12 # if EXP >= 64 - 52, double is >= 2^64 + bge 2f + # extract true mantissa + rlwinm r3, r3, 0, 12, 31 # HI &= ~0xFFF00000 + oris r3, r3, 0x10 # HI |= 0x00100000 + # shift it appropriately + cmpwi r5, 0 + blt 3f + # if EXP >= 0, shift left by EXP. Note that EXP < 12. + subfic r6, r5, 32 # r6 = 32 - EXP + slw r3, r3, r5 + srw r0, r4, r6 + or r3, r3, r0 + slw r4, r4, r5 + blr + # if EXP < 0, shift right by -EXP. Note that -EXP <= 52 but can be >= 32. +3: subfic r5, r5, 0 # r5 = -EXP = shift amount + subfic r6, r5, 32 # r6 = 32 - amount + addi r7, r5, -32 # r7 = amount - 32 (see i64_shr.s) + srw r4, r4, r5 + slw r0, r3, r6 + or r4, r4, r0 + srw r0, r3, r7 + or r4, r4, r0 + srw r3, r3, r5 + blr + # Special cases +1: li r3, 0 # result is 0 + li r4, 0 + blr +2: li r3, -1 # result is MAX_UINT + li r4, -1 + blr + .type __compcert_i64_dtou, @function + .size __compcert_i64_dtou, .-__compcert_i64_dtou + + \ No newline at end of file diff --git a/runtime/powerpc/i64_sar.s b/runtime/powerpc/i64_sar.s new file mode 100644 index 00000000..c7da448f --- /dev/null +++ b/runtime/powerpc/i64_sar.s @@ -0,0 +1,60 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +# Shift right signed + + .balign 16 + .globl __compcert_i64_sar +__compcert_i64_sar: + andi. r5, r5, 63 # take amount modulo 64 + cmpwi r5, 32 + bge 1f # amount < 32? + subfic r6, r5, 32 # r6 = 32 - amount + srw r4, r4, r5 # RH = XH >>s amount + slw r0, r3, r6 # RL = XL >>u amount | XH << (32 - amount) + or r4, r4, r0 + sraw r3, r3, r5 + blr +1: addi r6, r5, -32 # amount >= 32 + sraw r4, r3, r6 # RL = XH >>s (amount - 32) + srawi r3, r3, 31 # RL = sign extension of XH + blr + .type __compcert_i64_sar, @function + .size __compcert_i64_sar, .-__compcert_i64_sar + + \ No newline at end of file diff --git a/runtime/powerpc/i64_sdiv.s b/runtime/powerpc/i64_sdiv.s new file mode 100644 index 00000000..9787ea3b --- /dev/null +++ b/runtime/powerpc/i64_sdiv.s @@ -0,0 +1,71 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Signed division + + .balign 16 + .globl __compcert_i64_sdiv +__compcert_i64_sdiv: + mflr r0 + stw r0, 4(r1) # save return address in caller's frame + xor r0, r3, r5 # compute sign of result (top bit) + mtctr r0 # save it in CTR (why not?) + srawi r0, r3, 31 # take absolute value of N + xor r4, r4, r0 # (i.e. N = N ^ r0 - r0, + xor r3, r3, r0 # where r0 = 0 if N >= 0 and r0 = -1 if N < 0) + subfc r4, r0, r4 + subfe r3, r0, r3 + srawi r0, r5, 31 # take absolute value of D + xor r6, r6, r0 # (same trick) + xor r5, r5, r0 + subfc r6, r0, r6 + subfe r5, r0, r5 + bl __compcert_i64_udivmod # do unsigned division + lwz r0, 4(r1) + mtlr r0 # restore return address + mfctr r0 + srawi r0, r0, 31 # apply expected sign to quotient + xor r6, r6, r0 # RES = Q if CTR >= 0, -Q if CTR < 0 + xor r5, r5, r0 + subfc r4, r0, r6 + subfe r3, r0, r5 + blr + .type __compcert_i64_sdiv, @function + .size __compcert_i64_sdiv, .-__compcert_i64_sdiv + + \ No newline at end of file diff --git a/runtime/powerpc/i64_shl.s b/runtime/powerpc/i64_shl.s new file mode 100644 index 00000000..f6edb6c2 --- /dev/null +++ b/runtime/powerpc/i64_shl.s @@ -0,0 +1,64 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +# Shift left + + .balign 16 + .globl __compcert_i64_shl +__compcert_i64_shl: +# On PowerPC, shift instructions with amount mod 64 >= 32 return 0 +# hi = (hi << amount) | (lo >> (32 - amount)) | (lo << (amount - 32)) +# lo = lo << amount +# if 0 <= amount < 32: +# (amount - 32) mod 64 >= 32, hence lo << (amount - 32) == 0 +# if 32 <= amount < 64: +# lo << amount == 0 +# (32 - amount) mod 64 >= 32, hence lo >> (32 - amount) == 0 + andi. r5, r5, 63 # take amount modulo 64 + subfic r6, r5, 32 # r6 = 32 - amount + addi r7, r5, -32 # r7 = amount - 32 + slw r3, r3, r5 + srw r0, r4, r6 + or r3, r3, r0 + slw r0, r4, r7 + or r3, r3, r0 + slw r4, r4, r5 + blr + .type __compcert_i64_shl, @function + .size __compcert_i64_shl, .-__compcert_i64_shl + \ No newline at end of file diff --git a/runtime/powerpc/i64_shr.s b/runtime/powerpc/i64_shr.s new file mode 100644 index 00000000..b634aafd --- /dev/null +++ b/runtime/powerpc/i64_shr.s @@ -0,0 +1,65 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +# Shift right unsigned + + .balign 16 + .globl __compcert_i64_shr +__compcert_i64_shr: +# On PowerPC, shift instructions with amount mod 64 >= 32 return 0 +# lo = (lo >> amount) | (hi << (32 - amount)) | (hi >> (amount - 32)) +# hi = hi >> amount +# if 0 <= amount < 32: +# (amount - 32) mod 64 >= 32, hence hi >> (amount - 32) == 0 +# if 32 <= amount < 64: +# hi >> amount == 0 +# (32 - amount) mod 64 >= 32, hence hi << (32 - amount) == 0 + andi. r5, r5, 63 # take amount modulo 64 + subfic r6, r5, 32 # r6 = 32 - amount + addi r7, r5, -32 # r7 = amount - 32 + srw r4, r4, r5 + slw r0, r3, r6 + or r4, r4, r0 + srw r0, r3, r7 + or r4, r4, r0 + srw r3, r3, r5 + blr + .type __compcert_i64_shr, @function + .size __compcert_i64_shr, .-__compcert_i64_shr + + \ No newline at end of file diff --git a/runtime/powerpc/i64_smod.s b/runtime/powerpc/i64_smod.s new file mode 100644 index 00000000..6b4e1f89 --- /dev/null +++ b/runtime/powerpc/i64_smod.s @@ -0,0 +1,70 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +## Signed remainder + + .balign 16 + .globl __compcert_i64_smod +__compcert_i64_smod: + mflr r0 + stw r0, 4(r1) # save return address in caller's frame + mtctr r3 # save sign of result in CTR (sign of N) + srawi r0, r3, 31 # take absolute value of N + xor r4, r4, r0 # (i.e. N = N ^ r0 - r0, + xor r3, r3, r0 # where r0 = 0 if N >= 0 and r0 = -1 if N < 0) + subfc r4, r0, r4 + subfe r3, r0, r3 + srawi r0, r5, 31 # take absolute value of D + xor r6, r6, r0 # (same trick) + xor r5, r5, r0 + subfc r6, r0, r6 + subfe r5, r0, r5 + bl __compcert_i64_udivmod # do unsigned division + lwz r0, 4(r1) + mtlr r0 # restore return address + mfctr r0 + srawi r0, r0, 31 # apply expected sign to remainder + xor r4, r4, r0 # RES = R if CTR >= 0, -Q if CTR < 0 + xor r3, r3, r0 + subfc r4, r0, r4 + subfe r3, r0, r3 + blr + .type __compcert_i64_smod, @function + .size __compcert_i64_smod, .-__compcert_i64_smod + + \ No newline at end of file diff --git a/runtime/powerpc/i64_smulh.s b/runtime/powerpc/i64_smulh.s new file mode 100644 index 00000000..73393fce --- /dev/null +++ b/runtime/powerpc/i64_smulh.s @@ -0,0 +1,80 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris +# +# Copyright (c) 2016 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Signed multiply-high + +# Hacker's Delight section 8.3: +# - compute high 64 bits of the unsigned product X * Y (see i64_umulh.S) +# - subtract X if Y < 0 +# - subtract Y if X < 0 + + .balign 16 + .globl __compcert_i64_smulh +__compcert_i64_smulh: +# r7:r8:r9 accumulate bits 127:32 of the full unsigned product + mulhwu r9, r4, r6 # r9 = high half of XL.YL + mullw r0, r4, r5 # r0 = low half of XL.YH + addc r9, r9, r0 + mulhwu r0, r4, r5 # r0 = high half of XL.YH + addze r8, r0 + mullw r0, r3, r6 # r0 = low half of XH.YL + addc r9, r9, r0 + mulhwu r0, r3, r6 # r0 = high half of XH.YL + adde r8, r8, r0 + li r7, 0 + addze r7, r7 + mullw r0, r3, r5 # r0 = low half of XH.YH + addc r8, r8, r0 + mulhwu r0, r3, r5 # r0 = high half of XH.YH + adde r7, r7, r0 +# Here r7:r8 contains the high 64 bits of the unsigned product. +# Now, test signs and subtract if needed + srawi r0, r3, 31 # r0 = -1 if X < 0, r0 = 0 if X >= 0 + srawi r9, r5, 31 # r9 = -1 if Y < 0, r9 = 0 if Y >= 0 + and r3, r3, r9 # set X = 0 if Y >= 0 + and r4, r4, r9 + and r5, r5, r0 # set Y = 0 if X >= 0 + and r6, r6, r0 + subfc r8, r4, r8 # subtract X + subfe r7, r3, r7 + subfc r4, r6, r8 # subtract Y + subfe r3, r5, r7 + blr + .type __compcert_i64_smulh, @function + .size __compcert_i64_smulh, .-__compcert_i64_smulh + diff --git a/runtime/powerpc/i64_stod.s b/runtime/powerpc/i64_stod.s new file mode 100644 index 00000000..0c1ab720 --- /dev/null +++ b/runtime/powerpc/i64_stod.s @@ -0,0 +1,67 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + +### Conversion from signed long to double float + + .balign 16 + .globl __compcert_i64_stod +__compcert_i64_stod: + addi r1, r1, -16 + lis r5, 0x4330 + li r6, 0 + stw r5, 0(r1) + stw r4, 4(r1) # 0(r1) = 2^52 + (double) XL + stw r5, 8(r1) + stw r6, 12(r1) # 8(r1) = 2^52 + lfd f1, 0(r1) + lfd f2, 8(r1) + fsub f1, f1, f2 # f1 is XL (unsigned) as a double + lis r5, 0x4530 + lis r6, 0x8000 + stw r5, 0(r1) # 0(r1) = 2^84 + ((double)XH - 2^31) * 2^32 + add r3, r3, r6 + stw r3, 4(r1) + stw r5, 8(r1) # 8(r1) = 2^84 + 2^31 * 2^32 + stw r6, 12(r1) + lfd f2, 0(r1) + lfd f3, 8(r1) + fsub f2, f2, f3 # f2 is XH (signed) * 2^32 as a double + fadd f1, f1, f2 # add both to get result + addi r1, r1, 16 + blr + .type __compcert_i64_stod, @function + .size __compcert_i64_stod, .-__compcert_i64_stod + diff --git a/runtime/powerpc/i64_stof.s b/runtime/powerpc/i64_stof.s new file mode 100644 index 00000000..97fa6bb8 --- /dev/null +++ b/runtime/powerpc/i64_stof.s @@ -0,0 +1,68 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Conversion from signed long to single float + + .balign 16 + .globl __compcert_i64_stof +__compcert_i64_stof: + mflr r9 + # Check whether -2^53 <= X < 2^53 + srawi r5, r3, 31 + srawi r6, r3, 21 # (r5,r6) = X >> 53 + addic r6, r6, 1 + addze r5, r5 # (r5,r6) = (X >> 53) + 1 + cmplwi r5, 2 + blt 1f + # X is large enough that double rounding can occur. + # Avoid it by nudging X away from the points where double rounding + # occurs (the "round to odd" technique) + rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF + # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r0 are 0 + or r4, r4, r0 # correct bit number 12 of X + rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X + # Convert to double, then round to single +1: bl __compcert_i64_stod + mtlr r9 + frsp f1, f1 + blr + .type __compcert_i64_stof, @function + .size __compcert_i64_stof, .-__compcert_i64_stof + diff --git a/runtime/powerpc/i64_udiv.s b/runtime/powerpc/i64_udiv.s new file mode 100644 index 00000000..e2da855a --- /dev/null +++ b/runtime/powerpc/i64_udiv.s @@ -0,0 +1,54 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Unsigned division + + .balign 16 + .globl __compcert_i64_udiv +__compcert_i64_udiv: + mflr r0 + stw r0, 4(r1) # save return address in caller's frame + bl __compcert_i64_udivmod # unsigned divide + lwz r0, 4(r1) + mtlr r0 # restore return address + mr r3, r5 # result = quotient + mr r4, r6 + blr + .type __compcert_i64_udiv, @function + .size __compcert_i64_udiv, .-__compcert_i64_udiv + diff --git a/runtime/powerpc/i64_udivmod.s b/runtime/powerpc/i64_udivmod.s new file mode 100644 index 00000000..e81c6cef --- /dev/null +++ b/runtime/powerpc/i64_udivmod.s @@ -0,0 +1,234 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +# Unsigned division and modulus + +# This function computes both the quotient and the remainder of two +# unsigned 64-bit integers. + +# Input: numerator N in (r3,r4), divisor D in (r5,r6) +# Output: quotient Q in (r5,r6), remainder R in (r3,r4) +# Destroys: all integer caller-save registers + + .globl __compcert_i64_udivmod + .balign 16 +__compcert_i64_udivmod: + cmplwi r5, 0 # DH == 0 ? + stwu r1, -32(r1) + mflr r0 + stw r0, 8(r1) + stw r31, 12(r1) + beq 1f +# The general case + stw r30, 16(r1) + stw r29, 20(r1) + stw r28, 24(r1) + mr r28, r3 # Save N in (r28, r29) + mr r29, r4 + mr r30, r5 # Save D in (r30, r31) + mr r31, r6 + # Scale N and D down, giving N' and D', such that 2^31 <= D' < 2^32 + cntlzw r7, r5 # r7 = leading zeros in DH = 32 - shift amount + subfic r8, r7, 32 # r8 = shift amount + slw r0, r3, r7 # N' = N >> shift amount + srw r3, r3, r8 + srw r4, r4, r8 + or r4, r4, r0 + slw r0, r5, r7 # D' = D >> shift amount + srw r6, r6, r8 + or r5, r6, r0 + # Divide N' by D' to get an approximate quotient Q + bl __compcert_i64_udiv6432 # r3 = quotient, r4 = remainder + mr r6, r3 # low half of quotient Q + li r5, 0 # high half of quotient is 0 + # Tentative quotient is either correct or one too high + # Compute Q * D in (r7, r8) +4: mullw r7, r6, r30 # r7 = Q * DH + mullw r8, r6, r31 # r8 = low 32 bits of Q * DL + mulhwu r0, r6, r31 # r0 = high 32 bits of Q * DL + addc r7, r7, r0 + subfe. r0, r0, r0 # test carry: EQ iff carry + beq 2f # handle overflow case + # Compute R = N - Q * D, with borrow + subfc r4, r8, r29 + subfe r3, r7, r28 + subfe. r0, r0, r0 # test borrow: EQ iff no borrow + beq 3f # no borrow: N >= Q * D, we are good + addi r6, r6, -1 # borrow: adjust Q down by 1 + addc r4, r4, r31 # and R up by D + adde r3, r3, r30 + # Finished +3: lwz r0, 8(r1) + mtlr r0 + lwz r31, 12(r1) + lwz r30, 16(r1) + lwz r29, 20(r1) + lwz r28, 24(r1) + addi r1, r1, 32 + blr + # Special case when Q * D overflows +2: addi r6, r6, -1 # adjust Q down by 1 + b 4b # and redo computation and check of remainder + .balign 16 +# Special case 64 bits divided by 32 bits +1: cmplwi r3, 0 # NH == 0? + beq 4f + divwu r31, r3, r6 # Divide NH by DL, quotient QH in r31 + mullw r0, r31, r6 + subf r3, r0, r3 # NH is remainder of this division + mr r5, r6 + bl __compcert_i64_udiv6432 # divide NH : NL by DL + mr r5, r31 # high word of quotient + mr r6, r3 # low word of quotient + # r4 contains low word of remainder + li r3, 0 # high word of remainder = 0 + lwz r0, 8(r1) + mtlr r0 + lwz r31, 12(r1) + addi r1, r1, 32 + blr + .balign 16 +# Special case 32 bits divided by 32 bits +4: mr r0, r6 + divwu r6, r4, r6 # low word of quotient + li r5, 0 # high word of quotient is 0 + mullw r0, r6, r0 + subf r4, r0, r4 # low word of remainder + li r3, 0 # high word of remainder is 0 + addi r1, r1, 32 + blr + + .type __compcert_i64_udivmod, @function + .size __compcert_i64_udivmod, .-__compcert_i64_udivmod + +# Auxiliary division function: 64 bit integer divided by 32 bit integer +# Not exported +# Input: numerator N in (r3,r4), divisor D in r5 +# Output: quotient Q in r3, remainder R in r4 +# Destroys: all integer caller-save registers +# Assumes: high word of N is less than D + + .balign 16 +__compcert_i64_udiv6432: +# Algorithm 9.3 from Hacker's Delight, section 9.4 +# Initially: u1 in r3, u0 in r4, v in r5 +# s = __builtin_clz(v); + cntlzw r6, r5 # s in r6 +# v = v << s; + slw r5, r5, r6 +# vn1 = v >> 16; # vn1 in r7 + srwi r7, r5, 16 +# vn0 = v & 0xFFFF; # vn0 in r8 + rlwinm r8, r5, 0, 16, 31 +# un32 = (u1 << s) | (u0 >> 32 - s); + subfic r0, r6, 32 + srw r0, r4, r0 + slw r3, r3, r6 # u1 dies, un32 in r3 + or r3, r3, r0 +# un10 = u0 << s; + slw r4, r4, r6 # u0 dies, un10 in r4 +# un1 = un10 >> 16; + srwi r9, r4, 16 # un1 in r9 +# un0 = un10 & 0xFFFF; + rlwinm r4, r4, 0, 16, 31 # un10 dies, un0 in r4 +# q1 = un32/vn1; + divwu r10, r3, r7 # q in r10 +# rhat = un32 - q1*vn1; + mullw r0, r10, r7 + subf r11, r0, r3 # rhat in r11 +# again1: +1: +# if (q1 >= b || q1*vn0 > b*rhat + un1) { + cmplwi r10, 0xFFFF + bgt 2f + mullw r0, r10, r8 + slwi r12, r11, 16 + add r12, r12, r9 + cmplw r0, r12 + ble 3f +2: +# q1 = q1 - 1; + addi r10, r10, -1 +# rhat = rhat + vn1; + add r11, r11, r7 +# if (rhat < b) goto again1;} + cmplwi r11, 0xFFFF + ble 1b +3: +# un21 = un32*b + un1 - q1*v; + slwi r0, r3, 16 # un32 dies + add r9, r0, r9 # un1 dies + mullw r0, r10, r5 + subf r9, r0, r9 # un21 in r9 +# q0 = un21/vn1; + divwu r3, r9, r7 # q0 in r3 +# rhat = un21 - q0*vn1; + mullw r0, r3, r7 + subf r11, r0, r9 # rhat in r11 +# again2: +4: +# if (q0 >= b || q0*vn0 > b*rhat + un0) { + cmplwi r3, 0xFFFF + bgt 5f + mullw r0, r3, r8 + slwi r12, r11, 16 + add r12, r12, r4 + cmplw r0, r12 + ble 6f +5: +# q0 = q0 - 1; + addi r3, r3, -1 +# rhat = rhat + vn1; + add r11, r11, r7 +# if (rhat < b) goto again2;} + cmplwi r11, 0xFFFF + ble 4b +6: +# remainder = (un21*b + un0 - q0*v) >> s; + slwi r0, r9, 16 + add r4, r0, r4 # un0 dies, remainder in r4 + mullw r0, r3, r5 + subf r4, r0, r4 + srw r4, r4, r6 +# quotient = q1*b + q0; + slwi r0, r10, 16 + add r3, r0, r3 + blr + + .type __compcert_i64_udiv6432, @function + .size __compcert_i64_udiv6432,.-__compcert_i64_udiv6432 diff --git a/runtime/powerpc/i64_umod.s b/runtime/powerpc/i64_umod.s new file mode 100644 index 00000000..bf8d6121 --- /dev/null +++ b/runtime/powerpc/i64_umod.s @@ -0,0 +1,47 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Unsigned modulus + + .balign 16 + .globl __compcert_i64_umod +__compcert_i64_umod: + b __compcert_i64_udivmod + .type __compcert_i64_umod, @function + .size __compcert_i64_umod, .-__compcert_i64_umod + diff --git a/runtime/powerpc/i64_umulh.s b/runtime/powerpc/i64_umulh.s new file mode 100644 index 00000000..53b72948 --- /dev/null +++ b/runtime/powerpc/i64_umulh.s @@ -0,0 +1,65 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris +# +# Copyright (c) 2016 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Unsigned multiply-high + +# X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL + + .balign 16 + .globl __compcert_i64_umulh +__compcert_i64_umulh: +# r7:r8:r9 accumulate bits 127:32 of the full product + mulhwu r9, r4, r6 # r9 = high half of XL.YL + mullw r0, r4, r5 # r0 = low half of XL.YH + addc r9, r9, r0 + mulhwu r0, r4, r5 # r0 = high half of XL.YH + addze r8, r0 + mullw r0, r3, r6 # r0 = low half of XH.YL + addc r9, r9, r0 + mulhwu r0, r3, r6 # r0 = high half of XH.YL + adde r8, r8, r0 + li r7, 0 + addze r7, r7 + mullw r0, r3, r5 # r0 = low half of XH.YH + addc r4, r8, r0 + mulhwu r0, r3, r5 # r0 = high half of XH.YH + adde r3, r7, r0 + blr + .type __compcert_i64_umulh, @function + .size __compcert_i64_umulh, .-__compcert_i64_umulh + diff --git a/runtime/powerpc/i64_utod.s b/runtime/powerpc/i64_utod.s new file mode 100644 index 00000000..69de6fdb --- /dev/null +++ b/runtime/powerpc/i64_utod.s @@ -0,0 +1,66 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Conversion from unsigned long to double float + + .balign 16 + .globl __compcert_i64_utod +__compcert_i64_utod: + addi r1, r1, -16 + lis r5, 0x4330 + li r6, 0 + stw r5, 0(r1) + stw r4, 4(r1) # 0(r1) = 2^52 + (double) XL + stw r5, 8(r1) + stw r6, 12(r1) # 8(r1) = 2^52 + lfd f1, 0(r1) + lfd f2, 8(r1) + fsub f1, f1, f2 # f1 is (double) XL + lis r5, 0x4530 + stw r5, 0(r1) # 0(r1) = 2^84 + (double) XH * 2^32 + stw r3, 4(r1) + stw r5, 8(r1) # 8(r1) = 2^84 + lfd f2, 0(r1) + lfd f3, 8(r1) + fsub f2, f2, f3 # f2 is XH * 2^32 as a double + fadd f1, f1, f2 # add both to get result + addi r1, r1, 16 + blr + .type __compcert_i64_utod, @function + .size __compcert_i64_utod, .-__compcert_i64_utod + diff --git a/runtime/powerpc/i64_utof.s b/runtime/powerpc/i64_utof.s new file mode 100644 index 00000000..cdb2f867 --- /dev/null +++ b/runtime/powerpc/i64_utof.s @@ -0,0 +1,64 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Conversion from unsigned long to single float + + .balign 16 + .globl __compcert_i64_utof +__compcert_i64_utof: + mflr r9 + # Check whether X < 2^53 + andis. r0, r3, 0xFFE0 # test bits 53...63 of X + beq 1f + # X is large enough that double rounding can occur. + # Avoid it by nudging X away from the points where double rounding + # occurs (the "round to odd" technique) + rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF + # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r0 are 0 + or r4, r4, r0 # correct bit number 12 of X + rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X + # Convert to double, then round to single +1: bl __compcert_i64_utod + mtlr r9 + frsp f1, f1 + blr + .type __compcert_i64_utof, @function + .size __compcert_i64_utof, .-__compcert_i64_utof + diff --git a/runtime/powerpc/vararg.s b/runtime/powerpc/vararg.s new file mode 100644 index 00000000..8d7e62c8 --- /dev/null +++ b/runtime/powerpc/vararg.s @@ -0,0 +1,163 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for variadic functions . IA32 version + +# typedef struct { +# unsigned char ireg; // index of next integer register +# unsigned char freg; // index of next FP register +# char * stk; // pointer to next argument in stack +# struct { +# int iregs[8]; +# double fregs[8]; +# } * regs; // pointer to saved register area +# } va_list[1]; +# +# unsigned int __compcert_va_int32(va_list ap); +# unsigned long long __compcert_va_int64(va_list ap); +# double __compcert_va_float64(va_list ap); + + .text + + .balign 16 + .globl __compcert_va_int32 +__compcert_va_int32: + # r3 = ap = address of va_list structure + lbz r4, 0(r3) # r4 = ap->ireg = next integer register + cmplwi r4, 8 + bge 1f + # Next argument was passed in an integer register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4 + addi r4, r4, 1 # increment ap->ireg + stb r4, 0(r3) + lwzx r3, r5, r6 # load argument in r3 + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + addi r5, r5, 4 # advance ap->stk by 4 + stw r5, 4(r3) + lwz r3, -4(r5) # load argument in r3 + blr + .type __compcert_va_int32, @function + .size __compcert_va_int32, .-__compcert_va_int32 + + .balign 16 + .globl __compcert_va_int64 +__compcert_va_int64: + # r3 = ap = address of va_list structure + lbz r4, 0(r3) # r4 = ap->ireg = next integer register + cmplwi r4, 7 + bge 1f + # Next argument was passed in two consecutive integer register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + addi r4, r4, 3 # round r4 up to an even number and add 2 + rlwinm r4, r4, 0, 0, 30 + rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4 + add r5, r5, r6 # r5 = address of argument + 8 + stb r4, 0(r3) # update ap->ireg + lwz r3, -8(r5) # load argument in r3:r4 + lwz r4, -4(r5) + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + li r4, 8 + stb r4, 0(r3) # set ap->ireg = 8 so that no ireg is left + addi r5, r5, 15 # round r5 to a multiple of 8 and add 8 + rlwinm r5, r5, 0, 0, 28 + stw r5, 4(r3) # update ap->stk + lwz r3, -8(r5) # load argument in r3:r4 + lwz r4, -4(r5) + blr + .type __compcert_va_int64, @function + .size __compcert_va_int64, .-__compcert_va_int64 + + .balign 16 + .globl __compcert_va_float64 +__compcert_va_float64: + # r3 = ap = address of va_list structure + lbz r4, 1(r3) # r4 = ap->freg = next float register + cmplwi r4, 8 + bge 1f + # Next argument was passed in a FP register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + rlwinm r6, r4, 3, 0, 28 # r6 = r4 * 8 + add r5, r5, r6 + lfd f1, 32(r5) # load argument in f1 + addi r4, r4, 1 # increment ap->freg + stb r4, 1(r3) + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + addi r5, r5, 15 # round r5 to a multiple of 8 and add 8 + rlwinm r5, r5, 0, 0, 28 + lfd f1, -8(r5) # load argument in f1 + stw r5, 4(r3) # update ap->stk + blr + .type __compcert_va_float64, @function + .size __compcert_va_float64, .-__compcert_va_int64 + + .balign 16 + .globl __compcert_va_composite +__compcert_va_composite: + b __compcert_va_int32 + .type __compcert_va_composite, @function + .size __compcert_va_composite, .-__compcert_va_composite + +# Save integer and FP registers at beginning of vararg function + + .balign 16 + .globl __compcert_va_saveregs +__compcert_va_saveregs: + lwz r11, 0(r1) # r11 point to top of our frame + stwu r3, -96(r11) # register save area is 96 bytes below + stw r4, 4(r11) + stw r5, 8(r11) + stw r6, 12(r11) + stw r7, 16(r11) + stw r8, 20(r11) + stw r9, 24(r11) + stw r10, 28(r11) + bf 6, 1f # don't save FP regs if CR6 bit is clear + stfd f1, 32(r11) + stfd f2, 40(r11) + stfd f3, 48(r11) + stfd f4, 56(r11) + stfd f5, 64(r11) + stfd f6, 72(r11) + stfd f7, 80(r11) + stfd f8, 88(r11) +1: blr + .type __compcert_va_saveregs, @function + .size __compcert_va_saveregs, .-__compcert_va_saveregs -- cgit From 6d3118ad9eec104e8ed0bb86a3f5100d20224fd2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 9 Feb 2020 21:43:51 +0100 Subject: bringing back the ppc64 runtime --- runtime/powerpc64/i64_dtou.s | 66 ++++++++++++++++++ runtime/powerpc64/i64_stof.s | 68 ++++++++++++++++++ runtime/powerpc64/i64_utod.s | 79 +++++++++++++++++++++ runtime/powerpc64/i64_utof.s | 64 +++++++++++++++++ runtime/powerpc64/vararg.s | 163 +++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 440 insertions(+) create mode 100644 runtime/powerpc64/i64_dtou.s create mode 100644 runtime/powerpc64/i64_stof.s create mode 100644 runtime/powerpc64/i64_utod.s create mode 100644 runtime/powerpc64/i64_utof.s create mode 100644 runtime/powerpc64/vararg.s (limited to 'runtime') diff --git a/runtime/powerpc64/i64_dtou.s b/runtime/powerpc64/i64_dtou.s new file mode 100644 index 00000000..e58bcfaf --- /dev/null +++ b/runtime/powerpc64/i64_dtou.s @@ -0,0 +1,66 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Conversion from double float to unsigned long + + .balign 16 + .globl __compcert_i64_dtou +__compcert_i64_dtou: + lis r0, 0x5f00 # 0x5f00_0000 = 2^63 in binary32 format + stwu r0, -16(r1) + lfs f2, 0(r1) # f2 = 2^63 + fcmpu cr0, f1, f2 # crbit 0 is f1 < f2 + bf 0, 1f # branch if f1 >= 2^63 (or f1 is NaN) + fctidz f1, f1 # convert as signed + stfd f1, 0(r1) + lwz r3, 0(r1) + lwz r4, 4(r1) + addi r1, r1, 16 + blr +1: fsub f1, f1, f2 # shift argument down by 2^63 + fctidz f1, f1 # convert as signed + stfd f1, 0(r1) + lwz r3, 0(r1) + lwz r4, 4(r1) + addis r3, r3, 0x8000 # shift result up by 2^63 + addi r1, r1, 16 + blr + .type __compcert_i64_dtou, @function + .size __compcert_i64_dtou, .-__compcert_i64_dtou + + diff --git a/runtime/powerpc64/i64_stof.s b/runtime/powerpc64/i64_stof.s new file mode 100644 index 00000000..779cbc18 --- /dev/null +++ b/runtime/powerpc64/i64_stof.s @@ -0,0 +1,68 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Conversion from signed long to single float + + .balign 16 + .globl __compcert_i64_stof +__compcert_i64_stof: + rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 + # Check whether -2^53 <= X < 2^53 + sradi r5, r4, 53 + addi r5, r5, 1 + cmpldi r5, 2 + blt 1f + # X is large enough that double rounding can occur. + # Avoid it by nudging X away from the points where double rounding + # occurs (the "round to odd" technique) + rldicl r5, r4, 0, 53 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-63 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X + rldicr r4, r4, 0, 52 # set to 0 bits 0 to 11 of X + # Convert to double, then round to single +1: stdu r4, -16(r1) + lfd f1, 0(r1) + fcfid f1, f1 + frsp f1, f1 + addi r1, r1, 16 + blr + .type __compcert_i64_stof, @function + .size __compcert_i64_stof, .-__compcert_i64_stof + diff --git a/runtime/powerpc64/i64_utod.s b/runtime/powerpc64/i64_utod.s new file mode 100644 index 00000000..491ee26b --- /dev/null +++ b/runtime/powerpc64/i64_utod.s @@ -0,0 +1,79 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + + .text + +### Conversion from unsigned long to double float + + .balign 16 + .globl __compcert_i64_utod +__compcert_i64_utod: + rldicl r3, r3, 0, 32 # clear top 32 bits + rldicl r4, r4, 0, 32 # clear top 32 bits + lis r5, 0x4f80 # 0x4f80_0000 = 2^32 in binary32 format + stdu r3, -32(r1) + std r4, 8(r1) + stw r5, 16(r1) + lfd f1, 0(r1) # high 32 bits of argument + lfd f2, 8(r1) # low 32 bits of argument + lfs f3, 16(r1) # 2^32 + fcfid f1, f1 # convert both 32-bit halves to FP (exactly) + fcfid f2, f2 + fmadd f1, f1, f3, f2 # compute hi * 2^32 + lo + addi r1, r1, 32 + blr + .type __compcert_i64_utod, @function + .size __compcert_i64_utod, .-__compcert_i64_utod + +# Alternate implementation using round-to-odd: +# rldimi r4, r3, 32, 0 # reassemble (r3,r4) as a 64-bit integer in r4 +# cmpdi r4, 0 # is r4 >= 2^63 ? +# blt 1f +# stdu r4, -16(r1) # r4 < 2^63: convert as signed +# lfd f1, 0(r1) +# fcfid f1, f1 +# addi r1, r1, 16 +# blr +#1: rldicl r0, r4, 0, 63 # extract low bit of r4 +# srdi r4, r4, 1 +# or r4, r4, r0 # round r4 to 63 bits, using round-to-odd +# stdu r4, -16(r1) # convert to binary64 +# lfd f1, 0(r1) +# fcfid f1, f1 +# fadd f1, f1, f1 # multiply result by 2 +# addi r1, r1, 16 +# blr + \ No newline at end of file diff --git a/runtime/powerpc64/i64_utof.s b/runtime/powerpc64/i64_utof.s new file mode 100644 index 00000000..cdb2f867 --- /dev/null +++ b/runtime/powerpc64/i64_utof.s @@ -0,0 +1,64 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for 64-bit integer arithmetic. PowerPC version. + + .text + +### Conversion from unsigned long to single float + + .balign 16 + .globl __compcert_i64_utof +__compcert_i64_utof: + mflr r9 + # Check whether X < 2^53 + andis. r0, r3, 0xFFE0 # test bits 53...63 of X + beq 1f + # X is large enough that double rounding can occur. + # Avoid it by nudging X away from the points where double rounding + # occurs (the "round to odd" technique) + rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF + # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r0 are 0 + or r4, r4, r0 # correct bit number 12 of X + rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X + # Convert to double, then round to single +1: bl __compcert_i64_utod + mtlr r9 + frsp f1, f1 + blr + .type __compcert_i64_utof, @function + .size __compcert_i64_utof, .-__compcert_i64_utof + diff --git a/runtime/powerpc64/vararg.s b/runtime/powerpc64/vararg.s new file mode 100644 index 00000000..8d7e62c8 --- /dev/null +++ b/runtime/powerpc64/vararg.s @@ -0,0 +1,163 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for variadic functions . IA32 version + +# typedef struct { +# unsigned char ireg; // index of next integer register +# unsigned char freg; // index of next FP register +# char * stk; // pointer to next argument in stack +# struct { +# int iregs[8]; +# double fregs[8]; +# } * regs; // pointer to saved register area +# } va_list[1]; +# +# unsigned int __compcert_va_int32(va_list ap); +# unsigned long long __compcert_va_int64(va_list ap); +# double __compcert_va_float64(va_list ap); + + .text + + .balign 16 + .globl __compcert_va_int32 +__compcert_va_int32: + # r3 = ap = address of va_list structure + lbz r4, 0(r3) # r4 = ap->ireg = next integer register + cmplwi r4, 8 + bge 1f + # Next argument was passed in an integer register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4 + addi r4, r4, 1 # increment ap->ireg + stb r4, 0(r3) + lwzx r3, r5, r6 # load argument in r3 + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + addi r5, r5, 4 # advance ap->stk by 4 + stw r5, 4(r3) + lwz r3, -4(r5) # load argument in r3 + blr + .type __compcert_va_int32, @function + .size __compcert_va_int32, .-__compcert_va_int32 + + .balign 16 + .globl __compcert_va_int64 +__compcert_va_int64: + # r3 = ap = address of va_list structure + lbz r4, 0(r3) # r4 = ap->ireg = next integer register + cmplwi r4, 7 + bge 1f + # Next argument was passed in two consecutive integer register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + addi r4, r4, 3 # round r4 up to an even number and add 2 + rlwinm r4, r4, 0, 0, 30 + rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4 + add r5, r5, r6 # r5 = address of argument + 8 + stb r4, 0(r3) # update ap->ireg + lwz r3, -8(r5) # load argument in r3:r4 + lwz r4, -4(r5) + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + li r4, 8 + stb r4, 0(r3) # set ap->ireg = 8 so that no ireg is left + addi r5, r5, 15 # round r5 to a multiple of 8 and add 8 + rlwinm r5, r5, 0, 0, 28 + stw r5, 4(r3) # update ap->stk + lwz r3, -8(r5) # load argument in r3:r4 + lwz r4, -4(r5) + blr + .type __compcert_va_int64, @function + .size __compcert_va_int64, .-__compcert_va_int64 + + .balign 16 + .globl __compcert_va_float64 +__compcert_va_float64: + # r3 = ap = address of va_list structure + lbz r4, 1(r3) # r4 = ap->freg = next float register + cmplwi r4, 8 + bge 1f + # Next argument was passed in a FP register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + rlwinm r6, r4, 3, 0, 28 # r6 = r4 * 8 + add r5, r5, r6 + lfd f1, 32(r5) # load argument in f1 + addi r4, r4, 1 # increment ap->freg + stb r4, 1(r3) + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + addi r5, r5, 15 # round r5 to a multiple of 8 and add 8 + rlwinm r5, r5, 0, 0, 28 + lfd f1, -8(r5) # load argument in f1 + stw r5, 4(r3) # update ap->stk + blr + .type __compcert_va_float64, @function + .size __compcert_va_float64, .-__compcert_va_int64 + + .balign 16 + .globl __compcert_va_composite +__compcert_va_composite: + b __compcert_va_int32 + .type __compcert_va_composite, @function + .size __compcert_va_composite, .-__compcert_va_composite + +# Save integer and FP registers at beginning of vararg function + + .balign 16 + .globl __compcert_va_saveregs +__compcert_va_saveregs: + lwz r11, 0(r1) # r11 point to top of our frame + stwu r3, -96(r11) # register save area is 96 bytes below + stw r4, 4(r11) + stw r5, 8(r11) + stw r6, 12(r11) + stw r7, 16(r11) + stw r8, 20(r11) + stw r9, 24(r11) + stw r10, 28(r11) + bf 6, 1f # don't save FP regs if CR6 bit is clear + stfd f1, 32(r11) + stfd f2, 40(r11) + stfd f3, 48(r11) + stfd f4, 56(r11) + stfd f5, 64(r11) + stfd f6, 72(r11) + stfd f7, 80(r11) + stfd f8, 88(r11) +1: blr + .type __compcert_va_saveregs, @function + .size __compcert_va_saveregs, .-__compcert_va_saveregs -- cgit From b46cdc3ade397a57a7b748946fb58e16e95bf42b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 27 Mar 2020 16:53:59 +0100 Subject: fix broken test Makefile fix math.h so that it does special things only on K1C --- runtime/include/math.h | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'runtime') diff --git a/runtime/include/math.h b/runtime/include/math.h index d6475df1..01b8d8d8 100644 --- a/runtime/include/math.h +++ b/runtime/include/math.h @@ -1,6 +1,8 @@ #ifndef _COMPCERT_MATH_H #define _COMPCERT_MATH_H +#ifdef __K1C__ + #define isfinite(__y) (fpclassify((__y)) >= FP_ZERO) #include_next @@ -16,4 +18,9 @@ #define fmaf(x, y, z) __builtin_fmaf((x),(y),(z)) #endif +#else + +#include_next + +#endif #endif -- cgit From f1abe04e503f1c54c5a50f7b3f3906beca15a760 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 29 Mar 2020 11:20:01 +0200 Subject: Double rounding error in int64->float32 conversions on PowerPC and ARM The "stof" and "utof" runtime functions contain a round-to-odd step that avoids double rounding. However, this step was incorrectly coded on PowerPC (stof and utof), PowerPC64 (utof), and ARM (stof), making round-to-odd ineffective and causing double rounding. Closes: #343 --- runtime/arm/i64_stof.S | 9 ++++----- runtime/powerpc/i64_stof.s | 17 ++++++++--------- runtime/powerpc/i64_utof.s | 10 +++++----- runtime/powerpc64/i64_utof.s | 10 +++++----- 4 files changed, 22 insertions(+), 24 deletions(-) (limited to 'runtime') diff --git a/runtime/arm/i64_stof.S b/runtime/arm/i64_stof.S index bcfa471c..11e00a2a 100644 --- a/runtime/arm/i64_stof.S +++ b/runtime/arm/i64_stof.S @@ -39,12 +39,11 @@ @@@ Conversion from signed 64-bit integer to single float FUNCTION(__compcert_i64_stof) - @ Check whether -2^53 <= X < 2^53 - ASR r2, Reg0HI, #21 - ASR r3, Reg0HI, #31 @ (r2,r3) = X >> 53 + @ Check whether -2^53 <= X < 2^53 + ASR r2, Reg0HI, #21 @ r2 = high 32 bits of X >> 53 + @ -2^53 <= X < 2^53 iff r2 is -1 or 0, that is, iff r2 + 1 is 0 or 1 adds r2, r2, #1 - adc r3, r3, #0 @ (r2,r3) = X >> 53 + 1 - cmp r3, #2 + cmp r2, #2 blo 1f @ X is large enough that double rounding can occur. @ Avoid it by nudging X away from the points where double rounding diff --git a/runtime/powerpc/i64_stof.s b/runtime/powerpc/i64_stof.s index 97fa6bb8..ea23a1c8 100644 --- a/runtime/powerpc/i64_stof.s +++ b/runtime/powerpc/i64_stof.s @@ -43,20 +43,19 @@ __compcert_i64_stof: mflr r9 # Check whether -2^53 <= X < 2^53 - srawi r5, r3, 31 - srawi r6, r3, 21 # (r5,r6) = X >> 53 - addic r6, r6, 1 - addze r5, r5 # (r5,r6) = (X >> 53) + 1 + srawi r5, r3, 21 # r5 = high 32 bits of X >> 53 + # -2^53 <= X < 2^53 iff r5 is -1 or 0, that is, iff r5 + 1 is 0 or 1 + addi r5, r5, 1 cmplwi r5, 2 blt 1f # X is large enough that double rounding can occur. # Avoid it by nudging X away from the points where double rounding # occurs (the "round to odd" technique) - rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X - addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF - # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise - # bits 13-31 of r0 are 0 - or r4, r4, r0 # correct bit number 12 of X + rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X # Convert to double, then round to single 1: bl __compcert_i64_stod diff --git a/runtime/powerpc/i64_utof.s b/runtime/powerpc/i64_utof.s index cdb2f867..4a2a172b 100644 --- a/runtime/powerpc/i64_utof.s +++ b/runtime/powerpc/i64_utof.s @@ -48,11 +48,11 @@ __compcert_i64_utof: # X is large enough that double rounding can occur. # Avoid it by nudging X away from the points where double rounding # occurs (the "round to odd" technique) - rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X - addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF - # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise - # bits 13-31 of r0 are 0 - or r4, r4, r0 # correct bit number 12 of X + rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X # Convert to double, then round to single 1: bl __compcert_i64_utod diff --git a/runtime/powerpc64/i64_utof.s b/runtime/powerpc64/i64_utof.s index cdb2f867..4a2a172b 100644 --- a/runtime/powerpc64/i64_utof.s +++ b/runtime/powerpc64/i64_utof.s @@ -48,11 +48,11 @@ __compcert_i64_utof: # X is large enough that double rounding can occur. # Avoid it by nudging X away from the points where double rounding # occurs (the "round to odd" technique) - rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X - addi r0, r0, 0x7FF # r0 = (X & 0x7FF) + 0x7FF - # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise - # bits 13-31 of r0 are 0 - or r4, r4, r0 # correct bit number 12 of X + rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X + addi r5, r5, 0x7FF # r5 = (X & 0x7FF) + 0x7FF + # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise + # bits 13-31 of r5 are 0 + or r4, r4, r5 # correct bit number 12 of X rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X # Convert to double, then round to single 1: bl __compcert_i64_utod -- cgit