Stats: merge visited_fp and visited_re

Reviewed By: da319

Differential Revision: D10376556

fbshipit-source-id: a0db1485a

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)
 

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=

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: IntSet.t  (** Nodes visited *) }
-    ; mutable nodes_visited_re: IntSet.t  (** Nodes visited during the re-execution phase *) }
 
-  let empty =
+  let empty = {failure_kind= None; symops= 0; nodes_visited= IntSet.empty}
-    {failure_kind= None; symops= 0; nodes_visited_fp= IntSet.empty; nodes_visited_re= 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 nb_visited {nodes_visited} = IntSet.cardinal nodes_visited
-
-  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

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 nb_visited : t -> int
-
-  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
 

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*)
+(** Return true if the node was visited during analysis *)
-let node_is_visited node =
+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
+      Summary.Stats.is_visited stats node_id
-      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
 
 
 let pp_node_link path_to_root ?proof_cover ~description fmt node =

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
+  if not !BiabductionConfig.footprint then
-  let stats = summary.Summary.stats in
+    let node_id = (Procdesc.Node.get_id node :> int) in
-  if !BiabductionConfig.footprint then Summary.Stats.add_visited_fp stats node_id
+    let stats = summary.Summary.stats in
-  else Summary.Stats.add_visited_re stats node_id
+    Summary.Stats.add_visited stats node_id
 
 
 let forward_tabulate summary exe_env tenv proc_cfg wl =