Lazily load summaries from zip files

Reviewed By: sblackshear

Differential Revision: D3269015

fb-gh-sync-id: 19d0438
fbshipit-source-id: 19d0438
master
Jeremy Dubreil 9 years ago committed by Facebook Github Bot 1
parent 0cda42fc90
commit a352c0ffa8

@ -209,6 +209,17 @@ let filename_create_dir fname =
if not (Sys.file_exists dirname) if not (Sys.file_exists dirname)
then create_dir dirname then create_dir dirname
let rec create_path path =
try
Unix.mkdir path 0o700
with
| Unix.Unix_error (Unix.EEXIST, _, _) -> ()
| Unix.Unix_error (Unix.ENOENT, _, _) ->
create_path (Filename.dirname path);
create_path path
let read_whole_file fd = let read_whole_file fd =
let stats = Unix.fstat fd in let stats = Unix.fstat fd in
let size = stats.Unix.st_size in let size = stats.Unix.st_size in
@ -328,6 +339,12 @@ module Results_dir = struct
Unix.openfile full_fname [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o777 Unix.openfile full_fname [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o777
end end
(** origin of a analysis artifact: current results dir, a spec library, or models *)
type origin =
| Res_dir
| Spec_lib
| Models
let global_tenv_fname () = let global_tenv_fname () =
let basename = Config.global_tenv_filename in let basename = Config.global_tenv_filename in
filename_concat (captured_dir ()) basename filename_concat (captured_dir ()) basename

@ -63,6 +63,12 @@ module Results_dir : sig
val create_file : path_kind -> path -> Unix.file_descr val create_file : path_kind -> path -> Unix.file_descr
end end
(** origin of a analysis artifact: current results dir, a spec library, or models *)
type origin =
| Res_dir
| Spec_lib
| Models
(** {2 Source Files} *) (** {2 Source Files} *)
type source_file type source_file
@ -145,6 +151,10 @@ val find_source_dirs : unit -> source_dir list
(** create a directory if it does not exist already *) (** create a directory if it does not exist already *)
val create_dir : string -> unit val create_dir : string -> unit
(** [make_directory path] will create a directory [path] creating all the
sub directories if non-existing *)
val create_path : string -> unit
(** Read a file using a lock to allow write attempts in parallel. *) (** Read a file using a lock to allow write attempts in parallel. *)
val read_file_with_lock : string -> string -> bytes option val read_file_with_lock : string -> string -> bytes option

@ -72,9 +72,10 @@ let models_dir =
let string_crc_hex32 s = let string_crc_hex32 s =
Digest.to_hex (Digest.string s) Digest.to_hex (Digest.string s)
let infer_cache : string option ref = ref None
module JarCache = module JarCache =
struct struct
let infer_cache : string option ref = ref None
let mkdir s = let mkdir s =
try try
@ -108,7 +109,7 @@ end
type zip_library = { type zip_library = {
zip_filename: string; zip_filename: string;
zip_channel: Zip.in_file; zip_channel: Zip.in_file Lazy.t;
models: bool; models: bool;
} }
@ -116,22 +117,26 @@ let zip_filename zip_library =
zip_library.zip_filename zip_library.zip_filename
let zip_channel zip_library = let zip_channel zip_library =
zip_library.zip_channel Lazy.force zip_library.zip_channel
let is_models zip_library =
zip_library.models
(** list of the zip files to search for specs files *) (** list of the zip files to search for specs files *)
let zip_libraries : zip_library list ref = ref [] let zip_libraries : zip_library list ref = ref []
let zip_models : zip_library list ref = ref [] let zip_models : zip_library list ref = ref []
let use_jar_cache = from_env_variable "INFER_USE_JAR_CACHE"
let add_zip_library zip_filename = let add_zip_library zip_filename =
if !JarCache.infer_cache != None if !infer_cache != None && use_jar_cache then
then
JarCache.handle_jar zip_filename JarCache.handle_jar zip_filename
else else
(* The order matters, the jar files should be added following the order *) (* The order matters, the jar files should be added following the order *)
(* specs files should be searched in them *) (* specs files should be searched in them *)
let zip_library = { let zip_library = {
zip_filename = zip_filename; zip_filename = zip_filename;
zip_channel = Zip.open_in zip_filename; zip_channel = lazy (Zip.open_in zip_filename);
models = false models = false
} in } in
zip_libraries := zip_library :: !zip_libraries zip_libraries := zip_library :: !zip_libraries
@ -139,7 +144,7 @@ let add_zip_library zip_filename =
let add_models zip_filename = let add_models zip_filename =
let zip_library = { let zip_library = {
zip_filename = zip_filename; zip_filename = zip_filename;
zip_channel = Zip.open_in zip_filename; zip_channel = lazy (Zip.open_in zip_filename);
models = true models = true
} in } in
zip_models := zip_library :: !zip_models zip_models := zip_library :: !zip_models

@ -334,13 +334,7 @@ type summary =
attributes : ProcAttributes.t; (** Attributes of the procedure *) attributes : ProcAttributes.t; (** Attributes of the procedure *)
} }
(** origin of a summary: current results dir, a spec library, or models *) type spec_tbl = (summary * DB.origin) Procname.Hash.t
type origin =
| Res_dir
| Spec_lib
| Models
type spec_tbl = (summary * origin) Procname.Hash.t
let spec_tbl: spec_tbl = Procname.Hash.create 128 let spec_tbl: spec_tbl = Procname.Hash.create 128
@ -505,13 +499,13 @@ let summary_compact sh summary =
let set_summary_origin proc_name summary origin = let set_summary_origin proc_name summary origin =
Procname.Hash.replace spec_tbl proc_name (summary, origin) Procname.Hash.replace spec_tbl proc_name (summary, origin)
let add_summary_origin (proc_name : Procname.t) (summary: summary) (origin: origin) : unit = let add_summary_origin (proc_name : Procname.t) (summary: summary) (origin: DB.origin) : unit =
L.out "Adding summary for %a@\n@[<v 2> %a@]@." Procname.pp proc_name (pp_summary pe_text false) summary; L.out "Adding summary for %a@\n@[<v 2> %a@]@." Procname.pp proc_name (pp_summary pe_text false) summary;
set_summary_origin proc_name summary origin set_summary_origin proc_name summary origin
(** Add the summary to the table for the given function *) (** Add the summary to the table for the given function *)
let add_summary (proc_name : Procname.t) (summary: summary) : unit = let add_summary (proc_name : Procname.t) (summary: summary) : unit =
add_summary_origin proc_name summary Res_dir add_summary_origin proc_name summary DB.Res_dir
let specs_filename pname = let specs_filename pname =
let pname_file = Procname.to_filename pname in let pname_file = Procname.to_filename pname in
@ -560,22 +554,6 @@ let store_summary pname (summ: summary) =
let load_summary specs_file = let load_summary specs_file =
Serialization.from_file summary_serializer specs_file Serialization.from_file summary_serializer specs_file
(** Load procedure summary from the given zip file *)
(* TODO: instead of always going through the same list for zip files for every proc_name, *)
(* create beforehand a map from specs filenames to zip filenames, so that looking up the specs for a given procedure is fast *)
let load_summary_from_zip zip_specs_path zip_channel =
let found_summary =
try
let entry = Zip.find_entry zip_channel zip_specs_path in
begin
match Serialization.from_string summary_serializer (Zip.read_entry zip_channel entry) with
| Some summ -> Some summ
| None ->
L.err "Could not load specs datastructure from %s@." zip_specs_path;
None
end
with Not_found -> None in
found_summary
(** Load procedure summary for the given procedure name and update spec table *) (** Load procedure summary for the given procedure name and update spec table *)
let load_summary_to_spec_table proc_name = let load_summary_to_spec_table proc_name =
@ -585,7 +563,7 @@ let load_summary_to_spec_table proc_name =
let load_summary_models models_dir = let load_summary_models models_dir =
match load_summary models_dir with match load_summary models_dir with
| None -> false | None -> false
| Some summ -> add summ Models in | Some summ -> add summ DB.Models in
let rec load_summary_libs = function (* try to load the summary from a list of libs *) let rec load_summary_libs = function (* try to load the summary from a list of libs *)
| [] -> false | [] -> false
| spec_path :: spec_paths -> | spec_path :: spec_paths ->
@ -593,31 +571,20 @@ let load_summary_to_spec_table proc_name =
| None -> load_summary_libs spec_paths | None -> load_summary_libs spec_paths
| Some summ -> | Some summ ->
add summ Spec_lib) in add summ Spec_lib) in
let rec load_summary_ziplibs zip_libraries = (* try to load the summary from a list of zip libraries *) let load_summary_ziplibs zip_specs_filename =
let zip_specs_filename = specs_filename proc_name in let zip_specs_path = Filename.concat Config.specs_dir_name zip_specs_filename in
let zip_specs_path = match ZipLib.load summary_serializer zip_specs_path with
let root = Filename.concat Config.default_in_zip_results_dir Config.specs_dir_name in | None -> false
Filename.concat root zip_specs_filename in | Some (summary, origin) -> add summary origin in
match zip_libraries with
| [] -> false
| zip_library:: zip_libraries ->
begin
match load_summary_from_zip zip_specs_path (Config.zip_channel zip_library) with
| None -> load_summary_ziplibs zip_libraries
| Some summ ->
let origin = if zip_library.Config.models then Models else Spec_lib in
add summ origin
end in
let default_spec_dir = res_dir_specs_filename proc_name in let default_spec_dir = res_dir_specs_filename proc_name in
match load_summary default_spec_dir with match load_summary default_spec_dir with
| None -> | None ->
(* search on models, libzips, and libs *) (* search on models, libzips, and libs *)
if load_summary_models (specs_models_filename proc_name) then true load_summary_models (specs_models_filename proc_name) ||
else if load_summary_ziplibs (Config.get_zip_libraries ()) then true load_summary_ziplibs (specs_filename proc_name) ||
else load_summary_libs (specs_library_filenames proc_name) load_summary_libs (specs_library_filenames proc_name)
| Some summ -> | Some summ ->
add summ Res_dir add summ DB.Res_dir
let rec get_summary_origin proc_name = let rec get_summary_origin proc_name =
try try
@ -687,7 +654,7 @@ let pdesc_resolve_attributes proc_desc =
let get_origin proc_name = let get_origin proc_name =
match get_summary_origin proc_name with match get_summary_origin proc_name with
| Some (_, origin) -> origin | Some (_, origin) -> origin
| None -> Res_dir | None -> DB.Res_dir
let summary_exists proc_name = let summary_exists proc_name =
match get_summary proc_name with match get_summary proc_name with
@ -806,7 +773,7 @@ let init_summary
{ proc_attributes with { proc_attributes with
ProcAttributes.proc_flags = proc_flags; }; ProcAttributes.proc_flags = proc_flags; };
} in } in
Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, Res_dir) Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, DB.Res_dir)
(** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *) (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
let reset_summary call_graph proc_name attributes_opt = let reset_summary call_graph proc_name attributes_opt =

@ -147,12 +147,6 @@ type summary =
attributes : ProcAttributes.t; (** Attributes of the procedure *) attributes : ProcAttributes.t; (** Attributes of the procedure *)
} }
(** origin of a summary: current results dir, a spec library, or models *)
type origin =
| Res_dir
| Spec_lib
| Models
(** Add the summary to the table for the given function *) (** Add the summary to the table for the given function *)
val add_summary : Procname.t -> summary -> unit val add_summary : Procname.t -> summary -> unit
@ -184,7 +178,7 @@ val get_flag : Procname.t -> string -> string option
val get_phase : Procname.t -> phase val get_phase : Procname.t -> phase
(** Return the origin of the spec file *) (** Return the origin of the spec file *)
val get_origin: Procname.t -> origin val get_origin: Procname.t -> DB.origin
(** Return the signature of a procedure declaration as a string *) (** Return the signature of a procedure declaration as a string *)
val get_signature : summary -> string val get_signature : summary -> string

