diff --git a/regression/cbmc-java/lazyloading_array_parameter/asserthere.class b/regression/cbmc-java/lazyloading_array_parameter/asserthere.class new file mode 100644 index 00000000000..1ee2ea18dc1 Binary files /dev/null and b/regression/cbmc-java/lazyloading_array_parameter/asserthere.class differ diff --git a/regression/cbmc-java/lazyloading_array_parameter/test.class b/regression/cbmc-java/lazyloading_array_parameter/test.class new file mode 100644 index 00000000000..89b0a7dab49 Binary files /dev/null and b/regression/cbmc-java/lazyloading_array_parameter/test.class differ diff --git a/regression/cbmc-java/lazyloading_array_parameter/test.desc b/regression/cbmc-java/lazyloading_array_parameter/test.desc new file mode 100644 index 00000000000..15e3f99d782 --- /dev/null +++ b/regression/cbmc-java/lazyloading_array_parameter/test.desc @@ -0,0 +1,7 @@ +CORE +test.class +--lazy-methods --verbosity 10 --function test.g +^EXIT=0$ +^SIGNAL=0$ +elaborate java::test\.f:\(\)I +VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading_array_parameter/test.java b/regression/cbmc-java/lazyloading_array_parameter/test.java new file mode 100644 index 00000000000..db6730e70e5 --- /dev/null +++ b/regression/cbmc-java/lazyloading_array_parameter/test.java @@ -0,0 +1,22 @@ + +public class test { + + public int f() { return 1; } + + public static void g(test[] args) { + + if(args == null || args.length != 1 || args[0] == null) + return; + asserthere.doassert(args[0].f() == 1); + + } + +} + +class asserthere { + + // Used to avoid lazy-loading currently marking any class with an + // $assertionsEnabled member (i.e. any class that asserts) as needed. + public static void doassert(boolean condition) { assert(condition); } + +} diff --git a/regression/cbmc-java/lazyloading_indirect_array_parameter/asserthere.class b/regression/cbmc-java/lazyloading_indirect_array_parameter/asserthere.class new file mode 100644 index 00000000000..b59863c8fae Binary files /dev/null and b/regression/cbmc-java/lazyloading_indirect_array_parameter/asserthere.class differ diff --git a/regression/cbmc-java/lazyloading_indirect_array_parameter/container.class b/regression/cbmc-java/lazyloading_indirect_array_parameter/container.class new file mode 100644 index 00000000000..98dc6905dcd Binary files /dev/null and b/regression/cbmc-java/lazyloading_indirect_array_parameter/container.class differ diff --git a/regression/cbmc-java/lazyloading_indirect_array_parameter/test.class b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.class new file mode 100644 index 00000000000..39b01757de3 Binary files /dev/null and b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.class differ diff --git a/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc new file mode 100644 index 00000000000..15e3f99d782 --- /dev/null +++ b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc @@ -0,0 +1,7 @@ +CORE +test.class +--lazy-methods --verbosity 10 --function test.g +^EXIT=0$ +^SIGNAL=0$ +elaborate java::test\.f:\(\)I +VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading_indirect_array_parameter/test.java b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.java new file mode 100644 index 00000000000..f769643b86d --- /dev/null +++ b/regression/cbmc-java/lazyloading_indirect_array_parameter/test.java @@ -0,0 +1,29 @@ + +public class test { + + public int f() { return 1; } + + public static void g(container c) { + + if(c == null) + return; + test[] args = c.test_array; + if(args == null || args.length != 1 || args[0] == null) + return; + asserthere.doassert(args[0].f() == 1); + + } + +} + +class container { + public test[] test_array; +} + +class asserthere { + + // Used to avoid lazy-loading currently marking any class with an + // $assertionsEnabled member (i.e. any class that asserts) as needed. + public static void doassert(boolean condition) { assert(condition); } + +} diff --git a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/asserthere.class b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/asserthere.class new file mode 100644 index 00000000000..9368ffae749 Binary files /dev/null and b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/asserthere.class differ diff --git a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/container.class b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/container.class new file mode 100644 index 00000000000..1de2963dcbd Binary files /dev/null and b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/container.class differ diff --git a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.class b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.class new file mode 100644 index 00000000000..75992ea936b Binary files /dev/null and b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.class differ diff --git a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc new file mode 100644 index 00000000000..15e3f99d782 --- /dev/null +++ b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc @@ -0,0 +1,7 @@ +CORE +test.class +--lazy-methods --verbosity 10 --function test.g +^EXIT=0$ +^SIGNAL=0$ +elaborate java::test\.f:\(\)I +VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.java b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.java new file mode 100644 index 00000000000..e4dcf1dfcc6 --- /dev/null +++ b/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.java @@ -0,0 +1,29 @@ + +public class test { + + public int f() { return 1; } + + public static void g(container c) { + + if(c == null) + return; + test[] args = c.test_array; + if(args == null || args.length != 1 || args[0] == null) + return; + asserthere.doassert(args[0].f() == 1); + + } + +} + +class container { + public T[] test_array; +} + +class asserthere { + + // Used to avoid lazy-loading currently marking any class with an + // $assertionsEnabled member (i.e. any class that asserts) as needed. + public static void doassert(boolean condition) { assert(condition); } + +} diff --git a/regression/cbmc-java/lazyloading_multiple_generic_parameters/asserthere.class b/regression/cbmc-java/lazyloading_multiple_generic_parameters/asserthere.class new file mode 100644 index 00000000000..6c09f10e287 Binary files /dev/null and b/regression/cbmc-java/lazyloading_multiple_generic_parameters/asserthere.class differ diff --git a/regression/cbmc-java/lazyloading_multiple_generic_parameters/container.class b/regression/cbmc-java/lazyloading_multiple_generic_parameters/container.class new file mode 100644 index 00000000000..39645cf007c Binary files /dev/null and b/regression/cbmc-java/lazyloading_multiple_generic_parameters/container.class differ diff --git a/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.class b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.class new file mode 100644 index 00000000000..a46b3d3c1af Binary files /dev/null and b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.class differ diff --git a/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc new file mode 100644 index 00000000000..15e3f99d782 --- /dev/null +++ b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc @@ -0,0 +1,7 @@ +CORE +test.class +--lazy-methods --verbosity 10 --function test.g +^EXIT=0$ +^SIGNAL=0$ +elaborate java::test\.f:\(\)I +VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.java b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.java new file mode 100644 index 00000000000..a9974960830 --- /dev/null +++ b/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.java @@ -0,0 +1,29 @@ + +public class test { + + public int f() { return 1; } + + public static void g(container c) { + + if(c == null) + return; + test[] args = c.test_array; + if(args == null || args.length != 1 || args[0] == null) + return; + asserthere.doassert(args[0].f() == 1); + + } + +} + +class container { + public T[] test_array; +} + +class asserthere { + + // Used to avoid lazy-loading currently marking any class with an + // $assertionsEnabled member (i.e. any class that asserts) as needed. + public static void doassert(boolean condition) { assert(condition); } + +} diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/asserthere.class b/regression/cbmc-java/lazyloading_nested_generic_parameters/asserthere.class new file mode 100644 index 00000000000..fe2c323e94c Binary files /dev/null and b/regression/cbmc-java/lazyloading_nested_generic_parameters/asserthere.class differ diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/container.class b/regression/cbmc-java/lazyloading_nested_generic_parameters/container.class new file mode 100644 index 00000000000..df2a7d995f5 Binary files /dev/null and b/regression/cbmc-java/lazyloading_nested_generic_parameters/container.class differ diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/container2.class b/regression/cbmc-java/lazyloading_nested_generic_parameters/container2.class new file mode 100644 index 00000000000..69240fedfc8 Binary files /dev/null and b/regression/cbmc-java/lazyloading_nested_generic_parameters/container2.class differ diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/test.class b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.class new file mode 100644 index 00000000000..7f9ac7fe0ce Binary files /dev/null and b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.class differ diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc new file mode 100644 index 00000000000..ae44ea6da9b --- /dev/null +++ b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc @@ -0,0 +1,13 @@ +KNOWNBUG +test.class +--lazy-methods --verbosity 10 --function test.g +^EXIT=0$ +^SIGNAL=0$ +elaborate java::test\.f:\(\)I +VERIFICATION SUCCESSFUL +-- +-- +The right methods are loaded, but verification is not successful +because __CPROVER_start doesn't create appropriately typed input for +this kind of nested generic parameter, so dynamic cast checks fail upon +fetching the generic type's field. diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/test.java b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.java new file mode 100644 index 00000000000..564c26eb88e --- /dev/null +++ b/regression/cbmc-java/lazyloading_nested_generic_parameters/test.java @@ -0,0 +1,36 @@ + +public class test { + + public int f() { return 1; } + + public static void g(container2> c) { + + if(c == null) + return; + container outer = c.next; + if(outer == null) + return; + test[] args = outer.test_array; + if(args == null || args.length != 1 || args[0] == null) + return; + asserthere.doassert(args[0].f() == 1); + + } + +} + +class container { + public T[] test_array; +} + +class container2 { + public T next; +} + +class asserthere { + + // Used to avoid lazy-loading currently marking any class with an + // $assertionsEnabled member (i.e. any class that asserts) as needed. + public static void doassert(boolean condition) { assert(condition); } + +} diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index dd434acb372..0daa4aac95a 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -7,7 +7,6 @@ \*******************************************************************/ #include "ci_lazy_methods.h" - #include #include #include @@ -345,6 +344,22 @@ void ci_lazy_methodst::initialize_needed_classes_from_pointer( { 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_needed_classes_from_pointer( + generic_arg, ns, needed_lazy_methods); + } + } + } } /// Get places where virtual functions are called. @@ -477,17 +492,47 @@ void ci_lazy_methodst::gather_field_types( ci_lazy_methods_neededt &needed_lazy_methods) { const auto &underlying_type=to_struct_type(ns.follow(class_type)); - for(const auto &field : underlying_type.components()) + if(is_java_array_tag(underlying_type.get_tag())) { - 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 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) { - // Skip array primitive pointers, for example: - if(field.type().subtype().id()!=ID_symbol) - continue; - initialize_all_needed_classes_from_pointer( - to_pointer_type(field.type()), ns, needed_lazy_methods); + 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_needed_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_needed_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"); + } + } } } }