> 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
That would be really awesome.
