From 14e087355085aee1ccf332f6f6408da19eea7760 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 29 Nov 2025 20:38:04 +0100
Subject: [PATCH] Fix virtual method resolution for Java Object parameters

The skip condition for avoiding re-processing of already-visited classes
had inverted logic.

Fixes: #930
---
 .../SimpleEquals.class                        | Bin 0 -> 890 bytes
 .../SimpleEquals.java                         |  22 ++++++++++++++++++
 .../equals_Pass.class                         | Bin 0 -> 867 bytes
 .../equals_Pass.java                          |  13 +++++++++++
 .../simple_test.desc                          |   9 +++++++
 .../virtual_equals_object_param/test.desc     |   9 +++++++
 .../remove_virtual_functions.cpp              |   9 ++++---
 7 files changed, 57 insertions(+), 5 deletions(-)
 create mode 100644 jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.class
 create mode 100644 jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java
 create mode 100644 jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.class
 create mode 100644 jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java
 create mode 100644 jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc
 create mode 100644 jbmc/regression/jbmc/virtual_equals_object_param/test.desc

diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.class b/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.class
new file mode 100644
index 0000000000000000000000000000000000000000..3adeca6f588ec63595f35db7c52a7e503e7a57da
GIT binary patch
literal 890
zcmZvaUvJV-7{;GN3x(1NErX$gx;Y(x=J3MAixK0p%^R5}vXIEG3Y<V^X=nfFci{_o
zttQ)|iQfC2G`?pm>og?I={Y^``MuBcoc{Xr?FWDzJXVo_q(Ih?M2aDQY<@6Xw&{#p
zuLs9`7%-&TmSY9a7^GUgmqwZ)IpMbLW}qUgK+~{<8w^_4nx5Ev|9xoMK0{&M^nLCH
zmh1R?mTwMhK4M^f6?y0i3=IV=|I@D<c$PD!emp`HYn}hqY}fk=N(|+AV`tuG-}78g
zMG=zlq^l(FmWJEHl^SqA*t0zHlSY*cd~`i~Br5J|xQA5+T~r)SJU1Lq=EgS`^k1N;
zr{X@=6+F=J5E~4+Slg~mAuyCi+^6QFE2-VU3_{wVMEeZ#t~=s%u46g;RX81R?@+|W
zutaskcL(N4w3er)<q)oRbWO%(Y}@r7L%Kb*qq|bOZs-m93rleH>sPZS<YAS(C+H7g
z`Leh^nk7NGAVp)1R#kd4@wIUV_E{97PNUcc9n6SaX)a3N&|09XhVs%-I$w~Pq0nfa
zA~!?!JBn}5u<}zN5*G*qGR>2a2#|t;3esrMmn_(CR21atAwJzo#BWFZm6%*!NWOHW
zp+t@ZQ35Lwsfo>q^pr>vZRE~z)2MWe%0YAU9Cu=SCDH|IFTo&f1v<P;*%V3Pqbs{l
lE+PPQLp{aX42t{-vh)?1*y21TAtH%{_FQDSMT-Ple*qMHrS<>-

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java b/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java
new file mode 100644
index 00000000000..0bbcfdbcd6f
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/SimpleEquals.java
@@ -0,0 +1,22 @@
+// Simpler test case demonstrating the virtual method resolution bug
+public class SimpleEquals {
+  public static void testDirect() {
+    // Direct call on String - this works
+    String s1 = "hello";
+    String s2 = "hello";
+    assert(s1.equals(s2));
+  }
+
+  public static void testThroughObject(Object o1, Object o2) {
+    // Call through Object parameter - this was failing before the fix
+    assert(o1.equals(o2));
+  }
+
+  public static void main(String[] args) {
+    testDirect();
+    
+    String s1 = "world";
+    String s2 = "world";
+    testThroughObject(s1, s2);
+  }
+}
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.class b/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.class
new file mode 100644
index 0000000000000000000000000000000000000000..5246bc17974423f8f8c300f9d953c890155105f0
GIT binary patch
literal 867
zcmZuv-*3`T7(JI3+O?e&*nrL9&*^~T_Mk6@WpSDFMW!a0CBp|(%FWVQinhhXf5LZp
zUwrXJO~ANB-}d0&q{i<816<a${l0tech5QBx%b!K?>_)+V_icGk^<R490>;V$bM^Y
zc(#AI@w9oworoc^>H2Q8#UK?+`=VSmFb9nm_?xcng$#?u+WBqOQbU39A6`8QT>ntT
zB|@^Bjs_j3U`?F^7}Zrv`*X-(LBXPdEOHF`i0<VxJ0#A`Dg_=yZpRNFx}n|lc#DBG
z1gxrHnIS*bw0%~(8w8y|!xAKozzYVh;3|XKez!YrW$l7iE^1E0b=**J)4(cjF(jv4
zJKj)Vw#7p?;H?RDJ+h-N2`3jD4DwE=#c5y7_4$)-yUBy+q6LO|s&iiL*{{cAxox{X
zL$>&0M#jV<(!S|<<MYw#oo?XpN3OszXWUvB>PT>g4i8{vUKmQ53?@#U{<mpVpvWl3
z%LA~_q7ZBJ7t12ogjW<rX_bHkRIY3tBUwJB&+0?@07d=?S^7jvv6;;hiZqjel#(7W
zx;rJ5$3X8PkqV%80{tL8KOjRU+1?kVdswk5$H-Zy(5*@z`5yEWEFBDR`KML+hLx>h
zQL->IFQkvymx&WlNV<vz;=N1ReYziyVGI?Skp93@po{mnxMM1;i68e!qj*y3Odr>J
Z<KDg^Jta8vMzj}4%%JWVDl~}U&OgW4spJ3v

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java b/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java
new file mode 100644
index 00000000000..e5a9f365b6c
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/equals_Pass.java
@@ -0,0 +1,13 @@
+public class equals_Pass {
+  private static boolean myEquals(Object a, Object b) {
+      return (a == b) || (a != null && a.equals(b));
+  }
+
+  public static void main(String[] args) {
+    String a = new String("abc");
+    String b = new String("abc");
+    assert((a == b) || (a != null && a.equals(b)));  // This passes
+    boolean result = myEquals(a, b);
+    assert(result);  // This fails
+  }
+}
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc b/jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc
new file mode 100644
index 00000000000..2e69d6649e8
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/simple_test.desc
@@ -0,0 +1,9 @@
+CORE
+SimpleEquals.class
+--function SimpleEquals.main
+^EXIT=0$
+^SIGNAL=0$
+^\[SimpleEquals.testDirect.assertion.1\] line 6 .*: SUCCESS$
+^\[SimpleEquals.testThroughObject.assertion.1\] line 11 .*: SUCCESS$
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc/virtual_equals_object_param/test.desc b/jbmc/regression/jbmc/virtual_equals_object_param/test.desc
new file mode 100644
index 00000000000..2abada22906
--- /dev/null
+++ b/jbmc/regression/jbmc/virtual_equals_object_param/test.desc
@@ -0,0 +1,9 @@
+CORE
+equals_Pass.class
+--function equals_Pass.main
+^EXIT=0$
+^SIGNAL=0$
+^\[equals_Pass.main.assertion.1\] line 9 .*: SUCCESS$
+^\[equals_Pass.main.assertion.2\] line 11 .*: SUCCESS$
+--
+^warning: ignoring
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 21d96041a1e..9b3d502c0b7 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -518,13 +518,12 @@ void get_virtual_calleest::get_child_functions_rec(
   for(const auto &child : findit->second.children)
   {
     // 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"))
     {
       continue;
     }