AliveToolkit / alive2

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

Incorrect bit layout for vectors of overaligned elements #1002

Closed jasilvanus closed 5 months ago

jasilvanus commented 5 months ago

Alive2 complains about this valid transform:

target datalayout = "e-p:64:64-p1:16:16-p2:32:32:32-p3:64:64:64-f16:32"

@Global = external global [10 x i8]

; This should be turned into a constexpr instead of being an instruction
define void @test_overaligned_vec(i8 %B) {
; CHECK-LABEL: @test_overaligned_vec(
; CHECK-NEXT:    store i8 [[B:%.*]], ptr getelementptr inbounds ([10 x i8], ptr @Global, i64 0, i64 2), align 1
; CHECK-NEXT:    ret void
  %A = getelementptr <2 x half>, ptr @Global, i64 0, i64 1
  store i8 %B, ptr %A
  ret void
}

Link: https://alive2.llvm.org/ce/z/2iCNZ_

The complaint goes away if f16:32 is replaced by f16:16.

Apparently Alive2 assumes padding bits within vectors of overaligned elements. Such vectors however are always bit-packed. https://github.com/llvm/llvm-project/pull/75448 fixed some parts of LLVM in this regard, apparently a similar change is needed in Alive2, likely around here: https://github.com/AliveToolkit/alive2/blob/64fd5fb408a12439daed663a1136a8409f361261/llvm_util/llvm2alive.cpp#L631