diff --git a/jbmc/regression/jbmc-strings/StartsWith/Test.class b/jbmc/regression/jbmc-strings/StartsWith/Test.class new file mode 100644 index 00000000000..82850bfa7dc Binary files /dev/null and b/jbmc/regression/jbmc-strings/StartsWith/Test.class differ diff --git a/jbmc/regression/jbmc-strings/StartsWith/Test.java b/jbmc/regression/jbmc-strings/StartsWith/Test.java new file mode 100644 index 00000000000..fc849af54ab --- /dev/null +++ b/jbmc/regression/jbmc-strings/StartsWith/Test.java @@ -0,0 +1,72 @@ +// Must be compiled with CProverString: +// javac Test.java ../cprover/CProverString.java +public class Test { + + // Reference implementation + public static boolean referenceStartsWith(String s, String prefix, int offset) { + if (offset < 0 || offset > s.length() - prefix.length()) { + return false; + } + + for (int i = 0; i < prefix.length(); i++) { + if (org.cprover.CProverString.charAt(s, offset + i) + != org.cprover.CProverString.charAt(prefix, i)) { + return false; + } + } + return true; + } + + public static boolean check(String s, String t, int offset) { + // Filter out null strings + if(s == null || t == null) { + return false; + } + + // Act + final boolean result = s.startsWith(t, offset); + + // Assert + final boolean referenceResult = referenceStartsWith(s, t, offset); + assert(result == referenceResult); + + // Check reachability + assert(result == false); + return result; + } + + public static boolean checkDet() { + boolean result = false; + result = "foo".startsWith("foo", 0); + assert(result); + result = "foo".startsWith("f", -1); + assert(!result); + result = "foo".startsWith("oo", 1); + assert(result); + result = "foo".startsWith("f", 1); + assert(!result); + result = "foo".startsWith("bar", 0); + assert(!result); + result = "foo".startsWith("oo", 2); + assert(!result); + assert(false); + return result; + } + + public static boolean checkNonDet(String s) { + // Filter + if (s == null) { + return false; + } + + // Act + final boolean result = s.startsWith(s, 1); + + // Assert + assert(!result); + + // Check reachability + assert(false); + return result; + } +} diff --git a/jbmc/regression/jbmc-strings/StartsWith/test.desc b/jbmc/regression/jbmc-strings/StartsWith/test.desc new file mode 100644 index 00000000000..13bacc2677a --- /dev/null +++ b/jbmc/regression/jbmc-strings/StartsWith/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--refine-strings --string-max-input-length 10 --unwind 10 --function Test.check +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 31 .*: SUCCESS +assertion at file Test.java line 34 .*: FAILURE +-- diff --git a/jbmc/regression/jbmc-strings/StartsWith/test_det.desc b/jbmc/regression/jbmc-strings/StartsWith/test_det.desc new file mode 100644 index 00000000000..bb9017ada0d --- /dev/null +++ b/jbmc/regression/jbmc-strings/StartsWith/test_det.desc @@ -0,0 +1,13 @@ +CORE +Test.class +--refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkDet +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 41 .*: SUCCESS +assertion at file Test.java line 43 .*: SUCCESS +assertion at file Test.java line 45 .*: SUCCESS +assertion at file Test.java line 47 .*: SUCCESS +assertion at file Test.java line 49 .*: SUCCESS +assertion at file Test.java line 51 .*: SUCCESS +assertion at file Test.java line 52 .*: FAILURE +-- diff --git a/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc b/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc new file mode 100644 index 00000000000..b02b55f1509 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--refine-strings --string-max-input-length 100 --unwind 10 --function Test.checkNonDet +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 66 .*: SUCCESS +assertion at file Test.java line 69 .*: FAILURE +-- diff --git a/src/solvers/README.md b/src/solvers/README.md index 7a45f246662..e2f06856aff 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -231,9 +231,6 @@ allocates a new string before calling a primitive. * `cprover_string_is_prefix` : \copybrief string_constraint_generatort::add_axioms_for_is_prefix \link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink - * `cprover_string_is_suffix` : - \copybrief string_constraint_generatort::add_axioms_for_is_suffix - \link string_constraint_generatort::add_axioms_for_is_suffix More... \endlink * `cprover_string_index_of` : \copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink @@ -319,6 +316,8 @@ allocates a new string before calling a primitive. * `cprover_string_intern` : Never tested. * `cprover_string_is_empty` : Should use `cprover_string_length(s) == 0` instead. + * `cprover_string_is_suffix` : Should use `cprover_string_is_prefix` with an + offset argument. * `cprover_string_empty_string` : Can use literal of empty string instead. * `cprover_string_of_long` : Should be the same as `cprover_string_of_int`. * `cprover_string_delete_char_at` : A call to diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index 8c182f1dc49..829c1d21887 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -15,15 +15,19 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include /// Add axioms stating that the returned expression is true exactly when the -/// first string is a prefix of the second one, starting at position offset. +/// offset is greater or equal to 0 and the first string is a prefix of the +/// second one, starting at position offset. /// /// These axioms are: -/// 1. \f$ {\tt isprefix} \Rightarrow |str| \ge |{\tt prefix}|+offset \f$ -/// 2. \f$ \forall 0 \le qvar<|{\tt prefix}|.\ {\tt isprefix} -/// \Rightarrow s0[witness+{\tt offset}]=s2[witness] \f$ -/// 3. \f$ !{\tt isprefix} \Rightarrow |{\tt str}|<|{\tt prefix}|+{\tt offset} -/// \lor (0 \le witness<|{\tt prefix}| -/// \land {\tt str}[witness+{\tt offset}] \ne {\tt prefix}[witness])\f$ +/// 1. isprefix => offset_within_bounds +/// 2. forall qvar in [0, |prefix|). +/// isprefix => str[qvar + offset] = prefix[qvar] +/// 3. !isprefix => !offset_within_bounds +/// || 0 <= witness < |prefix| +/// && str[witness+offset] != prefix[witness] +/// +/// where offset_within_bounds is: +/// offset >= 0 && offset <= |str| && |str| - offset >= |prefix| /// /// \param prefix: an array of characters /// \param str: an array of characters @@ -34,34 +38,39 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( const array_string_exprt &str, const exprt &offset) { - symbol_exprt isprefix=fresh_boolean("isprefix"); - const typet &index_type=str.length().type(); + const symbol_exprt isprefix = fresh_boolean("isprefix"); + const typet &index_type = str.length().type(); + const exprt offset_within_bounds = and_exprt( + binary_relation_exprt(offset, ID_ge, from_integer(0, offset.type())), + binary_relation_exprt(offset, ID_le, str.length()), + binary_relation_exprt( + minus_exprt(str.length(), offset), ID_ge, prefix.length())); // Axiom 1. - lemmas.push_back( - implies_exprt( - isprefix, str.axiom_for_length_ge(plus_exprt(prefix.length(), offset)))); - - symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type); - string_constraintt a2( - qvar, - prefix.length(), - implies_exprt( - isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]))); - constraints.push_back(a2); - - symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type); - and_exprt witness_diff( - axiom_for_is_positive_index(witness), - and_exprt( + lemmas.push_back(implies_exprt(isprefix, offset_within_bounds)); + + // Axiom 2. + constraints.push_back([&] { + const symbol_exprt qvar = fresh_univ_index("QA_isprefix", index_type); + const exprt body = implies_exprt( + isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar])); + return string_constraintt(qvar, prefix.length(), body); + }()); + + // Axiom 3. + lemmas.push_back([&] { + const exprt witness = fresh_exist_index("witness_not_isprefix", index_type); + const exprt strings_differ_at_witness = and_exprt( + axiom_for_is_positive_index(witness), prefix.axiom_for_length_gt(witness), - notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]))); - or_exprt s0_notpref_s1( - not_exprt(str.axiom_for_length_ge(plus_exprt(prefix.length(), offset))), - witness_diff); + notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness])); + const exprt s1_does_not_start_with_s0 = or_exprt( + not_exprt(offset_within_bounds), + not_exprt(str.axiom_for_length_ge(plus_exprt(prefix.length(), offset))), + strings_differ_at_witness); + return implies_exprt(not_exprt(isprefix), s1_does_not_start_with_s0); + }()); - implies_exprt a3(not_exprt(isprefix), s0_notpref_s1); - lemmas.push_back(a3); return isprefix; } @@ -135,6 +144,7 @@ exprt string_constraint_generatort::add_axioms_for_is_empty( /// \param swap_arguments: boolean flag telling whether the suffix is the second /// argument or the first argument /// \return Boolean expression `issuffix` +DEPRECATED("should use `strings_startwith(s0, s1, s1.length - s0.length)`") exprt string_constraint_generatort::add_axioms_for_is_suffix( const function_application_exprt &f, bool swap_arguments) { diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index cdc7f984d32..57be41871c1 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1833,18 +1833,17 @@ static void update_index_set( } } -/// Finds an index on `str` used in `expr` that contains `qvar`, for instance -/// with arguments ``(str[k]=='a')``, `str`, and `k`, the function should -/// return `k`. -/// If two different such indexes exist, an invariant will fail. +/// Find indexes of `str` used in `expr` that contains `qvar`, for instance +/// with arguments ``(str[k+1]=='a')``, `str`, and `k`, the function should +/// return `k+1`. /// \param [in] expr: the expression to search /// \param [in] str: the string which must be indexed /// \param [in] qvar: the universal variable that must be in the index -/// \return an index expression in `expr` on `str` containing `qvar`. Returns -/// an empty optional when `expr` does not contain `str`. -static optionalt -find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar) +/// \return index expressions in `expr` on `str` containing `qvar`. +static std::unordered_set +find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar) { + decltype(find_indexes(expr, str, qvar)) result; auto index_str_containing_qvar = [&](const exprt &e) { if(auto index_expr = expr_try_dynamic_cast(e)) { @@ -1855,28 +1854,11 @@ find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar) return false; }; - auto it = std::find_if( - expr.depth_begin(), expr.depth_end(), index_str_containing_qvar); - if(it == expr.depth_end()) - return {}; - const exprt &index = to_index_expr(*it).index(); - - // Check that there are no two such indexes - it.next_sibling_or_parent(); - while(it != expr.depth_end()) - { - if(index_str_containing_qvar(*it)) - { - INVARIANT( - to_index_expr(*it).index() == index, - "string should always be indexed by same value in a given formula"); - it.next_sibling_or_parent(); - } - else - ++it; - } - - return index; + std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { + if(index_str_containing_qvar(e)) + result.insert(to_index_expr(e).index()); + }); + return result; } /// Instantiates a string constraint by substituting the quantifiers. @@ -1897,18 +1879,24 @@ static exprt instantiate( const exprt &str, const exprt &val) { - const optionalt idx = find_index(axiom.body, str, axiom.univ_var); - if(!idx.has_value()) - return true_exprt(); - - const exprt r = compute_inverse_function(stream, axiom.univ_var, val, *idx); - implies_exprt instance( - and_exprt( - binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound), - binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)), - axiom.body); - replace_expr(axiom.univ_var, r, instance); - return instance; + const auto indexes = find_indexes(axiom.body, str, axiom.univ_var); + INVARIANT( + str.id() == ID_array || indexes.size() <= 1, + "non constant array should always be accessed at the same index"); + exprt::operandst conjuncts; + for(const auto &index : indexes) + { + const exprt univ_var_value = + compute_inverse_function(stream, axiom.univ_var, val, index); + implies_exprt instance( + and_exprt( + binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound), + binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)), + axiom.body); + replace_expr(axiom.univ_var, univ_var_value, instance); + conjuncts.push_back(instance); + } + return conjunction(conjuncts); } /// Instantiates a quantified formula representing `not_contains` by