Skip to content

Allocations cannot shrink? Or alive fails to model extern function calls? #934

Open
@RalfJung

Description

@RalfJung

During a Rust discussion, the following interesting example came up:

----------------------------------------
define i32 @src() {
%0:
  %mem = call ptr @malloc(noundef i64 160) nofree noundef nothrow noalias willreturn dereferenceable_or_null(160) alloc-family(malloc) allockind(alloc, uninitialized) allocsize(0) memory(inaccessiblemem: readwrite)
  call void @bar(noundef ptr %mem)
  %arrayidx = gep inbounds ptr %mem, 4 x i64 0
  %1 = load i32, ptr %arrayidx, align 4 // load from `mem[0]`
  ret i32 %1
}
=>
define i32 @tgt() {
%0:
  %mem = call ptr @malloc(noundef i64 160) nofree noundef nothrow noalias willreturn dereferenceable_or_null(160) alloc-family(malloc) allockind(alloc, uninitialized) allocsize(0) memory(inaccessiblemem: readwrite)
  call void @bar(noundef ptr %mem)
  %arrayidx = gep inbounds ptr %mem, 4 x i64 39
  %1 = load i32, ptr %arrayidx, align 4 // load from `mem[39]`
  ret i32 %1
}
Transformation seems to be correct!

I am struggling to interpret this. As a transformation I would say this is definitely incorrect since bar could have initialized this memory, and then the tgt program can return a different value than the src program. Maybe that is some systematic Alive limitation that I am not understanding, but then it is hard to say what this actually says about the intended LLVM semantics.

In particular, what if there was an operation that can shrink an allocation in-place? In Rust we are considering adding such an operation. Then even though loading at offset 0 is still fine after bar, loading from offset 39 might not be fine any more. Maybe the fact that Alive accepts this transformation is a sign that LLVM assumes that allocations can never shrink (which would be a bummer), or maybe this is just Alive not properly modeling all the things bar could do -- we could use some help to interpret these results. :)

Metadata

Metadata

Assignees

No one assigned

    Labels

    memoryMemory Model

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions