> Am 10.12.2025 um 04:53 schrieb Krister Walfridsson via Gcc <[email protected]>:
> 
> 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.

IIRC only relational compares between different provenance pointers invoke UB 
in C, equality compares do not?

Richard 

> 
>   /Krister

Reply via email to