[infer] always store the procedure description in the summary

Summary:
We need to use the procedure description of the callees for lazy dynamic dispatch and for the resolution of the lambda. We may also need this information in other analyses, e.g. for RacerD. This diff makes the procedure description of the callees as part of the summary.

The procedure description has been part of the summary for a while already without noticeable decrease in performance.

Reviewed By: mbouaziz

Differential Revision: D6322038

fbshipit-source-id: 84101cb

infer/src/IR/Procdesc.ml

@@ -562,4 +562,3 @@ let is_captured_var procdesc pvar =
     Typ.Procname.is_objc_block procname && List.exists ~f:pvar_matches (get_captured procdesc)
   in
   is_captured_var_cpp_lambda || is_captured_var_objc_block
-

infer/src/backend/InferPrint.ml

@@ -140,8 +140,8 @@ type summary_val =
 (** compute values from summary data to export to csv format *)
 let summary_values summary =
   let stats = summary.Specs.stats in
-  let attributes = summary.Specs.attributes in
-  let err_log = attributes.ProcAttributes.err_log in
+  let attributes = Specs.get_attributes summary in
+  let err_log = Specs.get_err_log summary in
   let proc_name = Specs.get_proc_name summary in
   let signature = Specs.get_signature summary in
   let nodes_nr = List.length summary.Specs.nodes in
@@ -541,7 +541,7 @@ module CallsCsv = struct
       pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_filename caller_name)) ;
       pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_string callee_name)) ;
       pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_filename callee_name)) ;
-      pp "%s," (SourceFile.to_string summary.Specs.attributes.ProcAttributes.loc.Location.file) ;
+      pp "%s," (SourceFile.to_string (Specs.get_loc summary).Location.file) ;
       pp "%d," loc.Location.line ;
       pp "%a@\n" Specs.CallStats.pp_trace trace
     in
@@ -650,9 +650,7 @@ module Stats = struct
 
   let process_summary error_filter summary linereader stats =
     let specs = Specs.get_specs_from_payload summary in
-    let found_errors =
-      process_err_log error_filter linereader summary.Specs.attributes.ProcAttributes.err_log stats
-    in
+    let found_errors = process_err_log error_filter linereader (Specs.get_err_log summary) stats in
     let is_defective = found_errors in
     let is_verified = specs <> [] && not is_defective in
     let is_checked = not (is_defective || is_verified) in
@@ -665,7 +663,7 @@ module Stats = struct
     if is_checked then stats.nchecked <- stats.nchecked + 1 ;
     if is_timeout then stats.ntimeouts <- stats.ntimeouts + 1 ;
     if is_defective then stats.ndefective <- stats.ndefective + 1 ;
-    process_loc summary.Specs.attributes.ProcAttributes.loc stats
+    process_loc (Specs.get_loc summary) stats
 
 
   let num_files stats = Hashtbl.length stats.files
@@ -721,8 +719,8 @@ module Summary = struct
       then
         let xml_out = Utils.create_outfile (DB.filename_to_string xml_file) in
         Utils.do_outf xml_out (fun outf ->
-            Dotty.print_specs_xml (Specs.get_signature summary) specs
-              summary.Specs.attributes.ProcAttributes.loc outf.fmt ;
+            Dotty.print_specs_xml (Specs.get_signature summary) specs (Specs.get_loc summary)
+              outf.fmt ;
             Utils.close_outf outf )
 
 
@@ -896,9 +894,9 @@ let pp_issues_of_error_log error_filter linereader proc_loc_opt procname err_log
 
 
 let collect_issues summary issues_acc =
-  let err_log = summary.Specs.attributes.ProcAttributes.err_log in
+  let err_log = Specs.get_err_log summary in
   let proc_name = Specs.get_proc_name summary in
-  let proc_location = summary.Specs.attributes.ProcAttributes.loc in
+  let proc_location = Specs.get_loc summary in
   Errlog.fold
     (fun err_key err_data acc -> {Issue.proc_name; proc_location; err_key; err_data} :: acc)
     err_log issues_acc
@@ -1012,7 +1010,7 @@ let pp_lint_issues filters formats_by_report_kind linereader procname error_log
 
 (** Process a summary *)
 let process_summary filters formats_by_report_kind linereader stats fname summary issues_acc =
-  let file = summary.Specs.attributes.ProcAttributes.loc.Location.file in
+  let file = (Specs.get_loc summary).Location.file in
   let proc_name = Specs.get_proc_name summary in
   let error_filter = error_filter filters proc_name in
   let pp_simple_saved = !Config.pp_simple in
@@ -1056,14 +1054,9 @@ module AnalysisResults = struct
     let do_load () = spec_files_from_cmdline () |> List.iter ~f:load_file in
     Utils.without_gc ~f:do_load ;
     let summ_cmp (_, summ1) (_, summ2) =
-      let n =
-        SourceFile.compare summ1.Specs.attributes.ProcAttributes.loc.Location.file
-          summ2.Specs.attributes.ProcAttributes.loc.Location.file
-      in
-      if n <> 0 then n
-      else
-        Int.compare summ1.Specs.attributes.ProcAttributes.loc.Location.line
-          summ2.Specs.attributes.ProcAttributes.loc.Location.line
+      let loc1 = Specs.get_loc summ1 and loc2 = Specs.get_loc summ2 in
+      let n = SourceFile.compare loc1.Location.file loc2.Location.file in
+      if n <> 0 then n else Int.compare loc1.Location.line loc2.Location.line
     in
     List.sort ~cmp:summ_cmp !summaries
 

infer/src/backend/callbacks.ml

@@ -97,10 +97,8 @@ let iterate_callbacks call_graph exe_env =
     match Exe_env.get_proc_desc exe_env proc_name with
     | Some pdesc ->
         Some pdesc
-    | None when Config.(equal_dynamic_dispatch dynamic_dispatch Lazy) ->
-        Option.bind (Specs.get_summary proc_name) ~f:(fun summary -> summary.Specs.proc_desc_option)
     | None ->
-        None
+        Option.map ~f:Specs.get_proc_desc (Specs.get_summary proc_name)
   in
   let analyze_ondemand summary proc_desc =
     iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc
@@ -122,4 +120,3 @@ let iterate_callbacks call_graph exe_env =
   (* Unregister callbacks *)
   Ondemand.unset_callbacks () ;
   Config.curr_language := saved_language
-

infer/src/backend/interproc.ml

@@ -1165,7 +1165,7 @@ let report_custom_errors tenv summary =
   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.Specs.attributes.ProcAttributes.loc in
+      let loc = Specs.get_loc summary in
       let err_desc = Localise.desc_custom_error loc in
       let exn = Exceptions.Custom_error (custom_error, err_desc) in
       Reporting.log_error_deprecated pname exn
@@ -1400,28 +1400,16 @@ let do_analysis_closures exe_env : Tasks.closure list =
       match Exe_env.get_proc_desc exe_env pname with Some pdesc -> pdesc | None -> assert false
     in
     let nodes = List.map ~f:(fun n -> Procdesc.Node.get_id n) (Procdesc.get_nodes pdesc) in
-    let proc_flags = Procdesc.get_flags pdesc in
-    let static_err_log = Procdesc.get_err_log pdesc in
-    (* err log from translation *)
     let calls = get_calls pdesc in
-    let attributes =
-      {(Procdesc.get_attributes pdesc) with ProcAttributes.err_log= static_err_log}
-    in
-    let proc_desc_option =
-      if Config.(equal_dynamic_dispatch dynamic_dispatch Lazy) then Some pdesc else None
-    in
-    ignore (Specs.init_summary (nodes, proc_flags, calls, attributes, proc_desc_option))
+    ignore (Specs.init_summary (nodes, calls, pdesc))
   in
   let callbacks =
     let get_proc_desc proc_name =
       match Exe_env.get_proc_desc exe_env proc_name with
       | Some pdesc ->
           Some pdesc
-      | None when Config.(equal_dynamic_dispatch dynamic_dispatch Lazy) ->
-          Option.bind (Specs.get_summary proc_name) ~f:(fun summary ->
-              summary.Specs.proc_desc_option )
       | None ->
-          None
+          Option.map ~f:Specs.get_proc_desc (Specs.get_summary proc_name)
     in
     let analyze_ondemand _ proc_desc =
       let proc_name = Procdesc.get_proc_name proc_desc in
@@ -1503,7 +1491,7 @@ let print_stats_cfg proc_shadowed source cfg =
           Typ.Procname.pp proc_name
     | Some summary ->
         let stats = summary.Specs.stats in
-        let err_log = summary.Specs.attributes.ProcAttributes.err_log in
+        let err_log = Specs.get_err_log summary in
         incr num_proc ;
         let specs = Specs.get_specs_from_payload summary in
         tot_specs := List.length specs + !tot_specs ;
@@ -1578,4 +1566,3 @@ let print_stats cluster =
       in
       print_stats_cfg proc_shadowed source cfg)
     exe_env
-

infer/src/backend/printer.ml

