Implement table and reference instructions (#553)

* implement spectest module * allow function IDs in assertTableElem * update unsupported conformance tests * implement table instructions * update tests * fix binary parser tests * add links * use hooked lists for reference lists in table and elem * fix unused variable * tableGet explicit requires * skip redundant checks in recursive table instrs * rename `RVal => RefVal` `RValType => RefValType` * fix typo
runtimeverification · Jan 12, 2024 · b66c403 · b66c403
1 parent b0801d9
commit b66c403
Show file tree

Hide file tree

Showing 15 changed files with 1,182 additions and 232 deletions.
diff --git a/auxil.md b/auxil.md
@@ -38,6 +38,8 @@ module WASM-AUXIL
            <mems>            _ => .Bag      </mems>
            <nextGlobAddr>    _ => 0         </nextGlobAddr>
            <globals>         _ => .Bag      </globals>
+           <nextElemAddr>    _ => 0         </nextElemAddr>
+           <elems>           _ => .Bag      </elems>
          </mainStore>
 
 endmodule

diff --git a/data.md b/data.md
@@ -80,15 +80,23 @@ It is used when initializing a WebAssembly table, or used as the parameter of th
 
 ### WebAssembly Types
 
-#### Base Types
-
-WebAssembly has four basic types, for 32 and 64 bit integers and floats.
+#### Value Types
 
+WebAssembly has three kinds of [Value types](https://webassembly.github.io/spec/core/syntax/types.html#value-types):
+  1. [Number types](https://webassembly.github.io/spec/core/syntax/types.html#number-types)
+  2. [Vector types](https://webassembly.github.io/spec/core/syntax/types.html#vector-types)(currently not supported)
+  3. [Reference types](https://webassembly.github.io/spec/core/syntax/types.html#reference-types)
+
 ```k
     syntax IValType ::= "i32" [klabel(i32), symbol] | "i64" [klabel(i64), symbol]
     syntax FValType ::= "f32" [klabel(f32), symbol] | "f64" [klabel(f64), symbol]
-    syntax ValType  ::= IValType | FValType
+    syntax RefValType ::= "funcref"     [klabel(funcref), symbol]
+                        | "externref"   [klabel(externref), symbol]
+    syntax ValType  ::= IValType | FValType | RefValType
  // ---------------------------------------
+
+    syntax HeapType ::= "func"   [klabel(func), symbol]
+                      | "extern" [klabel(extern), symbol]
 ```
 
 #### Type Constructors
@@ -158,10 +166,12 @@ module WASM-DATA-INTERNAL-SYNTAX
 Proper values are numbers annotated with their types.
 
 ```k
-    syntax IVal ::= "<" IValType ">" Int    [klabel(<_>_)]
-    syntax FVal ::= "<" FValType ">" Float  [klabel(<_>_)]
+    syntax IVal ::= "<" IValType ">" Int        [klabel(<_>_)]
+    syntax FVal ::= "<" FValType ">" Float      [klabel(<_>_)]
+    syntax RefVal ::= "<" RefValType ">" Int    [klabel(<_>_)]
+                    | "<" RefValType ">" "null" [klabel(<_>null), symbol]
     syntax  Val ::= "<"  ValType ">" Number [klabel(<_>_)]
-                  | IVal | FVal
+                  | IVal | FVal | RefVal
  // ---------------------------
 ```
 
@@ -243,10 +253,14 @@ In KWasm we store identifiers in maps from `Identifier` to `Int`, the `Int` bein
 This rule handles adding an `OptionalId` as a map key, but only when it is a proper identifier.
 
 ```k
-    syntax Map ::= #saveId (Map, OptionalId, Int) [function]
+    syntax Map  ::= #saveId    (Map, OptionalId, Int) [function, total]
+    syntax Bool ::= #canSaveId (Map, OptionalId)      [function, total]
  // -------------------------------------------------------
     rule #saveId (MAP, ID:OptionalId, _)   => MAP             requires notBool isIdentifier(ID)
     rule #saveId (MAP, ID:Identifier, IDX) => MAP [ID <- IDX]
+
+    rule #canSaveId (_,   ID:OptionalId) => true                     requires notBool isIdentifier(ID)
+    rule #canSaveId (MAP, ID:Identifier) => notBool ID in_keys(MAP)
 ```
 
 `Int` is the basic form of index, and indices always need to resolve to integers.
@@ -268,9 +282,9 @@ For `Int`, however, a the context is irrelevant and the index always just resolv
     syntax Ints ::= List{Int, ""} [klabel(listInt), symbol]
  // -------------------------------------------------------
 
-    syntax Int   ::= #lenElemSegment (ElemSegment)      [function]
+    syntax Int   ::= #lenElemSegment (ElemSegment)      [function, total]
     syntax Index ::= #getElemSegment (ElemSegment, Int) [function]
-    syntax Int   ::= #lenInts        (Ints)             [function]
+    syntax Int   ::= #lenInts        (Ints)             [function, total]
     syntax Int   ::= #getInts        (Ints,        Int) [function]
  // --------------------------------------------------------------
     rule #lenElemSegment(.ElemSegment) => 0
@@ -289,6 +303,7 @@ For `Int`, however, a the context is irrelevant and the index always just resolv
  // -----------------------------------------------------------
     rule elemSegment2Ints(.ElemSegment) => .Ints
     rule elemSegment2Ints(E:Int ES)     => E elemSegment2Ints(ES)
+
 ```
 
 ### Limits
@@ -477,9 +492,10 @@ Each call site _must_ ensure that this is desired behavior before using these fu
                       | #revs ( ValStack )            [function, total]
                       | #revs ( ValStack , ValStack ) [function, total, klabel(#revsAux)]
  // ------------------------------------------------------------------------------------------
-    rule #zero(.ValTypes)             => .ValStack
-    rule #zero(ITYPE:IValType VTYPES) => < ITYPE > 0   : #zero(VTYPES)
-    rule #zero(FTYPE:FValType VTYPES) => < FTYPE > 0.0 : #zero(VTYPES)
+    rule #zero(.ValTypes)               => .ValStack
+    rule #zero(ITYPE:IValType VTYPES)   => < ITYPE > 0    : #zero(VTYPES)
+    rule #zero(FTYPE:FValType VTYPES)   => < FTYPE > 0.0  : #zero(VTYPES)
+    rule #zero(RTYPE:RefValType VTYPES) => < RTYPE > null : #zero(VTYPES)
 
     rule #take(N, _)         => .ValStack               requires notBool N >Int 0
     rule #take(N, .ValStack) => .ValStack               requires         N >Int 0

diff --git a/data/list-ref.k b/data/list-ref.k
@@ -0,0 +1,89 @@
+
+
+module LIST-REF
+  import WASM-DATA-INTERNAL-SYNTAX
+  imports private INT-SYNTAX
+  imports private BASIC-K
+
+  syntax Int
+
+  syntax ListRef [hook(LIST.List)]
+  syntax ListRef ::= ListRef ListRef
+          [ left, function, total, hook(LIST.concat),
+            klabel(_ListRef_), symbol, smtlib(smt_seq_concat),
+            assoc, unit(.ListRef), element(ListRefItem),
+            format(%1%n%2)
+          ]
+  syntax ListRef ::= ".ListRef"
+          [ function, total, hook(LIST.unit), klabel(.ListRef),
+            symbol, smtlib(smt_seq_nil), latex(\dotCt{ListRef})
+          ]
+  syntax ListRef ::= ListItem(RefVal)
+          [ function, total, hook(LIST.element), klabel(ListRefItem),
+            symbol, smtlib(smt_seq_elem)
+          ]
+  syntax RefVal ::= ListRef "[" Int "]"
+          [ function, hook(LIST.get), klabel(ListRef:get), symbol ]
+  syntax ListRef ::= ListRef "[" index: Int "<-" value: RefVal "]"
+          [function, hook(LIST.update), symbol, klabel(ListRef:set)]
+  syntax ListRef ::= makeListRef(length: Int, value: RefVal)
+          [function, hook(LIST.make)]
+  syntax ListRef ::= updateList(dest: ListRef, index: Int, src: ListRef)
+          [function, hook(LIST.updateAll)]
+  syntax ListRef ::= fillList(ListRef, index: Int, length: Int, value: RefVal)
+          [function, hook(LIST.fill)]
+  syntax ListRef ::= range(ListRef, fromFront: Int, fromBack: Int)
+          [function, hook(LIST.range), klabel(ListRef:range), symbol]
+  syntax Bool ::= RefVal "in" ListRef
+          [function, total, hook(LIST.in), symbol, klabel(_inListRef_)]
+  syntax Int ::= size(ListRef)
+          [function, total, hook(LIST.size), symbol, klabel (sizeListRef), smtlib(smt_seq_len)]
+endmodule
+
+module LIST-REF-EXTENSIONS
+  imports LIST-REF
+  imports BOOL
+  imports INT
+
+  syntax RefVal ::= ListRef "[" Int "]" "orDefault" RefVal
+          [ function, total, klabel(ListRef:getOrDefault), symbol ]
+// ----------------------------------------------------------------
+  rule ListItem(V:RefVal) _:ListRef [0] orDefault _:RefVal
+      => V
+  rule _:ListRef ListItem(V:RefVal) [-1] orDefault _:RefVal
+      => V
+  rule .ListRef [_:Int] orDefault D:RefVal => D
+
+  rule ListItem(_:RefVal) L:ListRef [I:Int] orDefault D:RefVal
+      => L[I -Int 1] orDefault D
+    requires 0 <Int I
+  rule L:ListRef ListItem(_:RefVal) [I:Int] orDefault D:RefVal
+      => L[I +Int 1] orDefault D
+    requires I <Int 0
+
+  rule L:ListRef[I:Int] orDefault D:RefVal => D
+    requires notBool (0 -Int size(L) <=Int I andBool I <Int size(L))
+    [simplification]
+
+  syntax RefVal ::= getRefOrNull(ListRef, Int)
+          [ function, total, klabel(ListRef:getOrNull), symbol ]
+// -------------------------------------------------------------
+  rule getRefOrNull(L, N) => L [N] orDefault (<funcref> null)
+
+  syntax ListRef ::= makeListRefTotal(Int, RefVal)
+      [function, total, klabel(ListRef:makeTotal), symbol]
+// ----------------------------------------------------
+  rule makeListRefTotal(N, V) => makeListRef(N, V)
+    requires N >=Int 0
+  rule makeListRefTotal(N, _) => .ListRef
+    requires N <Int 0
+
+  syntax ListRef ::= dropListRef(Int, ListRef)
+      [function, total, klabel(ListRef:drop), symbol]
+// --------------------------------------------------------------
+  rule dropListRef(N, ListItem(_) L) => dropListRef(N -Int 1, L)
+    requires N >Int 0
+  rule dropListRef(_, L)             => L
+    [owise]
+
+endmodule
diff --git a/preprocessor.py b/preprocessor.py
@@ -17,6 +17,8 @@ def hex2float(h):
             return h.split()[0] + " " + "%e" % (float.fromhex(h.split()[1]))
         except OverflowError:
             return h
+        except ValueError as e:
+            return h
     else:
         return h
 

diff --git a/pykwasm/src/pykwasm/kwasm_ast.py b/pykwasm/src/pykwasm/kwasm_ast.py
@@ -29,6 +29,9 @@
 INTS = 'listInt'
 INTS_NIL = '.List{\"listInt\"}_Ints'
 
+REFS = '_ListRef_'
+REFS_NIL = '.ListRef'
+
 FUNC = 'aFuncDefn'
 FUNC_METADATA = 'funcMeta'
 
@@ -116,6 +119,18 @@ def ints(iis: Iterable[int]) -> KInner:
     return KNamedList(INTS, INTS_NIL, kis)
 
 
+def refs(values: Iterable[int | None]) -> KInner:
+    def idx_to_ref(idx: int | None) -> KInner:
+        if idx is None:
+            ref = KApply('<_>null', [funcref])
+        else:
+            # TODO find a readable symbol for RefVals
+            ref = KApply('<_>__WASM-DATA-INTERNAL-SYNTAX_RefVal_RefValType_Int', [funcref, KInt(idx)])
+        return KApply('ListRefItem', [ref])
+
+    return KNamedList(REFS, REFS_NIL, [idx_to_ref(i) for i in values])
+
+
 ###########
 # Empties #
 ###########
@@ -135,6 +150,8 @@ def ints(iis: Iterable[int]) -> KInner:
 i64 = KApply('i64', [])
 f32 = KApply('f32', [])
 f64 = KApply('f64', [])
+funcref = KApply('funcref', [])
+externref = KApply('externref', [])
 
 MUT_CONST = KApply('mutConst', [])
 MUT_VAR = KApply('mutVar', [])
@@ -204,7 +221,8 @@ def CALL(function_idx: int) -> KInner:
 
 
 def CALL_INDIRECT(type_idx: int) -> KInner:
-    return KApply('aCall_indirect', [KInt(type_idx)])
+    type_use = KApply('aTypeUseIndex', [KInt(type_idx)])
+    return KApply('aCall_indirect', [KInt(0), type_use])
 
 
 ##########################
@@ -566,8 +584,8 @@ def func(type: KInner, locals: KInner, body: KInner, metadata: KInner = EMPTY_FU
     return KApply(FUNC, [type, locals, body, metadata])
 
 
-def table(lim: tuple[int, int], metadata: KInner = EMPTY_ID) -> KInner:
-    return KApply(TABLE, [limits(lim), metadata])
+def table(lim: tuple[int, int], typ: KInner, metadata: KInner = EMPTY_ID) -> KInner:
+    return KApply(TABLE, [limits(lim), typ, metadata])
 
 
 def memory(lim: tuple[int, int], metadata: KInner = EMPTY_ID) -> KInner:
@@ -578,8 +596,13 @@ def glob(type: KInner, init: KInner, metadata: KInner = EMPTY_ID) -> KInner:
     return KApply(GLOBAL, [type, init, metadata])
 
 
-def elem(table_idx: int, offset: KInner, init: Iterable[int]) -> KInner:
-    return KApply(ELEM, [KInt(table_idx), offset, ints(init)])
+def elem_mode(table_idx: int, offset: KInner) -> KInner:
+    # TODO Implement other elem modes
+    return KApply('aElemActive', [KInt(table_idx), offset])
+
+
+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])
 
 
 def data(memory_idx: int, offset: KInner, data: bytes) -> KInner:

diff --git a/pykwasm/src/pykwasm/wasm2kast.py b/pykwasm/src/pykwasm/wasm2kast.py
@@ -27,6 +27,7 @@
     TableType,
     TypeIdx,
     ValType,
+    addresses,
 )
 from wasm.opcodes import BinaryOpcode
 from wasm.parsers import parse_module
@@ -97,7 +98,11 @@ def func(f: Function):
 
 def table(t: Table):
     ls = limits(t.type.limits)
-    return a.table(ls)
+    if isinstance(t.type.elem_type, addresses.FunctionAddress):
+        typ = a.funcref
+    else:
+        typ = a.externref
+    return a.table(ls, typ)
 
 
 def memory(m: Memory):
@@ -113,7 +118,8 @@ def glob(g: Global):
 
 def elem(e: ElementSegment):
     offset = instrs(e.offset)
-    return a.elem(e.table_idx, offset, e.init)
+    elem_mode = a.elem_mode(e.table_idx, offset)
+    return a.elem(a.funcref, elem_mode, e.init)
 
 
 def data(d: DataSegment):