Exclude multithreaded main-main races by threadflag

src/analyses/threadFlag.ml

@@ -54,13 +54,15 @@ struct
 
   module A =
   struct
-    include BoolDomain.Bool
-    let name () = "multi"
-    let may_race m1 m2 = m1 && m2 (* kill access when single threaded *)
-    let should_print m = not m
+    include Flag
+    let name () = "flag"
+    let may_race f1 f2 =
+      (* TODO: no longer accounts for MustBeSingleThreaded from other analyses via is_currently_multi *)
+      Flag.is_multi f1 && Flag.is_multi f2 && (* both must be multi-threaded *)
+      (Flag.is_not_main f1 || Flag.is_not_main f2) (* at least one must be non-main *)
+    let should_print f = not (Flag.is_multi f)
   end
-  let access ctx _ =
-    is_currently_multi (Analyses.ask_of_ctx ctx)
+  let access ctx _ = ctx.local
 
   let threadenter ctx ~multiple lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then

tests/regression/10-synch/29-threadflag-main.c

@@ -0,0 +1,18 @@
+// PARAM: --set ana.activated[-] threadid
+// Deactivate threadid to rely on threadflag only.
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  myglobal=myglobal+1; // NORACE
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/13-privatized/63-access-threadspawn-lval.t

@@ -12,7 +12,7 @@ Should have (safe) write accesses to id1 and id2:
     dead: 0
     total lines: 13
   [Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14)
-    write with [multi:false, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
+    write with [flag:Singlethreaded, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
   [Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14)
     write with [mhp:{created={[main, [email protected]:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: (pthread_t * __restrict  )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37)
     write with [mhp:{created={[main, [email protected]:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)

tests/regression/13-privatized/64-access-invalidate.t

@@ -12,7 +12,7 @@ Should have (safe) write access to id1 and magic2 invalidate to A:
     dead: 0
     total lines: 10
   [Success][Race] Memory location id (safe): (64-access-invalidate.c:4:11-4:13)
-    write with [multi:false, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id))) (64-access-invalidate.c:21:3-21:36)
+    write with [flag:Singlethreaded, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id))) (64-access-invalidate.c:21:3-21:36)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0