On Wed, 10 Dec 2025, Martin Uecker wrote:
Date: Wed, 10 Dec 2025 09:11:14 +0100
From: Martin Uecker <[email protected]>
To: Krister Walfridsson <[email protected]>, [email protected]
Cc: Richard Biener <[email protected]>
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
/Krister
