Fix problem with String.equals not checking the argument is a String TG-1619

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));
+    }
+}

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
+--

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);

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;
 }