From 525c23dc7cea9b550a98e4495fec315231fdf868 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 Jul 2025 16:06:27 +0000 Subject: [PATCH 1/2] Incremental SMT2 back-end: simplify encoded expressions This is in preparation of moving to 3-operand with-expressions: without intervening use of the simplifier some generated expressions could become unnecessarily large. --- src/util/simplify_expr.cpp | 13 ++ src/util/simplify_expr_int.cpp | 11 +- .../encoding/struct_encoding.cpp | 113 +++++++++++------- 3 files changed, 94 insertions(+), 43 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index b6f19abda7b..3e6afaa792a 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1339,6 +1339,19 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) return changed(simplify_address_of(result)); // recursive call } } + else if(auto extractbits = expr_try_dynamic_cast(operand)) + { + if( + can_cast_type(expr_type) && + can_cast_type(operand.type()) && + to_bitvector_type(expr_type).get_width() == + to_bitvector_type(operand.type()).get_width()) + { + extractbits_exprt result = *extractbits; + result.type() = expr_type; + return changed(simplify_extractbits(result)); + } + } return unchanged(expr); } diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index aad92696471..f1fa489bdfc 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -992,10 +992,15 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) } // { x } = x - if( - new_expr.operands().size() == 1 && new_expr.op0().type() == new_expr.type()) + if(new_expr.operands().size() == 1) { - return new_expr.op0(); + if(new_expr.op0().type() == new_expr.type()) + return new_expr.op0(); + else + { + return changed( + simplify_typecast(typecast_exprt{new_expr.op0(), new_expr.type()})); + } } if(no_change) diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp index 96d96cb07e1..4cd37efac19 100644 --- a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -6,6 +6,7 @@ #include #include #include +#include #include #include @@ -242,12 +243,16 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") symbol_expr, make_member_name_expression("green"), from_integer(0, signedbv_typet{32})}; - const concatenation_exprt expected{ - {from_integer(0, signedbv_typet{32}), - extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, - extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}}, - bv_typet{72}}; - REQUIRE(test.struct_encoding.encode(with) == expected); + const exprt expected = simplify_expr( + concatenation_exprt{ + {from_integer(0, signedbv_typet{32}), + extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, + extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}}, + bv_typet{72}}, + test.ns); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with), test.ns); + REQUIRE(encoded == expected); } SECTION("Second member") { @@ -268,20 +273,26 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") symbol_expr, make_member_name_expression("ham"), from_integer(0, signedbv_typet{24})}; - const concatenation_exprt expected{ - {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}}, - extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, - from_integer(0, signedbv_typet{24})}, - bv_typet{72}}; - REQUIRE(test.struct_encoding.encode(with) == expected); + const exprt expected = simplify_expr( + concatenation_exprt{ + {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}}, + extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, + from_integer(0, signedbv_typet{24})}, + bv_typet{72}}, + test.ns); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with), test.ns); + REQUIRE(encoded == expected); } SECTION("First and second members") { - const concatenation_exprt expected{ - {from_integer(0, signedbv_typet{32}), - from_integer(1, unsignedbv_typet{16}), - extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}}, - bv_typet{72}}; + const exprt expected = simplify_expr( + concatenation_exprt{ + {from_integer(0, signedbv_typet{32}), + from_integer(1, unsignedbv_typet{16}), + extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}}, + bv_typet{72}}, + test.ns); SECTION("Operands in field order") { with_exprt with_in_order{ @@ -291,7 +302,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") with_in_order.operands().push_back(make_member_name_expression("eggs")); with_in_order.operands().push_back( from_integer(1, unsignedbv_typet{16})); - REQUIRE(test.struct_encoding.encode(with_in_order) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with_in_order), test.ns); + REQUIRE(encoded == expected); } SECTION("Operands in reverse order vs fields") { @@ -302,16 +315,20 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") with_reversed.operands().push_back( make_member_name_expression("green")); with_reversed.operands().push_back(from_integer(0, signedbv_typet{32})); - REQUIRE(test.struct_encoding.encode(with_reversed) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with_reversed), test.ns); + REQUIRE(encoded == expected); } } SECTION("First and third members") { - const concatenation_exprt expected{ - {from_integer(0, signedbv_typet{32}), - extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, - from_integer(1, signedbv_typet{24})}, - bv_typet{72}}; + const exprt expected = simplify_expr( + concatenation_exprt{ + {from_integer(0, signedbv_typet{32}), + extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, + from_integer(1, signedbv_typet{24})}, + bv_typet{72}}, + test.ns); SECTION("Operands in field order") { with_exprt with_in_order{ @@ -320,7 +337,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") from_integer(0, signedbv_typet{32})}; with_in_order.operands().push_back(make_member_name_expression("ham")); with_in_order.operands().push_back(from_integer(1, signedbv_typet{24})); - REQUIRE(test.struct_encoding.encode(with_in_order) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with_in_order), test.ns); + REQUIRE(encoded == expected); } SECTION("Operands in reverse order vs fields") { @@ -331,16 +350,20 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") with_reversed.operands().push_back( make_member_name_expression("green")); with_reversed.operands().push_back(from_integer(0, signedbv_typet{32})); - REQUIRE(test.struct_encoding.encode(with_reversed) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with_reversed), test.ns); + REQUIRE(encoded == expected); } } SECTION("Second and third members") { - const concatenation_exprt expected{ - {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}}, - from_integer(0, unsignedbv_typet{16}), - from_integer(1, signedbv_typet{24})}, - bv_typet{72}}; + const exprt expected = simplify_expr( + concatenation_exprt{ + {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}}, + from_integer(0, unsignedbv_typet{16}), + from_integer(1, signedbv_typet{24})}, + bv_typet{72}}, + test.ns); SECTION("Operands in field order") { with_exprt with_in_order{ @@ -349,7 +372,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") from_integer(0, unsignedbv_typet{16})}; with_in_order.operands().push_back(make_member_name_expression("ham")); with_in_order.operands().push_back(from_integer(1, signedbv_typet{24})); - REQUIRE(test.struct_encoding.encode(with_in_order) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with_in_order), test.ns); + REQUIRE(encoded == expected); } SECTION("Operands in reverse order vs fields") { @@ -360,16 +385,20 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") with_reversed.operands().push_back(make_member_name_expression("eggs")); with_reversed.operands().push_back( from_integer(0, unsignedbv_typet{16})); - REQUIRE(test.struct_encoding.encode(with_reversed) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with_reversed), test.ns); + REQUIRE(encoded == expected); } } SECTION("All members") { - const concatenation_exprt expected{ - {from_integer(1, signedbv_typet{32}), - from_integer(2, unsignedbv_typet{16}), - from_integer(3, signedbv_typet{24})}, - bv_typet{72}}; + const exprt expected = simplify_expr( + concatenation_exprt{ + {from_integer(1, signedbv_typet{32}), + from_integer(2, unsignedbv_typet{16}), + from_integer(3, signedbv_typet{24})}, + bv_typet{72}}, + test.ns); SECTION("Operands in field order") { with_exprt with{ @@ -380,7 +409,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") with.operands().push_back(from_integer(2, unsignedbv_typet{16})); with.operands().push_back(make_member_name_expression("ham")); with.operands().push_back(from_integer(3, signedbv_typet{24})); - REQUIRE(test.struct_encoding.encode(with) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with), test.ns); + REQUIRE(encoded == expected); } SECTION("Operands out of order vs fields") { @@ -392,7 +423,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") with.operands().push_back(from_integer(3, signedbv_typet{24})); with.operands().push_back(make_member_name_expression("green")); with.operands().push_back(from_integer(1, signedbv_typet{32})); - REQUIRE(test.struct_encoding.encode(with) == expected); + const exprt encoded = + simplify_expr(test.struct_encoding.encode(with), test.ns); + REQUIRE(encoded == expected); } } } From fc5c5a047146139ca6eff889b78d57dd2dd251f8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 Jul 2025 16:06:12 +0000 Subject: [PATCH 2/2] Restrict with_exprt to exactly three operands We cannot build a C++ API for the previous >= 3, odd-number operand variant. Alas, we ended up with various places in the code base silently ignoring additional operands, which led to wrong verification results in Kani as recent changes in CBMC made increasing use of the value set (which is one of the places that silently ignored additional operands). Resolves: #7272 --- src/goto-programs/graphml_witness.cpp | 34 ++++--- src/solvers/flattening/arrays.cpp | 40 +++----- src/solvers/flattening/boolbv_with.cpp | 37 ++------ src/solvers/smt2/smt2_conv.cpp | 20 +--- .../smt2_incremental/convert_expr_to_smt.cpp | 9 +- .../encoding/struct_encoding.cpp | 53 +++-------- .../smt2_incremental_decision_procedure.cpp | 17 ++-- src/util/lower_byte_operators.cpp | 7 +- src/util/simplify_expr.cpp | 94 +++++++------------ src/util/std_expr.h | 6 +- .../smt2_incremental/convert_expr_to_smt.cpp | 8 +- .../encoding/struct_encoding.cpp | 80 +++++++++------- .../smt2_incremental_decision_procedure.cpp | 12 ++- 13 files changed, 158 insertions(+), 259 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index e0aef679768..41f08f15515 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -170,26 +170,24 @@ std::string graphml_witnesst::convert_assign_rec( else if(assign.rhs().id() == ID_with) { const with_exprt &with_expr = to_with_expr(assign.rhs()); - const auto &ops = with_expr.operands(); - for(std::size_t i = 1; i < ops.size(); i += 2) - { - if(!result.empty()) - result += ' '; + if(!result.empty()) + result += ' '; - if(ops[i].id() == ID_member_name) - { - const member_exprt member{ - assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()}; - result += - convert_assign_rec(identifier, code_assignt(member, ops[i + 1])); - } - else - { - const index_exprt index{assign.lhs(), ops[i]}; - result += - convert_assign_rec(identifier, code_assignt(index, ops[i + 1])); - } + if(with_expr.where().id() == ID_member_name) + { + const member_exprt member{ + assign.lhs(), + with_expr.where().get(ID_component_name), + with_expr.new_value().type()}; + result += convert_assign_rec( + identifier, code_assignt(member, with_expr.new_value())); + } + else + { + const index_exprt index{assign.lhs(), with_expr.where()}; + result += convert_assign_rec( + identifier, code_assignt(index, with_expr.new_value())); } } else diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index ad3562ed4d4..96cb3c8045f 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -145,11 +145,8 @@ void arrayst::collect_arrays(const exprt &a) collect_arrays(with_expr.old()); // make sure this shows as an application - for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) - { - index_exprt index_expr(with_expr.old(), with_expr.operands()[i]); - record_array_index(index_expr); - } + index_exprt index_expr(with_expr.old(), with_expr.where()); + record_array_index(index_expr); } else if(a.id()==ID_update) { @@ -574,31 +571,24 @@ 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, ... + // We got x=(y with [i:=v]). + // First add constraint x[i]=v 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()); + index_exprt index_expr( + expr, expr.where(), 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}); + DATA_INVARIANT_WITH_DIAGNOSTICS( + index_expr.type() == expr.new_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]++; + lazy_constraintt lazy( + lazy_typet::ARRAY_WITH, equal_exprt(index_expr, expr.new_value())); + add_array_constraint(lazy, false); // added immediately + array_constraint_count[constraint_typet::ARRAY_WITH]++; - updated_indices.insert(index); - } + updated_indices.insert(expr.where()); // For all other indices use the existing value, i.e., add constraints // x[I]=y[I] for I!=i,j,... diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp index 5eb83b0b3c0..c7c335ff96c 100644 --- a/src/solvers/flattening/boolbv_with.cpp +++ b/src/solvers/flattening/boolbv_with.cpp @@ -16,28 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_with(const with_exprt &expr) { + DATA_INVARIANT( + expr.operands().size() == 3, + "with_exprt with more than 3 operands should no longer exist"); + auto &type = expr.type(); if( type.id() == ID_bv || type.id() == ID_unsignedbv || type.id() == ID_signedbv) { - if(expr.operands().size() > 3) - { - std::size_t s = expr.operands().size(); - - // strip off the trailing two operands - with_exprt tmp = expr; - tmp.operands().resize(s - 2); - - with_exprt new_with_expr( - tmp, expr.operands()[s - 2], expr.operands().back()); - - // recursive call - return convert_with(new_with_expr); - } - - PRECONDITION(expr.operands().size() == 3); if(expr.new_value().type().id() == ID_bool) { return convert_bv( @@ -50,7 +38,7 @@ bvt boolbvt::convert_with(const with_exprt &expr) } } - bvt bv = convert_bv(expr.old()); + bvt bv_old = convert_bv(expr.old()); std::size_t width = boolbv_width(type); @@ -61,21 +49,14 @@ bvt boolbvt::convert_with(const with_exprt &expr) } DATA_INVARIANT_WITH_DIAGNOSTICS( - bv.size() == width, + bv_old.size() == width, "unexpected operand 0 width", irep_pretty_diagnosticst{expr}); - bvt prev_bv; - prev_bv.resize(width); - - const exprt::operandst &ops=expr.operands(); + bvt bv; + bv.resize(width); - for(std::size_t op_no=1; op_no3) - { - std::size_t s=expr.operands().size(); - - // strip off the trailing two operands - with_exprt tmp = expr; - tmp.operands().resize(s-2); - - with_exprt new_with_expr( - tmp, expr.operands()[s - 2], expr.operands().back()); - - // recursive call - return convert_with(new_with_expr); - } - INVARIANT( expr.operands().size() == 3, - "with expression should have been converted to a version with three " - "operands above"); + "with expression should have exactly three operands"); const typet &expr_type = expr.type(); diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 4622c32eb9e..de901db4f59 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1005,12 +1005,9 @@ static smt_termt convert_array_update_to_smt( const sub_expression_mapt &converted) { smt_termt array = converted.at(with.old()); - for(auto it = ++with.operands().begin(); it != with.operands().end(); it += 2) - { - const smt_termt &index_term = converted.at(it[0]); - const smt_termt &value_term = converted.at(it[1]); - array = smt_array_theoryt::store(array, index_term, value_term); - } + const smt_termt &index_term = converted.at(with.where()); + const smt_termt &value_term = converted.at(with.new_value()); + array = smt_array_theoryt::store(array, index_term, value_term); return array; } diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index 7e8e946d86b..baf18f3187d 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -71,52 +71,25 @@ typet struct_encodingt::encode(typet type) const return type; } -/// \brief Extracts the component/field names and new values from a `with_exprt` -/// which expresses a new struct value where one or more members of a -/// struct have had their values substituted with new values. -/// \note This is implemented using direct access to the operands and other -/// underlying irept interfaces, because the interface for `with_exprt` -/// only supports a single `where` / `new_value` pair and does not -/// support extracting the name from the `where` operand. -static std::unordered_map -extricate_updates(const with_exprt &struct_expr) -{ - std::unordered_map pairs; - auto current_operand = struct_expr.operands().begin(); - // Skip the struct being updated in order to begin with the pairs. - current_operand++; - while(current_operand != struct_expr.operands().end()) - { - INVARIANT( - current_operand->id() == ID_member_name, - "operand is expected to be the name of a member"); - auto name = current_operand->find(ID_component_name).id(); - ++current_operand; - INVARIANT( - current_operand != struct_expr.operands().end(), - "every name is expected to be followed by a paired value"); - pairs[name] = *current_operand; - ++current_operand; - } - POSTCONDITION(!pairs.empty()); - return pairs; -} - static exprt encode(const with_exprt &with, const namespacet &ns) { const auto tag_type = type_checked_cast(with.type()); const auto struct_type = ns.follow_tag(tag_type); - const auto updates = extricate_updates(with); + INVARIANT( + with.where().id() == ID_member_name, + "operand is expected to be the name of a member"); + const auto update_name = with.where().find(ID_component_name).id(); const auto components = make_range(struct_type.components()) - .map([&](const struct_union_typet::componentt &component) -> exprt { - const auto &update = updates.find(component.get_name()); - if(update != updates.end()) - return update->second; - else - return member_exprt{ - with.old(), component.get_name(), component.type()}; - }) + .map( + [&](const struct_union_typet::componentt &component) -> exprt + { + if(component.get_name() == update_name) + return with.new_value(); + else + return member_exprt{ + with.old(), component.get_name(), component.type()}; + }) .collect(); return struct_exprt{components, tag_type}; } diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 72575d89f6b..0d8a91a6f89 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -334,16 +334,14 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined( void smt2_incremental_decision_proceduret::define_index_identifiers( const exprt &expr) { - expr.visit_pre([&](const exprt &expr_node) { - if(!can_cast_type(expr_node.type())) - return; - if(const auto with_expr = expr_try_dynamic_cast(expr_node)) + expr.visit_post( + [&](const exprt &expr_node) { - for(auto operand_ite = ++with_expr->operands().begin(); - operand_ite != with_expr->operands().end(); - operand_ite += 2) + if(!can_cast_type(expr_node.type())) + return; + if(const auto with_expr = expr_try_dynamic_cast(expr_node)) { - const auto index_expr = *operand_ite; + const auto index_expr = with_expr->where(); const auto index_term = convert_expr_to_smt(index_expr); const auto index_identifier = "index_" + std::to_string(index_sequence()); @@ -356,8 +354,7 @@ void smt2_incremental_decision_proceduret::define_index_identifiers( solver_process->send( smt_define_function_commandt{index_identifier, {}, index_term}); } - } - }); + }); } exprt smt2_incremental_decision_proceduret::substitute_defined_padding( diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index 2399796f695..2ba9ecdb6b2 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -1607,10 +1607,7 @@ static exprt lower_byte_update_byte_array_vector( index_exprt{src.op(), where}}; } - if(result.id() != ID_with) - result = with_exprt{result, std::move(where), std::move(update_value)}; - else - result.add_to_operands(std::move(where), std::move(update_value)); + result = with_exprt{result, std::move(where), std::move(update_value)}; } return simplify_expr(std::move(result), ns); @@ -1892,7 +1889,7 @@ static exprt lower_byte_update_array_vector_non_const( src.get_bits_per_byte()}, ns); - result.add_to_operands(std::move(where), std::move(element)); + result = with_exprt{result, std::move(where), std::move(element)}; }; std::size_t i = 1; diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 3e6afaa792a..18b2cf3fa8c 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1458,84 +1458,52 @@ simplify_exprt::simplify_lambda(const lambda_exprt &expr) simplify_exprt::resultt<> simplify_exprt::simplify_with(const with_exprt &expr) { - bool no_change = true; - - if((expr.operands().size()%2)!=1) - return unchanged(expr); - - // copy - auto with_expr = expr; - // now look at first operand if( - with_expr.old().type().id() == ID_struct || - with_expr.old().type().id() == ID_struct_tag) + expr.old().type().id() == ID_struct || + expr.old().type().id() == ID_struct_tag) { - if(with_expr.old().id() == ID_struct || with_expr.old().is_constant()) + if(expr.old().id() == ID_struct || expr.old().is_constant()) { - while(with_expr.operands().size() > 1) - { - const irep_idt &component_name = - with_expr.where().get(ID_component_name); - - const struct_typet &old_type_followed = - with_expr.old().type().id() == ID_struct_tag - ? ns.follow_tag(to_struct_tag_type(with_expr.old().type())) - : to_struct_type(with_expr.old().type()); - if(!old_type_followed.has_component(component_name)) - return unchanged(expr); + const irep_idt &component_name = expr.where().get(ID_component_name); - std::size_t number = old_type_followed.component_number(component_name); - - if(number >= with_expr.old().operands().size()) - return unchanged(expr); + const struct_typet &old_type_followed = + expr.old().type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(expr.old().type())) + : to_struct_type(expr.old().type()); + if(!old_type_followed.has_component(component_name)) + return unchanged(expr); - with_expr.old().operands()[number].swap(with_expr.new_value()); + std::size_t number = old_type_followed.component_number(component_name); - with_expr.operands().erase(++with_expr.operands().begin()); - with_expr.operands().erase(++with_expr.operands().begin()); + if(number >= expr.old().operands().size()) + return unchanged(expr); - no_change = false; - } + exprt result = expr.old(); + result.operands()[number] = expr.new_value(); + return result; } } else if( - with_expr.old().type().id() == ID_array || - with_expr.old().type().id() == ID_vector) + expr.old().type().id() == ID_array || expr.old().type().id() == ID_vector) { if( - with_expr.old().id() == ID_array || with_expr.old().is_constant() || - with_expr.old().id() == ID_vector) + expr.old().id() == ID_array || expr.old().is_constant() || + expr.old().id() == ID_vector) { - while(with_expr.operands().size() > 1) - { - const auto i = numeric_cast(with_expr.where()); + const auto i = numeric_cast(expr.where()); - if(!i.has_value()) - break; - - if(*i < 0 || *i >= with_expr.old().operands().size()) - break; - - with_expr.old().operands()[numeric_cast_v(*i)].swap( - with_expr.new_value()); - - with_expr.operands().erase(++with_expr.operands().begin()); - with_expr.operands().erase(++with_expr.operands().begin()); - - no_change = false; + if(i.has_value() && *i >= 0 && *i < expr.old().operands().size()) + { + exprt result = expr.old(); + result.operands()[numeric_cast_v(*i)] = expr.new_value(); + return result; } } } - if(with_expr.operands().size() == 1) - return with_expr.old(); - - if(no_change) - return unchanged(expr); - else - return std::move(with_expr); + return unchanged(expr); } simplify_exprt::resultt<> @@ -2276,7 +2244,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) for(mp_integer i = 1; i < n_elements; ++i) { - result_expr.add_to_operands( + result_expr = with_exprt{ + result_expr, from_integer(base_offset + i, array_type->index_type()), byte_extract_exprt{ matching_byte_extract_id, @@ -2284,7 +2253,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) from_integer( i * (*el_size / expr.get_bits_per_byte()), offset.type()), expr.get_bits_per_byte(), - array_type->element_type()}); + array_type->element_type()}}; } return changed(simplify_rec(result_expr)); @@ -2350,7 +2319,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) mp_integer n_elements = *val_size / *el_size; for(mp_integer i = 1; i < n_elements; ++i) { - result_expr.add_to_operands( + result_expr = with_exprt{ + result_expr, typecast_exprt::conditional_cast( plus_exprt{base_offset, from_integer(i, base_offset.type())}, array_type->index_type()), @@ -2360,7 +2330,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) from_integer( i * (*el_size / expr.get_bits_per_byte()), offset.type()), expr.get_bits_per_byte(), - array_type->element_type()}); + array_type->element_type()}}; } return changed(simplify_rec(result_expr)); } diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 90cac8a1d8d..c96f16eaf39 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2649,11 +2649,7 @@ inline bool can_cast_expr(const exprt &base) inline void validate_expr(const with_exprt &value) { - validate_operands( - value, 3, "array/structure update must have at least 3 operands", true); - DATA_INVARIANT( - value.operands().size() % 2 == 1, - "array/structure update must have an odd number of operands"); + validate_operands(value, 3, "array/structure update must have 3 operands"); } /// \brief Cast an exprt to a \ref with_exprt diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index a3ab0005dae..4a70592f67c 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1271,17 +1271,17 @@ TEST_CASE( INFO("Expression being converted: " + with.pretty(2, 0)); CHECK(test.convert(with) == expected); } - SECTION("Dual where/new_value pair update") + SECTION("Nested where/new_value pair update") { exprt index2 = from_integer(24, unsignedbv_typet{64}); exprt value2 = from_integer(21, value_type); - with.add_to_operands(std::move(index2), std::move(value2)); + with_exprt with2{with, std::move(index2), std::move(value2)}; const smt_termt expected2 = smt_array_theoryt::store( expected, smt_bit_vector_constant_termt{24, 64}, smt_bit_vector_constant_termt{21, 8}); - INFO("Expression being converted: " + with.pretty(2, 0)); - CHECK(test.convert(with) == expected2); + INFO("Expression being converted: " + with2.pretty(2, 0)); + CHECK(test.convert(with2) == expected2); } } } diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp index 4cd37efac19..9355bc93096 100644 --- a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -295,26 +295,28 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") test.ns); SECTION("Operands in field order") { - with_exprt with_in_order{ + with_exprt with_in_order_inner{ symbol_expr, make_member_name_expression("green"), from_integer(0, signedbv_typet{32})}; - with_in_order.operands().push_back(make_member_name_expression("eggs")); - with_in_order.operands().push_back( - from_integer(1, unsignedbv_typet{16})); + with_exprt with_in_order{ + with_in_order_inner, + make_member_name_expression("eggs"), + from_integer(1, unsignedbv_typet{16})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with_in_order), test.ns); REQUIRE(encoded == expected); } SECTION("Operands in reverse order vs fields") { - with_exprt with_reversed{ + with_exprt with_reversed_inner{ symbol_expr, make_member_name_expression("eggs"), from_integer(1, unsignedbv_typet{16})}; - with_reversed.operands().push_back( - make_member_name_expression("green")); - with_reversed.operands().push_back(from_integer(0, signedbv_typet{32})); + with_exprt with_reversed{ + with_reversed_inner, + make_member_name_expression("green"), + from_integer(0, signedbv_typet{32})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with_reversed), test.ns); REQUIRE(encoded == expected); @@ -331,25 +333,28 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") test.ns); SECTION("Operands in field order") { - with_exprt with_in_order{ + with_exprt with_in_order_inner{ symbol_expr, make_member_name_expression("green"), from_integer(0, signedbv_typet{32})}; - with_in_order.operands().push_back(make_member_name_expression("ham")); - with_in_order.operands().push_back(from_integer(1, signedbv_typet{24})); + with_exprt with_in_order{ + with_in_order_inner, + make_member_name_expression("ham"), + from_integer(1, signedbv_typet{24})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with_in_order), test.ns); REQUIRE(encoded == expected); } SECTION("Operands in reverse order vs fields") { - with_exprt with_reversed{ + with_exprt with_reversed_inner{ symbol_expr, make_member_name_expression("ham"), from_integer(1, signedbv_typet{24})}; - with_reversed.operands().push_back( - make_member_name_expression("green")); - with_reversed.operands().push_back(from_integer(0, signedbv_typet{32})); + with_exprt with_reversed{ + with_reversed_inner, + make_member_name_expression("green"), + from_integer(0, signedbv_typet{32})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with_reversed), test.ns); REQUIRE(encoded == expected); @@ -366,25 +371,28 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") test.ns); SECTION("Operands in field order") { - with_exprt with_in_order{ + with_exprt with_in_order_inner{ symbol_expr, make_member_name_expression("eggs"), from_integer(0, unsignedbv_typet{16})}; - with_in_order.operands().push_back(make_member_name_expression("ham")); - with_in_order.operands().push_back(from_integer(1, signedbv_typet{24})); + with_exprt with_in_order{ + with_in_order_inner, + make_member_name_expression("ham"), + from_integer(1, signedbv_typet{24})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with_in_order), test.ns); REQUIRE(encoded == expected); } SECTION("Operands in reverse order vs fields") { - with_exprt with_reversed{ + with_exprt with_reversed_inner{ symbol_expr, make_member_name_expression("ham"), from_integer(1, signedbv_typet{24})}; - with_reversed.operands().push_back(make_member_name_expression("eggs")); - with_reversed.operands().push_back( - from_integer(0, unsignedbv_typet{16})); + with_exprt with_reversed{ + with_reversed_inner, + make_member_name_expression("eggs"), + from_integer(0, unsignedbv_typet{16})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with_reversed), test.ns); REQUIRE(encoded == expected); @@ -401,28 +409,36 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") test.ns); SECTION("Operands in field order") { - with_exprt with{ + with_exprt with_innermost{ symbol_expr, make_member_name_expression("green"), from_integer(1, signedbv_typet{32})}; - with.operands().push_back(make_member_name_expression("eggs")); - with.operands().push_back(from_integer(2, unsignedbv_typet{16})); - with.operands().push_back(make_member_name_expression("ham")); - with.operands().push_back(from_integer(3, signedbv_typet{24})); + with_exprt with_inner{ + with_innermost, + make_member_name_expression("eggs"), + from_integer(2, unsignedbv_typet{16})}; + with_exprt with{ + with_inner, + make_member_name_expression("ham"), + from_integer(3, signedbv_typet{24})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with), test.ns); REQUIRE(encoded == expected); } SECTION("Operands out of order vs fields") { - with_exprt with{ + with_exprt with_innermost{ symbol_expr, make_member_name_expression("eggs"), from_integer(2, unsignedbv_typet{16})}; - with.operands().push_back(make_member_name_expression("ham")); - with.operands().push_back(from_integer(3, signedbv_typet{24})); - with.operands().push_back(make_member_name_expression("green")); - with.operands().push_back(from_integer(1, signedbv_typet{32})); + with_exprt with_inner{ + with_innermost, + make_member_name_expression("ham"), + from_integer(3, signedbv_typet{24})}; + with_exprt with{ + with_inner, + make_member_name_expression("green"), + from_integer(1, signedbv_typet{32})}; const exprt encoded = simplify_expr(test.struct_encoding.encode(with), test.ns); REQUIRE(encoded == expected); diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index a81069e8a99..5fd0a855875 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -766,14 +766,16 @@ TEST_CASE( const auto original_array_symbol = make_test_symbol("original_array", array_type); const auto result_array_symbol = make_test_symbol("result_array", array_type); - with_exprt with_expr{ + with_exprt with_expr_innermost{ original_array_symbol.symbol_expr(), from_integer(0, index_type), from_integer(0, value_type)}; - with_expr.add_to_operands( - from_integer(1, index_type), from_integer(1, value_type)); - with_expr.add_to_operands( - from_integer(2, index_type), from_integer(2, value_type)); + with_exprt with_expr_inner{ + with_expr_innermost, + from_integer(1, index_type), + from_integer(1, value_type)}; + with_exprt with_expr{ + with_expr_inner, from_integer(2, index_type), from_integer(2, value_type)}; const equal_exprt equal_expr{result_array_symbol.symbol_expr(), with_expr}; test.sent_commands.clear(); test.procedure.set_to(equal_expr, true);