diff --git a/runtime/powerpc/i64_dtos.S b/runtime/powerpc/i64_dtos.S index 85c60b278..0e2d3b140 100644 --- a/runtime/powerpc/i64_dtos.S +++ b/runtime/powerpc/i64_dtos.S @@ -1,98 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Conversion from double float to signed long +// 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 + 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) + 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 + // 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 + 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 + // 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 + // 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) + // 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 + // 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 + // 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 +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 +5: lis r3, 0x8000 // result is MIN_SINT = 0x8000_0000 li r4, 0 blr .type __compcert_i64_dtos, @function diff --git a/runtime/powerpc/i64_dtou.S b/runtime/powerpc/i64_dtou.S index 67a721d4c..7a040ce3a 100644 --- a/runtime/powerpc/i64_dtou.S +++ b/runtime/powerpc/i64_dtou.S @@ -1,77 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Conversion from double float to unsigned long +// 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 + 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) + 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 + // 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 + 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 + // 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 + // 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) + // 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 @@ -79,11 +81,11 @@ __compcert_i64_dtou: or r4, r4, r0 srw r3, r3, r5 blr - # Special cases -1: li r3, 0 # result is 0 + // Special cases +1: li r3, 0 // result is 0 li r4, 0 blr -2: li r3, -1 # result is MAX_UINT +2: li r3, -1 // result is MAX_UINT li r4, -1 blr .type __compcert_i64_dtou, @function diff --git a/runtime/powerpc/i64_sar.S b/runtime/powerpc/i64_sar.S index c7da448fb..744909db8 100644 --- a/runtime/powerpc/i64_sar.S +++ b/runtime/powerpc/i64_sar.S @@ -1,58 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -# Shift right signed +// Shift right signed .balign 16 .globl __compcert_i64_sar __compcert_i64_sar: - andi. r5, r5, 63 # take amount modulo 64 + 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) + 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 +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 diff --git a/runtime/powerpc/i64_sdiv.S b/runtime/powerpc/i64_sdiv.S index 9787ea3b1..d955ac8ec 100644 --- a/runtime/powerpc/i64_sdiv.S +++ b/runtime/powerpc/i64_sdiv.S @@ -1,66 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Signed division +// 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) + 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) + 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 + bl __compcert_i64_udivmod // do unsigned division lwz r0, 4(r1) - mtlr r0 # restore return address + 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 + 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 diff --git a/runtime/powerpc/i64_shl.S b/runtime/powerpc/i64_shl.S index f6edb6c25..028f72259 100644 --- a/runtime/powerpc/i64_shl.S +++ b/runtime/powerpc/i64_shl.S @@ -1,57 +1,59 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -# Shift left +// 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 +// 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 diff --git a/runtime/powerpc/i64_shr.S b/runtime/powerpc/i64_shr.S index b634aafd0..b05bdc4da 100644 --- a/runtime/powerpc/i64_shr.S +++ b/runtime/powerpc/i64_shr.S @@ -1,57 +1,59 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -# Shift right unsigned +// 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 +// 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 diff --git a/runtime/powerpc/i64_smod.S b/runtime/powerpc/i64_smod.S index 6b4e1f898..12f2f28f8 100644 --- a/runtime/powerpc/i64_smod.S +++ b/runtime/powerpc/i64_smod.S @@ -1,65 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -## Signed remainder +// 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) + 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) + 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 + bl __compcert_i64_udivmod // do unsigned division lwz r0, 4(r1) - mtlr r0 # restore return address + 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 + 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 diff --git a/runtime/powerpc/i64_smulh.S b/runtime/powerpc/i64_smulh.S index 73393fce6..855b45acd 100644 --- a/runtime/powerpc/i64_smulh.S +++ b/runtime/powerpc/i64_smulh.S @@ -1,78 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Signed multiply-high +// 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 +// 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 +// 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 + mulhwu r0, r4, r5 // r0 = high half of XL.YH addze r8, r0 - mullw r0, r3, r6 # r0 = low half of XH.YL + mullw r0, r3, r6 // r0 = low half of XH.YL addc r9, r9, r0 - mulhwu r0, r3, r6 # r0 = high half of XH.YL + 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 + mullw r0, r3, r5 // r0 = low half of XH.YH addc r8, r8, r0 - mulhwu r0, r3, r5 # r0 = high half of XH.YH + 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 +// 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 r5, r5, r0 // set Y = 0 if X >= 0 and r6, r6, r0 - subfc r8, r4, r8 # subtract X + subfc r8, r4, r8 // subtract X subfe r7, r3, r7 - subfc r4, r6, r8 # subtract Y + subfc r4, r6, r8 // subtract Y subfe r3, r5, r7 blr .type __compcert_i64_smulh, @function diff --git a/runtime/powerpc/i64_stod.S b/runtime/powerpc/i64_stod.S index 0c1ab7208..30e10e7aa 100644 --- a/runtime/powerpc/i64_stod.S +++ b/runtime/powerpc/i64_stod.S @@ -1,40 +1,44 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. -### Conversion from signed long to double float +#include "sysdeps.h" + + .text + +// Conversion from signed long to double float .balign 16 .globl __compcert_i64_stod @@ -43,23 +47,23 @@ __compcert_i64_stod: lis r5, 0x4330 li r6, 0 stw r5, 0(r1) - stw r4, 4(r1) # 0(r1) = 2^52 + (double) XL + stw r4, 4(r1) // 0(r1) = 2^52 + (double) XL stw r5, 8(r1) - stw r6, 12(r1) # 8(r1) = 2^52 + 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 + 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 + 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 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 + 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 diff --git a/runtime/powerpc/i64_stof.S b/runtime/powerpc/i64_stof.S index ea23a1c81..92e1fe475 100644 --- a/runtime/powerpc/i64_stof.S +++ b/runtime/powerpc/i64_stof.S @@ -1,63 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Conversion from signed long to single float +// 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, 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 + // Check whether -2^53 <= X < 2^53 + 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 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 + // 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 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 mtlr r9 frsp f1, f1 diff --git a/runtime/powerpc/i64_udiv.S b/runtime/powerpc/i64_udiv.S index e2da855a5..dd5ba635c 100644 --- a/runtime/powerpc/i64_udiv.S +++ b/runtime/powerpc/i64_udiv.S @@ -1,52 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Unsigned division +// 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 + 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 + mtlr r0 // restore return address + mr r3, r5 // result = quotient mr r4, r6 blr .type __compcert_i64_udiv, @function diff --git a/runtime/powerpc/i64_udivmod.S b/runtime/powerpc/i64_udivmod.S index e81c6cef5..e24e64ddb 100644 --- a/runtime/powerpc/i64_udivmod.S +++ b/runtime/powerpc/i64_udivmod.S @@ -1,98 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -# Unsigned division and modulus +// Unsigned division and modulus -# This function computes both the quotient and the remainder of two -# unsigned 64-bit integers. +// 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 +// 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 ? + cmplwi r5, 0 // DH == 0 ? stwu r1, -32(r1) mflr r0 stw r0, 8(r1) stw r31, 12(r1) beq 1f -# The general case +// The general case stw r30, 16(r1) stw r29, 20(r1) stw r28, 24(r1) - mr r28, r3 # Save N in (r28, r29) + mr r28, r3 // Save N in (r28, r29) mr r29, r4 - mr r30, r5 # Save D in (r30, r31) + 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 + // 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 + 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 + // 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 + 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 + 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 + // Finished 3: lwz r0, 8(r1) mtlr r0 lwz r31, 12(r1) @@ -101,79 +103,79 @@ __compcert_i64_udivmod: 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 + // 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? +// 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 + 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 + 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 + 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 +// 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 + 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 + 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 +// 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; +// 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 +// vn1 = v >> 16; # vn1 in r7 srwi r7, r5, 16 -# vn0 = v & 0xFFFF; # vn0 in r8 +// vn0 = v & 0xFFFF; # vn0 in r8 rlwinm r8, r5, 0, 16, 31 -# un32 = (u1 << s) | (u0 >> 32 - s); +// un32 = (u1 << s) | (u0 >> 32 - s); subfic r0, r6, 32 srw r0, r4, r0 - slw r3, r3, r6 # u1 dies, un32 in r3 + 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; +// 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: + subf r11, r0, r3 // rhat in r11 +// again1: 1: -# if (q1 >= b || q1*vn0 > b*rhat + un1) { +// if (q1 >= b || q1*vn0 > b*rhat + un1) { cmplwi r10, 0xFFFF bgt 2f mullw r0, r10, r8 @@ -182,27 +184,27 @@ __compcert_i64_udiv6432: cmplw r0, r12 ble 3f 2: -# q1 = q1 - 1; +// q1 = q1 - 1; addi r10, r10, -1 -# rhat = rhat + vn1; +// rhat = rhat + vn1; add r11, r11, r7 -# if (rhat < b) goto again1;} +// 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 +// 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; + 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: + subf r11, r0, r9 // rhat in r11 +// again2: 4: -# if (q0 >= b || q0*vn0 > b*rhat + un0) { +// if (q0 >= b || q0*vn0 > b*rhat + un0) { cmplwi r3, 0xFFFF bgt 5f mullw r0, r3, r8 @@ -211,21 +213,21 @@ __compcert_i64_udiv6432: cmplw r0, r12 ble 6f 5: -# q0 = q0 - 1; +// q0 = q0 - 1; addi r3, r3, -1 -# rhat = rhat + vn1; +// rhat = rhat + vn1; add r11, r11, r7 -# if (rhat < b) goto again2;} +// if (rhat < b) goto again2;} cmplwi r11, 0xFFFF ble 4b 6: -# remainder = (un21*b + un0 - q0*v) >> s; +// remainder = (un21*b + un0 - q0*v) >> s; slwi r0, r9, 16 - add r4, r0, r4 # un0 dies, remainder in r4 + 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; +// quotient = q1*b + q0; slwi r0, r10, 16 add r3, r0, r3 blr diff --git a/runtime/powerpc/i64_umod.S b/runtime/powerpc/i64_umod.S index bf8d6121c..9cabaf586 100644 --- a/runtime/powerpc/i64_umod.S +++ b/runtime/powerpc/i64_umod.S @@ -1,42 +1,44 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Unsigned modulus +// Unsigned modulus .balign 16 .globl __compcert_i64_umod diff --git a/runtime/powerpc/i64_umulh.S b/runtime/powerpc/i64_umulh.S index 53b729484..38f3f9d67 100644 --- a/runtime/powerpc/i64_umulh.S +++ b/runtime/powerpc/i64_umulh.S @@ -1,63 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Unsigned multiply-high +// Unsigned multiply-high -# X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL +// 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 +// 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 + mulhwu r0, r4, r5 // r0 = high half of XL.YH addze r8, r0 - mullw r0, r3, r6 # r0 = low half of XH.YL + mullw r0, r3, r6 // r0 = low half of XH.YL addc r9, r9, r0 - mulhwu r0, r3, r6 # r0 = high half of XH.YL + 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 + mullw r0, r3, r5 // r0 = low half of XH.YH addc r4, r8, r0 - mulhwu r0, r3, r5 # r0 = high half of XH.YH + mulhwu r0, r3, r5 // r0 = high half of XH.YH adde r3, r7, r0 blr .type __compcert_i64_umulh, @function diff --git a/runtime/powerpc/i64_utod.S b/runtime/powerpc/i64_utod.S index 69de6fdb5..3fd0e344d 100644 --- a/runtime/powerpc/i64_utod.S +++ b/runtime/powerpc/i64_utod.S @@ -1,42 +1,44 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Conversion from unsigned long to double float +// Conversion from unsigned long to double float .balign 16 .globl __compcert_i64_utod @@ -45,20 +47,20 @@ __compcert_i64_utod: lis r5, 0x4330 li r6, 0 stw r5, 0(r1) - stw r4, 4(r1) # 0(r1) = 2^52 + (double) XL + stw r4, 4(r1) // 0(r1) = 2^52 + (double) XL stw r5, 8(r1) - stw r6, 12(r1) # 8(r1) = 2^52 + stw r6, 12(r1) // 8(r1) = 2^52 lfd f1, 0(r1) lfd f2, 8(r1) - fsub f1, f1, f2 # f1 is (double) XL + fsub f1, f1, f2 // f1 is (double) XL lis r5, 0x4530 - stw r5, 0(r1) # 0(r1) = 2^84 + (double) XH * 2^32 + stw r5, 0(r1) // 0(r1) = 2^84 + (double) XH * 2^32 stw r3, 4(r1) - stw r5, 8(r1) # 8(r1) = 2^84 + 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 + 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 diff --git a/runtime/powerpc/i64_utof.S b/runtime/powerpc/i64_utof.S index 4a2a172b6..e8e8307ea 100644 --- a/runtime/powerpc/i64_utof.S +++ b/runtime/powerpc/i64_utof.S @@ -1,60 +1,62 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Conversion from unsigned long to single float +// 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 + // 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 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 + // 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 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 mtlr r9 frsp f1, f1 diff --git a/runtime/powerpc/sysdeps.h b/runtime/powerpc/sysdeps.h new file mode 100644 index 000000000..b65621a28 --- /dev/null +++ b/runtime/powerpc/sysdeps.h @@ -0,0 +1,39 @@ +// ***************************************************************** +// +// 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 + +#if defined(SYS_linux) || defined(SYS_bsd) + .section .note.GNU-stack,"",%progbits +#endif diff --git a/runtime/powerpc/vararg.S b/runtime/powerpc/vararg.S index 8d7e62c8b..73691cded 100644 --- a/runtime/powerpc/vararg.S +++ b/runtime/powerpc/vararg.S @@ -1,74 +1,76 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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 +// Helper functions for variadic functions . PowerPC 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); +// 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); + +#include "sysdeps.h" .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 + // 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 + // 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 + 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 + // 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 + lwz r3, -4(r5) // load argument in r3 blr .type __compcert_va_int32, @function .size __compcert_va_int32, .-__compcert_va_int32 @@ -76,28 +78,28 @@ __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 + // 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 + // 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 + 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 + // 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 + 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 + 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 @@ -106,24 +108,24 @@ __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 + // 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 + // 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 + 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 + // 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 + 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 @@ -135,13 +137,13 @@ __compcert_va_composite: .type __compcert_va_composite, @function .size __compcert_va_composite, .-__compcert_va_composite -# Save integer and FP registers at beginning of vararg function +// 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 + 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) @@ -149,7 +151,7 @@ __compcert_va_saveregs: 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 + 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) diff --git a/runtime/powerpc64/i64_dtou.S b/runtime/powerpc64/i64_dtou.S index e58bcfaf1..5d8e82698 100644 --- a/runtime/powerpc64/i64_dtou.S +++ b/runtime/powerpc64/i64_dtou.S @@ -1,63 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + +#include "sysdeps.h" .text -### Conversion from double float to unsigned long +// 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 + 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 + 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 +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 + addis r3, r3, 0x8000 // shift result up by 2^63 addi r1, r1, 16 blr .type __compcert_i64_dtou, @function diff --git a/runtime/powerpc64/i64_stof.S b/runtime/powerpc64/i64_stof.S index 779cbc18d..b4cb464e1 100644 --- a/runtime/powerpc64/i64_stof.S +++ b/runtime/powerpc64/i64_stof.S @@ -1,62 +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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + +#include "sysdeps.h" .text -### Conversion from signed long to single float +// 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 + 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 + // 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 diff --git a/runtime/powerpc64/i64_utod.S b/runtime/powerpc64/i64_utod.S index 491ee26b0..c18ee399f 100644 --- a/runtime/powerpc64/i64_utod.S +++ b/runtime/powerpc64/i64_utod.S @@ -1,79 +1,81 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC 64 version. + +#include "sysdeps.h" .text -### Conversion from unsigned long to double float +// 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 + 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) + 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 + 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 +// 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 index 4a2a172b6..e8e8307ea 100644 --- a/runtime/powerpc64/i64_utof.S +++ b/runtime/powerpc64/i64_utof.S @@ -1,60 +1,62 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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. +// Helper functions for 64-bit integer arithmetic. PowerPC version. + +#include "sysdeps.h" .text -### Conversion from unsigned long to single float +// 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 + // 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 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 + // 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 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 mtlr r9 frsp f1, f1 diff --git a/runtime/powerpc64/sysdeps.h b/runtime/powerpc64/sysdeps.h new file mode 100644 index 000000000..b65621a28 --- /dev/null +++ b/runtime/powerpc64/sysdeps.h @@ -0,0 +1,39 @@ +// ***************************************************************** +// +// 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 + +#if defined(SYS_linux) || defined(SYS_bsd) + .section .note.GNU-stack,"",%progbits +#endif diff --git a/runtime/powerpc64/vararg.S b/runtime/powerpc64/vararg.S index 8d7e62c8b..588451002 100644 --- a/runtime/powerpc64/vararg.S +++ b/runtime/powerpc64/vararg.S @@ -1,74 +1,76 @@ -# ***************************************************************** -# -# 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. -# -# ********************************************************************* +// ***************************************************************** +// +// 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 +// 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); +// 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); + +#include "sysdeps.h" .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 + // 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 + // 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 + 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 + // 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 + lwz r3, -4(r5) // load argument in r3 blr .type __compcert_va_int32, @function .size __compcert_va_int32, .-__compcert_va_int32 @@ -76,28 +78,28 @@ __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 + // 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 + // 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 + 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 + // 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 + 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 + 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 @@ -106,24 +108,24 @@ __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 + // 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 + // 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 + 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 + // 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 + 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 @@ -135,13 +137,13 @@ __compcert_va_composite: .type __compcert_va_composite, @function .size __compcert_va_composite, .-__compcert_va_composite -# Save integer and FP registers at beginning of vararg function +// 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 + 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) @@ -149,7 +151,7 @@ __compcert_va_saveregs: 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 + 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)