From 2fb5390dc0085864da2f1b426e1b5ba2cd97b800 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 24 Dec 2024 18:41:47 +0100
Subject: [PATCH 01/38] First steps

---
 src/analyses/pthreadBarriers.ml         | 43 +++++++++++++++++++++++++
 src/util/library/libraryDesc.ml         |  2 ++
 src/util/library/libraryFunctions.ml    |  2 ++
 tests/regression/82-barrier/01-simple.c | 34 +++++++++++++++++++
 4 files changed, 81 insertions(+)
 create mode 100644 src/analyses/pthreadBarriers.ml
 create mode 100644 tests/regression/82-barrier/01-simple.c

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
new file mode 100644
index 0000000000..c414175dc6
--- /dev/null
+++ b/src/analyses/pthreadBarriers.ml
@@ -0,0 +1,43 @@
+(** Must have waited barriers for Pthread barriers ([pthreadBarriers]). *)
+
+open GoblintCil
+open Analyses
+module LF = LibraryFunctions
+
+module Spec =
+struct
+  module Barriers = SetDomain.ToppedSet (ValueDomain.Addr) (struct let topname = "All barriers" end)
+  module MustBarriers = Lattice.Reverse (Barriers)
+
+  include Analyses.IdentitySpec
+  module V = VarinfoV
+
+  let name () = "pthreadBarriers"
+  module D = Lattice.Prod (Barriers) (MustBarriers)
+
+  include Analyses.ValueContexts(D)
+
+  let possible_vinfos (a: Queries.ask) barrier =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
+
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let desc = LF.find f in
+    match desc.special arglist with
+    | BarrierWait barrier ->
+      let may, must = man.local in
+      let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in
+      let may = List.fold_left (fun may a -> Barriers.add (ValueDomain.Addr.of_var a) may) may barriers in
+      let must = match barriers with
+      | [a] -> Barriers.add (ValueDomain.Addr.of_var a) must
+      | _ -> must
+      in
+      (may, must)
+    | _ -> man.local
+
+  let startstate v = (Barriers.empty (), Barriers.empty ())
+  let threadenter man ~multiple lval f args = [man.local]
+  let exitstate  v = (Barriers.empty (), Barriers.empty ())
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
index 6f34de1864..2da79dcc20 100644
--- a/src/util/library/libraryDesc.ml
+++ b/src/util/library/libraryDesc.ml
@@ -69,6 +69,8 @@ type special =
   | SemDestroy of Cil.exp
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
+  | BarrierWait of Cil.exp
+  | BarrierInit of { barrier: Cil.exp; count: Cil.exp; }
   | Math of { fun_args: math; }
   | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
   | Bzero of { dest: Cil.exp; count: Cil.exp; }
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 6643b58eef..ab7d682483 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -520,6 +520,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
     ("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]);
     ("pthread_key_delete", unknown [drop "key" [f]]);
+    ("pthread_barrier_init", special [__ "barrier" []; __ "attr" []; __ "count" []] @@ fun barrier attr count -> BarrierInit {barrier; count});
+    ("pthread_barrier_wait", special [__ "barrier" []] @@ fun barrier -> BarrierWait barrier);
     ("pthread_cancel", unknown [drop "thread" []]);
     ("pthread_testcancel", unknown []);
     ("pthread_setcancelstate", unknown [drop "state" []; drop "oldstate" [w]]);
diff --git a/tests/regression/82-barrier/01-simple.c b/tests/regression/82-barrier/01-simple.c
new file mode 100644
index 0000000000..69307e252f
--- /dev/null
+++ b/tests/regression/82-barrier/01-simple.c
@@ -0,0 +1,34 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+void* f1(void* ptr) {
+    return NULL;
+}
+
+void* f2(void* ptr) {
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    pthread_barrier_init(&barrier, NULL, 2);
+    pthread_barrier_wait(&barrier);
+    
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    sleep(1);
+    pthread_create(&t2,NULL,f2,NULL);
+
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+
+    return 0;
+}

From 29a39005efa967d9f5c214ac72db3eb02ffe67a5 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 24 Dec 2024 18:56:39 +0100
Subject: [PATCH 02/38] Record capacity

---
 src/analyses/pthreadBarriers.ml | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index c414175dc6..ad5759c458 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -6,12 +6,22 @@ module LF = LibraryFunctions
 
 module Spec =
 struct
-  module Barriers = SetDomain.ToppedSet (ValueDomain.Addr) (struct let topname = "All barriers" end)
-  module MustBarriers = Lattice.Reverse (Barriers)
+  module Barriers = struct
+    include SetDomain.ToppedSet (ValueDomain.Addr) (struct let topname = "All barriers" end)
+    let name () = "mayBarriers"
+  end
+
+  module MustBarriers = struct
+    include Lattice.Reverse (Barriers)
+    let name () = "mustBarriers" 
+  end
 
   include Analyses.IdentitySpec
   module V = VarinfoV
 
+  module Waiters = SetDomain.ToppedSet (MHP) (struct let topname = "All MHP" end)
+  module G = Lattice.Prod (Queries.ID) (Waiters)
+
   let name () = "pthreadBarriers"
   module D = Lattice.Prod (Barriers) (MustBarriers)
 
@@ -32,6 +42,12 @@ struct
       | _ -> must
       in
       (may, must)
+    | BarrierInit { barrier; count } ->
+      let count = man.ask (Queries.EvalInt count) in
+      let publish_one b = man.sideg b (count, Waiters.bot ()) in 
+      let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in
+      List.iter publish_one barriers;
+      man.local
     | _ -> man.local
 
   let startstate v = (Barriers.empty (), Barriers.empty ())

From 60c1d72fff598c29f06fd99e1b38e27e3098da1e Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 24 Dec 2024 19:41:24 +0100
Subject: [PATCH 03/38] Add first checks

---
 src/analyses/pthreadBarriers.ml         | 39 ++++++++++++++++++----
 tests/regression/82-barrier/01-simple.c | 26 ++++++---------
 tests/regression/82-barrier/02-more.c   | 43 +++++++++++++++++++++++++
 3 files changed, 84 insertions(+), 24 deletions(-)
 create mode 100644 tests/regression/82-barrier/02-more.c

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index ad5759c458..93f6638fd1 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -16,11 +16,14 @@ struct
     let name () = "mustBarriers" 
   end
 
+  module Capacity = Queries.ID
+
   include Analyses.IdentitySpec
   module V = VarinfoV
 
-  module Waiters = SetDomain.ToppedSet (MHP) (struct let topname = "All MHP" end)
-  module G = Lattice.Prod (Queries.ID) (Waiters)
+  module TID = ThreadIdDomain.Thread
+  module Waiters = SetDomain.ToppedSet (TID) (struct let topname = "All MHP" end)
+  module G = Lattice.Prod (Capacity) (Waiters)
 
   let name () = "pthreadBarriers"
   module D = Lattice.Prod (Barriers) (MustBarriers)
@@ -34,13 +37,35 @@ struct
     let desc = LF.find f in
     match desc.special arglist with
     | BarrierWait barrier ->
+      let ask = Analyses.ask_of_man man in
       let may, must = man.local in
-      let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in
-      let may = List.fold_left (fun may a -> Barriers.add (ValueDomain.Addr.of_var a) may) may barriers in
-      let must = match barriers with
-      | [a] -> Barriers.add (ValueDomain.Addr.of_var a) must
-      | _ -> must
+      let barriers = possible_vinfos ask barrier in
+      let tid = match ThreadId.get_current ask with
+        | `Lifted tid -> Waiters.singleton tid
+        | _ -> Waiters.top ()
+      in
+      let handle_one b =
+        man.sideg b (Capacity.bot (), tid);
+        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 may_run =
+          if Waiters.exists (fun tid -> not @@ TID.is_unique tid) relevant_waiters then
+            true
+          else
+            let count = Waiters.cardinal relevant_waiters in
+            match capacity with
+            | `Lifted c -> 
+              Z.geq (Z.of_int count) (BatOption.default Z.zero (Capacity.I.minimal c)) 
+            | _ -> true
+        in
+        if may_run then
+          (Barriers.add addr may, Barriers.add addr must)
+        else
+          D.bot ()
       in
+      let (may, must) = List.fold_left (fun acc b-> D.join acc (handle_one b)) (D.bot ()) barriers in
+      if Barriers.is_empty may then raise Analyses.Deadcode;
       (may, must)
     | BarrierInit { barrier; count } ->
       let count = man.ask (Queries.EvalInt count) in
diff --git a/tests/regression/82-barrier/01-simple.c b/tests/regression/82-barrier/01-simple.c
index 69307e252f..696e433962 100644
--- a/tests/regression/82-barrier/01-simple.c
+++ b/tests/regression/82-barrier/01-simple.c
@@ -7,28 +7,20 @@ int g;
 
 pthread_barrier_t barrier;
 
-void* f1(void* ptr) {
-    return NULL;
-}
-
-void* f2(void* ptr) {
-    return NULL;
-}
 
 int main(int argc, char const *argv[])
 {
+    int top;
+    int i = 0;
+    
     pthread_barrier_init(&barrier, NULL, 2);
-    pthread_barrier_wait(&barrier);
     
-    pthread_t t1;
-    pthread_t t2;
-
-    pthread_create(&t1,NULL,f1,NULL);
-    sleep(1);
-    pthread_create(&t2,NULL,f2,NULL);
-
-    pthread_join(t1, NULL);
-    pthread_join(t2, NULL);
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    }
 
+    __goblint_check(i == 0);
     return 0;
 }
diff --git a/tests/regression/82-barrier/02-more.c b/tests/regression/82-barrier/02-more.c
new file mode 100644
index 0000000000..9ff084be11
--- /dev/null
+++ b/tests/regression/82-barrier/02-more.c
@@ -0,0 +1,43 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+void* f2(void* ptr) {
+    return NULL;
+}
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    pthread_t t2;
+    pthread_create(&t2,NULL,f2,NULL);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 3);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    }
+
+    __goblint_check(i == 0);
+    pthread_t t1;
+
+
+    pthread_create(&t1,NULL,f1,NULL);
+
+    return 0;
+}

From 041e544c39fbbdcb027cd698fa938f0cba07fc52 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 24 Dec 2024 20:04:16 +0100
Subject: [PATCH 04/38] Use MHP information

---
 src/analyses/pthreadBarriers.ml       | 13 +++++--------
 src/cdomains/mHP.ml                   |  5 +++++
 tests/regression/82-barrier/02-more.c | 12 +++++++++---
 3 files changed, 19 insertions(+), 11 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 93f6638fd1..03d3620f5c 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/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
diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index 433486d4e0..13bf81819b 100644
--- a/src/cdomains/mHP.ml
+++ b/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
\ No newline at end of file
diff --git a/tests/regression/82-barrier/02-more.c b/tests/regression/82-barrier/02-more.c
index 9ff084be11..2b50b3ad06 100644
--- a/tests/regression/82-barrier/02-more.c
+++ b/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,6 +28,9 @@ 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);
@@ -33,11 +38,12 @@ int main(int argc, char const *argv[])
         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;
 }

From db320aed96ce7e7d413a2171e0f1e172953b98dd Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 24 Dec 2024 21:32:46 +0100
Subject: [PATCH 05/38] More involved MHP check

