AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

Source function always being UB warning may be missing #1017

Closed antoniofrighetto closed 4 months ago

antoniofrighetto commented 4 months ago

Source function always being UB is not displayed when Alive2 is given in input the following:

define i8 @src(i8 %0) {
  %2 = shl i8 %0, 8
  ret i8 %2
}
=>
define i8 @tgt(i8 %0) {
  ret i8 poison
}

The expression appears to be satisfiable, I wonder though whether the semantic for shift amount larger or equal than the bitwidth shouldn't be the same one as division by zero?

cc/ @regehr

regehr commented 4 months ago

the difference is that a shift-past-bitwidth results in poison whereas divide-by-zero results in immediate UB. the "undefined for all inputs" warning is about the latter thing, not the former. if you want to promote poison/undef values to immediate UB, you can add the "noundef" return attribute to your function, and then you will get the warning.

antoniofrighetto commented 4 months ago

Thanks, makes sense. I think I was slightly confused by the fact that division-by-zero indeed results in immediate UB, but we seem to refine it to poison (https://alive2.llvm.org/ce/z/M7mzno), rather than to undef (as strongest form of UB? – whereas deferred UB, like shift-past-bitwidth, is correctly defined as poison).

regehr commented 4 months ago

well, that's the thing about refinement-- there are a lot of choices.

divide by zero could be optimized to unreachable, that's stronger than both undef and poison. I don't know why LLVM doesn't do that, this is either a deliberate policy choice or else just a random historical accident like we often see in these big code bases