diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index fff6734f27..2721326f4d 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -12,11 +12,11 @@ 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*)
- val may_create: t -> t -> bool
+ (** 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 *)
- val is_must_parent: t -> t -> bool
+ (** 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
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,18 +140,34 @@ 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 must_be_ancestor ((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
- let cdef_ancestor = P.common_suffix p p' in
- P.equal p cdef_ancestor
+ 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 ( (* 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
+ )
- 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_be_ancestor ((p, s) as t) ((p', s') as t') =
+ if is_unique t' then
+ 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' *)
+ (* 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 (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 =
if BatList.mem_cmp Base.compare ni p then (
@@ -242,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' =
@@ -339,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/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 "\n\n\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..a81544715e 100644
--- a/src/util/std/gobList.ml
+++ b/src/util/std/gobList.ml
@@ -30,6 +30,22 @@ 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'
+ | _, _ -> (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) =
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
+
+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
+
+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
+
+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
+
+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
+
+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
new file mode 100644
index 0000000000..b02c1adf42
--- /dev/null
+++ b/tests/unit/cdomains/threadIdDomainTest.ml
@@ -0,0 +1,106 @@
+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_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 (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 (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 (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_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_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_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_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_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_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_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_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_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_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... *)
+ ()
+
+let tests =
+ "threadIdDomainTest" >::: [
+ "history" >::: [
+ "must_be_ancestor" >:: test_history_must_be_ancestor;
+ "may_be_ancestor" >:: test_history_may_be_ancestor;
+ ]
+ ]
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 () =