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, ""); +} 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..1c5bf753395 --- /dev/null +++ b/regression/cbmc/Array_UF22/test.desc @@ -0,0 +1,10 @@ +CORE 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. 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); } 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.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); 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 }