|
|
|
|
@ -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@[<v>%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@[<v>%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
|
|
|
|
|
|
Cristiano Calcagno
9 years ago