From 82948a4b1c7b57d4e3b00acb417e2bce03afe768 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Feb 2019 04:23:04 +0000 Subject: [PATCH 1/5] 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"); From 9e3fd5d26f0488b950dfae59a6a4135e006e28e0 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 18 Jul 2023 15:26:20 +0100 Subject: [PATCH 2/5] Define coverage blocks so as to be terminated by assumptions If a coverage block has an assumption in the middle then then an assertion at the end of the block could be reported as covered but actually be unreachable due to the preceding the assumption. Therefore coverage blocks should be terminated by assumptions in order to ensure than coverage reporting is accurate. --- regression/cbmc-cover/location12/test.desc | 5 ++-- regression/cbmc-cover/location15/test.desc | 3 +- regression/cbmc-cover/location16/test.desc | 5 ++-- regression/cbmc-cover/location2/test.desc | 4 +-- regression/cbmc-cover/simple_assert/test.desc | 2 +- .../test-no-failed-assertions.desc | 7 +++-- src/goto-instrument/cover_basic_blocks.cpp | 30 ++++++++++++++----- 7 files changed, 37 insertions(+), 19 deletions(-) diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc index bac822b042c..6cc5084011f 100644 --- a/regression/cbmc-cover/location12/test.desc +++ b/regression/cbmc-cover/location12/test.desc @@ -7,7 +7,8 @@ main.c ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: SATISFIED$ ^\[foo.coverage.2\] file main.c line 4 function foo block 2.*: FAILED$ -^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: SATISFIED$ -^\*\* 4 of 5 covered \(80.0%\) +^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: FAILED$ +^\[foo.coverage.4\] file main.c line 5 function foo block 4.*: SATISFIED$ +^\*\* 4 of 6 covered \(66.7%\) -- ^warning: ignoring diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc index b48161384c3..90cf7a9f26d 100644 --- a/regression/cbmc-cover/location15/test.desc +++ b/regression/cbmc-cover/location15/test.desc @@ -6,7 +6,8 @@ main.c ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$ ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$ ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$ -^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 14 function main block 4.*: FAILED$ +^\[main.coverage.5\] file main.c line 16 function main block 5.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$ ^\*\* 3 of \d+ covered -- diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc index 74d7080448c..40e65248f26 100644 --- a/regression/cbmc-cover/location16/test.desc +++ b/regression/cbmc-cover/location16/test.desc @@ -9,7 +9,8 @@ main.c ^\[func.coverage.2\] file main.c line 6 function func block 2.*: FAILED$ ^\[func.coverage.3\] file main.c line 8 function func block 3.*: FAILED$ ^\[func.coverage.4\] file main.c line 12 function func block 4.*: FAILED$ -^\[func.coverage.5\] file main.c line 15 function func block 5.*: SATISFIED$ -^\*\* 4 of 7 covered \(57.1%\) +^\[func.coverage.5\] file main.c line 14 function func block 5.*: FAILED$ +^\[func.coverage.6\] file main.c line 15 function func block 6.*: SATISFIED$ +^\*\* 4 of 8 covered \(50.0%\) -- ^warning: ignoring diff --git a/regression/cbmc-cover/location2/test.desc b/regression/cbmc-cover/location2/test.desc index 747ff0c5800..817de5431b9 100644 --- a/regression/cbmc-cover/location2/test.desc +++ b/regression/cbmc-cover/location2/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main.coverage.1\] file main.c line 9 function main block 1 \(lines main.c:main:9,10\): SATISFIED$ -^\[main.coverage.2\] file main.c line 11 function main block 2 \(lines main.c:main:11\): SATISFIED$ -^\*\* 2 of 2 covered \(100.0%\) +^\[main.coverage.3\] file main.c line 11 function main block 3 \(lines main.c:main:11\): SATISFIED$ +^\*\* 3 of 3 covered \(100.0%\) -- ^warning: ignoring main.c::5 diff --git a/regression/cbmc-cover/simple_assert/test.desc b/regression/cbmc-cover/simple_assert/test.desc index d3fac6c4c46..dfdc0dee6f9 100644 --- a/regression/cbmc-cover/simple_assert/test.desc +++ b/regression/cbmc-cover/simple_assert/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$ -(1 of 1|3 of 3) covered \(100\.0%\)$ +(1 of 1|2 of 2|3 of 3) covered \(100\.0%\)$ -- ^warning: ignoring ^CONVERSION ERROR$ diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index 0544dcdb715..7754c1e36e6 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,9 +1,10 @@ CORE paths-lifo-expected-failure test.c --cover location --pointer-check --malloc-may-fail --malloc-fail-null -\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED -\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED -\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED +\[main\.coverage\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:17,18\): SATISFIED +\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:15\): FAILED +\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:12,14\): SATISFIED +\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12\): SATISFIED \[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 81ff18b6b11..c290a1c3ce9 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -29,15 +29,34 @@ optionalt cover_basic_blockst::continuation_of_block( return {}; } +static bool +same_source_line(const source_locationt &a, const source_locationt &b) +{ + return a.get_file() == b.get_file() && a.get_line() == b.get_line(); +} + cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) { bool next_is_target = true; + const goto_programt::instructiont *preceding_assume = nullptr; std::size_t current_block = 0; forall_goto_program_instructions(it, goto_program) { + // For the purposes of coverage blocks, multiple consecutive assume + // instructions with the same source location are considered to be part of + // the same block. Assumptions should terminate a block, as subsequent + // instructions may be unreachable. However check instrumentation passes + // may insert multiple assertions in the same program location. Therefore + // these are combined for reasons of readability of the coverage output. + bool end_of_assume_group = + preceding_assume && + !(it->is_assume() && + same_source_line( + preceding_assume->source_location(), it->source_location())); + // Is it a potential beginning of a block? - if(next_is_target || it->is_target()) + if(next_is_target || it->is_target() || end_of_assume_group) { if(auto block_number = continuation_of_block(it, block_map)) { @@ -72,13 +91,8 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) block_info.source_location = it->source_location(); } - next_is_target = -#if 0 - // Disabled for being too messy - it->is_goto() || it->is_function_call() || it->is_assume(); -#else - it->is_goto() || it->is_function_call(); -#endif + next_is_target = it->is_goto() || it->is_function_call(); + preceding_assume = it->is_assume() ? &*it : nullptr; } } From ac26185fb43f7508945f2efa2597342d694df12c Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Sep 2023 13:50:56 +0100 Subject: [PATCH 3/5] Add tests of the affect of assumptions on coverage blocks --- regression/cbmc-cover/location-assume/end.c | 9 +++++++++ regression/cbmc-cover/location-assume/end.desc | 14 ++++++++++++++ regression/cbmc-cover/location-assume/middle.c | 11 +++++++++++ regression/cbmc-cover/location-assume/middle.desc | 15 +++++++++++++++ 4 files changed, 49 insertions(+) create mode 100644 regression/cbmc-cover/location-assume/end.c create mode 100644 regression/cbmc-cover/location-assume/end.desc create mode 100644 regression/cbmc-cover/location-assume/middle.c create mode 100644 regression/cbmc-cover/location-assume/middle.desc diff --git a/regression/cbmc-cover/location-assume/end.c b/regression/cbmc-cover/location-assume/end.c new file mode 100644 index 00000000000..0429196a1a1 --- /dev/null +++ b/regression/cbmc-cover/location-assume/end.c @@ -0,0 +1,9 @@ +#include + +void main() +{ + int i; + int *p = &i; + int j; + __CPROVER_assume(j == 1 / (*p)); +} diff --git a/regression/cbmc-cover/location-assume/end.desc b/regression/cbmc-cover/location-assume/end.desc new file mode 100644 index 00000000000..4d1bffdc81c --- /dev/null +++ b/regression/cbmc-cover/location-assume/end.desc @@ -0,0 +1,14 @@ +CORE +end.c +--pointer-check --div-by-zero-check --cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file end.c line 5 function main block 1 \(lines end\.c:main:5-8\): SATISFIED$ +^\[main.coverage.2\] file end.c line 9 function main block 2 \(lines end\.c:main:9\): SATISFIED$ +^\*\* 2 of 2 covered \(100.0%\) +-- +^warning: ignoring +-- +Test that in the case where multiple assertions are added on the same line of +code due to the addition of instrumentation checks, these do not result in +further splitting blocks. diff --git a/regression/cbmc-cover/location-assume/middle.c b/regression/cbmc-cover/location-assume/middle.c new file mode 100644 index 00000000000..64da9f6a25d --- /dev/null +++ b/regression/cbmc-cover/location-assume/middle.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + int i; + int j; + j = i; + __CPROVER_assume(0); + j = i + 2; + return 0; +} diff --git a/regression/cbmc-cover/location-assume/middle.desc b/regression/cbmc-cover/location-assume/middle.desc new file mode 100644 index 00000000000..650c62b33b1 --- /dev/null +++ b/regression/cbmc-cover/location-assume/middle.desc @@ -0,0 +1,15 @@ +CORE +middle.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file middle.c line 5 function main block 1 \(lines middle\.c:main:5-8\): SATISFIED$ +^\[main.coverage.2\] file middle.c line 9 function main block 2 \(lines middle\.c:main:9-11\): FAILED$ +^\*\* 1 of 2 covered \(50.0%\) +-- +^warning: ignoring +-- +This test confirms that assumptions in the middle of what would otherwise be a +single blocks without control flow will cause the code to be split into 2 +coverage blocks. This is required as an unsatisfiable assumption can result in +the following statements being unreachable. From 2b8a8fcb76f7b338cf3caa2a8085be483dabadf2 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 1 Dec 2023 13:23:11 +0000 Subject: [PATCH 4/5] Variables leaving scope on jumping should always be marked dead Even if new variables would be introduced to the scope, the existing variables which go out of scope still need to be marked as dead and/or have their destructors called. The placeholder for construction is moved to after the destruction, as destructions should be done first. --- .../cbmc/destructors/enter_lexical_block.desc | 12 +++- src/goto-programs/goto_convert.cpp | 60 +++++++++---------- 2 files changed, 38 insertions(+), 34 deletions(-) diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc index 296188dd84f..dd4f1e34852 100644 --- a/regression/cbmc/destructors/enter_lexical_block.desc +++ b/regression/cbmc/destructors/enter_lexical_block.desc @@ -2,7 +2,7 @@ CORE main.c --unwind 10 --show-goto-functions activate-multi-line-match -(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3 +(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc7[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc6[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc4[\s]*(?P>comment_block)[\s]*.*GOTO 3 ^EXIT=0$ ^SIGNAL=0$ -- @@ -22,8 +22,14 @@ Checks for: // 42 file main.c line 38 function main ASSIGN main::1::2::2::newAlloc7 := { 7 } // 43 file main.c line 39 function main + DEAD main::1::2::2::newAlloc7 + // 44 file main.c line 39 function main + DEAD main::1::2::2::newAlloc6 + // 45 file main.c line 39 function main + DEAD main::1::2::2::newAlloc4 + // 46 file main.c line 39 function main GOTO 3 This asserts that when the GOTO is going into a lexical block that destructors -are omitted. This used to be a limitation with the previous implementation and should -now be fixable, but for consistency it acts in the same way. +are not omitted. This used to be a limitation with the previous implementation +and has now been fixed. diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 172f1b3f0dc..f1cdce715ed 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -151,42 +151,40 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) targets.destructor_stack.get_nearest_common_ancestor_info( goto_target, label_target); - bool not_prefix = - intersection_result.right_depth_below_common_ancestor != 0; - // If our goto had no variables of note, just skip if(goto_target != 0) { // If the goto recorded a destructor stack, execute as much as is // appropriate for however many automatic variables leave scope. - // We don't currently handle variables *entering* scope, which - // is illegal for C++ non-pod types and impossible in Java in any case. - if(not_prefix) - { - debug().source_location = i.source_location(); - debug() << "encountered goto '" << goto_label - << "' that enters one or more lexical blocks; " - << "omitting constructors and destructors" << eom; - } - else - { - debug().source_location = i.source_location(); - debug() << "adding goto-destructor code on jump to '" << goto_label - << "'" << eom; - - node_indext end_destruct = intersection_result.common_ancestor; - goto_programt destructor_code; - unwind_destructor_stack( - i.source_location(), - destructor_code, - mode, - end_destruct, - goto_target); - dest.destructive_insert(g_it.first, destructor_code); - - // This should leave iterators intact, as long as - // goto_programt::instructionst is std::list. - } + debug().source_location = i.source_location(); + debug() << "adding goto-destructor code on jump to '" << goto_label + << "'" << eom; + + node_indext end_destruct = intersection_result.common_ancestor; + goto_programt destructor_code; + unwind_destructor_stack( + i.source_location(), + destructor_code, + mode, + end_destruct, + goto_target); + dest.destructive_insert(g_it.first, destructor_code); + + // This should leave iterators intact, as long as + // goto_programt::instructionst is std::list. + } + + // We don't currently handle variables *entering* scope, which + // is illegal for C++ non-pod types and impossible in Java in any case. + // This is however valid C. + const bool variables_added_to_scope = + intersection_result.right_depth_below_common_ancestor > 0; + if(variables_added_to_scope) + { + debug().source_location = i.source_location(); + debug() << "encountered goto '" << goto_label + << "' that enters one or more lexical blocks; " + << "omitting constructors." << eom; } } else From 89d5387439a41226631ab2925a050a0b9d0ff250 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Dec 2023 13:51:38 +0000 Subject: [PATCH 5/5] Dynamic frames: don't instrument __CPROVER_allocated_memory Doing so (rightly) yields an invariant failure in goto_check_ct. --- .../contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp index 24bce179189..a16f169dfe7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp @@ -23,6 +23,7 @@ init_function_symbols(std::unordered_set &function_symbols) if(function_symbols.empty()) { function_symbols.insert(CPROVER_PREFIX "_start"); + function_symbols.insert(CPROVER_PREFIX "allocated_memory"); function_symbols.insert(CPROVER_PREFIX "array_copy"); function_symbols.insert(CPROVER_PREFIX "array_replace"); function_symbols.insert(CPROVER_PREFIX "array_set");