Merge pull request #1939 from goblint/intdomain-equal_to

Use `ID.equal_to` instead of `ID.to_int` where possible

Author: sim642

.semgrep/intDomain.yml

@@ -0,0 +1,10 @@
+rules:
+  - id: intDomain-to_int-equal
+    pattern-either:
+      - pattern: ID.to_int $X = Some $Y
+      - pattern: $X |> ID.to_int = Some $Y # Fix doesn't add correct parentheses
+      - pattern: GobOption.exists (Z.equal $Y) (ID.to_int $X)
+    fix: ID.equal_to $Y $X = `Eq
+    message: use dedicated and optimized function instead
+    languages: [ocaml]
+    severity: WARNING

src/analyses/base.ml

@@ -2542,7 +2542,7 @@ struct
       let dest_a, dest_typ = addr_type_of_exp dest in
       let value =
         match eval_ch with
-        | Int i when ID.to_int i = Some Z.zero ->
+        | Int i when ID.equal_to Z.zero i = `Eq ->
           VD.zero_init_value dest_typ
         | _ ->
           VD.top_value dest_typ
@@ -2712,7 +2712,7 @@ struct
       let st' =
         (* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *)
         match eval_rv ~man st ret_var with
-        | Int n when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> st
+        | Int n when ID.equal_to Z.zero n = `Eq -> st
         | Address ret_a ->
           begin match eval_rv ~man st id with
             | Thread a when ValueDomain.Threads.is_top a -> invalidate ~must:true ~man st [ret_var]
@@ -2759,7 +2759,7 @@ struct
           let ik = Cilfacade.ptrdiff_ikind () in
           let sizeval = eval_int ~man st size in
           let countval = eval_int ~man st n in
-          if ID.to_int countval = Some Z.one then
+          if ID.equal_to Z.one countval = `Eq then
             let blob_set = Option.map_default (fun heap_var -> [heap_var, TVoid [], VD.Blob (VD.bot (), sizeval, ZeroInit.calloc)]) [] heap_var in
             set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address addr):: blob_set)
           else
@@ -2785,7 +2785,7 @@ struct
             match p_rv with
             | Address a -> a
             (* TODO: don't we already have logic for this? *)
-            | Int i when ID.to_int i = Some Z.zero -> AD.null_ptr
+            | Int i when ID.equal_to Z.zero i = `Eq -> AD.null_ptr
             | Int i -> AD.top_ptr
             | _ -> AD.top_ptr (* TODO: why does this ever happen? *)
           in

src/analyses/baseInvariant.ml

@@ -292,7 +292,7 @@ struct
     (* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *)
     let inv_bin_int (a, b) ikind c op =
       let warn_and_top_on_zero x =
-        if GobOption.exists (Z.equal Z.zero) (ID.to_int x) then
+        if ID.equal_to Z.zero x = `Eq then
           (M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
            Checks.error Checks.Category.DivisionByZero "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
            ID.top_of ikind)
@@ -348,7 +348,8 @@ struct
          * If the upper bound of a is divisible by b, we can also meet with the result of a/b*b - c to get the precise [3,3].
          * If b is negative we have to look at the lower bound. *)
         let is_divisible bound =
