From c9a237fffca67c89e92c594c14484d24b0b16d77 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Wed, 21 Feb 2024 11:43:53 +0000 Subject: [PATCH] Drop . in favour of .K (#581) * Drop . in favour of .K * Set Version: 0.1.4 --------- Co-authored-by: devops --- auxil.md | 2 +- package/version | 2 +- pykwasm/pyproject.toml | 2 +- test.md | 52 ++++++++++++------------ wasm.md | 90 +++++++++++++++++++++--------------------- 5 files changed, 74 insertions(+), 74 deletions(-) diff --git a/auxil.md b/auxil.md index eaf242300..a91d31c6d 100644 --- a/auxil.md +++ b/auxil.md @@ -21,7 +21,7 @@ module WASM-AUXIL imports WASM rule [clearConfig]: - #clearConfig => . ... + #clearConfig => .K ... _ => .Int _ => .ValStack _ => .Map diff --git a/package/version b/package/version index b1e80bb24..845639eef 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.3 +0.1.4 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index bb39b1544..7f86f943e 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pykwasm" -version = "0.1.3" +version = "0.1.4" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/test.md b/test.md index 2ac1dc30e..22ab590a6 100644 --- a/test.md +++ b/test.md @@ -129,7 +129,7 @@ Passing Control The test embedder passes control to the execution cell in Wasm. ```k - rule PGM => . + rule PGM => .K .K => #initSpectestModule ~> sequenceStmts(text2abstract(PGM)) @@ -165,7 +165,7 @@ We add `token` as a value in order to use as a separator in ``. ```k syntax Val ::= "token" // ---------------------- - rule token => . ... + rule token => .K ... S => token : S syntax ValStack ::= takeUntilToken(ValStack) [function, total] @@ -183,7 +183,7 @@ We add `token` as a value in order to use as a separator in ``. syntax Assertion ::= "#dropUntilToken" // -------------------------------------------------- - rule #dropUntilToken => . ... + rule #dropUntilToken => .K ... S => dropUntilToken(S) ``` @@ -255,7 +255,7 @@ We will reference modules by name in imports. rule ( register S ID:Identifier ) => ( register S IDX ) ... ... ID |-> IDX ... - rule ( register S:WasmString IDX:Int ) => . ... + rule ( register S:WasmString IDX:Int ) => .K ... ... .Map => S |-> IDX ... ``` @@ -363,13 +363,13 @@ Except `assert_return` and `assert_trap`, the remaining rules are directly reduc ... - rule (assert_return_canonical_nan _ACT) => . ... - rule (assert_return_arithmetic_nan _ACT) => . ... + rule (assert_return_canonical_nan _ACT) => .K ... + rule (assert_return_arithmetic_nan _ACT) => .K ... rule (assert_trap ACT:Action DESC) => ACT ~> #assertTrap DESC ... - rule (assert_exhaustion _ACT:Action _DESC) => . ... - rule (assert_malformed _MOD _DESC) => . ... - rule (assert_invalid _MOD _DESC) => . ... - rule (assert_unlinkable _MOD _DESC) => . ... + rule (assert_exhaustion _ACT:Action _DESC) => .K ... + rule (assert_malformed _MOD _DESC) => .K ... + rule (assert_invalid _MOD _DESC) => .K ... + rule (assert_unlinkable _MOD _DESC) => .K ... rule (assert_trap MOD:ModuleDecl DESC) => sequenceStmts(text2abstract(MOD .Stmts)) ~> #assertTrap DESC ... ``` @@ -390,7 +390,7 @@ And we implement some helper assertions to help testing. This asserts that a `trap` was just thrown. ```k - rule trap ~> #assertTrap _ => . ... + rule trap ~> #assertTrap _ => .K ... ``` ### ValStack Assertions @@ -400,16 +400,16 @@ These functions make assertions about the state of the `` cell. ```k syntax Assertion ::= "#assertStackAux" ValStack ValStack // --------------------------------------------------------------- - rule #assertTopStack VAL _ => . ... + rule #assertTopStack VAL _ => .K ... VAL' : _ requires equalVal(VAL, VAL') - rule #assertTopStackExactly A _ => . ... A : _VALSTACK + rule #assertTopStackExactly A _ => .K ... A : _VALSTACK rule #assertStack S1 _ => #assertStackAux S1 S2 ... S2 - rule #assertStackAux .ValStack _ => . ... + rule #assertStackAux .ValStack _ => .K ... rule #assertStackAux (V1 : S1) (V2 : S2) => #assertStackAux S1 S2 ... requires equalVal(V1, V2) @@ -427,10 +427,10 @@ These functions make assertions about the state of the `` cell. The operator `#assertLocal`/`#assertGlobal` operators perform a check for a local/global variable's value. ```k - rule #assertLocal INDEX VALUE _ => . ... + rule #assertLocal INDEX VALUE _ => .K ... ... INDEX |-> VALUE ... - rule #assertGlobal TFIDX VALUE _ => . ... + rule #assertGlobal TFIDX VALUE _ => .K ... CUR CUR @@ -454,7 +454,7 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca `#assertNextTypeIdx` checks whether the number of types are allocated correctly. ```k - rule #assertType IDX FTYPE => . ... + rule #assertType IDX FTYPE => .K ... CUR CUR @@ -462,7 +462,7 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca ... - rule #assertNextTypeIdx IDX => . ... + rule #assertNextTypeIdx IDX => .K ... CUR CUR @@ -487,7 +487,7 @@ This simply checks that the given function exists in the `` cell and has requires isListIndex(IDX, FUNCADDRS) - rule #assertFunctionHelper ADDR FTYPE LTYPE => . ... + rule #assertFunctionHelper ADDR FTYPE LTYPE => .K ... ADDR @@ -504,7 +504,7 @@ This simply checks that the given function exists in the `` cell and has This asserts related operation about tables. ```k - rule #assertTable TFIDX SIZE MAX _MSG => . ... + rule #assertTable TFIDX SIZE MAX _MSG => .K ... CUR CUR @@ -523,7 +523,7 @@ This asserts related operation about tables. requires size(DATA) ==Int SIZE - rule #assertTableElem (KEY , VAL:Int) _MSG => . ... + rule #assertTableElem (KEY , VAL:Int) _MSG => .K ... CUR CUR @@ -562,7 +562,7 @@ This asserts related operation about tables. This checks that the last allocated memory has the given size and max value. ```k - rule #assertMemory TFIDX SIZE MAX _MSG => . ... + rule #assertMemory TFIDX SIZE MAX _MSG => .K ... CUR CUR @@ -583,7 +583,7 @@ This checks that the last allocated memory has the given size and max value. rule #assertMemoryData (KEY , VAL) MSG => #assertMemoryData CUR (KEY, VAL) MSG ... CUR - rule #assertMemoryData MODIDX (KEY , VAL) _MSG => . ... + rule #assertMemoryData MODIDX (KEY , VAL) _MSG => .K ... MODIDX wrap(0) Int2Int|-> wrap(ADDR) @@ -607,7 +607,7 @@ These assertions act on the last module defined. ```k rule [assertNamedModule]: - #assertNamedModule NAME _S => . ... + #assertNamedModule NAME _S => .K ... ... NAME |-> IDX ... @@ -626,11 +626,11 @@ Registry Assertations We also want to be able to test that the embedder's registration function is working. ```k - rule #assertRegistrationUnnamed REGNAME _ => . ... + rule #assertRegistrationUnnamed REGNAME _ => .K ... IDX ... REGNAME |-> IDX ... - rule #assertRegistrationNamed REGNAME _NAME _ => . ... + rule #assertRegistrationNamed REGNAME _NAME _ => .K ... IDX ... REGNAME |-> IDX ... ``` diff --git a/wasm.md b/wasm.md index b7559b35a..070405484 100644 --- a/wasm.md +++ b/wasm.md @@ -319,13 +319,13 @@ Instructions | sequenceDefns ( Defns ) [function, total] | sequenceInstrs ( Instrs ) [function, total] // ------------------------------------------------- - rule sequenceStmts(.Stmts) => . + rule sequenceStmts(.Stmts) => .K rule sequenceStmts(S SS ) => S ~> sequenceStmts(SS) - rule sequenceDefns(.Defns) => . + rule sequenceDefns(.Defns) => .K rule sequenceDefns(D DS ) => D ~> sequenceDefns(DS) - rule sequenceInstrs(.Instrs) => . + rule sequenceInstrs(.Instrs) => .K rule sequenceInstrs(I IS ) => I ~> sequenceInstrs(IS) ``` @@ -340,10 +340,10 @@ Thus, a `trap` "bubbles up" (more correctly, to "consumes the continuation") unt ```k syntax Instr ::= "trap" // ----------------------- - rule trap ~> (_L:Label => .) ... - rule trap ~> (_F:Frame => .) ... - rule trap ~> (_I:Instr => .) ... - rule trap ~> (_D:Defn => .) ... + rule trap ~> (_L:Label => .K) ... + rule trap ~> (_F:Frame => .K) ... + rule trap ~> (_I:Instr => .K) ... + rule trap ~> (_D:Defn => .K) ... ``` When a single value ends up on the instruction stack (the `` cell), it is moved over to the value stack (the `` cell). @@ -351,7 +351,7 @@ If the value is the special `undefined`, then `trap` is generated instead. ```k rule undefined => trap ... - rule V:Val => . ... + rule V:Val => .K ... VALSTACK => V : VALSTACK requires V =/=K undefined ``` @@ -445,10 +445,10 @@ Operator `drop` removes a single item from the ``. The `select` operator picks one of the second or third stack values based on the first. ```k - rule drop => . ... + rule drop => .K ... _ : VALSTACK => VALSTACK - rule select => . ... + rule select => .K ... < i32 > C : V2 : V1 : VALSTACK => #if C =/=Int 0 #then V1 #else V2 #fi : VALSTACK @@ -462,7 +462,7 @@ Structured Control Flow `nop` does nothing. ```k - rule nop => . ... + rule nop => .K ... ``` `unreachable` causes an immediate `trap`. @@ -481,7 +481,7 @@ It simply executes the block then records a label with an empty continuation. ```k syntax Label ::= "label" VecType "{" Instrs "}" ValStack // -------------------------------------------------------- - rule label [ TYPES ] { _ } VALSTACK' => . ... + rule label [ TYPES ] { _ } VALSTACK' => .K ... VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' syntax BlockMetaData ::= OptionalInt @@ -501,7 +501,7 @@ Note that, unlike in the WebAssembly specification document, we do not need the ```k syntax Instr ::= #br( Int ) [klabel(aBr), symbol] // ------------------------------------------------- - rule #br(_IDX) ~> (_S:Stmt => .) ... + rule #br(_IDX) ~> (_S:Stmt => .K) ... rule #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ... VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' rule #br(N:Int) ~> _L:Label => #br(N -Int 1) ... @@ -512,7 +512,7 @@ Note that, unlike in the WebAssembly specification document, we do not need the rule #br_if(IDX) => #br(IDX) ... VAL : VALSTACK => VALSTACK requires VAL =/=Int 0 - rule #br_if(_IDX) => . ... + rule #br_if(_IDX) => .K ... VAL : VALSTACK => VALSTACK requires VAL ==Int 0 @@ -549,12 +549,12 @@ Variable Operators The various `init_local` variants assist in setting up the `locals` cell. ```k - rule init_local INDEX VALUE => . ... + rule init_local INDEX VALUE => .K ... LOCALS => LOCALS [ INDEX <- VALUE ] rule init_locals VALUES => #init_locals 0 VALUES ... - rule #init_locals _ .ValStack => . ... + rule #init_locals _ .ValStack => .K ... rule #init_locals N (VALUE : VALSTACK) => init_local N VALUE ~> #init_locals (N +Int 1) VALSTACK @@ -569,16 +569,16 @@ The `*_local` instructions are defined here. | "#local.set" "(" Int ")" [klabel(aLocal.set), symbol] | "#local.tee" "(" Int ")" [klabel(aLocal.tee), symbol] // ---------------------------------------------------------------------- - rule #local.get(I) => . ... + rule #local.get(I) => .K ... VALSTACK => VALUE : VALSTACK ... I |-> VALUE ... - rule #local.set(I) => . ... + rule #local.set(I) => .K ... VALUE : VALSTACK => VALSTACK LOCALS => LOCALS[I <- VALUE] requires I in_keys(LOCALS) - rule #local.tee(I) => . ... + rule #local.tee(I) => .K ... VALUE : _VALSTACK LOCALS => LOCALS[I <- VALUE] requires I in_keys(LOCALS) @@ -601,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) => . ... + rule allocglobal(OID:OptionalId, MUT:Mut TYP:ValType) => .K ... VAL : STACK => STACK CUR @@ -632,7 +632,7 @@ The `get` and `set` instructions read and write globals. syntax Instr ::= "#global.get" "(" Int ")" [klabel(aGlobal.get), symbol] | "#global.set" "(" Int ")" [klabel(aGlobal.set), symbol] // ------------------------------------------------------------------------ - rule #global.get(IDX) => . ... + rule #global.get(IDX) => .K ... VALSTACK => VALUE : VALSTACK CUR @@ -646,7 +646,7 @@ The `get` and `set` instructions read and write globals. ... - rule #global.set(IDX) => . ... + rule #global.set(IDX) => .K ... VALUE : VALSTACK => VALSTACK CUR @@ -744,7 +744,7 @@ The `get` and `set` instructions read and write globals. orBool size(TDATA) <=Int I rule [tableSet]: - #tableSet(TADDR, VAL, I) => . ... + #tableSet(TADDR, VAL, I) => .K ... TADDR TDATA => TDATA [ I <- VAL ] @@ -839,7 +839,7 @@ The `get` and `set` instructions read and write globals. syntax Instr ::= #tableFill(Int, Int, RefVal, Int) // ------------------------------------------------------ rule [tableFill-zero]: - #tableFill(_, 0, _, _) => . ... + #tableFill(_, 0, _, _) => .K ... rule [tableFill-loop]: #tableFill(TID, N, RVAL, I) @@ -888,7 +888,7 @@ The `get` and `set` instructions read and write globals. syntax Instr ::= #tableCopy(tix: Int, tiy: Int, n: Int, s: Int, d: Int) // ----------------------------------------------------------------------- rule [tableCopy-zero]: - #tableCopy(_, _, 0, _, _) => . ... + #tableCopy(_, _, 0, _, _) => .K ... // If D (destination index) is less than S (source), go from left to right // Otherwise, start from the end @@ -944,7 +944,7 @@ The `get` and `set` instructions read and write globals. syntax Instr ::= #tableInit(tidx: Int, n: Int, d: Int, es: ListRef) // ---------------------------------------------------- rule [tableInit-done]: - #tableInit(_, 0, _, _) => . ... + #tableInit(_, 0, _, _) => .K ... rule [tableInit]: #tableInit(TID, N, D, ListItem(R) RS) @@ -961,7 +961,7 @@ The `get` and `set` instructions read and write globals. ```k rule [elem.drop]: - #elem.drop(EID) => . ... + #elem.drop(EID) => .K ... CUR CUR @@ -982,7 +982,7 @@ The `get` and `set` instructions read and write globals. syntax Instr ::= #tableCheckSizeGTE(addr: Int, n: Int) // ------------------------------------------------------- rule [tableCheckSizeGTE-pass]: - #tableCheckSizeGTE(ADDR, N) => . ... + #tableCheckSizeGTE(ADDR, N) => .K ... ADDR TDATA @@ -998,7 +998,7 @@ The `get` and `set` instructions read and write globals. syntax Instr ::= #elemCheckSizeGTE(addr: Int, n: Int) // ------------------------------------------------------- rule [elemCheckSizeGTE-pass]: - #elemCheckSizeGTE(ADDR, N) => . ... + #elemCheckSizeGTE(ADDR, N) => .K ... ADDR ELEM @@ -1096,7 +1096,7 @@ When defining `TypeDefn`, the `identifier` for `param` will be ignored and will // ---------------------------------------------------- rule #type(... type: TYPE, metadata: OID) => alloctype(OID, TYPE) ... - rule alloctype(OID, TYPE) => . ... + rule alloctype(OID, TYPE) => .K ... CUR CUR @@ -1134,7 +1134,7 @@ The importing and exporting parts of specifications are dealt with in the respec NEXTADDR => NEXTADDR +Int 1 - rule allocfunc(MOD, ADDR, TYPE, LOCALS, INSTRS, #meta(... id: OID, localIds: LIDS)) => . ... + rule allocfunc(MOD, ADDR, TYPE, LOCALS, INSTRS, #meta(... id: OID, localIds: LIDS)) => .K ... ( .Bag => @@ -1166,7 +1166,7 @@ Unlike labels, only one frame can be "broken" through at a time. ```k syntax Frame ::= "frame" Int ValTypes ValStack Map // -------------------------------------------------- - rule frame MODIDX' TRANGE VALSTACK' LOCAL' => . ... + rule frame MODIDX' TRANGE VALSTACK' LOCAL' => .K ... VALSTACK => #take(lengthValTypes(TRANGE), VALSTACK) ++ VALSTACK' _ => LOCAL' _ => MODIDX' @@ -1198,9 +1198,9 @@ The `#take` function will return the parameter stack in the reversed order, then ... - rule return ~> (_S:Stmt => .) ... - rule return ~> (_L:Label => .) ... - rule (return => .) ~> _FR:Frame ... + rule return ~> (_S:Stmt => .K) ... + rule return ~> (_L:Label => .K) ... + rule (return => .K) ~> _FR:Frame ... ``` ### Function Call @@ -1305,7 +1305,7 @@ The importing and exporting parts of specifications are dealt with in the respec requires MIN <=Int #maxTableSize() andBool MAX <=Int #maxTableSize() - rule alloctable(ID, MIN, MAX, TYP) => . ... + rule alloctable(ID, MIN, MAX, TYP) => .K ... CUR CUR @@ -1350,7 +1350,7 @@ The importing and exporting parts of specifications are dealt with in the respec requires MIN <=Int #maxMemorySize() andBool MAX <=Int #maxMemorySize() - rule allocmemory(ID, MIN, MAX) => . ... + rule allocmemory(ID, MIN, MAX) => .K ... CUR CUR @@ -1395,7 +1395,7 @@ The value is encoded as bytes and stored at the "effective address", which is th requires 0 in_keys{{MEMADDRS}} andBool size(MEMADDRS) ==Int 1 - rule store { WIDTH EA VAL ADDR } => . ... + rule store { WIDTH EA VAL ADDR } => .K ... ADDR SIZE @@ -1591,7 +1591,7 @@ Element Segments rule [elem-passive-aux]: #elemAux(_LEN:Int, #elemPassive) - => . ... + => .K ... _IDX : S => S @@ -1637,7 +1637,7 @@ The `data` initializer simply puts these bytes into the specified memory, starti rule #data(IDX, IS, DATA) => sequenceInstrs(IS) ~> data { IDX DATA } ... // For now, deal only with memory 0. - rule data { MEMIDX DSBYTES } => . ... + rule data { MEMIDX DSBYTES } => .K ... < i32 > OFFSET : STACK => STACK CUR @@ -1683,7 +1683,7 @@ Exports make functions, tables, memories and globals available for importing int syntax ExportDefn ::= #export(name : WasmString, index : Int) [klabel(aExportDefn), symbol] syntax Alloc ::= ExportDefn // --------------------------- - rule #export(ENAME, IDX) => . ... + rule #export(ENAME, IDX) => .K ... CUR CUR @@ -1718,7 +1718,7 @@ The value of a global gets copied when it is imported. requires isListIndex(IDX, FS2) - rule #importHelper(#funcDesc(... type: TIDX), IMPORTEDADDR ) => . ... + rule #importHelper(#funcDesc(... type: TIDX), IMPORTEDADDR ) => .K ... CUR CUR @@ -1734,7 +1734,7 @@ The value of a global gets copied when it is imported. requires FTYPE ==K TYPES[TIDX] - rule #import(MOD, NAME, #tableDesc(... id: OID, type: LIM) ) => . ... + rule #import(MOD, NAME, #tableDesc(... id: OID, type: LIM) ) => .K ... CUR CUR @@ -1758,7 +1758,7 @@ The value of a global gets copied when it is imported. requires #limitsMatchImport(size(TDATA), MAX, LIM) - rule #import(MOD, NAME, #memoryDesc(... id: OID, type: LIM) ) => . ... + rule #import(MOD, NAME, #memoryDesc(... id: OID, type: LIM) ) => .K ... CUR CUR @@ -1782,7 +1782,7 @@ The value of a global gets copied when it is imported. requires #limitsMatchImport(SIZE, MAX, LIM) - rule #import(MOD, NAME, #globalDesc(... id: OID, type: MUT TYP) ) => . ... + rule #import(MOD, NAME, #globalDesc(... id: OID, type: MUT TYP) ) => .K ... CUR CUR