[PATCH] D143106: [SDAG] fix miscompiles caused by using ValueTracking matchSelectPattern to create FMINIMUM/FMAXIMUM

[Sanjay Patel via Phabricator via llvm-commits]

spatel added a comment.

In D143106#4106570 <https://reviews.llvm.org/D143106#4106570>, @uabelho wrote:

> Hi,
>
> Would the rewrite be legal if the fcmp was "fast" or would that also lead to miscompiles?
> So e.g. if we have
>
>   %cmp = fcmp fast ogt float %a, %b
>   %cond = select i1 %cmp, float %a, float %b
>
> ?

To make this transform sound, the inputs must be neither -0.0 nor NaN. But "nsz" doesn't guarantee that - it just means the sign of zero is "insignificant". That is already implied by the definition of fcmp, so "nsz" on fcmp is redundant/meaningless - "nsz" needs to be on the select. We have the opposite problem with "nnan" on the select. By definition, the select filters out a possible poison value (NaN), so a "nnan" on the select doesn't give us the required pre-condition that neither input is NaN.

That's why we have this strange proof:
https://alive2.llvm.org/ce/z/vjV9AC


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D143106/new/

https://reviews.llvm.org/D143106