search

AliveToolkit / alive2

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

unconditionally check for source functions that are UB for all executions, but don't error out #991

Closed regehr closed 6 months ago

regehr commented 6 months ago

I think this is a really important usability thing for Alive users

regehr commented 6 months ago 
Johns-MacBook-Pro:build regehr$ ./alive-tv test.ll 

----------------------------------------
define i16 @f(i16 %#0) {
#1:
  %x = sdiv i16 %#0, 0
  ret i16 %x
}
=>
define i16 @f(i16 %#0) nofree willreturn memory(none) {
#1:
  ret i16 poison
}

****************************************
WARNING: Source function is always UB.
It can be refined by any target function.
Please make sure this is what you wanted.
****************************************

Transformation seems to be correct!

Summary:
  1 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
Johns-MacBook-Pro:build regehr$