likely loop unroling bug

[regehr]

cc @MitchBriles

We're having trouble with this function:

define i32 @f() {
  br label %1

1:                                                ; preds = %6, %0
  %2 = phi i32 [ 0, %0 ], [ 1, %6 ]
  br label %3

3:                                                ; preds = %5, %1
  %4 = mul i32 %2, 1
  br label %5

5:                                                ; preds = %3
  br i1 false, label %3, label %6

6:                                                ; preds = %5
  %7 = icmp slt i32 %2, 1
  br i1 %7, label %1, label %8

8:                                                ; preds = %6
  ret i32 %4
}

this should return 1, and alive-exec agrees with that.

on the other hand, alive-tv with unrolling has a different opinion, it looks like probably that inner branch on false is confusing the unroller and it returns the value from the wrong iteration.

regehr@ohm:~/reduce$ ~/alive2-regehr/build/alive-tv r2.ll -src-unroll=2 

----------------------------------------
define i32 @f() {
#0:
  %#7#ptr#2 = alloca i32 4, align 16
  br label %#1

#1:
  %#6 = phi i32 [ 0, %#0 ], [ 1, %#4 ]
  br label %#2

#2:
  %#7 = mul i32 %#6, 1
  store i32 %#7, ptr %#7#ptr#2, align 16
  br label %#3

#3:
  br i1 0, label %#2#1#2, label %#4

#2#1#2:
  %#7#1#2 = mul i32 %#6, 1
  br label %#3#1#2

#3#1#2:
  br i1 0, label %#2#exit, label %#4

#2#exit:
  %#7#exit = mul i32 %#6, 1
  br label #sink

#4:
  %#7#phi#0 = phi i32 [ %#7, %#3 ], [ %#7#1#2, %#3#1#2 ]
  %#8 = icmp slt i32 %#6, 1
  br i1 %#8, label %#1#2, label %#5

#1#2:
  %#6#2 = phi i32 [ 1, %#4 ]
  br label %#2#2

#2#2:
  %#7#2 = mul i32 %#6#2, 1
  store i32 %#7#2, ptr %#7#ptr#2, align 16
  br label %#3#2

#3#2:
  br i1 0, label %#2#1#2#2, label %#4#2

#2#1#2#2:
  %#7#1#2#2 = mul i32 %#6#2, 1
  br label %#3#1#2#2

#3#1#2#2:
  br i1 0, label %#2#exit#2, label %#4#2

#2#exit#2:
  %#7#exit#2 = mul i32 %#6#2, 1
  br label #sink

#4#2:
  %#7#phi#0#2 = phi i32 [ %#7#2, %#3#2 ], [ %#7#1#2#2, %#3#1#2#2 ]
  %#8#2 = icmp slt i32 %#6#2, 1
  br i1 %#8#2, label %#1#exit, label %#5

#1#exit:
  %#6#exit = phi i32 [ 1, %#4#2 ]
  br label #sink

#5:
  %#7#phi#1 = phi i32 [ %#7, %#4 ], [ %#7#2, %#4#2 ]
  %#7#ptr#2#load = load i32, ptr %#7#ptr#2, align 16
  ret i32 %#7#phi#0
}
=>
define i32 @f() nofree noundef willreturn memory(none) {
#0:
  ret i32 1
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:

Source:
ptr %#7#ptr#2 = pointer(local, block_id=0, offset=0) / Address=#x100
  >> Jump to %#1
i32 %#6 = #x00000000 (0)
  >> Jump to %#2
i32 %#7 = #x00000000 (0)
  >> Jump to %#3
  >> Jump to %#4
i32 %#7#phi#0 = #x00000000 (0)
i1 %#8 = #x1 (1)
  >> Jump to %#1#2
i32 %#6#2 = #x00000001 (1)
  >> Jump to %#2#2
i32 %#7#2 = #x00000001 (1)
  >> Jump to %#3#2
  >> Jump to %#4#2
i32 %#7#phi#0#2 = #x00000001 (1)
i1 %#8#2 = #x0 (0)
  >> Jump to %#5
i32 %#7#phi#1 = #x00000001 (1)
i32 %#7#ptr#2#load = #x00000001 (1)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 64	alloc type: 2	alive: true

LOCAL BLOCKS:
Block 2 >	size: 4	align: 16	alloc type: 1	alive: true	address: #x100

Target:

TARGET MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 64	alloc type: 2	alive: true
Source value: #x00000000 (0)
Target value: #x00000001 (1)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

[regehr]

@MitchBriles do you want to take a stab at this? the loop unrolling isn't a very easy part of Alive.
cc also @zhengyang92

[MitchBriles]

I'm looking into this now and came across a crash that might be a result of the same bug. Reduced reproducer: https://alive2.llvm.org/ce/z/kAMSQv. Note src and tgt are equal here, so it could only be an unroller bug, right?