Test source: git
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!
+ : '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