diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index d601ef06e3f..eafb91a040a 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -236,22 +236,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(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); diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 22ac8b40f94..41f8adad246 100644 --- a/unit/util/simplify_expr.cpp +++ b/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()); }