diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index 87e117d7021..699b28f5cc0 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -37,9 +37,6 @@ struct string_constraintst final std::vector existential; std::vector universal; std::vector not_contains; - - /// Clear all constraints - void clear(); }; void merge(string_constraintst &result, string_constraintst other); @@ -60,23 +57,23 @@ class string_constraint_generatort final array_poolt array_pool; - string_constraintst constraints; - const namespacet ns; /// Associate array to pointer, and array to length /// \return an expression if the given function application is one of /// associate pointer and associate length - optionalt - make_array_pointer_association(const function_application_exprt &expr); + optionalt make_array_pointer_association( + const exprt &return_code, + const function_application_exprt &expr); private: - exprt associate_array_to_pointer(const function_application_exprt &f); - - exprt associate_length_to_array(const function_application_exprt &f); + exprt associate_array_to_pointer( + const exprt &return_code, + const function_application_exprt &f); - // MEMBERS - const messaget message; + exprt associate_length_to_array( + const exprt &return_code, + const function_application_exprt &f); }; // Type used by primitives to signal errors diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index b83fea17948..34443e33635 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -55,9 +55,12 @@ exprt sum_overflows(const plus_exprt &sum) /// Insert in `array_pool` a binding from `ptr` to `arr`. If the length of `arr` /// is infinite, a new integer symbol is created and stored in `array_pool`. /// This also adds the default axioms for `arr`. +/// \param return_code: expression which is assigned the result of the function /// \param f: a function application with argument a character array `arr` and /// a character pointer `ptr`. +/// \return a constraint exprt string_constraint_generatort::associate_array_to_pointer( + const exprt &return_code, const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); @@ -71,15 +74,17 @@ exprt string_constraint_generatort::associate_array_to_pointer( const exprt &pointer_expr = f.arguments()[1]; array_pool.insert(simplify_expr(pointer_expr, ns), array_expr); // created_strings.emplace(to_array_string_expr(array_expr)); - return from_integer(0, f.type()); + return equal_exprt{return_code, from_integer(0, f.type())}; } /// Associate an integer length to a char array. /// This adds an axiom ensuring that `arr.length` and `length` are equal. +/// \param return_code: expression which is assigned the result of the function /// \param f: a function application with argument a character array `arr` and /// an integer `length`. -/// \return integer expression equal to 0 +/// \return a constraint exprt string_constraint_generatort::associate_length_to_array( + const exprt &return_code, const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); @@ -87,15 +92,8 @@ exprt string_constraint_generatort::associate_length_to_array( const exprt &new_length = f.arguments()[1]; const auto &length = array_pool.get_or_create_length(array_expr); - constraints.existential.push_back(equal_exprt(length, new_length)); - return from_integer(0, f.type()); -} - -void string_constraintst::clear() -{ - existential.clear(); - universal.clear(); - not_contains.clear(); + return and_exprt{equal_exprt{return_code, from_integer(0, f.type())}, + equal_exprt(length, new_length)}; } /// Merge two sets of constraints by appending to the first one @@ -200,13 +198,14 @@ static irep_idt get_function_name(const function_application_exprt &expr) } optionalt string_constraint_generatort::make_array_pointer_association( + const exprt &return_code, const function_application_exprt &expr) { const irep_idt &id = get_function_name(expr); if(id == ID_cprover_associate_array_to_pointer_func) - return associate_array_to_pointer(expr); + return associate_array_to_pointer(return_code, expr); else if(id == ID_cprover_associate_length_to_array_func) - return associate_length_to_array(expr); + return associate_length_to_array(return_code, expr); return {}; } diff --git a/src/solvers/strings/string_dependencies.cpp b/src/solvers/strings/string_dependencies.cpp index 85323e3c20d..7caa62086c9 100644 --- a/src/solvers/strings/string_dependencies.cpp +++ b/src/solvers/strings/string_dependencies.cpp @@ -328,8 +328,8 @@ void string_dependenciest::output_dot(std::ostream &stream) const stream << '}' << std::endl; } -void string_dependenciest::add_constraints( - string_constraint_generatort &generator) +string_constraintst +string_dependenciest::add_constraints(string_constraint_generatort &generator) { std::unordered_set test_dependencies; for(const auto &builtin : builtin_function_nodes) @@ -346,16 +346,16 @@ void string_dependenciest::add_constraints( for_each_successor(n, f); }); + string_constraintst constraints; for(const auto &node : builtin_function_nodes) { if(test_dependencies.count(nodet(node))) { const auto &builtin = builtin_function_nodes[node.index]; - string_constraintst constraints = builtin.data->constraints(generator); - merge(generator.constraints, std::move(constraints)); + merge(constraints, builtin.data->constraints(generator)); } else - generator.constraints.existential.push_back( - node.data->length_constraint()); + constraints.existential.push_back(node.data->length_constraint()); } + return constraints; } diff --git a/src/solvers/strings/string_dependencies.h b/src/solvers/strings/string_dependencies.h index 46c96127859..1448a985035 100644 --- a/src/solvers/strings/string_dependencies.h +++ b/src/solvers/strings/string_dependencies.h @@ -14,6 +14,8 @@ Author: Diffblue Ltd. #include +#include + #include "string_builtin_function.h" /// Keep track of dependencies between strings. @@ -114,7 +116,8 @@ class string_dependenciest /// For all builtin call on which a test (or an unsupported buitin) /// result depends, add the corresponding constraints. For the other builtin /// only add constraints on the length. - void add_constraints(string_constraint_generatort &generatort); + NODISCARD string_constraintst + add_constraints(string_constraint_generatort &generatort); /// Clear the content of the dependency graph void clear(); diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index e987f2fa281..421e05cac9d 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -251,8 +251,13 @@ static void make_char_array_pointer_associations( const auto fun_app = expr_try_dynamic_cast(eq.rhs())) { - if(const auto result = generator.make_array_pointer_association(*fun_app)) - eq.rhs() = *result; + const auto new_equation = + generator.make_array_pointer_association(eq.lhs(), *fun_app); + if(new_equation) + { + eq = + equal_exprt{from_integer(true, new_equation->type()), *new_equation}; + } } } } @@ -645,9 +650,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() } } - // Generator is also used by get, so we have to use it as a class member - // but we make sure it is cleared at each `dec_solve` call. - generator.constraints.clear(); + // Constraints start clear at each `dec_solve` call. + string_constraintst constraints; make_char_array_pointer_associations(generator, equations); #ifdef DEBUG @@ -677,7 +681,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() #endif log.debug() << "dec_solve: add constraints" << messaget::eom; - dependencies.add_constraints(generator); + merge(constraints, dependencies.add_constraints(generator)); #ifdef DEBUG output_equations(log.debug(), equations); @@ -702,8 +706,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() } std::transform( - generator.constraints.universal.begin(), - generator.constraints.universal.end(), + constraints.universal.begin(), + constraints.universal.end(), std::back_inserter(axioms.universal), [&](string_constraintt constraint) { constraint.replace_expr(symbol_resolve); @@ -715,8 +719,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() }); std::transform( - generator.constraints.not_contains.begin(), - generator.constraints.not_contains.end(), + constraints.not_contains.begin(), + constraints.not_contains.end(), std::back_inserter(axioms.not_contains), [&](string_not_contains_constraintt axiom) { replace(symbol_resolve, axiom); @@ -737,7 +741,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() nc_axiom, generator.fresh_symbol("not_contains_witness", witness_type)); } - for(const exprt &lemma : generator.constraints.existential) + for(const exprt &lemma : constraints.existential) { add_lemma(substitute_array_access(lemma, generator.fresh_symbol, true)); }