TG-1877: Include array pointer types in needed classes

Lazy methods attempts a pointer graph walk starting from the main function's
parameters to determine what classes may exist before the main function is
entered; for example, starting at f(A a) implies that an A instance may exist,
and if A itself has a B field that too might exist, and so on. However, until
now this failed to account for array-typed parameters and fields. This commit
amends gather_field_types to account for this special case.

This also adds a test for the generic parameter case, which is not solved yet.

Author: smowton

regression/cbmc-java/lazyloading_array_parameter/asserthere.class

@@ -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.class

@@ -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_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,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_array_parameter/asserthere.class

@@ -0,0 +1,10 @@
+KNOWNBUG
+test.class
+--lazy-methods --verbosity 10 --function test.g
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::test\.f:\(\)I
+VERIFICATION SUCCESSFUL
+--
+--
+See https://diffblue.atlassian.net/browse/TG-1877

regression/cbmc-java/lazyloading_indirect_array_parameter/container.class

@@ -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_indirect_array_parameter/test.class

@@ -477,17 +477,33 @@ 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)
+      {
+        initialize_all_needed_classes_from_pointer(
+          to_pointer_type(field.type()), ns, needed_lazy_methods);
+      }
     }
   }
 }