@@ -437,7 +437,7 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro
         List.iter
           ~f:(fun sp -> proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover)
           (Specs.get_specs_from_payload summary) ;
-        Errlog.update global_err_log summary.Specs.attributes.ProcAttributes.err_log )
+        Errlog.update global_err_log (Specs.get_err_log summary) )
 
 
 (** Create filename.ext.html. *)
@@ -559,4 +559,3 @@ let write_all_html_files cluster =
         (fun file -> write_html_file linereader file (Cfg.get_all_procs cfg))
         source_files_in_cfg)
     exe_env
-

infer/src/backend/reporting.ml

@@ -41,11 +41,11 @@ let log_issue_from_summary err_kind summary ?loc ?node_id ?session ?ltr ?linters
   let should_suppress_lint =
     Config.curr_language_is Config.Java
     && Annotations.ia_is_suppress_lint
-         (fst summary.Specs.attributes.ProcAttributes.method_annotation)
+         (fst (Specs.get_attributes summary).ProcAttributes.method_annotation)
   in
   if should_suppress_lint || is_generated_method then () (* Skip the reporting *)
   else
-    let err_log = summary.Specs.attributes.ProcAttributes.err_log in
+    let err_log = Specs.get_err_log summary in
     log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr ?linters_def_file ?doc_url
       exn
 
@@ -87,4 +87,3 @@ let log_warning_deprecated ?(store_summary= false) =
 
 let log_info_deprecated ?(store_summary= false) =
   log_issue_deprecated ~store_summary Exceptions.Kinfo
-

infer/src/backend/specs.ml

@@ -365,8 +365,26 @@ type summary =
   ; sessions: int ref  (** Session number: how many nodes went trough symbolic execution *)
   ; stats: stats  (** statistics: execution time and list of errors *)
   ; status: status  (** Analysis status of the procedure *)
-  ; attributes: ProcAttributes.t  (** Attributes of the procedure *)
-  ; proc_desc_option: Procdesc.t option }
+  ; proc_desc: Procdesc.t  (** Proc desc of the procdure *) }
+
+let get_status summary = summary.status
+
+let get_proc_desc summary = summary.proc_desc
+
+let get_attributes summary = Procdesc.get_attributes summary.proc_desc
+
+let get_proc_name summary = (get_attributes summary).ProcAttributes.proc_name
+
+let get_ret_type summary = (get_attributes summary).ProcAttributes.ret_type
+
+let get_formals summary = (get_attributes summary).ProcAttributes.formals
+
+let get_err_log summary = (get_attributes summary).ProcAttributes.err_log
+
+let get_loc summary = (get_attributes summary).ProcAttributes.loc
+
+(** Return the current phase for the proc *)
+let get_phase summary = summary.phase
 
 type spec_tbl = summary Typ.Procname.Hash.t
 
@@ -465,10 +483,10 @@ let get_signature summary =
       let pp f = F.fprintf f "%a %a" (Typ.pp_full Pp.text) typ Mangled.pp p in
       let decl = F.asprintf "%t" pp in
       s := if String.equal !s "" then decl else !s ^ ", " ^ decl)
-    summary.attributes.ProcAttributes.formals ;
+    (get_formals summary) ;
   let pp f =
-    F.fprintf f "%a %a" (Typ.pp_full Pp.text) summary.attributes.ProcAttributes.ret_type
-      Typ.Procname.pp summary.attributes.ProcAttributes.proc_name
+    F.fprintf f "%a %a" (Typ.pp_full Pp.text) (get_ret_type summary) Typ.Procname.pp
+      (get_proc_name summary)
   in
   let decl = F.asprintf "%t" pp in
   decl ^ "(" ^ !s ^ ")"
@@ -521,32 +539,29 @@ let pp_payload pe fmt
 
 
 let pp_summary_text fmt summary =
-  let err_log = summary.attributes.ProcAttributes.err_log in
   let pe = Pp.text in
   pp_summary_no_stats_specs fmt summary ;
-  F.fprintf fmt "%a@\n%a%a" pp_errlog err_log pp_stats summary.stats (pp_payload pe)
+  F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) pp_stats summary.stats (pp_payload pe)
     summary.payload
 
 
 let pp_summary_latex color fmt summary =
-  let err_log = summary.attributes.ProcAttributes.err_log in
   let pe = Pp.latex color in
   F.fprintf fmt "\\begin{verbatim}@\n" ;
   pp_summary_no_stats_specs fmt summary ;
