diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index f600348b943..9da994b9ad7 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -677,7 +677,11 @@ void java_bytecode_convert_classt::convert( } } else - field_type = *java_type_from_string(f.descriptor); + { + auto type_opt = java_type_from_string(f.descriptor); + CHECK_RETURN(type_opt.has_value()); + field_type = *type_opt; + } // determine access irep_idt access; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 2fe7ccafbf7..afd32801bf1 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -85,7 +85,9 @@ class java_bytecode_parsert final : public parsert const typet type_entry(u2 index) { - return *java_type_from_string(id2string(pool_entry(index).s)); + auto type_opt = java_type_from_string(id2string(pool_entry(index).s)); + CHECK_RETURN(type_opt.has_value()); + return std::move(*type_opt); } void rClassFile(); @@ -408,6 +410,12 @@ bool java_bytecode_parsert::parse() return true; } + catch(const unsupported_java_class_signature_exceptiont &e) + { + log.error() << e.str() << messaget::eom; + return true; + } + catch(...) { log.error() << "parsing error" << messaget::eom; @@ -514,8 +522,11 @@ void java_bytecode_parsert::get_class_refs() break; case CONSTANT_NameAndType: - get_class_refs_rec( - *java_type_from_string(id2string(pool_entry(c.ref2).s))); + { + auto type_opt = java_type_from_string(id2string(pool_entry(c.ref2).s)); + CHECK_RETURN(type_opt.has_value()); + get_class_refs_rec(*type_opt); + } break; default: {} @@ -543,7 +554,9 @@ void java_bytecode_parsert::get_class_refs() } else { - get_class_refs_rec(*java_type_from_string(field.descriptor)); + auto type_opt = java_type_from_string(field.descriptor); + CHECK_RETURN(type_opt); + get_class_refs_rec(*type_opt); } } @@ -565,7 +578,9 @@ void java_bytecode_parsert::get_class_refs() } else { - get_class_refs_rec(*java_type_from_string(method.descriptor)); + auto type_opt = java_type_from_string(method.descriptor); + CHECK_RETURN(type_opt); + get_class_refs_rec(*type_opt); } for(const auto &var : method.local_variable_table) @@ -582,7 +597,9 @@ void java_bytecode_parsert::get_class_refs() } else { - get_class_refs_rec(*java_type_from_string(var.descriptor)); + auto type_opt = java_type_from_string(var.descriptor); + CHECK_RETURN(type_opt.has_value()); + get_class_refs_rec(*type_opt); } } } @@ -637,7 +654,9 @@ void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value) if(const auto &symbol_expr = expr_try_dynamic_cast(value)) { const irep_idt &value_id = symbol_expr->get_identifier(); - get_class_refs_rec(*java_type_from_string(id2string(value_id))); + auto type_opt = java_type_from_string(id2string(value_id)); + CHECK_RETURN(type_opt.has_value()); + get_class_refs_rec(*type_opt); } else if(const auto &array_expr = expr_try_dynamic_cast(value)) { @@ -1967,13 +1986,14 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) irep_idt method_name = name_and_type.get_name(pool_entry_lambda); std::string descriptor = name_and_type.get_descriptor(pool_entry_lambda); irep_idt mangled_method_name = id2string(method_name) + ":" + descriptor; - typet method_type = *java_type_from_string(descriptor); + auto method_type_opt = java_type_from_string(descriptor); + CHECK_RETURN(method_type_opt.has_value()); method_handle_typet handle_type = get_method_handle_type(entry.get_handle_kind()); class_method_descriptor_exprt method_descriptor{ - method_type, mangled_method_name, class_name, method_name}; + *method_type, mangled_method_name, class_name, method_name}; lambda_method_handlet lambda_method_handle{method_descriptor, handle_type}; return lambda_method_handle; diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index fa074554c8e..8574a065337 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -307,6 +307,7 @@ bool is_java_main(const symbolt &function) bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD); const java_method_typet &function_type = to_java_method_type(function.type); const auto string_array_type = java_type_from_string("[Ljava/lang/String;"); + CHECK_RETURN(string_array_type.has_value()); // checks whether the function is static and has a single String[] parameter bool is_static = !function_type.has_this(); // this should be implied by the signature diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index d6f2c1b9ffe..c4fe64da1c2 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -624,10 +624,14 @@ std::optional java_type_from_string( { std::size_t e_pos=src.rfind(')'); if(e_pos==std::string::npos) - return {}; + { + throw unsupported_java_class_signature_exceptiont( + "Failed to find function signature closing delimiter"); + } auto return_type = java_type_from_string( std::string(src, e_pos + 1, std::string::npos), class_name_prefix); + CHECK_RETURN(return_type.has_value()); std::vector param_types = parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')'); @@ -648,10 +652,14 @@ std::optional java_type_from_string( // If this is a reference array, we generate a plain array[reference] // with void* members, but note the real type in ID_element_type. if(src.size()<=1) - return {}; + { + throw unsupported_java_class_signature_exceptiont( + "Failed to find array signature closing delimiter"); + } char subtype_letter=src[1]; auto subtype = java_type_from_string( src.substr(1, std::string::npos), class_name_prefix); + CHECK_RETURN(subtype.has_value()); if(subtype_letter=='L' || // [L denotes a reference array of some sort. subtype_letter=='[' || // Array-of-arrays subtype_letter=='T') // Array of generic types @@ -681,11 +689,11 @@ std::optional java_type_from_string( INVARIANT(src[src.size()-1]==';', "Generic type name must end on ';'."); PRECONDITION(!class_name_prefix.empty()); irep_idt type_var_name(class_name_prefix+"::"+src.substr(1, src.size()-2)); + auto lang_object = java_type_from_string("Ljava/lang/Object;"); + CHECK_RETURN(lang_object.has_value()); return java_generic_parametert( type_var_name, - to_struct_tag_type( - to_java_reference_type(*java_type_from_string("Ljava/lang/Object;")) - .base_type())); + to_struct_tag_type(to_java_reference_type(*lang_object).base_type())); } case 'L': { @@ -781,13 +789,13 @@ std::vector java_generic_type_from_string( 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)); - + std::string bound_type_str( + signature.substr(bound_sep + 1, var_sep - bound_sep)); + auto bound_type = java_type_from_string(bound_type_str, class_name); + CHECK_RETURN(bound_type.has_value()); java_generic_parametert type_var_type( type_var_name, - to_struct_tag_type( - to_java_reference_type(*java_type_from_string(bound_type, class_name)) - .base_type())); + to_struct_tag_type(to_java_reference_type(*bound_type).base_type())); types.push_back(type_var_type); signature=signature.substr(var_sep+1, std::string::npos); @@ -809,8 +817,11 @@ static std::string slash_to_dot(const std::string &src) struct_tag_typet java_classname(const std::string &id) { if(!id.empty() && id[0]=='[') - return to_struct_tag_type( - to_java_reference_type(*java_type_from_string(id)).base_type()); + { + auto array_type = java_type_from_string(id); + CHECK_RETURN(array_type.has_value()); + return to_struct_tag_type(to_java_reference_type(*array_type).base_type()); + } std::string class_name=id; @@ -1014,6 +1025,7 @@ void get_dependencies_from_generic_parameters( { auto type_from_string = java_type_from_string(signature, erase_type_arguments(signature)); + CHECK_RETURN(type_from_string.has_value()); get_dependencies_from_generic_parameters_rec(*type_from_string, refs); } } @@ -1053,6 +1065,7 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet( { set(ID_C_java_generic_symbol, true); const auto base_type = java_type_from_string(base_ref, class_name_prefix); + CHECK_RETURN(base_type.has_value()); PRECONDITION(is_java_generic_type(*base_type)); const java_generic_typet &gen_base_type = to_java_generic_type(*base_type); INVARIANT(