diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 1469856cb66..502d89e23e9 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -54,6 +54,15 @@ class lazy_goto_functions_mapt final goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)> post_process_functiont; + typedef std::function + can_generate_function_bodyt; + typedef std::function< + bool( + const irep_idt &function_name, + symbol_table_baset &symbol_table, + goto_functiont &function, + bool body_available)> + generate_function_bodyt; private: typedef std::map underlying_mapt; @@ -66,6 +75,8 @@ class lazy_goto_functions_mapt final language_filest &language_files; symbol_tablet &symbol_table; const post_process_functiont post_process_function; + const can_generate_function_bodyt driver_program_can_generate_function_body; + const generate_function_bodyt driver_program_generate_function_body; message_handlert &message_handler; public: @@ -75,11 +86,17 @@ class lazy_goto_functions_mapt final language_filest &language_files, symbol_tablet &symbol_table, post_process_functiont post_process_function, + can_generate_function_bodyt driver_program_can_generate_function_body, + generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler) : goto_functions(goto_functions), language_files(language_files), symbol_table(symbol_table), - post_process_function(std::move(post_process_function)), + post_process_function(post_process_function), + driver_program_can_generate_function_body( + driver_program_can_generate_function_body), + driver_program_generate_function_body( + driver_program_generate_function_body), message_handler(message_handler) { } @@ -107,7 +124,9 @@ class lazy_goto_functions_mapt final /// it a bodyless stub. bool can_produce_function(const key_type &name) const { - return language_files.can_convert_lazy_method(name); + return + language_files.can_convert_lazy_method(name) || + driver_program_can_generate_function_body(name); } void unload(const key_type &name) const { goto_functions.erase(name); } @@ -153,14 +172,30 @@ class lazy_goto_functions_mapt final underlying_mapt::iterator it=goto_functions.find(name); if(it!=goto_functions.end()) return *it; - // Fill in symbol table entry body if not already done - // If this returns false then it's a stub - language_files.convert_lazy_method(name, function_symbol_table); - // Create goto_functiont - goto_functionst::goto_functiont function; - goto_convert_functionst convert_functions( - function_symbol_table, message_handler); - convert_functions.convert_function(name, function); + + goto_functiont function; + + // First chance: see if the driver program wants to provide a replacement: + bool body_provided = + driver_program_generate_function_body( + name, + function_symbol_table, + function, + language_files.can_convert_lazy_method(name)); + + // Second chance: see if language_filest can provide a body: + if(!body_provided) + { + // Fill in symbol table entry body if not already done + language_files.convert_lazy_method(name, function_symbol_table); + body_provided = function_symbol_table.lookup_ref(name).value.is_not_nil(); + + // Create goto_functiont + goto_convert_functionst convert_functions( + function_symbol_table, message_handler); + convert_functions.convert_function(name, function); + } + // Add to map return *goto_functions.emplace(name, std::move(function)).first; } diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index da019025f5a..90fcaaacf87 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -22,6 +22,8 @@ lazy_goto_modelt::lazy_goto_modelt( post_process_functiont post_process_function, post_process_functionst post_process_functions, + can_generate_function_bodyt driver_program_can_generate_function_body, + generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler) : goto_model(new goto_modelt()), symbol_table(goto_model->symbol_table), @@ -41,9 +43,15 @@ lazy_goto_modelt::lazy_goto_modelt( function); this->post_process_function(model_function, *this); }, + driver_program_can_generate_function_body, + driver_program_generate_function_body, message_handler), - post_process_function(std::move(post_process_function)), - post_process_functions(std::move(post_process_functions)), + post_process_function(post_process_function), + post_process_functions(post_process_functions), + driver_program_can_generate_function_body( + driver_program_can_generate_function_body), + driver_program_generate_function_body( + driver_program_generate_function_body), message_handler(message_handler) { language_files.set_message_handler(message_handler); @@ -68,10 +76,12 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other) function); this->post_process_function(model_function, *this); }, + other.driver_program_can_generate_function_body, + other.driver_program_generate_function_body, other.message_handler), language_files(std::move(other.language_files)), - post_process_function(std::move(other.post_process_function)), - post_process_functions(std::move(other.post_process_functions)), + post_process_function(other.post_process_function), + post_process_functions(other.post_process_functions), message_handler(other.message_handler) { } diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 417115024ce..ed2037dee6d 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -24,10 +24,16 @@ class lazy_goto_modelt : public abstract_goto_modelt void(goto_model_functiont &function, const abstract_goto_modelt &)> post_process_functiont; typedef std::function post_process_functionst; + typedef lazy_goto_functions_mapt::can_generate_function_bodyt + can_generate_function_bodyt; + typedef lazy_goto_functions_mapt::generate_function_bodyt + generate_function_bodyt; explicit lazy_goto_modelt( post_process_functiont post_process_function, post_process_functionst post_process_functions, + can_generate_function_bodyt driver_program_can_generate_function_body, + generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler); lazy_goto_modelt(lazy_goto_modelt &&other); @@ -60,6 +66,19 @@ class lazy_goto_modelt : public abstract_goto_modelt [&handler, &options](goto_modelt &goto_model) -> bool { return handler.process_goto_functions(goto_model, options); }, + [&handler](const irep_idt &name) -> bool { + return handler.can_generate_function_body(name); + }, + [&handler] + (const irep_idt &function_name, + symbol_table_baset &symbol_table, + goto_functiont &function, + bool is_first_chance) + { + return + handler.generate_function_body( + function_name, symbol_table, function, is_first_chance); + }, message_handler); } @@ -127,6 +146,8 @@ class lazy_goto_modelt : public abstract_goto_modelt // Function/module processing functions const post_process_functiont post_process_function; const post_process_functionst post_process_functions; + const can_generate_function_bodyt driver_program_can_generate_function_body; + const generate_function_bodyt driver_program_generate_function_body; /// Logging helper field message_handlert &message_handler; diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 1dc0f78daca..d0071f96912 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -37,6 +37,7 @@ SRC = bytecode_info.cpp \ remove_java_new.cpp \ replace_java_nondet.cpp \ select_pointer_type.cpp \ + simple_method_stubbing.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/java_bytecode/simple_method_stubbing.cpp b/src/java_bytecode/simple_method_stubbing.cpp new file mode 100644 index 00000000000..8bd484ed7e5 --- /dev/null +++ b/src/java_bytecode/simple_method_stubbing.cpp @@ -0,0 +1,280 @@ +/*******************************************************************\ + +Module: Simple Java method stubbing + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Java simple opaque stub generation + +#include "simple_method_stubbing.h" + +#include +#include + +#include +#include +#include +#include +#include + +class java_simple_method_stubst +{ +public: + java_simple_method_stubst( + symbol_table_baset &_symbol_table, + bool _assume_non_null, + const object_factory_parameterst &_object_factory_parameters, + message_handlert &_message_handler) + : symbol_table(_symbol_table), + assume_non_null(_assume_non_null), + object_factory_parameters(_object_factory_parameters), + message_handler(_message_handler) + { + } + + void create_method_stub_at( + const typet &expected_type, + const exprt &ptr, + const source_locationt &loc, + code_blockt &parent_block, + unsigned insert_before_index, + bool is_constructor, + bool update_in_place); + + void create_method_stub(symbolt &symbol); + + void check_method_stub(const irep_idt &); + +protected: + symbol_table_baset &symbol_table; + bool assume_non_null; + const object_factory_parameterst &object_factory_parameters; + message_handlert &message_handler; +}; + +/// Nondet-initialize an object, including allocating referees for reference +/// fields and nondet-initialising those recursively. Reference fields are +/// nondeterministically assigned either a fresh object or null; arrays are +/// additionally nondeterministically assigned between 0 and +/// `max_nondet_array_length` members. +/// \param expected_type: the expected actual type of `ptr`. We will cast +/// `ptr` to this type and initialize assuming the actual referee has this +/// type. +/// \param ptr: pointer to the memory to initialize +/// \param loc: source location to set for the opaque method stub +/// \param [out] parent_block: The parent block in which the new instructions +/// will be added. +/// \param insert_before_index: The position in which the new instructions +/// will be added. +/// \param is_constructor: true if we're initialising the `this` pointer of a +/// constructor. In this case the target's class identifier has been set and +/// should not be overridden. +/// \param update_in_place: Whether to generate the nondet in place or not. +void java_simple_method_stubst::create_method_stub_at( + const typet &expected_type, + const exprt &ptr, + const source_locationt &loc, + code_blockt &parent_block, + const unsigned insert_before_index, + const bool is_constructor, + const bool update_in_place) +{ + // At this point we know 'ptr' points to an opaque-typed object. + // We should nondet-initialize it and insert the instructions *after* + // the offending call at (*parent_block)[insert_before_index]. + + INVARIANT_WITH_IREP( + expected_type.id() == ID_pointer, + "Nondet initializer result type: expected a pointer", + expected_type); + + namespacet ns(symbol_table); + + const auto &expected_base = ns.follow(expected_type.subtype()); + if(expected_base.id() != ID_struct) + return; + + const exprt cast_ptr = + make_clean_pointer_cast(ptr, to_pointer_type(expected_type), ns); + + exprt to_init = cast_ptr; + // If it's a constructor the thing we're constructing has already + // been allocated by this point. + if(is_constructor) + to_init = dereference_exprt(to_init, expected_base); + + // Generate new instructions. + code_blockt new_instructions; + gen_nondet_init( + to_init, + new_instructions, + symbol_table, + loc, + is_constructor, + allocation_typet::DYNAMIC, + !assume_non_null, + object_factory_parameters, + update_in_place ? update_in_placet::MUST_UPDATE_IN_PLACE + : update_in_placet::NO_UPDATE_IN_PLACE); + + // Insert new_instructions into parent block. + if(!new_instructions.operands().empty()) + { + auto insert_position = parent_block.operands().begin(); + std::advance(insert_position, insert_before_index); + parent_block.operands().insert( + insert_position, + new_instructions.operands().begin(), + new_instructions.operands().end()); + } +} + +/// Replaces sym's value with an opaque method stub. If sym is a +/// constructor function this nondet-initializes `*this` using the function +/// above; otherwise it generates a return value using a similar method. +/// \param symbol: Function symbol to stub +void java_simple_method_stubst::create_method_stub(symbolt &symbol) +{ + code_blockt new_instructions; + const code_typet &required_type = to_code_type(symbol.type); + + // synthetic source location that contains the opaque function name only + source_locationt synthesized_source_location; + synthesized_source_location.set_function(symbol.name); + + // Initialize the return value or `this` parameter under construction. + // Note symbol.type is required_type, but with write access + // Probably required_type should not be const + const bool is_constructor = required_type.get_is_constructor(); + if(is_constructor) + { + const auto &this_argument = required_type.parameters()[0]; + const typet &this_type = this_argument.type(); + symbolt &init_symbol = get_fresh_aux_symbol( + this_type, + "to_construct", + "to_construct", + synthesized_source_location, + ID_java, + symbol_table); + const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr(); + code_assignt get_argument( + init_symbol_expression, symbol_exprt(this_argument.get_identifier())); + get_argument.add_source_location() = synthesized_source_location; + new_instructions.copy_to_operands(get_argument); + create_method_stub_at( + this_type, + init_symbol_expression, + synthesized_source_location, + new_instructions, + 1, + true, + false); + } + else + { + const typet &required_return_type = required_type.return_type(); + if(required_return_type != empty_typet()) + { + symbolt &to_return_symbol = get_fresh_aux_symbol( + required_return_type, + "to_return", + "to_return", + synthesized_source_location, + ID_java, + symbol_table); + const exprt &to_return = to_return_symbol.symbol_expr(); + if(to_return_symbol.type.id() != ID_pointer) + { + gen_nondet_init( + to_return, + new_instructions, + symbol_table, + source_locationt(), + false, + allocation_typet::LOCAL, // Irrelevant as type is primitive + !assume_non_null, + object_factory_parameters, + update_in_placet::NO_UPDATE_IN_PLACE); + } + else + create_method_stub_at( + required_return_type, + to_return, + synthesized_source_location, + new_instructions, + 0, + false, + false); + new_instructions.copy_to_operands(code_returnt(to_return)); + } + } + + symbol.value = new_instructions; +} + +/// Replaces `sym` with a function stub per the function above if it is +/// of suitable type. +/// \param symname: Symbol name to consider stubbing +void java_simple_method_stubst::check_method_stub(const irep_idt &symname) +{ + const symbolt &sym = *symbol_table.lookup(symname); + if( + !sym.is_type && sym.value.id() == ID_nil && sym.type.id() == ID_code && + // Don't stub internal locking primitives: + sym.name != "java::monitorenter" && sym.name != "java::monitorexit") + { + create_method_stub(*symbol_table.get_writeable(symname)); + } +} + +void java_generate_simple_method_stub( + const irep_idt &function_name, + symbol_table_baset &symbol_table, + bool assume_non_null, + const object_factory_parameterst &object_factory_parameters, + message_handlert &message_handler) +{ + java_simple_method_stubst stub_generator( + symbol_table, assume_non_null, object_factory_parameters, message_handler); + + stub_generator.check_method_stub(function_name); +} + +/// Generates function stubs for most undefined functions in the symbol +/// table, except as forbidden in +/// `java_simple_method_stubst::check_method_stub`. +/// \param symbol_table: Global symbol table +/// \param assume_non_null: If true, generated function stubs will never +/// initialize reference members with null. +/// \param object_factory_parameters: specifies exactly how nondet composite +/// objects should be created-- for example, object graph depth. +/// \param message_handler: Logging +void java_generate_simple_method_stubs( + symbol_table_baset &symbol_table, + bool assume_non_null, + const object_factory_parameterst &object_factory_parameters, + message_handlert &message_handler) +{ + // The intent here is to apply stub_generator.check_method_stub() to + // all the identifiers in the symbol table. However this method may alter the + // symbol table and iterating over a container which is being modified has + // undefined behaviour. Therefore in order for this to work reliably, we must + // take a copy of the identifiers in the symbol table and iterate over that, + // instead of iterating over the symbol table itself. + std::vector identifiers; + identifiers.reserve(symbol_table.symbols.size()); + for(const auto &symbol : symbol_table) + identifiers.push_back(symbol.first); + + java_simple_method_stubst stub_generator( + symbol_table, assume_non_null, object_factory_parameters, message_handler); + + for(const auto &identifier : identifiers) + { + stub_generator.check_method_stub(identifier); + } +} diff --git a/src/java_bytecode/simple_method_stubbing.h b/src/java_bytecode/simple_method_stubbing.h new file mode 100644 index 00000000000..d12ede725ae --- /dev/null +++ b/src/java_bytecode/simple_method_stubbing.h @@ -0,0 +1,34 @@ +/*******************************************************************\ + +Module: Simple Java method stubbing + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Java simple opaque stub generation + +#ifndef CPROVER_JAVA_BYTECODE_SIMPLE_METHOD_STUBBING_H +#define CPROVER_JAVA_BYTECODE_SIMPLE_METHOD_STUBBING_H + +#include + +class message_handlert; +struct object_factory_parameterst; +class symbol_table_baset; + +void java_generate_simple_method_stub( + const irep_idt &function_name, + symbol_table_baset &symbol_table, + bool assume_non_null, + const object_factory_parameterst &object_factory_parameters, + message_handlert &message_handler); + +void java_generate_simple_method_stubs( + symbol_table_baset &symbol_table, + bool assume_non_null, + const object_factory_parameterst &object_factory_parameters, + message_handlert &message_handler); + +#endif diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 72c7c1eacdd..fd461467060 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -48,6 +48,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include @@ -58,6 +60,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -522,6 +525,21 @@ int jbmc_parse_optionst::doit() }; } + object_factory_params.max_nondet_array_length = + cmdline.isset("java-max-input-array-length") + ? std::stoul(cmdline.get_value("java-max-input-array-length")) + : MAX_NONDET_ARRAY_LENGTH_DEFAULT; + object_factory_params.max_nondet_string_length = + cmdline.isset("string-max-input-length") + ? std::stoul(cmdline.get_value("string-max-input-length")) + : MAX_NONDET_STRING_LENGTH; + object_factory_params.max_nondet_tree_depth = + cmdline.isset("java-max-input-tree-depth") + ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) + : MAX_NONDET_TREE_DEPTH; + + stub_objects_are_not_null = cmdline.isset("java-assume-inputs-non-null"); + if(!cmdline.isset("symex-driven-lazy-loading")) { std::unique_ptr goto_model_ptr; @@ -757,23 +775,11 @@ void jbmc_parse_optionst::process_goto_function( replace_java_nondet(function); // Similar removal of java nondet statements: - // TODO Should really get this from java_bytecode_language somehow, but we - // don't have an instance of that here. - object_factory_parameterst factory_params; - factory_params.max_nondet_array_length= - cmdline.isset("java-max-input-array-length") - ? std::stoul(cmdline.get_value("java-max-input-array-length")) - : MAX_NONDET_ARRAY_LENGTH_DEFAULT; - factory_params.max_nondet_string_length= - cmdline.isset("string-max-input-length") - ? std::stoul(cmdline.get_value("string-max-input-length")) - : MAX_NONDET_STRING_LENGTH; - factory_params.max_nondet_tree_depth= - cmdline.isset("java-max-input-tree-depth") - ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) - : MAX_NONDET_TREE_DEPTH; - - convert_nondet(function, get_message_handler(), factory_params, ID_java); + convert_nondet( + function, + get_message_handler(), + object_factory_params, + ID_java); // add generic checks goto_check(ns, options, ID_java, function.get_goto_function()); @@ -1012,6 +1018,48 @@ bool jbmc_parse_optionst::process_goto_functions( return false; } +bool jbmc_parse_optionst::can_generate_function_body(const irep_idt &name) +{ + static const irep_idt initialize_id = INITIALIZE_FUNCTION; + + return name != goto_functionst::entry_point() && name != initialize_id; +} + +bool jbmc_parse_optionst::generate_function_body( + const irep_idt &function_name, + symbol_table_baset &symbol_table, + goto_functiont &function, + bool body_available) +{ + // Provide a simple stub implementation for any function we don't have a + // bytecode implementation for: + + if(body_available) + return false; + + if(!can_generate_function_body(function_name)) + return false; + + if(symbol_table.lookup_ref(function_name).mode == ID_java) + { + java_generate_simple_method_stub( + function_name, + symbol_table, + stub_objects_are_not_null, + object_factory_params, + get_message_handler()); + + goto_convert_functionst converter(symbol_table, get_message_handler()); + converter.convert_function(function_name, function); + + return true; + } + else + { + return false; + } +} + /// display command line help void jbmc_parse_optionst::help() { diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index d0c1919d93c..f176a96bce5 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -102,10 +102,20 @@ class jbmc_parse_optionst: const optionst &); bool process_goto_functions(goto_modelt &goto_model, const optionst &options); + bool can_generate_function_body(const irep_idt &name); + + bool generate_function_body( + const irep_idt &function_name, + symbol_table_baset &symbol_table, + goto_functiont &function, + bool body_available); + protected: ui_message_handlert ui_message_handler; std::unique_ptr cover_config; path_strategy_choosert path_strategy_chooser; + object_factory_parameterst object_factory_params; + bool stub_objects_are_not_null; void eval_verbosity(); void get_command_line_options(optionst &); diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index 217a3bb25d7..7beda3ec61e 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -97,6 +97,8 @@ symbol_tablet load_java_class( lazy_goto_modelt lazy_goto_model( [] (goto_model_functiont &function, const abstract_goto_modelt &model) { }, // NOLINT (*) [] (goto_modelt &goto_model) { return false; }, // NOLINT (*) + [] (const irep_idt &name) { return false; }, + [] (const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) { return false; }, // NOLINT (*) message_handler); // Configure the path loading