[TG-3067] Support generic type parameters that create recursion loops in instantiation stack

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

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

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

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -33,11 +33,10 @@ 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();
-      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);
-      }
     }
   }
 

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

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -32,8 +32,11 @@ pointer_typet select_pointer_typet::convert_pointer_type(
   // a generic parameter, specialize it with concrete types
   if(!generic_parameter_specialization_map.empty())
   {
-    return specialize_generics(
-      pointer_type, generic_parameter_specialization_map);
+    generic_parameter_recursion_trackingt visited;
+    const auto &type = specialize_generics(
+      pointer_type, generic_parameter_specialization_map, visited);
+    INVARIANT(visited.empty(), "recursion stack must be empty here");
+    return type;
   }
   else
   {
@@ -62,13 +65,24 @@ 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))
   {
     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
@@ -78,15 +92,20 @@ 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
-    return is_java_generic_parameter(type)
-             ? specialize_generics(
-                 to_java_generic_parameter(type),
-                 generic_parameter_specialization_map)
-             : type;
+    if(!is_java_generic_parameter(type))
+      return type;
+
+    visited_nodes.insert(parameter_name);
+    const 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)
   {
@@ -99,7 +118,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);
+          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);
@@ -109,3 +129,96 @@ pointer_typet select_pointer_typet::specialize_generics(
   }
   return pointer_type;
 }
+
+/// 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_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>
+select_pointer_typet::get_recursively_instantiated_type(
+  const irep_idt &parameter_name,
+  const generic_parameter_specialization_mapt
+    &generic_parameter_specialization_map) const
+{
+  generic_parameter_recursion_trackingt visited;
+  const size_t max_depth =
+    generic_parameter_specialization_map.find(parameter_name)->second.size();
+
+  irep_idt current_parameter = parameter_name;
+  for(size_t depth = 0; depth < max_depth; depth++)
+  {
+    const auto retval = get_recursively_instantiated_type(
+      current_parameter, generic_parameter_specialization_map, visited, depth);
+    if(retval.has_value())
+    {
+      CHECK_RETURN(!is_java_generic_parameter(*retval));
+      return retval;
+    }
+    CHECK_RETURN(visited.empty());
+
+    const auto &entry =
+      generic_parameter_specialization_map.find(current_parameter)
+        ->second.back();
+    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
+/// 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
+optionalt<pointer_typet>
+select_pointer_typet::get_recursively_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
+{
+  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");
+
+  const auto &replacements = val->second;
+
+  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 {};
+  }
+
+  const size_t index = (replacements.size() - 1) - depth;
+  const auto &type = replacements[index];
+
+  if(!is_java_generic_parameter(type))
+  {
+    return type;
+  }
+
+  visited.insert(parameter_name);
+  const auto inst_val = get_recursively_instantiated_type(
+    to_java_generic_parameter(type).get_name(),
+    generic_parameter_specialization_map,
+    visited,
+    depth);
+  visited.erase(parameter_name);
+  return inst_val;
+}

jbmc/src/java_bytecode/select_pointer_type.h

@@ -11,18 +11,29 @@
 /// \file
 /// Handle selection of correct pointer type (for example changing abstract
 /// classes to concrete versions).
+#include <vector>
 
-#include <util/std_types.h>
-#include <stack>
 #include "java_types.h"
+#include <util/optional.h>
+#include <util/std_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;
+typedef std::set<irep_idt> generic_parameter_recursion_trackingt;
 
 class namespacet;
 
 class select_pointer_typet
 {
+  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_recursively_instantiated_type(
+    const irep_idt &parameter_name,
+    const generic_parameter_specialization_mapt &visited) const;
+
 public:
   virtual ~select_pointer_typet() = default;
   virtual pointer_typet convert_pointer_type(
@@ -34,7 +45,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 &visited) const;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H

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

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() {
+  }
+}