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 -