From e53acb965230ccd03a9cc0097ce68b6325f5fd1d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 28 Aug 2019 15:34:06 +0100 Subject: [PATCH 1/4] Generate `INITIALIZE_FUNCTION` from `convert_single_method` This allows for an external lazy methods driver to control when the `INITIALIZE_FUNCTION` is generated. --- .../java_bytecode/java_bytecode_language.cpp | 22 ++++++++++++++++++- jbmc/src/java_bytecode/java_entry_point.cpp | 15 ++----------- jbmc/src/java_bytecode/java_entry_point.h | 10 +++++++++ 3 files changed, 33 insertions(+), 14 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 7062f452e12..a5d73af453c 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 @@ -1120,7 +1126,7 @@ void java_bytecode_languaget::convert_lazy_method( 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()) + if(symbol.value.is_not_nil() && function_id != INITIALIZE_FUNCTION) { java_bytecode_instrument_symbol( symbol_table, @@ -1201,6 +1207,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 From 398968983cceef88f018f5e3edaed0af8775c174 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 8 Oct 2019 12:56:40 +0100 Subject: [PATCH 2/4] Add unit tests of lazy `cprover_initialize` generation This tests that an empty bodied initialize function is generated by `typecheck` and that the body is then populated by `convert_lazy_method` --- .../java_bytecode_language/language.cpp | 48 +++++++++++++++++++ .../module_dependencies.txt | 2 + 2 files changed, 50 insertions(+) diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp index ada4c440109..4a49a811861 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,48 @@ 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); +} + +TEST_CASE( + "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; + language.typecheck(symbol_table, ""); + { + const symbolt *const initialise = symbol_table.lookup(INITIALIZE_FUNCTION); + REQUIRE(initialise); + REQUIRE(initialise->value.is_nil()); + } + language.convert_lazy_method(INITIALIZE_FUNCTION, symbol_table); + { + 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; + language.typecheck(symbol_table, ""); + 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 From cd75f9fa507f5b5b86f17b2aea7e9e5cdad0d059 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 9 Oct 2019 13:42:51 +0100 Subject: [PATCH 3/4] Update comment --- jbmc/src/java_bytecode/java_bytecode_language.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index a5d73af453c..54cf9e62015 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1125,7 +1125,8 @@ 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) + // 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( From 082b368ae6b2e8240cafd1586b986aaffb530a9f Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 9 Oct 2019 13:54:39 +0100 Subject: [PATCH 4/4] Restructure TEST_CASEs as SCENARIOs To describe what the tests are doing. --- .../java_bytecode_language/language.cpp | 50 +++++++++++++------ 1 file changed, 35 insertions(+), 15 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp index 4a49a811861..bb6d2c6894d 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp @@ -56,7 +56,7 @@ static void use_external_driver(java_bytecode_languaget &language) language.set_language_options(options); } -TEST_CASE( +SCENARIO( "LAZY_METHODS_MODE_EXTERNAL_DRIVER based generation of cprover_initialise", "[core][java_bytecode_language]") { @@ -65,17 +65,29 @@ TEST_CASE( language.set_message_handler(null_message_handler); use_external_driver(language); symbol_tablet symbol_table; - language.typecheck(symbol_table, ""); - { - const symbolt *const initialise = symbol_table.lookup(INITIALIZE_FUNCTION); - REQUIRE(initialise); - REQUIRE(initialise->value.is_nil()); - } - language.convert_lazy_method(INITIALIZE_FUNCTION, symbol_table); + GIVEN("java_bytecode_languaget::typecheck is run.") { - const symbolt *const initialise = symbol_table.lookup(INITIALIZE_FUNCTION); - REQUIRE(initialise); - REQUIRE(can_cast_expr(initialise->value)); + 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)); + } + } } } @@ -88,8 +100,16 @@ TEST_CASE( language.set_message_handler(null_message_handler); language.set_language_options(optionst{}); symbol_tablet symbol_table; - language.typecheck(symbol_table, ""); - const symbolt *const initialise = symbol_table.lookup(INITIALIZE_FUNCTION); - REQUIRE(initialise); - REQUIRE(can_cast_expr(initialise->value)); + 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)); + } + } }