llvm / llvm-project

The LLVM Project is a collection of modular and reusable compiler and toolchain technologies.
http://llvm.org
Other
29.38k stars 12.15k forks source link

Wrong simplification of `or` and `icmp`s on a undefined value #113860

Open bongjunj opened 1 month ago

bongjunj commented 1 month ago

Alive2 report: https://alive2.llvm.org/ce/z/gu_KaN

(y >= (x | y)) | (x = 0) -> (x | y) = y

----------------------------------------
define i1 @ule_swap_or_min.2(i8 %x, i8 %y) {
#0:
  %#1 = or i8 %x, %y
  %cmp = icmp uge i8 %y, %#1
  %cmpeq = icmp eq i8 %x, 0
  %r = or i1 %cmp, %cmpeq
  ret i1 %r
}
=>
define i1 @ule_swap_or_min.2(i8 %x, i8 %y) {
#0:
  %#1 = or i8 %x, %y
  %cmp = icmp eq i8 %#1, %y
  ret i1 %cmp
}
Transformation doesn't verify!

ERROR: Target's return value is more undefined

Example:
i8 %x = #x00 (0)
i8 %y = undef

Source:
i8 %#1 = #x00 (0)   [based on undef value]
i1 %cmp = #x1 (1)
i1 %cmpeq = #x1 (1)
i1 %r = #x1 (1)

Target:
i8 %#1 = #x00 (0)
i1 %cmp = #x0 (0)
Source value: #x1 (1)
Target value: #x0 (0)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
RKSimon commented 3 weeks ago

Missing freeze?


----------------------------------------
define i1 @src(i8 %x, i8 %y) {
#0:
  %#1 = or i8 %x, %y
  %cmp = icmp uge i8 %y, %#1
  %cmpeq = icmp eq i8 %x, 0
  %r = or i1 %cmp, %cmpeq
  ret i1 %r
}
=>
define i1 @tgt(i8 %x, i8 %y) {
#0:
  %fy = freeze i8 %y
  %#1 = or i8 %x, %fy
  %cmp = icmp eq i8 %#1, %fy
  ret i1 %cmp
}
Transformation seems to be correct!