Test Failure: Transforms/LoopVectorize/X86/propagate-metadata.ll

Test source: git

Comments: Bug in IR semantics or optimization: escapes noescape pointer

Log:

Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. LoopVectorizePass

----------------------------------------
define void @no_propagate_range_metadata(ptr nowrite %first.coerce, ptr noread nowrite %last.coerce, ptr nocapture %result) {
for.body.preheader:
  br label %for.body

for.body:
  %result.addr.05 = phi ptr [ %incdec.ptr, %for.body ], [ nocapture %result, %for.body.preheader ]
  %first.sroa.0.04 = phi ptr [ %incdec.ptr.i.i.i, %for.body ], [ nowrite %first.coerce, %for.body.preheader ]
  %#0 = load i8, ptr %first.sroa.0.04, align 1
  %#0_range = !range i8 %#0, i8 0, i8 2
  store i8 %#0_range, ptr %result.addr.05, align 1
  %incdec.ptr.i.i.i = gep inbounds ptr %first.sroa.0.04, 1 x i64 1
  %incdec.ptr = gep inbounds ptr %result.addr.05, 1 x i64 1
  %lnot.i = icmp eq ptr %incdec.ptr.i.i.i, noread nowrite %last.coerce
  br i1 %lnot.i, label %for.end.loopexit, label %for.body

for.end.loopexit:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 3. LoopVectorizePass

----------------------------------------
define void @no_propagate_range_metadata(ptr nowrite %first.coerce, ptr noread nowrite %last.coerce, ptr nocapture %result) {
for.body.preheader:
  br label %for.body

for.body:
  %result.addr.05 = phi ptr [ %incdec.ptr, %for.body ], [ nocapture %result, %for.body.preheader ]
  %first.sroa.0.04 = phi ptr [ %incdec.ptr.i.i.i, %for.body ], [ nowrite %first.coerce, %for.body.preheader ]
  %#0 = load i8, ptr %first.sroa.0.04, align 1
  %#0_range = !range i8 %#0, i8 0, i8 2
  store i8 %#0_range, ptr %result.addr.05, align 1
  %incdec.ptr.i.i.i = gep inbounds ptr %first.sroa.0.04, 1 x i64 1
  %incdec.ptr = gep inbounds ptr %result.addr.05, 1 x i64 1
  %lnot.i = icmp eq ptr %incdec.ptr.i.i.i, noread nowrite %last.coerce
  br i1 %lnot.i, label %for.end.loopexit, label %for.body

for.end.loopexit:
  ret void
}
=>
define void @no_propagate_range_metadata(ptr nowrite %first.coerce, ptr noread nowrite %last.coerce, ptr nocapture %result) {
iter.check:
  %first.coerce4 = ptrtoint ptr nowrite %first.coerce to i64
  %last.coerce3 = ptrtoint ptr noread nowrite %last.coerce to i64
  %first.coerce2 = ptrtoint ptr nowrite %first.coerce to i64
  %result1 = ptrtoint ptr nocapture %result to i64
  %#0 = sub i64 %last.coerce3, %first.coerce4
  %min.iters.check = icmp ult i64 %#0, 8
  br i1 %min.iters.check, label %vec.epilog.scalar.ph, label %vector.memcheck

vector.memcheck:
  %#1 = sub i64 %result1, %first.coerce2
  %diff.check = icmp ult i64 %#1, 32
  br i1 %diff.check, label %vec.epilog.scalar.ph, label %vector.main.loop.iter.check

vector.main.loop.iter.check:
  %min.iters.check5 = icmp ult i64 %#0, 32
  br i1 %min.iters.check5, label %vec.epilog.ph, label %vector.ph

vector.ph:
  %n.mod.vf = urem i64 %#0, 32
  %n.vec = sub i64 %#0, %n.mod.vf
  br label %vector.body

vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %#2 = add i64 %index, 0
  %next.gep = gep ptr nocapture %result, 1 x i64 %#2
  %#4 = add i64 %index, 0
  %next.gep7 = gep ptr nowrite %first.coerce, 1 x i64 %#4
  %#6 = gep ptr %next.gep7, 1 x i32 0
  %#7 = gep ptr %next.gep7, 1 x i32 16
  %wide.load = load <16 x i8>, ptr %#6, align 1
  %wide.load9 = load <16 x i8>, ptr %#7, align 1
  %#8 = gep ptr %next.gep, 1 x i32 0
  %#9 = gep ptr %next.gep, 1 x i32 16
  store <16 x i8> %wide.load, ptr %#8, align 1
  store <16 x i8> %wide.load9, ptr %#9, align 1
  %index.next = add nuw i64 %index, 32
  %#10 = icmp eq i64 %index.next, %n.vec
  br i1 %#10, label %middle.block, label %vector.body

middle.block:
  %cmp.n = icmp eq i64 %#0, %n.vec
  br i1 %cmp.n, label %for.end.loopexit, label %vec.epilog.iter.check

vec.epilog.iter.check:
  %ind.end14 = gep ptr nowrite %first.coerce, 1 x i64 %n.vec
  %ind.end12 = gep ptr nocapture %result, 1 x i64 %n.vec
  %n.vec.remaining = sub i64 %#0, %n.vec
  %min.epilog.iters.check = icmp ult i64 %n.vec.remaining, 8
  br i1 %min.epilog.iters.check, label %vec.epilog.scalar.ph, label %vec.epilog.ph

vec.epilog.ph:
  %vec.epilog.resume.val = phi i64 [ %n.vec, %vec.epilog.iter.check ], [ 0, %vector.main.loop.iter.check ]
  %n.mod.vf10 = urem i64 %#0, 8
  %n.vec11 = sub i64 %#0, %n.mod.vf10
  %ind.end = gep ptr nocapture %result, 1 x i64 %n.vec11
  %ind.end13 = gep ptr nowrite %first.coerce, 1 x i64 %n.vec11
  br label %vec.epilog.vector.body

vec.epilog.vector.body:
  %index17 = phi i64 [ %vec.epilog.resume.val, %vec.epilog.ph ], [ %index.next21, %vec.epilog.vector.body ]
  %#11 = add i64 %index17, 0
  %next.gep18 = gep ptr nocapture %result, 1 x i64 %#11
  %#12 = add i64 %index17, 0
  %next.gep19 = gep ptr nowrite %first.coerce, 1 x i64 %#12
  %#13 = gep ptr %next.gep19, 1 x i32 0
  %wide.load20 = load <8 x i8>, ptr %#13, align 1
  %#14 = gep ptr %next.gep18, 1 x i32 0
  store <8 x i8> %wide.load20, ptr %#14, align 1
  %index.next21 = add nuw i64 %index17, 8
  %#15 = icmp eq i64 %index.next21, %n.vec11
  br i1 %#15, label %vec.epilog.middle.block, label %vec.epilog.vector.body

vec.epilog.middle.block:
  %cmp.n16 = icmp eq i64 %#0, %n.vec11
  br i1 %cmp.n16, label %for.end.loopexit, label %vec.epilog.scalar.ph

vec.epilog.scalar.ph:
  %bc.resume.val = phi ptr [ %ind.end, %vec.epilog.middle.block ], [ %ind.end12, %vec.epilog.iter.check ], [ nocapture %result, %vector.memcheck ], [ nocapture %result, %iter.check ]
  %bc.resume.val15 = phi ptr [ %ind.end13, %vec.epilog.middle.block ], [ %ind.end14, %vec.epilog.iter.check ], [ nowrite %first.coerce, %vector.memcheck ], [ nowrite %first.coerce, %iter.check ]
  br label %for.body

for.body:
  %result.addr.05 = phi ptr [ %incdec.ptr, %for.body ], [ %bc.resume.val, %vec.epilog.scalar.ph ]
  %first.sroa.0.04 = phi ptr [ %incdec.ptr.i.i.i, %for.body ], [ %bc.resume.val15, %vec.epilog.scalar.ph ]
  %#16 = load i8, ptr %first.sroa.0.04, align 1
  %#16_range = !range i8 %#16, i8 0, i8 2
  store i8 %#16_range, ptr %result.addr.05, align 1
  %incdec.ptr.i.i.i = gep inbounds ptr %first.sroa.0.04, 1 x i64 1
  %incdec.ptr = gep inbounds ptr %result.addr.05, 1 x i64 1
  %lnot.i = icmp eq ptr %incdec.ptr.i.i.i, noread nowrite %last.coerce
  br i1 %lnot.i, label %for.end.loopexit, label %for.body

for.end.loopexit:
  ret void
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
ptr nowrite %first.coerce = pointer(non-local, block_id=1, offset=0, attrs=4)
ptr noread nowrite %last.coerce = pointer(non-local, block_id=0, offset=8, attrs=6)
ptr nocapture %result = pointer(non-local, block_id=2, offset=1, attrs=1)

Source:
  >> Jump to %for.body
ptr %result.addr.05 = pointer(non-local, block_id=2, offset=1, attrs=1)
ptr %first.sroa.0.04 = pointer(non-local, block_id=1, offset=0, attrs=4)
i8 %#0 = poison
i8 %#0_range = poison
ptr %incdec.ptr.i.i.i = pointer(non-local, block_id=1, offset=1, attrs=4)
ptr %incdec.ptr = pointer(non-local, block_id=2, offset=2, attrs=1)
i1 %lnot.i = #x1 (1)
  >> Jump to %for.end.loopexit

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0	alive: false	address: 0
Block 1 >	size: 1	align: 1	alloc type: 0	alive: true	address: 7
Block 2 >	size: 2	align: 1	alloc type: 0	alive: true	address: 13
Block 3 >	size: 5	align: 1	alloc type: 0	alive: true	address: 8

Target:
i64 %first.coerce4 = #x0000000000000007 (7)
i64 %last.coerce3 = #x0000000000000008 (8)
i64 %first.coerce2 = #x0000000000000007 (7)
i64 %result1 = UB triggered!


Pass: LoopVectorizePass
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' '-mtriple=x86_64-unknown-linux-gnu' '-passes=loop-vectorize' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_Ofgkh6uv_QpVt.bc"


------------------- SMT STATS -------------------
Num queries: 40
Num invalid: 0
Num skips:   0
Num trivial: 11 (21.6%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     27 (67.5%)
Num UNSAT:   13 (32.5%)
Alive2: Transform doesn't verify; aborting!

stderr:

RUN: at line 1: /home/nlopes/alive2/build/opt-alive.sh -S -mtriple="x86_64-unknown-linux-gnu" -passes=loop-vectorize < /bitbucket/nlopes/llvm/llvm/test/Transforms/LoopVectorize/X86/propagate-metadata.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LoopVectorize/X86/propagate-metadata.ll
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LoopVectorize/X86/propagate-metadata.ll
+ /home/nlopes/alive2/build/opt-alive.sh -S -mtriple=x86_64-unknown-linux-gnu -passes=loop-vectorize

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LoopVectorize/X86/propagate-metadata.ll

 

<-- Back