[TG-3374] Fix generic_type_index

regression/jbmc-cover/generics/AbstractTest.java

@@ -0,0 +1,22 @@
+interface AbstractInt<K,V> { V get(); }
+
+class AbstractImpl<K,V> implements AbstractInt<K,V> {
+    V t;
+    public V get() { return t; }
+}
+
+public class AbstractTest {
+    class Dummy { private boolean b; }
+    class ClassA { private int id; }
+    class ClassB {
+        private int id;
+        int getId() { return id; }
+    }
+
+    public int getFromAbstract(AbstractInt<ClassA, ClassB> arg) {
+        AbstractImpl<Dummy, Dummy> dummy = new AbstractImpl<>();
+        ClassB b = arg.get();
+        int i = b.getId();
+        return i;
+    }
+}

regression/jbmc-cover/generics/test.desc

@@ -0,0 +1,11 @@
+CORE
+AbstractTest.class
+--cover location --function AbstractTest.getFromAbstract
+^EXIT=0$
+^SIGNAL=0$
+file AbstractTest.java line 18 .* SATISFIED
+file AbstractTest.java line 19 .* SATISFIED
+file AbstractTest.java line 20 .* SATISFIED
+file AbstractTest.java line 21 .* SATISFIED
+
+

src/java_bytecode/java_types.cpp

@@ -416,8 +416,10 @@ size_t find_closing_semi_colon_for_reference_type(
 /// representation thereof.
 ///
 /// Example use are object types like "Ljava/lang/Integer;", type
-/// variables/parameters like "TE;" which require a non-empty \p class_name
-/// or generic types like "Ljava/util/List<T>;" or "Ljava/util/List<Integer>;"
+/// variables/parameters like "TE;" which require a non-empty
+/// \p class_name_prefix or generic types like "Ljava/util/List<TE;>;"
+/// or "Ljava/util/List<Ljava/lang/Integer;>;" also requiring
+/// \p class_name_prefix.
 ///
 /// \param src: the string representation as used in the class file
 /// \param class_name_prefix: name of class to append to generic type
@@ -833,3 +835,52 @@ void get_dependencies_from_generic_parameters(
 {
   get_dependencies_from_generic_parameters_rec(t, refs);
 }
+
+/// Construct a generic symbol type by extending the symbol type \p type with
+/// generic types extracted from the reference \p base_ref.
+/// This assumes that the class named \p class_name_prefix extends or implements
+/// the class \p type, and that \p base_ref corresponds to a generic class.
+/// For instance since HashMap<K,V> extends Map<K,V> we would call
+/// `java_generic_symbol_typet(symbol_typet("Map"), "Ljava/util/Map<TK;TV;>;",
+/// "java.util.HashMap")` which generates a symbol type with identifier "Map",
+/// and two generic types with identifier "java.util.HashMap::K" and
+/// "java.util.HashMap::V" respectively.
+java_generic_symbol_typet::java_generic_symbol_typet(
+  const symbol_typet &type,
+  const std::string &base_ref,
+  const std::string &class_name_prefix)
+  : symbol_typet(type)
+{
+  set(ID_C_java_generic_symbol, true);
+  const typet &base_type = java_type_from_string(base_ref, class_name_prefix);
+  PRECONDITION(is_java_generic_type(base_type));
+  const java_generic_typet &gen_base_type = to_java_generic_type(base_type);
+  INVARIANT(
+    type.get_identifier() == to_symbol_type(gen_base_type.subtype()).get_identifier(),
+    "identifier of "+type.pretty()+"\n and identifier of type "+
+    gen_base_type.subtype().pretty()+"\ncreated by java_type_from_string for "+
+    base_ref+" should be equal");
+  generic_types().insert(
+    generic_types().end(),
+    gen_base_type.generic_type_arguments().begin(),
+    gen_base_type.generic_type_arguments().end());
+}
+
+/// Check if this symbol has the given generic type. If yes, return its index
+/// in the vector of generic types.
+/// \param type The parameter type we are looking for.
+/// \return The index of the type in the vector of generic types.
+optionalt<size_t> java_generic_symbol_typet::generic_type_index(
+  const java_generic_parametert &type) const
+{
+  const auto &type_variable = type.get_name();
+  const auto &generics = generic_types();
+  for(std::size_t i = 0; i < generics.size(); ++i)
+  {
+    if(
+      is_java_generic_parameter(generics[i]) &&
+      to_java_generic_parameter(generics[i]).get_name() == type_variable)
+      return i;
+  }
+  return {};
+}

src/java_bytecode/java_types.h

@@ -582,18 +582,7 @@ class java_generic_symbol_typet : public symbol_typet
   java_generic_symbol_typet(
     const symbol_typet &type,
     const std::string &base_ref,
-    const std::string &class_name_prefix)
-    : symbol_typet(type)
-  {
-    set(ID_C_java_generic_symbol, true);
-    const typet &base_type = java_type_from_string(base_ref, class_name_prefix);
-    PRECONDITION(is_java_generic_type(base_type));
-    const java_generic_typet gen_base_type = to_java_generic_type(base_type);
-    generic_types().insert(
-      generic_types().end(),
-      gen_base_type.generic_type_arguments().begin(),
-      gen_base_type.generic_type_arguments().end());
-  }
+    const std::string &class_name_prefix);
 
   const generic_typest &generic_types() const
   {
@@ -605,18 +594,8 @@ 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 {};
-  }
+  optionalt<size_t>
+  generic_type_index(const java_generic_parametert &type) const;
 };
 
 /// \param type: the type to check

