Test Failure: Transforms/LoopUnswitch/preserve-analyses.ll

Test source: git

Log:

Source: <stdin>

----------------------------------------
@delim1 = global 4 bytes, align 4
@delim2 = global 4 bytes, align 4

define i32 @ineqn(* %s, * %p) nowrite nofree {
%entry:
  %0 = load i32, * @delim1, align 4
  %1 = load i32, * @delim2, align 4
  br label %bb8.outer

%bb8.outer:
  %ineq.0.ph = phi i32 [ 0, %entry ], [ %ineq.0.ph.be, %bb8.outer.backedge ]
  %p_addr.0.ph = phi * [ %p, %entry ], [ %.lcssa2, %bb8.outer.backedge ]
  %2 = icmp eq i32 %ineq.0.ph, 1
  br label %bb8

%bb8:
  %p_addr.0 = phi * [ %p_addr.0.ph, %bb8.outer ], [ %7, %bb8.backedge ]
  %3 = load i8, * %p_addr.0, align 1
  %4 = sext i8 %3 to i32
  %5 = icmp eq i8 %3, 0
  br i1 %5, label %bb10, label %bb

%bb:
  %6 = icmp eq * %p_addr.0, %s
  br i1 %6, label %bb10, label %bb2

%bb10:
  %.0 = phi i32 [ %ineq.0.ph, %bb ], [ 0, %bb8 ]
  ret i32 %.0

%bb2:
  %7 = gep inbounds * %p_addr.0, 1 x i32 1
  switch i32 %ineq.0.ph, label %bb8.backedge [
    i32 0, label %bb3
    i32 1, label %bb6
  ]

%bb3:
  %8 = icmp eq i32 %4, %0
  br i1 %8, label %bb8.outer.loopexit, label %bb5

%bb8.outer.loopexit:
  %.lcssa = phi * [ %7, %bb3 ]
  br label %bb8.outer.backedge

%bb5:
  br i1 %2, label %bb6, label %bb8.backedge

%bb6:
  %9 = icmp eq i32 %4, %1
  br i1 %9, label %bb7, label %bb8.backedge

%bb7:
  %.lcssa1 = phi * [ %7, %bb6 ]
  br label %bb8.outer.backedge

%bb8.outer.backedge:
  %.lcssa2 = phi * [ %.lcssa1, %bb7 ], [ %.lcssa, %bb8.outer.loopexit ]
  %ineq.0.ph.be = phi i32 [ 0, %bb7 ], [ 1, %bb8.outer.loopexit ]
  br label %bb8.outer

%bb8.backedge:
  br label %bb8
}
=>
@delim1 = global 4 bytes, align 4
@delim2 = global 4 bytes, align 4

