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. The scanner
is now fully reentrant.

doc/architectural/goto-program-transformations.md

@@ -17,7 +17,8 @@ This pass goes through the goto model and removes or lowers instances of
 assembly intructions. Assembly instructions are stored in instances of the
 `other` instruction.
 
-The implementation of this pass is called via the \ref remove_asm(goto_modelt &)
+The implementation of this pass is called via the
+\ref remove_asm(goto_modelt &, message_handlert &)
 function. For full documentation of this pass see \ref remove_asm.h
 
 <em>This pass has no predecessor.</em>

src/assembler/assembler_parser.cpp

@@ -8,12 +8,26 @@ Author: Daniel Kroening, [email protected]
 
 #include "assembler_parser.h"
 
-assembler_parsert assembler_parser;
+char *yyassemblerget_text(void *);
 
-extern char *yyassemblertext;
-
-int yyassemblererror(const std::string &error)
+int yyassemblererror(
+  assembler_parsert &assembler_parser,
+  void *scanner,
+  const std::string &error)
 {
-  assembler_parser.parse_error(error, yyassemblertext);
+  assembler_parser.parse_error(error, yyassemblerget_text(scanner));
   return 0;
 }
+
+int yyassemblerlex_init_extra(assembler_parsert *, void **);
+int yyassemblerlex(void *);
+int yyassemblerlex_destroy(void *);
+
+bool assembler_parsert::parse()
+{
+  void *scanner;
+  yyassemblerlex_init_extra(this, &scanner);
+  yyassemblerlex(scanner);
+  yyassemblerlex_destroy(scanner);
+  return false;
+}

src/assembler/assembler_parser.h

@@ -14,9 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <list>
 
-int yyassemblerlex();
-int yyassemblererror(const std::string &error);
-void assembler_scanner_init();
+class assembler_parsert;
+int yyassemblererror(assembler_parsert &, void *, const std::string &error);
 
 class assembler_parsert:public parsert
 {
@@ -37,24 +36,18 @@ 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()
+  void clear() override
   {
     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

@@ -2,6 +2,9 @@
 %option noinput
 %option nounistd
 %option never-interactive
+%option noyywrap
+%option reentrant
+%option extra-type="assembler_parsert *"
 
 %{
 
@@ -13,7 +16,7 @@
 #pragma warning(disable:4005)
 #endif
 
-#define PARSER assembler_parser
+#define PARSER (*yyextra)
 #define YYSTYPE unsigned
 #undef  ECHO
 #define ECHO
@@ -60,14 +63,6 @@ string_lit      ("L"|"u"|"U"|"u8")?["]{s_char}*["]
 %x GRAMMAR
 %x LINE_COMMENT
 
-%{
-void assemlber_scanner_init()
-{
-  YY_FLUSH_BUFFER;
-  BEGIN(0);
-}
-%}
-
 %%
 
 <INITIAL>.|\n   { BEGIN(GRAMMAR);
@@ -109,7 +104,3 @@ void assemlber_scanner_init()
 }
 
 <<EOF>>         { yyterminate(); /* done! */ }
-
-%%
-
-int yywrap() { return 1; }

src/cbmc/cbmc_parse_options.cpp

@@ -883,7 +883,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 << ")"
@@ -895,7 +895,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,