From cb2261f839815209d880a69315b5ed61717fdd95 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Mon, 2 Oct 2017 15:50:23 +0100 Subject: [PATCH 1/4] TG-949: feature/specialize generic methods with concrete types --- .../specialize_java_generic_method.cpp | 308 ++++++++++++++++ .../specialize_java_generic_method.h | 74 ++++ .../generics$GList.class | Bin 0 -> 373 bytes .../generics$GMap.class | Bin 0 -> 391 bytes .../generics$bound_element.class | Bin 0 -> 636 bytes .../generics$compound_element.class | Bin 0 -> 751 bytes .../generics$double_element.class | Bin 0 -> 866 bytes .../generics$element.class | Bin 0 -> 427 bytes .../generics.class | Bin 0 -> 974 bytes .../generics.java | 67 ++++ .../java_bytecode_specialize_generics.cpp | 338 ++++++++++++++++++ unit/testing-utils/require_type.cpp | 150 ++++++++ unit/testing-utils/require_type.h | 47 +++ 13 files changed, 984 insertions(+) create mode 100644 src/java_bytecode/specialize_java_generic_method.cpp create mode 100644 src/java_bytecode/specialize_java_generic_method.h create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics$GList.class create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics$GMap.class create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics$bound_element.class create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics$compound_element.class create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics$double_element.class create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics$element.class create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics.class create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/generics.java create mode 100644 unit/java_bytecode/java_bytecode_specialize_generics/java_bytecode_specialize_generics.cpp create mode 100644 unit/testing-utils/require_type.cpp create mode 100644 unit/testing-utils/require_type.h 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..2c04f944ef0 --- /dev/null +++ b/src/java_bytecode/specialize_java_generic_method.cpp @@ -0,0 +1,308 @@ +/*******************************************************************\ + +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; + + for(code_typet::parametert ¶meter : specialized_code.parameters()) + { + 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 0000000000000000000000000000000000000000..4fac9ebedbe26a4486a56ad81fee67087ec04bed GIT binary patch literal 373 zcmZWlO-sW-5Ph4ZNfVPcetQ(@A+}(9@MKFb1w{yYsPw*xOWYE-kWKtw9;D#GAK;G? zC&3^n%kF#oX6DT>pI`4E04{Oj!bIPLh0wvCgF^Jtv}g;7Lx3yOf#YWmOQ5W~-}s&0qL9=PDcDCu@3q zBvKTWW%td#8Q#2^_m9^%07LA#Fwyp4A#||eV4J}%@1*Vw7`!+WN)$5HBVr?|WI1LC zy5IESjKP{LZUsX-mP%Yz_lYQOc#;$2PGzQeSrrsV(ZxwT=a0OfbCvb4letLC(d-{? z{I`spOczy=ic?wZ21{4RwV;m`*ghQWIN1G>?3`Wl2XglX{<)$_COOwyXom2&6$Z0g z57Sy|W1se7(TZ3Y)*b4Iu7eh#OVI%gI)K+ZdIsygz<6qEJbLY>)+U8j`Wf&MG`NN> MLXWa0*0BkE0$ia}vj6}9 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..a637dfd3c9c8e9cf0af27c048203f82bd181091d GIT binary patch literal 636 zcmZuuO;5r=5PeH2m0GkS;3ta6q0~e?cv8ZJ#KZ*g0D3hA)>=|ZLR){ACK?kD{s4cJ zaTeM@#KU%HUf;}nGyDDX`32w{$7v+7qe8~6i1ri|6_gl~+~p&NY-?yeTQ%46>{>e< z_4wqHA>DCo&kDi`XOO$?yBoq%!IR@x&KT5|%{@MG`o2Kxj^_johKw-hWL52q z!%3fCIl@IIp5auCuR+DC1`S6VQcx6>8459@(i?}~;6bd5djXaH$+c^b*3on=-{(Gq zKHuj|nn5zAzT<`{(L2cWI0-r=2byV`rFC5xp;)4$Awz%GC@K?Ea8>i<9nAbd;*~O5 zE`3vUgP4Gh4Pps?kuZVE<{P9J3Kpq)B$g$76S=4)mPiQ+Y2IF)3g^gfKB~);xtZMp Twx~w}+c>0KC6y%haRB@RcMNzN literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..550d17bff226b2bc3a21b4b527d2ead6805b419b GIT binary patch literal 751 zcmZuvT~8B16g|_gZI>-wS^-f}gkqMOhz~p%yEFzOhNRI4h_7bbPL?6<)a-7JKT8t{ z2@n1NeiZRcyZs3GFgth7oO|xMd*}A<<}ZK)yec7wXEyTKG|_VlTNbtja;RKIjCWjATI9ztyS zY&eR#@i%G2NX##nMt#JAF9E$j+xOd0j=aPWON(!FnHC{lA6?th?pYZDU! z%QJ;^hFQ<_TAaez;>h!S2N^Dwg}~DIuHATj1<|-h<~L6Q zRelTHfp=UrJR)n6UucLcWanIatm3owVOnvOd23it^ERnv)bfo#$o^umSmHyP@|fl( Zb~o^ZoD80##J$SM!V44`=eWNF{sD5>o{#_l literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..57c1af60d23d017a364d69eb04f957763140efff GIT binary patch literal 866 zcmZuvTW=CU6#jdIk=jX5peN)-w^$MeMn#xTq+Xlkw?kJ0q=BHTkZ}= zyo1lWuLs)l3i8W=;_@T^HEFyhpVXIK)@GR45jFGMf9h zi$!70Xp(0WTg=?0^@P0%>TI=k4OP8C;yXQsdz20}P~q9eeO5_*jam@ar9N5RzeZ}& zkRPY&NaK*SUQVe!VEIElngYxQIs%Yh^k&C2j@bKZ+P6cr$#T1ROpFA{-l8tiD!@mP JwnJS7{s3}qteOA- literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..cb9f6f71273f6e5fcb7cd0404cc178ae3bc4baef GIT binary patch literal 427 zcmZWlO-sW-5Ph4(rb!bU>$hG+dPpl+51zF2QYr{R4=vs|afw^fE#$-hEJ$|i=@0} zaHcX2WNGAT4VluDK(20#3Rdk;iDUOv)nJCaJ=Rf|~U zGahGzgu}_zy5eXZBBklF$`f%T^_*X;p6hizIB-3*aA@O*A*hR8eUnfngZ&$Mw~F>1 zXS^sxLB0Rar3*v7a=W_lU_XynlgVl+6X8&u!Vi{E>%tJU=R2PG;CQE literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..a7a753ffa5fcb6e3e7f372157c6e3f5de1528fd4 GIT binary patch literal 974 zcmZ`&+int36kUe`rvpQ8D!pKXhp4pq)8Ji32h%RCVkQYj$|qf4VV6fzu-4$ zQc@#{@!5aUxDFI(gFeixefD1aa@L;t_2>H!0BPiW2p}pE^TCC<4+b6>v=S0YAH0Yg zFtH_((vgP-J&z=|B_2zp1?I|)`e~!%RNkqYsw<~0VCEf1HTP;(tEE~JPXuNvjZUei z#*{$mdWyVEmUt@Q-aoKTC7ua*_6v546+I;#7g#D(6-(RYR^(cNjDS(JtB%#~G?hT| zKeTM%K5HOr}{@=jY-RWp-gt~YBtb~`696^*@R|Gh?qRb~seqYgXul4`!OIK6=Q zAP|h^WB({45Gb~-@<&eICsR$zC*UhKI?b|rW$XOFaQZDhhly3JQNW=ya;bs#@0fUw zu!$Goc)=0l+NDh_V?|(o;!e6iR_DGHm>%Y`(U^EtI#Ffnx;%_VCbzgaicKtU6w!;~ zcE{(zx&qPB0y0`qd1lo*>WJ#O2YXz&qTpZ_UeirwNxm8zsGq?)zrX;$Rl$dsCWdIa zaGQ_NGV*ijec;XijUug*3<=fkL>cBd}v^Dh;Ja7|V_ux7ved-_)`UZCwo*ul~ zArIq2tBdJm55{rG{r&>JF8ra-@F&jU`3d7o@*IARtmW!=3uBu0Du0$W%(K@Dy_@Wu z#s+o}!7fi5WcVR|V^<;~agV8+{Q~zfN8IMfGraRG?Rnw?(M!D1=a{%jyv1{nxJX { + } + + 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 From 008563b00db7fd10c2851c7ec1d716aa5a757dd4 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Fri, 13 Oct 2017 17:33:06 +0100 Subject: [PATCH 2/4] When instantiating a generic type, first check if it's previously been instantiated --- src/java_bytecode/generate_java_generic_type.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) 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; } From e16286a9ba39036e95add2d9379308b097f44b43 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Mon, 9 Oct 2017 15:17:28 +0100 Subject: [PATCH 3/4] [DO NOT MERGE] Revert "Reverting method descriptor loading" This reverts commit be94ecdd2caf2bf5193c2cd2ced1b1ae19ce22d9. --- .../java_bytecode_convert_method.cpp | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) 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; From 092d1611cf30f6afaef998a9550f10c077c22d91 Mon Sep 17 00:00:00 2001 From: Chris Ryder Date: Mon, 16 Oct 2017 15:30:57 +0100 Subject: [PATCH 4/4] Ensure 'this' parameter has a specialized type --- .../specialize_java_generic_method.cpp | 29 +++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/specialize_java_generic_method.cpp b/src/java_bytecode/specialize_java_generic_method.cpp index 2c04f944ef0..37515d4f712 100644 --- a/src/java_bytecode/specialize_java_generic_method.cpp +++ b/src/java_bytecode/specialize_java_generic_method.cpp @@ -82,10 +82,35 @@ const symbolt& specialize_java_generic_methodt::operator()( specialized_method.name= id2string(specialized_method.name)+signature_decoration; + + namespacet ns(symbol_table); for(code_typet::parametert ¶meter : specialized_code.parameters()) { - typet ¶meter_type=parameter.type(); - instantiate_generic_types(parameter_type, concrete_type_map, symbol_table); + 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.