Merge pull request #7961 from thomasspriggs/tas/smt_union_member

Add support for union member expressions in incremental smt2 decision procedure

Author: thomasspriggs

regression/cbmc/Union_Initialization1/test.desc

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

regression/cbmc/Union_Initialization5/test.desc

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

regression/cbmc/union1/test.desc

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

regression/cbmc/union10/union_list2.desc

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

regression/cbmc/union11/union_list.desc

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

regression/cbmc/union13/no-arch.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arch none --little-endian
 (Starting CEGAR Loop|^Generated 1 VCC\(s\), 1 remaining after simplification$)

regression/cbmc/union13/test.desc

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

regression/cbmc/union14/test.desc

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

regression/cbmc/union15/test.desc

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

regression/cbmc/union16/test.desc

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

regression/cbmc/union18/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^Generated 1 VCC\(s\), 0 remaining after simplification$

regression/cbmc/union2/test.desc

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

regression/cbmc/union3/test.desc

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

regression/cbmc/union4/test.desc

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

regression/cbmc/union5/test.desc

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

regression/cbmc/union6/test.desc

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

regression/cbmc/union7/test.desc

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

regression/cbmc/union8/test.desc

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

regression/cbmc/union9/test.desc

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

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -176,19 +176,26 @@ static std::size_t count_trailing_bit_width(
     trailing_widths.begin(), trailing_widths.end(), std::size_t{0});
 }
 
-/// The member expression selects the value of a field from a struct. The
-/// struct is encoded as a single bitvector where the first field is stored
+/// The member expression selects the value of a field from a struct or union.
+/// Both structs and unions are encoded into a single large bit vector.
+/// The fields of a union are encoded into the lowest bits, with padding in the
+/// highest bits if needed.
+/// Structs are encoded as a single bitvector where the first field is stored
 /// in the highest bits. The second field is stored in the next highest set of
 /// bits and so on. As offsets are indexed from the lowest bit, any field can be
 /// selected by extracting the range of bits starting from an offset based on
 /// the combined width of the fields which follow the field being selected.
 exprt struct_encodingt::encode_member(const member_exprt &member_expr) const
 {
-  const auto &struct_type = type_checked_cast<struct_typet>(
-    ns.get().follow(member_expr.compound().type()));
-  const std::size_t offset_bits = count_trailing_bit_width(
-    struct_type, member_expr.get_component_name(), *boolbv_width);
+  const auto &type = ns.get().follow(member_expr.compound().type());
   const auto member_bits_width = (*boolbv_width)(member_expr.type());
+  const auto offset_bits = [&]() -> std::size_t {
+    if(can_cast_type<union_typet>(type))
+      return 0;
+    const auto &struct_type = type_checked_cast<struct_typet>(type);
+    return count_trailing_bit_width(
+      struct_type, member_expr.get_component_name(), *boolbv_width);
+  }();
   return extractbits_exprt{
     member_expr.compound(),
     offset_bits + member_bits_width - 1,

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -501,4 +501,26 @@ TEST_CASE("encoding of union expressions", "[core][smt2_incremental]")
     const auto bv_equal = equal_exprt{symbol_expr_as_bv, partial_union_as_bv};
     REQUIRE(test.struct_encoding.encode(union_equal) == bv_equal);
   }
+  SECTION("member expression selecting a data member of a union")
+  {
+    SECTION("Member which fits the size of the whole union")
+    {
+      const typet field_type = signedbv_typet{32};
+      const exprt zero = from_integer(0, field_type);
+      const exprt input =
+        equal_exprt{zero, member_exprt{symbol_expr, "ham", field_type}};
+      const exprt expected = equal_exprt{
+        zero, extractbits_exprt{symbol_expr_as_bv, 31, 0, field_type}};
+      REQUIRE(test.struct_encoding.encode(input) == expected);
+    }
+    SECTION("Member which is smaller than the union as a whole")
+    {
+      const typet field_type = unsignedbv_typet{8};
+      const exprt input =
+        equal_exprt{dozen, member_exprt{symbol_expr, "eggs", field_type}};
+      const exprt expected = equal_exprt{
+        dozen, extractbits_exprt{symbol_expr_as_bv, 7, 0, field_type}};
+      REQUIRE(test.struct_encoding.encode(input) == expected);
+    }
+  }
 }