Add struct decoding to encoding class

Author: thomasspriggs

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -7,6 +7,7 @@
 #include <util/make_unique.h>
 #include <util/namespace.h>
 #include <util/range.h>
+#include <util/simplify_expr.h>
 
 #include <solvers/flattening/boolbv_width.h>
 
@@ -177,3 +178,31 @@ exprt struct_encodingt::encode(exprt expr) const
   }
   return expr;
 }
+
+exprt struct_encodingt::decode(
+  const exprt &encoded,
+  const struct_tag_typet &original_type) const
+{
+  // The algorithm below works by extracting each of the separate fields from
+  // the combined encoded value using a `member_exprt` which is itself encoded
+  // into a `bit_extract_exprt`. These separated fields can then be combined
+  // using a `struct_exprt`. This is expected to duplicate the input encoded
+  // expression for each of the fields. However for the case where the input
+  // encoded expression is a `constant_exprt`, expression simplification will be
+  // able simplify away the duplicated portions of the constant and the bit
+  // extraction expressions. This yields a clean struct expression where each
+  // field is a separate constant containing the data solely relevant to that
+  // field.
+  INVARIANT(
+    can_cast_type<bv_typet>(encoded.type()),
+    "Structs are expected to be encoded into bit vectors.");
+  const struct_typet definition = ns.get().follow_tag(original_type);
+  exprt::operandst encoded_fields;
+  for(const auto &component : definition.components())
+  {
+    encoded_fields.push_back(typecast_exprt::conditional_cast(
+      encode(member_exprt{typecast_exprt{encoded, original_type}, component}),
+      component.type()));
+  }
+  return simplify_expr(struct_exprt{encoded_fields, original_type}, ns);
+}

src/solvers/smt2_incremental/encoding/struct_encoding.h

@@ -11,6 +11,7 @@
 class namespacet;
 class boolbv_widtht;
 class member_exprt;
+class struct_tag_typet;
 
 /// Encodes struct types/values into non-struct expressions/types.
 class struct_encodingt final
@@ -22,6 +23,10 @@ class struct_encodingt final
 
   typet encode(typet type) const;
   exprt encode(exprt expr) const;
+  /// Reconstructs a struct expression of the \p original_type using the data
+  /// from the bit vector \p encoded expression.
+  exprt
+  decode(const exprt &encoded, const struct_tag_typet &original_type) const;
 
 private:
   std::unique_ptr<boolbv_widtht> boolbv_width;

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -321,6 +321,26 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
   }
 }
 
+TEST_CASE("decoding into struct expressions.", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst component_types{
+    {"green", signedbv_typet{32}},
+    {"eggs", unsignedbv_typet{16}},
+    {"ham", signedbv_typet{24}}};
+  const struct_typet struct_type{component_types};
+  const type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  const struct_tag_typet struct_tag{type_symbol.name};
+  const struct_exprt expected{
+    {from_integer(3, signedbv_typet{32}),
+     from_integer(2, unsignedbv_typet{16}),
+     from_integer(1, signedbv_typet{24})},
+    struct_tag};
+  const exprt encoded = constant_exprt{"000000030002000001", bv_typet{72}};
+  REQUIRE(test.struct_encoding.decode(encoded, struct_tag) == expected);
+}
+
 TEST_CASE(
   "encoding of single member struct expressions",
   "[core][smt2_incremental]")