[infer][ondemand] skeleton code to have every checker update their respective payload in the analysis summary

Summary:
Changes every checker to take a summary as parameter and return the updated summary to the next checker. Since several operations, like `Reporting.log_*` are modifying the summary in memory by loading them from the in-memory cache of summaries, we currently need to rely on `Specs.get_summary_unsafe` to return the updated version of the summary.

This diff allows to change the API of `Reporting` to take a summary as input and progressively remove all the calls `Specs.get_summary_unsafe` independently from adding the possibility to run several checkers at the same time. The final objective to have every checker just passing around the summary of the procedure being analyzed, and having the in-memory cache only use to store the summaries of the callees.

Reviewed By: sblackshear

Differential Revision: D4649252

fbshipit-source-id: 98f7ca7

infer/src/backend/callbacks.ml

@@ -18,11 +18,11 @@ type proc_callback_args = {
   get_procs_in_file : Typ.Procname.t -> Typ.Procname.t list;
   idenv : Idenv.t;
   tenv : Tenv.t;
-  proc_name : Typ.Procname.t;
+  summary : Specs.summary;
   proc_desc : Procdesc.t;
 }
 
-type proc_callback_t = proc_callback_args -> unit
+type proc_callback_t = proc_callback_args -> Specs.summary
 
 type cluster_callback_t =
   Exe_env.t ->
@@ -58,10 +58,9 @@ let get_language proc_name = if Typ.Procname.is_java proc_name then Config.Java
 
 
 let reset_summary proc_name =
-  let should_reset =
-    is_none (Specs.get_summary proc_name) in
-  if should_reset
-  then
+  match Specs.get_summary proc_name with
+  | Some summary -> summary
+  | None ->
       let attributes_opt =
         Specs.proc_resolve_attributes proc_name in
       Specs.reset_summary proc_name attributes_opt None
@@ -82,24 +81,25 @@ let iterate_procedure_callbacks exe_env caller_pname =
     | None ->
         [] in
 
-  let update_time proc_name elapsed =
-    match Specs.get_summary proc_name with
-    | Some prev_summary ->
+  let update_time elapsed prev_summary =
     let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
     let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in
     let summary = { prev_summary with Specs.stats = stats } in
-        Specs.add_summary proc_name summary
-    | None -> () in
-
-  Option.iter
-    ~f:(fun (idenv, tenv, proc_name, proc_desc, _) ->
-        List.iter
-          ~f:(fun (language_opt, proc_callback) ->
+    let proc_name = Specs.get_proc_name summary in
+    Specs.add_summary proc_name summary;
+    summary in
+
+  match get_procedure_definition exe_env caller_pname with
+  | None -> ()
+  | Some (idenv, tenv, proc_name, proc_desc, _) ->
+      ignore
+        (List.fold
+           ~init:(reset_summary proc_name)
+           ~f:(fun summary (language_opt, proc_callback) ->
                let language_matches = match language_opt with
                  | Some language -> Config.equal_language language procedure_language
                  | None -> true in
                if language_matches then
-                begin
                  let init_time = Unix.gettimeofday () in
                  proc_callback
                    {
@@ -107,14 +107,15 @@ let iterate_procedure_callbacks exe_env caller_pname =
                      get_procs_in_file;
                      idenv;
                      tenv;
-                      proc_name;
+                     summary;
                      proc_desc;
-                    };
-                  let elapsed = Unix.gettimeofday () -. init_time in
-                  update_time proc_name elapsed
-                end)
-          !procedure_callbacks)
-    (get_procedure_definition exe_env caller_pname)
+                   }
+                 |> update_time (Unix.gettimeofday () -. init_time)
+               else
+                 summary)
+           !procedure_callbacks);
+      Specs.store_summary (Specs.get_summary_unsafe "iterate_procedure_callbacks" proc_name)
+
 
 (** Invoke all registered cluster callbacks on a cluster of procedures. *)
 let iterate_cluster_callbacks all_procs exe_env proc_names =
