AliveToolkit / alive2

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

wrong result? #1065

Closed regehr closed 2 days ago

regehr commented 2 days ago

I'm concerned about Alive's answer here. it looks to me (and to LLVM) like src should always return a vector of zeroes, but Alive disagrees.

define <4 x i32> @f(<4 x i32> %0) {
  %2 = icmp eq <4 x i32> %0, zeroinitializer
  %3 = shufflevector <4 x i32> %0, <4 x i32> zeroinitializer, <4 x i32> <i32 1, i32 1, i32 0, i32 3>
  %4 = select <4 x i1> %2, <4 x i32> %3, <4 x i32> zeroinitializer
  ret <4 x i32> %4
}
regehr@ohm:~$ ~/alive2-regehr/build/alive-tv foo.ll -disable-poison-input -disable-undef-input

----------------------------------------
define <4 x i32> @f(<4 x i32> %#0) {
#1:
  %#2 = icmp eq <4 x i32> %#0, { 0, 0, 0, 0 }
  %#3 = shufflevector <4 x i32> %#0, <4 x i32> { 0, 0, 0, 0 }, 1, 1, 0, 3
  %#4 = select <4 x i1> %#2, <4 x i32> %#3, <4 x i32> { 0, 0, 0, 0 }
  ret <4 x i32> %#4
}
=>
define <4 x i32> @f(<4 x i32> %#0) nofree noundef willreturn memory(none) {
#1:
  ret <4 x i32> { 0, 0, 0, 0 }
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
<4 x i32> %#0 = < #x00000001 (1), #x00000000 (0), #x00000000 (0), #x00000000 (0) >

Source:
<4 x i1> %#2 = < #x0 (0), #x1 (1), #x1 (1), #x1 (1) >
<4 x i32> %#3 = < #x00000000 (0), #x00000000 (0), #x00000001 (1), #x00000000 (0) >
<4 x i32> %#4 = < #x00000000 (0), #x00000000 (0), #x00000001 (1), #x00000000 (0) >

Target:
Source value: < #x00000000 (0), #x00000000 (0), #x00000001 (1), #x00000000 (0) >
Target value: < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) >

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
regehr@ohm:~$ 
regehr commented 2 days ago

wait I need to think about this more

regehr commented 2 days ago

yeah sorry, this was my mistake and LLVM's -- I was seeing some consistent behavior from the middle end and the ARM64 backend and I let that trick me