Add unit tests for mocked/unsupported generics

Author: svorenova

unit/goto-programs/goto_program_generics/GenericBases.java

@@ -103,3 +103,15 @@ public void foo() {
     f.inner_three.foo(x);
   }
 }
+
+class SuperclassUnsupported extends UnsupportedWrapper1<SuperclassUnsupported> {
+  public void foo() {
+    this.field = new SuperclassUnsupported();
+  }
+}
+
+class SuperclassMocked extends MockedWrapper<IWrapper> {
+  public void foo() {
+      this.field.i = 5;
+    }
+}

unit/goto-programs/goto_program_generics/GenericFieldMocked.class

@@ -80,3 +80,35 @@ public void foo(A<Integer> v) {
     }
   }
 }
+
+// class that implements two generic interfaces
+class InterfacesImplementation implements InterfaceWrapper<IWrapper>,
+                         InterfacePairWrapper<IWrapper, IWrapper> {
+  public IWrapper method(IWrapper t) {
+    return t;
+  }
+  public IWrapper method(IWrapper t, IWrapper tt) {
+    if (t.i>0)
+    {
+      return t;
+    }
+    else
+    {
+      return tt;
+    }
+  }
+}
+class GenericFieldUnsupported {
+  public UnsupportedWrapper2<InterfacesImplementation> f;
+  public void foo() {
+    f.field.method(new IWrapper(0));
+    f.field.method(new IWrapper(0), new IWrapper(2));
+  }
+}
+
+class GenericFieldMocked {
+  public MockedWrapper<IWrapper> f;
+  public void foo() {
+    f.field.i = 0;
+  }
+}

unit/goto-programs/goto_program_generics/GenericFieldUnsupported.class

@@ -23,3 +23,24 @@ class PairWrapper<K, V> {
 interface InterfaceWrapper<T> {
   public T method(T t);
 }
+
+// generic interface with two parameters
+interface InterfacePairWrapper<K, V> {
+  public K method(K k, V v);
+}
+
+// generic class with unsupported signature - generic bound
+class UnsupportedWrapper1<T extends UnsupportedWrapper1<T>> {
+  public T field;
+}
+
+// generic class with unsupported signature - multiple bounds
+class UnsupportedWrapper2<T extends InterfaceWrapper & InterfacePairWrapper>
+{
+  public T field;
+}
+
+// generic mocked class, make sure the .class file is not available
+class MockedWrapper<T> {
+  public T field;
+}

unit/goto-programs/goto_program_generics/GenericFields.java

@@ -9,6 +9,7 @@
 #include <testing-utils/load_java_class.h>
 #include <testing-utils/require_goto_statements.h>
 #include <util/config.h>
+#include <testing-utils/require_type.h>
 
 // NOTE: To inspect these tests at any point, use expr2java.
 // A good way to verify the validity of a test is to iterate
@@ -412,3 +413,99 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "Ignore generics for incomplete and non-generic bases",
+  "[core][goto_program_generics][generic_bases_test]")
+{
+  GIVEN(
+    "A class extending a generic class with unsupported class signature (thus"
+    " not marked as generic)")
+  {
+    const symbol_tablet &symbol_table = load_java_class(
+      "SuperclassUnsupported",
+      "./goto-programs/goto_program_generics",
+      "SuperclassUnsupported.foo");
+
+    THEN("The struct for UnsupportedWrapper1 is complete and non-generic")
+    {
+      const std::string superclass_name = "java::UnsupportedWrapper1";
+      REQUIRE(symbol_table.has_symbol(superclass_name));
+
+      const symbolt &superclass_symbol =
+        symbol_table.lookup_ref(superclass_name);
+      require_type::require_java_non_generic_class(superclass_symbol.type);
+    }
+
+    WHEN("The method input argument is created in the entry point function")
+    {
+      const std::vector<codet> &entry_point_code =
+        require_goto_statements::require_entry_point_statements(symbol_table);
+
+      // For an explanation of this part, look at the comments for the similar
+      // parts of the previous tests.
+      const irep_idt &this_tmp_name =
+        require_goto_statements::require_entry_point_argument_assignment(
+          "this", entry_point_code);
+
+      THEN("Object 'this' created has unspecialized inherited field")
+      {
+        require_goto_statements::require_struct_component_assignment(
+          this_tmp_name,
+          {"UnsupportedWrapper1"},
+          "field",
+          "java::java.lang.Object",
+          {},
+          entry_point_code);
+      }
+    }
+  }
+
+  GIVEN(
+    "A class extending a generic class that is mocked (thus incomplete and not "
+    "marked as generic)")
+  {
+    const symbol_tablet &symbol_table = load_java_class(
+      "SuperclassMocked",
+      "./goto-programs/goto_program_generics",
+      "SuperclassMocked.foo");
+
+    THEN("The struct for MockedWrapper is incomplete and not-generic")
+    {
+      const std::string superclass_name = "java::MockedWrapper";
+      REQUIRE(symbol_table.has_symbol(superclass_name));
+
+      const symbolt &superclass_symbol =
+        symbol_table.lookup_ref(superclass_name);
+      const java_class_typet &superclass_type =
+        to_java_class_type(to_class_type(superclass_symbol.type));
+      REQUIRE(
+        to_class_type(superclass_symbol.type).get_bool(ID_incomplete_class));
+      REQUIRE(!is_java_generic_class_type(superclass_type));
+      REQUIRE(!is_java_implicitly_generic_class_type(superclass_type));
+    }
+
+    WHEN("The method input argument is created in the entry point function")
+    {
+      const std::vector<codet> &entry_point_code =
+        require_goto_statements::require_entry_point_statements(symbol_table);
+
+      // For an explanation of this part, look at the comments for the similar
+      // parts of the previous tests.
+      const irep_idt &this_tmp_name =
+        require_goto_statements::require_entry_point_argument_assignment(
+          "this", entry_point_code);
+
+      THEN("Object 'this' created has unspecialized inherited field")
+      {
+        require_goto_statements::require_struct_component_assignment(
+          this_tmp_name,
+          {"MockedWrapper"},
+          "field",
+          "java::java.lang.Object",
+          {},
+          entry_point_code);
+      }
+    }
+  }
+}

