AliveToolkit
False negative for function with loop, only fails with sufficiently large unroll factor.
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-inputunexpectedly verifies as correct https://alive2.llvm.org/ce/z/56VVYj -
--disable-undef-input -tgt-unroll=1 -src-unroll=1unexpectedly verifies as correct https://alive2.llvm.org/ce/z/Wg7B8a -
--disable-undef-input -tgt-unroll=2 -src-unroll=2fails 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
}
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.
