From 31faaa66e146df275126a591aff1b82bede3d186 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 21 Sep 2017 17:37:06 +0100 Subject: [PATCH 01/28] Revert "Revert "TG-374 Feature/java support generics"" This reverts commit 3b3fee34be5bdbd119f6cdb90b6bdfe6ba4ad4d0. --- regression/cbmc-java/enum1/test.desc | 4 +- regression/cbmc-java/iterator2/test.desc | 6 +- regression/cbmc-java/lvt-groovy/test.desc | 3 +- src/java_bytecode/ci_lazy_methods.cpp | 3 +- .../java_bytecode_convert_class.cpp | 65 ++++- .../java_bytecode_convert_method.cpp | 29 +- .../java_bytecode_parse_tree.cpp | 7 +- src/java_bytecode/java_bytecode_parse_tree.h | 13 +- src/java_bytecode/java_bytecode_parser.cpp | 112 ++++++- .../java_local_variable_table.cpp | 15 +- src/java_bytecode/java_types.cpp | 199 ++++++++++++- src/java_bytecode/java_types.h | 276 +++++++++++++++++- src/java_bytecode/java_utils.cpp | 48 +++ src/java_bytecode/java_utils.h | 6 + src/util/irep_ids.def | 6 + unit/Makefile | 1 + .../generics$bound_element.class | Bin 0 -> 892 bytes .../generics$element.class | Bin 0 -> 573 bytes .../generics.class | Bin 0 -> 1032 bytes .../generics.java | 31 ++ .../parse_generic_class.cpp | 240 +++++++++++++++ 21 files changed, 1015 insertions(+), 49 deletions(-) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics$bound_element.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics$element.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc index eff2c2e6817..51d41e272c3 100644 --- a/regression/cbmc-java/enum1/test.desc +++ b/regression/cbmc-java/enum1/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG enum1.class --java-unwind-enum-static --unwind 3 ^VERIFICATION SUCCESSFUL$ @@ -7,3 +7,5 @@ enum1.class ^Unwinding loop java::enum1.:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.:\(\)V bytecode-index 78 thread 0$ -- ^warning: ignoring +-- +cf. https://diffblue.atlassian.net/browse/TG-611 diff --git a/regression/cbmc-java/iterator2/test.desc b/regression/cbmc-java/iterator2/test.desc index 68525dd9b76..4f4f1490295 100644 --- a/regression/cbmc-java/iterator2/test.desc +++ b/regression/cbmc-java/iterator2/test.desc @@ -1,8 +1,10 @@ -CORE +KNOWNBUG iterator2.class ---cover location --unwind 3 --function iterator2.f +--cover location --unwind 3 --function iterator2.f ^EXIT=0$ ^SIGNAL=0$ ^.*SATISFIED$ -- ^warning: ignoring +-- +https://diffblue.atlassian.net/browse/TG-610 diff --git a/regression/cbmc-java/lvt-groovy/test.desc b/regression/cbmc-java/lvt-groovy/test.desc index 050fcd09c7e..7bbc58e4854 100644 --- a/regression/cbmc-java/lvt-groovy/test.desc +++ b/regression/cbmc-java/lvt-groovy/test.desc @@ -1,7 +1,8 @@ -CORE +KNOWNBUG DetectSplitPackagesTask.class --show-symbol-table ^EXIT=0$ ^SIGNAL=0$ -- -- +cf. https://diffblue.atlassian.net/browse/TG-610 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..237ee26ceac 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,25 @@ void java_bytecode_convert_classt::convert(const classt &c) } java_class_typet class_type; + if(c.signature.has_value()) + { + 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 + for(auto t : java_generic_type_from_string( + id2string(c.name), + c.signature.value())) + { + generic_class_type.generic_types() + .push_back(to_java_generic_parameter(t)); + } + + class_type=generic_class_type; + } class_type.set_tag(c.name); class_type.set(ID_base_name, c.name); @@ -166,7 +186,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 +207,48 @@ 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( + f.signature.value(), + 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..cdd06ec86f4 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,19 @@ 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; + 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)); + } + else + member_type=java_type_from_string(m.descriptor); method_symbol.name=method_identifier; method_symbol.base_name=m.base_name; @@ -317,7 +329,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 +362,16 @@ 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( + v.signature.value(), + 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..9bea073ff14 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,45 @@ 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( + field.signature.value(), + "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( + method.signature.value(), + "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( + var.signature.value(), + "java::"+id2string(parse_tree.parsed_class.name)); + } + else + var_type=java_type_from_string(var.descriptor); get_class_refs_rec(var_type); } } @@ -628,7 +655,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 +964,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 +972,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 +993,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 +1060,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 +1349,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 +1403,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 +1448,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,15 @@ 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; + if(v.var.signature.has_value()) + t=java_type_from_string(v.var.signature.value()); + else + 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..e7c45dfc800 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() { @@ -114,7 +119,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,11 +163,32 @@ 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: 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) { 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 '(': // function type @@ -174,7 +200,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); 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); if(param.type().id()==ID_symbol) param.type()=java_reference_type(param.type()); @@ -215,7 +259,7 @@ 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); if(subtype_letter=='L' || // [L denotes a reference array of some sort. subtype_letter=='[') // Array-of-arrays subtype_letter='A'; @@ -233,7 +277,16 @@ 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.empty()); + irep_idt type_var_name(class_name+"::"+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 ; @@ -241,6 +294,91 @@ typet java_type_from_string(const std::string &src) 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) + return nil_typet(); + + // 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 base_class + size_t signature_end=src.find('>'); + INVARIANT( + src[0]=='<' && signature_end!=std::string::npos, + "Class signature has unexpected format"); + std::string signature(src.substr(1, signature_end-1)); + + 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..15d4f0689b9 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -10,8 +10,11 @@ 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 class java_class_typet:public class_typet { @@ -66,8 +69,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=""); 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 +84,270 @@ 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> +/// +/// \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/generics$bound_element.class b/unit/java_bytecode/java_bytecode_parse_generics/generics$bound_element.class new file mode 100644 index 0000000000000000000000000000000000000000..8076c290e12a9de020c7afdf303b3f7c5adbd307 GIT binary patch literal 892 zcmZ`%U2oGs5S)u+yD?51LJ8%wKm#~IqCD^fQ6y9e2`Ln$mOk);ob(!8xejt1B>ojh zAS5360sJV$>|IhfDm>WU+nt@Ao%8QMKYsyuf=&%p+zH^~u0&ft?)kW{P}QkEQD_d1 z<4^H+8fW9}-Py@d=g$;sd&xM9i&?G}-2L6RubA_S56QIsSRojUb*A%VG?i>G$&#Y4 zP>;%V=YaG(lS6i|4U$Y--u-x(GSeJPMsa!&=ZT!>$*Pc(WH^~+hwnw1&I*O_WyVQ6 zX*`{3mN!mEw3mR?(OPEx{Bgm&`JbMiS*y=hb)>K!b^hgpA9d#2tFgl6=sZSNRorSN zGC(hs8 z6dL6%T5bg=5;ZG}4&3JLyZj|8e8>mZ%&FFB$Rx%NpAdCcRvEn^Qm{ey;diL+4^+My z%o^VwF(5~S@0La3BG!2#-muXw#-YIlthG$-3O0xq_UEh!hui%I=L-V|C2?SgZL>Qk zF6ksAbXNXVM%QqCPWz5uv!IA}O2L82)@i`%8PVRUXb(4xB{Ib>BsD8qYBh?r^KMe9 Ujc#F+=n9R!#BV@E6>T(uzpNdiDgXcg literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..34cb36e36b49a205496b9dd54785cf9216aaf601 GIT binary patch literal 573 zcmZWmO;5r=5PeH4g;Jze1;6FM0WlE|o|JGQn3yzb0^z>Y4K68*X^V+J%Y!lT;1BRe z8E27dl*8`Mym|BHV?RFM-T|DUnumdH8zy!v>{-}nFhwXP44yyckGvUjHEP}r$0A5B z81g+iQaqVOg2Cu_3CSk+GOnF6*#1Z;5y>FdXiF-Yv>A%^U-)Q1;+^Ro<(7P@#Pw`4 z6j7fKLqa@%8t`zyBdPrbXlii=OLrtx!r)vfs?iB~9199~KjO6og=&}oDm^`pb4G+dhaGk$|6 zB{h;5pZxo));RKkcNtK(i6KIFnMkT+-*bQHq~ zB4@zFeH{-J^UxsjNJmM>V}WR+GjR4_%eFj}PG7*RI*#maw5?uG_5^f~2sD%_kf^mJ zJ?v&LbuP3lVASoFWAz7JDUiRwtx`L%j;&(ba$3cz)0ZvTEw3>)Sg{?uzb4>MXLbd& zjm|!^%+zd0ZVwI{vir(vw28!Oou<{^wYs+Yo`PEcolUV}uO<_Uw*v8WHS?c(Bpt3Q z*Epls(6m`b`x<28=WBg9a_g;lg;LXyi`t6T`&RS)mUT2%$_wI+P-wj~=r-j`TXht5 z%NNvSOe`QSFzbSD0fj#?@f1rYR`HDDJdbnNU}6q2fw_OCtP(s|vFtA7#?O4~rw9)bNq$5mcY?ro7@zVdh^UjfG^qNw5#qkUUnfra zi>#f%GS!r5ty0H2H7IS_NqtY-Ca&WK)fsq!n;e3VOo7>A@Z%2s<3uK0%H!tA-6a=+ e_=R;H%Q{v_rV06w!3@tBtsn<+X^fee1^xi|W7(tt literal 0 HcmV?d00001 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..0a0af41c63a --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/generics.java @@ -0,0 +1,31 @@ +public class generics { + + 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; + } +} 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..fc0f46bbb73 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -0,0 +1,240 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include + +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_parse_generics", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + std::unique_ptrjava_lang(new_java_bytecode_language()); + + // Configure the path loading + cmdlinet command_line; + command_line.set( + "java-cp-include-files", + "./java_bytecode/java_bytecode_parse_generics"); + config.java.classpath.push_back( + "./java_bytecode/java_bytecode_parse_generics"); + + std::istringstream java_code_stream("ignored"); + null_message_handlert message_handler; + + // Configure the language, load the class files + java_lang->get_language_options(command_line); + java_lang->set_message_handler(message_handler); + java_lang->parse(java_code_stream, "generics.class"); + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + java_lang->final(new_symbol_table); + + 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"); + 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"); + 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"); + 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;")); + + THEN("The method should have generic return type") + { + const symbolt &method_symbol= + new_symbol_table + .lookup("java::generics$bound_element.f:()Ljava/lang/Number;"); + 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")); + + 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); + } + } + } +} From b2f57e84f6efb7ede7487f7d1beeabadea428d31 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 22 Sep 2017 09:52:14 +0100 Subject: [PATCH 02/28] Fixing handling the case of * --- src/java_bytecode/java_types.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index e7c45dfc800..a2181ac66ad 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -389,6 +389,20 @@ typet java_type_from_string( return java_reference_type(symbol_type); } + case '*': + { + // parse name of type variable + INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); + PRECONDITION(!class_name.empty()); +// INVARIANT( +// src.substr(1, src.size()-2)=="*", +// "Wildcard types do not have a name"); + irep_idt type_var_name(class_name+"::*"); + return java_generic_parametert( + type_var_name, + java_type_from_string("Ljava/lang/Object;").subtype()); + } + default: return nil_typet(); From 1bd95c009841c38911dd9cbcda9877859b5b8afc Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 25 Sep 2017 13:26:30 +0100 Subject: [PATCH 03/28] Classes that aren't generic but inherit from a generic type have a signature This is a lazy fix to stop trying to create java_generics_class_typet when the signature doesn't have the correct format --- src/java_bytecode/java_bytecode_convert_class.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 237ee26ceac..8d4d1a00659 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -94,7 +94,7 @@ void java_bytecode_convert_classt::convert(const classt &c) } java_class_typet class_type; - if(c.signature.has_value()) + if(c.signature.has_value() && c.signature.value()[0]=='<') { java_generics_class_typet generic_class_type; #ifdef DEBUG From b59c65925bbd7c4e68e06b0505d9823dc036d33a Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 25 Sep 2017 13:27:35 +0100 Subject: [PATCH 04/28] When dealing with generic arrays we should treat them like ref arrays too For some reason, A indicates a reference array --- src/java_bytecode/java_types.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index a2181ac66ad..5b74c1ba52b 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -261,7 +261,8 @@ typet java_type_from_string( const typet subtype= java_type_from_string(src.substr(1, std::string::npos), class_name); 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); From a60ead480c6faf0bb1dcbf6361982d506c088485 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 25 Sep 2017 13:30:18 +0100 Subject: [PATCH 05/28] Correctly handle nested generic types Previously looked for first > and ;, but in nested types we need to find the last semi-colon and the matching angle bracket. --- src/java_bytecode/java_types.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 5b74c1ba52b..9992cd4c843 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -454,7 +454,7 @@ std::vector java_generic_type_from_string( const std::string &src) { /// the class signature is of the form base_class - size_t signature_end=src.find('>'); + size_t signature_end=find_closing_delimiter(src, 0, '<', '>'); INVARIANT( src[0]=='<' && signature_end!=std::string::npos, "Class signature has unexpected format"); @@ -463,7 +463,7 @@ std::vector java_generic_type_from_string( PRECONDITION(signature[signature.size()-1]==';'); std::vector types; - size_t var_sep=signature.find(';'); + size_t var_sep=signature.rfind(';'); while(var_sep!=std::string::npos) { size_t bound_sep=signature.find(':'); From 79f743bc337964df84874b2950ef76867fdaf7cf Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 25 Sep 2017 13:31:05 +0100 Subject: [PATCH 06/28] Adding conversions for wild cards Need to check all these are actually required after the other fixes --- src/java_bytecode/java_types.cpp | 35 ++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 9992cd4c843..dacbc6006d0 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -392,6 +392,41 @@ typet java_type_from_string( } case '*': { +#ifdef DEBUG + std::cout << class_name << std::endl; +#endif + // parse name of type variable + INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); + PRECONDITION(!class_name.empty()); +// INVARIANT( +// src.substr(1, src.size()-2)=="*", +// "Wildcard types do not have a name"); + irep_idt type_var_name(class_name+"::*"); + return java_generic_parametert( + type_var_name, + java_type_from_string("Ljava/lang/Object;").subtype()); + } + case '+': + { +#ifdef DEBUG + std::cout << class_name << std::endl; +#endif + // parse name of type variable + INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); + PRECONDITION(!class_name.empty()); +// INVARIANT( +// src.substr(1, src.size()-2)=="*", +// "Wildcard types do not have a name"); + irep_idt type_var_name(class_name+"::*"); + return java_generic_parametert( + type_var_name, + java_type_from_string("Ljava/lang/Object;").subtype()); + } + case '-': + { +#ifdef DEBUG + std::cout << class_name << std::endl; +#endif // parse name of type variable INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); PRECONDITION(!class_name.empty()); From 2f7f6957e6d2da47c0080751efc7a3d4bb063184 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 25 Sep 2017 13:31:24 +0100 Subject: [PATCH 07/28] Adding some useful debug info --- src/java_bytecode/java_types.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index dacbc6006d0..ff6d0bdb473 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -97,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+"]"; From 7320c466753a2dbcc238ac5d0fdc970aef922cc0 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 25 Sep 2017 13:31:36 +0100 Subject: [PATCH 08/28] Correcting a typo --- src/java_bytecode/java_types.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index ff6d0bdb473..e8f4edebf2e 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -357,7 +357,7 @@ typet java_type_from_string( #ifdef DEBUG std::cout << " generic type var " << gen_type.id() << " bound " << to_symbol_type(gen_type.subtype()).get_identifier() - << "\n2"; + << "\n"; #endif result.generic_type_variables().push_back(gen_type); } From 35cd16053ee4396d98cbedf55db30b573c6651d6 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 25 Sep 2017 16:51:42 +0100 Subject: [PATCH 09/28] Deal with generic methods The signature of a method can start with an angle bracket if it is a generic method on a non-generic type or a static generic method. Previously this would cause us to return a nil type rather than a code type. This information is currently ignored and instead we just skip over the Formal Type parameters and proceed using normal type evaluation. --- .../java_bytecode_convert_method.cpp | 1 + src/java_bytecode/java_types.cpp | 20 +++++++++++++++++++ 2 files changed, 21 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index cdd06ec86f4..7e0f09fcf47 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -273,6 +273,7 @@ void java_bytecode_convert_method_lazy( 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); diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index e8f4edebf2e..b6b8d6aef39 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -195,6 +195,26 @@ typet java_type_from_string( // - 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 + size_t closing_generic=find_closing_delimiter(src, 0, '<', '>'); + const typet &method_type=java_type_from_string( + src.substr(closing_generic+1, std::string::npos), class_name); + + // 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(')'); From a2344f830d1b8bfb585c8befca47a385b823ba5e Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 27 Sep 2017 15:06:38 +0100 Subject: [PATCH 10/28] Extending the tests for the generic class --- .../generics$bound_element.class | Bin 892 -> 892 bytes .../generics$double_bound_element.class | Bin 0 -> 705 bytes .../generics$dummyInterface.class | Bin 0 -> 195 bytes .../generics$element.class | Bin 573 -> 573 bytes .../generics$two_elements.class | Bin 0 -> 639 bytes .../generics.class | Bin 1032 -> 1202 bytes .../generics.java | 28 ++++++ .../parse_generic_class.cpp | 95 ++++++++++++++++++ 8 files changed, 123 insertions(+) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics$double_bound_element.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics$dummyInterface.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics$two_elements.class 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 index 8076c290e12a9de020c7afdf303b3f7c5adbd307..ef168d8e34c9af903d9a9ac61f16be5f379ea561 100644 GIT binary patch delta 29 lcmeyv_J?gl3KJvGGn8I0k8CV(kCQC6V0RV>_2VnpJ 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 0000000000000000000000000000000000000000..af550821f2ac6e23893bc73f3f464b0781dc0bc4 GIT binary patch literal 705 zcmaJbd(sP!WBb?Tx-A|_>s$H|L8It z_Jm(!NZdGm$%D`r3|hNQNG!N>MwMd*qtzEu_>MJFXx))c&|pYcr|@2f#LqpOaQw$ut>oUX?Y|)MM3IIJ?J66{BRk&5 sESOlLi1=eQnk)HAOCcs!$ZFpeSFuJ>1nbC=&5@^}h(+@AWDBwQCrLx9mjD0& literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..20f3e82c81bf8d6853c8693c2e366a323f3bfc78 GIT binary patch literal 195 zcmZ8bF%E)I6zfCeBZ6`B0uH*!;tfnpm>gVOzn>?8z&GK8iC1&*03OQtG+}XRo2G60 zdOw~3wn!90g(<-=xH}O>t93?*j@Q05yf14eBn4Y;OXD_`zG;P+uo$dm-Z#xXvmLh= zZ6rMVH{#4ndsl1c*b(O6jkMObNDt?VO-Bfau>c@=a!c5kEAT~m82>OpBpgYCpfCx- E4-Ba+!vFvP literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics$element.class b/unit/java_bytecode/java_bytecode_parse_generics/generics$element.class index 34cb36e36b49a205496b9dd54785cf9216aaf601..f1c63b72ddea8d7f270b013401c831b6dcb304c0 100644 GIT binary patch delta 13 UcmdnXvX^DU8%9Qs$!{4003}BR`Tzg` delta 13 UcmdnXvX^DU8%9Rv$!{4003|L2^#A|> 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 0000000000000000000000000000000000000000..4bbc9b11c6218b44d70098360ca722698cacafe1 GIT binary patch literal 639 zcmZuu%T5A85UgR5$GQljfQkwl4v2|(@T7zbiHU)z352UzaDt1=VwMHtXL&Ft9{d15 z%2yXNEb?H#}g_QTMS*5Su?5W7KS1jM~Syw){GX3;jCPVuVMm2K}# zAY8XPj_D0uDWEl~WW-2iO=bb_&Kl&71@u}+I?}b;1I3ms$MVVok^C=x&=l}j`nRkS ztyzw|9QIn$ZI~^aOuW`_n|9N5ErlnfUlkWHyvP2Hv}I2^o`M$+AF9~qU?2%oKQH8F zb?hQJU-Ri#>-6ldRy1V1;{> z*)_F3?t0HvbCRI!h*!Y5Ac&D z#F;^bSlsV?-}%n>xcA-$@AaFP_ort7^Vkca4$~4dA!wKlLC2g{gaBrB7+928 z@-oXhnH7mui8YCJ0i$$PNUNO6E4$<{+_!C2+{syvqa2A1ftF06e3Db?lS0|fd@BX& zVt)wv)kI=bpgvR1=dbtek}95Ar|Rw^C8}q*kNY5cha>0~Xv``OIzM%WzUmA_kT8(M zpn)xHyRRbB-;NG}@P&10#dDUOje8BVs_02~Jk_qdsP!GRR$BeOOSHoOe}(p+{I6}@ zLoI#8(Gck518eBw5uDjg8zmDb3Sy1<2yy32dT0YaDbP#b_!OWI{fvMC43deude!lb zryW3$c9=ghf-puoVvOE6f78S=Vtj^4zmJJ(>Qa?HDGaenur5LUsK4A4YdcWIYM_nG zXU?qTx|oYGR}1lmq)cE!vb%;UavCqwNHkG{dT!l7KTK>Q28hkR#y|_Pm2q1j_yLo> BZr=a^ delta 471 zcmX|-%TB^T7=_Q2ODPrwgmM!B<)VO~f{JLOi5p0K0T*hDHbjFpp~#l4`!0P7UAoY{ zPvR4}(|C%8#r!>U&iDT_(--B@H~IK^eFMhC)@7QTM}(ssa_8 zGPay#TcOjC(Uh?x5a``MnAexaz_>Hak$~DYO=Ea6&@Icb1ms!Z={Zs$e%d!k++11t z=l6ziS9pf~B{GF5G=bnO{BKkd#jc7yq*b)AZ?~mXE`+c^=vE)=^?`2o>s@nX^o^l| zwjJug9!pvKQ#wzOguo)-C?Ucnh-j=a`@*G_;`F`Tfh)nPPPGR~q__i?ke;$nuCs~5 zuE56{0lWdPEv4$EONX@5;aZ>!-Z9n8lAr^ mKg%M_3e4spzHuyb$U_&?+T diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics.java b/unit/java_bytecode/java_bytecode_parse_generics/generics.java index 0a0af41c63a..b2e18689158 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/generics.java +++ b/unit/java_bytecode/java_bytecode_parse_generics/generics.java @@ -1,5 +1,10 @@ public class generics { + interface dummyInterface + { + int getX(); + } + class element { E elem; } @@ -14,6 +19,29 @@ void g(NUM 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) { 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 index fc0f46bbb73..5484d3b79d5 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -237,4 +237,99 @@ SCENARIO( } } } + 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"); + 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$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") + { + // TODO (tkiley): Extend this unit test when bounds are correctly + // parsed. + } + } + } + } + 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"); + 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(0, java_generics_class_type)== + "java::generics$two_elements::V"); + } + } + } } From 33afe481921e9391867c5279b0a1f52ece92105b Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 27 Sep 2017 15:07:25 +0100 Subject: [PATCH 11/28] Adding unit tests for parsing wild card functions --- .../java_bytecode_parse_generics/Bar.class | Bin 0 -> 242 bytes .../BasicInterface.class | Bin 0 -> 140 bytes .../java_bytecode_parse_generics/Foo.class | Bin 0 -> 377 bytes .../SimpleGeneric.class | Bin 0 -> 451 bytes .../WildcardGenericFunctions.class | Bin 0 -> 2131 bytes .../WildcardGenericFunctions.java | 76 ++++++++++++++++ .../parse_generic_wildcard_function.cpp | 84 ++++++++++++++++++ 7 files changed, 160 insertions(+) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/Bar.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/Foo.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.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 0000000000000000000000000000000000000000..514dd58177aa495664e1a72f136fec3311a6e8f3 GIT binary patch literal 242 zcmXX=J#WH541I=tl#mkC9jPNQz`{n=p-AZxb)ka!xSWJhxRZ{A|HV|PLw`Vj6vCmk z;=vVyJoXpTGMKh>@h<*9I5 zRU75G?f=D~-t&nN7H`Tg3CY?uUYnd-!)VJ@sg*C^jWwQi-dJ6;v!~fXomGkep&S*X vVD22A(UHH}AW4}@jfBmmwn{kt0$qf35DP|kF~fuK^lt$@B+?Q3_pS5>xvnh3 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..aec76f72c2de16b6e40026abb64234d9b78096f4 GIT binary patch literal 140 zcmX^0Z`VEs1_l!bPId-%b_Nbc2A1^Hk_biyW(`eGMh33n{L-T2RJY8WR7M8b@XVZ) z2A!y{yEtL`DWar^MpSWY4^k)S|S+WS|BCkhp$MVqUtw he^ORzatRv)10w?y&^{o|0FMBm-3njy$DV~)r?m+rPpqTu+-G*-w=weFo8 zRh5F<@?2_ZmB<<`oHDvTT<}MpUM(~9ePdRZ)_a16s!UMn%xPTD&z zBzCEg5Bi*jY9OMr9t}kik7-N03lJQ53m-p_@=jZeL`u_L?aD@{G21YiHZHyV1X7Iu#f8o=dtHty&S&CHOF!Un1P+V7~ zU@+pC6w8-N>VW9ve9mCr6&alkLaD?-LLDv8>6<>rwjr4Cw_drn>W~%7@Vl6%2do`o$B;S=2^%b<2dI)ug&@J^^>0Z2py%8|5Pu1Fr a9$doiuK|4=5F50VA+b&~`Viih9sK~TKxAV8 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..c6e7ae228e78146807a344ef6b11d94c2722b2aa GIT binary patch literal 2131 zcmaKt?N=H{6vm$cWC7PGn4ppnHO5pyW81Xp3&i+JYQ!Wh(M0=lx-J{t6j{2vw9UWb zmwxQ$zQoviPTSA;1&?C* z6rU+52@GD>9LKO-)2ccvrlajvjIw~(5eVnas_D)P1gECA1VYPJ*%0V2npNXL{b1Ly zA4{=7qG;(_WlOV7+4qehci(gbQpG1`rL1dq`JPcVY*R1PtGdU^30$n%mTovs$vmi4 z3|~NhQ^ht*PSV8>65VbWNVcP2)K2k2}z6TeQCS<7j#8n3pTcX>wASV5Uf*$1@3Z!e>3Z3~#iJh~ zPmk5AZCf@2Z!ZcJPqEFj#azqEJbMIGT*HKl>)26|#RNqRNX1QQdQ9wBBwQS7vH@508nb*;kF%0tjKJk6URv}d?ay?bDdZus=KWL|ahB$f@w zw2g8zYMwQ>PM^Fyb}-IsXP9@J7#NlrV@rXM3FLp8y*a)G-#wXE5I?gKz*YW-J>w8Y z*;X3@jL{i*!!bov$;mq3a&qby1P+nR{Dz=7Lg)~^C+OLJh45d}W61LuqZR~@5Z&^c zVy-7?zrm-$k(RgEo8l9M7{N3f0b~f~j`-kxA3W-TFH7*>P<}^5K>6`}`WRO-euh5U zMVFSD7X7MEpCz3|;M1S^^t4AGY0#rbi2WaXl5yWS!%laxrDd+gzT&grCY!bAvmfy- z6B*8AUm_^e8$6TV8Gff`JxH>l@*#3VZ}Iyk&Lld_vG+N@k>A^-e9)|lH}o3hn0A6* z?xVV%5u{~~(U&t#KvyhJ}o27GBTdxAI>2`aLlB2L9%_81p^#m0>9;~1A( z0o+C(fjLBwXX_5Xn|HaK1=hkMH-4GRU%@<9v4#RR_`iw!_!{e8uwz_o1l#z~tEF4q zs*l(b)TsEFt$-JHOO+$3p~^Q^cc_YxaC$Igvg9wGNFHJ65K8DLgo3{!(0xc`srDeC NF36*Fmz@9>{srypx<>#2 literal 0 HcmV?d00001 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..cf7da93fbe5 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.java @@ -0,0 +1,76 @@ +interface BasicInterface +{ + int getX(); +} + +class Foo implements BasicInterface +{ + public int x; + + public int getX() { + return x; + } +} + +class Bar extends Foo +{} + +class SimpleGeneric +{ + public T t; +} + +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()); + } +} \ No newline at end of file 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..88b6c8c674a --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp @@ -0,0 +1,84 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include + +#include + +#include + +SCENARIO( + "java_bytecode_parse_generic_wildcard", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + std::unique_ptrjava_lang(new_java_bytecode_language()); + + // Configure the path loading + cmdlinet command_line; + command_line.set( + "java-cp-include-files", + "./java_bytecode/java_bytecode_parse_generics"); + config.java.classpath.push_back( + "./java_bytecode/java_bytecode_parse_generics"); + + std::istringstream java_code_stream("ignored"); + null_message_handlert message_handler; + + java_lang->get_language_options(command_line); + java_lang->set_message_handler(message_handler); + java_lang->parse(java_code_stream, "WildcardGenericFunctions.class"); + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + java_lang->final(new_symbol_table); + + std::string class_prefix="java::WildcardGenericFunctions"; + + // Validate loaded the java file + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + 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)); + } +} From 1dd221d378bbf6b8088460bec0a2cba11ad33b92 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 28 Sep 2017 17:11:21 +0100 Subject: [PATCH 12/28] Correct handling of the java generic class signature Previously the signature parsing would be confused into thinking that there were two generic parameters when there were two bounds on the first parameter. There exists TG-674 to make the conversion work correctly. --- .../java_bytecode_convert_class.cpp | 22 +++++++++++++------ src/java_bytecode/java_types.cpp | 7 ++++-- src/java_bytecode/java_types.h | 12 ++++++++++ .../parse_generic_class.cpp | 13 ++++++----- 4 files changed, 40 insertions(+), 14 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 8d4d1a00659..3231c347182 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -103,15 +103,23 @@ void java_bytecode_convert_classt::convert(const classt &c) << " in parsed class " << c.name << "\n"; #endif - for(auto t : java_generic_type_from_string( - id2string(c.name), - c.signature.value())) + try { - generic_class_type.generic_types() - .push_back(to_java_generic_parameter(t)); + 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_siganture_exceptiont) + { + // Do nothing: we don't support parsing for example double bounded or + // two entry elements } - - class_type=generic_class_type; } class_type.set_tag(c.name); diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index b6b8d6aef39..09f12d4d3fd 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -512,17 +512,20 @@ std::vector java_generic_type_from_string( const std::string &class_name, const std::string &src) { - /// the class signature is of the form base_class + /// 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_siganture_exceptiont(); + PRECONDITION(signature[signature.size()-1]==';'); std::vector types; - size_t var_sep=signature.rfind(';'); + size_t var_sep=signature.find(';'); while(var_sep!=std::string::npos) { size_t bound_sep=signature.find(':'); diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 15d4f0689b9..6ea659a773d 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -350,4 +350,16 @@ inline const typet &java_generics_class_type_bound( return gen_type.subtype(); } + +/// An exception that is raised for unsupported class signature. +/// Currently we do not parse multiple bounds. +class unsupported_java_class_siganture_exceptiont:public std::logic_error +{ +public: + unsupported_java_class_siganture_exceptiont(): + std::logic_error( + "Unsupported class signature: multiple bounds") + {} +}; + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H 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 index 5484d3b79d5..8bf81fa8c4c 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -253,8 +253,11 @@ SCENARIO( 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)); + 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); @@ -271,9 +274,9 @@ SCENARIO( "java::generics$double_bound_element::T"); THEN("Bound must be Number and dummyInterface") { - // TODO (tkiley): Extend this unit test when bounds are correctly - // parsed. + } +#endif } } } @@ -293,7 +296,7 @@ SCENARIO( 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); + REQUIRE(java_generics_class_type.generic_types().size()==2); auto generic_param_iterator= java_generics_class_type.generic_types().cbegin(); @@ -327,7 +330,7 @@ SCENARIO( generic_type_var.type_variable().get_identifier()== "java::generics$two_elements::V"); REQUIRE( - java_generics_class_type_var(0, java_generics_class_type)== + java_generics_class_type_var(1, java_generics_class_type)== "java::generics$two_elements::V"); } } From 8c7f4e44698ca40891a4ad054693c1c7f3f53a0f Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 28 Sep 2017 18:08:03 +0100 Subject: [PATCH 13/28] Adding unit test for java class that inherits from a generic class --- .../DerivedGeneric.class | Bin 0 -> 309 bytes .../DerivedGeneric.java | 4 ++ .../parse_derived_generic_class.cpp | 63 ++++++++++++++++++ 3 files changed, 67 insertions(+) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGeneric.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp 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 0000000000000000000000000000000000000000..65bdd950e8564a6fa2082c0a0b4ee4a7147f331d GIT binary patch literal 309 zcmY*UyKcfj5S#^L2gf`@Bx*{MA~fkhG>M=&(Kw<%%n245AG+B5SE@)U@&SAl%G#mv zNxL&Qvk&d%`tu9m6@w5>^aAt)JP`aDXPnOo&GFNk;Jw+cA@meyW>p+F#(n5bD#}3F zM5k-*xcuKlFW>Vgp|9SJ!n+TRl>-ih>C8U8svR{dWJK@oP Q0on*F|Gvr*Iu&;R0QdSqPyhe` literal 0 HcmV?d00001 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/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp new file mode 100644 index 00000000000..e736c61714f --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -0,0 +1,63 @@ +/*******************************************************************\ + + 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_derived_generic_class", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + std::unique_ptr java_lang(new_java_bytecode_language()); + + // Configure the path loading + cmdlinet command_line; + command_line.set( + "java-cp-include-files", + "./java_bytecode/java_bytecode_parse_generics"); + config.java.classpath.push_back( + "./java_bytecode/java_bytecode_parse_generics"); + + std::istringstream java_code_stream("ignored"); + null_message_handlert message_handler; + + // Configure the language, load the class files + java_lang->get_language_options(command_line); + java_lang->set_message_handler(message_handler); + java_lang->parse(java_code_stream, "DerivedGeneric.class"); + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + java_lang->final(new_symbol_table); + + 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); + 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)); + + std::cout << class_type.pretty() << std::endl; + + // TODO(tkiley): Currently we do not support extracting information + // about the base classes generic information. + } +} From 85c157457cbd3023beff6f7552a67c4457bfae78 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 29 Sep 2017 14:28:05 +0100 Subject: [PATCH 14/28] Applied use of utility function for loading a class file --- .../parse_derived_generic_class.cpp | 27 ++++--------------- .../parse_generic_class.cpp | 23 +++------------- .../parse_generic_wildcard_function.cpp | 27 ++++--------------- 3 files changed, 13 insertions(+), 64 deletions(-) diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index e736c61714f..94dc166b0c0 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -16,31 +16,16 @@ #include #include #include +#include SCENARIO( "java_bytecode_parse_derived_generic_class", "[core][java_bytecode][java_bytecode_parse_generics]") { - std::unique_ptr java_lang(new_java_bytecode_language()); - - // Configure the path loading - cmdlinet command_line; - command_line.set( - "java-cp-include-files", - "./java_bytecode/java_bytecode_parse_generics"); - config.java.classpath.push_back( - "./java_bytecode/java_bytecode_parse_generics"); - - std::istringstream java_code_stream("ignored"); - null_message_handlert message_handler; - - // Configure the language, load the class files - java_lang->get_language_options(command_line); - java_lang->set_message_handler(message_handler); - java_lang->parse(java_code_stream, "DerivedGeneric.class"); - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); - java_lang->final(new_symbol_table); + 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") { @@ -55,8 +40,6 @@ SCENARIO( REQUIRE(class_type.is_class()); REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class)); - std::cout << class_type.pretty() << std::endl; - // 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_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp index 8bf81fa8c4c..980a920bc4a 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -15,31 +15,14 @@ #include #include #include +#include SCENARIO( "java_bytecode_parse_generics", "[core][java_bytecode][java_bytecode_parse_generics]") { - std::unique_ptrjava_lang(new_java_bytecode_language()); - - // Configure the path loading - cmdlinet command_line; - command_line.set( - "java-cp-include-files", - "./java_bytecode/java_bytecode_parse_generics"); - config.java.classpath.push_back( - "./java_bytecode/java_bytecode_parse_generics"); - - std::istringstream java_code_stream("ignored"); - null_message_handlert message_handler; - - // Configure the language, load the class files - java_lang->get_language_options(command_line); - java_lang->set_message_handler(message_handler); - java_lang->parse(java_code_stream, "generics.class"); - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); - java_lang->final(new_symbol_table); + const symbol_tablet &new_symbol_table= + load_java_class("generics", "./java_bytecode/java_bytecode_parse_generics"); GIVEN("Some class files with Generics") { 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 index 88b6c8c674a..39d9329e2a9 100644 --- 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 @@ -16,36 +16,19 @@ #include #include +#include SCENARIO( "java_bytecode_parse_generic_wildcard", "[core][java_bytecode][java_bytecode_parse_generics]") { - std::unique_ptrjava_lang(new_java_bytecode_language()); - - // Configure the path loading - cmdlinet command_line; - command_line.set( - "java-cp-include-files", - "./java_bytecode/java_bytecode_parse_generics"); - config.java.classpath.push_back( - "./java_bytecode/java_bytecode_parse_generics"); - - std::istringstream java_code_stream("ignored"); - null_message_handlert message_handler; - - java_lang->get_language_options(command_line); - java_lang->set_message_handler(message_handler); - java_lang->parse(java_code_stream, "WildcardGenericFunctions.class"); - symbol_tablet new_symbol_table; - java_lang->typecheck(new_symbol_table, ""); - java_lang->final(new_symbol_table); + const symbol_tablet &new_symbol_table= + load_java_class( + "WildcardGenericFunctions", + "./java_bytecode/java_bytecode_parse_generics"); std::string class_prefix="java::WildcardGenericFunctions"; - // Validate loaded the java file - REQUIRE(new_symbol_table.has_symbol(class_prefix)); - THEN("There should be a symbol for processSimpleGeneric") { const std::string func_name=".processSimpleGeneric"; From de5c040f04269ca8ac51c559eb5690a452a3bec6 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 29 Sep 2017 17:35:26 +0100 Subject: [PATCH 15/28] Adding tests for generic functions --- .../BasicInterfaceCopy.class | Bin 0 -> 138 bytes .../BasicInterfaceCopy.java | 4 + .../GenericFunctions.class | Bin 0 -> 1791 bytes .../GenericFunctions.java | 26 ++++++ .../parse_generic_functions.cpp | 75 ++++++++++++++++++ 5 files changed, 105 insertions(+) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/BasicInterfaceCopy.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp 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 0000000000000000000000000000000000000000..c61caf0740a0fecd636a23e0b54ee6529d7fbefb GIT binary patch literal 138 zcmX^0Z`VEs1_l!bPId-%b_Nbc2A1^Hk_biyW(`eGMh33n{L-T2RJY8WR7M7Ir^MpS zWY4^k)S|S+QunW_&|MtN~U8X!=TPLewERe15y zXD=7xx6*XXqZ4ElV|R&Csn?&62kZYMy~@F|=khU9%S$ zTE-_f8T>0oUS;UWYP$NYbhxdWIqu95$r_4W*py9;uU(_x-qS3;_e9lIQ&ZMTy5ca> z4AG)#D5_;`Xotmu>N=3`c(%rp=2Z5UBWvvpv0CI&@d6vIb;OTZ`iVO@Ki3k z*#$SWU0t?ICZ#`}$<1f?UF%*%cTotKQ>LnWC+)GL_!7+N#1m_q`ulco+d+QJypPhghyDUtqP_r8LqNgK{K0Q zfO;Qlo{NTpw$39Enqzuq=^qh1WkI-Jr_FY zK>IlK9Ia;%7=(A1(}NUMtfCJ#(7C0GKH$=ai9X`dcU*eHq4$>QZ6^peV~456jw*Jd zfz2&d?0%O$O6+U@$L=O}^k3N5i9P1A58S$kow^6yQ$L4zhEVf^k2}4q2x+*Xcy6gG vKIs-ePJf{ZPpET_(txgrbb|I{2>$o*w|s)HQM6n>0r;dvF6~K2LN|T`0nl!( literal 0 HcmV?d00001 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..8673d2ee530 --- /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); + } +} \ No newline at end of file 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)); + } +} From e8c75ac60d66cba9e90ae98dfc5343806c77a318 Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 2 Oct 2017 11:33:52 +0100 Subject: [PATCH 16/28] Adding unit test for generic array --- .../GenericArray.class | Bin 0 -> 364 bytes .../GenericArray.java | 24 +++++++ .../parse_generic_array_class.cpp | 66 ++++++++++++++++++ 3 files changed, 90 insertions(+) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericArray.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp 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 0000000000000000000000000000000000000000..42dcdf0fee94533db44e9f0e50662719f9f4f13e GIT binary patch literal 364 zcmZWkO-sW-5Pg%{#MWp(^(J_%9_+#jK+!{kmz*|n30vwGmPF{!@+5fh2l%6; zFY!|BVQ1#OxASJ^=lAOyzzxpYXkZXv7~oVOg`@5mN9*RIkGH7|(-{?u4g%mj_mC-Di +{ + public T [] t; + public Integer [] Ia; + public int [] ia; +} + 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..08feff8716c --- /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) + .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()) + .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"); + } +} From 2f7925d9fd17e85977c571b38b34f9942f0d428c Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 2 Oct 2017 14:32:54 +0100 Subject: [PATCH 17/28] Adding unit test for recursive generic class --- .../java_bytecode_convert_class.cpp | 6 ++- .../java_bytecode_convert_method.cpp | 5 ++- src/java_bytecode/java_bytecode_parser.cpp | 15 +++++--- .../java_local_variable_table.cpp | 11 +++++- src/java_bytecode/java_types.cpp | 5 ++- src/java_bytecode/java_types.h | 21 ++++++++-- .../RecursiveGeneric.class | Bin 0 -> 346 bytes .../RecursiveGeneric.java | 4 ++ .../SimpleRecursiveGeneric.class | Bin 0 -> 466 bytes .../SimpleRecursiveGeneric.java | 4 ++ .../parse_recursive_generic_class.cpp | 36 ++++++++++++++++++ 11 files changed, 91 insertions(+), 16 deletions(-) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 3231c347182..cf3df55f6b7 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -119,6 +119,7 @@ void java_bytecode_convert_classt::convert(const classt &c) { // Do nothing: we don't support parsing for example double bounded or // two entry elements + } } @@ -218,8 +219,9 @@ void java_bytecode_convert_classt::convert( typet field_type; if(f.signature.has_value()) { - field_type=java_type_from_string( - f.signature.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;` diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 7e0f09fcf47..d412d05e88c 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -366,8 +366,9 @@ void java_bytecode_convert_methodt::convert( typet t; if(v.signature.has_value()) { - t=java_type_from_string( - v.signature.value(), + t=java_type_from_string_with_exception( + v.descriptor, + v.signature, id2string(class_symbol.name)); } else diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 9bea073ff14..ea41593e88a 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -339,8 +339,9 @@ void java_bytecode_parsert::get_class_refs() typet field_type; if(field.signature.has_value()) { - field_type=java_type_from_string( - field.signature.value(), + field_type=java_type_from_string_with_exception( + field.descriptor, + field.signature, "java::"+id2string(parse_tree.parsed_class.name)); } else @@ -354,8 +355,9 @@ void java_bytecode_parsert::get_class_refs() typet method_type; if(method.signature.has_value()) { - method_type=java_type_from_string( - method.signature.value(), + method_type=java_type_from_string_with_exception( + method.descriptor, + method.signature, "java::"+id2string(parse_tree.parsed_class.name)); } else @@ -367,8 +369,9 @@ void java_bytecode_parsert::get_class_refs() typet var_type; if(var.signature.has_value()) { - var_type=java_type_from_string( - var.signature.value(), + var_type=java_type_from_string_with_exception( + var.descriptor, + var.signature, "java::"+id2string(parse_tree.parsed_class.name)); } else diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index 573bac2e57f..1f777ed3095 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -770,7 +770,16 @@ void java_bytecode_convert_methodt::setup_local_variables( #endif typet t; if(v.var.signature.has_value()) - t=java_type_from_string(v.var.signature.value()); + { + try + { + t=java_type_from_string(v.var.signature.value()); + } + catch(unsupported_java_class_siganture_exceptiont &e) + { + t=java_type_from_string(v.var.descriptor); + } + } else t=java_type_from_string(v.var.descriptor); diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 09f12d4d3fd..9264295aff1 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -325,7 +325,8 @@ typet java_type_from_string( { std::size_t e_pos=find_closing_delimiter(src, f_pos, '<', '>'); if(e_pos==std::string::npos) - return nil_typet(); + throw unsupported_java_class_siganture_exceptiont( + "recursive generic"); // construct container type std::string generic_container_class=src.substr(1, f_pos-1); @@ -520,7 +521,7 @@ std::vector java_generic_type_from_string( std::string signature(src.substr(1, signature_end-1)); if(signature.find(";:")!=std::string::npos) - throw unsupported_java_class_siganture_exceptiont(); + throw unsupported_java_class_siganture_exceptiont("multiple bounds"); PRECONDITION(signature[signature.size()-1]==';'); diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 6ea659a773d..2834e505e33 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -356,10 +356,25 @@ inline const typet &java_generics_class_type_bound( class unsupported_java_class_siganture_exceptiont:public std::logic_error { public: - unsupported_java_class_siganture_exceptiont(): + explicit unsupported_java_class_siganture_exceptiont(std::string type): std::logic_error( - "Unsupported class signature: multiple bounds") - {} + "Unsupported class signature: "+type) + { + } }; +inline typet java_type_from_string_with_exception( + const std::string &descriptor, + const optionalt &signature, + const std::string &class_name) { + try + { + return java_type_from_string(signature.value(), class_name); + } + catch (unsupported_java_class_siganture_exceptiont &e) + { + return java_type_from_string(descriptor, class_name); + } +} + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H 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 0000000000000000000000000000000000000000..d637a7292a4e56ccfb0d490ac6e5ad3ebbe4315f GIT binary patch literal 346 zcmZusu};HK3_Q1KLeoG?C72lts$gLw>VgDI)PbPxufYPNG(oRP{)-8Tfe+xLD*QsH zfTia<-}z*{@7?DYfNM-c^f3-F32;pCV=1Is5c;$86~VhLpO`RCq~K+}S+jjK>s*y- zQf4M!87pqyi(d62TjxD+R@<#Ke9r}2$!-Y4RGte{)mFpvB$dru&fT^6Z*ZZ}FfD7F z@twHCC*9EHt7%LG4+FxaYZ6ZXKZP^&^xv*XpQaUkWmk$$8C-mT-j(zaX!l!@aG*T; QUBD1w>yO$V;jqP{AKchc6#xJL literal 0 HcmV?d00001 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..882452b71c1 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java @@ -0,0 +1,4 @@ +class RecursiveGeneric extends SimpleRecursiveGeneric +{ + +} \ No newline at end of file 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 0000000000000000000000000000000000000000..3ca52a2b92bb9bad327aa21a9a261425248ee460 GIT binary patch literal 466 zcmaJ-!AiqG5Ph4ZiH*_LszngNqk6ChJ=G8pK`%kUgx)uCsaw)b*=`DcmZyRTKfsR? zC$%0b)yvL%Z)V=i&d2B5JAg}cec0Ibu;*c)ff8YHFJE4S@`4vMm zkwe8zr3HhXrlh!`RMJF5PfiC6&Q1A5xmGNdxUa^U&?(OfQaW*&^J2iYtoc%O%(I*_ zbXRjPlb`(2ADe_UI-=nhVcP$> +{ + public T t; +} \ No newline at end of file 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. +} From 04e55be3b4964ab9ac1e3836d4f566dede0c3fc7 Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 3 Oct 2017 18:29:45 +0100 Subject: [PATCH 18/28] Reverting method descriptor loading MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The signature and the descriptor of a method do not match up (see java spec: The signature and descriptor (ยง4.3.3) of a given method or constructor may not correspond exactly, due to compiler-generated artifacts. In particular, the number of TypeSignatures that encode formal arguments in MethodTypeSignature may be less than the number of ParameterDescriptors in MethodDescriptor.) Reverting this to descriptor solves the current problem with passing tests. --- .../java_bytecode_convert_method.cpp | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index d412d05e88c..f6d267ef087 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -263,20 +263,7 @@ void java_bytecode_convert_method_lazy( symbol_tablet &symbol_table) { symbolt method_symbol; - 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); + typet member_type=java_type_from_string(m.descriptor); method_symbol.name=method_identifier; method_symbol.base_name=m.base_name; From a9dc64d3da1643859b99abac69bb927967a678a0 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 4 Oct 2017 10:23:21 +0100 Subject: [PATCH 19/28] Disabling part of the unit test for generic classes Due to methods no longer being recognised as generics (signature/descriptor issue). --- .../parse_generic_class.cpp | 62 ++++++++++--------- 1 file changed, 32 insertions(+), 30 deletions(-) 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 index 980a920bc4a..62047e4dff7 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -188,36 +188,38 @@ SCENARIO( new_symbol_table .has_symbol("java::generics$bound_element.g:(Ljava/lang/Number;)V")); - 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); - } +// 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") From 3a1962f21797ef45d590e61c7df1849bd06226b2 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 4 Oct 2017 10:37:38 +0100 Subject: [PATCH 20/28] Turning back on regression tests --- regression/cbmc-java/enum1/test.desc | 4 +--- regression/cbmc-java/iterator2/test.desc | 4 +--- regression/cbmc-java/lvt-groovy/test.desc | 3 +-- 3 files changed, 3 insertions(+), 8 deletions(-) diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc index 51d41e272c3..eff2c2e6817 100644 --- a/regression/cbmc-java/enum1/test.desc +++ b/regression/cbmc-java/enum1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE enum1.class --java-unwind-enum-static --unwind 3 ^VERIFICATION SUCCESSFUL$ @@ -7,5 +7,3 @@ enum1.class ^Unwinding loop java::enum1.:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.:\(\)V bytecode-index 78 thread 0$ -- ^warning: ignoring --- -cf. https://diffblue.atlassian.net/browse/TG-611 diff --git a/regression/cbmc-java/iterator2/test.desc b/regression/cbmc-java/iterator2/test.desc index 4f4f1490295..1919744c42d 100644 --- a/regression/cbmc-java/iterator2/test.desc +++ b/regression/cbmc-java/iterator2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE iterator2.class --cover location --unwind 3 --function iterator2.f ^EXIT=0$ @@ -6,5 +6,3 @@ iterator2.class ^.*SATISFIED$ -- ^warning: ignoring --- -https://diffblue.atlassian.net/browse/TG-610 diff --git a/regression/cbmc-java/lvt-groovy/test.desc b/regression/cbmc-java/lvt-groovy/test.desc index 7bbc58e4854..050fcd09c7e 100644 --- a/regression/cbmc-java/lvt-groovy/test.desc +++ b/regression/cbmc-java/lvt-groovy/test.desc @@ -1,8 +1,7 @@ -KNOWNBUG +CORE DetectSplitPackagesTask.class --show-symbol-table ^EXIT=0$ ^SIGNAL=0$ -- -- -cf. https://diffblue.atlassian.net/browse/TG-610 From 8f527f8fe33dca53108d100e6d93399b352ee012 Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 2 Oct 2017 14:52:00 +0100 Subject: [PATCH 21/28] Cleaning java files --- .../java_bytecode_parse_generics/Bar.class | Bin 242 -> 221 bytes .../java_bytecode_parse_generics/Bar.java | 4 +++ .../BasicInterface.class | Bin 140 -> 130 bytes .../BasicInterface.java | 4 +++ .../java_bytecode_parse_generics/Foo.class | Bin 377 -> 356 bytes .../java_bytecode_parse_generics/Foo.java | 8 ++++++ .../GenericArray.class | Bin 364 -> 492 bytes .../GenericArray.java | 18 ------------- .../GenericFunctions.java | 2 +- .../RecursiveGeneric.java | 2 +- .../SimpleGeneric.class | Bin 451 -> 698 bytes .../SimpleGeneric.java | 11 ++++++++ .../SimpleRecursiveGeneric.java | 2 +- .../WildcardGenericFunctions.class | Bin 2131 -> 2131 bytes .../WildcardGenericFunctions.java | 24 +----------------- 15 files changed, 31 insertions(+), 44 deletions(-) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/Bar.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/BasicInterface.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/Foo.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.java diff --git a/unit/java_bytecode/java_bytecode_parse_generics/Bar.class b/unit/java_bytecode/java_bytecode_parse_generics/Bar.class index 514dd58177aa495664e1a72f136fec3311a6e8f3..3b52a177ccaea0ff06e2439b8d485a80ce068fdc 100644 GIT binary patch delta 44 vcmeywc$aZP0SkvyV$sA-A6Z5Q4h9AW9tK7r$;!aVzy+ik8MuKY69W$b(WnK! delta 40 vcmcc1_=#~sfuwABW==|SVo{2FYF=tlX0lspUUErheqQm!5+6qXi3eo>L46N* 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 index aec76f72c2de16b6e40026abb64234d9b78096f4..83f7444582fd779e67f1716624b7b078895b92bf 100644 GIT binary patch delta 25 gcmeBSY+{_C!!PWVSe%*cnOBlpl$MyBI?>e~0A?x(e*gdg delta 35 qcmZo->|vasBPko6nUj*7Sd`+PnwMIXne0}Ymt2yWpI1E5+8qGZ`3$xI 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/Foo.class b/unit/java_bytecode/java_bytecode_parse_generics/Foo.class index 7951f8e22128e9365de3543ba637b8a3e3ef31f9..e64c1c07f6af0f6b43b48c686fa54ed4d3961607 100644 GIT binary patch delta 32 ocmey#^n__bFAIlTe*VN|m5hv&6&P(M%QK3x3oDG486?>mq$Y~iMhW@kCnx5FB^G5SCgr4tfCxqg zmXeIjVnzl&ANSO})S}E}$D*RdN^3?2F;vBs1uzZ5C@O72LagnqCr(%s;>f@VgbWO< wTH6^IHv$>V4E#Wn4J^pWAOK|ZKol?tG6(^A!YCplKpqoNHHZ{t5ChZV0C9dP*Z=?k delta 81 zcmaFE{Dw*N)W2Q(7#J8#7{s_3m>GoG8AR9_L??>YPJFk@K$d|K2pJeywYD=bZUizI Y8Tf%D8(2_?feFZB0FnX>f?!$*0I>iIZvX%Q diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java b/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java index 0569d66177b..98cf9333743 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java +++ b/unit/java_bytecode/java_bytecode_parse_generics/GenericArray.java @@ -1,24 +1,6 @@ -interface BasicInterface -{ - int getX(); -} - -class Foo implements BasicInterface -{ - public int x; - - public int getX() { - return x; - } -} - -class Bar extends Foo -{} - class GenericArray { public T [] t; public Integer [] Ia; public int [] ia; } - diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java b/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java index 8673d2ee530..5a5eb5221f7 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java +++ b/unit/java_bytecode/java_bytecode_parse_generics/GenericFunctions.java @@ -23,4 +23,4 @@ public static void processDoubleUpperBoundClass public static void processDoubleUpperBoundInterfaceGeneric(SimpleGeneric x) { assert(x.t.getX() == 4); } -} \ No newline at end of file +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java b/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java index 882452b71c1..d3582c8bd46 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java +++ b/unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java @@ -1,4 +1,4 @@ class RecursiveGeneric extends SimpleRecursiveGeneric { -} \ No newline at end of file +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/SimpleGeneric.class index 9548607d012dcff5823af843f83293beda9d6c0b..6ade3945c8dcc42a39eb17ae583b8b026e8b582b 100644 GIT binary patch literal 698 zcmZuuT}uK%6g{J^U#)3o_Wc39s6oE;R3b!BFH#RKL674$*wnhlwif-XdI+JQAJC7A z&S(~!F>vSJbI-Z=&fJgB*LMJW*v!JhY6@#v#ITy7Sx;d@K!gIt*0sEsbx-=;`dQ~% zx#598rmefa3y-nk64 ziNC=_c%|t1>T zPGE70X`URVra^fu!2)p*PZ24wscH3_ W%lzbu%#B~ONafgD!ZPzQtb75|or~-M delta 210 zcmdnRdYD=C)W2Q(7#J8#7{s|4m>ERa8ARC`#3ssbp6tPBVJsV-nUj*7Sd`+PnwMIX zne0}Ymt2yWpI5Axl~|U@!@$A7$;iMPoS9pYlL}Qbc`c(v1vAh@Mj&KiU;0BUxU_l`U9w3_sqJV*yfe*;zM-dSK@|d7T K3o;0SdBOnZSRK#+ 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.java b/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.java index 9f57670ecaa..e95851602da 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.java +++ b/unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.java @@ -1,4 +1,4 @@ class SimpleRecursiveGeneric> { public T t; -} \ No newline at end of file +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.class b/unit/java_bytecode/java_bytecode_parse_generics/WildcardGenericFunctions.class index c6e7ae228e78146807a344ef6b11d94c2722b2aa..bf78c910d1974ca2d3852501272b2636dd7fe16e 100644 GIT binary patch delta 130 zcmWNJI}QP16h_aT -{ - public T t; -} - public class WildcardGenericFunctions { // Test a wild card generic type @@ -73,4 +51,4 @@ public static void test() SimpleGeneric baseGenericValue = new SimpleGeneric(); processLowerBoundGeneric(baseGenericValue, new Foo()); } -} \ No newline at end of file +} From 4f305ded9f2a69c3b0117f688d38426cfd3d3f42 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 4 Oct 2017 15:46:10 +0100 Subject: [PATCH 22/28] Handling wild card generics with exception Instead of partial handling from before. --- src/java_bytecode/java_types.cpp | 43 +------------------------------- 1 file changed, 1 insertion(+), 42 deletions(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 9264295aff1..8e8b3e4789e 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -416,55 +416,14 @@ typet java_type_from_string( return java_reference_type(symbol_type); } case '*': - { -#ifdef DEBUG - std::cout << class_name << std::endl; -#endif - // parse name of type variable - INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); - PRECONDITION(!class_name.empty()); -// INVARIANT( -// src.substr(1, src.size()-2)=="*", -// "Wildcard types do not have a name"); - irep_idt type_var_name(class_name+"::*"); - return java_generic_parametert( - type_var_name, - java_type_from_string("Ljava/lang/Object;").subtype()); - } case '+': - { -#ifdef DEBUG - std::cout << class_name << std::endl; -#endif - // parse name of type variable - INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); - PRECONDITION(!class_name.empty()); -// INVARIANT( -// src.substr(1, src.size()-2)=="*", -// "Wildcard types do not have a name"); - irep_idt type_var_name(class_name+"::*"); - return java_generic_parametert( - type_var_name, - java_type_from_string("Ljava/lang/Object;").subtype()); - } case '-': { #ifdef DEBUG std::cout << class_name << std::endl; #endif - // parse name of type variable - INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); - PRECONDITION(!class_name.empty()); -// INVARIANT( -// src.substr(1, src.size()-2)=="*", -// "Wildcard types do not have a name"); - irep_idt type_var_name(class_name+"::*"); - return java_generic_parametert( - type_var_name, - java_type_from_string("Ljava/lang/Object;").subtype()); + throw unsupported_java_class_siganture_exceptiont("wild card generic"); } - - default: return nil_typet(); } From 97e1b9ad8eeb3c0f0755ade714fd894f15709407 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 4 Oct 2017 15:57:06 +0100 Subject: [PATCH 23/28] Adding a warning and a commentary for unsupported generics, cleaning --- src/java_bytecode/java_bytecode_convert_class.cpp | 5 ++--- src/java_bytecode/java_types.cpp | 7 +++++++ src/java_bytecode/java_types.h | 4 +++- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index cf3df55f6b7..bd975cf0bc3 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -117,9 +117,8 @@ void java_bytecode_convert_classt::convert(const classt &c) } catch(unsupported_java_class_siganture_exceptiont) { - // Do nothing: we don't support parsing for example double bounded or - // two entry elements - + warning() << "we currently don't support parsing for example double " + "bounded, recursive and wild card generics" << eom; } } diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 8e8b3e4789e..4ac37c09b78 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -201,6 +201,13 @@ typet java_type_from_string( // 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, '<', '>'); const typet &method_type=java_type_from_string( src.substr(closing_generic+1, std::string::npos), class_name); diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 2834e505e33..d15c3056b60 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include class java_class_typet:public class_typet { @@ -366,7 +367,8 @@ class unsupported_java_class_siganture_exceptiont:public std::logic_error inline typet java_type_from_string_with_exception( const std::string &descriptor, const optionalt &signature, - const std::string &class_name) { + const std::string &class_name) +{ try { return java_type_from_string(signature.value(), class_name); From cfb52122c37d06ab9080d070f58fd6578aa44e10 Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 9 Oct 2017 13:04:06 +0100 Subject: [PATCH 24/28] Resolving name shadowing class_name parameter renamed to class_name_prefix --- src/java_bytecode/java_types.cpp | 24 +++++++++++++----------- src/java_bytecode/java_types.h | 2 +- 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 4ac37c09b78..338092614aa 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -175,11 +175,11 @@ exprt java_bytecode_promotion(const exprt &expr) /// "Ljava/util/List;" or "Ljava/util/List;" /// /// \param src: the string representation as used in the class file -/// \param class_name: name of class to append to generic type variables +/// \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) + const std::string &class_name_prefix) { if(src.empty()) return nil_typet(); @@ -210,7 +210,7 @@ typet java_type_from_string( // (TT;TU;I)V size_t closing_generic=find_closing_delimiter(src, 0, '<', '>'); const typet &method_type=java_type_from_string( - src.substr(closing_generic+1, std::string::npos), class_name); + 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. @@ -233,7 +233,7 @@ typet java_type_from_string( result.return_type()= java_type_from_string( std::string(src, e_pos+1, std::string::npos), - class_name); + class_name_prefix); for(std::size_t i=1; i java_generic_type_from_string( const std::string &, From e140bb718c9388e8fd18a6a1ae99e950bf0368b0 Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 9 Oct 2017 14:36:54 +0100 Subject: [PATCH 25/28] Updating the calls of lookup method to reflect the new return type The return type of the method lookup for the symbol table has changed in a recent CBMC commit. --- .../parse_derived_generic_class.cpp | 3 ++- .../parse_generic_array_class.cpp | 4 ++-- .../parse_generic_class.cpp | 15 +++++++++------ 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index 94dc166b0c0..bb4c6c70337 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -32,7 +32,8 @@ SCENARIO( std::string class_prefix="java::DerivedGeneric"; REQUIRE(new_symbol_table.has_symbol(class_prefix)); - const symbolt &derived_symbol=new_symbol_table.lookup(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); 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 index 08feff8716c..35bf3a273a6 100644 --- 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 @@ -33,7 +33,7 @@ SCENARIO( const struct_typet &type=to_struct_type( new_symbol_table.lookup(class_prefix) - .type); + .value().get().type); THEN("There should be a component with name t") { @@ -49,7 +49,7 @@ SCENARIO( { const struct_typet &subtype_type=to_struct_type( new_symbol_table.lookup(subtype.get_identifier()) - .type); + .value().get().type); REQUIRE(is_valid_java_array(subtype_type)); } 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 index 62047e4dff7..3fe67dd7540 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -32,7 +32,7 @@ SCENARIO( THEN("The symbol type should be generic") { const symbolt &class_symbol= - new_symbol_table.lookup("java::generics$element"); + new_symbol_table.lookup("java::generics$element").value().get(); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -76,7 +76,7 @@ SCENARIO( THEN("The symbol type should be generic") { const symbolt &class_symbol= - new_symbol_table.lookup("java::generics$bound_element"); + new_symbol_table.lookup("java::generics$bound_element").value().get(); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -127,7 +127,8 @@ SCENARIO( THEN("The generic fields should be annotated with concrete types") { - const symbolt &class_symbol=new_symbol_table.lookup("java::generics"); + 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); @@ -176,7 +177,8 @@ SCENARIO( { const symbolt &method_symbol= new_symbol_table - .lookup("java::generics$bound_element.f:()Ljava/lang/Number;"); + .lookup("java::generics$bound_element.f:()Ljava/lang/Number;") + .value().get(); const typet &symbol_type=method_symbol.type; REQUIRE(symbol_type.id()==ID_code); @@ -231,7 +233,8 @@ SCENARIO( THEN("The symbol should have a generic parameter") { const symbolt &class_symbol= - new_symbol_table.lookup("java::generics$double_bound_element"); + new_symbol_table.lookup("java::generics$double_bound_element") + .value().get(); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -270,7 +273,7 @@ SCENARIO( THEN("Both generic parameters should be encoded") { const symbolt &class_symbol= - new_symbol_table.lookup("java::generics$two_elements"); + new_symbol_table.lookup("java::generics$two_elements").value().get(); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); From 608c6b680fb8ba8c97ff8eae6e42e95d7d18363d Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 9 Oct 2017 15:13:20 +0100 Subject: [PATCH 26/28] Disabling part of the unit test for generic classes Reintroduce when descriptor/signature issue is resolved. --- .../parse_generic_class.cpp | 27 ++++++++++--------- 1 file changed, 15 insertions(+), 12 deletions(-) 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 index 3fe67dd7540..d14553d2599 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -173,18 +173,21 @@ SCENARIO( new_symbol_table .has_symbol("java::generics$bound_element.f:()Ljava/lang/Number;")); - 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); - } +// 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 From 8d54be132662342b029a5cc7696287608add8270 Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 9 Oct 2017 15:46:15 +0100 Subject: [PATCH 27/28] Adding exception and tests for missing closing delimiter --- .../java_bytecode_convert_class.cpp | 2 +- .../java_local_variable_table.cpp | 2 +- src/java_bytecode/java_types.cpp | 11 +++- src/java_bytecode/java_types.h | 6 +- unit/java_bytecode/java_utils_test.cpp | 65 +++++++++++++++++++ 5 files changed, 78 insertions(+), 8 deletions(-) create mode 100644 unit/java_bytecode/java_utils_test.cpp diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index bd975cf0bc3..8f038c92440 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -115,7 +115,7 @@ void java_bytecode_convert_classt::convert(const classt &c) } class_type=generic_class_type; } - catch(unsupported_java_class_siganture_exceptiont) + catch(unsupported_java_class_signature_exceptiont) { warning() << "we currently don't support parsing for example double " "bounded, recursive and wild card generics" << eom; diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index 1f777ed3095..a64c13d61e2 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -775,7 +775,7 @@ void java_bytecode_convert_methodt::setup_local_variables( { t=java_type_from_string(v.var.signature.value()); } - catch(unsupported_java_class_siganture_exceptiont &e) + catch(unsupported_java_class_signature_exceptiont &e) { t=java_type_from_string(v.var.descriptor); } diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index 338092614aa..102cdb493cc 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -209,6 +209,11 @@ typet java_type_from_string( // 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); @@ -332,7 +337,7 @@ typet java_type_from_string( { std::size_t e_pos=find_closing_delimiter(src, f_pos, '<', '>'); if(e_pos==std::string::npos) - throw unsupported_java_class_siganture_exceptiont( + throw unsupported_java_class_signature_exceptiont( "recursive generic"); // construct container type @@ -431,7 +436,7 @@ typet java_type_from_string( #ifdef DEBUG std::cout << class_name_prefix << std::endl; #endif - throw unsupported_java_class_siganture_exceptiont("wild card generic"); + throw unsupported_java_class_signature_exceptiont("wild card generic"); } default: return nil_typet(); @@ -489,7 +494,7 @@ std::vector java_generic_type_from_string( std::string signature(src.substr(1, signature_end-1)); if(signature.find(";:")!=std::string::npos) - throw unsupported_java_class_siganture_exceptiont("multiple bounds"); + throw unsupported_java_class_signature_exceptiont("multiple bounds"); PRECONDITION(signature[signature.size()-1]==';'); diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index a00d6a27300..e4c370157e0 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -354,10 +354,10 @@ inline const typet &java_generics_class_type_bound( /// An exception that is raised for unsupported class signature. /// Currently we do not parse multiple bounds. -class unsupported_java_class_siganture_exceptiont:public std::logic_error +class unsupported_java_class_signature_exceptiont:public std::logic_error { public: - explicit unsupported_java_class_siganture_exceptiont(std::string type): + explicit unsupported_java_class_signature_exceptiont(std::string type): std::logic_error( "Unsupported class signature: "+type) { @@ -373,7 +373,7 @@ inline typet java_type_from_string_with_exception( { return java_type_from_string(signature.value(), class_name); } - catch (unsupported_java_class_siganture_exceptiont &e) + catch (unsupported_java_class_signature_exceptiont &e) { return java_type_from_string(descriptor, class_name); } 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); + } + } +} From b7aaad0bf81907c112ca31c202af4a61e64a682c Mon Sep 17 00:00:00 2001 From: svorenova Date: Mon, 9 Oct 2017 17:24:39 +0100 Subject: [PATCH 28/28] Removing signature parsing for local variables Might need changing once the signature/descriptor issue is resolved. --- src/java_bytecode/java_local_variable_table.cpp | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index a64c13d61e2..dc519b3fa09 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -769,19 +769,8 @@ void java_bytecode_convert_methodt::setup_local_variables( << v.var.descriptor << "' holes " << v.holes.size() << eom; #endif typet t; - if(v.var.signature.has_value()) - { - try - { - t=java_type_from_string(v.var.signature.value()); - } - catch(unsupported_java_class_signature_exceptiont &e) - { - t=java_type_from_string(v.var.descriptor); - } - } - else - t=java_type_from_string(v.var.descriptor); + // 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;