From c141611c66516a363bfc7adae57cf68237aaea56 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 27 Apr 2018 07:11:07 +0100 Subject: [PATCH 1/9] Fix generic_type_index This function needs to look at the type_variables comment to known which argument correspondsd to the given type. --- src/java_bytecode/java_types.h | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 0e47a33a218..72c3029ed1a 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -609,12 +609,18 @@ class java_generic_symbol_typet : public symbol_typet /// 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 + optionalt + generic_type_index(const java_generic_parametert &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(); + const auto &type_variable = type.type_variable(); + 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]).type_variable() == type_variable) + return i; + } return {}; } }; From b7c9ea195aebb6047b9467d724249910ae41e052 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 27 Apr 2018 07:30:52 +0100 Subject: [PATCH 2/9] Test for abstract class with two generic arguments --- .../jbmc-cover/generics/AbstractImpl.class | Bin 0 -> 466 bytes .../jbmc-cover/generics/AbstractInt.class | Bin 0 -> 240 bytes .../generics/AbstractTest$ClassA.class | Bin 0 -> 349 bytes .../generics/AbstractTest$ClassB.class | Bin 0 -> 416 bytes .../generics/AbstractTest$Dummy.class | Bin 0 -> 346 bytes .../jbmc-cover/generics/AbstractTest.class | Bin 0 -> 645 bytes .../jbmc-cover/generics/AbstractTest.java | 22 ++++++++++++++++++ regression/jbmc-cover/generics/test.desc | 11 +++++++++ 8 files changed, 33 insertions(+) create mode 100644 regression/jbmc-cover/generics/AbstractImpl.class create mode 100644 regression/jbmc-cover/generics/AbstractInt.class create mode 100644 regression/jbmc-cover/generics/AbstractTest$ClassA.class create mode 100644 regression/jbmc-cover/generics/AbstractTest$ClassB.class create mode 100644 regression/jbmc-cover/generics/AbstractTest$Dummy.class create mode 100644 regression/jbmc-cover/generics/AbstractTest.class create mode 100644 regression/jbmc-cover/generics/AbstractTest.java create mode 100644 regression/jbmc-cover/generics/test.desc diff --git a/regression/jbmc-cover/generics/AbstractImpl.class b/regression/jbmc-cover/generics/AbstractImpl.class new file mode 100644 index 0000000000000000000000000000000000000000..eff2707433f7be5cf764b36f877ff3a36597e54e GIT binary patch literal 466 zcmZvY%SyvQ6o&uFr7>x=7wc^yxJ+EM8&@_2L=Z}YA`RImaR@2tRMLshr633{d;lLx zJgHW&?c!YKoNxX)b3VV`KLA|d#Da#N2^9wh4h_=N_{w5Y&B@0=`sT>LEh2tS9`ZS<5nO9}XZ}NJI&WZ{7LiXzq+OW{H(SX5V zuezhzW5Li~UjRe%j}Q`Pv^5P3IvHvOiaV4kFv(C0Q^lt2lw!^3=Wk#ylrZd)Z!C){ d`8~Ag%763~%JUkk|LV61{&}f`E-?!BzX5inUe*8r literal 0 HcmV?d00001 diff --git a/regression/jbmc-cover/generics/AbstractInt.class b/regression/jbmc-cover/generics/AbstractInt.class new file mode 100644 index 0000000000000000000000000000000000000000..f595d5d3bcafb3db92a968f6003a0d1aac59cd9e GIT binary patch literal 240 zcmX^0Z`VEs1_l!b9(D#Ub_Q-n2IlnC5=I6Q4Nae{#Ii*FoW#6zegCAa)Z`LtMh4E{ z%=Em(lG377Mg~?5&5$sln2n9M6{gxSEMj(;$`~2Ag7Zs@l2hF>bAVAuM(V4zLI( E0PEsAfB*mh literal 0 HcmV?d00001 diff --git a/regression/jbmc-cover/generics/AbstractTest$ClassA.class b/regression/jbmc-cover/generics/AbstractTest$ClassA.class new file mode 100644 index 0000000000000000000000000000000000000000..b22a6b21506144982d0966e1a876aafac73a7b35 GIT binary patch literal 349 zcmY*UO-sW-5Pg%x#H4GRSig=UJ=6-;gEvJe1))&%VDY|57u^z5$Zq{#9z^iq5Aa8c zvjHKp%+9=-H*aRXe?GqeT;eE(k6wZRX@uPf`vgxf2{a>w_F0?31))2iHzq2DG9rlmAy!ju03F{>(7H%J*m>J-MMte(dA`AQX*;1At4qAi1CzBb^)J$_pV xfi!hfIYVqQ680UAP8tS~jLzOcqYrp*4M*@FHrx&~b{Ki+VvoJ+^pT+t`~o8aMIitH literal 0 HcmV?d00001 diff --git a/regression/jbmc-cover/generics/AbstractTest$ClassB.class b/regression/jbmc-cover/generics/AbstractTest$ClassB.class new file mode 100644 index 0000000000000000000000000000000000000000..bd168a7012123dd6898bff0d1ba784259ce2d253 GIT binary patch literal 416 zcmZ8dO-sW-5Ph5G!^W5<*6$CH(nA};dhn(QS`Y$74;Js6bg5fn3fZl{%8Q@~9{d6R zC~*=LqAcvpym|B9?0$Z|e*ieaUK1u(U07(B*_wk52ipvWoG`GM!PfUub&nbR(M6(k z!BagJN}p2aOy*LbGladrt^OT@Ih;=fLu({+alLp*L^0+`Mu;^PIwtK#uTSdk?R-(B z;!2jSux@ZPpDKp4;J{{a7 zGm+}bnHKcwGB}{OTl66Y9WnxfptPWLbpv370XBK fhrds;M6Kurji-N9pTq*f420OC=n~b$IyQlC&;m*- literal 0 HcmV?d00001 diff --git a/regression/jbmc-cover/generics/AbstractTest$Dummy.class b/regression/jbmc-cover/generics/AbstractTest$Dummy.class new file mode 100644 index 0000000000000000000000000000000000000000..76f7bb6167908438120d4013d98093af1a0ea6e6 GIT binary patch literal 346 zcmY+9O-sW-5Qg7L(!|8rCiU|u(nD>*dhn(QQW1or2a5-9o49C7l0tSP^k?-Tf(L(q zKT4bp9wN)^J0H)??tK4zegQbcfe#zK01hG#eGj_?O4yzVu71tb;FQpvT_s9aBGq%L z^f^~9vNF?`gn0PBbo@wgrpsqZ=*_ZH-ql4StGP&W&IAw3x=Q6uW`ejq@?;_2L6NJ7g;QwXIcp(|-oH`xBK zLZ`TdZnigd!^z&MccJuNj}-R=s`py{6|bC;6o3j+B7u6VJ$%@-L%o@F&QqBkG$DD9 z`pJRPqC&gKs6iA&bLSf3iVo+}7E-cETSJ{C`sfFuNnHDh+^1{gkKcZWA@B?4$-8eT vyf>DNuXhcqFz8n~vqoFTGM4!2>CgB*PrYSW#8u?kR-#0|Otgtlh);oA0#u5P literal 0 HcmV?d00001 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 + + From 0afbe0fe028359a3ab675fbdf7efb7160abe2b92 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 2 May 2018 09:25:08 +0100 Subject: [PATCH 3/9] Unit test java_type_from_string and fix doc Unit-testing this function revealed some mistakes in the examples given in the documentation. --- src/java_bytecode/java_types.cpp | 6 ++- .../java_types/java_type_from_string.cpp | 48 +++++++++++++++++++ 2 files changed, 52 insertions(+), 2 deletions(-) create mode 100644 unit/java_bytecode/java_types/java_type_from_string.cpp diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 1d1b247fe11..717ecae354c 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 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()); + } +} From 41b3a6aebebcd06a0a96d8430d3894024db17dc5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 2 May 2018 09:26:35 +0100 Subject: [PATCH 4/9] Move java_generic_symbol_typet definitions to cpp --- src/java_bytecode/java_types.cpp | 44 ++++++++++++++++++++++++++++++++ src/java_bytecode/java_types.h | 31 ++-------------------- 2 files changed, 46 insertions(+), 29 deletions(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 717ecae354c..e23c5b06965 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -835,3 +835,47 @@ 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); + 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 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.type_variable(); + 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]).type_variable() == type_variable) + return i; + } + return {}; +} diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 72c3029ed1a..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,24 +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 java_generic_parametert &type) const - { - const auto &type_variable = type.type_variable(); - 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]).type_variable() == type_variable) - return i; - } - return {}; - } + generic_type_index(const java_generic_parametert &type) const; }; /// \param type: the type to check From 8f0f780ce9bae42a7634f44184770c15d71e0bdb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 2 May 2018 09:27:29 +0100 Subject: [PATCH 5/9] Unit test for java_generic_symbol_type --- .../java_types/java_generic_symbol_type.cpp | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 unit/java_bytecode/java_types/java_generic_symbol_type.cpp 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..87b5f2e89ab --- /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]") +{ + WHEN("MyType is LGenericClass;") + { + auto symbol_type = symbol_typet("MyType"); + const auto generic_symbol_type = java_generic_symbol_typet( + symbol_type, "LGenericClass;", "PrefixClassName"); + + REQUIRE(generic_symbol_type.get_identifier() == "MyType"); + + 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"); + } +} From 4c5144dead75d5a03166bf94a8b78d4d3e6a3ef7 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 2 May 2018 09:27:48 +0100 Subject: [PATCH 6/9] Unit test for generic_type_index --- .../java_types/generic_type_index.cpp | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 unit/java_bytecode/java_types/generic_type_index.cpp 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()); + } + } + } +} From 4a6ae9babf772ecf16b1ddd92fbfdd6712486bfe Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 2 May 2018 11:22:04 +0100 Subject: [PATCH 7/9] Add java_types unit tests to Makefile --- unit/Makefile | 4 ++++ unit/java_bytecode/java_types/erase_type_arguments.cpp | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) 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]") { From e3f240ac25edb1028291271717d4568b470f0dee Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 2 May 2018 12:14:58 +0100 Subject: [PATCH 8/9] Use get_name in generic_type_index --- src/java_bytecode/java_types.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index e23c5b06965..f65042e4be3 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -863,18 +863,18 @@ java_generic_symbol_typet::java_generic_symbol_typet( /// 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. +/// \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.type_variable(); + 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]).type_variable() == type_variable) + to_java_generic_parameter(generics[i]).get_name() == type_variable) return i; } return {}; From 53bc89259adad1eec8bc81f0d259952fba3f672e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 2 May 2018 12:41:39 +0100 Subject: [PATCH 9/9] Add invariant in java_generic_symbol_type This also adapt unit tests that would make the invariant fail. --- src/java_bytecode/java_types.cpp | 7 ++++++- unit/java_bytecode/java_types/java_generic_symbol_type.cpp | 6 +++--- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index f65042e4be3..4f13d8ea265 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -854,7 +854,12 @@ java_generic_symbol_typet::java_generic_symbol_typet( 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); + 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(), diff --git a/unit/java_bytecode/java_types/java_generic_symbol_type.cpp b/unit/java_bytecode/java_types/java_generic_symbol_type.cpp index 87b5f2e89ab..d24e8bd2e54 100644 --- a/unit/java_bytecode/java_types/java_generic_symbol_type.cpp +++ b/unit/java_bytecode/java_types/java_generic_symbol_type.cpp @@ -11,13 +11,13 @@ SCENARIO("java_generic_symbol_type", "[core][java_types]") { - WHEN("MyType is LGenericClass;") + GIVEN("LGenericClass;") { - auto symbol_type = symbol_typet("MyType"); + 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() == "MyType"); + REQUIRE(generic_symbol_type.get_identifier() == "java::GenericClass"); auto types = generic_symbol_type.generic_types(); REQUIRE(types.size() == 2);