@@ -151,7 +152,7 @@ let iterate_callbacks call_graph exe_env =
     Cg.get_defined_nodes call_graph in
 
   (* Make sure summaries exists. *)
-  List.iter ~f:reset_summary procs_to_analyze;
+  List.iter ~f:(fun p -> ignore (reset_summary p)) procs_to_analyze;
 
   (* Invoke procedure callbacks. *)
   List.iter

infer/src/backend/callbacks.mli

@@ -16,7 +16,7 @@ type proc_callback_args = {
   get_procs_in_file : Typ.Procname.t -> Typ.Procname.t list;
   idenv : Idenv.t;
   tenv : Tenv.t;
-  proc_name : Typ.Procname.t;
+  summary : Specs.summary;
   proc_desc : Procdesc.t;
 }
 
@@ -26,7 +26,7 @@ type proc_callback_args = {
     - Idenv to look up the definition of ids in a cfg.
     - Type environment.
     - Procedure for the callback to act on. *)
-type proc_callback_t = proc_callback_args -> unit
+type proc_callback_t = proc_callback_args -> Specs.summary
 
 type cluster_callback_t =
   Exe_env.t ->

infer/src/backend/interproc.ml

@@ -1424,7 +1424,7 @@ let do_analysis_closures exe_env : Tasks.closure list =
       if Config.dynamic_dispatch = `Lazy
       then Some pdesc
       else None in
-    Specs.init_summary (nodes, proc_flags, calls, attributes, proc_desc_option) in
+    ignore (Specs.init_summary (nodes, proc_flags, calls, attributes, proc_desc_option)) in
 
   let callbacks =
     let get_proc_desc proc_name =

infer/src/backend/ondemand.ml

@@ -137,7 +137,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
       if Config.dynamic_dispatch = `Lazy
       then Some callee_pdesc
       else None in
-    Specs.reset_summary callee_pname attributes_opt callee_pdesc_option;
+    ignore (Specs.reset_summary callee_pname attributes_opt callee_pdesc_option);
     Specs.set_status callee_pname Specs.Active;
     source in
 

infer/src/backend/specs.ml

@@ -745,7 +745,8 @@ let init_summary
           ProcAttributes.proc_flags = proc_flags; };
       proc_desc_option;
     } in
-  Typ.Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name summary
+  Typ.Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name summary;
+  summary
 
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
 let reset_summary proc_name attributes_opt proc_desc_option =

infer/src/backend/specs.mli

@@ -213,17 +213,17 @@ val get_status : summary -> status
 val is_active : summary -> bool
 
 (** Initialize the summary for [proc_name] given dependent procs in list [depend_list].
-    Do nothing if a summary exists already. *)
+    This also stores the new summary in the spec table. *)
 val init_summary :
   ( Procdesc.Node.id list * (* nodes *)
     ProcAttributes.proc_flags * (* procedure flags *)
     (Typ.Procname.t * Location.t) list * (* calls *)
     ProcAttributes.t * (* attributes of the procedure *)
     Procdesc.t option) (* procdesc option *)
-  -> unit
+  -> summary
 
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
-val reset_summary : Typ.Procname.t -> ProcAttributes.t option -> Procdesc.t option -> unit
+val reset_summary : Typ.Procname.t -> ProcAttributes.t option -> Procdesc.t option -> summary
 
 (** Load procedure summary from the given file *)
 val load_summary : DB.filename -> summary option

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -444,8 +444,9 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit
     Dom.Summary.pp_summary F.err_formatter s;
     F.fprintf F.err_formatter "@]@."
 
-let checker : Callbacks.proc_callback_args -> unit
-  = fun ({ proc_name } as callback) ->
+let checker : Callbacks.proc_callback_args -> Specs.summary
+  = fun ({ summary } as callback) ->
+    let proc_name = Specs.get_proc_name summary in
     let make_extras _ = callback.get_proc_desc in
     let post =
       Interprocedural.compute_and_store_post
@@ -453,6 +454,9 @@ let checker : Callbacks.proc_callback_args -> unit
         ~make_extras
         callback
     in
