AliveToolkit / alive2

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

possible false alarm #1004

Closed regehr closed 5 months ago

regehr commented 5 months ago

here's a src/tgt pair that gives UB triggered! when invoked as:

./alive-tv --disable-undef-input --disable-poison-input baz.ll
@last = external local_unnamed_addr global ptr

define void @src(ptr %0) {
  %x3 = alloca ptr, align 8
  br i1 false, label %x5, label %x7

x5:
  %x6 = load ptr, ptr @last, align 4
  store ptr %x6, ptr %x3, align 8
  ret void

x7:
  %x4 = load ptr, ptr %0, align 4
  %x8 = load ptr, ptr %x4, align 4
  store ptr %x8, ptr %x3, align 8
  ret void
}

define void @tgt(ptr %0) {
arm_tv_entry:
  %stack = alloca ptr, align 1
  br i1 false, label %.LBB0_3, label %.LBB0_2

.LBB0_2:
  %x2 = load ptr, ptr %0, align 1
  br label %.LBB0_3

.LBB0_3:
  %X8.0 = phi ptr [ %x2, %.LBB0_2 ], [ @last, %arm_tv_entry ]
  %a10_1 = load ptr, ptr %X8.0, align 1
  store ptr %a10_1, ptr %stack, align 1
  ret void
}

however, if we make a simple change to tgt, replacing the final load with this code:

  %a10_1 = load ptr, ptr %x2, align 1

then it verifies. so, was the UB triggered! in the first case a false alarm? sorry if I'm missing something stupid

regehr commented 5 months ago

cc @tanmaytirpankar

nunoplopes commented 5 months ago

this is a bug in the preprocessor.

BTW, for performance sake, it would be best to align allocas in tgt to at least 8 bytes (if possible).

regehr commented 5 months ago

(I think the allocas were originally aligned, I had hand-edited this example A LOT before I could be certain it was an Alive2 issue)