From 9437fa07195b135ce47bb9071c57f4a41b2dc431 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 27 Nov 2017 09:33:23 +0000 Subject: [PATCH 1/4] Fix special case of empty string in (last)IndexOf The result should be length for lastIndexOf and 0 for indexOf. --- .../string_constraint_generator_indexof.cpp | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index edf532751d1..03f5efe579b 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -80,6 +80,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of( /// `haystack` of the first occurrence of `needle` starting the search at /// `from_index`, or `-1` if needle does not occur at or after position /// `from_index`. +/// If needle is an empty string then the result is `from_index`. /// /// These axioms are: /// 1. \f$ contains \Rightarrow {\tt from\_index} \le \tt{index} @@ -93,6 +94,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of( /// 5. \f$ \forall n \in [{\tt from\_index},|{\tt haystack}|-|{\tt needle}|] /// .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) /// .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$ +/// 6. \f$ |{\tt needle}| = 0 \Rightarrow \tt{index} = from_index \f$ /// \param haystack: an array of character expression /// \param needle: an array of character expression /// \param from_index: an integer expression @@ -152,6 +154,11 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( needle); axioms.push_back(a5); + const implies_exprt a6( + equal_exprt(needle.length(), from_integer(0, index_type)), + equal_exprt(offset, from_index)); + axioms.push_back(a6); + return offset; } @@ -159,6 +166,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( /// the last occurrence of needle starting the search backward at from_index (ie /// the index is smaller or equal to from_index), or -1 if needle does not occur /// before from_index. +/// If `needle` is the empty string, the result is `from_index`. /// /// These axioms are: /// 1. \f$ contains \Rightarrow -1 \le {\tt index} @@ -178,6 +186,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string( /// .\ \lnot contains \Rightarrow /// (\exists m \in [0,|{\tt needle}|) /// .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$ +/// 6. \f$ |{\tt needle}| = 0 \Rightarrow index = from_index \f$ /// \param haystack: an array of characters expression /// \param needle: an array of characters expression /// \param from_index: integer expression @@ -238,6 +247,11 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( needle); axioms.push_back(a5); + const implies_exprt a6( + equal_exprt(needle.length(), from_integer(0, index_type)), + equal_exprt(offset, from_index)); + axioms.push_back(a6); + return offset; } @@ -384,9 +398,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( const typet &char_type = str.content().type().subtype(); PRECONDITION(f.type() == index_type); - const exprt from_index = - args.size() == 2 ? minus_exprt(str.length(), from_integer(1, index_type)) - : args[2]; + const exprt from_index = args.size() == 2 ? str.length() : args[2]; if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv) { From e1f30e18b4145097ce828a3e5c99eba7ea35e12b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 27 Nov 2017 12:12:10 +0000 Subject: [PATCH 2/4] Fix bounds in axioms for lastIndexOf(char) --- .../string_constraint_generator_indexof.cpp | 32 +++++++++++-------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 03f5efe579b..2b703065cf5 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -309,13 +309,16 @@ exprt string_constraint_generatort::add_axioms_for_index_of( /// \todo Change argument names to match add_axioms_for_last_index_of_string /// /// These axioms are : -/// 1. \f$ -1 \le {\tt index} \le {\tt from\_index} \f$ +/// 1. \f$ -1 \le {\tt index} \le {\tt from\_index} +/// \land {\tt index} < |{\tt haystack}| \f$ /// 2. \f$ {\tt index} = -1 \Leftrightarrow \lnot contains\f$ -/// 3. \f$ contains \Rightarrow ({\tt index} \le {\tt from\_index} \land -/// {\tt haystack}[i] = {\tt needle} )\f$ -/// 4. \f$ \forall n \in [{\tt index} +1, {\tt from\_index}+1) +/// 3. \f$ contains \Rightarrow +/// {\tt haystack}[{\tt index}] = {\tt needle} )\f$ +/// 4. \f$ \forall n \in [{\tt index} +1, +/// min({\tt from\_index}+1, |{\tt haystack}|)) /// .\ contains \Rightarrow {\tt haystack}[n] \ne {\tt needle} \f$ -/// 5. \f$ \forall m \in [0, {\tt from\_index}+1) +/// 5. \f$ \forall m \in [0, +/// min({\tt from\_index}+1, |{\tt haystack}|)) /// .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}\f$ /// \param str: an array of characters expression /// \param c: a character expression @@ -331,12 +334,11 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( symbol_exprt index=fresh_exist_index("last_index_of", index_type); symbol_exprt contains=fresh_boolean("contains_in_last_index_of"); - exprt index1=from_integer(1, index_type); exprt minus1=from_integer(-1, index_type); - exprt from_index_plus_one=plus_exprt_with_overflow_check(from_index, index1); and_exprt a1( binary_relation_exprt(index, ID_ge, minus1), - binary_relation_exprt(index, ID_lt, from_index_plus_one)); + binary_relation_exprt(index, ID_lt, from_index_plus_one), + binary_relation_exprt(index, ID_lt, str.length())); axioms.push_back(a1); equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1)); @@ -351,19 +353,23 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( symbol_exprt n=fresh_univ_index("QA_last_index_of1", index_type); string_constraintt a4( + const exprt index1 = from_integer(1, index_type); + const plus_exprt from_index_plus_one(from_index, index1); + const if_exprt end_index( + binary_relation_exprt(from_index_plus_one, ID_le, str.length()), + from_index_plus_one, + str.length()); + n, plus_exprt(index, index1), - from_index_plus_one, + end_index, contains, not_exprt(equal_exprt(str[n], c))); axioms.push_back(a4); symbol_exprt m=fresh_univ_index("QA_last_index_of2", index_type); string_constraintt a5( - m, - from_index_plus_one, - not_exprt(contains), - not_exprt(equal_exprt(str[m], c))); + m, end_index, not_exprt(contains), notequal_exprt(str[m], c)); axioms.push_back(a5); return index; From 707ed94a8c7bd146cb922b95b6b37d0cb30a01fb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 30 Nov 2017 12:49:25 +0000 Subject: [PATCH 3/4] Refactoring in axioms for lastIndexOf(char) Making some variable constants, use notequal_exprt and smaller similar changes. --- .../string_constraint_generator_indexof.cpp | 28 ++++++++----------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 2b703065cf5..11067029b5a 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -331,28 +331,22 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( const exprt &from_index) { const typet &index_type = str.length().type(); - symbol_exprt index=fresh_exist_index("last_index_of", index_type); - symbol_exprt contains=fresh_boolean("contains_in_last_index_of"); + const symbol_exprt index = fresh_exist_index("last_index_of", index_type); + const symbol_exprt contains = fresh_boolean("contains_in_last_index_of"); - exprt minus1=from_integer(-1, index_type); - and_exprt a1( + const exprt minus1 = from_integer(-1, index_type); + const and_exprt a1( binary_relation_exprt(index, ID_ge, minus1), - binary_relation_exprt(index, ID_lt, from_index_plus_one), + binary_relation_exprt(index, ID_le, from_index), binary_relation_exprt(index, ID_lt, str.length())); axioms.push_back(a1); - equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1)); + const notequal_exprt a2(contains, equal_exprt(index, minus1)); axioms.push_back(a2); - implies_exprt a3( - contains, - and_exprt( - binary_relation_exprt(from_index, ID_ge, index), - equal_exprt(str[index], c))); + const implies_exprt a3(contains, equal_exprt(str[index], c)); axioms.push_back(a3); - symbol_exprt n=fresh_univ_index("QA_last_index_of1", index_type); - string_constraintt a4( const exprt index1 = from_integer(1, index_type); const plus_exprt from_index_plus_one(from_index, index1); const if_exprt end_index( @@ -360,15 +354,17 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of( from_index_plus_one, str.length()); + const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type); + const string_constraintt a4( n, plus_exprt(index, index1), end_index, contains, - not_exprt(equal_exprt(str[n], c))); + notequal_exprt(str[n], c)); axioms.push_back(a4); - symbol_exprt m=fresh_univ_index("QA_last_index_of2", index_type); - string_constraintt a5( + const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type); + const string_constraintt a5( m, end_index, not_exprt(contains), notequal_exprt(str[m], c)); axioms.push_back(a5); From 9ebdc8896641c1dc6195795fe084ed9bd3ea28a1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 27 Nov 2017 09:34:42 +0000 Subject: [PATCH 4/4] Test for String.lastIndexOf with empty argument --- .../jbmc-strings/StringLastIndexOf/Test.class | Bin 0 -> 968 bytes .../jbmc-strings/StringLastIndexOf/Test.java | 24 ++++++++++++++++++ .../jbmc-strings/StringLastIndexOf/test.desc | 9 +++++++ 3 files changed, 33 insertions(+) create mode 100644 regression/jbmc-strings/StringLastIndexOf/Test.class create mode 100644 regression/jbmc-strings/StringLastIndexOf/Test.java create mode 100644 regression/jbmc-strings/StringLastIndexOf/test.desc diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.class b/regression/jbmc-strings/StringLastIndexOf/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..609cc4f33481416a6f1774684d1197b0a3874146 GIT binary patch literal 968 zcmZvaOHUI~6vzL!o$0jGDTVSB85BhAOAtYXN{pmx(gY>3#6%V*)9Gy)C^I@UH7@)H zF5PvZ>~NtbK2j1*bjQLEWjuGJZ3ryp%)RIFKll9Z{qy(7F93@us7PW`#RXgxW-5jR zrWIULA!9O%nJ6v`{}tiCDpqM>G77RPa>y&V#t^Hy&R)r`@>dM3#4tExcpi6s%dx$C zmS?F(8U>3bRDx2x$ekG%RCD8isho@caPYMvYC2%>TAl9#TntD71F1wCeJv=`0i^IZNWI1#m_kHGNV_YzP6X%D F{{fgnyxaf) literal 0 HcmV?d00001 diff --git a/regression/jbmc-strings/StringLastIndexOf/Test.java b/regression/jbmc-strings/StringLastIndexOf/Test.java new file mode 100644 index 00000000000..38436b885bf --- /dev/null +++ b/regression/jbmc-strings/StringLastIndexOf/Test.java @@ -0,0 +1,24 @@ +public class Test { + int fromIndex; + + public void check(String input_String1, String input_String2, int i) { + if(input_String1 != null && input_String2 != null) { + if (i == 0) { + // The last occurrence of the empty string "" is considered to + // occur at the index value this.length() + int lio = input_String1.lastIndexOf(input_String2); + if (input_String2.length() == 0) + assert lio == input_String1.length(); + } else if (i == 1) { + // Contradiction with the previous condition (should fail). + assert "foo".lastIndexOf("") != 3; + } else if (i == 2 && input_String2.length() > 0) { + int lio = input_String1.lastIndexOf(input_String2.charAt(0), fromIndex); + if (input_String2.length() == 0) + assert lio == fromIndex; + } else if (i == 3) { + assert "foo".lastIndexOf("", 2) != 2; + } + } + } +} diff --git a/regression/jbmc-strings/StringLastIndexOf/test.desc b/regression/jbmc-strings/StringLastIndexOf/test.desc new file mode 100644 index 00000000000..4f1852669c0 --- /dev/null +++ b/regression/jbmc-strings/StringLastIndexOf/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.check --refine-strings --string-max-length 100 +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 11 .* SUCCESS$ +assertion at file Test.java line 14 .* FAILURE$ +assertion at file Test.java line 18 .* SUCCESS$ +assertion at file Test.java line 20 .* FAILURE$