Merge pull request #1617 from goblint/issue_1615

Fix `thread` for non-unique spawns

Author: michael-schwarz

src/analyses/threadAnalysis.ml

@@ -95,9 +95,7 @@ struct
   let startstate v = D.bot ()
 
   let threadenter ctx ~multiple lval f args =
-    if multiple then
-      (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
-       ctx.sideg tid (true, TS.bot (), false));
+    (* ctx is of creator, side-effects to denote non-uniqueness are performed in threadspawn *)
     [D.bot ()]
 
   let threadspawn ctx ~multiple lval f args fctx =
@@ -106,9 +104,9 @@ struct
     let repeated = D.mem tid ctx.local in
     let eff =
       match creator with
-      | `Lifted ctid -> (repeated, TS.singleton ctid, false)
-      | `Top         -> (true,     TS.bot (),         false)
-      | `Bot         -> (false,    TS.bot (),         false)
+      | `Lifted ctid -> (repeated || multiple, TS.singleton ctid, false)
+      | `Top         -> (true, TS.bot (), false)
+      | `Bot         -> (multiple, TS.bot (), false)
     in
     ctx.sideg tid eff;
     D.join ctx.local (D.singleton tid)

tests/regression/10-synch/29-multiple-created-only.c

@@ -0,0 +1,26 @@
+// PARAM: --set ana.activated[+] thread --set ana.activated[+] threadid --set ana.thread.domain plain
+
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+int myglobal2;
+
+void* bla(void *arg) {
+  // This is created multiple times, it should race with itself
+  myglobal = 10; //RACE
+  return NULL;
+}
+
+void* other(void) {
+  // This is created only once, it should not be marked as non-unique
+  unknown(bla);
+  myglobal2 = 30; //NORACE
+}
+
+int main(void) {
+    pthread_t id;
+    pthread_create(&id, NULL, other, NULL);
+
+    return 0;
+}

tests/regression/10-synch/30-no-crash.c

@@ -0,0 +1,31 @@
+// PARAM: --set ana.context.gas_value 0 --set ana.activated[+] thread --set ana.activated[+] threadid
+
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+int myglobal2;
+
+void *t_flurb(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+void* bla(void *arg) {
+    return NULL;
+}
+
+void *t_fun(void *arg) {
+  unknown(t_flurb); // NOCRASH
+  return NULL;
+}
+
+int main(void) {
+    pthread_t id;
+    pthread_create(&id, NULL, t_fun, NULL);
+    pthread_create(&id, NULL, t_fun, NULL);
+
+    unknown(bla);
+
+    return 0;
+}