From debae4b0c69060a637489c6d0afe93125c9d9268 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 18 Mar 2013 09:22:27 +0000
Subject: 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
---
 cparser/Ceval.ml        | 31 +++++++++++++++++++++++++------
 cparser/libCparser.clib |  1 -
 cparser/uint64.c        | 37 -------------------------------------
 myocamlbuild.ml         |  9 ---------
 4 files changed, 25 insertions(+), 53 deletions(-)
 delete mode 100644 cparser/libCparser.clib
 delete mode 100644 cparser/uint64.c

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);
-}
-
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 08b9b13..22709d7 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -4,15 +4,6 @@ dispatch begin function
     (* declare the tags "use_Cparser" and "include_Cparser" *)
     ocaml_lib "cparser/Cparser";
 
-    (* force linking of libCparser.a when use_Cparser is set *)
-    flag ["link"; "ocaml"; "native"; "use_Cparser"]
-         (S[A"cparser/libCparser.a"]);
-    flag ["link"; "ocaml"; "byte"; "use_Cparser"]
-         (S[A"-custom"; A"cparser/libCparser.a"]);
-
-    (* make sure libCparser.a is up to date *)
-    dep  ["link"; "ocaml"; "use_Cparser"] ["cparser/libCparser.a"];
-
     (* libraries and syntax extensions accessed via ocamlfind *)
     flag ["ocaml"; "link"; "pkg_unix"] & S[A"-package"; A "unix"];
     flag ["ocaml"; "link"; "pkg_str"] & S[A"-package"; A "str"];
-- 
cgit v1.2.3