specification of labels for loops and exiting from blocks

[pepyakin]

I have some problems with the spec. Namely, spec states for the loop:

• Let L be the label whose arity is 0 and whose continuation is the start of the loop.

And then in the Blocks section, in Exiting inst* with Label L (I assume this explains how end works?) it states:

• Let n be the arity of L
• ...
• Pop the results valⁿ from the stack

But is it correct? I'm interpreting this as "loop..end block can't return any values, because when executing loop we pushing label with arity=0 and when we execute end we pop 0 values". Which seems incorrect for me (e.g. counter-example).

Could someone clarify this to me?

[rossberg]

Note that at step 6, the same values are pushed back, after the label (i.e., the inner block) has been popped. That is because operand and label stack are interleaved in the abstract machine.

[pepyakin]

But isn't n is 0 for labels that is pushed by loop, so no values are pushed and poped?
(I assume that valⁿ is denoting "n number of values")

[rossberg]

Ah, you are right, thanks, good catch! I ported this incorrectly from the paper. The number of values ought to be independent from the label's arity. See #609 for a fix.