Remove thread

michael-schwarz · michael-schwarz · commit a84150722a08 · 2025-05-28T17:21:00.000+02:00
diff --git a/conf/race-digests/fresh-only.json b/conf/race-digests/fresh-only.json
@@ -56,7 +56,6 @@
       "call": false,
       "digests": {
         "lockset": false,
-        "thread": false,
         "fresh": true,
         "region": false,
         "symb_locks": false,
diff --git a/conf/race-digests/full-minus-region+symblocks.json b/conf/race-digests/full-minus-region+symblocks.json
@@ -56,7 +56,6 @@
       "call": false,
       "digests": {
         "lockset": true,
-        "thread": true,
         "fresh": true,
         "region": false,
         "symb_locks": false,
diff --git a/conf/race-digests/full-minus-region.json b/conf/race-digests/full-minus-region.json
@@ -56,7 +56,6 @@
       "call": false,
       "digests": {
         "lockset": true,
-        "thread": true,
         "fresh": true,
         "region": false,
         "symb_locks": true,
diff --git a/conf/race-digests/mutex+threadflag.json b/conf/race-digests/mutex+threadflag.json
@@ -56,8 +56,7 @@
       "call": false,
       "digests": {
         "lockset": true,
-        "thread": false,
-        "fresh": false,
+
         "region": false,
         "symb_locks": false,
         "threadflag": true,
diff --git a/conf/race-digests/mutex-only.json b/conf/race-digests/mutex-only.json
@@ -56,7 +56,6 @@
       "call": false,
       "digests": {
         "lockset": true,
-        "thread": false,
         "fresh": false,
         "region": false,
         "symb_locks": false,
diff --git a/conf/race-digests/none.json b/conf/race-digests/none.json
@@ -56,7 +56,6 @@
       "call": false,
       "digests": {
         "lockset": false,
-        "thread": false,
         "fresh": false,
         "region": false,
         "symb_locks": false,
diff --git a/conf/race-digests/region-only.json b/conf/race-digests/region-only.json
@@ -56,7 +56,7 @@
       "call": false,
       "digests": {
         "lockset": false,
-        "thread": false,
+
         "fresh": false,
         "region": true,
         "symb_locks": false,
diff --git a/conf/race-digests/symblocks-only.json b/conf/race-digests/symblocks-only.json
@@ -56,7 +56,7 @@
       "call": false,
       "digests": {
         "lockset": false,
-        "thread": false,
+
         "fresh": false,
         "region": false,
         "symb_locks": true,
diff --git a/conf/race-digests/tf+thread.json b/conf/race-digests/tf+thread.json
diff --git a/conf/race-digests/tf-only.json b/conf/race-digests/tf-only.json
@@ -56,7 +56,7 @@
       "call": false,
       "digests": {
         "lockset": false,
-        "thread": false,
+
         "fresh": false,
         "region": false,
         "symb_locks": false,
diff --git a/conf/race-digests/tid+mutex+join.json b/conf/race-digests/tid+mutex+join.json
@@ -56,7 +56,7 @@
       "call": false,
       "digests": {
         "lockset": true,
-        "thread": false,
+
         "fresh": false,
         "region": false,
         "symb_locks": false,
diff --git a/conf/race-digests/tid+mutex.json b/conf/race-digests/tid+mutex.json
@@ -56,7 +56,7 @@
       "call": false,
       "digests": {
         "lockset": true,
-        "thread": false,
+
         "fresh": false,
         "region": false,
         "symb_locks": false,
diff --git a/conf/race-digests/tid+thread.json b/conf/race-digests/tid+thread.json
diff --git a/conf/race-digests/tid-only.json b/conf/race-digests/tid-only.json
@@ -56,7 +56,7 @@
       "call": false,
       "digests": {
         "lockset": false,
-        "thread": false,
+
         "fresh": false,
         "region": false,
         "symb_locks": false,
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
@@ -54,15 +54,30 @@ struct
 
   module A =
   struct
-    include BoolDomain.Bool
-    let name () = "multi"
-    let may_race m1 m2 =
+    include Lattice.Prod(Flag)(BoolDomain.MayBool)
+    let name () = "threadflag"
+
+    let may_race (m1,b1) (m2,b2) =
       let use_threadflag = GobConfig.get_bool "ana.race.digests.threadflag" in
-      (not use_threadflag) || (m1 && m2) (* kill access when single threaded *)
-    let should_print m = not m
+      let both_mt = Flag.is_multi m1 && Flag.is_multi m2 in
+      let one_not_main = Flag.is_not_main m1 || Flag.is_not_main m2 in
+      ((not use_threadflag) || (both_mt && one_not_main)) && b1 && b2
+
+      (* kill access when single threaded *)
+
+    let should_print m = true
   end
+
   let access man _ =
-    is_currently_multi (Analyses.ask_of_man man)
+    let st =
+      if GobConfig.get_bool "ana.race.digests.join" then
+        is_currently_multi (Analyses.ask_of_man man)
+      else if GobConfig.get_bool "ana.race.digests.tid" then
+        has_ever_been_multi (Analyses.ask_of_man man)
+      else
+        true
+    in
+    ((man.local,st):A.t)
 
   let threadenter man ~multiple lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_man man)) then
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
