AliveToolkit / alive2

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

likely bug related to --disable-undef-input #997

Closed regehr closed 6 months ago

regehr commented 6 months ago

here's a source function:

target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
target triple = "aarch64-linux-gnu"

define i46 @f(i46 %0) {
  %2 = udiv i46 0, %0
  %3 = icmp sge i46 0, %2
  %4 = urem i46 0, %2
  %5 = zext i1 %3 to i46
  %6 = udiv i46 %5, 1
  ret i46 0
}

the optimized version validates just fine:

regehr@john-home:~/alive2-regehr/build$ ./alive-tv reduced.ll --fail-src-ub

----------------------------------------
define i46 @f(i46 %#0) {
#1:
  %#2 = udiv i46 0, %#0
  %#3 = icmp sge i46 0, %#2
  %#4 = urem i46 0, %#2
  %#5 = zext i1 %#3 to i46
  %#6 = udiv i46 %#5, 1
  ret i46 0
}
=>
define i46 @f(i46 %#0) nofree willreturn memory(none) {
#1:
  ret i46 0
}
Transformation seems to be correct!

Summary:
  1 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
regehr@john-home:~/alive2-regehr/build$ 

however, --disable-undef-input causes an error:

regehr@john-home:~/alive2-regehr/build$ ./alive-tv reduced.ll --disable-undef-input --fail-src-ub

----------------------------------------
define i46 @f(i46 %#0) {
#1:
  %#2 = udiv i46 0, %#0
  %#3 = icmp sge i46 0, %#2
  %#4 = urem i46 0, %#2
  %#5 = zext i1 %#3 to i46
  %#6 = udiv i46 %#5, 1
  ret i46 0
}
=>
define i46 @f(i46 %#0) nofree willreturn memory(none) {
#1:
  ret i46 0
}
ERROR: Source function is always UB

Summary:
  0 correct transformations
  0 incorrect transformations
  1 failed-to-prove transformations
  0 Alive2 errors
regehr@john-home:~/alive2-regehr/build$ 
regehr commented 6 months ago

or maybe this isn't a bug?? I would think that 0 / undef would give zero, but on second thought I'm not 100% on that

nunoplopes commented 6 months ago

Added workaround.