Add verification test for String.equals

We add tests which compare the internal String.equals with a reference
implementation which loops over the characters of the string.

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,10 @@
+KNOWNBUG
+Test.class
+ --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verify
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 60 .* SUCCESS
+--
+--
+Our current implementation does not handle the null case
+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