Revert "WIP: message handler"

This reverts commit 0e25e07cc8f1410080b4304caa5f5911c8fa4bc9.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -27,8 +27,8 @@ Author: Daniel Kroening, [email protected]
 class java_bytecode_parsert final : public parsert
 {
 public:
-  java_bytecode_parsert(bool skip_instructions, message_handlert &message_handler)
-    : parsert(message_handler), skip_instructions(skip_instructions)
+  explicit java_bytecode_parsert(bool skip_instructions)
+    : skip_instructions(skip_instructions)
   {
   }
 
@@ -1809,8 +1809,9 @@ std::optional<java_bytecode_parse_treet> java_bytecode_parse(
   message_handlert &message_handler,
   bool skip_instructions)
 {
-  java_bytecode_parsert java_bytecode_parser(skip_instructions, message_handler);
+  java_bytecode_parsert java_bytecode_parser(skip_instructions);
   java_bytecode_parser.in=&istream;
+  java_bytecode_parser.log.set_message_handler(message_handler);
 
   bool parser_result=java_bytecode_parser.parse();
 

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -172,7 +172,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
   info.ns = &ns;
   info.prop = &sat_check;
   info.output_xml = false;
-  bv_refinementt solver(info, null_message_handler);
+  bv_refinementt solver(info);
   solver << expr;
   return solver();
 }

src/ansi-c/ansi_c_language.cpp

@@ -71,22 +71,26 @@ bool ansi_c_languaget::parse(
   ansi_c_internal_additions(code);
   std::istringstream codestr(code);
 
-  ansi_c_parsert ansi_c_parser(message_handler);
+  ansi_c_parser.clear();
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=&codestr;
+  ansi_c_parser.log.set_message_handler(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++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
+  ansi_c_scanner_init();
+
   bool result=ansi_c_parser.parse();
 
   if(!result)
   {
     ansi_c_parser.set_line_no(0);
     ansi_c_parser.set_file(path);
     ansi_c_parser.in=&i_preprocessed;
+    ansi_c_scanner_init();
     result=ansi_c_parser.parse();
   }
 
@@ -201,12 +205,13 @@ bool ansi_c_languaget::to_expr(
 
   // parsing
 
-  ansi_c_parsert  ansi_c_parser(get_message_handler());
+  ansi_c_parser.clear();
   ansi_c_parser.set_file(irep_idt());
   ansi_c_parser.in=&i_preprocessed;
   ansi_c_parser.log.set_message_handler(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();
 
   bool result=ansi_c_parser.parse();
 

src/ansi-c/ansi_c_parser.cpp

@@ -10,37 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_storage_spec.h"
 
-void ansi_c_parser_init(ansi_c_parsert *ansi_c_parser);
-void ansi_c_scanner_init(ansi_c_parsert *ansi_c_parser);
-int yyansi_cparse();
-
-bool ansi_c_parsert::parse()
-{
-  clear();
-  ansi_c_scanner_init(this);
-  ansi_c_parser_init(this);
-  return yyansi_cparse()!=0;
-}
-
-void ansi_c_parsert::clear()
-{
-  parsert::clear();
-  parse_tree.clear();
-
-  // scanner state
-  tag_following=false;
-  asm_block_following=false;
-  parenthesis_counter=0;
-  string_literal.clear();
-  pragma_pack.clear();
-
-  // set up global scope
-  scopes.clear();
-  scopes.push_back(scopet());
-
-  ansi_c_scanner_init(nullptr);
-  ansi_c_parser_init(nullptr);
-}
+ansi_c_parsert ansi_c_parser;
 
 ansi_c_id_classt ansi_c_parsert::lookup(
   const irep_idt &base_name,
@@ -103,6 +73,14 @@ void ansi_c_parsert::add_tag_with_body(irept &tag)
   }
 }
 
+extern char *yyansi_ctext;
+
+int yyansi_cerror(const std::string &error)
+{
+  ansi_c_parser.parse_error(error, yyansi_ctext);
+  return 0;
+}
+
 void ansi_c_parsert::add_declarator(
   exprt &declaration,
   irept &declarator)

src/ansi-c/ansi_c_parser.h

@@ -18,12 +18,13 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_parse_tree.h"
 #include "ansi_c_scope.h"
 
+int yyansi_cparse();
+
 class ansi_c_parsert:public parsert
 {
 public:
   ansi_c_parse_treet parse_tree;
 
-<<<<<<< HEAD
   ansi_c_parsert()
     : tag_following(false),
       asm_block_following(false),
@@ -33,25 +34,14 @@ class ansi_c_parsert:public parsert
       cpp11(false),
       for_has_scope(false),
       ts_18661_3_Floatn_types(false)
-=======
-  explicit ansi_c_parsert(message_handlert &message_handler):
-    parsert(message_handler),
-    tag_following(false),
-    asm_block_following(false),
-    parenthesis_counter(0),
-    mode(modet::NONE),
-    cpp98(false),
-    cpp11(false),
-    for_has_scope(false),
-    ts_18661_3_Floatn_types(false),
-    Float128_type(false)
->>>>>>> WIP: message handler
   {
   }
 
-  bool parse() override;
+  virtual bool parse() override
+  {
+    return yyansi_cparse()!=0;
+  }
 
-<<<<<<< HEAD
   virtual void clear() override
   {
     parsert::clear();
@@ -69,9 +59,6 @@ class ansi_c_parsert:public parsert
     scopes.clear();
     scopes.push_back(scopet());
   }
-=======
-  void clear() override;
->>>>>>> WIP: message handler
 
   // internal state of the scanner
   bool tag_following;
@@ -179,4 +166,9 @@ class ansi_c_parsert:public parsert
   std::list<std::map<const irep_idt, bool>> pragma_cprover_stack;
 };
 
+extern ansi_c_parsert ansi_c_parser;
+
+int yyansi_cerror(const std::string &error);
+void ansi_c_scanner_init();
+
 #endif // CPROVER_ANSI_C_ANSI_C_PARSER_H

src/ansi-c/builtin_factory.cpp

@@ -47,7 +47,7 @@ static bool convert(
 {
   std::istringstream in(s.str());
 
-  ansi_c_parsert ansi_c_parser(message_handler);
+  ansi_c_parser.clear();
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=∈
   ansi_c_parser.log.set_message_handler(message_handler);
@@ -56,6 +56,8 @@ static bool convert(
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
 
+  ansi_c_scanner_init();
+
   if(ansi_c_parser.parse())
     return true;
 

src/ansi-c/parser.y

@@ -13,19 +13,12 @@
 #ifdef ANSI_C_DEBUG
 #define YYDEBUG 1
 #endif
-#define PARSER (*ansi_c_parser)
+#define PARSER ansi_c_parser
 
 #include "ansi_c_parser.h"
 
 int yyansi_clex();
-int yyansi_cerror(const std::string &error);
-
-static ansi_c_parsert *ansi_c_parser;
-
-void ansi_c_parser_init(ansi_c_parsert *_ansi_c_parser)
-{
-  ansi_c_parser = _ansi_c_parser;
-}
+extern char *yyansi_ctext;
 
 #include "parser_static.inc"
 

src/ansi-c/scanner.l

@@ -38,7 +38,7 @@ static int isatty(int) { return 0; }
 #include "literals/convert_string_literal.h"
 #include "literals/unescape_string.h"
 
-#define PARSER (*ansi_c_parser)
+#define PARSER ansi_c_parser
 #define YYSTYPE unsigned
 #undef  ECHO
 #define ECHO
@@ -52,10 +52,6 @@ extern int yyansi_cdebug;
 #define loc() \
   { newstack(yyansi_clval); PARSER.set_source_location(parser_stack(yyansi_clval)); }
 
-static ansi_c_parsert *ansi_c_parser;
-
-int yyansi_cerror(const std::string &error);
-
 int make_identifier()
 {
   loc();
@@ -269,9 +265,8 @@ enable_or_disable ("enable"|"disable")
 %x OTHER_PRAGMA
 
 %{
-void ansi_c_scanner_init(ansi_c_parsert *_ansi_c_parser)
+void ansi_c_scanner_init()
 {
-  ansi_c_parser = _ansi_c_parser;
 #ifdef ANSI_C_DEBUG
   yyansi_cdebug=1;
 #endif
@@ -282,8 +277,7 @@ void ansi_c_scanner_init(ansi_c_parsert *_ansi_c_parser)
 
 %%
 
-<INITIAL>.|\n   { PRECONDITION(ansi_c_parser);
-                  BEGIN(GRAMMAR);
+<INITIAL>.|\n   { BEGIN(GRAMMAR);
                   yyless(0); /* start again with this character */
                 }
 
@@ -1821,10 +1815,3 @@ __decltype          { if(PARSER.cpp98 &&
 %%
 
 int yywrap() { return 1; }
-
-int yyansi_cerror(const std::string &error)
-{
-  PRECONDITION(ansi_c_parser);
-  ansi_c_parser->parse_error(error, yyansi_ctext);
-  return 0;
-}

src/assembler/assembler_parser.cpp

@@ -8,25 +8,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "assembler_parser.h"
 
-<<<<<<< HEAD
 assembler_parsert assembler_parser;
 
 extern char *yyassemblertext;
-=======
-int yyassemblerlex();
-void assembler_scanner_init(assembler_parsert *assembler_parser);
 
-bool assembler_parsert::parse()
+int yyassemblererror(const std::string &error)
 {
-  assembler_scanner_init(this);
-  yyassemblerlex();
-  return false;
-}
->>>>>>> WIP: message handler
-
-void assembler_parsert::clear()
-{
-  parsert::clear();
-  instructions.clear();
-  assembler_scanner_init(nullptr);
+  assembler_parser.parse_error(error, yyassemblertext);
+  return 0;
 }

src/assembler/assembler_parser.h

@@ -11,15 +11,12 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H
 
 #include <util/parser.h>
-<<<<<<< HEAD
 
 #include <list>
 
 int yyassemblerlex();
 int yyassemblererror(const std::string &error);
 void assembler_scanner_init();
-=======
->>>>>>> WIP: message handler
 
 class assembler_parsert:public parsert
 {
@@ -40,14 +37,24 @@ class assembler_parsert:public parsert
     instructions.push_back(instructiont());
   }
 
-  explicit assembler_parsert(message_handlert &message_handler)
-    : parsert(message_handler)
+  assembler_parsert()
   {
   }
 
-  bool parse() override;
+  virtual bool parse()
+  {
+    yyassemblerlex();
+    return false;
+  }
 
-  void clear() override;
+  virtual void clear()
+  {
+    parsert::clear();
+    instructions.clear();
+    // assembler_scanner_init();
+  }
 };
 
+extern assembler_parsert assembler_parser;
+
 #endif // CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H