Implement conversion of bit vector casts into SMT2 terms

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -112,7 +112,7 @@ static smt_termt make_not_zero(const smt_termt &input, const typet &source_type)
 static smt_termt convert_c_bool_cast(
   const smt_termt &from_term,
   const typet &from_type,
-  const c_bool_typet &to_type)
+  const bitvector_typet &to_type)
 {
   const std::size_t c_bool_width = to_type.get_width();
   return smt_core_theoryt::if_then_else(
@@ -121,6 +121,83 @@ static smt_termt convert_c_bool_cast(
     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());
@@ -130,6 +207,8 @@ static smt_termt convert_expr_to_smt(const typecast_exprt &cast)
     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());
 }

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -5,6 +5,7 @@
 #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>
 
@@ -865,4 +866,78 @@ TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
       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}));
+    }
+  }
 }