+    begin
       match post with
       | Some s when Config.bo_debug >= 1 -> print_summary proc_name s
       | _ -> ()
+    end;
+    Specs.get_summary_unsafe "bufferOverrunChecker.checker" proc_name

infer/src/checkers/AbstractInterpreter.ml

@@ -159,7 +159,8 @@ end
 module Interprocedural (Summ : Summary.S) = struct
 
   let compute_and_store_post
-      ~compute_post ~make_extras { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } =
+      ~compute_post ~make_extras { Callbacks.get_proc_desc; proc_desc; tenv; } =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let analyze_ondemand_ _ pdesc =
       match compute_post (ProcData.make pdesc tenv (make_extras pdesc)) with
       | Some post ->

infer/src/checkers/BoundedCallTree.ml

@@ -163,7 +163,9 @@ let loaded_stacktraces =
   | None -> None
   | Some files -> Some (List.map ~f:Stacktrace.of_json_file files)
 
-let checker { Callbacks.proc_desc; tenv; get_proc_desc; } =
+let checker { Callbacks.proc_desc; tenv; get_proc_desc } : Specs.summary =
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  begin
     match loaded_stacktraces with
     | None -> failwith "Missing command line option. Either \
                         '--stacktrace stack.json' or '--stacktrace-dir ./dir' \
@@ -176,7 +178,9 @@ let checker { Callbacks.proc_desc; tenv; get_proc_desc; } =
     | Some stacktraces -> begin
         let extras = { get_proc_desc; stacktraces; } in
         SpecSummary.write_summary
-        (Procdesc.get_proc_name proc_desc)
+          proc_name
           (Some (stacktree_of_pdesc proc_desc "proc_start"));
         ignore (Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras) ~initial:Domain.empty)
       end
+  end;
+  Specs.get_summary_unsafe "BoundedCallTree.checker" proc_name

infer/src/checkers/SimpleChecker.ml

@@ -37,7 +37,7 @@ end
 
 module type S = sig
   (** add YourChecker.checker to registerCallbacks.ml to run your checker *)
-  val checker : Callbacks.proc_callback_args -> unit
+  val checker : Callbacks.proc_callback_t
 end
 
 module Make (Spec : Spec) : S = struct
@@ -82,7 +82,8 @@ module Make (Spec : Spec) : S = struct
 
   module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
 
-  let checker { Callbacks.proc_desc; proc_name; tenv; } =
+  let checker { Callbacks.proc_desc; tenv; } : Specs.summary =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let nodes = Procdesc.get_nodes proc_desc in
     let do_reporting node_id state =
       let astate_set = state.AbstractInterpreter.post in
@@ -99,5 +100,7 @@ module Make (Spec : Spec) : S = struct
           astate_set in
     let inv_map =
       Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) ~initial:Domain.empty in
-    Analyzer.InvariantMap.iter do_reporting inv_map
+    Analyzer.InvariantMap.iter do_reporting inv_map;
+    Specs.get_summary_unsafe "checker" proc_name
+
 end

infer/src/checkers/SimpleChecker.mli

@@ -20,6 +20,6 @@ sig
   val compare : astate -> astate -> int
 end
 
-module type S = sig val checker : Callbacks.proc_callback_args -> unit end
+module type S = sig val checker : Callbacks.proc_callback_t end
 
 module Make : functor (Spec : Spec) -> S

infer/src/checkers/Siof.ml

@@ -243,15 +243,18 @@ let compute_post proc_data =
     ~initial:(SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty)
   |> Option.map ~f:SiofDomain.normalize
 
-let checker ({ Callbacks.proc_desc; } as callback) =
+let checker ({ Callbacks.proc_desc } as callback) : Specs.summary =
   let post =
     Interprocedural.compute_and_store_post
       ~compute_post
       ~make_extras:ProcData.make_empty_extras
       callback in
   let pname = Procdesc.get_proc_name proc_desc in
