Merge pull request #1768 from goblint/issue-1762

Fix pointer arithmethic on NULL

Author: sim642

src/analyses/base.ml

@@ -200,7 +200,7 @@ struct
     | PlusA -> ID.add
     | MinusA -> ID.sub
     | Mult -> ID.mul
-    | Div -> 
+    | Div ->
       fun x y ->
         (match ID.equal_to Z.zero y with
          | `Eq ->
@@ -209,7 +209,7 @@ struct
            M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero"
          | `Neq -> ());
         ID.div x y
-    | Mod -> 
+    | Mod ->
       fun x y ->
         (match ID.equal_to Z.zero y with
          | `Eq ->
@@ -303,24 +303,33 @@ struct
           `Field(f, addToOffset n t' o)
         | `NoOffset -> `Index(iDtoIdx n, `NoOffset)
       in
-      let default = function
-        | Addr.NullPtr when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> Addr.NullPtr
-        | _ -> Addr.UnknownPtr
-      in
-      match Addr.to_mval addr with
-      | Some (x, o) -> Addr.of_mval (x, addToOffset n (Some x.vtype) o)
-      | None -> default addr
+      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
+      | UnknownPtr
+      | StrPtr _ ->
+        begin match ID.equal_to Z.zero n with
+          | `Eq -> AD.singleton addr (* remains unchanged *)
+          | `Neq
+          | `Top -> AD.top_ptr
+        end
     in
+    let ad_concat_map f a = AD.fold (fun a acc -> AD.join (f a) acc) a (AD.empty ()) in
     let addToAddrOp p (n:ID.t):value =
       match op with
       (* For array indexing e[i] and pointer addition e + i we have: *)
       | IndexPI | PlusPI ->
-        Address (AD.map (addToAddr n) p)
+        Address (ad_concat_map (addToAddr n) p)
       (* Pointer subtracted by a value (e-i) is very similar *)
       (* Cast n to the (signed) ptrdiff_ikind, then add the its negated value. *)
       | MinusPI ->
         let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in
-        Address (AD.map (addToAddr n) p)
+        Address (ad_concat_map (addToAddr n) p)
       | Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
       | _ -> Address AD.top_ptr
     in

tests/regression/01-cpa/79-null-ptr-arith.c

@@ -0,0 +1,20 @@
+int main(void) {
+  int *p;
+  int i;
+  int *q = p + i;
+  *q = 42; // WARN (may NULL dereference)
+
+  if (p) {
+    q = p + i;
+    *q = 42; // WARN (may NULL dereference)
+
+    if (i == 0) {
+      q = p + i;
+      *q = 42; // NOWARN (no NULL dereference)
+    }
+    else {
+      q = p + i;
+      *q = 42; // WARN (may NULL dereference)
+    }
+  }
+}

tests/regression/55-loop-unrolling/12-loop-no-overflows.c

@@ -1,6 +1,6 @@
 // PARAM: --enable ana.int.interval_set
 // extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i
-
+// CRAM
 typedef unsigned int size_t;
 struct ldv_list_head {
     struct ldv_list_head *next, *prev;
@@ -29,7 +29,7 @@ void ldv_msg_free(struct ldv_msg *msg) {
 void main(void) {
     struct ldv_msg *msg;
     struct ldv_msg *n;
-    for (msg = ({ const typeof( ((typeof(*msg) *)0)->list ) *__mptr = ((&ldv_global_msg_list)->next); (typeof(*msg) *)( (char *)__mptr - ((size_t) &((typeof(*msg) *)0)->list) ); }), n = ({ const typeof( ((typeof(*(msg)) *)0)->list ) *__mptr = ((msg)->list.next); (typeof(*(msg)) *)( (char *)__mptr - ((size_t) &((typeof(*(msg)) *)0)->list) ); }); &msg->list != (&ldv_global_msg_list); msg = n, n = ({ const typeof( ((typeof(*(n)) *)0)->list ) *__mptr = ((n)->list.next); (typeof(*(n)) *)( (char *)__mptr - ((size_t) &((typeof(*(n)) *)0)->list) ); })) // NOWARN
+    for (msg = ({ const typeof( ((typeof(*msg) *)0)->list ) *__mptr = ((&ldv_global_msg_list)->next); (typeof(*msg) *)( (char *)__mptr - ((size_t) &((typeof(*msg) *)0)->list) ); }), n = ({ const typeof( ((typeof(*(msg)) *)0)->list ) *__mptr = ((msg)->list.next); (typeof(*(msg)) *)( (char *)__mptr - ((size_t) &((typeof(*(msg)) *)0)->list) ); }); &msg->list != (&ldv_global_msg_list); msg = n, n = ({ const typeof( ((typeof(*(n)) *)0)->list ) *__mptr = ((n)->list.next); (typeof(*(n)) *)( (char *)__mptr - ((size_t) &((typeof(*(n)) *)0)->list) ); }))
     {
         ldv_list_del(&msg->list);
         ldv_msg_free(msg);

tests/regression/55-loop-unrolling/12-loop-no-overflows.t

@@ -0,0 +1,25 @@
+Should have no overflow warning (on line 32).
+Now has NULL dereference warning there still.
+
+  $ goblint --enable ana.int.interval_set 12-loop-no-overflows.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:32:9-32:550)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:34:9-34:33)
+  [Info][Unsound] Unknown address given as function argument (12-loop-no-overflows.c:34:9-34:33)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:20:5-20:45)
+  [Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
+                                                         next -> {&ldv_global_msg_list}
+                                                         prev -> {&ldv_global_msg_list}
+                                                       }) (12-loop-no-overflows.c:20:5-20:45)
+  [Info][Unsound] Unknown address given as function argument (12-loop-no-overflows.c:20:5-20:45)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:15:5-15:22)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:16:5-16:22)
+  [Info][Unsound] Unknown address given as function argument (12-loop-no-overflows.c:35:9-35:26)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:24:5-24:20)
+  [Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer msg->data in function free is top. Potentially invalid memory deallocation may occur (12-loop-no-overflows.c:24:5-24:20)
+  [Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer msg in function free is top. Potentially invalid memory deallocation may occur (12-loop-no-overflows.c:25:5-25:14)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:32:444-32:470)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 16
+    dead: 0
+    total lines: 16
+