Spawn threads created from unknown functions as non-unique

src/analyses/abortUnless.ml

@@ -65,7 +65,7 @@ struct
     false
 
   let startstate v = false
-  let threadenter ctx lval f args = [false]
+  let threadenter ctx ~multiple lval f args = [false]
   let threadspawn ctx lval f args fctx = false
   let exitstate v = false
 end

src/analyses/accessAnalysis.ml

@@ -54,7 +54,7 @@ struct
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
-  let threadenter ctx lval f args = [()]
+  let threadenter ctx ~multiple lval f args = [()]
   let exitstate  v = ()
   let context fd d = ()
 

src/analyses/activeLongjmp.ml

@@ -26,7 +26,7 @@ struct
 
   (* Initial values don't really matter: overwritten at longjmp call. *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

src/analyses/activeSetjmp.ml

@@ -25,7 +25,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

src/analyses/apron/relationAnalysis.apron.ml

@@ -647,7 +647,7 @@ struct
 
   (* Thread transfer functions. *)
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let st = ctx.local in
     match Cilfacade.find_varinfo_fundec f with
     | fd ->

src/analyses/base.ml

@@ -1902,7 +1902,7 @@ struct
 
 
 
-  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list =
+  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list * bool =
     let create_thread lval arg v =
       try
         (* try to get function declaration *)
@@ -1943,7 +1943,7 @@ struct
           else
             start_funvars
         in
-        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
+        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown, false
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
@@ -1956,9 +1956,9 @@ struct
       let deep_flist = collect_invalidate ~deep:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local deep_args in
       let flist = shallow_flist @ deep_flist in
       let addrs = List.concat_map AD.to_var_may flist in
-      if addrs <> [] then M.debug ~category:Analyzer "Spawning functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
-      List.filter_map (create_thread None None) addrs
-    | _, _ -> []
+      if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
+      List.filter_map (create_thread None None) addrs, true
+    | _, _ -> [], false
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
@@ -2024,9 +2024,9 @@ struct
       let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
       (addr, AD.type_of addr)
     in
-    let forks = forkfun ctx lv f args in
+    let forks, multiple = forkfun ctx lv f args in
     if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple3.second forks);
-    List.iter (BatTuple.Tuple3.uncurry ctx.spawn) forks;
+    List.iter (BatTuple.Tuple3.uncurry (ctx.spawn ~multiple)) forks;
     let st: store = ctx.local in
     let gs = ctx.global in
     let desc = LF.find f in
@@ -2503,7 +2503,7 @@ struct
     in
     combine_one ctx.local after
 
-  let threadenter ctx (lval: lval option) (f: varinfo) (args: exp list): D.t list =
+  let threadenter ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list): D.t list =
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
       [make_entry ~thread:true ctx fd args]

src/analyses/condVars.ml

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

src/analyses/expsplit.ml

@@ -84,7 +84,7 @@ struct
     in
     emit_splits ctx d
 
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
 
   let threadspawn ctx lval f args fctx =
     emit_splits_ctx ctx

src/analyses/extractPthread.ml

@@ -1238,7 +1238,7 @@ module Spec : Analyses.MCPSpec = struct
       (Ctx.top ())
 
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let d : D.t = ctx.local in
     let tasks = ctx.global tasks_var in
     (* TODO: optimize finding *)

src/analyses/fileUse.ml

@@ -287,7 +287,7 @@ struct
     | _ -> m
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end

src/analyses/locksetAnalysis.ml

@@ -18,7 +18,7 @@ struct
   module C = D
 
   let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let exitstate  v = D.empty ()
 end
 

src/analyses/mCP.ml

