diff options
| -rw-r--r-- | cparser/Ceval.ml | 31 | ||||
| -rw-r--r-- | cparser/libCparser.clib | 1 | ||||
| -rw-r--r-- | cparser/uint64.c | 37 | ||||
| -rw-r--r-- | myocamlbuild.ml | 9 |
4 files changed, 25 insertions, 53 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); -} - 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"]; |