Merge pull request #5596 from tautschnig/messaget-java_bytecode_convert

tautschnig · web-flow · commit 299307bb3fba · 2020-11-18T22:45:38.000+01:00
java_bytecode_convert* aren't messaget
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -31,7 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/suffix.h>
 
-class java_bytecode_convert_classt:public messaget
+class java_bytecode_convert_classt
 {
 public:
   java_bytecode_convert_classt(
@@ -41,7 +41,7 @@ class java_bytecode_convert_classt:public messaget
     method_bytecodet &method_bytecode,
     java_string_library_preprocesst &_string_preprocess,
     const std::unordered_set<std::string> &no_load_classes)
-    : messaget(_message_handler),
+    : log(_message_handler),
       symbol_table(_symbol_table),
       max_array_length(_max_array_length),
       method_bytecode(method_bytecode),
@@ -98,7 +98,7 @@ class java_bytecode_convert_classt:public messaget
       generate_class_stub(
         class_name,
         symbol_table,
-        get_message_handler(),
+        log.get_message_handler(),
         struct_union_typet::componentst{});
   }
 
@@ -108,6 +108,7 @@ class java_bytecode_convert_classt:public messaget
   typedef java_bytecode_parse_treet::annotationt annotationt;
 
 private:
+  messaget log;
   symbol_tablet &symbol_table;
   const size_t max_array_length;
   method_bytecodet &method_bytecode;
@@ -274,7 +275,8 @@ void java_bytecode_convert_classt::convert(
   std::string qualified_classname="java::"+id2string(c.name);
   if(symbol_table.has_symbol(qualified_classname))
   {
-    debug() << "Skip class " << c.name << " (already loaded)" << eom;
+    log.debug() << "Skip class " << c.name << " (already loaded)"
+                << messaget::eom;
     return;
   }
 
@@ -302,10 +304,10 @@ void java_bytecode_convert_classt::convert(
     }
     catch(const unsupported_java_class_signature_exceptiont &e)
     {
-      debug() << "Class: " << c.name
-              << "\n could not parse signature: " << c.signature.value()
-              << "\n " << e.what() << "\n ignoring that the class is generic"
-              << eom;
+      log.debug() << "Class: " << c.name
+                  << "\n could not parse signature: " << c.signature.value()
+                  << "\n " << e.what()
+                  << "\n ignoring that the class is generic" << messaget::eom;
     }
   }
 
@@ -325,9 +327,11 @@ void java_bytecode_convert_classt::convert(
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)
     {
-      warning() << "Java Enum " << c.name << " won't work properly because max "
-                << "array length (" << max_array_length << ") is less than the "
-                << "enum size (" << c.enum_elements << ")" << eom;
+      log.warning() << "Java Enum " << c.name
+                    << " won't work properly because max "
+                    << "array length (" << max_array_length
+                    << ") is less than the "
+                    << "enum size (" << c.enum_elements << ")" << messaget::eom;
     }
     class_type.set(
       ID_java_enum_static_unwind,
@@ -364,10 +368,12 @@ void java_bytecode_convert_classt::convert(
       }
       catch(const unsupported_java_class_signature_exceptiont &e)
       {
-        debug() << "Superclass: " << c.super_class << " of class: " << c.name
-                << "\n could not parse signature: " << superclass_ref.value()
-                << "\n " << e.what()
-                << "\n ignoring that the superclass is generic" << eom;
+        log.debug() << "Superclass: " << c.super_class
+                    << " of class: " << c.name
+                    << "\n could not parse signature: "
+                    << superclass_ref.value() << "\n " << e.what()
+                    << "\n ignoring that the superclass is generic"
+                    << messaget::eom;
         class_type.add_base(base);
       }
     }
@@ -404,10 +410,11 @@ void java_bytecode_convert_classt::convert(
       }
       catch(const unsupported_java_class_signature_exceptiont &e)
       {
-        debug() << "Interface: " << interface << " of class: " << c.name
-                << "\n could not parse signature: " << interface_ref.value()
-                << "\n " << e.what()
-                << "\n ignoring that the interface is generic" << eom;
+        log.debug() << "Interface: " << interface << " of class: " << c.name
+                    << "\n could not parse signature: " << interface_ref.value()
+                    << "\n " << e.what()
+                    << "\n ignoring that the interface is generic"
+                    << messaget::eom;
         class_type.add_base(base);
       }
     }