@@ -140,9 +140,9 @@ struct
         f ((k,v::a')::a) b
     in f [] xs
 
-  let do_spawns ctx (xs:(varinfo * (lval option * exp list)) list) =
+  let do_spawns ctx (xs:(varinfo * (lval option * exp list * bool)) list) =
     let spawn_one v d =
-      List.iter (fun (lval, args) -> ctx.spawn lval v args) d
+      List.iter (fun (lval, args, multiple) -> ctx.spawn ~multiple lval v args) d
     in
     if not (get_bool "exp.single-threaded") then
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
@@ -322,8 +322,8 @@ struct
 
   and outer_ctx tfname ?spawns ?sides ?emits ctx =
     let spawn = match spawns with
-      | Some spawns -> (fun l v a  -> spawns := (v,(l,a)) :: !spawns)
-      | None -> (fun v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
+      | Some spawns -> (fun ?(multiple=false) l v a  -> spawns := (v,(l,a,multiple)) :: !spawns)
+      | None -> (fun ?(multiple=false) v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
     in
     let sideg = match sides with
       | Some sides -> (fun v g    -> sides  := (v, (!WideningTokens.side_tokens, g)) :: !sides)
@@ -565,13 +565,13 @@ struct
     let d = do_emits ctx !emits d q in
     if q then raise Deadcode else d
 
-  let threadenter (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
+  let threadenter (ctx:(D.t, G.t, C.t, V.t) ctx) ~multiple lval f a =
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "threadenter" ~sides ~emits ctx in
     let f (n,(module S:MCPSpec),d) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "threadenter" ctx'' n d in
-      map (fun d -> (n, repr d)) @@ S.threadenter ctx' lval f a
+      map (fun d -> (n, repr d)) @@ (S.threadenter ~multiple) ctx' lval f a
     in
     let css = map f @@ spec_list ctx.local in
     do_sideg ctx !sides;

src/analyses/mallocFresh.ml

@@ -52,7 +52,7 @@ struct
       | None -> ctx.local
       | Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.empty ()]
 
   let threadspawn ctx lval f args fctx =

src/analyses/malloc_null.ml

@@ -215,7 +215,7 @@ struct
   let name () = "malloc_null"
 
   let startstate v = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.empty ()
 

src/analyses/modifiedSinceLongjmp.ml

@@ -63,7 +63,7 @@ struct
       ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

src/analyses/mutexTypeAnalysis.ml

@@ -65,7 +65,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 

src/analyses/poisonVariables.ml

@@ -61,7 +61,7 @@ struct
     VS.join au ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let event ctx e octx =

src/analyses/pthreadSignals.ml

@@ -73,7 +73,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = Signals.empty ()
-  let threadenter ctx lval f args = [ctx.local]
+  let threadenter ctx ~multiple lval f args = [ctx.local]
   let exitstate  v = Signals.empty ()
 end
 

src/analyses/region.ml

@@ -175,7 +175,7 @@ struct
   let startstate v =
     `Lifted (RegMap.bot ())
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [`Lifted (RegMap.bot ())]
   let threadspawn ctx lval f args fctx = ctx.local
 

src/analyses/spec.ml

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

src/analyses/stackTrace.ml

@@ -21,7 +21,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 end
 
@@ -45,7 +45,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.top ()
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.push !Tracing.current_loc ctx.local]
 end
 

src/analyses/symbLocks.ml

@@ -29,7 +29,7 @@ struct
   let name () = "symb_locks"
 
   let startstate v = D.top ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 

src/analyses/taintPartialContexts.ml

@@ -101,7 +101,7 @@ struct
     d
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.bot ()]
   let threadspawn ctx lval f args fctx =
     match lval with

src/analyses/termination.ml

@@ -217,7 +217,7 @@ struct
   (* | _ -> ctx.local *)
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.bot ()
 end
 

src/analyses/threadAnalysis.ml

@@ -84,7 +84,13 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+
+  let threadenter ctx ~multiple lval f args =
+    if multiple then
+      (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
+       ctx.sideg tid (true, TS.bot (), false));
+    [D.bot ()]
+
   let threadspawn ctx lval f args fctx =
     let creator = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx fctx) in

src/analyses/threadEscape.ml

@@ -150,7 +150,7 @@ struct
   let startstate v = D.bot ()
   let exitstate  v = D.bot ()
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     [D.bot ()]
 
   let threadspawn ctx lval f args fctx =

src/analyses/threadFlag.ml

@@ -58,7 +58,7 @@ struct
   let access ctx _ =
     is_currently_multi (Analyses.ask_of_ctx ctx)
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
       ctx.emit Events.EnterMultiThreaded;
     [create_tid f]

src/analyses/threadId.ml

@@ -56,9 +56,9 @@ struct
       Hashtbl.replace !tids tid ();
     (N.bot (), `Lifted (tid), (TD.bot (), TD.bot ()))
 
-  let create_tid (_, current, (td, _)) ((node, index): Node.t * int option) v =
+  let create_tid ?(multiple=false) (_, current, (td, _)) ((node, index): Node.t * int option) v =
     match current with
-    | `Lifted current ->
+    | `Lifted current when not multiple ->
       let+ tid = Thread.threadenter (current, td) node index v in
       if GobConfig.get_bool "dbg.print_tids" then
         Hashtbl.replace !tids tid ();
@@ -133,9 +133,9 @@ struct
     | `Lifted node, count -> node, Some count
     | (`Bot | `Top), _ -> ctx.prev_node, None
 
-  let threadenter ctx lval f args:D.t list =
+  let threadenter ctx ~multiple lval f args:D.t list =
     let n, i = indexed_node_for_ctx ctx in
-    let+ tid = create_tid ctx.local (n, i) f in
+    let+ tid = create_tid ~multiple ctx.local (n, i) f in
     (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
 
   let threadspawn ctx lval f args fctx =

src/analyses/threadReturn.ml

@@ -28,7 +28,7 @@ struct
     ctx.local (* keep local as opposed to IdentitySpec *)
 
   let startstate v = true
-  let threadenter ctx lval f args = [true]
+  let threadenter ctx ~multiple lval f args = [true]
   let exitstate  v = D.top ()
 
   let query (ctx: (D.t, _, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =

src/analyses/tmpSpecial.ml

@@ -88,7 +88,7 @@ struct
     | _ -> Queries.Result.top q
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.bot ()
 end

src/analyses/tutorials/taint.ml

@@ -129,7 +129,7 @@ struct
 
   (* You may leave these alone *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+  let threadenter ctx ~multiple lval f args = [D.top ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 end

src/analyses/tutorials/unitAnalysis.ml

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

src/analyses/uninit.ml

@@ -25,7 +25,7 @@ struct
   let name () = "uninit"
 
   let startstate v : D.t = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()