merge upstream including fma fixes

22 files changed, 0 insertions, 1870 deletions

diff --git a/runtime/powerpc/i64_dtos.s b/runtime/powerpc/i64_dtos.s
deleted file mode 100644
index 85c60b27..00000000
--- a/runtime/powerpc/i64_dtos.s
+++ /dev/null
@@ -1,100 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 double float to signed long	
-
-        .balign 16
-        .globl __compcert_i64_dtos
-__compcert_i64_dtos:
-        stfdu f1, -16(r1)       # extract LO (r4) and HI (r3) halves of double
-        lwz r3, 0(r1)
-        lwz r4, 4(r1)
-        addi r1, r1, 16
-        srawi r10, r3, 31       # save sign of double in r10
- # extract unbiased exponent  ((HI & 0x7FF00000) >> 20) - (1023 + 52)
-        rlwinm r5, r3, 12, 21, 31
-        addi r5, r5, -1075
- # check range of exponent
-        cmpwi r5, -52           # if EXP < -52, abs(double) is < 1.0
-        blt 1f
-        cmpwi r5, 11            # if EXP >= 63 - 52, abs(double) is >= 2^63
-        bge 2f
-  # extract true mantissa
-        rlwinm r3, r3, 0, 12, 31  # HI &= ~0xFFF00000
-        oris r3, r3, 0x10         # HI |=  0x00100000
-  # shift it appropriately
-        cmpwi r5, 0
-        blt 3f
-  # if EXP >= 0, shift left by EXP.  Note that EXP < 11.
-        subfic r6, r5, 32       # r6 = 32 - EXP
-        slw r3, r3, r5
-        srw r0, r4, r6
-        or r3, r3, r0
-        slw r4, r4, r5
-        b 4f
-  # if EXP < 0, shift right by -EXP.  Note that -EXP <= 52 but can be >= 32.
-3:      subfic r5, r5, 0        # r5 = -EXP = shift amount
-        subfic r6, r5, 32       # r6 = 32 - amount
-        addi r7, r5, -32        # r7 = amount - 32  (see i64_shr.s)
-        srw r4, r4, r5
-        slw r0, r3, r6
-        or r4, r4, r0
-        srw r0, r3, r7
-        or r4, r4, r0
-        srw r3, r3, r5
-  # apply sign to result	
-4:      xor r4, r4, r10
-        xor r3, r3, r10
-        subfc r4, r10, r4
-        subfe r3, r10, r3
-        blr
-  # Special cases
-1:      li r3, 0                # result is 0
-        li r4, 0
-        blr
-2:      li r4, -1               # result is MAX_SINT or MIN_SINT
-        bge 5f                  # depending on sign
-        li r4, -1               # result is MAX_SINT =  0x7FFF_FFFF
-        srwi r3, r4, 1
-        blr
-5:      lis r3, 0x8000          # result is MIN_SINT = 0x8000_0000
-        li r4, 0
-        blr
-        .type __compcert_i64_dtos, @function
-        .size __compcert_i64_dtos, .-__compcert_i64_dtos
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_dtou.s b/runtime/powerpc/i64_dtou.s
deleted file mode 100644
index 67a721d4..00000000
--- a/runtime/powerpc/i64_dtou.s
+++ /dev/null
@@ -1,92 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 double float to unsigned long	
-
-        .balign 16
-        .globl __compcert_i64_dtou
-__compcert_i64_dtou:
-        stfdu f1, -16(r1)       # extract LO (r4) and HI (r3) halves of double
-        lwz r3, 0(r1)
-        lwz r4, 4(r1)
-        addi r1, r1, 16
-        cmpwi r3, 0             # is double < 0?
-        blt 1f                  # then it converts to 0
-  # extract unbiased exponent  ((HI & 0x7FF00000) >> 20) - (1023 + 52)
-        rlwinm r5, r3, 12, 21, 31
-        addi r5, r5, -1075
-  # check range of exponent
-        cmpwi r5, -52           # if EXP < -52, double is < 1.0
-        blt 1f
-        cmpwi r5, 12            # if EXP >= 64 - 52, double is >= 2^64
-        bge 2f
-  # extract true mantissa
-        rlwinm r3, r3, 0, 12, 31  # HI &= ~0xFFF00000
-        oris r3, r3, 0x10         # HI |=  0x00100000
-  # shift it appropriately
-        cmpwi r5, 0
-        blt 3f
-  # if EXP >= 0, shift left by EXP.  Note that EXP < 12.
-        subfic r6, r5, 32       # r6 = 32 - EXP
-        slw r3, r3, r5
-        srw r0, r4, r6
-        or r3, r3, r0
-        slw r4, r4, r5
-        blr
-  # if EXP < 0, shift right by -EXP.  Note that -EXP <= 52 but can be >= 32.
-3:      subfic r5, r5, 0        # r5 = -EXP = shift amount
-        subfic r6, r5, 32       # r6 = 32 - amount
-        addi r7, r5, -32        # r7 = amount - 32 (see i64_shr.s)
-        srw r4, r4, r5
-        slw r0, r3, r6
-        or r4, r4, r0
-        srw r0, r3, r7
-        or r4, r4, r0
-        srw r3, r3, r5
-        blr
-  # Special cases
-1:      li r3, 0                # result is 0
-        li r4, 0
-        blr
-2:      li r3, -1               # result is MAX_UINT
-        li r4, -1
-        blr
-        .type __compcert_i64_dtou, @function
-        .size __compcert_i64_dtou, .-__compcert_i64_dtou
-
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_sar.s b/runtime/powerpc/i64_sar.s
deleted file mode 100644
index c7da448f..00000000
--- a/runtime/powerpc/i64_sar.s
+++ /dev/null
@@ -1,60 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-# Shift right signed	
-	
-        .balign 16
-        .globl __compcert_i64_sar
-__compcert_i64_sar:
-        andi. r5, r5, 63        # take amount modulo 64
-        cmpwi r5, 32
-        bge 1f                  # amount < 32?
-        subfic r6, r5, 32       # r6 = 32 - amount
-        srw r4, r4, r5          # RH = XH >>s amount
-        slw r0, r3, r6          # RL = XL >>u amount | XH << (32 - amount)
-        or r4, r4, r0
-        sraw r3, r3, r5
-        blr
-1:      addi r6, r5, -32        # amount >= 32
-        sraw r4, r3, r6         # RL = XH >>s (amount - 32)
-        srawi r3, r3, 31        # RL = sign extension of XH
-        blr
-        .type __compcert_i64_sar, @function
-        .size __compcert_i64_sar, .-__compcert_i64_sar
-
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_sdiv.s b/runtime/powerpc/i64_sdiv.s
deleted file mode 100644
index 9787ea3b..00000000
--- a/runtime/powerpc/i64_sdiv.s
+++ /dev/null
@@ -1,71 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Signed division	
-	
-        .balign 16
-        .globl __compcert_i64_sdiv
-__compcert_i64_sdiv:
-	mflr r0
-        stw r0, 4(r1)           # save return address in caller's frame
-        xor r0, r3, r5          # compute sign of result (top bit)
-	mtctr r0                # save it in CTR (why not?)
-        srawi r0, r3, 31        # take absolute value of N
-        xor r4, r4, r0          # (i.e.  N = N ^ r0 - r0,
-        xor r3, r3, r0          #  where r0 = 0 if N >= 0 and r0 = -1 if N < 0)
-        subfc r4, r0, r4
-        subfe r3, r0, r3
-        srawi r0, r5, 31        # take absolute value of D
-        xor r6, r6, r0          # (same trick)
-        xor r5, r5, r0
-        subfc r6, r0, r6
-        subfe r5, r0, r5
-        bl __compcert_i64_udivmod        # do unsigned division
-        lwz r0, 4(r1)
-        mtlr r0                 # restore return address
-        mfctr r0
-        srawi r0, r0, 31        # apply expected sign to quotient
-        xor r6, r6, r0          # RES = Q if CTR >= 0, -Q if CTR < 0
-        xor r5, r5, r0
-        subfc r4, r0, r6
-        subfe r3, r0, r5
-        blr
-        .type __compcert_i64_sdiv, @function
-        .size __compcert_i64_sdiv, .-__compcert_i64_sdiv
-	
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_shl.s b/runtime/powerpc/i64_shl.s
deleted file mode 100644
index f6edb6c2..00000000
--- a/runtime/powerpc/i64_shl.s
+++ /dev/null
@@ -1,64 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-# Shift left
-	
-        .balign 16
-        .globl __compcert_i64_shl
-__compcert_i64_shl:
-# On PowerPC, shift instructions with amount mod 64 >= 32 return 0
-# hi = (hi << amount) | (lo >> (32 - amount)) | (lo << (amount - 32))
-# lo = lo << amount
-# if 0 <= amount < 32:
-#    (amount - 32) mod 64 >= 32, hence lo << (amount - 32) == 0
-# if 32 <= amount < 64:
-#    lo << amount == 0
-#    (32 - amount) mod 64 >= 32, hence lo >> (32 - amount) == 0
-        andi. r5, r5, 63        # take amount modulo 64
-        subfic r6, r5, 32       # r6 = 32 - amount
-        addi r7, r5, -32        # r7 = amount - 32
-        slw r3, r3, r5
-        srw r0, r4, r6
-        or r3, r3, r0
-        slw r0, r4, r7
-        or r3, r3, r0
-        slw r4, r4, r5
-        blr
-        .type __compcert_i64_shl, @function
-        .size __compcert_i64_shl, .-__compcert_i64_shl
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_shr.s b/runtime/powerpc/i64_shr.s
deleted file mode 100644
index b634aafd..00000000
--- a/runtime/powerpc/i64_shr.s
+++ /dev/null
@@ -1,65 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-# Shift right unsigned
-	
-        .balign 16
-        .globl __compcert_i64_shr
-__compcert_i64_shr:
-# On PowerPC, shift instructions with amount mod 64 >= 32 return 0
-# lo = (lo >> amount) | (hi << (32 - amount)) | (hi >> (amount - 32))
-# hi = hi >> amount
-# if 0 <= amount < 32:
-#    (amount - 32) mod 64 >= 32, hence hi >> (amount - 32) == 0
-# if 32 <= amount < 64:
-#    hi >> amount == 0
-#    (32 - amount) mod 64 >= 32, hence hi << (32 - amount) == 0
-        andi. r5, r5, 63        # take amount modulo 64
-        subfic r6, r5, 32       # r6 = 32 - amount
-        addi r7, r5, -32        # r7 = amount - 32
-        srw r4, r4, r5
-        slw r0, r3, r6
-        or r4, r4, r0
-        srw r0, r3, r7
-        or r4, r4, r0
-        srw r3, r3, r5
-        blr
-        .type __compcert_i64_shr, @function
-        .size __compcert_i64_shr, .-__compcert_i64_shr
-	
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_smod.s b/runtime/powerpc/i64_smod.s
deleted file mode 100644
index 6b4e1f89..00000000
--- a/runtime/powerpc/i64_smod.s
+++ /dev/null
@@ -1,70 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-## Signed remainder	
-	
-        .balign 16
-        .globl __compcert_i64_smod
-__compcert_i64_smod:
-	mflr r0
-        stw r0, 4(r1)           # save return address in caller's frame
-	mtctr r3                # save sign of result in CTR (sign of N)
-        srawi r0, r3, 31        # take absolute value of N
-        xor r4, r4, r0          # (i.e.  N = N ^ r0 - r0,
-        xor r3, r3, r0          #  where r0 = 0 if N >= 0 and r0 = -1 if N < 0)
-        subfc r4, r0, r4
-        subfe r3, r0, r3
-        srawi r0, r5, 31        # take absolute value of D
-        xor r6, r6, r0          # (same trick)
-        xor r5, r5, r0
-        subfc r6, r0, r6
-        subfe r5, r0, r5
-        bl __compcert_i64_udivmod        # do unsigned division
-        lwz r0, 4(r1)
-        mtlr r0                 # restore return address
-        mfctr r0
-        srawi r0, r0, 31        # apply expected sign to remainder
-        xor r4, r4, r0          # RES = R if CTR >= 0, -Q if CTR < 0
-        xor r3, r3, r0
-        subfc r4, r0, r4
-        subfe r3, r0, r3
-        blr
-        .type __compcert_i64_smod, @function
-        .size __compcert_i64_smod, .-__compcert_i64_smod
-
-        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_smulh.s b/runtime/powerpc/i64_smulh.s
deleted file mode 100644
index 73393fce..00000000
--- a/runtime/powerpc/i64_smulh.s
+++ /dev/null
@@ -1,80 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris
-#
-# Copyright (c) 2016 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Signed multiply-high
-
-# Hacker's Delight section 8.3:
-# - compute high 64 bits of the unsigned product X * Y  (see i64_umulh.S)
-# - subtract X if Y < 0
-# - subtract Y if X < 0
-
-        .balign 16
-        .globl __compcert_i64_smulh
-__compcert_i64_smulh:
-# r7:r8:r9 accumulate bits 127:32 of the full unsigned product
-        mulhwu  r9, r4, r6        # r9 = high half of XL.YL
-        mullw   r0, r4, r5        # r0 = low half of XL.YH
-        addc    r9, r9, r0
-        mulhwu  r0, r4, r5        # r0 = high half of XL.YH
-        addze   r8, r0
-        mullw   r0, r3, r6        # r0 = low half of XH.YL
-        addc    r9, r9, r0
-        mulhwu  r0, r3, r6        # r0 = high half of XH.YL
-        adde    r8, r8, r0
-        li      r7, 0
-        addze   r7, r7
-        mullw   r0, r3, r5        # r0 = low half of XH.YH
-        addc    r8, r8, r0
-        mulhwu  r0, r3, r5        # r0 = high half of XH.YH
-        adde    r7, r7, r0
-# Here r7:r8 contains the high 64 bits of the unsigned product.
-# Now, test signs and subtract if needed
-        srawi   r0, r3, 31        # r0 = -1 if X < 0, r0 = 0 if X >= 0
-        srawi   r9, r5, 31        # r9 = -1 if Y < 0, r9 = 0 if Y >= 0
-        and     r3, r3, r9        # set X = 0 if Y >= 0
-        and     r4, r4, r9
-        and     r5, r5, r0        # set Y = 0 if X >= 0
-        and     r6, r6, r0
-        subfc   r8, r4, r8        # subtract X
-        subfe   r7, r3, r7
-        subfc   r4, r6, r8        # subtract Y
-        subfe   r3, r5, r7
-        blr
-        .type __compcert_i64_smulh, @function
-        .size __compcert_i64_smulh, .-__compcert_i64_smulh
-
diff --git a/runtime/powerpc/i64_stod.s b/runtime/powerpc/i64_stod.s
deleted file mode 100644
index 0c1ab720..00000000
--- a/runtime/powerpc/i64_stod.s
+++ /dev/null
@@ -1,67 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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.
-
-### Conversion from signed long to double float	
-
-        .balign 16
-        .globl __compcert_i64_stod
-__compcert_i64_stod:
-        addi r1, r1, -16
-        lis r5, 0x4330
-        li r6, 0
-        stw r5, 0(r1)
-        stw r4, 4(r1)           # 0(r1) = 2^52 + (double) XL
-        stw r5, 8(r1)
-        stw r6, 12(r1)          # 8(r1) = 2^52
-        lfd f1, 0(r1)
-        lfd f2, 8(r1)
-        fsub f1, f1, f2         # f1 is XL (unsigned) as a double
-        lis r5, 0x4530
-        lis r6, 0x8000
-        stw r5, 0(r1)           # 0(r1) = 2^84 + ((double)XH - 2^31) * 2^32
-        add r3, r3, r6
-        stw r3, 4(r1)
-        stw r5, 8(r1)           # 8(r1) = 2^84 + 2^31 * 2^32
-        stw r6, 12(r1)
-        lfd f2, 0(r1)
-        lfd f3, 8(r1)
-        fsub f2, f2, f3         # f2 is XH (signed) * 2^32 as a double
-        fadd f1, f1, f2         # add both to get result
-        addi r1, r1, 16
-        blr
-        .type __compcert_i64_stod, @function
-        .size __compcert_i64_stod, .-__compcert_i64_stod
-
diff --git a/runtime/powerpc/i64_stof.s b/runtime/powerpc/i64_stof.s
deleted file mode 100644
index 97fa6bb8..00000000
--- a/runtime/powerpc/i64_stof.s
+++ /dev/null
@@ -1,68 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 signed long to single float	
-
-        .balign 16
-        .globl __compcert_i64_stof
-__compcert_i64_stof:
-	mflr r9
-   # Check whether -2^53 <= X < 2^53	
-        srawi r5, r3, 31
-        srawi r6, r3, 21        # (r5,r6) = X >> 53
-        addic r6, r6, 1
-        addze r5, r5            # (r5,r6) = (X >> 53) + 1
-        cmplwi r5, 2
-        blt 1f
-   # X is large enough that double rounding can occur.
-   # Avoid it by nudging X away from the points where double rounding
-   # occurs (the "round to odd" technique)
-        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
-        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
-   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
-   # bits 13-31 of r0 are 0
-        or r4, r4, r0           # correct bit number 12 of X
-        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
-   # Convert to double, then round to single	
-1:      bl __compcert_i64_stod
-        mtlr r9
-        frsp f1, f1
-        blr
-        .type __compcert_i64_stof, @function
-        .size __compcert_i64_stof, .-__compcert_i64_stof
-	
diff --git a/runtime/powerpc/i64_udiv.s b/runtime/powerpc/i64_udiv.s
deleted file mode 100644
index e2da855a..00000000
--- a/runtime/powerpc/i64_udiv.s
+++ /dev/null
@@ -1,54 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Unsigned division	
-
-        .balign 16
-        .globl __compcert_i64_udiv
-__compcert_i64_udiv:
-	mflr r0
-        stw r0, 4(r1)           # save return address in caller's frame
-        bl __compcert_i64_udivmod        # unsigned divide
-        lwz r0, 4(r1)
-        mtlr r0                 # restore return address
-        mr r3, r5               # result = quotient
-        mr r4, r6
-        blr
-        .type __compcert_i64_udiv, @function
-        .size __compcert_i64_udiv, .-__compcert_i64_udiv
-
diff --git a/runtime/powerpc/i64_udivmod.s b/runtime/powerpc/i64_udivmod.s
deleted file mode 100644
index e81c6cef..00000000
--- a/runtime/powerpc/i64_udivmod.s
+++ /dev/null
@@ -1,234 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-	
-# Unsigned division and modulus
-
-# This function computes both the quotient and the remainder of two
-# unsigned 64-bit integers.
-
-# Input:  numerator N in (r3,r4), divisor D in (r5,r6)
-# Output: quotient Q in (r5,r6),  remainder R in (r3,r4)
-# Destroys: all integer caller-save registers
-	
-	.globl  __compcert_i64_udivmod
-	.balign 16
-__compcert_i64_udivmod:
-        cmplwi  r5, 0           # DH == 0 ?
-	stwu    r1, -32(r1)
-        mflr    r0
-        stw     r0, 8(r1)
-        stw     r31, 12(r1)
-        beq     1f
-# The general case	
-        stw     r30, 16(r1)
-        stw     r29, 20(r1)
-        stw     r28, 24(r1)
-        mr      r28, r3         # Save N in (r28, r29)
-        mr      r29, r4
-        mr      r30, r5         # Save D in (r30, r31)
-        mr      r31, r6 
-  # Scale N and D down, giving N' and D', such that 2^31 <= D' < 2^32
-        cntlzw  r7, r5          # r7 = leading zeros in DH = 32 - shift amount
-        subfic  r8, r7, 32      # r8 = shift amount
-	slw     r0, r3, r7      # N' = N >> shift amount
-        srw     r3, r3, r8
-        srw     r4, r4, r8
-        or      r4, r4, r0
-	slw     r0, r5, r7      # D' = D >> shift amount
-        srw     r6, r6, r8
-        or      r5, r6, r0
-  # Divide N' by D' to get an approximate quotient Q
-        bl      __compcert_i64_udiv6432  # r3 = quotient, r4 = remainder
-        mr      r6, r3          # low half of quotient Q
-        li      r5, 0           # high half of quotient is 0
-  # Tentative quotient is either correct or one too high
-  # Compute Q * D in (r7, r8)
-4:      mullw   r7, r6, r30     # r7 = Q * DH
-        mullw   r8, r6, r31     # r8 = low 32 bits of Q * DL
-        mulhwu  r0, r6, r31     # r0 = high 32 bits of Q * DL
-        addc    r7, r7, r0
-        subfe.  r0, r0, r0      # test carry: EQ iff carry
-        beq     2f              # handle overflow case
-   # Compute R = N - Q * D, with borrow
-        subfc   r4, r8, r29
-        subfe   r3, r7, r28
-        subfe.  r0, r0, r0      # test borrow: EQ iff no borrow
-        beq     3f              # no borrow: N >= Q * D, we are good
-        addi    r6, r6, -1      # borrow: adjust Q down by 1
-        addc    r4, r4, r31     # and R up by D
-        adde    r3, r3, r30
-   # Finished	
-3:      lwz     r0, 8(r1)
-        mtlr    r0
-        lwz     r31, 12(r1)
-        lwz     r30, 16(r1)
-        lwz     r29, 20(r1)
-        lwz     r28, 24(r1)
-        addi    r1, r1, 32
-        blr
-   # Special case when Q * D overflows
-2:      addi    r6, r6, -1      # adjust Q down by 1
-        b       4b              # and redo computation and check of remainder
-	.balign 16
-# Special case 64 bits divided by 32 bits
-1:      cmplwi  r3, 0           # NH == 0?
-        beq     4f
-        divwu   r31, r3, r6     # Divide NH by DL, quotient QH in r31
-        mullw   r0, r31, r6
-        subf    r3, r0, r3      # NH is remainder of this division
-        mr      r5, r6
-        bl      __compcert_i64_udiv6432  # divide NH : NL by DL
-        mr      r5, r31         # high word of quotient
-        mr      r6, r3          # low word of quotient
-                                # r4 contains low word of remainder
-        li      r3, 0           # high word of remainder = 0
-	lwz     r0, 8(r1)
-        mtlr    r0
-        lwz     r31, 12(r1)
-        addi    r1, r1, 32
-        blr
-	.balign 16
-# Special case 32 bits divided by 32 bits
-4:      mr      r0, r6
-	divwu   r6, r4, r6      # low word of quotient
-	li      r5, 0           # high word of quotient is 0
-        mullw   r0, r6, r0
-        subf    r4, r0, r4      # low word of remainder
-        li      r3, 0           # high word of remainder is 0
-        addi    r1, r1, 32
-        blr
-        
-        .type __compcert_i64_udivmod, @function
-        .size __compcert_i64_udivmod, .-__compcert_i64_udivmod
-
-# Auxiliary division function: 64 bit integer divided by 32 bit integer	
-# Not exported
-# Input:  numerator N in (r3,r4), divisor D in r5
-# Output: quotient Q in r3, remainder R in r4
-# Destroys: all integer caller-save registers
-# Assumes: high word of N is less than D	
-        
-	.balign 16
-__compcert_i64_udiv6432: 
-# Algorithm 9.3 from Hacker's Delight, section 9.4	
-# Initially: u1 in r3, u0 in r4, v in r5
-#   s = __builtin_clz(v);
-	cntlzw  r6, r5          # s in r6
-#   v = v << s;
-        slw     r5, r5, r6
-#   vn1 = v >> 16;              # vn1 in r7
-        srwi    r7, r5, 16
-#   vn0 = v & 0xFFFF;           # vn0 in r8
-        rlwinm  r8, r5, 0, 16, 31
-#   un32 = (u1 << s) | (u0 >> 32 - s);
-	subfic  r0, r6, 32
-        srw     r0, r4, r0
-        slw     r3, r3, r6     # u1 dies, un32 in r3
-        or      r3, r3, r0
-#   un10 = u0 << s;
-        slw     r4, r4, r6     # u0 dies, un10 in r4
-#   un1 = un10 >> 16;
-        srwi    r9, r4, 16     # un1 in r9
-#   un0 = un10 & 0xFFFF;
-        rlwinm  r4, r4, 0, 16, 31 # un10 dies, un0 in r4
-#   q1 = un32/vn1;
-        divwu   r10, r3, r7    # q in r10
-#   rhat = un32 - q1*vn1;
-        mullw   r0, r10, r7
-        subf    r11, r0, r3    # rhat in r11
-#  again1:
-1:      
-#   if (q1 >= b || q1*vn0 > b*rhat + un1) {
-        cmplwi  r10, 0xFFFF
-        bgt     2f
-        mullw   r0, r10, r8
-        slwi    r12, r11, 16
-        add     r12, r12, r9
-        cmplw   r0, r12
-        ble     3f
-2:      
-#     q1 = q1 - 1;
-        addi    r10, r10, -1
-#     rhat = rhat + vn1;
-        add     r11, r11, r7
-#     if (rhat < b) goto again1;}
-        cmplwi  r11, 0xFFFF
-        ble     1b
-3:      
-#   un21 = un32*b + un1 - q1*v;
-        slwi    r0, r3, 16     # un32 dies
-        add     r9, r0, r9     # un1 dies
-        mullw   r0, r10, r5
-        subf    r9, r0, r9     # un21 in r9
-#   q0 = un21/vn1;
-	divwu   r3, r9, r7     # q0 in r3
-#   rhat = un21 - q0*vn1;
-        mullw   r0, r3, r7
-        subf    r11, r0, r9    # rhat in r11
-# again2:
-4:      
-#   if (q0 >= b || q0*vn0 > b*rhat + un0) {
-        cmplwi  r3, 0xFFFF
-        bgt     5f
-        mullw   r0, r3, r8
-        slwi    r12, r11, 16
-        add     r12, r12, r4
-        cmplw   r0, r12
-        ble     6f
-5:      
-#     q0 = q0 - 1;
-	addi    r3, r3, -1
-#     rhat = rhat + vn1;
-        add     r11, r11, r7
-#     if (rhat < b) goto again2;}
-	cmplwi  r11, 0xFFFF
-        ble     4b
-6:      
-#   remainder = (un21*b + un0 - q0*v) >> s;
-        slwi    r0, r9, 16
-        add     r4, r0, r4  # un0 dies, remainder in r4
-        mullw   r0, r3, r5
-        subf    r4, r0, r4
-        srw     r4, r4, r6
-#   quotient = q1*b + q0;
-        slwi    r0, r10, 16
-        add     r3, r0, r3
-        blr
-
-	.type	__compcert_i64_udiv6432, @function
-	.size	__compcert_i64_udiv6432,.-__compcert_i64_udiv6432
diff --git a/runtime/powerpc/i64_umod.s b/runtime/powerpc/i64_umod.s
deleted file mode 100644
index bf8d6121..00000000
--- a/runtime/powerpc/i64_umod.s
+++ /dev/null
@@ -1,47 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Unsigned modulus
-
-        .balign 16
-        .globl __compcert_i64_umod
-__compcert_i64_umod:
-        b __compcert_i64_udivmod
-        .type __compcert_i64_umod, @function
-        .size __compcert_i64_umod, .-__compcert_i64_umod
-
diff --git a/runtime/powerpc/i64_umulh.s b/runtime/powerpc/i64_umulh.s
deleted file mode 100644
index 53b72948..00000000
--- a/runtime/powerpc/i64_umulh.s
+++ /dev/null
@@ -1,65 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris
-#
-# Copyright (c) 2016 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
-
-### Unsigned multiply-high
-
-# X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL
-
-        .balign 16
-        .globl __compcert_i64_umulh
-__compcert_i64_umulh:
-# r7:r8:r9 accumulate bits 127:32 of the full product
-        mulhwu  r9, r4, r6        # r9 = high half of XL.YL
-        mullw   r0, r4, r5        # r0 = low half of XL.YH
-        addc    r9, r9, r0
-        mulhwu  r0, r4, r5        # r0 = high half of XL.YH
-        addze   r8, r0
-        mullw   r0, r3, r6        # r0 = low half of XH.YL
-        addc    r9, r9, r0
-        mulhwu  r0, r3, r6        # r0 = high half of XH.YL
-        adde    r8, r8, r0
-        li      r7, 0
-        addze   r7, r7
-        mullw   r0, r3, r5        # r0 = low half of XH.YH
-        addc    r4, r8, r0
-        mulhwu  r0, r3, r5        # r0 = high half of XH.YH
-        adde    r3, r7, r0
-        blr
-        .type __compcert_i64_umulh, @function
-        .size __compcert_i64_umulh, .-__compcert_i64_umulh
-
diff --git a/runtime/powerpc/i64_utod.s b/runtime/powerpc/i64_utod.s
deleted file mode 100644
index 69de6fdb..00000000
--- a/runtime/powerpc/i64_utod.s
+++ /dev/null
@@ -1,66 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 double float	
-
-        .balign 16
-        .globl __compcert_i64_utod
-__compcert_i64_utod:
-        addi r1, r1, -16
-        lis r5, 0x4330
-        li r6, 0
-        stw r5, 0(r1)
-        stw r4, 4(r1)           # 0(r1) = 2^52 + (double) XL
-        stw r5, 8(r1)
-        stw r6, 12(r1)          # 8(r1) = 2^52
-        lfd f1, 0(r1)
-        lfd f2, 8(r1)
-        fsub f1, f1, f2         # f1 is (double) XL
-        lis r5, 0x4530
-        stw r5, 0(r1)           # 0(r1) = 2^84 + (double) XH * 2^32
-        stw r3, 4(r1)
-        stw r5, 8(r1)           # 8(r1) = 2^84
-        lfd f2, 0(r1)
-        lfd f3, 8(r1)
-        fsub f2, f2, f3         # f2 is XH * 2^32 as a double
-        fadd f1, f1, f2         # add both to get result
-        addi r1, r1, 16
-        blr
-        .type __compcert_i64_utod, @function
-        .size __compcert_i64_utod, .-__compcert_i64_utod
-	
diff --git a/runtime/powerpc/i64_utof.s b/runtime/powerpc/i64_utof.s
deleted file mode 100644
index cdb2f867..00000000
--- a/runtime/powerpc/i64_utof.s
+++ /dev/null
@@ -1,64 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 __compcert_i64_utof
-__compcert_i64_utof:
-	mflr r9
-   # Check whether X < 2^53	
-        andis. r0, r3, 0xFFE0       # test bits 53...63 of X
-        beq 1f
-   # X is large enough that double rounding can occur.
-   # Avoid it by nudging X away from the points where double rounding
-   # occurs (the "round to odd" technique)
-        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
-        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
-   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
-   # bits 13-31 of r0 are 0
-        or r4, r4, r0           # correct bit number 12 of X
-        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
-   # Convert to double, then round to single	
-1:      bl __compcert_i64_utod
-        mtlr r9
-        frsp f1, f1
-        blr
-        .type __compcert_i64_utof, @function
-        .size __compcert_i64_utof, .-__compcert_i64_utof
-	
diff --git a/runtime/powerpc/vararg.s b/runtime/powerpc/vararg.s
deleted file mode 100644
index 8d7e62c8..00000000
--- a/runtime/powerpc/vararg.s
+++ /dev/null
@@ -1,163 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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
diff --git a/runtime/powerpc64/i64_dtou.s b/runtime/powerpc64/i64_dtou.s
deleted file mode 100644
index e58bcfaf..00000000
--- a/runtime/powerpc64/i64_dtou.s
+++ /dev/null
@@ -1,66 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 __compcert_i64_dtou
-__compcert_i64_dtou:
-        lis r0, 0x5f00          # 0x5f00_0000 = 2^63 in binary32 format
-        stwu r0, -16(r1)
-        lfs f2, 0(r1)           # f2 = 2^63
-        fcmpu cr0, f1, f2       # crbit 0 is f1 < f2
-        bf 0, 1f                # branch if f1 >= 2^63 (or f1 is NaN)
-	fctidz f1, f1           # convert as signed
-        stfd f1, 0(r1)
-        lwz r3, 0(r1)
-        lwz r4, 4(r1)
-        addi r1, r1, 16
-        blr
-1:      fsub f1, f1, f2         # shift argument down by 2^63
-	fctidz f1, f1           # convert as signed
-        stfd f1, 0(r1)
-        lwz r3, 0(r1)
-        lwz r4, 4(r1)
-        addis r3, r3, 0x8000    # shift result up by 2^63
-        addi r1, r1, 16
-        blr
-        .type __compcert_i64_dtou, @function
-        .size __compcert_i64_dtou, .-__compcert_i64_dtou
-
-        
diff --git a/runtime/powerpc64/i64_stof.s b/runtime/powerpc64/i64_stof.s
deleted file mode 100644
index 779cbc18..00000000
--- a/runtime/powerpc64/i64_stof.s
+++ /dev/null
@@ -1,68 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 __compcert_i64_stof
-__compcert_i64_stof:
-        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-   # Check whether -2^53 <= X < 2^53	
-        sradi r5, r4, 53
-        addi r5, r5, 1
-        cmpldi r5, 2
-	blt 1f
-   # X is large enough that double rounding can occur.
-   # Avoid it by nudging X away from the points where double rounding
-   # occurs (the "round to odd" technique)
-        rldicl r5, r4, 0, 53     # extract bits 0 to 11 of X
-        addi r5, r5, 0x7FF       # r5 = (X & 0x7FF) + 0x7FF
-   # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
-   # bits 13-63 of r5 are 0
-        or r4, r4, r5            # correct bit number 12 of X
-        rldicr r4, r4, 0, 52     # set to 0 bits 0 to 11 of X
-   # Convert to double, then round to single
-1:      stdu r4, -16(r1)
-        lfd f1, 0(r1)
-        fcfid f1, f1
-	frsp f1, f1
-        addi r1, r1, 16
-        blr
-        .type __compcert_i64_stof, @function
-        .size __compcert_i64_stof, .-__compcert_i64_stof
-	
diff --git a/runtime/powerpc64/i64_utod.s b/runtime/powerpc64/i64_utod.s
deleted file mode 100644
index 491ee26b..00000000
--- a/runtime/powerpc64/i64_utod.s
+++ /dev/null
@@ -1,79 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 __compcert_i64_utod
-__compcert_i64_utod:
-	rldicl r3, r3, 0, 32    # clear top 32 bits
-	rldicl r4, r4, 0, 32    # clear top 32 bits
-	lis r5, 0x4f80          # 0x4f80_0000 = 2^32 in binary32 format
-        stdu r3, -32(r1)
-        std r4, 8(r1)
-        stw r5, 16(r1)
-        lfd f1, 0(r1)           # high 32 bits of argument
-        lfd f2, 8(r1)           # low 32 bits of argument
-	lfs f3, 16(r1)          # 2^32
-        fcfid f1, f1            # convert both 32-bit halves to FP (exactly)
-	fcfid f2, f2
-        fmadd f1, f1, f3, f2    # compute hi * 2^32 + lo
-        addi r1, r1, 32
-        blr
-        .type __compcert_i64_utod, @function
-        .size __compcert_i64_utod, .-__compcert_i64_utod
-	
-# Alternate implementation using round-to-odd:
-#       rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
-#       cmpdi r4, 0            # is r4 >= 2^63 ?
-#       blt 1f
-#	stdu r4, -16(r1)       # r4 < 2^63: convert as signed
-#       lfd f1, 0(r1)
-#       fcfid f1, f1
-#       addi r1, r1, 16
-#       blr
-#1:     rldicl r0, r4, 0, 63   # extract low bit of r4
-#       srdi r4, r4, 1
-#       or r4, r4, r0          # round r4 to 63 bits, using round-to-odd
-#	stdu r4, -16(r1)       # convert to binary64
-#       lfd f1, 0(r1)
-#       fcfid f1, f1
-#       fadd f1, f1, f1        # multiply result by 2
-#       addi r1, r1, 16
-#       blr
-        
\ No newline at end of file
diff --git a/runtime/powerpc64/i64_utof.s b/runtime/powerpc64/i64_utof.s
deleted file mode 100644
index cdb2f867..00000000
--- a/runtime/powerpc64/i64_utof.s
+++ /dev/null
@@ -1,64 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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 __compcert_i64_utof
-__compcert_i64_utof:
-	mflr r9
-   # Check whether X < 2^53	
-        andis. r0, r3, 0xFFE0       # test bits 53...63 of X
-        beq 1f
-   # X is large enough that double rounding can occur.
-   # Avoid it by nudging X away from the points where double rounding
-   # occurs (the "round to odd" technique)
-        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
-        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
-   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
-   # bits 13-31 of r0 are 0
-        or r4, r4, r0           # correct bit number 12 of X
-        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
-   # Convert to double, then round to single	
-1:      bl __compcert_i64_utod
-        mtlr r9
-        frsp f1, f1
-        blr
-        .type __compcert_i64_utof, @function
-        .size __compcert_i64_utof, .-__compcert_i64_utof
-	
diff --git a/runtime/powerpc64/vararg.s b/runtime/powerpc64/vararg.s
deleted file mode 100644
index 8d7e62c8..00000000
--- a/runtime/powerpc64/vararg.s
+++ /dev/null
@@ -1,163 +0,0 @@
-# *****************************************************************
-#
-#               The Compcert verified compiler
-#
-#           Xavier Leroy, INRIA Paris-Rocquencourt
-#
-# Copyright (c) 2013 Institut National de Recherche en Informatique et
-#  en Automatique.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#     * Redistributions of source code must retain the above copyright
-#       notice, this list of conditions and the following disclaimer.
-#     * Redistributions in binary form must reproduce the above copyright
-#       notice, this list of conditions and the following disclaimer in the
-#       documentation and/or other materials provided with the distribution.
-#     * Neither the name of the <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