AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

wrong result witn int2ptr? #1062

Closed regehr closed 1 week ago

regehr commented 1 week ago

I think Alive is just incorrect in this example.

here's src:

define i32 @f(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 = srem 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
}

clearly it returns 1 when invoked as f(nullptr, true)

here's tgt:

define i32 @f(ptr %0, i1 %1) local_unnamed_addr {
arm_tv_entry:
  %stack = alloca [1280 x i8], align 4
  %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
}

it looks like this should also return 1, but Alive with -tgt-is-asm gives me a CEX saying that for those same inputs, this returns 0

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

nunoplopes commented 1 week ago

dup of #1055