diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 046316415..a65042046 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -337,14 +337,13 @@ module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct F.pp_print_string fmt " WEAK TOPOLOGICAL ORDER" in let underlying_node = Node.underlying_node node in - NodePrinter.start_session ~pp_name underlying_node ; - 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 = - wto |> IContainer.to_rev_list ~fold:WeakTopologicalOrder.Partition.fold_heads |> List.rev - in - L.d_printfln "Loop heads: %a" (Pp.seq pp_node) loop_heads ; - NodePrinter.finish_session underlying_node + NodePrinter.with_session ~pp_name underlying_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 = + wto |> IContainer.to_rev_list ~fold:WeakTopologicalOrder.Partition.fold_heads |> List.rev + in + L.d_printfln "Loop heads: %a" (Pp.seq pp_node) loop_heads ) let exec_wto_node ~pp_instr cfg proc_data inv_map node ~is_loop_head ~is_narrowing = diff --git a/infer/src/absint/NodePrinter.ml b/infer/src/absint/NodePrinter.ml index 01adc5cd5..8f59ade82 100644 --- a/infer/src/absint/NodePrinter.ml +++ b/infer/src/absint/NodePrinter.ml @@ -22,14 +22,9 @@ let new_session node = !(summary.Summary.sessions) -let start_session ~pp_name node = - if Config.write_html then - let session = new_session node in - Printer.node_start_session ~pp_name node session - - -let finish_session node = if Config.write_html then Printer.node_finish_session node - let with_session ~pp_name node ~f = - start_session ~pp_name node ; - Utils.try_finally_swallow_timeout ~f ~finally:(fun () -> finish_session node) + if Config.write_html then ( + let session = new_session node 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 cf03d4d4d..f9bde0b24 100644 --- a/infer/src/absint/NodePrinter.mli +++ b/infer/src/absint/NodePrinter.mli @@ -9,12 +9,8 @@ open! IStd (** Simplified html node printer for checkers *) -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 -(** To be called after analyzing a node *) - val with_session : pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a -(** Wraps [f] between [start_session] and [finish_session]. Will swallow timeouts so do *not* use - from within biabduction *) +(** + Wraps [f] in an html debug session. + Will swallow timeouts so do *not* use from within biabduction. +*) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 732c721f1..1ea5b9a1c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -428,27 +428,23 @@ let checker : Callbacks.proc_callback_args -> Summary.t = in let underlying_exit_node = Procdesc.get_exit_node proc_desc in let pp_name f = F.pp_print_string f "bufferoverrun check" in - NodePrinter.start_session ~pp_name underlying_exit_node ; - let summary = - let cfg = CFG.from_pdesc proc_desc in - let checks = - let get_proc_summary callee_pname = - Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname - |> Option.bind ~f:(fun summary -> - let analysis_payload = BufferOverrunAnalysis.Payload.of_summary summary in - let checker_payload = Payload.of_summary summary in - Option.map2 analysis_payload checker_payload - ~f:(fun analysis_payload checker_payload -> - ( analysis_payload - , Summary.get_proc_desc summary |> Procdesc.get_pvar_formals - , checker_payload ) ) ) + NodePrinter.with_session ~pp_name underlying_exit_node ~f:(fun () -> + let cfg = CFG.from_pdesc proc_desc in + let checks = + let get_proc_summary callee_pname = + Ondemand.analyze_proc_name ~caller_pdesc:proc_desc callee_pname + |> Option.bind ~f:(fun summary -> + let analysis_payload = BufferOverrunAnalysis.Payload.of_summary summary in + let checker_payload = Payload.of_summary summary in + Option.map2 analysis_payload checker_payload + ~f:(fun analysis_payload checker_payload -> + ( analysis_payload + , Summary.get_proc_desc summary |> Procdesc.get_pvar_formals + , checker_payload ) ) ) + in + compute_checks get_proc_summary proc_desc tenv integer_type_widths cfg inv_map in - compute_checks get_proc_summary proc_desc tenv integer_type_widths cfg inv_map - in - report_errors tenv checks summary ; - let locals = BufferOverrunAnalysis.get_local_decls proc_desc in - let cond_set = get_checks_summary locals checks in - Payload.update_summary cond_set summary - in - NodePrinter.finish_session underlying_exit_node ; - summary + report_errors tenv checks summary ; + let locals = BufferOverrunAnalysis.get_local_decls proc_desc in + let cond_set = get_checks_summary locals checks in + Payload.update_summary cond_set summary ) diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 15b2c559c..cec2d488d 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -794,13 +794,12 @@ let compute_get_node_nb_exec node_cfg bound_map : get_node_nb_exec = {ConstraintSolver.f} in let start_node = NodeCFG.start_node node_cfg in - ( if Config.write_html then - let pp_name fmt = F.pp_print_string fmt "cost(constraints)" in - NodePrinter.start_session ~pp_name start_node ) ; - let equalities = ConstraintSolver.collect_constraints ~debug node_cfg in - let () = ConstraintSolver.compute_costs ~debug bound_map equalities in - if Config.write_html then NodePrinter.finish_session start_node ; - ConstraintSolver.get_node_nb_exec equalities + NodePrinter.with_session start_node + ~pp_name:(fun fmt -> F.pp_print_string fmt "cost(constraints)") + ~f:(fun () -> + let equalities = ConstraintSolver.collect_constraints ~debug node_cfg in + let () = ConstraintSolver.compute_costs ~debug bound_map equalities in + ConstraintSolver.get_node_nb_exec equalities ) let compute_worst_case_cost tenv integer_type_widths get_callee_summary_and_formals instr_cfg_wto diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index ea739536b..567f10c3c 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -84,20 +84,19 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct let pp_name fmt = F.pp_print_string fmt "eradicate" let do_node tenv node typestate = - NodePrinter.start_session ~pp_name node ; - State.set_node node ; - let typestates_succ, typestates_exn = - TypeCheck.typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc - find_canonical_duplicate annotated_signature typestate node linereader - in - if Config.write_html then ( - let d_typestate ts = L.d_printfln "%a" TypeState.pp ts in - L.d_strln "before:" ; - d_typestate typestate ; - L.d_strln "after:" ; - List.iter ~f:d_typestate typestates_succ ) ; - NodePrinter.finish_session node ; - (typestates_succ, typestates_exn) + NodePrinter.with_session ~pp_name node ~f:(fun () -> + State.set_node node ; + let typestates_succ, typestates_exn = + TypeCheck.typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc + find_canonical_duplicate annotated_signature typestate node linereader + in + if Config.write_html then ( + let d_typestate ts = L.d_printfln "%a" TypeState.pp ts in + L.d_strln "before:" ; + d_typestate typestate ; + L.d_strln "after:" ; + List.iter ~f:d_typestate typestates_succ ) ; + (typestates_succ, typestates_exn) ) let proc_throws _ = DontKnow