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.

12 files changed, 0 insertions, 677 deletions

diff --git a/runtime/powerpc/ppc64/i64_dtos.s b/runtime/powerpc/ppc64/i64_dtos.s
deleted file mode 100644
index 95f7f700..00000000
--- a/runtime/powerpc/ppc64/i64_dtos.s
+++ /dev/null
@@ -1,52 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 signed long	
-
-        .balign 16
-        .globl __i64_dtos
-__i64_dtos:
-	fctidz f1, f1
-        stfdu f1, -16(r1)
-        lwz r3, 0(r1)
-        lwz r4, 4(r1)
-        addi r1, r1, 16
-        blr
-        .type __i64_dtos, @function
-        .size __i64_dtos, .-__i64_dtos
-        
\ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_dtou.s b/runtime/powerpc/ppc64/i64_dtou.s
deleted file mode 100644
index 60d5c9bf..00000000
--- a/runtime/powerpc/ppc64/i64_dtou.s
+++ /dev/null
@@ -1,66 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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/powerpc/ppc64/i64_sar.s b/runtime/powerpc/ppc64/i64_sar.s
deleted file mode 100644
index 4fc4451e..00000000
--- a/runtime/powerpc/ppc64/i64_sar.s
+++ /dev/null
@@ -1,51 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-# Shift right signed	
-	
-        .balign 16
-        .globl __i64_sar
-__i64_sar:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-	srad r4, r4, r5
-        srdi r3, r4, 32        # split r4 into (r3,r4)
-        blr
-        .type __i64_sar, @function
-        .size __i64_sar, .-__i64_sar
-
-        
\ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_sdiv.s b/runtime/powerpc/ppc64/i64_sdiv.s
deleted file mode 100644
index 2bf5b574..00000000
--- a/runtime/powerpc/ppc64/i64_sdiv.s
+++ /dev/null
@@ -1,52 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Signed division	
-	
-        .balign 16
-        .globl __i64_sdiv
-__i64_sdiv:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-        rldimi r6, r5, 32, 0   # reassemble (r5,r6) as a 64-bit integer in r6
-	divd r4, r4, r6
-        srdi r3, r4, 32        # split r4 into (r3,r4)
-	blr
-        .type __i64_sdiv, @function
-        .size __i64_sdiv, .-__i64_sdiv
-	
-        
\ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_shl.s b/runtime/powerpc/ppc64/i64_shl.s
deleted file mode 100644
index 955de565..00000000
--- a/runtime/powerpc/ppc64/i64_shl.s
+++ /dev/null
@@ -1,50 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-# Shift left
-	
-        .balign 16
-        .globl __i64_shl
-__i64_shl:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-	sld r4, r4, r5
-        srdi r3, r4, 32        # split r4 into (r3,r4)
-        blr
-        .type __i64_shl, @function
-        .size __i64_shl, .-__i64_shl
-        
\ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_shr.s b/runtime/powerpc/ppc64/i64_shr.s
deleted file mode 100644
index ca5ac9b2..00000000
--- a/runtime/powerpc/ppc64/i64_shr.s
+++ /dev/null
@@ -1,51 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-# Shift right unsigned
-	
-        .balign 16
-        .globl __i64_shr
-__i64_shr:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-	srd r4, r4, r5
-        srdi r3, r4, 32        # split r4 into (r3,r4)
-        blr
-        .type __i64_shr, @function
-        .size __i64_shr, .-__i64_shr
-	
-        
\ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_smod.s b/runtime/powerpc/ppc64/i64_smod.s
deleted file mode 100644
index 35be366d..00000000
--- a/runtime/powerpc/ppc64/i64_smod.s
+++ /dev/null
@@ -1,54 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-## Signed remainder	
-	
-        .balign 16
-        .globl __i64_smod
-__i64_smod:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-        rldimi r6, r5, 32, 0   # reassemble (r5,r6) as a 64-bit integer in r6
-	divd r0, r4, r6
-	mulld r0, r0, r6
-        subf r4, r0, r4
-        srdi r3, r4, 32        # split r4 into (r3,r4)
-        blr
-        .type __i64_smod, @function
-        .size __i64_smod, .-__i64_smod
-
-        
\ No newline at end of file
diff --git a/runtime/powerpc/ppc64/i64_stod.s b/runtime/powerpc/ppc64/i64_stod.s
deleted file mode 100644
index 3636d0b5..00000000
--- a/runtime/powerpc/ppc64/i64_stod.s
+++ /dev/null
@@ -1,50 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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.
-
-### Conversion from signed long to double float	
-
-        .balign 16
-        .globl __i64_stod
-__i64_stod:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-	stdu r4, -16(r1)
-        lfd f1, 0(r1)
-        fcfid f1, f1
-        addi r1, r1, 16
-        blr
-        .type __i64_stod, @function
-        .size __i64_stod, .-__i64_stod
-
diff --git a/runtime/powerpc/ppc64/i64_stof.s b/runtime/powerpc/ppc64/i64_stof.s
deleted file mode 100644
index 8830d594..00000000
--- a/runtime/powerpc/ppc64/i64_stof.s
+++ /dev/null
@@ -1,68 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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/powerpc/ppc64/i64_udiv.s b/runtime/powerpc/ppc64/i64_udiv.s
deleted file mode 100644
index a6a3bcb3..00000000
--- a/runtime/powerpc/ppc64/i64_udiv.s
+++ /dev/null
@@ -1,51 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Unsigned division	
-
-        .balign 16
-        .globl __i64_udiv
-__i64_udiv:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-        rldimi r6, r5, 32, 0   # reassemble (r5,r6) as a 64-bit integer in r6
-	divdu r4, r4, r6
-        srdi r3, r4, 32        # split r4 into (r3,r4)
-        blr
-        .type __i64_udiv, @function
-        .size __i64_udiv, .-__i64_udiv
-
diff --git a/runtime/powerpc/ppc64/i64_umod.s b/runtime/powerpc/ppc64/i64_umod.s
deleted file mode 100644
index 6bda1903..00000000
--- a/runtime/powerpc/ppc64/i64_umod.s
+++ /dev/null
@@ -1,53 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Unsigned modulus
-
-        .balign 16
-        .globl __i64_umod
-__i64_umod:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-        rldimi r6, r5, 32, 0   # reassemble (r5,r6) as a 64-bit integer in r6
-	divdu r0, r4, r6
-	mulld r0, r0, r6
-        subf r4, r0, r4
-        srdi r3, r4, 32        # split r4 into (r3,r4)
-        blr
-        .type __i64_umod, @function
-        .size __i64_umod, .-__i64_umod
-
diff --git a/runtime/powerpc/ppc64/i64_utod.s b/runtime/powerpc/ppc64/i64_utod.s
deleted file mode 100644
index ddde91dd..00000000
--- a/runtime/powerpc/ppc64/i64_utod.s
+++ /dev/null
@@ -1,79 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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