From 8495451a9fa0fe337f0d89d9673b54a62a91868a Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Fri, 30 Jun 2017 10:43:27 +0100 Subject: [PATCH 1/2] For contains, added bounds for substring index in !contains case Previously, the startpos variable (the index at which the substring occurs) was only bound properly when the substring was contained in the string being searched. Hence, in the case where the substring was not contained, the notdet string would become enourmous, and during evaluation would cause out of memory errors. Now with startpos constrained, the solver does not attempt these enourmous strings. --- .../string_constraint_generator_testing.cpp | 32 +++++++++++-------- 1 file changed, 19 insertions(+), 13 deletions(-) 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()); } From 939fb876622b320ef4ae2d6a0239912fee4ecc96 Mon Sep 17 00:00:00 2001 From: Jesse Sigal Date: Mon, 3 Jul 2017 11:44:12 +0100 Subject: [PATCH 2/2] Added regression tests based on originating test-gen tests The relevant tests implemented in diffblue/test-gen/pull/479 (StringContains3 and StringContains4) for test-gen have been adapted and added as StringContains01 and StringContains02 resp. They have been marked as future in accordance to the standard for other tests. A contains smoke test already exists and is active, which was extended. --- .../strings-smoke-tests/java_contains/test.desc | 6 +++++- .../java_contains/test_contains.class | Bin 689 -> 825 bytes .../java_contains/test_contains.java | 9 ++++++--- regression/strings/StringContains01/test.class | Bin 0 -> 618 bytes regression/strings/StringContains01/test.desc | 6 ++++++ regression/strings/StringContains01/test.java | 8 ++++++++ regression/strings/StringContains02/test.class | Bin 0 -> 606 bytes regression/strings/StringContains02/test.desc | 6 ++++++ regression/strings/StringContains02/test.java | 7 +++++++ 9 files changed, 38 insertions(+), 4 deletions(-) create mode 100644 regression/strings/StringContains01/test.class create mode 100644 regression/strings/StringContains01/test.desc create mode 100644 regression/strings/StringContains01/test.java create mode 100644 regression/strings/StringContains02/test.class create mode 100644 regression/strings/StringContains02/test.desc create mode 100644 regression/strings/StringContains02/test.java 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 989f5f04279074c7c827f6aec6cb3100ff201b36..078a8565a353a343b0fb50fbfaac5235f1df0516 100644 GIT binary patch literal 825 zcmZ8eU2hUW6g>kAyDUpfm$E`Xto;z7l%h$WEHO4{6BAk=FedFwv%8FRE8W%I#W(#Q z@@(R>nm}R`efQDdV;b+QrAU*>%-lQo+>>iWpWD+)=Qa zf`&B_uglm_k;0M)?#d{sxQDWg3PWzg3KJT`b{giOGh}bJCRTfvEnW?Vm}S#uS{i1N z)v$>wLt%p08w-5u`<}013pJuOHA}{}hC1#~O?qyfaXTcsV@3>%|BGy%ntq$V?Q_@W zyA|PBkGtLQG;-`2Sv8^1?2*e1Mu!KE&pX$Q$eXZF4`lH%R_VKD=s#JuAcW8@4kq-| zo}*})PDW>9a|HH96k?wCWRzs|y?GdP7p1=mnxON;1!6~fd<3bbCl2)F;aA85ak zCF2@GKo_lat)-hPqJT8_C1NeMO6l*OO#|3{;m8UROn_9qIhk^PNW%_)3qTo1IW^6 YNbzrwCnLwUh?WV&w8z4{g^1DOU(~gs!~g&Q delta 454 zcmY*VO-lk%6g_Xo@s0CQGh>-)_MN5{LfA5>wk9oX<0{?^BAQs_(4tL0pq03D)3UV% zN(r^^M@e_Agy3=R=Q;P@_ZA)~M_-fo4**5%YcP@ENUB)TAR(nvu#Fv#boaDmn-yPpS7mW?A>3At_}yXQ(1OiiHN~AMv_!jJsQ9;ycAY^!aXkYT zG7OUI5eV179Oez|BHK%_WS+tFYaRd6yKeiU(e7~M4CJx*Pww1p);z!anCR76w)eyi z9&}nBU{*X(BTohqU=unNrN}a}N^S%;2pSP33{R7cj#`+tdPJ3}mKj5;I`RmilB1kC z;qnW3AJJTX2(=G=j7W6^?K2RQ5WOc8gF>i4BV7}m#;Zuv?=4bx4s3!nN9^ZOWob6C lINbuU9eoI+4<33(NPY$X)h7DiqJfkG$v6(qiBlk9`5ST;KIs4e 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 0000000000000000000000000000000000000000..ce12a0ee4702ada48f472f2a0f9293bb9faf9f38 GIT binary patch literal 618 zcmY*WOHUgy5dJ2c#L2RdkQ7Lu(9+WKs6;N@KnRqAdPv(ts!HYNY%FRTcERiLWAX=j zE=VAOMDP7g2r*tBDY7&k+cV!|{O|Vi8o(MBeH1ZOK&=RYx{qnh2)y)>!<4|Rk2$;& zculA-$Rtt5>NrY1>O^*Ws!O0fLViO>+HMlOrRDF0Y%}gELaC)A^`(Ep-5!Mo&ijjkYy9+Fy5lqirk0U!UbsS}rh8C~Sni2W-C`_f4pFwL>aemDp8> z5+J}RGs{jGz{d!;1$cwEgxZi~`%(CgF|lDGu3cauz&pGrl!ujHI|nMX&#vwjvX(H8 zEE`A&Gygki{*W7tcWCs|z zLhi=}@_$`_ChZ?%8V2QiD!ENIQ#i2f!t8_}lRw~D zt%548(z`#(vS$T?m+qeK*RNmq{QmR(CxC6NhNz-hg+MDnJH!lT1?EEdXbLE?h{R z5~kM<&g8Y+N@RMv)wM>ar#r51ylZ8A{$5_*!Gqm6xg!p{*}%kVUptzrRk_`C6cHkf zM+h-S@ZYH<$pjW6EaC;BJ(}_6UiVvLGQ&C?fxuFPWvmeDBjjQ4OvU!U)IWiQAkI?D z`g6kE;{`gOr0J@wfl6bwv(DG3jp#ZFpN!D#t6Uq^f6&2;+5s2%UMH+p@CN`?Z@W!6 zDuLW$Y@hIJo;|VmH*P^+91u0Ol_JU4KphhtJLpSzMYjDF-Vjq8jnWOuLyY}^|M3=; zU#{CLx