Add unit test with cycle of size 3 and skipped stack level

Author: Matthias Güdemann

jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class

@@ -1,3 +1,19 @@
+class Outer<K, V, U> {
+  class Inner<U> {
+    Outer<V, K, U> o;
+    U u;
+  }
+  Inner<U> inner;
+  K key;
+  V value;
+}
+class Three<X, E, U> {
+  Three<U, X, E> rotate;
+  Three<X, E, U> normal;
+  X x;
+  E e;
+  U u;
+}
 class KeyValue<K, V> {
     KeyValue<K, V> next;
     KeyValue<V, K> reverse;
@@ -6,6 +22,8 @@ class KeyValue<K, V> {
 }
 class MutuallyRecursiveGenerics {
   KeyValue<String, Integer> example1;
+  Three<Byte, Character, Integer> example2;
+  Outer<Boolean, Byte, Short> example3;
   void f() {
   }
 }

jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class

@@ -142,5 +142,169 @@ SCENARIO(
           reverse_field, "java::java.lang.Integer", "java::java.lang.String");
       }
     }
+    THEN(
+      "The Object has a field `example2` of type `Three<Byte, Character, "
+      "Integer>`")
+    {
+      const auto &example2_field =
+        require_goto_statements::require_struct_component_assignment(
+          tmp_object_name, {}, "example2", "java::Three", {}, entry_point_code);
+
+      auto has_x_u_e_fields = [&](
+        const irep_idt &field,
+        const irep_idt &x_type,
+        const irep_idt &e_type,
+        const irep_idt &u_type) {
+        require_goto_statements::require_struct_component_assignment(
+          field, {}, "x", x_type, {}, entry_point_code);
+        require_goto_statements::require_struct_component_assignment(
+          field, {}, "e", e_type, {}, entry_point_code);
+        require_goto_statements::require_struct_component_assignment(
+          field, {}, "u", u_type, {}, entry_point_code);
+      };
+
+      THEN(
+        "Object 'example2' has field 'x' of type `Byte`, field `u` of type "
+        "`Character` and a field `e` of type `Integer`.")
+      {
+        has_x_u_e_fields(
+          example2_field,
+          "java::java.lang.Byte",
+          "java::java.lang.Character",
+          "java::java.lang.Integer");
+
+        THEN("`example2` has field `rotate`")
+        {
+          const auto &rotate_field =
+            require_goto_statements::require_struct_component_assignment(
+              example2_field,
+              {},
+              "rotate",
+              "java::Three",
+              {},
+              entry_point_code);
+          has_x_u_e_fields(
+            rotate_field,
+            "java::java.lang.Integer",
+            "java::java.lang.Byte",
+            "java::java.lang.Character");
+
+          THEN("`rotate` has itself a field `rotate` ... ")
+          {
+            const auto &rotate_rec_field =
+              require_goto_statements::require_struct_component_assignment(
+                rotate_field,
+                {},
+                "rotate",
+                "java::Three",
+                {},
+                entry_point_code);
+            has_x_u_e_fields(
+              rotate_rec_field,
+              "java::java.lang.Character",
+              "java::java.lang.Integer",
+              "java::java.lang.Byte");
+          }
+          THEN("`rotate` has also a field `normal` ... ")
+          {
+            const auto &rotate_normal_field =
+              require_goto_statements::require_struct_component_assignment(
+                rotate_field,
+                {},
+                "normal",
+                "java::Three",
+                {},
+                entry_point_code);
+            has_x_u_e_fields(
+              rotate_normal_field,
+              "java::java.lang.Integer",
+              "java::java.lang.Byte",
+              "java::java.lang.Character");
+          }
+        }
+        THEN("`example2` has field `normal`")
+        {
+          const auto &normal_field =
+            require_goto_statements::require_struct_component_assignment(
+              example2_field,
+              {},
+              "normal",
+              "java::Three",
+              {},
+              entry_point_code);
+          has_x_u_e_fields(
+            normal_field,
+            "java::java.lang.Byte",
+            "java::java.lang.Character",
+            "java::java.lang.Integer");
+          THEN("`normal` has itself a field `normal`")
+          {
+            const auto &normal_rec_field =
+              require_goto_statements::require_struct_component_assignment(
+                example2_field,
+                {},
+                "normal",
+                "java::Three",
+                {},
+                entry_point_code);
+            has_x_u_e_fields(
+              normal_rec_field,
+              "java::java.lang.Byte",
+              "java::java.lang.Character",
+              "java::java.lang.Integer");
+          }
+          THEN("`normal` has also a field `rotate`")
+          {
+            const auto &normal_rotate_field =
+              require_goto_statements::require_struct_component_assignment(
+                example2_field,
+                {},
+                "rotate",
+                "java::Three",
+                {},
+                entry_point_code);
+            has_x_u_e_fields(
+              normal_rotate_field,
+              "java::java.lang.Integer",
+              "java::java.lang.Byte",
+              "java::java.lang.Character");
+          }
+        }
+      }
+    }
+    THEN("The Object has a field `example3` of type `Outer<Boolean, Byte>`")
+    {
+      const auto &example3_field =
+        require_goto_statements::require_struct_component_assignment(
+          tmp_object_name, {}, "example3", "java::Outer", {}, entry_point_code);
+
+      has_key_and_value_field(
+        example3_field, "java::java.lang.Boolean", "java::java.lang.Byte");
+
+      THEN("`example3` has a field `inner` of type `Outer.Inner`")
+      {
+        const auto &inner_field =
+          require_goto_statements::require_struct_component_assignment(
+            example3_field,
+            {},
+            "inner",
+            "java::Outer$Inner",
+            {},
+            entry_point_code);
+
+        THEN(
+          "Object 'inner' has field 'key' of type `Outer` with `K` and `V` "
+          "reversed")
+        {
+          const auto &inner_outer_field =
+            require_goto_statements::require_struct_component_assignment(
+              inner_field, {}, "o", "java::Outer", {}, entry_point_code);
+          has_key_and_value_field(
+            inner_outer_field,
+            "java::java.lang.Byte",
+            "java::java.lang.Boolean");
+        }
+      }
+    }
   }
 }