diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 635c7d38f..84e8c67be 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -76,7 +76,10 @@ struct in (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) let instr_ids = match CFG.instr_ids node with [] -> [(Sil.skip_instr, None)] | l -> l in - if debug then NodePrinter.start_session (CFG.underlying_node node) ; + if debug then + NodePrinter.start_session + ~pp_name:(TransferFunctions.pp_session_name node) + (CFG.underlying_node node) ; let astate_post, inv_map_post = List.fold ~f:compute_post ~init:(pre, inv_map) instr_ids in if debug then ( let instrs = List.map ~f:fst instr_ids in diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 1aadc5863..0e8e2de99 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -29,10 +29,12 @@ struct type extras = TransferFunctions.extras + let pp_session_name = TransferFunctions.pp_session_name + let pp_pre_post pre post hil_instr node = if Config.write_html then ( let underyling_node = CFG.underlying_node node in - NodePrinter.start_session underyling_node ; + NodePrinter.start_session ~pp_name:(pp_session_name node) underyling_node ; L.d_strln (Format.asprintf "PRE: %a@.INSTR: %a@.POST: %a@." TransferFunctions.Domain.pp pre HilInstr.pp hil_instr TransferFunctions.Domain.pp post) ; diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index 1bc9ddd18..64ff88e1d 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -31,6 +31,8 @@ module Make type extras = TransferFunctions.extras val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate + + val pp_session_name : CFG.node -> Format.formatter -> unit end (** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *) diff --git a/infer/src/absint/NodePrinter.ml b/infer/src/absint/NodePrinter.ml index dc66ebad7..ef16ccacb 100644 --- a/infer/src/absint/NodePrinter.ml +++ b/infer/src/absint/NodePrinter.ml @@ -26,10 +26,10 @@ let new_session node = !(summary.Specs.sessions) -let start_session node = +let start_session ~pp_name node = if Config.write_html then let session = new_session node in - Printer.node_start_session node session + Printer.node_start_session ~pp_name node session let finish_session node = if Config.write_html then Printer.node_finish_session node diff --git a/infer/src/absint/NodePrinter.mli b/infer/src/absint/NodePrinter.mli index 764e16467..b8833a244 100644 --- a/infer/src/absint/NodePrinter.mli +++ b/infer/src/absint/NodePrinter.mli @@ -11,7 +11,7 @@ open! IStd (** Simplified html node printer for checkers *) -val start_session : Procdesc.Node.t -> unit +val start_session : pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> unit (** To be called before analyzing a node *) val finish_session : Procdesc.Node.t -> unit diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 8edeedb47..c4c5c8651 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -19,6 +19,8 @@ module type S = sig type instr val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> instr -> Domain.astate + + val pp_session_name : CFG.node -> Format.formatter -> unit end module type SIL = sig diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 0af8487e4..9316c39ed 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -26,6 +26,9 @@ module type S = sig val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> instr -> Domain.astate (** {A} instr {A'}. [node] is the node of the current instruction *) + + val pp_session_name : CFG.node -> Format.formatter -> unit + (** print session name for HTML debug *) end module type SIL = sig diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 820ca0d18..523b1f077 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -107,6 +107,9 @@ module NullifyTransferFunctions = struct "Should not add nullify instructions before running nullify analysis!" in if is_last_instr_in_node instr node then postprocess astate' node extras else astate' + + + let pp_session_name _node fmt = Format.pp_print_string fmt "nullify" end module NullifyAnalysis = diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 3f3bcb47e..76dddad76 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -328,7 +328,7 @@ let force_delayed_prints () = (** Start a session, and create a new html fine for the node if it does not exist yet *) -let start_session node (loc: Location.t) proc_name session source = +let start_session ~pp_name node (loc: Location.t) proc_name session source = let node_id = Procdesc.Node.get_id node in if NodesHtml.start_node (node_id :> int) @@ -339,18 +339,18 @@ let start_session node (loc: Location.t) proc_name session source = Pp.Green (Procdesc.Node.pp_instrs (Pp.html Green) None ~sub_instrs:true) node Io_infer.Html.pp_end_color () ; - F.fprintf !curr_html_formatter "%a%a" Io_infer.Html.pp_hline () + F.fprintf !curr_html_formatter "%a%a %t" Io_infer.Html.pp_hline () (Io_infer.Html.pp_session_link source ~with_name:true [".."] ~proc_name) - ((node_id :> int), session, loc.Location.line) ; + ((node_id :> int), session, loc.Location.line) pp_name ; F.fprintf !curr_html_formatter "%a" Io_infer.Html.pp_start_color Pp.Black -let node_start_session node session = +let node_start_session ~pp_name node session = if Config.write_html then let loc = Procdesc.Node.get_loc node in let source = loc.Location.file in let pname = Procdesc.Node.get_proc_name node in - start_session node loc pname session source + start_session ~pp_name node loc pname session source (** Finish a session, and perform delayed print actions if required *) diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index 7d3bb8dfe..eddda096d 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -36,7 +36,7 @@ val force_delayed_prints : unit -> unit val node_finish_session : Procdesc.Node.t -> unit (** Finish a session, and perform delayed print actions if required *) -val node_start_session : Procdesc.Node.t -> int -> unit +val node_start_session : pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> int -> unit (** Start a session, and create a new html fine for the node if it does not exist yet *) val write_proc_html : Procdesc.t -> unit diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 88ed67d21..774c2104c 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -353,11 +353,13 @@ let reset_prop_metrics () = exception RE_EXE_ERROR +let pp_name fmt = F.pp_print_string fmt "interproc" + let do_before_node session node = State.set_node node ; State.set_session session ; L.reset_delayed_prints () ; - Printer.node_start_session node (session :> int) + Printer.node_start_session ~pp_name node (session :> int) let do_after_node node = Printer.node_finish_session node diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 226043872..3b46cd996 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -305,6 +305,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in print_debug_info instr mem output_mem ; output_mem + + + let pp_session_name node fmt = F.fprintf fmt "bufferoverrun %a" CFG.pp_id (CFG.id node) end module CFG = ProcCfg.NormalOneInstrPerNode diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml index 74d8df659..e4c70e43f 100644 --- a/infer/src/checkers/BoundedCallTree.ml +++ b/infer/src/checkers/BoundedCallTree.ml @@ -141,6 +141,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate | Sil.Load _ | Store _ | Prune _ | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "crashcontext" end module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/Litho.ml b/infer/src/checkers/Litho.ml index 28f269e37..beb076d93 100644 --- a/infer/src/checkers/Litho.ml +++ b/infer/src/checkers/Litho.ml @@ -279,6 +279,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct with Not_found -> astate ) | _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "litho" end module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/NullabilityCheck.ml b/infer/src/checkers/NullabilityCheck.ml index b52bcbd43..89445e7c4 100644 --- a/infer/src/checkers/NullabilityCheck.ml +++ b/infer/src/checkers/NullabilityCheck.ml @@ -335,6 +335,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else astate | _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "nullability check" end module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml index 63232eccf..f0ce2d7e6 100644 --- a/infer/src/checkers/NullabilityPreanalysis.ml +++ b/infer/src/checkers/NullabilityPreanalysis.ml @@ -58,6 +58,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate ) | _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "nullability preanalysis" end (* Tracks when block variables of ObjC classes have been assigned to in constructors *) diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 29d67f170..dbaa4505a 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -109,6 +109,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> astate else astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "nullability suggest" end module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml index 61474db62..00e0b20b0 100644 --- a/infer/src/checkers/Ownership.ml +++ b/infer/src/checkers/Ownership.ml @@ -340,6 +340,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match ret_opt with Some base -> Domain.remove base astate' | None -> astate' ) | Assume (assume_exp, _, _, loc) -> Domain.exp_add_reads assume_exp loc summary astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "ownership" end module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml index d7002179f..ccf8f0355 100644 --- a/infer/src/checkers/SimpleChecker.ml +++ b/infer/src/checkers/SimpleChecker.ml @@ -75,6 +75,9 @@ module Make (Spec : Spec) : S = struct (fun astate acc -> Domain.add (Spec.exec_instr astate instr node_kind pname proc_data.ProcData.tenv) acc ) astate_set Domain.empty + + + let pp_session_name _node fmt = F.pp_print_string fmt "simple checker" end module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 618a071e0..7046de8ee 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -174,6 +174,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct at_least_nonbottom | Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "siof" end module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 46012f236..a708ca48a 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -50,6 +50,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct List.fold ~f:add_actual_by_ref ~init:astate actuals | Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Declare_locals _ -> astate + + + let pp_session_name _node fmt = Format.pp_print_string fmt "address taken" end module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index a058470d7..0231b575e 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -440,6 +440,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct L.(die InternalError) "Expecting a return identifier" | _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "annotation reachability" end module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index b9c162b6d..732437941 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -92,6 +92,9 @@ module TransferFunctionsNodesBasicCost (CFG : ProcCfg.S) = struct let inferbo_mem = InferboTransferFunctions.exec_instr inferbo_mem pdata node instr in let costmap = exec_instr_cost inferbo_mem costmap pdata node instr in (inferbo_mem, costmap) + + + let pp_session_name _node fmt = F.pp_print_string fmt "cost(basic)" end module AnalyzerNodesBasicCost = AbstractInterpreter.Make (CFG) (TransferFunctionsNodesBasicCost) @@ -528,6 +531,9 @@ module TransferFunctionsWCET (CFG : ProcCfg.S) = struct else (cost_node, reported_so_far) in astate' + + + let pp_session_name _node fmt = F.pp_print_string fmt "cost(wcet)" end module AnalyzerWCET = AbstractInterpreter.Make (CFG) (TransferFunctionsWCET) diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index e3268b5af..5a9a3fee1 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -76,6 +76,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct |> exp_add_live call_exp |> add_live_actuals actuals call_exp | Sil.Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ -> astate + + + let pp_session_name node fmt = F.fprintf fmt "liveness %a" CFG.pp_id (CFG.id node) end module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional)) @@ -116,6 +119,9 @@ module CapturedByRefTransferFunctions (CFG : ProcCfg.S) = struct acc ) acc ) ~init:astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "captured by ref" end module CapturedByRefAnalyzer = diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index f735e4765..33bbb1df7 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -290,6 +290,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with uninit_vars} | Call _ | Assume _ -> astate + + + let pp_session_name node fmt = F.fprintf fmt "uninit %a" CFG.pp_id (CFG.id node) end module CFG = ProcCfg.NormalOneInstrPerNode diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index d9736cfdb..b3589f389 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -697,6 +697,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr | _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "racerd" end module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index f8ddbfe28..645ffc3ed 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -82,6 +82,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Domain.integrate_summary ~caller_state:astate ~callee_summary callee_pname loc ) ) | _ -> astate + + + let pp_session_name _node fmt = F.pp_print_string fmt "starvation" end module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index a09cc84e2..8d112d89a 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -103,8 +103,10 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct let join = TypeState.join Extension.ext + let pp_name fmt = F.pp_print_string fmt "eradicate" + let do_node tenv node typestate = - NodePrinter.start_session node ; + NodePrinter.start_session ~pp_name node ; State.set_node node ; let typestates_succ, typestates_exn = TypeCheck.typecheck_node tenv Extension.ext calls_this checks idenv get_proc_desc diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 03f616347..087652dea 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -88,6 +88,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr + + + let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" end (* Create an intraprocedural abstract interpreter from the transfer functions we defined *) diff --git a/infer/src/quandary/ClangTaintAnalysis.ml b/infer/src/quandary/ClangTaintAnalysis.ml index cbc7877e2..73d5497a0 100644 --- a/infer/src/quandary/ClangTaintAnalysis.ml +++ b/infer/src/quandary/ClangTaintAnalysis.ml @@ -102,4 +102,6 @@ include TaintAnalysis.Make (struct let is_taintable_type _ = true + + let name = "clang" end) diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml index c2bbb2fe8..52321a1c1 100644 --- a/infer/src/quandary/JavaTaintAnalysis.ml +++ b/infer/src/quandary/JavaTaintAnalysis.ml @@ -90,4 +90,7 @@ include TaintAnalysis.Make (struct false ) | _ -> false + + + let name = "java" end) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index d498415cb..7f40d13ad 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -724,6 +724,11 @@ module Make (TaintSpecification : TaintSpec.S) = struct analyze_call Domain.empty called_pname | _ -> astate + + + let pp_session_name = + let name = F.sprintf "quandary(%s)" TaintSpecification.name in + fun (_node: CFG.node) fmt -> F.pp_print_string fmt name end module HilConfig : LowerHil.HilConfig = struct diff --git a/infer/src/quandary/TaintSpec.ml b/infer/src/quandary/TaintSpec.ml index 3e54d5035..d3add8f22 100644 --- a/infer/src/quandary/TaintSpec.ml +++ b/infer/src/quandary/TaintSpec.ml @@ -40,4 +40,6 @@ module type S = sig val to_summary_access_tree : AccessTree.t -> QuandarySummary.AccessTree.t val of_summary_access_tree : QuandarySummary.AccessTree.t -> AccessTree.t + + val name : string end diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 1ce818413..451961406 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -56,6 +56,8 @@ module MockTaintAnalysis = TaintAnalysis.Make (struct let is_taintable_type _ = true let get_model _ _ _ _ _ = None + + let name = "" end) module TestInterpreter = diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index cf1ba533d..244a7755c 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -55,6 +55,8 @@ module PathCountTransferFunctions (CFG : ProcCfg.S) = struct (* just propagate the current path count *) let exec_instr astate _ _ _ = astate + + let pp_session_name _node _fmt = () end module NormalTestInterpreter = AnalyzerTester.Make (ProcCfg.Normal) (PathCountTransferFunctions)