From 9495ab2e883ae7c8eb6f6026a4de827c723ffbe2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 20 Dec 2023 13:25:06 +0000 Subject: [PATCH] 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. --- .../goto-program-transformations.md | 3 +- src/assembler/assembler_parser.cpp | 24 +++++++++++---- src/assembler/assembler_parser.h | 19 ++++-------- src/assembler/remove_asm.cpp | 30 +++++++++++++------ src/assembler/remove_asm.h | 5 ++-- src/assembler/scanner.l | 17 +++-------- src/cbmc/cbmc_parse_options.cpp | 4 +-- .../goto_analyzer_parse_options.cpp | 4 +-- src/goto-diff/goto_diff_parse_options.cpp | 4 +-- .../goto_instrument_parse_options.cpp | 6 ++-- src/goto-synthesizer/cegis_verifier.cpp | 4 +-- src/libcprover-cpp/api.cpp | 4 +-- 12 files changed, 68 insertions(+), 56 deletions(-) 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,