AliveToolkit / alive2

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

oops one more memory model thing #1059

Closed regehr closed 1 week ago

regehr commented 2 weeks ago

well, I spoke too soon when I said all integer widths and load/store combinations work now. I'm still getting a refinement failure for this one with -tgt-is-asm. all of my other tests work!

define void @src(ptr %0) {
  %2 = load i1, ptr %0, align 1
  store i1 %2, ptr %0, align 1
  ret void
}

define void @tgt(ptr %0) {
  ret void
}
regehr commented 2 weeks ago

thinking about this a bit more... the pattern here is that when the backend elides the memory operations, we get a refinement failure. this isn't going to matter is very many real situations. I don't know that it needs to be fixed.

regehr commented 1 week ago

ok here's one that's more real, that looks like a false alarm

define void @f(ptr %0, ptr %1, ptr %2) {
  %4 = load i1, ptr %1, align 1
  %5 = load i1, ptr %2, align 1
  %6 = load i1, ptr %0, align 1
  %7 = select i1 %6, i1 %4, i1 %5
  store i1 %7, ptr %0, align 1
  ret void
}

this turns into:

_f:                             
    ldrb    w8, [x0]
    cmp w8, #0
    csel    x8, x1, x2, ne
    ldrb    w8, [x8]
    strb    w8, [x0]
    ret

which seems perfectly fine, and then lifts to:

define void @f(ptr %0, ptr %1, ptr %2) local_unnamed_addr {
arm_tv_entry:
  %a3_1 = load i8, ptr %0, align 1
  %a3_2 = and i8 %a3_1, 1
  %a4_6.not = icmp eq i8 %a3_2, 0
  %a5_7.v = select i1 %a4_6.not, ptr %2, ptr %1
  %a6_1 = load i8, ptr %a5_7.v, align 1
  store i8 %a6_1, ptr %0, align 1
  ret void
}

which I think is again fine, but this fails due to something poison-related that I don't follow