From 5bbad539f96e4d42f64482eb3af0efe7884b3306 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. --- src/assembler/assembler_parser.cpp | 6 ++-- src/assembler/assembler_parser.h | 14 ++++----- src/assembler/remove_asm.cpp | 30 +++++++++++++------ src/assembler/remove_asm.h | 5 ++-- src/assembler/scanner.l | 16 +++++++--- 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 +-- 11 files changed, 58 insertions(+), 39 deletions(-) diff --git a/src/assembler/assembler_parser.cpp b/src/assembler/assembler_parser.cpp index 10200644d1de..0266de26ba9f 100644 --- a/src/assembler/assembler_parser.cpp +++ b/src/assembler/assembler_parser.cpp @@ -8,11 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #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; diff --git a/src/assembler/assembler_parser.h b/src/assembler/assembler_parser.h index 76f03c71aaf3..92d3a5d2023c 100644 --- a/src/assembler/assembler_parser.h +++ b/src/assembler/assembler_parser.h @@ -14,9 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -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,13 +37,14 @@ 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; } @@ -51,10 +52,7 @@ class assembler_parsert:public parsert { 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 102c9524703a..0979909f383c 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 00b4346d285f..e37ee6409426 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 d975de733155..74930ea7aef5 100755 --- a/src/assembler/scanner.l +++ b/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; } %} diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 5395a2eed4ce..97a5d76c1d64 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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( diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index f6463eca6569..4c18f105002b 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 010680189277..97c986731002 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 cc78444fcd8c..9957af707064 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 57bbfdf30fbb..570fa2b9e0f4 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 598da01eede9..f2285331d223 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,