From cae160cccf4c1e81b81cf303449e9a1e9ce89273 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 14 Apr 2020 06:48:26 -0700 Subject: [PATCH] [infer-out][5/9] migrate "specs" Summary: Another entry to practice adding entries to ResultsDirEntryName. Reviewed By: skcho Differential Revision: D20894299 fbshipit-source-id: 9c387e0f3 --- infer/src/backend/Summary.ml | 3 +-- infer/src/base/Config.ml | 4 +--- infer/src/base/Config.mli | 2 -- infer/src/base/DB.ml | 2 +- infer/src/base/ResultsDir.ml | 6 +++--- infer/src/base/ResultsDirEntryName.ml | 7 ++++++- infer/src/base/ResultsDirEntryName.mli | 4 +++- 7 files changed, 15 insertions(+), 13 deletions(-) diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 949cc7c7b..6f8775f43 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -137,8 +137,7 @@ module OnDisk = struct (** Return the path to the .specs file for the given procedure in the current results directory *) let specs_filename_of_procname pname = - DB.Results_dir.path_to_filename DB.Results_dir.Abs_root - [Config.specs_dir_name; specs_filename pname] + DB.filename_from_string (ResultsDir.get_path Specs ^/ specs_filename pname) (** paths to the .specs file for the given procedure in the models folder *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 3c1e48db6..8936b85a0 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -220,8 +220,6 @@ let smt_output = false let source_file_extentions = [".java"; ".m"; ".mm"; ".c"; ".cc"; ".cpp"; ".h"] -let specs_dir_name = "specs" - let specs_files_suffix = ".specs" let starvation_issues_dir_name = "starvation_issues" @@ -369,7 +367,7 @@ 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 *) -let biabduction_models_dir = lib_dir ^/ specs_dir_name +let biabduction_models_dir = lib_dir ^/ "specs" let biabduction_models_jar = lib_dir ^/ "java" ^/ "models.jar" diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 7276f0cdc..1955dc451 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -159,8 +159,6 @@ val sourcepath : string option val sources : string list -val specs_dir_name : string - val specs_files_suffix : string val starvation_issues_dir_name : string diff --git a/infer/src/base/DB.ml b/infer/src/base/DB.ml index 57eed2654..c72d24dcc 100644 --- a/infer/src/base/DB.ml +++ b/infer/src/base/DB.ml @@ -126,7 +126,7 @@ module Results_dir = struct (** directory of spec files *) - let specs_dir = path_to_filename Abs_root [Config.specs_dir_name] + let specs_dir = ResultsDir.get_path Specs (** initialize the results directory *) let init ?(debug = false) source = diff --git a/infer/src/base/ResultsDir.ml b/infer/src/base/ResultsDir.ml index 8fb151ada..472e8ca56 100644 --- a/infer/src/base/ResultsDir.ml +++ b/infer/src/base/ResultsDir.ml @@ -81,7 +81,7 @@ module RunState = struct store () end -let results_dir_dir_markers = [Config.results_dir ^/ Config.specs_dir_name] +let results_dir_dir_markers = [get_path Specs] let is_results_dir ~check_correct_version () = let not_found = ref "" in @@ -109,7 +109,7 @@ let non_empty_directory_exists results_dir = let remove_results_dir () = if non_empty_directory_exists Config.results_dir then ( - if not Config.force_delete_results_dir then + if (not Config.buck) && not Config.force_delete_results_dir then Result.iter_error (is_results_dir ~check_correct_version:false ()) ~f:(fun err -> L.(die UserError) "ERROR: '%s' exists but does not seem to be an infer results directory: %s@\n\ @@ -138,7 +138,7 @@ let create_results_dir () = ) ; Unix.mkdir_p Config.results_dir ; Unix.mkdir_p (get_path Temporary) ; - List.iter ~f:Unix.mkdir_p results_dir_dir_markers ; + Unix.mkdir_p (get_path Specs) ; prepare_logging_and_db () ; () diff --git a/infer/src/base/ResultsDirEntryName.ml b/infer/src/base/ResultsDirEntryName.ml index 589f9e410..1929b4068 100644 --- a/infer/src/base/ResultsDirEntryName.ml +++ b/infer/src/base/ResultsDirEntryName.ml @@ -6,7 +6,7 @@ *) open! IStd -type id = Temporary [@@deriving enumerate] +type id = Specs | Temporary [@@deriving enumerate] type cleanup_action = Delete | Keep [@@deriving equal] @@ -22,6 +22,11 @@ type t = e.g., a distributed Buck cache. *) } let of_id = function + | Specs -> + { rel_path= "specs" + ; kind= Directory + ; before_incremental_analysis= Keep + ; before_caching_capture= Delete } | Temporary -> { rel_path= "tmp" ; kind= Directory diff --git a/infer/src/base/ResultsDirEntryName.mli b/infer/src/base/ResultsDirEntryName.mli index 004cab723..6c7a11640 100644 --- a/infer/src/base/ResultsDirEntryName.mli +++ b/infer/src/base/ResultsDirEntryName.mli @@ -9,7 +9,9 @@ open! IStd (** Entries in the results directory (infer-out/). Unless you want to specify a custom results directory you probably want to use {!ResultsDir.Entry} instead of this module. *) -type id = Temporary (** directory containing temp files *) +type id = + | Specs (** directory containing summaries as .specs files *) + | Temporary (** directory containing temp files *) val get_path : results_dir:string -> id -> string (** the absolute path for the given entry *)