From 5b7fc96afb149ad916a9bf5015fe1eb2e0baaa7c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 17 May 2019 17:30:03 +0200 Subject: Prepend $(DESTDIR) to the installation target (#169) Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs. --- runtime/Makefile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'runtime') diff --git a/runtime/Makefile b/runtime/Makefile index 27ad6e8c..8fe00934 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -70,16 +70,16 @@ clean:: ifeq ($(strip $(HAS_RUNTIME_LIB)),true) install:: - install -d $(LIBDIR) - install -m 0644 $(LIB) $(LIBDIR) + install -d $(DESTDIR)$(LIBDIR) + install -m 0644 $(LIB) $(DESTDIR)$(LIBDIR) else install:: endif ifeq ($(strip $(HAS_STANDARD_HEADERS)),true) install:: - install -d $(LIBDIR)/include - install -m 0644 $(INCLUDES) $(LIBDIR)/include + install -d $(DESTDIR)$(LIBDIR)/include + install -m 0644 $(INCLUDES) $(DESTDIR)$(LIBDIR)/include else install:: endif -- cgit From 36e64ee96ded0c94c83da6fb12202c276e66ba45 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 3 Jun 2019 14:59:53 +0200 Subject: use all same exact include files --- runtime/mppa_k1c/i64_sdiv.c | 22 +++++++--------------- 1 file changed, 7 insertions(+), 15 deletions(-) (limited to 'runtime') diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c index 892aac07..60269cae 100644 --- a/runtime/mppa_k1c/i64_sdiv.c +++ b/runtime/mppa_k1c/i64_sdiv.c @@ -10,27 +10,19 @@ int i32_sdiv (int a, int b) return __divdi3 (a, b); } -#ifdef __K1C_COS__ -#include -#define K1_SFR_CS_IO_MASK COS_SFR_CS_IO_MASK -#define K1_SFR_CS_DZ_MASK COS_SFR_CS_DZ_MASK -#define K1_SFR_CS_OV_MASK COS_SFR_CS_OV_MASK -#define K1_SFR_CS_UN_MASK COS_SFR_CS_UN_MASK -#define K1_SFR_CS_IN_MASK COS_SFR_CS_IN_MASK -#define K1_SFR_CS COS_SFR_CS -#else -#include -#endif +#ifdef OUR_OWN_FE_EXCEPT +#include <../../k1-cos/include/hal/cos_registers.h> /* DM FIXME this is for floating point */ int fetestexcept(int excepts) { - int mask = (K1_SFR_CS_IO_MASK | K1_SFR_CS_DZ_MASK | K1_SFR_CS_OV_MASK | K1_SFR_CS_UN_MASK | K1_SFR_CS_IN_MASK) & excepts; - unsigned long long cs = __builtin_k1_get(K1_SFR_CS); + int mask = (COS_SFR_CS_IO_MASK | COS_SFR_CS_DZ_MASK | COS_SFR_CS_OV_MASK | COS_SFR_CS_UN_MASK | COS_SFR_CS_IN_MASK) & excepts; + unsigned long long cs = __builtin_k1_get(COS_SFR_CS); return cs & mask; } int feclearexcept(int excepts) { - int mask = (K1_SFR_CS_IO_MASK | K1_SFR_CS_DZ_MASK | K1_SFR_CS_OV_MASK | K1_SFR_CS_UN_MASK | K1_SFR_CS_IN_MASK) & excepts; - __builtin_k1_wfxl(K1_SFR_CS, mask); + int mask = (COS_SFR_CS_IO_MASK | COS_SFR_CS_DZ_MASK | COS_SFR_CS_OV_MASK | COS_SFR_CS_UN_MASK | COS_SFR_CS_IN_MASK) & excepts; + __builtin_k1_wfxl(COS_SFR_CS, mask); return 0; } +#endif -- cgit 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 a114da2cc9f6caca4824582eea75ec91b8439cc7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 28 Aug 2019 22:51:21 +0200 Subject: merge upstream including fma fixes --- 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 ----------------------------- 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 ----------------------------- 22 files changed, 1870 deletions(-) delete mode 100644 runtime/powerpc/i64_dtos.s delete mode 100644 runtime/powerpc/i64_dtou.s delete mode 100644 runtime/powerpc/i64_sar.s delete mode 100644 runtime/powerpc/i64_sdiv.s delete mode 100644 runtime/powerpc/i64_shl.s delete mode 100644 runtime/powerpc/i64_shr.s delete mode 100644 runtime/powerpc/i64_smod.s delete mode 100644 runtime/powerpc/i64_smulh.s delete mode 100644 runtime/powerpc/i64_stod.s delete mode 100644 runtime/powerpc/i64_stof.s delete mode 100644 runtime/powerpc/i64_udiv.s delete mode 100644 runtime/powerpc/i64_udivmod.s delete mode 100644 runtime/powerpc/i64_umod.s delete mode 100644 runtime/powerpc/i64_umulh.s delete mode 100644 runtime/powerpc/i64_utod.s delete mode 100644 runtime/powerpc/i64_utof.s delete mode 100644 runtime/powerpc/vararg.s delete mode 100644 runtime/powerpc64/i64_dtou.s delete mode 100644 runtime/powerpc64/i64_stof.s delete mode 100644 runtime/powerpc64/i64_utod.s delete mode 100644 runtime/powerpc64/i64_utof.s delete mode 100644 runtime/powerpc64/vararg.s (limited to 'runtime') diff --git a/runtime/powerpc/i64_dtos.s b/runtime/powerpc/i64_dtos.s deleted file mode 100644 index 85c60b27..00000000 --- a/runtime/powerpc/i64_dtos.s +++ /dev/null @@ -1,100 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 67a721d4..00000000 --- a/runtime/powerpc/i64_dtou.s +++ /dev/null @@ -1,92 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index c7da448f..00000000 --- a/runtime/powerpc/i64_sar.s +++ /dev/null @@ -1,60 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 9787ea3b..00000000 --- a/runtime/powerpc/i64_sdiv.s +++ /dev/null @@ -1,71 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index f6edb6c2..00000000 --- a/runtime/powerpc/i64_shl.s +++ /dev/null @@ -1,64 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index b634aafd..00000000 --- a/runtime/powerpc/i64_shr.s +++ /dev/null @@ -1,65 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 6b4e1f89..00000000 --- a/runtime/powerpc/i64_smod.s +++ /dev/null @@ -1,70 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 73393fce..00000000 --- a/runtime/powerpc/i64_smulh.s +++ /dev/null @@ -1,80 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 0c1ab720..00000000 --- a/runtime/powerpc/i64_stod.s +++ /dev/null @@ -1,67 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 97fa6bb8..00000000 --- a/runtime/powerpc/i64_stof.s +++ /dev/null @@ -1,68 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index e2da855a..00000000 --- a/runtime/powerpc/i64_udiv.s +++ /dev/null @@ -1,54 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index e81c6cef..00000000 --- a/runtime/powerpc/i64_udivmod.s +++ /dev/null @@ -1,234 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index bf8d6121..00000000 --- a/runtime/powerpc/i64_umod.s +++ /dev/null @@ -1,47 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 53b72948..00000000 --- a/runtime/powerpc/i64_umulh.s +++ /dev/null @@ -1,65 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 69de6fdb..00000000 --- a/runtime/powerpc/i64_utod.s +++ /dev/null @@ -1,66 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index cdb2f867..00000000 --- a/runtime/powerpc/i64_utof.s +++ /dev/null @@ -1,64 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 8d7e62c8..00000000 --- a/runtime/powerpc/vararg.s +++ /dev/null @@ -1,163 +0,0 @@ -# ***************************************************************** -# -# 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 diff --git a/runtime/powerpc64/i64_dtou.s b/runtime/powerpc64/i64_dtou.s deleted file mode 100644 index e58bcfaf..00000000 --- a/runtime/powerpc64/i64_dtou.s +++ /dev/null @@ -1,66 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 779cbc18..00000000 --- a/runtime/powerpc64/i64_stof.s +++ /dev/null @@ -1,68 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 491ee26b..00000000 --- a/runtime/powerpc64/i64_utod.s +++ /dev/null @@ -1,79 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index cdb2f867..00000000 --- a/runtime/powerpc64/i64_utof.s +++ /dev/null @@ -1,64 +0,0 @@ -# ***************************************************************** -# -# 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 deleted file mode 100644 index 8d7e62c8..00000000 --- a/runtime/powerpc64/vararg.s +++ /dev/null @@ -1,163 +0,0 @@ -# ***************************************************************** -# -# 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 51094cecd5d24023e3de2487e66765f8c54b5fcc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 29 Aug 2019 19:33:33 +0200 Subject: fmin/fmax/fminf/fmaxf non bien testés MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- runtime/include/math.h | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'runtime') diff --git a/runtime/include/math.h b/runtime/include/math.h index 805cc8e7..07feb14d 100644 --- a/runtime/include/math.h +++ b/runtime/include/math.h @@ -3,5 +3,14 @@ #define isfinite(__y) (fpclassify((__y)) >= FP_ZERO) +#ifndef COMPCERT_NO_FP_MACROS +#define fmin(x, y) __builtin_fmin((x),(y)) +#define fmax(x, y) __builtin_fmax((x),(y)) +#define fminf(x, y) __builtin_fminf((x),(y)) +#define fmaxf(x, y) __builtin_fmaxf((x),(y)) +#define fabs(x) __builtin_fabs((x)) +#define fabsf(x) __builtin_fabsf((x)) +#endif + #include_next #endif -- cgit From 2f7f68f69b6408e4de6210c827b108eff011af51 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 30 Aug 2019 19:39:58 +0200 Subject: macros for fma() fmaf() --- runtime/include/math.h | 2 ++ 1 file changed, 2 insertions(+) (limited to 'runtime') diff --git a/runtime/include/math.h b/runtime/include/math.h index 07feb14d..060968c8 100644 --- a/runtime/include/math.h +++ b/runtime/include/math.h @@ -10,6 +10,8 @@ #define fmaxf(x, y) __builtin_fmaxf((x),(y)) #define fabs(x) __builtin_fabs((x)) #define fabsf(x) __builtin_fabsf((x)) +#define fma(x, y, z) __builtin_fma((x),(y),(z)) +#define fmaf(x, y, z) __builtin_fmaf((x),(y),(z)) #endif #include_next -- cgit From 7cfc487a56aca2c1444e98a0b845ec25c9069476 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 5 Sep 2019 14:08:49 +0200 Subject: (#157) Fixing warning for desactivated afaddd builtin. No implementation yet --- runtime/include/ccomp_k1c_fixes.h | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'runtime') diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h index 5c543d8f..718ac3e5 100644 --- a/runtime/include/ccomp_k1c_fixes.h +++ b/runtime/include/ccomp_k1c_fixes.h @@ -17,6 +17,12 @@ extern __int128 __compcert_acswapd(void *address, unsigned long long new_value, #define __builtin_k1_acswapw __compcert_acswapw extern __int128 __compcert_acswapw(void *address, unsigned long long new_value, unsigned long long old_value); + +#define __builtin_k1_afaddd __compcert_afaddd +extern long long __compcert_afaddd(void *address, unsigned long long incr); + +#define __builtin_k1_afaddw __compcert_afaddw +extern int __compcert_afaddw(void *address, unsigned int incr); #endif #define __builtin_expect(x, y) (x) -- 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