Use string dependencies in the get method of the solver [TG-2607]

regression/jbmc-strings/StringConcat/Test.java

@@ -0,0 +1,315 @@
+public class Test {
+
+    public String stringDet() {
+        String s = "a";
+        s += "b";
+        s += "c";
+        s += "d";
+        s += "e";
+        s += "f";
+        s += "g";
+        s += "h";
+        s += "i";
+        s += "j";
+        s += "k";
+        s += "l";
+        s += "m";
+
+        assert(false);
+        return s;
+    }
+
+    public String stringNonDet(String arg) {
+        String s = arg;
+        s += "b";
+        s += "c";
+        s += "d";
+        s += "e";
+        s += "f";
+        s += arg;
+        s += "h";
+        s += "i";
+        s += "j";
+        s += "k";
+        s += "l";
+        s += arg;
+
+        assert(false);
+        return s;
+    }
+
+    public String bufferDet() {
+        StringBuffer s = new StringBuffer();
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        s.append("c");
+        s.append("d");
+        s.append("e");
+
+        s.append("a");
+        s.append("b");
+        assert(false);
+        return s.toString();
+    }
+
+    public String charBufferDet() {
+        StringBuffer s = new StringBuffer();
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+        s.append('c');
+        s.append('d');
+        s.append('e');
+
+        s.append('a');
+        s.append('b');
+
+        assert(false);
+        return s.toString();
+    }
+
+    public String charBufferDetLoop(int width) {
+        if(width <= 5)
+            return "";
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        for(int i=1; i < width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+
+        sb.append(' ');
+        sb.append('c');
+        int padding = width - 2;
+        while(padding-- > 0)
+            sb.append(' ');
+
+        sb.append(' ');
+        sb.append('|');
+        sb.append('\n');
+        assert(false);
+        return sb.toString();
+    }
+
+    public String charBufferDetLoop2(int width, int height) {
+        if(width <= 0 || height <= 0)
+            return "";
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        for(int i=1; i < width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+
+        sb.append(' ');
+        sb.append('c');
+        int padding = width - 2;
+        while(padding-- > 0)
+            sb.append(' ');
+        sb.append(' ');
+        sb.append('|');
+        sb.append('\n');
+
+        sb.append('+');
+        for(int i=1; i<width; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        for(int i = 0; i < height; ++i) {
+            sb.append('|');
+            sb.append(' ');
+            sb.append('d');
+            padding = width - 3;
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+            sb.append('\n');
+        }
+
+        sb.append('+');
+        for(int i=1; i<width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop(int width, String s) {
+        if(width <= 5 || s.length() >= width || s.length() == 0)
+            return "";
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        for(int i=1; i < width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+
+        sb.append(' ');
+        sb.append(s);
+        int padding = width - s.length();
+        while(padding-- > 0)
+            sb.append(' ');
+        sb.append(' ');
+        sb.append('|');
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop2(int width, String c) {
+        if(width < 5 || c.length() > width)
+            return "";
+
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+
+        for(int i=1; i<width-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+        for(int i = 0; i < width; ++i) {
+            sb.append(' ');
+            sb.append(c);
+            int padding = width - c.length();
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+        }
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop3(int cols, int columnWidth, String c) {
+        StringBuffer sb = new StringBuffer();
+        sb.append('-');
+        for(int i = 0; i < cols; ++i)
+            sb.append(c);
+
+        assert(false);
+        return sb.toString();
+    }
+    public String bufferNonDetLoop4(int cols, int columnWidth, String c) {
+        StringBuffer sb = new StringBuffer();
+        for(int i=1; i < columnWidth-1; ++i)
+            sb.append('-');
+        for(int i = 0; i < cols; ++i) {
+            sb.append(c);
+        }
+
+        assert(false);
+        return sb.toString();
+    }
+
+    public String bufferNonDetLoop5(int cols, int columnWidth, String c, String data[]) {
+        if(cols<1)
+            return "";
+
+        StringBuffer sb = new StringBuffer();
+        sb.append('+');
+        int totalWidth = columnWidth * cols;
+        for(int i=1; i<totalWidth-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+        sb.append('|');
+        for(int i = 0; i < cols; ++i) {
+            sb.append(' ');
+            sb.append(c);
+            int padding = columnWidth - c.length();
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+        }
+        sb.append('\n');
+
+        sb.append('+');
+        for(int i=1; i<totalWidth-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        for(int i = 0; i < data.length; ++i) {
+            sb.append('|');
+            String d = data[i];
+            sb.append(' ');
+            sb.append(d);
+            int padding = columnWidth - d.length();
+            while(padding-- > 0)
+                sb.append(' ');
+            sb.append(' ');
+            sb.append('|');
+
+            if(i % cols == 0)
+                sb.append('\n');
+        }
+
+        sb.append('+');
+        for(int i=1; i<totalWidth-1; ++i)
+            sb.append('-');
+        sb.append('+');
+        sb.append('\n');
+
+        assert(false);
+        return sb.toString();
+    }
+}

regression/jbmc-strings/StringConcat/test_buffer_det.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferDet --depth 10000  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop.desc

@@ -0,0 +1,14 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop --depth 10000 --unwind 5  --verbosity 10  --property "java::Test.bufferNonDetLoop:(ILjava/lang/String;)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
+
+This test seems to fail with AppVeyor, we should make sure it works
+once TG-2608 is done.

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop2.desc

@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop2 --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop3.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop3 --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop4.desc

@@ -0,0 +1,14 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop4 --depth 10000 --unwind 5  --verbosity 10 --property "java::Test.bufferNonDetLoop4:(IILjava/lang/String;)Ljava/lang/String;.assertion.1"
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.
+
+This test seems to fail with AppVeyor, we should make sure it works
+once TG-2608 is done.

regression/jbmc-strings/StringConcat/test_buffer_nondet_loop5.desc

@@ -0,0 +1,11 @@
+FUTURE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --function Test.bufferNonDetLoop5 --depth 10000 --unwind 5  --verbosity 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+check_SAT: got SAT but the model is not correct
+--
+Using the string dependences information to compute the model, refinement
+should not be needed when the execution is deterministic.