Tests for incremental SMT2 solver enum support

Author: Enrico Steffinlongo

unit/Makefile

@@ -115,6 +115,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_response_validation.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \
        solvers/smt2_incremental/encoding/struct_encoding.cpp \
+       solvers/smt2_incremental/encoding/enum_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/construct_value_expr_from_smt.cpp

@@ -31,10 +31,39 @@ static mp_integer max_int(const std::size_t bits)
   return power2(bits) - 1;
 }
 
+static type_symbolt make_c_enum_type_symbol(std::size_t underlying_size)
+{
+  const signedbv_typet underlying_type{underlying_size};
+  c_enum_typet enum_type{underlying_type};
+
+  auto &members = enum_type.add(ID_body).get_sub();
+
+  for(unsigned int i = 0; i < 20; ++i)
+  {
+    c_enum_typet::c_enum_membert member;
+    member.set_identifier("V" + std::to_string(i));
+    member.set_base_name("V" + std::to_string(i));
+    member.set_value(integer2bvrep(i, underlying_size));
+    members.push_back(member);
+  }
+  return type_symbolt{"my_enum", enum_type, ID_C};
+}
+
+static symbolt make_c_enum_tag_instance_symbol(const symbolt &enum_type_symbol)
+{
+  const c_enum_tag_typet enum_tag{enum_type_symbol.name};
+  return symbolt{"my_enum_value", enum_tag, ID_C};
+}
+
 TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
 {
-  const symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   const namespacet ns{symbol_table};
+  const symbolt enum_type_symbol = make_c_enum_type_symbol(42);
+  const symbolt enum_tag_value_symbol =
+    make_c_enum_tag_instance_symbol(enum_type_symbol);
+  symbol_table.insert(enum_type_symbol);
+  symbol_table.insert(enum_tag_value_symbol);
   optionalt<smt_termt> input_term;
   optionalt<exprt> expected_result;
 
@@ -66,7 +95,7 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
        from_integer(-1, signedbv_typet{(bits)})}
   // clang-format on
 
