Merge pull request #6689 from thomasspriggs/tas/smt_casting

Add conversion of cast expressions to SMT terms for incremental SMT solving

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1,13 +1,9 @@
 // Author: Diffblue Ltd.
 
-#include <solvers/smt2_incremental/convert_expr_to_smt.h>
-
-#include <solvers/prop/literal_expr.h>
-#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 #include <util/expr.h>
 #include <util/expr_cast.h>
 #include <util/floatbv_expr.h>
@@ -18,6 +14,11 @@
 #include <util/std_expr.h>
 #include <util/string_constant.h>
 
+#include <solvers/prop/literal_expr.h>
+#include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
+#include <solvers/smt2_incremental/smt_core_theory.h>
+
 #include <functional>
 #include <numeric>
 
@@ -98,8 +99,116 @@ static smt_termt convert_expr_to_smt(const nondet_symbol_exprt &nondet_symbol)
     nondet_symbol.pretty());
 }
 
+/// \brief Makes a term which is true if \p input is not 0 / false.
+static smt_termt make_not_zero(const smt_termt &input, const typet &source_type)
+{
+  if(input.get_sort().cast<smt_bool_sortt>())
+    return input;
+  return smt_core_theoryt::distinct(
+    input, convert_expr_to_smt(from_integer(0, source_type)));
+}
+
+/// \brief Returns a cast to C bool expressed in smt terms.
+static smt_termt convert_c_bool_cast(
+  const smt_termt &from_term,
+  const typet &from_type,
+  const bitvector_typet &to_type)
+{
+  const std::size_t c_bool_width = to_type.get_width();
+  return smt_core_theoryt::if_then_else(
+    make_not_zero(from_term, from_type),
+    smt_bit_vector_constant_termt{1, c_bool_width},
+    smt_bit_vector_constant_termt{0, c_bool_width});
+}
+
+static smt_termt make_bitvector_resize_cast(
+  const smt_termt &from_term,
+  const bitvector_typet &from_type,
+  const bitvector_typet &to_type)
+{
+  if(const auto to_fixedbv_type = type_try_dynamic_cast<fixedbv_typet>(to_type))
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for type cast to fixed-point bitvector "
+      "type: " +
+      to_type.pretty());
+  }
+  if(const auto to_floatbv_type = type_try_dynamic_cast<floatbv_typet>(to_type))
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for type cast to floating-point bitvector "
+      "type: " +
+      to_type.pretty());
+  }
+  const std::size_t from_width = from_type.get_width();
+  const std::size_t to_width = to_type.get_width();
+  if(to_width == from_width)
+    return from_term;
+  if(to_width < from_width)
+    return smt_bit_vector_theoryt::extract(to_width - 1, 0)(from_term);
+  const std::size_t extension_size = to_width - from_width;
+  if(can_cast_type<signedbv_typet>(from_type))
+    return smt_bit_vector_theoryt::sign_extend(extension_size)(from_term);
+  else
+    return smt_bit_vector_theoryt::zero_extend(extension_size)(from_term);
+}
+
+struct sort_based_cast_to_bit_vector_convertert final
+  : public smt_sort_const_downcast_visitort
+{
+  const smt_termt &from_term;
+  const typet &from_type;
+  const bitvector_typet &to_type;
+  optionalt<smt_termt> result;
+
+  sort_based_cast_to_bit_vector_convertert(
+    const smt_termt &from_term,
+    const typet &from_type,
+    const bitvector_typet &to_type)
+    : from_term{from_term}, from_type{from_type}, to_type{to_type}
+  {
+  }
+
+  void visit(const smt_bool_sortt &) override
+  {
+    result = convert_c_bool_cast(
+      from_term, from_type, c_bool_typet{to_type.get_width()});
+  }
+
+  void visit(const smt_bit_vector_sortt &) override
+  {
+    if(const auto bitvector = type_try_dynamic_cast<bitvector_typet>(from_type))
+      result = make_bitvector_resize_cast(from_term, *bitvector, to_type);
+    else
+      UNIMPLEMENTED_FEATURE(
+        "Generation of SMT formula for type cast to bit vector from type: " +
+        from_type.pretty());
+  }
+};
+
+static smt_termt convert_bit_vector_cast(
+  const smt_termt &from_term,
+  const typet &from_type,
+  const bitvector_typet &to_type)
+{
+  sort_based_cast_to_bit_vector_convertert converter{
+    from_term, from_type, to_type};
+  from_term.get_sort().accept(converter);
+  POSTCONDITION(converter.result);
+  return *converter.result;
+}
+
 static smt_termt convert_expr_to_smt(const typecast_exprt &cast)
 {
+  const auto from_term = convert_expr_to_smt(cast.op());
+  const typet &from_type = cast.op().type();
+  const typet &to_type = cast.type();
+  if(const auto bool_type = type_try_dynamic_cast<bool_typet>(to_type))
+    return make_not_zero(from_term, cast.op().type());
+  if(const auto c_bool_type = type_try_dynamic_cast<c_bool_typet>(to_type))
+    return convert_c_bool_cast(from_term, from_type, *c_bool_type);
+  if(const auto bit_vector = type_try_dynamic_cast<bitvector_typet>(to_type))
+    return convert_bit_vector_cast(from_term, from_type, *bit_vector);
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for type cast expression: " + cast.pretty());
 }

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -25,6 +25,15 @@ class smt_bit_vector_theoryt
     std::vector<smt_indext> indices() const;
     void validate(const smt_termt &operand) const;
   };
