Java bytecode front-end: do not crash upon invalid class names#8764
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Java bytecode front-end: do not crash upon invalid class names#8764tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
Do not make unchecked use of the result of `java_type_from_string`. Where `java_type_from_string` returns an empty optional for malformed type descriptors, either throw an `unsupported_java_class_signature_exceptiont` (in the parser, where it is caught and reported as an error) or use `CHECK_RETURN` to fail with a clear diagnostic instead of undefined behavior. Fix build errors: use `what()` instead of `str()` on the exception (which inherits from `std::logic_error`), and use the renamed variable `method_type_opt` consistently. Fixes: diffblue#728 Fixes: diffblue#849 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-728-jbmc-core-dump
branch
from
5e633f1 to
67824f0
Compare
There was a problem hiding this comment.
Pull request overview
This PR aims to prevent JBMC’s Java bytecode front-end from crashing on malformed/invalid class/type names by avoiding unchecked dereferences of java_type_from_string results and by adding an explicit error-handling path in the parser.
Changes:
- Add exception throwing for some malformed signatures in
java_type_from_stringand add additional checks around recursive parsing results. - Add handling for
unsupported_java_class_signature_exceptiontinjava_bytecode_parsert::parse(). - Replace several
*java_type_from_string(...)dereferences with intermediate optionals + validation in parser/converter code.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 16 comments.
| File | Description |
|---|---|
| jbmc/src/java_bytecode/java_types.cpp | Adds additional validation/exception behavior when parsing descriptors/signatures and refactors some call sites to avoid direct dereference. |
| jbmc/src/java_bytecode/java_entry_point.cpp | Adds a return-value check when constructing the String[] type used to recognize main. |
| jbmc/src/java_bytecode/java_bytecode_parser.cpp | Replaces direct dereferences of parsed types with optionals + checks, and adds a catch for unsupported signature exceptions. |
| jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | Avoids direct dereference when converting field descriptors by introducing an optional + check. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+822
to
+823
| CHECK_RETURN(array_type.has_value()); | ||
| return to_struct_tag_type(to_java_reference_type(*array_type).base_type()); |
Comment on lines
+581
to
584
| auto type_opt = java_type_from_string(method.descriptor); | ||
| CHECK_RETURN(type_opt); | ||
| get_class_refs_rec(*type_opt); | ||
| } |
| *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()); |
Comment on lines
+557
to
560
| auto type_opt = java_type_from_string(field.descriptor); | ||
| CHECK_RETURN(type_opt); | ||
| get_class_refs_rec(*type_opt); | ||
| } |
| 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()); |
Comment on lines
+681
to
+683
| auto type_opt = java_type_from_string(f.descriptor); | ||
| CHECK_RETURN(type_opt.has_value()); | ||
| field_type = *type_opt; |
Comment on lines
660
to
663
| 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. |
Comment on lines
+1028
to
1029
| CHECK_RETURN(type_from_string.has_value()); | ||
| get_dependencies_from_generic_parameters_rec(*type_from_string, refs); |
Comment on lines
1067
to
1070
| 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); |
Comment on lines
+89
to
+90
| CHECK_RETURN(type_opt.has_value()); | ||
| return std::move(*type_opt); |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8764 +/- ##
========================================
Coverage 80.41% 80.42%
========================================
Files 1703 1703
Lines 188398 188426 +28
Branches 73 73
========================================
+ Hits 151509 151539 +30
+ Misses 36889 36887 -2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Do not make unchecked use of the result of
java_type_from_string.Fixes: #728
Fixes: #849