WebAssembly：编译返回值不符合预期的循环

Question

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

下面的 sn-p（取自 WebAssembly loop test cases）显示了一个嵌套循环，预期返回一个 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

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

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

您可能会发现validation algorithm in the spec 很有用。我还写了关于 WebAssembly type-checking a while back 的文章，这可能对你很有帮助。