AliveToolkit / alive2

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

Incorrect handling of poison values #1038

Closed artagnon closed 1 month ago

artagnon commented 1 month ago

Input to Alive2:

define i16 @src() {
  %and = and i16 poison, 0
  ret i16 %and
}

define i16 @tgt() {
  ret i16 3
}

Changing ret i16 3 to any other return value has no impact on correctness.

Handy link: https://alive2.llvm.org/ce/z/2KR-wy

nunoplopes commented 1 month ago

Right, because poison can be replaced by any value. Alive2 is correct.