llvm / llvm-project

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

[InstCombine] miscompilation #115454

Closed bongjunj closed 3 hours ago

bongjunj commented 4 hours ago

Alive2 report: https://alive2.llvm.org/ce/z/ym5WV-

----------------------------------------
define i32 @abs_abs_x18.2(i32 %x, i32 %y) {
#0:
  %a = sub nsw i32 %x, %y
  %b = sub nsw nuw i32 %y, %x
  %cmp = icmp sgt i32 %x, 4294967295
  %cond = select i1 %cmp, i32 %a, i32 %b
  %sub16 = sub nsw i32 0, %cond
  ret i32 %sub16
}
=>
define i32 @abs_abs_x18.2(i32 %x, i32 %y) {
#0:
  %a = sub nsw i32 %x, %y
  %b = sub nsw nuw i32 %y, %x
  %cmp1 = icmp slt i32 %x, 0
  %#1 = select i1 %cmp1, i32 %a, i32 %b
  ret i32 %#1
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
i32 %x = #x0000000d (13)
i32 %y = #x00000000 (0)

Source:
i32 %a = #x0000000d (13)
i32 %b = poison
i1 %cmp = #x1 (1)
i32 %cond = #x0000000d (13)
i32 %sub16 = #xfffffff3 (4294967283, -13)

Target:
i32 %a = #x0000000d (13)
i32 %b = poison
i1 %cmp1 = #x0 (0)
i32 %#1 = poison
Source value: #xfffffff3 (4294967283, -13)
Target value: poison

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

Fixed by https://github.com/llvm/llvm-project/pull/112893.

----------------------------------------
define i32 @abs_abs_x18(i32 %x, i32 %y) {
#0:
  %a = sub nsw i32 %x, %y
  %b = sub nsw nuw i32 %y, %x
  %cmp = icmp sgt i32 %x, 4294967295
  %cond = select i1 %cmp, i32 %a, i32 %b
  %sub16 = sub nsw i32 0, %cond
  ret i32 %sub16
}
=>
define i32 @abs_abs_x18(i32 %x, i32 %y) {
#0:
  %a = sub i32 %x, %y
  %b = sub i32 %y, %x
  %cmp1 = icmp slt i32 %x, 0
  %#1 = select i1 %cmp1, i32 %a, i32 %b
  ret i32 %#1
}
Transformation seems to be correct!

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