From a2a4feb15f83be2ad5c8d237ce587a267134a248 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 24 Apr 2022 15:55:35 +0000 Subject: [PATCH 1/6] Use instantiate() when flattening array_comprehension_exprt Uses the capabilities of binding_exprt instead of relying on the unrelated replace_exprt to do the right thing. --- src/solvers/flattening/boolbv.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 5b1621c7543..5c66b1a82d6 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -258,8 +257,7 @@ bvt boolbvt::convert_array_comprehension(const array_comprehension_exprt &expr) { exprt counter=from_integer(i, counter_type); - exprt body = expr.body(); - replace_expr(expr.arg(), counter, body); + exprt body = expr.instantiate({counter}); const bvt &tmp = convert_bv(body); From 6f2263a3ebc652b0e6a2fbaba8635d6e8de9627f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 24 Apr 2022 16:05:59 +0000 Subject: [PATCH 2/6] Failing test to demonstrate need for extensionality rule All existing tests rely on indexed access to arrays, which is covered by the read-over-write axiom. --- regression/cbmc/Array_UF22/main.c | 6 ++++++ regression/cbmc/Array_UF22/test.desc | 10 ++++++++++ 2 files changed, 16 insertions(+) create mode 100644 regression/cbmc/Array_UF22/main.c create mode 100644 regression/cbmc/Array_UF22/test.desc diff --git a/regression/cbmc/Array_UF22/main.c b/regression/cbmc/Array_UF22/main.c new file mode 100644 index 00000000000..20ece5e5fe7 --- /dev/null +++ b/regression/cbmc/Array_UF22/main.c @@ -0,0 +1,6 @@ +int main() +{ + int a[2] = {0}; + int b[2] = {0}; + __CPROVER_assert(__CPROVER_array_equal(a, b), "equal"); +} diff --git a/regression/cbmc/Array_UF22/test.desc b/regression/cbmc/Array_UF22/test.desc new file mode 100644 index 00000000000..67011369611 --- /dev/null +++ b/regression/cbmc/Array_UF22/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG broken-smt-backend +main.c +--arrays-uf-always --no-propagation +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test demonstrates the need for implementing the extensionality rule. From b2589d46dc51b0a200184a6c730f764bd31a1738 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 24 Apr 2022 16:00:58 +0000 Subject: [PATCH 3/6] Flattening: support index expressions over zero bitwidth arrays There is not really anything wrong in having empty bitvectors, which we otherwise already support (as of e021eef4). --- src/solvers/flattening/boolbv_index.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index a399606ae50..a4a1f92a695 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -36,9 +36,6 @@ bvt boolbvt::convert_index(const index_exprt &expr) std::size_t width=boolbv_width(expr.type()); - if(width==0) - return conversion_failed(expr); - // see if the array size is constant if(is_unbounded_array(array_type)) @@ -290,9 +287,6 @@ bvt boolbvt::convert_index( std::size_t width = boolbv_width(array_type.element_type()); - if(width==0) - return conversion_failed(array); - // TODO: If the underlying array can use one of the // improvements given above then it may be better to use // the array theory for short chains of updates and then From ecfb7aeee26b0e0de6450f48defcba4a1fa36213 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 21 Apr 2022 18:04:30 +0000 Subject: [PATCH 4/6] Test trace-values: create reads to enforce instantiation The test specification expects that the indices 0, 1, and one other are instantiated. The array theory is only required to do so when also reading from these elements. --- regression/cbmc/trace-values/unbounded_array.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/regression/cbmc/trace-values/unbounded_array.c b/regression/cbmc/trace-values/unbounded_array.c index 2f9ced0fdf6..76d23252541 100644 --- a/regression/cbmc/trace-values/unbounded_array.c +++ b/regression/cbmc/trace-values/unbounded_array.c @@ -9,5 +9,8 @@ int main(int argc, char *argv[]) array[size - 1] = 42; int fixed_array[] = {1, 2}; __CPROVER_array_replace(array, fixed_array); + assert(array[0] == 1); + assert(array[1] == 2); + assert(array[size - 1] == 42); assert(array[0] == 0); } From 2178a2fedec4f41870642e3d9cb7d2c482d1ec70 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 30 May 2017 15:28:37 +0100 Subject: [PATCH 5/6] performance tests for reading/writing arrays --- performance/array_read1.c | 10 ++++++++++ performance/array_write1.c | 10 ++++++++++ 2 files changed, 20 insertions(+) create mode 100644 performance/array_read1.c create mode 100644 performance/array_write1.c diff --git a/performance/array_read1.c b/performance/array_read1.c new file mode 100644 index 00000000000..60d4c912ba4 --- /dev/null +++ b/performance/array_read1.c @@ -0,0 +1,10 @@ +int main() +{ + unsigned size; + char array[size]; + + for(unsigned i = 0; i < N; i++) + __CPROVER_assume(array[i] == 123); + + __CPROVER_assert(0, ""); +} diff --git a/performance/array_write1.c b/performance/array_write1.c new file mode 100644 index 00000000000..95eb89df7e1 --- /dev/null +++ b/performance/array_write1.c @@ -0,0 +1,10 @@ +int main() +{ + unsigned size; + char array[size]; + + for(unsigned i = 0; i < N; i++) + array[i] = 123; + + __CPROVER_assert(0, ""); +} From a02b480c35371336b1427e9dbca99a1cce3243e7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 26 Jul 2017 08:26:06 +0100 Subject: [PATCH 6/6] Array theory: implement weakly equivalent arrays This implements Christ and Hoenicke's Weakly Equivalent Arrays (https://arxiv.org/pdf/1405.6939.pdf) with in-place depth-first path enumeration. Co-authored-by: Michael Tautschnig --- regression/cbmc/Array_UF22/test.desc | 2 +- src/solvers/flattening/arrays.cpp | 1030 +++++++++------------- src/solvers/flattening/arrays.h | 168 ++-- src/solvers/flattening/boolbv_get.cpp | 4 +- src/solvers/refinement/refine_arrays.cpp | 7 +- 5 files changed, 535 insertions(+), 676 deletions(-) diff --git a/regression/cbmc/Array_UF22/test.desc b/regression/cbmc/Array_UF22/test.desc index 67011369611..1c5bf753395 100644 --- a/regression/cbmc/Array_UF22/test.desc +++ b/regression/cbmc/Array_UF22/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG broken-smt-backend +CORE broken-smt-backend main.c --arrays-uf-always --no-propagation ^VERIFICATION SUCCESSFUL$ diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 0fdd83ec127..3fa4ba26ac8 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -10,19 +10,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include #include #include -#ifdef DEBUG -#include +#ifdef DEBUG_ARRAYST +# include #endif -#include - arrayst::arrayst( const namespacet &_ns, propt &_prop, @@ -33,20 +29,13 @@ arrayst::arrayst( log(_message_handler), message_handler(_message_handler) { - lazy_arrays = false; // will be set to true when --refine is used - incremental_cache = false; // for incremental solving // get_array_constraints is true when --show-array-constraints is used get_array_constraints = _get_array_constraints; } void arrayst::record_array_index(const index_exprt &index) { - // we are not allowed to put the index directly in the - // entry for the root of the equivalence class - // because this map is accessed during building the error trace - std::size_t number=arrays.number(index.array()); - if(index_map[number].insert(index.index()).second) - update_indices.insert(number); + collect_indices(index); } literalt arrayst::record_array_equality( @@ -64,25 +53,18 @@ literalt arrayst::record_array_equality( op0.type().id() == ID_array, "record_array_equality parameter should be array-typed"); - array_equalities.push_back(array_equalityt()); - - array_equalities.back().f1=op0; - array_equalities.back().f2=op1; - array_equalities.back().l=SUB::equality(op0, op1); + literalt l = SUB::equality(op0, op1); +#ifdef DEBUG_ARRAYST + std::cout << "LIT " << l.get() << " == " << format(equality) << '\n'; +#endif - arrays.make_union(op0, op1); - collect_arrays(op0); - collect_arrays(op1); + wegt::node_indext a1 = collect_arrays(op0); + wegt::node_indext a2 = collect_arrays(op1); - return array_equalities.back().l; -} + // one undirected edge for each array equality + add_weg_edge(a1, a2, literal_exprt{l}); -void arrayst::collect_indices() -{ - for(std::size_t i=0; i" << (*pn.edge)->first << " " + << format(arrays[pn.n]) << "\n"; +#endif + + const exprt &weg_edge = (*pn.edge)->second; + + // TODO: we should filter out trivially-false conjunctions when literals and + // their negations or equalities and their notequal counterparts are + // included + if(weg_edge.id() == ID_with) { - if(expr_map.find(lazy.lazy) == expr_map.end()) + const auto &with_expr = to_with_expr(weg_edge); + for(std::size_t i = 1; i + 1 < with_expr.operands().size(); i += 2) { - lazy_array_constraints.push_back(lazy); - expr_map[lazy.lazy] = true; + notequal_exprt inequality(with_expr.operands()[i], index_a); + cond.push_back(inequality); } } - else + else if( + weg_edge.id() == ID_literal && + weg_edge != literal_exprt{const_literal(true)}) { - lazy_array_constraints.push_back(lazy); + cond.push_back(weg_edge); } - } - else - { - // add the constraint eagerly - prop.l_set_to_true(convert(lazy.lazy)); + else + UNIMPLEMENTED; } } -void arrayst::add_array_constraints() +void arrayst::process_weg_path(const weg_patht &path) { - collect_indices(); - // at this point all indices should in the index set + INVARIANT(!path.empty(), "path is not empty"); + wegt::node_indext a = path.front().n; + wegt::node_indext b = path.back().n; + +#ifdef DEBUG_ARRAYST + std::cout << "PATH: "; + for(const auto &n : path) + std::cout << n.n << ","; + std::cout << '\n'; +#endif - // reduce initial index map - update_index_map(true); + // do constraints + const index_sett &index_set_a = index_map[a]; + const index_sett &index_set_b = index_map[b]; - // add constraints for if, with, array_of, lambda - std::set roots_to_process, updated_roots; - for(std::size_t i=0; ia[i]=b[j] + // 3. The path condition requires the update indices + // on the stack to be different from i. + exprt::operandst cond; + cond.reserve(path.size() + 1); + cond.push_back(equal_exprt(index_a, index_b)); + weg_path_condition(path, index_a, cond); + + // a_i=b_i + index_exprt a_i(arrays[a], index_a); + // cond => a_i=b_i + implies_exprt implication(conjunction(cond), equal_exprt(a_i, value_b)); +# ifdef DEBUG_ARRAYST + std::cout << "C2a: " << format(implication) << '\n'; +# endif + set_to_true(implication); + } +#endif } - - roots_to_process = std::move(updated_roots); - updated_roots.clear(); - } - - // add constraints for equalities - for(const auto &equality : array_equalities) - { - add_array_constraints_equality( - index_map[arrays.find_number(equality.f1)], - equality); - - // update_index_map should not be necessary here - } - - // add the Ackermann constraints - add_array_Ackermann_constraints(); -} - -void arrayst::add_array_Ackermann_constraints() -{ - // this is quadratic! - -#ifdef DEBUG - std::cout << "arrays.size(): " << arrays.size() << '\n'; + else if(arrays[b].id() == ID_array_of) + { +#if 0 + const auto &expr_b = to_array_of_expr(arrays[b]); + const exprt &value_b = expr_b.what(); + + // 1. we got a[i]...b[j], given as edges on the stack + // 2. add (i=j AND path_cond)=>a[i]=b[j] + // 3. The path condition requires the update indices + // on the stack to be different from i. + exprt::operandst cond; + cond.reserve(path.size()); + weg_path_condition(path, index_a, cond); + + // a_i=value + index_exprt a_i(arrays[a], index_a); + // cond => a_i=b_i + implies_exprt implication(conjunction(cond), equal_exprt(a_i, value_b)); +# ifdef DEBUG_ARRAYST + std::cout << "C2b: " << format(implication) << '\n'; +# endif + set_to_true(implication); #endif - - // iterate over arrays - for(std::size_t i=0; ia[i]=b[j] + // 3. The path condition requires the update indices + // on the stack to be different from i. + exprt::operandst cond; + cond.reserve(path.size() + 1); + cond.push_back(equal_exprt(index_a, index_b)); + weg_path_condition(path, index_a, cond); + + // a_i=b_i + index_exprt a_i(arrays[a], index_a); + // cond => a_i=b_i + implies_exprt implication(conjunction(cond), equal_exprt(a_i, value_b)); +# ifdef DEBUG_ARRAYST + std::cout << "C2c: " << format(implication) << '\n'; +# endif + set_to_true(implication); + } +#endif + } + else if(arrays[b].id() == ID_array_comprehension) + { +#if 0 + const auto &expr_b = to_array_comprehension_expr(arrays[b]); + exprt value_b = expr_b.instantiate({index_a}); + + // 1. we got a[i]...b[j], given as edges on the stack + // 2. add (i=j AND path_cond)=>a[i]=b[j] + // 3. The path condition requires the update indices + // on the stack to be different from i. + exprt::operandst cond; + cond.reserve(path.size()); + weg_path_condition(path, index_a, cond); + + // a_i=value + index_exprt a_i(arrays[a], index_a); + // cond => a_i=b_i + implies_exprt implication(true_exprt{}, /*conjunction(cond),*/ equal_exprt(a_i, value_b)); +# ifdef DEBUG_ARRAYST + std::cout << "C2d: " << format(implication) << '\n'; +# endif + set_to_true(implication); #endif + } + else + { + DATA_INVARIANT_WITH_DIAGNOSTICS( + arrays[b].id() == ID_nondet_symbol || arrays[b].id() == ID_symbol || + arrays[b].id() == ID_if || arrays[b].id() == ID_index, + "expected symbol, if, or index; got ", + arrays[b].pretty()); + } - // iterate over indices, 2x! - for(index_sett::const_iterator - i1=index_set.begin(); - i1!=index_set.end(); - i1++) - for(index_sett::const_iterator - i2=i1; - i2!=index_set.end(); - i2++) - if(i1!=i2) + // TODO: a != b should be trivially true as we don't do self loops + if( + a != + b) // we handle same-array-different index in add_array_Ackermann_constraints + { + for(const auto &index_b : index_set_b) + { + // skip over comparisons that are trivially false + if(index_a.is_constant() && index_b.is_constant() && index_a != index_b) { - if(i1->is_constant() && i2->is_constant()) - continue; - - // index equality - const equal_exprt indices_equal( - *i1, typecast_exprt::conditional_cast(*i2, i1->type())); - - literalt indices_equal_lit=convert(indices_equal); - - if(indices_equal_lit!=const_literal(false)) - { - const typet &subtype = - to_array_type(arrays[i].type()).element_type(); - index_exprt index_expr1(arrays[i], *i1, subtype); - - index_exprt index_expr2=index_expr1; - index_expr2.index()=*i2; - - equal_exprt values_equal(index_expr1, index_expr2); - - // add constraint - lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN, - implies_exprt(literal_exprt(indices_equal_lit), values_equal)); - add_array_constraint(lazy, true); // added lazily - array_constraint_count[constraint_typet::ARRAY_ACKERMANN]++; + continue; + } -#if 0 // old code for adding, not significantly faster - prop.lcnf(!indices_equal_lit, convert(values_equal)); + // 1. we got a[i]...b[j], given as edges on the stack + // 2. add (i=j AND path_cond)=>a[i]=b[j] + // 3. The path condition requires the update indices + // on the stack to be different from i. + exprt::operandst cond; + cond.reserve(path.size() + 1); + cond.push_back(equal_exprt(index_a, index_b)); + weg_path_condition(path, index_a, cond); + + // a_i=b_i + index_exprt a_i(arrays[a], index_a); + index_exprt b_i(arrays[b], index_b); + // cond => a_i=b_i + implies_exprt implication(conjunction(cond), equal_exprt(a_i, b_i)); +#ifdef DEBUG_ARRAYST + std::cout << "C3: " << format(implication) << '\n'; #endif - } - } + set_to_true(implication); + } + } } -} - -/// merge the indices into the root -void arrayst::update_index_map(std::size_t i) -{ - if(arrays.is_root_number(i)) - return; - - std::size_t root_number=arrays.find_number(i); - INVARIANT(root_number!=i, "is_root_number incorrect?"); - index_sett &root_index_set=index_map[root_number]; - index_sett &index_set=index_map[i]; - - root_index_set.insert(index_set.begin(), index_set.end()); -} - -void arrayst::update_index_map(bool update_all) -{ - // iterate over non-roots - // possible reasons why update is needed: - // -- there are new equivalence classes in arrays - // -- there are new indices for arrays that are not the root - // of an equivalence class - // (and we cannot do that in record_array_index()) - // -- equivalence classes have been merged - if(update_all) - { - for(std::size_t i=0; i x[i]=y[i] - - for(const auto &index : index_set) - { - const typet &element_type1 = - to_array_type(array_equality.f1.type()).element_type(); - index_exprt index_expr1(array_equality.f1, index, element_type1); - - const typet &element_type2 = - to_array_type(array_equality.f2.type()).element_type(); - index_exprt index_expr2(array_equality.f2, index, element_type2); - - DATA_INVARIANT( - index_expr1.type()==index_expr2.type(), - "array elements should all have same type"); - - array_equalityt equal; - equal.f1 = index_expr1; - equal.f2 = index_expr2; - equal.l = array_equality.l; - equal_exprt equality_expr(index_expr1, index_expr2); - - // add constraint - // equality constraints are not added lazily - // convert must be done to guarantee correct update of the index_set - prop.lcnf(!array_equality.l, convert(equality_expr)); - array_constraint_count[constraint_typet::ARRAY_EQUALITY]++; - } -} - -void arrayst::add_array_constraints( - const index_sett &index_set, - const exprt &expr) +void arrayst::add_array_constraints() { - if(expr.id()==ID_with) - return add_array_constraints_with(index_set, to_with_expr(expr)); - else if(expr.id()==ID_update) - return add_array_constraints_update(index_set, to_update_expr(expr)); - else if(expr.id()==ID_if) - return add_array_constraints_if(index_set, to_if_expr(expr)); - else if(expr.id()==ID_array_of) - return add_array_constraints_array_of(index_set, to_array_of_expr(expr)); - else if(expr.id() == ID_array) - return add_array_constraints_array_constant(index_set, to_array_expr(expr)); - else if(expr.id() == ID_array_comprehension) - { - return add_array_constraints_comprehension( - index_set, to_array_comprehension_expr(expr)); - } - else if(expr.id()==ID_symbol || - expr.id()==ID_nondet_symbol || - expr.id()==ID_constant || - expr.id()=="zero_string" || - expr.id()==ID_string_constant) + // preprocessing + for(std::size_t i = 0; i < arrays.size(); ++i) { - } - else if( - expr.id() == ID_member && - (to_member_expr(expr).struct_op().id() == ID_symbol || - to_member_expr(expr).struct_op().id() == ID_nondet_symbol)) - { - } - else if(expr.id()==ID_byte_update_little_endian || - expr.id()==ID_byte_update_big_endian) - { - INVARIANT(false, "byte_update should be removed before arrayst"); - } - else if(expr.id()==ID_typecast) - { - // we got a=(type[])b - const auto &expr_typecast_op = to_typecast_expr(expr).op(); - - // add a[i]=b[i] - for(const auto &index : index_set) + if(arrays[i].id() == ID_array) { - const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, index, element_type); - index_exprt index_expr2(expr_typecast_op, index, element_type); - - DATA_INVARIANT( - index_expr1.type()==index_expr2.type(), - "array elements should all have same type"); - - // add constraint - lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST, - equal_exprt(index_expr1, index_expr2)); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_TYPECAST]++; - } - } - else if(expr.id()==ID_index) - { - } - else - { - DATA_INVARIANT( - false, - "unexpected array expression (add_array_constraints): '" + - expr.id_string() + "'"); - } -} + const auto &array_expr = to_array_expr(arrays[i]); -void arrayst::add_array_constraints_with( - const index_sett &index_set, - const with_exprt &expr) -{ - // We got x=(y with [i:=v, j:=w, ...]). - // First add constraints x[i]=v, x[j]=w, ... - std::unordered_set updated_indices; - - const exprt::operandst &operands = expr.operands(); - for(std::size_t i = 1; i + 1 < operands.size(); i += 2) - { - const exprt &index = operands[i]; - const exprt &value = operands[i + 1]; - - index_exprt index_expr( - expr, index, to_array_type(expr.type()).element_type()); - - DATA_INVARIANT_WITH_DIAGNOSTICS( - index_expr.type() == value.type(), - "with-expression operand should match array element type", - irep_pretty_diagnosticst{expr}); - - lazy_constraintt lazy( - lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value)); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_WITH]++; - - updated_indices.insert(index); - } - - // For all other indices use the existing value, i.e., add constraints - // x[I]=y[I] for I!=i,j,... - - for(auto other_index : index_set) - { - if(updated_indices.find(other_index) == updated_indices.end()) - { - // we first build the guard - exprt::operandst disjuncts; - disjuncts.reserve(updated_indices.size()); - for(const auto &index : updated_indices) + for(std::size_t j = 0; j < array_expr.operands().size(); ++j) { - disjuncts.push_back(equal_exprt{ - index, typecast_exprt::conditional_cast(other_index, index.type())}); + const exprt index_constant = + from_integer(j, to_array_type(array_expr.type()).index_type()); + const exprt &value = array_expr.operands()[j]; + + index_map[i].insert(index_constant); + equal_exprt eq{index_exprt{array_expr, index_constant}, value}; +#ifdef DEBUG_ARRAYST + std::cout << "PREPROC: " << format(eq) << '\n'; +#endif + set_to_true(eq); } + } + else if(arrays[i].id() == ID_array_comprehension) + { + const auto &array_comprehension = to_array_comprehension_expr(arrays[i]); + for(const auto r : weg.get_reachable(i, true)) + index_map[i].insert(index_map[r].begin(), index_map[r].end()); - literalt guard_lit = convert(disjunction(disjuncts)); - - if(guard_lit!=const_literal(true)) + for(const auto &index : index_map[i]) { - const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, other_index, element_type); - index_exprt index_expr2(expr.old(), other_index, element_type); - - equal_exprt equality_expr(index_expr1, index_expr2); - - // add constraint - lazy_constraintt lazy(lazy_typet::ARRAY_WITH, or_exprt(equality_expr, - literal_exprt(guard_lit))); - - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_WITH]++; + equal_exprt eq{ + index_exprt{array_comprehension, index}, + array_comprehension.instantiate({index})}; +#ifdef DEBUG_ARRAYST + std::cout << "PREPROC: " << format(eq) << '\n'; +#endif + set_to_true(eq); + } + } + else if(arrays[i].id() == ID_array_of) + { + const auto &array_of_expr = to_array_of_expr(arrays[i]); + const auto &value = array_of_expr.what(); -#if 0 // old code for adding, not significantly faster - { - literalt equality_lit=convert(equality_expr); + for(const auto &index : index_map[i]) + { + equal_exprt eq{index_exprt{array_of_expr, index}, value}; +#ifdef DEBUG_ARRAYST + std::cout << "PREPROC: " << format(eq) << '\n'; +#endif + set_to_true(eq); + } + } + else if(arrays[i].id() == ID_with) + { + const with_exprt &with_expr = to_with_expr(arrays[i]); - bvt bv; - bv.reserve(2); - bv.push_back(equality_lit); - bv.push_back(guard_lit); - prop.lcnf(bv); - } + for(std::size_t j = 1; j < with_expr.operands().size(); j += 2) + { + index_map[i].insert(with_expr.operands()[j]); + equal_exprt eq{ + index_exprt{with_expr, with_expr.operands()[j]}, + with_expr.operands()[j + 1]}; +#ifdef DEBUG_ARRAYST + std::cout << "PREPROC: " << format(eq) << '\n'; #endif + set_to_true(eq); } } } -} - -void arrayst::add_array_constraints_update( - const index_sett &, - const update_exprt &) -{ - // we got x=UPDATE(y, [i], v) - // add constaint x[i]=v - -#if 0 - const exprt &index=expr.where(); - const exprt &value=expr.new_value(); +#ifdef DEBUG_ARRAYST + weg.output_dot(std::cout); + for(std::size_t i = 0; i < arrays.size(); ++i) { - index_exprt index_expr(expr, index, expr.type().subtype()); - - DATA_INVARIANT_WITH_DIAGNOSTICS( - index_expr.type()==value.type(), - "update operand should match array element type", - irep_pretty_diagnosticst{expr}); + std::cout << "IS of " << i << ":"; + for(const auto &ind : index_map[i]) + std::cout << " " << format(ind); + std::cout << '\n'; + } +#endif - set_to_true(equal_exprt(index_expr, value)); +#ifdef DEBUG_ARRAYST + for(const auto &a : arrays) + { + std::cout << "array: " << format(a) << '\n'; } +#endif - // use other array index applications for "else" case - // add constraint x[I]=y[I] for I!=i + // Implement Algorithms 7.4.1 and 7.4.2 by enumerating all simple paths + // instead of iterating over all pairs of arrays and indices. Paths are + // enumerated by performing depth-first search from each node. - for(auto other_index : index_set) + // auxiliary bit per node for DFS + std::vector visited; + visited.resize(weg.size()); + + for(wegt::node_indext a = 0; a < arrays.size(); a++) { - if(other_index!=index) - { - // we first build the guard +#ifdef DEBUG_ARRAYST + std::cout << "a is: " << format(arrays[a]) << '\n'; +#endif - other_index = typecast_exprt::conditional_cast(other_index, index.type()); + // DFS from a_i to anything reachable in 'weg' + std::fill(visited.begin(), visited.end(), false); - literalt guard_lit=convert(equal_exprt(index, other_index)); + weg_patht path; + path.emplace_back(a, std::set()); + visited[a] = true; - if(guard_lit!=const_literal(true)) + while(!path.empty()) + { + // get next edge a->b + stack_entryt &entry = path.back(); + + if(!entry.edge.has_value()) { - const typet &subtype=expr.type().subtype(); - index_exprt index_expr1(expr, other_index, subtype); - index_exprt index_expr2(expr.op0(), other_index, subtype); + if(weg[entry.n].out.empty()) + { + // no successors + path.pop_back(); + continue; + } - equal_exprt equality_expr(index_expr1, index_expr2); + entry.edge = weg[entry.n].out.cbegin(); + } + else if(std::next(*entry.edge) == weg[entry.n].out.end()) + { + // no further successor + path.pop_back(); + continue; + } + else + ++(*entry.edge); - literalt equality_lit=convert(equality_expr); + wegt::node_indext b = (*entry.edge)->first; - // add constraint - bvt bv; - bv.reserve(2); - bv.push_back(equality_lit); - bv.push_back(guard_lit); - prop.lcnf(bv); - } - } - } -#endif -} + if(entry.path_nodes.find(b) != entry.path_nodes.end()) + continue; // already done it -void arrayst::add_array_constraints_array_of( - const index_sett &index_set, - const array_of_exprt &expr) -{ - // we got x=array_of[v] - // get other array index applications - // and add constraint x[i]=v + visited[b] = true; - for(const auto &index : index_set) - { - const typet &element_type = expr.type().element_type(); - index_exprt index_expr(expr, index, element_type); + // add node 'b' to path + path.emplace_back(b, entry.path_nodes); - DATA_INVARIANT( - index_expr.type() == expr.what().type(), - "array_of operand type should match array element type"); - - // add constraint - lazy_constraintt lazy( - lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what())); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_OF]++; + // process + process_weg_path(path); + } } + + // add the Ackermann constraints + add_array_Ackermann_constraints(); } -void arrayst::add_array_constraints_array_constant( - const index_sett &index_set, - const array_exprt &expr) +#if 1 +void arrayst::add_array_Ackermann_constraints() { - // we got x = { v, ... } - add constraint x[i] = v - const exprt::operandst &operands = expr.operands(); - - for(const auto &index : index_set) - { - const typet &element_type = expr.type().element_type(); - const index_exprt index_expr{expr, index, element_type}; + // this is quadratic! - if(index.is_constant()) - { - // We have a constant index - just pick the element at that index from the - // array constant. +# ifdef DEBUG_ARRAYST + std::cout << "arrays.size(): " << arrays.size() << '\n'; +# endif - const optionalt i = - numeric_cast(to_constant_expr(index)); - // if the access is out of bounds, we leave it unconstrained - if(!i.has_value() || *i >= operands.size()) - continue; + // iterate over arrays + // TODO: not clear when we really need this: certainly with arrays[i] == + // ID_array, perhaps also in other cases + for(std::size_t i = 0; i < arrays.size(); i++) + { + const index_sett &index_set = index_map[i]; - const exprt v = operands[*i]; - DATA_INVARIANT( - index_expr.type() == v.type(), - "array operand type should match array element type"); +# ifdef DEBUG_ARRAYST + std::cout << "index_set.size(): " << index_set.size() << '\n'; +# endif - // add constraint - lazy_constraintt lazy{lazy_typet::ARRAY_CONSTANT, - equal_exprt{index_expr, v}}; - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; - } - else + // iterate over indices, 2x! + for(index_sett::const_iterator i1 = index_set.begin(); + i1 != index_set.end(); + i1++) { - // We have a non-constant index into an array constant. We need to build a - // case statement testing the index against all possible values. Whenever - // neighbouring array elements are the same, we can test the index against - // the range rather than individual elements. This should be particularly - // helpful when we have arrays of zeros, as is the case for initializers. - - std::vector> ranges; - - for(std::size_t i = 0; i < operands.size(); ++i) + index_sett::const_iterator next = i1; + next++; + for(index_sett::const_iterator i2 = next; i2 != index_set.end(); i2++) { - if(ranges.empty() || operands[i] != operands[ranges.back().first]) - ranges.emplace_back(i, i); - else - ranges.back().second = i; - } + if(i1->is_constant() && i2->is_constant()) + continue; - for(const auto &range : ranges) - { - exprt index_constraint; + // index equality + equal_exprt indices_equal(*i1, *i2); - if(range.first == range.second) - { - index_constraint = - equal_exprt{index, from_integer(range.first, index.type())}; - } - else + if(indices_equal.op0().type() != indices_equal.op1().type()) { - index_constraint = and_exprt{ - binary_predicate_exprt{ - from_integer(range.first, index.type()), ID_le, index}, - binary_predicate_exprt{ - index, ID_le, from_integer(range.second, index.type())}}; + indices_equal.op1() = + typecast_exprt(indices_equal.op1(), indices_equal.op0().type()); } - lazy_constraintt lazy{ - lazy_typet::ARRAY_CONSTANT, - implies_exprt{index_constraint, - equal_exprt{index_expr, operands[range.first]}}}; - add_array_constraint(lazy, true); // added lazily - array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; - } - } - } -} + literalt indices_equal_lit = convert(indices_equal); -void arrayst::add_array_constraints_comprehension( - const index_sett &index_set, - const array_comprehension_exprt &expr) -{ - // we got x=lambda(i: e) - // get all other array index applications - // and add constraints x[j]=e[i/j] + if(indices_equal_lit != const_literal(false)) + { + const typet &subtype = arrays[i].type().subtype(); + index_exprt index_expr1(arrays[i], *i1, subtype); - for(const auto &index : index_set) - { - index_exprt index_expr{expr, index}; - exprt comprehension_body = expr.body(); - replace_expr(expr.arg(), index, comprehension_body); + index_exprt index_expr2 = index_expr1; + index_expr2.index() = *i2; - // add constraint - lazy_constraintt lazy( - lazy_typet::ARRAY_COMPREHENSION, - equal_exprt(index_expr, comprehension_body)); + equal_exprt values_equal(index_expr1, index_expr2); + prop.lcnf(!indices_equal_lit, convert(values_equal)); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_COMPREHENSION]++; +# ifdef DEBUG_ARRAYST + std::cout << "C4: " << format(indices_equal) << " => " + << format(values_equal) << '\n'; +# endif + } + } + } } } - -void arrayst::add_array_constraints_if( - const index_sett &index_set, - const if_exprt &expr) -{ - // we got x=(c?a:b) - literalt cond_lit=convert(expr.cond()); - - // get other array index applications - // and add c => x[i]=a[i] - // !c => x[i]=b[i] - - // first do true case - - for(const auto &index : index_set) - { - const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, index, element_type); - index_exprt index_expr2(expr.true_case(), index, element_type); - - // add implication - lazy_constraintt lazy(lazy_typet::ARRAY_IF, - or_exprt(literal_exprt(!cond_lit), - equal_exprt(index_expr1, index_expr2))); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_IF]++; - -#if 0 // old code for adding, not significantly faster - prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2))); #endif - } - - // now the false case - for(const auto &index : index_set) - { - const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, index, element_type); - index_exprt index_expr2(expr.false_case(), index, element_type); - - // add implication - lazy_constraintt lazy( - lazy_typet::ARRAY_IF, - or_exprt(literal_exprt(cond_lit), - equal_exprt(index_expr1, index_expr2))); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_IF]++; - -#if 0 // old code for adding, not significantly faster - prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2))); -#endif - } -} std::string arrayst::enum_to_string(constraint_typet type) { diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index 97ba49bef84..27a060bc217 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -12,14 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_FLATTENING_ARRAYS_H #define CPROVER_SOLVERS_FLATTENING_ARRAYS_H +#include +#include +#include + +#include "equality.h" + #include #include #include -#include - -#include "equality.h" - class array_comprehension_exprt; class array_exprt; class array_of_exprt; @@ -29,6 +31,11 @@ class index_exprt; class with_exprt; class update_exprt; +// #define DEBUG_ARRAYST +#ifdef DEBUG_ARRAYST +# include +#endif + class arrayst:public equalityt { public: @@ -49,7 +56,10 @@ class arrayst:public equalityt // NOLINTNEXTLINE(readability/identifiers) typedef equalityt SUB; + /// Notify array theory about the equality constraint \p expr over array-typed + /// operands. literalt record_array_equality(const equal_exprt &expr); + /// Notify array theory about the index expression \p expr. void record_array_index(const index_exprt &expr); protected: @@ -62,59 +72,100 @@ class arrayst:public equalityt add_array_constraints(); } - struct array_equalityt + /// A node of the weak equivalence graph. Each node uniquely corresponds to an + /// array term. + struct weg_nodet : public graph_nodet { - literalt l; - exprt f1, f2; +#ifdef DEBUG_ARRAYST + exprt array; + std::string dot_attributes(const node_indext &i) const override + { + return format_to_string(array); + } +#endif }; - // the list of all equalities between arrays - // references to objects in this container need to be stable as - // elements are added while references are held - typedef std::list array_equalitiest; - array_equalitiest array_equalities; + /// The weak equivalence graph. Based on J Christ, J Hoenicke: Weakly Equivalent + /// Arrays, FroCos 2015. Also described in D Kroening, O Strichman: Decision + /// Procedures, Section 7.4. + /// An edge of the weak equivalence graph is annotated with either a literal + /// recording the equality of the nodes the edge connects, or the store + /// operation that one of the nodes performs. + using wegt = grapht; + wegt weg; - // this is used to find the clusters of arrays being compared - union_find arrays; + void expand_weg(wegt::node_indext index) + { + if(index >= weg.size()) + { + weg.resize(index + 1); +#ifdef DEBUG_ARRAYST + weg[index].array = arrays[index]; +#endif + } + } - // this tracks the array indicies for each array + void + add_weg_edge(wegt::node_indext a1, wegt::node_indext a2, const exprt &cond) + { + // TODO -- we're not always adding a condition here it seems, it's mixed up + // with the literal encoding the equality over arrays + weg.edge(a1, a2) = cond; + weg.edge(a2, a1) = cond; + } + + /// Adds all the constraints eagerly by implementing preprocessing and + /// Algorithms 7.4.1 and 7.4.2 of Section 7.4 of Kroening and Strichman (which + /// describe how to instantiate Lemmas 1 and 2 of Christ and Hoenicke). + void add_array_constraints(); + void add_array_Ackermann_constraints(); + /// Extend the weak equivalence graph with an array term \p a and return its + /// graph node. + wegt::node_indext collect_arrays(const exprt &a); + /// Collect all indices of index expressions contained within \p i (which may + /// itself be an index expression. + void collect_indices(const exprt &i); + + // Map array terms to node indices in the weak equivalence graph. + using array_numberingt = numberingt; + array_numberingt arrays; + static_assert( + std::is_same::value, + "node index type and numbering type must match"); + + // this tracks the array indices for each array typedef std::set index_sett; - // references to values in this container need to be stable as - // elements are added while references are held - typedef std::map index_mapt; + using index_mapt = std::map; index_mapt index_map; - // adds array constraints lazily - enum class lazy_typet + // path search + struct stack_entryt { - ARRAY_ACKERMANN, - ARRAY_WITH, - ARRAY_IF, - ARRAY_OF, - ARRAY_TYPECAST, - ARRAY_CONSTANT, - ARRAY_COMPREHENSION - }; - - struct lazy_constraintt - { - lazy_typet type; - exprt lazy; - - lazy_constraintt(lazy_typet _type, const exprt &_lazy) + wegt::node_indext n; + optionalt edge; + std::set path_nodes; + explicit stack_entryt( + wegt::node_indext _n, + const std::set &_path_nodes) + : n(_n), path_nodes(_path_nodes) { - type = _type; - lazy = _lazy; + path_nodes.insert(n); } }; + using weg_patht = std::vector; + void process_weg_path(const weg_patht &); - bool lazy_arrays; - bool incremental_cache; - bool get_array_constraints; - std::list lazy_array_constraints; - void add_array_constraint(const lazy_constraintt &lazy, bool refine = true); - std::map expr_map; + void weg_path_condition( + const weg_patht &, + const exprt &index_a, + exprt::operandst &cond) const; + + //bool incremental_cache; + + virtual bool is_unbounded_array(const typet &type) const = 0; + // (maybe this function should be partially moved here from boolbv) + bool get_array_constraints; enum class constraint_typet { ARRAY_ACKERMANN, @@ -132,38 +183,7 @@ class arrayst:public equalityt void display_array_constraint_count(); std::string enum_to_string(constraint_typet); - // adds all the constraints eagerly - void add_array_constraints(); - void add_array_Ackermann_constraints(); - void add_array_constraints_equality( - const index_sett &index_set, const array_equalityt &array_equality); - void add_array_constraints( - const index_sett &index_set, const exprt &expr); - void add_array_constraints_if( - const index_sett &index_set, const if_exprt &exprt); - void add_array_constraints_with( - const index_sett &index_set, const with_exprt &expr); - void add_array_constraints_update( - const index_sett &index_set, const update_exprt &expr); - void add_array_constraints_array_of( - const index_sett &index_set, const array_of_exprt &exprt); - void add_array_constraints_array_constant( - const index_sett &index_set, - const array_exprt &exprt); - void add_array_constraints_comprehension( - const index_sett &index_set, - const array_comprehension_exprt &expr); - - void update_index_map(bool update_all); - void update_index_map(std::size_t i); - std::set update_indices; - void collect_arrays(const exprt &a); - void collect_indices(); - void collect_indices(const exprt &a); std::unordered_set array_comprehension_args; - - virtual bool is_unbounded_array(const typet &type) const=0; - // (maybe this function should be partially moved here from boolbv) }; #endif // CPROVER_SOLVERS_FLATTENING_ARRAYS_H diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 19fe12dd050..d7caca2122e 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -310,7 +310,9 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const if(opt_num.has_value()) { // get root - const auto number = arrays.find_number(*opt_num); + const auto number = *opt_num; + if(!number) + return nil_exprt(); assert(number 0) progress=true; +#endif } - /// freeze symbols for incremental solving void bv_refinementt::freeze_lazy_constraints() { +#if 0 if(!lazy_arrays) return; @@ -119,4 +123,5 @@ void bv_refinementt::freeze_lazy_constraints() prop.set_frozen(literal); } } +#endif }