assembler_parsert: construct with message handler

This both avoids an object of static lifetime as well as it fixes the
(transitive) use of the deprecated messaget() constructor.

Author: tautschnig

src/assembler/assembler_parser.cpp

@@ -8,11 +8,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "assembler_parser.h"
 
-assembler_parsert assembler_parser;
-
 extern char *yyassemblertext;
 
-int yyassemblererror(const std::string &error)
+int yyassemblererror(
+  assembler_parsert &assembler_parser,
+  const std::string &error)
 {
   assembler_parser.parse_error(error, yyassemblertext);
   return 0;

src/assembler/assembler_parser.h

@@ -14,9 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <list>
 
-int yyassemblerlex();
-int yyassemblererror(const std::string &error);
-void assembler_scanner_init();
+class assembler_parsert;
+int yyassemblerlex(assembler_parsert &);
+int yyassemblererror(assembler_parsert &, const std::string &error);
 
 class assembler_parsert:public parsert
 {
@@ -37,24 +37,22 @@ 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();
+    yyassemblerlex(*this);
     return false;
   }
 
   virtual void clear()
   {
     parsert::clear();
     instructions.clear();
-    // assembler_scanner_init();
   }
 };
 
-extern assembler_parsert assembler_parser;
-
 #endif // CPROVER_ASSEMBLER_ASSEMBLER_PARSER_H

src/assembler/remove_asm.cpp

