Replace Num with ZArith for Cilint (for OCaml 4.06.0).

Makefile.in

@@ -106,7 +106,7 @@ ocamlbuild:
 META:
 	@rm -f $@
 	@printf "description = \"C Intermediate Language\"\n" >>$@
-	@printf "requires = \"unix str num dynlink\"\n" >>$@
+	@printf "requires = \"unix str zarith dynlink\"\n" >>$@
 	@printf "version = \"$(CIL_VERSION)\"\n\n" >>$@
 	@printf "archive(byte) = \"cil.cma\"\n" >>$@
 	@printf "archive(native) = \"cil.cmxa\"\n\n" >>$@

README.md

@@ -31,8 +31,8 @@ check out the accompanying [project template][template].
 Installation
 -----------
 
-To build and install CIL, you need the OCaml compiler, perl, and
-[ocamlfind][findlib].  (Of course, you also need some C compiler,
+To build and install CIL, you need the OCaml compiler, perl, the [zarith]
+module and [ocamlfind][findlib].  (Of course, you also need some C compiler,
 preferably gcc.)
 
 Run the following commands to build and install CIL:
@@ -50,6 +50,7 @@ directory:
 
 [findlib]: http://projects.camlcity.org/projects/findlib.html
 [opam]: http://opam.ocamlpro.com/
+[zarith]: https://github.com/ocaml/Zarith
 
 Usage
 -----

myocamlbuild.ml

@@ -17,12 +17,21 @@ let find_modules builder mllib =
   (String.concat " " built_files) ^ " "
 ;;
 
+let ocamlfind_query pkg =
+  let cmd = Printf.sprintf "ocamlfind query %s" (Filename.quote pkg) in
+  Ocamlbuild_pack.My_unix.run_and_open cmd (fun ic ->
+      input_line ic
+    )
+
 let cil_version =
   try Printf.sprintf "(version %s)" (Sys.getenv "CIL_VERSION")
   with Not_found -> "" ;;
 
 dispatch begin function
 | After_rules ->
+    (* zarith exists *)
+  ocaml_lib ~extern:true ~dir:(ocamlfind_query "zarith") "zarith";
+
     (* the main CIL library *)
     ocaml_lib "src/cil";
 

src/_tags

@@ -1,4 +1,5 @@
 <ext> or <ext/*> or <frontc> or <ocamlutil>: include
 
 <feature.ml>: package(findlib)
-<main.{byte,native}>: use_unix, use_str, use_nums, use_dynlink, use_cil, linkall, package(findlib)
+<main.{byte,native}>: use_unix, use_str, use_dynlink, use_cil, use_zarith, linkall, package(findlib)
+<cilint.*>: use_zarith

src/cil.ml

@@ -2713,7 +2713,7 @@ let parseInt (str: string) : exp =
     let l = String.length str in
     fun s -> 
       let ls = String.length s in
-      l >= ls && s = String.uppercase (String.sub str (l - ls) ls)
+      l >= ls && s = String.uppercase_ascii (String.sub str (l - ls) ls)
   in
   let l = String.length str in
   (* See if it is octal or hex *)
@@ -5080,19 +5080,19 @@ let loadBinaryFile (filename : string) : file =
 (* Take the name of a file and make a valid symbol name out of it. There are 
  * a few characters that are not valid in symbols *)
 let makeValidSymbolName (s: string) = 
-  let s = String.copy s in (* So that we can update in place *)
-  let l = String.length s in
+  let s = Bytes.of_string s in (* strings are immutable; convert to mutable Bytes *)
+  let l = Bytes.length s in
   for i = 0 to l - 1 do
-    let c = String.get s i in
+    let c = Bytes.get s i in
     let isinvalid = 
       match c with
         '-' | '.' -> true
       | _ -> false
     in
     if isinvalid then 
-      String.set s i '_';
+      Bytes.set s i '_';
   done;
-  s
+  Bytes.to_string s
 
 let rec addOffset (toadd: offset) (off: offset) : offset =
   match off with

src/cilint.ml

@@ -21,68 +21,72 @@
    bitwise operations on big_ints, and bug-fixed versions of int64_of_big_int
    and big_int_of_int64. *)
 
-open Big_int
-
-type cilint = Small of int | Big of big_int
+type cilint = Small of int | Big of Z.t
 type truncation = NoTruncation | ValueTruncation | BitTruncation
 
-let zero_cilint = Small 0
-let one_cilint = Small 1
+let zero_cilint : cilint = Small 0
+let one_cilint : cilint = Small 1
 
 (* Precompute useful big_ints *)
-let b30 = power_int_positive_int 2 30
-let m1 = minus_big_int unit_big_int
+let b30 = Z.pow (Z.of_int 2) 30
+let m1 = Z.minus_one
+let two = Z.of_int 2
 
 (* True if 'b' is all 0's or all 1's *)
-let nobits (b:big_int) : bool = 
-  sign_big_int b = 0 || compare_big_int b m1 = 0
+let nobits (b:Z.t) : bool = 
+  Z.sign b = 0 || Z.equal b m1
 
-let big_int_of_cilint (c:cilint) : big_int = 
+let big_int_of_cilint (c:cilint) : Z.t = 
   match c with
-  | Small i -> big_int_of_int i
+  | Small i -> Z.of_int i
   | Big b -> b
 
-let cilint_of_big_int (b:big_int) : cilint = 
-  if is_int_big_int b then
-    Small (int_of_big_int b)
+
+let cilint_of_big_int (b:Z.t) : cilint =
+  if Z.fits_int b then
+    Small (Z.to_int b)
   else
-    Big b
+    Big b 
 
-let neg_cilint c = 
+
+let neg_cilint (c : cilint) : cilint = 
   match c with
-  | Small i when i <> min_int -> Small (-i)
-  | _ -> Big (minus_big_int (big_int_of_cilint c))
+  | Small((i: int)) 
+     when i <> Pervasives.min_int -> 
+      Small(-i)
+  | _ -> Big (Z.neg (big_int_of_cilint c))
 
 (* Apply big_int 'op' to two cilints, returning a cilint *)
 let b op c1 c2 = cilint_of_big_int (op (big_int_of_cilint c1) (big_int_of_cilint c2))
 
-let add_cilint = b add_big_int
-let sub_cilint = b sub_big_int
-let mul_cilint = b mult_big_int
-let div_cilint = b div_big_int
-let mod_cilint = b mod_big_int
+let add_cilint = b Z.add
+let sub_cilint = b Z.sub
+let mul_cilint = b Z.mul
+let div_cilint = b Z.div
+let mod_cilint = b Z.rem 
+
 
 let compare_cilint (c1:cilint) (c2:cilint) : int = 
   match c1, c2 with
-  | Small i1, Small i2 -> compare i1 i2
-  | _ -> compare_big_int (big_int_of_cilint c1) (big_int_of_cilint c2)
+  | Small i1, Small i2 -> Pervasives.compare i1 i2
+  | _ -> Z.compare (big_int_of_cilint c1) (big_int_of_cilint c2)
 
 let is_zero_cilint (c:cilint) : bool = 
   match c with
   | Small i -> i = 0
-  | Big b -> sign_big_int b = 0
+  | Big b -> Z.sign b = 0
 
 let negative_cilint (c:cilint) : bool = 
   match c with 
   | Small i -> i < 0
-  | Big b -> sign_big_int b < 0
+  | Big b -> Z.sign b < 0
 
 let cilint_of_int (i:int) : cilint = Small i
 
 let int_of_cilint (c:cilint) : int = 
   match c with 
   | Small i -> i
-  | Big b -> int_of_big_int b
+  | Big b -> Z.to_int b
 
 let rec cilint_of_int64 (i64:int64) : cilint = 
   if Int64.compare i64 (Int64.of_int min_int) >= 0 && 
@@ -92,12 +96,12 @@ let rec cilint_of_int64 (i64:int64) : cilint =
     (* We convert 30 bits at a time *)
     let rec loop i mul acc = 
       if i = 0L then acc
-      else if i = -1L then sub_big_int acc mul
+      else if i = -1L then Z.sub acc mul
       else 
 	let lo30 = Int64.to_int (Int64.logand i 0x3fffffffL) in
-	loop (Int64.shift_right i 30) (mult_big_int mul b30)
-	  (add_big_int acc (mult_big_int mul (big_int_of_int lo30)))
-    in Big (loop i64 unit_big_int zero_big_int)
+	loop (Int64.shift_right i 30) (Z.mul mul b30)
+	  (Z.add acc (Z.mul mul (Z.of_int lo30)))
+    in Big (loop i64 Z.one Z.zero)
 
 (* Note that this never fails, instead it returns the low-order 64-bits
    of the cilint. *)
@@ -106,23 +110,23 @@ let rec int64_of_cilint (c:cilint) : int64 =
   | Small i -> Int64.of_int i
   | Big b -> 
       let rec loop b mul acc = 
-	if sign_big_int b = 0 then 
+	if Z.sign b = 0 then 
 	  acc
-	else if compare_big_int b m1 == 0 then
+	else if Z.compare b m1 == 0 then
 	  Int64.sub acc mul
 	else
-	  let hi, lo = quomod_big_int b b30 in
+	  let hi, lo = Z.ediv_rem b b30 in
 	  loop hi (Int64.mul mul 0x40000000L)
-	    (Int64.add acc (Int64.mul mul (Int64.of_int (int_of_big_int lo))))
+	    (Int64.add acc (Int64.mul mul (Int64.of_int (Z.to_int lo))))
       in loop b 1L 0L
 
 let cilint_of_string (s:string) : cilint = 
-  cilint_of_big_int (big_int_of_string s)
+  cilint_of_big_int (Z.of_string s)
 
 let string_of_cilint (c:cilint) : string = 
   match c with 
   | Small i -> string_of_int i
-  | Big b -> string_of_big_int b
+  | Big b -> Z.to_string b
 
 (* Divide rounding towards zero *)
 let div0_cilint (c1:cilint) (c2:cilint) = 
@@ -131,12 +135,12 @@ let div0_cilint (c1:cilint) (c2:cilint) =
   | _ ->
       let b1 = big_int_of_cilint c1 in
       let b2 = big_int_of_cilint c2 in 
-      let q, r = quomod_big_int b1 b2 in
-      if lt_big_int b1 zero_big_int && (not (eq_big_int r zero_big_int)) then
-	if gt_big_int b2 zero_big_int then
-	  Big (succ_big_int q)
+      let q, r = Z.ediv_rem b1 b2 in
+      if Z.lt b1 Z.zero && (not (Z.equal r Z.zero)) then
+	if Z.gt b2 Z.zero then
+	  Big (Z.succ q)
 	else
-	  Big (pred_big_int q)
+	  Big (Z.pred q)
       else
 	Big q
 
@@ -157,17 +161,17 @@ let logop op c1 c2 =
 	  (* Once we only have all-0/all-1 values left, we can find whether
 	     the infinite high-order bits are all-0 or all-1 by checking the
 	     behaviour of op on b1 and b2. *)
-	  if op (int_of_big_int b1) (int_of_big_int b2) = 0 then
+	  if op (Z.to_int b1) (Z.to_int b2) = 0 then
 	    acc
 	  else
-	    sub_big_int acc mul
+	    Z.sub acc mul
 	else
-	  let hi1, lo1 = quomod_big_int b1 b30 in
-	  let hi2, lo2 = quomod_big_int b2 b30 in
-	  let lo = op (int_of_big_int lo1) (int_of_big_int lo2) in
-	  loop hi1 hi2 (mult_big_int mul b30) 
-	    (add_big_int acc (mult_big_int mul (big_int_of_int lo)))
-      in cilint_of_big_int (loop b1 b2 unit_big_int zero_big_int)
+	  let hi1, lo1 = Z.ediv_rem b1 b30 in
+	  let hi2, lo2 = Z.ediv_rem b2 b30 in
+	  let lo = op (Z.to_int lo1) (Z.to_int lo2) in
+	  loop hi1 hi2 (Z.mul mul b30) 
+	    (Z.add acc (Z.mul mul (Z.of_int lo)))
+      in cilint_of_big_int (loop b1 b2 Z.one Z.zero)
 
 let logand_cilint = logop (land)
 let logor_cilint = logop (lor)
@@ -176,15 +180,15 @@ let logxor_cilint = logop (lxor)
 let shift_right_cilint (c1:cilint) (n:int) : cilint = 
   match c1 with
   | Small i -> Small (i asr n)
-  | Big b -> cilint_of_big_int (div_big_int b (power_int_positive_int 2 n))
+  | Big b -> cilint_of_big_int (Z.shift_right b n)
 
 let shift_left_cilint (c1:cilint) (n:int) : cilint = 
-  cilint_of_big_int (mult_big_int (big_int_of_cilint c1) (power_int_positive_int 2 n))
+  cilint_of_big_int (Z.shift_left (big_int_of_cilint c1) n)
 
 let lognot_cilint (c1:cilint) : cilint = 
   match c1 with
   | Small i -> Small (lnot i)
-  | Big b -> Big (pred_big_int (minus_big_int b))
+  | Big b -> Big (Z.pred (Z.neg b))
 
 let truncate_signed_cilint (c:cilint) (n:int) : cilint * truncation =
   match c with
@@ -212,18 +216,18 @@ let truncate_signed_cilint (c:cilint) (n:int) : cilint * truncation =
       in Small tval, trunc
   | _ ->
       let b = big_int_of_cilint c in
-      let max = power_int_positive_int 2 (n - 1) in
-      let truncmax = power_int_positive_int 2 n in
-      let bits = mod_big_int b truncmax in
+      let max = Z.pow two (n - 1) in
+      let truncmax = Z.pow two n in
+      let bits = Z.rem b truncmax in
       let tval = 
-	if lt_big_int bits max then
+	if Z.lt bits max then
 	  bits
 	else
-	  sub_big_int bits truncmax
+	  Z.sub bits truncmax
       in
       let trunc = 
-	if ge_big_int b max || lt_big_int b (minus_big_int max) then
-	  if ge_big_int b truncmax then 
+	if Z.geq b max || Z.lt b (Z.neg max) then
+	  if Z.geq b truncmax then 
 	    BitTruncation
 	  else
 	    ValueTruncation
@@ -249,12 +253,12 @@ let truncate_unsigned_cilint (c:cilint) (n:int) : cilint * truncation =
       in Small bits, trunc
   | _ ->
       let b = big_int_of_cilint c in
-      let max = power_int_positive_int 2 (n - 1) in
-      let truncmax = power_int_positive_int 2 n in
-      let bits = mod_big_int b truncmax in
+      let max = Z.pow two (n - 1) in
+      let truncmax = Z.pow two n in
+      let bits = Z.rem b truncmax in
       let trunc = 
-	if ge_big_int b truncmax || lt_big_int b zero_big_int then
-	  if lt_big_int b (minus_big_int max) then
+	if Z.geq b truncmax || Z.lt b Z.zero then
+	  if Z.lt b (Z.neg max) then
 	    BitTruncation
 	  else
 	    ValueTruncation
@@ -265,4 +269,4 @@ let truncate_unsigned_cilint (c:cilint) (n:int) : cilint * truncation =
 let is_int_cilint (c:cilint) : bool = 
   match c with
   | Small _ -> true
-  | Big b -> is_int_big_int b
+  | Big b -> Z.fits_int b

src/cilint.mli

@@ -3,7 +3,7 @@
 (** The cilint type is public and not just big_int to make life with ocamldebug
     easier. Please do not rely on this representation, use the ..._of_cilint
     functions to get at a cilint's value. *)
-type cilint = Small of int | Big of Big_int.big_int
+type cilint = Small of int | Big of Z.t
 
 (** 0 as a cilint *)
 val zero_cilint : cilint
@@ -85,7 +85,7 @@ val int_of_cilint : cilint -> int
 val int64_of_cilint : cilint -> int64
 
 (** Return the cilint's value as a big_int *)
-val big_int_of_cilint : cilint -> Big_int.big_int
+val big_int_of_cilint : cilint -> Z.t
 
 (** Return the cilint's value as a string *)
 val string_of_cilint : cilint -> string
@@ -97,7 +97,7 @@ val cilint_of_int : int -> cilint
 val cilint_of_int64 : int64 -> cilint
 
 (** Make a cilint from a big_int *)
-val cilint_of_big_int : Big_int.big_int -> cilint
+val cilint_of_big_int : Z.t -> cilint
 
 (** Make a cilint from a string *)
 val cilint_of_string : string -> cilint

src/ext/partial/heap.ml

@@ -9,7 +9,7 @@ type ('a) t = {
 } 
 
 let create size = {
-  elements = Array.create (size+1) (max_int,None) ;
+  elements = Array.make (size+1) (max_int,None) ;
   size = 0 ;
   capacity = size ; 
 }