[infer][checkers] Add a pretty print of the annotation reachability payload when printing summaries

Summary:
Useful for debugging.

The pretty-print now looks like:

  > infer -g -a checkers -- javac Test.java
  > InferPrint infer-out/specs/Test.callsExpensive\(\)\:void.62c98ff4bca3529caf7daec79add8b47.specs
  Procedure: void Test.callsExpensive()
  void void Test.callsExpensive()(class Test* this)
  Analyzed
  Phase: FOOTPRINT
  ERRORS:
  WARNINGS:
  FAILURE:NONE SYMOPS:0
  ThreadSafety: Threads: false Locks: false Accesses {  } Return Attributes: {  }
  AnnotationReachability: { _Expensive -> { void Test.expensive1() at [line 19], void Test.expensive2() at [line 21] }, _ForNonUiThread -> {  }, _UiThread -> {  }, ___infer_is_constructor -> {  } }

Reviewed By: jberdine

Differential Revision: D4813995

fbshipit-source-id: 928d951

infer/src/IR/CallSite.ml

@@ -40,3 +40,5 @@ module Set = PrettyPrintable.MakePPSet(struct
     let compare = compare
     let pp = pp
   end)
+
+module SetDomain = AbstractDomain.FiniteSet (Set)

infer/src/IR/CallSite.mli

@@ -26,3 +26,5 @@ val dummy : t
 val pp : F.formatter -> t -> unit
 
 module Set : PrettyPrintable.PPSet with type elt = t
+
+module SetDomain : module type of AbstractDomain.FiniteSet (Set)

infer/src/backend/specs.ml

@@ -319,14 +319,12 @@ type phase = FOOTPRINT | RE_EXECUTION [@@deriving compare]
 
 let equal_phase = [%compare.equal : phase]
 
-type call_summary = CallSite.Set.t Annot.Map.t
-
 (** Payload: results of some analysis *)
 type payload =
   {
     preposts : NormSpec.t list option; (** list of specs *)
     typestate : unit TypeState.t option; (** final typestate *)
-    calls: call_summary option;
+    calls: AnnotReachabilityDomain.astate option;
     crashcontext_frame: Stacktree_t.stacktree option;
     (** Proc location and blame_range info for crashcontext analysis *)
     quandary : QuandarySummary.t option;
@@ -444,18 +442,21 @@ let pp_summary_no_stats_specs fmt summary =
   F.fprintf fmt "%a@\n" pp_status summary.status;
   F.fprintf fmt "%a@\n" pp_pair (describe_phase summary)
 
-let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun } =
+let pp_payload pe fmt
-  let pp_opt pp fmt = function
+    { preposts; typestate; crashcontext_frame;
-    | Some x -> pp fmt x
+      quandary; siof; threadsafety; buffer_overrun; calls } =
+  let pp_opt prefix pp fmt = function
+    | Some x -> F.fprintf fmt "%s: %a\n" prefix pp x
     | None -> () in
-  F.fprintf fmt "%a%a%a%a%a%a%a@\n"
+  F.fprintf fmt "%a%a%a%a%a%a%a%a@\n"
-    (pp_specs pe) (get_specs_from_preposts preposts)
+    (pp_opt "PrePosts" (pp_specs pe)) (Option.map ~f:NormSpec.tospecs preposts)
-    (pp_opt (TypeState.pp TypeState.unit_ext)) typestate
+    (pp_opt "TypeState" (TypeState.pp TypeState.unit_ext)) typestate
-    (pp_opt Crashcontext.pp_stacktree) crashcontext_frame
+    (pp_opt "CrashContext" Crashcontext.pp_stacktree) crashcontext_frame
-    (pp_opt QuandarySummary.pp) quandary
+    (pp_opt "Quandary" QuandarySummary.pp) quandary
-    (pp_opt SiofDomain.pp) siof
+    (pp_opt "Siof" SiofDomain.pp) siof
-    (pp_opt ThreadSafetyDomain.pp_summary) threadsafety
+    (pp_opt "ThreadSafety" ThreadSafetyDomain.pp_summary) threadsafety
-    (pp_opt BufferOverrunDomain.Summary.pp) buffer_overrun
+    (pp_opt "BufferOverrun" BufferOverrunDomain.Summary.pp) buffer_overrun
+    (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp) calls
 
 
 let pp_summary_text fmt summary =

infer/src/backend/specs.mli

@@ -129,14 +129,12 @@ type phase = FOOTPRINT | RE_EXECUTION
 
 val equal_phase : phase -> phase -> bool
 