-  F.fprintf fmt "%a@\n" pp_errlog err_log ;
+  F.fprintf fmt "%a@\n" pp_errlog (get_err_log summary) ;
   F.fprintf fmt "%a@\n" pp_stats summary.stats ;
   F.fprintf fmt "\\end{verbatim}@\n" ;
   F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary)
 
 
 let pp_summary_html source color fmt summary =
-  let err_log = summary.attributes.ProcAttributes.err_log in
   let pe = Pp.html color in
   Io_infer.Html.pp_start_color fmt Black ;
   F.fprintf fmt "@\n%a" pp_summary_no_stats_specs summary ;
   Io_infer.Html.pp_end_color fmt () ;
   F.fprintf fmt "<br />%a<br />@\n" pp_stats summary.stats ;
-  Errlog.pp_html source [] fmt err_log ;
+  Errlog.pp_html source [] fmt (get_err_log summary) ;
   Io_infer.Html.pp_hline fmt () ;
   F.fprintf fmt "<LISTING>@\n" ;
   pp_payload pe fmt summary.payload ;
@@ -683,9 +698,7 @@ let proc_is_library proc_attributes =
 *)
 let proc_resolve_attributes proc_name =
   let from_attributes_table () = Attributes.load proc_name in
-  let from_specs () =
-    match get_summary proc_name with Some summary -> Some summary.attributes | None -> None
-  in
+  let from_specs () = Option.map ~f:get_attributes (get_summary proc_name) in
   match from_specs () with
   | Some attributes
     -> (
@@ -713,19 +726,6 @@ let pdesc_resolve_attributes proc_desc =
 
 let summary_exists proc_name = match get_summary proc_name with Some _ -> true | None -> false
 
-let get_status summary = summary.status
-
-let get_proc_name summary = summary.attributes.ProcAttributes.proc_name
-
-let get_ret_type summary = summary.attributes.ProcAttributes.ret_type
-
-let get_formals summary = summary.attributes.ProcAttributes.formals
-
-let get_attributes summary = summary.attributes
-
-(** Return the current phase for the proc *)
-let get_phase summary = summary.phase
-
 (** Save summary for the procedure into the spec database *)
 let store_summary (summ1: summary) =
   let summ2 =
@@ -757,7 +757,7 @@ let empty_payload =
 (** [init_summary (depend_list, nodes,
     proc_flags, calls, in_out_calls_opt, proc_attributes)]
     initializes the summary for [proc_name] given dependent procs in list [depend_list]. *)
-let init_summary (nodes, proc_flags, calls, proc_attributes, proc_desc_option) =
+let init_summary (nodes, calls, proc_desc) =
   let summary =
     { nodes
     ; phase= FOOTPRINT
@@ -765,31 +765,20 @@ let init_summary (nodes, proc_flags, calls, proc_attributes, proc_desc_option) =
     ; payload= empty_payload
     ; stats= empty_stats calls
     ; status= Pending
-    ; attributes= {proc_attributes with ProcAttributes.proc_flags}
-    ; proc_desc_option }
+    ; proc_desc }
   in
-  Typ.Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name summary ;
+  Typ.Procname.Hash.replace spec_tbl (Procdesc.get_proc_name proc_desc) summary ;
   summary
 
 
 let dummy =
-  init_summary
-    ( []
-    , ProcAttributes.proc_flags_empty ()
-    , []
-    , ProcAttributes.default Typ.Procname.empty_block Config.Java
-    , None )
+  let dummy_attributes = ProcAttributes.default Typ.Procname.empty_block Config.Java in
+  let dummy_proc_desc = Procdesc.from_proc_attributes ~called_from_cfg:true dummy_attributes in
+  init_summary ([], [], dummy_proc_desc)
 
 
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
-let reset_summary proc_desc =
-  let proc_desc_option =
-    if Config.(equal_dynamic_dispatch dynamic_dispatch Lazy) then Some proc_desc else None
-  in
-  let attributes = Procdesc.get_attributes proc_desc in
-  let proc_flags = attributes.ProcAttributes.proc_flags in
-  init_summary ([], proc_flags, [], attributes, proc_desc_option)
-
+let reset_summary proc_desc = init_summary ([], [], proc_desc)
 
 (* =============== END of support for spec tables =============== *)
 (*

infer/src/backend/specs.mli

@@ -148,8 +148,7 @@ type summary =
   ; sessions: int ref  (** Session number: how many nodes went trough symbolic execution *)
   ; stats: stats  (** statistics: execution time and list of errors *)
   ; status: status  (** Analysis status of the procedure *)
-  ; attributes: ProcAttributes.t  (** Attributes of the procedure *)
-  ; proc_desc_option: Procdesc.t option }
+  ; proc_desc: Procdesc.t }
 
 val dummy : summary
 (** dummy summary for testing *)
