TG-58 New PR for Complete rework of string solver to avoid using infinite arrays

regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java

@@ -1,40 +1,52 @@
 public class StringMiscellaneous04
 {
-   public static void main(String[] args)
-   {
-      String s1 = "diffblue";
-      String s2 = "TESTGENERATION";
-      String s3 = "   automated   ";
-
-      assert s1.equals("diffblue");
-      assert s2.equals("TESTGENERATION");
-      assert s3.equals("   automated   ");
-
-      System.out.printf(
-         "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
-      String tmp=s1.replace('f', 'F');
-      assert tmp.equals("diFFblue");
-
-      tmp=s1.toUpperCase();
-      assert tmp.equals("DIFFBLUE");
-
-      tmp=s2.toLowerCase();
-      assert tmp.equals("testgeneration");
-
-      tmp=s3.trim();
-      assert tmp.equals("automated");
-
-      // test toCharArray method
-      char[] charArray = s1.toCharArray();
-      System.out.print("s1 as a character array = ");
-
-      int i=0;
-      for (char character : charArray)
-      {
-         assert character=="diffblue".charAt(i);
-         ++i;
-      }
-
-      System.out.println();
-   }
+    // This is a model of the String.toCharArray method
+    public static char[] toCharArray(String s)
+    {
+        int length=s.length();
+        assert(length<10);
+        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);
+        return arr;
+    }
+
+    public static void main(String[] args)
+    {
+        String s1 = "diffblue";
+        String s2 = "TESTGENERATION";
+        String s3 = "	automated   ";
+
+        assert s1.equals("diffblue");
+        assert s2.equals("TESTGENERATION");
+        assert s3.equals("   automated	 ");
+
+        System.out.printf(
+          "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F'));
+        String tmp=s1.replace('f', 'F');
+        assert tmp.equals("diFFblue");
+
+        tmp=s1.toUpperCase();
+        assert tmp.equals("DIFFBLUE");
+
+        tmp=s2.toLowerCase();
+        assert tmp.equals("testgeneration");
+
+        tmp=s3.trim();
+        assert tmp.equals("automated");
+
+        // test toCharArray method
+        char[] charArray = toCharArray(s1);
+        System.out.print("s1 as a character array = ");
+
+        int i=0;
+        for (char character : charArray)
+        {
+            assert character=="diffblue".charAt(i);
+            ++i;
+        }
+
+        System.out.println();
+    }
 }

regression/jbmc-strings/java_append_char/test.desc

@@ -4,5 +4,6 @@ test_append_char.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[.*assertion\.1\].* line 15.* FAILURE$
+^\[.*assertion\.1\].* line 16.* SUCCESS$
+^\[.*assertion\.2\].* line 18.* FAILURE$
 --

regression/jbmc-strings/java_append_char/test_append_char.java

@@ -1,6 +1,6 @@
 public class test_append_char
 {
-   public static void main(/*String[] args*/)
+  public static void main(boolean b)
    {
       char[] diff = {'d', 'i', 'f', 'f'};
       char[] blue = {'b', 'l', 'u', 'e'};
@@ -12,6 +12,9 @@ public static void main(/*String[] args*/)
 
       String tmp=buffer.toString();
       System.out.println(tmp);
-      assert(!tmp.equals("diffblue"));
+      if(b)
+	assert(tmp.equals("diffblue"));
+      else
+	assert(!tmp.equals("diffblue"));
    }
 }

regression/jbmc-strings/java_char_array_init/test.desc

@@ -3,5 +3,8 @@ test_init.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*assertion.1\].* line 14.* FAILURE$
+assertion.* file test_init.java line 31 .* SUCCESS$
+assertion.* file test_init.java line 33 .* SUCCESS$
+assertion.* file test_init.java line 35 .* FAILURE$
+assertion.* file test_init.java line 37 .* FAILURE$
 --

regression/jbmc-strings/java_char_array_init/test_init.java

@@ -1,18 +1,39 @@
-public class test_init {
+public class test_init
+{
+    // These are models for the constructors of strings from char arrays
+    public static String stringOfCharArray(char arr[])
+    {
+        // We give an arbitrary limit on the size of arrays
+        assert(arr.length<11);
+        StringBuilder sb=new StringBuilder("");
+        for(int i=0; i<arr.length && i<11; i++)
+            sb.append(arr[i]);
+        return sb.toString();
+    }
 
-  public static void main(/*String[] argv*/)
-  {
-     char [] str = new char[10];
-     str[0] = 'H';
-     str[1] = 'e';
-     str[2] = 'l';
-     str[3] = 'l';
-     str[4] = 'o';
-     String s = new String(str);
-     String t = new String(str,1,2);
+    public static String stringOfCharArray(char arr[], int i, int j)
+    {
+        return stringOfCharArray(arr).substring(i, i+j);
+    }
 
-     assert(s.length() != 10 || 
-            !t.equals("el") ||
-            !s.startsWith("Hello"));
-   }
+    public static void main(int i)
+    {
+        char [] str = new char[10];
+        str[0] = 'H';
+        str[1] = 'e';
+        str[2] = 'l';
+        str[3] = 'l';
+        str[4] = 'o';
+        String s = stringOfCharArray(str);
+        String t = stringOfCharArray(str,1,2);
+
+        if(i==0)
+            assert(s.startsWith("Hello"));
+        else if(i==1)
+            assert(t.equals("el"));
+        else if(i==2)
+            assert(!s.startsWith("Hello"));
+        else
+            assert(!t.equals("el"));
+    }
 }

regression/jbmc-strings/java_insert_char_array/test.desc

@@ -3,5 +3,6 @@ test_insert_char_array.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*assertion\.1\].* line 12.* FAILURE$
+assertion.* line 28.* SUCCESS$
+assertion.* line 30.* FAILURE$
 --

regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java

@@ -1,14 +1,30 @@
 public class test_insert_char_array
 {
-   public static void main(/*String[] argv*/)
-   {
-      StringBuilder sb = new StringBuilder("ad");
-      char[] array = new char[2];
-      array[0] = 'b';
-      array[1] = 'c';
-      sb.insert(1, array);
-      String s = sb.toString();
-      System.out.println(s);
-      assert(!s.equals("abcd"));
-   }
+    // These are models of the String methods manipulating char arrays
+    public static String stringOfCharArray(char arr[])
+    {
+        StringBuilder sb=new StringBuilder("");
+        for(int i=0; i<arr.length; i++)
+            sb.append(arr[i]);
+        return sb.toString();
+    }
+    public static void insert(StringBuilder sb, int pos, char arr[])
+    {
+        String s=stringOfCharArray(arr);
+        sb.insert(pos, s);
+    }
+    public static void main(int i)
+    {
+        StringBuilder sb = new StringBuilder("ad");
+        char[] array = new char[2];
+        array[0] = 'b';
+        array[1] = 'c';
+        insert(sb, 1, array);
+        String s = sb.toString();
+        System.out.println(s);
+        if(i==0)
+            assert(s.equals("abcd"));
+        else
+            assert(!s.equals("abcd"));
+    }
 }

regression/strings-smoke-tests/java_append_char/test.desc

@@ -1,7 +1,8 @@
 CORE
 test_append_char.class
 --refine-strings --string-max-length 1000
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+assertion.* file test_append_char.java line 23 .* SUCCESS
+assertion.* file test_append_char.java line 25 .* FAILURE
 --

regression/strings-smoke-tests/java_append_char/test_append_char.java

@@ -1,17 +1,27 @@
 public class test_append_char
 {
-   public static void main(/*String[] args*/)
-   {
-      char[] diff = {'d', 'i', 'f', 'f'};
-      char[] blue = {'b', 'l', 'u', 'e'};
+    public static String ofCharArray(char arr[])
+    {
+        StringBuilder sb = new StringBuilder("");
+        for(int i = 0; i < arr.length; i++)
+            sb.append(arr[i]);
+        return sb.toString();
+    }
+    public static void main(String[] args)
+    {
+        char[] diff = {'d', 'i', 'f', 'f'};
+        char[] blue = {'b', 'l', 'u', 'e'};
 
-      StringBuilder buffer = new StringBuilder();
+        StringBuilder buffer = new StringBuilder();
 
-      buffer.append(diff)
-            .append(blue);
+        buffer.append(ofCharArray(diff))
+              .append(ofCharArray(blue));
 
-      String tmp=buffer.toString();
-      System.out.println(tmp);
-      assert tmp.equals("diffblue");
-   }
+        String tmp=buffer.toString();
+        System.out.println(tmp);
+        if(args.length == 0)
+            assert tmp.equals("diffblue");
+        else
+            assert !tmp.equals("diffblue");
+    }
 }

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

@@ -1,14 +1,29 @@
 public class test_append_string
 {
-   public static void main(/*String[] args*/)
-   {
-      String di = new String("di");
-      StringBuilder diff = new StringBuilder();
-      diff.append(di);
-      diff.append("ff");
-      System.out.println(diff);
-      String s = diff.toString();
-      System.out.println(s);
-      assert s.equals("diff");
-   }
+    public static void main()
+    {
+        String di = new String("di");
+        StringBuilder diff = new StringBuilder();
+        diff.append(di);
+        diff.append("ff");
+        System.out.println(diff);
+        String s = diff.toString();
+        System.out.println(s);
+        assert s.equals("diff");
+    }
+
+    public static void check(StringBuilder sb, String str)
+    {
+        String init = sb.toString();
+        if(str.length() >= 4)
+        {
+            sb.append(str, 2, 4);
+            String res = sb.toString();
+            assert(res.startsWith(init));
+            assert(res.endsWith(str.substring(2, 4)));
+            assert(res.length() == init.length() + 2);
+            assert(!res.equals("foobarfuz"));
+        }
+    }
+
 }

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

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

regression/strings-smoke-tests/java_char_array/test.desc

@@ -3,11 +3,12 @@ test_char_array.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
-.*assertion.* test_char_array.java line 9 .* SUCCESS$
-.*assertion.* test_char_array.java line 10 .* SUCCESS$
-.*assertion.* test_char_array.java line 11 .* SUCCESS$
-.*assertion.* test_char_array.java line 13 .* FAILURE$
-.*assertion.* test_char_array.java line 15 .* FAILURE$
-.*assertion.* test_char_array.java line 17 .* FAILURE$
+.*assertion.* test_char_array.java line 7 .* SUCCESS$
+.*assertion.* test_char_array.java line 21 .* SUCCESS$
+.*assertion.* test_char_array.java line 22 .* SUCCESS$
+.*assertion.* test_char_array.java line 23 .* SUCCESS$
+.*assertion.* test_char_array.java line 25 .* FAILURE$
+.*assertion.* test_char_array.java line 27 .* FAILURE$
+.*assertion.* test_char_array.java line 29 .* FAILURE$
 ^VERIFICATION FAILED$
 --