define i32 @ineqn(* %s, * %p) nowrite nofree {
%entry:
  %0 = load i32, * @delim1, align 4
  %1 = load i32, * @delim2, align 4
  br label %bb8.outer

%bb8.outer:
  %ineq.0.ph = phi i32 [ 0, %entry ], [ %ineq.0.ph.be, %bb8.outer.backedge ]
  %p_addr.0.ph = phi * [ %p, %entry ], [ %.lcssa2, %bb8.outer.backedge ]
  %2 = icmp eq i32 %ineq.0.ph, 1
  %3 = icmp eq i32 %ineq.0.ph, 0
  br i1 %3, label %bb8.outer.split.us, label %bb8.outer.bb8.outer.split_crit_edge

%bb8.outer.split.us:
  br i1 %2, label %bb8.outer.split.us.split.us, label %bb8.outer.split.us.bb8.outer.split.us.split_crit_edge

%bb8.outer.split.us.split.us:
  br label %bb8.us.us

%bb8.us.us:
  %p_addr.0.us.us = phi * [ %p_addr.0.ph, %bb8.outer.split.us.split.us ], [ %8, %bb8.backedge.us.us ]
  %4 = load i8, * %p_addr.0.us.us, align 1
  %5 = sext i8 %4 to i32
  %6 = icmp eq i8 %4, 0
  br i1 %6, label %bb10.us-lcssa.us.us-lcssa.us, label %bb.us.us

%bb.us.us:
  %7 = icmp eq * %p_addr.0.us.us, %s
  br i1 %7, label %bb10.us-lcssa.us.us-lcssa.us, label %bb2.us.us

%bb10.us-lcssa.us.us-lcssa.us:
  %.0.ph.us.ph.us = phi i32 [ %ineq.0.ph, %bb.us.us ], [ 0, %bb8.us.us ]
  br label %bb10.us-lcssa.us

%bb2.us.us:
  %8 = gep inbounds * %p_addr.0.us.us, 1 x i32 1
  switch i32 0, label %bb8.backedge.us.us [
    i32 0, label %bb3.us.us
    i32 1, label %bb6.us.us
  ]

%bb3.us.us:
  %9 = icmp eq i32 %5, %0
  br i1 %9, label %bb8.outer.loopexit.us-lcssa.us.us-lcssa.us, label %bb5.us.us

%bb8.outer.loopexit.us-lcssa.us.us-lcssa.us:
  %.lcssa.ph.us.ph.us = phi * [ %8, %bb3.us.us ]
  br label %bb8.outer.loopexit.us-lcssa.us

%bb5.us.us:
  br i1 1, label %bb6.us.us, label %bb8.backedge.us.us

%bb6.us.us:
  %10 = icmp eq i32 %5, %1
  br i1 %10, label %bb7.us-lcssa.us.us-lcssa.us, label %bb8.backedge.us.us

%bb7.us-lcssa.us.us-lcssa.us:
  %.lcssa1.ph.us.ph.us = phi * [ %8, %bb6.us.us ]
  br label %bb7.us-lcssa.us

%bb8.backedge.us.us:
  br label %bb8.us.us

%bb8.outer.split.us.bb8.outer.split.us.split_crit_edge:
  br label %bb8.outer.split.us.split

%bb8.outer.split.us.split:
  br label %bb8.us

%bb8.us:
  %p_addr.0.us = phi * [ %p_addr.0.ph, %bb8.outer.split.us.split ], [ %15, %bb8.backedge.us ]
  %11 = load i8, * %p_addr.0.us, align 1
  %12 = sext i8 %11 to i32
  %13 = icmp eq i8 %11, 0
  br i1 %13, label %bb10.us-lcssa.us.us-lcssa, label %bb.us

%bb.us:
  %14 = icmp eq * %p_addr.0.us, %s
  br i1 %14, label %bb10.us-lcssa.us.us-lcssa, label %bb2.us

%bb10.us-lcssa.us.us-lcssa:
  %.0.ph.us.ph = phi i32 [ %ineq.0.ph, %bb.us ], [ 0, %bb8.us ]
  br label %bb10.us-lcssa.us

%bb10.us-lcssa.us:
  %.0.ph.us = phi i32 [ %.0.ph.us.ph, %bb10.us-lcssa.us.us-lcssa ], [ %.0.ph.us.ph.us, %bb10.us-lcssa.us.us-lcssa.us ]
  br label %bb10

%bb2.us:
  %15 = gep inbounds * %p_addr.0.us, 1 x i32 1
  switch i32 0, label %bb8.backedge.us [
    i32 0, label %bb3.us
    i32 1, label %bb6.us
  ]

%bb3.us:
  %16 = icmp eq i32 %12, %0
  br i1 %16, label %bb8.outer.loopexit.us-lcssa.us.us-lcssa, label %bb5.us

%bb8.outer.loopexit.us-lcssa.us.us-lcssa:
  %.lcssa.ph.us.ph = phi * [ %15, %bb3.us ]
  br label %bb8.outer.loopexit.us-lcssa.us

%bb8.outer.loopexit.us-lcssa.us:
  %.lcssa.ph.us = phi * [ %.lcssa.ph.us.ph, %bb8.outer.loopexit.us-lcssa.us.us-lcssa ], [ %.lcssa.ph.us.ph.us, %bb8.outer.loopexit.us-lcssa.us.us-lcssa.us ]
  br label %bb8.outer.loopexit

%bb5.us:
  br i1 0, label %bb6.us, label %bb8.backedge.us

%bb6.us:
  %17 = icmp eq i32 %12, %1
  br i1 %17, label %bb7.us-lcssa.us.us-lcssa, label %bb8.backedge.us

%bb7.us-lcssa.us.us-lcssa:
  %.lcssa1.ph.us.ph = phi * [ %15, %bb6.us ]
  br label %bb7.us-lcssa.us

%bb7.us-lcssa.us:
  %.lcssa1.ph.us = phi * [ %.lcssa1.ph.us.ph, %bb7.us-lcssa.us.us-lcssa ], [ %.lcssa1.ph.us.ph.us, %bb7.us-lcssa.us.us-lcssa.us ]
  br label %bb7

%bb8.backedge.us:
  br label %bb8.us

%bb8.outer.bb8.outer.split_crit_edge:
  br label %bb8.outer.split

%bb8.outer.split:
  %18 = icmp eq i32 %ineq.0.ph, 1
  br i1 %18, label %bb8.outer.split.split.us, label %bb8.outer.split.bb8.outer.split.split_crit_edge

%bb8.outer.split.split.us:
  br label %bb8.us1

%bb8.us1:
  %p_addr.0.us2 = phi * [ %p_addr.0.ph, %bb8.outer.split.split.us ], [ %23, %bb8.backedge.us8 ]
  %19 = load i8, * %p_addr.0.us2, align 1
  %20 = sext i8 %19 to i32
  %21 = icmp eq i8 %19, 0
  br i1 %21, label %bb10.us-lcssa.us-lcssa.us, label %bb.us3

%bb.us3:
  %22 = icmp eq * %p_addr.0.us2, %s
  br i1 %22, label %bb10.us-lcssa.us-lcssa.us, label %bb2.us4

%bb10.us-lcssa.us-lcssa.us:
  %.0.ph.ph.us = phi i32 [ %ineq.0.ph, %bb.us3 ], [ 0, %bb8.us1 ]
  br label %bb10.us-lcssa

%bb2.us4:
  %23 = gep inbounds * %p_addr.0.us2, 1 x i32 1
  switch i32 1, label %bb8.backedge.us8 [
    i32 0, label %bb3.split.us
    i32 1, label %bb6.us7
  ]

%bb3.split.us:
  br i1 1, label %us-unreachable.us-lcssa.us, label %bb3.us5

%us-unreachable.us-lcssa.us:
  br label %us-unreachable

%bb3.us5:
  %24 = icmp eq i32 %20, %0
  br i1 %24, label %bb8.outer.loopexit.us-lcssa.us-lcssa.us, label %bb5.us6

%bb8.outer.loopexit.us-lcssa.us-lcssa.us:
  %.lcssa.ph.ph.us = phi * [ %23, %bb3.us5 ]
  br label %bb8.outer.loopexit.us-lcssa

%bb5.us6:
  br i1 %2, label %bb6.us7, label %bb8.backedge.us8

%bb6.us7:
  %25 = icmp eq i32 %20, %1
  br i1 %25, label %bb7.us-lcssa.us-lcssa.us, label %bb8.backedge.us8

%bb7.us-lcssa.us-lcssa.us:
  %.lcssa1.ph.ph.us = phi * [ %23, %bb6.us7 ]
  br label %bb7.us-lcssa

%bb8.backedge.us8:
  br label %bb8.us1

%bb8.outer.split.bb8.outer.split.split_crit_edge:
  br label %bb8.outer.split.split

%bb8.outer.split.split:
  br label %bb8

%bb8:
  %p_addr.0 = phi * [ %p_addr.0.ph, %bb8.outer.split.split ], [ %30, %bb8.backedge ]
  %26 = load i8, * %p_addr.0, align 1
  %27 = sext i8 %26 to i32
  %28 = icmp eq i8 %26, 0
  br i1 %28, label %bb10.us-lcssa.us-lcssa, label %bb

%bb:
  %29 = icmp eq * %p_addr.0, %s
  br i1 %29, label %bb10.us-lcssa.us-lcssa, label %bb2

%bb10.us-lcssa.us-lcssa:
  %.0.ph.ph = phi i32 [ %ineq.0.ph, %bb ], [ 0, %bb8 ]
  br label %bb10.us-lcssa

%bb10.us-lcssa:
  %.0.ph = phi i32 [ %.0.ph.ph, %bb10.us-lcssa.us-lcssa ], [ %.0.ph.ph.us, %bb10.us-lcssa.us-lcssa.us ]
  br label %bb10

%bb10:
  %.0 = phi i32 [ %.0.ph, %bb10.us-lcssa ], [ %.0.ph.us, %bb10.us-lcssa.us ]
  ret i32 %.0

%bb2:
  %30 = gep inbounds * %p_addr.0, 1 x i32 1
  switch i32 %ineq.0.ph, label %bb8.backedge [
    i32 0, label %bb3.split
    i32 1, label %bb2.bb6_crit_edge
  ]

%bb3.split:
  br i1 1, label %us-unreachable.us-lcssa, label %bb3

%us-unreachable.us-lcssa:
  br label %us-unreachable

%us-unreachable:
  assume i1 0

%bb3:
  %31 = icmp eq i32 %27, %0
  br i1 %31, label %bb8.outer.loopexit.us-lcssa.us-lcssa, label %bb5

%bb8.outer.loopexit.us-lcssa.us-lcssa:
  %.lcssa.ph.ph = phi * [ %30, %bb3 ]
  br label %bb8.outer.loopexit.us-lcssa

%bb8.outer.loopexit.us-lcssa:
  %.lcssa.ph = phi * [ %.lcssa.ph.ph, %bb8.outer.loopexit.us-lcssa.us-lcssa ], [ %.lcssa.ph.ph.us, %bb8.outer.loopexit.us-lcssa.us-lcssa.us ]
  br label %bb8.outer.loopexit

%bb8.outer.loopexit:
  %.lcssa = phi * [ %.lcssa.ph, %bb8.outer.loopexit.us-lcssa ], [ %.lcssa.ph.us, %bb8.outer.loopexit.us-lcssa.us ]
  br label %bb8.outer.backedge

%bb5:
  br i1 %2, label %bb6, label %bb8.backedge

%bb2.bb6_crit_edge:
  br i1 1, label %us-unreachable9, label %bb6

%us-unreachable9:
  assume i1 0

%bb6:
  %32 = icmp eq i32 %27, %1
  br i1 %32, label %bb7.us-lcssa.us-lcssa, label %bb8.backedge

%bb7.us-lcssa.us-lcssa:
  %.lcssa1.ph.ph = phi * [ %30, %bb6 ]
  br label %bb7.us-lcssa

%bb7.us-lcssa:
  %.lcssa1.ph = phi * [ %.lcssa1.ph.ph, %bb7.us-lcssa.us-lcssa ], [ %.lcssa1.ph.ph.us, %bb7.us-lcssa.us-lcssa.us ]
  br label %bb7

%bb7:
  %.lcssa1 = phi * [ %.lcssa1.ph, %bb7.us-lcssa ], [ %.lcssa1.ph.us, %bb7.us-lcssa.us ]
  br label %bb8.outer.backedge

%bb8.outer.backedge:
  %.lcssa2 = phi * [ %.lcssa1, %bb7 ], [ %.lcssa, %bb8.outer.loopexit ]
  %ineq.0.ph.be = phi i32 [ 0, %bb7 ], [ 1, %bb8.outer.loopexit ]
  br label %bb8.outer

%bb8.backedge:
  br label %bb8
}
Transformation seems to be correct!


