unify jar list and classpath

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -39,6 +39,13 @@ Author: Daniel Kroening, [email protected]
 #include "expr2java.h"
 #include "load_method_by_regex.h"
 
+/// Set up the classpath
+void java_bytecode_languaget::setup_classpath()
+{
+  for(const auto &p : config.java.classpath)
+    java_class_loader(p);
+}
+
 /// Consume options that are java bytecode specific.
 /// \param Command:line options
 /// \return None
@@ -232,7 +239,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,16 @@ 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))
-  {}
+  {
+    setup_classpath();
+  }
 
   java_bytecode_languaget():
     java_bytecode_languaget(
       std::unique_ptr<select_pointer_typet>(new select_pointer_typet()))
-  {}
-
+  {
+    setup_classpath();
+  }
 
   bool from_expr(
     const exprt &expr,
@@ -162,6 +165,8 @@ class java_bytecode_languaget:public languaget
     symbol_table_baset &symbol_table) override;
 
 protected:
+  void setup_classpath();
+
   void convert_single_method(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table)

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,11 @@ 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)
+{
+  classpath_entries.push_back(path);
+}
+
 optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
   const irep_idt &class_name,
   const std::string &jar_file,
@@ -124,20 +128,8 @@ java_class_loadert::get_parse_tree(
     return parse_trees;
   }
 
-  // First add all given JAR files
-  for(const auto &jar_file : jar_files)
-  {
-    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)
+  // Rummage through the class path
+  for(const auto &cp_entry : classpath_entries)
   {
     if(has_suffix(cp_entry, ".jar"))
     {
@@ -234,12 +226,12 @@ void java_class_loadert::load_entire_jar(
   if(!jar_index)
     return;
 
-  jar_files.push_front(jar_path);
+  classpath_entries.push_front(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

@@ -73,10 +73,12 @@ 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)
-  {
-    jar_files.push_back(f);
-  }
+
+  /// 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 &);
@@ -122,10 +124,8 @@ 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;
+  /// List of entries in the classpath
+  std::list<std::string> classpath_entries;
 
   /// Classes to be explicitly loaded
   std::vector<irep_idt> java_load_classes;