Fix String.equals to check for class identifier

Author: romainbrenguier

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