diff --git a/regression/jbmc-cover/generics/AbstractImpl.class b/regression/jbmc-cover/generics/AbstractImpl.class new file mode 100644 index 00000000000..eff2707433f Binary files /dev/null and b/regression/jbmc-cover/generics/AbstractImpl.class differ diff --git a/regression/jbmc-cover/generics/AbstractInt.class b/regression/jbmc-cover/generics/AbstractInt.class new file mode 100644 index 00000000000..f595d5d3bca Binary files /dev/null and b/regression/jbmc-cover/generics/AbstractInt.class differ diff --git a/regression/jbmc-cover/generics/AbstractTest$ClassA.class b/regression/jbmc-cover/generics/AbstractTest$ClassA.class new file mode 100644 index 00000000000..b22a6b21506 Binary files /dev/null and b/regression/jbmc-cover/generics/AbstractTest$ClassA.class differ diff --git a/regression/jbmc-cover/generics/AbstractTest$ClassB.class b/regression/jbmc-cover/generics/AbstractTest$ClassB.class new file mode 100644 index 00000000000..bd168a70121 Binary files /dev/null and b/regression/jbmc-cover/generics/AbstractTest$ClassB.class differ diff --git a/regression/jbmc-cover/generics/AbstractTest$Dummy.class b/regression/jbmc-cover/generics/AbstractTest$Dummy.class new file mode 100644 index 00000000000..76f7bb61679 Binary files /dev/null and b/regression/jbmc-cover/generics/AbstractTest$Dummy.class differ diff --git a/regression/jbmc-cover/generics/AbstractTest.class b/regression/jbmc-cover/generics/AbstractTest.class new file mode 100644 index 00000000000..d2fff4e9d81 Binary files /dev/null and b/regression/jbmc-cover/generics/AbstractTest.class differ diff --git a/regression/jbmc-cover/generics/AbstractTest.java b/regression/jbmc-cover/generics/AbstractTest.java new file mode 100644 index 00000000000..5b6049a211c --- /dev/null +++ b/regression/jbmc-cover/generics/AbstractTest.java @@ -0,0 +1,22 @@ +interface AbstractInt { V get(); } + +class AbstractImpl implements AbstractInt { + 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 arg) { + AbstractImpl dummy = new AbstractImpl<>(); + ClassB b = arg.get(); + int i = b.getId(); + return i; + } +} diff --git a/regression/jbmc-cover/generics/test.desc b/regression/jbmc-cover/generics/test.desc new file mode 100644 index 00000000000..c11972c0136 --- /dev/null +++ b/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 + + diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 1d1b247fe11..4f13d8ea265 100644 --- a/src/java_bytecode/java_types.cpp +++ b/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;" or "Ljava/util/List;" +/// variables/parameters like "TE;" which require a non-empty +/// \p class_name_prefix or generic types like "Ljava/util/List;" +/// or "Ljava/util/List;" 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 extends Map we would call +/// `java_generic_symbol_typet(symbol_typet("Map"), "Ljava/util/Map;", +/// "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 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 {}; +} diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 0e47a33a218..8aa2dc114da 100644 --- a/src/java_bytecode/java_types.h +++ b/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 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 + generic_type_index(const java_generic_parametert &type) const; }; /// \param type: the type to check diff --git a/unit/Makefile b/unit/Makefile index 05f188506aa..b150bfa632c 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/java_bytecode/java_types/erase_type_arguments.cpp b/unit/java_bytecode/java_types/erase_type_arguments.cpp index e1214350bcc..225f2d8c4c3 100644 --- a/unit/java_bytecode/java_types/erase_type_arguments.cpp +++ b/unit/java_bytecode/java_types/erase_type_arguments.cpp @@ -7,7 +7,7 @@ \*******************************************************************/ #include -#include +#include SCENARIO("erase_type_arguments", "[core][java_types]") { diff --git a/unit/java_bytecode/java_types/generic_type_index.cpp b/unit/java_bytecode/java_types/generic_type_index.cpp new file mode 100644 index 00000000000..913658b4e89 --- /dev/null +++ b/unit/java_bytecode/java_types/generic_type_index.cpp @@ -0,0 +1,66 @@ +/*******************************************************************\ + + Module: Unit tests for java_types + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include + +SCENARIO("generic_type_index", "[core][java_types]") +{ + GIVEN("PrefixClassName extends GenericClass, " + "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;", "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 extends Map, 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;", "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()); + } + } + } +} diff --git a/unit/java_bytecode/java_types/java_generic_symbol_type.cpp b/unit/java_bytecode/java_types/java_generic_symbol_type.cpp new file mode 100644 index 00000000000..d24e8bd2e54 --- /dev/null +++ b/unit/java_bytecode/java_types/java_generic_symbol_type.cpp @@ -0,0 +1,31 @@ +/*******************************************************************\ + + Module: Unit tests for java_types + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include + +SCENARIO("java_generic_symbol_type", "[core][java_types]") +{ + GIVEN("LGenericClass;") + { + auto symbol_type = symbol_typet("java::GenericClass"); + const auto generic_symbol_type = java_generic_symbol_typet( + symbol_type, "LGenericClass;", "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"); + } +} diff --git a/unit/java_bytecode/java_types/java_type_from_string.cpp b/unit/java_bytecode/java_types/java_type_from_string.cpp new file mode 100644 index 00000000000..e6d7eac80ea --- /dev/null +++ b/unit/java_bytecode/java_types/java_type_from_string.cpp @@ -0,0 +1,48 @@ +/*******************************************************************\ + + Module: Unit tests for java_types + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include + +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;") + { + const auto generic_list_type = + java_type_from_string("Ljava/util/List;", "java.util.List"); + REQUIRE(generic_list_type != nil_typet()); + } + + GIVEN("Ljava/util/List;") + { + const auto integer_list_type = + java_type_from_string("Ljava/util/List;", ""); + REQUIRE(integer_list_type != nil_typet()); + } + + GIVEN("Ljava/util/Map;") + { + const auto generic_symbol_type = + java_type_from_string("Ljava/util/Map;", "java.util.Map"); + REQUIRE(generic_symbol_type != nil_typet()); + } +}