Skip to content

Commit ae89c94

Browse files
committed
Lazy loading: assume concrete generic parameter types are needed
This extends the previous commit to assume that generic parameter types are needed, which overapproximates what is requried, but seems likely to suffice in most cases.
1 parent 80eb6a6 commit ae89c94

File tree

13 files changed

+118
-7
lines changed

13 files changed

+118
-7
lines changed
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
test.class
33
--lazy-methods --verbosity 10 --function test.g
44
^EXIT=0$
55
^SIGNAL=0$
66
elaborate java::test\.f:\(\)I
77
VERIFICATION SUCCESSFUL
8-
--
9-
--
10-
See https://diffblue.atlassian.net/browse/TG-1877
Binary file not shown.
Binary file not shown.
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.g
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
elaborate java::test\.f:\(\)I
7+
VERIFICATION SUCCESSFUL
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
2+
public class test {
3+
4+
public int f() { return 1; }
5+
6+
public static void g(container<Integer, test> c) {
7+
8+
if(c == null)
9+
return;
10+
test[] args = c.test_array;
11+
if(args == null || args.length != 1 || args[0] == null)
12+
return;
13+
asserthere.doassert(args[0].f() == 1);
14+
15+
}
16+
17+
}
18+
19+
class container<S, T> {
20+
public T[] test_array;
21+
}
22+
23+
class asserthere {
24+
25+
// Used to avoid lazy-loading currently marking any class with an
26+
// $assertionsEnabled member (i.e. any class that asserts) as needed.
27+
public static void doassert(boolean condition) { assert(condition); }
28+
29+
}
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
KNOWNBUG
2+
test.class
3+
--lazy-methods --verbosity 10 --function test.g
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
elaborate java::test\.f:\(\)I
7+
VERIFICATION SUCCESSFUL
8+
--
9+
--
10+
The right methods are loaded, but verification is not successful
11+
because __CPROVER_start doesn't create appropriately typed input for
12+
this kind of nested generic parameter, so dynamic cast checks fail upon
13+
fetching the generic type's field.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
2+
public class test {
3+
4+
public int f() { return 1; }
5+
6+
public static void g(container2<container<test>> c) {
7+
8+
if(c == null)
9+
return;
10+
container<test> outer = c.next;
11+
if(outer == null)
12+
return;
13+
test[] args = outer.test_array;
14+
if(args == null || args.length != 1 || args[0] == null)
15+
return;
16+
asserthere.doassert(args[0].f() == 1);
17+
18+
}
19+
20+
}
21+
22+
class container<T> {
23+
public T[] test_array;
24+
}
25+
26+
class container2<T> {
27+
public T next;
28+
}
29+
30+
class asserthere {
31+
32+
// Used to avoid lazy-loading currently marking any class with an
33+
// $assertionsEnabled member (i.e. any class that asserts) as needed.
34+
public static void doassert(boolean condition) { assert(condition); }
35+
36+
}

src/java_bytecode/ci_lazy_methods.cpp

+32-3
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77
\*******************************************************************/
88
#include "ci_lazy_methods.h"
99

10-
1110
#include <java_bytecode/java_entry_point.h>
1211
#include <java_bytecode/java_class_loader.h>
1312
#include <java_bytecode/java_utils.h>
@@ -345,6 +344,22 @@ void ci_lazy_methodst::initialize_needed_classes_from_pointer(
345344
{
346345
gather_field_types(pointer_type.subtype(), ns, needed_lazy_methods);
347346
}
347+
348+
if(is_java_generic_type(pointer_type))
349+
{
350+
// Assume if this is a generic like X<A, B, C>, then any concrete parameters
351+
// will at some point be instantiated.
352+
const auto &generic_args =
353+
to_java_generic_type(pointer_type).generic_type_arguments();
354+
for(const auto &generic_arg : generic_args)
355+
{
356+
if(!is_java_generic_parameter(generic_arg))
357+
{
358+
initialize_needed_classes_from_pointer(
359+
generic_arg, ns, needed_lazy_methods);
360+
}
361+
}
362+
}
348363
}
349364

350365
/// Get places where virtual functions are called.
@@ -501,8 +516,22 @@ void ci_lazy_methodst::gather_field_types(
501516
gather_field_types(field.type(), ns, needed_lazy_methods);
502517
else if(field.type().id() == ID_pointer)
503518
{
504-
initialize_all_needed_classes_from_pointer(
505-
to_pointer_type(field.type()), ns, needed_lazy_methods);
519+
if(field.type().subtype().id() == ID_symbol)
520+
{
521+
initialize_all_needed_classes_from_pointer(
522+
to_pointer_type(field.type()), ns, needed_lazy_methods);
523+
}
524+
else
525+
{
526+
// If raw structs were possible this would lead to missed
527+
// dependencies, as both array element and specialised generic type
528+
// information cannot be obtained in this case.
529+
// We should therefore only be skipping pointers such as the uint16t*
530+
// in our internal String representation.
531+
INVARIANT(
532+
field.type().subtype().id() != ID_struct,
533+
"struct types should be referred to by symbol at this stage");
534+
}
506535
}
507536
}
508537
}

0 commit comments

Comments
 (0)