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,9 +84,14 @@ 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 = match Cil.isSigned ik with
+        | true ->  R.of_interval range_ikind (Int64.of_int @@ -(b-1), Int64.of_int b)
+        | false -> R.of_interval range_ikind (Int64.of_int 0, Int64.of_int b) in
+      `Excluded (S.empty (), range)
+    | _ -> `Excluded (S.empty (), size ik)
   let bot_of ik = bot ()
-
   let show x =
     let short_size x = "("^R.show x^")" in
     match x with
@@ -447,20 +452,47 @@ 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
+          (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 +501,52 @@ 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 -> let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1;p2;r1;r2]) in
+            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
+              `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,17 @@ 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) -> 
+        Exc (BISet.empty (), match Cil.isSigned ik with
+          | true -> R.of_interval range_ikind (Int64.of_int @@ -(b-1), Int64.of_int b)
+          | false -> R.of_interval range_ikind (Int64.of_int 0, Int64.of_int b)
+          )
+      | _ -> Exc (BISet.empty (), size ik)
 
   let range ik = Size.range ik
 
@@ -209,10 +216,102 @@ 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 *)
+    (* If the Int64 might overflow on us during computation, we instead go to top_range *)
+    match R.minimal r, R.maximal r with
+    | _ ->
+      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)
+    | 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) 
+        | _ -> 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 = fun 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) -> 
+          (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)
+        | _,_ -> 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 = fun 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 = fun 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 -> let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1;p2;r1;r2]) in
+            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
+              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

@@ -38,6 +38,7 @@ module IntDomTupleImpl = struct
 
   (* only first-order polymorphism on functions -> use records to get around monomorphism restriction on arguments *)
   type 'b poly_in  = { fi  : 'a. 'a m -> 'b -> 'a } [@@unboxed] (* inject *)
+  type 'b poly_in_bitfield  = { fi_bitfield  : 'a. 'a m ->  ?bitfield:int -> 'b -> 'a } [@@unboxed] (* inject *)
   type 'b poly2_in  = { fi2  : 'a. 'a m2 -> 'b -> 'a } [@@unboxed] (* inject for functions that depend on int_t *)
   type 'b poly2_in_ovc  = { fi2_ovc  : 'a. 'a m2 -> 'b -> 'a * overflow_info} [@@unboxed] (* inject for functions that depend on int_t *)
 
@@ -115,7 +116,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}