diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 6c6cbc4e1c8..639194b77e5 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -38,6 +38,12 @@ symbolt generate_java_generic_typet::operator()( to_java_class_type(pointer_subtype); const irep_idt new_tag=build_generic_tag( existing_generic_type, replacement_type); + + const auto expected_symbol="java::"+id2string(new_tag); + auto symbol=symbol_table.lookup(expected_symbol); + if(symbol) + return *symbol; + struct_union_typet::componentst replacement_components= replacement_type.components(); @@ -86,14 +92,12 @@ symbolt generate_java_generic_typet::operator()( pre_modification_size==after_modification_size, "All components in the original class should be in the new class"); - const auto expected_symbol="java::"+id2string(new_tag); - generate_class_stub( new_tag, symbol_table, message_handler, replacement_components); - auto symbol=symbol_table.lookup(expected_symbol); + symbol=symbol_table.lookup(expected_symbol); INVARIANT(symbol, "New class not created"); return *symbol; } diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index c342ff0f766..5554283406c 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -263,7 +263,20 @@ void java_bytecode_convert_method_lazy( symbol_tablet &symbol_table) { symbolt method_symbol; - typet member_type=java_type_from_string(m.descriptor); + typet member_type; + if(m.signature.has_value()) + { +#ifdef DEBUG + std::cout << "method " << m.name + << " has signature " << m.signature.value() << "\n"; +#endif + member_type=java_type_from_string( + m.signature.value(), + id2string(class_symbol.name)); + INVARIANT(member_type.id()==ID_code, "Must be code type"); + } + else + member_type=java_type_from_string(m.descriptor); method_symbol.name=method_identifier; method_symbol.base_name=m.base_name; diff --git a/src/java_bytecode/specialize_java_generic_method.cpp b/src/java_bytecode/specialize_java_generic_method.cpp new file mode 100644 index 00000000000..37515d4f712 --- /dev/null +++ b/src/java_bytecode/specialize_java_generic_method.cpp @@ -0,0 +1,333 @@ +/*******************************************************************\ + +Module: Generate Java Generic Method - Instantiate a generic method + with concrete type information. + +Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include "specialize_java_generic_method.h" +#include "generate_java_generic_type.h" +#include +#include +#include +#include + +specialize_java_generic_methodt::specialize_java_generic_methodt( + message_handlert &message_handler): + instantiate_generic_type(message_handler) +{} + +/// Generate a copy of a given generic method, specialized with +/// the given concrete types and insert the method into the symbol +/// table. +/// \param generic_method The generic method to be specialized. +/// \param concrete_types A map from generic type variables to concrete types +/// with which to instantiate the generic method. +/// \param symbol_table The symbol table into which the generated method will +/// be inserted. +/// \return The symbol that was inserting into the symbol_table, or the existing +/// symbol if the method has already been specialized. +const symbolt& specialize_java_generic_methodt::operator()( + const symbolt &generic_method, + const type_variable_instantiationst &concrete_types, + symbol_tablet &symbol_table) const +{ + INVARIANT(generic_method.type.id()==ID_code, "Only code symbols"); + INVARIANT(concrete_types.size()>0, "Should be at least one concrete type"); + // Another invariant is that concrete_types.size() > the total number of + // type variables used in the method. However, determining that essentially + // means iterating through the whole method structure and duplicating a + // large chunk of the work we're about to do... + + + // We need to decorate the signature of the specialized method to + // differentiate the symbols of the generic method and the specialized + // method. There's a design decision to be made here - do we actually modify + // the java signature, or do we decorate it with additional + // qualifiers. We are taking the approach of adding decorations because + // that avoids the situation where the user may have already + // declared an overloaded method that might have the same signature + // as the specialized method we are about to create. By decorating the + // existing symbol, we ensure that no legal Java program could have already + // defined the symbol. + const std::string& signature_decoration= + instantiation_decoration(concrete_types); + + // Check the method has not already been specialized + const symbolt *already_specialized= + symbol_table.lookup(id2string(generic_method.name)+signature_decoration); + if(already_specialized) + return *already_specialized; + + // Convert concrete types into a map for faster lookups + type_variable_instantiation_mapt concrete_type_map(concrete_types); + + // Copy the generic method as a starting point for the specialization + symbolt specialized_method=generic_method; + code_typet &specialized_code=to_code_type(specialized_method.type); + + // Handle a generic return type + typet &method_return_type=specialized_code.return_type(); + instantiate_generic_types( + method_return_type, + concrete_type_map, + symbol_table); + + // Set the name of the specialized method, but ensure we remember the + // original method name because we need it for cleaning up internal symbol + // names... + const irep_idt original_name=specialized_method.name; + specialized_method.name= + id2string(specialized_method.name)+signature_decoration; + + + namespacet ns(symbol_table); + for(code_typet::parametert ¶meter : specialized_code.parameters()) + { + if(parameter.get_this()) + { + // If the type of the 'this' parameter is a generic type, modify the + // type of the parameter to be the specialized type and not the generic + // type. + const typet ¤t_this_type=ns.follow(parameter.type().subtype()); + INVARIANT( + current_this_type.id() == ID_struct, + "'this' parameter should always be a class"); + + if(is_java_generics_class_type(current_this_type)) + { + const irep_idt &new_this_type_identifier= + id2string(current_this_type.get(ID_name))+signature_decoration; + parameter.type().subtype().set(ID_identifier, new_this_type_identifier); + } + } + else + { + typet ¶meter_type=parameter.type(); + instantiate_generic_types( + parameter_type, + concrete_type_map, + symbol_table); + } + + // Update the symbol name of the parameter to match the newly decorated + // name of the specialized method. + decorate_identifier(parameter, ID_C_identifier, original_name, + signature_decoration); + } + + // Updated the body of the specialized method so that all generic types are + // specialized and that all references to symbols inside the method body refer + // to the specialized method and not the generic method. + // FIXME: Probably also need to update references to class fields to point to + // FIXME: the specialized class fields, rather than the generic class fields? + auto body_iterator=specialized_method.value.depth_begin(); + const auto body_end=specialized_method.value.depth_end(); + + while(body_iterator!=body_end) + { + if(body_iterator->id()==ID_symbol) + { + exprt &symbol_expr=body_iterator.mutate(); + typet &symbol_type=symbol_expr.type(); + instantiate_generic_types(symbol_type, concrete_type_map, symbol_table); + + // Update the symbol identifier if needed to match the specialized + // method name. + decorate_identifier(symbol_expr, ID_identifier, original_name, + signature_decoration); + } + + ++body_iterator; + } + + if(symbol_table.add(specialized_method)) + { + // We should never hit this because the first thing + // we do before starting to specialize the method + // is check that the proposed symbol name doesn't + // already exist. + throw unsupported_java_method_specialization_exceptiont( + "specialized method symbol already exists"); + } + + return symbol_table.lookup_ref(specialized_method.name); +} + + +/// Given a mapping from generic type variables to concrete types, generate +/// a string suitable for decorating symbol names with. +/// \param concrete_types The mapping from type variables to concrete types +/// \return A string suitable for inserting into a java signature +/// +/// As an example, if a mapping such as this (pseudo code...): +/// [ {T,java.lang.Integer}, {U,java.lang.Double} ] is passed in, the return +/// string would look like "" +const std::string specialize_java_generic_methodt::instantiation_decoration( + type_variable_instantiationst concrete_types) +{ + std::ostringstream decorated_signature_buffer; + decorated_signature_buffer << "<"; + bool first=true; + for(auto &concrete_type_entry : concrete_types) + { + if(first) + first=false; + else + decorated_signature_buffer << ","; + + decorated_signature_buffer << + concrete_type_entry.second.get(ID_identifier); + } + decorated_signature_buffer << ">"; + return decorated_signature_buffer.str(); +} + +/// Instantiate a generic type with concrete types using a supplied mapping +/// from type variable to concrete type. +/// \param generic_type The typet that should be modified and instantiated. +/// \param concrete_type_map The mapping from type variable to concrete types. +/// \param symbol_table The symbol table into which we may add concrete types. +void specialize_java_generic_methodt::instantiate_generic_types( + typet &generic_type, + const type_variable_instantiation_mapt &concrete_type_map, + symbol_tablet &symbol_table) const +{ + if(is_java_generic_parameter(generic_type)) + { + // Instantiate a generic type variable 'T' + instantiate_java_generic_parameter( + to_java_generic_parameter(generic_type), + concrete_type_map, + symbol_table); + } + else if(is_java_generic_type(generic_type)) + { + // Instantiate a generic type, such as 'List' + instantiate_java_generic_type( + to_java_generic_type(generic_type), + concrete_type_map); + // At this point we have concrete types substituted into the generic type + // variables, but it's still a generic type. Now go ahead and instantiate + // this parameterized generic type fully. + const symbolt &concrete_type=instantiate_generic_type + (to_java_generic_type(generic_type), + symbol_table); + generic_type=concrete_type.type; + } +} + +/// Instantiate a given java generic parameter using a supplied mapping from +/// type variable to concrete type. +/// \param generic_parameter The java_generic_parametert that should be +/// modified and instantiated. +/// \param concrete_types The mapping of type variables to concrete types. +void specialize_java_generic_methodt::instantiate_java_generic_parameter( + java_generic_parametert &generic_parameter, + const type_variable_instantiation_mapt &concrete_types, + const symbol_tablet &symbol_table) const +{ + namespacet ns(symbol_table); + + INVARIANT( + generic_parameter.id()==ID_pointer, + "All generic parameters should be pointers in java"); + INVARIANT( + ns.follow(generic_parameter.subtype()).id()==ID_struct, + "All generic parameters should point to symbols"); + + const symbol_typet &generic_type_variable=generic_parameter.type_variable(); + const auto &instantiation_type= + concrete_types.find(generic_type_variable.get_identifier()); + + if(instantiation_type==concrete_types.end()) + { + // If we ever want/need to support partially instantiated types, + // we'll probably want to just return here. + throw unsupported_java_method_specialization_exceptiont( + "No concrete type supplied for generic type variable in parameter"); + } + generic_parameter.subtype()=instantiation_type->second; + generic_parameter.remove(ID_C_java_generic_parameter); + generic_parameter.remove(ID_type_variables); +} + + +/// Instantiate a given java generic type using a supplied mapping from type +/// variable to concrete type. +/// \param generic_type The java_generic_typet that should be modified and +/// instantiated. +/// \param concrete_types The mapping of type variables to concrete types. +void specialize_java_generic_methodt::instantiate_java_generic_type( + java_generic_typet &generic_type, + const type_variable_instantiation_mapt &concrete_types) const +{ + INVARIANT( + generic_type.subtype().id()==ID_symbol, + "All generic parameters should point to symbols"); + + // Replace the generic parameters + for(java_generic_parametert &generic_parameter : + to_java_generic_type(generic_type).generic_type_variables()) + { + if(!is_java_generic_inst_parameter(generic_parameter)) + { + const symbol_typet &generic_type_variable= + generic_parameter.type_variable(); + const auto &instantiation_type= + concrete_types.find(generic_type_variable.get_identifier()); + + if(instantiation_type==concrete_types.end()) + { + // If we ever want/need to support partially instantiated types, + // we'll probably want to just return here. + throw unsupported_java_method_specialization_exceptiont( + "no concrete type supplied for generic type parameter"); + } + generic_parameter.subtype()=instantiation_type->second; + generic_parameter.set(ID_C_java_generic_inst_parameter, true); + } + } +} + +/// Decorate an identifier on a given expression if the existing identifier +/// matches a given pattern. +/// \param expr The expression whos identifier should be decorated +/// \param identifier The particular identifier that should be modified +/// \param pattern The pattern to match and be decorated +/// \param decoration The string to use as decoration +/// +/// An example of the use of this function might be: +/// decorate_identifier( +/// symbol, +/// ID_identifier, +/// "java::array[boolean].clone:()Ljava/lang/Object;" +/// "") +/// which when given a 'symbol' expression who's 'ID_identifier' looks like: +/// 'java::array[boolean].clone:()Ljava/lang/Object;::this' would replace +/// the identifier with: +/// 'java::array[boolean].clone:()Ljava/lang/Object;::this' +/// If the given 'expr' parameter does not already contain an identifier +/// whos value begins with the given 'pattern' string, then no change will +/// be made. +void specialize_java_generic_methodt::decorate_identifier( + irept &expr, + const irep_idt &identifier, + const irep_idt &pattern, + const irep_idt &decoration) +{ + const std::string &expr_identifier=id2string(expr.get(identifier)); + const std::string &pattern_str=id2string(pattern); + + // Does the pattern match the existing identifier + if(has_prefix(expr_identifier, pattern_str)) + { + const std::string dec_str=id2string(decoration); + const std::string tail_str=expr_identifier.substr(pattern_str.size()); + const std::string new_ident=pattern_str+dec_str+tail_str; + + expr.set(identifier, new_ident); + } +} diff --git a/src/java_bytecode/specialize_java_generic_method.h b/src/java_bytecode/specialize_java_generic_method.h new file mode 100644 index 00000000000..8c3ddada89f --- /dev/null +++ b/src/java_bytecode/specialize_java_generic_method.h @@ -0,0 +1,74 @@ +/*******************************************************************\ + +Module: Generate Java Generic Method - Instantiate a generic method + with concrete type information. + +Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#ifndef CPROVER_JAVA_BYTECODE_SPECIALIZE_JAVA_GENERIC_METHOD_H +#define CPROVER_JAVA_BYTECODE_SPECIALIZE_JAVA_GENERIC_METHOD_H + +#include +#include +#include +#include +#include "generate_java_generic_type.h" + +/// An exception that is raised when specialization fails. +class unsupported_java_method_specialization_exceptiont:public std::logic_error +{ +public: + explicit unsupported_java_method_specialization_exceptiont(std::string type): + std::logic_error("Unsupported method specialisation: "+type){} +}; + +class specialize_java_generic_methodt +{ +public: + typedef std::initializer_list + > + type_variable_instantiationst; + + typedef std::unordered_map + + type_variable_instantiation_mapt; + + specialize_java_generic_methodt( + message_handlert &message_handler); + + const symbolt& operator()( + const symbolt &generic_method, + const type_variable_instantiationst &concrete_types, + symbol_tablet &symbol_table) const; + + void instantiate_generic_types( + typet &generic_type, + const type_variable_instantiation_mapt &concrete_type_map, + symbol_tablet &symbol_table) const; + + void instantiate_java_generic_parameter( + java_generic_parametert &generic_parameter, + const type_variable_instantiation_mapt &concrete_types, + const symbol_tablet &symbol_table) const; + + void instantiate_java_generic_type( + java_generic_typet &generic_type, + const type_variable_instantiation_mapt &concrete_types) const; + +private: + static const std::string instantiation_decoration( + type_variable_instantiationst concrete_types); + + static void decorate_identifier( + irept &expr, + const irep_idt &identifier, + const irep_idt &pattern, + const irep_idt &decoration); + + generate_java_generic_typet instantiate_generic_type; +}; + + +#endif // CPROVER_JAVA_BYTECODE_SPECIALIZE_JAVA_GENERIC_METHOD_H diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics$GList.class b/unit/java_bytecode/java_bytecode_specialize_generics/generics$GList.class new file mode 100644 index 00000000000..4fac9ebedbe Binary files /dev/null and b/unit/java_bytecode/java_bytecode_specialize_generics/generics$GList.class differ diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics$GMap.class b/unit/java_bytecode/java_bytecode_specialize_generics/generics$GMap.class new file mode 100644 index 00000000000..3540e3b5c5a Binary files /dev/null and b/unit/java_bytecode/java_bytecode_specialize_generics/generics$GMap.class differ diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics$bound_element.class b/unit/java_bytecode/java_bytecode_specialize_generics/generics$bound_element.class new file mode 100644 index 00000000000..a637dfd3c9c Binary files /dev/null and b/unit/java_bytecode/java_bytecode_specialize_generics/generics$bound_element.class differ diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics$compound_element.class b/unit/java_bytecode/java_bytecode_specialize_generics/generics$compound_element.class new file mode 100644 index 00000000000..550d17bff22 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_specialize_generics/generics$compound_element.class differ diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics$double_element.class b/unit/java_bytecode/java_bytecode_specialize_generics/generics$double_element.class new file mode 100644 index 00000000000..57c1af60d23 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_specialize_generics/generics$double_element.class differ diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics$element.class b/unit/java_bytecode/java_bytecode_specialize_generics/generics$element.class new file mode 100644 index 00000000000..cb9f6f71273 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_specialize_generics/generics$element.class differ diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics.class b/unit/java_bytecode/java_bytecode_specialize_generics/generics.class new file mode 100644 index 00000000000..a7a753ffa5f Binary files /dev/null and b/unit/java_bytecode/java_bytecode_specialize_generics/generics.class differ diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/generics.java b/unit/java_bytecode/java_bytecode_specialize_generics/generics.java new file mode 100644 index 00000000000..d7fe706445e --- /dev/null +++ b/unit/java_bytecode/java_bytecode_specialize_generics/generics.java @@ -0,0 +1,67 @@ +public class generics { + + class GList { + } + + class GMap { + } + + class element { + E elem; + } + + class bound_element { + NUM elem; + NUM f() { + return elem; + } + + void g(NUM e) { + elem=e; + } + + } + + bound_element belem; + + Integer f(int n) { + + element e=new element<>(); + e.elem=n; + bound_element be=new bound_element<>(); + belem=new bound_element<>(); + be.elem=new Integer(n+1); + + if(n>0) + return e.elem; + else + return be.elem; + } + + class double_element { + A first; + B second; + GMap map; + + void insert(A a, B b) { + first=a; + second=b; + } + + void setMap(GMap m) { + map=m; + } + } + + class compound_element { + GList elem; + + void setFixedElem(GList e) { + elem=null; + } + + GList getElem() { + return elem; + } + } +} diff --git a/unit/java_bytecode/java_bytecode_specialize_generics/java_bytecode_specialize_generics.cpp b/unit/java_bytecode/java_bytecode_specialize_generics/java_bytecode_specialize_generics.cpp new file mode 100644 index 00000000000..d3ec4aec81f --- /dev/null +++ b/unit/java_bytecode/java_bytecode_specialize_generics/java_bytecode_specialize_generics.cpp @@ -0,0 +1,338 @@ +/*******************************************************************\ + + Module: Unit tests for specializing generic methods + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_specialize_generics", + "[core][java_bytecode][java_bytecode_specialize_generics]") +{ + symbol_tablet new_symbol_table=load_java_class("generics", "" + "./java_bytecode/java_bytecode_specialize_generics"); + + stream_message_handlert message_handler(std::cout); + specialize_java_generic_methodt + instantiate_generic_method{message_handler}; + + + GIVEN("Some class files with Generics") + { + WHEN("A method returns a generic type") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$bound_element.f:()Ljava/lang/Number;")); + + const symbolt &generic_method_symbol= + new_symbol_table.lookup_ref( + "java::generics$bound_element.f:()Ljava/lang/Number;"); + + THEN("When parsing the method") + { + const code_typet &code= + require_type::require_code_type(generic_method_symbol.type, 1); + + require_type::require_java_generic_parameter_variables( + code.return_type(), + {"java::generics$bound_element::NUM"}); + } + + const symbolt &specialized_method_symbol=instantiate_generic_method( + generic_method_symbol, + { + {"java::generics$bound_element::NUM", + symbol_typet("java::java.lang.Integer") + } + }, + new_symbol_table); + + THEN("When specializing the method with a concrete type") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$bound_element.f:()Ljava/lang/Number;" + "")); + + const code_typet &new_code=require_type::require_code_type( + specialized_method_symbol.type, 1); + + require_type::require_java_non_generic_type( + new_code.return_type(), {"java::java.lang.Integer"}); + } + } + + WHEN("A method takes a single generic parameter") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$bound_element.g:(Ljava/lang/Number;)V")); + + const symbolt &generic_method_symbol= + new_symbol_table.lookup_ref( + "java::generics$bound_element.g:(Ljava/lang/Number;)V"); + + THEN("When parsing the method") + { + const code_typet &code=require_type::require_code_type( + generic_method_symbol.type, 2); + + require_type::require_java_generic_parameter_variables( + code.parameters()[1].type(), + {"java::generics$bound_element::NUM"}); + } + + const symbolt &specialized_method_symbol=instantiate_generic_method( + generic_method_symbol, + { + {"java::generics$bound_element::NUM", + symbol_typet("java::java.lang.Integer") + } + }, + new_symbol_table); + + THEN("When specializing the method with a single concrete type") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$bound_element.g:(Ljava/lang/Number;)V" + "")); + + const code_typet &new_code=require_type::require_code_type( + specialized_method_symbol.type, 2); + + require_type::require_java_non_generic_type( + new_code.parameters()[1].type(), {"java::java.lang.Integer"}); + } + } + + WHEN("A method takes two generic parameters") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$double_element.insert:" + "(Ljava/lang/Object;Ljava/lang/Object;)V")); + + const symbolt &generic_method_symbol= + new_symbol_table.lookup_ref( + "java::generics$double_element.insert:" + "(Ljava/lang/Object;Ljava/lang/Object;)V"); + + THEN("When parsing the method") + { + const code_typet &code=require_type::require_code_type( + generic_method_symbol.type, 3); + + require_type::require_java_generic_parameter_variables( + code.parameters()[1].type(), + {"java::generics$double_element::A"}); + + require_type::require_java_generic_parameter_variables( + code.parameters()[2].type(), + {"java::generics$double_element::B"}); + } + + const symbolt &specialized_method=instantiate_generic_method( + generic_method_symbol, + { + {"java::generics$double_element::A", + symbol_typet("java::java.lang.Integer") + }, + {"java::generics$double_element::B", + symbol_typet("java::java.lang.Double") + } + }, + new_symbol_table); + + THEN("When specializing the method with two concrete types") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$double_element.insert:" + "(Ljava/lang/Object;Ljava/lang/Object;)V" + "")); + + const code_typet &new_code=require_type::require_code_type( + specialized_method.type, 3); + + require_type::require_java_non_generic_type( + new_code.parameters()[1].type(), {"java::java.lang.Integer"}); + + require_type::require_java_non_generic_type( + new_code.parameters()[2].type(), {"java::java.lang.Double"}); + } + + + WHEN( + "A method takes a single argument which is parameterized" + "on two type variables") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$double_element.setMap:(Lgenerics$GMap;)V")); + + const symbolt &generic_method_symbol= + new_symbol_table.lookup_ref( + "java::generics$double_element.setMap:(Lgenerics$GMap;)V"); + + THEN("When parsing the method") + { + const code_typet &code=require_type::require_code_type( + generic_method_symbol.type, 2); + + require_type::require_java_generic_type_variables( + code.parameters()[1].type(), + {"java::generics$double_element::A", + "java::generics$double_element::B" + }); + } + + const symbolt &specialized_method=instantiate_generic_method( + generic_method_symbol, + { + {"java::generics$double_element::A", + symbol_typet("java::java.lang.Integer") + }, + {"java::generics$double_element::B", + symbol_typet("java::java.lang.Double") + } + }, + new_symbol_table); + + THEN("When specializing the method with two concrete types") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$double_element.setMap:(Lgenerics$GMap;)V" + "")); + + REQUIRE(new_symbol_table.has_symbol( + "java::generics$GMap" + "")); + + const symbolt &new_param_type=new_symbol_table.lookup_ref( + "java::generics$GMap" + ""); + + const code_typet &new_code=require_type::require_code_type( + specialized_method.type, 2); + + REQUIRE(new_code.parameters()[1].type()==new_param_type.type); + } + } + + WHEN( + "A method takes a single argument which is parameterized" + "on a single type variable") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$compound_element." + "setFixedElem:(Lgenerics$GList;)V")); + + const symbolt &generic_method_symbol= + new_symbol_table.lookup_ref( + "java::generics$compound_element.setFixedElem:(Lgenerics$GList;)V"); + + THEN("When parsing the method") + { + const code_typet &code=require_type::require_code_type( + generic_method_symbol.type, 2); + + require_type::require_java_generic_type_instantiations( + code.parameters()[1].type(), + {"java::java.lang.Integer"}); + } + + const symbolt &specialized_method=instantiate_generic_method( + generic_method_symbol, + { + {"java::generics$compound_element::B", + symbol_typet("java::java.lang.Integer") + } + }, + new_symbol_table); + + THEN("When specializing the method with a concrete type") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$compound_element.setFixedElem:(Lgenerics$GList;)V" + "")); + + const code_typet &new_code=require_type::require_code_type( + specialized_method.type, 2); + + REQUIRE(new_symbol_table.has_symbol( + "java::generics$GList")); + + const symbolt &new_param_type=new_symbol_table.lookup_ref( + "java::generics$GList"); + + REQUIRE(new_code.parameters()[1].type()==new_param_type.type); + } + } + + WHEN( + "A method returns a type which is parameterized on a" + "single type variable") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$compound_element.getElem:()Lgenerics$GList;")); + + const symbolt &generic_method_symbol= + new_symbol_table.lookup_ref( + "java::generics$compound_element.getElem:()Lgenerics$GList;"); + + THEN("When parsing the method") + { + const code_typet &code=require_type::require_code_type( + generic_method_symbol.type, 1); + + require_type::require_java_generic_type_variables( + code.return_type(), + {"java::generics$compound_element::B"}); + } + + const symbolt &specialized_method_symbol=instantiate_generic_method( + generic_method_symbol, + { + {"java::generics$compound_element::B", + symbol_typet("java::java.lang.Integer") + } + }, + new_symbol_table); + + THEN("When specializing the method with a concrete type") + { + REQUIRE( + new_symbol_table.has_symbol( + "java::generics$compound_element.getElem:()" + "Lgenerics$GList;")); + + const code_typet &new_code=require_type::require_code_type( + specialized_method_symbol.type, 1); + + REQUIRE(new_symbol_table.has_symbol( + "java::generics$GList")); + + const symbolt &new_param_type=new_symbol_table.lookup_ref( + "java::generics$GList"); + + REQUIRE(new_code.return_type()==new_param_type.type); + } + } + } + } +} diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp new file mode 100644 index 00000000000..d1b5e44b769 --- /dev/null +++ b/unit/testing-utils/require_type.cpp @@ -0,0 +1,150 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Helper functions for requiring specific types +/// If the type is of the wrong type, throw a CATCH exception +/// Also checks associated properties and returns a casted version of the +/// expression. + +#include "require_type.h" + +#include + +/// Verify a given type is an code_typet, optionally also checking it accepts +/// a givne number of parameters +/// \param type The type to check +/// \param num_params If given, check the the given code_typet expects this +/// number of parameters +/// \param return_type If given, check the return type of the given code_typet +/// matches return_type +/// \return The type cast to a code_typet +const code_typet &require_type::require_code_type( + const typet &type, + optionalt num_params) +{ + REQUIRE(type.id()==ID_code); + const code_typet &code_type=to_code_type(type); + if(num_params) + REQUIRE(code_type.parameters().size()==num_params.value()); + return code_type; +} + +/// Verify a given type is a java_generic_type, optionally checking +/// that it's associated type variables match a given set of identifiers +/// \param type The type to check +/// \param type_variables An optional set of type variable identifiers which +/// should be expected as the type parameters of the generic type. +/// \return The given type, cast to a java_generic_typet +const java_generic_typet &require_type::require_java_generic_type_variables( + const typet &type, + const optionalt> &type_variables) +{ + REQUIRE(is_java_generic_type(type)); + const java_generic_typet &generic_type=to_java_generic_type(type); + if(type_variables) + { + const java_generic_typet::generic_type_variablest &generic_type_vars= + generic_type.generic_type_variables(); + REQUIRE(generic_type_vars.size()==type_variables.value().size()); + REQUIRE( + std::equal( + type_variables->begin(), + type_variables->end(), + generic_type_vars.begin(), + [](const irep_idt &type_var_name, const java_generic_parametert ¶m) + { + REQUIRE(!is_java_generic_inst_parameter((param))); + return param.type_variable().get_identifier()==type_var_name; + })); + } + + return generic_type; +} + +/// Verify a given type is a java_generic_type, optionally checking +/// that it's associated type variables match a given set of identifiers +/// \param type The type to check +/// \param type_variables An optional set of type variable identifiers which +/// should be expected as the type parameters of the generic type. +/// \return The given type, cast to a java_generic_typet +const java_generic_typet + &require_type::require_java_generic_type_instantiations( + const typet &type, + const optionalt> &type_instantiations) +{ + REQUIRE(is_java_generic_type(type)); + const java_generic_typet &generic_type=to_java_generic_type(type); + if(type_instantiations) + { + const java_generic_typet::generic_type_variablest &generic_type_vars= + generic_type.generic_type_variables(); + REQUIRE(generic_type_vars.size()==type_instantiations.value().size()); + REQUIRE( + std::equal( + type_instantiations->begin(), + type_instantiations->end(), + generic_type_vars.begin(), + [](const irep_idt &type_id, const java_generic_parametert ¶m) + { + REQUIRE(is_java_generic_inst_parameter((param))); + return param.subtype()==symbol_typet(type_id); + })); + } + + + return generic_type; +} + +/// Verify a given type is a java_generic_parameter, optionally checking +/// that it's associated type variables match a given set of identifiers +/// \param type The type to check +/// \param type_variables An optional set of type variable identifiers which +/// should be expected as the type parameters of the generic type. +/// \return The given type, cast to a java_generic_typet +const java_generic_parametert + &require_type::require_java_generic_parameter_variables( + const typet &type, + const optionalt> &type_variables) +{ + REQUIRE(is_java_generic_parameter(type)); + const java_generic_parametert &generic_param=to_java_generic_parameter(type); + if(type_variables) + { + const java_generic_parametert::type_variablest &generic_type_vars= + generic_param.type_variables(); + REQUIRE(generic_type_vars.size()==type_variables.value().size()); + REQUIRE( + std::equal( + type_variables->begin(), + type_variables->end(), + generic_type_vars.begin(), + []( + const irep_idt &type_var_name, + const java_generic_parametert::type_variablet ¶m) + { + REQUIRE(!is_java_generic_inst_parameter((param))); + return param.get_identifier()==type_var_name; + })); + } + + return generic_param; +} + +const typet &require_type::require_java_non_generic_type( + const typet &type, + const optionalt &expect_type) +{ + REQUIRE(!is_java_generic_parameter(type)); + REQUIRE(!is_java_generic_type(type)); + REQUIRE(!is_java_generic_inst_parameter(type)); + if(expect_type) + REQUIRE(type.subtype()==symbol_typet(expect_type.value())); + return type; +} + diff --git a/unit/testing-utils/require_type.h b/unit/testing-utils/require_type.h new file mode 100644 index 00000000000..482b95c535d --- /dev/null +++ b/unit/testing-utils/require_type.h @@ -0,0 +1,47 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Helper functions for requiring specific types +/// If the type is of the wrong type, throw a CATCH exception +/// Also checks associated properties and returns a casted version of the +/// expression. + +#ifndef CPROVER_TESTING_UTILS_REQUIRE_TYPE_H +#define CPROVER_TESTING_UTILS_REQUIRE_TYPE_H + +#include +#include +#include + + +// NOLINTNEXTLINE(readability/namespace) +namespace require_type +{ + const code_typet &require_code_type( + const typet &type, + const optionalt num_params); + + const java_generic_typet &require_java_generic_type_variables( + const typet &type, + const optionalt> &type_variables); + + const java_generic_typet &require_java_generic_type_instantiations( + const typet &type, + const optionalt> &type_instantiations); + + const java_generic_parametert &require_java_generic_parameter_variables( + const typet &type, + const optionalt> &type_variables); + + const typet &require_java_non_generic_type( + const typet &type, + const optionalt &expect_type); +} + +#endif // CPROVER_TESTING_UTILS_REQUIRE_TYPE_H