[java] separate and improve model handling during capture

Summary: The classpath module doesn't need to know about model handling.  Also, strengthen some invariants, use option types instead of strings, and hash sets instead of tree sets.

Reviewed By: skcho

Differential Revision: D20228873

fbshipit-source-id: 18b6bb276

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
+    JModels.get_models_jar_filename ()
-    else collect_classes JBasics.ClassMap.empty !models_jar
+    |> Option.fold ~init:JBasics.ClassMap.empty ~f:collect_classes
   in
   let program =
     { classpath= {path= classpath; channel= Javalib.class_path classpath}

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
 

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

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

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)

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

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 *)