From 17d230ffaff21c4e036006d999d3024a64fd1779 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 23 Nov 2017 10:46:17 +0000
Subject: [PATCH 1/3] Fix String.equals to check for class identifier

---
 .../java_string_library_preprocess.cpp        | 27 ++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 452c59e0ddb..1da4340e163 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -913,7 +913,6 @@ codet java_string_library_preprocesst::make_equals_function_code(
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
 {
-  // TODO: Code should return false if Object is not String.
   code_blockt code;
   exprt::operandst ops;
   for(const auto &p : type.parameters())
@@ -923,8 +922,30 @@ codet java_string_library_preprocesst::make_equals_function_code(
   }
   exprt::operandst args=process_equals_function_operands(
     ops, loc, symbol_table, code);
-  code.add(code_return_function_application(
-    ID_cprover_string_equal_func, args, type.return_type(), symbol_table));
+
+  member_exprt class_identifier(
+    checked_dereference(ops[1], ops[1].type().subtype()),
+    "@class_identifier",
+    string_typet());
+
+  // Check the object argument is a String.
+  equal_exprt arg_is_string(
+    class_identifier, constant_exprt("java::java.lang.String", string_typet()));
+
+  // Check content equality
+  const symbolt string_equals_sym = get_fresh_aux_symbol(
+    java_boolean_type(), "string_equals", "str_eq", loc, ID_java, symbol_table);
+  const symbol_exprt string_equals = string_equals_sym.symbol_expr();
+  code.add(code_declt(string_equals));
+  code.add(code_assignt(
+    string_equals,
+    make_function_application(
+      ID_cprover_string_equal_func, args, type.return_type(), symbol_table)));
+
+  code.add(code_returnt(if_exprt(
+    arg_is_string,
+    string_equals,
+    from_integer(false, java_boolean_type()))));
   return code;
 }
 

From f4c9719b0c50ce6aec51065cc20163cca04b0226 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 23 Nov 2017 14:38:58 +0000
Subject: [PATCH 2/3] Test for String.equals with class identifier check

---
 .../jbmc-strings/StringEquals/Test.class      | Bin 0 -> 871 bytes
 .../jbmc-strings/StringEquals/Test.java       |  18 ++++++++++++++++++
 .../jbmc-strings/StringEquals/test.desc       |  12 ++++++++++++
 3 files changed, 30 insertions(+)
 create mode 100644 regression/jbmc-strings/StringEquals/Test.class
 create mode 100644 regression/jbmc-strings/StringEquals/Test.java
 create mode 100644 regression/jbmc-strings/StringEquals/test.desc

diff --git a/regression/jbmc-strings/StringEquals/Test.class b/regression/jbmc-strings/StringEquals/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..a03b132327c926fb10971dc8e7f81e89ef3bd6c6
GIT binary patch
literal 871
zcmY+C(NEJ*6vn^1wd>Xuw{?P}69q-Ku>mi<L5O5(m;rnk(LiEM*Ij3!cG`9(#uwxN
zpoudvy!i|!ERjUt{hu_R+p!K`Zg2ZL-?``eZh!y%@e{x*mQ<u+BvDjwT}2!-DWq^i
z#ZAmAm{Xy^P;g7dZOkjU!;qgheV==Q-F5wYwr{o^-ezD242gBywSx_Yc)9YJL8^D#
zoFTJqyL`9zvc<hUQOqD)FSvEYFja1BADVB>6~}ZtE6u>O-Oid&PBa74I@&Q`g#rZ&
zG#W#4-EuAtP@CPJXYmKNXqVdKey}VWX}E$6LwbulPIvZ6*K=sH-1vxw8}JVIL|I9L
zh6!q|p^OScVO+I2vUlI}x*quu{S_=~sG`P@9albT9dax9@6*r)iOLP(B*9<zOvh)K
zEMKxZ)U8!0v&^_#-JxJ9l{WWnkGG>SD2$*-fKolc99>SD?u}&&!T{~!V8S-7S$dnH
zC!?plH~>2lg~-vG2tQI*(2=J-m9hd!C1R&~Z08*DeR%+B*XYAIh1|ziJyttIqK}W~
zQ1%B%{xYQF3-&>eRf&DZ+la{{_FRuGh3sj>5+n9-$oklfm~xEi@Vw>fP__`E<Ot<M
z)JJ-Rgs)iWYlDo72!s<2GWklNM89keNz}>h7F0Z=z}iILQC#mSs!yc(LX{_!#Z^+1
z<_}5=CKXH-i$%jA?X@V-)i60Ar>D-K_Mu4MAjQ8!9uF}JS2U9m)9#8ZD1<Xk{{x|x
BtkM7g

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/StringEquals/Test.java b/regression/jbmc-strings/StringEquals/Test.java
new file mode 100644
index 00000000000..51e9dfc96e5
--- /dev/null
+++ b/regression/jbmc-strings/StringEquals/Test.java
@@ -0,0 +1,18 @@
+public class Test {
+    public static void check(int i, String s) {
+        String t = "Hello World";
+        Integer x = new Integer(2);
+        if (i==0)
+            assert("Hello World".equals(t));
+        else if (i==1)
+            assert(! "Hello World".equals(s));
+        else if (i==2)
+            assert(! "Hello World".equals(x));
+        else if (i==3)
+            assert("Hello World".equals(x));
+        else if (i==4)
+            assert(! s.equals(x));
+        else if (i==5)
+            assert(s.equals(x));
+    }
+}
diff --git a/regression/jbmc-strings/StringEquals/test.desc b/regression/jbmc-strings/StringEquals/test.desc
new file mode 100644
index 00000000000..b71cf70c218
--- /dev/null
+++ b/regression/jbmc-strings/StringEquals/test.desc
@@ -0,0 +1,12 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --function Test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 6 .* SUCCESS
+assertion at file Test.java line 8 .* FAILURE
+assertion at file Test.java line 10 .* SUCCESS
+assertion at file Test.java line 12 .* FAILURE
+assertion at file Test.java line 14 .* SUCCESS
+assertion at file Test.java line 16 .* FAILURE
+--

From 0dd029db161c16d50d19e4a8b36c99cedec3f019 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Nov 2017 12:58:20 +0000
Subject: [PATCH 3/3] Prevent use of CharSequence as a class_identifier

CharSequence is abstract and should not appear as a class identifer.
Instead we use Sring which implements CharSequence.
---
 src/java_bytecode/java_object_factory.cpp | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 18fe7238fba..c44eaeb7edf 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -571,9 +571,19 @@ 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 = "java::" + id2string(struct_type.get_tag());
-
-  // @clsid = String and @lock = false:
+  // @clsid = java::java.lang.String or similar.
+  // We allow type StringBuffer and StringBuilder to be initialized
+  // in the same way has String, because they have the same structure and
+  // are treated in the same way by CBMC.
+  // Note that CharSequence cannot be used as classid because it's abstract,
+  // so it is replaced by String.
+  // \todo allow StringBuffer and StringBuilder as classid for Charsequence
+  const irep_idt &class_id =
+    struct_type.get_tag() == "java.lang.CharSequence"
+    ? "java::java.lang.String"
+    : "java::" + id2string(struct_type.get_tag());
+
+  // @lock = false:
   const symbol_typet jlo_symbol("java::java.lang.Object");
   const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol));
   struct_exprt jlo_init(jlo_symbol);