AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
769 stars 97 forks source link

The counterexample given by alive2 is incorrect #995

Closed dtcxzyw closed 9 months ago

dtcxzyw commented 9 months ago

Alive2: https://alive2.llvm.org/ce/z/iqr-nS

----------------------------------------
define float @src(float %a) {
#0:
  %max = fmax float %a, 0.000000
  %fabs = fabs float %max
  ret float %fabs
}
=>
define float @tgt(float %a) {
#0:
  %max = fmax float %a, 0.000000
  ret float %max
}
Transformation doesn't verify!

ERROR: Target's return value is more undefined

Example:
float %a = #x00000000 (+0.0)

Source:
float %max = #x80000000 (-0.0)
float %fabs = #x00000000 (+0.0)

Target:
float %max = #x00000000 (+0.0)
Source value: #x00000000 (+0.0)
Target value: #x00000000 (+0.0)

It should be:

Example:
float %a = #x80000000 (-0.0)

Source:
float %max = #x80000000 (-0.0)
float %fabs = #x00000000 (+0.0)

Target:
float %max = #x80000000 (-0.0)
Source value: #x00000000 (0.0)
Target value: #x80000000 (-0.0)

See also https://llvm.org/docs/LangRef.html#llvm-maxnum-intrinsic.

For example, this means that fmax(+0.0, -0.0) returns either -0.0 or 0.0.