From 52055b1c4239929f89e40f280303164e6059f4aa Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 14 Aug 2024 19:18:28 +0300
Subject: [PATCH 01/17] Improve history thread ID may_create for unique threads

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index fff6734f27..1c65b53b75 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -150,8 +150,11 @@ struct
       let cdef_ancestor = P.common_suffix p p' in
       P.equal p cdef_ancestor
 
-  let may_create (p,s) (p',s') =
-    S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s')
+  let may_create ((p, s) as t) ((p', s') as t') =
+    if is_unique t' then
+      is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
+    else
+      S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s')
 
   let compose ((p, s) as current) ni =
     if BatList.mem_cmp Base.compare ni p then (

From baa497a83d95d6a8071ab269807c72f3fc30d6f0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 14 Aug 2024 19:27:33 +0300
Subject: [PATCH 02/17] Improve history thread ID may_create for incompatible
 prefixes

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 1c65b53b75..c6b0d664e5 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -154,7 +154,9 @@ struct
     if is_unique t' then
       is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
     else
-      S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s')
+      let cdef_ancestor = P.common_suffix p p' in
+      (P.equal cdef_ancestor p || P.equal cdef_ancestor p') && (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
+      S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
 
   let compose ((p, s) as current) ni =
     if BatList.mem_cmp Base.compare ni p then (

From 4f6a7637b8d0dc723fe382f94bed6c822cd4a2ce Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 14 Aug 2024 19:41:52 +0300
Subject: [PATCH 03/17] Improve history thread ID may_create for both
 non-unique threads

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index c6b0d664e5..ff5ccb56f6 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -153,10 +153,16 @@ struct
   let may_create ((p, s) as t) ((p', s') as t') =
     if is_unique t' then
       is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
-    else
+    else if is_unique t then ( (* t' is already non-unique *)
       let cdef_ancestor = P.common_suffix p p' in
       (P.equal cdef_ancestor p || P.equal cdef_ancestor p') && (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
       S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
+    )
+    else ( (* both are non-unique *)
+      let cdef_ancestor = P.common_suffix p p' in
+      P.equal cdef_ancestor p' && (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
+      S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
+    )
 
   let compose ((p, s) as current) ni =
     if BatList.mem_cmp Base.compare ni p then (

From dbd487438a573a845c449e7a5619a70cccdb6cf9 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 14 Aug 2024 19:53:14 +0300
Subject: [PATCH 04/17] Improve history thread ID may_create for first unique
 thread extension

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index ff5ccb56f6..c52852a47a 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -155,8 +155,15 @@ struct
       is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
     else if is_unique t then ( (* t' is already non-unique *)
       let cdef_ancestor = P.common_suffix p p' in
-      (P.equal cdef_ancestor p || P.equal cdef_ancestor p') && (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
-      S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
+      if P.equal cdef_ancestor p then ( (* p is prefix of p' *)
+        (* TODO: avoid length calculations? *)
+        let dp = BatList.take (List.length p' - List.length cdef_ancestor) p' in (* elements added to prefix *)
+        S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *)
+      )
+      else ( (* p is not prefix of p' *)
+        P.equal cdef_ancestor p' && (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
+        S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
+      )
     )
     else ( (* both are non-unique *)
       let cdef_ancestor = P.common_suffix p p' in

From c2c596f43798f081cbeadd6997c7a9b07da43bba Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 14 Aug 2024 20:00:49 +0300
Subject: [PATCH 05/17] Improve history thread ID may_create for first unique
 thread prefix shortening

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index c52852a47a..47c04e1fab 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -160,10 +160,14 @@ struct
         let dp = BatList.take (List.length p' - List.length cdef_ancestor) p' in (* elements added to prefix *)
         S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *)
       )
-      else ( (* p is not prefix of p' *)
-        P.equal cdef_ancestor p' && (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
-        S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
+      else if P.equal cdef_ancestor p' then ( (* p is not prefix of p', but p' is prefix of p *)
+        (* TODO: avoid length calculations? *)
+        let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *)
+        S.subset (S.of_list dp') s' (* removed elements become part of set, must be contained, because compose can only add them *)
+        (* TODO: also check disjointness *)
       )
+      else
+        false (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
     )
     else ( (* both are non-unique *)
       let cdef_ancestor = P.common_suffix p p' in

From bb2fa08788ba8fbbd76128ca02ea7689418ce21e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 14 Aug 2024 20:04:49 +0300
Subject: [PATCH 06/17] Remove history thread ID may_create for first unique
 thread prefix TODO

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 47c04e1fab..31ea29d425 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -164,7 +164,7 @@ struct
         (* TODO: avoid length calculations? *)
         let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *)
         S.subset (S.of_list dp') s' (* removed elements become part of set, must be contained, because compose can only add them *)
-        (* TODO: also check disjointness *)
+        (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *)
       )
       else
         false (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)

From f3dda0e7e8eb174792733b680367f51d8f9418b6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 11:44:30 +0300
Subject: [PATCH 07/17] Add history thread ID domain unit tests

---
 tests/unit/cdomains/threadIdDomainTest.ml | 104 ++++++++++++++++++++++
 tests/unit/mainTest.ml                    |   1 +
 2 files changed, 105 insertions(+)
 create mode 100644 tests/unit/cdomains/threadIdDomainTest.ml

diff --git a/tests/unit/cdomains/threadIdDomainTest.ml b/tests/unit/cdomains/threadIdDomainTest.ml
new file mode 100644
index 0000000000..2b8b60df5a
--- /dev/null
+++ b/tests/unit/cdomains/threadIdDomainTest.ml
@@ -0,0 +1,104 @@
+open OUnit2
+open Goblint_lib
+open ThreadIdDomain
+
+module History = History (FunNode)
+
+let main = GoblintCil.makeGlobalVar "main" GoblintCil.voidType
+let a = GoblintCil.makeGlobalVar "a" GoblintCil.voidType
+let b = GoblintCil.makeGlobalVar "b" GoblintCil.voidType
+let c = GoblintCil.makeGlobalVar "c" GoblintCil.voidType
+let d = GoblintCil.makeGlobalVar "d" GoblintCil.voidType
+
+let main: History.t = History.threadinit main ~multiple:false
+
+let (>>) (parent: History.t) (v: GoblintCil.varinfo): History.t =
+  match History.threadenter ~multiple:false (parent, History.D.bot ()) MyCFG.dummy_node None v with
+  | [child] -> child
+  | _ -> assert false
+
+let test_history_is_must_parent _ =
+  let open History in
+  let assert_equal = assert_equal ~printer:string_of_bool in
+
+  (* non-unique is not must parent *)
+  assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a));
+  assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a >> a));
+  assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a >> b));
+
+  (* unique is not self-parent *)
+  assert_equal false (is_must_parent main main);
+  assert_equal false (is_must_parent (main >> a) (main >> a));
+  assert_equal false (is_must_parent (main >> a >> b) (main >> a >> b));
+
+  (* unique is must parent if prefix *)
+  assert_equal true (is_must_parent main (main >> a));
+  assert_equal true (is_must_parent main (main >> a >> a));
+  assert_equal true (is_must_parent main (main >> a >> b));
+  assert_equal true (is_must_parent (main >> a) (main >> a >> b));
+  assert_equal false (is_must_parent (main >> a) main);
+  assert_equal false (is_must_parent (main >> b) (main >> a >> b));
+  assert_equal false (is_must_parent (main >> a) (main >> b >> a));
+  assert_equal false (is_must_parent (main >> a) (main >> a >> a)); (* may be created by just main (non-uniquely) *)
+  ()
+
+let test_history_may_create _ =
+  let open History in
+  let assert_equal = assert_equal ~printer:string_of_bool in
+
+  (* unique may only be created by unique (prefix) *)
+  assert_equal true (may_create main (main >> a));
+  assert_equal true (may_create main (main >> a >> b));
+  assert_equal true (may_create (main >> a) (main >> a >> b));
+  assert_equal false (may_create (main >> a) (main >> a));
+  assert_equal false (may_create (main >> b) (main >> a >> b));
+  assert_equal false (may_create (main >> a >> a) (main >> a >> b));
+
+  (* unique creates non-unique and is prefix: added elements cannot be in prefix *)
+  assert_equal true (may_create main (main >> a >> a));
+  assert_equal true (may_create main (main >> a >> b >> b));
+  assert_equal true (may_create (main >> a) (main >> a >> b >> b));
+  (* TODO: added elements condition always true by construction in tests? *)
+
+  (* non-unique created by unique and is prefix: removed elements must be in set *)
+  assert_equal true (may_create (main >> a) (main >> a >> a));
+  assert_equal true (may_create (main >> a >> b) (main >> a >> b >> b));
+  assert_equal true (may_create (main >> a >> b) (main >> a >> b >> a));
+  assert_equal false (may_create (main >> a >> b) (main >> a >> a));
+  assert_equal false (may_create (main >> a >> b) (main >> b >> b));
+
+  (* unique creates non-unique and prefixes are incompatible *)
+  assert_equal false (may_create (main >> a) (main >> b >> a >> a));
+  assert_equal false (may_create (main >> a >> b) (main >> b >> a >> c >> c));
+  assert_equal false (may_create (main >> a >> b) (main >> a >> c >> d >> d));
+
+  (* non-unique creates non-unique: prefix must not lengthen *)
+  assert_equal false (may_create (main >> a >> a) (main >> a >> b >> b));
+  assert_equal false (may_create (main >> a >> a) (main >> b >> a >> a));
+  (* non-unique creates non-unique: prefix must be compatible *)
+  assert_equal false (may_create (main >> a >> b >> c >> c) (main >> b >> a >> c >> c));
+  (* non-unique creates non-unique: elements must not be removed *)
+  assert_equal false (may_create (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *)
+  assert_equal false (may_create (main >> a >> b >> b) (main >> b >> b)); (* from prefix *)
+  (* non-unique creates non-unique: removed elements and set must be in new set *)
+  (* assert_equal false (may_create (main >> a >> b >> c >> c) (main >> a >> c >> c)); *)
+  (* TODO: cannot test due because by construction after prefix check? *)
+  (* non-unique creates non-unique *)
+  assert_equal true (may_create (main >> a >> a) (main >> a >> a));
+  assert_equal true (may_create (main >> a >> a) (main >> a >> a >> b));
+  assert_equal true (may_create (main >> a >> a) (main >> a >> b >> a));
+  assert_equal true (may_create (main >> a >> a) (main >> a >> b >> c >> a));
+  assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> b));
+  assert_equal true (may_create (main >> a >> b >> b) (main >> a >> a >> b));
+  assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> a));
+  assert_equal true (may_create (main >> a >> b >> b) (main >> b >> b >> a));
+  assert_equal true (may_create (main >> a >> b >> b) (main >> b >> a >> b));
+  ()
+
+let tests =
+  "threadIdDomainTest" >::: [
+    "history" >::: [
+      "is_must_parent" >:: test_history_is_must_parent;
+      "may_create" >:: test_history_may_create;
+    ]
+  ]
diff --git a/tests/unit/mainTest.ml b/tests/unit/mainTest.ml
index 4f071ea25c..44f1096655 100644
--- a/tests/unit/mainTest.ml
+++ b/tests/unit/mainTest.ml
@@ -13,6 +13,7 @@ let all_tests =
     (* etc *)
     "domaintest" >::: QCheck_ounit.to_ounit2_test_list Maindomaintest.all_testsuite;
     IntOpsTest.tests;
+    ThreadIdDomainTest.tests;
   ]
 
 let () =

From be2b3e2011f2253006237d96a9b0e7f7c971ccfb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 11:44:44 +0300
Subject: [PATCH 08/17] Add TODOs to history thread ID may_create

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 31ea29d425..489e5b572e 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -159,6 +159,7 @@ struct
         (* TODO: avoid length calculations? *)
         let dp = BatList.take (List.length p' - List.length cdef_ancestor) p' in (* elements added to prefix *)
         S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *)
+        (* TODO: no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway? *)
       )
       else if P.equal cdef_ancestor p' then ( (* p is not prefix of p', but p' is prefix of p *)
         (* TODO: avoid length calculations? *)
@@ -173,6 +174,7 @@ struct
       let cdef_ancestor = P.common_suffix p p' in
       P.equal cdef_ancestor p' && (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
       S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
+      (* TODO: can just subset s' thanks to well-formedness conditions? *)
     )
 
   let compose ((p, s) as current) ni =

From 73a22d7b3eca43f8f1cd067dd4752a70f1b8dd8c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 12:25:32 +0300
Subject: [PATCH 09/17] Do additional simplifications to history thread ID
 may_create

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 20 +++++++++++++-------
 tests/unit/cdomains/threadIdDomainTest.ml    |  2 ++
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 489e5b572e..e7b915df3d 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -156,10 +156,10 @@ struct
     else if is_unique t then ( (* t' is already non-unique *)
       let cdef_ancestor = P.common_suffix p p' in
       if P.equal cdef_ancestor p then ( (* p is prefix of p' *)
-        (* TODO: avoid length calculations? *)
-        let dp = BatList.take (List.length p' - List.length cdef_ancestor) p' in (* elements added to prefix *)
-        S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *)
-        (* TODO: no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway? *)
+        (* let dp = elements added to prefix *)
+        (* S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *) *)
+        (* no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway *)
+        true
       )
       else if P.equal cdef_ancestor p' then ( (* p is not prefix of p', but p' is prefix of p *)
         (* TODO: avoid length calculations? *)
@@ -172,9 +172,15 @@ struct
     )
     else ( (* both are non-unique *)
       let cdef_ancestor = P.common_suffix p p' in
-      P.equal cdef_ancestor p' && (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
-      S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s') (* elements must be contained, because compose can only add them *)
-      (* TODO: can just subset s' thanks to well-formedness conditions? *)
+      if P.equal cdef_ancestor p' then ( (* p' is prefix of p *)
+        (* TODO: avoid length calculations? *)
+        let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *)
+        S.subset (S.union (S.of_list dp') s) s' (* elements must be contained, because compose can only add them *)
+        (* can just subset s' thanks to well-formedness conditions *)
+        (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *)
+      )
+      else
+        false (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
     )
 
   let compose ((p, s) as current) ni =
diff --git a/tests/unit/cdomains/threadIdDomainTest.ml b/tests/unit/cdomains/threadIdDomainTest.ml
index 2b8b60df5a..22b30c8c07 100644
--- a/tests/unit/cdomains/threadIdDomainTest.ml
+++ b/tests/unit/cdomains/threadIdDomainTest.ml
@@ -93,6 +93,8 @@ let test_history_may_create _ =
   assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> a));
   assert_equal true (may_create (main >> a >> b >> b) (main >> b >> b >> a));
   assert_equal true (may_create (main >> a >> b >> b) (main >> b >> a >> b));
+
+  (* 4f6a7637b8d0dc723fe382f94bed6c822cd4a2ce passes all... *)
   ()
 
 let tests =

From b6fd349f56fa122e0256a31af081bc297e0d9791 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 12:45:26 +0300
Subject: [PATCH 10/17] Optimize history thread IDs using
 GobList.remove_common_prefix

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 34 +++++++++-----------
 src/common/domains/printable.ml              | 10 ------
 src/util/std/gobList.ml                      |  5 +++
 3 files changed, 20 insertions(+), 29 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index e7b915df3d..882717f01a 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -147,40 +147,36 @@ struct
       (* We do not consider a thread its own parent *)
       false
     else
-      let cdef_ancestor = P.common_suffix p p' in
-      P.equal p cdef_ancestor
+      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with
+      | [], _ -> true
+      | _ :: _, _ -> false
 
   let may_create ((p, s) as t) ((p', s') as t') =
     if is_unique t' then
       is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
     else if is_unique t then ( (* t' is already non-unique *)
-      let cdef_ancestor = P.common_suffix p p' in
-      if P.equal cdef_ancestor p then ( (* p is prefix of p' *)
-        (* let dp = elements added to prefix *)
+      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with
+      | [], dp -> (* p is prefix of p' *)
+        (* dp = elements added to prefix *)
         (* S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *) *)
         (* no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway *)
         true
-      )
-      else if P.equal cdef_ancestor p' then ( (* p is not prefix of p', but p' is prefix of p *)
-        (* TODO: avoid length calculations? *)
-        let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *)
+      | dp', [] -> (* p is not prefix of p', but p' is prefix of p *)
+        (* dp' = elements removed from prefix *)
         S.subset (S.of_list dp') s' (* removed elements become part of set, must be contained, because compose can only add them *)
         (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *)
-      )
-      else
-        false (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
+      | _ :: _, _ :: _ -> (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
+        false
     )
     else ( (* both are non-unique *)
-      let cdef_ancestor = P.common_suffix p p' in
-      if P.equal cdef_ancestor p' then ( (* p' is prefix of p *)
-        (* TODO: avoid length calculations? *)
-        let dp' = BatList.take (List.length p - List.length cdef_ancestor) p in (* elements removed from prefix *)
+      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with
+      | dp', [] -> (* p' is prefix of p *)
+        (* dp' = elements removed from prefix *)
         S.subset (S.union (S.of_list dp') s) s' (* elements must be contained, because compose can only add them *)
         (* can just subset s' thanks to well-formedness conditions *)
         (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *)
-      )
-      else
-        false (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
+      | _, _ :: _ -> (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
+        false
     )
 
   let compose ((p, s) as current) ni =
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index 93d3f99edc..9ef9e7e79a 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -631,16 +631,6 @@ struct
     BatPrintf.fprintf f "<value>\n<map>\n";
     loop 0 xs;
     BatPrintf.fprintf f "</map>\n</value>\n"
-
-  let common_prefix x y =
-    let rec helper acc x y =
-      match x,y with
-      | x::xs, y::ys when Base.equal x y-> helper (x::acc) xs ys
-      | _ -> acc
-    in
-    List.rev (helper [] x y)
-
-  let common_suffix x y = List.rev (common_prefix (List.rev x) (List.rev y))
 end
 
 module type ChainParams = sig
diff --git a/src/util/std/gobList.ml b/src/util/std/gobList.ml
index 3743b0127e..f0b3b99932 100644
--- a/src/util/std/gobList.ml
+++ b/src/util/std/gobList.ml
@@ -30,6 +30,11 @@ let rec fold_while_some (f : 'a -> 'b -> 'a option) (acc: 'a) (xs: 'b list): 'a
 
 let equal = List.eq
 
+let rec remove_common_prefix eq l1 l2 =
+  match l1, l2 with
+  | x1 :: l1', x2 :: l2' when eq x1 x2 -> remove_common_prefix eq l1' l2'
+  | _, _ -> (l1, l2)
+
 (** Given a predicate and a list, returns two lists [(l1, l2)].
     [l1] contains the prefix of the list until the last element that satisfies the predicate, [l2] contains all subsequent elements. The order of elements is preserved. *)
 let until_last_with (pred: 'a -> bool) (xs: 'a list) =

From 31d22ef99c1ecab70c7de5ff3cdee8001e039cee Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 13:12:46 +0300
Subject: [PATCH 11/17] Simplify history thread ID may_create

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 36 +++++++-------------
 src/util/std/gobList.ml                      | 10 ++++++
 2 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 882717f01a..466b8ae72b 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -147,36 +147,26 @@ struct
       (* We do not consider a thread its own parent *)
       false
     else
-      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with
+      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
       | [], _ -> true
       | _ :: _, _ -> false
 
   let may_create ((p, s) as t) ((p', s') as t') =
     if is_unique t' then
       is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
-    else if is_unique t then ( (* t' is already non-unique *)
-      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with
-      | [], dp -> (* p is prefix of p' *)
-        (* dp = elements added to prefix *)
-        (* S.disjoint (S.of_list p) (S.union (S.of_list dp) s') (* added elements must not appear in p, otherwise compose would become shorter and non-unique *) *)
-        (* no need to check disjointness, because if t' is well-formed, then dp and s' won't have anything from cdef_ancestor anyway *)
-        true
-      | dp', [] -> (* p is not prefix of p', but p' is prefix of p *)
-        (* dp' = elements removed from prefix *)
-        S.subset (S.of_list dp') s' (* removed elements become part of set, must be contained, because compose can only add them *)
-        (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *)
-      | _ :: _, _ :: _ -> (* prefixes must not be incompatible (one is prefix of another or vice versa), because compose cannot fix incompatibility there *)
-        false
-    )
-    else ( (* both are non-unique *)
-      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with
+    else ( (* t' is already non-unique (but doesn't matter) *)
+      match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
+      | [], dp when is_unique t -> (* p is prefix of p' *)
+        (* dp = elements added to prefix (reversed, but doesn't matter) *)
+        true (* all elements are contained: p is prefix of p' and s is empty (due to uniqueness) *)
       | dp', [] -> (* p' is prefix of p *)
-        (* dp' = elements removed from prefix *)
-        S.subset (S.union (S.of_list dp') s) s' (* elements must be contained, because compose can only add them *)
-        (* can just subset s' thanks to well-formedness conditions *)
-        (* no need to check disjointness, because if t' is well-formed, then s' won't have anything from cdef_ancestor anyway *)
-      | _, _ :: _ -> (* p' must be prefix of p, because non-unique compose can only shorten prefix *)
-        false
+        (* dp' = elements removed from prefix (reversed, but doesn't matter) *)
+        S.subset (S.of_list dp') s' && (* removed elements become part of set, must be contained, because compose can only add them *)
+        S.subset s s' (* set elements must be contained, because compose can only add them *)
+      | [], _ :: _ -> (* p is strict prefix of p' and t is non-unique *)
+        false (* composing to non-unique cannot lengthen prefix *)
+      | _ :: _, _ :: _ -> (* prefixes are incompatible *)
+        false (* composing cannot fix incompatibility there *)
     )
 
   let compose ((p, s) as current) ni =
diff --git a/src/util/std/gobList.ml b/src/util/std/gobList.ml
index f0b3b99932..bcf030cb05 100644
--- a/src/util/std/gobList.ml
+++ b/src/util/std/gobList.ml
@@ -30,6 +30,16 @@ let rec fold_while_some (f : 'a -> 'b -> 'a option) (acc: 'a) (xs: 'b list): 'a
 
 let equal = List.eq
 
+(** [remove_common_prefix eq l1 l2] removes the common prefix ([p]) of [l1] and [l2] and
+    returns the rest of both lists a pair [(l1', l2')].
+    Formally, [p @ l1' = l1] and [p @ l2' = l2] such that [p] has maximal length.
+
+    This can be used to check being a prefix in both directions simultaneously:
+    - if [l1' = []], then [l1] is a prefix of [l2],
+    - if [l2' = []], then [l2] is a prefix of [l1].
+    In other cases, the common prefix is not returned (i.e. reconstructed) for efficiency reasons.
+
+    @param eq equality predicate for elements *)
 let rec remove_common_prefix eq l1 l2 =
   match l1, l2 with
   | x1 :: l1', x2 :: l2' when eq x1 x2 -> remove_common_prefix eq l1' l2'

From 5f1b296dec23ce3418737c7f956f71e36d1fdc7f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 13:17:13 +0300
Subject: [PATCH 12/17] Clean up history thread ID is_must_parent

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 466b8ae72b..7e208cba0e 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -140,16 +140,16 @@ struct
   let is_unique (_, s) =
     S.is_empty s
 
-  let is_must_parent (p,s) (p',s') =
-    if not (S.is_empty s) then
+  let is_must_parent ((p, s) as t) ((p', s') as t') =
+    if not (is_unique t) then
       false
-    else if P.equal p' p && S.is_empty s' then (* s is already empty *)
-      (* We do not consider a thread its own parent *)
-      false
-    else
+    else if is_unique t' && P.equal p p' then (* t is already unique, so no need to compare sets *)
+      false (* thread is not its own parent *)
+    else ( (* both are unique, but different *)
       match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
-      | [], _ -> true
+      | [], _ -> true (* p is prefix of p' *)
       | _ :: _, _ -> false
+    )
 
   let may_create ((p, s) as t) ((p', s') as t') =
     if is_unique t' then

From 9744751aeb77f85995124fe088b68d90dda4db60 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 13:20:49 +0300
Subject: [PATCH 13/17] Fix GobList.remove_common_prefix doc indentation

---
 src/util/std/gobList.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/util/std/gobList.ml b/src/util/std/gobList.ml
index bcf030cb05..a81544715e 100644
--- a/src/util/std/gobList.ml
+++ b/src/util/std/gobList.ml
@@ -37,6 +37,7 @@ let equal = List.eq
     This can be used to check being a prefix in both directions simultaneously:
     - if [l1' = []], then [l1] is a prefix of [l2],
     - if [l2' = []], then [l2] is a prefix of [l1].
+
     In other cases, the common prefix is not returned (i.e. reconstructed) for efficiency reasons.
 
     @param eq equality predicate for elements *)

From 8e54444f8fd5ee0e05780c59f09a2d76cfb433d7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 15:42:27 +0300
Subject: [PATCH 14/17] Construct feasible races-mhp regression tests for
 improved history thread ID may_create

---
 .../regression/53-races-mhp/04-not-created2.c | 25 +++++++++++++
 .../regression/53-races-mhp/05-not-created3.c | 27 ++++++++++++++
 .../regression/53-races-mhp/06-not-created4.c | 36 +++++++++++++++++++
 .../regression/53-races-mhp/07-not-created5.c | 27 ++++++++++++++
 .../regression/53-races-mhp/08-not-created6.c | 31 ++++++++++++++++
 tests/unit/cdomains/threadIdDomainTest.ml     | 26 +++++++-------
 6 files changed, 159 insertions(+), 13 deletions(-)
 create mode 100644 tests/regression/53-races-mhp/04-not-created2.c
 create mode 100644 tests/regression/53-races-mhp/05-not-created3.c
 create mode 100644 tests/regression/53-races-mhp/06-not-created4.c
 create mode 100644 tests/regression/53-races-mhp/07-not-created5.c
 create mode 100644 tests/regression/53-races-mhp/08-not-created6.c

diff --git a/tests/regression/53-races-mhp/04-not-created2.c b/tests/regression/53-races-mhp/04-not-created2.c
new file mode 100644
index 0000000000..5bf2bff134
--- /dev/null
+++ b/tests/regression/53-races-mhp/04-not-created2.c
@@ -0,0 +1,25 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *b(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // NORACE
+  return NULL;
+}
+
+void *a(void *arg) {
+  pthread_t id;
+  pthread_create(&id, NULL, b, arg);
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, b, NULL);
+  g++; // NORACE
+  pthread_create(&id2, NULL, a, &g);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/05-not-created3.c b/tests/regression/53-races-mhp/05-not-created3.c
new file mode 100644
index 0000000000..ab62f44fa1
--- /dev/null
+++ b/tests/regression/53-races-mhp/05-not-created3.c
@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *a(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *b(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, a, NULL);
+  pthread_create(&id2, NULL, a, &g);
+  return NULL;
+}
+
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, a, NULL);
+  g++; // NORACE
+  pthread_create(&id2, NULL, b, NULL);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/06-not-created4.c b/tests/regression/53-races-mhp/06-not-created4.c
new file mode 100644
index 0000000000..87fe8c8a5b
--- /dev/null
+++ b/tests/regression/53-races-mhp/06-not-created4.c
@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *d(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *c(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, d, NULL);
+  pthread_create(&id2, NULL, d, &g);
+  return NULL;
+}
+
+void *b(void *arg) {
+  return NULL;
+}
+
+void *a(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, b, NULL);
+  g++; // NORACE
+  pthread_create(&id2, NULL, c, NULL);
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, a, NULL);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/07-not-created5.c b/tests/regression/53-races-mhp/07-not-created5.c
new file mode 100644
index 0000000000..e096690720
--- /dev/null
+++ b/tests/regression/53-races-mhp/07-not-created5.c
@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *a(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *b(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, a, NULL);
+  pthread_create(&id2, NULL, a, &g);
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2, id3;
+  pthread_create(&id, NULL, a, NULL);
+  pthread_create(&id, NULL, a, NULL);
+  g++; // NORACE
+  pthread_create(&id, NULL, b, NULL);
+  return 0;
+}
diff --git a/tests/regression/53-races-mhp/08-not-created6.c b/tests/regression/53-races-mhp/08-not-created6.c
new file mode 100644
index 0000000000..73b5530efa
--- /dev/null
+++ b/tests/regression/53-races-mhp/08-not-created6.c
@@ -0,0 +1,31 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *b(void *arg) {
+  return NULL;
+}
+
+void *c(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *a(void *arg) {
+  pthread_t id, id2, id3, id4;
+  pthread_create(&id, NULL, b, NULL);
+  pthread_create(&id2, NULL, b, NULL);
+  g++; // NORACE
+  pthread_create(&id, NULL, c, NULL);
+  pthread_create(&id2, NULL, c, &g);
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, a, NULL);
+  return 0;
+}
diff --git a/tests/unit/cdomains/threadIdDomainTest.ml b/tests/unit/cdomains/threadIdDomainTest.ml
index 22b30c8c07..3e352738fd 100644
--- a/tests/unit/cdomains/threadIdDomainTest.ml
+++ b/tests/unit/cdomains/threadIdDomainTest.ml
@@ -50,9 +50,9 @@ let test_history_may_create _ =
   assert_equal true (may_create main (main >> a));
   assert_equal true (may_create main (main >> a >> b));
   assert_equal true (may_create (main >> a) (main >> a >> b));
-  assert_equal false (may_create (main >> a) (main >> a));
-  assert_equal false (may_create (main >> b) (main >> a >> b));
-  assert_equal false (may_create (main >> a >> a) (main >> a >> b));
+  assert_equal false (may_create (main >> a) (main >> a)); (* infeasible for race: definitely_not_started allows equality *)
+  assert_equal false (may_create (main >> b) (main >> a >> b)); (* 53-races-mhp/04-not-created2 *)
+  assert_equal false (may_create (main >> a >> a) (main >> a >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique (main >> a >> b) *)
 
   (* unique creates non-unique and is prefix: added elements cannot be in prefix *)
   assert_equal true (may_create main (main >> a >> a));
@@ -64,22 +64,22 @@ let test_history_may_create _ =
   assert_equal true (may_create (main >> a) (main >> a >> a));
   assert_equal true (may_create (main >> a >> b) (main >> a >> b >> b));
   assert_equal true (may_create (main >> a >> b) (main >> a >> b >> a));
-  assert_equal false (may_create (main >> a >> b) (main >> a >> a));
-  assert_equal false (may_create (main >> a >> b) (main >> b >> b));
+  assert_equal false (may_create (main >> a >> b) (main >> a >> a)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> a >> a), which it is not *)
+  assert_equal false (may_create (main >> a >> b) (main >> b >> b)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> b), which it is not *)
 
   (* unique creates non-unique and prefixes are incompatible *)
-  assert_equal false (may_create (main >> a) (main >> b >> a >> a));
-  assert_equal false (may_create (main >> a >> b) (main >> b >> a >> c >> c));
-  assert_equal false (may_create (main >> a >> b) (main >> a >> c >> d >> d));
+  assert_equal false (may_create (main >> a) (main >> b >> a >> a)); (* 53-races-mhp/05-not-created3 *)
+  assert_equal false (may_create (main >> a >> b) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
+  assert_equal false (may_create (main >> a >> b) (main >> a >> c >> d >> d)); (* 53-races-mhp/06-not-created4, also passes with simple may_create *)
 
   (* non-unique creates non-unique: prefix must not lengthen *)
-  assert_equal false (may_create (main >> a >> a) (main >> a >> b >> b));
-  assert_equal false (may_create (main >> a >> a) (main >> b >> a >> a));
+  assert_equal false (may_create (main >> a >> a) (main >> a >> b >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique prefix-ed (main >> a >> b >> b) *)
+  assert_equal false (may_create (main >> a >> a) (main >> b >> a >> a)); (* 53-races-mhp/07-not-created5 *)
   (* non-unique creates non-unique: prefix must be compatible *)
-  assert_equal false (may_create (main >> a >> b >> c >> c) (main >> b >> a >> c >> c));
+  assert_equal false (may_create (main >> a >> b >> c >> c) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a >> b or main >> a >> b >> c), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
   (* non-unique creates non-unique: elements must not be removed *)
-  assert_equal false (may_create (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *)
-  assert_equal false (may_create (main >> a >> b >> b) (main >> b >> b)); (* from prefix *)
+  assert_equal false (may_create (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *) (* 53-races-mhp/08-not-created6, also passes with simple may_create *)
+  assert_equal false (may_create (main >> a >> b >> b) (main >> b >> b)); (* from prefix *) (* infeasible for race: definitely_not_started requires (main >> a or main >> a >> b), where this must happen, to be must parent for (main >> b >> b), which it is not *)
   (* non-unique creates non-unique: removed elements and set must be in new set *)
   (* assert_equal false (may_create (main >> a >> b >> c >> c) (main >> a >> c >> c)); *)
   (* TODO: cannot test due because by construction after prefix check? *)

From cc7a76a77d28f1b9b90b1f0b36d8df4d48a2cf97 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Aug 2024 15:48:51 +0300
Subject: [PATCH 15/17] Fix comment in history thread ID is_must_parent

---
 src/cdomain/value/cdomains/threadIdDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 7e208cba0e..f684aace22 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -145,7 +145,7 @@ struct
       false
     else if is_unique t' && P.equal p p' then (* t is already unique, so no need to compare sets *)
       false (* thread is not its own parent *)
-    else ( (* both are unique, but different *)
+    else ( (* t is already unique, so no need to check sets *)
       match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
       | [], _ -> true (* p is prefix of p' *)
       | _ :: _, _ -> false

From fc9ecfcfe5b01746cd18dc098373d18f4da6b772 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 20 Aug 2024 15:18:00 +0300
Subject: [PATCH 16/17] Rename to must_be_ancestor and may_be_ancestor

---
 src/cdomain/value/cdomains/threadIdDomain.ml |  26 ++---
 src/cdomains/mHP.ml                          |   6 +-
 tests/unit/cdomains/threadIdDomainTest.ml    | 100 +++++++++----------
 3 files changed, 66 insertions(+), 66 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index f684aace22..6162ff6c80 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -13,10 +13,10 @@ sig
   val is_unique: t -> bool
 
   (** Overapproximates whether the first TID can be involved in the creation fo the second TID*)
-  val may_create: t -> t -> bool
+  val may_be_ancestor: t -> t -> bool
 
   (** Is the first TID a must parent of the second thread. Always false if the first TID is not unique *)
-  val is_must_parent: t -> t -> bool
+  val must_be_ancestor: t -> t -> bool
 end
 
 module type Stateless =
@@ -87,8 +87,8 @@ struct
     | _ -> false
 
   let is_unique _ = false (* TODO: should this consider main unique? *)
-  let may_create _ _ = true
-  let is_must_parent _ _ = false
+  let may_be_ancestor _ _ = true
+  let must_be_ancestor _ _ = false
 end
 
 
@@ -140,7 +140,7 @@ struct
   let is_unique (_, s) =
     S.is_empty s
 
-  let is_must_parent ((p, s) as t) ((p', s') as t') =
+  let must_be_ancestor ((p, s) as t) ((p', s') as t') =
     if not (is_unique t) then
       false
     else if is_unique t' && P.equal p p' then (* t is already unique, so no need to compare sets *)
@@ -151,9 +151,9 @@ struct
       | _ :: _, _ -> false
     )
 
-  let may_create ((p, s) as t) ((p', s') as t') =
+  let may_be_ancestor ((p, s) as t) ((p', s') as t') =
     if is_unique t' then
-      is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
+      must_be_ancestor t t' (* unique must be created by something unique (that's a prefix) *)
     else ( (* t' is already non-unique (but doesn't matter) *)
       match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
       | [], dp when is_unique t -> (* p is prefix of p' *)
@@ -258,8 +258,8 @@ struct
 
   let is_main = unop H.is_main P.is_main
   let is_unique = unop H.is_unique P.is_unique
-  let may_create = binop H.may_create P.may_create
-  let is_must_parent = binop H.is_must_parent P.is_must_parent
+  let may_be_ancestor = binop H.may_be_ancestor P.may_be_ancestor
+  let must_be_ancestor = binop H.must_be_ancestor P.must_be_ancestor
 
   let created x d =
     let lifth x' d' =
@@ -355,14 +355,14 @@ struct
     | Thread tid -> FlagConfiguredTID.is_unique tid
     | UnknownThread -> false
 
-  let may_create t1 t2 =
+  let may_be_ancestor t1 t2 =
     match t1, t2 with
-    | Thread tid1, Thread tid2 -> FlagConfiguredTID.may_create tid1 tid2
+    | Thread tid1, Thread tid2 -> FlagConfiguredTID.may_be_ancestor tid1 tid2
     | _, _ -> true
 
-  let is_must_parent t1 t2 =
+  let must_be_ancestor t1 t2 =
     match t1, t2 with
-    | Thread tid1, Thread tid2 -> FlagConfiguredTID.is_must_parent tid1 tid2
+    | Thread tid1, Thread tid2 -> FlagConfiguredTID.must_be_ancestor tid1 tid2
     | _, _ -> false
 
   module D = FlagConfiguredTID.D
diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index 433486d4e0..afaf6d67e3 100644
--- a/src/cdomains/mHP.ml
+++ b/src/cdomains/mHP.ml
@@ -21,7 +21,7 @@ let current (ask:Queries.ask) =
   }
 
 let pretty () {tid; created; must_joined} =
-  let tid_doc = 
+  let tid_doc =
     if GobConfig.get_bool "dbg.full-output" then
       Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid)
     else
@@ -53,10 +53,10 @@ include Printable.SimplePretty (
 (** Can it be excluded that the thread tid2 is running at a program point where  *)
 (*  thread tid1 has created the threads in created1 *)
 let definitely_not_started (current, created) other =
-  if (not (TID.is_must_parent current other)) then
+  if (not (TID.must_be_ancestor current other)) then
     false
   else
-    let ident_or_may_be_created creator = TID.equal creator other || TID.may_create creator other in
+    let ident_or_may_be_created creator = TID.equal creator other || TID.may_be_ancestor creator other in
     if ConcDomain.ThreadSet.is_top created then
       false
     else
diff --git a/tests/unit/cdomains/threadIdDomainTest.ml b/tests/unit/cdomains/threadIdDomainTest.ml
index 3e352738fd..b02c1adf42 100644
--- a/tests/unit/cdomains/threadIdDomainTest.ml
+++ b/tests/unit/cdomains/threadIdDomainTest.ml
@@ -17,82 +17,82 @@ let (>>) (parent: History.t) (v: GoblintCil.varinfo): History.t =
   | [child] -> child
   | _ -> assert false
 
-let test_history_is_must_parent _ =
+let test_history_must_be_ancestor _ =
   let open History in
   let assert_equal = assert_equal ~printer:string_of_bool in
 
   (* non-unique is not must parent *)
-  assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a));
-  assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a >> a));
-  assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a >> b));
+  assert_equal false (must_be_ancestor (main >> a >> a) (main >> a >> a));
+  assert_equal false (must_be_ancestor (main >> a >> a) (main >> a >> a >> a));
+  assert_equal false (must_be_ancestor (main >> a >> a) (main >> a >> a >> b));
 
   (* unique is not self-parent *)
-  assert_equal false (is_must_parent main main);
-  assert_equal false (is_must_parent (main >> a) (main >> a));
-  assert_equal false (is_must_parent (main >> a >> b) (main >> a >> b));
+  assert_equal false (must_be_ancestor main main);
+  assert_equal false (must_be_ancestor (main >> a) (main >> a));
+  assert_equal false (must_be_ancestor (main >> a >> b) (main >> a >> b));
 
   (* unique is must parent if prefix *)
-  assert_equal true (is_must_parent main (main >> a));
-  assert_equal true (is_must_parent main (main >> a >> a));
-  assert_equal true (is_must_parent main (main >> a >> b));
-  assert_equal true (is_must_parent (main >> a) (main >> a >> b));
-  assert_equal false (is_must_parent (main >> a) main);
-  assert_equal false (is_must_parent (main >> b) (main >> a >> b));
-  assert_equal false (is_must_parent (main >> a) (main >> b >> a));
-  assert_equal false (is_must_parent (main >> a) (main >> a >> a)); (* may be created by just main (non-uniquely) *)
+  assert_equal true (must_be_ancestor main (main >> a));
+  assert_equal true (must_be_ancestor main (main >> a >> a));
+  assert_equal true (must_be_ancestor main (main >> a >> b));
+  assert_equal true (must_be_ancestor (main >> a) (main >> a >> b));
+  assert_equal false (must_be_ancestor (main >> a) main);
+  assert_equal false (must_be_ancestor (main >> b) (main >> a >> b));
+  assert_equal false (must_be_ancestor (main >> a) (main >> b >> a));
+  assert_equal false (must_be_ancestor (main >> a) (main >> a >> a)); (* may be created by just main (non-uniquely) *)
   ()
 
-let test_history_may_create _ =
+let test_history_may_be_ancestor _ =
   let open History in
   let assert_equal = assert_equal ~printer:string_of_bool in
 
   (* unique may only be created by unique (prefix) *)
-  assert_equal true (may_create main (main >> a));
-  assert_equal true (may_create main (main >> a >> b));
-  assert_equal true (may_create (main >> a) (main >> a >> b));
-  assert_equal false (may_create (main >> a) (main >> a)); (* infeasible for race: definitely_not_started allows equality *)
-  assert_equal false (may_create (main >> b) (main >> a >> b)); (* 53-races-mhp/04-not-created2 *)
-  assert_equal false (may_create (main >> a >> a) (main >> a >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique (main >> a >> b) *)
+  assert_equal true (may_be_ancestor main (main >> a));
+  assert_equal true (may_be_ancestor main (main >> a >> b));
+  assert_equal true (may_be_ancestor (main >> a) (main >> a >> b));
+  assert_equal false (may_be_ancestor (main >> a) (main >> a)); (* infeasible for race: definitely_not_started allows equality *)
+  assert_equal false (may_be_ancestor (main >> b) (main >> a >> b)); (* 53-races-mhp/04-not-created2 *)
+  assert_equal false (may_be_ancestor (main >> a >> a) (main >> a >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique (main >> a >> b) *)
 
   (* unique creates non-unique and is prefix: added elements cannot be in prefix *)
-  assert_equal true (may_create main (main >> a >> a));
-  assert_equal true (may_create main (main >> a >> b >> b));
-  assert_equal true (may_create (main >> a) (main >> a >> b >> b));
+  assert_equal true (may_be_ancestor main (main >> a >> a));
+  assert_equal true (may_be_ancestor main (main >> a >> b >> b));
+  assert_equal true (may_be_ancestor (main >> a) (main >> a >> b >> b));
   (* TODO: added elements condition always true by construction in tests? *)
 
   (* non-unique created by unique and is prefix: removed elements must be in set *)
-  assert_equal true (may_create (main >> a) (main >> a >> a));
-  assert_equal true (may_create (main >> a >> b) (main >> a >> b >> b));
-  assert_equal true (may_create (main >> a >> b) (main >> a >> b >> a));
-  assert_equal false (may_create (main >> a >> b) (main >> a >> a)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> a >> a), which it is not *)
-  assert_equal false (may_create (main >> a >> b) (main >> b >> b)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> b), which it is not *)
+  assert_equal true (may_be_ancestor (main >> a) (main >> a >> a));
+  assert_equal true (may_be_ancestor (main >> a >> b) (main >> a >> b >> b));
+  assert_equal true (may_be_ancestor (main >> a >> b) (main >> a >> b >> a));
+  assert_equal false (may_be_ancestor (main >> a >> b) (main >> a >> a)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> a >> a), which it is not *)
+  assert_equal false (may_be_ancestor (main >> a >> b) (main >> b >> b)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> b), which it is not *)
 
   (* unique creates non-unique and prefixes are incompatible *)
-  assert_equal false (may_create (main >> a) (main >> b >> a >> a)); (* 53-races-mhp/05-not-created3 *)
-  assert_equal false (may_create (main >> a >> b) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
-  assert_equal false (may_create (main >> a >> b) (main >> a >> c >> d >> d)); (* 53-races-mhp/06-not-created4, also passes with simple may_create *)
+  assert_equal false (may_be_ancestor (main >> a) (main >> b >> a >> a)); (* 53-races-mhp/05-not-created3 *)
+  assert_equal false (may_be_ancestor (main >> a >> b) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
+  assert_equal false (may_be_ancestor (main >> a >> b) (main >> a >> c >> d >> d)); (* 53-races-mhp/06-not-created4, also passes with simple may_be_ancestor *)
 
   (* non-unique creates non-unique: prefix must not lengthen *)
-  assert_equal false (may_create (main >> a >> a) (main >> a >> b >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique prefix-ed (main >> a >> b >> b) *)
-  assert_equal false (may_create (main >> a >> a) (main >> b >> a >> a)); (* 53-races-mhp/07-not-created5 *)
+  assert_equal false (may_be_ancestor (main >> a >> a) (main >> a >> b >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique prefix-ed (main >> a >> b >> b) *)
+  assert_equal false (may_be_ancestor (main >> a >> a) (main >> b >> a >> a)); (* 53-races-mhp/07-not-created5 *)
   (* non-unique creates non-unique: prefix must be compatible *)
-  assert_equal false (may_create (main >> a >> b >> c >> c) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a >> b or main >> a >> b >> c), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
+  assert_equal false (may_be_ancestor (main >> a >> b >> c >> c) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a >> b or main >> a >> b >> c), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
   (* non-unique creates non-unique: elements must not be removed *)
-  assert_equal false (may_create (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *) (* 53-races-mhp/08-not-created6, also passes with simple may_create *)
-  assert_equal false (may_create (main >> a >> b >> b) (main >> b >> b)); (* from prefix *) (* infeasible for race: definitely_not_started requires (main >> a or main >> a >> b), where this must happen, to be must parent for (main >> b >> b), which it is not *)
+  assert_equal false (may_be_ancestor (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *) (* 53-races-mhp/08-not-created6, also passes with simple may_be_ancestor *)
+  assert_equal false (may_be_ancestor (main >> a >> b >> b) (main >> b >> b)); (* from prefix *) (* infeasible for race: definitely_not_started requires (main >> a or main >> a >> b), where this must happen, to be must parent for (main >> b >> b), which it is not *)
   (* non-unique creates non-unique: removed elements and set must be in new set *)
-  (* assert_equal false (may_create (main >> a >> b >> c >> c) (main >> a >> c >> c)); *)
+  (* assert_equal false (may_be_ancestor (main >> a >> b >> c >> c) (main >> a >> c >> c)); *)
   (* TODO: cannot test due because by construction after prefix check? *)
   (* non-unique creates non-unique *)
-  assert_equal true (may_create (main >> a >> a) (main >> a >> a));
-  assert_equal true (may_create (main >> a >> a) (main >> a >> a >> b));
-  assert_equal true (may_create (main >> a >> a) (main >> a >> b >> a));
-  assert_equal true (may_create (main >> a >> a) (main >> a >> b >> c >> a));
-  assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> b));
-  assert_equal true (may_create (main >> a >> b >> b) (main >> a >> a >> b));
-  assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> a));
-  assert_equal true (may_create (main >> a >> b >> b) (main >> b >> b >> a));
-  assert_equal true (may_create (main >> a >> b >> b) (main >> b >> a >> b));
+  assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> a));
+  assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> a >> b));
+  assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> b >> a));
+  assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> b >> c >> a));
+  assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> a >> b >> b));
+  assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> a >> a >> b));
+  assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> a >> b >> a));
+  assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> b >> b >> a));
+  assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> b >> a >> b));
 
   (* 4f6a7637b8d0dc723fe382f94bed6c822cd4a2ce passes all... *)
   ()
@@ -100,7 +100,7 @@ let test_history_may_create _ =
 let tests =
   "threadIdDomainTest" >::: [
     "history" >::: [
-      "is_must_parent" >:: test_history_is_must_parent;
-      "may_create" >:: test_history_may_create;
+      "must_be_ancestor" >:: test_history_must_be_ancestor;
+      "may_be_ancestor" >:: test_history_may_be_ancestor;
     ]
   ]

From 205d2b92d746e57e48ef9d54dec36c88d9ffe4f5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 17 Dec 2024 10:53:20 +0200
Subject: [PATCH 17/17] Fix ThreadIdDomain comments from review

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
---
 src/cdomain/value/cdomains/threadIdDomain.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 6162ff6c80..2721326f4d 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -12,10 +12,10 @@ sig
   val is_main: t -> bool
   val is_unique: t -> bool
 
-  (** Overapproximates whether the first TID can be involved in the creation fo the second TID*)
+  (** Overapproximates whether the first TID can be involved in the creation of the second TID*)
   val may_be_ancestor: t -> t -> bool
 
-  (** Is the first TID a must parent of the second thread. Always false if the first TID is not unique *)
+  (** Is the first TID a must ancestor of the second thread. Always false if the first TID is not unique *)
   val must_be_ancestor: t -> t -> bool
 end