diff --git a/regression/strings-smoke-tests/java_contains/test.desc b/regression/strings-smoke-tests/java_contains/test.desc index 0c10fd4de93..e0ca4731a42 100644 --- a/regression/strings-smoke-tests/java_contains/test.desc +++ b/regression/strings-smoke-tests/java_contains/test.desc @@ -1,8 +1,12 @@ CORE test_contains.class --refine-strings -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ +^\[.*assertion.2\].* line 9.* SUCCESS$ +^\[.*assertion.3\].* line 12.* FAILURE$ +^\[.*assertion.4\].* line 13.* FAILURE$ +^VERIFICATION FAILED$ -- Issue: diffblue/test-gen#201 diff --git a/regression/strings-smoke-tests/java_contains/test_contains.class b/regression/strings-smoke-tests/java_contains/test_contains.class index 989f5f04279..078a8565a35 100644 Binary files a/regression/strings-smoke-tests/java_contains/test_contains.class and b/regression/strings-smoke-tests/java_contains/test_contains.class differ diff --git a/regression/strings-smoke-tests/java_contains/test_contains.java b/regression/strings-smoke-tests/java_contains/test_contains.java index fb585a2f0eb..f385c0593d2 100644 --- a/regression/strings-smoke-tests/java_contains/test_contains.java +++ b/regression/strings-smoke-tests/java_contains/test_contains.java @@ -1,12 +1,15 @@ public class test_contains { - public static void main(/*String[] argv*/) + public static void main(String x) { String s = new String("Abc"); String u = "bc"; String t = "ab"; assert(s.contains(u)); - // Long version: - // assert(s.contains(t)); + assert(!s.contains(t)); + + String z = new String(x); + if (z.length() > 3) assert(t.contains(z)); + else assert(z.contains(u)); } } diff --git a/regression/strings/StringContains01/test.class b/regression/strings/StringContains01/test.class new file mode 100644 index 00000000000..ce12a0ee470 Binary files /dev/null and b/regression/strings/StringContains01/test.class differ diff --git a/regression/strings/StringContains01/test.desc b/regression/strings/StringContains01/test.desc new file mode 100644 index 00000000000..2e66f73126f --- /dev/null +++ b/regression/strings/StringContains01/test.desc @@ -0,0 +1,6 @@ +FUTURE +test.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/strings/StringContains01/test.java b/regression/strings/StringContains01/test.java new file mode 100644 index 00000000000..de588381d8a --- /dev/null +++ b/regression/strings/StringContains01/test.java @@ -0,0 +1,8 @@ +public class test +{ + public static void main(String s) + { + String ab = "abc"; + assert(ab.contains(s)); + } +} diff --git a/regression/strings/StringContains02/test.class b/regression/strings/StringContains02/test.class new file mode 100644 index 00000000000..c1b575d8c6e Binary files /dev/null and b/regression/strings/StringContains02/test.class differ diff --git a/regression/strings/StringContains02/test.desc b/regression/strings/StringContains02/test.desc new file mode 100644 index 00000000000..2e66f73126f --- /dev/null +++ b/regression/strings/StringContains02/test.desc @@ -0,0 +1,6 @@ +FUTURE +test.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/strings/StringContains02/test.java b/regression/strings/StringContains02/test.java new file mode 100644 index 00000000000..77fa0284700 --- /dev/null +++ b/regression/strings/StringContains02/test.java @@ -0,0 +1,7 @@ +public class test +{ + public static void main(String s) + { + assert(s.contains("Hello")); + } +} diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 878441cd0d1..4e2134d6388 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -194,9 +194,10 @@ exprt string_constraint_generatort::add_axioms_for_contains( // We add axioms: // a1 : contains ==> |s0| >= |s1| - // a2 : 0 <= startpos <= |s0|-|s1| - // a3 : forall qvar < |s1|. contains ==> s1[qvar] = s0[startpos + qvar] - // a4 : !contains ==> |s1| > |s0| || + // a2 : contains ==> 0 <= startpos <= |s0|-|s1| + // a3 : !contains ==> startpos = -1 + // a4 : forall qvar < |s1|. contains ==> s1[qvar] = s0[startpos + qvar] + // a5 : !contains ==> |s1| > |s0| || // (forall startpos <= |s0| - |s1|. // exists witness < |s1|. s1[witness] != s0[witness + startpos]) @@ -211,9 +212,14 @@ exprt string_constraint_generatort::add_axioms_for_contains( implies_exprt a2(contains, bounds); axioms.push_back(a2); + implies_exprt a3( + not_exprt(contains), + equal_exprt(startpos, from_integer(-1, index_type))); + axioms.push_back(a3); + if(constant) { - // If the string is constant, we can use a more efficient axiom for a3: + // If the string is constant, we can use a more efficient axiom for a4: // contains ==> AND_{i < |s1|} s1[i] = s0[startpos + i] mp_integer s1_length; assert(!to_integer(s1.length(), s1_length)); @@ -224,10 +230,10 @@ exprt string_constraint_generatort::add_axioms_for_contains( plus_exprt shifted_i(expr_i, startpos); conjuncts.push_back(equal_exprt(s1[expr_i], s0[shifted_i])); } - implies_exprt a3(contains, conjunction(conjuncts)); - axioms.push_back(a3); + implies_exprt a4(contains, conjunction(conjuncts)); + axioms.push_back(a4); - // The a4 constraint for constant strings translates to: + // The a5 constraint for constant strings translates to: // !contains ==> |s1| > |s0| || // (forall qvar <= |s0| - |s1|. // !(AND_{i < |s1|} s1[i] == s0[i + qvar]) @@ -244,30 +250,30 @@ exprt string_constraint_generatort::add_axioms_for_contains( conjuncts1.push_back(equal_exprt(s1[expr_i], s0[shifted_i])); } - string_constraintt a4( + string_constraintt a5( qvar, plus_exprt(from_integer(1, index_type), length_diff), and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)), not_exprt(conjunction(conjuncts1))); - axioms.push_back(a4); + axioms.push_back(a5); } else { symbol_exprt qvar=fresh_univ_index("QA_contains", index_type); exprt qvar_shifted=plus_exprt(qvar, startpos); - string_constraintt a3( + string_constraintt a4( qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted])); - axioms.push_back(a3); + axioms.push_back(a4); // We rewrite axiom a4 as: // forall startpos <= |s0|-|s1|. (!contains && |s0| >= |s1|) // ==> exists witness < |s1|. s1[witness] != s0[startpos+witness] - string_not_contains_constraintt a4( + string_not_contains_constraintt a5( from_integer(0, index_type), plus_exprt(from_integer(1, index_type), length_diff), and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)), from_integer(0, index_type), s1.length(), s0, s1); - axioms.push_back(a4); + axioms.push_back(a5); } return typecast_exprt(contains, f.type()); }