llvm / llvm/llvm-project

[InstCombine] Wrong fold of `fabs` with `nsz`

Open
#217,505 0 comments 0 reactions 0 assignees View on GitHub
confirmed llvm:instcombine miscompilation
Dominant language
LLVM
Stars
40.5k
Forks
18.7k
PR merge metrics
PR metrics pending

Description

_Opening a new issue for this because https://github.com/llvm/llvm-project/issues/214312 is owned by my NVIDIA account, which is temporarily deactivated._

`fabs nsz -0.0` is sometimes folded to `-0.0` which is no longer sound since https://github.com/llvm/llvm-project/pull/180906. This was fixed for `float`, `double`, and `half`, but still miscompiles with `fp128`, `bfloat`, `x86_fp80`, and `ppc_fp128`. Local Alive2 proof:
```
$ ./build/alive-tv -passes=instcombine temp/nsz.ll

----------------------------------------
define bfloat @f() {
#0:
%#1 = fabs nsz bfloat 0x8000
ret bfloat %#1
}
=>
define bfloat @f() {
#0:
ret bfloat 0x8000
}
Transformation doesn't verify!

ERROR: Value mismatch

NOTE: The counterexample is unique.

Example:

Source:
bfloat %#1 = #x0000 (+0.0)

Target:
Source value: #x0000 (+0.0)
Target value: #x8000 (-0.0)
```

@GabrielWu2004 is already working on this as a first PR. See https://github.com/llvm/llvm-project/pull/216232.

Contributor guide

Open the contributing guide

Research direction

Start in the InstCombine area and reproduce the issue with the provided Alive2 command using temp/nsz.ll. Check the existing handling for float, double, and half against fp128, bfloat, x86_fp80, and ppc_fp128. Done means the listed cases no longer produce the unsound fold and the Alive2 transformation verifies.

Written by the indexing model from the issue text.

Assessment

Domain
compilers
Issue type
Bug
Difficulty
3/5
Estimated time
1-2 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
20/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.