search

runtimeverification / wasm-semantics

A Prototype Formal Semantics of WebAssembly in K
Other
74 stars 18 forks source link

Allow optional table indices #661

Closed gtrepta closed 2 days ago

gtrepta commented 1 week ago

https://github.com/WebAssembly/spec/commit/6798f054ad1b0493919f0b5244fa46682ccd3e69 introduces tests that exercise optional table indices. Currently these cause our parser to fail.

Example of a change that breaks:

diff --git a/test/core/table_get.wast b/test/core/table_get.wast
index 5d57c319..0dedb19f 100644
--- a/test/core/table_get.wast
+++ b/test/core/table_get.wast
@@ -10,7 +10,7 @@
   )

   (func (export "get-externref") (param $i i32) (result externref)
-    (table.get $t2 (local.get $i))
+    (table.get (local.get $i))
   )
   (func $f3 (export "get-funcref") (param $i i32) (result funcref)
     (table.get $t3 (local.get $i))