diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 712e80acad9..882b2b28e5d 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -20,6 +20,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include +#include #include #include #include @@ -29,8 +30,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include -static exprt substitute_array_with_expr(const exprt &expr, const exprt &index); - static bool is_valid_string_constraint( messaget::mstreamt &stream, const namespacet &ns, @@ -124,6 +123,12 @@ static optionalt get_array( messaget::mstreamt &stream, const array_string_exprt &arr); +static exprt substitute_array_access( + const index_exprt &index_expr, + const std::function + &symbol_generator, + const bool left_propagate); + /// Convert index-value map to a vector of values. If a value for an /// index is not defined, set it to the value referenced by the next higher /// index. @@ -171,7 +176,7 @@ string_refinementt::string_refinementt(const infot &info, bool): string_refinementt::string_refinementt(const infot &info): string_refinementt(info, validate(info)) { } -/// display the current index set, for debugging +/// Write index set to the given stream, use for debugging static void display_index_set( messaget::mstreamt &stream, const namespacet &ns, @@ -669,6 +674,7 @@ union_find_replacet string_identifiers_resolution_from_equations( return result; } +/// Output a vector of equations to the given stream, used for debugging. void output_equations( std::ostream &output, const std::vector &equations, @@ -1021,8 +1027,12 @@ void string_refinementt::add_lemma( /// Get a model of an array and put it in a certain form. /// If the model is incomplete or if it is too big, return no value. -/// \par parameters: an expression representing an array and an expression -/// representing an integer +/// \param super_get: function returning the valuation of an expression +/// in a model +/// \param ns: namespace +/// \param max_string_length: maximum length of strings to analyze +/// \param stream: output stream for warning messages +/// \param arr: expression of type array representing a string /// \return an optional array expression or array_of_exprt static optionalt get_array( const std::function &super_get, @@ -1104,7 +1114,7 @@ static optionalt get_array( /// convert the content of a string to a more readable representation. This /// should only be used for debugging. -/// \par parameters: a constant array expression and a integer expression +/// \param arr: a constant array expression /// \return a string static std::string string_of_array(const array_exprt &arr) { @@ -1212,36 +1222,87 @@ void debug_model( stream << messaget::eom; } +sparse_arrayt::sparse_arrayt(const with_exprt &expr) +{ + auto ref = std::ref(static_cast(expr)); + while(can_cast_expr(ref.get())) + { + const auto &with_expr = expr_dynamic_cast(ref.get()); + const auto current_index = numeric_cast_v(with_expr.where()); + entries.emplace_back(current_index, with_expr.new_value()); + ref = with_expr.old(); + } + + // This function only handles 'with' and 'array_of' expressions + PRECONDITION(ref.get().id() == ID_array_of); + default_value = expr_dynamic_cast(ref.get()).what(); +} + +exprt sparse_arrayt::to_if_expression(const exprt &index) const +{ + return std::accumulate( + entries.begin(), + entries.end(), + default_value, + [&]( + const exprt if_expr, + const std::pair &entry) { // NOLINT + const exprt entry_index = from_integer(entry.first, index.type()); + const exprt &then_expr = entry.second; + CHECK_RETURN(then_expr.type() == if_expr.type()); + const equal_exprt index_equal(index, entry_index); + return if_exprt(index_equal, then_expr, if_expr, if_expr.type()); + }); +} + +interval_sparse_arrayt::interval_sparse_arrayt(const with_exprt &expr) + : sparse_arrayt(expr) +{ + // Entries are sorted so that successive entries correspond to intervals + std::sort( + entries.begin(), + entries.end(), + []( + const std::pair &a, + const std::pair &b) { return a.first < b.first; }); +} + +exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const +{ + return std::accumulate( + entries.rbegin(), + entries.rend(), + default_value, + [&]( + const exprt if_expr, + const std::pair &entry) { // NOLINT + const exprt entry_index = from_integer(entry.first, index.type()); + const exprt &then_expr = entry.second; + CHECK_RETURN(then_expr.type() == if_expr.type()); + const binary_relation_exprt index_small_eq(index, ID_le, entry_index); + return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type()); + }); +} + /// Create a new expression where 'with' expressions on arrays are replaced by -/// 'if' expressions. e.g. for an array access arr[x], where: `arr := +/// 'if' expressions. e.g. for an array access arr[index], where: `arr := /// array_of(12) with {0:=24} with {2:=42}` the constructed expression will be: /// `index==0 ? 24 : index==2 ? 42 : 12` +/// If `left_propagate` is set to true, the expression will look like +/// `index<=0 ? 24 : index<=2 ? 42 : 12` /// \param expr: A (possibly nested) 'with' expression on an `array_of` -/// expression +/// expression. The function checks that the expression is of the form +/// `with_expr(with_expr(...(array_of(...)))`. This is the form in which +/// array valuations coming from the underlying solver are given. /// \param index: An index with which to build the equality condition /// \return An expression containing no 'with' expression -static exprt substitute_array_with_expr(const exprt &expr, const exprt &index) +static exprt substitute_array_access( + const with_exprt &expr, + const exprt &index, + const bool left_propagate) { - if(expr.id()==ID_with) - { - const with_exprt &with_expr=to_with_expr(expr); - const exprt &then_expr=with_expr.new_value(); - exprt else_expr=substitute_array_with_expr(with_expr.old(), index); - const typet &type=then_expr.type(); - CHECK_RETURN(else_expr.type()==type); - CHECK_RETURN(index.type()==with_expr.where().type()); - return if_exprt( - equal_exprt(index, with_expr.where()), then_expr, else_expr, type); - } - else - { - // Only handle 'with' expressions and 'array_of' expressions. - INVARIANT( - expr.id()==ID_array_of, - string_refinement_invariantt("only handles 'with' and 'array_of' " - "expressions, and expr is 'with' is handled above")); - return to_array_of_expr(expr).what(); - } + return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index) + : sparse_arrayt(expr).to_if_expression(index); } /// Fill an array represented by a list of with_expr by propagating values to @@ -1252,9 +1313,8 @@ static exprt substitute_array_with_expr(const exprt &expr, const exprt &index) /// \param string_max_length: bound on the length of strings /// \return an array expression with filled in values, or expr if it is simply /// an `ARRAY_OF(x)` expression -exprt fill_in_array_with_expr( - const exprt &expr, - const std::size_t string_max_length) +static array_exprt +fill_in_array_with_expr(const exprt &expr, const std::size_t string_max_length) { PRECONDITION(expr.type().id()==ID_array); PRECONDITION(expr.id()==ID_with || expr.id()==ID_array_of); @@ -1320,112 +1380,129 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length) return result; } -/// create an equivalent expression where array accesses and 'with' expressions +/// Create an equivalent expression where array accesses are replaced by 'if' +/// expressions: for instance in array access `arr[index]`, where: +/// `arr := {12, 24, 48}` the constructed expression will be: +/// `index==0 ? 12 : index==1 ? 24 : 48` +static exprt substitute_array_access( + const array_exprt &array_expr, + const exprt &index, + const std::function + &symbol_generator) +{ + const typet &char_type = array_expr.type().subtype(); + const std::vector &operands = array_expr.operands(); + + exprt result = symbol_generator("out_of_bound_access", char_type); + + for(std::size_t i = 0; i < operands.size(); ++i) + { + // Go in reverse order so that smaller indexes appear first in the result + const std::size_t pos = operands.size() - 1 - i; + const equal_exprt equals(index, from_integer(pos, java_int_type())); + if(operands[pos].type() != char_type) + { + INVARIANT( + operands[pos].id() == ID_unknown, + string_refinement_invariantt( + "elements can only have type char or " + "unknown, and it is not char type")); + result = if_exprt(equals, exprt(ID_unknown, char_type), result); + } + else + result = if_exprt(equals, operands[pos], result); + } + return result; +} + +static exprt substitute_array_access( + const if_exprt &if_expr, + const exprt &index, + const std::function + &symbol_generator, + const bool left_propagate) +{ + // Substitute recursively in branches of conditional expressions + const exprt true_case = substitute_array_access( + index_exprt(if_expr.true_case(), index), symbol_generator, left_propagate); + const exprt false_case = substitute_array_access( + index_exprt(if_expr.false_case(), index), symbol_generator, left_propagate); + + return if_exprt(if_expr.cond(), true_case, false_case); +} + +static exprt substitute_array_access( + const index_exprt &index_expr, + const std::function + &symbol_generator, + const bool left_propagate) +{ + const exprt &array = index_expr.array(); + + if(array.id() == ID_symbol) + return index_expr; + if(auto array_of = expr_try_dynamic_cast(array)) + return array_of->op(); + if(auto array_with = expr_try_dynamic_cast(array)) + return substitute_array_access( + *array_with, index_expr.index(), left_propagate); + if(auto array_expr = expr_try_dynamic_cast(array)) + return substitute_array_access( + *array_expr, index_expr.index(), symbol_generator); + if(auto if_expr = expr_try_dynamic_cast(array)) + return substitute_array_access( + *if_expr, index_expr.index(), symbol_generator, left_propagate); + + UNREACHABLE; +} + +/// Auxiliary function for substitute_array_access +/// Performs the same operation but modifies the argument instead of returning +/// the resulting expression. +static void substitute_array_access_in_place( + exprt &expr, + const std::function + &symbol_generator, + const bool left_propagate) +{ + if(const auto index_expr = expr_try_dynamic_cast(expr)) + { + expr = + substitute_array_access(*index_expr, symbol_generator, left_propagate); + } + + for(auto &op : expr.operands()) + substitute_array_access_in_place(op, symbol_generator, left_propagate); +} + +/// Create an equivalent expression where array accesses and 'with' expressions /// are replaced by 'if' expressions, in particular: -/// * for an array access `arr[x]`, where: +/// * for an array access `arr[index]`, where: /// `arr := {12, 24, 48}` the constructed expression will be: /// `index==0 ? 12 : index==1 ? 24 : 48` -/// * for an array access `arr[x]`, where: +/// * for an array access `arr[index]`, where: /// `arr := array_of(12) with {0:=24} with {2:=42}` the constructed /// expression will be: `index==0 ? 24 : index==2 ? 42 : 12` /// * for an array access `(g1?arr1:arr2)[x]` where `arr1 := {12}` and /// `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34` /// * for an access in an empty array `{ }[x]` returns a fresh symbol, this /// corresponds to a non-deterministic result +/// Note that if left_propagate is set to true, the `with` case will result in +/// something like: `index <= 0 ? 24 : index <= 2 ? 42 : 12` /// \param expr: an expression containing array accesses /// \param symbol_generator: function which given a prefix and a type generates /// a fresh symbol of the given type +/// \param left_propagate: should values be propagated to the left in with +/// expressions /// \return an expression containing no array access -static void substitute_array_access( - exprt &expr, +exprt substitute_array_access( + exprt expr, const std::function - &symbol_generator) + &symbol_generator, + const bool left_propagate) { - for(auto &op : expr.operands()) - substitute_array_access(op, symbol_generator); - - if(expr.id()==ID_index) - { - index_exprt &index_expr=to_index_expr(expr); - - if(index_expr.array().id()==ID_symbol) - { - expr=index_expr; - return; - } - - if(index_expr.array().id()==ID_with) - { - expr=substitute_array_with_expr(index_expr.array(), index_expr.index()); - return; - } - - if(index_expr.array().id()==ID_array_of) - { - expr=to_array_of_expr(index_expr.array()).op(); - return; - } - - if(index_expr.array().id()==ID_if) - { - // Substitute recursively in branches of conditional expressions - if_exprt if_expr=to_if_expr(index_expr.array()); - exprt true_case=index_exprt(if_expr.true_case(), index_expr.index()); - substitute_array_access(true_case, symbol_generator); - exprt false_case=index_exprt(if_expr.false_case(), index_expr.index()); - substitute_array_access(false_case, symbol_generator); - expr=if_exprt(if_expr.cond(), true_case, false_case); - return; - } - - DATA_INVARIANT( - index_expr.array().id()==ID_array, - string_refinement_invariantt("and index expression must be on a symbol, " - "with, array_of, if, or array, and all cases besides array are handled " - "above")); - array_exprt &array_expr=to_array_expr(index_expr.array()); - - const typet &char_type = index_expr.array().type().subtype(); - - // Access to an empty array is undefined (non deterministic result) - if(array_expr.operands().empty()) - { - expr = symbol_generator("out_of_bound_access", char_type); - return; - } - - size_t last_index=array_expr.operands().size()-1; - - exprt ite=array_expr.operands().back(); - - if(ite.type()!=char_type) - { - // We have to manually set the type for unknown values - INVARIANT( - ite.id()==ID_unknown, - string_refinement_invariantt("the last element can only have type char " - "or unknown, and it is not char type")); - ite.type()=char_type; - } - - auto op_it=++array_expr.operands().rbegin(); - - for(size_t i=last_index-1; - op_it!=array_expr.operands().rend(); ++op_it, --i) - { - equal_exprt equals(index_expr.index(), from_integer(i, java_int_type())); - if(op_it->type()!=char_type) - { - INVARIANT( - op_it->id()==ID_unknown, - string_refinement_invariantt("elements can only have type char or " - "unknown, and it is not char type")); - op_it->type()=char_type; - } - ite=if_exprt(equals, *op_it, ite); - } - expr=ite; - } + substitute_array_access_in_place(expr, symbol_generator, left_propagate); + return expr; } /// Negates the constraint to be fed to a solver. The intended usage is to find @@ -1652,12 +1729,10 @@ static std::pair> check_axioms( exprt negaxiom=negation_of_constraint(axiom_in_model); negaxiom = simplify_expr(negaxiom, ns); - exprt with_concretized_arrays = - concretize_arrays_in_expression(negaxiom, max_string_length, ns); - - substitute_array_access(with_concretized_arrays, gen_symbol); stream << indent << i << ".\n"; + const exprt with_concretized_arrays = + substitute_array_access(negaxiom, gen_symbol, true); debug_check_axioms_step( stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays); @@ -1708,10 +1783,8 @@ static std::pair> check_axioms( negation_of_not_contains_constraint(nc_axiom_in_model, univ_var); negaxiom = simplify_expr(negaxiom, ns); - exprt with_concrete_arrays = - concretize_arrays_in_expression(negaxiom, max_string_length, ns); - - substitute_array_access(with_concrete_arrays, gen_symbol); + const exprt with_concrete_arrays = + substitute_array_access(negaxiom, gen_symbol, true); stream << indent << i << ".\n"; debug_check_axioms_step( diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 2b6e5524915..e3fdf335820 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -43,6 +43,41 @@ struct string_axiomst std::vector not_contains; }; +/// Represents arrays of the form `array_of(x) with {i:=a} with {j:=b} ...` +/// by a default value `x` and a list of entries `(i,a)`, `(j,b)` etc. +class sparse_arrayt +{ +public: + /// Initialize a sparse array from an expression of the form + /// `array_of(x) with {i:=a} with {j:=b} ...` + /// This is the form in which array valuations coming from the underlying + /// solver are given. + explicit sparse_arrayt(const with_exprt &expr); + + /// Creates an if_expr corresponding to the result of accessing the array + /// at the given index + virtual exprt to_if_expression(const exprt &index) const; + +protected: + exprt default_value; + std::vector> entries; +}; + +/// Represents arrays by the indexes up to which the value remains the same. +/// For instance `{'a', 'a', 'a', 'b', 'b', 'c'}` would be represented by +/// by ('a', 2) ; ('b', 4), ('c', 5). +/// This is particularly useful when the array is constant on intervals. +class interval_sparse_arrayt final : public sparse_arrayt +{ +public: + /// An expression of the form `array_of(x) with {i:=a} with {j:=b}` is + /// converted to an array `arr` where for all index `k` smaller than `i`, + /// `arr[k]` is `a`, for all index between `i` (exclusive) and `j` it is `b` + /// and for the others it is `x`. + explicit interval_sparse_arrayt(const with_exprt &expr); + exprt to_if_expression(const exprt &index) const override; +}; + class string_refinementt final: public bv_refinementt { private: @@ -116,4 +151,11 @@ union_find_replacet string_identifiers_resolution_from_equations( const namespacet &ns, messaget::mstreamt &stream); +// Declaration required for unit-test: +exprt substitute_array_access( + exprt expr, + const std::function + &symbol_generator, + const bool left_propagate); + #endif diff --git a/unit/Makefile b/unit/Makefile index 20185bd20ed..198bfb49c2a 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -36,6 +36,7 @@ SRC += unit_tests.cpp \ solvers/refinement/string_refinement/has_subtype.cpp \ solvers/refinement/string_refinement/substitute_array_list.cpp \ solvers/refinement/string_refinement/string_symbol_resolution.cpp \ + solvers/refinement/string_refinement/sparse_array.cpp \ solvers/refinement/string_refinement/union_find_replace.cpp \ util/expr_cast/expr_cast.cpp \ util/expr_iterator.cpp \ diff --git a/unit/solvers/refinement/string_refinement/sparse_array.cpp b/unit/solvers/refinement/string_refinement/sparse_array.cpp new file mode 100644 index 00000000000..ccd9a8e4482 --- /dev/null +++ b/unit/solvers/refinement/string_refinement/sparse_array.cpp @@ -0,0 +1,88 @@ +/*******************************************************************\ + + Module: Unit tests for sparse arrays + solvers/refinement/string_refinement.cpp + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include +#include + +SCENARIO("sparse_array", "[core][solvers][refinement][string_refinement]") +{ + GIVEN("`ARRAY_OF(0) WITH [4:=x] WITH [1:=y] WITH [100:=z]`") + { + const typet char_type = unsignedbv_typet(16); + const typet int_type = signedbv_typet(32); + const exprt index1 = from_integer(1, int_type); + const exprt charx = from_integer('x', char_type); + const exprt index4 = from_integer(4, int_type); + const exprt chary = from_integer('y', char_type); + const exprt index100 = from_integer(100, int_type); + const exprt char0 = from_integer('0', char_type); + const exprt index2 = from_integer(2, int_type); + const exprt charz = from_integer('z', char_type); + const array_typet array_type(char_type, infinity_exprt(int_type)); + + const with_exprt input_expr( + with_exprt( + with_exprt( + array_of_exprt(from_integer(0, char_type), array_type), + index4, + charx), + index1, + chary), + index100, + charz); + + WHEN("It is converted to a sparse array") + { + const sparse_arrayt sparse_array(input_expr); + THEN("The resulting if expression is index=4?x:index=1?y:index=100?z:0") + { + const symbol_exprt index("index", int_type); + const if_exprt expected( + equal_exprt(index, index4), + charx, + if_exprt( + equal_exprt(index, index1), + chary, + if_exprt( + equal_exprt(index, index100), + charz, + from_integer(0, char_type)))); + REQUIRE(sparse_array.to_if_expression(index) == expected); + } + } + + WHEN("It is converted to an interval sparse array") + { + const interval_sparse_arrayt sparse_array(input_expr); + + THEN( + "The resulting if expression is index<=1?x:index<=4?y:index<=100?z:0") + { + const symbol_exprt index("index", int_type); + const if_exprt expected( + binary_relation_exprt(index, ID_le, index1), + chary, + if_exprt( + binary_relation_exprt(index, ID_le, index4), + charx, + if_exprt( + binary_relation_exprt(index, ID_le, index100), + charz, + from_integer(0, char_type)))); + REQUIRE(sparse_array.to_if_expression(index) == expected); + } + } + } +}