Add struct encoding class

Author: thomasspriggs

src/solvers/Makefile

@@ -210,6 +210,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
+      smt2_incremental/struct_encoding.cpp \
       smt2_incremental/theories/smt_array_theory.cpp \
       smt2_incremental/theories/smt_bit_vector_theory.cpp \
       smt2_incremental/theories/smt_core_theory.cpp \

src/solvers/smt2_incremental/struct_encoding.cpp

@@ -0,0 +1,42 @@
+// Author: Diffblue Ltd.
+
+#include "struct_encoding.h"
+
+#include <util/bitvector_types.h>
+#include <util/make_unique.h>
+
+#include <solvers/flattening/boolbv_width.h>
+
+#include <queue>
+
+struct_encodingt::struct_encodingt(const namespacet &ns)
+  : boolbv_width{util_make_unique<boolbv_widtht>(ns)}
+{
+}
+
+struct_encodingt::struct_encodingt(const struct_encodingt &other)
+  : boolbv_width{util_make_unique<boolbv_widtht>(*other.boolbv_width)}
+{
+}
+
+struct_encodingt::~struct_encodingt() = default;
+
+typet struct_encodingt::encode(typet type) const
+{
+  std::queue<typet *> work_queue;
+  work_queue.push(&type);
+  while(!work_queue.empty())
+  {
+    typet &current = *work_queue.front();
+    work_queue.pop();
+    if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(current))
+    {
+      current = bv_typet{(*boolbv_width)(*struct_tag)};
+    }
+    if(const auto array = type_try_dynamic_cast<array_typet>(current))
+    {
+      work_queue.push(&array->element_type());
+    }
+  }
+  return type;
+}

src/solvers/smt2_incremental/struct_encoding.h

@@ -0,0 +1,27 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
+
+#include <util/type.h> // For passing `typet` by value. // IWYU pragma: keep
+
+#include <memory>
+
+class namespacet;
+class boolbv_widtht;
+
+/// Encodes struct types/values into non-struct expressions/types.
+class struct_encodingt final
+{
+public:
+  explicit struct_encodingt(const namespacet &ns);
+  struct_encodingt(const struct_encodingt &other);
+  ~struct_encodingt();
+
+  typet encode(typet type) const;
+
+private:
+  std::unique_ptr<boolbv_widtht> boolbv_width;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H

unit/Makefile

@@ -114,6 +114,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_object_size.cpp \
        solvers/smt2_incremental/smt_response_validation.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \
+       solvers/smt2_incremental/struct_encoding.cpp \
        solvers/smt2_incremental/theories/smt_array_theory.cpp \
        solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/theories/smt_core_theory.cpp \

unit/solvers/smt2_incremental/struct_encoding.cpp

@@ -0,0 +1,85 @@
+// Author: Diffblue Ltd.
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+#include <solvers/smt2_incremental/struct_encoding.h>
+#include <testing-utils/use_catch.h>
+
+struct struct_encoding_test_environmentt
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  struct_encodingt struct_encoding{ns};
+
+  static struct_encoding_test_environmentt make()
+  {
+    return {};
+  }
+
+private:
+  struct_encoding_test_environmentt() = default;
+};
+
+TEST_CASE(
+  "struct encoding of non-stuct type is a no-op",
+  "[core][smt2_incremental]")
+{
+  auto test = struct_encoding_test_environmentt::make();
+  typet input = signedbv_typet{8};
+  REQUIRE(test.struct_encoding.encode(input) == input);
+}
+
+TEST_CASE("struct encoding of struct_tag_type", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+  struct_typet struct_type{components};
+  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  struct_tag_typet struct_tag{type_symbol.name};
+  REQUIRE(test.struct_encoding.encode(struct_tag) == bv_typet{24});
+}
+
+TEST_CASE("struct encoding of array of structs", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+  struct_typet struct_type{components};
+  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  struct_tag_typet struct_tag{type_symbol.name};
+  const auto index_type = signedbv_typet{32};
+  const auto array_size = from_integer(5, index_type);
+  array_typet array_of_struct{struct_tag, array_size};
+  array_typet expected_encoded_array{bv_typet{24}, array_size};
+  REQUIRE(
+    test.struct_encoding.encode(array_of_struct) == expected_encoded_array);
+}
+
+TEST_CASE(
+  "struct encoding of array of array of structs",
+  "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+  struct_typet struct_type{components};
+  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  struct_tag_typet struct_tag{type_symbol.name};
+  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{struct_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{24}, array_size_inner}, array_size_outer};
+  REQUIRE(
+    test.struct_encoding.encode(array_of_array_of_struct) ==
+    expected_encoded_array);
+}