On Wed, 10 Dec 2025, Richard Biener wrote:
Date: Wed, 10 Dec 2025 08:18:49 +0100
From: Richard Biener <[email protected]>
To: Krister Walfridsson <[email protected]>
Cc: [email protected]
Subject: Re: pointer comparison in GIMPLE
Am 10.12.2025 um 04:53 schrieb Krister Walfridsson via Gcc <[email protected]>:
I have a problem in smtgcc with the semantics of pointer comparison in GIMPLE.
Consider the function foo:
void foo(char *p, long long i)
{
char a;
if (p + i == &a)
__builtin_abort();
}
The FRE pass determines that the condition is always false, and the
if-statement is removed. This is correct in the C semantics, as the only way
the condition can be true invokes undefined behavior. But GIMPLE is more
permissive, so p + i may in fact evaluate to the address of a. So something
else is needed to allow this optimization for GIMPLE.
This could easily be fixed by letting EQ_EXPR evaluate to false for pointers with
different provenance. But that makes other optimizations invalid because then p >
q, p == q, and p < q can all be false simultaneously.
So I guess I am missing something... Why is this optimization allowed on GIMPLE?
We do the optimization based on pointer analysis which computes provenance
that’s useful for alias analysis. GIMPLE does not optimize relational compares
this way - while those are UB we do not decide one way or the other IIRC.
But my point is that the GIMPLE semantics do not allow you to conclude
that the pointers do not alias!
In C, a pointer must point into an object (or one past it), otherwise the
behavior is undefined. So we know that p points into some object (or one
past it), and p + i must also point into that same object (or one past
it). Therefore it cannot be equal to &a (at least if we assume there is at
least a one-byte gap at the start of the stack, or we can argue as in the
comments of PR61502).
The problem is that in GIMPLE, a pointer does not need to be in bounds.
The caller could call the function with a value of i such that p + i
happens to be equal to &a. So, as I understand it, the GIMPLE semantics
do not allow the pass to conclude that p + i == &a is false, unless p + i
is dereferenced (because dereferencing a through p + i would be UB due to
provenance).
/Krister