@ -664,7 +664,7 @@ let prop_set_exn pname prop se_exn =
(** Include a subtrace for a procedure call if the callee is not a model. *) (** Include a subtrace for a procedure call if the callee is not a model. *)
let include_subtrace callee_pname = let include_subtrace callee_pname =
Specs.get_origin callee_pname <> Specs.Models Specs.get_origin callee_pname <> DB.Models
(** combine the spec's post with a splitting and actual precondition *) (** combine the spec's post with a splitting and actual precondition *)
let combine let combine

@ -520,7 +520,7 @@ let base_arg_desc =
"root directory of the project"; "root directory of the project";
"-infer_cache", "-infer_cache",
Arg.String (fun s -> Config.JarCache.infer_cache := Some (filename_to_absolute s)), Arg.String (fun s -> Config.infer_cache := Some (filename_to_absolute s)),
Some "dir", Some "dir",
"Select a directory to contain the infer cache"; "Select a directory to contain the infer cache";

@ -0,0 +1,65 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! Utils
module L = Logging
let get_cache_dir infer_cache zip_filename =
let basename = Filename.basename zip_filename in
let key = basename ^ string_crc_hex32 zip_filename in
Filename.concat infer_cache key
let load_from_cache serializer zip_path cache_dir zip_library =
let absolute_path = Filename.concat cache_dir zip_path in
let deserialize = Serialization.from_file serializer in
let extract to_path =
if not (Sys.file_exists to_path) then
begin
DB.create_path (Filename.dirname to_path);
let zip_channel = Config.zip_channel zip_library in
let entry = Zip.find_entry zip_channel zip_path in
Zip.copy_entry_to_file zip_channel entry to_path
end;
DB.filename_from_string to_path in
match deserialize (extract absolute_path) with
| Some data when Config.is_models zip_library -> Some (data, DB.Models)
| Some data -> Some (data, DB.Spec_lib)
| None -> None
| exception Not_found -> None
let load_from_zip serializer zip_path zip_library =
let zip_channel = Config.zip_channel zip_library in
let deserialize = Serialization.from_string serializer in
match deserialize (Zip.read_entry zip_channel (Zip.find_entry zip_channel zip_path)) with
| Some data when Config.is_models zip_library -> Some (data, DB.Models)
| Some data -> Some (data, DB.Spec_lib)
| None -> None
| exception Not_found -> None
let load_data serializer path zip_library =
let zip_path = Filename.concat Config.default_in_zip_results_dir path in
match !Config.infer_cache with
| None ->
load_from_zip serializer zip_path zip_library
| Some infer_cache ->
let cache_dir = get_cache_dir infer_cache (Config.zip_filename zip_library) in
load_from_cache serializer zip_path cache_dir zip_library
(* Search path in the list of zip libraries and use a cache directory to save already
deserialized data *)
let load serializer path =
let rec loop = function
| [] -> None
| zip_library :: other_libraries ->
let opt = load_data serializer path zip_library in
if Option.is_some opt then opt
else loop other_libraries in
loop (Config.get_zip_libraries ())

@ -0,0 +1,13 @@
(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
(** [load serializer path] searches for the file at the given path in the zip libraries.
If Config.infer_cache is set, already deserialized data will be saved there and [path]
will be searched from the cache first. *)
val load : 'a Serialization.serializer -> string -> ('a * DB.origin) option
Loading…
Cancel
Save