Merge pull request #4929 from NathanJPhillips/bugfix/generic_parameter_specialization_map

Fix generic_parameter_specialization_map in the presence of non-symmetric generic recursion [TG-7815]

Author: NathanJPhillips

jbmc/src/java_bytecode/Makefile

@@ -5,6 +5,7 @@ SRC = assignments_from_json.cpp \
       ci_lazy_methods_needed.cpp \
       convert_java_nondet.cpp \
       expr2java.cpp \
+      generic_parameter_specialization_map.cpp \
       generic_parameter_specialization_map_keys.cpp \
       jar_file.cpp \
       jar_pool.cpp \

jbmc/src/java_bytecode/README.md

@@ -76,11 +76,7 @@ types so we keep a stack of types for each parameter.
 
 We use the map in \ref select_pointer_typet::specialize_generics to
 retrieve the concrete type of generic parameters such as `MyGeneric::T` and of
-arrays of generic parameters such as `MyGeneric::T[]`. Special attention
-is paid to breaking infinite recursion when searching the map, e.g.,
-`MyGeneric::T` being specialized with `MyGeneric::U` and vice versa, for an
-example of such a recursion see
-\ref select_pointer_typet::get_recursively_instantiated_type. More complicated
+arrays of generic parameters such as `MyGeneric::T[]`. More complicated
 generic types such as `MyGeneric<T>` are specialized indirectly within \ref
 java_object_factoryt. Their concrete types are already stored in the map and are
 retrieved when needed, e.g., to initialize their fields.

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

@@ -0,0 +1,67 @@
+/// Author: Diffblue Ltd.
+
+#include "generic_parameter_specialization_map.h"
+
+std::size_t generic_parameter_specialization_mapt::insert(
+  const std::vector<java_generic_parametert> &parameters,
+  std::vector<reference_typet> types)
+{
+  PRECONDITION(!parameters.empty());
+  const auto first_param_it =
+    param_to_container.find(parameters.front().get_name());
+  std::size_t container_index;
+  if(first_param_it == param_to_container.end())
+  {
+    container_index = container_to_specializations.size();
+    container_to_specializations.emplace_back();
+    std::size_t param_index = 0;
+    for(const java_generic_parametert &parameter : parameters)
+    {
+      const auto result = param_to_container.emplace(
+        parameter.get_name(), container_paramt{container_index, param_index++});
+      INVARIANT(
+        result.second, "Some type parameters are already mapped but not all");
+    }
+  }
+  else
+  {
+    container_index = first_param_it->second.container_index;
+    std::size_t param_index = 0;
+    for(const java_generic_parametert &parameter : parameters)
+    {
+      const auto param_it = param_to_container.find(parameter.get_name());
+      INVARIANT(
+        param_it != param_to_container.end(),
+        "Some type parameters are already mapped but not all");
+      INVARIANT(
+        param_it->second.container_index == container_index,
+        "Not all type parameters are assigned to same container");
+      INVARIANT(
+        param_it->second.param_index == param_index,
+        "Type parameters have been encountered in two different orders");
+      ++param_index;
+    }
+  }
+  container_to_specializations[container_index].push(std::move(types));
+  return container_index;
+}
+
+void generic_parameter_specialization_mapt::pop(std::size_t container_index)
+{
+  container_to_specializations.at(container_index).pop();
+}
+
+optionalt<reference_typet>
+generic_parameter_specialization_mapt::pop(const irep_idt &parameter_name)
+{
+  const auto types_it = param_to_container.find(parameter_name);
+  if(types_it == param_to_container.end())
+    return {};
+  std::stack<std::vector<reference_typet>> &stack =
+    container_to_specializations.at(types_it->second.container_index);
+  if(stack.empty())
+    return {};
+  reference_typet result = stack.top().at(types_it->second.param_index);
+  stack.pop();
+  return result;
+}

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

