Update py-wasm and binary parser (#562)

* update py-wasm

* suppress 'function 1 is not declared in any elem sections'

pykwasm/pyproject.toml

@@ -15,7 +15,7 @@ python = "^3.10"
 cytoolz = "^0.12.1"
 numpy = "^1.24.2"
 pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.572" }
-py-wasm = {url = "https://github.com/runtimeverification/py-wasm/archive/refs/tags/0.1.1.tar.gz"}
+py-wasm = {url = "https://github.com/runtimeverification/py-wasm/archive/refs/tags/0.2.0.tar.gz"}
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

pykwasm/src/pykwasm/kwasm_ast.py

@@ -225,6 +225,59 @@ def CALL_INDIRECT(type_idx: int) -> KInner:
     return KApply('aCall_indirect', [KInt(0), type_use])
 
 
+##########################
+# Reference Instructions #
+##########################
+
+
+def REF_FUNC(func_idx: int) -> KInner:
+    return KApply('aRef.func', [KInt(func_idx)])
+
+
+REF_IS_NULL: KInner = KApply('aRef.is_null', [])
+
+
+def REF_NULL(t: str) -> KInner:
+    return KApply('aRef.null', [KApply(t, [])])
+
+
+##########################
+# Table Instructions #
+##########################
+
+
+def TABLE_GET(table_idx: int) -> KInner:
+    return KApply('aTable.get', [KInt(table_idx)])
+
+
+def TABLE_SET(table_idx: int) -> KInner:
+    return KApply('aTable.set', [KInt(table_idx)])
+
+
+def TABLE_INIT(table_idx: int, elem_idx: int) -> KInner:
+    return KApply('aTable.init', [KInt(table_idx), KInt(elem_idx)])
+
+
+def ELEM_DROP(elem_idx: int) -> KInner:
+    return KApply('aElem.drop', [KInt(elem_idx)])
+
+
+def TABLE_COPY(table_idx1: int, table_idx2: int) -> KInner:
+    return KApply('aTable.copy', [KInt(table_idx1), KInt(table_idx2)])
+
+
+def TABLE_GROW(table_idx: int) -> KInner:
+    return KApply('aTable.grow', [KInt(table_idx)])
+
+
+def TABLE_SIZE(table_idx: int) -> KInner:
+    return KApply('aTable.size', [KInt(table_idx)])
+
+
+def TABLE_FILL(table_idx: int) -> KInner:
+    return KApply('aTable.fill', [KInt(table_idx)])
+
+
 ##########################
 # Parametric Instruction #
 ##########################
@@ -596,11 +649,18 @@ def glob(type: KInner, init: KInner, metadata: KInner = EMPTY_ID) -> KInner:
     return KApply(GLOBAL, [type, init, metadata])
 
 
-def elem_mode(table_idx: int, offset: KInner) -> KInner:
-    # TODO Implement other elem modes
+def elem_active(table_idx: int, offset: KInner) -> KInner:
     return KApply('aElemActive', [KInt(table_idx), offset])
 
 
+def elem_declarative() -> KInner:
+    return KApply('aElemDeclarative', [])
+
+
+def elem_passive() -> KInner:
+    return KApply('aElemPassive', [])
+
+
 def elem(typ: KInner, elem_mode: KInner, init: Iterable[int | None], metadata: KInner = EMPTY_ID) -> KInner:
     return KApply(ELEM, [typ, refs(init), elem_mode, metadata])
 

pykwasm/src/pykwasm/wasm2kast.py

@@ -8,6 +8,7 @@
 from typing import IO, Iterable
 
 from pyk.kast.inner import KInner
+from wasm import instructions
 from wasm.datatypes import (
     DataSegment,
     ElementSegment,
@@ -22,13 +23,16 @@
     MemoryType,
     Module,
     Mutability,
+    RefType,
     StartFunction,
     Table,
     TableType,
     TypeIdx,
     ValType,
     addresses,
 )
+from wasm.datatypes.element_segment import ElemMode, ElemModeActive, ElemModeDeclarative, ElemModePassive
+from wasm.instructions import BaseInstruction
 from wasm.opcodes import BinaryOpcode
 from wasm.parsers import parse_module
 
@@ -116,10 +120,43 @@ def glob(g: Global):
     return a.glob(t, init)
 
 
+def ref_type(t: RefType):
+    if t is addresses.FunctionAddress:
+        return a.funcref
+    return a.externref
+
+
+def elem_mode(m: ElemMode) -> KInner:
+    if isinstance(m, ElemModeActive):
+        offset = instrs(m.offset)
+        return a.elem_active(m.table, offset)
+    if isinstance(m, ElemModeDeclarative):
+        return a.elem_declarative()
+    if isinstance(m, ElemModePassive):
+        return a.elem_passive()
+    raise ValueError(f'Unknown ElemMode: {m}')
+
+
+def elem_init(init: tuple[Iterable[BaseInstruction], ...]) -> Iterable[int | None]:
+    def expr_to_int(expr: Iterable[BaseInstruction]) -> int | None:
+        # 'expr' must be a constant expression consisting of a reference instruction
+        assert len(expr) == 1 or len(expr) == 2 and isinstance(expr[1], instructions.End), expr
+        instr = expr[0]
+
+        if isinstance(instr, instructions.RefFunc):
+            return instr.funcidx
+        if isinstance(instr, instructions.RefNull):
+            return None
+        raise ValueError(f'Invalid reference expression: {expr}')
+
+    return [expr_to_int(e) for e in init]
+
+
 def elem(e: ElementSegment):
-    offset = instrs(e.offset)
-    elem_mode = a.elem_mode(e.table_idx, offset)
-    return a.elem(a.funcref, elem_mode, e.init)
+    typ = ref_type(e.type)
+    mode = elem_mode(e.mode)
+    init = elem_init(e.init)
+    return a.elem(typ, mode, init)
 
 
 def data(d: DataSegment):
@@ -173,6 +210,7 @@ def instrs(iis):
 def instr(i):
     B = BinaryOpcode
     global block_id
+    # TODO rewrite 'i.opcode == _' conditions as isinstance for better type-checking
     if i.opcode == B.BLOCK:
         cur_block_id = block_id
         block_id += 1
@@ -278,6 +316,31 @@ def instr(i):
         return a.SET_LOCAL(i.local_idx)
     if i.opcode == B.TEE_LOCAL:
         return a.TEE_LOCAL(i.local_idx)
+    if isinstance(i, instructions.RefFunc):
+        return a.REF_FUNC(i.funcidx)
+    if isinstance(i, instructions.RefNull):
+        if i.reftype is addresses.FunctionAddress:
+            return a.REF_NULL('func')
+        if i.reftype is addresses.ExternAddress:
+            return a.REF_NULL('extern')
+        raise ValueError(f'Unknown heap type: {i}, {i.reftype}')
+    if isinstance(i, instructions.TableGet):
+        return a.TABLE_GET(i.tableidx)
+    if isinstance(i, instructions.TableSet):
+        return a.TABLE_SET(i.tableidx)
+    if isinstance(i, instructions.TableInit):
+        return a.TABLE_INIT(i.tableidx, i.elemidx)
+    if isinstance(i, instructions.ElemDrop):
+        return a.ELEM_DROP(i.elemidx)
+    if isinstance(i, instructions.TableCopy):
+        return a.TABLE_COPY(i.tableidx1, i.tableidx2)
+    if isinstance(i, instructions.TableGrow):
+        return a.TABLE_GROW(i.tableidx)
+    if isinstance(i, instructions.TableSize):
+        return a.TABLE_SIZE(i.tableidx)
+    if isinstance(i, instructions.TableFill):
+        return a.TABLE_FILL(i.tableidx)
+
     # Catch all for operations without direct arguments.
     return eval('a.' + i.opcode.name)
 
@@ -296,6 +359,11 @@ def val_type(t: ValType):
         return a.f32
     if t == ValType.f64:
         return a.f64
+    if t == ValType.externref:
+        return a.externref
+    if t == ValType.funcref:
+        return a.funcref
+    raise ValueError(f'Unknown value type: {t}')
 
 
 def vec_type(ts: Iterable[ValType]):

pykwasm/src/tests/integration/binary/instrs.wat

@@ -1,8 +1,11 @@
 (module
   (memory 0)
   (table 100 funcref)
+  (elem func $f)
   (global (mut i32) (i32.const 0))
   (func (param i32 i64) (local f64))
+  (func $f)
+  (global funcref (ref.func $f))
   (func (local i32)
         ;; `unreachable` and `drop` are inserted as needed to
         ;; ensure correct typing.
@@ -171,6 +174,25 @@
         call 0
         call_indirect (type 0)
         ;; --
+
+        ;; Reference Instrs
+        ref.is_null      drop
+        ref.null extern  drop
+        ref.null func    drop
+        ref.func $f      drop
+        ;; --
+
+        ;; Table Instrs
+        table.get 0      drop
+        table.set 0      drop
+        table.init 0 0   drop
+        elem.drop 0      drop
+        table.copy 0 0   drop
+        table.grow 0     drop
+        table.size 0     drop
+        table.fill 0     drop
+        ;; --
+
         unreachable
     )
 

pykwasm/src/tests/integration/binary/spec_elem_0.wat

@@ -0,0 +1,75 @@
+;; Syntax
+(module
+  (table $t 10 funcref)
+  (func $f)
+  (func $g)
+
+  ;; Passive
+  (elem funcref)
+  (elem funcref (ref.func $f) (item ref.func $f) (item (ref.null func)) (ref.func $g))
+  (elem func)
+  (elem func $f $f $g $g)
+
+  (elem $p1 funcref)
+  (elem $p2 funcref (ref.func $f) (ref.func $f) (ref.null func) (ref.func $g))
+  (elem $p3 func)
+  (elem $p4 func $f $f $g $g)
+
+  ;; Active
+  (elem (table $t) (i32.const 0) funcref)
+  (elem (table $t) (i32.const 0) funcref (ref.func $f) (ref.null func))
+  (elem (table $t) (i32.const 0) func)
+  (elem (table $t) (i32.const 0) func $f $g)
+  (elem (table $t) (offset (i32.const 0)) funcref)
+  (elem (table $t) (offset (i32.const 0)) func $f $g)
+  (elem (table 0) (i32.const 0) func)
+  (elem (table 0x0) (i32.const 0) func $f $f)
+  (elem (table 0x000) (offset (i32.const 0)) func)
+  (elem (table 0) (offset (i32.const 0)) func $f $f)
+  (elem (table $t) (i32.const 0) func)
+  (elem (table $t) (i32.const 0) func $f $f)
+  (elem (table $t) (offset (i32.const 0)) func)
+  (elem (table $t) (offset (i32.const 0)) func $f $f)
+  (elem (offset (i32.const 0)))
+  (elem (offset (i32.const 0)) funcref (ref.func $f) (ref.null func))
+  (elem (offset (i32.const 0)) func $f $f)
+  (elem (offset (i32.const 0)) $f $f)
+  (elem (i32.const 0))
+  (elem (i32.const 0) funcref (ref.func $f) (ref.null func))
+  (elem (i32.const 0) func $f $f)
+  (elem (i32.const 0) $f $f)
+
+  (elem $a1 (table $t) (i32.const 0) funcref)
+  (elem $a2 (table $t) (i32.const 0) funcref (ref.func $f) (ref.null func))
+  (elem $a3 (table $t) (i32.const 0) func)
+  (elem $a4 (table $t) (i32.const 0) func $f $g)
+  (elem $a9 (table $t) (offset (i32.const 0)) funcref)
+  (elem $a10 (table $t) (offset (i32.const 0)) func $f $g)
+  (elem $a11 (table 0) (i32.const 0) func)
+  (elem $a12 (table 0x0) (i32.const 0) func $f $f)
+  (elem $a13 (table 0x000) (offset (i32.const 0)) func)
+  (elem $a14 (table 0) (offset (i32.const 0)) func $f $f)
+  (elem $a15 (table $t) (i32.const 0) func)
+  (elem $a16 (table $t) (i32.const 0) func $f $f)
+  (elem $a17 (table $t) (offset (i32.const 0)) func)
+  (elem $a18 (table $t) (offset (i32.const 0)) func $f $f)
+  (elem $a19 (offset (i32.const 0)))
+  (elem $a20 (offset (i32.const 0)) funcref (ref.func $f) (ref.null func))
+  (elem $a21 (offset (i32.const 0)) func $f $f)
+  (elem $a22 (offset (i32.const 0)) $f $f)
+  (elem $a23 (i32.const 0))
+  (elem $a24 (i32.const 0) funcref (ref.func $f) (ref.null func))
+  (elem $a25 (i32.const 0) func $f $f)
+  (elem $a26 (i32.const 0) $f $f)
+
+  ;; Declarative
+  (elem declare funcref)
+  (elem declare funcref (ref.func $f) (ref.func $f) (ref.null func) (ref.func $g))
+  (elem declare func)
+  (elem declare func $f $f $g $g)
+
+  (elem $d1 declare funcref)
+  (elem $d2 declare funcref (ref.func $f) (ref.func $f) (ref.null func) (ref.func $g))
+  (elem $d3 declare func)
+  (elem $d4 declare func $f $f $g $g)
+)

pykwasm/src/tests/integration/binary/spec_elem_1.wat

@@ -0,0 +1,14 @@
+(module
+  (type $out-i32 (func (result i32)))
+  (table 10 funcref)
+  (elem (i32.const 7) $const-i32-a)
+  (elem (i32.const 9) $const-i32-b)
+  (func $const-i32-a (type $out-i32) (i32.const 65))
+  (func $const-i32-b (type $out-i32) (i32.const 66))
+  (func (export "call-7") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 7))
+  )
+  (func (export "call-9") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 9))
+  )
+)

