From 1709db408955f1d50982c85b27c8dbce66a8192f Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Tue, 14 Nov 2017 23:50:51 -0800 Subject: [PATCH] [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 | 1 - infer/src/backend/InferPrint.ml | 33 ++++---- infer/src/backend/callbacks.ml | 5 +- infer/src/backend/interproc.ml | 21 +----- infer/src/backend/printer.ml | 3 +- infer/src/backend/reporting.ml | 5 +- infer/src/backend/specs.ml | 79 +++++++++----------- infer/src/backend/specs.mli | 23 +++--- infer/src/backend/symExec.ml | 9 +-- infer/src/checkers/annotationReachability.ml | 7 +- 10 files changed, 71 insertions(+), 115 deletions(-) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 303e9fc27..4996b40be 100644 --- a/infer/src/IR/Procdesc.ml +++ b/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 - diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index e2633987f..4d66577ac 100644 --- a/infer/src/backend/InferPrint.ml +++ b/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 diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 38b6302a5..c6d326e4b 100644 --- a/infer/src/backend/callbacks.ml +++ b/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 - diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index a52974fef..ec2ff665d 100644 --- a/infer/src/backend/interproc.ml +++ b/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 - diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index ac3505541..b6a7bce50 100644 --- a/infer/src/backend/printer.ml +++ b/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 - diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml index 375a1c105..4ea4c8d94 100644 --- a/infer/src/backend/reporting.ml +++ b/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 - diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index ee2a799ad..ddaeb11e4 100644 --- a/infer/src/backend/specs.ml +++ b/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 "
%a
@\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 "@\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 =============== *) (* diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 88aa21bb6..ab1c71145 100644 --- a/infer/src/backend/specs.mli +++ b/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. *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index e8eeb3a9d..cfec5f394 100644 --- a/infer/src/backend/symExec.ml +++ b/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) - diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 947b44099..342c4f57c 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/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 -