Test source: git
Comments: LLVM PR57523
Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. IRCEPass
----------------------------------------
define i32 @test_01(i32 %A, i64 %Len, ptr %array) {
preheader:
%tripcheck = icmp sgt i64 %Len, 2
br i1 %tripcheck, label %loop, label %zero
loop:
%indvar = phi i64 [ 1, %preheader ], [ %indvar.next, %latch ]
%#0 = icmp ult i64 %indvar, %Len
br i1 %#0, label %guarded, label %deopt
guarded:
%addr = gep inbounds ptr %array, 4 x i64 %indvar
%res = load i32, ptr %addr, align 4
%cmp = icmp eq i32 %res, 0
br i1 %cmp, label %zero, label %latch
zero:
ret i32 0
latch:
%indvar.next = add nsw nuw i64 %indvar, 2
%res2 = mul i32 %res, 3
%#1 = zext i32 %A to i64
%cmp2 = icmp ugt i64 %indvar.next, %#1
br i1 %cmp2, label %loopexit, label %loop
loopexit:
ret i32 %res2
deopt:
ret i32 1
}
Transformation seems to be correct! (syntactically equal)
-- 3. IRCEPass
----------------------------------------
define i32 @test_01(i32 %A, i64 %Len, ptr %array) {
preheader:
%tripcheck = icmp sgt i64 %Len, 2
br i1 %tripcheck, label %loop, label %zero
loop:
%indvar = phi i64 [ 1, %preheader ], [ %indvar.next, %latch ]
%#0 = icmp ult i64 %indvar, %Len
br i1 %#0, label %guarded, label %deopt
guarded:
%addr = gep inbounds ptr %array, 4 x i64 %indvar
%res = load i32, ptr %addr, align 4
%cmp = icmp eq i32 %res, 0
br i1 %cmp, label %zero, label %latch
zero:
ret i32 0
latch:
%indvar.next = add nsw nuw i64 %indvar, 2
%res2 = mul i32 %res, 3
%#1 = zext i32 %A to i64
%cmp2 = icmp ugt i64 %indvar.next, %#1
br i1 %cmp2, label %loopexit, label %loop
loopexit:
ret i32 %res2
deopt:
ret i32 1
}
=>
define i32 @test_01(i32 %A, i64 %Len, ptr %array) {
preheader:
%tripcheck = icmp sgt i64 %Len, 2
br i1 %tripcheck, label %loop.preheader, label %zero
loop.preheader:
%#0 = zext i32 %A to i64
%#1 = add nsw nuw i64 %#0, 1
%smin = smin i64 %Len, 0
%#2 = sub i64 %Len, %smin
%umin = umin i64 %#2, %#1
%exit.mainloop.at = umax i64 %umin, 1
%#3 = icmp ult i64 1, %exit.mainloop.at
br i1 %#3, label %loop.preheader2, label %main.pseudo.exit
loop.preheader2:
br label %loop
loop:
%indvar = phi i64 [ %indvar.next, %latch ], [ 1, %loop.preheader2 ]
br i1 1, label %guarded, label %deopt.loopexit3
guarded:
%addr = gep inbounds ptr %array, 4 x i64 %indvar
%res = load i32, ptr %addr, align 4
%cmp = icmp ne i32 %res, 0
br i1 %cmp, label %latch, label %zero.loopexit.loopexit4
latch:
%indvar.next = add nsw nuw i64 %indvar, 2
%res2 = mul i32 %res, 3
%#6 = icmp ult i64 %indvar.next, %exit.mainloop.at
%#7 = xor i1 %#6, 1
br i1 %#7, label %main.exit.selector, label %loop
main.exit.selector:
%indvar.next.lcssa = phi i64 [ %indvar.next, %latch ]
%res2.lcssa1 = phi i32 [ %res2, %latch ]
%#8 = icmp ult i64 %indvar.next.lcssa, %#1
br i1 %#8, label %main.pseudo.exit, label %loopexit
zero.loopexit.loopexit4:
br label %zero.loopexit
deopt.loopexit3:
br label %deopt
main.pseudo.exit:
%indvar.copy = phi i64 [ 1, %loop.preheader ], [ %indvar.next.lcssa, %main.exit.selector ]
br label %postloop
postloop:
br label %loop.postloop
loop.postloop:
%indvar.postloop = phi i64 [ %indvar.next.postloop, %latch.postloop ], [ %indvar.copy, %postloop ]
%#9 = icmp ult i64 %indvar.postloop, %Len
br i1 %#9, label %guarded.postloop, label %deopt.loopexit
guarded.postloop:
%addr.postloop = gep inbounds ptr %array, 4 x i64 %indvar.postloop
%res.postloop = load i32, ptr %addr.postloop, align 4
%cmp.postloop = icmp ne i32 %res.postloop, 0
br i1 %cmp.postloop, label %latch.postloop, label %zero.loopexit.loopexit
latch.postloop:
%indvar.next.postloop = add nsw nuw i64 %indvar.postloop, 2
%res2.postloop = mul i32 %res.postloop, 3
%#10 = zext i32 %A to i64
%cmp2.postloop = icmp ugt i64 %indvar.next.postloop, %#10
br i1 %cmp2.postloop, label %loopexit.loopexit, label %loop.postloop
loopexit.loopexit:
%res2.lcssa.ph = phi i32 [ %res2.postloop, %latch.postloop ]
br label %loopexit
loopexit:
%res2.lcssa = phi i32 [ %res2.lcssa1, %main.exit.selector ], [ %res2.lcssa.ph, %loopexit.loopexit ]
ret i32 %res2.lcssa
zero.loopexit.loopexit:
br label %zero.loopexit
zero.loopexit:
br label %zero
zero:
ret i32 0
deopt.loopexit:
br label %deopt
deopt:
ret i32 1
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target
Example:
i32 %A = poison
i64 %Len = #x0000000000000003 (3)
ptr %array = pointer(non-local, block_id=1, offset=0) / Address=#x0000000000000004
Source:
i1 %tripcheck = #x1 (1)
>> Jump to %loop
i64 %indvar = #x0000000000000001 (1)
i1 %#0 = #x1 (1)
>> Jump to %guarded
ptr %addr = pointer(non-local, block_id=1, offset=4) / Address=#x0000000000000008
i32 %res = #x00000000 (0)
i1 %cmp = #x1 (1)
>> Jump to %zero
SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 > size: 0 align: 4 alloc type: 0 alive: false address: 0
Block 1 > size: 8 align: 1 alloc type: 0 alive: true address: 4
Contents:
*: #x00000000
Target:
i1 %tripcheck = #x1 (1)
>> Jump to %loop.preheader
i64 %#0 = poison
i64 %#1 = poison
i64 %smin = #x0000000000000000 (0)
i64 %#2 = #x0000000000000003 (3)
i64 %umin = poison
i64 %exit.mainloop.at = poison
i1 %#3 = poison
UB triggered on br
Pass: IRCEPass
Command line: '/home/nlopes/llvm/build/bin/opt' '-load=/home/nlopes/alive2/build/tv/tv.so' '-load-pass-plugin=/home/nlopes/alive2/build/tv/tv.so' '-tv-exit-on-error' '-S' '-passes=irce,verify' '-verify-loop-info' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_VMcDE78u_Q2eH.bc"
------------------- SMT STATS -------------------
Num queries: 37
Num invalid: 0
Num skips: 0
Num trivial: 11 (22.9%)
Num timeout: 0 (0.0%)
Num errors: 0 (0.0%)
Num SAT: 29 (78.4%)
Num UNSAT: 8 (21.6%)
Alive2: Transform doesn't verify; aborting!
RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh -S -passes=irce,verify -verify-loop-info < /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/non-loop-invariant-rhs-instr.ll 2>&1 | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/non-loop-invariant-rhs-instr.ll
+ /home/nlopes/alive2/build/opt-alive.sh -S -passes=irce,verify -verify-loop-info
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/non-loop-invariant-rhs-instr.ll
/bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/non-loop-invariant-rhs-instr.ll:6:16: error: CHECK-LABEL: expected string not found in input
; CHECK-LABEL: @test_01(
^
<stdin>:1:1: note: scanning from here
^
<stdin>:1:11: note: possible intended match here
^
Input file: <stdin>
Check file: /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/non-loop-invariant-rhs-instr.ll
-dump-input=help explains the following input dump.
Input was:
<<<<<<
1:
label:6'0 X~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ error: no match found
label:6'1 ? possible intended match
>>>>>>