Use MHP information

src/analyses/pthreadBarriers.ml

@@ -22,7 +22,7 @@ struct
   module V = VarinfoV
 
   module TID = ThreadIdDomain.Thread
-  module Waiters = SetDomain.ToppedSet (TID) (struct let topname = "All MHP" end)
+  module Waiters = SetDomain.ToppedSet (MHP) (struct let topname = "All MHP" end)
   module G = Lattice.Prod (Capacity) (Waiters)
 
   let name () = "pthreadBarriers"
@@ -40,17 +40,14 @@ struct
       let ask = Analyses.ask_of_man man in
       let may, must = man.local in
       let barriers = possible_vinfos ask barrier in
-      let tid = match ThreadId.get_current ask with
-        | `Lifted tid -> Waiters.singleton tid
-        | _ -> Waiters.top ()
-      in
+      let mhp = MHP.current ask in
       let handle_one b =
-        man.sideg b (Capacity.bot (), tid);
+        man.sideg b (Capacity.bot (), Waiters.singleton mhp);
         let addr = ValueDomain.Addr.of_var b in
         let (capacity, waiters) = man.global b in
-        let relevant_waiters = Waiters.filter (fun tid -> true) waiters in
+        let relevant_waiters = Waiters.filter (fun other -> MHP.may_happen_in_parallel mhp other) waiters in
         let may_run =
-          if Waiters.exists (fun tid -> not @@ TID.is_unique tid) relevant_waiters then
+          if Waiters.exists MHP.may_be_non_unique_thread relevant_waiters then
             true
           else
             let count = Waiters.cardinal relevant_waiters in

src/cdomains/mHP.ml

@@ -92,3 +92,8 @@ let may_happen_in_parallel one two =
     else
       true
   | _ -> true
+
+let may_be_non_unique_thread mhp =
+  match mhp.tid with
+  | `Lifted tid -> not (TID.is_unique tid)
+  | _ -> true

tests/regression/82-barrier/02-more.c

@@ -8,12 +8,14 @@ int g;
 pthread_barrier_t barrier;
 
 void* f2(void* ptr) {
+    pthread_barrier_wait(&barrier);
     return NULL;
 }
 
 void* f1(void* ptr) {
     pthread_barrier_wait(&barrier);
 
+    // This is past the barrier, so it will not be reached
     pthread_t t2;
     pthread_create(&t2,NULL,f2,NULL);
 
@@ -26,18 +28,22 @@ int main(int argc, char const *argv[])
     int i = 0;
 
     pthread_barrier_init(&barrier, NULL, 3);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
 
     if(top) {
         pthread_barrier_wait(&barrier);
         // Unreachable
         i = 1;
     }
 
-    __goblint_check(i == 0);
-    pthread_t t1;
+    // Created too late to have any effect
+    pthread_t t2;
+    pthread_create(&t2,NULL,f1,NULL);
 
+    __goblint_check(i == 0);
 
-    pthread_create(&t1,NULL,f1,NULL);
 
     return 0;
 }