diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.class new file mode 100644 index 00000000000..d35c14928a9 Binary files /dev/null and b/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.class differ diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java new file mode 100644 index 00000000000..5382afb1aaf --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java @@ -0,0 +1,7 @@ +public class Bar { + public int x; + + public void cproverNondetInitialize() { + + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.class new file mode 100644 index 00000000000..85193230e37 Binary files /dev/null and b/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.class differ diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.java new file mode 100644 index 00000000000..5c7d8398174 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.java @@ -0,0 +1,5 @@ +public class Baz { + public void cproverNondetInitialize() { + + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.class new file mode 100644 index 00000000000..20f98193c01 Binary files /dev/null and b/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.class differ diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java new file mode 100644 index 00000000000..d5765648a32 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java @@ -0,0 +1,11 @@ +public class Foo { + public Bar subType; + + public Baz[] arraySubtype; + + public Gen genSubtype; + + public void cproverNondetInitialize() { + + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.class new file mode 100644 index 00000000000..baaed0ba8e2 Binary files /dev/null and b/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.class differ diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java new file mode 100644 index 00000000000..afcffe05ae6 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java @@ -0,0 +1,3 @@ +public class Gen { + T t; +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.class new file mode 100644 index 00000000000..70deaa0b6b7 Binary files /dev/null and b/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.class differ diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.java new file mode 100644 index 00000000000..1e9d6a5720a --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.java @@ -0,0 +1,7 @@ +public class GenFiller { + public int i; + + public void cproverNondetInitialize() { + + } + diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Opaque.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Opaque.java new file mode 100644 index 00000000000..9d7bf8d1c19 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Opaque.java @@ -0,0 +1,6 @@ +public class Opaque +{ + static Foo opaqueMethod() { + return null; + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.class new file mode 100644 index 00000000000..5bdb52e0006 Binary files /dev/null and b/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.class differ diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.java new file mode 100644 index 00000000000..dc1cbf52248 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.java @@ -0,0 +1,5 @@ +public class TestClass { + public static void testFunction() { + int x = Opaque.opaqueMethod().subType.x; + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc new file mode 100644 index 00000000000..882dc0b8b44 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc @@ -0,0 +1,13 @@ +CORE symex-driven-lazy-loading-expected-failure +TestClass.class +--function TestClass.testFunction --lazy-methods --verbosity 10 +CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V +CI lazy methods: elaborate java::Bar\.cproverNondetInitialize:\(\)V +CI lazy methods: elaborate java::Baz\.cproverNondetInitialize:\(\)V +CI lazy methods: elaborate java::GenFiller\.cproverNondetInitialize:\(\)V +-- +-- +Testing that the return type of an opaque method is correctly elaborated. The +cproverNondetInitialize should be loaded for all classes where an instance might +be seen. +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 3a8eae3fc30..647dc6b9c84 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -113,7 +113,10 @@ bool ci_lazy_methodst::operator()( { std::unordered_set initial_callable_methods; ci_lazy_methods_neededt initial_lazy_methods( - initial_callable_methods, instantiated_classes, symbol_table); + initial_callable_methods, + instantiated_classes, + symbol_table, + pointer_type_selector); initialize_instantiated_classes( methods_to_convert_later, namespacet(symbol_table), initial_lazy_methods); methods_to_convert_later.insert( @@ -174,17 +177,6 @@ bool ci_lazy_methodst::operator()( symbol_table); } - // cproverNondetInitialize has to be force-loaded for mocks to return valid - // objects (objects which satisfy invariants specified in the - // cproverNondetInitialize method) - for(const auto &class_name : instantiated_classes) - { - const irep_idt cprover_validate = - id2string(class_name) + ".cproverNondetInitialize:()V"; - if(symbol_table.symbols.count(cprover_validate)) - methods_already_populated.insert(cprover_validate); - } - // Remove symbols for methods that were declared but never used: symbol_tablet keep_symbols; // Manually keep @inflight_exception, as it is unused at this stage @@ -298,7 +290,10 @@ ci_lazy_methodst::convert_and_analyze_method( // Note this wraps *references* to methods_to_convert_later & // instantiated_classes ci_lazy_methods_neededt needed_methods( - methods_to_convert_later, instantiated_classes, symbol_table); + methods_to_convert_later, + instantiated_classes, + symbol_table, + pointer_type_selector); const bool could_not_convert_function = method_converter(method_name, needed_methods); @@ -430,8 +425,7 @@ void ci_lazy_methodst::initialize_instantiated_classes( if(param.type().id()==ID_pointer) { const pointer_typet &original_pointer=to_pointer_type(param.type()); - initialize_all_instantiated_classes_from_pointer( - original_pointer, ns, needed_lazy_methods); + needed_lazy_methods.add_all_needed_classes(original_pointer); } } } @@ -448,75 +442,6 @@ void ci_lazy_methodst::initialize_instantiated_classes( needed_lazy_methods.add_needed_class("java::" + id2string(id)); } -/// Build up list of methods for types for a pointer and any types it -/// might be subsituted for. See -/// `initialize_instantiated_classes` for more details. -/// \param pointer_type: The type to gather methods for. -/// \param ns: global namespace -/// \param [out] needed_lazy_methods: Populated with all Java reference types -/// whose references may be passed, directly or indirectly, to any of the -/// functions in `entry_points` -void ci_lazy_methodst::initialize_all_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods) -{ - initialize_instantiated_classes_from_pointer( - pointer_type, - ns, - needed_lazy_methods); - - // TODO we should be passing here a map that maps generic parameters - // to concrete types in the current context TG-2664 - const pointer_typet &subbed_pointer_type = - pointer_type_selector.convert_pointer_type(pointer_type, {}, ns); - - if(subbed_pointer_type!=pointer_type) - { - initialize_instantiated_classes_from_pointer( - subbed_pointer_type, ns, needed_lazy_methods); - } -} - -/// Build up list of methods for types for a specific pointer type. See -/// `initialize_instantiated_classes` for more details. -/// \param pointer_type: The type to gather methods for. -/// \param ns: global namespace -/// \param [out] needed_lazy_methods: Populated with all Java reference types -/// whose references may be passed, directly or indirectly, to any of the -/// functions in `entry_points` -void ci_lazy_methodst::initialize_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods) -{ - const symbol_typet &class_type=to_symbol_type(pointer_type.subtype()); - const auto ¶m_classid=class_type.get_identifier(); - - // Note here: different arrays may have different element types, so we should - // explore again even if we've seen this classid before in the array case. - if(needed_lazy_methods.add_needed_class(param_classid) || - is_java_array_tag(param_classid)) - { - gather_field_types(pointer_type.subtype(), ns, needed_lazy_methods); - } - - if(is_java_generic_type(pointer_type)) - { - // Assume if this is a generic like X, then any concrete parameters - // will at some point be instantiated. - const auto &generic_args = - to_java_generic_type(pointer_type).generic_type_arguments(); - for(const auto &generic_arg : generic_args) - { - if(!is_java_generic_parameter(generic_arg)) - { - initialize_instantiated_classes_from_pointer( - generic_arg, ns, needed_lazy_methods); - } - } - } -} /// Get places where virtual functions are called. /// \param e: expression tree to search @@ -611,64 +536,6 @@ void ci_lazy_methodst::gather_needed_globals( gather_needed_globals(*opit, symbol_table, needed); } -/// See param needed_lazy_methods -/// \param class_type: root of class tree to search -/// \param ns: global namespace -/// \param [out] needed_lazy_methods: Popualted with all Java reference types -/// reachable starting at `class_type`. For example if `class_type` is -/// `symbol_typet("java::A")` and A has a B field, then `B` (but not `A`) will -/// noted as a needed class. -void ci_lazy_methodst::gather_field_types( - const typet &class_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods) -{ - const auto &underlying_type=to_struct_type(ns.follow(class_type)); - if(is_java_array_tag(underlying_type.get_tag())) - { - // If class_type is not a symbol this may be a reference array, - // but we can't tell what type. - if(class_type.id() == ID_symbol) - { - const typet &element_type = - java_array_element_type(to_symbol_type(class_type)); - if(element_type.id() == ID_pointer) - { - // This is a reference array -- mark its element type available. - initialize_all_instantiated_classes_from_pointer( - to_pointer_type(element_type), ns, needed_lazy_methods); - } - } - } - else - { - for(const auto &field : underlying_type.components()) - { - if(field.type().id() == ID_struct || field.type().id() == ID_symbol) - gather_field_types(field.type(), ns, needed_lazy_methods); - else if(field.type().id() == ID_pointer) - { - if(field.type().subtype().id() == ID_symbol) - { - initialize_all_instantiated_classes_from_pointer( - to_pointer_type(field.type()), ns, needed_lazy_methods); - } - else - { - // If raw structs were possible this would lead to missed - // dependencies, as both array element and specialised generic type - // information cannot be obtained in this case. - // We should therefore only be skipping pointers such as the uint16t* - // in our internal String representation. - INVARIANT( - field.type().subtype().id() != ID_struct, - "struct types should be referred to by symbol at this stage"); - } - } - } - } -} - /// Find a virtual callee, if one is defined and the callee type is known to /// exist. /// \param instantiated_classes: set of classes that can be instantiated. diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index 156e67fe240..7e9d506488c 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods.h @@ -121,16 +121,6 @@ class ci_lazy_methodst:public messaget const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods); - void initialize_all_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods); - - void initialize_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods); - void gather_virtual_callsites( const exprt &e, std::unordered_set &result); @@ -146,11 +136,6 @@ class ci_lazy_methodst:public messaget const symbol_tablet &symbol_table, symbol_tablet &needed); - void gather_field_types( - const typet &class_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods); - irep_idt get_virtual_method_target( const std::unordered_set &instantiated_classes, const irep_idt &call_basename, diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index e3b10b0ebbf..b1467c205c0 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -11,12 +11,14 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "ci_lazy_methods.h" +#include #include +#include +#include /// Notes `method_symbol_name` is referenced from some reachable function, and /// should therefore be elaborated. -/// \par parameters: `method_symbol_name`: method name; must exist in symbol -/// table. +/// \param: `method_symbol_name`: method name; must exist in symbol table. void ci_lazy_methods_neededt::add_needed_method( const irep_idt &method_symbol_name) { @@ -26,8 +28,7 @@ void ci_lazy_methods_neededt::add_needed_method( /// Notes class `class_symbol_name` will be instantiated, or a static field /// belonging to it will be accessed. Also notes that its static initializer is /// therefore reachable. -/// \par parameters: `class_symbol_name`: class name; must exist in symbol -/// table. +/// \param: `class_symbol_name`: class name; must exist in symbol table. /// \return Returns true if `class_symbol_name` is new (not seen before). bool ci_lazy_methods_neededt::add_needed_class( const irep_idt &class_symbol_name) @@ -43,3 +44,109 @@ bool ci_lazy_methods_neededt::add_needed_class( return true; } + +/// Add to the needed classes all classes specified, the replacement type if it +/// will be replaced, and all fields it contains. +/// \param pointer_type: The type to add +void ci_lazy_methods_neededt::add_all_needed_classes( + const pointer_typet &pointer_type) +{ + namespacet ns{symbol_table}; + + initialize_instantiated_classes_from_pointer(pointer_type, ns); + + // TODO we should be passing here a map that maps generic parameters + // to concrete types in the current context TG-2664 + const pointer_typet &subbed_pointer_type = + pointer_type_selector.convert_pointer_type(pointer_type, {}, ns); + + if(subbed_pointer_type != pointer_type) + { + initialize_instantiated_classes_from_pointer(subbed_pointer_type, ns); + } +} + +/// Build up list of methods for types for a specific pointer type. See +/// `add_all_needed_classes` for more details. +/// \param pointer_type: The type to gather methods for. +/// \param ns: global namespace +void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer( + const pointer_typet &pointer_type, + const namespacet &ns) +{ + const symbol_typet &class_type = to_symbol_type(pointer_type.subtype()); + const auto ¶m_classid = class_type.get_identifier(); + + // Note here: different arrays may have different element types, so we should + // explore again even if we've seen this classid before in the array case. + if(add_needed_class(param_classid) || is_java_array_tag(param_classid)) + { + gather_field_types(pointer_type.subtype(), ns); + } + + if(is_java_generic_type(pointer_type)) + { + // Assume if this is a generic like X, then any concrete parameters + // will at some point be instantiated. + const auto &generic_args = + to_java_generic_type(pointer_type).generic_type_arguments(); + for(const auto &generic_arg : generic_args) + { + if(!is_java_generic_parameter(generic_arg)) + { + initialize_instantiated_classes_from_pointer(generic_arg, ns); + } + } + } +} + +/// For a given type, gather all fields referenced by that type +/// \param class_type: root of class tree to search +/// \param ns: global namespaces. +void ci_lazy_methods_neededt::gather_field_types( + const typet &class_type, + const namespacet &ns) +{ + const auto &underlying_type = to_struct_type(ns.follow(class_type)); + if(is_java_array_tag(underlying_type.get_tag())) + { + // If class_type is not a symbol this may be a reference array, + // but we can't tell what type. + if(class_type.id() == ID_symbol) + { + const typet &element_type = + java_array_element_type(to_symbol_type(class_type)); + if(element_type.id() == ID_pointer) + { + // This is a reference array -- mark its element type available. + add_all_needed_classes(to_pointer_type(element_type)); + } + } + } + else + { + for(const auto &field : underlying_type.components()) + { + if(field.type().id() == ID_struct || field.type().id() == ID_symbol) + gather_field_types(field.type(), ns); + else if(field.type().id() == ID_pointer) + { + if(field.type().subtype().id() == ID_symbol) + { + add_all_needed_classes(to_pointer_type(field.type())); + } + else + { + // If raw structs were possible this would lead to missed + // dependencies, as both array element and specialised generic type + // information cannot be obtained in this case. + // We should therefore only be skipping pointers such as the uint16t* + // in our internal String representation. + INVARIANT( + field.type().subtype().id() != ID_struct, + "struct types should be referred to by symbol at this stage"); + } + } + } + } +} diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h index ecb95c0d129..e062962050d 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h @@ -17,22 +17,29 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +class select_pointer_typet; +class pointer_typet; + class ci_lazy_methods_neededt { public: ci_lazy_methods_neededt( std::unordered_set &_callable_methods, std::unordered_set &_instantiated_classes, - symbol_tablet &_symbol_table) + symbol_tablet &_symbol_table, + const select_pointer_typet &pointer_type_selector) : callable_methods(_callable_methods), instantiated_classes(_instantiated_classes), - symbol_table(_symbol_table) + symbol_table(_symbol_table), + pointer_type_selector(pointer_type_selector) {} void add_needed_method(const irep_idt &); // Returns true if new bool add_needed_class(const irep_idt &); + void add_all_needed_classes(const pointer_typet &pointer_type); + private: // callable_methods is a vector because it's used as a work-list // which is periodically cleared. It can't be relied upon to @@ -45,6 +52,14 @@ class ci_lazy_methods_neededt // repeatedly exploring a class hierarchy. std::unordered_set &instantiated_classes; symbol_tablet &symbol_table; + + const select_pointer_typet &pointer_type_selector; + + void initialize_instantiated_classes_from_pointer( + const pointer_typet &pointer_type, + const namespacet &ns); + + void gather_field_types(const typet &class_type, const namespacet &ns); }; #endif diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 6baf3216e63..155304d7514 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1038,6 +1038,26 @@ bool java_bytecode_languaget::convert_single_method( return false; } + // The return of an opaque function is a source of an otherwise invisible + // instantiation, so here we ensure we've loaded the appropriate classes. + const code_typet function_type = to_code_type(symbol.type); + if( + const pointer_typet *pointer_return_type = + type_try_dynamic_cast(function_type.return_type())) + { + // If the return type is abstract, we won't forcibly instantiate it here + // otherwise this can cause abstract methods to be explictly called + // TODO(tkiley): Arguably no abstract class should ever be added to + // TODO(tkiley): ci_lazy_methods_neededt, but this needs further + // TODO(tkiley): investigation + namespacet ns{symbol_table}; + const java_class_typet &underlying_type = + to_java_class_type(ns.follow(pointer_return_type->subtype())); + + if(!underlying_type.is_abstract()) + needed_lazy_methods->add_all_needed_classes(*pointer_return_type); + } + return true; } diff --git a/src/util/std_types.h b/src/util/std_types.h index 591a91d4de4..9693f10b78e 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -151,6 +151,12 @@ inline symbol_typet &to_symbol_type(typet &type) return static_cast(type); } +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_symbol; +} + /*! \brief Base type of C structs and unions, and C++ classes */ class struct_union_typet:public typet