Implement conversion of boolean casts into SMT2 terms

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,37 @@ 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 c_bool_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 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);
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for type cast expression: " + cast.pretty());
 }

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -3,13 +3,16 @@
 #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/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 +817,52 @@ 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);
+    }
+  }
+}