Merge pull request #7839 from thomasspriggs/tas/smt_empty_structs

Add empty struct support to incremental SMT decision procedure

Author: thomasspriggs

regression/cbmc/CMakeLists.txt

@@ -34,7 +34,7 @@ add_test_pl_profile(
 add_test_pl_profile(
   "cbmc-new-smt-backend"
   "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-  "-I;new-smt-backend;-s;new-smt-backend"
+  "${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
   "CORE"
 )
 

regression/cbmc/Empty_struct1/test.desc

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

regression/cbmc/Empty_struct2/test.desc

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

regression/cbmc/Empty_struct3/test.desc

@@ -1,4 +1,4 @@
-CORE gcc-only
+CORE gcc-only new-smt-backend
 main.c
 --json-ui
 VERIFICATION FAILED

regression/cbmc/empty_compound_type1/test.desc

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

regression/cbmc/empty_compound_type2/test.desc

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

regression/cbmc/empty_compound_type3/test.desc

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

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()};

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -497,14 +497,15 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
     {
       return identifier_descriptor;
     }
-    if(gather_dependent_expressions(expr).empty())
+    const exprt lowered = lower(expr);
+    if(gather_dependent_expressions(lowered).empty())
     {
       INVARIANT(
-        objects_are_already_tracked(expr, object_map),
+        objects_are_already_tracked(lowered, object_map),
         "Objects in expressions being read should already be tracked from "
         "point of being set/handled.");
       return ::convert_expr_to_smt(
-        expr,
+        lowered,
         object_map,
         pointer_sizes_map,
         object_size_function.make_application,

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,62 @@ 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();
+
+  INFO("Getting values involving empty structs.");
+  test.mock_responses.push_front(
+    smt_get_value_responset{{{expected_handle, smt_bool_literal_termt{true}}}});
+  CHECK(test.procedure.get(equality_expression) == true_exprt{});
+  test.mock_responses.push_front(smt_get_value_responset{
+    {{smt_identifier_termt{"foo", smt_bit_vector_sortt{8}},
+      smt_bit_vector_constant_termt{0, 8}}}});
+  const struct_exprt expected_empty{{}, type_reference};
+  CHECK(test.procedure.get(foo.symbol_expr()) == expected_empty);
+  const std::vector<smt_commandt> expected_get_commands{
+    smt_get_value_commandt{expected_handle},
+    smt_get_value_commandt{expected_foo}};
+  CHECK(test.sent_commands == expected_get_commands);
+}