Improve int domain bitwise operators, support struct bitfields

src/analyses/base.ml

@@ -1641,7 +1641,7 @@ struct
               M.debug ~category:Analyzer "Cilfacade.typeOfLval failed Could not obtain the type of %a" d_lval (Var x, cil_offset);
               lval_type
       in
-      let update_offset old_value =
+      let update_offset old_value = 
         (* Projection globals to highest Precision *)
         let projected_value = project_val (Queries.to_value_domain_ask ask) None None value (is_global ask x) in
         let new_value = VD.update_offset ~blob_destructive (Queries.to_value_domain_ask ask) old_value offs projected_value lval_raw ((Var x), cil_offset) t in

src/analyses/tutorials/signs.ml

@@ -23,12 +23,12 @@ struct
 
   (* TODO: An attempt to abstract integers, but it's just a little wrong... *)
   let of_int i =
-    if Z.compare i Z.zero < 0 then Zero
-    else if Z.compare i Z.zero > 0 then Zero
+    if Z.compare i Z.zero < 0 then Neg
+    else if Z.compare i Z.zero > 0 then Pos
     else Zero
 
   let lt x y = match x, y with
-    | Neg, Pos | Neg, Zero -> true (* TODO: Maybe something missing? *)
+    | Neg, Pos | Neg, Zero | Zero, Pos -> true (* TODO: Maybe something missing? *)
     | _ -> false
 end
 
@@ -59,7 +59,7 @@ struct
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
-    | Const (CInt (i, _, _)) -> SL.top () (* TODO: Fix me! *)
+    | Const (CInt (i, _, _)) -> SL.of_int i (* TODO: Fix me! *)
     | Lval (Var x, NoOffset) -> D.find x d
     | _ -> SL.top ()
 

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 top_range = R.of_interval range_ikind (-99L, 99L) (* Since there is no top ikind we use a range that includes both ILongLong [-63,63] and IULongLong [0,64]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
   let top () = `Excluded (S.empty (), top_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
@@ -440,20 +445,39 @@ 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 -> 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 if Z.compare i Z.zero >= 0 then
+          `Excluded (S.empty (), R.meet r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)))
         else
-          top ()
-      | `Definite _, `Excluded _
-      | `Excluded _, `Excluded _ -> top ()
+          (match (R.minimal r, R.maximal r) with 
+          | (None, _) | (_, None) -> top ()
+          | (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 r2 Int64.zero < 0) then
+                `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, Int64.zero)) 
+              else if (Int64.compare r1 Int64.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))
+          ) 
+      | `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.meet r1 r2)
       (* The good case: *)
       | `Definite x, `Definite y ->
         (try `Definite (Z.logand x y) with | Division_by_zero -> top ())
@@ -462,9 +486,44 @@ 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 ()
+        | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in
+          `Excluded (S.empty (), R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int 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 ())
+    | `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
+      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 ()
+        | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in
+          `Excluded (S.empty (), R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int b)) 
+      end
+    | `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.join r1 r2)
+    (* The good case: *)
+    | `Definite x, `Definite y ->
+      (try `Definite (Z.logxor x y) with | Division_by_zero -> top ())
+    | `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

@@ -19,10 +19,17 @@ module Enums : S with type int_t = Z.t = struct
   let top () = failwith "top () 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
 
@@ -207,10 +214,83 @@ 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)))
+    | 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')
+    | _ -> top_of ikind
+
+  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 -> 
+          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 -> top ()
+            | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in
+              R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int 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.meet r1 r2)
+      | _,_ -> 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 -> top ()
+          | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in
+            R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int 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 -> 
+        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 -> top ()
+          | Some r1, Some r2 -> let b = Int.max (Z.numbits i) (Int64.to_int(Int64.max (Int64.abs r1) (Int64.abs r2))) in
+            R.of_interval range_ikind (Int64.of_int @@ -b, Int64.of_int 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 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

@@ -36,6 +36,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 *)
 
@@ -114,7 +115,7 @@ module IntDomTupleImpl = struct
   (* f0: constructors *)
   let top () = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top } ()
   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}