AliveToolkit / alive2

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

another possible bug with -tgt-is-asm and oversized loads #1053

Closed regehr closed 2 weeks ago

regehr commented 2 weeks ago

here's another one where Alive is giving a value mismatch but the lifted ARM code looks fine

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

define i1 @src(ptr %0) {
  %2 = load i33, ptr %0, align 4
  %3 = icmp slt i33 %2, 0
  ret i1 %3
}

define i1 @tgt(ptr %0)  {
arm_tv_entry:
  %1 = getelementptr i8, ptr %0, i64 4
  %a3_1 = load i8, ptr %1, align 1
  %a6_23 = trunc i8 %a3_1 to i1
  ret i1 %a6_23
}