Merge pull request #5585 from tautschnig/messaget-java_class_loader

java_class_loader(_base)t isn't a messaget

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -292,7 +292,6 @@ bool java_bytecode_languaget::preprocess(
 void java_bytecode_languaget::set_message_handler(
   message_handlert &message_handler)
 {
-  java_class_loader.set_message_handler(message_handler);
   languaget::set_message_handler(message_handler);
 }
 
@@ -301,7 +300,7 @@ void java_bytecode_languaget::initialize_class_loader()
   java_class_loader.clear_classpath();
 
   for(const auto &p : config.java.classpath)
-    java_class_loader.add_classpath_entry(p);
+    java_class_loader.add_classpath_entry(p, get_message_handler());
 
   java_class_loader.set_java_cp_include_files(
     language_options->java_cp_include_files);
@@ -330,7 +329,7 @@ void java_bytecode_languaget::parse_from_main_class()
   {
     // Try to load class
     status() << "Trying to load Java main class: " << main_class << eom;
-    if(!java_class_loader.can_load_class(main_class))
+    if(!java_class_loader.can_load_class(main_class, get_message_handler()))
     {
       // Try to extract class name and load class
       const auto maybe_class_name =
@@ -342,7 +341,8 @@ void java_bytecode_languaget::parse_from_main_class()
       }
       status() << "Trying to load Java main class: " << maybe_class_name.value()
                << eom;
-      if(!java_class_loader.can_load_class(maybe_class_name.value()))
+      if(!java_class_loader.can_load_class(
+           maybe_class_name.value(), get_message_handler()))
       {
         throwMainClassLoadingError(id2string(main_class));
         return;
@@ -354,7 +354,8 @@ void java_bytecode_languaget::parse_from_main_class()
     }
     status() << "Found Java main class: " << main_class << eom;
     // Now really load it.
-    const auto &parse_trees = java_class_loader(main_class);
+    const auto &parse_trees =
+      java_class_loader(main_class, get_message_handler());
     if(parse_trees.empty() || !parse_trees.front().loading_successful)
     {
       throwMainClassLoadingError(id2string(main_class));
@@ -429,12 +430,13 @@ bool java_bytecode_languaget::parse(
     if(main_class.empty())
     {
       status() << "JAR file without entry point: loading class files" << eom;
-      const auto classes = java_class_loader.load_entire_jar(path);
+      const auto classes =
+        java_class_loader.load_entire_jar(path, get_message_handler());
       for(const auto &c : classes)
         main_jar_classes.push_back(c);
     }
     else
-      java_class_loader.add_classpath_entry(path);
+      java_class_loader.add_classpath_entry(path, get_message_handler());
   }
   else
     main_class = config.java.main_class;
@@ -1504,7 +1506,7 @@ bool java_bytecode_languaget::final(symbol_table_baset &)
 void java_bytecode_languaget::show_parse(std::ostream &out)
 {
   java_class_loadert::parse_tree_with_overlayst &parse_trees =
-    java_class_loader(main_class);
+    java_class_loader(main_class, get_message_handler());
   parse_trees.front().output(out);
   if(parse_trees.size() > 1)
   {

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -16,15 +16,17 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_bytecode_parser.h"
 
-java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
-  const irep_idt &class_name)
+java_class_loadert::parse_tree_with_overlayst &java_class_loadert::
+operator()(const irep_idt &class_name, message_handlert &message_handler)
 {
-  debug() << "Classpath:";
+  messaget log(message_handler);
+
+  log.debug() << "Classpath:";
   for(const auto &entry : classpath_entries)
   {
-    debug() << "\n  " << entry.path;
+    log.debug() << "\n  " << entry.path;
   }
-  debug() << messaget::eom;
+  log.debug() << messaget::eom;
 
   std::stack<irep_idt> queue;
   // Always require java.lang.Object, as it is the base of
@@ -44,7 +46,7 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
     queue.push(id);
 
   java_class_loader_limitt class_loader_limit(
-    get_message_handler(), java_cp_include_files);
+    message_handler, java_cp_include_files);
 
   while(!queue.empty())
   {
@@ -54,10 +56,10 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
     if(class_map.count(c) != 0)
       continue;
 
-    debug() << "Reading class " << c << eom;
+    log.debug() << "Reading class " << c << messaget::eom;
 
     parse_tree_with_overlayst &parse_trees =
-      get_parse_tree(class_loader_limit, c);
+      get_parse_tree(class_loader_limit, c, message_handler);
 
     // Add any dependencies to queue
     for(const java_bytecode_parse_treet &parse_tree : parse_trees)
@@ -103,11 +105,13 @@ static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
     .has_value();
 }
 
-bool java_class_loadert::can_load_class(const irep_idt &class_name)
+bool java_class_loadert::can_load_class(
+  const irep_idt &class_name,
+  message_handlert &message_handler)
 {
   for(const auto &cp_entry : classpath_entries)
   {
-    auto parse_tree = load_class(class_name, cp_entry);
+    auto parse_tree = load_class(class_name, cp_entry, message_handler);
     if(parse_tree.has_value())
       return true;
   }
@@ -121,6 +125,7 @@ bool java_class_loadert::can_load_class(const irep_idt &class_name)
 /// to find the .class file.
 /// \param class_loader_limit: Filter to decide whether to load classes
 /// \param class_name: Name of class to load
+/// \param message_handler: message handler
 /// \return The list of valid implementations, including overlays
 /// \remarks
 ///   Allows multiple definitions of the same class to appear on the
@@ -129,23 +134,27 @@ bool java_class_loadert::can_load_class(const irep_idt &class_name)
 java_class_loadert::parse_tree_with_overlayst &
 java_class_loadert::get_parse_tree(
   java_class_loader_limitt &class_loader_limit,
-  const irep_idt &class_name)
+  const irep_idt &class_name,
+  message_handlert &message_handler)
 {
   parse_tree_with_overlayst &parse_trees = class_map[class_name];
   PRECONDITION(parse_trees.empty());
 
+  messaget log(message_handler);
+
   // do we refuse to load?
   if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
   {
-    debug() << "not loading " << class_name << " because of limit" << eom;
+    log.debug() << "not loading " << class_name << " because of limit"
+                << messaget::eom;
     parse_trees.emplace_back(class_name);
     return parse_trees;
   }
 
   // Rummage through the class path
   for(const auto &cp_entry : classpath_entries)
   {
-    auto parse_tree = load_class(class_name, cp_entry);
+    auto parse_tree = load_class(class_name, cp_entry, message_handler);
     if(parse_tree.has_value())
       parse_trees.emplace_back(std::move(*parse_tree));
   }
@@ -164,10 +173,10 @@ java_class_loadert::get_parse_tree(
         ++parse_tree_it;
         break;
       }
-      debug() << "Skipping class " << class_name
-              << " marked with OverlayClassImplementation but found before"
-                 " original definition"
-              << eom;
+      log.debug() << "Skipping class " << class_name
+                  << " marked with OverlayClassImplementation but found before"
+                     " original definition"
+                  << messaget::eom;
     }
     auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
     ++parse_tree_it;
@@ -179,8 +188,9 @@ java_class_loadert::get_parse_tree(
     // Remove non-initial classes that aren't overlays
     if(!is_overlay_class(parse_tree_it->parsed_class))
     {
-      debug() << "Skipping duplicate definition of class " << class_name
-              << " not marked with OverlayClassImplementation" << eom;
+      log.debug() << "Skipping duplicate definition of class " << class_name
+                  << " not marked with OverlayClassImplementation"
+                  << messaget::eom;
       auto duplicate_non_overlay_it = parse_tree_it;
       ++parse_tree_it;
       parse_trees.erase(duplicate_non_overlay_it);
@@ -192,45 +202,50 @@ java_class_loadert::get_parse_tree(
     return parse_trees;
 
   // Not found or failed to load
-  debug() << "failed to load class " << class_name << eom;
+  log.debug() << "failed to load class " << class_name << messaget::eom;
   parse_trees.emplace_back(class_name);
   return parse_trees;
 }
 
 /// Load all class files from a .jar file
 /// \param jar_path: the path for the .jar to load
 std::vector<irep_idt> java_class_loadert::load_entire_jar(
-  const std::string &jar_path)
+  const std::string &jar_path,
+  message_handlert &message_handler)
 {
-  auto classes = read_jar_file(jar_path);
+  auto classes = read_jar_file(jar_path, message_handler);
   if(!classes.has_value())
     return {};
 
   classpath_entries.push_front(
     classpath_entryt(classpath_entryt::JAR, jar_path));
 
   for(const auto &c : *classes)
-    operator()(c);
+    operator()(c, message_handler);
 
   classpath_entries.pop_front();
 
   return *classes;
 }
 
-optionalt<std::vector<irep_idt>>
-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,
+  message_handlert &message_handler)
 {
+  messaget log(message_handler);
+
   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;
+    log.error() << "failed to open JAR file '" << jar_path << "'"
+                << messaget::eom;
     return {};
   }
-  debug() << "Adding JAR file '" << jar_path << "'" << eom;
+  log.debug() << "Adding JAR file '" << jar_path << "'" << messaget::eom;
 
   // Create a new entry in the map and initialize using the list of file names
   // that are in jar_filet
@@ -239,8 +254,8 @@ java_class_loadert::read_jar_file(const std::string &jar_path)
   {
     if(has_suffix(file_name, ".class"))
     {
-      debug() << "Found class file " << file_name << " in JAR '" << jar_path
-              << "'" << eom;
+      log.debug() << "Found class file " << file_name << " in JAR '" << jar_path
+                  << "'" << messaget::eom;
       irep_idt class_name=file_to_class_name(file_name);
       classes.push_back(class_name);
     }

jbmc/src/java_bytecode/java_class_loader.h

@@ -41,15 +41,17 @@ class java_class_loadert : public java_class_loader_baset
   {
   }
 
-  parse_tree_with_overlayst &operator()(const irep_idt &class_name);
+  parse_tree_with_overlayst &
+  operator()(const irep_idt &class_name, message_handlert &);
 
   /// Checks whether \p class_name is parseable from the classpath,
   /// ignoring class loading limits.
-  bool can_load_class(const irep_idt &class_name);
+  bool can_load_class(const irep_idt &class_name, message_handlert &);
 
   parse_tree_with_overlayst &get_parse_tree(
     java_class_loader_limitt &class_loader_limit,
-    const irep_idt &class_name);
+    const irep_idt &class_name,
+    message_handlert &);
 
   /// Set the argument of the class loader limit \ref java_class_loader_limitt
   /// \param cp_include_files: argument string for java_class_loader_limit
@@ -74,7 +76,8 @@ class java_class_loadert : public java_class_loader_baset
       java_load_classes.push_back(id);
   }
 
-  std::vector<irep_idt> load_entire_jar(const std::string &jar_path);
+  std::vector<irep_idt>
+  load_entire_jar(const std::string &jar_path, message_handlert &);
 
   /// Map from class names to the bytecode parse trees
   fixed_keys_map_wrappert<parse_tree_with_overridest_mapt>
@@ -103,7 +106,8 @@ class java_class_loadert : public java_class_loader_baset
   /// Map from class names to the bytecode parse trees
   parse_tree_with_overridest_mapt class_map;
 
-  optionalt<std::vector<irep_idt>> read_jar_file(const std::string &jar_path);
+  optionalt<std::vector<irep_idt>>
+  read_jar_file(const std::string &jar_path, message_handlert &);
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H