From 30476789a95941746ec1a60f818e23b09b5333c0 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 30 Oct 2017 11:42:17 +0000 Subject: [PATCH 1/4] Removed old method of specalising generics We now use the select_pointer_type to specalise the type so we don't need to convert all references. --- .../generate_java_generic_type.cpp | 43 ------------------- .../generate_java_generic_type.h | 4 -- src/java_bytecode/java_bytecode_language.cpp | 15 +------ 3 files changed, 1 insertion(+), 61 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 6c6cbc4e1c8..d5747657ee6 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -126,46 +126,3 @@ irep_idt generate_java_generic_typet::build_generic_tag( return new_tag_buffer.str(); } - - -/// Activate the generic instantiation code. -/// \param message_handler -/// \param symbol_table The symbol table so far. -void -instantiate_generics( - message_handlert &message_handler, - symbol_tablet &symbol_table) -{ - generate_java_generic_typet instantiate_generic_type(message_handler); - // check out the symbols in the symbol table at this point to see if we - // have a a generic type in. - for(const auto &symbol : symbol_table.symbols) - { - if(symbol.second.type.id()==ID_struct) - { - auto symbol_struct=to_struct_type(symbol.second.type); - auto &components=symbol_struct.components(); - - for(const auto &component : components) - { - if(is_java_generic_type(component.type())) - { - const auto &type_vars=to_java_generic_type(component.type()). - generic_type_variables(); - - // Before we can instantiate a generic component, we need - // its type variables to be instantiated parameters - if(all_of(type_vars.cbegin(), type_vars.cend(), - [](const typet &type) - { - return is_java_generic_inst_parameter(type); - })) - { - instantiate_generic_type( - to_java_generic_type(component.type()), symbol_table); - } - } - } - } - } -} diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 6ba48378a31..c171976e5c7 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -31,8 +31,4 @@ class generate_java_generic_typet message_handlert &message_handler; }; -void instantiate_generics( - message_handlert &message_handler, - symbol_tablet &symbol_table); - #endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index b2653c9488d..9a7b9066cde 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -240,21 +240,8 @@ bool java_bytecode_languaget::typecheck( get_message_handler()); // now typecheck all - bool res=java_bytecode_typecheck( + return java_bytecode_typecheck( symbol_table, get_message_handler(), string_refinement_enabled); - // NOTE (FOTIS): There is some unintuitive logic here, where - // java_bytecode_check will return TRUE if typechecking failed, and FALSE - // if everything went well... - if(res) - { - // there is no point in continuing to concretise - // the generic types if typechecking failed. - return res; - } - - instantiate_generics(get_message_handler(), symbol_table); - - return res; } bool java_bytecode_languaget::generate_support_functions( From bba9f76747dc1b5d813443c7ff2cfde5922f8de8 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 2 Nov 2017 10:55:32 +0000 Subject: [PATCH 2/4] Remove redundant regression test Due to no longer creating specalisations for each generic type, the symbol table should no longer create specialisations for each type. --- .../generics$bound_element.class | Bin 892 -> 0 bytes .../generics_symtab1/generics$element.class | Bin 573 -> 0 bytes .../cbmc-java/generics_symtab1/generics.class | Bin 1032 -> 0 bytes .../cbmc-java/generics_symtab1/generics.java | 31 ------------------ .../cbmc-java/generics_symtab1/test.desc | 8 ----- 5 files changed, 39 deletions(-) delete mode 100644 regression/cbmc-java/generics_symtab1/generics$bound_element.class delete mode 100644 regression/cbmc-java/generics_symtab1/generics$element.class delete mode 100644 regression/cbmc-java/generics_symtab1/generics.class delete mode 100644 regression/cbmc-java/generics_symtab1/generics.java delete mode 100644 regression/cbmc-java/generics_symtab1/test.desc diff --git a/regression/cbmc-java/generics_symtab1/generics$bound_element.class b/regression/cbmc-java/generics_symtab1/generics$bound_element.class deleted file mode 100644 index 8076c290e12a9de020c7afdf303b3f7c5adbd307..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 892 zcmZ`%U2oGs5S)u+yD?51LJ8%wKm#~IqCD^fQ6y9e2`Ln$mOk);ob(!8xejt1B>ojh zAS5360sJV$>|IhfDm>WU+nt@Ao%8QMKYsyuf=&%p+zH^~u0&ft?)kW{P}QkEQD_d1 z<4^H+8fW9}-Py@d=g$;sd&xM9i&?G}-2L6RubA_S56QIsSRojUb*A%VG?i>G$&#Y4 zP>;%V=YaG(lS6i|4U$Y--u-x(GSeJPMsa!&=ZT!>$*Pc(WH^~+hwnw1&I*O_WyVQ6 zX*`{3mN!mEw3mR?(OPEx{Bgm&`JbMiS*y=hb)>K!b^hgpA9d#2tFgl6=sZSNRorSN zGC(hs8 z6dL6%T5bg=5;ZG}4&3JLyZj|8e8>mZ%&FFB$Rx%NpAdCcRvEn^Qm{ey;diL+4^+My z%o^VwF(5~S@0La3BG!2#-muXw#-YIlthG$-3O0xq_UEh!hui%I=L-V|C2?SgZL>Qk zF6ksAbXNXVM%QqCPWz5uv!IA}O2L82)@i`%8PVRUXb(4xB{Ib>BsD8qYBh?r^KMe9 Ujc#F+=n9R!#BV@E6>T(uzpNdiDgXcg diff --git a/regression/cbmc-java/generics_symtab1/generics$element.class b/regression/cbmc-java/generics_symtab1/generics$element.class deleted file mode 100644 index 34cb36e36b49a205496b9dd54785cf9216aaf601..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 573 zcmZWmO;5r=5PeH4g;Jze1;6FM0WlE|o|JGQn3yzb0^z>Y4K68*X^V+J%Y!lT;1BRe z8E27dl*8`Mym|BHV?RFM-T|DUnumdH8zy!v>{-}nFhwXP44yyckGvUjHEP}r$0A5B z81g+iQaqVOg2Cu_3CSk+GOnF6*#1Z;5y>FdXiF-Yv>A%^U-)Q1;+^Ro<(7P@#Pw`4 z6j7fKLqa@%8t`zyBdPrbXlii=OLrtx!r)vfs?iB~9199~KjO6og=&}oDm^`pb4G+dhaGk$|6 zB{h;5pZxo));RKkcNtK(i6KIFnMkT+-*bQHq~ zB4@zFeH{-J^UxsjNJmM>V}WR+GjR4_%eFj}PG7*RI*#maw5?uG_5^f~2sD%_kf^mJ zJ?v&LbuP3lVASoFWAz7JDUiRwtx`L%j;&(ba$3cz)0ZvTEw3>)Sg{?uzb4>MXLbd& zjm|!^%+zd0ZVwI{vir(vw28!Oou<{^wYs+Yo`PEcolUV}uO<_Uw*v8WHS?c(Bpt3Q z*Epls(6m`b`x<28=WBg9a_g;lg;LXyi`t6T`&RS)mUT2%$_wI+P-wj~=r-j`TXht5 z%NNvSOe`QSFzbSD0fj#?@f1rYR`HDDJdbnNU}6q2fw_OCtP(s|vFtA7#?O4~rw9)bNq$5mcY?ro7@zVdh^UjfG^qNw5#qkUUnfra zi>#f%GS!r5ty0H2H7IS_NqtY-Ca&WK)fsq!n;e3VOo7>A@Z%2s<3uK0%H!tA-6a=+ e_=R;H%Q{v_rV06w!3@tBtsn<+X^fee1^xi|W7(tt diff --git a/regression/cbmc-java/generics_symtab1/generics.java b/regression/cbmc-java/generics_symtab1/generics.java deleted file mode 100644 index 0a0af41c63a..00000000000 --- a/regression/cbmc-java/generics_symtab1/generics.java +++ /dev/null @@ -1,31 +0,0 @@ -public class generics { - - class element { - E elem; - } - - class bound_element { - NUM elem; - NUM f() { - return elem; - } - void g(NUM e) { - elem=e; - } - } - - bound_element belem; - - Integer f(int n) { - - element e=new element<>(); - e.elem=n; - bound_element be=new bound_element<>(); - belem=new bound_element<>(); - be.elem=new Integer(n+1); - if(n>0) - return e.elem; - else - return be.elem; - } -} diff --git a/regression/cbmc-java/generics_symtab1/test.desc b/regression/cbmc-java/generics_symtab1/test.desc deleted file mode 100644 index fe6b3693bf3..00000000000 --- a/regression/cbmc-java/generics_symtab1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -generics.class ---show-symbol-table -^EXIT=0$ -^SIGNAL=0$ -^Type........: struct generics\$bound_element\ \{ -__CPROVER_string \@class_identifier; boolean \@lock; struct java.lang.Object \@java.lang.Object; struct java.lang.Integer \*elem; struct generics \*this\$0; \}$ --- From bf10b1bb2a74ebe17f98f61775c54d96e7820a21 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 2 Nov 2017 16:51:16 +0000 Subject: [PATCH 3/4] Manually call specalisation code --- .../generate_java_generic_type.cpp | 31 ++++++++++++++++ unit/testing-utils/Makefile | 1 + unit/testing-utils/generic_utils.cpp | 37 +++++++++++++++++++ unit/testing-utils/generic_utils.h | 26 +++++++++++++ 4 files changed, 95 insertions(+) create mode 100644 unit/testing-utils/generic_utils.cpp create mode 100644 unit/testing-utils/generic_utils.h diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index b4c1a7ea07a..3455f341ed9 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -9,13 +9,33 @@ #include #include +#include #include #include #include +#include #include +/// Helper function to specalise a generic class from a named component of a +/// named class +/// \param class_name: The name of the class that has a generic component. +/// \param component_name: The name of the generic component +/// \param new_symbol_table: The symbol table to use. +void specialise_generic_from_component( + const irep_idt &class_name, + const irep_idt &component_name, + symbol_tablet &new_symbol_table) +{ + const symbolt &harness_symbol = new_symbol_table.lookup_ref(class_name); + const struct_typet::componentt &harness_component = + require_type::require_component( + to_struct_type(harness_symbol.type), component_name); + generic_utils::specialise_generic( + to_java_generic_type(harness_component.type()), new_symbol_table); +} + SCENARIO( "generate_java_generic_type_from_file", "[core][java_bytecode][generate_java_generic_type]") @@ -30,6 +50,9 @@ SCENARIO( load_java_class("generic_two_fields", "./java_bytecode/generate_concrete_generic_type"); + specialise_generic_from_component( + "java::generic_two_fields", "belem", new_symbol_table); + REQUIRE(new_symbol_table.has_symbol(expected_symbol)); THEN("The class should contain two instantiated fields.") { @@ -77,6 +100,9 @@ SCENARIO( load_java_class("generic_two_parameters", "./java_bytecode/generate_concrete_generic_type"); + specialise_generic_from_component( + "java::generic_two_parameters", "bomb", new_symbol_table); + REQUIRE(new_symbol_table.has_symbol( "java::generic_two_parameters$KeyValuePair")); THEN("The class should have two subtypes in the vector of the types of " @@ -140,6 +166,11 @@ SCENARIO( load_java_class("generic_two_instances", "./java_bytecode/generate_concrete_generic_type"); + specialise_generic_from_component( + "java::generic_two_instances", "bool_element", new_symbol_table); + specialise_generic_from_component( + "java::generic_two_instances", "int_element", new_symbol_table); + REQUIRE(new_symbol_table.has_symbol(first_expected_symbol)); auto first_symbol=new_symbol_table.lookup(first_expected_symbol); REQUIRE(first_symbol->type.id()==ID_struct); diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 45ccd69ec7b..73f1331d5de 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,5 +1,6 @@ SRC = \ c_to_expr.cpp \ + generic_utils.cpp \ load_java_class.cpp \ require_expr.cpp \ require_goto_statements.cpp \ diff --git a/unit/testing-utils/generic_utils.cpp b/unit/testing-utils/generic_utils.cpp new file mode 100644 index 00000000000..57c9cc20145 --- /dev/null +++ b/unit/testing-utils/generic_utils.cpp @@ -0,0 +1,37 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include +#include "generic_utils.h" +#include "catch.hpp" +#include "require_type.h" + +/// Generic a specalised version of a Java generic class and add it to the +/// symbol table. +/// \param example_type: A reference type that is a specalised generic to use +/// as the base for the specalised version (e.g. a variable of type +/// `Generic` +/// \param new_symbol_table: The symbol table to store the new type in +void generic_utils::specialise_generic( + const java_generic_typet &example_type, + symbol_tablet &new_symbol_table) +{ + // Should be a fully instantiated generic type + REQUIRE( + std::all_of( + example_type.generic_type_variables().begin(), + example_type.generic_type_variables().end(), + is_java_generic_inst_parameter)); + + // Generate the specialised version. + ui_message_handlert message_handler; + generate_java_generic_typet instantiate_generic_type(message_handler); + instantiate_generic_type( + to_java_generic_type(example_type), new_symbol_table); +} diff --git a/unit/testing-utils/generic_utils.h b/unit/testing-utils/generic_utils.h new file mode 100644 index 00000000000..4bfc70fb4be --- /dev/null +++ b/unit/testing-utils/generic_utils.h @@ -0,0 +1,26 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Utility methods for dealing with Java generics in unit tests + +#ifndef CPROVER_TESTING_UTILS_GENERIC_UTILS_H +#define CPROVER_TESTING_UTILS_GENERIC_UTILS_H + +#include +#include + +// NOLINTNEXTLINE(readability/namespace) +namespace generic_utils +{ +void specialise_generic( + const java_generic_typet &example_type, + symbol_tablet &new_symbol_table); +} + +#endif // CPROVER_TESTING_UTILS_GENERIC_UTILS_H From 51133db88b995b088922d9e587eea362dcf2ca39 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 2 Nov 2017 17:42:40 +0000 Subject: [PATCH 4/4] Remove test checking don't specalise unspecalised generic types Previously this test verified that a a List reference wouldn't cause us to create a specalisation of List with generic type paramter T. Given that we now don't specalise any types except manually, this test doesn't make sense. --- .../generate_java_generic_type.cpp | 21 ------------------- 1 file changed, 21 deletions(-) diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index 3455f341ed9..40ada0c6cf7 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -126,27 +126,6 @@ SCENARIO( } } - -SCENARIO( - "generate_java_generic_type_from_file_uninstantiated_param", - "[core][java_bytecode][generate_java_generic_type]") -{ - GIVEN("A generic java type with a field that refers to another generic with" - " an uninstantiated parameter.") - { - symbol_tablet new_symbol_table= - load_java_class("generic_unknown_field", - "./java_bytecode/generate_concrete_generic_type"); - - // It's illegal to create an instantiation of a field that refers - // to a (still) uninstantiated generic class, so this is checking that - // this hasn't happened. - REQUIRE_FALSE(new_symbol_table.has_symbol - ("java::generic_unknown_field$element")); - } -} - - SCENARIO( "generate_java_generic_type_from_file_two_instances", "[core][java_bytecode][generate_java_generic_type]")