+  begin
     match Typ.Procname.get_global_name_of_initializer pname with
     | Some gname ->
         siof_check proc_desc gname post
     | None ->
         ()
+  end;
+  Specs.get_summary_unsafe "SIOF checker" pname

infer/src/checkers/Siof.mli

@@ -9,4 +9,4 @@
 
 open! IStd
 
-val checker: Callbacks.proc_callback_args -> unit
+val checker: Callbacks.proc_callback_t

infer/src/checkers/ThreadSafety.ml

@@ -807,8 +807,10 @@ let analyze_procedure callback =
   | Some post -> post
   | None -> empty
 
-let checker callback =
-  ignore (analyze_procedure callback)
+let checker ({ Callbacks.summary } as callback_args) : Specs.summary =
+  let proc_name = Specs.get_proc_name summary in
+  ignore (analyze_procedure callback_args);
+  Specs.get_summary_unsafe "ThreadSafety.checker" proc_name
 
 (* creates a map from proc_envs to postconditions *)
 let make_results_table get_proc_desc file_env =
@@ -824,8 +826,9 @@ let make_results_table get_proc_desc file_env =
       | Some summ -> summ
       | None ->
           let callback_arg =
+            let summary = Specs.get_summary_unsafe "compute_post_for_procedure" proc_name in
             let get_procs_in_file _ = [] in
-            { Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; proc_name; proc_desc } in
+            { Callbacks.get_proc_desc; get_procs_in_file; idenv; tenv; summary; proc_desc } in
           analyze_procedure callback_arg in
   map_post_computation_over_procs compute_post_for_procedure file_env
 

infer/src/checkers/annotationReachability.ml

@@ -347,7 +347,8 @@ module Interprocedural = struct
   let method_is_expensive tenv pname =
     is_modeled_expensive tenv pname || is_expensive tenv pname
 
-  let check_and_report ({ Callbacks.proc_desc; proc_name; tenv; } as proc_data) =
+  let check_and_report ({ Callbacks.proc_desc; tenv; } as proc_data) : Specs.summary =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let loc = Procdesc.get_loc proc_desc in
     let expensive = is_expensive tenv proc_name in
     (* TODO: generalize so we can check subtyping on arbitrary annotations *)
@@ -397,6 +398,7 @@ module Interprocedural = struct
           (src_snk_pairs ()) in
       Domain.NonBottom
         (init_map, Domain.TrackingVar.empty) in
+    begin
       match compute_and_store_post
               ~compute_post:(Analyzer.compute_post ~initial)
               ~make_extras:ProcData.make_empty_extras
@@ -405,6 +407,9 @@ module Interprocedural = struct
           List.iter ~f:(report_src_snk_paths call_map) (src_snk_pairs ())
       | Some Domain.Bottom | None ->
           ()
+    end;
+    Specs.get_summary_unsafe "AnnotationReachability.checker" proc_name
+
 end
 
 let checker = Interprocedural.check_and_report

infer/src/checkers/checkDeadCode.ml

@@ -91,7 +91,8 @@ let check_final_state tenv proc_name proc_desc final_s =
     end
 
 (** Simple check for dead code. *)