----------------------------------------
define void @simplified_ineqn() nowrite nofree {
%entry:
  br label %bb8.outer

%bb8.outer:
  %x = phi i32 [ 0, %entry ], [ 0, %bb6 ], [ 1, %bb2 ]
  br i1 undef, label %return, label %bb2

%return:
  ret void

%bb2:
  switch i32 %x, label %bb6 [
    i32 0, label %bb8.outer
  ]

%bb6:
  br i1 undef, label %bb8.outer, label %bb2
}
=>
define void @simplified_ineqn() nowrite nofree {
%entry:
  br label %bb8.outer

%bb8.outer:
  %x = phi i32 [ 0, %entry ], [ %x.ph, %bb8.outer.loopexit ]
  br i1 1, label %return, label %bb2.preheader

%return:
  ret void

%bb2.preheader:
  %0 = icmp eq i32 %x, 0
  br i1 %0, label %bb2.preheader.split.us, label %bb2.preheader.bb2.preheader.split_crit_edge

%bb2.preheader.split.us:
  br label %bb2.us

%bb2.us:
  switch i32 0, label %bb6.us [
    i32 0, label %bb8.outer.loopexit.us-lcssa.us
  ]

%bb6.us:
  br i1 1, label %bb8.outer.loopexit.us-lcssa.us, label %bb2.us

%bb8.outer.loopexit.us-lcssa.us:
  %x.ph.ph.us = phi i32 [ 0, %bb6.us ], [ 1, %bb2.us ]
  br label %bb8.outer.loopexit

%bb2.preheader.bb2.preheader.split_crit_edge:
  br label %bb2.preheader.split

%bb2.preheader.split:
  br label %bb2

%bb2:
  switch i32 %x, label %bb6 [
    i32 0, label %bb2.bb8.outer.loopexit.us-lcssa_crit_edge
  ]

%bb6:
  br i1 1, label %bb8.outer.loopexit.us-lcssasplit, label %bb2

%bb8.outer.loopexit.us-lcssasplit:
  %x.ph.ph.ph = phi i32 [ 0, %bb6 ]
  br label %bb8.outer.loopexit.us-lcssa

%bb2.bb8.outer.loopexit.us-lcssa_crit_edge:
  %split = phi i32 [ undef, %bb2 ]
  br i1 1, label %us-unreachable, label %bb8.outer.loopexit.us-lcssa

%us-unreachable:
  assume i1 0

%bb8.outer.loopexit.us-lcssa:
  %x.ph.ph = phi i32 [ %split, %bb2.bb8.outer.loopexit.us-lcssa_crit_edge ], [ %x.ph.ph.ph, %bb8.outer.loopexit.us-lcssasplit ]
  br label %bb8.outer.loopexit

%bb8.outer.loopexit:
  %x.ph = phi i32 [ %x.ph.ph, %bb8.outer.loopexit.us-lcssa ], [ %x.ph.ph.us, %bb8.outer.loopexit.us-lcssa.us ]
  br label %bb8.outer
}
Transformation seems to be correct!


