From 3afff86e97c96128c005052cf86be9d2e52ea52b Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 15 Apr 2018 17:20:21 +0100
Subject: [PATCH 1/3] Make disjuncts in virtual method removal independent of
 class loading

The disjuncts created by virtual method removal depended
on the class loading order, causing goto-diff to think that
there was a change in the classes.
---
 src/goto-programs/remove_virtual_functions.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index fad271b0d27..f3b53c57a9b 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/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();
     });

From b44589e6bebf64b7222ba3f4059135cb6a0955c8 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 16 Apr 2018 16:09:05 +0100
Subject: [PATCH 2/3] Make disjuncts in instanceof removal independent of class
 loading

The disjuncts created by instanceof removal depended
on the class loading order, causing goto-diff to think that
there was a change in the classes.
---
 src/goto-programs/remove_instanceof.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index 50166e33d03..e859c8d9384 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/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

From 4222a940748523f075d8a15bb4e10275f12dfcc9 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 15 Apr 2018 17:54:59 +0100
Subject: [PATCH 3/3] Regression tests for unstable instanceof and virtual
 method disjuncts

---
 regression/goto-diff/java-instanceof/new.jar  | Bin 0 -> 1184 bytes
 .../goto-diff/java-instanceof/new/Test.java   |  16 ++++++++++++
 regression/goto-diff/java-instanceof/old.jar  | Bin 0 -> 1179 bytes
 .../goto-diff/java-instanceof/old/Test.java   |  22 ++++++++++++++++
 .../goto-diff/java-instanceof/test.desc       |  10 ++++++++
 .../goto-diff/java-virtual-methods/new.jar    | Bin 0 -> 1215 bytes
 .../java-virtual-methods/new/Test.java        |  18 +++++++++++++
 .../goto-diff/java-virtual-methods/old.jar    | Bin 0 -> 1217 bytes
 .../java-virtual-methods/old/Test.java        |  24 ++++++++++++++++++
 .../goto-diff/java-virtual-methods/test.desc  |  10 ++++++++
 10 files changed, 100 insertions(+)
 create mode 100644 regression/goto-diff/java-instanceof/new.jar
 create mode 100644 regression/goto-diff/java-instanceof/new/Test.java
 create mode 100644 regression/goto-diff/java-instanceof/old.jar
 create mode 100644 regression/goto-diff/java-instanceof/old/Test.java
 create mode 100644 regression/goto-diff/java-instanceof/test.desc
 create mode 100644 regression/goto-diff/java-virtual-methods/new.jar
 create mode 100644 regression/goto-diff/java-virtual-methods/new/Test.java
 create mode 100644 regression/goto-diff/java-virtual-methods/old.jar
 create mode 100644 regression/goto-diff/java-virtual-methods/old/Test.java
 create mode 100644 regression/goto-diff/java-virtual-methods/test.desc

