From 9e73699019733c01d552a504c1b30764c826ff91 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 9 May 2018 15:43:39 +0100 Subject: [PATCH 1/2] Refactor negation of not contains constraints This now uses get. Get is called on index_exprt which avoids concretizing array_string_exprt, which can potentially represent long strings. This makes string_refinement more efficient in programs with not_contains_constraints, when the underlying solver can come up with very long strings. --- src/solvers/refinement/string_refinement.cpp | 92 ++++++-------------- 1 file changed, 28 insertions(+), 64 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 4fe87dfc7cb..24c94ebd408 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1202,51 +1202,38 @@ exprt substitute_array_access( /// have been replaced by their valuation in the current model. /// \pre Symbols other than the universal variable should have been replaced by /// their valuation in the current model. -/// \param axiom: the not_contains constraint to add the negation of +/// \param constraint: the not_contains constraint to add the negation of /// \param univ_var: the universal variable for the negation of the axiom +/// \param get: valuation function, the result should have been simplified /// \return: the negation of the axiom under the current evaluation static exprt negation_of_not_contains_constraint( - const string_not_contains_constraintt &axiom, - const symbol_exprt &univ_var) + const string_not_contains_constraintt &constraint, + const symbol_exprt &univ_var, + const std::function &get) { // If the for all is vacuously true, the negation is false. - const exprt &lbu=axiom.univ_lower_bound(); - const exprt &ubu=axiom.univ_upper_bound(); - if(lbu.id()==ID_constant && ubu.id()==ID_constant) - { - const auto lb_int = numeric_cast(lbu); - const auto ub_int = numeric_cast(ubu); - if(!lb_int || !ub_int || *ub_int<=*lb_int) - return false_exprt(); - } - - const auto lbe = numeric_cast_v(axiom.exists_lower_bound()); - const auto ube = numeric_cast_v(axiom.exists_upper_bound()); - - // If the premise is false, the implication is trivially true, so the - // negation is false. - if(axiom.premise()==false_exprt()) - return false_exprt(); - - and_exprt univ_bounds( - binary_relation_exprt(lbu, ID_le, univ_var), - binary_relation_exprt(ubu, ID_gt, univ_var)); + const auto lbe = + numeric_cast_v(get(constraint.exists_lower_bound())); + const auto ube = + numeric_cast_v(get(constraint.exists_upper_bound())); + const auto univ_bounds = and_exprt( + binary_relation_exprt(get(constraint.univ_lower_bound()), ID_le, univ_var), + binary_relation_exprt(get(constraint.univ_upper_bound()), ID_gt, univ_var)); // The negated existential becomes an universal, and this is the unrolling of // that universal quantifier. std::vector conjuncts; + conjuncts.reserve(numeric_cast_v(ube - lbe)); for(mp_integer i=lbe; i> check_axioms( for(std::size_t i = 0; i < axioms.not_contains.size(); i++) { const string_not_contains_constraintt &nc_axiom=axioms.not_contains[i]; - const exprt &univ_bound_inf=nc_axiom.univ_lower_bound(); - const exprt &univ_bound_sup=nc_axiom.univ_upper_bound(); - const exprt &prem=nc_axiom.premise(); - const exprt &exists_bound_inf=nc_axiom.exists_lower_bound(); - const exprt &exists_bound_sup=nc_axiom.exists_upper_bound(); - const array_string_exprt &s0 = nc_axiom.s0(); - const array_string_exprt &s1 = nc_axiom.s1(); - - symbol_exprt univ_var=generator.fresh_univ_index( + const symbol_exprt univ_var = generator.fresh_univ_index( "not_contains_univ_var", nc_axiom.s0().length().type()); - string_not_contains_constraintt nc_axiom_in_model( - get(univ_bound_inf), - get(univ_bound_sup), - get(prem), - get(exists_bound_inf), - get(exists_bound_sup), - to_array_string_expr(get(s0)), - to_array_string_expr(get(s1))); - - // necessary so that expressions such as `1 + (3 - (TRUE ? 0 : 0))` do not - // appear in bounds - nc_axiom_in_model = - to_string_not_contains_constraint(simplify_expr(nc_axiom_in_model, ns)); - - exprt negaxiom = - negation_of_not_contains_constraint(nc_axiom_in_model, univ_var); - - negaxiom = simplify_expr(negaxiom, ns); - const exprt with_concrete_arrays = - substitute_array_access(negaxiom, gen_symbol, true); + const exprt negated_axiom = negation_of_not_contains_constraint( + nc_axiom, univ_var, [&](const exprt &expr) { + return simplify_expr(get(expr), ns); }); stream << indent << i << ".\n"; debug_check_axioms_step( - stream, ns, nc_axiom, nc_axiom_in_model, negaxiom, with_concrete_arrays); + stream, ns, nc_axiom, nc_axiom, negated_axiom, negated_axiom); - if(const auto witness = find_counter_example(ns, ui, negaxiom, univ_var)) + if( + const auto witness = + find_counter_example(ns, ui, negated_axiom, univ_var)) { stream << indent2 << "- violated_for: " << univ_var.get_identifier() << "=" << format(*witness) << eom; From 386faa8ee58d42496a90a38cb5b2eb49d0a6af74 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 9 May 2018 16:17:46 +0100 Subject: [PATCH 2/2] Test for String.contains and very large strings This tests string refinement is able to deal with very large strings in string_not_contains_constraintt objects. --- .../jbmc-strings/StringContains03/Test.class | Bin 0 -> 779 bytes .../jbmc-strings/StringContains03/Test.java | 23 ++++++++++++++++++ .../jbmc-strings/StringContains03/test.desc | 11 +++++++++ 3 files changed, 34 insertions(+) create mode 100644 regression/jbmc-strings/StringContains03/Test.class create mode 100644 regression/jbmc-strings/StringContains03/Test.java create mode 100644 regression/jbmc-strings/StringContains03/test.desc diff --git a/regression/jbmc-strings/StringContains03/Test.class b/regression/jbmc-strings/StringContains03/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..c30a13b71bc47fa152f55afba9606bfc6f083fbb GIT binary patch literal 779 zcmZWnL2nX47<~f^yDW>)MJpCt!6E``(b`*y(V!+KwH~M@?QK{_*mm93*~P@4Vvkh3KrrODTwiRDU-gCDQDBCYGZM}LL%p%J&)@R4$Ngcu7fIJ2ZZ`ivV#xI(?i@Vj zua60gj^iCmnY~~v9r4&z#F-rtMr(@Gf{h|Wc6;o3l`y8(al^t*+)}V0sDz_HM&$Wr z5cIjUu!c6>bOS%)$q*<4%Qh8^LNks z`@$imGe@&rN!%0uFdD@Ld%|EiGxd<6e6}>*5tlvjW-NS1Y&NOT`8j*nqi!%P4n*im zF*r3z6^q7nL9N(BmHL^d*0VxMrA50Wn5q!X=P6pImC>4N9f5sPKwO|X9UoFvu!xJa zSI~Dz&;Zt3KasW*lhzbTTl+x!)TCvnr_ej)_Y@hE&&V7i`wiyq5wbsQYeKIQF>jq1 z0gXlqI*kH-zalIwk;xT`s-)B=WQkB2XnOV!ax6!nOQ()EVr#&Hotxs^A$08{wB#3L Wl>3>=iF?J8Lc+SQa$Jh9%l`n#?wg?i literal 0 HcmV?d00001 diff --git a/regression/jbmc-strings/StringContains03/Test.java b/regression/jbmc-strings/StringContains03/Test.java new file mode 100644 index 00000000000..825760356aa --- /dev/null +++ b/regression/jbmc-strings/StringContains03/Test.java @@ -0,0 +1,23 @@ +public class Test { + public static String check(String s) { + // Filter + if (s == null) { + return "Null string"; + } + if (s.length() < 16_000_000) { + return "Too short"; + } + + // Act + boolean b1 = s.contains("foobar"); + + // Filter output + if (b1) { + return "Contained"; + } + + // Assert + assert(false); + return "Unreachable"; + } +} diff --git a/regression/jbmc-strings/StringContains03/test.desc b/regression/jbmc-strings/StringContains03/test.desc new file mode 100644 index 00000000000..b2842da00f2 --- /dev/null +++ b/regression/jbmc-strings/StringContains03/test.desc @@ -0,0 +1,11 @@ +CORE +Test.class +--refine-strings --function Test.check +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +file Test.java line 20 .*: FAILURE$ +-- +-- +--string-max-length is not used on purpose, because this tests the behaviour +of string refinement on very large strings.