diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index a65042046..950b897a5 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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 = diff --git a/infer/src/absint/NodePrinter.ml b/infer/src/absint/NodePrinter.ml index 8f59ade82..9852f832c 100644 --- a/infer/src/absint/NodePrinter.ml +++ b/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 () diff --git a/infer/src/absint/NodePrinter.mli b/infer/src/absint/NodePrinter.mli index f9bde0b24..cf25c1c7f 100644 --- a/infer/src/absint/NodePrinter.mli +++ b/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.