Merge pull request #8139 from tautschnig/cleanup/assembler_parsert

assembler_parsert: construct with message handler

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

@@ -951,7 +951,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
@@ -1067,7 +1067,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 << ")"
@@ -1078,7 +1078,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,