---
 src/analyses/pthreadBarriers.ml               | 21 +++++++-
 tests/regression/82-barrier/02-more.c         |  4 --
 tests/regression/82-barrier/03-problem.c      | 36 ++++++++++++++
 tests/regression/82-barrier/04-challenge.c    | 49 +++++++++++++++++++
 .../regression/82-barrier/05-mhp-not-enough.c | 45 +++++++++++++++++
 5 files changed, 150 insertions(+), 5 deletions(-)
 create mode 100644 tests/regression/82-barrier/03-problem.c
 create mode 100644 tests/regression/82-barrier/04-challenge.c
 create mode 100644 tests/regression/82-barrier/05-mhp-not-enough.c

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 03d3620f5c..a02c3332f4 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -53,7 +53,26 @@ struct
             let count = Waiters.cardinal relevant_waiters in
             match capacity with
             | `Lifted c -> 
-              Z.geq (Z.of_int count) (BatOption.default Z.zero (Capacity.I.minimal c)) 
+              (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
+              let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
+              if Z.leq min_cap Z.one then
+                true
+              else if min_cap = Z.of_int 2 && count = 1 then
+                true
+              else if Z.geq (Z.of_int (count + 1)) min_cap then
+                (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
+                  MHP is pairwise true? This solution is a sledgehammer, there should be something much
+                  better algorithmically (beyond just laziness) *)
+                let waiters = Waiters.elements relevant_waiters in
+                let min_cap = Z.to_int min_cap in
+                let lists = List.init (min_cap - 1) (fun _ -> waiters) in
+                let candidates = BatList.n_cartesian_product lists in
+                List.exists (fun candidate ->
+                  let pairwise = BatList.cartesian_product candidate candidate in
+                  List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise
+                ) candidates
+              else
+                false
             | _ -> true
         in
         if may_run then
diff --git a/tests/regression/82-barrier/02-more.c b/tests/regression/82-barrier/02-more.c
index 2b50b3ad06..cdabe740ea 100644
--- a/tests/regression/82-barrier/02-more.c
+++ b/tests/regression/82-barrier/02-more.c
@@ -38,10 +38,6 @@ int main(int argc, char const *argv[])
         i = 1;
     }
 
-    // Created too late to have any effect
-    pthread_t t2;
-    pthread_create(&t2,NULL,f1,NULL);
-
     __goblint_check(i == 0);
 
 
diff --git a/tests/regression/82-barrier/03-problem.c b/tests/regression/82-barrier/03-problem.c
new file mode 100644
index 0000000000..d75245ccdd
--- /dev/null
+++ b/tests/regression/82-barrier/03-problem.c
@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Live!
+        i = 1;
+    }
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/04-challenge.c b/tests/regression/82-barrier/04-challenge.c
new file mode 100644
index 0000000000..2b50b3ad06
--- /dev/null
+++ b/tests/regression/82-barrier/04-challenge.c
@@ -0,0 +1,49 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+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);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    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;
+    }
+
+    // Created too late to have any effect
+    pthread_t t2;
+    pthread_create(&t2,NULL,f1,NULL);
+
+    __goblint_check(i == 0);
+
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/05-mhp-not-enough.c b/tests/regression/82-barrier/05-mhp-not-enough.c
new file mode 100644
index 0000000000..4fcb460d61
--- /dev/null
+++ b/tests/regression/82-barrier/05-mhp-not-enough.c
@@ -0,0 +1,45 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    // This should not be reached as either main calls wait or the other thread is created
+    // -> In the concrete, there never are three threads calling wait
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int top2;
+    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;
+    } else {
+        pthread_t t2;
+        pthread_create(&t2,NULL,f1,NULL);    
+    }
+
+
+    __goblint_check(i == 0);
+
+
+    return 0;
+}

From 8b2ede3fe3d21e6c6ad84ffb6575b021215764dd Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 24 Dec 2024 21:33:29 +0100
Subject: [PATCH 06/38] Rm spurious variable

---
 tests/regression/82-barrier/05-mhp-not-enough.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/regression/82-barrier/05-mhp-not-enough.c b/tests/regression/82-barrier/05-mhp-not-enough.c
index 4fcb460d61..c627a4ff04 100644
--- a/tests/regression/82-barrier/05-mhp-not-enough.c
+++ b/tests/regression/82-barrier/05-mhp-not-enough.c
@@ -20,7 +20,6 @@ void* f1(void* ptr) {
 int main(int argc, char const *argv[])
 {
     int top;
-    int top2;
     int i = 0;
     
     pthread_barrier_init(&barrier, NULL, 3);

From f418b00dc200772d4fa0e16ead0e181602792afd Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 24 Dec 2024 21:35:11 +0100
Subject: [PATCH 07/38] Document pthread barriers

---
 src/goblint_lib.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 415fb21605..b63d804a2f 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -129,6 +129,7 @@ module BasePriv = BasePriv
 module RelationPriv = RelationPriv
 module ThreadEscape = ThreadEscape
 module PthreadSignals = PthreadSignals
+module PthreadBarriers = PthreadBarriers
 module ExtractPthread = ExtractPthread
 
 (** {2 Longjmp}

From 93b7f0c766d00919cba7cba8be0ce63c8e5572d7 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 16:00:13 +0100
Subject: [PATCH 08/38] Add `NOMAC` option

---
 .github/workflows/coverage.yml                  | 3 +++
 .github/workflows/docs.yml                      | 3 +++
 .github/workflows/locked.yml                    | 9 +++++++++
 .github/workflows/unlocked.yml                  | 6 ++++++
 make.sh                                         | 1 +
 scripts/update_suite.rb                         | 4 ++++
 tests/regression/82-barrier/01-simple.c         | 2 +-
 tests/regression/82-barrier/02-more.c           | 2 +-
 tests/regression/82-barrier/03-problem.c        | 2 +-
 tests/regression/82-barrier/04-challenge.c      | 2 +-
 tests/regression/82-barrier/05-mhp-not-enough.c | 2 +-
 11 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index fd2c55b84e..3f924869fc 100644
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -46,6 +46,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+        
       - name: Install coverage dependencies
         run: opam install bisect_ppx
 
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 0ada04e369..1a6d17fab4 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -46,6 +46,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-doc
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build API docs
         run: opam exec -- dune build @doc
 
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 16655bfdc7..8205d4ef34 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -48,6 +48,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 
@@ -100,6 +103,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 
@@ -142,6 +148,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Setup Gobview
         run: ./make.sh setup_gobview
 
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index f3fe6cc558..81d1d3dc1c 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -57,6 +57,9 @@ jobs:
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
+      
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
 
       - name: Install Apron dependencies
         if: ${{ matrix.apron }}
@@ -118,6 +121,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Install Apron dependencies
         run: |
           opam depext apron
diff --git a/make.sh b/make.sh
index 0f76759065..1ed5317aee 100755
--- a/make.sh
+++ b/make.sh
@@ -90,6 +90,7 @@ rule() {
       # Use `git commit -n` to temporarily bypass the hook if necessary.
       echo "Installing gem parallel (not needed for ./scripts/update_suite.rb -s)"
       sudo gem install parallel
+      sudo gem install os
     ;; headers)
       curl -L -O https://github.com/goblint/linux-headers/archive/master.tar.gz
       tar xf master.tar.gz && rm master.tar.gz
diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index b21fb4b532..74fddc7b04 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -2,6 +2,7 @@
 
 # gobopt environment variable can be used to override goblint defaults and PARAMs
 
+require 'os'
 require 'find'
 require 'fileutils'
 require 'timeout'
@@ -575,6 +576,8 @@ def run ()
     end
 end
 
+mac = OS.mac?
+
 #processing the file information
 projects = []
 project_ids = Set.new
@@ -603,6 +606,7 @@ def run ()
     lines = IO.readlines(path, :encoding => "UTF-8")
 
     next if not future and only.nil? and lines[0] =~ /SKIP/
+    next if mac and lines[0] =~ /NOMAC/
     next if marshal and lines[0] =~ /NOMARSHAL/
     next if not has_linux_headers and lines[0] =~ /kernel/
     if incremental then
diff --git a/tests/regression/82-barrier/01-simple.c b/tests/regression/82-barrier/01-simple.c
index 696e433962..285da1a6fb 100644
--- a/tests/regression/82-barrier/01-simple.c
+++ b/tests/regression/82-barrier/01-simple.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'pthreadBarriers'
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
 #include<pthread.h>
 #include<stdio.h>
 #include<unistd.h>
diff --git a/tests/regression/82-barrier/02-more.c b/tests/regression/82-barrier/02-more.c
index cdabe740ea..53b4e99de2 100644
--- a/tests/regression/82-barrier/02-more.c
+++ b/tests/regression/82-barrier/02-more.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'pthreadBarriers'
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
 #include<pthread.h>
 #include<stdio.h>
 #include<unistd.h>
diff --git a/tests/regression/82-barrier/03-problem.c b/tests/regression/82-barrier/03-problem.c
index d75245ccdd..2d80706b92 100644
--- a/tests/regression/82-barrier/03-problem.c
+++ b/tests/regression/82-barrier/03-problem.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'pthreadBarriers'
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
 #include<pthread.h>
 #include<stdio.h>
 #include<unistd.h>
diff --git a/tests/regression/82-barrier/04-challenge.c b/tests/regression/82-barrier/04-challenge.c
index 2b50b3ad06..73d66e5c51 100644
--- a/tests/regression/82-barrier/04-challenge.c
+++ b/tests/regression/82-barrier/04-challenge.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'pthreadBarriers'
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
 #include<pthread.h>
 #include<stdio.h>
 #include<unistd.h>
diff --git a/tests/regression/82-barrier/05-mhp-not-enough.c b/tests/regression/82-barrier/05-mhp-not-enough.c
index c627a4ff04..b289f3b0c0 100644
--- a/tests/regression/82-barrier/05-mhp-not-enough.c
+++ b/tests/regression/82-barrier/05-mhp-not-enough.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'pthreadBarriers'
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
 #include<pthread.h>
 #include<stdio.h>
 #include<unistd.h>

From a990b5f7fbcc225a5cba183ba29a3646c471eae3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 16:09:30 +0100
Subject: [PATCH 09/38] Remark that `os` gem is needed

---
 make.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/make.sh b/make.sh
index 1ed5317aee..fddbf73ae0 100755
--- a/make.sh
+++ b/make.sh
@@ -75,7 +75,7 @@ rule() {
     ;; setup)
       echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config"
       echo "For the --html output you also need: javac, ant, dot (graphviz)"
-      echo "For running the regression tests you also need: ruby, gem, curl"
+      echo "For running the regression tests you also need: ruby, gem, curl, and the `os` gem"
       echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
       opam_setup
     ;; dev)

From 27dd03001fc5d556b6d4d7fe154012f84e44869d Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 16:52:56 +0100
Subject: [PATCH 10/38] Make sound for multiprocess

---
 src/analyses/pthreadBarriers.ml               | 66 ++++++++++---------
 src/util/library/libraryDesc.ml               |  2 +-
 src/util/library/libraryFunctions.ml          |  2 +-
 tests/regression/82-barrier/06-multiprocess.c | 35 ++++++++++
 4 files changed, 73 insertions(+), 32 deletions(-)
 create mode 100644 tests/regression/82-barrier/06-multiprocess.c

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index a02c3332f4..049e0dbcf9 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -23,7 +23,8 @@ struct
 
   module TID = ThreadIdDomain.Thread
   module Waiters = SetDomain.ToppedSet (MHP) (struct let topname = "All MHP" end)
-  module G = Lattice.Prod (Capacity) (Waiters)
+  module Multiprocess = BoolDomain.MayBool
+  module G = Lattice.Prod3 (Multiprocess) (Capacity) (Waiters)
 
   let name () = "pthreadBarriers"
   module D = Lattice.Prod (Barriers) (MustBarriers)
@@ -42,37 +43,40 @@ struct
       let barriers = possible_vinfos ask barrier in
       let mhp = MHP.current ask in
       let handle_one b =
-        man.sideg b (Capacity.bot (), Waiters.singleton mhp);
+        man.sideg b (Multiprocess.bot (), 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 other -> MHP.may_happen_in_parallel mhp other) waiters in
+        let (multiprocess,capacity, waiters) = man.global b in
         let may_run =
-          if Waiters.exists MHP.may_be_non_unique_thread relevant_waiters then
+          if multiprocess then
             true
           else
-            let count = Waiters.cardinal relevant_waiters in
-            match capacity with
-            | `Lifted c -> 
-              (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
-              let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
-              if Z.leq min_cap Z.one then
-                true
-              else if min_cap = Z.of_int 2 && count = 1 then
-                true
-              else if Z.geq (Z.of_int (count + 1)) min_cap then
-                (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
-                  MHP is pairwise true? This solution is a sledgehammer, there should be something much
-                  better algorithmically (beyond just laziness) *)
-                let waiters = Waiters.elements relevant_waiters in
-                let min_cap = Z.to_int min_cap in
-                let lists = List.init (min_cap - 1) (fun _ -> waiters) in
-                let candidates = BatList.n_cartesian_product lists in
-                List.exists (fun candidate ->
-                  let pairwise = BatList.cartesian_product candidate candidate in
-                  List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise
-                ) candidates
-              else
-                false
+            let relevant_waiters = Waiters.filter (fun other -> MHP.may_happen_in_parallel mhp other) waiters in    
+            if Waiters.exists MHP.may_be_non_unique_thread relevant_waiters then
+              true
+            else
+              let count = Waiters.cardinal relevant_waiters in
+              match capacity with
+              | `Lifted c -> 
+                (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
+                let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
+                if Z.leq min_cap Z.one then
+                  true
+                else if min_cap = Z.of_int 2 && count = 1 then
+                  true
+                else if Z.geq (Z.of_int (count + 1)) min_cap then
+                  (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
+                    MHP is pairwise true? This solution is a sledgehammer, there should be something much
+                    better algorithmically (beyond just laziness) *)
+                  let waiters = Waiters.elements relevant_waiters in
+                  let min_cap = Z.to_int min_cap in
+                  let lists = List.init (min_cap - 1) (fun _ -> waiters) in
+                  let candidates = BatList.n_cartesian_product lists in
+                  List.exists (fun candidate ->
+                    let pairwise = BatList.cartesian_product candidate candidate in
+                    List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise
+                  ) candidates
+                else
+                  false
             | _ -> true
         in
         if may_run then
@@ -83,9 +87,11 @@ struct
       let (may, must) = List.fold_left (fun acc b-> D.join acc (handle_one b)) (D.bot ()) barriers in
       if Barriers.is_empty may then raise Analyses.Deadcode;
       (may, must)
-    | BarrierInit { barrier; count } ->
+    | BarrierInit { barrier; attr; count } ->
+      let multitprocess = not @@ Queries.AD.is_null @@ man.ask (Queries.MayPointTo attr) in
+      if multitprocess then M.warn "Barrier initialized with a non-NULL attr argument. Handled as if PTHREAD_PROCESS_SHARED potentially set.";
       let count = man.ask (Queries.EvalInt count) in
-      let publish_one b = man.sideg b (count, Waiters.bot ()) in 
+      let publish_one b = man.sideg b (multitprocess, count, Waiters.bot ()) in 
       let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in
       List.iter publish_one barriers;
       man.local
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
index 2da79dcc20..e439e97946 100644
--- a/src/util/library/libraryDesc.ml
+++ b/src/util/library/libraryDesc.ml
@@ -70,7 +70,7 @@ type special =
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
   | BarrierWait of Cil.exp
-  | BarrierInit of { barrier: Cil.exp; count: Cil.exp; }
+  | BarrierInit of { barrier: Cil.exp; attr:Cil.exp; count: Cil.exp; }
   | Math of { fun_args: math; }
   | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
   | Bzero of { dest: Cil.exp; count: Cil.exp; }
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index ab7d682483..1d36f69f3e 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -520,7 +520,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
     ("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]);
     ("pthread_key_delete", unknown [drop "key" [f]]);
-    ("pthread_barrier_init", special [__ "barrier" []; __ "attr" []; __ "count" []] @@ fun barrier attr count -> BarrierInit {barrier; count});
+    ("pthread_barrier_init", special [__ "barrier" []; __ "attr" []; __ "count" []] @@ fun barrier attr count -> BarrierInit {barrier; attr; count});
     ("pthread_barrier_wait", special [__ "barrier" []] @@ fun barrier -> BarrierWait barrier);
     ("pthread_cancel", unknown [drop "thread" []]);
     ("pthread_testcancel", unknown []);
diff --git a/tests/regression/82-barrier/06-multiprocess.c b/tests/regression/82-barrier/06-multiprocess.c
new file mode 100644
index 0000000000..f55790cfab
--- /dev/null
+++ b/tests/regression/82-barrier/06-multiprocess.c
@@ -0,0 +1,35 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrierattr_t barattr;
+    pthread_barrierattr_setpshared(&barattr, PTHREAD_PROCESS_SHARED);
+
+    pthread_barrier_init(&barrier, &barattr, 2);
+
+    fork();
+    pthread_t t1;
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Reachable if both processes go into this branch
+        i = 1;
+    }
+
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+
+    return 0;
+}

From 24d61c00f86e91036f023aa19c6c8beb365ae25c Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 16:56:56 +0100
Subject: [PATCH 11/38] Fix indentation

---
 src/analyses/pthreadBarriers.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 049e0dbcf9..2f2a1bb0fb 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -65,19 +65,19 @@ struct
                   true
                 else if Z.geq (Z.of_int (count + 1)) min_cap then
                   (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
-                    MHP is pairwise true? This solution is a sledgehammer, there should be something much
-                    better algorithmically (beyond just laziness) *)
+                     MHP is pairwise true? This solution is a sledgehammer, there should be something much
+                     better algorithmically (beyond just laziness) *)
                   let waiters = Waiters.elements relevant_waiters in
                   let min_cap = Z.to_int min_cap in
                   let lists = List.init (min_cap - 1) (fun _ -> waiters) in
                   let candidates = BatList.n_cartesian_product lists in
                   List.exists (fun candidate ->
-                    let pairwise = BatList.cartesian_product candidate candidate in
-                    List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise
-                  ) candidates
+                      let pairwise = BatList.cartesian_product candidate candidate in
+                      List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise
+                    ) candidates
                 else
                   false
-            | _ -> true
+              | _ -> true
         in
         if may_run then
           (Barriers.add addr may, Barriers.add addr must)

From 8fe2e16e4b8611215dc56d7946cfff5b6be09b72 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 18:10:50 +0100
Subject: [PATCH 12/38] Also consider locks

---
 src/analyses/pthreadBarriers.ml               | 26 +++++++---
 tests/regression/82-barrier/07-lockset.c      | 39 +++++++++++++++
 tests/regression/82-barrier/08-lockset-more.c | 47 +++++++++++++++++++
 3 files changed, 106 insertions(+), 6 deletions(-)
 create mode 100644 tests/regression/82-barrier/07-lockset.c
 create mode 100644 tests/regression/82-barrier/08-lockset-more.c

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 2f2a1bb0fb..56c615aa53 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -22,7 +22,20 @@ struct
   module V = VarinfoV
 
   module TID = ThreadIdDomain.Thread
-  module Waiters = SetDomain.ToppedSet (MHP) (struct let topname = "All MHP" end)
+
+  module MHPplusLock = struct
+    module Locks = LockDomain.MustLockset
+
+    include Printable.Prod (MHP) (Locks)
+    let name () = "MHPplusLock"
+
+    let mhp (mhp1, l1) (mhp2, l2) = 
+      MHP.may_happen_in_parallel mhp1 mhp2 && Locks.is_empty (Locks.inter l1 l2)
+
+    let may_be_non_unique_thread (mhp, _) = MHP.may_be_non_unique_thread mhp
+  end
+
+  module Waiters = SetDomain.ToppedSet (MHPplusLock) (struct let topname = "All MHP" end)
   module Multiprocess = BoolDomain.MayBool
   module G = Lattice.Prod3 (Multiprocess) (Capacity) (Waiters)
 
@@ -43,15 +56,16 @@ struct
       let barriers = possible_vinfos ask barrier in
       let mhp = MHP.current ask in
       let handle_one b =
-        man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton mhp);
+        let locks = man.ask (Queries.MustLockset) in
+        man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks));
         let addr = ValueDomain.Addr.of_var b in
         let (multiprocess,capacity, waiters) = man.global b in
         let may_run =
           if multiprocess then
             true
           else
-            let relevant_waiters = Waiters.filter (fun other -> MHP.may_happen_in_parallel mhp other) waiters in    
-            if Waiters.exists MHP.may_be_non_unique_thread relevant_waiters then
+            let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in    
+            if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then
               true
             else
               let count = Waiters.cardinal relevant_waiters in
@@ -61,7 +75,7 @@ struct
                 let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
                 if Z.leq min_cap Z.one then
                   true
-                else if min_cap = Z.of_int 2 && count = 1 then
+                else if min_cap = Z.of_int 2 && count >= 1 then
                   true
                 else if Z.geq (Z.of_int (count + 1)) min_cap then
                   (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
@@ -73,7 +87,7 @@ struct
                   let candidates = BatList.n_cartesian_product lists in
                   List.exists (fun candidate ->
                       let pairwise = BatList.cartesian_product candidate candidate in
-                      List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise
+                      List.for_all (fun (a,b) -> MHPplusLock.mhp a b) pairwise
                     ) candidates
                 else
                   false
diff --git a/tests/regression/82-barrier/07-lockset.c b/tests/regression/82-barrier/07-lockset.c
new file mode 100644
index 0000000000..d1c68f3d7f
--- /dev/null
+++ b/tests/regression/82-barrier/07-lockset.c
@@ -0,0 +1,39 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    pthread_barrier_wait(&barrier);
+    pthread_mutex_unlock(&mutex);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_mutex_lock(&mutex);
+        pthread_barrier_wait(&barrier);
+        // Deadlocks
+        pthread_mutex_unlock(&mutex);
+        i = 1;
+    }
+
+    __goblint_check(i == 0);
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/08-lockset-more.c b/tests/regression/82-barrier/08-lockset-more.c
new file mode 100644
index 0000000000..a33ecc1a78
--- /dev/null
+++ b/tests/regression/82-barrier/08-lockset-more.c
@@ -0,0 +1,47 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    pthread_barrier_wait(&barrier);
+    pthread_mutex_unlock(&mutex);
+    return NULL;
+}
+
+void* f2(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    pthread_barrier_wait(&barrier);
+    pthread_mutex_unlock(&mutex);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+
+    pthread_t t2;
+    pthread_create(&t2,NULL,f2,NULL);
+    
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        i = 1;
+    }
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+    return 0;
+}

From 05d2f60ffcc0faae7f7673a30822cd29f42603e8 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 19:15:04 +0100
Subject: [PATCH 13/38] Minimal race handling

---
 src/analyses/pthreadBarriers.ml       | 54 ++++++++++++++++++++-------
 tests/regression/82-barrier/09-race.c | 36 ++++++++++++++++++
 2 files changed, 77 insertions(+), 13 deletions(-)
 create mode 100644 tests/regression/82-barrier/09-race.c

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 56c615aa53..6c8a823658 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -21,7 +21,7 @@ struct
   include Analyses.IdentitySpec
   module V = VarinfoV
 
-  module TID = ThreadIdDomain.Thread
+  module TID = ThreadIdDomain.ThreadLifted
 
   module MHPplusLock = struct
     module Locks = LockDomain.MustLockset
@@ -32,6 +32,8 @@ struct
     let mhp (mhp1, l1) (mhp2, l2) = 
       MHP.may_happen_in_parallel mhp1 mhp2 && Locks.is_empty (Locks.inter l1 l2)
 
+    let tid ((mhp:MHP.t), _) = mhp.tid
+
     let may_be_non_unique_thread (mhp, _) = MHP.may_be_non_unique_thread mhp
   end
 
@@ -40,7 +42,9 @@ struct
   module G = Lattice.Prod3 (Multiprocess) (Capacity) (Waiters)
 
   let name () = "pthreadBarriers"
-  module D = Lattice.Prod (Barriers) (MustBarriers)
+
+  module MustObserved = MapDomain.MapTop_LiftBot (TID) (MustBarriers)
+  module D = Lattice.Prod (Barriers) (MustObserved)
 
   include Analyses.ValueContexts(D)
 
@@ -60,13 +64,13 @@ struct
         man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks));
         let addr = ValueDomain.Addr.of_var b in
         let (multiprocess,capacity, waiters) = man.global b in
-        let may_run =
+        let may_run, must =
           if multiprocess then
-            true
+            true, must
           else
             let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in    
             if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then
-              true
+              true, must
             else
               let count = Waiters.cardinal relevant_waiters in
               match capacity with
@@ -74,9 +78,14 @@ struct
                 (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
                 let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
                 if Z.leq min_cap Z.one then
-                  true
+                  true, must
+                else if min_cap = Z.of_int 2 && count = 1 then
+                  let elem = Waiters.choose relevant_waiters in
+                  let curr = MustObserved.find (MHPplusLock.tid elem) must in
+                  let must' = MustObserved.add (MHPplusLock.tid elem) (Barriers.add addr curr) must in
+                  true, must'
                 else if min_cap = Z.of_int 2 && count >= 1 then
-                  true
+                  true, must
                 else if Z.geq (Z.of_int (count + 1)) min_cap then
                   (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
                      MHP is pairwise true? This solution is a sledgehammer, there should be something much
@@ -88,13 +97,13 @@ struct
                   List.exists (fun candidate ->
                       let pairwise = BatList.cartesian_product candidate candidate in
                       List.for_all (fun (a,b) -> MHPplusLock.mhp a b) pairwise
-                    ) candidates
+                    ) candidates, must
                 else
-                  false
-              | _ -> true
+                  false, must
+              | _ -> true, must
         in
         if may_run then
-          (Barriers.add addr may, Barriers.add addr must)
+          (Barriers.add addr may, must)
         else
           D.bot ()
       in
@@ -111,9 +120,28 @@ struct
       man.local
     | _ -> man.local
 
-  let startstate v = (Barriers.empty (), Barriers.empty ())
+  let startstate v = (Barriers.empty (), MustObserved.empty ())
   let threadenter man ~multiple lval f args = [man.local]
-  let exitstate  v = (Barriers.empty (), Barriers.empty ())
+  let exitstate  v = (Barriers.empty (), MustObserved.empty ())
+
+  module A =
+  struct
+    include Lattice.Prod3 (Barriers) (MustObserved) (TID)
+    let name () = "barriers"
+    let may_race (may_await_t1, must_observed_by_t1, t1) (may_await_t2, must_observed_by_t2, t2) =
+      let observed_from_t2 = MustObserved.find t2 must_observed_by_t1 in
+      if not (Barriers.subset observed_from_t2 may_await_t2) then
+        false
+      else
+        let observed_from_t1 = MustObserved.find t1 must_observed_by_t2 in
+        Barriers.subset observed_from_t1 may_await_t1
+    let should_print f = true
+  end
+
+  let access man (a: Queries.access) = 
+    let (may,must) = man.local in
+    let mhp = MHP.current (Analyses.ask_of_man man) in
+    (may, must, mhp.tid)
 end
 
 let _ =
diff --git a/tests/regression/82-barrier/09-race.c b/tests/regression/82-barrier/09-race.c
new file mode 100644
index 0000000000..fad6ad6243
--- /dev/null
+++ b/tests/regression/82-barrier/09-race.c
@@ -0,0 +1,36 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+int h;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    g = 2; //NORACE
+    h = 3; //RACE
+    pthread_barrier_wait(&barrier);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+
+    h = 5; //RACE
+
+    pthread_barrier_wait(&barrier);
+    g = 3; //NORACE
+
+    return 0;
+}

From 1b3a0d8ebdf9107c285cbdcb229d6a7304536cb0 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 19:44:26 +0100
Subject: [PATCH 14/38] Fix pairwise MHP check

---
 src/analyses/pthreadBarriers.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 6c8a823658..52e040544f 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -90,14 +90,20 @@ struct
                   (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
                      MHP is pairwise true? This solution is a sledgehammer, there should be something much
                      better algorithmically (beyond just laziness) *)
+                  (
                   let waiters = Waiters.elements relevant_waiters in
                   let min_cap = Z.to_int min_cap in
+                  M.warn "entered case min_cap is %i, waiters is %i" min_cap (List.length waiters);
                   let lists = List.init (min_cap - 1) (fun _ -> waiters) in
                   let candidates = BatList.n_cartesian_product lists in
-                  List.exists (fun candidate ->
-                      let pairwise = BatList.cartesian_product candidate candidate in
-                      List.for_all (fun (a,b) -> MHPplusLock.mhp a b) pairwise
-                    ) candidates, must
+                  let pred = List.exists (fun candidate ->
+                      let rec do_it = function
+                        | [] -> true
+                        | x::xs -> List.for_all (fun y -> MHPplusLock.mhp x y) xs  && do_it xs
+                      in
+                      do_it candidate
+                    ) candidates in
+                  pred, must)
                 else
                   false, must
               | _ -> true, must

From 7e98213918bc92e59a13bc9eb341872f7ce1d691 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 19:57:53 +0100
Subject: [PATCH 15/38] Add case for more waiters

---
 src/analyses/pthreadBarriers.ml            | 39 +++++++++++++++-------
 tests/regression/82-barrier/10-several.c   | 36 ++++++++++++++++++++
 tests/regression/82-barrier/11-race-more.c | 37 ++++++++++++++++++++
 3 files changed, 100 insertions(+), 12 deletions(-)
 create mode 100644 tests/regression/82-barrier/10-several.c
 create mode 100644 tests/regression/82-barrier/11-race-more.c

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 52e040544f..83e253f66f 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -91,19 +91,34 @@ struct
                      MHP is pairwise true? This solution is a sledgehammer, there should be something much
                      better algorithmically (beyond just laziness) *)
                   (
-                  let waiters = Waiters.elements relevant_waiters in
-                  let min_cap = Z.to_int min_cap in
-                  M.warn "entered case min_cap is %i, waiters is %i" min_cap (List.length waiters);
-                  let lists = List.init (min_cap - 1) (fun _ -> waiters) in
-                  let candidates = BatList.n_cartesian_product lists in
-                  let pred = List.exists (fun candidate ->
-                      let rec do_it = function
-                        | [] -> true
-                        | x::xs -> List.for_all (fun y -> MHPplusLock.mhp x y) xs  && do_it xs
+                    let waiters = Waiters.elements relevant_waiters in
+                    let min_cap = Z.to_int min_cap in
+                    let lists = List.init (min_cap - 1) (fun _ -> waiters) in
+                    let candidates = BatList.n_cartesian_product lists in
+                    let pred = List.exists (fun candidate ->
+                        let rec do_it = function
+                          | [] -> true
+                          | x::xs -> List.for_all (fun y -> MHPplusLock.mhp x y) xs  && do_it xs
+                        in
+                        do_it candidate
+                      ) candidates
+                    in
+                    if pred then
+                      (* limit to this case to avoid having to construct all permutations above *)
+                      let must = if (List.length waiters) = min_cap-1 then
+                          List.fold_left (fun acc elem -> 
+                              let tid = MHPplusLock.tid elem in
+                              let curr = MustObserved.find tid acc in
+                              let must' = MustObserved.add tid (Barriers.add addr curr) acc in
+                              must'
+                            ) must waiters
+                        else 
+                          must
                       in
-                      do_it candidate
-                    ) candidates in
-                  pred, must)
+                      true, must
+                    else
+                      false, must
+                  )
                 else
                   false, must
               | _ -> true, must
diff --git a/tests/regression/82-barrier/10-several.c b/tests/regression/82-barrier/10-several.c
new file mode 100644
index 0000000000..6fc9f57681
--- /dev/null
+++ b/tests/regression/82-barrier/10-several.c
@@ -0,0 +1,36 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 4);
+
+    pthread_t t1, t2, t3;
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_create(&t2,NULL,f1,NULL);
+    pthread_create(&t3,NULL,f1,NULL);
+
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        i = 1;
+    }
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/11-race-more.c b/tests/regression/82-barrier/11-race-more.c
new file mode 100644
index 0000000000..ed6c7ef29d
--- /dev/null
+++ b/tests/regression/82-barrier/11-race-more.c
@@ -0,0 +1,37 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    g = 4711; //NORACE
+    pthread_mutex_unlock(&mutex);
+    pthread_barrier_wait(&barrier);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 4);
+
+    pthread_t t1, t2, t3;
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_create(&t2,NULL,f1,NULL);
+    pthread_create(&t3,NULL,f1,NULL);
+
+    pthread_barrier_wait(&barrier);
+
+    g = 3; //NORACE
+
+    return 0;
+}

From 1b4beae60e768f729843a600d387d5bd00fe0911 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 20:01:08 +0100
Subject: [PATCH 16/38] Get rid of overcomplicated logic

---
 src/analyses/pthreadBarriers.ml | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 83e253f66f..4ea5f1540a 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -79,13 +79,6 @@ struct
                 let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
                 if Z.leq min_cap Z.one then
                   true, must
-                else if min_cap = Z.of_int 2 && count = 1 then
-                  let elem = Waiters.choose relevant_waiters in
-                  let curr = MustObserved.find (MHPplusLock.tid elem) must in
-                  let must' = MustObserved.add (MHPplusLock.tid elem) (Barriers.add addr curr) must in
-                  true, must'
-                else if min_cap = Z.of_int 2 && count >= 1 then
-                  true, must
                 else if Z.geq (Z.of_int (count + 1)) min_cap then
                   (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
                      MHP is pairwise true? This solution is a sledgehammer, there should be something much

From 1bfb9857b586969f701c32ff03439faa70ddb532 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 25 Dec 2024 20:20:39 +0100
Subject: [PATCH 17/38] Cleanup

---
 src/analyses/pthreadBarriers.ml | 68 +++++++++++++++------------------
 1 file changed, 31 insertions(+), 37 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 4ea5f1540a..e26b657805 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -60,35 +60,37 @@ struct
       let barriers = possible_vinfos ask barrier in
       let mhp = MHP.current ask in
       let handle_one b =
-        let locks = man.ask (Queries.MustLockset) in
-        man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks));
-        let addr = ValueDomain.Addr.of_var b in
-        let (multiprocess,capacity, waiters) = man.global b in
-        let may_run, must =
+        try 
+          let locks = man.ask (Queries.MustLockset) in
+          man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks));
+          let addr = ValueDomain.Addr.of_var b in
+          let (multiprocess, capacity, waiters) = man.global b in
+          let may = Barriers.add addr may in
           if multiprocess then
-            true, must
+            (may, must)
           else
-            let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in    
+            let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in 
             if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then
-              true, must
+              (may, must) 
             else
-              let count = Waiters.cardinal relevant_waiters in
               match capacity with
+              | `Top | `Bot -> (may, must)
               | `Lifted c -> 
+                let count = Waiters.cardinal relevant_waiters in
                 (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
                 let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
                 if Z.leq min_cap Z.one then
-                  true, must
+                  (may, must)
                 else if Z.geq (Z.of_int (count + 1)) min_cap then
                   (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
-                     MHP is pairwise true? This solution is a sledgehammer, there should be something much
-                     better algorithmically (beyond just laziness) *)
-                  (
+                      MHP is pairwise true? This solution is a sledgehammer, there should be something much
+                      better algorithmically (beyond just laziness) *)
+                  let must = 
                     let waiters = Waiters.elements relevant_waiters in
                     let min_cap = Z.to_int min_cap in
                     let lists = List.init (min_cap - 1) (fun _ -> waiters) in
                     let candidates = BatList.n_cartesian_product lists in
-                    let pred = List.exists (fun candidate ->
+                    let can_proceed = List.exists (fun candidate ->
                         let rec do_it = function
                           | [] -> true
                           | x::xs -> List.for_all (fun y -> MHPplusLock.mhp x y) xs  && do_it xs
@@ -96,30 +98,22 @@ struct
                         do_it candidate
                       ) candidates
                     in
-                    if pred then
-                      (* limit to this case to avoid having to construct all permutations above *)
-                      let must = if (List.length waiters) = min_cap-1 then
-                          List.fold_left (fun acc elem -> 
-                              let tid = MHPplusLock.tid elem in
-                              let curr = MustObserved.find tid acc in
-                              let must' = MustObserved.add tid (Barriers.add addr curr) acc in
-                              must'
-                            ) must waiters
-                        else 
-                          must
-                      in
-                      true, must
-                    else
-                      false, must
-                  )
+                    if not can_proceed then raise Analyses.Deadcode;
+                    (* limit to this case to avoid having to construct all permutations above *)
+                    if List.length waiters = min_cap - 1 then
+                      List.fold_left (fun acc elem -> 
+                          let tid = MHPplusLock.tid elem in
+                          let curr = MustObserved.find tid acc in
+                          let must' = MustObserved.add tid (Barriers.add addr curr) acc in
+                          must'
+                        ) must waiters
+                    else 
+                      must
+                  in
+                  (may, must)
                 else
-                  false, must
-              | _ -> true, must
-        in
-        if may_run then
-          (Barriers.add addr may, must)
-        else
-          D.bot ()
+                  raise Analyses.Deadcode;
+        with Analyses.Deadcode -> D.bot ()
       in
       let (may, must) = List.fold_left (fun acc b-> D.join acc (handle_one b)) (D.bot ()) barriers in
       if Barriers.is_empty may then raise Analyses.Deadcode;

From 35bec2d199f888e034b7e6fe08361e7988304ea9 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 17 Jan 2025 14:26:12 +0100
Subject: [PATCH 18/38] Fix `List.length` call

---
 src/analyses/pthreadBarriers.ml | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index e26b657805..1cea151fed 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -13,7 +13,7 @@ struct
 
   module MustBarriers = struct
     include Lattice.Reverse (Barriers)
-    let name () = "mustBarriers" 
+    let name () = "mustBarriers"
   end
 
   module Capacity = Queries.ID
@@ -29,7 +29,7 @@ struct
     include Printable.Prod (MHP) (Locks)
     let name () = "MHPplusLock"
 
-    let mhp (mhp1, l1) (mhp2, l2) = 
+    let mhp (mhp1, l1) (mhp2, l2) =
       MHP.may_happen_in_parallel mhp1 mhp2 && Locks.is_empty (Locks.inter l1 l2)
 
     let tid ((mhp:MHP.t), _) = mhp.tid
@@ -60,7 +60,7 @@ struct
       let barriers = possible_vinfos ask barrier in
       let mhp = MHP.current ask in
       let handle_one b =
-        try 
+        try
           let locks = man.ask (Queries.MustLockset) in
           man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks));
           let addr = ValueDomain.Addr.of_var b in
