Source and Target Example Values Diverge Before Source Code Does

[FlashSheridan]

Source and Target Example Values Diverge Before Source Code Does

[nunoplopes]

Thank you @nunoplopes for your response! What puzzles me is that @llvm.uadd.with.overflow will be converted to the add + ult during legalization phase (LLVM common code is responsible for this), so does that mean we can get the same problem with undef like here?

No one said that LLVM was correct 🙂
Legalization at the end of the pipeline, so in practice it may not matter since assembly doesn't have undef. SDAG does have undef & poison, so I'm not saying everything is great, but the chances of miscompilations is low.
That's not true if done in the middle of the optimization pipeline. But these days. clang adds noundef to most (all?) function arguments, so it's relatively easy to ensure something isn't undef. You can also use freeze.

[nunoplopes]

I'm sorry to say but the optimization is indeed incorrect when %arg1 is undef. You can see that Alive2 proves it correct if you add noundef to the first argument.
This is because @llvm.uadd.with.overflow does the addition and overflow check with the same value, while if you lower it into add+icmp, each operation may observe different values for %arg1m (undef can yield a different value each time it is used).

Take the counterexample, where %modulo = #x3.
Then %arg1m and %arg2m must be in [0,2] and so their sum never overflows. So %obit in src is always false.
On the other hand, in tgt, icmp ult %sum, %arg1m can yield true or false depending on the inputs. Then branching on a non-deterministic value is UB.

I know the counterexample isn't too easy to read. But the optimization is incorrect.

[vladimirradosavljevic]

Thank you @nunoplopes for your response!
What puzzles me is that @llvm.uadd.with.overflow will be converted to the add + ult during legalization phase (LLVM common code is responsible for this), so does that mean we can get the same problem with undef like here?