Collect thread spawns instead of doing them immediately (issue #148)

src/analyses/arinc.ml

@@ -665,7 +665,7 @@ struct
     let f_d = snd (Tasks.choose tasks_f) in
     { f_d with pre = d.pre }
 
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 end
 
 let _ =

src/analyses/base.ml

@@ -2034,7 +2034,7 @@ struct
       end
     (* handling thread creations *)
     | `ThreadCreate _ ->
-      D.bot () (* actual results joined via threadspawn *)
+      ctx.local (* actual results joined via threadspawn *)
     (* handling thread joins... sort of *)
     | `ThreadJoin (id,ret_var) ->
       begin match (eval_rv ctx.ask gs st ret_var) with
@@ -2184,6 +2184,7 @@ struct
       ctx.local
 
   let threadspawn ctx (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
+    (* D.join ctx.local @@ *)
     match lval with
     | Some lval ->
       begin match ThreadId.get_current fctx.ask with

src/analyses/condVars.ml

@@ -144,7 +144,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.bot ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 

src/analyses/contain.ml

@@ -806,7 +806,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.bot ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 

src/analyses/deadlock.ml

@@ -53,7 +53,7 @@ struct
   (* Some required states *)
   let startstate _ : D.t = D.empty ()
   let threadenter ctx lval f args : D.t = D.empty ()
-  let threadspawn ctx lval f args fctx = D.empty ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  _ : D.t = D.empty ()
 
   (* ======== Transfer functions ======== *)

src/analyses/expRelation.ml

@@ -113,7 +113,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 

src/analyses/extract_arinc.ml

@@ -401,7 +401,7 @@ struct
     let f_d = snd (Tasks.choose tasks_f) in
     f_d
 
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 end
 
 let _ =

src/analyses/extract_osek.ml

@@ -318,7 +318,7 @@ struct
 
   let startstate v = Pid.of_int 0L, Ctx.top (), Pred.of_node (MyCFG.Function (emptyFunction "main").svar)
   let threadenter ctx lval f args = D.bot ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 
   let init () = (* registers which functions to extract and writes out their definitions *)

src/analyses/fileUse.ml

@@ -297,7 +297,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.bot ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 

src/analyses/flag.ml

@@ -127,7 +127,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let name () = "flag"

src/analyses/flagModes.ml

@@ -131,7 +131,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 

src/analyses/mallocWrapperAnalysis.ml

@@ -52,7 +52,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let heap_hash = Hashtbl.create 113

src/analyses/malloc_null.ml

@@ -226,7 +226,7 @@ struct
 
   let startstate v = D.empty ()
   let threadenter ctx lval f args = D.empty ()
-  let threadspawn ctx lval f args fctx = D.empty ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 
   let init () =

src/analyses/mayLocks.ml

@@ -70,7 +70,7 @@ struct
 
   let startstate v = D.empty ()
   let threadenter ctx lval f args = D.empty ()
-  let threadspawn ctx lval f args fctx = D.empty ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 

src/analyses/mutexAnalysis.ml

@@ -226,7 +226,7 @@ struct
   (** We just lift start state, global and dependency functions: *)
   let startstate v = Lockset.empty ()
   let threadenter ctx lval f args = Lockset.empty ()
-  let threadspawn ctx lval f args fctx = Lockset.empty ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = Lockset.empty ()
 
   let query ctx (q:Queries.t) : Queries.Result.t =

src/analyses/octagon.ml

@@ -371,7 +371,7 @@ struct
       else `Top
     | _ -> Queries.Result.top ()
 
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 end
 
 

src/analyses/osek.ml

@@ -714,7 +714,7 @@ struct
   let exitstate  v = D.top ()
 
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 
   let activate_task ctx (task_name : string) : unit =
     let task = Cilfacade.getFun task_name in

src/analyses/osektransactionality.ml

@@ -115,7 +115,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   (** Finalization and other result printing functions: *)

src/analyses/poly.ml

@@ -20,7 +20,7 @@ struct
   let context x = if GobConfig.get_bool "exp.full-context" then x else D.bot ()
 
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  _ = D.top ()
   let startstate _ = D.top ()
 

src/analyses/region.ml

@@ -176,7 +176,7 @@ struct
 
   let threadenter ctx lval f args =
     `Lifted (RegMap.bot ())
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 
   let exitstate v = `Lifted (RegMap.bot ())
 

src/analyses/shapes.ml

@@ -71,7 +71,7 @@ struct
   let threadenter ctx lval f args =
     let st, re = ctx.local in
     (LD.singleton (SHMap.top ()), Re.threadenter (re_context ctx re) lval f args)
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 
   let sync_ld ask gl upd st =
     let f sm (st, ds, rm, part)=

src/analyses/spec.ml

@@ -512,7 +512,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.bot ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 

src/analyses/stackTrace.ml

@@ -37,7 +37,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.bot ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 
@@ -79,7 +79,7 @@ struct
   let threadenter ctx lval f args =
     D.push !Tracing.current_loc ctx.local
 
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 end
 
 

src/analyses/symbLocks.ml

@@ -24,7 +24,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let branch ctx exp tv = ctx.local

src/analyses/termination.ml

@@ -230,7 +230,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.bot ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end
 

src/analyses/threadAnalysis.ml

@@ -15,6 +15,8 @@ struct
   module C = D
   module G = ConcDomain.ThreadCreation
 
+  let should_join = D.equal
+
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t = ctx.local
   let branch ctx (exp:exp) (tv:bool) : D.t =  ctx.local
@@ -100,7 +102,7 @@ struct
       | `Bot         -> (false,    TS.bot (),         false)
     in
     ctx.sideg tid eff;
-    D.singleton tid
+    D.join ctx.local (D.singleton tid)
   let exitstate  v = D.bot ()
 end
 
@@ -131,7 +133,7 @@ struct
     let location x = let l = !Tracing.current_loc in l.file ^ ":" ^ string_of_int l.line ^ ":" ^ x.vname in
     D.singleton (location f)
 
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
 end
 
 let _ = MCP.register_analysis (module StartLocIDs : MCPSpec)

src/analyses/threadEscape.ml

@@ -70,13 +70,14 @@ struct
     | _ -> D.bot ()
 
   let threadspawn ctx lval f args fctx =
-    match args with
-    | [ptc_arg] ->
-      let escaped = fctx.local in (* reuse reachable computation from threadenter *)
-      if not (D.is_empty escaped) then (* avoid emitting unnecessary event *)
-        ctx.emit (Events.Escape escaped);
-      escaped
-    | _ -> D.bot ()
+    D.join ctx.local @@
+      match args with
+      | [ptc_arg] ->
+        let escaped = fctx.local in (* reuse reachable computation from threadenter *)
+        if not (D.is_empty escaped) then (* avoid emitting unnecessary event *)
+          ctx.emit (Events.Escape escaped);
+        escaped
+      | _ -> D.bot ()
 end
 
 let _ =

src/analyses/threadFlag.ml

@@ -32,6 +32,8 @@ struct
   let create_tid v =
     Flag.get_multi ()
 
+  let should_join = D.equal
+
   let body ctx f = ctx.local
 
   let branch ctx exp tv = ctx.local
@@ -84,7 +86,7 @@ struct
   let threadspawn ctx lval f args fctx =
     if not (is_multi ctx.ask) then
       ctx.emit Events.EnterMultiThreaded;
-    Flag.get_main ()
+    D.join ctx.local (Flag.get_main ())
 end
 
 let _ =

src/analyses/threadId.ml

@@ -89,7 +89,7 @@ struct
     create_tid f
 
   let threadspawn ctx lval f args fctx =
-    ThreadLifted.bot ()
+    ctx.local
 end
 
 let _ =

src/analyses/threadReturn.ml

@@ -43,7 +43,7 @@ struct
 
   let startstate v = true
   let threadenter ctx lval f args = true
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let query ctx x =

src/analyses/uninit.ml

@@ -28,7 +28,7 @@ struct
 
   let startstate v : D.t = D.empty ()
   let threadenter ctx lval f args : D.t = D.empty ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
   (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain

src/analyses/unit.ml

@@ -36,7 +36,7 @@ struct
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end
 

src/analyses/varEq.ml

@@ -48,7 +48,7 @@ struct
 
   let startstate v = D.top ()
   let threadenter ctx lval f args = D.top ()
-  let threadspawn ctx lval f args fctx = D.bot ()
+  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   let const_equal c1 c2 =