Simplify pointer casts of pointer arithmetic

src/util/simplify_expr.cpp

@@ -1012,6 +1012,44 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     }
   }
 
+  // Push a pointer typecast into pointer arithmetic
+  // (T)(ptr + int) ---> (T)ptr + sizeof(inner-st)/sizeof(outer-st)*int
+  // when the inner subtype's size is a multiple of the outer subtype's size
+  if(
+    expr_type.id() == ID_pointer && op_type.id() == ID_pointer &&
+    expr.op().id() == ID_plus)
+  {
+    const auto step =
+      pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
+    const auto new_step =
+      pointer_offset_size(to_pointer_type(expr_type).base_type(), ns);
+
+    if(
+      step.has_value() && *step != 0 && new_step.has_value() &&
+      *new_step != 0 && *step >= *new_step && *step % *new_step == 0)
+    {
+      auto new_expr = expr.op();
+      new_expr.type() = expr.type();
+
+      for(auto &op : new_expr.operands())
+      {
+        if(op.type().id() == ID_pointer)
+        {
+          exprt new_op = simplify_typecast(typecast_exprt{op, expr.type()});
+          op = std::move(new_op);
+        }
+        else if(*step > *new_step)
+        {
+          exprt new_op = simplify_mult(
+            mult_exprt{from_integer(*step / *new_step, op.type()), op});
+          op = std::move(new_op);
+        }
+      }
+
+      return changed(simplify_plus(to_plus_expr(new_expr)));
+    }
+  }
+
   const irep_idt &expr_type_id=expr_type.id();
   const exprt &operand = expr.op();
   const irep_idt &op_type_id=op_type.id();

unit/util/simplify_expr.cpp

@@ -587,6 +587,48 @@ TEST_CASE("Simplify power", "[core][util]")
   }
 }
 
+TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]")
+{
+  config.set_arch("none");
+
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  SECTION("Same element size: (char*)(unsigned_char_ptr + 1)")
+  {
+    // (char*)(ptr + 1) where ptr is unsigned char* should push the cast inside
+    auto uchar_ptr_type = pointer_type(unsigned_char_type());
+    auto char_ptr_type = pointer_type(signed_char_type());
+    symbol_exprt ptr{"ptr", uchar_ptr_type};
+    plus_exprt ptr_plus_1{ptr, from_integer(1, pointer_diff_type())};
+    typecast_exprt cast{ptr_plus_1, char_ptr_type};
+
+    exprt result = simplify_expr(cast, ns);
+
+    // Expected: (char*)ptr + 1
+    plus_exprt expected{
+      typecast_exprt{ptr, char_ptr_type}, from_integer(1, pointer_diff_type())};
+    REQUIRE(result == expected);
+  }
+
+  SECTION("Element size ratio 4: (char*)(int_ptr + 1)")
+  {
+    // (char*)(ptr + 1) where ptr is int* should scale offset by 4
+    auto int_ptr_type = pointer_type(signed_int_type());
+    auto char_ptr_type = pointer_type(signed_char_type());
+    symbol_exprt ptr{"ptr", int_ptr_type};
+    plus_exprt ptr_plus_1{ptr, from_integer(1, pointer_diff_type())};
+    typecast_exprt cast{ptr_plus_1, char_ptr_type};
+
+    exprt result = simplify_expr(cast, ns);
+
+    // Expected: (char*)ptr + 4
+    plus_exprt expected{
+      typecast_exprt{ptr, char_ptr_type}, from_integer(4, pointer_diff_type())};
+    REQUIRE(result == expected);
+  }
+}
+
 TEST_CASE("Simplify quantifier", "[core][util]")
 {
   const symbol_tablet symbol_table;