I'm wondering if it's possible for there to be unbounded operand stack usage within WebAssembly code.
Closest I could think is loops, which doesn't exactly happen:
(func
loop (result i32)
i32.const 5
br 0
end
unreachable)
The above example will implicitly pop the 5
before branching.
(func
i32.const 6
loop (param i32) (result i32)
i32.const 5
br 0
end
unreachable)
The above example will implicitly copy the 5
before branching, and pop the 6
. (making the stack look like 6 5
on the first loop, then 5 5
on all subsequent branches)
I'm wondering if there's any edge-cases where unbounded stack usage can happen.
By unbounded, I don't include recursion. I mean unbounded with respect to the current call frame (not including any sub-calls' frames)
No, stack space is bounded. I was hoping it would be a consequence of the soundness theorem, but I don't see an obvious way to get it. Instead, you can argue as follows:
loop
instruction must be used, and in particular one of the finitely many labels must be traversed infinitely many times (and with different configurations, because otherwise the whole program would recur and not use unbounded memory).
and the label blocks the stack below it until it is jumped to in this operation:
But this is a problem, because the state at the end of the second transition is exactly the starting state of the first transition. That means that if is the upper part of the stack, we will always either have or in this loop, where is fixed and inaccessible. So we can't get an infinite number of different stack shapes; the only state we have to work with is the , where is predetermined from the block type of the loop label.
An alternative proof is: it's intended to run on regular hardware via standard compiler analyses, so of course the size of the stack frame is statically determinable, else the spec would be broken.
Thanks. Yeah, I realized that it would be pretty much impossible to determine the stack's validity with respect to its operands, if it were able to use unbounded space, since the only real operations where that could happen would likely have to be dependent on the value of the operand put in, which is not allowed by the spec--WASM instructions can be dependent on the stack's current type, but not dependent on values within the stack (this would end up having more of a... dependent type system which would be kind of infeasible to check in the general case within a reasonable amount of time and with a reasonable amount of simplicity).
Last updated: Dec 23 2024 at 12:05 UTC