Merge pull request #1224 from goblint/issue-392

Add unknown thread ID

src/analyses/apron/relationPriv.apron.ml

@@ -1010,17 +1010,17 @@ struct
       )
     )
     else (
-      match ConcDomain.ThreadSet.elements tids with
-      | [tid] ->
-        let lmust',l' = G.thread (getg (V.thread tid)) in
-        {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
-      | _ ->
-        (* To match the paper more closely, one would have to join in the non-definite case too *)
-        (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
-        st
-      | exception SetDomain.Unsupported _ ->
-        (* elements throws if the thread set is top *)
+      if ConcDomain.ThreadSet.is_top tids then
         st
+      else
+        match ConcDomain.ThreadSet.elements tids with
+        | [tid] ->
+          let lmust',l' = G.thread (getg (V.thread tid)) in
+          {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
+        | _ ->
+          (* To match the paper more closely, one would have to join in the non-definite case too *)
+          (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
+          st
     )
 
   let thread_return ask getg sideg tid (st: relation_components_t) =

src/analyses/base.ml

@@ -2397,10 +2397,12 @@ struct
     (* handling thread joins... sort of *)
     | ThreadJoin { thread = id; ret_var }, _ ->
       let st' =
+        (* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *)
         match (eval_rv (Analyses.ask_of_ctx ctx) gs st ret_var) with
         | Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st
         | Address ret_a ->
           begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with
+            | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
             | Thread a ->
               let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in
               (* TODO: is this type right? *)

src/analyses/basePriv.ml

@@ -544,17 +544,17 @@ struct
       )
     )
     else (
-      match ConcDomain.ThreadSet.elements tids with
-      | [tid] ->
-        let lmust',l' = G.thread (getg (V.thread tid)) in
-        {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
-      | _ ->
-        (* To match the paper more closely, one would have to join in the non-definite case too *)
-        (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
-        st
-      | exception SetDomain.Unsupported _ ->
-        (* elements throws if the thread set is top *)
+      if ConcDomain.ThreadSet.is_top tids then 
         st
+      else
+        match ConcDomain.ThreadSet.elements tids with
+        | [tid] ->
+          let lmust',l' = G.thread (getg (V.thread tid)) in
+          {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
+        | _ ->
+          (* To match the paper more closely, one would have to join in the non-definite case too *)
+          (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
+          st
     )
 
   let thread_return ask getg sideg tid (st: BaseComponents (D).t) =

src/analyses/threadAnalysis.ml

@@ -57,16 +57,18 @@ struct
     | ThreadJoin { thread = id; ret_var } ->
       (* TODO: generalize ThreadJoin like ThreadCreate *)
       (let has_clean_exit tid = not (BatTuple.Tuple3.third (ctx.global tid)) in
+       let tids = ctx.ask (Queries.EvalThread id) in
        let join_thread s tid =
          if has_clean_exit tid && not (is_not_unique ctx tid) then
            D.remove tid s
          else
            s
        in
-       match TS.elements (ctx.ask (Queries.EvalThread id)) with
-       | [t] -> join_thread ctx.local t (* single thread *)
-       | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *)
-       | exception SetDomain.Unsupported _ -> ctx.local)
+       if TS.is_top tids
+       then ctx.local
+       else match TS.elements tids with
+         | [t] -> join_thread ctx.local t (* single thread *)
+         | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *))
     | ThreadExit { ret_val } ->
       handle_thread_return ctx (Some ret_val);
       ctx.local

src/analyses/threadJoins.ml

@@ -52,7 +52,7 @@ struct
       if TIDs.is_top threads then
         ctx.local
       else (
-        (* elements throws if the thread set is top *)
+        (* all elements are known *)
         let threads = TIDs.elements threads in
         match threads with
         | [tid] when TID.is_unique tid->
@@ -70,7 +70,7 @@ struct
         (MustTIDs.bot(), true) (* consider everything joined, MustTIDs is reversed so bot is All threads *)
       )
       else (
-        (* elements throws if the thread set is top *)
+        (* all elements are known *)
         let threads = TIDs.elements threads in
         if List.compare_length_with threads 1 > 0 then
           M.info ~category:Unsound "Ambiguous thread ID assume-joined, assuming all of those threads must-joined.";

src/analyses/useAfterFree.ml

@@ -76,7 +76,7 @@ struct
           end
           else if HeapVars.mem heap_var (snd ctx.local) then begin
             if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
-            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.Thread.pretty current CilType.Varinfo.pretty heap_var
           end
         end
       | `Top ->

src/cdomains/concDomain.ml

@@ -1,6 +1,25 @@
 (** Domains for thread sets and their uniqueness. *)
 
-module ThreadSet = SetDomain.ToppedSet (ThreadIdDomain.Thread) (struct let topname = "All Threads" end)
+module ThreadSet = 
+struct 
+  include SetDomain.Make (ThreadIdDomain.Thread)
+
+  let is_top = mem UnknownThread
+
+  let top () = singleton UnknownThread
+
+  let merge uop cop x y =
+    match is_top x, is_top y with
+    | true, true -> uop x y
+    | false, true -> x
+    | true, false -> y
+    | false, false -> cop x y
+
+  let meet x y = merge join meet x y
+
+  let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y
+
+end
 module MustThreadSet = SetDomain.Reverse(ThreadSet)
 
 module CreatedThreadSet = ThreadSet

src/cdomains/mHP.ml

@@ -4,7 +4,7 @@ include Printable.Std
 
 let name () = "mhp"
 
-module TID = ThreadIdDomain.FlagConfiguredTID
+module TID = ThreadIdDomain.Thread
 module Pretty = GoblintCil.Pretty
 
 type t = {

src/cdomains/threadIdDomain.ml

@@ -280,6 +280,79 @@ struct
   let name () = "FlagConfiguredTID: " ^ if history_enabled () then H.name () else P.name ()
 end
 
-module Thread = FlagConfiguredTID
+type thread =
+  | Thread of FlagConfiguredTID.t
+  | UnknownThread
+[@@deriving eq, ord, hash]
+
+module Thread : Stateful with type t = thread =
+struct
+  include Printable.Std
+  type t = thread [@@deriving eq, ord, hash]
+
+  let name () = "Thread id"
+  let pretty () t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.pretty () tid
+    | UnknownThread -> Pretty.text "Unknown thread id"
+
+  let show t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.show tid
+    | UnknownThread -> "Unknown thread id"
+
+  let printXml f t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.printXml f tid
+    | UnknownThread -> BatPrintf.fprintf f "<value>\n<data>\nUnknown thread id\n</data>\n</value>\n"
+
+  let to_yojson t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.to_yojson tid
+    | UnknownThread -> `String "Unknown thread id"
+
+  let relift t =
+    match t with
+    | Thread tid -> Thread (FlagConfiguredTID.relift tid)
+    | UnknownThread -> UnknownThread
+
+  let lift t = Thread t
+
+  let threadinit v ~multiple = Thread (FlagConfiguredTID.threadinit v ~multiple)
+
+  let is_main t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.is_main tid
+    | UnknownThread -> false
+
+  let is_unique t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.is_unique tid
+    | UnknownThread -> false
+
+  let may_create t1 t2 =
+    match t1, t2 with
+    | Thread tid1, Thread tid2 -> FlagConfiguredTID.may_create tid1 tid2
+    | _, _ -> true
+
+  let is_must_parent t1 t2 =
+    match t1, t2 with
+    | Thread tid1, Thread tid2 -> FlagConfiguredTID.is_must_parent tid1 tid2
+    | _, _ -> false
+
+  module D = FlagConfiguredTID.D
+
+  let threadenter ~multiple (t, d) node i v =
+    match t with
+    | Thread tid -> List.map lift (FlagConfiguredTID.threadenter ~multiple (tid, d) node i v)
+    | UnknownThread -> assert false
+
+  let threadspawn = FlagConfiguredTID.threadspawn
+
+  let created t d =
+    match t with
+    | Thread tid -> Option.map (List.map lift) (FlagConfiguredTID.created tid d)
+    | UnknownThread -> None
+end
 
 module ThreadLifted = Lift (Thread)

src/cdomains/valueDomain.ml

@@ -552,11 +552,9 @@ struct
     | y, Blob (x,s,o) -> Blob (join (x:t) y, s, o)
     | (Thread x, Thread y) -> Thread (Threads.join x y)
     | (Int x, Thread y)
-    | (Thread y, Int x) ->
-      Thread y (* TODO: ignores int! *)
+    | (Thread y, Int x) -> Thread (Threads.join y (Threads.top ()))
     | (Address x, Thread y)
-    | (Thread y, Address x) ->
-      Thread y (* TODO: ignores address! *)
+    | (Thread y, Address x) -> Thread (Threads.join y (Threads.top ()))
     | (JmpBuf x, JmpBuf y) -> JmpBuf (JmpBufs.join x y)
     | (Mutex, Mutex) -> Mutex
     | (MutexAttr x, MutexAttr y) -> MutexAttr (MutexAttr.join x y)
@@ -585,11 +583,9 @@ struct
     | (Blob x, Blob y) -> Blob (Blobs.widen x y) (* TODO: why no blob special cases like in join? *)
     | (Thread x, Thread y) -> Thread (Threads.widen x y)
     | (Int x, Thread y)
-    | (Thread y, Int x) ->
-      Thread y (* TODO: ignores int! *)
+    | (Thread y, Int x) -> Thread (Threads.widen y (Threads.join y (Threads.top ())))
     | (Address x, Thread y)
-    | (Thread y, Address x) ->
-      Thread y (* TODO: ignores address! *)
+    | (Thread y, Address x) -> Thread (Threads.widen y (Threads.join y (Threads.top ())))
     | (Mutex, Mutex) -> Mutex
     | (JmpBuf x, JmpBuf y) -> JmpBuf (JmpBufs.widen x y)
     | (MutexAttr x, MutexAttr y) -> MutexAttr (MutexAttr.widen x y)
@@ -708,7 +704,7 @@ struct
       let v = invalidate_value ask voidType (CArrays.get ask n (array_idx_top)) in
       Array (CArrays.set ask n (array_idx_top) v)
     |                 t , Blob n       -> Blob (Blobs.invalidate_value ask t n)
-    |                 _ , Thread _     -> state (* TODO: no top thread ID set! *)
+    |                 _ , Thread tid   -> Thread (Threads.join (Threads.top ()) tid)
     |                 _ , JmpBuf _     -> state (* TODO: no top jmpbuf *)
     | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t

tests/regression/51-threadjoins/07-trivial-unknowntid.c

@@ -0,0 +1,34 @@
+//PARAM: --set ana.activated[+] threadJoins
+#include <pthread.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  g++; // RACE!
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  h++; // NORACE
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+  foo(&id2);
+  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
+
+  g++; // RACE!
+  h++; // NORACE
+
+  return 0;
+}