Analysis of Thread Must Joins

src/analyses/threadJoins.ml

@@ -0,0 +1,50 @@
+(** Thread join analysis. *)
+open Prelude.Ana
+open Analyses
+
+module TID  = ThreadIdDomain.Thread
+module TIDs = ConcDomain.ThreadSet
+module MustTIDs = ConcDomain.MustThreadSet
+
+module Spec =
+struct
+  include Analyses.IdentitySpec
+
+  let name () = "threadJoins"
+  module D = MustTIDs
+  module C = D
+  module G = MustTIDs
+
+  (* transfer functions *)
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    (
+      match ctx.ask CurrentThreadId with
+      | `Lifted tid -> ctx.sideg (TID.to_varinfo tid) ctx.local
+      | _ -> () (* correct? *)
+    );
+    ctx.local
+
+  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    match LibraryFunctions.classify f.vname arglist with
+    | `ThreadJoin (id, ret_var) ->
+      (
+        let threads = TIDs.elements (ctx.ask (Queries.EvalThread id)) in
+        match threads with
+        | [tid] when TID.is_unique tid->
+          let joined = ctx.global (TID.to_varinfo tid) in
+          D.union (D.add tid ctx.local) joined
+        | _ -> ctx.local (* if multiple possible thread ids are joined, none of them is must joined*)
+        (* Possible improvement: Do the intersection first, things that are must joined in all possibly joined threads are must-joined *)
+      )
+    | _ -> ctx.local
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.MustJoinedThreads -> (ctx.local:ConcDomain.MustThreadSet.t) (* type annotation needed to avoid "would escape the scope of its equation" *)
+    | _ ->  Queries.Result.top q
+
+  let startstate v = D.top ()
+  let exitstate  v = D.top ()
+end
+
+let _ = MCP.register_analysis ~dep:["threadid"] (module Spec : MCPSpec)

src/cdomains/concDomain.ml

@@ -1,4 +1,5 @@
 module ThreadSet = SetDomain.ToppedSet (ThreadIdDomain.Thread) (struct let topname = "All Threads" end)
+module MustThreadSet = SetDomain.Reverse(ThreadSet)
 
 module CreatedThreadSet = ThreadSet
 

src/domains/queries.ml

@@ -94,6 +94,8 @@ type _ t =
   | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *)
   | IsMultiple: varinfo -> MustBool.t t (* Is no other copy of this local variable reachable via pointers? *)
   | EvalThread: exp -> ConcDomain.ThreadSet.t t
+  | CreatedThreads: ConcDomain.ThreadSet.t t
+  | MustJoinedThreads: ConcDomain.MustThreadSet.t t
 
 type 'a result = 'a
 
@@ -143,6 +145,8 @@ struct
     | PartAccess _ -> (module PartAccessResult)
     | IsMultiple _ -> (module MustBool) (* see https://github.com/goblint/analyzer/pull/310#discussion_r700056687 on why this needs to be MustBool *)
     | EvalThread _ -> (module ConcDomain.ThreadSet)
+    | CreatedThreads ->  (module ConcDomain.ThreadSet)
+    | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -191,6 +195,8 @@ struct
     | PartAccess _ -> PartAccessResult.top ()
     | IsMultiple _ -> MustBool.top ()
     | EvalThread _ -> ConcDomain.ThreadSet.top ()
+    | CreatedThreads -> ConcDomain.ThreadSet.top ()
+    | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -237,6 +243,8 @@ struct
       | Any (IsHeapVar _) -> 30
       | Any (IsMultiple _) -> 31
       | Any (EvalThread _) -> 32
+      | Any CreatedThreads -> 33
+      | Any MustJoinedThreads -> 34
     in
     let r = Stdlib.compare (order a) (order b) in
     if r <> 0 then

tests/regression/51-threadjoins/01-trivial.c

@@ -0,0 +1,29 @@
+//PARAM: --set ana.activated[+] threadJoins
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_join(id2, NULL);
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_benign, NULL);
+  pthread_join(id2, NULL);
+  // t_benign and t_fun should be in here
+
+  return 0;
+}

tests/regression/51-threadjoins/02-other.c

@@ -0,0 +1,34 @@
+//PARAM: --set ana.activated[+] threadJoins
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_join(id2, NULL);
+  // should be empty
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id2[10];
+  for(int i =0; i < 10;i++) {
+  pthread_create(&id2[i], NULL, t_benign, NULL);
+  }
+
+  pthread_join(id2[2], NULL);
+
+  // should be empty
+
+  return 0;
+}