Remove the C primitives for unsigned long long arithmetic, replaced

by pure OCaml code.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2153 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 25 insertions, 44 deletions

diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index d38054a..504f7e0 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -21,12 +21,31 @@ open Machine
 
 (* Extra arith on int64 *)
 
-external int64_unsigned_div: int64 -> int64 -> int64
-  = "cparser_int64_unsigned_div"
-external int64_unsigned_mod: int64 -> int64 -> int64
-  = "cparser_int64_unsigned_mod"
-external int64_unsigned_compare: int64 -> int64 -> int
-  = "cparser_int64_unsigned_compare"
+(* Unsigned comparison: do signed comparison after shifting range *)
+
+let int64_unsigned_compare x y =
+  Int64.compare (Int64.add x Int64.min_int) (Int64.add y Int64.min_int)
+
+(* Unsigned division and modulus: synthesized from signed division
+   as described in "Hacker's Delight", section 9.3. *)
+
+let int64_unsigned_div n d =
+  if d < 0L then
+    if int64_unsigned_compare n d < 0 then 0L else 1L
+  else begin
+    let q = Int64.shift_left (Int64.div (Int64.shift_right_logical n 1) d) 1 in
+    let r = Int64.sub n (Int64.mul q d) in
+    if int64_unsigned_compare r d >= 0 then Int64.succ q else q
+  end
+
+let int64_unsigned_mod n d =
+  if d < 0L then
+    if int64_unsigned_compare n d < 0 then n else Int64.sub n d
+  else begin
+    let q = Int64.shift_left (Int64.div (Int64.shift_right_logical n 1) d) 1 in
+    let r = Int64.sub n (Int64.mul q d) in
+    if int64_unsigned_compare r d >= 0 then Int64.sub r d else r
+  end
 
 exception Notconst
 
diff --git a/cparser/libCparser.clib b/cparser/libCparser.clib
deleted file mode 100644
index 1b55150..0000000
--- a/cparser/libCparser.clib
+++ /dev/null
@@ -1 +0,0 @@
-cparser/uint64.o
diff --git a/cparser/uint64.c b/cparser/uint64.c
deleted file mode 100644
index 1528887..0000000
--- a/cparser/uint64.c
+++ /dev/null
@@ -1,37 +0,0 @@
-/* *********************************************************************/
-/*                                                                     */
-/*              The Compcert verified compiler                         */
-/*                                                                     */
-/*          Xavier Leroy, INRIA Paris-Rocquencourt                     */
-/*                                                                     */
-/*  Copyright Institut National de Recherche en Informatique et en     */
-/*  Automatique.  All rights reserved.  This file is distributed       */
-/*  under the terms of the GNU General Public License as published by  */
-/*  the Free Software Foundation, either version 2 of the License, or  */
-/*  (at your option) any later version.  This file is also distributed */
-/*  under the terms of the INRIA Non-Commercial License Agreement.     */
-/*                                                                     */
-/* *********************************************************************/
-
-#include <caml/mlvalues.h>
-#include <caml/alloc.h>
-
-value cparser_int64_unsigned_div(value v1, value v2)
-{
-  return caml_copy_int64((uint64) Int64_val(v1) / (uint64) Int64_val(v2));
-}
-
-value cparser_int64_unsigned_mod(value v1, value v2)
-{
-  return caml_copy_int64((uint64) Int64_val(v1) % (uint64) Int64_val(v2));
-}
-
-value cparser_int64_unsigned_compare(value v1, value v2)
-{
-  uint64 n1 = (uint64) Int64_val(v1);
-  uint64 n2 = (uint64) Int64_val(v2);
-  if (n1 < n2) return Val_int(-1);
-  if (n1 > n2) return Val_int(1);
-  return Val_int(0);
-}
-