Filter non-racing accesses of racing variable

src/domains/access.ml

@@ -333,8 +333,16 @@ struct
       let pretty = pretty
     end
     )
+
+  let conf (conf, _, _, _, _) = conf
+end
+module AS =
+struct
+  include SetDomain.Make (A)
+
+  let max_conf accs =
+    accs |> elements |> List.map A.conf |> List.max
 end
-module AS = SetDomain.Make (A)
 module T =
 struct
   include Printable.Std
@@ -377,28 +385,34 @@ module LVOpt = Printable.Option (LV) (struct let name = "NONE" end)
 (* Check if two accesses may race and if yes with which confidence *)
 let may_race (conf,w,loc,e,a) (conf2,w2,loc2,e2,a2) =
   if not w && not w2 then
-    None (* two read/read accesses do not race *)
+    false (* two read/read accesses do not race *)
   else if not (MCPAccess.A.may_race a a2) then
-    None (* analysis-specific information excludes race *)
+    false (* analysis-specific information excludes race *)
   else
-    Some (max conf conf2)
+    true
 
-let check_safe accs =
+let filter_may_race accs =
   let accs = AS.elements accs in
   let cart = List.cartesian_product accs accs in
-  let conf = List.filter_map (fun (x,y) -> if A.compare x y <= 0 then may_race x y else None) cart in
-  if conf = [] then
-    None
-  else
-    let maxconf = List.max conf in
-    Some maxconf
+  List.fold_left (fun acc (x, y) ->
+      if A.compare x y <= 0 && may_race x y then
+        AS.add y (AS.add x acc)
+      else
+        acc
+    ) (AS.empty ()) cart
 
 let is_all_safe = ref true
 
 (* Commenting your code is for the WEAK! *)
 let incr_summary safe vulnerable unsafe (lv, ty) accs =
   (* ignore(printf "Checking safety of %a:\n" d_memo (ty,lv)); *)
-  let safety = check_safe accs in
+  let race_accs = filter_may_race accs in
+  let safety =
+    if AS.is_empty race_accs then
+      None
+    else
+      Some (AS.max_conf race_accs)
+  in
   match safety with
   | None -> incr safe
   | Some n when n >= 100 -> is_all_safe := false; incr unsafe
@@ -407,7 +421,7 @@ let incr_summary safe vulnerable unsafe (lv, ty) accs =
 let print_accesses (lv, ty) accs =
   let allglobs = get_bool "allglobs" in
   let debug = get_bool "dbg.debug" in
-  let msgs () =
+  let msgs race_accs =
     let h (conf,w,loc,e,a) =
       let atyp = if w then "write" else "read" in
       let d_msg () = dprintf "%s with %a (conf. %d)" atyp MCPAccess.A.pretty a conf in
@@ -419,12 +433,13 @@ let print_accesses (lv, ty) accs =
       in
       (doc, Some loc)
     in
-    AS.elements accs
+    AS.elements race_accs
     |> List.map h
   in
-  match check_safe accs with
-  | None ->
+  match filter_may_race accs with
+  | race_accs when AS.is_empty race_accs ->
     if allglobs then
-      M.msg_group Success ~category:Race "Memory location %a (safe)" d_memo (ty,lv) (msgs ())
-  | Some n ->
-    M.msg_group Warning ~category:Race "Memory location %a (race with conf. %d)" d_memo (ty,lv) n (msgs ())
+      M.msg_group Success ~category:Race "Memory location %a (safe)" d_memo (ty,lv) (msgs accs)
+  | race_accs ->
+    let conf = AS.max_conf race_accs in
+    M.msg_group Warning ~category:Race "Memory location %a (race with conf. %d)" d_memo (ty,lv) conf (msgs (if allglobs then accs else race_accs))

tests/regression/04-mutex/27-base_rc.c

@@ -9,7 +9,7 @@ void bad() {
 }
 void good() {
   pthread_mutex_lock(&gm);
-  global++; // RACE
+  global++; // NORACE (MHP)
   pthread_mutex_unlock(&gm);
 }
 

tests/regression/04-mutex/35-trylock_rc.c

@@ -49,7 +49,7 @@ void *monitor_thread (void *arg) {
     if (status != EBUSY) {
       if (status != 0)
         err_abort (status, "Trylock mutex");
-      printf ("Counter is %ld\n", counter/SPIN); // RACE
+      printf ("Counter is %ld\n", counter/SPIN); // NORACE (MHP)
       status = pthread_mutex_unlock (&mutex);
       if (status != 0)
         err_abort (status, "Unlock mutex");

tests/regression/10-synch/12-join_rc.c

@@ -18,7 +18,7 @@ int main(void) {
   for (i=0; i<10; i++)
     pthread_create(&id[i], NULL, t_fun, NULL);
   pthread_mutex_lock(&mutex);
-  myglobal=myglobal+1; // RACE
+  myglobal=myglobal+1; // NORACE (MHP)
   pthread_mutex_unlock(&mutex);
   for (i=0; i<9; i++)
     pthread_join(id[i], NULL);

tests/regression/53-races-mhp/03-not-created_rc.c

@@ -0,0 +1,29 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+void *t_fun2(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
+  myglobal = 5; // NORACE
+
+  pthread_create(&id2, NULL, t_fun2, NULL);
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+  return 0;
+}