Merge pull request #7990 from thomasspriggs/tas/smt_union_traces

Add support for union values in traces for incremental smt2 decision procedure

Author: thomasspriggs

regression/cbmc-incr-smt2/unions/padded.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdint.h>
+
+union my_uniont
+{
+  uint16_t a;
+  uint8_t b;
+};
+
+int main()
+{
+  union my_uniont my_union = {.b = 5};
+  assert(my_union.a == 5);
+}

regression/cbmc-incr-smt2/unions/padded.desc

@@ -0,0 +1,12 @@
+CORE
+padded.c
+--trace
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line 13 assertion my_union\.a \=\= 5\: FAILURE
+my_union\=\{ \.a\=\d+ \} \(\d{8} 00000101\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support union values and traces for a example where the trace
+should include non deterministic padding.

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -277,3 +277,30 @@ exprt struct_encodingt::decode(
   }
   return simplify_expr(struct_exprt{encoded_fields, original_type}, ns);
 }
+
+exprt struct_encodingt::decode(
+  const exprt &encoded,
+  const union_tag_typet &original_type) const
+{
+  INVARIANT(
+    can_cast_type<bv_typet>(encoded.type()),
+    "Unions are expected to be encoded into bit vectors.");
+  const union_typet definition = ns.get().follow_tag(original_type);
+  const auto &components = definition.components();
+  if(components.empty())
+    return empty_union_exprt{original_type};
+  // A union expression is built here using the first component in the
+  // declaration of the union. There may be better alternatives but this matches
+  // the SAT backend. See the case for `type.id() == ID_union` in
+  // `boolbvt::bv_get_rec`.
+  const auto &component_for_definition = components[0];
+  return simplify_expr(
+    union_exprt{
+      component_for_definition.get_name(),
+      typecast_exprt{
+        encode(member_exprt{
+          typecast_exprt{encoded, original_type}, component_for_definition}),
+        component_for_definition.type()},
+      original_type},
+    ns);
+}

src/solvers/smt2_incremental/encoding/struct_encoding.h

@@ -12,6 +12,7 @@ class namespacet;
 class boolbv_widtht;
 class member_exprt;
 class struct_tag_typet;
+class union_tag_typet;
 
 /// Encodes struct types/values into non-struct expressions/types.
 class struct_encodingt final
@@ -27,6 +28,8 @@ class struct_encodingt final
   /// from the bit vector \p encoded expression.
   exprt
   decode(const exprt &encoded, const struct_tag_typet &original_type) const;
+  exprt
+  decode(const exprt &encoded, const union_tag_typet &original_type) const;
 
 private:
   std::unique_ptr<boolbv_widtht> boolbv_width;

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -4,6 +4,7 @@
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/nodiscard.h>
 #include <util/range.h>
@@ -478,6 +479,17 @@ optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   return {struct_encoding.decode(*encoded_result, type)};
 }
 
+optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
+  const smt_termt &union_term,
+  const union_tag_typet &type) const
+{
+  const auto encoded_result =
+    get_expr(union_term, struct_encoding.encode(type));
+  if(!encoded_result)
+    return {};
+  return {struct_encoding.decode(*encoded_result, type)};
+}
+
 optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   const smt_termt &descriptor,
   const typet &type) const
@@ -492,6 +504,10 @@ optionalt<exprt> smt2_incremental_decision_proceduret::get_expr(
   {
     return get_expr(descriptor, *struct_type);
   }
+  if(const auto union_type = type_try_dynamic_cast<union_tag_typet>(type))
+  {
+    return get_expr(descriptor, *union_type);
+  }
   const smt_get_value_commandt get_value_command{descriptor};
   const smt_responset response = get_response_to_command(
     *solver_process, get_value_command, identifier_table);

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -23,6 +23,7 @@
 class namespacet;
 class smt_base_solver_processt; // IWYU pragma: keep
 class string_constantt;
+class union_tag_typet;
 
 class smt2_incremental_decision_proceduret final
   : public stack_decision_proceduret
@@ -60,6 +61,8 @@ class smt2_incremental_decision_proceduret final
   optionalt<exprt>
   get_expr(const smt_termt &struct_term, const struct_tag_typet &type) const;
   optionalt<exprt>
+  get_expr(const smt_termt &union_term, const union_tag_typet &type) const;
+  optionalt<exprt>
   get_expr(const smt_termt &array, const array_typet &type) const;
 
 protected:

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -418,6 +418,50 @@ TEST_CASE("decoding into struct expressions.", "[core][smt2_incremental]")
   REQUIRE(test.struct_encoding.decode(encoded, struct_tag) == expected);
 }
 
