[NodePrinter] Force usage of with_session

Summary:
- Makes sure that `start_session` and `finish_session` are well parenthesized
- Avoids a try finally when debug is disabled

Reviewed By: ngorogiannis

Differential Revision: D15371841

fbshipit-source-id: 340203edb
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 4a44bd4430
commit 0a5810c579

@ -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 =

@ -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 ()

@ -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.
*)

@ -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 )

@ -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

@ -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

Loading…
Cancel
Save