Turn 64-bit integer division and modulus by constants into multiply-high

This trick was already implemented for 32-bit integer division and modulus.  Here we extend it to the 64-bit case.

For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned).  Tentative implementations are provided for IA32 and PowerPC, but need testing.

8 files changed, 433 insertions, 0 deletions

diff --git a/runtime/Makefile b/runtime/Makefile
index 59d2bb64..b94db3ca 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -14,6 +14,7 @@ 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
 
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/ia32/i64_smulh.S b/runtime/ia32/i64_smulh.S
new file mode 100644
index 00000000..cc0f0167
--- /dev/null
+++ b/runtime/ia32/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_umulh.S b/runtime/ia32/i64_umulh.S
new file mode 100644
index 00000000..449a0f8b
--- /dev/null
+++ b/runtime/ia32/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/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_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