diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index ea46c4e1250..b9371e734f1 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -3,7 +3,6 @@ SRC = bytecode_info.cpp \ ci_lazy_methods.cpp \ ci_lazy_methods_needed.cpp \ expr2java.cpp \ - generic_arguments_name_builder.cpp \ generic_parameter_specialization_map_keys.cpp \ jar_file.cpp \ java_bytecode_convert_class.cpp \ @@ -30,7 +29,6 @@ SRC = bytecode_info.cpp \ java_string_literals.cpp \ java_types.cpp \ java_utils.cpp \ - generate_java_generic_type.cpp \ mz_zip_archive.cpp \ select_pointer_type.cpp \ # Empty last line diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp deleted file mode 100644 index 70764e20e97..00000000000 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ /dev/null @@ -1,343 +0,0 @@ -/*******************************************************************\ - - Module: Generate Java Generic Type - Instantiate a generic class with - concrete type information. - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include - -#include "generate_java_generic_type.h" -#include "generic_arguments_name_builder.h" -#include -#include -#include - -generate_java_generic_typet::generate_java_generic_typet( - message_handlert &message_handler): - message_handler(message_handler) -{} - -/// Small auxiliary function, to print a single generic argument name. -/// \param argument argument type -/// \return printed name of the argument -static std::string argument_name_printer(const reference_typet &argument) -{ - const irep_idt &id(id2string(argument.subtype().get(ID_identifier))); - if(is_java_array_tag(id)) - { - std::string name = pretty_print_java_type(id2string(id)); - const typet &element_type = - java_array_element_type(to_symbol_type(argument.subtype())); - - // If this is an array of references then we will specialize its - // identifier using the type of the objects in the array. Else, there - // can be a problem with the same symbols for different instantiations - // using arrays with different types. - if(element_type.id() == ID_pointer) - { - const symbol_typet element_symbol = - to_symbol_type(element_type.subtype()); - name.append("of_" + id2string(element_symbol.get_identifier())); - } - return name; - } - else - { - return id2string(id); - } -} - -/// Generate a concrete instantiation of a generic type. -/// \param existing_generic_type The type to be concretised -/// \param symbol_table The symbol table that the concrete type will be -/// inserted into. -/// \return The symbol as it was retrieved from the symbol table after -/// it has been inserted into. -symbolt generate_java_generic_typet::operator()( - const java_generic_typet &existing_generic_type, - symbol_tablet &symbol_table) const -{ - namespacet ns(symbol_table); - - const typet &pointer_subtype=ns.follow(existing_generic_type.subtype()); - - INVARIANT( - pointer_subtype.id()==ID_struct, "Only pointers to classes in java"); - INVARIANT( - is_java_generic_class_type(pointer_subtype) || - is_java_implicitly_generic_class_type(pointer_subtype), - "Generic references type must be a generic class"); - - const java_class_typet &class_definition = - to_java_class_type(pointer_subtype); - - const std::string generic_name = build_generic_name( - existing_generic_type, class_definition, argument_name_printer); - struct_union_typet::componentst replacement_components = - class_definition.components(); - - // Small auxiliary function, to perform the inplace - // modification of the generic fields. - auto replace_type_for_generic_field = - [&](struct_union_typet::componentt &component) { - - component.type() = substitute_type( - component.type(), class_definition, existing_generic_type); - - return component; - }; - - std::size_t pre_modification_size=to_java_class_type( - ns.follow(existing_generic_type.subtype())).components().size(); - - std::for_each( - replacement_components.begin(), - replacement_components.end(), - replace_type_for_generic_field); - - std::size_t after_modification_size = class_definition.components().size(); - - INVARIANT( - pre_modification_size==after_modification_size, - "All components in the original class should be in the new class"); - - const java_specialized_generic_class_typet new_java_class{ - generic_name, - class_definition, - replacement_components, - existing_generic_type.generic_type_arguments()}; - - const type_symbolt &class_symbol = - build_symbol_from_specialised_class(new_java_class); - - std::pair res = symbol_table.insert(std::move(class_symbol)); - if(!res.second) - { - messaget message(message_handler); - message.warning() << "stub class symbol " << class_symbol.name - << " already exists" << messaget::eom; - } - - const auto expected_symbol="java::"+id2string(generic_name); - auto symbol=symbol_table.lookup(expected_symbol); - INVARIANT(symbol, "New class not created"); - return *symbol; -} - -/// For a given type, if the type contains a Java generic parameter, we look -/// that parameter up and return the relevant type. This works recursively on -/// arrays so that T [] is converted to RelevantType []. -/// \param parameter_type: The type under consideration -/// \param generic_class: The generic class that the \p parameter_type -/// belongs to (e.g. the type of a component of the class). This is used to -/// look up the mapping from name of generic parameter to its index. -/// \param generic_reference: The instantiated version of the generic class -/// used to look up the instantiated type. This is expected to be fully -/// instantiated. -/// \return A newly constructed type with generic parameters replaced, or if -/// there are none to replace, the original type. -typet generate_java_generic_typet::substitute_type( - const typet ¶meter_type, - const java_class_typet &class_definition, - const java_generic_typet &generic_reference) const -{ - if(is_java_generic_parameter(parameter_type)) - { - auto component_identifier = to_java_generic_parameter(parameter_type) - .type_variable() - .get_identifier(); - - // see if it is a generic parameter introduced by this class - optionalt results; - if(is_java_generic_class_type(class_definition)) - { - const java_generic_class_typet &generic_class = - to_java_generic_class_type(class_definition); - - results = java_generics_get_index_for_subtype( - generic_class.generic_types(), component_identifier); - } - // see if it is an implicit generic parameter introduced by an outer class - if(!results.has_value()) - { - INVARIANT( - is_java_implicitly_generic_class_type(class_definition), - "The parameter must either be a generic type or implicit generic type"); - const java_implicitly_generic_class_typet &implicitly_generic_class = - to_java_implicitly_generic_class_type(class_definition); - results = java_generics_get_index_for_subtype( - implicitly_generic_class.implicit_generic_types(), - component_identifier); - } - - INVARIANT(results.has_value(), "generic component type not found"); - return generic_reference.generic_type_arguments()[*results]; - } - else if(parameter_type.id() == ID_pointer) - { - if(is_java_generic_type(parameter_type)) - { - const java_generic_typet &generic_type = - to_java_generic_type(parameter_type); - - java_generic_typet::generic_type_argumentst replaced_type_variables; - - // Swap each parameter - std::transform( - generic_type.generic_type_arguments().begin(), - generic_type.generic_type_arguments().end(), - std::back_inserter(replaced_type_variables), - [&](const reference_typet &generic_param) -> reference_typet - { - const typet &replacement_type = - substitute_type(generic_param, class_definition, generic_reference); - - // This code will be simplified when references aren't considered to - // be generic parameters - if(is_java_generic_parameter(replacement_type)) - { - return to_java_generic_parameter(replacement_type); - } - else - { - INVARIANT( - is_reference(replacement_type), - "All generic parameters should be references"); - return to_reference_type(replacement_type); - } - }); - - java_generic_typet new_type = generic_type; - new_type.generic_type_arguments() = replaced_type_variables; - return new_type; - } - else if(parameter_type.subtype().id() == ID_symbol) - { - const symbol_typet &array_subtype = - to_symbol_type(parameter_type.subtype()); - if(is_java_array_tag(array_subtype.get_identifier())) - { - const typet &array_element_type = - java_array_element_type(array_subtype); - - const typet &new_array_type = substitute_type( - array_element_type, class_definition, generic_reference); - - typet replacement_array_type = java_array_type('a'); - replacement_array_type.subtype().set(ID_C_element_type, new_array_type); - return replacement_array_type; - } - } - } - return parameter_type; -} - -/// Build a unique name for the generic to be instantiated. -/// Example: if \p existing_generic_type is a pointer to `Outer.Inner` -/// (\p original_class) with parameter `T` being specialized with argument -/// `Integer`, then the function returns a string `Outer<\p -/// argument_name_printer(Integer)>$Inner`. -/// \param existing_generic_type The type we want to concretise -/// \param original_class The original class type for \p existing_generic_type -/// \param argument_name_printer A custom function to print names of individual -/// arguments (such as `Integer`, `Integer[]` for concise names or `java::java -/// .lang.Integer`, `array[reference]of_java::java.lang.Integer`) -/// \return A name for the new specialized generic class we want a unique name -/// for. -std::string generate_java_generic_typet::build_generic_name( - const java_generic_typet &existing_generic_type, - const java_class_typet &original_class, - const generic_arguments_name_buildert::name_printert &argument_name_printer) - const -{ - std::ostringstream generic_name_buffer; - const std::string &original_class_name = original_class.get_tag().c_str(); - - // gather together all implicit generic types and generic types - std::vector generic_types; - if(is_java_implicitly_generic_class_type(original_class)) - { - const java_implicitly_generic_class_typet - &implicitly_generic_original_class = - to_java_implicitly_generic_class_type(original_class); - generic_types.insert( - generic_types.end(), - implicitly_generic_original_class.implicit_generic_types().begin(), - implicitly_generic_original_class.implicit_generic_types().end()); - } - if(is_java_generic_class_type(original_class)) - { - const java_generic_class_typet &generic_original_class = - to_java_generic_class_type(original_class); - generic_types.insert( - generic_types.end(), - generic_original_class.generic_types().begin(), - generic_original_class.generic_types().end()); - } - - INVARIANT( - generic_types.size() == - existing_generic_type.generic_type_arguments().size(), - "All generic types must be concretized"); - - auto generic_type_p = generic_types.begin(); - std::string previous_class_name; - std::string current_class_name; - generic_arguments_name_buildert build_generic_arguments( - argument_name_printer); - - // add generic arguments to each generic (outer) class - for(const auto &generic_argument : - existing_generic_type.generic_type_arguments()) - { - previous_class_name = current_class_name; - current_class_name = generic_type_p->get_parameter_class_name(); - - // if the class names do not match, it means that the next generic - // (outer) class is being handled - if(current_class_name != previous_class_name) - { - // add the arguments of the previous generic class to the buffer - // and reset the builder - generic_name_buffer << build_generic_arguments.finalize(); - - INVARIANT( - has_prefix(current_class_name, previous_class_name), - "Generic types are ordered from the outermost outer class inwards"); - - // add the remaining part of the current generic class name to the buffer - // example: if current_outer_class = A$B$C, previous_outer_class = A, - // then substr of current, starting at the length of previous is $B$C - generic_name_buffer << current_class_name.substr( - previous_class_name.length()); - } - - // add an argument to the current generic class - build_generic_arguments.add_argument(generic_argument); - ++generic_type_p; - } - generic_name_buffer << build_generic_arguments.finalize(); - - // add the remaining part of the original class name to the buffer - generic_name_buffer << original_class_name.substr( - current_class_name.length()); - - return generic_name_buffer.str(); -} - -/// Construct the symbol to be moved into the symbol table -/// \param specialised_class: The newly constructed specialised class -/// \return The symbol to add to the symbol table -type_symbolt generate_java_generic_typet::build_symbol_from_specialised_class( - const java_class_typet &specialised_class) const -{ - type_symbolt new_symbol(specialised_class); - new_symbol.base_name = specialised_class.get(ID_base_name); - new_symbol.pretty_name = specialised_class.get(ID_base_name); - new_symbol.name = specialised_class.get(ID_name); - new_symbol.mode = ID_java; - return new_symbol; -} diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h deleted file mode 100644 index c0c7113f691..00000000000 --- a/src/java_bytecode/generate_java_generic_type.h +++ /dev/null @@ -1,45 +0,0 @@ -/*******************************************************************\ - - Module: Generate Java Generic Type - Instantiate a generic class with - concrete type information. - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ -#ifndef CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H -#define CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H - -#include -#include -#include -#include -#include -#include "generic_arguments_name_builder.h" - -class generate_java_generic_typet -{ -public: - explicit generate_java_generic_typet(message_handlert &message_handler); - - symbolt operator()( - const java_generic_typet &existing_generic_type, - symbol_tablet &symbol_table) const; -private: - std::string build_generic_name( - const java_generic_typet &existing_generic_type, - const java_class_typet &original_class, - const generic_arguments_name_buildert::name_printert &argument_name_printer) - const; - - typet substitute_type( - const typet ¶meter_type, - const java_class_typet &replacement_type, - const java_generic_typet &generic_reference) const; - - type_symbolt build_symbol_from_specialised_class( - const java_class_typet &specialised_class) const; - - message_handlert &message_handler; -}; - -#endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H diff --git a/src/java_bytecode/generic_arguments_name_builder.cpp b/src/java_bytecode/generic_arguments_name_builder.cpp deleted file mode 100644 index a1ff2c5a497..00000000000 --- a/src/java_bytecode/generic_arguments_name_builder.cpp +++ /dev/null @@ -1,42 +0,0 @@ -/*******************************************************************\ - - Module: Generic Arguments Name Builder - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -/// file - A class to aid in building the name of specialized generic classes. -/// Allows for custom builder function for a single argument name. - -#include -#include "generic_arguments_name_builder.h" -#include "java_utils.h" - -std::string generic_arguments_name_buildert::finalize() -{ - std::ostringstream name_buffer; - - if(!type_arguments.empty()) - { - bool first = true; - for(const auto &argument : type_arguments) - { - if(first) - { - name_buffer << "<"; - first = false; - } - else - { - name_buffer << ", "; - } - - name_buffer << argument_name_printer(argument); - } - name_buffer << ">"; - type_arguments.clear(); - } - - return name_buffer.str(); -} diff --git a/src/java_bytecode/generic_arguments_name_builder.h b/src/java_bytecode/generic_arguments_name_builder.h deleted file mode 100644 index b27b6b1b117..00000000000 --- a/src/java_bytecode/generic_arguments_name_builder.h +++ /dev/null @@ -1,43 +0,0 @@ -/*******************************************************************\ - - Module: Generic Arguments Name Builder - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -/// file - A class to aid in building the name of specialized generic classes. -/// Allows for custom builder function for a single argument name. - -#ifndef CPROVER_JAVA_BYTECODE_GENERIC_ARGUMENTS_NAME_BUILDER_H -#define CPROVER_JAVA_BYTECODE_GENERIC_ARGUMENTS_NAME_BUILDER_H - -#include "java_types.h" -#include - -class generic_arguments_name_buildert -{ -public: - typedef std::function - name_printert; - - explicit generic_arguments_name_buildert( - const name_printert &argument_name_printer) - : argument_name_printer(argument_name_printer) - { - } - - void add_argument(const reference_typet &argument) - { - PRECONDITION(!is_java_generic_parameter(argument)); - type_arguments.push_back(argument); - } - - std::string finalize(); - -private: - std::vector type_arguments; - name_printert argument_name_printer; -}; - -#endif // CPROVER_JAVA_BYTECODE_GENERIC_ARGUMENTS_NAME_BUILDER_H diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index b10c7b93796..bf226bb38f4 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -34,7 +34,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_static_initializers.h" #include "java_utils.h" #include -#include #include "expr2java.h" diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 775cada45a2..59a2e0e146d 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -127,16 +127,6 @@ class java_generic_parametert:public reference_typet return type_variable().get_identifier(); } - const std::string get_parameter_class_name() const - { - const std::string ¶meter_name = get_name().c_str(); - PRECONDITION(has_prefix(parameter_name, "java::")); - int prefix_length = std::string("java::").length(); - const std::string name = parameter_name.substr( - prefix_length, parameter_name.rfind("::") - prefix_length); - return name; - } - private: typedef std::vector type_variablest; const type_variablest &type_variables() const @@ -457,77 +447,6 @@ void get_dependencies_from_generic_parameters( const typet &, std::set &); -class java_specialized_generic_class_typet : public java_class_typet -{ -public: - typedef std::vector generic_type_argumentst; - - /// Build the specialised version of the specific class, with the specified - /// parameters and name. - /// \param generic_name: The new name for the class - /// (like Generic) - /// \param originating_class: The name for the original class (like - /// java::Generic) - /// \param new_components: The specialised components - /// \return The newly constructed class. - java_specialized_generic_class_typet( - const irep_idt &generic_name, - const java_class_typet &originating_class, - const struct_typet::componentst &new_components, - const generic_type_argumentst &specialised_parameters) - { - set(ID_C_specialized_generic_java_class, true); - set(ID_name, "java::" + id2string(generic_name)); - set(ID_base_name, id2string(generic_name)); - components() = new_components; - set_tag(originating_class.get_tag()); - set_access(originating_class.get_access()); - - generic_type_arguments() = specialised_parameters; - } - - /// \return vector of type variables - const generic_type_argumentst &generic_type_arguments() const - { - return (const generic_type_argumentst &)(find(ID_type_variables).get_sub()); - } - -private: - /// \return vector of type variables - generic_type_argumentst &generic_type_arguments() - { - return (generic_type_argumentst &)(add(ID_type_variables).get_sub()); - } -}; - -inline bool is_java_specialized_generic_class_type(const typet &type) -{ - return type.get_bool(ID_C_specialized_generic_java_class); -} - -inline bool is_java_specialized_generic_class_type(typet &type) -{ - return type.get_bool(ID_C_specialized_generic_java_class); -} - -inline java_specialized_generic_class_typet -to_java_specialized_generic_class_type(const typet &type) -{ - INVARIANT( - is_java_specialized_generic_class_type(type), - "Tried to convert a type that was not a specialised generic java class"); - return static_cast(type); -} - -inline java_specialized_generic_class_typet -to_java_specialized_generic_class_type(typet &type) -{ - INVARIANT( - is_java_specialized_generic_class_type(type), - "Tried to convert a type that was not a specialised generic java class"); - return static_cast(type); -} - /// Type for a generic symbol, extends symbol_typet with a /// vector of java generic types. /// This is used to store the type of generic superclasses and interfaces. 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 deleted file mode 100644 index 8155bdf3ef7..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ /dev/null @@ -1,373 +0,0 @@ -/*******************************************************************\ - - Module: Unit tests for generating new type with generic parameters - substitued for concrete types - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include -#include -#include -#include - -#include -#include - -SCENARIO( - "generate_java_generic_type_from_file", - "[core][java_bytecode][generate_java_generic_type]") -{ - auto expected_symbol = - "java::generic_two_fields$bound_element"; - - GIVEN("A generic java type with two generic fields and a concrete " - "substitution") - { - symbol_tablet new_symbol_table= - load_java_class("generic_two_fields", - "./java_bytecode/generate_concrete_generic_type"); - - generic_utils::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.") - { - const auto &class_symbol = new_symbol_table.lookup( - "java::generic_two_fields$bound_element"); - const typet &symbol_type=class_symbol->type; - - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); - REQUIRE(class_type.is_class()); - - REQUIRE(class_type.has_component("first")); - const auto &first_component=class_type.get_component("first"); - REQUIRE(!is_java_generic_parameter(first_component.type())); - REQUIRE(first_component.type().id()==ID_pointer); - REQUIRE(first_component.type().subtype().id()==ID_symbol); - REQUIRE(to_symbol_type( - first_component.type().subtype()).get_identifier()== - "java::java.lang.Integer"); - REQUIRE(class_type.has_component("second")); - const auto &second_component=class_type.get_component("second"); - REQUIRE(!is_java_generic_parameter(second_component.type())); - REQUIRE(second_component.type().id()==ID_pointer); - REQUIRE(second_component.type().subtype().id()==ID_symbol); - REQUIRE(to_symbol_type( - second_component.type().subtype()).get_identifier()== - "java::java.lang.Integer"); - } - } -} - - -SCENARIO( - "generate_java_generic_type_from_file_two_params", - "[core][java_bytecode][generate_java_generic_type]") -{ - auto expected_symbol = - "java::generic_two_parameters$KeyValuePair"; - - GIVEN("A generic java type with two generic parameters, like a Hashtable") - { - symbol_tablet new_symbol_table= - load_java_class("generic_two_parameters", - "./java_bytecode/generate_concrete_generic_type"); - - generic_utils::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 " - "the generic components.") - { - const auto &class_symbol=new_symbol_table.lookup( - expected_symbol); - const typet &symbol_type=class_symbol->type; - - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); - REQUIRE(class_type.is_class()); - - REQUIRE(class_type.has_component("key")); - const auto &first_component=class_type.get_component("key"); - REQUIRE(!is_java_generic_parameter(first_component.type())); - REQUIRE(class_type.has_component("value")); - const auto &second_component=class_type.get_component("value"); - REQUIRE(!is_java_generic_parameter(second_component.type())); - } - } -} - -SCENARIO( - "generate_java_generic_type_from_file_two_instances", - "[core][java_bytecode][generate_java_generic_type]") -{ - // After we have loaded the class and converted the generics, - // the presence of these two symbols in the symbol table is - // proof enough that we did the work we needed to do correctly. - auto first_expected_symbol = - "java::generic_two_instances$element"; - auto second_expected_symbol = - "java::generic_two_instances$element"; - - 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_two_instances", - "./java_bytecode/generate_concrete_generic_type"); - - generic_utils::specialise_generic_from_component( - "java::generic_two_instances", "bool_element", new_symbol_table); - generic_utils::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); - const struct_union_typet::componentt &component = - require_type::require_component( - to_struct_type(first_symbol->type), "elem"); - auto first_symbol_type=component.type(); - require_type::require_pointer( - first_symbol_type, symbol_typet("java::java.lang.Boolean")); - - REQUIRE(new_symbol_table.has_symbol(second_expected_symbol)); - auto second_symbol=new_symbol_table.lookup(second_expected_symbol); - REQUIRE(second_symbol->type.id()==ID_struct); - const struct_union_typet::componentt &second_component = - require_type::require_component( - to_struct_type(second_symbol->type), "elem"); - auto second_symbol_type=second_component.type(); - require_type::require_pointer( - second_symbol_type, symbol_typet("java::java.lang.Integer")); - } -} - -SCENARIO( - "generate_java_generic_type_with_array_concrete_type", - "[core][java_bytecode][generate_java_generic_type]") -{ - // We have a 'harness' class who's only purpose is to contain a reference - // to the generic class so that we can test the specialization of that generic - // class - const irep_idt harness_class = "java::generic_field_array_instantiation"; - - // We want to test that the specialized/instantiated class has it's field - // type updated, so find the specialized class, not the generic class. - const irep_idt test_class = - "java::generic_field_array_instantiation$generic"; - - GIVEN("A generic type instantiated with an array type") - { - symbol_tablet new_symbol_table = load_java_class( - "generic_field_array_instantiation", - "./java_bytecode/generate_concrete_generic_type"); - - // Ensure the class has been specialized - REQUIRE(new_symbol_table.has_symbol(harness_class)); - const symbolt &harness_symbol = new_symbol_table.lookup_ref(harness_class); - - const struct_typet::componentt &harness_component = - require_type::require_component(to_struct_type(harness_symbol.type), "f"); - - ui_message_handlert message_handler; - generate_java_generic_typet instantiate_generic_type(message_handler); - instantiate_generic_type( - to_java_generic_type(harness_component.type()), new_symbol_table); - - // Test the specialized class - REQUIRE(new_symbol_table.has_symbol(test_class)); - const symbolt test_class_symbol = new_symbol_table.lookup_ref(test_class); - - REQUIRE(test_class_symbol.type.id() == ID_struct); - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "gf"); - const typet &test_field_type = field_component.type(); - - REQUIRE(test_field_type.id() == ID_pointer); - REQUIRE(test_field_type.subtype().id() == ID_symbol); - const symbol_typet test_field_array = - to_symbol_type(test_field_type.subtype()); - REQUIRE(test_field_array.get_identifier() == "java::array[reference]"); - const pointer_typet &element_type = require_type::require_pointer( - java_array_element_type(test_field_array), - symbol_typet("java::java.lang.Float")); - - // check for other specialized classes, in particular different symbol ids - // for arrays with different element types - GIVEN("A generic type instantiated with different array types") - { - const irep_idt test_class_integer = - "java::generic_field_array_instantiation$generic"; - - const irep_idt test_class_int = - "java::generic_field_array_instantiation$generic"; - - const irep_idt test_class_float = - "java::generic_field_array_instantiation$generic"; - - const struct_typet::componentt &component_g = - require_type::require_component( - to_struct_type(harness_symbol.type), "g"); - instantiate_generic_type( - to_java_generic_type(component_g.type()), new_symbol_table); - REQUIRE(new_symbol_table.has_symbol(test_class_integer)); - - const struct_typet::componentt &component_h = - require_type::require_component( - to_struct_type(harness_symbol.type), "h"); - instantiate_generic_type( - to_java_generic_type(component_h.type()), new_symbol_table); - REQUIRE(new_symbol_table.has_symbol(test_class_int)); - - const struct_typet::componentt &component_i = - require_type::require_component( - to_struct_type(harness_symbol.type), "i"); - instantiate_generic_type( - to_java_generic_type(component_i.type()), new_symbol_table); - REQUIRE(new_symbol_table.has_symbol(test_class_float)); - } - } -} - -SCENARIO( - "generate_java_generic_type with a generic array field", - "[core][java_bytecode][generate_java_generic_type]") -{ - const irep_idt harness_class = "java::generic_field_array_instantiation"; - GIVEN("A generic class with a field of type T []") - { - symbol_tablet new_symbol_table = load_java_class( - "generic_field_array_instantiation", - "./java_bytecode/generate_concrete_generic_type"); - - const irep_idt inner_class = "genericArray"; - - WHEN("We specialise that class from a reference to it") - { - generic_utils::specialise_generic_from_component( - harness_class, "genericArrayField", new_symbol_table); - THEN( - "There should be a specialised version of the class in the symbol " - "table") - { - const irep_idt specialised_class_name = id2string(harness_class) + "$" + - id2string(inner_class) + - ""; - REQUIRE(new_symbol_table.has_symbol(specialised_class_name)); - - const symbolt test_class_symbol = - new_symbol_table.lookup_ref(specialised_class_name); - - REQUIRE(test_class_symbol.type.id() == ID_struct); - THEN("The array field should be specialised to be an array of floats") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "arrayField"); - - const pointer_typet &component_pointer_type = - require_type::require_pointer(field_component.type(), {}); - - const symbol_typet &pointer_subtype = require_type::require_symbol( - component_pointer_type.subtype(), "java::array[reference]"); - - const typet &array_type = java_array_element_type(pointer_subtype); - - require_type::require_pointer( - array_type, symbol_typet("java::java.lang.Float")); - } - - THEN( - "The generic class field should be specialised to be a generic " - "class with the appropriate type") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "genericClassField"); - - require_type::require_java_generic_type( - field_component.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Float"}}); - } - } - } - WHEN( - "We specialise the class with an array we should have appropriate types") - { - generic_utils::specialise_generic_from_component( - harness_class, "genericArrayArrayField", new_symbol_table); - THEN( - "There should be a specialised version of the class in the symbol " - "table") - { - const std::string specialised_string = - ""; - const irep_idt specialised_class_name = id2string(harness_class) + "$" + - id2string(inner_class) + - specialised_string; - - REQUIRE(new_symbol_table.has_symbol(specialised_class_name)); - - const symbolt test_class_symbol = - new_symbol_table.lookup_ref(specialised_class_name); - - REQUIRE(test_class_symbol.type.id() == ID_struct); - THEN("The array field should be specialised to be an array of floats") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "arrayField"); - - const pointer_typet &component_pointer_type = - require_type::require_pointer(field_component.type(), {}); - - const symbol_typet &pointer_subtype = require_type::require_symbol( - component_pointer_type.subtype(), "java::array[reference]"); - - const typet &array_type = java_array_element_type(pointer_subtype); - - require_type::require_pointer( - array_type, symbol_typet("java::array[reference]")); - - const typet &array_subtype = - java_array_element_type(to_symbol_type(array_type.subtype())); - - require_type::require_pointer( - array_subtype, symbol_typet("java::java.lang.Float")); - } - - THEN( - "The generic class field should be specialised to be a generic " - "class with the appropriate type") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "genericClassField"); - - const java_generic_typet ¶m_type = - require_type::require_java_generic_type( - field_component.type(), - {{require_type::type_argument_kindt::Inst, - "java::array[reference]"}}); - - const typet &array_type = java_array_element_type( - to_symbol_type(param_type.generic_type_arguments()[0].subtype())); - require_type::require_pointer( - array_type, symbol_typet("java::java.lang.Float")); - } - } - } - } -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp deleted file mode 100644 index d6c8b271d38..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp +++ /dev/null @@ -1,598 +0,0 @@ -/*******************************************************************\ - - Module: Unit tests for generating new type with generic parameters - substitued for concrete types - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include -#include -#include -#include - -SCENARIO("generate_outer_inner", "[core][java_bytecode][generate_outer_inner]") -{ - WHEN("Loading a class with generic and non-generic inner classes") - { - symbol_tablet new_symbol_table = load_java_class( - "generic_outer_inner", "./java_bytecode/generate_concrete_generic_type"); - const std::string &class_prefix = "java::generic_outer_inner"; - - WHEN("Its field t1 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t1", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter"; - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), - symbol_typet("java::generic_outer_inner$GenericOuter$Inner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}}); - } - - THEN("It has field f3 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f3"); - require_type::require_pointer( - field.type(), - symbol_typet( - "java::generic_outer_inner$GenericOuter$GenericInner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}, - {require_type::type_argument_kindt::Inst, - "java::java.lang.String"}}); - } - - THEN("It has field this$0 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$0"); - require_type::require_pointer( - field.type(), symbol_typet("java::generic_outer_inner")); - } - } - } - - WHEN("Its field t2 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t2", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter$Inner"; - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t2a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t2a", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$GenericOuter$Inner"; - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t3 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t3", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter$Inner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t3a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t3a", new_symbol_table); - const std::string &expected_prefix = class_prefix + - "$GenericOuter$Inner$" - "InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - // TODO add test for field t4 once TG-1633 is done - - WHEN("Its field t5 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t5", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$Inner$GenericInnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix + "$Outer$Inner")); - } - } - } - - WHEN("Its field t6 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t6", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$Outer$GenericInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), - symbol_typet( - "java::generic_outer_inner$Outer$" - "GenericInner$GenericInnerInner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}, - {require_type::type_argument_kindt::Inst, - "java::java.lang.String"}}); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix + "$Outer")); - } - } - } - - WHEN("Its field t7 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t7", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$GenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t7a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t7a", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$GenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - // TODO add test for field t8 once TG-1633 is done - - WHEN("Its field t9 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t9", new_symbol_table); - const std::string &expected_prefix = class_prefix + - "$Outer$TwoParamGenericInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix + "$Outer")); - } - } - } - - WHEN("Its field t10 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t10", new_symbol_table); - const std::string &expected_prefix = class_prefix + - "$Outer$TwoParamGenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t10a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t10a", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$TwoParamGenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t11 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t11", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::generic_outer_inner$Outer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), - symbol_typet("java::generic_outer_inner$GenericOuter$Inner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::generic_outer_inner$Outer"}}); - } - - THEN("It has field f3 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f3"); - require_type::require_pointer( - field.type(), - symbol_typet( - "java::generic_outer_inner$GenericOuter$GenericInner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::generic_outer_inner$Outer"}, - {require_type::type_argument_kindt::Inst, - "java::java.lang.String"}}); - } - - THEN("It has field this$0 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$0"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix)); - } - } - } - } -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class deleted file mode 100644 index 694991b2962..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class deleted file mode 100644 index 184f8383980..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class deleted file mode 100644 index 45f98be34c7..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java deleted file mode 100644 index c24758d2ef0..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java +++ /dev/null @@ -1,21 +0,0 @@ -public class generic_field_array_instantiation { - - class generic { - T gf; - } - - class genericArray { - T [] arrayField; - - generic genericClassField; - } - - generic f; - generic g; - generic h; - generic i; - Float [] af; - - genericArray genericArrayField; - genericArray genericArrayArrayField; -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$GenericInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$GenericInner.class deleted file mode 100644 index 1d9fe54995c..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$GenericInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner$InnerInner.class deleted file mode 100644 index 8f6d49bec1f..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner$InnerInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner.class deleted file mode 100644 index bc9fa9be685..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter.class deleted file mode 100644 index be62d73f664..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$GenericInnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$GenericInnerInner.class deleted file mode 100644 index be2037c6c88..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$GenericInnerInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$InnerInner.class deleted file mode 100644 index 36972ebe360..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$InnerInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner.class deleted file mode 100644 index 2368c6b18ab..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$GenericInnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$GenericInnerInner.class deleted file mode 100644 index af00787fbf9..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$GenericInnerInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$InnerInner.class deleted file mode 100644 index d481c3322f3..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$InnerInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner.class deleted file mode 100644 index 7495bb55358..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner$InnerInner.class deleted file mode 100644 index d7e166e8c9a..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner$InnerInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner.class deleted file mode 100644 index 8ce274e530c..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer.class deleted file mode 100644 index 508f964ddf8..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.class deleted file mode 100644 index acf46950e1e..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.java b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.java deleted file mode 100644 index 7de5a6bea30..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.java +++ /dev/null @@ -1,82 +0,0 @@ -public class generic_outer_inner -{ - class GenericOuter - { - class Inner { - T f1; - Integer f2; - - class InnerInner { - T f1; - } - } - - class GenericInner - { - - } - - T f1; - Inner f2; - GenericInner f3; - } - - class Outer - { - class Inner - { - class GenericInnerInner - { - T f1; - } - } - - class GenericInner - { - class InnerInner - { - T f1; - } - - class GenericInnerInner - { - T f1; - U f2; - } - - GenericInnerInner f1; - } - - class TwoParamGenericInner - { - class InnerInner - { - U f1; - V f2; - } - - U f1; - V f2; - } - } - - GenericOuter t1; - GenericOuter.Inner t2; - GenericOuter.Inner t2a; - GenericOuter.Inner.InnerInner t3; - GenericOuter.Inner.InnerInner t3a; - GenericOuter.GenericInner t4; - - Outer.Inner.GenericInnerInner t5; - Outer.GenericInner t6; - Outer.GenericInner.InnerInner t7; - Outer.GenericInner.InnerInner t7a; - Outer.GenericInner.GenericInnerInner t8; - - Outer.TwoParamGenericInner t9; - Outer.TwoParamGenericInner.InnerInner t10; - Outer.TwoParamGenericInner.InnerInner t10a; - - GenericOuter t11; -} - diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields$bound_element.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields$bound_element.class deleted file mode 100644 index 0e61e55d0de..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields$bound_element.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.class deleted file mode 100644 index 5d14a465aaf..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.java b/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.java deleted file mode 100644 index e8e6dc80d9e..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.java +++ /dev/null @@ -1,11 +0,0 @@ -public class generic_two_fields { - - // For this to work we need to compile with -g, otherwise the symbols we are looking for - // are entering the symbol table as anonlocal::1 and anonlocal::2 and nothing works. - class bound_element { - NUM first; - NUM second; - } - - bound_element belem; -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances$element.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances$element.class deleted file mode 100644 index 3229b26a832..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances$element.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.class deleted file mode 100644 index 61d336211cd..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java b/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java deleted file mode 100644 index 48144b5ecaf..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java +++ /dev/null @@ -1,8 +0,0 @@ -class generic_two_instances { - class element { - T elem; - } - - element bool_element; - element int_element; -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters$KeyValuePair.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters$KeyValuePair.class deleted file mode 100644 index 8c4e5674b68..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters$KeyValuePair.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.class deleted file mode 100644 index 2527db38675..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java b/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java deleted file mode 100644 index 0f5bed55482..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java +++ /dev/null @@ -1,22 +0,0 @@ -class generic_two_parameters { - class KeyValuePair { - K key; - V value; - } - - KeyValuePair bomb; - - public String func() { - KeyValuePair e = new KeyValuePair(); - e.key = "Hello"; - e.value = 5; - if (e.value >= 4) - { - return e.key; - } - else - { - return "Oops"; - } - } -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$G.class b/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$G.class deleted file mode 100644 index 39888ab1dbc..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$G.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$element.class b/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$element.class deleted file mode 100644 index 39b647093cb..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$element.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.class b/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.class deleted file mode 100644 index 73db45376b9..00000000000 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.class and /dev/null differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.java b/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.java deleted file mode 100644 index 3b918d9664f..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.java +++ /dev/null @@ -1,9 +0,0 @@ -class generic_unknown_field { - class G { - element ref; - } - - class element { - T elem; - } -} diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 73f1331d5de..45ccd69ec7b 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,6 +1,5 @@ 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 deleted file mode 100644 index caa3f8db341..00000000000 --- a/unit/testing-utils/generic_utils.cpp +++ /dev/null @@ -1,62 +0,0 @@ -/*******************************************************************\ - - Module: Unit test utilities - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include -#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::none_of( - example_type.generic_type_arguments().begin(), - example_type.generic_type_arguments().end(), - is_java_generic_parameter)); - - namespacet ns(new_symbol_table); - const typet &class_type = ns.follow(example_type.subtype()); - REQUIRE( - (is_java_generic_class_type(class_type) || - is_java_implicitly_generic_class_type(class_type))); - - // 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); -} - -/// Helper function to specialise 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 generic_utils::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); -} diff --git a/unit/testing-utils/generic_utils.h b/unit/testing-utils/generic_utils.h deleted file mode 100644 index e0d36d7beb7..00000000000 --- a/unit/testing-utils/generic_utils.h +++ /dev/null @@ -1,31 +0,0 @@ -/*******************************************************************\ - - 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); - -void specialise_generic_from_component( - const irep_idt &class_name, - const irep_idt &component_name, - symbol_tablet &new_symbol_table); -} - -#endif // CPROVER_TESTING_UTILS_GENERIC_UTILS_H