[llvm-dev] Possibly incorrect transformation

[Kaylor, Andrew via llvm-dev]

Hi Akash,

This isn’t well-documented in most references, but the C99 and C11 standards say that you can only modify the floating point environment (as fesetround does) when access to the environment is enabled by #pragma STDC FENV_ACCESS ON. Some compilers provide other ways to control this, but the basic idea is that unless you’ve told the compiler that you’re changing the environment the compiler is free to assume the default environment. This fact is mentioned here (https://en.cppreference.com/w/c/numeric/fenv) but not in the corresponding documentation for fesetround.

Support for this is a work-in-progress in clang. Currently, you can enable fenv access using the “-ffp-model=strict” option. The -frounding-math option also works correctly now, but this was only recently enabled.

If you use one of these options, we will generate a call to llvm.experimental.constrained.rint for the code you cited and this will not get constant folded.

-Andy

From: llvm-dev <llvm-dev-bounces at lists.llvm.org> On Behalf Of Akash Banerjee via llvm-dev
Sent: Thursday, January 30, 2020 3:43 AM
To: llvm-dev <llvm-dev at lists.llvm.org>
Subject: [llvm-dev] Possibly incorrect transformation

Hi,
Please consider the following C code snippet taken from the latest SVComp(Software Verification) Benchmark:
#include <fenv.h>
#include <math.h>
int main(void) {
fesetround(FE_DOWNWARD);
assert(rint(12.9) == 12.);
assert(rint(-12.1) == -13.);
return 0;
}
The above code is marked as SAFE by the svcomp benchmark, ie, the assert can never fail.
The corresponding LLVM-IR for the above code is:
define dso_local i32 @main() #0 {
entry:
  %retval = alloca i32, align 4
  store i32 0, i32* %retval, align 4
  %call = call i32 @fesetround(i32 1024) #4
  %0 = call double @llvm.rint.f64(double 1.290000e+01)
  %cmp = fcmp oeq double %0, 1.200000e+01
  %conv = zext i1 %cmp to i32
  %call1 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 %conv)
  %1 = call double @llvm.rint.f64(double -1.210000e+01)
  %cmp2 = fcmp oeq double %1, -1.300000e+01
  %conv3 = zext i1 %cmp2 to i32
  %call4 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 %conv3)
  ret i32 0
},
however on applying the -ipsccp -dce, optimization passes, the transformed IR is:
define dso_local i32 @main() #0 {
entry:
  %retval = alloca i32, align 4
  store i32 0, i32* %retval, align 4
  %call = call i32 @fesetround(i32 1024) #4
  %call1 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 0)
  %call4 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 0)
  ret i32 0
}
, where the assert calls have been made false.

Thanks,
Akash.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20200130/f2a06436/attachment-0001.html>