[biabduction][models] move to sqlite

Summary:
Store model summaries in the `model_specs` database table instead of in spec files.

This table is populated when a new database is created by loading a dump of the `specs` table in the models database.  This avoids the perf and reliability implications of ATTACHing the same, non-read-only models-DB by many processes.

- `BiabductionModels` is moved into `IR` so that `JsonReports` can access it.
- The binary `sqlite3` is now required on the host compiling infer.

Reviewed By: skcho

Differential Revision: D23191601

fbshipit-source-id: 1532481ee

.gitignore

@@ -118,6 +118,7 @@ buck-out/
 /infer/models/java/models/
 /infer/models/models.jar
 /infer/lib/java/models.jar
+/infer/lib/models.sql
 /infer/models/java/bootclasspath
 /infer/models/c/out/
 /infer/models/cpp/out/

Makefile

@@ -432,7 +432,7 @@ clang_plugin_test_replace: clang_setup
 	)
 
 .PHONY: ocaml_unit_test
-ocaml_unit_test: src_build_common
+ocaml_unit_test: src_build_common infer_models
 	$(QUIET)$(call silent_on_success,Running OCaml unit tests,\
 	$(MAKE_SOURCE) unit)
 
@@ -639,8 +639,6 @@ endif
 	  $(MKDIR_P) '$(DESTDIR)$(libdir)/infer/infer/annotations/'
 	test -d      '$(DESTDIR)$(libdir)/infer/infer/lib/wrappers/' || \
 	  $(MKDIR_P) '$(DESTDIR)$(libdir)/infer/infer/lib/wrappers/'
-	test -d      '$(DESTDIR)$(libdir)/infer/infer/lib/specs/' || \
-	  $(MKDIR_P) '$(DESTDIR)$(libdir)/infer/infer/lib/specs/'
 	test -d      '$(DESTDIR)$(libdir)/infer/infer/bin/' || \
 	  $(MKDIR_P) '$(DESTDIR)$(libdir)/infer/infer/bin/'
 # copy files
@@ -661,8 +659,8 @@ ifeq ($(BUILD_C_ANALYZERS),yes)
 	  [ $(cc) -ef '$(INFER_BIN)' ] && \
 	  $(REMOVE) '$(notdir $(cc))' && \
 	  $(LN_S) ../../bin/infer '$(notdir $(cc))';))