pykwasm/src/tests/integration/binary/spec_elem_2.wat

@@ -0,0 +1,17 @@
+(module $module1
+  (type $out-i32 (func (result i32)))
+  (table (export "shared-table") 10 funcref)
+  (elem (i32.const 8) $const-i32-a)
+  (elem (i32.const 9) $const-i32-b)
+  (func $const-i32-a (type $out-i32) (i32.const 65))
+  (func $const-i32-b (type $out-i32) (i32.const 66))
+  (func (export "call-7") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 7))
+  )
+  (func (export "call-8") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 8))
+  )
+  (func (export "call-9") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 9))
+  )
+)

wasm.md

@@ -78,7 +78,7 @@ The sorts `EmptyStmt` and `EmptyStmts` are administrative so that the empty list
 ```k
     syntax PlainInstr ::= IValType "." "const" WasmInt    [klabel(aIConst), symbol]
                         | FValType "." "const" Number     [klabel(aFConst), symbol]
-                        | "ref.null" HeapType             [klabel(aRefNull), symbol]
+                        | "ref.null" HeapType             [klabel(aRef.null), symbol]
                         | IValType "." IUnOp              [klabel(aIUnOp), symbol]
                         | FValType "." FUnOp              [klabel(aFUnOp), symbol]
                         | IValType "." ExtendS            [klabel(aExtendS), symbol] // TODO this is more permissive than the official spec as it allows 'i32.extend32_s'