Merge branch 'funcref'

Author: rossberg

document/core/exec/instructions.rst

@@ -1836,31 +1836,31 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 1. Assert: due to :ref:`validation <valid-vec-replace_lane>`, :math:`x < \dim(\shape)`.
 
-2. Let :math:`t_1` be the type :math:`\unpacked(\shape)`.
+2. Let :math:`t_2` be the type :math:`\unpacked(\shape)`.
 
 3. Assert: due to :ref:`validation <valid-vec-replace_lane>`, a value of :ref:`value type <syntax-valtype>` :math:`t_1` is on the top of the stack.
 
-4. Pop the value :math:`t_1.\CONST~c_1` from the stack.
+4. Pop the value :math:`t_2.\CONST~c_2` from the stack.
 
 5. Assert: due to :ref:`validation <valid-vec-replace_lane>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
 
-6. Pop the value :math:`\V128.\VCONST~c_2` from the stack.
+6. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
 
-7. Let :math:`i^\ast` be the result of computing :math:`\lanes_{\shape}(c_2)`.
+7. Let :math:`i^\ast` be the result of computing :math:`\lanes_{\shape}(c_1)`.
 
-8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\shape}(i^\ast \with [x] = c_1)`.
+8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\shape}(i^\ast \with [x] = c_2)`.
 
 9. Push :math:`\V128.\VCONST~c` on the stack.
 
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   (t_1\K{.}\CONST~c_1)~(\V128\K{.}\VCONST~c_2)~(\shape\K{.}\REPLACELANE~x) &\stepto& (\V128\K{.}\VCONST~c)
+   (\V128\K{.}\VCONST~c_1)~(t_2\K{.}\CONST~c_2)~(\shape\K{.}\REPLACELANE~x) &\stepto& (\V128\K{.}\VCONST~c)
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-      (\iff & i^\ast = \lanes_{\shape}(c_2) \\
-       \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_1))
+      (\iff & i^\ast = \lanes_{\shape}(c_1) \\
+       \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_2))
      \end{array}
    \end{array}
 
@@ -1992,9 +1992,9 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 1. Assert: due to :ref:`validation <valid-vtestop>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
 
-2. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
+2. Pop the value :math:`\V128.\VCONST~c` from the stack.
 
-3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c_1)`.
+3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c)`.
 
 4. Let :math:`i` be the result of computing :math:`\tobool(\bigwedge(i_1 \neq 0)^\ast)`.
 
@@ -2004,7 +2004,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i)
+   (\V128\K{.}\VCONST~c)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i)
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
@@ -2021,7 +2021,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 1. Assert: due to :ref:`validation <valid-vec-bitmask>`, a value of :ref:`value type <syntax-valtype>` |V128| is on the top of the stack.
 
-2. Pop the value :math:`\V128.\VCONST~c_1` from the stack.
+2. Pop the value :math:`\V128.\VCONST~c` from the stack.
 
 3. Let :math:`i_1^N` be the result of computing :math:`\lanes_{t\K{x}N}(c)`.
 
@@ -2031,14 +2031,14 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 6. Let :math:`j^\ast` be the concatenation of the two sequences :math:`i_2^N` and :math:`0^{32-N}`.
 
-7. Let :math:`c` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`.
+7. Let :math:`i` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`.
 
-8. Push the value :math:`\I32.\CONST~c` onto the stack.
+8. Push the value :math:`\I32.\CONST~i` onto the stack.
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~c)
-     & (\iff c = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N)))
+   (\V128\K{.}\VCONST~c)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~i)
+     & (\iff i = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N)))
      \\
    \end{array}
 
@@ -2160,8 +2160,8 @@ where:
    \end{array}
 
 
-:math:`t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx\K{\_zero}`
-...............................................................
+:math:`t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx^?\K{\_zero}`
+.................................................................
 
 1. Assert: due to :ref:`syntax <syntax-instr-vec>`, :math:`N = 2 \cdot M`.
 
@@ -2171,7 +2171,7 @@ where:
 
 4. Let :math:`i^\ast` be the result of computing :math:`\lanes_{t_1\K{x}M}(c_1)`.
 
-5. Let :math:`j^\ast` be the result of computing :math:`\vcvtop^{\sx}_{|t_1|,|t_2|}(i^\ast)`.
+5. Let :math:`j^\ast` be the result of computing :math:`\vcvtop^{\sx^?}_{|t_1|,|t_2|}(i^\ast)`.
 
 6. Let :math:`k^\ast` be the concatenation of the two sequences :math:`j^\ast` and :math:`0^M`.
 
@@ -2182,11 +2182,11 @@ where:
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx\K{\_zero} &\stepto& (\V128\K{.}\VCONST~c) \\
+   (\V128\K{.}\VCONST~c_1)~t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx^?\K{\_zero} &\stepto& (\V128\K{.}\VCONST~c) \\
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-     (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M))
+     (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx^?}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M))
      \end{array}
    \end{array}
 
@@ -2265,7 +2265,7 @@ where:
 
 10. Let :math:`k_2^\ast` be the result of computing :math:`\extend^{\sx}_{|t_1|,|t_2|}(j_2^\ast)`.
 