@@ -69,23 +69,23 @@ struct
           if multiprocess then
             (may, must)
           else
-            let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in 
+            let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in
             if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then
-              (may, must) 
+              (may, must)
             else
               match capacity with
               | `Top | `Bot -> (may, must)
-              | `Lifted c -> 
+              | `Lifted c ->
                 let count = Waiters.cardinal relevant_waiters in
                 (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
                 let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
                 if Z.leq min_cap Z.one then
                   (may, must)
                 else if Z.geq (Z.of_int (count + 1)) min_cap then
-                  (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
+                  (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that
                       MHP is pairwise true? This solution is a sledgehammer, there should be something much
                       better algorithmically (beyond just laziness) *)
-                  let must = 
+                  let must =
                     let waiters = Waiters.elements relevant_waiters in
                     let min_cap = Z.to_int min_cap in
                     let lists = List.init (min_cap - 1) (fun _ -> waiters) in
@@ -100,14 +100,14 @@ struct
                     in
                     if not can_proceed then raise Analyses.Deadcode;
                     (* limit to this case to avoid having to construct all permutations above *)
-                    if List.length waiters = min_cap - 1 then
-                      List.fold_left (fun acc elem -> 
+                    if BatList.compare_length_with waiters (min_cap - 1) = 0 then
+                      List.fold_left (fun acc elem ->
                           let tid = MHPplusLock.tid elem in
                           let curr = MustObserved.find tid acc in
                           let must' = MustObserved.add tid (Barriers.add addr curr) acc in
                           must'
                         ) must waiters
-                    else 
+                    else
                       must
                   in
                   (may, must)
@@ -122,7 +122,7 @@ struct
       let multitprocess = not @@ Queries.AD.is_null @@ man.ask (Queries.MayPointTo attr) in
       if multitprocess then M.warn "Barrier initialized with a non-NULL attr argument. Handled as if PTHREAD_PROCESS_SHARED potentially set.";
       let count = man.ask (Queries.EvalInt count) in
-      let publish_one b = man.sideg b (multitprocess, count, Waiters.bot ()) in 
+      let publish_one b = man.sideg b (multitprocess, count, Waiters.bot ()) in
       let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in
       List.iter publish_one barriers;
       man.local
@@ -146,7 +146,7 @@ struct
     let should_print f = true
   end
 
-  let access man (a: Queries.access) = 
+  let access man (a: Queries.access) =
     let (may,must) = man.local in
     let mhp = MHP.current (Analyses.ask_of_man man) in
     (may, must, mhp.tid)

From ea90d39aed8d8c8068709ce0b1e715ed097c66b1 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 24 Jan 2025 15:28:48 +0100
Subject: [PATCH 19/38] Add first handling to constraints

---
 src/framework/constraints.ml          | 24 +++++++++++++++---------
 src/util/library/libraryDesc.ml       |  1 +
 src/util/library/libraryFunctions.ml  | 10 +++++-----
 src/util/library/libraryFunctions.mli |  2 +-
 tests/regression/83-once/01-sanity.c  | 24 ++++++++++++++++++++++++
 5 files changed, 46 insertions(+), 15 deletions(-)
 create mode 100644 tests/regression/83-once/01-sanity.c

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index c7cfce95d2..9ff295355e 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -245,7 +245,7 @@ struct
 
   let tf_special_call man lv f args = S.special man lv f args
 
-  let tf_proc var edge prev_node lv e args getl sidel getg sideg d =
+  let rec tf_proc var edge prev_node lv e args getl sidel getg sideg d =
     let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
     let functions =
       match e with
@@ -266,14 +266,20 @@ struct
         (* Check whether number of arguments fits. *)
         (* If params is None, the function or its parameters are not declared, so we still analyze the unknown function call. *)
         if Option.is_none params || p_length = arg_length || (var_arg && arg_length >= p_length) then
-          begin Some (match Cilfacade.find_varinfo_fundec f with
-              | fd when LibraryFunctions.use_special f.vname ->
-                M.info ~category:Analyzer "Using special for defined function %s" f.vname;
-                tf_special_call man lv f args
-              | fd ->
-                tf_normal_call man lv e fd args getl sidel getg sideg
-              | exception Not_found ->
-                tf_special_call man lv f args)
+          begin
+            let is_once = LibraryFunctions.find ~nowarn:true f in
+            match is_once.special args with
+            | Once { once_control; init_routine } ->
+              Some (D.join d (tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d))
+            | _ ->
+              Some (match Cilfacade.find_varinfo_fundec f with
+                  | fd when LibraryFunctions.use_special f.vname ->
+                    M.info ~category:Analyzer "Using special for defined function %s" f.vname;
+                    tf_special_call man lv f args
+                  | fd ->
+                    tf_normal_call man lv e fd args getl sidel getg sideg
+                  | exception Not_found ->
+                    tf_special_call man lv f args)
           end
         else begin
           let geq = if var_arg then ">=" else "" in
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
index 6f34de1864..85de9d0f05 100644
--- a/src/util/library/libraryDesc.ml
+++ b/src/util/library/libraryDesc.ml
@@ -84,6 +84,7 @@ type special =
   | Longjmp of { env: Cil.exp; value: Cil.exp; }
   | Bounded of { exp: Cil.exp}  (** Used to check for bounds for termination analysis. *)
   | Rand
+  | Once of { once_control: Cil.exp; init_routine: Cil.exp; }
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 
 
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 6643b58eef..1fa4ecc8e9 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -464,6 +464,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
     ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
     ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
+    ("pthread_once", special [__ "once_control" []; __ "init_routine" []] @@ fun once_control init_routine -> Once {once_control; init_routine});
     ("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
     ("pthread_equal", unknown [drop "t1" []; drop "t2" []]);
     ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
@@ -1298,7 +1299,7 @@ let is_safe_uncalled fn_name =
   List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex
 
 
-let unknown_desc f : LibraryDesc.t =
+let unknown_desc f ~nowarn : LibraryDesc.t =
   let accs args : (LibraryDesc.Access.t * 'a list) list = [
     ({ kind = Read; deep = true; }, if GobConfig.get_bool "sem.unknown_function.read.args" then args else []);
     ({ kind = Write; deep = true; }, if GobConfig.get_bool "sem.unknown_function.invalidate.args" then args else []);
@@ -1314,7 +1315,7 @@ let unknown_desc f : LibraryDesc.t =
       []
   in
   (* TODO: remove hack when all classify are migrated *)
-  if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
+  if not nowarn && not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
     M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing";
     M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname
   );
@@ -1324,12 +1325,11 @@ let unknown_desc f : LibraryDesc.t =
     special = fun _ -> Unknown;
   }
 
-let find f =
+let find ?(nowarn=false) f =
   let name = f.vname in
   match Hashtbl.find_option (ResettableLazy.force activated_library_descs) name with
   | Some desc -> desc
-  | None -> unknown_desc f
-
+  | None -> unknown_desc ~nowarn f
 
 let is_special fv =
   if use_special fv.vname then
diff --git a/src/util/library/libraryFunctions.mli b/src/util/library/libraryFunctions.mli
index 9a8e55a48a..7eb9c531fe 100644
--- a/src/util/library/libraryFunctions.mli
+++ b/src/util/library/libraryFunctions.mli
@@ -11,7 +11,7 @@ val use_special : string -> bool
 val is_safe_uncalled : string -> bool
 
 (** Find library function descriptor for {e special} function (as per {!is_special}). *)
-val find: Cil.varinfo -> LibraryDesc.t
+val find: ?nowarn:bool -> Cil.varinfo -> LibraryDesc.t
 
 val is_special: Cil.varinfo -> bool
 (** Check if function is treated specially. *)
diff --git a/tests/regression/83-once/01-sanity.c b/tests/regression/83-once/01-sanity.c
new file mode 100644
index 0000000000..954f70dd4b
--- /dev/null
+++ b/tests/regression/83-once/01-sanity.c
@@ -0,0 +1,24 @@
+// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void fun() {
+  g++;
+}
+
+
+int main(void) {
+  pthread_t id;
+
+  pthread_once(&once, fun);
+  pthread_once(&once, fun);
+
+  // This fails if the (actual) case that it is not executed twice is ignored.
+  __goblint_check(g == 1); //TODO
+
+  return 0;
+}

From 383ad9495d416b397e7d02b9d998a5ce2ab78b29 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 24 Jan 2025 16:12:36 +0100
Subject: [PATCH 20/38] Fix failing test

---
 src/framework/constraints.ml    | 8 ++++++--
 src/util/library/libraryDsl.ml  | 2 ++
 src/util/library/libraryDsl.mli | 2 ++
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 9ff295355e..cb510501b7 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -258,6 +258,9 @@ struct
         let ad = man.ask (Queries.EvalFunvar e) in
         Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
+    let once once_control init_routine =
+      D.join d (tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d)
+    in
     let one_function f =
       match f.vtype with
       | TFun (_, params, var_arg, _)  ->
@@ -270,8 +273,9 @@ struct
             let is_once = LibraryFunctions.find ~nowarn:true f in
             match is_once.special args with
             | Once { once_control; init_routine } ->
-              Some (D.join d (tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d))
-            | _ ->
+              Some (once once_control init_routine)
+            | _
+            | exception LibraryDsl.Expected _-> (* propagate weirdness inside *)
               Some (match Cilfacade.find_varinfo_fundec f with
                   | fd when LibraryFunctions.use_special f.vname ->
                     M.info ~category:Analyzer "Using special for defined function %s" f.vname;
diff --git a/src/util/library/libraryDsl.ml b/src/util/library/libraryDsl.ml
index a380714dc0..240c318579 100644
--- a/src/util/library/libraryDsl.ml
+++ b/src/util/library/libraryDsl.ml
@@ -30,6 +30,8 @@ struct
     | [] -> fail "^::"
 end
 
+exception Expected = Pattern.Expected
+
 type access =
   | Access of LibraryDesc.Access.t
   | If of (unit -> bool) * access
diff --git a/src/util/library/libraryDsl.mli b/src/util/library/libraryDsl.mli
index 42c300af8e..2eed55666d 100644
--- a/src/util/library/libraryDsl.mli
+++ b/src/util/library/libraryDsl.mli
@@ -82,3 +82,5 @@ val c_deep: access
 
 (** Conditional access, e.g. on an option. *)
 val if_: (unit -> bool) -> access -> access
+
+exception Expected of string

From ff411e44f34b6a7fe5f5047886d6fd7053f0eb16 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 24 Jan 2025 16:34:22 +0100
Subject: [PATCH 21/38] More events & constraints

---
 src/domains/events.ml        |  8 +++++++-
 src/framework/constraints.ml | 16 +++++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/domains/events.ml b/src/domains/events.ml
index cc4af83819..205b81e443 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -16,6 +16,8 @@ type t =
   | Assert of exp
   | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list}
   | Longjmped of {lval: CilType.Lval.t option}
+  | EnterOnce of {once_control: CilType.Exp.t; tf:bool}
+  | LeaveOnce of {once_control: CilType.Exp.t}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
 let emit_on_deadcode = function
@@ -31,7 +33,9 @@ let emit_on_deadcode = function
   | UpdateExpSplit _ (* Pointless to split on dead. *)
   | Unassume _ (* Avoid spurious writes. *)
   | Assert _ (* Pointless to refine dead. *)
-  | Longjmped _ ->
+  | Longjmped _
+  | EnterOnce _
+  | LeaveOnce _ ->
     false
 
 let pretty () = function
@@ -47,3 +51,5 @@ let pretty () = function
   | Assert exp -> dprintf "Assert %a" d_exp exp
   | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
+  | EnterOnce {once_control; tf} -> dprintf "todo"
+  | LeaveOnce {once_control} -> dprintf "todo"
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index cb510501b7..d2c1c8215b 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -259,7 +259,21 @@ struct
         Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
     let once once_control init_routine =
-      D.join d (tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d)
+      let enter =
+        let d' = S.event man (Events.EnterOnce { once_control;  tf = true }) man in
+        let proc = tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d' in
+        let rec proc_man =
+          { man with
+            ask = (fun (type a) (q: a Queries.t) -> S.query proc_man q);
+            local = proc;
+          }
+        in
+        S.event proc_man (Events.LeaveOnce { once_control }) proc_man
+      in
+      let not_enter =
+        S.event man (Events.EnterOnce { once_control;  tf = false }) man
+      in
+      D.join enter not_enter
     in
     let one_function f =
       match f.vtype with

From 8fff9a5d9b8c89f2e8d1a0a294a8e0ea64edb86b Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 24 Jan 2025 17:43:27 +0100
Subject: [PATCH 22/38] Onces

---
 src/analyses/pthreadOnce.ml          | 90 ++++++++++++++++++++++++++++
 src/framework/constraints.ml         |  9 ++-
 tests/regression/83-once/01-sanity.c |  2 +-
 3 files changed, 99 insertions(+), 2 deletions(-)
 create mode 100644 src/analyses/pthreadOnce.ml

diff --git a/src/analyses/pthreadOnce.ml b/src/analyses/pthreadOnce.ml
new file mode 100644
index 0000000000..30c7756089
--- /dev/null
+++ b/src/analyses/pthreadOnce.ml
@@ -0,0 +1,90 @@
+(** Must active and have passed pthreadOnce calls ([pthreadOnce]). *)
+
+open GoblintCil
+open Analyses
+module LF = LibraryFunctions
+
+module Spec =
+struct
+  module Onces = struct
+    include SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All onces" end)
+    let name () = "mayOnces"
+  end
+
+  module ActiveOnces = struct
+    include Lattice.Reverse (Onces)
+    let name () = "active"
+  end
+
+  module SeenOnces = struct
+    include Lattice.Reverse (Onces)
+    let name () = "seen"
+  end
+
+  include Analyses.DefaultSpec
+
+  let name () = "pthreadOnce"
+  module D = Lattice.Prod (ActiveOnces) (SeenOnces)
+  include Analyses.ValueContexts(D)
+
+  (* transfer functions *)
+  let assign man (lval:lval) (rval:exp) : D.t =
+    man.local
+
+  let branch man (exp:exp) (tv:bool) : D.t =
+    man.local
+
+  let body man (f:fundec) : D.t =
+    man.local
+
+  let return man (exp:exp option) (f:fundec) : D.t =
+    man.local
+
+  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [man.local, man.local]
+
+  let combine_env man lval fexp f args fc au f_ask =
+    au
+
+  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+    man.local
+
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    man.local
+
+  let startstate v = (Onces.empty (), Onces.empty ())
+
+  let possible_vinfos (a: Queries.ask) barrier =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
+
+  let event man (e: Events.t) oman : D.t =
+    match e with
+    | Events.EnterOnce { once_control; tf } ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       match possible_vinfos ask once_control with
+       | [v] ->
+         (Onces.add v active, seen)
+       | _ ->
+         man.local)
+    | Events.LeaveOnce { once_control } ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       let active' = Onces.diff active (Onces.of_list (possible_vinfos ask once_control)) in
+       let seen' = match possible_vinfos ask once_control with
+         | [v] -> Onces.add v seen
+         | _ -> seen
+       in
+       (active', seen'))
+    | _ -> man.local
+
+  let threadenter man ~multiple lval f args =
+    let (_, seen) = man.local in
+    [Onces.empty (), seen]
+
+  let threadspawn man ~multiple lval f args fman = man.local
+  let exitstate  v = D.top ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index d2c1c8215b..97dffe5d6c 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -271,7 +271,14 @@ struct
         S.event proc_man (Events.LeaveOnce { once_control }) proc_man
       in
       let not_enter =
