java_class_loader(_base)t isn't a messaget

Pass a message handler as an argument to several of their functions, but do not
construct a messaget object without a configured message handler as that is
deprecated.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -330,13 +330,16 @@ void java_bytecode_languaget::initialize_class_loader()
   for(const auto &p : config.java.classpath)
     java_class_loader.add_classpath_entry(p);
 
+<<<<<<< HEAD
 <<<<<<< HEAD
   java_class_loader.set_java_cp_include_files(
     language_options->java_cp_include_files);
   java_class_loader.add_load_classes(language_options->java_load_classes);
   if(language_options->string_refinement_enabled)
 =======
   java_class_loader.set_message_handler(message_handler);
+=======
+>>>>>>> java_class_loader(_base)t isn't a messaget
   java_class_loader.set_java_cp_include_files(java_cp_include_files);
   java_class_loader.add_load_classes(java_load_classes);
   if(string_refinement_enabled)
@@ -469,7 +472,7 @@ bool java_bytecode_languaget::parse(
       messaget log(message_handler);
       log.status() << "JAR file without entry point: loading class files"
                    << messaget::eom;
-      const auto classes = java_class_loader.load_entire_jar(path);
+      const auto classes = java_class_loader.load_entire_jar(path, message_handler);
       for(const auto &c : classes)
         main_jar_classes.push_back(c);
     }
@@ -486,7 +489,7 @@ bool java_bytecode_languaget::parse(
   {
     messaget log(message_handler);
     log.status() << "Java main class: " << main_class << messaget::eom;
-    java_class_loader(main_class);
+    java_class_loader(main_class, message_handler);
   }
 >>>>>>> languaget is not a messaget
 
@@ -1665,10 +1668,10 @@ bool java_bytecode_languaget::final(symbol_table_baset &)
   return false;
 }
 
-void java_bytecode_languaget::show_parse(std::ostream &out, message_handlert &)
+void java_bytecode_languaget::show_parse(std::ostream &out, message_handlert &message_handler)
 {
   java_class_loadert::parse_tree_with_overlayst &parse_trees =
-    java_class_loader(main_class);
+    java_class_loader(main_class, message_handler);
   parse_trees.front().output(out);
   if(parse_trees.size() > 1)
   {

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -17,7 +17,8 @@ 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)
+  const irep_idt &class_name,
+  message_handlert &message_handler)
 {
   debug() << "Classpath:";
   for(const auto &entry : classpath_entries)
@@ -44,7 +45,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 +55,11 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
     if(class_map.count(c) != 0)
       continue;
 
-    debug() << "Reading class " << c << eom;
+    messaget log(message_handler);
+    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)
@@ -121,6 +123,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 +132,26 @@ 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 +170,18 @@ java_class_loadert::get_parse_tree(
         ++parse_tree_it;
         break;
       }
+<<<<<<< HEAD
       debug() << "Skipping class " << class_name
               << " marked with OverlayClassImplementation but found before"
                  " original definition"
               << eom;
+=======
+      log.warning()
+        << "Skipping class " << class_name
+        << " marked with OverlayClassImplementation but found before"
+          " original definition"
+        << messaget::eom;
+>>>>>>> java_class_loader(_base)t isn't a messaget
     }
     auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
     ++parse_tree_it;
@@ -179,8 +193,14 @@ java_class_loadert::get_parse_tree(
     // Remove non-initial classes that aren't overlays
     if(!is_overlay_class(parse_tree_it->parsed_class))
     {
+<<<<<<< HEAD
       debug() << "Skipping duplicate definition of class " << class_name
               << " not marked with OverlayClassImplementation" << eom;
+=======
+      log.warning()
+        << "Skipping duplicate definition of class " << class_name
+        << " not marked with OverlayClassImplementation" << messaget::eom;
+>>>>>>> java_class_loader(_base)t isn't a messaget
       auto duplicate_non_overlay_it = parse_tree_it;
       ++parse_tree_it;
       parse_trees.erase(duplicate_non_overlay_it);
@@ -192,45 +212,60 @@ java_class_loadert::get_parse_tree(
     return parse_trees;
 
   // Not found or failed to load
+<<<<<<< HEAD
   debug() << "failed to load class " << class_name << eom;
+=======
+  log.warning() << "failed to load class `" << class_name << '\'' << messaget::eom;
+>>>>>>> java_class_loader(_base)t isn't a messaget
   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)
+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 &)
   {
+<<<<<<< HEAD
     error() << "failed to open JAR file '" << jar_path << "'" << eom;
     return {};
   }
   debug() << "Adding JAR file '" << jar_path << "'" << eom;
+=======
+    log.error() << "failed to open JAR file `" << jar_path << "'" << messaget::eom;
+    return {};
+  }
+  log.debug() << "Adding JAR file `" << jar_path << "'" << messaget::eom;
+>>>>>>> java_class_loader(_base)t isn't a messaget
 
   // Create a new entry in the map and initialize using the list of file names
   // that are in jar_filet
