WebAssembly / spec

WebAssembly specification, reference interpreter, and test suite.
https://webassembly.github.io/spec/
Other
3.13k stars 445 forks source link

[spec] br_table has unspecified semantics for negative branch target #1570

Closed kazzmir closed 1 year ago

kazzmir commented 1 year ago
(module
  (func (export "test") 
    (block $default
      (block $1
        (block $2
          (br_table $1 $2 $default (i32.const -5))))))

  )

(assert_return (invoke "test"))

The spec says l* for the br_table instruction here is [$1 $2], with indices [0, 1], and l_N is $default. The two rules for br_table based on the value i, which is -5 here, are:

br l_i ;; if i < len(l*)
br l_N ;; otherwise

In this case, i < len(l*) is true since -5 < 2, which would mean the machine would try to lookup l*[-5], which is meaningless.

The reference spec interpreter seems use the $default label here, which suggests it requires that i >= 0 before the br l_i rule is invoked.

br l_i ;; if i >= 0 && i < len(l*)
kazzmir commented 1 year ago

Also just a minor thing I guess, but the spec uses a condition for the br l_i rule that is tautological in that l_i is defined to be the same as l*[i].

image

image

I guess the condition should be (if 0 <= i < |l*|)

kazzmir commented 1 year ago

Well I see why it works in the reference interpreter actually. It is because the interpreter uses I32.ge_u, so any negative number will most likely be larger than the length of the list of targets.

      | BrTable (xs, x), Num (I32 i) :: vs' ->
        if I32.ge_u i (Lib.List32.length xs) then
          vs', [Plain (Br x) @@ e.at]
        else
          vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at]
titzer commented 1 year ago

Yes, the input value to br_table is interpreted as a 32-bit unsigned int.

kazzmir commented 1 year ago

I agree, therefore the spec seems to not specify this.

rossberg commented 1 year ago

The abstract syntax for const is supposed to only allow positive numbers, and as noted in that section, all signed uses perform explicit reinterpretation via the signed meta operator.

However, there is indeed a bug there, because the AST grammar for const specifies iN instead of uN for integer immediates. Fixed in #1577.