-        S.event man (Events.EnterOnce { once_control;  tf = false }) man
+        let d' = S.event man (Events.EnterOnce { once_control;  tf = false }) man in
+        let rec d'_man =
+          { man with
+            ask = (fun (type a) (q: a Queries.t) -> S.query d'_man q);
+            local = d';
+          }
+        in
+        S.event d'_man (Events.LeaveOnce { once_control }) d'_man
       in
       D.join enter not_enter
     in
diff --git a/tests/regression/83-once/01-sanity.c b/tests/regression/83-once/01-sanity.c
index 954f70dd4b..3d7875e0c5 100644
--- a/tests/regression/83-once/01-sanity.c
+++ b/tests/regression/83-once/01-sanity.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 

From ab0a9dbce376ade09bcaad25e567d16575daa61e Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 24 Jan 2025 18:04:16 +0100
Subject: [PATCH 23/38] Refine

---
 src/analyses/pthreadOnce.ml          | 15 +++++++++++----
 src/framework/constraints.ml         | 18 +++++++++++-------
 tests/regression/83-once/01-sanity.c |  7 +++++--
 3 files changed, 27 insertions(+), 13 deletions(-)

diff --git a/src/analyses/pthreadOnce.ml b/src/analyses/pthreadOnce.ml
index 30c7756089..96877bc485 100644
--- a/src/analyses/pthreadOnce.ml
+++ b/src/analyses/pthreadOnce.ml
@@ -59,14 +59,21 @@ struct
 
   let event man (e: Events.t) oman : D.t =
     match e with
+    | Events.EnterOnce { once_control; tf } when tf ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       let possible_vinfos = possible_vinfos ask once_control in
+       let unseen = List.filter (fun v -> not (Onces.mem v seen) && not (Onces.mem v active)) possible_vinfos in
+       match unseen with
+       | [] -> raise Deadcode
+       | [v] -> (Onces.add v active, seen)
+       | _ :: _ -> man.local)
     | Events.EnterOnce { once_control; tf } ->
       (let (active, seen) = man.local in
        let ask = Analyses.ask_of_man man in
        match possible_vinfos ask once_control with
-       | [v] ->
-         (Onces.add v active, seen)
-       | _ ->
-         man.local)
+       | [v] -> (Onces.add v active, seen)
+       | _ -> man.local)
     | Events.LeaveOnce { once_control } ->
       (let (active, seen) = man.local in
        let ask = Analyses.ask_of_man man in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 97dffe5d6c..93755e668c 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -262,15 +262,19 @@ struct
       let enter =
         let d' = S.event man (Events.EnterOnce { once_control;  tf = true }) man in
         let proc = tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d' in
-        let rec proc_man =
-          { man with
-            ask = (fun (type a) (q: a Queries.t) -> S.query proc_man q);
-            local = proc;
-          }
-        in
-        S.event proc_man (Events.LeaveOnce { once_control }) proc_man
+        if not (S.D.is_bot proc) then
+          let rec proc_man =
+            { man with
+              ask = (fun (type a) (q: a Queries.t) -> S.query proc_man q);
+              local = proc;
+            }
+          in
+          S.event proc_man (Events.LeaveOnce { once_control }) proc_man
+        else
+          S.D.bot ()
       in
       let not_enter =
+        (* Always possible, will never yield `Bot *)
         let d' = S.event man (Events.EnterOnce { once_control;  tf = false }) man in
         let rec d'_man =
           { man with
diff --git a/tests/regression/83-once/01-sanity.c b/tests/regression/83-once/01-sanity.c
index 3d7875e0c5..7b26a6cbcf 100644
--- a/tests/regression/83-once/01-sanity.c
+++ b/tests/regression/83-once/01-sanity.c
@@ -17,8 +17,11 @@ int main(void) {
   pthread_once(&once, fun);
   pthread_once(&once, fun);
 
-  // This fails if the (actual) case that it is not executed twice is ignored.
-  __goblint_check(g == 1); //TODO
+  __goblint_check(g < 2);
+
+  if(g = 1) {
+    __goblint_check(1); //Reachable
+  }
 
   return 0;
 }

From e255c60b92d4861248b0fc75351b4170ac665ea4 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 24 Jan 2025 18:24:05 +0100
Subject: [PATCH 24/38] Document `pthread_once`

---
 src/goblint_lib.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 415fb21605..1819331d6b 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -130,6 +130,7 @@ module RelationPriv = RelationPriv
 module ThreadEscape = ThreadEscape
 module PthreadSignals = PthreadSignals
 module ExtractPthread = ExtractPthread
+module PthreadOnce = PthreadOnce
 
 (** {2 Longjmp}
 

From 6df3ff8f4e7a15f033bee709bcbc1f92acc5a42b Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 24 Jan 2025 18:31:05 +0100
Subject: [PATCH 25/38] Add race checking

---
 src/analyses/pthreadOnce.ml          | 12 ++++++++++
 tests/regression/83-once/02-normal.c | 34 ++++++++++++++++++++++++++++
 2 files changed, 46 insertions(+)
 create mode 100644 tests/regression/83-once/02-normal.c

diff --git a/src/analyses/pthreadOnce.ml b/src/analyses/pthreadOnce.ml
index 96877bc485..fb91fae8f6 100644
--- a/src/analyses/pthreadOnce.ml
+++ b/src/analyses/pthreadOnce.ml
@@ -85,6 +85,18 @@ struct
        (active', seen'))
     | _ -> man.local
 
+  let access man _ = man.local
+
+  module A =
+  struct
+    include D
+    let name () = "onces"
+    let may_race (a1, s1) (a2, s2) =
+      (Onces.is_empty (Onces.inter a1 (Onces.union a2 s2))) && (Onces.is_empty (Onces.inter a2 (Onces.union a1 s1)))
+    let should_print f = true
+  end
+
+
   let threadenter man ~multiple lval f args =
     let (_, seen) = man.local in
     [Onces.empty (), seen]
diff --git a/tests/regression/83-once/02-normal.c b/tests/regression/83-once/02-normal.c
new file mode 100644
index 0000000000..bc6cab582d
--- /dev/null
+++ b/tests/regression/83-once/02-normal.c
@@ -0,0 +1,34 @@
+// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void fun() {
+  g = 42; //NORACE
+}
+
+
+void *t_fun(void *arg) {
+  pthread_once(&once, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 10; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_once(&once, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 11; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}

From 46d4904d5de9ea0caafc830648ce68350c74ccb1 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 27 Jan 2025 09:28:42 +0100
Subject: [PATCH 26/38] Add further example

---
 tests/regression/83-once/03-unknown.c | 44 +++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 tests/regression/83-once/03-unknown.c

diff --git a/tests/regression/83-once/03-unknown.c b/tests/regression/83-once/03-unknown.c
new file mode 100644
index 0000000000..42c43dab29
--- /dev/null
+++ b/tests/regression/83-once/03-unknown.c
@@ -0,0 +1,44 @@
+// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once1 = PTHREAD_ONCE_INIT;
+pthread_once_t once2; // PTHREAD_ONCE_INIT is `0`
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+pthread_once_t *ptr;
+
+void fun() {
+  g = 42; //RACE
+}
+
+
+void *t_fun(void *arg) {
+  pthread_once(ptr, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 10; //RACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  int top;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  ptr = &once1;
+
+  if(top) {
+    ptr = &once2;
+  }
+
+  pthread_once(ptr, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 11; //RACE
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}

From e31ce2ace101f7cb17412ce64e601a0609438cd3 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 27 Jan 2025 09:30:52 +0100
Subject: [PATCH 27/38] Only print onces in race info if one of the sets is
 non-empty

---
 src/analyses/pthreadOnce.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/pthreadOnce.ml b/src/analyses/pthreadOnce.ml
index fb91fae8f6..cc7dc3e611 100644
--- a/src/analyses/pthreadOnce.ml
+++ b/src/analyses/pthreadOnce.ml
@@ -93,7 +93,7 @@ struct
     let name () = "onces"
     let may_race (a1, s1) (a2, s2) =
       (Onces.is_empty (Onces.inter a1 (Onces.union a2 s2))) && (Onces.is_empty (Onces.inter a2 (Onces.union a1 s1)))
-    let should_print f = true
+    let should_print (a1, s1) = not (Onces.is_empty a1) || not (Onces.is_empty s1)
   end
 
 

From 9dae4045a8c539bc92d99ca1d919b2c36369a7d4 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 27 Jan 2025 09:56:01 +0100
Subject: [PATCH 28/38] Further test

---
 tests/regression/83-once/04-thread.c | 58 ++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 tests/regression/83-once/04-thread.c

diff --git a/tests/regression/83-once/04-thread.c b/tests/regression/83-once/04-thread.c
new file mode 100644
index 0000000000..c9522040c3
--- /dev/null
+++ b/tests/regression/83-once/04-thread.c
@@ -0,0 +1,58 @@
+// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+int h;
+int i;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_once_t i_once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mut;
+
+void *t_other(void* arg) {
+  g = 17; //RACE
+
+  pthread_mutex_lock(&mut);
+  i = 7; //NORACE
+  pthread_mutex_unlock(&mut);
+}
+
+void nesting() {
+  h = 5; //NORACE
+}
+
+void fun() {
+  // Even though this is only called inside the once, the accesses in the new thread and the accesses here can happen in parallel
+  // Checks that active is not passed to the created thread, but seen is passed
+  pthread_t tid = pthread_create(&tid, NULL, t_other, NULL);
+  g = 42; //RACE
+
+  h = 8; //NORACE
+  // Active onces get passed to the callee and back to the caller
+  nesting();
+  h = 12; //NORACE
+}
+
+void ifun() {
+  i = 11; //NORACE
+}
+
+void *t_fun(void *arg) {
+  pthread_once(&i_once, ifun);
+  pthread_once(&once, fun);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  int top;
+
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_once(&i_once, ifun);
+  pthread_once(&once, fun);
+
+  h = 5; //NORACE
+
+  return 0;
+}

From 010380e3b2cc53a8b68cf44e97210299d88155e6 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 27 Jan 2025 10:50:52 +0100
Subject: [PATCH 29/38] Remove workaround for #547

---
 conf/bench-yaml-validate.json                         |  1 -
 conf/bench-yaml.json                                  |  1 -
 conf/ldv-races.json                                   |  1 -
 conf/traces-rel.json                                  |  1 -
 lib/libc/stub/src/pthread.c                           | 11 -----------
 scripts/sv-comp/archive.sh                            |  1 -
 src/maingoblint.ml                                    |  3 ---
 tests/regression/03-practical/35-base-mutex-macos.t   |  2 +-
 tests/regression/71-doublelocking/07-rec-dyn-osx.c    |  3 +--
 .../regression/71-doublelocking/20-default-init-osx.c |  2 +-
 tests/regression/83-once/01-sanity.c                  |  2 +-
 tests/regression/83-once/02-normal.c                  |  2 +-
 tests/regression/83-once/03-unknown.c                 |  2 +-
 tests/regression/83-once/04-thread.c                  |  2 +-
 14 files changed, 7 insertions(+), 27 deletions(-)
 delete mode 100644 lib/libc/stub/src/pthread.c

diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
index 7b18371bd1..2fcdb418da 100644
--- a/conf/bench-yaml-validate.json
+++ b/conf/bench-yaml-validate.json
@@ -71,7 +71,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
index fd97b2c08c..52f0b33347 100644
--- a/conf/bench-yaml.json
+++ b/conf/bench-yaml.json
@@ -67,7 +67,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/ldv-races.json b/conf/ldv-races.json
index a06a6da610..da8355c7e8 100644
--- a/conf/ldv-races.json
+++ b/conf/ldv-races.json
@@ -1,7 +1,6 @@
 {
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/traces-rel.json b/conf/traces-rel.json
index 2b82a57554..fafb397a7f 100644
--- a/conf/traces-rel.json
+++ b/conf/traces-rel.json
@@ -83,7 +83,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/lib/libc/stub/src/pthread.c b/lib/libc/stub/src/pthread.c
deleted file mode 100644
index 1de6202b4b..0000000000
--- a/lib/libc/stub/src/pthread.c
+++ /dev/null
@@ -1,11 +0,0 @@
-#ifndef GOBLINT_NO_PTHREAD_ONCE
-#include <pthread.h>
-
-int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) __attribute__((goblint_stub));
-int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) {
-  // Not actually once, just call it
-  int top;
-  init_routine();
-  return top;
-}
-#endif
diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh
index aefac8f769..33ea1b4368 100755
--- a/scripts/sv-comp/archive.sh
+++ b/scripts/sv-comp/archive.sh
@@ -37,7 +37,6 @@ zip goblint/scripts/sv-comp/goblint.zip \
     goblint/lib/libc/stub/include/assert.h \
     goblint/lib/goblint/runtime/include/goblint.h \
     goblint/lib/libc/stub/src/stdlib.c \
-    goblint/lib/libc/stub/src/pthread.c \
     goblint/lib/sv-comp/stub/src/sv-comp.c \
     goblint/README.md \
     goblint/LICENSE
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index cb81ea0b86..c3f1d0f9ea 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -418,9 +418,6 @@ let preprocess_files () =
   if List.mem "c" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "stdlib.c") :: !extra_files;
 
-  if List.mem "pthread" (get_string_list "lib.activated") then
-    extra_files := find_custom_include (Fpath.v "pthread.c") :: !extra_files;
-
   if List.mem "sv-comp" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "sv-comp.c") :: !extra_files;
 
diff --git a/tests/regression/03-practical/35-base-mutex-macos.t b/tests/regression/03-practical/35-base-mutex-macos.t
index 1d8a184d4c..929d03eb5b 100644
--- a/tests/regression/03-practical/35-base-mutex-macos.t
+++ b/tests/regression/03-practical/35-base-mutex-macos.t
@@ -1,4 +1,4 @@
-  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+] -DGOBLINT_NO_PTHREAD_ONCE 35-base-mutex-macos.c
+  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed 35-base-mutex-macos.c
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
diff --git a/tests/regression/71-doublelocking/07-rec-dyn-osx.c b/tests/regression/71-doublelocking/07-rec-dyn-osx.c
index bb3cf65657..4059356371 100644
--- a/tests/regression/71-doublelocking/07-rec-dyn-osx.c
+++ b/tests/regression/71-doublelocking/07-rec-dyn-osx.c
@@ -1,6 +1,5 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, so MutexAttr.recursive_int remains at `2`, emulating the behavior of OS X.
-#define GOBLINT_NO_PTHREAD_ONCE 1
 typedef signed char __int8_t;
 typedef unsigned char __uint8_t;
 typedef short __int16_t;
diff --git a/tests/regression/71-doublelocking/20-default-init-osx.c b/tests/regression/71-doublelocking/20-default-init-osx.c
index 4d3ec1f8d7..eaa6ec58be 100644
--- a/tests/regression/71-doublelocking/20-default-init-osx.c
+++ b/tests/regression/71-doublelocking/20-default-init-osx.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, to emulate the behavior of OS X.
 #define NULL ((void *)0)
 typedef signed char __int8_t;
diff --git a/tests/regression/83-once/01-sanity.c b/tests/regression/83-once/01-sanity.c
index 7b26a6cbcf..8a26012571 100644
--- a/tests/regression/83-once/01-sanity.c
+++ b/tests/regression/83-once/01-sanity.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/83-once/02-normal.c b/tests/regression/83-once/02-normal.c
index bc6cab582d..ee10a7d6b4 100644
--- a/tests/regression/83-once/02-normal.c
+++ b/tests/regression/83-once/02-normal.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/83-once/03-unknown.c b/tests/regression/83-once/03-unknown.c
index 42c43dab29..16cb2c5a12 100644
--- a/tests/regression/83-once/03-unknown.c
+++ b/tests/regression/83-once/03-unknown.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 
diff --git a/tests/regression/83-once/04-thread.c b/tests/regression/83-once/04-thread.c
index c9522040c3..c467bacc22 100644
--- a/tests/regression/83-once/04-thread.c
+++ b/tests/regression/83-once/04-thread.c
@@ -1,4 +1,4 @@
-// PARAM: --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --set ana.activated[+] pthreadOnce
+// PARAM: --set ana.activated[+] pthreadOnce
 #include <pthread.h>
 #include <stdio.h>
 

From aa6850912076728e8b31708d0c6359bab575d39e Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 29 Jan 2025 11:11:17 +0100
Subject: [PATCH 30/38] Use Seq instead of constructing from scratch

---
 src/analyses/pthreadBarriers.ml | 29 ++++++++++++++++++++---------
 src/domain/disjointDomain.ml    |  2 ++
 src/domain/setDomain.ml         |  8 ++++++++
 3 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
index 1cea151fed..cc51c163c6 100644
--- a/src/analyses/pthreadBarriers.ml
+++ b/src/analyses/pthreadBarriers.ml
@@ -52,6 +52,19 @@ struct
     Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
 
   let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let exists_k pred k waiters =
+      let k_product elems =
+        let rec doit k =
+          if k = 1 then
+            Seq.map (Seq.return) elems
+          else
+            let arg = doit (k-1) in
+            Seq.map_product (Seq.cons) elems arg
+        in
+        doit k
+      in
+      Seq.exists pred (k_product (Waiters.to_seq waiters))
+    in
     let desc = LF.find f in
     match desc.special arglist with
     | BarrierWait barrier ->
@@ -88,16 +101,14 @@ struct
                   let must =
                     let waiters = Waiters.elements relevant_waiters in
                     let min_cap = Z.to_int min_cap in
-                    let lists = List.init (min_cap - 1) (fun _ -> waiters) in
-                    let candidates = BatList.n_cartesian_product lists in
-                    let can_proceed = List.exists (fun candidate ->
-                        let rec do_it = function
-                          | [] -> true
-                          | x::xs -> List.for_all (fun y -> MHPplusLock.mhp x y) xs  && do_it xs
-                        in
-                        do_it candidate
-                      ) candidates
+                    let can_proceed_pred seq =
+                      let rec doit seq = match Seq.uncons seq with
+                        | None -> true
+                        | Some (h, t) -> Seq.for_all (MHPplusLock.mhp h) t && doit t
+                      in
+                      doit seq
                     in
+                    let can_proceed = exists_k can_proceed_pred (min_cap - 1) relevant_waiters in
                     if not can_proceed then raise Analyses.Deadcode;
                     (* limit to this case to avoid having to construct all permutations above *)
                     if BatList.compare_length_with waiters (min_cap - 1) = 0 then
diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml
index 3e02c1d3a0..35a730a4d5 100644
--- a/src/domain/disjointDomain.ml
+++ b/src/domain/disjointDomain.ml
@@ -117,6 +117,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f m = fold (fun e acc ->
       add (f e) acc
     ) m (empty ()) (* no intermediate lists *)
@@ -323,6 +324,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f s = fold (fun e acc ->
       add (f e) acc
     ) s (empty ()) (* no intermediate lists *)
diff --git a/src/domain/setDomain.ml b/src/domain/setDomain.ml
index c552363f3d..e11c8182de 100644
--- a/src/domain/setDomain.ml
+++ b/src/domain/setDomain.ml
@@ -95,6 +95,12 @@ sig
       On set abstractions this lists only canonical elements,
       not all subsumed elements. *)
 
+  val to_seq: t -> elt Seq.t
+  (** See {!Set.S.to_seq}.
+
+      On set abstractions this lists only canonical elements,
+      not all subsumed elements. *)
+
   val of_list: elt list -> t
 
   val min_elt: t -> elt
@@ -332,6 +338,7 @@ struct
   let exists f = schema_default true (S.exists f)
   let filter f = schema (fun t -> `Lifted (S.filter f t)) "filter on `Top"
   let elements = schema S.elements "elements on `Top"
+  let to_seq = schema S.to_seq "to_seq on `Top"
   let of_list xs = `Lifted (S.of_list xs)
   let cardinal = schema S.cardinal "cardinal on `Top"
   let min_elt = schema S.min_elt "min_elt on `Top"
@@ -471,6 +478,7 @@ struct
   let mem e e' = E.leq e e'
   let choose e = e
   let elements e = [e]
+  let to_seq e = Seq.return e
   let remove e e' =
     if E.leq e' e then
       E.bot () (* NB! strong removal *)

From 31323cd214123f40f3eac63a33a72298a84d2c73 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 30 Jan 2025 10:53:48 +0100
Subject: [PATCH 31/38] Add switch to not use mutexes in race detection

---
 src/analyses/mutexAnalysis.ml  |  2 ++
 src/config/options.schema.json | 13 +++++++++++++
 2 files changed, 15 insertions(+)

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index c712ca9644..996eca9954 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/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
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 39c863ad49..a2aa7b8feb 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1105,6 +1105,19 @@
               "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
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false

From d9bd9cadaec38dbe6f5b5a75d767864a968a2fbe Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 30 Jan 2025 11:28:50 +0100
Subject: [PATCH 32/38] Add option to disable thread digest

---
 src/analyses/threadId.ml       | 5 ++++-
 src/config/options.schema.json | 6 ++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 53d070a056..d9724b2c2e 100644
--- a/src/analyses/threadId.ml
+++ b/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
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index a2aa7b8feb..ecda257c92 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1115,6 +1115,12 @@
                   "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
                 }
               },
               "additionalProperties": false

