Merge pull request #7754 from thomasspriggs/tas/fix_single_member_structs

Fix support for single member structs in incremental SMT decision procedure

Author: thomasspriggs

regression/cbmc/Initialization7/test.desc

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

src/solvers/smt2_incremental/struct_encoding.cpp

@@ -32,7 +32,10 @@ typet struct_encodingt::encode(typet type) const
     work_queue.pop();
     if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(current))
     {
-      current = bv_typet{(*boolbv_width)(*struct_tag)};
+      const auto width = (*boolbv_width)(*struct_tag);
+      if(width == 0)
+        UNIMPLEMENTED_FEATURE("support for zero bit width structs.");
+      current = bv_typet{width};
     }
     if(const auto array = type_try_dynamic_cast<array_typet>(current))
     {
@@ -44,6 +47,11 @@ typet struct_encodingt::encode(typet type) const
 
 static exprt encode(const struct_exprt &struct_expr)
 {
+  INVARIANT(
+    !struct_expr.operands().empty(),
+    "empty structs may not be encoded into SMT terms.");
+  if(struct_expr.operands().size() == 1)
+    return struct_expr.operands().front();
   return concatenation_exprt{struct_expr.operands(), struct_expr.type()};
 }
 

unit/solvers/smt2_incremental/struct_encoding.cpp

@@ -105,3 +105,35 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
     REQUIRE(test.struct_encoding.encode(struct_expr) == expected_result);
   }
 }
+
+TEST_CASE(
+  "encoding of single member struct expressions",
+  "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst component_types{
+    {"eggs", signedbv_typet{32}}};
+  const type_symbolt type_symbol{"foot", struct_typet{component_types}, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  const struct_tag_typet struct_tag{type_symbol.name};
+  const symbolt struct_value_symbol{"foo", struct_tag, ID_C};
+  test.symbol_table.insert(struct_value_symbol);
+  const auto symbol_expr = struct_value_symbol.symbol_expr();
+  const auto symbol_expr_as_bv = symbol_exprt{"foo", bv_typet{32}};
+  SECTION("struct typed symbol expression")
+  {
+    REQUIRE(test.struct_encoding.encode(symbol_expr) == symbol_expr_as_bv);
+  }
+  SECTION("struct equality expression")
+  {
+    const auto struct_equal = equal_exprt{symbol_expr, symbol_expr};
+    const auto bv_equal = equal_exprt{symbol_expr_as_bv, symbol_expr_as_bv};
+    REQUIRE(test.struct_encoding.encode(struct_equal) == bv_equal);
+  }
+  SECTION("expression for a struct from (single item) list of components")
+  {
+    const auto dozen = from_integer(12, signedbv_typet{32});
+    const struct_exprt struct_expr{{dozen}, struct_tag};
+    REQUIRE(test.struct_encoding.encode(struct_expr) == dozen);
+  }
+}