First steps towards a Proof-of-Concept for analyzing threadpools

src/analyses/base.ml

@@ -1276,7 +1276,7 @@ struct
         let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
         (* ignore (Pretty.eprintf "evalthread %a (%a): %a" d_exp e d_plainexp e VD.pretty v); *)
         match v with
-        | Thread a -> a
+        | Thread a -> snd a
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | _ -> Queries.Result.top q
       end
@@ -2251,9 +2251,14 @@ struct
         | Address ret_a ->
           begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with
             | 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
+              let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ConcDomain.ThreadSet.elements (snd a))) in
               (* TODO: is this type right? *)
-              set ~ctx (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v
+              let res = set ~ctx (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v in
+              (match ConcDomain.ThreadSet.elements (snd a), id with
+              | _::_, Lval l ->
+                let lv = eval_lv (Analyses.ask_of_ctx ctx) gs st l in
+                set ~ctx (Analyses.ask_of_ctx ctx) gs res lv (Cilfacade.typeOf id) (Thread (true, snd a))
+              | _ -> res)
             | _      -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
           end
         | _      -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
@@ -2677,7 +2682,7 @@ struct
       Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
     | Events.AssignSpawnedThread (lval, tid) ->
       (* TODO: is this type right? *)
-      set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid))
+      set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (false, ConcDomain.ThreadSet.singleton tid))
     | Events.Assert exp ->
       assert_fn ctx exp true
     | Events.Unassume {exp; uuids} ->

src/cdomains/concDomain.ml

@@ -2,6 +2,7 @@
 
 module ThreadSet = SetDomain.ToppedSet (ThreadIdDomain.Thread) (struct let topname = "All Threads" end)
 module MustThreadSet = SetDomain.Reverse(ThreadSet)
+module ThreadSetMustJoined = Lattice.Prod (BoolDomain.MustBool) (ThreadSet)
 
 module CreatedThreadSet = ThreadSet
 

src/cdomains/valueDomain.ml

@@ -73,7 +73,7 @@ struct
   let invalidate_value ask t (v, s, o) = Value.invalidate_value ask t v, s, o
 end
 
-module Threads = ConcDomain.ThreadSet
+module Threads = ConcDomain.ThreadSetMustJoined
 module JmpBufs = JmpBufDomain.JmpBufSetTaint
 
 module rec Compound: sig
@@ -146,7 +146,7 @@ struct
       let typAttr = typeAttrs ai in
       let len = array_length_idx (IndexDomain.bot ()) length in
       Array (CArrays.make ~varAttr ~typAttr len (bot_value ai))
-    | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ())
+    | t when is_thread_type t -> Thread (true, ConcDomain.ThreadSet.empty ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.bot ())
     | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false)
     | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t)
@@ -958,7 +958,7 @@ struct
           | Thread t -> value (* if actually assigning thread, use value *)
           | _ ->
             if !AnalysisState.global_initialization then
-              Thread (ConcDomain.ThreadSet.empty ()) (* if assigning global init (int on linux, ptr to struct on mac), use empty set instead *)
+              Thread (true, ConcDomain.ThreadSet.empty ()) (* if assigning global init (int on linux, ptr to struct on mac), use empty set instead *)
             else
               Top
         end

tests/regression/40-threadid/09-poc.c

@@ -0,0 +1,36 @@
+// PARAM: --set ana.base.arrays.domain partitioned --enable ana.int.interval
+#include <goblint.h>
+#include <pthread.h>
+
+
+void *t_fun(void *arg) {
+  return 5;
+}
+
+int main() {
+  pthread_t idtmp;
+  pthread_t id[10];
+  int x;
+
+  pthread_create(&id[0], NULL, t_fun, NULL);
+  x = 8;
+
+  for(int i =0; i < 10; i++) {
+    pthread_create(&idtmp, NULL, t_fun, NULL);
+    id[i] = idtmp;
+  }
+
+  x = 2;
+
+  for(int i =0; i < 10; i++) {
+    // Pulled into temporary assignment, as set in pthread_join does not provide needed information to
+    // partitioned arrays
+    idtmp = id[i];
+    pthread_join(idtmp, &x); //Providing a pointer to x to go into the code that handles it
+    id[i] = idtmp;
+  }
+
+  // We know all threads who have their tids in the array id have been joined
+  // Only additional thing that is needed is proof that the array contains all thread ids that have been created
+  // e.g. by all distinct
+}