From 164e0c9ec341129755ffd644122592e9812bca84 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 30 Jan 2025 11:42:51 +0100
Subject: [PATCH 33/38] Add option for freshness

---
 src/analyses/mallocFresh.ml    | 4 +++-
 src/config/options.schema.json | 6 ++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index c226d7e6ce..4e7bd84571 100644
--- a/src/analyses/mallocFresh.ml
+++ b/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) =
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index ecda257c92..07d6bf974f 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1121,6 +1121,12 @@
                   "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
                 }
               },
               "additionalProperties": false

From 7ae5e0798b650160e46c9e209f3d98f0e875b4bc Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 30 Jan 2025 11:47:41 +0100
Subject: [PATCH 34/38] Add toggle for region / symbLocks

---
 src/analyses/region.ml         |  5 ++++-
 src/analyses/symbLocks.ml      |  4 +++-
 src/config/options.schema.json | 12 ++++++++++++
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 0fb61059e2..d02df20d0d 100644
--- a/src/analyses/region.ml
+++ b/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 *)
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 0850fac317..9cf212b6b9 100644
--- a/src/analyses/symbLocks.ml
+++ b/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
 
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 07d6bf974f..e27e89ab92 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1127,6 +1127,18 @@
                   "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
                 }
               },
               "additionalProperties": false

