Merge pull request #1962 from goblint/int-predicates

Simplify return type of int domain comparison predicates

Author: sim642

src/analyses/base.ml

@@ -169,6 +169,11 @@ struct
 
   let iDtoIdx x = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) x (* TODO: proper castkind *)
 
+  let id_binary_pred result_ik f x y =
+    match f x y with
+    | Some b -> ID.of_bool result_ik b
+    | None -> ID.of_interval result_ik (Z.zero, Z.one)
+
   (** Unary float predicates return non-zero for [true].
       @see C11 7.12.3 *)
   let fd_unary_pred = function
@@ -180,7 +185,7 @@ struct
       @see C11 7.12.14, 6.5.8, 6.5.9 *)
   let fd_binary_pred = function
     | Some b -> ID.of_bool IInt b
-    | None -> ID.top_of IInt
+    | None -> ID.of_interval IInt (Z.zero, Z.one)
 
   let unop_ID = function
     | Neg  -> ID.neg
@@ -235,17 +240,17 @@ struct
          | `Neq ->
            Checks.safe Checks.Category.DivisionByZero);
         ID.rem x y
-    | Lt -> ID.lt
-    | Gt -> ID.gt
-    | Le -> ID.le
-    | Ge -> ID.ge
-    | Eq -> ID.eq
+    | Lt -> id_binary_pred result_ik ID.lt
+    | Gt -> id_binary_pred result_ik ID.gt
+    | Le -> id_binary_pred result_ik ID.le
+    | Ge -> id_binary_pred result_ik ID.ge
+    | Eq -> id_binary_pred result_ik ID.eq
     (* TODO: This causes inconsistent results:
        def_exc and interval definitely in conflict:
          evalint: base eval_rv m -> (Not {0, 1}([-31,31]),[1,1])
          evalint: base eval_rv 1 -> (1,[1,1])
          evalint: base query_evalint m == 1 -> (0,[1,1]) *)
-    | Ne -> ID.ne
+    | Ne -> id_binary_pred result_ik ID.ne
     | BAnd -> ID.logand
     | BOr -> ID.logor
     | BXor -> ID.logxor
@@ -306,7 +311,7 @@ struct
             | Some t ->
               let f_offset_bytes = Cilfacade.bytesOffsetOnly t (Field (f, NoOffset)) in
               let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int f_offset_bytes) in
-              begin match IdxDom.(to_bool (eq f_offset (neg n_offset))) with
+              begin match IdxDom.(eq f_offset (neg n_offset)) with
                 | Some true -> `NoOffset
                 | _ -> `Field (f, `Index (n_offset, `NoOffset))
               end
@@ -2388,10 +2393,10 @@ struct
           let casted_n = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) n in (* TODO: proper castkind *)
           let ds_eq_n =
             begin try ID.eq casted_ds casted_n
-              with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
+              with IntDomain.ArithmeticOnIntegerBot _ -> None
             end
           in
-          Option.default false (ID.to_bool ds_eq_n)
+          Option.default false ds_eq_n
         | _ -> false
       in
       let dest_a, dest_typ = addr_type_of_exp dst in

src/analyses/baseInvariant.ml

@@ -329,8 +329,8 @@ struct
          * However, a%b will give [-b+1, b-1] for a=top, but we only want the positive/negative side depending on the sign of c*b.
          * If c*b = 0 or it can be positive or negative, we need the full range for the remainder. *)
         let rem =
-          let is_pos = ID.to_bool @@ ID.gt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
-          let is_neg = ID.to_bool @@ ID.lt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
+          let is_pos = ID.gt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
+          let is_neg = ID.lt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
           let full = ID.rem a b in
           if is_pos then ID.meet (ID.starting ikind Z.zero) full
           else if is_neg then ID.meet (ID.ending ikind Z.zero) full

src/analyses/memOutOfBounds.ml

@@ -295,12 +295,12 @@ struct
               let one = intdom_of_int 1 in
               let casted_es = ID.sub casted_es one in
               begin try ID.lt casted_es casted_offs
-                with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+                with IntDomain.ArithmeticOnIntegerBot _ -> None
               end
             in
             let behavior = Undefined MemoryOutOfBoundsAccess in
             let cwe_number = 823 in
-            begin match ID.to_bool ptr_size_lt_offs with
+            begin match ptr_size_lt_offs with
               | Some true ->
                 (set_mem_safety_flag InvalidDeref;
                  M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs);
@@ -345,7 +345,7 @@ struct
           let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
           let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ao in (* TODO: proper castkind *)
           let ptr_size_lt_offs = ID.lt casted_ps casted_ao in
-          begin match ID.to_bool ptr_size_lt_offs with
+          begin match ptr_size_lt_offs with
             | Some true ->
               set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao;
@@ -433,7 +433,7 @@ struct
               let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
               let casted_o = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) o in (* TODO: proper castkind *)
               let ptr_size_lt_offs = ID.lt casted_ps casted_o in
-              begin match ID.to_bool ptr_size_lt_offs with
+              begin match ptr_size_lt_offs with
                 | Some true ->
                   set_mem_safety_flag InvalidDeref;
                   M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o;
@@ -479,7 +479,7 @@ struct
       let casted_en = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) en in (* TODO: proper castkind *)
       let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *)
       let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) in
-      begin match ID.to_bool dest_size_lt_count with
+      begin match dest_size_lt_count with
         | Some true ->
           set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en;

src/cdomain/value/cdomains/arrayDomain.ml

@@ -803,8 +803,8 @@ end
 (* This is the main array out of bounds check *)
 let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (e, v) =
   if GobConfig.get_bool "ana.arrayoob" then (* The purpose of the following 2 lines is to give the user extra info about the array oob *)
-    let idx_before_end = Idx.to_bool (Idx.lt v l) in (* check whether index is before the end of the array *)
-    let idx_after_start = Idx.to_bool (Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero)) in (* check whether the index is non-negative *)
+    let idx_before_end = Idx.lt v l in (* check whether index is before the end of the array *)
+    let idx_after_start = Idx.ge v (Idx.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) in (* check whether the index is non-negative *)
     (* For an explanation of the warning types check the Pull Request #255 *)
     match idx_after_start, idx_before_end with
     | Some true, Some true -> (* Certainly in bounds on both sides.*)

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

@@ -52,7 +52,6 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let one = of_int Ints_t.one
   let zero = of_int Ints_t.zero
-  let top_bool = join one zero
 
   let bits_known (z,o) = z ^: o
   let bits_invalid (z,o) = !:(z |: o)
@@ -591,34 +590,31 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   let eq ik x y =
     if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 && Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then
-      of_bool ik true
+      Some true
     else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 || Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then
-      of_bool ik false
+      Some false
     else
-      BArith.top_bool
+      None
 
-  let ne ik x y = match eq ik x y with
-    | t when t = of_bool ik true -> of_bool ik false
-    | t when t = of_bool ik false -> of_bool ik true
-    | _ -> BArith.top_bool
+  let ne ik x y = Option.map not (eq ik x y)
 
   let le ik x y =
     if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 then
-      of_bool ik true
+      Some true
     else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 then
-      of_bool ik false
+      Some false
     else
-      BArith.top_bool
+      None
 
   let ge ik x y = le ik y x
 
   let lt ik x y =
     if Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then
-      of_bool ik true
+      Some true
     else if Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then
-      of_bool ik false
+      Some false
     else
-      BArith.top_bool
+      None
 
   let gt ik x y = lt ik y x
 

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

@@ -124,7 +124,6 @@ struct
   let of_int ik (x: int_t) = normalize ik @@ Some (x, Z.zero)
   let zero = Some (Z.zero, Z.zero)
   let one  = Some (Z.one, Z.zero)
-  let top_bool = top()
 
   let of_bool _ik = function true -> one | false -> zero
 
@@ -444,48 +443,50 @@ struct
     res
 
   let ne ik (x: t) (y: t) = match x, y with
-    | Some (c1, m1), Some (c2, m2) when (m1 =: Z.zero) && (m2 =: Z.zero) -> of_bool ik (not (c1 =: c2 ))
-    | x, y -> if meet ik x y = None then of_bool ik true else top_bool
+    | Some (c1, m1), Some (c2, m2) when (m1 =: Z.zero) && (m2 =: Z.zero) -> Some (not (c1 =: c2))
+    | x, y -> if meet ik x y = None then Some true else None
 
   let eq ik (x: t) (y: t) = match x, y with
-    | Some (c1, m1), Some (c2, m2) when (m1 =: Z.zero) && (m2 =: Z.zero) -> of_bool ik (c1 =: c2)
-    | x, y -> if meet ik x y <> None then top_bool else of_bool ik false
+    | Some (c1, m1), Some (c2, m2) when (m1 =: Z.zero) && (m2 =: Z.zero) -> Some (c1 =: c2)
+    | x, y -> if meet ik x y <> None then None else Some false
 
   let comparison ik op x y = match x, y with
-    | None, None -> bot_of ik
+    | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c1, m1), Some (c2, m2) ->
       if m1 =: Z.zero && m2 =: Z.zero then
-        if op c1 c2 then of_bool ik true else of_bool ik false
+        Some (op c1 c2)
       else
-        top_bool
+        None
 
   let ge ik x y = comparison ik (>=:) x y
 
+  let pretty_bool_option = Pretty.docOpt (Pretty.dprintf "%B")
+
   let ge ik x y =
     let res = ge ik x y in
-    if M.tracing then  M.trace "congruence" "greater or equal : %a %a -> %a " pretty x pretty y pretty res;
+    if M.tracing then  M.trace "congruence" "greater or equal : %a %a -> %a" pretty x pretty y pretty_bool_option res;
     res
 
   let le ik x y = comparison ik (<=:) x y
 
   let le ik x y =
     let res = le ik x y in
-    if M.tracing then  M.trace "congruence" "less or equal : %a %a -> %a " pretty x pretty y pretty res;
+    if M.tracing then  M.trace "congruence" "less or equal : %a %a -> %a" pretty x pretty y pretty_bool_option res;
     res
 
   let gt ik x y = comparison ik (>:) x y
 
   let gt ik x y =
     let res = gt ik x y in
-    if M.tracing then  M.trace "congruence" "greater than : %a %a -> %a " pretty x pretty y pretty res;
+    if M.tracing then  M.trace "congruence" "greater than : %a %a -> %a" pretty x pretty y pretty_bool_option res;
     res
 
   let lt ik x y = comparison ik (<:) x y
 
   let lt ik x y =
     let res = lt ik x y in
-    if M.tracing then  M.trace "congruence" "less than : %a %a -> %a " pretty x pretty y pretty res;
+    if M.tracing then  M.trace "congruence" "less than : %a %a -> %a" pretty x pretty y pretty_bool_option res;
     res
 
   let invariant_ikind e ik x =

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

@@ -298,7 +298,6 @@ 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 (), (0, 1))
 
   let of_interval ik (x,y) =
     if Z.compare x y = 0 then
@@ -392,29 +391,29 @@ struct
   (* The equality check: *)
   let eq ik x y = match x,y with
     (* Not much to do with two exclusion sets: *)
-    | `Excluded _, `Excluded _ -> top_of IInt
+    | `Excluded _, `Excluded _ -> None
     (* Is x equal to an exclusion set, if it is a member then NO otherwise we
      * don't know: *)
-    | `Definite x, `Excluded (s,r) -> if S.mem x s then of_bool IInt false else top_of IInt
-    | `Excluded (s,r), `Definite x -> if S.mem x s then of_bool IInt false else top_of IInt
+    | `Definite x, `Excluded (s,r) -> if S.mem x s then Some false else None
+    | `Excluded (s,r), `Definite x -> if S.mem x s then Some false else None
     (* The good case: *)
-    | `Definite x, `Definite y -> of_bool IInt (x = y)
-    | `Bot, `Bot -> `Bot
+    | `Definite x, `Definite y -> Some (x = y)
+    | `Bot, `Bot -> None
     | _ ->
       (* 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)))
 
   (* The inequality check: *)
   let ne ik x y = match x,y with
     (* Not much to do with two exclusion sets: *)