@@ -0,0 +1,141 @@
+/// Author: Diffblue Ltd.
+
+#ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H
+#define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H
+
+#include <stack>
+#include <vector>
+
+#include <util/string_utils.h>
+
+#include "expr2java.h"
+#include "java_types.h"
+
+/// A map from generic type parameters to their specializations (type arguments)
+/// We need to map from the names of parameters to the container (class or
+/// method) that contains them as well as the particular specialization of that
+/// parameter. However we do not need the name of the container, merely the full
+/// set of specializations for the parameters of that container.
+/// We store a stack of specializations for each container for a particular
+/// context. Finding the value for a type parameter is a matter of following
+/// the specialization for that parameter, unwinding the stack of its container
+/// as you do so and repeating until one reaches a non-generic type.
+class generic_parameter_specialization_mapt
+{
+private:
+  /// The index of the container and the type parameter inside that container
+  struct container_paramt
+  {
+    std::size_t container_index;
+    std::size_t param_index;
+  };
+  /// A map from parameter names to container_paramt instances
+  std::unordered_map<irep_idt, container_paramt> param_to_container;
+  /// The list of containers and, for each one, the stack of lists of
+  /// specializations
+  std::vector<std::stack<std::vector<reference_typet>>>
+    container_to_specializations;
+
+public:
+  /// Insert a specialization for each type parameters of a container
+  /// \param parameters: The type parameters
+  /// \param types: The type arguments
+  /// \returns: The index of the added container
+  std::size_t insert(
+    const std::vector<java_generic_parametert> &parameters,
+    std::vector<reference_typet> types);
+
+  /// Pop the top of the specialization stack for a given container
+  /// \param container_index: The index of the container to pop
+  void pop(std::size_t container_index);
+
+  /// Pop the top of the specialization stack for the container associated with
+  /// a given type parameter
+  /// \param parameter_name: The name of the type parameter
+  /// \returns: The specialization for the given type parameter, if there was
+  ///   one before the pop, or an empty optionalt if the stack was empty
+  optionalt<reference_typet> pop(const irep_idt &parameter_name);
+
+  /// A wrapper for a generic_parameter_specialization_mapt and a namespacet
+  /// that can be output to a stream
+  struct printert
+  {
+    const generic_parameter_specialization_mapt &map;
+    const namespacet &ns;
+
+    printert(
+      const generic_parameter_specialization_mapt &map,
+      const namespacet &ns)
+      : map(map), ns(ns)
+    {
+    }
+  };
+
+  template <typename ostreamt>
+  friend ostreamt &operator<<(ostreamt &stm, const printert &map);
+};
+
+/// Output a generic_parameter_specialization_mapt wrapped in a
+/// generic_parameter_specialization_mapt::printert to a stream
+/// \tparam ostreamt: The type of stream to output to (not restricted to be
+///   derived from std::ostream)
+/// \param stm: The stream to output to
+/// \param map: The generic_parameter_specialization_mapt printer to output
+/// \returns: A reference to the stream passed in
+template <typename ostreamt>
+ostreamt &operator<<(
+  ostreamt &stm,
+  const generic_parameter_specialization_mapt::printert &map)
+{
+  if(map.map.container_to_specializations.empty())
+    stm << "empty map";
+  else
+    stm << "map:\n";
+  std::vector<std::vector<irep_idt>> container_to_params(
+    map.map.container_to_specializations.size());
+  for(const auto &elt : map.map.param_to_container)
+  {
+    std::vector<irep_idt> &params =
+      container_to_params[elt.second.container_index];
+    if(params.size() < elt.second.param_index + 1)
+      params.resize(elt.second.param_index + 1);
+    params[elt.second.param_index] = elt.first;
+  }
+  const namespacet &ns = map.ns;
+  for(std::size_t index = 0; index < container_to_params.size(); ++index)
+  {
+    stm << "<";
+    join_strings(
+      stm,
+      container_to_params.at(index).begin(),
+      container_to_params.at(index).end(),
+      ", ");
+    stm << ">: ";
+    std::stack<std::vector<reference_typet>> stack =
+      map.map.container_to_specializations.at(index);
+    while(!stack.empty())
+    {
+      stm << "<";
+      join_strings(
+        stm,
+        stack.top().begin(),
+        stack.top().end(),
+        ", ",
+        [&ns](const reference_typet &pointer_type) {
+          if(is_java_generic_parameter(pointer_type))
+          {
+            return id2string(
+              to_java_generic_parameter(pointer_type).get_name());
+          }
+          else
+            return type2java(pointer_type, ns);
+        });
+      stm << ">, ";
+      stack.pop();
+    }
+    stm << "\n";
+  }
+  return stm;
+}
+
+#endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -35,51 +35,18 @@ get_all_generic_parameters(const typet &type)
   return generic_parameters;
 }
 
-/// Add pairs to the controlled map. Own the keys and pop from their stack
-/// on destruction; otherwise do nothing.
-/// \param parameters: generic parameters that are the keys of the pairs to add
-/// \param types: a type to add for each parameter
-void generic_parameter_specialization_map_keyst::insert_pairs(
-  const std::vector<java_generic_parametert> &parameters,
-  const std::vector<reference_typet> &types)
-{
-  INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
-
-  for(const auto &pair : make_range(parameters).zip(types))
-  {
-    // Only add the pair if the type is not the parameter itself, e.g.,
-    // pair.first = pair.second = java::A::T. This can happen for example
-    // when initializing a pointer to an implicitly generic Java class type
-    // in gen_nondet_init and would result in a loop when the map is used
-    // to look up the type of the parameter.
-    if(
-      !(is_java_generic_parameter(pair.second) &&
-        to_java_generic_parameter(pair.second).get_name() ==
-          pair.first.get_name()))
-    {
-      const irep_idt &key = pair.first.get_name();
-      const auto map_it = generic_parameter_specialization_map
-                            .emplace(key, std::vector<reference_typet>{})
-                            .first;
-      map_it->second.push_back(pair.second);
-
-      // We added something; pop it when this
-      // generic_parameter_specialization_map_keyst is destroyed
-      erase_keys.push_back(key);
-    }
-  }
-}
-
-/// Add a pair of a parameter and its types for each generic parameter of the
-/// given generic pointer type to the controlled map. Own the keys and pop
-/// from their stack on destruction; otherwise do nothing.
+/// Add the parameters and their types for each generic parameter of the
+/// given generic pointer type to the map.
+/// Own the keys and pop from their stack on destruction.
 /// \param pointer_type: pointer type to get the specialized generic types from
 /// \param pointer_subtype_struct: struct type to which the generic pointer
 ///   points, must be generic if the pointer is generic
