unify jar list and classpath

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -185,6 +185,12 @@ bool java_bytecode_languaget::parse(
   const std::string &path)
 {
   PRECONDITION(language_options_initialized);
+
+  java_class_loader.clear_classpath();
+
+  for(const auto &p : config.java.classpath)
+    java_class_loader.add_classpath_entry(p);
+
   java_class_loader.set_message_handler(get_message_handler());
   java_class_loader.set_java_cp_include_files(java_cp_include_files);
   java_class_loader.add_load_classes(java_load_classes);
@@ -232,7 +238,7 @@ bool java_bytecode_languaget::parse(
         main_jar_classes.push_back(kv.first);
     }
     else
-      java_class_loader.add_jar_file(path);
+      java_class_loader.add_classpath_entry(path);
   }
   else
     UNREACHABLE;

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -123,13 +123,14 @@ class java_bytecode_languaget:public languaget
       lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER),
       string_refinement_enabled(false),
       pointer_type_selector(std::move(pointer_type_selector))
-  {}
+  {
+  }
 
   java_bytecode_languaget():
     java_bytecode_languaget(
       std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
-  {}
-
+  {
+  }
 
   bool from_expr(
     const exprt &expr,

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/suffix.h>
 #include <util/prefix.h>
-#include <util/config.h>
 
 #include "java_bytecode_parser.h"
 
@@ -69,6 +68,19 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
   return class_map.at(class_name);
 }
 
+void java_class_loadert::add_classpath_entry(const std::string &path)
+{
+  if(has_suffix(path, ".jar"))
+  {
+    classpath_entries.push_back(classpath_entryt(classpath_entryt::JAR, path));
+  }
+  else
+  {
+    classpath_entries.push_back(
+      classpath_entryt(classpath_entryt::DIRECTORY, path));
+  }
+}
+
 optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
   const irep_idt &class_name,
   const std::string &jar_file,
@@ -124,55 +136,44 @@ java_class_loadert::get_parse_tree(
     return parse_trees;
   }
 
-  // First add all given JAR files
-  for(const auto &jar_file : jar_files)
+  // Rummage through the class path
+  for(const auto &cp_entry : classpath_entries)
   {
-    jar_index_optcreft index = read_jar_file(jar_file);
-    if(!index)
-      continue;
-    optionalt<java_bytecode_parse_treet> parse_tree =
-      get_class_from_jar(class_name, jar_file, *index);
-    if(parse_tree)
-      parse_trees.emplace_back(std::move(*parse_tree));
-  }
-
-  // Then add everything on the class path
-  for(const auto &cp_entry : config.java.classpath)
-  {
-    if(has_suffix(cp_entry, ".jar"))
-    {
-      jar_index_optcreft index = read_jar_file(cp_entry);
-      if(!index)
-        continue;
-      optionalt<java_bytecode_parse_treet> parse_tree =
-        get_class_from_jar(class_name, cp_entry, *index);
-      if(parse_tree)
-        parse_trees.emplace_back(std::move(*parse_tree));
-    }
-    else
+    switch(cp_entry.kind)
     {
-      // Look in the given directory
-      const std::string class_file = class_name_to_file(class_name);
-      const std::string full_path =
-        #ifdef _WIN32
-        cp_entry + '\\' + class_file;
-        #else
-        cp_entry + '/' + class_file;
-        #endif
-
-      if(!class_loader_limit.load_class_file(class_file))
-        continue;
-
-      if(std::ifstream(full_path))
+    case classpath_entryt::JAR:
       {
-        debug()
-          << "Getting class `" << class_name << "' from file " << full_path
-          << eom;
+        jar_index_optcreft index = read_jar_file(cp_entry.path);
+        if(!index)
+          continue;
         optionalt<java_bytecode_parse_treet> parse_tree =
-          java_bytecode_parse(full_path, get_message_handler());
+          get_class_from_jar(class_name, cp_entry.path, *index);
         if(parse_tree)
           parse_trees.emplace_back(std::move(*parse_tree));
       }
+      break;
+
+    case classpath_entryt::DIRECTORY:
+      {
+        // Look in the given directory
+        const std::string class_file = class_name_to_file(class_name);
+        const std::string full_path =
+#ifdef _WIN32
+          cp_entry.path + '\\' + class_file;
+#else
+          cp_entry.path + '/' + class_file;
+#endif
+
+        if(std::ifstream(full_path))
+        {
+          debug() << "Getting class `" << class_name << "' from file "
+                  << full_path << eom;
+          optionalt<java_bytecode_parse_treet> parse_tree =
+            java_bytecode_parse(full_path, get_message_handler());
+          if(parse_tree)
+            parse_trees.emplace_back(std::move(*parse_tree));
+        }
+      }
     }
   }
 
@@ -234,12 +235,13 @@ void java_class_loadert::load_entire_jar(
   if(!jar_index)
     return;
 
-  jar_files.push_front(jar_path);
+  classpath_entries.push_front(
+    classpath_entryt(classpath_entryt::JAR, jar_path));
 
   for(const auto &e : jar_index->get())
     operator()(e.first);
 
-  jar_files.pop_front();
+  classpath_entries.pop_front();
 }
 
 java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(

jbmc/src/java_bytecode/java_class_loader.h

@@ -74,11 +74,19 @@ class java_class_loadert:public messaget
     for(const auto &id : classes)
       java_load_classes.push_back(id);
   }
-  void add_jar_file(const std::string &f)
+
+  /// Clear all classpath entries
+  void clear_classpath()
   {
-    jar_files.push_back(f);
+    classpath_entries.clear();
   }
 
+  /// Appends an entry to the class path, used for loading classes.  The
+  /// argument may be
+  /// 1) The name of a directory, used for searching for .class files
+  /// 2) The name of a JAR file
+  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 &);
 
@@ -111,10 +119,21 @@ class java_class_loadert:public messaget
   /// information.
   std::string java_cp_include_files;
 
-  /// List of filesystem paths to .jar files that will be used, in the given
-  /// order, to find and load a class, provided its name (see \ref
-  /// get_parse_tree).
-  std::list<std::string> jar_files;
+  /// An entry in the classpath
+  struct classpath_entryt
+  {
+    using kindt = enum { JAR, DIRECTORY };
+    kindt kind;
+    std::string path;
+
+    classpath_entryt(kindt _kind, const std::string &_path)
+      : kind(_kind), path(_path)
+    {
+    }
+  };
+
+  /// List of entries in the classpath
+  std::list<classpath_entryt> classpath_entries;
 
   /// Classes to be explicitly loaded
   std::vector<irep_idt> java_load_classes;