AliveToolkit / alive2

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

`ERROR: program doesn't type check!` is raised when the intrinsic call has both noundef and range metadata. #1043

Closed dtcxzyw closed 1 month ago

dtcxzyw commented 1 month ago

Reproducer: https://alive2.llvm.org/ce/z/n5hPD-

define i32 @src(i32 %0) {
entry:
  %1 = call noundef i32 @llvm.ctlz.i32(i32 %0, i1 true), !range !0
  ret i32 %1
}

define i32 @tgt(i32 %0) {
entry:
  %1 = call noundef i32 @llvm.ctlz.i32(i32 %0, i1 true), !range !0
  ret i32 %1
}

!0 = !{i32 0, i32 33}
----------------------------------------
define i32 @src(i32 %#0) {
entry:
  %#1 = ctlz i32 %#0, 1
  assume_welldefined i32 %#1
  assume_range = !range void, i32 0, i32 33
  ret i32 assume_range
}
=>
define i32 @tgt(i32 %#0) {
entry:
  %#1 = ctlz i32 %#0, 1
  assume_welldefined i32 %#1
  assume_range = !range void, i32 0, i32 33
  ret i32 assume_range
}
Transformation doesn't verify!
ERROR: program doesn't type check!

It is weird that the input type of assume_range is void.

Without noundef, it works well:

----------------------------------------
define i32 @src(i32 %#0) {
entry:
  %#1 = ctlz i32 %#0, 1
  %#1_range = !range i32 %#1, i32 0, i32 33
  ret i32 %#1_range
}
=>
define i32 @tgt(i32 %#0) {
entry:
  %#1 = ctlz i32 %#0, 1
  %#1_range = !range i32 %#1, i32 0, i32 33
  ret i32 %#1_range
}
Transformation seems to be correct!