Merge branch 'funcref'

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 <[email protected]")
 (maintainers "Andreas Rossberg <[email protected]")
@@ -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