From bafaddcc1d5159d5912b97dcc2d658e91fd1cd34 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 11 Oct 2023 17:37:50 +0100 Subject: [PATCH 1/2] Fix encoding of structs which contain a single struct field In the case where a struct contains a single struct typed field, then the construction of the outer class is encoded into the construction of the inner class which then itself needs to be encoded. Therefore the result of the encoding itself may need encoding. This general solution will also avoid further variations on the same issue such as constructing unions containing structs, or selecting struct fields from a union etc. --- .../encoding/struct_encoding.cpp | 20 +++++++++++++++---- .../encoding/struct_encoding.cpp | 12 +++++++++++ 2 files changed, 28 insertions(+), 4 deletions(-) diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index b761a00fc19..07c8dddbf92 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -203,19 +203,31 @@ exprt struct_encodingt::encode(exprt expr) const while(!work_queue.empty()) { exprt ¤t = *work_queue.front(); - work_queue.pop(); // Note that "with" expressions are handled before type encoding in order to // facilitate checking that they are applied to structs rather than arrays. if(const auto with_expr = expr_try_dynamic_cast(current)) if(can_cast_type(current.type())) current = ::encode(*with_expr, ns); current.type() = encode(current.type()); + optionalt update; if(const auto struct_expr = expr_try_dynamic_cast(current)) - current = ::encode(*struct_expr); + update = ::encode(*struct_expr); if(const auto union_expr = expr_try_dynamic_cast(current)) - current = ::encode(*union_expr, *boolbv_width); + update = ::encode(*union_expr, *boolbv_width); if(const auto member_expr = expr_try_dynamic_cast(current)) - current = encode_member(*member_expr); + update = encode_member(*member_expr); + if(update) + { + INVARIANT( + current != *update, + "Updates in struct encoding are expected to be a change of state."); + current = std::move(*update); + // Repeat on the updated node until we reach a fixed point. This is needed + // because the encoding of an outer struct/union may be initially + // expressed in terms of an inner struct/union which it contains. + continue; + } + work_queue.pop(); for(auto &operand : current.operands()) work_queue.push(&operand); } diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp index 30b98c5ef27..d6f523b129c 100644 --- a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -169,6 +169,18 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") const concatenation_exprt expected_result{ {green_ham.symbol_expr(), forty_two, minus_one}, bv_typet{72}}; REQUIRE(test.struct_encoding.encode(struct_expr) == expected_result); + SECTION("struct containing a single struct") + { + const struct_typet struct_struct_type{ + struct_union_typet::componentst{{"inner", struct_tag}}}; + const type_symbolt struct_struct_type_symbol{ + "struct_structt", struct_type, ID_C}; + test.symbol_table.insert(type_symbol); + const struct_tag_typet struct_struct_tag{type_symbol.name}; + const struct_exprt struct_struct{ + exprt::operandst{struct_expr}, struct_struct_tag}; + REQUIRE(test.struct_encoding.encode(struct_struct) == expected_result); + } } SECTION("member expression selecting a data member of a struct") { From 7eab7ac6e6e375ca4fc1759845c57cac1549485d Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 11 Oct 2023 18:55:38 +0100 Subject: [PATCH 2/2] Switch on smt test fixed by struct of single struct support --- regression/cbmc/Struct_Initialization5/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc/Struct_Initialization5/test.desc b/regression/cbmc/Struct_Initialization5/test.desc index 9efefbc7362..f4cb0fa5f29 100644 --- a/regression/cbmc/Struct_Initialization5/test.desc +++ b/regression/cbmc/Struct_Initialization5/test.desc @@ -1,4 +1,4 @@ -CORE +CORE new-smt-backend main.c ^EXIT=0$