> Am 10.12.2025 um 09:07 schrieb Krister Walfridsson
> <[email protected]>:
>
> 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).
GIMPLE adopts most of the C pointer restrictions here thus we can (and do)
conclude that pointers stay within an object when advanced. This is used by
the PTA pass which results are used when we optimize your example. You have to
divert to integer arithmetic to circumvent this and the PTA pass, while
tracking provenance through integers as well, does the right thing with this.
Richard
>
> /Krister
