TG-2153 Add more String primitives to JBMC

regression/jbmc-strings/cprover/CProverString.java

@@ -8,6 +8,29 @@ public static char charAt(String s, int i) {
             return '\u0000';
     }
 
+    public static int codePointAt(String s, int index) {
+        return s.codePointAt(index);
+    }
+
+    public static int codePointBefore(String s, int index) {
+        return s.codePointBefore(index);
+    }
+
+    public static int codePointCount(
+            String s, int beginIndex, int endIndex) {
+        return s.codePointCount(beginIndex, endIndex);
+    }
+
+    public static int offsetByCodePoints(
+            String s, int index, int codePointOffset) {
+        return s.offsetByCodePoints(index, codePointOffset);
+    }
+
+    public static CharSequence subSequence(
+            String s, int beginIndex, int endIndex) {
+        return s.subSequence(beginIndex, endIndex);
+    }
+
     public static String substring(String s, int i) {
         if (i <= 0)
             return s;
@@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) {
             return "";
         return s.substring(i, j);
     }
+
+    public static StringBuilder append(
+            StringBuilder sb, CharSequence cs, int i, int j) {
+        return sb.append(cs, i, j);
+    }
+
+    public static StringBuilder delete(StringBuilder sb, int start, int end) {
+        return sb.delete(start, end);
+    }
+
+    public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
+        return sb.deleteCharAt(index);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, String str) {
+        return sb.insert(offset, str);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, boolean b) {
+        return sb.insert(offset, b);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, char c) {
+        return sb.insert(offset, c);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, int i) {
+        return sb.insert(offset, i);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, long l) {
+        return sb.insert(offset, l);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, float f) {
+        return sb.insert(offset, f);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, double d) {
+        return sb.insert(offset, d);
+    }
+
+    public static void setLength(StringBuffer sb, int newLength) {
+        sb.setLength(newLength);
+    }
+
+    public static char charAt(StringBuffer sb, int index) {
+        return sb.charAt(index);
+    }
+
+    public static void setCharAt(StringBuffer sb, int index, char c) {
+        sb.setCharAt(index, c);
+    }
+
+    public static StringBuffer delete(
+            StringBuffer sb, int start, int end) {
+        return sb.delete(start, end);
+    }
+
+    public static StringBuffer deleteCharAt(StringBuffer sb, int index) {
+        return sb.deleteCharAt(index);
+    }
+
+    public static String substring(StringBuffer sb, int start, int end) {
+        return sb.substring(start, end);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, String str) {
+        return sb.insert(offset, str);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, boolean b) {
+        return sb.insert(offset, b);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, char c) {
+        return sb.insert(offset, c);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, int i) {
+        return sb.insert(offset, i);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, long l) {
+        return sb.insert(offset, l);
+    }
 }

regression/jbmc-strings/java_delete/test_delete.java

@@ -3,7 +3,7 @@ public class test_delete
    public static void main(/*String[] argv*/)
    {
       StringBuilder s = new StringBuilder("Abc");
-      s.delete(1,2);
+      org.cprover.CProverString.delete(s,1,2);
       String str = s.toString();
       assert(!str.equals("Ac"));
    }

regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java

@@ -4,7 +4,7 @@ public static void main(/*String[] argv*/)
    {
       StringBuilder s = new StringBuilder();
       s.append("Abc");
-      s.deleteCharAt(1);
+      org.cprover.CProverString.deleteCharAt(s, 1);
       String str = s.toString();
       assert(!str.equals("Ac"));
    }

regression/jbmc-strings/java_insert_char/test_insert_char.java

@@ -3,7 +3,7 @@ public class test_insert_char
    public static void main(/*String[] argv*/)
    {
       StringBuilder sb = new StringBuilder("ac");
-      sb.insert(1, 'b');
+      org.cprover.CProverString.insert(sb, 1, 'b');
       String s = sb.toString();
       assert(!s.equals("abc"));
    }

