From 06c40698769178af0c9a23fd853ed23dc0c3410b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 18 Sep 2019 14:41:31 +0100 Subject: [PATCH 1/4] Extract java_bytecode_language_optionst class Extract java_bytecode_language_optionst class from java_bytecode_language class, to make it more structured by separating the fields that are expected to remain constant during the execution once they are initialized. --- jbmc/src/java_bytecode/README.md | 6 +- .../java_bytecode/java_bytecode_language.cpp | 152 ++++++++++-------- .../java_bytecode/java_bytecode_language.h | 87 +++++----- 3 files changed, 132 insertions(+), 113 deletions(-) diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index 9bdbaa6e495..23d9e8161a4 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -666,12 +666,12 @@ and the methods in them. The methods, along with their parsed representation \ref java_bytecode_languaget::method_bytecode via a reference held in \ref java_bytecode_convert_classt::method_bytecode. typecheck then performs a switch over the value of -[lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode) to +[lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) to determine which loading strategy to use. \subsection eager-loading Eager loading -If [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode) is +If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is \ref java_bytecode_languaget::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 &) @@ -695,7 +695,7 @@ method parameters) and function references (at function call sites) to locate further classes and methods to load. The following paragraph describes the mechanism used. -If [lazy_methods_mode](\ref java_bytecode_languaget::lazy_methods_mode) is +If [lazy_methods_mode](\ref java_bytecode_language_optionst::lazy_methods_mode) is \ref lazy_methods_modet::LAZY_METHODS_MODE_CONTEXT_INSENSITIVE then context-insensitive lazy loading is used. Under this stragegy \ref java_bytecode_languaget::do_ci_lazy_method_conversion is called to do all diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 4062317b58a..cdd64caac5d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -132,11 +132,10 @@ void lazy_class_to_declared_symbols_mapt::reinitialize() map.clear(); } -/// Consume options that are java bytecode specific. -void java_bytecode_languaget::set_language_options(const optionst &options) +java_bytecode_language_optionst::java_bytecode_language_optionst( + const optionst &options, + messaget &log) { - object_factory_parameters.set(options); - assume_inputs_non_null = options.get_bool_option("java-assume-inputs-non-null"); string_refinement_enabled = options.get_bool_option("refine-strings"); @@ -182,9 +181,6 @@ void java_bytecode_languaget::set_language_options(const optionst &options) extra_entry_points.end(), std::back_inserter(extra_methods), build_load_method_by_regex); - const auto &new_points = build_extra_entry_points(options); - extra_methods.insert( - extra_methods.end(), new_points.begin(), new_points.end()); java_cp_include_files = options.get_option("java-cp-include-files"); if(!java_cp_include_files.empty()) @@ -195,7 +191,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options) jsont json_cp_config; if(parse_json( java_cp_include_files.substr(1), - get_message_handler(), + log.get_message_handler(), json_cp_config)) throw "cannot read JSON input configuration for JAR loading"; @@ -224,17 +220,18 @@ void java_bytecode_languaget::set_language_options(const optionst &options) { const std::string filename = options.get_option("static-values"); jsont tmp_json; - if(parse_json(filename, *message_handler, tmp_json)) + if(parse_json(filename, log.get_message_handler(), tmp_json)) { - warning() << "Provided JSON file for static-values cannot be parsed; it" - << " will be ignored." << messaget::eom; + log.warning() + << "Provided JSON file for static-values cannot be parsed; it" + << " will be ignored." << messaget::eom; } else { if(!tmp_json.is_object()) { - warning() << "Provided JSON file for static-values is not a JSON " - << "object; it will be ignored." << messaget::eom; + log.warning() << "Provided JSON file for static-values is not a JSON " + << "object; it will be ignored." << messaget::eom; } else static_values_json = std::move(to_json_object(tmp_json)); @@ -246,8 +243,18 @@ void java_bytecode_languaget::set_language_options(const optionst &options) if(options.is_set("context-include") || options.is_set("context-exclude")) method_context = get_context(options); +} - language_options_initialized=true; +/// Consume options that are java bytecode specific. +void java_bytecode_languaget::set_language_options(const optionst &options) +{ + object_factory_parameters.set(options); + language_options = java_bytecode_language_optionst{options, *this}; + const auto &new_points = build_extra_entry_points(options); + language_options->extra_methods.insert( + language_options->extra_methods.end(), + new_points.begin(), + new_points.end()); } std::set java_bytecode_languaget::extensions() const @@ -283,7 +290,7 @@ bool java_bytecode_languaget::parse( std::istream &, const std::string &path) { - PRECONDITION(language_options_initialized); + PRECONDITION(language_options.has_value()); java_class_loader.clear_classpath(); @@ -291,9 +298,10 @@ bool java_bytecode_languaget::parse( java_class_loader.add_classpath_entry(p); java_class_loader.set_message_handler(get_message_handler()); - java_class_loader.set_java_cp_include_files(java_cp_include_files); - java_class_loader.add_load_classes(java_load_classes); - if(string_refinement_enabled) + java_class_loader.set_java_cp_include_files( + language_options->java_cp_include_files); + java_class_loader.add_load_classes(language_options->java_load_classes); + if(language_options->string_refinement_enabled) { string_preprocess.initialize_known_type_table(); @@ -314,8 +322,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(), - java_cp_include_files); + get_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. @@ -331,8 +338,12 @@ bool java_bytecode_languaget::parse( std::string manifest_main_class = manifest["Main-Class"]; // if the manifest declares a Main-Class line, we got a main class - if(!manifest_main_class.empty() && !ignore_manifest_main_class) + if( + !manifest_main_class.empty() && + !language_options->ignore_manifest_main_class) + { main_class = manifest_main_class; + } } } else @@ -725,7 +736,7 @@ bool java_bytecode_languaget::typecheck( symbol_tablet &symbol_table, const std::string &) { - PRECONDITION(language_options_initialized); + PRECONDITION(language_options.has_value()); // There are various cases in the Java front-end where pre-existing symbols // from a previous load are not handled. We just rule this case out for now; // a user wishing to ensure a particular class is loaded should use @@ -738,7 +749,7 @@ bool java_bytecode_languaget::typecheck( java_internal_additions(symbol_table); - if(string_refinement_enabled) + if(language_options->string_refinement_enabled) string_preprocess.initialize_conversion_table(); // Must load java.lang.Object first to avoid stubbing @@ -748,15 +759,14 @@ bool java_bytecode_languaget::typecheck( java_class_loader.get_class_with_overlays_map().find("java.lang.Object"); if(it != java_class_loader.get_class_with_overlays_map().end()) { - if( - java_bytecode_convert_class( - it->second, - symbol_table, - get_message_handler(), - max_user_array_length, - method_bytecode, - string_preprocess, - no_load_classes)) + if(java_bytecode_convert_class( + it->second, + symbol_table, + get_message_handler(), + language_options->max_user_array_length, + method_bytecode, + string_preprocess, + language_options->no_load_classes)) { return true; } @@ -769,15 +779,14 @@ bool java_bytecode_languaget::typecheck( if(class_trees.second.front().parsed_class.name.empty()) continue; - if( - java_bytecode_convert_class( - class_trees.second, - symbol_table, - get_message_handler(), - max_user_array_length, - method_bytecode, - string_preprocess, - no_load_classes)) + if(java_bytecode_convert_class( + class_trees.second, + symbol_table, + get_message_handler(), + language_options->max_user_array_length, + method_bytecode, + string_preprocess, + language_options->no_load_classes)) { return true; } @@ -852,7 +861,7 @@ bool java_bytecode_languaget::typecheck( for(java_bytecode_parse_treet &parse_tree : class_to_trees.second) { generate_constant_global_variables( - parse_tree, symbol_table, string_refinement_enabled); + parse_tree, symbol_table, language_options->string_refinement_enabled); } } status() << "Java: added " @@ -888,14 +897,14 @@ bool java_bytecode_languaget::typecheck( create_static_initializer_symbols( symbol_table, synthetic_methods, - threading_support, - static_values_json.has_value()); + language_options->threading_support, + language_options->static_values_json.has_value()); lazy_class_to_declared_symbols_mapt class_to_declared_symbols; // Now incrementally elaborate methods // that are reachable from this entry point. - switch(lazy_methods_mode) + switch(language_options->lazy_methods_mode) { case LAZY_METHODS_MODE_CONTEXT_INSENSITIVE: // ci = context-insensitive @@ -940,15 +949,17 @@ bool java_bytecode_languaget::typecheck( // now instrument runtime exceptions java_bytecode_instrument( symbol_table, - throw_runtime_exceptions, + language_options->throw_runtime_exceptions, get_message_handler()); // now typecheck all bool res = java_bytecode_typecheck( - symbol_table, get_message_handler(), string_refinement_enabled); + symbol_table, + get_message_handler(), + language_options->string_refinement_enabled); // now instrument thread-blocks and synchronized methods. - if(threading_support) + if(language_options->threading_support) { convert_threadblock(symbol_table); convert_synchronized_methods(symbol_table, get_message_handler()); @@ -960,7 +971,7 @@ bool java_bytecode_languaget::typecheck( bool java_bytecode_languaget::generate_support_functions( symbol_tablet &symbol_table) { - PRECONDITION(language_options_initialized); + PRECONDITION(language_options.has_value()); symbol_table_buildert symbol_table_builder = symbol_table_buildert::wrap(symbol_table); @@ -990,16 +1001,16 @@ bool java_bytecode_languaget::generate_support_functions( symbol_table_builder, main_class, get_message_handler(), - assume_inputs_non_null, - assert_uncaught_exceptions, + language_options->assume_inputs_non_null, + language_options->assert_uncaught_exceptions, object_factory_parameters, get_pointer_type_selector(), - string_refinement_enabled, + language_options->string_refinement_enabled, [&](const symbolt &function, symbol_table_baset &symbol_table) { return java_build_arguments( function, symbol_table, - assume_inputs_non_null, + language_options->assume_inputs_non_null, object_factory_parameters, get_pointer_type_selector(), get_message_handler()); @@ -1040,9 +1051,9 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion( symbol_table, main_class, main_jar_classes, - extra_methods, + language_options->extra_methods, java_class_loader, - java_load_classes, + language_options->java_load_classes, get_pointer_type_selector(), get_message_handler(), synthetic_methods); @@ -1105,13 +1116,15 @@ void java_bytecode_languaget::convert_lazy_method( java_bytecode_instrument_symbol( symbol_table, symbol_table.get_writeable_ref(function_id), - throw_runtime_exceptions, + language_options->throw_runtime_exceptions, get_message_handler()); } // now typecheck this function java_bytecode_typecheck_updated_symbols( - symbol_table, get_message_handler(), string_refinement_enabled); + symbol_table, + get_message_handler(), + language_options->string_refinement_enabled); } /// Notify ci_lazy_methods, if present, of any static function calls made by @@ -1216,12 +1229,12 @@ bool java_bytecode_languaget::convert_single_method( switch(synthetic_method_it->second) { case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER: - if(threading_support) + if(language_options->threading_support) writable_symbol.value = get_thread_safe_clinit_wrapper_body( function_id, symbol_table, - nondet_static, - static_values_json.has_value(), + language_options->nondet_static, + language_options->static_values_json.has_value(), object_factory_parameters, get_pointer_type_selector(), get_message_handler()); @@ -1229,8 +1242,8 @@ bool java_bytecode_languaget::convert_single_method( writable_symbol.value = get_clinit_wrapper_body( function_id, symbol_table, - nondet_static, - static_values_json.has_value(), + language_options->nondet_static, + language_options->static_values_json.has_value(), object_factory_parameters, get_pointer_type_selector(), get_message_handler()); @@ -1242,13 +1255,14 @@ bool java_bytecode_languaget::convert_single_method( INVARIANT( class_name, "user_specified_clinit must be declared by a class."); INVARIANT( - static_values_json.has_value(), "static-values JSON must be available"); + language_options->static_values_json.has_value(), + "static-values JSON must be available"); writable_symbol.value = get_user_specified_clinit_body( *class_name, - *static_values_json, + *language_options->static_values_json, symbol_table, needed_lazy_methods, - max_user_array_length, + language_options->max_user_array_length, references, class_to_declared_symbols.get(symbol_table)); break; @@ -1301,13 +1315,13 @@ bool java_bytecode_languaget::convert_single_method( cmb->get().method, symbol_table, get_message_handler(), - max_user_array_length, - throw_assertion_error, + language_options->max_user_array_length, + language_options->throw_assertion_error, std::move(needed_lazy_methods), string_preprocess, class_hierarchy, - threading_support, - method_context); + language_options->threading_support, + language_options->method_context); INVARIANT(declaring_class(symbol), "Method must have a declaring class."); return false; } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 622785470d8..1899d90ce7c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -150,6 +150,50 @@ class lazy_class_to_declared_symbols_mapt std::unordered_multimap map; }; +struct java_bytecode_language_optionst +{ + java_bytecode_language_optionst(const optionst &options, messaget &log); + + java_bytecode_language_optionst() = default; + + /// assume inputs variables to be non-null + bool assume_inputs_non_null = false; + bool string_refinement_enabled = false; + bool throw_runtime_exceptions = false; + bool assert_uncaught_exceptions = false; + bool throw_assertion_error = false; + bool threading_support = false; + bool nondet_static = false; + bool ignore_manifest_main_class = false; + + /// max size for user code created arrays + size_t max_user_array_length = 0; + lazy_methods_modet lazy_methods_mode = + lazy_methods_modet::LAZY_METHODS_MODE_EAGER; + + /// list of classes to force load even without reference from the entry point + std::vector java_load_classes; + std::string java_cp_include_files; + /// JSON which contains initial values of static fields (right + /// after the static initializer of the class was run). This is read from the + /// file specified by the --static-values command-line option. + optionalt static_values_json; + + /// List of classes to never load + std::unordered_set no_load_classes; + + std::vector extra_methods; + + /// If set, method bodies are only elaborated if they pass the filter. + /// Methods that do not pass the filter are "excluded": their symbols will + /// include all the meta-information that is available from the bytecode + /// (parameter types, return type, accessibility etc.) but the value of the + /// symbol (corresponding to the body of the method) will be replaced with the + /// same kind of "return nondet null or instance of return type" body that we + /// use for stubbed methods. The original method body will never be loaded. + optionalt method_context; +}; + #define JAVA_CLASS_MODEL_SUFFIX "@class_model" class java_bytecode_languaget:public languaget @@ -180,17 +224,7 @@ class java_bytecode_languaget:public languaget virtual ~java_bytecode_languaget(); java_bytecode_languaget( std::unique_ptr pointer_type_selector) - : language_options_initialized(false), - threading_support(false), - assume_inputs_non_null(false), - object_factory_parameters(), - max_user_array_length(0), - lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER), - string_refinement_enabled(false), - throw_runtime_exceptions(false), - assert_uncaught_exceptions(false), - throw_assertion_error(false), - nondet_static(false), + : object_factory_parameters(), pointer_type_selector(std::move(pointer_type_selector)) { } @@ -252,31 +286,14 @@ class java_bytecode_languaget:public languaget bool do_ci_lazy_method_conversion(symbol_tablet &); const select_pointer_typet &get_pointer_type_selector() const; - bool language_options_initialized; + optionalt language_options; irep_idt main_class; std::vector main_jar_classes; - bool ignore_manifest_main_class; java_class_loadert java_class_loader; - bool threading_support; - bool assume_inputs_non_null; // assume inputs variables to be non-null java_object_factory_parameterst object_factory_parameters; - size_t max_user_array_length; // max size for user code created arrays method_bytecodet method_bytecode; - lazy_methods_modet lazy_methods_mode; - bool string_refinement_enabled; - bool throw_runtime_exceptions; - bool assert_uncaught_exceptions; - bool throw_assertion_error; java_string_library_preprocesst string_preprocess; - std::string java_cp_include_files; - bool nondet_static; - /// JSON which contains initial values of static fields (right - /// after the static initializer of the class was run). This is read from the - /// file specified by the --static-values command-line option. - optionalt static_values_json; - // list of classes to force load even without reference from the entry point - std::vector java_load_classes; private: virtual std::vector @@ -289,10 +306,6 @@ class java_bytecode_languaget:public languaget synthetic_methods_mapt synthetic_methods; stub_global_initializer_factoryt stub_global_initializer_factory; class_hierarchyt class_hierarchy; - // List of classes to never load - std::unordered_set no_load_classes; - - std::vector extra_methods; /// Map used in all calls to functions that deterministically create objects /// (currently only \ref assign_from_json). @@ -300,14 +313,6 @@ class java_bytecode_languaget:public languaget /// IDs of such objects to symbols that store their values. std::unordered_map references; - /// If set, method bodies are only elaborated if they pass the filter. - /// Methods that do not pass the filter are "excluded": their symbols will - /// include all the meta-information that is available from the bytecode - /// (parameter types, return type, accessibility etc.) but the value of the - /// symbol (corresponding to the body of the method) will be replaced with the - /// same kind of "return nondet null or instance of return type" body that we - /// use for stubbed methods. The original method body will never be loaded. - optionalt method_context; }; std::unique_ptr new_java_bytecode_language(); From 2ed5dfd4c273b413193e5768461875f064592113 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 11 Sep 2019 11:41:20 +0100 Subject: [PATCH 2/4] Add an assert-no-exceptions-thrown option This is to specify that we want to replace all throw instructions by assert false. This is useful mainly for performance reasons as it simplifies conditions for symex, while retaining the non-exceptional behaviour of the program. --- .../java_bytecode_convert_method.cpp | 13 ++++++++----- .../java_bytecode/java_bytecode_convert_method.h | 3 ++- .../java_bytecode_convert_method_class.h | 5 ++++- .../src/java_bytecode/java_bytecode_language.cpp | 9 +++++++-- jbmc/src/java_bytecode/java_bytecode_language.h | 8 ++++++++ .../convert_method.cpp | 16 ++++++++++++---- 6 files changed, 41 insertions(+), 13 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 0e4327b048e..92214d1d7eb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2349,9 +2349,10 @@ void java_bytecode_convert_methodt::convert_athrow( exprt::operandst &results) const { if( - !throw_assertion_error && - uncaught_exceptions_domaint::get_exception_type(op[0].type()) == - "java::java.lang.AssertionError") + assert_no_exceptions_thrown || + ((uncaught_exceptions_domaint::get_exception_type(op[0].type()) == + "java::java.lang.AssertionError") && + !throw_assertion_error)) { // we translate athrow into // ASSERT false; @@ -3190,7 +3191,8 @@ void java_bytecode_convert_method( java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, - const optionalt &method_context) + const optionalt &method_context, + bool assert_no_exceptions_thrown) { java_bytecode_convert_methodt java_bytecode_convert_method( @@ -3201,7 +3203,8 @@ void java_bytecode_convert_method( needed_lazy_methods, string_preprocess, class_hierarchy, - threading_support); + threading_support, + assert_no_exceptions_thrown); java_bytecode_convert_method(class_symbol, method, method_context); } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/jbmc/src/java_bytecode/java_bytecode_convert_method.h index 9e7da326674..ed44b414165 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -39,7 +39,8 @@ void java_bytecode_convert_method( java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, - const optionalt &method_context); + const optionalt &method_context, + bool assert_no_exceptions_thrown); void create_method_stub_symbol( const irep_idt &identifier, diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index d7f31044704..e0cf6190728 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -40,12 +40,14 @@ class java_bytecode_convert_methodt:public messaget optionalt needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, - bool threading_support) + bool threading_support, + bool assert_no_exceptions_thrown) : messaget(_message_handler), symbol_table(symbol_table), ns(symbol_table), max_array_length(_max_array_length), throw_assertion_error(throw_assertion_error), + assert_no_exceptions_thrown(assert_no_exceptions_thrown), threading_support(threading_support), needed_lazy_methods(std::move(needed_lazy_methods)), string_preprocess(_string_preprocess), @@ -76,6 +78,7 @@ class java_bytecode_convert_methodt:public messaget namespacet ns; const size_t max_array_length; const bool throw_assertion_error; + const bool assert_no_exceptions_thrown; const bool threading_support; optionalt needed_lazy_methods; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index cdd64caac5d..596e2479afd 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -59,6 +59,8 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options) "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check")); options.set_option( "throw-assertion-error", cmd.isset("throw-assertion-error")); + options.set_option( + "assert-no-exceptions-thrown", cmd.isset("assert-no-exceptions-thrown")); options.set_option("java-threading", cmd.isset("java-threading")); if(cmd.isset("java-max-vla-length")) @@ -144,6 +146,8 @@ java_bytecode_language_optionst::java_bytecode_language_optionst( assert_uncaught_exceptions = options.get_bool_option("uncaught-exception-check"); throw_assertion_error = options.get_bool_option("throw-assertion-error"); + assert_no_exceptions_thrown = + options.get_bool_option("assert-no-exceptions-thrown"); threading_support = options.get_bool_option("java-threading"); max_user_array_length = options.get_unsigned_int_option("java-max-vla-length"); @@ -1321,7 +1325,8 @@ bool java_bytecode_languaget::convert_single_method( string_preprocess, class_hierarchy, language_options->threading_support, - language_options->method_context); + language_options->method_context, + language_options->assert_no_exceptions_thrown); INVARIANT(declaring_class(symbol), "Method must have a declaring class."); return false; } @@ -1355,7 +1360,7 @@ bool java_bytecode_languaget::convert_single_method( bool java_bytecode_languaget::final(symbol_table_baset &) { - PRECONDITION(language_options_initialized); + PRECONDITION(language_options.has_value()); return false; } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 1899d90ce7c..4bfd2544f7f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -33,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ "(disable-uncaught-exception-check)" \ "(throw-assertion-error)" \ + "(assert-no-exceptions-thrown)" \ "(java-assume-inputs-non-null)" \ "(java-assume-inputs-interval):" \ "(java-assume-inputs-integral)" \ @@ -57,6 +58,9 @@ Author: Daniel Kroening, kroening@kroening.com " assert statements instead of failing\n" \ " at the location of the assert statement\n" \ " --throw-runtime-exceptions make implicit runtime exceptions explicit\n" \ + " --assert-no-exceptions-thrown\n"\ + " transform `throw` instructions into `assert FALSE`\n"/* NOLINT(*) */ \ + " followed by `assume FALSE`.\n" \ " --max-nondet-array-length N limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \ " --max-nondet-tree-depth N limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \ " at level N references are set to null\n" /* NOLINT(*) */ \ @@ -166,6 +170,10 @@ struct java_bytecode_language_optionst bool nondet_static = false; bool ignore_manifest_main_class = false; + /// Transform `athrow` bytecode instructions into `assert FALSE` followed + /// by `assume FALSE`. + bool assert_no_exceptions_thrown = false; + /// max size for user code created arrays size_t max_user_array_length = 0; lazy_methods_modet lazy_methods_mode = diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index 213dfdcd927..8d04dde17e7 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -457,6 +457,7 @@ SCENARIO( symbol_tablet symbol_table; java_string_library_preprocesst string_preprocess; const class_hierarchyt class_hierarchy{}; + const bool assert_no_exceptions_thrown = false; java_bytecode_convert_methodt converter{symbol_table, null_message_handler, 10, @@ -464,7 +465,8 @@ SCENARIO( {}, string_preprocess, class_hierarchy, - false}; + false, + assert_no_exceptions_thrown}; GIVEN("An int array") { @@ -571,6 +573,7 @@ SCENARIO( const std::size_t max_array_length = 10; const bool throw_assertion_error = true; const bool threading_support = false; + const bool assert_no_exceptions_thrown = false; java_bytecode_convert_methodt converter{symbol_table, null_message_handler, max_array_length, @@ -578,7 +581,8 @@ SCENARIO( {}, string_preprocess, class_hierarchy, - threading_support}; + threading_support, + assert_no_exceptions_thrown}; GIVEN("An int_array variable") { @@ -677,6 +681,7 @@ SCENARIO( const std::size_t max_array_length = 10; const bool throw_assertion_error = true; const bool threading_support = false; + const bool assert_no_exceptions_thrown = false; java_bytecode_convert_methodt converter{symbol_table, null_message_handler, max_array_length, @@ -684,7 +689,8 @@ SCENARIO( {}, string_preprocess, class_hierarchy, - threading_support}; + threading_support, + assert_no_exceptions_thrown}; GIVEN("An int_array variable") { @@ -818,6 +824,7 @@ SCENARIO( const std::size_t max_array_length = 10; const bool throw_assertion_error = true; const bool threading_support = false; + const bool assert_no_exceptions_thrown = false; java_bytecode_convert_methodt converter{symbol_table, null_message_handler, max_array_length, @@ -825,7 +832,8 @@ SCENARIO( {}, string_preprocess, class_hierarchy, - threading_support}; + threading_support, + assert_no_exceptions_thrown}; GIVEN("An int_array variable") { From 7cdd2e2777ff0e1fb122dc3498c3d91cca8abfdd Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 18 Sep 2019 16:19:37 +0100 Subject: [PATCH 3/4] Add regression test for --assert-no-exceptions-thrown This tests the option behaves as desired. --- .../MyException.class | Bin 0 -> 192 bytes .../assert-no-exceptions-thrown/Test.class | Bin 0 -> 964 bytes .../assert-no-exceptions-thrown/Test.java | 33 ++++++++++++++++++ .../test-with-throw.desc | 14 ++++++++ .../assert-no-exceptions-thrown/test.desc | 18 ++++++++++ 5 files changed, 65 insertions(+) create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class new file mode 100644 index 0000000000000000000000000000000000000000..5578fa11a8f315cee834ac189ccca4cbadae3b8c GIT binary patch literal 192 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSN!0lVH^YiK$a|!28pn0ZD(NI2$p6Cl5Ai>kQ4`y I$Hc%105{kpi2wiq literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..9b30d4d418e8e5e87211093334a7f249582c8833 GIT binary patch literal 964 zcmZWnOHUJF6g^)%4?3NeQWS@lw}?QM8q>H!QbbHlco-lgvYSr7$UteybgJ-ISh4Gd z4VsA2ME3p?e}gf`^9_$GZ0_qjbI-Z=&W}G|zXK?tXd#VJ6Jr))%HOx3DL-z(z^DZq z4-zyJCLUU_)XSuWDNLIv2=tD-&87@Ozfo_#^qX#_CaVHsOTd`*>wY*V5TBgd6wnqL zRVmQDh=&3J)#U~=~T*u!&u2Si0em=k<#;%9b@#B+!x+5 zuOFl5BN9hSnML;Gd0x9!YUA0`|DZO;Z&k84DyN8(r+^u%P`(`T7O+M|7gNn~x!^21 z_hoTo4)qVx7BI}O`cb6n=Zwq9W1jP_GF~HM9Yb(25>4x%>o*+n3)vSY@@bj@Wd_sS r(9re4O3@8~o~->DsUw(L8(RDm66$ytVy=#-R;VLpm(_`fqvw&ob0Vyk literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java new file mode 100644 index 00000000000..ed234bf44a2 --- /dev/null +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java @@ -0,0 +1,33 @@ +class MyException extends Exception {} + +public class Test { + public static int mayThrow(char branch) throws Throwable { + if (branch == 'n') { + throw new NullPointerException(); + } else if (branch == 'c') { + throw new MyException(); + } else if (branch == 't') { + throw new Throwable(); + } else if (branch == 'r') { + return 2; + } else { + return 1; + } + } + + public static void check(char branch) { + try { + int i = mayThrow(branch); + if (i == 2) + assert false; + if (i == 1) + assert false; + } catch (MyException e) { + assert false; + } catch (NullPointerException e) { + assert false; + } catch (Throwable e) { + assert false; + } + } +} diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc new file mode 100644 index 00000000000..d3f015b3f8b --- /dev/null +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc @@ -0,0 +1,14 @@ +CORE +Test.class +--function Test.check +line 22 assertion at file Test.java line 22 .*: FAILURE +line 24 assertion at file Test.java line 24 .*: FAILURE +line 26 assertion at file Test.java line 26 .*: FAILURE +line 28 assertion at file Test.java line 28 .*: FAILURE +line 30 assertion at file Test.java line 30 .*: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that we get the expected behaviour when --assert-no-exceptions-thrown is +not used. This is to make sure that test.desc is actually testing what we wanted. diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc new file mode 100644 index 00000000000..9b6f000e11b --- /dev/null +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc @@ -0,0 +1,18 @@ +CORE +Test.class +--function Test.check --assert-no-exceptions-thrown +line 6 assertion at file Test.java line 6 .*: FAILURE +line 8 assertion at file Test.java line 8 .*: FAILURE +line 10 assertion at file Test.java line 10 .*: FAILURE +line 22 assertion at file Test.java line 22 .*: FAILURE +line 24 assertion at file Test.java line 24 .*: FAILURE +line 26 assertion at file Test.java line 26 .*: SUCCESS +line 28 assertion at file Test.java line 28 .*: SUCCESS +line 30 assertion at file Test.java line 30 .*: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that the `throw` instructions have been replaced by assertions, which +are failing here because they are reachable, and assumptions which prevent +the last three assertions from failing. From b433f5c688e0c5ce647448dd72f1d5e534db3c08 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 25 Sep 2019 13:01:55 +0100 Subject: [PATCH 4/4] Test assert-no-exceptions-thrown and runtime exception Test that when both are combined, --throw-runtime-exception still works. --- .../assert-no-exceptions-thrown/Thrower.class | Bin 0 -> 1455 bytes .../assert-no-exceptions-thrown/Thrower.java | 54 ++++++++++++++++++ .../test-thrower.desc | 14 +++++ 3 files changed, 68 insertions(+) create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java create mode 100644 jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class new file mode 100644 index 0000000000000000000000000000000000000000..ed6f21fd4e383252f3fe82263b317877a38a25a5 GIT binary patch literal 1455 zcmZux&vV;E7=0VdURhRaM^4%#)Pa`J+OC_FCWVruC64P-Q^n5UPMKtegJN%81xF70 z5lZ6x?On@&upW#&A+_ZMAnXct@W@?TvI>KF$i6@%A)%tkF+79`2Y>qO6y4dRW z>ub$k;I_mqTUOKWK5%=V3U^u-({Tnl2IyEug$`1wR2hbky++b*GGqoo(|2vB!w@gm z8p~B3Ror42DpR&nFE=T~>Z`Q<9&R(78KhOZ)QpPd`PGLlu`PSTFg1YdqGS2?jwrjX z^;y$?BqFrQ2rcM#S9>N@c147xg{RdmZw_6cBAH}JD&1s8=jlgf*U+x7?+xw5I zV*;<}sNsEvu}IR9j8)g|xeUDDNRB%?Osu@rpT@?fXpv|WgZvKy$G5klS5oN;_pEL} zs*nY0)Vq953d(onX5+rpyjJ)h)frNL&y*@sFDZK@A7veCvp@zDp9EIdV;GHE=kRC? z1#)0|aJo<#dSP35wkz7@qsx-F{D4Z(0oQSstUgX(4acW(ib_JC+SH>auedk z1F$EOh*xP&gqsXWyhbHLD*K&MIT2FEkXihhC5roqeMwvqW>E=>XK7reQKiwKv1Tad zQ^eO|2S}`xegv=YVb)O1#P`~~GOno8-y(U(&`dSf4Ob~M^VbiE&&LhjWb=vf#6C`Z zxQE@9(oZ<~7!zM3yNi*FhO&>5U8J63bnO7Ao)emmps8bMCW7k6(BTNG9Yc)>s=kaq zp-XdY!^6pbO!s4^ABX$Vz);xOM`71v)Jlbr1WKSk7Pa{rG+ajtOH`?XG;SkDM9cHc7Q@`VV?I2OsD0IWFJ}6z~{Dd_@%xa0$Os)!%R#f8YxK#4OWD zmUARX4*Cm}I9|`DlgZRF$J7f<(wxiX{w7ex8=)nnHReJO0K>-VeT?mbD|=94-ykb( Va(J5~o5;#>4CzbKOy@)R!oS46JbnNG literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java new file mode 100644 index 00000000000..7da5ab69dc9 --- /dev/null +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java @@ -0,0 +1,54 @@ +public class Thrower { + public static void test(Integer t) { + String ret = ""; + if (t != null) + try { + switch (t) { + case 1: + ret = "CCE"; + Object o = new Integer(0); + String x = ((String) o); + break; + + case 2: + ret = "AIOBE"; + int[] xs = new int[3]; + t = xs[5]; + + case 3: + ret = "AE"; + t = 5 / 0; + + case 4: + ret = "NASE"; + Integer[] arr = new Integer[-7]; + + case 5: + ret = "NPE"; + String str = null; + str.toLowerCase(); + + default: + break; + } + } catch (ClassCastException | NegativeArraySizeException + | NullPointerException | ArithmeticException + | ArrayIndexOutOfBoundsException e3) { + + if (e3 instanceof ClassCastException) + assert ret.equals("CCE"); + + if (e3 instanceof NegativeArraySizeException) + assert ret.equals("NASE"); + + if (e3 instanceof NullPointerException) + assert ret.equals("NPE"); + + if (e3 instanceof ArithmeticException) + assert ret.equals("AE"); + + if (e3 instanceof ArrayIndexOutOfBoundsException) + assert ret.equals("AIOBE"); + } + } +} diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc new file mode 100644 index 00000000000..728d667be1f --- /dev/null +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc @@ -0,0 +1,14 @@ +CORE +Thrower.class +--function Thrower.test --assert-no-exceptions-thrown --throw-runtime-exceptions +line 39 assertion at file Thrower.java line 39 .*: FAILURE +line 42 assertion at file Thrower.java line 42 .*: FAILURE +line 45 assertion at file Thrower.java line 45 .*: FAILURE +line 48 assertion at file Thrower.java line 48 .*: FAILURE +line 51 assertion at file Thrower.java line 51 .*: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that the runtime exceptions still throw with `--throw-runtime-exceptions` +even when `--assert-no-exceptions-thrown` is specified.