llvm / llvm/llvm-project

[InstCombine] Moving freeze before fdiv makes the result more undefined

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

Description

InstCombine moves a `freeze` from the result of a floating-point division to its operand while simplifying a vector operation:

```llvm
freeze (fdiv %a, 3.0)
```

is effectively transformed into:

```llvm
fdiv (freeze %a), 3.0
```

When `%a` is poison, The operand freeze may choose an SNaN. A subsequent ordinary
floating-point operation may produce a NaN whose sign is nondeterministic and whose quiet bit and payload are nondeterministically selected according to LLVM's NaN propagation
rules.

As a result, the transformed expression may introduce new NaN-related nondeterminism after the original value has been frozen.

Alive2 also reports that this transformation is invalid because the target return value is more undefined.

### Reproducer

```llvm
define <2 x float> @test_fdiv(float %a, float %b, i1 %cmp) {
%splatinsert = insertelement <2 x float> poison, float %a, i32 0
%denom = insertelement <2 x float> , float 1.000000e+00, i32 1
%t1 = fdiv <2 x float> %splatinsert, %denom
%freeze.ins = freeze <2 x float> %t1
%splat.op = shufflevector <2 x float> %freeze.ins, <2 x float> poison, <2 x i32>
br i1 %cmp, label %sel.true, label %sel.false

sel.true: ; preds = %0
br label %sel.merge

sel.false: ; preds = %0
br label %sel.merge

sel.merge: ; preds = %sel.false, %sel.true
%sel.phi = phi <2 x float> [ , %sel.true ], [ %splat.op, %sel.false ]
ret <2 x float> %sel.phi
}
```

The optimized result (by `opt 22.1`):

```llvm
define <2 x float> @test_fdiv(float %a, float %b, i1 %cmp) local_unnamed_addr #0 {
sel.merge:
%splatinsert = insertelement <2 x float> poison, float %a, i64 0
%splatinsert.fr = freeze <2 x float> %splatinsert
%t1 = fdiv <2 x float> %splatinsert.fr,
%splat.op = shufflevector <2 x float> %t1, <2 x float> poison, <2 x i32>
%.splat.op = select i1 %cmp, <2 x float> , <2 x float> %splat.op
ret <2 x float> %.splat.op
}

attributes #0 = { mustprogress nofree norecurse nosync nounwind willreturn memory(none) }
```

### Alive2 result

The online alive2 fails to reproduce it since it timed out. Attaching alive2 result of local machine

```
----------------------------------------
define <2 x float> @test_fdiv(float %a, float %b, i1 %cmp) {
#0:
%splatinsert = insertelement <2 x float> poison, float %a, i32 0
%denom = insertelement <2 x float> { 3.000000, undef }, float 1.000000, i32 1
%t1 = fdiv <2 x float> %splatinsert, %denom
%freeze.ins = freeze <2 x float> %t1
%splat.op = shufflevector <2 x float> %freeze.ins, <2 x float> poison, 4294967295, 0
br i1 %cmp, label %sel.true, label %sel.false

sel.false:
br label %sel.merge

sel.true:
br label %sel.merge

sel.merge:
%sel.phi = phi <2 x float> [ { 77.000000, 99.000000 }, %sel.true ], [ %splat.op, %sel.false ]
ret <2 x float> %sel.phi
}
=>
define <2 x float> @test_fdiv(float %a, float %b, i1 %cmp) nofree willreturn memory(none) {
sel.merge:
%splatinsert = insertelement <2 x float> poison, float %a, i64 0
%splatinsert.fr = freeze <2 x float> %splatinsert
%t1 = fdiv <2 x float> %splatinsert.fr, { 3.000000, poison }
%splat.op = shufflevector <2 x float> %t1, <2 x float> poison, 4294967295, 0
%.splat.op = select i1 %cmp, <2 x float> { 77.000000, 99.000000 }, <2 x float> %splat.op
ret <2 x float> %.splat.op
}
Transformation doesn't verify!

ERROR: Target's return value is more undefined

Example:
float %a = poison
float %b = poison
i1 %cmp = #x0 (0)

Source:
<2 x float> %splatinsert = < poison, poison >
<2 x float> %denom = < #x40400000 (3), #x3f800000 (1) >
<2 x float> %t1 = < poison, poison >
<2 x float> %freeze.ins = < #x00000003 (0.000000000000?), #x00000003 (0.000000000000?) >
<2 x float> %splat.op = < poison, #x00000003 (0.000000000000?) >
>> Jump to %sel.false
>> Jump to %sel.merge
<2 x float> %sel.phi = < poison, #x00000003 (0.000000000000?) >

Target:
<2 x float> %splatinsert = < poison, poison >
<2 x float> %splatinsert.fr = < #xff800004 (SNaN), #x00000000 (+0.0) >
<2 x float> %t1 = < #x7f800004 (SNaN), poison >
<2 x float> %splat.op = < poison, #x7f800004 (SNaN) >
<2 x float> %.splat.op = < poison, #x7f800004 (SNaN) >
Source value: < poison, #x00000003 (0.000000000000?) >
Target value: < poison, #x7f800004 (SNaN) >

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

Contributor guide

Open the contributing guide

Research direction

Start in the InstCombine implementation responsible for moving freeze across floating-point division, and reproduce the issue with the supplied LLVM IR using opt 22.1. Use the local Alive2 counterexample to guide a regression test; done means this transformation no longer produces a more-undefined return value for the reproducer.

Written by the indexing model from the issue text.

Assessment

Domain
compilers
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Active
Clarity
Mostly clear
Newbie friendliness
45/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.