diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index ca6ff4177de..a969ad6594e 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -94,8 +94,6 @@ class string_constraint_generatort static constant_exprt constant_char(int i, const typet &char_type); - // Used by string refinement - void add_axioms_for_if_array(const exprt &lhs, const if_exprt &expr); private: // The integer with the longest string is Integer.MIN_VALUE which is -2^31, diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index d697514767c..823295777d4 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -24,7 +24,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include -#include unsigned string_constraint_generatort::next_symbol_id=1; @@ -232,6 +231,25 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string( else if(string.id()==ID_struct) { const string_exprt &s=to_string_expr(string); + INVARIANT( + s.length().id()==ID_symbol || s.length().id()==ID_constant, + "string length should be a symbol or a constant"); + irep_idt content_id=s.content().id(); + INVARIANT( + content_id==ID_symbol || content_id==ID_array || content_id==ID_if, + "string content should be a symbol, a constant array, or an if"); + if(content_id==ID_if) + { + // If the string content is an if expression, we add axioms ensuring + // the content is the same as the content in the 'true' branch when the + // condition holds and the 'false' branch otherwise. + if_exprt if_expr=to_if_expr(s.content()); + string_exprt str_true=add_axioms_for_refined_string( + string_exprt(s.length(), if_expr.true_case(), type)); + string_exprt str_false=add_axioms_for_refined_string( + string_exprt(s.length(), if_expr.false_case(), type)); + return add_axioms_for_if(if_exprt(if_expr.cond(), str_true, str_false)); + } add_default_axioms(s); return s; } @@ -267,56 +285,17 @@ string_exprt string_constraint_generatort::add_axioms_for_if( implies_exprt(expr.cond(), res.axiom_for_has_same_length_as(t))); symbol_exprt qvar=fresh_univ_index("QA_string_if_true", index_type); equal_exprt qequal(res[qvar], t[qvar]); - axioms.push_back(string_constraintt(qvar, t.length(), expr.cond(), qequal)); + string_constraintt sc1(qvar, t.length(), implies_exprt(expr.cond(), qequal)); + axioms.push_back(sc1); axioms.push_back( implies_exprt(not_exprt(expr.cond()), res.axiom_for_has_same_length_as(f))); symbol_exprt qvar2=fresh_univ_index("QA_string_if_false", index_type); equal_exprt qequal2(res[qvar2], f[qvar2]); - string_constraintt sc2(qvar2, f.length(), not_exprt(expr.cond()), qequal2); + string_constraintt sc2(qvar2, f.length(), or_exprt(expr.cond(), qequal2)); axioms.push_back(sc2); return res; } -/// Add axioms enforcing that the content of the first array is equal to -/// the true case array if the condition is true and -/// the else case array otherwise. -/// \param lhs: an expression -/// \param expr: an if expression of type array -void string_constraint_generatort::add_axioms_for_if_array( - const exprt &lhs, const if_exprt &expr) -{ - PRECONDITION(lhs.type()==expr.type()); - PRECONDITION(expr.type().id()==ID_array); - exprt t=expr.true_case(); - exprt f=expr.false_case(); - INVARIANT(t.type()==f.type(), "branches of if_exprt should have same type"); - const array_typet &type=to_array_type(t.type()); - const typet &index_type=type.size().type(); - const exprt max_length=from_integer(max_string_length, index_type); - - // We add axioms: - // a1 : forall qvar lhs[qvar] = t[qvar] - // a1 : forall qvar2 lhs[qvar] = f[qvar] - symbol_exprt qvar=fresh_univ_index("QA_array_if_true", index_type); - equal_exprt qequal(index_exprt(lhs, qvar), index_exprt(t, qvar)); - - // In case t is a constant array of fixed length is does not make sense - // to talk about indexes exceeding this length - exprt upper_bound_t= - (t.id()==ID_array)?from_integer(t.operands().size(), index_type):max_length; - string_constraintt a1(qvar, upper_bound_t, expr.cond(), qequal); - axioms.push_back(a1); - - symbol_exprt qvar2=fresh_univ_index("QA_array_if_false", index_type); - equal_exprt qequal2(index_exprt(lhs, qvar2), index_exprt(f, qvar2)); - // In case f is a constant array of fixed length is does not make sense - // to talk about indexes exceeding this length - exprt upper_bound_f= - (f.id()==ID_array)?from_integer(f.operands().size(), index_type):max_length; - string_constraintt a2(qvar2, upper_bound_f, not_exprt(expr.cond()), qequal2); - axioms.push_back(a2); -} - /// if a symbol representing a string is present in the symbol_to_string table, /// returns the corresponding string, if the symbol is not yet present, creates /// a new string with the correct type depending on whether the mode is java or diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c04f8185210..87d7f9a313c 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -117,28 +117,71 @@ void string_refinementt::add_instantiations() } } +/// List the simple expressions on which the expression depends in the +/// `symbol_resolve` map. A simple expression is either a symbol or a +/// constant array +/// \param expr: an expression +static void depends_in_symbol_map(const exprt &expr, std::vector &accu) +{ + if(expr.id()==ID_if) + { + if_exprt if_expr=to_if_expr(expr); + depends_in_symbol_map(if_expr.true_case(), accu); + depends_in_symbol_map(if_expr.false_case(), accu); + } + else if(expr.id()==ID_struct) + { + string_exprt str=to_string_expr(expr); + depends_in_symbol_map(str.content(), accu); + } + else + { + INVARIANT( + expr.id()==ID_symbol || expr.id()==ID_array || expr.id()==ID_array_of, + "leaf in symbol resolve should be a symbol or a constant array"); + accu.push_back(expr); + } +} + /// keeps a map of symbols to expressions, such as none of the mapped values /// exist as a key /// \param lhs: a symbol expression -/// \param rhs: an expression to map it to +/// \param rhs: an expression to map it to, which should be either a symbol +/// a string_exprt, an array_exprt, an array_of_exprt or an +/// if_exprt with branches of the previous kind void string_refinementt::add_symbol_to_symbol_map( const exprt &lhs, const exprt &rhs) { PRECONDITION(lhs.id()==ID_symbol); + PRECONDITION(rhs.id()==ID_symbol || + rhs.id()==ID_array || + rhs.id()==ID_array_of || + rhs.id()==ID_if || + (rhs.id()==ID_struct && + refined_string_typet::is_refined_string_type(rhs.type()))); // We insert the mapped value of the rhs, if it exists. auto it=symbol_resolve.find(rhs); const exprt &new_rhs=it!=symbol_resolve.end()?it->second:rhs; - symbol_resolve[lhs]=new_rhs; - reverse_symbol_resolve[new_rhs].push_back(lhs); - const std::list &symbols_to_update_with_new_rhs( - reverse_symbol_resolve[lhs]); - for(exprt item : symbols_to_update_with_new_rhs) + // List the leaves of new_rhs + std::vector leaves; + depends_in_symbol_map(new_rhs, leaves); + + const auto &symbols_to_update_with_new_rhs=reverse_symbol_resolve[lhs]; + + // We need to update all the symbols which depend on lhs + for(const exprt &item : symbols_to_update_with_new_rhs) + replace_expr(symbol_resolve, symbol_resolve[item]); + + // Every time a symbol at the leaves is updated we need to update lhs + // and the symbols that depend on it + for(const auto &leaf : leaves) { - symbol_resolve[item]=new_rhs; - reverse_symbol_resolve[new_rhs].push_back(item); + reverse_symbol_resolve[leaf].push_back(lhs); + for(const exprt &item : symbols_to_update_with_new_rhs) + reverse_symbol_resolve[leaf].push_back(item); } } @@ -158,9 +201,6 @@ void string_refinementt::set_char_array_equality( index_exprt arraycell(rhs, from_integer(i, index_type)); equal_exprt arrayeq(arraycell, rhs.operands()[i]); add_lemma(arrayeq, false); -#if 0 - generator.axioms.push_back(arrayeq); -#endif } } // At least for Java (as it is currently pre-processed), we need not consider @@ -205,7 +245,8 @@ bool string_refinementt::is_char_array(const typet &type) const /// add lemmas to the solver corresponding to the given equation /// \param lhs: left hand side of an equality expression /// \param rhs: right and side of the equality -/// \return false if the lemmas were added successfully, true otherwise +/// \return true if the assignemnt needs to be handled by the parent class +/// via `set_to` bool string_refinementt::add_axioms_for_string_assigns( const exprt &lhs, const exprt &rhs) { @@ -225,8 +266,8 @@ bool string_refinementt::add_axioms_for_string_assigns( } else if(rhs.id()==ID_if) { - generator.add_axioms_for_if_array(lhs, to_if_expr(rhs)); - return false; + add_symbol_to_symbol_map(lhs, rhs); + return true; } else { @@ -632,7 +673,7 @@ void string_refinementt::add_lemma( /// \return an array expression or an array_of_exprt exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const { - exprt arr_val=get_array(arr); + exprt arr_val=simplify_expr(get_array(arr), ns); exprt size_val=supert::get(size); size_val=simplify_expr(size_val, ns); typet char_type=arr.type().subtype(); @@ -1412,6 +1453,30 @@ void string_refinementt::update_index_set(const std::vector &cur) update_index_set(axiom); } +/// An expression representing an array of characters can be in the form of an +/// if expression for instance `cond?array1:(cond2:array2:array3)`. +/// We return all the array expressions contained in `array_expr`. +/// \param array_expr : an expression representing an array +/// \return a vector containing symbols and constant arrays contained in the +/// expression +static std::vector sub_arrays(const exprt &array_expr) +{ + if(array_expr.id()==ID_if) + { + std::vector res1=sub_arrays(to_if_expr(array_expr).true_case()); + std::vector res2=sub_arrays(to_if_expr(array_expr).false_case()); + res1.insert(res1.end(), res2.begin(), res2.end()); + return res1; + } + else + { + INVARIANT( + array_expr.id()==ID_symbol || array_expr.id()==ID_array, + "character arrays should be symbol, constant array, or if expression"); + return std::vector(1, array_expr); + } +} + /// add to the index set all the indices that appear in the formula and the /// upper bound minus one /// \par parameters: a string constraint @@ -1423,17 +1488,13 @@ void string_refinementt::add_to_index_set(const exprt &s, exprt i) mp_integer mpi; to_integer(i, mpi); if(mpi<0) - { - debug() << "add_to_index_set : ignoring negative number " << mpi << eom; return; - } - } - if(index_set[s].insert(i).second) - { - debug() << "adding to index set of " << from_expr(ns, "", s) - << ": " << from_expr(ns, "", i) << eom; - current_index_set[s].insert(i); } + + std::vector subs=sub_arrays(s); + for(const auto &sub : subs) + if(index_set[sub].insert(i).second) + current_index_set[sub].insert(i); } void string_refinementt::initial_index_set(const string_constraintt &axiom) @@ -1504,7 +1565,6 @@ void string_refinementt::update_index_set(const exprt &formula) } } - // Will be used to visit an expression and return the index used // with the given char array that contains qvar class find_index_visitort: public const_expr_visitort