From 1273af27c33c1e42a7707c543df00e789ad6fb8d Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 31 Jan 2025 14:10:38 +0100
Subject: [PATCH 35/38] Thread flag option

---
 src/analyses/threadFlag.ml     | 4 +++-
 src/config/options.schema.json | 6 ++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 1e0ff7db9f..454ea28961 100644
--- a/src/analyses/threadFlag.ml
+++ b/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 _ =
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index e27e89ab92..808f11eaa8 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1139,6 +1139,12 @@
                   "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
                 }
               },
               "additionalProperties": false

From aa976793a9b847521a204f9ce05ffa13a96f45a6 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 31 Jan 2025 14:16:51 +0100
Subject: [PATCH 36/38] Add `tid` and `joins` digest

---
 src/cdomains/mHP.ml            | 12 +++++++-----
 src/config/options.schema.json | 12 ++++++++++++
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index afaf6d67e3..18aa1719fd 100644
--- a/src/cdomains/mHP.ml
+++ b/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
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 808f11eaa8..6bcab0d253 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1145,6 +1145,18 @@
                   "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

From 4c2d8a38cafeb41214db369ad384fbbfb0f6459f Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 31 Jan 2025 14:35:49 +0100
Subject: [PATCH 37/38] Add configs for experiments

---
 conf/race-digests/full.json           | 118 ++++++++++++++++++++++++
 conf/race-digests/mutex-only.json     | 128 ++++++++++++++++++++++++++
 conf/race-digests/none.json           | 128 ++++++++++++++++++++++++++
 conf/race-digests/tid+mutex+join.json | 128 ++++++++++++++++++++++++++
 conf/race-digests/tid+mutex.json      | 128 ++++++++++++++++++++++++++
 conf/race-digests/tid-only.json       | 128 ++++++++++++++++++++++++++
 6 files changed, 758 insertions(+)
 create mode 100644 conf/race-digests/full.json
 create mode 100644 conf/race-digests/mutex-only.json
 create mode 100644 conf/race-digests/none.json
 create mode 100644 conf/race-digests/tid+mutex+join.json
 create mode 100644 conf/race-digests/tid+mutex.json
 create mode 100644 conf/race-digests/tid-only.json

