diff --git a/regression/strings/Makefile b/regression/strings/Makefile new file mode 100644 index 00000000000..545b36925ac --- /dev/null +++ b/regression/strings/Makefile @@ -0,0 +1,3 @@ + +test: + ../test.pl -c ../../../src/cbmc/cbmc diff --git a/regression/strings/cprover-string-hack.h b/regression/strings/cprover-string-hack.h new file mode 100644 index 00000000000..8a560e9d70d --- /dev/null +++ b/regression/strings/cprover-string-hack.h @@ -0,0 +1,73 @@ +typedef struct __CPROVER_string { char *s; } __CPROVER_string; +//typedef struct __CPROVER_char { char c; } __CPROVER_char; +typedef unsigned char __CPROVER_char; + +/****************************************************************************** + * CPROVER string functions + ******************************************************************************/ +/* returns s[p] */ +#define __CPROVER_char_at(s, p) __CPROVER_uninterpreted_string_char_at_func(s, p) + +/* string equality */ +#define __CPROVER_string_equal(s1, s2) __CPROVER_uninterpreted_string_equal_func(s1, s2) + +/* defines a string literal, e.g. __CPROVER_string_literal("foo") */ +#define __CPROVER_string_literal(s) __CPROVER_uninterpreted_string_literal_func(s) + +/* defines a char literal, e.g. __CPROVER_char_literal("c"). NOTE: you + * *must* use a C string literal as argument (i.e. double quotes "c", not + * single 'c') */ +#define __CPROVER_char_literal(c) __CPROVER_uninterpreted_char_literal_func(c) + +/* produces the concatenation of s1 and s2 */ +#define __CPROVER_string_concat(s1, s2) __CPROVER_uninterpreted_string_concat_func(s1, s2) + +/* return the length of s */ +#define __CPROVER_string_length(s) __CPROVER_uninterpreted_string_length_func(s) + +/* extracts the substring between positions i and j (j not included) */ +#define __CPROVER_string_substring(s, i, j) __CPROVER_uninterpreted_string_substring_func(s, i, j) + +/* test whether p is a prefix of s */ +#define __CPROVER_string_isprefix(p, s) __CPROVER_uninterpreted_string_is_prefix_func(p, s) + +/* test whether p is a suffix of s */ +#define __CPROVER_string_issuffix(p, s) __CPROVER_uninterpreted_string_is_suffix_func(p, s) +/* test whether p contains s */ +#define __CPROVER_string_contains(p, s) __CPROVER_uninterpreted_string_contains_func(p, s) + +/* first index where character c appears, -1 if not found */ +#define __CPROVER_string_index_of(s, c) __CPROVER_uninterpreted_string_index_of_func(s, c) + +/* last index where character c appears */ +#define __CPROVER_string_last_index_of(s, c) __CPROVER_uninterpreted_string_last_index_of_func(s, c) + +/* returns a new string obtained from s by setting s[p] = c */ +#define __CPROVER_char_set(s, p, c) __CPROVER_uninterpreted_string_char_set_func(s, p, c) + + +#define __CPROVER_string_copy(s) __CPROVER_uninterpreted_string_copy_func(s) +#define __CPROVER_parse_int(s) __CPROVER_uninterpreted_string_parse_int_func(s) +#define __CPROVER_string_of_int(i) __CPROVER_uninterpreted_string_of_int_func(i) + + +/****************************************************************************** + * don't use these directly + ******************************************************************************/ +extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos); +extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2); +extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func(); +extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func(); +extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2); +extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str); +extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func(__CPROVER_string str, int i, int j); +extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func(__CPROVER_string pref, __CPROVER_string str); +extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_string suff, __CPROVER_string str); +extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func(__CPROVER_string str1, __CPROVER_string str2); +extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __CPROVER_char c); +extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c); +extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c); +extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str); +extern unsigned __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str); +extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(unsigned i); + diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc new file mode 100644 index 00000000000..7397314cca8 --- /dev/null +++ b/regression/strings/java_case/test.desc @@ -0,0 +1,10 @@ +CORE +test_case.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_case.java line 11: SUCCESS$ +^\[assertion.2\] assertion at file test_case.java line 12: SUCCESS$ +^\[assertion.3\] assertion at file test_case.java line 13: SUCCESS$ +^\[assertion.4\] assertion at file test_case.java line 14: FAILURE$ +-- \ No newline at end of file diff --git a/regression/strings/java_case/test_case.class b/regression/strings/java_case/test_case.class new file mode 100644 index 00000000000..8579881de17 Binary files /dev/null and b/regression/strings/java_case/test_case.class differ diff --git a/regression/strings/java_case/test_case.java b/regression/strings/java_case/test_case.java new file mode 100644 index 00000000000..ce3a51814c8 --- /dev/null +++ b/regression/strings/java_case/test_case.java @@ -0,0 +1,16 @@ +public class test_case { + + public static void main(String[] argv) { + + String s = new String("AbcCdE"); + String l = s.toLowerCase(); + System.out.println(l); + + String u = s.toUpperCase(); + System.out.println(u); + assert(l.equals("abccde")); + assert(u.equals("ABCCDE")); + assert(s.equalsIgnoreCase("ABccDe")); + assert(!l.equals("abccde") || !u.equals("ABCCDE")); + } +} diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc new file mode 100644 index 00000000000..babcc395bcf --- /dev/null +++ b/regression/strings/java_char_at/test.desc @@ -0,0 +1,9 @@ +CORE +test_char_at.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_char_at.java line 11: SUCCESS$ +^\[assertion.2\] assertion at file test_char_at.java line 13: FAILURE$ +^\[assertion.3\] assertion at file test_char_at.java line 15: SUCCESS$ +-- diff --git a/regression/strings/java_char_at/test_char_at.class b/regression/strings/java_char_at/test_char_at.class new file mode 100644 index 00000000000..7d1f07fad7d Binary files /dev/null and b/regression/strings/java_char_at/test_char_at.class differ diff --git a/regression/strings/java_char_at/test_char_at.java b/regression/strings/java_char_at/test_char_at.java new file mode 100644 index 00000000000..337c6524099 --- /dev/null +++ b/regression/strings/java_char_at/test_char_at.java @@ -0,0 +1,17 @@ +public class test_char_at { + + public static void main(String[] argv) { + String s = new String("Hello World!"); + char c = s.charAt(4); + StringBuilder sb = new StringBuilder(s); + sb.setCharAt(5,'-'); + s = sb.toString(); + + if(argv.length==1) + assert(c == 'o'); + else if(argv.length==2) + assert(c == 'p'); + else + assert(s.equals("Hello-World!")); + } +} diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc new file mode 100644 index 00000000000..bb69366ce61 --- /dev/null +++ b/regression/strings/java_code_point/test.desc @@ -0,0 +1,11 @@ +CORE +test_code_point.class +--pass +^EXIT=0$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_code_point.java line 5: SUCCESS$ +^\[assertion.2\] assertion at file test_code_point.java line 6: SUCCESS$ +^\[assertion.3\] assertion at file test_code_point.java line 7: SUCCESS$ +^\[assertion.4\] assertion at file test_code_point.java line 8: SUCCESS$ +^\[assertion.5\] assertion at file test_code_point.java line 11: SUCCESS$ +-- \ No newline at end of file diff --git a/regression/strings/java_code_point/test_code_point.class b/regression/strings/java_code_point/test_code_point.class new file mode 100644 index 00000000000..c257f0633ec Binary files /dev/null and b/regression/strings/java_code_point/test_code_point.class differ diff --git a/regression/strings/java_code_point/test_code_point.java b/regression/strings/java_code_point/test_code_point.java new file mode 100644 index 00000000000..c27a56f575c --- /dev/null +++ b/regression/strings/java_code_point/test_code_point.java @@ -0,0 +1,13 @@ +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); + StringBuilder sb = new StringBuilder(); + sb.appendCodePoint(0x10907); + assert(s.charAt(1) == sb.charAt(0)); + } +} diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc new file mode 100644 index 00000000000..c500900a21e --- /dev/null +++ b/regression/strings/java_compare/test.desc @@ -0,0 +1,10 @@ +CORE +test_compare.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_compare.java line 6: SUCCESS$ +^\[assertion.2\] assertion at file test_compare.java line 8: FAILURE$ +^\[assertion.3\] assertion at file test_compare.java line 11: SUCCESS$ +^\[assertion.4\] assertion at file test_compare.java line 12: FAILURE$ +-- diff --git a/regression/strings/java_compare/test_compare.class b/regression/strings/java_compare/test_compare.class new file mode 100644 index 00000000000..5616013c523 Binary files /dev/null and b/regression/strings/java_compare/test_compare.class differ diff --git a/regression/strings/java_compare/test_compare.java b/regression/strings/java_compare/test_compare.java new file mode 100644 index 00000000000..8c1d4b71a0c --- /dev/null +++ b/regression/strings/java_compare/test_compare.java @@ -0,0 +1,18 @@ +public class test_compare { + + public static void main(String[] argv) { + String s1 = "abc"; + String s2 = "aac"; + assert(s1.compareTo(s2) == 1); + + assert(s2.compareTo(argv[0]) != -1); + + String s3 = "abc"; + assert(s3.hashCode() == s1.hashCode()); + assert(s3.hashCode() == s2.hashCode()); + + /*String x = s1.intern(); + String y = s3.intern(); + assert(x == y);*/ + } +} diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc new file mode 100644 index 00000000000..c6c0b193e5b --- /dev/null +++ b/regression/strings/java_concat/test.desc @@ -0,0 +1,8 @@ +CORE +test_concat.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_concat.java line 9: SUCCESS$ +^\[assertion.2\] assertion at file test_concat.java line 10: FAILURE$ +-- diff --git a/regression/strings/java_concat/test_concat.class b/regression/strings/java_concat/test_concat.class new file mode 100644 index 00000000000..a6d4008aa26 Binary files /dev/null and b/regression/strings/java_concat/test_concat.class differ diff --git a/regression/strings/java_concat/test_concat.java b/regression/strings/java_concat/test_concat.java new file mode 100644 index 00000000000..d714ea89538 --- /dev/null +++ b/regression/strings/java_concat/test_concat.java @@ -0,0 +1,12 @@ +public class test_concat { + + public static void main(String[] argv) { + String s = new String("pi"); + int i = s.length(); + String t = new String("ppo"); + String u = s.concat(t); + char c = u.charAt(i); + assert(c == 'p'); + assert(c == 'o'); + } +} diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc new file mode 100644 index 00000000000..ade6b433bf1 --- /dev/null +++ b/regression/strings/java_contains/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +test_contains.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_contains.java line 7: SUCCESS$ +^\[assertion.2\] assertion at file test_contains.java line 8: FAILURE$ +-- diff --git a/regression/strings/java_contains/test_contains.class b/regression/strings/java_contains/test_contains.class new file mode 100644 index 00000000000..855ab828393 Binary files /dev/null and b/regression/strings/java_contains/test_contains.class differ diff --git a/regression/strings/java_contains/test_contains.java b/regression/strings/java_contains/test_contains.java new file mode 100644 index 00000000000..fce2ee63047 --- /dev/null +++ b/regression/strings/java_contains/test_contains.java @@ -0,0 +1,10 @@ +public class test_contains { + + public static void main(String[] argv) { + String s = new String("Hello World!"); + String u = "o W"; + String t = "W o"; + assert(s.contains(u)); + assert(s.contains(t)); + } +} diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc new file mode 100644 index 00000000000..377ada44770 --- /dev/null +++ b/regression/strings/java_delete/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +test_delete.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_delete.java line 11: SUCCESS$ +^\[assertion.2\] assertion at file test_delete.java line 12: FAILURE$ +-- diff --git a/regression/strings/java_delete/test_delete.class b/regression/strings/java_delete/test_delete.class new file mode 100644 index 00000000000..6d30024f108 Binary files /dev/null and b/regression/strings/java_delete/test_delete.class differ diff --git a/regression/strings/java_delete/test_delete.java b/regression/strings/java_delete/test_delete.java new file mode 100644 index 00000000000..c91b16c5b89 --- /dev/null +++ b/regression/strings/java_delete/test_delete.java @@ -0,0 +1,15 @@ +public class test_delete { + + public static void main(String[] argv) { + StringBuilder s = new StringBuilder(); + s.append("Hello World!"); + s.delete(4,6); + s.deleteCharAt(1); + + String str = s.toString(); + System.out.println(str); + assert(str.equals("HllWorld!")); + assert(!str.equals("HllWorld!")); + + } +} diff --git a/regression/strings/java_easychair/easychair.class b/regression/strings/java_easychair/easychair.class new file mode 100644 index 00000000000..e47900cc0b2 Binary files /dev/null and b/regression/strings/java_easychair/easychair.class differ diff --git a/regression/strings/java_easychair/easychair.java b/regression/strings/java_easychair/easychair.java new file mode 100644 index 00000000000..55ca2a31bb3 --- /dev/null +++ b/regression/strings/java_easychair/easychair.java @@ -0,0 +1,34 @@ +public class easychair { + + public static void main(String[] argv) { + if(argv.length > 1){ + String str = new String(argv[1]); + if(str.length() < 40){ + + // containing "/" and containing "EasyChair" + int lastSlash = str.lastIndexOf('/'); + if(lastSlash < 0) return ; + + String rest = str.substring(lastSlash + 1); + // warning: removed this because contains is not efficient at the moment + if(! rest.contains("EasyChair")) return ; + // (2) Check that str starts with "http://" + if(! str.startsWith("http://")) return ; + // (3) Take the string between "http://" and the last "/". + // if it starts with "www." strip the "www." off + String t = str.substring("http://".length(),lastSlash - "http://".length()); + if(t.startsWith("www.")) + t = t.substring("www.".length()); + + // + //(4) Check that after stripping we have either "live.com" + // or "google.com" + if(!t.equals("live.com") && !t.equals("google.com")) + return ; + // s survived all checks + assert(false); //return true; + } + } + } + +} diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc new file mode 100644 index 00000000000..bd68fd1f60a --- /dev/null +++ b/regression/strings/java_easychair/test.desc @@ -0,0 +1,7 @@ +KNOWNBUG +easychair.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file easychair.java line 29: FAILURE$ +-- diff --git a/regression/strings/java_empty/test.desc b/regression/strings/java_empty/test.desc new file mode 100644 index 00000000000..56b21e2041c --- /dev/null +++ b/regression/strings/java_empty/test.desc @@ -0,0 +1,8 @@ +CORE +test_empty.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_empty.java line 4: SUCCESS$ +^\[assertion.2\] assertion at file test_empty.java line 5: FAILURE$ +-- diff --git a/regression/strings/java_empty/test_empty.class b/regression/strings/java_empty/test_empty.class new file mode 100644 index 00000000000..f0ced290ee3 Binary files /dev/null and b/regression/strings/java_empty/test_empty.class differ diff --git a/regression/strings/java_empty/test_empty.java b/regression/strings/java_empty/test_empty.java new file mode 100644 index 00000000000..2465fb16e41 --- /dev/null +++ b/regression/strings/java_empty/test_empty.java @@ -0,0 +1,7 @@ +public class test_empty { + public static void main(String[] argv) { + String empty = " "; + assert(empty.trim().isEmpty()); + assert(empty.isEmpty()); + } +} diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc new file mode 100644 index 00000000000..6375cfdc3d8 --- /dev/null +++ b/regression/strings/java_equal/test.desc @@ -0,0 +1,8 @@ +CORE +test_equal.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_equal.java line 7: FAILURE$ +^\[assertion.2\] assertion at file test_equal.java line 8: SUCCESS$ +-- diff --git a/regression/strings/java_equal/test_equal.class b/regression/strings/java_equal/test_equal.class new file mode 100644 index 00000000000..26ee19e6cb1 Binary files /dev/null and b/regression/strings/java_equal/test_equal.class differ diff --git a/regression/strings/java_equal/test_equal.java b/regression/strings/java_equal/test_equal.java new file mode 100644 index 00000000000..151162a106d --- /dev/null +++ b/regression/strings/java_equal/test_equal.java @@ -0,0 +1,10 @@ +public class test_equal { + + public static void main(String[] argv) { + String s = new String("pi"); + String t = new String("po"); + String u = "po"; + assert(s.equals(t)); + assert(t.equals(u)); + } +} diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc new file mode 100644 index 00000000000..47e915cda98 --- /dev/null +++ b/regression/strings/java_float/test.desc @@ -0,0 +1,10 @@ +CORE +test_float.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_float.java line 14: SUCCESS$ +^\[assertion.2\] assertion at file test_float.java line 15: SUCCESS$ +^\[assertion.3\] assertion at file test_float.java line 16: SUCCESS$ +^\[assertion.4\] assertion at file test_float.java line 17: FAILURE$ +-- \ No newline at end of file diff --git a/regression/strings/java_float/test_float.class b/regression/strings/java_float/test_float.class new file mode 100644 index 00000000000..356d0e17871 Binary files /dev/null and b/regression/strings/java_float/test_float.class differ diff --git a/regression/strings/java_float/test_float.java b/regression/strings/java_float/test_float.java new file mode 100644 index 00000000000..e59c631d91e --- /dev/null +++ b/regression/strings/java_float/test_float.java @@ -0,0 +1,20 @@ +public class test_float { + + public static void main(String[] arg) { + float inf = 100.0f / 0.0f; + float minus_inf = -100.0f / 0.0f; + float nan = 0.0f / 0.0f; + String inf_string = Float.toString(inf); + String mininf_string = Float.toString(minus_inf); + String nan_string = Float.toString(nan); + //String arg1 = arg[0]; + System.out.println(nan_string); + System.out.println(inf_string); + System.out.println(mininf_string); + assert(nan_string.equals("NaN")); + assert(inf_string.equals("Infinity")); + assert(mininf_string.equals("-Infinity")); + assert(!nan_string.equals("NaN") || !inf_string.equals("Infinity") + || !mininf_string.equals("-Infinity")); + } +} diff --git a/regression/strings/java_index_of/test.desc b/regression/strings/java_index_of/test.desc new file mode 100644 index 00000000000..dd5c60464d5 --- /dev/null +++ b/regression/strings/java_index_of/test.desc @@ -0,0 +1,16 @@ +CORE +test_index_of.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_index_of.java line 13: SUCCESS$ +^\[assertion.2\] assertion at file test_index_of.java line 14: FAILURE$ +^\[assertion.3\] assertion at file test_index_of.java line 17: SUCCESS$ +^\[assertion.4\] assertion at file test_index_of.java line 18: FAILURE$ +^\[assertion.5\] assertion at file test_index_of.java line 21: SUCCESS$ +^\[assertion.6\] assertion at file test_index_of.java line 22: FAILURE$ +^\[assertion.7\] assertion at file test_index_of.java line 25: SUCCESS$ +^\[assertion.8\] assertion at file test_index_of.java line 26: FAILURE$ +^\[assertion.9\] assertion at file test_index_of.java line 28: SUCCESS$ +^\[assertion.10\] assertion at file test_index_of.java line 29: SUCCESS$ +-- diff --git a/regression/strings/java_index_of/test_index_of.class b/regression/strings/java_index_of/test_index_of.class new file mode 100644 index 00000000000..8b3b7525f1a Binary files /dev/null and b/regression/strings/java_index_of/test_index_of.class differ diff --git a/regression/strings/java_index_of/test_index_of.java b/regression/strings/java_index_of/test_index_of.java new file mode 100644 index 00000000000..bbe06d279ec --- /dev/null +++ b/regression/strings/java_index_of/test_index_of.java @@ -0,0 +1,32 @@ +public class test_index_of { + + public static void main(String[] argv) { + String s = "Hello World!"; + char c = 'o'; + int i = s.indexOf(c); + int j = s.lastIndexOf('o'); + int k = s.indexOf(c,5); + int l = s.lastIndexOf(c,5); + int m = s.indexOf("lo"); + int n = s.lastIndexOf("lo"); + if(argv.length == 1){ + assert(i == 4); + assert(i != 4); + } + else if(argv.length == 2){ + assert(j == 7); + assert(j != 7); + } + else if(argv.length == 3){ + assert(k == 7); + assert(k != 7); + } + else if(argv.length == 4){ + assert(l == 4); + assert(l != 4); + } else { + assert(m != 2); + assert(n != 2); + } + } +} diff --git a/regression/strings/java_insert/test_insert.class b/regression/strings/java_insert/test_insert.class new file mode 100644 index 00000000000..5fa0f425061 Binary files /dev/null and b/regression/strings/java_insert/test_insert.class differ diff --git a/regression/strings/java_insert/test_insert.java b/regression/strings/java_insert/test_insert.java new file mode 100644 index 00000000000..6871a51716c --- /dev/null +++ b/regression/strings/java_insert/test_insert.java @@ -0,0 +1,19 @@ +public class test_insert { + + public static void main(String[] argv) { + int i = 123; + long j = 123; + char c = '/'; + boolean b = true; + StringBuilder sb = new StringBuilder("hello"); + sb.insert(2,i); + sb.insert(2,c); + sb.insert(2,j); + sb.insert(2,b); + sb.insert(2,"abc"); + String s = sb.toString(); + System.out.println(s); + assert(s.equals("heabctrue123/123llo")); + assert(!s.equals("heabctrue123/123llo")); + } +} diff --git a/regression/strings/java_insert/test_insert1.class b/regression/strings/java_insert/test_insert1.class new file mode 100644 index 00000000000..80091936cea Binary files /dev/null and b/regression/strings/java_insert/test_insert1.class differ diff --git a/regression/strings/java_insert/test_insert1.java b/regression/strings/java_insert/test_insert1.java new file mode 100644 index 00000000000..54e754302c5 --- /dev/null +++ b/regression/strings/java_insert/test_insert1.java @@ -0,0 +1,23 @@ +public class test_insert1 { + + public static void main(String[] argv) { + int i = 123; + long j = 123; + char c = '/'; + boolean b = true; + StringBuilder sb = new StringBuilder("hello"); + sb.insert(2,i); + + /* + sb.insert(2,c); + sb.insert(2,j); + sb.insert(2,b); + sb.insert(2,"abc"); + */ + String s = sb.toString(); + System.out.println(s); + assert(s.equals("he123llo")); + //assert(s.equals("heabctrue123/123llo")); + //assert(!s.equals("heabctrue123/123llo")); + } +} diff --git a/regression/strings/java_int/test.desc b/regression/strings/java_int/test.desc new file mode 100644 index 00000000000..5211656c61b --- /dev/null +++ b/regression/strings/java_int/test.desc @@ -0,0 +1,13 @@ +CORE +test_int.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_int.java line 8: SUCCESS$ +^\[assertion.2\] assertion at file test_int.java line 9: SUCCESS$ +^\[assertion.3\] assertion at file test_int.java line 12: SUCCESS$ +^\[assertion.4\] assertion at file test_int.java line 15: SUCCESS$ +^\[assertion.5\] assertion at file test_int.java line 18: SUCCESS$ +^\[assertion.6\] assertion at file test_int.java line 21: SUCCESS$ +^\[assertion.7\] assertion at file test_int.java line 23: FAILURE$ +-- diff --git a/regression/strings/java_int/test_int.class b/regression/strings/java_int/test_int.class new file mode 100644 index 00000000000..643d7eca09c Binary files /dev/null and b/regression/strings/java_int/test_int.class differ diff --git a/regression/strings/java_int/test_int.java b/regression/strings/java_int/test_int.java new file mode 100644 index 00000000000..620ae638dce --- /dev/null +++ b/regression/strings/java_int/test_int.java @@ -0,0 +1,25 @@ +public class test_int { + + public static void main(String[] argv) { + String s = Integer.toString(2345); + char c = s.charAt(1); + char d = s.charAt(2); + char e = s.charAt(3); + assert(c == '3'); + assert(d == '4'); + + int i = Integer.parseInt("1234"); + assert(i == 1234); + + String t = Integer.toString(-2345); + assert(t.charAt(0) == '-'); + + int j = Integer.parseInt("-4231"); + assert(j == -4231); + + String u = Integer.toHexString(43981); + assert(u.equals("abcd")); + + assert(e == '2' || i < 1234 || t.charAt(0) != '-' || j != -4231 || !u.equals("abcd")); + } +} diff --git a/regression/strings/java_prefix/test.desc b/regression/strings/java_prefix/test.desc new file mode 100644 index 00000000000..b234bba1788 --- /dev/null +++ b/regression/strings/java_prefix/test.desc @@ -0,0 +1,10 @@ +CORE +test_prefix.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_prefix.java line 14: SUCCESS$ +^\[assertion.2\] assertion at file test_prefix.java line 16: FAILURE$ +^\[assertion.3\] assertion at file test_prefix.java line 18: SUCCESS$ +^\[assertion.4\] assertion at file test_prefix.java line 20: FAILURE$ +-- diff --git a/regression/strings/java_prefix/test_prefix.class b/regression/strings/java_prefix/test_prefix.class new file mode 100644 index 00000000000..6f5f4025932 Binary files /dev/null and b/regression/strings/java_prefix/test_prefix.class differ diff --git a/regression/strings/java_prefix/test_prefix.java b/regression/strings/java_prefix/test_prefix.java new file mode 100644 index 00000000000..c9b5fa72fcf --- /dev/null +++ b/regression/strings/java_prefix/test_prefix.java @@ -0,0 +1,23 @@ +public class test_prefix { + + public static void main(String[] argv) { + String s = new String("Hello World!"); + //String t = new String("Hello"); + //String u = new String("Wello"); + String u = "Wello"; + boolean b = s.startsWith("Hello"); + //boolean c = s.startsWith("Wello"); + //boolean b = s.startsWith(t); + boolean c = s.startsWith(u); + boolean d = s.startsWith("lo",3); + if(argv.length == 1){ + assert(b); + } else if(argv.length == 2){ + assert(c); + } else if(argv.length == 3){ + assert(d); + } else if(argv.length == 4){ + assert(!d); + } + } +} diff --git a/regression/strings/java_replace/test.desc b/regression/strings/java_replace/test.desc new file mode 100644 index 00000000000..a5b15efd737 --- /dev/null +++ b/regression/strings/java_replace/test.desc @@ -0,0 +1,8 @@ +CORE +test_replace.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_replace.java line 6: SUCCESS$ +^\[assertion.2\] assertion at file test_replace.java line 8: FAILURE$ +-- diff --git a/regression/strings/java_replace/test_replace.class b/regression/strings/java_replace/test_replace.class new file mode 100644 index 00000000000..c795826dc15 Binary files /dev/null and b/regression/strings/java_replace/test_replace.class differ diff --git a/regression/strings/java_replace/test_replace.java b/regression/strings/java_replace/test_replace.java new file mode 100644 index 00000000000..342bf9afddc --- /dev/null +++ b/regression/strings/java_replace/test_replace.java @@ -0,0 +1,10 @@ +public class test_replace { + + public static void main(String[] argv) { + String s = new String("Hello World!"); + String t = s.replace('o','u'); + assert(t.equals("Hellu Wurld!")); + System.out.println(t); + assert(!t.equals("Hellu Wurld!")); + } +} diff --git a/regression/strings/java_set_length/test.desc b/regression/strings/java_set_length/test.desc new file mode 100644 index 00000000000..59204c9c5a8 --- /dev/null +++ b/regression/strings/java_set_length/test.desc @@ -0,0 +1,9 @@ +CORE +test_set_length.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_set_length.java line 8: SUCCESS$ +^\[assertion.2\] assertion at file test_set_length.java line 9: SUCCESS$ +^\[assertion.3\] assertion at file test_set_length.java line 10: FAILURE$ +-- \ No newline at end of file diff --git a/regression/strings/java_set_length/test_set_length.class b/regression/strings/java_set_length/test_set_length.class new file mode 100644 index 00000000000..8836640967a Binary files /dev/null and b/regression/strings/java_set_length/test_set_length.class differ diff --git a/regression/strings/java_set_length/test_set_length.java b/regression/strings/java_set_length/test_set_length.java new file mode 100644 index 00000000000..97b20f2332d --- /dev/null +++ b/regression/strings/java_set_length/test_set_length.java @@ -0,0 +1,12 @@ +public class test_set_length { + + public static void main(String[] argv) { + + StringBuilder s = new StringBuilder("abc"); + s.setLength(10); + String t = s.toString(); + assert(t.startsWith("abc")); + assert(t.length() == 10); + assert(t.length() == 3); + } +} diff --git a/regression/strings/java_string_builder/test.desc b/regression/strings/java_string_builder/test.desc new file mode 100644 index 00000000000..c0b3b6a51ce --- /dev/null +++ b/regression/strings/java_string_builder/test.desc @@ -0,0 +1,9 @@ +CORE +test_string_builder.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_string_builder.java line 11: SUCCESS$ +^\[assertion.2\] assertion at file test_string_builder.java line 12: SUCCESS$ +^\[assertion.3\] assertion at file test_string_builder.java line 13: FAILURE$ +-- diff --git a/regression/strings/java_string_builder/test_string_builder.class b/regression/strings/java_string_builder/test_string_builder.class new file mode 100644 index 00000000000..7a61d1f02be Binary files /dev/null and b/regression/strings/java_string_builder/test_string_builder.class differ diff --git a/regression/strings/java_string_builder/test_string_builder.java b/regression/strings/java_string_builder/test_string_builder.java new file mode 100644 index 00000000000..1d76b34e9f8 --- /dev/null +++ b/regression/strings/java_string_builder/test_string_builder.java @@ -0,0 +1,16 @@ +public class test_string_builder { + public static void main(String[] argv) { + if(argv.length > 2) { + StringBuilder tmp = new StringBuilder(); + tmp.append("prefix "); + tmp.append(argv[1]); + tmp.append(" middle ").append(argv[2]).append(" end"); + //StringBuilder tmp1 = tmp.append(argv[2]); + //tmp1.append(" end"); + String r = tmp.toString(); + assert(r.startsWith("pref")); + assert(r.endsWith("end")); + assert(r.startsWith("pr3f")); + } + } +} diff --git a/regression/strings/java_string_builder_length/test.desc b/regression/strings/java_string_builder_length/test.desc new file mode 100644 index 00000000000..a15660ee85b --- /dev/null +++ b/regression/strings/java_string_builder_length/test.desc @@ -0,0 +1,8 @@ +CORE +test_sb_length.class +--pass +^EXIT=10$ +^SIGNAL=0$ +\[assertion.1\] assertion at file test_sb_length.java line 6: SUCCESS$ +\[assertion.2\] assertion at file test_sb_length.java line 8: FAILURE$ +-- diff --git a/regression/strings/java_string_builder_length/test_sb_length.class b/regression/strings/java_string_builder_length/test_sb_length.class new file mode 100644 index 00000000000..586e8f71935 Binary files /dev/null and b/regression/strings/java_string_builder_length/test_sb_length.class differ diff --git a/regression/strings/java_string_builder_length/test_sb_length.java b/regression/strings/java_string_builder_length/test_sb_length.java new file mode 100644 index 00000000000..652b72cdc90 --- /dev/null +++ b/regression/strings/java_string_builder_length/test_sb_length.java @@ -0,0 +1,11 @@ +public class test_sb_length { + public static void main(String[] argv) { + StringBuilder tmp = new StringBuilder("prefix"); + //tmp.append("prefix"); + tmp.append("end"); + assert(tmp.length() == 9); + if(argv.length > 1) { + assert(tmp.length() == 12); + } + } +} diff --git a/regression/strings/java_strlen/test.desc b/regression/strings/java_strlen/test.desc new file mode 100644 index 00000000000..78007186493 --- /dev/null +++ b/regression/strings/java_strlen/test.desc @@ -0,0 +1,8 @@ +CORE +test_length.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_length.java line 10: SUCCESS$ +^\[assertion.2\] assertion at file test_length.java line 11: FAILURE$ +-- diff --git a/regression/strings/java_strlen/test_length.class b/regression/strings/java_strlen/test_length.class new file mode 100644 index 00000000000..7f1c10c02ca Binary files /dev/null and b/regression/strings/java_strlen/test_length.class differ diff --git a/regression/strings/java_strlen/test_length.java b/regression/strings/java_strlen/test_length.java new file mode 100644 index 00000000000..9410315db38 --- /dev/null +++ b/regression/strings/java_strlen/test_length.java @@ -0,0 +1,14 @@ +public class test_length { + + public static void main(String[] argv) { + String s = new String("hello"); + if(argv.length > 1) { + String t = argv[1]; + int i = t.length(); + String u = t.concat(s); + char c = u.charAt(i); + assert(c == 'h'); + assert(c == 'o'); + } + } +} diff --git a/regression/strings/java_substring/test.desc b/regression/strings/java_substring/test.desc new file mode 100644 index 00000000000..78a9bcca9cb --- /dev/null +++ b/regression/strings/java_substring/test.desc @@ -0,0 +1,10 @@ +CORE +test_substring.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_substring.java line 12: SUCCESS$ +^\[assertion.2\] assertion at file test_substring.java line 13: FAILURE$ +^\[assertion.3\] assertion at file test_substring.java line 20: SUCCESS$ +^\[assertion.4\] assertion at file test_substring.java line 21: FAILURE$ +-- diff --git a/regression/strings/java_substring/test_substring.class b/regression/strings/java_substring/test_substring.class new file mode 100644 index 00000000000..e6532aca43e Binary files /dev/null and b/regression/strings/java_substring/test_substring.class differ diff --git a/regression/strings/java_substring/test_substring.java b/regression/strings/java_substring/test_substring.java new file mode 100644 index 00000000000..8a2ac883cca --- /dev/null +++ b/regression/strings/java_substring/test_substring.java @@ -0,0 +1,27 @@ +public class test_substring { + + public static void main(String[] argv) { + if(argv.length > 1) { + String t = argv[1]; + + if(t.length() == 6) { + String u = t.substring(2,4); + char c = u.charAt(1); + char d = t.charAt(3); + char e = t.charAt(4); + assert(c == d); + assert(c == e); + } + else if(t.length() == 5){ + CharSequence u = t.subSequence(2,4); + char c = u.charAt(1); + char d = t.charAt(3); + char e = t.charAt(4); + assert(c == d); + assert(c == e); + } + + + } + } +} diff --git a/regression/strings/java_suffix/test.desc b/regression/strings/java_suffix/test.desc new file mode 100644 index 00000000000..f9472f03b47 --- /dev/null +++ b/regression/strings/java_suffix/test.desc @@ -0,0 +1,8 @@ +CORE +test_suffix.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_suffix.java line 12: SUCCESS$ +^\[assertion.2\] assertion at file test_suffix.java line 13: FAILURE$ +-- diff --git a/regression/strings/java_suffix/test_suffix.class b/regression/strings/java_suffix/test_suffix.class new file mode 100644 index 00000000000..557acd02653 Binary files /dev/null and b/regression/strings/java_suffix/test_suffix.class differ diff --git a/regression/strings/java_suffix/test_suffix.java b/regression/strings/java_suffix/test_suffix.java new file mode 100644 index 00000000000..f61b0b8ba36 --- /dev/null +++ b/regression/strings/java_suffix/test_suffix.java @@ -0,0 +1,15 @@ +public class test_suffix { + + public static void main(String[] argv) { + String s = new String("Hello World!"); + //String t = new String("Hello"); + //String u = new String("Wello"); + String u = "Wello!"; + boolean b = s.endsWith("World!"); + //boolean c = s.startsWith("Wello"); + //boolean b = s.startsWith(t); + boolean c = s.startsWith(u); + assert(b); + assert(c); + } +} diff --git a/regression/strings/java_trim/test.desc b/regression/strings/java_trim/test.desc new file mode 100644 index 00000000000..fa0e10a1ca7 --- /dev/null +++ b/regression/strings/java_trim/test.desc @@ -0,0 +1,8 @@ +CORE +test_trim.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_trim.java line 5: SUCCESS$ +^\[assertion.2\] assertion at file test_trim.java line 6: FAILURE$ +-- diff --git a/regression/strings/java_trim/test_trim.class b/regression/strings/java_trim/test_trim.class new file mode 100644 index 00000000000..8e6a923dcbc Binary files /dev/null and b/regression/strings/java_trim/test_trim.class differ diff --git a/regression/strings/java_trim/test_trim.java b/regression/strings/java_trim/test_trim.java new file mode 100644 index 00000000000..8d8d41cb29a --- /dev/null +++ b/regression/strings/java_trim/test_trim.java @@ -0,0 +1,8 @@ +public class test_trim { + public static void main(String[] argv) { + String t = " a b c "; + String x = t.trim(); + assert(x.equals("a b c")); + assert(x.equals("abc ")); + } +} diff --git a/regression/strings/test1/test.c b/regression/strings/test1/test.c new file mode 100644 index 00000000000..d3830e38a3f --- /dev/null +++ b/regression/strings/test1/test.c @@ -0,0 +1,18 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s; + __CPROVER_char c1, c2; + int i; + int j; + i = 2; + s = __CPROVER_string_literal("pippo"); + c1 = __CPROVER_char_at(s, i); + c2 = __CPROVER_char_literal("p"); + assert (c1 == c2); + assert (c1 != c2); + return 0; +} diff --git a/regression/strings/test1/test.desc b/regression/strings/test1/test.desc new file mode 100644 index 00000000000..3483081c0f0 --- /dev/null +++ b/regression/strings/test1/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion c1 == c2: SUCCESS$ +^\[main.assertion.2\] assertion c1 != c2: FAILURE$ +-- diff --git a/regression/strings/test2/test.c b/regression/strings/test2/test.c new file mode 100644 index 00000000000..aedc37ba3b3 --- /dev/null +++ b/regression/strings/test2/test.c @@ -0,0 +1,13 @@ +#include +#include "../cprover-string-hack.h" + +int main() +{ + __CPROVER_string s; + int n; + s = __CPROVER_string_literal("pippo"); + n = __CPROVER_string_length(s); + assert(n == 5); + assert(n != 5); + return 0; +} diff --git a/regression/strings/test2/test.desc b/regression/strings/test2/test.desc new file mode 100644 index 00000000000..d3054f813f1 --- /dev/null +++ b/regression/strings/test2/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion n == 5: SUCCESS$ +^\[main.assertion.2\] assertion n != 5: FAILURE$ +-- diff --git a/regression/strings/test3.1/test.c b/regression/strings/test3.1/test.c new file mode 100644 index 00000000000..e0d408322be --- /dev/null +++ b/regression/strings/test3.1/test.c @@ -0,0 +1,20 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s, s2, s3; + int i; + + s = __CPROVER_string_concat(s2, s3); + __CPROVER_assume(__CPROVER_string_length(s2) == i); + __CPROVER_assume(__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo"))); + + // proving the assertions individually seems to be much faster + assert(__CPROVER_string_length(s) == i + 5); + //assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"), s)); + //assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")); + + return 0; +} diff --git a/regression/strings/test3.1/test.desc b/regression/strings/test3.1/test.desc new file mode 100644 index 00000000000..0f5bd6ccca7 --- /dev/null +++ b/regression/strings/test3.1/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--pass +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings/test3.2/test.c b/regression/strings/test3.2/test.c new file mode 100644 index 00000000000..86d93224878 --- /dev/null +++ b/regression/strings/test3.2/test.c @@ -0,0 +1,22 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s, s2, s3; + int i; + + //__CPROVER_assume(i < 10); + //__CPROVER_assume(__CPROVER_string_equal(s3, __CPROVER_string_literal("pippo"))); + s3 = __CPROVER_string_literal("pippo"); + s = __CPROVER_string_concat(s2, s3); + __CPROVER_assume(__CPROVER_string_length(s2) == i); + + // proving the assertions individually seems to be much faster + //assert(__CPROVER_string_length(s) == i + 5); + assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s)); + //assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")); + + return 0; +} diff --git a/regression/strings/test3.2/test.desc b/regression/strings/test3.2/test.desc new file mode 100644 index 00000000000..0f5bd6ccca7 --- /dev/null +++ b/regression/strings/test3.2/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--pass +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings/test3.3/test.c b/regression/strings/test3.3/test.c new file mode 100644 index 00000000000..35e25d82ee5 --- /dev/null +++ b/regression/strings/test3.3/test.c @@ -0,0 +1,22 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s, s2, s3; + int i; + + s = __CPROVER_string_concat(s2, s3); + __CPROVER_assume(i < 10); + __CPROVER_assume(__CPROVER_string_length(s2) == i); + __CPROVER_assume( + __CPROVER_string_equal(s3, __CPROVER_string_literal("pippo"))); + + // proving the assertions individually seems to be much faster + //assert(__CPROVER_string_length(s) == i + 5); + //assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"), s)); + assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")); + + return 0; +} diff --git a/regression/strings/test3.3/test.desc b/regression/strings/test3.3/test.desc new file mode 100644 index 00000000000..0f5bd6ccca7 --- /dev/null +++ b/regression/strings/test3.3/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--pass +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings/test3.4/test.c b/regression/strings/test3.4/test.c new file mode 100644 index 00000000000..70931d803d1 --- /dev/null +++ b/regression/strings/test3.4/test.c @@ -0,0 +1,18 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s, s2, s3; + int i; + + s = __CPROVER_string_concat(s2, s3); + __CPROVER_assume(__CPROVER_string_length(s2) == i); + __CPROVER_assume( + __CPROVER_string_equal(s3, __CPROVER_string_literal("pippo"))); + + assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s)); + + return 0; +} diff --git a/regression/strings/test3.4/test.desc b/regression/strings/test3.4/test.desc new file mode 100644 index 00000000000..dbf3c40cfdb --- /dev/null +++ b/regression/strings/test3.4/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/strings/test3/test-bv-to-int-onebyone.smt2 b/regression/strings/test3/test-bv-to-int-onebyone.smt2 new file mode 100644 index 00000000000..61e490a72bf --- /dev/null +++ b/regression/strings/test3/test-bv-to-int-onebyone.smt2 @@ -0,0 +1,37 @@ +(set-option :produce-models true) +(set-logic ALL_SUPPORTED) + +(declare-fun s () String) +(declare-fun s2 () String) +(declare-fun s3 () String) + +(define-sort cprover.Pos () (_ BitVec 32)) +(define-fun cprover.ubv_to_int ((?x cprover.Pos)) Int (let ((bit0 (_ bv0 1))) + (+ (ite (= ((_ extract 0 0) ?x) bit0) 0 1) (ite (= ((_ extract 1 1) ?x) bit0) 0 2) (ite (= ((_ extract 2 2) ?x) bit0) 0 4) (ite (= ((_ extract 3 3) ?x) bit0) 0 8) (ite (= ((_ extract 4 4) ?x) bit0) 0 16) (ite (= ((_ extract 5 5) ?x) bit0) 0 32) (ite (= ((_ extract 6 6) ?x) bit0) 0 64) (ite (= ((_ extract 7 7) ?x) bit0) 0 128) (ite (= ((_ extract 8 8) ?x) bit0) 0 256) (ite (= ((_ extract 9 9) ?x) bit0) 0 512) (ite (= ((_ extract 10 10) ?x) bit0) 0 1024) (ite (= ((_ extract 11 11) ?x) bit0) 0 2048) (ite (= ((_ extract 12 12) ?x) bit0) 0 4096) (ite (= ((_ extract 13 13) ?x) bit0) 0 8192) (ite (= ((_ extract 14 14) ?x) bit0) 0 16384) (ite (= ((_ extract 15 15) ?x) bit0) 0 32768) (ite (= ((_ extract 16 16) ?x) bit0) 0 65536) (ite (= ((_ extract 17 17) ?x) bit0) 0 131072) (ite (= ((_ extract 18 18) ?x) bit0) 0 262144) (ite (= ((_ extract 19 19) ?x) bit0) 0 524288) (ite (= ((_ extract 20 20) ?x) bit0) 0 1048576) (ite (= ((_ extract 21 21) ?x) bit0) 0 2097152) (ite (= ((_ extract 22 22) ?x) bit0) 0 4194304) (ite (= ((_ extract 23 23) ?x) bit0) 0 8388608) (ite (= ((_ extract 24 24) ?x) bit0) 0 16777216) (ite (= ((_ extract 25 25) ?x) bit0) 0 33554432) (ite (= ((_ extract 26 26) ?x) bit0) 0 67108864) (ite (= ((_ extract 27 27) ?x) bit0) 0 134217728) (ite (= ((_ extract 28 28) ?x) bit0) 0 268435456) (ite (= ((_ extract 29 29) ?x) bit0) 0 536870912) (ite (= ((_ extract 30 30) ?x) bit0) 0 1073741824) (ite (= ((_ extract 31 31) ?x) bit0) 0 2147483648) 0))) + +(declare-fun bvi () cprover.Pos) +(define-fun i () Int (cprover.ubv_to_int bvi)) + +(assert (= s (str.++ s2 s3))) + +(assert (= (str.len s2) i)) +(assert (= s3 "pippo")) + +(define-fun p1 () Bool (= (str.len s) (+ i 5))) +(define-fun p2 () Bool (str.suffixof "po" s)) +(define-fun p3 () Bool (= (str.at s i) "p")) + +(push 1) +(assert (not p1)) +(check-sat) +(pop 1) + +(push 1) +(assert (not p2)) +(check-sat) +(pop 1) + +(push 1) +(assert (not p3)) +(check-sat) +(pop 1) diff --git a/regression/strings/test3/test-bv-to-int.smt2 b/regression/strings/test3/test-bv-to-int.smt2 new file mode 100644 index 00000000000..8e036a3aaa4 --- /dev/null +++ b/regression/strings/test3/test-bv-to-int.smt2 @@ -0,0 +1,25 @@ +(set-option :produce-models true) +(set-logic ALL_SUPPORTED) + +(declare-fun s () String) +(declare-fun s2 () String) +(declare-fun s3 () String) + +(define-sort cprover.Pos () (_ BitVec 32)) +(define-fun cprover.ubv_to_int ((?x cprover.Pos)) Int (let ((bit0 (_ bv0 1))) + (+ (ite (= ((_ extract 0 0) ?x) bit0) 0 1) (ite (= ((_ extract 1 1) ?x) bit0) 0 2) (ite (= ((_ extract 2 2) ?x) bit0) 0 4) (ite (= ((_ extract 3 3) ?x) bit0) 0 8) (ite (= ((_ extract 4 4) ?x) bit0) 0 16) (ite (= ((_ extract 5 5) ?x) bit0) 0 32) (ite (= ((_ extract 6 6) ?x) bit0) 0 64) (ite (= ((_ extract 7 7) ?x) bit0) 0 128) (ite (= ((_ extract 8 8) ?x) bit0) 0 256) (ite (= ((_ extract 9 9) ?x) bit0) 0 512) (ite (= ((_ extract 10 10) ?x) bit0) 0 1024) (ite (= ((_ extract 11 11) ?x) bit0) 0 2048) (ite (= ((_ extract 12 12) ?x) bit0) 0 4096) (ite (= ((_ extract 13 13) ?x) bit0) 0 8192) (ite (= ((_ extract 14 14) ?x) bit0) 0 16384) (ite (= ((_ extract 15 15) ?x) bit0) 0 32768) (ite (= ((_ extract 16 16) ?x) bit0) 0 65536) (ite (= ((_ extract 17 17) ?x) bit0) 0 131072) (ite (= ((_ extract 18 18) ?x) bit0) 0 262144) (ite (= ((_ extract 19 19) ?x) bit0) 0 524288) (ite (= ((_ extract 20 20) ?x) bit0) 0 1048576) (ite (= ((_ extract 21 21) ?x) bit0) 0 2097152) (ite (= ((_ extract 22 22) ?x) bit0) 0 4194304) (ite (= ((_ extract 23 23) ?x) bit0) 0 8388608) (ite (= ((_ extract 24 24) ?x) bit0) 0 16777216) (ite (= ((_ extract 25 25) ?x) bit0) 0 33554432) (ite (= ((_ extract 26 26) ?x) bit0) 0 67108864) (ite (= ((_ extract 27 27) ?x) bit0) 0 134217728) (ite (= ((_ extract 28 28) ?x) bit0) 0 268435456) (ite (= ((_ extract 29 29) ?x) bit0) 0 536870912) (ite (= ((_ extract 30 30) ?x) bit0) 0 1073741824) (ite (= ((_ extract 31 31) ?x) bit0) 0 2147483648) 0))) + +(declare-fun bvi () cprover.Pos) +(define-fun i () Int (cprover.ubv_to_int bvi)) + +(assert (= s (str.++ s2 s3))) + +(assert (= (str.len s2) i)) +(assert (= s3 "pippo")) + +(define-fun p1 () Bool (= (str.len s) (+ i 5))) +(define-fun p2 () Bool (str.suffixof "po" s)) +(define-fun p3 () Bool (= (str.at s i) "p")) + +(assert (or (not p1) (not p2) (not p3))) +(check-sat) diff --git a/regression/strings/test3/test-int.smt2 b/regression/strings/test3/test-int.smt2 new file mode 100644 index 00000000000..1cebe5cba31 --- /dev/null +++ b/regression/strings/test3/test-int.smt2 @@ -0,0 +1,20 @@ +(set-option :produce-models true) +(set-logic ALL_SUPPORTED) + +(declare-fun s () String) +(declare-fun s2 () String) +(declare-fun s3 () String) + +(declare-fun i () Int) + +(assert (= s (str.++ s2 s3))) + +(assert (= (str.len s2) i)) +(assert (= s3 "pippo")) + +(define-fun p1 () Bool (= (str.len s) (+ i 5))) +(define-fun p2 () Bool (str.suffixof "po" s)) +(define-fun p3 () Bool (= (str.at s i) "p")) + +(assert (or (not p1) (not p2) (not p3))) +(check-sat) diff --git a/regression/strings/test3/test.c b/regression/strings/test3/test.c new file mode 100644 index 00000000000..2fa4b22e017 --- /dev/null +++ b/regression/strings/test3/test.c @@ -0,0 +1,21 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s, s2, s3; + int i; + + s = __CPROVER_string_concat(s2, s3); + __CPROVER_assume(__CPROVER_string_length(s2) == i); + __CPROVER_assume( + __CPROVER_string_equal(s3, __CPROVER_string_literal("pippo"))); + + assert(__CPROVER_string_length(s) == i + 5); + assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s)); + assert(__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")); + assert(__CPROVER_string_issuffix(__CPROVER_string_literal("p!o"), s)); + + return 0; +} diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc new file mode 100644 index 00000000000..6cacec86a19 --- /dev/null +++ b/regression/strings/test3/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s) == i + 5: SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$ +^\[main.assertion.3\] assertion __CPROVER_uninterpreted_string_char_at_func(s, i) == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$ +^\[main.assertion.4\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"p!o\"), s): FAILURE$ +-- diff --git a/regression/strings/test4/test.c b/regression/strings/test4/test.c new file mode 100644 index 00000000000..d73324f8ef4 --- /dev/null +++ b/regression/strings/test4/test.c @@ -0,0 +1,17 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s; + int i; + int j; + i = 2; + s = __CPROVER_string_literal("pippo"); + if (__CPROVER_char_at(s, i) == __CPROVER_char_literal("p")) { + j = 1; + } + assert(j == 1); + return 0; +} diff --git a/regression/strings/test4/test.desc b/regression/strings/test4/test.desc new file mode 100644 index 00000000000..0f5bd6ccca7 --- /dev/null +++ b/regression/strings/test4/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--pass +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings/test5/test.c b/regression/strings/test5/test.c new file mode 100644 index 00000000000..812a20f3442 --- /dev/null +++ b/regression/strings/test5/test.c @@ -0,0 +1,14 @@ +#include +#include "../cprover-string-hack.h" + + +void main() +{ + __CPROVER_string x, y, z, w; + + if (__CPROVER_string_equal(z, __CPROVER_string_concat(x, y)) && + __CPROVER_string_equal(z, __CPROVER_string_concat(w, __CPROVER_string_literal("c"))) && + __CPROVER_string_equal(__CPROVER_string_concat(__CPROVER_string_literal("c"), y), __CPROVER_string_concat(__CPROVER_string_literal("c"), __CPROVER_string_concat(__CPROVER_string_literal("b"), __CPROVER_string_literal("c"))))) { + assert(0); + } +} diff --git a/regression/strings/test5/test.desc b/regression/strings/test5/test.desc new file mode 100644 index 00000000000..dbf3c40cfdb --- /dev/null +++ b/regression/strings/test5/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/strings/test_char_set/test.c b/regression/strings/test_char_set/test.c new file mode 100644 index 00000000000..61aaf9b768e --- /dev/null +++ b/regression/strings/test_char_set/test.c @@ -0,0 +1,14 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s = __CPROVER_string_literal("abc");; + char c = 'p'; + __CPROVER_string t = __CPROVER_char_set(s,1,c);; + + assert(__CPROVER_string_equal(t, __CPROVER_string_literal("apc"))); + assert(__CPROVER_string_equal(t, __CPROVER_string_literal("abc"))); + return 0; +} diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc new file mode 100644 index 00000000000..8cf42dda8f3 --- /dev/null +++ b/regression/strings/test_char_set/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("apc")): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func("abc")): FAILURE$ +-- diff --git a/regression/strings/test_concat/test.c b/regression/strings/test_concat/test.c new file mode 100644 index 00000000000..ceab520e960 --- /dev/null +++ b/regression/strings/test_concat/test.c @@ -0,0 +1,16 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s,t,u; + unsigned i = __CPROVER_string_length(s); + t = __CPROVER_string_literal("ppo"); + u = __CPROVER_string_concat(s, t); + __CPROVER_char c = __CPROVER_char_at(u,i); + + assert(c == __CPROVER_char_literal("p")); + assert(__CPROVER_char_at(u,2) == __CPROVER_char_literal("p")); + return 0; +} diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc new file mode 100644 index 00000000000..e5d8b30d6da --- /dev/null +++ b/regression/strings/test_concat/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion c == __CPROVER_uninterpreted_char_literal_func(\"p\"): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(u, 2) == __CPROVER_uninterpreted_char_literal_func(\"p\"): FAILURE$ +-- diff --git a/regression/strings/test_contains/test.c b/regression/strings/test_contains/test.c new file mode 100644 index 00000000000..9e7c627f3c4 --- /dev/null +++ b/regression/strings/test_contains/test.c @@ -0,0 +1,22 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s1 = __CPROVER_string_literal("a1"); + __CPROVER_string s2 = __CPROVER_string_literal("2b"); + __CPROVER_string t = __CPROVER_string_concat(s1, s2); + + int i = nondet_int(); + + + if(i==1) + assert(!__CPROVER_string_contains(t,__CPROVER_string_literal("3"))); + else if(i==2) + assert(__CPROVER_string_contains(t,__CPROVER_string_literal("12"))); + else if(i==3) + assert(!__CPROVER_string_contains(t,__CPROVER_string_literal("b"))); + + return 0; +} diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc new file mode 100644 index 00000000000..8275425c548 --- /dev/null +++ b/regression/strings/test_contains/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"3\")): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"12\")): SUCCESS$ +^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"b\")): FAILURE$ +-- diff --git a/regression/strings/test_easychair/test.c b/regression/strings/test_easychair/test.c new file mode 100644 index 00000000000..5d249225280 --- /dev/null +++ b/regression/strings/test_easychair/test.c @@ -0,0 +1,43 @@ +#include +#include "../cprover-string-hack.h" +#define false 0 +#define true 1 + +int main(){ + //IsEasyChairQuery + __CPROVER_string str; + // (1) check that str contains "/" followed by anything not + // containing "/" and containing "EasyChair" + int lastSlash = __CPROVER_string_last_index_of(str,__CPROVER_char_literal("/")); + if(lastSlash < 0) { + __CPROVER_assert(false,"PC1"); + return false; + } + + __CPROVER_string rest = __CPROVER_string_substring(str,lastSlash + 1, __CPROVER_string_length(str)-1); + + if(! __CPROVER_string_contains(rest,__CPROVER_string_literal("EasyChair"))) { + __CPROVER_assert(false,"PC2"); + return false; + } + + // (2) Check that str starts with "http://" + if(! __CPROVER_string_isprefix(__CPROVER_string_literal("http://"),str)) { + __CPROVER_assert(false,"PC3"); + return false; + } + //(3) Take the string between "http://" and the last "/". + // if it starts with "www." strip the "www." off + __CPROVER_string t = __CPROVER_string_substring(str,__CPROVER_string_length(__CPROVER_string_literal("http://")), lastSlash - __CPROVER_string_length(__CPROVER_string_literal("http://"))); + if(__CPROVER_string_isprefix(__CPROVER_string_literal("www."),t)) + t = __CPROVER_string_substring(t,__CPROVER_string_length(__CPROVER_string_literal("www.")), __CPROVER_string_length(t)-1); + // (4) Check that after stripping we have either "live.com" + // or "google.com" + if (!__CPROVER_string_equal(t,__CPROVER_string_literal("live.com")) && !__CPROVER_string_equal(t,__CPROVER_string_literal( "google.com"))) { + __CPROVER_assert(false,"PC4"); + return false; + } + // s survived all checks + return true; +} + diff --git a/regression/strings/test_equal/test.c b/regression/strings/test_equal/test.c new file mode 100644 index 00000000000..2f26689589d --- /dev/null +++ b/regression/strings/test_equal/test.c @@ -0,0 +1,13 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s; + s = __CPROVER_string_literal("pippo"); + assert(__CPROVER_string_equal(s, __CPROVER_string_literal("pippo"))); + assert(__CPROVER_string_equal(s, __CPROVER_string_literal("mippo"))); + + return 0; +} diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc new file mode 100644 index 00000000000..81ad6913856 --- /dev/null +++ b/regression/strings/test_equal/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"pippo\")): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(s, __CPROVER_uninterpreted_string_literal_func(\"mippo\")): FAILURE$ +-- diff --git a/regression/strings/test_index_of/test.c b/regression/strings/test_index_of/test.c new file mode 100644 index 00000000000..d64d3c2d66e --- /dev/null +++ b/regression/strings/test_index_of/test.c @@ -0,0 +1,20 @@ +#include +#include "../cprover-string-hack.h" +#define false 0 +#define true 1 + +int main(){ + __CPROVER_string str; + int firstSlash = __CPROVER_string_index_of(str,'/'); + //__CPROVER_char_literal("/")); + int lastSlash = __CPROVER_string_last_index_of(str,__CPROVER_char_literal("/")); + + __CPROVER_assume(__CPROVER_string_equal(str, __CPROVER_string_literal("abc/abc/abc"))); + + assert(firstSlash == 3); + assert(lastSlash == 7); + + assert(firstSlash != 3 || lastSlash != 7); + + return 0; +} diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc new file mode 100644 index 00000000000..af22cc2efb5 --- /dev/null +++ b/regression/strings/test_index_of/test.desc @@ -0,0 +1,9 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$ +^\[main.assertion.2\] assertion lastSlash == 7: SUCCESS$ +^\[main.assertion.3\] assertion firstSlash != 3 || lastSlash != 7: FAILURE$ +-- \ No newline at end of file diff --git a/regression/strings/test_int/test.c b/regression/strings/test_int/test.c new file mode 100644 index 00000000000..3f8f8651783 --- /dev/null +++ b/regression/strings/test_int/test.c @@ -0,0 +1,18 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s; + unsigned i = 10; + s = __CPROVER_string_of_int(123); + assert(__CPROVER_char_at(s,0) == '1'); + assert(__CPROVER_char_at(s,1) == '2'); + + unsigned j = __CPROVER_parse_int(__CPROVER_string_literal("234")); + + assert(j == 234); + assert(j < 233 || __CPROVER_char_at(s,2) == '4'); + return 0; +} diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc new file mode 100644 index 00000000000..e46e43ed936 --- /dev/null +++ b/regression/strings/test_int/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 0) == .1.: SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_char_at_func(s, 1) == .2.: SUCCESS$ +^\[main.assertion.3\] assertion j == 234: SUCCESS$ +^\[main.assertion.4\] assertion j < 233 || __CPROVER_uninterpreted_string_char_at_func(s, 2) == .4.: FAILURE$ +-- diff --git a/regression/strings/test_pass1/test.c b/regression/strings/test_pass1/test.c new file mode 100644 index 00000000000..0ec758c9f64 --- /dev/null +++ b/regression/strings/test_pass1/test.c @@ -0,0 +1,18 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string t; + __CPROVER_string s = __CPROVER_string_concat(t, t); + __CPROVER_assume(__CPROVER_string_equal(s, __CPROVER_string_literal("aa"))); + + assert(__CPROVER_string_equal(t,__CPROVER_string_literal("a"))); + assert(!__CPROVER_string_equal(t,__CPROVER_string_literal("a"))); + // Warning the following does not express the same thing, because + // equality can fail while the two sides represent the same thing: + //assert(t == __CPROVER_string_literal("a")); + //assert(t != __CPROVER_string_literal("a")); + return 0; +} diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc new file mode 100644 index 00000000000..2531c253510 --- /dev/null +++ b/regression/strings/test_pass1/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): SUCCESS +^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): FAILURE$ +^\*\* 1 of 2 failed (2 iterations)$ + diff --git a/regression/strings/test_pass_pc1/test.c b/regression/strings/test_pass_pc1/test.c new file mode 100644 index 00000000000..95dadef8c1d --- /dev/null +++ b/regression/strings/test_pass_pc1/test.c @@ -0,0 +1,18 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s1,s2; + __CPROVER_string t = __CPROVER_string_concat(s1, s2); + __CPROVER_assume(__CPROVER_string_isprefix(__CPROVER_string_literal("a1"),s1)); + + __CPROVER_assume(__CPROVER_string_contains(s2,__CPROVER_string_literal("12"))); + + __CPROVER_assume(__CPROVER_string_issuffix(__CPROVER_string_literal("cd"),t)); + + assert(__CPROVER_string_length(t) > 3); + assert(__CPROVER_string_length(t) > 4); + return 0; +} diff --git a/regression/strings/test_pass_pc3/test.c b/regression/strings/test_pass_pc3/test.c new file mode 100644 index 00000000000..e70b34b898d --- /dev/null +++ b/regression/strings/test_pass_pc3/test.c @@ -0,0 +1,16 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s1,s2,s3; + __CPROVER_string t = __CPROVER_string_concat(s1,__CPROVER_string_concat(s2, s3)); + __CPROVER_assume(__CPROVER_string_equal(t, __CPROVER_string_literal("aaaa"))); + __CPROVER_assume(__CPROVER_string_length(s1) >= __CPROVER_string_length(s2)); + __CPROVER_assume(__CPROVER_string_length(s2) >= __CPROVER_string_length(s3)); + + assert(__CPROVER_string_length(s3) == 0); + assert(__CPROVER_string_length(s3) < 2); + return 0; +} diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc new file mode 100644 index 00000000000..b4c45aee0ee --- /dev/null +++ b/regression/strings/test_pass_pc3/test.desc @@ -0,0 +1,9 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_length_func(s3) == 0: FAILURE$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_length_func(s3) < 2: SUCCESS$ +^VERIFICATION FAILED$ + diff --git a/regression/strings/test_prefix/test.c b/regression/strings/test_prefix/test.c new file mode 100644 index 00000000000..041a6a3ed41 --- /dev/null +++ b/regression/strings/test_prefix/test.c @@ -0,0 +1,17 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s = __CPROVER_string_literal("Hello World!"); + + //__CPROVER_assume(__CPROVER_string_equal(s, __CPROVER_string_literal("Hello World!"))); + + __CPROVER_bool b = __CPROVER_string_isprefix(__CPROVER_string_literal("Hello"),s); + __CPROVER_bool c = __CPROVER_string_isprefix(__CPROVER_string_literal("Wello"),s); + assert(b); + assert(c); + + return 0; +} diff --git a/regression/strings/test_prefix/test.desc b/regression/strings/test_prefix/test.desc new file mode 100644 index 00000000000..187565433e4 --- /dev/null +++ b/regression/strings/test_prefix/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion b: SUCCESS$ +^\[main.assertion.2\] assertion c: FAILURE$ +-- diff --git a/regression/strings/test_strlen/test.c b/regression/strings/test_strlen/test.c new file mode 100644 index 00000000000..d3a4348bd43 --- /dev/null +++ b/regression/strings/test_strlen/test.c @@ -0,0 +1,16 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s,t; + int len_s, len_t; + s = __CPROVER_string_literal("abc"); + t = __CPROVER_string_literal("xyz"); + len_s = __CPROVER_string_length(s); + len_t = __CPROVER_string_length(t); + assert(len_s == len_t); + assert(len_s == 2); + return 0; +} diff --git a/regression/strings/test_strlen/test.desc b/regression/strings/test_strlen/test.desc new file mode 100644 index 00000000000..a35e2499c9f --- /dev/null +++ b/regression/strings/test_strlen/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion len_s == len_t: SUCCESS$ +^\[main.assertion.2\] assertion len_s == 2: FAILURE$ +-- diff --git a/regression/strings/test_substring/test.c b/regression/strings/test_substring/test.c new file mode 100644 index 00000000000..d2c26eca01a --- /dev/null +++ b/regression/strings/test_substring/test.c @@ -0,0 +1,15 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s = __CPROVER_string_literal("abcdef"); + __CPROVER_string t = __CPROVER_string_substring(s,2,4); + + assert(__CPROVER_string_equal(t,__CPROVER_string_literal("cd"))); + assert(__CPROVER_string_equal(t,__CPROVER_string_literal("cc"))); + assert(!__CPROVER_string_equal(t,__CPROVER_string_literal("bc"))); + assert(!__CPROVER_string_equal(t,__CPROVER_string_literal("cd"))); + return 0; +} diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc new file mode 100644 index 00000000000..6fe9134b59d --- /dev/null +++ b/regression/strings/test_substring/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cc\")): FAILURE$ +^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"bc\")): SUCCESS$ +^\[main.assertion.4\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"cd\")): FAILURE$ +-- \ No newline at end of file diff --git a/regression/strings/test_suffix/test.c b/regression/strings/test_suffix/test.c new file mode 100644 index 00000000000..d28bde61712 --- /dev/null +++ b/regression/strings/test_suffix/test.c @@ -0,0 +1,15 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s; + + __CPROVER_assume(__CPROVER_string_equal(s, __CPROVER_string_literal("pippo"))); + + assert(__CPROVER_string_issuffix(__CPROVER_string_literal("po"),s)); + assert(__CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s)); + + return 0; +} diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc new file mode 100644 index 00000000000..e0e8af7704c --- /dev/null +++ b/regression/strings/test_suffix/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"po\"), s): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_uninterpreted_string_literal_func(\"pp\"), s): FAILURE$ +-- diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 3b0d7b5bc6a..0ac16a59fec 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -341,6 +342,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("refine-arithmetic", true); } + if(cmdline.isset("pass")) + { + options.set_option("pass", true); + } + if(cmdline.isset("max-node-refinement")) options.set_option("max-node-refinement", cmdline.get_value("max-node-refinement")); @@ -911,6 +917,12 @@ bool cbmc_parse_optionst::process_goto_program( status() << "Partial Inlining" << eom; goto_partial_inline(goto_functions, ns, ui_message_handler); + + if(cmdline.isset("pass")) { + status() << "PASS Preprocessing " << eom; + pass_preprocess(symbol_table, goto_functions); + } + // remove returns, gcc vectors, complex remove_returns(symbol_table, goto_functions); remove_vector(symbol_table, goto_functions); @@ -1175,6 +1187,7 @@ void cbmc_parse_optionst::help() " --yices use Yices\n" " --z3 use Z3\n" " --refine use refinement procedure (experimental)\n" + " --pass use pass procedure (experimental)\n" " --outfile filename output formula to given file\n" " --arrays-uf-never never turn arrays into uninterpreted functions\n" " --arrays-uf-always always turn arrays into uninterpreted functions\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 33fe0ba5175..397dff4cf2b 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -36,7 +36,7 @@ class optionst; "(no-sat-preprocessor)" \ "(no-pretty-names)(beautify)" \ "(fixedbv)" \ - "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)(aig)" \ + "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)(aig)(pass)" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ "(little-endian)(big-endian)" \ "(show-goto-functions)(show-loops)" \ diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 319b60fe08b..cdf2ed03fae 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -324,6 +325,29 @@ cbmc_solverst::solvert* cbmc_solverst::get_bv_refinement() /*******************************************************************\ +Function: cbmc_solverst::get_string_refinement + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +cbmc_solverst::solvert* cbmc_solverst::get_string_refinement() +{ + propt *prop; + prop=new satcheck_no_simplifiert(); + prop->set_message_handler(get_message_handler()); + + string_refinementt *string_refinement = new string_refinementt(ns, *prop); + string_refinement->set_ui(ui); + return new cbmc_solver_with_propt(string_refinement, prop); +} + +/*******************************************************************\ + Function: cbmc_solverst::get_smt1 Inputs: diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index e121b8fa2af..cc4a48dcb30 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -79,11 +79,14 @@ class cbmc_solverst:public messaget virtual std::unique_ptr get_solver() { solvert *solver; - if(options.get_bool_option("dimacs")) solver = get_dimacs(); else if(options.get_bool_option("refine")) solver = get_bv_refinement(); + else if(options.get_bool_option("pass")) { + std::cout << "PASS solver" << std::endl; + solver = get_string_refinement(); + } else if(options.get_bool_option("smt1")) solver = get_smt1(get_smt1_solver_type()); else if(options.get_bool_option("smt2")) @@ -111,6 +114,7 @@ class cbmc_solverst:public messaget solvert* get_default(); solvert* get_dimacs(); solvert* get_bv_refinement(); + solvert* get_string_refinement(); solvert* get_smt1(smt1_dect::solvert solver); solvert* get_smt2(smt2_dect::solvert solver); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 0b0119112f2..145b53d984f 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -16,7 +16,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \ goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ graphml_goto_trace.cpp remove_virtual_functions.cpp \ - class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp + class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \ + pass_preprocess.cpp INCLUDES= -I .. diff --git a/src/goto-programs/pass_preprocess.cpp b/src/goto-programs/pass_preprocess.cpp new file mode 100644 index 00000000000..b67edede518 --- /dev/null +++ b/src/goto-programs/pass_preprocess.cpp @@ -0,0 +1,424 @@ +/*******************************************************************\ + +Module: Preprocess a goto-programs so that calls to the java String + library are recognized by the PASS algorithm + +Author: Romain Brenguier + +Date: September 2016 + +\*******************************************************************/ + +#include +#include + +#include "pass_preprocess.h" + +#include +#include + +void make_string_function(symbol_tablet & symbol_table, goto_functionst & goto_functions, + goto_programt::instructionst::iterator & i_it, irep_idt function_name) { + // replace "lhs=s.charAt(x)" by "lhs=__CPROVER_uninterpreted_string_char_at(s,i)" + // Warning: in pass_preprocess::make_string_function: + // we should introduce an intermediary variable for each argument + code_function_callt &function_call=to_code_function_call(i_it->code); + code_typet old_type=to_code_type(function_call.function().type()); + + auxiliary_symbolt tmp_symbol; + //tmp_symbol.base_name=base_name; + tmp_symbol.is_static_lifetime=false; + tmp_symbol.mode=ID_java; + tmp_symbol.name=function_name; + // tmp_symbol.type=type; + tmp_symbol.type=old_type; + symbol_table.add(tmp_symbol); + // make sure it is in the function map + goto_functions.function_map[irep_idt(function_name)]; + + function_application_exprt rhs; + rhs.type()=old_type.return_type(); + rhs.add_source_location()=function_call.source_location(); + rhs.function()=symbol_exprt(function_name); + for(int i = 0; i < function_call.arguments().size(); i++) + rhs.arguments().push_back(replace_string_literals(symbol_table,goto_functions,function_call.arguments()[i])); + code_assignt assignment(function_call.lhs(), rhs); + assignment.add_source_location()=function_call.source_location(); + i_it->make_assignment(); + i_it->code=assignment; +} + +void make_string_function_of_assign(symbol_tablet & symbol_table, goto_functionst & goto_functions, + goto_programt::instructionst::iterator & i_it, irep_idt function_name){ + assert(i_it->is_assign()); + code_assignt &assign=to_code_assign(i_it->code); + typet old_type=assign.rhs().type(); + + auxiliary_symbolt tmp_symbol; + tmp_symbol.is_static_lifetime=false; + tmp_symbol.mode=ID_java; + tmp_symbol.name=function_name; + symbol_table.add(tmp_symbol); + + exprt rhs = replace_string_literals(symbol_table,goto_functions,assign.rhs().op0()); + /*function_application_exprt rhs; + rhs.type()=old_type; + rhs.add_source_location()=assign.source_location(); + rhs.function()=symbol_exprt(function_name); + rhs.arguments().push_back(address_of_exprt(assign.rhs().op0()));*/ + code_assignt assignment(assign.lhs(), rhs); + assignment.add_source_location()=assign.source_location(); + i_it->make_assignment(); + i_it->code=assignment; + goto_functions.function_map[irep_idt(function_name)]; +} + +void make_string_function_call(symbol_tablet & symbol_table, goto_functionst & goto_functions, + goto_programt::instructionst::iterator & i_it, irep_idt function_name){ + // replace "s.init(x)" by "s=__CPROVER_uninterpreted_string_literal(x)" + code_function_callt &function_call=to_code_function_call(i_it->code); + code_typet old_type=to_code_type(function_call.function().type()); + + auxiliary_symbolt tmp_symbol; + tmp_symbol.is_static_lifetime=false; + tmp_symbol.mode=ID_java; + tmp_symbol.name=function_name; + symbol_table.add(tmp_symbol); + + function_application_exprt rhs; + rhs.type()=function_call.arguments()[0].type(); + rhs.add_source_location()=function_call.source_location(); + rhs.function()=symbol_exprt(function_name); + for(int i = 1; i < function_call.arguments().size(); i++) + rhs.arguments().push_back(replace_string_literals(symbol_table,goto_functions,function_call.arguments()[i])); + code_assignt assignment(function_call.arguments()[0], rhs); + assignment.add_source_location()=function_call.source_location(); + i_it->make_assignment(); + i_it->code=assignment; + // make sure it is in the function map + goto_functions.function_map[irep_idt(function_name)]; +} + +void make_string_function_side_effect +(symbol_tablet & symbol_table, goto_functionst & goto_functions, + goto_programt & goto_program, goto_programt::instructionst::iterator & i_it, + irep_idt function_name, std::map & string_builders){ + // replace "s.append(x)" by "s=__CPROVER_uninterpreted_string_concat(s,x)" + code_function_callt &function_call=to_code_function_call(i_it->code); + code_typet old_type=to_code_type(function_call.function().type()); + + auxiliary_symbolt tmp_symbol; + tmp_symbol.is_static_lifetime=false; + tmp_symbol.mode=ID_java; + tmp_symbol.name=function_name; + symbol_table.add(tmp_symbol); + + function_application_exprt rhs; + typet return_type = function_call.arguments()[0].type(); + rhs.type()=return_type;//to_pointer_type(return_type).subtype(); + rhs.add_source_location()=function_call.source_location(); + rhs.function()=symbol_exprt(function_name); + for(int i = 0; i < function_call.arguments().size(); i++) + rhs.arguments().push_back(replace_string_literals(symbol_table,goto_functions,function_call.arguments()[i])); + //code_assignt assignment(dereference_exprt(function_call.arguments()[0]), rhs); + code_assignt assignment(function_call.arguments()[0], rhs); + //code_assignt assignment2(function_call.lhs(), function_call.arguments()[0]); + // add a mapping from the left hand side to the first argument + string_builders[function_call.lhs()]=function_call.arguments()[0]; + assignment.add_source_location()=function_call.source_location(); + i_it->make_assignment(); + i_it->code=assignment; + // make sure it is in the function map + goto_functions.function_map[irep_idt(function_name)]; + + //i_it = goto_program.insert_after(i_it); + //i_it->make_assignment(); + //i_it->code=assignment2; + // add a mapping from the left hand side to the first argument + //string_builders[function_call.lhs()]=function_call.arguments()[0]; +} + + + +bool has_java_string_type(const exprt &expr) +{ + const typet type = expr.type(); + if(type.id() == ID_pointer) { + pointer_typet pt = to_pointer_type(type); + typet subtype = pt.subtype(); + if(subtype.id() == ID_symbol) { + irep_idt tag = to_symbol_type(subtype).get_identifier(); + return (tag == irep_idt("java::java.lang.String")); + } else return false; + } else return false; +} +void replace_string_calls(symbol_tablet & symbol_table,goto_functionst & goto_functions, + goto_functionst::function_mapt::iterator f_it) +{ + goto_programt &goto_program=f_it->second.body; + // map several names of a string builder to a unique one + std::map string_builders; + + Forall_goto_program_instructions(i_it, goto_program) { + if(i_it->is_function_call()) { + + code_function_callt &function_call=to_code_function_call(i_it->code); + for(int i = 0; i < function_call.arguments().size(); i++) + if(string_builders.find(function_call.arguments()[i]) != string_builders.end()) + function_call.arguments()[i]= string_builders[function_call.arguments()[i]]; + + if(function_call.function().id()==ID_symbol){ + const irep_idt function_id= + to_symbol_expr(function_call.function()).get_identifier(); + + if(function_id == irep_idt("java::java.lang.String.charAt:(I)C") + || function_id == irep_idt("java::java.lang.StringBuilder.charAt:(I)C") + || function_id == irep_idt("java::java.lang.CharSequence.charAt:(I)C") + ) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_char_at_func); + } else if(function_id == irep_idt("java::java.lang.String.codePointAt:(I)I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_code_point_at_func); + } else if(function_id == irep_idt("java::java.lang.String.codePointBefore:(I)I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_code_point_before_func); + } else if(function_id == irep_idt("java::java.lang.String.codePointCount:(II)I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_code_point_count_func); + } else if(function_id == irep_idt("java::java.lang.String.offsetByCodePoints:(II)I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_offset_by_code_point_func); + + } else if(function_id == irep_idt("java::java.lang.String.hashCode:()I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_hash_code_func); + + } else if(function_id == irep_idt + ("java::java.lang.String.indexOf:(I)I") + || function_id == irep_idt + ("java::java.lang.String.indexOf:(II)I") + || function_id == irep_idt + ("java::java.lang.String.indexOf:(Ljava/lang/String;)I") + || function_id == irep_idt + ("java::java.lang.String.indexOf:(Ljava/lang/String;I)I") + ) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_index_of_func); + } else if(function_id == irep_idt + ("java::java.lang.String.lastIndexOf:(I)I") + || function_id == irep_idt + ("java::java.lang.String.lastIndexOf:(II)I") + || function_id == irep_idt + ("java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I") + || function_id == irep_idt + ("java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I") + ) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_last_index_of_func); + } else if(function_id == irep_idt("java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_concat_func); + } else if(function_id == irep_idt("java::java.lang.String.length:()I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_length_func); + } else if(function_id == irep_idt("java::java.lang.StringBuilder.length:()I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_length_func); + } else if(function_id == irep_idt("java::java.lang.String.equals:(Ljava/lang/Object;)Z")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_equal_func); + } else if(function_id == irep_idt("java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_equals_ignore_case_func); + } else if(function_id == irep_idt + ("java::java.lang.String.startsWith:(Ljava/lang/String;)Z") + || function_id == irep_idt + ("java::java.lang.String.startsWith:(Ljava/lang/String;I)Z") + ) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_startswith_func); + } else if(function_id == irep_idt("java::java.lang.String.endsWith:(Ljava/lang/String;)Z")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_endswith_func); + } else if(function_id == irep_idt("java::java.lang.String.substring:(II)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_substring_func); + } else if(function_id == irep_idt("java::java.lang.String.substring:(II)Ljava/lang/String;") + || function_id == irep_idt("java::java.lang.String.substring:(I)Ljava/lang/String;") + || function_id == irep_idt("java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;") + || function_id == irep_idt("java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;") + || function_id == irep_idt("java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;") + ) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_substring_func); + } else if(function_id == irep_idt("java::java.lang.String.trim:()Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_trim_func); + } else if(function_id == irep_idt("java::java.lang.String.toLowerCase:()Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_to_lower_case_func); + } else if(function_id == irep_idt("java::java.lang.String.toUpperCase:()Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_to_upper_case_func); + } else if(function_id == irep_idt("java::java.lang.String.replace:(CC)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_replace_func); + } else if(function_id == irep_idt("java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_contains_func); + } else if(function_id == irep_idt("java::java.lang.String.compareTo:(Ljava/lang/String;)I")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_compare_to_func); + } else if(function_id == irep_idt("java::java.lang.String.intern:()Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_intern_func); + } else if(function_id == irep_idt("java::java.lang.String.isEmpty:()Z")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_is_empty_func); + } else if(function_id == irep_idt("java::java.lang.String.toCharArray:()[C")) { + make_string_function(symbol_table, goto_functions, i_it,cprover_string_to_char_array_func); + } else if(function_id == irep_idt("java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_int_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.append:(J)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_long_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_bool_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_char_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_double_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.append:(F)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_float_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.appendCodePoint:(I)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it,cprover_string_concat_code_point_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.delete:(II)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions, goto_program, i_it,cprover_string_delete_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions, goto_program, i_it,cprover_string_delete_char_at_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.insert:(ILjava/lang/String;)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions, goto_program, i_it,cprover_string_insert_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions, goto_program, i_it,cprover_string_insert_int_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions, goto_program, i_it,cprover_string_insert_long_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;")) { + make_string_function_side_effect(symbol_table, goto_functions, goto_program, i_it,cprover_string_insert_char_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;") ) { + make_string_function_side_effect(symbol_table, goto_functions, goto_program, i_it,cprover_string_insert_bool_func,string_builders); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.setCharAt:(IC)V")) { + // warning: this should return void type + make_string_function_side_effect + (symbol_table, goto_functions, goto_program, i_it, + cprover_string_char_set_func,string_builders); + } else if(function_id == irep_idt("java::java.lang.StringBuilder.toString:()Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_copy_func); + } else if(function_id == irep_idt + ("java::java.lang.String.:(Ljava/lang/String;)V") + || function_id == irep_idt + ("java::java.lang.String.:(Ljava/lang/StringBuilder;)V")) { + make_string_function_call(symbol_table, goto_functions, i_it, + cprover_string_copy_func); + } else if(function_id == irep_idt + ("java::java.lang.StringBuilder.:(Ljava/lang/String;)V")) { + make_string_function_call(symbol_table, goto_functions, i_it, + cprover_string_copy_func); + } else if(function_id == irep_idt("java::java.lang.String.:()V")) { + make_string_function_call(symbol_table, goto_functions, i_it, + cprover_string_empty_string_func); + } else if(function_id == irep_idt("java::java.lang.StringBuilder.:()V")) { + make_string_function_call(symbol_table, goto_functions, i_it, + cprover_string_empty_string_func); + } else if(function_id == irep_idt + ("java::java.lang.Integer.toString:(I)Ljava/lang/String;") + || function_id == irep_idt + ("java::java.lang.String.valueOf:(I)Ljava/lang/String;") + ) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_of_int_func); + } else if(function_id == irep_idt + ("java::java.lang.Integer.toHexString:(I)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_of_int_hex_func); + } else if(function_id == irep_idt + ("java::java.lang.String.valueOf:(L)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_of_long_func); + } else if(function_id == irep_idt + ("java::java.lang.String.valueOf:(F)Ljava/lang/String;") + ||function_id == irep_idt + ("java::java.lang.Float.toString:(F)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_of_float_func); + } else if(function_id == irep_idt + ("java::java.lang.String.valueOf:(D)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_of_double_func); + } else if(function_id == irep_idt + ("java::java.lang.String.valueOf:(Z)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_of_bool_func); + } else if(function_id == irep_idt + ("java::java.lang.String.valueOf:(C)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_of_char_func); + + } else if(function_id == irep_idt + ("java::java.lang.Integer.parseInt:(Ljava/lang/String;)I")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_parse_int_func); + } else if(function_id == irep_idt + ("java::java.lang.String.valueOf:([CII)Ljava/lang/String;") + ||function_id == irep_idt + ("java::java.lang.String.valueOf:([C)Ljava/lang/String;") + ) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_value_of_func); + } else if(function_id == irep_idt("java::java.lang.StringBuilder.setLength:(I)V")) { + make_string_function_side_effect(symbol_table, goto_functions,goto_program, i_it, + cprover_string_set_length_func,string_builders); + } else if(function_id == irep_idt("java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)Ljava/lang/String;")) { + make_string_function(symbol_table, goto_functions, i_it, + cprover_string_format_func); + } + } + + } else { + if(i_it->is_assign()) { + code_assignt assignment = to_code_assign(i_it->code); + exprt new_rhs = replace_string_literals(symbol_table,goto_functions,assignment.rhs()); + code_assignt new_assignment(assignment.lhs(),new_rhs); + new_assignment.add_source_location()=assignment.source_location(); + i_it->make_assignment(); + i_it->code=new_assignment; + } + } + } + return; +} + +exprt replace_string_literals(symbol_tablet & symbol_table,goto_functionst & goto_functions, + const exprt & expr) { + if(has_java_string_type(expr) ) { + if(expr.operands().size() == 1 && expr.op0().id() ==ID_symbol) { + std::string id(to_symbol_expr(expr.op0()).get_identifier().c_str()); + if(id.substr(0,31) == "java::java.lang.String.Literal."){ + function_application_exprt rhs; + rhs.type()=expr.type(); + rhs.add_source_location()=expr.source_location(); + rhs.function()=symbol_exprt(cprover_string_literal_func); + goto_functions.function_map[cprover_string_literal_func]; + rhs.arguments().push_back(address_of_exprt(expr.op0())); + auxiliary_symbolt tmp_symbol; + tmp_symbol.is_static_lifetime=false; + tmp_symbol.mode=ID_java; + tmp_symbol.name=cprover_string_literal_func; + symbol_table.add(tmp_symbol); + return rhs; + } + } + } + return expr; +} + +void pass_preprocess(symbol_tablet & symbol_table, goto_functionst & goto_functions){ + Forall_goto_functions(it, goto_functions) + { + replace_string_calls(symbol_table,goto_functions,it); + } +} + + diff --git a/src/goto-programs/pass_preprocess.h b/src/goto-programs/pass_preprocess.h new file mode 100644 index 00000000000..c591ba2eced --- /dev/null +++ b/src/goto-programs/pass_preprocess.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: Preprocess a goto-programs so that calls to the java String + library are recognized by the PASS algorithm + +Author: Romain Brenguier + +Date: September 2016 + +\*******************************************************************/ + +#ifndef CPROVER_PASS_PREPROCESS_H +#define CPROVER_PASS_PREPROCESS_H + +#include + + +exprt replace_string_literals(symbol_tablet &, goto_functionst &,const exprt & ); +void pass_preprocess(symbol_tablet &, goto_functionst &); + +#endif diff --git a/src/solvers/Makefile b/src/solvers/Makefile index b806aa47886..4003e19c39a 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -118,6 +118,11 @@ SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \ floatbv/float_utils.cpp floatbv/float_bv.cpp \ refinement/bv_refinement_loop.cpp refinement/refine_arithmetic.cpp \ refinement/refine_arrays.cpp \ + refinement/string_constraint.cpp \ + refinement/string_functions.cpp \ + refinement/refined_string_type.cpp \ + refinement/string_expr.cpp \ + refinement/string_refinement.cpp \ miniBDD/miniBDD.cpp INCLUDES= -I .. \ diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index a97233dc11d..c41d8440d6c 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -334,11 +334,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr) } else if(expr.id()==ID_function_application) { - // record - functions.record(to_function_application_expr(expr)); - - // make it free bits - return prop.new_variables(boolbv_width(expr.type())); + return convert_function_application(to_function_application_expr(expr)); } else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and || expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand || @@ -502,6 +498,30 @@ bvt boolbvt::convert_symbol(const exprt &expr) return bv; } + + +/*******************************************************************\ + +Function: boolbvt::convert_function_application + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bvt boolbvt::convert_function_application( + const function_application_exprt &expr) +{ + // record + functions.record(expr); + + // make it free bits + return prop.new_variables(boolbv_width(expr.type())); +} + /*******************************************************************\ diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 714387f0dfb..f56cc4db294 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -169,6 +169,7 @@ class boolbvt:public arrayst virtual bvt convert_bv_reduction(const unary_exprt &expr); virtual bvt convert_not(const not_exprt &expr); virtual bvt convert_power(const binary_exprt &expr); + virtual bvt convert_function_application(const function_application_exprt &expr); virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest); virtual void make_free_bv_expr(const typet &type, exprt &dest); diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 69ca3b8e322..e4e5da7ce3c 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -83,8 +83,8 @@ class bv_refinementt:public bv_pointerst void get_values(approximationt &approximation); bool is_in_conflict(approximationt &approximation); - void check_SAT(); - void check_UNSAT(); + virtual void check_SAT(); + virtual void check_UNSAT(); bool progress; // we refine the theory of arrays diff --git a/src/solvers/refinement/refined_string_type.cpp b/src/solvers/refinement/refined_string_type.cpp new file mode 100644 index 00000000000..8f739ea2520 --- /dev/null +++ b/src/solvers/refinement/refined_string_type.cpp @@ -0,0 +1,76 @@ +/** -*- C++ -*- *****************************************************\ + +Module: Type of string expressions for PASS algorithm + (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include +#include + +refined_string_typet::refined_string_typet(unsignedbv_typet char_type) : struct_typet() { + components().resize(2); + components()[0].set_name("length"); + components()[0].set_pretty_name("length"); + components()[0].type()=refined_string_typet::index_type(); + + array_typet char_array(char_type,infinity_exprt(refined_string_typet::index_type())); + components()[1].set_name("content"); + components()[1].set_pretty_name("content"); + components()[1].type()=char_array; +} + +bool refined_string_typet::is_c_string_type(const typet &type) +{ + if (type.id() == ID_struct) { + irep_idt tag = to_struct_type(type).get_tag(); + return (tag == irep_idt("__CPROVER_string")); + } else return false; +} + +bool refined_string_typet::is_java_string_type(const typet &type) +{ + if(type.id() == ID_pointer) { + pointer_typet pt = to_pointer_type(type); + typet subtype = pt.subtype(); + return is_java_deref_string_type(subtype); + } else return false; +} + +bool refined_string_typet::is_java_deref_string_type(const typet &type) +{ + if(type.id() == ID_struct) { + irep_idt tag = to_struct_type(type).get_tag(); + return (tag == irep_idt("java.lang.String")); + } + else return false; +} + +bool refined_string_typet::is_java_string_builder_type(const typet &type) +{ + if(type.id() == ID_pointer) { + pointer_typet pt = to_pointer_type(type); + typet subtype = pt.subtype(); + if(subtype.id() == ID_struct) { + irep_idt tag = to_struct_type(subtype).get_tag(); + return (tag == irep_idt("java.lang.StringBuilder")); + } + else return false; + } else return false; +} + +bool refined_string_typet::is_java_char_sequence_type(const typet &type) +{ + if(type.id() == ID_pointer) { + pointer_typet pt = to_pointer_type(type); + typet subtype = pt.subtype(); + if(subtype.id() == ID_struct) { + irep_idt tag = to_struct_type(subtype).get_tag(); + return (tag == irep_idt("java.lang.CharSequence")); + } + else return false; + } else return false; +} + diff --git a/src/solvers/refinement/refined_string_type.h b/src/solvers/refinement/refined_string_type.h new file mode 100644 index 00000000000..3226587d912 --- /dev/null +++ b/src/solvers/refinement/refined_string_type.h @@ -0,0 +1,73 @@ +/** -*- C++ -*- *****************************************************\ + +Module: Type of string expressions for PASS algorithm + (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_SOLVER_REFINED_STRING_TYPE_H +#define CPROVER_SOLVER_REFINED_STRING_TYPE_H + +#include +#include + +#define STRING_SOLVER_INDEX_WIDTH 32 +#define STRING_SOLVER_CHAR_WIDTH 8 +#define JAVA_STRING_SOLVER_CHAR_WIDTH 16 + +// Internal type used for string refinement +class refined_string_typet : public struct_typet { +public: + refined_string_typet(unsignedbv_typet char_type); + + // Type for the content (list of characters) of a string + inline array_typet get_content_type() + { return to_array_type((to_struct_type(*this)).components()[1].type());} + + // Types used in this refinement + static inline unsignedbv_typet char_type() { return unsignedbv_typet(STRING_SOLVER_CHAR_WIDTH);} + + static inline unsignedbv_typet java_char_type() { return unsignedbv_typet(JAVA_STRING_SOLVER_CHAR_WIDTH);} + + static inline signedbv_typet index_type() { return signedbv_typet(STRING_SOLVER_INDEX_WIDTH);} + + static inline exprt index_zero() { return constant_exprt(integer2binary(0, STRING_SOLVER_INDEX_WIDTH), index_type());} + + // For C the unrefined string type is __CPROVER_string, for java it is a + // pointer to a strict with tag java.lang.String + + static bool is_c_string_type(const typet & type); + + static bool is_java_string_type(const typet & type); + + static bool is_java_deref_string_type(const typet & type); + + static bool is_java_string_builder_type(const typet & type); + + static bool is_java_char_sequence_type(const typet & type); + + static inline unsignedbv_typet get_char_type(const exprt & expr) { + if(is_c_string_type(expr.type())) return char_type(); + else return java_char_type(); + } + + static inline bool is_unrefined_string_type(const typet & type) + { return (is_c_string_type(type) + || is_java_string_type(type) + || is_java_string_builder_type(type) + || is_java_char_sequence_type(type) + ); } + + static inline bool is_unrefined_string(const exprt & expr) + { return (is_unrefined_string_type(expr.type())); } + + static inline constant_exprt index_of_int(int i) + { return constant_exprt(integer2binary(i, STRING_SOLVER_INDEX_WIDTH), + index_type()); } + +}; + + +#endif diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp new file mode 100644 index 00000000000..c6fbf6016db --- /dev/null +++ b/src/solvers/refinement/string_constraint.cpp @@ -0,0 +1,67 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String constraints + (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include + + +exprt string_constraintt::premise() const { + if(form == SIMPLE || form == UNIV_QUANT) { + if(id() == ID_implies) + return op0(); + else + return true_exprt(); + } + else { + return(*this); + } +} + +exprt string_constraintt::body() const { + if(form == SIMPLE || form == UNIV_QUANT) { + if(id() == ID_implies) + return op1(); + else + return(*this); + } else throw "string_constraintt::body() should not be applied to NOT_CONTAINS expression"; +} + +string_constraintt string_constraintt::forall(const symbol_exprt & univ, const exprt & bound_inf, const exprt & bound_sup) +{ + string_constraintt sc(*this); + sc.form = UNIV_QUANT; + sc.quantified_variable = univ; + sc.bounds.push_back(bound_inf); + sc.bounds.push_back(bound_sup); + return sc; +} + +string_constraintt string_constraintt::not_contains(exprt univ_bound_inf, exprt univ_bound_sup, + exprt premise, exprt exists_bound_inf, + exprt exists_bound_sup, exprt s0, exprt s1) +{ + string_constraintt sc(premise); + sc.form = NOT_CONTAINS; + sc.bounds.push_back(univ_bound_inf); + sc.bounds.push_back(univ_bound_inf); + sc.bounds.push_back(univ_bound_sup); + sc.bounds.push_back(exists_bound_inf); + sc.bounds.push_back(exists_bound_sup); + sc.compared_strings.push_back(s0); + sc.compared_strings.push_back(s1); + return sc; +} + +string_constraintt string_constraintt::exists(const symbol_exprt & exist, const exprt & bound_inf, const exprt & bound_sup) +{ + assert(is_simple() || is_string_constant()); + return string_constraintt + (and_exprt(*this, + and_exprt(binary_relation_exprt(exist, ID_ge, bound_inf), + binary_relation_exprt(exist, ID_lt, bound_sup)))); +} diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h new file mode 100644 index 00000000000..58c0211e2d5 --- /dev/null +++ b/src/solvers/refinement/string_constraint.h @@ -0,0 +1,105 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String constraints + (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_SOLVER_STRING_CONSTRAINT_H +#define CPROVER_SOLVER_STRING_CONSTRAINT_H + +#include +#include + +class string_constraintt : public exprt +{ +private: + // String axioms can have 4 different forms: + // either a simple expression p, + // or a string constant: forall x in [0,|s|[. s(x) = c(x) + // or universally quantified expression: forall x in [lb,ub[. p(x) + // or a expression for non containment: + // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y] + enum {SIMPLE, STRING_CONSTANT, UNIV_QUANT, NOT_CONTAINS} form; + + // Universally quantified symbol + symbol_exprt quantified_variable; + // Bounds on the quantified variables (alternate between inf and sup) + std::vector bounds; + // Only for NOT_CONTAINS constraints (represent s1 and s2) + std::vector compared_strings; + +public: + +// used to store information about witnesses for not_contains constraints + symbol_exprt witness; + + + // True axiom + string_constraintt() : exprt(true_exprt()) { form = SIMPLE; } + + // Axiom with no quantification, and no premise + string_constraintt(exprt bod, bool is_string_constant=false) : exprt(bod) { form = is_string_constant?SIMPLE:STRING_CONSTANT; } + + // Axiom with no quantification: prem => bod + string_constraintt(exprt prem, exprt bod) : exprt(implies_exprt(prem,bod)) + { form = SIMPLE; } + + // Add an universal quantifier + string_constraintt forall(const symbol_exprt & univ, const exprt & bound_inf, const exprt & bound_sup); + + // Bound a variable that is existentially quantified + string_constraintt exists(const symbol_exprt & exist, const exprt & bound_inf, const exprt & bound_sup); + + static string_constraintt not_contains + (exprt univ_lower_bound, exprt univ_bound_sup, exprt premise, + exprt exists_bound_inf, exprt exists_bound_sup, exprt s0, exprt s1); + + bool is_simple() const { return (form == SIMPLE); }; + bool is_string_constant() const { return (form == STRING_CONSTANT); }; + bool is_univ_quant() const { return (form == UNIV_QUANT); }; + bool is_not_contains() const { return (form == NOT_CONTAINS); }; + + exprt premise() const; + + exprt body() const; + + inline exprt s0() const { assert(is_not_contains()); return compared_strings[0];} + inline exprt s1() const { assert(is_not_contains()); return compared_strings[1];} + + + inline symbol_exprt get_univ_var() const { assert(form==UNIV_QUANT); return quantified_variable;} + inline exprt univ_bound_inf() const { return bounds[0]; } + inline exprt univ_bound_sup() const { return bounds[1]; } + inline exprt univ_within_bounds() const + { return and_exprt(binary_relation_exprt(bounds[0],ID_le,get_univ_var()), + binary_relation_exprt(bounds[1],ID_gt,get_univ_var())); } + inline exprt exists_bound_inf() const { return bounds[2]; } + inline exprt exists_bound_sup() const { return bounds[3]; } + + inline exprt witness_of(const exprt & univ_val) const { return index_exprt(witness, univ_val); } + + + // Warning: this assumes a simple form + inline string_constraintt operator&&(const exprt & a) { + assert(form == SIMPLE); + return string_constraintt(and_exprt(*this, a)); + } + + inline string_constraintt operator||(const exprt & a) { + assert(form == SIMPLE); + return string_constraintt(or_exprt(*this, a)); + } + + inline string_constraintt operator!() { + assert(form == SIMPLE); + return string_constraintt(not_exprt(*this)); + } + + +}; + + +#endif diff --git a/src/solvers/refinement/string_expr.cpp b/src/solvers/refinement/string_expr.cpp new file mode 100644 index 00000000000..24a883e0b8a --- /dev/null +++ b/src/solvers/refinement/string_expr.cpp @@ -0,0 +1,1210 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String expressions for PASS algorithm + (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +exprt index_zero = refined_string_typet::index_zero(); +unsigned string_exprt::next_symbol_id = 1; + +symbol_exprt string_exprt::fresh_symbol(const irep_idt &prefix, + const typet &tp) +{ + std::ostringstream buf; + buf << "string_refinement#" << prefix << "#" << (next_symbol_id++); + std::string s = buf.str(); + irep_idt name(s.c_str()); + return symbol_exprt(name, tp); +} + +constant_exprt constant_of_nat(int i,int width, typet t) { + return constant_exprt(integer2binary(i,width), t); +} + +string_exprt::string_exprt(unsignedbv_typet char_type) : struct_exprt(refined_string_typet(char_type)) +{ + refined_string_typet t(char_type); + symbol_exprt length = fresh_symbol("string_length",refined_string_typet::index_type()); + symbol_exprt content = fresh_symbol("string_content",t.get_content_type()); + move_to_operands(length,content); +} + + +void string_exprt::of_if(const if_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + assert(refined_string_typet::is_unrefined_string_type(expr.true_case().type())); + string_exprt t = of_expr(expr.true_case(),symbol_to_string,axioms); + assert(refined_string_typet::is_unrefined_string_type(expr.false_case().type())); + string_exprt f = of_expr(expr.false_case(),symbol_to_string,axioms); + + axioms.emplace_back(expr.cond(),equal_exprt(length(),t.length())); + symbol_exprt qvar = fresh_symbol("string_if_true",refined_string_typet::index_type()); + axioms.push_back(string_constraintt(expr.cond(),equal_exprt((*this)[qvar],t[qvar])).forall(qvar,index_zero,t.length())); + + axioms.emplace_back(not_exprt(expr.cond()),equal_exprt(length(),f.length())); + symbol_exprt qvar2 = fresh_symbol("string_if_false",refined_string_typet::index_type()); + axioms.push_back(string_constraintt(not_exprt(expr.cond()),equal_exprt((*this)[qvar2],f[qvar2])).forall(qvar2,index_zero,f.length())); +} + + +string_exprt string_exprt::get_string_of_symbol(std::map & symbol_to_string, const symbol_exprt & sym) { + if(refined_string_typet::is_c_string_type(sym.type())) { + irep_idt id = sym.get_identifier(); + std::map::iterator f = symbol_to_string.find(id); + if(f == symbol_to_string.end()) { + symbol_to_string[id]= string_exprt(refined_string_typet::char_type()); + return symbol_to_string[id]; + } else return f->second; + } else { // otherwise we assume it is a java string + irep_idt id = sym.get_identifier(); + std::map::iterator f = symbol_to_string.find(id); + if(f == symbol_to_string.end()) { + symbol_to_string[id]= string_exprt(refined_string_typet::java_char_type()); + return symbol_to_string[id]; + } else return f->second; + } + +} + +string_exprt string_exprt::of_expr(const exprt & unrefined_string, std::map & symbol_to_string, axiom_vect & axioms) +{ + unsignedbv_typet char_type; + + if(refined_string_typet::is_c_string_type(unrefined_string.type())) + char_type = refined_string_typet::char_type(); + else + char_type = refined_string_typet::java_char_type(); + + string_exprt s(char_type); + + if(unrefined_string.id()==ID_function_application) + s.of_function_application(to_function_application_expr(unrefined_string), symbol_to_string,axioms); + else if(unrefined_string.id()==ID_symbol) + s = get_string_of_symbol(symbol_to_string,to_symbol_expr(unrefined_string)); + else if(unrefined_string.id()==ID_address_of) { + assert(unrefined_string.op0().id()==ID_symbol); + s = get_string_of_symbol(symbol_to_string,to_symbol_expr(unrefined_string.op0())); + } + else if(unrefined_string.id()==ID_if) + s.of_if(to_if_expr(unrefined_string),symbol_to_string,axioms); + else if(unrefined_string.id()==ID_nondet_symbol || unrefined_string.id()==ID_struct) { + // We ignore non deterministic symbols and struct + } + else + throw ("string_exprt of:\n" + unrefined_string.pretty() + + "\nwhich is not a function application, a symbol or an if expression"); + + axioms.emplace_back(s >= index_zero); + return s; +} + +void string_exprt::of_function_application(const function_application_exprt & expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const exprt &name = expr.function(); + if (name.id() == ID_symbol) { + const irep_idt &id = to_symbol_expr(name).get_identifier(); + if(starts_with(id,cprover_string_literal_func)) + return of_string_literal(expr,axioms); + else if(starts_with(id,cprover_string_concat_func)) + return of_string_concat(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_concat_int_func)) + return of_string_concat_int(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_concat_long_func)) + return of_string_concat_long(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_concat_bool_func)) + return of_string_concat_bool(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_concat_char_func)) + return of_string_concat_char(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_concat_double_func)) + return of_string_concat_double(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_concat_float_func)) + return of_string_concat_float(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_concat_code_point_func)) + return of_string_concat_code_point(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_insert_func)) + return of_string_insert(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_insert_int_func)) + return of_string_insert_int(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_insert_long_func)) + return of_string_insert_long(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_insert_bool_func)) + return of_string_insert_bool(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_insert_char_func)) + return of_string_insert_char(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_insert_double_func)) + return of_string_insert_double(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_insert_float_func)) + return of_string_insert_float(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_substring_func)) + return of_string_substring(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_trim_func)) + return of_string_trim(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_to_lower_case_func)) + return of_string_to_lower_case(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_to_upper_case_func)) + return of_string_to_upper_case(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_char_set_func)) + return of_string_char_set(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_value_of_func)) + return of_string_value_of(expr,axioms); + else if(starts_with(id,cprover_string_empty_string_func)) + return of_empty_string(expr,axioms); + else if(starts_with(id,cprover_string_copy_func)) + return of_string_copy(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_of_int_func)) + return of_int(expr,axioms); + else if(starts_with(id,cprover_string_of_int_hex_func)) + return of_int_hex(expr,axioms); + else if(starts_with(id,cprover_string_of_float_func)) + return of_float(expr,axioms); + else if(starts_with(id,cprover_string_of_double_func)) + return of_double(expr,axioms); + else if(starts_with(id,cprover_string_of_long_func)) + return of_long(expr,axioms); + else if(starts_with(id,cprover_string_of_bool_func)) + return of_bool(expr,axioms); + else if(starts_with(id,cprover_string_of_char_func)) + return of_char(expr,axioms); + else if(starts_with(id,cprover_string_set_length_func)) + return of_string_set_length(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_delete_func)) + return of_string_delete(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_delete_char_at_func)) + return of_string_delete_char_at(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_replace_func)) + return of_string_replace(expr,symbol_to_string,axioms); + else if(starts_with(id,cprover_string_format_func)) + return of_string_format(expr,symbol_to_string,axioms); + else { + std::string msg("string_exprt::of_function_application: unknown symbol :"); + msg+=id.c_str(); + throw msg; + } + } + throw "string_exprt::of_function_application: not a string function"; +} + +irep_idt string_exprt::extract_java_string(const symbol_exprt & s){ + std::string tmp(s.get(ID_identifier).c_str()); + std::string value = tmp.substr(31); + return irep_idt(value); +} + +void string_exprt::of_string_constant(irep_idt sval, int char_width, unsignedbv_typet char_type, axiom_vect &axioms){ + + std::string str = sval.c_str(); + // should only do this for java + std::wstring utf16 = utf8_to_utf16(str); + // warning: endianness should be used as a flag when using this function + + for (std::size_t i = 0; i < utf16.size(); ++i) { + std::string idx_binary = integer2binary(i,STRING_SOLVER_INDEX_WIDTH); + constant_exprt idx(idx_binary, refined_string_typet::index_type()); + // warning: this should disappear if utf8_to_utf16 takes into account endianness + wchar_t big_endian = ((utf16[i] << 8) & 0xFF00) | (utf16[i] >> 8); + + std::string sval_binary=integer2binary((unsigned)big_endian, char_width); + constant_exprt c(sval_binary,char_type); + equal_exprt lemma(index_exprt(content(), idx), c); + axioms.emplace_back(lemma,true); + } + + std::string s_length_binary = integer2binary(unsigned(utf16.size()),STRING_SOLVER_INDEX_WIDTH); + exprt s_length = constant_exprt(s_length_binary, refined_string_typet::index_type()); + + axioms.emplace_back(equal_exprt(length(),s_length)); +} + +void string_exprt::of_empty_string(const function_application_exprt &f, axiom_vect & axioms) +{ + assert(f.arguments().size() == 0); + axioms.emplace_back(equal_exprt(length(),index_zero)); +} + +void string_exprt::of_string_literal(const function_application_exprt &f, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 1); //bad args to string literal? + const exprt &arg = args[0]; + + irep_idt sval; + int char_width; + unsignedbv_typet char_type; + + if (arg.operands().size() == 1 && + arg.op0().operands().size() == 1 && + arg.op0().op0().operands().size() == 2 && + arg.op0().op0().op0().id() == ID_string_constant) { + // C string constant + + const exprt &s = arg.op0().op0().op0(); + sval = to_string_constant(s).get_value(); + char_width = STRING_SOLVER_CHAR_WIDTH; + char_type = refined_string_typet::char_type(); + + } else { + // Java string constant + assert (arg.operands().size() == 1); + assert(refined_string_typet::is_unrefined_string_type(arg.type())); + const exprt &s = arg.op0(); + + //it seems the value of the string is lost, we need to recover it from the identifier + sval = extract_java_string(to_symbol_expr(s)); + char_width = JAVA_STRING_SOLVER_CHAR_WIDTH; + char_type = refined_string_typet::java_char_type(); + } + + of_string_constant(sval,char_width,char_type,axioms); +} + + +void string_exprt::of_string_concat(const string_exprt & s1, const string_exprt & s2, axiom_vect & axioms) { + equal_exprt length_sum_lem(length(), plus_exprt(s1.length(), s2.length())); + axioms.emplace_back(length_sum_lem); + + symbol_exprt idx = fresh_symbol("QA_index_concat",refined_string_typet::index_type()); + + string_constraintt a1(equal_exprt(s1[idx],(*this)[idx])); + axioms.push_back(a1.forall(idx, index_zero, s1.length())); + + + symbol_exprt idx2 = fresh_symbol("QA_index_concat2",refined_string_typet::index_type()); + + string_constraintt a2(equal_exprt(s2[idx2],(*this)[plus_exprt(idx2,s1.length())])); + axioms.push_back(a2.forall(idx2, index_zero, s2.length())); +} + +void string_exprt::of_string_concat(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); //bad args to string concat + + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2 = string_exprt::of_expr(args[1],symbol_to_string,axioms); + + of_string_concat(s1, s2, axioms); +} + + + +void string_exprt::of_string_copy(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 1); + + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + axioms.emplace_back(equal_exprt(length(), s1.length())); + symbol_exprt idx = fresh_symbol("QA_index_copy",refined_string_typet::index_type()); + string_constraintt a1(equal_exprt(s1[idx],(*this)[idx])); + axioms.push_back(a1.forall(idx, index_zero, s1.length())); +} + +void string_exprt::of_string_set_length(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + + bool is_c_string = refined_string_typet::is_c_string_type(f.type()); + exprt null_char; + if(is_c_string) + null_char = constant_of_nat(0,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + else + null_char = constant_of_nat(0,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + + // |s| = k + // && forall i < |s|. (i < k ==> s[i] = s1[i]) && (i >= k ==> s[i] = 0) + + axioms.emplace_back(equal_exprt(length(), args[1])); + symbol_exprt idx = fresh_symbol("QA_index_set_length",refined_string_typet::index_type()); + + + string_constraintt a1 + (and_exprt(implies_exprt(s1 > idx, equal_exprt(s1[idx],(*this)[idx])), + implies_exprt(s1 <= idx, equal_exprt(s1[idx],null_char)))); + axioms.push_back(a1.forall(idx, index_zero, (*this).length())); +} + + + +void string_exprt::of_java_char_array(const exprt & char_array, axiom_vect & axioms) +{ + exprt arr = to_address_of_expr(char_array).object(); + exprt len = member_exprt(arr, "length",length().type()); + exprt cont = member_exprt(arr, "data",content().type()); + op0() = len; + op1() = cont; +} + + +void string_exprt::of_string_value_of(const function_application_exprt &f, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = f.arguments(); + if(args.size() == 3) + { + exprt char_array = args[0]; + exprt offset = args[1]; + exprt count = args[2]; + string_exprt str(refined_string_typet::java_char_type()); + str.of_java_char_array(args[0],axioms); + axioms.emplace_back(equal_exprt(length(), count)); + + symbol_exprt idx = fresh_symbol("QA_index_value_of",refined_string_typet::index_type()); + string_constraintt a1(equal_exprt(str[plus_exprt(idx,offset)],(*this)[idx])); + axioms.push_back(a1.forall(idx, index_zero, count)); + } + else + { + assert(args.size() == 1); + of_java_char_array(args[0],axioms); + } +} + +void string_exprt::of_string_substring +(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() >= 2); + + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + + exprt i(args[1]); + + exprt j; + if(args.size() == 3) j = args[2]; + else j = str.length(); + + of_string_substring(str,i,j,symbol_to_string,axioms); +} + +void string_exprt::of_string_substring + (const string_exprt & str, const exprt & start, const exprt & end, std::map & symbol_to_string, axiom_vect & axioms) +{ + symbol_exprt idx = fresh_symbol("index_substring", refined_string_typet::index_type()); + assert(start.type() == refined_string_typet::index_type()); + assert(end.type() == refined_string_typet::index_type()); + + axioms.emplace_back(equal_exprt(length(), minus_exprt(end, start))); + axioms.emplace_back(binary_relation_exprt(start, ID_lt, end)); + axioms.emplace_back(str >= end); + + // forall idx < str.length, str[idx] = arg_str[idx+i] + string_constraintt a(equal_exprt((*this)[idx], str[plus_exprt(start, idx)])); + + axioms.push_back(a.forall(idx,index_zero,length())); +} + +void string_exprt::of_string_trim +(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() == 1); + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + symbol_exprt idx = fresh_symbol("index_trim", refined_string_typet::index_type()); + + bool is_c_string = refined_string_typet::is_c_string_type(expr.type()); + exprt space_char; + if(is_c_string) + space_char = constant_of_nat(32,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + else + space_char = constant_of_nat(32,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + + // m + |s1| <= |str| + axioms.emplace_back(str >= plus_exprt(idx, length())); + axioms.emplace_back(binary_relation_exprt(idx, ID_ge, index_zero)); + axioms.emplace_back(str >= idx); + axioms.emplace_back(str >= length()); + ///axioms.emplace_back(binary_relation_exprt(length(), ID_gt, index_zero)); + + symbol_exprt n = fresh_symbol("QA_index_trim",refined_string_typet::index_type()); + // forall n < m, str[n] = ' ' + string_constraintt a(equal_exprt(str[n], space_char)); + axioms.push_back(a.forall(n,index_zero,idx)); + + symbol_exprt n2 = fresh_symbol("QA_index_trim2",refined_string_typet::index_type()); + // forall n < |str|-m-|s1|, str[m+|s1|+n] = ' ' + string_constraintt a1(equal_exprt(str[plus_exprt(idx,plus_exprt(length(),n2))], space_char)); + axioms.push_back(a1.forall(n2,index_zero,minus_exprt(str.length(),plus_exprt(idx,length())))); + + symbol_exprt n3 = fresh_symbol("QA_index_trim3",refined_string_typet::index_type()); + // forall n < |s1|, s[idx+n] = s1[n] + string_constraintt a2(equal_exprt((*this)[n3], str[plus_exprt(n3, idx)])); + axioms.push_back(a2.forall(n3,index_zero,length())); + // (s[m] != ' ' && s[m+|s1|-1] != ' ') || m = |s| + or_exprt m_index_condition(equal_exprt(idx,str.length()), + and_exprt + (not_exprt(equal_exprt(str[idx],space_char)), + not_exprt(equal_exprt(str[minus_exprt(plus_exprt(idx,length()),refined_string_typet::index_of_int(1))],space_char)))); + axioms.push_back(m_index_condition); +} + +void string_exprt::of_string_to_lower_case +(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() == 1); + + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + bool is_c_string = refined_string_typet::is_c_string_type(expr.type()); + exprt char_a; + exprt char_A; + exprt char_z; + exprt char_Z; + if(is_c_string) { + char_a = constant_of_nat(97,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + char_A = constant_of_nat(65,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + char_z = constant_of_nat(122,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + char_Z = constant_of_nat(90,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + } else { + char_a = constant_of_nat(97,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + char_A = constant_of_nat(65,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + char_z = constant_of_nat(122,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + char_Z = constant_of_nat(90,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + } + + axioms.emplace_back(equal_exprt(length(), str.length())); + + symbol_exprt idx = fresh_symbol("QA_lower_case",refined_string_typet::index_type()); + // forall idx < str.length, this[idx] = 'A'<=str[idx]<='Z' ? str[idx]+'a'-'A' : str[idx] + exprt is_upper_case = and_exprt(binary_relation_exprt(char_A,ID_le,str[idx]), + binary_relation_exprt(str[idx],ID_le,char_Z)); + equal_exprt convert((*this)[idx],plus_exprt(str[idx],minus_exprt(char_a,char_A))); + equal_exprt eq((*this)[idx], str[idx]); + string_constraintt a(and_exprt(implies_exprt(is_upper_case,convert),implies_exprt(not_exprt(is_upper_case),eq))); + axioms.push_back(a.forall(idx,index_zero,length())); +} + + +void string_exprt::of_string_to_upper_case +(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() == 1); + + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + bool is_c_string = refined_string_typet::is_c_string_type(expr.type()); + exprt char_a; + exprt char_A; + exprt char_z; + exprt char_Z; + + if(is_c_string) { + char_a = constant_of_nat(97,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + char_A = constant_of_nat(65,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + char_z = constant_of_nat(122,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + char_Z = constant_of_nat(90,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + } else { + char_a = constant_of_nat(97,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + char_A = constant_of_nat(65,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + char_z = constant_of_nat(122,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + char_Z = constant_of_nat(90,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + } + + axioms.emplace_back(equal_exprt(length(), str.length())); + + symbol_exprt idx = fresh_symbol("QA_upper_case",refined_string_typet::index_type()); + // forall idx < str.length, this[idx] = 'a'<=str[idx]<='z' ? str[idx]+'A'-'a' : str[idx] + exprt is_lower_case = and_exprt(binary_relation_exprt(char_a,ID_le,str[idx]), + binary_relation_exprt(str[idx],ID_le,char_z)); + equal_exprt convert((*this)[idx],plus_exprt(str[idx],minus_exprt(char_A,char_a))); + equal_exprt eq((*this)[idx], str[idx]); + string_constraintt a(and_exprt(implies_exprt(is_lower_case,convert),implies_exprt(not_exprt(is_lower_case),eq))); + axioms.push_back(a.forall(idx,index_zero,length())); +} + + +void string_exprt::of_int +(const function_application_exprt &expr,axiom_vect & axioms) +{ + assert(expr.arguments().size() == 1); + of_int(expr.arguments()[0],axioms,refined_string_typet::is_c_string_type(expr.type()),10); +} + +void string_exprt::of_long +(const function_application_exprt &expr,axiom_vect & axioms) +{ + assert(expr.arguments().size() == 1); + of_int(expr.arguments()[0],axioms,refined_string_typet::is_c_string_type(expr.type()),30); +} + + +void string_exprt::of_float +(const function_application_exprt &f,axiom_vect & axioms) +{ + assert(f.arguments().size() == 1); + of_float(f.arguments()[0],axioms,refined_string_typet::is_c_string_type(f.type()),false); +} + +void string_exprt::of_float +(const exprt &f, axiom_vect & axioms, bool is_c_string, bool double_precision) +{ + // Warning: we currently only have partial specification + unsignedbv_typet char_type; + int char_width; + if(is_c_string) { + char_type = refined_string_typet::char_type(); + char_width = STRING_SOLVER_CHAR_WIDTH; + } else { + char_type = refined_string_typet::java_char_type(); + char_width = JAVA_STRING_SOLVER_CHAR_WIDTH; + } + + axioms.emplace_back(binary_relation_exprt(length(), ID_le, refined_string_typet::index_of_int(24))); + + + string_exprt magnitude(char_type); + string_exprt sign_string(char_type); + + // If the argument is NaN, the result is the string "NaN". + string_exprt nan_string(char_type); + nan_string.of_string_constant("NaN",char_width,char_type,axioms); + + ieee_float_spect fspec = double_precision?ieee_float_spect::double_precision():ieee_float_spect::single_precision(); + + exprt isnan = float_bvt().isnan(f,fspec); + axioms.emplace_back(isnan, equal_exprt(magnitude.length(),nan_string.length())); + symbol_exprt qvar = string_exprt::fresh_symbol("qvar_equal_nan", refined_string_typet::index_type()); + axioms.push_back + (string_constraintt(isnan,equal_exprt(magnitude[qvar],nan_string[qvar]) + ).forall(qvar,index_zero,nan_string.length())); + + // If the argument is not NaN, the result is a string that represents the sign and magnitude (absolute value) of the argument. If the sign is negative, the first character of the result is '-' ('\u002D'); if the sign is positive, no sign character appears in the result. + + const bitvector_typet &bv_type=to_bitvector_type(f.type()); + unsigned width=bv_type.get_width(); + exprt isneg = extractbit_exprt(f, width-1); + + axioms.emplace_back(isneg, equal_exprt(sign_string.length(),refined_string_typet::index_of_int(1))); + + axioms.emplace_back(not_exprt(isneg), equal_exprt(sign_string.length(),refined_string_typet::index_of_int(0))); + axioms.emplace_back(isneg,equal_exprt(sign_string[refined_string_typet::index_of_int(0)], constant_of_nat(0x2D,char_width,char_type))); + + + // If m is infinity, it is represented by the characters "Infinity"; thus, positive infinity produces the result "Infinity" and negative infinity produces the result "-Infinity". + + string_exprt infinity_string(char_type); + infinity_string.of_string_constant("Infinity",char_width,char_type,axioms); + exprt isinf = float_bvt().isinf(f,fspec); + axioms.emplace_back(isinf, equal_exprt(magnitude.length(),infinity_string.length())); + symbol_exprt qvar_inf = string_exprt::fresh_symbol("qvar_equal_infinity", refined_string_typet::index_type()); + axioms.push_back + (string_constraintt(isinf,equal_exprt(magnitude[qvar_inf],infinity_string[qvar_inf]) + ).forall(qvar_inf,index_zero,infinity_string.length())); + + //If m is zero, it is represented by the characters "0.0"; thus, negative zero produces the result "-0.0" and positive zero produces the result "0.0". + + string_exprt zero_string(char_type); + zero_string.of_string_constant("0.0",char_width,char_type,axioms); + exprt iszero = float_bvt().is_zero(f,fspec); + axioms.emplace_back(iszero, equal_exprt(magnitude.length(),zero_string.length())); + symbol_exprt qvar_zero = string_exprt::fresh_symbol("qvar_equal_zero", refined_string_typet::index_type()); + axioms.push_back + (string_constraintt(iszero,equal_exprt(magnitude[qvar_zero],zero_string[qvar_zero]) + ).forall(qvar_zero,index_zero,zero_string.length())); + + + /* + ieee_floatt milli(fspec); + milli.from_float(0.001); + ieee_floatt decamega(fspec); + decamega.from_float(1e7); + exprt scientific = or_exprt + (float_bvt().relation(f,float_bvt().LT,milli.to_expr(),fspec), + float_bvt().relation(f,float_bvt().GE,decamega.to_expr(),fspec)); + */ + + // If m is greater than or equal to 10^-3 but less than 10^7, then it is represented as the integer part of m, in decimal form with no leading zeroes, followed by '.' ('\u002E'), followed by one or more decimal digits representing the fractional part of m. + + //string_exprt integer_part(char_type); + //exprt integer = float_bvt().to_integer(float_bvt.abs(f,fspec),32,true,fspec); + + //integer_part.of_int(integer); + //string_exprt dot_string(char_type); + //dot_string.of_string_constant(".",char_width,char_type,axioms); + + //string_exprt fractional_part(char_type); + + /* Here is the remainder of the specification of Float.toString, for the magnitude m : + + If m is less than 10^-3 or greater than or equal to 10^7, then it is represented in so-called "computerized scientific notation." Let n be the unique integer such that 10n ≤ m < 10n+1; then let a be the mathematically exact quotient of m and 10n so that 1 ≤ a < 10. The magnitude is then represented as the integer part of a, as a single decimal digit, followed by '.' ('\u002E'), followed by decimal digits representing the fractional part of a, followed by the letter 'E' ('\u0045'), followed by a representation of n as a decimal integer, as produced by the method Integer.toString(int). + + How many digits must be printed for the fractional part of m or a? There must be at least one digit to represent the fractional part, and beyond that as many, but only as many, more digits as are needed to uniquely distinguish the argument value from adjacent values of type float. That is, suppose that x is the exact mathematical value represented by the decimal representation produced by this method for a finite nonzero argument f. Then f must be the float value nearest to x; or, if two float values are equally close to x, then f must be one of them and the least significant bit of the significand of f must be 0. */ + + of_string_concat(sign_string,magnitude,axioms); + + + /* + exprt char_0 = constant_of_nat(48,char_width,char_type); + exprt char_9 = constant_of_nat(57,char_width,char_type); + exprt char_dot = constant_of_nat(46,char_width,char_type); + + symbol_exprt idx = fresh_symbol("QA_float",refined_string_typet::index_type()); + exprt c = (*this)[idx]; + exprt is_digit = + or_exprt(and_exprt(binary_relation_exprt(char_0,ID_le,c), + binary_relation_exprt(c,ID_le,char_9)), + equal_exprt(c,char_dot) + ); + string_constraintt a(is_digit);*/ + //axioms.push_back(a.forall(idx,index_zero,length())); + + +} + +void string_exprt::of_double +(const function_application_exprt &f,axiom_vect & axioms) +{ + assert(f.arguments().size() == 1); + of_float(f.arguments()[0],axioms,refined_string_typet::is_c_string_type(f.type()),true); +} + + +void string_exprt::of_bool +(const function_application_exprt &f,axiom_vect & axioms) +{ + assert(f.arguments().size() == 1); + of_bool(f.arguments()[0],axioms,refined_string_typet::is_c_string_type(f.type())); + +} + +void string_exprt::of_bool +(const exprt &i,axiom_vect & axioms,bool is_c_string) +{ + unsignedbv_typet char_type; + int char_width; + if(is_c_string) { + char_type = refined_string_typet::char_type(); + char_width = STRING_SOLVER_CHAR_WIDTH; + } else { + char_type = refined_string_typet::java_char_type(); + char_width = JAVA_STRING_SOLVER_CHAR_WIDTH; + } + + assert(i.type() == bool_typet() || i.type().id() == ID_c_bool); + + typecast_exprt eq(i,bool_typet()); + + string_exprt true_string(char_type); + string_exprt false_string(char_type); + true_string.of_string_constant("true",char_width,char_type,axioms); + false_string.of_string_constant("false",char_width,char_type,axioms); + + axioms.emplace_back(eq, equal_exprt(length(),true_string.length())); + symbol_exprt qvar = string_exprt::fresh_symbol("qvar_equal_true", refined_string_typet::index_type()); + axioms.push_back + (string_constraintt(eq,equal_exprt((*this)[qvar],true_string[qvar]) + ).forall(qvar,index_zero,true_string.length())); + + axioms.emplace_back(not_exprt(eq), equal_exprt(length(),false_string.length())); + symbol_exprt qvar1 = string_exprt::fresh_symbol("qvar_equal_false", refined_string_typet::index_type()); + axioms.push_back + (string_constraintt(not_exprt(eq),equal_exprt((*this)[qvar1],false_string[qvar1]) + ).forall(qvar,index_zero,false_string.length())); + + + +} + + +void string_exprt::of_int +(const exprt &i,axiom_vect & axioms,bool is_c_string, int max_size) +{ + typet type = i.type(); + int width = type.get_unsigned_int(ID_width); + exprt ten = constant_of_nat(10,width,type); + exprt zero_char; + exprt nine_char; + exprt minus_char; + + if(is_c_string) { + minus_char = constant_of_nat(45,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + zero_char = constant_of_nat(48,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + nine_char = constant_of_nat(57,STRING_SOLVER_CHAR_WIDTH,refined_string_typet::char_type()); + } else { + minus_char = constant_of_nat(45,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + zero_char = constant_of_nat(48,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + nine_char = constant_of_nat(57,JAVA_STRING_SOLVER_CHAR_WIDTH,refined_string_typet::java_char_type()); + } + + axioms.emplace_back(and_exprt(*this > index_zero,*this <= refined_string_typet::index_of_int(max_size))); + + exprt chr = (*this)[refined_string_typet::index_of_int(0)]; + exprt starts_with_minus = equal_exprt(chr,minus_char); + exprt starts_with_digit = and_exprt + (binary_relation_exprt(chr,ID_ge,zero_char), + binary_relation_exprt(chr,ID_le,nine_char)); + axioms.emplace_back(or_exprt(starts_with_digit,starts_with_minus)); + + for(int size=1; size<=max_size;size++) { + exprt sum = constant_of_nat(0,width,type); + exprt all_numbers = true_exprt(); + chr = (*this)[refined_string_typet::index_of_int(0)]; + exprt first_value = typecast_exprt(minus_exprt(chr,zero_char),type); + + for(int j=1; j1) { + axioms.emplace_back(and_exprt(premise,starts_with_digit), + not_exprt(equal_exprt((*this)[index_zero],zero_char))); + axioms.emplace_back(and_exprt(premise,starts_with_minus), + not_exprt(equal_exprt((*this)[refined_string_typet::index_of_int(1)],zero_char))); + } + + //we have to be careful when exceeding the maximal size of integers + // Warning this should be different depending on max size + if(size == max_size) { + exprt smallest_with_10_digits = constant_of_nat(1000000000,width,type); + axioms.emplace_back(premise,binary_relation_exprt(i,ID_ge,smallest_with_10_digits)); + } + } +} + + +exprt int_of_hex_char(exprt chr, unsigned char_width, typet char_type) { + exprt zero_char = constant_of_nat(48,char_width,char_type); + exprt nine_char = constant_of_nat(57,char_width,char_type); + exprt a_char = constant_of_nat(0x61,char_width,char_type); + return if_exprt(binary_relation_exprt(chr,ID_gt,nine_char), + minus_exprt(chr,constant_of_nat(0x61 - 10,char_width,char_type)), + minus_exprt(chr,zero_char)); +} + + +void string_exprt::of_int_hex +(const exprt &i,axiom_vect & axioms,bool is_c_string) +{ + typet type = i.type(); + int width = type.get_unsigned_int(ID_width); + exprt sixteen = constant_of_nat(16,width,type); + typet char_type; + unsigned char_width; + + if(is_c_string) { + char_type = refined_string_typet::char_type(); + char_width = STRING_SOLVER_CHAR_WIDTH; + } else { + char_type = refined_string_typet::java_char_type(); + char_width = JAVA_STRING_SOLVER_CHAR_WIDTH; + } + + exprt minus_char = constant_of_nat(45,char_width,char_type); + exprt zero_char = constant_of_nat(48,char_width,char_type); + exprt nine_char = constant_of_nat(57,char_width,char_type); + exprt a_char = constant_of_nat(0x61,char_width,char_type); + exprt f_char = constant_of_nat(0x66,char_width,char_type); + + int max_size = 8; + axioms.emplace_back(and_exprt(*this > index_zero,*this <= refined_string_typet::index_of_int(max_size))); + + for(int size=1; size<=max_size;size++) { + exprt sum = constant_of_nat(0,width,type); + exprt all_numbers = true_exprt(); + exprt chr = (*this)[refined_string_typet::index_of_int(0)]; + + for(int j=0; j1) { + axioms.emplace_back(premise, + not_exprt(equal_exprt((*this)[index_zero],zero_char))); + } + + } +} + +void string_exprt::of_int_hex +(const function_application_exprt &f,axiom_vect & axioms) +{ + assert(f.arguments().size() == 1); + of_int_hex(f.arguments()[0],axioms,refined_string_typet::is_c_string_type(f.type())); +} + +void string_exprt::of_char +(const function_application_exprt &f,axiom_vect & axioms) +{ + assert(f.arguments().size() == 1); + of_char(f.arguments()[0],axioms,refined_string_typet::is_c_string_type(f.type())); + +} + +void string_exprt::of_char +(const exprt &c, axiom_vect & axioms, bool is_c_string) +{ + and_exprt lemma(equal_exprt((*this)[refined_string_typet::index_of_int(0)], c), + equal_exprt(length(), refined_string_typet::index_of_int(1))); + axioms.push_back(lemma); + +} + + +void string_exprt::of_code_point(const exprt &code_point, axiom_vect & axioms, bool is_c_string) +{ + typet type = code_point.type(); + binary_relation_exprt small(code_point,ID_lt,constant_of_nat(0x010000,32, type)); + axioms.emplace_back(small, + equal_exprt(length(), refined_string_typet::index_of_int(1))); + axioms.emplace_back(not_exprt(small), + equal_exprt(length(), refined_string_typet::index_of_int(2))); + axioms.emplace_back(small,equal_exprt((*this)[refined_string_typet::index_of_int(0)],typecast_exprt(code_point,refined_string_typet::java_char_type()))); + + axioms.emplace_back(not_exprt(small), + equal_exprt + ((*this)[refined_string_typet::index_of_int(0)], + typecast_exprt + (plus_exprt(constant_of_nat(0xD800,32, type), + div_exprt(minus_exprt(code_point,constant_of_nat(0x010000,32,type)),constant_of_nat(0x0400,32, type))), + refined_string_typet::java_char_type()))); + axioms.emplace_back(not_exprt(small), + equal_exprt + ((*this)[refined_string_typet::index_of_int(1)], + typecast_exprt + (plus_exprt(constant_of_nat(0xDC00,32, type), + mod_exprt(code_point,constant_of_nat(0x0400,32, type))), + refined_string_typet::java_char_type()))); + +} + + +void string_exprt::of_string_char_set +(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() == 3); //bad args to string_char_set? + + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + symbol_exprt c = fresh_symbol("char", refined_string_typet::get_char_type(args[0])); + + axioms.emplace_back(equal_exprt(c,args[2])); + with_exprt sarrnew(str.content(), args[1], c); + implies_exprt lemma(binary_relation_exprt(args[1], ID_lt, str.length()), + and_exprt(equal_exprt(content(), sarrnew), + equal_exprt(length(), str.length()))); + axioms.push_back(lemma); + +} + +void string_exprt::of_string_replace +(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + exprt oldChar = args[1]; + exprt newChar = args[2]; + + axioms.emplace_back(equal_exprt(length(), str.length())); + symbol_exprt qvar = string_exprt::fresh_symbol("QA_replace", refined_string_typet::index_type()); + + axioms.push_back + (string_constraintt + (and_exprt + (implies_exprt(equal_exprt(str[qvar],oldChar),equal_exprt((*this)[qvar],newChar)), + implies_exprt(not_exprt(equal_exprt(str[qvar],oldChar)), + equal_exprt((*this)[qvar],str[qvar])) + ) + ).forall(qvar,index_zero,length())); + +} + +void string_exprt::of_string_delete_char_at +(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() == 2); + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + exprt index_one = refined_string_typet::index_of_int(1); + of_string_delete(str,args[1],plus_exprt(args[1],index_one),symbol_to_string,axioms); +} + +void string_exprt::of_string_delete +(const string_exprt &str, const exprt & start, const exprt & end, std::map & symbol_to_string, axiom_vect & axioms) +{ + // We should have these formulas: + // (index < |str| ==> |s| = |str| - 1) && (index >= |str| ==> |s| = |str|) + // forall i < |s| (i < index ==> s[i] = str[i] + // && i >= index ==> s[i] = str[i+1]) + // However this may make the index set computation loop because the same + // index appears switched by one. + // It may be better to call two substrings functions + + assert(start.type() == refined_string_typet::index_type()); + assert(end.type() == refined_string_typet::index_type()); + string_exprt str1(refined_string_typet::get_char_type(str)); + string_exprt str2(refined_string_typet::get_char_type(str)); + str1.of_string_substring(str,index_zero,start,symbol_to_string,axioms); + str2.of_string_substring(str,end,str.length(),symbol_to_string,axioms); + of_string_concat(str1,str2,axioms); + +} + +void string_exprt::of_string_delete +(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() == 3); + string_exprt str = of_expr(args[0],symbol_to_string,axioms); + of_string_delete(str,args[1],args[2],symbol_to_string,axioms); +} + + +void string_exprt::of_string_concat_int(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_int(args[1],axioms,refined_string_typet::is_c_string_type(args[0].type()),10); + of_string_concat(s1,s2,axioms); +} + +void string_exprt::of_string_concat_long(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + + s2.of_int(args[1],axioms,refined_string_typet::is_c_string_type(args[0].type()),30); + of_string_concat(s1,s2,axioms); +} + +void string_exprt::of_string_concat_bool(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_bool(args[1],axioms,refined_string_typet::is_c_string_type(f.type())); + of_string_concat(s1,s2,axioms); +} + +void string_exprt::of_string_concat_char(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_char(args[1],axioms,refined_string_typet::is_c_string_type(f.type())); + of_string_concat(s1,s2,axioms); +} + +void string_exprt::of_string_concat_double(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_float(args[1],axioms,refined_string_typet::is_c_string_type(f.type()),30); + of_string_concat(s1,s2,axioms); +} + +void string_exprt::of_string_concat_float(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_float(args[1],axioms,refined_string_typet::is_c_string_type(f.type()),10); + of_string_concat(s1,s2,axioms); +} + +void string_exprt::of_string_concat_code_point(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_code_point(args[1],axioms,refined_string_typet::is_c_string_type(f.type())); + of_string_concat(s1,s2,axioms); +} + +void string_exprt::of_string_insert(const string_exprt & s1, const string_exprt & s2, + const exprt & offset, + std::map & symbol_to_string, + axiom_vect & axioms) +{ + assert(offset.type() == refined_string_typet::index_type()); + unsignedbv_typet char_type = refined_string_typet::get_char_type(s1); + string_exprt pref(char_type); + string_exprt suf(char_type); + string_exprt concat1(char_type); + pref.of_string_substring(s1,index_zero,offset,symbol_to_string,axioms); + suf.of_string_substring(s1,offset,s1.length(),symbol_to_string,axioms); + concat1.of_string_concat(pref,s2,axioms); + of_string_concat(concat1,suf,axioms); +} + + +void string_exprt::of_string_insert(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2 = string_exprt::of_expr(args[2],symbol_to_string,axioms); + of_string_insert(s1, s2, args[1],symbol_to_string, axioms); +} + +void string_exprt::of_string_insert_int(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[2])); + s2.of_int(args[2],axioms,refined_string_typet::is_c_string_type(args[0].type()),10); + of_string_insert(s1,s2,args[1],symbol_to_string,axioms); +} + +void string_exprt::of_string_insert_long(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[2])); + s2.of_int(args[2],axioms,refined_string_typet::is_c_string_type(args[0].type()),30); + of_string_insert(s1,s2,args[1],symbol_to_string,axioms); +} + +void string_exprt::of_string_insert_bool(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_bool(args[2],axioms,refined_string_typet::is_c_string_type(args[0].type())); + of_string_insert(s1,s2,args[1],symbol_to_string,axioms); +} + +void string_exprt::of_string_insert_char(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_char(args[2],axioms,refined_string_typet::is_c_string_type(args[0].type())); + of_string_insert(s1,s2,args[1],symbol_to_string,axioms); +} + +void string_exprt::of_string_insert_double(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_float(args[2],axioms,refined_string_typet::is_c_string_type(args[0].type()),30); + of_string_insert(s1,s2,args[1],symbol_to_string,axioms); +} + +void string_exprt::of_string_insert_float(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 3); + string_exprt s1 = string_exprt::of_expr(args[0],symbol_to_string,axioms); + string_exprt s2(refined_string_typet::get_char_type(args[0])); + s2.of_float(args[2],axioms,refined_string_typet::is_c_string_type(args[0].type()),10); + of_string_insert(s1,s2,args[1],symbol_to_string,axioms); +} + + +#include + +void string_exprt::of_string_format(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms){ + const function_application_exprt::argumentst &args = f.arguments(); + // warning this is right now only for java: + bool is_c_string = false; + unsignedbv_typet char_type = is_c_string?refined_string_typet::char_type():refined_string_typet::java_char_type(); + size_t char_width = is_c_string?STRING_SOLVER_CHAR_WIDTH:JAVA_STRING_SOLVER_CHAR_WIDTH; + + if(args.size() == 2) + { + + // Warning: this is not very clean: + irep_idt literal = extract_java_string(to_symbol_expr(args[0].op1().op0().op0())); + std::string format_string = id2string(literal); + std::cout << "string_exprt::of_string_format " << format_string << std::endl; + size_t position = format_string.find_first_of('%'); + std::vector strings; + int arg_counter = 0; + + string_exprt begin(char_type); + begin.of_string_constant(format_string.substr(0,position),char_width,char_type,axioms); + strings.push_back(begin); + //std::cout << "string_exprt::of_string_format : " << f.pretty() << std::endl; + //typecast_exprt arg_tab(member_exprt(args[1].op0(),"data"),array_typet(java_type_from_string("Ljava/lang/Object;"),infinity_exprt(refined_string_typet::index_type()))); + member_exprt arg_tab(args[1].op0(),"data",array_typet(java_type_from_string("Ljava/lang/Object;"),infinity_exprt(refined_string_typet::index_type()))); + std::cout << "string_exprt::arg_tab : " << arg_tab.type().pretty() << std::endl; + + while(position != std::string::npos) + { + switch(format_string[position+1]) { + case 'd' : + { + string_exprt str(char_type); + index_exprt arg_object(arg_tab,refined_string_typet::index_of_int(arg_counter++)); + typecast_exprt arg_int(arg_object, signedbv_typet(32)); + symbol_exprt var_arg_int = string_exprt::fresh_symbol("format_arg_int", signedbv_typet(32)); + axioms.push_back(equal_exprt(arg_int,var_arg_int)); + axioms.push_back(equal_exprt(var_arg_int,refined_string_typet::index_of_int(12))); + str.of_int(var_arg_int,axioms,is_c_string,10); + + strings.push_back(str); + std::cout << "string format: position " << position << " int arg: " << arg_int.pretty() << std::endl; + break; + } + + default: + { + std::cout << "warning: unknown string format: " << format_string << std::endl; + break; + } + } + size_t new_position = format_string.find_first_of('%',position+2); + if(new_position != std::string::npos) { + string_exprt str(char_type); + str.of_string_constant(format_string.substr(position+2,new_position),char_width,char_type,axioms); + strings.push_back(str); + } + position = new_position; + } + + + string_exprt * concatenation = &strings[0]; + int i; + for(i = 1; i < strings.size() - 1; i++) + { + string_exprt str(refined_string_typet::java_char_type()); + str.of_string_concat(*concatenation,strings[i],axioms); + concatenation = &str; + } + + of_string_concat(*concatenation,strings[i],axioms); + } + +} diff --git a/src/solvers/refinement/string_expr.h b/src/solvers/refinement/string_expr.h new file mode 100644 index 00000000000..052469b4d34 --- /dev/null +++ b/src/solvers/refinement/string_expr.h @@ -0,0 +1,153 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String expressions for PASS algorithm + (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_SOLVER_STRING_EXPR_H +#define CPROVER_SOLVER_STRING_EXPR_H + +#include + +#include +#include +#include +#include + + +typedef std::vector axiom_vect; + +// Expressions that encode strings +class string_exprt : public struct_exprt { +public: + + // Initialize string from the type of characters + string_exprt(unsignedbv_typet char_type); + + // Default uses C character type + string_exprt() : string_exprt(refined_string_typet::char_type()) {}; + + // Add to the list of axioms, lemmas which should hold for the string to be + // equal to the given expression. + static string_exprt of_expr(const exprt & unrefined_string, std::map & symbol_to_string, axiom_vect & axioms); + + // We maintain a map from symbols to strings. If a symbol is not yet present we will create a new one with the correct type depending on whether this is a java or c string + static string_exprt get_string_of_symbol(std::map & symbol_to_string, const symbol_exprt & sym); + + // Generate a new symbol of the given type tp with a prefix + static symbol_exprt fresh_symbol(const irep_idt &prefix, + const typet &tp=bool_typet()); + + // Expression corresponding to the length of the string + inline const exprt & length() const { return op0();}; + + // Expression corresponding to the content (array of characters) of the string + inline const exprt & content() const { return op1();}; + + static exprt within_bounds(const exprt & idx, const exprt & bound); + + // Expression of the character at position idx in the string + inline index_exprt operator[] (const exprt & idx) const + { return index_exprt(content(), idx);} + + // Comparison on the length of the strings + inline binary_relation_exprt operator> (const string_exprt & rhs) const + { return binary_relation_exprt(rhs.length(), ID_lt, length()); } + inline binary_relation_exprt operator<= (const string_exprt & rhs) const + { return binary_relation_exprt(length(), ID_le, rhs.length()); } + inline binary_relation_exprt operator>= (const string_exprt & rhs) const + { return binary_relation_exprt(length(), ID_ge, rhs.length()); } + inline binary_relation_exprt operator> (const exprt & rhs) const + { return binary_relation_exprt(rhs, ID_lt, length()); } + inline binary_relation_exprt operator>= (const exprt & rhs) const + { return binary_relation_exprt(length(), ID_ge, rhs); } + inline binary_relation_exprt operator<= (const exprt & rhs) const + { return binary_relation_exprt(length(), ID_le, rhs); } + //this one is used by maps: inline binary_relation_exprt operator< (const string_exprt & rhs) const { return binary_relation_exprt(length(), ID_lt, rhs.length()); } + // inline binary_relation_exprt operator< (const exprt & rhs) const { return binary_relation_exprt(length(), ID_lt, rhs); } + + static irep_idt extract_java_string(const symbol_exprt & s); + + void of_string_constant(irep_idt sval, int char_width, unsignedbv_typet char_type, axiom_vect &axioms); + +private: + // Auxiliary functions for of_expr + void of_function_application(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms); + void of_string_literal(const function_application_exprt &f,axiom_vect &axioms); + void of_string_concat(const string_exprt & s1, const string_exprt & s2, axiom_vect & axioms); + void of_string_concat(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_concat_int(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_concat_long(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_concat_bool(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_concat_char(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_concat_double(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_concat_float(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_concat_code_point(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + + // insert s2 in s1 at the given position + void of_string_insert(const string_exprt & s1, const string_exprt & s2, const exprt &offset, std::map & symbol_to_string, axiom_vect & axioms); + void of_string_insert(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_insert_int(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_insert_long(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_insert_bool(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_insert_char(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_insert_double(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_insert_float(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect &axioms); + + void of_string_substring(const string_exprt & str, const exprt & start, const exprt & end, std::map & symbol_to_string, axiom_vect & axioms); + void of_string_substring(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_trim(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_to_lower_case(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_to_upper_case(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_char_set(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_delete (const string_exprt &str, const exprt & start, const exprt & end, std::map & symbol_to_string, axiom_vect & axioms); + void of_string_delete(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_delete_char_at(const function_application_exprt &expr, std::map & symbol_to_string, axiom_vect &axioms); + void of_string_replace(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms); + + // Warning: not working correctly at the moment + void of_string_value_of(const function_application_exprt &f, axiom_vect &axioms); + void of_string_set_length(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms); + void of_string_copy(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms); + void of_string_format(const function_application_exprt &f, std::map & symbol_to_string, axiom_vect & axioms); + + void of_empty_string(const function_application_exprt &f, axiom_vect & axioms); + + void of_int(const function_application_exprt &f, axiom_vect & axioms); + void of_int(const exprt &i, axiom_vect & axioms, bool is_c_string, int max_size); + void of_int_hex(const exprt &i, axiom_vect & axioms, bool is_c_string); + void of_int_hex(const function_application_exprt &f,axiom_vect & axioms); + void of_long(const function_application_exprt &f, axiom_vect & axioms); + void of_long(const exprt &i, axiom_vect & axioms, bool is_c_string, int max_size); + void of_bool(const function_application_exprt &f, axiom_vect & axioms); + void of_bool(const exprt &i, axiom_vect & axioms, bool is_c_string); + void of_char(const function_application_exprt &f, axiom_vect & axioms); + void of_char(const exprt &i, axiom_vect & axioms, bool is_c_string); + + // Warning: the specifications of these functions is only partial: + void of_float(const function_application_exprt &f, axiom_vect & axioms); + void of_float(const exprt &f, axiom_vect & axioms, bool is_c_string, bool double_precision=false); + void of_double(const function_application_exprt &f, axiom_vect & axioms); + + void of_code_point(const exprt &code_point, axiom_vect & axioms, bool is_c_string); + void of_java_char_array(const exprt & char_array, axiom_vect & axioms); + + void of_if(const if_exprt &expr, std::map & symbol_to_string, axiom_vect & axioms); + + static unsigned next_symbol_id; + + friend inline string_exprt &to_string_expr(exprt &expr); + +}; + + +extern inline string_exprt &to_string_expr(exprt &expr){ + assert(expr.id()==ID_struct); + return static_cast(expr); +} + + +#endif diff --git a/src/solvers/refinement/string_functions.cpp b/src/solvers/refinement/string_functions.cpp new file mode 100644 index 00000000000..f3383f436f0 --- /dev/null +++ b/src/solvers/refinement/string_functions.cpp @@ -0,0 +1,19 @@ +/*******************************************************************\ + +Module: Defines identifiers for string functions + +Author: Romain Brenguier + +Date: September 2016 + +\*******************************************************************/ + +#include + +bool starts_with(irep_idt id, irep_idt prefix) { + std::string s = id2string(id); + std::string t = id2string(prefix); + for(int i = 0; i < t.length(); i++) + if(s[i] != t[i]) return false; + return true; +} diff --git a/src/solvers/refinement/string_functions.h b/src/solvers/refinement/string_functions.h new file mode 100644 index 00000000000..f07294ac0a4 --- /dev/null +++ b/src/solvers/refinement/string_functions.h @@ -0,0 +1,76 @@ +/*******************************************************************\ + +Module: Defines identifiers for string functions + +Author: Romain Brenguier + +Date: September 2016 + +\*******************************************************************/ + +#ifndef CPROVER_STRING_FUNCTIONS_H +#define CPROVER_STRING_FUNCTIONS_H + +#include + +bool starts_with(irep_idt id, irep_idt prefix); +const irep_idt cprover_char_literal_func("__CPROVER_uninterpreted_char_literal_func"); +const irep_idt cprover_string_literal_func("__CPROVER_uninterpreted_string_literal_func"); +const irep_idt cprover_string_char_at_func("__CPROVER_uninterpreted_string_char_at_func"); +const irep_idt cprover_string_char_set_func("__CPROVER_uninterpreted_string_char_set_func"); +const irep_idt cprover_string_code_point_at_func("__CPROVER_uninterpreted_string_code_point_at_func"); +const irep_idt cprover_string_code_point_before_func("__CPROVER_uninterpreted_string_code_point_before_func"); +const irep_idt cprover_string_code_point_count_func("__CPROVER_uninterpreted_string_code_point_count_func"); +const irep_idt cprover_string_offset_by_code_point_func("__CPROVER_uninterpreted_string_offset_by_code_point_func"); +const irep_idt cprover_string_compare_to_func("__CPROVER_uninterpreted_string_compare_to_func"); +const irep_idt cprover_string_concat_func("__CPROVER_uninterpreted_string_concat_func"); +const irep_idt cprover_string_concat_int_func("__CPROVER_uninterpreted_string_concat_int_func"); +const irep_idt cprover_string_concat_long_func("__CPROVER_uninterpreted_string_concat_long_func"); +const irep_idt cprover_string_concat_char_func("__CPROVER_uninterpreted_string_concat_char_func"); +const irep_idt cprover_string_concat_bool_func("__CPROVER_uninterpreted_string_concat_bool_func"); +const irep_idt cprover_string_concat_double_func("__CPROVER_uninterpreted_string_concat_double_func"); +const irep_idt cprover_string_concat_float_func("__CPROVER_uninterpreted_string_concat_float_func"); +const irep_idt cprover_string_concat_code_point_func("__CPROVER_uninterpreted_string_concat_code_point_func"); +const irep_idt cprover_string_contains_func("__CPROVER_uninterpreted_string_contains_func"); +const irep_idt cprover_string_copy_func("__CPROVER_uninterpreted_string_copy_func"); +const irep_idt cprover_string_delete_func("__CPROVER_uninterpreted_string_delete_func"); +const irep_idt cprover_string_delete_char_at_func("__CPROVER_uninterpreted_string_delete_char_at_func"); +const irep_idt cprover_string_equal_func("__CPROVER_uninterpreted_string_equal_func"); +const irep_idt cprover_string_equals_ignore_case_func("__CPROVER_uninterpreted_string_equals_ignore_case_func"); +const irep_idt cprover_string_empty_string_func("__CPROVER_uninterpreted_string_empty_string_func"); +const irep_idt cprover_string_endswith_func("__CPROVER_uninterpreted_string_endswith_func"); +const irep_idt cprover_string_format_func("__CPROVER_uninterpreted_string_format_func"); +const irep_idt cprover_string_hash_code_func("__CPROVER_uninterpreted_string_hash_code_func"); +const irep_idt cprover_string_index_of_func("__CPROVER_uninterpreted_string_index_of_func"); +const irep_idt cprover_string_intern_func("__CPROVER_uninterpreted_string_intern_func"); +const irep_idt cprover_string_insert_func("__CPROVER_uninterpreted_string_insert_func"); +const irep_idt cprover_string_insert_int_func("__CPROVER_uninterpreted_string_insert_int_func"); +const irep_idt cprover_string_insert_long_func("__CPROVER_uninterpreted_string_insert_long_func"); +const irep_idt cprover_string_insert_bool_func("__CPROVER_uninterpreted_string_insert_bool_func"); +const irep_idt cprover_string_insert_char_func("__CPROVER_uninterpreted_string_insert_char_func"); +const irep_idt cprover_string_insert_float_func("__CPROVER_uninterpreted_string_insert_float_func"); +const irep_idt cprover_string_insert_double_func("__CPROVER_uninterpreted_string_insert_double_func"); +const irep_idt cprover_string_is_prefix_func("__CPROVER_uninterpreted_string_is_prefix_func"); +const irep_idt cprover_string_is_suffix_func("__CPROVER_uninterpreted_string_is_suffix_func"); +const irep_idt cprover_string_is_empty_func("__CPROVER_uninterpreted_string_is_empty_func"); +const irep_idt cprover_string_last_index_of_func("__CPROVER_uninterpreted_string_last_index_of_func"); +const irep_idt cprover_string_length_func("__CPROVER_uninterpreted_string_length_func"); +const irep_idt cprover_string_of_int_func("__CPROVER_uninterpreted_string_of_int_func"); +const irep_idt cprover_string_of_int_hex_func("__CPROVER_uninterpreted_string_of_int_hex_func"); +const irep_idt cprover_string_of_long_func("__CPROVER_uninterpreted_string_of_long_func"); +const irep_idt cprover_string_of_bool_func("__CPROVER_uninterpreted_string_of_bool_func"); +const irep_idt cprover_string_of_float_func("__CPROVER_uninterpreted_string_of_float_func"); +const irep_idt cprover_string_of_double_func("__CPROVER_uninterpreted_string_of_double_func"); +const irep_idt cprover_string_of_char_func("__CPROVER_uninterpreted_string_of_char_func"); +const irep_idt cprover_string_parse_int_func("__CPROVER_uninterpreted_string_parse_int_func"); +const irep_idt cprover_string_replace_func("__CPROVER_uninterpreted_string_replace_func"); +const irep_idt cprover_string_set_length_func("__CPROVER_uninterpreted_string_set_length_func"); +const irep_idt cprover_string_startswith_func("__CPROVER_uninterpreted_string_startswith_func"); +const irep_idt cprover_string_substring_func("__CPROVER_uninterpreted_string_substring_func"); +const irep_idt cprover_string_to_char_array_func("__CPROVER_uninterpreted_string_to_char_array_func"); +const irep_idt cprover_string_to_lower_case_func("__CPROVER_uninterpreted_string_to_lower_case_func"); +const irep_idt cprover_string_to_upper_case_func("__CPROVER_uninterpreted_string_to_upper_case_func"); +const irep_idt cprover_string_trim_func("__CPROVER_uninterpreted_string_trim_func"); +const irep_idt cprover_string_value_of_func("__CPROVER_uninterpreted_string_value_of_func"); + +#endif diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp new file mode 100644 index 00000000000..57ba1840df4 --- /dev/null +++ b/src/solvers/refinement/string_refinement.cpp @@ -0,0 +1,1760 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String support via axiom instantiation + (see the PASS paper at HVC'13) + +Author: Alberto Griggio, alberto.griggio@gmail.com + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include + + +// This is mostly for debugging: +#include +#include +#include + + +unsignedbv_typet char_type = refined_string_typet::char_type(); +signedbv_typet index_type = refined_string_typet::index_type(); +unsignedbv_typet java_char_type = refined_string_typet::java_char_type(); +constant_exprt zero = refined_string_typet::index_of_int(0); + +// Succinct version of pretty() +std::string string_refinementt::pretty_short(const exprt & expr) { + languagest languages(ns, new_ansi_c_language()); + std::string string_value; + languages.from_expr(expr, string_value); + return string_value; +} + +string_refinementt::string_refinementt(const namespacet &_ns, propt &_prop): + SUB(_ns, _prop) +{ + use_counter_example = false; + //use_counter_example = true; + variable_with_multiple_occurence_in_index = false; + initial_loop_bound = 100; +} + +void string_refinementt::display_index_set() { + for (std::map::iterator i = index_set.begin(), + end = index_set.end(); i != end; ++i) { + const exprt &s = i->first; + debug() << "IS(" << pretty_short(s) << ") == {"; + + for (expr_sett::const_iterator j = i->second.begin(), end = i->second.end(); + j != end; ++j) + debug() << pretty_short (*j) << "; "; + debug() << "}" << eom; + } +} + + +std::chrono::high_resolution_clock::time_point start_time = std::chrono::high_resolution_clock::now(); + + + +literalt string_refinementt::convert_rest(const exprt &expr) +{ + if(expr.id()==ID_function_application) + { + bvt bv = convert_function_application(to_function_application_expr(expr)); + assert(bv.size() == 1); + return bv[0]; + } + else { + //debug() << "string_refinementt::convert_rest("<< pretty_short(expr) << ")" << eom; + return SUB::convert_rest(expr); + } +} + +bvt string_refinementt::convert_pointer_type(const exprt &expr) +{ + if(expr.id()==ID_function_application) + { + bvt bv = convert_function_application(to_function_application_expr(expr)); + return bv; + } + else { + if(expr.id()==ID_typecast) + { + if(expr.operands().size()!=1) + throw "typecast takes one operand"; + + const exprt &op=expr.op0(); + const typet &op_type=ns.follow(op.type()); + + if(op_type.id()==ID_pointer) + return convert_pointer_type(op); + else if(op_type.id()==ID_signedbv || + op_type.id()==ID_unsignedbv) + { + debug() << "string_refinementt::convert_pointer_type("<< pretty_short(expr) << ")" << eom; + debug() << "details:"<< op.pretty() << ")" << eom; + return convert_bv(typecast_exprt(op,unsignedbv_typet(64))); + } + } + else{ + return SUB::convert_pointer_type(expr); + } + } +} + +void string_refinementt::make_string(const symbol_exprt & sym, const exprt & str) +{ + debug() << "string_refinementt::make_string of " << pretty_short(sym) << eom; + //<< " --> " << pretty_short(str) << eom; + if(str.id()==ID_symbol) + assign_to_symbol(sym,string_of_symbol(to_symbol_expr(str))); + else { + // assign_to_symbol(sym,string_exprt::of_expr(str,symbol_to_string,string_axioms)); + if (str.id() == ID_function_application && + starts_with(to_symbol_expr(to_function_application_expr(str).function()).get_identifier(),cprover_string_intern_func)) { + symbol_exprt sym1 = convert_string_intern(to_function_application_expr(str)); + string_exprt s(refined_string_typet::java_char_type()); + assign_to_symbol(sym1,s); + assign_to_symbol(sym,s); + } + else + assign_to_symbol(sym,string_exprt::of_expr(str,symbol_to_string,string_axioms)); + } + //debug() << "string = " << symbol_to_string[sym.get_identifier()].pretty() << eom; +} + +string_exprt string_refinementt::make_string(const exprt & str) +{ + debug() << "string_refinementt::make_string of " << pretty_short(str) << eom; + if(str.id()==ID_symbol) + return string_of_symbol(to_symbol_expr(str)); + else + if (str.id() == ID_function_application && + starts_with(to_symbol_expr(to_function_application_expr(str).function()).get_identifier(),cprover_string_intern_func)) { + symbol_exprt sym1 = convert_string_intern(to_function_application_expr(str)); + string_exprt s(refined_string_typet::java_char_type()); + assign_to_symbol(sym1,s); + return s; + } + else + return string_exprt::of_expr(str,symbol_to_string,string_axioms); +} + + +bool string_refinementt::boolbv_set_equality_to_true(const equal_exprt &expr) +{ + std::chrono::high_resolution_clock::time_point t1 = std::chrono::high_resolution_clock::now(); + + auto duration = std::chrono::duration_cast(t1-start_time).count(); + + if(!equality_propagation) return true; + + const typet &type=ns.follow(expr.lhs().type()); + + if(expr.lhs().id()==ID_symbol && + // We can have affectation of string from StringBuilder or CharSequence + //type==ns.follow(expr.rhs().type()) && + type.id()!=ID_bool) + { + debug() << "string_refinementt(" << (duration / 1000) << "ms)"; + debug() << " " << pretty_short(expr.lhs()) << " <- " + << pretty_short(expr.rhs()) << eom; + + if(refined_string_typet::is_unrefined_string_type(type)) { + symbol_exprt sym = to_symbol_expr(expr.lhs()); + make_string(sym,expr.rhs()); + return false; + } + else if(type == char_type) { + const bvt &bv1=convert_bv(expr.rhs()); + symbol_exprt sym = to_symbol_expr(expr.lhs()); + const irep_idt &identifier = sym.get_identifier(); + map.set_literals(identifier, char_type, bv1); + if(freeze_all) set_frozen(bv1); + return false; + } + else if(type == java_char_type) { + const bvt &bv1=convert_bv(expr.rhs()); + symbol_exprt sym = to_symbol_expr(expr.lhs()); + const irep_idt &identifier = sym.get_identifier(); + map.set_literals(identifier, java_char_type, bv1); + if(freeze_all) set_frozen(bv1); + return false; + } + else if(type==ns.follow(expr.rhs().type())) { + if(is_unbounded_array(type)) + return true; + + const bvt &bv1=convert_bv(expr.rhs()); + + const irep_idt &identifier= + to_symbol_expr(expr.lhs()).get_identifier(); + + map.set_literals(identifier, type, bv1); + + if(freeze_all) set_frozen(bv1); + + return false; + } + } + + return true; +} + +bvt string_refinementt::convert_symbol(const exprt &expr) +{ + const typet &type = expr.type(); + const irep_idt &identifier = expr.get(ID_identifier); + if(identifier.empty()) + //throw "string_refinementt::convert_symbol got empty identifier"; + assert(false); + + //debug() << "convert symbol " << expr << eom; + + if (refined_string_typet::is_unrefined_string_type(type)) { + debug() << "string_refinementt::convert_symbol of unrefined string" << eom; + // this can happen because of boolbvt::convert_equality + string_exprt str = string_of_symbol(to_symbol_expr(expr)); + bvt bv = convert_bv(str); + return bv; + } else if (expr.type() == char_type) { + bvt bv; + bv.resize(STRING_SOLVER_CHAR_WIDTH); + map.get_literals(identifier, char_type, STRING_SOLVER_CHAR_WIDTH, bv); + + forall_literals(it, bv) + if(it->var_no()>=prop.no_variables() && !it->is_constant()) + { + error() << identifier << eom; + assert(false); + } + return bv; + } else if (expr.type() == java_char_type) { + bvt bv; + bv.resize(JAVA_STRING_SOLVER_CHAR_WIDTH); + map.get_literals(identifier, java_char_type, JAVA_STRING_SOLVER_CHAR_WIDTH, bv); + + forall_literals(it, bv) + if(it->var_no()>=prop.no_variables() && !it->is_constant()) + { + error() << identifier << eom; + assert(false); + } + return bv; + } else return SUB::convert_symbol(expr); +} + + +bvt string_refinementt::convert_function_application( + const function_application_exprt &expr) +{ + const exprt &name = expr.function(); + debug() << "string_refinementt::convert_function_application" << eom; + + if (name.id() == ID_symbol) { + const irep_idt &id = to_symbol_expr(name).get_identifier(); + debug() << "string_refinementt::convert_function_application(" + << id << ")" << eom; + + if (starts_with(id,cprover_string_literal_func) + || starts_with(id,cprover_string_concat_func) + || starts_with(id,cprover_string_substring_func) + || starts_with(id,cprover_string_char_set_func)) { + string_exprt str = make_string(expr); + bvt bv = convert_bv(str); + return bv; + } else if (starts_with(id,cprover_char_literal_func)) { + return convert_char_literal(expr); + } else if (starts_with(id,cprover_string_length_func)) { + return convert_string_length(expr); + } else if (starts_with(id,cprover_string_equal_func)) { + return convert_bv(convert_string_equal(expr)); + } else if (starts_with(id,cprover_string_equals_ignore_case_func)) { + return convert_bv(convert_string_equals_ignore_case(expr)); + } else if (starts_with(id,cprover_string_is_empty_func)) { + return convert_bv(convert_string_is_empty(expr)); + } else if (starts_with(id,cprover_string_char_at_func)) { + return convert_string_char_at(expr); + } else if (starts_with(id,cprover_string_is_prefix_func)) { + return convert_bv(convert_string_is_prefix(expr)); + } else if (starts_with(id,cprover_string_is_suffix_func)) { + return convert_string_is_suffix(expr); + } else if (starts_with(id,cprover_string_startswith_func)) { + return convert_bv(convert_string_is_prefix(expr,true)); + } else if (starts_with(id,cprover_string_endswith_func)) { + return convert_string_is_suffix(expr,true); + } else if (starts_with(id,cprover_string_contains_func)) { + return convert_string_contains(expr); + } else if (starts_with(id,cprover_string_hash_code_func)) { + return convert_bv(convert_string_hash_code(expr)); + } else if (starts_with(id,cprover_string_index_of_func)) { + return convert_bv(convert_string_index_of(expr)); + } else if (starts_with(id,cprover_string_last_index_of_func)) { + return convert_bv(convert_string_last_index_of(expr)); + } else if (starts_with(id,cprover_string_parse_int_func)) { + return convert_bv(convert_string_parse_int(expr)); + } else if (starts_with(id,cprover_string_to_char_array_func)) { + return convert_bv(convert_string_to_char_array(expr)); + } else if (starts_with(id,cprover_string_code_point_at_func)) { + return convert_bv(convert_string_code_point_at(expr)); + } else if (starts_with(id,cprover_string_code_point_before_func)) { + return convert_bv(convert_string_code_point_before(expr)); + } else if (starts_with(id,cprover_string_code_point_count_func)) { + return convert_bv(convert_string_code_point_count(expr)); + } else if (starts_with(id,cprover_string_offset_by_code_point_func)) { + return convert_bv(convert_string_offset_by_code_point(expr)); + } else if (starts_with(id,cprover_string_compare_to_func)) { + return convert_bv(convert_string_compare_to(expr)); + } + } + + //return SUB::convert_function_application(expr); + throw "string_refinement::convert_function_application: not a string function"; +} + + +void string_refinementt::print_time(std::string s) { + debug() << s << " TIME == " + << (std::chrono::duration_cast(std::chrono::high_resolution_clock::now()-start_time).count() / 1000) << eom; +} + +// We add instantiations before launching the solver +void string_refinementt::post_process() +{ + + /* + debug() << not_contains_axioms.size() << " not_contains constraints" << eom; + nb_sat_iteration = 0; + debug() << "string_refinementt::post_process at step" << step++ << " time in ms " + << (std::chrono::duration_cast(std::chrono::high_resolution_clock::now()-start_time).count() / 1000) << eom; + + debug() << "string_refinementt::post_process: warning update_index_set has to be checked" << eom; + update_index_set(universal_axioms); + update_index_set(cur); + cur.clear(); + add_instantiations(); + debug() << "string_refinementt::post_process at step" << step++ << " time in ms " + << (std::chrono::duration_cast(std::chrono::high_resolution_clock::now()-start_time).count() / 1000) << eom; + */ + + SUB::post_process(); +} + +decision_proceduret::resultt string_refinementt::dec_solve() +{ + + print_time("string_refinementt::dec_solve"); + for(int i = 0; i < string_axioms.size(); i++) + if(string_axioms[i].is_simple()) + add_lemma(string_axioms[i]); + else if(string_axioms[i].is_string_constant()) + add_lemma(string_axioms[i]); //,false); + else if(string_axioms[i].is_univ_quant()) { + debug() << "universaly quantified : " << pretty_short(string_axioms[i]) << eom; + universal_axioms.push_back(string_axioms[i]); + } + else { + assert(string_axioms[i].is_not_contains()); + string_axioms[i].witness = string_exprt::fresh_symbol + ("not_contains_witness", + array_typet(refined_string_typet::index_type(), + infinity_exprt(refined_string_typet::index_type()))); + not_contains_axioms.push_back(string_axioms[i]); + } + + string_axioms.clear(); + + initial_index_set(universal_axioms); + debug() << "string_refinementt::dec_solve: warning update_index_set has to be checked" << eom; + update_index_set(cur); + cur.clear(); + add_instantiations(); + + while(initial_loop_bound-- > 0) + { + print_time("string_refinementt::dec_solve"); + decision_proceduret::resultt res = SUB::dec_solve(); + + switch(res) + { + case D_SATISFIABLE: + if(!check_axioms()) { + debug() << "check_SAT: got SAT but the model is not correct" << eom; + } + else { + debug() << "check_SAT: the model is correct" << eom; + return D_SATISFIABLE; + } + + debug() << "refining.." << eom; + current_index_set.clear(); + update_index_set(cur); + cur.clear(); + add_instantiations(); + + if(variable_with_multiple_occurence_in_index) { + debug() << "WARNING: some variable appears multiple times" << eom; + return D_ERROR; + } + + if(current_index_set.empty()){ + debug() << "current index set is empty" << eom; + return D_SATISFIABLE; + } + + display_index_set(); + debug()<< "instantiating NOT_CONTAINS constraints" << eom; + for(int i=0; i lemmas; + instantiate_not_contains(not_contains_axioms[i],lemmas); + for(int j=0; j (s1.length = s2.length && forall i < s1.length. s1[i] = s2[i]) + // We can't do it directly because of the universal quantification inside. + // So we say instead the three following: + // eq => s1.length = s2.length + // forall i < s1.length. eq => s1[i] = s2[i] + // !eq => s1.length != s2.length || (witness < s1.length && s1[witness] != s2[witness]) + + symbol_exprt witness = fresh_index("witness_unequal"); + symbol_exprt qvar = string_exprt::fresh_symbol("qvar_equal", index_type); + + string_axioms.emplace_back(eq, equal_exprt(s1.length(), s2.length())); + + string_axioms.push_back + (string_constraintt(eq,equal_exprt(s1[qvar],s2[qvar]) + ).forall(qvar,zero,s1.length())); + + string_axioms.emplace_back + (not_exprt(eq), + or_exprt(notequal_exprt(s1.length(), s2.length()), + string_constraintt(notequal_exprt(s1[witness],s2[witness])).exists(witness,zero,s1.length()))); + + return tc_eq; +} + +exprt character_equals_ignore_case(exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z) { + exprt is_upper_case_1 = and_exprt(binary_relation_exprt(char_A,ID_le,char1), + binary_relation_exprt(char1,ID_le,char_Z)); + exprt is_upper_case_2 = and_exprt(binary_relation_exprt(char_A,ID_le,char2), + binary_relation_exprt(char2,ID_le,char_Z)); + return or_exprt(or_exprt(equal_exprt(char1,char2), + and_exprt(is_upper_case_1, equal_exprt(minus_exprt(plus_exprt(char_a,char1),char_A),char2))), + and_exprt(is_upper_case_2, equal_exprt(minus_exprt(plus_exprt(char_a,char2),char_A),char1))); +} + +exprt string_refinementt::convert_string_equals_ignore_case(const function_application_exprt &f) { + assert(f.type() == bool_typet() || f.type().id() == ID_c_bool); + + symbol_exprt eq = fresh_boolean("equal_ignore_case"); + typecast_exprt tc_eq(eq,f.type()); + + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); //bad args to string equal? + + bool is_c_string = refined_string_typet::is_c_string_type(f.type()); + exprt char_a; + exprt char_A; + exprt char_Z; + if(is_c_string) { + char_a = constant_of_nat(97,refined_string_typet::char_type()); + char_A = constant_of_nat(65,refined_string_typet::char_type()); + char_Z = constant_of_nat(90,refined_string_typet::char_type()); + } else { + char_a = constant_of_nat(97,refined_string_typet::java_char_type()); + char_A = constant_of_nat(65,refined_string_typet::java_char_type()); + char_Z = constant_of_nat(90,refined_string_typet::java_char_type()); + } + + string_exprt s1 = make_string(args[0]); + string_exprt s2 = make_string(args[1]); + symbol_exprt witness = fresh_index("witness_unequal_ignore_case"); + symbol_exprt qvar = string_exprt::fresh_symbol("qvar_equal_ignore_case", index_type); + + string_axioms.emplace_back(eq, equal_exprt(s1.length(), s2.length())); + + string_axioms.push_back + (string_constraintt(eq,character_equals_ignore_case(s1[qvar],s2[qvar],char_a,char_A,char_Z) + ).forall(qvar,zero,s1.length())); + + string_axioms.emplace_back + (not_exprt(eq), + or_exprt(notequal_exprt(s1.length(), s2.length()), + string_constraintt(not_exprt(character_equals_ignore_case(s1[witness],s2[witness],char_a,char_A,char_Z))).exists(witness,zero,s1.length()))); + + return tc_eq; +} + + +bvt string_refinementt::convert_string_length( + const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 1); + string_exprt str = make_string(args[0]); + exprt length = str.length(); + return convert_bv(length); +} + +exprt string_refinementt::is_positive(const exprt & x) +{ return binary_relation_exprt(x, ID_ge, refined_string_typet::index_of_int(0)); } + + +exprt string_refinementt::convert_string_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt & offset) +{ + symbol_exprt isprefix = fresh_boolean("isprefix"); + string_axioms.emplace_back(isprefix, str >= plus_exprt(prefix.length(),offset)); + + // forall 0 <= witness < prefix.length. isprefix => s0[witness+offset] = s2[witness] + symbol_exprt qvar = string_exprt::fresh_symbol("QA_isprefix", index_type); + string_axioms.push_back + (string_constraintt(isprefix, equal_exprt(str[plus_exprt(qvar,offset)],prefix[qvar]) + ).forall(qvar,zero,prefix.length())); + + symbol_exprt witness = fresh_index("witness_not_isprefix"); + + or_exprt s0_notpref_s1(not_exprt(str >= plus_exprt(prefix.length(),offset)), + and_exprt + (str >= plus_exprt(prefix.length(),offset), + and_exprt(binary_relation_exprt(witness,ID_ge,zero), + and_exprt(prefix > witness, + notequal_exprt(str[plus_exprt(witness,offset)],prefix[witness]))))); + + string_axioms.emplace_back(implies_exprt (not_exprt(isprefix),s0_notpref_s1)); + return isprefix; +} + +exprt string_refinementt::convert_string_is_prefix +(const function_application_exprt &f, bool swap_arguments) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(f.type() == bool_typet() || f.type().id() == ID_c_bool); + string_exprt s0 = make_string(args[swap_arguments?1:0]); + string_exprt s1 = make_string(args[swap_arguments?0:1]); + exprt offset; + + if(args.size() == 2) offset = zero; + else if (args.size() == 3) offset = args[2]; + + return typecast_exprt(convert_string_is_prefix(s0,s1,offset),f.type()); +} + +exprt string_refinementt::convert_string_is_empty +(const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 1); + assert(f.type() == bool_typet() || f.type().id() == ID_c_bool); + + symbol_exprt is_empty = fresh_boolean("is_empty"); + string_exprt s0 = make_string(args[0]); + string_axioms.emplace_back(implies_exprt(is_empty, equal_exprt(s0.length(),zero))); + string_axioms.emplace_back(implies_exprt(equal_exprt(s0.length(),zero),is_empty)); + return typecast_exprt(is_empty,f.type()); + +} + +bvt string_refinementt::convert_string_is_suffix +(const function_application_exprt &f, bool swap_arguments) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); // bad args to string issuffix? + assert(f.type() == bool_typet() || f.type().id() == ID_c_bool); + + symbol_exprt issuffix = fresh_boolean("issuffix"); + typecast_exprt tc_issuffix(issuffix,f.type()); + string_exprt s0 = make_string(args[swap_arguments?1:0]); + string_exprt s1 = make_string(args[swap_arguments?0:1]); + + + // issufix(s1,s0) => s0.length >= s1.length + // && forall witness < s1.length. + // issufix => s1[witness] = s0[witness + s0.length - s1.length] + // && !issuffix => s1.length > s0.length + // || (s1.length > witness && s1[witness] != s0[witness + s0.length - s1.length] + + string_axioms.emplace_back(implies_exprt(issuffix, s1 >= s0)); + + symbol_exprt qvar = string_exprt::fresh_symbol("QA_suffix", index_type); + exprt qvar_shifted = plus_exprt(qvar, + minus_exprt(s1.length(), s0.length())); + string_axioms.push_back + (string_constraintt(issuffix, equal_exprt(s0[qvar],s1[qvar_shifted]) + ).forall(qvar,zero,s0.length())); + + symbol_exprt witness = fresh_index("witness_not_suffix"); + + exprt shifted = plus_exprt(witness, + minus_exprt(s1.length(), s0.length())); + + implies_exprt lemma2(not_exprt(issuffix), + and_exprt(is_positive(witness), + or_exprt(s0 > s1, + and_exprt(s0 > witness, + notequal_exprt(s0[witness],s1[shifted]))))); + + string_axioms.emplace_back(lemma2); + + return convert_bv(tc_issuffix); +} + + +bvt string_refinementt::convert_string_contains( + const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); // bad args to string contains? + assert(f.type() == bool_typet() || f.type().id() == ID_c_bool); + + symbol_exprt contains = fresh_boolean("contains"); + typecast_exprt tc_contains(contains,f.type()); + string_exprt s0 = make_string(args[0]); + string_exprt s1 = make_string(args[1]); + + // contains => s0.length >= s1.length + // && startpos <= s0.length - s1.length + // && forall qvar < s1.length. + // contains => s1[qvar] = s0[startpos + qvar] + // !contains => s1.length > s0.length + // || (forall startpos <= s0.length - s1.length. + // exists witness < s1.length && s1[witness] != s0[witness + startpos] + + string_axioms.emplace_back(implies_exprt(contains, s0 >= s1)); + + symbol_exprt startpos = fresh_index("startpos_contains"); + + string_axioms.emplace_back(//implies_exprt(contains, + and_exprt(is_positive(startpos),binary_relation_exprt(startpos, ID_le, minus_exprt(s0.length(),s1.length())))); + + symbol_exprt qvar = string_exprt::fresh_symbol("QA_contains", index_type); + exprt qvar_shifted = plus_exprt(qvar, startpos); + string_axioms.push_back + (string_constraintt(contains,equal_exprt(s1[qvar],s0[qvar_shifted]) + ).forall(qvar,zero,s1.length())); + + // We rewrite the axiom for !contains as: + // forall startpos <= |s0| - |s1|. (!contains && |s0| >= |s1| ) + // ==> exists witness < |s1|. s1[witness] != s0[startpos+witness] + + string_axioms.push_back + (string_constraintt::not_contains + (zero,plus_exprt(refined_string_typet::index_of_int(1),minus_exprt(s0.length(),s1.length())), + and_exprt(not_exprt(contains),s0 >= s1),zero,s1.length(),s0,s1)); + + return convert_bv(tc_contains); +} + + +symbol_exprt string_refinementt::fresh_index(const irep_idt &prefix){ + symbol_exprt i = string_exprt::fresh_symbol(prefix,index_type); + index_symbols.push_back(i); + return i; +} + +symbol_exprt string_refinementt::fresh_boolean(const irep_idt &prefix){ + symbol_exprt b = string_exprt::fresh_symbol(prefix,bool_typet()); + boolean_symbols.push_back(b); + return b; +} + +exprt string_refinementt::convert_string_hash_code(const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + string_exprt str = make_string(args[0]); + typet return_type = f.type(); + + // initialisation of the missing pool variable + std::map::iterator it; + for(it = symbol_to_string.begin(); it != symbol_to_string.end(); it++) + if(hash.find(it->second) == hash.end()) + hash[it->second] = string_exprt::fresh_symbol("hash", return_type); + + // for each string s. + // hash(str) = hash(s) || |str| != |s| || (|str| == |s| && exists i < |s|. s[i] != str[i]) + + // WARNING: the specification may be incomplete + for(it = symbol_to_string.begin(); it != symbol_to_string.end(); it++) { + symbol_exprt i = string_exprt::fresh_symbol("index_hash", refined_string_typet::index_type()); + string_axioms.emplace_back + (or_exprt + (equal_exprt(hash[it->second],hash[str]), + or_exprt + (not_exprt(equal_exprt(it->second.length(),str.length())), + and_exprt(equal_exprt(it->second.length(),str.length()), + and_exprt + (not_exprt(equal_exprt(str[i],it->second[i])), + and_exprt(str>i,binary_relation_exprt(i,ID_ge,zero ))) + )))); + } + + + return hash[str]; +} + +exprt string_refinementt::convert_string_index_of(const string_exprt &str, const exprt & c, const exprt & from_index){ + symbol_exprt index = fresh_index("index_of"); + symbol_exprt contains = fresh_boolean("contains_in_index_of"); + + // from_index <= i < |s| && (i = -1 <=> !contains) && (contains => i >= from_index && s[i] = c) + // && forall n. from_index <= n < i => s[n] != c + + string_axioms.push_back(string_constraintt(equal_exprt(index,refined_string_typet::index_of_int(-1)),not_exprt(contains)).exists(index,refined_string_typet::index_of_int(-1),str.length())); + string_axioms.emplace_back(not_exprt(contains),equal_exprt(index,refined_string_typet::index_of_int(-1))); + string_axioms.emplace_back(contains,and_exprt(binary_relation_exprt(from_index,ID_le,index),equal_exprt(str[index],c))); + + symbol_exprt n = string_exprt::fresh_symbol("QA_index_of",index_type); + + string_axioms.push_back(string_constraintt(contains,not_exprt(equal_exprt(str[n],c))).forall(n,from_index,index)); + + symbol_exprt m = string_exprt::fresh_symbol("QA_index_of",index_type); + + string_axioms.push_back(string_constraintt(not_exprt(contains),not_exprt(equal_exprt(str[m],c))).forall(m,from_index,str.length())); + + return index; +} + +exprt string_refinementt::convert_string_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index) +{ + symbol_exprt offset = fresh_index("index_of"); + + symbol_exprt contains = fresh_boolean("contains_substring"); + string_axioms.emplace_back(contains, and_exprt + (str >= plus_exprt(substring.length(),offset), + binary_relation_exprt(offset,ID_ge,from_index))); + string_axioms.emplace_back(not_exprt(contains), equal_exprt(offset,refined_string_typet::index_of_int(-1))); + + // forall 0 <= witness < substring.length. contains => str[witness+offset] = substring[witness] + symbol_exprt qvar = string_exprt::fresh_symbol("QA_index_of_string", index_type); + string_axioms.push_back + (string_constraintt(contains, equal_exprt(str[plus_exprt(qvar,offset)],substring[qvar]) + ).forall(qvar,zero,substring.length())); + + + debug() << "string_refinementt::convert_string_index_of_string : warning the stpecification is only partial" << eom; + + return offset; +} + +exprt string_refinementt::convert_string_last_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index) +{ + symbol_exprt offset = fresh_index("index_of"); + + symbol_exprt contains = fresh_boolean("contains_substring"); + string_axioms.emplace_back(contains, and_exprt + (str >= plus_exprt(substring.length(),offset), + binary_relation_exprt(offset,ID_le,from_index))); + string_axioms.emplace_back(not_exprt(contains), equal_exprt(offset,refined_string_typet::index_of_int(-1))); + + // forall 0 <= witness < substring.length. contains => str[witness+offset] = substring[witness] + symbol_exprt qvar = string_exprt::fresh_symbol("QA_index_of_string", index_type); + string_axioms.push_back + (string_constraintt(contains, equal_exprt(str[plus_exprt(qvar,offset)],substring[qvar]) + ).forall(qvar,zero,substring.length())); + + debug() << "string_refinementt::convert_string_last_index_of_string : warning the stpecification is only partial" << eom; + return offset; +} + + +exprt string_refinementt::convert_string_index_of( + const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(f.type() == index_type); + string_exprt str = make_string(args[0]); + exprt c = args[1]; + exprt from_index; + + if(args.size() == 2) from_index = zero; + else if (args.size() == 3) from_index = args[2]; + else assert(false); + + if(refined_string_typet::is_java_string_type(c.type())){ + string_exprt sub = make_string(c); + return convert_string_index_of_string(str,sub,from_index); + } else { + if(!(c.type() == char_type || c.type() == java_char_type)){ + debug() << "warning: argument to string_index_of does not have char type: " + << c.type().pretty() << eom; + c = typecast_exprt(c,java_char_type); + } + return convert_string_index_of(str,c,from_index); + } + +} + +exprt string_refinementt::convert_string_last_index_of(const string_exprt &str, const exprt & c, const exprt & from_index) { + symbol_exprt index = fresh_index("last_index_of"); + symbol_exprt contains = fresh_boolean("contains_in_last_index_of"); + + // -1 <= i <= from_index && (i = -1 <=> !contains) && (contains => i <= from_index && s[i] = c) + // && forall n. i <= n <= from_index => s[n] != c + + exprt from_index_plus_one = plus_exprt(from_index,refined_string_typet::index_of_int(1)); + string_axioms.push_back(string_constraintt(equal_exprt(index,refined_string_typet::index_of_int(-1)),not_exprt(contains)).exists(index,refined_string_typet::index_of_int(-1),from_index_plus_one)); + string_axioms.emplace_back(not_exprt(contains),equal_exprt(index,refined_string_typet::index_of_int(-1))); + string_axioms.emplace_back(contains,and_exprt(binary_relation_exprt(zero,ID_le,index),and_exprt(binary_relation_exprt(from_index,ID_ge,index),equal_exprt(str[index],c)))); + + symbol_exprt n = string_exprt::fresh_symbol("QA_last_index_of",index_type); + string_axioms.push_back(string_constraintt(contains,not_exprt(equal_exprt(str[n],c))).forall(n,plus_exprt(index,refined_string_typet::index_of_int(1)),from_index_plus_one)); + + symbol_exprt m = string_exprt::fresh_symbol("QA_last_index_of",index_type); + string_axioms.push_back(string_constraintt(not_exprt(contains),not_exprt(equal_exprt(str[m],c))).forall(m,zero,from_index_plus_one)); + + return index; + +} + +exprt string_refinementt::convert_string_last_index_of( + const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(f.type() == index_type); + string_exprt str = make_string(args[0]); + exprt c = args[1]; + exprt from_index; + + if(args.size() == 2) from_index = minus_exprt(str.length(),refined_string_typet::index_of_int(1)); + else if (args.size() == 3) from_index = args[2]; + else assert(false); + + if(refined_string_typet::is_java_string_type(c.type())){ + string_exprt sub = make_string(c); + return convert_string_last_index_of_string(str,sub,from_index); + } else { + if(!(c.type() == char_type || c.type() == java_char_type)){ + debug() << "warning: argument to string_index_of does not have char type: " + << c.type().pretty() << eom; + c = typecast_exprt(c,java_char_type); + } + return convert_string_last_index_of(str,c,from_index); + } +} + +bvt string_refinementt::convert_char_literal( + const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 1); // there should be exactly 1 argument to char literal + + const exprt &arg = args[0]; + // for C programs argument to char literal should be one string constant of size one + if(arg.operands().size() == 1 && + arg.op0().operands().size() == 1 && + arg.op0().op0().operands().size() == 2 && + arg.op0().op0().op0().id() == ID_string_constant) + { + const string_constantt s = to_string_constant(arg.op0().op0().op0()); + irep_idt sval = s.get_value(); + assert(sval.size() == 1); + + std::string binary=integer2binary(unsigned(sval[0]), STRING_SOLVER_CHAR_WIDTH); + + return convert_bv(constant_exprt(binary, char_type)); + } + else { + throw "convert_char_literal unimplemented"; + } + +} + + +bvt string_refinementt::convert_string_char_at( + const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); //string_char_at expects 2 arguments + string_exprt str = make_string(args[0]); + + if(f.type() == char_type) { + symbol_exprt char_sym = string_exprt::fresh_symbol("char",char_type); + string_axioms.emplace_back(equal_exprt(char_sym,str[args[1]])); + return convert_bv(char_sym); + } else { + assert(f.type() == java_char_type); + symbol_exprt char_sym = string_exprt::fresh_symbol("char",java_char_type); + string_axioms.emplace_back(equal_exprt(char_sym,str[args[1]])); + return convert_bv(char_sym); + } +} + + + +constant_exprt string_refinementt::constant_of_nat(int i,typet t) { + return constant_exprt(integer2binary(i, boolbv_width(t)), t); +} + +exprt string_refinementt::convert_string_parse_int +(const function_application_exprt &expr) +{ + const function_application_exprt::argumentst &args = expr.arguments(); + assert(args.size() == 1); + + string_exprt str = make_string(args[0]); + typet type = expr.type(); + symbol_exprt i = string_exprt::fresh_symbol("parsed_int",type); + + exprt zero_char; + exprt minus_char; + exprt plus_char; + if(refined_string_typet::is_c_string_type(args[0].type())) { + plus_char = constant_of_nat(43,refined_string_typet::char_type()); + minus_char = constant_of_nat(45,refined_string_typet::char_type()); + zero_char = constant_of_nat(48,refined_string_typet::char_type()); + } + else { + plus_char = constant_of_nat(43,refined_string_typet::java_char_type()); + minus_char = constant_of_nat(45,refined_string_typet::java_char_type()); + zero_char = constant_of_nat(48,refined_string_typet::java_char_type()); + } + + exprt ten = constant_of_nat(10,type); + + exprt chr = str[refined_string_typet::index_of_int(0)]; + exprt starts_with_minus = equal_exprt(chr,minus_char); + exprt starts_with_plus = equal_exprt(chr,plus_char); + exprt starts_with_digit = binary_relation_exprt(chr,ID_ge,zero_char); + + for(int size=1; size<=10;size++) { + exprt sum = constant_of_nat(0,type); + exprt first_value = typecast_exprt(minus_exprt(chr,zero_char),type); + + for(int j=1; j::iterator i = current_index_set.begin(), + end = current_index_set.end(); i != end; ++i) { + const exprt &s = i->first; + debug() << "IS(" << pretty_short(s) << ") == {"; + + for (expr_sett::const_iterator j = i->second.begin(), end = i->second.end(); + j != end; ++j) + debug() << pretty_short (*j) << "; "; + debug() << "}" << eom; + + + for (expr_sett::const_iterator j = i->second.begin(), end = i->second.end(); + j != end; ++j) { + const exprt &val = *j; + + for (size_t k = 0; k < universal_axioms.size(); ++k) { + assert(universal_axioms[k].is_univ_quant()); + string_constraintt lemma = instantiate(universal_axioms[k], s, val); + assert(lemma.is_simple()); + add_lemma(lemma); + } + } + } +} + +exprt string_refinementt::convert_string_to_char_array +(const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 1); + + string_exprt str = make_string(args[0]); + debug() << "convert_string_to_char_array returns: " << str.content().pretty() << eom; + return str.content(); +} + + + + + +exprt string_refinementt::convert_string_compare_to(const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + + string_exprt s1 = make_string(args[0]); + string_exprt s2 = make_string(args[1]); + typet return_type = f.type(); + symbol_exprt res = string_exprt::fresh_symbol("compare_to",return_type); + + // In the lexicographic comparison, x is the first point where the two strings differ. + // res == 0 => |s1| = |s2| && forall i < |s1|. s1[i] == s2[i] + // res != 0 => + // (|s1| <= |s2| && exists x < |s1|. res = s1[x] - s2[x] && forall i= |s2| && exists x < |s2|. res = s1[x] - s2[x] && forall i |s2| && res = |s1| - |s2| && forall i<|s2| s1[i]=s2[i]) + + // The second part can be rewriten as: + // exists x. + // res != 0 ==> x> 0 && + // ((|s1| <= |s2| && x < |s1|) || (|s1| >= |s2| && x < |s2|) && res = s1[x] - s2[x] ) + // || (|s1| < |s2| && x = |s1|) || (|s1| > |s2| && x = |s2|) && res = |s1| - |s2| + // && forall i < x. res != 0 => s1[i] = s2[i] + + symbol_exprt i = string_exprt::fresh_symbol("QA_compare_to",index_type); + equal_exprt res_null = equal_exprt(res,constant_of_nat(0,return_type)); + string_axioms.emplace_back(res_null, equal_exprt(s1.length(),s2.length())); + string_axioms.push_back(string_constraintt(res_null,equal_exprt(s1[i],s2[i])).forall(i,zero,s1.length())); + symbol_exprt x = fresh_index("index_compare_to"); + string_axioms.push_back + (implies_exprt + (not_exprt(res_null), + and_exprt + (binary_relation_exprt(x,ID_ge,constant_of_nat(0,return_type)), + or_exprt + (and_exprt + (equal_exprt(res,typecast_exprt(minus_exprt(s1[x],s2[x]),return_type)), + or_exprt + (and_exprt(s1<=s2,s1 > x), and_exprt(s1>=s2,s2 > x))), + and_exprt + (equal_exprt(res,typecast_exprt(minus_exprt(s1.length(),s2.length()),return_type)), + or_exprt + (and_exprt(s2>s1,equal_exprt(x,s1.length())), and_exprt(s1>s2,equal_exprt(x,s2.length())))))) + )); + + string_axioms.push_back(string_constraintt(not_exprt(res_null),equal_exprt(s1[i],s2[i])).forall(i,zero,x)); + + return res; +} + +symbol_exprt string_refinementt::convert_string_intern(const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 1); + string_exprt str = make_string(args[0]); + typet return_type = f.type(); + + + // initialisation of the missing pool variable + std::map::iterator it; + for(it = symbol_to_string.begin(); it != symbol_to_string.end(); it++) + if(pool.find(it->second) == pool.end()) + pool[it->second] = string_exprt::fresh_symbol("pool", return_type); + + // intern(str) = s_0 || s_1 || ... + // for each string s. + // intern(str) = intern(s) || |str| != |s| || (|str| == |s| && exists i < |s|. s[i] != str[i]) + + //symbol_exprt intern = string_exprt::fresh_symbol("intern",return_type); + + exprt disj = false_exprt(); + for(it = symbol_to_string.begin(); it != symbol_to_string.end(); it++) + disj = or_exprt(disj, equal_exprt(pool[str], symbol_exprt(it->first,return_type))); + + string_axioms.emplace_back(disj); + + + // WARNING: the specification may be incomplete or incorrect + for(it = symbol_to_string.begin(); it != symbol_to_string.end(); it++) + if(it->second != str) { + symbol_exprt i = string_exprt::fresh_symbol("index_intern", refined_string_typet::index_type()); + string_axioms.emplace_back + (or_exprt + (equal_exprt(pool[it->second],pool[str]), + or_exprt + (not_exprt(equal_exprt(it->second.length(),str.length())), + and_exprt(equal_exprt(it->second.length(),str.length()), + and_exprt(not_exprt(equal_exprt(str[i],it->second[i])), + and_exprt(str>i,binary_relation_exprt(i,ID_ge,zero))) + )))); + } + + + return pool[str]; +} + + +//// Pass algorithm + +unsigned integer_of_expr(const constant_exprt & expr) { + return integer2unsigned(string2integer(as_string(expr.get_value()),2)); +} + +std::string string_refinementt::string_of_array(const exprt &arr, const exprt &size) +{ + if(size.id() != ID_constant) return "string of unknown size"; + unsigned n = integer_of_expr(to_constant_expr(size)); + if(n>500) return "very long string"; + if(n==0) return "\"\""; + unsigned str[n]; + exprt val = get(arr); + if(val.id() == "array-list") { + for (size_t i = 0; i < val.operands().size()/2; i++) { + exprt index = val.operands()[i*2]; + unsigned idx = integer_of_expr(to_constant_expr(index)); + if(idx < n){ + exprt value = val.operands()[i*2+1]; + str[idx] = integer_of_expr(to_constant_expr(value)); + } + } + } else { + return "unable to get array-list"; + } + + std::ostringstream buf; + buf << "\""; + for(unsigned i = 0; i < n; i++) { + char c = (char) str[i]; + if(31::iterator it; + for (it = symbol_to_string.begin(); it != symbol_to_string.end(); ++it) + { + string_exprt refined = it->second; + const exprt &econtent = refined.content(); + const exprt &elength = refined.length(); + + exprt len = get(elength); + exprt arr = get_array(econtent, len); + + fmodel[elength] = len; + fmodel[econtent] = arr; + debug() << it->first << " = " << pretty_short(it->second) + << " of length " << pretty_short(len) <<" := " << eom + << pretty_short(get(econtent)) << eom + << string_of_array(econtent,len) << eom; + } + + for(std::vector::iterator it = boolean_symbols.begin(); + it != boolean_symbols.end(); it++) { + debug() << "" << it->get_identifier() << " := " << pretty_short(get(*it)) << eom; + fmodel[*it] = get(*it); + } + + for(std::vector::iterator it = index_symbols.begin(); + it != index_symbols.end(); it++) { + debug() << "" << it->get_identifier() << " := " << pretty_short(get(*it)) << eom; + fmodel[*it] = get(*it); + } + + debug() << "in check axiom, the model may be incomplete" << eom; + std::vector< std::pair > violated; + + debug() << "there are " << universal_axioms.size() << " universal axioms" << eom; + for (size_t i = 0; i < universal_axioms.size(); ++i) { + const string_constraintt &axiom = universal_axioms[i]; + + exprt negaxiom = and_exprt(axiom.premise(), not_exprt(axiom.body())); + replace_expr(fmodel, negaxiom); + + debug() << "negaxiom: " << pretty_short(negaxiom) << eom; + + satcheck_no_simplifiert sat_check; + SUB solver(ns, sat_check); + solver << negaxiom; + + switch (solver()) { + case decision_proceduret::D_SATISFIABLE: { + exprt val = solver.get(axiom.get_univ_var()); + violated.push_back(std::make_pair(i, val)); + } break; + case decision_proceduret::D_UNSATISFIABLE: + break; + default: + throw "failure in checking axiom"; + } + } + + + debug() << "there are " << not_contains_axioms.size() << " not_contains axioms" << eom; + for (size_t i = 0; i < not_contains_axioms.size(); ++i) { + exprt val = get(not_contains_axioms[i].witness_of(zero)); + violated.push_back(std::make_pair(i, val)); + } + + + if (violated.empty()) { + debug() << "no violated property" << eom; + return true; + } + else { + debug() << violated.size() << " string axioms can be violated" << eom; + + if(use_counter_example) { + + std::vector new_axioms(violated.size()); + + // Checking if the current solution satisfies the constraints + for (size_t i = 0; i < violated.size(); ++i) { + + new_axioms[i] = universal_axioms[violated[i].first]; + + const exprt &val = violated[i].second; + const string_constraintt &axiom = universal_axioms[violated[i].first]; + + exprt premise(axiom.premise()); + exprt body(axiom.body()); + implies_exprt instance(premise, body); + debug() << "warning: we don't eliminate the existential quantifier" << eom; + replace_expr(axiom.get_univ_var(), val, instance); + if (seen_instances.insert(instance).second) { + add_lemma(instance); + } else debug() << "instance already seen" << eom; + } + } + + return false; + } + +} + + +// Gets the upper bounds that are applied to [qvar], in the expression [expr] +/* Shouldn't be necessary with the new way string constraints are encoded +void get_bounds(const exprt &qvar, const exprt &expr, std::vector & out) + { + std::vector to_treat; + to_treat.push_back(expr); + while(!to_treat.empty()) { + exprt e = to_treat.back(); + to_treat.pop_back(); + if (e.id() == ID_lt && e.op0() == qvar) { + assert(e.op1().type() == index_type || e.op1().type() == integer_typet()); + out.push_back(minus_exprt(e.op1(), refined_string_typet::index_of_int(1))); + } else if (e.id() == ID_le && e.op0() == qvar) { + out.push_back(e.op1()); + } else { + forall_operands(it, e) { + to_treat.push_back(*it); + } + } + } + } +*/ + + +std::map< exprt, int> string_refinementt::map_of_sum(const exprt &f) { + // number of time the element should be added (can be negative) + std::map< exprt, int> elems; + + std::vector< std::pair > to_process; + to_process.push_back(std::make_pair(f, true)); + + while (!to_process.empty()) { + exprt cur = to_process.back().first; + bool positive = to_process.back().second; + to_process.pop_back(); + if (cur.id() == ID_plus) { + to_process.push_back(std::make_pair(cur.op1(), positive)); + to_process.push_back(std::make_pair(cur.op0(), positive)); + } else if (cur.id() == ID_minus) { + to_process.push_back(std::make_pair(cur.op1(), !positive)); + to_process.push_back(std::make_pair(cur.op0(), positive)); + } else if (cur.id() == ID_unary_minus) { + to_process.push_back(std::make_pair(cur.op0(), !positive)); + } else { + if(positive) elems[cur] = elems[cur]+1; + else elems[cur] = elems[cur] - 1; + } + } + return elems; +} + + +exprt string_refinementt::sum_of_map(std::map & m, bool negated) { + exprt sum = refined_string_typet::index_of_int(0); + mp_integer constants = 0; + + for (std::map::iterator it = m.begin(); + it != m.end(); it++) { + // We should group constants together... + const exprt &t = it->first; + int second = negated?(-it->second):it->second; + if(t.id() == ID_constant) { + std::string value(to_constant_expr(t).get_value().c_str()); + constants += binary2integer(value,true) * second; + } else { + if(second != 0) + if(second == -1) + if(sum == refined_string_typet::index_of_int(0)) sum = unary_minus_exprt(t); + else sum = minus_exprt(sum,t); + else if(second == 1) + if(sum == refined_string_typet::index_of_int(0)) sum = t; + else sum = plus_exprt(sum, t); + else { + debug() << "in string_refinementt::sum_of_map:" + << " warning: several occurences of the same variable: " + << t.pretty() << eom; + variable_with_multiple_occurence_in_index = true; + if(second > 1) + for(int i = 0; i < second; i++) + sum = plus_exprt(sum, t); + else + for(int i = 0; i > second; i--) + sum = minus_exprt(sum, t); + } + } + } + + return plus_exprt(sum,constant_exprt(integer2binary(constants, STRING_SOLVER_INDEX_WIDTH), refined_string_typet::index_type())); +} + +exprt string_refinementt::simplify_sum(const exprt &f) { + std::map map = map_of_sum(f); + return sum_of_map(map); +} + +exprt string_refinementt::compute_subst(const exprt &qvar, const exprt &val, const exprt &f) +{ + exprt positive, negative; + // number of time the element should be added (can be negative) + // qvar has to be equal to val - f(0) if it appears positively in f + // (ie if f(qvar) = f(0) + qvar) and f(0) - val if it appears negatively + // in f. So we start by computing val - f(0). + std::map< exprt, int> elems = map_of_sum(minus_exprt(val,f)); + + bool found = false; + bool neg = false; // true if qvar appears negatively in f, ie positively in the elements + + for (std::map::iterator it = elems.begin(); + it != elems.end(); it++) { + const exprt &t = it->first; + if (t == qvar) { + if(it->second == 1 || it->second == -1){ + found = true; + neg = (it->second == 1); + } else { + debug() << "in string_refinementt::compute_subst:" + << " warning: occurences of qvar canceled out " << eom; + assert(it->second == 0); + } + elems.erase(it); + } + } + + if (!found) { + debug() << "string_refinementt::compute_subst: qvar not found" << eom; + debug() << "qvar = " << qvar.pretty() << eom + << "val = " << val.pretty() << eom + << "f = " << f.pretty() << eom; + assert(false); + } + + return sum_of_map(elems,neg); +} + + + +class find_qvar_visitor: public const_expr_visitort { +private: + const exprt &qvar_; + +public: + find_qvar_visitor(const exprt &qvar): qvar_(qvar) {} + + void operator()(const exprt &expr) { + if (expr == qvar_) throw true; + } +}; + +// Look for the given symbol in the index expression +bool find_qvar(const exprt index, const symbol_exprt & qvar) { + find_qvar_visitor v2(qvar); + try { + index.visit(v2); + return false; + } catch (bool found) {return found;} +} + + +void string_refinementt::initial_index_set(const axiom_vect & string_axioms) { + for (size_t i = 0; i < string_axioms.size(); ++i) { + initial_index_set(string_axioms[i]); + } +} + +void string_refinementt::update_index_set(const std::vector & cur) { + for (size_t i = 0; i < cur.size(); ++i) { + update_index_set(cur[i]); + } +} + +void string_refinementt::initial_index_set(const string_constraintt &axiom) +{ + assert(axiom.is_univ_quant()); + symbol_exprt qvar = axiom.get_univ_var(); + std::vector to_process; + to_process.push_back(axiom.body()); + + while (!to_process.empty()) { + exprt cur = to_process.back(); + to_process.pop_back(); + if (cur.id() == ID_index) { + const exprt &s = cur.op0(); + const exprt &i = cur.op1(); + + bool has_quant_var = find_qvar(i,qvar); + + // if cur is of the form s[i] and no quantified variable appears in i + if(!has_quant_var){ + current_index_set[s].insert(i); + index_set[s].insert(i); + } else { + // otherwise we add k-1 + exprt e(i); + replace_expr(qvar,minus_exprt(axiom.univ_bound_sup(),refined_string_typet::index_of_int(1)),e); + current_index_set[s].insert(e); + index_set[s].insert(e); + } + + } else { + forall_operands(it, cur) { + to_process.push_back(*it); + } + } + } +} + + +void string_refinementt::update_index_set(const exprt &formula) +{ + std::vector to_process; + to_process.push_back(formula); + + while (!to_process.empty()) { + exprt cur = to_process.back(); + to_process.pop_back(); + if (cur.id() == ID_index) { + const exprt &s = cur.op0(); + const exprt &i = cur.op1(); + assert(s.type().id() == ID_array); + const exprt &simplified = simplify_sum(i); + if(index_set[s].insert(simplified).second) { + debug() << "adding to index set of " << pretty_short(s) + << ": " << pretty_short(simplified) << eom; + current_index_set[s].insert(simplified); + } + } else { + forall_operands(it, cur) { + to_process.push_back(*it); + } + } + } +} + + +// Will be used to visit an expression and return the index used +// with the given char array +class find_index_visitor: public const_expr_visitort { +private: + const exprt &str_; + +public: + find_index_visitor(const exprt &str): str_(str){} + + void operator()(const exprt &expr) { + if (expr.id() == ID_index) { + const index_exprt &i = to_index_expr(expr); + if (i.array() == str_) + throw i.index(); + } + } +}; + +// Find an index used in the char array str +exprt find_index(const exprt & expr, const exprt & str) { + find_index_visitor v1(str); + try { + expr.visit(v1); + return nil_exprt(); + } + catch (exprt i) { return i; } +} + + + +string_constraintt string_refinementt::instantiate(const string_constraintt &axiom, + const exprt &str, const exprt &val) +{ + assert(axiom.is_univ_quant()); + exprt idx = find_index(axiom.body(),str); + if(idx.is_nil()) return string_constraintt(); + if(!find_qvar(idx,axiom.get_univ_var())) return string_constraintt(); + + exprt r = compute_subst(axiom.get_univ_var(), val, idx); + exprt instance(axiom); + replace_expr(axiom.get_univ_var(), r, instance); + // We are not sure the index set contains only positive numbers + exprt bounds = and_exprt(axiom.univ_within_bounds(),binary_relation_exprt(zero,ID_le,val)); + replace_expr(axiom.get_univ_var(), r, bounds); + return string_constraintt(bounds,instance); +} + + +void string_refinementt::instantiate_not_contains(const string_constraintt & axiom, std::vector & new_lemmas){ + assert(axiom.is_not_contains()); + exprt s0 = axiom.s0(); + exprt s1 = axiom.s1(); + + debug() << "instantiate not contains " << pretty_short(s0) << " : " << pretty_short(s1) << eom; + expr_sett index_set0 = index_set[to_string_expr(s0).content()]; + expr_sett index_set1 = index_set[to_string_expr(s1).content()]; + + for(expr_sett::iterator it0 = index_set0.begin(); it0 != index_set0.end(); it0++) + for(expr_sett::iterator it1 = index_set1.begin(); it1 != index_set1.end(); it1++) + { + debug() << pretty_short(*it0) << " : " << pretty_short(*it1) << eom; + exprt val = minus_exprt(*it0,*it1); + exprt lemma = implies_exprt(and_exprt(axiom.premise(),equal_exprt(axiom.witness_of(val), *it1)), not_exprt(equal_exprt(to_string_expr(s0)[*it0],to_string_expr(s1)[*it1]))); + new_lemmas.push_back(lemma); + // we put bounds on the witnesses: 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1| + exprt witness_bounds = implies_exprt + (and_exprt(binary_relation_exprt(zero,ID_le,val), binary_relation_exprt(minus_exprt(to_string_expr(s0).length(),to_string_expr(s1).length()),ID_ge,val)), + and_exprt(binary_relation_exprt(zero,ID_le,plus_exprt(val,axiom.witness_of(val))), + and_exprt(binary_relation_exprt(to_string_expr(s0).length(),ID_gt,plus_exprt(val,axiom.witness_of(val))), + and_exprt(binary_relation_exprt(to_string_expr(s1).length(),ID_gt,axiom.witness_of(val)), + binary_relation_exprt(zero,ID_le,axiom.witness_of(val)))))); + new_lemmas.push_back(witness_bounds); + } +} diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h new file mode 100644 index 00000000000..07334e19d96 --- /dev/null +++ b/src/solvers/refinement/string_refinement.h @@ -0,0 +1,216 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String support via axiom instantiation + (see the PASS paper at HVC'13) + +Author: Alberto Griggio, alberto.griggio@gmail.com + +\*******************************************************************/ + +#ifndef CPROVER_SOLVER_STRING_REFINEMENT_H +#define CPROVER_SOLVER_STRING_REFINEMENT_H + +#include + +#include +#include +#include + +class string_refinementt: public bv_refinementt +{ +public: + string_refinementt(const namespacet &_ns, propt &_prop); + ~string_refinementt() {}; + + // Should we use counter examples at each iteration? + bool use_counter_example; + + // Number of time we refine the index set before actually launching the solver + int initial_loop_bound; + + virtual std::string decision_procedure_text() const + { return "string refinement loop with "+prop.solver_text(); } + + symbol_exprt fresh_index(const irep_idt &prefix); + symbol_exprt fresh_boolean(const irep_idt &prefix); + + static exprt is_positive(const exprt & x); + +private: + typedef bv_refinementt SUB; + +protected: + + typedef std::set expr_sett; + typedef std::map expr_mapt; + + virtual void post_process(); + virtual bvt convert_symbol(const exprt &expr); + virtual bvt convert_function_application( + const function_application_exprt &expr); + virtual bvt convert_pointer_type(const exprt &expr); + + decision_proceduret::resultt dec_solve(); + + // fills as many 0 as necessary in the bit vectors to have the right width + bvt convert_bool_bv(const exprt &boole, const exprt &orig); + + // The following functions convert different string functions + // and add the corresponding lemmas to a list of properties to be checked + exprt convert_string_equal(const function_application_exprt &f); + exprt convert_string_equals_ignore_case(const function_application_exprt &f); + exprt convert_string_is_empty(const function_application_exprt &f); + bvt convert_string_length(const function_application_exprt &f); + exprt convert_string_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt & offset); + exprt convert_string_is_prefix(const function_application_exprt &f, bool swap_arguments=false); + bvt convert_string_is_suffix(const function_application_exprt &f, bool swap_arguments=false); + bvt convert_string_contains(const function_application_exprt &f); + exprt convert_string_hash_code(const function_application_exprt &f); + exprt convert_string_index_of(const string_exprt &str, const exprt & c, const exprt & from_index); + exprt convert_string_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index); + exprt convert_string_last_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index); + exprt convert_string_index_of(const function_application_exprt &f); + exprt convert_string_last_index_of(const string_exprt &str, const exprt & c, const exprt & from_index); + exprt convert_string_last_index_of(const function_application_exprt &f); + bvt convert_char_literal(const function_application_exprt &f); + bvt convert_string_char_at(const function_application_exprt &f); + exprt convert_string_code_point_at(const function_application_exprt &f); + exprt convert_string_code_point_before(const function_application_exprt &f); + + // Warning: this function is underspecified + exprt convert_string_code_point_count(const function_application_exprt &f); + // Warning: this function is underspecified + exprt convert_string_offset_by_code_point(const function_application_exprt &f); + exprt convert_string_parse_int(const function_application_exprt &f); + exprt convert_string_to_char_array(const function_application_exprt &f); + + exprt convert_string_compare_to(const function_application_exprt &f); + + // Warning: this does not work at the moment because of the way we treat string pointers + symbol_exprt convert_string_intern(const function_application_exprt &f); + + +private: + + // Tells if a char value is in the high-surrogates or low surrogates ranges + exprt is_high_surrogate(const exprt & chr); + exprt is_low_surrogate(const exprt & chr); + + // All constraints produced by the code + axiom_vect string_axioms; + + // Simple constraints that have been given to the solver + expr_sett seen_instances; + // + axiom_vect universal_axioms; + // + axiom_vect not_contains_axioms; + + int nb_sat_iteration; + + // Boolean symbols that are used to know whether the results + // of some functions should be true. + std::vector boolean_symbols; + + // Symbols used in existential quantifications + std::vector index_symbols; + + + // Unquantified lemmas that have newly been added + std::vector cur; + + // See the definition in the PASS article + // Warning: this is indexed by array_expressions and not string expressions + std::map current_index_set; + std::map index_set; + + // for debugging + void display_index_set(); + + // Tells if there is a index in the index set where the same variable occurs several time. + bool variable_with_multiple_occurence_in_index; + + std::map symbol_to_string; + inline void assign_to_symbol(const symbol_exprt & sym, const string_exprt & expr){ + symbol_to_string[sym.get_identifier()]= expr; + } + + string_exprt string_of_symbol(const symbol_exprt & sym); + + + std::map pool; + std::map hash; + + // Create a new string expression and add the necessary lemma + // to ensure its equal to the given string expression. + string_exprt make_string(const exprt &str); + + // Same thing but associates the string to the given symbol instead + // of returning it. + void make_string(const symbol_exprt & sym, const exprt &str); + + // Natural number expression corresponding to a constant integer + constant_exprt constant_of_nat(int i,typet t); + + void add_lemma(const exprt &lemma, bool add_to_index_set=true); + + //void set_to(const exprt &expr, bool value); + bool boolbv_set_equality_to_true(const equal_exprt &expr); + //bool set_equality_to_true(const equal_exprt &expr); + literalt convert_rest(const exprt &expr); + + // Instantiate forall constraints with index from the index set + void add_instantiations(); + + // Return true if the current model satisfies all the axioms + bool check_axioms(); + + // Add to the index set all the indices that appear in the formula + void update_index_set(const exprt &formula); + void update_index_set(const std::vector &cur); + void initial_index_set(const string_constraintt &axiom); + void initial_index_set(const axiom_vect &string_axioms); + + // Takes an universaly quantified formula [axiom], + // an array of char variable [s], and an index expression [val]. + // Computes one index [v1] in which [axiom.idx] appears, takes the + // corresponding substitition [r] (obtained with [compute_subst]). + // Then substitutes [axiom.idx] with [r] in [axiom]. + // axiom is not constant because we may record some information about + // instantiation of existential variables. + string_constraintt instantiate(const string_constraintt &axiom, const exprt &str, + const exprt &val); + + void instantiate_not_contains(const string_constraintt &axiom, std::vector & new_lemmas); + + // For expressions f of a certain form, // + // returns an expression corresponding to $f^{−1}(val)$.// + // i.e. the value that is necessary for qvar for f to // + // be equal to val. // + // Takes an expression containing + and − operations // + // in which qvar appears exactly once. // + // Rewrites it as a sum of qvar and elements in list // + // elems different from qvar. // + // Takes e minus the sum of the element in elems. // + exprt compute_subst(const exprt &qvar, const exprt &val, const exprt &f); + + // Rewrite a sum in a simple form: sum m_i * expr_i + std::map< exprt, int> map_of_sum(const exprt &f); + exprt sum_of_map(std::map &m,bool negated=false); + + // Simplify a sum (an expression with only plus and minus expr) + exprt simplify_sum(const exprt &f); + + // Gets a model of an array and put it in a certain form + exprt get_array(const exprt &arr, const exprt &size); + + // Convert the content of a string to a more readable representation + std::string string_of_array(const exprt &arr, const exprt &size); + + // succinct and pretty way to display an expression + std::string pretty_short(const exprt & expr); + + void print_time(std::string s); +}; + +#endif diff --git a/src/util/unicode.cpp b/src/util/unicode.cpp index 59aea736547..ee675cb8834 100644 --- a/src/util/unicode.cpp +++ b/src/util/unicode.cpp @@ -7,6 +7,8 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include +#include #include "unicode.h" @@ -253,3 +255,9 @@ const char **narrow_argv(int argc, const wchar_t **argv_wide) return argv_narrow; } + +std::wstring utf8_to_utf16(const std::string& in) +{ + std::wstring_convert > converter; + return converter.from_bytes(in); +} diff --git a/src/util/unicode.h b/src/util/unicode.h index 44038a26c04..05bc84a463d 100644 --- a/src/util/unicode.h +++ b/src/util/unicode.h @@ -22,6 +22,8 @@ std::wstring widen(const std::string &s); std::string utf32_to_utf8(const std::basic_string &s); std::string utf16_to_utf8(const std::basic_string &s); +std::wstring utf8_to_utf16(const std::string&); + const char **narrow_argv(int argc, const wchar_t **argv_wide); #endif