-let callback_check_dead_code { Callbacks.proc_desc; proc_name; tenv } =
+let callback_check_dead_code { Callbacks.proc_desc; tenv } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
 
   let module DFDead = MakeDF(struct
       type t = State.t
@@ -113,4 +114,5 @@ let callback_check_dead_code { Callbacks.proc_desc; proc_name; tenv } =
       | DFDead.Dead_state -> ()
     end in
 
-  do_check ()
+  do_check ();
+  Specs.get_summary_unsafe "callback_check_dead_code" proc_name

infer/src/checkers/checkTraceCallSequence.ml

@@ -317,7 +317,8 @@ let check_final_state tenv proc_name proc_desc exit_node final_s =
 (** Check that the trace calls are balanced.
     This is done by using the most general control flow including exceptions.
     The begin() and end() function are assumed not to throw exceptions. *)
-let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv; tenv } : unit =
+let callback_check_trace_call_sequence { Callbacks.proc_desc; idenv; tenv } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
 
   let module DFTrace = MakeDF(struct
       type t = State.t
@@ -341,4 +342,5 @@ let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv;
       | DFTrace.Dead_state -> ()
     end in
 
-  if not (APIs.is_begin_or_end proc_name) then do_check ()
+  if not (APIs.is_begin_or_end proc_name) then do_check ();
+  Specs.get_summary_unsafe "callback_check_trace_call_sequence" proc_name

infer/src/checkers/checkers.ml

@@ -168,10 +168,12 @@ let report_calls_and_accesses tenv callback proc_desc instr =
       | None -> ()
 
 (** Report all field accesses and method calls of a procedure. *)
-let callback_check_access { Callbacks.tenv; proc_desc } =
+let callback_check_access { Callbacks.tenv; proc_desc; } =
   Procdesc.iter_instrs
     (fun _ instr  -> report_calls_and_accesses tenv Localise.proc_callback proc_desc instr)
-    proc_desc
+    proc_desc;
+  Specs.get_summary_unsafe "callback_check_access" (Procdesc.get_proc_name proc_desc)
+
 
 (** Report all field accesses and method calls of a class. *)
 let callback_check_cluster_access exe_env all_procs get_proc_desc _ =
@@ -189,7 +191,8 @@ let callback_check_cluster_access exe_env all_procs get_proc_desc _ =
 
 (** Looks for writeToParcel methods and checks whether read is in reverse *)
 let callback_check_write_to_parcel_java
-    pname_java ({ Callbacks.tenv; proc_desc; idenv; get_proc_desc } as args) =
+    pname_java { Callbacks.tenv; proc_desc; idenv; get_proc_desc } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = ref false in
 
   let is_write_to_parcel this_expr this_type =
@@ -265,17 +268,17 @@ let callback_check_write_to_parcel_java
       | rc:: rcs, wc:: wcs ->
           if not (is_inverse rc wc) then
             L.stdout "Serialization missmatch in %a for %a and %a@."
-              Typ.Procname.pp args.Callbacks.proc_name
+              Typ.Procname.pp proc_name
               Typ.Procname.pp rc
               Typ.Procname.pp wc
           else
             check_match (rcs, wcs)
       | rc:: _, [] ->
           L.stdout "Missing write in %a: for %a@."
-            Typ.Procname.pp args.Callbacks.proc_name Typ.Procname.pp rc
+            Typ.Procname.pp proc_name Typ.Procname.pp rc
       | _, wc:: _ ->
           L.stdout "Missing read in %a: for %a@."
-            Typ.Procname.pp args.Callbacks.proc_name Typ.Procname.pp wc
+            Typ.Procname.pp proc_name Typ.Procname.pp wc
       | _ ->
           () in
 
@@ -287,7 +290,7 @@ let callback_check_write_to_parcel_java
         if is_write_to_parcel this_exp this_type then begin
           if !verbose then
             L.stdout "Serialization check for %a@."
-              Typ.Procname.pp args.Callbacks.proc_name;
+              Typ.Procname.pp proc_name;
           try
             match parcel_constructors tenv this_type with
             | x :: _ ->
@@ -296,7 +299,7 @@ let callback_check_write_to_parcel_java
                  | None -> raise Not_found)
             | _ ->
                 L.stdout "No parcel constructor found for %a@."
-                  Typ.Procname.pp args.Callbacks.proc_name
+                  Typ.Procname.pp proc_name
           with Not_found ->
             if !verbose then L.stdout "Methods not available@."
         end
@@ -304,15 +307,18 @@ let callback_check_write_to_parcel_java
   Procdesc.iter_instrs do_instr proc_desc
 
 (** Looks for writeToParcel methods and checks whether read is in reverse *)
-let callback_check_write_to_parcel ({ Callbacks.proc_name } as args) =
-  match proc_name with
+let callback_check_write_to_parcel ({ Callbacks.summary } as args) =
+  begin
+    match Specs.get_proc_name summary with
     | Typ.Procname.Java pname_java ->
         callback_check_write_to_parcel_java pname_java args
