From 0ffd0aee2ed448f401baffc77961ece69fee6c5a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 22 Mar 2018 14:23:55 +0000 Subject: [PATCH 1/2] Replace negation of constraint by a method --- src/solvers/refinement/string_constraint.h | 5 +++ src/solvers/refinement/string_refinement.cpp | 34 +------------------- 2 files changed, 6 insertions(+), 33 deletions(-) diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index e72ead2495d..41e36ae3254 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -118,6 +118,11 @@ class string_constraintt : public exprt binary_relation_exprt(lower_bound(), ID_le, univ_var()), binary_relation_exprt(upper_bound(), ID_gt, univ_var())); } + + exprt negation() const + { + return and_exprt(univ_within_bounds(), not_exprt(body())); + } }; extern inline const string_constraintt &to_string_constraint(const exprt &expr) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 24c94ebd408..4b1eade4307 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1236,38 +1236,6 @@ static exprt negation_of_not_contains_constraint( return and_exprt(univ_bounds, get(constraint.premise()), equal_strings); } -/// Negates the constraint to be fed to a solver. The intended usage is to find -/// an assignment of the universal variable that would violate the axiom. To -/// avoid false positives, the symbols other than the universal variable should -/// 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 -/// \return: the negation of the axiom under the current evaluation -static exprt negation_of_constraint(const string_constraintt &axiom) -{ - // If the for all is vacuously true, the negation is false. - const exprt &lb=axiom.lower_bound(); - const exprt &ub=axiom.upper_bound(); - if(lb.id()==ID_constant && ub.id()==ID_constant) - { - const auto lb_int = numeric_cast(lb); - const auto ub_int = numeric_cast(ub); - if(!lb_int || !ub_int || ub_int<=lb_int) - return false_exprt(); - } - - // 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 premise(axiom.premise(), axiom.univ_within_bounds()); - and_exprt negaxiom(premise, not_exprt(axiom.body())); - - return negaxiom; -} - /// Debugging function which outputs the different steps an axiom goes through /// to be checked in check axioms. static void debug_check_axioms_step( @@ -1365,7 +1333,7 @@ static std::pair> check_axioms( const string_constraintt axiom_in_model( univ_var, get(bound_inf), get(bound_sup), get(body)); - exprt negaxiom=negation_of_constraint(axiom_in_model); + exprt negaxiom = axiom_in_model.negation(); negaxiom = simplify_expr(negaxiom, ns); stream << indent << i << ".\n"; From c6c2928272be8642862cc179b130512ba40176aa Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 22 Mar 2018 14:25:03 +0000 Subject: [PATCH 2/2] Drop inheritance from constraint on exprt There is no strong reason for making string_constraintt inherit from exprt. Getting rid of this inheritance makes usage of the class safer by preventing the application of exprt method that do not make sense for string constraints. --- .../instantiate_not_contains.cpp | 6 +- src/solvers/refinement/string_constraint.h | 100 ++++++-------- src/solvers/refinement/string_refinement.cpp | 122 +++++++----------- src/util/irep_ids.def | 1 - 4 files changed, 84 insertions(+), 145 deletions(-) diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index 7e6773e50c0..c4aa4736b42 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -206,10 +206,8 @@ SCENARIO("instantiate_not_contains", constraints.end(), axioms, [&](const std::string &accu, string_constraintt sc) { - simplify(sc, ns); - std::string s; - java_lang->from_expr(sc, s, ns); - return accu + s + "\n\n"; + simplify(sc.body, ns); + return accu + to_string(sc) + "\n\n"; }); const auto nc_contraints = generator.get_not_contains_constraints(); diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 41e36ae3254..3284faa6305 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -27,6 +27,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include +#include /// ### Universally quantified string constraint /// @@ -54,89 +55,60 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// \f$f\f$ [explicitly stated, implied]. /// /// \todo The fact that we follow this grammar is not enforced at the moment. -class string_constraintt : public exprt +class string_constraintt final { public: // String constraints are of the form - // forall univ_var in [lower_bound,upper_bound[. premise => body + // forall univ_var in [lower_bound,upper_bound[. body + symbol_exprt univ_var; + exprt lower_bound; + exprt upper_bound; + exprt body; - const exprt &premise() const - { - return op0(); - } - - const exprt &body() const - { - return op1(); - } + string_constraintt() = delete; - const symbol_exprt &univ_var() const + string_constraintt( + symbol_exprt _univ_var, + exprt lower_bound, + exprt upper_bound, + exprt body) + : univ_var(_univ_var), + lower_bound(lower_bound), + upper_bound(upper_bound), + body(body) { - return to_symbol_expr(op2()); } - const exprt &upper_bound() const - { - return op3(); - } - - const exprt &lower_bound() const + // Default bound inferior is 0 + string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body) + : string_constraintt( + univ_var, + from_integer(0, univ_var.type()), + upper_bound, + body) { - return operands()[4]; } - private: - string_constraintt(); - - public: - string_constraintt( - const symbol_exprt &_univ_var, - const exprt &bound_inf, - const exprt &bound_sup, - const exprt &body): - exprt(ID_string_constraint) + exprt univ_within_bounds() const { - copy_to_operands(true_exprt(), body); - copy_to_operands(_univ_var, bound_sup, bound_inf); + return and_exprt( + binary_relation_exprt(lower_bound, ID_le, univ_var), + binary_relation_exprt(upper_bound, ID_gt, univ_var)); } - // Default bound inferior is 0 - string_constraintt( - const symbol_exprt &_univ_var, - const exprt &bound_sup, - const exprt &body): - string_constraintt( - _univ_var, - from_integer(0, _univ_var.type()), - bound_sup, - body) - {} - - exprt univ_within_bounds() const + void replace_expr(union_find_replacet &replace_map) { - return and_exprt( - binary_relation_exprt(lower_bound(), ID_le, univ_var()), - binary_relation_exprt(upper_bound(), ID_gt, univ_var())); + replace_map.replace_expr(lower_bound); + replace_map.replace_expr(upper_bound); + replace_map.replace_expr(body); } exprt negation() const { - return and_exprt(univ_within_bounds(), not_exprt(body())); + return and_exprt(univ_within_bounds(), not_exprt(body)); } }; -extern inline const string_constraintt &to_string_constraint(const exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5); - return static_cast(expr); -} - -extern inline string_constraintt &to_string_constraint(exprt &expr) -{ - PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5); - return static_cast(expr); -} - /// Used for debug printing. /// \param [in] ns: namespace for `from_expr` /// \param [in] identifier: identifier for `from_expr` @@ -145,9 +117,9 @@ extern inline string_constraintt &to_string_constraint(exprt &expr) inline std::string to_string(const string_constraintt &expr) { std::ostringstream out; - out << "forall " << format(expr.univ_var()) << " in [" - << format(expr.lower_bound()) << ", " << format(expr.upper_bound()) - << "). " << format(expr.premise()) << " => " << format(expr.body()); + out << "forall " << format(expr.univ_var) << " in [" + << format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). " + << format(expr.body); return out.str(); } diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 4b1eade4307..cdc7f984d32 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -33,7 +33,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com static bool is_valid_string_constraint( messaget::mstreamt &stream, const namespacet &ns, - const string_constraintt &expr); + const string_constraintt &constraint); static optionalt find_counter_example( const namespacet &ns, @@ -697,7 +697,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() constraints.end(), std::back_inserter(axioms.universal), [&](string_constraintt constraint) { - symbol_resolve.replace_expr(constraint); + constraint.replace_expr(symbol_resolve); DATA_INVARIANT( is_valid_string_constraint(error(), ns, constraint), string_refinement_invariantt( @@ -1238,34 +1238,23 @@ static exprt negation_of_not_contains_constraint( /// Debugging function which outputs the different steps an axiom goes through /// to be checked in check axioms. +/// \tparam T: can be either string_constraintt or +/// string_not_contains_constraintt +template static void debug_check_axioms_step( messaget::mstreamt &stream, const namespacet &ns, - const exprt &axiom, - const exprt &axiom_in_model, + const T &axiom, + const T &axiom_in_model, const exprt &negaxiom, const exprt &with_concretized_arrays) { static const std::string indent = " "; static const std::string indent2 = " "; stream << indent2 << "- axiom:\n" << indent2 << indent; - - if(axiom.id() == ID_string_constraint) - stream << to_string(to_string_constraint(axiom)); - else if(axiom.id() == ID_string_not_contains_constraint) - stream << to_string(to_string_not_contains_constraint(axiom)); - else - stream << format(axiom); + stream << to_string(axiom); stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent; - - if(axiom_in_model.id() == ID_string_constraint) - stream << to_string(to_string_constraint(axiom_in_model)); - else if(axiom_in_model.id() == ID_string_not_contains_constraint) - stream << to_string(to_string_not_contains_constraint(axiom_in_model)); - else - stream << format(axiom_in_model); - - stream << '\n' + stream << to_string(axiom_in_model) << '\n' << indent2 << "- negated_axiom:\n" << indent2 << indent << format(negaxiom) << '\n'; stream << indent2 << "- negated_axiom_with_concretized_arrays:\n" @@ -1322,16 +1311,11 @@ static std::pair> check_axioms( for(size_t i=0; i> check_axioms( debug_check_axioms_step( stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays); - if(const auto &witness= - find_counter_example(ns, ui, with_concretized_arrays, univ_var)) + if( + const auto &witness = + find_counter_example(ns, ui, with_concretized_arrays, axiom.univ_var)) { - stream << indent2 << "- violated_for: " << univ_var.get_identifier() - << "=" << format(*witness) << eom; + stream << indent2 << "- violated_for: " << format(axiom.univ_var) << "=" + << format(*witness) << eom; violated[i]=*witness; } else @@ -1402,13 +1387,13 @@ static std::pair> check_axioms( const exprt &val=v.second; const string_constraintt &axiom=axioms.universal[v.first]; - implies_exprt instance(axiom.premise(), axiom.body()); - replace_expr(axiom.univ_var(), val, instance); + exprt instance(axiom.body); + replace_expr(axiom.univ_var, val, instance); // We are not sure the index set contains only positive numbers and_exprt bounds( axiom.univ_within_bounds(), binary_relation_exprt(from_integer(0, val.type()), ID_le, val)); - replace_expr(axiom.univ_var(), val, bounds); + replace_expr(axiom.univ_var, val, bounds); const implies_exprt counter(bounds, instance); lemmas.push_back(counter); } @@ -1766,10 +1751,10 @@ static void initial_index_set( const namespacet &ns, const string_constraintt &axiom) { - const symbol_exprt &qvar=axiom.univ_var(); - const auto &bound = axiom.upper_bound(); - auto it = axiom.body().depth_begin(); - const auto end = axiom.body().depth_end(); + const symbol_exprt &qvar = axiom.univ_var; + const auto &bound = axiom.upper_bound; + auto it = axiom.body.depth_begin(); + const auto end = axiom.body.depth_end(); while(it != end) { if(it->id() == ID_index && is_char_type(it->type())) @@ -1912,18 +1897,17 @@ static exprt instantiate( const exprt &str, const exprt &val) { - const optionalt idx = find_index(axiom.body(), str, axiom.univ_var()); + const optionalt idx = find_index(axiom.body, str, axiom.univ_var); if(!idx.has_value()) return true_exprt(); - const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, *idx); + const exprt r = compute_inverse_function(stream, axiom.univ_var, val, *idx); implies_exprt instance( and_exprt( - binary_relation_exprt(axiom.univ_var(), ID_ge, axiom.lower_bound()), - binary_relation_exprt(axiom.univ_var(), ID_lt, axiom.upper_bound()), - axiom.premise()), - axiom.body()); - replace_expr(axiom.univ_var(), r, instance); + binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound), + binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)), + axiom.body); + replace_expr(axiom.univ_var, r, instance); return instance; } @@ -2175,11 +2159,11 @@ is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var) /// \param [in] expr: The string constraint to check /// \return true if the universal variable only occurs in index expressions, /// false otherwise. -static bool universal_only_in_index(const string_constraintt &expr) +static bool universal_only_in_index(const string_constraintt &constr) { - for(auto it = expr.body().depth_begin(); it != expr.body().depth_end();) + for(auto it = constr.body.depth_begin(); it != constr.body.depth_end();) { - if(*it == expr.univ_var()) + if(*it == constr.univ_var) return false; if(it->id() == ID_index) it.next_sibling_or_parent(); @@ -2193,35 +2177,20 @@ static bool universal_only_in_index(const string_constraintt &expr) /// \related string_constraintt /// \param stream: message stream /// \param ns: namespace -/// \param [in] expr: the string constraint to check +/// \param [in] constraint: the string constraint to check /// \return whether the constraint satisfies the invariant static bool is_valid_string_constraint( messaget::mstreamt &stream, const namespacet &ns, - const string_constraintt &expr) + const string_constraintt &constraint) { const auto eom=messaget::eom; - // Condition 1: The premise cannot contain any string indices - const array_index_mapt premise_indices=gather_indices(expr.premise()); - if(!premise_indices.empty()) - { - stream << "Premise has indices: " << format(expr) << ", map: {"; - for(const auto &pair : premise_indices) - { - stream << format(pair.first) << ": {"; - for(const auto &i : pair.second) - stream << format(i) << ", "; - } - stream << "}}" << eom; - return false; - } - - const array_index_mapt body_indices=gather_indices(expr.body()); + const array_index_mapt body_indices = gather_indices(constraint.body); // Must validate for each string. Note that we have an invariant that the // second value in the pair is non-empty. for(const auto &pair : body_indices) { - // Condition 2: All indices of the same string must be the of the same form + // Condition 1: All indices of the same string must be the of the same form const exprt rep=pair.second.back(); for(size_t j=0; j