WebAssembly:编译返回值未按预期运行的循环

Question

我正在编写一个WebAssembly字节码分析器，遇到了各种WebAssembly编译器如何处理循环指令的一些行为，我发现这些行为很难与WebAssembly规范相协调。

以下代码段(取自WebAssembly循环测试用例(显示了一个嵌套循环，该循环应返回i32整数。

(module
(type $t0 (func (result i32)))
(func $cont-inner (export "cont-inner") (type $t0) (result i32)
(local $l0 i32)
i32.const 0
local.set $l0
local.get $l0
loop $L0 (result i32)
loop $L1 (result i32)
br $L0
end
end
i32.add
local.set $l0

对以上内容的可视化分析表明，这种语法并不严格符合规范(据我所知(，因为循环的主体没有任何要返回的堆栈值。

当然，上面的循环形成了一个无限循环，因此在执行时程序实际上不会退出最外层的循环。

但我尝试过的一些编译器在编译时没有遇到任何问题，例如webassembly.studio。相反，如果用条件分支替换无条件分支，那么编译器实际上会像我预期的那样运行，并抱怨缺少返回值。

我是否在WebAssembly规范中遗漏了一些关于循环如何操作的内容？或者编译器是在隐式地进行可达性分析？

Answer 1

您观察到的是在无条件分支之后堆栈变得多态。这意味着堆栈的行为就像它具有验证所需的值一样。

在这种情况下，br $L0指令使堆栈具有多态性。通常情况下，从末尾loop $L1下降需要堆栈上的i32，但由于堆栈是多态的，类型检查器的行为就好像这是真的一样。

您可能会发现规范中的验证算法很有用。不久前我还写过关于WebAssembly类型检查的文章，这可能对您很有帮助。