+TEST_CASE("decoding into union expressions.", "[core][smt2_incremental]")
+{
+  auto test = struct_encoding_test_environmentt::make();
+  SECTION("Single union component")
+  {
+    const struct_union_typet::componentst type_components{
+      {"eggs", unsignedbv_typet{16}}};
+    const union_typet union_type{type_components};
+    const type_symbolt type_symbol{"my_uniont", union_type, ID_C};
+    test.symbol_table.insert(type_symbol);
+    const union_tag_typet union_tag{type_symbol.name};
+    const union_exprt expected{
+      "eggs", from_integer(12, unsignedbv_typet{16}), union_tag};
+    const exprt encoded = from_integer(12, bv_typet{16});
+    REQUIRE(test.struct_encoding.decode(encoded, union_tag) == expected);
+  }
+  SECTION("Multiple union components")
+  {
+    const struct_union_typet::componentst type_components{
+      {"green", signedbv_typet{32}},
+      {"eggs", unsignedbv_typet{16}},
+      {"ham", signedbv_typet{24}}};
+    const union_typet union_type{type_components};
+    const type_symbolt type_symbol{"my_uniont", union_type, ID_C};
+    test.symbol_table.insert(type_symbol);
+    const union_tag_typet union_tag{type_symbol.name};
+    const union_exprt expected{
+      "green", from_integer(-42, signedbv_typet{32}), union_tag};
+    const exprt encoded = from_integer((~uint32_t{42} + 1), bv_typet{32});
+    REQUIRE(test.struct_encoding.decode(encoded, union_tag) == expected);
+  }
+  SECTION("Empty union")
+  {
+    const struct_union_typet::componentst type_components{};
+    const union_typet union_type{type_components};
+    const type_symbolt type_symbol{"my_empty_uniont", union_type, ID_C};
+    test.symbol_table.insert(type_symbol);
+    const union_tag_typet union_tag{type_symbol.name};
+    const empty_union_exprt expected{union_tag};
+    const exprt encoded = from_integer(0, bv_typet{8});
+    REQUIRE(test.struct_encoding.decode(encoded, union_tag) == expected);
+  }
+}
+
 TEST_CASE("encoding of struct with no members", "[core][smt2_incremental]")
 {
   auto test = struct_encoding_test_environmentt::make();

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -871,14 +871,28 @@ TEST_CASE(
   const auto foo_term = smt_identifier_termt{"foo", smt_bit_vector_sortt{32}};
   const auto padding_term =
     smt_identifier_termt{"padding_0", smt_bit_vector_sortt{24}};
-  const std::vector<smt_commandt> expected_commands{
+  const std::vector<smt_commandt> expected_set_commands{
     smt_declare_function_commandt{foo_term, {}},
     smt_declare_function_commandt{padding_term, {}},
     smt_assert_commandt{smt_core_theoryt::equal(
       foo_term,
       smt_bit_vector_theoryt::concat(
         padding_term, smt_bit_vector_constant_termt{12, 8}))}};
-  REQUIRE(test.sent_commands == expected_commands);
+  REQUIRE(test.sent_commands == expected_set_commands);
+
+  INFO("Ensuring decision procedure in suitable state for getting values.");
+  test.mock_responses.push_back(smt_check_sat_responset{smt_sat_responset{}});
+  test.procedure();
+
+  INFO("Getting union typed value.");
+  test.sent_commands.clear();
+  test.mock_responses.push_back(smt_get_value_responset{
+    {{foo_term, smt_bit_vector_constant_termt{~uint32_t{255} | 12, 32}}}});
+  const auto expected_value = union_exprt{"eggs", dozen, union_tag};
+  REQUIRE(test.procedure.get(symbol_expr) == expected_value);
+  const std::vector<smt_commandt> expected_get_commands{
+    smt_get_value_commandt{foo_term}};
+  REQUIRE(test.sent_commands == expected_get_commands);
 }
 
 TEST_CASE(