Merge pull request #7914 from thomasspriggs/tas/smt_union_tag

Encode union tag types in smt2 decision procedure

Author: thomasspriggs

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -5,6 +5,7 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
 #include <util/make_unique.h>
 #include <util/namespace.h>
 #include <util/range.h>
@@ -29,6 +30,19 @@ struct_encodingt::struct_encodingt(const struct_encodingt &other)
 
 struct_encodingt::~struct_encodingt() = default;
 
+/// If the given \p type needs re-encoding as a bit-vector then this function
+/// \returns the width of the new bitvector type. The width calculation is
+/// delegated to \p boolbv_width.
+static optionalt<std::size_t>
+needs_width(const typet &type, const boolbv_widtht &boolbv_width)
+{
+  if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(type))
+    return boolbv_width(*struct_tag);
+  if(const auto union_tag = type_try_dynamic_cast<union_tag_typet>(type))
+    return boolbv_width(*union_tag);
+  return {};
+}
+
 typet struct_encodingt::encode(typet type) const
 {
   std::queue<typet *> work_queue;
@@ -37,17 +51,16 @@ typet struct_encodingt::encode(typet type) const
   {
     typet &current = *work_queue.front();
     work_queue.pop();
-    if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(current))
+    if(auto assigned_bit_width = needs_width(current, *boolbv_width))
     {
-      auto width = (*boolbv_width)(*struct_tag);
       // The bit vector theory of SMT disallows zero bit length length bit
       // vectors. C++ gives a minimum size for a struct (even an empty struct)
       // as being one byte; in order to ensure that structs have unique memory
       // locations. Therefore encoding empty structs as having 8 bits / 1 byte
       // is a reasonable solution in this case.
-      if(width == 0)
-        width = 8;
-      current = bv_typet{width};
+      if(*assigned_bit_width == 0)
+        assigned_bit_width = 8;
+      current = bv_typet{*assigned_bit_width};
     }
     if(const auto array = type_try_dynamic_cast<array_typet>(current))
     {

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -3,6 +3,7 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
 #include <util/mathematical_types.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
@@ -71,6 +72,58 @@ TEST_CASE("struct encoding of types", "[core][smt2_incremental]")
   }
 }
 
+TEST_CASE("Encoding of union types", "[core][smt2_incremental]")
+{
+  auto test = struct_encoding_test_environmentt::make();
+  SECTION("Two components")
+  {
+    const struct_union_typet::componentst components{
+      {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+    union_typet union_type{components};
+    type_symbolt type_symbol{"my_uniont", union_type, ID_C};
+    test.symbol_table.insert(type_symbol);
+    union_tag_typet union_tag{type_symbol.name};
+    SECTION("Direct union_tag_type encoding")
+    {
+      REQUIRE(test.struct_encoding.encode(union_tag) == bv_typet{16});
+    }
+    SECTION("Array of unions encoding")
+    {
+      const auto index_type = signedbv_typet{32};
+      const auto array_size = from_integer(5, index_type);
+      array_typet array_of_struct{union_tag, array_size};
+      array_typet expected_encoded_array{bv_typet{16}, array_size};
+      REQUIRE(
+        test.struct_encoding.encode(array_of_struct) == expected_encoded_array);
+    }
+    SECTION("Array of array of unions encoding")
+    {
+      const auto index_type = signedbv_typet{32};
+      const auto array_size_inner = from_integer(4, index_type);
+      const auto array_size_outer = from_integer(2, index_type);
+      array_typet array_of_struct{union_tag, array_size_inner};
+      array_typet array_of_array_of_struct{array_of_struct, array_size_outer};
+      array_typet expected_encoded_array{
+        array_typet{bv_typet{16}, array_size_inner}, array_size_outer};
+      REQUIRE(
+        test.struct_encoding.encode(array_of_array_of_struct) ==
+        expected_encoded_array);
+    }
+  }
+  SECTION("Empty union")
+  {
+    const struct_union_typet::componentst components{};
+    union_typet union_type{components};
+    type_symbolt type_symbol{"my_empty_uniont", union_type, ID_C};
+    test.symbol_table.insert(type_symbol);
+    union_tag_typet union_tag{type_symbol.name};
+    SECTION("Direct union_tag_type encoding")
+    {
+      REQUIRE(test.struct_encoding.encode(union_tag) == bv_typet{8});
+    }
+  }
+}
+
 exprt make_member_name_expression(const irep_idt component_name)
 {
   exprt result{ID_member_name};