WIP: message handler

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -29,8 +29,8 @@ Author: Daniel Kroening, [email protected]
 class java_bytecode_parsert final : public parsert
 {
 public:
-  explicit java_bytecode_parsert(bool skip_instructions)
-    : skip_instructions(skip_instructions)
+  java_bytecode_parsert(bool skip_instructions, message_handlert &message_handler)
+    : parsert(message_handler), skip_instructions(skip_instructions)
   {
   }
 
@@ -1811,9 +1811,8 @@ optionalt<java_bytecode_parse_treet> java_bytecode_parse(
   message_handlert &message_handler,
   bool skip_instructions)
 {
-  java_bytecode_parsert java_bytecode_parser(skip_instructions);
+  java_bytecode_parsert java_bytecode_parser(skip_instructions, message_handler);
   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

@@ -168,7 +168,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);
+  bv_refinementt solver(info, null_message_handler);
   solver << expr;
   return solver();
 }

src/ansi-c/ansi_c_language.cpp

@@ -77,26 +77,22 @@ bool ansi_c_languaget::parse(
   ansi_c_internal_additions(code);
   std::istringstream codestr(code);
 
-  ansi_c_parser.clear();
+  ansi_c_parsert ansi_c_parser(message_handler);
   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();
   }
 
@@ -196,13 +192,12 @@ bool ansi_c_languaget::to_expr(
 
   // parsing
 
-  ansi_c_parser.clear();
+  ansi_c_parsert  ansi_c_parser(get_message_handler());
   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,7 +10,37 @@ Author: Daniel Kroening, [email protected]
 
 #include "c_storage_spec.h"
 
-ansi_c_parsert ansi_c_parser;
+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_id_classt ansi_c_parsert::lookup(
   const irep_idt &base_name,
@@ -73,14 +103,6 @@ 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

@@ -22,13 +22,12 @@ 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),
@@ -38,14 +37,25 @@ 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
   {
   }
 
-  virtual bool parse() override
-  {
-    return yyansi_cparse()!=0;
-  }
+  bool parse() override;
 
+<<<<<<< HEAD
   virtual void clear() override
   {
     parsert::clear();
@@ -63,6 +73,9 @@ 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;
@@ -158,9 +171,4 @@ class ansi_c_parsert:public parsert
   }
 };
 
-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_parser.clear();
+  ansi_c_parsert ansi_c_parser(message_handler);
   ansi_c_parser.set_file(ID_built_in);
   ansi_c_parser.in=∈
   ansi_c_parser.log.set_message_handler(message_handler);
@@ -56,8 +56,6 @@ 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,12 +13,19 @@
 #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();
-extern char *yyansi_ctext;
+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;
+}
 
 #include "parser_static.inc"
 

src/ansi-c/scanner.l

@@ -40,7 +40,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
@@ -54,6 +54,10 @@ 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();
@@ -263,8 +267,9 @@ named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check})[
 %x OTHER_PRAGMA
 
 %{
-void ansi_c_scanner_init()
+void ansi_c_scanner_init(ansi_c_parsert *_ansi_c_parser)
 {
+  ansi_c_parser = _ansi_c_parser;
 #ifdef ANSI_C_DEBUG
   yyansi_cdebug=1;
 #endif
@@ -275,7 +280,8 @@ void ansi_c_scanner_init()
 
 %%
 
-<INITIAL>.|\n   { BEGIN(GRAMMAR);
+<INITIAL>.|\n   { PRECONDITION(ansi_c_parser);
+                  BEGIN(GRAMMAR);
                   yyless(0); /* start again with this character */
                 }
 
@@ -1780,3 +1786,10 @@ __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,12 +8,25 @@ 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);
 
-int yyassemblererror(const std::string &error)
+bool assembler_parsert::parse()
 {
-  assembler_parser.parse_error(error, yyassemblertext);
-  return 0;
+  assembler_scanner_init(this);
+  yyassemblerlex();
+  return false;
+}
+>>>>>>> WIP: message handler
+
+void assembler_parsert::clear()
+{
+  parsert::clear();
+  instructions.clear();
+  assembler_scanner_init(nullptr);
 }

src/assembler/assembler_parser.h

@@ -11,12 +11,15 @@ 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
 {
@@ -37,24 +40,14 @@ class assembler_parsert:public parsert
     instructions.push_back(instructiont());
   }
 
-  assembler_parsert()
+  explicit assembler_parsert(message_handlert &message_handler)
+    : parsert(message_handler)
   {
   }
 
-  virtual bool parse()
-  {
-    yyassemblerlex();
-    return false;
-  }
+  bool parse() override;
 
-  virtual void clear()
-  {
-    parsert::clear();
-    instructions.clear();
-    // assembler_scanner_init();
-  }
+  void clear() override;
 };
 
-extern assembler_parsert assembler_parser;
-
 #endif // CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H