llvm / llvm-project

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

Wrong simplification by GVN #99797

Open bongjunj opened 4 months ago

bongjunj commented 4 months ago

alive2 report: https://alive2.llvm.org/ce/z/Q7wtE9

----------------------------------------
define i1 @fun0(i8 %val0, i8 %val1) {
#0:
  %val2 = and i8 %val0, 1
  %val3 = icmp eq i8 %val2, 0
  %val4 = add i8 %val1, %val2
  %val5 = icmp eq i8 %val1, %val4
  %val6 = or i1 %val3, %val5
  ret i1 %val6
}
=>
define i1 @fun0(i8 %val0, i8 %val1) {
#0:
  %val2 = and i8 %val0, 1
  %val4 = add i8 %val1, %val2
  %val5 = icmp eq i8 %val1, %val4
  ret i1 %val5
}
Transformation doesn't verify!

ERROR: Target's return value is more undefined

Example:
i8 %val0 = #x00 (0)
i8 %val1 = undef

Source:
i8 %val2 = #x00 (0)
i1 %val3 = #x1 (1)
i8 %val4 = #x00 (0) [based on undef value]
i1 %val5 = #x1 (1)  [based on undef value]
i1 %val6 = #x1 (1)

Target:
i8 %val2 = #x00 (0)
i8 %val4 = #x01 (1)
i1 %val5 = #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
wangbyby commented 4 months ago

What if %val0 and %val1 both not undef?

bongjunj commented 4 months ago

What if %val0 and %val1 both not undef?

Then the transformation is reported to be correct by Alive2.

--passes=gvn --disable-undef-input

----------------------------------------
define i1 @fun0(i8 %val0, i8 %val1) {
#0:
  %val2 = and i8 %val0, 1
  %val3 = icmp eq i8 %val2, 0
  %val4 = add i8 %val1, %val2
  %val5 = icmp eq i8 %val1, %val4
  %val6 = or i1 %val3, %val5
  ret i1 %val6
}
=>
define i1 @fun0(i8 %val0, i8 %val1) {
#0:
  %val2 = and i8 %val0, 1
  %val4 = add i8 %val1, %val2
  %val5 = icmp eq i8 %val1, %val4
  ret i1 %val5
}
Transformation seems to be correct!

Summary:
  1 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors