From 8a95c8a2d4fa776624da179a803c021058563577 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 27 Nov 2023 12:29:07 +0200 Subject: [PATCH] Add multiple flag to ThreadCreate --- src/analyses/base.ml | 22 +++++++++++----------- src/analyses/libraryDesc.ml | 2 +- src/analyses/libraryFunctions.ml | 4 ++-- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index bdae887b4a..3630395282 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1953,8 +1953,8 @@ 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 * bool = - let create_thread lval arg v = + 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 * bool) list = + let create_thread ~multiple lval arg v = try (* try to get function declaration *) let fd = Cilfacade.find_varinfo_fundec v in @@ -1963,7 +1963,7 @@ struct | Some x -> [x] | None -> List.map (fun x -> MyCFG.unknown_exp) fd.sformals in - Some (lval, v, args) + Some (lval, v, args, multiple) with Not_found -> if LF.use_special f.vname then None (* we handle this function *) else if isFunctionType v.vtype then @@ -1973,7 +1973,7 @@ struct | Some x -> [x] | None -> List.map (fun x -> MyCFG.unknown_exp) (Cil.argsToList v_args) in - Some (lval, v, args) + Some (lval, v, args, multiple) else ( M.debug ~category:Analyzer "Not creating a thread from %s because its type is %a" v.vname d_type v.vtype; None @@ -1982,7 +1982,7 @@ struct let desc = LF.find f in match desc.special args, f.vname with (* handling thread creations *) - | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg }, _ -> begin + | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg; multiple }, _ -> begin (* extra sync so that we do not analyze new threads with bottom global invariant *) publish_all ctx `Thread; (* Collect the threads. *) @@ -1994,7 +1994,7 @@ struct else start_funvars in - List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown, false + List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown 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. @@ -2008,8 +2008,8 @@ struct 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 non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs; - List.filter_map (create_thread None None) addrs, true - | _, _ -> [], false + List.filter_map (create_thread ~multiple:true None None) addrs + | _, _ -> [] let assert_fn ctx e refine = (* make the state meet the assertion in the rest of the code *) @@ -2140,9 +2140,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, 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 ~multiple)) forks; + let forks = 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.Tuple4.second forks); + List.iter (fun (lval, f, args, multiple) -> ctx.spawn ~multiple lval f args) forks; let st: store = ctx.local in let gs = ctx.global in let desc = LF.find f in diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 4997b306a9..e426c32235 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -53,7 +53,7 @@ type special = | Assert of { exp: Cil.exp; check: bool; refine: bool; } | Lock of { lock: Cil.exp; try_: bool; write: bool; return_on_success: bool; } | Unlock of Cil.exp - | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; } + | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool } | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; } | ThreadExit of { ret_val: Cil.exp; } | Signal of Cil.exp diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index b94f751568..ab0d04d3ec 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -422,7 +422,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ (** Pthread functions. *) let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ - ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *) + ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *) ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *) ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval}); ("pthread_kill", unknown [drop "thread" []; drop "sig" []]); @@ -1007,7 +1007,7 @@ let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock (** LDV Klever functions. *) let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ - ("pthread_create_N", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* TODO: add multiple flag to ThreadCreate *) + ("pthread_create_N", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = true }); ("pthread_join_N", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval}); ("ldv_mutex_model_lock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("ldv_mutex_model_unlock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Unlock lock);