Encode empty structs as as zero byte

Author: thomasspriggs

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -2,6 +2,7 @@
 
 #include "struct_encoding.h"
 
+#include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/make_unique.h>
@@ -38,9 +39,14 @@ typet struct_encodingt::encode(typet type) const
     work_queue.pop();
     if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(current))
     {
-      const auto width = (*boolbv_width)(*struct_tag);
+      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)
-        UNIMPLEMENTED_FEATURE("support for zero bit width structs.");
+        width = 8;
       current = bv_typet{width};
     }
     if(const auto array = type_try_dynamic_cast<array_typet>(current))
@@ -102,11 +108,16 @@ static exprt encode(const with_exprt &with, const namespacet &ns)
   return struct_exprt{components, tag_type};
 }
 
+/// Non-empty structs are flattened into a large bit vector using concatenation
+/// to express all the member operands of \p struct_expr. Empty structs are
+/// encoded as a zero byte. This has useful properties such as -
+///   * A zero byte is valid SMT, unlike zero length bit vectors.
+///   * Any two zero byte instances are always equal. This property would not
+///     be true of two instances of a non-det byte for instance.
 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().empty())
+    return from_integer(0, bv_typet{8});
   if(struct_expr.operands().size() == 1)
     return struct_expr.operands().front();
   return concatenation_exprt{struct_expr.operands(), struct_expr.type()};

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -341,6 +341,34 @@ TEST_CASE("decoding into struct expressions.", "[core][smt2_incremental]")
   REQUIRE(test.struct_encoding.decode(encoded, struct_tag) == expected);
 }
 
+TEST_CASE("encoding of struct with no members", "[core][smt2_incremental]")
+{
+  auto test = struct_encoding_test_environmentt::make();
+  const struct_union_typet::componentst component_types{};
+  const type_symbolt type_symbol{"emptyt", struct_typet{component_types}, ID_C};
+  test.symbol_table.insert(type_symbol);
+  const struct_tag_typet type_reference{type_symbol.name};
+  const auto expected_type = bv_typet{8};
+  const auto expected_zero_byte = from_integer(0, expected_type);
+  SECTION("Type of empty struct")
+  {
+    REQUIRE(test.struct_encoding.encode(type_reference) == expected_type);
+  }
+  SECTION("Empty struct typed symbol expression")
+  {
+    const symbolt empty_value_symbol{"foo", type_reference, ID_C};
+    test.symbol_table.insert(empty_value_symbol);
+    const auto symbol_expr = empty_value_symbol.symbol_expr();
+    const exprt expected_symbol = symbol_exprt{"foo", expected_type};
+    REQUIRE(test.struct_encoding.encode(symbol_expr) == expected_symbol);
+  }
+  SECTION("Struct expression")
+  {
+    const struct_exprt empty{{}, type_reference};
+    REQUIRE(test.struct_encoding.encode(empty) == expected_zero_byte);
+  }
+}
+
 TEST_CASE(
   "encoding of single member struct expressions",
   "[core][smt2_incremental]")

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -1000,3 +1000,48 @@ TEST_CASE(
 
   REQUIRE(returned == constant_exprt{"true", bool_typet{}});
 }
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret getting value of empty struct",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  const struct_union_typet::componentst component_types{};
+  const type_symbolt type_symbol{"emptyt", struct_typet{component_types}, ID_C};
+  test.symbol_table.insert(type_symbol);
+  const struct_tag_typet type_reference{type_symbol.name};
+  const symbolt foo{"foo", type_reference, ID_C};
+  test.symbol_table.insert(foo);
+  const symbolt bar{"bar", type_reference, ID_C};
+  test.symbol_table.insert(bar);
+
+  INFO("Sanity checking decision procedure and flushing size definitions");
+  test.mock_responses.push_front(smt_check_sat_responset{smt_sat_responset{}});
+  CHECK(test.procedure() == decision_proceduret::resultt::D_SATISFIABLE);
+  test.sent_commands.clear();
+
+  INFO("Defining an equality over empty structs");
+  const auto equality_expression =
+    test.procedure.handle(equal_exprt{foo.symbol_expr(), bar.symbol_expr()});
+  test.procedure.set_to(equality_expression, true);
+  const smt_identifier_termt expected_foo{"foo", smt_bit_vector_sortt{8}};
+  const smt_identifier_termt expected_bar{"bar", smt_bit_vector_sortt{8}};
+  const smt_identifier_termt expected_handle{"B0", smt_bool_sortt{}};
+  const smt_termt expected_equality =
+    smt_core_theoryt::equal(expected_foo, expected_bar);
+  const std::vector<smt_commandt> expected_problem_commands{
+    smt_declare_function_commandt{expected_foo, {}},
+    smt_declare_function_commandt{expected_bar, {}},
+    smt_define_function_commandt{"B0", {}, expected_equality},
+    smt_assert_commandt{expected_equality}};
+  REQUIRE(test.sent_commands == expected_problem_commands);
+  test.sent_commands.clear();
+
+  INFO("Ensuring decision procedure is in suitable state for getting output.");
+  const std::vector<smt_commandt> expected_check_commands{
+    smt_check_sat_commandt{}};
+  test.mock_responses.push_front(smt_check_sat_responset{smt_sat_responset{}});
+  REQUIRE(test.procedure() == decision_proceduret::resultt::D_SATISFIABLE);
+  CHECK(test.sent_commands == expected_check_commands);
+  test.sent_commands.clear();
+}