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.