Skip to content

Simplify pointer casts of pointer arithmetic#8836

Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:simp-tc-pointer-arith
Open

Simplify pointer casts of pointer arithmetic#8836
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:simp-tc-pointer-arith

Conversation

@tautschnig
Copy link
Collaborator

This permits simplifying, e.g., (char*)(ptr + 1) + -1 to (char*)ptr when ptr is unsigned char*. This, in turn, avoids different formulae produced on AArch64 (where char is unsigned) and Apple Silicon/macOS (where char is signed, as is the case on x86).

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

This permits simplifying, e.g., `(char*)(ptr + 1) + -1` to `(char*)ptr`
when `ptr` is `unsigned char*`. This, in turn, avoids different formulae
produced on AArch64 (where `char` is unsigned) and Apple Silicon/macOS
(where `char` is signed, as is the case on x86).
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

This PR extends the expression simplifier to normalize pointer-to-pointer casts around pointer arithmetic, enabling cast-pushdown and offset scaling based on element-size ratios to avoid target-dependent formula differences (e.g., due to char signedness on different architectures).

Changes:

  • Add a new simplify_typecast rewrite that pushes pointer typecasts into pointer + expressions when element-size ratios are integral.
  • Scale integer offset operands by sizeof(inner)/sizeof(outer) and simplify the resulting + expression.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

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.
Comment on lines +1015 to +1051
// 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());
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)));
}
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

@codecov
Copy link

codecov bot commented Feb 16, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.00%. Comparing base (15eb10a) to head (92349db).

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8836   +/-   ##
========================================
  Coverage    80.00%   80.00%           
========================================
  Files         1700     1700           
  Lines       188252   188274   +22     
  Branches        73       73           
========================================
+ Hits        150613   150631   +18     
- Misses       37639    37643    +4     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants