From 75950384c90dcaef6fd674e8e82d136d8fbe7486 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Mon, 28 Sep 2015 10:08:16 -0200 Subject: [PATCH] [backend] Extend results directory with attributes for each procedure. --- infer/src/backend/DB.ml | 1 + infer/src/backend/attributesTable.ml | 39 ++++++++ infer/src/backend/attributesTable.mli | 17 ++++ infer/src/backend/callbacks.ml | 22 ++--- infer/src/backend/cfg.ml | 129 +++++++++++++------------- infer/src/backend/cfg.mli | 3 - infer/src/backend/config.ml | 3 +- infer/src/backend/exe_env.ml | 42 ++++----- infer/src/backend/exe_env.mli | 3 - infer/src/backend/fork.ml | 19 ++-- infer/src/backend/inferanalyze.ml | 49 +++------- infer/src/backend/interproc.ml | 13 +-- infer/src/backend/ondemand.ml | 4 +- infer/src/backend/serialization.ml | 5 +- infer/src/backend/serialization.mli | 32 ++++--- infer/src/backend/specs.ml | 37 ++++---- infer/src/backend/specs.mli | 11 +-- infer/src/backend/symExec.ml | 2 +- infer/src/checkers/checkers.ml | 4 +- infer/src/checkers/codeQuery.ml | 2 +- infer/src/checkers/eradicate.ml | 90 ++++++++++-------- infer/src/checkers/eradicateChecks.ml | 2 +- infer/src/checkers/patternMatch.ml | 9 +- infer/src/checkers/patternMatch.mli | 10 +- infer/src/checkers/typeCheck.ml | 22 ++--- 25 files changed, 299 insertions(+), 271 deletions(-) create mode 100644 infer/src/backend/attributesTable.ml create mode 100644 infer/src/backend/attributesTable.mli diff --git a/infer/src/backend/DB.ml b/infer/src/backend/DB.ml index 1c580e86d..615cd216e 100644 --- a/infer/src/backend/DB.ml +++ b/infer/src/backend/DB.ml @@ -292,6 +292,7 @@ module Results_dir = struct let init () = create_dir !Config.results_dir; create_dir (specs_dir ()); + create_dir (path_to_filename Abs_root [Config.attributes_dir_name]); create_dir (path_to_filename Abs_root [Config.sources_dir_name]); create_dir (path_to_filename Abs_root [Config.captured_dir_name]); if not (source_file_equal !current_source source_file_empty) then diff --git a/infer/src/backend/attributesTable.ml b/infer/src/backend/attributesTable.ml new file mode 100644 index 000000000..caea23f09 --- /dev/null +++ b/infer/src/backend/attributesTable.ml @@ -0,0 +1,39 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open Utils +module F = Format +module L = Logging + +(** Module to manage the table of attributes. *) + +let serializer : ProcAttributes.t Serialization.serializer = + Serialization.create_serializer Serialization.attributes_key + +let attributes_filename pname = + let pname_file = Procname.to_filename pname in + pname_file ^ ".attr" + +(** path to the .attr file for the given procedure in the current results directory *) +let res_dir_attr_filename pname = + DB.Results_dir.path_to_filename + DB.Results_dir.Abs_root [Config.attributes_dir_name; attributes_filename pname] + +let store_attributes proc_attributes = + let proc_name = proc_attributes.ProcAttributes.proc_name in + let attributes_file = res_dir_attr_filename proc_name in + let should_write = (* only overwrite defined procedures *) + proc_attributes.ProcAttributes.is_defined || + not (DB.file_exists attributes_file) in + if should_write then + Serialization.to_file serializer attributes_file proc_attributes + +let load_attributes proc_name = + let attributes_file = res_dir_attr_filename proc_name in + Serialization.from_file serializer attributes_file diff --git a/infer/src/backend/attributesTable.mli b/infer/src/backend/attributesTable.mli new file mode 100644 index 000000000..e615d93d7 --- /dev/null +++ b/infer/src/backend/attributesTable.mli @@ -0,0 +1,17 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Module to manage the table of attributes. *) + + +(** Save .attr file for the procedure into the attributes database. *) +val store_attributes : ProcAttributes.t -> unit + +(** Load the attributes for the procedure from the attributes database. *) +val load_attributes : Procname.t -> ProcAttributes.t option diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 3434babe3..d084f82d2 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -138,11 +138,13 @@ let iterate_procedure_callbacks all_procs exe_env proc_name = Cfg.Procdesc.find_from_name cfg proc_name in let update_time proc_name elapsed = - let prev_summary = Specs.get_summary_unsafe proc_name in - let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in - let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in - let summary = { prev_summary with Specs.stats = stats } in - Specs.add_summary proc_name summary in + match Specs.get_summary proc_name with + | Some prev_summary -> + let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in + let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in + let summary = { prev_summary with Specs.stats = stats } in + Specs.add_summary proc_name summary + | None -> () in Option.may (fun (idenv, tenv, proc_name, proc_desc, language) -> @@ -213,16 +215,8 @@ let iterate_callbacks store_summary call_graph exe_env = (* Return all values of the map *) list_map snd (StringMap.bindings cluster_map) in let reset_summary proc_name = - let cfg_opt = - try - Some (Exe_env.get_cfg exe_env proc_name) with - | Not_found -> None in - let procdesc_opt = match cfg_opt with - | Some cfg -> - Cfg.Procdesc.find_from_name cfg proc_name - | None -> None in let attributes_opt = - Option.map Cfg.Procdesc.get_attributes procdesc_opt in + Specs.proc_resolve_attributes proc_name in Specs.reset_summary call_graph proc_name attributes_opt in diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index 9f8fa5f0d..32b1e3eef 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -118,36 +118,6 @@ module Node = struct with Not_found -> () in Procname.Hash.iter mark_pdesc_if_unchanged new_procs - let compute_enabled_verbose = false - - (** restrict the cfg to the given enabled (active and not shadowed) procedures *) - let cfg_restrict_enabled cfg source enabled = - match enabled with - | None -> () - | Some enabled_procs -> - if compute_enabled_verbose then L.err "cfg_restrict_enabled: checking enabled in %s@." (DB.source_file_to_string source); - let is_enabled pname = Procname.Set.mem pname enabled_procs in - let in_address_set pname = Procname.Set.mem pname cfg.priority_set in - let node_list' = - let filter_node node = match node.nd_proc with - | None -> true - | Some pdesc -> is_enabled pdesc.pd_attributes.ProcAttributes.proc_name in - list_filter filter_node !(cfg.node_list) in - let procs_to_remove = - let psetr = ref Procname.Set.empty in - let do_proc pname pdesc = - if pdesc.pd_attributes.ProcAttributes.is_defined && - not (is_enabled pname) && - not (in_address_set pname) then - psetr := Procname.Set.add pname !psetr in - Procname.Hash.iter do_proc cfg.name_pdesc_tbl; - !psetr in - let remove_proc pname = - if compute_enabled_verbose then L.err "cfg_restrict_enabled: Removing proc not enabled from the cfg: %s@." (Procname.to_filename pname); - Procname.Hash.remove cfg.name_pdesc_tbl pname in - cfg.node_list := node_list'; - Procname.Set.iter remove_proc procs_to_remove - let node_id_gen cfg = incr cfg.node_id; !(cfg.node_id) let pdesc_tbl_add cfg proc_name proc_desc = @@ -638,42 +608,6 @@ end type node = Node.t type cfg = Node.cfg -(** Serializer for control flow graphs *) -let cfg_serializer : cfg Serialization.serializer = Serialization.create_serializer Serialization.cfg_key - -(** Load a cfg from a file *) -let load_cfg_from_file (filename : DB.filename) : cfg option = - Serialization.from_file cfg_serializer filename - -(** save a copy in the results dir of the source files of procedures defined in the cfg, unless an updated copy already exists *) -let save_source_files cfg = - let process_proc pname pdesc = - let loc = Node.proc_desc_get_loc pdesc in - let source_file = loc.Location.file in - let source_file_str = DB.source_file_to_abs_path source_file in - let dest_file = DB.source_file_in_resdir source_file in - let dest_file_str = DB.filename_to_string dest_file in - let needs_copy = - Node.proc_desc_is_defined pdesc && - Sys.file_exists source_file_str && - (not (Sys.file_exists dest_file_str) || - DB.file_modified_time (DB.filename_from_string source_file_str) > DB.file_modified_time dest_file) in - if needs_copy then - match Utils.copy_file source_file_str dest_file_str with - | Some _ -> () - | None -> L.err "Error cannot create copy of source file %s@." source_file_str in - Node.iter_proc_desc cfg process_proc - -(** Save a cfg into a file *) -let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg: cfg) = - if save_sources then save_source_files cfg; - if !Config.incremental_procs then - begin - match load_cfg_from_file filename with - | Some old_cfg -> Node.mark_unchanged_pdescs cfg old_cfg - | None -> () - end; - Serialization.to_file cfg_serializer filename cfg (* =============== START of module Procdesc =============== *) module Procdesc = struct @@ -1000,3 +934,66 @@ let remove_seed_captured_vars_block captured_vars prop = let sigma = Prop.get_sigma prop in let sigma' = list_filter (fun hpred -> not (hpred_seed_captured hpred)) sigma in Prop.normalize (Prop.replace_sigma sigma' prop) + +(** Serializer for control flow graphs *) +let cfg_serializer : cfg Serialization.serializer = + Serialization.create_serializer Serialization.cfg_key + +(** Load a cfg from a file *) +let load_cfg_from_file (filename : DB.filename) : cfg option = + Serialization.from_file cfg_serializer filename + +(** save a copy in the results dir of the source files of procedures defined in the cfg, + unless an updated copy already exists *) +let save_source_files cfg = + let process_proc pname pdesc = + let loc = Node.proc_desc_get_loc pdesc in + let source_file = loc.Location.file in + let source_file_str = DB.source_file_to_abs_path source_file in + let dest_file = DB.source_file_in_resdir source_file in + let dest_file_str = DB.filename_to_string dest_file in + let needs_copy = + Node.proc_desc_is_defined pdesc && + Sys.file_exists source_file_str && + (not (Sys.file_exists dest_file_str) || + DB.file_modified_time (DB.filename_from_string source_file_str) + > + DB.file_modified_time dest_file) in + if needs_copy then + match Utils.copy_file source_file_str dest_file_str with + | Some _ -> () + | None -> L.err "Error cannot create copy of source file %s@." source_file_str in + Node.iter_proc_desc cfg process_proc + +(** Save the .attr files for the procedures in the cfg. *) +let save_attributes filename cfg = + let save_proc proc_desc = + let attributes = Procdesc.get_attributes proc_desc in + let loc = attributes.ProcAttributes.loc in + let attributes' = + if Location.equal loc Location.dummy then + let loc' = {loc with Location.file = !DB.current_source } in + {attributes with ProcAttributes.loc = loc'} + else + attributes in + (* + L.stderr "save_proc@. proc_name:%a@. filename:%s@. current_source:%s@. loc:%s@." + Procname.pp (Procdesc.get_proc_name proc_desc) + (DB.filename_to_string filename) + (DB.source_file_to_string !DB.current_source) + (Location.to_string loc); + *) + AttributesTable.store_attributes attributes' in + list_iter save_proc (get_all_procs cfg) + +(** Save a cfg into a file *) +let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg : cfg) = + if save_sources then save_source_files cfg; + if !Config.incremental_procs then + begin + match load_cfg_from_file filename with + | Some old_cfg -> Node.mark_unchanged_pdescs cfg old_cfg + | None -> () + end; + save_attributes filename cfg; + Serialization.to_file cfg_serializer filename cfg diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index d03919f0d..cd5ef02a8 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -157,9 +157,6 @@ module Node : sig (** Add declarations for local variables and return variable to the node *) val add_locals_ret_declaration : t -> (Mangled.t * Sil.typ) list -> unit - (** restrict the cfg to the given enabled (active and not shadowed) procedures *) - val cfg_restrict_enabled : cfg -> DB.source_file -> Procname.Set.t option -> unit - (** Compare two nodes *) val compare : t -> t -> int diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 7938bbd26..6cbefb12f 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -27,9 +27,10 @@ let from_env_variable var_name = let _ = Sys.getenv var_name in true with Not_found -> false -let specs_dir_name = "specs" +let attributes_dir_name = "attributes" let captured_dir_name = "captured" let sources_dir_name = "sources" +let specs_dir_name = "specs" let default_in_zip_results_dir = "infer" diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index ac51d0568..3ddce96d4 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -52,7 +52,6 @@ type t = proc_map: file_data Procname.Hash.t; (** map from procedure name to file data *) file_map: (DB.source_file, file_data) Hashtbl.t; (** map from filaname to file data *) mutable active_opt : Procname.Set.t option; (** if not None, restrict the active procedures to the given set *) - mutable callees : Procname.Set.t; (** callees of active procedures *) mutable procs_defined_in_several_files : Procname.Set.t; (** Procedures defined in more than one file *) } @@ -68,7 +67,6 @@ let create procset_opt = proc_map = Procname.Hash.create 17; file_map = Hashtbl.create 17; active_opt = procset_opt; - callees = Procname.Set.empty; procs_defined_in_several_files = Procname.Set.empty; } @@ -84,26 +82,6 @@ let add_active_proc exe_env proc_name = | None -> () | Some procset -> exe_env.active_opt <- Some (Procname.Set.add proc_name procset) -(** Add a callee to the exe_env, and extend the file_map and proc_map. *) -let add_callee (exe_env: t) (source_file : DB.source_file) (pname: Procname.t) = - exe_env.callees <- Procname.Set.add pname exe_env.callees; - let file_data_opt = - try Some (Hashtbl.find exe_env.file_map source_file) - with Not_found -> - let source_dir = DB.source_dir_from_source_file source_file in - let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in - (match Cg.load_from_file cg_fname with - | None -> None - | Some cg -> - let nLOC = Cg.get_nLOC cg in - let file_data = new_file_data source_file nLOC cg_fname in - Some file_data) in - match file_data_opt with - | None -> () - | Some file_data -> - if (not (Procname.Hash.mem exe_env.proc_map pname)) - then Procname.Hash.replace exe_env.proc_map pname file_data - (** like add_cg, but use exclude_fun to determine files to be excluded *) let add_cg_exclude_fun (exe_env: t) (source_dir : DB.source_dir) exclude_fun = let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in @@ -160,8 +138,21 @@ let get_file_data exe_env pname = try Procname.Hash.find exe_env.proc_map pname with Not_found -> - L.err "can't find tenv_cfg_object for %a@." Procname.pp pname; - raise Not_found + begin + match AttributesTable.load_attributes pname with + | None -> + L.err "can't find tenv_cfg_object for %a@." Procname.pp pname; + raise Not_found + | Some proc_attributes -> + let loc = proc_attributes.ProcAttributes.loc in + let source_file = loc.Location.file in + let nLOC = loc.Location.nLOC in + let source_dir = DB.source_dir_from_source_file source_file in + let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in + let file_data = new_file_data source_file nLOC cg_fname in + Procname.Hash.replace exe_env.proc_map pname file_data; + file_data + end (** return the source file associated to the procedure *) let get_source exe_env pname = @@ -188,7 +179,7 @@ let procs_enabled exe_env source = let pset'' = Procname.Set.add proc_name pset' in res := Procname.Set.union pset'' !res in Procname.Set.iter do_pname pset; - Some (Procname.Set.union !res exe_env.callees) (* keep callees in the cfg *) + Some !res | None -> None let file_data_to_cfg exe_env file_data = @@ -199,7 +190,6 @@ let file_data_to_cfg exe_env file_data = L.err "Cannot find cfg for %s@." (DB.filename_to_string file_data.tenv_file); assert false | Some cfg -> cfg in - Cfg.Node.cfg_restrict_enabled cfg file_data.source (procs_enabled exe_env file_data.source); file_data.cfg <- Some cfg; cfg | Some cfg -> cfg diff --git a/infer/src/backend/exe_env.mli b/infer/src/backend/exe_env.mli index 6a0089d4a..680b5c1bf 100644 --- a/infer/src/backend/exe_env.mli +++ b/infer/src/backend/exe_env.mli @@ -24,9 +24,6 @@ val freeze : initial -> t (** create a new execution environment, given an optional set restricting the active procedures *) val create : Procname.Set.t option -> initial -(** Add a callee to the exe_env, and extend the file_map and proc_map. *) -val add_callee : t -> DB.source_file -> Procname.t -> unit - (** add call graph from the source dir in the spec db, with relative tenv and cfg, to the execution environment *) val add_cg : initial -> DB.source_dir -> Cg.t option diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index 32253643a..15b75bf22 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -58,7 +58,7 @@ let should_perform_transition gr proc_name : Procname.t list = (** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *) let transition_footprint_re_exe proc_name joined_pres = L.out "Transition %a from footprint to re-exe@." Procname.pp proc_name; - let summary = Specs.get_summary_unsafe proc_name in + let summary = Specs.get_summary_unsafe "transition_footprint_re_exe" proc_name in let summary' = if !Config.only_footprint then { summary with @@ -166,7 +166,7 @@ let trace = ref false let procs_become_done gr pname : Procname.t list = let recursive_dependents = Cg.get_recursive_dependents gr pname in let nonrecursive_dependents = Cg.get_nonrecursive_dependents gr pname in - let summary = Specs.get_summary_unsafe pname in + let summary = Specs.get_summary_unsafe "procs_become_done" pname in let is_done = Specs.get_timestamp summary <> 0 && (!Config.only_footprint || Specs.get_phase pname == Specs.RE_EXECUTION) && Procname.Set.for_all (proc_is_done gr) nonrecursive_dependents && @@ -184,7 +184,7 @@ let post_process_procs exe_env procs_done = let check_no_specs pn = if Specs.get_specs pn = [] then begin Errdesc.warning_err - (Specs.get_summary_unsafe pn).Specs.attributes.ProcAttributes.loc + (Specs.get_summary_unsafe "post_process_procs" pn).Specs.attributes.ProcAttributes.loc "No specs found for %a@." Procname.pp pn end in let cg = Exe_env.get_cg exe_env in @@ -305,7 +305,7 @@ end let main_algorithm exe_env analyze_proc filter_out process_result : unit = let call_graph = Exe_env.get_cg exe_env in let filter_initial (pname, w) = - let summary = Specs.get_summary_unsafe pname in + let summary = Specs.get_summary_unsafe "main_algorithm" pname in Specs.get_timestamp summary = 0 in wpnames_todo := WeightedPnameSet.filter filter_initial (compute_weighed_pnameset call_graph); let wpnames_address_of = (* subset of the procedures whose address is taken *) @@ -319,16 +319,19 @@ let main_algorithm exe_env analyze_proc filter_out process_result : unit = (* Return true if [pname] is not up to date and it can be analyzed right now *) Procname.Set.for_all (proc_is_done call_graph) (Cg.get_nonrecursive_dependents call_graph pname) && - (Specs.get_timestamp (Specs.get_summary_unsafe pname) = 0 + (Specs.get_timestamp (Specs.get_summary_unsafe "main_algorithm" pname) = 0 || not (proc_is_up_to_date call_graph pname)) in let process_one_proc pname (calls: Cg.in_out_calls) = DB.current_source := - (Specs.get_summary_unsafe pname).Specs.attributes.ProcAttributes.loc.Location.file; + (Specs.get_summary_unsafe "main_algorithm" pname) + .Specs.attributes.ProcAttributes.loc.Location.file; if !trace then begin let whole_seconds = false in L.err "@[ *********** Summary of %a ***********@," Procname.pp pname; - L.err "%a@]@\n" (Specs.pp_summary pe_text whole_seconds) (Specs.get_summary_unsafe pname) + L.err "%a@]@\n" + (Specs.pp_summary pe_text whole_seconds) + (Specs.get_summary_unsafe "main_algorithm" pname) end; if filter_out call_graph pname then @@ -376,7 +379,7 @@ let interprocedural_algorithm try _analyze_proc exe_env pname with | exn -> Reporting.log_error pname exn; - let prev_summary = Specs.get_summary_unsafe pname in + let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in let timestamp = max 1 (prev_summary.Specs.timestamp) in let stats = { prev_summary.Specs.stats with Specs.stats_timeout = true } in let summ = diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 27fa6c07f..922aae193 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -232,7 +232,7 @@ module Simulator = struct (** Simulate the analysis only *) let analyze_proc exe_env tenv proc_name = L.err "in analyze_proc %a@." Procname.pp proc_name; (* for i = 1 to Random.int 1000000 do () done; *) - let prev_summary = Specs.get_summary_unsafe proc_name in + let prev_summary = Specs.get_summary_unsafe "Simulator" proc_name in let timestamp = max 1 (prev_summary.Specs.timestamp) in { prev_summary with Specs.timestamp = timestamp } @@ -329,7 +329,7 @@ type cluster_elem = { ce_file : DB.source_file; ce_naprocs : int; (** number of active procedures defined in the file *) ce_active_procs : Procname.t list; (** list of active procedures *) - ce_source_map : DB.source_file Procname.Map.t; (** map from undefined procedures to the file where they are defined *) } + } (** cluster of files *) type cluster = @@ -385,7 +385,10 @@ let create_minimal_clusters file_cg exe_env to_analyze_map : cluster list = if !trace_clusters then L.err " [create_cluster_elem] %s@." (DB.source_file_to_string source_file); DB.current_source := source_file; match file_pname_to_cg file_pname with - | None -> { ce_file = source_file; ce_naprocs = 0; ce_active_procs = []; ce_source_map = Procname.Map.empty } + | None -> { + ce_file = source_file; + ce_naprocs = 0; + ce_active_procs = [];} | Some cg -> (* decide whether a proc is active using pname_to_fname, i.e. whether this is the file associated to it *) let proc_is_selected pname = match !select_proc with @@ -396,28 +399,14 @@ let create_minimal_clusters file_cg exe_env to_analyze_map : cluster list = DB.source_file_equal (Exe_env.get_source exe_env pname) source_file in let active_procs = list_filter proc_is_active (Procname.Set.elements changed_procs) in let naprocs = list_length active_procs in - let source_map = - let all_procs, _ = Cg.get_nodes_and_edges cg in - let mapr = ref Procname.Map.empty in - let do_proc (pn, isdefined) = - let extend_map proc_name = - try - let source = Exe_env.get_source exe_env proc_name in - mapr := Procname.Map.add proc_name source !mapr; - with Not_found -> () in - if isdefined && Procname.is_java pn then - let tenv = Exe_env.get_tenv exe_env pn in - (* Add the overridden methods, so they can be found by the cluster. *) - PatternMatch.proc_iter_overridden_methods extend_map tenv pn - else - (* Add the procedures that are called but not defined in the current file. *) - extend_map pn in - list_iter do_proc all_procs; - !mapr in total_files := !total_files + 1; total_procs := !total_procs + naprocs; total_LOC := !total_LOC + (Cg.get_nLOC cg); - { ce_file = source_file; ce_naprocs = naprocs; ce_active_procs = active_procs; ce_source_map = source_map } in + { + ce_file = source_file; + ce_naprocs = naprocs; + ce_active_procs = active_procs; + } in let choose_next_file list = (* choose next file from the weakly ordered list *) let file_has_no_unseen_dependents fname = Procname.Set.subset (Cg.get_dependents file_cg fname) !seen in @@ -468,17 +457,11 @@ let clusters_nfiles clusters = list_fold_left (fun n cluster -> cluster_nfiles c let clusters_naprocs clusters = list_fold_left (fun n cluster -> cluster_naprocs cluster + n) 0 clusters let print_clusters_stats clusters = - let pp_source_map_ce fmt cluster_elem = - let do_map_elem proc_name source_file = F.fprintf fmt "%s " (Procname.to_string proc_name) in - Procname.Map.iter do_map_elem cluster_elem.ce_source_map in - let pp_source_map fmt cluster = - list_iter (pp_source_map_ce fmt) cluster in let pp_cluster num cluster = - L.err "cluster #%d files: %d active procedures: %d source_map: %a@." + L.err "cluster #%d files: %d active procedures: %d@." num (cluster_nfiles cluster) - (cluster_naprocs cluster) - pp_source_map cluster in + (cluster_naprocs cluster) in let i = ref 0 in list_iter (fun cluster -> @@ -786,19 +769,13 @@ let compute_files_changed_map _exe_env (source_dirs : DB.source_dir list) exclud let exe_env_from_cluster cluster = let _exe_env = Exe_env.create (Some (cluster_to_active_procs cluster)) in let source_files, callees = - let fold_callees pn file callees = - (pn, file) :: callees in let fold_cluster_elem (source_files, callees) ce = - let callees = Procname.Map.fold fold_callees ce.ce_source_map callees in let source_files = DB.source_dir_from_source_file ce.ce_file :: source_files in source_files, callees in list_fold_left fold_cluster_elem ([], []) cluster in let sorted_files = list_sort DB.source_dir_compare source_files in list_iter (fun src_dir -> ignore(Exe_env.add_cg _exe_env src_dir)) sorted_files; let exe_env = Exe_env.freeze _exe_env in - let do_callee (pn, file) = - Exe_env.add_callee exe_env file pn in - list_iter do_callee callees; exe_env (** Analyze a cluster of files *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 98b7c3109..b2d7eed6d 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -530,7 +530,7 @@ let forward_tabulate cfg tenv = let sid_curr_node = Cfg.Node.get_id curr_node in let proc_desc = Cfg.Node.get_proc_desc curr_node in let proc_name = Cfg.Procdesc.get_proc_name proc_desc in - let summary = Specs.get_summary_unsafe proc_name in + let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in mark_visited summary curr_node; (* mark nodes visited in fp and re phases *) let session = incr summary.Specs.sessions; @@ -549,7 +549,7 @@ let forward_tabulate cfg tenv = Paths.PathSet.iter exe pathset in let log_string proc_name = let phase_string = (if Specs.get_phase proc_name == Specs.FOOTPRINT then "FP" else "RE") in - let summary = Specs.get_summary_unsafe proc_name in + let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in let timestamp = Specs.get_timestamp summary in F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in let doit () = @@ -879,7 +879,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t let start_node = Cfg.Procdesc.get_start_node pdesc in let check_recursion_level () = - let summary = Specs.get_summary_unsafe pname in + let summary = Specs.get_summary_unsafe "check_recursion_level" pname in let recursion_level = Specs.get_timestamp summary in if recursion_level > !Config.max_recursion then begin @@ -1105,7 +1105,7 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary = let res = Fork.Timeout.exe_timeout (Specs.get_iterations proc_name) go () in let specs = get_results () in let elapsed = Unix.gettimeofday () -. init_time in - let prev_summary = Specs.get_summary_unsafe proc_name in + let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in let updated_summary = update_summary prev_summary specs proc_name elapsed res in if (!Config.curr_language <> Config.Java && Config.report_assertion_failure) @@ -1182,7 +1182,8 @@ let check_skipped_procs procs_and_defined_children = let skipped_procs = ref Procname.Set.empty in let proc_check_skips (pname, dep) = let process_skip () = - let call_stats = (Specs.get_summary_unsafe pname).Specs.stats.Specs.call_stats in + let call_stats = + (Specs.get_summary_unsafe "check_skipped_procs" pname).Specs.stats.Specs.call_stats in let do_tr_elem pn = function | Specs.CallStats.CR_skip, _ -> skipped_procs := Procname.Set.add pn !skipped_procs @@ -1285,7 +1286,7 @@ let print_stats_cfg proc_shadowed proc_is_active cfg = if proc_shadowed proc_desc then L.out "print_stats: ignoring function %a which is also defined in another file@." Procname.pp proc_name else - let summary = Specs.get_summary_unsafe proc_name in + let summary = Specs.get_summary_unsafe "print_stats_cfg" proc_name in let stats = summary.Specs.stats in let err_log = summary.Specs.attributes.ProcAttributes.err_log in incr num_proc; diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 1cf72b22c..2ba7e0c3f 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -46,7 +46,7 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name = Specs.set_status proc_name Specs.ACTIVE in let postprocess () = - let summary = Specs.get_summary_unsafe proc_name in + let summary = Specs.get_summary_unsafe "ondemand" proc_name in let summary' = { summary with Specs.status = Specs.INACTIVE; @@ -96,7 +96,7 @@ let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name = (** Mark the return type @Nullable by modifying the spec. *) let proc_add_return_nullable curr_pname = - let summary = Specs.get_summary_unsafe curr_pname in + let summary = Specs.get_summary_unsafe "proc_add_return_nullable" curr_pname in let proc_attributes = Specs.get_attributes summary in let method_annotation = proc_attributes.ProcAttributes.method_annotation in let method_annotation' = Annotations.method_annotation_mark_return diff --git a/infer/src/backend/serialization.ml b/infer/src/backend/serialization.ml index 394f2a61e..3742f2e2a 100644 --- a/infer/src/backend/serialization.ml +++ b/infer/src/backend/serialization.ml @@ -19,7 +19,10 @@ type 'a serializer = (string -> 'a option) * (DB.filename -> 'a option) * (DB.fi type key = int (** current key for tenv, procedure summary, cfg, error trace, call graph *) -let tenv_key, summary_key, cfg_key, trace_key, cg_key, analysis_results_key, cluster_key = (425184201, 160179325, 1062389858, 221487792, 477305409, 799050016, 579094948) +let tenv_key, summary_key, cfg_key, trace_key, cg_key, + analysis_results_key, cluster_key, attributes_key = + 425184201, 160179325, 1062389858, 221487792, 477305409, + 799050016, 579094948, 972393003 (** version of the binary files, to be incremented for each change *) let version = 24 diff --git a/infer/src/backend/serialization.mli b/infer/src/backend/serialization.mli index dd30b89dd..9dd28884a 100644 --- a/infer/src/backend/serialization.mli +++ b/infer/src/backend/serialization.mli @@ -18,35 +18,39 @@ type 'a serializer (** Serialization key, used to distinguish versions of serializers and avoid assert faults *) type key -(** current key for tenv *) -val tenv_key : key +(** current key for an analysis results value *) +val analysis_results_key : key -(** current key for a procedure summary *) -val summary_key : key +(** current key for proc attributes *) +val attributes_key : key (** current key for a cfg *) val cfg_key : key -(** current key for an error trace *) -val trace_key : key - (** current key for a call graph *) val cg_key : key +(** create a serializer from a file name + given an integer key used as double-check of the file type *) +val create_serializer : key -> 'a serializer + (** current key for a cluster *) val cluster_key : key -(** current key for an analysis results value *) -val analysis_results_key : key - -(** create a serializer from a file name, given an integer key used as double-check of the file type *) -val create_serializer : key -> 'a serializer +(** extract a from_file function from a serializer *) +val from_file : 'a serializer -> DB.filename -> 'a option (** extract a from_string function from a serializer *) val from_string : 'a serializer -> string -> 'a option -(** extract a from_file function from a serializer *) -val from_file : 'a serializer -> DB.filename -> 'a option +(** current key for a procedure summary *) +val summary_key : key + +(** current key for tenv *) +val tenv_key : key (** extract a to_file function from a serializer *) val to_file : 'a serializer -> DB.filename -> 'a -> unit + +(** current key for an error trace *) +val trace_key : key diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 8c5b854b2..571323c7b 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -521,7 +521,8 @@ let specs_models_filename pname = let summary_exists_in_models pname = Sys.file_exists (DB.filename_to_string (specs_models_filename pname)) -let summary_serializer : summary Serialization.serializer = Serialization.create_serializer Serialization.summary_key +let summary_serializer : summary Serialization.serializer = + Serialization.create_serializer Serialization.summary_key (** Save summary for the procedure into the spec database *) let store_summary pname (summ: summary) = @@ -610,10 +611,11 @@ let get_summary proc_name = | Some (summary, _) -> Some summary | None -> None -let get_summary_unsafe proc_name = +let get_summary_unsafe s proc_name = match get_summary proc_name with | None -> - raise (Failure ("Specs.get_summary_unsafe: " ^ (Procname.to_string proc_name) ^ "Not_found")) + raise (Failure ( + "[" ^ s ^ "] Specs.get_summary_unsafe: " ^ (Procname.to_string proc_name) ^ "Not_found")) | Some summary -> summary (** Check if the procedure is from a library: @@ -625,17 +627,14 @@ let proc_is_library proc_attributes = | Some _ -> false else false -(** Try to find the attributes for a defined proc, by first looking at the procdesc - then looking at .specs files if required. - Return the attributes for an underfined procedure otherwise. +(** Try to find the attributes for a defined proc. + First look at specs (to get attributes computed by analysis) + then look at the attributes table. If no attributes can be found, return None. *) -let proc_resolve_attributes get_proc_desc proc_name = - let from_proc_desc () = match get_proc_desc proc_name with - | Some proc_desc -> - Some (Cfg.Procdesc.get_attributes proc_desc) - | None -> - None in +let proc_resolve_attributes proc_name = + let from_attributes_table () = + AttributesTable.load_attributes proc_name in let from_specs () = match get_summary proc_name with | Some summary -> Some summary.attributes @@ -645,23 +644,19 @@ let proc_resolve_attributes get_proc_desc proc_name = if attributes.ProcAttributes.is_defined then Some attributes else begin - match from_proc_desc () with + match from_attributes_table () with | Some attributes' -> Some attributes' | None -> Some attributes end | None -> - from_proc_desc () + from_attributes_table () (** Like proc_resolve_attributes but start from a proc_desc. *) let pdesc_resolve_attributes proc_desc = let proc_name = Cfg.Procdesc.get_proc_name proc_desc in - let get_proc_desc proc_name' = - if Procname.equal proc_name proc_name' - then Some proc_desc - else None in - match proc_resolve_attributes get_proc_desc proc_name with + match proc_resolve_attributes proc_name with | Some proc_attributes -> proc_attributes | None -> @@ -682,10 +677,10 @@ let get_status summary = summary.status let is_active proc_name = - get_status (get_summary_unsafe proc_name) = ACTIVE + get_status (get_summary_unsafe "is_active" proc_name) = ACTIVE let is_inactive proc_name = - get_status (get_summary_unsafe proc_name) = INACTIVE + get_status (get_summary_unsafe "is_active" proc_name) = INACTIVE let get_timestamp summary = summary.timestamp diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 0ae1f073d..e373a0eec 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -196,7 +196,7 @@ val get_specs_from_payload : summary -> Prop.normal spec list val get_summary : Procname.t -> summary option (** @deprecated Return the summary for the procedure name. Raises an exception when not found. *) -val get_summary_unsafe : Procname.t -> summary +val get_summary_unsafe : string -> Procname.t -> summary (** Return the current timestamp for the summary *) val get_timestamp : summary -> int @@ -249,13 +249,12 @@ val pp_summary : printenv -> bool -> Format.formatter -> summary -> unit (** Like proc_resolve_attributes but start from a proc_desc. *) val pdesc_resolve_attributes : Cfg.Procdesc.t -> ProcAttributes.t -(** Try to find the attributes for a defined proc, by first looking at the procdesc - then looking at .specs files if required. - Return the attributes for an underfined procedure otherwise. +(** Try to find the attributes for a defined proc. + First look at specs (to get attributes computed by analysis) + then look at the attributes table. If no attributes can be found, return None. *) -val proc_resolve_attributes : - (Procname.t -> Cfg.Procdesc.t option) -> Procname.t -> ProcAttributes.t option +val proc_resolve_attributes : Procname.t -> ProcAttributes.t option (** Check if the procedure is from a library: It's not defined, and there is no spec file for it. *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 19f0d947d..a940f9ab5 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1264,7 +1264,7 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop and sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop path actual_params callee_pname loc = - match Specs.proc_resolve_attributes (Cfg.Procdesc.find_from_name cfg) callee_pname with + match Specs.proc_resolve_attributes callee_pname with | None -> [(prop, path)] | Some callee_attributes -> diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index bef68ac3e..24c1d05b7 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -35,14 +35,14 @@ module ST = struct proc_flags_add summary.Specs.attributes.ProcAttributes.proc_flags key value let pname_add proc_name key value = - let summary = Specs.get_summary_unsafe proc_name in + let summary = Specs.get_summary_unsafe "ST.pname_add" proc_name in add summary key value let files_open = ref Procname.Set.empty let pname_find proc_name key = if Procname.Set.mem proc_name !files_open then - let summary = Specs.get_summary_unsafe proc_name in + let summary = Specs.get_summary_unsafe "ST.pname_find" proc_name in proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key else begin match Specs.get_summary proc_name with diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml index 34e801cc3..31d8c3ecd 100644 --- a/infer/src/checkers/codeQuery.ml +++ b/infer/src/checkers/codeQuery.ml @@ -37,7 +37,7 @@ let query_ast = module Err = struct (** Update the summary with stats from the checker. *) let update_summary proc_name proc_desc = - let old_summ = Specs.get_summary_unsafe proc_name in + let old_summ = Specs.get_summary_unsafe "codeQuery" proc_name in let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in let specs = let spec = diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml index fda2e434a..92d8dd8f9 100644 --- a/infer/src/checkers/eradicate.ml +++ b/infer/src/checkers/eradicate.ml @@ -51,23 +51,25 @@ module MkCallback struct (** Update the summary with stats from the checker. *) let update_summary proc_name proc_desc final_typestate_opt = - let old_summ = Specs.get_summary_unsafe proc_name in - let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in - let method_annotation = - (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in - let new_summ = - { - old_summ with - Specs.nodes = nodes; - Specs.payload = Extension.mkpayload final_typestate_opt; - Specs.attributes = + match Specs.get_summary proc_name with + | Some old_summ -> + let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in + let method_annotation = + (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.method_annotation in + let new_summ = { - old_summ.Specs.attributes with - ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc; - method_annotation; - }; - } in - Specs.add_summary proc_name new_summ + old_summ with + Specs.nodes = nodes; + Specs.payload = Extension.mkpayload final_typestate_opt; + Specs.attributes = + { + old_summ.Specs.attributes with + ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc; + method_annotation; + }; + } in + Specs.add_summary proc_name new_summ + | None -> () let callback1 find_canonical_duplicate calls_this checks get_proc_desc idenv tenv curr_pname @@ -185,18 +187,23 @@ struct let get_private_called (initializers : init list) : init list = let res = ref [] in let do_proc (init_pn, init_pd) = - let filter callee_pn callee_pd = + let filter callee_pn callee_attributes = let is_private = - let attr = Specs.pdesc_resolve_attributes callee_pd in - attr.ProcAttributes.access = Sil.Private in + callee_attributes.ProcAttributes.access = Sil.Private in let same_class = let get_class_opt pn = if Procname.is_java pn then Some (Procname.java_get_class pn) else None in get_class_opt init_pn = get_class_opt callee_pn in is_private && same_class in - let private_called = PatternMatch.proc_calls get_proc_desc init_pn init_pd filter in - res := private_called @ !res in + let private_called = PatternMatch.proc_calls + Specs.proc_resolve_attributes init_pn init_pd filter in + let do_called (callee_pn, callee_attributes) = + match get_proc_desc callee_pn with + | Some callee_pd -> + res := (callee_pn, callee_pd) :: !res + | None -> () in + list_iter do_called private_called in list_iter do_proc initializers; !res in @@ -233,29 +240,34 @@ struct list_rev !final_typestates let pname_and_pdescs_with f = - list_map - (fun n -> match get_proc_desc n with - | Some d -> [(n, d)] - | None -> []) - all_procs - |> list_flatten - |> list_filter f + let res = ref [] in + let filter pname = match Specs.proc_resolve_attributes pname with + | Some proc_attributes -> f (pname, proc_attributes) + | None -> false in + let do_proc pname = + if filter pname then + match get_proc_desc pname with + | Some pdesc -> + res := (pname, pdesc) :: !res + | None -> () in + list_iter do_proc all_procs; + list_rev !res (** Typestates after the current procedure and all initializer procedures. *) let final_initializer_typestates_lazy = lazy begin - let is_initializer pdesc pname = - PatternMatch.method_is_initializer tenv (Cfg.Procdesc.get_attributes pdesc) || + let is_initializer pname proc_attributes = + PatternMatch.method_is_initializer tenv proc_attributes || let ia, _ = - (Models.get_modelled_annotated_signature - (Cfg.Procdesc.get_attributes pdesc)).Annotations.ret in + (Models.get_modelled_annotated_signature proc_attributes).Annotations.ret in Annotations.ia_is_initializer ia in let initializers_current_class = pname_and_pdescs_with - (fun (pname, pdesc) -> - is_initializer pdesc pname && - Procname.java_get_class pname = Procname.java_get_class curr_pname) in - final_typestates ((curr_pname, curr_pdesc):: initializers_current_class) + (function (pname, proc_attributes) -> + is_initializer pname proc_attributes && + Procname.java_get_class pname = Procname.java_get_class curr_pname) in + final_typestates + ((curr_pname, curr_pdesc) :: initializers_current_class) end (** Typestates after all constructors. *) @@ -263,9 +275,9 @@ struct begin let constructors_current_class = pname_and_pdescs_with - (fun (n, d) -> - Procname.is_constructor n && - Procname.java_get_class n = Procname.java_get_class curr_pname) in + (fun (pname, proc_attributes) -> + Procname.is_constructor pname && + Procname.java_get_class pname = Procname.java_get_class curr_pname) in final_typestates constructors_current_class end diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml index 7fa35b1ed..4929c4245 100644 --- a/infer/src/checkers/eradicateChecks.ml +++ b/infer/src/checkers/eradicateChecks.ml @@ -536,7 +536,7 @@ let check_overridden_annotations ignore (list_fold_left2 compare initial_pos current_params overridden_params) in let check overriden_proc_name = - match Specs.proc_resolve_attributes get_proc_desc overriden_proc_name with + match Specs.proc_resolve_attributes overriden_proc_name with | Some attributes -> let overridden_signature = Models.get_modelled_annotated_signature attributes in check_return overriden_proc_name overridden_signature; diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index bbc1da7ad..fb6c81941 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -302,14 +302,15 @@ let java_get_vararg_values node pvar idenv pdesc = | None -> () in !values -let proc_calls get_proc_desc pname pdesc filter : (Procname.t * Cfg.Procdesc.t) list = +let proc_calls resolve_attributes pname pdesc filter : (Procname.t * ProcAttributes.t) list = let res = ref [] in let do_instruction node instr = match instr with | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _) -> begin - match get_proc_desc callee_pn with - | Some callee_pd -> - if filter callee_pn callee_pd then res := (callee_pn, callee_pd) :: !res + match resolve_attributes callee_pn with + | Some callee_attributes -> + if filter callee_pn callee_attributes then + res := (callee_pn, callee_attributes) :: !res | None -> () end | _ -> () in diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli index 5beb76434..9be3ae895 100644 --- a/infer/src/checkers/patternMatch.mli +++ b/infer/src/checkers/patternMatch.mli @@ -48,10 +48,12 @@ val java_get_vararg_values : Cfg.Node.t -> Sil.pvar -> Idenv.t -> Cfg.Procdesc.t val java_proc_name_with_class_method : Procname.t -> string -> string -> bool -(** [proc_calls get_proc_desc pn pd filter] returns the callees that satisfy [filter]. *) -val proc_calls : (Procname.t -> Cfg.Procdesc.t option) -> Procname.t -> Cfg.Procdesc.t -> - (Procname.t -> Cfg.Procdesc.t -> bool) -> - (Procname.t * Cfg.Procdesc.t) list +(** Return the callees that satisfy [filter]. *) +val proc_calls : + (Procname.t -> ProcAttributes.t option) -> + Procname.t -> Cfg.Procdesc.t -> + (Procname.t -> ProcAttributes.t -> bool) -> + (Procname.t * ProcAttributes.t) list (** Iterate over all the methods overridden by the procedure. Only Java supported at the moment. *) diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index b96dfa05f..05505c1f5 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -46,9 +46,8 @@ module ComplexExpressions = struct let procname_instanceof = Procname.equal SymExec.ModelBuiltins.__instanceof let procname_is_false_on_null get_proc_desc pn = - match get_proc_desc pn with - | Some pdesc -> - let proc_attributes = Specs.pdesc_resolve_attributes pdesc in + match Specs.proc_resolve_attributes pn with + | Some proc_attributes -> let annotated_signature = Models.get_modelled_annotated_signature proc_attributes in let ret_ann, _ = annotated_signature.Annotations.ret in @@ -58,9 +57,8 @@ module ComplexExpressions = struct let procname_is_true_on_null get_proc_desc pn = let annotated_true_on_null () = - match get_proc_desc pn with - | Some pdesc -> - let proc_attributes = Specs.pdesc_resolve_attributes pdesc in + match Specs.proc_resolve_attributes pn with + | Some proc_attributes -> let annotated_signature = Models.get_modelled_annotated_signature proc_attributes in let ret_ann, _ = annotated_signature.Annotations.ret in @@ -558,12 +556,12 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _) when SymExec.function_is_builtin pn -> typestate (* skip othe builtins *) | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags) - when get_proc_desc callee_pname <> None -> - Ondemand.do_analysis get_proc_desc curr_pname callee_pname; + when Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname <> None -> + if Ondemand.enabled () then + Ondemand.do_analysis get_proc_desc curr_pname callee_pname; let callee_attributes = - match get_proc_desc callee_pname with - | Some pdesc -> - Specs.pdesc_resolve_attributes pdesc + match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with + | Some proc_attributes -> proc_attributes | None -> assert false in let callee_loc = callee_attributes.ProcAttributes.loc in @@ -1003,7 +1001,7 @@ let typecheck_node let handle_exceptions typestate instr = match instr with | Sil.Call (_, Sil.Const (Sil.Cfun callee_pname), _, _, _) -> let callee_attributes_opt = - Specs.proc_resolve_attributes get_proc_desc callee_pname in + Specs.proc_resolve_attributes callee_pname in (* check if the call might throw an exception *) let has_exceptions = match callee_attributes_opt with | Some callee_attributes ->