diff --git a/regression/goto-diff/java-instanceof/new.jar b/regression/goto-diff/java-instanceof/new.jar
new file mode 100644
index 0000000000000000000000000000000000000000..bc067de9a6aacfd63b49bdc8e13d69931683614a
GIT binary patch
literal 1184
zcmWIWW@Zs#;Nak3Fz)X6VL$?$3@i-3t|5-Po_=on|4uP5Ff#;rvvYt{FhP|C;M6Pv
zQ~}rQ>*(j{<{BKL=j-;__snS@Z(Y5MyxzK6=gyqp9At3C_`%a6JuhD!Pv48Bt5`TA
zUPvC1o+YK3@k3ly?fDWdi|68^PsCNHF<j05RP?ck5$uY*T`Ej2Ks#K47~u*{G%v6N
zWgYdBa}tY-t-t19w_{^t6K0FkV@qSxD`U$mW0P}ZGn;*8&lw?WH?}n1vj%Q#V$c6f
z32|eqn}23c$o@-rmRwmh;m8u11svf8b(w)htD@C94ogmoidi&$YQ(e?hYuV&aO%W?
z7bi|AFg$wwT;<u)*T2<Mm#R%S&@eDyT+77hrog7faw*4Qn$85a&J9_)=?Ql@rlqk@
z%1LmXAi_Q&E$IOZ*f)~?Dm62KZrx1KH%_$o4a<=}9xfgqhs}-+f*p-U4zqYqOk%yH
zAQ-mxEl-d1!Aox(Ch@N7nb^qeVQg5y1a|+rwDP2Gpxc+=bw3wSHYByU1mXo<KU;q$
zN0B+@@vmiN7VK@6^-$uKZEKkk(I_Usy?bx5>G9*Tjfejqs$a0sXrsZ#ukM2B`g@Yn
z?(dm-^55Kj^$cGMMGrbVFI;&cXom>P_sDruof~hz+rzP^{n1&DS&wzh{db2ZnHkU3
zS-IoAt7Cb!jZ{e->&GouUM4NN{=C>kw`}$mo3t{{^t9-EXTL6Aci3HFg5d168X1v0
zw_o|`{@!xt>@7!lWB#4&W8PS|=uw%k*rxj5td^e?cPOw;UD2VqX!BP8vJ+e1>CdsP
zdH+Cem7R3P2Kg;oS0p++7bqzje?2AgpBa=}{CgvW9|8R>#|TQNj7%a7sF@9xlR%jb
z6~J>3DC?nXMNa;ptcC!#Kqg!(QpQ6z0hCRUlN>0UAi!ZD6PjtzH6h0{s-}rR|3T9x
ix+dfx03`tg2n6~bkst!RS=m5xtUxFaG%lMN!~+0P23?*2

literal 0
HcmV?d00001

diff --git a/regression/goto-diff/java-instanceof/new/Test.java b/regression/goto-diff/java-instanceof/new/Test.java
new file mode 100644
index 00000000000..0bd39087a0b
--- /dev/null
+++ b/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;
+    }
+  }
+}
diff --git a/regression/goto-diff/java-instanceof/old.jar b/regression/goto-diff/java-instanceof/old.jar
new file mode 100644
index 0000000000000000000000000000000000000000..25aba503dd7a55e674cda857c9db88e9f0db1b58
GIT binary patch
literal 1179
zcmWIWW@Zs#;Nak3nAqFz!+-=h8CV#6T|*poJ^kGD|D9rBU}gyLX6FE@V1g<Oz^PdT
zr~<Cp*U`_@%{4eg&)4m<@0rs+-nx1hdA)VD&Yd~GImqCO@q?#DdS1Rdp1v1LSFvzL
zypTL1JxfY6<A=Da+Vdq^7SF{+pNOkYW4N0Aspw-7BiI#ryHuE5fOfb7F~SwqXkK6k
z$~x&K=Oh*vTYt^JZpX&PCd?M6$Ck#XSH_lC#wO>+W;XlGo-;z$Zft41XARug#Ge0|
z65_^IH~-9@ko}kLEV;61!jUC13pm0H>M{e1Rz<6I9G09E6|-pi)QD*(4j(vl;M9o&
zFIbNB@o@3@IBa%o5bS6)a+t+?ViM~m1;MbjZ+Uv84_<oXFo{=(W6~prOFlevz|Mbj
zN<p{_=(r_#ozDf74M{C7f%rhzZ?E5B1BpHQeo2%59XfYmEo-OVT?da))n!c1T5WlL
z1{zCMRxH`W{r<vI;UIREFgdQmzDEzwmG86u`ThL|-h`&f5_Y?!Y<u?|+o-VTRQH};
zVk;iLaC~t7l)Ltev!4&$%Z(4-9XX@K*WGri>gB^fzZ7i|DVcOCMSuIVwUvF7i*}!U
z<NMBK%ZB$?kDjWTVaC+LG_&aD%%**tk7ozl^uND6^{f`pf*<PTHXWyhO|NQ3o;Y|@
zJmq}%gAR#n%lvx;%rA1@RNj8B{z0wMhw`lO_dA`Y|4#4;-s#ot<)~D4t8~R@eo*R?
zYU#Ip2=ulbBXYbpV~JNsYRBud6)2H<;)DXjqu0+>o-KX-TRnBD+H?aA0|UmljErsy
zY+5XravY}VOknHWkd>RBaED`B8vCT21jh*?>=V+G9<YGp_}BVldDDPi*#M4XMkWyk
z)O-fZM4)_z3g8(Bl<NY#QMDqcd{8b!09zmvt`#ZIA)5foA;^gjltU2UFpvq&FX)<(
uBL<W%5ugbeRftrItPd1z$f1C0*=%3{KqE20o0Sb@AS)2c1C2{#2Jrx!#A~Vm

literal 0
HcmV?d00001

diff --git a/regression/goto-diff/java-instanceof/old/Test.java b/regression/goto-diff/java-instanceof/old/Test.java
new file mode 100644
index 00000000000..6ec791ae253
--- /dev/null
+++ b/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;
+    }
+  }
+}
diff --git a/regression/goto-diff/java-instanceof/test.desc b/regression/goto-diff/java-instanceof/test.desc
new file mode 100644
index 00000000000..9e5863b5a5e
--- /dev/null
+++ b/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
diff --git a/regression/goto-diff/java-virtual-methods/new.jar b/regression/goto-diff/java-virtual-methods/new.jar
new file mode 100644
index 0000000000000000000000000000000000000000..5c9c5990a03b79dbd8f63f108808ca47be4f8ff7
GIT binary patch
literal 1215
zcmWIWW@Zs#;Nak3nA+Fx!+-=h8CV#6T|*poJ^kGD|D9rBU}gyLX6FE@V1g<Oz^PdT
zr~<Cp*U`_@%{4eg&)4m<@0rs+-nx1hdA)VD&Yd~GImqCO@q?#DdS1Rdp1v1LSFvzL
zypTL1JxfY6<A=Da+Vdq^7SF{+pNOkYW4N0Aspw-7BiI#ryHuE5fOfb7F~SuS(Y(M8
zly%fg&PgmTw*H!b-HwfoO_;4tk1dT&u8b|NjLpuC&209WJ!gch-PqE2&l<R~i9P=_
zCB%)bZvL4)A^R`gS#o93gd<C27H|{?B?(3ZiYPOO7u0127Ojd_^Jp?w*}B6;Uwfm@
z#P-J4#;Fq<FHW53$Z+KPdCxQ6*T4Ip^77S73`j^|isEMSao`C#!LUX8#3a^BJr1)%
zv#psQyD2nJY?Srb)X3^Mqq$LdRS4IrDV?djv#in-PO_TKk_P+pfs%pSW}q*g6ZEGO
z9sSAKAuA~&F{9yI1B0*tbE-tcG{(qH4zmP3HfQCgC*0vkF)-S|>}j?^q2uVm1Dv5+
ztf8ll>|yhj^<Wjhk&y@X*z`Ak6-$7gx`EeYTtL~7)Z!9|-(vlC^Dzbr*ls?pm%TA=
zsnhd`7hZIvC<k(~2EKS#bdqcL$*P*EZqAE7Fxq*Yx$EUqnD%VWWaH2OY~mSqt%&eY
z$X0CM!+G4LG2zSK1NOWeReLuosI)zd68e;EKVkCcgOe}DR8*&Z@s-%L+pes-SM}hm
z*5?_j?)xrXDz3EITK-5WM<sEF#x0G7XEMDMEWBR5aozCNXYbq?LsvcbDy6RXdV$U7
z=C8cupw)cw$=XwMcc{<iztGF>)OE4rq)xKbwf@lHYu99NeLermAnj4fZ*EX#I@orR
z<s8tDyo{h^%*Z6dfSMO!84Z*dQ2{)2fpR9gR^;3P%83YI3uMBzBIQeD6F|8LIo*MB
z5ds_rGNE}2T@!MgqH0<V^dB^VqH9790#I}#Knu|Kh{zA{W@Q7(u>zqy(6}yU5Dx&*
CgJ%2y

literal 0
HcmV?d00001

diff --git a/regression/goto-diff/java-virtual-methods/new/Test.java b/regression/goto-diff/java-virtual-methods/new/Test.java
new file mode 100644
index 00000000000..a048bc7cf61
--- /dev/null
+++ b/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();
+  }
+}
diff --git a/regression/goto-diff/java-virtual-methods/old.jar b/regression/goto-diff/java-virtual-methods/old.jar
new file mode 100644
index 0000000000000000000000000000000000000000..fdea5e45df83ca4d110a6075f9bada90768ab6ff
GIT binary patch
literal 1217
zcmWIWW@Zs#;Nak3=<MtFVL$?$3@i-3t|5-Po_=on|4uP5Ff#;rvvYt{FhP|C;M6Pv
zQ~}rQ>*(j{<{BKL=j-;__snS@Z(Y5MyxzK6=gyqp9At3C_`%a6JuhD!Pv48Bt5`TA
zUPvC1o+YK3@k3ly?fDWdi|68^PsCNHF<j05RP?ck5$uY*T`Ej2Ks#K47~zT*G%v6N
zWu5era}tY-t-t19w_{^t6K1Q^V@qR`D`Sf*W3zK(Gn;*8&lw?WH?}n1vj%Q#V$c6f
z32|eqn}23c$o@-rmRwmh;m8u11sugeNrDl9BFfC+1$CK$MXRFKJerJEw(fAz*WRcz
zvAwaiaq7gzi<}*@k|Gi_8oo6!2n#T$N;FJkjNIffOVDF;R&IL29gY+OqYccSW*Zdr
z1&R#{oThp?PBk)I?-+cXUuEY3w_->D=ecaPSO#?X4ZL3C0?LM@7MDPL7wfm1k1<fd
zcJpby?7i}Hot{s;@S?*-Wfd=L;EQ)fC%JZ?tg4yn=Dg?wqn+28yIwwpY0u_NHvat2
zCZ1uJMs$Z_u440=&N-bn2VYe0E0+@ZQkCr3(c83DB}Ml9^vRzOPJI}&qdM)2ufT@g
z?|7<vRS(W$eO{n?eBPx=#g#T&%O5G_97&v^aYJL#kxVazCsVH6<gULxbC>nbq^>rZ
zmt6+CcDwLe)i3j6UdiJ&dAnBmBe{G#2Xi?NPB&$x?jFww`!L_g=<<x~_Svn5qDybb
zgOb^^{B!@#0sY9!NGO6G=@`KiCpt15xqjaBjQ92L{-?Zr^%4UT5}2a6nS300LQXJj
zkv=hr^-_<+tk7(0=ErUd%@Z4CJvKG6I_mJT`K<`jToI%;%{1ecgVqjsY@dznD%}k9
z=W}puGct)VpyozcRs-cmQ~=Ljpu8F2jj9zne}M8L0@wnXaIHu=6WIh%K0;20pnQY?
zhk;CJu0q#@9BZHyiU9L~@rX#T==zXD0oAf4zyN^8aDX=}8^}ObAe09h*TW3r0RTyL
BVeJ3_

literal 0
HcmV?d00001

diff --git a/regression/goto-diff/java-virtual-methods/old/Test.java b/regression/goto-diff/java-virtual-methods/old/Test.java
new file mode 100644
index 00000000000..41b3d813c18
--- /dev/null
+++ b/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();
+  }
+}
diff --git a/regression/goto-diff/java-virtual-methods/test.desc b/regression/goto-diff/java-virtual-methods/test.desc
new file mode 100644
index 00000000000..9e5863b5a5e
--- /dev/null
+++ b/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