Add encoding of member expressions in new SMT decision procedure

Author: thomasspriggs

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -5,18 +5,23 @@
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/make_unique.h>
+#include <util/namespace.h>
+#include <util/range.h>
 
 #include <solvers/flattening/boolbv_width.h>
 
+#include <algorithm>
+#include <numeric>
 #include <queue>
 
 struct_encodingt::struct_encodingt(const namespacet &ns)
-  : boolbv_width{util_make_unique<boolbv_widtht>(ns)}
+  : boolbv_width{util_make_unique<boolbv_widtht>(ns)}, ns{ns}
 {
 }
 
 struct_encodingt::struct_encodingt(const struct_encodingt &other)
-  : boolbv_width{util_make_unique<boolbv_widtht>(*other.boolbv_width)}
+  : boolbv_width{util_make_unique<boolbv_widtht>(*other.boolbv_width)},
+    ns{other.ns}
 {
 }
 
@@ -55,6 +60,49 @@ static exprt encode(const struct_exprt &struct_expr)
   return concatenation_exprt{struct_expr.operands(), struct_expr.type()};
 }
 
+static std::size_t count_trailing_bit_width(
+  const struct_typet &type,
+  const irep_idt name,
+  const boolbv_widtht &boolbv_width)
+{
+  auto member_component_rit = std::find_if(
+    type.components().rbegin(),
+    type.components().rend(),
+    [&](const struct_union_typet::componentt &component) {
+      return component.get_name() == name;
+    });
+  INVARIANT(
+    member_component_rit != type.components().rend(),
+    "Definition of struct type should include named component.");
+  const auto trailing_widths =
+    make_range(type.components().rbegin(), member_component_rit)
+      .map([&](const struct_union_typet::componentt &component) -> std::size_t {
+        return boolbv_width(component.type());
+      });
+  return std::accumulate(
+    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
+/// 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 member_bits_width = (*boolbv_width)(member_expr.type());
+  return extractbits_exprt{
+    member_expr.compound(),
+    offset_bits + member_bits_width - 1,
+    offset_bits,
+    member_expr.type()};
+}
+
 exprt struct_encodingt::encode(exprt expr) const
 {
   std::queue<exprt *> work_queue;
@@ -66,6 +114,8 @@ exprt struct_encodingt::encode(exprt expr) const
     current.type() = encode(current.type());
     if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
       current = ::encode(*struct_expr);
+    if(const auto member_expr = expr_try_dynamic_cast<member_exprt>(current))
+      current = encode_member(*member_expr);
     for(auto &operand : current.operands())
       work_queue.push(&operand);
   }

src/solvers/smt2_incremental/encoding/struct_encoding.h

@@ -10,6 +10,7 @@
 
 class namespacet;
 class boolbv_widtht;
+class member_exprt;
 
 /// Encodes struct types/values into non-struct expressions/types.
 class struct_encodingt final
@@ -24,6 +25,9 @@ class struct_encodingt final
 
 private:
   std::unique_ptr<boolbv_widtht> boolbv_width;
+  std::reference_wrapper<const namespacet> ns;
+
+  exprt encode_member(const member_exprt &member_expr) const;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -3,6 +3,7 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/mathematical_types.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
@@ -108,6 +109,47 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
       {green_ham.symbol_expr(), forty_two, minus_one}, bv_typet{72}};
     REQUIRE(test.struct_encoding.encode(struct_expr) == expected_result);
   }
+  SECTION("member expression selecting a data member of a struct")
+  {
+    const symbolt breakfast{"breakfast", struct_tag, ID_C};
+    test.symbol_table.insert(breakfast);
+    SECTION("First member")
+    {
+      const typet field_type = signedbv_typet{32};
+      const exprt zero = from_integer(0, field_type);
+      const exprt input = equal_exprt{
+        zero, member_exprt{breakfast.symbol_expr(), "green", field_type}};
+      const exprt expected = equal_exprt{
+        zero,
+        extractbits_exprt{
+          symbol_exprt{"breakfast", bv_typet{72}}, 71, 40, field_type}};
+      REQUIRE(test.struct_encoding.encode(input) == expected);
+    }
+    SECTION("Second member")
+    {
+      const typet field_type = unsignedbv_typet{16};
+      const exprt dozen = from_integer(12, field_type);
+      const exprt input = equal_exprt{
+        dozen, member_exprt{breakfast.symbol_expr(), "eggs", field_type}};
+      const exprt expected = equal_exprt{
+        dozen,
+        extractbits_exprt{
+          symbol_exprt{"breakfast", bv_typet{72}}, 39, 24, field_type}};
+      REQUIRE(test.struct_encoding.encode(input) == expected);
+    }
+    SECTION("Third member")
+    {
+      const typet field_type = signedbv_typet{24};
+      const exprt two = from_integer(2, field_type);
+      const exprt input = equal_exprt{
+        two, member_exprt{breakfast.symbol_expr(), "ham", field_type}};
+      const exprt expected = equal_exprt{
+        two,
+        extractbits_exprt{
+          symbol_exprt{"breakfast", bv_typet{72}}, 23, 0, field_type}};
+      REQUIRE(test.struct_encoding.encode(input) == expected);
+    }
+  }
 }
 
 TEST_CASE(