-void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
+void generic_parameter_specialization_map_keyst::insert(
   const pointer_typet &pointer_type,
   const typet &pointer_subtype_struct)
 {
+  // Use a fresh generic_parameter_specialization_map_keyst for each scope
+  PRECONDITION(!container_id);
   if(!is_java_generic_type(pointer_type))
     return;
   // The supplied type must be the full type of the pointer's subtype
@@ -91,7 +58,7 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
   // - an incomplete class or
   // - a class that is neither generic nor implicitly generic (this
   //   may be due to unsupported class signature)
-  // then ignore the generic types in the pointer and do not add any pairs.
+  // then ignore the generic types in the pointer and do not add an entry.
   // TODO TG-1996 should decide how mocking and generics should work
   //   together. Currently an incomplete class is never marked as generic. If
   //   this changes in TG-1996 then the condition below should be updated.
@@ -115,34 +82,39 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
     type_args.size() == generic_parameters.size(),
     "All generic parameters of the pointer type need to be specified");
 
-  insert_pairs(generic_parameters, type_args);
+  container_id =
+    generic_parameter_specialization_map.insert(generic_parameters, type_args);
 }
 
-/// Add a pair of a parameter and its types for each generic parameter of the
-/// given generic symbol type to the controlled map. This function is used
-/// for generic bases (superclass or interfaces) where the reference to it is
-/// in the form of a symbol rather than a pointer (as opposed to the function
-/// insert_pairs_for_pointer). Own the keys and pop from their stack
-/// on destruction; otherwise do nothing.
+/// Add the parameters and their types for each generic parameter of the
+/// given generic symbol type to the map.
+/// This function is used for generic bases (superclass or interfaces) where
+/// the reference to it is in the form of a symbol rather than a pointer.
+/// Own the keys and pop from their stack on destruction.
 /// \param struct_tag_type: symbol type to get the specialized generic types
 ///   from
 /// \param symbol_struct: struct type of the symbol type, must be generic if
 ///   the symbol is generic
-void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
+void generic_parameter_specialization_map_keyst::insert(
   const struct_tag_typet &struct_tag_type,
   const typet &symbol_struct)
 {
+  // Use a fresh generic_parameter_specialization_map_keyst for each scope
+  PRECONDITION(!container_id);
+  if(!is_java_generic_struct_tag_type(struct_tag_type))
+    return;
+  // The supplied type must be the full type of the pointer's subtype
+  PRECONDITION(
+    struct_tag_type.get(ID_identifier) == symbol_struct.get(ID_name));
+
   // If the struct is:
   // - an incomplete class or
   // - a class that is neither generic nor implicitly generic (this
   //  may be due to unsupported class signature)
-  // then ignore the generic types in the struct_tag_type and do not add any
-  // pairs.
+  // then ignore the generic types in the struct and do not add an entry.
   // TODO TG-1996 should decide how mocking and generics should work
   //   together. Currently an incomplete class is never marked as generic. If
   //   this changes in TG-1996 then the condition below should be updated.
-  if(!is_java_generic_struct_tag_type(struct_tag_type))
-    return;
   if(to_java_class_type(symbol_struct).get_is_stub())
     return;
   if(
@@ -151,17 +123,18 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
   {
     return;
   }
+
   const java_generic_struct_tag_typet &generic_symbol =
     to_java_generic_struct_tag_type(struct_tag_type);
 
   const std::vector<java_generic_parametert> &generic_parameters =
     get_all_generic_parameters(symbol_struct);
   const java_generic_typet::generic_type_argumentst &type_args =
     generic_symbol.generic_types();
-
   INVARIANT(
     type_args.size() == generic_parameters.size(),
     "All generic parameters of the superclass need to be concretized");
 
-  insert_pairs(generic_parameters, type_args);
+  container_id =
+    generic_parameter_specialization_map.insert(generic_parameters, type_args);
 }