-type call_summary = CallSite.Set.t Annot.Map.t
-
 (** Payload: results of some analysis *)
 type payload =
   {
     preposts : NormSpec.t list option; (** list of specs *)
     typestate : unit TypeState.t option; (** final typestate *)
-    calls:  call_summary option; (** list of calls of the form (call, loc) *)
+    calls: AnnotReachabilityDomain.astate option; (** list of calls of the form (call, loc) *)
     crashcontext_frame: Stacktree_j.stacktree option;
     (** Procedure location and blame_range info for crashcontext analysis *)
     quandary : QuandarySummary.t option;

infer/src/checkers/AnnotReachabilityDomain.ml

@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) 2016 - 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.
+ *)
+
+include AbstractDomain.Map (Annot.Map) (CallSite.SetDomain)

infer/src/checkers/annotationReachability.ml

@@ -13,9 +13,6 @@ module F = Format
 module L = Logging
 module MF = MarkupFormatter
 
-module CallSiteSet = AbstractDomain.FiniteSet (CallSite.Set)
-module CallsDomain = AbstractDomain.Map (Annot.Map) (CallSiteSet)
-
 let dummy_constructor_annot = "__infer_is_constructor"
 
 let annotation_of_str annot_str =
@@ -46,21 +43,21 @@ let src_snk_pairs () =
 
 module Domain = struct
   module TrackingVar = AbstractDomain.FiniteSet (Var.Set)
-  module TrackingDomain = AbstractDomain.Pair (CallsDomain) (TrackingVar)
+  module TrackingDomain = AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingVar)
   include TrackingDomain
 
   let add_call key call ((call_map, vars) as astate) =
     let call_set =
-      try CallsDomain.find key call_map
+      try AnnotReachabilityDomain.find key call_map
-      with Not_found -> CallSiteSet.empty in
+      with Not_found -> CallSite.SetDomain.empty in
-    let call_set' = CallSiteSet.add call call_set in
+    let call_set' = CallSite.SetDomain.add call call_set in
     if phys_equal call_set' call_set
     then astate
-    else (CallsDomain.add key call_set' call_map, vars)
+    else (AnnotReachabilityDomain.add key call_set' call_map, vars)
 
   let stop_tracking (_ : astate) =
     (* The empty call map here prevents any subsequent calls to be added *)
-    (CallsDomain.empty, TrackingVar.empty)
+    (AnnotReachabilityDomain.empty, TrackingVar.empty)
 
   let add_tracking_var var (calls, previous_vars) =
     (calls, TrackingVar.add var previous_vars)
@@ -73,7 +70,7 @@ module Domain = struct
 end
 
 module Summary = Summary.Make (struct
-    type payload = CallsDomain.astate
+    type payload = AnnotReachabilityDomain.astate
 
     let update_payload call_map (summary : Specs.summary) =
       { summary with payload = { summary.payload with calls = Some call_map }}
@@ -146,7 +143,7 @@ let lookup_annotation_calls caller_pdesc annot pname : CallSite.t list =
       begin
         try
           Annot.Map.find annot call_map
-          |> CallSiteSet.elements
+          |> CallSite.SetDomain.elements
         with Not_found ->
           []
       end
@@ -276,8 +273,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let add_call_for_annot annot _ astate =
       let calls =
         try Annot.Map.find annot callee_call_map
-        with Not_found -> CallSiteSet.empty in
+        with Not_found -> CallSite.SetDomain.empty in
-      if (not (CallSiteSet.is_empty calls) || method_has_annot annot tenv callee_pname) &&
+      if (not (CallSite.SetDomain.is_empty calls) || method_has_annot annot tenv callee_pname) &&
          (not (method_is_sanitizer annot tenv caller_pname))
       then
         Domain.add_call annot call_site astate
@@ -355,7 +352,7 @@ module Interprocedural = struct
       let extract_calls_with_annot annot call_map =
         try
           Annot.Map.find annot call_map
-          |> CallSiteSet.elements
+          |> CallSite.SetDomain.elements
         with Not_found -> [] in
       let report_src_snk_path (calls : CallSite.t list) (src_annot: Annot.t) =
         if method_overrides_annot src_annot tenv proc_name
@@ -377,8 +374,8 @@ module Interprocedural = struct
       let init_map =
         List.fold
           ~f:(fun astate_acc (_, snk_annot) ->
-              CallsDomain.add snk_annot CallSiteSet.empty astate_acc)
+              AnnotReachabilityDomain.add snk_annot CallSite.SetDomain.empty astate_acc)
-          ~init:CallsDomain.empty
+          ~init:AnnotReachabilityDomain.empty
           (src_snk_pairs ()) in
       (init_map, Domain.TrackingVar.empty) in
     let compute_post proc_data =