diff --git a/infer/src/IR/BiabductionModels.ml b/infer/src/IR/BiabductionModels.ml new file mode 100644 index 000000000..53bff3021 --- /dev/null +++ b/infer/src/IR/BiabductionModels.ml @@ -0,0 +1,33 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +let scan_models () = + let rec next_entry index dir = + match Unix.readdir_opt dir with + | None -> + Unix.closedir dir ; index + | Some entry -> ( + match String.chop_suffix entry ~suffix:Config.specs_files_suffix with + | Some file_proc_name -> + next_entry (String.Set.add index file_proc_name) dir + | None -> + next_entry index dir ) + in + match Unix.opendir Config.biabduction_models_dir with + | dir -> + next_entry String.Set.empty dir + | exception Unix.Unix_error ((ENOTDIR | ENOENT), _, _) -> + String.Set.empty + + +let models_index = + lazy (if not Config.biabduction_models_mode then scan_models () else String.Set.empty) + + +let mem proc_name = String.Set.mem (Lazy.force models_index) (Procname.to_filename proc_name) diff --git a/infer/src/IR/BiabductionModels.mli b/infer/src/IR/BiabductionModels.mli new file mode 100644 index 000000000..6f2ecbdee --- /dev/null +++ b/infer/src/IR/BiabductionModels.mli @@ -0,0 +1,11 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +val mem : Procname.t -> bool +(** Check if a summary for a given procedure exists in the models directory *) diff --git a/infer/src/backend/BackendStats.ml b/infer/src/backend/BackendStats.ml index 9b78d6b0c..8f770e932 100644 --- a/infer/src/backend/BackendStats.ml +++ b/infer/src/backend/BackendStats.ml @@ -17,7 +17,6 @@ include struct ; mutable summary_read_from_disk: int ; mutable summary_cache_hits: int ; mutable summary_cache_misses: int - ; mutable summary_has_model_queries: int ; mutable ondemand_procs_analyzed: int ; mutable ondemand_local_cache_hits: int ; mutable ondemand_local_cache_misses: int @@ -39,7 +38,6 @@ let global_stats = ; summary_read_from_disk= 0 ; summary_cache_hits= 0 ; summary_cache_misses= 0 - ; summary_has_model_queries= 0 ; ondemand_procs_analyzed= 0 ; ondemand_local_cache_hits= 0 ; ondemand_local_cache_misses= 0 @@ -72,8 +70,6 @@ let incr_summary_cache_hits () = incr Fields.summary_cache_hits let incr_summary_cache_misses () = incr Fields.summary_cache_misses -let incr_summary_has_model_queries () = incr Fields.summary_has_model_queries - let incr_ondemand_procs_analyzed () = incr Fields.ondemand_procs_analyzed let incr_ondemand_local_cache_hits () = incr Fields.ondemand_local_cache_hits @@ -106,7 +102,6 @@ let copy from ~into : unit = ; summary_read_from_disk ; summary_cache_hits ; summary_cache_misses - ; summary_has_model_queries ; ondemand_procs_analyzed ; ondemand_local_cache_hits ; ondemand_local_cache_misses @@ -118,10 +113,9 @@ let copy from ~into : unit = from in Fields.Direct.set_all_mutable_fields into ~summary_file_try_load ~summary_read_from_disk - ~summary_cache_hits ~summary_cache_misses ~summary_has_model_queries ~ondemand_procs_analyzed - ~ondemand_local_cache_hits ~ondemand_local_cache_misses ~proc_locker_lock_time - ~proc_locker_unlock_time ~restart_scheduler_useful_time ~restart_scheduler_total_time - ~scheduler_process_analysis_time + ~summary_cache_hits ~summary_cache_misses ~ondemand_procs_analyzed ~ondemand_local_cache_hits + ~ondemand_local_cache_misses ~proc_locker_lock_time ~proc_locker_unlock_time + ~restart_scheduler_useful_time ~restart_scheduler_total_time ~scheduler_process_analysis_time let merge stats1 stats2 = @@ -129,7 +123,6 @@ let merge stats1 stats2 = ; summary_read_from_disk= stats1.summary_read_from_disk + stats2.summary_read_from_disk ; summary_cache_hits= stats1.summary_cache_hits + stats2.summary_cache_hits ; summary_cache_misses= stats1.summary_cache_misses + stats2.summary_cache_misses - ; summary_has_model_queries= stats1.summary_has_model_queries + stats2.summary_has_model_queries ; ondemand_procs_analyzed= stats1.ondemand_procs_analyzed + stats2.ondemand_procs_analyzed ; ondemand_local_cache_hits= stats1.ondemand_local_cache_hits + stats2.ondemand_local_cache_hits ; ondemand_local_cache_misses= @@ -151,7 +144,6 @@ let initial = ; summary_read_from_disk= 0 ; summary_cache_hits= 0 ; summary_cache_misses= 0 - ; summary_has_model_queries= 0 ; ondemand_procs_analyzed= 0 ; ondemand_local_cache_hits= 0 ; ondemand_local_cache_misses= 0 @@ -186,8 +178,7 @@ let pp f stats = Fields.iter ~summary_file_try_load:(pp_int_field stats f) ~summary_read_from_disk:(pp_int_field stats f) ~summary_cache_hits:(pp_cache_hits stats stats.summary_cache_misses f) - ~summary_cache_misses:(pp_int_field stats f) ~summary_has_model_queries:(pp_int_field stats f) - ~ondemand_procs_analyzed:(pp_int_field stats f) + ~summary_cache_misses:(pp_int_field stats f) ~ondemand_procs_analyzed:(pp_int_field stats f) ~ondemand_local_cache_hits:(pp_cache_hits stats stats.ondemand_local_cache_misses f) ~ondemand_local_cache_misses:(pp_int_field stats f) ~proc_locker_lock_time:(pp_execution_duration_field stats f) @@ -219,10 +210,9 @@ let log_to_scuba stats = let entries = Fields.to_list ~summary_file_try_load:create_counter ~summary_read_from_disk:create_counter ~summary_cache_hits:create_counter ~summary_cache_misses:create_counter - ~summary_has_model_queries:create_counter ~ondemand_procs_analyzed:create_counter - ~ondemand_local_cache_hits:create_counter ~ondemand_local_cache_misses:create_counter - ~proc_locker_lock_time:create_time_entry ~proc_locker_unlock_time:create_time_entry - ~restart_scheduler_useful_time:create_time_entry + ~ondemand_procs_analyzed:create_counter ~ondemand_local_cache_hits:create_counter + ~ondemand_local_cache_misses:create_counter ~proc_locker_lock_time:create_time_entry + ~proc_locker_unlock_time:create_time_entry ~restart_scheduler_useful_time:create_time_entry ~restart_scheduler_total_time:create_time_entry ~scheduler_process_analysis_time:create_time_entry |> List.concat diff --git a/infer/src/backend/BackendStats.mli b/infer/src/backend/BackendStats.mli index d9ddac63a..2d2cb4b53 100644 --- a/infer/src/backend/BackendStats.mli +++ b/infer/src/backend/BackendStats.mli @@ -22,9 +22,6 @@ val incr_summary_cache_hits : unit -> unit val incr_summary_cache_misses : unit -> unit -val incr_summary_has_model_queries : unit -> unit -(** someone asked if a proc name has a biabduction model *) - val incr_ondemand_procs_analyzed : unit -> unit val incr_ondemand_local_cache_hits : unit -> unit diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index d146261d1..fe0cdd335 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -117,8 +117,6 @@ let pp_html source fmt summary = module OnDisk = struct - open PolyVariantEqual - type cache = t Procname.Hash.t let cache : cache = Procname.Hash.create 128 @@ -148,11 +146,6 @@ module OnDisk = struct DB.filename_from_string (Filename.concat Config.biabduction_models_dir (specs_filename pname)) - let has_model pname = - BackendStats.incr_summary_has_model_queries () ; - Sys.file_exists (DB.filename_to_string (specs_models_filename pname)) = `Yes - - let summary_serializer : t Serialization.serializer = Serialization.create_serializer Serialization.Key.summary @@ -165,6 +158,11 @@ module OnDisk = struct opt + let load_biabduction_model proc_name = + if BiabductionModels.mem proc_name then load_from_file (specs_models_filename proc_name) + else None + + (** Load procedure summary for the given procedure name and update spec table *) let load_summary_to_spec_table = let load_summary_ziplibs zip_specs_filename = @@ -177,7 +175,7 @@ module OnDisk = struct fun proc_name -> let summ_opt = load_from_file (specs_filename_of_procname proc_name) - |> or_from load_from_file specs_models_filename proc_name + |> or_from load_biabduction_model Fn.id proc_name |> or_from load_summary_ziplibs specs_filename proc_name in Option.iter ~f:(add proc_name) summ_opt ; diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index cc27da35c..1023ff996 100644 --- a/infer/src/backend/Summary.mli +++ b/infer/src/backend/Summary.mli @@ -70,9 +70,6 @@ val pp_text : Format.formatter -> t -> unit (** Print the summary in text format *) module OnDisk : sig - val has_model : Procname.t -> bool - (** Check if a summary for a given procedure exists in the models directory *) - val clear_cache : unit -> unit (** Remove all the elements from the cache of summaries *) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 2dd890e11..4c0af61d7 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -509,7 +509,7 @@ let method_exists right_proc_name methods = | Some attrs -> attrs.ProcAttributes.is_defined | None -> - Summary.OnDisk.has_model right_proc_name + BiabductionModels.mem right_proc_name let resolve_method tenv class_name proc_name = @@ -1108,7 +1108,7 @@ let resolve_and_analyze_clang current_summary tenv prop_r n_actual_params callee (* to be extended to other methods *) then try - let has_clang_model = Summary.OnDisk.has_model callee_pname in + let has_clang_model = BiabductionModels.mem callee_pname in let resolve_and_analyze_result = resolve_and_analyze tenv ~caller_summary:current_summary ~has_clang_model prop_r n_actual_params callee_pname call_flags diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index 519cc3f78..06875f710 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -13,10 +13,6 @@ module F = Format module L = Logging module CFrontend_decl_funct (T : CModule_type.CTranslation) : CModule_type.CFrontend = struct - let model_exists procname = - (not Config.biabduction_models_mode) && Summary.OnDisk.has_model procname - - (** Translates the method/function's body into nodes of the cfg. *) let add_method ?(is_destructor_wrapper = false) trans_unit_ctx tenv cfg class_decl_opt procname body ms has_return_param outer_context_opt extra_instrs = @@ -35,7 +31,7 @@ module CFrontend_decl_funct (T : CModule_type.CTranslation) : CModule_type.CFron in let f () = match Procname.Hash.find_opt cfg procname with - | Some procdesc when Procdesc.is_defined procdesc && not (model_exists procname) -> + | Some procdesc when Procdesc.is_defined procdesc && not (BiabductionModels.mem procname) -> L.(debug Capture Verbose) "@\n@\n>>---------- Start translating body of function: '%s' ---------<<@\n@." (Procname.to_string procname) ;