[biabd] cache the list of modelled functions

Summary:
Instead of looking up each proc name in models/, pre-compute the list of
models and do lookups there instead of in the filesystem.

Reviewed By: ngorogiannis

Differential Revision: D16603148

fbshipit-source-id: 5eb534a14

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)

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 *)

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
+    ~summary_cache_hits ~summary_cache_misses ~ondemand_procs_analyzed ~ondemand_local_cache_hits
-    ~ondemand_local_cache_hits ~ondemand_local_cache_misses ~proc_locker_lock_time
+    ~ondemand_local_cache_misses ~proc_locker_lock_time ~proc_locker_unlock_time
-    ~proc_locker_unlock_time ~restart_scheduler_useful_time ~restart_scheduler_total_time
+    ~restart_scheduler_useful_time ~restart_scheduler_total_time ~scheduler_process_analysis_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)
+      ~summary_cache_misses:(pp_int_field stats f) ~ondemand_procs_analyzed:(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_procs_analyzed:create_counter ~ondemand_local_cache_hits:create_counter
-      ~ondemand_local_cache_hits:create_counter ~ondemand_local_cache_misses:create_counter
+      ~ondemand_local_cache_misses:create_counter ~proc_locker_lock_time:create_time_entry
-      ~proc_locker_lock_time:create_time_entry ~proc_locker_unlock_time:create_time_entry
+      ~proc_locker_unlock_time:create_time_entry ~restart_scheduler_useful_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

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

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 ;

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 *)
 

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

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) ;