-  | _ ->
-      ()
+    | _ -> ()
+  end;
+  summary
 
 (** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *)
-let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
+let callback_monitor_nullcheck { Callbacks.proc_desc; idenv } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = ref false in
 
   let class_formal_names = lazy (
@@ -389,23 +395,28 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
                ())
     | _ -> () in
   Procdesc.iter_instrs do_instr proc_desc;
-  summary_checks_of_formals ()
+  summary_checks_of_formals ();
+  Specs.get_summary_unsafe "callback_monitor_nullcheck" proc_name
 
 (** Test persistent state. *)
-let callback_test_state { Callbacks.proc_name } =
-  ST.pname_add proc_name "somekey" "somevalue"
+let callback_test_state { Callbacks.summary } =
+  let proc_name = Specs.get_proc_name summary in
+  ST.pname_add proc_name "somekey" "somevalue";
+  Specs.get_summary_unsafe "callback_test_state" proc_name
 
 (** Check the uses of VisibleForTesting *)
-let callback_checkVisibleForTesting { Callbacks.proc_desc } =
+let callback_checkVisibleForTesting { Callbacks.proc_desc; summary } =
   if Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting then
     begin
       let loc = Procdesc.get_loc proc_desc in
       let linereader = Printer.LineReader.create () in
       L.stdout "%a@." (PP.pp_loc_range linereader 10 10) loc
-    end
+    end;
+  summary
 
 (** Check for readValue and readValueAs json deserialization *)
-let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; proc_name } =
+let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = true in
 
   let ret_const_key = "return_const" in
@@ -498,10 +509,11 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
     ST.pname_add proc_name ret_const_key ret_const in
 
   store_return ();
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  Specs.get_summary_unsafe "callback_find_deserialization" proc_name
 
 (** Check field accesses. *)
-let callback_check_field_access { Callbacks.proc_desc } =
+let callback_check_field_access { Callbacks.proc_desc; summary } =
   let rec do_exp is_read = function
     | Exp.Var _ -> ()
     | Exp.UnOp (_, e, _) ->
@@ -541,10 +553,12 @@ let callback_check_field_access { Callbacks.proc_desc } =
     | Sil.Remove_temps _
     | Sil.Declare_locals _ ->
         () in
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  summary
 
 (** Print c method calls. *)
-let callback_print_c_method_calls { Callbacks.tenv; proc_desc; proc_name } =
+let callback_print_c_method_calls { Callbacks.tenv; proc_desc } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let do_instr node = function
     | Sil.Call (_, Exp.Const (Const.Cfun pn), (e, _):: _, loc, _)
       when Typ.Procname.is_c_method pn ->
@@ -569,10 +583,12 @@ let callback_print_c_method_calls { Callbacks.tenv; proc_desc; proc_name } =
           loc
           description
     | _ -> () in
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  Specs.get_summary_unsafe "callback_print_c_method_calls" proc_name
 
 (** Print access to globals. *)
-let callback_print_access_to_globals { Callbacks.tenv; proc_desc; proc_name } =
+let callback_print_access_to_globals { Callbacks.tenv; proc_desc } =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let do_pvar is_read pvar loc =
     let description =
       Printf.sprintf "%s of global %s"
@@ -597,4 +613,5 @@ let callback_print_access_to_globals { Callbacks.tenv; proc_desc; proc_name } =
     | Sil.Store (e, _, _, loc) when get_global_var e <> None ->
         Option.iter ~f:(fun pvar -> do_pvar false pvar loc) (get_global_var e)
     | _ -> () in
-  Procdesc.iter_instrs do_instr proc_desc
+  Procdesc.iter_instrs do_instr proc_desc;
+  Specs.get_summary_unsafe "callback_print_access_to_globals" proc_name

infer/src/checkers/dataflow.ml

