Simplify (T1)(T2)x over bv types where T1 and x have the same type

When T2 has the same width (and also is a bitvector type) then the
typecasts do not change the result -- we can use `x` directly.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -1366,6 +1366,20 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       // might enable further simplification
       return changed(simplify_typecast(new_expr)); // recursive call
     }
+    // (T1)(T2)x over bv types where T1 and T2 have the same width and the type
+    // of x is T1 --> x
+    const exprt &inner_op = to_typecast_expr(operand).op();
+    if(
+      inner_op.type() == expr_type &&
+      (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
+       expr_type_id == ID_bv) &&
+      (op_type_id == ID_unsignedbv || op_type_id == ID_signedbv ||
+       op_type_id == ID_bv) &&
+      to_bitvector_type(expr_type).get_width() ==
+        to_bitvector_type(operand.type()).get_width())
+    {
+      return inner_op;
+    }
   }
   else if(operand.id()==ID_address_of)
   {

unit/util/simplify_expr.cpp

@@ -652,3 +652,19 @@ TEST_CASE("Simplify quantifier", "[core][util]")
     REQUIRE(simplify_expr(forall_exprt{a, true_exprt{}}, ns) == true_exprt{});
   }
 }
+
+
+TEST_CASE("Simplify double typecast over bv types", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+
+  // (unsigned)(signed)x where x is unsigned and same width -> x
+  const unsignedbv_typet u32{32};
+  const signedbv_typet s32{32};
+  const symbol_exprt x{"x", u32};
+  const typecast_exprt inner{x, s32};
+  const typecast_exprt outer{inner, u32};
+  REQUIRE(simplify_expr(outer, ns) == x);
+}
+