Hi All,
Can someone please explain why the following transformations are safe to do?
Say we have the following C code:
int main(){
int x;
assume(x>=0);
assert(x<=-1);
assume(x==1);
assert(x!=1);
}
The corresponding IR with -O0 is:
define dso_local i32 @main() #0 {
%1 = alloca i32, align 4
%2 = load i32, i32* %1, align 4
%3 = icmp sge i32 %2, 0
%4 = zext i1 %3 to i32
%5 = call i32 (i32, …) bitcast (i32 (…)* @CPROVER_assume to i32 (i32, …))(i32 %4)
__%6 = load i32, i32 %1, align 4
%7 = icmp sle i32 %6, -1
%8 = zext i1 %7 to i32
%9 = call i32 (i32, …) bitcast (i32 (…)* @assert to i32 (i32, …)*)(i32 %8)
%10 = load i32, i32* %1, align 4
%11 = icmp eq i32 %10, 1
%12 = zext i1 %11 to i32
%13 = call i32 (i32, …) bitcast (i32 (…)* @CPROVER_assume to i32 (i32, …))(i32 %12)
__%14 = load i32, i32 %1, align 4
%15 = icmp ne i32 %14, 1
%16 = zext i1 %15 to i32
%17 = call i32 (i32, …) bitcast (i32 (…)* @assert to i32 (i32, …)*)(i32 %16)
ret i32 0
}
However, if you run -O1 on this IR we are left with the following:
define dso_local i32 @main() local_unnamed_addr #0 {
%1 = call i32 (i32, …) bitcast (i32 (…)* @CPROVER_assume to i32 (i32, …))(i32 1) #2
__%2 = call i32 (i32, …) bitcast (i32 (…) @assert to i32 (i32, …)*)(i32 1) #2
%3 = call i32 (i32, …) bitcast (i32 (…)* @CPROVER_assume to i32 (i32, …))(i32 0) #2
__%4 = call i32 (i32, …) bitcast (i32 (…) @assert to i32 (i32, …)*)(i32 0) #2
ret i32 0
}
Is there any particular reason why assert(x<=1) is taken as true while assert(x!=1) is taken as false?
Thanks,
Akash.