@@ -172,6 +171,8 @@ val get_summary : Typ.Procname.t -> summary option
 val get_proc_name : summary -> Typ.Procname.t
 (** Get the procedure name *)
 
+val get_proc_desc : summary -> Procdesc.t
+
 val get_attributes : summary -> ProcAttributes.t
 (** Get the attributes of the procedure. *)
 
@@ -184,6 +185,10 @@ val get_formals : summary -> (Mangled.t * Typ.t) list
 val get_phase : summary -> phase
 (** Return the current phase for the proc *)
 
+val get_err_log : summary -> Errlog.t
+
+val get_loc : summary -> Location.t
+
 val get_signature : summary -> string
 (** Return the signature of a procedure declaration as a string *)
 
@@ -197,16 +202,10 @@ val get_status : summary -> status
 (** Return the status (active v.s. inactive) of a procedure summary *)
 
 val init_summary :
-  Procdesc.Node.id list
-  * (* nodes *)
-    ProcAttributes.proc_flags
-  * (* procedure flags *)
-    (Typ.Procname.t * Location.t) list
-  * (* calls *)
-    ProcAttributes.t
-  * (* attributes of the procedure *)
-    Procdesc.t option
-  (* procdesc option *) -> summary
+  Procdesc.Node.id list * (* nodes *)
+                          (Typ.Procname.t * Location.t) list * (* calls *)
+                                                               Procdesc.t
+  (* procdesc *) -> summary
 (** Initialize the summary for [proc_name] given dependent procs in list [depend_list].
     This also stores the new summary in the spec table. *)
 

infer/src/backend/symExec.ml

@@ -386,7 +386,7 @@ let check_inherently_dangerous_function caller_pname callee_pname =
 
 
 let reason_to_skip callee_summary : string option =
-  let attributes = callee_summary.Specs.attributes in
+  let attributes = Specs.get_attributes callee_summary in
   if attributes.ProcAttributes.is_abstract then Some "abstract method"
   else if not attributes.ProcAttributes.is_defined then Some "method has no implementation"
   else if List.is_empty (Specs.get_specs_from_payload callee_summary) then
@@ -1214,7 +1214,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
             | None ->
                 proc_call resolved_summary (call_args prop_ callee_pname norm_args ret_id loc)
             | Some reason ->
-                let proc_attrs = resolved_summary.Specs.attributes in
+                let proc_attrs = Specs.get_attributes resolved_summary in
                 let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
                 exec_skip_call ~reason resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type
           )
@@ -1240,7 +1240,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                   let handled_args = call_args norm_prop pname url_handled_args ret_id loc in
                   proc_call callee_summary handled_args
               | Some reason ->
-                  let proc_attrs = callee_summary.Specs.attributes in
+                  let proc_attrs = Specs.get_attributes callee_summary in
                   let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in
                   exec_skip_call ~reason ret_annots proc_attrs.ProcAttributes.ret_type
           in
@@ -1318,7 +1318,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                         match resolved_summary_opt with
                         | Some summ ->
                             let ret_annots, _ =
-                              summ.Specs.attributes.ProcAttributes.method_annotation
+                              (Specs.get_attributes summ).ProcAttributes.method_annotation
                             in
                             ret_annots
                         | None ->
@@ -1881,4 +1881,3 @@ let node handle_exn tenv proc_cfg (node: ProcCfg.Exceptional.node) (pset: Paths.
     Paths.PathSet.fold (exe_instr_prop instr) pset Paths.PathSet.empty
   in
   List.fold ~f:exe_instr_pset ~init:pset (ProcCfg.Exceptional.instrs node)
-

infer/src/checkers/annotationReachability.ml

@@ -189,11 +189,7 @@ let report_annotation_stack src_annot snk_annot src_summary loc trace stack_str
 let report_call_stack summary end_of_stack lookup_next_calls report call_site sink_map =
   (* TODO: stop using this; we can use the call site instead *)
   let lookup_location pname =
-    match Specs.get_summary pname with
-    | None ->
-        Location.dummy
-    | Some summary ->
-        summary.Specs.attributes.ProcAttributes.loc
+    Option.value_map ~f:Specs.get_loc ~default:Location.dummy (Specs.get_summary pname)
   in
   let rec loop fst_call_loc visited_pnames (trace, stack_str) (callee_pname, call_loc) =
     if end_of_stack callee_pname then
@@ -473,4 +469,3 @@ let checker ({Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary =
       Summary.update_summary annot_map summary
   | None ->
       summary
-