diff --git a/regression/cbmc-java/iterator2/test.desc b/regression/cbmc-java/iterator2/test.desc index 68525dd9b76..1919744c42d 100644 --- a/regression/cbmc-java/iterator2/test.desc +++ b/regression/cbmc-java/iterator2/test.desc @@ -1,6 +1,6 @@ CORE iterator2.class ---cover location --unwind 3 --function iterator2.f +--cover location --unwind 3 --function iterator2.f ^EXIT=0$ ^SIGNAL=0$ ^.*SATISFIED$ diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index c9ddec10d81..240dafc0e29 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -79,7 +79,7 @@ bool ci_lazy_methodst::operator()( { const irep_idt methodid="java::"+id2string(classname)+"."+ id2string(method.name)+":"+ - id2string(method.signature); + id2string(method.descriptor); method_worklist2.push_back(methodid); } } @@ -505,4 +505,3 @@ irep_idt ci_lazy_methodst::get_virtual_method_target( else return irep_idt(); } - diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index d27ff99b41b..8f038c92440 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_language.h" #include "java_utils.h" +#include #include #include #include @@ -93,6 +94,33 @@ void java_bytecode_convert_classt::convert(const classt &c) } java_class_typet class_type; + if(c.signature.has_value() && c.signature.value()[0]=='<') + { + java_generics_class_typet generic_class_type; +#ifdef DEBUG + std::cout << "INFO: found generic class signature " + << c.signature.value() + << " in parsed class " + << c.name << "\n"; +#endif + try + { + const std::vector &generic_types=java_generic_type_from_string( + id2string(c.name), + c.signature.value()); + for(const typet &t : generic_types) + { + generic_class_type.generic_types() + .push_back(to_java_generic_parameter(t)); + } + class_type=generic_class_type; + } + catch(unsupported_java_class_signature_exceptiont) + { + warning() << "we currently don't support parsing for example double " + "bounded, recursive and wild card generics" << eom; + } + } class_type.set_tag(c.name); class_type.set(ID_base_name, c.name); @@ -166,7 +194,7 @@ void java_bytecode_convert_classt::convert(const classt &c) const irep_idt method_identifier= id2string(qualified_classname)+ "."+id2string(method.name)+ - ":"+method.signature; + ":"+method.descriptor; // Always run the lazy pre-stage, as it symbol-table // registers the function. debug() << "Adding symbol: method '" << method_identifier << "'" << eom; @@ -187,7 +215,49 @@ void java_bytecode_convert_classt::convert( symbolt &class_symbol, const fieldt &f) { - typet field_type=java_type_from_string(f.signature); + typet field_type; + if(f.signature.has_value()) + { + field_type=java_type_from_string_with_exception( + f.descriptor, + f.signature, + id2string(class_symbol.name)); + + /// this is for a free type variable, e.g., a field of the form `T f;` + if(is_java_generic_parameter(field_type)) + { +#ifdef DEBUG + std::cout << "fieldtype: generic " + << to_java_generic_parameter(field_type).type_variable() + .get_identifier() + << " name " << f.name << "\n"; +#endif + } + + /// this is for a field that holds a generic type, wither with instantiated + /// or with free type variables, e.g., `List l;` or `List l;` + else if(is_java_generic_type(field_type)) + { + java_generic_typet &with_gen_type= + to_java_generic_type(field_type); +#ifdef DEBUG + std::cout << "fieldtype: generic container type " + << std::to_string(with_gen_type.generic_type_variables().size()) + << " type " << with_gen_type.id() + << " name " << f.name + << " subtype id " << with_gen_type.subtype().id() << "\n"; +#endif + field_type=with_gen_type; + } + + /// This case is not possible, a field is either a non-instantiated type + /// variable or a generics container type. + INVARIANT( + !is_java_generic_inst_parameter(field_type), + "Cannot be an instantiated type variable here."); + } + else + field_type=java_type_from_string(f.descriptor); // is this a static field? if(f.is_static) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 00652d34618..f6d267ef087 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -252,7 +252,7 @@ const exprt java_bytecode_convert_methodt::variable( /// method conversion just yet. The caller should call /// java_bytecode_convert_method later to give the symbol/method a body. /// \par parameters: `class_symbol`: class this method belongs to -/// `method_identifier`: fully qualified method name, including type signature +/// `method_identifier`: fully qualified method name, including type descriptor /// (e.g. "x.y.z.f:(I)") /// `m`: parsed method object to convert /// `symbol_table`: global symbol table (will be modified) @@ -263,7 +263,7 @@ void java_bytecode_convert_method_lazy( symbol_tablet &symbol_table) { symbolt method_symbol; - typet member_type=java_type_from_string(m.signature); + typet member_type=java_type_from_string(m.descriptor); method_symbol.name=method_identifier; method_symbol.base_name=m.base_name; @@ -317,7 +317,7 @@ void java_bytecode_convert_methodt::convert( // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy) // associated to the method const irep_idt method_identifier= - id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature; + id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor; method_id=method_identifier; const symbolt &old_sym=*symbol_table.lookup(method_identifier); @@ -350,7 +350,17 @@ void java_bytecode_convert_methodt::convert( // Construct a fully qualified name for the parameter v, // e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a // symbol_exprt with the parameter and its type - typet t=java_type_from_string(v.signature); + typet t; + if(v.signature.has_value()) + { + t=java_type_from_string_with_exception( + v.descriptor, + v.signature, + id2string(class_symbol.name)); + } + else + t=java_type_from_string(v.descriptor); + std::ostringstream id_oss; id_oss << method_id << "::" << v.name; irep_idt identifier(id_oss.str()); diff --git a/src/java_bytecode/java_bytecode_parse_tree.cpp b/src/java_bytecode/java_bytecode_parse_tree.cpp index f19de120195..b8a60d8ddca 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -28,6 +28,7 @@ void java_bytecode_parse_treet::classt::swap( std::swap(other.is_public, is_public); std::swap(other.is_protected, is_protected); std::swap(other.is_private, is_private); + std::swap(other.signature, signature); other.implements.swap(implements); other.fields.swap(fields); other.methods.swap(methods); @@ -151,7 +152,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const out << "synchronized "; out << name; - out << " : " << signature; + out << " : " << descriptor; out << '\n'; @@ -188,7 +189,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const for(const auto &v : local_variable_table) { out << " " << v.index << ": " << v.name << ' ' - << v.signature << '\n'; + << v.descriptor << '\n'; } out << '\n'; @@ -212,7 +213,7 @@ void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const out << "static "; out << name; - out << " : " << signature << ';'; + out << " : " << descriptor << ';'; out << '\n'; } diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index d982a62cd39..8470d0cb864 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include @@ -54,7 +55,8 @@ class java_bytecode_parse_treet class membert { public: - std::string signature; + std::string descriptor; + optionalt signature; irep_idt name; bool is_public, is_protected, is_private, is_static, is_final; annotationst annotations; @@ -62,8 +64,8 @@ class java_bytecode_parse_treet virtual void output(std::ostream &out) const = 0; membert(): - is_public(false), is_protected(false), is_private(false), - is_static(false), is_final(false) + is_public(false), is_protected(false), + is_private(false), is_static(false), is_final(false) { } }; @@ -100,7 +102,8 @@ class java_bytecode_parse_treet { public: irep_idt name; - std::string signature; + std::string descriptor; + optionalt signature; std::size_t index; std::size_t start_pc; std::size_t length; @@ -174,7 +177,7 @@ class java_bytecode_parse_treet typedef std::list implementst; implementst implements; - + optionalt signature; typedef std::list fieldst; typedef std::list methodst; fieldst fields; diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 1b424291a5c..ea41593e88a 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -125,6 +125,7 @@ class java_bytecode_parsert:public parsert void rbytecode(methodt::instructionst &); void get_class_refs(); void get_class_refs_rec(const typet &); + void parse_local_variable_type_table(methodt &method); void skip_bytes(std::size_t bytes) { @@ -333,19 +334,48 @@ void java_bytecode_parsert::get_class_refs() } } - for(const auto &m : parse_tree.parsed_class.fields) + for(const auto &field : parse_tree.parsed_class.fields) { - typet t=java_type_from_string(m.signature); - get_class_refs_rec(t); + typet field_type; + if(field.signature.has_value()) + { + field_type=java_type_from_string_with_exception( + field.descriptor, + field.signature, + "java::"+id2string(parse_tree.parsed_class.name)); + } + else + field_type=java_type_from_string(field.descriptor); + + get_class_refs_rec(field_type); } - for(const auto &m : parse_tree.parsed_class.methods) + for(const auto &method : parse_tree.parsed_class.methods) { - typet t=java_type_from_string(m.signature); - get_class_refs_rec(t); - for(const auto &var : m.local_variable_table) + typet method_type; + if(method.signature.has_value()) { - typet var_type=java_type_from_string(var.signature); + method_type=java_type_from_string_with_exception( + method.descriptor, + method.signature, + "java::"+id2string(parse_tree.parsed_class.name)); + } + else + method_type=java_type_from_string(method.descriptor); + + get_class_refs_rec(method_type); + for(const auto &var : method.local_variable_table) + { + typet var_type; + if(var.signature.has_value()) + { + var_type=java_type_from_string_with_exception( + var.descriptor, + var.signature, + "java::"+id2string(parse_tree.parsed_class.name)); + } + else + var_type=java_type_from_string(var.descriptor); get_class_refs_rec(var_type); } } @@ -628,7 +658,8 @@ void java_bytecode_parsert::rfields(classt &parsed_class) field.is_static=(access_flags&ACC_STATIC)!=0; field.is_final=(access_flags&ACC_FINAL)!=0; field.is_enum=(access_flags&ACC_ENUM)!=0; - field.signature=id2string(pool_entry(descriptor_index).s); + + field.descriptor=id2string(pool_entry(descriptor_index).s); field.is_public=(access_flags&ACC_PUBLIC)!=0; field.is_protected=(access_flags&ACC_PROTECTED)!=0; field.is_private=(access_flags&ACC_PRIVATE)!=0; @@ -936,7 +967,7 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method) it->source_location .set_function( "java::"+id2string(parse_tree.parsed_class.name)+"."+ - id2string(method.name)+":"+method.signature); + id2string(method.name)+":"+method.descriptor); } // line number of method @@ -944,6 +975,11 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method) method.source_location.set_line( method.instructions.begin()->source_location.get_line()); } + else if(attribute_name=="Signature") + { + u2 signature_index=read_u2(); + method.signature=id2string(pool_entry(signature_index).s); + } else if(attribute_name=="RuntimeInvisibleAnnotations" || attribute_name=="RuntimeVisibleAnnotations") { @@ -960,7 +996,12 @@ void java_bytecode_parsert::rfield_attribute(fieldt &field) irep_idt attribute_name=pool_entry(attribute_name_index).s; - if(attribute_name=="RuntimeInvisibleAnnotations" || + if(attribute_name=="Signature") + { + u2 signature_index=read_u2(); + field.signature=id2string(pool_entry(signature_index).s); + } + else if(attribute_name=="RuntimeInvisibleAnnotations" || attribute_name=="RuntimeVisibleAnnotations") { rRuntimeAnnotation_attribute(field.annotations); @@ -1022,12 +1063,16 @@ void java_bytecode_parsert::rcode_attribute(methodt &method) method.local_variable_table[i].index=index; method.local_variable_table[i].name=pool_entry(name_index).s; - method.local_variable_table[i].signature= + method.local_variable_table[i].descriptor= id2string(pool_entry(descriptor_index).s); method.local_variable_table[i].start_pc=start_pc; method.local_variable_table[i].length=length; } } + else if(attribute_name=="LocalVariableTypeTable") + { + parse_local_variable_type_table(method); + } else if(attribute_name=="StackMapTable") { u2 stack_map_entries=read_u2(); @@ -1307,6 +1352,11 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class) } } } + else if(attribute_name=="Signature") + { + u2 signature_index=read_u2(); + parsed_class.signature=id2string(pool_entry(signature_index).s); + } else if(attribute_name=="RuntimeInvisibleAnnotations" || attribute_name=="RuntimeVisibleAnnotations") { @@ -1356,7 +1406,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class) method.is_native=(access_flags&ACC_NATIVE)!=0; method.name=pool_entry(name_index).s; method.base_name=pool_entry(name_index).s; - method.signature=id2string(pool_entry(descriptor_index).s); + method.descriptor=id2string(pool_entry(descriptor_index).s); size_t flags=(method.is_public?1:0)+ (method.is_protected?1:0)+ @@ -1401,3 +1451,42 @@ bool java_bytecode_parse( return java_bytecode_parse(in, parse_tree, message_handler); } + +/// Parses the local variable type table of a method. The LVTT holds generic +/// type information for variables in the local variable table (LVT). At most as +/// many variables as present in the LVT can be in the LVTT. +void java_bytecode_parsert::parse_local_variable_type_table(methodt &method) +{ + u2 local_variable_type_table_length=read_u2(); + + INVARIANT( + local_variable_type_table_length<=method.local_variable_table.size(), + "Local variable type table cannot have more elements " + "than the local variable table."); + for(std::size_t i=0; ivar.name!=it->var.name || - pred_var->var.signature!=it->var.signature) + pred_var->var.descriptor!=it->var.descriptor) { // These sorts of infeasible edges can occur because // jsr handling is presently vague (any subroutine is @@ -714,7 +714,7 @@ void java_bytecode_convert_methodt::setup_local_variables( #ifdef DEBUG debug() << "jcm: setup-local-vars: m.is_static " - << m.is_static << " m.signature " << m.signature << eom; + << m.is_static << " m.descriptor " << m.descriptor << eom; debug() << "jcm: setup-local-vars: lv arg slots " << slots_for_parameters << eom; debug() << "jcm: setup-local-vars: lvt size " @@ -765,10 +765,13 @@ void java_bytecode_convert_methodt::setup_local_variables( #ifdef DEBUG debug() << "jcm: setup-local-vars: merged variable: idx " << v.var.index - << " name " << v.var.name << " v.var.signature '" - << v.var.signature << "' holes " << v.holes.size() << eom; + << " name " << v.var.name << " v.var.descriptor '" + << v.var.descriptor << "' holes " << v.holes.size() << eom; #endif - typet t=java_type_from_string(v.var.signature); + typet t; + // TODO: might need changing once descriptor/signature issue is resolved + t=java_type_from_string(v.var.descriptor); + std::ostringstream id_oss; id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name; irep_idt identifier(id_oss.str()); diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index b3f908a1ca8..102cdb493cc 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -6,9 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "java_types.h" - -#include #include #include @@ -16,6 +13,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include + +#include "java_types.h" +#include "java_utils.h" + +#ifdef DEBUG +#include +#endif typet java_int_type() { @@ -92,7 +97,11 @@ reference_typet java_array_type(const char subtype) case 'j': subtype_str="long"; break; case 'l': subtype_str="long"; break; case 'a': subtype_str="reference"; break; - default: UNREACHABLE; + default: +#ifdef DEBUG + std::cout << "Unrecognised subtype str: " << subtype << std::endl; +#endif + UNREACHABLE; } irep_idt class_name="array["+subtype_str+"]"; @@ -114,7 +123,7 @@ bool is_java_array_tag(const irep_idt& tag) bool is_reference_type(const char t) { - return 'a' == t; + return 'a'==t; } typet java_type_from_char(char t) @@ -158,13 +167,66 @@ exprt java_bytecode_promotion(const exprt &expr) return typecast_exprt(expr, new_type); } -typet java_type_from_string(const std::string &src) +/// Transforms a string representation of a Java type into an internal type +/// representation thereof. +/// +/// Example use are object types like "Ljava/lang/Integer;", type variables like +/// "TE;" which require a non-empty \p class_name or generic types like +/// "Ljava/util/List;" or "Ljava/util/List;" +/// +/// \param src: the string representation as used in the class file +/// \param class_name_prefix: name of class to append to generic type variables +/// \returns internal type representation for GOTO programs +typet java_type_from_string( + const std::string &src, + const std::string &class_name_prefix) { if(src.empty()) return nil_typet(); + // a java type is encoded in different ways + // - a method type is encoded as '(...)R' where the parenthesis include the + // parameter types and R is the type of the return value + // - atomic types are encoded as single characters + // - array types are encoded as '[' followed by the type of the array + // content + // - object types are named with prefix 'L' and suffix ';', e.g., + // Ljava/lang/Object; + // - type variables are similar to object types but have the prefix 'T' switch(src[0]) { + case '<': + { + // The method signature can optionally have a collection of formal + // type parameters (e.g. on generic methods on non-generic classes + // or generic static methods). For now we skip over this part of the + // signature and continue parsing the rest of the signature as normal + // So for example, the following java method: + // static void foo(T t, U u, int x); + // Would have a signature that looks like: + // (TT;TU;I)V + // So we skip all inside the angle brackets and parse the rest of the + // string: + // (TT;TU;I)V + size_t closing_generic=find_closing_delimiter(src, 0, '<', '>'); + if(closing_generic==std::string::npos) + { + throw unsupported_java_class_signature_exceptiont( + "Failed to find generic signature closing delimiter"); + } + const typet &method_type=java_type_from_string( + src.substr(closing_generic+1, std::string::npos), class_name_prefix); + + // This invariant being violated means that tkiley has not understood + // part of the signature spec. + // Only class and method signatures can start with a '<' and classes are + // handled separately. + INVARIANT( + method_type.id()==ID_code, + "This should correspond to method signatures only"); + + return method_type; + } case '(': // function type { std::size_t e_pos=src.rfind(')'); @@ -174,7 +236,9 @@ typet java_type_from_string(const std::string &src) code_typet result; result.return_type()= - java_type_from_string(std::string(src, e_pos+1, std::string::npos)); + java_type_from_string( + std::string(src, e_pos+1, std::string::npos), + class_name_prefix); for(std::size_t i=1; i' + i=find_closing_delimiter(src, generic_open, '<', '>')+1; + else + i=src.find(';', i); // ends on ; break; } + + // parameter is an array else if(src[i]=='[') i++; + + // parameter is a type variable + else if(src[i]=='T') + i=src.find(';', i); // ends on ; + + // type is an atomic type (just one character) else break; } std::string sub_str=src.substr(start, i-start+1); - param.type()=java_type_from_string(sub_str); + param.type()=java_type_from_string(sub_str, class_name_prefix); if(param.type().id()==ID_symbol) param.type()=java_reference_type(param.type()); @@ -215,9 +295,11 @@ typet java_type_from_string(const std::string &src) return nil_typet(); char subtype_letter=src[1]; const typet subtype= - java_type_from_string(src.substr(1, std::string::npos)); + java_type_from_string(src.substr(1, std::string::npos), + class_name_prefix); if(subtype_letter=='L' || // [L denotes a reference array of some sort. - subtype_letter=='[') // Array-of-arrays + subtype_letter=='[' || // Array-of-arrays + subtype_letter=='T') // Array of generic types subtype_letter='A'; typet tmp=java_array_type(std::tolower(subtype_letter)); tmp.subtype().set(ID_C_element_type, subtype); @@ -233,14 +315,110 @@ typet java_type_from_string(const std::string &src) case 'Z': return java_boolean_type(); case 'V': return java_void_type(); case 'J': return java_long_type(); - + case 'T': + { + // parse name of type variable + INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); + PRECONDITION(!class_name_prefix.empty()); + irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2)); + return java_generic_parametert( + type_var_name, + java_type_from_string("Ljava/lang/Object;").subtype()); + } case 'L': { // ends on ; if(src[src.size()-1]!=';') return nil_typet(); - std::string class_name=src.substr(1, src.size()-2); + std::size_t f_pos=src.find('<', 1); + // get generic type information + if(f_pos!=std::string::npos) + { + std::size_t e_pos=find_closing_delimiter(src, f_pos, '<', '>'); + if(e_pos==std::string::npos) + throw unsupported_java_class_signature_exceptiont( + "recursive generic"); + + // construct container type + std::string generic_container_class=src.substr(1, f_pos-1); + + for(unsigned i=0; i` a vector with two elements would be returned +/// +/// \returns vector of java types representing the generic type variables +std::vector java_generic_type_from_string( + const std::string &class_name, + const std::string &src) +{ + /// the class signature is of the form + size_t signature_end=find_closing_delimiter(src, 0, '<', '>'); + INVARIANT( + src[0]=='<' && signature_end!=std::string::npos, + "Class signature has unexpected format"); + std::string signature(src.substr(1, signature_end-1)); + + if(signature.find(";:")!=std::string::npos) + throw unsupported_java_class_signature_exceptiont("multiple bounds"); + + PRECONDITION(signature[signature.size()-1]==';'); + + std::vector types; + size_t var_sep=signature.find(';'); + while(var_sep!=std::string::npos) + { + size_t bound_sep=signature.find(':'); + INVARIANT(bound_sep!=std::string::npos, "No bound for type variable."); + std::string type_var_name( + "java::"+class_name+"::"+signature.substr(0, bound_sep)); + std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep)); + + java_generic_parametert type_var_type( + type_var_name, + java_type_from_string(bound_type, class_name).subtype()); + + types.push_back(type_var_type); + signature=signature.substr(var_sep+1, std::string::npos); + var_sep=signature.find(';'); + } + return types; +} + // java/lang/Object -> java.lang.Object static std::string slash_to_dot(const std::string &src) { diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 27ec5becbb4..e4c370157e0 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -10,8 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_TYPES_H #define CPROVER_JAVA_BYTECODE_JAVA_TYPES_H +#include #include #include +#include +#include +#include class java_class_typet:public class_typet { @@ -66,8 +70,13 @@ bool is_reference_type(char t); // a reference typet java_type_from_char(char t); -typet java_type_from_string(const std::string &); +typet java_type_from_string( + const std::string &, + const std::string &class_name_prefix=""); char java_char_from_type(const typet &type); +std::vector java_generic_type_from_string( + const std::string &, + const std::string &); typet java_bytecode_promotion(const typet &); exprt java_bytecode_promotion(const exprt &); @@ -76,4 +85,298 @@ bool is_java_array_tag(const irep_idt& tag); bool is_valid_java_array(const struct_typet &type); + +/// class to hold a Java generic type +/// upper bound can specify type requirements +class java_generic_parametert:public reference_typet +{ +public: + typedef symbol_typet type_variablet; + typedef std::vector type_variablest; + + java_generic_parametert(const irep_idt &_type_var_name, const typet &_bound) : + // the reference_typet now needs a pointer width, here it uses the one + // defined in the reference_type function from c_types.cpp + reference_typet(_bound, config.ansi_c.pointer_width) + { + PRECONDITION(_bound.id()==ID_symbol); + set(ID_C_java_generic_parameter, true); + // bound must be symbol type + type_variables().push_back(symbol_typet(_type_var_name)); + } + + /// \return the type variable as symbol type + const type_variablet &type_variable() const + { + PRECONDITION(!type_variables().empty()); + return type_variables().front(); + } + + const type_variablest &type_variables() const + { + return (const type_variablest &)(find(ID_type_variables).get_sub()); + } + + type_variablest &type_variables() + { + return (type_variablest &)(add(ID_type_variables).get_sub()); + } +}; + +/// \param type: type the type to check +/// \return true if type is a generic Java parameter type, e.g., T in List +inline bool is_java_generic_parameter(const typet &type) +{ + return type.get_bool(ID_C_java_generic_parameter); +} + +/// \param type: source type +/// \return cast of type into a java_generic_parametert +inline const java_generic_parametert &to_java_generic_parameter( + const typet &type) +{ + PRECONDITION(is_java_generic_parameter(type)); + return static_cast(type); +} + +/// \param type: source type +/// \return cast of type into a java_generic_parameter +inline java_generic_parametert &to_java_generic_parameter(typet &type) +{ + PRECONDITION(is_java_generic_parameter(type)); + return static_cast(type); +} + +/// class to hold an instantiated type variable bound is exact, for example the +/// `java.lang.Integer` type in a `List` +class java_generic_inst_parametert:public java_generic_parametert +{ +public: + // uses empty name for base type variable java_generic_parametert as real name + // is not known here + explicit java_generic_inst_parametert(const typet &type) : + java_generic_parametert(irep_idt(), type) + { + set(ID_C_java_generic_inst_parameter, true); + } +}; + +/// \param type: the type to check +/// \return true if type is an instantiated generic Java type, e.g., the Integer +/// in List +inline bool is_java_generic_inst_parameter(const typet &type) +{ + return type.get_bool(ID_C_java_generic_inst_parameter); +} + +/// \param type: source type +/// \return cast of type into an instantiated java_generic_parameter +inline const java_generic_inst_parametert &to_java_generic_inst_parameter( + const typet &type) +{ + PRECONDITION( + type.id()==ID_pointer && + is_java_generic_inst_parameter(type)); + return static_cast(type); +} + +/// \param type: source type +/// \return cast of type into an instantiated java_generic_inst_parametert +inline java_generic_inst_parametert &to_java_generic_inst_parameter(typet &type) +{ + PRECONDITION( + type.id()==ID_pointer && + is_java_generic_inst_parameter(type)); + return static_cast(type); +} + +/// class to hold type with generic type variable, for example `java.util.List` +/// in either a reference of type List or List. The vector holds +/// the types of the type Variables, that is the vector has the length of the +/// number of type variables of the generic class. For example in `HashMap` it would contain two elements, each of type `java_generic_parametert`, +/// in `HashMap` it would contains two elements, the first of type +/// `java_generic_inst_parametert` and the second of type +/// `java_generic_parametert`. +class java_generic_typet:public reference_typet +{ +public: + typedef std::vector generic_type_variablest; + + explicit java_generic_typet(const typet &_type) : + reference_typet(_type, config.ansi_c.pointer_width) + { + set(ID_C_java_generic_type, true); + } + + + /// \return vector of type variables + const generic_type_variablest &generic_type_variables() const + { + return (const generic_type_variablest &)(find(ID_type_variables).get_sub()); + } + + /// \return vector of type variables + generic_type_variablest &generic_type_variables() + { + return (generic_type_variablest &)(add(ID_type_variables).get_sub()); + } +}; + + +/// \param type: the type to check +/// \return true if type is java type containing with generics, e.g., List +inline bool is_java_generic_type(const typet &type) +{ + return type.get_bool(ID_C_java_generic_type); +} + +/// \param type: source type +/// \return cast of type into java type with generics +inline const java_generic_typet &to_java_generic_type( + const typet &type) +{ + PRECONDITION( + type.id()==ID_pointer && + is_java_generic_type(type)); + return static_cast(type); +} + +/// \param type: source type +/// \return cast of type into java type with generics +inline java_generic_typet &to_java_generic_type(typet &type) +{ + PRECONDITION( + type.id()==ID_pointer && + is_java_generic_type(type)); + return static_cast(type); +} + +/// Class to hold a class with generics, extends the java class type with a +/// vector of java_generic_type variables. +/// +/// For example, a class definition `class MyGenericClass` +class java_generics_class_typet:public java_class_typet +{ + public: + typedef std::vector generic_typest; + + java_generics_class_typet() + { + set(ID_C_java_generics_class_type, true); + } + + const generic_typest &generic_types() const + { + return (const generic_typest &)(find(ID_generic_types).get_sub()); + } + + generic_typest &generic_types() + { + return (generic_typest &)(add(ID_generic_types).get_sub()); + } +}; + +/// \param type: the type to check +/// \return true if type is a java class type with generics +inline bool is_java_generics_class_type(const typet &type) +{ + return type.get_bool(ID_C_java_generics_class_type); +} + +/// \param type: the type to check +/// \return cast of type to java_generics_class_typet +inline const java_generics_class_typet &to_java_generics_class_type( + const java_class_typet &type) +{ + PRECONDITION(is_java_generics_class_type(type)); + return static_cast(type); +} + +/// \param type: source type +/// \return cast of type into a java class type with generics +inline java_generics_class_typet &to_java_generics_class_type( + java_class_typet &type) +{ + PRECONDITION(is_java_generics_class_type(type)); + return static_cast(type); +} + +/// Access information of instantiated type params of java instantiated type. +/// \param index: the index of the type variable +/// \param type: the type from which to extract the type variable +/// \return the type variable of t at the given index +inline const typet &java_generic_get_inst_type( + size_t index, + const java_generic_typet &type) +{ + const std::vector &gen_types= + type.generic_type_variables(); + PRECONDITION(index &gen_types=type.generic_types(); + + PRECONDITION(index &gen_types=type.generic_types(); + + PRECONDITION(index &signature, + const std::string &class_name) +{ + try + { + return java_type_from_string(signature.value(), class_name); + } + catch (unsupported_java_class_signature_exceptiont &e) + { + return java_type_from_string(descriptor, class_name); + } +} + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 9cb7fab0492..6521f9903d6 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -182,3 +182,51 @@ dereference_exprt checked_dereference(const exprt &expr, const typet &type) result.set(ID_java_member_access, true); return result; } + +/// Finds the corresponding closing delimiter to the given opening delimiter. It +/// is assumed that \p open_pos points to the opening delimiter \p open_char in +/// the \p src string. The depth of nesting is counted to identify the correct +/// closing delimiter. +/// +/// A typical use case is for example Java generic types, e.g., List> +/// +/// \param src: the source string to scan +/// \param open_pos: the initial position of the opening delimiter from where to +/// start the search +/// \param open_char: the opening delimiter +/// \param close_char: the closing delimiter +/// \returns the index of the matching corresponding closing delimiter in \p src +size_t find_closing_delimiter( + const std::string &src, + size_t open_pos, + char open_char, + char close_char) +{ + // having the same opening and closing delimiter does not allow for hierarchic + // structuring + PRECONDITION(open_char!=close_char); + PRECONDITION(src[open_pos]==open_char); + size_t c_pos=open_pos+1; + const size_t end_pos=src.size()-1; + size_t depth=0; + + while(c_pos<=end_pos) + { + if(src[c_pos]=='<') + depth++; + else if(src[c_pos]=='>') + { + if(depth==0) + return c_pos; + depth--; + } + c_pos++; + // limit depth to sensible values + INVARIANT( + depth<=(src.size()-open_pos), + "No closing \'"+std::to_string(close_char)+ + "\' found in signature to parse."); + } + // did not find corresponding closing '>' + return std::string::npos; +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index ed26fe1caf6..9428494db93 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -66,4 +66,10 @@ irep_idt resolve_friendly_method_name( /// \param type: expected result type (typically expr.type().subtype()) dereference_exprt checked_dereference(const exprt &expr, const typet &type); +size_t find_closing_delimiter( + const std::string &src, + size_t position, + char open_char, + char close_char); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 30e7b73a1a1..540e09bf5b8 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -824,6 +824,12 @@ IREP_ID_ONE(switch_case_number) IREP_ID_ONE(java_array_access) IREP_ID_ONE(java_member_access) IREP_ID_ONE(integer_dereference) +IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter) +IREP_ID_TWO(C_java_generic_inst_parameter, #java_generic_inst_parameter) +IREP_ID_TWO(C_java_generic_type, #java_generic_type) +IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) +IREP_ID_TWO(generic_types, #generic_types) +IREP_ID_TWO(type_variables, #type_variables) #undef IREP_ID_ONE #undef IREP_ID_TWO diff --git a/unit/Makefile b/unit/Makefile index dfeb41376e1..1d5b11ff73b 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,6 +20,7 @@ SRC += unit_tests.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ miniBDD_new.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/Bar.class b/unit/java_bytecode/java_bytecode_parse_generics/Bar.class new file mode 100644 index 00000000000..3b52a177cca Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/Bar.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/Bar.java b/unit/java_bytecode/java_bytecode_parse_generics/Bar.java new file mode 100644 index 00000000000..273a20744dc --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/Bar.java @@ -0,0 +1,4 @@ +class Bar extends Foo +{ + +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.class b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.class new file mode 100644 index 00000000000..83f7444582f Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.java b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.java new file mode 100644 index 00000000000..47f91d66f86 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.java @@ -0,0 +1,4 @@ +interface BasicInterface +{ + int getX(); +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.class b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.class new file mode 100644 index 00000000000..c61caf0740a Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.java b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.java new file mode 100644 index 00000000000..3a87c8d8c88 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.java @@ -0,0 +1,4 @@ +interface BasicInterfaceCopy +{ + int getX(); +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.class new file mode 100644 index 00000000000..65bdd950e85 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.java b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.java new file mode 100644 index 00000000000..5eb08c7a2a9 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.java @@ -0,0 +1,4 @@ +class DerivedGeneric extends SimpleGeneric +{ + +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/Foo.class b/unit/java_bytecode/java_bytecode_parse_generics/Foo.class new file mode 100644 index 00000000000..e64c1c07f6a Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/Foo.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/Foo.java b/unit/java_bytecode/java_bytecode_parse_generics/Foo.java new file mode 100644 index 00000000000..c81911835c6 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/Foo.java @@ -0,0 +1,8 @@ +class Foo implements BasicInterface +{ + public int x; + + public int getX() { + return x; + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.class b/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.class new file mode 100644 index 00000000000..1b69af949ac Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java b/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java new file mode 100644 index 00000000000..98cf9333743 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java @@ -0,0 +1,6 @@ +class GenericArray +{ + public T [] t; + public Integer [] Ia; + public int [] ia; +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.class b/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.class new file mode 100644 index 00000000000..e82142ef77c Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java b/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java new file mode 100644 index 00000000000..5a5eb5221f7 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java @@ -0,0 +1,26 @@ +public class GenericFunctions +{ + public static void processSimpleGeneric(SimpleGeneric x) { + assert(x.t==null); + } + + // Test a wildcard generic bound by an interface + public static void processUpperBoundInterfaceGeneric(SimpleGeneric x) { + assert(x.t.getX() == 4); + } + + // Test a wild card generic bound by a class + public static void processUpperBoundClassGeneric(SimpleGeneric x) { + assert(x.t.getX() == 4); + } + + // Test a wild card generic bound by a class and an interface + public static void processDoubleUpperBoundClassGeneric(SimpleGeneric x) { + assert(x.t.getX() == 4); + } + + // Test a wild card generic bound by two interfaces + public static void processDoubleUpperBoundInterfaceGeneric(SimpleGeneric x) { + assert(x.t.getX() == 4); + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.class new file mode 100644 index 00000000000..d637a7292a4 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java b/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java new file mode 100644 index 00000000000..d3582c8bd46 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java @@ -0,0 +1,4 @@ +class RecursiveGeneric extends SimpleRecursiveGeneric +{ + +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.class new file mode 100644 index 00000000000..6ade3945c8d Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.java b/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.java new file mode 100644 index 00000000000..6db3d7bacbe --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.java @@ -0,0 +1,11 @@ +class SimpleGeneric +{ + public T t; + + public static SimpleGeneric makeGeneric(T value) + { + SimpleGeneric newST = new SimpleGeneric(); + newST.t = value; + return newST; + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.class new file mode 100644 index 00000000000..3ca52a2b92b Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.java b/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.java new file mode 100644 index 00000000000..e95851602da --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.java @@ -0,0 +1,4 @@ +class SimpleRecursiveGeneric> +{ + public T t; +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.class b/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.class new file mode 100644 index 00000000000..bf78c910d19 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.java b/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.java new file mode 100644 index 00000000000..29ad10e2e25 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.java @@ -0,0 +1,54 @@ +public class WildcardGenericFunctions +{ + // Test a wild card generic type + public static void processSimpleGeneric(SimpleGeneric x) { + assert(x.t.equals(null)); + } + + // Test a wildcard generic bound by an interface + public static void processUpperBoundInterfaceGeneric(SimpleGeneric x) { + assert(x.t.getX() == 4); + } + + // Test a wild card generic bound by a class + public static void processUpperBoundClassGeneric(SimpleGeneric x) { + assert(x.t.getX() == 4); + } + + // It isn't legal to have an wild card with two upper bounds + // Per language spec on intersection types + + public static void processLowerBoundGeneric(SimpleGeneric x, Foo assign) { + x.t = assign; + } + + // It is not legal Java to specify both an upper and lower bound + // public static void processBoundSuperClassGeneric(SimpleGeneric x, Foo assign) { + // x.t = assign; + // } + + // Test a wild card generic bound by a class + // public static void processBoundClassGenericDoubleBound(SimpleGeneric x) { + // assert(x.t.getX() == 4); + // } + + public static void test() + { + SimpleGeneric myGenericValue = new SimpleGeneric(); + myGenericValue.t = null; + processSimpleGeneric(myGenericValue); + + myGenericValue.t = new Foo(); + myGenericValue.t.x = 4; + processUpperBoundInterfaceGeneric(myGenericValue); + + SimpleGeneric anotherGenericValue = new SimpleGeneric(); + anotherGenericValue.t = new Bar(); + anotherGenericValue.t.x = 4; + processUpperBoundClassGeneric(anotherGenericValue); + + + SimpleGeneric baseGenericValue = new SimpleGeneric(); + processLowerBoundGeneric(baseGenericValue, new Foo()); + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics$bound_element.class b/unit/java_bytecode/java_bytecode_parse_generics/generics$bound_element.class new file mode 100644 index 00000000000..ef168d8e34c Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/generics$bound_element.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics$double_bound_element.class b/unit/java_bytecode/java_bytecode_parse_generics/generics$double_bound_element.class new file mode 100644 index 00000000000..af550821f2a Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/generics$double_bound_element.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics$dummyInterface.class b/unit/java_bytecode/java_bytecode_parse_generics/generics$dummyInterface.class new file mode 100644 index 00000000000..20f3e82c81b Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/generics$dummyInterface.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics$element.class b/unit/java_bytecode/java_bytecode_parse_generics/generics$element.class new file mode 100644 index 00000000000..f1c63b72dde Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/generics$element.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics$two_elements.class b/unit/java_bytecode/java_bytecode_parse_generics/generics$two_elements.class new file mode 100644 index 00000000000..4bbc9b11c62 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/generics$two_elements.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics.class b/unit/java_bytecode/java_bytecode_parse_generics/generics.class new file mode 100644 index 00000000000..476830f150a Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/generics.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics.java b/unit/java_bytecode/java_bytecode_parse_generics/generics.java new file mode 100644 index 00000000000..b2e18689158 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/generics.java @@ -0,0 +1,59 @@ +public class generics { + + interface dummyInterface + { + int getX(); + } + + class element { + E elem; + } + + class bound_element { + NUM elem; + NUM f() { + return elem; + } + void g(NUM e) { + elem=e; + } + } + + class double_bound_element + { + T elem; + } + +// definitely need to do some tests with bounded two elements + // the java_generic_type_from_string does not work for complex types + // Need to to unblock just get it so it throws when failing rather than wrong + class two_elements + { + K k; + V v; + } + + + + public static boolean foo(String s) + { + if(s.length == 0) + return true; + return false; + } + + 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; + } +} 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 new file mode 100644 index 00000000000..bb4c6c70337 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -0,0 +1,47 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include + +#include +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_parse_derived_generic_class", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table= + load_java_class( + "DerivedGeneric", + "./java_bytecode/java_bytecode_parse_generics"); + + THEN("There should be a symbol for the DerivedGenreic class") + { + std::string class_prefix="java::DerivedGeneric"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol=new_symbol_table.lookup(class_prefix).value + ().get(); + REQUIRE(derived_symbol.is_type); + const typet &derived_type=derived_symbol.type; + REQUIRE(derived_type.id()==ID_struct); + const class_typet &class_type=to_class_type(derived_type); + REQUIRE(class_type.is_class()); + REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class)); + + // TODO(tkiley): Currently we do not support extracting information + // about the base classes generic information. + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp new file mode 100644 index 00000000000..35bf3a273a6 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp @@ -0,0 +1,66 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include + +#include +#include + +#include +#include + +SCENARIO( + "java_bytecode_parse_generic_array_class", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table= + load_java_class("GenericArray", "" + "./java_bytecode/java_bytecode_parse_generics"); + + std::string class_prefix="java::GenericArray"; + + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const struct_typet &type=to_struct_type( + new_symbol_table.lookup(class_prefix) + .value().get().type); + + THEN("There should be a component with name t") + { + REQUIRE(type.has_component("t")); + } + + const pointer_typet &t_component=to_pointer_type( + type.get_component("t") + .type()); + const symbol_typet &subtype=to_symbol_type(t_component.subtype()); + + THEN("The t component is a valid java array") + { + const struct_typet &subtype_type=to_struct_type( + new_symbol_table.lookup(subtype.get_identifier()) + .value().get().type); + REQUIRE(is_valid_java_array(subtype_type)); + } + + THEN("The elements of the t component have the parametric type T") + { + const typet &element=static_cast(subtype.find( + ID_C_element_type)); + REQUIRE(is_java_generic_parameter(element)); + + REQUIRE( + to_java_generic_parameter(element).type_variable().get_identifier()== + "java::GenericArray::T"); + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp new file mode 100644 index 00000000000..d14553d2599 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -0,0 +1,329 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include + +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_parse_generics", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table= + load_java_class("generics", "./java_bytecode/java_bytecode_parse_generics"); + + GIVEN("Some class files with Generics") + { + WHEN("Parsing a class with type variable") + { + REQUIRE(new_symbol_table.has_symbol("java::generics$element")); + THEN("The symbol type should be generic") + { + const symbolt &class_symbol= + new_symbol_table.lookup("java::generics$element").value().get(); + 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()); + java_class_typet java_class_type=to_java_class_type(class_type); + REQUIRE(is_java_generics_class_type(java_class_type)); + java_generics_class_typet java_generics_class_type= + to_java_generics_class_type(java_class_type); + + const struct_union_typet::componentt &elem= + java_generics_class_type.get_component("elem"); + const typet &elem_type=java_class_type.component_type("elem"); + + REQUIRE(is_java_generic_parameter(elem_type)); + + REQUIRE(java_generics_class_type.generic_types().size()==1); + THEN("Type variable is named 'E'") + { + typet &type_var=java_generics_class_type.generic_types().front(); + REQUIRE(is_java_generic_parameter(type_var)); + java_generic_parametert generic_type_var= + to_java_generic_parameter(type_var); + REQUIRE( + generic_type_var.type_variable().get_identifier()== + "java::generics$element::E"); + typet &sub_type=generic_type_var.subtype(); + REQUIRE(sub_type.id()==ID_symbol); + symbol_typet &bound_type=to_symbol_type(sub_type); + REQUIRE(bound_type.get_identifier()=="java::java.lang.Object"); + } + } + } + } + + GIVEN("Some class files with generic type variable") + { + WHEN("Parsing a class with bounded type variable") + { + REQUIRE(new_symbol_table.has_symbol("java::generics$bound_element")); + THEN("The symbol type should be generic") + { + const symbolt &class_symbol= + new_symbol_table.lookup("java::generics$bound_element").value().get(); + 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()); + java_class_typet java_class_type=to_java_class_type(class_type); + REQUIRE(is_java_generics_class_type(java_class_type)); + java_generics_class_typet java_generics_class_type= + to_java_generics_class_type(java_class_type); + REQUIRE(java_generics_class_type.generic_types().size()==1); + typet &type_var=java_generics_class_type.generic_types().front(); + REQUIRE(is_java_generic_parameter(type_var)); + java_generic_parametert generic_type_var= + to_java_generic_parameter(type_var); + + REQUIRE( + generic_type_var.type_variable().get_identifier()== + "java::generics$bound_element::NUM"); + REQUIRE( + java_generics_class_type_var(0, java_generics_class_type)== + "java::generics$bound_element::NUM"); + THEN("Bound must be Number") + { + typet &sub_type=generic_type_var.subtype(); + REQUIRE(sub_type.id()==ID_symbol); + symbol_typet &bound_type=to_symbol_type(sub_type); + REQUIRE(bound_type.get_identifier()=="java::java.lang.Number"); + REQUIRE( + to_symbol_type( + java_generics_class_type_bound(0, java_generics_class_type)) + .get_identifier()=="java::java.lang.Number"); + } + + const struct_union_typet::componentt &elem= + java_generics_class_type.get_component("elem"); + const typet &elem_type=java_class_type.component_type("elem"); + + REQUIRE(is_java_generic_parameter(elem_type)); + } + } + } + + GIVEN("Some class files with generic type variable") + { + WHEN("Parsing a class with bounded type variable") + { + REQUIRE(new_symbol_table.has_symbol("java::generics")); + + THEN("The generic fields should be annotated with concrete types") + { + const symbolt &class_symbol=new_symbol_table.lookup("java::generics") + .value().get(); + 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()); + java_class_typet java_class_type=to_java_class_type(class_type); + REQUIRE(!is_java_generics_class_type(java_class_type)); + + const struct_union_typet::componentt &belem= + java_class_type.get_component("belem"); + const typet &belem_type=java_class_type.component_type("belem"); + + REQUIRE(belem_type!=nil_typet()); + REQUIRE(is_java_generic_type(belem_type)); + THEN("Field has instantiated type variable") + { + const java_generic_typet &container= + to_java_generic_type(belem_type); + + const std::vector &generic_types= + container.generic_type_variables(); + REQUIRE(generic_types.size()==1); + + const typet& inst_type=java_generic_get_inst_type(0, container); + + REQUIRE(inst_type.id()==ID_pointer); + const typet &inst_type_symbol=inst_type.subtype(); + REQUIRE(inst_type_symbol.id()==ID_symbol); + REQUIRE( + to_symbol_type(inst_type_symbol).get_identifier()== + "java::java.lang.Integer"); + } + } + } + } + + GIVEN("Some class files with Generics") + { + WHEN("Methods with generic signatures") + { + REQUIRE( + new_symbol_table + .has_symbol("java::generics$bound_element.f:()Ljava/lang/Number;")); + +// TODO: methods should have generic return type (the tests needs to be +// extended), reintroduce when the issue of signature/descriptor for methods is +// resolved +// THEN("The method should have generic return type") +// { +// const symbolt &method_symbol= +// new_symbol_table +// .lookup("java::generics$bound_element.f:()Ljava/lang/Number;") +// .value().get(); +// const typet &symbol_type=method_symbol.type; +// +// REQUIRE(symbol_type.id()==ID_code); +// +// const code_typet &code=to_code_type(symbol_type); +// } + + REQUIRE( + new_symbol_table + .has_symbol("java::generics$bound_element.g:(Ljava/lang/Number;)V")); + +// TODO: methods are not recognized as generic, reintroduce when +// the issue of signature/descriptor for methods is resolved +// THEN("The method should have a generic parameter.") +// { +// const symbolt &method_symbol= +// new_symbol_table +// .lookup("java::generics$bound_element.g:(Ljava/lang/Number;)V"); +// const typet &symbol_type=method_symbol.type; +// +// REQUIRE(symbol_type.id()==ID_code); +// +// const code_typet &code=to_code_type(symbol_type); +// +// bool found=false; +// for(const auto &p : code.parameters()) +// { +// if(p.get_identifier()== +// "java::generics$bound_element.g:(Ljava/lang/Number;)V::e") +// { +// found=true; +// const typet &t=p.type(); +// REQUIRE(is_java_generic_parameter(p.type())); +// const java_generic_parametert &gen_type= +// to_java_generic_parameter(p.type()); +// const symbol_typet &type_var=gen_type.type_variable(); +// REQUIRE(type_var.get_identifier()== +// "java::generics$bound_element::NUM"); +// break; +// } +// } +// REQUIRE(found); +// } + } + } + GIVEN("A class with multiple bounds") + { + THEN("The bounds should be encoded") + { + REQUIRE( + new_symbol_table.has_symbol("java::generics$double_bound_element")); + THEN("The symbol should have a generic parameter") + { + const symbolt &class_symbol= + new_symbol_table.lookup("java::generics$double_bound_element") + .value().get(); + 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()); + java_class_typet java_class_type=to_java_class_type(class_type); + REQUIRE_FALSE(is_java_generics_class_type(java_class_type)); + + // TODO (tkiley): Extend this unit test when bounds are correctly + // parsed. +#if 0 + java_generics_class_typet java_generics_class_type= + to_java_generics_class_type(java_class_type); + REQUIRE(java_generics_class_type.generic_types().size()==1); + typet &type_var=java_generics_class_type.generic_types().front(); + REQUIRE(is_java_generic_parameter(type_var)); + java_generic_parametert generic_type_var= + to_java_generic_parameter(type_var); + + REQUIRE( + generic_type_var.type_variable().get_identifier()== + "java::generics$double_bound_element::T"); + REQUIRE( + java_generics_class_type_var(0, java_generics_class_type)== + "java::generics$double_bound_element::T"); + THEN("Bound must be Number and dummyInterface") + { + + } +#endif + } + } + } + GIVEN("A class with multiple generic parameters") + { + THEN("Both generic parameters should be encoded") + { + const symbolt &class_symbol= + new_symbol_table.lookup("java::generics$two_elements").value().get(); + 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()); + java_class_typet java_class_type=to_java_class_type(class_type); + REQUIRE(is_java_generics_class_type(java_class_type)); + + java_generics_class_typet java_generics_class_type= + to_java_generics_class_type(java_class_type); + REQUIRE(java_generics_class_type.generic_types().size()==2); + + auto generic_param_iterator= + java_generics_class_type.generic_types().cbegin(); + + // The first parameter should be called K + { + const typet &first_param=*generic_param_iterator; + REQUIRE(is_java_generic_parameter(first_param)); + java_generic_parametert generic_type_var= + to_java_generic_parameter(first_param); + + REQUIRE( + generic_type_var.type_variable().get_identifier()== + "java::generics$two_elements::K"); + REQUIRE( + java_generics_class_type_var(0, java_generics_class_type)== + "java::generics$two_elements::K"); + } + + ++generic_param_iterator; + + + // The second parameter should be called V + { + const typet &second_param=*generic_param_iterator; + REQUIRE(is_java_generic_parameter(second_param)); + java_generic_parametert generic_type_var= + to_java_generic_parameter(second_param); + + REQUIRE( + generic_type_var.type_variable().get_identifier()== + "java::generics$two_elements::V"); + REQUIRE( + java_generics_class_type_var(1, java_generics_class_type)== + "java::generics$two_elements::V"); + } + } + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp new file mode 100644 index 00000000000..2ce3d5b5c34 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp @@ -0,0 +1,75 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include + +#include + +#include +#include + +SCENARIO( + "java_bytecode_parse_generic_function", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table= + load_java_class( + "GenericFunctions", + "./java_bytecode/java_bytecode_parse_generics"); + + std::string class_prefix="java::GenericFunctions"; + THEN("There should be a symbol for processSimpleGeneric") + { + const std::string func_name=".processSimpleGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } + + THEN("There should be a symbol for processUpperBoundInterfaceGeneric") + { + const std::string func_name=".processUpperBoundInterfaceGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } + + THEN("There should be a symbol for processUpperBoundClassGeneric") + { + const std::string func_name=".processUpperBoundClassGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } + + THEN("There should be a symbol for processDoubleUpperBoundClassGeneric") + { + const std::string func_name=".processDoubleUpperBoundClassGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } + + THEN("There should be a symbol for processDoubleUpperBoundInterfaceGeneric") + { + const std::string func_name=".processDoubleUpperBoundInterfaceGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp new file mode 100644 index 00000000000..39d9329e2a9 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include + +#include + +#include +#include + +SCENARIO( + "java_bytecode_parse_generic_wildcard", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table= + load_java_class( + "WildcardGenericFunctions", + "./java_bytecode/java_bytecode_parse_generics"); + + std::string class_prefix="java::WildcardGenericFunctions"; + + THEN("There should be a symbol for processSimpleGeneric") + { + const std::string func_name=".processSimpleGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } + + THEN("There should be a symbol for processUpperBoundInterfaceGeneric") + { + const std::string func_name=".processUpperBoundInterfaceGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } + + THEN("There should be a symbol for processUpperBoundClassGeneric") + { + const std::string func_name=".processUpperBoundClassGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } + + THEN("There should be a symbol for processLowerBoundGeneric") + { + const std::string func_name=".processLowerBoundGeneric"; + const std::string func_descriptor=":(LSimpleGeneric;LFoo;)V"; + const std::string process_func_name=class_prefix+func_name+func_descriptor; + + REQUIRE(new_symbol_table.has_symbol(process_func_name)); + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp new file mode 100644 index 00000000000..21c190a88b8 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp @@ -0,0 +1,36 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include + +#include +#include + +#include +#include + +SCENARIO( + "java_bytecode_parse_recursive_generic_class", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table= + load_java_class("RecursiveGeneric", "" + "./java_bytecode/java_bytecode_parse_generics"); + + std::string class_prefix="java::RecursiveGeneric"; + + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + // TODO: Extend this unit test when recursive generic types are correctly + // parsed. +} diff --git a/unit/java_bytecode/java_utils_test.cpp b/unit/java_bytecode/java_utils_test.cpp new file mode 100644 index 00000000000..5f4ad25bb04 --- /dev/null +++ b/unit/java_bytecode/java_utils_test.cpp @@ -0,0 +1,65 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + + Note: Created by fotis on 09/10/2017. + +\*******************************************************************/ + +#include +#include + +#include + +#include + +SCENARIO("Test that the generic signature delimiter lookup works reliably", + "[core][java_util_test]") +{ + GIVEN("Given the signatures of some generic classes") + { + std::vector generic_sigs + { + // Valid inputs + "List", + "HashMap", + "List>", + "List>>", + // Invalid inputs + "<", + "List", + }; + + WHEN("We check if the closing tag is recognised correctly") + { + // TEST VALID CASES + + // List + REQUIRE(find_closing_delimiter(generic_sigs[0], 4, '<', '>')==12); + // HashMap + REQUIRE(find_closing_delimiter(generic_sigs[1], 7, '<', '>')==23); + // List> + REQUIRE(find_closing_delimiter(generic_sigs[2], 4, '<', '>')==14); + REQUIRE(find_closing_delimiter(generic_sigs[2], 9, '<', '>')==13); + // List>> + REQUIRE(find_closing_delimiter(generic_sigs[3], 14, '<', '>')==18); + + // TEST INVALID CASES + + // < + REQUIRE(find_closing_delimiter(generic_sigs[4], 0, '<', '>') + ==std::string::npos); + // List') + ==std::string::npos); + // List + // (make sure that we still recognise the first delimiter correctly) + REQUIRE(find_closing_delimiter(generic_sigs[6], 4, '<', '>') + ==std::string::npos); + REQUIRE(find_closing_delimiter(generic_sigs[6], 9, '<', '>')==17); + } + } +}