@@ -239,8 +274,14 @@ java_class_loadert::read_jar_file(const std::string &jar_path)
   {
     if(has_suffix(file_name, ".class"))
     {
+<<<<<<< HEAD
       debug() << "Found class file " << file_name << " in JAR '" << jar_path
               << "'" << eom;
+=======
+      log.debug()
+        << "Found class file " << file_name << " in JAR `" << jar_path << "'"
+        << messaget::eom;
+>>>>>>> java_class_loader(_base)t isn't a messaget
       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,15 @@ 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);
 
   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 +74,7 @@ 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 +103,7 @@ 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

jbmc/src/java_bytecode/java_class_loader_base.cpp

@@ -12,7 +12,11 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_parser.h"
 
 #include <util/file_util.h>
+<<<<<<< HEAD
 #include <util/prefix.h>
+=======
+#include <util/message.h>
+>>>>>>> java_class_loader(_base)t isn't a messaget
 #include <util/suffix.h>
 
 #include <fstream>
@@ -127,15 +131,16 @@ java_class_loader_baset::class_name_to_os_file(const irep_idt &class_name)
 /// attempt to load a class from a classpath_entry
 optionalt<java_bytecode_parse_treet> java_class_loader_baset::load_class(
   const irep_idt &class_name,
-  const classpath_entryt &cp_entry)
+  const classpath_entryt &cp_entry,
+  message_handlert &message_handler)
 {
   switch(cp_entry.kind)
   {
   case classpath_entryt::JAR:
-    return get_class_from_jar(class_name, cp_entry.path);
+    return get_class_from_jar(class_name, cp_entry.path, message_handler);
 
   case classpath_entryt::DIRECTORY:
-    return get_class_from_directory(class_name, cp_entry.path);
+    return get_class_from_directory(class_name, cp_entry.path, message_handler);
   }
 
   UNREACHABLE;
@@ -144,12 +149,16 @@ optionalt<java_bytecode_parse_treet> java_class_loader_baset::load_class(
 /// Load class from jar file.
 /// \param class_name: name of class to load in Java source format
 /// \param jar_file: path of the jar file
+/// \param message_handler: message handler
 /// \return optional value of parse tree, empty if class cannot be loaded
 optionalt<java_bytecode_parse_treet>
 java_class_loader_baset::get_class_from_jar(
   const irep_idt &class_name,
-  const std::string &jar_file)
+  const std::string &jar_file,
+  message_handlert &message_handler)
 {
+  messaget log(message_handler);
+
   try
   {
     auto &jar = jar_pool(jar_file);
@@ -158,6 +167,7 @@ java_class_loader_baset::get_class_from_jar(
     if(!data.has_value())
       return {};
 
+<<<<<<< HEAD
     debug() << "Getting class '" << class_name << "' from JAR " << jar_file
             << eom;
 
@@ -167,28 +177,48 @@ java_class_loader_baset::get_class_from_jar(
   catch(const std::runtime_error &)
   {
     error() << "failed to open JAR file '" << jar_file << "'" << eom;
+=======
+    log.debug() << "Getting class `" << class_name << "' from JAR " << jar_file
+            << messaget::eom;
+
+    std::istringstream istream(*data);
+    return java_bytecode_parse(istream, message_handler);
+  }
+  catch(const std::runtime_error &)
+  {
+    log.error() << "failed to open JAR file `" << jar_file << "'" << messaget::eom;
+>>>>>>> java_class_loader(_base)t isn't a messaget
     return {};
   }
 }
 
 /// Load class from directory.
 /// \param class_name: name of class to load in Java source format
 /// \param path: directory to load from
+/// \param message_handler: message handler
 /// \return optional value of parse tree, empty if class cannot be loaded
 optionalt<java_bytecode_parse_treet>
 java_class_loader_baset::get_class_from_directory(
   const irep_idt &class_name,
-  const std::string &path)
+  const std::string &path,
+  message_handlert &message_handler)
 {
   // Look in the given directory
   const std::string class_file = class_name_to_os_file(class_name);
   const std::string full_path = concat_dir_file(path, class_file);
 
   if(std::ifstream(full_path))
   {
+<<<<<<< HEAD
     debug() << "Getting class '" << class_name << "' from file " << full_path
             << eom;
     return java_bytecode_parse(full_path, class_name, get_message_handler());
+=======
+    messaget log(message_handler);
+    log.debug() << "Getting class `" << class_name << "' from file " << full_path
+            << messaget::eom;
+    return java_bytecode_parse(full_path, message_handler);
+>>>>>>> java_class_loader(_base)t isn't a messaget
   }
   else
     return {};