pointer comparison in GIMPLE

[Jose E. Marchesi]

> On Wed, 10 Dec 2025, Martin Uecker wrote:
>
>> Date: Wed, 10 Dec 2025 09:11:14 +0100
>> From: Martin Uecker <muecker@gwdg.de>
>> To: Krister Walfridsson <krister.walfridsson@gmail.com>, gcc@gcc.gnu.org
>> Cc: Richard Biener <richard.guenther@gmail.com>
>> Subject: Re: pointer comparison in GIMPLE
>> Am Mittwoch, dem 10.12.2025 um 03:51 +0000 schrieb Krister
>> Walfridsson via Gcc:
>>> 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?
>>
>> Are the precise GIMPLE semantics documented somewhere?   I would guess that
>> some notion of provenance would be criticial also for GIMPLE.
>
> It is, to my knowledge, not conveniently documented in one place, even
> though the information is probably available spread out across the
> internals manual, various .def files, and comments in the source code.
>
> I plan to write some documentation when I have fully figured out the
> rules. The following two earlier mail threads and bug report are part
> of that effort:
> * https://gcc.gnu.org/pipermail/gcc/2025-March/245763.html
> * https://gcc.gnu.org/pipermail/gcc/2025-April/245870.html
> * https://gcc.gnu.org/bugzilla/show_bug.cgi?id=120980

That would be really awesome.