@@ -171,7 +171,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct
 end (* MakeDF *)
 
 (** Example dataflow callback: compute the the distance from a node to the start node. *)
-let callback_test_dataflow { Callbacks.proc_desc; tenv } =
+let callback_test_dataflow { Callbacks.proc_desc; tenv; summary } =
   let verbose = false in
   let module DFCount = MakeDF(struct
       type t = int
@@ -187,4 +187,5 @@ let callback_test_dataflow { Callbacks.proc_desc; tenv } =
     match transitions node with
     | DFCount.Transition _ -> ()
     | DFCount.Dead_state -> () in
-  List.iter ~f:do_node (Procdesc.get_nodes proc_desc)
+  List.iter ~f:do_node (Procdesc.get_nodes proc_desc);
+  summary

infer/src/checkers/fragmentRetainsViewChecker.ml

@@ -51,9 +51,13 @@ let callback_fragment_retains_view_java
       | _ -> ()
     end
 
-let callback_fragment_retains_view ({ Callbacks.proc_name } as args) =
+let callback_fragment_retains_view ({ Callbacks.summary } as args) : Specs.summary =
+  let proc_name = Specs.get_proc_name summary in
+  begin
     match proc_name  with
     | Typ.Procname.Java pname_java ->
         callback_fragment_retains_view_java pname_java args
     | _ ->
         ()
+  end;
+  Specs.get_summary_unsafe "callback_fragment_retains_view" proc_name

infer/src/checkers/printfArgs.ml

@@ -206,8 +206,10 @@ let check_printf_args_ok tenv
       | None -> ())
   | _ -> ()
 
-let callback_printf_args { Callbacks.tenv; proc_desc; proc_name } : unit =
-  Procdesc.iter_instrs (fun n i -> check_printf_args_ok tenv n i proc_name proc_desc) proc_desc
+let callback_printf_args { Callbacks.tenv; proc_desc } : Specs.summary =
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  Procdesc.iter_instrs (fun n i -> check_printf_args_ok tenv n i proc_name proc_desc) proc_desc;
+  Specs.get_summary_unsafe "Callbacks.proc_callback_t" proc_name
 
 (*
 let printf_signature_to_string

infer/src/checkers/sqlChecker.ml

@@ -13,7 +13,8 @@ module L = Logging
 
 
 (** Find SQL statements in string concatenations *)
-let callback_sql { Callbacks.proc_desc; proc_name; tenv } =
+let callback_sql { Callbacks.proc_desc; tenv } : Specs.summary =
+  let proc_name = Procdesc.get_proc_name proc_desc in
   let verbose = false in
 
   (* Case insensitive SQL statement patterns *)
@@ -63,8 +64,11 @@ let callback_sql { Callbacks.proc_desc; proc_name; tenv } =
         end
     | _ -> () in
 
+  begin
     try
       let const_map = ConstantPropagation.build_const_map tenv proc_desc in
       if verbose then L.stdout "Analyzing %a...\n@." Typ.Procname.pp proc_name;
       Procdesc.iter_instrs (do_instr const_map) proc_desc
     with _ -> ()
+  end;
+  Specs.get_summary_unsafe "SqlChecker.callback_sql" proc_name

infer/src/eradicate/eradicate.ml

@@ -27,7 +27,7 @@ type parameters = TypeState.parameters
 (** Type for a module that provides a main callback function *)
 module type CallBackT =
 sig
-  val callback : TypeCheck.checks -> Callbacks.proc_callback_args -> unit
+  val callback : TypeCheck.checks -> Callbacks.proc_callback_t
 end (* CallBackT *)
 
 (** Extension to the type checker. *)
@@ -153,13 +153,14 @@ struct
       calls_this checks
       {
         Callbacks.proc_desc = curr_pdesc;
-        proc_name = curr_pname;
+        summary;
         get_proc_desc;
         idenv;
         tenv;
         get_procs_in_file;
       }
       annotated_signature linereader proc_loc : unit =
+    let curr_pname = Specs.get_proc_name summary in
 
     let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in
     let find_canonical_duplicate node =
@@ -340,7 +341,8 @@ struct
     update_summary curr_pname curr_pdesc final_typestate_opt
 
   (** Entry point for the eradicate-based checker infrastructure. *)
-  let callback checks ({ Callbacks.proc_desc; proc_name } as callback_args) =
+  let callback checks ({ Callbacks.proc_desc } as callback_args) : Specs.summary =
+    let proc_name = Procdesc.get_proc_name proc_desc in
     let calls_this = ref false in
 
     let filter_special_cases () =
@@ -353,6 +355,7 @@ struct
             Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes proc_desc) in
           Some annotated_signature
         end in