@@ -30,8 +30,13 @@ Date:   December 2014
 class remove_asmt
 {
 public:
-  remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
-    : symbol_table(_symbol_table), goto_functions(_goto_functions)
+  remove_asmt(
+    symbol_tablet &_symbol_table,
+    goto_functionst &_goto_functions,
+    message_handlert &message_handler)
+    : symbol_table(_symbol_table),
+      goto_functions(_goto_functions),
+      message_handler(message_handler)
   {
   }
 
@@ -44,6 +49,7 @@ class remove_asmt
 protected:
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
+  message_handlert &message_handler;
 
   void process_function(const irep_idt &, goto_functionst::goto_functiont &);
 
@@ -228,7 +234,7 @@ void remove_asmt::process_instruction_gcc(
   const irep_idt &i_str = to_string_constant(code.asm_text()).value();
 
   std::istringstream str(id2string(i_str));
-  assembler_parser.clear();
+  assembler_parsert assembler_parser{message_handler};
   assembler_parser.in = &str;
   assembler_parser.parse();
 
@@ -399,7 +405,7 @@ void remove_asmt::process_instruction_msc(
   const irep_idt &i_str = to_string_constant(code.op0()).value();
 
   std::istringstream str(id2string(i_str));
-  assembler_parser.clear();
+  assembler_parsert assembler_parser{message_handler};
   assembler_parser.in = &str;
   assembler_parser.parse();
 
@@ -544,13 +550,17 @@ void remove_asmt::process_function(
     remove_skip(goto_function.body);
 }
 
-/// \copybrief remove_asm(goto_modelt &)
+/// \copybrief remove_asm(goto_modelt &, message_handlert &)
 ///
 /// \param goto_functions: The goto functions
 /// \param symbol_table: The symbol table
-void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
+/// \param message_handler: Message handler
+void remove_asm(
+  goto_functionst &goto_functions,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
 {
-  remove_asmt rem(symbol_table, goto_functions);
+  remove_asmt rem(symbol_table, goto_functions, message_handler);
   rem();
 }
 
@@ -561,9 +571,11 @@ void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
 /// Unrecognised assembly instructions are ignored.
 ///
 /// \param goto_model: The goto model
-void remove_asm(goto_modelt &goto_model)
+/// \param message_handler: Message handler
+void remove_asm(goto_modelt &goto_model, message_handlert &message_handler)
 {
-  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
+  remove_asm(
+    goto_model.goto_functions, goto_model.symbol_table, message_handler);
 }
 
 bool has_asm(const goto_functionst &goto_functions)

src/assembler/remove_asm.h

@@ -54,11 +54,12 @@ Date:   December 2014
 
 class goto_functionst;
 class goto_modelt;
+class message_handlert;
 class symbol_tablet;
 
-void remove_asm(goto_functionst &, symbol_tablet &);
+void remove_asm(goto_functionst &, symbol_tablet &, message_handlert &);
 
-void remove_asm(goto_modelt &);
+void remove_asm(goto_modelt &, message_handlert &);
 
 /// returns true iff the given goto functions use asm instructions
 bool has_asm(const goto_functionst &);

src/assembler/scanner.l

@@ -13,7 +13,7 @@
 #pragma warning(disable:4005)
 #endif
 
-#define PARSER assembler_parser
+#define PARSER (*assembler_parser)
 #define YYSTYPE unsigned
 #undef  ECHO
 #define ECHO
@@ -61,10 +61,18 @@ string_lit      ("L"|"u"|"U"|"u8")?["]{s_char}*["]
 %x LINE_COMMENT
 
 %{
-void assemlber_scanner_init()
+static assembler_parsert *assembler_parser;
+
+int yyassemblerlex(void);
+
+int yyassemblerlex(assembler_parsert &_assembler_parser)
 {
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
+  // our scanner is not reentrant
+  PRECONDITION(!assembler_parser);
+  assembler_parser = &_assembler_parser;
+  int result = yyassemblerlex();
+  assembler_parser = nullptr;
+  return result;
 }
 %}
 

src/cbmc/cbmc_parse_options.cpp

@@ -882,7 +882,7 @@ bool cbmc_parse_optionst::process_goto_program(
 {
   // Remove inline assembler; this needs to happen before
   // adding the library.
-  remove_asm(goto_model);
+  remove_asm(goto_model, log.get_message_handler());
 
   // add the library
   log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -894,7 +894,7 @@ bool cbmc_parse_optionst::process_goto_program(
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, log.get_message_handler());
     link_to_library(
       goto_model, log.get_message_handler(), cprover_cpp_library_factory);
     link_to_library(

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -698,7 +698,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
 {
   // Remove inline assembler; this needs to happen before
   // adding the library.
-  remove_asm(goto_model);
+  remove_asm(goto_model, ui_message_handler);
 
   // add the library
   log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -708,7 +708,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, ui_message_handler);
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);

src/goto-diff/goto_diff_parse_options.cpp

@@ -176,7 +176,7 @@ bool goto_diff_parse_optionst::process_goto_program(
 {
   // Remove inline assembler; this needs to happen before
   // adding the library.
-  remove_asm(goto_model);
+  remove_asm(goto_model, ui_message_handler);
 
   // add the library
   log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -186,7 +186,7 @@ bool goto_diff_parse_optionst::process_goto_program(
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, ui_message_handler);
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -949,7 +949,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
   log.status() << "Virtual function removal" << messaget::eom;
   remove_virtual_functions(goto_model);
   log.status() << "Cleaning inline assembler statements" << messaget::eom;
-  remove_asm(goto_model);
+  remove_asm(goto_model, log.get_message_handler());
 }
 
 /// Remove function pointers that can be resolved by analysing const variables
@@ -1065,7 +1065,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     // remove inline assembler as that may yield further library function calls
     // that need to be resolved
-    remove_asm(goto_model);
+    remove_asm(goto_model, ui_message_handler);
 
     // add the library
     log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
@@ -1076,7 +1076,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     // library functions may introduce inline assembler
     while(has_asm(goto_model))
     {
-      remove_asm(goto_model);
+      remove_asm(goto_model, ui_message_handler);
       link_to_library(
         goto_model, ui_message_handler, cprover_cpp_library_factory);
       link_to_library(

src/goto-synthesizer/cegis_verifier.cpp

@@ -84,15 +84,15 @@ get_checked_pointer_from_null_pointer_check(const exprt &violation)
 void cegis_verifiert::preprocess_goto_model()
 {
   // Preprocess `goto_model`. Copied from `cbmc_parse_options.cpp`.
-  remove_asm(goto_model);
+  remove_asm(goto_model, log.get_message_handler());
   link_to_library(
     goto_model, log.get_message_handler(), cprover_cpp_library_factory);
   link_to_library(
     goto_model, log.get_message_handler(), cprover_c_library_factory);
   // library functions may introduce inline assembler
   while(has_asm(goto_model))
   {
-    remove_asm(goto_model);
+    remove_asm(goto_model, log.get_message_handler());
     link_to_library(
       goto_model, log.get_message_handler(), cprover_cpp_library_factory);
     link_to_library(

src/libcprover-cpp/api.cpp

@@ -178,7 +178,7 @@ bool api_sessiont::is_goto_binary(std::string &file) const
 bool api_sessiont::preprocess_model() const
 {
   // Remove inline assembler; this needs to happen before adding the library.
-  remove_asm(*implementation->model);
+  remove_asm(*implementation->model, *implementation->message_handler);
 
   // add the library
   messaget log{*implementation->message_handler};
@@ -191,7 +191,7 @@ bool api_sessiont::preprocess_model() const
   // library functions may introduce inline assembler
   while(has_asm(*implementation->model))
   {
-    remove_asm(*implementation->model);
+    remove_asm(*implementation->model, *implementation->message_handler);
     link_to_library(
       *implementation->model,
       *implementation->message_handler,