Merge pull request #7926 from thomasspriggs/tas/smt_union_exprt

Add `union_exprt` encoding support in incremental smt2 decision procedure

Author: thomasspriggs

src/solvers/Makefile

@@ -211,6 +211,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
       smt2_incremental/encoding/struct_encoding.cpp \
       smt2_incremental/encoding/enum_encoding.cpp \
+      smt2_incremental/encoding/nondet_padding.cpp \
       smt2_incremental/theories/smt_array_theory.cpp \
       smt2_incremental/theories/smt_bit_vector_theory.cpp \
       smt2_incremental/theories/smt_core_theory.cpp \

src/solvers/smt2_incremental/encoding/module_dependencies.txt

@@ -1 +1,2 @@
-util
+solvers/smt2_incremental/encoding
+util

src/solvers/smt2_incremental/encoding/nondet_padding.cpp

@@ -0,0 +1,5 @@
+// Author: Diffblue Ltd.
+
+#include "nondet_padding.h"
+
+const irep_idt nondet_padding_exprt::ID_nondet_padding = "nondet_padding";

src/solvers/smt2_incremental/encoding/nondet_padding.h

@@ -0,0 +1,45 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Expressions for use in incremental SMT2 decision procedure
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H
+
+#include <util/bitvector_types.h>
+#include <util/expr.h>
+#include <util/invariant.h>
+
+class nondet_padding_exprt;
+void validate_expr(const nondet_padding_exprt &padding);
+
+/// This expression serves as a placeholder for the bits which have non
+/// deterministic value in a larger bit vector. It is inserted in contexts where
+/// a subset of the bits are assigned to an expression and the remainder are
+/// left unspecified.
+class nondet_padding_exprt : public expr_protectedt
+{
+public:
+  static const irep_idt ID_nondet_padding;
+
+  explicit nondet_padding_exprt(typet type)
+    : expr_protectedt{ID_nondet_padding, std::move(type)}
+  {
+    validate_expr(*this);
+  }
+};
+
+template <>
+inline bool can_cast_expr<nondet_padding_exprt>(const exprt &base)
+{
+  return base.id() == nondet_padding_exprt::ID_nondet_padding;
+}
+
+inline void validate_expr(const nondet_padding_exprt &padding)
+{
+  INVARIANT(
+    can_cast_type<bv_typet>(padding.type()),
+    "Nondet padding is expected to pad a bit vector type.");
+}
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -12,6 +12,7 @@
 #include <util/simplify_expr.h>
 
 #include <solvers/flattening/boolbv_width.h>
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
 
 #include <algorithm>
 #include <numeric>
@@ -136,6 +137,22 @@ static exprt encode(const struct_exprt &struct_expr)
   return concatenation_exprt{struct_expr.operands(), struct_expr.type()};
 }
 
+static exprt
+encode(const union_exprt &union_expr, const boolbv_widtht &bit_width)
+{
+  const std::size_t union_width = bit_width(union_expr.type());
+  const exprt &component = union_expr.op();
+  const std::size_t component_width = bit_width(union_expr.op().type());
+  if(union_width == component_width)
+    return typecast_exprt(component, bv_typet{union_width});
+  INVARIANT(
+    union_width >= component_width,
+    "Union must be at least as wide as its component.");
+  return concatenation_exprt{
+    {nondet_padding_exprt{bv_typet{union_width - component_width}}, component},
+    bv_typet{union_width}};
+}
+
 static std::size_t count_trailing_bit_width(
   const struct_typet &type,
   const irep_idt name,
@@ -195,6 +212,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 union_expr = expr_try_dynamic_cast<union_exprt>(current))
+      current = ::encode(*union_expr, *boolbv_width);
     if(const auto member_expr = expr_try_dynamic_cast<member_exprt>(current))
       current = encode_member(*member_expr);
     for(auto &operand : current.operands())

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -18,6 +18,7 @@
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/encoding/enum_encoding.h>
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
@@ -364,12 +365,28 @@ void smt2_incremental_decision_proceduret::define_index_identifiers(
   });
 }
 
+exprt smt2_incremental_decision_proceduret::substitute_defined_padding(
+  exprt root_expr)
+{
+  root_expr.visit_pre([&](exprt &node) {
+    if(const auto pad = expr_try_dynamic_cast<nondet_padding_exprt>(node))
+    {
+      const auto instance = "padding_" + std::to_string(padding_sequence());
+      const auto term =
+        smt_identifier_termt{instance, convert_type_to_smt_sort(pad->type())};
+      solver_process->send(smt_declare_function_commandt{term, {}});
+      node = symbol_exprt{instance, node.type()};
+    }
+  });
+  return root_expr;
+}
+
 smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
   define_index_identifiers(expr);
-  const exprt substituted =
-    substitute_identifiers(expr, expression_identifiers);
+  const exprt substituted = substitute_defined_padding(
+    substitute_identifiers(expr, expression_identifiers));
   track_expression_objects(substituted, ns, object_map);
   associate_pointer_sizes(
     substituted,

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -102,6 +102,11 @@ class smt2_incremental_decision_proceduret final
   /// \note This function is non-const because it mutates the object_map.
   smt_termt convert_expr_to_smt(const exprt &expr);
   void define_index_identifiers(const exprt &expr);
+  /// In the case where lowering passes insert instances of the anonymous
+  /// `nondet_padding_exprt`, these need functions declaring for each instance.
+  /// These instances are then substituted for the function identifier in order
+  /// to free the solver to choose a non-det value.
+  exprt substitute_defined_padding(exprt expr);
   /// Sends the solver the definitions of the object sizes and dynamic memory
   /// statuses.
   void define_object_properties();
@@ -135,7 +140,7 @@ class smt2_incremental_decision_proceduret final
     {
       return next_id++;
     }
-  } handle_sequence, array_sequence, index_sequence;
+  } handle_sequence, array_sequence, index_sequence, padding_sequence;
   /// When the `handle(exprt)` member function is called, the decision procedure
   /// commands the SMT solver to define a new function corresponding to the
   /// given expression. The mapping of the expressions to the function

unit/Makefile

@@ -117,6 +117,7 @@ SRC += analyses/ai/ai.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/encoding/nondet_padding.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/encoding/nondet_padding.cpp

@@ -0,0 +1,43 @@
+// Author: Diffblue Ltd.
+
+#include <util/expr_cast.h>
+#include <util/std_expr.h>
+
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
+#include <testing-utils/invariant.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Nondet padding expression", "[core][smt2_incremental]")
+{
+  const bv_typet type{8};
+  const exprt padding = nondet_padding_exprt{type};
+  SECTION("Valid usage")
+  {
+    REQUIRE(padding.type() == type);
+    REQUIRE(nullptr != expr_try_dynamic_cast<nondet_padding_exprt>(padding));
+  }
+  const auto type_error = invariant_failure_containing(
+    "Nondet padding is expected to pad a bit vector type.");
+  SECTION("Failed downcasts")
+  {
+    const exprt not_padding = symbol_exprt{"foo", empty_typet{}};
+    REQUIRE(
+      nullptr == expr_try_dynamic_cast<nondet_padding_exprt>(not_padding));
+    const exprt wrong_type = [&]() {
+      exprt padding = nondet_padding_exprt{type};
+      padding.type() = empty_typet{};
+      return padding;
+    }();
+    cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS_MATCHES(
+      expr_checked_cast<nondet_padding_exprt>(wrong_type),
+      invariant_failedt,
+      type_error);
+  }
+  SECTION("Construction with incorrect type")
+  {
+    cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS_MATCHES(
+      nondet_padding_exprt{empty_typet{}}, invariant_failedt, type_error);
+  }
+}

unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -8,6 +8,7 @@
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
 #include <solvers/smt2_incremental/encoding/struct_encoding.h>
 #include <testing-utils/use_catch.h>
 
@@ -453,3 +454,39 @@ TEST_CASE(
     REQUIRE(test.struct_encoding.encode(struct_expr) == dozen);
   }
 }
+
+TEST_CASE("encoding of union expressions", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"eggs", unsignedbv_typet{8}}, {"ham", signedbv_typet{32}}};
+  const type_symbolt type_symbol{"foot", union_typet{components}, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  const union_tag_typet union_tag{type_symbol.name};
+  const symbolt union_value_symbol{"foo", union_tag, ID_C};
+  test.symbol_table.insert(union_value_symbol);
+  const auto symbol_expr = union_value_symbol.symbol_expr();
+  const auto symbol_expr_as_bv = symbol_exprt{"foo", bv_typet{32}};
+  const auto dozen = from_integer(12, unsignedbv_typet{8});
+  const auto partial_union = union_exprt{"eggs", dozen, union_tag};
+  const auto partial_union_as_bv = concatenation_exprt{
+    {nondet_padding_exprt{bv_typet{24}}, dozen}, bv_typet{32}};
+  SECTION("Union typed symbol expression")
+  {
+    REQUIRE(test.struct_encoding.encode(symbol_expr) == symbol_expr_as_bv);
+  }
+  SECTION("Expression for a union from a component")
+  {
+    REQUIRE(test.struct_encoding.encode(partial_union) == partial_union_as_bv);
+    const auto one = from_integer(1, unsignedbv_typet{32});
+    const auto full_union = union_exprt{"ham", one, union_tag};
+    const auto full_union_as_bv = typecast_exprt{one, bv_typet{32}};
+    REQUIRE(test.struct_encoding.encode(full_union) == full_union_as_bv);
+  }
+  SECTION("Union equality expression")
+  {
+    const auto union_equal = equal_exprt{symbol_expr, partial_union};
+    const auto bv_equal = equal_exprt{symbol_expr_as_bv, partial_union_as_bv};
+    REQUIRE(test.struct_encoding.encode(union_equal) == bv_equal);
+  }
+}

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -1,6 +1,7 @@
 // Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
@@ -13,6 +14,7 @@
 #include <solvers/smt2_incremental/ast/smt_responses.h>
 #include <solvers/smt2_incremental/ast/smt_sorts.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
@@ -268,6 +270,28 @@ TEST_CASE(
               smt_identifier_termt{"third_comparison", smt_bool_sortt{}})},
           smt_assert_commandt{comparison_conjunction_term}});
     }
+    SECTION("Set with nondet_padding")
+    {
+      const exprt to_set = equal_exprt{
+        concatenation_exprt{
+          {nondet_padding_exprt{bv_typet{8}}, from_integer(42, bv_typet{8})},
+          bv_typet{16}},
+        from_integer(42, bv_typet{16})};
+      test.sent_commands.clear();
+      test.procedure.set_to(to_set, true);
+      // (declare-fun padding_0 () (_ BitVec 8))
+      // (assert (= (concat padding_0 (_ bv42 8)) (_ bv42 16)))
+      const auto expected_padding_term =
+        smt_identifier_termt{"padding_0", smt_bit_vector_sortt{8}};
+      REQUIRE(
+        test.sent_commands ==
+        std::vector<smt_commandt>{
+          smt_declare_function_commandt{expected_padding_term, {}},
+          smt_assert_commandt{smt_core_theoryt::equal(
+            smt_bit_vector_theoryt::concat(
+              expected_padding_term, smt_bit_vector_constant_termt{42, 8}),
+            smt_bit_vector_constant_termt{42, 16})}});
+    }
     SECTION("Handle of value-less symbol.")
     {
       const symbolt foo = make_test_symbol("foo", bool_typet{});
@@ -820,6 +844,43 @@ TEST_CASE(
   REQUIRE(test.sent_commands == expected_commands);
 }
 
+TEST_CASE(
+  "smt2_incremental_decision_proceduret union support.",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  // union foot{ int8_t eggs, uint32_t ham } foo;
+  const struct_union_typet::componentst components{
+    {"eggs", unsignedbv_typet{8}}, {"ham", signedbv_typet{32}}};
+  const type_symbolt type_symbol{"foot", union_typet{components}, ID_C};
+  test.symbol_table.insert(type_symbol);
+  const union_tag_typet union_tag{type_symbol.name};
+  const symbolt union_value_symbol{"foo", union_tag, ID_C};
+  test.symbol_table.insert(union_value_symbol);
+  // assume(foo == foot{ .eggs = 12 });
+  const auto symbol_expr = union_value_symbol.symbol_expr();
+  const auto dozen = from_integer(12, unsignedbv_typet{8});
+  const auto union_needing_padding = union_exprt{"eggs", dozen, union_tag};
+  const auto equals = equal_exprt{symbol_expr, union_needing_padding};
+  test.sent_commands.clear();
+  test.procedure.set_to(equals, true);
+
+  // (declare-fun foo () (_ BitVec 32))
+  // (declare-fun padding_0 () (_ BitVec 24))
+  // (assert (= foo (concat padding_0 (_ bv12 8)))) }
+  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{
+    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);
+}
+
 TEST_CASE(
   "smt2_incremental_decision_proceduret byte update-extract commands.",
   "[core][smt2_incremental]")