Hybrid 64bit/32bit PowerPC port

This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.

The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.

In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.

5 files changed, 440 insertions, 0 deletions

diff --git a/runtime/powerpc64/i64_dtou.s b/runtime/powerpc64/i64_dtou.s
new file mode 100644
index 00000000..60d5c9bf
--- /dev/null
+++ b/runtime/powerpc64/i64_dtou.s
@@ -0,0 +1,66 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> 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 <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from double float to unsigned long	
+
+        .balign 16
+        .globl __i64_dtou
+__i64_dtou:
+        lis r0, 0x5f00          # 0x5f00_0000 = 2^63 in binary32 format
+        stwu r0, -16(r1)
+        lfs f2, 0(r1)           # f2 = 2^63
+        fcmpu cr0, f1, f2       # crbit 0 is f1 < f2
+        bf 0, 1f                # branch if f1 >= 2^63 (or f1 is NaN)
+	fctidz f1, f1           # convert as signed
+        stfd f1, 0(r1)
+        lwz r3, 0(r1)
+        lwz r4, 4(r1)
+        addi r1, r1, 16
+        blr
+1:      fsub f1, f1, f2         # shift argument down by 2^63
+	fctidz f1, f1           # convert as signed
+        stfd f1, 0(r1)
+        lwz r3, 0(r1)
+        lwz r4, 4(r1)
+        addis r3, r3, 0x8000    # shift result up by 2^63
+        addi r1, r1, 16
+        blr
+        .type __i64_dtou, @function
+        .size __i64_dtou, .-__i64_dtou
+
+        
diff --git a/runtime/powerpc64/i64_stof.s b/runtime/powerpc64/i64_stof.s
new file mode 100644
index 00000000..8830d594
--- /dev/null
+++ b/runtime/powerpc64/i64_stof.s
@@ -0,0 +1,68 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> 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 <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from signed long to single float	
+
+        .balign 16
+        .globl __i64_stof
+__i64_stof:
+        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
+   # Check whether -2^53 <= X < 2^53	
+        sradi r5, r4, 53
+        addi r5, r5, 1
+        cmpldi r5, 2
+	blt 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rldicl r5, r4, 0, 53     # extract bits 0 to 11 of X
+        addi r5, r5, 0x7FF       # r5 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-63 of r5 are 0
+        or r4, r4, r5            # correct bit number 12 of X
+        rldicr r4, r4, 0, 52     # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single
+1:      stdu r4, -16(r1)
+        lfd f1, 0(r1)
+        fcfid f1, f1
+	frsp f1, f1
+        addi r1, r1, 16
+        blr
+        .type __i64_stof, @function
+        .size __i64_stof, .-__i64_stof
+	
diff --git a/runtime/powerpc64/i64_utod.s b/runtime/powerpc64/i64_utod.s
new file mode 100644
index 00000000..ddde91dd
--- /dev/null
+++ b/runtime/powerpc64/i64_utod.s
@@ -0,0 +1,79 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> 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 <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from unsigned long to double float	
+
+        .balign 16
+        .globl __i64_utod
+__i64_utod:
+	rldicl r3, r3, 0, 32    # clear top 32 bits
+	rldicl r4, r4, 0, 32    # clear top 32 bits
+	lis r5, 0x4f80          # 0x4f80_0000 = 2^32 in binary32 format
+        stdu r3, -32(r1)
+        std r4, 8(r1)
+        stw r5, 16(r1)
+        lfd f1, 0(r1)           # high 32 bits of argument
+        lfd f2, 8(r1)           # low 32 bits of argument
+	lfs f3, 16(r1)          # 2^32
+        fcfid f1, f1            # convert both 32-bit halves to FP (exactly)
+	fcfid f2, f2
+        fmadd f1, f1, f3, f2    # compute hi * 2^32 + lo
+        addi r1, r1, 32
+        blr
+        .type __i64_utod, @function
+        .size __i64_utod, .-__i64_utod
+	
+# Alternate implementation using round-to-odd:
+#       rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
+#       cmpdi r4, 0            # is r4 >= 2^63 ?
+#       blt 1f
+#	stdu r4, -16(r1)       # r4 < 2^63: convert as signed
+#       lfd f1, 0(r1)
+#       fcfid f1, f1
+#       addi r1, r1, 16
+#       blr
+#1:     rldicl r0, r4, 0, 63   # extract low bit of r4
+#       srdi r4, r4, 1
+#       or r4, r4, r0          # round r4 to 63 bits, using round-to-odd
+#	stdu r4, -16(r1)       # convert to binary64
+#       lfd f1, 0(r1)
+#       fcfid f1, f1
+#       fadd f1, f1, f1        # multiply result by 2
+#       addi r1, r1, 16
+#       blr
+        
\ No newline at end of file
diff --git a/runtime/powerpc64/i64_utof.s b/runtime/powerpc64/i64_utof.s
new file mode 100644
index 00000000..2617cbda
--- /dev/null
+++ b/runtime/powerpc64/i64_utof.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> 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 <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from unsigned long to single float	
+
+        .balign 16
+        .globl __i64_utof
+__i64_utof:
+	mflr r9
+   # Check whether X < 2^53	
+        andis. r0, r3, 0xFFE0       # test bits 53...63 of X
+        beq 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r0 are 0
+        or r4, r4, r0           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+1:      bl __i64_utod
+        mtlr r9
+        frsp f1, f1
+        blr
+        .type __i64_utof, @function
+        .size __i64_utof, .-__i64_utof
+	
diff --git a/runtime/powerpc64/vararg.s b/runtime/powerpc64/vararg.s
new file mode 100644
index 00000000..8d7e62c8
--- /dev/null
+++ b/runtime/powerpc64/vararg.s
@@ -0,0 +1,163 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> 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 <COPYRIGHT
+# HOLDER> 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 <stdarg.h>.  IA32 version
+
+# typedef struct {
+#   unsigned char ireg;    // index of next integer register
+#   unsigned char freg;    // index of next FP register
+#   char * stk;            // pointer to next argument in stack
+#   struct {
+#     int iregs[8];
+#     double fregs[8];
+#   } * regs;              // pointer to saved register area
+# } va_list[1];
+#
+# unsigned int __compcert_va_int32(va_list ap);
+# unsigned long long __compcert_va_int64(va_list ap);
+# double __compcert_va_float64(va_list ap);
+
+        .text
+
+        .balign 16
+        .globl __compcert_va_int32
+__compcert_va_int32:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in an integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	addi    r4, r4, 1       # increment ap->ireg
+        stb     r4, 0(r3)
+        lwzx    r3, r5, r6      # load argument in r3
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+        addi    r5, r5, 4       # advance ap->stk by 4
+        stw     r5, 4(r3)
+	lwz     r3, -4(r5)      # load argument in r3
+        blr
+        .type   __compcert_va_int32, @function
+        .size   __compcert_va_int32, .-__compcert_va_int32
+
+        .balign 16
+        .globl __compcert_va_int64
+__compcert_va_int64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 7
+        bge     1f
+  # Next argument was passed in two consecutive integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+	addi    r4, r4, 3       # round r4 up to an even number and add 2
+        rlwinm  r4, r4, 0, 0, 30 
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	add     r5, r5, r6      # r5 = address of argument + 8
+        stb     r4, 0(r3)       # update ap->ireg
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	li      r4, 8
+        stb     r4, 0(r3)       # set ap->ireg = 8 so that no ireg is left
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+	stw     r5, 4(r3)       # update ap->stk
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+        .type   __compcert_va_int64, @function
+        .size   __compcert_va_int64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_float64
+__compcert_va_float64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 1(r3)       # r4 = ap->freg = next float register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in a FP register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 3, 0, 28 # r6 = r4 * 8
+	add     r5, r5, r6
+        lfd     f1, 32(r5)      # load argument in f1
+	addi    r4, r4, 1       # increment ap->freg
+        stb     r4, 1(r3)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+        lfd     f1, -8(r5)      # load argument in f1
+	stw     r5, 4(r3)       # update ap->stk
+        blr
+        .type   __compcert_va_float64, @function
+        .size   __compcert_va_float64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_composite
+__compcert_va_composite:
+	b       __compcert_va_int32
+        .type   __compcert_va_composite, @function
+        .size   __compcert_va_composite, .-__compcert_va_composite
+
+# Save integer and FP registers at beginning of vararg function        
+
+        .balign 16
+        .globl  __compcert_va_saveregs
+__compcert_va_saveregs:
+        lwz     r11, 0(r1)      # r11 point to top of our frame
+        stwu    r3, -96(r11)    # register save area is 96 bytes below
+        stw     r4, 4(r11)
+        stw     r5, 8(r11)
+        stw     r6, 12(r11)
+        stw     r7, 16(r11)
+        stw     r8, 20(r11)
+        stw     r9, 24(r11)
+        stw     r10, 28(r11)
+	bf      6, 1f           # don't save FP regs if CR6 bit is clear
+        stfd    f1, 32(r11)
+        stfd    f2, 40(r11)
+        stfd    f3, 48(r11)
+        stfd    f4, 56(r11)
+        stfd    f5, 64(r11)
+        stfd    f6, 72(r11)
+        stfd    f7, 80(r11)
+        stfd    f8, 88(r11)
+1:      blr
+        .type   __compcert_va_saveregs, @function
+        .size   __compcert_va_saveregs, .-__compcert_va_saveregs