Open
Description
In simplify case, the function retruns %sel5 > @umin(undef, 1), which always produces true before optimization.
After optimization, it produces undef which can be either of 0 or 1.
The miscompilation seems to happen in instcombine too, but I am not sure at the moment.
Alive2 report: https://alive2.llvm.org/ce/z/nHEYp4
; instsimplify
----------------------------------------
define i1 @potential_test14.2(i1 %c0, i1 %c2, i1 %c3) {
#0:
%shl1 = shl nsw i1 %c3, 0
%sel1 = select i1 %c2, i1 %shl1, i1 %c3
%sel2 = select i1 %sel1, i32 0, i32 1
%sel3 = select i1 %c0, i32 %sel2, i32 undef
%sel4 = select i1 %c2, i32 0, i32 7
%max = umax i32 3, %sel4
%sel5 = select i1 %c3, i32 %sel3, i32 %max
%min = umin i32 %sel3, 1
%cmp1 = icmp ugt i32 %sel5, %min
ret i1 %cmp1
}
=>
define i1 @potential_test14.2(i1 %c0, i1 %c2, i1 %c3) {
#0:
%sel2 = select i1 %c3, i32 0, i32 1
%sel3 = select i1 %c0, i32 %sel2, i32 undef
%sel4 = select i1 %c2, i32 0, i32 7
%max = umax i32 3, %sel4
%sel5 = select i1 %c3, i32 %sel3, i32 %max
%cmp1 = icmp ugt i32 %sel5, %sel3
ret i1 %cmp1
}
Transformation doesn't verify!
ERROR: Target's return value is more undefined
Example:
i1 %c0 = #x0 (0)
i1 %c2 = #x1 (1)
i1 %c3 = #x0 (0)
Source:
i1 %shl1 = #x0 (0)
i1 %sel1 = #x0 (0)
i32 %sel2 = #x00000001 (1)
i32 %sel3 = #x00000000 (0) [based on undef value]
i32 %sel4 = #x00000000 (0)
i32 %max = #x00000003 (3)
i32 %sel5 = #x00000003 (3)
i32 %min = #x00000000 (0) [based on undef value]
i1 %cmp1 = #x1 (1)
Target:
i32 %sel2 = #x00000001 (1)
i32 %sel3 = #x00000000 (0) [based on undef value]
i32 %sel4 = #x00000000 (0)
i32 %max = #x00000003 (3)
i32 %sel5 = #x00000003 (3)
i1 %cmp1 = #x1 (1)
Source value: #x1 (1)
Target value: #x1 (1)
Summary:
0 correct transformations
1 incorrect transformations
0 failed-to-prove transformations
0 Alive2 errors; instcombine
----------------------------------------
define i1 @potential_test14.2(i1 %c0, i1 %c2, i1 %c3) {
#0:
%shl1 = shl nsw i1 %c3, 0
%sel1 = select i1 %c2, i1 %shl1, i1 %c3
%sel2 = select i1 %sel1, i32 0, i32 1
%sel3 = select i1 %c0, i32 %sel2, i32 undef
%sel4 = select i1 %c2, i32 0, i32 7
%max = umax i32 3, %sel4
%sel5 = select i1 %c3, i32 %sel3, i32 %max
%min = umin i32 %sel3, 1
%cmp1 = icmp ugt i32 %sel5, %min
ret i1 %cmp1
}
=>
define i1 @potential_test14.2(i1 %c0, i1 %c2, i1 %c3) {
#0:
%not.c3 = xor i1 %c3, 1
%cmp1 = select i1 %not.c3, i1 %c0, i1 0
ret i1 %cmp1
}
Transformation doesn't verify!
ERROR: Value mismatch
Example:
i1 %c0 = #x0 (0)
i1 %c2 = #x0 (0)
i1 %c3 = #x0 (0)
Source:
i1 %shl1 = #x0 (0)
i1 %sel1 = #x0 (0)
i32 %sel2 = #x00000001 (1)
i32 %sel3 = #x00000000 (0) [based on undef value]
i32 %sel4 = #x00000007 (7)
i32 %max = #x00000007 (7)
i32 %sel5 = #x00000007 (7)
i32 %min = #x00000000 (0) [based on undef value]
i1 %cmp1 = #x1 (1)
Target:
i1 %not.c3 = #x1 (1)
i1 %cmp1 = #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