TG-1877: Include array pointer types in needed classes

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

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); }
+
+}

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

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); }
+
+}

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

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<test> 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<T> {
+  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); }
+
+}

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

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<Integer, test> 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<S, T> {
+  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); }
+
+}

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.

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<container<test>> c) {
+
+    if(c == null)
+      return;
+    container<test> 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<T> {
+  public T[] test_array;
+}
+
+class container2<T> {
+  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); }
+
+}

src/java_bytecode/ci_lazy_methods.cpp

@@ -7,7 +7,6 @@
 \*******************************************************************/
 #include "ci_lazy_methods.h"
 
-
 #include <java_bytecode/java_entry_point.h>
 #include <java_bytecode/java_class_loader.h>
 #include <java_bytecode/java_utils.h>
@@ -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<A, B, C>, 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");
+        }
+      }
     }
   }
 }