-    | `Excluded _, `Excluded _ -> top_of IInt
+    | `Excluded _, `Excluded _ -> None
     (* Is x unequal to an exclusion set, if it is a member then Yes otherwise we
      * don't know: *)
-    | `Definite x, `Excluded (s,r) -> if S.mem x s then of_bool IInt true else top_of IInt
-    | `Excluded (s,r), `Definite x -> if S.mem x s then of_bool IInt true else top_of IInt
+    | `Definite x, `Excluded (s,r) -> if S.mem x s then Some true else None
+    | `Excluded (s,r), `Definite x -> if S.mem x s then Some true else None
     (* The good case: *)
-    | `Definite x, `Definite y -> of_bool IInt (x <> y)
-    | `Bot, `Bot -> `Bot
+    | `Definite x, `Definite y -> Some (x <> y)
+    | `Bot, `Bot -> None
     | _ ->
       (* 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)))
@@ -436,26 +435,26 @@ struct
 
   (* Comparison handling copied from Enums. *)
   let handle_bot x y f = match x, y with
-    | `Bot, `Bot -> `Bot
+    | `Bot, `Bot -> None
     | `Bot, _
     | _, `Bot -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | _, _ -> f ()
 
   let lt ik x y =
     handle_bot x y (fun () ->
         match minimal x, maximal x, minimal y, maximal y with
-        | _, Some x2, Some y1, _ when Z.compare x2 y1 < 0 -> of_bool ik true
-        | Some x1, _, _, Some y2 when Z.compare x1 y2 >= 0 -> of_bool ik false
-        | _, _, _, _ -> top_bool)
+        | _, Some x2, Some y1, _ when Z.compare x2 y1 < 0 -> Some true
+        | Some x1, _, _, Some y2 when Z.compare x1 y2 >= 0 -> Some false
+        | _, _, _, _ -> None)
 
   let gt ik x y = lt ik y x
 
   let le ik x y =
     handle_bot x y (fun () ->
         match minimal x, maximal x, minimal y, maximal y with
-        | _, Some x2, Some y1, _ when Z.compare x2 y1 <= 0 -> of_bool ik true
-        | Some x1, _, _, Some y2 when Z.compare x1 y2 > 0 -> of_bool ik false
-        | _, _, _, _ -> top_bool)
+        | _, Some x2, Some y1, _ when Z.compare x2 y1 <= 0 -> Some true
+        | Some x1, _, _, Some y2 when Z.compare x1 y2 > 0 -> Some false
+        | _, _, _, _ -> None)
 
   let ge ik x y = le ik y x
 
@@ -576,7 +575,7 @@ struct
       of_bool ik true
     | _, _ ->
       lift2 IntOps.BigIntOps.c_logor ik x y
-  let c_lognot ik = eq ik (of_int ik Z.zero)
+  let c_lognot ik x = match eq ik (of_int ik Z.zero) x with None -> top_of IInt | Some x -> of_bool IInt x (* TODO: avoid conversion *)
 
   let invariant_ikind e ik (x:t) =
     match x with