unit/Makefile

@@ -24,6 +24,10 @@ SRC += unit_tests.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
        miniBDD_new.cpp \
        java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
+       java_bytecode/java_types/erase_type_arguments.cpp \
+       java_bytecode/java_types/generic_type_index.cpp \
+       java_bytecode/java_types/java_generic_symbol_type.cpp \
+       java_bytecode/java_types/java_type_from_string.cpp \
        java_bytecode/java_utils_test.cpp \
        java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
        pointer-analysis/custom_value_set_analysis.cpp \

unit/java_bytecode/java_types/erase_type_arguments.cpp

@@ -7,7 +7,7 @@
 \*******************************************************************/
 
 #include <testing-utils/catch.hpp>
-#include <java_types.h>
+#include <java_bytecode/java_types.h>
 
 SCENARIO("erase_type_arguments", "[core][java_types]")
 {

unit/java_bytecode/java_types/generic_type_index.cpp

@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+ Module: Unit tests for java_types
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <java_bytecode/java_types.h>
+
+SCENARIO("generic_type_index", "[core][java_types]")
+{
+  GIVEN("PrefixClassName<X, value> extends GenericClass<X,value>, "
+          "and parameters X, value, Z")
+  {
+    const auto symbol_type = symbol_typet("java::GenericClass");
+    const auto generic_symbol_type = java_generic_symbol_typet(
+      symbol_type, "LGenericClass<TX;Tvalue;>;", "PrefixClassName");
+    java_generic_parametert paramX("PrefixClassName::X", symbol_typet());
+    java_generic_parametert value("PrefixClassName::value", symbol_typet());
+    java_generic_parametert paramZ("PrefixClassName::Z", symbol_typet());
+
+    WHEN("Looking for parameter indexes")
+    {
+      const auto indexX = generic_symbol_type.generic_type_index(paramX);
+      const auto index_value = generic_symbol_type.generic_type_index(value);
+      const auto indexZ = generic_symbol_type.generic_type_index(paramZ);
+
+      THEN("X has index 0, Y index 1 and Z is not found")
+      {
+        REQUIRE(indexX.has_value());
+        REQUIRE(indexX.value() == 0);
+        REQUIRE(index_value.has_value());
+        REQUIRE(index_value.value() == 1);
+        REQUIRE_FALSE(indexZ.has_value());
+      }
+    }
+  }
+
+  GIVEN("HashMap<K,V> extends Map<K,V>, and parameters K, V, T")
+  {
+    const auto symbol_type = symbol_typet("java::java.util.Map");
+    const auto generic_symbol_type = java_generic_symbol_typet(
+      symbol_type, "Ljava/util/Map<TK;TV;>;", "java.util.HashMap");
+    java_generic_parametert param0("java.util.HashMap::K", symbol_typet());
+    java_generic_parametert param1("java.util.HashMap::V", symbol_typet());
+    java_generic_parametert param2("java.util.HashMap::T", symbol_typet());
+
+    WHEN("Looking for parameter indexes")
+    {
+      const auto index_param0 = generic_symbol_type.generic_type_index(param0);
+      const auto index_param1 = generic_symbol_type.generic_type_index(param1);
+      const auto index_param2 = generic_symbol_type.generic_type_index(param2);
+
+      THEN("K has index 0, V index 1 and T is not found")
+      {
+        REQUIRE(index_param0.has_value());
+        REQUIRE(index_param0.value() == 0);
+        REQUIRE(index_param1.has_value());
+        REQUIRE(index_param1.value() == 1);
+        REQUIRE_FALSE(index_param2.has_value());
+      }
+    }
+  }
+}

unit/java_bytecode/java_types/java_generic_symbol_type.cpp

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+ Module: Unit tests for java_types
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <java_bytecode/java_types.h>
+
+SCENARIO("java_generic_symbol_type", "[core][java_types]")
+{
+  GIVEN("LGenericClass<TX;TY;>;")
+  {
+    auto symbol_type = symbol_typet("java::GenericClass");
+    const auto generic_symbol_type = java_generic_symbol_typet(
+      symbol_type, "LGenericClass<TX;TY;>;", "PrefixClassName");
+
+    REQUIRE(generic_symbol_type.get_identifier() == "java::GenericClass");
+
+    auto types = generic_symbol_type.generic_types();
+    REQUIRE(types.size() == 2);
+
+    auto generic_var0 = to_java_generic_parameter(types[0]).type_variable();
+    REQUIRE(generic_var0.get_identifier() == "PrefixClassName::X");
+
+    auto generic_var1 = to_java_generic_parameter(types[1]).type_variable();
+    REQUIRE(generic_var1.get_identifier() == "PrefixClassName::Y");
+  }
+}

unit/java_bytecode/java_types/java_type_from_string.cpp

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+ Module: Unit tests for java_types
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <java_bytecode/java_types.h>
+
+SCENARIO("java_type_from_string", "[core][java_types]")
+{
+  // TODO : add more cases, the current test is not comprehensive
+
+  GIVEN("Ljava/lang/Integer;")
+  {
+    const auto integer_type = java_type_from_string("Ljava/lang/Integer;", "");
+    REQUIRE(integer_type != nil_typet());
+  }
+
+  GIVEN("TE;")
+  {
+    const auto generic_type_E = java_type_from_string("TE;", "MyClass");
+    REQUIRE(generic_type_E != nil_typet());
+  }
+
+  GIVEN("Ljava/util/List<TX;>;")
+  {
+    const auto generic_list_type =
+      java_type_from_string("Ljava/util/List<TX;>;", "java.util.List");
+    REQUIRE(generic_list_type != nil_typet());
+  }
+
+  GIVEN("Ljava/util/List<Ljava/lang/Integer>;")
+  {
+    const auto integer_list_type =
+      java_type_from_string("Ljava/util/List<Ljava/lang/Integer;>;", "");
+    REQUIRE(integer_list_type != nil_typet());
+  }
+
+  GIVEN("Ljava/util/Map<TK;TV;>;")
+  {
+    const auto generic_symbol_type =
+      java_type_from_string("Ljava/util/Map<TK;TV;>;", "java.util.Map");
+    REQUIRE(generic_symbol_type != nil_typet());
+  }
+}