search

AliveToolkit / alive2

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

bug relating to too-big store? #1034

Closed regehr closed 1 month ago

regehr commented 1 month ago

alive-tv is giving me a value mismatch on this code but shouldn't it be undefined in all executions due to storing an i64 into that i8 that we alloca'ed?

define i64 @f() {
  %1 = alloca i8, align 8
  %2 = alloca ptr, align 8
  store i64 1, ptr %1, align 8
  store ptr %1, ptr %2, align 8
  %3 = load ptr, ptr %2, align 8
  %4 = load i64, ptr %3, align 8
  ret i64 %4
}
nunoplopes commented 1 month ago

Ah, that is related with a fix for https://github.com/AliveToolkit/alive2/issues/1028 Allocation sites are rounded up to the alignment.

It's unclear to me if we really want that at the middle-end, or just for later codegen passes. There's a bit of a discussion going on LLVM's side. So right now, the code is not UB as expected. Though I'm happy to look at concrete examples to try to bias the semantics either way.