Make disjuncts in instanceof and virtual method removal stable

regression/goto-diff/java-instanceof/new/Test.java

@@ -0,0 +1,16 @@
+class A {
+}
+
+class B extends A {
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    if (x instanceof A) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+}

regression/goto-diff/java-instanceof/old/Test.java

@@ -0,0 +1,22 @@
+/* 
+old.jar needs to be created by first adding B.class and Test.class and then
+updated to add A.class. This makes the class loader load the classes A and B
+in reverse order.
+*/
+
+class A {
+}
+
+class B extends A {
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    if (x instanceof A) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+}

regression/goto-diff/java-instanceof/test.desc

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\ndeleted functions:
+--
+^warning: ignoring

regression/goto-diff/java-virtual-methods/new/Test.java

@@ -0,0 +1,18 @@
+class A {
+  boolean bar() {
+    return true;
+  }
+}
+
+class B extends A {
+  boolean bar() {
+    return false;
+  }
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    return x.bar();
+  }
+}

regression/goto-diff/java-virtual-methods/old/Test.java

@@ -0,0 +1,24 @@
+/* 
+old.jar needs to be created by first adding B.class and Test.class and then
+updated to add A.class. This makes the class loader load the classes A and B
+in reverse order.
+*/
+
+class A {
+  boolean bar() {
+    return true;
+  }
+}
+
+class B extends A {
+  boolean bar() {
+    return false;
+  }
+}
+
+public class Test {
+
+  public boolean foo(A x) {
+    return x.bar();
+  }
+}

regression/goto-diff/java-virtual-methods/test.desc

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\ndeleted functions:
+--
+^warning: ignoring

src/goto-programs/remove_instanceof.cpp

@@ -87,6 +87,14 @@ std::size_t remove_instanceoft::lower_instanceof(
   std::vector<irep_idt> children=
     class_hierarchy.get_children_trans(target_name);
   children.push_back(target_name);
+  // Sort alphabetically to make order of generated disjuncts
+  // independent of class loading order
+  std::sort(
+    children.begin(),
+    children.end(),
+    [](const irep_idt &a, const irep_idt &b) { // NOLINT
+      return a.compare(b) < 0;
+    });
 
   // Insert an instruction before the new check that assigns the clsid we're
   // checking for to a temporary, as GOTO program if-expressions should

src/goto-programs/remove_virtual_functions.cpp

@@ -445,6 +445,8 @@ void remove_virtual_functionst::get_functions(
         has_prefix(
           id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
         return true;
+      else if(a.symbol_expr.get_identifier() == b.symbol_expr.get_identifier())
+        return a.class_id < b.class_id;
       else
         return a.symbol_expr.get_identifier() < b.symbol_expr.get_identifier();
     });