Open
Description
With 9cd7c53 InstCombine is able to fold select into binary floating point operation operands. For example the following code:
%C = fadd %A, %B
%D = select %cond, %C, %A
is transformed into:
%C = select %cond, %B, -0.000000e+00
%D = fadd %A, %C
From the commit message there were Alive2 verification links -- which at the time were timing out:
- FAdd - https://alive2.llvm.org/ce/z/eUxN4Y
- FMul - https://alive2.llvm.org/ce/z/5SWZz4
- FSub - https://alive2.llvm.org/ce/z/Dhj8dU
- FDiv - https://alive2.llvm.org/ce/z/Yj_NA2
However today they report the transformation seems not semantic preserving in the cases of NaNs -- e.g.
----------------------------------------
define half @src(i1 %cond, half %A, half %B) {
#0:
%C = fsub half %A, %B
%D = select i1 %cond, half %C, half %A
ret half %D
}
=>
define half @tgt(i1 %cond, half %A, half %B) {
#0:
%C = select i1 %cond, half %B, half 0x0000
%D = fsub half %A, %C
ret half %D
}
Transformation doesn't verify!
ERROR: Value mismatch
Example:
i1 %cond = #x0 (0)
half %A = #xfc80 (SNaN)
half %B = #x0000 (+0.0)
Source:
half %C = #x7e00 (QNaN)
half %D = #xfc80 (SNaN)
Target:
half %C = #x0000 (+0.0)
half %D = #x7c80 (SNaN)
Source value: #xfc80 (SNaN)
Target value: #x7c80 (SNaN)
The counter example reported above suggests that the transformation is not sound w.r.t. NaNs.
It is not clear to me if according to https://llvm.org/docs/LangRef.html#behavior-of-floating-point-nan-values select is considered a floating point operation or not, hence I wonder if the transformation should be allowed only when nnan is being on the select instruction.
@spatel @huihzhang any comment?