Fix virtual method resolution for Java Object parameters#8759
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Fix virtual method resolution for Java Object parameters#8759tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
The skip condition in get_child_functions_rec for avoiding re-processing of already-visited classes had inverted logic. The original code skipped children with no resolved symbol (unresolved entries), preventing them from being re-visited. The fix only skips children that have a concrete non-Object implementation, allowing unresolved entries and Object-resolved entries to be re-visited. The regression test uses a custom class with an overridden toString() method called through an Object parameter, verifying that the virtual dispatch correctly resolves to the subclass implementation. The original test from issue diffblue#930 (String.equals) cannot be used as a regression test because JBMC's String model does not support proving equality of String objects through the equals() method. Fixes: diffblue#930 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-930-virtual
branch
from
14e0873 to
4006e98
Compare
There was a problem hiding this comment.
Pull request overview
Fixes JBMC’s Java virtual-call callee discovery so classes previously visited with an unresolved/java.lang.Object target aren’t prematurely skipped, which could prevent resolving the correct override when dispatching through Object-typed receivers/parameters (issue #930).
Changes:
- Correct the “already visited” skip condition in
get_child_functions_recto only skip when a prior visit resolved to a non-java.lang.Objectimplementation. - Add a JBMC regression test for virtual dispatch through an
Object-typed parameter, including the corresponding.descand compiled.classartifacts.
Reviewed changes
Copilot reviewed 3 out of 5 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
src/goto-programs/remove_virtual_functions.cpp |
Fixes inverted skip logic in virtual callee traversal to enable correct resolution beyond java.lang.Object. |
jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc |
Adds a new regression driver for the Java test. |
jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java |
Adds a Java regression program exercising virtual dispatch via an Object-typed parameter. |
jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.class |
Compiled bytecode for the new regression. |
jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals$MyClass.class |
Compiled bytecode for the nested class in the new regression. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
520
to
+526
| // Skip if we have already visited this and we found a function call that | ||
| // did not resolve to non java.lang.Object. | ||
| // resolved to a non-Object implementation (i.e., we don't need to revisit). | ||
| auto it = entry_map.find(child); | ||
| if( | ||
| it != entry_map.end() && | ||
| (!it->second.symbol_expr.has_value() || | ||
| !it->second.symbol_expr->get_identifier().starts_with( | ||
| "java::java.lang.Object"))) | ||
| it != entry_map.end() && it->second.symbol_expr.has_value() && | ||
| !it->second.symbol_expr->get_identifier().starts_with( | ||
| "java::java.lang.Object")) |
Comment on lines
+6
to
+20
| public String toString() { | ||
| counter++; | ||
| return "MyClass"; | ||
| } | ||
| } | ||
|
|
||
| public static void testDirect() { | ||
| MyClass m = new MyClass(); | ||
| m.toString(); | ||
| assert(counter == 1); | ||
| } | ||
|
|
||
| public static void testThroughObject(Object o) { | ||
| // Virtual call through Object parameter should resolve to MyClass.toString | ||
| o.toString(); |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8759 +/- ##
========================================
Coverage 80.41% 80.41%
========================================
Files 1703 1703
Lines 188398 188397 -1
Branches 73 73
========================================
Hits 151498 151498
+ Misses 36900 36899 -1 ☔ 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.
The skip condition for avoiding re-processing of already-visited classes had inverted logic.
Fixes: #930