From fae14fc217e2dcb44b5a8f48992b15c737a4b10b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 16 Nov 2017 23:30:00 +0100 Subject: [PATCH 1/2] Add type parameters in signatures as dependencies This patch analyzes the generic signatures in a class file in order to load generic type args as class dependencies. All those types are added to the class_refs of the parser to complete the dependency information. Before, a Java object type that was only used as a generic type argument was not necessarily loaded. --- .../java_bytecode_convert_method.cpp | 9 -- src/java_bytecode/java_bytecode_parser.cpp | 12 +++ src/java_bytecode/java_types.cpp | 90 +++++++++++++++++++ src/java_bytecode/java_types.h | 8 ++ src/java_bytecode/java_utils.cpp | 12 +++ src/java_bytecode/java_utils.h | 2 + 6 files changed, 124 insertions(+), 9 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index d9cbab10fed..07627b0d062 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -116,15 +116,6 @@ static bool operator==(const irep_idt &what, const patternt &pattern) return pattern==what; } -static irep_idt strip_java_namespace_prefix(const irep_idt to_strip) -{ - const std::string to_strip_str=id2string(to_strip); - const std::string prefix="java::"; - - PRECONDITION(has_prefix(to_strip_str, prefix)); - return to_strip_str.substr(prefix.size(), std::string::npos); -} - // name contains or bool java_bytecode_convert_methodt::is_constructor( const class_typet::methodt &method) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 38a1045c50d..4b71fd29f13 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -343,6 +343,11 @@ void java_bytecode_parsert::get_class_refs() field.descriptor, field.signature, "java::"+id2string(parse_tree.parsed_class.name)); + + // add generic type args to class refs as dependencies, same below for + // method types and entries from the local variable type table + get_dependencies_from_generic_parameters( + field_type, parse_tree.class_refs); } else field_type=java_type_from_string(field.descriptor); @@ -359,6 +364,8 @@ void java_bytecode_parsert::get_class_refs() method.descriptor, method.signature, "java::"+id2string(parse_tree.parsed_class.name)); + get_dependencies_from_generic_parameters( + method_type, parse_tree.class_refs); } else method_type=java_type_from_string(method.descriptor); @@ -373,6 +380,8 @@ void java_bytecode_parsert::get_class_refs() var.descriptor, var.signature, "java::"+id2string(parse_tree.parsed_class.name)); + get_dependencies_from_generic_parameters( + var_type, parse_tree.class_refs); } else var_type=java_type_from_string(var.descriptor); @@ -1356,6 +1365,9 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class) { u2 signature_index=read_u2(); parsed_class.signature=id2string(pool_entry(signature_index).s); + get_dependencies_from_generic_parameters( + parsed_class.signature.value(), + parse_tree.class_refs); } else if(attribute_name=="RuntimeInvisibleAnnotations" || attribute_name=="RuntimeVisibleAnnotations") diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp index bbb24205439..3e9f3925274 100644 --- a/src/java_bytecode/java_types.cpp +++ b/src/java_bytecode/java_types.cpp @@ -715,3 +715,93 @@ bool is_valid_java_array(const struct_typet &type) length_component_valid && data_component_valid; } + +void get_dependencies_from_generic_parameters_rec( + const typet &t, + std::set &refs) +{ + // Java generic type that holds different types in its type arguments + if(is_java_generic_type(t)) + { + for(const auto type_arg : to_java_generic_type(t).generic_type_arguments()) + get_dependencies_from_generic_parameters_rec(type_arg, refs); + } + + // Java reference type + else if(t.id() == ID_pointer) + { + get_dependencies_from_generic_parameters_rec(t.subtype(), refs); + } + + // method type with parameters and return value + else if(t.id() == ID_code) + { + const code_typet &c = to_code_type(t); + get_dependencies_from_generic_parameters_rec(c.return_type(), refs); + for(const auto ¶m : c.parameters()) + get_dependencies_from_generic_parameters_rec(param.type(), refs); + } + + // symbol type + else if(t.id() == ID_symbol) + { + const symbol_typet &symbol_type = to_symbol_type(t); + const irep_idt class_name(symbol_type.get_identifier()); + if(is_java_array_tag(class_name)) + { + get_dependencies_from_generic_parameters( + java_array_element_type(symbol_type), refs); + } + else + refs.insert(strip_java_namespace_prefix(class_name)); + } +} + +/// Collect information about generic type parameters from a given +/// signature. This is used to get information about class dependencies that +/// must be loaded but only appear as generic type argument, not as a field +/// reference. +/// \param signature: the string representation of the signature to analyze +/// \param refs [out]: the set to insert the names of the found dependencies +void get_dependencies_from_generic_parameters( + const std::string &signature, + std::set &refs) +{ + try + { + // class signature with bounds + if(signature[0] == '<') + { + const std::vector types = java_generic_type_from_string( + erase_type_arguments(signature), signature); + + for(const auto &t : types) + get_dependencies_from_generic_parameters_rec(t, refs); + } + + // class signature without bounds and without wildcards + else if(signature.find('*') == std::string::npos) + { + get_dependencies_from_generic_parameters_rec( + java_type_from_string(signature, erase_type_arguments(signature)), + refs); + } + } + catch(unsupported_java_class_signature_exceptiont &) + { + // skip for now, if we cannot parse it, we cannot detect which additional + // classes should be loaded as dependencies + } +} + +/// Collect information about generic type parameters from a given type. This is +/// used to get information about class dependencies that must be loaded but +/// only appear as generic type argument, not as a field reference. +/// \param t: the type to analyze +/// \param refs [out]: the set to insert the names of the found dependencies +void get_dependencies_from_generic_parameters( + const typet &t, + std::set &refs) +{ + get_dependencies_from_generic_parameters_rec(t, refs); +} diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 4925f03a4f8..3c4df0ade38 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -366,4 +367,11 @@ inline const optionalt java_generics_get_index_for_subtype( return std::distance(gen_types.cbegin(), iter); } +void get_dependencies_from_generic_parameters( + const std::string &, + std::set &); +void get_dependencies_from_generic_parameters( + const typet &, + std::set &); + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index aba810677ce..f720d32ada8 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -293,3 +293,15 @@ exprt make_function_application( call.arguments()=arguments; return call; } + +/// Strip java:: prefix from given identifier +/// \param to_strip: identifier from which the prefix is stripped +/// \return the identifier without without java:: prefix +irep_idt strip_java_namespace_prefix(const irep_idt &to_strip) +{ + const std::string to_strip_str=id2string(to_strip); + const std::string prefix="java::"; + + PRECONDITION(has_prefix(to_strip_str, prefix)); + return to_strip_str.substr(prefix.size(), std::string::npos); +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index f45df9ef62c..6f163df484f 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -92,4 +92,6 @@ exprt make_function_application( const typet &type, symbol_table_baset &symbol_table); +irep_idt strip_java_namespace_prefix(const irep_idt &to_strip); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H From e8f5e0817b0e2de165faab6fd0941d72dea2676a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 17 Nov 2017 08:56:30 +0100 Subject: [PATCH 2/2] Add regression tests for generic type arg dependencies --- .../generics_type_param/FWrapper.class | Bin 0 -> 195 bytes .../GenericFields$SimpleGenericField.class | Bin 0 -> 715 bytes .../generics_type_param/GenericFields.class | Bin 0 -> 290 bytes .../generics_type_param/GenericFields.java | 25 ++++++++++++++++++ .../generics_type_param/IWrapper.class | Bin 0 -> 211 bytes .../generics_type_param/SimpleWrapper.class | Bin 0 -> 263 bytes .../cbmc-java/generics_type_param/test.desc | 8 ++++++ 7 files changed, 33 insertions(+) create mode 100644 regression/cbmc-java/generics_type_param/FWrapper.class create mode 100644 regression/cbmc-java/generics_type_param/GenericFields$SimpleGenericField.class create mode 100644 regression/cbmc-java/generics_type_param/GenericFields.class create mode 100644 regression/cbmc-java/generics_type_param/GenericFields.java create mode 100644 regression/cbmc-java/generics_type_param/IWrapper.class create mode 100644 regression/cbmc-java/generics_type_param/SimpleWrapper.class create mode 100644 regression/cbmc-java/generics_type_param/test.desc diff --git a/regression/cbmc-java/generics_type_param/FWrapper.class b/regression/cbmc-java/generics_type_param/FWrapper.class new file mode 100644 index 0000000000000000000000000000000000000000..962e5833c97b68776a11b5f7771569814c31988a GIT binary patch literal 195 zcmXAiy$ZrW5QOKNTmIB6jauhIEMM46-jml|TUn0^68D&hoeNpR}Le+%9 znsU-A4i#m|b(YGT^kKphaKn?9Wl36~-{2sV`8n7{Da92=Xz}Z&1UKKa+dK`~8)8i# R5cl8OVYUB|)#cPe`wQ@+Bwhdj literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generics_type_param/GenericFields$SimpleGenericField.class b/regression/cbmc-java/generics_type_param/GenericFields$SimpleGenericField.class new file mode 100644 index 0000000000000000000000000000000000000000..daf2c6ff9b4723df28d0a53bbaa39326b018e644 GIT binary patch literal 715 zcmZuv+e!ja6kW&hI%?Wvmf6L^2Q|nZdQ*fD3}L7TrHCG4)T134N14&Ss~$oq=mYww zXdg3lh91t@m$mlV`&_=h-#-Cd;5dQ+c2xwC31Lr#BJF+%M-0)v;AZbpSd-b5A)&X# zXkzj^+n7waU15l{#K1D9Gn+GH-Dp*B{_$$W3{IbflRuXtSKQ*Z=r*LZBcZCW#I(ks z6+Bq+mcd^i_eedV3yWXRMjdXqjgCnfr9U3iUXUc#XDAok15`X=(GxSYJrz~Gu^QRU zu0H6OE6gM1IjY(k&+IO52sx$ZI_=recs62)A{Ij&8bjQ5qaoxNa;}Q}FJV1LqW>jh zO^fceZW@lm9fqWARW=Q4P`>F5d6(WVzOLdRN6#LlAK;@ELKyU%i%3l-<%HxbwBpzx zBthN@F(p?moxXvU=J35zM4f04k_CATo6wg0%mO8bmzE-63n>zlvN^J{QTPMO{T%+6 bMcGO;y&P+scxl3X*uf!LmD&W5#R2dG!wsaT literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generics_type_param/GenericFields.class b/regression/cbmc-java/generics_type_param/GenericFields.class new file mode 100644 index 0000000000000000000000000000000000000000..b8681542a7aa3a30dffc3213253a359e7706fc99 GIT binary patch literal 290 zcmZXPKMw&x5XIm4cbxOLmyjq>&?rSCArhe=`n@xem9^v!-%BM?_y9hXm{Sou$!vb_ z&A!Y&U-t)qJ}NGfC^#rOC^;w-s!P2;8lJG_PzPhpW<&6%R&Zog6mdkz47Am!AtBjn zuL-HqVZ(&dOk19x_dbU!4F#Jk~K(zayjWPF<7-2U$Yl$03wsuV<9q_7?t* zgA<|tGt&Iu5e+2dC-EUE$(5cHs(lzpcW$8T$9AP>L#ya9*d BKMeo? literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generics_type_param/GenericFields.java b/regression/cbmc-java/generics_type_param/GenericFields.java new file mode 100644 index 00000000000..3b903ebaa56 --- /dev/null +++ b/regression/cbmc-java/generics_type_param/GenericFields.java @@ -0,0 +1,25 @@ +class IWrapper { + public int i; +} + +class FWrapper { +} + +class AWrapper { +} + +class SimpleWrapper { +} + +public class GenericFields +{ + class SimpleGenericField { + // IWrapper field; // for this to work, uncomment this line + SimpleWrapper field_input; + public void foo() { + } + SimpleWrapper f(SimpleWrapper s, SimpleWrapper a) { + return new SimpleWrapper<>(); + } + } +} diff --git a/regression/cbmc-java/generics_type_param/IWrapper.class b/regression/cbmc-java/generics_type_param/IWrapper.class new file mode 100644 index 0000000000000000000000000000000000000000..2036cfbb8c3f23e46ce07b65a5e09c724610ec03 GIT binary patch literal 211 zcmXAj%?`m(5QWbaZPjn=C6-vQu@oCgrHQa0tZ&vy_c25!UK3HF|Eb?eCOn3 z=JS2M0Zh>HP(s~7!$FfkS}GveQ=RJDj8N(ic7*c$95bP{)G4pBQ^;nk!bB8rbIwe} zzRsbu;FOJye9cLG9UawO)nUUSxWV42%Y_Z0oy+4yrHAo4JaTkH50<#5Iy5#_gOrme~A(WjSA7cghnVrw<3B^u#Ln!^9c1&n2wBcoX4A`z!5Q$Rp_1>r? zwZc1-^=NTW7d42K*$-C1fx~1x{gw!xe@bo0Go59$=4{yNaHcuho%>lr4JDKbbzdLj xh__b7F