-11. Let :math:`k^\ast` be the result of computing :math:`\imul_{t_2\K{x}N}(k_1^\ast, k_2^\ast)`.
+11. Let :math:`k^\ast` be the result of computing :math:`\imul_{|t_2|}(k_1^\ast, k_2^\ast)`.
 
 12. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{t_2\K{x}N}(k^\ast)`.
 
@@ -2279,7 +2279,7 @@ where:
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & i^\ast = \lanes_{t_1\K{x}M}(c_1)[\half(0, N) \slice N] \\
      \wedge & j^\ast = \lanes_{t_1\K{x}M}(c_2)[\half(0, N) \slice N] \\
-     \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{t_2\K{x}N}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast))))
+     \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{|t_2|}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast))))
      \end{array}
 
 where:
@@ -2306,7 +2306,7 @@ where:
 
 5. Let :math:`(j_1~j_2)^\ast` be the result of computing :math:`\extend^{\sx}_{|t_1|,|t_2|}(i^\ast)`.
 
-6. Let :math:`k^\ast` be the result of computing :math:`\iadd_{N}(j_1, j_2)^\ast`.
+6. Let :math:`k^\ast` be the result of computing :math:`\iadd_{|t_2|}(j_1, j_2)^\ast`.
 
 7. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{t_2\K{x}N}(k^\ast)`.
 
@@ -2320,7 +2320,7 @@ where:
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
      (\iff & (i_1~i_2)^\ast = \extend^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1)) \\
-     \wedge & j^\ast = \iadd_{N}(i_1, i_2)^\ast \\
+     \wedge & j^\ast = \iadd_{|t_2|}(i_1, i_2)^\ast \\
      \wedge & c = \lanes^{-1}_{t_2\K{x}N}(j^\ast))
      \end{array}
    \end{array}

document/core/valid/instructions.rst

@@ -1972,9 +1972,9 @@ Control Instructions
 ...........................
 
 
-* The label :math:`C.\CLABELS[l_N]` must be defined in the context.
+* The :ref:`label <syntax-label>` :math:`C.\CLABELS[l_N]` must be defined in the context.
 
-* For all :math:`l_i` in :math:`l^\ast`,
+* For each :ref:`label <syntax-label>` :math:`l_i` in :math:`l^\ast`,
   the label :math:`C.\CLABELS[l_i]` must be defined in the context.
 
 * There must be a sequence :math:`t^\ast` of :ref:`value types <syntax-valtype>`, such that:

interpreter/dune

@@ -6,7 +6,8 @@
  ; Wasm REPL every time in all the dependencies.
  ; We exclude the 'wast' module as it is only used for the JS build.
  ; 'smallint' is a separate test module.
- (modules :standard \ main wasm smallint wast))
+ (modules :standard \ main wasm smallint wast)
+ (libraries menhirLib))
 
 (executable
  (public_name wasm)
@@ -43,7 +44,7 @@
    (chdir
     %{workspace_root}
     (run %{bin:ocamllex} -ml -q -o %{target} %{deps}))))
- (ocamlyacc
+ (menhir
   (modules parser)))
 
 (env

interpreter/dune-project

@@ -3,11 +3,11 @@
 (name wasm)
 
 (generate_opam_files true)
+(using menhir 2.1)
+(implicit_transitive_deps false)
 
 (license Apache-2.0)
-
-(source
-  (github WebAssembly/spec))
+(source (github WebAssembly/spec))
 
 (authors "Andreas Rossberg <rossberg@mpi-sws.org")
 (maintainers "Andreas Rossberg <rossberg@mpi-sws.org")
@@ -17,4 +17,7 @@
   (synopsis "Library to read and write WebAssembly (Wasm) files and manipulate their AST")
   (tags (wasm webassembly spec interpreter))
   (depends
-    (ocaml (>= 4.12))))
+    (ocaml (>= 4.12))
+    (menhir (>= 20220210))
+  )
+)

interpreter/jslib/wast.ml

@@ -4,12 +4,12 @@
 open Wasm
 open Js_of_ocaml
 
