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

regression/contracts/no_redudant_checks/test.desc

@@ -23,8 +23,7 @@ main.c
 ^\[main.pointer_arithmetic.15\].*: SUCCESS
 ^\[main.pointer_arithmetic.16\].*: SUCCESS
 ^\[main.pointer_arithmetic.17\].*: SUCCESS
-^\[main.pointer_arithmetic.18\].*: SUCCESS
-^\*\* 0 of 21 failed \(1 iterations\)
+^\*\* 0 of 20 failed \(1 iterations\)
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.overflow.\d+\].*: FAILURE
@@ -33,10 +32,10 @@ Checks that assertions generated by the first --pointer-overflow-check:
 - do not get duplicated by the second --unsigned-overflow-check
 - do not get instrumented with --unsigned-overflow-check (would fail the proof)
 
-We expect 20 assertions to be generated:
+We expect 19 assertions to be generated:
 In the goto-instrument run:
 - 2 for using malloc
-- 18 caused by --pointer-overflow-check
+- 17 caused by --pointer-overflow-check
 
 In the final cbmc run:
 - 0 caused by --pointer-overflow-check

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,17 @@ 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);
+}