possible regression witn ptr2int

regehr commented 2 weeks ago

Here's a src/tgt pair that registers as a refinement using the Alive2 that I built the other day, it's 405c202e69d6dc576c739ddb891659a22cec5ecd from June 13.

However, the same src/tgt pair registers as a value mismatch using Alive2 from today.

https://alive2.llvm.org/ce/z/4d5oCY

define i32 @src(ptr %0, i1 %1) {
  %3 = alloca i32, align 4
  br i1 %1, label %4, label %5

4:                                                ; preds = %2
  store i32 1, ptr %3, align 4
  br label %7

5:                                                ; preds = %2
  %6 = udiv i32 0, 0
  store i32 0, ptr %0, align 4
  br label %7

7:                                                ; preds = %5, %4
  %8 = load i32, ptr %3, align 4
  ret i32 %8
}

define i32 @tgt(ptr %0, i1 %1) local_unnamed_addr {
arm_tv_entry:
  %stack = tail call align 16 dereferenceable(1280) ptr @myalloc(i64 1280, i64 16)
  %2 = getelementptr inbounds i8, ptr %stack, i64 1024
  %3 = ptrtoint ptr %2 to i64
  %a3_1 = add i64 %3, -16
  br i1 %1, label %"1", label %.LBB0_2

"1":                                              ; preds = %arm_tv_entry
  %4 = inttoptr i64 %a3_1 to ptr
  %5 = getelementptr i8, ptr %4, i64 12
  store i32 1, ptr %5, align 4
  br label %.LBB0_3

.LBB0_2:                                          ; preds = %arm_tv_entry
  store i32 0, ptr %0, align 1
  %.pre = inttoptr i64 %a3_1 to ptr
  br label %.LBB0_3

.LBB0_3:                                          ; preds = %.LBB0_2, %"1"
  %.pre-phi = phi ptr [ %.pre, %.LBB0_2 ], [ %4, %"1" ]
  %6 = getelementptr i8, ptr %.pre-phi, i64 12
  %a12_1 = load i32, ptr %6, align 1
  ret i32 %a12_1
}

; Function Attrs: mustprogress willreturn allockind("alloc") allocsize(0)
declare nonnull ptr @myalloc(i64, i64 allocalign) local_unnamed_addr #0

; Function Attrs: mustprogress willreturn allockind("free")
declare void @myfree(ptr allocptr) local_unnamed_addr #1

attributes #0 = { mustprogress willreturn allockind("alloc") allocsize(0) "alloc-family"="arm-tv-alloc" }
attributes #1 = { mustprogress willreturn allockind("free") "alloc-family"="arm-tv-alloc" }

nunoplopes commented 2 weeks ago

(I'll defer int2ptr issues until after PLDI)

regehr commented 2 weeks ago

if it's helpful, here's another pair that validated not long ago, that alarms (incorrectly, I believe) now

https://alive2.llvm.org/ce/z/gc5mhP

AliveToolkit / alive2

possible regression witn ptr2int #1055