Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 39 additions & 0 deletions src/util/simplify_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1012,6 +1012,45 @@ 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)
{
const typet size_t_type(size_type());
Copy link

Copilot AI Feb 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

size_t_type is declared but never used in this new pointer-typecast rewrite branch. This will trigger an unused-variable warning (and can fail builds when warnings are treated as errors). Remove it or use it as intended (e.g., if operands are meant to be cast to size_t, apply it explicitly).

Suggested change
const typet size_t_type(size_type());

Copilot uses AI. Check for mistakes.
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)));
}
Comment on lines +1015 to +1051
Copy link

Copilot AI Feb 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This introduces new simplification behaviour for pointer-to-pointer casts over pointer arithmetic, but there doesn’t appear to be a unit/regression test exercising it. Please add a test (e.g., covering the motivating case (char*)(ptr + 1) + -1 -> (char*)ptr when ptr is unsigned char*, and at least one non-trivial element-size ratio case) to prevent regressions across architectures/char signedness.

Copilot uses AI. Check for mistakes.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@copilot open a new pull request to apply changes based on this feedback

}

const irep_idt &expr_type_id=expr_type.id();
const exprt &operand = expr.op();
const irep_idt &op_type_id=op_type.id();
Expand Down
Loading