Merge pull request #145 from AbsInt/64

Support for 64-bit target processors + support for x86 in 64-bit mode

34 files changed, 1122 insertions, 0 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index c01ef38d..641c9fdc 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -1,11 +1,27 @@
 include ../Makefile.config
 
 CFLAGS=-O1 -g -Wall
+
+ifeq ($(ARCH),x86)
+ifeq ($(MODEL),64)
+ARCH=x86_64
+else
+ARCH=x86_32
+endif
+endif
+
+ifeq ($(ARCH),x86_64)
+OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o
+else
 OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
   i64_shr.o i64_smod.o i64_stod.o i64_stof.o \
   i64_udivmod.o i64_udiv.o i64_umod.o i64_utod.o i64_utof.o \
+  i64_smulh.o i64_umulh.o \
   vararg.o
+endif
+
 LIB=libcompcert.a
+
 INCLUDES=include/float.h include/stdarg.h include/stdbool.h \
   include/stddef.h include/varargs.h include/stdalign.h \
   include/stdnoreturn.h
diff --git a/runtime/arm/i64_smulh.S b/runtime/arm/i64_smulh.S
new file mode 100644
index 00000000..476f51ce
--- /dev/null
+++ b/runtime/arm/i64_smulh.S
@@ -0,0 +1,77 @@
+@ *****************************************************************
+@
+@               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.  ARM version.
+
+#include "sysdeps.h"
+
+@@@ Multiply-high signed
+
+@ 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
+
+FUNCTION(__i64_smulh)
+        push  {r4, r5, r6, r7}
+@@@ r7:r6 accumulate bits 95-32 of the full product	
+        umull r4, r6, Reg0LO, Reg1LO   @ r6 = high half of XL.YL product
+	umull r4, r5, Reg0LO, Reg1HI   @ r5:r4 = product XL.YH
+        adds  r6, r6, r4
+        ADC   r7, r5, #0               @ no carry out
+	umull r4, r5, Reg0HI, Reg1LO   @ r5:r4 = product XH.YL
+        adds  r6, r6, r4
+        adcs  r7, r7, r5               @ carry out is possible
+@@@ r6:r7 accumulate bits 127-64 of the full product
+        mov   r6, #0
+        ADC   r6, r6, #0               @ put carry out in bits 127-96
+	umull r4, r5, Reg0HI, Reg1HI   @ r5:r4 = product XH.YH
+        adds  r7, r7, r4
+        ADC   r6, r6, r5
+@@@ subtract X if Y < 0
+        cmp   Reg1HI, #0
+        bge   1f
+        subs  r7, r7, Reg0LO
+        sbcs  r6, r6, Reg0HI
+@@@ subtract Y if X < 0
+1:      cmp   Reg0HI, #0
+        bge 2f
+        subs  r7, r7, Reg1LO
+        sbcs  r6, r6, Reg1HI
+@@@ return result in Reg0 pair
+2:      mov   Reg0LO, r7
+        mov   Reg0HI, r6
+        pop   {r4, r5, r6, r7}
+        bx    lr
+ENDFUNCTION(__i64_smulh)
diff --git a/runtime/arm/i64_umulh.S b/runtime/arm/i64_umulh.S
new file mode 100644
index 00000000..c14f0c6b
--- /dev/null
+++ b/runtime/arm/i64_umulh.S
@@ -0,0 +1,61 @@
+@ *****************************************************************
+@
+@               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.  ARM version.
+
+#include "sysdeps.h"
+
+@@@ Multiply-high unsigned
+
+@ X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL
+
+FUNCTION(__i64_umulh)
+        push  {r4, r5, r6, r7}
+@@@ r7:r6 accumulate bits 95-32 of the full product	
+        umull r4, r6, Reg0LO, Reg1LO   @ r6 = high half of XL.YL product
+	umull r4, r5, Reg0LO, Reg1HI   @ r5:r4 = product XL.YH
+        adds  r6, r6, r4
+        ADC   r7, r5, #0               @ no carry out
+	umull r4, r5, Reg0HI, Reg1LO   @ r5:r4 = product XH.YL
+        adds  r6, r6, r4
+        adcs  r7, r7, r5               @ carry out is possible
+@@@ r6:r7 accumulate bits 127-64 of the full product
+        mov   r6, #0
+        ADC   r6, r6, #0               @ put carry out in bits 127-96
+	umull r4, r5, Reg0HI, Reg1HI   @ r5:r4 = product XH.YH
+        adds  Reg0LO, r7, r4
+        ADC   Reg0HI, r6, r5
+        pop   {r4, r5, r6, r7}
+        bx    lr
+ENDFUNCTION(__i64_umulh)
diff --git a/runtime/arm/sysdeps.h b/runtime/arm/sysdeps.h
index fd4ea61d..ae59f977 100644
--- a/runtime/arm/sysdeps.h
+++ b/runtime/arm/sysdeps.h
@@ -70,6 +70,7 @@ f:
 #define THUMB_S(x) x
 #endif
 
+#define ADC THUMB_S(adc)
 #define ADD THUMB_S(add)
 #define AND THUMB_S(and)
 #define ASR THUMB_S(asr)
diff --git a/runtime/c/i64.h b/runtime/c/i64.h
index dd584533..a75214fe 100644
--- a/runtime/c/i64.h
+++ b/runtime/c/i64.h
@@ -41,3 +41,5 @@ extern signed long long __i64_sar(signed long long x, int amount);
 extern unsigned long long __i64_udivmod(unsigned long long n,
                                         unsigned long long d,
                                         unsigned long long * rp);
+extern unsigned long long __i64_umulh(unsigned long long u,
+                                      unsigned long long v);
diff --git a/runtime/c/i64_smulh.c b/runtime/c/i64_smulh.c
new file mode 100644
index 00000000..b7a42474
--- /dev/null
+++ b/runtime/c/i64_smulh.c
@@ -0,0 +1,56 @@
+/*****************************************************************
+ *
+ *               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. Reference C implementation */
+
+#include "i64.h"
+
+typedef signed long long s64;
+typedef unsigned long long u64;
+
+/* Signed multiply high */
+
+/* Hacker's Delight section 8.3:
+ * - compute high 64 bits of the unsigned product X * Y
+ * - subtract X if Y < 0
+ * - subtract Y if X < 0 
+ */
+
+s64 __i64_smulh(s64 x, s64 y)
+{
+  s64 t = (s64) __i64_umulh(x, y);
+  if (y < 0) t = t - x;
+  if (x < 0) t = t - y;
+  return t;
+}
diff --git a/runtime/c/i64_umulh.c b/runtime/c/i64_umulh.c
new file mode 100644
index 00000000..d2394d09
--- /dev/null
+++ b/runtime/c/i64_umulh.c
@@ -0,0 +1,66 @@
+/*****************************************************************
+ *
+ *               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. Reference C implementation */
+
+#include "i64.h"
+
+typedef unsigned long long u64;
+typedef unsigned int u32;
+
+/* Unsigned multiply high */
+
+/* Hacker's Delight, algorithm 8.1, specialized to two 32-bit words */
+
+u64 __i64_umulh(u64 u, u64 v)
+{
+  u32 u0 = u, u1 = u >> 32;
+  u32 v0 = v, v1 = v >> 32;
+  u32 w1, w2, w3, k;
+  u64 t;
+
+  t = (u64) u0 * (u64) v0;
+  k = t >> 32;
+
+  t = (u64) u1 * (u64) v0 + k;
+  w1 = t;
+  w2 = t >> 32;
+
+  t = (u64) u0 * (u64) v1 + w1;
+  k = t >> 32;
+
+  t = (u64) u1 * (u64) v1 + w2 + k;
+
+  return t;
+}
diff --git a/runtime/powerpc/i64_smul.s b/runtime/powerpc/i64_smul.s
new file mode 100644
index 00000000..9eb453d4
--- /dev/null
+++ b/runtime/powerpc/i64_smul.s
@@ -0,0 +1,76 @@
+# *****************************************************************
+#
+#               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
+	
+# Reference C implementation in ../c/i64_smul.c
+
+        .balign 16
+        .globl __i64_smulh
+__i64_smulh:
+     # u1 in r3; u0 in r4; v1 in r5; v0 in r6
+     # First compute unsigned product (see i64_umul.s)
+        mulhwu   r0, r4, r6     # k (in r0) = high((u64) u0 * (u64) v0)
+        mullw    r8, r3, r6
+        mulhwu   r7, r3, r6     # t (in r8:r7) = (u64) u1 * (u64) v0
+        addc     r0, r8, r0     # w1 (in r0) = low (t + k)
+        addze    r9, r7         # w2 (in r9) = high (t + k)
+        mullw    r8, r4, r5
+        mulhwu   r7, r4, r5     # t (in r8:r7) = (u64) u0 * (u64) v1
+        addc     r0, r8, r0     # tmp (in r0) = low (t + w1)
+        addze    r0, r7         # k (in r0) = high(t + w1)
+        mullw    r8, r3, r5
+        mulhwu   r7, r3, r5     # t (in r8:r7) = (u64) u1 * (u64) v1
+        addc     r8, r8, r9     # add w2
+        addze    r7, r7
+        addc     r8, r8, r0     # add k
+        addze    r7, r7
+     # Here r8:r7 contains the high 64 bits of the unsigned product
+        srawi    r0, r3, 31     # r0 = 0 if U >= 0, -1 if U < 0
+        srawi    r9, r5, 31     # r9 = 0 if V >= 0, -1 if V < 0
+        and      r3, r3, r9
+        and      r4, r4, r9     # r3:r4 = U if V < 0, = 0 if V >= 0
+        and      r5, r5, r0
+        and      r6, r6, r0     # r5:r6 = V if U < 0, = 0 if U >= 0
+        subfc    r8, r4, r8
+        subfe    r7, r3, r7
+        subfc    r4, r6, r8
+        subfe    r3, r5, r7     # result is r8:r7 - r3:r4 - r5:r6
+        blr
+        .type __i64_umulh, @function
+        .size __i64_umulh, .-__i64_umulh
diff --git a/runtime/powerpc/i64_smulh.s b/runtime/powerpc/i64_smulh.s
new file mode 100644
index 00000000..4dc97a48
--- /dev/null
+++ b/runtime/powerpc/i64_smulh.s
@@ -0,0 +1,79 @@
+# *****************************************************************
+#
+#               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 __i64_smulh
+__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
+# Test signs
+        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 __i64_smulh, @function
+        .size __i64_smulh, .-__i64_smulh
+
diff --git a/runtime/powerpc/i64_umul.s b/runtime/powerpc/i64_umul.s
new file mode 100644
index 00000000..e734b93c
--- /dev/null
+++ b/runtime/powerpc/i64_umul.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               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
+	
+# Reference C implementation in ../c/i64_umul.c
+
+        .balign 16
+        .globl __i64_umulh
+__i64_umulh:
+     # u1 in r3; u0 in r4; v1 in r5; v0 in r6
+        mulhwu   r0, r4, r6     # k (in r0) = high((u64) u0 * (u64) v0)
+        mullw    r8, r3, r6
+        mulhwu   r7, r3, r6     # t (in r8:r7) = (u64) u1 * (u64) v0
+        addc     r0, r8, r0     # w1 (in r0) = low (t + k)
+        addze    r9, r7         # w2 (in r9) = high (t + k)
+        mullw    r8, r4, r5
+        mulhwu   r7, r4, r5     # t (in r8:r7) = (u64) u0 * (u64) v1
+        addc     r0, r8, r0     # tmp (in r0) = low (t + w1)
+        addze    r0, r7         # k (in r0) = high(t + w1)
+        mullw    r8, r3, r5
+        mulhwu   r7, r3, r5     # t (in r8:r7) = (u64) u1 * (u64) v1
+        addc     r4, r8, r9     # add w2
+        addze    r3, r7
+        addc     r4, r4, r0     # add k
+        addze    r3, r3
+        blr
+        .type __i64_umulh, @function
+        .size __i64_umulh, .-__i64_umulh
diff --git a/runtime/powerpc/i64_umulh.s b/runtime/powerpc/i64_umulh.s
new file mode 100644
index 00000000..1c609466
--- /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 __i64_umulh
+__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 __i64_umulh, @function
+        .size __i64_umulh, .-__i64_umulh
+
diff --git a/runtime/ia32/i64_dtos.S b/runtime/x86_32/i64_dtos.S
index 3cc381bf..3cc381bf 100644
--- a/runtime/ia32/i64_dtos.S
+++ b/runtime/x86_32/i64_dtos.S
diff --git a/runtime/ia32/i64_dtou.S b/runtime/x86_32/i64_dtou.S
index 4903f847..4903f847 100644
--- a/runtime/ia32/i64_dtou.S
+++ b/runtime/x86_32/i64_dtou.S
diff --git a/runtime/ia32/i64_sar.S b/runtime/x86_32/i64_sar.S
index cf2233b1..cf2233b1 100644
--- a/runtime/ia32/i64_sar.S
+++ b/runtime/x86_32/i64_sar.S
diff --git a/runtime/ia32/i64_sdiv.S b/runtime/x86_32/i64_sdiv.S
index f6551c7d..f6551c7d 100644
--- a/runtime/ia32/i64_sdiv.S
+++ b/runtime/x86_32/i64_sdiv.S
diff --git a/runtime/ia32/i64_shl.S b/runtime/x86_32/i64_shl.S
index 1fabebce..1fabebce 100644
--- a/runtime/ia32/i64_shl.S
+++ b/runtime/x86_32/i64_shl.S
diff --git a/runtime/ia32/i64_shr.S b/runtime/x86_32/i64_shr.S
index 34196f09..34196f09 100644
--- a/runtime/ia32/i64_shr.S
+++ b/runtime/x86_32/i64_shr.S
diff --git a/runtime/ia32/i64_smod.S b/runtime/x86_32/i64_smod.S
index 28f47ad4..28f47ad4 100644
--- a/runtime/ia32/i64_smod.S
+++ b/runtime/x86_32/i64_smod.S
diff --git a/runtime/x86_32/i64_smulh.S b/runtime/x86_32/i64_smulh.S
new file mode 100644
index 00000000..cc0f0167
--- /dev/null
+++ b/runtime/x86_32/i64_smulh.S
@@ -0,0 +1,94 @@
+// *****************************************************************
+//
+//               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.  IA32 version.
+	
+#include "sysdeps.h"
+
+// Multiply-high signed
+
+#define XL 12(%esp)
+#define XH 16(%esp)
+#define YL 20(%esp)
+#define YH 24(%esp)
+
+// 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
+
+FUNCTION(__i64_smulh)
+        pushl %esi
+        pushl %edi
+	movl XL, %eax
+        mull YL                 // EDX:EAX = 64-bit product XL.YL
+        movl %edx, %ecx
+        xorl %esi, %esi
+        xorl %edi, %edi         // EDI:ESI:ECX accumulatesbits 127:32 of result
+        movl XH, %eax
+        mull YL                 // EDX:EAX = 64-bit product XH.YL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl YH, %eax
+        mull XL                 // EDX:EAX = 64-bit product YH.XL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl XH, %eax
+        mull YH                 // EDX:EAX = 64-bit product XH.YH
+	addl %eax, %esi
+        adcl %edx, %edi
+// Here, EDI:ESI is the high 64 bits of the unsigned product X.Y
+        xorl %eax, %eax
+        xorl %edx, %edx
+        cmpl $0, XH
+        cmovl YL, %eax
+        cmovl YH, %edx          // EDX:EAX = Y if X < 0, = 0 if X >= 0
+        subl %eax, %esi
+        sbbl %edx, %edi         // EDI:ESI -= Y  if X < 0
+        xorl %eax, %eax
+        xorl %edx, %edx
+        cmpl $0, YH
+        cmovl XL, %eax
+        cmovl XH, %edx          // EDX:EAX = X if Y < 0, = 0 if Y >= 0
+        subl %eax, %esi
+        sbbl %edx, %edi         // EDI:ESI -= X  if Y < 0
+// Now EDI:ESI contains the high 64 bits of the signed product X.Y
+        movl %esi, %eax
+        movl %edi, %edx
+        popl %edi
+        popl %esi
+        ret
+ENDFUNCTION(__i64_smulh)
diff --git a/runtime/ia32/i64_stod.S b/runtime/x86_32/i64_stod.S
index d020e2fc..d020e2fc 100644
--- a/runtime/ia32/i64_stod.S
+++ b/runtime/x86_32/i64_stod.S
diff --git a/runtime/ia32/i64_stof.S b/runtime/x86_32/i64_stof.S
index 25b1d4f7..25b1d4f7 100644
--- a/runtime/ia32/i64_stof.S
+++ b/runtime/x86_32/i64_stof.S
diff --git a/runtime/ia32/i64_udiv.S b/runtime/x86_32/i64_udiv.S
index 75305433..75305433 100644
--- a/runtime/ia32/i64_udiv.S
+++ b/runtime/x86_32/i64_udiv.S
diff --git a/runtime/ia32/i64_udivmod.S b/runtime/x86_32/i64_udivmod.S
index dccfc286..dccfc286 100644
--- a/runtime/ia32/i64_udivmod.S
+++ b/runtime/x86_32/i64_udivmod.S
diff --git a/runtime/ia32/i64_umod.S b/runtime/x86_32/i64_umod.S
index a019df28..a019df28 100644
--- a/runtime/ia32/i64_umod.S
+++ b/runtime/x86_32/i64_umod.S
diff --git a/runtime/x86_32/i64_umulh.S b/runtime/x86_32/i64_umulh.S
new file mode 100644
index 00000000..449a0f8b
--- /dev/null
+++ b/runtime/x86_32/i64_umulh.S
@@ -0,0 +1,74 @@
+// *****************************************************************
+//
+//               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.  IA32 version.
+	
+#include "sysdeps.h"
+
+// Multiply-high unsigned
+
+#define XL 12(%esp)
+#define XH 16(%esp)
+#define YL 20(%esp)
+#define YH 24(%esp)
+
+// X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL
+
+FUNCTION(__i64_umulh)
+        pushl %esi
+        pushl %edi
+	movl XL, %eax
+        mull YL                 // EDX:EAX = 64-bit product XL.YL
+        movl %edx, %ecx
+        xorl %esi, %esi
+        xorl %edi, %edi         // EDI:ESI:ECX accumulate bits 127:32 of result
+        movl XH, %eax
+        mull YL                 // EDX:EAX = 64-bit product XH.YL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl YH, %eax
+        mull XL                 // EDX:EAX = 64-bit product YH.XL
+        addl %eax, %ecx
+        adcl %edx, %esi
+	adcl $0, %edi
+        movl XH, %eax
+        mull YH                 // EDX:EAX = 64-bit product XH.YH
+	addl %esi, %eax
+        adcl %edi, %edx
+	popl %edi
+	popl %esi
+        ret
+ENDFUNCTION(__i64_umulh)
+
diff --git a/runtime/ia32/i64_utod.S b/runtime/x86_32/i64_utod.S
index 428a3b94..428a3b94 100644
--- a/runtime/ia32/i64_utod.S
+++ b/runtime/x86_32/i64_utod.S
diff --git a/runtime/ia32/i64_utof.S b/runtime/x86_32/i64_utof.S
index 0b58f48b..0b58f48b 100644
--- a/runtime/ia32/i64_utof.S
+++ b/runtime/x86_32/i64_utof.S
diff --git a/runtime/ia32/sysdeps.h b/runtime/x86_32/sysdeps.h
index 9d957a88..9d957a88 100644
--- a/runtime/ia32/sysdeps.h
+++ b/runtime/x86_32/sysdeps.h
diff --git a/runtime/ia32/vararg.S b/runtime/x86_32/vararg.S
index 78666c70..78666c70 100644
--- a/runtime/ia32/vararg.S
+++ b/runtime/x86_32/vararg.S
diff --git a/runtime/x86_64/i64_dtou.S b/runtime/x86_64/i64_dtou.S
new file mode 100644
index 00000000..e455ea6f
--- /dev/null
+++ b/runtime/x86_64/i64_dtou.S
@@ -0,0 +1,56 @@
+// *****************************************************************
+//
+//               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.  x86_64 version.
+	
+#include "sysdeps.h"
+
+// Conversion float -> unsigned long
+
+FUNCTION(__i64_dtou)
+        ucomisd .LC1(%rip), %xmm0
+        jnb 1f
+        cvttsd2siq %xmm0, %rax
+        ret
+1:      subsd .LC1(%rip), %xmm0
+        cvttsd2siq %xmm0, %rax
+        addq .LC2(%rip), %rax
+        ret
+
+        .p2align 3
+.LC1:   .quad 0x43e0000000000000       // 2^63 in double precision
+.LC2:   .quad 0x8000000000000000       // 2^63 as an integer
+
+ENDFUNCTION(__i64_dtou)
+        
diff --git a/runtime/x86_64/i64_utod.S b/runtime/x86_64/i64_utod.S
new file mode 100644
index 00000000..96b77a64
--- /dev/null
+++ b/runtime/x86_64/i64_utod.S
@@ -0,0 +1,56 @@
+// *****************************************************************
+//
+//               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.  x86_64 version.
+	
+#include "sysdeps.h"
+
+// Conversion unsigned long -> double-precision float
+
+FUNCTION(__i64_utod)
+        testq   %rdi, %rdi
+        js      1f
+        pxor    %xmm0, %xmm0            // if < 2^63,
+        cvtsi2sdq %rdi, %xmm0           // convert as if signed
+        ret
+1:                                      // if >= 2^63, use round-to-odd trick
+        movq    %rdi, %rax
+        shrq    %rax
+        andq    $1, %rdi
+        orq     %rdi, %rax              // (arg >> 1) | (arg & 1)
+        pxor    %xmm0, %xmm0
+        cvtsi2sdq %rax, %xmm0           // convert as if signed
+        addsd   %xmm0, %xmm0            // multiply result by 2.0
+        ret
+ENDFUNCTION(__i64_utod)       
diff --git a/runtime/x86_64/i64_utof.S b/runtime/x86_64/i64_utof.S
new file mode 100644
index 00000000..d0935341
--- /dev/null
+++ b/runtime/x86_64/i64_utof.S
@@ -0,0 +1,56 @@
+// *****************************************************************
+//
+//               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.  x86_64 version.
+	
+#include "sysdeps.h"
+
+// Conversion unsigned long -> single-precision float
+
+FUNCTION(__i64_utof)
+        testq   %rdi, %rdi
+        js      1f
+        pxor    %xmm0, %xmm0            // if < 2^63,
+        cvtsi2ssq %rdi, %xmm0           // convert as if signed
+        ret
+1:                                      // if >= 2^63, use round-to-odd trick
+        movq    %rdi, %rax
+        shrq    %rax
+        andq    $1, %rdi
+        orq     %rdi, %rax              // (arg >> 1) | (arg & 1)
+        pxor    %xmm0, %xmm0
+        cvtsi2ssq %rax, %xmm0           // convert as if signed
+        addss   %xmm0, %xmm0            // multiply result by 2.0
+        ret
+ENDFUNCTION(__i64_utof)       
diff --git a/runtime/x86_64/sysdeps.h b/runtime/x86_64/sysdeps.h
new file mode 100644
index 00000000..e9d456af
--- /dev/null
+++ b/runtime/x86_64/sysdeps.h
@@ -0,0 +1,75 @@
+// *****************************************************************
+//
+//               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.
+//
+// *********************************************************************
+
+// System dependencies
+
+#if defined(SYS_linux) || defined(SYS_bsd)
+
+#define GLOB(x) x
+#define FUNCTION(f) \
+	.text; \
+	.globl f; \
+	.align 16; \
+f:
+
+#define ENDFUNCTION(f) \
+	.type f, @function; .size f, . - f
+
+#endif
+
+#if defined(SYS_macosx)
+
+#define GLOB(x) _##x
+#define FUNCTION(f) \
+	.text; \
+	.globl _##f; \
+	.align 4; \
+_##f:
+
+#define ENDFUNCTION(f)
+
+#endif
+
+#if defined(SYS_cygwin)
+
+#define GLOB(x) _##x
+#define FUNCTION(f) \
+	.text; \
+	.globl _##f; \
+	.align 16; \
+_##f:
+
+#define ENDFUNCTION(f)
+
+#endif
diff --git a/runtime/x86_64/vararg.S b/runtime/x86_64/vararg.S
new file mode 100644
index 00000000..9c0d787b
--- /dev/null
+++ b/runtime/x86_64/vararg.S
@@ -0,0 +1,148 @@
+// *****************************************************************
+//
+//               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 variadic functions <stdarg.h>.  x86_64 version.
+	
+// typedef struct {
+//    unsigned int gp_offset;
+//    unsigned int fp_offset;
+//    void *overflow_arg_area;
+//    void *reg_save_area;
+// } va_list[1];
+
+// The va_start macro initializes the structure as follows:
+// - reg_save_area: The element points to the start of the register save area.
+// - overflow_arg_area: This pointer is used to fetch arguments passed on
+//   the stack. It is initialized with the address of the first argument
+//   passed on the stack, if any, and then always updated to point to the
+//   start of the next argument on the stack.
+// - gp_offset: The element holds the offset in bytes from reg_save_area
+//   to the place where the next available general purpose argument
+//   register is saved. In case all argument registers have been
+//   exhausted, it is set to the value 48 (6 * 8).
+// - fp_offset: The element holds the offset in bytes from reg_save_area
+//   to the place where the next available floating point argument
+//   register is saved. In case all argument registers have been
+//   exhausted, it is set to the value 176 (6 * 8 + 8 * 16).
+
+// unsigned int __compcert_va_int32(va_list ap);
+// unsigned long long __compcert_va_int64(va_list ap);
+// double __compcert_va_float64(va_list ap);
+
+#include "sysdeps.h"
+
+FUNCTION(__compcert_va_int32)
+        movl    0(%rdi), %edx           // edx = gp_offset
+        cmpl    $48, %edx
+        jae     1f
+  // next argument is in gp reg area
+        movq    16(%rdi), %rsi          // rsi = reg_save_area
+        movl    0(%rsi, %rdx, 1), %eax  // next integer argument
+        addl    $8, %edx
+        movl    %edx, 0(%rdi)           // increment gp_offset by 8
+        ret
+  // next argument is in overflow arg area
+1:      movq    8(%rdi), %rsi           // rsi = overflow_arg_area
+        movq    0(%rsi), %rax           // next integer argument
+        addq    $8, %rsi
+        movq    %rsi, 8(%rdi)           // increment overflow_arg_area by 8
+        ret
+ENDFUNCTION(__compcert_va_int32)
+
+FUNCTION(__compcert_va_int64)
+        movl    0(%rdi), %edx           // edx = gp_offset
+        cmpl    $48, %edx
+        jae     1f
+  // next argument is in gp reg area
+        movq    16(%rdi), %rsi          // rsi = reg_save_area
+        movq    0(%rsi, %rdx, 1), %rax  // next integer argument
+        addl    $8, %edx
+        movl    %edx, 0(%rdi)            // increment gp_offset by 8
+        ret
+  // next argument is in overflow arg area
+1:      movq    8(%rdi), %rsi           // rsi = overflow_arg_area
+        movq    0(%rsi), %rax           // next integer argument
+        addq    $8, %rsi
+        movq    %rsi, 8(%rdi)           // increment overflow_arg_area by 8
+        ret
+ENDFUNCTION(__compcert_va_int64)
+
+FUNCTION(__compcert_va_float64)
+        movl    4(%rdi), %edx           // edx = fp_offset
+        cmpl    $176, %edx
+        jae     1f
+  // next argument is in fp reg area
+        movq    16(%rdi), %rsi          // rsi = reg_save_area
+        movsd   0(%rsi, %rdx, 1), %xmm0 // next floating-point argument
+        addl    $16, %edx
+        movl    %edx, 4(%rdi)           // increment fp_offset by 16
+        ret
+  // next argument is in overflow arg area
+1:      movq    8(%rdi), %rsi           // rsi = overflow_arg_area
+        movsd   0(%rsi), %xmm0          // next floating-point argument
+        addq    $8, %rsi
+        movq    %rsi, 8(%rdi)           // increment overflow_arg_area by 8
+        ret
+ENDFUNCTION(__compcert_va_float64)
+
+FUNCTION(__compcert_va_composite)
+        jmp     GLOB(__compcert_va_int64)     // by-ref convention, FIXME
+ENDFUNCTION(__compcert_va_composite)	
+	
+// Save integer and FP registers at beginning of vararg function
+// r10 points to register save area
+// al contains number of FP arguments passed in registers
+// The register save area has the following shape:
+//   0, 8, ..., 40   -> 6 x 8-byte slots for saving rdi, rsi, rdx, rcx, r8, r9
+//   48, 64, ... 160 -> 8 x 16-byte slots for saving xmm0...xmm7
+
+FUNCTION(__compcert_va_saveregs)
+        movq %rdi, 0(%r10)
+        movq %rsi, 8(%r10)
+        movq %rdx, 16(%r10)
+        movq %rcx, 24(%r10)
+        movq %r8, 32(%r10)
+        movq %r9, 40(%r10)
+        testb %al, %al
+        je 1f
+        movaps %xmm0, 48(%r10)
+        movaps %xmm1, 64(%r10)
+        movaps %xmm2, 80(%r10)
+        movaps %xmm3, 96(%r10)
+        movaps %xmm4, 112(%r10)
+        movaps %xmm5, 128(%r10)
+        movaps %xmm6, 144(%r10)
+        movaps %xmm7, 160(%r10)
+1:      ret
+ENDFUNCTION(__compcert_va_saveregs)