llvm dev - Mar 2020 - Passing undefined values as arguments transformed into constants

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200301/888a1789/attachment.html>

Using an uninitialized variable is undefined behavior, the compiler is
allowed assume that it does not happen. Since In your example program
happens anyway, since there is no code in the compiler handling
undefined behavior cases, the result is unpredictable.

In this case the variable x has the value 'undef'. It's semantics is
that LLVM can chose an arbitrary value, whatever is most convenient.
There is no specific reason why it selected '0' for one comparison but
'1' for another.

Michael


Am Sa., 29. Feb. 2020 um 22:01 Uhr schrieb Akash Banerjee via llvm-dev
<llvm-dev at lists.llvm.org>:
>
> 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.
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev