Merge pull request #2051 from svorenova/generics_tg2717

[TG-2717] Generic inheritance with pointer replacement

Author: Thomas Kiley

src/java_bytecode/java_object_factory.cpp

@@ -766,6 +766,13 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // for java types, technical debt TG-2707
   if(!equal_java_types(replacement_pointer_type, pointer_type))
   {
+    // update generic_parameter_specialization_map for the new pointer
+    generic_parameter_specialization_map_keyst
+      generic_parameter_specialization_map_keys(
+        generic_parameter_specialization_map);
+    generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
+      replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
+
     const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
       assignments, alloc_type, replacement_pointer_type, depth);
 

src/java_bytecode/java_types.h

@@ -604,6 +604,19 @@ class java_generic_symbol_typet : public symbol_typet
   {
     return (generic_typest &)(add(ID_generic_types).get_sub());
   }
+
+  /// Check if this symbol has the given generic type. If yes, return its index
+  /// in the vector of generic types.
+  /// \param type The type we are looking for.
+  /// \return The index of the type in the vector of generic types.
+  optionalt<size_t> generic_type_index(const reference_typet &type) const
+  {
+    const auto &type_pointer =
+      std::find(generic_types().begin(), generic_types().end(), type);
+    if(type_pointer != generic_types().end())
+      return type_pointer - generic_types().begin();
+    return {};
+  }
 };
 
 /// \param type: the type to check

src/util/std_types.h

@@ -396,15 +396,22 @@ class class_typet:public struct_typet
     bases().push_back(baset(base));
   }
 
-  bool has_base(const irep_idt &id) const
+  /// Return the base with the given name, if exists.
+  /// \param id The name of the base we are looking for.
+  /// \return The base if exists.
+  optionalt<baset> get_base(const irep_idt &id) const
   {
     for(const auto &b : bases())
     {
-      if(to_symbol_type(b.type()).get(ID_identifier)==id)
-        return true;
+      if(to_symbol_type(b.type()).get_identifier() == id)
+        return b;
     }
+    return {};
+  }
 
-    return false;
+  bool has_base(const irep_idt &id) const
+  {
+    return get_base(id).has_value();
   }
 
   bool is_abstract() const