Merge pull request #1940 from goblint/addressdomain-of_int

Make int to pointer case more precise for non-zero ints, reuse `AD.of_int`

Author: sim642

src/analyses/base.ml

@@ -322,12 +322,7 @@ struct
       in
       match addr with
       | Addr (x, o) -> AD.of_mval (x, addToOffset n (Some x.vtype) o)
-      | NullPtr ->
-        begin match ID.equal_to Z.zero n with
-          | `Eq -> AD.null_ptr
-          | `Neq -> AD.unknown_ptr
-          | `Top -> AD.top_ptr
-        end
+      | NullPtr -> AD.of_int n
       | UnknownPtr
       | StrPtr _ ->
         begin match ID.equal_to Z.zero n with
@@ -2784,9 +2779,7 @@ struct
           let p_addr =
             match p_rv with
             | Address a -> a
-            (* TODO: don't we already have logic for this? *)
-            | Int i when ID.equal_to Z.zero i = `Eq -> AD.null_ptr
-            | Int i -> AD.top_ptr
+            | Int i -> AD.of_int i
             | _ -> AD.top_ptr (* TODO: why does this ever happen? *)
           in
           let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *)

src/cdomain/value/cdomains/addressDomain.ml

@@ -222,14 +222,10 @@ 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 =
-    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
+    match ID.equal_to Z.zero i with
+    | `Eq -> null_ptr
+    | `Neq -> not_null
+    | `Top -> top_ptr
 
   let to_int x =
     let ik = Cilfacade.ptr_ikind () in

src/cdomain/value/cdomains/valueDomain.ml

@@ -522,8 +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.equal_to Z.zero x = `Eq -> AD.null_ptr
-              | Int x -> AD.top_ptr
+              | Int x -> AD.of_int x
               (* we ignore casts to void* (above)! TODO report UB! *)
               | Address x -> cast_addr t x
               (*| Address x -> x*)
@@ -613,10 +612,7 @@ 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.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 y, Int x) -> Address (AD.join y (AD.of_int x))
     | (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)
@@ -646,10 +642,7 @@ 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.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 y, Int x) -> Address (AD.widen y (AD.join y (AD.of_int x)))
     | (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)

tests/regression/00-sanity/53-ptr-and-int.c

@@ -9,5 +9,8 @@ int main ()
   // &x equaling the constant 3 is exceedingly unlikely
   __goblint_check(y == 1); //UNKNOWN!
 
+  int *p = three; // implicit cast of 3 to pointer
+  __goblint_check(p);
+
   return 0;
 }