Use the map of parameter-type pairs to specialize generics

Author: svorenova

src/java_bytecode/ci_lazy_methods.cpp

@@ -322,8 +322,10 @@ void ci_lazy_methodst::initialize_all_needed_classes_from_pointer(
 {
   initialize_needed_classes_from_pointer(pointer_type, ns, needed_lazy_methods);
 
-  const pointer_typet &subbed_pointer_type=
-    pointer_type_selector.convert_pointer_type(pointer_type, ns);
+  // TODO we should be passing here a map that maps generic parameters
+  // to concrete types in the current context TG-2664
+  const pointer_typet &subbed_pointer_type =
+    pointer_type_selector.convert_pointer_type(pointer_type, {}, ns);
 
   if(subbed_pointer_type!=pointer_type)
   {

src/java_bytecode/java_object_factory.cpp

@@ -753,18 +753,19 @@ void java_object_factoryt::gen_nondet_pointer_init(
   const update_in_placet &update_in_place)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
-  const pointer_typet &replacement_pointer_type=
-    pointer_type_selector.convert_pointer_type(pointer_type, ns);
+  const pointer_typet &replacement_pointer_type =
+    pointer_type_selector.convert_pointer_type(
+      pointer_type, generic_parameter_specialization_map, ns);
 
   // If we are changing the pointer, we generate code for creating a pointer
   // to the substituted type instead
-  if(replacement_pointer_type!=pointer_type)
+  // TODO if we are comparing array types we need to compare their element
+  // types. this is for now done by implementing equality function especially
+  // for java types, technical debt TG-2707
+  if(!equal_java_types(replacement_pointer_type, pointer_type))
   {
-    const symbol_exprt real_pointer_symbol=gen_nondet_subtype_pointer_init(
-      assignments,
-      alloc_type,
-      replacement_pointer_type,
-      depth);
+    const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
+      assignments, alloc_type, replacement_pointer_type, depth);
 
     // Having created a pointer to object of type replacement_pointer_type
     // we now assign it back to the original pointer with a cast

src/java_bytecode/java_object_factory.h

@@ -107,9 +107,6 @@ 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.cpp

@@ -713,6 +713,37 @@ bool is_valid_java_array(const struct_typet &type)
     data_component_valid;
 }
 
+/// Compares the types, including checking element types if both types are
+/// arrays.
+/// \param type1 First type to compare
+/// \param type2 Second type to compare
+/// \return True if the types are equal, including elemnt types if they are
+/// both arrays
+bool equal_java_types(const typet &type1, const typet &type2)
+{
+  bool arrays_with_same_element_type = true;
+  if(
+    type1.id() == ID_pointer && type2.id() == ID_pointer &&
+    type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
+  {
+    const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
+    const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
+    if(
+      subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
+      is_java_array_tag(subtype_symbol1.get_identifier()))
+    {
+      const typet &array_element_type1 =
+        java_array_element_type(subtype_symbol1);
+      const typet &array_element_type2 =
+        java_array_element_type(subtype_symbol2);
+
+      arrays_with_same_element_type =
+        equal_java_types(array_element_type1, array_element_type2);
+    }
+  }
+  return (type1 == type2 && arrays_with_same_element_type);
+}
+
 void get_dependencies_from_generic_parameters_rec(
   const typet &t,
   std::set<irep_idt> &refs)

src/java_bytecode/java_types.h

@@ -90,6 +90,8 @@ size_t find_closing_semi_colon_for_reference_type(
 bool is_java_array_tag(const irep_idt &tag);
 bool is_valid_java_array(const struct_typet &);
 
+bool equal_java_types(const typet &type1, const typet &type2);
+
 /// Class to hold a Java generic type parameter (also called type variable),
 /// e.g., `T` in `List<T>`.
 /// The bound can specify type requirements.

src/java_bytecode/select_pointer_type.cpp

@@ -11,15 +11,101 @@
 /// classes to concrete versions).
 
 #include "select_pointer_type.h"
+#include "java_types.h"
 #include <util/std_types.h>
 
 /// Select what type should be used for a given pointer type. For the base class
 /// we just use the supplied type. Derived classes can override this behaviour
-/// to provide more sophisticated type selection
+/// to provide more sophisticated type selection. Generic parameters are
+/// replaced with their concrete type.
 /// \param pointer_type: The pointer type replace
+/// \param generic_parameter_specialization_map map of types for all generic
+/// parameters in the current scope
 /// \return A pointer type where the subtype may have been modified
 pointer_typet select_pointer_typet::convert_pointer_type(
-  const pointer_typet &pointer_type, const namespacet &ns) const
+  const pointer_typet &pointer_type,
+  const generic_parameter_specialization_mapt
+    &generic_parameter_specialization_map,
+  const namespacet &ns) const
 {
-  return  pointer_type;
+  // if we have a map of generic parameters -> types and the pointer is
+  // a generic parameter, specialize it with concrete types
+  if(!generic_parameter_specialization_map.empty())
+  {
+    return specialize_generics(
+      pointer_type, generic_parameter_specialization_map);
+  }
+  else
+  {
+    return pointer_type;
+  }
+}
+
+/// Specialize generic parameters in a pointer type based on the current map
+/// of parameters -> types. We specialize generics if the pointer is a java
+/// generic parameter or an array with generic parameters (java generic types
+/// are specialized recursively, their concrete types are already stored in
+/// the map and will be retrieved when needed e.g., to initialize fields).
+/// Example:
+/// - generic type: T
+/// - map: T -> U; U -> String
+/// - result: String
+///
+/// - generic type: T[]
+/// - map: T -> U; U -> String
+/// - result: String
+/// \param pointer_type pointer to be specialized
+/// \param generic_parameter_specialization_map map of types for all generic
+/// parameters in the current scope
+/// \return pointer type where generic parameters are replaced with concrete
+/// types, if set in the current scope
+pointer_typet select_pointer_typet::specialize_generics(
+  const pointer_typet &pointer_type,
+  const generic_parameter_specialization_mapt
+    &generic_parameter_specialization_map) 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();
+    if(generic_parameter_specialization_map.count(parameter_name) == 0)
+    {
+      // this means that the generic pointer_type has not been specialized
+      // in the current context (e.g., the method under test is generic);
+      // we return the pointer_type itself which is basically a pointer to
+      // its upper bound
+      return pointer_type;
+    }
+    const pointer_typet &type =
+      generic_parameter_specialization_map.find(parameter_name)->second.top();
+
+    // 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;
+  }
+  else if(pointer_type.subtype().id() == ID_symbol)
+  {
+    // if the pointer is an array, recursively specialize its element type
+    const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());
+    if(is_java_array_tag(array_subtype.get_identifier()))
+    {
+      const typet &array_element_type = java_array_element_type(array_subtype);
+      if(array_element_type.id() == ID_pointer)
+      {
+        const pointer_typet &new_array_type = specialize_generics(
+          to_pointer_type(array_element_type),
+          generic_parameter_specialization_map);
+
+        pointer_typet replacement_array_type = java_array_type('a');
+        replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
+        return replacement_array_type;
+      }
+    }
+  }
+  return pointer_type;
 }

src/java_bytecode/select_pointer_type.h

@@ -13,15 +13,28 @@
 /// classes to concrete versions).
 
 #include <util/std_types.h>
+#include <stack>
+#include "java_types.h"
+
+typedef std::unordered_map<irep_idt, std::stack<reference_typet>, irep_id_hash>
+  generic_parameter_specialization_mapt;
 
 class namespacet;
 
 class select_pointer_typet
 {
 public:
-  virtual ~select_pointer_typet()=default;
+  virtual ~select_pointer_typet() = default;
   virtual pointer_typet convert_pointer_type(
-    const pointer_typet &pointer_type, const namespacet &ns) const;
+    const pointer_typet &pointer_type,
+    const generic_parameter_specialization_mapt
+      &generic_parameter_specialization_map,
+    const namespacet &ns) const;
+
+  pointer_typet specialize_generics(
+    const pointer_typet &pointer_type,
+    const generic_parameter_specialization_mapt
+      &generic_parameter_specialization_map) const;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H