[llvm-dev] Possibly incorrect transformation

[Akash Banerjee via llvm-dev]

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>