diff --git a/infer/src/java/jClasspath.ml b/infer/src/java/jClasspath.ml index cbc5573ba..00eeec284 100644 --- a/infer/src/java/jClasspath.ml +++ b/infer/src/java/jClasspath.ml @@ -7,39 +7,12 @@ *) open! IStd -open PolyVariantEqual open Javalib_pack module L = Logging (** version of Javalib.get_class that does not spam stderr *) let javalib_get_class = Utils.suppress_stderr2 Javalib.get_class -let models_specs_filenames = ref String.Set.empty - -let models_jar = ref "" - -let collect_specs_filenames jar_filename = - let zip_channel = Zip.open_in jar_filename in - let collect set e = - let filename = e.Zip.filename in - if not (Filename.check_suffix filename Config.specs_files_suffix) then set - else - let proc_filename = Filename.chop_extension (Filename.basename filename) in - String.Set.add set proc_filename - in - models_specs_filenames := - List.fold ~f:collect ~init:!models_specs_filenames (Zip.entries zip_channel) ; - Zip.close_in zip_channel - - -let add_models jar_filename = - models_jar := jar_filename ; - if Sys.file_exists !models_jar = `Yes then collect_specs_filenames jar_filename - else L.(die InternalError) "Java model file not found" - - -let is_model procname = String.Set.mem !models_specs_filenames (Procname.to_filename procname) - let split_classpath = String.split ~on:JFile.sep let classpath_of_paths paths = @@ -308,8 +281,8 @@ let collect_classes start_classmap jar_filename = let load_program classpath classes = L.(debug Capture Medium) "loading program ... %!" ; let models = - if String.equal !models_jar "" then JBasics.ClassMap.empty - else collect_classes JBasics.ClassMap.empty !models_jar + JModels.get_models_jar_filename () + |> Option.fold ~init:JBasics.ClassMap.empty ~f:collect_classes in let program = { classpath= {path= classpath; channel= Javalib.class_path classpath} diff --git a/infer/src/java/jClasspath.mli b/infer/src/java/jClasspath.mli index 559e64a2f..bd3daa824 100644 --- a/infer/src/java/jClasspath.mli +++ b/infer/src/java/jClasspath.mli @@ -9,13 +9,6 @@ open! IStd open Javalib_pack -val add_models : string -> unit -(** Adds the set of procnames for the models of Java libraries so that methods with similar names - are skipped during the capture *) - -val is_model : Procname.t -> bool -(** Check if there is a model for the given procname *) - (** map entry for source files with potential basename collision within the same compiler call *) type file_entry = Singleton of SourceFile.t | Duplicate of (string * SourceFile.t) list diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index f89ccc588..7b6b6b1eb 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -141,7 +141,7 @@ let create_icfg source_file program tenv icfg cn node = let translate m = let proc_name = JTransType.translate_method_name program tenv m in JClasspath.set_callee_translated program proc_name ; - if JClasspath.is_model proc_name then + if JModels.is_model proc_name then (* do not translate the method if there is a model for it *) L.debug Capture Verbose "Skipping method with a model: %a@." Procname.pp proc_name else diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index aa8338538..b6fd735d1 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -120,7 +120,7 @@ let main load_sources_and_classes = | true, true -> L.(die UserError) "Not expecting model file when analyzing the models" | false, true -> - JClasspath.add_models Config.biabduction_models_jar ) ; + JModels.set_models ~jar_filename:Config.biabduction_models_jar ) ; JBasics.set_permissive true ; let classpath, sources, classes = match load_sources_and_classes with diff --git a/infer/src/java/jModels.ml b/infer/src/java/jModels.ml new file mode 100644 index 000000000..69c640076 --- /dev/null +++ b/infer/src/java/jModels.ml @@ -0,0 +1,46 @@ +(* + * Copyright (c) 2009-2013, Monoidics ltd. + * 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 +module L = Logging + +let models_jar = ref None + +let get_models_jar_filename () = !models_jar + +module StringHash = Caml.Hashtbl.Make (String) + +let models_specs_filenames = StringHash.create 1 + +let collect_specs_filenames jar_filename = + let zip_channel = Zip.open_in jar_filename in + let collect entry = + let filename = entry.Zip.filename in + if Filename.check_suffix filename Config.specs_files_suffix then + let proc_filename = Filename.chop_extension (Filename.basename filename) in + StringHash.replace models_specs_filenames proc_filename () + in + List.iter ~f:collect (Zip.entries zip_channel) ; + Zip.close_in zip_channel + + +let set_models ~jar_filename = + match !models_jar with + | None when match Sys.file_exists jar_filename with `Yes -> false | _ -> true -> + L.die InternalError "Java model file not found@." + | None -> + models_jar := Some jar_filename ; + collect_specs_filenames jar_filename + | Some filename when String.equal filename jar_filename -> + () + | Some filename -> + L.die InternalError "Asked to load a 2nd models jar (%s) when %s was loaded.@." jar_filename + filename + + +let is_model procname = StringHash.mem models_specs_filenames (Procname.to_filename procname) diff --git a/infer/src/java/jModels.mli b/infer/src/java/jModels.mli new file mode 100644 index 000000000..c6e8126cb --- /dev/null +++ b/infer/src/java/jModels.mli @@ -0,0 +1,17 @@ +(* + * Copyright (c) 2009-2013, Monoidics ltd. + * 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 set_models : jar_filename:string -> unit +(** Sets the procnames in the given jar file as models *) + +val is_model : Procname.t -> bool +(** Check if there is a model for the given procname *) + +val get_models_jar_filename : unit -> string option diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 863db86f3..38d64bdc4 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -678,7 +678,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex let instrs = match call_args with (* modeling a class bypasses the treatment of Closeable *) - | _ when Config.biabduction_models_mode || JClasspath.is_model callee_procname -> + | _ when Config.biabduction_models_mode || JModels.is_model callee_procname -> call_instrs | ((_, {Typ.desc= Typ.Tptr ({desc= Tstruct typename}, _)}) as exp) :: _ (* add a file attribute when calling the constructor of a subtype of Closeable *)