From b71af05f0051fd0a4a37083505d08ca821ce2296 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 15 Oct 2018 05:30:35 -0700 Subject: [PATCH] Stats: merge visited_fp and visited_re Reviewed By: da319 Differential Revision: D10376556 fbshipit-source-id: a0db1485a --- infer/src/absint/NodePrinter.ml | 2 +- infer/src/backend/InferPrint.ml | 2 +- infer/src/backend/Summary.ml | 21 +++++---------------- infer/src/backend/Summary.mli | 10 +++------- infer/src/backend/printer.ml | 16 ++++------------ infer/src/biabduction/interproc.ml | 8 ++++---- 6 files changed, 18 insertions(+), 41 deletions(-) diff --git a/infer/src/absint/NodePrinter.ml b/infer/src/absint/NodePrinter.ml index f1ad46e70..3deee6371 100644 --- a/infer/src/absint/NodePrinter.ml +++ b/infer/src/absint/NodePrinter.ml @@ -17,7 +17,7 @@ let new_session node = | None -> 0 | Some summary -> - Summary.Stats.add_visited_fp summary.stats node_id ; + Summary.Stats.add_visited 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 a20b4ef03..57a97de48 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -614,7 +614,7 @@ module StatsLogs = struct let lang = Typ.Procname.get_language proc_name in let stats = EventLogger.AnalysisStats - { analysis_nodes_visited= Summary.Stats.nb_visited_re summary.stats + { analysis_nodes_visited= Summary.Stats.nb_visited 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= diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 6a17cc763..80933ca35 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -15,26 +15,15 @@ module Stats = struct { 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 *) } + ; mutable nodes_visited: IntSet.t (** Nodes visited *) } - let empty = - {failure_kind= None; symops= 0; nodes_visited_fp= IntSet.empty; nodes_visited_re= IntSet.empty} + let empty = {failure_kind= None; symops= 0; nodes_visited= IntSet.empty} + let is_visited stats node_id = IntSet.mem node_id stats.nodes_visited - let is_visited_fp stats node_id = IntSet.mem node_id stats.nodes_visited_fp + let add_visited stats node_id = stats.nodes_visited <- IntSet.add node_id stats.nodes_visited - 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 nb_visited {nodes_visited} = IntSet.cardinal nodes_visited let update ?(add_symops = 0) ?failure_kind stats = let symops = stats.symops + add_symops in diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index 1108d98c5..e0869bfcd 100644 --- a/infer/src/backend/Summary.mli +++ b/infer/src/backend/Summary.mli @@ -15,15 +15,11 @@ module Stats : sig (** Execution statistics *) type t - val add_visited_fp : t -> int -> unit + val add_visited : t -> int -> unit - val add_visited_re : t -> int -> unit + val is_visited : t -> int -> bool - val is_visited_fp : t -> int -> bool - - val is_visited_re : t -> int -> bool - - val nb_visited_re : t -> int + val nb_visited : t -> int val update : ?add_symops:int -> ?failure_kind:SymOp.failure_kind -> t -> t diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index efbc74d86..971b5d595 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -67,23 +67,15 @@ end (** Current formatter for the html output *) let curr_html_formatter = ref F.std_formatter -(** Return true if the node was visited during footprint and during re-execution*) -let node_is_visited node = +(** Return true if the node was visited during analysis *) +let is_visited node = match Summary.get (Procdesc.Node.get_proc_name node) with | None -> - (false, false) + false | Some summary -> let stats = summary.Summary.stats 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) - - -(** Return true if the node was visited during analysis *) -let is_visited node = - let visited_fp, visited_re = node_is_visited node in - visited_fp || visited_re + Summary.Stats.is_visited stats node_id let pp_node_link path_to_root ?proof_cover ~description fmt node = diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 1df50b5cd..13ad15397 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -401,10 +401,10 @@ let do_symbolic_execution exe_env summary proc_cfg handle_exn tenv let mark_visited summary node = - let node_id = (Procdesc.Node.get_id node :> int) in - let stats = summary.Summary.stats in - if !BiabductionConfig.footprint then Summary.Stats.add_visited_fp stats node_id - else Summary.Stats.add_visited_re stats node_id + if not !BiabductionConfig.footprint then + let node_id = (Procdesc.Node.get_id node :> int) in + let stats = summary.Summary.stats in + Summary.Stats.add_visited stats node_id let forward_tabulate summary exe_env tenv proc_cfg wl =