From fb55a4cda6f6ff6b9a68bc21adaafcff25f8f45a Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 11:52:03 +0100 Subject: [PATCH 01/12] replace deprecated Array.create, String.set and String.uppercase with modern equivalents --- src/cil.ml | 4 ++-- src/ext/partial/heap.ml | 2 +- src/frontc/cabs2cil.ml | 4 ++-- src/ocamlutil/bitmap.ml | 2 +- src/ocamlutil/errormsg.ml | 4 ++-- src/ocamlutil/inthash.ml | 2 +- src/ocamlutil/longarray.ml | 2 +- src/ocamlutil/pretty.ml | 6 +++--- 8 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 63da92793..bd3920744 100755 --- a/src/cil.ml +++ b/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 *) @@ -5090,7 +5090,7 @@ let makeValidSymbolName (s: string) = | _ -> false in if isinvalid then - String.set s i '_'; + Bytes.set s i '_'; done; s diff --git a/src/ext/partial/heap.ml b/src/ext/partial/heap.ml index 10f48a045..5fbbe372c 100644 --- a/src/ext/partial/heap.ml +++ b/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 ; } diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index dc185e133..61721cd7d 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -1924,7 +1924,7 @@ let rec setOneInit (this: preInit) let pMaxIdx, pArray = match this with NoInitPre -> (* No initializer so far here *) - ref idx, ref (Array.create (max 32 (idx + 1)) NoInitPre) + ref idx, ref (Array.make (max 32 (idx + 1)) NoInitPre) | CompoundPre (pMaxIdx, pArray) -> if !pMaxIdx < idx then begin @@ -3417,7 +3417,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) 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 match ct with A.CONST_INT str -> begin diff --git a/src/ocamlutil/bitmap.ml b/src/ocamlutil/bitmap.ml index 14d26a08b..33f5f9aea 100644 --- a/src/ocamlutil/bitmap.ml +++ b/src/ocamlutil/bitmap.ml @@ -10,7 +10,7 @@ type t = { mutable nrWords : int; let enlarge b newWords = let newbitmap = if newWords > b.nrWords then - let a = Array.create newWords Int32.zero in + let a = Array.make newWords Int32.zero in Array.blit b.bitmap 0 a 0 b.nrWords; a else diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index 2ffee51cf..857d62b5c 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -217,9 +217,9 @@ let cleanFileName str = else let c = String.get str1 i in if c <> '\\' then begin - String.set str1 copyto c; loop (copyto + 1) (i + 1) + Bytes.set str1 copyto c; loop (copyto + 1) (i + 1) end else begin - String.set str1 copyto '/'; + Bytes.set str1 copyto '/'; if i < l - 2 && String.get str1 (i + 1) = '\\' then loop (copyto + 1) (i + 2) else diff --git a/src/ocamlutil/inthash.ml b/src/ocamlutil/inthash.ml index 8d5bd32af..a6253b9b6 100644 --- a/src/ocamlutil/inthash.ml +++ b/src/ocamlutil/inthash.ml @@ -34,7 +34,7 @@ let resize tbl = let osize = Array.length odata in let nsize = min (2 * osize + 1) Sys.max_array_length in if nsize <> osize then begin - let ndata = Array.create nsize Empty in + let ndata = Array.make nsize Empty in let rec insert_bucket = function Empty -> () | Cons(key, data, rest) -> diff --git a/src/ocamlutil/longarray.ml b/src/ocamlutil/longarray.ml index ed9f533b1..0cdef6154 100644 --- a/src/ocamlutil/longarray.ml +++ b/src/ocamlutil/longarray.ml @@ -24,7 +24,7 @@ let split_idx (idx: int) : int option = let rec create (len: int) (init: 'a) : 'a t = let len1, len2 = split_len len in - (Array.create len1 init) :: (if len2 > 0 then create len2 init else []) + (Array.make len1 init) :: (if len2 > 0 then create len2 init else []) let rec init (len: int) (fn: int -> 'a) : 'a t = let len1, len2 = split_len len in diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml index 41180974f..ce889d356 100644 --- a/src/ocamlutil/pretty.ml +++ b/src/ocamlutil/pretty.ml @@ -726,7 +726,7 @@ let gprintf (finish : doc -> 'b) ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) let format_spec = "% " in - String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc (Int64.format format_spec n)) @@ -736,7 +736,7 @@ let gprintf (finish : doc -> 'b) ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) let format_spec = "% " in - String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc (Int32.format format_spec n)) @@ -746,7 +746,7 @@ let gprintf (finish : doc -> 'b) ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) let format_spec = "% " in - String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc (Nativeint.format format_spec n)) From 3220ccb3d744bc33df9f81cd84d1334bd88c1fae Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 11:55:49 +0100 Subject: [PATCH 02/12] Change improper usage of String.copy (deprecated; Strings are immutable) to use Bytes instead --- src/cil.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index bd3920744..64e60bb0b 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -5080,10 +5080,10 @@ 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 @@ -5092,7 +5092,7 @@ let makeValidSymbolName (s: string) = if isinvalid then Bytes.set s i '_'; done; - s + Bytes.to_string s let rec addOffset (toadd: offset) (off: offset) : offset = match off with From a475694a39cc0ea8c0b40582c259d36862a80d05 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 13:06:23 +0100 Subject: [PATCH 03/12] start of effort to remove bigint and replace with zarith; does not currently build (can't find Z) --- Makefile.in | 2 +- src/cilint.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Makefile.in b/Makefile.in index 9e6b59d24..b68a247c0 100644 --- a/Makefile.in +++ b/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" >>$@ diff --git a/src/cilint.ml b/src/cilint.ml index ae17e4d97..ddd6a1bd0 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -21,9 +21,9 @@ 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 +open Z + +type cilint = Small of int | Big of Z.t type truncation = NoTruncation | ValueTruncation | BitTruncation let zero_cilint = Small 0 From a9db4135189f81329cf2c332249a3703c3ee7023 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 13:08:01 +0100 Subject: [PATCH 04/12] update one more secret use of String.set to Bytes --- src/formatlex.mll | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/formatlex.mll b/src/formatlex.mll index 584a060d5..93d7ee61e 100644 --- a/src/formatlex.mll +++ b/src/formatlex.mll @@ -145,11 +145,11 @@ let scan_oct_escape str = * We convert L"Hi" to "H\000i\000" *) let wbtowc wstr = let len = String.length wstr in - let dest = String.make (len * 2) '\000' in + let dest = Bytes.make (len * 2) '\000' in for i = 0 to len-1 do dest.[i*2] <- wstr.[i] ; done ; - dest + Bytes.to_string dest (* This function converst the "Hi" in L"Hi" to { L'H', L'i', L'\0' } *) let wstr_to_warray wstr = From 565e6c7264aac2379d5ae66a21361e0a329336bf Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 13:28:38 +0100 Subject: [PATCH 05/12] update tags and myocamlbuild to link zarith for building of cilint and use ocamlfind with ocamlbuild to find the library --- myocamlbuild.ml | 9 +++++++++ src/_tags | 3 ++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 5f3800b90..d0e0470c2 100644 --- a/myocamlbuild.ml +++ b/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"; diff --git a/src/_tags b/src/_tags index 646cc2d47..6f2aab1ab 100644 --- a/src/_tags +++ b/src/_tags @@ -1,4 +1,5 @@ or or or : include : package(findlib) -: use_unix, use_str, use_nums, use_dynlink, use_cil, linkall, package(findlib) +: use_unix, use_str, use_dynlink, use_cil, linkall, package(findlib) +: use_zarith From e6c856eec409619847cd5cbe85325357aa78920f Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 13:28:57 +0100 Subject: [PATCH 06/12] straight replacement of Big_int with Z.t in cilint.mli --- src/cilint.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cilint.mli b/src/cilint.mli index f6d6983e4..bfafc4bf9 100644 --- a/src/cilint.mli +++ 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 From 3afd67834fa90c1e3fd622526484d75b13666f04 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 16:17:49 +0100 Subject: [PATCH 07/12] first pass of edits to convert cilint to Zarith. --- src/cilint.ml | 139 ++++++++++++++++++++++++++------------------------ 1 file changed, 73 insertions(+), 66 deletions(-) diff --git a/src/cilint.ml b/src/cilint.ml index ddd6a1bd0..1e472d18c 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -20,69 +20,76 @@ The implementation can be simplified once OCaml 3.11.1 shows up, with bitwise operations on big_ints, and bug-fixed versions of int64_of_big_int and big_int_of_int64. *) - -open Z +(* CLG notes: it's not obvious to me that we need all this; it might make + more sense to just transition all of Cil to Z/Zarith. However, I'm making + the small/local change for now *) 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 = (* CLG: the equality b/w minus 1 and b here isn't obvious to me, double-check *) + 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 (* CLG: remember to check when sinus headache goes away that rem <--> mod *) + 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 (* CLG: to_int might overflow, was that true of bigint? I assume yes? *) let rec cilint_of_int64 (i64:int64) : cilint = if Int64.compare i64 (Int64.of_int min_int) >= 0 && @@ -92,12 +99,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 +113,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 +138,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 +164,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 +183,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 +219,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 +256,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 +272,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 From 2bfc2db81863486a74a65cdb24e03019ebb02832 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 16:27:56 +0100 Subject: [PATCH 08/12] update treatment of Strings to Bytes in errormsg module; should have same behavior with previous versions of OCaml, while fixing compilation failure on 4.06 --- src/ocamlutil/errormsg.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index 857d62b5c..6b6ef06d6 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -205,28 +205,29 @@ let setHFile (f: string) : unit = let rem_quotes str = String.sub str 1 ((String.length str) - 2) +(* Change \ into / in file names. To avoid complications with escapes *) (* Change \ into / in file names. To avoid complications with escapes *) let cleanFileName str = let str1 = if str <> "" && String.get str 0 = '"' (* '"' ( *) - then rem_quotes str else str in - let l = String.length str1 in + then Bytes.of_string (rem_quotes str) else Bytes.of_string str in + let l = Bytes.length str1 in let rec loop (copyto: int) (i: int) = if i >= l then - String.sub str1 0 copyto + Bytes.sub str1 0 copyto else - let c = String.get str1 i in + let c = Bytes.get str1 i in if c <> '\\' then begin Bytes.set str1 copyto c; loop (copyto + 1) (i + 1) end else begin Bytes.set str1 copyto '/'; - if i < l - 2 && String.get str1 (i + 1) = '\\' then + if i < l - 2 && Bytes.get str1 (i + 1) = '\\' then loop (copyto + 1) (i + 2) else loop (copyto + 1) (i + 1) end in - loop 0 0 + Bytes.to_string (loop 0 0) let readingFromStdin = ref false From 20b04da92583cd5526054c2f0a26b76ea1776c45 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 16:34:24 +0100 Subject: [PATCH 09/12] update treatment of Strings to Bytes in Pretty; should have same behavior with previous versions of OCaml, while fixing compilation failure on 4.06 --- src/ocamlutil/pretty.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml index ce889d356..0076361d6 100644 --- a/src/ocamlutil/pretty.ml +++ b/src/ocamlutil/pretty.ml @@ -725,31 +725,31 @@ let gprintf (finish : doc -> 'b) invalid_arg ("dprintf: unimplemented format " ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) - let format_spec = "% " in + let format_spec = Bytes.of_string "% " in Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc - (Int64.format format_spec n)) + (Int64.format (Bytes.to_string format_spec) n)) (succ j')) | 'l' -> if j != i + 1 then invalid_arg ("dprintf: unimplemented format " ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) - let format_spec = "% " in + let format_spec = Bytes.of_string "% " in Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc - (Int32.format format_spec n)) + (Int32.format (Bytes.to_string format_spec) n)) (succ j')) | 'n' -> if j != i + 1 then invalid_arg ("dprintf: unimplemented format " ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) - let format_spec = "% " in + let format_spec = Bytes.of_string "% " in Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc - (Nativeint.format format_spec n)) + (Nativeint.format (Bytes.to_string format_spec) n)) (succ j')) | 'f' | 'e' | 'E' | 'g' | 'G' -> Obj.magic(fun f -> From 92c817ccf70a777cf4e47b3aea65358786c7ffb8 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 16:37:54 +0100 Subject: [PATCH 10/12] minor _tags update to make zarith findable --- src/_tags | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/_tags b/src/_tags index 6f2aab1ab..f61a3e388 100644 --- a/src/_tags +++ b/src/_tags @@ -1,5 +1,5 @@ or or or : include : package(findlib) -: use_unix, use_str, use_dynlink, use_cil, linkall, package(findlib) +: use_unix, use_str, use_dynlink, use_cil, use_zarith, linkall, package(findlib) : use_zarith From bdba0050f0638335847231e4ca3b206418ee1385 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 17:45:04 +0100 Subject: [PATCH 11/12] update README to note zarith dependency --- README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 608fec202..71e01f57a 100644 --- a/README.md +++ b/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 ----- From ed9109eb49d0afb69205e02415cb35c701d6cb5d Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 17:55:54 +0100 Subject: [PATCH 12/12] remove notes to self that no longer apply --- src/cilint.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/cilint.ml b/src/cilint.ml index 1e472d18c..102201116 100644 --- a/src/cilint.ml +++ b/src/cilint.ml @@ -20,9 +20,6 @@ The implementation can be simplified once OCaml 3.11.1 shows up, with bitwise operations on big_ints, and bug-fixed versions of int64_of_big_int and big_int_of_int64. *) -(* CLG notes: it's not obvious to me that we need all this; it might make - more sense to just transition all of Cil to Z/Zarith. However, I'm making - the small/local change for now *) type cilint = Small of int | Big of Z.t type truncation = NoTruncation | ValueTruncation | BitTruncation @@ -36,7 +33,7 @@ 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:Z.t) : bool = (* CLG: the equality b/w minus 1 and b here isn't obvious to me, double-check *) +let nobits (b:Z.t) : bool = Z.sign b = 0 || Z.equal b m1 let big_int_of_cilint (c:cilint) : Z.t = @@ -66,7 +63,7 @@ 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 (* CLG: remember to check when sinus headache goes away that rem <--> mod *) +let mod_cilint = b Z.rem let compare_cilint (c1:cilint) (c2:cilint) : int = @@ -89,7 +86,7 @@ let cilint_of_int (i:int) : cilint = Small i let int_of_cilint (c:cilint) : int = match c with | Small i -> i - | Big b -> Z.to_int b (* CLG: to_int might overflow, was that true of bigint? I assume yes? *) + | Big b -> Z.to_int b let rec cilint_of_int64 (i64:int64) : cilint = if Int64.compare i64 (Int64.of_int min_int) >= 0 &&