+  /// \brief
+  ///   Makes a factory for extract function applications.
+  /// \param i
+  ///   Index of the highest bit to be included in the resulting bit vector.
+  /// \param j
+  ///   Index of the lowest bit to be included in the resulting bit vector.
+  /// \note
+  ///   Bit vectors are zero indexed. So the lowest bit index is zero and the
+  ///   largest index is the size of the bit vector minus one.
   static smt_function_application_termt::factoryt<extractt>
   extract(std::size_t i, std::size_t j);
 

src/solvers/smt2_incremental/smt_core_theory.h

@@ -62,6 +62,8 @@ class smt_core_theoryt
     static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
     static void validate(const smt_termt &lhs, const smt_termt &rhs);
   };
+  /// Makes applications of the function which returns true iff its two
+  /// arguments are not identical.
   static const smt_function_application_termt::factoryt<distinctt> distinct;
 
   struct if_then_elset final

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -3,13 +3,17 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
+#include <util/config.h>
+#include <util/constructor_of.h>
 #include <util/format.h>
 #include <util/std_expr.h>
 
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/smt_bit_vector_theory.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/use_catch.h>
 
 TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
@@ -814,3 +818,126 @@ SCENARIO(
     }
   }
 }
+
+TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
+{
+  const symbol_exprt bool_expr{"foo", bool_typet{}};
+  const smt_termt bool_term = smt_identifier_termt{"foo", smt_bool_sortt{}};
+  const symbol_exprt bv_expr{"bar", signedbv_typet(12)};
+  const smt_termt bv_term =
+    smt_identifier_termt{"bar", smt_bit_vector_sortt{12}};
+  SECTION("Casts to bool")
+  {
+    CHECK(
+      convert_expr_to_smt(typecast_exprt{bool_expr, bool_typet{}}) ==
+      bool_term);
+    CHECK(
+      convert_expr_to_smt(typecast_exprt{bv_expr, bool_typet{}}) ==
+      smt_core_theoryt::distinct(
+        bv_term, smt_bit_vector_constant_termt{0, 12}));
+  }
+  SECTION("Casts to C bool")
+  {
+    // The config lines are necessary because when we do casting to C bool the
+    // bit width depends on the configuration.
+    config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+    config.ansi_c.set_arch_spec_i386();
+    const std::size_t c_bool_width = config.ansi_c.bool_width;
+    const smt_bit_vector_constant_termt c_true{1, c_bool_width};
+    const smt_bit_vector_constant_termt c_false{0, c_bool_width};
+    SECTION("from bool")
+    {
+      const auto cast_bool =
+        convert_expr_to_smt(typecast_exprt{bool_expr, c_bool_type()});
+      const auto expected_bool_conversion =
+        smt_core_theoryt::if_then_else(bool_term, c_true, c_false);
+      CHECK(cast_bool == expected_bool_conversion);
+    }
+    SECTION("from bit vector")
+    {
+      const auto cast_bit_vector =
+        convert_expr_to_smt(typecast_exprt{bv_expr, c_bool_type()});
+      const auto expected_bit_vector_conversion =
+        smt_core_theoryt::if_then_else(
+          smt_core_theoryt::distinct(
+            bv_term, smt_bit_vector_constant_termt{0, 12}),
+          c_true,
+          c_false);
+      CHECK(cast_bit_vector == expected_bit_vector_conversion);
+    }
+  }
+  SECTION("Casts to bit vector")
+  {
+    SECTION("Matched width casts")
+    {
+      typet from_type, to_type;
+      using rowt = std::pair<typet, typet>;
+      std::tie(from_type, to_type) = GENERATE(
+        rowt{unsignedbv_typet{8}, unsignedbv_typet{8}},
+        rowt{unsignedbv_typet{8}, signedbv_typet{8}},
+        rowt{signedbv_typet{8}, unsignedbv_typet{8}});
+      CHECK(
+        convert_expr_to_smt(
+          typecast_exprt{from_integer(1, from_type), to_type}) ==
+        smt_bit_vector_constant_termt{1, 8});
+    }
+    SECTION("Narrowing casts")
+    {
+      CHECK(
+        convert_expr_to_smt(typecast_exprt{bv_expr, signedbv_typet{8}}) ==
+        smt_bit_vector_theoryt::extract(7, 0)(bv_term));
+      CHECK(
+        convert_expr_to_smt(typecast_exprt{
+          from_integer(42, unsignedbv_typet{32}), unsignedbv_typet{16}}) ==
+        smt_bit_vector_theoryt::extract(15, 0)(
+          smt_bit_vector_constant_termt{42, 32}));
+    }
+    SECTION("Widening casts")
+    {
+      std::size_t from_width, to_width, extension_width;
+      using size_rowt = std::tuple<std::size_t, std::size_t, std::size_t>;
+      std::tie(from_width, to_width, extension_width) = GENERATE(
+        size_rowt{8, 64, 56}, size_rowt{16, 32, 16}, size_rowt{16, 128, 112});
+      PRECONDITION(from_width < to_width);
+      PRECONDITION(to_width - from_width == extension_width);
+      using make_typet = std::function<typet(std::size_t)>;
+      const make_typet make_unsigned = constructor_oft<unsignedbv_typet>{};
+      const make_typet make_signed = constructor_oft<signedbv_typet>{};
+      using make_extensiont =
+        std::function<std::function<smt_termt(smt_termt)>(std::size_t)>;
+      const make_extensiont zero_extend = smt_bit_vector_theoryt::zero_extend;
+      const make_extensiont sign_extend = smt_bit_vector_theoryt::sign_extend;
+      make_typet make_source_type, make_destination_type;
+      make_extensiont make_extension;
+      using types_rowt = std::tuple<make_typet, make_typet, make_extensiont>;
+      std::tie(make_source_type, make_destination_type, make_extension) =
+        GENERATE_REF(
+          types_rowt{make_unsigned, make_unsigned, zero_extend},
+          types_rowt{make_signed, make_signed, sign_extend},
+          types_rowt{make_signed, make_unsigned, sign_extend},
+          types_rowt{make_unsigned, make_signed, zero_extend});
+      const typecast_exprt cast{
+        from_integer(42, make_source_type(from_width)),
+        make_destination_type(to_width)};
+      const smt_termt expected_term = make_extension(extension_width)(
+        smt_bit_vector_constant_termt{42, from_width});
+      CHECK(convert_expr_to_smt(cast) == expected_term);
+    }
+    SECTION("from bool")
+    {
+      const exprt from_expr = GENERATE(
+        exprt{symbol_exprt{"baz", bool_typet{}}},
+        exprt{true_exprt{}},
+        exprt{false_exprt{}});
+      const smt_termt from_term = convert_expr_to_smt(from_expr);
+      const std::size_t width = GENERATE(1, 8, 16, 32, 64);
+      const typecast_exprt cast{from_expr, bitvector_typet{ID_bv, width}};
+      CHECK(
+        convert_expr_to_smt(cast) ==
+        smt_core_theoryt::if_then_else(
+          from_term,
+          smt_bit_vector_constant_termt{1, width},
+          smt_bit_vector_constant_termt{0, width}));
+    }
+  }
+}