[llvm-dev] Passing undefined values as arguments transformed into constants

[Akash Banerjee via llvm-dev]

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>