The reference makes guarantees about "stack memory" that do not reflect our op.sem

[RalfJung]

https://doc.rust-lang.org/reference/variables.html says that "A local variable (or stack-local allocation) holds a value directly, allocated within the stack's memory." However, on the level of the Abstract Machine, there is no such thing as "the stack's memory". All allocated objects are placed at arbitrary locations in memory and there is no guarantee whatsoever that stack allocations are in "the stack" or Box allocations are on "the heap".

For instance, many local variables end up not having any actual memory allocated anywhere as they are entirely turned into registers.

The wording in the reference should be adjusted to avoid claims that cannot be held up by the Abstract Machine.

Thanks to @tautschnig for pointing this out.

Cc @rust-lang/opsem

[mattheww]

I observe that the return expressions page uses the term "Activation frame".

[RalfJung]

The notion of a stack frame exists in the Abstract Machine. It records the location to jump to when the function returns, and the place in memory that stores each local variable. However, this Abstract Machine stack lives outside of memory in a dedicated, non-addressable part of the AM state.

[CAD97]

Well, we do actually expose a concept of "the stack's memory" via the thread builder's stack size configuration. So the reference refers to locals being in stack in that concept of stack, and in that the stack local allocations die with the stack frame.

That's not to say the wording can't be improved to avoid implying the formal existence of a concept which doesn't exist in the abstract opsem. But I do think saying that locals are stack allocated is a meaningful QOI property, even if it isn't formally meaningful in the opsem.

[RalfJung]

Well, we do actually expose a concept of "the stack's memory" via the thread builder's stack size configuration. So the reference refers to locals being in stack in that concept of stack, and in that the stack local allocations die with the stack frame.

True. But we don't provide a way to compute how much stack memory will be needed to hold any particular function.

Instead, each time a function is called the spec just decides non-deterministically whether we're out of stack space or not. Setting a larger stack space is supposed to make that error happen later. But that's a QOI question as you say, not something we can provide exact bounds/guarantees for.