From f5f122e556f5f55fbb5ad026bbbe47f1b7989a28 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Thu, 29 Jun 2017 13:46:33 +0100 Subject: [PATCH 1/2] Added lower bound in lastIndexOf Added a lower bound to the offset index in lastIndex of, should at minimum reduce the number of valid valuations by 1/2, but especially for fixed strings by much more. --- .../string_constraint_generator_indexof.cpp | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 2e3e6424c36..677262092e1 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -193,20 +193,22 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( symbol_exprt contains=fresh_boolean("contains_substring"); // We add axioms: - // a1 : contains ==> offset <= from_index && offset <= |haystack| - |needle| + // a1 : contains ==> -1 <= offset && offset <= from_index + // && offset <= |haystack| - |needle| // a2 : !contains <=> offset = -1 - // a3 : forall n:[0, needle.length[, + // a3 : forall n:[0, |needle|[, // 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]]) + // (exists m:[0,|needle|[. haystack[m+n] != needle[m]]) // a5: forall n:[0, min(from_index, |haystack| - |needle|)]. // !contains ==> - // (exists m:[0,|substring|[. haystack[m+n] != needle[m]) + // (exists m:[0,|needle|[. haystack[m+n] != needle[m]) implies_exprt a1( contains, and_exprt( + binary_relation_exprt(from_integer(-1, index_type), ID_le, offset), binary_relation_exprt( offset, ID_le, minus_exprt(haystack.length(), needle.length())), binary_relation_exprt(offset, ID_le, from_index))); @@ -255,8 +257,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( { // 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 ==> + // 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); @@ -273,6 +275,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string( or_exprt premise( not_exprt(contains), binary_relation_exprt(qvar2, ID_gt, offset)); + string_constraintt a6( qvar2, from_integer(0, index_type), From bb31bb547a9649b697eed2ae1fbe25f263347165 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Thu, 29 Jun 2017 14:18:29 +0100 Subject: [PATCH 2/2] Added regression test for lastIndexOf Added regression (smoke test) for usage of long strings with lastIndexOf to detect future performance degredations. --- .../java_last_index_of2/test.desc | 7 +++++++ .../java_last_index_of2/test_last_index_of2.class | Bin 0 -> 699 bytes .../java_last_index_of2/test_last_index_of2.java | 8 ++++++++ 3 files changed, 15 insertions(+) create mode 100644 regression/strings-smoke-tests/java_last_index_of2/test.desc create mode 100644 regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.class create mode 100644 regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.java diff --git a/regression/strings-smoke-tests/java_last_index_of2/test.desc b/regression/strings-smoke-tests/java_last_index_of2/test.desc new file mode 100644 index 00000000000..5348cbe7fce --- /dev/null +++ b/regression/strings-smoke-tests/java_last_index_of2/test.desc @@ -0,0 +1,7 @@ +CORE +test_last_index_of2.class +--refine-strings +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.class b/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.class new file mode 100644 index 0000000000000000000000000000000000000000..9c82a7040752c9690160ca8f0b3b456e9c6f0157 GIT binary patch literal 699 zcmZuvU279T6g{(>>~1#OG)=Wl)mHnZiGl^`n?;nW5Qz36B3K{FWOov#Zf0e6R{Sk} z@zG}$T2Rn;f0KxJR?{H*a_@Ycd+xbs=KIgjUjgi*8zMwIz)B4PE(N$8;tE!MtcCE< z_Hi}DHLUyCU|8JZc`me(naUr^oDWlxFt9@gZ%-;|?lHKX?sJC9ewGM^`My-*X)zfJ z{mg>tV#1|jSn9m&AM-bSC*^9qGca1J@m*UuH!wVY^@P7J@jf;gg1tEXLmm#YLdW8< zv{Y>)a&we&3Q{HF?NK(mbK8V)NJ0?_nA0R(a0~KNwj< z{`I5R?U98uvVE$^37UvpYLT3aBFjuc7i9e**69&LdRNwL+sSCD;ymqEDKpB| zn`dAjED%kKUU|q+!vb2gw$MJ6I+WL1PX8m^6D;3qRhlcOs5+hy6?!Xm#;i#BSLQSZD>OsGY#Cyhp|T1b0R@6=X@OaH9KG_EOnv F`4?selxF|{ literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.java b/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.java new file mode 100644 index 00000000000..f533835fda4 --- /dev/null +++ b/regression/strings-smoke-tests/java_last_index_of2/test_last_index_of2.java @@ -0,0 +1,8 @@ +public class test_last_index_of2 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + assert(letters.lastIndexOf("diffblue", 25)==-1); + } +}