Simplify exclusion bit range module

Author: sim642

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

@@ -11,12 +11,12 @@ end
 (* The module [Exclusion] constains common functionality about handling of exclusion sets between [DefExc] and [Enums] *)
 module Exclusion =
 struct
-  module R = Interval32
+  module R = IntervalArith (IntOps.Int64Ops)
   (* We use these types for the functions in this module to make the intended meaning more explicit *)
-  type t = Exc of BISet.t * Interval32.t
+  type t = Exc of BISet.t * R.t
   type inc = Inc of BISet.t [@@unboxed]
-  let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
-  let min_of_range r = Size.min_from_bit_range (Option.get (R.minimal r))
+  let max_of_range r = Size.max_from_bit_range (R.maximal r)
+  let min_of_range r = Size.min_from_bit_range (R.minimal r)
   let cardinality_of_range r = Z.succ (Z.add (Z.neg (min_of_range r)) (max_of_range r))
 
   let cardinality_BISet s =
@@ -65,11 +65,11 @@ end
 module DefExc : S with type int_t = Z.t = (* definite or set of excluded values *)
 struct
   module S = BISet
-  module R = Interval32 (* range for exclusion *)
+  module R = Exclusion.R (* range for exclusion *)
 
   (* Ikind used for intervals representing the domain *)
   let range_ikind = Cil.IInt
