AliveToolkit / alive2

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

Incorrect handling of undef values #1039

Closed artagnon closed 1 month ago

artagnon commented 1 month ago

Input to Alive2:

%struct.widget = type { i16, i16, i16, i16, i16, i16 }

; Miscompile. Correct output: 1, incorrect output: poison.
define i16 @src(ptr %p, i16 %x, i16 %y) {
  store %struct.widget { i16 0, i16 0, i16 0, i16 0, i16 2, i16 0 }, ptr %p
  %insert.y = insertelement <2 x i16> zeroinitializer, i16 %y, i64 0
  %insert.x = insertelement <2 x i16> %insert.y, i16 %x, i64 1
  %shufflevector = shufflevector <2 x i16> %insert.x, <2 x i16> zeroinitializer, <4 x i32> <i32 0, i32 1, i32 undef, i32 undef>
  %extract = extractelement <4 x i16> %shufflevector, i32 2 ; undef
  %and = and i16 %extract, 0 ; 0
  %gep = getelementptr %struct.widget, ptr %p, i32 0, i32 4
  %load = load i16, ptr %gep ; 2
  %or = or i16 %and, %load ; 2
  %ashr = ashr i16 %or, 1 ; 1
  ret i16 %ashr ; 1
}

define i16 @tgt(ptr %p, i16 %x, i16 %y) {
  store i16 0, ptr %p, align 2
  %p.repack1 = getelementptr inbounds i8, ptr %p, i64 2
  store i16 0, ptr %p.repack1, align 2
  %p.repack2 = getelementptr inbounds i8, ptr %p, i64 4
  store i16 0, ptr %p.repack2, align 2
  %p.repack3 = getelementptr inbounds i8, ptr %p, i64 6
  store i16 0, ptr %p.repack3, align 2
  %p.repack4 = getelementptr inbounds i8, ptr %p, i64 8
  store i16 2, ptr %p.repack4, align 2
  %p.repack5 = getelementptr inbounds i8, ptr %p, i64 10
  store i16 0, ptr %p.repack5, align 2
  ret i16 poison
}

Output: Transformation seems to be correct.

Reasoning by hand, we see that the function should return 1, not poison. Handy link: https://alive2.llvm.org/ce/z/AR3vZm

nunoplopes commented 1 month ago

Stop opening issues if you don't understand UB please. The result is correct to be poison.