Merge pull request #1825 from goblint/biset-reduce

Fix enums bitwise operations crashing in `Inc`-`Exc` cases

Author: sim642

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

@@ -7,8 +7,8 @@ module BISet = struct
   include SetDomain.Make (IntOps.BigIntOps)
   let is_singleton s = cardinal s = 1
 
-  let reduce f s =
-    BatOption.get_exn (fold (fun x acc -> Option.map (f x) acc) s None) (Invalid_argument "BISet.reduce: empty set")
+  let map_reduce f g s =
+    s |> to_seq |> Seq.map f |> BatSeq.reduce g
 end
 
 (* The module [Exclusion] constains common functionality about handling of exclusion sets between [DefExc] and [Enums] *)

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

@@ -252,7 +252,7 @@ module Enums : S with type int_t = Z.t = struct
             let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
             (-b, b)
         in
-        let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
+        let r' = BISet.map_reduce f R.join x in (* reduce is safe because arguments are not bot here *)
         Exc (BISet.empty (), r')
       | Exc (_, ((p1, p2) as p)), Exc (_, ((r1, r2) as r)) ->
         begin match p1 >= 0, r1 >= 0 with
@@ -278,7 +278,7 @@ module Enums : S with type int_t = Z.t = struct
             (-b, b)
           )
         in
-        let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
+        let r' = BISet.map_reduce f R.join x in (* reduce is safe because arguments are not bot here *)
         Exc (BISet.empty (), r')
       | Exc (_, r1), Exc (_, r2) -> Exc (BISet.empty (), R.join r1 r2)
       | _ -> top_of ikind
@@ -297,7 +297,7 @@ module Enums : S with type int_t = Z.t = struct
           else
             (-b, b)
         in
-        let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
+        let r' = BISet.map_reduce f R.join x in (* reduce is safe because arguments are not bot here *)
         Exc (BISet.empty (), r')
       | Exc (_, (p1, p2)), Exc (_, (r1, r2)) ->
         if p1 >= 0 && r1 >= 0 then

tests/regression/98-bitwise-operations/08-logand-enums.c

@@ -0,0 +1,7 @@
+// PARAM: --enable ana.int.enums
+
+int main() {
+  int r; // rand
+  int x = r & 1; // NOCRASH
+  return 0;
+}