1/*******************************************************************\
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
27#include <unordered_set>
39 lazy_arrays =
false;
// will be set to true when --refine is used
41 // get_array_constraints is true when --show-array-constraints is used
47 // we are not allowed to put the index directly in the
48 // entry for the root of the equivalence class
49 // because this map is accessed during building the error trace
63 "record_array_equality got equality without matching types",
68 "record_array_equality parameter should be array-typed");
89 "record_array_let_binding parameter should be array-typed");
112 for(
const auto &op : expr.
operands())
154 "collect_arrays got 'with' without matching types",
160 // make sure this shows as an application
170 "collect_arrays got 'update' without matching types",
177 // make sure this shows as an application
188 "collect_arrays got if without matching types",
193 "collect_arrays got if without matching types",
213 "unexpected array expression: member with '" + struct_op.id_string() +
227 "byte_update should be removed before collect_arrays");
233 // cast between array types?
236 "unexpected array type cast from " +
typecast_op.type().id_string());
243 // nested unbounded arrays
260 "unexpected array expression (collect_arrays): '" +
a.id_string() +
"'");
269 // lazily add the constraint
285 // add the constraint eagerly
293 // at this point all indices should in the index set
295 // reduce initial index map
298 // add constraints for if, with, array_of, lambda
305 for(std::size_t i = 0; i <
arrays.
size(); i++)
310 // take a copy as arrays may get modified by add_array_constraints
311 // in case of nested unbounded arrays
316 // we have to update before it gets used in the next add_* call
326 // add constraints for equalities
333 // update_index_map should not be necessary here
336 // add the Ackermann constraints
342 // this is quadratic!
345 std::cout <<
"arrays.size(): " <<
arrays.
size() <<
'\n';
348 // iterate over arrays
354 std::cout <<
"index_set.size(): " <<
index_set.size() <<
'\n';
357 // iterate over indices, 2x!
358 for(index_sett::const_iterator
362 for(index_sett::const_iterator
368 if(
i1->is_constant() &&
i2->is_constant())
379 const typet &subtype =
394#if 0 // old code for adding, not significantly faster
419 // iterate over non-roots
420 // possible reasons why update is needed:
421 // -- there are new equivalence classes in arrays
422 // -- there are new indices for arrays that are not the root
423 // of an equivalence class
424 // (and we cannot do that in record_array_index())
425 // -- equivalence classes have been merged
443 std::cout <<
"Index set (" <<
index_entry.first <<
" = "
446 <<
"): " <<
format(index) <<
'\n';
447 std::cout <<
"-----\n";
455 // add constraints x=y => x[i]=y[i]
469 "array elements should all have same type");
478 // equality constraints are not added lazily
479 // convert must be done to guarantee correct update of the index_set
519 INVARIANT(
false,
"byte_update should be removed before arrayst");
523 // we got a=(type[])b
535 "array elements should all have same type");
549 // we got x=let(a=e, A)
550 // add x[i]=A[a/e][i]
554 for(
const auto &binding :
557 replace_symbol.
insert(binding.first, binding.second);
559 replace_symbol(where);
578 "unexpected array expression (add_array_constraints): '" +
587 // We got x=(y with [i:=v]).
588 // First add constraint x[i]=v
596 "with-expression operand should match array element type",
606 // For all other indices use the existing value, i.e., add constraints
607 // x[I]=y[I] for I!=i,j,...
613 // we first build the guard
639#if 0 // old code for adding, not significantly faster
659 // we got x=UPDATE(y, [i], v)
660 // add constaint x[i]=v
663 const exprt &index=expr.where();
664 const exprt &value=expr.new_value();
671 "update operand should match array element type",
677 // use other array index applications for "else" case
678 // add constraint x[I]=y[I] for I!=i
684 // we first build the guard
692 const typet &subtype=expr.type().subtype();
716 // we got x=array_of[v]
717 // get other array index applications
718 // and add constraint x[i]=v
722 const typet &element_type = expr.
type().element_type();
727 "array_of operand type should match array element type");
741 // we got x = { v, ... } - add constraint x[i] = v
746 const typet &element_type = expr.
type().element_type();
749 if(index.is_constant())
751 // We have a constant index - just pick the element at that index from the
754 const std::optional<std::size_t> i =
756 // if the access is out of bounds, we leave it unconstrained
757 if(!i.has_value() || *i >= operands.size())
760 const exprt v = operands[*i];
763 "array operand type should match array element type");
773 // We have a non-constant index into an array constant. We need to build a
774 // case statement testing the index against all possible values. Whenever
775 // neighbouring array elements are the same, we can test the index against
776 // the range rather than individual elements. This should be particularly
777 // helpful when we have arrays of zeros, as is the case for initializers.
779 std::vector<std::pair<std::size_t, std::size_t>>
ranges;
781 for(std::size_t i = 0; i < operands.size(); ++i)
783 if(
ranges.empty() || operands[i] != operands[
ranges.back().first])
784 ranges.emplace_back(i, i);
789 for(
const auto &range :
ranges)
793 if(range.first == range.second)
822 // we got x=lambda(i: e)
823 // get all other array index applications
824 // and add constraints x[j]=e[i/j]
849 // get other array index applications
850 // and add c => x[i]=a[i]
853 // first do true case
868#if 0 // old code for adding, not significantly faster
873 // now the false case
888#if 0 // old code for adding, not significantly faster
899 return "arrayAckermann";
907 return "arrayTypecast";
909 return "arrayConstant";
911 return "arrayComprehension";
913 return "arrayEquality";
Theory of Arrays with Extensionality.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Boolean AND All operands must be boolean, and the result is always boolean.
Expression to define a mapping from an argument (index) to elements.
const symbol_exprt & arg() const
const exprt & body() const
Array constructor from list of elements.
const array_typet & type() const
Array constructor from single element.
const array_typet & type() const
std::list< lazy_constraintt > lazy_array_constraints
std::unordered_set< irep_idt > array_comprehension_args
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
std::set< std::size_t > update_indices
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
void add_array_Ackermann_constraints()
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
void collect_arrays(const exprt &a)
void record_array_let_binding(const symbol_exprt &symbol, const exprt &value)
Record that symbol is equal to value for the purposes of the array theory.
union_find< exprt, irep_hash > arrays
literalt record_array_equality(const equal_exprt &expr)
void add_array_constraints_array_constant(const index_sett &index_set, const array_exprt &exprt)
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
std::map< exprt, bool > expr_map
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
std::string enum_to_string(constraint_typet)
bool get_array_constraints
void add_array_constraints()
void add_array_constraints_comprehension(const index_sett &index_set, const array_comprehension_exprt &expr)
virtual bool is_unbounded_array(const typet &type) const =0
void record_array_index(const index_exprt &expr)
array_equalitiest array_equalities
std::set< exprt > index_sett
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
array_constraint_countt array_constraint_count
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
void display_array_constraint_count()
void update_index_map(bool update_all)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
virtual literalt equality(const exprt &e1, const exprt &e2)
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Boolean OR All operands must be boolean, and the result is always boolean.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
void l_set_to_true(literalt a)
void lcnf(literalt l0, literalt l1)
Replace a symbol expression by a given expression.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
Expression to hold a symbol (variable)
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
size_type number(const T &a)
bool make_union(const T &a, const T &b)
size_type find_number(const_iterator it) const
bool is_root_number(size_type a) const
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
auto lazy(funt fun) -> lazyt< decltype(fun())>
Delay the computation of fun to the next time the force method is called.
std::vector< literalt > bvt
literalt const_literal(bool value)
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.