biabduction is an InterproceduralAnalysis.t

Summary:
This shows how the strategy for making each analysis its own library
looks like. Starting with biabduction since it's one of the worst ones.

A checker cannot depend on ProcData (in its current form) as it contains
a Summary.t. We don't want to change all the analyzers at once so let's
make up a new type. The new type also contains callbacks for Ondemand
since a checker that is its own dune library cannot call Ondemand
directly either (because Ondemand needs Summary.OnDisk).

Once all checkers are migrated we should be able to reclaim the
callbacks set up by callbacks.ml in exchange for these new callbacks,
therefore achieving a neutral callback karma.

Reviewed By: dulmarod, skcho

Differential Revision: D21261638

fbshipit-source-id: fa91ca50f

infer/src/absint/AnalysisCallbacks.ml

@@ -9,7 +9,8 @@ open! IStd
 module L = Logging
 
 type callbacks =
-  { html_debug_new_node_session_f:
+  { get_proc_desc_f: Procname.t -> Procdesc.t option
+  ; html_debug_new_node_session_f:
       'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
       -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
   ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option }
@@ -26,6 +27,8 @@ let get_callbacks () =
       L.die InternalError "Callbacks not set"
 
 
+let get_proc_desc proc_name = (get_callbacks ()).get_proc_desc_f proc_name
+
 let html_debug_new_node_session ?kind ~pp_name node ~f =
   (get_callbacks ()).html_debug_new_node_session_f ?kind ~pp_name node ~f
 

infer/src/absint/AnalysisCallbacks.mli

@@ -9,16 +9,19 @@ open! IStd
 
 (** {2 Analysis API} *)
 
+val get_proc_desc : Procname.t -> Procdesc.t option
+(** set to [Ondemand.get_proc_desc] *)
+
 val html_debug_new_node_session :
      ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
   -> pp_name:(Format.formatter -> unit)
   -> Procdesc.Node.t
   -> f:(unit -> 'a)
   -> 'a
-(** set to {!NodePrinter.with_session} *)
+(** set to [NodePrinter.with_session] *)
 
 val proc_resolve_attributes : Procname.t -> ProcAttributes.t option
-(** set to {!Summary.OnDisk.proc_resolve_attributes} *)
+(** set to [Summary.OnDisk.proc_resolve_attributes] *)
 
 (** {2 Callbacks management}*)
 
@@ -26,7 +29,8 @@ val proc_resolve_attributes : Procname.t -> ProcAttributes.t option
     put here functions needed for the analysis that depend on modules higher up the dependency graph
     than this library but whose type does not. *)
 type callbacks =
-  { html_debug_new_node_session_f:
+  { get_proc_desc_f: Procname.t -> Procdesc.t option
+  ; html_debug_new_node_session_f:
       'a.    ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
       -> pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
   ; proc_resolve_attributes_f: Procname.t -> ProcAttributes.t option }

infer/src/absint/InterproceduralAnalysis.ml

@@ -0,0 +1,17 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+type 'payload t =
+  { proc_desc: Procdesc.t
+  ; tenv: Tenv.t
+  ; err_log: Errlog.t
+  ; exe_env: Exe_env.t
+  ; analyze_dependency: Procname.t -> (Procdesc.t * 'payload) option
+  ; analyze_pdesc_dependency: Procdesc.t -> 'payload option
+  ; update_stats: ?add_symops:int -> ?failure_kind:SymOp.failure_kind -> unit -> unit }

infer/src/absint/InterproceduralAnalysis.mli

@@ -0,0 +1,26 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** Analysis data for interprocedural analysis. This is the data for one procedure under analysis,
+    and callbacks to analyze dependencies of it as well as do bookkeeping regarding the current
+    procedure. Basically anything that needs to access the [Summary.t] of the current procedure
+    should go here. *)
+type 'payload t =
+  { proc_desc: Procdesc.t  (** the procedure to analyze *)
+  ; tenv: Tenv.t  (** {!Tenv.t} corresponding to the current procedure *)
+  ; err_log: Errlog.t
+        (** the issue log for the current procedure (internally a mutable data structure) *)
+  ; exe_env: Exe_env.t  (** {!Exe_env.t} for the current analysis *)
+  ; analyze_dependency: Procname.t -> (Procdesc.t * 'payload) option
+        (** On-demand analysis of callees or other dependencies of the analysis of the current
+            procedure. Uses [Ondemand.analyze_procedure]. *)
+  ; analyze_pdesc_dependency: Procdesc.t -> 'payload option
+        (** same as above when we already know the {!Procdesc.t} *)
+  ; update_stats: ?add_symops:int -> ?failure_kind:SymOp.failure_kind -> unit -> unit
+        (** update the [Summary.Stats.t] of the summary of the current procedure *) }

infer/src/backend/Summary.mli

@@ -27,8 +27,6 @@ module Status : sig
   type t
 
   val is_analyzed : t -> bool
-
-  val to_string : t -> string
 end
 
 (** summary of a procedure name *)
@@ -53,9 +51,6 @@ val get_proc_desc : t -> Procdesc.t
 val get_attributes : t -> ProcAttributes.t
 (** Get the attributes of the procedure. *)
 
-val get_formals : t -> (Mangled.t * Typ.t) list
-(** Get the formal parameters of the procedure *)
-
 val get_err_log : t -> Errlog.t
 
 val get_loc : t -> Location.t

infer/src/backend/SummaryReporting.ml

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module L = Logging
 
 type log_t = Reporting.log_t
 
@@ -24,3 +25,18 @@ let log_warning summary ~loc ?ltr ?extras issue_type error_message =
 let log_error_using_state summary exn =
   BiabductionReporting.log_error_using_state (Summary.get_proc_desc summary)
     (Summary.get_err_log summary) exn
+
+
+let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn =
+  if !BiabductionConfig.footprint then
+    match Summary.OnDisk.get proc_name with
+    | Some summary ->
+        let proc_attributes = Summary.get_attributes summary in
+        let err_log = Summary.get_err_log summary in
+        BiabductionReporting.log_issue_deprecated_using_state proc_attributes err_log severity ?node
+          ?loc ?ltr exn
+    | None ->
+        L.(die InternalError)
+          "Trying to report error on procedure %a, but cannot because no summary exists for this \
+           procedure. Did you mean to log the error on the caller of %a instead?"
+          Procname.pp proc_name Procname.pp proc_name

infer/src/backend/SummaryReporting.mli

@@ -19,3 +19,14 @@ val log_warning : Summary.t -> loc:Location.t -> log_t
 
 val log_error_using_state : Summary.t -> exn -> unit
 (** Add an error to the given summary using biabduction state (DO NOT USE ELSEWHERE). *)
+
+val log_issue_deprecated_using_state :
+     Exceptions.severity
+  -> Procname.t
+  -> ?node:Procdesc.Node.t
+  -> ?loc:Location.t
+  -> ?ltr:Errlog.loc_trace
+  -> exn
+  -> unit
+(** Report an issue in the given procedure using biabduction state. DEPRECATED as it can create race
+    conditions between checkers. Use log_error_using_state instead *)

infer/src/biabduction/Abs.ml

@@ -1138,7 +1138,7 @@ let check_junk pname tenv prop =
             let report_leak () =
               if not report_and_continue then raise exn
               else (
-                BiabductionReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
+                SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
                 leaks_reported := alloc_attribute :: !leaks_reported )
             in
             if not ignore_leak then report_leak () ;

infer/src/biabduction/BiabductionReporting.ml

@@ -6,26 +6,17 @@
  *)
 
 open! IStd
-module L = Logging
 
-let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn =
+let log_issue_deprecated_using_state proc_attributes err_log severity ?node ?loc ?ltr exn =
   if !BiabductionConfig.footprint then
-    match Summary.OnDisk.get proc_name with
+    let node =
-    | Some summary ->
+      let node = match node with None -> AnalysisState.get_node_exn () | Some node -> node in
-        let node =
+      Errlog.BackendNode {node}
-          let node = match node with None -> AnalysisState.get_node_exn () | Some node -> node in
+    in
-          Errlog.BackendNode {node}
+    let session = AnalysisState.get_session () in
-        in
+    let loc = match loc with None -> AnalysisState.get_loc_exn () | Some loc -> loc in
-        let session = AnalysisState.get_session () in
+    let ltr = match ltr with None -> State.get_loc_trace () | Some ltr -> ltr in
-        let loc = match loc with None -> AnalysisState.get_loc_exn () | Some loc -> loc in
+    Reporting.log_issue_from_summary severity proc_attributes err_log ~node ~session ~loc ~ltr exn
-        let ltr = match ltr with None -> State.get_loc_trace () | Some ltr -> ltr in
-        Reporting.log_issue_from_summary severity (Summary.get_attributes summary)
-          summary.Summary.err_log ~node ~session ~loc ~ltr exn
-    | None ->
-        L.(die InternalError)
-          "Trying to report error on procedure %a, but cannot because no summary exists for this \
-           procedure. Did you mean to log the error on the caller of %a instead?"
-          Procname.pp proc_name Procname.pp proc_name
 
 
 let log_error_using_state proc_desc err_log exn =

infer/src/biabduction/BiabductionReporting.mli

@@ -11,8 +11,9 @@ val log_error_using_state : Procdesc.t -> Errlog.t -> exn -> unit
 (** Add an error to the given summary using biabduction state. *)
 
 val log_issue_deprecated_using_state :
-     Exceptions.severity
+     ProcAttributes.t
-  -> Procname.t
+  -> Errlog.t
+  -> Exceptions.severity
   -> ?node:Procdesc.Node.t
   -> ?loc:Location.t
   -> ?ltr:Errlog.loc_trace

infer/src/biabduction/BiabductionSummary.ml

@@ -295,6 +295,8 @@ type t = {preposts: NormSpec.t list; phase: phase}
 
 let opt_get_phase = function None -> FOOTPRINT | Some {phase} -> phase
 
+let get_specs {preposts} = get_specs_from_preposts (Some preposts)
+
 let pp pe fmt {preposts; phase} =
   F.fprintf fmt "phase= %s@\n%a" (string_of_phase phase) (pp_specs pe)
     (List.map ~f:NormSpec.tospec preposts)

infer/src/biabduction/BiabductionSummary.mli

@@ -81,10 +81,10 @@ val equal_phase : phase -> phase -> bool
 
 val string_of_phase_short : phase -> string
 
-val get_specs_from_preposts : NormSpec.t list option -> Prop.normal spec list
-
 type t = {preposts: NormSpec.t list; phase: phase}
 
+val get_specs : t -> Prop.normal spec list
+
 val opt_get_phase : t option -> phase
 
 val pp : Pp.env -> Format.formatter -> t -> unit

infer/src/biabduction/Builtin.ml

@@ -11,16 +11,14 @@ module L = Logging
 (** Module for builtin functions with their symbolic execution handler *)
 
 type args =
-  { summary: Summary.t
+  { instr: Sil.instr
-  ; instr: Sil.instr
-  ; tenv: Tenv.t
   ; prop_: Prop.normal Prop.t
   ; path: Paths.Path.t
   ; ret_id_typ: Ident.t * Typ.t
   ; args: (Exp.t * Typ.t) list
   ; proc_name: Procname.t
   ; loc: Location.t
-  ; exe_env: Exe_env.t }
+  ; analysis_data: BiabductionSummary.t InterproceduralAnalysis.t }
 
 type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
 

infer/src/biabduction/Builtin.mli

@@ -10,16 +10,14 @@ open! IStd
 (** Module for builtin functions with their symbolic execution handler *)
 
 type args =
-  { summary: Summary.t
+  { instr: Sil.instr
-  ; instr: Sil.instr
-  ; tenv: Tenv.t
   ; prop_: Prop.normal Prop.t
   ; path: Paths.Path.t
   ; ret_id_typ: Ident.t * Typ.t
   ; args: (Exp.t * Typ.t) list
   ; proc_name: Procname.t
   ; loc: Location.t
-  ; exe_env: Exe_env.t }
+  ; analysis_data: BiabductionSummary.t InterproceduralAnalysis.t }
 
 type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
 

infer/src/biabduction/BuiltinDefn.ml

@@ -15,12 +15,11 @@ module L = Logging
 type t = Builtin.registered
 
 (** model va_arg as always returning 0 *)
-let execute___builtin_va_arg {Builtin.summary; tenv; prop_; path; args; loc; exe_env} :
+let execute___builtin_va_arg {Builtin.analysis_data; prop_; path; args; loc} : Builtin.ret_typ =
-    Builtin.ret_typ =
   match args with
   | [(lexp3, typ3)] ->
       let instr' = Sil.Store {e1= lexp3; root_typ= typ3; typ= typ3; e2= Exp.zero; loc} in
-      SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton instr') [(prop_, path)]
+      SymExec.instrs ~mask_errors:true analysis_data (Instrs.singleton instr') [(prop_, path)]
   | _ ->
       raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -86,11 +85,11 @@ let add_array_to_prop tenv pdesc prop_ lexp typ =
 
 
 (* Add an array in prop if it is not allocated.*)
-let execute___require_allocated_array {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ =
+let execute___require_allocated_array {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args}
-  let pdesc = Summary.get_proc_desc summary in
+    : Builtin.ret_typ =
   match args with
   | [(lexp, typ)] -> (
-    match add_array_to_prop tenv pdesc prop_ lexp typ with
+    match add_array_to_prop tenv proc_desc prop_ lexp typ with
     | None ->
         []
     | Some (_, prop) ->
@@ -99,11 +98,11 @@ let execute___require_allocated_array {Builtin.tenv; summary; prop_; path; args}
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute___get_array_length {Builtin.tenv; summary; prop_; path; ret_id_typ; args} :
+let execute___get_array_length
-    Builtin.ret_typ =
+    {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ =
   match args with
   | [(lexp, typ)] -> (
-    match add_array_to_prop tenv (Summary.get_proc_desc summary) prop_ lexp typ with
+    match add_array_to_prop tenv proc_desc prop_ lexp typ with
     | None ->
         []
     | Some (len, prop) ->
@@ -112,16 +111,16 @@ let execute___get_array_length {Builtin.tenv; summary; prop_; path; ret_id_typ;
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute___set_array_length {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ =
+let execute___set_array_length {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} :
-  let pdesc = Summary.get_proc_desc summary in
+    Builtin.ret_typ =
   match args with
   | [(lexp, typ); (len, _)] -> (
-    match add_array_to_prop tenv pdesc prop_ lexp typ with
+    match add_array_to_prop tenv proc_desc prop_ lexp typ with
     | None ->
         []
     | Some (_, prop_a) -> (
         (* Invariant: prop_a has an array pointed to by lexp *)
-        let pname = Procdesc.get_proc_name pdesc in
+        let pname = Procdesc.get_proc_name proc_desc in
         let n_lexp, prop__ = check_arith_norm_exp tenv pname lexp prop_a in
         let n_len, prop = check_arith_norm_exp tenv pname len prop__ in
         let hpred, sigma' =
@@ -141,9 +140,10 @@ let execute___set_array_length {Builtin.tenv; summary; prop_; path; args} : Buil
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute___print_value {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ =
+let execute___print_value {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} :
+    Builtin.ret_typ =
   L.(debug Analysis Medium) "__print_value: " ;
-  let pname = Summary.get_proc_name summary in
+  let pname = Procdesc.get_proc_name proc_desc in
   let do_arg (lexp, _) =
     let n_lexp, _ = check_arith_norm_exp tenv pname lexp prop_ in
     L.(debug Analysis Medium) "%a " Exp.pp n_lexp
@@ -213,10 +213,11 @@ let create_type tenv n_lexp typ prop =
   else null_case @ non_null_case
 
 
-let execute___get_type_of {Builtin.summary; tenv; prop_; path; ret_id_typ; args} : Builtin.ret_typ =
+let execute___get_type_of {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args}
+    : Builtin.ret_typ =
   match args with
   | [(lexp, typ)] ->
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
       let props = create_type tenv n_lexp typ prop in
       let aux prop =
@@ -259,11 +260,11 @@ let replace_ptsto_texp tenv prop root_e texp =
   Prop.normalize tenv prop''
 
 
-let execute___instanceof_cast ~instof {Builtin.summary; tenv; prop_; path; ret_id_typ; args} :
+let execute___instanceof_cast ~instof
-    Builtin.ret_typ =
+    {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ =
   match args with
   | [(val1_, typ1); (texp2_, _)] ->
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in
       let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in
       let is_cast_to_reference =
@@ -362,10 +363,11 @@ let set_resource_attribute tenv prop path n_lexp loc ra_res =
 
 
 (** Set the attibute of the value as file *)
-let execute___set_file_attribute {Builtin.tenv; summary; prop_; path; args; loc} : Builtin.ret_typ =
+let execute___set_file_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc}
+    : Builtin.ret_typ =
   match args with
   | [(lexp, _)] ->
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
       set_resource_attribute tenv prop path n_lexp loc PredSymb.Rfile
   | _ ->
@@ -374,11 +376,11 @@ let execute___set_file_attribute {Builtin.tenv; summary; prop_; path; args; loc}
 
 (** Set the resource attribute of the first real argument of method as ignore, the first argument is
     assumed to be "this" *)
-let execute___method_set_ignore_attribute {Builtin.tenv; summary; prop_; path; args; loc} :
+let execute___method_set_ignore_attribute
-    Builtin.ret_typ =
+    {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc} : Builtin.ret_typ =
   match args with
   | [_; (lexp, _)] ->
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
       set_resource_attribute tenv prop path n_lexp loc PredSymb.Rignore
   | _ ->
@@ -386,10 +388,11 @@ let execute___method_set_ignore_attribute {Builtin.tenv; summary; prop_; path; a
 
 
 (** Set the attibute of the value as memory *)
-let execute___set_mem_attribute {Builtin.tenv; summary; prop_; path; args; loc} : Builtin.ret_typ =
+let execute___set_mem_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args; loc} :
+    Builtin.ret_typ =
   match args with
   | [(lexp, _)] ->
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
       set_resource_attribute tenv prop path n_lexp loc (PredSymb.Rmemory PredSymb.Mnew)
   | _ ->
@@ -409,19 +412,21 @@ let delete_attr tenv pdesc prop path exp attr =
 
 
 (** Set attibute att *)
-let execute___set_attr attr {Builtin.tenv; summary; prop_; path; args} : Builtin.ret_typ =
+let execute___set_attr attr {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args} :
+    Builtin.ret_typ =
   match args with
   | [(lexp, _)] ->
-      set_attr tenv (Summary.get_proc_desc summary) prop_ path lexp attr
+      set_attr tenv proc_desc prop_ path lexp attr
   | _ ->
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
 (** Delete the locked attibute of the value*)
-let execute___delete_locked_attribute {Builtin.tenv; prop_; summary; path; args} : Builtin.ret_typ =
+let execute___delete_locked_attribute {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; args}
+    : Builtin.ret_typ =
   match args with
   | [(lexp, _)] ->
-      delete_attr tenv (Summary.get_proc_desc summary) prop_ path lexp PredSymb.Alocked
+      delete_attr tenv proc_desc prop_ path lexp PredSymb.Alocked
   | _ ->
       raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -493,11 +498,11 @@ let execute_free_nonzero_ mk ?(mark_as_freed = true) pdesc tenv instr prop lexp
       raise (Exceptions.Array_of_pointsto __POS__) )
 
 
-let execute_free mk ?(mark_as_freed = true) {Builtin.summary; instr; tenv; prop_; path; args; loc} :
+let execute_free mk ?(mark_as_freed = true)
-    Builtin.ret_typ =
+    {Builtin.analysis_data= {proc_desc; tenv}; instr; prop_; path; args; loc} : Builtin.ret_typ =
   match args with
   | [(lexp, typ)] ->
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
       let prop_nonzero =
         (* case n_lexp!=0 *)
@@ -512,7 +517,7 @@ let execute_free mk ?(mark_as_freed = true) {Builtin.summary; instr; tenv; prop_
         @ (* model: if 0 then skip else execute_free_nonzero_ *)
         List.concat_map
           ~f:(fun p ->
-            execute_free_nonzero_ mk ~mark_as_freed (Summary.get_proc_desc summary) tenv instr p
+            execute_free_nonzero_ mk ~mark_as_freed proc_desc tenv instr p
               (Prop.exp_normalize_prop tenv p lexp)
               typ loc )
           prop_nonzero
@@ -529,9 +534,10 @@ let execute_free mk ?(mark_as_freed = true) {Builtin.summary; instr; tenv; prop_
  This should behave correctly most of the time. *)
 let execute_free_cf mk = execute_free mk ~mark_as_freed:false
 
-let execute_alloc mk can_return_null {Builtin.summary; tenv; prop_; path; ret_id_typ; args; loc} :
+let execute_alloc mk can_return_null
-    Builtin.ret_typ =
+    {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args; loc} : Builtin.ret_typ
-  let pname = Summary.get_proc_name summary in
+    =
+  let pname = Procdesc.get_proc_name proc_desc in
   let rec evaluate_char_sizeof e =
     match e with
     | Exp.Var _ ->
@@ -603,14 +609,15 @@ let execute_alloc mk can_return_null {Builtin.summary; tenv; prop_; path; ret_id
   else [(prop_alloc, path)]
 
 
-let execute___cxx_typeid ({Builtin.summary; tenv; prop_; args; loc; exe_env} as r) : Builtin.ret_typ
+let execute___cxx_typeid
-    =
+    ({Builtin.analysis_data= {proc_desc; tenv} as analysis_data; prop_; args; loc} as r) :
+    Builtin.ret_typ =
   match args with
   | type_info_exp :: rest -> (
       let res = execute_alloc PredSymb.Mnew false {r with args= [type_info_exp]} in
       match rest with
       | [(field_exp, _); (lexp, typ_)] ->
-          let pname = Summary.get_proc_name summary in
+          let pname = Procdesc.get_proc_name proc_desc in
           let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in
           let typ =
             List.find
@@ -629,14 +636,15 @@ let execute___cxx_typeid ({Builtin.summary; tenv; prop_; args; loc; exe_env} as
               ; e2= Exp.Const (Const.Cstr typ_string)
               ; loc }
           in
-          SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) res
+          SymExec.instrs ~mask_errors:true analysis_data (Instrs.singleton set_instr) res
       | _ ->
           res )
   | _ ->
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute_pthread_create ({Builtin.tenv; summary; prop_; path; args; exe_env} as builtin_args) :
+let execute_pthread_create
+    ({Builtin.analysis_data= {analyze_dependency; tenv}; prop_; path; args} as builtin_args) :
     Builtin.ret_typ =
   match args with
   | [_; _; start_routine; arg] -> (
@@ -661,13 +669,13 @@ let execute_pthread_create ({Builtin.tenv; summary; prop_; path; args; exe_env}
           [(prop_, path)]
       | Some pname -> (
           L.d_printfln "pthread_create: calling function %a" Procname.pp pname ;
-          match Ondemand.analyze_proc_name ~caller_summary:summary pname with
+          match analyze_dependency pname with
           | None ->
               (* no precondition to check, skip *)
               [(prop_, path)]
           | Some callee_summary ->
-              SymExec.proc_call exe_env callee_summary
+              SymExec.proc_call callee_summary {builtin_args with args= [(routine_arg, snd arg)]} )
-                {builtin_args with args= [(routine_arg, snd arg)]} ) )
+      )
   | _ ->
       raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -686,11 +694,11 @@ let execute_scan_function skip_n_arguments ({Builtin.args; ret_id_typ} as call_a
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute__unwrap_exception {Builtin.tenv; summary; prop_; path; ret_id_typ; args} :
+let execute__unwrap_exception
-    Builtin.ret_typ =
+    {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ =
   match args with
   | [(ret_exn, _)] -> (
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let n_ret_exn, prop = check_arith_norm_exp tenv pname ret_exn prop_ in
       match n_ret_exn with
       | Exp.Exn exp ->
@@ -702,11 +710,11 @@ let execute__unwrap_exception {Builtin.tenv; summary; prop_; path; ret_id_typ; a
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute_return_first_argument {Builtin.tenv; summary; prop_; path; ret_id_typ; args} :
+let execute_return_first_argument
-    Builtin.ret_typ =
+    {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args} : Builtin.ret_typ =
   match args with
   | (arg1_, _) :: _ ->
-      let pname = Procdesc.get_proc_name (Summary.get_proc_desc summary) in
+      let pname = Procdesc.get_proc_name proc_desc in
       let arg1, prop = check_arith_norm_exp tenv pname arg1_ prop_ in
       let prop' = return_result tenv arg1 prop ret_id_typ in
       [(prop', path)]
@@ -714,11 +722,11 @@ let execute_return_first_argument {Builtin.tenv; summary; prop_; path; ret_id_ty
       raise (Exceptions.Wrong_argument_number __POS__)
 
 
-let execute___split_get_nth {Builtin.tenv; summary; prop_; path; ret_id_typ; args} : Builtin.ret_typ
+let execute___split_get_nth {Builtin.analysis_data= {proc_desc; tenv}; prop_; path; ret_id_typ; args}
-    =
+    : Builtin.ret_typ =
   match args with
   | [(lexp1, _); (lexp2, _); (lexp3, _)] -> (
-      let pname = Summary.get_proc_name summary in
+      let pname = Procdesc.get_proc_name proc_desc in
       let n_lexp1, prop__ = check_arith_norm_exp tenv pname lexp1 prop_ in
       let n_lexp2, prop___ = check_arith_norm_exp tenv pname lexp2 prop__ in
       let n_lexp3, prop = check_arith_norm_exp tenv pname lexp3 prop___ in
@@ -739,7 +747,7 @@ let execute___split_get_nth {Builtin.tenv; summary; prop_; path; ret_id_typ; arg
 
 (* forces the expression passed as parameter to be assumed true at the point where this
    builtin is called, diverges if this causes an inconsistency *)
-let execute___infer_assume {Builtin.tenv; prop_; path; args} : Builtin.ret_typ =
+let execute___infer_assume {Builtin.analysis_data= {tenv}; prop_; path; args} : Builtin.ret_typ =
   match args with
   | [(lexp, _)] ->
       let prop_assume = Prop.conjoin_eq tenv lexp (Exp.bool true) prop_ in
@@ -750,8 +758,8 @@ let execute___infer_assume {Builtin.tenv; prop_; path; args} : Builtin.ret_typ =
 
 
 (* creates a named error state *)
-let execute___infer_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ
+let execute___infer_fail {Builtin.analysis_data= {tenv} as analysis_data; prop_; path; args; loc} :
-    =
+    Builtin.ret_typ =
   let error_str =
     match args with
     | [(lexp_msg, _)] -> (
@@ -771,12 +779,11 @@ let execute___infer_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env
       ; e2= Exp.Const (Const.Cstr error_str)
       ; loc }
   in
-  SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) [(prop_, path)]
+  SymExec.instrs ~mask_errors:true analysis_data (Instrs.singleton set_instr) [(prop_, path)]
 
 
 (* translate builtin assertion failure *)
-let execute___assert_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env} : Builtin.ret_typ
+let execute___assert_fail {Builtin.analysis_data; prop_; path; args; loc} : Builtin.ret_typ =
-    =
   let error_str =
     match List.length args with
     | 4 ->
@@ -792,11 +799,11 @@ let execute___assert_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_en
       ; e2= Exp.Const (Const.Cstr error_str)
       ; loc }
   in
-  SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) [(prop_, path)]
+  SymExec.instrs ~mask_errors:true analysis_data (Instrs.singleton set_instr) [(prop_, path)]
 
 
-let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt
+let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt {Builtin.analysis_data; ret_id_typ; loc}
-    {Builtin.summary; tenv; ret_id_typ; loc; exe_env} =
+    =
   let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in
   let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in
   let sizeof_typ = Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in
@@ -806,7 +813,7 @@ let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt
   let alloc_instr =
     Sil.Call (ret_id_typ, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default)
   in
-  SymExec.instrs exe_env tenv summary (Instrs.singleton alloc_instr) symb_state
+  SymExec.instrs analysis_data (Instrs.singleton alloc_instr) symb_state
 
 
 (* NSArray models *)

infer/src/biabduction/Prover.ml

@@ -2573,7 +2573,7 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
       L.d_printfln "WARNING: footprint failed to find MISSING because: %s" s ;
       None
   | Exceptions.Abduction_case_not_implemented _ as exn ->
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
       None
 
 

infer/src/biabduction/Rearrange.ml

@@ -55,7 +55,7 @@ let check_bad_index tenv pname p len index loc =
         Exceptions.Array_out_of_bounds_l1
           (Errdesc.explain_array_access pname tenv deref_str p loc, __POS__)
       in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
     else if len_is_constant then
       let deref_str = Localise.deref_str_array_bound len_const_opt index_const_opt in
       let desc = Errdesc.explain_array_access pname tenv deref_str p loc in
@@ -63,7 +63,7 @@ let check_bad_index tenv pname p len index loc =
         if index_has_bounds () then Exceptions.Array_out_of_bounds_l2 (desc, __POS__)
         else Exceptions.Array_out_of_bounds_l3 (desc, __POS__)
       in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
 
 
 (** Perform bounds checking *)
@@ -991,7 +991,7 @@ let check_type_size tenv pname prop texp off typ_from_instr =
           Exceptions.Pointer_size_mismatch
             (Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__)
         in
-        BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
+        SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
   | None ->
       L.d_str "texp: " ; Exp.d_texp_full texp ; L.d_ln ()
 

infer/src/biabduction/RetainCycles.ml

@@ -236,7 +236,7 @@ let exn_retain_cycle tenv cycle =
   Exceptions.Retain_cycle (desc, __POS__)
 
 
-let report_cycle tenv summary prop =
+let report_cycle {InterproceduralAnalysis.proc_desc; tenv; err_log} prop =
   (* When there is a cycle in objc we ignore it only if it's empty or it has weak or
      unsafe_unretained fields.  Otherwise we report a retain cycle. *)
   let cycles = get_retain_cycles tenv prop in
@@ -245,7 +245,7 @@ let report_cycle tenv summary prop =
     RetainCyclesType.Set.iter
       (fun cycle ->
         let exn = exn_retain_cycle tenv cycle in
-        SummaryReporting.log_error_using_state summary exn )
+        BiabductionReporting.log_error_using_state proc_desc err_log exn )
       cycles ;
     (* we report the retain cycles above but need to raise an exception as well to stop the analysis *)
     raise (Exceptions.Dummy_exception (Localise.verbatim_desc "retain cycle found")) )

infer/src/biabduction/RetainCycles.mli

@@ -7,4 +7,4 @@
 
 open! IStd
 
-val report_cycle : Tenv.t -> Summary.t -> Prop.normal Prop.t -> unit
+val report_cycle : BiabductionSummary.t InterproceduralAnalysis.t -> Prop.normal Prop.t -> unit

infer/src/biabduction/SymExec.ml

@@ -344,7 +344,7 @@ let check_inherently_dangerous_function caller_pname callee_pname =
       Exceptions.Inherently_dangerous_function
         (Localise.desc_inherently_dangerous_function callee_pname)
     in
-    BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn
+    SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn
 
 
 let reason_to_skip ~callee_desc : string option =
@@ -359,10 +359,10 @@ let reason_to_skip ~callee_desc : string option =
     else None
   in
   match callee_desc with
-  | `Summary callee_summary ->
+  | `Summary (callee_pdesc, callee_summary) ->
-      let attr_reason = Summary.get_attributes callee_summary |> reason_from_attributes in
+      let attr_reason = Procdesc.get_attributes callee_pdesc |> 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
+      else if List.is_empty (BiabductionSummary.get_specs callee_summary) then
         Some "empty list of specs"
       else (* we are not skipping *) None
   | `ProcDesc procdesc ->
@@ -409,7 +409,7 @@ let check_arith_norm_exp tenv pname exp prop =
           (AnalysisState.get_loc_exn ())
       in
       let exn = Exceptions.Divide_by_zero (desc, __POS__) in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
       (Prop.exp_normalize_prop tenv prop exp, prop')
   | Some (Attribute.UminusUnsigned (e, typ)), prop' ->
       let desc =
@@ -417,7 +417,7 @@ let check_arith_norm_exp tenv pname exp prop =
           (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ())
       in
       let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
       (Prop.exp_normalize_prop tenv prop exp, prop')
   | None, prop' ->
       (Prop.exp_normalize_prop tenv prop exp, prop')
@@ -475,7 +475,7 @@ let check_already_dereferenced tenv pname cond prop =
           (AnalysisState.get_node_exn ()) n (AnalysisState.get_loc_exn ())
       in
       let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
   | None ->
       ()
 
@@ -684,29 +684,26 @@ let resolve_args prop args =
 type resolve_and_analyze_result =
   { resolved_pname: Procname.t
   ; resolved_procdesc_opt: Procdesc.t option
-  ; resolved_summary_opt: Summary.t option }
+  ; resolved_summary_opt: (Procdesc.t * BiabductionSummary.t) option }
 
 (** Resolve the procedure name and run the analysis of the resolved procedure if not already
     analyzed *)
-let resolve_and_analyze tenv ~caller_summary ?(has_clang_model = false) prop args callee_proc_name
+let resolve_and_analyze
-    call_flags : resolve_and_analyze_result =
+    {InterproceduralAnalysis.analyze_dependency; analyze_pdesc_dependency; proc_desc; tenv}
+    ?(has_clang_model = false) prop args callee_proc_name call_flags : resolve_and_analyze_result =
   (* 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 : Procdesc.t option * Summary.t option =
+  let analyze_ondemand resolved_pname =
     if Procname.equal resolved_pname callee_proc_name then
-      ( Ondemand.get_proc_desc callee_proc_name
+      (AnalysisCallbacks.get_proc_desc callee_proc_name, analyze_dependency callee_proc_name)
-      , Ondemand.analyze_proc_name ~caller_summary callee_proc_name )
     else
       (* Create the type specialized procedure description and analyze it directly *)
-      let analyze specialized_pdesc =
-        Ondemand.analyze_proc_desc ~caller_summary specialized_pdesc
-      in
       let resolved_proc_desc_option =
-        match Ondemand.get_proc_desc resolved_pname with
+        match AnalysisCallbacks.get_proc_desc resolved_pname with
         | Some _ as resolved_proc_desc ->
             resolved_proc_desc
         | None ->
-            let procdesc_opt = Ondemand.get_proc_desc callee_proc_name in
+            let procdesc_opt = AnalysisCallbacks.get_proc_desc callee_proc_name in
             Option.map procdesc_opt ~f:(fun callee_proc_desc ->
                 (* It is possible that the types of the arguments are not as precise as the type of
                    the objects in the heap, so we should update them to get the best results. *)
@@ -714,12 +711,12 @@ let resolve_and_analyze tenv ~caller_summary ?(has_clang_model = false) prop arg
                 SpecializeProcdesc.with_formals_types ~has_clang_model callee_proc_desc
                   resolved_pname resolved_args )
       in
-      (resolved_proc_desc_option, Option.bind resolved_proc_desc_option ~f:analyze)
+      ( resolved_proc_desc_option
+      , Option.bind resolved_proc_desc_option ~f:(fun pdesc ->
+            analyze_pdesc_dependency pdesc |> Option.map ~f:(fun summary -> (pdesc, summary)) ) )
   in
   let resolved_pname =
-    resolve_pname
+    resolve_pname ~caller_pdesc:proc_desc tenv prop args callee_proc_name call_flags
-      ~caller_pdesc:(Summary.get_proc_desc caller_summary)
-      tenv prop args callee_proc_name call_flags
   in
   let resolved_procdesc_opt, resolved_summary_opt = analyze_ondemand resolved_pname in
   {resolved_pname; resolved_procdesc_opt; resolved_summary_opt}
@@ -858,9 +855,7 @@ let handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_
 (* This method handles ObjC instance method calls, in particular the fact that calling a method *)
 (* with nil returns nil. The exec_call function is either standard call execution or execution *)
 (* of ObjC getters and setters using a builtin. *)
-let handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc callee_pname
+let handle_objc_instance_method_call actual_pars pre tenv ret_id pdesc callee_pname path res =
-    loc path exec_call =
-  let res () = exec_call tenv ret_id pdesc callee_pname loc actual_params pre path in
   handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_pname pre ret_id res
 
 
@@ -1078,13 +1073,13 @@ let execute_store ?(report_deref_errors = true) pname pdesc tenv lhs_exp typ rhs
 
 let is_variadic_procname callee_pname =
   Option.value_map
-    (Ondemand.get_proc_desc callee_pname)
+    (AnalysisCallbacks.get_proc_desc callee_pname)
     ~f:(fun proc_desc -> (Procdesc.get_attributes proc_desc).ProcAttributes.is_variadic)
     ~default:false
 
 
-let resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params callee_pname
+let resolve_and_analyze_no_dynamic_dispatch {InterproceduralAnalysis.analyze_dependency; tenv}
-    call_flags =
+    prop_r n_actual_params callee_pname call_flags =
   let resolved_pname =
     match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with
     | resolved_pname :: _ ->
@@ -1092,15 +1087,13 @@ let resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual
     | [] ->
         callee_pname
   in
-  let resolved_summary_opt =
+  let resolved_summary_opt = analyze_dependency resolved_pname in
-    Ondemand.analyze_proc_name ~caller_summary:current_summary resolved_pname
-  in
   { resolved_pname
-  ; resolved_procdesc_opt= Ondemand.get_proc_desc resolved_pname
+  ; resolved_procdesc_opt= AnalysisCallbacks.get_proc_desc resolved_pname
   ; resolved_summary_opt }
 
 
-let resolve_and_analyze_clang current_summary tenv prop_r n_actual_params callee_pname call_flags =
+let resolve_and_analyze_clang analysis_data prop_r n_actual_params callee_pname call_flags =
   if
     Config.dynamic_dispatch
     && (not (is_variadic_procname callee_pname))
@@ -1111,30 +1104,30 @@ let resolve_and_analyze_clang current_summary tenv prop_r n_actual_params callee
     try
       let has_clang_model = BiabductionModels.mem callee_pname in
       let resolve_and_analyze_result =
-        resolve_and_analyze tenv ~caller_summary:current_summary ~has_clang_model prop_r
+        resolve_and_analyze analysis_data ~has_clang_model prop_r n_actual_params callee_pname
-          n_actual_params callee_pname call_flags
+          call_flags
       in
       (* It could be useful to specialize a model, but also it could cause a failure,
          because we don't have the correct fields in the tenv.
          In that case, default to the non-specialized spec for the model. *)
       let clang_model_specialized_failure =
         match resolve_and_analyze_result.resolved_summary_opt with
-        | Some summary when has_clang_model ->
+        | Some (_, summary) when has_clang_model ->
-            List.is_empty (Tabulation.get_specs_from_payload summary)
+            List.is_empty (BiabductionSummary.get_specs summary)
         | None ->
             true
         | _ ->
             false
       in
       if clang_model_specialized_failure then
-        resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params
+        resolve_and_analyze_no_dynamic_dispatch analysis_data prop_r n_actual_params callee_pname
-          callee_pname call_flags
+          call_flags
       else resolve_and_analyze_result
     with SpecializeProcdesc.UnmatchedParameters ->
-      resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params
+      resolve_and_analyze_no_dynamic_dispatch analysis_data prop_r n_actual_params callee_pname
-        callee_pname call_flags
+        call_flags
   else
-    resolve_and_analyze_no_dynamic_dispatch current_summary tenv prop_r n_actual_params callee_pname
+    resolve_and_analyze_no_dynamic_dispatch analysis_data prop_r n_actual_params callee_pname
       call_flags
 
 
@@ -1171,9 +1164,9 @@ let declare_locals_and_ret tenv pdesc (prop_ : Prop.normal Prop.t) =
 
 
 (** Execute [instr] with a symbolic heap [prop].*)
-let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t) path :
+let rec sym_exec
-    (Prop.normal Prop.t * Paths.Path.t) list =
+    ({InterproceduralAnalysis.proc_desc= current_pdesc; analyze_dependency; tenv} as analysis_data)
-  let current_pdesc = Summary.get_proc_desc current_summary in
+    instr_ (prop_ : Prop.normal Prop.t) path : (Prop.normal Prop.t * Paths.Path.t) list =
   let current_pname = Procdesc.get_proc_name current_pdesc in
   AnalysisState.set_instr instr_ ;
   (* mark instruction last seen *)
@@ -1207,20 +1200,17 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
       ret_id_typ ret_typ actual_args =
     let skip_res () =
       let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Info current_pname exn ;
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Info current_pname exn ;
       L.d_printfln "Skipping function '%a': %s" Procname.pp callee_pname reason ;
       unknown_or_scan_call ~is_scan:false ~reason ret_typ ret_annots
-        Builtin.
+        { Builtin.instr
-          { summary= current_summary
+        ; prop_= prop
-          ; instr
+        ; path
-          ; tenv
+        ; ret_id_typ
-          ; prop_= prop
+        ; args= actual_args
-          ; path
+        ; proc_name= callee_pname
-          ; ret_id_typ
+        ; loc
-          ; args= actual_args
+        ; analysis_data }
-          ; proc_name= callee_pname
-          ; loc
-          ; exe_env }
     in
     if is_objc_instance_method then
       handle_objc_instance_method_call_or_skip current_pdesc tenv actual_args path callee_pname prop
@@ -1228,16 +1218,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
     else skip_res ()
   in
   let call_args prop_ proc_name args ret_id_typ loc =
-    { Builtin.summary= current_summary
+    {Builtin.instr; prop_; path; ret_id_typ; args; proc_name; loc; analysis_data}
-    ; instr
-    ; tenv
-    ; prop_
-    ; path
-    ; ret_id_typ
-    ; args
-    ; proc_name
-    ; loc
-    ; exe_env }
   in
   match instr with
   | Sil.Load {id; e= rhs_exp; root_typ= typ; loc} ->
@@ -1270,8 +1251,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
               let exn =
                 Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__)
               in
-              BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning current_pname
+              SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning current_pname exn
-                exn
           | _ ->
               ()
       in
@@ -1294,8 +1274,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
               norm_args
           in
           let resolve_and_analyze_result =
-            resolve_and_analyze tenv ~caller_summary:current_summary norm_prop norm_args
+            resolve_and_analyze analysis_data norm_prop norm_args callee_pname call_flags
-              callee_pname call_flags
           in
           let resolved_pname = resolve_and_analyze_result.resolved_pname in
           match resolve_and_analyze_result.resolved_summary_opt with
@@ -1303,13 +1282,12 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
               let ret_typ = Procname.Java.get_return_typ callee_pname_java in
               let ret_annots = load_ret_annots callee_pname in
               exec_skip_call ~reason:"unknown method" resolved_pname ret_annots ret_typ
-          | Some resolved_summary -> (
+          | Some ((callee_proc_desc, _) as resolved_summary) -> (
             match reason_to_skip ~callee_desc:(`Summary resolved_summary) with
             | None ->
-                proc_call exe_env resolved_summary
+                proc_call resolved_summary (call_args prop_ callee_pname norm_args ret_id_typ loc)
-                  (call_args prop_ callee_pname norm_args ret_id_typ loc)
             | Some reason ->
-                let proc_attrs = Summary.get_attributes resolved_summary in
+                let proc_attrs = Procdesc.get_attributes callee_proc_desc in
                 let ret_annots = proc_attrs.ProcAttributes.method_annotation.return in
                 exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type
             ) )
@@ -1324,18 +1302,18 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
               skip_call ~reason norm_prop path pname ret_annots loc ret_id_typ ret_type
                 url_handled_args
             in
-            match Ondemand.analyze_proc_name ~caller_summary:current_summary pname with
+            match analyze_dependency pname with
             | None ->
                 let ret_typ = Procname.Java.get_return_typ callee_pname_java in
                 let ret_annots = load_ret_annots callee_pname in
                 exec_skip_call ~reason:"unknown method" ret_annots ret_typ
-            | Some callee_summary -> (
+            | Some ((callee_proc_desc, _) as callee_summary) -> (
               match reason_to_skip ~callee_desc:(`Summary callee_summary) with
               | None ->
                   let handled_args = call_args norm_prop pname url_handled_args ret_id_typ loc in
-                  proc_call exe_env callee_summary handled_args
+                  proc_call callee_summary handled_args
               | Some reason ->
-                  let proc_attrs = Summary.get_attributes callee_summary in
+                  let proc_attrs = Procdesc.get_attributes callee_proc_desc in
                   let ret_annots = proc_attrs.ProcAttributes.method_annotation.return in
                   exec_skip_call ~reason ret_annots proc_attrs.ProcAttributes.ret_type )
           in
@@ -1346,8 +1324,8 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
           (* method with block parameters *)
           let with_block_parameters_summary_opt =
             if call_flags.CallFlags.cf_with_block_parameters then
-              SymExecBlocks.resolve_method_with_block_args_and_analyze
+              SymExecBlocks.resolve_method_with_block_args_and_analyze analysis_data callee_pname
-                ~caller_summary:current_summary callee_pname actual_params
+                actual_params
             else None
           in
           match with_block_parameters_summary_opt with
@@ -1356,12 +1334,12 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
                 normalize_params tenv current_pname prop_r extended_actual_params
               in
               Logging.d_strln "Calling method specialized with blocks... " ;
-              proc_call exe_env resolved_summary
+              proc_call resolved_summary
                 (call_args prop_r callee_pname n_extended_actual_params ret_id_typ loc)
           | None ->
               (* Generic fun call with known name *)
               let resolve_and_analyze_result =
-                resolve_and_analyze_clang current_summary tenv prop_r n_actual_params callee_pname
+                resolve_and_analyze_clang analysis_data prop_r n_actual_params callee_pname
                   call_flags
               in
               let resolved_pname = resolve_and_analyze_result.resolved_pname in
@@ -1389,8 +1367,9 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
                 | Some reason -> (
                     let ret_annots =
                       match resolved_summary_opt with
-                      | Some summ ->
+                      | Some (proc_desc, _) ->
-                          (Summary.get_attributes summ).ProcAttributes.method_annotation.return
+                          (Procdesc.get_attributes proc_desc).ProcAttributes.method_annotation
+                            .return
                       | None ->
                           load_ret_annots resolved_pname
                     in
@@ -1404,13 +1383,15 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
                         match attrs.ProcAttributes.objc_accessor with
                         | Some objc_accessor ->
                             (* If it's an ObjC getter or setter, call the builtin rather than skipping *)
-                            handle_objc_instance_method_call n_actual_params n_actual_params prop
+                            handle_objc_instance_method_call n_actual_params prop tenv
-                              tenv (fst ret_id_typ) current_pdesc resolved_pname loc path
+                              (fst ret_id_typ) current_pdesc resolved_pname path (fun () ->
-                              (sym_exec_objc_accessor resolved_pname objc_accessor ret_type)
+                                sym_exec_objc_accessor resolved_pname objc_accessor ret_type tenv
+                                  (fst ret_id_typ) current_pdesc callee_pname loc n_actual_params
+                                  prop path )
                         | None when model_as_malloc ret_type resolved_pname ->
                             (* If it's an alloc model, call alloc rather than skipping *)
-                            sym_exec_alloc_model exe_env resolved_pname ret_type tenv ret_id_typ
+                            sym_exec_alloc_model analysis_data resolved_pname ret_type ret_id_typ
-                              current_summary loc prop path
+                              loc prop path
                         | _ ->
                             let is_objc_instance_method =
                               ClangMethodKind.equal attrs.ProcAttributes.clang_method_kind
@@ -1422,7 +1403,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
                         skip_call ~reason prop path resolved_pname ret_annots loc ret_id_typ
                           (snd ret_id_typ) n_actual_params )
                 | None ->
-                    proc_call exe_env
+                    proc_call
                       (Option.value_exn resolved_summary_opt)
                       (call_args prop resolved_pname n_actual_params ret_id_typ loc)
               in
@@ -1441,17 +1422,14 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
       let callee_pname = Procname.from_string_c_fun "__function_pointer__" in
       unknown_or_scan_call ~is_scan:false ~reason:"unresolved function pointer" (snd ret_id_typ)
         Annot.Item.empty
-        Builtin.
+        { Builtin.analysis_data
-          { summary= current_summary
+        ; instr
-          ; instr
+        ; prop_= prop_r
-          ; tenv
+        ; path
-          ; prop_= prop_r
+        ; ret_id_typ
-          ; path
+        ; args= n_actual_params
-          ; ret_id_typ
+        ; proc_name= callee_pname
-          ; args= n_actual_params
+        ; loc }
-          ; proc_name= callee_pname
-          ; loc
-          ; exe_env }
   | Sil.Metadata (Nullify (pvar, _)) -> (
       let eprop = Prop.expose prop_ in
       match
@@ -1494,12 +1472,12 @@ and diverge prop path =
 
 (** Symbolic execution of a sequence of instructions. If errors occur and [mask_errors] is true,
     just treat as skip. *)
-and instrs ?(mask_errors = false) exe_env tenv summary instrs ppl =
+and instrs ?(mask_errors = false) analysis_data instrs ppl =
   let exe_instr instr (p, path) =
     L.d_str "Executing Generated Instruction " ;
     Sil.d_instr instr ;
     L.d_ln () ;
-    try sym_exec exe_env tenv summary instr p path
+    try sym_exec analysis_data instr p path
     with exn ->
       IExn.reraise_if exn ~f:(fun () -> (not mask_errors) || not (SymOp.exn_not_failure exn)) ;
       let error = Exceptions.recognize_exception exn in
@@ -1607,8 +1585,14 @@ and add_constraints_on_actuals_by_ref tenv caller_pdesc prop actuals_by_ref call
 
 (** execute a call for an unknown or scan function *)
 and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots
-    {Builtin.tenv; summary; prop_= pre; path; ret_id_typ; args; proc_name= callee_pname; loc; instr}
+    { Builtin.analysis_data= {proc_desc; tenv; _}
-    =
+    ; prop_= pre
+    ; path
+    ; ret_id_typ
+    ; args
+    ; proc_name= callee_pname
+    ; loc
+    ; instr } =
   let remove_file_attribute prop =
     let do_exp p (e, _) =
       let do_attribute q atom =
@@ -1662,16 +1646,15 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots
   in
   let has_nonnull_annot = Annotations.ia_is_nonnull ret_annots in
   let pre_final =
-    let pdesc = Summary.get_proc_desc summary in
     (* in Java, assume that skip functions close resources passed as params *)
     let pre_1 = if Procname.is_java callee_pname then remove_file_attribute pre else pre in
     let pre_2 =
       (* TODO(jjb): Should this use the type of ret_id, or ret_type from the procedure type? *)
-      add_constraints_on_retval tenv pdesc pre_1
+      add_constraints_on_retval tenv proc_desc pre_1
         (Exp.Var (fst ret_id_typ))
         ret_typ ~has_nonnull_annot callee_pname loc
     in
-    add_constraints_on_actuals_by_ref tenv pdesc pre_2 actuals_by_ref callee_pname loc
+    add_constraints_on_actuals_by_ref tenv proc_desc pre_2 actuals_by_ref callee_pname loc
   in
   if is_scan (* if scan function, don't mark anything with undef attributes *) then
     [(Tabulation.remove_constant_string_class tenv pre_final, path)]
@@ -1694,7 +1677,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_typ ret_annots
 
 
 and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_pos)
-    {Builtin.summary; tenv; prop_; path; args; proc_name; loc; exe_env} =
+    {Builtin.analysis_data= {tenv; _} as analysis_data; prop_; path; args; proc_name; loc} =
   (* from clang's lib/Sema/SemaExpr.cpp: *)
   (* "nullPos" is the number of formal parameters at the end which *)
   (* effectively count as part of the variadic arguments.  This is *)
@@ -1713,7 +1696,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po
     (* simulate a Load for [lexp] *)
     let tmp_id_deref = Ident.create_fresh Ident.kprimed in
     let load_instr = Sil.Load {id= tmp_id_deref; e= lexp; root_typ= typ; typ; loc} in
-    try instrs exe_env tenv summary (Instrs.singleton load_instr) result
+    try instrs analysis_data (Instrs.singleton load_instr) result
     with e when SymOp.exn_not_failure e ->
       IExn.reraise_if e ~f:(fun () -> fails_on_nil) ;
       let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in
@@ -1794,8 +1777,7 @@ and sym_exec_objc_accessor callee_pname property_accesor ret_typ tenv ret_id pde
   f_accessor ret_typ tenv ret_id pdesc cur_pname loc args prop |> List.map ~f:(fun p -> (p, path))
 
 
-and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ summary loc prop path :
+and sym_exec_alloc_model analysis_data pname ret_typ ret_id_typ loc prop path : Builtin.ret_typ =
-    Builtin.ret_typ =
   let alloc_source_function_arg = (Exp.Const (Const.Cfun pname), Typ.void) in
   let args =
     let sizeof_exp =
@@ -1807,17 +1789,22 @@ and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ summary loc prop
   let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.malloc_no_fail) in
   let alloc_instr = Sil.Call (ret_id_typ, alloc_fun, args, loc, CallFlags.default) in
   L.d_strln "No spec found, method should be model as alloc, executing alloc... " ;
-  instrs exe_env tenv summary (Instrs.singleton alloc_instr) [(prop, path)]
+  instrs analysis_data (Instrs.singleton alloc_instr) [(prop, path)]
 
 
 (** Perform symbolic execution for a function call *)
-and proc_call exe_env callee_summary
+and proc_call (callee_pdesc, callee_summary)
-    {Builtin.summary; tenv; prop_= pre; path; ret_id_typ; args= actual_pars; loc} =
+    { Builtin.analysis_data= {proc_desc= caller_pdesc; tenv; _} as analysis_data
-  let caller_pname = Summary.get_proc_name summary in
+    ; prop_= pre
-  let callee_attrs = Summary.get_attributes callee_summary in
+    ; path
-  let callee_pname = Summary.get_proc_name callee_summary in
+    ; ret_id_typ
+    ; args= actual_pars
+    ; loc } =
+  let caller_pname = Procdesc.get_proc_name caller_pdesc in
+  let callee_pname = Procdesc.get_proc_name callee_pdesc in
+  let callee_attributes = Procdesc.get_attributes callee_pdesc in
   check_inherently_dangerous_function caller_pname callee_pname ;
-  let formal_types = List.map ~f:snd (Summary.get_formals callee_summary) in
+  let formal_types = List.map ~f:snd callee_attributes.ProcAttributes.formals in
   let rec comb actual_pars formal_types =
     match (actual_pars, formal_types) with
     | [], [] ->
@@ -1851,23 +1838,23 @@ and proc_call exe_env callee_summary
      parameter type if there are enough formal parameters, and
      to their actual type otherwise. The latter case happens
      with variable - arguments functions *)
-  let actual_params = comb actual_pars formal_types in
+  let actuals = comb actual_pars formal_types in
   (* In case we call an objc instance method we add an extra spec
      where the receiver is null and the semantics of the call is nop *)
-  let pdesc = Summary.get_proc_desc summary in
+  match (!Language.curr_language, callee_attributes.ProcAttributes.clang_method_kind) with
-  match (!Language.curr_language, callee_attrs.ProcAttributes.clang_method_kind) with
   | Language.Clang, ClangMethodKind.OBJC_INSTANCE ->
-      handle_objc_instance_method_call actual_pars actual_params pre tenv (fst ret_id_typ) pdesc
+      handle_objc_instance_method_call actual_pars pre tenv (fst ret_id_typ) caller_pdesc
-        callee_pname loc path
+        callee_pname path (fun () ->
-        (Tabulation.exe_function_call exe_env callee_summary)
+          Tabulation.exe_function_call analysis_data ~callee_attributes ~callee_pname
+            ~callee_summary ~ret_id:(fst ret_id_typ) loc ~actuals pre path )
   | _ ->
       (* non-objective-c method call. Standard tabulation *)
-      Tabulation.exe_function_call exe_env callee_summary tenv (fst ret_id_typ) pdesc callee_pname
+      Tabulation.exe_function_call analysis_data ~callee_summary ~ret_id:(fst ret_id_typ)
-        loc actual_params pre path
+        ~callee_pname ~callee_attributes loc ~actuals pre path
 
 
 (** perform symbolic execution for a single prop, and check for junk *)
-and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
+and sym_exec_wrapper ({InterproceduralAnalysis.tenv; _} as analysis_data) handle_exn proc_cfg instr
     ((prop : Prop.normal Prop.t), path) : Paths.PathSet.t =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let prop_primed_to_normal p =
@@ -1911,7 +1898,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
       (* Check for retain cycles after assignments and method calls *)
       ( match instr with
       | (Sil.Store _ | Sil.Call _) when !BiabductionConfig.footprint ->
-          RetainCycles.report_cycle tenv summary p
+          RetainCycles.report_cycle analysis_data p
       | _ ->
           () ) ;
       let node_has_abstraction node =
@@ -1934,7 +1921,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
     let res_list =
       BiabductionConfig.run_with_abs_val_equal_zero
         (* no exp abstraction during sym exe *)
-          (fun () -> sym_exec exe_env tenv summary instr prop' path )
+          (fun () -> sym_exec analysis_data instr prop' path)
         ()
     in
     let res_list_nojunk =
@@ -1960,7 +1947,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
 
 (** {2 Lifted Abstract Transfer Functions} *)
 
-let node handle_exn exe_env tenv summary proc_cfg (node : ProcCfg.Exceptional.Node.t)
+let node handle_exn analysis_data proc_cfg (node : ProcCfg.Exceptional.Node.t)
     (pset : Paths.PathSet.t) : Paths.PathSet.t =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let exe_instr_prop instr p tr (pset1 : Paths.PathSet.t) =
@@ -1979,7 +1966,7 @@ let node handle_exn exe_env tenv summary proc_cfg (node : ProcCfg.Exceptional.No
         Sil.d_instr instr ;
         L.d_strln " due to exception" ;
         Paths.PathSet.from_renamed_list [(p, tr)] )
-      else sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr (p, tr)
+      else sym_exec_wrapper analysis_data handle_exn proc_cfg instr (p, tr)
     in
     Paths.PathSet.union pset2 pset1
   in

infer/src/biabduction/SymExec.mli

@@ -15,9 +15,7 @@ val declare_locals_and_ret : Tenv.t -> Procdesc.t -> Prop.normal Prop.t -> Prop.
 
 val node :
      (exn -> unit)
-  -> Exe_env.t
+  -> BiabductionSummary.t InterproceduralAnalysis.t
-  -> Tenv.t
-  -> Summary.t
   -> ProcCfg.Exceptional.t
   -> ProcCfg.Exceptional.Node.t
   -> Paths.PathSet.t
@@ -26,9 +24,7 @@ val node :
 
 val instrs :
      ?mask_errors:bool
-  -> Exe_env.t
+  -> BiabductionSummary.t InterproceduralAnalysis.t
-  -> Tenv.t
-  -> Summary.t
   -> Instrs.not_reversed_t
   -> (Prop.normal Prop.t * Paths.Path.t) list
   -> (Prop.normal Prop.t * Paths.Path.t) list
@@ -38,7 +34,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 -> Summary.t -> Builtin.t
+val proc_call : Procdesc.t * BiabductionSummary.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

@@ -43,13 +43,14 @@ let get_extended_args_for_method_with_block_analysis act_params =
   List.map ~f:(fun (exp, _, typ) -> (exp, typ)) args_and_captured
 
 
-let resolve_method_with_block_args_and_analyze ~caller_summary pname act_params =
+let resolve_method_with_block_args_and_analyze
+    {InterproceduralAnalysis.analyze_dependency; analyze_pdesc_dependency} pname act_params =
   let pdesc_opt =
-    match Ondemand.analyze_proc_name ~caller_summary pname with
+    match analyze_dependency pname with
-    | Some summary ->
+    | Some (proc_desc, _) ->
-        Some (Summary.get_proc_desc summary)
+        Some proc_desc
     | None ->
-        Ondemand.get_proc_desc pname
+        AnalysisCallbacks.get_proc_desc pname
   in
   match pdesc_opt with
   | Some pdesc
@@ -88,12 +89,12 @@ let resolve_method_with_block_args_and_analyze ~caller_summary pname act_params
           Logging.(debug Analysis Verbose) "%a@." (Sil.pp_instr ~print_types:false Pp.text) instr )
         specialized_pdesc ;
       Logging.(debug Analysis Verbose) "End of instructions@." ;
-      match Ondemand.analyze_proc_desc ~caller_summary specialized_pdesc with
+      match analyze_pdesc_dependency specialized_pdesc with
       | Some summary ->
           (* Since the closures in the formals were replaced by the captured variables,
              we do the same with the actual arguments *)
           let extended_args = get_extended_args_for_method_with_block_analysis act_params in
-          Some (summary, extended_args)
+          Some ((specialized_pdesc, summary), extended_args)
       | None ->
           None )
   | _ ->

infer/src/biabduction/SymExecBlocks.mli

@@ -8,10 +8,10 @@
 open! IStd
 
 val resolve_method_with_block_args_and_analyze :
-     caller_summary:Summary.t
+     BiabductionSummary.t InterproceduralAnalysis.t
   -> Procname.t
   -> (Exp.t * Typ.t) list
-  -> (Summary.t * (Exp.t * Typ.t) list) option
+  -> ((Procdesc.t * BiabductionSummary.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. The copy is created by adding extra formals for each captured variable, and

infer/src/biabduction/Tabulation.ml

@@ -58,11 +58,6 @@ let print_results tenv actual_pre results =
   L.d_strln "***** END RESULTS FUNCTION CALL *******"
 
 
-let get_specs_from_payload summary =
-  Option.map summary.Summary.payloads.biabduction ~f:(fun BiabductionSummary.{preposts} -> preposts)
-  |> BiabductionSummary.get_specs_from_preposts
-
-
 (** Rename the variables in the spec. *)
 let spec_rename_vars pname spec =
   let prop_add_callee_suffix p =
@@ -94,23 +89,24 @@ let spec_rename_vars pname spec =
   BiabductionSummary.{pre= pre''; posts= posts''; visited= spec.BiabductionSummary.visited}
 
 
-(** Find and number the specs for [proc_name], after renaming their vars, and also return the
+(** Find and number the specs for [proc_attrs], after renaming their vars, and also return the
     parameters *)
-let spec_find_rename summary : (int * Prop.exposed BiabductionSummary.spec) list * Pvar.t list =
+let spec_find_rename proc_attrs specs :
-  let proc_name = Summary.get_proc_name summary in
+    (int * Prop.exposed BiabductionSummary.spec) list * Pvar.t list =
+  let proc_name = proc_attrs.ProcAttributes.proc_name in
   try
     let count = ref 0 in
     let rename_vars spec =
       incr count ;
       (!count, spec_rename_vars proc_name spec)
     in
-    let specs = get_specs_from_payload summary in
-    let formals = Summary.get_formals summary in
     if List.is_empty specs then
       raise
         (Exceptions.Precondition_not_found
            (Localise.verbatim_desc (Procname.to_string proc_name), __POS__)) ;
-    let formal_parameters = List.map ~f:(fun (x, _) -> Pvar.mk_callee x proc_name) formals in
+    let formal_parameters =
+      List.map ~f:(fun (x, _) -> Pvar.mk_callee x proc_name) proc_attrs.ProcAttributes.formals
+    in
     (List.map ~f:rename_vars specs, formal_parameters)
   with Caml.Not_found ->
     L.d_printfln "ERROR: found no entry for procedure %a. Give up..." Procname.pp proc_name ;
@@ -404,8 +400,7 @@ let check_path_errors_in_post tenv caller_pname post post_path =
           in
           State.set_path new_path path_pos_opt ;
           let exn = Exceptions.Divide_by_zero (desc, __POS__) in
-          BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn
+          SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn )
-          )
     | _ ->
         ()
   in
@@ -1041,13 +1036,12 @@ let missing_sigma_need_adding_to_tenv tenv hpreds =
   List.exists hpreds ~f:missing_hpred_need_adding_to_tenv
 
 
-let add_missing_field_to_tenv ~missing_sigma exe_env caller_tenv callee_pname hpreds callee_summary
+let add_missing_field_to_tenv ~missing_sigma exe_env caller_tenv callee_pname hpreds
-    =
+    callee_attributes =
   (* if hpreds are missing_sigma, we may not need to add the fields to the tenv, so we check that first *)
   let add_fields =
     if missing_sigma then missing_sigma_need_adding_to_tenv caller_tenv hpreds else true
   in
-  let callee_attributes = Summary.get_attributes callee_summary in
   (* if the callee is a model, then we don't have a tenv for it *)
   if (not callee_attributes.ProcAttributes.is_biabduction_model) && add_fields then
     let callee_tenv_opt =
@@ -1133,7 +1127,7 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
           missing_sigma_objc_class callee_summary ) ;
       let log_check_exn check =
         let exn = get_check_exn tenv check callee_pname loc __POS__ in
-        BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn
+        SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning caller_pname exn
       in
       let do_split () =
         process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld
@@ -1379,18 +1373,19 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results =
 
 
 (** 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
+let exe_function_call {InterproceduralAnalysis.exe_env; proc_desc= caller_pdesc; tenv}
-    prop path =
+    ~callee_attributes ~callee_pname ~callee_summary ~ret_id loc ~actuals prop path =
-  let callee_attributes = Summary.get_attributes callee_summary in
+  let spec_list, formal_params =
-  let spec_list, formal_params = spec_find_rename callee_summary in
+    spec_find_rename callee_attributes (BiabductionSummary.get_specs callee_summary)
+  in
   let nspecs = List.length spec_list in
   L.d_printfln "Found %d specs for function %s" nspecs (Procname.to_unique_id callee_pname) ;
   L.d_printfln "START EXECUTING SPECS FOR %s from state" (Procname.to_unique_id callee_pname) ;
   Prop.d_prop prop ;
   L.d_ln () ;
   let exe_one_spec (n, spec) =
-    exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop path spec
+    exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop path spec actuals
-      actual_params formal_params callee_summary
+      formal_params callee_attributes
   in
   let results = List.map ~f:exe_one_spec spec_list in
   exe_call_postprocess tenv ret_id callee_pname callee_attributes loc results

infer/src/biabduction/Tabulation.mli

@@ -36,18 +36,14 @@ val lookup_custom_errors : 'a Prop.t -> string option
 (** search in prop contains an error state *)
 
 val exe_function_call :
-     Exe_env.t
+     BiabductionSummary.t InterproceduralAnalysis.t
-  -> Summary.t
+  -> callee_attributes:ProcAttributes.t
-  -> Tenv.t
+  -> callee_pname:Procname.t
-  -> Ident.t
+  -> callee_summary:BiabductionSummary.t
-  -> Procdesc.t
+  -> ret_id:Ident.t
-  -> Procname.t
   -> Location.t
-  -> (Exp.t * Typ.t) list
+  -> actuals:(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_specs_from_payload : Summary.t -> Prop.normal BiabductionSummary.spec list
-(** Get the specs from the payload of the summary. *)

infer/src/biabduction/interproc.ml

@@ -192,8 +192,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 collect_preconditions proc_name tenv summary : Prop.normal BiabductionSummary.Jprop.t list =
-  let proc_name = Summary.get_proc_name summary in
   let collect_do_abstract_one tenv prop =
     if !BiabductionConfig.footprint then
       BiabductionConfig.run_in_re_execution_mode (Abs.abstract_no_symop tenv) prop
@@ -202,7 +201,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
   let pres =
     List.map
       ~f:(fun spec -> BiabductionSummary.Jprop.to_prop spec.BiabductionSummary.pre)
-      (Tabulation.get_specs_from_payload summary)
+      (BiabductionSummary.get_specs summary)
   in
   let pset = Propset.from_proplist tenv pres in
   let pset' =
@@ -368,14 +367,14 @@ let instrs_get_normal_vars instrs =
 
 
 (** Perform symbolic execution for a node starting from an initial prop *)
-let do_symbolic_execution exe_env summary proc_cfg handle_exn tenv
+let do_symbolic_execution ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_cfg handle_exn
     (node : ProcCfg.Exceptional.Node.t) (prop : Prop.normal Prop.t) (path : Paths.Path.t) =
   State.mark_execution_start node ;
   let instrs = ProcCfg.Exceptional.instrs node in
   (* fresh normal vars must be fresh w.r.t. instructions *)
   Ident.update_name_generator (instrs_get_normal_vars instrs) ;
   let pset =
-    SymExec.node handle_exn exe_env tenv summary proc_cfg node
+    SymExec.node handle_exn analysis_data proc_cfg node
       (Paths.PathSet.from_renamed_list [(prop, path)])
   in
   L.d_strln ".... After Symbolic Execution ...." ;
@@ -386,7 +385,7 @@ let do_symbolic_execution exe_env summary proc_cfg handle_exn tenv
   pset
 
 
-let forward_tabulate summary exe_env tenv proc_cfg wl =
+let forward_tabulate ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_cfg summary wl =
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let handle_exn_node curr_node exn =
     Exceptions.print_exception_html "Failure of symbolic execution: " exn ;
@@ -402,7 +401,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
     L.d_strln "SIL INSTR:" ;
     Procdesc.Node.d_instrs ~highlight:(AnalysisState.get_instr ()) curr_node ;
     L.d_ln () ;
-    BiabductionReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
+    SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
     State.mark_instr_fail exn
   in
   let exe_iter f pathset =
@@ -415,11 +414,9 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
     let log_string proc_name =
       let phase_string =
         let open BiabductionSummary in
-        summary.Summary.payloads.biabduction |> opt_get_phase |> string_of_phase_short
+        opt_get_phase summary |> string_of_phase_short
       in
-      let status = Summary.get_status summary in
+      F.sprintf "[%s:Pending] %s" phase_string (Procname.to_string proc_name)
-      F.sprintf "[%s:%s] %s" phase_string (Summary.Status.to_string status)
-        (Procname.to_string proc_name)
     in
     L.d_printfln "**** %s Node: %a, Procedure: %a, Todo: %d ****" (log_string pname)
       Procdesc.Node.pp curr_node Procname.pp pname (Paths.PathSet.size pathset_todo) ;
@@ -435,9 +432,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
     L.d_increase_indent () ;
     try
       State.reset_diverging_states_node () ;
-      let pset =
+      let pset = do_symbolic_execution analysis_data proc_cfg handle_exn curr_node prop path in
-        do_symbolic_execution exe_env summary proc_cfg handle_exn tenv curr_node prop path
-      in
       propagate_nodes_divergence tenv proc_cfg pset curr_node wl ;
       L.d_decrease_indent () ;
       L.d_ln ()
@@ -491,7 +486,7 @@ let remove_locals_formals_and_check tenv proc_cfg p =
       let dexp_opt, _ = Errdesc.vpath_find tenv p (Exp.Lvar pvar) in
       let desc = Errdesc.explain_stack_variable_address_escape loc pvar dexp_opt in
       let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
   in
   List.iter ~f:check_pvar pvars ; p'
 
@@ -696,7 +691,7 @@ let initial_prop_from_pre tenv curr_f pre =
 
 
 (** Re-execute one precondition and return some spec if there was no re-execution error. *)
-let execute_filter_prop summary exe_env tenv proc_cfg
+let execute_filter_prop ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_cfg summary
     (precondition : Prop.normal BiabductionSummary.Jprop.t) :
     Prop.normal BiabductionSummary.spec option =
   let init_node = ProcCfg.Exceptional.start_node proc_cfg in
@@ -719,7 +714,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg
   try
     Worklist.add wl init_node ;
     ignore (path_set_put_todo wl init_node init_edgeset) ;
-    forward_tabulate summary exe_env tenv proc_cfg wl ;
+    forward_tabulate analysis_data proc_cfg summary wl ;
     AnalysisCallbacks.html_debug_new_node_session ~pp_name init_node ~f:(fun () ->
         L.d_printfln ~color:Green "#### Finished: RE-execution for %a ####" Procname.pp pname ;
         L.d_increase_indent () ;
@@ -760,9 +755,9 @@ type exe_phase =
     [do, get_results] where [go ()] performs the analysis 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 : Summary.t) (proc_cfg : ProcCfg.Exceptional.t) :
+let perform_analysis_phase ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data)
-    exe_phase =
+    (proc_cfg : ProcCfg.Exceptional.t) summary_opt : exe_phase =
-  let pname = Summary.get_proc_name summary in
+  let pname = Procdesc.get_proc_name proc_desc in
   let start_node = ProcCfg.Exceptional.start_node proc_cfg in
   let compute_footprint () : exe_phase =
     let go (wl : Worklist.t) () =
@@ -770,12 +765,13 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
       let init_prop = initial_prop_from_emp tenv pdesc in
       (* use existing pre's (in recursion some might exist) as starting points *)
       let init_props_from_pres =
-        let specs = Tabulation.get_specs_from_payload summary in
         (* rename spec vars to footprint vars, and copy current to footprint *)
         let mk_init precondition =
           initial_prop_from_pre tenv pdesc (BiabductionSummary.Jprop.to_prop precondition)
         in
-        List.map ~f:(fun spec -> mk_init spec.BiabductionSummary.pre) specs
+        List.map
+          ~f:(fun spec -> mk_init spec.BiabductionSummary.pre)
+          (Option.value_map summary_opt ~default:[] ~f:BiabductionSummary.get_specs)
       in
       let init_props = Propset.from_proplist tenv (init_prop :: init_props_from_pres) in
       let init_edgeset =
@@ -792,11 +788,11 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
       L.d_decrease_indent () ;
       Worklist.add wl start_node ;
       ignore (path_set_put_todo wl start_node init_edgeset) ;
-      forward_tabulate summary exe_env tenv proc_cfg wl
+      forward_tabulate analysis_data proc_cfg summary_opt wl
     in
     let get_results (wl : Worklist.t) () =
       State.process_execution_failures
-        (BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning)
+        (SummaryReporting.log_issue_deprecated_using_state Exceptions.Warning)
         pname ;
       let results = collect_analysis_result tenv wl proc_cfg in
       let specs =
@@ -806,7 +802,7 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
             Exceptions.Internal_error
               (Localise.verbatim_desc "Leak_while_collecting_specs_after_footprint")
           in
-          BiabductionReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
+          SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
           (* returning no specs *) []
       in
       (specs, BiabductionSummary.FOOTPRINT)
@@ -816,14 +812,13 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
   in
   let re_execution () : exe_phase =
     let candidate_preconditions =
-      List.map
+      Option.value_map summary_opt ~default:[] ~f:BiabductionSummary.get_specs
-        ~f:(fun spec -> spec.BiabductionSummary.pre)
+      |> List.map ~f:(fun spec -> spec.BiabductionSummary.pre)
-        (Tabulation.get_specs_from_payload summary)
     in
     let valid_specs_rev = ref [] in
     let go () =
       let filter p =
-        let speco = execute_filter_prop summary exe_env tenv proc_cfg p in
+        let speco = execute_filter_prop analysis_data proc_cfg summary_opt p in
         (match speco with None -> () | Some spec -> valid_specs_rev := spec :: !valid_specs_rev) ;
         speco
       in
@@ -841,7 +836,7 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
     in
     (go, get_results)
   in
-  match BiabductionSummary.opt_get_phase summary.payloads.biabduction with
+  match BiabductionSummary.opt_get_phase summary_opt with
   | FOOTPRINT ->
       compute_footprint ()
   | RE_EXECUTION ->
@@ -877,7 +872,7 @@ let custom_error_preconditions summary =
       ~f:(collect_errors spec.BiabductionSummary.pre)
       ~init:errors spec.BiabductionSummary.posts
   in
-  List.fold ~f:collect_spec ~init:([], true) (Tabulation.get_specs_from_payload summary)
+  List.fold ~f:collect_spec ~init:([], true) (BiabductionSummary.get_specs summary)
 
 
 (* Remove the constrain of the form this != null which is true for all Java virtual calls *)
@@ -916,15 +911,15 @@ let is_unavoidable tenv pre =
       false
 
 
-let report_custom_errors tenv summary =
+let report_custom_errors {InterproceduralAnalysis.proc_desc; tenv} summary =
-  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 = Summary.get_loc summary in
+      let loc = Procdesc.get_loc proc_desc in
+      let pname = Procdesc.get_proc_name proc_desc in
       let err_desc = Localise.desc_custom_error loc in
       let exn = Exceptions.Custom_error (custom_error, err_desc) in
-      BiabductionReporting.log_issue_deprecated_using_state Exceptions.Error pname exn
+      SummaryReporting.log_issue_deprecated_using_state Exceptions.Error pname exn
   in
   List.iter ~f:report error_preconditions
 
@@ -936,10 +931,10 @@ module SpecMap = Caml.Map.Make (struct
 end)
 
 (** Update the specs of the current proc after the execution of one phase *)
-let update_specs tenv prev_summary phase (new_specs : BiabductionSummary.NormSpec.t list) :
+let update_specs {InterproceduralAnalysis.proc_desc; tenv} prev_summary_opt phase
-    BiabductionSummary.NormSpec.t list * bool =
+    (new_specs : BiabductionSummary.NormSpec.t list) : BiabductionSummary.NormSpec.t list * bool =
   let new_specs = BiabductionSummary.normalized_specs_to_specs new_specs in
-  let old_specs = Tabulation.get_specs_from_payload prev_summary in
+  let old_specs = Option.value_map ~default:[] ~f:BiabductionSummary.get_specs prev_summary_opt in
   let changed = ref false in
   let current_specs =
     ref
@@ -990,7 +985,7 @@ let update_specs tenv prev_summary phase (new_specs : BiabductionSummary.NormSpe
   in
   let res = ref [] in
   let convert pre (post_set, visited) =
-    let pname = Summary.get_proc_name prev_summary in
+    let pname = Procdesc.get_proc_name proc_desc in
     res :=
       Abs.abstract_spec pname tenv
         BiabductionSummary.{pre; posts= Paths.PathSet.elements post_set; visited}
@@ -1005,13 +1000,11 @@ let update_specs tenv prev_summary phase (new_specs : BiabductionSummary.NormSpe
 
 
 (** update a summary after analysing a procedure *)
-let update_summary tenv prev_summary specs phase res =
+let update_summary ({InterproceduralAnalysis.tenv; update_stats} as analysis_data) 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 new_specs, _ = update_specs analysis_data prev_summary phase normal_specs in
-  let stats =
+  update_stats ~add_symops:(SymOp.get_total ()) ?failure_kind:res () ;
-    Summary.Stats.update prev_summary.Summary.stats ~add_symops:(SymOp.get_total ())
-      ?failure_kind:res
-  in
   let preposts =
     match phase with
     | BiabductionSummary.FOOTPRINT ->
@@ -1019,55 +1012,37 @@ let update_summary tenv prev_summary specs phase res =
     | BiabductionSummary.RE_EXECUTION ->
         List.map ~f:(BiabductionSummary.NormSpec.erase_join_info_pre tenv) new_specs
   in
-  let payloads =
+  {BiabductionSummary.preposts; phase}
-    { prev_summary.Summary.payloads with
-      Payloads.biabduction= Some BiabductionSummary.{preposts; phase} }
-  in
-  {prev_summary with Summary.stats; payloads}
 
 
 (** Analyze the procedure and return the resulting summary. *)
-let analyze_proc summary exe_env tenv proc_cfg : Summary.t =
+let analyze_proc analysis_data summary_opt proc_cfg : BiabductionSummary.t =
   let proc_desc = ProcCfg.Exceptional.proc_desc proc_cfg in
   reset_global_values proc_desc ;
-  let go, get_results = perform_analysis_phase exe_env tenv summary proc_cfg in
+  let go, get_results = perform_analysis_phase analysis_data proc_cfg summary_opt in
   let res = Timeout.exe_timeout go () in
   let specs, phase = get_results () in
-  let updated_summary = update_summary tenv summary specs phase res in
+  let updated_summary = update_summary analysis_data summary_opt specs phase res in
   if Language.curr_language_is Clang && Config.report_custom_error then
-    report_custom_errors tenv updated_summary ;
+    report_custom_errors analysis_data updated_summary ;
   updated_summary
 
 
 (** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
-let transition_footprint_re_exe summary tenv joined_pres : Summary.t =
+let transition_footprint_re_exe summary tenv joined_pres : BiabductionSummary.t =
-  let summary' =
+  if Config.only_footprint then
-    if Config.only_footprint then
+    if BiabductionSummary.equal_phase summary.BiabductionSummary.phase FOOTPRINT then
-      match summary.Summary.payloads.biabduction with
+      {summary with BiabductionSummary.phase= RE_EXECUTION}
-      | Some ({phase= FOOTPRINT} as biabduction) ->
+    else summary
-          { summary with
+  else
-            Summary.payloads=
+    let preposts =
-              { summary.Summary.payloads with
+      List.map
-                Payloads.biabduction= Some {biabduction with BiabductionSummary.phase= RE_EXECUTION}
+        ~f:(fun jp ->
-              } }
+          BiabductionSummary.spec_normalize tenv
-      | _ ->
+            {BiabductionSummary.pre= jp; posts= []; visited= BiabductionSummary.Visitedset.empty} )
-          summary
+        joined_pres
-    else
+    in
-      let preposts =
+    {BiabductionSummary.preposts; phase= RE_EXECUTION}
-        List.map
-          ~f:(fun jp ->
-            BiabductionSummary.spec_normalize tenv
-              {BiabductionSummary.pre= jp; posts= []; visited= BiabductionSummary.Visitedset.empty}
-            )
-          joined_pres
-      in
-      let payloads =
-        { summary.Summary.payloads with
-          biabduction= Some BiabductionSummary.{preposts; phase= RE_EXECUTION} }
-      in
-      {summary with Summary.payloads}
-  in
-  summary'
 
 
 (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for the procedures enabled after the
@@ -1088,7 +1063,7 @@ let perform_transition proc_cfg tenv proc_name summary =
       with_start_node_session ~f:(fun () ->
           try
             BiabductionConfig.allow_leak := true ;
-            let res = collect_preconditions tenv summary in
+            let res = collect_preconditions proc_name tenv summary in
             BiabductionConfig.allow_leak := allow_leak ;
             res
           with exn when SymOp.exn_not_failure exn ->
@@ -1102,49 +1077,45 @@ let perform_transition proc_cfg tenv proc_name summary =
     in
     transition_footprint_re_exe summary tenv joined_pres
   in
-  if
+  if BiabductionSummary.equal_phase summary.BiabductionSummary.phase FOOTPRINT then
-    let open BiabductionSummary in
+    transition summary
-    summary.Summary.payloads.biabduction |> opt_get_phase |> equal_phase FOOTPRINT
-  then transition summary
   else summary
 
 
-let analyze_procedure_aux summary exe_env tenv : Summary.t =
+let analyze_procedure_aux ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) :
-  let proc_desc = Summary.get_proc_desc summary in
+    BiabductionSummary.t =
   let proc_name = Procdesc.get_proc_name proc_desc in
   let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
   let summaryfp =
-    BiabductionConfig.run_in_footprint_mode (analyze_proc summary exe_env tenv) proc_cfg
+    BiabductionConfig.run_in_footprint_mode (analyze_proc analysis_data None) proc_cfg
     |> perform_transition proc_cfg tenv proc_name
   in
   let summaryre =
-    BiabductionConfig.run_in_re_execution_mode (analyze_proc summaryfp exe_env tenv) proc_cfg
+    BiabductionConfig.run_in_re_execution_mode
+      (analyze_proc analysis_data (Some summaryfp))
+      proc_cfg
   in
   let summary_compact =
-    match summaryre.Summary.payloads.biabduction with
+    if Config.save_compact_summaries then
-    | Some BiabductionSummary.({preposts} as biabduction) when Config.save_compact_summaries ->
+      let sharing_env = Predicates.create_sharing_env () in
-        let sharing_env = Predicates.create_sharing_env () in
+      let compact_preposts =
-        let compact_preposts =
+        List.map
-          List.map ~f:(BiabductionSummary.NormSpec.compact sharing_env) preposts
+          ~f:(BiabductionSummary.NormSpec.compact sharing_env)
-        in
+          summaryre.BiabductionSummary.preposts
-        { summaryre with
+      in
-          payloads=
+      {summaryre with BiabductionSummary.preposts= compact_preposts}
-            { summaryre.payloads with
+    else summaryre
-              biabduction= Some {biabduction with BiabductionSummary.preposts= compact_preposts} }
-        }
-    | _ ->
-        summaryre
   in
   summary_compact
 
 
-let analyze_procedure {Callbacks.summary; exe_env} : Summary.t =
+let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv; err_log} as analysis_data) :
-  let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
+    BiabductionSummary.t option =
   (* make sure models have been registered *)
   BuiltinDefn.init () ;
-  if Topl.is_active () then Topl.instrument tenv (Summary.get_proc_desc summary) ;
+  if Topl.is_active () then Topl.instrument tenv proc_desc ;
-  try analyze_procedure_aux summary exe_env tenv
+  try Some (analyze_procedure_aux analysis_data)
   with exn ->
     IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
-    SummaryReporting.log_error_using_state summary exn ;
+    BiabductionReporting.log_error_using_state proc_desc err_log exn ;
-    summary
+    None

infer/src/biabduction/interproc.mli

@@ -10,5 +10,6 @@ open! IStd
 
 (** Interprocedural Analysis *)
 
-val analyze_procedure : Callbacks.proc_callback_t
+val analyze_procedure :
+  BiabductionSummary.t InterproceduralAnalysis.t -> BiabductionSummary.t option
 (** Run the biabduction analysis on the given procedure *)

infer/src/checkers/registerCheckers.ml

@@ -20,7 +20,8 @@ let () =
 
 let () =
   AnalysisCallbacks.set_callbacks
-    { html_debug_new_node_session_f= NodePrinter.with_session
+    { get_proc_desc_f= Ondemand.get_proc_desc
+    ; html_debug_new_node_session_f= NodePrinter.with_session
     ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes }
 
 
@@ -29,6 +30,38 @@ type callback_fun =
   | DynamicDispatch of Callbacks.proc_callback_t
   | File of {callback: Callbacks.file_callback_t; issue_dir: ResultsDirEntryName.id}
 
+let proc_callback_of_interprocedural payload_field checker {Callbacks.summary; exe_env} =
+  let analyze_dependency proc_name =
+    let summary = Ondemand.analyze_proc_name ~caller_summary:summary proc_name in
+    Option.bind summary ~f:(fun {Summary.payloads; proc_desc; _} ->
+        Field.get payload_field payloads |> Option.map ~f:(fun payload -> (proc_desc, payload)) )
+  in
+  let analyze_pdesc_dependency proc_desc =
+    let summary = Ondemand.analyze_proc_desc ~caller_summary:summary proc_desc in
+    Option.bind summary ~f:(fun {Summary.payloads; _} ->
+        Field.get payload_field payloads |> Option.map ~f:(fun payload -> payload) )
+  in
+  let stats = ref summary.Summary.stats in
+  let update_stats ?add_symops ?failure_kind () =
+    stats := Summary.Stats.update ?add_symops ?failure_kind !stats
+  in
+  let result =
+    checker
+      { InterproceduralAnalysis.proc_desc= Summary.get_proc_desc summary
+      ; tenv= Exe_env.get_tenv exe_env (Summary.get_proc_name summary)
+      ; err_log= Summary.get_err_log summary
+      ; exe_env
+      ; analyze_dependency
+      ; analyze_pdesc_dependency
+      ; update_stats }
+  in
+  {summary with payloads= Field.fset payload_field summary.payloads result; stats= !stats}
+
+
+let dynamic_dispatch payload_field checker =
+  DynamicDispatch (proc_callback_of_interprocedural payload_field checker)
+
+
 type callback = callback_fun * Language.t
 
 type checker = {name: string; active: bool; callbacks: callback list}
@@ -144,8 +177,9 @@ let all_checkers =
   ; { name= "biabduction"
     ; active= Config.is_checker_enabled Biabduction
     ; callbacks=
-        [ (DynamicDispatch Interproc.analyze_procedure, Language.Clang)
+        [ (dynamic_dispatch Payloads.Fields.biabduction Interproc.analyze_procedure, Language.Clang)
-        ; (DynamicDispatch Interproc.analyze_procedure, Language.Java) ] }
+        ; (dynamic_dispatch Payloads.Fields.biabduction Interproc.analyze_procedure, Language.Java)
+        ] }
   ; { name= "annotation reachability"
     ; active= Config.is_checker_enabled AnnotationReachability
     ; callbacks=

infer/src/nullsafe/eradicateCheckers.ml

@@ -16,4 +16,4 @@ let report_error tenv proc_name proc_desc kind loc ?(field_name = None)
     let localized_description = Localise.verbatim_desc description in
     let exn = exception_kind kind localized_description in
     let trace = [Errlog.make_trace_element 0 loc description []] in
-    BiabductionReporting.log_issue_deprecated_using_state severity proc_name ~loc ~ltr:trace exn
+    SummaryReporting.log_issue_deprecated_using_state severity proc_name ~loc ~ltr:trace exn

infer/src/unit/analyzerTester.ml

@@ -297,7 +297,8 @@ module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) =
 
   let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests =
     AnalysisCallbacks.set_callbacks
-      { html_debug_new_node_session_f= NodePrinter.with_session
+      { get_proc_desc_f= Ondemand.get_proc_desc
+      ; html_debug_new_node_session_f= NodePrinter.with_session
       ; proc_resolve_attributes_f= Summary.OnDisk.proc_resolve_attributes } ;
     let open OUnit2 in
     List.concat_map