diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc index 6033af25d1b..e0e7de66561 100644 --- a/regression/strings-smoke-tests/java_index_of/test.desc +++ b/regression/strings-smoke-tests/java_index_of/test.desc @@ -1,8 +1,7 @@ -KNOWNBUG +CORE test_index_of.class --refine-strings ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -Issue: cbmc/test-gen#77 diff --git a/regression/strings-smoke-tests/java_index_of/test_index_of.class b/regression/strings-smoke-tests/java_index_of/test_index_of.class index 1acb3335d57..8a989bdc95c 100644 Binary files a/regression/strings-smoke-tests/java_index_of/test_index_of.class and b/regression/strings-smoke-tests/java_index_of/test_index_of.class differ diff --git a/regression/strings-smoke-tests/java_index_of/test_index_of.java b/regression/strings-smoke-tests/java_index_of/test_index_of.java index 270267196c5..3568dab9696 100644 --- a/regression/strings-smoke-tests/java_index_of/test_index_of.java +++ b/regression/strings-smoke-tests/java_index_of/test_index_of.java @@ -1,10 +1,13 @@ public class test_index_of { - public static void main(/*String[] argv*/) - { - String s = "Abc"; - String bc = "bc"; - int i = s.indexOf(bc); - assert(i == 1); - } + public static void main(/*String[] argv*/) + { + String s = "Abc"; + String bc = "bc"; + String ab = "ab"; + int i = s.indexOf(bc); + int j = s.indexOf(ab); + assert(i == 1); + assert(j == -1); + } } diff --git a/regression/strings-smoke-tests/java_last_index_of/test.desc b/regression/strings-smoke-tests/java_last_index_of/test.desc index 5ee1604e846..381078254cd 100644 --- a/regression/strings-smoke-tests/java_last_index_of/test.desc +++ b/regression/strings-smoke-tests/java_last_index_of/test.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE test_last_index_of.class --refine-strings -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^\[.*assertion.1\].* line 8.* SUCCESS$ +^\[.*assertion.2\].* line 9.* FAILURE$ -- -Issue: diffblue/test-gen#77 diff --git a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class index 4455da4d179..26f5ec3a7c3 100644 Binary files a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class and b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.class differ diff --git a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java index 8b3a0904d5b..59b9f5ab36d 100644 --- a/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java +++ b/regression/strings-smoke-tests/java_last_index_of/test_last_index_of.java @@ -1,10 +1,11 @@ public class test_last_index_of { - public static void main(/*String[] argv*/) - { - String s = "abcab"; - String ab = "ab"; - int i = s.lastIndexOf(ab); - assert(i == 3); - } + public static void main(/*String[] argv*/) + { + String s = "abcab"; + String ab = "ab"; + int i = s.lastIndexOf(ab); + assert(i == 3); + assert(i == 1); + } } diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 525f0fee3d7..94234b810de 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -194,24 +194,18 @@ class string_constraint_generatort const exprt &from_index); // Add axioms corresponding to the String.indexOf:(String;I) java function - // TODO: the specifications are only partial: - // we add axioms stating that the returned value is either -1 or greater than - // from_index and the string beggining there has prefix substring exprt add_axioms_for_index_of_string( - const string_exprt &str, - const string_exprt &substring, + const string_exprt &haystack, + const string_exprt &needle, const exprt &from_index); // Add axioms corresponding to the String.indexOf java functions - // TODO: the specifications are only partial for the ones that look for - // strings exprt add_axioms_for_index_of(const function_application_exprt &f); // Add axioms corresponding to the String.lastIndexOf:(String;I) java function - // TODO: the specifications are only partial exprt add_axioms_for_last_index_of_string( - const string_exprt &str, - const string_exprt &substring, + const string_exprt &haystack, + const string_exprt &needle, const exprt &from_index); // Add axioms corresponding to the String.lastIndexOf:(CI) java function @@ -221,7 +215,6 @@ class string_constraint_generatort const exprt &from_index); // Add axioms corresponding to the String.lastIndexOf java functions - // TODO: the specifications is only partial exprt add_axioms_for_last_index_of(const function_application_exprt &f); // TODO: the specifications of these functions is only partial diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index d799091a573..9386639e594 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -13,12 +13,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com Function: string_constraint_generatort::add_axioms_for_index_of - Inputs: a string expression, a character expression and an integer expression + Inputs: + str - a string expression + c - an expression representing a character + from_index - an expression representing an index in the string Outputs: a integer expression - Purpose: add axioms that the returned value is either -1 or greater than - from_index and the character at that position equals to c + Purpose: Add axioms stating that the returned value is the index within + str of the first occurence of c starting the search at from_index, + or -1 if no such character occurs at or after position from_index. \*******************************************************************/ @@ -30,11 +34,11 @@ exprt string_constraint_generatort::add_axioms_for_index_of( symbol_exprt contains=fresh_boolean("contains_in_index_of"); // We add axioms: - // a1 : -1 <= index<|str| + // a1 : -1 <= index < |str| // a2 : !contains <=> index=-1 - // a3 : contains => from_index<=index&&str[index]=c - // a4 : forall n, from_index<=n str[n]!=c - // a5 : forall m, from_index<=n<|str|. !contains => str[m]!=c + // a3 : contains ==> from_index <= index && str[index] = c + // a4 : forall n, n:[from_index,index[. contains ==> str[n] != c + // a5 : forall m, n:[from_index,|str|[. !contains ==> str[m] != c exprt minus1=from_integer(-1, index_type); and_exprt a1( @@ -73,39 +77,49 @@ exprt string_constraint_generatort::add_axioms_for_index_of( Function: string_constraint_generatort::add_axioms_for_index_of_string - Inputs: two string expressions and an integer expression + Inputs: + haystack - a string expression + needle - a string expression + from_index - an expression representing an index in strings - Outputs: a integer expression + Outputs: an integer expression representing the first index of needle in + haystack after from_index, or -1 if there is none - Purpose: add axioms stating that the returned value is either -1 or greater - than from_index and the string beggining there has prefix substring + Purpose: Add axioms stating that the returned value is the index within + haystack of the first occurence of needle starting the search at + from_index, or -1 if needle does not occur at or after position + from_index. \*******************************************************************/ exprt string_constraint_generatort::add_axioms_for_index_of_string( - const string_exprt &str, - const string_exprt &substring, + const string_exprt &haystack, + const string_exprt &needle, const exprt &from_index) { - const typet &index_type=str.length().type(); + const typet &index_type=haystack.length().type(); symbol_exprt offset=fresh_exist_index("index_of", index_type); symbol_exprt contains=fresh_boolean("contains_substring"); // We add axioms: - // a1 : contains => |str|-|substring|>=offset>=from_index - // a2 : !contains => offset=-1 - // a3 : forall 0<=witness<|substring|. - // contains => str[witness+offset]=substring[witness] + // a1 : contains ==> from_index <= offset <= |haystack|-|needle| + // a2 : !contains <=> offset=-1 + // a3 : forall n:[0,|needle|[. + // contains ==> haystack[n+offset]=needle[n] + // a4 : forall n:[from_index,offset[. + // contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]]) + // a5: forall n:[from_index,|haystack|-|needle|[. + // !contains ==> (exists m:[0,|needle|[. haystack[m+n] != needle[m]) implies_exprt a1( contains, and_exprt( - str.axiom_for_is_longer_than(plus_exprt_with_overflow_check( - substring.length(), offset)), - binary_relation_exprt(offset, ID_ge, from_index))); + binary_relation_exprt(from_index, ID_le, offset), + binary_relation_exprt( + offset, ID_le, minus_exprt(haystack.length(), needle.length())))); axioms.push_back(a1); - implies_exprt a2( + equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); axioms.push_back(a2); @@ -113,47 +127,188 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type); string_constraintt a3( qvar, - substring.length(), + needle.length(), contains, - equal_exprt(str[plus_exprt(qvar, offset)], substring[qvar])); + equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])); axioms.push_back(a3); + if(!is_constant_string(needle)) + { + // string_not contains_constraintt are formulas of the form: + // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y] + string_not_contains_constraintt a4( + from_index, + offset, + contains, + from_integer(0, index_type), + needle.length(), + haystack, + needle); + axioms.push_back(a4); + + string_not_contains_constraintt a5( + from_index, + minus_exprt(haystack.length(), needle.length()), + not_exprt(contains), + from_integer(0, index_type), + needle.length(), + haystack, + needle); + axioms.push_back(a5); + } + else + { + // Unfold the existential quantifier as a disjunction in case of a constant + // a4 && a5 <=> a6: + // forall n:[from_index,|haystack|-|needle|]. + // !contains || n < offset ==> + // haystack[n] != needle[0] || ... || + // haystack[n+|needle|-1] != needle[|needle|-1] + symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type); + mp_integer sub_length; + assert(!to_integer(needle.length(), sub_length)); + exprt::operandst disjuncts; + for(mp_integer offset=0; offset |substring| >= length &&offset <= from_index - // a2 : !contains => offset=-1 - // a3 : forall 0 <= witness str[witness+offset]=substring[witness] + // a1 : contains ==> offset <= from_index && offset <= |haystack| - |needle| + // a2 : !contains <=> offset = -1 + // a3 : forall n:[0, needle.length[, + // contains ==> haystack[n+offset] = needle[n] + // a4 : forall n:[offset+1, min(from_index, |haystack| - |needle|)]. + // contains ==> + // (exists m:[0,|substring|[. haystack[m+n] != needle[m]]) + // a5: forall n:[0, min(from_index, |haystack| - |needle|)]. + // !contains ==> + // (exists m:[0,|substring|[. haystack[m+n] != needle[m]) implies_exprt a1( contains, and_exprt( - str.axiom_for_is_longer_than( - plus_exprt_with_overflow_check(substring.length(), offset)), + binary_relation_exprt( + offset, ID_le, minus_exprt(haystack.length(), needle.length())), binary_relation_exprt(offset, ID_le, from_index))); axioms.push_back(a1); - implies_exprt a2( + equal_exprt a2( not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type))); axioms.push_back(a2); symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type); - equal_exprt constr3(str[plus_exprt(qvar, offset)], substring[qvar]); - string_constraintt a3(qvar, substring.length(), contains, constr3); + equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]); + string_constraintt a3(qvar, needle.length(), contains, constr3); axioms.push_back(a3); + // end_index is min(from_index, |str| - |substring|) + minus_exprt length_diff(haystack.length(), needle.length()); + if_exprt end_index( + binary_relation_exprt(from_index, ID_le, length_diff), + from_index, + length_diff); + + if(!is_constant_string(needle)) + { + string_not_contains_constraintt a4( + plus_exprt(offset, from_integer(1, index_type)), + plus_exprt(end_index, from_integer(1, index_type)), + contains, + from_integer(0, index_type), + needle.length(), + haystack, + needle); + axioms.push_back(a4); + + string_not_contains_constraintt a5( + from_integer(0, index_type), + plus_exprt(end_index, from_integer(1, index_type)), + not_exprt(contains), + from_integer(0, index_type), + needle.length(), + haystack, + needle); + axioms.push_back(a5); + } + else + { + // Unfold the existential quantifier as a disjunction in case of a constant + // a4 && a5 <=> a6: + // forall n:[0, min(from_index,|haystack|-|needle|)]. + // !contains || n > offset ==> + // haystack[n] != needle[0] || ... || + // haystack[n+|needle|-1] != needle[|needle|-1] + symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type); + mp_integer sub_length; + assert(!to_integer(needle.length(), sub_length)); + exprt::operandst disjuncts; + for(mp_integer offset=0; offset !contains) - // a3 : (contains => i <= from_index &&s[i]=c) - // a4 : forall n. i+1 <= n < from_index +1 &&contains => s[n]!=c - // a5 : forall m. 0 <= m < from_index +1 &&!contains => s[m]!=c + // a2 : i = -1 <=> !contains + // a3 : contains ==> (i <= from_index && s[i] = c) + // a4 : forall n:[i+1, from_index+1[ && contains ==> s[n] != c + // a5 : forall m:[0, from_index+1[ && !contains ==> s[m] != c exprt index1=from_integer(1, index_type); exprt minus1=from_integer(-1, index_type);