[debug] Session kinds

Summary:
I was wondering what were the empty sessions and why inferbo was running twice.
Answer: the empty sessions were 'compute pre' and the second run of inferbo was the narrowing phase.

Reviewed By: ngorogiannis

Differential Revision: D15378138

fbshipit-source-id: 507a3df42

infer/src/absint/AbstractInterpreter.ml

@@ -237,8 +237,10 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
 
   (* shadowed for HTML debug *)
   let exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing astate_pre inv_map =
-    NodePrinter.with_session ~pp_name:(TransferFunctions.pp_session_name node)
-      (Node.underlying_node node) ~f:(fun () ->
+    NodePrinter.with_session (Node.underlying_node node)
+      ~kind:(if is_narrowing then `ExecNodeNarrowing else `ExecNode)
+      ~pp_name:(TransferFunctions.pp_session_name node)
+      ~f:(fun () ->
         exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing astate_pre inv_map )
 
 
@@ -260,7 +262,7 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
 
   (* shadowed for HTML debug *)
   let compute_pre cfg node inv_map =
-    NodePrinter.with_session (Node.underlying_node node)
+    NodePrinter.with_session (Node.underlying_node node) ~kind:`ComputePre
       ~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () -> compute_pre cfg node inv_map
     )
 
@@ -332,12 +334,9 @@ module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct
   include AbstractInterpreterCommon (TransferFunctions)
 
   let debug_wto wto node =
-    let pp_name fmt =
-      TransferFunctions.pp_session_name node fmt ;
-      F.pp_print_string fmt " WEAK TOPOLOGICAL ORDER"
-    in
     let underlying_node = Node.underlying_node node in
-    NodePrinter.with_session ~pp_name underlying_node ~f:(fun () ->
+    NodePrinter.with_session underlying_node ~kind:`WTO
+      ~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () ->
         let pp_node fmt node = node |> Node.id |> Node.pp_id fmt in
         L.d_printfln "%a" (WeakTopologicalOrder.Partition.pp ~pp_node) wto ;
         let loop_heads =

infer/src/absint/NodePrinter.ml

@@ -22,9 +22,23 @@ let new_session node =
       !(summary.Summary.sessions)
 
 
-let with_session ~pp_name node ~f =
+let kind_to_string = function
+  | `ComputePre ->
+      "compute pre"
+  | `ExecNode ->
+      "exec"
+  | `ExecNodeNarrowing ->
+      "exec NARROWING"
+  | `WTO ->
+      "WEAK TOPOLOGICAL ORDER"
+
+
+let with_kind pp_name kind f = Format.fprintf f "[%s] %t" (kind_to_string kind) pp_name
+
+let with_session ?kind ~pp_name node ~f =
   if Config.write_html then (
     let session = new_session node in
+    let pp_name = Option.fold kind ~init:pp_name ~f:with_kind in
     Printer.node_start_session ~pp_name node session ;
     Utils.try_finally_swallow_timeout ~f ~finally:(fun () -> Printer.node_finish_session node) )
   else f ()

infer/src/absint/NodePrinter.mli

@@ -9,7 +9,12 @@ open! IStd
 
 (** Simplified html node printer for checkers *)
 
-val with_session : pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
+val with_session :
+     ?kind:[< `ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
+  -> pp_name:(Format.formatter -> unit)
+  -> Procdesc.Node.t
+  -> f:(unit -> 'a)
+  -> 'a
 (**
   Wraps [f] in an html debug session.
   Will swallow timeouts so do *not* use from within biabduction.