diff --git a/infer/src/IR/Tenv.re b/infer/src/IR/Tenv.re index 7ff6aa864..f7ce17c60 100644 --- a/infer/src/IR/Tenv.re +++ b/infer/src/IR/Tenv.re @@ -143,12 +143,12 @@ let expand_type tenv typ => let tenv_serializer: Serialization.serializer t = Serialization.create_serializer Serialization.tenv_key; let global_tenv: Lazy.t (option t) = - lazy (Serialization.from_file tenv_serializer (DB.global_tenv_fname ())); + lazy (Serialization.from_file tenv_serializer DB.global_tenv_fname); /** Load a type environment from a file */ let load_from_file (filename: DB.filename) :option t => - if (filename == DB.global_tenv_fname ()) { + if (filename == DB.global_tenv_fname) { Lazy.force global_tenv } else { Serialization.from_file tenv_serializer filename diff --git a/infer/src/backend/DB.ml b/infer/src/backend/DB.ml index 95dc14f4e..afbb2732d 100644 --- a/infer/src/backend/DB.ml +++ b/infer/src/backend/DB.ml @@ -121,25 +121,24 @@ let source_dir_get_internal_file source_dir extension = let fname = source_dir_name ^ extension in Filename.concat source_dir fname -let captured_dir () = +let captured_dir = Filename.concat Config.results_dir Config.captured_dir_name -let sources_dir () = +let sources_dir = Filename.concat Config.results_dir Config.sources_dir_name (** get the source directory corresponding to a source file *) let source_dir_from_source_file source_file = - Filename.concat (captured_dir ()) (source_file_encoding source_file) + Filename.concat captured_dir (source_file_encoding source_file) (** get the path to the copy of the source file to be stored in the results directory *) let source_file_in_resdir source_file = - Filename.concat (sources_dir ()) (source_file_encoding source_file) + Filename.concat sources_dir (source_file_encoding source_file) (** Find the source directories in the results dir *) let find_source_dirs () = let source_dirs = ref [] in - let capt_dir = captured_dir () in - let files_in_results_dir = Array.to_list (Sys.readdir capt_dir) in + let files_in_results_dir = Array.to_list (Sys.readdir captured_dir) in let add_cg_files_from_dir dir = let files = Array.to_list (Sys.readdir dir) in IList.iter (fun fname -> @@ -147,7 +146,7 @@ let find_source_dirs () = if Filename.check_suffix path ".cg" then source_dirs := dir :: !source_dirs) files in IList.iter (fun fname -> - let dir = Filename.concat capt_dir fname in + let dir = Filename.concat captured_dir fname in if Sys.is_directory dir then add_cg_files_from_dir dir) files_in_results_dir; IList.rev !source_dirs @@ -303,12 +302,12 @@ module Results_dir = struct filename_from_base base path (** directory of spec files *) - let specs_dir () = path_to_filename Abs_root [Config.specs_dir_name] + let specs_dir = path_to_filename Abs_root [Config.specs_dir_name] (** initialize the results directory *) let init () = create_dir Config.results_dir; - create_dir (specs_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]); @@ -316,9 +315,8 @@ module Results_dir = struct create_dir (path_to_filename Abs_source_dir []) let clean_specs_dir () = - let specs_dir_path = specs_dir () in - create_dir specs_dir_path; (* create dir just in case it doesn't exist to avoid errors *) - let files_to_remove = Array.map (Filename.concat specs_dir_path) (Sys.readdir specs_dir_path) in + create_dir specs_dir; (* create dir just in case it doesn't exist to avoid errors *) + let files_to_remove = Array.map (Filename.concat specs_dir) (Sys.readdir specs_dir) in Array.iter Sys.remove files_to_remove (** create a file at the given path, creating any missing directories *) @@ -345,9 +343,9 @@ type origin = | Spec_lib | Models -let global_tenv_fname () = +let global_tenv_fname = let basename = Config.global_tenv_filename in - filename_concat (captured_dir ()) basename + filename_concat captured_dir basename let is_source_file path = IList.exists diff --git a/infer/src/backend/DB.mli b/infer/src/backend/DB.mli index b4ccb8334..282662f3b 100644 --- a/infer/src/backend/DB.mli +++ b/infer/src/backend/DB.mli @@ -51,7 +51,7 @@ module Results_dir : sig val path_to_filename : path_kind -> path -> filename (** directory of spec files *) - val specs_dir : unit -> filename + val specs_dir : filename (** Initialize the results directory *) val init : unit -> unit @@ -106,11 +106,6 @@ val source_file_to_string : source_file -> string (** convert a string obtained by source_file_to_string to a source file *) val source_file_from_string : string -> source_file -exception No_project_root - -(** get the project root when it exists or raise No_project_root otherwise *) -val project_root : unit -> string - (** get the full path of a source file, raise No_project_root exception when used with a relative source file and no project root specified *) val source_file_to_abs_path : source_file -> string @@ -125,7 +120,7 @@ type source_dir val source_dir_compare : source_dir -> source_dir -> int (** get the absolute path to the sources dir *) -val sources_dir : unit -> string +val sources_dir : string (** expose the source dir as a string *) val source_dir_to_string : source_dir -> string @@ -140,7 +135,7 @@ val source_dir_from_source_file : source_file -> source_dir val source_file_in_resdir : source_file -> filename (** directory where the results of the capture phase are stored *) -val captured_dir : unit -> filename +val captured_dir : filename (** create the directory containing the file bane *) val filename_create_dir : filename -> unit @@ -165,7 +160,7 @@ val read_file_with_lock : string -> string -> bytes option val update_file_with_lock : string -> string -> (bytes -> bytes) -> unit (** get the path of the global type environment (only used in Java) *) -val global_tenv_fname : unit -> filename +val global_tenv_fname : filename (** Check if a path is a Java, C, C++ or Objectve C source file according to the file extention *) val is_source_file: string -> bool diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index 54a0cece2..e884d3cd1 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -31,7 +31,7 @@ let tenv_filename file_base = if Sys.file_exists (DB.filename_to_string per_source_tenv_filename) then per_source_tenv_filename else - DB.global_tenv_fname () + DB.global_tenv_fname (** create a new file_data *) let new_file_data source nLOC cg_fname = diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index a9fc5c731..3edad6dec 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -36,7 +36,7 @@ let load_specfiles () = let all_filepaths = IList.map (fun fname -> Filename.concat dir fname) all_filenames in IList.filter is_specs_file all_filepaths in let specs_dirs = - let result_specs_dir = DB.filename_to_string (DB.Results_dir.specs_dir ()) in + let result_specs_dir = DB.filename_to_string DB.Results_dir.specs_dir in result_specs_dir :: Config.specs_library in IList.flatten (IList.map specs_files_in_dir specs_dirs) diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 530ba6593..0fa39eb44 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -195,8 +195,7 @@ let inhabit_call (procname, receiver) cfg env = let create_dummy_harness_file harness_name = let dummy_file_name = let dummy_file_dir = - let sources_dir = DB.sources_dir () in - if Sys.file_exists sources_dir then sources_dir + if Sys.file_exists DB.sources_dir then DB.sources_dir else Filename.get_temp_dir_name () in let file_str = Procname.java_get_class_name diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index 0498d006f..2c37839a4 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -92,35 +92,31 @@ let capture_libs linereader program tenv = (* load a stored global tenv if the file is found, and create a new one otherwise *) let load_tenv () = - let tenv_filename = DB.global_tenv_fname () in - let tenv = - if DB.file_exists tenv_filename then - begin - match Tenv.load_from_file tenv_filename with - | None -> - Tenv.create () - | Some _ when Config.analyze_models -> - let error_msg = - "Unexpected tenv file " - ^ (DB.filename_to_string tenv_filename) - ^ " found while generating the models" in - failwith error_msg - | Some tenv -> - tenv - end - else - Tenv.create () in - tenv + if DB.file_exists DB.global_tenv_fname then + begin + match Tenv.load_from_file DB.global_tenv_fname with + | None -> + Tenv.create () + | Some _ when Config.analyze_models -> + let error_msg = + "Unexpected tenv file " + ^ (DB.filename_to_string DB.global_tenv_fname) + ^ " found while generating the models" in + failwith error_msg + | Some tenv -> + tenv + end + else + Tenv.create () (* Store to a file the type environment containing all the types required to perform the analysis *) let save_tenv tenv = if not Config.analyze_models then JTransType.add_models_types tenv; - let tenv_filename = DB.global_tenv_fname () in (* TODO: this prevents per compilation step incremental analysis at this stage *) - if DB.file_exists tenv_filename then DB.file_remove tenv_filename; - JUtils.log "writing new tenv %s@." (DB.filename_to_string tenv_filename); - Tenv.store_to_file tenv_filename tenv + if DB.file_exists DB.global_tenv_fname then DB.file_remove DB.global_tenv_fname; + JUtils.log "writing new tenv %s@." (DB.filename_to_string DB.global_tenv_fname); + Tenv.store_to_file DB.global_tenv_fname tenv (* The program is loaded and translated *) diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index c0c6101da..24aa97480 100644 --- a/infer/src/llvm/lMain.ml +++ b/infer/src/llvm/lMain.ml @@ -44,9 +44,8 @@ let store_icfg cg cfg = end let store_tenv tenv = - let tenv_filename = DB.global_tenv_fname () in - if DB.file_exists tenv_filename then DB.file_remove tenv_filename; - Tenv.store_to_file tenv_filename tenv + if DB.file_exists DB.global_tenv_fname then DB.file_remove DB.global_tenv_fname; + Tenv.store_to_file DB.global_tenv_fname tenv let () = begin match Config.source_file with