Merge pull request diffblue#1665 from romainbrenguier/bugfix/string-out-of-bound#TG-1808

Make clear that cbmc version of charAt and substring do not throw OutOfBound TG-1808

Author: Thomas Kiley

regression/jbmc-strings/StringLastIndexOf/Test.class

@@ -13,7 +13,7 @@ public void check(String input_String1, String input_String2, int i) {
                 // Contradiction with the previous condition (should fail).
                 assert "foo".lastIndexOf("") != 3;
             } else if (i == 2 && input_String2.length() > 0) {
-                int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex);
+                int lio = input_String1.lastIndexOf(org.cprover.CProverString.charAt(input_String2, 0), fromIndex);
                 if (input_String2.length() == 0)
                     assert lio == fromIndex;
             } else if (i == 3) {

regression/jbmc-strings/StringLastIndexOf/Test.java

@@ -8,19 +8,19 @@ public static char[] toCharArray(String s)
         char arr[]=new char[s.length()];
         // We limit arbitrarly the loop unfolding to 10
         for(int i=0; i<length && i<10; i++)
-            arr[i]=s.charAt(i);
+            arr[i]=org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
     public static void main(String[] args)
     {
         String s1 = "diffblue";
         String s2 = "TESTGENERATION";
-        String s3 = "	automated   ";
+        String s3 = "   automated   ";
 
         assert s1.equals("diffblue");
         assert s2.equals("TESTGENERATION");
-        assert s3.equals("   automated	 ");
+        assert s3.equals("   automated   ");
 
         System.out.printf(
           "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
@@ -43,7 +43,7 @@ public static void main(String[] args)
         int i=0;
         for (char character : charArray)
         {
-            assert character=="diffblue".charAt(i);
+            assert character==org.cprover.CProverString.charAt("diffblue", i);
             ++i;
         }
 

regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class

@@ -1,13 +1,12 @@
 public class SubString01
 {
-   public static void main(String[] args)
-   {
-      String letters = "automatictestcasegenerationatdiffblue";
+    public static void main(String[] args)
+    {
+        String letters = "automatictestcasegenerationatdiffblue";
 
-      String tmp=letters.substring(20);
-      assert tmp.equals("erationatdiffblue");
-
-      tmp=letters.substring(9, 13);
-      assert tmp.equals("test");
-   }
+        String tmp=org.cprover.CProverString.substring(letters, 20);
+        assert tmp.equals("erationatdiffblue");
+        tmp=org.cprover.CProverString.substring(letters, 9, 13);
+        assert tmp.equals("test");
+    }
 }

regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java

@@ -0,0 +1,29 @@
+package org.cprover;
+
+public final class CProverString {
+    public static char charAt(String s, int i) {
+        if (0 <= i && i < s.length())
+            return s.charAt(i);
+        else
+            return '\u0000';
+    }
+
+    public static String substring(String s, int i) {
+        if (i <= 0)
+            return s;
+        else if (i >= s.length())
+            return "";
+        else
+            return s.substring(i);
+    }
+
+    public static String substring(String s, int i, int j) {
+        if (i < 0)
+            return substring(s, 0, j);
+        if (j >= s.length())
+            return substring(s, 0, s.length() - 1);
+        if (i >= j)
+            return "";
+        return s.substring(i, j);
+    }
+}

regression/jbmc-strings/SubString01/SubString01.class

@@ -13,7 +13,7 @@ public static String stringOfCharArray(char arr[])
 
     public static String stringOfCharArray(char arr[], int i, int j)
     {
-        return stringOfCharArray(arr).substring(i, i+j);
+        return org.cprover.CProverString.substring(stringOfCharArray(arr), i, i+j);
     }
 
     public static void main(int i)

regression/jbmc-strings/SubString01/SubString01.java

@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
       int i = s.length();
       String t = new String("ppo");
       String u = s.concat(t);
-      char c = u.charAt(i);
+      char c = org.cprover.CProverString.charAt(u, i);
       assert(c == 'p');
       assert(c != 'p');
    }

regression/jbmc-strings/cprover/CProverString.class

@@ -0,0 +1,29 @@
+package org.cprover;
+
+public final class CProverString {
+    public static char charAt(String s, int i) {
+        if (0 <= i && i < s.length())
+            return s.charAt(i);
+        else
+            return '\u0000';
+    }
+
+    public static String substring(String s, int i) {
+        if (i <= 0)
+            return s;
+        else if (i >= s.length())
+            return "";
+        else
+            return s.substring(i);
+    }
+
+    public static String substring(String s, int i, int j) {
+        if (i < 0)
+            return substring(s, 0, j);
+        if (j >= s.length())
+            return substring(s, 0, s.length() - 1);
+        if (i >= j)
+            return "";
+        return s.substring(i, j);
+    }
+}

regression/jbmc-strings/cprover/CProverString.java

@@ -20,7 +20,7 @@ public static void check(StringBuilder sb, String str)
             sb.append(str, 2, 4);
             String res = sb.toString();
             assert(res.startsWith(init));
-            assert(res.endsWith(str.substring(2, 4)));
+            assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4)));
             assert(res.length() == init.length() + 2);
             assert(!res.equals("foobarfuz"));
         }