-let _ =
+let () =
   Js.export "WebAssemblyText"
     (object%js (_self)
 
       method encode (s : Js.js_string Js.t) : (Typed_array.arrayBuffer Js.t) =
-        let def = Parse.string_to_definition (Js.to_string s) in
+        let _, def = Parse.Module.parse_string (Js.to_string s) in
         let bs =
           match def.Source.it with
           | Script.Textual m -> Encode.encode m

interpreter/script/js.ml

@@ -33,8 +33,8 @@ let spectest = {
   print_f64: console.log.bind(console),
   global_i32: 666,
   global_i64: 666n,
-  global_f32: 666,
-  global_f64: 666,
+  global_f32: 666.6,
+  global_f64: 666.6,
   table: new WebAssembly.Table({initial: 10, maximum: 20, element: 'anyfunc'}),
   memory: new WebAssembly.Memory({initial: 1, maximum: 2})
 };
@@ -530,7 +530,8 @@ let rec of_definition def =
   | Textual m -> of_bytes (Encode.encode m)
   | Encoded (_, bs) -> of_bytes bs
   | Quoted (_, s) ->
-    try of_definition (Parse.string_to_definition s) with Parse.Syntax _ ->
+    try of_definition (snd (Parse.Module.parse_string s))
+    with Parse.Syntax _ ->
       of_bytes "<malformed quote>"
 
 let of_wrapper mods x_opt name wrap_action wrap_assertion at =
@@ -601,7 +602,7 @@ let of_command mods cmd =
       match def.it with
       | Textual m -> m
       | Encoded (_, bs) -> Decode.decode "binary" bs
-      | Quoted (_, s) -> unquote (Parse.string_to_definition s)
+      | Quoted (_, s) -> unquote (snd (Parse.Module.parse_string s))
     in bind mods x_opt (unquote def);
     "let " ^ current_var mods ^ " = instance(" ^ of_definition def ^ ");\n" ^
     (if x_opt = None then "" else

interpreter/script/run.ml

@@ -118,17 +118,20 @@ let input_from get_script run =
   | Assert (at, msg) -> error at "assertion failure" msg
   | Abort _ -> false
 
-let input_script start name lexbuf run =
-  input_from (fun _ -> Parse.parse name lexbuf start) run
+let input_script name lexbuf run =
+  input_from (fun () -> Parse.Script.parse name lexbuf) run
+
+let input_script1 name lexbuf run =
+  input_from (fun () -> Parse.Script1.parse name lexbuf) run
 
 let input_sexpr name lexbuf run =
-  input_from (fun _ ->
-    let var_opt, def = Parse.parse name lexbuf Parse.Module in
+  input_from (fun () ->
+    let var_opt, def = Parse.Module.parse name lexbuf in
     [Module (var_opt, def) @@ no_region]) run
 
 let input_binary name buf run =
   let open Source in
-  input_from (fun _ ->
+  input_from (fun () ->
     [Module (None, Encoded (name, buf) @@ no_region) @@ no_region]) run
 
 let input_sexpr_file input file run =
@@ -162,16 +165,16 @@ let input_file file run =
   dispatch_file_ext
     input_binary_file
     (input_sexpr_file input_sexpr)
-    (input_sexpr_file (input_script Parse.Script))
-    (input_sexpr_file (input_script Parse.Script))
+    (input_sexpr_file input_script)
+    (input_sexpr_file input_script)
     input_js_file
     file run
 
 let input_string string run =
   trace ("Running (\"" ^ String.escaped string ^ "\")...");
   let lexbuf = Lexing.from_string string in
   trace "Parsing...";
-  input_script Parse.Script "string" lexbuf run
+  input_script "string" lexbuf run
 
 
 (* Interactive *)
@@ -195,7 +198,7 @@ let lexbuf_stdin buf len =
 let input_stdin run =
   let lexbuf = Lexing.from_function lexbuf_stdin in
   let rec loop () =
-    let success = input_script Parse.Script1 "stdin" lexbuf run in
+    let success = input_script1 "stdin" lexbuf run in
     if not success then Lexing.flush_input lexbuf;
     if Lexing.(lexbuf.lex_curr_pos >= lexbuf.lex_buffer_len - 1) then
       continuing := false;
@@ -315,7 +318,7 @@ let rec run_definition def : Ast.module_ =
     Decode.decode name bs
   | Quoted (_, s) ->
     trace "Parsing quote...";
-    let def' = Parse.string_to_definition s in
+    let _, def' = Parse.Module.parse_string s in
     run_definition def'
 
 let run_action act : Value.t list =

interpreter/script/script.ml

@@ -64,8 +64,6 @@ and meta' =
 
 and script = command list
 
-exception Syntax of Source.region * string
-
 
 let () =
   let type_of_ref' = !Value.type_of_ref' in

interpreter/text/arrange.ml

@@ -766,14 +766,14 @@ let definition mode x_opt def =
         match def.it with
         | Textual m -> m
         | Encoded (_, bs) -> Decode.decode "" bs
-        | Quoted (_, s) -> unquote (Parse.string_to_definition s)
+        | Quoted (_, s) -> unquote (snd (Parse.Module.parse_string s))
       in module_with_var_opt x_opt (unquote def)
     | `Binary ->
       let rec unquote def =
         match def.it with
         | Textual m -> Encode.encode m
         | Encoded (_, bs) -> Encode.encode (Decode.decode "" bs)
-        | Quoted (_, s) -> unquote (Parse.string_to_definition s)
+        | Quoted (_, s) -> unquote (snd (Parse.Module.parse_string s))
       in binary_module_with_var_opt x_opt (unquote def)
     | `Original ->
       match def.it with

interpreter/text/lexer.mll

@@ -14,7 +14,7 @@ let region lexbuf =
   let right = convert_pos (Lexing.lexeme_end_p lexbuf) in
   {left = left; right = right}
 
-let error lexbuf msg = raise (Script.Syntax (region lexbuf, msg))
+let error lexbuf msg = raise (Parse_error.Syntax (region lexbuf, msg))
 let error_nest start lexbuf msg =
   lexbuf.Lexing.lex_start_p <- start;
   error lexbuf msg