Skip to content

Commit

Permalink
Add multiple flag to ThreadCreate
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Nov 27, 2023
1 parent 670e7cf commit 8a95c8a
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 14 deletions.
22 changes: 11 additions & 11 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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. *)
Expand All @@ -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.
Expand All @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/libraryDesc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/analyses/libraryFunctions.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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" []]);
Expand Down Expand Up @@ -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);
Expand Down

0 comments on commit 8a95c8a

Please sign in to comment.