regression/jbmc-strings/java_char_array_init/test_init.class

@@ -8,7 +8,7 @@ public static char[] toCharArray(String s)
         char arr[] = new char[s.length()];
         // We limit arbitrarly the loop unfolding to 5
         for(int i = 0; i < length && i < 5; i++)
-        arr[i] = s.charAt(i);
+            arr[i] = org.cprover.CProverString.charAt(s, i);
         return arr;
     }
 
@@ -17,7 +17,7 @@ public static void main(int i)
         String s = "abc";
         char [] str = toCharArray(s);
         char c = str[2];
-        char a = s.charAt(0);
+        char a = org.cprover.CProverString.charAt(s, 0);
         assert(str.length == 3);
         assert(a == 'a');
         assert(c == 'c');

regression/jbmc-strings/java_char_array_init/test_init.java

@@ -2,6 +2,6 @@ public class test_char_at {
 
   public static void main(/*String[] argv*/) {
     String s = new String("abc");
-    assert(s.charAt(2)=='c');
+    assert(org.cprover.CProverString.charAt(s, 2)=='c');
   }
 }

regression/jbmc-strings/java_concat/test_concat.class

@@ -9,6 +9,6 @@ public static void main(/*String[] argv*/)
       assert(s.offsetByCodePoints(1,2) >= 3);
       StringBuilder sb = new StringBuilder();
       sb.appendCodePoint(0x10907);
-      assert(s.charAt(1) == sb.charAt(0));
+      assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0));
    }
 }

regression/jbmc-strings/java_concat/test_concat.java

@@ -6,7 +6,7 @@ public static void main(/*String[] argv*/)
       int i = s.length();
       String t = new String("ppo");
       String u = s.concat(t);
-      char c = u.charAt(i);
+      char c = org.cprover.CProverString.charAt(u, i);
       assert(c == 'p');
       assert(c == 'o');
    }

regression/strings-smoke-tests/cprover/CProverString.class

@@ -3,11 +3,11 @@ public class test_set_char_at
    public static void main(/*String[] argv*/)
    {
       String s = new String("Abc");
-      char c = s.charAt(1);
+      char c = org.cprover.CProverString.charAt(s, 1);
       StringBuilder sb = new StringBuilder(s);
       sb.setCharAt(1,'w');
       s = sb.toString();
       assert(s.equals("Awc"));
-      assert(s.charAt(2)=='c');
+      assert(org.cprover.CProverString.charAt(s, 2)=='c');
    }
 }

regression/strings-smoke-tests/cprover/CProverString.java

@@ -3,10 +3,10 @@ public class test_substring
    public static void main(/*String[] argv*/)
    {
       String abcdef = "AbcDef";
-      String cde = abcdef.substring(2,5);
-      char c = cde.charAt(0);
-      char d = cde.charAt(1);
-      char e = cde.charAt(2);
+      String cde = org.cprover.CProverString.substring(abcdef, 2,5);
+      char c = org.cprover.CProverString.charAt(cde, 0);
+      char d = org.cprover.CProverString.charAt(cde, 1);
+      char e = org.cprover.CProverString.charAt(cde, 2);
       assert(c == 'c');
       assert(d == 'D');
       assert(e == 'e');

regression/strings-smoke-tests/java_append_string/test_append_string.class

@@ -1890,8 +1890,10 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::java.lang.String.<init>:()V"]=
       ID_cprover_string_empty_string_func;
 
+  // CProverString.charAt differs from the Java String.charAt in that no
+  // exception is raised for the out of bounds case.
   cprover_equivalent_to_java_function
-    ["java::java.lang.String.charAt:(I)C"]=
+    ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
       ID_cprover_string_char_at_func;
   cprover_equivalent_to_java_function
     ["java::java.lang.String.codePointAt:(I)I"]=
@@ -1999,11 +2001,15 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]=
       ID_cprover_string_substring_func;
+  // CProverString.substring differs from the Java String.substring in that no
+  // exception is raised for the out of bounds case.
   cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.substring:(II)Ljava/lang/String;"]=
+    ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
+    "Ljava/lang/String;"]=
       ID_cprover_string_substring_func;
   cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.substring:(I)Ljava/lang/String;"]=
+    ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
+    "Ljava/lang/String;"]=
       ID_cprover_string_substring_func;
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=