From 82948a4b1c7b57d4e3b00acb417e2bce03afe768 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Feb 2019 04:23:04 +0000 Subject: [PATCH] languaget is not a messaget Pass a message handler as an argument to several of its functions, but do not construct a messaget object without a configured message handler as that is deprecated. --- .../src/janalyzer/janalyzer_parse_options.cpp | 8 +- jbmc/src/java_bytecode/README.md | 4 +- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 1 + .../java_bytecode/java_bytecode_language.cpp | 211 ++++++++++-------- .../java_bytecode/java_bytecode_language.h | 50 +++-- jbmc/src/java_bytecode/java_entry_point.cpp | 1 + jbmc/src/java_bytecode/lazy_goto_model.cpp | 5 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 8 +- .../java-testing-utils/load_java_class.cpp | 13 +- .../java_bytecode_language/language.cpp | 30 ++- .../parse_java_annotations.cpp | 6 +- src/ansi-c/ansi_c_language.cpp | 42 ++-- src/ansi-c/ansi_c_language.h | 28 ++- src/ansi-c/cprover_library.cpp | 6 +- src/cbmc/cbmc_parse_options.cpp | 13 +- src/cpp/cpp_language.cpp | 39 ++-- src/cpp/cpp_language.h | 24 +- src/goto-cc/compile.cpp | 10 +- .../contracts/memory_predicates.cpp | 6 +- src/goto-instrument/model_argc_argv.cpp | 6 +- src/goto-programs/initialize_goto_model.cpp | 17 +- .../rebuild_goto_start_function.cpp | 3 +- src/jsil/jsil_language.cpp | 38 ++-- src/jsil/jsil_language.h | 27 ++- .../json_symtab_language.cpp | 21 +- .../json_symtab_language.h | 32 ++- src/langapi/language.cpp | 2 +- src/langapi/language.h | 47 ++-- src/langapi/language_file.cpp | 42 ++-- src/langapi/language_file.h | 15 +- src/langapi/language_util.cpp | 8 +- .../statement_list_language.cpp | 30 ++- src/statement-list/statement_list_language.h | 29 ++- src/symtab2gb/symtab2gb_parse_options.cpp | 6 +- unit/analyses/ai/ai_simplify_lhs.cpp | 6 +- unit/testing-utils/get_goto_model_from_c.cpp | 7 +- 36 files changed, 489 insertions(+), 352 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index aeabc8f7650..54f37bc1b0a 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -376,18 +376,18 @@ int janalyzer_parse_optionst::doit() { std::unique_ptr language = get_language_from_mode(ID_java); CHECK_RETURN(language != nullptr); - language->set_language_options(options); - language->set_message_handler(ui_message_handler); + language->set_language_options(options, ui_message_handler); log.status() << "Parsing ..." << messaget::eom; - if(static_cast(language.get())->parse()) + if(static_cast(language.get()) + ->parse(ui_message_handler)) { log.error() << "PARSING ERROR" << messaget::eom; return CPROVER_EXIT_PARSE_ERROR; } - language->show_parse(std::cout); + language->show_parse(std::cout, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index 105c61fb77c..ccb0445f864 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -674,10 +674,10 @@ determine which loading strategy to use. If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is \ref LAZY_METHODS_MODE_EAGER then eager loading is used. Under eager loading -\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &) +\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &) is called once for each method listed in method_bytecode (described above). This then calls -\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt, lazy_class_to_declared_symbols_mapt &); +\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt, lazy_class_to_declared_symbols_mapt &, message_handlert &); without a ci_lazy_methods_neededt object, which calls \ref java_bytecode_convert_method, passing in the method parse tree. This in diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 048866bd40c..db24a2579c0 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -9,6 +9,7 @@ Author: Diffblue Ltd. #include "ci_lazy_methods.h" #include +#include #include #include #include diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index dd19585c248..389c1555ba4 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -142,7 +142,7 @@ void lazy_class_to_declared_symbols_mapt::reinitialize() java_bytecode_language_optionst::java_bytecode_language_optionst( const optionst &options, - messaget &log) + message_handlert &message_handler) { assume_inputs_non_null = options.get_bool_option("java-assume-inputs-non-null"); @@ -200,10 +200,10 @@ java_bytecode_language_optionst::java_bytecode_language_optionst( { jsont json_cp_config; if(parse_json( - java_cp_include_files.substr(1), - log.get_message_handler(), - json_cp_config)) + java_cp_include_files.substr(1), message_handler, json_cp_config)) + { throw "cannot read JSON input configuration for JAR loading"; + } if(!json_cp_config.is_object()) throw "the JSON file has a wrong format"; @@ -230,7 +230,8 @@ java_bytecode_language_optionst::java_bytecode_language_optionst( { const std::string filename = options.get_option("static-values"); jsont tmp_json; - if(parse_json(filename, log.get_message_handler(), tmp_json)) + messaget log{message_handler}; + if(parse_json(filename, message_handler, tmp_json)) { log.warning() << "Provided JSON file for static-values cannot be parsed; it" @@ -258,10 +259,12 @@ java_bytecode_language_optionst::java_bytecode_language_optionst( } /// Consume options that are java bytecode specific. -void java_bytecode_languaget::set_language_options(const optionst &options) +void java_bytecode_languaget::set_language_options( + const optionst &options, + message_handlert &message_handler) { object_factory_parameters.set(options); - language_options = java_bytecode_language_optionst{options, *this}; + language_options = java_bytecode_language_optionst{options, message_handler}; const auto &new_points = build_extra_entry_points(options); language_options->extra_methods.insert( language_options->extra_methods.end(), @@ -283,24 +286,20 @@ void java_bytecode_languaget::modules_provided(std::set &) bool java_bytecode_languaget::preprocess( std::istream &, const std::string &, - std::ostream &) + std::ostream &, + message_handlert &) { // there is no preprocessing! return true; } -void java_bytecode_languaget::set_message_handler( +void java_bytecode_languaget::initialize_class_loader( message_handlert &message_handler) -{ - languaget::set_message_handler(message_handler); -} - -void java_bytecode_languaget::initialize_class_loader() { java_class_loader.clear_classpath(); for(const auto &p : config.java.classpath) - java_class_loader.add_classpath_entry(p, get_message_handler()); + java_class_loader.add_classpath_entry(p, message_handler); java_class_loader.set_java_cp_include_files( language_options->java_cp_include_files); @@ -323,13 +322,17 @@ static void throwMainClassLoadingError(const std::string &main_class) "Error: Could not find or load main class " + main_class); } -void java_bytecode_languaget::parse_from_main_class() +void java_bytecode_languaget::parse_from_main_class( + message_handlert &message_handler) { + messaget log{message_handler}; + if(!main_class.empty()) { // Try to load class - status() << "Trying to load Java main class: " << main_class << eom; - if(!java_class_loader.can_load_class(main_class, get_message_handler())) + log.status() << "Trying to load Java main class: " << main_class + << messaget::eom; + if(!java_class_loader.can_load_class(main_class, message_handler)) { // Try to extract class name and load class const auto maybe_class_name = @@ -339,10 +342,10 @@ void java_bytecode_languaget::parse_from_main_class() throwMainClassLoadingError(id2string(main_class)); return; } - status() << "Trying to load Java main class: " << maybe_class_name.value() - << eom; + log.status() << "Trying to load Java main class: " + << maybe_class_name.value() << messaget::eom; if(!java_class_loader.can_load_class( - maybe_class_name.value(), get_message_handler())) + maybe_class_name.value(), message_handler)) { throwMainClassLoadingError(id2string(main_class)); return; @@ -352,10 +355,9 @@ void java_bytecode_languaget::parse_from_main_class() config.main = id2string(main_class); main_class = maybe_class_name.value(); } - status() << "Found Java main class: " << main_class << eom; + log.status() << "Found Java main class: " << main_class << messaget::eom; // Now really load it. - const auto &parse_trees = - java_class_loader(main_class, get_message_handler()); + const auto &parse_trees = java_class_loader(main_class, message_handler); if(parse_trees.empty() || !parse_trees.front().loading_successful) { throwMainClassLoadingError(id2string(main_class)); @@ -365,12 +367,12 @@ void java_bytecode_languaget::parse_from_main_class() /// We set the main class (i.e.\ class to start the class loading analysis, /// see \ref java_class_loadert) when we have have been given a main class. -bool java_bytecode_languaget::parse() +bool java_bytecode_languaget::parse(message_handlert &message_handler) { PRECONDITION(language_options.has_value()); - initialize_class_loader(); + initialize_class_loader(message_handler); main_class = config.java.main_class; - parse_from_main_class(); + parse_from_main_class(message_handler); return false; } @@ -382,10 +384,11 @@ bool java_bytecode_languaget::parse() /// If no main class was found, all classes in the JAR file are loaded. bool java_bytecode_languaget::parse( std::istream &instream, - const std::string &path) + const std::string &path, + message_handlert &message_handler) { PRECONDITION(language_options.has_value()); - initialize_class_loader(); + initialize_class_loader(message_handler); // look at extension if(has_suffix(path, ".jar")) @@ -398,7 +401,7 @@ bool java_bytecode_languaget::parse( // build an object to potentially limit which classes are loaded java_class_loader_limitt class_loader_limit( - get_message_handler(), language_options->java_cp_include_files); + message_handler, language_options->java_cp_include_files); if(config.java.main_class.empty()) { // If we have an entry method, we can derive a main class. @@ -428,19 +431,21 @@ bool java_bytecode_languaget::parse( // do we have one now? if(main_class.empty()) { - status() << "JAR file without entry point: loading class files" << eom; + messaget log{message_handler}; + log.status() << "JAR file without entry point: loading class files" + << messaget::eom; const auto classes = - java_class_loader.load_entire_jar(path, get_message_handler()); + java_class_loader.load_entire_jar(path, message_handler); for(const auto &c : classes) main_jar_classes.push_back(c); } else - java_class_loader.add_classpath_entry(path, get_message_handler()); + java_class_loader.add_classpath_entry(path, message_handler); } else main_class = config.java.main_class; - parse_from_main_class(); + parse_from_main_class(message_handler); return false; } @@ -801,7 +806,8 @@ static void create_stub_global_symbols( bool java_bytecode_languaget::typecheck( symbol_table_baset &symbol_table, - const std::string &) + const std::string &, + message_handlert &message_handler) { PRECONDITION(language_options.has_value()); // There are various cases in the Java front-end where pre-existing symbols @@ -830,7 +836,7 @@ bool java_bytecode_languaget::typecheck( if(java_bytecode_convert_class( it->second, symbol_table, - get_message_handler(), + message_handler, language_options->max_user_array_length, method_bytecode, string_preprocess, @@ -850,7 +856,7 @@ bool java_bytecode_languaget::typecheck( if(java_bytecode_convert_class( class_trees.second, symbol_table, - get_message_handler(), + message_handler, language_options->max_user_array_length, method_bytecode, string_preprocess, @@ -892,7 +898,7 @@ bool java_bytecode_languaget::typecheck( method_bytecode.get(id)->get().method.instructions, symbol_table, synthetic_methods, - get_message_handler()); + message_handler); } } @@ -913,10 +919,10 @@ bool java_bytecode_languaget::typecheck( } catch(missing_outer_class_symbol_exceptiont &) { - messaget::warning() - << "Not marking class " << c.first - << " implicitly generic due to missing outer class symbols" - << messaget::eom; + messaget log(message_handler); + log.warning() << "Not marking class " << c.first + << " implicitly generic due to missing outer class symbols" + << messaget::eom; } } @@ -942,10 +948,11 @@ bool java_bytecode_languaget::typecheck( parse_tree, symbol_table, language_options->string_refinement_enabled); } } - status() << "Java: added " - << (symbol_table.symbols.size() - before_constant_globals_size) - << " String or Class constant symbols" - << messaget::eom; + + messaget log(message_handler); + log.status() << "Java: added " + << (symbol_table.symbols.size() - before_constant_globals_size) + << " String or Class constant symbols" << messaget::eom; // For each reference to a stub global (that is, a global variable declared on // a class we don't have bytecode for, and therefore don't know the static @@ -964,7 +971,7 @@ bool java_bytecode_languaget::typecheck( for(const java_bytecode_parse_treet &parse_tree : class_to_trees.second) { create_stub_global_symbols( - parse_tree, symbol_table_journal, class_hierarchy, *this); + parse_tree, symbol_table_journal, class_hierarchy, log); } } @@ -986,7 +993,7 @@ bool java_bytecode_languaget::typecheck( { case LAZY_METHODS_MODE_CONTEXT_INSENSITIVE: // ci = context-insensitive - if(do_ci_lazy_method_conversion(symbol_table)) + if(do_ci_lazy_method_conversion(symbol_table, message_handler)) return true; break; case LAZY_METHODS_MODE_EAGER: @@ -1003,21 +1010,29 @@ bool java_bytecode_languaget::typecheck( convert_single_method( function_id_and_type.first, journalling_symbol_table, - class_to_declared_symbols); + class_to_declared_symbols, + message_handler); } // Convert all methods for which we have bytecode now for(const auto &method_sig : method_bytecode) { convert_single_method( - method_sig.first, journalling_symbol_table, class_to_declared_symbols); + method_sig.first, + journalling_symbol_table, + class_to_declared_symbols, + message_handler); } convert_single_method( - INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols); + INITIALIZE_FUNCTION, + journalling_symbol_table, + class_to_declared_symbols, + message_handler); // Now convert all newly added string methods for(const auto &fn_name : journalling_symbol_table.get_inserted()) { if(string_preprocess.implements_function(fn_name)) - convert_single_method(fn_name, symbol_table, class_to_declared_symbols); + convert_single_method( + fn_name, symbol_table, class_to_declared_symbols, message_handler); } } break; @@ -1028,42 +1043,40 @@ bool java_bytecode_languaget::typecheck( // now instrument runtime exceptions java_bytecode_instrument( - symbol_table, - language_options->throw_runtime_exceptions, - get_message_handler()); + symbol_table, language_options->throw_runtime_exceptions, message_handler); // now typecheck all bool res = java_bytecode_typecheck( - symbol_table, - get_message_handler(), - language_options->string_refinement_enabled); + symbol_table, message_handler, language_options->string_refinement_enabled); // now instrument thread-blocks and synchronized methods. if(language_options->threading_support) { convert_threadblock(symbol_table); - convert_synchronized_methods(symbol_table, get_message_handler()); + convert_synchronized_methods(symbol_table, message_handler); } return res; } bool java_bytecode_languaget::generate_support_functions( - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { PRECONDITION(language_options.has_value()); symbol_table_buildert symbol_table_builder = symbol_table_buildert::wrap(symbol_table); - main_function_resultt res= - get_main_symbol(symbol_table, main_class, get_message_handler()); + main_function_resultt res = + get_main_symbol(symbol_table, main_class, message_handler); if(!res.is_success()) return res.is_error(); // Load the main function into the symbol table to get access to its // parameter names - convert_lazy_method(res.main_function.name, symbol_table_builder); + convert_lazy_method( + res.main_function.name, symbol_table_builder, message_handler); const symbolt &symbol = symbol_table_builder.lookup_ref(res.main_function.name); @@ -1080,7 +1093,7 @@ bool java_bytecode_languaget::generate_support_functions( return java_entry_point( symbol_table_builder, main_class, - get_message_handler(), + message_handler, language_options->assume_inputs_non_null, language_options->assert_uncaught_exceptions, object_factory_parameters, @@ -1093,7 +1106,7 @@ bool java_bytecode_languaget::generate_support_functions( language_options->assume_inputs_non_null, object_factory_parameters, get_pointer_type_selector(), - get_message_handler()); + message_handler); }); } @@ -1105,11 +1118,13 @@ bool java_bytecode_languaget::generate_support_functions( /// instantiated (or evidence that an object of that type exists before the main /// function is entered, such as being passed as a parameter). /// \param symbol_table: global symbol table +/// \param message_handler: message handler /// \return Elaborates lazily-converted methods that may be reachable starting /// from the main entry point (usually provided with the --function command- /// line option) (side-effect on the symbol_table). Returns false on success. bool java_bytecode_languaget::do_ci_lazy_method_conversion( - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { symbol_table_buildert symbol_table_builder = symbol_table_buildert::wrap(symbol_table); @@ -1117,14 +1132,15 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion( lazy_class_to_declared_symbols_mapt class_to_declared_symbols; const method_convertert method_converter = - [this, &symbol_table_builder, &class_to_declared_symbols]( + [this, &symbol_table_builder, &class_to_declared_symbols, &message_handler]( const irep_idt &function_id, ci_lazy_methods_neededt lazy_methods_needed) { return convert_single_method( function_id, symbol_table_builder, std::move(lazy_methods_needed), - class_to_declared_symbols); + class_to_declared_symbols, + message_handler); }; ci_lazy_methodst method_gather( @@ -1138,7 +1154,7 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion( synthetic_methods); return method_gather( - symbol_table, method_bytecode, method_converter, get_message_handler()); + symbol_table, method_bytecode, method_converter, message_handler); } const select_pointer_typet & @@ -1177,9 +1193,11 @@ void java_bytecode_languaget::methods_provided( /// using eager method conversion. /// \param function_id: method ID to convert /// \param symtab: global symbol table +/// \param message_handler: message handler void java_bytecode_languaget::convert_lazy_method( const irep_idt &function_id, - symbol_table_baset &symtab) + symbol_table_baset &symtab, + message_handlert &message_handler) { const symbolt &symbol = symtab.lookup_ref(function_id); if(symbol.value.is_not_nil()) @@ -1189,7 +1207,8 @@ void java_bytecode_languaget::convert_lazy_method( journalling_symbol_tablet::wrap(symtab); lazy_class_to_declared_symbols_mapt class_to_declared_symbols; - convert_single_method(function_id, symbol_table, class_to_declared_symbols); + convert_single_method( + function_id, symbol_table, class_to_declared_symbols, message_handler); // Instrument runtime exceptions (unless symbol is a stub or is the // INITIALISE_FUNCTION). @@ -1199,14 +1218,12 @@ void java_bytecode_languaget::convert_lazy_method( symbol_table, symbol_table.get_writeable_ref(function_id), language_options->throw_runtime_exceptions, - get_message_handler()); + message_handler); } // now typecheck this function java_bytecode_typecheck_updated_symbols( - symbol_table, - get_message_handler(), - language_options->string_refinement_enabled); + symbol_table, message_handler, language_options->string_refinement_enabled); } /// Notify ci_lazy_methods, if present, of any static function calls made by @@ -1274,11 +1291,13 @@ static void notify_static_method_calls( /// update with any methods touched during the conversion /// \param class_to_declared_symbols: maps classes to the symbols that /// they declare. +/// \param message_handler: message handler bool java_bytecode_languaget::convert_single_method( const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt needed_lazy_methods, - lazy_class_to_declared_symbols_mapt &class_to_declared_symbols) + lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, + message_handlert &message_handler) { const symbolt &symbol = symbol_table.lookup_ref(function_id); @@ -1295,14 +1314,18 @@ bool java_bytecode_languaget::convert_single_method( object_factory_parameters, *pointer_type_selector, language_options->string_refinement_enabled, - get_message_handler()); + message_handler); return false; } INVARIANT(declaring_class(symbol), "Method must have a declaring class."); bool ret = convert_single_method_code( - function_id, symbol_table, needed_lazy_methods, class_to_declared_symbols); + function_id, + symbol_table, + needed_lazy_methods, + class_to_declared_symbols, + message_handler); if(symbol.value.is_not_nil() && language_options->should_lift_clinit_calls) { @@ -1327,11 +1350,13 @@ bool java_bytecode_languaget::convert_single_method( /// update with any methods touched during the conversion /// \param class_to_declared_symbols: maps classes to the symbols that /// they declare. +/// \param message_handler: message handler bool java_bytecode_languaget::convert_single_method_code( const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt needed_lazy_methods, - lazy_class_to_declared_symbols_mapt &class_to_declared_symbols) + lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, + message_handlert &message_handler) { const auto &symbol = symbol_table.lookup_ref(function_id); PRECONDITION(symbol.value.is_nil()); @@ -1353,7 +1378,7 @@ bool java_bytecode_languaget::convert_single_method_code( } // Populate body of the function with code generated by string preprocess codet generated_code = string_preprocess.code_for_function( - writable_symbol, symbol_table, get_message_handler()); + writable_symbol, symbol_table, message_handler); // String solver can make calls to functions that haven't yet been seen. // Add these to the needed_lazy_methods collection notify_static_method_calls(generated_code, needed_lazy_methods); @@ -1378,7 +1403,7 @@ bool java_bytecode_languaget::convert_single_method_code( language_options->static_values_json.has_value(), object_factory_parameters, get_pointer_type_selector(), - get_message_handler()); + message_handler); else writable_symbol.value = get_clinit_wrapper_body( function_id, @@ -1387,7 +1412,7 @@ bool java_bytecode_languaget::convert_single_method_code( language_options->static_values_json.has_value(), object_factory_parameters, get_pointer_type_selector(), - get_message_handler()); + message_handler); break; case synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER: { @@ -1415,15 +1440,15 @@ bool java_bytecode_languaget::convert_single_method_code( symbol_table, object_factory_parameters, get_pointer_type_selector(), - get_message_handler()); + message_handler); break; case synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR: writable_symbol.value = invokedynamic_synthetic_constructor( - function_id, symbol_table, get_message_handler()); + function_id, symbol_table, message_handler); break; case synthetic_method_typet::INVOKEDYNAMIC_METHOD: writable_symbol.value = invokedynamic_synthetic_method( - function_id, symbol_table, get_message_handler()); + function_id, symbol_table, message_handler); break; case synthetic_method_typet::CREATE_ARRAY_WITH_TYPE: { @@ -1433,8 +1458,8 @@ bool java_bytecode_languaget::convert_single_method_code( "we have a real implementation available"); java_bytecode_initialize_parameter_names( writable_symbol, cmb->get().method.local_variable_table, symbol_table); - writable_symbol.value = create_array_with_type_body( - function_id, symbol_table, get_message_handler()); + writable_symbol.value = + create_array_with_type_body(function_id, symbol_table, message_handler); break; } } @@ -1453,7 +1478,7 @@ bool java_bytecode_languaget::convert_single_method_code( symbol_table.lookup_ref(cmb->get().class_id), cmb->get().method, symbol_table, - get_message_handler(), + message_handler, language_options->max_user_array_length, language_options->throw_assertion_error, std::move(needed_lazy_methods), @@ -1497,10 +1522,12 @@ bool java_bytecode_languaget::final(symbol_table_baset &) return false; } -void java_bytecode_languaget::show_parse(std::ostream &out) +void java_bytecode_languaget::show_parse( + std::ostream &out, + message_handlert &message_handler) { java_class_loadert::parse_tree_with_overlayst &parse_trees = - java_class_loader(main_class, get_message_handler()); + java_class_loader(main_class, message_handler); parse_trees.front().output(out); if(parse_trees.size() > 1) { @@ -1542,7 +1569,8 @@ bool java_bytecode_languaget::to_expr( const std::string &code, const std::string &module, exprt &expr, - const namespacet &ns) + const namespacet &ns, + message_handlert &message_handler) { #if 0 expr.make_nil(); @@ -1586,6 +1614,7 @@ bool java_bytecode_languaget::to_expr( (void)module; (void)expr; (void)ns; + (void)message_handler; #endif return true; // fail for now diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 22189337dc1..45a0f69534c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -201,7 +201,7 @@ class lazy_class_to_declared_symbols_mapt struct java_bytecode_language_optionst { - java_bytecode_language_optionst(const optionst &options, messaget &log); + java_bytecode_language_optionst(const optionst &options, message_handlert &); java_bytecode_language_optionst() = default; @@ -260,33 +260,37 @@ struct java_bytecode_language_optionst class java_bytecode_languaget:public languaget { public: - void set_language_options(const optionst &) override; - - void set_message_handler(message_handlert &message_handler) override; + void set_language_options(const optionst &, message_handlert &) override; virtual bool preprocess( std::istream &instream, const std::string &path, - std::ostream &outstream) override; + std::ostream &outstream, + message_handlert &message_handler) override; // This is an extension to languaget // required because parsing of Java programs can be initiated without // opening a file first or providing a path to a file // as dictated by \ref languaget. - virtual bool parse(); + virtual bool parse(message_handlert &); bool parse( std::istream &instream, - const std::string &path) override; + const std::string &path, + message_handlert &message_handler) override; - bool generate_support_functions(symbol_table_baset &symbol_table) override; + bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &message_handler) override; - bool - typecheck(symbol_table_baset &context, const std::string &module) override; + bool typecheck( + symbol_table_baset &context, + const std::string &module, + message_handlert &message_handler) override; virtual bool final(symbol_table_baset &context) override; - void show_parse(std::ostream &out) override; + void show_parse(std::ostream &out, message_handlert &) override; virtual ~java_bytecode_languaget(); java_bytecode_languaget( @@ -316,7 +320,8 @@ class java_bytecode_languaget:public languaget const std::string &code, const std::string &module, exprt &expr, - const namespacet &ns) override; + const namespacet &ns, + message_handlert &message_handler) override; std::unique_ptr new_language() override { return util_make_unique(); } @@ -330,32 +335,37 @@ class java_bytecode_languaget:public languaget methods_provided(std::unordered_set &methods) const override; virtual void convert_lazy_method( const irep_idt &function_id, - symbol_table_baset &symbol_table) override; + symbol_table_baset &symbol_table, + message_handlert &message_handler) override; protected: void convert_single_method( const irep_idt &function_id, symbol_table_baset &symbol_table, - lazy_class_to_declared_symbols_mapt &class_to_declared_symbols) + lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, + message_handlert &message_handler) { convert_single_method( function_id, symbol_table, optionalt(), - class_to_declared_symbols); + class_to_declared_symbols, + message_handler); } bool convert_single_method( const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt needed_lazy_methods, - lazy_class_to_declared_symbols_mapt &class_to_declared_symbols); + lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, + message_handlert &); bool convert_single_method_code( const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt needed_lazy_methods, - lazy_class_to_declared_symbols_mapt &class_to_declared_symbols); + lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, + message_handlert &); - bool do_ci_lazy_method_conversion(symbol_table_baset &); + bool do_ci_lazy_method_conversion(symbol_table_baset &, message_handlert &); const select_pointer_typet &get_pointer_type_selector() const; optionalt language_options; @@ -384,8 +394,8 @@ class java_bytecode_languaget:public languaget /// IDs of such objects to symbols that store their values. std::unordered_map references; - void parse_from_main_class(); - void initialize_class_loader(); + void parse_from_main_class(message_handlert &); + void initialize_class_loader(message_handlert &); }; std::unique_ptr new_java_bytecode_language(); diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 0477fb383d0..86c463480bc 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include diff --git a/jbmc/src/java_bytecode/lazy_goto_model.cpp b/jbmc/src/java_bytecode/lazy_goto_model.cpp index c3a183d74fe..66da36b57bd 100644 --- a/jbmc/src/java_bytecode/lazy_goto_model.cpp +++ b/jbmc/src/java_bytecode/lazy_goto_model.cpp @@ -141,12 +141,11 @@ void lazy_goto_modelt::initialize( CHECK_RETURN(lf.language != nullptr); languaget &language = *lf.language; - language.set_message_handler(message_handler); - language.set_language_options(options); + language.set_language_options(options, message_handler); msg.status() << "Parsing ..." << messaget::eom; - if(dynamic_cast(language).parse()) + if(dynamic_cast(language).parse(message_handler)) { throw invalid_input_exceptiont("PARSING ERROR"); } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index ef776c63f3c..88a2179f1a5 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -453,18 +453,18 @@ int jbmc_parse_optionst::doit() { std::unique_ptr language = get_language_from_mode(ID_java); CHECK_RETURN(language != nullptr); - language->set_language_options(options); - language->set_message_handler(ui_message_handler); + language->set_language_options(options, ui_message_handler); log.status() << "Parsing ..." << messaget::eom; - if(static_cast(language.get())->parse()) + if(static_cast(language.get()) + ->parse(ui_message_handler)) { log.error() << "PARSING ERROR" << messaget::eom; return CPROVER_EXIT_PARSE_ERROR; } - language->show_parse(std::cout); + language->show_parse(std::cout, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp index e1f1fcf787b..b2a0a40fa23 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.cpp +++ b/jbmc/unit/java-testing-utils/load_java_class.cpp @@ -115,7 +115,8 @@ goto_modelt load_goto_model_from_java_class( // Add the language to the model language_filet &lf=lazy_goto_model.add_language_file(filename); lf.language=std::move(java_lang); - languaget &language=*lf.language; + java_bytecode_languaget &language = + dynamic_cast(*lf.language); std::istringstream java_code_stream("ignored"); @@ -123,11 +124,11 @@ goto_modelt load_goto_model_from_java_class( parse_java_language_options(command_line, options); // Configure the language, load the class files - language.set_message_handler(null_message_handler); - language.set_language_options(options); - language.parse(java_code_stream, filename); - language.typecheck(lazy_goto_model.symbol_table, ""); - language.generate_support_functions(lazy_goto_model.symbol_table); + language.set_language_options(options, null_message_handler); + language.parse(java_code_stream, filename, null_message_handler); + language.typecheck(lazy_goto_model.symbol_table, "", null_message_handler); + language.generate_support_functions( + lazy_goto_model.symbol_table, null_message_handler); language.final(lazy_goto_model.symbol_table); lazy_goto_model.load_all_functions(); diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp index 229405787ba..1e6200fb62d 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp @@ -6,13 +6,15 @@ Author: Diffblue Limited. \*******************************************************************/ -#include - #include + +#include +#include + #include #include #include -#include +#include SCENARIO( "java_bytecode_language_opaque_field", @@ -47,25 +49,19 @@ SCENARIO( } } -static void use_external_driver(java_bytecode_languaget &language) -{ - optionst options; - options.set_option("symex-driven-lazy-loading", true); - language.set_language_options(options); -} - SCENARIO( "LAZY_METHODS_MODE_EXTERNAL_DRIVER based generation of cprover_initialise", "[core][java_bytecode_language]") { java_bytecode_languaget language; null_message_handlert null_message_handler; - language.set_message_handler(null_message_handler); - use_external_driver(language); + optionst options; + options.set_option("symex-driven-lazy-loading", true); + language.set_language_options(options, null_message_handler); symbol_tablet symbol_table; GIVEN("java_bytecode_languaget::typecheck is run.") { - language.typecheck(symbol_table, ""); + language.typecheck(symbol_table, "", null_message_handler); THEN("The " INITIALIZE_FUNCTION " is in the symbol table without code.") { const symbolt *const initialise = @@ -77,7 +73,8 @@ SCENARIO( "java_bytecode_languaget::convert_lazy_method is used to " "generate " INITIALIZE_FUNCTION) { - language.convert_lazy_method(INITIALIZE_FUNCTION, symbol_table); + language.convert_lazy_method( + INITIALIZE_FUNCTION, symbol_table, null_message_handler); THEN("The " INITIALIZE_FUNCTION " is in the symbol table with code.") { const symbolt *const initialise = @@ -95,12 +92,11 @@ TEST_CASE( { java_bytecode_languaget language; null_message_handlert null_message_handler; - language.set_message_handler(null_message_handler); - language.set_language_options(optionst{}); + language.set_language_options(optionst{}, null_message_handler); symbol_tablet symbol_table; GIVEN("java_bytecode_languaget::typecheck is run.") { - language.typecheck(symbol_table, ""); + language.typecheck(symbol_table, "", null_message_handler); THEN("The " INITIALIZE_FUNCTION " function is in the symbol table with code.") { diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp index dff5c035f41..7b7d6b3a098 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp @@ -174,14 +174,14 @@ SCENARIO( free_form_cmdlinet command_line; command_line.add_flag("no-lazy-methods"); test_java_bytecode_languaget language; - language.set_message_handler(null_message_handler); optionst options; parse_java_language_options(command_line, options); - language.set_language_options(options); + language.set_language_options(options, null_message_handler); config.java.main_class = "AnnotationsEverywhere"; std::istringstream java_code_stream("ignored"); - language.parse(java_code_stream, "AnnotationsEverywhere.class"); + language.parse( + java_code_stream, "AnnotationsEverywhere.class", null_message_handler); const java_class_loadert::parse_tree_with_overlayst &parse_trees = language.get_parse_trees_for_class("AnnotationsEverywhere"); REQUIRE(parse_trees.size() == 1); diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index cf82835ceb8..cfba92b8a82 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -39,18 +39,20 @@ void ansi_c_languaget::modules_provided(std::set &modules) bool ansi_c_languaget::preprocess( std::istream &instream, const std::string &path, - std::ostream &outstream) + std::ostream &outstream, + message_handlert &message_handler) { // stdin? if(path.empty()) - return c_preprocess(instream, outstream, get_message_handler()); + return c_preprocess(instream, outstream, message_handler); - return c_preprocess(path, outstream, get_message_handler()); + return c_preprocess(path, outstream, message_handler); } bool ansi_c_languaget::parse( std::istream &instream, - const std::string &path) + const std::string &path, + message_handlert &message_handler) { // store the path parse_path=path; @@ -58,7 +60,7 @@ bool ansi_c_languaget::parse( // preprocessing std::ostringstream o_preprocessed; - if(preprocess(instream, path, o_preprocessed)) + if(preprocess(instream, path, o_preprocessed, message_handler)) return true; std::istringstream i_preprocessed(o_preprocessed.str()); @@ -72,7 +74,7 @@ bool ansi_c_languaget::parse( ansi_c_parser.clear(); ansi_c_parser.set_file(ID_built_in); ansi_c_parser.in=&codestr; - ansi_c_parser.log.set_message_handler(get_message_handler()); + ansi_c_parser.log.set_message_handler(message_handler); ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope; ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types; ansi_c_parser.cpp98=false; // it's not C++ @@ -104,46 +106,45 @@ bool ansi_c_languaget::parse( bool ansi_c_languaget::typecheck( symbol_table_baset &symbol_table, const std::string &module, + message_handlert &message_handler, const bool keep_file_local) { - return typecheck(symbol_table, module, keep_file_local, {}); + return typecheck(symbol_table, module, message_handler, keep_file_local, {}); } bool ansi_c_languaget::typecheck( symbol_table_baset &symbol_table, const std::string &module, + message_handlert &message_handler, const bool keep_file_local, const std::set &keep) { symbol_tablet new_symbol_table; - if(ansi_c_typecheck( - parse_tree, - new_symbol_table, - module, - get_message_handler())) + if(ansi_c_typecheck(parse_tree, new_symbol_table, module, message_handler)) { return true; } remove_internal_symbols( - new_symbol_table, this->get_message_handler(), keep_file_local, keep); + new_symbol_table, message_handler, keep_file_local, keep); - if(linking(symbol_table, new_symbol_table, get_message_handler())) + if(linking(symbol_table, new_symbol_table, message_handler)) return true; return false; } bool ansi_c_languaget::generate_support_functions( - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { // This creates __CPROVER_start and __CPROVER_initialize: return ansi_c_entry_point( - symbol_table, get_message_handler(), object_factory_params); + symbol_table, message_handler, object_factory_params); } -void ansi_c_languaget::show_parse(std::ostream &out) +void ansi_c_languaget::show_parse(std::ostream &out, message_handlert &) { parse_tree.output(out); } @@ -184,7 +185,8 @@ bool ansi_c_languaget::to_expr( const std::string &code, const std::string &, exprt &expr, - const namespacet &ns) + const namespacet &ns, + message_handlert &message_handler) { expr.make_nil(); @@ -198,7 +200,7 @@ bool ansi_c_languaget::to_expr( ansi_c_parser.clear(); ansi_c_parser.set_file(irep_idt()); ansi_c_parser.in=&i_preprocessed; - ansi_c_parser.log.set_message_handler(get_message_handler()); + ansi_c_parser.log.set_message_handler(message_handler); ansi_c_parser.mode=config.ansi_c.mode; ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types; ansi_c_scanner_init(); @@ -212,7 +214,7 @@ bool ansi_c_languaget::to_expr( expr=ansi_c_parser.parse_tree.items.front().declarator().value(); // typecheck it - result=ansi_c_typecheck(expr, get_message_handler(), ns); + result = ansi_c_typecheck(expr, message_handler, ns); } // save some memory diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index db80e687549..e11f61d91f9 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -36,7 +36,8 @@ Author: Daniel Kroening, kroening@kroening.com class ansi_c_languaget:public languaget { public: - void set_language_options(const optionst &options) override + void + set_language_options(const optionst &options, message_handlert &) override { object_factory_params.set(options); } @@ -44,22 +45,28 @@ class ansi_c_languaget:public languaget bool preprocess( std::istream &instream, const std::string &path, - std::ostream &outstream) override; + std::ostream &outstream, + message_handlert &message_handler) override; bool parse( std::istream &instream, - const std::string &path) override; + const std::string &path, + message_handlert &message_handler) override; - bool generate_support_functions(symbol_table_baset &symbol_table) override; + bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &message_handler) override; bool typecheck( symbol_table_baset &symbol_table, const std::string &module, + message_handlert &message_handler, const bool keep_file_local) override; bool typecheck( symbol_table_baset &symbol_table, const std::string &module, + message_handlert &message_handler, const bool keep_file_local, const std::set &keep); @@ -68,13 +75,15 @@ class ansi_c_languaget:public languaget return true; } - bool typecheck(symbol_table_baset &symbol_table, const std::string &module) - override + bool typecheck( + symbol_table_baset &symbol_table, + const std::string &module, + message_handlert &message_handler) override { - return typecheck(symbol_table, module, true); + return typecheck(symbol_table, module, message_handler, true); } - void show_parse(std::ostream &out) override; + void show_parse(std::ostream &out, message_handlert &) override; ~ansi_c_languaget() override; ansi_c_languaget() { } @@ -98,7 +107,8 @@ class ansi_c_languaget:public languaget const std::string &code, const std::string &module, exprt &expr, - const namespacet &ns) override; + const namespacet &ns, + message_handlert &message_handler) override; std::unique_ptr new_language() override { return util_make_unique(); } diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index 9966e83e669..f9b932f53d6 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -123,10 +123,10 @@ void add_library( std::istringstream in(src); ansi_c_languaget ansi_c_language; - ansi_c_language.set_message_handler(message_handler); - ansi_c_language.parse(in, ""); + ansi_c_language.parse(in, "", message_handler); - ansi_c_language.typecheck(symbol_table, "", true, keep); + ansi_c_language.typecheck( + symbol_table, "", message_handler, true, keep); } void cprover_c_library_factory_force_load( diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e310b2a623e..0d9125319cf 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -523,18 +523,17 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - language->set_language_options(options); - language->set_message_handler(ui_message_handler); + language->set_language_options(options, ui_message_handler); log.status() << "Parsing " << filename << messaget::eom; - if(language->parse(infile, filename)) + if(language->parse(infile, filename, ui_message_handler)) { log.error() << "PARSING ERROR" << messaget::eom; return CPROVER_EXIT_INCORRECT_TASK; } - language->show_parse(std::cout); + language->show_parse(std::cout, ui_message_handler); return CPROVER_EXIT_SUCCESS; } @@ -793,7 +792,7 @@ void cbmc_parse_optionst::preprocessing(const optionst &options) } std::unique_ptr language = get_language_from_filename(filename); - language->set_language_options(options); + language->set_language_options(options, ui_message_handler); if(language == nullptr) { @@ -801,9 +800,7 @@ void cbmc_parse_optionst::preprocessing(const optionst &options) return; } - language->set_message_handler(ui_message_handler); - - if(language->preprocess(infile, filename, std::cout)) + if(language->preprocess(infile, filename, std::cout, ui_message_handler)) log.error() << "PREPROCESSING ERROR" << messaget::eom; } diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index 2e2119d83c8..a48fcbbaeef 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -57,10 +57,11 @@ void cpp_languaget::modules_provided(std::set &modules) bool cpp_languaget::preprocess( std::istream &instream, const std::string &path, - std::ostream &outstream) + std::ostream &outstream, + message_handlert &message_handler) { if(path.empty()) - return c_preprocess(instream, outstream, get_message_handler()); + return c_preprocess(instream, outstream, message_handler); // check extension @@ -77,12 +78,13 @@ bool cpp_languaget::preprocess( return false; } - return c_preprocess(path, outstream, get_message_handler()); + return c_preprocess(path, outstream, message_handler); } bool cpp_languaget::parse( std::istream &instream, - const std::string &path) + const std::string &path, + message_handlert &message_handler) { // store the path @@ -94,7 +96,7 @@ bool cpp_languaget::parse( cpp_internal_additions(o_preprocessed); - if(preprocess(instream, path, o_preprocessed)) + if(preprocess(instream, path, o_preprocessed, message_handler)) return true; std::istringstream i_preprocessed(o_preprocessed.str()); @@ -104,7 +106,7 @@ bool cpp_languaget::parse( cpp_parser.clear(); cpp_parser.set_file(path); cpp_parser.in=&i_preprocessed; - cpp_parser.log.set_message_handler(get_message_handler()); + cpp_parser.log.set_message_handler(message_handler); cpp_parser.mode=config.ansi_c.mode; bool result=cpp_parser.parse(); @@ -120,29 +122,31 @@ bool cpp_languaget::parse( bool cpp_languaget::typecheck( symbol_table_baset &symbol_table, - const std::string &module) + const std::string &module, + message_handlert &message_handler) { if(module.empty()) return false; symbol_tablet new_symbol_table; - if(cpp_typecheck( - cpp_parse_tree, new_symbol_table, module, get_message_handler())) + if(cpp_typecheck(cpp_parse_tree, new_symbol_table, module, message_handler)) return true; - remove_internal_symbols(new_symbol_table, get_message_handler(), false); + remove_internal_symbols(new_symbol_table, message_handler, false); - return linking(symbol_table, new_symbol_table, get_message_handler()); + return linking(symbol_table, new_symbol_table, message_handler); } -bool cpp_languaget::generate_support_functions(symbol_table_baset &symbol_table) +bool cpp_languaget::generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &message_handler) { return ansi_c_entry_point( - symbol_table, get_message_handler(), object_factory_params); + symbol_table, message_handler, object_factory_params); } -void cpp_languaget::show_parse(std::ostream &out) +void cpp_languaget::show_parse(std::ostream &out, message_handlert &) { for(const auto &i : cpp_parse_tree.items) show_parse(out, i); @@ -231,7 +235,8 @@ bool cpp_languaget::to_expr( const std::string &code, const std::string &, exprt &expr, - const namespacet &ns) + const namespacet &ns, + message_handlert &message_handler) { expr.make_nil(); @@ -244,7 +249,7 @@ bool cpp_languaget::to_expr( cpp_parser.clear(); cpp_parser.set_file(irep_idt()); cpp_parser.in=&i_preprocessed; - cpp_parser.log.set_message_handler(get_message_handler()); + cpp_parser.log.set_message_handler(message_handler); bool result=cpp_parser.parse(); @@ -256,7 +261,7 @@ bool cpp_languaget::to_expr( // expr.swap(cpp_parser.parse_tree.declarations.front()); // typecheck it - result=cpp_typecheck(expr, get_message_handler(), ns); + result = cpp_typecheck(expr, message_handler, ns); } // save some memory diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index a2133f9cf95..764c77af311 100644 --- a/src/cpp/cpp_language.h +++ b/src/cpp/cpp_language.h @@ -25,7 +25,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu class cpp_languaget:public languaget { public: - void set_language_options(const optionst &options) override + void + set_language_options(const optionst &options, message_handlert &) override { object_factory_params.set(options); } @@ -33,16 +34,22 @@ class cpp_languaget:public languaget bool preprocess( std::istream &instream, const std::string &path, - std::ostream &outstream) override; + std::ostream &outstream, + message_handlert &message_handler) override; bool parse( std::istream &instream, - const std::string &path) override; + const std::string &path, + message_handlert &message_handler) override; - bool generate_support_functions(symbol_table_baset &symbol_table) override; + bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &message_handler) override; - bool typecheck(symbol_table_baset &symbol_table, const std::string &module) - override; + bool typecheck( + symbol_table_baset &symbol_table, + const std::string &module, + message_handlert &message_handler) override; bool merge_symbol_table( symbol_table_baset &dest, @@ -50,7 +57,7 @@ class cpp_languaget:public languaget const std::string &module, class replace_symbolt &replace_symbol) const; - void show_parse(std::ostream &out) override; + void show_parse(std::ostream &out, message_handlert &) override; // constructor, destructor ~cpp_languaget() override; @@ -78,7 +85,8 @@ class cpp_languaget:public languaget const std::string &code, const std::string &module, exprt &expr, - const namespacet &ns) override; + const namespacet &ns, + message_handlert &message_handler) override; std::unique_ptr new_language() override { return util_make_unique(); } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 7823142a6b7..3d76ace4579 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -469,8 +469,6 @@ bool compilet::parse( return true; } - languagep->set_message_handler(log.get_message_handler()); - if(file_name == "-") return parse_stdin(*languagep); @@ -506,13 +504,13 @@ bool compilet::parse( } } - lf.language->preprocess(infile, file_name, *os); + lf.language->preprocess(infile, file_name, *os, log.get_message_handler()); } else { log.statistics() << "Parsing: " << file_name << messaget::eom; - if(lf.language->parse(infile, file_name)) + if(lf.language->parse(infile, file_name, log.get_message_handler())) { log.error() << "PARSING ERROR" << messaget::eom; return true; @@ -548,11 +546,11 @@ bool compilet::parse_stdin(languaget &language) } } - language.preprocess(std::cin, "", *os); + language.preprocess(std::cin, "", *os, log.get_message_handler()); } else { - if(language.parse(std::cin, "")) + if(language.parse(std::cin, "", log.get_message_handler())) { log.error() << "PARSING ERROR" << messaget::eom; return true; diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index 5784e31f169..d36da815fb2 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -172,14 +172,14 @@ void is_fresh_baset::add_declarations(const std::string &decl_string) std::istringstream iss(decl_string); ansi_c_languaget ansi_c_language; - ansi_c_language.set_message_handler(message_handler); configt::ansi_ct::preprocessort pp = config.ansi_c.preprocessor; config.ansi_c.preprocessor = configt::ansi_ct::preprocessort::NONE; - ansi_c_language.parse(iss, ""); + ansi_c_language.parse(iss, "", log.get_message_handler()); config.ansi_c.preprocessor = pp; symbol_tablet tmp_symbol_table; - ansi_c_language.typecheck(tmp_symbol_table, ""); + ansi_c_language.typecheck( + tmp_symbol_table, "", log.get_message_handler()); exprt value = nil_exprt(); goto_functionst tmp_functions; diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index ca3c5d1e26b..1875f2e2495 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -105,14 +105,14 @@ bool model_argc_argv( std::istringstream iss(oss.str()); ansi_c_languaget ansi_c_language; - ansi_c_language.set_message_handler(message_handler); configt::ansi_ct::preprocessort pp=config.ansi_c.preprocessor; config.ansi_c.preprocessor=configt::ansi_ct::preprocessort::NONE; - ansi_c_language.parse(iss, ""); + ansi_c_language.parse(iss, "", message_handler); config.ansi_c.preprocessor=pp; symbol_tablet tmp_symbol_table; - ansi_c_language.typecheck(tmp_symbol_table, ""); + ansi_c_language.typecheck( + tmp_symbol_table, "", message_handler); goto_programt init_instructions; exprt value=nil_exprt(); diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index b5d420cc308..11c0870f1f7 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -52,9 +52,9 @@ static bool generate_entry_point_for_function( PRECONDITION(!entry_point_mode.empty()); auto const entry_language = get_language_from_mode(entry_point_mode); CHECK_RETURN(entry_language != nullptr); - entry_language->set_message_handler(message_handler); - entry_language->set_language_options(options); - return entry_language->generate_support_functions(symbol_table); + entry_language->set_language_options(options, message_handler); + return entry_language->generate_support_functions( + symbol_table, message_handler); } void initialize_from_source_files( @@ -88,12 +88,11 @@ void initialize_from_source_files( } languaget &language = *lf.language; - language.set_message_handler(message_handler); - language.set_language_options(options); + language.set_language_options(options, message_handler); msg.status() << "Parsing " << filename << messaget::eom; - if(language.parse(infile, filename)) + if(language.parse(infile, filename, message_handler)) { throw invalid_input_exceptiont("PARSING ERROR"); } @@ -137,7 +136,7 @@ void set_up_custom_entry_point( // Create the new entry-point entry_point_generation_failed = - language->generate_support_functions(symbol_table); + language->generate_support_functions(symbol_table, message_handler); // Remove the function from the goto functions so it is copied back in // from the symbol table during goto_convert @@ -159,8 +158,8 @@ void set_up_custom_entry_point( { // Allow all language front-ends to try to provide the user-specified // (--function) entry-point, or some language-specific default: - entry_point_generation_failed = - language_files.generate_support_functions(symbol_table); + entry_point_generation_failed = language_files.generate_support_functions( + symbol_table, message_handler); } } diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index ea59938b423..d7f0762fe23 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -32,8 +32,7 @@ std::unique_ptr get_entry_point_language( std::unique_ptr language = get_language_from_mode(mode); // This might fail if the driver program hasn't registered that language. INVARIANT(language, "No language found for mode: " + id2string(mode)); - language->set_message_handler(message_handler); - language->set_language_options(options); + language->set_language_options(options, message_handler); return language; } diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index 58caa64c018..fe457f8d295 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -32,9 +32,11 @@ void jsil_languaget::modules_provided(std::set &modules) } /// Adding symbols for all procedure declarations -bool jsil_languaget::interfaces(symbol_table_baset &symbol_table) +bool jsil_languaget::interfaces( + symbol_table_baset &symbol_table, + message_handlert &message_handler) { - if(jsil_convert(parse_tree, symbol_table, get_message_handler())) + if(jsil_convert(parse_tree, symbol_table, message_handler)) return true; jsil_internal_additions(symbol_table); @@ -44,7 +46,8 @@ bool jsil_languaget::interfaces(symbol_table_baset &symbol_table) bool jsil_languaget::preprocess( std::istream &, const std::string &, - std::ostream &) + std::ostream &, + message_handlert &) { // there is no preprocessing! return true; @@ -52,7 +55,8 @@ bool jsil_languaget::preprocess( bool jsil_languaget::parse( std::istream &instream, - const std::string &path) + const std::string &path, + message_handlert &message_handler) { // store the path parse_path=path; @@ -61,7 +65,7 @@ bool jsil_languaget::parse( jsil_parser.clear(); jsil_parser.set_file(path); jsil_parser.in=&instream; - jsil_parser.log.set_message_handler(get_message_handler()); + jsil_parser.log.set_message_handler(message_handler); jsil_scanner_init(); bool result=jsil_parser.parse(); @@ -78,23 +82,23 @@ bool jsil_languaget::parse( /// Converting from parse tree and type checking. bool jsil_languaget::typecheck( symbol_table_baset &symbol_table, - const std::string &) + const std::string &, + message_handlert &message_handler) { - if(jsil_typecheck(symbol_table, get_message_handler())) + if(jsil_typecheck(symbol_table, message_handler)) return true; return false; } bool jsil_languaget::generate_support_functions( - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { - return jsil_entry_point( - symbol_table, - get_message_handler()); + return jsil_entry_point(symbol_table, message_handler); } -void jsil_languaget::show_parse(std::ostream &out) +void jsil_languaget::show_parse(std::ostream &out, message_handlert &) { parse_tree.output(out); } @@ -126,7 +130,8 @@ bool jsil_languaget::to_expr( const std::string &code, const std::string &, exprt &expr, - const namespacet &ns) + const namespacet &ns, + message_handlert &message_handler) { expr.make_nil(); std::istringstream instream(code); @@ -136,7 +141,7 @@ bool jsil_languaget::to_expr( jsil_parser.clear(); jsil_parser.set_file(irep_idt()); jsil_parser.in=&instream; - jsil_parser.log.set_message_handler(get_message_handler()); + jsil_parser.log.set_message_handler(message_handler); jsil_scanner_init(); bool result=jsil_parser.parse(); @@ -146,8 +151,7 @@ bool jsil_languaget::to_expr( else { symbol_tablet symbol_table; - result= - jsil_convert(parse_tree, symbol_table, get_message_handler()); + result = jsil_convert(parse_tree, symbol_table, message_handler); if(symbol_table.symbols.size()!=1) result=true; @@ -157,7 +161,7 @@ bool jsil_languaget::to_expr( // typecheck it if(!result) - result=jsil_typecheck(expr, get_message_handler(), ns); + result = jsil_typecheck(expr, message_handler, ns); } // save some memory diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 7138620118b..80271b4fc21 100644 --- a/src/jsil/jsil_language.h +++ b/src/jsil/jsil_language.h @@ -26,16 +26,24 @@ class jsil_languaget:public languaget bool preprocess( std::istream &instream, const std::string &path, - std::ostream &outstream) override; + std::ostream &outstream, + message_handlert &) override; - bool parse(std::istream &instream, const std::string &path) override; + bool parse( + std::istream &instream, + const std::string &path, + message_handlert &message_handler) override; - bool generate_support_functions(symbol_table_baset &symbol_table) override; + bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &message_handler) override; - bool - typecheck(symbol_table_baset &context, const std::string &module) override; + bool typecheck( + symbol_table_baset &context, + const std::string &module, + message_handlert &message_handler) override; - void show_parse(std::ostream &out) override; + void show_parse(std::ostream &out, message_handlert &) override; virtual ~jsil_languaget(); jsil_languaget() { } @@ -50,7 +58,8 @@ class jsil_languaget:public languaget const std::string &code, const std::string &module, exprt &expr, - const namespacet &ns) override; + const namespacet &ns, + message_handlert &message_handler) override; std::unique_ptr new_language() override { return util_make_unique(); } @@ -64,7 +73,9 @@ class jsil_languaget:public languaget std::set extensions() const override; void modules_provided(std::set &modules) override; - bool interfaces(symbol_table_baset &symbol_table) override; + bool interfaces( + symbol_table_baset &symbol_table, + message_handlert &message_handler) override; protected: jsil_parse_treet parse_tree; diff --git a/src/json-symtab-language/json_symtab_language.cpp b/src/json-symtab-language/json_symtab_language.cpp index 4bd0e6ef83b..05bbc3c888b 100644 --- a/src/json-symtab-language/json_symtab_language.cpp +++ b/src/json-symtab-language/json_symtab_language.cpp @@ -20,21 +20,25 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// Parse a goto program in json form. /// \param instream: The input stream /// \param path: A file path +/// \param message_handler: A message handler /// \return boolean signifying success or failure of the parsing bool json_symtab_languaget::parse( std::istream &instream, - const std::string &path) + const std::string &path, + message_handlert &message_handler) { - return parse_json(instream, path, get_message_handler(), parsed_json_file); + return parse_json(instream, path, message_handler, parsed_json_file); } /// Typecheck a goto program in json form. /// \param symbol_table: The symbol table containing symbols read from file. /// \param module: A useless parameter, there for interface consistency. +/// \param message_handler: A message handler /// \return boolean signifying success or failure of the typechecking. bool json_symtab_languaget::typecheck( symbol_table_baset &symbol_table, - const std::string &module) + const std::string &module, + message_handlert &message_handler) { (void)module; // unused parameter @@ -43,11 +47,12 @@ bool json_symtab_languaget::typecheck( try { symbol_table_from_json(parsed_json_file, new_symbol_table); - return linking(symbol_table, new_symbol_table, get_message_handler()); + return linking(symbol_table, new_symbol_table, message_handler); } catch(const std::string &str) { - error() << "typecheck: " << str << eom; + messaget log(message_handler); + log.error() << "typecheck: " << str << messaget::eom; return true; } } @@ -55,7 +60,11 @@ bool json_symtab_languaget::typecheck( /// Output the result of the parsed json file to the output stream /// passed as a parameter to this function. /// \param out: The stream to use to output the parsed_json_file. -void json_symtab_languaget::show_parse(std::ostream &out) +/// \param message_handler: A message handler +void json_symtab_languaget::show_parse( + std::ostream &out, + message_handlert &message_handler) { + (void)message_handler; parsed_json_file.output(out); } diff --git a/src/json-symtab-language/json_symtab_language.h b/src/json-symtab-language/json_symtab_language.h index cea1ceefb89..221d0348640 100644 --- a/src/json-symtab-language/json_symtab_language.h +++ b/src/json-symtab-language/json_symtab_language.h @@ -25,16 +25,24 @@ Author: Chris Smowton, chris.smowton@diffblue.com class json_symtab_languaget : public languaget { public: - bool parse(std::istream &instream, const std::string &path) override; - - bool typecheck(symbol_table_baset &symbol_table, const std::string &module) - override; - - void show_parse(std::ostream &out) override; - - bool - to_expr(const std::string &, const std::string &, exprt &, const namespacet &) - override + bool parse( + std::istream &instream, + const std::string &path, + message_handlert &message_handler) override; + + bool typecheck( + symbol_table_baset &symbol_table, + const std::string &module, + message_handlert &message_handler) override; + + void show_parse(std::ostream &out, message_handlert &) override; + + bool to_expr( + const std::string &, + const std::string &, + exprt &, + const namespacet &, + message_handlert &) override { UNIMPLEMENTED; } @@ -58,7 +66,9 @@ class json_symtab_languaget : public languaget return util_make_unique(); } - bool generate_support_functions(symbol_table_baset &symbol_table) override + bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &) override { // check if entry point is already there bool entry_point_exists = diff --git a/src/langapi/language.cpp b/src/langapi/language.cpp index b9bb5ab38ea..985908d77cb 100644 --- a/src/langapi/language.cpp +++ b/src/langapi/language.cpp @@ -18,7 +18,7 @@ bool languaget::final(symbol_table_baset &) return false; } -bool languaget::interfaces(symbol_table_baset &) +bool languaget::interfaces(symbol_table_baset &, message_handlert &) { return false; } diff --git a/src/langapi/language.h b/src/langapi/language.h index 7433e7f0fb7..5b47d4c9475 100644 --- a/src/langapi/language.h +++ b/src/langapi/language.h @@ -12,16 +12,17 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_LANGAPI_LANGUAGE_H #define CPROVER_LANGAPI_LANGUAGE_H +#include +#include + #include #include // unique_ptr #include #include #include -#include -#include - class exprt; +class message_handlert; class namespacet; class optionst; class symbol_table_baset; @@ -32,11 +33,11 @@ class typet; #define HELP_FUNCTIONS " {y--function} {uname} \t set main function name\n" -class languaget:public messaget +class languaget { public: /// Set language-specific options - virtual void set_language_options(const optionst &) + virtual void set_language_options(const optionst &, message_handlert &) { } @@ -45,7 +46,8 @@ class languaget:public messaget virtual bool preprocess( std::istream &instream, const std::string &path, - std::ostream &outstream) + std::ostream &outstream, + message_handlert &) { // unused parameters (void)instream; @@ -56,7 +58,8 @@ class languaget:public messaget virtual bool parse( std::istream &instream, - const std::string &path)=0; + const std::string &path, + message_handlert &message_handler) = 0; /// Create language-specific support functions, such as __CPROVER_start, /// __CPROVER_initialize and language-specific library functions. @@ -66,7 +69,9 @@ class languaget:public messaget /// complete. Functions introduced here are visible to lazy loading and /// can influence its decisions (e.g. picking the types of input parameters /// and globals), whereas anything introduced during `final` cannot. - virtual bool generate_support_functions(symbol_table_baset &symbol_table) = 0; + virtual bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &message_handler) = 0; // add external dependencies of a given module to set @@ -95,13 +100,15 @@ class languaget:public messaget /// in `symbol_table`. This will only be called if `methods_provided` /// advertised the given `function_id` could be provided by this `languaget` /// instance. - virtual void - convert_lazy_method( - const irep_idt &function_id, symbol_table_baset &symbol_table) + virtual void convert_lazy_method( + const irep_idt &function_id, + symbol_table_baset &symbol_table, + message_handlert &message_handler) { // unused parameters (void)function_id; (void)symbol_table; + (void)message_handler; } /// Final adjustments, e.g. initializing stub functions and globals that @@ -110,12 +117,16 @@ class languaget:public messaget // type check interfaces of currently parsed file - virtual bool interfaces(symbol_table_baset &symbol_table); + virtual bool interfaces( + symbol_table_baset &symbol_table, + message_handlert &message_handler); // type check a module in the currently parsed file - virtual bool - typecheck(symbol_table_baset &symbol_table, const std::string &module) = 0; + virtual bool typecheck( + symbol_table_baset &symbol_table, + const std::string &module, + message_handlert &message_handler) = 0; /// \brief Is it possible to call three-argument typecheck() on this object? virtual bool can_keep_file_local() @@ -135,6 +146,7 @@ class languaget:public messaget virtual bool typecheck( symbol_table_baset &symbol_table, const std::string &module, + message_handlert &message_handler, const bool keep_file_local) { INVARIANT( @@ -151,7 +163,8 @@ class languaget:public messaget // show parse tree - virtual void show_parse(std::ostream &out)=0; + virtual void + show_parse(std::ostream &out, message_handlert &message_handler) = 0; // conversion of expressions @@ -190,12 +203,14 @@ class languaget:public messaget /// \param module: prefix to be used for identifiers /// \param expr: the parsed expression /// \param ns: a namespace + /// \param message_handler: a message handler /// \return false if the conversion succeeds virtual bool to_expr( const std::string &code, const std::string &module, exprt &expr, - const namespacet &ns)=0; + const namespacet &ns, + message_handlert &message_handler) = 0; virtual std::unique_ptr new_language()=0; diff --git a/src/langapi/language_file.cpp b/src/langapi/language_file.cpp index 8cad3c7d18b..b46be2f3d17 100644 --- a/src/langapi/language_file.cpp +++ b/src/langapi/language_file.cpp @@ -8,10 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "language_file.h" -#include +#include #include "language.h" +#include + language_filet::language_filet(const language_filet &rhs): modules(rhs.modules), language(rhs.language==nullptr?nullptr:rhs.language->new_language()), @@ -37,15 +39,18 @@ void language_filet::get_modules() void language_filet::convert_lazy_method( const irep_idt &id, - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { - language->convert_lazy_method(id, symbol_table); + language->convert_lazy_method(id, symbol_table, message_handler); } -void language_filest::show_parse(std::ostream &out) +void language_filest::show_parse( + std::ostream &out, + message_handlert &message_handler) { for(const auto &file : file_map) - file.second.language->show_parse(out); + file.second.language->show_parse(out, message_handler); } bool language_filest::parse(message_handlert &message_handler) @@ -68,7 +73,7 @@ bool language_filest::parse(message_handlert &message_handler) languaget &language=*(file.second.language); - if(language.parse(infile, file.first)) + if(language.parse(infile, file.first, message_handler)) { log.error() << "Parsing of " << file.first << " failed" << messaget::eom; return true; @@ -91,7 +96,7 @@ bool language_filest::typecheck( for(auto &file : file_map) { - if(file.second.language->interfaces(symbol_table)) + if(file.second.language->interfaces(symbol_table, message_handler)) return true; } @@ -134,12 +139,13 @@ bool language_filest::typecheck( { if(file.second.language->can_keep_file_local()) { - if(file.second.language->typecheck(symbol_table, "", keep_file_local)) + if(file.second.language->typecheck( + symbol_table, "", message_handler, keep_file_local)) return true; } else { - if(file.second.language->typecheck(symbol_table, "")) + if(file.second.language->typecheck(symbol_table, "", message_handler)) return true; } // register lazy methods. @@ -165,14 +171,16 @@ bool language_filest::typecheck( } bool language_filest::generate_support_functions( - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { std::set languages; for(auto &file : file_map) { if(languages.insert(file.second.language->id()).second) - if(file.second.language->generate_support_functions(symbol_table)) + if(file.second.language->generate_support_functions( + symbol_table, message_handler)) return true; } @@ -193,11 +201,13 @@ bool language_filest::final(symbol_table_baset &symbol_table) return false; } -bool language_filest::interfaces(symbol_table_baset &symbol_table) +bool language_filest::interfaces( + symbol_table_baset &symbol_table, + message_handlert &message_handler) { for(auto &file : file_map) { - if(file.second.language->interfaces(symbol_table)) + if(file.second.language->interfaces(symbol_table, message_handler)) return true; } @@ -273,12 +283,12 @@ bool language_filest::typecheck_module( if(module.file->language->can_keep_file_local()) { module.in_progress = !module.file->language->typecheck( - symbol_table, module.name, keep_file_local); + symbol_table, module.name, message_handler, keep_file_local); } else { - module.in_progress = - !module.file->language->typecheck(symbol_table, module.name); + module.in_progress = !module.file->language->typecheck( + symbol_table, module.name, message_handler); } if(!module.in_progress) diff --git a/src/langapi/language_file.h b/src/langapi/language_file.h index 70d1db6fa6e..be4722d4ad2 100644 --- a/src/langapi/language_file.h +++ b/src/langapi/language_file.h @@ -50,7 +50,8 @@ class language_filet final void convert_lazy_method( const irep_idt &id, - symbol_table_baset &symbol_table); + symbol_table_baset &symbol_table, + message_handlert &message_handler); explicit language_filet(const std::string &filename); language_filet(const language_filet &rhs); @@ -103,9 +104,11 @@ class language_filest bool parse(message_handlert &message_handler); - void show_parse(std::ostream &out); + void show_parse(std::ostream &out, message_handlert &message_handler); - bool generate_support_functions(symbol_table_baset &symbol_table); + bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &message_handler); bool @@ -121,7 +124,9 @@ class language_filest bool final(symbol_table_baset &symbol_table); - bool interfaces(symbol_table_baset &symbol_table); + bool interfaces( + symbol_table_baset &symbol_table, + message_handlert &message_handler); // The method must have been added to the symbol table and registered // in lazy_method_map (currently always in language_filest::typecheck) @@ -134,7 +139,7 @@ class language_filest PRECONDITION(symbol_table.has_symbol(id)); lazy_method_mapt::iterator it=lazy_method_map.find(id); if(it!=lazy_method_map.end()) - it->second->convert_lazy_method(id, symbol_table); + it->second->convert_lazy_method(id, symbol_table, message_handler); } bool can_convert_lazy_method(const irep_idt &id) const diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index 5e058af5176..324ed0f01da 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "language_util.h" #include +#include #include #include #include @@ -93,14 +94,13 @@ exprt to_expr( { std::unique_ptr p(get_language_from_identifier(ns, identifier)); - null_message_handlert null_message_handler; - p->set_message_handler(null_message_handler); - const symbolt &symbol=ns.lookup(identifier); exprt expr; - if(p->to_expr(src, id2string(symbol.module), expr, ns)) + null_message_handlert null_message_handler; + + if(p->to_expr(src, id2string(symbol.module), expr, ns, null_message_handler)) return nil_exprt(); return expr; diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp index f9d7fe9be6b..6b8390d076a 100644 --- a/src/statement-list/statement_list_language.cpp +++ b/src/statement-list/statement_list_language.cpp @@ -22,32 +22,35 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include #include -void statement_list_languaget::set_language_options(const optionst &options) +void statement_list_languaget::set_language_options( + const optionst &options, + message_handlert &) { params = object_factory_parameterst{options}; } bool statement_list_languaget::generate_support_functions( - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + message_handlert &message_handler) { - return statement_list_entry_point(symbol_table, get_message_handler()); + return statement_list_entry_point(symbol_table, message_handler); } bool statement_list_languaget::typecheck( symbol_table_baset &symbol_table, const std::string &module, + message_handlert &message_handler, const bool keep_file_local) { symbol_tablet new_symbol_table; if(statement_list_typecheck( - parse_tree, new_symbol_table, module, get_message_handler())) + parse_tree, new_symbol_table, module, message_handler)) return true; - remove_internal_symbols( - new_symbol_table, get_message_handler(), keep_file_local); + remove_internal_symbols(new_symbol_table, message_handler, keep_file_local); - if(linking(symbol_table, new_symbol_table, get_message_handler())) + if(linking(symbol_table, new_symbol_table, message_handler)) return true; return false; @@ -55,7 +58,8 @@ bool statement_list_languaget::typecheck( bool statement_list_languaget::parse( std::istream &instream, - const std::string &path) + const std::string &path, + message_handlert &message_handler) { statement_list_parser.clear(); parse_path = path; @@ -71,7 +75,7 @@ bool statement_list_languaget::parse( return result; } -void statement_list_languaget::show_parse(std::ostream &out) +void statement_list_languaget::show_parse(std::ostream &out, message_handlert &) { output_parse_tree(out, parse_tree); } @@ -83,9 +87,10 @@ bool statement_list_languaget::can_keep_file_local() bool statement_list_languaget::typecheck( symbol_table_baset &symbol_table, - const std::string &module) + const std::string &module, + message_handlert &message_handler) { - return typecheck(symbol_table, module, true); + return typecheck(symbol_table, module, message_handler, true); } bool statement_list_languaget::from_expr( @@ -118,7 +123,8 @@ bool statement_list_languaget::to_expr( const std::string &, const std::string &, exprt &, - const namespacet &) + const namespacet &, + message_handlert &) { return true; } diff --git a/src/statement-list/statement_list_language.h b/src/statement-list/statement_list_language.h index 312d6a2d741..352c973fa24 100644 --- a/src/statement-list/statement_list_language.h +++ b/src/statement-list/statement_list_language.h @@ -26,38 +26,51 @@ class statement_list_languaget : public languaget /// Sets language specific options. /// \param options: Options that shall apply during the parse and /// typecheck process. - void set_language_options(const optionst &options) override; + /// \param message_handler: Message handler. + void set_language_options( + const optionst &options, + message_handlert &message_handler) override; /// Parses input given by \p instream and saves this result to this /// instance's parse tree. /// \param instream: Input to parse. /// \param path: Path of the input. + /// \param message_handler: Message handler. /// \return False if successful. - bool parse(std::istream &instream, const std::string &path) override; + bool parse( + std::istream &instream, + const std::string &path, + message_handlert &message_handler) override; /// Currently unused. - bool generate_support_functions(symbol_table_baset &symbol_table) override; + bool generate_support_functions( + symbol_table_baset &symbol_table, + message_handlert &) override; /// Converts the current parse tree into a symbol table. /// \param [out] symbol_table: Object that shall be filled by this function. /// If the symbol table is not empty when calling this function, its /// contents are merged with the new entries. /// \param module: Name of the file that has been parsed. + /// \param message_handler: Message handler. /// \param keep_file_local: Set to true if local variables of this module /// should be included in the table. /// \return False if no errors occurred, true otherwise. bool typecheck( symbol_table_baset &symbol_table, const std::string &module, + message_handlert &message_handler, const bool keep_file_local) override; - bool typecheck(symbol_table_baset &symbol_table, const std::string &module) - override; + bool typecheck( + symbol_table_baset &symbol_table, + const std::string &module, + message_handlert &) override; bool can_keep_file_local() override; /// Prints the parse tree to the given output stream. - void show_parse(std::ostream &out) override; + void show_parse(std::ostream &out, message_handlert &) override; // Constructor and destructor. ~statement_list_languaget() override; @@ -92,12 +105,14 @@ class statement_list_languaget : public languaget /// \param module: prefix to be used for identifiers /// \param expr: the parsed expression /// \param ns: a namespace + /// \param message_handler: Message handler. /// \return false if the conversion succeeds bool to_expr( const std::string &code, const std::string &module, exprt &expr, - const namespacet &ns) override; + const namespacet &ns, + message_handlert &message_handler) override; std::unique_ptr new_language() override; diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp index 031c837db1a..c299b9acb13 100644 --- a/src/symtab2gb/symtab2gb_parse_options.cpp +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -69,7 +69,6 @@ static void run_symtab2gb( cmdline_verbosity, messaget::M_STATISTICS, message_handler); auto const symtab_language = new_json_symtab_language(); - symtab_language->set_message_handler(message_handler); symbol_tablet linked_symbol_table; @@ -77,7 +76,8 @@ static void run_symtab2gb( { auto const &symtab_filename = symtab_filenames[ix]; auto &symtab_file = symtab_files[ix]; - if(failed(symtab_language->parse(symtab_file, symtab_filename))) + if(failed( + symtab_language->parse(symtab_file, symtab_filename, message_handler))) { source_locationt source_location; source_location.set_file(symtab_filename); @@ -85,7 +85,7 @@ static void run_symtab2gb( "failed to parse symbol table", source_location}; } symbol_tablet symtab{}; - if(failed(symtab_language->typecheck(symtab, ""))) + if(failed(symtab_language->typecheck(symtab, "", message_handler))) { source_locationt source_location; source_location.set_file(symtab_filename); diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index ac76defc184..7e38f26f392 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -72,9 +72,7 @@ bool constant_simplification_mockt::ai_simplify( SCENARIO("ai_domain_baset::ai_simplify_lhs", "[core][analyses][ai][ai_simplify_lhs]") { - ui_message_handlert message_handler(null_message_handler); ansi_c_languaget language; - language.set_message_handler(message_handler); symbol_tablet symbol_table; namespacet ns(symbol_table); @@ -87,8 +85,8 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs", { // Construct an expression that the simplify_expr can simplify exprt simplifiable_expression; - bool compile_failed= - language.to_expr("1 + 1", "", simplifiable_expression, ns); + bool compile_failed = language.to_expr( + "1 + 1", "", simplifiable_expression, ns, null_message_handler); const unsigned int array_size=5; array_typet array_type( diff --git a/unit/testing-utils/get_goto_model_from_c.cpp b/unit/testing-utils/get_goto_model_from_c.cpp index e9437bacc80..e1f3c879cce 100644 --- a/unit/testing-utils/get_goto_model_from_c.cpp +++ b/unit/testing-utils/get_goto_model_from_c.cpp @@ -51,10 +51,9 @@ goto_modelt get_goto_model_from_c(std::istream &in) CHECK_RETURN(language_file.language); languaget &language = *language_file.language; - language.set_message_handler(null_message_handler); { - const bool error = language.parse(in, ""); + const bool error = language.parse(in, "", null_message_handler); if(error) throw invalid_input_exceptiont("parsing failed"); @@ -73,8 +72,8 @@ goto_modelt get_goto_model_from_c(std::istream &in) } { - const bool error = - language_files.generate_support_functions(goto_model.symbol_table); + const bool error = language_files.generate_support_functions( + goto_model.symbol_table, null_message_handler); if(error) throw invalid_input_exceptiont("support function generation failed");