Introduce a map of parameter-type pairs

The map of generic parameters and a stack of their concrete types in the
various depths of the current scope.

Author: svorenova

src/java_bytecode/Makefile

@@ -4,6 +4,7 @@ SRC = bytecode_info.cpp \
       ci_lazy_methods_needed.cpp \
       expr2java.cpp \
       generic_arguments_name_builder.cpp \
+      generic_parameter_specialization_map_keys.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \

src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -0,0 +1,155 @@
+/// Author: DiffBlue Limited. All Rights Reserved.
+
+#include "generic_parameter_specialization_map_keys.h"
+
+/// \param type Source type
+/// \return The vector of implicitly generic and (explicitly) generic type
+/// parameters of the given type.
+const std::vector<java_generic_parametert>
+get_all_generic_parameters(const typet &type)
+{
+  PRECONDITION(
+    is_java_generic_class_type(type) ||
+    is_java_implicitly_generic_class_type(type));
+  std::vector<java_generic_parametert> generic_parameters;
+  if(is_java_implicitly_generic_class_type(type))
+  {
+    const java_implicitly_generic_class_typet &implicitly_generic_class =
+      to_java_implicitly_generic_class_type(to_java_class_type(type));
+    generic_parameters.insert(
+      generic_parameters.end(),
+      implicitly_generic_class.implicit_generic_types().begin(),
+      implicitly_generic_class.implicit_generic_types().end());
+  }
+  if(is_java_generic_class_type(type))
+  {
+    const java_generic_class_typet &generic_class =
+      to_java_generic_class_type(to_java_class_type(type));
+    generic_parameters.insert(
+      generic_parameters.end(),
+      generic_class.generic_types().begin(),
+      generic_class.generic_types().end());
+  }
+  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
+const 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");
+  PRECONDITION(parameters.size() == types.size());
+
+  // Pair up the parameters and types for easier manipulation later
+  std::vector<std::pair<java_generic_parametert, reference_typet>> pairs;
+  pairs.reserve(parameters.size());
+  std::transform(
+    parameters.begin(),
+    parameters.end(),
+    types.begin(),
+    std::back_inserter(pairs),
+    [&](java_generic_parametert param, reference_typet type)
+    {
+      return std::make_pair(param, type);
+    });
+
+  for(const auto &pair : pairs)
+  {
+    // 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 initiating a pointer to an implicitly java generic 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();
+      if(generic_parameter_specialization_map.count(key) == 0)
+        generic_parameter_specialization_map.emplace(
+          key, std::stack<reference_typet>());
+      (*generic_parameter_specialization_map.find(key))
+        .second.push(pair.second);
+
+      // We added something, so pop it when this 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.
+/// \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
+const void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
+  const pointer_typet &pointer_type,
+  const typet &pointer_subtype_struct)
+{
+  if(is_java_generic_type(pointer_type))
+  {
+    // The supplied type must be the full type of the pointer's subtype
+    PRECONDITION(
+      pointer_type.subtype().get(ID_identifier) ==
+      pointer_subtype_struct.get(ID_name));
+
+    const java_generic_typet &generic_pointer =
+      to_java_generic_type(pointer_type);
+
+    // If the pointer points to an incomplete class, don't treat the generics
+    if(!pointer_subtype_struct.get_bool(ID_incomplete_class))
+    {
+      PRECONDITION(
+        is_java_generic_class_type(pointer_subtype_struct) ||
+        is_java_implicitly_generic_class_type(pointer_subtype_struct));
+      const std::vector<java_generic_parametert> &generic_parameters =
+        get_all_generic_parameters(pointer_subtype_struct);
+
+      INVARIANT(
+        generic_pointer.generic_type_arguments().size() ==
+          generic_parameters.size(),
+        "All generic parameters of the pointer type need to be specified");
+
+      insert_pairs(
+        generic_parameters, generic_pointer.generic_type_arguments());
+    }
+  }
+}
+
+/// 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.
+/// \param symbol_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
+const void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
+  const symbol_typet &symbol_type,
+  const typet &symbol_struct)
+{
+  if(is_java_generic_symbol_type(symbol_type))
+  {
+    java_generic_symbol_typet generic_symbol =
+      to_java_generic_symbol_type(symbol_type);
+
+    PRECONDITION(
+      is_java_generic_class_type(symbol_struct) ||
+      is_java_implicitly_generic_class_type(symbol_struct));
+    const std::vector<java_generic_parametert> &generic_parameters =
+      get_all_generic_parameters(symbol_struct);
+
+    INVARIANT(
+      generic_symbol.generic_types().size() == generic_parameters.size(),
+      "All generic parameters of the superclass need to be concretized");
+
+    insert_pairs(generic_parameters, generic_symbol.generic_types());
+  }
+}

src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -0,0 +1,69 @@
+/// Author: DiffBlue Limited. All Rights Reserved.
+
+#ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
+#define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H
+
+#include "select_pointer_type.h"
+#include "java_types.h"
+
+/// \file
+/// Generic-parameter-specialization-map entries owner class.
+/// Generic-parameter-specialization-map maps generic parameters to a stack
+/// of their types in (every depth of) the current scope. This class adds
+/// entries to the map for a particular scope, and ensures that they are erased
+/// on leaving that scope.
+class generic_parameter_specialization_map_keyst
+{
+public:
+  /// Initialize a generic-parameter-specialization-map entry owner operating
+  /// on a given map. Initially it does not own any map entry.
+  /// \param _generic_parameter_specialization_map: map to operate on.
+  explicit generic_parameter_specialization_map_keyst(
+    generic_parameter_specialization_mapt
+      &_generic_parameter_specialization_map)
+    : generic_parameter_specialization_map(
+        _generic_parameter_specialization_map)
+  {
+  }
+
+  /// Removes the top of the stack for each key in erase_keys from the
+  /// controlled map.
+  ~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())
+      {
+        generic_parameter_specialization_map.erase(key);
+      }
+    }
+  }
+
+  // Objects of these class cannot be copied in any way - delete the copy
+  // constructor and copy assignment operator
+  generic_parameter_specialization_map_keyst(
+    const generic_parameter_specialization_map_keyst &) = delete;
+  generic_parameter_specialization_map_keyst &
+  operator=(const generic_parameter_specialization_map_keyst &) = delete;
+
+  const void insert_pairs_for_pointer(
+    const pointer_typet &pointer_type,
+    const typet &pointer_subtype_struct);
+  const void insert_pairs_for_symbol(
+    const symbol_typet &symbol_type,
+    const typet &symbol_struct);
+
+private:
+  /// Generic parameter specialization map to modify
+  generic_parameter_specialization_mapt &generic_parameter_specialization_map;
+  /// Keys of the entries to pop on destruction
+  std::vector<irep_idt> erase_keys;
+
+  const void insert_pairs(
+    const std::vector<java_generic_parametert> &parameters,
+    const std::vector<reference_typet> &types);
+};
+
+#endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H

src/java_bytecode/java_object_factory.cpp

@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_utils.h"
 #include "java_string_library_preprocess.h"
 #include "java_root_class.h"
+#include "generic_parameter_specialization_map_keys.h"
 
 static symbolt &new_tmp_symbol(
   symbol_table_baset &symbol_table,
@@ -68,6 +69,16 @@ class java_object_factoryt
   /// this set AND the tree depth becomes >= than the maximum value above.
   std::unordered_set<irep_idt, irep_id_hash> recursion_set;
 
+  /// 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
+  /// 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
+  /// of the scope the parameters can be specialized with different types
+  /// so we keep a stack of types for each parameter.
+  generic_parameter_specialization_mapt generic_parameter_specialization_map;
+
   /// The symbol table.
   symbol_table_baset &symbol_table;
 
@@ -1151,6 +1162,15 @@ void java_object_factoryt::gen_nondet_init(
   {
     // dereferenced type
     const pointer_typet &pointer_type=to_pointer_type(type);
+
+    // If we are about to initialize a generic pointer type, add its concrete
+    // types to the map and delete them on leaving this function scope.
+    generic_parameter_specialization_map_keyst
+      generic_parameter_specialization_map_keys(
+        generic_parameter_specialization_map);
+    generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
+      pointer_type, ns.follow(pointer_type.subtype()));
+
     gen_nondet_pointer_init(
       assignments,
       expr,
@@ -1164,6 +1184,21 @@ void java_object_factoryt::gen_nondet_init(
   else if(type.id()==ID_struct)
   {
     const struct_typet struct_type=to_struct_type(type);
+
+    // If we are about to initialize a generic class (as a superclass object
+    // for a different object), add its concrete types to the map and delete
+    // them on leaving this function scope.
+    generic_parameter_specialization_map_keyst
+      generic_parameter_specialization_map_keys(
+        generic_parameter_specialization_map);
+    if(is_sub)
+    {
+      const typet &symbol = override_ ? override_type : expr.type();
+      PRECONDITION(symbol.id() == ID_symbol);
+      generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
+        to_symbol_type(symbol), struct_type);
+    }
+
     gen_nondet_struct_init(
       assignments,
       expr,

src/java_bytecode/java_object_factory.h

@@ -107,6 +107,9 @@ exprt object_factory(
   allocation_typet alloc_type,
   const source_locationt &location);
 
+typedef std::unordered_map<irep_idt, std::stack<reference_typet>,
+  irep_id_hash> generic_parameter_specialization_mapt;
+
 enum class update_in_placet
 {
   NO_UPDATE_IN_PLACE,

src/java_bytecode/java_types.h

@@ -120,10 +120,14 @@ class java_generic_parametert:public reference_typet
     return const_cast<type_variablet &>(type_variables().front());
   }
 
+  const irep_idt get_name() const
+  {
+    return type_variable().get_identifier();
+  }
+
   const std::string get_parameter_class_name() const
   {
-    const std::string &parameter_name =
-      type_variable().get_identifier().c_str();
+    const std::string &parameter_name = get_name().c_str();
     PRECONDITION(has_prefix(parameter_name, "java::"));
     int prefix_length = std::string("java::").length();
     const std::string name = parameter_name.substr(