AliveToolkit / alive2

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

False positive with hoisted load of `dereferenceable` pointer. #984

Closed fhahn closed 6 months ago

fhahn commented 6 months ago

Test case https://alive2.llvm.org/ce/z/YrATgy

Alive2 claims UB is triggered after hoisting the load, but the pointer is marked as dereferenceable(24), so speculatively loading 8 bytes should be fine, unless I am missing something.

declare noundef i1 @fn()

define i64 @src(ptr dereferenceable(24) align(8) %this, i1 %call1) {
entry:
  %call11 = call i1 @fn()
  br i1 %call1, label %cond.true, label %cond.end

cond.true:
  %l = load i64, ptr %this, align 8
  br label %cond.end

cond.end:
  ret i64 0
}

define i64 @tgt(ptr dereferenceable(24) align(8) %this, i1 %call1) {
entry:
  %call11 = call i1 @fn()
  %l = load i64, ptr %this, align 8
  ret i64 0
}
----------------------------------------
declare i1 @fn()

define i64 @src(ptr dereferenceable(24) align(8) %this, i1 %call1) {
entry:
  %call11 = call i1 @fn() noundef
  br i1 %call1, label %cond.true, label %cond.end

cond.true:
  %l = load i64, ptr dereferenceable(24) align(8) %this, align 8
  br label %cond.end

cond.end:
  ret i64 0
}
=>
declare i1 @fn()

define i64 @tgt(ptr dereferenceable(24) align(8) %this, i1 %call1) {
entry:
  %call11 = call i1 @fn() noundef
  %l = load i64, ptr dereferenceable(24) align(8) %this, align 8
  ret i64 0
}
Transformation doesn't verify!

ERROR: Source is more defined than target

Example:
ptr dereferenceable(24) align(8) %this = pointer(non-local, block_id=1, offset=0)
i1 %call1 = #x0 (0)

Source:
i1 %call11 = #x0 (0)
  >> Jump to %cond.end

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 8    alloc type: 0   alive: false    address: 0
Block 1 >   size: 128   align: 8    alloc type: 2   alive: false    address: 8
Block 2 >   align: 8    alloc type: 0   alive: true

Target:
i1 %call11 = #x0 (0)
i64 %l = UB triggered!
nunoplopes commented 6 months ago

My understanding is that dereferenceable is valid at function entry. Then function @fn may free that memory, and thus loading from that pointer may not be safe anymore. If you tag @fn with nofree, the test goes through.