Java bytecode front-end: fix main method detection#8763
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Java bytecode front-end: fix main method detection#8763tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
When a Java class has multiple methods named 'main' with different signatures, resolve_friendly_method_name reports ambiguity. Fix this by first trying resolve_friendly_method_name, and when it fails for a name without a colon (i.e., potentially a class name rather than a method specification), fall back to looking for the standard main(String[]) entry point directly. This preserves the existing --function ClassName.methodName behavior while fixing the case where config.main is just a class name. Fixes: diffblue#759 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-759-ambiguous-main
branch
from
6afa932 to
073532d
Compare
There was a problem hiding this comment.
Pull request overview
Updates JBMC’s Java entry-point selection to avoid spurious “ambiguous main” conversion errors when the user provides a class name (rather than a fully-qualified method signature), aligning entry-point selection with the Java public static void main(String[] args) convention.
Changes:
- Adjust
get_main_symbolto return a resolved symbol immediately whenresolve_friendly_method_namesucceeds, and otherwise fall back to searching for the standard Java main signature when the input looks like a class name. - Add a regression test based on issue #759 with multiple
mainoverloads to ensure JBMC does not fail conversion due to ambiguity.
Reviewed changes
Copilot reviewed 3 out of 4 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| jbmc/src/java_bytecode/java_entry_point.cpp | Changes main symbol resolution logic; adds class-name fallback to locate the standard Java main signature. |
| jbmc/regression/jbmc/main-method-ambiguity/Test.java | New Java source exhibiting multiple main overloads. |
| jbmc/regression/jbmc/main-method-ambiguity/Test.class | Precompiled class file for the new regression test. |
| jbmc/regression/jbmc/main-method-ambiguity/test.desc | New regression expectations for the ambiguity scenario. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+573
to
580
| // resolve_friendly_method_name failed; if config.main has no colon | ||
| // it may be a class name rather than a method name, so fall back to | ||
| // looking for the standard main method in that class. | ||
| if(config.main.value().find(':') != std::string::npos) | ||
| { | ||
| message.error() << "main symbol resolution failed: " << error_message | ||
| << messaget::eom; | ||
| return main_function_resultt::Error; |
Comment on lines
+573
to
595
| // resolve_friendly_method_name failed; if config.main has no colon | ||
| // it may be a class name rather than a method name, so fall back to | ||
| // looking for the standard main method in that class. | ||
| if(config.main.value().find(':') != std::string::npos) | ||
| { | ||
| message.error() << "main symbol resolution failed: " << error_message | ||
| << messaget::eom; | ||
| return main_function_resultt::Error; | ||
| } | ||
|
|
||
| const symbolt *symbol = symbol_table.lookup(main_symbol_id); | ||
| INVARIANT( | ||
| symbol != nullptr, | ||
| "resolve_friendly_method_name should return a symbol-table identifier"); | ||
| std::string class_name = config.main.value(); | ||
| if(has_suffix(class_name, ".class")) | ||
| class_name.resize(class_name.size() - 6); | ||
|
|
||
| std::string entry_method = "java::" + class_name + "." + JAVA_MAIN_METHOD; | ||
| const symbolt *symbol = symbol_table.lookup(entry_method); | ||
|
|
||
| if(symbol && is_java_main(*symbol)) | ||
| return *symbol; | ||
|
|
||
| return *symbol; // Return found function | ||
| // allow this situation to output symbol table, goto functions, etc | ||
| return main_function_resultt::NotFound; | ||
| } |
| CORE | ||
| Test.class | ||
|
|
||
| ^EXIT=(0|10)$ |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8763 +/- ##
===========================================
- Coverage 80.41% 80.41% -0.01%
===========================================
Files 1703 1703
Lines 188398 188407 +9
Branches 73 73
===========================================
- Hits 151509 151505 -4
- Misses 36889 36902 +13 ☔ 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.
When parsing Java classes with just a class name (without method signature), JBMC was incorrectly using
resolve_friendly_method_namewhich could report 'main method is ambiguous' errors. This fix checks ifconfig.maincontains a method signature (has a colon) and handles simple class names separately by looking for the standard main method signature directly.This aligns the Java front-end with Java's specification, where only
public static void main(String[] args)is recognized as a valid program entry point.Fixes: #759