From 12a0fdc1b894bb5c0ce26abe78881d92ab5d8bf7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Aug 2024 10:45:17 +0000 Subject: [PATCH 1/2] Array reasoning: support let expressions We may have `let var=expr in array` expressions, which SMT2 conversion generates (and our in-tree SMT2 solver may have to consume). --- src/solvers/flattening/arrays.cpp | 35 +++++++++++++++++++++++++++++++ src/solvers/flattening/arrays.h | 6 ++++-- 2 files changed, 39 insertions(+), 2 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index cfc6297791a..ad3562ed4d4 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -237,6 +238,11 @@ void arrayst::collect_arrays(const exprt &a) else if(a.id() == ID_array_comprehension) { } + else if(auto let_expr = expr_try_dynamic_cast(a)) + { + arrays.make_union(a, let_expr->where()); + collect_arrays(let_expr->where()); + } else { DATA_INVARIANT( @@ -528,6 +534,33 @@ void arrayst::add_array_constraints( else if(expr.id()==ID_index) { } + else if(auto let_expr = expr_try_dynamic_cast(expr)) + { + // we got x=let(a=e, A) + // add x[i]=A[a/e][i] + + exprt where = let_expr->where(); + replace_symbolt replace_symbol; + for(const auto &binding : + make_range(let_expr->variables()).zip(let_expr->values())) + { + replace_symbol.insert(binding.first, binding.second); + } + replace_symbol(where); + + for(const auto &index : index_set) + { + index_exprt index_expr{expr, index}; + index_exprt where_indexed{where, index}; + + // add constraint + lazy_constraintt lazy{ + lazy_typet::ARRAY_LET, equal_exprt{index_expr, where_indexed}}; + + add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_LET]++; + } + } else { DATA_INVARIANT( @@ -875,6 +908,8 @@ std::string arrayst::enum_to_string(constraint_typet type) return "arrayComprehension"; case constraint_typet::ARRAY_EQUALITY: return "arrayEquality"; + case constraint_typet::ARRAY_LET: + return "arrayLet"; default: UNREACHABLE; } diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index 97ba49bef84..34aea006ca6 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -93,7 +93,8 @@ class arrayst:public equalityt ARRAY_OF, ARRAY_TYPECAST, ARRAY_CONSTANT, - ARRAY_COMPREHENSION + ARRAY_COMPREHENSION, + ARRAY_LET }; struct lazy_constraintt @@ -124,7 +125,8 @@ class arrayst:public equalityt ARRAY_TYPECAST, ARRAY_CONSTANT, ARRAY_COMPREHENSION, - ARRAY_EQUALITY + ARRAY_EQUALITY, + ARRAY_LET }; typedef std::map array_constraint_countt; From af46479ba2a8c52c21cb3dbc6dc5089b757d4966 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Jul 2024 20:51:44 +0000 Subject: [PATCH 2/2] SMT2 back-end: fix inconsistent array flattening Whether we flatten or don't (when datatype support is not available) depends on the expression, but we may need to unflatten when the context expects an array. Fixes: #8399 --- src/solvers/smt2/smt2_conv.cpp | 109 +++++++++++++++++---------------- 1 file changed, 56 insertions(+), 53 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index f63137fdeb7..b5c5366658c 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4445,15 +4445,22 @@ void smt2_convt::convert_member(const member_exprt &expr) CHECK_RETURN_WITH_DIAGNOSTICS( width != 0, "failed to get union member width"); - unflatten(wheret::BEGIN, expr.type()); + if(use_datatypes) + { + unflatten(wheret::BEGIN, expr.type()); - out << "((_ extract " - << (width-1) - << " 0) "; - convert_expr(struct_op); - out << ")"; + out << "((_ extract " << (width - 1) << " 0) "; + convert_expr(struct_op); + out << ")"; - unflatten(wheret::END, expr.type()); + unflatten(wheret::END, expr.type()); + } + else + { + out << "((_ extract " << (width - 1) << " 0) "; + convert_expr(struct_op); + out << ")"; + } } else UNEXPECTEDCASE( @@ -4565,57 +4572,50 @@ void smt2_convt::unflatten( } else if(type.id() == ID_array) { - if(use_datatypes) + PRECONDITION(use_as_const); + + if(where == wheret::BEGIN) + out << "(let ((?ufop" << nesting << " "; + else { - PRECONDITION(use_as_const); + out << ")) "; - if(where == wheret::BEGIN) - out << "(let ((?ufop" << nesting << " "; - else - { - out << ")) "; + const array_typet &array_type = to_array_type(type); - const array_typet &array_type = to_array_type(type); + std::size_t subtype_width = boolbv_width(array_type.element_type()); - std::size_t subtype_width = boolbv_width(array_type.element_type()); + DATA_INVARIANT( + array_type.size().is_constant(), + "cannot unflatten arrays of non-constant size"); + mp_integer size = + numeric_cast_v(to_constant_expr(array_type.size())); - DATA_INVARIANT( - array_type.size().is_constant(), - "cannot unflatten arrays of non-constant size"); - mp_integer size = - numeric_cast_v(to_constant_expr(array_type.size())); + for(mp_integer i = 1; i < size; ++i) + out << "(store "; - for(mp_integer i = 1; i < size; ++i) - out << "(store "; + out << "((as const "; + convert_type(array_type); + out << ") "; + // use element at index 0 as default value + unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1); + out << "((_ extract " << subtype_width - 1 << " " + << "0) ?ufop" << nesting << ")"; + unflatten(wheret::END, array_type.element_type(), nesting + 1); + out << ") "; - out << "((as const "; - convert_type(array_type); - out << ") "; - // use element at index 0 as default value + std::size_t offset = subtype_width; + for(mp_integer i = 1; i < size; ++i, offset += subtype_width) + { + convert_expr(from_integer(i, array_type.index_type())); + out << ' '; unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1); - out << "((_ extract " << subtype_width - 1 << " " - << "0) ?ufop" << nesting << ")"; + out << "((_ extract " << offset + subtype_width - 1 << " " << offset + << ") ?ufop" << nesting << ")"; unflatten(wheret::END, array_type.element_type(), nesting + 1); - out << ") "; - - std::size_t offset = subtype_width; - for(mp_integer i = 1; i < size; ++i, offset += subtype_width) - { - convert_expr(from_integer(i, array_type.index_type())); - out << ' '; - unflatten(wheret::BEGIN, array_type.element_type(), nesting + 1); - out << "((_ extract " << offset + subtype_width - 1 << " " << offset - << ") ?ufop" << nesting << ")"; - unflatten(wheret::END, array_type.element_type(), nesting + 1); - out << ")"; // store - } - - out << ")"; // let + out << ")"; // store } - } - else - { - // nop, already a bv + + out << ")"; // let } } else if(type.id() == ID_struct || type.id() == ID_struct_tag) @@ -4767,19 +4767,22 @@ void smt2_convt::set_to(const exprt &expr, bool value) { out << "(define-fun " << smt2_identifier; out << " () "; + convert_type(equal_expr.lhs().type()); + out << ' '; if( equal_expr.lhs().type().id() != ID_array || use_array_theory(prepared_rhs)) { - convert_type(equal_expr.lhs().type()); + convert_expr(prepared_rhs); } else { - std::size_t width = boolbv_width(equal_expr.lhs().type()); - out << "(_ BitVec " << width << ")"; + unflatten(wheret::BEGIN, equal_expr.lhs().type()); + + convert_expr(prepared_rhs); + + unflatten(wheret::END, equal_expr.lhs().type()); } - out << ' '; - convert_expr(prepared_rhs); out << ')' << '\n'; }