diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 7062f452e12..54cf9e62015 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + #include #include #include @@ -757,6 +759,7 @@ bool java_bytecode_languaget::typecheck( "the Java front-end should only be used with an empty symbol table"); java_internal_additions(symbol_table); + create_java_initialize(symbol_table); if(language_options->string_refinement_enabled) string_preprocess.initialize_conversion_table(); @@ -942,6 +945,8 @@ bool java_bytecode_languaget::typecheck( convert_single_method( method_sig.first, journalling_symbol_table, class_to_declared_symbols); } + convert_single_method( + INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols); // Now convert all newly added string methods for(const auto &fn_name : journalling_symbol_table.get_inserted()) { @@ -1095,6 +1100,7 @@ void java_bytecode_languaget::methods_provided( // Add all synthetic methods to map for(const auto &kv : synthetic_methods) methods.insert(kv.first); + methods.insert(INITIALIZE_FUNCTION); } /// \brief Promote a lazy-converted method (one whose type is known but whose @@ -1119,8 +1125,9 @@ void java_bytecode_languaget::convert_lazy_method( lazy_class_to_declared_symbols_mapt class_to_declared_symbols; convert_single_method(function_id, symbol_table, class_to_declared_symbols); - // Instrument runtime exceptions (unless symbol is a stub) - if(symbol.value.is_not_nil()) + // Instrument runtime exceptions (unless symbol is a stub or is the + // INITIALISE_FUNCTION). + if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION) { java_bytecode_instrument_symbol( symbol_table, @@ -1201,6 +1208,20 @@ bool java_bytecode_languaget::convert_single_method( // Nothing to do if body is already loaded if(symbol.value.is_not_nil()) return false; + + if(function_id == INITIALIZE_FUNCTION) + { + java_static_lifetime_init( + symbol_table, + symbol.location, + language_options->assume_inputs_non_null, + object_factory_parameters, + *pointer_type_selector, + language_options->string_refinement_enabled, + get_message_handler()); + return false; + } + INVARIANT(declaring_class(symbol), "Method must have a declaring class."); bool ret = convert_single_method_code( diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index dccebd9eaae..1b183ac3044 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -53,7 +53,6 @@ void create_java_initialize(symbol_table_baset &symbol_table) initialize.mode=ID_java; initialize.type = java_method_typet({}, java_void_type()); - symbol_table.add(initialize); } @@ -104,7 +103,7 @@ static constant_exprt constant_bool(bool val) return from_integer(val ? 1 : 0, java_boolean_type()); } -static void java_static_lifetime_init( +void java_static_lifetime_init( symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, @@ -115,6 +114,7 @@ static void java_static_lifetime_init( { symbolt &initialize_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION); + PRECONDITION(initialize_symbol.value.is_nil()); code_blockt code_block; const symbol_exprt rounding_mode = @@ -590,17 +590,6 @@ bool java_entry_point( assert(symbol.type.id()==ID_code); - create_java_initialize(symbol_table); - - java_static_lifetime_init( - symbol_table, - symbol.location, - assume_init_pointers_not_null, - object_factory_parameters, - pointer_type_selector, - string_refinement_enabled, - message_handler); - return generate_java_start_function( symbol, symbol_table, diff --git a/jbmc/src/java_bytecode/java_entry_point.h b/jbmc/src/java_bytecode/java_entry_point.h index 531557375a7..bd7da4f5736 100644 --- a/jbmc/src/java_bytecode/java_entry_point.h +++ b/jbmc/src/java_bytecode/java_entry_point.h @@ -190,4 +190,14 @@ std::pair> java_build_arguments( /// code for it yet. void create_java_initialize(symbol_table_baset &symbol_table); +/// Adds the body to __CPROVER_initialize +void java_static_lifetime_init( + symbol_table_baset &symbol_table, + const source_locationt &source_location, + bool assume_init_pointers_not_null, + java_object_factory_parameterst object_factory_parameters, + const select_pointer_typet &pointer_type_selector, + bool string_refinement_enabled, + message_handlert &message_handler); + #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp index ada4c440109..bb6d2c6894d 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp @@ -12,6 +12,9 @@ Author: Diffblue Limited. #include #include +#include +#include +#include SCENARIO( "java_bytecode_language_opaque_field", @@ -45,3 +48,68 @@ 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); + symbol_tablet symbol_table; + GIVEN("java_bytecode_languaget::typecheck is run.") + { + language.typecheck(symbol_table, ""); + THEN("The " INITIALIZE_FUNCTION " is in the symbol table without code.") + { + const symbolt *const initialise = + symbol_table.lookup(INITIALIZE_FUNCTION); + REQUIRE(initialise); + REQUIRE(initialise->value.is_nil()); + } + GIVEN( + "java_bytecode_languaget::convert_lazy_method is used to " + "generate " INITIALIZE_FUNCTION) + { + language.convert_lazy_method(INITIALIZE_FUNCTION, symbol_table); + THEN("The " INITIALIZE_FUNCTION " is in the symbol table with code.") + { + const symbolt *const initialise = + symbol_table.lookup(INITIALIZE_FUNCTION); + REQUIRE(initialise); + REQUIRE(can_cast_expr(initialise->value)); + } + } + } +} + +TEST_CASE( + "Standard 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); + language.set_language_options(optionst{}); + symbol_tablet symbol_table; + GIVEN("java_bytecode_languaget::typecheck is run.") + { + language.typecheck(symbol_table, ""); + THEN("The " INITIALIZE_FUNCTION + " function is in the symbol table with code.") + { + const symbolt *const initialise = + symbol_table.lookup(INITIALIZE_FUNCTION); + REQUIRE(initialise); + REQUIRE(can_cast_expr(initialise->value)); + } + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt index 0b24c99c483..2275c6ca788 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_bytecode_language/module_dependencies.txt @@ -1,3 +1,5 @@ +java_bytecode java-testing-utils +linking testing-utils util