From a9f3a70b93eec75d1f2c62b005a8517739be2719 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Fri, 28 Oct 2016 08:03:10 -0700
Subject: [PATCH] [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  |  3 +++
 infer/src/backend/crashcontext.mli |  2 ++
 infer/src/backend/specs.ml         | 30 ++++++++++++++++++++++--------
 infer/src/eradicate/typeState.ml   |  7 +++++++
 infer/src/eradicate/typeState.mli  |  1 +
 5 files changed, 35 insertions(+), 8 deletions(-)

diff --git a/infer/src/backend/crashcontext.ml b/infer/src/backend/crashcontext.ml
index 0aa75c3ff..654e6a0a5 100644
--- a/infer/src/backend/crashcontext.ml
+++ b/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)
diff --git a/infer/src/backend/crashcontext.mli b/infer/src/backend/crashcontext.mli
index 09c70efc9..4acae8edc 100644
--- a/infer/src/backend/crashcontext.mli
+++ b/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
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index d34eb66b7..2560889e5 100644
--- a/infer/src/backend/specs.ml
+++ b/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 =
-  match summary.payload.preposts with
-  | Some specs -> NormSpec.tospecs specs
-  | None -> []
+let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof } =
+  let pp_opt pp fmt = function
+    | Some x -> pp fmt x
+    | 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" (pp_stats whole_seconds) summary.stats;
-  F.fprintf fmt "%a" (pp_specs pe) (get_specs_from_payload summary)
+  F.fprintf fmt "%a@\n%a%a"
+    pp_errlog err_log
+    (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
diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml
index f49f91732..848cb05fa 100644
--- a/infer/src/eradicate/typeState.ml
+++ b/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
diff --git a/infer/src/eradicate/typeState.mli b/infer/src/eradicate/typeState.mli
index f35b3f646..3468df77c 100644
--- a/infer/src/eradicate/typeState.mli
+++ b/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