+    begin
       match filter_special_cases () with
       | None -> ()
       | Some annotated_signature ->
@@ -363,6 +366,8 @@ struct
 
           callback2
             calls_this checks callback_args annotated_signature linereader loc
+    end;
+    Specs.get_summary_unsafe "callback" proc_name
 
 end (* MkCallback *)
 
@@ -399,7 +404,7 @@ module Main =
 
 (** Eradicate checker for Java @Nullable annotations. *)
 let callback_eradicate
-    ({ Callbacks.get_proc_desc; proc_name } as callback_args) =
+    ({ Callbacks.get_proc_desc; summary } as callback_args) =
   let checks =
     {
       TypeCheck.eradicate = true;
@@ -409,24 +414,28 @@ let callback_eradicate
   let callbacks =
     let analyze_ondemand _ pdesc =
       let idenv_pname = Idenv.create pdesc in
+      let proc_name = Procdesc.get_proc_name pdesc in
+      let summary = Specs.get_summary_unsafe "Eradicate.analyze_ondemand" proc_name in
       Main.callback checks
         { callback_args with
           Callbacks.idenv = idenv_pname;
-          proc_name = (Procdesc.get_proc_name pdesc);
-          proc_desc = pdesc; };
-      Specs.get_summary_unsafe "callback_eradicate" (Procdesc.get_proc_name pdesc) in
+          summary;
+          proc_desc = pdesc; } in
     {
       Ondemand.analyze_ondemand;
       get_proc_desc;
     } in
 
-  if Ondemand.procedure_should_be_analyzed proc_name
+  if Ondemand.procedure_should_be_analyzed (Specs.get_proc_name summary)
   then
     begin
       Ondemand.set_callbacks callbacks;
-      Main.callback checks callback_args;
-      Ondemand.unset_callbacks ()
+      let final_summary = Main.callback checks callback_args in
+      Ondemand.unset_callbacks ();
+      final_summary
     end
+  else
+    summary
 
 (** Call the given check_return_type at the end of every procedure. *)
 let callback_check_return_type check_return_type callback_args =

infer/src/eradicate/eradicate.mli

@@ -23,7 +23,7 @@ type parameters = (Exp.t * Typ.t) list
 (** Type for a module that provides a main callback function *)
 module type CallBackT =
 sig
-  val callback : TypeCheck.checks -> Callbacks.proc_callback_args -> unit
+  val callback : TypeCheck.checks -> Callbacks.proc_callback_t
 end (* CallBackT *)
 
 

infer/src/quandary/TaintAnalysis.ml

@@ -495,7 +495,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
   module Interprocedural = AbstractInterpreter.Interprocedural(Summary)
 
-  let checker ({ Callbacks.tenv } as callback) =
+  let checker ({ Callbacks.tenv; summary } as callback) : Specs.summary =
+    let proc_name = Specs.get_proc_name summary in
 
     (* bind parameters to a trace with a tainted source (if applicable) *)
     let make_initial pdesc =
@@ -530,5 +531,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           then failwith "Couldn't compute post"
           else None in
     let make_extras = FormalMap.make in
-    ignore(Interprocedural.compute_and_store_post ~compute_post ~make_extras callback)
+    ignore (Interprocedural.compute_and_store_post ~compute_post ~make_extras callback);
+    Specs.get_summary_unsafe "taint analysis" proc_name
 end