Use int instead of int64 for bit ranges

Author: sim642

src/cdomain/value/cdomains/int/bitfieldDomain.ml

@@ -641,7 +641,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   let refine_with_bitfield ik x y = meet ik x y
 
-  let refine_with_excl_list ik t (excl : (int_t list * (int64 * int64)) option) : t = norm ik t
+  let refine_with_excl_list ik t (excl : (int_t list * (int * int)) option) : t = norm ik t
 
   let refine_with_incl_list ik t (incl : (int_t list) option) : t =
     let joined =match incl with

src/cdomain/value/cdomains/int/defExcDomain.ml

@@ -11,7 +11,7 @@ end
 (* The module [Exclusion] constains common functionality about handling of exclusion sets between [DefExc] and [Enums] *)
 module Exclusion =
 struct
-  module R = IntervalArith (IntOps.Int64Ops)
+  module R = IntervalArith (IntOps.NIntOps)
   (* We use these types for the functions in this module to make the intended meaning more explicit *)
   type t = Exc of BISet.t * R.t
   type inc = Inc of BISet.t [@@unboxed]
@@ -69,7 +69,7 @@ struct
 
   (* Ikind used for intervals representing the domain *)
   let range_ikind = Cil.IInt
-  let size t = let a,b = Size.bits_i64 t in Int64.neg a,b
+  let size t = let a,b = Size.bits t in -a,b
 
 
   type t = [
@@ -81,7 +81,7 @@ struct
   let name () = "def_exc"
 
 
-  let overflow_range = (-999L, 999L) (* Since there is no top ikind we use a range that includes both IInt128 [-127,127] and IUInt128 [0,128]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
+  let overflow_range = (-999, 999) (* Since there is no top ikind we use a range that includes both IInt128 [-127,127] and IUInt128 [0,128]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
   let top_overflow () = `Excluded (S.empty (), overflow_range)
   let bot () = `Bot
   let top_of ik = `Excluded (S.empty (), size ik)
@@ -288,7 +288,7 @@ struct
     | `Definite x -> Some (IntOps.BigIntOps.to_bool x)
     | `Excluded (s,r) when S.mem Z.zero s -> Some true
     | _ -> None
-  let top_bool = `Excluded (S.empty (), (0L, 1L))
+  let top_bool = `Excluded (S.empty (), (0, 1))
 
   let of_interval ik (x,y) =
     if Z.compare x y = 0 then

src/cdomain/value/cdomains/int/enumsDomain.ml

@@ -9,7 +9,7 @@ module Enums : S with type int_t = Z.t = struct
   module R = Exclusion.R (* range for exclusion *)
 
   let range_ikind = Cil.IInt
-  let size t = let a,b = Size.bits_i64 t in Int64.neg a,b
+  let size t = let a,b = Size.bits t in -a,b
 
   type t =
     | Inc of BISet.t (* Inclusion set. *)

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -413,7 +413,7 @@ struct
 
   let refine_with_interval ik a b = meet ik a b
 
-  let refine_with_excl_list ik (intv : t) (excl : (int_t list * (int64 * int64)) option) : t =
+  let refine_with_excl_list ik (intv : t) (excl : (int_t list * (int * int)) option) : t =
     match intv, excl with
     | None, _ | _, None -> intv
     | Some(l, u), Some(ls, (rl, rh)) ->

src/cdomain/value/cdomains/int/intervalSetDomain.ml

@@ -529,7 +529,7 @@ struct
   let refine_with_excl_list ik (intv : t) = function
     | None -> intv
     | Some (xs, range) ->
-      let excl_to_intervalset (ik: ikind) ((rl, rh): (int64 * int64)) (excl: int_t): t =
+      let excl_to_intervalset (ik: ikind) ((rl, rh): (int * int)) (excl: int_t): t =
         excl_range_to_intervalset ik (Ints_t.of_bigint (Size.min_from_bit_range rl),Ints_t.of_bigint (Size.max_from_bit_range rh)) excl
       in
       let excl_list = List.map (excl_to_intervalset ik range) xs in

src/cdomain/value/cdomains/intDomain0.ml

@@ -244,7 +244,7 @@ module Size = struct (* size in bits as int, range as int64 *)
   let bits ik = (* highest bits for neg/pos values *)
     let s = bit ik in
     if isSigned ik then s-1, s-1 else 0, s
-  let bits_i64 ik = BatTuple.Tuple2.mapn Int64.of_int (bits ik)
+  (* let bits_i64 ik = BatTuple.Tuple2.mapn Int64.of_int (bits ik) *)
   let range ik =
     let a,b = bits ik in
     let x = if isSigned ik then Z.neg (Z.shift_left Z.one a) (* -2^a *) else Z.zero in
@@ -275,16 +275,16 @@ module Size = struct (* size in bits as int, range as int64 *)
   (** @return Bit range always includes 0. *)
   let min_range_sign_agnostic x =
     let size ik =
-      let a,b = bits_i64 ik in
-      Int64.neg a,b
+      let a,b = bits ik in
+      -a,b
     in
     if sign x = `Signed then
       size (min_for x)
     else
       let a, b = size (min_for x) in
-      if b <= 64L then
-        let upper_bound_less = Int64.sub b 1L in
-        let max_one_less = Z.(pred @@ shift_left Z.one (Int64.to_int upper_bound_less)) in
+      if b <= 64 then
+        let upper_bound_less = b - 1 in
+        let max_one_less = Z.(pred @@ shift_left Z.one upper_bound_less) in
         if x <= max_one_less then
           a, upper_bound_less
         else
@@ -293,10 +293,10 @@ module Size = struct (* size in bits as int, range as int64 *)
         a, b
 
   (* From the number of bits used to represent a positive value, determines the maximal representable value *)
-  let max_from_bit_range pos_bits = Z.(pred @@ shift_left Z.one (to_int (Z.of_int64 pos_bits)))
+  let max_from_bit_range pos_bits = Z.(pred @@ shift_left Z.one (to_int (Z.of_int pos_bits)))
 
   (* From the number of bits used to represent a non-positive value, determines the minimal representable value *)
-  let min_from_bit_range neg_bits = Z.(if neg_bits = 0L then Z.zero else neg @@ shift_left Z.one (to_int (neg (Z.of_int64 neg_bits))))
+  let min_from_bit_range neg_bits = Z.(if neg_bits = 0 then Z.zero else neg @@ shift_left Z.one (to_int (neg (Z.of_int neg_bits))))
 
 end
 

src/cdomain/value/cdomains/intDomain_intf.ml

@@ -182,7 +182,7 @@ sig
   (** Give a boolean interpretation of an abstract value if possible, otherwise
     * don't return anything.*)
 
-  val to_excl_list: t -> (int_t list * (int64 * int64)) option
+  val to_excl_list: t -> (int_t list * (int * int)) option
   (** Gives a list representation of the excluded values from included range of bits if possible. *)
 
   val of_excl_list: Cil.ikind -> int_t list -> t
@@ -267,7 +267,7 @@ sig
   val refine_with_congruence: Cil.ikind -> t -> (int_t * int_t) option -> t
   val refine_with_bitfield: Cil.ikind -> t -> (int_t * int_t) -> t
   val refine_with_interval: Cil.ikind -> t -> (int_t * int_t) option -> t
-  val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t
+  val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int * int)) option -> t
   val refine_with_incl_list: Cil.ikind -> t -> int_t list option -> t
 
   val project: Cil.ikind -> PrecisionUtil.int_precision -> t -> t

src/domains/intDomainProperties.ml

@@ -13,7 +13,7 @@ sig
   val to_bool: t -> bool option
   val of_excl_list: Cil.ikind -> Z.t list -> t
   val is_excl_list: t -> bool
-  val to_excl_list: t -> (Z.t list * (int64 * int64)) option
+  val to_excl_list: t -> (Z.t list * (int * int)) option
 end
 
 module type OldSWithIkind =