regression/jbmc-strings/java_insert_char_array/test.desc

@@ -3,6 +3,6 @@ test_insert_char_array.class
 --refine-strings --string-max-length 1000 --function test_insert_char_array.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion.* line 28.* SUCCESS$
-assertion.* line 30.* FAILURE$
+assertion.* line 26.* SUCCESS$
+assertion.* line 28.* FAILURE$
 --

regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java

@@ -11,7 +11,7 @@ public static String stringOfCharArray(char arr[])
     public static void insert(StringBuilder sb, int pos, char arr[])
     {
         String s=stringOfCharArray(arr);
-        sb.insert(pos, s);
+        org.cprover.CProverString.insert(sb, pos, s);
     }
     public static void main(int i)
     {

regression/jbmc-strings/java_insert_int/test_insert_int.java

@@ -3,7 +3,7 @@ public class test_insert_int
    public static void main(/*String[] argv*/)
    {
       StringBuilder sb = new StringBuilder("ac");
-      sb.insert(1, 42);
+      org.cprover.CProverString.insert(sb, 1, 42);
       String s = sb.toString();
       assert(!s.equals("a42c"));
    }

regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java

@@ -3,8 +3,8 @@ public class test_insert_multiple
    public static void main(/*String[] argv*/)
    {
       StringBuilder sb = new StringBuilder("ad");
-      sb.insert(1, 'c');
-      sb.insert(1, "b");
+      org.cprover.CProverString.insert(sb, 1, 'c');
+      org.cprover.CProverString.insert(sb, 1, "b");
       String s = sb.toString();
       assert(!s.equals("abcd"));
    }

regression/jbmc-strings/java_insert_string/test_insert_string.java

@@ -3,7 +3,7 @@ public class test_insert_string
    public static void main(/*String[] argv*/)
    {
       StringBuilder sb = new StringBuilder("ad");
-      sb.insert(1, "bc");
+      org.cprover.CProverString.insert(sb, 1, "bc");
       String s = sb.toString();
       assert(!s.equals("abcd"));
    }

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

@@ -8,6 +8,29 @@ public static char charAt(String s, int i) {
             return '\u0000';
     }
 
+    public static int codePointAt(String s, int index) {
+        return s.codePointAt(index);
+    }
+
+    public static int codePointBefore(String s, int index) {
+        return s.codePointBefore(index);
+    }
+
+    public static int codePointCount(
+            String s, int beginIndex, int endIndex) {
+        return s.codePointCount(beginIndex, endIndex);
+    }
+
+    public static int offsetByCodePoints(
+            String s, int index, int codePointOffset) {
+        return s.offsetByCodePoints(index, codePointOffset);
+    }
+
+    public static CharSequence subSequence(
+            String s, int beginIndex, int endIndex) {
+        return s.subSequence(beginIndex, endIndex);
+    }
+
     public static String substring(String s, int i) {
         if (i <= 0)
             return s;
@@ -26,4 +49,102 @@ public static String substring(String s, int i, int j) {
             return "";
         return s.substring(i, j);
     }
+
+    public static StringBuilder append(
+            StringBuilder sb, CharSequence cs, int i, int j) {
+        return sb.append(cs, i, j);
+    }
+
+    public static StringBuilder delete(StringBuilder sb, int start, int end) {
+        return sb.delete(start, end);
+    }
+
+    public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
+        return sb.deleteCharAt(index);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, String str) {
+        return sb.insert(offset, str);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, boolean b) {
+        return sb.insert(offset, b);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, char c) {
+        return sb.insert(offset, c);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, int i) {
+        return sb.insert(offset, i);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, long l) {
+        return sb.insert(offset, l);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, float f) {
+        return sb.insert(offset, f);
+    }
+
+    public static StringBuilder insert(
+            StringBuilder sb, int offset, double d) {
+        return sb.insert(offset, d);
+    }
+
+    public static void setLength(StringBuffer sb, int newLength) {
+        sb.setLength(newLength);
+    }
+
+    public static char charAt(StringBuffer sb, int index) {
+        return sb.charAt(index);
+    }
+
+    public static void setCharAt(StringBuffer sb, int index, char c) {
+        sb.setCharAt(index, c);
+    }
+
+    public static StringBuffer delete(
+            StringBuffer sb, int start, int end) {
+        return sb.delete(start, end);
+    }
+
+    public static StringBuffer deleteCharAt(StringBuffer sb, int index) {
+        return sb.deleteCharAt(index);
+    }
+
+    public static String substring(StringBuffer sb, int start, int end) {
+        return sb.substring(start, end);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, String str) {
+        return sb.insert(offset, str);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, boolean b) {
+        return sb.insert(offset, b);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, char c) {
+        return sb.insert(offset, c);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, int i) {
+        return sb.insert(offset, i);
+    }
+
+    public static StringBuffer insert(
+            StringBuffer sb, int offset, long l) {
+        return sb.insert(offset, l);
+    }
 }

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

