Fix NULL and unknown pointer handling in MayPointTo and ReachableFrom for race analysis

src/analyses/base.ml

@@ -1270,6 +1270,7 @@ struct
         match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | Address a -> a
         | Bot -> Queries.Result.bot q (* TODO: remove *)
+        | Int i -> AD.of_int i
         | _ -> Queries.Result.top q
       end
     | Q.EvalThread e -> begin
@@ -1287,7 +1288,17 @@ struct
         | Address a ->
           let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *)
           let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
-          List.fold_left (AD.join) (AD.empty ()) addrs
+          let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in
+          if AD.may_be_unknown a then
+            AD.add UnknownPtr addrs' (* add unknown back *)
+          else
+            addrs'
+        | Int i ->
+          begin match Cilfacade.typeOf e with
+            | t when Cil.isPointerType t -> AD.of_int i (* integer used as pointer *)
+            | _
+            | exception Cilfacade.TypeOfError _ -> AD.empty () (* avoid unknown pointer result for non-pointer expression *)
+          end
         | _ -> AD.empty ()
       end
     | Q.ReachableUkTypes e -> begin

tests/regression/05-lval_ls/20-race-null-void.c

@@ -0,0 +1,54 @@
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void **top;
+  free(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      pthread_join(id, NULL); // NORACE
+      break;
+    case 1:
+      pthread_join(id, 0); // NORACE
+      break;
+    case 2:
+      pthread_join(id, zero); // NORACE
+      break;
+    case 3:
+      pthread_join(id, 1); // RACE
+      break;
+    case 4:
+      pthread_join(id, one); // RACE
+      break;
+    case 5:
+      pthread_join(id, r); // RACE
+      break;
+    case 6:
+      pthread_join(id, null); // NORACE
+      break;
+    case 7:
+      pthread_join(id, unknown); // RACE
+      break;
+    case 8:
+      pthread_join(id, top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}

tests/regression/05-lval_ls/21-race-null-type.c

@@ -0,0 +1,55 @@
+// PARAM: --enable ana.race.direct-arithmetic
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void *top;
+  time(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      time(NULL); // NORACE
+      break;
+    case 1:
+      time(0); // NORACE
+      break;
+    case 2:
+      time(zero); // NORACE
+      break;
+    case 3:
+      time(1); // RACE
+      break;
+    case 4:
+      time(one); // RACE
+      break;
+    case 5:
+      time(r); // RACE
+      break;
+    case 6:
+      time(null); // NORACE
+      break;
+    case 7:
+      time(unknown); // RACE
+      break;
+    case 8:
+      time(top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}

tests/regression/05-lval_ls/22-race-null-void-deep.c

@@ -0,0 +1,56 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_key_t key;
+
+void *t_fun(void *arg) {
+  void *top;
+  pthread_setspecific(key, top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      pthread_setspecific(key, NULL); // NORACE
+      break;
+    case 1:
+      pthread_setspecific(key, 0); // NORACE
+      break;
+    case 2:
+      pthread_setspecific(key, zero); // NORACE
+      break;
+    case 3:
+      pthread_setspecific(key, 1); // RACE
+      break;
+    case 4:
+      pthread_setspecific(key, one); // RACE
+      break;
+    case 5:
+      pthread_setspecific(key, r); // RACE
+      break;
+    case 6:
+      pthread_setspecific(key, null); // NORACE
+      break;
+    case 7:
+      pthread_setspecific(key, unknown); // RACE
+      break;
+    case 8:
+      pthread_setspecific(key, top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}

tests/regression/05-lval_ls/23-race-null-type-deep.c

@@ -0,0 +1,54 @@
+#include <pthread.h>
+#include <stdio.h>
+
+void *t_fun(void *arg) {
+  void *top;
+  fclose(top); // RACE
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  int r; // rand
+  int zero = 0; // IntDomain zero
+  void *null;
+  __goblint_assume(null == NULL); // AddressDomain NULL
+  int one = 1; // IntDomain one
+  void *unknown;
+  __goblint_assume(unknown != NULL); // AddressDomain unknown
+  void *top;
+  switch (r) {
+    case 0:
+      feof(NULL); // NORACE
+      break;
+    case 1:
+      feof(0); // NORACE
+      break;
+    case 2:
+      feof(zero); // NORACE
+      break;
+    case 3:
+      feof(1); // RACE
+      break;
+    case 4:
+      feof(one); // RACE
+      break;
+    case 5:
+      feof(r); // RACE
+      break;
+    case 6:
+      feof(null); // NORACE
+      break;
+    case 7:
+      feof(unknown); // RACE
+      break;
+    case 8:
+      feof(top); // RACE
+      break;
+    default:
+      break;
+  }
+  return 0;
+}