[rename] specs -> summary, Summary -> SummaryPayload

Summary:
Attempt at a better naming scheme:
- `Specs.summary` are now `Summary.t`. The `Summary` module (replacing `Specs`) contains the summary of a procedure: the results of all the analyses, etc.
- `Summary.ml` is now `SummaryPayload.ml`. This concerns how each (AI) analysis extracts its payload from the master summary.
- Accordingly, checkers now define a `Payload` module where previously they defined a `Summary` module. The type is also cleaned up to use `t` instead of `payload`, etc.
- Cleaned up some names as a result, for instance `Specs.get_summary` -> `Summary.get`, etc.

Reviewed By: ngorogiannis

Differential Revision: D7935883

fbshipit-source-id: 1766545

infer/src/absint/Checkers.ml

@@ -20,7 +20,7 @@ module ST = struct
       Localise.custom_desc description [("always_report", string_of_bool always_report)]
     in
     let exn = exception_kind kind localized_description in
-    let proc_attributes = Specs.pdesc_resolve_attributes proc_desc in
+    let proc_attributes = Summary.pdesc_resolve_attributes proc_desc in
     (* Errors can be suppressed with annotations. An error of kind CHECKER_ERROR_NAME can be
        suppressed with the following annotations:
        - @android.annotation.SuppressLint("checker-error-name")

infer/src/absint/NodePrinter.ml

@@ -15,13 +15,13 @@ open! IStd
 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
+  match Summary.get pname with
   | None ->
       0
   | Some summary ->
       (summary.stats).nodes_visited_fp <- IntSet.add node_id summary.stats.nodes_visited_fp ;
-      incr summary.Specs.sessions ;
+      incr summary.Summary.sessions ;
-      !(summary.Specs.sessions)
+      !(summary.Summary.sessions)
 
 
 let start_session ~pp_name node =

infer/src/absint/Summary.ml

@@ -1,39 +0,0 @@
-(*
- * 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.
- *)
-
-open! IStd
-
-module type Payload = sig
-  type payload
-
-  val update_payload : payload -> Specs.summary -> Specs.summary
-
-  val read_payload : Specs.summary -> payload option
-end
-
-module type S = sig
-  type payload
-
-  val update_summary : payload -> Specs.summary -> Specs.summary
-
-  val read_summary : Procdesc.t -> Typ.Procname.t -> payload option
-end
-
-module Make (P : Payload) : S with type payload = P.payload = struct
-  type payload = P.payload
-
-  let update_summary payload summary = P.update_payload payload summary
-
-  let read_summary caller_pdesc callee_pname =
-    match Ondemand.analyze_proc_name ~caller_pdesc callee_pname with
-    | None ->
-        None
-    | Some summary ->
-        P.read_payload summary
-end

infer/src/absint/SummaryPayload.ml

@@ -0,0 +1,35 @@
+(*
+ * 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.
+ *)
+
+open! IStd
+
+module type Payload = sig
+  type t
+
+  val update_summary : t -> Summary.t -> Summary.t
+
+  val of_summary : Summary.t -> t option
+end
+
+module type S = sig
+  type t
+
+  val update_summary : t -> Summary.t -> Summary.t
+
+  val read_summary : Procdesc.t -> Typ.Procname.t -> t option
+end
+
+module Make (P : Payload) : S with type t = P.t = struct
+  type t = P.t
+
+  let update_summary = P.update_summary
+
+  let read_summary caller_pdesc callee_pname =
+    Ondemand.analyze_proc_name ~caller_pdesc callee_pname |> Option.bind ~f:P.of_summary
+end

infer/src/absint/SummaryPayload.mli

@@ -10,24 +10,23 @@
 open! IStd
 
 module type Payload = sig
-  type payload
+  type t
 
-  val update_payload : payload -> Specs.summary -> Specs.summary
+  val update_summary : t -> Summary.t -> Summary.t
   (** Update the corresponding part of the payload in the procedure summary *)
 
-  val read_payload : Specs.summary -> payload option
+  val of_summary : Summary.t -> t option
   (** Read the corresponding part of the payload from the procedure summary *)
 end
 
 module type S = sig
-  type payload
+  type t
 
-  val update_summary : payload -> Specs.summary -> Specs.summary
+  val update_summary : t -> Summary.t -> Summary.t
   (** Update the corresponding part of the payload in the procedure summary *)
 
-  val read_summary : Procdesc.t -> Typ.Procname.t -> payload option
+  val read_summary : Procdesc.t -> Typ.Procname.t -> t option
-  (** Return the payload for the given procedure.
+  (** Return the payload for the given procedure. Runs the analysis on-demand if necessary. *)
-      Runs the analysis on-demand if necessary *)
 end
 
-module Make (P : Payload) : S with type payload = P.payload
+module Make (P : Payload) : S with type t = P.t

infer/src/backend/InferAnalyze.ml

@@ -15,7 +15,7 @@ module L = Logging
 (** Create tasks to analyze an execution environment *)
 let create_exe_env_tasks source_file exe_env : Tasks.t =
   L.progressbar_file () ;
-  Specs.clear_spec_tbl () ;
+  Summary.clear_cache () ;
   Typ.Procname.SQLite.clear_cache () ;
   Random.self_init () ;
   Tasks.create

infer/src/backend/InferPrint.ml

@@ -96,11 +96,11 @@ type summary_val =
 
 (** compute values from summary data to export to csv format *)
 let summary_values summary =
-  let stats = summary.Specs.stats in
+  let stats = summary.Summary.stats in
-  let attributes = Specs.get_attributes summary in
+  let attributes = Summary.get_attributes summary in
-  let err_log = Specs.get_err_log summary in
+  let err_log = Summary.get_err_log summary in
-  let proc_name = Specs.get_proc_name summary in
+  let proc_name = Summary.get_proc_name summary in
-  let vsignature = Specs.get_signature summary in
+  let vsignature = Summary.get_signature summary in
   let specs = Tabulation.get_specs_from_payload summary in
   let lines_visited =
     let visited = ref BiabductionSummary.Visitedset.empty in
@@ -123,8 +123,8 @@ let summary_values summary =
   { vname= Typ.Procname.to_string proc_name
   ; vname_id= Typ.Procname.to_filename proc_name
   ; vspecs= List.length specs
-  ; vto= Option.value_map ~f:pp_failure ~default:"NONE" stats.Specs.stats_failure
+  ; vto= Option.value_map ~f:pp_failure ~default:"NONE" stats.Summary.stats_failure
-  ; vsymop= stats.Specs.symops
+  ; vsymop= stats.Summary.symops
   ; verr=
       Errlog.size
         (fun ekind in_footprint ->
@@ -493,12 +493,18 @@ module Stats = struct
 
   let process_summary error_filter summary linereader stats =
     let specs = Tabulation.get_specs_from_payload summary in
-    let found_errors = process_err_log error_filter linereader (Specs.get_err_log summary) stats in
+    let found_errors =
+      process_err_log error_filter linereader (Summary.get_err_log summary) stats
+    in
     let is_defective = found_errors in
     let is_verified = specs <> [] && not is_defective in
     let is_checked = not (is_defective || is_verified) in
     let is_timeout =
-      match Specs.(summary.stats.stats_failure) with None | Some (FKcrash _) -> false | _ -> true
+      match Summary.(summary.stats.stats_failure) with
+      | None | Some (FKcrash _) ->
+          false
+      | _ ->
+          true
     in
     stats.nprocs <- stats.nprocs + 1 ;
     stats.nspecs <- stats.nspecs + List.length specs ;
@@ -506,7 +512,7 @@ module Stats = struct
     if is_checked then stats.nchecked <- stats.nchecked + 1 ;
     if is_timeout then stats.ntimeouts <- stats.ntimeouts + 1 ;
     if is_defective then stats.ndefective <- stats.ndefective + 1 ;
-    process_loc (Specs.get_loc summary) stats
+    process_loc (Summary.get_loc summary) stats
 
 
   let num_files stats = Hashtbl.length stats.files
@@ -528,24 +534,24 @@ module Stats = struct
 end
 
 module StatsLogs = struct
-  let process _ (summary: Specs.summary) _ _ =
+  let process _ (summary: Summary.t) _ _ =
     let num_preposts =
       match summary.payload.biabduction with Some {preposts} -> List.length preposts | None -> 0
     in
     let clang_method_kind =
-      ProcAttributes.string_of_clang_method_kind (Specs.get_attributes summary).clang_method_kind
+      ProcAttributes.string_of_clang_method_kind (Summary.get_attributes summary).clang_method_kind
     in
-    let proc_name = Specs.get_proc_name summary in
+    let proc_name = Summary.get_proc_name summary in
     let lang = Typ.Procname.get_language proc_name in
     let stats =
       EventLogger.AnalysisStats
         { analysis_nodes_visited= IntSet.cardinal summary.stats.nodes_visited_re
         ; analysis_status= summary.stats.stats_failure
-        ; analysis_total_nodes= Specs.get_proc_desc summary |> Procdesc.get_nodes_num
+        ; analysis_total_nodes= Summary.get_proc_desc summary |> Procdesc.get_nodes_num
         ; clang_method_kind=
             (match lang with Language.Clang -> Some clang_method_kind | _ -> None)
         ; lang= Language.to_explicit_string lang
-        ; method_location= Specs.get_loc summary
+        ; method_location= Summary.get_loc summary
         ; method_name= Typ.Procname.to_string proc_name
         ; num_preposts
         ; symops= summary.stats.symops }
@@ -736,9 +742,9 @@ let pp_issues_of_error_log error_filter linereader proc_loc_opt procname err_log
 
 
 let collect_issues summary issues_acc =
-  let err_log = Specs.get_err_log summary in
+  let err_log = Summary.get_err_log summary in
-  let proc_name = Specs.get_proc_name summary in
+  let proc_name = Summary.get_proc_name summary in
-  let proc_location = Specs.get_loc summary in
+  let proc_location = Summary.get_loc summary in
   Errlog.fold
     (fun err_key err_data acc -> {Issue.proc_name; proc_location; err_key; err_data} :: acc)
     err_log issues_acc
@@ -761,8 +767,8 @@ let pp_stats error_filter linereader summary stats stats_format_list =
 
 
 let pp_summary summary =
-  L.result "Procedure: %a@\n%a@." Typ.Procname.pp (Specs.get_proc_name summary)
+  L.result "Procedure: %a@\n%a@." Typ.Procname.pp (Summary.get_proc_name summary) Summary.pp_text
-    Specs.pp_summary_text summary
+    summary
 
 
 let pp_summary_by_report_kind formats_by_report_kind summary error_filter linereader stats file
@@ -838,8 +844,8 @@ let pp_lint_issues filters formats_by_report_kind linereader procname error_log
 
 (** Process a summary *)
 let process_summary filters formats_by_report_kind linereader stats summary issues_acc =
-  let file = (Specs.get_loc summary).Location.file in
+  let file = (Summary.get_loc summary).Location.file in
-  let proc_name = Specs.get_proc_name summary in
+  let proc_name = Summary.get_proc_name summary in
   let error_filter = error_filter filters proc_name in
   let pp_simple_saved = !Config.pp_simple in
   Config.pp_simple := true ;
@@ -870,7 +876,7 @@ let spec_files_from_cmdline () =
 let get_summary_iterator () =
   let sorted_spec_files = List.sort ~compare:String.compare (spec_files_from_cmdline ()) in
   let do_spec f fname =
-    match Specs.load_summary (DB.filename_from_string fname) with
+    match Summary.load_from_file (DB.filename_from_string fname) with
     | None ->
         L.(die UserError) "Error: cannot open file %s@." fname
     | Some summary ->

infer/src/backend/Summary.ml

@@ -12,13 +12,11 @@ open! IStd
 module F = Format
 open PolyVariantEqual
 
-(** Execution statistics *)
 type stats =
   { stats_failure: SymOp.failure_kind option
-        (** what type of failure stopped the analysis (if any) *)
+  ; symops: int
-  ; symops: int  (** Number of SymOp's throughout the whole analysis of the function *)
+  ; mutable nodes_visited_fp: IntSet.t
-  ; mutable nodes_visited_fp: IntSet.t  (** Nodes visited during the footprint phase *)
+  ; mutable nodes_visited_re: IntSet.t }
-  ; mutable nodes_visited_re: IntSet.t  (** Nodes visited during the re-execution phase *) }
 
 type status = Pending | Analyzed [@@deriving compare]
 
@@ -28,7 +26,6 @@ let pp_status fmt status = F.pp_print_string fmt (string_of_status status)
 
 let equal_status = [%compare.equal : status]
 
-(** Payload: results of some analysis *)
 type payload =
   { annot_map: AnnotReachabilityDomain.astate option
   ; biabduction: BiabductionSummary.t option
@@ -44,12 +41,7 @@ type payload =
   ; cost: CostDomain.summary option
   ; starvation: StarvationDomain.summary option }
 
-type summary =
+type t = {payload: payload; sessions: int ref; stats: stats; status: status; proc_desc: Procdesc.t}
-  { payload: payload  (** payload containing the result of some analysis *)
-  ; sessions: int ref  (** Session number: how many nodes went trough symbolic execution *)
-  ; stats: stats  (** statistics: execution time and list of errors *)
-  ; status: status  (** Analysis status of the procedure *)
-  ; proc_desc: Procdesc.t  (** Proc desc of the procdure *) }
 
 let get_status summary = summary.status
 
@@ -67,11 +59,11 @@ let get_err_log summary = (get_attributes summary).ProcAttributes.err_log
 
 let get_loc summary = (get_attributes summary).ProcAttributes.loc
 
-type spec_tbl = summary Typ.Procname.Hash.t
+type cache = t Typ.Procname.Hash.t
 
-let spec_tbl : spec_tbl = Typ.Procname.Hash.create 128
+let cache : cache = Typ.Procname.Hash.create 128
 
-let clear_spec_tbl () = Typ.Procname.Hash.clear spec_tbl
+let clear_cache () = Typ.Procname.Hash.clear cache
 
 let pp_failure_kind_opt fmt failure_kind_opt =
   match failure_kind_opt with
@@ -103,7 +95,7 @@ let get_signature summary =
     (get_proc_name summary) !s
 
 
-let pp_summary_no_stats_specs fmt summary =
+let pp_no_stats_specs fmt summary =
   F.fprintf fmt "%s@\n" (get_signature summary) ;
   F.fprintf fmt "%a@\n" pp_status summary.status
 
@@ -150,17 +142,17 @@ let pp_payload pe fmt
     starvation
 
 
-let pp_summary_text fmt summary =
+let pp_text fmt summary =
   let pe = Pp.text in
-  pp_summary_no_stats_specs fmt summary ;
+  pp_no_stats_specs fmt summary ;
   F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) pp_stats summary.stats (pp_payload pe)
     summary.payload
 
 
-let pp_summary_html source color fmt summary =
+let pp_html source color fmt summary =
   let pe = Pp.html color in
   Io_infer.Html.pp_start_color fmt Black ;
-  F.fprintf fmt "@\n%a" pp_summary_no_stats_specs summary ;
+  F.fprintf fmt "@\n%a" pp_no_stats_specs summary ;
   Io_infer.Html.pp_end_color fmt () ;
   F.fprintf fmt "<br />%a<br />@\n" pp_stats summary.stats ;
   Errlog.pp_html source [] fmt (get_err_log summary) ;
@@ -175,8 +167,8 @@ let empty_stats =
 
 
 (** Add the summary to the table for the given function *)
-let add_summary (proc_name: Typ.Procname.t) (summary: summary) : unit =
+let add (proc_name: Typ.Procname.t) (summary: t) : unit =
-  Typ.Procname.Hash.replace spec_tbl proc_name summary
+  Typ.Procname.Hash.replace cache proc_name summary
 
 
 let specs_filename pname =
@@ -200,16 +192,14 @@ let specs_models_filename pname =
   DB.filename_from_string (Filename.concat Config.models_dir (specs_filename pname))
 
 
-let summary_exists_in_models pname =
+let has_model pname = Sys.file_exists (DB.filename_to_string (specs_models_filename pname)) = `Yes
-  Sys.file_exists (DB.filename_to_string (specs_models_filename pname)) = `Yes
 
-
+let summary_serializer : t Serialization.serializer =
-let summary_serializer : summary Serialization.serializer =
   Serialization.create_serializer Serialization.Key.summary
 
 
 (** Load procedure summary from the given file *)
-let load_summary specs_file = Serialization.read_from_file summary_serializer specs_file
+let load_from_file specs_file = Serialization.read_from_file summary_serializer specs_file
 
 (** Load procedure summary for the given procedure name and update spec table *)
 let load_summary_to_spec_table =
@@ -218,7 +208,7 @@ let load_summary_to_spec_table =
     | Some _, _ | _, [] ->
         summ_opt
     | None, specs_dir :: specs_dirs ->
-        load_summary (specs_library_filename specs_dir proc_name)
+        load_from_file (specs_library_filename specs_dir proc_name)
         |> or_load_summary_libs specs_dirs proc_name
   in
   let load_summary_ziplibs zip_specs_filename =
@@ -230,31 +220,27 @@ let load_summary_to_spec_table =
   in
   fun proc_name ->
     let summ_opt =
-      None |> or_from load_summary res_dir_specs_filename proc_name
+      load_from_file (res_dir_specs_filename proc_name)
-      |> or_from load_summary specs_models_filename proc_name
+      |> or_from load_from_file specs_models_filename proc_name
       |> or_from load_summary_ziplibs specs_filename proc_name
       |> or_load_summary_libs Config.specs_library proc_name
     in
-    Option.iter ~f:(add_summary proc_name) summ_opt ;
+    Option.iter ~f:(add proc_name) summ_opt ;
     summ_opt
 
 
-let get_summary proc_name =
+let get proc_name =
-  try Some (Typ.Procname.Hash.find spec_tbl proc_name) with Caml.Not_found ->
+  try Some (Typ.Procname.Hash.find cache proc_name) with Caml.Not_found ->
     load_summary_to_spec_table proc_name
 
 
-let get_summary_unsafe proc_name = Option.value_exn (get_summary proc_name)
+let get_unsafe proc_name = Option.value_exn (get proc_name)
 
 (** Check if the procedure is from a library:
     It's not defined, and there is no spec file for it. *)
 let proc_is_library proc_attributes =
   if not proc_attributes.ProcAttributes.is_defined then
-    match get_summary proc_attributes.ProcAttributes.proc_name with
+    match get proc_attributes.ProcAttributes.proc_name with None -> true | Some _ -> false
-    | None ->
-        true
-    | Some _ ->
-        false
   else false
 
 
@@ -264,7 +250,7 @@ let proc_is_library proc_attributes =
     If no attributes can be found, return None.
 *)
 let proc_resolve_attributes proc_name =
-  match get_summary proc_name with
+  match get proc_name with
   | Some summary ->
       Some (get_attributes summary)
   | None ->
@@ -283,11 +269,11 @@ let pdesc_resolve_attributes proc_desc =
 
 
 (** Save summary for the procedure into the spec database *)
-let store_summary (summ: summary) =
+let store (summ: t) =
   let final_summary = {summ with status= Analyzed} in
   let proc_name = get_proc_name final_summary in
   (* Make sure the summary in memory is identical to the saved one *)
-  add_summary proc_name final_summary ;
+  add proc_name final_summary ;
   Serialization.write_to_file summary_serializer
     (res_dir_specs_filename proc_name)
     ~data:final_summary
@@ -316,7 +302,7 @@ let init_summary proc_desc =
   let summary =
     {sessions= ref 0; payload= empty_payload; stats= empty_stats; status= Pending; proc_desc}
   in
-  Typ.Procname.Hash.replace spec_tbl (Procdesc.get_proc_name proc_desc) summary ;
+  Typ.Procname.Hash.replace cache (Procdesc.get_proc_name proc_desc) summary ;
   summary
 
 
@@ -327,6 +313,6 @@ let dummy =
 
 
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
-let reset_summary proc_desc = init_summary proc_desc
+let reset proc_desc = init_summary proc_desc
 
 (* =============== END of support for spec tables =============== *)

infer/src/backend/Summary.mli

@@ -10,9 +10,8 @@
 
 open! IStd
 
-(** Specifications and spec table *)
+(** Procedure summaries: the results of the capture and all the analysis for a single procedure,
-
+   plus some statistics *)
-(** {2 Spec Tables} *)
 
 (** Execution statistics *)
 type stats =
@@ -22,16 +21,16 @@ type stats =
   ; mutable nodes_visited_fp: IntSet.t  (** Nodes visited during the footprint phase *)
   ; mutable nodes_visited_re: IntSet.t  (** Nodes visited during the re-execution phase *) }
 
-(** Analysis status of the procedure:
+(** Analysis status of the procedure *)
-    - Pending means that the summary has been created by the procedure has not been analyzed yet
+type status =
-    - Analyzed means that the analysis of the procedure is finished *)
+  | Pending  (** the summary has been created by the procedure has not been analyzed yet *)
-type status = Pending | Analyzed
+  | Analyzed  (** the analysis of the procedure is finished *)
 
 val equal_status : status -> status -> bool
 
 val string_of_status : status -> string
 
-(** Payload: results of some analysis *)
+(** analysis results *)
 type payload =
   { annot_map: AnnotReachabilityDomain.astate option
   ; biabduction: BiabductionSummary.t option
@@ -47,63 +46,62 @@ type payload =
   ; cost: CostDomain.summary option
   ; starvation: StarvationDomain.summary option }
 
-(** Procedure summary *)
+(** summary of a procedure name *)
-type summary =
+type t =
-  { payload: payload  (** payload containing the result of some analysis *)
+  { payload: payload
   ; sessions: int ref  (** Session number: how many nodes went trough symbolic execution *)
-  ; stats: stats  (** statistics: execution time and list of errors *)
+  ; stats: stats
-  ; status: status  (** Analysis status of the procedure *)
+  ; status: status
   ; proc_desc: Procdesc.t }
 
-val dummy : summary
+val dummy : t
 (** dummy summary for testing *)
 
-val add_summary : Typ.Procname.t -> summary -> unit
+val add : Typ.Procname.t -> t -> unit
 (** Add the summary to the table for the given function *)
 
-val summary_exists_in_models : Typ.Procname.t -> bool
+val has_model : Typ.Procname.t -> bool
 (** Check if a summary for a given procedure exists in the models directory *)
 
-val clear_spec_tbl : unit -> unit
+val clear_cache : unit -> unit
-(** remove all the elements from the spec table *)
+(** remove all the elements from the cache of summaries *)
 
-val get_summary : Typ.Procname.t -> summary option
+val get : Typ.Procname.t -> t option
 (** Return the summary option for the procedure name *)
 
-val get_proc_name : summary -> Typ.Procname.t
+val get_proc_name : t -> Typ.Procname.t
 (** Get the procedure name *)
 
-val get_proc_desc : summary -> Procdesc.t
+val get_proc_desc : t -> Procdesc.t
 
-val get_attributes : summary -> ProcAttributes.t
+val get_attributes : t -> ProcAttributes.t
 (** Get the attributes of the procedure. *)
 
-val get_formals : summary -> (Mangled.t * Typ.t) list
+val get_formals : t -> (Mangled.t * Typ.t) list
 (** Get the formal parameters of the procedure *)
 
-val get_err_log : summary -> Errlog.t
+val get_err_log : t -> Errlog.t
 
-val get_loc : summary -> Location.t
+val get_loc : t -> Location.t
 
-val get_signature : summary -> string
+val get_signature : t -> string
 (** Return the signature of a procedure declaration as a string *)
 
-val get_summary_unsafe : Typ.Procname.t -> summary
+val get_unsafe : Typ.Procname.t -> t
 (** @deprecated Return the summary for the procedure name. Raises an exception when not found. *)
 
-val get_status : summary -> status
+val get_status : t -> status
 (** Return the status (active v.s. inactive) of a procedure summary *)
 
-val reset_summary : Procdesc.t -> summary
+val reset : Procdesc.t -> t
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
 
-val load_summary : DB.filename -> summary option
+val load_from_file : DB.filename -> t option
-(** Load procedure summary from the given file *)
 
-val pp_summary_html : SourceFile.t -> Pp.color -> Format.formatter -> summary -> unit
+val pp_html : SourceFile.t -> Pp.color -> Format.formatter -> t -> unit
 (** Print the summary in html format *)
 
-val pp_summary_text : Format.formatter -> summary -> unit
+val pp_text : Format.formatter -> t -> unit
 (** Print the summary in text format *)
 
 val pdesc_resolve_attributes : Procdesc.t -> ProcAttributes.t
@@ -120,5 +118,5 @@ val proc_is_library : ProcAttributes.t -> bool
 (** Check if the procedure is from a library:
     It's not defined, and there is no spec file for it. *)
 
-val store_summary : summary -> unit
+val store : t -> unit
 (** Save summary for the procedure into the spec database *)

infer/src/backend/callbacks.ml

@@ -16,11 +16,11 @@ type proc_callback_args =
   { get_proc_desc: Typ.Procname.t -> Procdesc.t option
   ; get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
   ; tenv: Tenv.t
-  ; summary: Specs.summary
+  ; summary: Summary.t
   ; proc_desc: Procdesc.t
   ; exe_env: Exe_env.t }
 
-type proc_callback_t = proc_callback_args -> Specs.summary
+type proc_callback_t = proc_callback_args -> Summary.t
 
 type cluster_callback_args =
   { procedures: (Tenv.t * Procdesc.t) list
@@ -135,7 +135,7 @@ let iterate_callbacks (exe_env: Exe_env.t) =
     | Some _ as pdesc_opt ->
         pdesc_opt
     | None ->
-        Option.map ~f:Specs.get_proc_desc (Specs.get_summary proc_name)
+        Option.map ~f:Summary.get_proc_desc (Summary.get proc_name)
   in
   let analyze_ondemand summary proc_desc =
     iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc
@@ -147,7 +147,7 @@ let iterate_callbacks (exe_env: Exe_env.t) =
     SourceFiles.proc_names_of_source exe_env.source_file
   in
   if Config.dump_duplicate_symbols then dump_duplicate_procs exe_env procs_to_analyze ;
-  let analyze_proc_name pname = ignore (Ondemand.analyze_proc_name pname : Specs.summary option) in
+  let analyze_proc_name pname = ignore (Ondemand.analyze_proc_name pname : Summary.t option) in
   List.iter ~f:analyze_proc_name procs_to_analyze ;
   (* Invoke cluster callbacks. *)
   iterate_cluster_callbacks procs_to_analyze exe_env get_proc_desc ;

infer/src/backend/callbacks.mli

@@ -15,7 +15,7 @@ type proc_callback_args =
   { get_proc_desc: Typ.Procname.t -> Procdesc.t option
   ; get_procs_in_file: Typ.Procname.t -> Typ.Procname.t list
   ; tenv: Tenv.t
-  ; summary: Specs.summary
+  ; summary: Summary.t
   ; proc_desc: Procdesc.t
   ; exe_env: Exe_env.t }
 
@@ -24,7 +24,7 @@ type proc_callback_args =
     - get_proc_desc to get a proc desc from a proc name
     - Type environment.
     - Procedure for the callback to act on. *)
-type proc_callback_t = proc_callback_args -> Specs.summary
+type proc_callback_t = proc_callback_args -> Summary.t
 
 type cluster_callback_args =
   { procedures: (Tenv.t * Procdesc.t) list

infer/src/backend/ondemand.ml

@@ -14,7 +14,7 @@ open! IStd
 module L = Logging
 module F = Format
 
-type analyze_ondemand = Specs.summary -> Procdesc.t -> Specs.summary
+type analyze_ondemand = Summary.t -> Procdesc.t -> Summary.t
 
 type get_proc_desc = Typ.Procname.t -> Procdesc.t option
 
@@ -51,9 +51,9 @@ let should_create_summary proc_name proc_attributes =
 
 let should_be_analyzed proc_name proc_attributes =
   let already_analyzed () =
-    match Specs.get_summary proc_name with
+    match Summary.get proc_name with
     | Some summary ->
-        Specs.equal_status (Specs.get_status summary) Specs.Analyzed
+        Summary.equal_status (Summary.get_status summary) Summary.Analyzed
     | None ->
         false
   in
@@ -63,7 +63,7 @@ let should_be_analyzed proc_name proc_attributes =
 
 
 let procedure_should_be_analyzed proc_name =
-  match Specs.proc_resolve_attributes proc_name with
+  match Summary.proc_resolve_attributes proc_name with
   | Some proc_attributes when Config.reactive_capture && not proc_attributes.is_defined ->
       (* try to capture procedure first *)
       let defined_proc_attributes = OndemandCapture.try_capture proc_attributes in
@@ -122,12 +122,12 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc =
       Typ.Procname.pp callee_pname ;
   let preprocess () =
     incr nesting ;
-    let initial_summary = Specs.reset_summary callee_pdesc in
+    let initial_summary = Summary.reset callee_pdesc in
     add_active callee_pname ; initial_summary
   in
   let postprocess summary =
     decr nesting ;
-    Specs.store_summary summary ;
+    Summary.store summary ;
     remove_active callee_pname ;
     Printer.write_proc_html callee_pdesc ;
     log_elapsed_time () ;
@@ -135,18 +135,15 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc =
   in
   let log_error_and_continue exn summary kind =
     Reporting.log_error summary exn ;
-    let stats = {summary.Specs.stats with Specs.stats_failure= Some kind} in
+    let stats = {summary.Summary.stats with Summary.stats_failure= Some kind} in
     let payload =
       let biabduction =
         Some BiabductionSummary.{preposts= []; phase= Tabulation.get_phase summary}
       in
-      {summary.Specs.payload with Specs.biabduction}
+      {summary.Summary.payload with Summary.biabduction}
     in
-    let new_summary = {summary with Specs.stats; payload} in
+    let new_summary = {summary with Summary.stats; payload} in
-    Specs.store_summary new_summary ;
+    Summary.store new_summary ; remove_active callee_pname ; log_elapsed_time () ; new_summary
-    remove_active callee_pname ;
-    log_elapsed_time () ;
-    new_summary
   in
   let old_state = save_global_state () in
   let initial_summary = preprocess () in
@@ -187,7 +184,7 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc =
         let proc_attributes = Procdesc.get_attributes callee_pdesc in
         if should_be_analyzed callee_pname proc_attributes then
           analyze_proc ~caller_pdesc callee_pdesc
-        else Specs.get_summary callee_pname
+        else Summary.get callee_pname
       in
       Typ.Procname.Hash.add cache callee_pname summary_option ;
       summary_option
@@ -207,8 +204,8 @@ let analyze_proc_name ?caller_pdesc callee_pname =
           | Some callee_pdesc ->
               analyze_proc ?caller_pdesc callee_pdesc
           | None ->
-              Specs.get_summary callee_pname
+              Summary.get callee_pname
-        else Specs.get_summary callee_pname
+        else Summary.get callee_pname
       in
       Typ.Procname.Hash.add cache callee_pname summary_option ;
       summary_option

infer/src/backend/ondemand.mli

@@ -11,7 +11,7 @@ open! IStd
 
 (** Module for on-demand analysis. *)
 
-type analyze_ondemand = Specs.summary -> Procdesc.t -> Specs.summary
+type analyze_ondemand = Summary.t -> Procdesc.t -> Summary.t
 
 type get_proc_desc = Typ.Procname.t -> Procdesc.t option
 
@@ -20,11 +20,11 @@ type callbacks = {analyze_ondemand: analyze_ondemand; get_proc_desc: get_proc_de
 val get_proc_desc : get_proc_desc
 (** Find a proc desc for the procedure, perhaps loading it from disk. *)
 
-val analyze_proc_desc : caller_pdesc:Procdesc.t -> Procdesc.t -> Specs.summary option
+val analyze_proc_desc : caller_pdesc:Procdesc.t -> Procdesc.t -> Summary.t option
 (** [analyze_proc_desc ~caller_pdesc callee_pdesc] performs an on-demand analysis of callee_pdesc
    triggered during the analysis of caller_pdesc *)
 
-val analyze_proc_name : ?caller_pdesc:Procdesc.t -> Typ.Procname.t -> Specs.summary option
+val analyze_proc_name : ?caller_pdesc:Procdesc.t -> Typ.Procname.t -> Summary.t option
 (** [analyze_proc_name ~caller_pdesc proc_name] performs an on-demand analysis of proc_name
    triggered during the analysis of caller_pdesc *)
 

infer/src/backend/printer.ml

@@ -72,16 +72,16 @@ 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 node =
-  match Specs.get_summary (Procdesc.Node.get_proc_name node) with
+  match Summary.get (Procdesc.Node.get_proc_name node) with
   | None ->
       (false, false)
   | Some summary ->
-      let stats = summary.Specs.stats in
+      let stats = summary.Summary.stats in
       let is_visited_fp =
-        IntSet.mem (Procdesc.Node.get_id node :> int) stats.Specs.nodes_visited_fp
+        IntSet.mem (Procdesc.Node.get_id node :> int) stats.Summary.nodes_visited_fp
       in
       let is_visited_re =
-        IntSet.mem (Procdesc.Node.get_id node :> int) stats.Specs.nodes_visited_re
+        IntSet.mem (Procdesc.Node.get_id node :> int) stats.Summary.nodes_visited_re
       in
       (is_visited_fp, is_visited_re)
 
@@ -387,11 +387,11 @@ let write_proc_html pdesc =
          [])
       linenum ;
     Pp.seq (pp_node_link [] ~description:true) fmt nodes ;
-    match Specs.get_summary pname with
+    match Summary.get pname with
     | None ->
         ()
     | Some summary ->
-        Specs.pp_summary_html source Black fmt summary ;
+        Summary.pp_html source Black fmt summary ;
         Io_infer.Html.close (fd, fmt) )
 
 
@@ -435,7 +435,7 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro
   in
   if process_proc then (
     List.iter ~f:process_node (Procdesc.get_nodes proc_desc) ;
-    match Specs.get_summary proc_name with
+    match Summary.get proc_name with
     | None ->
         ()
     | Some summary ->
@@ -444,7 +444,7 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro
             proof_cover :=
               BiabductionSummary.Visitedset.union sp.BiabductionSummary.visited !proof_cover )
           (Tabulation.get_specs_from_payload summary) ;
-        Errlog.update global_err_log (Specs.get_err_log summary) )
+        Errlog.update global_err_log (Summary.get_err_log summary) )
 
 
 (** Create filename.ext.html. *)
@@ -484,7 +484,7 @@ let write_html_file linereader filename procs =
         match Procdesc.Node.get_kind n with
         | Procdesc.Node.Start_node proc_name ->
             let num_specs =
-              match Specs.get_summary proc_name with
+              match Summary.get proc_name with
               | None ->
                   0
               | Some summary ->

infer/src/backend/reporting.ml

@@ -41,7 +41,7 @@ let log_issue_from_errlog procname ?clang_method_kind err_kind err_log ?loc ?nod
 
 let log_issue_from_summary err_kind summary ?loc ?node_id ?session ?ltr ?linters_def_file ?doc_url
     ?access exn =
-  let attrs = Specs.get_attributes summary in
+  let attrs = Summary.get_attributes summary in
   let procname = attrs.proc_name in
   let clang_method_kind = attrs.clang_method_kind in
   let is_java_generated_method =
@@ -54,24 +54,24 @@ let log_issue_from_summary err_kind summary ?loc ?node_id ?session ?ltr ?linters
   let should_suppress_lint =
     Language.curr_language_is Java
     && Annotations.ia_is_suppress_lint
-         (fst (Specs.get_attributes summary).ProcAttributes.method_annotation)
+         (fst (Summary.get_attributes summary).ProcAttributes.method_annotation)
   in
   if should_suppress_lint || is_java_generated_method then () (* Skip the reporting *)
   else
-    let err_log = Specs.get_err_log summary in
+    let err_log = Summary.get_err_log summary in
     log_issue_from_errlog procname ~clang_method_kind err_kind err_log ?loc ?node_id ?session ?ltr
       ?linters_def_file ?doc_url ?access exn
 
 
 let log_issue_deprecated ?(store_summary= false) err_kind proc_name ?loc ?node_id ?session ?ltr
     ?linters_def_file ?doc_url ?access exn =
-  match Specs.get_summary proc_name with
+  match Summary.get proc_name with
   | Some summary ->
       log_issue_from_summary err_kind summary ?loc ?node_id ?session ?ltr ?linters_def_file
         ?doc_url ?access exn ;
       if store_summary then
         (* TODO (#16348004): This is currently needed as ThreadSafety works as a cluster checker *)
-        Specs.store_summary summary
+        Summary.store summary
   | None ->
       L.(die InternalError)
         "Trying to report error on procedure %a, but cannot because no summary exists for this \

infer/src/backend/reporting.mli

@@ -37,10 +37,10 @@ val log_issue_from_errlog :
   -> log_issue_from_errlog
 (** Report an issue of a given kind  in the given error log. *)
 
-val log_error : Specs.summary -> log_t
+val log_error : Summary.t -> log_t
 (** Add an error to the given summary. *)
 
-val log_warning : Specs.summary -> log_t
+val log_warning : Summary.t -> log_t
 (** Add an warning to the given summary. *)
 
 val log_issue_external :

infer/src/biabduction/BuiltinDefn.ml

@@ -650,7 +650,7 @@ let execute_pthread_create ({Builtin.tenv; prop_; path; args; exe_env} as builti
           let fun_name = Pvar.get_name pvar in
           let fun_string = Mangled.to_string fun_name in
           L.d_strln ("pthread_create: calling function " ^ fun_string) ;
-          match Specs.get_summary (Typ.Procname.from_string_c_fun fun_string) with
+          match Summary.get (Typ.Procname.from_string_c_fun fun_string) with
           | None ->
               assert false
           | Some callee_summary ->

infer/src/biabduction/Rearrange.ml

@@ -1507,7 +1507,7 @@ let is_weak_captured_var pdesc var_name =
 
 let var_has_annotation ?(check_weak_captured_var= false) pdesc is_annotation pvar =
   let is_weak_captured_var = is_weak_captured_var pdesc (Pvar.to_string pvar) in
-  let ann_sig = Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes pdesc) in
+  let ann_sig = Models.get_modelled_annotated_signature (Summary.pdesc_resolve_attributes pdesc) in
   AnnotatedSignature.param_has_annot is_annotation pvar ann_sig
   || (check_weak_captured_var && is_weak_captured_var)
 

infer/src/biabduction/RetainCycles.ml

@@ -241,7 +241,7 @@ let report_cycle tenv pname prop =
         Otherwise we report a retain cycle. *)
   let cycles = get_retain_cycles tenv prop in
   RetainCyclesType.Set.iter RetainCyclesType.print_cycle cycles ;
-  match Specs.get_summary pname with
+  match Summary.get pname with
   | Some summary ->
       if RetainCyclesType.Set.cardinal cycles > 0 then (
         RetainCyclesType.Set.iter

infer/src/biabduction/SymExec.ml

@@ -371,7 +371,7 @@ let reason_to_skip ~callee_desc : string option =
   in
   match callee_desc with
   | `Summary callee_summary ->
-      let attr_reason = Specs.get_attributes callee_summary |> reason_from_attributes in
+      let attr_reason = Summary.get_attributes callee_summary |> reason_from_attributes in
       if Option.is_some attr_reason then attr_reason
       else if List.is_empty (Tabulation.get_specs_from_payload callee_summary) then
         Some "empty list of specs"
@@ -517,7 +517,7 @@ let method_exists right_proc_name methods =
     | Some attrs ->
         attrs.ProcAttributes.is_defined
     | None ->
-        Specs.summary_exists_in_models right_proc_name
+        Summary.has_model right_proc_name
 
 
 let resolve_method tenv class_name proc_name =
@@ -678,10 +678,10 @@ let resolve_java_pname tenv prop args pname_java call_flags : Typ.Procname.Java.
 (** Resolve the procedure name and run the analysis of the resolved procedure
     if not already analyzed *)
 let resolve_and_analyze tenv ~caller_pdesc prop args callee_proc_name call_flags
-    : Typ.Procname.t * Specs.summary option =
+    : Typ.Procname.t * Summary.t option =
   (* TODO (#15748878): Fix conflict with method overloading by encoding in the procedure name
      whether the method is defined or generated by the specialization *)
-  let analyze_ondemand resolved_pname : Specs.summary option =
+  let analyze_ondemand resolved_pname : Summary.t option =
     if Typ.Procname.equal resolved_pname callee_proc_name then
       Ondemand.analyze_proc_name ~caller_pdesc callee_proc_name
     else
@@ -1092,13 +1092,12 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
       let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
       Reporting.log_info_deprecated current_pname exn ;
       L.d_strln
-        (F.sprintf "Undefined function %s, returning undefined value."
+        (F.sprintf "Skipping function '%s': %s" (Typ.Procname.to_string callee_pname) reason) ;
-           (Typ.Procname.to_string callee_pname)) ;
+      ( match Summary.get current_pname with
-      ( match Specs.get_summary current_pname with
       | None ->
           ()
       | Some summary ->
-          let proc_name = Specs.get_proc_name summary in
+          let proc_name = Summary.get_proc_name summary in
           Tabulation.log_call_trace proc_name callee_pname ~reason loc Tabulation.CR_skip ) ;
       unknown_or_scan_call ~is_scan:false ~reason ret_typ ret_annots
         Builtin.
@@ -1200,7 +1199,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
                 proc_call exe_env resolved_summary
                   (call_args prop_ callee_pname norm_args ret_id_typ loc)
             | Some reason ->
-                let proc_attrs = Specs.get_attributes resolved_summary in
+                let proc_attrs = Summary.get_attributes resolved_summary in
                 let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
                 exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type
           )
@@ -1226,7 +1225,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
                   let handled_args = call_args norm_prop pname url_handled_args ret_id_typ loc in
                   proc_call exe_env callee_summary handled_args
               | Some reason ->
-                  let proc_attrs = Specs.get_attributes callee_summary in
+                  let proc_attrs = Summary.get_attributes callee_summary in
                   let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
                   exec_skip_call ~reason ret_annots proc_attrs.ProcAttributes.ret_type
           in
@@ -1285,7 +1284,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
                       match resolved_summary_opt with
                       | Some summ ->
                           let ret_annots, _ =
-                            (Specs.get_attributes summ).ProcAttributes.method_annotation
+                            (Summary.get_attributes summ).ProcAttributes.method_annotation
                           in
                           ret_annots
                       | None ->
@@ -1598,7 +1597,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots
     let callee_loc_opt =
       Option.map
         ~f:(fun attributes -> attributes.ProcAttributes.loc)
-        (Specs.proc_resolve_attributes callee_pname)
+        (Summary.proc_resolve_attributes callee_pname)
     in
     let skip_path = Paths.Path.add_skipped_call path callee_pname reason callee_loc_opt in
     [(prop_with_undef_attr, skip_path)]
@@ -1639,7 +1638,7 @@ and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos
 
 
 and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as builtin_args) =
-  match Specs.proc_resolve_attributes proc_name with
+  match Summary.proc_resolve_attributes proc_name with
   | None ->
       [(prop_, path)]
   | Some callee_attributes ->
@@ -1729,10 +1728,10 @@ and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ pdesc loc prop pa
 and proc_call exe_env callee_summary
     {Builtin.pdesc; tenv; prop_= pre; path; ret_id_typ; args= actual_pars; loc} =
   let caller_pname = Procdesc.get_proc_name pdesc in
-  let callee_attrs = Specs.get_attributes callee_summary in
+  let callee_attrs = Summary.get_attributes callee_summary in
-  let callee_pname = Specs.get_proc_name callee_summary in
+  let callee_pname = Summary.get_proc_name callee_summary in
   check_inherently_dangerous_function caller_pname callee_pname ;
-  let formal_types = List.map ~f:snd (Specs.get_formals callee_summary) in
+  let formal_types = List.map ~f:snd (Summary.get_formals callee_summary) in
   let rec comb actual_pars formal_types =
     match (actual_pars, formal_types) with
     | [], [] ->

infer/src/biabduction/SymExec.mli

@@ -26,7 +26,7 @@ val instrs :
 val diverge : Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list
 (** Symbolic execution of the divergent pure computation. *)
 
-val proc_call : Exe_env.t -> Specs.summary -> Builtin.t
+val proc_call : Exe_env.t -> Summary.t -> Builtin.t
 
 val unknown_or_scan_call : is_scan:bool -> reason:string -> Typ.t -> Annot.Item.t -> Builtin.t
 

infer/src/biabduction/SymExecBlocks.ml

@@ -49,7 +49,7 @@ let resolve_method_with_block_args_and_analyze ~caller_pdesc pname act_params =
   let pdesc_opt =
     match Ondemand.analyze_proc_name ~caller_pdesc pname with
     | Some summary ->
-        Some (Specs.get_proc_desc summary)
+        Some (Summary.get_proc_desc summary)
     | None ->
         Ondemand.get_proc_desc pname
   in

infer/src/biabduction/SymExecBlocks.mli

@@ -9,7 +9,7 @@
 
 val resolve_method_with_block_args_and_analyze :
   caller_pdesc:Procdesc.t -> Typ.Procname.t -> (Exp.t * Typ.t) list
-  -> (Specs.summary * (Exp.t * Typ.t) list) option
+  -> (Summary.t * (Exp.t * Typ.t) list) option
 (* [resolve_method_with_block_args_and_analyze caller_pdesc pname args]
   create a copy of the method pname if it is defined and it's called with
   the correct number of arguments, and some arguments are block closures.

infer/src/biabduction/Tabulation.ml

@@ -99,13 +99,14 @@ let log_call_trace caller_name callee_name ?reason loc res =
 (***************)
 
 let get_specs_from_payload summary =
-  Option.map summary.Specs.payload.biabduction ~f:(fun BiabductionSummary.({preposts}) -> preposts)
+  Option.map summary.Summary.payload.biabduction ~f:(fun BiabductionSummary.({preposts}) ->
+      preposts )
   |> BiabductionSummary.get_specs_from_preposts
 
 
 (** Return the current phase for the proc *)
 let get_phase summary =
-  Option.value_map summary.Specs.payload.biabduction ~default:BiabductionSummary.FOOTPRINT ~f:
+  Option.value_map summary.Summary.payload.biabduction ~default:BiabductionSummary.FOOTPRINT ~f:
     (fun BiabductionSummary.({phase}) -> phase )
 
 
@@ -144,12 +145,12 @@ let spec_rename_vars pname spec =
     after renaming their vars, and also return the parameters *)
 let spec_find_rename trace_call summary
     : (int * Prop.exposed BiabductionSummary.spec) list * Pvar.t list =
-  let proc_name = Specs.get_proc_name summary in
+  let proc_name = Summary.get_proc_name summary in
   try
     let count = ref 0 in
     let f spec = incr count ; (!count, spec_rename_vars proc_name spec) in
     let specs = get_specs_from_payload summary in
-    let formals = Specs.get_formals summary in
+    let formals = Summary.get_formals summary in
     if List.is_empty specs then (
       trace_call CR_not_found ;
       raise
@@ -817,7 +818,7 @@ let prop_set_exn tenv pname prop se_exn =
 
 (** Include a subtrace for a procedure call if the callee is not a model. *)
 let include_subtrace callee_pname =
-  match Specs.proc_resolve_attributes callee_pname with
+  match Summary.proc_resolve_attributes callee_pname with
   | Some attrs ->
       not attrs.ProcAttributes.is_model
       && SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file
@@ -1427,7 +1428,7 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re
 (** Execute the function call and return the list of results with return value *)
 let exe_function_call exe_env callee_summary tenv ret_id caller_pdesc callee_pname loc
     actual_params prop path =
-  let callee_attrs = Specs.get_attributes callee_summary in
+  let callee_attrs = Summary.get_attributes callee_summary in
   let caller_pname = Procdesc.get_proc_name caller_pdesc in
   let trace_call = log_call_trace caller_pname callee_pname loc in
   let spec_list, formal_params = spec_find_rename trace_call callee_summary in

infer/src/biabduction/Tabulation.mli

@@ -47,13 +47,13 @@ val lookup_custom_errors : 'a Prop.t -> string option
 (** search in prop contains an error state *)
 
 val exe_function_call :
-  Exe_env.t -> Specs.summary -> Tenv.t -> Ident.t -> Procdesc.t -> Typ.Procname.t -> Location.t
+  Exe_env.t -> Summary.t -> Tenv.t -> Ident.t -> Procdesc.t -> Typ.Procname.t -> Location.t
   -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t
   -> (Prop.normal Prop.t * Paths.Path.t) list
 (** Execute the function call and return the list of results with return value *)
 
-val get_phase : Specs.summary -> BiabductionSummary.phase
+val get_phase : Summary.t -> BiabductionSummary.phase
 (** Return the current phase for the proc *)
 
-val get_specs_from_payload : Specs.summary -> Prop.normal BiabductionSummary.spec list
+val get_specs_from_payload : Summary.t -> Prop.normal BiabductionSummary.spec list
 (** Get the specs from the payload of the summary. *)

infer/src/biabduction/interproc.ml

@@ -199,7 +199,7 @@ let do_meet_pre tenv pset =
 (** Find the preconditions in the current spec table,
     apply meet then join, and return the joined preconditions *)
 let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t list =
-  let proc_name = Specs.get_proc_name summary in
+  let proc_name = Summary.get_proc_name summary in
   let collect_do_abstract_one tenv prop =
     if !Config.footprint then Config.run_in_re_execution_mode (Abs.abstract_no_symop tenv) prop
     else Abs.abstract_no_symop tenv prop
@@ -397,10 +397,10 @@ let do_symbolic_execution exe_env proc_cfg handle_exn tenv (node: ProcCfg.Except
 
 let mark_visited summary node =
   let node_id = Procdesc.Node.get_id node in
-  let stats = summary.Specs.stats in
+  let stats = summary.Summary.stats in
   if !Config.footprint then
-    stats.Specs.nodes_visited_fp <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_fp
+    stats.Summary.nodes_visited_fp <- IntSet.add (node_id :> int) stats.Summary.nodes_visited_fp
-  else stats.Specs.nodes_visited_re <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_re
+  else stats.Summary.nodes_visited_re <- IntSet.add (node_id :> int) stats.Summary.nodes_visited_re
 
 
 let forward_tabulate exe_env tenv proc_cfg wl =
@@ -434,16 +434,12 @@ let forward_tabulate exe_env tenv proc_cfg wl =
   in
   let print_node_preamble curr_node session pathset_todo =
     let log_string proc_name =
-      let summary = Specs.get_summary_unsafe proc_name in
+      let summary = Summary.get_unsafe proc_name in
       let phase_string =
-        if
+        match Tabulation.get_phase summary with FOOTPRINT -> "FP" | RE_EXECUTION -> "RE"
-          BiabductionSummary.equal_phase (Tabulation.get_phase summary)
-            BiabductionSummary.FOOTPRINT
-        then "FP"
-        else "RE"
       in
-      let status = Specs.get_status summary in
+      let status = Summary.get_status summary in
-      F.sprintf "[%s:%s] %s" phase_string (Specs.string_of_status status)
+      F.sprintf "[%s:%s] %s" phase_string (Summary.string_of_status status)
         (Typ.Procname.to_string proc_name)
     in
     L.d_strln
@@ -509,10 +505,10 @@ let forward_tabulate exe_env tenv proc_cfg wl =
   in
   while not (Worklist.is_empty wl) do
     let curr_node = Worklist.remove wl in
-    let summary = Specs.get_summary_unsafe pname in
+    let summary = Summary.get_unsafe pname in
     mark_visited summary curr_node ;
     (* mark nodes visited in fp and re phases *)
-    let session = incr summary.Specs.sessions ; !(summary.Specs.sessions) in
+    let session = incr summary.Summary.sessions ; !(summary.Summary.sessions) in
     do_before_node session curr_node ;
     do_node_and_handle curr_node session
   done ;
@@ -827,9 +823,9 @@ type exe_phase =
     and [get_results ()] returns the results computed.
     This function is architected so that [get_results ()] can be called even after
     [go ()] was interrupted by and exception. *)
-let perform_analysis_phase exe_env tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exceptional.t)
+let perform_analysis_phase exe_env tenv (summary: Summary.t) (proc_cfg: ProcCfg.Exceptional.t)
     : exe_phase =
-  let pname = Specs.get_proc_name summary in
+  let pname = Summary.get_proc_name summary in
   let start_node = ProcCfg.Exceptional.start_node proc_cfg in
   let compute_footprint () : exe_phase =
     let go (wl: Worklist.t) () =
@@ -1005,9 +1001,9 @@ let is_unavoidable tenv pre =
     an error in that case, generating the trace that lead to the runtime exception if the method is
     called in the context { precondition } *)
 let report_runtime_exceptions tenv pdesc summary =
-  let pname = Specs.get_proc_name summary in
+  let pname = Summary.get_proc_name summary in
   let is_public_method =
-    PredSymb.equal_access (Specs.get_attributes summary).access PredSymb.Public
+    PredSymb.equal_access (Summary.get_attributes summary).access PredSymb.Public
   in
   let is_main =
     is_public_method
@@ -1037,11 +1033,11 @@ let report_runtime_exceptions tenv pdesc summary =
 
 
 let report_custom_errors tenv summary =
-  let pname = Specs.get_proc_name summary in
+  let pname = Summary.get_proc_name summary in
   let error_preconditions, all_post_error = custom_error_preconditions summary in
   let report (pre, custom_error) =
     if all_post_error || is_unavoidable tenv pre then
-      let loc = Specs.get_loc summary in
+      let loc = Summary.get_loc summary in
       let err_desc = Localise.desc_custom_error loc in
       let exn = Exceptions.Custom_error (custom_error, err_desc) in
       Reporting.log_error_deprecated pname exn
@@ -1125,11 +1121,11 @@ let update_specs tenv prev_summary phase (new_specs: BiabductionSummary.NormSpec
 let update_summary tenv prev_summary specs phase res =
   let normal_specs = List.map ~f:(BiabductionSummary.spec_normalize tenv) specs in
   let new_specs, _ = update_specs tenv prev_summary phase normal_specs in
-  let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in
+  let symops = prev_summary.Summary.stats.Summary.symops + SymOp.get_total () in
   let stats_failure =
-    match res with None -> prev_summary.Specs.stats.Specs.stats_failure | Some _ -> res
+    match res with None -> prev_summary.Summary.stats.Summary.stats_failure | Some _ -> res
   in
-  let stats = {prev_summary.Specs.stats with symops; stats_failure} in
+  let stats = {prev_summary.Summary.stats with symops; stats_failure} in
   let preposts =
     match phase with
     | BiabductionSummary.FOOTPRINT ->
@@ -1138,17 +1134,18 @@ let update_summary tenv prev_summary specs phase res =
         List.map ~f:(BiabductionSummary.NormSpec.erase_join_info_pre tenv) new_specs
   in
   let payload =
-    {prev_summary.Specs.payload with Specs.biabduction= Some BiabductionSummary.{preposts; phase}}
+    { prev_summary.Summary.payload with
+      Summary.biabduction= Some BiabductionSummary.{preposts; phase} }
   in
-  {prev_summary with Specs.stats; payload}
+  {prev_summary with Summary.stats; payload}
 
 
 (** Analyze the procedure and return the resulting summary. *)
-let analyze_proc exe_env tenv proc_cfg : Specs.summary =
+let analyze_proc exe_env tenv proc_cfg : Summary.t =
   let proc_desc = ProcCfg.Exceptional.proc_desc proc_cfg in
   let proc_name = Procdesc.get_proc_name proc_desc in
   reset_global_values proc_desc ;
-  let summary = Specs.get_summary_unsafe proc_name in
+  let summary = Summary.get_unsafe proc_name in
   let go, get_results = perform_analysis_phase exe_env tenv summary proc_cfg in
   let res = Timeout.exe_timeout go () in
   let specs, phase = get_results () in
@@ -1162,15 +1159,15 @@ let analyze_proc exe_env tenv proc_cfg : Specs.summary =
 
 (** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
 let transition_footprint_re_exe tenv proc_name joined_pres =
-  let summary = Specs.get_summary_unsafe proc_name in
+  let summary = Summary.get_unsafe proc_name in
   let summary' =
     if Config.only_footprint then
-      match summary.Specs.payload.biabduction with
+      match summary.Summary.payload.biabduction with
       | Some ({phase= FOOTPRINT} as biabduction) ->
           { summary with
-            Specs.payload=
+            Summary.payload=
               { summary.payload with
-                Specs.biabduction= Some {biabduction with BiabductionSummary.phase= RE_EXECUTION}
+                Summary.biabduction= Some {biabduction with BiabductionSummary.phase= RE_EXECUTION}
               } }
       | _ ->
           summary
@@ -1184,12 +1181,12 @@ let transition_footprint_re_exe tenv proc_name joined_pres =
           joined_pres
       in
       let payload =
-        { summary.Specs.payload with
+        { summary.Summary.payload with
           biabduction= Some BiabductionSummary.{preposts; phase= RE_EXECUTION} }
       in
-      {summary with Specs.payload}
+      {summary with Summary.payload}
   in
-  Specs.add_summary proc_name summary'
+  Summary.add proc_name summary'
 
 
 (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for
@@ -1223,7 +1220,7 @@ let perform_transition proc_cfg tenv proc_name =
     in
     transition_footprint_re_exe tenv proc_name joined_pres
   in
-  match Specs.get_summary proc_name with
+  match Summary.get proc_name with
   | Some summary when BiabductionSummary.equal_phase (Tabulation.get_phase summary) FOOTPRINT ->
       transition summary
   | _ ->
@@ -1235,11 +1232,11 @@ let analyze_procedure_aux exe_env tenv proc_desc =
   let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
   Preanal.do_preanalysis proc_desc tenv ;
   let summaryfp = Config.run_in_footprint_mode (analyze_proc exe_env tenv) proc_cfg in
-  Specs.add_summary proc_name summaryfp ;
+  Summary.add proc_name summaryfp ;
   perform_transition proc_cfg tenv proc_name ;
   let summaryre = Config.run_in_re_execution_mode (analyze_proc exe_env tenv) proc_cfg in
   let summary_compact =
-    match summaryre.Specs.payload.biabduction with
+    match summaryre.Summary.payload.biabduction with
     | Some BiabductionSummary.({preposts} as biabduction) when Config.save_compact_summaries ->
         let sharing_env = Sil.create_sharing_env () in
         let compact_preposts =
@@ -1253,16 +1250,16 @@ let analyze_procedure_aux exe_env tenv proc_desc =
     | _ ->
         summaryre
   in
-  Specs.add_summary proc_name summary_compact ;
+  Summary.add proc_name summary_compact ;
   summary_compact
 
 
-let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Specs.summary =
+let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Summary.t =
   (* make sure models have been registered *)
   BuiltinDefn.init () ;
   let proc_name = Procdesc.get_proc_name proc_desc in
-  Specs.add_summary proc_name summary ;
+  Summary.add proc_name summary ;
   ( try ignore (analyze_procedure_aux exe_env tenv proc_desc) with exn ->
       IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
       Reporting.log_error_deprecated proc_name exn ) ;
-  Specs.get_summary_unsafe proc_name
+  Summary.get_unsafe proc_name

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -21,14 +21,14 @@ module Sem = BufferOverrunSemantics
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = Dom.Summary.t
+  type t = Dom.Summary.t
 
-  let update_payload astate (summary: Specs.summary) =
+  let update_summary astate (summary: Summary.t) =
     {summary with payload= {summary.payload with buffer_overrun= Some astate}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.buffer_overrun
+  let of_summary (summary: Summary.t) = summary.payload.buffer_overrun
 end)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
@@ -252,7 +252,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let model_env = Models.mk_model_env callee_pname node_hash location tenv ~ret in
             exec model_env mem
         | None ->
-          match Summary.read_summary pdesc callee_pname with
+          match Payload.read_summary pdesc callee_pname with
           | Some summary ->
               let callee = Ondemand.get_proc_desc callee_pname in
               instantiate_mem tenv ret callee callee_pname params mem summary location
@@ -425,7 +425,7 @@ module Report = struct
 
   let instantiate_cond
       : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate
-        -> Summary.payload -> Location.t -> PO.ConditionSet.t =
+        -> Payload.t -> Location.t -> PO.ConditionSet.t =
    fun tenv caller_pname callee_pdesc params caller_mem summary location ->
     let callee_entry_mem = Dom.Summary.get_input summary in
     let callee_cond = Dom.Summary.get_cond_set summary in
@@ -454,7 +454,7 @@ module Report = struct
           let node_hash = CFG.hash node in
           check (Models.mk_model_env pname node_hash location tenv) mem cond_set
       | None ->
-        match Summary.read_summary pdesc callee_pname with
+        match Payload.read_summary pdesc callee_pname with
         | Some callee_summary ->
             let callee = Ondemand.get_proc_desc callee_pname in
             instantiate_cond tenv pname callee params mem callee_summary location
@@ -476,7 +476,7 @@ module Report = struct
 
 
   let check_instrs
-      : Specs.summary -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.node -> Sil.instr list
+      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.node -> Sil.instr list
         -> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t -> PO.ConditionSet.t =
    fun summary pdesc tenv cfg node instrs state cond_set ->
     match (state, instrs) with
@@ -498,8 +498,8 @@ module Report = struct
 
 
   let check_node
-      : Specs.summary -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map
+      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t
-        -> PO.ConditionSet.t -> CFG.node -> PO.ConditionSet.t =
+        -> CFG.node -> PO.ConditionSet.t =
    fun summary pdesc tenv cfg inv_map cond_set node ->
     match Analyzer.extract_state (CFG.id node) inv_map with
     | Some state ->
@@ -510,8 +510,7 @@ module Report = struct
 
 
   let check_proc
-      : Specs.summary -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map
+      : Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t =
-        -> PO.ConditionSet.t =
    fun summary pdesc tenv cfg inv_map ->
     CFG.nodes cfg
     |> List.fold ~f:(check_node summary pdesc tenv cfg inv_map) ~init:PO.ConditionSet.empty
@@ -545,7 +544,7 @@ module Report = struct
     List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev
 
 
-  let report_errors : Specs.summary -> Procdesc.t -> PO.ConditionSet.t -> PO.ConditionSet.t =
+  let report_errors : Summary.t -> Procdesc.t -> PO.ConditionSet.t -> PO.ConditionSet.t =
    fun summary pdesc cond_set ->
     let pname = Procdesc.get_proc_name pdesc in
     let report cond trace issue_type =
@@ -582,7 +581,7 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit =
     "@\n@[<v 2>Summary of %a:@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s
 
 
-let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Specs.summary =
+let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
  fun {proc_desc; tenv; summary} ->
   Preanal.do_preanalysis proc_desc tenv ;
   let pdata = ProcData.make_default proc_desc tenv in
@@ -600,12 +599,12 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
         ( if Config.bo_debug >= 1 then
             let proc_name = Procdesc.get_proc_name proc_desc in
             print_summary proc_name post ) ;
-        Summary.update_summary post summary
+        Payload.update_summary post summary
     | _ ->
         summary
   in
   (inv_map, summary)
 
 
-let checker : Callbacks.proc_callback_args -> Specs.summary =
+let checker : Callbacks.proc_callback_args -> Summary.t =
  fun args -> compute_invariant_map_and_check args |> snd

infer/src/bufferoverrun/bufferOverrunChecker.mli

@@ -11,12 +11,12 @@ open! IStd
 
 val checker : Callbacks.proc_callback_t
 
-module Summary : Summary.S with type payload = BufferOverrunDomain.Summary.t
+module Payload : SummaryPayload.S with type t = BufferOverrunDomain.Summary.t
 
 module CFG = ProcCfg.NormalOneInstrPerNode
 
 type invariant_map
 
-val compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Specs.summary
+val compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t
 
 val extract_pre : CFG.id -> invariant_map -> BufferOverrunDomain.Mem.t option

infer/src/checkers/BoundedCallTree.ml

@@ -19,15 +19,15 @@ module Domain = AbstractDomain.FiniteSet (Typ.Procname)
    always []. Instead, the expanded per-method summaries are directly stored
    in the output directory as JSON files and *only* for those methods that
    will be part of the final crashcontext.json. *)
-module SpecSummary = Summary.Make (struct
+module SpecPayload = SummaryPayload.Make (struct
-  type payload = Stacktree_j.stacktree
+  type t = Stacktree_j.stacktree
 
-  let update_payload frame (summary: Specs.summary) =
+  let update_summary frame (summary: Summary.t) =
-    let payload = {summary.payload with Specs.crashcontext_frame= Some frame} in
+    let payload = {summary.payload with Summary.crashcontext_frame= Some frame} in
     {summary with payload}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.crashcontext_frame
+  let of_summary (summary: Summary.t) = summary.payload.crashcontext_frame
 end)
 
 type extras_t = {get_proc_desc: Typ.Procname.t -> Procdesc.t option; stacktraces: Stacktrace.t list}
@@ -70,14 +70,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let callees =
       List.map
         ~f:(fun pn ->
-          match SpecSummary.read_summary pdesc pn with
+          match SpecPayload.read_summary pdesc pn with
           | None -> (
             match get_proc_desc pn with
             | None ->
                 stacktree_stub_of_procname pn
             (* This can happen when the callee is in the same cluster/ buck
                     target, but it hasn't been checked yet. So we need both the
-                    inter-target lookup (SpecSummary) and the intra-target
+                    inter-target lookup (SpecPayload) and the intra-target
                     lookup (using get_proc_desc). *)
             | Some callee_pdesc ->
                 stacktree_of_pdesc callee_pdesc "proc_start" )
@@ -174,7 +174,7 @@ let loaded_stacktraces =
       Some (List.map ~f:Stacktrace.of_json_file files)
 
 
-let checker {Callbacks.proc_desc; tenv; get_proc_desc; summary} : Specs.summary =
+let checker {Callbacks.proc_desc; tenv; get_proc_desc; summary} : Summary.t =
   ( match loaded_stacktraces with
   | None ->
       L.(die UserError)

infer/src/checkers/Litho.ml

@@ -11,14 +11,14 @@ open! IStd
 module F = Format
 module Domain = LithoDomain
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = Domain.astate
+  type t = Domain.astate
 
-  let update_payload astate (summary: Specs.summary) =
+  let update_summary astate (summary: Summary.t) =
     {summary with payload= {summary.payload with litho= Some astate}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.litho
+  let of_summary (summary: Summary.t) = summary.payload.litho
 end)
 
 module LithoFramework = struct
@@ -93,7 +93,7 @@ module GraphQLGetters = struct
       let exn =
         Exceptions.Checkers (IssueType.graphql_field_access, Localise.verbatim_desc message)
       in
-      let loc = Specs.get_loc summary in
+      let loc = Summary.get_loc summary in
       let ltr = [Errlog.make_trace_element 0 loc message []] in
       Reporting.log_error summary ~loc ~ltr exn
     in
@@ -179,7 +179,7 @@ module RequiredProps = struct
               ~f:(fun required_prop ->
                 if not (has_prop prop_set required_prop) then
                   report_missing_required_prop summary required_prop parent_typename
-                    (Specs.get_loc summary) )
+                    (Summary.get_loc summary) )
               required_props
         | _ ->
             () )
@@ -229,7 +229,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         , (HilExp.AccessExpression receiver_ae :: _ as actuals)
         , _
         , _ ) ->
-        let summary = Summary.read_summary proc_data.pdesc callee_procname in
+        let summary = Payload.read_summary proc_data.pdesc callee_procname in
         let receiver =
           Domain.LocalAccessPath.make (AccessExpression.to_access_path receiver_ae) caller_pname
         in
@@ -257,7 +257,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           (* treat it like a normal call *)
           apply_callee_summary summary caller_pname return_base actuals astate
     | Call (ret_id_typ, Direct callee_procname, actuals, _, _) ->
-        let summary = Summary.read_summary proc_data.pdesc callee_procname in
+        let summary = Payload.read_summary proc_data.pdesc callee_procname in
         apply_callee_summary summary caller_pname ret_id_typ actuals astate
     | Assign (lhs_ae, HilExp.AccessExpression rhs_ae, _)
       -> (
@@ -294,6 +294,6 @@ let checker {Callbacks.summary; proc_desc; tenv} =
         Domain.substitute ~f_sub astate
       in
       let payload = postprocess post (FormalMap.make proc_desc) in
-      Summary.update_summary payload summary
+      Payload.update_summary payload summary
   | None ->
       summary

infer/src/checkers/NullabilityCheck.ml

@@ -20,7 +20,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = Specs.summary
+  type extras = Summary.t
 
   let rec is_pointer_subtype tenv typ1 typ2 =
     match (typ1.Typ.desc, typ2.Typ.desc) with
@@ -43,7 +43,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           ~f:(fun attributes ->
             ProcAttributes.equal_clang_method_kind attributes.ProcAttributes.clang_method_kind
               ProcAttributes.CPP_INSTANCE )
-          (Specs.proc_resolve_attributes callee_pname)
+          (Summary.proc_resolve_attributes callee_pname)
 
 
   let is_objc_instance_method callee_pname =
@@ -51,7 +51,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       ~f:(fun attributes ->
         ProcAttributes.equal_clang_method_kind attributes.ProcAttributes.clang_method_kind
           ProcAttributes.OBJC_INSTANCE )
-      (Specs.proc_resolve_attributes callee_pname)
+      (Summary.proc_resolve_attributes callee_pname)
 
 
   let is_blacklisted_method : Typ.Procname.t -> bool =
@@ -88,7 +88,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           || in_footprint && IssueType.equal err_name IssueType.null_dereference
              && Location.equal loc report_location
              && Localise.error_desc_is_reportable_bucket err_desc )
-        (Specs.get_err_log summary) false
+        (Summary.get_err_log summary) false
 
 
   (* On Clang languages, the annotations like _Nullabe can be found on the declaration
@@ -98,7 +98,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let lookup_local_attributes = function
     | Typ.Procname.Java _ as pname ->
         (* Looking up the attribute according to the classpath *)
-        Specs.proc_resolve_attributes pname
+        Summary.proc_resolve_attributes pname
     | pname ->
         (* Looking up the attributes locally, i.e. either from the file of from the includes *)
         Option.map ~f:Procdesc.get_attributes (Ondemand.get_proc_desc pname)

infer/src/checkers/Ownership.ml

@@ -202,7 +202,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type extras = Specs.summary
+  type extras = Summary.t
 
   let is_aggregate (_, typ) =
     match typ.Typ.desc with

infer/src/checkers/SimpleChecker.ml

@@ -82,7 +82,7 @@ module Make (Spec : Spec) : S = struct
 
   module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
 
-  let checker {Callbacks.proc_desc; tenv; summary} : Specs.summary =
+  let checker {Callbacks.proc_desc; tenv; summary} : Summary.t =
     let proc_name = Procdesc.get_proc_name proc_desc in
     let nodes = Procdesc.get_nodes proc_desc in
     let do_reporting node_id state =

infer/src/checkers/Siof.ml

@@ -50,14 +50,14 @@ let is_modelled =
     Typ.Procname.get_qualifiers pname |> QualifiedCppName.Match.match_qualifiers models_matcher
 
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = SiofDomain.astate
+  type t = SiofDomain.astate
 
-  let update_payload astate (summary: Specs.summary) =
+  let update_summary astate (summary: Summary.t) =
     {summary with payload= {summary.payload with siof= Some astate}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.siof
+  let of_summary (summary: Summary.t) = summary.payload.siof
 end)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
@@ -68,7 +68,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   let is_compile_time_constructed pdesc pv =
     let init_pname = Pvar.get_initializer_pname pv in
-    match Option.bind init_pname ~f:(Summary.read_summary pdesc) with
+    match Option.bind init_pname ~f:(Payload.read_summary pdesc) with
     | Some (Bottom, _) ->
         (* we analyzed the initializer for this global and found that it doesn't require any runtime
            initialization so cannot participate in SIOF *)
@@ -145,7 +145,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         add_actuals_globals astate pdesc loc actuals_without_self
     | Call (_, Const (Cfun callee_pname), actuals, loc, _) ->
         let callee_astate =
-          match Summary.read_summary pdesc callee_pname with
+          match Payload.read_summary pdesc callee_pname with
           | Some (NonBottom trace, initialized_by_callee) ->
               let already_initialized = snd astate in
               let dangerous_accesses =
@@ -194,7 +194,7 @@ let is_foreign tu_opt v =
 
 let report_siof summary trace pdesc gname loc =
   let trace_of_pname pname =
-    match Summary.read_summary pdesc pname with
+    match Payload.read_summary pdesc pname with
     | Some (NonBottom summary, _) ->
         summary
     | _ ->
@@ -222,7 +222,7 @@ let report_siof summary trace pdesc gname loc =
   else List.iter ~f:report_one_path reportable_paths
 
 
-let siof_check pdesc gname (summary: Specs.summary) =
+let siof_check pdesc gname (summary: Summary.t) =
   match summary.payload.siof with
   | Some (NonBottom post, _) ->
       let attrs = Procdesc.get_attributes pdesc in
@@ -243,7 +243,7 @@ let siof_check pdesc gname (summary: Specs.summary) =
       ()
 
 
-let checker {Callbacks.proc_desc; tenv; summary; get_procs_in_file} : Specs.summary =
+let checker {Callbacks.proc_desc; tenv; summary; get_procs_in_file} : Summary.t =
   let pname = Procdesc.get_proc_name proc_desc in
   let standard_streams_initialized_in_tu =
     let includes_iostream tu =
@@ -278,11 +278,11 @@ let checker {Callbacks.proc_desc; tenv; summary; get_procs_in_file} : Specs.summ
           Typ.Procname.ObjC_Cpp.is_constexpr cpp_pname
       | _ ->
           false
-    then Summary.update_summary initial summary
+    then Payload.update_summary initial summary
     else
       match Analyzer.compute_post proc_data ~initial with
       | Some post ->
-          Summary.update_summary post summary
+          Payload.update_summary post summary
       | None ->
           summary
   in

infer/src/checkers/annotationReachability.ml

@@ -60,14 +60,14 @@ module Domain = struct
     match vstate with Bottom -> false | NonBottom vars -> TrackingVar.mem var vars
 end
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = AnnotReachabilityDomain.astate
+  type t = AnnotReachabilityDomain.astate
 
-  let update_payload annot_map (summary: Specs.summary) =
+  let update_summary annot_map (summary: Summary.t) =
     {summary with payload= {summary.payload with annot_map= Some annot_map}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.annot_map
+  let of_summary (summary: Summary.t) = summary.payload.annot_map
 end)
 
 let is_modeled_expensive tenv = function
@@ -100,7 +100,7 @@ let is_allocator tenv pname =
 
 let check_attributes check tenv pname =
   PatternMatch.check_class_attributes check tenv pname
-  || Annotations.pname_has_return_annot pname ~attrs_of_pname:Specs.proc_resolve_attributes check
+  || Annotations.pname_has_return_annot pname ~attrs_of_pname:Summary.proc_resolve_attributes check
 
 
 let method_overrides is_annotated tenv pname =
@@ -119,7 +119,7 @@ let method_overrides_annot annot tenv pname = method_overrides (method_has_annot
 
 let lookup_annotation_calls ~caller_pdesc annot pname =
   match Ondemand.analyze_proc_name ~caller_pdesc pname with
-  | Some {Specs.payload= {Specs.annot_map= Some annot_map}} -> (
+  | Some {Summary.payload= {Summary.annot_map= Some annot_map}} -> (
     try AnnotReachabilityDomain.find annot annot_map with Caml.Not_found ->
       AnnotReachabilityDomain.SinkMap.empty )
   | _ ->
@@ -135,7 +135,7 @@ let string_of_pname = Typ.Procname.to_simplified_string ~withclass:true
 
 let report_allocation_stack src_annot summary fst_call_loc trace stack_str constructor_pname
     call_loc =
-  let pname = Specs.get_proc_name summary in
+  let pname = Summary.get_proc_name summary in
   let final_trace = List.rev (update_trace call_loc trace) in
   let constr_str = string_of_pname constructor_pname in
   let description =
@@ -151,7 +151,7 @@ let report_allocation_stack src_annot summary fst_call_loc trace stack_str const
 
 
 let report_annotation_stack src_annot snk_annot src_summary loc trace stack_str snk_pname call_loc =
-  let src_pname = Specs.get_proc_name src_summary in
+  let src_pname = Summary.get_proc_name src_summary in
   if String.equal snk_annot dummy_constructor_annot then
     report_allocation_stack src_annot src_summary loc trace stack_str snk_pname call_loc
   else
@@ -176,7 +176,7 @@ let report_annotation_stack src_annot snk_annot src_summary loc trace stack_str
 let report_call_stack summary end_of_stack lookup_next_calls report call_site sink_map =
   (* TODO: stop using this; we can use the call site instead *)
   let lookup_location pname =
-    Option.value_map ~f:Specs.get_loc ~default:Location.dummy (Specs.get_summary pname)
+    Option.value_map ~f:Summary.get_loc ~default:Location.dummy (Summary.get pname)
   in
   let rec loop fst_call_loc visited_pnames (trace, stack_str) (callee_pname, call_loc) =
     if end_of_stack callee_pname then
@@ -405,7 +405,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   let merge_callee_map call_site pdesc callee_pname astate =
-    match Summary.read_summary pdesc callee_pname with
+    match Payload.read_summary pdesc callee_pname with
     | None ->
         astate
     | Some callee_call_map ->
@@ -444,12 +444,12 @@ end
 
 module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
 
-let checker ({Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary =
+let checker ({Callbacks.proc_desc; tenv; summary} as callback) : Summary.t =
   let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in
   let proc_data = ProcData.make_default proc_desc tenv in
   match Analyzer.compute_post proc_data ~initial with
   | Some (annot_map, _) ->
       List.iter annot_specs ~f:(fun (spec: AnnotationSpec.t) -> spec.report callback annot_map) ;
-      Summary.update_summary annot_map summary
+      Payload.update_summary annot_map summary
   | None ->
       summary

infer/src/checkers/annotations.ml

@@ -142,7 +142,7 @@ let pdesc_return_annot_ends_with pdesc annot =
   pdesc_has_return_annot pdesc (fun ia -> ia_ends_with ia annot)
 
 
-(* note: we would use Specs.proc_resolve_attributes directly instead of requiring [attrs_of_pname],
+(* note: we would use Summary.proc_resolve_attributes directly instead of requiring [attrs_of_pname],
    but doing so creates a circular dependency *)
 let pname_has_return_annot pname ~attrs_of_pname predicate =
   match attrs_of_pname pname with

infer/src/checkers/cost.ml

@@ -13,14 +13,14 @@ module L = Logging
 module BasicCost = CostDomain.BasicCost
 module NodesBasicCostDomain = CostDomain.NodeInstructionToCostMap
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = CostDomain.summary
+  type t = CostDomain.summary
 
-  let update_payload sum (summary: Specs.summary) =
+  let update_summary sum (summary: Summary.t) =
     {summary with payload= {summary.payload with cost= Some sum}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.cost
+  let of_summary (summary: Summary.t) = summary.payload.cost
 end)
 
 (* We use this treshold to give error if the cost is above it.
@@ -58,7 +58,7 @@ module TransferFunctionsNodesBasicCost = struct
           "Can't instantiate symbolic cost %a from call to %a (can't get procdesc)" BasicCost.pp
           callee_cost Typ.Procname.pp callee_pname
     | Some callee_pdesc ->
-      match BufferOverrunChecker.Summary.read_summary caller_pdesc callee_pname with
+      match BufferOverrunChecker.Payload.read_summary caller_pdesc callee_pname with
       | None ->
           L.(die InternalError)
             "Can't instantiate symbolic cost %a from call to %a (can't get summary)" BasicCost.pp
@@ -82,7 +82,7 @@ module TransferFunctionsNodesBasicCost = struct
       match instr with
       | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) ->
           let callee_cost =
-            match Summary.read_summary pdesc callee_pname with
+            match Payload.read_summary pdesc callee_pname with
             | Some {post= callee_cost} ->
                 if BasicCost.is_symbolic callee_cost then
                   instantiate_cost ~tenv ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem
@@ -448,7 +448,7 @@ module ReportedOnNodes = AbstractDomain.FiniteSetOfPPSet (Node.IdSet)
 type extras_TransferFunctionsWCET =
   { basic_cost_map: AnalyzerNodesBasicCost.invariant_map
   ; min_trees_map: BasicCost.astate Node.IdMap.t
-  ; summary: Specs.summary }
+  ; summary: Summary.t }
 
 (* Calculate the final Worst Case Execution Time predicted for each node.
    It uses the basic cost of the nodes (computed previously by AnalyzerNodesBasicCost)
@@ -568,7 +568,7 @@ let check_and_report_infinity cost proc_desc summary =
     Reporting.log_error ~loc summary exn
 
 
-let checker ({Callbacks.tenv; proc_desc} as callback_args) : Specs.summary =
+let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t =
   let inferbo_invariant_map, summary =
     BufferOverrunChecker.compute_invariant_map_and_check callback_args
   in
@@ -620,7 +620,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Specs.summary =
   | Some (exit_cost, _) ->
       L.internal_error "  PROCEDURE COST = %a @\n" BasicCost.pp exit_cost ;
       check_and_report_infinity exit_cost proc_desc summary ;
-      Summary.update_summary {post= exit_cost} summary
+      Payload.update_summary {post= exit_cost} summary
   | None ->
       if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (
         L.internal_error "Failed to compute final cost for function %a" Typ.Procname.pp

infer/src/checkers/fragmentRetainsViewChecker.ml

@@ -53,8 +53,8 @@ let callback_fragment_retains_view_java pname_java {Callbacks.proc_desc; summary
         ()
 
 
-let callback_fragment_retains_view ({Callbacks.summary} as args) : Specs.summary =
+let callback_fragment_retains_view ({Callbacks.summary} as args) : Summary.t =
-  let proc_name = Specs.get_proc_name summary in
+  let proc_name = Summary.get_proc_name summary in
   ( match proc_name with
   | Typ.Procname.Java pname_java ->
       callback_fragment_retains_view_java pname_java args

infer/src/checkers/liveness.ml

@@ -129,7 +129,7 @@ let get_captured_by_ref_invariant_map proc_desc proc_data =
   CapturedByRefAnalyzer.exec_cfg cfg proc_data ~initial:VarSet.empty ~debug:false
 
 
-let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
+let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
   let proc_data = ProcData.make_default proc_desc tenv in
   let captured_by_ref_invariant_map = get_captured_by_ref_invariant_map proc_desc proc_data in
   let cfg = CFG.from_pdesc proc_desc in

infer/src/checkers/printfArgs.ml

@@ -194,7 +194,7 @@ let check_printf_args_ok tenv (node: Procdesc.Node.t) (instr: Sil.instr)
       ()
 
 
-let callback_printf_args {Callbacks.tenv; proc_desc; summary} : Specs.summary =
+let callback_printf_args {Callbacks.tenv; proc_desc; summary} : Summary.t =
   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 summary)

infer/src/checkers/uninit.ml

@@ -18,14 +18,14 @@ module UninitVars = AbstractDomain.FiniteSet (AccessPath)
 module AliasedVars = AbstractDomain.FiniteSet (UninitDomain.VarPair)
 module RecordDomain = UninitDomain.Record (UninitVars) (AliasedVars) (D)
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = UninitDomain.summary
+  type t = UninitDomain.summary
 
-  let update_payload sum (summary: Specs.summary) =
+  let update_summary sum (summary: Summary.t) =
     {summary with payload= {summary.payload with uninit= Some sum}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.uninit
+  let of_summary (summary: Summary.t) = summary.payload.uninit
 end)
 
 let blacklisted_functions = [BuiltinDecl.__set_array_length]
@@ -57,7 +57,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     Reporting.log_error summary ~loc ~ltr exn
 
 
-  type extras = FormalMap.t * Specs.summary
+  type extras = FormalMap.t * Summary.t
 
   let is_struct t = match t.Typ.desc with Typ.Tstruct _ -> true | _ -> false
 
@@ -181,7 +181,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   let remove_initialized_params pdesc call acc idx (base, al) remove_fields =
-    match Summary.read_summary pdesc call with
+    match Payload.read_summary pdesc call with
     | Some {pre= initialized_formal_params; post= _} -> (
       match init_nth_actual_param call idx initialized_formal_params with
       | Some nth_formal ->
@@ -196,7 +196,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   (* true if a function initializes at least a param or a field of a struct param *)
   let function_initializes_some_formal_params pdesc call =
-    match Summary.read_summary pdesc call with
+    match Payload.read_summary pdesc call with
     | Some {pre= initialized_formal_params; post= _} ->
         not (D.is_empty initialized_formal_params)
     | _ ->
@@ -325,7 +325,7 @@ let get_locals cfg tenv pdesc =
     ~init:[] (Procdesc.get_locals cfg)
 
 
-let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
+let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
   let cfg = CFG.from_pdesc proc_desc in
   (* start with empty set of uninit local vars and  empty set of init formal params *)
   let formal_map = FormalMap.make proc_desc in
@@ -345,7 +345,7 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
   | Some
       ( {RecordDomain.uninit_vars= _; RecordDomain.aliased_vars= _; RecordDomain.prepost= pre, post}
       , _ ) ->
-      Summary.update_summary {pre; post} summary
+      Payload.update_summary {pre; post} summary
   | None ->
       if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (
         L.internal_error "Uninit analyzer failed to compute post for %a" Typ.Procname.pp

infer/src/clang/cFrontend_decl.ml

@@ -43,7 +43,7 @@ let protect ~f ~recover ~pp_context (trans_unit_ctx: CFrontend_config.translatio
 
 
 module CFrontend_decl_funct (T : CModule_type.CTranslation) : CModule_type.CFrontend = struct
-  let model_exists procname = Specs.summary_exists_in_models procname && not Config.models_mode
+  let model_exists procname = not Config.models_mode && Summary.has_model procname
 
   (** Translates the method/function's body into nodes of the cfg. *)
   let add_method ?(is_destructor_wrapper= false) trans_unit_ctx tenv cfg class_decl_opt procname

infer/src/concurrency/RacerD.ml

@@ -12,14 +12,14 @@ module F = Format
 module L = Logging
 module MF = MarkupFormatter
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = RacerDDomain.summary
+  type t = RacerDDomain.summary
 
-  let update_payload post (summary: Specs.summary) =
+  let update_summary post (summary: Summary.t) =
     {summary with payload= {summary.payload with racerd= Some post}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.racerd
+  let of_summary (summary: Summary.t) = summary.payload.racerd
 end)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
@@ -248,7 +248,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         make_container_access callee_pname ~is_write:false (get_receiver_ap actuals) callee_loc
           tenv caller_pdesc astate
     | None, _ ->
-        Summary.read_summary caller_pdesc callee_pname
+        Payload.read_summary caller_pdesc callee_pname
 
 
   let add_reads exps loc accesses locks threads ownership proc_data =
@@ -769,10 +769,10 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
             AttributeSetDomain.empty
         in
         let post = {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} in
-        Summary.update_summary post summary
+        Payload.update_summary post summary
     | None ->
         summary
-  else Summary.update_summary empty_post summary
+  else Payload.update_summary empty_post summary
 
 
 module AccessListMap = Caml.Map.Make (RacerDDomain.Access)
@@ -894,7 +894,7 @@ let desc_of_sink sink =
 let trace_of_pname orig_sink orig_pdesc callee_pname =
   let open RacerDDomain in
   let orig_access = PathDomain.Sink.kind orig_sink in
-  match Summary.read_summary orig_pdesc callee_pname with
+  match Payload.read_summary orig_pdesc callee_pname with
   | Some {accesses} ->
       AccessDomain.fold
         (fun snapshot acc ->
@@ -1502,7 +1502,7 @@ let make_results_table (module AccessListMap : QuotientedAccessListMap) file_env
       accesses acc
   in
   let aggregate_posts acc (tenv, proc_desc) =
-    match Summary.read_summary proc_desc (Procdesc.get_proc_name proc_desc) with
+    match Payload.read_summary proc_desc (Procdesc.get_proc_name proc_desc) with
     | Some summary ->
         aggregate_post summary tenv proc_desc acc
     | None ->

infer/src/concurrency/RacerDConfig.ml

@@ -310,7 +310,7 @@ module Models = struct
 
 
   let has_return_annot predicate pn =
-    Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes predicate
+    Annotations.pname_has_return_annot pn ~attrs_of_pname:Summary.proc_resolve_attributes predicate
 
 
   let is_functional pname =
@@ -521,7 +521,7 @@ module Models = struct
   let is_thread_safe_method pname tenv =
     PatternMatch.override_exists
       (fun pn ->
-        Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes
+        Annotations.pname_has_return_annot pn ~attrs_of_pname:Summary.proc_resolve_attributes
           is_thread_safe )
       tenv pname
 

infer/src/concurrency/starvation.ml

@@ -16,14 +16,14 @@ let is_on_main_thread pn =
   RacerDConfig.(match Models.get_thread pn with Models.MainThread -> true | _ -> false)
 
 
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = StarvationDomain.summary
+  type t = StarvationDomain.summary
 
-  let update_payload post (summary: Specs.summary) =
+  let update_summary post (summary: Summary.t) =
     {summary with payload= {summary.payload with starvation= Some post}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.starvation
+  let of_summary (summary: Summary.t) = summary.payload.starvation
 end)
 
 (* using an indentifier for a class object, create an access path representing that lock;
@@ -76,7 +76,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | NoEffect when is_on_main_thread callee ->
           Domain.set_on_main_thread astate
       | _ ->
-          Summary.read_summary pdesc callee
+          Payload.read_summary pdesc callee
           |> Option.value_map ~default:astate ~f:(Domain.integrate_summary astate callee loc) )
     | _ ->
         astate
@@ -123,7 +123,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
   Analyzer.compute_post proc_data ~initial
   |> Option.value_map ~default:summary ~f:(fun lock_state ->
          let lock_order = StarvationDomain.to_summary lock_state in
-         Summary.update_summary lock_order summary )
+         Payload.update_summary lock_order summary )
 
 
 let make_trace_with_header ?(header= "") elem start_loc pname =
@@ -144,7 +144,7 @@ let get_summaries_of_methods_in_class get_proc_desc tenv current_pdesc clazz =
   in
   let pdescs = List.rev_filter_map methods ~f:get_proc_desc in
   let get_summary callee_pdesc =
-    Summary.read_summary current_pdesc (Procdesc.get_proc_name callee_pdesc)
+    Payload.read_summary current_pdesc (Procdesc.get_proc_name callee_pdesc)
     |> Option.map ~f:(fun summary -> (callee_pdesc, summary))
   in
   List.rev_filter_map pdescs ~f:get_summary
@@ -307,7 +307,7 @@ let report_blocks_on_main_thread get_proc_desc tenv current_pdesc summary =
 let reporting {Callbacks.procedures; get_proc_desc; exe_env} =
   let report_procedure (tenv, proc_desc) =
     die_if_not_java proc_desc ;
-    Summary.read_summary proc_desc (Procdesc.get_proc_name proc_desc)
+    Payload.read_summary proc_desc (Procdesc.get_proc_name proc_desc)
     |> Option.iter ~f:(fun ((s, main) as summary) ->
            report_deadlocks get_proc_desc tenv proc_desc summary ;
            if main then report_blocks_on_main_thread get_proc_desc tenv proc_desc s )

infer/src/eradicate/eradicate.ml

@@ -33,20 +33,21 @@ module type ExtensionT = sig
 
   val ext : extension TypeState.ext
 
-  val update_payload : extension TypeState.t option -> Specs.payload -> Specs.payload
+  val update_payload : extension TypeState.t option -> Summary.payload -> Summary.payload
 end
 
 (** Create a module with the toplevel callback. *)
 module MkCallback (Extension : ExtensionT) : CallBackT = struct
   (** Update the summary with stats from the checker. *)
   let update_summary proc_name final_typestate_opt =
-    match Specs.get_summary proc_name with
+    match Summary.get proc_name with
     | Some old_summ ->
         let new_summ =
           { old_summ with
-            Specs.payload= Extension.update_payload final_typestate_opt old_summ.Specs.payload }
+            Summary.payload= Extension.update_payload final_typestate_opt old_summ.Summary.payload
+          }
         in
-        Specs.add_summary proc_name new_summ
+        Summary.add proc_name new_summ
     | None ->
         ()
 
@@ -140,7 +141,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
       {Callbacks.proc_desc= curr_pdesc; summary; get_proc_desc; tenv; get_procs_in_file}
       annotated_signature linereader proc_loc : unit =
     let idenv = Idenv.create curr_pdesc in
-    let curr_pname = Specs.get_proc_name summary in
+    let curr_pname = Summary.get_proc_name summary in
     let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in
     let find_canonical_duplicate node =
       let duplicate_nodes = find_duplicate_nodes node in
@@ -192,7 +193,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
               is_private && same_class
             in
             let private_called =
-              PatternMatch.proc_calls Specs.proc_resolve_attributes init_pd filter
+              PatternMatch.proc_calls Summary.proc_resolve_attributes init_pd filter
             in
             let do_called (callee_pn, _) =
               match get_proc_desc callee_pn with
@@ -241,7 +242,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
       let pname_and_pdescs_with f =
         let res = ref [] in
         let filter pname =
-          match Specs.proc_resolve_attributes pname with
+          match Summary.proc_resolve_attributes pname with
           | Some proc_attributes ->
               f (pname, proc_attributes)
           | None ->
@@ -326,7 +327,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
 
 
   (** Entry point for the eradicate-based checker infrastructure. *)
-  let callback checks ({Callbacks.proc_desc; summary} as callback_args) : Specs.summary =
+  let callback checks ({Callbacks.proc_desc; summary} as callback_args) : Summary.t =
     let proc_name = Procdesc.get_proc_name proc_desc in
     let calls_this = ref false in
     let filter_special_cases () =
@@ -336,11 +337,11 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
             Typ.Procname.Java.is_access_method java_pname
         | _ ->
             false )
-        || (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.is_bridge_method
+        || (Summary.pdesc_resolve_attributes proc_desc).ProcAttributes.is_bridge_method
       then None
       else
         let annotated_signature =
-          Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes proc_desc)
+          Models.get_modelled_annotated_signature (Summary.pdesc_resolve_attributes proc_desc)
         in
         Some annotated_signature
     in
@@ -378,7 +379,7 @@ module EmptyExtension : ExtensionT = struct
     {TypeState.empty; check_instr; join; pp}
 
 
-  let update_payload typestate_opt payload = {payload with Specs.typestate= typestate_opt}
+  let update_payload typestate_opt payload = {payload with Summary.typestate= typestate_opt}
 end
 
 module Main = Build (EmptyExtension)

infer/src/eradicate/eradicate.mli

@@ -27,5 +27,5 @@ module type ExtensionT = sig
 
   val ext : extension TypeState.ext
 
-  val update_payload : extension TypeState.t option -> Specs.payload -> Specs.payload
+  val update_payload : extension TypeState.t option -> Summary.payload -> Summary.payload
 end

infer/src/eradicate/eradicateChecks.ml

@@ -47,7 +47,7 @@ let classify_procedure proc_attributes =
   let unique_id = Typ.Procname.to_unique_id pn in
   let classification =
     if Models.is_modelled_nullable pn then "M" (* modelled *)
-    else if Specs.proc_is_library proc_attributes then "L" (* library *)
+    else if Summary.proc_is_library proc_attributes then "L" (* library *)
     else if not proc_attributes.ProcAttributes.is_defined then "S" (* skip *)
     else if String.is_prefix ~prefix:"com.facebook" unique_id then "F" (* FB *)
     else "?"
@@ -473,7 +473,7 @@ let check_overridden_annotations find_canonical_duplicate tenv proc_name proc_de
       ignore (List.fold2_exn ~f:compare ~init:initial_pos current_params overridden_params)
   in
   let check overriden_proc_name =
-    match Specs.proc_resolve_attributes overriden_proc_name with
+    match Summary.proc_resolve_attributes overriden_proc_name with
     | Some attributes ->
         let overridden_signature = Models.get_modelled_annotated_signature attributes in
         check_return overriden_proc_name overridden_signature ;

infer/src/eradicate/typeCheck.ml

@@ -44,7 +44,7 @@ module ComplexExpressions = struct
   let procname_instanceof = Typ.Procname.equal BuiltinDecl.__instanceof
 
   let procname_is_false_on_null pn =
-    match Specs.proc_resolve_attributes pn with
+    match Summary.proc_resolve_attributes pn with
     | Some proc_attributes ->
         let annotated_signature = Models.get_modelled_annotated_signature proc_attributes in
         let ret_ann, _ = annotated_signature.AnnotatedSignature.ret in
@@ -55,7 +55,7 @@ module ComplexExpressions = struct
 
   let procname_is_true_on_null pn =
     let annotated_true_on_null () =
-      match Specs.proc_resolve_attributes pn with
+      match Summary.proc_resolve_attributes pn with
       | Some proc_attributes ->
           let annotated_signature = Models.get_modelled_annotated_signature proc_attributes in
           let ret_ann, _ = annotated_signature.AnnotatedSignature.ret in
@@ -533,8 +533,8 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get
       let callee_attributes =
         let proc_attriutes_opt =
           Option.value_map
-            ~default:(Specs.proc_resolve_attributes callee_pname)
+            ~default:(Summary.proc_resolve_attributes callee_pname)
-            ~f:(fun summary -> Some (Specs.get_attributes summary))
+            ~f:(fun summary -> Some (Summary.get_attributes summary))
             callee_summary_opt
         in
         match proc_attriutes_opt with
@@ -788,7 +788,7 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get
         in
         let resolved_ret_ =
           let ret_ia, ret_typ = annotated_signature.AnnotatedSignature.ret in
-          let is_library = Specs.proc_is_library callee_attributes in
+          let is_library = Summary.proc_is_library callee_attributes in
           let origin =
             TypeOrigin.Proc {TypeOrigin.pname= callee_pname; loc; annotated_signature; is_library}
           in
@@ -1085,7 +1085,7 @@ let typecheck_node tenv ext calls_this checks idenv get_proc_desc curr_pname cur
       when Models.is_noreturn callee_pname ->
         noreturn := true
     | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), _, _, _) ->
-        let callee_attributes_opt = Specs.proc_resolve_attributes callee_pname in
+        let callee_attributes_opt = Summary.proc_resolve_attributes callee_pname in
         (* check if the call might throw an exception *)
         let has_exceptions =
           match callee_attributes_opt with

infer/src/labs/ResourceLeaks.ml

@@ -13,14 +13,14 @@ module L = Logging
 module Domain = ResourceLeakDomain
 
 (* Boilerplate to write/read our summaries alongside the summaries of other analyzers *)
-module Summary = Summary.Make (struct
+module Payload = SummaryPayload.Make (struct
-  type payload = Domain.astate
+  type t = Domain.astate
 
-  let update_payload resources_payload (summary: Specs.summary) =
+  let update_summary resources_payload (summary: Summary.t) =
     {summary with payload= {summary.payload with resources= Some resources_payload}}
 
 
-  let read_payload (summary: Specs.summary) = summary.payload.resources
+  let of_summary (summary: Summary.t) = summary.payload.resources
 end)
 
 type extras = FormalMap.t
@@ -70,7 +70,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           else if releases_resource callee_procname tenv then astate - 1 (* 2(a) *)
           else astate
         in
-        match Summary.read_summary pdesc callee_procname with
+        match Payload.read_summary pdesc callee_procname with
         | Some _summary ->
             (* Looked up the summary for callee_procname... do something with it *)
             (* 4(a) *)
@@ -103,7 +103,7 @@ module Analyzer =
     (TransferFunctions)
 
 (* Callback for invoking the checker from the outside--registered in RegisterCheckers *)
-let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary =
+let checker {Callbacks.summary; proc_desc; tenv} : Summary.t =
   (* Report an error when we have acquired more resources than we have released *)
   let report leak_count (proc_data: extras ProcData.t) =
     if leak_count > 0 (* 2(a) *) then
@@ -123,7 +123,7 @@ let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary =
   | Some post ->
       (* 1(f) *)
       report post proc_data ;
-      Summary.update_summary (convert_to_summary post) summary
+      Payload.update_summary (convert_to_summary post) summary
   | None ->
       L.(die InternalError)
         "Analyzer failed to compute post for %a" Typ.Procname.pp

infer/src/quandary/TaintAnalysis.ml

@@ -16,19 +16,19 @@ module Make (TaintSpecification : TaintSpec.S) = struct
   module TraceDomain = TaintSpecification.Trace
   module TaintDomain = TaintSpecification.AccessTree
 
-  module Summary = Summary.Make (struct
+  module Payload = SummaryPayload.Make (struct
-    type payload = QuandarySummary.t
+    type t = QuandarySummary.t
 
-    let update_payload quandary_payload (summary: Specs.summary) =
+    let update_summary quandary_payload (summary: Summary.t) =
       {summary with payload= {summary.payload with quandary= Some quandary_payload}}
 
 
-    let read_payload (summary: Specs.summary) = summary.payload.quandary
+    let of_summary (summary: Summary.t) = summary.payload.quandary
   end)
 
   module Domain = TaintDomain
 
-  type extras = {formal_map: FormalMap.t; summary: Specs.summary}
+  type extras = {formal_map: FormalMap.t; summary: Summary.t}
 
   module TransferFunctions (CFG : ProcCfg.S) = struct
     module CFG = CFG
@@ -137,7 +137,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           (* read_summary will trigger ondemand analysis of the current proc. we don't want that. *)
           TaintDomain.empty
         else
-          match Summary.read_summary proc_data.pdesc pname with
+          match Payload.read_summary proc_data.pdesc pname with
           | Some summary ->
               TaintSpecification.of_summary_access_tree summary
           | None ->
@@ -695,7 +695,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                 (* don't use a summary for a procedure that is a direct source *)
                 astate_with_source
               else
-                match Summary.read_summary proc_data.pdesc callee_pname with
+                match Payload.read_summary proc_data.pdesc callee_pname with
                 | None ->
                     handle_unknown_call callee_pname astate_with_source
                 | Some summary ->
@@ -862,7 +862,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     TaintSpecification.to_summary_access_tree with_footprint_vars
 
 
-  let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
+  let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
     (* bind parameters to a trace with a tainted source (if applicable) *)
     let make_initial pdesc =
       let pname = Procdesc.get_proc_name pdesc in
@@ -887,7 +887,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     let proc_data = ProcData.make proc_desc tenv extras in
     match Analyzer.compute_post proc_data ~initial with
     | Some access_tree ->
-        Summary.update_summary (make_summary proc_data access_tree) summary
+        Payload.update_summary (make_summary proc_data access_tree) summary
     | None ->
         if Procdesc.Node.get_succs (Procdesc.get_start_node proc_desc) <> [] then (
           L.internal_error "Couldn't compute post for %a. Broken CFG suspected" Typ.Procname.pp

infer/src/unit/TaintTests.ml

@@ -160,7 +160,7 @@ let tests =
     ; ( "sink without source not tracked"
       , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ]
     |> TestInterpreter.create_tests ~pp_opt:pp_sparse
-         {formal_map= FormalMap.empty; summary= Specs.dummy}
+         {formal_map= FormalMap.empty; summary= Summary.dummy}
          ~initial:(MockTaintAnalysis.Domain.empty, IdAccessPathMapDomain.empty)
   in
   "taint_test_suite" >::: test_list