Design: Clarification of stack popping for conditional branches

[cretz]

I am toying w/ writing a WebAssembly compiler. I am looking at the test https://github.com/WebAssembly/spec/blob/634f0d9009404f498ef8d8bd510bd6f0941219cc/test/core/br_if.wast#L272 which looks like this expanded a bit:

(module
    (func
      $type-arg-void-vs-num-nested
      (result i32)

      block i32
        (i32.const 0)
        block
          (i32.const 1)
          (br_if 1)
        end
      end
    )
)

The error I get is:

Error: check failed:
test.wast:10:12
type stack size too small at br_if value. got 0, expected at least 1
          (br_if 1)
           ^^^^^^^

I would think the stack size when it reaches br_if is 2 which means that it pops 1 for the conditional and then has one leftover to satisfy the outer block. I assumed (i32.const 0) would fall through to the nested block. Which part am I missing? Thanks in advance.

[binji]

Yes, the error reporting of wabt can improve here. Even though there are two i32s on the stack, operators will never pop past the beginning of a block, so there is effectively only one.

[cretz]

Does this mean each block gets its own stack? I was confused by the following statement in the semantics doc:

Executing a block or loop instruction has no effect on the value stack.

Maybe that should change to:

Executing a block or loop instruction has no effect on the value stack, but all stack values outside of the executing block are inaccessible.

Or am I misunderstanding?

[binji]

Does this mean each block gets its own stack?

I wouldn't say that they get their own stacks, just that there is a limit to what can be popped. That's actually how it's implemented in wabt, there is a value stack and a "label" stack. Each label stores a "limit" which is the size of the value stack when the label is pushed. Then whenever you pop, you check against the top label's limit.

Executing a block or loop instruction has no effect on the value stack.

Maybe that should change to:

Executing a block or loop instruction has no effect on the value stack, but all stack values outside of the block executing block are inaccessible.

Or am I misunderstanding?

Yes, it's probably worth mentioning something like that in Semantics.md. Though I should mention that there is work on a formal prose spec as well.

[rossberg]

>

Does this mean each block gets its own stack?

I wouldn't say that they get their own stacks, just that there is a limit
to what can be popped. That's actually how it's implemented in wabt, there
is a value stack and a "label" stack. Each label stores a "limit" which is
the size of the value stack when the label is pushed. Then whenever you
pop, you check against the top label's limit.

Both are valid views. Semantically, the "block-local stack" view has the
advantage that it requires no extra invariants. With "single stack"
additional correctness assumptions are necessary, such as all limits
occurring in the label stack must be in bounds of the current operand stack
height, they must occur in (not necessarily strictly) increasing order, and
the label stack must never be empty.

[cretz]

Thanks for the info. I am closing this as there is nothing actionable to come from it and more formal specs are coming along to spell this out.