AliveToolkit / alive2

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

False positive with function argument refinement: local -> non-local #958

Open nunoplopes opened 8 months ago

nunoplopes commented 8 months ago

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

define void @src(ptr align 4 dereferenceable(128) %dst) {
  %src = alloca [128 x i8], align 4
  call void @accept_ptr(ptr nocapture %src) memory(argmem: readwrite)
  call void @llvm.memcpy.p0.p0.i64(ptr align 4 %dst, ptr %src, i64 128, i1 false)
  ret void
}

define void @tgt(ptr align 4 dereferenceable(128) %dst) {
  call void @accept_ptr(ptr nocapture %dst) memory(argmem: readwrite)
  ret void
}

declare void @accept_ptr(ptr)
declare void @llvm.memcpy.p0.p0.i64(ptr, ptr, i64, i1)
nunoplopes commented 8 months ago

cc @nikic