Merge pull request #5621 from tautschnig/messaget-parser

parsert is not a messaget

Author: kroening

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -66,8 +66,10 @@ class java_bytecode_parsert final : public parsert
   {
     if(index==0 || index>=constant_pool.size())
     {
-      error() << "invalid constant pool index (" << index << ")" << eom;
-      error() << "constant pool size: " << constant_pool.size() << eom;
+      log.error() << "invalid constant pool index (" << index << ")"
+                  << messaget::eom;
+      log.error() << "constant pool size: " << constant_pool.size()
+                  << messaget::eom;
       throw 0;
     }
 
@@ -117,7 +119,7 @@ class java_bytecode_parsert final : public parsert
     {
       if(!*in)
       {
-        error() << "unexpected end of bytecode file" << eom;
+        log.error() << "unexpected end of bytecode file" << messaget::eom;
         throw 0;
       }
       in->get();
@@ -135,7 +137,7 @@ class java_bytecode_parsert final : public parsert
     {
       if(!*in)
       {
-        error() << "unexpected end of bytecode file" << eom;
+        log.error() << "unexpected end of bytecode file" << messaget::eom;
         throw 0;
       }
       result <<= 8u;
@@ -384,19 +386,19 @@ bool java_bytecode_parsert::parse()
 
   catch(const char *message)
   {
-    error() << message << eom;
+    log.error() << message << messaget::eom;
     return true;
   }
 
   catch(const std::string &message)
   {
-    error() << message << eom;
+    log.error() << message << messaget::eom;
     return true;
   }
 
   catch(...)
   {
-    error() << "parsing error" << eom;
+    log.error() << "parsing error" << messaget::eom;
     return true;
   }
 
@@ -435,13 +437,13 @@ void java_bytecode_parsert::rClassFile()
 
   if(magic!=0xCAFEBABE)
   {
-    error() << "wrong magic" << eom;
+    log.error() << "wrong magic" << messaget::eom;
     throw 0;
   }
 
   if(major_version<44)
   {
-    error() << "unexpected major version" << eom;
+    log.error() << "unexpected major version" << messaget::eom;
     throw 0;
   }
 
@@ -641,7 +643,7 @@ void java_bytecode_parsert::rconstant_pool()
   const u2 constant_pool_count = read<u2>();
   if(constant_pool_count==0)
   {
-    error() << "invalid constant_pool_count" << eom;
+    log.error() << "invalid constant_pool_count" << messaget::eom;
     throw 0;
   }
 
@@ -683,7 +685,7 @@ void java_bytecode_parsert::rconstant_pool()
       // Eight-byte constants take up two entries in the constant_pool table.
       if(it==constant_pool.end())
       {
-        error() << "invalid double entry" << eom;
+        log.error() << "invalid double entry" << messaget::eom;
         throw 0;
       }
       it++;
@@ -707,8 +709,8 @@ void java_bytecode_parsert::rconstant_pool()
       break;
 
     default:
-      error() << "unknown constant pool entry (" << it->tag << ")"
-              << eom;
+      log.error() << "unknown constant pool entry (" << it->tag << ")"
+                  << messaget::eom;
       throw 0;
     }
   }
@@ -1140,7 +1142,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
 
   if(address!=code_length)
   {
-    error() << "bytecode length mismatch" << eom;
+    log.error() << "bytecode length mismatch" << messaget::eom;
     throw 0;
   }
 }
