Summary:public Remove back-end infrastructure that exists only when on-demand mode is disabled. This, together with removing a few command-line options, sheds a lot of weight in the back-end. No changes expected for on-demand mode. Reviewed By: sblackshear Differential Revision: D2960242 fb-gh-sync-id: 220d821 shipit-source-id: 220d821master
Cristiano Calcagno
9 years ago
committed by
Facebook Github Bot 1
parent
761902afad
commit
89a2f2a7b4
@ -0,0 +1,31 @@
|
||||
(*
|
||||
* Copyright (c) 2016 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
module L = Logging
|
||||
module F = Format
|
||||
|
||||
(** Module to process clusters of procedures. *)
|
||||
|
||||
(** a cluster is a file *)
|
||||
type t = DB.source_dir
|
||||
|
||||
(** type stored in .cluster file: (n,m,cl) indicates cl is cluster n out of m *)
|
||||
type serializer_t = int * int * t
|
||||
|
||||
(** Load a cluster from a file *)
|
||||
val load_from_file : DB.filename -> serializer_t option
|
||||
|
||||
(** Print a cluster *)
|
||||
val pp_cluster : int -> int -> t -> F.formatter -> unit -> unit
|
||||
|
||||
(** Print a cluster name *)
|
||||
val pp_cluster_name : F.formatter -> int -> unit
|
||||
|
||||
(** Print clusters *)
|
||||
val print_clusters : t list -> unit
|
||||
@ -1,351 +0,0 @@
|
||||
(*
|
||||
* Copyright (c) 2009 - 2013 Monoidics ltd.
|
||||
* Copyright (c) 2013 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
module L = Logging
|
||||
module F = Format
|
||||
|
||||
(** Procedure name with weight given by the number of in-calls.
|
||||
Used to form a set ordered by weight. *)
|
||||
module WeightedPname =
|
||||
struct
|
||||
type t = (Procname.t * Cg.in_out_calls)
|
||||
let compare (pn1, calls1) (pn2, calls2) =
|
||||
let n = int_compare calls1.Cg.in_calls calls2.Cg.in_calls in
|
||||
if n != 0 then n
|
||||
else Procname.compare pn1 pn2
|
||||
end
|
||||
|
||||
let weighted_pname_from_cg cg pname =
|
||||
(pname, Cg.get_calls cg pname)
|
||||
|
||||
module WeightedPnameSet =
|
||||
Set.Make(WeightedPname)
|
||||
|
||||
let pp_weightedpnameset fmt set =
|
||||
let f (pname, _) = F.fprintf fmt "%a@ " Procname.pp pname in
|
||||
WeightedPnameSet.iter f set
|
||||
|
||||
let compute_weighed_pnameset cg =
|
||||
let set = ref WeightedPnameSet.empty in
|
||||
let add_pname_calls (pn, _) =
|
||||
set := WeightedPnameSet.add (weighted_pname_from_cg cg pn) !set in
|
||||
IList.iter add_pname_calls (Cg.get_nodes_and_calls cg);
|
||||
!set
|
||||
|
||||
(* Return true if there are no children of [pname] whose specs
|
||||
have changed since [pname] was last analyzed. *)
|
||||
let proc_is_up_to_date cg pname =
|
||||
match Specs.get_summary pname with
|
||||
| None -> false
|
||||
| Some summary ->
|
||||
let filter dependent_proc =
|
||||
try
|
||||
Specs.get_timestamp summary =
|
||||
Procname.Map.find dependent_proc summary.Specs.dependency_map
|
||||
with Not_found -> (* can happen in on-demand *)
|
||||
true in
|
||||
Procname.Set.for_all filter (Cg.get_defined_children cg pname)
|
||||
|
||||
(** Return the list of procedures which should perform a phase
|
||||
transition from [FOOTPRINT] to [RE_EXECUTION] *)
|
||||
let should_perform_transition cg proc_name : Procname.t list =
|
||||
let recursive_dependents =
|
||||
if !Config.ondemand_enabled then Procname.Set.empty
|
||||
else Cg.get_recursive_dependents cg proc_name in
|
||||
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 (proc_is_up_to_date cg) recursive_dependents in
|
||||
if should_transition then Procname.Set.elements recursive_dependents_plus_self
|
||||
else []
|
||||
|
||||
(** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
|
||||
let transition_footprint_re_exe proc_name joined_pres =
|
||||
L.out "Transition %a from footprint to re-exe@." Procname.pp proc_name;
|
||||
let summary = Specs.get_summary_unsafe "transition_footprint_re_exe" proc_name in
|
||||
let summary' =
|
||||
if !Config.only_footprint then
|
||||
{ summary with
|
||||
Specs.phase = Specs.RE_EXECUTION;
|
||||
}
|
||||
else
|
||||
let specs =
|
||||
IList.map
|
||||
(fun jp ->
|
||||
Specs.spec_normalize
|
||||
{ Specs.pre = jp;
|
||||
posts = [];
|
||||
visited = Specs.Visitedset.empty })
|
||||
joined_pres in
|
||||
let payload =
|
||||
{ summary.Specs.payload with
|
||||
Specs.preposts = Some specs; } in
|
||||
let dependency_map =
|
||||
Specs.re_initialize_dependency_map summary.Specs.dependency_map in
|
||||
{ summary with
|
||||
Specs.timestamp = 0;
|
||||
phase = Specs.RE_EXECUTION;
|
||||
dependency_map;
|
||||
payload;
|
||||
} in
|
||||
Specs.add_summary proc_name summary'
|
||||
|
||||
module SpecMap = Map.Make (struct
|
||||
type t = Prop.normal Specs.Jprop.t
|
||||
let compare = Specs.Jprop.compare
|
||||
end)
|
||||
|
||||
(** Update the specs of the current proc after the execution of one phase *)
|
||||
let update_specs proc_name phase (new_specs : Specs.NormSpec.t list)
|
||||
: Specs.NormSpec.t list * bool =
|
||||
let new_specs = Specs.normalized_specs_to_specs new_specs in
|
||||
let old_specs = Specs.get_specs proc_name in
|
||||
let changed = ref false in
|
||||
let current_specs =
|
||||
ref
|
||||
(IList.fold_left
|
||||
(fun map spec ->
|
||||
SpecMap.add
|
||||
spec.Specs.pre
|
||||
(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 (IList.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;
|
||||
current_specs := SpecMap.remove old_spec.Specs.pre !current_specs end
|
||||
else () in
|
||||
let add_spec spec = (* add a new spec by doing union of the posts *)
|
||||
try
|
||||
let old_post, old_visited = SpecMap.find spec.Specs.pre !current_specs in
|
||||
let new_post, new_visited =
|
||||
Paths.PathSet.union
|
||||
old_post
|
||||
(Paths.PathSet.from_renamed_list spec.Specs.posts),
|
||||
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
|
||||
|
||||
with Not_found ->
|
||||
changed := true;
|
||||
L.out "Specs changed: added new pre@\n%a@." (Specs.Jprop.pp_short pe_text) spec.Specs.pre;
|
||||
current_specs :=
|
||||
SpecMap.add
|
||||
spec.Specs.pre
|
||||
((Paths.PathSet.from_renamed_list spec.Specs.posts), spec.Specs.visited)
|
||||
!current_specs in
|
||||
let res = ref [] in
|
||||
let convert pre (post_set, visited) =
|
||||
res :=
|
||||
Specs.spec_normalize
|
||||
{ Specs.pre = pre;
|
||||
Specs.posts = Paths.PathSet.elements post_set;
|
||||
Specs.visited = visited }:: !res in
|
||||
IList.iter re_exe_filter old_specs; (* filter out pre's which failed re-exe *)
|
||||
IList.iter add_spec new_specs; (* add new specs *)
|
||||
SpecMap.iter convert !current_specs;
|
||||
!res,!changed
|
||||
|
||||
module GlobalState =
|
||||
struct
|
||||
(** Total number of procedures to analyze *)
|
||||
let tot_procs =
|
||||
ref 0
|
||||
|
||||
(** Number of procedures done *)
|
||||
let num_procs_done =
|
||||
ref 0
|
||||
|
||||
(** Weighted pnames (procedure names with weight) to do *)
|
||||
let wpnames_todo =
|
||||
ref WeightedPnameSet.empty
|
||||
end
|
||||
|
||||
module G = GlobalState
|
||||
|
||||
(** Return true if [pname] is done and requires no further analysis *)
|
||||
let proc_is_done cg pname =
|
||||
not (WeightedPnameSet.mem (weighted_pname_from_cg cg pname) !G.wpnames_todo)
|
||||
|
||||
(** flag to activate tracing of the algorithm *)
|
||||
let trace = ref false
|
||||
|
||||
(** Return true if [pname] has just become done *)
|
||||
let procs_become_done cg pname : Procname.t list =
|
||||
let recursive_dependents = Cg.get_recursive_dependents cg pname in
|
||||
let nonrecursive_dependents = Cg.get_nonrecursive_dependents cg pname in
|
||||
let summary = Specs.get_summary_unsafe "procs_become_done" pname in
|
||||
let is_done = Specs.get_timestamp summary <> 0 &&
|
||||
(!Config.only_footprint || Specs.get_phase pname == Specs.RE_EXECUTION) &&
|
||||
Procname.Set.for_all (proc_is_done cg) nonrecursive_dependents &&
|
||||
Procname.Set.for_all (proc_is_up_to_date cg) recursive_dependents in
|
||||
if !trace then L.err "proc is%s done@." (if is_done then "" else " not");
|
||||
if is_done
|
||||
then
|
||||
let procs_to_remove =
|
||||
(* the proc itself if not recursive, otherwise all the recursive circle *)
|
||||
Procname.Set.add pname recursive_dependents in
|
||||
Procname.Set.elements procs_to_remove
|
||||
else []
|
||||
|
||||
let post_process_procs exe_env procs_done =
|
||||
let check_no_specs pn =
|
||||
if Specs.get_specs pn = [] then begin
|
||||
Errdesc.warning_err
|
||||
(Specs.get_summary_unsafe "post_process_procs" pn).Specs.attributes.ProcAttributes.loc
|
||||
"No specs found for %a@." Procname.pp pn
|
||||
end in
|
||||
let cg = Exe_env.get_cg exe_env in
|
||||
IList.iter (fun pn ->
|
||||
let elem = weighted_pname_from_cg cg pn in
|
||||
if WeightedPnameSet.mem elem !G.wpnames_todo then
|
||||
begin
|
||||
incr G.num_procs_done;
|
||||
G.wpnames_todo := WeightedPnameSet.remove elem !G.wpnames_todo;
|
||||
let whole_seconds = false in
|
||||
check_no_specs pn;
|
||||
Printer.proc_write_log whole_seconds (Exe_env.get_cfg exe_env pn) pn
|
||||
end
|
||||
) procs_done
|
||||
|
||||
(** 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 filter set priority_set =
|
||||
let rec find_max n filter set =
|
||||
let elem = WeightedPnameSet.max_elt set in
|
||||
if filter elem then
|
||||
begin
|
||||
let proc_name = fst elem in
|
||||
Config.footprint := Specs.get_phase proc_name = Specs.FOOTPRINT;
|
||||
let file_name = Exe_env.get_source exe_env proc_name in
|
||||
let action = if !Config.footprint then "Discovering" else "Verifying" 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@."
|
||||
!G.num_procs_done !G.tot_procs;
|
||||
elem
|
||||
end
|
||||
else
|
||||
begin
|
||||
find_max (n + 1) filter (WeightedPnameSet.remove elem set)
|
||||
end in
|
||||
try
|
||||
(* try with priority elements first *)
|
||||
find_max 1 filter (WeightedPnameSet.inter set priority_set)
|
||||
with Not_found -> find_max 1 filter set
|
||||
|
||||
|
||||
(** Main algorithm responsible for driving the analysis of an Exe_env (set of procedures).
|
||||
The algorithm computes dependencies between procedures,
|
||||
propagates results, and handles fixpoints in the call graph. *)
|
||||
let main_algorithm exe_env analyze_proc process_result : unit =
|
||||
let call_graph = Exe_env.get_cg exe_env in
|
||||
let filter_initial (pname, _) =
|
||||
let summary = Specs.get_summary_unsafe "main_algorithm" pname in
|
||||
Specs.get_timestamp summary = 0 in
|
||||
G.wpnames_todo :=
|
||||
WeightedPnameSet.filter filter_initial (compute_weighed_pnameset call_graph);
|
||||
let wpnames_address_of = (* subset of the procedures whose address is taken *)
|
||||
let address_taken_of n =
|
||||
Procname.Set.mem n (Cfg.get_priority_procnames (Exe_env.get_cfg exe_env n)) in
|
||||
WeightedPnameSet.filter (fun (n, _) -> address_taken_of n) !G.wpnames_todo in
|
||||
G.tot_procs := WeightedPnameSet.cardinal !G.wpnames_todo;
|
||||
G.num_procs_done := 0;
|
||||
let wpname_can_be_analyzed (pname, _) : 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) &&
|
||||
(Specs.get_timestamp (Specs.get_summary_unsafe "main_algorithm" pname) = 0
|
||||
|| not (proc_is_up_to_date call_graph pname)) in
|
||||
let process_one_proc ((pname, _) as elem) =
|
||||
DB.current_source :=
|
||||
(Specs.get_summary_unsafe "main_algorithm" pname)
|
||||
.Specs.attributes.ProcAttributes.loc.Location.file;
|
||||
if !trace then
|
||||
begin
|
||||
let whole_seconds = false in
|
||||
L.err "@[<v 3> *********** Summary of %a ***********@," Procname.pp pname;
|
||||
L.err "%a@]@\n"
|
||||
(Specs.pp_summary pe_text whole_seconds)
|
||||
(Specs.get_summary_unsafe "main_algorithm" pname)
|
||||
end;
|
||||
Specs.update_dependency_map pname;
|
||||
process_result exe_env elem (analyze_proc exe_env pname) in
|
||||
while not (WeightedPnameSet.is_empty !G.wpnames_todo) do
|
||||
begin
|
||||
if !trace then begin
|
||||
let analyzable_pnames = WeightedPnameSet.filter wpname_can_be_analyzed !G.wpnames_todo in
|
||||
L.err "Nodes todo: %a@\n" pp_weightedpnameset !G.wpnames_todo;
|
||||
L.err "Analyzable procs: %a@\n" pp_weightedpnameset analyzable_pnames
|
||||
end;
|
||||
try
|
||||
let elem =
|
||||
(** find max analyzable proc *)
|
||||
filter_max exe_env wpname_can_be_analyzed !G.wpnames_todo wpnames_address_of in
|
||||
process_one_proc elem
|
||||
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) ();
|
||||
if !Config.ondemand_enabled then G.wpnames_todo := WeightedPnameSet.empty
|
||||
else raise (Failure "Stopping")
|
||||
end
|
||||
done
|
||||
|
||||
type analyze_proc = Exe_env.t -> Procname.t -> Specs.summary
|
||||
|
||||
type process_result = Exe_env.t -> WeightedPname.t -> Specs.summary -> unit
|
||||
|
||||
(** Execute [analyze_proc] respecting dependencies between procedures,
|
||||
and apply [process_result] to the result of the analysis. *)
|
||||
let interprocedural_algorithm
|
||||
(exe_env: Exe_env.t)
|
||||
(_analyze_proc: analyze_proc)
|
||||
(_process_result: process_result)
|
||||
: unit =
|
||||
let analyze_proc exe_env pname = (* wrap _analyze_proc and handle exceptions *)
|
||||
let log_error_and_continue exn kind =
|
||||
Reporting.log_error pname exn;
|
||||
let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in
|
||||
let timestamp = max 1 (prev_summary.Specs.timestamp) in
|
||||
let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in
|
||||
let payload =
|
||||
{ prev_summary.Specs.payload with Specs.preposts = Some []; } in
|
||||
{ prev_summary with Specs.stats; payload; timestamp; } in
|
||||
|
||||
try _analyze_proc exe_env pname with
|
||||
| Analysis_failure_exe kind as exn ->
|
||||
(* in production mode, log the timeout/crash and continue with the summary we had before
|
||||
the failure occurred *)
|
||||
log_error_and_continue exn kind
|
||||
| exn ->
|
||||
(* this happens due to exceptions from assert false or some other unrecognized exception *)
|
||||
log_error_and_continue exn (FKcrash (Printexc.to_string exn)) in
|
||||
|
||||
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, _, _, _, _, _, _ = Exceptions.recognize_exception exn in
|
||||
let err_str = "process_result raised " ^ (Localise.to_string err_name) in
|
||||
L.err "Error: %s@." err_str;
|
||||
let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in
|
||||
Reporting.log_error pname exn';
|
||||
post_process_procs exe_env [pname] in
|
||||
main_algorithm exe_env analyze_proc process_result
|
||||
@ -1,34 +0,0 @@
|
||||
(*
|
||||
* Copyright (c) 2009 - 2013 Monoidics ltd.
|
||||
* Copyright (c) 2013 - present Facebook, Inc.
|
||||
* All rights reserved.
|
||||
*
|
||||
* This source code is licensed under the BSD style license found in the
|
||||
* LICENSE file in the root directory of this source tree. An additional grant
|
||||
* of patent rights can be found in the PATENTS file in the same directory.
|
||||
*)
|
||||
|
||||
(** Implementation of the Interprocedural Footprint Analysis Algorithm *)
|
||||
|
||||
val procs_become_done : Cg.t -> Procname.t -> Procname.t list
|
||||
|
||||
val post_process_procs : Exe_env.t -> Procname.t list -> unit
|
||||
|
||||
(** Return the list of procedures which should perform a phase
|
||||
transition from [FOOTPRINT] to [RE_EXECUTION] *)
|
||||
val should_perform_transition : Cg.t -> Procname.t -> Procname.t list
|
||||
|
||||
(** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
|
||||
val transition_footprint_re_exe : Procname.t -> Prop.normal Specs.Jprop.t list -> unit
|
||||
|
||||
(** Update the specs of the current proc after the execution of one phase *)
|
||||
val update_specs :
|
||||
Procname.t -> Specs.phase -> Specs.NormSpec.t list -> Specs.NormSpec.t list * bool
|
||||
|
||||
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
|
||||
|
||||
(** Execute [analyze_proc] respecting dependencies between procedures,
|
||||
and apply [process_result] to the result of the analysis. *)
|
||||
val interprocedural_algorithm : Exe_env.t -> analyze_proc -> process_result -> unit
|
||||
Loading…
Reference in new issue