AliveToolkit / alive2

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

Add a flag to disable counterexamples with type punning through memory #1035

Open nunoplopes opened 1 month ago

nunoplopes commented 1 month ago

So we don't get counterexamples with loads being poison. We have something similar in place for the asm mode already. Can likely reuse that code.

for @regehr

regehr commented 1 month ago

just as a random example I get a lot of stuff like this where (if I understand correctly) a byte containing pointer data poisons the results

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

define void @f(ptr %0, ptr %1) {
  %3 = load i32, ptr %0, align 8
  %4 = load i16, ptr %0, align 1
  %5 = insertelement <8 x i16> zeroinitializer, i16 %4, i64 0
  %6 = bitcast <8 x i16> %5 to <4 x i32>
  %7 = insertelement <4 x i32> zeroinitializer, i32 %3, i64 0
  %8 = shufflevector <4 x i32> %6, <4 x i32> %7, <4 x i32> <i32 0, i32 4, i32 1, i32 5>
  store <4 x i32> %8, ptr %0, align 4
  ret void
}