From 5524078e409c30b613b1e1f5a6445c9d67c23bb7 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 21 Nov 2017 08:34:51 +0000
Subject: [PATCH 1/4] Correct class_id of nondet strings

This could cause problems in particular in the use of instanceof.
---
 src/java_bytecode/java_object_factory.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 2d443a2e890..5c05b26c295 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -554,7 +554,7 @@ codet initialize_nondet_string_struct(
 
   // `obj` is `*expr`
   const struct_typet &struct_type = to_struct_type(ns.follow(obj.type()));
-  const irep_idt &class_id = struct_type.get_tag();
+  const irep_idt &class_id = "java::" + id2string(struct_type.get_tag());
 
   // @clsid = String and @lock = false:
   const symbol_typet jlo_symbol("java::java.lang.Object");

From 12ca989950e6b108974bf7424121e239c46cbabf Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 21 Nov 2017 08:36:15 +0000
Subject: [PATCH 2/4] Document class_identifier argument of root class

This can prevent mistake in forgetting the "java::" prefix.
---
 src/java_bytecode/java_root_class.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/java_bytecode/java_root_class.cpp b/src/java_bytecode/java_root_class.cpp
index cbeec3ff40d..4c2d98b43b9 100644
--- a/src/java_bytecode/java_root_class.cpp
+++ b/src/java_bytecode/java_root_class.cpp
@@ -57,7 +57,8 @@ void java_root_class(symbolt &class_symbol)
 /// \param jlo [out] : object to initialize
 /// \param root_type: type of the root class
 /// \param lock: lock field
-/// \param class_identifier: class identifier field
+/// \param class_identifier: class identifier field, generally begins with
+///        "java::" prefix.
 void java_root_class_init(
   struct_exprt &jlo,
   const struct_typet &root_type,

From 10d3857ce0b01d8c9ad76b8e9d1c4cc2b1eef3db Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 21 Nov 2017 08:45:51 +0000
Subject: [PATCH 3/4] Add test for instanceof String

This checks the bug with class identifier of nondet strings was fixed.
---
 regression/jbmc-strings/instanceof/Test.class | Bin 0 -> 602 bytes
 regression/jbmc-strings/instanceof/Test.java  |   9 +++++++++
 regression/jbmc-strings/instanceof/test.desc  |   8 ++++++++
 3 files changed, 17 insertions(+)
 create mode 100644 regression/jbmc-strings/instanceof/Test.class
 create mode 100644 regression/jbmc-strings/instanceof/Test.java
 create mode 100644 regression/jbmc-strings/instanceof/test.desc

diff --git a/regression/jbmc-strings/instanceof/Test.class b/regression/jbmc-strings/instanceof/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..052fc84e52143ccdcc56f4f160a00b24ee7b21e2
GIT binary patch
literal 602
zcmZXQO;6iE5Qg9JN7gY0g82&NBS51HB2g~ficnF26O=;`65JeT1tzXt*-n2<{y?u#
zB#@{C;)KMHs+cuN5Up04oqc!q*>~po@7+Cs4ODH|n6^+Z!orNe2Z31|rjq6a=4~vX
zBCtppuX<@JlPrj%bSFr?W++<(Iwce~gDA+h2>QzEF~O+EElC*N4<h-k^SvpPBUMZ=
z{d4KJ37=N>FT9`Ldgw)G>y0c4qO&in|4W47M&|kL1Mf!<U~T$g?<>0zcM@Oj1qxg|
zl4<r?F&zwJge^p!Fmx~khfw<WFGBfE+V1zXn<Q~Uu%b9xQ?D7Kr~*q4mhtf&=dgJp
z{ft|D<J3c*4q>V#(;$(p0hT++I()&SImHr>*ygEIsjR$lrh~i02**)A&GSyYo3&fe
zl`2GuV<8v0O^m_iT$LU`%hgKl2?bZX{0+SexAq95i=jU-Pi|3oaK$B;YB|J(!MVZ9
zgka<x$MIaz#02}A7`WKT!N8bn-JsZoFn+<%uc0ePudu!&1u&sGUzP94{CesIzL0a&

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/instanceof/Test.java b/regression/jbmc-strings/instanceof/Test.java
new file mode 100644
index 00000000000..c01fcccf084
--- /dev/null
+++ b/regression/jbmc-strings/instanceof/Test.java
@@ -0,0 +1,9 @@
+public class Test {
+
+    public static String check(String s) {
+        if (s == null)
+            return "null";
+        assert(s instanceof String);
+        return "non-null";
+    }
+}
diff --git a/regression/jbmc-strings/instanceof/test.desc b/regression/jbmc-strings/instanceof/test.desc
new file mode 100644
index 00000000000..3c597735589
--- /dev/null
+++ b/regression/jbmc-strings/instanceof/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --function Test.check
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 6 .* SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--

From ac2a5998c05a3d92289754431659ed3a0a8c4d38 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 21 Nov 2017 10:18:10 +0000
Subject: [PATCH 4/4] Correct unit test for gen_nondet_string

The "java::" prefix was missing from the previous implementation and
this is now fixed.
---
 .../java_object_factory/gen_nondet_string_init.cpp              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
index 3d2dc659b3c..b410805e488 100644
--- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
+++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
@@ -79,7 +79,7 @@ SCENARIO(
           "return_array = cprover_associate_length_to_array_func"
           "(nondet_infinite_array, tmp_object_factory);",
           "arg = { .@java.lang.Object={ .@class_identifier"
-          "=\"java.lang.String\", .@lock=false },"
+          "=\"java::java.lang.String\", .@lock=false },"
           " .length=tmp_object_factory, "
           ".data=nondet_infinite_array };"};