Test source: git
Comments: LLVM PR57523
Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. IRCEPass
----------------------------------------
define i32 @test_increasing_slt_slt_wide_simple_no_postloop() {
%entry:
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %backedge ]
%rc = icmp slt i64 %iv, 100
br i1 %rc, label %backedge, label %check_failed
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%latch.cond = icmp slt i32 %narrow.iv, 100
br i1 %latch.cond, label %loop, label %exit
%exit:
ret i32 %narrow.iv
%check_failed:
ret i32 4294967295
}
Transformation seems to be correct! (syntactically equal)
-- 3. IRCEPass
----------------------------------------
define i32 @test_increasing_slt_slt_wide_simple_no_postloop() {
%entry:
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %backedge ]
%rc = icmp slt i64 %iv, 100
br i1 %rc, label %backedge, label %check_failed
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%latch.cond = icmp slt i32 %narrow.iv, 100
br i1 %latch.cond, label %loop, label %exit
%exit:
ret i32 %narrow.iv
%check_failed:
ret i32 4294967295
}
=>
define i32 @test_increasing_slt_slt_wide_simple_no_postloop() {
%entry:
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %backedge ]
br i1 1, label %backedge, label %check_failed
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%latch.cond = icmp slt i32 %narrow.iv, 100
br i1 %latch.cond, label %loop, label %exit
%exit:
%narrow.iv.lcssa = phi i32 [ %narrow.iv, %backedge ]
ret i32 %narrow.iv.lcssa
%check_failed:
ret i32 4294967295
}
Transformation seems to be correct!
-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. IRCEPass
----------------------------------------
define i32 @test_increasing_slt_slt_wide_simple_postloop() {
%entry:
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %backedge ]
%rc = icmp slt i64 %iv, 99
br i1 %rc, label %backedge, label %check_failed
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%latch.cond = icmp slt i32 %narrow.iv, 100
br i1 %latch.cond, label %loop, label %exit
%exit:
ret i32 %narrow.iv
%check_failed:
ret i32 4294967295
}
Transformation seems to be correct! (syntactically equal)
-- 7. IRCEPass
----------------------------------------
define i32 @test_increasing_slt_slt_wide_simple_postloop() {
%entry:
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %backedge ]
%rc = icmp slt i64 %iv, 99
br i1 %rc, label %backedge, label %check_failed
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%latch.cond = icmp slt i32 %narrow.iv, 100
br i1 %latch.cond, label %loop, label %exit
%exit:
ret i32 %narrow.iv
%check_failed:
ret i32 4294967295
}
=>
define i32 @test_increasing_slt_slt_wide_simple_postloop() {
%entry:
br i1 1, label %loop.preheader, label %main.pseudo.exit
%loop.preheader:
br label %loop
%loop:
%iv = phi i64 [ %iv.next, %backedge ], [ 0, %loop.preheader ]
br i1 1, label %backedge, label %check_failed.loopexit2
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%wide.narrow.iv = sext i32 %narrow.iv to i64
%0 = icmp slt i64 %wide.narrow.iv, 99
br i1 %0, label %loop, label %main.exit.selector
%main.exit.selector:
%iv.next.lcssa = phi i64 [ %iv.next, %backedge ]
%narrow.iv.lcssa1 = phi i32 [ %narrow.iv, %backedge ]
%wide.narrow.iv.lcssa = phi i64 [ %wide.narrow.iv, %backedge ]
%1 = icmp slt i64 %wide.narrow.iv.lcssa, 100
br i1 %1, label %main.pseudo.exit, label %exit
%main.pseudo.exit:
%iv.copy = phi i64 [ 0, %entry ], [ %iv.next.lcssa, %main.exit.selector ]
%indvar.end = phi i64 [ 0, %entry ], [ %wide.narrow.iv.lcssa, %main.exit.selector ]
br label %postloop
%postloop:
br label %loop.postloop
%loop.postloop:
%iv.postloop = phi i64 [ %iv.copy, %postloop ], [ %iv.next.postloop, %backedge.postloop ]
%rc.postloop = icmp slt i64 %iv.postloop, 99
br i1 %rc.postloop, label %backedge.postloop, label %check_failed.loopexit
%backedge.postloop:
%iv.next.postloop = add i64 %iv.postloop, 1
%narrow.iv.postloop = trunc i64 %iv.next.postloop to i32
%latch.cond.postloop = icmp slt i32 %narrow.iv.postloop, 100
br i1 %latch.cond.postloop, label %loop.postloop, label %exit.loopexit
%exit.loopexit:
%narrow.iv.lcssa.ph = phi i32 [ %narrow.iv.postloop, %backedge.postloop ]
br label %exit
%check_failed.loopexit:
br label %check_failed
%exit:
%narrow.iv.lcssa = phi i32 [ %narrow.iv.lcssa1, %main.exit.selector ], [ %narrow.iv.lcssa.ph, %exit.loopexit ]
ret i32 %narrow.iv.lcssa
%check_failed.loopexit2:
br label %check_failed
%check_failed:
ret i32 4294967295
}
Transformation seems to be correct!
-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. IRCEPass
----------------------------------------
define i32 @test_increasing_slt_slt_wide_non-negative(ptr %n_ptr, ptr %m_ptr) {
%entry:
%N = load i32, ptr %n_ptr, align 4
%range_l#0%N = icmp sge i32 %N, 1
%range_h#0%N = icmp slt i32 %N, 2147483647
%range#0%N = and i1 %range_l#0%N, %range_h#0%N
assume_non_poison i1 %range#0%N
%M = load i64, ptr %m_ptr, align 4
%range_l#0%M = icmp sge i64 %M, 0
%range_h#0%M = icmp slt i64 %M, 9223372036854775807
%range#0%M = and i1 %range_l#0%M, %range_h#0%M
assume_non_poison i1 %range#0%M
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %backedge ]
%rc = icmp slt i64 %iv, %M
br i1 %rc, label %backedge, label %check_failed
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%latch.cond = icmp slt i32 %narrow.iv, %N
br i1 %latch.cond, label %loop, label %exit
%exit:
ret i32 %narrow.iv
%check_failed:
ret i32 4294967295
}
Transformation seems to be correct! (syntactically equal)
-- 11. IRCEPass
----------------------------------------
define i32 @test_increasing_slt_slt_wide_non-negative(ptr %n_ptr, ptr %m_ptr) {
%entry:
%N = load i32, ptr %n_ptr, align 4
%range_l#0%N = icmp sge i32 %N, 1
%range_h#0%N = icmp slt i32 %N, 2147483647
%range#0%N = and i1 %range_l#0%N, %range_h#0%N
assume_non_poison i1 %range#0%N
%M = load i64, ptr %m_ptr, align 4
%range_l#0%M = icmp sge i64 %M, 0
%range_h#0%M = icmp slt i64 %M, 9223372036854775807
%range#0%M = and i1 %range_l#0%M, %range_h#0%M
assume_non_poison i1 %range#0%M
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %backedge ]
%rc = icmp slt i64 %iv, %M
br i1 %rc, label %backedge, label %check_failed
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%latch.cond = icmp slt i32 %narrow.iv, %N
br i1 %latch.cond, label %loop, label %exit
%exit:
ret i32 %narrow.iv
%check_failed:
ret i32 4294967295
}
=>
define i32 @test_increasing_slt_slt_wide_non-negative(ptr %n_ptr, ptr %m_ptr) {
%entry:
%N = load i32, ptr %n_ptr, align 4
%range_l#0%N = icmp sge i32 %N, 1
%range_h#0%N = icmp slt i32 %N, 2147483647
%range#0%N = and i1 %range_l#0%N, %range_h#0%N
assume_non_poison i1 %range#0%N
%M = load i64, ptr %m_ptr, align 4
%range_l#0%M = icmp sge i64 %M, 0
%range_h#0%M = icmp slt i64 %M, 9223372036854775807
%range#0%M = and i1 %range_l#0%M, %range_h#0%M
assume_non_poison i1 %range#0%M
%0 = zext i32 %N to i64
%exit.mainloop.at = smin i64 %M, %0
%1 = icmp slt i64 0, %exit.mainloop.at
br i1 %1, label %loop.preheader, label %main.pseudo.exit
%loop.preheader:
br label %loop
%loop:
%iv = phi i64 [ %iv.next, %backedge ], [ 0, %loop.preheader ]
br i1 1, label %backedge, label %check_failed.loopexit2
%backedge:
%iv.next = add i64 %iv, 1
%narrow.iv = trunc i64 %iv.next to i32
%wide.narrow.iv = sext i32 %narrow.iv to i64
%2 = icmp slt i64 %wide.narrow.iv, %exit.mainloop.at
br i1 %2, label %loop, label %main.exit.selector
%main.exit.selector:
%iv.next.lcssa = phi i64 [ %iv.next, %backedge ]
%narrow.iv.lcssa1 = phi i32 [ %narrow.iv, %backedge ]
%wide.narrow.iv.lcssa = phi i64 [ %wide.narrow.iv, %backedge ]
%wide.N = sext i32 %N to i64
%3 = icmp slt i64 %wide.narrow.iv.lcssa, %wide.N
br i1 %3, label %main.pseudo.exit, label %exit
%main.pseudo.exit:
%iv.copy = phi i64 [ 0, %entry ], [ %iv.next.lcssa, %main.exit.selector ]
%indvar.end = phi i64 [ 0, %entry ], [ %wide.narrow.iv.lcssa, %main.exit.selector ]
br label %postloop
%postloop:
br label %loop.postloop
%loop.postloop:
%iv.postloop = phi i64 [ %iv.copy, %postloop ], [ %iv.next.postloop, %backedge.postloop ]
%rc.postloop = icmp slt i64 %iv.postloop, %M
br i1 %rc.postloop, label %backedge.postloop, label %check_failed.loopexit
%backedge.postloop:
%iv.next.postloop = add i64 %iv.postloop, 1
%narrow.iv.postloop = trunc i64 %iv.next.postloop to i32
%latch.cond.postloop = icmp slt i32 %narrow.iv.postloop, %N
br i1 %latch.cond.postloop, label %loop.postloop, label %exit.loopexit
%exit.loopexit:
%narrow.iv.lcssa.ph = phi i32 [ %narrow.iv.postloop, %backedge.postloop ]
br label %exit
%check_failed.loopexit:
br label %check_failed
%exit:
%narrow.iv.lcssa = phi i32 [ %narrow.iv.lcssa1, %main.exit.selector ], [ %narrow.iv.lcssa.ph, %exit.loopexit ]
ret i32 %narrow.iv.lcssa
%check_failed.loopexit2:
br label %check_failed
%check_failed:
ret i32 4294967295
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target
Example:
ptr %n_ptr = pointer(non-local, block_id=1, offset=60)
ptr %m_ptr = pointer(non-local, block_id=2, offset=56)
Source:
i32 %N = poison
i1 %range_l#0%N = poison
i1 %range_h#0%N = poison
i1 %range#0%N = poison
i64 %M = #x0000000000000000 (0)
i1 %range_l#0%M = #x1 (1)
i1 %range_h#0%M = #x1 (1)
i1 %range#0%M = #x1 (1)
>> Jump to %loop
i64 %iv = #x0000000000000000 (0)
i1 %rc = #x0 (0)
>> Jump to %check_failed
SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 > size: 0 align: 4 alloc type: 0
Block 1 > size: 128 align: 131072 alloc type: 0
Block 2 > size: 128 align: 256 alloc type: 0
Target:
i32 %N = poison
i1 %range_l#0%N = poison
i1 %range_h#0%N = poison
i1 %range#0%N = poison
i64 %M = #x0000000000000000 (0)
i1 %range_l#0%M = #x1 (1)
i1 %range_h#0%M = #x1 (1)
i1 %range#0%M = #x1 (1)
i64 %0 = poison
i64 %exit.mainloop.at = poison
i1 %1 = 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' '-verify-loop-info' '-irce-print-changed-loops' '-passes=irce' '-irce-allow-narrow-latch=true' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
------------------- SMT STATS -------------------
Num queries: 6
Num invalid: 0
Num skips: 0
Num trivial: 24 (80.0%)
Num timeout: 0 (0.0%)
Num errors: 0 (0.0%)
Num SAT: 6 (100.0%)
Num UNSAT: 0 (0.0%)
Alive2: Transform doesn't verify; aborting!
+ : 'RUN: at line 1'
+ /home/nlopes/alive2/build/opt-alive.sh -verify-loop-info -irce-print-changed-loops -passes=irce -irce-allow-narrow-latch=true -S
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/wide_indvar.ll
/bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/wide_indvar.ll:7:16: error: CHECK-LABEL: expected string not found in input
; CHECK-LABEL: @test_increasing_slt_slt_wide_simple_no_postloop(
^
<stdin>:1:1: note: scanning from here
irce: in function test_increasing_slt_slt_wide_simple_no_postloop: constrained Loop at depth 1 containing: %loop<header><exiting>,%backedge<latch><exiting>
^
<stdin>:1:17: note: possible intended match here
irce: in function test_increasing_slt_slt_wide_simple_no_postloop: constrained Loop at depth 1 containing: %loop<header><exiting>,%backedge<latch><exiting>
^
Input file: <stdin>
Check file: /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/wide_indvar.ll
-dump-input=help explains the following input dump.
Input was:
<<<<<<
1: irce: in function test_increasing_slt_slt_wide_simple_no_postloop: constrained Loop at depth 1 containing: %loop<header><exiting>,%backedge<latch><exiting>
label:7'0 X~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ error: no match found
label:7'1 ? possible intended match
2: irce: in function test_increasing_slt_slt_wide_simple_postloop: constrained Loop at depth 1 containing: %loop<header><exiting>,%backedge<latch><exiting>
label:7'0 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3: irce: in function test_increasing_slt_slt_wide_non-negative: constrained Loop at depth 1 containing: %loop<header><exiting>,%backedge<latch><exiting>
label:7'0 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4:
label:7'0 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>>>>>>