[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

@@ -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: []
   };

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;

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;

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;

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

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 =

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 "<br>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 "<br>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 "<br>@\n";
@@ -393,9 +393,11 @@ let start_session node (loc: Location.t) proc_name session source =
   F.fprintf !curr_html_formatter "<LISTING>%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

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

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;

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

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

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

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

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

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;