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 00000000000..962e5833c97 Binary files /dev/null and b/regression/cbmc-java/generics_type_param/FWrapper.class differ 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 00000000000..daf2c6ff9b4 Binary files /dev/null and b/regression/cbmc-java/generics_type_param/GenericFields$SimpleGenericField.class differ 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 00000000000..b8681542a7a Binary files /dev/null and b/regression/cbmc-java/generics_type_param/GenericFields.class differ 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 00000000000..2036cfbb8c3 Binary files /dev/null and b/regression/cbmc-java/generics_type_param/IWrapper.class differ diff --git a/regression/cbmc-java/generics_type_param/SimpleWrapper.class b/regression/cbmc-java/generics_type_param/SimpleWrapper.class new file mode 100644 index 00000000000..dc027a9d615 Binary files /dev/null and b/regression/cbmc-java/generics_type_param/SimpleWrapper.class differ diff --git a/regression/cbmc-java/generics_type_param/test.desc b/regression/cbmc-java/generics_type_param/test.desc new file mode 100644 index 00000000000..762ac73f8ec --- /dev/null +++ b/regression/cbmc-java/generics_type_param/test.desc @@ -0,0 +1,8 @@ +CORE +GenericFields$SimpleGenericField.class +--cover location --function GenericFields\$SimpleGenericField.foo --verbosity 10 +^EXIT=0$ +^SIGNAL=0$ +Reading class AWrapper +Reading class FWrapper +Reading class IWrapper 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