Test source: git
Comments: LLVM PR57523
Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. IRCEPass
----------------------------------------
define void @test_01() {
%entry:
br label %loop
%loop:
%iv = phi i64 [ 380, %entry ], [ %limit, %guarded ]
%bad_phi = phi i32 [ 3, %entry ], [ %bad_phi.next, %guarded ]
%bad_phi.next = add nsw nuw i32 %bad_phi, 1
%iv.next = add nsw nuw i64 %iv, 1
%rc = icmp slt i64 %iv.next, 5
br i1 %rc, label %guarded, label %exit
%guarded:
%limit = add nsw i64 %iv, -1
%tmp5 = add nsw nuw i32 %bad_phi, 8
%tmp6 = zext i32 %tmp5 to i64
%tmp7 = icmp eq i64 %limit, %tmp6
br i1 %tmp7, label %exit, label %loop
%exit:
ret void
}
Transformation seems to be correct! (syntactically equal)
-- 3. IRCEPass
----------------------------------------
define void @test_01() {
%entry:
br label %loop
%loop:
%iv = phi i64 [ 380, %entry ], [ %limit, %guarded ]
%bad_phi = phi i32 [ 3, %entry ], [ %bad_phi.next, %guarded ]
%bad_phi.next = add nsw nuw i32 %bad_phi, 1
%iv.next = add nsw nuw i64 %iv, 1
%rc = icmp slt i64 %iv.next, 5
br i1 %rc, label %guarded, label %exit
%guarded:
%limit = add nsw i64 %iv, -1
%tmp5 = add nsw nuw i32 %bad_phi, 8
%tmp6 = zext i32 %tmp5 to i64
%tmp7 = icmp eq i64 %limit, %tmp6
br i1 %tmp7, label %exit, label %loop
%exit:
ret void
}
Transformation seems to be correct! (syntactically equal)
-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. IRCEPass
----------------------------------------
define void @test_02(ptr %p1, ptr %p2, i1 %maybe_exit) {
%entry:
%num = load i64, ptr %p1, align 4
%range_l#0%num = icmp sge i64 %num, 0
%range_h#0%num = icmp slt i64 %num, 100
%range#0%num = and i1 %range_l#0%num, %range_h#0%num
assume_non_poison i1 %range#0%num
%denom = load i64, ptr %p2, align 4
%range_l#0%denom = icmp sge i64 %denom, 0
%range_h#0%denom = icmp slt i64 %denom, 100
%range#0%denom = and i1 %range_l#0%denom, %range_h#0%denom
assume_non_poison i1 %range#0%denom
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %guarded ]
%iv.next = add nsw nuw i64 %iv, 1
br i1 %maybe_exit, label %range_check, label %exit
%range_check:
%div_result = udiv i64 %num, %denom
%rc = icmp slt i64 %iv.next, %div_result
br i1 %rc, label %guarded, label %exit
%guarded:
%gep = gep ptr %p1, 8 x i64 %iv.next
%loaded = load i64, ptr %gep, align 4
%tmp7 = icmp slt i64 %iv.next, 1000
br i1 %tmp7, label %loop, label %exit
%exit:
ret void
}
Transformation seems to be correct! (syntactically equal)
-- 7. IRCEPass
----------------------------------------
define void @test_02(ptr %p1, ptr %p2, i1 %maybe_exit) {
%entry:
%num = load i64, ptr %p1, align 4
%range_l#0%num = icmp sge i64 %num, 0
%range_h#0%num = icmp slt i64 %num, 100
%range#0%num = and i1 %range_l#0%num, %range_h#0%num
assume_non_poison i1 %range#0%num
%denom = load i64, ptr %p2, align 4
%range_l#0%denom = icmp sge i64 %denom, 0
%range_h#0%denom = icmp slt i64 %denom, 100
%range#0%denom = and i1 %range_l#0%denom, %range_h#0%denom
assume_non_poison i1 %range#0%denom
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %guarded ]
%iv.next = add nsw nuw i64 %iv, 1
br i1 %maybe_exit, label %range_check, label %exit
%range_check:
%div_result = udiv i64 %num, %denom
%rc = icmp slt i64 %iv.next, %div_result
br i1 %rc, label %guarded, label %exit
%guarded:
%gep = gep ptr %p1, 8 x i64 %iv.next
%loaded = load i64, ptr %gep, align 4
%tmp7 = icmp slt i64 %iv.next, 1000
br i1 %tmp7, label %loop, label %exit
%exit:
ret void
}
Transformation seems to be correct! (syntactically equal)
-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. IRCEPass
----------------------------------------
define void @test_03(ptr %p1, ptr %p2, i1 %maybe_exit) {
%entry:
%num = load i64, ptr %p1, align 4
%range_l#0%num = icmp sge i64 %num, 0
%range_h#0%num = icmp slt i64 %num, 100
%range#0%num = and i1 %range_l#0%num, %range_h#0%num
assume_non_poison i1 %range#0%num
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %guarded ]
%iv.next = add nsw nuw i64 %iv, 1
br i1 %maybe_exit, label %range_check, label %exit
%range_check:
%div_result = udiv i64 %num, 13
%rc = icmp slt i64 %iv.next, %div_result
br i1 %rc, label %guarded, label %exit
%guarded:
%gep = gep ptr %p1, 8 x i64 %iv.next
%loaded = load i64, ptr %gep, align 4
%tmp7 = icmp slt i64 %iv.next, 1000
br i1 %tmp7, label %loop, label %exit
%exit:
ret void
}
Transformation seems to be correct! (syntactically equal)
-- 11. IRCEPass
----------------------------------------
define void @test_03(ptr %p1, ptr %p2, i1 %maybe_exit) {
%entry:
%num = load i64, ptr %p1, align 4
%range_l#0%num = icmp sge i64 %num, 0
%range_h#0%num = icmp slt i64 %num, 100
%range#0%num = and i1 %range_l#0%num, %range_h#0%num
assume_non_poison i1 %range#0%num
br label %loop
%loop:
%iv = phi i64 [ 0, %entry ], [ %iv.next, %guarded ]
%iv.next = add nsw nuw i64 %iv, 1
br i1 %maybe_exit, label %range_check, label %exit
%range_check:
%div_result = udiv i64 %num, 13
%rc = icmp slt i64 %iv.next, %div_result
br i1 %rc, label %guarded, label %exit
%guarded:
%gep = gep ptr %p1, 8 x i64 %iv.next
%loaded = load i64, ptr %gep, align 4
%tmp7 = icmp slt i64 %iv.next, 1000
br i1 %tmp7, label %loop, label %exit
%exit:
ret void
}
=>
define void @test_03(ptr %p1, ptr %p2, i1 %maybe_exit) {
%entry:
%num = load i64, ptr %p1, align 4
%range_l#0%num = icmp sge i64 %num, 0
%range_h#0%num = icmp slt i64 %num, 100
%range#0%num = and i1 %range_l#0%num, %range_h#0%num
assume_non_poison i1 %range#0%num
%div_result = udiv i64 %num, 13
%0 = add nsw i64 %div_result, -1
%exit.mainloop.at = smax i64 %0, 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, %guarded ], [ 0, %loop.preheader ]
%iv.next = add nsw nuw i64 %iv, 1
%or.cond = select i1 %maybe_exit, i1 1, i1 0
br i1 %or.cond, label %guarded, label %exit.loopexit1
%guarded:
%gep = gep ptr %p1, 8 x i64 %iv.next
%loaded = load i64, ptr %gep, align 4
%2 = icmp slt i64 %iv.next, %exit.mainloop.at
br i1 %2, label %loop, label %main.exit.selector
%main.exit.selector:
%iv.next.lcssa = phi i64 [ %iv.next, %guarded ]
%3 = icmp slt i64 %iv.next.lcssa, 1000
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 ], [ %iv.next.lcssa, %main.exit.selector ]
br label %postloop
%postloop:
br label %loop.postloop
%loop.postloop:
%iv.postloop = phi i64 [ %iv.copy, %postloop ], [ %iv.next.postloop, %guarded.postloop ]
%iv.next.postloop = add nsw nuw i64 %iv.postloop, 1
%rc.postloop = icmp slt i64 %iv.next.postloop, %div_result
%or.cond.postloop = select i1 %maybe_exit, i1 %rc.postloop, i1 0
br i1 %or.cond.postloop, label %guarded.postloop, label %exit.loopexit
%guarded.postloop:
%gep.postloop = gep ptr %p1, 8 x i64 %iv.next.postloop
%loaded.postloop = load i64, ptr %gep.postloop, align 4
%tmp7.postloop = icmp slt i64 %iv.next.postloop, 1000
br i1 %tmp7.postloop, label %loop.postloop, label %exit.loopexit
%exit.loopexit:
br label %exit
%exit.loopexit1:
br label %exit
%exit:
ret void
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target
Example:
ptr %p1 = pointer(non-local, block_id=1, offset=4)
ptr %p2 = poison
i1 %maybe_exit = #x0 (0)
Source:
i64 %num = poison
i1 %range_l#0%num = poison
i1 %range_h#0%num = poison
i1 %range#0%num = poison
>> Jump to %loop
i64 %iv = #x0000000000000000 (0)
i64 %iv.next = #x0000000000000001 (1)
>> Jump to %exit
SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 > size: 0 align: 4 alloc type: 0
Block 1 > size: 1152921504606846976 align: 4294967296 alloc type: 0
Block 2 > align: 1048576 alloc type: 0
Target:
i64 %num = poison
i1 %range_l#0%num = poison
i1 %range_h#0%num = poison
i1 %range#0%num = poison
i64 %div_result = poison
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' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
------------------- SMT STATS -------------------
Num queries: 5
Num invalid: 0
Num skips: 0
Num trivial: 4 (44.4%)
Num timeout: 0 (0.0%)
Num errors: 0 (0.0%)
Num SAT: 5 (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 -S
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/bad_expander.ll
/bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/bad_expander.ll:18:16: error: CHECK-LABEL: expected string not found in input
; CHECK-LABEL: test_01
^
<stdin>:1:44: note: scanning from here
irce: in function test_03: constrained Loop at depth 1 containing: %loop<header><exiting>,%guarded<latch><exiting>
^
<stdin>:1:48: note: possible intended match here
irce: in function test_03: constrained Loop at depth 1 containing: %loop<header><exiting>,%guarded<latch><exiting>
^
Input file: <stdin>
Check file: /bitbucket/nlopes/llvm/llvm/test/Transforms/IRCE/bad_expander.ll
-dump-input=help explains the following input dump.
Input was:
<<<<<<
1: irce: in function test_03: constrained Loop at depth 1 containing: %loop<header><exiting>,%guarded<latch><exiting>
label:18'0 X~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ error: no match found
label:18'1 ? possible intended match
2:
label:18'0 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>>>>>>