From 1eaaf84a9035e6572b5fdd35f2594812eca31f29 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Tue, 17 Jan 2017 10:33:02 -0800 Subject: [PATCH] [checkers] Add support for html output in checkers, starting with Eradicate Summary: Make the html output available to checkers when -g is used on the command-line. A checker needs to call a function to start and finish the processing of each node, and add prints during the processing. This diff illustrates the case for Eradicate, by adding printing of the pre-state and post-states. Reviewed By: sblackshear Differential Revision: D4421379 fbshipit-source-id: 67501ba --- infer/src/IR/Procdesc.re | 15 ++++++----- infer/src/IR/Procdesc.rei | 2 +- infer/src/backend/InferAnalyze.re | 3 ++- infer/src/backend/interproc.ml | 17 ++++++------ infer/src/backend/paths.ml | 2 +- infer/src/backend/preanal.ml | 2 +- infer/src/backend/printer.ml | 30 +++++++++++---------- infer/src/backend/printer.mli | 7 ++--- infer/src/backend/state.ml | 2 +- infer/src/base/Config.ml | 5 ---- infer/src/base/Config.mli | 1 - infer/src/checkers/NodePrinter.ml | 43 ++++++++++++++++++++++++++++++ infer/src/checkers/NodePrinter.mli | 18 +++++++++++++ infer/src/eradicate/eradicate.ml | 20 +++++++++----- infer/src/eradicate/typeState.ml | 2 +- 15 files changed, 116 insertions(+), 53 deletions(-) create mode 100644 infer/src/checkers/NodePrinter.ml create mode 100644 infer/src/checkers/NodePrinter.mli diff --git a/infer/src/IR/Procdesc.re b/infer/src/IR/Procdesc.re index e54ad2853..66ecf2b5f 100644 --- a/infer/src/IR/Procdesc.re +++ b/infer/src/IR/Procdesc.re @@ -47,20 +47,20 @@ let module Node = { /** predecessor nodes in the cfg */ mutable preds: list t, /** name of the procedure the node belongs to */ - pname: option Procname.t, + pname_opt: option Procname.t, /** successor nodes in the cfg */ mutable succs: list t }; let exn_handler_kind = Stmt_node "exception handler"; let exn_sink_kind = Stmt_node "exceptions sink"; let throw_kind = Stmt_node "throw"; - let dummy () => { + let dummy pname_opt => { id: 0, dist_exit: None, instrs: [], kind: Skip_node "dummy", loc: Location.dummy, - pname: None, + pname_opt, succs: [], preds: [], exn: [] @@ -120,7 +120,7 @@ let module Node = { /** Get the name of the procedure the node belongs to */ let get_proc_name node => - switch node.pname { + switch node.pname_opt { | None => L.out "get_proc_name: at node %d@\n" node.id; assert false @@ -308,7 +308,10 @@ let from_proc_attributes called_from_cfg::called_from_cfg attributes => { if (not called_from_cfg) { assert false }; - {attributes, nodes: [], nodes_num: 0, start_node: Node.dummy (), exit_node: Node.dummy ()} + let pname_opt = Some attributes.ProcAttributes.proc_name; + let start_node = Node.dummy pname_opt; + let exit_node = Node.dummy pname_opt; + {attributes, nodes: [], nodes_num: 0, start_node, exit_node} }; @@ -498,7 +501,7 @@ let create_node pdesc loc kind instrs => { kind, loc, preds: [], - pname: Some pdesc.attributes.proc_name, + pname_opt: Some pdesc.attributes.proc_name, succs: [], exn: [] }; diff --git a/infer/src/IR/Procdesc.rei b/infer/src/IR/Procdesc.rei index 4d7b87c87..11c435d59 100644 --- a/infer/src/IR/Procdesc.rei +++ b/infer/src/IR/Procdesc.rei @@ -51,7 +51,7 @@ let module Node: { let d_instrs: sub_instrs::bool => option Sil.instr => t => unit; /** Create a dummy node */ - let dummy: unit => t; + let dummy: option Procname.t => t; /** Check if two nodes are equal */ let equal: t => t => bool; diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index b6b9b3fc6..0d4dc9485 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/infer/src/backend/InferAnalyze.re @@ -23,7 +23,8 @@ let analyze_exe_env exe_env => { if Config.checkers { /* run the checkers only */ let call_graph = Exe_env.get_cg exe_env; - Callbacks.iterate_callbacks Checkers.ST.store_summary call_graph exe_env + Callbacks.iterate_callbacks Checkers.ST.store_summary call_graph exe_env; + Printer.write_all_html_files exe_env } else { /* run the full analysis */ Interproc.do_analysis exe_env; diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 56424d60e..0a1c25d94 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -333,12 +333,11 @@ let reset_prop_metrics () = exception RE_EXE_ERROR -let do_before_node pname source session node = - let loc = Procdesc.Node.get_loc node in +let do_before_node source session node = State.set_node node; State.set_session session; L.reset_delayed_prints (); - Printer.node_start_session node loc pname (session :> int) source + Printer.node_start_session node (session :> int) source let do_after_node source node = Printer.node_finish_session node source @@ -605,7 +604,7 @@ let forward_tabulate tenv pdesc wl source = let session = incr summary.Specs.sessions; !(summary.Specs.sessions) in - do_before_node pname source session curr_node; + do_before_node source session curr_node; do_node_and_handle curr_node session done; L.d_strln ".... Work list empty. Stop ...."; L.d_ln () @@ -908,7 +907,7 @@ let initial_prop_from_pre tenv curr_f pre = let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t) source : Prop.normal Specs.spec option = let pname = Procdesc.get_proc_name pdesc in - do_before_node pname source 0 init_node; + do_before_node source 0 init_node; L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string pname ^ " ####"); L.d_indent 1; L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition; @@ -925,7 +924,7 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec Worklist.add wl init_node; ignore (path_set_put_todo wl init_node init_edgeset); forward_tabulate tenv pdesc wl source; - do_before_node pname source 0 init_node; + do_before_node source 0 init_node; L.d_strln_color Green ("#### Finished: RE-execution for " ^ Procname.to_string pname ^ " ####"); L.d_increase_indent 1; @@ -948,7 +947,7 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec do_after_node source init_node; Some spec with RE_EXE_ERROR -> - do_before_node pname source 0 init_node; + do_before_node source 0 init_node; Printer.force_delayed_prints (); L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string pname ^ "] ...ERROR"); L.d_increase_indent 1; @@ -1379,7 +1378,7 @@ let perform_transition exe_env tenv proc_name source = f start_node | None -> () with exn when SymOp.exn_not_failure exn -> () in - apply_start_node (do_before_node proc_name source 0); + apply_start_node (do_before_node source 0); try Config.allow_leak := true; let res = collect_preconditions tenv proc_name in @@ -1521,7 +1520,7 @@ let visited_and_total_nodes ~filter cfg = if filter_node pdesc n then begin set := Procdesc.NodeSet.add n !set; - if snd (Printer.node_is_visited (Procdesc.get_proc_name pdesc) n) + if snd (Printer.node_is_visited n) then set_visited_re := Procdesc.NodeSet.add n !set_visited_re end in Cfg.iter_all_nodes add cfg; diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index fc6d0d4c5..58b4dfeb7 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -343,7 +343,7 @@ end = struct | None -> () in iter_shortest_sequence (fun _ p _ _ -> add_node (curr_node p)) None path; - let max_rep_node = ref (Procdesc.Node.dummy ()) in + let max_rep_node = ref (Procdesc.Node.dummy None) in let max_rep_num = ref 0 in Procdesc.NodeMap.iter (fun node num -> if num > !max_rep_num then (max_rep_node := node; max_rep_num := num)) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 9f56d1356..9acb3754a 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -124,7 +124,7 @@ module NullifyTransferFunctions = struct (reaching_defs', to_nullify) | None -> astate - let cache_node = ref (Procdesc.Node.dummy ()) + let cache_node = ref (Procdesc.Node.dummy None) let cache_instr = ref Sil.skip_instr let last_instr_in_node node = diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 679f795da..ec29c996f 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -74,8 +74,8 @@ end let curr_html_formatter = ref F.std_formatter (** Return true if the node was visited during footprint and during re-execution*) -let node_is_visited proc_name node = - match Specs.get_summary proc_name with +let node_is_visited node = + match Specs.get_summary (Procdesc.Node.get_proc_name node) with | None -> false, false | Some summary -> @@ -87,8 +87,8 @@ let node_is_visited proc_name node = is_visited_fp, is_visited_re (** Return true if the node was visited during analysis *) -let is_visited proc_name node = - let visited_fp, visited_re = node_is_visited proc_name node in +let is_visited node = + let visited_fp, visited_re = node_is_visited node in visited_fp || visited_re (* =============== START of module NodesHtml =============== *) @@ -134,7 +134,7 @@ end = struct ~preds:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_preds node) :> int list) ~succs:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_succs node) :> int list) ~exn:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_exn node) :> int list) - ~isvisited:(is_visited proc_name node) + ~isvisited:(is_visited node) ~isproof:false fmt (Procdesc.Node.get_id node :> int)) preds; F.fprintf fmt "
SUCCS: @\n"; @@ -146,7 +146,7 @@ end = struct ~preds:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_preds node) :> int list) ~succs:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_succs node) :> int list) ~exn:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_exn node) :> int list) - ~isvisited:(is_visited proc_name node) + ~isvisited:(is_visited node) ~isproof:false fmt (Procdesc.Node.get_id node :> int)) succs; F.fprintf fmt "
EXN: @\n"; @@ -158,7 +158,7 @@ end = struct ~preds:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_preds node) :> int list) ~succs:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_succs node) :> int list) ~exn:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_exn node) :> int list) - ~isvisited:(is_visited proc_name node) + ~isvisited:(is_visited node) ~isproof:false fmt (Procdesc.Node.get_id node :> int)) exns; F.fprintf fmt "
@\n"; @@ -393,9 +393,11 @@ let start_session node (loc: Location.t) proc_name session source = F.fprintf !curr_html_formatter "%a" Io_infer.Html.pp_start_color Pp.Black -let node_start_session node loc proc_name session source = +let node_start_session node session source = if Config.write_html then - start_session node loc proc_name session source + let loc = Procdesc.Node.get_loc node in + let pname = Procdesc.Node.get_proc_name node in + start_session node loc pname session source (** Finish a session, and perform delayed print actions if required *) let node_finish_session node source = @@ -436,7 +438,7 @@ let write_proc_html source whole_seconds pdesc = ~preds:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_preds n) :> int list) ~succs:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_succs n) :> int list) ~exn:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_exn n) :> int list) - ~isvisited:(is_visited pname n) + ~isvisited:(is_visited n) ~isproof:false fmt (Procdesc.Node.get_id n :> int)) nodes; @@ -475,7 +477,7 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro let curr_nodes = try Hashtbl.find table_nodes_at_linenum lnum with Not_found -> [] in - Hashtbl.replace table_nodes_at_linenum lnum ((n, proc_desc) :: curr_nodes) in + Hashtbl.replace table_nodes_at_linenum lnum (n :: curr_nodes) in let proc_loc = Procdesc.get_loc proc_desc in let process_proc = Procdesc.is_defined proc_desc && @@ -534,7 +536,7 @@ let write_html_file linereader filename procs = line_html in F.fprintf fmt "%s" str; IList.iter - (fun (n, pdesc) -> + (fun n -> let isproof = Specs.Visitedset.mem (Procdesc.Node.get_id n, []) !proof_cover in Io_infer.Html.pp_node_link @@ -544,12 +546,12 @@ let write_html_file linereader filename procs = ~preds:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_preds n) :> int list) ~succs:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_succs n) :> int list) ~exn:(IList.map Procdesc.Node.get_id (Procdesc.Node.get_exn n) :> int list) - ~isvisited:(is_visited (Procdesc.get_proc_name pdesc) n) + ~isvisited:(is_visited n) ~isproof fmt (Procdesc.Node.get_id n :> int)) nodes_at_linenum; IList.iter - (fun (n, _) -> + (fun n -> match Procdesc.Node.get_kind n with | Procdesc.Node.Start_node proc_name -> let num_specs = IList.length (Specs.get_specs proc_name) in diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index 3dc46a1c0..7497bc5b8 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -40,17 +40,14 @@ val force_delayed_prints : unit -> unit val node_finish_session : Procdesc.Node.t -> SourceFile.t -> unit (** Return true if the node was visited during footprint and during re-execution *) -val node_is_visited : Procname.t -> Procdesc.Node.t -> bool * bool +val node_is_visited : Procdesc.Node.t -> bool * bool (** Start a session, and create a new html fine for the node if it does not exist yet *) -val node_start_session : - Procdesc.Node.t -> Location.t -> Procname.t -> int -> SourceFile.t -> unit +val node_start_session : Procdesc.Node.t -> int -> SourceFile.t -> unit (** Write html file for the procedure. The boolean indicates whether to print whole seconds only. *) val write_proc_html : SourceFile.t -> bool -> Procdesc.t -> unit -val write_html_file : LineReader.t -> SourceFile.t -> Procdesc.t list -> unit - (** Create filename.ext.html for each file in the exe_env. *) val write_all_html_files : Exe_env.t -> unit diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index fd78f5d3a..dbbbc4778 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -64,7 +64,7 @@ let initial () = { diverging_states_node = Paths.PathSet.empty; diverging_states_proc = Paths.PathSet.empty; last_instr = None; - last_node = Procdesc.Node.dummy (); + last_node = Procdesc.Node.dummy None; last_path = None; last_prop_tenv_pdesc = None; last_session = 0; diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 077b931c2..06db4ab51 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -763,10 +763,6 @@ and eradicate_debug = CLOpt.mk_bool ~long:"eradicate-debug" "Print debug info when errors are found" -and eradicate_trace = - CLOpt.mk_bool ~long:"eradicate-trace" - "Print step-by-step tracing information" - and eradicate_verbose = CLOpt.mk_bool ~long:"eradicate-verbose" "Print initial and final typestates" @@ -1419,7 +1415,6 @@ and eradicate_optional_present = !eradicate_optional_present and eradicate_propagate_return_nullable = !eradicate_propagate_return_nullable and eradicate_return_over_annotated = !eradicate_return_over_annotated and eradicate_debug = !eradicate_debug -and eradicate_trace = !eradicate_trace and eradicate_verbose = !eradicate_verbose and err_file_cmdline = !err_file and fail_on_bug = !fail_on_bug diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index a09ae9389..772e2ac62 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -185,7 +185,6 @@ val eradicate_optional_present : bool val eradicate_propagate_return_nullable : bool val eradicate_return_over_annotated : bool val eradicate_debug : bool -val eradicate_trace : bool val eradicate_verbose : bool val err_file_cmdline : string val fail_on_bug : bool diff --git a/infer/src/checkers/NodePrinter.ml b/infer/src/checkers/NodePrinter.ml new file mode 100644 index 000000000..29b3673ee --- /dev/null +++ b/infer/src/checkers/NodePrinter.ml @@ -0,0 +1,43 @@ +(* + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd + + +module L = Logging +module F = Format + +(** Simplified html node printer for checkers *) + +(** Mark the node visited and return the new session number *) +let new_session node = + let pname = Procdesc.Node.get_proc_name node in + let node_id = (Procdesc.Node.get_id node :> int) in + match Specs.get_summary pname with + | None -> + 0 + | Some summary -> + summary.stats.nodes_visited_fp <- IntSet.add node_id summary.stats.nodes_visited_fp; + incr summary.Specs.sessions; + !(summary.Specs.sessions) + +let start_session node = + if Config.write_html then + begin + let session = new_session node in + let source = (Procdesc.Node.get_loc node).file in + Printer.node_start_session node session source + end + +let finish_session node = + if Config.write_html then + begin + let source = (Procdesc.Node.get_loc node).file in + Printer.node_finish_session node source + end diff --git a/infer/src/checkers/NodePrinter.mli b/infer/src/checkers/NodePrinter.mli new file mode 100644 index 000000000..4a9087c68 --- /dev/null +++ b/infer/src/checkers/NodePrinter.mli @@ -0,0 +1,18 @@ +(* + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd + +(** Simplified html node printer for checkers *) + +(** To be called before analyzing a node *) +val start_session : Procdesc.Node.t -> unit + +(** To be called after analyzing a node *) +val finish_session : Procdesc.Node.t -> unit diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 3af57c4d6..b1f1bf0a7 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -115,18 +115,24 @@ struct let equal = TypeState.equal let join = TypeState.join Extension.ext let do_node tenv node typestate = + NodePrinter.start_session node; State.set_node node; let typestates_succ, typestates_exn = TypeCheck.typecheck_node tenv Extension.ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc find_canonical_duplicate annotated_signature typestate node linereader in - if Config.eradicate_trace then - IList.iter (fun typestate_succ -> - L.stdout - "Typestate After Node %a@\n%a@." - Procdesc.Node.pp node - (TypeState.pp Extension.ext) typestate_succ) - typestates_succ; + + if Config.write_html then + begin + let d_typestate ts = + L.d_strln (F.asprintf "%a" (TypeState.pp Extension.ext) ts) in + L.d_strln "before:"; + d_typestate typestate; + L.d_strln "after:"; + IList.iter d_typestate typestates_succ + end; + + NodePrinter.finish_session node; typestates_succ, typestates_exn let proc_throws _ = DontKnow end) in diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index 2b50a1972..3e01be452 100644 --- a/infer/src/eradicate/typeState.ml +++ b/infer/src/eradicate/typeState.ml @@ -122,7 +122,7 @@ let map_join m1 m2 = ) let join ext t1 t2 = - if Config.eradicate_trace + if Config.eradicate_debug then L.stderr "@.@.**********join@.-------@.%a@.------@.%a@.********@.@." (pp ext) t1 (pp ext) t2;