AliveToolkit / alive2

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

ERROR: Invalid expr (with --tgt-is-asm) #993

Closed regehr closed 6 months ago

regehr commented 6 months ago
regehr@john-home:~/alive2-regehr/build$ cat src.ll
; ModuleID = 'M2'
source_filename = "M2"
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
target triple = "aarch64-linux-gnu"

define i32 @non_speculatable_load_of_select_inner_inverted(i1 %0, i1 %1, ptr %2, ptr %3) {
  %5 = alloca i32, align 4
  store i32 0, ptr %5, align 4
  %6 = select i1 %0, ptr %3, ptr %5, !prof !0
  %7 = select i1 %1, ptr %6, ptr %2, !prof !0
  %8 = load i32, ptr %7, align 4
  ret i32 %8
}

!0 = !{!"branch_weights", i32 1, i32 99}
regehr@john-home:~/alive2-regehr/build$ cat tgt.ll
; ModuleID = 'M2'
source_filename = "M2"
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
target triple = "aarch64-linux-gnu"

define i32 @non_speculatable_load_of_select_inner_inverted(i1 %0, i1 %1, ptr %2, ptr %3) local_unnamed_addr {
arm_tv_entry:
  %stack = tail call align 16 dereferenceable(1280) ptr @myalloc(i32 1280, i32 16)
  %4 = getelementptr inbounds i8, ptr %stack, i64 1024
  %5 = ptrtoint ptr %4 to i64
  %6 = ptrtoint ptr %2 to i64
  %7 = ptrtoint ptr %3 to i64
  %a2_1 = add i64 %5, -16
  %a3_1 = add i64 %5, -4
  %8 = inttoptr i64 %a2_1 to ptr
  %a5_3 = getelementptr i8, ptr %8, i64 12
  store i32 0, ptr %a5_3, align 4
  %a6_7 = select i1 %0, i64 %7, i64 %a3_1
  %a8_7 = select i1 %1, i64 %a6_7, i64 %6
  %9 = inttoptr i64 %a8_7 to ptr
  %a9_1 = load i32, ptr %9, align 1
  ret i32 %a9_1
}

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

attributes #0 = { allockind("alloc") allocsize(0) }
regehr@john-home:~/alive2-regehr/build$ ./alive-tv src.ll tgt.ll --tgt-is-asm

----------------------------------------
define i32 @non_speculatable_load_of_select_inner_inverted(i1 %#0, i1 %#1, ptr %#2, ptr %#3) {
#4:
  %#5 = alloca i64 4, align 4
  store i32 0, ptr %#5, align 4
  %#6 = select i1 %#0, ptr %#3, ptr %#5
  %#7 = select i1 %#1, ptr %#6, ptr %#2
  %#8 = load i32, ptr %#7, align 4
  assume_dereferenceable ptr %#7, i64 4
  ret i32 %#8
}
=>
declare ptr @myalloc(i32, allocalign i32)

define i32 @non_speculatable_load_of_select_inner_inverted(i1 %#0, i1 %#1, ptr %#2, ptr %#3) asm {
arm_tv_entry:
  %stack = call ptr @myalloc(i32 1280, allocalign i32 16) dereferenceable(1280) nonnull align(16) allockind(alloc) allocsize(0)
  %#4 = gep inbounds ptr %stack, 1 x i64 1024
  %#5 = ptrtoint ptr %#4 to i64
  %#6 = ptrtoint ptr %#2 to i64
  %#7 = ptrtoint ptr %#3 to i64
  %a2_1 = add i64 %#5, -16
  %a3_1 = add i64 %#5, -4
  %#8 = int2ptr i64 %a2_1 to ptr
  %a5_3 = gep ptr %#8, 1 x i64 12
  store i32 0, ptr %a5_3, align 4
  %a6_7 = select i1 %#0, i64 %#7, i64 %a3_1
  %a8_7 = select i1 %#1, i64 %a6_7, i64 %#6
  %#9 = int2ptr i64 %a8_7 to ptr
  %a9_1 = load i32, ptr %#9, align 1
  ret i32 %a9_1
}
ERROR: Invalid expr

Summary:
  0 correct transformations
  0 incorrect transformations
  1 failed-to-prove transformations
  0 Alive2 errors
regehr@john-home:~/alive2-regehr/build$ 
nunoplopes commented 6 months ago

This one has been fixed already. At least I can't repro it.