AliveToolkit / alive2

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

load widening not working? #1005

Closed regehr closed 5 months ago

regehr commented 5 months ago

here's src:

define void @f(ptr %0, ptr %1) {
  %3 = load <6 x i32>, ptr %0, align 16
  %4 = insertelement <6 x i32> %3, i32 0, i64 4
  store <6 x i32> %4, ptr %1, align 16
  ret void
}

this gives AArch64 code that looks fine, but it issues two 16-byte loads instead of a 16 and an 8:

f:
        ldp     q1, q0, [x0]
        mov     v0.s[0], wzr
        str     q1, [x1]
        str     d0, [x1, #16]
        ret

we're lifting to:

define void @f(ptr nocapture readonly %0, ptr nocapture writeonly %1) local_unnamed_addr {
arm_tv_entry:
  %a2_1 = load i128, ptr %0, align 1
  %2 = getelementptr i8, ptr %0, i64 16
  %a2_213 = load <4 x i32>, ptr %2, align 1
  %a3_4 = insertelement <4 x i32> %a2_213, i32 0, i64 0
  store i128 %a2_1, ptr %1, align 1
  %bc = bitcast <4 x i32> %a3_4 to <2 x i64>
  %a5_2 = extractelement <2 x i64> %bc, i64 0
  %a5_3 = getelementptr i8, ptr %1, i64 16
  store i64 %a5_2, ptr %a5_3, align 1
  ret void
}

but then Alive gives:

<4 x i32> %a2_213 = UB triggered!

are we doing something wrong here, such that Alive isn't making sure there's enough dereferenceable storage to absorb the widened load? I tried making the loads align 16 and that didn't help

regehr commented 5 months ago

cc @tanmaytirpankar