Merge pull request #1438 from reuk/reuk/simplify-expr-improvement

Remove tautological typecasts

Author: tautschnig

src/util/simplify_expr.cpp

@@ -240,6 +240,18 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
   if(expr_type.id()==ID_c_bool &&
      op_type.id()!=ID_bool)
   {
+    // casts from boolean to a signed int and back:
+    // (boolean)(int)boolean -> boolean
+    if(expr.op0().id()==ID_typecast && op_type.id()==ID_signedbv)
+    {
+      const auto &typecast=to_typecast_expr(expr.op0());
+      if(typecast.op().type().id()==ID_c_bool)
+      {
+        expr=typecast.op0();
+        return false;
+      }
+    }
+
     // rewrite (_Bool)x to (_Bool)(x!=0)
     binary_relation_exprt inequality;
     inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);

unit/util/simplify_expr.cpp

@@ -8,8 +8,10 @@
 
 #include <catch.hpp>
 
+#include <java_bytecode/java_types.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/namespace.h>
 #include <util/pointer_predicates.h>
 #include <util/simplify_expr.h>
@@ -18,6 +20,8 @@
 
 TEST_CASE("Simplify pointer_offset(address of array index)")
 {
+  config.set_arch("none");
+
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
@@ -38,6 +42,8 @@ TEST_CASE("Simplify pointer_offset(address of array index)")
 
 TEST_CASE("Simplify const pointer offset")
 {
+  config.set_arch("none");
+
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
@@ -54,3 +60,23 @@ TEST_CASE("Simplify const pointer offset")
   REQUIRE(!to_integer(simp, offset_value));
   REQUIRE(offset_value==1234);
 }
+
+TEST_CASE("Simplify Java boolean -> int -> boolean casts")
+{
+  config.set_arch("none");
+
+  const exprt simplified=simplify_expr(
+    typecast_exprt(
+      typecast_exprt(
+        symbol_exprt(
+          "foo",
+          java_boolean_type()),
+        java_int_type()),
+      java_boolean_type()),
+    namespacet(symbol_tablet()));
+
+  REQUIRE(simplified.id()==ID_symbol);
+  REQUIRE(simplified.type()==java_boolean_type());
+  const auto &symbol=to_symbol_expr(simplified);
+  REQUIRE(symbol.get_identifier()=="foo");
+}