Test Failure: Transforms/StructurizeCFG/loop-break-phi.ll

Test source: git

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/StructurizeCFG/loop-break-phi.ll
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. StructurizeCFGPass

----------------------------------------
define float @while_break(i32 %z, float %v, i32 %x, i32 %y) {
entry:
  br label %header

header:
  %v.1 = phi float [ %v, %entry ], [ %v.2, %latch ]
  %ind = phi i32 [ 0, %entry ], [ %ind.inc, %latch ]
  %cc = icmp slt i32 %ind, %x
  br i1 %cc, label %if, label %else

if:
  %v.if = fadd float %v.1, 1.000000
  br label %latch

else:
  %cc2 = icmp slt i32 %ind, %y
  br i1 %cc2, label %latch, label %end

latch:
  %v.2 = phi float [ %v.if, %if ], [ %v.1, %else ]
  %ind.inc = add i32 %ind, 1
  %cc3 = icmp slt i32 %ind, %z
  br i1 %cc3, label %end, label %header

end:
  %r = phi float [ %v.2, %latch ], [ %v.1, %else ]
  ret float %r
}
Transformation seems to be correct! (syntactically equal)

-- 3. StructurizeCFGPass

----------------------------------------
define float @while_break(i32 %z, float %v, i32 %x, i32 %y) {
entry:
  br label %header

header:
  %v.1 = phi float [ %v, %entry ], [ %v.2, %latch ]
  %ind = phi i32 [ 0, %entry ], [ %ind.inc, %latch ]
  %cc = icmp slt i32 %ind, %x
  br i1 %cc, label %if, label %else

if:
  %v.if = fadd float %v.1, 1.000000
  br label %latch

else:
  %cc2 = icmp slt i32 %ind, %y
  br i1 %cc2, label %latch, label %end

latch:
  %v.2 = phi float [ %v.if, %if ], [ %v.1, %else ]
  %ind.inc = add i32 %ind, 1
  %cc3 = icmp slt i32 %ind, %z
  br i1 %cc3, label %end, label %header

end:
  %r = phi float [ %v.2, %latch ], [ %v.1, %else ]
  ret float %r
}
=>
define float @while_break(i32 %z, float %v, i32 %x, i32 %y) {
entry:
  br label %header

header:
  %v.1 = phi float [ %v, %entry ], [ %#7, %Flow2 ]
  %ind = phi i32 [ 0, %entry ], [ %#6, %Flow2 ]
  %cc = icmp sge i32 %ind, %x
  br i1 %cc, label %else, label %Flow

else:
  %cc2 = icmp slt i32 %ind, %y
  br label %Flow

Flow:
  %#0 = phi float [ %v.1, %else ], [ undef, %header ]
  %#1 = phi i1 [ %cc2, %else ], [ 0, %header ]
  %#2 = phi i1 [ 0, %else ], [ 1, %header ]
  br i1 %#2, label %if, label %Flow1

if:
  %v.if = fadd float %v.1, 1.000000
  br label %Flow1

Flow1:
  %#3 = phi float [ undef, %if ], [ %#0, %Flow ]
  %#4 = phi float [ %v.if, %if ], [ %#0, %Flow ]
  %#5 = phi i1 [ 1, %if ], [ %#1, %Flow ]
  br i1 %#5, label %latch, label %Flow2

latch:
  %ind.inc = add i32 %ind, 1
  %cc3 = icmp slt i32 %ind, %z
  br label %Flow2

Flow2:
  %#6 = phi i32 [ %ind.inc, %latch ], [ undef, %Flow1 ]
  %#7 = phi float [ %#4, %latch ], [ undef, %Flow1 ]
  %#8 = phi float [ %#4, %latch ], [ %#3, %Flow1 ]
  %#9 = phi i1 [ %cc3, %latch ], [ 1, %Flow1 ]
  br i1 %#9, label %end, label %header

end:
  ret float %#8
}
Transformation doesn't verify! (unsound)
ERROR: Value mismatch

Example:
i32 %z = #x00000004 (4)
float %v = undef
i32 %x = #x00000002 (2)
i32 %y = #x00000000 (0)

Source:
  >> Jump to %header
float %v.1 = #x00000000 (+0.0)
i32 %ind = #x00000000 (0)
i1 %cc = #x1 (1)
  >> Jump to %if
float %v.if = #x3f800000 (1)
  >> Jump to %latch
float %v.2 = #x3f800000 (1)	[based on undef value]
i32 %ind.inc = #x00000001 (1)
i1 %cc3 = #x1 (1)
  >> Jump to %end
float %r = #x3f800000 (1)	[based on undef value]

Target:
  >> Jump to %header
float %v.1 = #x00000000 (+0.0)	[based on undef value]
i32 %ind = #x00000000 (0)
i1 %cc = #x0 (0)
  >> Jump to %Flow
float %#0 = #x00000000 (+0.0)	[based on undef value]
i1 %#1 = #x0 (0)
i1 %#2 = #x1 (1)
  >> Jump to %if
float %v.if = #x7f800040 (SNaN)
  >> Jump to %Flow1
float %#3 = #x00000000 (+0.0)
float %#4 = #x3f800000 (1)	[based on undef value]
i1 %#5 = #x1 (1)
  >> Jump to %latch
i32 %ind.inc = #x00000001 (1)
i1 %cc3 = #x1 (1)
  >> Jump to %Flow2
i32 %#6 = #x00000001 (1)
float %#7 = #x3f800000 (1)
float %#8 = #x7fa00000 (SNaN)
i1 %#9 = #x1 (1)
  >> Jump to %end
Source value: #x3f800000 (1)
Target value: #x7fa00000 (SNaN)

Pass: StructurizeCFGPass
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=structurizecfg' '/bitbucket/nlopes/llvm/llvm/test/Transforms/StructurizeCFG/loop-break-phi.ll' '-o' '-' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/loop-break-phi_VFhYCM9x_LMT1.bc"


------------------- SMT STATS -------------------
Num queries: 40
Num invalid: 0
Num skips:   0
Num trivial: 31 (43.7%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     28 (70.0%)
Num UNSAT:   12 (30.0%)
Alive2: Transform doesn't verify; aborting!

stderr:

RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh -S -passes='structurizecfg' /bitbucket/nlopes/llvm/llvm/test/Transforms/StructurizeCFG/loop-break-phi.ll -o - | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/StructurizeCFG/loop-break-phi.ll
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/StructurizeCFG/loop-break-phi.ll
+ /home/nlopes/alive2/build/opt-alive.sh -S -passes=structurizecfg /bitbucket/nlopes/llvm/llvm/test/Transforms/StructurizeCFG/loop-break-phi.ll -o -

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/StructurizeCFG/loop-break-phi.ll

NOTE: This test would pass if undef didn't exist!

<-- Back