-	find infer/lib/specs/* -print0 | xargs -0 -I \{\} \
+	$(INSTALL_DATA) -C          'infer/lib/models.sql' \
-	  $(INSTALL_DATA) -C \{\} '$(DESTDIR)$(libdir)'/infer/\{\}
+	  '$(DESTDIR)$(libdir)/infer/infer/lib/models.sql'
 	$(INSTALL_DATA) -C          'infer/lib/linter_rules/linters.al' \
 	  '$(DESTDIR)$(libdir)/infer/infer/lib/linter_rules/linters.al'
 	$(INSTALL_DATA) -C          'infer/etc/clang_ast.dict' \

Makefile.config

@@ -54,7 +54,6 @@ SRC_DIR = $(INFER_DIR)/src
 BUILD_DIR = $(INFER_DIR)/_build
 
 JAVA_LIB_DIR = $(LIB_DIR)/java
-SPECS_LIB_DIR = $(LIB_DIR)/specs
 
 INFER_BIN = $(BIN_DIR)/infer
 INFER_COMMANDS = \
@@ -90,7 +89,7 @@ JAVA_HOME=$(USER_JAVA_HOME)
 endif
 
 # marker to keep track of when models have been rebuilt
-MODELS_RESULTS_FILE = $(SPECS_LIB_DIR)/models
+MODELS_RESULTS_FILE = $(LIB_DIR)/models.sql
 
 ANDROID_JAR = $(LIB_DIR)/java/android/android-23.jar
 GUAVA_JAR = $(DEPENDENCIES_DIR)/java/guava/guava-23.0.jar

infer/models/Makefile

@@ -12,84 +12,64 @@ JAVA_MODELS_DIR = java
 OBJC_MODELS_DIR = objc/src
 OBJCPP_MODELS_DIR = objcpp/src
 
-CLANG_RESULTS_DIR = infer-out-clang
+RESULTS_DIR = infer-out
-CLANG_INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(CLANG_RESULTS_DIR) --biabduction-models-mode
+RESULTS_DB = $(RESULTS_DIR)/results.db
+INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(RESULTS_DIR) --biabduction-models-mode
 
 JAVA_MODELS_OUT = java/models
-JAVA_RESULTS_DIR = infer-out-java
-INFER_REPORT = $(JAVA_RESULTS_DIR)/report.json
 MODELS_JAR = models.jar
 
 JAVA_SOURCES = $(shell find $(JAVA_BUILTINS_DIR) $(JAVA_MODELS_DIR) -name "*.java")
+JAVA_MODELS_CLASSPATH = $(ANDROID_JAR):$(GUAVA_JAR):$(JACKSON_JAR):$(JSR_305_JAR):$(INFER_ANNOTATIONS_JAR)
+JAVAC_OPTIONS = -bootclasspath $(ANDROID_JAR) -d $(JAVA_MODELS_OUT) -classpath $(JAVA_MODELS_CLASSPATH) \
+	$(JAVA_SOURCES) -source 7 -target 7
+
+SQL_DUMP_MODEL_SPECS = \
+	-cmd ".mode insert model_specs" \
+	-cmd ".output $(MODELS_RESULTS_FILE)" \
+	-cmd "select * from specs order by proc_uid ;"
 
-MODELS_CLASSPATH = $(ANDROID_JAR):$(GUAVA_JAR):$(JACKSON_JAR):$(JSR_305_JAR):$(INFER_ANNOTATIONS_JAR)
 
 .PHONY: all
 all: $(MODELS_RESULTS_FILE)
 
-.PHONY: clean_specs
+capture:
-clean_specs:
-	$(REMOVE) $(SPECS_LIB_DIR)/*.specs $(MODELS_RESULTS_FILE)
-
-clang:
-	$(QUIET)$(REMOVE_DIR) $(CLANG_RESULTS_DIR)
-#	[make clean] each time to recompile all the models
 ifeq ($(BUILD_C_ANALYZERS),yes)
-	$(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean
-	$(QUIET)$(MAKE) -C $(CPP_MODELS_DIR) clean
-ifeq (yes, $(HAS_OBJC))
-	$(QUIET)$(MAKE) -C $(OBJC_MODELS_DIR) clean
-	$(QUIET)$(MAKE) -C $(OBJCPP_MODELS_DIR) clean
-endif
 	$(QUIET)$(call silent_on_success,Capturing C models,\
-	  $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(C_MODELS_DIR) all)
+	  $(INFER_BIN) capture $(INFER_OPTIONS) --continue -- $(MAKE) -C $(C_MODELS_DIR) all)
 	$(QUIET)$(call silent_on_success,Capturing C++ models,\
-	  $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(CPP_MODELS_DIR) all)
+	  $(INFER_BIN) capture $(INFER_OPTIONS) --continue -- $(MAKE) -C $(CPP_MODELS_DIR) all)
 ifeq (yes, $(HAS_OBJC))
 	$(QUIET)$(call silent_on_success,Capturing ObjCPP models,\
-	  $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJCPP_MODELS_DIR) all)
+	  $(INFER_BIN) capture $(INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJCPP_MODELS_DIR) all)
 	$(QUIET)$(call silent_on_success,Capturing ObjC models,\
-	  $(INFER_BIN) capture $(CLANG_INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJC_MODELS_DIR) all)
+	  $(INFER_BIN) capture $(INFER_OPTIONS) --continue -- $(MAKE) -C $(OBJC_MODELS_DIR) all)
 endif
 endif
-	$(QUIET)$(call silent_on_success,Analyzing clang models,\
+ifeq ($(BUILD_JAVA_ANALYZERS),yes)
-	  $(INFER_BIN) analyze $(CLANG_INFER_OPTIONS))
+	$(QUIET)$(REMOVE_DIR) $(JAVA_MODELS_OUT)
-	$(QUIET)$(INSTALL_DATA) $(CLANG_RESULTS_DIR)/specs/*.specs $(SPECS_LIB_DIR)
-
-.PHONY: java
-java:
-	$(QUIET)rm -fr $(JAVA_MODELS_OUT)
 	$(QUIET)$(MKDIR_P) $(JAVA_MODELS_OUT)
-	$(QUIET)rm -f $(JAVA_MODELS_JAR)
+	$(QUIET)$(REMOVE) $(JAVA_MODELS_JAR)
-	$(QUIET)$(call silent_on_success,Building Java models,\
+	$(QUIET)$(call silent_on_success,Capturing Java models,\
-	  $(INFER_BIN) --biabduction-only --results-dir $(JAVA_RESULTS_DIR) --biabduction-models-mode -- \
+	  $(INFER_BIN) --continue capture $(INFER_OPTIONS) -- $(JAVAC) $(JAVAC_OPTIONS))
-	  $(JAVAC) -bootclasspath $(ANDROID_JAR) -d $(JAVA_MODELS_OUT) -classpath $(MODELS_CLASSPATH) \
-	    $(JAVA_SOURCES) -source 7 -target 7)
 	cd $(JAVA_MODELS_OUT); jar cf ../../$(MODELS_JAR) *
-#	install .specs files into the models directory
-	$(QUIET)$(INSTALL_DATA) $(JAVA_RESULTS_DIR)/specs/*.specs $(SPECS_LIB_DIR)
 #	install the models.jar file too
 	$(INSTALL_DATA) -C $(MODELS_JAR) $(JAVA_MODELS_JAR)
 	$(QUIET)touch $(JAVA_MODELS_JAR)
-
-
-ALL_MODELS=
-ifeq ($(BUILD_C_ANALYZERS),yes)
-ALL_MODELS += clang
-endif
-ifeq ($(BUILD_JAVA_ANALYZERS),yes)
-ALL_MODELS += java
 endif
 
+
 # If the models deps have changed then the models need to be rebuilt. If infer itself has changed,
 # we need to nuke the previous specs files in case the serialization has changed, otherwise we might
 # encounter a segfault reading them.
 $(MODELS_RESULTS_FILE): $(MAKEFILE_LIST)
 #	clean first
-	$(MAKE) clean_specs
+	$(MAKE) clean
-#	build java and clang models in parallel
+#	no parallelism between clang and java; racing on creating the db with --continue doesn't work
-	$(MAKE) $(ALL_MODELS)
+	$(MAKE) capture
-	$(QUIET)touch $@
+	$(QUIET)$(call silent_on_success,Analyzing models,$(INFER_BIN) analyze $(INFER_OPTIONS))
+	sqlite3 $(RESULTS_DB) $(SQL_DUMP_MODEL_SPECS) </dev/null
+
 
 ifeq ($(BUILD_C_ANALYZERS),yes)
 $(MODELS_RESULTS_FILE): $(CLANG_DEPS_NO_MODELS)
@@ -99,14 +79,19 @@ $(MODELS_RESULTS_FILE): $(JAVA_DEPS_NO_MODELS) $(JAVA_SOURCES)
 endif
 
 .PHONY: clean
-clean: clean_specs
+clean:
+	$(QUIET)$(REMOVE) $(MODELS_RESULTS_FILE)
+	$(QUIET)$(REMOVE_DIR) $(RESULTS_DIR)
+ifeq ($(BUILD_C_ANALYZERS),yes)
 	$(QUIET)$(MAKE) -C $(C_MODELS_DIR) clean
 	$(QUIET)$(MAKE) -C $(CPP_MODELS_DIR) clean
 ifeq (yes, $(HAS_OBJC))
 	$(QUIET)$(MAKE) -C $(OBJC_MODELS_DIR) clean
 	$(QUIET)$(MAKE) -C $(OBJCPP_MODELS_DIR) clean
 endif
-	$(QUIET)rm -rf $(CLANG_RESULTS_DIR) $(JAVA_RESULTS_DIR)
+endif
-	$(QUIET)rm -rf $(JAVA_MODELS_OUT)
+ifeq ($(BUILD_JAVA_ANALYZERS),yes)
-	$(QUIET)rm -f $(MODELS_JAR)
+	$(QUIET)$(REMOVE_DIR) $(JAVA_MODELS_OUT)
-	$(QUIET)rm -f $(JAVA_MODELS_JAR)
+	$(QUIET)$(REMOVE) $(MODELS_JAR)
+	$(QUIET)$(REMOVE) $(JAVA_MODELS_JAR)
+endif

infer/src/IR/BiabductionModels.ml

@@ -0,0 +1,25 @@
+(*
+ * 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_model_proc_names () =
+  let db = ResultsDatabase.get_database () in
+  Sqlite3.prepare db "SELECT proc_uid FROM model_specs"
+  |> SqliteUtils.result_fold_single_column_rows db ~log:"scan model procnames"
+       ~init:String.Set.empty ~f:(fun acc proc_uid_sqlite ->
+         let[@warning "-8"] (Sqlite3.Data.TEXT proc_uid) = proc_uid_sqlite in
+         String.Set.add acc proc_uid )
+
+
+let models_index =
+  lazy (if Config.biabduction_models_mode then String.Set.empty else scan_model_proc_names ())
+
+
+let mem proc_name =
+  let proc_uid = Procname.to_unique_id proc_name in
+  String.Set.mem (Lazy.force models_index) proc_uid

infer/src/backend/Summary.ml

@@ -188,50 +188,43 @@ module OnDisk = struct
     Procname.Hash.replace cache proc_name summary
 
 
-  let specs_filename pname =
+  let spec_of_procname, spec_of_model =
-    let pname_file = Procname.to_filename pname in
+    (* both load queries must agree with these column numbers *)
-    pname_file ^ Config.specs_files_suffix
+    let analysis_summary_column = 0 in
-
+    let report_summary_column = 1 in
-
+    let load_spec ~load_statement proc_name =
-  (** Return the path to the .specs file for the given procedure in the current results directory *)
+      ResultsDatabase.with_registered_statement load_statement ~f:(fun db load_stmt ->
-  let specs_filename_of_procname pname =
+          Sqlite3.bind load_stmt 1 (Sqlite3.Data.TEXT (Procname.to_unique_id proc_name))
-    let filename = specs_filename pname in
+          |> SqliteUtils.check_result_code db ~log:"load proc specs bind proc_name" ;
-    DB.filename_from_string (ResultsDir.get_path Specs ^/ filename)
+          SqliteUtils.result_option ~finalize:false db ~log:"load proc specs run" load_stmt
-
+            ~read_row:(fun stmt ->
-
+              let analysis_summary =
-  (** paths to the .specs file for the given procedure in the models folder *)
+                Sqlite3.column stmt analysis_summary_column |> AnalysisSummary.SQLite.deserialize
-  let specs_models_filename pname =
+              in
-    DB.filename_from_string (Filename.concat Config.biabduction_models_dir (specs_filename pname))
+              let report_summary =
-
+                Sqlite3.column stmt report_summary_column |> ReportSummary.SQLite.deserialize
-
+              in
-  let summary_serializer : t Serialization.serializer =
+              mk_full_summary report_summary analysis_summary ) )
-    Serialization.create_serializer Serialization.Key.summary
+    in
-
-
-  (** Load procedure summary from the given file *)
-  let load_from_file specs_file =
-    BackendStats.incr_summary_file_try_load () ;
-    let opt = Serialization.read_from_file summary_serializer specs_file in
-    if Option.is_some opt then BackendStats.incr_summary_read_from_disk () ;
-    opt
-
-
-  let spec_of_model proc_name = load_from_file (specs_models_filename proc_name)
-
     let spec_of_procname =
       let load_statement =
         ResultsDatabase.register_statement
           "SELECT analysis_summary, report_summary FROM specs WHERE proc_uid = :k"
       in
       fun proc_name ->
-      ResultsDatabase.with_registered_statement load_statement ~f:(fun db stmt ->
+        BackendStats.incr_summary_file_try_load () ;
-          Sqlite3.bind stmt 1 (Sqlite3.Data.TEXT (Procname.to_unique_id proc_name))
+        let opt = load_spec ~load_statement proc_name in
-          |> SqliteUtils.check_result_code db ~log:"load proc specs bind proc_uid" ;
+        if Option.is_some opt then BackendStats.incr_summary_read_from_disk () ;
-          SqliteUtils.result_option ~finalize:false db ~log:"load proc specs run" stmt
+        opt
-            ~read_row:(fun stmt ->
+    in
-              let analysis_summary = Sqlite3.column stmt 0 |> AnalysisSummary.SQLite.deserialize in
+    let spec_of_model =
-              let report_summary = Sqlite3.column stmt 1 |> ReportSummary.SQLite.deserialize in
+      let load_statement =
-              mk_full_summary report_summary analysis_summary ) )
+        ResultsDatabase.register_statement
+          "SELECT analysis_summary, report_summary FROM model_specs WHERE proc_uid = :k"
+      in
+      fun proc_name -> load_spec ~load_statement proc_name
+    in
+    (spec_of_procname, spec_of_model)
 
 
   (** Load procedure summary for the given procedure name and update spec table *)
@@ -272,11 +265,6 @@ module OnDisk = struct
     let proc_name = get_proc_name summary in
     (* Make sure the summary in memory is identical to the saved one *)
     add proc_name summary ;
-    if Config.biabduction_models_mode then
-      Serialization.write_to_file summary_serializer
-        (specs_filename_of_procname proc_name)
-        ~data:summary
-    else
     let analysis_summary = AnalysisSummary.of_full_summary summary in
     let report_summary = ReportSummary.of_full_summary summary in
     DBWriter.store_spec ~proc_uid:(Procname.to_unique_id proc_name)
@@ -313,11 +301,7 @@ module OnDisk = struct
 
   let delete pname =
     remove_from_cache pname ;
-    if Config.biabduction_models_mode then
+    DBWriter.delete_spec ~proc_uid:(Procname.to_unique_id pname)
-      let filename = specs_filename_of_procname pname |> DB.filename_to_string in
-      (* Unix_error is raised if the file isn't present so do nothing in this case *)
-      try Unix.unlink filename with Unix.Unix_error _ -> ()
-    else DBWriter.delete_spec ~proc_uid:(Procname.to_unique_id pname)
 
 
   let iter_filtered_specs ~filter ~f =

infer/src/base/Config.ml

@@ -188,8 +188,6 @@ let source_file_extentions = [".java"; ".m"; ".mm"; ".c"; ".cc"; ".cpp"; ".h"]
 
 let kotlin_source_extension = ".kt"
 
-let specs_files_suffix = ".specs"
-
 (** Enable detailed tracing information during array abstraction *)
 let trace_absarray = false
 
@@ -330,17 +328,11 @@ let lib_dir = bin_dir ^/ Filename.parent_dir_name ^/ "lib"
 
 let etc_dir = bin_dir ^/ Filename.parent_dir_name ^/ "etc"
 
-(** Path to lib/specs to retrieve the default models *)
+(** Path to the database dump with model summaries *)
-let biabduction_models_dir = lib_dir ^/ "specs"
+let biabduction_models_sql = lib_dir ^/ "models.sql"
 
 let biabduction_models_jar = lib_dir ^/ "java" ^/ "models.jar"
 
-let biabduction_models_src_dir =
-  let root = Unix.getcwd () in
-  let dir = bin_dir ^/ Filename.parent_dir_name ^/ "models" in
-  Utils.filename_to_absolute ~root dir
-
-
 (* Normalize the path *)
 
 let linters_def_dir = lib_dir ^/ "linter_rules"

infer/src/base/Config.mli

@@ -43,12 +43,10 @@ val append_buck_flavors : string list
 
 val assign : string
 
-val biabduction_models_dir : string
+val biabduction_models_sql : string
 
 val biabduction_models_jar : string
 
-val biabduction_models_src_dir : string
-
 val bin_dir : string
 
 val bound_error_allowed_in_procedure_call : bool
@@ -134,8 +132,6 @@ val sourcepath : string option
 
 val sources : string list
 
-val specs_files_suffix : string
-
 val trace_absarray : bool
 
 val unsafe_unret : string

infer/src/base/ResultsDatabase.ml

@@ -12,6 +12,8 @@ module L = Logging
 let results_dir_get_path entry = ResultsDirEntryName.get_path ~results_dir:Config.results_dir entry
 
 let procedures_schema prefix =
+  (* it would be nice to use "WITHOUT ROWID" here but ancient versions of sqlite do not support
+     it *)
   Printf.sprintf
     {|
       CREATE TABLE IF NOT EXISTS %sprocedures
@@ -53,13 +55,14 @@ let specs_schema prefix =
     prefix
 
 
+let model_specs_schema prefix = specs_schema (prefix ^ "model_")
+
 let schema_hum =
-  String.concat ~sep:";\n" [procedures_schema ""; source_files_schema ""; specs_schema ""]
+  String.concat ~sep:";\n"
+    [procedures_schema ""; source_files_schema ""; specs_schema ""; model_specs_schema ""]
 
 
 let create_procedures_table ~prefix db =
-  (* it would be nice to use "WITHOUT ROWID" here but ancient versions of sqlite do not support
-     it *)
   SqliteUtils.exec db ~log:"creating procedures table" ~stmt:(procedures_schema prefix)
 
 
@@ -67,14 +70,28 @@ let create_source_files_table ~prefix db =
   SqliteUtils.exec db ~log:"creating source_files table" ~stmt:(source_files_schema prefix)
 
 
-let create_specs_table ~prefix db =
+let create_specs_tables ~prefix db =
-  SqliteUtils.exec db ~log:"creating specs table" ~stmt:(specs_schema prefix)
+  SqliteUtils.exec db ~log:"creating specs table" ~stmt:(specs_schema prefix) ;
+  SqliteUtils.exec db ~log:"creating model specs table" ~stmt:(model_specs_schema prefix)
 
 
 let create_tables ?(prefix = "") db =
   create_procedures_table ~prefix db ;
   create_source_files_table ~prefix db ;
-  create_specs_table ~prefix db
+  create_specs_tables ~prefix db
+
+
+let load_model_specs db =
+  if not Config.biabduction_models_mode then
+    try
+      let time0 = Mtime_clock.counter () in
+      SqliteUtils.exec db ~log:"begin transaction" ~stmt:"BEGIN IMMEDIATE TRANSACTION" ;
+      Utils.with_file_in Config.biabduction_models_sql
+        ~f:(In_channel.iter_lines ~f:(fun stmt -> SqliteUtils.exec db ~log:"load models" ~stmt)) ;
+      SqliteUtils.exec db ~log:"commit transaction" ~stmt:"COMMIT" ;
+      L.debug Capture Quiet "Loading models took %a@." Mtime.Span.pp (Mtime_clock.count time0)
+    with Sys_error _ ->
+      L.die ExternalError "Could not load model file %s@." Config.biabduction_models_sql
 
 
 let create_db () =
@@ -92,6 +109,8 @@ let create_db () =
   | Some _ ->
       (* Can't use WAL with custom VFS *)
       () ) ;
+  (* load biabduction models *)
+  load_model_specs db ;
   SqliteUtils.db_close db ;
   try Sys.rename temp_db (results_dir_get_path CaptureDB)
   with Sys_error _ -> (* lost the race, doesn't matter *) ()

infer/src/base/ResultsDir.ml

@@ -80,24 +80,10 @@ module RunState = struct
     store ()
 end
 
-let results_dir_dir_markers = [get_path Specs]
-
 let is_results_dir ~check_correct_version () =
-  let not_found = ref "" in
   let capture_db_path = get_path CaptureDB in
-  let has_all_markers =
+  let has_all_markers = (not check_correct_version) || Sys.is_file capture_db_path = `Yes in
-    List.for_all results_dir_dir_markers ~f:(fun d ->
+  Result.ok_if_true has_all_markers ~error:(Printf.sprintf "'%s' not found" capture_db_path)
-        Sys.is_directory d = `Yes
-        ||
-        ( not_found := d ^ "/" ;
-          false ) )
-    && ( (not check_correct_version)
-       || Sys.is_file capture_db_path = `Yes
-       ||
-       ( not_found := capture_db_path ;
-         false ) )
-  in
-  Result.ok_if_true has_all_markers ~error:(Printf.sprintf "'%s' not found" !not_found)
 
 
 let non_empty_directory_exists results_dir =
@@ -137,7 +123,6 @@ let create_results_dir () =
              L.die UserError "ERROR: %s@\nPlease remove '%s' and try again" error Config.results_dir ) ;
   Unix.mkdir_p Config.results_dir ;
   Unix.mkdir_p (get_path Temporary) ;
-  Unix.mkdir_p (get_path Specs) ;
   prepare_logging_and_db () ;
   ()
 

infer/src/base/ResultsDirEntryName.ml

@@ -32,7 +32,6 @@ type id =
   | ReportXML
   | RetainCycles
   | RunState
-  | Specs
   | StarvationIssues
   | Temporary
   | TestDeterminatorReport
@@ -163,11 +162,6 @@ let of_id = function
       ; kind= File
       ; before_incremental_analysis= Keep
       ; before_caching_capture= Delete }
-  | Specs ->
-      { rel_path= "specs"
-      ; kind= Directory
-      ; before_incremental_analysis= Keep
-      ; before_caching_capture= Delete }
   | StarvationIssues ->
       { rel_path= "starvation_issues"
       ; kind= IssuesDirectory

infer/src/base/ResultsDirEntryName.mli

@@ -33,7 +33,6 @@ type id =
   | ReportXML  (** a PMD-style XML version of [report.json] *)
   | RetainCycles  (** directory of retain cycles dotty files *)
   | RunState  (** internal data about the last infer run *)
-  | Specs  (** directory containing summaries as .specs files *)
   | StarvationIssues  (** directory of issues reported by the starvation analysis *)
   | Temporary  (** directory containing temp files *)
   | TestDeterminatorReport  (** the report produced by the test determinator capture mode *)

infer/src/base/Serialization.ml

@@ -22,10 +22,7 @@ module Key = struct
 
   (** Current keys for various serializable objects. The keys are computed using the [generate_keys]
       function below *)
-  let tenv, summary, issues =
+  let tenv, issues = ({name= "tenv"; key= 425184201}, {name= "issues"; key= 852343110})
-    ( {name= "tenv"; key= 425184201}
-    , {name= "summary"; key= 160179325}
-    , {name= "issues"; key= 852343110} )
 end
 
 (** version of the binary files, to be incremented for each change *)

infer/src/base/Serialization.mli

@@ -17,9 +17,6 @@ module Key : sig
   val issues : t
   (** current key for lint issues *)
 
-  val summary : t
-  (** current key for a procedure summary *)
-
   val tenv : t
   (** current key for tenv *)
 end

infer/src/base/SourceFile.ml

@@ -13,10 +13,7 @@ type t =
   | Invalid of {ml_source_file: string}
   | Absolute of string
   | RelativeProjectRoot of string  (** relative to project root *)
-  | RelativeInferBiabductionModel of string  (** relative to infer models *)
+[@@deriving compare, equal]
-[@@deriving compare]
-
-let equal = [%compare.equal: t]
 
 module OrderedSourceFile = struct
   type nonrec t = t [@@deriving compare]
@@ -39,7 +36,6 @@ let from_abs_path ?(warn_on_error = true) fname =
   (* try to get realpath of source file. Use original if it fails *)
   let fname_real = try Utils.realpath ~warn_on_error fname with Unix.Unix_error _ -> fname in
   let project_root_real = Utils.realpath ~warn_on_error Config.project_root in
-  let models_dir_real = Config.biabduction_models_src_dir in
   match
     Utils.filename_to_relative ~backtrack:Config.relative_path_backtrack ~root:project_root_real
       fname_real
@@ -48,13 +44,9 @@ let from_abs_path ?(warn_on_error = true) fname =
       RelativeProjectRoot path
   | None when Config.buck_cache_mode && Filename.check_suffix fname_real "java" ->
       L.(die InternalError) "%s is not relative to %s" fname_real project_root_real
-  | None -> (
-    match Utils.filename_to_relative ~root:models_dir_real fname_real with
-    | Some path ->
-        RelativeInferBiabductionModel path
   | None ->
       (* fname_real is absolute already *)
-        Absolute fname_real )
+      Absolute fname_real
 
 
 let to_string =
@@ -63,8 +55,6 @@ let to_string =
     match fname with
     | Invalid {ml_source_file} ->
         "DUMMY from " ^ ml_source_file
-    | RelativeInferBiabductionModel path ->
-        "INFER_MODEL/" ^ path
     | RelativeProjectRoot path ->
         path
     | Absolute path ->
@@ -84,8 +74,6 @@ let to_abs_path fname =
         "cannot be called with Invalid source file originating in %s" ml_source_file
   | RelativeProjectRoot path ->
       Filename.concat Config.project_root path
-  | RelativeInferBiabductionModel path ->
-      Filename.concat Config.biabduction_models_src_dir path
   | Absolute path ->
       path
 
@@ -96,22 +84,12 @@ let invalid ml_source_file = Invalid {ml_source_file}
 
 let is_invalid = function Invalid _ -> true | _ -> false
 
-let is_biabduction_model source_file =
-  match source_file with
-  | Invalid {ml_source_file} ->
-      L.(die InternalError) "cannot be called with Invalid source file from %s" ml_source_file
-  | RelativeProjectRoot _ | Absolute _ ->
-      false
-  | RelativeInferBiabductionModel _ ->
-      true
-
-
 let is_under_project_root = function
   | Invalid {ml_source_file} ->
       L.(die InternalError) "cannot be called with Invalid source file from %s" ml_source_file
   | RelativeProjectRoot _ ->
       true
-  | Absolute _ | RelativeInferBiabductionModel _ ->
+  | Absolute _ ->
       false
 
 

infer/src/base/SourceFile.mli

@@ -39,8 +39,6 @@ val create : ?warn_on_error:bool -> string -> t
     WARNING: If warn_on_error is false, no warning will be shown whenever an error occurs for the
     given path (e.g. if it does not exist). *)
 
-val is_biabduction_model : t -> bool
-
 val is_under_project_root : t -> bool
 (** Returns true if the file is in project root *)
 

infer/src/biabduction/BiabductionModels.ml

@@ -1,34 +0,0 @@
-(*
- * 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/integration/JsonReports.ml

@@ -158,13 +158,12 @@ module JsonIssuePrinter = MakeJsonListPrinter (struct
       L.(die InternalError)
         "Invalid source file for %a %a@.Trace: %a@." IssueType.pp err_key.issue_type
         Localise.pp_error_desc err_key.err_desc Errlog.pp_loc_trace err_data.loc_trace ;
-    let should_report_source_file =
+    let should_report_proc_name =
-      (not (SourceFile.is_biabduction_model source_file))
+      Config.debug_mode || Config.debug_exceptions || not (BiabductionModels.mem proc_name)
-      || Config.debug_mode || Config.debug_exceptions
     in
     if
       error_filter source_file err_key.issue_type
-      && should_report_source_file
+      && should_report_proc_name
       && should_report err_key.issue_type err_key.err_desc
     then
       let severity = IssueType.string_of_severity err_key.severity in