removed jar_indext types and data structures

Author: Daniel Kroening

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -83,21 +83,32 @@ void java_class_loadert::add_classpath_entry(const std::string &path)
 
 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())
-    return {};
+  const auto filename = class_name_to_file(class_name);
 
-  debug()
-    << "Getting class `" << class_name << "' from JAR " << jar_file << eom;
+  optionalt<std::string> data;
 
-  auto data = jar_pool(jar_file).get_entry(jar_index_it->second);
+  try
+  {
+    // Opening the jar file might fail, throwing an exception,
+    // and also reading the file (with get_entry) might fail,
+    // e.g., if it doesn't exist in the JAR. In this case,
+    // {} is returned.
+    data = jar_pool(jar_file).get_entry(filename);
+  }
+  catch(const std::runtime_error &)
+  {
+    error() << "failed to open JAR file `" << jar_file << "'" << eom;
+    return {};
+  }
 
   if(!data.has_value())
     return {};
 
+  debug() << "Getting class `" << class_name << "' from JAR " << jar_file
+          << eom;
+
   std::istringstream istream(*data);
   return java_bytecode_parse(istream, get_message_handler());
 }
@@ -143,11 +154,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));
       }
@@ -231,60 +239,40 @@ java_class_loadert::get_parse_tree(
 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 {};
-
-  classpath_entries.push_front(
-    classpath_entryt(classpath_entryt::JAR, jar_path));
-
-  std::vector<irep_idt> classes;
-
-  for(const auto &e : jar_index->get())
-  {
-    operator()(e.first);
-    classes.push_back(e.first);
-  }
-
-  classpath_entries.pop_front();
-
-  return classes;
-}
-
-java_class_loadert::jar_index_optcreft 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
   {
     filenames = jar_pool(jar_path).filenames();
   }
   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"))
     {
       debug()
         << "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(file_to_class_name(file_name));
     }
   }
-  return std::cref(jar_index);
+
+  classpath_entries.push_front(
+    classpath_entryt(classpath_entryt::JAR, jar_path));
+
+  for(const auto &c : classes)
+    operator()(c);
+
+  classpath_entries.pop_front();
+
+  return classes;
 }
 
 std::string java_class_loadert::file_to_class_name(const std::string &file)

jbmc/src/java_bytecode/java_class_loader.h

@@ -25,10 +25,6 @@ Author: Daniel Kroening, [email protected]
 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;
-
   typedef std::list<java_bytecode_parse_treet> parse_tree_with_overlayst;
   typedef std::map<irep_idt, parse_tree_with_overlayst>
     parse_tree_with_overridest_mapt;
@@ -92,10 +88,6 @@ class java_class_loadert:public messaget
 
   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()
@@ -139,22 +131,11 @@ 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<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