Merge remote-tracking branch 'origin/mppa-work' into mppa-expect

28 files changed, 2040 insertions, 8 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index 0a18e0f8..3b1cabc4 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -28,6 +28,8 @@ OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o\
 		 i64_shl.o i64_shr.o
 # Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o
 DOMAKE:=$(shell (cd mppa_k1c && make))
+else ifeq ($(ARCH),aarch64)
+OBJS=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 \
diff --git a/runtime/aarch64/sysdeps.h b/runtime/aarch64/sysdeps.h
new file mode 100644
index 00000000..0cee9ae3
--- /dev/null
+++ b/runtime/aarch64/sysdeps.h
@@ -0,0 +1,45 @@
+// *****************************************************************
+//
+//               The Compcert verified compiler
+//
+//           Xavier Leroy, Collège de France and INRIA Paris
+//
+// Copyright (c) Institut National de Recherche en Informatique et
+//  en Automatique.
+//	
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//     * Redistributions of source code must retain the above copyright
+//       notice, this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//     * Neither the name of the <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.
+//
+// *********************************************************************
+
+// System dependencies
+
+#define FUNCTION(f) \
+	.text; \
+        .balign 16; \
+	.globl f; \
+f:
+
+#define ENDFUNCTION(f) \
+	.type f, @function; .size f, . - f
+
diff --git a/runtime/aarch64/vararg.S b/runtime/aarch64/vararg.S
new file mode 100644
index 00000000..b7347d65
--- /dev/null
+++ b/runtime/aarch64/vararg.S
@@ -0,0 +1,109 @@
+// *****************************************************************
+//
+//               The Compcert verified compiler
+//
+//           Xavier Leroy, Collège de France and INRIA Paris
+//
+// Copyright (c) Institut National de Recherche en Informatique et
+//  en Automatique.
+//	
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//     * Redistributions of source code must retain the above copyright
+//       notice, this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//     * Neither the name of the <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>.  AArch64 version.
+
+#include "sysdeps.h"	
+
+// typedef struct __va_list {
+//   void *__stack;             // next stack parameter
+//   void *__gr_top;            // top of the save area for int regs
+//   void *__vr_top;            // top of the save area for float regs
+//   int__gr_offs;              // offset from gr_top to next int reg
+//   int__vr_offs;              // offset from gr_top to next FP reg
+// }
+// typedef struct __va_list va_list;   // struct passed by reference
+// unsigned int __compcert_va_int32(va_list * ap);
+// unsigned long long __compcert_va_int64(va_list * ap);
+// double __compcert_va_float64(va_list * ap);
+
+FUNCTION(__compcert_va_int32)
+        ldr     w1, [x0, #24]   // w1 = gr_offs
+        cbz     w1, 1f
+  // gr_offs is not zero: load from int save area and update gr_offs
+        ldr     x2, [x0, #8]    // x2 = gr_top
+        ldr     w2, [x2, w1, sxtw] // w2 = the next integer
+        add     w1, w1, #8
+        str     w1, [x0, #24]   // update gr_offs
+        mov     w0, w2
+	ret
+  // gr_offs is zero: load from stack save area and update stack pointer
+1:      ldr     x1, [x0, #0]    // x1 = stack
+        ldr     w2, [x1, #0]    // w2 = the next integer
+        add     x1, x1, #8
+        str     x1, [x0, #0]    // update stack
+        mov     w0, w2
+	ret
+ENDFUNCTION(__compcert_va_int32)
+
+FUNCTION(__compcert_va_int64)
+        ldr     w1, [x0, #24]   // w1 = gr_offs
+        cbz     w1, 1f
+  // gr_offs is not zero: load from int save area and update gr_offs
+        ldr     x2, [x0, #8]    // x2 = gr_top
+        ldr     x2, [x2, w1, sxtw] // w2 = the next long integer
+        add     w1, w1, #8
+        str     w1, [x0, #24]   // update gr_offs
+        mov     x0, x2
+	ret
+  // gr_offs is zero: load from stack save area and update stack pointer
+1:      ldr     x1, [x0, #0]    // x1 = stack
+        ldr     x2, [x1, #0]    // w2 = the next long integer
+        add     x1, x1, #8
+        str     x1, [x0, #0]    // update stack
+        mov     x0, x2
+	ret
+ENDFUNCTION(__compcert_va_int64)
+
+FUNCTION(__compcert_va_float64)
+        ldr     w1, [x0, #28]   // w1 = vr_offs
+        cbz     w1, 1f
+  // vr_offs is not zero: load from float save area and update vr_offs
+        ldr     x2, [x0, #16]   // x2 = vr_top
+        ldr     d0, [x2, w1, sxtw] // d0 = the next float
+        add     w1, w1, #16
+        str     w1, [x0, #28]   // update vr_offs
+	ret
+  // gr_offs is zero: load from stack save area and update stack pointer
+1:      ldr     x1, [x0, #0]    // x1 = stack
+        ldr     d0, [x1, #0]    // d0 = the next float
+        add     x1, x1, #8
+        str     x1, [x0, #0]    // update stack
+	ret
+ENDFUNCTION(__compcert_va_float64)
+
+// Right now we pass structs by reference.  This is not ABI conformant.
+FUNCTION(__compcert_va_composite)
+	b	__compcert_va_int64
+ENDFUNCTION(__compcert_va_composite)
diff --git a/runtime/arm/i64_stof.S b/runtime/arm/i64_stof.S
index bcfa471c..11e00a2a 100644
--- a/runtime/arm/i64_stof.S
+++ b/runtime/arm/i64_stof.S
@@ -39,12 +39,11 @@
 @@@ Conversion from signed 64-bit integer to single float
 
 FUNCTION(__compcert_i64_stof)
-    @ Check whether -2^53 <= X < 2^53
-        ASR r2, Reg0HI, #21
-        ASR r3, Reg0HI, #31     @ (r2,r3) = X >> 53
+   @ Check whether -2^53 <= X < 2^53
+        ASR r2, Reg0HI, #21     @ r2 = high 32 bits of X >> 53
+   @ -2^53 <= X < 2^53 iff r2 is -1 or 0, that is, iff r2 + 1 is 0 or 1
         adds r2, r2, #1
-        adc r3, r3, #0          @ (r2,r3) = X >> 53 + 1
-        cmp r3, #2
+        cmp r2, #2
         blo 1f
    @ X is large enough that double rounding can occur.
    @ Avoid it by nudging X away from the points where double rounding
diff --git a/runtime/include/math.h b/runtime/include/math.h
index 060968c8..01b8d8d8 100644
--- a/runtime/include/math.h
+++ b/runtime/include/math.h
@@ -1,8 +1,12 @@
 #ifndef _COMPCERT_MATH_H
 #define _COMPCERT_MATH_H
 
+#ifdef __K1C__
+
 #define isfinite(__y) (fpclassify((__y)) >= FP_ZERO)
 
+#include_next <math.h>
+
 #ifndef COMPCERT_NO_FP_MACROS
 #define fmin(x, y) __builtin_fmin((x),(y))
 #define fmax(x, y) __builtin_fmax((x),(y))
@@ -14,5 +18,9 @@
 #define fmaf(x, y, z) __builtin_fmaf((x),(y),(z))
 #endif
 
+#else
+
 #include_next <math.h>
+
+#endif
 #endif
diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.s
index 9e23e0b3..65c1eab8 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.s
@@ -1,7 +1,7 @@
 
-// typedef void * va_list;
-// unsigned int __compcert_va_int32(va_list * ap);
-// unsigned long long __compcert_va_int64(va_list * ap);
+# typedef void * va_list;
+# unsigned int __compcert_va_int32(va_list * ap);
+# unsigned long long __compcert_va_int64(va_list * ap);
 
 	.text
 	.balign 2
diff --git a/runtime/powerpc/i64_dtos.s b/runtime/powerpc/i64_dtos.s
new file mode 100644
index 00000000..85c60b27
--- /dev/null
+++ b/runtime/powerpc/i64_dtos.s
@@ -0,0 +1,100 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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
new file mode 100644
index 00000000..67a721d4
--- /dev/null
+++ b/runtime/powerpc/i64_dtou.s
@@ -0,0 +1,92 @@
+# *****************************************************************
+#
+#               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
new file mode 100644
index 00000000..c7da448f
--- /dev/null
+++ b/runtime/powerpc/i64_sar.s
@@ -0,0 +1,60 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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
new file mode 100644
index 00000000..9787ea3b
--- /dev/null
+++ b/runtime/powerpc/i64_sdiv.s
@@ -0,0 +1,71 @@
+# *****************************************************************
+#
+#               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
new file mode 100644
index 00000000..f6edb6c2
--- /dev/null
+++ b/runtime/powerpc/i64_shl.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+# 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
new file mode 100644
index 00000000..b634aafd
--- /dev/null
+++ b/runtime/powerpc/i64_shr.s
@@ -0,0 +1,65 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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
new file mode 100644
index 00000000..6b4e1f89
--- /dev/null
+++ b/runtime/powerpc/i64_smod.s
@@ -0,0 +1,70 @@
+# *****************************************************************
+#
+#               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
new file mode 100644
index 00000000..73393fce
--- /dev/null
+++ b/runtime/powerpc/i64_smulh.s
@@ -0,0 +1,80 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris
+#
+# Copyright (c) 2016 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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
new file mode 100644
index 00000000..0c1ab720
--- /dev/null
+++ b/runtime/powerpc/i64_stod.s
@@ -0,0 +1,67 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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
new file mode 100644
index 00000000..ea23a1c8
--- /dev/null
+++ b/runtime/powerpc/i64_stof.s
@@ -0,0 +1,67 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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, 21        # r5 = high 32 bits of X >> 53
+   # -2^53 <= X < 2^53 iff r5 is -1 or 0, that is, iff r5 + 1 is 0 or 1
+        addi r5, r5, 1
+        cmplwi r5, 2
+        blt 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rlwinm r5, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r5, r5, 0x7FF      # r5 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r5 are 0
+        or r4, r4, r5           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+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
new file mode 100644
index 00000000..e2da855a
--- /dev/null
+++ b/runtime/powerpc/i64_udiv.s
@@ -0,0 +1,54 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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
new file mode 100644
index 00000000..e81c6cef
--- /dev/null
+++ b/runtime/powerpc/i64_udivmod.s
@@ -0,0 +1,234 @@
+# *****************************************************************
+#
+#               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
new file mode 100644
index 00000000..bf8d6121
--- /dev/null
+++ b/runtime/powerpc/i64_umod.s
@@ -0,0 +1,47 @@
+# *****************************************************************
+#
+#               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
new file mode 100644
index 00000000..53b72948
--- /dev/null
+++ b/runtime/powerpc/i64_umulh.s
@@ -0,0 +1,65 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris
+#
+# Copyright (c) 2016 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <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
new file mode 100644
index 00000000..69de6fdb
--- /dev/null
+++ b/runtime/powerpc/i64_utod.s
@@ -0,0 +1,66 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 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
new file mode 100644
index 00000000..4a2a172b
--- /dev/null
+++ b/runtime/powerpc/i64_utof.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from unsigned long to single float	
+
+        .balign 16
+        .globl __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 r5, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r5, r5, 0x7FF      # r5 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r5 are 0
+        or r4, r4, r5           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+1:      bl __compcert_i64_utod
+        mtlr r9
+        frsp f1, f1
+        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
new file mode 100644
index 00000000..8d7e62c8
--- /dev/null
+++ b/runtime/powerpc/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
diff --git a/runtime/powerpc64/i64_dtou.s b/runtime/powerpc64/i64_dtou.s
new file mode 100644
index 00000000..e58bcfaf
--- /dev/null
+++ b/runtime/powerpc64/i64_dtou.s
@@ -0,0 +1,66 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from double float to unsigned long	
+
+        .balign 16
+        .globl __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
new file mode 100644
index 00000000..779cbc18
--- /dev/null
+++ b/runtime/powerpc64/i64_stof.s
@@ -0,0 +1,68 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from signed long to single float	
+
+        .balign 16
+        .globl __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
new file mode 100644
index 00000000..491ee26b
--- /dev/null
+++ b/runtime/powerpc64/i64_utod.s
@@ -0,0 +1,79 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from unsigned long to double float	
+
+        .balign 16
+        .globl __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
new file mode 100644
index 00000000..4a2a172b
--- /dev/null
+++ b/runtime/powerpc64/i64_utof.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from unsigned long to single float	
+
+        .balign 16
+        .globl __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 r5, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r5, r5, 0x7FF      # r5 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r5 are 0
+        or r4, r4, r5           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+1:      bl __compcert_i64_utod
+        mtlr r9
+        frsp f1, f1
+        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
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