-          GobOption.exists (fun ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some Z.zero) (bound a)
+          (* TODO: could check divisibility directly, instead of via ID? *)
+          GobOption.exists (fun ba -> ID.equal_to Z.zero (ID.rem (ID.of_int ikind ba) b) = `Eq) (bound a)
         in
         let max_pos = match ID.maximal b with None -> true | Some x -> Z.compare x Z.zero >= 0 in
         let min_neg = match ID.minimal b with None -> true | Some x -> Z.compare x Z.zero < 0 in
@@ -372,11 +373,11 @@ struct
         let callerFundec = Node.find_fundec man.node in
         let a = if PrecisionUtil.(is_congruence_active (int_precision_from_fundec_or_config callerFundec)) then
             let two = Z.of_int 2 in
-            match ID.to_int b, ID.to_excl_list c with
-            | Some b, Some ([v], _) when Z.equal b two ->
+            match ID.to_excl_list c with
+            | Some ([v], _) when ID.equal_to two b = `Eq ->
               let k = if Z.equal (Z.abs (Z.rem v two)) Z.zero then Z.one else Z.zero in
-              ID.meet (ID.of_congruence ikind (k, b)) a
-            | _, _ -> a
+              ID.meet (ID.of_congruence ikind (k, two)) a
+            | _ -> a
           else a
         in
         a, b
@@ -457,26 +458,25 @@ struct
         else
           a, b
       | BAnd ->
-        (* we only attempt to refine a here *)
-        let b_int = ID.to_int b in
+        (* we only attempt to refine a here *) (* TODO: why? *)
         let a =
-          match b_int with
-          | Some x when Z.equal x Z.one ->
-            (match ID.to_bool c with
-             | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
-             | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
-             | None -> a)
-          | _ -> a
+          if ID.equal_to Z.one b = `Eq then (
+            match ID.to_bool c with
+            | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
+            | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
+            | None -> a
+          )
+          else (
+            if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
+            a
+          )
         in
         if PrecisionUtil.get_bitfield () then
           (* refinement based on the following idea: bit set to zero in c and set to one in b must be zero in a and bit set to one in c must be one in a too (analogously for b) *)
           let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_band (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
           ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
-        else if b_int = None then
-          (if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
-           (a, b)
-          )
-        else a, b
+        else
+          (a, b)
       | op ->
         if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
         a, b

src/cdomain/value/cdomains/addressDomain.ml

@@ -222,10 +222,12 @@ struct
   let to_bool x      = if is_null x then Some false else if is_not_null x then Some true else None
 
   let of_int i =
-    match ID.to_int i with
-    | x when GobOption.exists BigIntOps.(equal (zero)) x -> null_ptr
-    | x when GobOption.exists BigIntOps.(equal (one)) x -> not_null
-    | _ -> match ID.to_excl_list i with
+    if ID.equal_to Z.zero i = `Eq then
+      null_ptr
+    else if ID.equal_to Z.one i = `Eq then
+      not_null
+    else
+      match ID.to_excl_list i with
       | Some (xs, _) when List.exists BigIntOps.(equal (zero)) xs -> not_null
       | _ -> top_ptr
 

src/cdomain/value/cdomains/arrayDomain.ml

@@ -541,6 +541,7 @@ struct
         let n = ask.eval_int e in
         VDQ.ID.to_int n
       in
+      (* TODO: use ID.equal_to here, VDQ.ID doesn't have though *)
       let equals_zero e = GobOption.exists (Z.equal Z.zero) (exp_value e) in
       let equals_maxIndex e =
         GobOption.exists2 (fun l -> Z.equal (Z.pred l)) (Option.bind length Idx.to_int) (exp_value e)

src/cdomain/value/cdomains/valueDomain.ml

@@ -291,10 +291,12 @@ struct
 
   type retnull = Null | NotNull | Maybe
   let is_null = function
-    | Int n  when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> Null
     | Int n ->
-      let zero_ik = ID.of_int (ID.ikind n) Z.zero in
-      if ID.to_bool (ID.ne n zero_ik) = Some true then NotNull else Maybe
+      begin match ID.equal_to Z.zero n with
+        | `Eq -> Null
+        | `Neq -> NotNull
+        | `Top -> Maybe
+      end
     | _ -> Maybe
 
   let get_ikind = function
@@ -520,7 +522,7 @@ struct
         (* cast to voidPtr are ignored TODO what happens if our value does not fit? *)
         | TPtr (t,_) ->
           Address (match v with
-              | Int x when ID.to_int x = Some Z.zero -> AD.null_ptr
+              | Int x when ID.equal_to Z.zero x = `Eq -> AD.null_ptr
               | Int x -> AD.top_ptr
               (* we ignore casts to void* (above)! TODO report UB! *)
               | Address x -> cast_addr t x
@@ -584,7 +586,7 @@ struct
         false
     | (Int x, Int y) -> ID.leq x y
     | (Float x, Float y) -> FD.leq x y
-    | (Int x, Address y) when ID.to_int x = Some Z.zero && not (AD.is_not_null y) -> true
+    | (Int x, Address y) when ID.equal_to Z.zero x = `Eq && not (AD.is_not_null y) -> true
     | (Int _, Address y) when AD.may_be_unknown y -> true
     | (Address _, Int y) when ID.is_top_of (Cilfacade.ptrdiff_ikind ()) y -> true
     | (Address x, Address y) -> AD.leq x y
@@ -611,10 +613,10 @@ struct
     | (Int x, Int y) -> (try Int (ID.join x y) with IntDomain.IncompatibleIKinds m -> Messages.warn ~category:Analyzer ~tags:[Category Imprecise] "%s" m; Top)
     | (Float x, Float y) -> Float (FD.join x y)
     | (Int x, Address y)
-    | (Address y, Int x) -> Address (match ID.to_int x with
-        | Some x when Z.equal x Z.zero -> AD.join AD.null_ptr y
-        | Some x -> AD.(join y not_null)
-        | None -> AD.join y AD.top_ptr)
+    | (Address y, Int x) -> Address (match ID.equal_to Z.zero x with (* TODO: AD.of_int? *)
+        | `Eq -> AD.join AD.null_ptr y
+        | `Neq -> AD.(join y not_null)
+        | `Top -> AD.join y AD.top_ptr)
     | (Address x, Address y) -> Address (AD.join x y)
     | (Struct x, Struct y) -> Struct (Structs.join x y)
     | (Union x, Union y) -> Union (Unions.join x y)
@@ -644,10 +646,10 @@ struct
     | (Float x, Float y) -> Float (FD.widen x y)
     (* TODO: symmetric widen, wtf? *)
     | (Int x, Address y)
-    | (Address y, Int x) -> Address (match ID.to_int x with
-        | Some x when Z.equal x Z.zero -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
-        | Some x -> AD.(widen y (join y not_null))
-        | None -> AD.widen y (AD.join y AD.top_ptr))
+    | (Address y, Int x) -> Address (match ID.equal_to Z.zero x with (* TODO: AD.of_int? *)
+        | `Eq -> AD.widen AD.null_ptr (AD.join AD.null_ptr y)
+        | `Neq -> AD.(widen y (join y not_null))
+        | `Top -> AD.widen y (AD.join y AD.top_ptr))
     | (Address x, Address y) -> Address (AD.widen x y)
     | (Struct x, Struct y) -> Struct (Structs.widen x y)
     | (Union x, Union y) -> Union (Unions.widen x y)
@@ -1008,12 +1010,9 @@ struct
               match v with
               | (Var var, Field (fld,_)) ->
                 let toptype = fld.fcomp in
-                let blob_size_opt = ID.to_int s in
                 not @@ ask.is_multiple var
                 && not @@ Cil.isVoidType t      (* Size of value is known *)
-                && GobOption.exists (fun blob_size -> (* Size of blob is known *)
-                    Z.equal blob_size (Z.of_int @@ Cilfacade.bytesSizeOf (TComp (toptype, [])))
-                  ) blob_size_opt
+                && ID.equal_to (Z.of_int @@ Cilfacade.bytesSizeOf (TComp (toptype, []))) s = `Eq (* Size of blob is known *)
               | _ -> false
             in
             if do_strong_update then
@@ -1034,6 +1033,7 @@ struct
                   | (Var var, _) ->
                     let blob_size_opt = ID.to_int s in
                     not @@ ask.is_multiple var
+                    (* TODO: could use ID.equal_to, but only if blob_destructive doesn't actually need known (but ignored!) size *)
                     && GobOption.exists (fun blob_size -> (* Size of blob is known *)
                         (not @@ Cil.isVoidType t     (* Size of value is known *)
                          && Z.equal blob_size (Z.of_int @@ Cil.alignOf_int t))