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 8076c290e12..00000000000 Binary files a/regression/cbmc-java/generics_symtab1/generics$bound_element.class and /dev/null differ 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 34cb36e36b4..00000000000 Binary files a/regression/cbmc-java/generics_symtab1/generics$element.class and /dev/null differ diff --git a/regression/cbmc-java/generics_symtab1/generics.class b/regression/cbmc-java/generics_symtab1/generics.class deleted file mode 100644 index 4fde1b4d6c4..00000000000 Binary files a/regression/cbmc-java/generics_symtab1/generics.class and /dev/null differ 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; \}$ --- 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( 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..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 @@ -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 " @@ -100,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]") @@ -140,6 +145,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