AliveToolkit / alive2

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

possible wrong result due to @llvm.is.constant #1061

Closed regehr closed 1 week ago

regehr commented 1 week ago

this transformation seems fine?

https://alive2.llvm.org/ce/z/FqXseG

----------------------------------------
define i32 @f(ptr %p) {
#0:
  %#3 = load i32, ptr %p, align 4
  %#4 = is.constant i32 %#3
  br i1 %#4, label %#2, label %#1

#1:
  br label %#2

#2:
  ret i32 %#3
}
=>
define i32 @f(ptr nocapture nowrite %p) nofree willreturn memory(argmem: read) {
#0:
  %#1 = load i32, ptr nocapture nowrite %p, align 4
  ret i32 %#1
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
ptr %p = pointer(non-local, block_id=1, offset=1, attrs=4)

Source:
i32 %#3 = poison
i1 %#4 = #x0 (0)
  >> Jump to %#1
  >> Jump to %#2

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 4    alloc type: 0   alive: false    address: 0
Block 1 >   size: 6 align: 1    alloc type: 0   alive: true address: 3

Target:
i32 %#1 = poison
Source value: #x00000000 (0)
Target value: poison