From 2080cd37bc3db0f4fc947240961eccdf4e651373 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 9 Jan 2018 15:16:05 +0100
Subject: [PATCH 1/2] Complete instanceof for Java.

The current implementation did not consider correctly the case of `null` in
`ID_java_instanceof`. An instanceof with `null` always fails. For `a instanceof
B` this now adds `a != null` to the condition.
---
 src/goto-programs/remove_instanceof.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index b893c38b0ff..0e0999cf0d0 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -113,7 +113,12 @@ std::size_t remove_instanceoft::lower_instanceof(
   newinst->source_location=this_inst->source_location;
   newinst->function=this_inst->function;
 
-  // Replace the instanceof construct with a big-or.
+  // Replace the instanceof construct with a conjunction of non-null and the
+  // disjunction of all possible object types. According to the Java
+  // specification, null instanceof T is false for all possible values of T.
+  // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
+  notequal_exprt non_null_expr(
+    check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type())));
   exprt::operandst or_ops;
   for(const auto &clsname : children)
   {
@@ -121,7 +126,7 @@ std::size_t remove_instanceoft::lower_instanceof(
     equal_exprt test(newsym.symbol_expr(), clsexpr);
     or_ops.push_back(test);
   }
-  expr=disjunction(or_ops);
+  expr = and_exprt(non_null_expr, disjunction(or_ops));
 
   return 1;
 }

From 9c457b7912faeed5c77baaf12a2ff78a53877f1e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 10 Jan 2018 09:07:04 +0100
Subject: [PATCH 2/2] Add regression test for null instanceof.

---
 .../cbmc-java/instanceof8/InstanceOf8.class       | Bin 0 -> 716 bytes
 regression/cbmc-java/instanceof8/InstanceOf8.java |  14 ++++++++++++++
 regression/cbmc-java/instanceof8/test.desc        |   7 +++++++
 3 files changed, 21 insertions(+)
 create mode 100644 regression/cbmc-java/instanceof8/InstanceOf8.class
 create mode 100644 regression/cbmc-java/instanceof8/InstanceOf8.java
 create mode 100644 regression/cbmc-java/instanceof8/test.desc

diff --git a/regression/cbmc-java/instanceof8/InstanceOf8.class b/regression/cbmc-java/instanceof8/InstanceOf8.class
new file mode 100644
index 0000000000000000000000000000000000000000..24568fd857fd8fd53e628b1ffd85e1d254d01f21
GIT binary patch
literal 716
zcmZWmT~8B16g{&$+wFeP4-jlc6cn-WAkpw(0x=rYqzTGH4GHMWb~`o;Wol-({ulZO
zeBnh+tdT_Ht3S$kZ$sH8?!(NzbI(2Jp1Xhk{`d)C3-^8asJpn~p@>DFj+-u)d^o84
zuyD)8Z6C{6adAgrZZ%3%WwNBN)8|PVwR@@~AdUnIJBd!RCjxe3{XjtO_B%?Tyq9S8
zdT`oS<_&|Xkf}5iSZM4WM<1ijUZlI5O`WN(GTZCKGt<hV_~cdeVS+!663zIxQw^=m
zB)YrJLdBi9cd6{R`U4ZImkH}snmWxQ9jpEKj~}p9h#8aws{hG`2oQ#-VpgD*SD#Ic
zzA&b5xcja^FvaR(HN-uvkyhTd-#%6``IC(%Pgl+>yFFSR8R@7rF{*P#Pkyrj6=-iq
zSfTa%^jk!w##2!wK|4W-&N5|7bPKwjjS<9W2BJb|Vf-lIu?vbBx<xlbgN@&?&fv&%
z`<zm1+)#o|u??5_J!+pDXTqc88s;w<-VuNq9({p5r0sl%JVS5+=Wv9=ukmC30@k4%
z!KK<TukmElLIH7xct}QANWz+5B%=#gws=<ls<Xv!@P=^ZCrJA%?3`#~kqI1F;Zt^Z
Ioe~SRf7^M2TL1t6

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/instanceof8/InstanceOf8.java b/regression/cbmc-java/instanceof8/InstanceOf8.java
new file mode 100644
index 00000000000..1d5abbf33f0
--- /dev/null
+++ b/regression/cbmc-java/instanceof8/InstanceOf8.java
@@ -0,0 +1,14 @@
+public class InstanceOf8 {
+  public static boolean test(Integer i) {
+    if (i instanceof Integer) {
+      return true;
+    } else {
+      return false;
+    }
+  }
+  public static void main(String[] args)
+  {
+    assert(!test(null));
+    assert(test(new Integer(1)));
+  }
+}
diff --git a/regression/cbmc-java/instanceof8/test.desc b/regression/cbmc-java/instanceof8/test.desc
new file mode 100644
index 00000000000..21d65c684aa
--- /dev/null
+++ b/regression/cbmc-java/instanceof8/test.desc
@@ -0,0 +1,7 @@
+CORE
+InstanceOf8.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--