From 736069678405bf03403e1974d6708213ea772243 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 22 May 2018 16:51:25 +0200
Subject: [PATCH 01/15] Use `std::vector` instead of `std::stack`

This makes the generics type tracking information traversable, allows for
push_back / pop_back and provides constant time access to any element.
---
 .../generic_parameter_specialization_map_keys.cpp            | 4 ++--
 .../generic_parameter_specialization_map_keys.h              | 2 +-
 jbmc/src/java_bytecode/select_pointer_type.cpp               | 2 +-
 jbmc/src/java_bytecode/select_pointer_type.h                 | 5 +++--
 4 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
index 18cc04a0918..8666806e040 100644
--- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
+++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
@@ -72,9 +72,9 @@ const void generic_parameter_specialization_map_keyst::insert_pairs(
       const irep_idt &key = pair.first.get_name();
       if(generic_parameter_specialization_map.count(key) == 0)
         generic_parameter_specialization_map.emplace(
-          key, std::stack<reference_typet>());
+          key, std::vector<reference_typet>());
       (*generic_parameter_specialization_map.find(key))
-        .second.push(pair.second);
+        .second.push_back(pair.second);
 
       // We added something, so pop it when this is destroyed:
       erase_keys.push_back(key);
diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
index 9a68dd73d87..737c2164f0a 100644
--- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
+++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
@@ -33,7 +33,7 @@ class generic_parameter_specialization_map_keyst
     for(const auto key : erase_keys)
     {
       PRECONDITION(generic_parameter_specialization_map.count(key) != 0);
-      (*generic_parameter_specialization_map.find(key)).second.pop();
+      (*generic_parameter_specialization_map.find(key)).second.pop_back();
       if((*generic_parameter_specialization_map.find(key)).second.empty())
       {
         generic_parameter_specialization_map.erase(key);
diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index cd0c99505e5..d6c1ceaa692 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -78,7 +78,7 @@ pointer_typet select_pointer_typet::specialize_generics(
       return pointer_type;
     }
     const pointer_typet &type =
-      generic_parameter_specialization_map.find(parameter_name)->second.top();
+      generic_parameter_specialization_map.find(parameter_name)->second.back();
 
     // generic parameters can be adopted from outer classes or superclasses so
     // we may need to search for the concrete type recursively
diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h
index 2f2af2792f1..2e8ed3c2226 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.h
+++ b/jbmc/src/java_bytecode/select_pointer_type.h
@@ -12,11 +12,12 @@
 /// Handle selection of correct pointer type (for example changing abstract
 /// classes to concrete versions).
 
+#include <util/optional.h>
 #include <util/std_types.h>
-#include <stack>
+#include <vector>
 #include "java_types.h"
 
-typedef std::unordered_map<irep_idt, std::stack<reference_typet>>
+typedef std::unordered_map<irep_idt, std::vector<reference_typet>>
   generic_parameter_specialization_mapt;
 
 class namespacet;

From 258e3ae5172abaa9ff9909f28c3b21cf0136ce84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 23 May 2018 09:59:37 +0200
Subject: [PATCH 02/15] Track recursion for generic type parameter definition

---
 .../src/java_bytecode/select_pointer_type.cpp | 19 +++++++++++++++----
 jbmc/src/java_bytecode/select_pointer_type.h  |  4 +++-
 2 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index d6c1ceaa692..65bae89f7d1 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -32,8 +32,9 @@ pointer_typet select_pointer_typet::convert_pointer_type(
   // a generic parameter, specialize it with concrete types
   if(!generic_parameter_specialization_map.empty())
   {
+    generic_parameter_recursion_trackingt visited;
     return specialize_generics(
-      pointer_type, generic_parameter_specialization_map);
+      pointer_type, generic_parameter_specialization_map, visited);
   }
   else
   {
@@ -62,7 +63,8 @@ pointer_typet select_pointer_typet::convert_pointer_type(
 pointer_typet select_pointer_typet::specialize_generics(
   const pointer_typet &pointer_type,
   const generic_parameter_specialization_mapt
-    &generic_parameter_specialization_map) const
+    &generic_parameter_specialization_map,
+  generic_parameter_recursion_trackingt &visited_nodes) const
 {
   if(is_java_generic_parameter(pointer_type))
   {
@@ -80,12 +82,21 @@ pointer_typet select_pointer_typet::specialize_generics(
     const pointer_typet &type =
       generic_parameter_specialization_map.find(parameter_name)->second.back();
 
+    // if we have already seen this before, we will not learn any additional
+    // information from further recursion, only cause a segmentation fault.
+    if(visited_nodes.find(parameter_name) != visited_nodes.end())
+    {
+      throw "no infinite recursion";
+    }
+
+    visited_nodes.insert(parameter_name);
+
     // generic parameters can be adopted from outer classes or superclasses so
     // we may need to search for the concrete type recursively
     return is_java_generic_parameter(type)
              ? specialize_generics(
                  to_java_generic_parameter(type),
-                 generic_parameter_specialization_map)
+                 generic_parameter_specialization_map, visited_nodes)
              : type;
   }
   else if(pointer_type.subtype().id() == ID_symbol)
@@ -99,7 +110,7 @@ pointer_typet select_pointer_typet::specialize_generics(
       {
         const pointer_typet &new_array_type = specialize_generics(
           to_pointer_type(array_element_type),
-          generic_parameter_specialization_map);
+          generic_parameter_specialization_map, visited_nodes);
 
         pointer_typet replacement_array_type = java_array_type('a');
         replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h
index 2e8ed3c2226..fa1c163e8de 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.h
+++ b/jbmc/src/java_bytecode/select_pointer_type.h
@@ -19,6 +19,7 @@
 
 typedef std::unordered_map<irep_idt, std::vector<reference_typet>>
   generic_parameter_specialization_mapt;
+typedef std::set<irep_idt> generic_parameter_recursion_trackingt;
 
 class namespacet;
 
@@ -35,7 +36,8 @@ class select_pointer_typet
   pointer_typet specialize_generics(
     const pointer_typet &pointer_type,
     const generic_parameter_specialization_mapt
-      &generic_parameter_specialization_map) const;
+      &generic_parameter_specialization_map,
+    generic_parameter_recursion_trackingt &) const;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H

From 3264023b9bd85633b27d81058aea9bc4f2c67d9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 25 May 2018 09:54:26 +0200
Subject: [PATCH 03/15] Fix Typo

---
 jbmc/src/java_bytecode/java_object_factory.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index b8ed2371242..5ec5909620b 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -41,7 +41,7 @@ class java_object_factoryt
 
   /// Every time the non-det generator visits a type and the type is generic
   /// (either a struct or a pointer), the following map is used to store and
-  /// look up the concrete types of the generic paramaters in the current
+  /// look up the concrete types of the generic parameters in the current
   /// scope. Note that not all generic parameters need to have a concrete
   /// type, e.g., the method under test is generic. The types are removed
   /// from the map when the scope changes. Note that in different depths

From 31004f50d8ec5f0456db043a91031aeda14e4945 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 25 May 2018 09:54:36 +0200
Subject: [PATCH 04/15] Search through stack for instantiation

---
 .../src/java_bytecode/select_pointer_type.cpp | 116 ++++++++++++++++--
 jbmc/src/java_bytecode/select_pointer_type.h  |   9 ++
 2 files changed, 117 insertions(+), 8 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 65bae89f7d1..6d57f1845c6 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -33,8 +33,10 @@ pointer_typet select_pointer_typet::convert_pointer_type(
   if(!generic_parameter_specialization_map.empty())
   {
     generic_parameter_recursion_trackingt visited;
-    return specialize_generics(
+    auto type = specialize_generics(
       pointer_type, generic_parameter_specialization_map, visited);
+    INVARIANT(visited.empty(), "recursion stack must be empty here");
+    return type;
   }
   else
   {
@@ -86,18 +88,31 @@ pointer_typet select_pointer_typet::specialize_generics(
     // information from further recursion, only cause a segmentation fault.
     if(visited_nodes.find(parameter_name) != visited_nodes.end())
     {
+      optionalt<pointer_typet> result = get_instantiated_type(
+        parameter_name, generic_parameter_specialization_map);
+      if(result.has_value())
+      {
+        return result.value();
+      }
       throw "no infinite recursion";
     }
 
-    visited_nodes.insert(parameter_name);
-
     // generic parameters can be adopted from outer classes or superclasses so
     // we may need to search for the concrete type recursively
-    return is_java_generic_parameter(type)
-             ? specialize_generics(
-                 to_java_generic_parameter(type),
-                 generic_parameter_specialization_map, visited_nodes)
-             : type;
+    if(is_java_generic_parameter(type))
+    {
+      visited_nodes.insert(parameter_name);
+      auto returned_type = specialize_generics(
+        to_java_generic_parameter(type),
+        generic_parameter_specialization_map,
+        visited_nodes);
+      visited_nodes.erase(parameter_name);
+      return returned_type;
+    }
+    else
+    {
+      return type;
+    }
   }
   else if(pointer_type.subtype().id() == ID_symbol)
   {
@@ -120,3 +135,88 @@ pointer_typet select_pointer_typet::specialize_generics(
   }
   return pointer_type;
 }
+
+/// Return the first concrete type instantiation if any such exists.
+/// \param parameter_name The name of the generic parameter type we want to have
+///   instantiated
+/// \param generic_specialization_map Map of type names to specialization stack
+/// \param depth start depth for instantiation search
+/// \return the first instantiated type for the generic type or nothing if no
+/// such instantiation exists.
+optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
+  const irep_idt &parameter_name,
+  const generic_parameter_specialization_mapt
+    &generic_parameter_specialization_map) const
+{
+  generic_parameter_recursion_trackingt visited;
+  const auto retval = get_instantiated_type(
+    parameter_name, generic_parameter_specialization_map, visited, 0);
+  INVARIANT(visited.empty(), "recursion set must be empty here");
+  return retval;
+}
+
+/// See above, the additional parameter just tracks the recursion to prevent
+/// visiting the same depth again.
+/// \param visited tracks the visited parameter names
+optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
+  const irep_idt &parameter_name,
+  const generic_parameter_specialization_mapt
+    &generic_parameter_specialization_map,
+  generic_parameter_recursion_trackingt &visited,
+  const size_t depth) const
+{
+  // Get the pointed to instantiation type at the desired stack depth.
+  // - f this type is not a generic type, it is returned as a valid
+  //   instantiation
+  // - if another recursion at this depth level is found, the search depth is
+  //   increased
+  // - if nothing can be found an empty optional is returned
+
+  if(
+    generic_parameter_specialization_map.find(parameter_name) !=
+    generic_parameter_specialization_map.end())
+  {
+    const auto &replacements =
+      generic_parameter_specialization_map.find(parameter_name)->second;
+
+    // max depth reached and nothing found
+    if(replacements.size() <= depth)
+      return {};
+
+    // Check if there is a recursion loop, if yes increase search depth
+    if(visited.find(parameter_name) != visited.end())
+    {
+      visited.clear();
+      return get_instantiated_type(
+        parameter_name, generic_parameter_specialization_map, visited, depth+1);
+    }
+    else
+    {
+      const size_t index = (replacements.size() - depth) - 1;
+      const auto &type = replacements[index];
+      {
+        if(!is_java_generic_parameter(type))
+        {
+          return type;
+        }
+        else
+        {
+          visited.insert(parameter_name);
+          const auto &gen_type = to_java_generic_parameter(type).type_variable();
+          const auto val = get_instantiated_type(
+            gen_type.get_identifier(),
+            generic_parameter_specialization_map,
+            visited,
+            depth);
+          visited.erase(parameter_name);
+          return val;
+        }
+      }
+    }
+  }
+  // parameter_name not found in map
+  else
+  {
+    UNREACHABLE;
+  }
+}
diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h
index fa1c163e8de..a77b5c36738 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.h
+++ b/jbmc/src/java_bytecode/select_pointer_type.h
@@ -25,6 +25,15 @@ class namespacet;
 
 class select_pointer_typet
 {
+  optionalt<pointer_typet> get_instantiated_type(
+    const irep_idt &,
+    const generic_parameter_specialization_mapt &,
+    generic_parameter_recursion_trackingt &,
+    const size_t) const;
+  optionalt<pointer_typet> get_instantiated_type(
+    const irep_idt &parameter_name,
+    const generic_parameter_specialization_mapt &) const;
+
 public:
   virtual ~select_pointer_typet() = default;
   virtual pointer_typet convert_pointer_type(

From 6ff2993fab6be32fae98dcc8fecd595ced0af9b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 25 May 2018 20:31:36 +0200
Subject: [PATCH 05/15] Choose mapped-to type when doing higher depth search

---
 .../src/java_bytecode/select_pointer_type.cpp | 46 ++++++++++++++-----
 jbmc/src/java_bytecode/select_pointer_type.h  |  4 +-
 2 files changed, 37 insertions(+), 13 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 6d57f1845c6..3a6ab1e086a 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -125,7 +125,8 @@ pointer_typet select_pointer_typet::specialize_generics(
       {
         const pointer_typet &new_array_type = specialize_generics(
           to_pointer_type(array_element_type),
-          generic_parameter_specialization_map, visited_nodes);
+          generic_parameter_specialization_map,
+          visited_nodes);
 
         pointer_typet replacement_array_type = java_array_type('a');
         replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
@@ -149,10 +150,34 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
     &generic_parameter_specialization_map) const
 {
   generic_parameter_recursion_trackingt visited;
-  const auto retval = get_instantiated_type(
-    parameter_name, generic_parameter_specialization_map, visited, 0);
-  INVARIANT(visited.empty(), "recursion set must be empty here");
-  return retval;
+  size_t depth = 0;
+  const size_t max =
+    generic_parameter_specialization_map.find(parameter_name)->second.size();
+
+  irep_idt current_parameter = parameter_name;
+  while(depth < max)
+  {
+    const auto retval = get_instantiated_type(
+      current_parameter, generic_parameter_specialization_map, visited, depth);
+    if(retval.has_value())
+    {
+      if(is_java_generic_parameter(*retval))
+      {
+        UNREACHABLE;
+      }
+      return retval;
+    }
+    INVARIANT(visited.empty(), "recursion set must be empty here");
+
+    const auto &entry =
+      generic_parameter_specialization_map.find(current_parameter)
+        ->second.back();
+    const java_generic_parametert &gen_param = to_java_generic_parameter(entry);
+    const auto &type_var = gen_param.type_variable();
+    current_parameter = type_var.get_identifier();
+    depth++;
+  }
+  return {};
 }
 
 /// See above, the additional parameter just tracks the recursion to prevent
@@ -179,16 +204,14 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
     const auto &replacements =
       generic_parameter_specialization_map.find(parameter_name)->second;
 
-    // max depth reached and nothing found
+    // max depth reached and nothing found, TODO return bound
     if(replacements.size() <= depth)
       return {};
 
-    // Check if there is a recursion loop, if yes increase search depth
+    // Check if there is a recursion loop, if yes return with nothing found
     if(visited.find(parameter_name) != visited.end())
     {
-      visited.clear();
-      return get_instantiated_type(
-        parameter_name, generic_parameter_specialization_map, visited, depth+1);
+      return {};
     }
     else
     {
@@ -202,7 +225,8 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
         else
         {
           visited.insert(parameter_name);
-          const auto &gen_type = to_java_generic_parameter(type).type_variable();
+          const auto &gen_type =
+            to_java_generic_parameter(type).type_variable();
           const auto val = get_instantiated_type(
             gen_type.get_identifier(),
             generic_parameter_specialization_map,
diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h
index a77b5c36738..85b52e3a4f1 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.h
+++ b/jbmc/src/java_bytecode/select_pointer_type.h
@@ -11,11 +11,11 @@
 /// \file
 /// Handle selection of correct pointer type (for example changing abstract
 /// classes to concrete versions).
+#include <vector>
 
+#include "java_types.h"
 #include <util/optional.h>
 #include <util/std_types.h>
-#include <vector>
-#include "java_types.h"
 
 typedef std::unordered_map<irep_idt, std::vector<reference_typet>>
   generic_parameter_specialization_mapt;

From 26e5433bf560c7bd11ea0186be74069a2e7fbc36 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 25 May 2018 20:32:39 +0200
Subject: [PATCH 06/15] Add unit test for mutually recursive generic parameters

---
 jbmc/unit/Makefile                            |   1 +
 .../goto_program_generics/KeyValue.class      | Bin 0 -> 562 bytes
 .../MutuallyRecursiveGenerics.class           | Bin 0 -> 671 bytes
 .../MutuallyRecursiveGenerics.java            |  29 ++
 .../goto_program_generics/Outer$Inner.class   | Bin 0 -> 613 bytes
 .../goto_program_generics/Outer.class         | Bin 0 -> 634 bytes
 .../goto_program_generics/Three.class         | Bin 0 -> 597 bytes
 .../mutually_recursive_generics.cpp           | 278 ++++++++++++++++++
 8 files changed, 308 insertions(+)
 create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class
 create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class
 create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java
 create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class
 create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/Outer.class
 create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/Three.class
 create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
index 16da78dcda2..0b6df177183 100644
--- a/jbmc/unit/Makefile
+++ b/jbmc/unit/Makefile
@@ -32,6 +32,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        util/simplify_expr.cpp \
        java_bytecode/java_virtual_functions/virtual_functions.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
+       java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class b/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class
new file mode 100644
index 0000000000000000000000000000000000000000..d093b9493294bc8edb2cfcbce204f3f5dd9dd7a0
GIT binary patch
literal 562
zcmZut%TB^T6g|VMfG7_YpD`}gg=}2ehQyfY0@OrE_d}iFU@d0aY3ygYGI8Mt_)*3?
zRZzgi+_~p5Id|^I=i57g6YQ3e#g>I_3p)(CKs-kb<!(nLF88&t8A?4l40xoKU}#JQ
zr{A&ruH7bsr9>=LI48R{IgFfr5Q%v?;xTXeJQ%ia1|#7`Mj{JCJ~l}Pxr7Ri3}n<M
zcyQ>_MCao>(yCn<h->{g5US4yewsD*xbJc$4gMi>(Y*{An%x;Kd79{s(>Yxn#QleB
zFWP7?y|GrFxR7Rmy(=AQ?)%BD@U#kLEG|VLl=Q-5^VJHfs4)~Ln`EfXZvgwq(Ds2`
zdh(#(Q<s57wTNF_B3#DORId<T{)1OYfytx0PTd*ZhRGkjg1u0aMT2S~CF@wFzVdCr
U8pQzXGmMGP{EX7XMv6AS0MT}KTL1t6

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class
new file mode 100644
index 0000000000000000000000000000000000000000..ed2b36215260644dd843a70e930ff028a7701c03
GIT binary patch
literal 671
zcmah`+b%;v6kWTjr7m@^BI3~{(YU-72~CJNNL2bhJ+^k_I7g;)L_f=u#Dfp;QDRS3
z9Yj3L?6vl+wdVHv_WS~18}m8zVK$3m7ITCFeo(h}0dEj;-U+vBDu}sE7_90>sBCPQ
zu+dxC@ov<;Dg`QRl&aR~uu)EQjzh~0Hsw9>f97ryvfgFWunXP)K*^MYw&i3-rKyba
zt)%=Dyyb$=W2YqSexPr`Q53KWlQBQ{sx~8IJEzU;=uq1|Lf`UAjgYQHS90&Xr$auA
zZ|iI>RXvc-gctcLs41fz?>5u6sau43?=-ft3WD|p`>|>1dp_cjjrLn|Lb{d*u12x(
z`B1y4#Xr^S?u~~riaeqCr;0H4^%v*$8}==hkdnVeXQa^&LPl5$S(yhg*yB0jLm2My
z5z)YHD4j7uC8;E}fAtCUC?JJ#nKPYc0TY6qSp=BGlvH54XI>NL)_xfm5=QD82{R&1
Gq3{mTPo1#<

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java
new file mode 100644
index 00000000000..55dea15389b
--- /dev/null
+++ b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java
@@ -0,0 +1,29 @@
+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;
+    K key;
+    V value;
+}
+class MutuallyRecursiveGenerics {
+  KeyValue<String, Integer> example1;
+  Three<Byte, Character, Integer> example2;
+  Outer<Boolean, Byte, Short> example3;
+  void f() {
+  }
+}
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class b/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class
new file mode 100644
index 0000000000000000000000000000000000000000..136c195e97df665129f992026280d4aea55b80a8
GIT binary patch
literal 613
zcmZWm$w~u35PhA=V#bNaxbF)dVg&Wz$%I@4MT`p?bMK6ewu}>*Mewsch~U8w@T0`n
zohYb>uCA(n{i<Ho$LHHSfL*K=;b7iH77GO|6|gKIdIE*kS(>P*E>OJGH=#_@NC{N>
z*+#olZy(p&SM??VA~g?p@=<OFGQ8P7>)t6p;e$hfKt8$E@%j#(h7NVo6mY8p@{Nu_
zcE5K`=Fyf8)oFU)RZ&}Z16!--%b+78ZQ?;PYsdt0M`5TU0ngt1fsA9tbg9p~ZnG>s
z)%r#8^zcoy_^pE?D1|z<?4QO!Qnhil_g_)-e~Mx*duimW18sU<I!TjM2Eo&X^3y2R
zkLpmdQSHZDW<DM~<UN$IQoyRfupM!~TY>W5337l{GohS?VTF6ja%B!r4ta1#^fDNt
zEyDeYhs$MChFQT=!U*qCdgsJuc)PXD7l_&`GS7@0lxYo{;Tofz>Z4G>BqQQ28;42X
bvpAP;(~O)!2Q!#ul))S(ES`;H5#zuYx5R&B

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Outer.class b/jbmc/unit/java_bytecode/goto_program_generics/Outer.class
new file mode 100644
index 0000000000000000000000000000000000000000..06ce8540988ea668829886e8c54486766aeb9a6f
GIT binary patch
literal 634
zcmZuu$xZ@65Pi*vqb#DRxPlx!s0X=tk_m|+(HL-vBKKzOVB<KLSxERSPbMDx06)t3
zW<aCDp}Xq6dbOnL<MZtuz!AzR7}z#ZG*L3KBal3IUF8X6Vq15l?<=3Q9?{w6RTwC5
zH;z^X=5KY^l|kq!f#N7;wHnn{yV|;|)(&Ht6}i+Jk7_88Z}#LsRvhVeD_5PKvV$nZ
z95xw9CuAXm=>oHsc6CrA+}m#p%+&k$jOCizRhQvYM|myTameJGeOo$h>FEfM$(i6m
zb8K@o5~~&ds)o<s%KXICR9{<-<H<SOQ@Fb+Tx~K{Aa&ahJzJgXXy(#I7=+SshBwL%
zJzo#hnc~{D?H@+l$zTyn+(*1?fyMtD6G;C$1IkG7iin?yIq)n*38eU^k@>+{;)P#0
z#|WZUw0U|bv=Ng$c!hYOV_=#8Y)lHQ(2t5yfK?P|*Zwf;M8>%F1~!Qj*kU#~2=7Of
G1ik>0+>9Ck

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Three.class b/jbmc/unit/java_bytecode/goto_program_generics/Three.class
new file mode 100644
index 0000000000000000000000000000000000000000..3921f56904040ddb6fe635f50d0223fb88357d6e
GIT binary patch
literal 597
zcmZuu%TB^T6g|VENJT+Zd=r=ILN=}}Au$Hs;3HB9+o4WiNNLT`68S7wCNBH{KgxKg
zpee$lcg}0>+}wVBe|!SCK-okR2N@h@aKvCJKj492$TaM}62fB0Hf7J_L8wSAPSvX2
zvh0p!*R2`_49{0X?#A56qKtOgt2PFF%quSUdX<OnKsW&zN$Nm0bxl$uLZL=2LPk}3
zGN=(fIc+nfuKj09<r~ry_u;TBl+C+tG>z|Yx6PH*d?u!Xz8o=>8gt&{<=20#b}kpk
zsV~u5OSIbJRR*)^hsqH*QV&(W3xklm?&L{0p&H4txD}pI(ixrWCFHPyB11abE<@q}
zVsMNE{SY8cUy3TNgHQq)sw**`C2nH%&(9HGi}7{h`4}%y68dpEHwj(Qsg?BEJJ=h6
fB(|s;k!WI@aBdnvDH>*HPSMXNW~1$5FJk*Y0#kYS

literal 0
HcmV?d00001

diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
new file mode 100644
index 00000000000..e11a40e996e
--- /dev/null
+++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
@@ -0,0 +1,278 @@
+/*******************************************************************\
+
+ Module: Unit tests for parsing mutually generic classes
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <java-testing-utils/load_java_class.h>
+#include <java-testing-utils/require_goto_statements.h>
+#include <java-testing-utils/require_type.h>
+#include <testing-utils/catch.hpp>
+
+SCENARIO(
+  "Generics class with mutually recursive_generic parameters",
+  "[core][java_bytecode][goto_programs_generics]")
+{
+  const symbol_tablet &symbol_table = load_java_class(
+    "MutuallyRecursiveGenerics",
+    "./java_bytecode/goto_program_generics",
+    "MutuallyRecursiveGenerics.f");
+
+  std::string class_prefix = "java::MutuallyRecursiveGenerics";
+
+  REQUIRE(symbol_table.has_symbol(class_prefix));
+
+  WHEN(
+    "parsing class which has generic type parameters and two field with those"
+    "parameters in use")
+  {
+    const auto &root = symbol_table.lookup_ref(class_prefix);
+    const typet &type = root.type;
+    REQUIRE(type.id() == ID_struct);
+
+    // needs an `example1` local variable ...
+    const struct_union_typet::componentt &example1 =
+      require_type::require_component(to_struct_type(type), "example1");
+
+    // ... which is generic and has two explicit generic parameter
+    // instantiations, String and Integer ...
+    const java_generic_typet &gen_type =
+      require_type::require_java_generic_type(
+        example1.type(),
+        {{require_type::type_argument_kindt::Inst, "java::java.lang.String"},
+         {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});
+
+    // ... which is of type `KeyValue` ...
+    const auto &subtype = gen_type.subtype();
+    const auto &key_value =
+      symbol_table.lookup_ref(to_symbol_type(subtype).get_identifier());
+    REQUIRE(key_value.type.id() == ID_struct);
+    REQUIRE(key_value.name == "java::KeyValue");
+
+    // ... and contains two local variables of type `KeyValue` ...
+    const auto &next =
+      require_type::require_component(to_struct_type(key_value.type), "next");
+    const auto &reverse = require_type::require_component(
+      to_struct_type(key_value.type), "reverse");
+
+    // ... where `next` has the same generic parameter instantiations ...
+    const java_generic_typet &next_type =
+      require_type::require_java_generic_type(
+        next.type(),
+        {{require_type::type_argument_kindt::Var, "java::KeyValue::K"},
+         {require_type::type_argument_kindt::Var, "java::KeyValue::V"}});
+    REQUIRE(next_type.subtype().id() == ID_symbol);
+    const symbol_typet &next_symbol = to_symbol_type(next_type.subtype());
+    REQUIRE(
+      symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
+      "java::KeyValue");
+
+    // ... and `reverse` has the same but in reversed order
+    const java_generic_typet &reverse_type =
+      require_type::require_java_generic_type(
+        reverse.type(),
+        {{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
+         {require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
+    REQUIRE(next_type.subtype().id() == ID_symbol);
+    const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype());
+    REQUIRE(
+      symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
+      "java::KeyValue");
+  }
+  WHEN("The class of type `MutuallyRecursiveGenerics` is created")
+  {
+    const std::vector<codet> &entry_point_code =
+      require_goto_statements::require_entry_point_statements(symbol_table);
+
+    auto has_key_and_value_field = [&](
+      const irep_idt &field,
+      const irep_idt &key_type,
+      const irep_idt &val_type) {
+      require_goto_statements::require_struct_component_assignment(
+        field, {}, "key", key_type, {}, entry_point_code);
+      require_goto_statements::require_struct_component_assignment(
+        field, {}, "value", val_type, {}, entry_point_code);
+    };
+
+    const irep_idt &tmp_object_name =
+      require_goto_statements::require_entry_point_argument_assignment(
+        "this", entry_point_code);
+
+    THEN(
+      "The Object has a field `example1` of type `KeyValue<String, Integer>`")
+    {
+      const auto &example1_field =
+        require_goto_statements::require_struct_component_assignment(
+          tmp_object_name,
+          {},
+          "example1",
+          "java::KeyValue",
+          {},
+          entry_point_code);
+
+      THEN(
+        "Object 'example1' has field 'key' of type `String` and field `value` "
+        "of type `Integer`")
+      {
+        has_key_and_value_field(
+          example1_field, "java::java.lang.String", "java::java.lang.Integer");
+      }
+
+      THEN("`example1` has field next")
+      {
+        const auto &next_field =
+          require_goto_statements::require_struct_component_assignment(
+            example1_field, {}, "next", "java::KeyValue", {}, entry_point_code);
+        has_key_and_value_field(
+          next_field, "java::java.lang.String", "java::java.lang.Integer");
+      }
+      THEN("`example1` has field `reverse`")
+      {
+        const auto &reverse_field =
+          require_goto_statements::require_struct_component_assignment(
+            example1_field,
+            {},
+            "reverse",
+            "java::KeyValue",
+            {},
+            entry_point_code);
+        has_key_and_value_field(
+          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");
+          }
+        }
+      }
+    }
+  }
+
+  // TODO: add test for TG-3828
+}

From 2c5e0b8393200e8aecf4d2dbcc24e938de1bfb6a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 29 May 2018 14:23:19 +0200
Subject: [PATCH 07/15] Return bound if no concrete instantiation is found

---
 jbmc/src/java_bytecode/select_pointer_type.cpp | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 3a6ab1e086a..9b0d37f005d 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -94,7 +94,11 @@ pointer_typet select_pointer_typet::specialize_generics(
       {
         return result.value();
       }
-      throw "no infinite recursion";
+      else
+      {
+        // return pointer type of generic parameter bound
+        return java_reference_type(parameter.subtype());
+      }
     }
 
     // generic parameters can be adopted from outer classes or superclasses so
@@ -204,9 +208,8 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
     const auto &replacements =
       generic_parameter_specialization_map.find(parameter_name)->second;
 
-    // max depth reached and nothing found, TODO return bound
-    if(replacements.size() <= depth)
-      return {};
+    INVARIANT(
+      depth < replacements.size(), "cannot access elements outside stack");
 
     // Check if there is a recursion loop, if yes return with nothing found
     if(visited.find(parameter_name) != visited.end())

From 05ff12d1b154ec27a188338a093ff436c6c64869 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 29 May 2018 14:45:26 +0200
Subject: [PATCH 08/15] Clarifications and corrections

---
 ...eneric_parameter_specialization_map_keys.h |   5 +-
 .../src/java_bytecode/select_pointer_type.cpp | 114 ++++++++----------
 2 files changed, 50 insertions(+), 69 deletions(-)

diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
index 737c2164f0a..47ed3ade15d 100644
--- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
+++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
@@ -33,8 +33,9 @@ class generic_parameter_specialization_map_keyst
     for(const auto key : erase_keys)
     {
       PRECONDITION(generic_parameter_specialization_map.count(key) != 0);
-      (*generic_parameter_specialization_map.find(key)).second.pop_back();
-      if((*generic_parameter_specialization_map.find(key)).second.empty())
+      auto &val = generic_parameter_specialization_map.find(key)->second;
+      val.pop_back();
+      if(val.empty())
       {
         generic_parameter_specialization_map.erase(key);
       }
diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 9b0d37f005d..903c36895d5 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -33,7 +33,7 @@ pointer_typet select_pointer_typet::convert_pointer_type(
   if(!generic_parameter_specialization_map.empty())
   {
     generic_parameter_recursion_trackingt visited;
-    auto type = specialize_generics(
+    const auto &type = specialize_generics(
       pointer_type, generic_parameter_specialization_map, visited);
     INVARIANT(visited.empty(), "recursion stack must be empty here");
     return type;
@@ -84,8 +84,7 @@ pointer_typet select_pointer_typet::specialize_generics(
     const pointer_typet &type =
       generic_parameter_specialization_map.find(parameter_name)->second.back();
 
-    // if we have already seen this before, we will not learn any additional
-    // information from further recursion, only cause a segmentation fault.
+    // avoid infinite recursion
     if(visited_nodes.find(parameter_name) != visited_nodes.end())
     {
       optionalt<pointer_typet> result = get_instantiated_type(
@@ -103,20 +102,16 @@ pointer_typet select_pointer_typet::specialize_generics(
 
     // generic parameters can be adopted from outer classes or superclasses so
     // we may need to search for the concrete type recursively
-    if(is_java_generic_parameter(type))
-    {
-      visited_nodes.insert(parameter_name);
-      auto returned_type = specialize_generics(
-        to_java_generic_parameter(type),
-        generic_parameter_specialization_map,
-        visited_nodes);
-      visited_nodes.erase(parameter_name);
-      return returned_type;
-    }
-    else
-    {
+    if(!is_java_generic_parameter(type))
       return type;
-    }
+
+    visited_nodes.insert(parameter_name);
+    auto returned_type = specialize_generics(
+      to_java_generic_parameter(type),
+      generic_parameter_specialization_map,
+      visited_nodes);
+    visited_nodes.erase(parameter_name);
+    return returned_type;
   }
   else if(pointer_type.subtype().id() == ID_symbol)
   {
@@ -165,13 +160,10 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
       current_parameter, generic_parameter_specialization_map, visited, depth);
     if(retval.has_value())
     {
-      if(is_java_generic_parameter(*retval))
-      {
-        UNREACHABLE;
-      }
+      CHECK_RETURN(!is_java_generic_parameter(*retval));
       return retval;
     }
-    INVARIANT(visited.empty(), "recursion set must be empty here");
+    CHECK_RETURN(visited.empty());
 
     const auto &entry =
       generic_parameter_specialization_map.find(current_parameter)
@@ -184,9 +176,11 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
   return {};
 }
 
-/// See above, the additional parameter just tracks the recursion to prevent
-/// visiting the same depth again.
+/// See get_instantiated_type, the additional parameters just track the
+/// recursion to prevent, visiting the same depth again and specify which stack
+/// depth is analyzed.
 /// \param visited tracks the visited parameter names
+/// \param depth stack depth to analyze
 optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
   const irep_idt &parameter_name,
   const generic_parameter_specialization_mapt
@@ -195,55 +189,41 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
   const size_t depth) const
 {
   // Get the pointed to instantiation type at the desired stack depth.
-  // - f this type is not a generic type, it is returned as a valid
+  // - if this type is not a generic type, it is returned as a valid
   //   instantiation
-  // - if another recursion at this depth level is found, the search depth is
-  //   increased
-  // - if nothing can be found an empty optional is returned
+  // - if nothing can be found at the given depth, an empty optional is returned
 
-  if(
-    generic_parameter_specialization_map.find(parameter_name) !=
-    generic_parameter_specialization_map.end())
-  {
-    const auto &replacements =
-      generic_parameter_specialization_map.find(parameter_name)->second;
+  auto val = generic_parameter_specialization_map.find(parameter_name);
+  INVARIANT(
+    val != generic_parameter_specialization_map.end(),
+    "generic parameter must be a key in map");
 
-    INVARIANT(
-      depth < replacements.size(), "cannot access elements outside stack");
+  const auto &replacements = val->second;
 
-    // Check if there is a recursion loop, if yes return with nothing found
-    if(visited.find(parameter_name) != visited.end())
-    {
-      return {};
-    }
-    else
-    {
-      const size_t index = (replacements.size() - depth) - 1;
-      const auto &type = replacements[index];
-      {
-        if(!is_java_generic_parameter(type))
-        {
-          return type;
-        }
-        else
-        {
-          visited.insert(parameter_name);
-          const auto &gen_type =
-            to_java_generic_parameter(type).type_variable();
-          const auto val = get_instantiated_type(
-            gen_type.get_identifier(),
-            generic_parameter_specialization_map,
-            visited,
-            depth);
-          visited.erase(parameter_name);
-          return val;
-        }
-      }
-    }
+  INVARIANT(
+    depth < replacements.size(), "cannot access elements outside stack");
+
+  // Check if there is a recursion loop, if yes return with nothing found
+  if(visited.find(parameter_name) != visited.end())
+  {
+    return {};
   }
-  // parameter_name not found in map
-  else
+
+  const size_t index = (replacements.size() - depth) - 1;
+  const auto &type = replacements[index];
+
+  if(!is_java_generic_parameter(type))
   {
-    UNREACHABLE;
+    return type;
   }
+
+  visited.insert(parameter_name);
+  const auto &gen_type = to_java_generic_parameter(type).type_variable();
+  const auto inst_val = get_instantiated_type(
+    gen_type.get_identifier(),
+    generic_parameter_specialization_map,
+    visited,
+    depth);
+  visited.erase(parameter_name);
+  return inst_val;
 }

From 8b4920e066ebea0f9576eadf4ceb373b736c2274 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 29 May 2018 18:06:42 +0200
Subject: [PATCH 09/15] Return input pointer_type in case of no instantiation

---
 jbmc/src/java_bytecode/select_pointer_type.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 903c36895d5..97fe0dd62e1 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -96,7 +96,7 @@ pointer_typet select_pointer_typet::specialize_generics(
       else
       {
         // return pointer type of generic parameter bound
-        return java_reference_type(parameter.subtype());
+        return pointer_type;
       }
     }
 

From b0fde14a115cc7225479897012d723bcc5e3e08d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 29 May 2018 18:19:00 +0200
Subject: [PATCH 10/15] Doxygen update, clarification

---
 jbmc/src/java_bytecode/select_pointer_type.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 97fe0dd62e1..6d916fbc68d 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -136,12 +136,13 @@ pointer_typet select_pointer_typet::specialize_generics(
   return pointer_type;
 }
 
-/// Return the first concrete type instantiation if any such exists.
+/// Return the first concrete type instantiation if any such exists. This method
+/// is only to be called when the `specialize_generics` cannot find an
+/// instantiation due to a loop in its recursion.
 /// \param parameter_name The name of the generic parameter type we want to have
 ///   instantiated
 /// \param generic_specialization_map Map of type names to specialization stack
-/// \param depth start depth for instantiation search
-/// \return the first instantiated type for the generic type or nothing if no
+/// \return The first instantiated type for the generic type or nothing if no
 /// such instantiation exists.
 optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
   const irep_idt &parameter_name,
@@ -179,8 +180,8 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
 /// See get_instantiated_type, the additional parameters just track the
 /// recursion to prevent, visiting the same depth again and specify which stack
 /// depth is analyzed.
-/// \param visited tracks the visited parameter names
-/// \param depth stack depth to analyze
+/// \param visited Tracks the visited parameter names
+/// \param depth Stack depth to analyze
 optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
   const irep_idt &parameter_name,
   const generic_parameter_specialization_mapt

From f6586ed1ad07425de50d5eee2083bae57a2e593d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 29 May 2018 18:31:26 +0200
Subject: [PATCH 11/15] Rename functions to `get_recursively_instantiated_type`

---
 jbmc/src/java_bytecode/select_pointer_type.cpp | 18 ++++++++++--------
 jbmc/src/java_bytecode/select_pointer_type.h   |  4 ++--
 2 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 6d916fbc68d..1e05289995a 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -87,7 +87,7 @@ pointer_typet select_pointer_typet::specialize_generics(
     // avoid infinite recursion
     if(visited_nodes.find(parameter_name) != visited_nodes.end())
     {
-      optionalt<pointer_typet> result = get_instantiated_type(
+      optionalt<pointer_typet> result = get_recursively_instantiated_type(
         parameter_name, generic_parameter_specialization_map);
       if(result.has_value())
       {
@@ -144,7 +144,8 @@ pointer_typet select_pointer_typet::specialize_generics(
 /// \param generic_specialization_map Map of type names to specialization stack
 /// \return The first instantiated type for the generic type or nothing if no
 /// such instantiation exists.
-optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
+optionalt<pointer_typet>
+select_pointer_typet::get_recursively_instantiated_type(
   const irep_idt &parameter_name,
   const generic_parameter_specialization_mapt
     &generic_parameter_specialization_map) const
@@ -157,7 +158,7 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
   irep_idt current_parameter = parameter_name;
   while(depth < max)
   {
-    const auto retval = get_instantiated_type(
+    const auto retval = get_recursively_instantiated_type(
       current_parameter, generic_parameter_specialization_map, visited, depth);
     if(retval.has_value())
     {
@@ -177,12 +178,13 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
   return {};
 }
 
-/// See get_instantiated_type, the additional parameters just track the
-/// recursion to prevent, visiting the same depth again and specify which stack
-/// depth is analyzed.
+/// See get_recursively instantiated_type, the additional parameters just track
+/// the recursion to prevent, visiting the same depth again and specify which
+/// stack depth is analyzed.
 /// \param visited Tracks the visited parameter names
 /// \param depth Stack depth to analyze
-optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
+optionalt<pointer_typet>
+select_pointer_typet::get_recursively_instantiated_type(
   const irep_idt &parameter_name,
   const generic_parameter_specialization_mapt
     &generic_parameter_specialization_map,
@@ -220,7 +222,7 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
 
   visited.insert(parameter_name);
   const auto &gen_type = to_java_generic_parameter(type).type_variable();
-  const auto inst_val = get_instantiated_type(
+  const auto inst_val = get_recursively_instantiated_type(
     gen_type.get_identifier(),
     generic_parameter_specialization_map,
     visited,
diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h
index 85b52e3a4f1..3f9cc18f82d 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.h
+++ b/jbmc/src/java_bytecode/select_pointer_type.h
@@ -25,12 +25,12 @@ class namespacet;
 
 class select_pointer_typet
 {
-  optionalt<pointer_typet> get_instantiated_type(
+  optionalt<pointer_typet> get_recursively_instantiated_type(
     const irep_idt &,
     const generic_parameter_specialization_mapt &,
     generic_parameter_recursion_trackingt &,
     const size_t) const;
-  optionalt<pointer_typet> get_instantiated_type(
+  optionalt<pointer_typet> get_recursively_instantiated_type(
     const irep_idt &parameter_name,
     const generic_parameter_specialization_mapt &) const;
 

From 43b41a4f913fa2d776673c076e0998f15d80e941 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 29 May 2018 18:33:15 +0200
Subject: [PATCH 12/15] Simplify return

---
 jbmc/src/java_bytecode/select_pointer_type.cpp | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 1e05289995a..e335b82db8b 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -89,15 +89,7 @@ pointer_typet select_pointer_typet::specialize_generics(
     {
       optionalt<pointer_typet> result = get_recursively_instantiated_type(
         parameter_name, generic_parameter_specialization_map);
-      if(result.has_value())
-      {
-        return result.value();
-      }
-      else
-      {
-        // return pointer type of generic parameter bound
-        return pointer_type;
-      }
+      return result.has_value() ? result.value() : pointer_type;
     }
 
     // generic parameters can be adopted from outer classes or superclasses so

From 2d9970c3d551c4ecdd587a9d96d8404bd63aadfa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 5 Jun 2018 14:22:43 +0200
Subject: [PATCH 13/15] Clarify and correct

---
 ...eneric_parameter_specialization_map_keys.h |  2 -
 .../src/java_bytecode/select_pointer_type.cpp | 49 +++++++++----------
 jbmc/src/java_bytecode/select_pointer_type.h  |  4 +-
 .../mutually_recursive_generics.cpp           | 20 ++++----
 4 files changed, 34 insertions(+), 41 deletions(-)

diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
index 47ed3ade15d..36f0efb2afb 100644
--- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
+++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
@@ -36,9 +36,7 @@ class generic_parameter_specialization_map_keyst
       auto &val = generic_parameter_specialization_map.find(key)->second;
       val.pop_back();
       if(val.empty())
-      {
         generic_parameter_specialization_map.erase(key);
-      }
     }
   }
 
diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index e335b82db8b..af24baaad3a 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -73,6 +73,16 @@ pointer_typet select_pointer_typet::specialize_generics(
     const java_generic_parametert &parameter =
       to_java_generic_parameter(pointer_type);
     const irep_idt &parameter_name = parameter.get_name();
+
+    // avoid infinite recursion by looking at each generic argument from
+    // previous assignments
+    if(visited_nodes.find(parameter_name) != visited_nodes.end())
+    {
+      const optionalt<pointer_typet> result = get_recursively_instantiated_type(
+        parameter_name, generic_parameter_specialization_map);
+      return result.has_value() ? result.value() : pointer_type;
+    }
+
     if(generic_parameter_specialization_map.count(parameter_name) == 0)
     {
       // this means that the generic pointer_type has not been specialized
@@ -84,21 +94,13 @@ pointer_typet select_pointer_typet::specialize_generics(
     const pointer_typet &type =
       generic_parameter_specialization_map.find(parameter_name)->second.back();
 
-    // avoid infinite recursion
-    if(visited_nodes.find(parameter_name) != visited_nodes.end())
-    {
-      optionalt<pointer_typet> result = get_recursively_instantiated_type(
-        parameter_name, generic_parameter_specialization_map);
-      return result.has_value() ? result.value() : pointer_type;
-    }
-
     // generic parameters can be adopted from outer classes or superclasses so
     // we may need to search for the concrete type recursively
     if(!is_java_generic_parameter(type))
       return type;
 
     visited_nodes.insert(parameter_name);
-    auto returned_type = specialize_generics(
+    const auto returned_type = specialize_generics(
       to_java_generic_parameter(type),
       generic_parameter_specialization_map,
       visited_nodes);
@@ -135,7 +137,7 @@ pointer_typet select_pointer_typet::specialize_generics(
 ///   instantiated
 /// \param generic_specialization_map Map of type names to specialization stack
 /// \return The first instantiated type for the generic type or nothing if no
-/// such instantiation exists.
+///   such instantiation exists.
 optionalt<pointer_typet>
 select_pointer_typet::get_recursively_instantiated_type(
   const irep_idt &parameter_name,
@@ -143,12 +145,11 @@ select_pointer_typet::get_recursively_instantiated_type(
     &generic_parameter_specialization_map) const
 {
   generic_parameter_recursion_trackingt visited;
-  size_t depth = 0;
-  const size_t max =
+  const size_t max_depth =
     generic_parameter_specialization_map.find(parameter_name)->second.size();
 
   irep_idt current_parameter = parameter_name;
-  while(depth < max)
+  for(size_t depth = 0; depth < max_depth; depth++)
   {
     const auto retval = get_recursively_instantiated_type(
       current_parameter, generic_parameter_specialization_map, visited, depth);
@@ -162,19 +163,19 @@ select_pointer_typet::get_recursively_instantiated_type(
     const auto &entry =
       generic_parameter_specialization_map.find(current_parameter)
         ->second.back();
-    const java_generic_parametert &gen_param = to_java_generic_parameter(entry);
-    const auto &type_var = gen_param.type_variable();
-    current_parameter = type_var.get_identifier();
-    depth++;
+    current_parameter = to_java_generic_parameter(entry).get_name();
   }
   return {};
 }
 
 /// See get_recursively instantiated_type, the additional parameters just track
-/// the recursion to prevent, visiting the same depth again and specify which
+/// the recursion to prevent visiting the same depth again and specify which
 /// stack depth is analyzed.
 /// \param visited Tracks the visited parameter names
 /// \param depth Stack depth to analyze
+/// \return if this type is not a generic type, it is returned as a valid
+///   instantiation, if nothing can be found at the given depth, en empty optional
+///   is returned
 optionalt<pointer_typet>
 select_pointer_typet::get_recursively_instantiated_type(
   const irep_idt &parameter_name,
@@ -183,12 +184,7 @@ select_pointer_typet::get_recursively_instantiated_type(
   generic_parameter_recursion_trackingt &visited,
   const size_t depth) const
 {
-  // Get the pointed to instantiation type at the desired stack depth.
-  // - if this type is not a generic type, it is returned as a valid
-  //   instantiation
-  // - if nothing can be found at the given depth, an empty optional is returned
-
-  auto val = generic_parameter_specialization_map.find(parameter_name);
+  const auto &val = generic_parameter_specialization_map.find(parameter_name);
   INVARIANT(
     val != generic_parameter_specialization_map.end(),
     "generic parameter must be a key in map");
@@ -204,7 +200,7 @@ select_pointer_typet::get_recursively_instantiated_type(
     return {};
   }
 
-  const size_t index = (replacements.size() - depth) - 1;
+  const size_t index = (replacements.size() - 1) - depth;
   const auto &type = replacements[index];
 
   if(!is_java_generic_parameter(type))
@@ -213,9 +209,8 @@ select_pointer_typet::get_recursively_instantiated_type(
   }
 
   visited.insert(parameter_name);
-  const auto &gen_type = to_java_generic_parameter(type).type_variable();
   const auto inst_val = get_recursively_instantiated_type(
-    gen_type.get_identifier(),
+    to_java_generic_parameter(type).get_name(),
     generic_parameter_specialization_map,
     visited,
     depth);
diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h
index 3f9cc18f82d..64c1127f6c1 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.h
+++ b/jbmc/src/java_bytecode/select_pointer_type.h
@@ -32,7 +32,7 @@ class select_pointer_typet
     const size_t) const;
   optionalt<pointer_typet> get_recursively_instantiated_type(
     const irep_idt &parameter_name,
-    const generic_parameter_specialization_mapt &) const;
+    const generic_parameter_specialization_mapt &visited) const;
 
 public:
   virtual ~select_pointer_typet() = default;
@@ -46,7 +46,7 @@ class select_pointer_typet
     const pointer_typet &pointer_type,
     const generic_parameter_specialization_mapt
       &generic_parameter_specialization_map,
-    generic_parameter_recursion_trackingt &) const;
+    generic_parameter_recursion_trackingt &visited) const;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
index e11a40e996e..98dc10b63ed 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
@@ -20,7 +20,7 @@ SCENARIO(
     "./java_bytecode/goto_program_generics",
     "MutuallyRecursiveGenerics.f");
 
-  std::string class_prefix = "java::MutuallyRecursiveGenerics";
+  const std::string class_prefix = "java::MutuallyRecursiveGenerics";
 
   REQUIRE(symbol_table.has_symbol(class_prefix));
 
@@ -86,7 +86,7 @@ SCENARIO(
     const std::vector<codet> &entry_point_code =
       require_goto_statements::require_entry_point_statements(symbol_table);
 
-    auto has_key_and_value_field = [&](
+    const auto has_key_and_value_field = [&](
       const irep_idt &field,
       const irep_idt &key_type,
       const irep_idt &val_type) {
@@ -150,7 +150,7 @@ SCENARIO(
         require_goto_statements::require_struct_component_assignment(
           tmp_object_name, {}, "example2", "java::Three", {}, entry_point_code);
 
-      auto has_x_u_e_fields = [&](
+      const auto has_x_e_u_fields = [&](
         const irep_idt &field,
         const irep_idt &x_type,
         const irep_idt &e_type,
@@ -167,7 +167,7 @@ SCENARIO(
         "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(
+        has_x_e_u_fields(
           example2_field,
           "java::java.lang.Byte",
           "java::java.lang.Character",
@@ -183,7 +183,7 @@ SCENARIO(
               "java::Three",
               {},
               entry_point_code);
-          has_x_u_e_fields(
+          has_x_e_u_fields(
             rotate_field,
             "java::java.lang.Integer",
             "java::java.lang.Byte",
@@ -199,7 +199,7 @@ SCENARIO(
                 "java::Three",
                 {},
                 entry_point_code);
-            has_x_u_e_fields(
+            has_x_e_u_fields(
               rotate_rec_field,
               "java::java.lang.Character",
               "java::java.lang.Integer",
@@ -215,7 +215,7 @@ SCENARIO(
                 "java::Three",
                 {},
                 entry_point_code);
-            has_x_u_e_fields(
+            has_x_e_u_fields(
               rotate_normal_field,
               "java::java.lang.Integer",
               "java::java.lang.Byte",
@@ -232,7 +232,7 @@ SCENARIO(
               "java::Three",
               {},
               entry_point_code);
-          has_x_u_e_fields(
+          has_x_e_u_fields(
             normal_field,
             "java::java.lang.Byte",
             "java::java.lang.Character",
@@ -247,7 +247,7 @@ SCENARIO(
                 "java::Three",
                 {},
                 entry_point_code);
-            has_x_u_e_fields(
+            has_x_e_u_fields(
               normal_rec_field,
               "java::java.lang.Byte",
               "java::java.lang.Character",
@@ -263,7 +263,7 @@ SCENARIO(
                 "java::Three",
                 {},
                 entry_point_code);
-            has_x_u_e_fields(
+            has_x_e_u_fields(
               normal_rotate_field,
               "java::java.lang.Integer",
               "java::java.lang.Byte",

From d7b1572d2ee66f7d975afe15e0cf79e56304076d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 5 Jun 2018 15:38:10 +0200
Subject: [PATCH 14/15] Doxygen update

---
 jbmc/src/java_bytecode/select_pointer_type.cpp | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index af24baaad3a..ed657af0384 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -135,7 +135,8 @@ pointer_typet select_pointer_typet::specialize_generics(
 /// instantiation due to a loop in its recursion.
 /// \param parameter_name The name of the generic parameter type we want to have
 ///   instantiated
-/// \param generic_specialization_map Map of type names to specialization stack
+/// \param generic_parameter_specialization_map Map of type names to
+///   specialization stack
 /// \return The first instantiated type for the generic type or nothing if no
 ///   such instantiation exists.
 optionalt<pointer_typet>
@@ -171,11 +172,15 @@ select_pointer_typet::get_recursively_instantiated_type(
 /// See get_recursively instantiated_type, the additional parameters just track
 /// the recursion to prevent visiting the same depth again and specify which
 /// stack depth is analyzed.
+/// \param parameter_name The name of the generic parameter type we want to have
+///   instantiated
+/// \param generic_parameter_specialization_map Map of type names to
+/// specialization stack
 /// \param visited Tracks the visited parameter names
 /// \param depth Stack depth to analyze
 /// \return if this type is not a generic type, it is returned as a valid
-///   instantiation, if nothing can be found at the given depth, en empty optional
-///   is returned
+///   instantiation, if nothing can be found at the given depth, en empty
+///   optional is returned
 optionalt<pointer_typet>
 select_pointer_typet::get_recursively_instantiated_type(
   const irep_idt &parameter_name,

From d196cf78a7832810667a39ef452bcd4ea5ecbdb8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 7 Jun 2018 16:23:15 +0200
Subject: [PATCH 15/15] Add regression test for recursive generic-parameters

---
 .../generics_recursive_parameters/KeyValue.class  | Bin 0 -> 562 bytes
 .../MutuallyRecursiveGenerics.class               | Bin 0 -> 361 bytes
 .../MutuallyRecursiveGenerics.java                |  11 +++++++++++
 .../jbmc/generics_recursive_parameters/test.desc  |   9 +++++++++
 4 files changed, 20 insertions(+)
 create mode 100644 jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class
 create mode 100644 jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class
 create mode 100644 jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java
 create mode 100644 jbmc/regression/jbmc/generics_recursive_parameters/test.desc

diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class b/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class
new file mode 100644
index 0000000000000000000000000000000000000000..a7920d988fcaf3c390cb899fbff5698729e872f0
GIT binary patch
literal 562
zcmZut%TB^T6g|VMfGCKH&ls2LLN=~!Lt;#H0cs+o`=L&7uog4zH1@MxnYi!+{3zp{
z3Mk-W?%ea3oICgP>-_`3DfY_9V%x%wg<XbRAYLMda;Gg4m-|}S45h9d1U%A8Fx01l
z(`(y3*KU!)QX&>AoReLf97fJQip0De@|ZV$9t@hd{h{z8Baww6ADbkDTtWp$1~O_9
zJUnt~qKnZzY1NJl#EpLH3)SO&Kg}9>+;_Q>29L>H^dLiqMrTG#o+rBFw9gg?asT03
zi#FOzcchgkE~Ob@|5`_y`+jmKJgq_*iz^WbCB5*(e6@lqY7E86CK+n;8^8fFw0$6#
zo;>LH)Ma2%E#eoK2$!)m)hmRT|KJr;VDji*rS6<=!{m?Oz+S1zqE5Atk_>CqSAGmw
Trx;*khB5J(@hA;!rfBOM&IWc%

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class
new file mode 100644
index 0000000000000000000000000000000000000000..58e7cc0256ac79b80d38be9adf6e069a22a2efd4
GIT binary patch
literal 361
zcmZ`!%Sr=55Ufr%SzV)v-a<ff^a1Y0o8m>#%c@{P?z59tCycu=yA$xUJP9810r@Dg
zCk7ED4b$CKQ&rH*ug?X5bL=N*VlPHFMvu_GG=-_J2+gD82_d>Jr%dQ(rr>-3nzI|L
z+zNA$m0H<}awgz48PzYQA`G%SUwdWk+aqi5Dl_L>F4!4eT@dJrkc>+2G~bvIb+}P|
zHdAxeL4+2ezfnc#1zl=Y@ti*7GuAbRXvkHe8uBCna+++ZOp@6;`2fAIzGLa_6&Yho
f_Rfz0+eicfJHO^rK_Tv+G5KSpwUHz!$alX1Rn$gz

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java
new file mode 100644
index 00000000000..1fbdeb644d2
--- /dev/null
+++ b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java
@@ -0,0 +1,11 @@
+class KeyValue<K, V> {
+    KeyValue<K, V> next;
+    KeyValue<V, K> reverse;
+    K key;
+    V value;
+}
+class MutuallyRecursiveGenerics {
+  void f() {
+    KeyValue<String, Integer> example1;
+  }
+}
diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/test.desc b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc
new file mode 100644
index 00000000000..859670558b4
--- /dev/null
+++ b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc
@@ -0,0 +1,9 @@
+CORE
+MutuallyRecursiveGenerics.class
+--cover location --function MutuallyRecursiveGenerics.f
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This failed before due to infinite recursion in the way how the instantiated
+generic parameters were used. cf. TG-3067