diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 64d6c1436..7938bbd26 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -178,9 +178,6 @@ let forcing_delayed_prints = ref false (** If true, treat calls to no-arg getters as idempotent w.r.t non-nullness *) let idempotent_getters = ref true -(** Flag set when running in a child process (thus changes to global state will be lost *) -let in_child_process = ref false - (** if true, changes to code are checked at the procedure level; if false, at the file level *) let incremental_procs = ref true @@ -210,9 +207,6 @@ let nLOC = ref 0 (** max number of procedures in each cluster *) let max_cluster_size = ref 2000 -(** Maximum number of processes to be used for parallel execution *) -let max_num_proc = ref 0 - (** Maximum level of recursion during the analysis, after which a timeout is generated *) let max_recursion = ref 5 @@ -229,9 +223,6 @@ let monitor_prop_size = ref false (** Flag for using the nonempty lseg only **) let nelseg = ref false -(** Number of cores to be used for parallel execution *) -let num_cores = ref 1 - (** Flag to activate nonstop mode: the analysis continues after in encounters errors *) let nonstop = ref false diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index 1e0348d6f..32253643a 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -12,268 +12,12 @@ module L = Logging module F = Format open Utils -(* =============== START of module Process =============== *) - -module type Process_signature = -sig - type t - type val_t = (Procname.t * Cg.in_out_calls) (** type of values sent to children *) - val get_remaining_processes : unit -> t list (** return the list of remaining processes *) - val kill_remaining_processes : unit -> unit (** kill the remaining processes *) - val kill_process : t -> unit - val get_node_calls : t -> val_t option - val spawn_fun : (val_t -> Specs.summary) -> t - val send_to_child : t -> val_t -> unit - val receive_from_child : unit -> t * Specs.summary - val get_last_input : t -> val_t -end - -(** Implementation of the process interface for the simulator (processes are implemented just as functions) *) -module Process_simulate : Process_signature = struct - type t = int - type val_t = (Procname.t * Cg.in_out_calls) - let count = ref 0 - let funs = Hashtbl.create 17 - - let spawn_fun f = - incr count; - Hashtbl.add funs !count (f, None); - !count - - let get_remaining_processes () = - let ids = ref [] in - Hashtbl.iter (fun id _ -> ids := id :: !ids) funs; - list_rev !ids - - let kill_remaining_processes () = - Hashtbl.clear funs - - let kill_process id = - Hashtbl.remove funs id - - let get_node_calls p = - try - match Hashtbl.find funs p with - | (f, Some (x, res)) -> Some x - | _ -> None - with Not_found -> None - - let send_to_child id (x : val_t) = - let (f, _) = Hashtbl.find funs id in - Hashtbl.replace funs id (f, Some (x, f x)) - - let receive_from_child () : t * Specs.summary = - let some_id = ref (- 1) in - Hashtbl.iter (fun id _ -> some_id := id) funs; - match Hashtbl.find funs !some_id with - | (f, Some (x, res)) -> (!some_id, res) - | _ -> assert false - - let get_last_input id = - match Hashtbl.find funs id with - | (f, Some (x, res)) -> x - | _ -> assert false -end - -(** Implementation of the process interface using fork and pipes *) -module Process_fork : Process_signature = struct - - let shared_in, shared_out = (* shared channel from children to parent *) - let (read, write) = Unix.pipe () - in Unix.in_channel_of_descr read, Unix.out_channel_of_descr write - - type val_t = Procname.t * Cg.in_out_calls - - type pipe_str = - { p2c_in : in_channel; - p2c_out : out_channel; - c2p_in : in_channel; - c2p_out : out_channel; - mutable input : val_t option; - mutable pid : int } - - type t = pipe_str - - let processes = ref [] - - let get_node_calls p_str = - p_str.input - - let send_to_child p_str (v : val_t) = - p_str.input <- Some v; - Marshal.to_channel p_str.p2c_out v []; - flush p_str.p2c_out - - let incr_process_count p_str = - processes := p_str :: !processes - (* ; F.printf "@.Number of processes: %d@." (list_length !processes) *) - - let decr_process_count pid = - processes := list_filter (fun p_str' -> pid != p_str'.pid) !processes - (* ; F.printf "@.Number of processes: %d@." (list_length !processes) *) - - let kill_process p_str = - L.out "killing process %d@." p_str.pid; - Unix.kill p_str.pid Sys.sigkill; - Unix.close (Unix.descr_of_in_channel p_str.p2c_in); - Unix.close (Unix.descr_of_out_channel p_str.p2c_out); - Unix.close (Unix.descr_of_in_channel p_str.c2p_in); - Unix.close (Unix.descr_of_out_channel p_str.c2p_out); - ignore (Unix.waitpid [] p_str.pid); - decr_process_count p_str.pid - - let get_remaining_processes () = - !processes - - let kill_remaining_processes () = - L.out "@.%d remaining processes@." (list_length !processes); - list_iter kill_process !processes - - let rec receive_from_child () : t * Specs.summary = - let sender_pid = input_binary_int shared_in in - try - let p_str = (* find which process sent its pid on the shared channel *) - list_find (fun p_str -> p_str.pid = sender_pid) !processes in - let (summ : Specs.summary) = Marshal.from_channel p_str.c2p_in in - (p_str, summ) - with Not_found -> - L.err "@.ERROR: process %d was killed while trying to communicate with the parent@." sender_pid; - receive_from_child () (* wait for communication from the next process *) - - let receive_from_parent p_str : val_t = - Marshal.from_channel p_str.p2c_in - - let send_to_parent (p_str: t) (summ: Specs.summary) = - output_binary_int shared_out p_str.pid; (* tell parent I'm sending the result *) - flush shared_out; - Marshal.to_channel p_str.c2p_out summ []; - flush p_str.c2p_out - - let get_last_input p_str = - match p_str.input with - | None -> assert false - | Some x -> x - - let spawn_fun (service_f : val_t -> Specs.summary) = - let p_str = - let (p2c_read, p2c_write) = Unix.pipe () in - let (c2p_read, c2p_write) = Unix.pipe () in - (* Unix.set_nonblock c2p_read; *) - { p2c_in = Unix.in_channel_of_descr p2c_read; - p2c_out = Unix.out_channel_of_descr p2c_write; - c2p_in = Unix.in_channel_of_descr c2p_read; - c2p_out = Unix.out_channel_of_descr c2p_write; - input = None; - pid = 0 } in - let colour = L.next_colour () in - match Unix.fork () with - | 0 -> - Config.in_child_process := true; - p_str.pid <- Unix.getpid (); - L.change_terminal_colour colour; - L.out "@.STARTING PROCESS %d@." p_str.pid; - let rec loop () = - let n = receive_from_parent p_str in - let res = service_f n in - send_to_parent p_str res; - loop () in - loop () - | cid -> - p_str.pid <- cid; - incr_process_count p_str; - p_str -end - -(* =============== END of module Process =============== *) - -let parallel_mode = ref false - -(* =============== START of module Timing_log =============== *) -module Timing_log : sig - val event_start : string -> unit - val event_finish : string -> unit - val print_timing : unit -> unit -end = struct - type ev_kind = START | FINISH - type event = { time : float; kind : ev_kind; name : string } - - let active = ref [] - let log = ref [] - let bogus_time = - 1000.0 - let bogus_event = { time = bogus_time; kind = START; name ="" } - let last_event = ref bogus_event - let initial_time = ref bogus_time - let total_procs_time = ref 0.0 - let total_cores_time = ref 0.0 - - let reset () = - active := []; - log := []; - last_event := bogus_event; - initial_time := bogus_time; - total_procs_time := 0.0; - total_cores_time := 0.0 - - let expand_log event = - let elapsed = event.time -. !last_event.time in - let num_procs = list_length !active in - let num_cores = min num_procs !Config.num_cores in - match Pervasives.(=) !last_event bogus_event with - | true -> - last_event := event; - initial_time := event.time; - | false -> - let label = - list_fold_left (fun s name -> "\\n" ^ name ^s) "" (list_rev !active) in - if !Config.write_dotty then log := (!last_event, label, event)::!log; - total_procs_time := (float_of_int num_procs) *. elapsed +. !total_procs_time; - total_cores_time := (float_of_int num_cores) *. elapsed +. !total_cores_time; - last_event := event - - let event_start s = - expand_log { time = (Unix.gettimeofday ()); kind = START; name = s }; - active := s :: !active; - L.err " %d cores active@." (list_length !active) - - let event_finish s = - expand_log { time = (Unix.gettimeofday ()); kind = FINISH; name = s }; - active := list_filter (fun s' -> s' <> s) !active - - let print_timing () = - let total_time = !last_event.time -. !initial_time in - (* - let avg_num_proc = !total_procs_time /. total_time in - let avg_num_cores = !total_cores_time /. total_time in - *) - if !Config.write_dotty then begin - let pp_event fmt event = match event.kind with - | START -> F.fprintf fmt "\"%fs START %s\"" event.time event.name - | FINISH -> F.fprintf fmt "\"%fs FINISH %s\"" event.time event.name in - let pp_edge fmt (event1, label, event2) = - let color = match event1.kind with - | START -> "green" - | FINISH -> "red" in - F.fprintf fmt "%a -> %a [label=\"{%fs}%s\",color=\"%s\"]\n" pp_event event1 pp_event event2 (event2.time -. event1.time) label color in - let outc = open_out (DB.filename_to_string (DB.Results_dir.path_to_filename DB.Results_dir.Abs_root ["timing.dot"])) in - let fmt = F.formatter_of_out_channel outc in - F.fprintf fmt "digraph {\n"; - list_iter (pp_edge fmt) !log; - F.fprintf fmt "}@."; - close_out outc; - end; - reset (); - L.err "Analysis time: %fs@." total_time -end -(* =============== END of module Timing_log =============== *) - -(** print the timing stats, and generate timing.dot if in dotty mode *) -let print_timing () = - Timing_log.print_timing () - module WeightedPnameSet = Set.Make(struct type t = (Procname.t * Cg.in_out_calls) - let compare ((pn1: Procname.t), (calls1: Cg.in_out_calls)) ((pn2: Procname.t), (calls2: Cg.in_out_calls)) = + let compare + ((pn1: Procname.t), (calls1: Cg.in_out_calls)) + ((pn2: Procname.t), (calls2: Cg.in_out_calls)) = let n = int_compare calls1.Cg.in_calls calls2.Cg.in_calls in if n != 0 then n else Procname.compare pn1 pn2 end) @@ -295,12 +39,10 @@ let proc_is_up_to_date gr pname = match Specs.get_summary pname with | None -> false | Some summary -> - let filter dependent_proc = Specs.get_timestamp summary = - Procname.Map.find dependent_proc summary.Specs.dependency_map in - let res = - Specs.is_inactive pname && - Procname.Set.for_all filter (Cg.get_defined_children gr pname) in - res + let filter dependent_proc = + Specs.get_timestamp summary = + Procname.Map.find dependent_proc summary.Specs.dependency_map in + Procname.Set.for_all filter (Cg.get_defined_children gr pname) (** Return the list of procedures which should perform a phase transition from [FOOTPRINT] to [RE_EXECUTION] *) @@ -309,7 +51,6 @@ let should_perform_transition gr proc_name : Procname.t list = let recursive_dependents_plus_self = Procname.Set.add proc_name recursive_dependents in let should_transition = Specs.get_phase proc_name == Specs.FOOTPRINT && - Procname.Set.for_all (fun pn -> Specs.is_inactive pn) recursive_dependents && Procname.Set.for_all (proc_is_up_to_date gr) recursive_dependents in if should_transition then Procname.Set.elements recursive_dependents_plus_self else [] @@ -361,7 +102,10 @@ let update_specs proc_name (new_specs : Specs.NormSpec.t list) : Specs.NormSpec. (Paths.PathSet.from_renamed_list spec.Specs.posts, spec.Specs.visited) map) SpecMap.empty old_specs) in let re_exe_filter old_spec = (* filter out pres which failed re-exe *) - if phase == Specs.RE_EXECUTION && not (list_exists (fun new_spec -> Specs.Jprop.equal new_spec.Specs.pre old_spec.Specs.pre) new_specs) + if phase == Specs.RE_EXECUTION && + not (list_exists + (fun new_spec -> Specs.Jprop.equal new_spec.Specs.pre old_spec.Specs.pre) + new_specs) then begin changed:= true; L.out "Specs changed: removing pre of spec@\n%a@." (Specs.pp_spec pe_text None) old_spec; @@ -377,8 +121,12 @@ let update_specs proc_name (new_specs : Specs.NormSpec.t list) : Specs.NormSpec. Specs.Visitedset.union old_visited spec.Specs.visited in if not (Paths.PathSet.equal old_post new_post) then begin changed := true; - L.out "Specs changed: added new post@\n%a@." (Propset.pp pe_text (Specs.Jprop.to_prop spec.Specs.pre)) (Paths.PathSet.to_propset new_post); - current_specs := SpecMap.add spec.Specs.pre (new_post, new_visited) (SpecMap.remove spec.Specs.pre !current_specs) end + L.out "Specs changed: added new post@\n%a@." + (Propset.pp pe_text (Specs.Jprop.to_prop spec.Specs.pre)) + (Paths.PathSet.to_propset new_post); + current_specs := + SpecMap.add spec.Specs.pre (new_post, new_visited) + (SpecMap.remove spec.Specs.pre !current_specs) end with Not_found -> changed := true; @@ -411,7 +159,7 @@ let this_cluster_files = ref 1 (** Number of files in the current cluster *) let proc_is_done gr pname = not (WeightedPnameSet.mem (pname, Cg.get_calls gr pname) !wpnames_todo) -(** flag to activate tracing of the parallel algorithm *) +(** flag to activate tracing of the algorithm *) let trace = ref false (** Return true if [pname] has just become done *) @@ -420,7 +168,6 @@ let procs_become_done gr pname : Procname.t list = let nonrecursive_dependents = Cg.get_nonrecursive_dependents gr pname in let summary = Specs.get_summary_unsafe pname in let is_done = Specs.get_timestamp summary <> 0 && - Specs.is_inactive pname && (!Config.only_footprint || Specs.get_phase pname == Specs.RE_EXECUTION) && Procname.Set.for_all (proc_is_done gr) nonrecursive_dependents && Procname.Set.for_all (proc_is_up_to_date gr) recursive_dependents in @@ -453,21 +200,11 @@ let post_process_procs exe_env procs_done = end ) procs_done -(** Activate a check which ensures that multi-core mode gives the same result as one-core. - If true, detect when a dependent proc is active (analyzed concurrently) - and in that case wait for a process to terminate next *) -let one_core_compatibility_mode = ref true - -(** Find the max string in the [set] which satisfies [filter], and count the number of attempts. +(** Find the max string in the [set] which satisfies [filter],and count the number of attempts. Precedence is given to strings in [priority_set] *) let filter_max exe_env cg filter set priority_set = let rec find_max n filter set = let elem = WeightedPnameSet.max_elt set in - let check_one_core_compatibility () = - if !one_core_compatibility_mode && - Procname.Set.exists (fun child -> Specs.is_active child) (Cg.get_dependents cg (fst elem)) - then raise Not_found in - check_one_core_compatibility (); if filter elem then begin let proc_name = fst elem in @@ -476,25 +213,32 @@ let filter_max exe_env cg filter set priority_set = let action = if !Config.footprint then "Discovering" else "Verifying" in let pp_cluster_info fmt () = let files_done_previous_clusters = float_of_int !tot_files_done in - let ratio_procs_this_cluster = (float_of_int !num_procs_done) /. (float_of_int !tot_procs) in - let files_done_this_cluster = (float_of_int !this_cluster_files) *. ratio_procs_this_cluster in + let ratio_procs_this_cluster = + (float_of_int !num_procs_done) /. (float_of_int !tot_procs) in + let files_done_this_cluster = + (float_of_int !this_cluster_files) *. ratio_procs_this_cluster in let files_done = files_done_previous_clusters +. files_done_this_cluster in let perc_total = 100. *. files_done /. (float_of_int !tot_files) in F.fprintf fmt " (%3.2f%% total)" perc_total in - L.err "@\n**%s specs: %a file: %s@\n" action Procname.pp proc_name (DB.source_file_to_string file_name); - L.err " %d/%d procedures done%a@." !num_procs_done !tot_procs pp_cluster_info (); + L.err "@\n**%s specs: %a file: %s@\n" + action Procname.pp proc_name (DB.source_file_to_string file_name); + L.err " %d/%d procedures done%a@." + !num_procs_done !tot_procs pp_cluster_info (); elem end else begin find_max (n + 1) filter (WeightedPnameSet.remove elem set) end in - try find_max 1 filter (WeightedPnameSet.inter set priority_set) (* try with priority elements first *) + try + (* try with priority elements first *) + find_max 1 filter (WeightedPnameSet.inter set priority_set) with Not_found -> find_max 1 filter set (** Handle timeout events *) module Timeout : sig - val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option (* execute the function up to a given timeout given by the parameter *) + (** execute the function up to a given timeout given by the parameter *) + val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option end = struct let set_alarm nsecs = match Config.os_type with @@ -529,7 +273,8 @@ end = struct Sys.set_signal Sys.sigalrm (Sys.Signal_handle timeout_action) | Config.Win32 -> SymOp.set_wallclock_timeout_handler timeout_action; - ignore (Gc.create_alarm SymOp.check_wallclock_alarm) (* use the Gc alarm for periodic timeout checks *) + (* use the Gc alarm for periodic timeout checks *) + ignore (Gc.create_alarm SymOp.check_wallclock_alarm) end let exe_timeout iterations f x = @@ -553,13 +298,11 @@ end = struct raise exe end -module Process = Process_fork (** Main algorithm responsible for driving the analysis of an Exe_env (set of procedures). - The algorithm computes dependencies between procedures, spawns processes if required, + The algorithm computes dependencies between procedures, propagates results, and handles fixpoints in the call graph. *) -let parallel_execution exe_env num_processes analyze_proc filter_out process_result : unit = - parallel_mode := num_processes > 1 || !Config.max_num_proc > 0; +let main_algorithm exe_env analyze_proc filter_out process_result : unit = let call_graph = Exe_env.get_cg exe_env in let filter_initial (pname, w) = let summary = Specs.get_summary_unsafe pname in @@ -571,14 +314,11 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res WeightedPnameSet.filter (fun (n, _) -> address_taken_of n) !wpnames_todo in tot_procs := WeightedPnameSet.cardinal !wpnames_todo; num_procs_done := 0; - let avail_num = ref num_processes (* number of processors available *) in let max_timeout = ref 1 in - let wpname_can_be_analyzed (pname, weight) : bool = (* Return true if [pname] is not up to date and it can be analyzed right now *) - Specs.is_inactive pname && + let wpname_can_be_analyzed (pname, weight) : bool = + (* Return true if [pname] is not up to date and it can be analyzed right now *) Procname.Set.for_all (proc_is_done call_graph) (Cg.get_nonrecursive_dependents call_graph pname) && - Procname.Set.for_all - (fun child -> Specs.is_inactive child) (Cg.get_defined_children call_graph pname) && (Specs.get_timestamp (Specs.get_summary_unsafe pname) = 0 || not (proc_is_up_to_date call_graph pname)) in let process_one_proc pname (calls: Cg.in_out_calls) = @@ -595,84 +335,43 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res post_process_procs exe_env [pname] else begin - Specs.set_status pname Specs.ACTIVE; max_timeout := max (Specs.get_iterations pname) !max_timeout; Specs.update_dependency_map pname; - if !parallel_mode then - let p_str = Process.spawn_fun (analyze_proc exe_env) in - Timing_log.event_start (Procname.to_string pname); - Process.send_to_child p_str (pname, calls); - decr avail_num - else - begin - Timing_log.event_start (Procname.to_string pname); - process_result exe_env (pname, calls) (analyze_proc exe_env (pname, calls)); - Timing_log.event_finish (Procname.to_string pname) - end + process_result exe_env (pname, calls) (analyze_proc exe_env (pname, calls)); end in - let wait_for_next_result () = - try - match Timeout.exe_timeout (2 * !max_timeout) Process.receive_from_child () with - | None -> - let remaining_procedures = - let procs = list_map Process.get_node_calls (Process.get_remaining_processes ()) in - list_map (function None -> assert false | Some x -> x) procs in - L.err "No process is responding: killing %d pending processes@." (list_length remaining_procedures); - Process.kill_remaining_processes (); - let do_proc (pname, calls) = - let prev_summary = Specs.get_summary_unsafe pname in - let timestamp = max 1 (prev_summary.Specs.timestamp) in - let stats = { prev_summary.Specs.stats with Specs.stats_timeout = true } in - let summ = - { prev_summary with - Specs.stats = stats; - Specs.payload = Specs.PrePosts []; - Specs.timestamp = timestamp; - Specs.status = Specs.INACTIVE } in - process_result exe_env (pname, calls) summ; - Timing_log.event_finish (Procname.to_string pname); - incr avail_num in - list_iter do_proc remaining_procedures - | Some (p_str, summ) -> - let (pname, weight) = Process.get_last_input p_str in - (try - DB.current_source := - (Specs.get_summary_unsafe pname).Specs.attributes.ProcAttributes.loc.Location.file; - process_result exe_env (pname, weight) summ - with exn -> assert false); - Timing_log.event_finish (Procname.to_string pname); - Process.kill_process p_str; - incr avail_num - with - | Sys_blocked_io -> () in while not (WeightedPnameSet.is_empty !wpnames_todo) do - if !avail_num > 0 then - begin - if !trace then begin - let analyzable_pnames = WeightedPnameSet.filter wpname_can_be_analyzed !wpnames_todo in - L.err "Nodes todo: %a@\n" pp_weightedpnameset !wpnames_todo; - L.err "Analyzable procs: %a@\n" pp_weightedpnameset analyzable_pnames - end; - try - let pname, calls = filter_max exe_env call_graph wpname_can_be_analyzed !wpnames_todo wpnames_address_of in (** find max analyzable proc *) - process_one_proc pname calls - with Not_found -> (* no analyzable procs *) - if !avail_num < num_processes (* some other process is doing work *) - then wait_for_next_result () - else - (L.err "Error: can't analyze any procs. Printing current spec table@\n@[%a@]@." (Specs.pp_spec_table pe_text false) (); - raise (Failure "Stopping")) - end - else - wait_for_next_result () + begin + if !trace then begin + let analyzable_pnames = WeightedPnameSet.filter wpname_can_be_analyzed !wpnames_todo in + L.err "Nodes todo: %a@\n" pp_weightedpnameset !wpnames_todo; + L.err "Analyzable procs: %a@\n" pp_weightedpnameset analyzable_pnames + end; + try + let pname, calls = + (** find max analyzable proc *) + filter_max exe_env call_graph wpname_can_be_analyzed !wpnames_todo wpnames_address_of in + process_one_proc pname calls + with Not_found -> (* no analyzable procs *) + L.err "Error: can't analyze any procs. Printing current spec table@\n@[%a@]@." + (Specs.pp_spec_table pe_text false) (); + raise (Failure "Stopping") + end done -(** [parallel_iter_nodes cfg call_graph analyze_proc process_result filter_out] - executes [analyze_proc] in parallel as much as possible as allowed - by the call graph, and applies [process_result] to the result as - soon as it is returned by a child process. If [filter_out] returns - true, no execution. *) -let parallel_iter_nodes (exe_env: Exe_env.t) (_analyze_proc: Exe_env.t -> Procname.t -> 'a) (_process_result: Exe_env.t -> (Procname.t * Cg.in_out_calls) -> 'a -> unit) (filter_out: Cg.t -> Procname.t -> bool) : unit = +type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary + +type process_result = Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit + +type filter_out = Cg.t -> Procname.t -> bool + +(** Execute [analyze_proc] respecting dependencies between procedures, + and apply [process_result] to the result of the analysis. + If [filter_out] returns true, don't analyze the procedure. *) +let interprocedural_algorithm + (exe_env: Exe_env.t) + (_analyze_proc: analyze_proc) + (_process_result: process_result) + (filter_out: filter_out) : unit = let analyze_proc exe_env pname = (* wrap _analyze_proc and handle exceptions *) try _analyze_proc exe_env pname with | exn -> @@ -686,7 +385,8 @@ let parallel_iter_nodes (exe_env: Exe_env.t) (_analyze_proc: Exe_env.t -> Procna Specs.payload = Specs.PrePosts []; Specs.timestamp = timestamp } in summ in - let process_result exe_env (pname, calls) summary = (* wrap _process_result and handle exceptions *) + let process_result exe_env (pname, calls) summary = + (* wrap _process_result and handle exceptions *) try _process_result exe_env (pname, calls) summary with | exn -> let err_name, _, mloco, _, _, _, _ = Exceptions.recognize_exception exn in @@ -695,5 +395,5 @@ let parallel_iter_nodes (exe_env: Exe_env.t) (_analyze_proc: Exe_env.t -> Procna let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in Reporting.log_error pname exn'; post_process_procs exe_env [pname] in - let num_processes = if !Config.max_num_proc = 0 then !Config.num_cores else !Config.max_num_proc in - Unix.handle_unix_error (parallel_execution exe_env num_processes (fun exe_env (n, w) -> analyze_proc exe_env n) filter_out) process_result + main_algorithm + exe_env (fun exe_env (n, w) -> analyze_proc exe_env n) filter_out process_result diff --git a/infer/src/backend/fork.mli b/infer/src/backend/fork.mli index 2634e2cb1..53f8aee04 100644 --- a/infer/src/backend/fork.mli +++ b/infer/src/backend/fork.mli @@ -8,11 +8,12 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -(** Implementation of the Parallel Interprocedural Footprint Analysis Algorithm *) +(** Implementation of the Interprocedural Footprint Analysis Algorithm *) (** Handle timeout events *) module Timeout : sig - val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option (* execute the function up to a given timeout given by the iterations parameter *) + (** execute the function up to a given timeout given by the iterations parameter *) + val exe_timeout : int -> ('a -> 'b) -> 'a -> 'b option end val this_cluster_files : int ref (** Number of files in the current cluster *) @@ -35,12 +36,13 @@ val transition_footprint_re_exe : Procname.t -> Prop.normal Specs.Jprop.t list - (** Update the specs of the current proc after the execution of one phase *) val update_specs : Procname.t -> Specs.NormSpec.t list -> Specs.NormSpec.t list * bool -(** [parallel_iter_nodes tenv cfg call_graph analyze_proc process_result filter_out] - executes [analyze_proc] in parallel as much as possible as allowed - by the call graph, and applies [process_result] to the result as - soon as it is returned by a child process. If [filter_out] returns - true, no execution. *) -val parallel_iter_nodes : Exe_env.t -> (Exe_env.t -> Procname.t -> Specs.summary) -> (Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit) -> (Cg.t -> Procname.t -> bool) -> unit +type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary -(** print the timing stats, and generate timing.dot if in dotty mode *) -val print_timing : unit -> unit +type process_result = Exe_env.t -> (Procname.t * Cg.in_out_calls) -> Specs.summary -> unit + +type filter_out = Cg.t -> Procname.t -> bool + +(** Execute [analyze_proc] respecting dependencies between procedures, + and apply [process_result] to the result of the analysis. + If [filter_out] returns true, don't analyze the procedure. *) +val interprocedural_algorithm : Exe_env.t -> analyze_proc -> process_result -> filter_out -> unit diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index c0931d224..2a92a5fa2 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -221,7 +221,9 @@ module Simulator = struct (** Simulate the analysis only *) let process_result (exe_env: Exe_env.t) ((proc_name: Procname.t), (calls: Cg.in_out_calls)) (_summ: Specs.summary) : unit = L.err "in process_result %a@." Procname.pp proc_name; - let summ = { _summ with Specs.status = Specs.INACTIVE; Specs.stats = { _summ.Specs.stats with Specs.stats_calls = calls }} in + let summ = + { _summ with + Specs.stats = { _summ.Specs.stats with Specs.stats_calls = calls }} in Specs.add_summary proc_name summ; perform_transition exe_env proc_name; let procs_done = Fork.procs_become_done (Exe_env.get_cg exe_env) proc_name in @@ -250,7 +252,11 @@ let analyze exe_env = else if !simulate then (* simulate the analysis *) begin Simulator.reset_summaries (Exe_env.get_cg exe_env); - Fork.parallel_iter_nodes exe_env (Simulator.analyze_proc exe_env) Simulator.process_result Simulator.filter_out + Fork.interprocedural_algorithm + exe_env + (Simulator.analyze_proc exe_env) + Simulator.process_result + Simulator.filter_out end else (* full analysis *) begin @@ -805,8 +811,7 @@ let analyze_cluster cluster_num tot_clusters (cluster : cluster) = L.err "@.Processing cluster #%d/%d with %d files and %d procedures@." !cluster_num tot_clusters num_files num_procs; Fork.this_cluster_files := num_files; analyze exe_env; - Fork.tot_files_done := num_files + !Fork.tot_files_done; - Fork.print_timing () + Fork.tot_files_done := num_files + !Fork.tot_files_done let process_cluster_cmdline_exit () = match !cluster_cmdline with diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 7585c6006..98b7c3109 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1153,7 +1153,9 @@ let perform_transition exe_env cg proc_name = let process_result (exe_env: Exe_env.t) (proc_name, calls) (_summ: Specs.summary) : unit = if !Config.trace_anal then L.err "===process_result@."; Ident.reset_name_generator (); (* for consistency with multi-core mode *) - let summ = { _summ with Specs.status = Specs.INACTIVE; Specs.stats = { _summ.Specs.stats with Specs.stats_calls = calls }} in + let summ = + { _summ with + Specs.stats = { _summ.Specs.stats with Specs.stats_calls = calls }} in Specs.add_summary proc_name summ; let call_graph = Exe_env.get_cg exe_env in perform_transition exe_env call_graph proc_name; @@ -1213,7 +1215,6 @@ let filter_nospecs (pname, dep) = (** Perform the analysis of an exe_env *) let do_analysis exe_env = if !Config.trace_anal then L.err "do_analysis@."; - let do_parallel = !Config.num_cores > 1 || !Config.max_num_proc > 0 in let cg = Exe_env.get_cg exe_env in let procs_and_defined_children = get_procs_and_defined_children cg in let get_calls caller_pdesc = @@ -1244,10 +1245,7 @@ let do_analysis exe_env = else if !Config.only_nospecs then filter_nospecs else (fun _ -> true) in list_iter (fun x -> if filter x then init_proc x) procs_and_defined_children; - (try Fork.parallel_iter_nodes exe_env analyze_proc process_result filter_out with - exe when do_parallel -> - L.out "@.@. ERROR exception raised in parallel execution@."; - raise exe) + Fork.interprocedural_algorithm exe_env analyze_proc process_result filter_out let visited_and_total_nodes cfg = let all_nodes = diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index c18c86969..7d8484962 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -13,49 +13,6 @@ module F = Format open Utils -type colour = - C30 | C31 | C32 | C33 | C34 | C35 | C36 - -let black = C30 -let red = C31 -let green = C32 -let yellow = C33 -let blue = C34 -let magenta = C35 -let cyan = C36 - -let next_c = function - | C30 -> assert false - | C31 -> C32 - | C32 -> C33 - | C33 -> C34 - | C34 -> C35 - | C35 -> C36 - | C36 -> C31 - -let current_thread_colour = ref C31 - -let next_colour () = - let c = !current_thread_colour in - current_thread_colour := next_c c; - c - -let _set_print_colour fmt = function - | C30 -> F.fprintf fmt "\027[30m" - | C31 -> F.fprintf fmt "\027[31m" - | C32 -> F.fprintf fmt "\027[32m" - | C33 -> F.fprintf fmt "\027[33m" - | C34 -> F.fprintf fmt "\027[34m" - | C35 -> F.fprintf fmt "\027[35m" - | C36 -> F.fprintf fmt "\027[36m" - -let change_terminal_colour c = _set_print_colour F.std_formatter c -let change_terminal_colour_err c = _set_print_colour F.err_formatter c - -(** Can be applied to any number of arguments and throws them all away *) -let rec throw_away x = Obj.magic throw_away - -let use_colours = ref false (* =============== START of module MyErr =============== *) (** type of printable elements *) @@ -145,23 +102,7 @@ let reset_delayed_prints () = let get_delayed_prints () = !delayed_actions -let current_colour = ref black - -let set_colour c = - use_colours := true; - current_colour := c - let do_print fmt fmt_string = - begin - if !Config.num_cores > 1 then - begin - if !Config.in_child_process - then change_terminal_colour !current_thread_colour - else change_terminal_colour black - end - else if !use_colours then - change_terminal_colour !current_colour - end; F.fprintf fmt fmt_string (** print on the out stream *) diff --git a/infer/src/backend/logging.mli b/infer/src/backend/logging.mli index e05757e82..806f44d96 100644 --- a/infer/src/backend/logging.mli +++ b/infer/src/backend/logging.mli @@ -12,22 +12,6 @@ open Utils (** log messages at different levels of verbosity *) -type colour - -val black : colour -val red : colour -val green : colour -val yellow : colour -val blue : colour -val magenta : colour -val cyan : colour - -(** Return the next "coloured" (i.e. not black) colour *) -val next_colour : unit -> colour - -(** Print escape code to change the terminal's colour *) -val change_terminal_colour : colour -> unit - (** type of printable elements *) type print_type = | PTatom @@ -84,9 +68,6 @@ val get_delayed_prints : unit -> print_action list (** reset the delayed print actions *) val reset_delayed_prints : unit -> unit -(** Set the colours of the printer *) -val set_colour : colour -> unit - (** print to the current out stream *) val out : ('a, Format.formatter, unit) format -> 'a diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index ac4456596..28e15c166 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -836,13 +836,11 @@ let reserved_arg_desc = "-html", Arg.Set Config.write_html, None, "produce hmtl output in the results directory"; "-join_cond", Arg.Set_int Config.join_cond, Some "n", "set the strength of the final information-loss check used by the join (default n=1)"; "-leak", Arg.Set Config.allowleak, None, "forget leaks during abstraction"; - "-max_procs", Arg.Set_int Config.max_num_proc, Some "n", "set the maximum number of processes to be used for parallel execution (default n=0)"; "-monitor_prop_size", Arg.Set Config.monitor_prop_size, None, "monitor size of props"; "-nelseg", Arg.Set Config.nelseg, None, "use only nonempty lsegs"; "-noliveness", Arg.Clear Config.liveness, None, "turn the dead program variable elimination off"; "-noprintdiff", Arg.Clear Config.print_using_diff, None, "turn off highlighting diff w.r.t. previous prop in printing"; "-notest", Arg.Clear Config.test, None, "turn test mode off"; - "-num_cores", Arg.Set_int Config.num_cores, Some "n", "set the number of cores used in parallel by the analysis (default n=1)"; "-only_footprint", Arg.Set Config.only_footprint, None, "skip the re-execution phase"; "-print_types", Arg.Set Config.print_types, None, "print types in symbolic heaps"; "-set_pp_margin", Arg.Int (fun i -> F.set_margin i), Some "n", "set right margin for the pretty printing functions";