@@ -1809,7 +1811,7 @@ optionalt<java_bytecode_parse_treet> java_bytecode_parse(
 {
   java_bytecode_parsert java_bytecode_parser(skip_instructions);
   java_bytecode_parser.in=&istream;
-  java_bytecode_parser.set_message_handler(message_handler);
+  java_bytecode_parser.log.set_message_handler(message_handler);
 
   bool parser_result=java_bytecode_parser.parse();
 
@@ -1979,8 +1981,8 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
     method_handle_infot method_handle{entry};
 
     const u2 num_bootstrap_arguments = read<u2>();
-    debug() << "INFO: parse BootstrapMethod handle " << num_bootstrap_arguments
-            << " #args" << eom;
+    log.debug() << "INFO: parse BootstrapMethod handle "
+                << num_bootstrap_arguments << " #args" << messaget::eom;
 
     // read u2 values of entry into vector
     std::vector<u2> u2_values(num_bootstrap_arguments);
@@ -2020,9 +2022,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
     if(num_bootstrap_arguments < 3)
     {
       store_unknown_method_handle(bootstrap_method_index);
-      debug()
+      log.debug()
         << "format of BootstrapMethods entry not recognized: too few arguments"
-        << eom;
+        << messaget::eom;
       continue;
     }
 
@@ -2043,9 +2045,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
 
     if(!recognized)
     {
-      debug() << "format of BootstrapMethods entry not recognized: extra "
-                 "arguments of wrong type"
-              << eom;
+      log.debug() << "format of BootstrapMethods entry not recognized: extra "
+                     "arguments of wrong type"
+                  << messaget::eom;
       store_unknown_method_handle(bootstrap_method_index);
       continue;
     }
@@ -2060,22 +2062,23 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
       method_handle_argument.tag != CONSTANT_MethodHandle ||
       method_type_argument.tag != CONSTANT_MethodType)
     {
-      debug() << "format of BootstrapMethods entry not recognized: arguments "
-                 "wrong type"
-              << eom;
+      log.debug()
+        << "format of BootstrapMethods entry not recognized: arguments "
+           "wrong type"
+        << messaget::eom;
       store_unknown_method_handle(bootstrap_method_index);
       continue;
     }
 
-    debug() << "INFO: parse lambda handle" << eom;
+    log.debug() << "INFO: parse lambda handle" << messaget::eom;
     optionalt<lambda_method_handlet> lambda_method_handle =
       parse_method_handle(method_handle_infot{method_handle_argument});
 
     if(!lambda_method_handle.has_value())
     {
-      debug() << "format of BootstrapMethods entry not recognized: method "
-                 "handle not recognised"
-              << eom;
+      log.debug() << "format of BootstrapMethods entry not recognized: method "
+                     "handle not recognised"
+                  << messaget::eom;
       store_unknown_method_handle(bootstrap_method_index);
       continue;
     }
@@ -2084,14 +2087,15 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
     POSTCONDITION(
       lambda_method_handle->handle_type != method_handle_typet::UNKNOWN_HANDLE);
 
-    debug() << "lambda function reference "
-            << id2string(lambda_method_handle->get_method_descriptor()
-                           .base_method_name())
-            << " in class \"" << parse_tree.parsed_class.name << "\""
-            << "\n  interface type is "
-            << id2string(pool_entry(interface_type_argument.ref1).s)
-            << "\n  method type is "
-            << id2string(pool_entry(method_type_argument.ref1).s) << eom;
+    log.debug()
+      << "lambda function reference "
+      << id2string(
+           lambda_method_handle->get_method_descriptor().base_method_name())
+      << " in class \"" << parse_tree.parsed_class.name << "\""
+      << "\n  interface type is "
+      << id2string(pool_entry(interface_type_argument.ref1).s)
+      << "\n  method type is "
+      << id2string(pool_entry(method_type_argument.ref1).s) << messaget::eom;
     parse_tree.parsed_class.add_method_handle(
       bootstrap_method_index, *lambda_method_handle);
   }

src/ansi-c/ansi_c_language.cpp

@@ -72,7 +72,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.clear();
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&codestr;
-  ansi_c_parser.set_message_handler(get_message_handler());
+  ansi_c_parser.log.set_message_handler(get_message_handler());
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.cpp98=false; // it's not C++
@@ -198,7 +198,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.clear();
   ansi_c_parser.set_file(irep_idt());
   ansi_c_parser.in=&i_preprocessed;
-  ansi_c_parser.set_message_handler(get_message_handler());
+  ansi_c_parser.log.set_message_handler(get_message_handler());
   ansi_c_parser.mode=config.ansi_c.mode;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_scanner_init();

src/ansi-c/builtin_factory.cpp

