Skip to content

Java bytecode front-end: do not crash upon invalid class names #8764

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
tautschnig wants to merge 1 commit into
base: develop
Choose a base branch
from
Draft

Java bytecode front-end: do not crash upon invalid class names #8764

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
38 changes: 29 additions & 9 deletions jbmc/src/java_bytecode/java_bytecode_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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: {}
Expand Down Expand Up @@ -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);
}
}

Expand All @@ -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)
Expand All @@ -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);
}
}
}
Expand Down Expand Up @@ -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<symbol_exprt>(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<array_exprt>(value))
{
Expand Down Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/java_entry_point.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
37 changes: 25 additions & 12 deletions jbmc/src/java_bytecode/java_types.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -624,10 +624,14 @@ std::optional<typet> 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<typet> param_types =
parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
Expand All @@ -648,10 +652,14 @@ std::optional<typet> 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
Expand Down Expand Up @@ -681,11 +689,11 @@ std::optional<typet> 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':
{
Expand Down Expand Up @@ -781,13 +789,13 @@ std::vector<typet> 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);
Expand All @@ -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;

Expand Down Expand Up @@ -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);
}
}
Expand Down Expand Up @@ -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(
Expand Down
Loading