Remove int64 emulation in bytecode interpreter.

We now assume an int64 type is provided by the C compiler.

The emulation file was already not compiling, so it is probably not used even
on exotic architectures. These files come from OCaml, where they are no longer
used either.

4 files changed, 13 insertions, 338 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index dc571699e..bf383a33a 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -22,18 +22,10 @@
 #include "coq_memory.h" 
 #include "coq_values.h" 
 
-/*spiwack : imports support functions for 64-bit integers */
-#include <caml/config.h>
-#ifdef ARCH_INT64_TYPE
-#include "int64_native.h"
-#else
-#include "int64_emul.h"
-#endif
-
 /* spiwack: I append here a few macros for value/number manipulation */
 #define uint32_of_value(val) (((uint32_t)val >> 1))
 #define value_of_uint32(i)   ((value)(((uint32_t)(i) << 1) | 1))
-#define UI64_of_uint32(lo)  ((uint64_t)(I64_literal(0,(uint32_t)(lo))))
+#define UI64_of_uint32(lo) ((uint64_t)(lo))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
 /* /spiwack */
 
@@ -1201,8 +1193,8 @@ value coq_interprete
         print_instr("MULCINT31");
 	uint64_t p;
         /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
-        p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
-	if ( I64_is_zero(p) ) {
+        p = UI64_of_value (accu) * UI64_of_uint32 ((*sp++)^1);
+	if (p == 0) {
 	  accu = (value)1;
 	}
 	else {
@@ -1211,8 +1203,8 @@ value coq_interprete
 	     of the non-constant constructor is then 1 */
 	  Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
 	  /*unsigned shift*/
-	  Field(accu, 0) = (value)(I64_lsr(p,31)|1) ;  /*higher part*/
-	  Field(accu, 1) = (value)(I64_to_int32(p)|1); /*lower part*/
+	  Field(accu, 0) = (value)((p >> 31)|1) ;  /*higher part*/
+	  Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/
 	}
 	Next;
       }
@@ -1224,19 +1216,20 @@ value coq_interprete
                     int62 by the int31 */
         uint64_t bigint;
         bigint = UI64_of_value(accu);
