Merge pull request #1187 from goblint/issue_843

Spawn threads created from unknown functions as non-unique

Author: michael-schwarz

src/analyses/abortUnless.ml

@@ -65,8 +65,8 @@ struct
     false
 
   let startstate v = false
-  let threadenter ctx lval f args = [false]
-  let threadspawn ctx lval f args fctx = false
+  let threadenter ctx ~multiple lval f args = [false]
+  let threadspawn ctx ~multiple 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 = ()
 
@@ -121,7 +121,7 @@ struct
     ctx.local
 
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx  ~multiple lval f args fctx =
     (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
     begin match lval with
       | None -> ()

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 ->
@@ -665,7 +665,7 @@ struct
       (* TODO: do something like base? *)
       failwith "relation.threadenter: unknown function"
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     ctx.local
 
   let event ctx e octx =

src/analyses/base.ml

@@ -1944,7 +1944,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 *)
@@ -1985,7 +1985,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.
@@ -1998,9 +1998,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 *)
@@ -2131,9 +2131,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
@@ -2641,7 +2641,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]
@@ -2651,7 +2651,7 @@ struct
       let st = special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) ctx.global st f args in
       [st]
 
-  let threadspawn ctx (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
+  let threadspawn ctx ~multiple (lval: lval option) (f: varinfo) (args: exp list) fctx: D.t =
     begin match lval with
       | Some lval ->
         begin match ThreadId.get_current (Analyses.ask_of_ctx fctx) with

src/analyses/basePriv.ml

@@ -893,7 +893,7 @@ end
 module MinePrivBase =
 struct
   include NoFinalize
-  include ConfCheck.RequireMutexPathSensInit
+  include ConfCheck.RequireMutexPathSensOneMainInit
   include MutexGlobals (* explicit not needed here because G is Prod anyway? *)
 
   let thread_join ?(force=false) ask get e st = st

src/analyses/commonPriv.ml

@@ -19,12 +19,14 @@ struct
       if not mutex_active then failwith "Privatization (to be useful) requires the 'mutex' analysis to be enabled (it is currently disabled)"
   end
 
-  module RequireMutexPathSensInit =
+  module RequireMutexPathSensOneMainInit =
   struct
     let init () =
       RequireMutexActivatedInit.init ();
       let mutex_path_sens = List.mem "mutex" (GobConfig.get_string_list "ana.path_sens") in
       if not mutex_path_sens then failwith "The activated privatization requires the 'mutex' analysis to be enabled & path sensitive (it is currently enabled, but not path sensitive)";
+      let mainfuns = List.length @@ GobConfig.get_list "mainfun" in
+      if not (mainfuns = 1) then failwith "The activated privatization requires exactly one main function to be specified";
       ()
   end
 

src/analyses/condVars.ml

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

src/analyses/expsplit.ml

@@ -84,9 +84,9 @@ 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 =
+  let threadspawn ctx ~multiple lval f args fctx =
     emit_splits_ctx ctx
 
   let event ctx (event: Events.t) octx =