Validation Algorithm in Appendix doesn't specify what unreachable() should do if the control stack is empty

[MarkDerosier]

Reading how typechecking works it appears that pushing an unreachable control frame to the stack would allow the algorithm to work, but I am uncertain. Explicitly documenting how this edge case should be handled would be appreciated.

[conrad-watt]

During validation it's an invariant that the control stack will always be non-empty when unreachable is encountered, because functions implicitly define an outer label that's in scope for the whole function body.

The algorithm in the appendix specifically seems a tiny bit inconsistent here. In particular the pop_ctrl() helper used to validate end has an error_if(ctrls.is_empty()) check which is strictly-speaking redundant for the same reason, and validating a spurious end that's not the closing bracket of a block\loop\if appears to allow the outer (function-level) control stack entry to be popped (although there may be an implicit assumption that bracketing of end has already been checked at decode-time).

The quickest way to make things consistent might be for us to move the error_if(ctrls.is_empty()) check in pop_ctrl() to the end of the helper, to ensure that unpaired end causes an error, and document via a note that it's an invariant that the control stack is non-empty throughout.

[rossberg]

Good catch.

Not sure if moving the check in pop_ctrl is the ideal solution, though. A more complete validator based on this code would likely want to use push/pop_ctrl for the function's outermost block as well, which would then fail.

The simpler fix may be to add a non-empty check to unreachable.

[rossberg]

Closing via #1498.