@@ -17,7 +17,7 @@ public static void check(StringBuilder sb, String str)
         String init = sb.toString();
         if(str.length() >= 4)
         {
-            sb.append(str, 2, 4);
+            org.cprover.CProverString.append(sb, str, 2, 4);
             String res = sb.toString();
             assert(res.startsWith(init));
             assert(res.endsWith(org.cprover.CProverString.substring(str, 2, 4)));

regression/strings-smoke-tests/java_append_string/test_substring.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---refine-strings --verbosity 10 --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
+--refine-strings  --string-max-length 10 --function test_append_string.check --java-assume-inputs-non-null
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.*\].* line 22.* SUCCESS$

regression/strings-smoke-tests/java_code_point/test_code_point.java

@@ -3,10 +3,10 @@ public class test_code_point
    public static void main(/*String[] argv*/)
    {
       String s = "!𐤇𐤄𐤋𐤋𐤅";
-      assert(s.codePointAt(1) == 67847);
-      assert(s.codePointBefore(3) == 67847);
-      assert(s.codePointCount(1,5) >= 2);
-      assert(s.offsetByCodePoints(1,2) >= 3);
+      assert(org.cprover.CProverString.codePointAt(s, 1) == 67847);
+      assert(org.cprover.CProverString.codePointBefore(s, 3) == 67847);
+      assert(org.cprover.CProverString.codePointCount(s,1,5) >= 2);
+      assert(org.cprover.CProverString.offsetByCodePoints(s,1,2) >= 3);
       StringBuilder sb = new StringBuilder();
       sb.appendCodePoint(0x10907);
       assert(org.cprover.CProverString.charAt(s, 1) == org.cprover.CProverString.charAt(sb.toString(), 0));

regression/strings-smoke-tests/java_delete/test_delete.java

@@ -3,7 +3,7 @@ public class test_delete
    public static void main(/*String[] argv*/)
    {
       StringBuilder s = new StringBuilder("Abc");
-      s.delete(1,2);
+      org.cprover.CProverString.delete(s,1,2);
       String str = s.toString();
       assert(str.equals("Ac"));
    }

regression/strings-smoke-tests/java_delete_char_at/test_delete_char_at.java

@@ -4,7 +4,7 @@ public static void main(/*String[] argv*/)
    {
       StringBuilder s = new StringBuilder();
       s.append("Abc");
-      s.deleteCharAt(1);
+      org.cprover.CProverString.deleteCharAt(s, 1);
       String str = s.toString();
       assert(str.equals("Ac"));
    }

regression/strings-smoke-tests/java_insert_char/test_insert_char.java

@@ -3,7 +3,7 @@ public class test_insert_char
    public static void main(/*String[] argv*/)
    {
       StringBuilder sb = new StringBuilder("ac");
-      sb.insert(1, 'b');
+      org.cprover.CProverString.insert(sb, 1, 'b');
       String s = sb.toString();
       assert(s.equals("abc"));
    }