Improve int domain bitwise operators, support struct bitfields

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

@@ -193,7 +193,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
   (* bot = all bits are invalid *)
   let bot () = (BArith.zero_mask, BArith.zero_mask)
 
-  let top_of ik =
+  let top_of ?bitfield ik = (* TODO: use bitfield *)
     if GoblintCil.isSigned ik then top ()
     else (BArith.one_mask, Ints_t.of_bigint (snd (Size.range ik)))
 

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

@@ -44,7 +44,7 @@ struct
   let range ik = Size.range ik
 
   let top () = Some (Z.zero, Z.one)
-  let top_of ik = Some (Z.zero, Z.one)
+  let top_of ?bitfield ik = Some (Z.zero, Z.one)
   let bot () = None
   let bot_of ik = bot ()
 

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

@@ -84,7 +84,17 @@ struct
   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 top_overflow () = `Excluded (S.empty (), overflow_range)
   let bot () = `Bot
-  let top_of ik = `Excluded (S.empty (), size ik)
+  let top_of ?bitfield ik =
+    match bitfield with
+    | Some b when b <= Z.numbits (Size.range ik |> snd) ->
+      let range =
+        if Cil.isSigned ik then
+          R.of_interval range_ikind (Int64.of_int @@ -(b - 1), Int64.of_int b)
+        else
+          R.of_interval range_ikind (Int64.zero, Int64.of_int b)
+      in
+      `Excluded (S.empty (), range)
+    | _ -> `Excluded (S.empty (), size ik)
   let bot_of ik = bot ()
 
   let show x =
@@ -447,20 +457,49 @@ struct
 
   let ge ik x y = le ik y x
 
-  let lognot = lift1 Z.lognot
+  let lognot ik x = norm ik @@ match x with
+    | `Excluded (s, r) ->
+      let s' = S.map Z.lognot s in
+      let r' = match R.minimal r, R.maximal r with
+        | Some min, Some max when Int64.compare (Int64.neg max) Int64.zero <= 0 && Int64.compare (Int64.neg min) Int64.zero > 0 ->
+          R.of_interval range_ikind (Int64.neg max, Int64.neg min)
+        | _, _ -> apply_range Z.lognot r
+      in
+      `Excluded (s', r')
+    | `Definite x -> `Definite (Z.lognot x)
+    | `Bot -> `Bot
 
   let logand ik x y = norm ik (match x,y with
-      (* We don't bother with exclusion sets: *)
-      | `Excluded _, `Definite i ->
-        (* Except in two special cases *)
+      | `Excluded (_, r), `Definite i
+      | `Definite i, `Excluded (_, r) ->
         if Z.equal i Z.zero then
           `Definite Z.zero
         else if Z.equal i Z.one then
           of_interval IBool (Z.zero, Z.one)
-        else
-          top_of ik
-      | `Definite _, `Excluded _
-      | `Excluded _, `Excluded _ -> top_of ik
+        else (
+          match R.minimal r, R.maximal r with
+          | None, _
+          | _, None -> top_of ik
+          | Some r1, Some r2 ->
+            match Z.compare i Z.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+            | true, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.min r2 (Int64.of_int @@ Z.numbits i)))
+            | true, _ -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))
+            | _, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, r2))
+            | _, _ ->
+              let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
+        )
+      | `Excluded (_, p), `Excluded (_, r) ->
+        begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+          | Some p1, Some p2, Some r1, Some r2 ->
+            begin match Int64.compare p1 Int64.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+              | true, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.min p2 r2))
+              | true, _ -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, p2))
+              | _, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, r2))
+              | _, _ -> `Excluded (S.empty (), R.join p r)
+            end
+          | _ -> top_of ik
+        end
       (* The good case: *)
       | `Definite x, `Definite y ->
         (try `Definite (Z.logand x y) with | Division_by_zero -> top_of ik)