-  let size t = R.of_interval range_ikind (let a,b = Size.bits_i64 t in Int64.neg a,b)
+  let size t = let a,b = Size.bits_i64 t in Int64.neg a,b
 
 
   type t = [
@@ -81,7 +81,7 @@ struct
   let name () = "def_exc"
 
 
-  let overflow_range = R.of_interval range_ikind (-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 = (-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 top_overflow () = `Excluded (S.empty (), overflow_range)
   let bot () = `Bot
   let top_of ik = `Excluded (S.empty (), size ik)
@@ -226,14 +226,14 @@ struct
       (* Unless one of them is zero, we can exclude it: *)
       else
         let a,b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
-        let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
+        let r = R.join a b in
         `Excluded ((if Z.equal x Z.zero || Z.equal y Z.zero then S.empty () else S.singleton Z.zero), r)
     (* A known value and an exclusion set... the definite value should no
      * longer be excluded: *)
     | `Excluded (s,r), `Definite x
     | `Definite x, `Excluded (s,r) ->
       if not (in_range r x) then
-        let a = R.of_interval range_ikind (Size.min_range_sign_agnostic x) in
+        let a = Size.min_range_sign_agnostic x in
         `Excluded (S.remove x s, R.join a r)
       else
         `Excluded (S.remove x s, r)
@@ -266,9 +266,11 @@ struct
     (* The greatest lower bound of two exclusion sets is their union, this is
      * just DeMorgans Law *)
     | `Excluded (x,r1), `Excluded (y,r2) ->
-      let r' = R.meet r1 r2 in
-      let s' = S.union x y |> S.filter (in_range r') in
-      `Excluded (s', r')
+      match R.meet r1 r2 with
+      | None -> `Bot
+      | Some r' ->
+        let s' = S.union x y |> S.filter (in_range r') in
+        `Excluded (s', r')
 
   let narrow ik x y = x
 
@@ -286,14 +288,14 @@ 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 (), R.of_interval range_ikind (0L, 1L))
+  let top_bool = `Excluded (S.empty (), (0L, 1L))
 
   let of_interval ik (x,y) =
     if Z.compare x y = 0 then
       of_int ik x
     else
       let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
-      let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
+      let r = R.join a b in
       let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else  S.empty () in
       norm ik @@ (`Excluded (ex, r))
 
@@ -323,7 +325,7 @@ struct
   let is_excl_list l = match l with `Excluded _ -> true | _ -> false
   let to_excl_list (x:t) = match x with
     | `Definite _ -> None
-    | `Excluded (s,r) -> Some (S.elements s, (Option.get (R.minimal r), Option.get (R.maximal r)))
+    | `Excluded (s,r) -> Some (S.elements s, r)
     | `Bot -> None
 
   let to_incl_list x = match x with

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

@@ -6,10 +6,10 @@ open GoblintCil
 
 (* Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions. *)
 module Enums : S with type int_t = Z.t = struct
-  module R = Interval32 (* range for exclusion *)
+  module R = Exclusion.R (* range for exclusion *)
 
   let range_ikind = Cil.IInt
-  let size t = R.of_interval range_ikind (let a,b = Size.bits_i64 t in Int64.neg a,b)
+  let size t = let a,b = Size.bits_i64 t in Int64.neg a,b
 
   type t =
     | Inc of BISet.t (* Inclusion set. *)
@@ -18,8 +18,8 @@ module Enums : S with type int_t = Z.t = struct
 
   type int_t = Z.t
   let name () = "enums"
-  let bot () = failwith "bot () not implemented for Enums"
-  let bot_of ik = Inc (BISet.empty ())
+  let bot () = Inc (BISet.empty ())
+  let bot_of ik = bot ()
   let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
   let top_of ik =
     match ik with
@@ -113,7 +113,7 @@ module Enums : S with type int_t = Z.t = struct
       of_int ik x
     else
       let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
-      let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
+      let r = R.join a b in
       let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in
       norm ik @@ (Exc (ex, r))
 
@@ -126,22 +126,25 @@ module Enums : S with type int_t = Z.t = struct
       let r = if BISet.is_empty y
         then r
         else
-          let (min_el_range, max_el_range) = Batteries.Tuple2.mapn (fun x -> R.of_interval range_ikind (Size.min_range_sign_agnostic x)) (BISet.min_elt y, BISet.max_elt y) in
+          let (min_el_range, max_el_range) = Batteries.Tuple2.mapn Size.min_range_sign_agnostic (BISet.min_elt y, BISet.max_elt y) in
           let range = R.join min_el_range max_el_range in
           R.join r range
       in
       Exc (BISet.diff x y, r)
 
-  let meet _ x y =
+  let meet ik x y =
     match x, y with
     | Inc x, Inc y -> Inc (BISet.inter x y)
     | Exc (x,r1), Exc (y,r2) ->
-      let r = R.meet r1 r2 in
-      let r_min, r_max = Exclusion.min_of_range r, Exclusion.max_of_range r in
-      let filter_by_range = BISet.filter (value_in_range (r_min, r_max)) in
-      (* We remove those elements from the exclusion set that do not fit in the range anyway *)
-      let excl = BISet.union (filter_by_range x) (filter_by_range y) in
-      Exc (excl, r)
+      begin match R.meet r1 r2 with
+        | None -> bot ()
+        | Some r ->
+          let r_min, r_max = Exclusion.min_of_range r, Exclusion.max_of_range r in
+          let filter_by_range = BISet.filter (value_in_range (r_min, r_max)) in
+          (* We remove those elements from the exclusion set that do not fit in the range anyway *)
+          let excl = BISet.union (filter_by_range x) (filter_by_range y) in
+          Exc (excl, r)
+      end
     | Inc x, Exc (y,r)
     | Exc (y,r), Inc x -> Inc (BISet.diff x y)
 
@@ -244,7 +247,7 @@ module Enums : S with type int_t = Z.t = struct
     | _ -> None
   let to_int = function Inc x when BISet.is_singleton x -> Some (BISet.choose x) | _ -> None
 
-  let to_excl_list = function Exc (x,r) when not (BISet.is_empty x) -> Some (BISet.elements x, (Option.get (R.minimal r), Option.get (R.maximal r))) | _ -> None
+  let to_excl_list = function Exc (x,r) when not (BISet.is_empty x) -> Some (BISet.elements x, r) | _ -> None
   let of_excl_list ik xs =
     let min_ik, max_ik = Size.range ik in
     let exc = BISet.of_list @@ List.filter (value_in_range (min_ik, max_ik)) xs in

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

@@ -123,7 +123,6 @@ struct
   let ending ik n =
     norm ik @@ Some (fst (range ik), n)
 
-  (* TODO: change signature of maximal, minimal to return big_int*)
   let maximal = function None -> None | Some (x,y) -> Some y
   let minimal = function None -> None | Some (x,y) -> Some x
 
@@ -445,4 +444,3 @@ struct
 end
 
 module Interval = IntervalFunctor (IntOps.BigIntOps)
-module Interval32 = IntDomWithDefaultIkind (IntDomLifter (SOverflowUnlifter (IntervalFunctor (IntOps.Int64Ops)))) (IntIkind)

src/cdomain/value/cdomains/intDomain0.ml

@@ -346,6 +346,11 @@ end
 
 (* Textbook interval arithmetic, without any overflow handling etc. *)
 module IntervalArith (Ints_t : IntOps.IntOps) = struct
+  type t = Ints_t.t * Ints_t.t [@@deriving eq, ord, hash]
+
+  (* TODO: use this for Interval and IntervalSet *)
+  let show (x,y) = "["^Ints_t.to_string x^","^Ints_t.to_string y^"]"
+
   let min4 a b c d = Ints_t.min (Ints_t.min a b) (Ints_t.min c d)
   let max4 a b c d = Ints_t.max (Ints_t.max a b) (Ints_t.max c d)
 
@@ -381,6 +386,20 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
   let zero = (Ints_t.zero, Ints_t.zero)
   let top_bool = (Ints_t.zero, Ints_t.one)
 
+  (* TODO: use these for Interval and IntervalSet *)
+  let maximal = snd
+  let minimal = fst
+
+  (* TODO: use these for Interval and IntervalSet *)
+  let leq (x1,x2) (y1,y2) = Ints_t.compare x1 y1 >= 0 && Ints_t.compare x2 y2 <= 0
+  let join (x1,x2) (y1,y2) = (Ints_t.min x1 y1, Ints_t.max x2 y2)
+  let meet (x1,x2) (y1,y2) =
+    let (r1, r2) as r = (Ints_t.max x1 y1, Ints_t.min x2 y2) in
+    if Ints_t.compare r1 r2 > 0 then
+      None
+    else
+      Some r
+
   let to_int (x1, x2) =
     if Ints_t.equal x1 x2 then Some x1 else None
 

src/cdomain/value/cdomains/intDomain_intf.ml

@@ -440,8 +440,6 @@ sig
 
   module IntervalSetFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list
 
-  module Interval32 :Y with (* type t = (IntOps.Int64Ops.t * IntOps.Int64Ops.t) option and *) type int_t = IntOps.Int64Ops.t
-
   module Interval : SOverflow with type int_t = Z.t
 
   module Bitfield : SOverflow with type int_t = Z.t

tests/unit/maindomaintest.ml

@@ -48,7 +48,6 @@ let intDomains: (module IntDomainProperties.S2) list = [
   (module IntDomain.SOverflowUnlifter(IntDomain.IntervalSet));
   (module IntDomain.SOverflowUnlifter(IntDomain.Bitfield));
   (* (module IntDomain.Flattened); *)
-  (* (module IntDomain.Interval32); *)
   (* (module IntDomain.Booleans); *)
   (* (module IntDomain.IntDomTuple); *)
 ]