[llvm-dev] Passing undefined values as arguments transformed into constants (original) (raw)

Akash Banerjee via llvm-dev llvm-dev at lists.llvm.org
Sat Feb 29 19:59:56 PST 2020

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>

More information about the llvm-dev mailing list