pointer comparison in GIMPLE

[Krister Walfridsson]

On Wed, 10 Dec 2025, Richard Biener wrote:

> Date: Wed, 10 Dec 2025 08:18:49 +0100
> From: Richard Biener <richard.guenther@gmail.com>
> To: Krister Walfridsson <krister.walfridsson@gmail.com>
> Cc: gcc@gcc.gnu.org
> Subject: Re: pointer comparison in GIMPLE
> 
>
>
>> Am 10.12.2025 um 04:53 schrieb Krister Walfridsson via Gcc <gcc@gcc.gnu.org>:
>>
>> 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