Merge pull request #1473 from reuk/reuk/simplify-expr-fixup

Simplify a broader range of java primitive types

Author: Thomas Kiley

src/util/simplify_expr.cpp

@@ -237,22 +237,29 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     return false;
   }
 
-  // eliminate casts to _Bool
-  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)
+  // circular casts through types shorter than `int`
+  if(op_type==signedbv_typet(32) &&
+     expr.op0().id()==ID_typecast)
+  {
+    if(expr_type==c_bool_typet(8) ||
+       expr_type==signedbv_typet(8) ||
+       expr_type==signedbv_typet(16) ||
+       expr_type==unsignedbv_typet(16))
     {
-      const auto &typecast=to_typecast_expr(expr.op0());
-      if(typecast.op().type().id()==ID_c_bool)
+      // We checked that the id was ID_typecast in the enclosing `if`
+      const auto &typecast=expr_checked_cast<typecast_exprt>(expr.op0());
+      if(typecast.op().type()==expr_type)
       {
         expr=typecast.op0();
         return false;
       }
     }
+  }
 
+  // eliminate casts to _Bool
+  if(expr_type.id()==ID_c_bool &&
+     op_type.id()!=ID_bool)
+  {
     // 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

@@ -61,22 +61,87 @@ TEST_CASE("Simplify const pointer offset")
   REQUIRE(offset_value==1234);
 }
 
-TEST_CASE("Simplify Java boolean -> int -> boolean casts")
+namespace
+{
+
+void test_unnecessary_cast(const typet &type)
 {
   config.set_arch("none");
 
-  const exprt simplified=simplify_expr(
-    typecast_exprt(
+  WHEN("The casts can be removed, they are")
+  {
+    const exprt simplified=simplify_expr(
       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");
+        typecast_exprt(symbol_exprt("foo", type), java_int_type()),
+        type),
+      namespacet(symbol_tablet()));
+
+    REQUIRE(simplified.id()==ID_symbol);
+    REQUIRE(simplified.type()==type);
+    const auto &symbol=to_symbol_expr(simplified);
+    REQUIRE(symbol.get_identifier()=="foo");
+  }
+
+  WHEN("Casts should remain, they are left untouched")
+  {
+    {
+      const exprt simplified=simplify_expr(
+        typecast_exprt(symbol_exprt("foo", type), java_int_type()),
+        namespacet(symbol_tablet()));
+
+      REQUIRE(simplified.id()==ID_typecast);
+      REQUIRE(simplified.type()==java_int_type());
+    }
+
+    {
+      const exprt simplified=simplify_expr(
+        typecast_exprt(symbol_exprt("foo", java_int_type()), type),
+        namespacet(symbol_tablet()));
+
+      REQUIRE(simplified.id()==ID_typecast);
+      REQUIRE(simplified.type()==type);
+    }
+  }
+
+  WHEN("Deeply nested casts are present, they are collapsed appropriately")
+  {
+    {
+      const exprt simplified=simplify_expr(
+        typecast_exprt(
+          typecast_exprt(
+            typecast_exprt(
+              typecast_exprt(
+                typecast_exprt(symbol_exprt("foo", type), java_int_type()),
+                type),
+              java_int_type()),
+            type),
+          java_int_type()),
+        namespacet(symbol_tablet()));
+
+      REQUIRE(
+        simplified==typecast_exprt(symbol_exprt("foo", type), java_int_type()));
+    }
+  }
+}
+
+} // namespace
+
+TEST_CASE("Simplify Java boolean -> int -> boolean casts")
+{
+  test_unnecessary_cast(java_boolean_type());
+}
+
+TEST_CASE("Simplify Java byte -> int -> byte casts")
+{
+  test_unnecessary_cast(java_byte_type());
+}
+
+TEST_CASE("Simplify Java char -> int -> char casts")
+{
+  test_unnecessary_cast(java_char_type());
+}
+
+TEST_CASE("Simplify Java short -> int -> short casts")
+{
+  test_unnecessary_cast(java_short_type());
 }