simplifier: eliminate casts from bool to number

This usually enables subsequent simplification, e.g.,

((int)B) != 0

turns into

(B?1:0) != 0

and then into

B?1!=0:0!=0

and then into

B?true:false

which then turns into

B

Author: Daniel Kroening

jbmc/unit/util/simplify_expr.cpp

@@ -47,6 +47,17 @@ void test_unnecessary_cast(const typet &type)
       REQUIRE(simplified.type()==java_int_type());
     }
 
+    // casts from boolean get rewritten to ?:
+    if(type == java_boolean_type())
+    {
+      const exprt simplified = simplify_expr(
+        typecast_exprt(symbol_exprt("foo", java_int_type()), type),
+        namespacet(symbol_tablet()));
+
+      REQUIRE(simplified.id() == ID_if);
+      REQUIRE(simplified.type() == type);
+    }
+    else
     {
       const exprt simplified=simplify_expr(
         typecast_exprt(symbol_exprt("foo", java_int_type()), type),

src/util/simplify_expr.cpp

@@ -576,6 +576,19 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     return std::move(inequality);
   }
 
+  // eliminate casts from proper bool
+  if(
+    op_type.id() == ID_bool &&
+    (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv ||
+     expr_type.id() == ID_c_bool || expr_type.id() == ID_c_bit_field))
+  {
+    // rewrite (T)(bool) to bool?1:0
+    auto one = from_integer(1, expr_type);
+    auto zero = from_integer(0, expr_type);
+    exprt new_expr = if_exprt(expr.op(), std::move(one), std::move(zero));
+    return changed(simplify_rec(new_expr)); // recursive call
+  }
+
   // circular casts through types shorter than `int`
   if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)
   {

unit/util/simplify_expr.cpp

@@ -244,3 +244,18 @@ TEST_CASE("Simplify pointer_object equality", "[core][util]")
 
   REQUIRE(simp.is_true());
 }
+
+TEST_CASE("Simplify cast from bool", "[core][util]")
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  // this checks that ((int)B)==1 turns into B
+  exprt B = symbol_exprt("B", bool_typet());
+  exprt comparison = equal_exprt(
+    typecast_exprt(B, signedbv_typet(32)), from_integer(1, signedbv_typet(32)));
+
+  exprt simp = simplify_expr(comparison, ns);
+
+  REQUIRE(simp == B);
+}