----------------------------------------
define void @pnp_check_irq() {
%entry:
  %conv56 = trunc i64 undef to i32
  br label %while.cond.i

%while.cond.i:
  %call.i25 = call * @pci_get_device()
  br i1 undef, label %if.then65, label %while.body.i

%if.then65:
  assume i1 0

%while.body.i:
  br i1 undef, label %if.then31.i.i, label %while.cond.i.backedge

%if.then31.i.i:
  switch i32 %conv56, label %while.cond.i.backedge [
    i32 14, label %if.then42.i.i
    i32 15, label %if.then42.i.i
  ]

%if.then42.i.i:
  %call.i25.lcssa48 = phi * [ %call.i25, %if.then31.i.i ], [ %call.i25, %if.then31.i.i ]
  assume i1 0

%while.cond.i.backedge:
  br label %while.cond.i
}
=>
define void @pnp_check_irq() {
%entry:
  %conv56 = trunc i64 undef to i32
  %0 = icmp eq i32 %conv56, 14
  br i1 %0, label %entry.split.us, label %entry.entry.split_crit_edge

%entry.entry.split_crit_edge:
  br label %entry.split

%entry.split:
  %1 = icmp eq i32 %conv56, 15
  br i1 %1, label %entry.split.split.us, label %entry.split.entry.split.split_crit_edge

%entry.split.split.us:
  br label %while.cond.i.us1

%while.cond.i.us1:
  %call.i25.us2 = call * @pci_get_device()
  br i1 1, label %if.then65.us-lcssa.us-lcssa.us, label %while.body.i.us3

%if.then65.us-lcssa.us-lcssa.us:
  br label %if.then65.us-lcssa

%while.body.i.us3:
  br i1 undef, label %if.then31.i.i.us4, label %while.cond.i.backedge.us5

%if.then31.i.i.us4:
  switch i32 15, label %while.cond.i.backedge.us5 [
    i32 14, label %if.then42.i.i.us-lcssa.us-lcssa.us
    i32 15, label %if.then42.i.i.us-lcssa.us-lcssa.us
  ]

%if.then42.i.i.us-lcssa.us-lcssa.us:
  %call.i25.lcssa48.ph.ph.us = phi * [ %call.i25.us2, %if.then31.i.i.us4 ], [ %call.i25.us2, %if.then31.i.i.us4 ]
  br label %if.then42.i.i.us-lcssa

%while.cond.i.backedge.us5:
  br label %while.cond.i.us1

%entry.split.entry.split.split_crit_edge:
  br label %entry.split.split

%entry.split.split:
  br label %while.cond.i

%while.cond.i:
  %call.i25 = call * @pci_get_device()
  br i1 1, label %if.then65.us-lcssa.us-lcssa, label %while.body.i

%if.then65.us-lcssa.us-lcssa:
  br label %if.then65.us-lcssa

%if.then65.us-lcssa:
  br label %if.then65

%while.body.i:
  br i1 undef, label %if.then31.i.i, label %while.cond.i.backedge

%if.then31.i.i:
  switch i32 %conv56, label %while.cond.i.backedge [
    i32 14, label %if.then42.i.i.us-lcssa.us-lcssa
    i32 15, label %if.then42.i.i.us-lcssa.us-lcssa
  ]

%if.then42.i.i.us-lcssa.us-lcssa:
  %call.i25.lcssa48.ph.ph = phi * [ %call.i25, %if.then31.i.i ], [ %call.i25, %if.then31.i.i ]
  br label %if.then42.i.i.us-lcssa

%if.then42.i.i.us-lcssa:
  %call.i25.lcssa48.ph = phi * [ %call.i25.lcssa48.ph.ph, %if.then42.i.i.us-lcssa.us-lcssa ], [ %call.i25.lcssa48.ph.ph.us, %if.then42.i.i.us-lcssa.us-lcssa.us ]
  br label %if.then42.i.i

%while.cond.i.backedge:
  br label %while.cond.i

%entry.split.us:
  br label %while.cond.i.us

%while.cond.i.us:
  %call.i25.us = call * @pci_get_device()
  br i1 1, label %if.then65.us-lcssa.us, label %while.body.i.us

%if.then65.us-lcssa.us:
  br label %if.then65

%if.then65:
  assume i1 0

%while.body.i.us:
  br i1 undef, label %if.then31.i.i.us, label %while.cond.i.backedge.us

%if.then31.i.i.us:
  switch i32 14, label %while.cond.i.backedge.us [
    i32 14, label %if.then42.i.i.us-lcssa.us
    i32 15, label %if.then42.i.i.us-lcssa.us
  ]

%if.then42.i.i.us-lcssa.us:
  %call.i25.lcssa48.ph.us = phi * [ %call.i25.us, %if.then31.i.i.us ], [ %call.i25.us, %if.then31.i.i.us ]
  br label %if.then42.i.i

%if.then42.i.i:
  %call.i25.lcssa48 = phi * [ %call.i25.lcssa48.ph, %if.then42.i.i.us-lcssa ], [ %call.i25.lcssa48.ph.us, %if.then42.i.i.us-lcssa.us ]
  assume i1 0

%while.cond.i.backedge.us:
  br label %while.cond.i.us
}
Transformation doesn't verify!
ERROR: Source is more defined than target

Example:

Source:
i32 %conv56 = any
  >> Jump to %while.cond.i
* %call.i25 = UB triggered!

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0
Block 1 >	size: 0	align: 1

Target:
i32 %conv56 = #xfffffff1 (4294967281, -15)
i1 %0 = #x0 (0)
UB triggered on br



------------------- SMT STATS -------------------
Num queries: 12
Num invalid: 0
Num skips:   0
Num trivial: 14 (53.8%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     10 (83.3%)
Num UNSAT:   2 (16.7%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 1'
+ /home/nuno/alive2/build/opt-alive.sh -loop-unswitch -enable-new-pm=0 -verify-memoryssa -verify-loop-info -verify-dom-info -disable-output

 

<-- Back