unit/goto-programs/goto_program_generics/GenericHelper.java

@@ -9,6 +9,7 @@
 #include <testing-utils/load_java_class.h>
 #include <testing-utils/require_goto_statements.h>
 #include <util/config.h>
+#include <testing-utils/require_type.h>
 
 // NOTE: To inspect these tests at any point, use expr2java.
 // A good way to verify the validity of a test is to iterate
@@ -486,3 +487,124 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "Ignore generic parameters in fields and methods with incomplete and "
+  "non-generic types",
+  "[core][goto_program_generics][generic_parameters_test]")
+{
+  GIVEN(
+    "A class with a generic field pointing to a class with unsupported "
+    "signature (thus not marked as generic)")
+  {
+    const symbol_tablet &symbol_table = load_java_class(
+      "GenericFieldUnsupported",
+      "./goto-programs/goto_program_generics",
+      "GenericFieldUnsupported.foo");
+
+    THEN("The struct for UnsupportedWrapper2 is complete and non-generic")
+    {
+      const std::string superclass_name = "java::UnsupportedWrapper2";
+      REQUIRE(symbol_table.has_symbol(superclass_name));
+
+      const symbolt &superclass_symbol =
+        symbol_table.lookup_ref(superclass_name);
+      require_type::require_java_non_generic_class(superclass_symbol.type);
+    }
+
+    WHEN("The method input argument is created in the entry point function")
+    {
+      // For an explanation of this part, look at the comments for the similar
+      // parts of the previous tests.
+      const std::vector<codet> &entry_point_code =
+        require_goto_statements::require_entry_point_statements(symbol_table);
+
+      const irep_idt &tmp_object_name =
+        require_goto_statements::require_entry_point_argument_assignment(
+          "this", entry_point_code);
+
+      THEN("Object 'this' has field 'f' of type UnsupportedWrapper2")
+      {
+        const auto &field_input_name =
+          require_goto_statements::require_struct_component_assignment(
+            tmp_object_name,
+            {},
+            "f",
+            "java::UnsupportedWrapper2",
+            {},
+            entry_point_code);
+
+        THEN("Object 'f' has unspecialized field 'field'")
+        {
+          require_goto_statements::require_struct_component_assignment(
+            field_input_name,
+            {},
+            "field",
+            "java::java.lang.Object",
+            {},
+            entry_point_code);
+        }
+      }
+    }
+  }
+
+  GIVEN(
+    "A class with a generic field pointing to a mocked class (thus "
+    "incomplete and not marked as generic)")
+  {
+    const symbol_tablet &symbol_table = load_java_class(
+      "GenericFieldMocked",
+      "./goto-programs/goto_program_generics",
+      "GenericFieldMocked.foo");
+
+    THEN("The struct for MockedWrapper is incomplete and not-generic")
+    {
+      const std::string superclass_name = "java::MockedWrapper";
+      REQUIRE(symbol_table.has_symbol(superclass_name));
+
+      const symbolt &superclass_symbol =
+        symbol_table.lookup_ref(superclass_name);
+      const java_class_typet &superclass_type =
+        to_java_class_type(to_class_type(superclass_symbol.type));
+      REQUIRE(
+        to_class_type(superclass_symbol.type).get_bool(ID_incomplete_class));
+      REQUIRE(!is_java_generic_class_type(superclass_type));
+      REQUIRE(!is_java_implicitly_generic_class_type(superclass_type));
+    }
+
+    WHEN("The method input argument is created in the entry point function")
+    {
+      // For an explanation of this part, look at the comments for the similar
+      // parts of the previous tests.
+      const std::vector<codet> &entry_point_code =
+        require_goto_statements::require_entry_point_statements(symbol_table);
+
+      const irep_idt &tmp_object_name =
+        require_goto_statements::require_entry_point_argument_assignment(
+          "this", entry_point_code);
+
+      THEN("Object 'this' has field 'f' of type MockedWrapper")
+      {
+        const auto &field_input_name =
+          require_goto_statements::require_struct_component_assignment(
+            tmp_object_name,
+            {},
+            "f",
+            "java::MockedWrapper",
+            {},
+            entry_point_code);
+
+        THEN("Object 'f' has unspecialized field 'field'")
+        {
+          require_goto_statements::require_struct_component_assignment(
+            field_input_name,
+            {},
+            "field",
+            "java::java.lang.Object",
+            {},
+            entry_point_code);
+        }
+      }
+    }
+  }
+}