Merge pull request #1607 from goblint/pthread_self

Add `pthread_self` support

src/analyses/base.ml

@@ -2651,6 +2651,15 @@ struct
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd args in
       Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st
+    | ThreadSelf, _ ->
+      begin match lv, ThreadId.get_current (Analyses.ask_of_ctx ctx) with
+        | Some lv, `Lifted tid ->
+          set ~ctx st (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid))
+        | Some lv, _ ->
+          invalidate_ret_lv st
+        | None, _ ->
+          st
+      end
     | Alloca size, _ -> begin
         match lv with
         | Some lv ->

src/cdomain/value/cdomains/threadIdDomain.ml

@@ -83,10 +83,10 @@ struct
       (v, None)
 
   let is_main = function
-    | ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun"
+    | ({vname; _}, None) -> GobConfig.get_bool "ana.thread.include-node" && List.mem vname @@ GobConfig.get_string_list "mainfun"
     | _ -> false
 
-  let is_unique _ = false (* TODO: should this consider main unique? *)
+  let is_unique = is_main
   let may_create _ _ = true
   let is_must_parent _ _ = false
 end

src/util/library/libraryDesc.ml

@@ -56,6 +56,7 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
+  | ThreadSelf
   | Globalize of Cil.exp
   | Signal of Cil.exp
   | Broadcast of Cil.exp

src/util/library/libraryFunctions.ml

@@ -504,7 +504,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_attr_setstacksize", unknown [drop "attr" [w]; drop "stacksize" []]);
     ("pthread_attr_getscope", unknown [drop "attr" [r]; drop "scope" [w]]);
     ("pthread_attr_setscope", unknown [drop "attr" [w]; drop "scope" []]);
-    ("pthread_self", unknown []);
+    ("pthread_self", special [] ThreadSelf);
     ("pthread_sigmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]);
     ("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]);
     ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);

tests/regression/51-threadjoins/09-join-main.c

@@ -0,0 +1,29 @@
+//PARAM: --set ana.activated[+] threadJoins
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_t mainid;
+
+int g = 10;
+
+void *t_fun(void *arg) {
+  int r = pthread_join(mainid, NULL); // TSan doesn't like this...
+  printf("j: %d\n", r);
+  g++; // NORACE
+  printf("t_fun: %d\n", g);
+  return NULL;
+}
+
+
+int main(void) {
+  mainid = pthread_self();
+
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+
+  g++; // NORACE
+  printf("main: %d\n", g);
+
+  pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2
+  return 0;
+}

tests/regression/51-threadjoins/10-join-main-plain.c

@@ -0,0 +1,29 @@
+//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_t mainid;
+
+int g = 10;
+
+void *t_fun(void *arg) {
+  int r = pthread_join(mainid, NULL); // TSan doesn't like this...
+  printf("j: %d\n", r);
+  g++; // RACE (imprecise by plain thread IDs)
+  printf("t_fun: %d\n", g);
+  return NULL;
+}
+
+
+int main(void) {
+  mainid = pthread_self();
+
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+
+  g++; // NORACE
+  printf("main: %d\n", g);
+
+  pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2
+  return 0;
+}

tests/regression/51-threadjoins/11-join-main-plain-no-node.c

@@ -0,0 +1,29 @@
+//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain --disable ana.thread.include-node
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_t mainid;
+
+int g = 10;
+
+void *t_fun(void *arg) {
+  int r = pthread_join(mainid, NULL); // TSan doesn't like this...
+  printf("j: %d\n", r);
+  g++; // RACE (imprecise by plain thread IDs)
+  printf("t_fun: %d\n", g);
+  return NULL;
+}
+
+
+int main(void) {
+  mainid = pthread_self();
+
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+
+  g++; // RACE (imprecise by plain thread IDs not knowing if main is actual main or spawned by program)
+  printf("main: %d\n", g);
+
+  pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2
+  return 0;
+}