Merge pull request #7951 from thomasspriggs/tas/smt_struct_of_struct

Fix SMT encoding of structs which contain a single struct field

Author: thomasspriggs

regression/cbmc/Struct_Initialization5/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -203,19 +203,31 @@ exprt struct_encodingt::encode(exprt expr) const
   while(!work_queue.empty())
   {
     exprt &current = *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<with_exprt>(current))
       if(can_cast_type<struct_tag_typet>(current.type()))
         current = ::encode(*with_expr, ns);
     current.type() = encode(current.type());
+    optionalt<exprt> update;
     if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
-      current = ::encode(*struct_expr);
+      update = ::encode(*struct_expr);
     if(const auto union_expr = expr_try_dynamic_cast<union_exprt>(current))
-      current = ::encode(*union_expr, *boolbv_width);
+      update = ::encode(*union_expr, *boolbv_width);
     if(const auto member_expr = expr_try_dynamic_cast<member_exprt>(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);
   }

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")
   {