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..136633390b5 --- /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 int __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str); +extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(int 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_array/test.desc b/regression/strings/java_char_array/test.desc new file mode 100644 index 00000000000..59c8a082b1b --- /dev/null +++ b/regression/strings/java_char_array/test.desc @@ -0,0 +1,9 @@ +CORE +test_char_array.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_char_array.java line 11: SUCCESS$ +^\[assertion.2\] assertion at file test_char_array.java line 12: SUCCESS$ +^\[assertion.3\] assertion at file test_char_array.java line 13: FAILURE$ +-- \ No newline at end of file diff --git a/regression/strings/java_char_array/test_char_array.class b/regression/strings/java_char_array/test_char_array.class new file mode 100644 index 00000000000..836942da134 Binary files /dev/null and b/regression/strings/java_char_array/test_char_array.class differ diff --git a/regression/strings/java_char_array/test_char_array.java b/regression/strings/java_char_array/test_char_array.java new file mode 100644 index 00000000000..22ff962f2df --- /dev/null +++ b/regression/strings/java_char_array/test_char_array.java @@ -0,0 +1,15 @@ +public class test_char_array { + + public static void main(String[] argv) + { + String s = "abc"; + char [] str = s.toCharArray(); + int[] test = new int[312]; + char c = str[2]; + String t = argv[0]; + char d = t.charAt(0); + assert(str.length == 3); + assert(c == 'c'); + assert(c == d || d < 'a' || d > 'z' ); + } +} diff --git a/regression/strings/java_char_array_init/test.desc b/regression/strings/java_char_array_init/test.desc new file mode 100644 index 00000000000..102b24ceb72 --- /dev/null +++ b/regression/strings/java_char_array_init/test.desc @@ -0,0 +1,11 @@ +CORE +test_init.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_init.java line 16: SUCCESS$ +^\[assertion.2\] assertion at file test_init.java line 17: SUCCESS$ +^\[assertion.3\] assertion at file test_init.java line 18: SUCCESS$ +^\[assertion.4\] assertion at file test_init.java line 20: SUCCESS$ +^\[assertion.5\] assertion at file test_init.java line 21: FAILURE$ +-- \ No newline at end of file diff --git a/regression/strings/java_char_array_init/test_init.class b/regression/strings/java_char_array_init/test_init.class new file mode 100644 index 00000000000..be3baee56bd Binary files /dev/null and b/regression/strings/java_char_array_init/test_init.class differ diff --git a/regression/strings/java_char_array_init/test_init.java b/regression/strings/java_char_array_init/test_init.java new file mode 100644 index 00000000000..3f6b6e3a640 --- /dev/null +++ b/regression/strings/java_char_array_init/test_init.java @@ -0,0 +1,23 @@ +public class test_init { + + public static void main(String[] argv) + { + char [] str = new char[10]; + str[0] = 'H'; + str[1] = 'e'; + str[2] = 'l'; + str[3] = 'l'; + str[4] = 'o'; + String s = new String(str); + String t = new String(str,1,2); + + System.out.println(s); + System.out.println(s.length()); + assert(s.startsWith("Hello")); + assert(s.length() == 10); + assert(t.equals("el")); + String u = String.valueOf(str,3,2); + assert(u.equals("lo")); + assert(s.equals("Hello") || !t.equals("el") || !u.equals("lo")); + } +} 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_insert/test.desc b/regression/strings/java_string_builder_insert/test.desc new file mode 100644 index 00000000000..72b86d46f27 --- /dev/null +++ b/regression/strings/java_string_builder_insert/test.desc @@ -0,0 +1,8 @@ +CORE +test_insert.class +--pass +^EXIT=10$ +^SIGNAL=0$ +^\[assertion.1\] assertion at file test_insert.java line 17: SUCCESS$ +^\[assertion.2\] assertion at file test_insert.java line 18: FAILURE$ +-- diff --git a/regression/strings/java_string_builder_insert/test_insert.class b/regression/strings/java_string_builder_insert/test_insert.class new file mode 100644 index 00000000000..69a32d7f93f Binary files /dev/null and b/regression/strings/java_string_builder_insert/test_insert.class differ diff --git a/regression/strings/java_string_builder_insert/test_insert.java b/regression/strings/java_string_builder_insert/test_insert.java new file mode 100644 index 00000000000..5c291b76fe5 --- /dev/null +++ b/regression/strings/java_string_builder_insert/test_insert.java @@ -0,0 +1,20 @@ +public class test_insert { + + public static void main(String[] argv) + { + char [] str = new char[5]; + str[0] = 'H'; + str[1] = 'e'; + str[2] = 'l'; + str[3] = 'l'; + str[4] = 'o'; + + + StringBuilder sb = new StringBuilder(" world"); + sb.insert(0,str); + String s = sb.toString(); + System.out.println(s); + assert(s.equals("Hello world")); + assert(!s.equals("Hello world")); + } +} 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..a6895e71aea --- /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_string_length(s) == i + 5: SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"po\"),s): SUCCESS$ +^\[main.assertion.3\] assertion __CPROVER_char_at(s, i) == __CPROVER_char_literal(\"p\"): SUCCESS$ +^\[main.assertion.4\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"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..0445499cd88 --- /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_string_equal(t, __CPROVER_string_literal("apc")): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("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..499e1fe9e46 --- /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_char_literal("p"): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_char_at(u,2) == __CPROVER_char_literal("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..7e5b17c8994 --- /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_string_equal(s, __CPROVER_string_literal("pippo")): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("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..28aa9c7e156 --- /dev/null +++ b/regression/strings/test_int/test.c @@ -0,0 +1,18 @@ +#include +#include "../cprover-string-hack.h" + + +int main() +{ + __CPROVER_string s; + int i = 10; + s = __CPROVER_string_of_int(123); + assert(__CPROVER_char_at(s,0) == '1'); + assert(__CPROVER_char_at(s,1) == '2'); + + int 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..25a6a7ff59b --- /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_char_at(s,0) == .1.: SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_char_at(s,1) == .2.: SUCCESS$ +^\[main.assertion.3\] assertion j == 234: SUCCESS$ +^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at(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..b8d49988f50 --- /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_string_length(s3) == 0: FAILURE$ +^\[main.assertion.2\] assertion __CPROVER_string_length(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..da28fb44155 --- /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_string_equal(t,__CPROVER_string_literal("cd")): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cc")): FAILURE$ +^\[main.assertion.3\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("bc")): SUCCESS$ +^\[main.assertion.4\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("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..7c4823e9eb8 --- /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_string_issuffix(__CPROVER_string_literal("po"),s): SUCCESS$ +^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s): FAILURE$ +-- diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 3b0d7b5bc6a..6872dd31bed 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,13 @@ 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_preprocesst(symbol_table, goto_functions, ui_message_handler); + } + // remove returns, gcc vectors, complex remove_returns(symbol_table, goto_functions); remove_vector(symbol_table, goto_functions); @@ -1175,6 +1188,7 @@ void cbmc_parse_optionst::help() " --yices use Yices\n" " --z3 use Z3\n" " --refine use refinement procedure (experimental)\n" + " --pass use parameterized array for string solving (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..4d094819fad 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -84,6 +84,8 @@ class cbmc_solverst:public messaget solver = get_dimacs(); else if(options.get_bool_option("refine")) solver = get_bv_refinement(); + else if(options.get_bool_option("pass")) + 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 +113,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/config.inc b/src/config.inc index f8a78536372..19b64895c90 100644 --- a/src/config.inc +++ b/src/config.inc @@ -2,6 +2,7 @@ BUILD_ENV = AUTO # Variables you may want to override +CXXFLAGS = -Wall -O0 -g -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic #CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic #CXXFLAGS = -std=c++11 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..0e611956ddf --- /dev/null +++ b/src/goto-programs/pass_preprocess.cpp @@ -0,0 +1,437 @@ +/*******************************************************************\ + +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 "pass_preprocess.h" + +#include +#include +#include +#include +#include + +symbol_exprt pass_preprocesst::new_tmp_symbol +(const std::string &name, const typet &type) +{ + auxiliary_symbolt tmp_symbol; + tmp_symbol.base_name=name; + tmp_symbol.is_static_lifetime=false; + tmp_symbol.mode=ID_java; + tmp_symbol.name=name; + tmp_symbol.type=type; + symbol_table.add(tmp_symbol); + return symbol_exprt(name,type); +} + +void pass_preprocesst::declare_function(irep_idt function_name, const typet &type) +{ + auxiliary_symbolt func_symbol; + func_symbol.base_name=function_name; + func_symbol.is_static_lifetime=false; + func_symbol.mode=ID_java; + func_symbol.name=function_name; + func_symbol.type=type; + symbol_table.add(func_symbol); + goto_functions.function_map[function_name]; +} + +void pass_preprocesst::make_string_function +(goto_programt::instructionst::iterator & i_it, irep_idt function_name) +{ + code_function_callt &function_call=to_code_function_call(i_it->code); + code_typet function_type=to_code_type(function_call.function().type()); + declare_function(function_name,function_type); + function_application_exprt rhs; + rhs.type()=function_type.return_type(); + rhs.add_source_location()=function_call.source_location(); + rhs.function()=symbol_exprt(function_name); + for(unsigned i = 0; i < function_call.arguments().size(); i++) + rhs.arguments().push_back(replace_string_literals(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 pass_preprocesst::make_string_function_call +(goto_programt::instructionst::iterator & i_it, irep_idt function_name) +{ + code_function_callt &function_call=to_code_function_call(i_it->code); + code_typet function_type=to_code_type(function_call.function().type()); + declare_function(function_name,function_type); + 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(unsigned i = 1; i < function_call.arguments().size(); i++) + rhs.arguments().push_back(replace_string_literals(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; +} + +void pass_preprocesst::make_string_function_side_effect +(goto_programt::instructionst::iterator & i_it, irep_idt function_name) +{ + code_function_callt &function_call=to_code_function_call(i_it->code); + code_typet function_type=to_code_type(function_call.function().type()); + declare_function(function_name,function_type); + function_application_exprt rhs; + typet return_type = function_call.arguments()[0].type(); + rhs.type()=return_type; + rhs.add_source_location()=function_call.source_location(); + rhs.function()=symbol_exprt(function_name); + for(unsigned i = 0; i < function_call.arguments().size(); i++) + rhs.arguments().push_back(replace_string_literals(function_call.arguments()[i])); + code_assignt assignment(function_call.arguments()[0], rhs); + + // 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; +} + +void pass_preprocesst::make_to_char_array_function +(goto_programt & goto_program, goto_programt::instructionst::iterator & i_it) +{ + + code_function_callt &function_call=to_code_function_call(i_it->code); + if(function_call.lhs().type().id()!=ID_pointer) + debug() << "pass_preprocesst::make_to_char_array_function: " + << "the function call should return a pointer" << eom; + + typet object_type = function_call.lhs().type().subtype(); + exprt object_size = size_of_expr(object_type, ns); + + if(object_size.is_nil()) + debug() << "pass_preprocesst::make_to_char_array_function got nil object_size" << eom; + + auto location = function_call.source_location(); + std::vector new_code; + + side_effect_exprt malloc_expr(ID_malloc); + malloc_expr.copy_to_operands(object_size); + malloc_expr.type()=pointer_typet(object_type); + malloc_expr.add_source_location()=location; + + assert(function_call.arguments().size() >= 1); + exprt string_argument = replace_string_literals(function_call.arguments()[0]); + typet string_argument_type = string_argument.type(); + + // tmp_assign = MALLOC(struct java::array[reference],sizeof(s)) + symbol_exprt tmp_assign = new_tmp_symbol("tmp_assign", pointer_typet(object_type)); + code_assignt assign_malloc(tmp_assign, malloc_expr); + new_code.push_back(assign_malloc); + + // tmp_assign->length = (int)__CPROVER_uninterpreted_string_length_func(s); + declare_function(cprover_string_length_func,unsignedbv_typet(32)); + + function_application_exprt call_to_length; + call_to_length.type()=unsignedbv_typet(32); + call_to_length.add_source_location()=location; + call_to_length.function()=symbol_exprt(cprover_string_length_func); + call_to_length.arguments().push_back(string_argument); + + const struct_typet &struct_type=to_struct_type(ns.follow(object_type)); + dereference_exprt deref(tmp_assign, object_type); + member_exprt length(deref,struct_type.components()[1].get_name(), + struct_type.components()[1].type()); + code_assignt assign_length(length,typecast_exprt(call_to_length,signedbv_typet(32))); + new_code.push_back(assign_length); + + // tmp_assign->data = new data.type[length]; + assert(ns.follow(object_type).id()==ID_struct); + member_exprt data(deref,struct_type.components()[2].get_name(), + struct_type.components()[2].type()); + side_effect_exprt data_cpp_new_expr(ID_cpp_new_array, data.type()); + data_cpp_new_expr.set(ID_size, length); + symbol_exprt tmp_data = new_tmp_symbol("tmp_data", struct_type.components()[2].type()); + new_code.push_back(code_assignt(data, data_cpp_new_expr)); + + // tmp_assign->data = __CPROVER_uninterpreted_string_data_func(s,tmp_assing->data); + declare_function(cprover_string_data_func,void_typet()); + function_application_exprt call_to_data; + call_to_data.type()=void_typet(); + call_to_data.add_source_location()=location; + call_to_data.function()=symbol_exprt(cprover_string_data_func); + call_to_data.arguments().push_back(string_argument); + call_to_data.arguments().push_back(data); + call_to_data.arguments().push_back(dereference_exprt(data)); + + exprt tmp_nil = new_tmp_symbol("tmp_nil", void_typet()); + new_code.push_back(code_assignt(tmp_nil,call_to_data)); + + // return_tmp0 = tmp_assign + new_code.push_back(code_assignt(function_call.lhs(), tmp_assign)); + + // putting the assignements into the program + for(int i=0; imake_assignment(); + i_it->code=new_code[i]; + i_it->source_location=location; + if(icode); + exprt arg = function_call.arguments()[0]; + auto location = function_call.source_location(); + typet object_type = arg.type().subtype(); + + exprt array_size = member_exprt(dereference_exprt(arg,object_type) + ,"length",signedbv_typet(32)); + exprt data_pointer = member_exprt(dereference_exprt(arg,object_type),"data", + pointer_typet(pointer_typet(unsignedbv_typet(16)))); + exprt data = dereference_exprt(data_pointer, pointer_typet(unsignedbv_typet(16))); + + std::vector::iterator it = function_call.arguments().begin(); + *it = array_size; + function_call.arguments().insert(++it,data); + make_string_function(i_it,function_name); +} + +void pass_preprocesst::make_of_char_array_function_call +(goto_programt::instructionst::iterator & i_it, irep_idt function_name) +{ + code_function_callt &function_call=to_code_function_call(i_it->code); + exprt arg = function_call.arguments()[1]; + auto location = function_call.source_location(); + typet object_type = arg.type().subtype(); + exprt array_size = member_exprt(dereference_exprt(arg,object_type) + ,"length",signedbv_typet(32)); + exprt data_pointer = member_exprt(dereference_exprt(arg,object_type),"data", + pointer_typet(pointer_typet(unsignedbv_typet(16)))); + exprt data = dereference_exprt(data_pointer, pointer_typet(unsignedbv_typet(16))); + + std::vector::iterator it = function_call.arguments().begin(); + *(++it) = array_size; + function_call.arguments().insert(++it,data); + make_string_function_call(i_it,function_name); +} + +void pass_preprocesst::make_of_char_array_side_effect +(goto_programt::instructionst::iterator & i_it, irep_idt function_name) +{ + code_function_callt &function_call=to_code_function_call(i_it->code); + exprt arg = function_call.arguments()[2]; + auto location = function_call.source_location(); + typet object_type = arg.type().subtype(); + exprt array_size = member_exprt(dereference_exprt(arg,object_type) + ,"length",signedbv_typet(32)); + exprt data_pointer = member_exprt(dereference_exprt(arg,object_type),"data", + pointer_typet(pointer_typet(unsignedbv_typet(16)))); + exprt data = dereference_exprt(data_pointer, pointer_typet(unsignedbv_typet(16))); + + std::vector::iterator it = std::next(std::next(function_call.arguments().begin())); + *it = array_size; + function_call.arguments().insert(++it,data); + make_string_function_side_effect(i_it,function_name); +} + + +void pass_preprocesst::replace_string_calls +(goto_functionst::function_mapt::iterator f_it) +{ + goto_programt &goto_program=f_it->second.body; + + 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(unsigned 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(string_functions.find(function_id) != string_functions.end()) + make_string_function(i_it,string_functions[function_id]); + else if(side_effect_functions.find(function_id) != side_effect_functions.end()) + make_string_function_side_effect(i_it,side_effect_functions[function_id]); + else if(string_function_calls.find(function_id) != string_function_calls.end()) + make_string_function_call(i_it, string_function_calls[function_id]); + else if(string_of_char_array_functions.find(function_id) != string_of_char_array_functions.end()) + make_of_char_array_function(i_it,string_of_char_array_functions[function_id]); + else if(string_of_char_array_function_calls.find(function_id) != string_of_char_array_function_calls.end()) + make_of_char_array_function_call(i_it,string_of_char_array_function_calls[function_id]); + else if(side_effect_char_array_functions.find(function_id) != side_effect_char_array_functions.end()) + make_of_char_array_side_effect(i_it,side_effect_char_array_functions[function_id]); + else if(function_id == irep_idt("java::java.lang.String.toCharArray:()[C")) + make_to_char_array_function(goto_program,i_it); + } + } + else + { + if(i_it->is_assign()) + { + code_assignt assignment = to_code_assign(i_it->code); + exprt new_rhs = replace_string_literals(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; +} + +bool pass_preprocesst::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; +} + +exprt pass_preprocesst::replace_string_literals(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; +} + +pass_preprocesst::pass_preprocesst (symbol_tablet & _symbol_table, goto_functionst & _goto_functions, + message_handlert &_message_handler): + messaget(_message_handler), symbol_table(_symbol_table), ns(_symbol_table), + goto_functions(_goto_functions) + { + + // initialiasing the function maps + string_functions[irep_idt("java::java.lang.String.codePointAt:(I)I")] = cprover_string_code_point_at_func; + string_functions[irep_idt("java::java.lang.String.codePointBefore:(I)I")] = cprover_string_code_point_before_func; + string_functions[irep_idt("java::java.lang.String.codePointCount:(II)I")] = cprover_string_code_point_count_func; + string_functions[irep_idt("java::java.lang.String.offsetByCodePoints:(II)I")] = cprover_string_offset_by_code_point_func; + string_functions[irep_idt("java::java.lang.String.hashCode:()I")] = cprover_string_hash_code_func; + string_functions[irep_idt("java::java.lang.String.indexOf:(I)I")] = cprover_string_index_of_func; + string_functions[irep_idt("java::java.lang.String.indexOf:(II)I")] = cprover_string_index_of_func; + string_functions[irep_idt("java::java.lang.String.indexOf:(Ljava/lang/String;)I")] = cprover_string_index_of_func; + string_functions[irep_idt("java::java.lang.String.indexOf:(Ljava/lang/String;I)I")] = cprover_string_index_of_func; + string_functions[irep_idt("java::java.lang.String.lastIndexOf:(I)I")]=cprover_string_last_index_of_func; + string_functions[irep_idt("java::java.lang.String.lastIndexOf:(II)I")]=cprover_string_last_index_of_func; + string_functions[irep_idt("java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I")]=cprover_string_last_index_of_func; + string_functions[irep_idt("java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I")]=cprover_string_last_index_of_func; + string_functions[irep_idt("java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;")] = cprover_string_concat_func; + string_functions[irep_idt("java::java.lang.String.length:()I")] = cprover_string_length_func; + string_functions[irep_idt("java::java.lang.StringBuilder.length:()I")] = cprover_string_length_func; + string_functions[irep_idt("java::java.lang.String.equals:(Ljava/lang/Object;)Z")] = cprover_string_equal_func; + string_functions[irep_idt("java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z")] = cprover_string_equals_ignore_case_func; + string_functions[irep_idt("java::java.lang.String.startsWith:(Ljava/lang/String;)Z")] = cprover_string_startswith_func; + string_functions[irep_idt ("java::java.lang.String.startsWith:(Ljava/lang/String;I)Z")] = cprover_string_startswith_func; + string_functions[irep_idt("java::java.lang.String.endsWith:(Ljava/lang/String;)Z")] = cprover_string_endswith_func; + string_functions[irep_idt("java::java.lang.String.substring:(II)Ljava/lang/String;")] = cprover_string_substring_func; + string_functions[irep_idt("java::java.lang.String.substring:(II)Ljava/lang/String;")] = cprover_string_substring_func; + string_functions[irep_idt("java::java.lang.String.substring:(I)Ljava/lang/String;")] = cprover_string_substring_func; + string_functions[irep_idt("java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;")] = cprover_string_substring_func; + string_functions[irep_idt("java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;")] = cprover_string_substring_func; + string_functions[irep_idt("java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;")] = cprover_string_substring_func; + string_functions[irep_idt("java::java.lang.String.trim:()Ljava/lang/String;")] = cprover_string_trim_func; + string_functions[irep_idt("java::java.lang.String.toLowerCase:()Ljava/lang/String;")] = cprover_string_to_lower_case_func; + string_functions[irep_idt("java::java.lang.String.toUpperCase:()Ljava/lang/String;")] = cprover_string_to_upper_case_func; + string_functions[irep_idt("java::java.lang.String.replace:(CC)Ljava/lang/String;")] = cprover_string_replace_func; + string_functions[irep_idt("java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z")] = cprover_string_contains_func; + string_functions[irep_idt("java::java.lang.String.compareTo:(Ljava/lang/String;)I")] = cprover_string_compare_to_func; + string_functions[irep_idt("java::java.lang.String.intern:()Ljava/lang/String;")] = cprover_string_intern_func; + string_functions[irep_idt("java::java.lang.String.isEmpty:()Z")] = cprover_string_is_empty_func; + string_functions[irep_idt("java::java.lang.String.charAt:(I)C")] = cprover_string_char_at_func; + string_functions[irep_idt("java::java.lang.StringBuilder.charAt:(I)C")] = cprover_string_char_at_func; + string_functions[irep_idt("java::java.lang.CharSequence.charAt:(I)C")] = cprover_string_char_at_func; + string_functions[irep_idt("java::java.lang.StringBuilder.toString:()Ljava/lang/String;")] = cprover_string_copy_func; + + string_functions[irep_idt("java::java.lang.String.valueOf:(F)Ljava/lang/String;")] = cprover_string_of_float_func; + string_functions[irep_idt("java::java.lang.Float.toString:(F)Ljava/lang/String;")] = cprover_string_of_float_func; + string_functions[irep_idt("java::java.lang.Integer.toString:(I)Ljava/lang/String;")] = cprover_string_of_int_func; + string_functions[irep_idt("java::java.lang.String.valueOf:(I)Ljava/lang/String;")] = cprover_string_of_int_func; + string_functions[irep_idt("java::java.lang.Integer.toHexString:(I)Ljava/lang/String;")] = cprover_string_of_int_hex_func; + string_functions[irep_idt("java::java.lang.String.valueOf:(L)Ljava/lang/String;")] = cprover_string_of_long_func; + string_functions[irep_idt("java::java.lang.String.valueOf:(D)Ljava/lang/String;")] = cprover_string_of_double_func; + string_functions[irep_idt("java::java.lang.String.valueOf:(Z)Ljava/lang/String;")] = cprover_string_of_bool_func; + string_functions[irep_idt("java::java.lang.String.valueOf:(C)Ljava/lang/String;")] = cprover_string_of_char_func; + string_functions[irep_idt("java::java.lang.Integer.parseInt:(Ljava/lang/String;)I")] = cprover_string_parse_int_func; + + side_effect_functions[irep_idt("java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;")] = cprover_string_concat_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.setCharAt:(IC)V")] = cprover_string_char_set_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;")] = cprover_string_concat_int_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.append:(J)Ljava/lang/StringBuilder;")] = cprover_string_concat_long_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;")] = cprover_string_concat_bool_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;")] = cprover_string_concat_char_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;")] = cprover_string_concat_double_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.append:(F)Ljava/lang/StringBuilder;")] = cprover_string_concat_float_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.appendCodePoint:(I)Ljava/lang/StringBuilder;")] = cprover_string_concat_code_point_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.delete:(II)Ljava/lang/StringBuilder;")] = cprover_string_delete_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;")] = cprover_string_delete_char_at_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.insert:(ILjava/lang/String;)Ljava/lang/StringBuilder;")] = cprover_string_insert_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;")] = cprover_string_insert_int_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;")] = cprover_string_insert_long_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;")] = cprover_string_insert_char_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;") ] = cprover_string_insert_bool_func; + side_effect_functions[irep_idt("java::java.lang.StringBuilder.setLength:(I)V")] = cprover_string_set_length_func; + + + side_effect_char_array_functions[irep_idt("java::java.lang.StringBuilder.insert:(I[CII)Ljava/lang/StringBuilder;")] = cprover_string_insert_char_array_func; + side_effect_char_array_functions[irep_idt("java::java.lang.StringBuilder.insert:(I[C)Ljava/lang/StringBuilder;")] = cprover_string_insert_char_array_func; + + string_function_calls[irep_idt("java::java.lang.String.:(Ljava/lang/String;)V")] = cprover_string_copy_func; + string_function_calls[irep_idt("java::java.lang.String.:(Ljava/lang/StringBuilder;)V")] = cprover_string_copy_func; + string_function_calls[irep_idt("java::java.lang.StringBuilder.:(Ljava/lang/String;)V")] = cprover_string_copy_func; + string_function_calls[irep_idt("java::java.lang.String.:()V")] = cprover_string_empty_string_func; + string_function_calls[irep_idt("java::java.lang.StringBuilder.:()V")] = cprover_string_empty_string_func; + + string_of_char_array_function_calls[irep_idt("java::java.lang.String.:([C)V")] = cprover_string_of_char_array_func; + string_of_char_array_function_calls[irep_idt("java::java.lang.String.:([CII)V")] = cprover_string_of_char_array_func; + string_of_char_array_functions[irep_idt("java::java.lang.String.valueOf:([CII)Ljava/lang/String;")] = cprover_string_of_char_array_func; + string_of_char_array_functions[irep_idt("java::java.lang.String.valueOf:([C)Ljava/lang/String;")] = cprover_string_of_char_array_func; + string_of_char_array_functions[irep_idt("java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;")] = cprover_string_of_char_array_func; + string_of_char_array_functions[irep_idt("java::java.lang.String.copyValueOf:([C)Ljava/lang/String;")] = cprover_string_of_char_array_func; + + Forall_goto_functions(it, goto_functions) + replace_string_calls(it); + } + + diff --git a/src/goto-programs/pass_preprocess.h b/src/goto-programs/pass_preprocess.h new file mode 100644 index 00000000000..5812c05a3eb --- /dev/null +++ b/src/goto-programs/pass_preprocess.h @@ -0,0 +1,87 @@ +/*******************************************************************\ + +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 +#include + +class pass_preprocesst:public messaget +{ + private: + namespacet ns; + symbol_tablet & symbol_table; + goto_functionst & goto_functions; + std::map string_builders; + std::map side_effect_functions; + std::map string_functions; + std::map string_function_calls; + std::map string_of_char_array_functions; + std::map string_of_char_array_function_calls; + std::map side_effect_char_array_functions; + + public: + pass_preprocesst(symbol_tablet &, goto_functionst &, message_handlert &); + + private: + + // add a temporary symbol to the symbol table + symbol_exprt new_tmp_symbol(const std::string &name, const typet &type); + + void declare_function(irep_idt function_name, const typet &type); + + exprt replace_string_literals(const exprt & ); + + // replace "lhs=s.some_function(x,...)" by "lhs=function_name(s,x,...)" + void make_string_function + (goto_programt::instructionst::iterator & i_it, irep_idt function_name); + + // replace "s.some_function(x,...)" by "s=function_name(x,...)" + void make_string_function_call + (goto_programt::instructionst::iterator & i_it, irep_idt function_name); + + // replace "r = s.some_function(x,...)" by "s=function_name(s,x,...)" + // and add a correspondance from r to s in the string_builders map + void make_string_function_side_effect + (goto_programt::instructionst::iterator & i_it, irep_idt function_name); + + // replace "return_tmp0 = s.toCharArray()" with: + // tmp_assign = MALLOC(struct java::array[reference], 17L); + // tmp_assign->length = (int)__CPROVER_uninterpreted_string_length_func(s); + // tmp_assign->data = new (void **)[tmp_assign->length]; + // tmp_nil = __CPROVER_uninterpreted_string_data_func(s, tmp_assign->data); + // return_tmp0 = tmp_assign; + void make_to_char_array_function + (goto_programt & goto_program, goto_programt::instructionst::iterator &); + + // replace "r.some_function(arr,...)" by + // "r = function_name(arr.length,arr.data,...); + void make_of_char_array_function_call + (goto_programt::instructionst::iterator & i_it, irep_idt function_name); + + // replace "r = some_function(arr,...)" by + // "r = function_name(arr.length,arr.data,...); + void make_of_char_array_function + (goto_programt::instructionst::iterator & i_it, irep_idt function_name); + + // replace "r = s.some_function(i,arr,...)" by "s=function_name(s,i,arr.length,arr.data)" + // and add a correspondance from r to s in the string_builders map + void make_of_char_array_side_effect + (goto_programt::instructionst::iterator & i_it, irep_idt function_name); + + bool has_java_string_type(const exprt &expr); + + void replace_string_calls(goto_functionst::function_mapt::iterator f_it); + +}; + +#endif diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 4a1320d4731..d9ffe06e011 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -73,6 +73,14 @@ void remove_returnst::replace_returns( symbol_tablet::symbolst::iterator s_it= symbol_table.symbols.find(function_id); + if(s_it==symbol_table.symbols.end()) + { + std::string str = "function symbol for "; + str += function_id.c_str(); + str += " not found"; + throw str; + } + assert(s_it!=symbol_table.symbols.end()); symbolt &function_symbol=s_it->second; diff --git a/src/solvers/Makefile b/src/solvers/Makefile index b806aa47886..aadf2307495 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -118,6 +118,12 @@ 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 \ + refinement/string_constraint_generator.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/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp index d0c5ac524ed..ab97180718b 100644 --- a/src/solvers/flattening/boolbv_with.cpp +++ b/src/solvers/flattening/boolbv_with.cpp @@ -287,6 +287,9 @@ void boolbvt::convert_with_struct( if(!base_type_eq(subtype, op2.type(), ns)) { error().source_location=type.source_location(); + error() << "solvers/flattening/boolbv_with.cpp:" << eom; + error() << "expected gobal type = " << type.pretty() << eom; + error() << "op2 = " << op2.pretty() << eom; error() << "with/struct: component `" << component_name << "' type does not match: " << subtype.pretty() << " vs. " 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..dbba21d805c --- /dev/null +++ b/src/solvers/refinement/string_constraint.cpp @@ -0,0 +1,77 @@ +/** -*- 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::forall(const symbol_exprt & univ, const exprt & bound_sup) +{ + return forall(univ,refined_string_typet::index_zero(),bound_sup); +} + +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)))); +} + +string_constraintt string_constraintt::exists(const symbol_exprt & univ, const exprt & bound_sup) +{ + return exists(univ,refined_string_typet::index_zero(),bound_sup); +} diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h new file mode 100644 index 00000000000..49bc79335ae --- /dev/null +++ b/src/solvers/refinement/string_constraint.h @@ -0,0 +1,115 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String constraints + (see the PASS paper at HVC'13 and chapter 7 on arrays of ???) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_SOLVER_STRING_CONSTRAINT_H +#define CPROVER_SOLVER_STRING_CONSTRAINT_H + +#include +#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; + + // we should change the structure of the class to adopt the notations of chapter 7 + // exprt index_guard; + +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); + // Default bound inferior is 0 + string_constraintt forall(const symbol_exprt & univ, 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); + // Default bound inferior is 0 + string_constraintt exists(const symbol_exprt & exist, 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_constraint_generator.cpp b/src/solvers/refinement/string_constraint_generator.cpp new file mode 100644 index 00000000000..d5e919cafed --- /dev/null +++ b/src/solvers/refinement/string_constraint_generator.cpp @@ -0,0 +1,1840 @@ +/** -*- C++ -*- *****************************************************\ + +Module: Constraint generation from string function calls + for the PASS algorithm (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include + +constant_exprt string_constraint_generatort::constant_char(int i) +{ + switch(language) + { + case C : + return constant_exprt(integer2binary(i,STRING_SOLVER_CHAR_WIDTH),refined_string_typet::char_type()); + break; + case JAVA : return constant_exprt(integer2binary(i,JAVA_STRING_SOLVER_CHAR_WIDTH),refined_string_typet::java_char_type()); + break; + default: assert(false); + } +} + + +constant_exprt string_constraint_generatort::constant_unsigned(int i, size_t width) +{ return constant_exprt(integer2binary(i,width),unsignedbv_typet(width)); } + +constant_exprt string_constraint_generatort::constant_signed(int i, size_t width) +{ return constant_exprt(integer2binary(i,width),signedbv_typet(width)); } + +void string_constraint_generatort::check_char_type(const exprt & str) +{ + if(language == C) + assert(refined_string_typet::is_c_string_type(str.type())); + else + if(language == UNKNOWN) + { + if(refined_string_typet::is_c_string_type(str.type())) + language = C; + else + language = JAVA; + } + +} + +unsignedbv_typet string_constraint_generatort::get_char_type() +{ + if(language==C) + return refined_string_typet::char_type(); + else if(language==JAVA) return refined_string_typet::java_char_type(); + else assert(false); +} + +size_t string_constraint_generatort::get_char_width() +{ + if(language==C) + return STRING_SOLVER_CHAR_WIDTH; + else if(language==JAVA) return JAVA_STRING_SOLVER_CHAR_WIDTH; + else assert(false); +} + +symbol_exprt string_constraint_generatort::fresh_univ_index(const irep_idt &prefix) +{ + return string_exprt::fresh_symbol(prefix,refined_string_typet::index_type()); +} + +symbol_exprt string_constraint_generatort::fresh_exist_index(const irep_idt &prefix) +{ + symbol_exprt s = string_exprt::fresh_symbol(prefix,refined_string_typet::index_type()); + index_symbols.push_back(s); + return s; +} + +symbol_exprt string_constraint_generatort::fresh_boolean(const irep_idt &prefix) +{ + symbol_exprt b = string_exprt::fresh_symbol(prefix,bool_typet()); + boolean_symbols.push_back(b); + return b; +} + + +string_exprt string_constraint_generatort::string_of_expr(const exprt & unrefined_string) +{ + string_exprt s; + + check_char_type(unrefined_string); + + if(unrefined_string.id() == ID_function_application) + { + exprt res = function_application(to_function_application_expr(unrefined_string)); + assert(res.type() == refined_string_typet(get_char_type())); + s = to_string_expr(res); + } + else if(unrefined_string.id()==ID_symbol) + s = get_string_of_symbol(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(to_symbol_expr(unrefined_string.op0())); + } + else if(unrefined_string.id()==ID_if) + s = string_if(to_if_expr(unrefined_string)); + 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.longer(refined_string_typet::index_zero())); + return s; +} + + + +string_exprt string_constraint_generatort::string_if(const if_exprt &expr) +{ + string_exprt res(get_char_type()); + assert(refined_string_typet::is_unrefined_string_type(expr.true_case().type())); + string_exprt t = string_of_expr(expr.true_case()); + assert(refined_string_typet::is_unrefined_string_type(expr.false_case().type())); + string_exprt f = string_of_expr(expr.false_case()); + + axioms.emplace_back(expr.cond(),res.same_length(t)); + symbol_exprt qvar = fresh_univ_index("QA_string_if_true"); + axioms.push_back(string_constraintt(expr.cond(),equal_exprt(res[qvar],t[qvar]) + ).forall(qvar,t.length())); + + axioms.emplace_back(not_exprt(expr.cond()),res.same_length(f)); + symbol_exprt qvar2 = fresh_univ_index("QA_string_if_false"); + axioms.push_back(string_constraintt(not_exprt(expr.cond()), + equal_exprt(res[qvar2],f[qvar2]) + ).forall(qvar2,f.length())); + return res; +} + + +string_exprt string_constraint_generatort::get_string_of_symbol(const symbol_exprt & sym) +{ + irep_idt id = sym.get_identifier(); + std::map::iterator f = symbol_to_string.find(id); + if(f != symbol_to_string.end()) + return f->second; + + symbol_to_string[id]= string_exprt(get_char_type()); + return symbol_to_string[id]; +} + +string_exprt string_constraint_generatort::string_of_symbol(const symbol_exprt & sym) +{ return get_string_of_symbol(sym); } + + +exprt string_constraint_generatort::function_application +(const function_application_exprt & expr) +{ + const exprt &name = expr.function(); + assert(name.id() == ID_symbol); + + const irep_idt &id = to_symbol_expr(name).get_identifier(); + if (starts_with(id,cprover_char_literal_func)) + return char_literal(expr); + else if (starts_with(id,cprover_string_length_func)) + return string_length(expr); + else if (starts_with(id,cprover_string_equal_func)) + return string_equal(expr); + else if (starts_with(id,cprover_string_equals_ignore_case_func)) + return string_equals_ignore_case(expr); + else if (starts_with(id,cprover_string_is_empty_func)) + return string_is_empty(expr); + else if (starts_with(id,cprover_string_char_at_func)) + return string_char_at(expr); + else if (starts_with(id,cprover_string_is_prefix_func)) + return string_is_prefix(expr); + else if (starts_with(id,cprover_string_is_suffix_func)) + return string_is_suffix(expr); + else if (starts_with(id,cprover_string_startswith_func)) + return string_is_prefix(expr,true); + else if (starts_with(id,cprover_string_endswith_func)) + return string_is_suffix(expr,true); + else if (starts_with(id,cprover_string_contains_func)) + return string_contains(expr); + else if (starts_with(id,cprover_string_hash_code_func)) + return string_hash_code(expr); + else if (starts_with(id,cprover_string_index_of_func)) + return string_index_of(expr); + else if (starts_with(id,cprover_string_last_index_of_func)) + return string_last_index_of(expr); + else if (starts_with(id,cprover_string_parse_int_func)) + return string_parse_int(expr); + else if (starts_with(id,cprover_string_to_char_array_func)) + return string_to_char_array(expr); + else if (starts_with(id,cprover_string_code_point_at_func)) + return string_code_point_at(expr); + else if (starts_with(id,cprover_string_code_point_before_func)) + return string_code_point_before(expr); + else if (starts_with(id,cprover_string_code_point_count_func)) + return string_code_point_count(expr); + else if (starts_with(id,cprover_string_offset_by_code_point_func)) + return string_offset_by_code_point(expr); + else if (starts_with(id,cprover_string_compare_to_func)) + return string_compare_to(expr); + else if(starts_with(id,cprover_string_literal_func)) + return string_literal(expr); + else if(starts_with(id,cprover_string_concat_func)) + return string_concat(expr); + else if(starts_with(id,cprover_string_concat_int_func)) + return string_concat_int(expr); + else if(starts_with(id,cprover_string_concat_long_func)) + return string_concat_long(expr); + else if(starts_with(id,cprover_string_concat_bool_func)) + return string_concat_bool(expr); + else if(starts_with(id,cprover_string_concat_char_func)) + return string_concat_char(expr); + else if(starts_with(id,cprover_string_concat_double_func)) + return string_concat_double(expr); + else if(starts_with(id,cprover_string_concat_float_func)) + return string_concat_float(expr); + else if(starts_with(id,cprover_string_concat_code_point_func)) + return string_concat_code_point(expr); + else if(starts_with(id,cprover_string_insert_func)) + return string_insert(expr); + else if(starts_with(id,cprover_string_insert_int_func)) + return string_insert_int(expr); + else if(starts_with(id,cprover_string_insert_long_func)) + return string_insert_long(expr); + else if(starts_with(id,cprover_string_insert_bool_func)) + return string_insert_bool(expr); + else if(starts_with(id,cprover_string_insert_char_func)) + return string_insert_char(expr); + else if(starts_with(id,cprover_string_insert_double_func)) + return string_insert_double(expr); + else if(starts_with(id,cprover_string_insert_float_func)) + return string_insert_float(expr); + else if(starts_with(id,cprover_string_insert_char_array_func)) + return string_insert_char_array(expr); + else if(starts_with(id,cprover_string_substring_func)) + return string_substring(expr); + else if(starts_with(id,cprover_string_trim_func)) + return string_trim(expr); + else if(starts_with(id,cprover_string_to_lower_case_func)) + return string_to_lower_case(expr); + else if(starts_with(id,cprover_string_to_upper_case_func)) + return string_to_upper_case(expr); + else if(starts_with(id,cprover_string_char_set_func)) + return string_char_set(expr); + else if(starts_with(id,cprover_string_value_of_func)) + return string_value_of(expr); + else if(starts_with(id,cprover_string_empty_string_func)) + return empty_string(expr); + else if(starts_with(id,cprover_string_copy_func)) + return string_copy(expr); + else if(starts_with(id,cprover_string_of_int_func)) + return of_int(expr); + else if(starts_with(id,cprover_string_of_int_hex_func)) + return of_int_hex(expr); + else if(starts_with(id,cprover_string_of_float_func)) + return of_float(expr); + else if(starts_with(id,cprover_string_of_double_func)) + return of_double(expr); + else if(starts_with(id,cprover_string_of_long_func)) + return of_long(expr); + else if(starts_with(id,cprover_string_of_bool_func)) + return of_bool(expr); + else if(starts_with(id,cprover_string_of_char_func)) + return of_char(expr); + else if(starts_with(id,cprover_string_of_char_array_func)) + return of_char_array(expr); + else if(starts_with(id,cprover_string_set_length_func)) + return string_set_length(expr); + else if(starts_with(id,cprover_string_delete_func)) + return string_delete(expr); + else if(starts_with(id,cprover_string_delete_char_at_func)) + return string_delete_char_at(expr); + else if(starts_with(id,cprover_string_replace_func)) + return string_replace(expr); + else if(starts_with(id,cprover_string_data_func)) + return string_data(expr); + else + { + std::string msg("string_exprt::function_application: unknown symbol :"); + msg+=id.c_str(); + throw msg; + } +} + + +irep_idt 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); +} + +string_exprt string_constraint_generatort::string_constant(irep_idt sval, int char_width, unsignedbv_typet char_type){ + + string_exprt res(char_type); + std::string str = sval.c_str(); + // should only do this for java + std::wstring utf16 = utf8_to_utf16le(str); + + 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()); + std::string sval_binary=integer2binary((unsigned)utf16[i], char_width); + constant_exprt c(sval_binary,char_type); + equal_exprt lemma(res[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(res.has_length(s_length)); + return res; +} + +string_exprt string_constraint_generatort::empty_string(const function_application_exprt &f) +{ + assert(f.arguments().size() == 0); + string_exprt res(get_char_type()); + axioms.emplace_back(res.has_length(0)); + return res; +} + +string_exprt string_constraint_generatort::string_literal(const function_application_exprt &f) +{ + 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(); + } + + return string_constant(sval,char_width,char_type); +} + + +string_exprt string_constraint_generatort::string_concat(const string_exprt & s1, const string_exprt & s2) +{ + // |res| = |s1| + |s2| + string_exprt res(get_char_type()); + axioms.emplace_back(res.has_length(plus_exprt(s1.length(), s2.length()))); + axioms.emplace_back(s1.shorter(res)); // we have to be careful about very long strings + axioms.emplace_back(s2.shorter(res)); + + // forall i<|s1|. res[i] = s1[i] + symbol_exprt idx = fresh_univ_index("QA_index_concat"); + string_constraintt a1(equal_exprt(s1[idx],res[idx])); + axioms.push_back(a1.forall(idx, s1.length())); + + // forall i<|s2|. res[i+|s1|] = s2[i] + symbol_exprt idx2 = fresh_univ_index("QA_index_concat2"); + string_constraintt a2(equal_exprt(s2[idx2],res[plus_exprt(idx2,s1.length())])); + axioms.push_back(a2.forall(idx2, s2.length())); + + return res; +} + + +string_exprt string_constraint_generatort::string_concat(const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(args.size() == 2); + + string_exprt s1 = string_of_expr(args[0]); + string_exprt s2 = string_of_expr(args[1]); + + return string_concat(s1, s2); +} + + +string_exprt string_constraint_generatort::string_copy(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,1)[0]); + string_exprt res(get_char_type()); + axioms.emplace_back(res.same_length(s1)); + symbol_exprt idx = fresh_univ_index("QA_index_copy"); + string_constraintt a1(equal_exprt(s1[idx],res[idx])); + axioms.push_back(a1.forall(idx, s1.length())); + return res; +} + +string_exprt string_constraint_generatort::string_set_length(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + exprt k = args(f,2)[1]; + string_exprt res(get_char_type()); + + // |s| = k + // && forall i < k. (i < k ==> s[i] = s1[i]) && (i >= k ==> s[i] = 0) + + axioms.emplace_back(res.has_length(k)); + symbol_exprt idx = fresh_univ_index("QA_index_set_length"); + string_constraintt a1 + (and_exprt(implies_exprt(s1.strictly_longer(idx), equal_exprt(s1[idx],res[idx])), + implies_exprt(s1.shorter(idx), equal_exprt(s1[idx],constant_char(0))))); + axioms.push_back(a1.forall(idx, k)); + + return res; +} + + +string_exprt string_constraint_generatort::java_char_array(const exprt & char_array) +{ + string_exprt res(get_char_type()); + exprt arr = to_address_of_expr(char_array).object(); + exprt len = member_exprt(arr, "length", res.length().type()); + exprt cont = member_exprt(arr, "data", res.content().type()); + res.op0() = len; + res.op1() = cont; + return res; +} + + +string_exprt string_constraint_generatort::string_value_of(const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + if(args.size() == 3) + { + string_exprt res(get_char_type()); + exprt char_array = args[0]; + exprt offset = args[1]; + exprt count = args[2]; + string_exprt str = java_char_array(char_array); + axioms.emplace_back(res.has_length(count)); + symbol_exprt idx = fresh_univ_index("QA_index_value_of"); + string_constraintt a1(equal_exprt(str[plus_exprt(idx,offset)],res[idx])); + axioms.push_back(a1.forall(idx, count)); + return res; + } + else + { + assert(args.size() == 1); + return java_char_array(args[0]); + } +} + +string_exprt string_constraint_generatort::string_substring +(const function_application_exprt &f) +{ + assert(f.arguments().size() >= 2); + string_exprt str = string_of_expr(f.arguments()[0]); + exprt i(f.arguments()[1]); + exprt j; + if(f.arguments().size() == 3) j = f.arguments()[2]; + else { assert(f.arguments().size() == 2); j = str.length(); } + return string_substring(str,i,j); +} + +string_exprt string_constraint_generatort::string_substring + (const string_exprt & str, const exprt & start, const exprt & end) +{ + symbol_exprt idx = fresh_exist_index("index_substring"); + assert(start.type() == refined_string_typet::index_type()); + assert(end.type() == refined_string_typet::index_type()); + string_exprt res(get_char_type()); + + axioms.emplace_back(binary_relation_exprt(start, ID_lt, end),res.has_length(minus_exprt(end, start))); + axioms.emplace_back(binary_relation_exprt(start, ID_ge, end),res.has_length(refined_string_typet::index_zero())); + // Warning: check what to do if the string is not long enough + axioms.emplace_back(str.longer(end)); + + // forall idx < str.length, str[idx] = arg_str[idx+i] + string_constraintt a(equal_exprt(res[idx], str[plus_exprt(start, idx)])); + axioms.push_back(a.forall(idx,res.length())); + return res; +} + +string_exprt string_constraint_generatort::string_trim +(const function_application_exprt &expr) +{ + string_exprt str = string_of_expr(args(expr,1)[0]); + string_exprt res(get_char_type()); + symbol_exprt idx = fresh_exist_index("index_trim"); + exprt space_char = constant_char(32); + + // m + |s1| <= |str| + axioms.emplace_back(str.longer(plus_exprt(idx, res.length()))); + axioms.emplace_back(binary_relation_exprt(idx, ID_ge, refined_string_typet::index_zero())); + axioms.emplace_back(str.longer(idx)); + axioms.emplace_back(res.longer(refined_string_typet::index_zero())); + axioms.emplace_back(res.shorter(str)); // necessary to prevent exceeding the biggest integer + + symbol_exprt n = fresh_univ_index("QA_index_trim"); + // forall n < m, str[n] = ' ' + string_constraintt a(equal_exprt(str[n], space_char)); + axioms.push_back(a.forall(n,idx)); + + symbol_exprt n2 = fresh_univ_index("QA_index_trim2"); + // forall n < |str|-m-|s1|, str[m+|s1|+n] = ' ' + string_constraintt a1(equal_exprt(str[plus_exprt(idx,plus_exprt(res.length(),n2))], space_char)); + axioms.push_back(a1.forall(n2,minus_exprt(str.length(),plus_exprt(idx,res.length())))); + + symbol_exprt n3 = fresh_univ_index("QA_index_trim3"); + // forall n < |s1|, s[idx+n] = s1[n] + string_constraintt a2(equal_exprt(res[n3], str[plus_exprt(n3, idx)])); + axioms.push_back(a2.forall(n3,res.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,res.length()),refined_string_typet::index_of_int(1))],space_char)))); + axioms.push_back(m_index_condition); + return res; +} + +string_exprt string_constraint_generatort::string_to_lower_case +(const function_application_exprt &expr) +{ + string_exprt str = string_of_expr(args(expr,1)[0]); + string_exprt res(get_char_type()); + exprt char_a = constant_char(97); + exprt char_A = constant_char(65); + exprt char_z = constant_char(122); + exprt char_Z = constant_char(90); + + axioms.emplace_back(res.same_length(str)); + + symbol_exprt idx = fresh_univ_index("QA_lower_case"); + // 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(res[idx],plus_exprt(str[idx],minus_exprt(char_a,char_A))); + equal_exprt eq(res[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,res.length())); + return res; +} + + +string_exprt string_constraint_generatort::string_to_upper_case +(const function_application_exprt &expr) +{ + string_exprt str = string_of_expr(args(expr,1)[0]); + string_exprt res(get_char_type()); + exprt char_a = constant_char(97); + exprt char_A = constant_char(65); + exprt char_z = constant_char(122); + exprt char_Z = constant_char(90); + + axioms.emplace_back(res.same_length(str)); + + symbol_exprt idx = fresh_univ_index("QA_upper_case"); + // 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(res[idx],plus_exprt(str[idx],minus_exprt(char_A,char_a))); + equal_exprt eq(res[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,res.length())); + return res; +} + + +string_exprt string_constraint_generatort::of_int +(const function_application_exprt &expr) +{ return of_int(args(expr,1)[0],10); } + +string_exprt string_constraint_generatort::of_long +(const function_application_exprt &expr) +{ return of_int(args(expr,1)[0],30); } + +string_exprt string_constraint_generatort::of_float +(const function_application_exprt &f) +{ return of_float(args(f,1)[0],false); } + +string_exprt string_constraint_generatort::of_double +(const function_application_exprt &f) +{ return of_float(args(f,1)[0],true); } + +string_exprt string_constraint_generatort::of_float +(const exprt &f, bool double_precision) +{ + // Warning: we currently only have partial specification + unsignedbv_typet char_type = get_char_type(); + size_t char_width = get_char_width(); + + string_exprt res(char_type); + axioms.emplace_back(res.shorter(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 = string_constant("NaN",char_width,char_type); + + 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, magnitude.same_length(nan_string)); + symbol_exprt qvar = fresh_univ_index("QA_equal_nan"); + axioms.push_back + (string_constraintt(isnan,equal_exprt(magnitude[qvar],nan_string[qvar]) + ).forall(qvar,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, sign_string.has_length(1)); + + axioms.emplace_back(not_exprt(isneg), sign_string.has_length(0)); + axioms.emplace_back(isneg,equal_exprt(sign_string[0], constant_char(0x2D))); + + // 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 = string_constant("Infinity",char_width,char_type); + exprt isinf = float_bvt().isinf(f,fspec); + axioms.emplace_back(isinf, magnitude.same_length(infinity_string)); + symbol_exprt qvar_inf = fresh_univ_index("QA_equal_infinity"); + axioms.push_back + (string_constraintt(isinf,equal_exprt(magnitude[qvar_inf],infinity_string[qvar_inf]) + ).forall(qvar_inf,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 = string_constant("0.0",char_width,char_type); + exprt iszero = float_bvt().is_zero(f,fspec); + axioms.emplace_back(iszero, magnitude.same_length(zero_string)); + symbol_exprt qvar_zero = fresh_univ_index("QA_equal_zero"); + axioms.push_back + (string_constraintt(iszero,equal_exprt(magnitude[qvar_zero],zero_string[qvar_zero]) + ).forall(qvar_zero,zero_string.length())); + + return string_concat(sign_string,magnitude); +} + + +string_exprt string_constraint_generatort::of_bool +(const function_application_exprt &f) +{ return of_bool(args(f,1)[0]); } + + +string_exprt string_constraint_generatort::of_bool(const exprt &i) +{ + unsignedbv_typet char_type = get_char_type(); + int char_width = get_char_width(); + string_exprt res(char_type); + + assert(i.type() == bool_typet() || i.type().id() == ID_c_bool); + + typecast_exprt eq(i,bool_typet()); + + string_exprt true_string = string_constant("true",char_width,char_type); + string_exprt false_string = string_constant("false",char_width,char_type); + + axioms.emplace_back(eq, res.same_length(true_string)); + symbol_exprt qvar = fresh_univ_index("QA_equal_true"); + axioms.push_back + (string_constraintt(eq,equal_exprt(res[qvar],true_string[qvar]) + ).forall(qvar,true_string.length())); + + axioms.emplace_back(not_exprt(eq), res.same_length(false_string)); + symbol_exprt qvar1 = fresh_univ_index("QA_equal_false"); + axioms.push_back + (string_constraintt(not_exprt(eq),equal_exprt(res[qvar1],false_string[qvar1]) + ).forall(qvar,false_string.length())); + + return res; +} + + +string_exprt string_constraint_generatort::of_int +(const exprt &i, size_t max_size) +{ + string_exprt res(get_char_type()); + typet type = i.type(); + assert(type.id() == ID_signedbv); + size_t width = to_bitvector_type(type).get_width(); + exprt ten = constant_signed(10,width); + exprt zero_char = constant_char('0'); + exprt nine_char = constant_char('9'); + exprt minus_char = constant_char('-'); + + axioms.emplace_back(and_exprt(res.strictly_longer(refined_string_typet::index_zero()), + res.shorter(refined_string_typet::index_of_int(max_size)))); + + exprt chr = res[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(size_t size=1; size<=max_size;size++) + { + exprt sum = constant_signed(0,width); + exprt all_numbers = true_exprt(); + chr = res[0]; + exprt first_value = typecast_exprt(minus_exprt(chr,zero_char),type); + + for(size_t j=1; j1) + { + axioms.emplace_back(and_exprt(premise,starts_with_digit), + not_exprt(equal_exprt(res[refined_string_typet::index_zero()],zero_char))); + axioms.emplace_back(and_exprt(premise,starts_with_minus), + not_exprt(equal_exprt(res[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_signed(1000000000,width); + axioms.emplace_back(premise,binary_relation_exprt(i,ID_ge,smallest_with_10_digits)); + } + } + return res; +} + + +exprt string_constraint_generatort::int_of_hex_char(exprt chr, unsigned char_width, typet char_type) +{ + exprt zero_char = constant_char(48); + exprt nine_char = constant_char(57); + exprt a_char = constant_char(0x61); + return if_exprt(binary_relation_exprt(chr,ID_gt,nine_char), + minus_exprt(chr,constant_char(0x61 - 10)), + minus_exprt(chr,zero_char)); +} + + +string_exprt string_constraint_generatort::of_int_hex(const exprt &i) +{ + string_exprt res(get_char_type()); + typet type = i.type(); + assert(type.id() == ID_signedbv); + size_t width = to_bitvector_type(type).get_width(); + exprt sixteen = constant_signed(16,width); + exprt minus_char = constant_char(45); + exprt zero_char = constant_char(48); + exprt nine_char = constant_char(57); + exprt a_char = constant_char(0x61); + exprt f_char = constant_char(0x66); + + size_t max_size = 8; + axioms.emplace_back(and_exprt(res.strictly_longer(0), + res.shorter(max_size))); + + for(size_t size=1; size<=max_size;size++) + { + exprt sum = constant_signed(0,width); + exprt all_numbers = true_exprt(); + exprt chr = res[0]; + + for(size_t j=0; j1) + axioms.emplace_back(premise, not_exprt(equal_exprt(res[0],zero_char))); + } + return res; +} + +string_exprt string_constraint_generatort::of_int_hex +(const function_application_exprt &f) +{ return of_int_hex(args(f,1)[0]); } + +string_exprt string_constraint_generatort::of_char +(const function_application_exprt &f) +{ return of_char(args(f,1)[0]); } + +string_exprt string_constraint_generatort::of_char(const exprt &c) +{ + string_exprt res(get_char_type()); + and_exprt lemma(equal_exprt(res[0], c), res.has_length(1)); + axioms.push_back(lemma); + return res; +} + + +string_exprt string_constraint_generatort::code_point(const exprt &code_point) +{ + string_exprt res(get_char_type()); + typet type = code_point.type(); + assert(type.id() == ID_signedbv); + size_t width = to_bitvector_type(type).get_width(); + binary_relation_exprt small(code_point,ID_lt,constant_signed(0x010000,width)); + axioms.emplace_back(small, res.has_length(1)); + axioms.emplace_back(not_exprt(small),res.has_length(2)); + axioms.emplace_back(small,equal_exprt(res[0],typecast_exprt(code_point,get_char_type()))); + + axioms.emplace_back(not_exprt(small), + equal_exprt + (res[0], + typecast_exprt + (plus_exprt(constant_signed(0xD800,width), + div_exprt(minus_exprt(code_point,constant_signed(0x010000,width)),constant_signed(0x0400,width))), + get_char_type()))); + axioms.emplace_back(not_exprt(small), + equal_exprt + (res[1], + typecast_exprt + (plus_exprt(constant_signed(0xDC00,width), + mod_exprt(code_point,constant_signed(0x0400,width))), + get_char_type()))); + return res; +} + + +string_exprt string_constraint_generatort::string_char_set +(const function_application_exprt &f) +{ + string_exprt res(get_char_type()); + string_exprt str = string_of_expr(args(f,3)[0]); + with_exprt sarrnew(str.content(), args(f,3)[1], args(f,3)[2]); + implies_exprt lemma(binary_relation_exprt(args(f,3)[1], ID_lt, str.length()), + and_exprt(equal_exprt(res.content(), sarrnew), + res.same_length(str))); + axioms.push_back(lemma); + return res; +} + +string_exprt string_constraint_generatort::string_replace +(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,3)[0]); + exprt oldChar = args(f,3)[1]; + exprt newChar = args(f,3)[2]; + string_exprt res(get_char_type()); + + axioms.emplace_back(res.same_length(str)); + symbol_exprt qvar = fresh_univ_index("QA_replace"); + axioms.push_back + (string_constraintt + (and_exprt + (implies_exprt(equal_exprt(str[qvar],oldChar),equal_exprt(res[qvar],newChar)), + implies_exprt(not_exprt(equal_exprt(str[qvar],oldChar)), + equal_exprt(res[qvar],str[qvar])) + ) + ).forall(qvar,res.length())); + return res; +} + +string_exprt string_constraint_generatort::string_delete_char_at +(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,2)[0]); + exprt index_one = refined_string_typet::index_of_int(1); + return string_delete(str,args(f,2)[1],plus_exprt(args(f,2)[1],index_one)); +} + +string_exprt string_constraint_generatort::string_delete +(const string_exprt &str, const exprt & start, const exprt & end) +{ + assert(start.type() == refined_string_typet::index_type()); + assert(end.type() == refined_string_typet::index_type()); + string_exprt str1 = string_substring(str,refined_string_typet::index_zero(),start); + string_exprt str2 = string_substring(str,end,str.length()); + return string_concat(str1,str2); +} + +string_exprt string_constraint_generatort::string_delete +(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,3)[0]); + return string_delete(str,args(f,3)[1],args(f,3)[2]); +} + + +string_exprt string_constraint_generatort::string_concat_int +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = of_int(args(f,2)[1],10); + return string_concat(s1,s2); +} + +string_exprt string_constraint_generatort::string_concat_long +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = of_int(args(f,2)[1],30); + return string_concat(s1,s2); +} + +string_exprt string_constraint_generatort::string_concat_bool +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = of_bool(args(f,2)[1]); + return string_concat(s1,s2); +} + +string_exprt string_constraint_generatort::string_concat_char +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = of_char(args(f,2)[1]); + return string_concat(s1,s2); +} + +string_exprt string_constraint_generatort::string_concat_double +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = of_float(args(f,2)[1],30); + return string_concat(s1,s2); +} + +string_exprt string_constraint_generatort::string_concat_float +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = of_float(args(f,2)[1],10); + return string_concat(s1,s2); +} + +string_exprt string_constraint_generatort::string_concat_code_point +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = code_point(args(f,2)[1]); + return string_concat(s1,s2); +} + +string_exprt string_constraint_generatort::string_insert +(const string_exprt & s1, const string_exprt & s2, const exprt & offset) +{ + assert(offset.type() == refined_string_typet::index_type()); + string_exprt pref = string_substring(s1,refined_string_typet::index_zero(),offset); + string_exprt suf = string_substring(s1,offset,s1.length()); + string_exprt concat1 = string_concat(pref,s2); + return string_concat(concat1,suf); +} + +string_exprt string_constraint_generatort::string_insert +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,3)[0]); + string_exprt s2 = string_of_expr(args(f,3)[2]); + return string_insert(s1, s2, args(f,3)[1]); +} + +string_exprt string_constraint_generatort::string_insert_int +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,3)[0]); + string_exprt s2 = of_int(args(f,3)[2],10); + return string_insert(s1,s2,args(f,3)[1]); +} + +string_exprt string_constraint_generatort::string_insert_long +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,3)[0]); + string_exprt s2 = of_int(args(f,3)[2],30); + return string_insert(s1,s2,args(f,3)[1]); +} + +string_exprt string_constraint_generatort::string_insert_bool +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,3)[0]); + string_exprt s2 = of_bool(args(f,3)[2]); + return string_insert(s1,s2,args(f,3)[1]); +} + +string_exprt string_constraint_generatort::string_insert_char +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,3)[0]); + string_exprt s2 = of_char(args(f,3)[2]); + return string_insert(s1,s2,args(f,3)[1]); +} + +string_exprt string_constraint_generatort::string_insert_double +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,3)[0]); + string_exprt s2 = of_float(args(f,3)[2]); + return string_insert(s1,s2,args(f,3)[1]); +} + +string_exprt string_constraint_generatort::string_insert_float +(const function_application_exprt &f) +{ + string_exprt s1 = string_of_expr(args(f,3)[0]); + string_exprt s2 = of_float(args(f,3)[2]); + return string_insert(s1,s2,args(f,3)[1]); +} + + +exprt string_constraint_generatort::string_equal +(const function_application_exprt &f) + { + assert(f.type() == bool_typet() || f.type().id() == ID_c_bool); + symbol_exprt eq = fresh_boolean("equal"); + typecast_exprt tc_eq(eq,f.type()); + + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = string_of_expr(args(f,2)[1]); + + // We want to write: + // eq <=> (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_exist_index("witness_unequal"); + symbol_exprt qvar = fresh_univ_index("QA_equal"); + + axioms.emplace_back(eq, s1.same_length(s2)); + axioms.push_back + (string_constraintt(eq,equal_exprt(s1[qvar],s2[qvar]) + ).forall(qvar,s1.length())); + + axioms.emplace_back + (not_exprt(eq), + or_exprt(notequal_exprt(s1.length(), s2.length()), + string_constraintt(notequal_exprt(s1[witness],s2[witness])).exists(witness,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_constraint_generatort::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()); + + check_char_type(f); // is this necessary? + + exprt char_a = constant_char(97); + exprt char_A = constant_char(65); + exprt char_Z = constant_char(90); + string_exprt s1 = string_of_expr(args(f,2)[0]); + string_exprt s2 = string_of_expr(args(f,2)[1]); + symbol_exprt witness = fresh_exist_index("witness_unequal_ignore_case"); + symbol_exprt qvar = fresh_univ_index("QA_equal_ignore_case"); + + axioms.emplace_back(eq, s1.same_length(s2)); + + axioms.push_back + (string_constraintt(eq,character_equals_ignore_case(s1[qvar],s2[qvar],char_a,char_A,char_Z) + ).forall(qvar,s1.length())); + + 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,s1.length()))); + + return tc_eq; +} + + +exprt string_constraint_generatort::string_length +(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,1)[0]); + return str.length(); +} + +exprt string_constraint_generatort::string_data +(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,3)[0]); + exprt tab_data = args(f,3)[1]; + exprt data = args(f,3)[2]; + symbol_exprt qvar = fresh_univ_index("QA_string_data"); + // translating data[qvar] to the correct expression + // which is (signed int)byte_extract_little_endian(data, (2l*qvar) + POINTER_OFFSET(byte_extract_little_endian(tab.data, 0l, unsigned short int *)), unsigned short int) + exprt char_in_tab = typecast_exprt + (byte_extract_exprt(ID_byte_extract_little_endian,data, + plus_exprt + (mult_exprt(constant_signed(2,64),typecast_exprt(qvar,signedbv_typet(64))), + pointer_offset(byte_extract_exprt + (ID_byte_extract_little_endian, + tab_data + ,constant_signed(0,64),pointer_typet(unsignedbv_typet(16))))),unsignedbv_typet(16)), + get_char_type()); + + string_constraintt eq(equal_exprt(str[qvar],char_in_tab)); + axioms.push_back(eq.forall(qvar,str.length())); + + exprt void_expr; + void_expr.type() = void_typet(); + return void_expr; +} + +string_exprt string_constraint_generatort::of_char_array +(const exprt & length, const exprt & data, const exprt & offset, const exprt & count) +{ + string_exprt str(get_char_type()); + symbol_exprt qvar = fresh_univ_index("QA_string_of_char_array"); + exprt char_in_tab = data; + assert(char_in_tab.id() == ID_index); + char_in_tab.op1() = plus_exprt(qvar,offset); + + string_constraintt eq(equal_exprt(str[qvar],char_in_tab)); + axioms.push_back(eq.forall(qvar,count)); + axioms.emplace_back(equal_exprt(str.length(),count)); + + return str; +} + +string_exprt string_constraint_generatort::of_char_array +(const function_application_exprt &f) +{ + exprt offset; + exprt count; + if(f.arguments().size() == 4) + { + offset = f.arguments()[2]; + count = f.arguments()[3]; + } + else + { + assert(f.arguments().size() == 2); + count = f.arguments()[0]; + offset = constant_signed(0,32); + } + exprt tab_length = f.arguments()[0]; + exprt data = f.arguments()[1]; + return of_char_array(tab_length,data,offset,count); +} + +string_exprt string_constraint_generatort::string_insert_char_array +(const function_application_exprt &f) +{ + exprt offset; + exprt count; + if(f.arguments().size() == 6) + { + offset = f.arguments()[4]; + count = f.arguments()[5]; + } + else + { + assert(f.arguments().size() == 4); + count = f.arguments()[2]; + offset = constant_signed(0,32); + } + + string_exprt str = string_of_expr(f.arguments()[0]); + exprt length = f.arguments()[2]; + exprt data = f.arguments()[3]; + string_exprt arr = of_char_array(length,data,offset,count); + return string_insert(str,arr,f.arguments()[1]); +} + + + +exprt is_positive(const exprt & x) +{ return binary_relation_exprt(x, ID_ge, refined_string_typet::index_of_int(0)); } + + +exprt string_constraint_generatort::string_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt & offset) +{ + symbol_exprt isprefix = fresh_boolean("isprefix"); + axioms.emplace_back(isprefix, str.longer(plus_exprt(prefix.length(),offset))); + + // forall 0 <= witness < prefix.length. isprefix => s0[witness+offset] = s2[witness] + symbol_exprt qvar = fresh_univ_index("QA_isprefix"); + axioms.push_back + (string_constraintt(isprefix, equal_exprt(str[plus_exprt(qvar,offset)],prefix[qvar]) + ).forall(qvar,prefix.length())); + + symbol_exprt witness = fresh_exist_index("witness_not_isprefix"); + + or_exprt s0_notpref_s1(not_exprt(str.longer(plus_exprt(prefix.length(),offset))), + and_exprt + (str.longer(plus_exprt(prefix.length(),offset)), + and_exprt(is_positive(witness), + and_exprt(prefix.strictly_longer(witness), + notequal_exprt(str[plus_exprt(witness,offset)],prefix[witness]))))); + + axioms.emplace_back(implies_exprt(not_exprt(isprefix),s0_notpref_s1)); + return isprefix; +} + +exprt string_constraint_generatort::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 = string_of_expr(args[swap_arguments?1:0]); + string_exprt s1 = string_of_expr(args[swap_arguments?0:1]); + exprt offset; + if(args.size() == 2) offset = refined_string_typet::index_zero(); + else if (args.size() == 3) offset = args[2]; + return typecast_exprt(string_is_prefix(s0,s1,offset),f.type()); +} + +exprt string_constraint_generatort::string_is_empty +(const function_application_exprt &f) +{ + assert(f.type() == bool_typet() || f.type().id() == ID_c_bool); + symbol_exprt is_empty = fresh_boolean("is_empty"); + string_exprt s0 = string_of_expr(args(f,1)[0]); + axioms.emplace_back(implies_exprt(is_empty, s0.has_length(0))); + axioms.emplace_back(implies_exprt(s0.has_length(0),is_empty)); + return typecast_exprt(is_empty,f.type()); + +} + +exprt string_constraint_generatort::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 = string_of_expr(args[swap_arguments?1:0]); + string_exprt s1 = string_of_expr(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] + + axioms.emplace_back(implies_exprt(issuffix, s1.longer(s0))); + + symbol_exprt qvar = fresh_univ_index("QA_suffix"); + exprt qvar_shifted = plus_exprt(qvar, + minus_exprt(s1.length(), s0.length())); + axioms.push_back + (string_constraintt(issuffix, equal_exprt(s0[qvar],s1[qvar_shifted]) + ).forall(qvar,s0.length())); + + symbol_exprt witness = fresh_exist_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.strictly_longer(s1), + and_exprt(s0.strictly_longer(witness), + notequal_exprt(s0[witness],s1[shifted]))))); + + axioms.emplace_back(lemma2); + + return tc_issuffix; +} + + +exprt string_constraint_generatort::string_contains +( const function_application_exprt &f) +{ + 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 = string_of_expr(args(f,2)[0]); + string_exprt s1 = string_of_expr(args(f,2)[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] + + axioms.emplace_back(implies_exprt(contains, s0.longer(s1))); + symbol_exprt startpos = fresh_exist_index("startpos_contains"); + axioms.emplace_back( + and_exprt(is_positive(startpos),binary_relation_exprt(startpos, ID_le, minus_exprt(s0.length(),s1.length())))); + + symbol_exprt qvar = fresh_univ_index("QA_contains"); + exprt qvar_shifted = plus_exprt(qvar, startpos); + axioms.push_back + (string_constraintt(contains,equal_exprt(s1[qvar],s0[qvar_shifted]) + ).forall(qvar,s1.length())); + + // We rewrite the axiom for !contains as: + // forall startpos <= |s0| - |s1|. (!contains && |s0| >= |s1| ) + // ==> exists witness < |s1|. s1[witness] != s0[startpos+witness] + axioms.push_back + (string_constraintt::not_contains + (refined_string_typet::index_zero(),plus_exprt(refined_string_typet::index_of_int(1),minus_exprt(s0.length(),s1.length())), + and_exprt(not_exprt(contains),s0.longer(s1)),refined_string_typet::index_zero(),s1.length(),s0,s1)); + + return tc_contains; +} + + +exprt string_constraint_generatort::string_hash_code(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,1)[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 = fresh_exist_index("index_hash"); + 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.strictly_longer(i),is_positive(i)) + ))))); + } + return hash[str]; +} + +exprt string_constraint_generatort::string_index_of +(const string_exprt &str, const exprt & c, const exprt & from_index) +{ + symbol_exprt index = fresh_exist_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 + + 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())); + axioms.emplace_back(not_exprt(contains),equal_exprt(index,refined_string_typet::index_of_int(-1))); + axioms.emplace_back(contains,and_exprt(binary_relation_exprt(from_index,ID_le,index),equal_exprt(str[index],c))); + + symbol_exprt n = fresh_univ_index("QA_index_of"); + axioms.push_back(string_constraintt + (contains,not_exprt(equal_exprt(str[n],c))).forall(n,from_index,index)); + + symbol_exprt m = fresh_univ_index("QA_index_of"); + + 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_constraint_generatort::string_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index) +{ + symbol_exprt offset = fresh_exist_index("index_of"); + symbol_exprt contains = fresh_boolean("contains_substring"); + axioms.emplace_back(contains, and_exprt + (str.longer(plus_exprt(substring.length(),offset)), + binary_relation_exprt(offset,ID_ge,from_index))); + 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 = fresh_univ_index("QA_index_of_string"); + axioms.push_back + (string_constraintt(contains, equal_exprt(str[plus_exprt(qvar,offset)],substring[qvar]) + ).forall(qvar,substring.length())); + + return offset; +} + +exprt string_constraint_generatort::string_last_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index) +{ + symbol_exprt offset = fresh_exist_index("index_of"); + symbol_exprt contains = fresh_boolean("contains_substring"); + axioms.emplace_back(contains, and_exprt + (str.longer(plus_exprt(substring.length(),offset)), + binary_relation_exprt(offset,ID_le,from_index))); + 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 = fresh_univ_index("QA_index_of_string"); + axioms.push_back + (string_constraintt(contains, equal_exprt(str[plus_exprt(qvar,offset)],substring[qvar]) + ).forall(qvar,substring.length())); + + return offset; +} + + +exprt string_constraint_generatort::string_index_of +( const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(f.type() == refined_string_typet::index_type()); + string_exprt str = string_of_expr(args[0]); + exprt c = args[1]; + exprt from_index; + + if(args.size() == 2) from_index = refined_string_typet::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 = string_of_expr(c); + return string_index_of_string(str,sub,from_index); + } + else + return string_index_of(str,typecast_exprt(c,get_char_type()),from_index); +} + +exprt string_constraint_generatort::string_last_index_of +(const string_exprt &str, const exprt & c, const exprt & from_index) +{ + symbol_exprt index = fresh_exist_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)); + 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)); + axioms.emplace_back(not_exprt(contains),equal_exprt(index,refined_string_typet::index_of_int(-1))); + axioms.emplace_back(contains,and_exprt(is_positive(index),and_exprt(binary_relation_exprt(from_index,ID_ge,index),equal_exprt(str[index],c)))); + + symbol_exprt n = fresh_univ_index("QA_last_index_of"); + 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 = fresh_univ_index("QA_last_index_of"); + axioms.push_back(string_constraintt(not_exprt(contains),not_exprt(equal_exprt(str[m],c))).forall(m,from_index_plus_one)); + + return index; +} + +exprt string_constraint_generatort::string_last_index_of +( const function_application_exprt &f) +{ + const function_application_exprt::argumentst &args = f.arguments(); + assert(f.type() == refined_string_typet::index_type()); + string_exprt str = string_of_expr(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 = string_of_expr(c); + return string_last_index_of_string(str,sub,from_index); + } + else + return string_last_index_of(str,typecast_exprt(c,get_char_type()),from_index); +} + +exprt string_constraint_generatort::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 constant_exprt(binary, get_char_type()); + } + else + { + throw "convert_char_literal unimplemented"; + } + +} + + +exprt string_constraint_generatort::string_char_at +( const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,2)[0]); + symbol_exprt char_sym = string_exprt::fresh_symbol("char",get_char_type()); + axioms.emplace_back(equal_exprt(char_sym,str[args(f,2)[1]])); + return char_sym; +} + +exprt string_constraint_generatort::string_parse_int +(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,1)[0]); + typet type = f.type(); + symbol_exprt i = string_exprt::fresh_symbol("parsed_int",type); + + exprt zero_char = constant_char(48); + exprt minus_char = constant_char(45); + exprt plus_char = constant_char(43); + assert(type.id() == ID_signedbv); + size_t width = to_bitvector_type(type).get_width(); + constant_exprt ten(integer2binary(10,width),type); + + exprt chr = str[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(unsigned size=1; size<=10;size++) + { + exprt sum = constant_exprt(integer2binary(0,width),type); + exprt first_value = typecast_exprt(minus_exprt(chr,zero_char),type); + + for(unsigned j=1; j |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] + + assert(return_type.id() == ID_signedbv); + size_t width = to_bitvector_type(return_type).get_width(); + + symbol_exprt i = fresh_univ_index("QA_compare_to"); + equal_exprt res_null = equal_exprt(res,constant_signed(0,width)); + axioms.emplace_back(res_null, s1.same_length(s2)); + axioms.push_back(string_constraintt + (res_null,equal_exprt(s1[i],s2[i])).forall(i,s1.length())); + + symbol_exprt x = fresh_exist_index("index_compare_to"); + axioms.push_back + (implies_exprt + (not_exprt(res_null), + and_exprt + (binary_relation_exprt(x,ID_ge,constant_signed(0,width)), + or_exprt + (and_exprt + (equal_exprt(res,typecast_exprt(minus_exprt(s1[x],s2[x]),return_type)), + or_exprt + (and_exprt(s1.shorter(s2),s1.strictly_longer(x)), + and_exprt(s1.longer(s2),s2.strictly_longer(x)))), + and_exprt + (equal_exprt(res,typecast_exprt(minus_exprt(s1.length(),s2.length()), + return_type)), + or_exprt + (and_exprt(s2.strictly_longer(s1),s1.has_length(x)), + and_exprt(s1.strictly_longer(s2),s2.has_length(x)))))))); + + axioms.push_back(string_constraintt + (not_exprt(res_null),equal_exprt(s1[i],s2[i])).forall(i,x)); + + return res; +} + +symbol_exprt string_constraint_generatort::string_intern(const function_application_exprt &f) +{ + string_exprt str = string_of_expr(args(f,1)[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))); + + 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 = fresh_exist_index("index_intern"); + axioms.emplace_back + (or_exprt + (equal_exprt(pool[it->second],pool[str]), + or_exprt + (not_exprt(str.same_length(it->second)), + and_exprt(str.same_length(it->second), + and_exprt(not_exprt(equal_exprt(str[i],it->second[i])), + and_exprt(str.strictly_longer(i),is_positive(i) + )))))); + } + + + return pool[str]; +} + + +void string_constraint_generatort::string_of_expr(const symbol_exprt & sym, const exprt & str) +{ + if(str.id()==ID_symbol) + assign_to_symbol(sym,string_of_symbol(to_symbol_expr(str))); + else + assign_to_symbol(sym,string_of_expr(str)); +} + diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h new file mode 100644 index 00000000000..cb42863f2dc --- /dev/null +++ b/src/solvers/refinement/string_constraint_generator.h @@ -0,0 +1,196 @@ +/** -*- C++ -*- *****************************************************\ + +Module: Constraint generation from string function calls + for the PASS algorithm (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_SOLVER_STRING_CONSTRAINT_GENERATOR_H +#define CPROVER_SOLVER_STRING_CONSTRAINT_GENERATOR_H + +#include + +class string_constraint_generatort { +public: + + string_constraint_generatort() : language(UNKNOWN){ } + + constant_exprt constant_char(int i); + constant_exprt constant_unsigned(int i,size_t width); + constant_exprt constant_signed(int i,size_t width); + unsignedbv_typet get_char_type(); + size_t get_char_width(); + inline signedbv_typet get_index_type() {return refined_string_typet::index_type();}; + + std::vector axioms; + + // 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); + + + // 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; + + symbol_exprt fresh_exist_index(const irep_idt &prefix); + symbol_exprt fresh_univ_index(const irep_idt &prefix); + symbol_exprt fresh_boolean(const irep_idt &prefix); + + 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; } + + + // 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 + string_exprt get_string_of_symbol(const symbol_exprt & sym); + + // Add to the list of axioms, lemmas which should hold for the string to be + // equal to the given expression. + string_exprt of_expr(const exprt & unrefined_string); + + string_exprt string_of_expr(const exprt & expr); + void string_of_expr(const symbol_exprt & sym, const exprt & str); + string_exprt string_of_symbol(const symbol_exprt & sym); + + // The following functions convert different string functions + // and add the corresponding lemmas to a list of properties to be checked + exprt function_application(const function_application_exprt &expr); + + string_exprt empty_string(const function_application_exprt &f); + string_exprt string_char_set(const function_application_exprt &expr); + exprt string_char_at(const function_application_exprt &f); + exprt string_code_point_at(const function_application_exprt &f); + exprt string_code_point_before(const function_application_exprt &f); + string_exprt string_copy(const function_application_exprt &f); + string_exprt string_concat(const string_exprt & s1, const string_exprt & s2); + string_exprt string_concat(const function_application_exprt &f); + string_exprt string_concat_int(const function_application_exprt &f); + string_exprt string_concat_long(const function_application_exprt &f); + string_exprt string_concat_bool(const function_application_exprt &f); + string_exprt string_concat_char(const function_application_exprt &f); + string_exprt string_concat_double(const function_application_exprt &f); + string_exprt string_concat_float(const function_application_exprt &f); + string_exprt string_concat_code_point(const function_application_exprt &f); + string_exprt string_constant(irep_idt sval, int char_width, unsignedbv_typet char_type); + exprt string_contains(const function_application_exprt &f); + exprt string_equal(const function_application_exprt &f); + exprt string_equals_ignore_case(const function_application_exprt &f); + exprt string_data(const function_application_exprt &f); + string_exprt string_delete (const string_exprt &str, const exprt & start, const exprt & end); + string_exprt string_delete(const function_application_exprt &expr); + string_exprt string_delete_char_at(const function_application_exprt &expr); + exprt string_hash_code(const function_application_exprt &f); + + // Warning: the specifications are only partial for some of the "index_of" functions + exprt string_index_of(const string_exprt &str, const exprt & c, const exprt & from_index); + exprt string_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index); + exprt string_index_of(const function_application_exprt &f); + exprt string_last_index_of_string(const string_exprt &str, const string_exprt & substring, const exprt & from_index); + exprt string_last_index_of(const string_exprt &str, const exprt & c, const exprt & from_index); + exprt string_last_index_of(const function_application_exprt &f); + + string_exprt string_insert(const string_exprt & s1, const string_exprt & s2, const exprt &offset); + string_exprt string_insert(const function_application_exprt &f); + string_exprt string_insert_int(const function_application_exprt &f); + string_exprt string_insert_long(const function_application_exprt &f); + string_exprt string_insert_bool(const function_application_exprt &f); + string_exprt string_insert_char(const function_application_exprt &f); + string_exprt string_insert_double(const function_application_exprt &f); + string_exprt string_insert_float(const function_application_exprt &f); + string_exprt string_insert_char_array(const function_application_exprt &f); + exprt string_is_empty(const function_application_exprt &f); + exprt string_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt & offset); + exprt string_is_prefix(const function_application_exprt &f, bool swap_arguments=false); + exprt string_is_suffix(const function_application_exprt &f, bool swap_arguments=false); + exprt string_length(const function_application_exprt &f); + string_exprt string_literal(const function_application_exprt &f); + string_exprt of_int(const function_application_exprt &f); + string_exprt of_int(const exprt &i, size_t max_size); + string_exprt of_int_hex(const exprt &i); + string_exprt of_int_hex(const function_application_exprt &f); + string_exprt of_long(const function_application_exprt &f); + string_exprt of_long(const exprt &i, size_t max_size); + string_exprt of_bool(const function_application_exprt &f); + string_exprt of_bool(const exprt &i); + string_exprt of_char(const function_application_exprt &f); + string_exprt of_char(const exprt &i); + string_exprt of_char_array(const function_application_exprt &f); + string_exprt of_char_array + (const exprt & length, const exprt & data, const exprt & offset, const exprt & count); + + // Warning: the specifications of these functions is only partial: + string_exprt of_float(const function_application_exprt &f); + string_exprt of_float(const exprt &f, bool double_precision=false); + string_exprt of_double(const function_application_exprt &f); + + string_exprt string_replace(const function_application_exprt &f); + string_exprt string_set_length(const function_application_exprt &f); + + // Warning: the specification may not be correct for the case where the string is not long enough + string_exprt string_substring(const string_exprt & str, const exprt & start, const exprt & end); + string_exprt string_substring(const function_application_exprt &expr); + + string_exprt string_to_lower_case(const function_application_exprt &expr); + string_exprt string_to_upper_case(const function_application_exprt &expr); + string_exprt string_trim(const function_application_exprt &expr); + + // Warning: not working correctly at the moment + string_exprt string_value_of(const function_application_exprt &f); + + string_exprt code_point(const exprt &code_point); + string_exprt java_char_array(const exprt & char_array); + + string_exprt string_if(const if_exprt &expr); + + exprt char_literal(const function_application_exprt &f); + + + // Warning: this function is underspecified + exprt string_code_point_count(const function_application_exprt &f); + // Warning: this function is underspecified + exprt string_offset_by_code_point(const function_application_exprt &f); + exprt string_parse_int(const function_application_exprt &f); + exprt string_to_char_array(const function_application_exprt &f); + + exprt 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 string_intern(const function_application_exprt &f); + + // Check that the given string is from the right language + void check_char_type(const exprt & str); + +private: + + enum {C, JAVA, UNKNOWN} language; + + + inline bool use_c_string() {return (language == C);} + + // assert that the number of argument is equal to nb and extract them + inline function_application_exprt::argumentst args(const function_application_exprt &expr, size_t nb) + { + function_application_exprt::argumentst args = expr.arguments(); + assert(args.size() == nb); + return args; + } + + exprt int_of_hex_char(exprt chr, unsigned char_width, typet char_type); + exprt is_high_surrogate(const exprt & chr); + exprt is_low_surrogate(const exprt & chr); + std::map pool; + std::map hash; + +}; + +#endif diff --git a/src/solvers/refinement/string_expr.cpp b/src/solvers/refinement/string_expr.cpp new file mode 100644 index 00000000000..263f06a6838 --- /dev/null +++ b/src/solvers/refinement/string_expr.cpp @@ -0,0 +1,33 @@ +/** -*- C++ -*- *****************************************************\ + +Module: String expressions for PASS algorithm + (see the PASS paper at HVC'13) + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include + +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); +} + +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); +} + + diff --git a/src/solvers/refinement/string_expr.h b/src/solvers/refinement/string_expr.h new file mode 100644 index 00000000000..2c0a3c4dc56 --- /dev/null +++ b/src/solvers/refinement/string_expr.h @@ -0,0 +1,92 @@ +/** -*- 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 + + +// 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()) {}; + + // 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);} + inline index_exprt operator[] (int i) const + { return index_exprt(content(), refined_string_typet::index_of_int(i));} + + // Comparison on the length of the strings + inline binary_relation_exprt longer(const string_exprt & rhs) const + { return binary_relation_exprt(length(), ID_ge, rhs.length()); } + inline binary_relation_exprt longer (const exprt & rhs) const + { return binary_relation_exprt(length(), ID_ge, rhs); } + inline binary_relation_exprt strictly_longer (const exprt & rhs) const + { return binary_relation_exprt(rhs, ID_lt, length()); } + inline binary_relation_exprt strictly_longer (const string_exprt & rhs) const + { return binary_relation_exprt(rhs.length(), ID_lt, length()); } + inline binary_relation_exprt strictly_longer (int i) const + { return strictly_longer(refined_string_typet::index_of_int(i)); } + inline binary_relation_exprt shorter (const string_exprt & rhs) const + { return binary_relation_exprt(length(), ID_le, rhs.length()); } + inline binary_relation_exprt shorter (const exprt & rhs) const + { return binary_relation_exprt(length(), ID_le, rhs); } + inline binary_relation_exprt shorter (int i) const + { return shorter(refined_string_typet::index_of_int(i)); } + inline binary_relation_exprt strictly_shorter (const string_exprt & rhs) const + { return binary_relation_exprt(length(), ID_lt, rhs.length()); } + inline binary_relation_exprt strictly_shorter (const exprt & rhs) const + { return binary_relation_exprt(length(), ID_lt, rhs); } + inline equal_exprt same_length (const string_exprt & rhs) const + { return equal_exprt(length(), rhs.length()); } + inline equal_exprt has_length (const exprt & rhs) const + { return equal_exprt(length(), rhs); } + inline equal_exprt has_length (int i) const + { return has_length(refined_string_typet::index_of_int(i)); } + + static irep_idt extract_java_string(const symbol_exprt & s); + + 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..83786de2098 --- /dev/null +++ b/src/solvers/refinement/string_functions.h @@ -0,0 +1,79 @@ +/*******************************************************************\ + +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_insert_char_array_func("__CPROVER_uninterpreted_string_insert_char_array_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_data_func("__CPROVER_uninterpreted_string_data_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_of_char_array_func("__CPROVER_uninterpreted_string_of_char_array_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..a3a1cb6be0c --- /dev/null +++ b/src/solvers/refinement/string_refinement.cpp @@ -0,0 +1,769 @@ +/** -*- 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 + +// 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; + start_time = std::chrono::high_resolution_clock::now(); +} + +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; + } +} + +// We compute the index set for all formulas, instantiate the formulas +// with the found indexes, and add them as lemmas. +void string_refinementt::add_instantiations() +{ + debug() << "string_constraint_generatort::add_instantiations: " + << "going through the current index set:" << eom; + for (std::map::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); + } + } + } +} + +literalt string_refinementt::convert_rest(const exprt &expr) +{ + if(expr.id()==ID_function_application) + { + // can occur in __CPROVER_assume + bvt bv = convert_function_application(to_function_application_expr(expr)); + assert(bv.size() == 1); + return bv[0]; + } + else + { + return SUB::convert_rest(expr); + } +} + +bvt string_refinementt::convert_symbol(const exprt &expr) +{ + const typet &type = expr.type(); + const irep_idt &identifier = expr.get(ID_identifier); + assert(!identifier.empty()); + + if (refined_string_typet::is_unrefined_string_type(type)) + { + generator.check_char_type(expr); + string_exprt str = generator.string_of_symbol(to_symbol_expr(expr)); + bvt bv = convert_bv(str); + return bv; + } + else return SUB::convert_symbol(expr); +} + + +bvt string_refinementt::convert_function_application(const function_application_exprt &expr) +{ + debug() << "string_refinementt::convert_function_application " << pretty_short(expr) << eom; + exprt f = generator.function_application(expr); + return convert_bv(f); +} + +bool string_refinementt::boolbv_set_equality_to_true(const equal_exprt &expr) +{ + 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 " << pretty_short(expr.lhs()) << " <- " + << pretty_short(expr.rhs()) << eom; + + if(refined_string_typet::is_unrefined_string_type(type)) + { + generator.check_char_type(expr.lhs()); + symbol_exprt sym = to_symbol_expr(expr.lhs()); + generator.string_of_expr(sym,expr.rhs()); + 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; +} + + + +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; +} + +decision_proceduret::resultt string_refinementt::dec_solve() +{ + + print_time("string_refinementt::dec_solve"); + for(unsigned i = 0; i < generator.axioms.size(); i++) + if(generator.axioms[i].is_simple()) + add_lemma(generator.axioms[i]); + else if(generator.axioms[i].is_string_constant()) + add_lemma(generator.axioms[i]); //,false); + else if(generator.axioms[i].is_univ_quant()) { + debug() << "universaly quantified : " << pretty_short(generator.axioms[i]) << eom; + universal_axioms.push_back(generator.axioms[i]); + } + else { + assert(generator.axioms[i].is_not_contains()); + generator.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(generator.axioms[i]); + } + + //string_axioms.clear(); should not be necessary + + 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; + } + + 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(unsigned i=0; i lemmas; + instantiate_not_contains(not_contains_axioms[i],lemmas); + for(unsigned j=0; j500) 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 = generator.symbol_to_string.begin(); it != generator.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 = generator.boolean_symbols.begin(); + it != generator.boolean_symbols.end(); it++) { + debug() << "" << it->get_identifier() << " := " << pretty_short(get(*it)) << eom; + fmodel[*it] = get(*it); + } + + for(std::vector::iterator it = generator.index_symbols.begin(); + it != generator.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(refined_string_typet::index_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; + } + +} + + +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 std::vector & 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(refined_string_typet::index_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(refined_string_typet::index_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(refined_string_typet::index_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(refined_string_typet::index_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..ecd21143b2c --- /dev/null +++ b/src/solvers/refinement/string_refinement.h @@ -0,0 +1,150 @@ +/** -*- 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 +#include + +// This is to analyse the performances of the different steps +#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(); } + + static exprt is_positive(const exprt & x); + +private: + typedef bv_refinementt SUB; + std::chrono::high_resolution_clock::time_point start_time; + + +protected: + + typedef std::set expr_sett; + + virtual bvt convert_symbol(const exprt &expr); + virtual bvt convert_function_application + (const function_application_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); + + +private: + + string_constraint_generatort generator; + + // Simple constraints that have been given to the solver + expr_sett seen_instances; + // + std::vector universal_axioms; + // + std::vector not_contains_axioms; + + int nb_sat_iteration; + + // 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; + + // 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 std::vector &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..cb22f3a5d65 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,34 @@ const char **narrow_argv(int argc, const wchar_t **argv_wide) return argv_narrow; } + +std::wstring utf8_to_utf16be(const std::string& in) +{ + std::wstring_convert > converter; + return converter.from_bytes(in); +} + +std::wstring utf8_to_utf16le(const std::string& in) +{ + std::wstring_convert > converter; + return converter.from_bytes(in); +} + +std::string utf16le_to_ascii(const std::wstring& in) +{ + std::string result; + std::locale loc; + for(const auto c : in) + { + if(c <= 255 && isprint(c,loc)) + result+=(unsigned char)c; + else + { + result+="\\u"; + char hex[5]; + sprintf(hex,"%04x",(wchar_t)c); + result+=hex; + } + } + return result; +} diff --git a/src/util/unicode.h b/src/util/unicode.h index 44038a26c04..e22bb10574c 100644 --- a/src/util/unicode.h +++ b/src/util/unicode.h @@ -21,6 +21,10 @@ 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::string utf16le_to_ascii(const std::wstring&); + +std::wstring utf8_to_utf16be(const std::string&); +std::wstring utf8_to_utf16le(const std::string&); const char **narrow_argv(int argc, const wchar_t **argv_wide);