diff --git a/regression/jbmc-strings/StringBuilderInsert/Test.class b/regression/jbmc-strings/StringBuilderInsert/Test.class new file mode 100644 index 00000000000..3496f23684e Binary files /dev/null and b/regression/jbmc-strings/StringBuilderInsert/Test.class differ diff --git a/regression/jbmc-strings/StringBuilderInsert/Test.java b/regression/jbmc-strings/StringBuilderInsert/Test.java new file mode 100644 index 00000000000..173b3b53dd2 --- /dev/null +++ b/regression/jbmc-strings/StringBuilderInsert/Test.java @@ -0,0 +1,48 @@ + +public class Test { + public void check (int i) { + if(i == 0) + { + // Arrange + StringBuilder s = new StringBuilder("bar"); + + // Act + s = org.cprover.CProverString.insert(s, 0, "foo"); + + // Should succeed + assert s.toString().equals("foobar"); + + // Should fail + assert !s.toString().equals("foobar"); + } + if(i == 1) + { + // Arrange + StringBuilder s = new StringBuilder("bar"); + + // Act + s = org.cprover.CProverString.insert(s, -10, "foo"); + + // Should succeed + assert s.toString().equals("foobar"); + + // Should fail + assert !s.toString().equals("foobar"); + } + if(i == 2) + { + // Arrange + StringBuilder s = new StringBuilder("bar"); + + // Act + s = org.cprover.CProverString.insert(s, 10, "foo"); + + // Should succeed + assert s.toString().equals("barfoo"); + + // Should fail + assert !s.toString().equals("barfoo"); + } + + } +} diff --git a/regression/jbmc-strings/StringBuilderInsert/test.desc b/regression/jbmc-strings/StringBuilderInsert/test.desc new file mode 100644 index 00000000000..68b636a5d67 --- /dev/null +++ b/regression/jbmc-strings/StringBuilderInsert/test.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--refine-strings --function Test.check +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 13 .*: SUCCESS +assertion at file Test.java line 16 .*: FAILURE +assertion at file Test.java line 27 .*: SUCCESS +assertion at file Test.java line 30 .*: FAILURE +assertion at file Test.java line 41 .*: SUCCESS +assertion at file Test.java line 44 .*: FAILURE +-- diff --git a/regression/jbmc-strings/StringConcat_StringII/Test.class b/regression/jbmc-strings/StringConcat_StringII/Test.class new file mode 100644 index 00000000000..c1783156f96 Binary files /dev/null and b/regression/jbmc-strings/StringConcat_StringII/Test.class differ diff --git a/regression/jbmc-strings/StringConcat_StringII/Test.java b/regression/jbmc-strings/StringConcat_StringII/Test.java new file mode 100644 index 00000000000..50faba13c80 --- /dev/null +++ b/regression/jbmc-strings/StringConcat_StringII/Test.java @@ -0,0 +1,40 @@ +// This test uses CProverString so should be compiled with +// javac Test.java ../cprover/CProverString.java +import org.cprover.CProverString; + +class Test { + public void testSuccess(String s, String t, int start, int end) { + // Filter + if (s == null || t == null) + return; + + // Act + StringBuilder sb = new StringBuilder(s); + String result = CProverString.append(sb, t, start, end).toString(); + + // Arrange + StringBuilder reference = new StringBuilder(s); + if(start < 0) + start = 0; + for (int i = start; i < end && i < t.length(); i++) + reference.append(org.cprover.CProverString.charAt(t, i)); + + // Assert + assert result.equals(reference.toString()); + } + + public void testFail(int i) { + // Arrange + StringBuilder sb = new StringBuilder("foo"); + + // Act + CProverString.append(sb, "bar", 0, 1); + CProverString.append(sb, "bar", 0, 4); + CProverString.append(sb, "foo", -1, 0); + CProverString.append(sb, "foo", -10, -1); + CProverString.append(sb, "bar", -10, 25); + + // Assert + assert !sb.toString().equals("foobbarbar"); + } +} diff --git a/regression/jbmc-strings/StringConcat_StringII/test.desc b/regression/jbmc-strings/StringConcat_StringII/test.desc new file mode 100644 index 00000000000..4876a04b8e4 --- /dev/null +++ b/regression/jbmc-strings/StringConcat_StringII/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--refine-strings --string-max-length 100 --string-max-input-length 4 --verbosity 10 --unwind 5 Test.class --function Test.testSuccess +^EXIT=0$ +^SIGNAL=0$ +assertion at file Test.java line 23 .*: SUCCESS +-- +^warning: ignoring diff --git a/regression/jbmc-strings/StringConcat_StringII/test_fail.desc b/regression/jbmc-strings/StringConcat_StringII/test_fail.desc new file mode 100644 index 00000000000..f8751dbb3a3 --- /dev/null +++ b/regression/jbmc-strings/StringConcat_StringII/test_fail.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--refine-strings --string-max-length 10000 --verbosity 10 Test.class --function Test.testFail +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 38 .*: FAILURE +-- +^warning: ignoring diff --git a/regression/jbmc-strings/StringSubstring/Test.class b/regression/jbmc-strings/StringSubstring/Test.class new file mode 100644 index 00000000000..87ab45d5ca6 Binary files /dev/null and b/regression/jbmc-strings/StringSubstring/Test.class differ diff --git a/regression/jbmc-strings/StringSubstring/Test.java b/regression/jbmc-strings/StringSubstring/Test.java new file mode 100644 index 00000000000..8ae23b3290c --- /dev/null +++ b/regression/jbmc-strings/StringSubstring/Test.java @@ -0,0 +1,47 @@ +// This test uses CProverString so should be compiled with +// javac Test.java ../cprover/CProverString.java + +class Test { + public void testSuccess(String s, int start, int end) { + // Filter + if (s == null) + return; + + // Act + String sub = org.cprover.CProverString.substring(s, start, end); + + // Arrange + StringBuilder reference = new StringBuilder(); + if(start < 0) + start = 0; + for (int i = start; i < end && i < s.length(); i++) + reference.append(org.cprover.CProverString.charAt(s, i)); + + // Assert + assert sub.equals(reference.toString()); + } + + public void testFail(int i) { + // Arrange + String[] s = new String[5]; + + // Act + s[0] = org.cprover.CProverString.substring("foo", 0, 1); + s[1] = org.cprover.CProverString.substring("foo", 0, 4); + s[2] = org.cprover.CProverString.substring("foo", -1, 0); + s[3] = org.cprover.CProverString.substring("foo", -10, -1); + s[4] = org.cprover.CProverString.substring("foo", -10, 25); + + // Assert + if(i == 0) + assert !s[0].equals("f"); + if(i == 1) + assert !s[1].equals("foo"); + if(i == 2) + assert !s[2].equals(""); + if(i == 3) + assert !s[3].equals(""); + if(i == 4) + assert !s[4].equals("foo"); + } +} diff --git a/regression/jbmc-strings/StringSubstring/test.desc b/regression/jbmc-strings/StringSubstring/test.desc new file mode 100644 index 00000000000..651248f8a5c --- /dev/null +++ b/regression/jbmc-strings/StringSubstring/test.desc @@ -0,0 +1,6 @@ +CORE +Test.class +--refine-strings --unwind 10 --string-max-input-length 6 --function Test.testSuccess +^EXIT=0$ +^SIGNAL=0$ +assertion at file Test.java line 21.*: SUCCESS diff --git a/regression/jbmc-strings/StringSubstring/test_fail.desc b/regression/jbmc-strings/StringSubstring/test_fail.desc new file mode 100644 index 00000000000..aa7239263fd --- /dev/null +++ b/regression/jbmc-strings/StringSubstring/test_fail.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--refine-strings --unwind 10 --string-max-input-length 6 --function Test.testFail +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 37 .*: FAILURE +assertion at file Test.java line 39 .*: FAILURE +assertion at file Test.java line 41 .*: FAILURE +assertion at file Test.java line 43 .*: FAILURE +assertion at file Test.java line 45 .*: FAILURE diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 68e77136a15..b7a3397acb9 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -439,4 +439,7 @@ utf16_constant_array_to_java(const array_exprt &arr, std::size_t length); /// \return expression representing the minimum of two expressions exprt minimum(const exprt &a, const exprt &b); +/// \return expression representing the maximum of two expressions +exprt maximum(const exprt &a, const exprt &b); + #endif diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index fa38ac46bc1..6c258566351 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -14,22 +14,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include /// Add axioms enforcing that `res` is the concatenation of `s1` with -/// the substring of `s2` starting at index `start_index` and ending -/// at index `end_index`. -/// -/// If `start_index >= end_index`, the value returned is `s1`. -/// If `end_index > |s2|` and/or `start_index < 0`, the appended string will -/// be of length `end_index - start_index` and padded with non-deterministic -/// values. +/// the substring of `s2` starting at index `start_index'` and ending +/// at index `end_index'`. +/// Where start_index' is max(0, start_index) and end_index' is +/// max(min(end_index, s2.length), start_index') /// /// These axioms are: -/// 1. \f$end\_index > start\_index \Rightarrow |res| = |s_1| + end\_index - -/// start\_index -/// \f$ -/// 2. \f$end\_index \le start\_index \Rightarrow res = s_1 \f$ -/// 3. \f$\forall i<|s_1|. res[i]=s_1[i] \f$ -/// 4. \f$\forall i< end\_index - start\_index.\ res[i+|s_1|] -/// = s_2[start\_index+i]\f$ +/// 1. \f$|res| = |s_1| + end\_index' - start\_index' \f$ +/// 2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$ +/// 3. \f$\forall i< end\_index' - start\_index'.\ res[i+|s_1|] +/// = s_2[start\_index'+i]\f$ /// /// \param res: an array of characters expression /// \param s1: an array of characters expression @@ -44,28 +38,33 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr( const exprt &start_index, const exprt &end_index) { - binary_relation_exprt prem(end_index, ID_gt, start_index); - - exprt res_length=plus_exprt_with_overflow_check( - s1.length(), minus_exprt(end_index, start_index)); - implies_exprt a1(prem, equal_exprt(res.length(), res_length)); - lemmas.push_back(a1); - - implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length())); - lemmas.push_back(a2); + const typet &index_type = start_index.type(); + const exprt start1 = maximum(start_index, from_integer(0, index_type)); + const exprt end1 = maximum(minimum(end_index, s2.length()), start1); + + // Axiom 1. + lemmas.push_back([&] { // NOLINT + const plus_exprt res_length(s1.length(), minus_exprt(end1, start1)); + return equal_exprt(res.length(), res_length); + }()); + + // Axiom 2. + constraints.push_back([&] { // NOLINT + const symbol_exprt idx = + fresh_univ_index("QA_index_concat", res.length().type()); + return string_constraintt(idx, s1.length(), equal_exprt(s1[idx], res[idx])); + }()); + + // Axiom 3. + constraints.push_back([&] { // NOLINT + const symbol_exprt idx2 = + fresh_univ_index("QA_index_concat2", res.length().type()); + const equal_exprt res_eq( + res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]); + return string_constraintt(idx2, minus_exprt(end1, start1), res_eq); + }()); - symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type()); - string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx])); - constraints.push_back(a3); - - symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type()); - equal_exprt res_eq( - res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]); - string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq); - constraints.push_back(a4); - - // We should have a enum type for the possible error codes - return from_integer(0, res.length().type()); + return from_integer(0, get_return_code_type()); } /// Add axioms enforcing that `res` is the concatenation of `s1` with diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index a739aa18efe..efd85c8165b 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -667,3 +667,8 @@ exprt minimum(const exprt &a, const exprt &b) { return if_exprt(binary_relation_exprt(a, ID_le, b), a, b); } + +exprt maximum(const exprt &a, const exprt &b) +{ + return if_exprt(binary_relation_exprt(a, ID_le, b), b, a); +} diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index e4df62603fd..a5b01005c7b 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -98,16 +98,14 @@ exprt string_constraint_generatort::add_axioms_for_substring( } /// Add axioms ensuring that `res` corresponds to the substring of `str` -/// between indexes `start` and `end`. +/// between indexes `start' = max(start, 0)` and +/// `end' = max(min(end, |str|), start')`. /// /// These axioms are: -/// 1. \f$ {\tt start} < {\tt end} \Rightarrow -/// |{\tt res}| = {\tt end} - {\tt start} \f$ -/// 2. \f$ {\tt start} \ge {\tt end} \Rightarrow |{\tt res}| = 0 \f$ -/// 3. \f$ |{\tt str}| > {\tt end} \f$ -/// 4. \f$ \forall i<|{\tt str}|.\ {\tt res}[i]={\tt str}[{\tt start}+i] \f$ -/// \todo Should return code different from 0 if `|str| <= |end|` instead of -/// adding constraint 3. +/// 1. \f$ |{\tt res}| = end' - start' \f$ +/// 2. \f$ \forall i<|{\tt res}|.\ {\tt res}[i]={\tt str}[{\tt start'}+i] \f$ +/// \todo Should return code different from 0 if `start' != start` or +/// `end' != end` /// \param res: array of characters expression /// \param str: array of characters expression /// \param start: integer expression @@ -123,26 +121,19 @@ exprt string_constraint_generatort::add_axioms_for_substring( PRECONDITION(start.type()==index_type); PRECONDITION(end.type()==index_type); - // We add axioms: + const exprt start1 = maximum(start, from_integer(0, start.type())); + const exprt end1 = maximum(minimum(end, str.length()), start1); - implies_exprt a1( - binary_relation_exprt(start, ID_lt, end), - res.axiom_for_has_length(minus_exprt(end, start))); - lemmas.push_back(a1); + // Axiom 1. + lemmas.push_back(equal_exprt(res.length(), minus_exprt(end1, start1))); - exprt is_empty=res.axiom_for_has_length(from_integer(0, index_type)); - implies_exprt a2(binary_relation_exprt(start, ID_ge, end), is_empty); - lemmas.push_back(a2); + // Axiom 2. + constraints.push_back([&] { // NOLINT + const symbol_exprt idx = fresh_univ_index("QA_index_substring", index_type); + return string_constraintt( + idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start1, idx)])); + }()); - // Warning: check what to do if the string is not long enough - lemmas.push_back(str.axiom_for_length_ge(end)); - - symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type); - string_constraintt a4(idx, - res.length(), - equal_exprt(res[idx], - str[plus_exprt(start, idx)])); - constraints.push_back(a4); return from_integer(0, signedbv_typet(32)); } diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 236847659a0..c9071509452 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -292,17 +292,19 @@ std::vector string_concatenation_builtin_functiont::eval( const std::vector &input2_value, const std::vector &args_value) const { - const std::size_t start_index = - args_value.size() > 0 && args_value[0] > 0 ? args_value[0].to_ulong() : 0; - const std::size_t end_index = args_value.size() > 1 && args_value[1] > 0 - ? args_value[1].to_ulong() - : input2_value.size(); + const auto start_index = + args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0); + const mp_integer input2_size(input2_value.size()); + const auto end_index = + args_value.size() > 1 + ? std::max(std::min(args_value[1], input2_size), start_index) + : input2_size; std::vector result(input1_value); result.insert( result.end(), - input2_value.begin() + start_index, - input2_value.begin() + end_index); + input2_value.begin() + numeric_cast_v(start_index), + input2_value.begin() + numeric_cast_v(end_index)); return result; } @@ -322,18 +324,22 @@ std::vector string_insertion_builtin_functiont::eval( const std::vector &args_value) const { PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3); - const std::size_t &offset = numeric_cast_v(args_value[0]); - const std::size_t &start = - args_value.size() > 1 ? numeric_cast_v(args_value[1]) : 0; - const std::size_t &end = args_value.size() > 2 - ? numeric_cast_v(args_value[2]) - : input2_value.size(); + const auto offset = std::max(args_value[0], mp_integer(0)); + const auto start = args_value.size() > 1 + ? std::max(args_value[1], mp_integer(0)) + : mp_integer(0); + + const mp_integer input2_size(input2_value.size()); + const auto end = + args_value.size() > 2 + ? std::max(std::min(args_value[2], input2_size), mp_integer(0)) + : input2_size; std::vector result(input1_value); result.insert( - result.begin() + offset, - input2_value.begin() + start, - input2_value.end() + end); + result.begin() + numeric_cast_v(offset), + input2_value.begin() + numeric_cast_v(start), + input2_value.begin() + numeric_cast_v(end)); return result; }