Merge pull request #6519 from thomasspriggs/tas/smt_to_expr

Add construction of value `exprt`s from smt terms.

Author: thomasspriggs

src/solvers/Makefile

@@ -193,6 +193,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_parser.cpp \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
+      smt2_incremental/construct_value_expr_from_smt.cpp \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -0,0 +1,85 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
+
+#include <solvers/smt2_incremental/smt_terms.h>
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/type.h>
+
+class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
+{
+private:
+  const typet &type_to_construct;
+  optionalt<exprt> result;
+
+  explicit value_expr_from_smt_factoryt(const typet &type_to_construct)
+    : type_to_construct{type_to_construct}, result{}
+  {
+  }
+
+  void visit(const smt_bool_literal_termt &bool_literal) override
+  {
+    INVARIANT(
+      type_to_construct == bool_typet{},
+      "Bool terms may only be used to construct bool typed expressions.");
+    result = bool_literal.value() ? (exprt)true_exprt{} : false_exprt{};
+  }
+
+  void visit(const smt_identifier_termt &identifier_term) override
+  {
+    INVARIANT(
+      false, "Unexpected conversion of identifier to value expression.");
+  }
+
+  void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
+  {
+    if(
+      const auto integer_type =
+        type_try_dynamic_cast<integer_bitvector_typet>(type_to_construct))
+    {
+      INVARIANT(
+        integer_type->get_width() == bit_vector_constant.get_sort().bit_width(),
+        "Width of smt bit vector term must match the width of bit vector "
+        "type.");
+      result = from_integer(bit_vector_constant.value(), type_to_construct);
+      return;
+    }
+
+    INVARIANT(
+      false,
+      "construct_value_expr_from_smt for bit vector should not be applied to "
+      "unsupported type " +
+        type_to_construct.pretty());
+  }
+
+  void
+  visit(const smt_function_application_termt &function_application) override
+  {
+    INVARIANT(
+      false,
+      "Unexpected conversion of function application to value expression.");
+  }
+
+public:
+  /// \brief This function is complete the external interface to this class. All
+  ///   construction of this class and construction of expressions should be
+  ///   carried out via this function.
+  static exprt make(const smt_termt &value_term, const typet &type_to_construct)
+  {
+    value_expr_from_smt_factoryt factory{type_to_construct};
+    value_term.accept(factory);
+    INVARIANT(factory.result.has_value(), "Factory must result in expr value.");
+    return *factory.result;
+  }
+};
+
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct)
+{
+  return value_expr_from_smt_factoryt::make(value_term, type_to_construct);
+}

src/solvers/smt2_incremental/construct_value_expr_from_smt.h

@@ -0,0 +1,31 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
+
+#include <util/expr.h>
+
+class smt_termt;
+class typet;
+
+/// \brief Given a \p value_term and a \p type_to_construct, this function
+/// constructs a value exprt with a value based on \p value_term and a type of
+/// \p type_to_construct.
+/// \param value_term
+///   This must be a "simple" term encoding a value. It must not be a term
+///   requiring any kind of further evaluation to get a value, such as would be
+///   the case for identifiers or function applications.
+/// \param type_to_construct
+///   The type which the constructed expr returned is expected to have. This
+///   type must be compatible with the sort of \p value_term.
+/// \note The type is required separately in order to carry out this conversion,
+/// because the smt value term does not contain all the required information.
+/// For example an 8 bit, bit vector with a value of 255 could be used to
+/// construct an `unsigned char` with the value 255 or alternatively a
+/// `signed char` with the value -1. So these alternatives are disambiguated
+/// using the type.
+exprt construct_value_expr_from_smt(
+  const smt_termt &value_term,
+  const typet &type_to_construct);
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H

unit/Makefile

@@ -100,6 +100,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/smt2/smt2_conv.cpp \
        solvers/smt2/smt2irep.cpp \
+       solvers/smt2_incremental/construct_value_expr_from_smt.cpp \
        solvers/smt2_incremental/convert_expr_to_smt.cpp \
        solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \

unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -0,0 +1,124 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
+
+#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
+
+#include <testing-utils/invariant.h>
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/mp_arith.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+#include <string>
+
+static mp_integer power2(unsigned exponent)
+{
+  mp_integer result;
+  result.setPower2(exponent);
+  return result;
+}
+
+/// Returns the maximum integer value which can be stored in \p bits as an
+/// unsigned integer.
+static mp_integer max_int(const std::size_t bits)
+{
+  return power2(bits) - 1;
+}
+
+TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
+{
+  optionalt<smt_termt> input_term;
+  optionalt<exprt> expected_result;
+
+  using rowt = std::pair<smt_termt, exprt>;
+
+  // clang-format off
+#define UNSIGNED_BIT_VECTOR_TESTS(bits)                                        \
+  rowt{smt_bit_vector_constant_termt{0, (bits)},                               \
+       from_integer(0, unsignedbv_typet{(bits)})},                             \
+  rowt{smt_bit_vector_constant_termt{42, (bits)},                              \
+       from_integer(42, unsignedbv_typet{(bits)})},                            \
+  rowt{smt_bit_vector_constant_termt{max_int((bits) - 1), (bits)},             \
+       from_integer(max_int((bits) - 1), unsignedbv_typet{(bits)})},           \
+  rowt{smt_bit_vector_constant_termt{power2((bits) - 1), (bits)},              \
+       from_integer(power2((bits) - 1), unsignedbv_typet{(bits)})},            \
+  rowt{smt_bit_vector_constant_termt{max_int((bits)), (bits)},                 \
+       from_integer(max_int((bits)), unsignedbv_typet{(bits)})}
+
+#define SIGNED_BIT_VECTOR_TESTS(bits)                                          \
+  rowt{smt_bit_vector_constant_termt{0, (bits)},                               \
+       from_integer(0, signedbv_typet{(bits)})},                               \
+  rowt{smt_bit_vector_constant_termt{42, (bits)},                              \
+       from_integer(42, signedbv_typet{(bits)})},                              \
+  rowt{smt_bit_vector_constant_termt{max_int((bits) - 1), (bits)},             \
+       from_integer(max_int((bits) - 1), signedbv_typet{(bits)})},             \
+  rowt{smt_bit_vector_constant_termt{power2((bits) - 1), (bits)},              \
+       from_integer(-power2((bits) - 1), signedbv_typet{(bits)})},             \
+  rowt{smt_bit_vector_constant_termt{max_int((bits)), (bits)},                 \
+       from_integer(-1, signedbv_typet{(bits)})}
+  // clang-format on
+
+  std::tie(input_term, expected_result) = GENERATE(
+    rowt{smt_bool_literal_termt{true}, true_exprt{}},
+    rowt{smt_bool_literal_termt{false}, false_exprt{}},
+    UNSIGNED_BIT_VECTOR_TESTS(8),
+    SIGNED_BIT_VECTOR_TESTS(8),
+    UNSIGNED_BIT_VECTOR_TESTS(16),
+    SIGNED_BIT_VECTOR_TESTS(16),
+    UNSIGNED_BIT_VECTOR_TESTS(32),
+    SIGNED_BIT_VECTOR_TESTS(32),
+    UNSIGNED_BIT_VECTOR_TESTS(64),
+    SIGNED_BIT_VECTOR_TESTS(64));
+  SECTION(
+    "Construction of \"" + id2string(expected_result->type().id()) +
+    "\" from \"" + smt_to_smt2_string(*input_term) + "\"")
+  {
+    REQUIRE(
+      construct_value_expr_from_smt(*input_term, expected_result->type()) ==
+      *expected_result);
+  }
+}
+
+TEST_CASE(
+  "Invariant violations in value expr construction from smt.",
+  "[core][smt2_incremental]")
+{
+  optionalt<smt_termt> input_term;
+  optionalt<typet> input_type;
+  std::string invariant_reason;
+
+  using rowt = std::tuple<smt_termt, typet, std::string>;
+  std::tie(input_term, input_type, invariant_reason) = GENERATE(
+    rowt{smt_bool_literal_termt{true},
+         unsignedbv_typet{16},
+         "Bool terms may only be used to construct bool typed expressions."},
+    rowt{smt_identifier_termt{"foo", smt_bit_vector_sortt{16}},
+         unsignedbv_typet{16},
+         "Unexpected conversion of identifier to value expression."},
+    rowt{
+      smt_bit_vector_constant_termt{0, 8},
+      unsignedbv_typet{16},
+      "Width of smt bit vector term must match the width of bit vector type."},
+    rowt{smt_bit_vector_constant_termt{0, 8},
+         empty_typet{},
+         "construct_value_expr_from_smt for bit vector should not be applied "
+         "to unsupported type empty"},
+    rowt{smt_core_theoryt::make_not(smt_bool_literal_termt{true}),
+         unsignedbv_typet{16},
+         "Unexpected conversion of function application to value expression."});
+  SECTION(invariant_reason)
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS_MATCHES(
+      construct_value_expr_from_smt(*input_term, *input_type),
+      invariant_failedt,
+      invariant_failure_containing(invariant_reason));
+  }
+}