diff --git a/conf/race-digests/full.json b/conf/race-digests/full.json
new file mode 100644
index 0000000000..dedc393ba1
--- /dev/null
+++ b/conf/race-digests/full.json
@@ -0,0 +1,118 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/mutex-only.json b/conf/race-digests/mutex-only.json
new file mode 100644
index 0000000000..864dfeb9be
--- /dev/null
+++ b/conf/race-digests/mutex-only.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "thread": false,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/none.json b/conf/race-digests/none.json
new file mode 100644
index 0000000000..533e0b8a0d
--- /dev/null
+++ b/conf/race-digests/none.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+        "thread": false,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tid+mutex+join.json b/conf/race-digests/tid+mutex+join.json
new file mode 100644
index 0000000000..d24fd6603a
--- /dev/null
+++ b/conf/race-digests/tid+mutex+join.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "thread": false,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": true,
+        "join" : true
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tid+mutex.json b/conf/race-digests/tid+mutex.json
new file mode 100644
index 0000000000..98e4732913
--- /dev/null
+++ b/conf/race-digests/tid+mutex.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "thread": false,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": true,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tid-only.json b/conf/race-digests/tid-only.json
new file mode 100644
index 0000000000..90acc8fd5a
--- /dev/null
+++ b/conf/race-digests/tid-only.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+        "thread": false,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": true,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

From cea4416735bea146ae3722366dbd0bb50f1d5fc8 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 31 Jan 2025 17:40:33 +0100
Subject: [PATCH 38/38] Add two more configs

---
 conf/race-digests/full-minus-region.json | 128 +++++++++++++++++++++++
 conf/race-digests/mutex+threadflag.json  | 128 +++++++++++++++++++++++
 2 files changed, 256 insertions(+)
 create mode 100644 conf/race-digests/full-minus-region.json
 create mode 100644 conf/race-digests/mutex+threadflag.json

diff --git a/conf/race-digests/full-minus-region.json b/conf/race-digests/full-minus-region.json
new file mode 100644
index 0000000000..ed045fa6f2
--- /dev/null
+++ b/conf/race-digests/full-minus-region.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "thread": true,
+        "fresh": true,
+        "region": false,
+        "symb_locks": true,
+        "threadflag": true,
+        "tid": true,
+        "join" : true
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/mutex+threadflag.json b/conf/race-digests/mutex+threadflag.json
new file mode 100644
index 0000000000..2e0049736c
--- /dev/null
+++ b/conf/race-digests/mutex+threadflag.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "thread": false,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": true,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}