diff --git a/regression/jbmc-strings/StringContains03/Test.class b/regression/jbmc-strings/StringContains03/Test.class new file mode 100644 index 00000000000..c30a13b71bc Binary files /dev/null and b/regression/jbmc-strings/StringContains03/Test.class differ 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. 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;