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.

15 files changed, 200 insertions, 435 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index b819991d..213779a4 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -10,8 +10,18 @@ ARCH=x86_32
 endif
 endif
 
+ifeq ($(ARCH),powerpc)
+ifeq ($(MODEL),ppc64)
+ARCH=powerpc64
+else ifeq ($(MODEL),e5500)
+ARCH=powerpc64
+endif
+endif
+
 ifeq ($(ARCH),x86_64)
 OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o
+else ifeq ($(ARCH),powerpc64)
+OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o
 else
 OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
   i64_shr.o i64_smod.o i64_stod.o i64_stof.o \
@@ -28,14 +38,6 @@ INCLUDES=include/float.h include/stdarg.h include/stdbool.h \
 
 VPATH=$(ARCH)
 
-ifeq ($(ARCH),powerpc)
-ifeq ($(MODEL),ppc64)
-VPATH=powerpc/ppc64 $(ARCH)
-else ifeq ($(MODEL),e5500)
-VPATH=powerpc/ppc64 $(ARCH)
-endif
-endif
-
 ifeq ($(strip $(HAS_RUNTIME_LIB)),true)
 all: $(LIB)
 else
diff --git a/runtime/README b/runtime/README
index 5d824300..f38ed894 100644
--- a/runtime/README
+++ b/runtime/README
@@ -1,11 +1,11 @@
 This is the support library for CompCert-generated code.
+
 It provides helper functions for:
 - 64-bit integer arithmetic
 - implementing the va_arg macro from <stdarg.h>
 
 The implementation is written in assembly language in the
-arm/ ia32/ powerpc/ directories.
+arm/ powerpc/ powerpc64/ riscV/ x86_32/ x86_64/ directories.
 
 The c/ directory contains a C implementation of the 64-bit integer functions.
 It is provided for reference and as a guide for the asm implementations.
-
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_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_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_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_dtou.s b/runtime/powerpc64/i64_dtou.s
index 60d5c9bf..60d5c9bf 100644
--- a/runtime/powerpc/ppc64/i64_dtou.s
+++ b/runtime/powerpc64/i64_dtou.s
diff --git a/runtime/powerpc/ppc64/i64_stof.s b/runtime/powerpc64/i64_stof.s
index 8830d594..8830d594 100644
--- a/runtime/powerpc/ppc64/i64_stof.s
+++ b/runtime/powerpc64/i64_stof.s
diff --git a/runtime/powerpc/ppc64/i64_utod.s b/runtime/powerpc64/i64_utod.s
index ddde91dd..ddde91dd 100644
--- a/runtime/powerpc/ppc64/i64_utod.s
+++ b/runtime/powerpc64/i64_utod.s
diff --git a/runtime/powerpc/ppc64/i64_smod.s b/runtime/powerpc64/i64_utof.s
index 35be366d..2617cbda 100644
--- a/runtime/powerpc/ppc64/i64_smod.s
+++ b/runtime/powerpc64/i64_utof.s
@@ -32,23 +32,33 @@
 #
 # *********************************************************************
 
-# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
 
         .text
 
-## Signed remainder	
-	
+### Conversion from unsigned long to single float	
+
         .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)
+        .globl __i64_utof
+__i64_utof:
+	mflr r9
+   # Check whether X < 2^53	
+        andis. r0, r3, 0xFFE0       # test bits 53...63 of X
+        beq 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r0 are 0
+        or r4, r4, r0           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+1:      bl __i64_utod
+        mtlr r9
+        frsp f1, f1
         blr
-        .type __i64_smod, @function
-        .size __i64_smod, .-__i64_smod
-
-        
\ No newline at end of file
+        .type __i64_utof, @function
+        .size __i64_utof, .-__i64_utof
+	
diff --git a/runtime/powerpc64/vararg.s b/runtime/powerpc64/vararg.s
new file mode 100644
index 00000000..8d7e62c8
--- /dev/null
+++ b/runtime/powerpc64/vararg.s
@@ -0,0 +1,163 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for variadic functions <stdarg.h>.  IA32 version
+
+# typedef struct {
+#   unsigned char ireg;    // index of next integer register
+#   unsigned char freg;    // index of next FP register
+#   char * stk;            // pointer to next argument in stack
+#   struct {
+#     int iregs[8];
+#     double fregs[8];
+#   } * regs;              // pointer to saved register area
+# } va_list[1];
+#
+# unsigned int __compcert_va_int32(va_list ap);
+# unsigned long long __compcert_va_int64(va_list ap);
+# double __compcert_va_float64(va_list ap);
+
+        .text
+
+        .balign 16
+        .globl __compcert_va_int32
+__compcert_va_int32:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in an integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	addi    r4, r4, 1       # increment ap->ireg
+        stb     r4, 0(r3)
+        lwzx    r3, r5, r6      # load argument in r3
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+        addi    r5, r5, 4       # advance ap->stk by 4
+        stw     r5, 4(r3)
+	lwz     r3, -4(r5)      # load argument in r3
+        blr
+        .type   __compcert_va_int32, @function
+        .size   __compcert_va_int32, .-__compcert_va_int32
+
+        .balign 16
+        .globl __compcert_va_int64
+__compcert_va_int64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 7
+        bge     1f
+  # Next argument was passed in two consecutive integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+	addi    r4, r4, 3       # round r4 up to an even number and add 2
+        rlwinm  r4, r4, 0, 0, 30 
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	add     r5, r5, r6      # r5 = address of argument + 8
+        stb     r4, 0(r3)       # update ap->ireg
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	li      r4, 8
+        stb     r4, 0(r3)       # set ap->ireg = 8 so that no ireg is left
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+	stw     r5, 4(r3)       # update ap->stk
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+        .type   __compcert_va_int64, @function
+        .size   __compcert_va_int64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_float64
+__compcert_va_float64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 1(r3)       # r4 = ap->freg = next float register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in a FP register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 3, 0, 28 # r6 = r4 * 8
+	add     r5, r5, r6
+        lfd     f1, 32(r5)      # load argument in f1
+	addi    r4, r4, 1       # increment ap->freg
+        stb     r4, 1(r3)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+        lfd     f1, -8(r5)      # load argument in f1
+	stw     r5, 4(r3)       # update ap->stk
+        blr
+        .type   __compcert_va_float64, @function
+        .size   __compcert_va_float64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_composite
+__compcert_va_composite:
+	b       __compcert_va_int32
+        .type   __compcert_va_composite, @function
+        .size   __compcert_va_composite, .-__compcert_va_composite
+
+# Save integer and FP registers at beginning of vararg function        
+
+        .balign 16
+        .globl  __compcert_va_saveregs
+__compcert_va_saveregs:
+        lwz     r11, 0(r1)      # r11 point to top of our frame
+        stwu    r3, -96(r11)    # register save area is 96 bytes below
+        stw     r4, 4(r11)
+        stw     r5, 8(r11)
+        stw     r6, 12(r11)
+        stw     r7, 16(r11)
+        stw     r8, 20(r11)
+        stw     r9, 24(r11)
+        stw     r10, 28(r11)
+	bf      6, 1f           # don't save FP regs if CR6 bit is clear
+        stfd    f1, 32(r11)
+        stfd    f2, 40(r11)
+        stfd    f3, 48(r11)
+        stfd    f4, 56(r11)
+        stfd    f5, 64(r11)
+        stfd    f6, 72(r11)
+        stfd    f7, 80(r11)
+        stfd    f8, 88(r11)
+1:      blr
+        .type   __compcert_va_saveregs, @function
+        .size   __compcert_va_saveregs, .-__compcert_va_saveregs