Ability to enable/disable may_race checks per race diges

src/analyses/mallocFresh.ml

@@ -64,7 +64,9 @@ struct
   struct
     include BoolDomain.Bool
     let name () = "fresh"
-    let may_race f1 f2 = not (f1 || f2)
+    let may_race f1 f2 =
+      let use_fresh = GobConfig.get_bool "ana.race.digests.fresh" in
+      (not use_fresh) || not (f1 || f2)
     let should_print f = f
   end
   let access man (a: Queries.access) =

src/analyses/mutexAnalysis.ml

@@ -267,6 +267,8 @@ struct
     include MustLocksetRW
     let name () = "lock"
     let may_race ls1 ls2 =
+      let use_lockset = GobConfig.get_bool "ana.race.digests.lockset" in
+      (not use_lockset) ||
       (* not mutually exclusive *)
       not @@ exists (fun ((m1, w1) as l1) ->
           if w1 then

src/analyses/region.ml

@@ -64,7 +64,10 @@ struct
   struct
     include Printable.Option (Lvals) (struct let name = "no region" end)
     let name () = "region"
-    let may_race r1 r2 = match r1, r2 with
+    let may_race r1 r2 =
+      let use_region = GobConfig.get_bool "ana.race.digests.region" in
+      (not use_region) ||
+      match r1, r2 with
       | None, _
       | _, None -> false
       (* TODO: Should it happen in the first place that RegMap has empty value? Happens in 09-regions/34-escape_rc *)

src/analyses/symbLocks.ml

@@ -121,7 +121,9 @@ struct
     include SetDomain.Make (E)
 
     let name () = "symblock"
-    let may_race lp lp2 = disjoint lp lp2
+    let may_race lp lp2 =
+      let use_symblocks = GobConfig.get_bool "ana.race.digests.symb_locks" in
+      (not use_symblocks) || disjoint lp lp2
     let should_print lp = not (is_empty lp)
   end
 

src/analyses/threadFlag.ml

@@ -56,7 +56,9 @@ struct
   struct
     include BoolDomain.Bool
     let name () = "multi"
-    let may_race m1 m2 = m1 && m2 (* kill access when single threaded *)
+    let may_race m1 m2 =
+      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
   end
   let access man _ =

src/analyses/threadId.ml

@@ -132,7 +132,10 @@ struct
   struct
     include Printable.Option (ThreadLifted) (struct let name = "nonunique" end)
     let name () = "thread"
-    let may_race (t1: t) (t2: t) = match t1, t2 with
+    let may_race (t1: t) (t2: t) =
+      let use_tid = GobConfig.get_bool "ana.race.digests.thread" in
+      (not use_tid) ||
+      match t1, t2 with
       | Some t1, Some t2 when ThreadLifted.equal t1 t2 -> false (* only unique threads *)
       | _, _ -> true
     let should_print = Option.is_some

src/cdomains/mHP.ml

@@ -77,17 +77,19 @@ let must_be_joined other joined =
 
 (** May two program points with respective MHP information happen in parallel *)
 let may_happen_in_parallel one two =
-  let {tid=tid; created=created; must_joined=must_joined} = one in
+  let use_tid = GobConfig.get_bool "ana.race.digests.tid" in
+  let use_join = GobConfig.get_bool "ana.race.digests.join" in
+  let {tid; created; must_joined} = one in
   let {tid=tid2; created=created2; must_joined=must_joined2} = two in
   match tid,tid2 with
   | `Lifted tid, `Lifted tid2 ->
-    if (TID.is_unique tid) && (TID.equal tid tid2) then
+    if use_tid && (TID.is_unique tid) && (TID.equal tid tid2) then
       false
-    else if definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid then
+    else if use_tid && (definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid) then
       false
-    else if must_be_joined tid2 must_joined || must_be_joined tid must_joined2 then
+    else if use_tid && use_join && (must_be_joined tid2 must_joined || must_be_joined tid must_joined2) then
       false
-    else if exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined then
+    else if use_tid && use_join && (exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined) then
       false
     else
       true

src/config/options.schema.json

@@ -1105,6 +1105,61 @@
               "description": "Report races for volatile variables.",
               "type": "boolean",
               "default": true
+            },
+            "digests": {
+              "title": "ana.race.digests",
+              "type" : "object",
+              "properties" : {
+                "lockset" : {
+                  "title": "ana.race.digests.lockset",
+                  "description": "Use lockset digest for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "thread" : {
+                  "title": "ana.race.digests.thread",
+                  "description": "TODO! How does relate to the MHP one? Seems to hit only in one case",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "fresh" : {
+                  "title": "ana.race.digests.fresh",
+                  "description": "Use freshness analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "region" : {
+                  "title": "ana.race.digests.region",
+                  "description": "Use region analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "symb_locks" : {
+                  "title": "ana.race.digests.symb_locks",
+                  "description": "Use symb_locks analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "threadflag" : {
+                  "title": "ana.race.digests.threadflag",
+                  "description": "Use threadflag analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "tid" : {
+                  "title": "ana.race.digests.tid",
+                  "description": "Use tid analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "join" : {
+                  "title": "ana.race.digests.join",
+                  "description": "Use join analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false