diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index a868fdd5c90..b9371e734f1 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -3,7 +3,7 @@ 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 \ java_bytecode_convert_method.cpp \ @@ -29,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/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 965d117ddea..5dcfd87a9a9 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -322,8 +322,10 @@ void ci_lazy_methodst::initialize_all_needed_classes_from_pointer( { initialize_needed_classes_from_pointer(pointer_type, ns, needed_lazy_methods); - const pointer_typet &subbed_pointer_type= - pointer_type_selector.convert_pointer_type(pointer_type, ns); + // TODO we should be passing here a map that maps generic parameters + // to concrete types in the current context TG-2664 + const pointer_typet &subbed_pointer_type = + pointer_type_selector.convert_pointer_type(pointer_type, {}, ns); if(subbed_pointer_type!=pointer_type) { 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/generic_parameter_specialization_map_keys.cpp b/src/java_bytecode/generic_parameter_specialization_map_keys.cpp new file mode 100644 index 00000000000..1c6da2d43dc --- /dev/null +++ b/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -0,0 +1,155 @@ +/// Author: DiffBlue Limited. All Rights Reserved. + +#include "generic_parameter_specialization_map_keys.h" + +/// \param type Source type +/// \return The vector of implicitly generic and (explicitly) generic type +/// parameters of the given type. +const std::vector +get_all_generic_parameters(const typet &type) +{ + PRECONDITION( + is_java_generic_class_type(type) || + is_java_implicitly_generic_class_type(type)); + std::vector generic_parameters; + if(is_java_implicitly_generic_class_type(type)) + { + const java_implicitly_generic_class_typet &implicitly_generic_class = + to_java_implicitly_generic_class_type(to_java_class_type(type)); + generic_parameters.insert( + generic_parameters.end(), + implicitly_generic_class.implicit_generic_types().begin(), + implicitly_generic_class.implicit_generic_types().end()); + } + if(is_java_generic_class_type(type)) + { + const java_generic_class_typet &generic_class = + to_java_generic_class_type(to_java_class_type(type)); + generic_parameters.insert( + generic_parameters.end(), + generic_class.generic_types().begin(), + generic_class.generic_types().end()); + } + return generic_parameters; +} + +/// Add pairs to the controlled map. Own the keys and pop from their stack +/// on destruction; otherwise do nothing. +/// \param parameters generic parameters that are the keys of the pairs to add +/// \param types a type to add for each parameter +const void generic_parameter_specialization_map_keyst::insert_pairs( + const std::vector ¶meters, + const std::vector &types) +{ + INVARIANT(erase_keys.empty(), "insert_pairs should only be called once"); + PRECONDITION(parameters.size() == types.size()); + + // Pair up the parameters and types for easier manipulation later + std::vector> pairs; + pairs.reserve(parameters.size()); + std::transform( + parameters.begin(), + parameters.end(), + types.begin(), + std::back_inserter(pairs), + [&](java_generic_parametert param, reference_typet type) + { + return std::make_pair(param, type); + }); + + for(const auto &pair : pairs) + { + // Only add the pair if the type is not the parameter itself, e.g., + // pair.first = pair.second = java::A::T. This can happen for example + // when initiating a pointer to an implicitly java generic class type + // in gen_nondet_init and would result in a loop when the map is used + // to look up the type of the parameter. + if( + !(is_java_generic_parameter(pair.second) && + to_java_generic_parameter(pair.second).get_name() == + pair.first.get_name())) + { + const irep_idt &key = pair.first.get_name(); + if(generic_parameter_specialization_map.count(key) == 0) + generic_parameter_specialization_map.emplace( + key, std::stack()); + (*generic_parameter_specialization_map.find(key)) + .second.push(pair.second); + + // We added something, so pop it when this is destroyed: + erase_keys.push_back(key); + } + } +} + +/// Add a pair of a parameter and its types for each generic parameter of the +/// given generic pointer type to the controlled map. Own the keys and pop +/// from their stack on destruction; otherwise do nothing. +/// \param pointer_type pointer type to get the specialized generic types from +/// \param pointer_subtype_struct struct type to which the generic pointer +/// points, must be generic if the pointer is generic +const void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( + const pointer_typet &pointer_type, + const typet &pointer_subtype_struct) +{ + if(is_java_generic_type(pointer_type)) + { + // The supplied type must be the full type of the pointer's subtype + PRECONDITION( + pointer_type.subtype().get(ID_identifier) == + pointer_subtype_struct.get(ID_name)); + + const java_generic_typet &generic_pointer = + to_java_generic_type(pointer_type); + + // If the pointer points to an incomplete class, don't treat the generics + if(!pointer_subtype_struct.get_bool(ID_incomplete_class)) + { + PRECONDITION( + is_java_generic_class_type(pointer_subtype_struct) || + is_java_implicitly_generic_class_type(pointer_subtype_struct)); + const std::vector &generic_parameters = + get_all_generic_parameters(pointer_subtype_struct); + + INVARIANT( + generic_pointer.generic_type_arguments().size() == + generic_parameters.size(), + "All generic parameters of the pointer type need to be specified"); + + insert_pairs( + generic_parameters, generic_pointer.generic_type_arguments()); + } + } +} + +/// Add a pair of a parameter and its types for each generic parameter of the +/// given generic symbol type to the controlled map. This function is used +/// for generic bases (superclass or interfaces) where the reference to it is +/// in the form of a symbol rather than a pointer (as opposed to the function +/// insert_pairs_for_pointer). Own the keys and pop from their stack +/// on destruction; otherwise do nothing. +/// \param symbol_type symbol type to get the specialized generic types from +/// \param symbol_struct struct type of the symbol type, must be generic if +/// the symbol is generic +const void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( + const symbol_typet &symbol_type, + const typet &symbol_struct) +{ + if(is_java_generic_symbol_type(symbol_type)) + { + java_generic_symbol_typet generic_symbol = + to_java_generic_symbol_type(symbol_type); + + PRECONDITION( + is_java_generic_class_type(symbol_struct) || + is_java_implicitly_generic_class_type(symbol_struct)); + const std::vector &generic_parameters = + get_all_generic_parameters(symbol_struct); + + INVARIANT( + generic_symbol.generic_types().size() == generic_parameters.size(), + "All generic parameters of the superclass need to be concretized"); + + insert_pairs(generic_parameters, generic_symbol.generic_types()); + } +} diff --git a/src/java_bytecode/generic_parameter_specialization_map_keys.h b/src/java_bytecode/generic_parameter_specialization_map_keys.h new file mode 100644 index 00000000000..74f3803f704 --- /dev/null +++ b/src/java_bytecode/generic_parameter_specialization_map_keys.h @@ -0,0 +1,69 @@ +/// Author: DiffBlue Limited. All Rights Reserved. + +#ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H +#define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H + +#include "select_pointer_type.h" +#include "java_types.h" + +/// \file +/// Generic-parameter-specialization-map entries owner class. +/// Generic-parameter-specialization-map maps generic parameters to a stack +/// of their types in (every depth of) the current scope. This class adds +/// entries to the map for a particular scope, and ensures that they are erased +/// on leaving that scope. +class generic_parameter_specialization_map_keyst +{ +public: + /// Initialize a generic-parameter-specialization-map entry owner operating + /// on a given map. Initially it does not own any map entry. + /// \param _generic_parameter_specialization_map: map to operate on. + explicit generic_parameter_specialization_map_keyst( + generic_parameter_specialization_mapt + &_generic_parameter_specialization_map) + : generic_parameter_specialization_map( + _generic_parameter_specialization_map) + { + } + + /// Removes the top of the stack for each key in erase_keys from the + /// controlled map. + ~generic_parameter_specialization_map_keyst() + { + for(const auto key : erase_keys) + { + PRECONDITION(generic_parameter_specialization_map.count(key) != 0); + (*generic_parameter_specialization_map.find(key)).second.pop(); + if((*generic_parameter_specialization_map.find(key)).second.empty()) + { + generic_parameter_specialization_map.erase(key); + } + } + } + + // Objects of these class cannot be copied in any way - delete the copy + // constructor and copy assignment operator + generic_parameter_specialization_map_keyst( + const generic_parameter_specialization_map_keyst &) = delete; + generic_parameter_specialization_map_keyst & + operator=(const generic_parameter_specialization_map_keyst &) = delete; + + const void insert_pairs_for_pointer( + const pointer_typet &pointer_type, + const typet &pointer_subtype_struct); + const void insert_pairs_for_symbol( + const symbol_typet &symbol_type, + const typet &symbol_struct); + +private: + /// Generic parameter specialization map to modify + generic_parameter_specialization_mapt &generic_parameter_specialization_map; + /// Keys of the entries to pop on destruction + std::vector erase_keys; + + const void insert_pairs( + const std::vector ¶meters, + const std::vector &types); +}; + +#endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index fc4d787e8a3..9c3a03dbd64 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -151,7 +151,16 @@ static optionalt extract_generic_interface_reference( start = find_closing_semi_colon_for_reference_type(signature.value(), start) + 1; - start = signature.value().find("L" + interface_name + "<", start); + // if the interface name includes package name, convert dots to slashes + std::string interface_name_slash_to_dot = interface_name; + std::replace( + interface_name_slash_to_dot.begin(), + interface_name_slash_to_dot.end(), + '.', + '/'); + + start = + signature.value().find("L" + interface_name_slash_to_dot + "<", start); if(start != std::string::npos) { const size_t &end = 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_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index c8ea63d72fe..cad25eb6a16 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -33,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_utils.h" #include "java_string_library_preprocess.h" #include "java_root_class.h" +#include "generic_parameter_specialization_map_keys.h" static symbolt &new_tmp_symbol( symbol_table_baset &symbol_table, @@ -68,6 +69,16 @@ class java_object_factoryt /// this set AND the tree depth becomes >= than the maximum value above. std::unordered_set recursion_set; + /// Every time the non-det generator visits a type and the type is generic + /// (either a struct or a pointer), the following map is used to store and + /// look up the concrete types of the generic paramaters in the current + /// scope. Note that not all generic parameters need to have a concrete + /// type, e.g., the method under test is generic. The types are removed + /// from the map when the scope changes. Note that in different depths + /// of the scope the parameters can be specialized with different types + /// so we keep a stack of types for each parameter. + generic_parameter_specialization_mapt generic_parameter_specialization_map; + /// The symbol table. symbol_table_baset &symbol_table; @@ -742,18 +753,19 @@ void java_object_factoryt::gen_nondet_pointer_init( const update_in_placet &update_in_place) { PRECONDITION(expr.type().id()==ID_pointer); - const pointer_typet &replacement_pointer_type= - pointer_type_selector.convert_pointer_type(pointer_type, ns); + const pointer_typet &replacement_pointer_type = + pointer_type_selector.convert_pointer_type( + pointer_type, generic_parameter_specialization_map, ns); // If we are changing the pointer, we generate code for creating a pointer // to the substituted type instead - if(replacement_pointer_type!=pointer_type) + // TODO if we are comparing array types we need to compare their element + // types. this is for now done by implementing equality function especially + // for java types, technical debt TG-2707 + if(!equal_java_types(replacement_pointer_type, pointer_type)) { - const symbol_exprt real_pointer_symbol=gen_nondet_subtype_pointer_init( - assignments, - alloc_type, - replacement_pointer_type, - depth); + const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init( + assignments, alloc_type, replacement_pointer_type, depth); // Having created a pointer to object of type replacement_pointer_type // we now assign it back to the original pointer with a cast @@ -1151,6 +1163,15 @@ void java_object_factoryt::gen_nondet_init( { // dereferenced type const pointer_typet &pointer_type=to_pointer_type(type); + + // If we are about to initialize a generic pointer type, add its concrete + // types to the map and delete them on leaving this function scope. + generic_parameter_specialization_map_keyst + generic_parameter_specialization_map_keys( + generic_parameter_specialization_map); + generic_parameter_specialization_map_keys.insert_pairs_for_pointer( + pointer_type, ns.follow(pointer_type.subtype())); + gen_nondet_pointer_init( assignments, expr, @@ -1164,6 +1185,21 @@ void java_object_factoryt::gen_nondet_init( else if(type.id()==ID_struct) { const struct_typet struct_type=to_struct_type(type); + + // If we are about to initialize a generic class (as a superclass object + // for a different object), add its concrete types to the map and delete + // them on leaving this function scope. + generic_parameter_specialization_map_keyst + generic_parameter_specialization_map_keys( + generic_parameter_specialization_map); + if(is_sub) + { + const typet &symbol = override_ ? override_type : expr.type(); + PRECONDITION(symbol.id() == ID_symbol); + generic_parameter_specialization_map_keys.insert_pairs_for_symbol( + to_symbol_type(symbol), struct_type); + } + gen_nondet_struct_init( assignments, expr, diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index cf3095f1366..1d1b247fe11 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -713,6 +713,37 @@ bool is_valid_java_array(const struct_typet &type) data_component_valid; } +/// Compares the types, including checking element types if both types are +/// arrays. +/// \param type1 First type to compare +/// \param type2 Second type to compare +/// \return True if the types are equal, including elemnt types if they are +/// both arrays +bool equal_java_types(const typet &type1, const typet &type2) +{ + bool arrays_with_same_element_type = true; + if( + type1.id() == ID_pointer && type2.id() == ID_pointer && + type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol) + { + const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype()); + const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype()); + if( + subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() && + is_java_array_tag(subtype_symbol1.get_identifier())) + { + const typet &array_element_type1 = + java_array_element_type(subtype_symbol1); + const typet &array_element_type2 = + java_array_element_type(subtype_symbol2); + + arrays_with_same_element_type = + equal_java_types(array_element_type1, array_element_type2); + } + } + return (type1 == type2 && arrays_with_same_element_type); +} + void get_dependencies_from_generic_parameters_rec( const typet &t, std::set &refs) diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 043eb5abca8..59a2e0e146d 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -90,6 +90,8 @@ size_t find_closing_semi_colon_for_reference_type( bool is_java_array_tag(const irep_idt &tag); bool is_valid_java_array(const struct_typet &); +bool equal_java_types(const typet &type1, const typet &type2); + /// Class to hold a Java generic type parameter (also called type variable), /// e.g., `T` in `List`. /// The bound can specify type requirements. @@ -120,15 +122,9 @@ class java_generic_parametert:public reference_typet return const_cast(type_variables().front()); } - const std::string get_parameter_class_name() const + const irep_idt get_name() const { - const std::string ¶meter_name = - type_variable().get_identifier().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; + return type_variable().get_identifier(); } private: @@ -451,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/src/java_bytecode/select_pointer_type.cpp b/src/java_bytecode/select_pointer_type.cpp index 4529b11e97b..cd20dcbbb79 100644 --- a/src/java_bytecode/select_pointer_type.cpp +++ b/src/java_bytecode/select_pointer_type.cpp @@ -11,15 +11,101 @@ /// classes to concrete versions). #include "select_pointer_type.h" +#include "java_types.h" #include /// Select what type should be used for a given pointer type. For the base class /// we just use the supplied type. Derived classes can override this behaviour -/// to provide more sophisticated type selection +/// to provide more sophisticated type selection. Generic parameters are +/// replaced with their concrete type. /// \param pointer_type: The pointer type replace +/// \param generic_parameter_specialization_map map of types for all generic +/// parameters in the current scope /// \return A pointer type where the subtype may have been modified pointer_typet select_pointer_typet::convert_pointer_type( - const pointer_typet &pointer_type, const namespacet &ns) const + const pointer_typet &pointer_type, + const generic_parameter_specialization_mapt + &generic_parameter_specialization_map, + const namespacet &ns) const { - return pointer_type; + // if we have a map of generic parameters -> types and the pointer is + // a generic parameter, specialize it with concrete types + if(!generic_parameter_specialization_map.empty()) + { + return specialize_generics( + pointer_type, generic_parameter_specialization_map); + } + else + { + return pointer_type; + } +} + +/// Specialize generic parameters in a pointer type based on the current map +/// of parameters -> types. We specialize generics if the pointer is a java +/// generic parameter or an array with generic parameters (java generic types +/// are specialized recursively, their concrete types are already stored in +/// the map and will be retrieved when needed e.g., to initialize fields). +/// Example: +/// - generic type: T +/// - map: T -> U; U -> String +/// - result: String +/// +/// - generic type: T[] +/// - map: T -> U; U -> String +/// - result: String +/// \param pointer_type pointer to be specialized +/// \param generic_parameter_specialization_map map of types for all generic +/// parameters in the current scope +/// \return pointer type where generic parameters are replaced with concrete +/// types, if set in the current scope +pointer_typet select_pointer_typet::specialize_generics( + const pointer_typet &pointer_type, + const generic_parameter_specialization_mapt + &generic_parameter_specialization_map) const +{ + if(is_java_generic_parameter(pointer_type)) + { + const java_generic_parametert ¶meter = + to_java_generic_parameter(pointer_type); + const irep_idt ¶meter_name = parameter.get_name(); + if(generic_parameter_specialization_map.count(parameter_name) == 0) + { + // this means that the generic pointer_type has not been specialized + // in the current context (e.g., the method under test is generic); + // we return the pointer_type itself which is basically a pointer to + // its upper bound + return pointer_type; + } + const pointer_typet &type = + generic_parameter_specialization_map.find(parameter_name)->second.top(); + + // generic parameters can be adopted from outer classes or superclasses so + // we may need to search for the concrete type recursively + return is_java_generic_parameter(type) + ? specialize_generics( + to_java_generic_parameter(type), + generic_parameter_specialization_map) + : type; + } + else if(pointer_type.subtype().id() == ID_symbol) + { + // if the pointer is an array, recursively specialize its element type + const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype()); + if(is_java_array_tag(array_subtype.get_identifier())) + { + const typet &array_element_type = java_array_element_type(array_subtype); + if(array_element_type.id() == ID_pointer) + { + const pointer_typet &new_array_type = specialize_generics( + to_pointer_type(array_element_type), + generic_parameter_specialization_map); + + pointer_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 pointer_type; } diff --git a/src/java_bytecode/select_pointer_type.h b/src/java_bytecode/select_pointer_type.h index 78a74bd4883..35d4bca2d79 100644 --- a/src/java_bytecode/select_pointer_type.h +++ b/src/java_bytecode/select_pointer_type.h @@ -13,15 +13,28 @@ /// classes to concrete versions). #include +#include +#include "java_types.h" + +typedef std::unordered_map, irep_id_hash> + generic_parameter_specialization_mapt; class namespacet; class select_pointer_typet { public: - virtual ~select_pointer_typet()=default; + virtual ~select_pointer_typet() = default; virtual pointer_typet convert_pointer_type( - const pointer_typet &pointer_type, const namespacet &ns) const; + const pointer_typet &pointer_type, + const generic_parameter_specialization_mapt + &generic_parameter_specialization_map, + const namespacet &ns) const; + + pointer_typet specialize_generics( + const pointer_typet &pointer_type, + const generic_parameter_specialization_mapt + &generic_parameter_specialization_map) const; }; #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H diff --git a/unit/goto-programs/goto_program_generics/GenericBases.java b/unit/goto-programs/goto_program_generics/GenericBases.java new file mode 100644 index 00000000000..65b5b2a5534 --- /dev/null +++ b/unit/goto-programs/goto_program_generics/GenericBases.java @@ -0,0 +1,123 @@ +// Helper classes +class Wrapper { + public T field; +} + +class IntWrapper { + public int i; +} + +class TwoWrapper { + public K first; + public V second; +} + +interface InterfaceWrapper { + public T method(T t); +} + +// A class extending a generic class instantiated with a standard library class +class SuperclassInst extends Wrapper { + public void foo() { + this.field = 5; + } +} + +// A class extending a generic class instantiated with a user-defined class +class SuperclassInst2 extends Wrapper { + public void foo() { + this.field.i = 5; + } +} + +// A class extending an instantiated nested generic class +class SuperclassInst3 extends Wrapper> { + public void foo() { + this.field.field.i = 5; + } +} + +// A generic class extending a generic class (must be with the same parameter) +class SuperclassUninst extends Wrapper { + public void foo(U value) { + this.field = value; + } +} +class SuperclassUninstTest +{ + SuperclassUninst f; + public void foo() { + f.foo(new Integer(1)); + } +} + + +// A generic class extending a generic class with both instantiated and +// uninstantiated parameters +class SuperclassMixed extends TwoWrapper { + public void foo(U value) { + this.first = value; + this.second.i = 5; + } +} +class SuperclassMixedTest +{ + SuperclassMixed f; + public void foo() { + f.foo(true); + } +} + +// Inner classes (generic or not) extending generic classes +class SuperclassInnerInst { + class Inner extends Wrapper { + public void foo() { + this.field = 5; + } + } + public Inner inner; + + class InnerGen extends Wrapper { + public void foo(T value) { + this.field = value; + } + } + public InnerGen inner_gen; + + public void foo() { + inner.foo(); + inner_gen.foo(true); + } +} + +// Implicitly generic inner classes (generic or not) extending generic classes +class SuperclassInnerUninst { + class Inner extends Wrapper { + public void foo(U value) { + this.field = value; + } + } + public Inner inner; + + class InnerGen extends TwoWrapper { + public void foo(U uvalue, T tvalue) { + this.first = uvalue; + this.second = tvalue; + } + } + public InnerGen inner_gen; + + class InnerThree extends Inner { + } + public InnerThree inner_three; +} +class SuperclassInnerUninstTest +{ + SuperclassInnerUninst f; + public void foo() { + IntWrapper x = new IntWrapper(); + f.inner.foo(x); + f.inner_gen.foo(x,true); + f.inner_three.foo(x); + } +} diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class new file mode 100644 index 00000000000..faa5d2304ea Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class new file mode 100644 index 00000000000..fa60ef8a06e Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class new file mode 100644 index 00000000000..26460abadeb Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class new file mode 100644 index 00000000000..d94e1b6e0b3 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class new file mode 100644 index 00000000000..970da292bad Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class new file mode 100644 index 00000000000..1fa20e2c5f9 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class new file mode 100644 index 00000000000..419f729c848 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class b/unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class new file mode 100644 index 00000000000..d757be60547 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class b/unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class new file mode 100644 index 00000000000..e987035b12f Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class b/unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class new file mode 100644 index 00000000000..e1fb3fe67c3 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class b/unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class new file mode 100644 index 00000000000..f2990766703 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields.class b/unit/goto-programs/goto_program_generics/GenericFields.class new file mode 100644 index 00000000000..b25d3be89ab Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFields.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields.java b/unit/goto-programs/goto_program_generics/GenericFields.java new file mode 100644 index 00000000000..92833f7743c --- /dev/null +++ b/unit/goto-programs/goto_program_generics/GenericFields.java @@ -0,0 +1,98 @@ +class SimpleWrapper { + public T field; + public T[] array_field; + + public int int_field; +} + +class IWrapper { + public int i; +} + +class PairWrapper { + public K key; + public V value; +} + +public class GenericFields +{ + IWrapper field; + class SimpleGenericField { + SimpleWrapper field_input; + public void foo() { + field_input.field.i = 5; + field_input.array_field = new IWrapper[2]; + } + } + + class MultipleGenericFields { + SimpleWrapper field_input1; + SimpleWrapper field_input2; + public void foo() { + field_input1.field.i = 10; + field_input2.field.i = 20; + } + } + + class NestedGenericFields { + SimpleWrapper> field_input1; + public void foo() { + field_input1.field.field.i = 30; + } + } + + class PairGenericField { + PairWrapper field_input; + public void foo() { + field_input.key.i = 40; + field_input.value.i = 50; + } + } + + class GenericMethodParameter { + public void foo(SimpleWrapper v) { + v.field.i = 20; + } + } + + class GenericMethodUninstantiatedParameter { + public void foo_unspec(SimpleWrapper v) { + v.int_field=10; + } + } + + class GenericInnerOuter { + class Outer { + public class InnerClass + { + T t; + } + + public Outer() + { + field = new InnerClass(); + } + + public InnerClass field; + } + + public void foo(Outer v) { + Outer t = new Outer(); + t.field.t = v.field.t; + } + } + + class GenericRewriteParameter { + class A { + T value; + A field; + } + + public void foo(A v) { + if(v.field.value) + { + v.value = 1; + } + } + } +} diff --git a/unit/goto-programs/goto_program_generics/IWrapper.class b/unit/goto-programs/goto_program_generics/IWrapper.class new file mode 100644 index 00000000000..9374dd90e43 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/IWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/IntWrapper.class b/unit/goto-programs/goto_program_generics/IntWrapper.class new file mode 100644 index 00000000000..0ab2423e107 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/IntWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/InterfaceWrapper.class b/unit/goto-programs/goto_program_generics/InterfaceWrapper.class new file mode 100644 index 00000000000..84a1e72c248 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/InterfaceWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/PairWrapper.class b/unit/goto-programs/goto_program_generics/PairWrapper.class new file mode 100644 index 00000000000..3684152febb Binary files /dev/null and b/unit/goto-programs/goto_program_generics/PairWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/SimpleWrapper.class b/unit/goto-programs/goto_program_generics/SimpleWrapper.class new file mode 100644 index 00000000000..fbff730183d Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SimpleWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class new file mode 100644 index 00000000000..af39fafee64 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class new file mode 100644 index 00000000000..3ae78c84180 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerInst.class b/unit/goto-programs/goto_program_generics/SuperclassInnerInst.class new file mode 100644 index 00000000000..35d49ee1151 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerInst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class new file mode 100644 index 00000000000..dce417187a0 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class new file mode 100644 index 00000000000..a87c8573a0e Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class new file mode 100644 index 00000000000..c89fee8796a Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class new file mode 100644 index 00000000000..5e496ac02e8 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class new file mode 100644 index 00000000000..085f7e320e2 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInst.class b/unit/goto-programs/goto_program_generics/SuperclassInst.class new file mode 100644 index 00000000000..bdd24f4a62f Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInst2.class b/unit/goto-programs/goto_program_generics/SuperclassInst2.class new file mode 100644 index 00000000000..4a9bbf66465 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInst2.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInst3.class b/unit/goto-programs/goto_program_generics/SuperclassInst3.class new file mode 100644 index 00000000000..d91f3da54ae Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassInst3.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassMixed.class b/unit/goto-programs/goto_program_generics/SuperclassMixed.class new file mode 100644 index 00000000000..0b2f3b90c69 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassMixed.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassMixedTest.class b/unit/goto-programs/goto_program_generics/SuperclassMixedTest.class new file mode 100644 index 00000000000..550ff51a98e Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassMixedTest.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassUninst.class b/unit/goto-programs/goto_program_generics/SuperclassUninst.class new file mode 100644 index 00000000000..8b30a539bbf Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassUninst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassUninstTest.class b/unit/goto-programs/goto_program_generics/SuperclassUninstTest.class new file mode 100644 index 00000000000..a6c038edac5 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassUninstTest.class differ diff --git a/unit/goto-programs/goto_program_generics/TwoWrapper.class b/unit/goto-programs/goto_program_generics/TwoWrapper.class new file mode 100644 index 00000000000..7181bd114ba Binary files /dev/null and b/unit/goto-programs/goto_program_generics/TwoWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/Wrapper.class b/unit/goto-programs/goto_program_generics/Wrapper.class new file mode 100644 index 00000000000..ae6aa9aaf61 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/Wrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/generic_bases_test.cpp b/unit/goto-programs/goto_program_generics/generic_bases_test.cpp new file mode 100644 index 00000000000..4e7a1085c40 --- /dev/null +++ b/unit/goto-programs/goto_program_generics/generic_bases_test.cpp @@ -0,0 +1,414 @@ +/*******************************************************************\ + + Module: Unit tests for instantiating generic superclasses and interfaces. + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ +#include +#include +#include +#include + +// NOTE: To inspect these tests at any point, use expr2java. +// A good way to verify the validity of a test is to iterate +// through all the entry point instructions and print them +// with expr2java. + +SCENARIO( + "Instantiate generic parameters of superclasses", + "[core][goto_program_generics][generic_bases_test]") +{ + GIVEN( + "A class extending a generic class instantiated with a standard library " + "class") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassInst", + "./goto-programs/goto_program_generics", + "SuperclassInst.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // We trace the creation of the object that is being supplied as + // the input to the method under test. There must be one non-null + // assignment only, and usually looks like this: + // this = &tmp_object_factory$1; + const irep_idt &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' created has correctly specialized inherited field") + { + // The following checks that the superclass field gets assigned an + // object of a correct type, e.g.: + // tmp_object_factory$1.@Wrapper.field = + // (struct java.lang.Object *) tmp_object_factory$2; + // tmp_object_factory$2 = &tmp_object_factory$3; + // struct java.lang.Integer { __CPROVER_string @class_identifier; + // boolean @lock; } tmp_object_factory$3; + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {"Wrapper"}, + "field", + "java::java.lang.Integer", + {"java::java.lang.Object"}, + entry_point_code); + } + } + } + + GIVEN( + "A class extending a generic class instantiated with a user-defined class") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassInst2", + "./goto-programs/goto_program_generics", + "SuperclassInst2.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const auto &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has correctly specialized inherited field") + { + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {"Wrapper"}, + "field", + "java::IntWrapper", + {"java::java.lang.Object"}, + entry_point_code); + } + } + } + + GIVEN("A class extending an instantiated nested generic class") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassInst3", + "./goto-programs/goto_program_generics", + "SuperclassInst3.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const auto &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has correctly specialized inherited field") + { + const irep_idt &wrapper_tmp_name = + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {"Wrapper"}, + "field", + "java::Wrapper", + {"java::java.lang.Object"}, + entry_point_code); + + THEN("Object 'this.field' has correctly specialized field") + { + require_goto_statements::require_struct_component_assignment( + wrapper_tmp_name, + {}, + "field", + "java::IntWrapper", + {}, + entry_point_code); + } + } + } + } + + GIVEN("A generic class extending an uninstantiated generic class") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassUninstTest", + "./goto-programs/goto_program_generics", + "SuperclassUninstTest.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const auto &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN( + "The object 'this' has field 'f' of type " + "java::SuperclassUninst") + { + const irep_idt &f_tmp_name = + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {}, + "f", + "java::SuperclassUninst", + {}, + entry_point_code); + + THEN("The object for 'f' has correctly specialized inherited field") + { + require_goto_statements::require_struct_component_assignment( + f_tmp_name, + {"Wrapper"}, + "field", + "java::java.lang.Integer", + {"java::java.lang.Object"}, + entry_point_code); + } + } + } + } + + GIVEN("A generic class extending a partially instantiated generic class") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassMixedTest", + "./goto-programs/goto_program_generics", + "SuperclassMixedTest.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const auto &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("The object 'this' has field 'f' of type java::SuperclassMixed") + { + const irep_idt &f_tmp_name = + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {}, + "f", + "java::SuperclassMixed", + {}, + entry_point_code); + + THEN("The object for 'f' has correctly specialized inherited fields") + { + require_goto_statements::require_struct_component_assignment( + f_tmp_name, + {"TwoWrapper"}, + "first", + "java::java.lang.Boolean", + {"java::java.lang.Object"}, + entry_point_code); + + require_goto_statements::require_struct_component_assignment( + f_tmp_name, + {"TwoWrapper"}, + "second", + "java::IntWrapper", + {"java::java.lang.Object"}, + entry_point_code); + } + } + } + } + + GIVEN( + "A class with an inner classes that extend instantiated or " + "uninstantiated generic classes") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassInnerInst", + "./goto-programs/goto_program_generics", + "SuperclassInnerInst.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const auto &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN( + "The object 'this' has fields 'inner' and 'inner_gen' " + "of correct types") + { + const irep_idt &inner_tmp_name = + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {}, + "inner", + "java::SuperclassInnerInst$Inner", + {}, + entry_point_code); + THEN( + "The object of 'inner' has correctly specialized inherited " + "field") + { + require_goto_statements::require_struct_component_assignment( + inner_tmp_name, + {"Wrapper"}, + "field", + "java::java.lang.Integer", + {}, + entry_point_code); + } + + const irep_idt &inner_gen_tmp_name = + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {}, + "inner_gen", + "java::SuperclassInnerInst$InnerGen", + {}, + entry_point_code); + THEN( + "The object of 'inner_gen' has correctly specialized inherited " + "field") + { + require_goto_statements::require_struct_component_assignment( + inner_gen_tmp_name, + {"Wrapper"}, + "field", + "java::java.lang.Boolean", + {"java::java.lang.Object"}, + entry_point_code); + } + } + } + } + + GIVEN( + "A generic class with inner classes that extend generic classes with " + "the use of the implicit generic parameter") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassInnerUninstTest", + "./goto-programs/goto_program_generics", + "SuperclassInnerUninstTest.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const auto &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN( + "The object 'this' has field 'f' of type " + "java::SuperclassInnerUninst") + { + const irep_idt &f_tmp_name = + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {}, + "f", + "java::SuperclassInnerUninst", + {}, + entry_point_code); + + THEN( + "The object for 'f' has fields 'inner' and 'inner_gen' " + "of correct types") + { + const irep_idt &inner_tmp_name = + require_goto_statements::require_struct_component_assignment( + f_tmp_name, + {}, + "inner", + "java::SuperclassInnerUninst$Inner", + {}, + entry_point_code); + THEN( + "The object of 'inner' has correctly specialized inherited " + "field") + { + require_goto_statements::require_struct_component_assignment( + inner_tmp_name, + {"Wrapper"}, + "field", + "java::IntWrapper", + {"java::java.lang.Object"}, + entry_point_code); + } + + const irep_idt &inner_gen_tmp_name = + require_goto_statements::require_struct_component_assignment( + f_tmp_name, + {}, + "inner_gen", + "java::SuperclassInnerUninst$InnerGen", + {}, + entry_point_code); + THEN( + "The object of 'inner_gen' has correctly specialized inherited " + "fields") + { + require_goto_statements::require_struct_component_assignment( + inner_gen_tmp_name, + {"TwoWrapper"}, + "first", + "java::IntWrapper", + {"java::java.lang.Object"}, + entry_point_code); + require_goto_statements::require_struct_component_assignment( + inner_gen_tmp_name, + {"TwoWrapper"}, + "second", + "java::java.lang.Boolean", + {"java::java.lang.Object"}, + entry_point_code); + } + + const irep_idt &inner_three_tmp_name = + require_goto_statements::require_struct_component_assignment( + f_tmp_name, + {}, + "inner_three", + "java::SuperclassInnerUninst$InnerThree", + {}, + entry_point_code); + THEN( + "The object of 'inner_three' has correctly specialized " + "inherited fields") + { + require_goto_statements::require_struct_component_assignment( + inner_three_tmp_name, + {"Wrapper"}, + "field", + "java::IntWrapper", + {"java::java.lang.Object"}, + entry_point_code); + } + } + } + } + } +} diff --git a/unit/goto-programs/goto_program_generics/generic_parameters_test.cpp b/unit/goto-programs/goto_program_generics/generic_parameters_test.cpp new file mode 100644 index 00000000000..8bd0a407ebe --- /dev/null +++ b/unit/goto-programs/goto_program_generics/generic_parameters_test.cpp @@ -0,0 +1,488 @@ +/*******************************************************************\ + + Module: Unit tests for instantiating generic classes. + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ +#include +#include +#include +#include + +// NOTE: To inspect these tests at any point, use expr2java. +// A good way to verify the validity of a test is to iterate +// through all the entry point instructions and print them +// with expr2java. + +SCENARIO( + "Instantiate generic parameters to methods or fields used within", + "[core][goto_program_generics][generic_parameters_test]") +{ + GIVEN("A class with a generic field") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$SimpleGenericField", + "./goto-programs/goto_program_generics", + "GenericFields$SimpleGenericField.foo"); + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // We trace the creation of the object that is being supplied as + // the input to the method under test. There must be one non-null + // assignment only, and usually looks like this: + // this = &tmp_object_factory$1; + const irep_idt &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has field 'field_input' of type SimpleWrapper") + { + const auto &field_input_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field_input", + "java::SimpleWrapper", + {}, + entry_point_code); + + THEN("Object 'field_input' has field 'field' of type IWrapper") + { + require_goto_statements::require_struct_component_assignment( + field_input_name, + {}, + "field", + "java::IWrapper", + {}, + entry_point_code); + } + THEN("Object 'field_input' has field 'array_field' of type IWrapper[]") + { + require_goto_statements::require_struct_array_component_assignment( + field_input_name, + {}, + "array_field", + "java::array[reference]", + "java::IWrapper", + entry_point_code); + } + } + } + } + + GIVEN("A class with multiple generic fields") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$MultipleGenericFields", + "./goto-programs/goto_program_generics", + "GenericFields$MultipleGenericFields.foo"); + + WHEN("The method input argument is created in the entry point function") + { + // Again, the logic here is the same as the first test: + // We trace the this pointer, which is the input to the + // function we have provided as the entry point, and we + // try to trace it down to its components, to make sure that + // the specific fields we are interested in belong to a class with the + // expected type, and that they behave to the expected type protocol + // themselves. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // The this pointer will be assigned to the object whose class is the + // type we are looking for, and that contains the fields we are looking + // for, so we need to extract its identifier, and start looking for that. + const auto &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has field 'field_input1' of type SimpleWrapper") + { + const auto &field_input1_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field_input1", + "java::SimpleWrapper", + {}, + entry_point_code); + + THEN("Object 'field_input1' has field 'field' of type IWrapper") + { + require_goto_statements::require_struct_component_assignment( + field_input1_name, + {}, + "field", + "java::IWrapper", + {}, + entry_point_code); + } + } + + THEN("Object 'this' has field 'field_input2' of type SimpleWrapper") + { + const auto &field_input2_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field_input2", + "java::SimpleWrapper", + {}, + entry_point_code); + + THEN("Object 'field_input1' has field 'field' of type IWrapper") + { + require_goto_statements::require_struct_component_assignment( + field_input2_name, + {}, + "field", + "java::IWrapper", + {}, + entry_point_code); + } + } + } + } + + GIVEN("A class with a nested generic field") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$NestedGenericFields", + "./goto-programs/goto_program_generics", + "GenericFields$NestedGenericFields.foo"); + + WHEN("The method input argument is created in the entry point function") + { + // Same idea as in the other tests: Start tracing the expected types, + // starting from the this pointer, which symbolises the input object for + // the function we have denoted as our entry point above. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + const auto &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has field 'field_input1' of type SimpleWrapper") + { + const auto &field_input1_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field_input1", + "java::SimpleWrapper", + {}, + entry_point_code); + + THEN("Object 'field_input1' has field 'field' of type SimpleWrapper") + { + const auto &field_name = + require_goto_statements::require_struct_component_assignment( + field_input1_name, + {}, + "field", + "java::SimpleWrapper", + {}, + entry_point_code); + + THEN("Object 'field' has field 'field' of type IWrapper") + { + require_goto_statements::require_struct_component_assignment( + field_name, {}, "field", "java::IWrapper", {}, entry_point_code); + } + } + } + } + } + + GIVEN("A class with a pair generic field") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$PairGenericField", + "./goto-programs/goto_program_generics", + "GenericFields$PairGenericField.foo"); + + WHEN("The method input argument is created in the entry point function") + { + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + const auto &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has field 'field_input' of type PairWrapper") + { + const auto &field_input_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field_input", + "java::PairWrapper", + {}, + entry_point_code); + + THEN("Object 'field_input' has field 'key' of type IWrapper") + { + require_goto_statements::require_struct_component_assignment( + field_input_name, + {}, + "key", + "java::IWrapper", + {}, + entry_point_code); + } + + THEN("Object 'field_input' has field 'value' of type IWrapper") + { + require_goto_statements::require_struct_component_assignment( + field_input_name, + {}, + "value", + "java::IWrapper", + {}, + entry_point_code); + } + } + } + } + + GIVEN("A class with a method that accepts a generic type parameter") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$GenericMethodParameter", + "./goto-programs/goto_program_generics", + "GenericFields$GenericMethodParameter.foo"); + + WHEN("The method input argument is created in the entry point function") + { + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // Instead of the this pointer, we need to trace the "v" pointer, which + // is the name of the pointer of the object that gets passed as a + // parameter to the function. + const auto &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "v", entry_point_code); + + THEN("Object 'v' is of type SimpleWrapper") + { + const auto &tmp_object_declaration = + require_goto_statements::require_declaration_of_name( + tmp_object_name, entry_point_code); + + // Trace the assignments back to the declaration of the generic type + // and verify that it is what we expect. + const auto &tmp_object_struct = + to_struct_type(tmp_object_declaration.symbol().type()); + REQUIRE(tmp_object_struct.get_tag() == "SimpleWrapper"); + + THEN("Object 'v' has field 'field' of type IWrapper") + { + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field", + "java::IWrapper", + {}, + entry_point_code); + } + } + } + } + + GIVEN( + "A class with a method that accepts a generic uninstantiated type " + "parameter") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$GenericMethodUninstantiatedParameter", + "./goto-programs/goto_program_generics", + "GenericFields$GenericMethodUninstantiatedParameter.foo_unspec"); + + WHEN("The method input argument is created in the entry point function") + { + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // Instead of the this pointer, we need to trace the "v" pointer, which + // is the name of the pointer of the object that gets passed as a + // parameter to the function. + const auto &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "v", entry_point_code); + + THEN("Object 'v' is of type SimpleWrapper") + { + const auto &tmp_object_declaration = + require_goto_statements::require_declaration_of_name( + tmp_object_name, entry_point_code); + + // Trace the assignments back to the declaration of the generic type + // and verify that it is what we expect. + const auto &tmp_object_struct = + to_struct_type(tmp_object_declaration.symbol().type()); + REQUIRE(tmp_object_struct.get_tag() == "SimpleWrapper"); + + THEN( + "Object 'v' has field 'field' of type Object (upper bound of the " + "uninstantiated parameter T)") + { + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field", + "java::java.lang.Object", + {}, + entry_point_code); + } + } + } + } + + GIVEN("A generic class with an inner class (implicitly generic)") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$GenericInnerOuter", + "./goto-programs/goto_program_generics", + "GenericFields$GenericInnerOuter.foo"); + + WHEN("The method input argument is created in the entry point function") + { + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // Instead of the this pointer, we need to trace the "v" pointer, which + // is the name of the pointer of the object that gets passed as a + // parameter to the function. + const auto &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "v", entry_point_code); + + THEN("Object 'v' is of type Outer") + { + const auto &tmp_object_declaration = + require_goto_statements::require_declaration_of_name( + tmp_object_name, entry_point_code); + + // Trace the assignments back to the declaration of the generic type + // and verify that it is what we expect. + const auto &tmp_object_struct = + to_struct_type(tmp_object_declaration.symbol().type()); + REQUIRE( + tmp_object_struct.get_tag() == + "GenericFields$GenericInnerOuter$Outer"); + + THEN("Object 'v' has field 'field' of type InnerClass") + { + const auto &field_tmp_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field", + "java::GenericFields$GenericInnerOuter$Outer$InnerClass", + {}, + entry_point_code); + + THEN("Object 'field' has field 't' of type Integer") + { + require_goto_statements::require_struct_component_assignment( + field_tmp_name, + {}, + "t", + "java::java.lang.Integer", + {}, + entry_point_code); + } + } + } + } + } + + GIVEN( + "A generic class that instantiates its parameter with different type " + "in different scope depth") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFields$GenericRewriteParameter", + "./goto-programs/goto_program_generics", + "GenericFields$GenericRewriteParameter.foo"); + + WHEN("The method input argument is created in the entry point function") + { + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // Instead of the this pointer, we need to trace the "v" pointer, which + // is the name of the pointer of the object that gets passed as a + // parameter to the function. + const auto &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "v", entry_point_code); + + THEN("Object 'v' is of type A") + { + const auto &tmp_object_declaration = + require_goto_statements::require_declaration_of_name( + tmp_object_name, entry_point_code); + + // Trace the assignments back to the declaration of the generic type + // and verify that it is what we expect. + const auto &tmp_object_struct = + to_struct_type(tmp_object_declaration.symbol().type()); + REQUIRE( + tmp_object_struct.get_tag() == + "GenericFields$GenericRewriteParameter$A"); + + THEN("Object 'v' has field 'value' of type Integer") + { + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "value", + "java::java.lang.Integer", + {}, + entry_point_code); + } + + THEN("Object 'v' has field 'field' of type A") + { + const auto &field_tmp_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "field", + "java::GenericFields$GenericRewriteParameter$A", + {}, + entry_point_code); + + THEN("Object 'field' has field 'value' of type Boolean") + { + require_goto_statements::require_struct_component_assignment( + field_tmp_name, + {}, + "value", + "java::java.lang.Boolean", + {}, + entry_point_code); + } + } + } + } + } +} 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/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index 3095615b8fb..5071daac3d3 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -36,8 +36,6 @@ SCENARIO( {{require_type::type_argument_kindt::Inst, "java::Interface_Implementation"}}); } - - // TODO: Check that specialised superclass is created. TG-1419 } THEN("There should be a symbol for the DerivedGenericInst2 class") @@ -61,8 +59,6 @@ SCENARIO( "java::Interface_Implementation"}, {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); } - - // TODO: Check that specialised superclass is created. TG-1419 } THEN("There should be a symbol for the DerivedGenericUninst class") @@ -85,8 +81,6 @@ SCENARIO( {{require_type::type_argument_kindt::Var, "java::DerivedGenericUninst::T"}}); } - - // TODO: Check that specialised superclass is created. TG-1418 } THEN("There should be a symbol for the DerivedGenericMixed1 class") @@ -109,8 +103,6 @@ SCENARIO( {{require_type::type_argument_kindt::Inst, "java::Interface_Implementation"}}); } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN("There should be a symbol for the DerivedGenericMixed2 class") @@ -134,8 +126,6 @@ SCENARIO( "java::DerivedGenericMixed2::T"}, {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN("There should be a symbol for the ContainsInnerClass$InnerClass class") @@ -157,8 +147,6 @@ SCENARIO( "java::Generic", {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -183,8 +171,6 @@ SCENARIO( {{require_type::type_argument_kindt::Var, "java::ContainsInnerClass$InnerClassGeneric::T"}}); } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -210,8 +196,6 @@ SCENARIO( {{require_type::type_argument_kindt::Var, "java::ContainsInnerClassGeneric::T"}}); } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN("There should be a symbol for the ThreeHierarchy class") @@ -233,8 +217,6 @@ SCENARIO( "java::DerivedGenericMixed2", {{require_type::type_argument_kindt::Inst, "java::java.lang.String"}}); } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -268,8 +250,6 @@ SCENARIO( "java::java.lang.Integer"}}); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -302,8 +282,6 @@ SCENARIO( "java::ImplementsInterfaceGenericUnspec::E"}}); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -342,8 +320,6 @@ SCENARIO( require_type::require_symbol(base_type, "java::Interface"); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -386,8 +362,6 @@ SCENARIO( "java::java.lang.Integer"}}); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -432,8 +406,6 @@ SCENARIO( "java::ExtendsAndImplementsGeneric::T"}}); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -471,8 +443,6 @@ SCENARIO( "java::java.lang.Integer"}}); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -517,8 +487,6 @@ SCENARIO( "java::java.lang.Integer"}}); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN( @@ -556,8 +524,6 @@ SCENARIO( "java::ExtendsAndImplementsSameInterfaceGeneric::T"}}); } } - - // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } THEN("There should be a symbol for the `ExtendImplicit` class") 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 diff --git a/unit/testing-utils/require_goto_statements.cpp b/unit/testing-utils/require_goto_statements.cpp index 8881ad54666..b4deb68b936 100644 --- a/unit/testing-utils/require_goto_statements.cpp +++ b/unit/testing-utils/require_goto_statements.cpp @@ -11,6 +11,8 @@ #include #include +#include +#include /// Expand value of a function to include all child codets /// \param function_value: The value of the function (e.g. got by looking up @@ -33,18 +35,38 @@ require_goto_statements::get_all_statements(const exprt &function_value) return statements; } -/// Find assignment statements of the form \p structure_name.\component_name = +/// \param symbol_table Symbol table for the test +/// \return All codet statements of the __CPROVER_start function +const std::vector +require_goto_statements::require_entry_point_statements( + const symbol_tablet &symbol_table) +{ + // Retrieve __CPROVER_start + const symbolt *entry_point_function = + symbol_table.lookup(goto_functionst::entry_point()); + REQUIRE(entry_point_function != nullptr); + return get_all_statements(entry_point_function->value); +} + +/// Find assignment statements of the form: +/// - \p structure_name +/// .@\p superclass_name.\p component_name = (if it's a component inherited +/// from the superclass) +/// - \p structure_name.\p component_name = (otherwise) /// \param statements: The statements to look through /// \param structure_name: The name of variable of type struct -/// \param component_name: The name of the component that should be assigned +/// \param superclass_name: The name of the superclass (if given) +/// \param component_name: The name of the component of the superclass that +/// should be assigned /// \return: All the assignments to that component. -std::vector +require_goto_statements::pointer_assignment_locationt require_goto_statements::find_struct_component_assignments( const std::vector &statements, const irep_idt &structure_name, + const optionalt &superclass_name, const irep_idt &component_name) { - std::vector component_assignments; + pointer_assignment_locationt locations; for(const auto &assignment : statements) { @@ -54,19 +76,69 @@ require_goto_statements::find_struct_component_assignments( if(code_assign.lhs().id() == ID_member) { - const auto &member_expr = to_member_expr(code_assign.lhs()); - const auto &symbol = member_expr.symbol(); + const member_exprt &member_expr = to_member_expr(code_assign.lhs()); - if( - symbol.get_identifier() == structure_name && - member_expr.get_component_name() == component_name) + if(superclass_name.has_value()) { - component_assignments.push_back(code_assign); + // Structure of the expression: + // member_exprt member_expr: + // - component name: \p component_name + // - operand (component of): member_exprt superclass_expr: + // - component name: @\p superclass_name + // - operand (component of): symbol for \p structure_name + if( + member_expr.get_component_name() == component_name && + member_expr.compound().id() == ID_member) + { + const member_exprt &superclass_expr = + to_member_expr(member_expr.op0()); + const irep_idt supercomponent_name = + "@" + id2string(superclass_name.value()); + + if( + superclass_expr.get_component_name() == supercomponent_name && + superclass_expr.symbol().get_identifier() == structure_name) + { + if( + code_assign.rhs() == + null_pointer_exprt(to_pointer_type(code_assign.lhs().type()))) + { + locations.null_assignment = code_assign; + } + else + { + locations.non_null_assignments.push_back(code_assign); + } + } + } + } + else + { + // Structure of the expression: + // member_exprt member_expr: + // - component name: \p component_name + // - operand (component of): symbol for \p structure_name + if( + member_expr.op().id() == ID_symbol && + member_expr.symbol().get_identifier() == structure_name && + member_expr.get_component_name() == component_name) + { + if( + code_assign.rhs() == + null_pointer_exprt(to_pointer_type(code_assign.lhs().type()))) + { + locations.null_assignment = code_assign; + } + else + { + locations.non_null_assignments.push_back(code_assign); + } + } } } } } - return component_assignments; + return locations; } /// For a given variable name, gets the assignments to it in the provided @@ -131,3 +203,195 @@ const code_declt &require_goto_statements::require_declaration_of_name( } throw no_decl_found_exceptiont(variable_name.c_str()); } + +/// Checks that the component of the structure (possibly inherited from +/// the superclass) is assigned an object of the given type. +/// \param structure_name The name the variable +/// \param superclass_name The name of its superclass (if given) +/// \param component_name The name of the field of the superclass +/// \param component_type_name The name of the required type of the field +/// \param typecast_name The name of the type to which the object is cast (if +/// there is a typecast) +/// \param entry_point_instructions The statements to look through +/// \return The identifier of the variable assigned to the field +const irep_idt &require_goto_statements::require_struct_component_assignment( + const irep_idt &structure_name, + const optionalt &superclass_name, + const irep_idt &component_name, + const irep_idt &component_type_name, + const optionalt &typecast_name, + const std::vector &entry_point_instructions) +{ + // First we need to find the assignments to the component belonging to + // the structure_name object + const auto &component_assignments = + require_goto_statements::find_struct_component_assignments( + entry_point_instructions, + structure_name, + superclass_name, + component_name); + REQUIRE(component_assignments.non_null_assignments.size() == 1); + + // We are expecting that the resulting statement can be of two forms: + // 1. structure_name.(@superclass_name if given).component = + // (struct cast_type_name *) tmp_object_factory$1; + // followed by a direct assignment like this: + // tmp_object_factory$1 = &tmp_object_factory$2; + // 2. structure_name.component = &tmp_object_factory$1; + exprt component_assignment_rhs_expr = + component_assignments.non_null_assignments[0].rhs(); + + // If the rhs is a typecast (case 1 above), deconstruct it to get the name of + // the variable and find the assignment to it + if(component_assignment_rhs_expr.id() == ID_typecast) + { + const auto &component_assignment_rhs = + to_typecast_expr(component_assignment_rhs_expr); + + // Check the type we are casting to + if(typecast_name.has_value()) + { + REQUIRE(component_assignment_rhs.type().id() == ID_pointer); + REQUIRE( + to_symbol_type( + to_pointer_type(component_assignment_rhs.type()).subtype()) + .get(ID_identifier) == typecast_name.value()); + } + + const auto &component_reference_tmp_name = + to_symbol_expr(component_assignment_rhs.op()).get_identifier(); + const auto &component_reference_assignments = + require_goto_statements::find_pointer_assignments( + component_reference_tmp_name, entry_point_instructions) + .non_null_assignments; + REQUIRE(component_reference_assignments.size() == 1); + component_assignment_rhs_expr = component_reference_assignments[0].rhs(); + } + + // The rhs assigns an address of a variable, get its name + const auto &component_reference_assignment_rhs = + to_address_of_expr(component_assignment_rhs_expr); + const auto &component_tmp_name = + to_symbol_expr(component_reference_assignment_rhs.op()).get_identifier(); + + // After we have found the declaration of the final assignment's + // right hand side, then we want to identify that the type + // is the one we expect, e.g.: + // struct java.lang.Integer { __CPROVER_string @class_identifier; + // boolean @lock; } tmp_object_factory$2; + const auto &component_declaration = + require_goto_statements::require_declaration_of_name( + component_tmp_name, entry_point_instructions); + REQUIRE(component_declaration.symbol().type().id() == ID_struct); + const auto &component_struct = + to_struct_type(component_declaration.symbol().type()); + REQUIRE(component_struct.get(ID_name) == component_type_name); + + return component_tmp_name; +} + +/// Checks that the array component of the structure (possibly inherited from +/// the superclass) is assigned an array with given element type. +/// \param structure_name The name the variable +/// \param superclass_name The name of its superclass (if given) +/// \param array_component_name The name of the array field of the superclass +/// \param array_type_name The type of the array, e.g., java::array[reference] +/// \param array_component_element_type_name The element type of the array +/// \param entry_point_instructions The statements to look through +/// \return The identifier of the variable assigned to the field +const irep_idt & +require_goto_statements::require_struct_array_component_assignment( + const irep_idt &structure_name, + const optionalt &superclass_name, + const irep_idt &array_component_name, + const irep_idt &array_type_name, + const irep_idt &array_component_element_type_name, + const std::vector &entry_point_instructions) +{ + // First we need to find the assignments to the component belonging to + // the structure_name object + const auto &component_assignments = + require_goto_statements::find_struct_component_assignments( + entry_point_instructions, + structure_name, + superclass_name, + array_component_name); + REQUIRE(component_assignments.non_null_assignments.size() == 1); + + // We are expecting that the resulting statement is of form: + // structure_name.array_component_name = (struct array_type_name *) + // tmp_object_factory$1; + const exprt &component_assignment_rhs_expr = + component_assignments.non_null_assignments[0].rhs(); + + // The rhs is a typecast, deconstruct it to get the name of the variable + // and find the assignment to it + PRECONDITION(component_assignment_rhs_expr.id() == ID_typecast); + const auto &component_assignment_rhs = + to_typecast_expr(component_assignment_rhs_expr); + const auto &component_reference_tmp_name = + to_symbol_expr(component_assignment_rhs.op()).get_identifier(); + + // Check the type we are casting to matches the array type + REQUIRE(component_assignment_rhs.type().id() == ID_pointer); + REQUIRE( + to_symbol_type(to_pointer_type(component_assignment_rhs.type()).subtype()) + .get(ID_identifier) == array_type_name); + + // Get the tmp_object name and find assignments to it, there should be only + // one that assigns the correct array through side effect + const auto &component_reference_assignments = + require_goto_statements::find_pointer_assignments( + component_reference_tmp_name, entry_point_instructions); + REQUIRE(component_reference_assignments.non_null_assignments.size() == 1); + const exprt &component_reference_assignment_rhs_expr = + component_reference_assignments.non_null_assignments[0].rhs(); + + // The rhs is side effect + PRECONDITION(component_reference_assignment_rhs_expr.id() == ID_side_effect); + const auto &array_component_reference_assignment_rhs = + to_side_effect_expr(component_reference_assignment_rhs_expr); + + // The type of the side effect is an array with the correct element type + PRECONDITION( + array_component_reference_assignment_rhs.type().id() == ID_pointer); + const typet &array = + to_pointer_type(array_component_reference_assignment_rhs.type()).subtype(); + PRECONDITION(is_java_array_tag(array.get(ID_identifier))); + REQUIRE(array.get(ID_identifier) == array_type_name); + + return component_reference_tmp_name; +} + +/// Checks that the input argument (of method under test) with given name is +/// assigned a single non-null object in the entry point function. +/// \param argument_name Name of the input argument of method under test +/// \param entry_point_statements The statements to look through +/// \return The identifier of the variable assigned to the input argument +const irep_idt & +require_goto_statements::require_entry_point_argument_assignment( + const irep_idt &argument_name, + const std::vector &entry_point_statements) +{ + // Trace the creation of the object that is being supplied as the input + // argument to the function under test + const pointer_assignment_locationt &argument_assignments = + find_pointer_assignments( + id2string(goto_functionst::entry_point()) + "::" + + id2string(argument_name), + entry_point_statements); + + // There should be at most one assignment to it + REQUIRE(argument_assignments.non_null_assignments.size() == 1); + + // The following finds the name of the tmp object that gets assigned + // to the input argument. There must be one such assignment only, + // and usually looks like this: + // argument_name = &tmp_object_factory$1; + const auto &argument_assignment = + argument_assignments.non_null_assignments[0]; + const auto &argument_tmp_name = + to_symbol_expr(to_address_of_expr(argument_assignment.rhs()).object()) + .get_identifier(); + return argument_tmp_name; +} diff --git a/unit/testing-utils/require_goto_statements.h b/unit/testing-utils/require_goto_statements.h index d55a96fde7c..95b368a1092 100644 --- a/unit/testing-utils/require_goto_statements.h +++ b/unit/testing-utils/require_goto_statements.h @@ -47,13 +47,17 @@ class no_decl_found_exceptiont : public std::exception std::string _varname; }; -std::vector find_struct_component_assignments( +pointer_assignment_locationt find_struct_component_assignments( const std::vector &statements, const irep_idt &structure_name, + const optionalt &superclass_name, const irep_idt &component_name); std::vector get_all_statements(const exprt &function_value); +const std::vector +require_entry_point_statements(const symbol_tablet &symbol_table); + pointer_assignment_locationt find_pointer_assignments( const irep_idt &pointer_name, const std::vector &instructions); @@ -61,6 +65,26 @@ pointer_assignment_locationt find_pointer_assignments( const code_declt &require_declaration_of_name( const irep_idt &variable_name, const std::vector &entry_point_instructions); + +const irep_idt &require_struct_component_assignment( + const irep_idt &structure_name, + const optionalt &superclass_name, + const irep_idt &component_name, + const irep_idt &component_type_name, + const optionalt &typecast_name, + const std::vector &entry_point_instructions); + +const irep_idt &require_struct_array_component_assignment( + const irep_idt &structure_name, + const optionalt &superclass_name, + const irep_idt &array_component_name, + const irep_idt &array_type_name, + const irep_idt &array_component_element_type_name, + const std::vector &entry_point_instructions); + +const irep_idt &require_entry_point_argument_assignment( + const irep_idt &argument_name, + const std::vector &entry_point_statements); } #endif // CPROVER_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H