diff --git a/auxil.md b/auxil.md index 10f77f999..eaf242300 100644 --- a/auxil.md +++ b/auxil.md @@ -38,6 +38,8 @@ module WASM-AUXIL _ => .Bag _ => 0 _ => .Bag + _ => 0 + _ => .Bag endmodule diff --git a/data.md b/data.md index 5592aa97c..a60554842 100644 --- 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 new file mode 100644 index 000000000..fb920ba4d --- /dev/null +++ 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 L[I +Int 1] orDefault D + requires I D + requires notBool (0 -Int size(L) <=Int I andBool I L [N] orDefault ( 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 dropListRef(N -Int 1, L) + requires N >Int 0 + rule dropListRef(_, L) => L + [owise] + +endmodule \ No newline at end of file diff --git a/preprocessor.py b/preprocessor.py index a2ef63dec..d75820fce 100644 --- 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 index 0471e06de..8392fc58e 100644 --- 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 index 5d6dea2ae..46cd24741 100644 --- 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): diff --git a/test.md b/test.md index a13c9ab4a..2ac1dc30e 100644 --- a/test.md +++ b/test.md @@ -23,9 +23,7 @@ module WASM-TEST-COMMON-SYNTAX imports WASM-AUXIL-SYNTAX imports WASM-REFERENCE-INTERPRETER-SYNTAX - syntax Assertion ::= "#assertAndRemoveEqual" - | "#assertAndRemoveToken" - | "#assertTopStack" Val WasmString + syntax Assertion ::= "#assertTopStack" Val WasmString | "#assertTopStackExactly" Val WasmString | "#assertStack" ValStack WasmString | "#assertLocal" Int Val WasmString @@ -38,7 +36,7 @@ module WASM-TEST-COMMON-SYNTAX | "#assertMemoryData" "(" Int "," Int ")" WasmString | "#assertMemoryData" Int "(" Int "," Int ")" WasmString | "#assertTable" Index Int OptionalInt WasmString - | "#assertTableElem" "(" Int "," Int ")" WasmString + | "#assertTableElem" "(" Int "," Index ")" WasmString | "#assertNamedModule" Identifier WasmString | "#assertRegistrationUnnamed" WasmString WasmString | "#assertRegistrationNamed" WasmString Identifier WasmString @@ -53,6 +51,8 @@ module WASM-REFERENCE-INTERPRETER-SYNTAX | "(" "get" OptionalId WasmString ")" | "get" Int WasmString // ---------------------------------------------------- + syntax PlainInstr ::= "ref" Int + | "ref.extern" Int syntax Auxil ::= "(" "register" WasmString ")" | "(" "register" WasmString Index ")" @@ -91,8 +91,7 @@ Here we inplement the conformance assertions specified in [spec interpreter] inc ``` ```k - syntax Assertion ::= "(" "assert_return" Action Instr ")" - | "(" "assert_return" Action ")" + syntax Assertion ::= "(" "assert_return" Action Instrs ")" | "(" "assert_return_canonical_nan" Action ")" | "(" "assert_return_arithmetic_nan" Action ")" | "(" "assert_trap" Action WasmString ")" @@ -131,7 +130,10 @@ The test embedder passes control to the execution cell in Wasm. ```k rule PGM => . - .K => sequenceStmts(text2abstract(PGM)) + .K + => #initSpectestModule + ~> sequenceStmts(text2abstract(PGM)) + ``` Bare Allocations @@ -158,11 +160,31 @@ We allow writing instructions at the top level in the test embedder. Auxiliary --------- -We add `token` as a value in order to implement some test assertions. +We add `token` as a value in order to use as a separator in ``. ```k syntax Val ::= "token" // ---------------------- + rule token => . ... + S => token : S + + syntax ValStack ::= takeUntilToken(ValStack) [function, total] + | dropUntilToken(ValStack) [function, total] + // ----------------------------------------------------------------- + rule takeUntilToken(.ValStack) => .ValStack + rule takeUntilToken(token : _ ) => token : .ValStack + rule takeUntilToken(V : Vs) => V : takeUntilToken(Vs) + requires V =/=K token + + rule dropUntilToken(.ValStack) => .ValStack + rule dropUntilToken(token : Vs ) => Vs + rule dropUntilToken(V : Vs) => dropUntilToken(Vs) + requires V =/=K token + + syntax Assertion ::= "#dropUntilToken" + // -------------------------------------------------- + rule #dropUntilToken => . ... + S => dropUntilToken(S) ``` Reference Interpreter Commands @@ -249,29 +271,80 @@ In order to parse the conformance test cases, we handle these declarations here rule ( module OID quote _DS ) => ( module OID .Defns ) ``` + +### Spectest Host Module + The conformance tests contain imports of the `"spectest"` module. -For now, we just introduce some special handling that ignores any tests that make use of `"spectest"`. -The handling consists of trapping whenever a `"spectest"` function is called, and removing the trap whenever a new module or assertion comes up. -TODO: Actually implement the `"spectest"` module, or call out to the supplied on in the spec repo. +- [Module signature](https://github.com/WebAssembly/spec/blob/f83a375df438067de1eafc25a2b5e249b7115a92/interpreter/README.md#spectest-host-module) +- [JS implementation](https://github.com/WebAssembly/spec/blob/f83a375df438067de1eafc25a2b5e249b7115a92/test/harness/async_index.js#L88) ```k - syntax Instr ::= "spectest_trap" - // -------------------------------- - rule spectest_trap ~> (_L:Label => .) ... - rule spectest_trap ~> (_F:Frame => .) ... - rule spectest_trap ~> (_I:Instr => .) ... - rule spectest_trap ~> (_D:Defn => .) ... - - rule (spectest_trap => .) ~> _M:ModuleDecl ... - rule (spectest_trap => .) ~> _A:Assertion ... - - rule #import(MOD, _, #funcDesc(... id: OID, type: TIDX)) - => #func(... type: TIDX, locals: [ .ValTypes ], body: spectest_trap .Instrs, metadata: #meta(... id: OID, localIds: .Map)) - ... - - requires MOD ==K #token("\"spectest\"", "WasmStringToken") - orBool MOD ==K #token("\"test\"" , "WasmStringToken") + syntax ModuleDecl ::= "#spectestModule" [function, total] + | "#emp" + // ----------------------------------------------------------- + rule #spectestModule + => #module ( ... + types: #type (... type: [ .ValTypes ] -> [ .ValTypes ] , metadata: ) + #type (... type: [ i32 .ValTypes ] -> [ .ValTypes ] , metadata: ) + #type (... type: [ i64 .ValTypes ] -> [ .ValTypes ] , metadata: ) + #type (... type: [ f32 .ValTypes ] -> [ .ValTypes ] , metadata: ) + #type (... type: [ f64 .ValTypes ] -> [ .ValTypes ] , metadata: ) + #type (... type: [ i32 f32 .ValTypes ] -> [ .ValTypes ] , metadata: ) + #type (... type: [ f64 f64 .ValTypes ] -> [ .ValTypes ] , metadata: ) + .EmptyStmts , + funcs: + #func (... type: 0 , locals: [ .ValTypes ] , body: .EmptyStmts , metadata: #meta (... id: , localIds: .Map ) ) + #func (... type: 1 , locals: [ .ValTypes ] , body: .EmptyStmts , metadata: #meta (... id: , localIds: .Map ) ) + #func (... type: 2 , locals: [ .ValTypes ] , body: .EmptyStmts , metadata: #meta (... id: , localIds: .Map ) ) + #func (... type: 3 , locals: [ .ValTypes ] , body: .EmptyStmts , metadata: #meta (... id: , localIds: .Map ) ) + #func (... type: 4 , locals: [ .ValTypes ] , body: .EmptyStmts , metadata: #meta (... id: , localIds: .Map ) ) + #func (... type: 5 , locals: [ .ValTypes ] , body: .EmptyStmts , metadata: #meta (... id: , localIds: .Map ) ) + #func (... type: 6 , locals: [ .ValTypes ] , body: .EmptyStmts , metadata: #meta (... id: , localIds: .Map ) ) + .EmptyStmts , + tables: + #table (... limits: #limits ( 10 , 20 ) , type: funcref, metadata: ) + .EmptyStmts , + mems: + #memory (... limits: #limits ( 1 , 2 ) , metadata: ) + .EmptyStmts , + globals: + #global (... type: const i32 , init: i32 . const 666 .EmptyStmts , metadata: ) + #global (... type: const i64 , init: i64 . const 666 .EmptyStmts , metadata: ) + #global (... type: const f32 , init: f32 . const 666.0 .EmptyStmts , metadata: ) + #global (... type: const f64 , init: f64 . const 666.0 .EmptyStmts , metadata: ) + .EmptyStmts , + elem: .EmptyStmts , + data: .EmptyStmts , + start: .EmptyStmts , + importDefns: .EmptyStmts , + exports: + #export (... name: #token("\"global_i32\"" , "WasmStringToken") , index: 0 ) + #export (... name: #token("\"global_i64\"" , "WasmStringToken") , index: 1 ) + #export (... name: #token("\"global_f32\"" , "WasmStringToken") , index: 2 ) + #export (... name: #token("\"global_f64\"" , "WasmStringToken") , index: 3 ) + #export (... name: #token("\"table\"" , "WasmStringToken") , index: 0 ) + #export (... name: #token("\"memory\"" , "WasmStringToken") , index: 0 ) + #export (... name: #token("\"print\"" , "WasmStringToken") , index: 0 ) + #export (... name: #token("\"print_i32\"" , "WasmStringToken") , index: 1 ) + #export (... name: #token("\"print_i64\"" , "WasmStringToken") , index: 2 ) + #export (... name: #token("\"print_f32\"" , "WasmStringToken") , index: 3 ) + #export (... name: #token("\"print_f64\"" , "WasmStringToken") , index: 4 ) + #export (... name: #token("\"print_i32_f32\"" , "WasmStringToken") , index: 5 ) + #export (... name: #token("\"print_f64_f64\"" , "WasmStringToken") , index: 6 ) + .EmptyStmts , + metadata: #meta (... id: , funcIds: .Map , filename: .String ) + ) + syntax Stmt ::= "#initSpectestModule" + // -------------------------------------------------------------------- + rule [initSpectestModule]: + #initSpectestModule + => #spectestModule + ~> ( register #token("\"spectest\"", "WasmStringToken") ) + ~> #emptyModule() // create an empty module for the test instructions + ... + + ``` Except `assert_return` and `assert_trap`, the remaining rules are directly reduced to empty. We are not planning to implement them and these rules are only used to make it easier to parse conformance tests. @@ -279,10 +352,17 @@ Except `assert_return` and `assert_trap`, the remaining rules are directly reduc *TODO:* Make use of `assert_exhaustion`, by detecting stack overflow. ```k - rule (assert_return ACT INSTR) => ACT ~> INSTR ~> #assertAndRemoveEqual ~> #assertAndRemoveToken ... - VALSTACK => token : VALSTACK - rule (assert_return ACT) => ACT ~> #assertAndRemoveToken ... - VALSTACK => token : VALSTACK + rule (assert_return ACT EXPECTED) + => token + ~> ACT + ~> token // separator between actual and expected value + ~> sequenceInstrs(EXPECTED) // evaluate the expected value(s) + ~> #assertReturn + ~> #dropUntilToken // clean expected value + ~> #dropUntilToken // clean return value + ... + + rule (assert_return_canonical_nan _ACT) => . ... rule (assert_return_arithmetic_nan _ACT) => . ... rule (assert_trap ACT:Action DESC) => ACT ~> #assertTrap DESC ... @@ -296,10 +376,13 @@ Except `assert_return` and `assert_trap`, the remaining rules are directly reduc And we implement some helper assertions to help testing. ```k - rule #assertAndRemoveEqual => #assertTopStack V .WasmString ~> ( drop ) ... - V : VALSTACK => VALSTACK - rule #assertAndRemoveToken => . ... - token : VALSTACK => VALSTACK + syntax Assertion ::= "#assertReturn" + // -------------------------------------- + rule #assertReturn + => #assertStackAux takeUntilToken(S) takeUntilToken(dropUntilToken(S)) + ... + + S ``` ### Trap Assertion @@ -317,20 +400,26 @@ These functions make assertions about the state of the `` cell. ```k syntax Assertion ::= "#assertStackAux" ValStack ValStack // --------------------------------------------------------------- - rule #assertTopStack S _ => . ... S : _VALSTACK - rule #assertTopStack < ITYPE:IValType > VAL _ => . ... < ITYPE > VAL' : _VALSTACK - requires #unsigned(ITYPE, VAL) ==Int VAL' - rule #assertTopStack < FTYPE:FValType > VAL _ => . ... < FTYPE > VAL' : _VALSTACK - requires signFloat(VAL) ==Bool signFloat(VAL') andBool VAL ==Float VAL' + rule #assertTopStack VAL _ => . ... + VAL' : _ + requires equalVal(VAL, VAL') - rule #assertTopStackExactly A _ => . ... A : _VALSTACK + rule #assertTopStackExactly A _ => . ... A : _VALSTACK rule #assertStack S1 _ => #assertStackAux S1 S2 ... S2 - rule #assertStackAux .ValStack _ => . ... - rule #assertStackAux ( V : S1') (V : S2') => #assertStackAux S1' S2' ... - rule #assertStackAux (< ITYPE > VAL : S1') (< ITYPE > VAL' : S2') => #assertStackAux S1' S2' ... - requires #unsigned(ITYPE, VAL) ==Int VAL' + + rule #assertStackAux .ValStack _ => . ... + rule #assertStackAux (V1 : S1) (V2 : S2) => #assertStackAux S1 S2 ... + requires equalVal(V1, V2) + + syntax Bool ::= equalVal(Val, Val) [function, total] + // ------------------------------------------------------- + rule equalVal( X, Y) => #unsigned(ITYPE, X) ==Int Y + rule equalVal( X, Y) => signFloat(X) ==Bool signFloat(Y) andBool X ==Float Y + rule equalVal( X, Y) => X ==Int Y + rule equalVal( X, Y) => X ==K Y [owise] + ``` ### Variables Assertions @@ -427,13 +516,14 @@ This asserts related operation about tables. ADDR MAX - SIZE + DATA ... ... + requires size(DATA) ==Int SIZE - rule #assertTableElem (KEY , VAL) _MSG => . ... + rule #assertTableElem (KEY , VAL:Int) _MSG => . ... CUR CUR @@ -443,11 +533,28 @@ This asserts related operation about tables. ADDR - ... KEY |-> VAL ... + TDATA ... ... + requires VAL ==K getRefOrNull(TDATA, KEY) + + rule #assertTableElem (KEY , FID:Identifier) MSG + => #assertTableElem (KEY , FADDRS {{ FUNC_ID }} orDefault -1) MSG + ... + + CUR + + CUR + + ... FID |-> FUNC_ID ... + ... + + FADDRS + ... + + ``` ### Memory Assertions @@ -528,6 +635,13 @@ We also want to be able to test that the embedder's registration function is wor ... REGNAME |-> IDX ... ``` +## Administrative instructions + +```k + rule ref I => I ... + rule ref.extern I => I ... +``` + ```k endmodule ``` diff --git a/tests/conformance/unparseable.txt b/tests/conformance/unparseable.txt index e9238bbaf..64de12c20 100644 --- a/tests/conformance/unparseable.txt +++ b/tests/conformance/unparseable.txt @@ -1,6 +1,9 @@ +block.wast br_table.wast +bulk.wast comments.wast conversions.wast +data.wast endianness.wast f32_cmp.wast f32.wast @@ -8,7 +11,14 @@ f64_cmp.wast f64.wast float_exprs.wast float_literals.wast -globals.wast +global.wast +if.wast +imports.wast +loop.wast +memory_copy.wast +memory_fill.wast +memory_init.wast memory.wast -names.wast +select.wast skip-stack-guard-page.wast +table_copy.wast diff --git a/tests/conformance/unsupported-llvm.txt b/tests/conformance/unsupported-llvm.txt index 19dabfd83..d154172d0 100644 --- a/tests/conformance/unsupported-llvm.txt +++ b/tests/conformance/unsupported-llvm.txt @@ -2,14 +2,14 @@ address.wast align.wast call_indirect.wast const.wast -data.wast -elem.wast f32_bitwise.wast f64_bitwise.wast +fac.wast float_memory.wast float_misc.wast -imports.wast +func.wast left-to-right.wast +linking.wast memory_redundancy.wast memory_trap.wast traps.wast diff --git a/tests/simple/functions_call.wast b/tests/simple/functions_call.wast index 39a804c9f..470792b96 100644 --- a/tests/simple/functions_call.wast +++ b/tests/simple/functions_call.wast @@ -36,7 +36,7 @@ (table 1 funcref) - (elem 0 (i32.const 0) 2) + (elem (i32.const 0) 2) ;; More complicated function with locals diff --git a/tests/simple/table.wast b/tests/simple/table.wast index fe7972b0b..ddeaf4557 100644 --- a/tests/simple/table.wast +++ b/tests/simple/table.wast @@ -11,19 +11,19 @@ table $named2 funcref (elem $f $g $k)) (func $f) (func $g) (func $k) ) -#assertTableElem (0, 0) "table elem 0" -#assertTableElem (1, 1) "table elem 1" -#assertTableElem (2, 2) "table elem 2" +#assertTableElem (0, $f) "table elem 0" +#assertTableElem (1, $g) "table elem 1" +#assertTableElem (2, $k) "table elem 2" #assertTable $named2 3 3 "table one with elements" (module - ( elem 0 (i32.const 1) $f $g) + ( elem (i32.const 1) $f $g) ( table 4 funcref) (func $f) (func $g) ) -#assertTableElem (1, 3) "table elem 1" -#assertTableElem (2, 4) "table elem 2" +#assertTableElem (1, $f) "table elem 1" +#assertTableElem (2, $g) "table elem 2" #assertTable 0 4 .Int "table two with elements" (module @@ -32,8 +32,8 @@ (func $f) (func $g) ) -#assertTableElem (1, 5) "table elem 1" -#assertTableElem (2, 6) "table elem 2" +#assertTableElem (1, $f) "table elem 1" +#assertTableElem (2, $g) "table elem 2" #assertTable 0 4 .Int "table two with elements" (module @@ -67,8 +67,8 @@ #assertFunction 2 [ ] -> [ i32 ] [ ] "call function 3 exists" #assertFunction 3 [ ] -> [ i32 ] [ ] "call function 4 exists" #assertFunction 4 [ ] -> [ i32 ] [ ] "call function 5 exists" -#assertTableElem (8, 7) "table elem 8" -#assertTableElem (9, 8) "table elem 9" +#assertTableElem (8, $const-i32-a) "table elem 8" +#assertTableElem (9, $const-i32-b) "table elem 9" #assertTable $tab 10 .Int "table three with elements" ;; Test offset unfolding. @@ -80,18 +80,18 @@ (elem (offset (i32.const 0)) 0) (elem (offset (nop) (i32.const 1)) 0) (elem (offset (i32.const 2) (nop)) 0) - (elem $t (offset (i32.const 3)) 0) - (elem $t (offset (nop) (i32.const 4)) 0) - (elem $t (offset (i32.const 5) (nop)) 0) + (elem (table $t) (offset (i32.const 3)) 0) + (elem (table $t) (offset (nop) (i32.const 4)) 0) + (elem (table $t) (offset (i32.const 5) (nop)) 0) (elem (offset (i32.const 6 (nop))) 0) - (elem $t (offset (i32.const 7 (nop))) 0) + (elem (table $t) (offset (i32.const 7 (nop))) 0) (global $g i32 (i32.const 8)) (global $h i32 (i32.const 9)) (elem (offset (global.get $g)) 0) - (elem $t (offset (global.get $h)) 0) + (elem (table $t) (offset (global.get $h)) 0) (func $main (local i32) (local.set 0 (i32.const 7)) diff --git a/tests/success-llvm.out b/tests/success-llvm.out index 873d19486..5407e65cc 100644 --- a/tests/success-llvm.out +++ b/tests/success-llvm.out @@ -54,6 +54,12 @@ 0 + + .ElemInstCellMap + + + 0 + true diff --git a/tests/wasm-tests b/tests/wasm-tests index d22a7659e..7fa2f20a6 160000 --- a/tests/wasm-tests +++ b/tests/wasm-tests @@ -1 +1 @@ -Subproject commit d22a7659e5f2f09be9532e2c72c04407134cc08e +Subproject commit 7fa2f20a6df4cf1c114582c8cb60f5bfcdbf1be1 diff --git a/wasm-text.md b/wasm-text.md index a5da10d6b..8246ba752 100644 --- a/wasm-text.md +++ b/wasm-text.md @@ -85,6 +85,8 @@ module WASM-TEXT-COMMON-SYNTAX ### Instructions +- [https://webassembly.github.io/spec/core/text/instructions.html](https://webassembly.github.io/spec/core/text/instructions.html) + #### Plain Instructions ```k @@ -97,7 +99,25 @@ module WASM-TEXT-COMMON-SYNTAX | "local.get" Index | "local.set" Index | "local.tee" Index + | "ref.is_null" + | "ref.func" Index + | "table.get" Index + | "table.set" Index + | "table.size" Index + | "table.grow" Index + | "table.fill" Index + | "table.copy" Index Index + | "table.copy" [macro] + | "table.init" Index Index + | "table.init" Index [macro] + | "elem.drop" Index + | "call_indirect" Index TypeUse + | "call_indirect" TypeUse [macro] // --------------------------------------- + // Abbreviations + rule table.init I => table.init 0 I + rule call_indirect TU:TypeUse => call_indirect 0 TU + rule table.copy => table.copy 0 0 syntax PlainInstr ::= IValType "." StoreOpM | FValType "." StoreOpM @@ -153,7 +173,7 @@ One type of folded instruction are `PlainInstr`s wrapped in parentheses and opti syntax TypeDefn ::= "(type" OptionalId "(" "func" TypeDecls ")" ")" // ------------------------------------------------------------------- - syntax TextLimits ::= Int | Int Int + syntax TextLimits ::= WasmInt | WasmInt WasmInt // ----------------------------------- ``` @@ -218,16 +238,19 @@ The following is the text format representation of an import specification. ### Tables +- [https://webassembly.github.io/spec/core/text/modules.html#tables](https://webassembly.github.io/spec/core/text/modules.html#tables) + ```k syntax TableDefn ::= "(" "table" OptionalId TableSpec ")" syntax TableSpec ::= TableType - | TableElemType "(" "elem" ElemSegment ")" + | TableElemType "(" "elem" ElemSegment ")" [prefer] + | TableElemType "(" "elem" ElemExprs ")" | InlineImport TableType | InlineExport TableSpec // ------------------------------------------- syntax TableType ::= TextLimits TableElemType - syntax TableElemType ::= "funcref" + syntax TableElemType ::= RefValType // ---------------------------------- ``` @@ -275,18 +298,35 @@ This is not optional. The offset can either be specified explicitly with the `offset` key word, or be a single instruction. ```k - syntax Offset ::= Instrs - // ------------------------ + syntax Offset ::= "(" Instrs ")" [macro] + // ------------------------------------------ + rule (IS:Instrs):Offset => (offset IS) ``` ### Element Segments +- [https://webassembly.github.io/spec/core/text/modules.html#element-segments](https://webassembly.github.io/spec/core/text/modules.html#element-segments) + ```k - syntax ElemDefn ::= "(" "elem" Index Offset ElemSegment ")" - | "(" "elem" Offset ElemSegment ")" - | "(" "elem" Offset "func" ElemSegment ")" + syntax ElemDefn ::= "(" "elem" OptionalId TableUse Offset ElemList ")" + | "(" "elem" OptionalId Offset ElemList ")" [macro, avoid] + | "(" "elem" OptionalId ElemList ")" // passive + | "(" "elem" OptionalId "declare" ElemList ")" // declarative // ------------------------------------------------------------ + rule (elem OID:OptionalId OF:Offset EL:ElemList) => (elem OID (table 0) OF EL) + + syntax ElemList ::= "func" ElemSegment + | ElemSegment // backwards compatibility + | RefValType ElemExprs + + syntax ElemExpr ::= "(" "item" Instrs ")" + | "(" Instrs ")" [macro] + rule (IS:Instrs):ElemExpr => (item IS) + syntax ElemExprs ::= List{ElemExpr, ""} + + syntax TableUse ::= "(" "table" Index ")" + ``` ### Data Segments @@ -468,15 +508,30 @@ Since the inserted type is module-level, any subsequent functions declaring the #### Tables +- [Abbreviations](https://webassembly.github.io/spec/core/text/modules.html#text-table-abbrev) + ```k - rule #unfoldDefns(( table funcref ( elem ELEM ) ) DS, I, M) + rule #unfoldDefns(( table funcref ( elem ELEM:ElemSegment ) ) DS, I, M) + => #unfoldDefns(( table #freshId(I) funcref ( elem ELEM ) ) DS, I +Int 1, M) + + rule #unfoldDefns(( table funcref ( elem ELEM:ElemExprs ) ) DS, I, M) => #unfoldDefns(( table #freshId(I) funcref ( elem ELEM ) ) DS, I +Int 1, M) - rule #unfoldDefns(( table ID:Identifier funcref ( elem ELEM ) ) DS, I, M) + rule #unfoldDefns(( table ID:Identifier funcref ( elem ELEM:ElemSegment ) ) DS, I, M) => ( table ID #lenElemSegment(ELEM) #lenElemSegment(ELEM) funcref ):TableDefn - ( elem ID (offset (i32.const 0) .Instrs) ELEM ) + ( elem ID (offset (i32.const 0) .Instrs) func ELEM ) + #unfoldDefns(DS, I, M) + + rule #unfoldDefns(( table ID:Identifier funcref ( elem ELEM:ElemExprs ) ) DS, I, M) + => ( table ID #lenElemExprs(ELEM) #lenElemExprs(ELEM) funcref ):TableDefn + ( elem ID (offset (i32.const 0) .Instrs) funcref ELEM ) #unfoldDefns(DS, I, M) + syntax Int ::= #lenElemExprs(ElemExprs) [function, total] + // ----------------------------------------------------------- + rule #lenElemExprs(.ElemExprs) => 0 + rule #lenElemExprs(_ EE) => 1 +Int #lenElemExprs(EE) + rule #unfoldDefns(( table OID:OptionalId (import MOD NAME) TT:TableType ) DS, I, M) => #unfoldDefns(( import MOD NAME (table OID TT) ) DS, I, M) @@ -534,19 +589,38 @@ Since the inserted type is module-level, any subsequent functions declaring the #### Element Segments +- [Abbreviations](https://webassembly.github.io/spec/core/text/modules.html#id7) + ```k - rule #unfoldDefns(((elem OFFSET func ES) => (elem OFFSET ES)) _DS, _I, _M) - rule #unfoldDefns(((elem OFFSET:Offset ES ) => ( elem 0 OFFSET ES )) _DS, _I, _M) - rule #unfoldDefns(((elem IDX OFFSET:Instrs ES ) => ( elem IDX ( offset OFFSET ) ES )) _DS, _I, _M) + // Active + rule #unfoldDefns((elem IDX TU (offset IS) ES) DS, I, M) + => (elem IDX TU (offset unfoldInstrs(IS)) #unfoldElemList(ES)) #unfoldDefns(DS, I, M) + + // Passive + rule #unfoldDefns((elem IDX:OptionalId ES:ElemList) DS, I, M) + => (elem IDX #unfoldElemList(ES)) #unfoldDefns(DS, I, M) + + // Declarative + rule #unfoldDefns((elem IDX:OptionalId declare ES:ElemList) DS, I, M) + => (elem IDX declare #unfoldElemList(ES)) #unfoldDefns(DS, I, M) + + syntax ElemList ::= #unfoldElemList(ElemList) [function] + rule #unfoldElemList(TYP EE) => TYP #unfoldElemExprs(EE) + rule #unfoldElemList(EL) => EL [owise] + + syntax ElemExprs ::= #unfoldElemExprs(ElemExprs) [function] + syntax ElemExpr ::= #unfoldElemExpr (ElemExpr) [function] + rule #unfoldElemExprs(.ElemExprs) => .ElemExprs + rule #unfoldElemExprs(E ES) => #unfoldElemExpr(E) #unfoldElemExprs(ES) - rule #unfoldDefns((elem IDX (offset IS) ES) DS, I, M) => (elem IDX (offset unfoldInstrs(IS)) ES) #unfoldDefns(DS, I, M) + rule #unfoldElemExpr((item IS:Instrs)) => (item unfoldInstrs(IS)) + ``` #### Data Segments ```k rule #unfoldDefns(((data OFFSET:Offset DATA ) => ( data 0 OFFSET DATA )) _DS, _I, _M) - rule #unfoldDefns(((data IDX OFFSET:Instrs DATA ) => ( data IDX ( offset OFFSET ) DATA )) _DS, _I, _M) rule #unfoldDefns((data IDX (offset IS) DATA) DS, I, M) => (data IDX (offset unfoldInstrs(IS)) DATA) #unfoldDefns(DS, I, M) ``` @@ -700,14 +774,16 @@ The `Context` contains information of how to map text-level identifiers to corre Record updates can currently not be done in a function rule which also does other updates, so we have helper functions to update specific fields. ```k - syntax Context ::= ctx(localIds: Map, globalIds: Map, funcIds: Map, typeIds: Map) + syntax Context ::= ctx(localIds: Map, globalIds: Map, funcIds: Map, typeIds: Map, + tableIds: Map, elemIds: Map, memoryIds: Map) | #freshCtx ( ) [function, total] | #updateLocalIds ( Context , Map ) [function, total] | #updateLocalIdsAux ( Context , Map , Bool ) [function, total] | #updateFuncIds ( Context , Map ) [function, total] | #updateFuncIdsAux ( Context , Map , Bool ) [function, total] // ------------------------------------------------------------------------------------- - rule #freshCtx ( ) => ctx(... localIds: .Map, globalIds: .Map, funcIds: .Map, typeIds: .Map) + rule #freshCtx ( ) + => ctx(... localIds: .Map, globalIds: .Map, funcIds: .Map, typeIds: .Map, tableIds: .Map, elemIds: .Map, memoryIds: .Map) rule #updateLocalIds(C, M) => #updateLocalIdsAux(C, M, false) rule #updateLocalIdsAux(ctx(... localIds: (_ => M)), M, false => true) @@ -716,6 +792,19 @@ Record updates can currently not be done in a function rule which also does othe rule #updateFuncIds(C, M) => #updateFuncIdsAux(C, M, false) rule #updateFuncIdsAux(ctx(... funcIds: (_ => M)), M, false => true) rule #updateFuncIdsAux(C, _, true) => C + + // lookup an identifier from the context + syntax Int ::= idxLookup(Map, Index) [function] + // --------------------------------------------------------------------- + rule idxLookup(_, I:Int) => I + rule idxLookup(M, I:Identifier) => {M[I] orDefault -1}:>Int requires validIdx(M,I) + + syntax Bool ::= validIdx(Map, Index) [function, total] + // ----------------------------------------------------------- + rule validIdx(_, _:Int) => true + rule validIdx(M, I:Identifier) => I in_keys(M) + andBool isInt(M[I] orDefault -1) + ``` #### Traversing the Full Program @@ -737,7 +826,14 @@ Since we do not have polymorphic functions available, we define one function per rule #t2aStmt(I:Instr) => #t2aInstr(I) rule #t2aStmt<_>(S) => S [owise] - rule #t2aModuleDecl<_>(#module(... types: TS, funcs: FS, globals: GS, importDefns: IS) #as M) => #t2aModule(M) + rule #t2aModuleDecl<_>(#module(... types: TS, funcs: FS, globals: GS, importDefns: IS, tables:TBS, elem: ES, mems: MS) #as M) + => #t2aModule(M) rule #t2aModule(#module(... types: TS, funcs: FS, tables: TABS, mems: MS, globals: GS, elem: EL, data: DAT, start: S, importDefns: IS, exports: ES, metadata: #meta(... id: OID))) => #module( ... types: #t2aDefns(TS) , funcs: #t2aDefns(FS) @@ -769,7 +865,7 @@ Since we do not have polymorphic functions available, we define one function per rule #t2aDefn<_ >(( import MOD NAME (global OID:OptionalId TYP:TextFormatGlobalType))) => #import(MOD, NAME, #globalDesc(... id: OID:OptionalId, type: asGMut(TYP))) - rule #t2aDefn<_ >(( import MOD NAME (table OID:OptionalId LIM:TextLimits funcref))) => #import(MOD, NAME, #tableDesc(... id: OID:OptionalId, type: t2aLimits(LIM))) + rule #t2aDefn<_ >(( import MOD NAME (table OID:OptionalId LIM:TextLimits _:RefValType))) => #import(MOD, NAME, #tableDesc(... id: OID:OptionalId, type: t2aLimits(LIM))) rule #t2aDefn<_ >(( import MOD NAME (memory OID:OptionalId LIM:TextLimits ))) => #import(MOD, NAME, #memoryDesc(... id: OID:OptionalId, type: t2aLimits(LIM))) ``` @@ -811,7 +907,8 @@ After unfolding, each type use in a function starts with an explicit reference t #### Tables ```k - rule #t2aDefn<_>((table OID:OptionalId LIMITS:TextLimits funcref )) => #table(... limits: t2aLimits(LIMITS), metadata: OID) + rule #t2aDefn<_>((table OID:OptionalId LIMITS:TextLimits TYP:RefValType )) + => #table(... limits: t2aLimits(LIMITS), type: TYP, metadata: OID) ``` #### Memories @@ -840,14 +937,48 @@ After unfolding, each type use in a function starts with an explicit reference t Wasm currently supports only one table, so we do not need to resolve any identifiers. ```k - rule #t2aDefn(( elem _:Index (offset IS) ES )) => #elem(0, #t2aInstrs(IS), #t2aElemSegment(ES) ) + rule #t2aDefn(( elem OID:OptionalId (table TID:Index) (offset IS) EL:ElemList )) + => #elem( getElemType(EL), #t2aElemList(EL), #elemActive(idxLookup(TIDS,TID), #t2aInstrs(IS)), OID) + requires validIdx(TIDS, TID) - syntax Ints ::= "#t2aElemSegment" "<" Context ">" "(" ElemSegment ")" [function] + rule #t2aDefn(( elem OID:OptionalId EL:ElemList )) + => #elem( getElemType(EL), #t2aElemList(EL), #elemPassive, OID) + + rule #t2aDefn(( elem OID:OptionalId declare EL:ElemList )) + => #elem( getElemType(EL), #t2aElemList(EL), #elemDeclarative, OID) + + syntax RefValType ::= getElemType(ElemList) [function, total] + // --------------------------------------------------------- + rule getElemType(func _) => funcref + rule getElemType(_:ElemSegment) => funcref + rule getElemType(T:RefValType _IS) => T + + syntax ListRef ::= "#t2aElemList" "<" Context ">" "(" ElemList ")" [function] + | "#t2aElemSegment" "<" Context ">" "(" ElemSegment ")" [function] + | "#t2aElemExprs" "<" Context ">" "(" ElemExprs ")" [function] + syntax RefVal ::= "#t2aElemExpr" "<" Context ">" "(" ElemExpr ")" [function] // -------------------------------------------------------------------------------- - rule #t2aElemSegment(ID:Identifier ES) => {FIDS[ID]}:>Int #t2aElemSegment(ES) - requires ID in_keys(FIDS) - rule #t2aElemSegment(I:Int ES) => I #t2aElemSegment(ES) - rule #t2aElemSegment<_C>(.ElemSegment) => .Ints + rule #t2aElemList(func ES) => #t2aElemSegment(ES) + rule #t2aElemList(ES) => #t2aElemSegment(ES) + rule #t2aElemList(_TYP:RefValType ES) => #t2aElemExprs(ES) + + rule #t2aElemSegment<_C>(.ElemSegment) => .ListRef + rule #t2aElemSegment(ID:Index ES) + => ListItem( idxLookup(FIDS, ID)) #t2aElemSegment(ES) + requires validIdx(FIDS, ID) + + rule #t2aElemExprs(E:ElemExpr ES:ElemExprs) + => ListItem(#t2aElemExpr(E)) #t2aElemExprs(ES) + rule #t2aElemExprs<_>(.ElemExprs) => .ListRef + + rule #t2aElemExpr((item ref.func ID)) + => idxLookup(FIDS, ID) + requires validIdx(FIDS, ID) + + rule #t2aElemExpr<_>((item ref.null func)) => null + rule #t2aElemExpr<_>((item ref.null extern)) => null + + ``` #### Data Segments @@ -899,7 +1030,10 @@ Wasm currently supports only one memory, so we do not need to resolve any identi requires ID in_keys(FIDS) rule #t2aInstr<_> (call I:Int) => #call(I) - rule #t2aInstr<_>(call_indirect TU) => call_indirect TU + rule #t2aInstr<_>(call_indirect TX:Int TU) => #call_indirect(TX, TU) + rule #t2aInstr(call_indirect TX:Identifier TU) + => #call_indirect({TIDS[TX]}:>Int, TU) + requires TX in_keys(TIDS) ``` #### Parametric Instructions @@ -932,6 +1066,52 @@ Wasm currently supports only one memory, so we do not need to resolve any identi rule #t2aInstr<_>(global.set I:Int) => #global.set(I) ``` +#### Table Instructions + +```k + rule #t2aInstr(table.get TI) + => #table.get(idxLookup(TIDS,TI)) + requires validIdx(TIDS, TI) + + rule #t2aInstr(table.set TI) + => #table.set(idxLookup(TIDS,TI)) + requires validIdx(TIDS, TI) + + rule #t2aInstr(elem.drop EI) + => #elem.drop(idxLookup(EIDS,EI)) + requires validIdx(EIDS, EI) + + rule #t2aInstr(table.size TI) + => #table.size(idxLookup(TIDS, TI)) + requires validIdx(TIDS, TI) + + rule #t2aInstr(table.grow TI) + => #table.grow(idxLookup(TIDS,TI)) + requires validIdx(TIDS, TI) + + rule #t2aInstr(table.fill TI) + => #table.fill(idxLookup(TIDS,TI)) + requires validIdx(TIDS, TI) + + rule #t2aInstr(table.init TI EI) + => #table.init(idxLookup(TIDS,TI), idxLookup(EIDS, EI)) + requires validIdx(TIDS, TI) + andBool validIdx(EIDS, EI) + + rule #t2aInstr(table.copy TI TI2) + => #table.copy(idxLookup(TIDS,TI), idxLookup(TIDS, TI2)) + requires validIdx(TIDS, TI) + andBool validIdx(TIDS, TI2) +``` + +#### Reference Instructions + +```k + rule #t2aInstr <_>( ref.null HT) => ref.null HT + rule #t2aInstr <_>( ref.is_null ) => #ref.is_null + rule #t2aInstr ( ref.func F:Index ) + => #ref.func(idxLookup(FIDS, F)) +``` #### Memory Instructions `MemArg`s can optionally be passed to `load` and `store` operations. @@ -1045,6 +1225,74 @@ The following are helper functions for gathering and updating context. rule #idcFuncsAux(.Defns, (func _:FuncSpec) FS => FS, IDX => IDX +Int 1, _ACC) rule #idcFuncsAux(.Defns, .Defns, _, ACC) => ACC + syntax Map ::= #idcTables (Defns, Defns ) [function] + | #idcTablesAux (Defns, Defns, Int, Map ) [function] + // ---------------------------------------------------- + rule #idcTables(IMPORTS, DEFNS) => #idcTablesAux(IMPORTS, DEFNS, 0, .Map) + rule #idcTablesAux(.Defns, .Defns, _IDX, ACC) => ACC + + // Consume imports + rule #idcTablesAux((import _ _ (table OID _)) IS, DS, IDX, ACC) + => #idcTablesAux(IS, DS, IDX +Int 1, #saveId(ACC, OID, IDX)) + requires #canSaveId(ACC, OID) + + rule #idcTablesAux(_ IS, DS, IDX, ACC) + => #idcTablesAux( IS, DS, IDX, ACC) + [owise] + + // Consume definitions + rule #idcTablesAux(.Defns, (table OID _) DS, IDX, ACC) + => #idcTablesAux(.Defns, DS, IDX +Int 1, #saveId(ACC, OID, IDX)) + requires #canSaveId(ACC, OID) + + rule #idcTablesAux(.Defns, _ DS, IDX, ACC) + => #idcTablesAux(.Defns, DS, IDX, ACC) + [owise] + + + syntax Map ::= #idcElems (Defns ) [function] + | #idcElemsAux (Defns, Int, Map ) [function] + // ----------------------------------------------------------- + rule #idcElems(DEFNS) => #idcElemsAux(DEFNS, 0, .Map) + + rule #idcElemsAux(.Defns, _IDX, ACC) => ACC + + rule #idcElemsAux((elem OID:OptionalId _:TableUse _:Offset _:ElemList) DS, IDX, ACC) + => #idcElemsAux(DS, IDX +Int 1, #saveId(ACC, OID, IDX)) + requires #canSaveId(ACC, OID) + + rule #idcElemsAux((elem OID:OptionalId _:ElemList) DS, IDX, ACC) + => #idcElemsAux(DS, IDX +Int 1, #saveId(ACC, OID, IDX)) + requires #canSaveId(ACC, OID) + + rule #idcElemsAux((elem OID:OptionalId declare _:ElemList) DS, IDX, ACC) + => #idcElemsAux(DS, IDX +Int 1, #saveId(ACC, OID, IDX)) + requires #canSaveId(ACC, OID) + + syntax Map ::= #idcMems (Defns, Defns ) [function] + | #idcMemsAux(Defns, Defns, Int, Map ) [function] + // -------------------------------------------------------------- + rule #idcMems(IMPORTS, DEFNS) => #idcMemsAux(IMPORTS, DEFNS, 0, .Map) + rule #idcMemsAux(.Defns, .Defns, _IDX, ACC) => ACC + + // Consume imports + rule #idcMemsAux((import _ _ (memory OID _)) IS, DS, IDX, ACC) + => #idcMemsAux(IS, DS, IDX +Int 1, #saveId(ACC, OID, IDX)) + requires #canSaveId(ACC, OID) + + rule #idcMemsAux(_ IS, DS, IDX, ACC) + => #idcMemsAux( IS, DS, IDX, ACC) + [owise] + + // Consume definitions + rule #idcMemsAux(.Defns, (memory OID _) DS, IDX, ACC) + => #idcMemsAux(.Defns, DS, IDX +Int 1, #saveId(ACC, OID, IDX)) + requires #canSaveId(ACC, OID) + + rule #idcMemsAux(.Defns, _ DS, IDX, ACC) + => #idcMemsAux(.Defns, DS, IDX, ACC) + [owise] + syntax Map ::= #idcGlobals ( Defns, Defns ) [function] | #idcGlobalsAux ( Defns, Defns, Int, Map ) [function] // ------------------------------------------------------------------- diff --git a/wasm.md b/wasm.md index 39adb9e74..2121d4b6d 100644 --- a/wasm.md +++ b/wasm.md @@ -4,6 +4,7 @@ WebAssembly State and Semantics ```k require "data.md" require "data/list-int.k" +require "data/list-ref.k" require "data/map-int-to-int.k" require "data/sparse-bytes.k" require "data/tools.k" @@ -77,6 +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] | 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' @@ -95,9 +97,8 @@ The sorts `EmptyStmt` and `EmptyStmts` are administrative so that the empty list | "memory.grow" [klabel(aGrow), symbol] // ----------------------------------- - syntax PlainInstr ::= "call_indirect" TypeUse syntax TypeUse ::= TypeDecls - | "(type" Index ")" [prefer] // TODO: Remove and move to wasm-text. + | "(type" Index ")" [prefer, klabel(aTypeUseIndex), symbol] // TODO: Remove and move to wasm-text. | "(type" Index ")" TypeDecls syntax TypeKeyWord ::= "param" | "result" syntax TypeDecl ::= "(" TypeDecl ")" [bracket] @@ -190,6 +191,7 @@ module WASM imports WASM-DATA imports WASM-DATA-TOOLS imports WASM-NUMERIC + imports LIST-REF-EXTENSIONS ``` ### Configuration @@ -215,8 +217,12 @@ module WASM 0 .Map .Map + 0 .Map .MapIntToInt + .Map + .MapIntToInt + 0 .Map .Map 0 @@ -246,10 +252,9 @@ module WASM 0 - 0 - .Int - 0 - .Map + 0 + .Int + .ListRef // TODO use ARRAY O(1) lookup 0 @@ -270,6 +275,14 @@ module WASM 0 + + + 0 + funcref + .ListRef // TODO use ARRAY O(1) lookup + + + 0 true @@ -357,6 +370,9 @@ Function `#unsigned` is called on integers to allow programs to use negative num ```k rule ITYPE:IValType . const VAL => #chop (< ITYPE > VAL) ... rule FTYPE:FValType . const VAL => #round( FTYPE , VAL) ... + + rule ref.null extern => null ... + rule ref.null func => null ... ``` ### Unary Operations @@ -585,7 +601,7 @@ The importing and exporting parts of specifications are dealt with in the respec rule #global(... type: TYP, init: IS, metadata: OID) => sequenceInstrs(IS) ~> allocglobal(OID, TYP) ... rule allocglobal(OID:OptionalId, MUT:Mut TYP:ValType) => . ... - < TYP > VAL : STACK => STACK + VAL : STACK => STACK CUR CUR @@ -598,13 +614,21 @@ The importing and exporting parts of specifications are dealt with in the respec ( .Bag => - NEXTADDR - VAL - MUT + NEXTADDR + VAL + MUT ) ... + requires #typeMatches(TYP, VAL) + + syntax Bool ::= #typeMatches(ValType, Val) [function, total] + // ------------------------------------------------------------- + rule #typeMatches(TYP, _) => true + rule #typeMatches(TYP, null) => true + rule #typeMatches(_, _) => false [owise] + ``` The `get` and `set` instructions read and write globals. @@ -645,6 +669,387 @@ The `get` and `set` instructions read and write globals. // - Map update preserves definedness () ``` +### Table Instructions + +- [Structure](https://webassembly.github.io/spec/core/syntax/instructions.html#table-instructions) +- [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#table-instructions) + +```k + syntax Instr ::= "#table.get" "(" Int ")" [klabel(aTable.get), symbol] + | "#table.set" "(" Int ")" [klabel(aTable.set), symbol] + | "#table.size" "(" Int ")" [klabel(aTable.size), symbol] + | "#table.grow" "(" Int ")" [klabel(aTable.grow), symbol] + | "#table.fill" "(" Int ")" [klabel(aTable.fill), symbol] + | "#table.copy" "(" Int "," Int ")" [klabel(aTable.copy), symbol] + | "#table.init" "(" Int "," Int ")" [klabel(aTable.init), symbol] + | "#elem.drop" "(" Int ")" [klabel(aElem.drop), symbol] + // --------------------------------------------------------------------------------- +``` + +#### `table.get` + +```k + rule [table.get]: + #table.get( TID ) => #tableGet(TADDR, I) ... + I : REST => REST + CUR + + CUR + ... TID |-> TADDR ... + ... + + + syntax Instr ::= #tableGet( addr: Int, index: Int) + rule [tableGet]: + #tableGet( TADDR, I) => getRefOrNull(TDATA, I) ... + + TADDR + TDATA + ... + + requires 0 <=Int I + andBool I #tableGet( TADDR, I) => trap ... + + TADDR + TDATA + ... + + requires I #table.set( TID ) + => #tableSet(TADDR, VAL, I) ... + + VAL:RefVal : I : REST => REST + CUR + + CUR + ... TID |-> TADDR ... + ... + + + rule [tableSet-oob]: + #tableSet(TADDR, _VAL, I) => trap ... + + TADDR + TDATA + ... + + requires I #tableSet(TADDR, VAL, I) => . ... + + TADDR + TDATA => TDATA [ I <- VAL ] + ... + + requires 0 <=Int I + andBool I #table.size(TID) => i32.const size(TDATA) ... + CUR + + CUR + ... TID |-> TADDR ... + ... + + + TADDR + TDATA + ... + +``` + +#### `table.grow` + +```k + rule [table.grow]: + #table.grow(TID) => i32.const size(TDATA) ... + N : REFVAL : STACK => STACK + CUR + + CUR + ... TID |-> TADDR ... + ... + + + TADDR + TMAX + TDATA => TDATA makeListRefTotal(N, REFVAL) + ... + + requires #canGrow(size(TDATA), N, TMAX) + + rule [table.grow-fail]: + #table.grow(TID) => i32.const (#pow(i32) -Int 1) ... + N : _REFVAL : STACK => STACK + CUR + + CUR + ... TID |-> TADDR ... + ... + + + TADDR + TMAX + TDATA + ... + + requires notBool #canGrow(size(TDATA), N, TMAX) + + syntax Bool ::= #canGrow(len: Int, n: Int, max: OptionalInt) [function, total] + // -------------------------------------------------------------------------------- + rule #canGrow(LEN, N, MAX) => LEN +Int N LEN +Int N #table.fill(TID) + => #tableCheckSizeGTE(TADDR, I +Int N) + ~> #tableFill(TID, N, RVAL, I) ... + + N : RVAL : I : STACK => STACK + CUR + + CUR + ... TID |-> TADDR ... + ... + + + syntax Instr ::= #tableFill(Int, Int, RefVal, Int) + // ------------------------------------------------------ + rule [tableFill-zero]: + #tableFill(_, 0, _, _) => . ... + + rule [tableFill-loop]: + #tableFill(TID, N, RVAL, I) + => I + ~> RVAL + ~> #table.set(TID) + ~> #tableFill(TID, N -Int 1, RVAL, I +Int 1) + ... + + requires N >Int 0 + +``` + +#### `table.copy` + +```k + rule [table.copy]: + #table.copy(TX, TY) + => #tableCheckSizeGTE(TYADDR, S +Int N) + ~> #tableCheckSizeGTE(TXADDR, D +Int N) + ~> #tableCopy(TX, TY, N, S, D) + ... + + N : S : D : STACK => STACK + CUR + + CUR + ... (TX |-> TXADDR) (TY |-> TYADDR) ... + ... + + + rule [table.copy-self]: + #table.copy(TX, TX) + => #tableCheckSizeGTE(TXADDR, maxInt(S, D) +Int N) + ~> #tableCopy(TX, TX, N, S, D) + ... + + N : S : D : STACK => STACK + CUR + + CUR + ... TX |-> TXADDR ... + ... + + + syntax Instr ::= #tableCopy(tix: Int, tiy: Int, n: Int, s: Int, d: Int) + // ----------------------------------------------------------------------- + rule [tableCopy-zero]: + #tableCopy(_, _, 0, _, _) => . ... + + // If D (destination index) is less than S (source), go from left to right + // Otherwise, start from the end + rule [tableCopy-LR]: + #tableCopy(TIX, TIY, N, S, D) + => D + ~> S + ~> #table.get(TIY) + ~> #table.set(TIX) + ~> #tableCopy(TIX, TIY, N -Int 1, S +Int 1, D +Int 1) + ... + + requires N >Int 0 + andBool D <=Int S + + rule [tableCopy-RL]: + #tableCopy(TIX, TIY, N, S, D) + => (D +Int N -Int 1) + ~> (S +Int N -Int 1) + ~> #table.get(TIY) + ~> #table.set(TIX) + ~> #tableCopy(TIX, TIY, N -Int 1, S, D) + ... + + requires N >Int 0 + andBool D >Int S +``` + +#### `table.init` + +```k + rule [table.init]: + #table.init(TID, EID) + => #elemCheckSizeGTE (EA, S +Int N) + ~> #tableCheckSizeGTE(TA, D +Int N) + ~> #tableInit(TID, N, D, dropListRef(S, ELEM)) + ... + + N : S : D : REST => REST + CUR + + CUR + ... TID |-> TA ... + ... wrap(EID) Int2Int|-> wrap(EA) ... + ... + + + EA + ELEM + ... + + + syntax Instr ::= #tableInit(tidx: Int, n: Int, d: Int, es: ListRef) + // ---------------------------------------------------- + rule [tableInit-done]: + #tableInit(_, 0, _, _) => . ... + + rule [tableInit]: + #tableInit(TID, N, D, ListItem(R) RS) + => #table.set(TID) + ~> #tableInit(TID, N -Int 1, D +Int 1, RS) + ... + + STACK => R : D : STACK + requires N >Int 0 + +``` + +#### `elem.drop` + +```k + rule [elem.drop]: + #elem.drop(EID) => . ... + CUR + + CUR + ... wrap(EID) Int2Int|-> wrap(EA) ... + ... + + + EA + _ => .ListRef + ... + + +``` + +#### Misc + +```k + syntax Instr ::= #tableCheckSizeGTE(addr: Int, n: Int) + // ------------------------------------------------------- + rule [tableCheckSizeGTE-pass]: + #tableCheckSizeGTE(ADDR, N) => . ... + + ADDR + TDATA + ... + + requires N <=Int size(TDATA) + + rule [tableCheckSizeGTE-fail]: + #tableCheckSizeGTE(_, _) => trap ... + [owise] + + + syntax Instr ::= #elemCheckSizeGTE(addr: Int, n: Int) + // ------------------------------------------------------- + rule [elemCheckSizeGTE-pass]: + #elemCheckSizeGTE(ADDR, N) => . ... + + ADDR + ELEM + ... + + requires N <=Int size(ELEM) + + rule [elemCheckSizeGTE-fail]: + #elemCheckSizeGTE(_, _) => trap ... + [owise] +``` + +### Reference Instructions + +- [Structure](https://webassembly.github.io/spec/core/syntax/instructions.html#reference-instructions) +- [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#reference-instructions) + +```k + syntax Instr ::= "#ref.is_null" [klabel(aRef.is_null), symbol] + | "#ref.func" "(" Int ")" [klabel(aRef.func), symbol] + // ------------------------------------------------------------------------ + + rule [ref.null.func]: + ref.null func => null ... + rule [ref.null.extern]: + ref.null extern => null ... + + rule [ref.isNull-true]: + #ref.is_null => i32.const 1 ... + <_:RefValType> null : STACK => STACK + + rule [ref.isNull-false]: + #ref.is_null => i32.const 0 ... + <_:RefValType> _:Int : STACK => STACK + + rule [ref.func]: + #ref.func(IDX) => ( FUNCADDRS {{ IDX }} orDefault 0 ) ... + CUR + + CUR + FUNCADDRS + ... + + requires isListIndex(IDX, FUNCADDRS) +``` + Types ----- @@ -805,7 +1210,7 @@ The `#take` function will return the parameter stack in the reversed order, then ### Function Call -`call funcidx` and `call_indirect typeidx` are 2 control instructions that invokes a function in the current frame. +`call funcidx` and `call_indirect tableidx typeuse` are 2 control instructions that invoke a function in the current frame. ```k syntax Instr ::= #call(Int) [klabel(aCall), symbol] @@ -821,9 +1226,8 @@ The `#take` function will return the parameter stack in the reversed order, then ``` ```k - syntax Instr ::= "#call_indirect" "(" Int ")" [klabel(aCall_indirect), symbol] + syntax Instr ::= "#call_indirect" "(" Int "," TypeUse ")" [klabel(aCall_indirect), symbol] // ------------------------------------------------------------------------------ - rule #call_indirect(I) => call_indirect (type I) ... ``` TODO: This is kept for compatibility with the text format. @@ -832,64 +1236,56 @@ But this requires a recursive descent into all the instructions of a function, w The types need to be inserted at the definitions level, if a previously undeclared type is present in a `call_indirect` function. ```k - rule call_indirect TUSE:TypeUse => ( invoke FADDR ) ... - CUR - < i32 > IDX : VALSTACK => VALSTACK - - CUR - TYPEIDS - TYPES - 0 |-> ADDR - ... - - - ADDR - ... IDX |-> FADDR ... - ... - - - FADDR - FTYPE - ... - - requires asFuncType(TYPEIDS, TYPES, TUSE) ==K FTYPE - - rule call_indirect TUSE:TypeUse => trap ... - CUR - < i32 > IDX : VALSTACK => VALSTACK - - CUR - TYPEIDS - TYPES - 0 |-> ADDR - ... - - - ADDR - ... IDX |-> FADDR ... - ... - - - FADDR - FTYPE - ... - - requires asFuncType(TYPEIDS, TYPES, TUSE) =/=K FTYPE + rule [call-indirect-getRef]: + #call_indirect(TIDX:Int,TUSE:TypeUse) + => #callIndirect( + getRefOrNull(TDATA, IDX), + asFuncType(TYPEIDS, TYPES, TUSE) + ) ... + + CUR + < i32 > IDX : VALSTACK => VALSTACK + + CUR + TYPEIDS + TYPES + ... TIDX |-> ADDR ... + ... + + + ADDR + TDATA + ... + + + + syntax Instr ::= #callIndirect(RefVal, FuncType) + // ------------------------------------------ + rule [callIndirect-invoke]: + #callIndirect( FADDR, ETYPE) + => ( invoke FADDR ) ... + + + FADDR + FTYPE + ... + + requires ETYPE ==K FTYPE + + rule [callIndirect-wrong-type]: + #callIndirect( FADDR, ETYPE) + => trap ... + + + FADDR + FTYPE + ... + + requires ETYPE =/=K FTYPE + + rule [callIndirect-null-ref]: + #callIndirect(<_> null, _) => trap ... - rule call_indirect _TUSE:TypeUse => trap ... - CUR - < i32 > IDX : VALSTACK => VALSTACK - - CUR - 0 |-> ADDR - ... - - - ADDR - TDATA - ... - - requires notBool IDX in_keys(TDATA) ``` Table @@ -905,31 +1301,33 @@ The specification can also include export directives. The importing and exporting parts of specifications are dealt with in the respective sections for import and export. ```k - syntax TableDefn ::= #table (limits: Limits, metadata: OptionalId) [klabel(aTableDefn), symbol] - syntax Alloc ::= alloctable (OptionalId, Int, OptionalInt) - // ---------------------------------------------------------- - rule #table(... limits: #limitsMin(MIN), metadata: OID) => alloctable(OID, MIN, .Int) ... + syntax TableDefn ::= #table (limits: Limits, type: RefValType, metadata: OptionalId) [klabel(aTableDefn), symbol] + syntax Alloc ::= alloctable (OptionalId, Int, OptionalInt, RefValType) + // -------------------------------------------------------------------- + rule #table(... limits: #limitsMin(MIN), type: TYP, metadata: OID) => alloctable(OID, MIN, .Int, TYP) ... requires MIN <=Int #maxTableSize() - rule #table(... limits: #limits(MIN, MAX), metadata: OID) => alloctable(OID, MIN, MAX) ... + rule #table(... limits: #limits(MIN, MAX), type: TYP, metadata: OID) => alloctable(OID, MIN, MAX, TYP) ... requires MIN <=Int #maxTableSize() andBool MAX <=Int #maxTableSize() - rule alloctable(ID, MIN, MAX) => . ... + rule alloctable(ID, MIN, MAX, TYP) => . ... CUR CUR - IDS => #saveId(IDS, ID, 0) - .Map => (0 |-> NEXTADDR) + IDS => #saveId(IDS, ID, NEXTIDX) + ADDRS => ADDRS [ NEXTIDX <- NEXTADDR] + NEXTIDX => NEXTIDX +Int 1 ... NEXTADDR => NEXTADDR +Int 1 ( .Bag => - NEXTADDR - MAX - MIN - .Map + NEXTADDR + MAX + + makeListRefTotal(MIN, null) + ) ... @@ -1159,43 +1557,79 @@ The maximum of table size is 2^32 bytes. rule #maxTableSize() => 4294967296 ``` -Initializers ------------- - -### Table initialization - -Tables can be initialized with element and the element type is always `funcref`. -The initialization of a table needs an offset and a list of functions, given as `Index`s. -A table index is optional and will be default to zero. +Element Segments +---------------- ```k + syntax ElemDefn ::= #elem(type: RefValType, elemSegment: ListRef, mode: ElemMode, oid: OptionalId) [klabel(aElemDefn), symbol] + | #elemAux(segmentLen: Int, mode: ElemMode) + syntax ElemMode ::= #elemActive(table: Int, offset: Instrs) [klabel(aElemActive), symbol] + | "#elemPassive" [klabel(aElemPassive), symbol] + | "#elemDeclarative" [klabel(aElemDeclarative), symbol] - syntax ElemDefn ::= #elem(index : Int, offset : Instrs, elemSegment : Ints) [klabel(aElemDefn), symbol] - | "elem" "{" Int Ints "}" - syntax Stmt ::= #initElements ( Int, Int, ListInt, Ints ) + syntax Alloc ::= allocelem(RefValType, ListRef, OptionalId) // ----------------------------------------------------- - rule #elem(TABIDX, IS, ELEMSEGMENT ) => sequenceInstrs(IS) ~> elem { TABIDX ELEMSEGMENT } ... - - rule elem { TABIDX ELEMSEGMENT } => #initElements ( ADDR, OFFSET, FADDRS, ELEMSEGMENT ) ... - CUR - < i32 > OFFSET : STACK => STACK - - CUR - FADDRS - TABIDX |-> ADDR - ... - + rule [elem-active]: + #elem(TYPE:RefValType, INIT:ListRef, MODE:ElemMode, OID:OptionalId) + => allocelem(TYPE, INIT, OID) + ~> #elemAux(size(INIT), MODE) + ... + + + rule [elem-active-aux]: + #elemAux(LEN:Int, #elemActive(... table: TID, offset: OFFSET)) + => sequenceInstrs(OFFSET) + ~> i32.const 0 + ~> i32.const LEN + ~> #table.init(TID, IDX) + ~> #elem.drop(IDX) + ... + + IDX : S => S - rule #initElements ( _, _, _, .Ints ) => . ... - rule #initElements ( ADDR, OFFSET, FADDRS, E:Int ES ) => #initElements ( ADDR, OFFSET +Int 1, FADDRS, ES ) ... - - ADDR - DATA => DATA [ OFFSET <- FADDRS{{E}} ] - ... - + rule [elem-declarative-aux]: + #elemAux(_LEN:Int, #elemDeclarative) + => #elem.drop(IDX) + ... + + IDX : S => S + + rule [elem-passive-aux]: + #elemAux(_LEN:Int, #elemPassive) + => . ... + + _IDX : S => S + + rule [allocelem]: + allocelem(TYPE, ELEMS, OID) => i32.const NEXTIDX ... + CUR + + CUR + FADDRS + ADDRS => ADDRS {{ NEXTIDX <- NEXTADDR }} + NEXTIDX => NEXTIDX +Int 1 + IDS => #saveId(IDS, OID, 0) + ... + + NEXTADDR => NEXTADDR +Int 1 + (.Bag => + NEXTADDR + TYPE + resolveAddrs(FADDRS, ELEMS) + ) + + syntax ListRef ::= resolveAddrs(ListInt, ListRef) [function] + // ----------------------------------------------------------- + rule resolveAddrs(_, .ListRef) => .ListRef + rule resolveAddrs(FADDRS, ListItem( I) IS) + => ListItem( FADDRS {{ I }} orDefault -1) resolveAddrs(FADDRS, IS) + rule resolveAddrs(FADDRS, ListItem( null) IS) + => ListItem( null) resolveAddrs(FADDRS, IS) + ``` -### Memory initialization +Data Segments +------------- Memories can be initialized with data, specified as a list of bytes together with an offset. The `data` initializer simply puts these bytes into the specified memory, starting at the offset. @@ -1324,10 +1758,10 @@ The value of a global gets copied when it is imported. ADDR MAX - SIZE + TDATA ... - requires #limitsMatchImport(SIZE, MAX, LIM) + requires #limitsMatchImport(size(TDATA), MAX, LIM) rule #import(MOD, NAME, #memoryDesc(... id: OID, type: LIM) ) => . ... CUR