False positive with memory?

[nikic]

https://alive2.llvm.org/ce/z/9jjAiv

define void @src(ptr align 4 %val) {
  %val1 = alloca i32, align 4
  call void @llvm.memcpy.p0.p0.i64(ptr align 4 %val1, ptr align 4 %val, i64 4, i1 false)
  call void @f(ptr align 4 nocapture readonly %val1) memory(argmem: read)
  ret void
}

define void @tgt(ptr align 4 %val) {
  call void @f(ptr align 4 nocapture readonly %val) memory(argmem: read)
  ret void
}

declare void @f(ptr)

Gives:

ERROR: Source is more defined than target

Example:
ptr align(4) %val = pointer(non-local, block_id=1, offset=3) / Address=#x04

Source:
ptr %val1 = pointer(local, block_id=0, offset=0) / Address=#x10
void = function did not return!

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

LOCAL BLOCKS:
Block 2 >	size: 4	align: 4	alloc type: 1	alive: true	address: 16

Target:
Function @f triggered UB

I've been staring at this output for a while, but I don't understand what the issue here is supposed to be.

[nunoplopes]

I think nocapture is not sufficient. It doesn't cover pointer comparisons.
Imagine this example:

call @src(@global)

..

define @f(ptr %p) {
   %cmp = icmp eq ptr %p, @global
   br i1 %cmp, label then, label else

then:
  ret 1

else
  ret 2
}

So changing from an alloca to a particular global var changes the output of the function.
No you tell me that f doesn't return or write anything. But it can still exit the program (or not) depending on the address of the input ptr.

We don't have an easy way of expressing that a function is agnostic to concrete pointer addresses.

[nikic]

nocapture in LLVM covers both address capture and provenance escape. Your example is the 3rd point in https://llvm.org/docs/LangRef.html#pointercapture. (Splitting this into two attributes is on my TODO list, but I never get around to it...)

So it sounds like alive2 models nocapture as only forbidding provenance escape, but still allowing address capture?

[nunoplopes]

Ok, then the whole nocapture needs revamping. We don't check for address escaping.