diff --git a/doc/architectural/goto-program-transformations.md b/doc/architectural/goto-program-transformations.md
index a0447b7a9af..400168fd6bb 100644
--- a/doc/architectural/goto-program-transformations.md
+++ b/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
This pass has no predecessor.
diff --git a/src/assembler/assembler_parser.cpp b/src/assembler/assembler_parser.cpp
index 10200644d1d..1dcf25719f6 100644
--- a/src/assembler/assembler_parser.cpp
+++ b/src/assembler/assembler_parser.cpp
@@ -8,12 +8,26 @@ Author: Daniel Kroening, kroening@kroening.com
#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;
+}
diff --git a/src/assembler/assembler_parser.h b/src/assembler/assembler_parser.h
index 76f03c71aaf..28e0542a128 100644
--- a/src/assembler/assembler_parser.h
+++ b/src/assembler/assembler_parser.h
@@ -14,9 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
#include
-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
diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp
index 102c9524703..0979909f383 100644
--- a/src/assembler/remove_asm.cpp
+++ b/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)
diff --git a/src/assembler/remove_asm.h b/src/assembler/remove_asm.h
index 00b4346d285..e37ee640942 100644
--- a/src/assembler/remove_asm.h
+++ b/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 &);
diff --git a/src/assembler/scanner.l b/src/assembler/scanner.l
index d975de73315..614185472bb 100755
--- a/src/assembler/scanner.l
+++ b/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);
-}
-%}
-
%%
.|\n { BEGIN(GRAMMAR);
@@ -109,7 +104,3 @@ void assemlber_scanner_init()
}
<> { yyterminate(); /* done! */ }
-
-%%
-
-int yywrap() { return 1; }
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ea738a735ce..ae9c2876c9d 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/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(
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index f6463eca656..4c18f105002 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/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);
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 01068018927..97c98673100 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/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);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index cc78444fcd8..9957af70706 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/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(
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index 57bbfdf30fb..570fa2b9e0f 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -84,7 +84,7 @@ 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(
@@ -92,7 +92,7 @@ void cegis_verifiert::preprocess_goto_model()
// 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(
diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp
index 598da01eede..f2285331d22 100644
--- a/src/libcprover-cpp/api.cpp
+++ b/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,