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

[RalfJung]

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

[nunoplopes]

The current LLVM memory model doesn't allow changing the size of objects in place.

Thanks! That's what we wanted to find out. Is this written down anywhere?

I don't recall, but I don't think so. But I can guarantee you that optimizations follow that semantics. And Alive2 too, and these days it is kind of the oracle.

[nunoplopes]

The current LLVM memory model doesn't allow changing the size of objects in place.

So, either bar does realloc on the pointer, which is equivalent to freeing it, and thus the load would be UB. Or it doesn't touch the pointer and the load is all fine.

C and C++ don't have object resizing. Or at least not to a point where we may need to model in the IR.
If Rust needs something along these lines, then we need to change LLVM IR's semantics and its optimizations. LLVM is not correct per the semantics you want.

The easiest way would be for Rust to hide the resizing in some function that returns a new pointer, so LLVM can think it's a new object. If that isn't viable (for some reason), then there's a ton of work to be done on LLVM. The Alive2 side is easy FWIW.

[RalfJung]

The current LLVM memory model doesn't allow changing the size of objects in place.

Thanks! That's what we wanted to find out. Is this written down anywhere?

The easiest way would be for Rust to hide the resizing in some function that returns a new pointer, so LLVM can think it's a new object

That doesn't work, since the entire point of this is to allow old pointers to still be used with the resized allocation. Otherwise we could just use realloc.

[RalfJung]

What about the other question -- isn't the example an Alive bug since bar might initialize mem[0] to some value and then the source would return that value, but the target would return poison/undef since memory is uninit?

[nunoplopes]

What about the other question -- isn't the example an Alive bug since bar might initialize mem[0] to some value and then the source would return that value, but the target would return poison/undef since memory is uninit?

It's a bug, yes.
It's a know problem: Alive2 doesn't havoc local memory blocks on function calls. This requires aligning the allocations in the src & tgt programs, and that stuff isn't implemented yet.