From c1f4db15f70845095b0cca9b88afd431bd3099f2 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Tue, 1 Aug 2017 15:32:01 +0100 Subject: [PATCH 1/2] Refactoring in string_refinementt::set_to() Move invariant checks to top of function. --- src/solvers/refinement/string_refinement.cpp | 84 ++++++++------------ 1 file changed, 35 insertions(+), 49 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 1c876567a2c..f99e3064b2a 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -415,52 +415,45 @@ void string_refinementt::concretize_lengths() /// \par parameters: an expression and the value to set it to void string_refinementt::set_to(const exprt &expr, bool value) { - INVARIANT( - equality_propagation, - string_refinement_invariantt("set_to should only be called when equality " - "propagation is enabled")); + PRECONDITION(expr.type().id()==ID_bool); + PRECONDITION(equality_propagation); if(expr.id()==ID_equal) { equal_exprt eq_expr=to_equal_expr(expr); + const exprt &lhs=eq_expr.lhs(); + const exprt &rhs=eq_expr.rhs(); - if(eq_expr.lhs().type()!=eq_expr.rhs().type()) + // The assignment of a string equality to false is not supported. + PRECONDITION(value || !is_char_array(rhs.type())); + PRECONDITION(value || + !refined_string_typet::is_refined_string_type(rhs.type())); + + if(lhs.id()!=ID_symbol) { - warning() << "ignoring " << from_expr(ns, "", expr) - << " [inconsistent types]" << eom; - debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom; - debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom; + warning() << "ignoring " << from_expr(ns, "", expr) << eom; return; } - if(expr.type().id()!=ID_bool) + if(lhs.type()!=rhs.type()) { - error() << "string_refinementt::set_to got non-boolean operand: " - << expr.pretty() << eom; - INVARIANT( - false, - string_refinement_invariantt("set_to should only be called with exprs " - "of type bool")); + warning() << "ignoring " << from_expr(ns, "", expr) + << " [inconsistent types]" << eom; + debug() << "lhs has type: " << lhs.type().pretty(12) << eom; + debug() << "rhs has type: " << rhs.type().pretty(12) << eom; + return; } // Preprocessing to remove function applications. - const exprt &lhs=eq_expr.lhs(); debug() << "(sr::set_to) " << from_expr(ns, "", lhs) - << " = " << from_expr(ns, "", eq_expr.rhs()) << eom; + << " = " << from_expr(ns, "", rhs) << eom; - // TODO: See if this happens at all. - if(lhs.id()!=ID_symbol) + const exprt subst_rhs=substitute_function_applications(rhs); + if(lhs.type()!=subst_rhs.type()) { - warning() << "ignoring " << from_expr(ns, "", expr) << eom; - return; - } - - exprt subst_rhs=substitute_function_applications(eq_expr.rhs()); - if(eq_expr.lhs().type()!=subst_rhs.type()) - { - if(eq_expr.lhs().type().id() != ID_array || - subst_rhs.type().id() != ID_array || - eq_expr.lhs().type().subtype() != subst_rhs.type().subtype()) + if(lhs.type().id()!=ID_array || + subst_rhs.type().id()!=ID_array || + lhs.type().subtype()!=subst_rhs.type().subtype()) { warning() << "ignoring " << from_expr(ns, "", expr) << " [inconsistent types after substitution]" << eom; @@ -473,29 +466,22 @@ void string_refinementt::set_to(const exprt &expr, bool value) } } - if(value) - { - if(!add_axioms_for_string_assigns(lhs, subst_rhs)) - return; - } - else - { - // TODO: Something should also be done if value is false. - INVARIANT( - !is_char_array(eq_expr.rhs().type()), - string_refinement_invariantt("set_to cannot set a char_array")); - INVARIANT( - !refined_string_typet::is_refined_string_type(eq_expr.rhs().type()), - string_refinement_invariantt("set_to cannot set a refined_string")); - } + if(value && !add_axioms_for_string_assigns(lhs, subst_rhs)) + return; - non_string_axioms.push_back(std::make_pair(equal_exprt(lhs, subst_rhs), - value)); + // Push the substituted equality to the list of axioms to be given to + // supert::set_to. + non_string_axioms.push_back( + std::make_pair(equal_exprt(lhs, subst_rhs), value)); } - // We keep a list of the axioms to give to supert::set_to in order to - // substitute the symbols in dec_solve(). + // Push the unmodified equality to the list of axioms to be given to + // supert::set_to. else + { + // TODO: Verify that the expression contains no string. + // This will be easy once exprt iterators will have been implemented. non_string_axioms.push_back(std::make_pair(expr, value)); + } } /// use a refinement loop to instantiate universal axioms, call the sat solver, From 6ec155b80bad1467873646b06c4e3595e1236059 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Tue, 1 Aug 2017 16:13:34 +0100 Subject: [PATCH 2/2] Call supert::set_to on non-symbol lhs When string_refinementt::set_to() is called on an equality where the lhs is not a symbol, we must call supert::set_to(). We also assert that the equality is not of refined string type. --- src/solvers/refinement/string_refinement.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index f99e3064b2a..bddd6640672 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -429,9 +429,14 @@ void string_refinementt::set_to(const exprt &expr, bool value) PRECONDITION(value || !refined_string_typet::is_refined_string_type(rhs.type())); + PRECONDITION(lhs.id()==ID_symbol || !is_char_array(rhs.type())); + PRECONDITION(lhs.id()==ID_symbol || + !refined_string_typet::is_refined_string_type(rhs.type())); + + // If lhs is not a symbol, let supert::set_to() handle it. if(lhs.id()!=ID_symbol) { - warning() << "ignoring " << from_expr(ns, "", expr) << eom; + non_string_axioms.push_back(std::make_pair(expr, value)); return; }