Merge pull request #2766 from diffblue/jar_index

jar_index cleanout

Author: kroening

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -235,9 +235,9 @@ bool java_bytecode_languaget::parse(
     if(main_class.empty())
     {
       status() << "JAR file without entry point: loading class files" << eom;
-      java_class_loader.load_entire_jar(path);
-      for(const auto &kv : java_class_loader.get_jar_index(path))
-        main_jar_classes.push_back(kv.first);
+      const auto classes = java_class_loader.load_entire_jar(path);
+      for(const auto &c : classes)
+        main_jar_classes.push_back(c);
     }
     else
       java_class_loader.add_classpath_entry(path);

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -88,17 +88,16 @@ void java_class_loadert::add_classpath_entry(const std::string &path)
 /// \return optional value of parse tree, empty if class cannot be loaded
 optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
   const irep_idt &class_name,
-  const std::string &jar_file,
-  const jar_indext &jar_index)
+  const std::string &jar_file)
 {
-  auto jar_index_it = jar_index.find(class_name);
-  if(jar_index_it == jar_index.end())
+  auto classes = read_jar_file(jar_file);
+  if(!classes.has_value())
     return {};
 
   debug()
     << "Getting class `" << class_name << "' from JAR " << jar_file << eom;
 
-  auto data = jar_pool(jar_file).get_entry(jar_index_it->second);
+  auto data = jar_pool(jar_file).get_entry(class_name_to_jar_file(class_name));
 
   if(!data.has_value())
     return {};
@@ -137,7 +136,7 @@ java_class_loadert::get_parse_tree(
   PRECONDITION(parse_trees.empty());
 
   // do we refuse to load?
-  if(!class_loader_limit.load_class_file(class_name_to_file(class_name)))
+  if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
   {
     debug() << "not loading " << class_name << " because of limit" << eom;
     java_bytecode_parse_treet parse_tree;
@@ -153,11 +152,8 @@ java_class_loadert::get_parse_tree(
     {
     case classpath_entryt::JAR:
       {
-        jar_index_optcreft index = read_jar_file(cp_entry.path);
-        if(!index)
-          continue;
         optionalt<java_bytecode_parse_treet> parse_tree =
-          get_class_from_jar(class_name, cp_entry.path, *index);
+          get_class_from_jar(class_name, cp_entry.path);
         if(parse_tree)
           parse_trees.emplace_back(std::move(*parse_tree));
       }
@@ -166,7 +162,7 @@ java_class_loadert::get_parse_tree(
     case classpath_entryt::DIRECTORY:
       {
         // Look in the given directory
-        const std::string class_file = class_name_to_file(class_name);
+        const std::string class_file = class_name_to_os_file(class_name);
         const std::string full_path =
 #ifdef _WIN32
           cp_entry.path + '\\' + class_file;
@@ -238,32 +234,29 @@ java_class_loadert::get_parse_tree(
   return parse_trees;
 }
 
-/// Load all class files from a .jar file, and store name of .jar in
-/// `classpath_entreies`.
+/// Load all class files from a .jar file
 /// \param jar_path: the path for the .jar to load
-void java_class_loadert::load_entire_jar(
+std::vector<irep_idt> java_class_loadert::load_entire_jar(
   const std::string &jar_path)
 {
-  jar_index_optcreft jar_index = read_jar_file(jar_path);
-  if(!jar_index)
-    return;
+  auto classes = read_jar_file(jar_path);
+  if(!classes.has_value())
+    return {};
 
   classpath_entries.push_front(
     classpath_entryt(classpath_entryt::JAR, jar_path));
 
-  for(const auto &e : jar_index->get())
-    operator()(e.first);
+  for(const auto &c : *classes)
+    operator()(c);
 
   classpath_entries.pop_front();
+
+  return *classes;
 }
 
-java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
-  const std::string &jar_path)
+optionalt<std::vector<irep_idt>>
+java_class_loadert::read_jar_file(const std::string &jar_path)
 {
-  auto existing_it = jars_by_path.find(jar_path);
-  if(existing_it != jars_by_path.end())
-    return std::cref(existing_it->second);
-
   std::vector<std::string> filenames;
   try
   {
@@ -272,13 +265,13 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
   catch(const std::runtime_error &)
   {
     error() << "failed to open JAR file `" << jar_path << "'" << eom;
-    return jar_index_optcreft();
+    return {};
   }
   debug() << "Adding JAR file `" << jar_path << "'" << eom;
 
   // Create a new entry in the map and initialize using the list of file names
   // that are in jar_filet
-  jar_indext &jar_index = jars_by_path[jar_path];
+  std::vector<irep_idt> classes;
   for(auto &file_name : filenames)
   {
     if(has_suffix(file_name, ".class"))
@@ -287,10 +280,10 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
         << "Found class file " << file_name << " in JAR `" << jar_path << "'"
         << eom;
       irep_idt class_name=file_to_class_name(file_name);
-      jar_index[class_name] = file_name;
+      classes.push_back(class_name);
     }
   }
-  return std::cref(jar_index);
+  return classes;
 }
 
 /// Convert a file name to the class name. Java interprets folders as packages,
@@ -330,7 +323,27 @@ std::string java_class_loadert::file_to_class_name(const std::string &file)
 /// file_to_class_name.
 /// \param class_name: the name of the class
 /// \return the class name converted to file name
-std::string java_class_loadert::class_name_to_file(const irep_idt &class_name)
+std::string
+java_class_loadert::class_name_to_jar_file(const irep_idt &class_name)
+{
+  std::string result = id2string(class_name);
+
+  // dots (package name separators) to slash
+  for(std::string::iterator it = result.begin(); it != result.end(); it++)
+    if(*it == '.')
+      *it = '/';
+
+  // add .class suffix
+  result += ".class";
+
+  return result;
+}
+
+/// Convert a class name to a file name, with OS-dependent syntax
+/// \param class_name: the name of the class
+/// \return the class name converted to file name
+std::string
+java_class_loadert::class_name_to_os_file(const irep_idt &class_name)
 {
   std::string result=id2string(class_name);
 

jbmc/src/java_bytecode/java_class_loader.h

@@ -27,10 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
 class java_class_loadert:public messaget
 {
 public:
-  /// A map associating logical class names with the name of the .class file
-  /// implementing it for all classes inside a single JAR file
-  typedef std::map<irep_idt, std::string> jar_indext;
-
   /// A list of parse trees supporting overlay classes
   typedef std::list<java_bytecode_parse_treet> parse_tree_with_overlayst;
   /// A map from class names to list of parse tree where multiple entries can
@@ -95,14 +91,11 @@ class java_class_loadert:public messaget
   void add_classpath_entry(const std::string &);
 
   static std::string file_to_class_name(const std::string &);
-  static std::string class_name_to_file(const irep_idt &);
+  static std::string class_name_to_os_file(const irep_idt &);
+  static std::string class_name_to_jar_file(const irep_idt &);
 
-  void load_entire_jar(const std::string &jar_path);
+  std::vector<irep_idt> load_entire_jar(const std::string &jar_path);
 
-  const jar_indext &get_jar_index(const std::string &jar_path)
-  {
-    return jars_by_path.at(jar_path);
-  }
   /// Map from class names to the bytecode parse trees
   fixed_keys_map_wrappert<parse_tree_with_overridest_mapt>
   get_class_with_overlays_map()
@@ -146,22 +139,13 @@ class java_class_loadert:public messaget
   std::vector<irep_idt> java_load_classes;
   get_extra_class_refs_functiont get_extra_class_refs;
 
-  /// The jar_indext for each jar file we've read
-  std::map<std::string, jar_indext> jars_by_path;
-
   /// Map from class names to the bytecode parse trees
   parse_tree_with_overridest_mapt class_map;
 
-  typedef optionalt<std::reference_wrapper<const jar_indext>>
-    jar_index_optcreft;
-
-  jar_index_optcreft read_jar_file(
-    const std::string &jar_path);
+  optionalt<std::vector<irep_idt>> read_jar_file(const std::string &jar_path);
 
-  optionalt<java_bytecode_parse_treet> get_class_from_jar(
-    const irep_idt &class_name,
-    const std::string &jar_file,
-    const jar_indext &jar_index);
+  optionalt<java_bytecode_parse_treet>
+  get_class_from_jar(const irep_idt &class_name, const std::string &jar_file);
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H