llvm dev - Jan 2020 - 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/62006909/attachment.html>

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>