@@ -469,9 +508,58 @@ struct
         (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
         raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
+  let logor ik x y = norm ik (match x,y with
+      | `Excluded (_, r), `Definite i
+      | `Definite i, `Excluded (_, r) ->
+        if Z.compare i Z.zero >= 0 then
+          `Excluded (S.empty (), R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)))
+        else (
+          match R.minimal r, R.maximal r with
+          | None, _
+          | _, None -> top_of ik
+          | Some r1, Some r2 ->
+            let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+            `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
+        )
+      | `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.join r1 r2)
+      | `Definite x, `Definite y ->
+        (try `Definite (Z.logor x y) with | Division_by_zero -> top_of ik)
+      | `Bot, `Bot -> `Bot
+      | _ ->
+        (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
+        raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
-  let logor  = lift2 Z.logor
-  let logxor = lift2 Z.logxor
+  let logxor ik x y = norm ik (match x,y with
+      | `Definite i, `Excluded (_, r)
+      | `Excluded (_, r), `Definite i ->
+        begin match R.minimal r, R.maximal r with
+          | None, _
+          | _, None -> top_of ik
+          | Some r1, Some r2 ->
+            let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+            if Int64.compare r1 Int64.zero >= 0 && Z.compare i Z.zero >= 0 then
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, b))
+            else
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
+        end
+      | `Excluded (_, p), `Excluded (_, r) ->
+        begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+          | Some p1, Some p2, Some r1, Some r2 ->
+            if Int64.compare p1 Int64.zero >= 0 && Int64.compare r1 Int64.zero >= 0 then
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.max p2 r2))
+            else (
+              let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1; p2; r1; r2]) in
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
+            )
+          | _, _, _, _ -> top_of ik
+        end
+      (* The good case: *)
+      | `Definite x, `Definite y ->
+        (try `Definite (Z.logxor x y) with | Division_by_zero -> top_of ik)
+      | `Bot, `Bot -> `Bot
+      | _ ->
+        (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
+        raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     (* BigInt only accepts int as second argument for shifts; perform conversion here *)

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

@@ -21,10 +21,21 @@ module Enums : S with type int_t = Z.t = struct
   let bot () = failwith "bot () not implemented for Enums"
   let bot_of ik = Inc (BISet.empty ())
   let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
-  let top_of ik =
+
+  let top_of ?bitfield ik =
     match ik with
     | IBool -> top_bool
-    | _ -> Exc (BISet.empty (), size ik)
+    | _ ->
+      match bitfield with
+      | Some b when b <= Z.numbits (Size.range ik |> snd) ->
+        let range =
+          if Cil.isSigned ik then
+            R.of_interval range_ikind (Int64.of_int @@ -(b - 1), Int64.of_int b)
+          else
+            R.of_interval range_ikind (Int64.of_int 0, Int64.of_int b)
+        in
+        Exc (BISet.empty (), range)
+      | _ -> Exc (BISet.empty (), size ik)
 
   let range ik = Size.range ik
 
@@ -209,10 +220,114 @@ module Enums : S with type int_t = Z.t = struct
 
   let rem = lift2 Z.rem
 
-  let lognot = lift1 Z.lognot
-  let logand = lift2 Z.logand
-  let logor  = lift2 Z.logor
-  let logxor = lift2 Z.logxor
+  let apply_range f r = (* apply f to the min/max of the old range r to get a new range *)
+    let rf m = (size % Size.min_for % f) (m r) in
+    let r1, r2 = rf Exclusion.min_of_range, rf Exclusion.max_of_range in
+    R.join r1 r2
+
+  let lognot ikind v = norm ikind @@ match v with
+    | Inc x when BISet.is_empty x -> v
+    | Inc x when BISet.is_singleton x -> Inc (BISet.singleton (Z.lognot (BISet.choose x)))
+    | Inc x -> Inc (BISet.map Z.lognot x) (* TODO: don't operate on Inc? *)
+    | Exc (s, r) ->
+      let s' = BISet.map Z.lognot s in
+      let r' = match R.minimal r, R.maximal r with
+        | Some min, Some max -> R.of_interval range_ikind (Int64.neg max, Int64.neg min) (* TODO: why missing conditions compared to DefExc lognot? *)
+        | _, _ -> apply_range Z.lognot r
+      in
+      Exc (s', r')
+
+  let logand ikind u v = handle_bot u v (fun () ->
+      norm ikind @@ match u, v with
+      | Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
+        Inc (BISet.singleton (Z.logand (BISet.choose x) (BISet.choose y)))
+      | Inc x, Exc (s, r)
+      | Exc (s, r), Inc x ->
+        let f i =
+          match R.minimal r, R.maximal r with
+          | None, _
+          | _, None -> R.top_of ikind
+          | Some r1, Some r2 ->
+            match Z.compare i Z.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+            | true, true -> R.of_interval range_ikind (Int64.zero, Int64.min r2 (Int64.of_int @@ Z.numbits i))
+            | true, _ -> R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)
+            | _, true -> R.of_interval range_ikind (Int64.zero, r2)
+            | _, _ ->
+              let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+              R.of_interval range_ikind (Int64.neg b, b)
+        in
+        let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in
+        Exc (BISet.empty (), r')
+      | Exc (_, p), Exc (_, r) ->
+        begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+          | Some p1, Some p2, Some r1, Some r2 ->
+            begin match Int64.compare p1 Int64.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+              | true, true -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, Int64.min p2 r2))
+              | true, _ -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, p2))
+              | _, true -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, r2))
+              | _, _ -> Exc (BISet.empty (), R.join p r)
+            end
+          | _ -> top_of ikind
+        end
+      | _, _ -> top_of ikind
+    )
+
+  let logor ikind u v = handle_bot u v (fun () ->
+      norm ikind @@ match u, v with
+      | Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
+        Inc (BISet.singleton (Z.logor (BISet.choose x) (BISet.choose y)))
+      | Inc x, Exc (_, r)
+      | Exc (_, r), Inc x ->
+        let f i =
+          if Z.compare i Z.zero >= 0 then
+            R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))
+          else (
+            match R.minimal r, R.maximal r with
+            | None, _
+            | _, None -> R.top_of ikind
+            | Some r1, Some r2 ->
+              let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+              R.of_interval range_ikind (Int64.neg b, b)
+          )
+        in
+        let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in
+        Exc (BISet.empty (), r')
+      | Exc (_, r1), Exc (_, r2) -> Exc (BISet.empty (), R.join r1 r2)
+      | _ -> top_of ikind
+    )
+
+  let logxor ikind u v = handle_bot u v (fun () ->
+      norm ikind @@ match u, v with
+      | Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
+        Inc (BISet.singleton (Z.logxor (BISet.choose x) (BISet.choose y)))
+      | Inc x, Exc (_, r)
+      | Exc (_, r), Inc x ->
+        let f i =
+          match R.minimal r, R.maximal r with
+          | None, _
+          | _, None -> R.top_of ikind
+          | Some r1, Some r2 ->
+            let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+            if Int64.compare r1 Int64.zero >= 0 && Z.compare i Z.zero >= 0 then
+              R.of_interval range_ikind (Int64.zero, b)
+            else
+              R.of_interval range_ikind (Int64.neg b, b)
+        in
+        let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in
+        Exc (BISet.empty (), r')
+      | Exc (_, p), Exc (_, r) ->
+        begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+          | Some p1, Some p2, Some r1, Some r2 ->
+            if Int64.compare p1 Int64.zero >= 0 && Int64.compare r1 Int64.zero >= 0 then
+              Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, Int64.max p2 r2))
+            else (
+              let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1; p2; r1; r2]) in
+              Exc (BISet.empty (), R.of_interval range_ikind (Int64.neg b, b))
+            )
+          | _, _, _, _ -> top_of ikind
+        end
+      | _ -> top_of ikind
+    )
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     handle_bot x y (fun () ->

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

@@ -115,7 +115,7 @@ module IntDomTupleImpl = struct
 
   (* f0: constructors *)
   let bot () = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot } ()
-  let top_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top_of }
+  let top_of ?bitfield = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top_of ?bitfield }
   let bot_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot_of }
   let of_bool ik = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.of_bool ik }
   let of_excl_list ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_excl_list ik}