-        bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
+        bigint = (bigint << 31) | UI64_of_value(*sp++);
         uint64_t divisor;
         divisor = UI64_of_value(*sp++);
         Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-        if (I64_is_zero (divisor)) {
+        if (divisor == 0) {
           Field(accu, 0) = 1; /* 2*0+1 */
           Field(accu, 1) = 1; /* 2*0+1 */
 	}
 	else {
 	  uint64_t quo, mod;
-          I64_udivmod(bigint, divisor, &quo, &mod);
-          Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
-	  Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
+	  quo = bigint / divisor;
+	  mod = bigint % divisor;
+          Field(accu, 0) = value_of_uint32((uint32_t)(quo));
+	  Field(accu, 1) = value_of_uint32((uint32_t)(mod));
 	}
 	Next;
       }
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
deleted file mode 100644
index 86bee72ed..000000000
--- a/kernel/byterun/int64_emul.h
+++ /dev/null
@@ -1,270 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Objective Caml                            */
-/*                                                                     */
-/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
-/*                                                                     */
-/*  Copyright 2002 Institut National de Recherche en Informatique et   */
-/*  en Automatique.  All rights reserved.  This file is distributed    */
-/*  under the terms of the GNU Library General Public License, with    */
-/*  the special exception on linking described in file ../LICENSE.     */
-/*                                                                     */
-/***********************************************************************/
-
-/* Software emulation of 64-bit integer arithmetic, for C compilers
-   that do not support it.  */
-
-#ifndef CAML_INT64_EMUL_H
-#define CAML_INT64_EMUL_H
-
-#include <math.h>
-
-#ifdef ARCH_BIG_ENDIAN
-#define I64_literal(hi,lo) { hi, lo }
-#else
-#define I64_literal(hi,lo) { lo, hi }
-#endif
-
-/* Unsigned comparison */
-static int I64_ucompare(uint64 x, uint64 y)
-{
-  if (x.h > y.h) return 1;
-  if (x.h < y.h) return -1;
-  if (x.l > y.l) return 1;
-  if (x.l < y.l) return -1;
-  return 0;
-}
-
-#define I64_ult(x, y) (I64_ucompare(x, y) < 0)
-
-/* Signed comparison */
-static int I64_compare(int64 x, int64 y)
-{
-  if ((int32)x.h > (int32)y.h) return 1;
-  if ((int32)x.h < (int32)y.h) return -1;
-  if (x.l > y.l) return 1;
-  if (x.l < y.l) return -1;
-  return 0;
-}
-
-/* Negation */
-static int64 I64_neg(int64 x)
-{
-  int64 res;
-  res.l = -x.l;
-  res.h = ~x.h;
-  if (res.l == 0) res.h++;
-  return res;
-}
-
-/* Addition */
-static int64 I64_add(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l + y.l;
-  res.h = x.h + y.h;
-  if (res.l < x.l) res.h++;
-  return res;
-}
-
-/* Subtraction */
-static int64 I64_sub(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l - y.l;
-  res.h = x.h - y.h;
-  if (x.l < y.l) res.h--;
-  return res;
-}
-
-/* Multiplication */
-static int64 I64_mul(int64 x, int64 y)
-{
-  int64 res;
-  uint32 prod00 = (x.l & 0xFFFF) * (y.l & 0xFFFF);
-  uint32 prod10 = (x.l >> 16) * (y.l & 0xFFFF);
-  uint32 prod01 = (x.l & 0xFFFF) * (y.l >> 16);
-  uint32 prod11 = (x.l >> 16) * (y.l >> 16);
-  res.l = prod00;
-  res.h = prod11 + (prod01 >> 16) + (prod10 >> 16);
-  prod01 = prod01 << 16; res.l += prod01; if (res.l < prod01) res.h++;
-  prod10 = prod10 << 16; res.l += prod10; if (res.l < prod10) res.h++;
-  res.h += x.l * y.h + x.h * y.l;
-  return res;
-}
-
-#define I64_is_zero(x) (((x).l | (x).h) == 0)
-
-#define I64_is_negative(x) ((int32) (x).h < 0)
-
-/* Bitwise operations */
-static int64 I64_and(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l & y.l;
-  res.h = x.h & y.h;
-  return res;
-}
-
-static int64 I64_or(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l | y.l;
-  res.h = x.h | y.h;
-  return res;
-}
-
-static int64 I64_xor(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l ^ y.l;
-  res.h = x.h ^ y.h;
-  return res;
-}
-
-/* Shifts */
-static int64 I64_lsl(int64 x, int s)
-{
-  int64 res;
-  s = s & 63;
-  if (s == 0) return x;
-  if (s < 32) {
-    res.l = x.l << s;
-    res.h = (x.h << s) | (x.l >> (32 - s));
-  } else {
-    res.l = 0;
-    res.h = x.l << (s - 32);
-  }
-  return res;
-}
-
-static int64 I64_lsr(int64 x, int s)
-{
-  int64 res;
-  s = s & 63;
-  if (s == 0) return x;
-  if (s < 32) {
-    res.l = (x.l >> s) | (x.h << (32 - s));
-    res.h = x.h >> s;
-  } else {
-    res.l = x.h >> (s - 32);
-    res.h = 0;
-  }
-  return res;
-}
-
-static int64 I64_asr(int64 x, int s)
-{
-  int64 res;
-  s = s & 63;
-  if (s == 0) return x;
-  if (s < 32) {
-    res.l = (x.l >> s) | (x.h << (32 - s));
-    res.h = (int32) x.h >> s;
-  } else {
-    res.l = (int32) x.h >> (s - 32);
-    res.h = (int32) x.h >> 31;
-  }
-  return res;
-}
-
-/* Division and modulus */
-
-#define I64_SHL1(x) x.h = (x.h << 1) | (x.l >> 31); x.l <<= 1
-#define I64_SHR1(x) x.l = (x.l >> 1) | (x.h << 31); x.h >>= 1
-
-static void I64_udivmod(uint64 modulus, uint64 divisor,
-                        uint64 * quo, uint64 * mod)
-{
-  int64 quotient, mask;
-  int cmp;
-
-  quotient.h = 0; quotient.l = 0;
-  mask.h = 0; mask.l = 1;
-  while ((int32) divisor.h >= 0) {
-    cmp = I64_ucompare(divisor, modulus);
-    I64_SHL1(divisor);
-    I64_SHL1(mask);
-    if (cmp >= 0) break;
-  }
-  while (mask.l | mask.h) {
-    if (I64_ucompare(modulus, divisor) >= 0) {
-      quotient.h |= mask.h; quotient.l |= mask.l;
-      modulus = I64_sub(modulus, divisor);
-    }
-    I64_SHR1(mask);
-    I64_SHR1(divisor);
-  }
-  *quo = quotient;
-  *mod = modulus;
-}
-
-static int64 I64_div(int64 x, int64 y)
-{
-  int64 q, r;
-  int32 sign;
-
-  sign = x.h ^ y.h;
-  if ((int32) x.h < 0) x = I64_neg(x);
-  if ((int32) y.h < 0) y = I64_neg(y);
-  I64_udivmod(x, y, &q, &r);
-  if (sign < 0) q = I64_neg(q);
-  return q;
-}
-
-static int64 I64_mod(int64 x, int64 y)
-{
-  int64 q, r;
-  int32 sign;
-
-  sign = x.h;
-  if ((int32) x.h < 0) x = I64_neg(x);
-  if ((int32) y.h < 0) y = I64_neg(y);
-  I64_udivmod(x, y, &q, &r);
-  if (sign < 0) r = I64_neg(r);
-  return r;
-}
-
-/* Coercions */
-
-static int64 I64_of_int32(int32 x)
-{
-  int64 res;
-  res.l = x;
-  res.h = x >> 31;
-  return res;
-}
-
-#define I64_to_int32(x) ((int32) (x).l)
-
-/* Note: we assume sizeof(intnat) = 4 here, which is true otherwise
-   autoconfiguration would have selected native 64-bit integers */
-#define I64_of_intnat I64_of_int32
-#define I64_to_intnat I64_to_int32
-
-static double I64_to_double(int64 x)
-{
-  double res;
-  int32 sign = x.h;
-  if (sign < 0) x = I64_neg(x);
-  res = ldexp((double) x.h, 32) + x.l;
-  if (sign < 0) res = -res;
-  return res;
-}
-
-static int64 I64_of_double(double f)
-{
-  int64 res;
-  double frac, integ;
-  int neg;
-
-  neg = (f < 0);
-  f = fabs(f);
-  frac = modf(ldexp(f, -32), &integ);
-  res.h = (uint32) integ;
-  res.l = (uint32) ldexp(frac, 32);
-  if (neg) res = I64_neg(res);
-  return res;
-}
-
-#endif /* CAML_INT64_EMUL_H */
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
deleted file mode 100644
index 657d0a07e..000000000
--- a/kernel/byterun/int64_native.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Objective Caml                            */
-/*                                                                     */
-/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
-/*                                                                     */
-/*  Copyright 2002 Institut National de Recherche en Informatique et   */
-/*  en Automatique.  All rights reserved.  This file is distributed    */
-/*  under the terms of the GNU Library General Public License, with    */
-/*  the special exception on linking described in file ../LICENSE.     */
-/*                                                                     */
-/***********************************************************************/
-
-/* Wrapper macros around native 64-bit integer arithmetic,
-   so that it has the same interface as the software emulation
-   provided in int64_emul.h */
-
-#ifndef CAML_INT64_NATIVE_H
-#define CAML_INT64_NATIVE_H
-
-#define I64_literal(hi,lo) ((int64_t)(hi) << 32 | (lo))
-#define I64_compare(x,y) (((x) > (y)) - ((x) < (y)))
-#define I64_ult(x,y) ((uint64_t)(x) < (uint64_t)(y))
-#define I64_neg(x) (-(x))
-#define I64_add(x,y) ((x) + (y))
-#define I64_sub(x,y) ((x) - (y))
-#define I64_mul(x,y) ((x) * (y))
-#define I64_is_zero(x) ((x) == 0)
-#define I64_is_negative(x) ((x) < 0)
-#define I64_div(x,y) ((x) / (y))
-#define I64_mod(x,y) ((x) % (y))
-#define I64_udivmod(x,y,quo,rem) \
-  (*(rem) = (uint64_t)(x) % (uint64_t)(y), \
-   *(quo) = (uint64_t)(x) / (uint64_t)(y))
-#define I64_and(x,y) ((x) & (y))
-#define I64_or(x,y) ((x) | (y))
-#define I64_xor(x,y) ((x) ^ (y))
-#define I64_lsl(x,y) ((x) << (y))
-#define I64_asr(x,y) ((x) >> (y))
-#define I64_lsr(x,y) ((uint64_t)(x) >> (y))
-#define I64_to_intnat(x) ((intnat) (x))
-#define I64_of_intnat(x) ((intnat) (x))
-#define I64_to_int32(x) ((int32_t) (x))
-#define I64_of_int32(x) ((int64_t) (x))
-#define I64_to_double(x) ((double)(x))
-#define I64_of_double(x) ((int64_t)(x))
-
-#endif /* CAML_INT64_NATIVE_H */
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index ad1f8cbcc..90df4f00c 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -115,8 +115,8 @@ let core_mllib = List.map (fun s -> s^".mllib") core_libs
 let tolink = "tools/tolink.ml"
 
 let c_headers_base =
-  ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h";
-   "coq_gc.h"; "coq_interp.h"; "coq_values.h"; "int64_native.h";
+  ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h";
+   "coq_gc.h"; "coq_interp.h"; "coq_values.h";
    "coq_jumptbl.h"]
 let c_headers = List.map ((^) "kernel/byterun/") c_headers_base