pointer comparison in GIMPLE

[Richard Biener]

> Am 10.12.2025 um 09:07 schrieb Krister Walfridsson <krister.walfridsson@gmail.com>:
> 
> 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).

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