From 7f8511c2df35943acb82e4e1a83d47101973d2a4 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 14 May 2018 03:55:46 -0700 Subject: [PATCH] [Summary] move Stats and Status to modules Reviewed By: ngorogiannis Differential Revision: D7972093 fbshipit-source-id: 422a68c --- infer/src/absint/NodePrinter.ml | 2 +- infer/src/backend/InferPrint.ml | 13 ++-- infer/src/backend/Summary.ml | 95 ++++++++++++++++++++---------- infer/src/backend/Summary.mli | 49 +++++++++------ infer/src/backend/ondemand.ml | 14 ++--- infer/src/backend/printer.ml | 9 +-- infer/src/biabduction/interproc.ml | 16 +++-- 7 files changed, 120 insertions(+), 78 deletions(-) diff --git a/infer/src/absint/NodePrinter.ml b/infer/src/absint/NodePrinter.ml index bb0caa3eb..2c6b760d2 100644 --- a/infer/src/absint/NodePrinter.ml +++ b/infer/src/absint/NodePrinter.ml @@ -19,7 +19,7 @@ let new_session node = | None -> 0 | Some summary -> - (summary.stats).nodes_visited_fp <- IntSet.add node_id summary.stats.nodes_visited_fp ; + Summary.Stats.add_visited_fp summary.stats node_id ; incr summary.Summary.sessions ; !(summary.Summary.sessions) diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index a458249a7..d44c5415a 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -119,12 +119,11 @@ let summary_values summary = let pp fmt = Pp.seq pp_line fmt lines_visited in F.asprintf "%t" pp in - let pp_failure failure = F.asprintf "%a" SymOp.pp_failure_kind failure in { vname= Typ.Procname.to_string proc_name ; vname_id= Typ.Procname.to_filename proc_name ; vspecs= List.length specs - ; vto= Option.value_map ~f:pp_failure ~default:"NONE" stats.Summary.stats_failure - ; vsymop= stats.Summary.symops + ; vto= Summary.Stats.failure_kind_to_string stats + ; vsymop= Summary.Stats.symops stats ; verr= Errlog.size (fun ekind in_footprint -> @@ -500,7 +499,7 @@ module Stats = struct let is_verified = specs <> [] && not is_defective in let is_checked = not (is_defective || is_verified) in let is_timeout = - match Summary.(summary.stats.stats_failure) with + match Summary.(Stats.failure_kind summary.stats) with | None | Some (FKcrash _) -> false | _ -> @@ -545,8 +544,8 @@ module StatsLogs = struct let lang = Typ.Procname.get_language proc_name in let stats = EventLogger.AnalysisStats - { analysis_nodes_visited= IntSet.cardinal summary.stats.nodes_visited_re - ; analysis_status= summary.stats.stats_failure + { analysis_nodes_visited= Summary.Stats.nb_visited_re summary.stats + ; analysis_status= Summary.Stats.failure_kind summary.stats ; analysis_total_nodes= Summary.get_proc_desc summary |> Procdesc.get_nodes_num ; clang_method_kind= (match lang with Language.Clang -> Some clang_method_kind | _ -> None) @@ -554,7 +553,7 @@ module StatsLogs = struct ; method_location= Summary.get_loc summary ; method_name= Typ.Procname.to_string proc_name ; num_preposts - ; symops= summary.stats.symops } + ; symops= Summary.Stats.symops summary.stats } in EventLogger.log stats end diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 6fd1060cc..ecd971ef6 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -12,19 +12,67 @@ open! IStd module F = Format open PolyVariantEqual -type stats = - { stats_failure: SymOp.failure_kind option - ; symops: int - ; mutable nodes_visited_fp: IntSet.t - ; mutable nodes_visited_re: IntSet.t } +module Stats = struct + type t = + { failure_kind: SymOp.failure_kind option + (** what type of failure stopped the analysis (if any) *) + ; symops: int (** Number of SymOp's throughout the whole analysis of the function *) + ; mutable nodes_visited_fp: IntSet.t (** Nodes visited during the footprint phase *) + ; mutable nodes_visited_re: IntSet.t (** Nodes visited during the re-execution phase *) } -type status = Pending | Analyzed [@@deriving compare] + let empty = + {failure_kind= None; symops= 0; nodes_visited_fp= IntSet.empty; nodes_visited_re= IntSet.empty} -let string_of_status = function Pending -> "Pending" | Analyzed -> "Analyzed" -let pp_status fmt status = F.pp_print_string fmt (string_of_status status) + let is_visited_fp stats node_id = IntSet.mem node_id stats.nodes_visited_fp -let equal_status = [%compare.equal : status] + let is_visited_re stats node_id = IntSet.mem node_id stats.nodes_visited_re + + let add_visited_fp stats node_id = + stats.nodes_visited_fp <- IntSet.add node_id stats.nodes_visited_fp + + + let add_visited_re stats node_id = + stats.nodes_visited_re <- IntSet.add node_id stats.nodes_visited_re + + + let nb_visited_re {nodes_visited_re} = IntSet.cardinal nodes_visited_re + + let update ?(add_symops= 0) ?failure_kind stats = + let symops = stats.symops + add_symops in + let failure_kind = match failure_kind with None -> stats.failure_kind | some -> some in + {stats with symops; failure_kind} + + + let failure_kind {failure_kind} = failure_kind + + let symops {symops} = symops + + let pp_failure_kind_opt fmt failure_kind_opt = + match failure_kind_opt with + | Some failure_kind -> + SymOp.pp_failure_kind fmt failure_kind + | None -> + F.pp_print_string fmt "NONE" + + + let failure_kind_to_string {failure_kind} = F.asprintf "%a" pp_failure_kind_opt failure_kind + + let pp fmt {failure_kind; symops} = + F.fprintf fmt "FAILURE:%a SYMOPS:%d@\n" pp_failure_kind_opt failure_kind symops +end + +module Status = struct + type t = + | Pending (** the summary has been created by the procedure has not been analyzed yet *) + | Analyzed (** the analysis of the procedure is finished *) + + let to_string = function Pending -> "Pending" | Analyzed -> "Analyzed" + + let pp fmt status = F.pp_print_string fmt (to_string status) + + let is_analyzed = function Analyzed -> true | _ -> false +end type payload = { annot_map: AnnotReachabilityDomain.astate option @@ -41,7 +89,8 @@ type payload = ; cost: CostDomain.summary option ; starvation: StarvationDomain.summary option } -type t = {payload: payload; sessions: int ref; stats: stats; status: status; proc_desc: Procdesc.t} +type t = + {payload: payload; sessions: int ref; stats: Stats.t; status: Status.t; proc_desc: Procdesc.t} let get_status summary = summary.status @@ -65,23 +114,11 @@ let cache : cache = Typ.Procname.Hash.create 128 let clear_cache () = Typ.Procname.Hash.clear cache -let pp_failure_kind_opt fmt failure_kind_opt = - match failure_kind_opt with - | Some failure_kind -> - SymOp.pp_failure_kind fmt failure_kind - | None -> - F.pp_print_string fmt "NONE" - - let pp_errlog fmt err_log = F.fprintf fmt "ERRORS: @[%a@]@\n%!" Errlog.pp_errors err_log ; F.fprintf fmt "WARNINGS: @[%a@]" Errlog.pp_warnings err_log -let pp_stats fmt stats = - F.fprintf fmt "FAILURE:%a SYMOPS:%d@\n" pp_failure_kind_opt stats.stats_failure stats.symops - - (** Return the signature of a procedure declaration as a string *) let get_signature summary = let s = ref "" in @@ -97,7 +134,7 @@ let get_signature summary = let pp_no_stats_specs fmt summary = F.fprintf fmt "%s@\n" (get_signature summary) ; - F.fprintf fmt "%a@\n" pp_status summary.status + F.fprintf fmt "%a@\n" Status.pp summary.status let pp_payload pe fmt @@ -145,7 +182,7 @@ let pp_payload pe fmt let pp_text fmt summary = let pe = Pp.text in pp_no_stats_specs fmt summary ; - F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) pp_stats summary.stats (pp_payload pe) + F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) Stats.pp summary.stats (pp_payload pe) summary.payload @@ -154,7 +191,7 @@ let pp_html source color fmt summary = Io_infer.Html.pp_start_color fmt Black ; F.fprintf fmt "@\n%a" pp_no_stats_specs summary ; Io_infer.Html.pp_end_color fmt () ; - F.fprintf fmt "
%a
@\n" pp_stats summary.stats ; + F.fprintf fmt "
%a
@\n" Stats.pp summary.stats ; Errlog.pp_html source [] fmt (get_err_log summary) ; Io_infer.Html.pp_hline fmt () ; F.fprintf fmt "@\n" ; @@ -162,10 +199,6 @@ let pp_html source color fmt summary = F.fprintf fmt "@\n" -let empty_stats = - {stats_failure= None; symops= 0; nodes_visited_fp= IntSet.empty; nodes_visited_re= IntSet.empty} - - (** Add the summary to the table for the given function *) let add (proc_name: Typ.Procname.t) (summary: t) : unit = Typ.Procname.Hash.replace cache proc_name summary @@ -270,7 +303,7 @@ let pdesc_resolve_attributes proc_desc = (** Save summary for the procedure into the spec database *) let store (summ: t) = - let final_summary = {summ with status= Analyzed} in + let final_summary = {summ with status= Status.Analyzed} in let proc_name = get_proc_name final_summary in (* Make sure the summary in memory is identical to the saved one *) add proc_name final_summary ; @@ -300,7 +333,7 @@ let empty_payload = initializes the summary for [proc_name] given dependent procs in list [depend_list]. *) let init_summary proc_desc = let summary = - {sessions= ref 0; payload= empty_payload; stats= empty_stats; status= Pending; proc_desc} + {sessions= ref 0; payload= empty_payload; stats= Stats.empty; status= Status.Pending; proc_desc} in Typ.Procname.Hash.replace cache (Procdesc.get_proc_name proc_desc) summary ; summary diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index d5579ac13..74c08f6e8 100644 --- a/infer/src/backend/Summary.mli +++ b/infer/src/backend/Summary.mli @@ -13,22 +13,37 @@ open! IStd (** Procedure summaries: the results of the capture and all the analysis for a single procedure, plus some statistics *) -(** Execution statistics *) -type stats = - { stats_failure: SymOp.failure_kind option - (** what type of failure stopped the analysis (if any) *) - ; symops: int (** Number of SymOp's throughout the whole analysis of the function *) - ; mutable nodes_visited_fp: IntSet.t (** Nodes visited during the footprint phase *) - ; mutable nodes_visited_re: IntSet.t (** Nodes visited during the re-execution phase *) } +module Stats : sig + (** Execution statistics *) + type t -(** Analysis status of the procedure *) -type status = - | Pending (** the summary has been created by the procedure has not been analyzed yet *) - | Analyzed (** the analysis of the procedure is finished *) + val add_visited_fp : t -> int -> unit -val equal_status : status -> status -> bool + val add_visited_re : t -> int -> unit -val string_of_status : status -> string + val is_visited_fp : t -> int -> bool + + val is_visited_re : t -> int -> bool + + val nb_visited_re : t -> int + + val update : ?add_symops:int -> ?failure_kind:SymOp.failure_kind -> t -> t + + val failure_kind : t -> SymOp.failure_kind option + + val failure_kind_to_string : t -> string + + val symops : t -> int +end + +module Status : sig + (** Analysis status of the procedure *) + type t + + val is_analyzed : t -> bool + + val to_string : t -> string +end (** analysis results *) type payload = @@ -49,9 +64,9 @@ type payload = (** summary of a procedure name *) type t = { payload: payload - ; sessions: int ref (** Session number: how many nodes went trough symbolic execution *) - ; stats: stats - ; status: status + ; sessions: int ref (** Session number: how many nodes went through symbolic execution *) + ; stats: Stats.t + ; status: Status.t ; proc_desc: Procdesc.t } val dummy : t @@ -90,7 +105,7 @@ val get_signature : t -> string val get_unsafe : Typ.Procname.t -> t (** @deprecated Return the summary for the procedure name. Raises an exception when not found. *) -val get_status : t -> status +val get_status : t -> Status.t (** Return the status (active v.s. inactive) of a procedure summary *) val reset : Procdesc.t -> t diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index e7e02eb77..6ff01349e 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -50,16 +50,16 @@ let should_create_summary proc_name proc_attributes = let should_be_analyzed proc_name proc_attributes = - let already_analyzed () = + let already_analyzed proc_name = match Summary.get proc_name with | Some summary -> - Summary.equal_status (Summary.get_status summary) Summary.Analyzed + Summary.(Status.is_analyzed (get_status summary)) | None -> false in should_create_summary proc_name proc_attributes && not (is_active proc_name) && (* avoid infinite loops *) - not (already_analyzed ()) + not (already_analyzed proc_name) let procedure_should_be_analyzed proc_name = @@ -133,16 +133,16 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc = log_elapsed_time () ; summary in - let log_error_and_continue exn summary kind = + let log_error_and_continue exn (summary: Summary.t) kind = Reporting.log_error summary exn ; - let stats = {summary.Summary.stats with Summary.stats_failure= Some kind} in + let stats = Summary.Stats.update summary.stats ~failure_kind:kind in let payload = let biabduction = Some BiabductionSummary.{preposts= []; phase= Tabulation.get_phase summary} in - {summary.Summary.payload with Summary.biabduction} + {summary.payload with Summary.biabduction} in - let new_summary = {summary with Summary.stats; payload} in + let new_summary = {summary with stats; payload} in Summary.store new_summary ; remove_active callee_pname ; log_elapsed_time () ; new_summary in let old_state = save_global_state () in diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 47a1bae7f..f88e0d96a 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -77,12 +77,9 @@ let node_is_visited node = (false, false) | Some summary -> let stats = summary.Summary.stats in - let is_visited_fp = - IntSet.mem (Procdesc.Node.get_id node :> int) stats.Summary.nodes_visited_fp - in - let is_visited_re = - IntSet.mem (Procdesc.Node.get_id node :> int) stats.Summary.nodes_visited_re - in + let node_id = (Procdesc.Node.get_id node :> int) in + let is_visited_fp = Summary.Stats.is_visited_fp stats node_id in + let is_visited_re = Summary.Stats.is_visited_re stats node_id in (is_visited_fp, is_visited_re) diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 789536b50..f899763a6 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -396,11 +396,10 @@ let do_symbolic_execution exe_env proc_cfg handle_exn tenv (node: ProcCfg.Except let mark_visited summary node = - let node_id = Procdesc.Node.get_id node in + let node_id = (Procdesc.Node.get_id node :> int) in let stats = summary.Summary.stats in - if !Config.footprint then - stats.Summary.nodes_visited_fp <- IntSet.add (node_id :> int) stats.Summary.nodes_visited_fp - else stats.Summary.nodes_visited_re <- IntSet.add (node_id :> int) stats.Summary.nodes_visited_re + if !Config.footprint then Summary.Stats.add_visited_fp stats node_id + else Summary.Stats.add_visited_re stats node_id let forward_tabulate exe_env tenv proc_cfg wl = @@ -439,7 +438,7 @@ let forward_tabulate exe_env tenv proc_cfg wl = match Tabulation.get_phase summary with FOOTPRINT -> "FP" | RE_EXECUTION -> "RE" in let status = Summary.get_status summary in - F.sprintf "[%s:%s] %s" phase_string (Summary.string_of_status status) + F.sprintf "[%s:%s] %s" phase_string (Summary.Status.to_string status) (Typ.Procname.to_string proc_name) in L.d_strln @@ -1121,11 +1120,10 @@ let update_specs tenv prev_summary phase (new_specs: BiabductionSummary.NormSpec let update_summary tenv prev_summary specs phase res = let normal_specs = List.map ~f:(BiabductionSummary.spec_normalize tenv) specs in let new_specs, _ = update_specs tenv prev_summary phase normal_specs in - let symops = prev_summary.Summary.stats.Summary.symops + SymOp.get_total () in - let stats_failure = - match res with None -> prev_summary.Summary.stats.Summary.stats_failure | Some _ -> res + let stats = + Summary.Stats.update prev_summary.Summary.stats ~add_symops:(SymOp.get_total ()) + ?failure_kind:res in - let stats = {prev_summary.Summary.stats with symops; stats_failure} in let preposts = match phase with | BiabductionSummary.FOOTPRINT ->