[checkers] print checkers summary in InferPrint

Summary: Useful for debugging checkers.

Reviewed By: sblackshear

Differential Revision: D4095479

fbshipit-source-id: afaa9c6

infer/src/backend/crashcontext.ml

@@ -132,3 +132,6 @@ let crashcontext_epilogue ~in_buck_mode =
     else Config.results_dir in
   collect_all_summaries
     root_summaries_dir Config.stacktrace Config.stacktraces_dir
+
+let pp_stacktree fmt st =
+  Format.fprintf fmt "%s" (Stacktree_j.string_of_stacktree st)

infer/src/backend/crashcontext.mli

@@ -40,3 +40,5 @@
    TODO: Similar integration with build systems other than buck.
 *)
 val crashcontext_epilogue : in_buck_mode:bool -> unit
+
+val pp_stacktree : Format.formatter -> Stacktree_t.stacktree -> unit

infer/src/backend/specs.ml

@@ -323,7 +323,7 @@ type payload =
     preposts : NormSpec.t list option; (** list of specs *)
     typestate : unit TypeState.t option; (** final typestate *)
     calls: call_summary option;
-    crashcontext_frame: Stacktree_j.stacktree option;
+    crashcontext_frame: Stacktree_t.stacktree option;
     (** Proc location and blame_range info for crashcontext analysis *)
     quandary : QuandarySummary.t option;
     siof : SiofDomain.astate option;
@@ -435,6 +435,12 @@ let get_signature summary =
   let decl = pp_to_string pp () in
   decl ^ "(" ^ !s ^ ")"
 
+let get_specs_from_preposts preposts =
+  Option.map_default NormSpec.tospecs [] preposts
+
+let get_specs_from_payload summary =
+  get_specs_from_preposts summary.payload.preposts
+
 let pp_summary_no_stats_specs fmt summary =
   let pp_pair fmt (x, y) = F.fprintf fmt "%s: %s" x y in
   F.fprintf fmt "%s@\n" (get_signature summary);
@@ -443,18 +449,26 @@ let pp_summary_no_stats_specs fmt summary =
   F.fprintf fmt "%a@\n" pp_pair (describe_phase summary);
   F.fprintf fmt "Dependency_map: @[%a@]@\n" pp_dependency_map summary.dependency_map
 
-let get_specs_from_payload summary =
+let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof } =
-  match summary.payload.preposts with
+  let pp_opt pp fmt = function
-  | Some specs -> NormSpec.tospecs specs
+    | Some x -> pp fmt x
-  | None -> []
+    | None -> () in
+  F.fprintf fmt "%a%a%a%a%a"
+    (pp_specs pe) (get_specs_from_preposts preposts)
+    (pp_opt (TypeState.pp TypeState.unit_ext)) typestate
+    (pp_opt Crashcontext.pp_stacktree) crashcontext_frame
+    (pp_opt QuandarySummary.pp) quandary
+    (pp_opt SiofDomain.pp) siof
+
 
 let pp_summary_text ~whole_seconds fmt summary =
   let err_log = summary.attributes.ProcAttributes.err_log in
   let pe = pe_text in
   pp_summary_no_stats_specs fmt summary;
-  F.fprintf fmt "%a@\n" pp_errlog err_log;
+  F.fprintf fmt "%a@\n%a%a"
-  F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats;
+    pp_errlog err_log
-  F.fprintf fmt "%a" (pp_specs pe) (get_specs_from_payload summary)
+    (pp_stats whole_seconds) summary.stats
+    (pp_payload pe) summary.payload
 
 let pp_summary_latex ~whole_seconds color fmt summary =
   let err_log = summary.attributes.ProcAttributes.err_log in

infer/src/eradicate/typeState.ml

@@ -32,6 +32,13 @@ type 'a ext =
     pp : Format.formatter -> 'a -> unit (** pretty print an extension *)
   }
 
+let unit_ext : unit ext = {
+  empty = ();
+  check_instr = (fun _ _ _ _ () _ _ -> ());
+  join = (fun () () -> ());
+  pp = (fun _ () -> ());
+}
+
 
 module M = Map.Make (struct
     type t = Exp.t

infer/src/eradicate/typeState.mli

@@ -45,3 +45,4 @@ val pp : 'a ext -> Format.formatter -> 'a t -> unit
 val range_add_locs : range -> (Location.t list) -> range
 val remove_id : Ident.t -> 'a t -> 'a t
 val set_extension : 'a t -> 'a -> 'a t
+val unit_ext : unit ext