From 3111255c34f41c5bdcdade5ea91ae64dab3c5e91 Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 9 Feb 2018 17:19:10 +0000 Subject: [PATCH 1/6] Introduce a map of parameter-type pairs The map of generic parameters and a stack of their concrete types in the various depths of the current scope. --- src/java_bytecode/Makefile | 1 + ...eric_parameter_specialization_map_keys.cpp | 155 ++++++++++++++++++ ...eneric_parameter_specialization_map_keys.h | 69 ++++++++ src/java_bytecode/java_object_factory.cpp | 35 ++++ src/java_bytecode/java_object_factory.h | 3 + src/java_bytecode/java_types.h | 8 +- 6 files changed, 269 insertions(+), 2 deletions(-) create mode 100644 src/java_bytecode/generic_parameter_specialization_map_keys.cpp create mode 100644 src/java_bytecode/generic_parameter_specialization_map_keys.h diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index a868fdd5c90..ea46c4e1250 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -4,6 +4,7 @@ SRC = bytecode_info.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 \ 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_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index c8ea63d72fe..e455fa70921 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; @@ -1151,6 +1162,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 +1184,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_object_factory.h b/src/java_bytecode/java_object_factory.h index 7262f7dc652..4e3b43caa82 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -107,6 +107,9 @@ exprt object_factory( allocation_typet alloc_type, const source_locationt &location); +typedef std::unordered_map, + irep_id_hash> generic_parameter_specialization_mapt; + enum class update_in_placet { NO_UPDATE_IN_PLACE, diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 043eb5abca8..9e59d522ee8 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -120,10 +120,14 @@ class java_generic_parametert:public reference_typet return const_cast(type_variables().front()); } + const irep_idt get_name() const + { + return type_variable().get_identifier(); + } + const std::string get_parameter_class_name() const { - const std::string ¶meter_name = - type_variable().get_identifier().c_str(); + const std::string ¶meter_name = get_name().c_str(); PRECONDITION(has_prefix(parameter_name, "java::")); int prefix_length = std::string("java::").length(); const std::string name = parameter_name.substr( From 624cc918d1150c2d26a889647cad5bff0345f450 Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 2 Mar 2018 12:36:42 +0000 Subject: [PATCH 2/6] Use the map of parameter-type pairs to specialize generics --- src/java_bytecode/ci_lazy_methods.cpp | 6 +- src/java_bytecode/java_object_factory.cpp | 17 +++-- src/java_bytecode/java_object_factory.h | 3 - src/java_bytecode/java_types.cpp | 31 ++++++++ src/java_bytecode/java_types.h | 2 + src/java_bytecode/select_pointer_type.cpp | 92 ++++++++++++++++++++++- src/java_bytecode/select_pointer_type.h | 17 ++++- 7 files changed, 150 insertions(+), 18 deletions(-) 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/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index e455fa70921..cad25eb6a16 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -753,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 diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index 4e3b43caa82..7262f7dc652 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -107,9 +107,6 @@ exprt object_factory( allocation_typet alloc_type, const source_locationt &location); -typedef std::unordered_map, - irep_id_hash> generic_parameter_specialization_mapt; - enum class update_in_placet { NO_UPDATE_IN_PLACE, 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 9e59d522ee8..775cada45a2 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. 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 From 5c00440eeb3fefb78607f1539240a78ffb1968f0 Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 2 Mar 2018 13:45:43 +0000 Subject: [PATCH 3/6] Remove the old way of specializing generics We now specialize generics on-the-fly using a context-sensitive map of parameter-type pairs --- src/java_bytecode/Makefile | 2 - .../generate_java_generic_type.cpp | 343 ---------- .../generate_java_generic_type.h | 45 -- .../generic_arguments_name_builder.cpp | 42 -- .../generic_arguments_name_builder.h | 43 -- src/java_bytecode/java_bytecode_language.cpp | 1 - src/java_bytecode/java_types.h | 81 --- .../generate_java_generic_type.cpp | 373 ----------- .../generate_outer_inner.cpp | 598 ------------------ ...ic_field_array_instantiation$generic.class | Bin 746 -> 0 bytes ...eld_array_instantiation$genericArray.class | Bin 974 -> 0 bytes .../generic_field_array_instantiation.class | Bin 1162 -> 0 bytes .../generic_field_array_instantiation.java | 21 - ...uter_inner$GenericOuter$GenericInner.class | Bin 751 -> 0 bytes ..._inner$GenericOuter$Inner$InnerInner.class | Bin 825 -> 0 bytes ...neric_outer_inner$GenericOuter$Inner.class | Bin 826 -> 0 bytes .../generic_outer_inner$GenericOuter.class | Bin 1060 -> 0 bytes ...Outer$GenericInner$GenericInnerInner.class | Bin 929 -> 0 bytes ..._inner$Outer$GenericInner$InnerInner.class | Bin 818 -> 0 bytes ...neric_outer_inner$Outer$GenericInner.class | Bin 1031 -> 0 bytes ..._inner$Outer$Inner$GenericInnerInner.class | Bin 848 -> 0 bytes ...c_outer_inner$Outer$Inner$InnerInner.class | Bin 769 -> 0 bytes .../generic_outer_inner$Outer$Inner.class | Bin 605 -> 0 bytes ...uter$TwoParamGenericInner$InnerInner.class | Bin 904 -> 0 bytes ...ter_inner$Outer$TwoParamGenericInner.class | Bin 911 -> 0 bytes .../generic_outer_inner$Outer.class | Bin 654 -> 0 bytes .../generic_outer_inner.class | Bin 3112 -> 0 bytes .../generic_outer_inner.java | 82 --- .../generic_two_fields$bound_element.class | Bin 699 -> 0 bytes .../generic_two_fields.class | Bin 495 -> 0 bytes .../generic_two_fields.java | 11 - .../generic_two_instances$element.class | Bin 664 -> 0 bytes .../generic_two_instances.class | Bin 581 -> 0 bytes .../generic_two_instances.java | 8 - .../generic_two_parameters$KeyValuePair.class | Bin 743 -> 0 bytes .../generic_two_parameters.class | Bin 1009 -> 0 bytes .../generic_two_parameters.java | 22 - .../generic_unknown_field$G.class | Bin 738 -> 0 bytes .../generic_unknown_field$element.class | Bin 664 -> 0 bytes .../generic_unknown_field.class | Bin 405 -> 0 bytes .../generic_unknown_field.java | 9 - unit/testing-utils/Makefile | 1 - unit/testing-utils/generic_utils.cpp | 62 -- unit/testing-utils/generic_utils.h | 31 - 44 files changed, 1775 deletions(-) delete mode 100644 src/java_bytecode/generate_java_generic_type.cpp delete mode 100644 src/java_bytecode/generate_java_generic_type.h delete mode 100644 src/java_bytecode/generic_arguments_name_builder.cpp delete mode 100644 src/java_bytecode/generic_arguments_name_builder.h delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$GenericInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner$InnerInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$GenericInnerInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$InnerInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$GenericInnerInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$InnerInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner$InnerInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.java delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_fields$bound_element.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.java delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_instances$element.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters$KeyValuePair.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$G.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$element.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.class delete mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.java delete mode 100644 unit/testing-utils/generic_utils.cpp delete mode 100644 unit/testing-utils/generic_utils.h diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index ea46c4e1250..b9371e734f1 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -3,7 +3,6 @@ SRC = bytecode_info.cpp \ ci_lazy_methods.cpp \ ci_lazy_methods_needed.cpp \ expr2java.cpp \ - generic_arguments_name_builder.cpp \ generic_parameter_specialization_map_keys.cpp \ jar_file.cpp \ java_bytecode_convert_class.cpp \ @@ -30,7 +29,6 @@ SRC = bytecode_info.cpp \ java_string_literals.cpp \ java_types.cpp \ java_utils.cpp \ - generate_java_generic_type.cpp \ mz_zip_archive.cpp \ select_pointer_type.cpp \ # Empty last line diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp deleted file mode 100644 index 70764e20e97..00000000000 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ /dev/null @@ -1,343 +0,0 @@ -/*******************************************************************\ - - Module: Generate Java Generic Type - Instantiate a generic class with - concrete type information. - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include - -#include "generate_java_generic_type.h" -#include "generic_arguments_name_builder.h" -#include -#include -#include - -generate_java_generic_typet::generate_java_generic_typet( - message_handlert &message_handler): - message_handler(message_handler) -{} - -/// Small auxiliary function, to print a single generic argument name. -/// \param argument argument type -/// \return printed name of the argument -static std::string argument_name_printer(const reference_typet &argument) -{ - const irep_idt &id(id2string(argument.subtype().get(ID_identifier))); - if(is_java_array_tag(id)) - { - std::string name = pretty_print_java_type(id2string(id)); - const typet &element_type = - java_array_element_type(to_symbol_type(argument.subtype())); - - // If this is an array of references then we will specialize its - // identifier using the type of the objects in the array. Else, there - // can be a problem with the same symbols for different instantiations - // using arrays with different types. - if(element_type.id() == ID_pointer) - { - const symbol_typet element_symbol = - to_symbol_type(element_type.subtype()); - name.append("of_" + id2string(element_symbol.get_identifier())); - } - return name; - } - else - { - return id2string(id); - } -} - -/// Generate a concrete instantiation of a generic type. -/// \param existing_generic_type The type to be concretised -/// \param symbol_table The symbol table that the concrete type will be -/// inserted into. -/// \return The symbol as it was retrieved from the symbol table after -/// it has been inserted into. -symbolt generate_java_generic_typet::operator()( - const java_generic_typet &existing_generic_type, - symbol_tablet &symbol_table) const -{ - namespacet ns(symbol_table); - - const typet &pointer_subtype=ns.follow(existing_generic_type.subtype()); - - INVARIANT( - pointer_subtype.id()==ID_struct, "Only pointers to classes in java"); - INVARIANT( - is_java_generic_class_type(pointer_subtype) || - is_java_implicitly_generic_class_type(pointer_subtype), - "Generic references type must be a generic class"); - - const java_class_typet &class_definition = - to_java_class_type(pointer_subtype); - - const std::string generic_name = build_generic_name( - existing_generic_type, class_definition, argument_name_printer); - struct_union_typet::componentst replacement_components = - class_definition.components(); - - // Small auxiliary function, to perform the inplace - // modification of the generic fields. - auto replace_type_for_generic_field = - [&](struct_union_typet::componentt &component) { - - component.type() = substitute_type( - component.type(), class_definition, existing_generic_type); - - return component; - }; - - std::size_t pre_modification_size=to_java_class_type( - ns.follow(existing_generic_type.subtype())).components().size(); - - std::for_each( - replacement_components.begin(), - replacement_components.end(), - replace_type_for_generic_field); - - std::size_t after_modification_size = class_definition.components().size(); - - INVARIANT( - pre_modification_size==after_modification_size, - "All components in the original class should be in the new class"); - - const java_specialized_generic_class_typet new_java_class{ - generic_name, - class_definition, - replacement_components, - existing_generic_type.generic_type_arguments()}; - - const type_symbolt &class_symbol = - build_symbol_from_specialised_class(new_java_class); - - std::pair res = symbol_table.insert(std::move(class_symbol)); - if(!res.second) - { - messaget message(message_handler); - message.warning() << "stub class symbol " << class_symbol.name - << " already exists" << messaget::eom; - } - - const auto expected_symbol="java::"+id2string(generic_name); - auto symbol=symbol_table.lookup(expected_symbol); - INVARIANT(symbol, "New class not created"); - return *symbol; -} - -/// For a given type, if the type contains a Java generic parameter, we look -/// that parameter up and return the relevant type. This works recursively on -/// arrays so that T [] is converted to RelevantType []. -/// \param parameter_type: The type under consideration -/// \param generic_class: The generic class that the \p parameter_type -/// belongs to (e.g. the type of a component of the class). This is used to -/// look up the mapping from name of generic parameter to its index. -/// \param generic_reference: The instantiated version of the generic class -/// used to look up the instantiated type. This is expected to be fully -/// instantiated. -/// \return A newly constructed type with generic parameters replaced, or if -/// there are none to replace, the original type. -typet generate_java_generic_typet::substitute_type( - const typet ¶meter_type, - const java_class_typet &class_definition, - const java_generic_typet &generic_reference) const -{ - if(is_java_generic_parameter(parameter_type)) - { - auto component_identifier = to_java_generic_parameter(parameter_type) - .type_variable() - .get_identifier(); - - // see if it is a generic parameter introduced by this class - optionalt results; - if(is_java_generic_class_type(class_definition)) - { - const java_generic_class_typet &generic_class = - to_java_generic_class_type(class_definition); - - results = java_generics_get_index_for_subtype( - generic_class.generic_types(), component_identifier); - } - // see if it is an implicit generic parameter introduced by an outer class - if(!results.has_value()) - { - INVARIANT( - is_java_implicitly_generic_class_type(class_definition), - "The parameter must either be a generic type or implicit generic type"); - const java_implicitly_generic_class_typet &implicitly_generic_class = - to_java_implicitly_generic_class_type(class_definition); - results = java_generics_get_index_for_subtype( - implicitly_generic_class.implicit_generic_types(), - component_identifier); - } - - INVARIANT(results.has_value(), "generic component type not found"); - return generic_reference.generic_type_arguments()[*results]; - } - else if(parameter_type.id() == ID_pointer) - { - if(is_java_generic_type(parameter_type)) - { - const java_generic_typet &generic_type = - to_java_generic_type(parameter_type); - - java_generic_typet::generic_type_argumentst replaced_type_variables; - - // Swap each parameter - std::transform( - generic_type.generic_type_arguments().begin(), - generic_type.generic_type_arguments().end(), - std::back_inserter(replaced_type_variables), - [&](const reference_typet &generic_param) -> reference_typet - { - const typet &replacement_type = - substitute_type(generic_param, class_definition, generic_reference); - - // This code will be simplified when references aren't considered to - // be generic parameters - if(is_java_generic_parameter(replacement_type)) - { - return to_java_generic_parameter(replacement_type); - } - else - { - INVARIANT( - is_reference(replacement_type), - "All generic parameters should be references"); - return to_reference_type(replacement_type); - } - }); - - java_generic_typet new_type = generic_type; - new_type.generic_type_arguments() = replaced_type_variables; - return new_type; - } - else if(parameter_type.subtype().id() == ID_symbol) - { - const symbol_typet &array_subtype = - to_symbol_type(parameter_type.subtype()); - if(is_java_array_tag(array_subtype.get_identifier())) - { - const typet &array_element_type = - java_array_element_type(array_subtype); - - const typet &new_array_type = substitute_type( - array_element_type, class_definition, generic_reference); - - typet replacement_array_type = java_array_type('a'); - replacement_array_type.subtype().set(ID_C_element_type, new_array_type); - return replacement_array_type; - } - } - } - return parameter_type; -} - -/// Build a unique name for the generic to be instantiated. -/// Example: if \p existing_generic_type is a pointer to `Outer.Inner` -/// (\p original_class) with parameter `T` being specialized with argument -/// `Integer`, then the function returns a string `Outer<\p -/// argument_name_printer(Integer)>$Inner`. -/// \param existing_generic_type The type we want to concretise -/// \param original_class The original class type for \p existing_generic_type -/// \param argument_name_printer A custom function to print names of individual -/// arguments (such as `Integer`, `Integer[]` for concise names or `java::java -/// .lang.Integer`, `array[reference]of_java::java.lang.Integer`) -/// \return A name for the new specialized generic class we want a unique name -/// for. -std::string generate_java_generic_typet::build_generic_name( - const java_generic_typet &existing_generic_type, - const java_class_typet &original_class, - const generic_arguments_name_buildert::name_printert &argument_name_printer) - const -{ - std::ostringstream generic_name_buffer; - const std::string &original_class_name = original_class.get_tag().c_str(); - - // gather together all implicit generic types and generic types - std::vector generic_types; - if(is_java_implicitly_generic_class_type(original_class)) - { - const java_implicitly_generic_class_typet - &implicitly_generic_original_class = - to_java_implicitly_generic_class_type(original_class); - generic_types.insert( - generic_types.end(), - implicitly_generic_original_class.implicit_generic_types().begin(), - implicitly_generic_original_class.implicit_generic_types().end()); - } - if(is_java_generic_class_type(original_class)) - { - const java_generic_class_typet &generic_original_class = - to_java_generic_class_type(original_class); - generic_types.insert( - generic_types.end(), - generic_original_class.generic_types().begin(), - generic_original_class.generic_types().end()); - } - - INVARIANT( - generic_types.size() == - existing_generic_type.generic_type_arguments().size(), - "All generic types must be concretized"); - - auto generic_type_p = generic_types.begin(); - std::string previous_class_name; - std::string current_class_name; - generic_arguments_name_buildert build_generic_arguments( - argument_name_printer); - - // add generic arguments to each generic (outer) class - for(const auto &generic_argument : - existing_generic_type.generic_type_arguments()) - { - previous_class_name = current_class_name; - current_class_name = generic_type_p->get_parameter_class_name(); - - // if the class names do not match, it means that the next generic - // (outer) class is being handled - if(current_class_name != previous_class_name) - { - // add the arguments of the previous generic class to the buffer - // and reset the builder - generic_name_buffer << build_generic_arguments.finalize(); - - INVARIANT( - has_prefix(current_class_name, previous_class_name), - "Generic types are ordered from the outermost outer class inwards"); - - // add the remaining part of the current generic class name to the buffer - // example: if current_outer_class = A$B$C, previous_outer_class = A, - // then substr of current, starting at the length of previous is $B$C - generic_name_buffer << current_class_name.substr( - previous_class_name.length()); - } - - // add an argument to the current generic class - build_generic_arguments.add_argument(generic_argument); - ++generic_type_p; - } - generic_name_buffer << build_generic_arguments.finalize(); - - // add the remaining part of the original class name to the buffer - generic_name_buffer << original_class_name.substr( - current_class_name.length()); - - return generic_name_buffer.str(); -} - -/// Construct the symbol to be moved into the symbol table -/// \param specialised_class: The newly constructed specialised class -/// \return The symbol to add to the symbol table -type_symbolt generate_java_generic_typet::build_symbol_from_specialised_class( - const java_class_typet &specialised_class) const -{ - type_symbolt new_symbol(specialised_class); - new_symbol.base_name = specialised_class.get(ID_base_name); - new_symbol.pretty_name = specialised_class.get(ID_base_name); - new_symbol.name = specialised_class.get(ID_name); - new_symbol.mode = ID_java; - return new_symbol; -} diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h deleted file mode 100644 index c0c7113f691..00000000000 --- a/src/java_bytecode/generate_java_generic_type.h +++ /dev/null @@ -1,45 +0,0 @@ -/*******************************************************************\ - - Module: Generate Java Generic Type - Instantiate a generic class with - concrete type information. - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ -#ifndef CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H -#define CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H - -#include -#include -#include -#include -#include -#include "generic_arguments_name_builder.h" - -class generate_java_generic_typet -{ -public: - explicit generate_java_generic_typet(message_handlert &message_handler); - - symbolt operator()( - const java_generic_typet &existing_generic_type, - symbol_tablet &symbol_table) const; -private: - std::string build_generic_name( - const java_generic_typet &existing_generic_type, - const java_class_typet &original_class, - const generic_arguments_name_buildert::name_printert &argument_name_printer) - const; - - typet substitute_type( - const typet ¶meter_type, - const java_class_typet &replacement_type, - const java_generic_typet &generic_reference) const; - - type_symbolt build_symbol_from_specialised_class( - const java_class_typet &specialised_class) const; - - message_handlert &message_handler; -}; - -#endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H diff --git a/src/java_bytecode/generic_arguments_name_builder.cpp b/src/java_bytecode/generic_arguments_name_builder.cpp deleted file mode 100644 index a1ff2c5a497..00000000000 --- a/src/java_bytecode/generic_arguments_name_builder.cpp +++ /dev/null @@ -1,42 +0,0 @@ -/*******************************************************************\ - - Module: Generic Arguments Name Builder - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -/// file - A class to aid in building the name of specialized generic classes. -/// Allows for custom builder function for a single argument name. - -#include -#include "generic_arguments_name_builder.h" -#include "java_utils.h" - -std::string generic_arguments_name_buildert::finalize() -{ - std::ostringstream name_buffer; - - if(!type_arguments.empty()) - { - bool first = true; - for(const auto &argument : type_arguments) - { - if(first) - { - name_buffer << "<"; - first = false; - } - else - { - name_buffer << ", "; - } - - name_buffer << argument_name_printer(argument); - } - name_buffer << ">"; - type_arguments.clear(); - } - - return name_buffer.str(); -} diff --git a/src/java_bytecode/generic_arguments_name_builder.h b/src/java_bytecode/generic_arguments_name_builder.h deleted file mode 100644 index b27b6b1b117..00000000000 --- a/src/java_bytecode/generic_arguments_name_builder.h +++ /dev/null @@ -1,43 +0,0 @@ -/*******************************************************************\ - - Module: Generic Arguments Name Builder - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -/// file - A class to aid in building the name of specialized generic classes. -/// Allows for custom builder function for a single argument name. - -#ifndef CPROVER_JAVA_BYTECODE_GENERIC_ARGUMENTS_NAME_BUILDER_H -#define CPROVER_JAVA_BYTECODE_GENERIC_ARGUMENTS_NAME_BUILDER_H - -#include "java_types.h" -#include - -class generic_arguments_name_buildert -{ -public: - typedef std::function - name_printert; - - explicit generic_arguments_name_buildert( - const name_printert &argument_name_printer) - : argument_name_printer(argument_name_printer) - { - } - - void add_argument(const reference_typet &argument) - { - PRECONDITION(!is_java_generic_parameter(argument)); - type_arguments.push_back(argument); - } - - std::string finalize(); - -private: - std::vector type_arguments; - name_printert argument_name_printer; -}; - -#endif // CPROVER_JAVA_BYTECODE_GENERIC_ARGUMENTS_NAME_BUILDER_H diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index b10c7b93796..bf226bb38f4 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -34,7 +34,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_static_initializers.h" #include "java_utils.h" #include -#include #include "expr2java.h" diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 775cada45a2..59a2e0e146d 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -127,16 +127,6 @@ class java_generic_parametert:public reference_typet return type_variable().get_identifier(); } - const std::string get_parameter_class_name() const - { - const std::string ¶meter_name = get_name().c_str(); - PRECONDITION(has_prefix(parameter_name, "java::")); - int prefix_length = std::string("java::").length(); - const std::string name = parameter_name.substr( - prefix_length, parameter_name.rfind("::") - prefix_length); - return name; - } - private: typedef std::vector type_variablest; const type_variablest &type_variables() const @@ -457,77 +447,6 @@ void get_dependencies_from_generic_parameters( const typet &, std::set &); -class java_specialized_generic_class_typet : public java_class_typet -{ -public: - typedef std::vector generic_type_argumentst; - - /// Build the specialised version of the specific class, with the specified - /// parameters and name. - /// \param generic_name: The new name for the class - /// (like Generic) - /// \param originating_class: The name for the original class (like - /// java::Generic) - /// \param new_components: The specialised components - /// \return The newly constructed class. - java_specialized_generic_class_typet( - const irep_idt &generic_name, - const java_class_typet &originating_class, - const struct_typet::componentst &new_components, - const generic_type_argumentst &specialised_parameters) - { - set(ID_C_specialized_generic_java_class, true); - set(ID_name, "java::" + id2string(generic_name)); - set(ID_base_name, id2string(generic_name)); - components() = new_components; - set_tag(originating_class.get_tag()); - set_access(originating_class.get_access()); - - generic_type_arguments() = specialised_parameters; - } - - /// \return vector of type variables - const generic_type_argumentst &generic_type_arguments() const - { - return (const generic_type_argumentst &)(find(ID_type_variables).get_sub()); - } - -private: - /// \return vector of type variables - generic_type_argumentst &generic_type_arguments() - { - return (generic_type_argumentst &)(add(ID_type_variables).get_sub()); - } -}; - -inline bool is_java_specialized_generic_class_type(const typet &type) -{ - return type.get_bool(ID_C_specialized_generic_java_class); -} - -inline bool is_java_specialized_generic_class_type(typet &type) -{ - return type.get_bool(ID_C_specialized_generic_java_class); -} - -inline java_specialized_generic_class_typet -to_java_specialized_generic_class_type(const typet &type) -{ - INVARIANT( - is_java_specialized_generic_class_type(type), - "Tried to convert a type that was not a specialised generic java class"); - return static_cast(type); -} - -inline java_specialized_generic_class_typet -to_java_specialized_generic_class_type(typet &type) -{ - INVARIANT( - is_java_specialized_generic_class_type(type), - "Tried to convert a type that was not a specialised generic java class"); - return static_cast(type); -} - /// Type for a generic symbol, extends symbol_typet with a /// vector of java generic types. /// This is used to store the type of generic superclasses and interfaces. diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp deleted file mode 100644 index 8155bdf3ef7..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ /dev/null @@ -1,373 +0,0 @@ -/*******************************************************************\ - - Module: Unit tests for generating new type with generic parameters - substitued for concrete types - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include -#include -#include -#include - -#include -#include - -SCENARIO( - "generate_java_generic_type_from_file", - "[core][java_bytecode][generate_java_generic_type]") -{ - auto expected_symbol = - "java::generic_two_fields$bound_element"; - - GIVEN("A generic java type with two generic fields and a concrete " - "substitution") - { - symbol_tablet new_symbol_table= - load_java_class("generic_two_fields", - "./java_bytecode/generate_concrete_generic_type"); - - generic_utils::specialise_generic_from_component( - "java::generic_two_fields", "belem", new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol(expected_symbol)); - THEN("The class should contain two instantiated fields.") - { - const auto &class_symbol = new_symbol_table.lookup( - "java::generic_two_fields$bound_element"); - const typet &symbol_type=class_symbol->type; - - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); - REQUIRE(class_type.is_class()); - - REQUIRE(class_type.has_component("first")); - const auto &first_component=class_type.get_component("first"); - REQUIRE(!is_java_generic_parameter(first_component.type())); - REQUIRE(first_component.type().id()==ID_pointer); - REQUIRE(first_component.type().subtype().id()==ID_symbol); - REQUIRE(to_symbol_type( - first_component.type().subtype()).get_identifier()== - "java::java.lang.Integer"); - REQUIRE(class_type.has_component("second")); - const auto &second_component=class_type.get_component("second"); - REQUIRE(!is_java_generic_parameter(second_component.type())); - REQUIRE(second_component.type().id()==ID_pointer); - REQUIRE(second_component.type().subtype().id()==ID_symbol); - REQUIRE(to_symbol_type( - second_component.type().subtype()).get_identifier()== - "java::java.lang.Integer"); - } - } -} - - -SCENARIO( - "generate_java_generic_type_from_file_two_params", - "[core][java_bytecode][generate_java_generic_type]") -{ - auto expected_symbol = - "java::generic_two_parameters$KeyValuePair"; - - GIVEN("A generic java type with two generic parameters, like a Hashtable") - { - symbol_tablet new_symbol_table= - load_java_class("generic_two_parameters", - "./java_bytecode/generate_concrete_generic_type"); - - generic_utils::specialise_generic_from_component( - "java::generic_two_parameters", "bomb", new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol( - "java::generic_two_parameters$KeyValuePair")); - THEN("The class should have two subtypes in the vector of the types of " - "the generic components.") - { - const auto &class_symbol=new_symbol_table.lookup( - expected_symbol); - const typet &symbol_type=class_symbol->type; - - REQUIRE(symbol_type.id()==ID_struct); - class_typet class_type=to_class_type(symbol_type); - REQUIRE(class_type.is_class()); - - REQUIRE(class_type.has_component("key")); - const auto &first_component=class_type.get_component("key"); - REQUIRE(!is_java_generic_parameter(first_component.type())); - REQUIRE(class_type.has_component("value")); - const auto &second_component=class_type.get_component("value"); - REQUIRE(!is_java_generic_parameter(second_component.type())); - } - } -} - -SCENARIO( - "generate_java_generic_type_from_file_two_instances", - "[core][java_bytecode][generate_java_generic_type]") -{ - // After we have loaded the class and converted the generics, - // the presence of these two symbols in the symbol table is - // proof enough that we did the work we needed to do correctly. - auto first_expected_symbol = - "java::generic_two_instances$element"; - auto second_expected_symbol = - "java::generic_two_instances$element"; - - GIVEN("A generic java type with a field that refers to another generic with" - " an uninstantiated parameter.") - { - symbol_tablet new_symbol_table= - load_java_class("generic_two_instances", - "./java_bytecode/generate_concrete_generic_type"); - - generic_utils::specialise_generic_from_component( - "java::generic_two_instances", "bool_element", new_symbol_table); - generic_utils::specialise_generic_from_component( - "java::generic_two_instances", "int_element", new_symbol_table); - - REQUIRE(new_symbol_table.has_symbol(first_expected_symbol)); - auto first_symbol=new_symbol_table.lookup(first_expected_symbol); - REQUIRE(first_symbol->type.id()==ID_struct); - const struct_union_typet::componentt &component = - require_type::require_component( - to_struct_type(first_symbol->type), "elem"); - auto first_symbol_type=component.type(); - require_type::require_pointer( - first_symbol_type, symbol_typet("java::java.lang.Boolean")); - - REQUIRE(new_symbol_table.has_symbol(second_expected_symbol)); - auto second_symbol=new_symbol_table.lookup(second_expected_symbol); - REQUIRE(second_symbol->type.id()==ID_struct); - const struct_union_typet::componentt &second_component = - require_type::require_component( - to_struct_type(second_symbol->type), "elem"); - auto second_symbol_type=second_component.type(); - require_type::require_pointer( - second_symbol_type, symbol_typet("java::java.lang.Integer")); - } -} - -SCENARIO( - "generate_java_generic_type_with_array_concrete_type", - "[core][java_bytecode][generate_java_generic_type]") -{ - // We have a 'harness' class who's only purpose is to contain a reference - // to the generic class so that we can test the specialization of that generic - // class - const irep_idt harness_class = "java::generic_field_array_instantiation"; - - // We want to test that the specialized/instantiated class has it's field - // type updated, so find the specialized class, not the generic class. - const irep_idt test_class = - "java::generic_field_array_instantiation$generic"; - - GIVEN("A generic type instantiated with an array type") - { - symbol_tablet new_symbol_table = load_java_class( - "generic_field_array_instantiation", - "./java_bytecode/generate_concrete_generic_type"); - - // Ensure the class has been specialized - REQUIRE(new_symbol_table.has_symbol(harness_class)); - const symbolt &harness_symbol = new_symbol_table.lookup_ref(harness_class); - - const struct_typet::componentt &harness_component = - require_type::require_component(to_struct_type(harness_symbol.type), "f"); - - ui_message_handlert message_handler; - generate_java_generic_typet instantiate_generic_type(message_handler); - instantiate_generic_type( - to_java_generic_type(harness_component.type()), new_symbol_table); - - // Test the specialized class - REQUIRE(new_symbol_table.has_symbol(test_class)); - const symbolt test_class_symbol = new_symbol_table.lookup_ref(test_class); - - REQUIRE(test_class_symbol.type.id() == ID_struct); - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "gf"); - const typet &test_field_type = field_component.type(); - - REQUIRE(test_field_type.id() == ID_pointer); - REQUIRE(test_field_type.subtype().id() == ID_symbol); - const symbol_typet test_field_array = - to_symbol_type(test_field_type.subtype()); - REQUIRE(test_field_array.get_identifier() == "java::array[reference]"); - const pointer_typet &element_type = require_type::require_pointer( - java_array_element_type(test_field_array), - symbol_typet("java::java.lang.Float")); - - // check for other specialized classes, in particular different symbol ids - // for arrays with different element types - GIVEN("A generic type instantiated with different array types") - { - const irep_idt test_class_integer = - "java::generic_field_array_instantiation$generic"; - - const irep_idt test_class_int = - "java::generic_field_array_instantiation$generic"; - - const irep_idt test_class_float = - "java::generic_field_array_instantiation$generic"; - - const struct_typet::componentt &component_g = - require_type::require_component( - to_struct_type(harness_symbol.type), "g"); - instantiate_generic_type( - to_java_generic_type(component_g.type()), new_symbol_table); - REQUIRE(new_symbol_table.has_symbol(test_class_integer)); - - const struct_typet::componentt &component_h = - require_type::require_component( - to_struct_type(harness_symbol.type), "h"); - instantiate_generic_type( - to_java_generic_type(component_h.type()), new_symbol_table); - REQUIRE(new_symbol_table.has_symbol(test_class_int)); - - const struct_typet::componentt &component_i = - require_type::require_component( - to_struct_type(harness_symbol.type), "i"); - instantiate_generic_type( - to_java_generic_type(component_i.type()), new_symbol_table); - REQUIRE(new_symbol_table.has_symbol(test_class_float)); - } - } -} - -SCENARIO( - "generate_java_generic_type with a generic array field", - "[core][java_bytecode][generate_java_generic_type]") -{ - const irep_idt harness_class = "java::generic_field_array_instantiation"; - GIVEN("A generic class with a field of type T []") - { - symbol_tablet new_symbol_table = load_java_class( - "generic_field_array_instantiation", - "./java_bytecode/generate_concrete_generic_type"); - - const irep_idt inner_class = "genericArray"; - - WHEN("We specialise that class from a reference to it") - { - generic_utils::specialise_generic_from_component( - harness_class, "genericArrayField", new_symbol_table); - THEN( - "There should be a specialised version of the class in the symbol " - "table") - { - const irep_idt specialised_class_name = id2string(harness_class) + "$" + - id2string(inner_class) + - ""; - REQUIRE(new_symbol_table.has_symbol(specialised_class_name)); - - const symbolt test_class_symbol = - new_symbol_table.lookup_ref(specialised_class_name); - - REQUIRE(test_class_symbol.type.id() == ID_struct); - THEN("The array field should be specialised to be an array of floats") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "arrayField"); - - const pointer_typet &component_pointer_type = - require_type::require_pointer(field_component.type(), {}); - - const symbol_typet &pointer_subtype = require_type::require_symbol( - component_pointer_type.subtype(), "java::array[reference]"); - - const typet &array_type = java_array_element_type(pointer_subtype); - - require_type::require_pointer( - array_type, symbol_typet("java::java.lang.Float")); - } - - THEN( - "The generic class field should be specialised to be a generic " - "class with the appropriate type") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "genericClassField"); - - require_type::require_java_generic_type( - field_component.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Float"}}); - } - } - } - WHEN( - "We specialise the class with an array we should have appropriate types") - { - generic_utils::specialise_generic_from_component( - harness_class, "genericArrayArrayField", new_symbol_table); - THEN( - "There should be a specialised version of the class in the symbol " - "table") - { - const std::string specialised_string = - ""; - const irep_idt specialised_class_name = id2string(harness_class) + "$" + - id2string(inner_class) + - specialised_string; - - REQUIRE(new_symbol_table.has_symbol(specialised_class_name)); - - const symbolt test_class_symbol = - new_symbol_table.lookup_ref(specialised_class_name); - - REQUIRE(test_class_symbol.type.id() == ID_struct); - THEN("The array field should be specialised to be an array of floats") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "arrayField"); - - const pointer_typet &component_pointer_type = - require_type::require_pointer(field_component.type(), {}); - - const symbol_typet &pointer_subtype = require_type::require_symbol( - component_pointer_type.subtype(), "java::array[reference]"); - - const typet &array_type = java_array_element_type(pointer_subtype); - - require_type::require_pointer( - array_type, symbol_typet("java::array[reference]")); - - const typet &array_subtype = - java_array_element_type(to_symbol_type(array_type.subtype())); - - require_type::require_pointer( - array_subtype, symbol_typet("java::java.lang.Float")); - } - - THEN( - "The generic class field should be specialised to be a generic " - "class with the appropriate type") - { - const struct_typet::componentt &field_component = - require_type::require_component( - to_struct_type(test_class_symbol.type), "genericClassField"); - - const java_generic_typet ¶m_type = - require_type::require_java_generic_type( - field_component.type(), - {{require_type::type_argument_kindt::Inst, - "java::array[reference]"}}); - - const typet &array_type = java_array_element_type( - to_symbol_type(param_type.generic_type_arguments()[0].subtype())); - require_type::require_pointer( - array_type, symbol_typet("java::java.lang.Float")); - } - } - } - } -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp deleted file mode 100644 index d6c8b271d38..00000000000 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp +++ /dev/null @@ -1,598 +0,0 @@ -/*******************************************************************\ - - Module: Unit tests for generating new type with generic parameters - substitued for concrete types - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include -#include -#include -#include - -SCENARIO("generate_outer_inner", "[core][java_bytecode][generate_outer_inner]") -{ - WHEN("Loading a class with generic and non-generic inner classes") - { - symbol_tablet new_symbol_table = load_java_class( - "generic_outer_inner", "./java_bytecode/generate_concrete_generic_type"); - const std::string &class_prefix = "java::generic_outer_inner"; - - WHEN("Its field t1 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t1", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter"; - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), - symbol_typet("java::generic_outer_inner$GenericOuter$Inner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}}); - } - - THEN("It has field f3 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f3"); - require_type::require_pointer( - field.type(), - symbol_typet( - "java::generic_outer_inner$GenericOuter$GenericInner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}, - {require_type::type_argument_kindt::Inst, - "java::java.lang.String"}}); - } - - THEN("It has field this$0 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$0"); - require_type::require_pointer( - field.type(), symbol_typet("java::generic_outer_inner")); - } - } - } - - WHEN("Its field t2 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t2", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter$Inner"; - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t2a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t2a", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$GenericOuter$Inner"; - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t3 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t3", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter$Inner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t3a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t3a", new_symbol_table); - const std::string &expected_prefix = class_prefix + - "$GenericOuter$Inner$" - "InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - // TODO add test for field t4 once TG-1633 is done - - WHEN("Its field t5 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t5", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$Inner$GenericInnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix + "$Outer$Inner")); - } - } - } - - WHEN("Its field t6 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t6", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$Outer$GenericInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), - symbol_typet( - "java::generic_outer_inner$Outer$" - "GenericInner$GenericInnerInner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::java.lang.Integer"}, - {require_type::type_argument_kindt::Inst, - "java::java.lang.String"}}); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix + "$Outer")); - } - } - } - - WHEN("Its field t7 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t7", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$GenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t7a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t7a", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$GenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - // TODO add test for field t8 once TG-1633 is done - - WHEN("Its field t9 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t9", new_symbol_table); - const std::string &expected_prefix = class_prefix + - "$Outer$TwoParamGenericInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$1"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix + "$Outer")); - } - } - } - - WHEN("Its field t10 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t10", new_symbol_table); - const std::string &expected_prefix = class_prefix + - "$Outer$TwoParamGenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t10a is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t10a", new_symbol_table); - const std::string &expected_prefix = - class_prefix + - "$Outer$TwoParamGenericInner$InnerInner"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.Integer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - const symbol_typet &field_array = - to_symbol_type(field.type().subtype()); - REQUIRE(field_array.get_identifier() == "java::array[reference]"); - require_type::require_pointer( - java_array_element_type(field_array), - symbol_typet("java::java.lang.String")); - } - - THEN("It has field this$2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$2"); - // TODO should be java generic type - TG-1826 - } - } - } - - WHEN("Its field t11 is specialised") - { - generic_utils::specialise_generic_from_component( - class_prefix, "t11", new_symbol_table); - const std::string &expected_prefix = - class_prefix + "$GenericOuter"; - - THEN("The corresponding specialised class symbol is created") - { - REQUIRE(new_symbol_table.has_symbol(expected_prefix)); - const symbolt &expected_symbol = - new_symbol_table.lookup_ref(expected_prefix); - - const struct_typet class_struct = to_struct_type(expected_symbol.type); - REQUIRE(is_java_specialized_generic_class_type(class_struct)); - - THEN("It has field f1 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f1"); - require_type::require_pointer( - field.type(), symbol_typet("java::generic_outer_inner$Outer")); - } - - THEN("It has field f2 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f2"); - require_type::require_pointer( - field.type(), - symbol_typet("java::generic_outer_inner$GenericOuter$Inner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::generic_outer_inner$Outer"}}); - } - - THEN("It has field f3 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "f3"); - require_type::require_pointer( - field.type(), - symbol_typet( - "java::generic_outer_inner$GenericOuter$GenericInner")); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Inst, - "java::generic_outer_inner$Outer"}, - {require_type::type_argument_kindt::Inst, - "java::java.lang.String"}}); - } - - THEN("It has field this$0 of correct type") - { - const struct_union_typet::componentt &field = - require_type::require_component(class_struct, "this$0"); - require_type::require_pointer( - field.type(), symbol_typet(class_prefix)); - } - } - } - } -} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class deleted file mode 100644 index 694991b296232ba2d5248935750dbf0ebde2a804..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 746 zcma)4O-lkn7=A{r&2`Jo%D&4;#1BXhol3k2K_C^lc$IM-ZDbo`T?2nshX^|K1Nu?X zJGLImgC1t)eV=*W@AvEb;}gIoGI2z)Zz6^R14jmq86y22L#i?0FTCt=)i2+72Eq-l z8RAXZS3DT|f+6ZSgscXSa+IwwoHzPH317PHo)liU&3&Iw+ER@It^&yeIaHcnl}ZLR zhFpFLexbz>s}H*rE!mJt+>M_)!gqMbBP7)ry4-7VUur!BV>%rMBg}=tx>b}_-Q%N? zppVkxsM*k#vQ7UDF?pVasVwiNN^Po!38Eo|$B9+ZVR zObZE|7&v7pEVP=H$zcBI5peQCtT4!zMZVj8=oMX-m| L^p}djAvS>@A2-7X 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 184f8383980052e6d864c8b38d7bdcd1a9adb057..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 974 zcmb7D%St0b6g}0Qu}#cq;%gkonTZ-hR8SYX8AD(Ygn=*)7~HrBl~@x?+KO~{1V77# z2rm2pKT15+b_8|NaZ!(Z?>YBXw;mqv?g4D0l7)*OIb`tD!=i^Jft(Bid9|;VeC{OXiB5G`-V#_&=URA88y(dJ zD%BzIt4Az+uXn=wCmPzQzy0&J3YxO*Q#0A-{6w->WzphrNE#QTy7KSxJ4s4Ldq{OrVfQ5oHf6 z0voBUS4j#K-p-%E>d-y}+^T)6#Z(4L{0JHT376{=M!?zS&A}-5EIz-;Pbsa6R%?G#6roMThrUT@2!@1&v=21C^non6oJ-EVM#xxM}a;4`XuWKedo@8ZBkg;4OMmZ2K8!chEV z*wqZ%zK9|jxi}=aNdke!gipN$4#rCQ=L2DB1EnJ)v{AySK<_6RCxo@W^0YA1P!hf@ z&TRbXO~jR``$Bv5jvokf(quLA2(ABA>1rcA8Q$q!5bDe5bmP<2lB|wpIf9#3oV^cW zGu`-(Z6@J(@v7qg#Rs&Pq%XcGDvOg~)?BEFP@Z23pOo(h({Lm^%F0#d4(pK}v;tn@ z6`?dYo3QaPnBRsIIWmN!xwL;TB6(xAg$XFZ;r9x-yw;Eh;R$;V3T&UI@H58iDZIgW zGlh$cx3J9?c#fTWon6K+Qh1Md$aaJ6Yu>BJ7|4D64f@3a2XEM}a2UMavMt1Z4)5@u Xk;5fh`+;+SB70e0Ird%tt^$7nRpL&| 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 1d9fe54995c41473bf2672c2c508fc9c4aef8038..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 751 zcmah{TT22#6#m9FH*M2R%j_;;U`9&NOS$+W6v2{#mseSBu#s(z-8JZE^$CA%6;fCsBpD 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 8f6d49bec1f34eac75ae7bf452a6d39aa5d135e8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 825 zcma)4T}uK%6g}6qHaE*n%f8FX!W0y%hamAqC<3V<@l{rvY{b@BcY}Ub4-xdx59mil zcXkyl1bf&!=iEK_&Y3&&_5JY)-~{^-XxK0i#-@%f9ovM^eUT8acC2Ts(6#J#;kwxo zE%%HNxs`3(ay>^7v|5cb)9!=pr;l{(5TX~t7LIIPd#-SpUfN76U8~<0eI2`mDL+HV zRNH~F(NoffRKoOVb=p^|{v~Nkw@k?WyXde^2v>S{>@ilAwz%>ho5HDC%`Ru+)n3c$ z)-6XWK1hbuAqa-Q>A>UhKRpIchjx>{+rK;ww>X{HuEg^!=lw=O9QHJBd!Ex0=TiA! z88f-Ox~V84h(%#yk5C*V8Z+Jz>jd-fb?ZnIQj(W#>AhA1zzKfZdj?bMmF~b%DyA?%1lFoqpAj1Epki-DlB1{8SDLS jJVnM)UuW>YRc0Zq`Ei}|V63q=g;~aPjOKaO7$t!pJm=Uv 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 bc9fa9be68599fa59170c15aa5018d24295ef73d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 826 zcmah|O;5r=5Pj2vm5Ne95%CKZ6){3E-ZWlJG$ce!AYM(u1=nCPrI`4$JQx!X{s4cJ zakhm-4M`6>GjIC#?dx>=_5JY);23)`=vX%q!G?jHflUM3g!rX!ge%+ip(k91Rfpku z&mIiKfDrYefjq(VOFs~_PKA)HJ=o87xo11wa=rB++TIBv){tGt_J*z?=*=c~w9XMB z^^03|Jkb>{KbrFHeTeWUrDS+)Cvl|J#~kpGrr1XM~+XIDP+y5IOJPv5iDc zI^t^h*b;8jZuPj6to7S=@5Xke!lPzHnIVL0=lvnDq4Zywm#4ARVW_`T9?e;4EMzwN zL$@t1q%xP8Fp83zbR6?Y#*xAfVRr)Q&%6SY1nd7dGO$a?g>5HP!YIKBK^$ERy`aXP zny?c&zI+kBhdQqr#6g(lO2Zt-1T4U^)ax-KUMVbaUgYYUIT~lPc<=@)zC(Luq$AC7 z%I8M0#C1AgA%kT`%=gs@S+3P-s*}MAXAP@Vbl_=_4GLKqj{(V zZof~DGkPkhcgKrlr&E*dRGVD2JT=R{C zZ;-}!IA4ie+~jlBa$Ve_U0$%TjoU=zTQ$KQ+NKKQ*~VS2Zd_3n_lO+qPzTg=c|E`i OZI9L^uI87J2mSyT+8eO| 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 be2037c6c8873fa2b5d6a371fdbff5143c1e6b41..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 929 zcma)4T}vB56g_u0y3M*ZF>3s3)z)aEf>QB8G~~rnDTG=`^i?)-j3eo$Y&L>F%LfsB z@CW##if7gciHVShnK}2&xp(f|d!PP4JObE7J_#F3E)rOF@WsJbfpzg+kSSgH*Zy|H z59-^;)hktt4g|@vt_Ob94wb;JRLEEtI|iN*jz*WdmD_QU6O0_UBNYm~UqPV4!-n5# zsg{FPGDnJxuEiIEe5w9opEZrgnKt@d?49dYn)n4B=%^^z9NKC9RFF7qo-^H4NeAk8 z`)^f+6~EdblPNW8e&f^+wXr*7!hAw7(fxKO)%_t;?a4d#W%AkH$8P?;KKNtEs0Eh0 zxYd_dfu%1pe!g(B-`}xfKP7O>&30H*KeZ{s?11ubna+C{!-R(n)&zS4L<4%%|8YV3 z?G!oqCYXCSpkVFYyPo)*y1Z%c>AyKFa|Hs2>p3LA zoFe)|t;N&b*t~;m+{3!1Wn-GVi3Y4A%RT#|!VKnUQ6EPW%oBUD&gI<#ExVJ!Cw!)5 XVG-jz=gE6m!AIg0Q94$pFbg~bq+9Y< 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 36972ebe360552e5d277b3381c4a95fbadf1d6e8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 818 zcma)4+e*Vg5IvKm#>Q%6tMz`5Qd>~GJP3*}1w{xdSo&Jhy4IDLN}39OmJcHM;0O3o z;%uzgN`*e`?wQ#$vu9`K_vL0U$ z@^0hXt~OOfRVuy{M?2k2mH$WvGCC#{2M*e-5R6junl+|f8Hn@teNBXAujaES<2LJ_ zU-3ez?2gk=pCDMVypG1b0W~_mK`b}doBrwH=ZS*>(;abDkGFbqT35|>SQjT!>7VXX zxh>VH6p~1%U}KH2(}&cjyj{`>_TP4!a0oO1W+H6-d)L!Mo|L?5NwyCi%RGDr&!NUE zfgupg*c!HN^&iH>%f>jL8Ag}PR9vf2d;t|+p*^#uBg?yr1{_TAp8IBD5>sq3KhDPG iW1Nb47T?XVrC~PS=hzR%I&+sX!g!R?7@s<$9PkBgpw)>0 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 2368c6b18abecb67f59d4a944659ca6a37f03e96..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1031 zcma)5T}vB56g@W|u5Pz&G;RE9)yAk%sUq}2OvsC1DTG=`@KrYHG>*iLY&JrFmJcHI zp+BHMs`Sic#Vk$4hnaiN-E+^}xp(K!-(SB0e8Tn&(pYto!J2~)4vG#+g6!!aQlY^6 z5(Fwd?)v?{>Jxregt~2`4mJd{qmekgDR8Z8H$m#hf#9g#8Rnk%jP$uS!XVbvx*dA} 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 af00787fbf9d3d4f96a81cbe376b29082d8ff9f1..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 848 zcmb7CT~8WO5Iw_(E8A5UsI+J+erye;i3IIK(-K}x+L(~qM8d0C@QRnvrCF9H{aJlz zOnmSM_@j*HE;MNi#Ps3bJ0EAx%$=FL`zW?2? z4*Z~3J?->WH~JvRoatWRN8?ZllC2gkOVO1cd50Eu1?kgqq(Xsn5(Fwd9{8h?8d=z* zC$*dhZihot*Ha`dHl7b!j|6| z(2{EoyZ)fe<^VP-31G;1jU6+g3?0Y zWYFB7vYB3f4i4K~$rQIU!IQ=k1XipqyRP{NW#Ms=<(s4Qg-C<7D{p>5D%VK-q?SaU zw}}Q`;3@CI1ch}xqegtp#=cQ@Vw_E1ky>(^aRZyw5{!5FZqROH2Tv%kP+EDn 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 d481c3322f3bff43511df16204c9f774d4c4ed36..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 769 zcmah{T}uK%6g}5fH#f^o%d#)EHZTjN=q>Rj2m+}<@l{qEY{b@B*Px%(Lj*na1Nu?X zol&7e>0$4jd+(VuXYb7C*ZT*6GaSTVVB10%J0^BbWC@`lAS7!&_sK2yU9VfdY4=1Y zI48vFvg^6Q$QJ~o(cnrnxR*oc)I^>Txfun*C&aHjPxu#ocQ_P76MNjz6+*t&72J}Y z)<98PQV|`!&CwL4SdpF#ssyL-FZ-}b2wx2D*iND*J#jsHXbZpLw)pnkDwNK{jRCrj`l2#bUshCwCjQozcl*;kOjOmor zHN+7^A`Tn-gyIa+&k_DGOR)c5q6vqPnJYoa&h3qb`Qi&|?5P<%sT*8U+oUc2FAv7VgFnC@ zWt?rj31-uoH#2YE&hGZ>`{NV9CEDA_p=LtIfq}Y#hJh9#KUpOrB3QRUAfln~#<7Sw zorVSu3FVRCiuBSAnY>MT?`GpSUZRP%~y*D{dFfN?) z5K3bih`ZJETtpA<+~-VX9D1%lbt9?b-=wa#C!B5;b<#n31oJ*zMV`2kO02$S*o&q6 z;#$~&Wub^8LVFDp+1Z0sZSH`X#uXY}`ua~*Xt)is?s z;g{6;QOUN|;0p0q#4h_1qX9HtfZ08N19jh_y>g_%W?M+PO_UkeG8QVRa>V>pjX1l< Xk%oO3?3=t>o^64#LR;+BzhnYGaG94H 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 d7e166e8c9a1e2daac85d364a32f9b75b6417a10..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 904 zcmb7DT~8BH5IwV7Si7uJ3sgQt0apb~3IZ<%!b=m3NdqL*zLMK|sh5;pvfXO@Sv(LD z9{2(LDC4;cL@2c{FLw4Z2!+xSY4bF^k*lW;iwZhGOGhc|+uy?&|_LGUGtbW-c8 zUQhQtgo5$L&v;)Y>g2QLjcI2Ag4KHG#y*T~=Ap59Va5{XW!QRKCNk-^V104Wa8@jnTS^^lty8rIUtgb?GVBnzyj1b+71+c$3xST_8d%;#4gmicvh zSE@E3?G^{Y0c=+v(EA5*KWXb7V_TZc`M6a(-vA?c9-xf3f=@X?|CzwOZUm)&m&L<7 z!PKLSg6gApx%1|dE!wG#<)mSbD_r0&-P0t+b_MsQ^pweIMF_1 z9cq91!#QO60?rvN7Za40&Hg79%F0a?USNtA<1;qFG;xr{`MjH<<=|x|XYq`Bnp^=E P@RWFzs6_1&O#*)aQ*G|r 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 8ce274e530ce1ce6d4ea37986fefaa410410220d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 911 zcmb7DT~8B16g_vhWuaCnE!G0chb&kj0U9fnc_E88%gxmmg@A06dPez_1h{kHogTjHof50cu_yCeO6TdQ|{~M-;!_s zQ>(_2a1?cF)@sM^?oY6tg4OTScppdMFzV`kW81ByjC0H0P98HT=261BU@L_*nt5v5 zg2LbT>*0l9Zmf*p?bx%_6#m^ePqdJZ0OpS}|p3I*FQ zQQ<0Kmi95dCb6Y**ed=VR#)#Mt3XrsqwBGZen9;&n2vN)k#@a<%YqT-JE>mi|QE z+DgWX*jjTYUPKDJ*h?XeijGr4F@jqu5=_On9N|t|{qamr0zz{mUW@7^;cWAQ?w^(u z%A3J;-(z*vxNHQ63SW7gZ=Xz49Zz{Y(lFWXv)6{kA7C^t-a(BIXm1>8$nZZIvKF%J p7giK<$aBPes79PEaHQdYX`srrVmL&CeVx56w(8LtYkQ_`6<)!*flGd}nO z{85fyE)5&IZQ6(K?)mmR-z7QO?VrEDegjy+=Lmv$E8(4lf`s=B;lqZZ=nT=krYZVv zRj${Sx`YF=qp(_k&U&2=5QvN0< zs_@2F_#s#eKl?Mm#i87XL_sJDIpczkc20tSo~2_LTI z;`EvD&Crxhv$8W^hOkFRd{z|R!Ke@bKTEZuWPQCLfy?X4_JI@kk|6h=45@cTZ@&)bivUFduH)6n8 zmvF+c*=0yX=!aLO=x{JnN0>+%&(WLWA@gor^APkW?@ z>gP^1uGXNDT#|6ckm)gnS30F0* zrQ|K4hqYy0d3{@|rW#p>;M_dvH?&*3peuBsplZrN| z3>jb5I>VSK2k9bGtTptqvZtB>#w)G2c-*{(qj-r|3?qVlhQaHL`ml7VlnsUnfn&^S zh+#^!m-GCmnDuk9rNfZy&XH3Z!=f+8DaN@4CPn`C3FLSPtKd9Z4-y7pi#ErbzC&={ z(bM93`;t8z9yqmfign;T5D^yiRxn z85eI6-sW(Y@DA7C3-V;<7e(VP?IkP>gcp8-{UAdCuW9TfGwAn*#;COpV-GoNf8QGO z - { - 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 0e61e55d0dea065a0a62964d01ce3c42dd73a3d1..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 699 zcmah{%T5A85UgQQWL*_e!MA8Q04CzWlM*f_CMNhud|b)0j5ubUHM@((&+=eQJoo{A zl(7ahN-*&-JzYK3T|GVX{_*+-UNT&XaM1+tAB_uj4guI^Ni zySFVF?g^yNR7bmUHd)G}0FGkyq~S4#Tr$PjBv ztGF(ZFa1R*UkW7mgEmV~HI$Zp(Q~)uGm>otp6g$_p)&X@m^6X{6Rn`D+fC`qTdCQ( zbEv7l@4HbXdA#w5SaBeQz2ye$Ki++7l>g1H_2y7#kxGpd*&Uu+{a5IubtAo)Wcw`W zhMqi7=6d0voMWWBJz9H f1m@^FJ)X_89Fg_aK_2r&2`pfy$LB4uj4bd8Mnk7< 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 5d14a465aaf2fc9af840739223d64c194b918e84..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 495 zcmah_O-sW-5Ph3AjjgGzwOWrV9<&E@5j?c?QVT2f3K(z$>;)0)z0EVGO< z0Xr}ifipiM##Ok?Uy|jcqIi{^Z?%pDnsXItnHMPu-2B@x_Sf=Rda=}zH`6&ql#V8> z(ikhP@`*t0;&LHSpC&8T>-b93U9kx$eUL%SNY76~882k2O#TDb^C!h?_y3sA(ye(? zq#@lZ(?6*G=*n#5VizvUSIYw3-<9u!HHCbzlPYifFgS(9M+XEy2RrPW99d{_B+M|j qZAQE@2khY+#A`{}W7}ZZG { - 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 3229b26a8326ae4ab6b3afdfedf403cc75933b23..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 664 zcmaJ;O;5r=5Pb{PN~uy&Kv9GP2gF1?cv8ZJ#KeTC2@O}W)D12vi)o9-pXI@rc<=}K zql~i%2c>%0-I>`p@6E@@=i57gQ&dt&V%LI!qKSPIB?d$IV$6{3jQ9g@_*@Me*MpJp zqH~5+R}K}Arh#Bcx-LalqdOT^PZ$cFp->`_UO#%A^rZ?Tt~?QHNK+~qwHS)EKQMC2E=9M&&^XbS2{6L`;?rn2m^u5sS30-X-oqBzu7}~As?j^N*y>?yoRJ6jCe#{ zX|rDWk0BFnD4;kWQX49*%t)Yoc0LoRjH7$LsOc(AH|f%&_)dBuXWDM$%Wx)RmEl#g zVjdJfzFT}hpJ-2`H1_FQWg~ipnp|d&YhVl80-ZvJKx-|)t+ybb^*<`4ehZ8fl=$nw z7O=1Z7Cc8b+xjou;0m(k?3)}p?6XYu;sxTFgA!V7Yk5*&hvTo7D%#l1>wCHFFbA-i JSK*#2@Cl)umY@It 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 8c4e5674b68c64a89a6fa4994461bb71e705fa64..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 743 zcma)4%T59@6g_27WE=%i@qrIiOnk)0!j%vJ<%YbId!F>`duP># zs)c!h_=T?fGVBD3v`UGQp*!hyddMXj4zG1Pw=XbTt}9;!x^@}fw=QpGAe$;wLECT& z+Sg%GAhYooY10*m9<{Ehn<#5vopzd46;x!^V)uiXjKpXrSjGDv(PDyoLQ_#88 z0pW?yB91)SZY!Ry|B)}(e~T5Szh~&)er4JDk3fNQskr$fg$jkz;qNiJ17gMBGy(gf z)d_0qSev#pg9o~6Udh2I90y~_#;_u=HkkUYO@ZXk_vMprn8~LHUq_ZdCCX1@aSdS@ z0x^0KjL^pWu$@erdKeX4V;JY2pm$DgguA`9{Rpx3gvbMtg(R&}Gg=e0=?@lCm?k2> gr^dSIJ3XGwvl$}mvw~U75k)YMsUDx5U=fqRJ8HeQtN;K2 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 2527db386759c91ac8add3793ffa91cf4399cdc1..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1009 zcma)5T~8B16g|_g-EJ3wf<^HQg-T0>BH~98JNPdh7|)b%#A_~na;vT@{5^+vyQ0gGXnO4?L*8l$3QPMS z_~0FMxX;@n5Po-Mw79~MuFICogPt!KtpBOmv5xo&FFV|AmFs~o-Bx8JQgs8-5`JZu zpi?{2mBB7UyijaVV|(5^BAK?ND_-^5P2s=cO@|^`%d@%D;J#G;Aeac=OPc1|B`pzr z;;`r14D*HJ2>+lX21dZSao~RE0(`0-aQpZr?}TKeKZ8;CdcG~5OV!bh$=YqG$xY1T zD#P;Rlrec#>Lx?-g>W3t#6xVEc!X^ekFmutJJfNYnu#ZP$}lth5RF5#*1Qg>k(*39 zR#Iyo2|J(}3YSTzE+c*{`bzmBRa8g1YA5P#)eecSP#x9w;%;f8Foi*vZV80Kg}=|+(pS!Fs^PIB!V*yk{1f%a4wq)R8;j1q7ii{#NbxJkPz z{)l)8xA_yXw*(NkO4-C2k|q5+QfJUgU!a{s|BAHs2^sQ|=P*vQnNzAwK=CXR6JQ{X z45o=`ftt>fwN8yH?p%aF;7(%|x58m=(>K*u6qzII4n=gZKkDaPqN=;($8e9Z6h0%{ H#1-Hl@AB%M 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 39888ab1dbc0313dbadc8cd262d7bd3be8dc6cd9..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 738 zcmaKq%TB^T6o&tyNChh(3JA(Y?E*0o7p{b`A(5C6HG!}t1qK`}gDFMhW4SOUE_?tV z%6MAAL@h36=KQDMxy91MUFwS_&`OTLFFbNb7?bZ7gBPo zW*XBepEBecLrz-sIx~4ICl9hS5ZvtRbH2J^Y?3u+G^#AEft5vR2NWi`kQ~iV? z>CHPxMMz;+8PbI%%we0sUz_x)Y@{J1znqP`+-ezJlRUA;q-U6I!xE03JN-^s23BWC zc_-EDR66l9_VI2JpIsKTxL2XlI%|xKd!u9;a#*_Rj(E>5SO2;gLe0s{>hW{ober~^ z@v)OhgNAhtVeF~cr-6BrI^8JxyDme<8~*;)O2L_7+>=6{9*dvejgQs}f}oaNwHA#! zEs@P=g%P1MO4c=z4jU>SJ%bfr;CmvaV1xF6%lZ%_JMl$f6LC_+yV+>!WNR)LqHjr3 Z%Dmz>QlxxHW0lSrSpj6AxBb5Pb{C$#Kew0*WFO6o`pfSSg_)F)_KQ351p`u;SveXO26KKg+_HSoj0{ zQN~$>LP3k2osT#3=Huh@?H#}gN(n@&9+vJG{w{lWGX2>~1p@c8{-B8^r?@@Jcq;LlsQkO~w4TgN>56nS_ zXq(=Es-_&N#AP_{3BS#IE_u?9*XM4B`%>F8XH3&F7`j)X0tV|s5qs0+lZl`}aXC|Y zhNrHwKg&Md&r6s8Pp#9~4a%?7+oy{wYAm`K%$67WeQ_@JIQgY(I?~Iwkbr3+iG2e_ zhQd=0outmzGDR}`je?C$vIsw|#;`@YuBAOTGW17hj9KK!ieMY*X_OkrE;fKK DdrzSq 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 73db45376b9a53d426d4f37e50632ae73abb1191..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 405 zcmZvY&q~8U5XQf0)2_y7YqSOg!Gj0&U@qPiF9nMb^q}-wHtATmrW?o~eJ)Re2Oq$P z5+_kSWnpH%{pQCkvtQpIp8(Dgxah)H*iqP37!eewykc7tyc=sdAE&w~xKP+5(1g&x zG}e??gzoXll;DiBITHqvv3y&tV$L6QoQmT|S)$Xa&P{#)GoA9u6oepJu#7gztg_EG zd$qGi!|D8j;NE9dp76D)N9?y!XG{H}J*>kej9Ll8ux7$k+eLU6FFBEI4qDNp|80Zz z{sf2U$QRXzB;;AC8=^v~wbMI&2fc~tz?0l>Ov0vU?-#%p22Fq1 { - element ref; - } - - class element { - T elem; - } -} diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 73f1331d5de..45ccd69ec7b 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,6 +1,5 @@ SRC = \ c_to_expr.cpp \ - generic_utils.cpp \ load_java_class.cpp \ require_expr.cpp \ require_goto_statements.cpp \ diff --git a/unit/testing-utils/generic_utils.cpp b/unit/testing-utils/generic_utils.cpp deleted file mode 100644 index caa3f8db341..00000000000 --- a/unit/testing-utils/generic_utils.cpp +++ /dev/null @@ -1,62 +0,0 @@ -/*******************************************************************\ - - Module: Unit test utilities - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include -#include -#include -#include "generic_utils.h" -#include "catch.hpp" -#include "require_type.h" - -/// Generic a specalised version of a Java generic class and add it to the -/// symbol table. -/// \param example_type: A reference type that is a specalised generic to use -/// as the base for the specalised version (e.g. a variable of type -/// `Generic` -/// \param new_symbol_table: The symbol table to store the new type in -void generic_utils::specialise_generic( - const java_generic_typet &example_type, - symbol_tablet &new_symbol_table) -{ - // Should be a fully instantiated generic type - REQUIRE( - std::none_of( - example_type.generic_type_arguments().begin(), - example_type.generic_type_arguments().end(), - is_java_generic_parameter)); - - namespacet ns(new_symbol_table); - const typet &class_type = ns.follow(example_type.subtype()); - REQUIRE( - (is_java_generic_class_type(class_type) || - is_java_implicitly_generic_class_type(class_type))); - - // Generate the specialised version. - ui_message_handlert message_handler; - generate_java_generic_typet instantiate_generic_type(message_handler); - instantiate_generic_type( - to_java_generic_type(example_type), new_symbol_table); -} - -/// Helper function to specialise a generic class from a named component of a -/// named class -/// \param class_name: The name of the class that has a generic component. -/// \param component_name: The name of the generic component -/// \param new_symbol_table: The symbol table to use. -void generic_utils::specialise_generic_from_component( - const irep_idt &class_name, - const irep_idt &component_name, - symbol_tablet &new_symbol_table) -{ - const symbolt &harness_symbol = new_symbol_table.lookup_ref(class_name); - const struct_typet::componentt &harness_component = - require_type::require_component( - to_struct_type(harness_symbol.type), component_name); - generic_utils::specialise_generic( - to_java_generic_type(harness_component.type()), new_symbol_table); -} diff --git a/unit/testing-utils/generic_utils.h b/unit/testing-utils/generic_utils.h deleted file mode 100644 index e0d36d7beb7..00000000000 --- a/unit/testing-utils/generic_utils.h +++ /dev/null @@ -1,31 +0,0 @@ -/*******************************************************************\ - - Module: Unit test utilities - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -/// \file -/// Utility methods for dealing with Java generics in unit tests - -#ifndef CPROVER_TESTING_UTILS_GENERIC_UTILS_H -#define CPROVER_TESTING_UTILS_GENERIC_UTILS_H - -#include -#include - -// NOLINTNEXTLINE(readability/namespace) -namespace generic_utils -{ -void specialise_generic( - const java_generic_typet &example_type, - symbol_tablet &new_symbol_table); - -void specialise_generic_from_component( - const irep_idt &class_name, - const irep_idt &component_name, - symbol_tablet &new_symbol_table); -} - -#endif // CPROVER_TESTING_UTILS_GENERIC_UTILS_H From 2964910f792720ec6c17b603972799c777780389 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 7 Mar 2018 16:49:06 +0000 Subject: [PATCH 4/6] Fix a bug in function for extracting generic interface reference --- src/java_bytecode/java_bytecode_convert_class.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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 = From a1e9d00b737f3db7c35ec1a6b0b8c46edf5fe0b7 Mon Sep 17 00:00:00 2001 From: svorenova Date: Thu, 22 Feb 2018 17:51:53 +0000 Subject: [PATCH 5/6] Updating and extending utility functions --- .../testing-utils/require_goto_statements.cpp | 286 +++++++++++++++++- unit/testing-utils/require_goto_statements.h | 26 +- 2 files changed, 300 insertions(+), 12 deletions(-) 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 From c53cb2971b2186c620fd1a90efcbe56408e42853 Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 23 Feb 2018 10:29:11 +0000 Subject: [PATCH 6/6] Adding and updating unit tests --- .../goto_program_generics/GenericBases.java | 123 +++++ ...s$GenericInnerOuter$Outer$InnerClass.class | Bin 0 -> 810 bytes ...enericFields$GenericInnerOuter$Outer.class | Bin 0 -> 1000 bytes .../GenericFields$GenericInnerOuter.class | Bin 0 -> 1137 bytes ...GenericFields$GenericMethodParameter.class | Bin 0 -> 814 bytes ...GenericMethodUninstantiatedParameter.class | Bin 0 -> 820 bytes ...ericFields$GenericRewriteParameter$A.class | Bin 0 -> 871 bytes ...enericFields$GenericRewriteParameter.class | Bin 0 -> 1126 bytes .../GenericFields$MultipleGenericFields.class | Bin 0 -> 796 bytes .../GenericFields$NestedGenericFields.class | Bin 0 -> 753 bytes .../GenericFields$PairGenericField.class | Bin 0 -> 759 bytes .../GenericFields$SimpleGenericField.class | Bin 0 -> 786 bytes .../goto_program_generics/GenericFields.class | Bin 0 -> 908 bytes .../goto_program_generics/GenericFields.java | 98 ++++ .../goto_program_generics/IWrapper.class | Bin 0 -> 270 bytes .../goto_program_generics/IntWrapper.class | Bin 0 -> 273 bytes .../InterfaceWrapper.class | Bin 0 -> 249 bytes .../goto_program_generics/PairWrapper.class | Bin 0 -> 489 bytes .../goto_program_generics/SimpleWrapper.class | Bin 0 -> 527 bytes .../SuperclassInnerInst$Inner.class | Bin 0 -> 670 bytes .../SuperclassInnerInst$InnerGen.class | Bin 0 -> 788 bytes .../SuperclassInnerInst.class | Bin 0 -> 792 bytes .../SuperclassInnerUninst$Inner.class | Bin 0 -> 766 bytes .../SuperclassInnerUninst$InnerGen.class | Bin 0 -> 899 bytes .../SuperclassInnerUninst$InnerThree.class | Bin 0 -> 633 bytes .../SuperclassInnerUninst.class | Bin 0 -> 928 bytes .../SuperclassInnerUninstTest.class | Bin 0 -> 1109 bytes .../SuperclassInst.class | Bin 0 -> 491 bytes .../SuperclassInst2.class | Bin 0 -> 455 bytes .../SuperclassInst3.class | Bin 0 -> 477 bytes .../SuperclassMixed.class | Bin 0 -> 675 bytes .../SuperclassMixedTest.class | Bin 0 -> 579 bytes .../SuperclassUninst.class | Bin 0 -> 592 bytes .../SuperclassUninstTest.class | Bin 0 -> 560 bytes .../goto_program_generics/TwoWrapper.class | Bin 0 -> 488 bytes .../goto_program_generics/Wrapper.class | Bin 0 -> 425 bytes .../generic_bases_test.cpp | 414 +++++++++++++++ .../generic_parameters_test.cpp | 488 ++++++++++++++++++ .../parse_derived_generic_class.cpp | 34 -- 39 files changed, 1123 insertions(+), 34 deletions(-) create mode 100644 unit/goto-programs/goto_program_generics/GenericBases.java create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields.class create mode 100644 unit/goto-programs/goto_program_generics/GenericFields.java create mode 100644 unit/goto-programs/goto_program_generics/IWrapper.class create mode 100644 unit/goto-programs/goto_program_generics/IntWrapper.class create mode 100644 unit/goto-programs/goto_program_generics/InterfaceWrapper.class create mode 100644 unit/goto-programs/goto_program_generics/PairWrapper.class create mode 100644 unit/goto-programs/goto_program_generics/SimpleWrapper.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerInst.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInst.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInst2.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassInst3.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassMixed.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassMixedTest.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassUninst.class create mode 100644 unit/goto-programs/goto_program_generics/SuperclassUninstTest.class create mode 100644 unit/goto-programs/goto_program_generics/TwoWrapper.class create mode 100644 unit/goto-programs/goto_program_generics/Wrapper.class create mode 100644 unit/goto-programs/goto_program_generics/generic_bases_test.cpp create mode 100644 unit/goto-programs/goto_program_generics/generic_parameters_test.cpp 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 0000000000000000000000000000000000000000..faa5d2304eaec2f269d4282cd741a113ac92364b GIT binary patch literal 810 zcma)4+e*Vg5IxgGV`J1NC2z6hjy>hpCTM969|ZloTtcnCY}U6A7hB9mf4u+7u-9L-1OC=}B@3d4nPC1Nv<8c?+#?WSy$7Q+KVFp0WE>+IHcGs7D(_#8&j1EN&{8yH znn^dT^BQtX<17n|E|{5c_44*JsQiN56C(u^EE8|w5R)v69TuiA&4~GFG{Ow)M#|Iq dZI)3EbE%wXJ6KnkyMkfXM_3!>TVbsT`UE^;&nEx? literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..fa60ef8a06ee872a4b255db9cc573a05e3a43425 GIT binary patch literal 1000 zcma)5T}$IY6g{`8jg7IbA6s4B^)qUX(yk&bY)fARca^d}v3RFYKiXZaut zyWkJ-M=jooStR<95|}&Z%sppr?q#0-{doj%fSo*YST>+zMaQZE4Qq;7*J0_{(6L3B z`Yt@-%igia;dB@ZpI}Dd&~<`91cb4eHeP8a&!uqtg#A`*aHMcxy|c3-we_m46Y_0& z;W^>Z7lf~)88kYbdb65v$%U6Pu=WV6X%>8Ct|2`cHVIZGHGBJvkUbpqxw>LYdgABs zx-0yS({-7dZVh^ld*=93;h4;-QV3gV)-TQAa>_}UyPN+`yQ5h|?O>luqw}qG<=i?o z*YPfDr`;>j3+v7I6v1c@hJH^R$>=W!Wm6H}NrF@p->OX7Hhp(@?BiAfX)8zYGc zrMGqKunEg4YJyf#1F}=+7&lubPbN&U!jC}b7m@)Vp}=b~LZwnkHG%iU-wbAX{lKV? zEaw7cd*=aU|3=3C3+)$gvJV)$=MxQOUJD$7AIRgFbtjlpninPJ@sW|j>IT9B?@f-1 ina3hWEw17dJ~PT-2?oan=Et$gp5Us-F%f0vl=c}BsRtnd literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..26460abadebbdf40a17c499562c0ac2bb30fe498 GIT binary patch literal 1137 zcma)5U2hUW6g|TN+r=%VsFnIvs*9yi3pTz%(4S4{Q4chQ|wqUQOsZg>n0v#VBn#}$+1wvBNJs4 zn*z%(WFSMYyB}~l7)CM_u=QrwcLxJG5J-*P>F9$uaOwg}?QzhaC;j6=Lm=Js0xxO_ z@ZO%v2Y@fR4Zq0XtUTr^!WKV{T7R6hK zUN3N?VaP^2o3n&}bE&#Ahy7vLm3yAb7Hwov5h%ru|JN=BuG-kbwuzdJ zRn$#95m=iMERdVjd(b(RUG~r@D~-;~D)kkmPSmqvNt0(Nurpt?ok|WJ zLg6}Ya7VmmeWtk1_+t&Og>Nw4lPdXg>jJ4N#|6@tNGoOoiaD!suVLX0ZsD!Y zP#nen$xz@)f&3P=uF^{2HY07VNuAxHb(fw5?s44L)*5wzID=JhFjD0+agA$<)?Mj`m>Ng zNIg`X`B8`&Hq$iYCFZ5AlbSY0+w3bN|{3{r)Q+0>m@GX-l9kKNYCp^Qg{8eFPAlgi9aI~tj; z+SAE6GGkpom1ok$By1NBmMwg7QN@bDWJ>3vhPs7Sfwb%Y3rW34qw^VZBaq?o#;?w) z>c%vcD$DRPy$ehn@n(5J4=boaq3JZKC?gkT`aKqXB;orknyefh2UDP(k<}nSiPY+s z5Vb4h&XXLE?jq&z7kokY+_-KUCGr@7(TEbSFhg&QbvVZI>KDjgqu|e6VuIoFU^pj% t_(rK)_aHr_kRE1a;^E3bpppTz+o zap(`=N1=|FwCbWBIM^D`ym>QkJogWGzX0suV+jSkbuor_CA`O+gLwxF3`KJxliDYS za{G%=Ld#%Zim;zFDAbfnnifN){v@_~%uv{i`ogA3CB6*@J)yh27m}yajshMYb1m(A zufkkJ{Uaq+Vz@Gr8__@Hnh%5#n!!6z)XHASlSEL~PPY8BNT`4JEQ(Ht zDv3pqYUs#89Euao<5=j1)xfT-fUKXPnicRf{v%>03vG70jTY4@b>z9?W~fR0Mzg!y zzT{VYE9B~Y>wE7~1g6od|1Z;a;C7;+4#d7pCzttwO-tjU2*<-X79A{ksA1W`3d42= z`K*C3_)q&{$k%NXlbH#SAgRphnOy@K(E-IX)i6(+G)7CseBX9QR*ud%N+3OCwdid< z?%Mhd*xD^}*C}R#?jm7;U3hd?A5oZuPcOo!Y*Z4{s8Gyu{TOjM>%Mz~yd}!R61iz| tlTtqaL+1P?bMOK)MD>!eURu<8s$|WQCx=&bUZ>U@lv6%hX?(yG@EarEzSjT% literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..1fa20e2c5f94ac83216544527dccd4b0bae6c758 GIT binary patch literal 871 zcma)4+e*Vg5IvK$#>T3(YQ5hh)(VQ?la@ji6rreS>HD^>x)KvfQpL~mK?EQC06$8c zja957B(S?PbIx2cGjH!NuK>2NoPmiM8!60Mn6ofXNZ$#!EeZMBwYU=-uJA55j+@uA z73~l*XX?@uQ9EFQS+BDteW9d#Zefuyb|5_&sMe{x4^$*iL?CWtBm+YB&|_rJ6=5ht z0#ymCwGMk<`-jdyzD|{MRFZPbKWg6feOC%^r@{exqAL|Tn}n5Qk+e%$c`B+9O2vde zs|`YG&p+qZ4Aztj)8PrA7jl1c$gxe5-(t5|3(q$0}wJz-8_6uK6mf5M6c@+9T zi{<+Ej}~;sR{3ip*k^t_XvuvQSJyR*bv^hjau~`Yk0tI}7ySRI2)W-oW5FRTC-Ucw zD(W8gcd;?g8=B%}HTk5`1A@hpfnL5d82Hu)b2(iyTZvB|!~Bl0bi!PNU%RyS1S&nl zcx27QDBn67&_IFj!Y2!398-UG9E~u}ayI7Kj7_j+b}E>}6l(^i8P^#N_E|t*%&^f9 Fd;m>s-!=dM literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..419f729c848bff656b513fffcbf19489a93296f8 GIT binary patch literal 1126 zcma)5+iuf95IvhXaqPOS8=!5Q5{{92NHXdq7;kphDH#8W?%4JQ(O&tlW z>&PLmqNrknVd=4OglDy%iw~X^h-cj6M=wg( zedM`k3H!h=)76gUSV4s$og2H$HyM;&_drND%MnleM=jyK;4Pap>AKtIc9VOSJdc!$ z48yP<1qVRaoI^gSw2b?T(fMwglD4Y%*L#hw*bJkq&M$;iMQ z<_(zGG*H5dfi2u-SU4s7$aQVO9Rqi8SH-r0d$_OS0mE7ZY*N7)%u}rW)}d$z)ZM9E zvov+_oJ=Cok)uZYfZP3Wa>g;Kl16LDv^lgP&sUK|Mpb7}LzMjvwKZ4EpV1fUN`xR* z=}~F)zL;ssa*-6H-^2oFib<-_S!(n`@dT{!6|v8u%{f|=WCOg!d0H2TR=7Zt{PYlw z#t}3z0zv tD-_@&SsEb~skubbWzxjKmT`rI7_QR48cNqNLwlOeDHMpKbWC9u_yay76Yl^3 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..d757be60547f124bc71bd014a3576eca3a37ccbb GIT binary patch literal 796 zcmZuvO;6iE6r9bMu`$F1C~eb1fB+#-QYvmmxgb$RN?TQ_;D|P1fknoS9Gm}z1gg|S z)pLJT)malnjX3P{zJ0SZ^Y;1A-=Dt#?4f020*el8ESX)+#xhnctlB7|Zcf%LY*=Ur zxMy1VrzbiXCh@L7x!coMLth<7ayV4cM*+L1&jT4JkrJq8tNY!~1FlWv|5P6YO7Vpr z)!!S=PbyH69vm8}5s{^R9q70%P-#4=Z5{~}4#HE4mAg7nUy`f7ioVOf&yz|w97z92 zM%v`#!-A0!nE#ykv8MBk7EN^mY9IJ=G*X1EW%cUM-lD_&Sr{@lj31{LCec70>eNGq zf9FzOOBZE$E@n`5;b79jri&)F1STGy$Hg|@xtKP^9f8#h$MYTpJj31cWpLj5+P_qT zSYRqM9D!mwJo7M5v1~zTt`09{)KKH}ZT=*AF1iJuh`Su77-{e^_dL^AS_7M_urkZ6 zO>B-|r@3_p(fonjO^TUgED-~|!93%OdlbK~m>Dg@MoV~&>X_>rG3Lfn^A`DA6n>-V sId>>AwZ`cj(?@~n)OL+j%UHxpD&*c%jD>QPH|@N|%T$z8z&aLyf0VPP%m4rY literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..e987035b12f96531caefb0999a87f3a99f964137 GIT binary patch literal 753 zcmZuvO;5r=5Pge4X{}OG@f$%=5shf#4Z=mEAt8Fe;L$9w>YCb;w)nqHFeV<1XMdD& zwqi_)hn?>1n|bf;bU(k|-T@qAUq=dS26W`qZe2$Lc?|^(8#c*mxbOw;XhyUjhR^3h>j$uP`b z2tN?Lh!Wke;gIr)&3#``(PmVw_)ibHo49pdiY4X6Xt@KgE6!x7A7MXu;7{DdG}0z4 zESoSeX<`Q@hN;LH8B)KaF|muXhCPNtgzG;i43<);*xb3RTy`ErH(*GFKTM5c93$gQ z(rS==gd2H!0XjX47%lP$8cUc>S(b7?LM+S>lA)|lm0@jp?***hsDQ@$pi*m&s R!%7%eu|QvguoQ}{h13d( z1LDk&Ld-g;nuNoycJ`Z{nf-SE{Qdb0z#DXIl<}+r8%?uXvayU63#&GYSTmqy;e~~D zf$FJN!O5`>hv`V5=6{qrK8odVsN%N*_JKYNwj8{KXJK2QIivBPJ+EM7JAn+(Iv@JyYQR^hPCWvH zU8rxS3-dfC7n-9dP`s2u%2w58%=pY@{s17y!LVR+GE{S2bB#&G#T`}}L|rm7uD5v& z;r&4Fd&arTxkL`Ig?pSIOcd|q5s}e0YK(%%Se$5mBFCIq@~)7-Lg6=xZu=UgF|-VP nO?YdtfIR6P3hkhYSDBGBmcZC3hbLs@@DvX-Q#KvX83z9Vek`63 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..f29907667033e506c171d5622060fb364c3f9289 GIT binary patch literal 786 zcmZuvT}$IY6g|^6O;b}F>v#Rux?8Jjeeg}`i=Y&OK2+R?eUND#btEQb(k|@J5-ftS z%Rc*~#5-w3qY`GwoqO&%XYQS+=f{5lcClk2hlM;WEb6}{3(HtBv1-AxrL=ce_IEF<32mhHP3?Hm4^+ZaXB zhJ&(=JVs1ZZET>%kbCWfjZJLX_?D|U=$S`M_)9~I2fZ$iJ}G} zBW!JR09JcI>Mp{J)1D;^FhL(M6*Ep^h9b?a*~lhlQI5G>!sv=}?H=iSWd6g*4UpB5 q@fXGb<{S4Y(uABQmKkE0jWq0GHHI1~%n>4mc|vJDnh4g(2VMZBL8uY{ literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..b25d3be89ab454f3c11d1c0d86ee3442e70d9365 GIT binary patch literal 908 zcmaKqSx*}=6ot#V56Hq_||C4b!AkC zEgM4iC=lhqS7FGZhgCvh;EjdTzPLP82&;qgG25GN>mtxWXjNdfvfO&^=V6U7>o{L& zUkLfS(q^C^YW7a5K=#*o`g*8=*p;G zkIh%Y_%|JByGIyX-?$_s54tTT z(lv9|?VBba>UgW8ZnxDhmBk$92~&mzW4U zBOU)u>?PPZj_~RCkDH#uBP_bThjS#9UBie-2`jE=WV(c9*Y!4Nl#!4Z4v>5^n2l%h z$}umM1zA;vk(S!L2i?gef%h_w$Hf9Z$UOUKz(;(F^~HEx5)ZJCG?KC>C38=h7ETB= X!bxFPI3;{1%n9?tg0Lto38#U7dr$ZM literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..9374dd90e433f67b08f9580b79b4c520de7afd8d GIT binary patch literal 270 zcmXwzy>7xl5QJxqe~9@FPmnT65jS)onn*-Q78F5HpUnyu85 zxY5kFH>DkwBtvM)1dyOF1Dlo?li3_r2IKp%+We^YbBLyEI9r zWDpmr$yUZnmH(hy?&L%Wk?c7w@dQV21@uI?@M?#ur@5&qswaT=`VIP0;NU^kR}B3SsKBL@hcU&}@xDX-+U@V_{bc<=}Cqlo(& z6AwF?ncdmU`SSe(V2ojm4tf##5e5X(GBZN>tc`A72%Y=Uir~LiYbNwEZTNk^&Dkzh zUWzl!szQ}3Wwq0Prr&(&nvi5O(|lO9+p&Ej#EWWg3!ZA18@#b$tBZ-MxqjTJgGvx0 zlB@p=q3;%Hsmy0O&o^8&xPvEk0ci;zLCfHhqPwEfb^`B(|66+_f2tgnZ@NgC$z(X0I+DS3loiCfs z%=2}B0GMHD!Z9%*7*}pC<%uwHcbT{eKNm&f?~fVBP2hDA!4A`;5KSwYV7XBgcuE9! z5zV{j%Pt}~VcE)<*J-X^j5l1cOyiZPxt@L^5JuagVR;rYAEc-%mJ0ocGXR37%BZOm SdeD{cE2qIw`fVnxFR|Y{YCjGD literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..3684152febb684014d3099991d06120bb28d8941 GIT binary patch literal 489 zcmZvY!A`XzF<>8(geyv$P~UmM0SrK7bEp zoK{Rgyv)q^&%d*i`TTnS0C0(86B@b(4h=GP#?)@ z%(GkxviU<&^aYRdk^-WdBV(Dl)I2>47^*kPgnBJc#^Nr284Km}aYTykB_WRju4KV0 zv6?-}IYZNX;8Hy*o~A<4%qdvR@q@lg4;*KBwY_}skLGUM7|c5-)=Dy{+F9c|F^Z9tEvl|5 n7m9xV2KGvYh9<>YDO%X2+WIk|g*MUNhGG*{R$uMoprp<>2Wn}p literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..fbff730183d66c009f54cfc86694871820ab433c GIT binary patch literal 527 zcmZutO;5r=6r2Yw$d@1>ejYr62f27sLSjrXCPWWy@W8=r%Zf`%X_jKb&+=sA!5`p{ zGQL(Ysd(7knb~=7XW!@7`v-t?9Ose7K^BKu91+YXCA|@$+MkFQ(e{KtZr?i->4ukt zoTbLT2p3us(zeY?L1-^PJ1cB5XsF8FpgLOqcY3*>PF8iAu z`(iV6cT*zdt=U4mvZvxyH`13{xxHvy^RsAJMU=2jC?z5hDt`xw6Qp?L;KkpD$$N%b z3Ry;5$o=v>qXLS2N4&T>pJhf@d`60S`UZMskVb{~Oe_+17#DvGsG`QKo=|p~rB+Wi IuotuaZ-*Ll8~^|S literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..af39fafee64ff01ac3ef1b58ffe1fd1422799838 GIT binary patch literal 670 zcmZuu%TB^T6g|VMwpKwAL{UUVgP4d56Big3nrIpuU0`rM)B(rT)|A%&azQjM`~W}7 zc&CuKu#3*jy*;nF^ZoPr1>gkxIODE~co+p_RI~2`{zCcB>?i)p+b;J; zZOaSANCcfO5sjW71&+9sD%R4KpbJXpoRj5|BAC!HXF^9&L*2wSc1-M|p<$0qOgc1st6yeF+wb(IMX^MjAH1m pxeuf#$oxqeG5wkX*s+{B1m^#sN%zLoU}>k=ujtJftA)m#)l(;!hSSV0u@h(>Pz}_pyIw91k5aX zkuQTI8EX?ylLccbP|93Bt5Cqr;J&d|tgJ0EYR>4Kss6w0o-rys-_zhva6&0h9-l6%LLp;DW}>Ul%BB_b1=C~*VNS1bocb{KRk$T1KCxCU_Pe1|p7S?4U--TZW@DBEmwulYW0PBT0DwU-4f1THK0eAauWZ5Qc#iy0y;^g*~NJvQNm?>Rm$aFuY)|skYMc zYkJd@(Kpcxn5ncwUj$tdDYGAvx#UX4gqd+Kvv>9~3<+*0Oe0@@QpTptdCN%o2ZFn^ zYf|#?5;GnqG38;wplOsH)IBt?ZI~TGbxgkq)1!ipd)LxW2#aHcgT~sgnSb_}6C1e= z+e2_}MUcwlOTujJtUjiJTzc&ZJxHTf?_!xJrN}ds0h!7ealRzVA hoYyJmaQ4KqI<(ASkrf%d!34(&BQx(VV~^tt;4i}dv4H>p literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..dce417187a087b3cba84e83060c4b666fc556bfd GIT binary patch literal 766 zcmZ`$%TC)s6g`uNO*DbK&5Wb#0)UV*pXu+^|M$Y zBo=%?KMHYX94M&i!sGim_ndQQ{@mT%0{Dd08Y-CgP{lhFEx1^6u`J+Zr+U!(C@>Rr z^S(;MNDc;H<5;Epv5p5>hmb8D>ug(Kw*4Q>+JQi2Cpl6A6M>G^xBR@P(mmOWSeXox zP(}wb)g~VnD@InJYLx_h``!b{Yd z5pUVJ5@X-uJoYA;2~1&{Xv6+%$nF^S@?U1pvPnAYJz;kq*&Q^fSg;q$rf1lVs|IG+ ad(F6nH}qOWvzW7$x0vAHBcj6X$ANoM>7G#l literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..a87c8573a0ef58a657a1a74668bbee469509f68c GIT binary patch literal 899 zcmZ`%%Wl&^6g`t?NtlELN4r~Xj+NozS`<}9Vxa+GFsEmfFxPP2K6k(?p|m7cx~ zWRga#syIwAYN*_{_hwn7)Aeq`FOeMcZ7HDhqj&JEavXf z6S$8pq7C~E?>z6SVb8lSZ&6s#uV<+%HmFHA%w!r9_*|w+;d(}2#RFQoOmKlRf}|(v f;T*L?)FVc7cucm5^#r?Ft%A)APW6 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..c89fee8796a449d6dd4f6e4e10a22da3fbe9f42c GIT binary patch literal 633 zcmaJ;TT22#6#m9t-CVc4lv-LKAyf*|LvM-?2}K}5czGYUAt!8w9|_Q5R^NN7pwo3&}^mE=1+@Xfus29&T!Q3wpLoC2l7twAoOU2q|U6> zUaBT-doT|@S6s;GmibFTZzkPyPQ$nE`6G9bM9P7M4Ga4Wwb9S>ErYEMU_Wi6Q|~5mMAHLRf+(W)udQab!D{`dM8evFHc% zqpBW{Aq~Q%3;UjPeb2quXXe-Mr=I{mp;|;1TMo7z>^RsJC|($&g3G%=DS?tDXPyj0 z6*|}x7_*skWgP4a=u}EO8)gJU!;Kl;`sbjPWqg{*Z0^@DnGcpP*`rmmkm4${jI%*1JYag!!a%cW6Jt()dQC|iRT{3r;8Xt(`<}AQ6Rv1@bW!A{D&!g9| YL6+fa1;%COb7Xm9hjEN?oUsV}0mI_=Q~&?~ literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..085f7e320e20467441f9431583a9a4e9765b644a GIT binary patch literal 1109 zcmaJ>YflqF6g|_|w#y<9r3e+QJfx*Uec-dTDkK_`Mm~TT{bHtdfF*U8Y#*Zk%7lQ? z#2?^~GM<@jgqTe~Z10`B=bm%+&P;#*`SA9=0+aRa?vVAzb=Om`yPp~=*pZDEE8}&)DOdgYeyMZ@jc(C^J4+$qPT#)?RSHwdg*HZu~&+p;x^Z1TeVjYWluU7 z$7Q0<4Li7m5eush%D8Lco`Wf@Ik=C979Kfxj3*W$Aa6wfR?7nq71mbNA^s%6S8 z>Ft-d8i%UM(nKU&AnEE!Gn$F>Q%u~@d!RUhndk{D7!;?Ri=+)-Q?yY3-$_MpM#hMK z*jJuF+E8&w0{KB=L{M++oNwLtTS~Ic>d97DZSe$U3-5~;6#EFa%?_|>q?aO`USJBR zXuJ=F-a7|@;_h-2Ili56F*nG+!O%*6fE9y5o_A-McS`W#xnLY+7Q+}H=(EGh6=r2d zjY%$_L3}fi3I3)`F+i5N69O=at6cHW{A&&nH*~8%5qo!rczyWuSPW+GWS)}y!O+`Q9Xuh?1^CpcNnMXV4i;j Ox0x3hA25~}YrtPkoe&-X literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..bdd24f4a62f3fb3a6eebc4fbf559df64ab02737a GIT binary patch literal 491 zcmZutOHaZ;5dOAMN^9jMg70ty4stQ^0O6pChNO`L2G2`ba7k^+w&j0$Fd7g30DqKm zT8U`%usgFe-(z;(KVIJeoZ;Alj*5jHR83^DYoKPJ&XDU#Uq*d~OtUp+$X*6h!BBLh zFK*(8iBPwE;!&mI1TOc+T*>6UE@q>988VcdQM?q&^>`Q#{4na0+AIhd%#ob?Jc<9kBh zqeIhxAx~L{BBQ9cpTQo}wwVHwVigwM_7?zKl!5Z?Z}K^bB{;L4e}VRd%tpXUeQM-U S{~=^F%#*+{ZnrKKGJz(&>lm(a6E!npIFB6T42jkfv zWt`SVjEC9z*qP^@%;(qJJAhNPY?#=npoC2eTNMK6~!lA!cD`Fp)!;+ z#p6U1q2b+WzM#IIH&AgNcl*?955q+J;!>tUwJV{7mi{@9M07mokKBQUvV&dhQR{Nl zK@OXA;D`zv5rcwlxborFy23*bDoAF%uF{v_1Hb9%MV$ziWgN&3wYg6QsXXHzr zSFoq-+ospdicPFg?EEy4U!{y;?RWT$VCk^ad4})KO7<)+F382pFuc z94Q_rArWfsL&zs|uQhi%D$bM5HZ6v7H%LNHT+6g)?CLjaO9i~4fT<;c2Yr#2CP1QTvg$(%K2Ns;3|V)Zy%hXeCK3}L zjL-Zi!^Q=F9#koRVQ$zcPv9~;%PD$pXo@T;`EY{3SCb|(Pw?B zhAn~m-Toh=TTK0abGv`k>JX7V2?BwohI1~*a>tYY>CV@|xpL!{87x1RUXsr7piC$! z1d2U<>dQC@*;Z&UWpMA>N4pOhJ5K*1_!i0$$2R&-*N>-RI!mb+B%!N5YO{Lflk!!l z-2)k^Xxqr!m_yOVYt(G4qb5+A;caYSlP`GhN!T-!7D$t*JBBB+wq&}mvDP-$*m zA=CVY>_6n@u8^Nmmni|XkVhMf*h?kq6VOzGa6Cqh#71mZGh&n45^Ht(89d>cc*|Hx GGpjdtZ+E`!o=`qZ9m zN?Y6qPd(vwc+Vmv-E>TDb-63U{R~w6N9i$SSBG_k=aY7H;5ZCg+X-A#+{jSIxD~c= zrCH~m@Xo_4=~#!ZL&chkLmfvrR*~0{#tB1a#bl_I4QDguoHp#efRs47zqIkD0Q*z1I{ zNo#xpULi?!NF@SNFeuZ*&YLeuEIiXoZ-^+Lh`vKvXiP^nXxR0Vjy~7PP-g^Ne?gjg AqyPW_ literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..8b30a539bbfe2b89b8017045570b7e62d5eed441 GIT binary patch literal 592 zcmZWlNlyYX6#fdsAmb>D0AqC5`xzp#qRQEZkg-YJcL<+iz1LPTU|DVf{o~O~6Ln)j` z9MLCh^yxr?7I{G;sxIhc3aPz=y;70H8tsY(s>sl8&IB;99^ZZ=8-y@yB1^FCjM2BZW;3TRIeM>)64rhCL1Y3~a!VvpVA^;oA-m zf?HR*LD*nOcjVCJ;n)`p$4i8!HR8{_?r?WlZ@Zxw3ct}JRjMgn8MYXda;3+hUU>JU z&sfqG*W<^&@VmV45R$Vzn>#)3%P9W^)$lDcf7H0i%S{x$zBOp z_|iV-fe31mCj$o746Gnc)g_Zr^+3a+fen-x@{1RbCNY>Z-A#WaY=YEsJGzj$C}1d* z=iXvUZ&Z3H(UWWR1&kJ%p;M#O3_<(Y!PN2RaIqRdx<4%yl>0B@KzgIq1kl(gPC#%{0e>7*+#?Txmg$l)` z)G<3(A{I)9=R6bHu`a|y6YJ#qjmXgc+Z6Uup-w@QI)F*DHm5pWYYW^UhJKN@Mb{Z^ mt(ZrzU@vqS*q~V}ZJTsk-v+eMCh9CHU7||))fRel+WrFaylII5 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..ae6aa9aaf6196b41e19792e5e9875419e55721e4 GIT binary patch literal 425 zcmZWlyH3ME5S;Uq7?X#A&{75p(olhA36P+%pokUfvvY)tjBTB5Bt9!uBnm!&k3y`2 zQ-tWG-I=-Bz1{o%`TPQKi4zApj%*y;7&4eIQlv8mFI@0O2oZvCK)`4OemS$@=}x+&5|zm z&|$FKDH!_ySH~$d`XqqSFjAtqJNyOaj#>f$ literal 0 HcmV?d00001 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/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")