Merge pull request #1977 from romainbrenguier/bugfix/string-equals-TG-2179

Fix bug in preprocessing of String.equals

Author: romainbrenguier

regression/jbmc-strings/StringEquals/Test.class

@@ -1,3 +1,6 @@
+// Uses CProverString, must be compiled with ../cprover/CProverString.java
+import org.cprover.*;
+
 public class Test {
     public static void check(int i, String s) {
         String t = "Hello World";
@@ -15,4 +18,49 @@ else if (i==4)
         else if (i==5)
             assert(s.equals(x));
     }
+
+    public static boolean referenceImplementation(String s, Object o) {
+        if (! (o instanceof String))
+            return false;
+
+        String s2 = (String) o;
+        if (s.length() != s2.length())
+            return false;
+
+        for (int i = 0; i < s.length(); i++) {
+            if (CProverString.charAt(s, i) != CProverString.charAt(s2, i))
+                return false;
+        }
+
+        return true;
+    }
+
+    public static boolean verifyNonNull(String s, Object o) {
+        // Filter
+        if (s == null || o == null)
+            return false;
+
+        // Act
+        boolean result = s.equals(o);
+        boolean referenceResult = referenceImplementation(s, o);
+
+        // Assert
+        assert result == referenceResult;
+
+        // Return
+        return result;
+    }
+
+    public static boolean verify(String s, Object o) {
+        // Act
+        boolean result = s.equals(o);
+        boolean referenceResult = referenceImplementation(s, o);
+
+        // Assert
+        assert result == referenceResult;
+
+        // Return
+        return result;
+    }
+
 }

regression/jbmc-strings/StringEquals/Test.java

@@ -3,10 +3,10 @@ Test.class
 --refine-strings --string-max-length 40 --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
+assertion at file Test.java line 9 .* SUCCESS
+assertion at file Test.java line 11 .* FAILURE
+assertion at file Test.java line 13 .* SUCCESS
+assertion at file Test.java line 15 .* FAILURE
+assertion at file Test.java line 17 .* SUCCESS
+assertion at file Test.java line 19 .* FAILURE
 --

regression/jbmc-strings/StringEquals/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+Test.class
+--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 60 .* SUCCESS
+--
+--
+null case not handled currently
+TG-2179
+

regression/jbmc-strings/StringEquals/test_verify.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verifyNonNull
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 48 .* SUCCESS

regression/jbmc-strings/StringEquals/test_verify_non_null.desc

@@ -930,53 +930,56 @@ java_string_library_preprocesst::string_literal_to_string_expr(
 /// \param symbol_table: symbol table
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// string_expr1 = {this->length; *this->data}
-/// string_expr2 = {arg->length; *arg->data}
-/// return cprover_string_equal(string_expr1, string_expr2)
+/// IF arg->@class_identifier == "java.lang.String"
+/// THEN
+///   string_expr1 = {this->length; *this->data}
+///   string_expr2 = {arg->length; *arg->data}
+///   bool string_equals_tmp = cprover_string_equal(string_expr1, string_expr2)
+///   return string_equals_tmp
+/// ELSE
+///   return false
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::make_equals_function_code(
   const code_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
 {
-  code_blockt code;
+  const typet &return_type = type.return_type();
   exprt::operandst ops;
   for(const auto &p : type.parameters())
   {
     symbol_exprt sym(p.get_identifier(), p.type());
     ops.push_back(sym);
   }
-  exprt::operandst args=process_equals_function_operands(
-    ops, loc, symbol_table, code);
-
-  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), loc);
-  code.add(
-    code_assignt(
-      string_equals,
-      make_function_application(
-        ID_cprover_string_equal_func, args, type.return_type(), symbol_table)),
-    loc);
-
-  code.add(
-    code_returnt(
-      if_exprt(
-        arg_is_string,
-        string_equals,
-        from_integer(false, java_boolean_type()))),
-    loc);
+  code_ifthenelset code;
+  code.cond() = [&] {
+    const member_exprt class_identifier(
+      checked_dereference(ops[1], ops[1].type().subtype()),
+      "@class_identifier",
+      string_typet());
+    return equal_exprt(
+      class_identifier,
+      constant_exprt("java::java.lang.String", string_typet()));
+  }();
+
+  code.then_case() = [&] {
+    code_blockt instance_case;
+    // Check content equality
+    const symbolt string_equals_sym = get_fresh_aux_symbol(
+      return_type, "string_equals", "str_eq", loc, ID_java, symbol_table);
+    const symbol_exprt string_equals = string_equals_sym.symbol_expr();
+    instance_case.add(code_declt(string_equals), loc);
+    const exprt::operandst args =
+      process_equals_function_operands(ops, loc, symbol_table, instance_case);
+    const auto fun_app = make_function_application(
+      ID_cprover_string_equal_func, args, return_type, symbol_table);
+    instance_case.add(code_assignt(string_equals, fun_app), loc);
+    instance_case.add(code_returnt(string_equals), loc);
+    return instance_case;
+  }();
+
+  code.else_case() = code_returnt(from_integer(false, return_type));
   return code;
 }