From 10177c6a77df1e4c2848cd51ddd3b3d3841cbbbb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 13 Apr 2019 14:02:38 +0000 Subject: [PATCH] Record constraints of indexed access to array constants When even constant arrays are left to be handled by the array theory, expressions such as { 3, 4 }[1] were actually unconstrained as we never recorded the fact that this expression evaluates to 4. To reduce the number of constraints to be generated for non-constant indices, ranges of equal values just yield a single constraint, optimising the case of large zero-initialised arrays. --- regression/cbmc/array-tests/uf-always.c | 33 +++++++++ regression/cbmc/array-tests/uf-always.desc | 10 +++ src/solvers/flattening/arrays.cpp | 82 +++++++++++++++++++++- src/solvers/flattening/arrays.h | 6 +- 4 files changed, 129 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc/array-tests/uf-always.c create mode 100644 regression/cbmc/array-tests/uf-always.desc diff --git a/regression/cbmc/array-tests/uf-always.c b/regression/cbmc/array-tests/uf-always.c new file mode 100644 index 00000000000..f53a831b2d4 --- /dev/null +++ b/regression/cbmc/array-tests/uf-always.c @@ -0,0 +1,33 @@ +#include + +// C semantics are that these will be zero +int uninitializedGlobalArray1[2]; +int uninitializedGlobalArray2[2]; + +int main(void) +{ + // Variable access + long directUseReadLocation; // Non-det + + long x = directUseReadLocation; + if(0 <= directUseReadLocation && directUseReadLocation < 2) + assert(uninitializedGlobalArray1[directUseReadLocation] == 0); + + /*** Variable non-redundant update ***/ + // No obvious simplifications to writes + + long nonRedundantWriteLocation; + + if( + 0 <= nonRedundantWriteLocation && nonRedundantWriteLocation < 2 && + nonRedundantWriteLocation != 1) + { + uninitializedGlobalArray2[nonRedundantWriteLocation] = 1; + } + + // Constant access + // Again, constant index into a fully known but non-constant array + assert(uninitializedGlobalArray2[1] == 0); + + return 0; +} diff --git a/regression/cbmc/array-tests/uf-always.desc b/regression/cbmc/array-tests/uf-always.desc new file mode 100644 index 00000000000..c51f158c2f5 --- /dev/null +++ b/regression/cbmc/array-tests/uf-always.desc @@ -0,0 +1,10 @@ +CORE +uf-always.c +--arrays-uf-always +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This test is extracted from main.c to showcase a bug in the array encoding. diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index f655298301e..bc9a993febd 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -436,11 +436,12 @@ void arrayst::add_array_constraints( 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_symbol || expr.id()==ID_nondet_symbol || expr.id()==ID_constant || expr.id()=="zero_string" || - expr.id()==ID_array || expr.id()==ID_string_constant) { } @@ -647,6 +648,85 @@ void arrayst::add_array_constraints_array_of( } } +void arrayst::add_array_constraints_array_constant( + const index_sett &index_set, + const array_exprt &expr) +{ + // we got x = { v, ... } - add constraint x[i] = v + const exprt::operandst &operands = expr.operands(); + + for(const auto &index : index_set) + { + const typet &subtype = expr.type().subtype(); + const index_exprt index_expr{expr, index, subtype}; + + if(index.is_constant()) + { + // We have a constant index - just pick the element at that index from the + // array constant. + + const std::size_t i = + numeric_cast_v(to_constant_expr(index)); + // if the access is out of bounds, we leave it unconstrained + if(i >= operands.size()) + continue; + + const exprt v = operands[i]; + DATA_INVARIANT( + index_expr.type() == v.type(), + "array operand type should match array element type"); + + // add constraint + lazy_constraintt lazy{lazy_typet::ARRAY_CONSTANT, + equal_exprt{index_expr, v}}; + add_array_constraint(lazy, false); // added immediately + } + else + { + // 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) + { + if(ranges.empty() || operands[i] != operands[ranges.back().first]) + ranges.emplace_back(i, i); + else + ranges.back().second = i; + } + + for(const auto &range : ranges) + { + exprt index_constraint; + + if(range.first == range.second) + { + index_constraint = + equal_exprt{index, from_integer(range.first, index.type())}; + } + else + { + 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())}}; + } + + 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 + } + } + } +} + void arrayst::add_array_constraints_if( const index_sett &index_set, const if_exprt &expr) diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index fce015291f2..5a7192b24bb 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -83,7 +83,8 @@ class arrayst:public equalityt ARRAY_WITH, ARRAY_IF, ARRAY_OF, - ARRAY_TYPECAST + ARRAY_TYPECAST, + ARRAY_CONSTANT }; struct lazy_constraintt @@ -119,6 +120,9 @@ class arrayst:public equalityt 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 update_index_map(bool update_all); void update_index_map(std::size_t i);