Exclude multithreaded main-main races by threadflag

goblint · Oct 2, 2024 · 30e5ef1 · 30e5ef1
1 parent 0713e84
commit 30e5ef1
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 8 deletions.
diff --git a/src/analyses/threadFlag.ml b/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

diff --git a/tests/regression/13-privatized/63-access-threadspawn-lval.t b/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, f@63-access-threadspawn-lval.c: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, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)

diff --git a/tests/regression/13-privatized/64-access-invalidate.t b/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