AliveToolkit / alive2

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

ERROR: program doesn't type check! #994

Closed regehr closed 6 months ago

regehr commented 6 months ago

not super important that we support this but I'm seeing vectors this big in some of the unit tests

define void @reduce_i1() {
  %1 = call i1 @llvm.vector.reduce.and.v1024i1(<1024 x i1> zeroinitializer)
  ret void
}

declare i1 @llvm.vector.reduce.and.v1024i1(<1024 x i1>)
regehr@john-home:~/test/results/840$ /home/regehr/alive2-regehr/build/alive-tv reduced.ll

----------------------------------------
define void @reduce_i1() {
#0:
  ret void
}
=>
define void @reduce_i1() nofree willreturn memory(none) {
#0:
  ret void
}
Transformation doesn't verify!
ERROR: program doesn't type check!

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