Merge pull request #1561 from goblint/threadid-history-may_create

Improve history thread ID `may_create`

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 = is_main
-  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

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

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

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) =

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;
+}

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;
+}

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;
+}

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;
+}

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;
+}