-  std::tie(input_term, expected_result) = GENERATE(
+  std::tie(input_term, expected_result) = GENERATE_REF(
     rowt{smt_bool_literal_termt{true}, true_exprt{}},
     rowt{smt_bool_literal_termt{false}, false_exprt{}},
     rowt{smt_bit_vector_constant_termt{0, 8}, from_integer(0, c_bool_typet(8))},
@@ -81,6 +110,9 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
       smt_bit_vector_constant_termt{12, 64},
       constant_exprt(
         integer2bvrep(12, 64), pointer_typet(void_type(), 64 /* bits */))},
+    rowt{
+      smt_bit_vector_constant_termt{2, 42},
+      constant_exprt{"2", c_enum_tag_typet{enum_type_symbol.name}}},
     UNSIGNED_BIT_VECTOR_TESTS(8),
     SIGNED_BIT_VECTOR_TESTS(8),
     UNSIGNED_BIT_VECTOR_TESTS(16),
@@ -103,14 +135,19 @@ TEST_CASE(
   "Invariant violations in value expr construction from smt.",
   "[core][smt2_incremental]")
 {
-  const symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   const namespacet ns{symbol_table};
+  const symbolt enum_type_symbol = make_c_enum_type_symbol(5);
+  const symbolt enum_tag_value_symbol =
+    make_c_enum_tag_instance_symbol(enum_type_symbol);
+  symbol_table.insert(enum_type_symbol);
+  symbol_table.insert(enum_tag_value_symbol);
   optionalt<smt_termt> input_term;
   optionalt<typet> input_type;
   std::string invariant_reason;
 
   using rowt = std::tuple<smt_termt, typet, std::string>;
-  std::tie(input_term, input_type, invariant_reason) = GENERATE(
+  std::tie(input_term, input_type, invariant_reason) = GENERATE_REF(
     rowt{
       smt_bool_literal_termt{true},
       unsignedbv_typet{16},
@@ -147,7 +184,17 @@ TEST_CASE(
     rowt{
       smt_bit_vector_constant_termt{0, 16},
       pointer_typet{unsigned_int_type(), 0},
-      "Width of smt bit vector term must match the width of pointer type"});
+      "Width of smt bit vector term must match the width of pointer type"},
+    rowt{
+      smt_bit_vector_constant_termt{2, 42},
+      c_enum_tag_typet{"foo"},
+      "we are assuming that a name exists in the namespace when this function "
+      "is called - identifier foo was not found"},
+    rowt{
+      smt_bit_vector_constant_termt{8796093022208ul, 64},
+      enum_tag_value_symbol.type,
+      "Width of smt bit vector term must match the width of bit vector "
+      "underlying type of the original c_enum type."});
   SECTION(invariant_reason)
   {
     const cbmc_invariants_should_throwt invariants_throw;

unit/solvers/smt2_incremental/encoding/enum_encoding.cpp

@@ -0,0 +1,108 @@
+// Author: Diffblue Ltd.
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/c_types.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+#include <solvers/smt2_incremental/encoding/enum_encoding.h>
+#include <testing-utils/use_catch.h>
+
+static c_enum_typet make_c_enum_type(
+  const unsignedbv_typet &underlying_type,
+  unsigned int value_count)
+{
+  c_enum_typet enum_type{underlying_type};
+
+  auto &members = enum_type.add(ID_body).get_sub();
+
+  for(unsigned int i = 0; i < value_count; ++i)
+  {
+    c_enum_typet::c_enum_membert member;
+    member.set_identifier("V" + std::to_string(i));
+    member.set_base_name("V" + std::to_string(i));
+    member.set_value(integer2bvrep(i, underlying_type.get_width()));
+    members.push_back(member);
+  }
+  return enum_type;
+}
+
+constant_exprt create_enum_tag_typed_constant(
+  const mp_integer &value,
+  const c_enum_typet &enum_type,
+  const c_enum_tag_typet &enum_tag_type)
+{
+  constant_exprt constant = from_integer(value, enum_type);
+  constant.type() = enum_tag_type;
+  return constant;
+}
+
+TEST_CASE("enum encoding of expressions", "[core][smt2_incremental]")
+{
+  std::size_t size;
+  int value_count;
+  using rowt = std::pair<int, int>;
+  std::tie(size, value_count) = GENERATE(
+    rowt{32, 42},
+    rowt{64, 42},
+    rowt{42, 42},
+    rowt{2, 42},
+    rowt{1, 42},
+    rowt{42, 1},
+    rowt{42, 0});
+
+  INFO(
+    "Checking enum of underlying size " + std::to_string(size) + " with " +
+    std::to_string(value_count) + " elements");
+
+  const unsignedbv_typet enum_underlying_type{size};
+  const c_enum_typet enum_type =
+    make_c_enum_type(enum_underlying_type, value_count);
+  const type_symbolt enum_symbol{"my_enum", enum_type, ID_C};
+  symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+  symbol_table.insert(enum_symbol);
+  const c_enum_tag_typet enum_tag{enum_symbol.name};
+  const symbolt enum_value_symbol{"my_enum_value", enum_tag, ID_C};
+  symbol_table.insert(enum_value_symbol);
+  const auto symbol_expr = enum_value_symbol.symbol_expr();
+  const auto symbol_expr_as_bv =
+    symbol_exprt{"my_enum_value", unsignedbv_typet{size}};
+
+  SECTION("enum lowering of non-enum type is a no-op")
+  {
+    constant_exprt expr = from_integer(10, signedbv_typet{42});
+    REQUIRE(lower_enum(expr, ns) == expr);
+  }
+
+  SECTION("enum_tag typed symbol expression")
+  {
+    REQUIRE(lower_enum(symbol_expr, ns) == symbol_expr_as_bv);
+  }
+
+  SECTION("enum_tag equality expression")
+  {
+    const auto enum_equal = equal_exprt{symbol_expr, symbol_expr};
+    const auto expected_bv_equal =
+      equal_exprt{symbol_expr_as_bv, symbol_expr_as_bv};
+    REQUIRE(lower_enum(enum_equal, ns) == expected_bv_equal);
+  }
+
+  SECTION("enum_tag in array")
+  {
+    const array_typet original_array_type{
+      enum_tag, from_integer(2, unsignedbv_typet{32})};
+    const array_typet lowered_array_type{
+      enum_underlying_type, from_integer(2, unsignedbv_typet{32})};
+    const array_exprt original_array_expr{
+      {create_enum_tag_typed_constant(3, enum_type, enum_tag),
+       create_enum_tag_typed_constant(3, enum_type, enum_tag)},
+      original_array_type};
+    const array_exprt expected_array_expr{
+      {from_integer(3, unsignedbv_typet{size}),
+       from_integer(3, unsignedbv_typet{size})},
+      lowered_array_type};
+    REQUIRE(lower_enum(original_array_expr, ns) == expected_array_expr);
+  }
+}