@@ -455,10 +462,11 @@ void java_bytecode_convert_classt::convert(
   symbolt *class_symbol;
 
   // add before we do members
-  debug() << "Adding symbol: class '" << c.name << "'" << eom;
+  log.debug() << "Adding symbol: class '" << c.name << "'" << messaget::eom;
   if(symbol_table.move(new_symbol, class_symbol))
   {
-    error() << "failed to add class symbol " << new_symbol.name << eom;
+    log.error() << "failed to add class symbol " << new_symbol.name
+                << messaget::eom;
     throw 0;
   }
 
@@ -477,12 +485,11 @@ void java_bytecode_convert_classt::convert(
         std::string err =
           "Duplicate field definition for " + field_id + " in overlay class";
         // TODO: This could just be a warning if the types match
-        error() << err << eom;
+        log.error() << err << messaget::eom;
         throw err.c_str();
       }
-      debug()
-        << "Adding symbol from overlay class:  field '" << field.name << "'"
-        << eom;
+      log.debug() << "Adding symbol from overlay class:  field '" << field.name
+                  << "'" << messaget::eom;
       convert(*class_symbol, field);
       POSTCONDITION(check_field_exists(field, field_id, fields));
     }
@@ -493,12 +500,12 @@ void java_bytecode_convert_classt::convert(
     if(check_field_exists(field, field_id, fields))
     {
       // TODO: This could be a warning if the types match
-      error()
-        << "Field definition for " << field_id
-        << " already loaded from overlay class" << eom;
+      log.error() << "Field definition for " << field_id
+                  << " already loaded from overlay class" << messaget::eom;
       continue;
     }
-    debug() << "Adding symbol:  field '" << field.name << "'" << eom;
+    log.debug() << "Adding symbol:  field '" << field.name << "'"
+                << messaget::eom;
     convert(*class_symbol, field);
     POSTCONDITION(check_field_exists(field, field_id, fields));
   }
@@ -514,9 +521,8 @@ void java_bytecode_convert_classt::convert(
           + ":" + method.descriptor;
       if(is_ignored_method(c.name, method))
       {
-        debug()
-          << "Ignoring method:  '" << method_identifier << "'"
-          << eom;
+        log.debug() << "Ignoring method:  '" << method_identifier << "'"
+                    << messaget::eom;
         continue;
       }
       if(method_bytecode.contains_method(method_identifier))
@@ -530,26 +536,25 @@ void java_bytecode_convert_classt::convert(
         {
           // This method was defined in a previous class definition without
           // being marked as an overlay method
-          warning()
+          log.warning()
             << "Method " << method_identifier
             << " exists in an overlay class without being marked as an "
-              "overlay and also exists in another overlay class that appears "
-              "earlier in the classpath"
-            << eom;
+               "overlay and also exists in another overlay class that appears "
+               "earlier in the classpath"
+            << messaget::eom;
         }
         continue;
       }
       // Always run the lazy pre-stage, as it symbol-table
       // registers the function.
-      debug()
-        << "Adding symbol from overlay class:  method '" << method_identifier
-        << "'" << eom;
+      log.debug() << "Adding symbol from overlay class:  method '"
+                  << method_identifier << "'" << messaget::eom;
       java_bytecode_convert_method_lazy(
         *class_symbol,
         method_identifier,
         method,
         symbol_table,
-        get_message_handler());
+        log.get_message_handler());
       method_bytecode.add(qualified_classname, method_identifier, method);
       if(is_overlay_method(method))
         overlay_methods.insert(method_identifier);
@@ -562,9 +567,8 @@ void java_bytecode_convert_classt::convert(
         + ":" + method.descriptor;
     if(is_ignored_method(c.name, method))
     {
-      debug()
-        << "Ignoring method:  '" << method_identifier << "'"
-        << eom;
+      log.debug() << "Ignoring method:  '" << method_identifier << "'"
+                  << messaget::eom;
       continue;
     }
     if(method_bytecode.contains_method(method_identifier))
@@ -577,39 +581,41 @@ void java_bytecode_convert_classt::convert(
       {
         // This method was defined in a previous class definition without
         // being marked as an overlay method
-        warning()
+        log.warning()
           << "Method " << method_identifier
           << " exists in an overlay class without being marked as an overlay "
-            "and also exists in the underlying class"
-          << eom;
+             "and also exists in the underlying class"
+          << messaget::eom;
       }
       continue;
     }
     // Always run the lazy pre-stage, as it symbol-table
     // registers the function.
-    debug() << "Adding symbol:  method '" << method_identifier << "'" << eom;
+    log.debug() << "Adding symbol:  method '" << method_identifier << "'"
+                << messaget::eom;
     java_bytecode_convert_method_lazy(
       *class_symbol,
       method_identifier,
       method,
       symbol_table,
-      get_message_handler());
+      log.get_message_handler());
     method_bytecode.add(qualified_classname, method_identifier, method);
     if(is_overlay_method(method))
     {
-      warning()
+      log.warning()
         << "Method " << method_identifier
-        << " marked as an overlay where defined in the underlying class" << eom;
+        << " marked as an overlay where defined in the underlying class"
+        << messaget::eom;
     }
   }
   if(!overlay_methods.empty())
   {
-    error()
+    log.error()
       << "Overlay methods defined in overlay classes did not exist in the "
-        "underlying class:\n";
+         "underlying class:\n";
     for(const irep_idt &method_id : overlay_methods)
-      error() << "  " << method_id << "\n";
-    error() << eom;
+      log.error() << "  " << method_id << "\n";
+    log.error() << messaget::eom;
   }
 
   // is this a root class?
@@ -744,8 +750,8 @@ void java_bytecode_convert_classt::convert(
     const auto value = zero_initializer(field_type, class_symbol.location, ns);
     if(!value.has_value())
     {
-      error().source_location = class_symbol.location;
-      error() << "failed to zero-initialize " << f.name << eom;
+      log.error().source_location = class_symbol.location;
+      log.error() << "failed to zero-initialize " << f.name << messaget::eom;
       throw 0;
     }
     new_symbol.value = *value;
@@ -1025,12 +1031,14 @@ bool java_bytecode_convert_class(
 
   catch(const char *e)
   {
-    java_bytecode_convert_class.error() << e << messaget::eom;
+    messaget log{message_handler};
+    log.error() << e << messaget::eom;
   }
 
   catch(const std::string &e)
   {
-    java_bytecode_convert_class.error() << e << messaget::eom;
+    messaget log{message_handler};
+    log.error() << e << messaget::eom;
   }
 
   return true;
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -134,7 +134,7 @@ exprt::operandst java_bytecode_convert_methodt::pop(std::size_t n)
 {
   if(stack.size()<n)
   {
-    error() << "malformed bytecode (pop too high)" << eom;
+    log.error() << "malformed bytecode (pop too high)" << messaget::eom;
     throw 0;
   }
 
@@ -575,8 +575,8 @@ void java_bytecode_convert_methodt::convert(
   // the formal parameters
   slots_for_parameters = java_method_parameter_slots(method_type);
 
-  debug() << "Generating codet: class " << class_symbol.name << ", method "
-          << m.name << eom;
+  log.debug() << "Generating codet: class " << class_symbol.name << ", method "
+              << m.name << messaget::eom;
 
   // Add parameter symbols to the symbol table
   create_parameter_symbols(parameters, variables, symbol_table);
@@ -870,11 +870,11 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
     {
       if(p<(*findstart) || p>=findlim_block_start_address)
       {
-        debug() << "Generating codet:  "
-                << "warning: refusing to create lexical block spanning "
-                << (*findstart) << "-" << findlim_block_start_address
-                << " due to incoming edge " << p << " -> "
-                << checkit->first << eom;
+        log.debug() << "Generating codet:  "
+                    << "warning: refusing to create lexical block spanning "
+                    << (*findstart) << "-" << findlim_block_start_address
+                    << " due to incoming edge " << p << " -> " << checkit->first
+                    << messaget::eom;
         return this_block;
       }
     }
@@ -893,10 +893,10 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   code_blockt &newblock=to_code_block(newlabel.code());
   auto nblocks=std::distance(findstart, findlim);
   assert(nblocks>=2);
-  debug() << "Generating codet:  combining "
-          << std::distance(findstart, findlim)
-          << " blocks for addresses " << (*findstart) << "-"
-          << findlim_block_start_address << eom;
+  log.debug() << "Generating codet:  combining "
+              << std::distance(findstart, findlim) << " blocks for addresses "
+              << (*findstart) << "-" << findlim_block_start_address
+              << messaget::eom;
 
   // Make a new block containing every child of interest:
   auto &this_block_children = this_block.statements();
@@ -2312,7 +2312,7 @@ void java_bytecode_convert_methodt::convert_invoke(
       method_type,
       class_method_descriptor.class_id(),
       symbol_table,
-      get_message_handler());
+      log.get_message_handler());
   }
 
   exprt function;
@@ -3075,8 +3075,8 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
     const auto value = zero_initializer(return_type, location, ns);
     if(!value.has_value())
     {
-      error().source_location = location;
-      error() << "failed to zero-initialize return type" << eom;
+      log.error().source_location = location;
+      log.error() << "failed to zero-initialize return type" << messaget::eom;
       throw 0;
     }
     return value;
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class symbol_tablet;
 class symbolt;
 
-class java_bytecode_convert_methodt:public messaget
+class java_bytecode_convert_methodt
 {
 public:
   java_bytecode_convert_methodt(
@@ -42,7 +42,7 @@ class java_bytecode_convert_methodt:public messaget
     const class_hierarchyt &class_hierarchy,
     bool threading_support,
     bool assert_no_exceptions_thrown)
-    : messaget(_message_handler),
+    : log(_message_handler),
       symbol_table(symbol_table),
       ns(symbol_table),
       max_array_length(_max_array_length),
@@ -74,6 +74,7 @@ class java_bytecode_convert_methodt:public messaget
   typedef uint16_t method_offsett;
 
 protected:
+  messaget log;
   symbol_table_baset &symbol_table;
   namespacet ns;
   const size_t max_array_length;
diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp
