Merge pull request #7740 from thomasspriggs/tas/smt2_structs

Add initial struct support for incremental SMT2 decision procedure

Author: thomasspriggs

regression/cbmc-incr-smt2/structs/simple.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdint.h>
+
+struct my_struct_type
+{
+  int16_t a;
+  int16_t b;
+};
+
+int main()
+{
+  int16_t nondet;
+  struct my_struct_type my_struct;
+  if(nondet == 3)
+    my_struct.a = 10;
+  else
+    my_struct.a = 12;
+  struct my_struct_type struct_copy;
+  struct_copy = my_struct;
+  assert(my_struct.b != 30 || struct_copy.a != 10);
+}

regression/cbmc-incr-smt2/structs/simple.desc

@@ -0,0 +1,17 @@
+CORE
+simple.c
+--trace
+Passing problem to incremental SMT2 solving
+line 20 assertion my_struct.b != 30 || struct_copy.a != 10: FAILURE
+nondet=3
+struct_copy.a=10
+struct_copy.b=30
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support struct values and traces for a trivial example. At the
+time of adding the regression test, this exercised the conversion code specific
+to struct_tag_typet and struct_exprt. Field sensitivity is expected to eliminate
+many of the struct specific expressions before they can reach the decision
+procedure with this simple example.

src/solvers/Makefile

@@ -210,6 +210,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
+      smt2_incremental/struct_encoding.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/smt2_incremental_decision_procedure.cpp

@@ -249,7 +249,8 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
     number_of_solver_calls{0},
     solver_process(std::move(_solver_process)),
     log{message_handler},
-    object_map{initial_smt_object_map()}
+    object_map{initial_smt_object_map()},
+    struct_encoding{_ns}
 {
   solver_process->send(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
@@ -268,7 +269,7 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
     return;
   }
 
-  const exprt lowered_expr = lower_byte_operators(in_expr, ns);
+  const exprt lowered_expr = lower(in_expr);
 
   define_dependent_functions(lowered_expr);
   smt_define_function_commandt function{
@@ -514,12 +515,12 @@ void smt2_incremental_decision_proceduret::set_to(
   const exprt &in_expr,
   bool value)
 {
-  const exprt lowered_expr = lower_byte_operators(in_expr, ns);
-  PRECONDITION(can_cast_type<bool_typet>(lowered_expr.type()));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n  "
-          << lowered_expr.pretty(2, 0) << messaget::eom;
+          << in_expr.pretty(2, 0) << messaget::eom;
   });
+  const exprt lowered_expr = lower(in_expr);
+  PRECONDITION(can_cast_type<bool_typet>(lowered_expr.type()));
 
   define_dependent_functions(lowered_expr);
   auto converted_term = [&]() -> smt_termt {
@@ -587,6 +588,17 @@ void smt2_incremental_decision_proceduret::define_object_properties()
   }
 }
 
+exprt smt2_incremental_decision_proceduret::lower(exprt expression)
+{
+  const exprt lowered =
+    struct_encoding.encode(lower_byte_operators(expression, ns));
+  log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
+    if(lowered != expression)
+      debug << "lowered to -\n  " << lowered.pretty(2, 0) << messaget::eom;
+  });
+  return lowered;
+}
+
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -13,6 +13,7 @@
 #include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
+#include <solvers/smt2_incremental/struct_encoding.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>
 
@@ -93,6 +94,10 @@ class smt2_incremental_decision_proceduret final
   /// Sends the solver the definitions of the object sizes and dynamic memory
   /// statuses.
   void define_object_properties();
+  /// Performs a combination of transformations which reduces the set of
+  /// possible expression forms by expressing these in terms of the remaining
+  /// language features.
+  exprt lower(exprt expression);
 
   /// Namespace for looking up the expressions which symbol_exprts relate to.
   /// This includes the symbols defined outside of the decision procedure but
@@ -165,6 +170,7 @@ class smt2_incremental_decision_proceduret final
   smt_is_dynamic_objectt is_dynamic_object_function;
   /// Precalculated type sizes used for pointer arithmetic.
   type_size_mapt pointer_sizes_map;
+  struct_encodingt struct_encoding;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H

src/solvers/smt2_incremental/struct_encoding.cpp

@@ -0,0 +1,65 @@
+// Author: Diffblue Ltd.
+
+#include "struct_encoding.h"
+
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/make_unique.h>
+
+#include <solvers/flattening/boolbv_width.h>
+
+#include <queue>
+
+struct_encodingt::struct_encodingt(const namespacet &ns)
+  : boolbv_width{util_make_unique<boolbv_widtht>(ns)}
+{
+}
+
+struct_encodingt::struct_encodingt(const struct_encodingt &other)
+  : boolbv_width{util_make_unique<boolbv_widtht>(*other.boolbv_width)}
+{
+}
+
+struct_encodingt::~struct_encodingt() = default;
+
+typet struct_encodingt::encode(typet type) const
+{
+  std::queue<typet *> work_queue;
+  work_queue.push(&type);
+  while(!work_queue.empty())
+  {
+    typet &current = *work_queue.front();
+    work_queue.pop();
+    if(const auto struct_tag = type_try_dynamic_cast<struct_tag_typet>(current))
+    {
+      current = bv_typet{(*boolbv_width)(*struct_tag)};
+    }
+    if(const auto array = type_try_dynamic_cast<array_typet>(current))
+    {
+      work_queue.push(&array->element_type());
+    }
+  }
+  return type;
+}
+
+static exprt encode(const struct_exprt &struct_expr)
+{
+  return concatenation_exprt{struct_expr.operands(), struct_expr.type()};
+}
+
+exprt struct_encodingt::encode(exprt expr) const
+{
+  std::queue<exprt *> work_queue;
+  work_queue.push(&expr);
+  while(!work_queue.empty())
+  {
+    exprt &current = *work_queue.front();
+    work_queue.pop();
+    current.type() = encode(current.type());
+    if(const auto struct_expr = expr_try_dynamic_cast<struct_exprt>(current))
+      current = ::encode(*struct_expr);
+    for(auto &operand : current.operands())
+      work_queue.push(&operand);
+  }
+  return expr;
+}

src/solvers/smt2_incremental/struct_encoding.h

@@ -0,0 +1,29 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H
+
+#include <util/expr.h> // For passing exprt by value. // IWYU pragma: keep
+#include <util/type.h> // For passing `typet` by value. // IWYU pragma: keep
+
+#include <memory>
+
+class namespacet;
+class boolbv_widtht;
+
+/// Encodes struct types/values into non-struct expressions/types.
+class struct_encodingt final
+{
+public:
+  explicit struct_encodingt(const namespacet &ns);
+  struct_encodingt(const struct_encodingt &other);
+  ~struct_encodingt();
+
+  typet encode(typet type) const;
+  exprt encode(exprt expr) const;
+
+private:
+  std::unique_ptr<boolbv_widtht> boolbv_width;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_STRUCT_ENCODING_H

unit/Makefile

@@ -114,6 +114,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_object_size.cpp \
        solvers/smt2_incremental/smt_response_validation.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \
+       solvers/smt2_incremental/struct_encoding.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/struct_encoding.cpp

@@ -0,0 +1,107 @@
+// Author: Diffblue Ltd.
+
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+#include <solvers/smt2_incremental/struct_encoding.h>
+#include <testing-utils/use_catch.h>
+
+struct struct_encoding_test_environmentt
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  struct_encodingt struct_encoding{ns};
+
+  static struct_encoding_test_environmentt make()
+  {
+    return {};
+  }
+
+private:
+  struct_encoding_test_environmentt() = default;
+};
+
+TEST_CASE(
+  "struct encoding of non-stuct type is a no-op",
+  "[core][smt2_incremental]")
+{
+  auto test = struct_encoding_test_environmentt::make();
+  typet input = signedbv_typet{8};
+  REQUIRE(test.struct_encoding.encode(input) == input);
+}
+
+TEST_CASE("struct encoding of types", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst components{
+    {"foo", unsignedbv_typet{8}}, {"bar", signedbv_typet{16}}};
+  struct_typet struct_type{components};
+  type_symbolt type_symbol{"my_structt", struct_type, ID_C};
+  auto test = struct_encoding_test_environmentt::make();
+  test.symbol_table.insert(type_symbol);
+  struct_tag_typet struct_tag{type_symbol.name};
+  SECTION("direct struct_tag_type encoding")
+  {
+    REQUIRE(test.struct_encoding.encode(struct_tag) == bv_typet{24});
+  }
+  SECTION("array of structs encoding")
+  {
+    const auto index_type = signedbv_typet{32};
+    const auto array_size = from_integer(5, index_type);
+    array_typet array_of_struct{struct_tag, array_size};
+    array_typet expected_encoded_array{bv_typet{24}, array_size};
+    REQUIRE(
+      test.struct_encoding.encode(array_of_struct) == expected_encoded_array);
+  }
+  SECTION("array of array of structs encoding")
+  {
+    const auto index_type = signedbv_typet{32};
+    const auto array_size_inner = from_integer(4, index_type);
+    const auto array_size_outer = from_integer(2, index_type);
+    array_typet array_of_struct{struct_tag, array_size_inner};
+    array_typet array_of_array_of_struct{array_of_struct, array_size_outer};
+    array_typet expected_encoded_array{
+      array_typet{bv_typet{24}, array_size_inner}, array_size_outer};
+    REQUIRE(
+      test.struct_encoding.encode(array_of_array_of_struct) ==
+      expected_encoded_array);
+  }
+}
+
+TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
+{
+  const struct_union_typet::componentst component_types{
+    {"green", signedbv_typet{32}}, {"eggs", unsignedbv_typet{16}}};
+  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 symbolt struct_value_symbol{"my_struct", struct_tag, ID_C};
+  test.symbol_table.insert(struct_value_symbol);
+  const auto symbol_expr = struct_value_symbol.symbol_expr();
+  const auto symbol_expr_as_bv = symbol_exprt{"my_struct", bv_typet{48}};
+  SECTION("struct typed symbol expression")
+  {
+    REQUIRE(test.struct_encoding.encode(symbol_expr) == symbol_expr_as_bv);
+  }
+  SECTION("struct equality expression")
+  {
+    const auto struct_equal = equal_exprt{symbol_expr, symbol_expr};
+    const auto bv_equal = equal_exprt{symbol_expr_as_bv, symbol_expr_as_bv};
+    REQUIRE(test.struct_encoding.encode(struct_equal) == bv_equal);
+  }
+  SECTION("expression for a struct from list of components")
+  {
+    const symbolt green_ham{"ham", signedbv_typet{32}, ID_C};
+    test.symbol_table.insert(green_ham);
+    const auto forty_two = from_integer(42, unsignedbv_typet{16});
+    const exprt::operandst components{green_ham.symbol_expr(), forty_two};
+    const struct_exprt struct_expr{components, struct_tag};
+    const concatenation_exprt expected_result{
+      {green_ham.symbol_expr(), forty_two}, bv_typet{48}};
+    REQUIRE(test.struct_encoding.encode(struct_expr) == expected_result);
+  }
+}