@@ -50,7 +50,7 @@ static bool convert(
   ansi_c_parser.clear();
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=∈
-  ansi_c_parser.set_message_handler(message_handler);
+  ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++

src/cpp/cpp_language.cpp

@@ -104,7 +104,7 @@ bool cpp_languaget::parse(
   cpp_parser.clear();
   cpp_parser.set_file(path);
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.set_message_handler(get_message_handler());
+  cpp_parser.log.set_message_handler(get_message_handler());
   cpp_parser.mode=config.ansi_c.mode;
 
   bool result=cpp_parser.parse();
@@ -244,7 +244,7 @@ bool cpp_languaget::to_expr(
   cpp_parser.clear();
   cpp_parser.set_file(irep_idt());
   cpp_parser.in=&i_preprocessed;
-  cpp_parser.set_message_handler(get_message_handler());
+  cpp_parser.log.set_message_handler(get_message_handler());
 
   bool result=cpp_parser.parse();
 

src/cpp/cpp_parser.cpp

@@ -29,7 +29,7 @@ bool cpp_parsert::parse()
   ansi_c_parser.in=in;
   ansi_c_parser.mode=mode;
   ansi_c_parser.set_file(get_file());
-  ansi_c_parser.set_message_handler(get_message_handler());
+  ansi_c_parser.log.set_message_handler(log.get_message_handler());
 
   return cpp_parse();
 }

src/cpp/parse.cpp

@@ -512,8 +512,8 @@ bool Parser::SyntaxError()
 
     message+="'";
 
-    parser.error().source_location=source_location;
-    parser.error() << message << messaget::eom;
+    parser.log.error().source_location = source_location;
+    parser.log.error() << message << messaget::eom;
   }
 
   return ++number_of_errors < max_errors;

src/jsil/jsil_language.cpp

@@ -61,7 +61,7 @@ bool jsil_languaget::parse(
   jsil_parser.clear();
   jsil_parser.set_file(path);
   jsil_parser.in=&instream;
-  jsil_parser.set_message_handler(get_message_handler());
+  jsil_parser.log.set_message_handler(get_message_handler());
 
   jsil_scanner_init();
   bool result=jsil_parser.parse();
@@ -136,7 +136,7 @@ bool jsil_languaget::to_expr(
   jsil_parser.clear();
   jsil_parser.set_file(irep_idt());
   jsil_parser.in=&instream;
-  jsil_parser.set_message_handler(get_message_handler());
+  jsil_parser.log.set_message_handler(get_message_handler());
   jsil_scanner_init();
 
   bool result=jsil_parser.parse();

src/json/json_parser.cpp

@@ -22,7 +22,7 @@ bool parse_json(
   json_parser.clear();
   json_parser.set_file(filename);
   json_parser.in=∈
-  json_parser.set_message_handler(message_handler);
+  json_parser.log.set_message_handler(message_handler);
 
   bool result=json_parser.parse();
 

src/util/parser.cpp

@@ -40,7 +40,7 @@ void parsert::parse_error(
   tmp_source_location.set_column(column-before.size());
   print(1, tmp, -1, tmp_source_location);
 #else
-  error().source_location=source_location;
-  error() << tmp << eom;
+  log.error().source_location = source_location;
+  log.error() << tmp << messaget::eom;
 #endif
 }

src/util/parser.h

@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "message.h"
 #include "file_util.h"
 
-class parsert:public messaget
+class parsert
 {
 public:
   std::istream *in;
@@ -131,6 +131,10 @@ class parsert:public messaget
     column+=token_width;
   }
 
+  // should be protected or even just be a reference to a message handler, but
+  // for now enables a step-by-step transition
+  messaget log;
+
 protected:
   source_locationt source_location;
   unsigned line_no, previous_line_no;

src/xmllang/xml_parser.cpp

@@ -22,7 +22,7 @@ bool parse_xml(
   xml_parser.clear();
   xml_parser.set_file(filename);
   xml_parser.in=∈
-  xml_parser.set_message_handler(message_handler);
+  xml_parser.log.set_message_handler(message_handler);
 
   bool result=yyxmlparse()!=0;