False negative for function with loop, only fails with sufficiently large unroll factor.

[fhahn]

Alive2 verifies the example below (nsw added to %iv.next in %loop) as correct without any unrolling options and with --disable-undef-input -tgt-unroll=1 -src-unroll=1. It fails to verify with --disable-undef-input -tgt-unroll=2 -src-unroll=2.

The current behavior might give a false sense of security to the user, as it appears as if Alive2 can successfully verify the function, even though it is incorrect.

Perhaps there's a way to better communicate the restrictions around loops to the user?

• --disable-undef-input unexpectedly verifies as correct https://alive2.llvm.org/ce/z/56VVYj
• --disable-undef-input -tgt-unroll=1 -src-unroll=1 unexpectedly verifies as correct https://alive2.llvm.org/ce/z/Wg7B8a
• --disable-undef-input -tgt-unroll=2 -src-unroll=2 fails as expected https://alive2.llvm.org/ce/z/2kR5JJ

  
  define void @src(i4 %a, i4 %b, i4 %c, i4* %ptr, i4 %n) {
  entry:
  %u = urem i4 %n, 4
  %cc = icmp eq i4 %u, 0
  br i1 %cc, label %loop, label %exit

loop: %iv = phi i4 [ 0, %entry ], [ %iv.next, %loop ] %gep = getelementptr i4, i4 %ptr, i4 %iv store i4 0, i4 %gep %iv.next = add i4 %iv, 4 %ec = icmp eq i4 %iv.next, %n br i1 %ec, label %exit, label %loop

exit: ret void }

define void @tgt(i4 %a, i4 %b, i4 %c, i4* %ptr, i4 %n) { entry: %u = urem i4 %n, 4 %cc = icmp eq i4 %u, 0 br i1 %cc, label %loop, label %exit

loop: %iv = phi i4 [ 0, %entry ], [ %iv.next, %loop ] %gep = getelementptr i4, i4 %ptr, i4 %iv store i4 0, i4 %gep %iv.next = add nsw i4 %iv, 4 %ec = icmp eq i4 %iv.next, %n br i1 %ec, label %exit, label %loop

exit: ret void }

[nunoplopes]

Not sure what to do in the short term.. Most loops require unroll of at least 2 for any decent coverage: 1 iteration for the initial phi edge, and another for the phi backedge value. But if you have vectorization you'll need more. We have thoughts on a longer-term solution, but it won't happen this year for sure.

For the short-term, maybe issue a warning when we detect a BB or phi entry that hasn't been covered? That shouldn't be too hard for static coverage (famous last words..). A full coverage detection isn't cheap as we would need to ask the theorem prover to do it for us.

[fhahn]

I see, thanks! A warning certainly sounds very helpful :)