From f04f7d5fb985f3b3ccb31ba6c025cfd674fada1d Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 25 Jul 2024 19:00:23 -0300 Subject: [PATCH 1/7] Modifying #br(N) to not rewrite to #br(N-1) --- .../src/pykwasm/kdist/wasm-semantics/auxil.md | 2 + .../src/pykwasm/kdist/wasm-semantics/wasm.md | 41 ++++++++++++++++--- 2 files changed, 37 insertions(+), 6 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md index 2374dcf8c..b80863d5a 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md @@ -30,6 +30,8 @@ module WASM-AUXIL _ => 0 _ => .Map + _ => 0 + _ => .Bag _ => 0 _ => .Bag _ => 0 diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index 99e296fae..451ed51a3 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -235,6 +235,13 @@ module WASM 0 + 0 + + + 0 + + + 0 @@ -475,7 +482,7 @@ A block is the simplest way to create targets for break instructions (ie. jump d It simply executes the block then records a label with an empty continuation. ```k - syntax Label ::= "label" VecType "{" Instrs "}" ValStack + syntax Label ::= "label" VecType "{" Instrs "}" ValStack | ".Label" // -------------------------------------------------------- rule label [ TYPES ] { _ } VALSTACK' => .K ... VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' @@ -487,6 +494,18 @@ It simply executes the block then records a label with an empty continuation. // -------------------------------------------------------------------------------- rule #block(VECTYP, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... VALSTACK => .ValStack + NEXTID => NEXTID +Int 1 + + (.Bag + => + NEXTID + + + ) + ... + + + ``` The `br*` instructions search through the instruction stack (the `` cell) for the correct label index. @@ -495,14 +514,24 @@ Upon reaching it, the label itself is executed. Note that, unlike in the WebAssembly specification document, we do not need the special "context" operator here because the value and instruction stacks are separate. ```k - syntax Instr ::= #br( Int ) [symbol(aBr)] + syntax Instr ::= #br( Int ) [symbol(aBr)] | "#br_aux" "(" Int ")" [symbol(aBr_aux)] // ------------------------------------------------- - 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) ... + rule #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ... + VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' + rule #br(N:Int) ~> _L:Label => #br_aux(SIZE -Int N -Int 1) ... + SIZE requires N >Int 0 + rule #br_aux(_IDX) ~> (_S:Stmt => .K) ... + + rule #br_aux(N:Int) ~> _L:Label => #br_aux(N:Int) ... + rule #br_aux(N:Int) => sequenceInstrs(IS) ... + + N + + + VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' [owise] + syntax Instr ::= "#br_if" "(" Int ")" [symbol(aBr_if)] // -------------------------------------------------------------- rule #br_if(IDX) => #br(IDX) ... From ab5345c1b8c505a2f4a5fe8ebbb4bb19d228d479 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 25 Jul 2024 19:28:42 -0300 Subject: [PATCH 2/7] Fixing code --- pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index 451ed51a3..d7365861b 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -516,15 +516,24 @@ Note that, unlike in the WebAssembly specification document, we do not need the ```k syntax Instr ::= #br( Int ) [symbol(aBr)] | "#br_aux" "(" Int ")" [symbol(aBr_aux)] // ------------------------------------------------- - rule #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ... - VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' + 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_aux(SIZE -Int N -Int 1) ... SIZE requires N >Int 0 rule #br_aux(_IDX) ~> (_S:Stmt => .K) ... - rule #br_aux(N:Int) ~> _L:Label => #br_aux(N:Int) ... + rule #br_aux(N:Int) ~> _L:Label => sequenceInstrs(IS) ... + + N + + + VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' + rule #br_aux(N:Int) => sequenceInstrs(IS) ... N From 36b37c2799e7311f2e3b30ac869d28916bc6db1b Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 30 Jul 2024 10:58:43 -0300 Subject: [PATCH 3/7] Adding `#if` and `#loop` on the places to populate the `labeIsntance` bag --- .../src/pykwasm/kdist/wasm-semantics/wasm.md | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index d7365861b..d8c0fe54f 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -569,16 +569,46 @@ Finally, we have the conditional and loop instructions. // ------------------------------------------------------------------------------------------------------------ rule #if(VECTYP, IS, _, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... < i32 > VAL : VALSTACK => VALSTACK + NEXTID => NEXTID +Int 1 + + (.Bag + => + NEXTID + + + ) + ... + requires VAL =/=Int 0 rule #if(VECTYP, _, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... < i32 > VAL : VALSTACK => VALSTACK + NEXTID => NEXTID +Int 1 + + (.Bag + => + NEXTID + + + ) + ... + requires VAL ==Int 0 syntax Instr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)] // ------------------------------------------------------------------------------ rule #loop(VECTYP, IS, BLOCKMETA) => sequenceInstrs(IS) ~> label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK ... VALSTACK => .ValStack + NEXTID => NEXTID +Int 1 + + (.Bag + => + NEXTID + + + ) + ... + ``` Variable Operators From e022c9f879ddb2443c607aa75ae1c5f0dd0060f1 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 30 Jul 2024 14:01:40 -0300 Subject: [PATCH 4/7] Replacing cell Map with cell List Deleting `#br_aux` Storing the whole cell and using with continuation --- .../src/pykwasm/kdist/wasm-semantics/auxil.md | 3 +- .../src/pykwasm/kdist/wasm-semantics/wasm.md | 94 ++++--------------- 2 files changed, 18 insertions(+), 79 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md index b80863d5a..08ec3c5f7 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md @@ -30,8 +30,7 @@ module WASM-AUXIL _ => 0 _ => .Map - _ => 0 - _ => .Bag + _ => .List _ => 0 _ => .Bag _ => 0 diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index d8c0fe54f..9b3f98978 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -235,13 +235,7 @@ module WASM 0 - 0 - - - 0 - - - + .List 0 @@ -482,30 +476,20 @@ A block is the simplest way to create targets for break instructions (ie. jump d It simply executes the block then records a label with an empty continuation. ```k - syntax Label ::= "label" VecType "{" Instrs "}" ValStack | ".Label" + syntax Label ::= "label" VecType "{" Instrs "}" ValStack K | ".Label" // -------------------------------------------------------- - rule label [ TYPES ] { _ } VALSTACK' => .K ... + rule label [ TYPES ] { IS } VALSTACK' KCELL => KCELL VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' + ListItem(label [ TYPES ] { IS } VALSTACK' KCELL) LABELS => LABELS syntax BlockMetaData ::= OptionalInt // ------------------------------------ syntax Instr ::= #block(VecType, Instrs, BlockMetaData) [symbol(aBlock)] // -------------------------------------------------------------------------------- - rule #block(VECTYP, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... + rule #block(VECTYP, IS, _) ~> KCELL => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK KCELL VALSTACK => .ValStack - NEXTID => NEXTID +Int 1 - - (.Bag - => - NEXTID - - - ) - ... - - - + LABELS => pushList(label VECTYP { .Instrs } VALSTACK KCELL, LABELS) ``` The `br*` instructions search through the instruction stack (the `` cell) for the correct label index. @@ -514,33 +498,16 @@ Upon reaching it, the label itself is executed. Note that, unlike in the WebAssembly specification document, we do not need the special "context" operator here because the value and instruction stacks are separate. ```k - syntax Instr ::= #br( Int ) [symbol(aBr)] | "#br_aux" "(" Int ")" [symbol(aBr_aux)] + syntax Instr ::= #br( Int ) [symbol(aBr)] // ------------------------------------------------- - rule #br(_IDX) ~> (_S:Stmt => .K) ... - rule #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ... + rule #br(0 ) ~> _ => sequenceInstrs(IS) ~> KCELL' VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' + ListItem(label [ TYPES ] { IS } VALSTACK' KCELL') LABELS => LABELS - - rule #br(N:Int) ~> _L:Label => #br_aux(SIZE -Int N -Int 1) ... - SIZE + rule #br(N:Int) => #br(0) ... + LABELS => range(LABELS, N, 0) requires N >Int 0 - rule #br_aux(_IDX) ~> (_S:Stmt => .K) ... - - rule #br_aux(N:Int) ~> _L:Label => sequenceInstrs(IS) ... - - N - - - VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' - - rule #br_aux(N:Int) => sequenceInstrs(IS) ... - - N - - - VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' [owise] - syntax Instr ::= "#br_if" "(" Int ")" [symbol(aBr_if)] // -------------------------------------------------------------- rule #br_if(IDX) => #br(IDX) ... @@ -567,48 +534,21 @@ Finally, we have the conditional and loop instructions. ```k syntax Instr ::= #if( VecType, then : Instrs, else : Instrs, blockInfo: BlockMetaData) [symbol(aIf)] // ------------------------------------------------------------------------------------------------------------ - rule #if(VECTYP, IS, _, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... + rule #if(VECTYP, IS, _, _) ~> KCELL => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK KCELL < i32 > VAL : VALSTACK => VALSTACK - NEXTID => NEXTID +Int 1 - - (.Bag - => - NEXTID - - - ) - ... - + LABELS => pushList(label VECTYP { .Instrs } VALSTACK KCELL, LABELS) requires VAL =/=Int 0 - rule #if(VECTYP, _, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... + rule #if(VECTYP, _, IS, _) ~> KCELL => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK KCELL < i32 > VAL : VALSTACK => VALSTACK - NEXTID => NEXTID +Int 1 - - (.Bag - => - NEXTID - - - ) - ... - + LABELS => pushList(label VECTYP { .Instrs } VALSTACK KCELL, LABELS) requires VAL ==Int 0 syntax Instr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)] // ------------------------------------------------------------------------------ - rule #loop(VECTYP, IS, BLOCKMETA) => sequenceInstrs(IS) ~> label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK ... + rule #loop(VECTYP, IS, BLOCKMETA) ~> KCELL => sequenceInstrs(IS) ~> label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK KCELL VALSTACK => .ValStack - NEXTID => NEXTID +Int 1 - - (.Bag - => - NEXTID - - - ) - ... - + LABELS => pushList(label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK KCELL, LABELS) ``` Variable Operators From e10cf3ff2ac123a60af0f321189ffbd16ad8358d Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 31 Jul 2024 12:41:41 -0300 Subject: [PATCH 5/7] Corner cases --- pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index 9b3f98978..0326a9bdb 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -332,7 +332,7 @@ Thus, a `trap` "bubbles up" (more correctly, to "consumes the continuation") unt ```k syntax Instr ::= "trap" // ----------------------- - rule trap ~> (_L:Label => .K) ... + rule trap ~> label _ {_} _ KCELL ~> _ => (trap ~> KCELL) rule trap ~> (_F:Frame => .K) ... rule trap ~> (_I:Instr => .K) ... rule trap ~> (_D:Defn => .K) ... @@ -1207,7 +1207,7 @@ The `#take` function will return the parameter stack in the reversed order, then rule return ~> (_S:Stmt => .K) ... - rule return ~> (_L:Label => .K) ... + rule return ~> (label [_] {_} _ KCELL) ~> _ => (return ~> KCELL) rule (return => .K) ~> _FR:Frame ... ``` From 1a9c3144405f8f7c602da62ad69f7b021bfc7d3b Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 31 Jul 2024 13:48:32 -0300 Subject: [PATCH 6/7] Fixing gold test --- tests/success-llvm.out | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/success-llvm.out b/tests/success-llvm.out index 2dee704ab..8a47d4faa 100644 --- a/tests/success-llvm.out +++ b/tests/success-llvm.out @@ -30,6 +30,9 @@ 0 + + .List + .FuncDefCellMap From 476baf06fb956f502b54e03dc9bb6191bb241e22 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 31 Jul 2024 14:38:43 -0300 Subject: [PATCH 7/7] Fixing more corner cases --- pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index 0326a9bdb..ee5ce1f34 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md @@ -476,7 +476,7 @@ A block is the simplest way to create targets for break instructions (ie. jump d It simply executes the block then records a label with an empty continuation. ```k - syntax Label ::= "label" VecType "{" Instrs "}" ValStack K | ".Label" + syntax Label ::= "label" VecType "{" Instrs "}" ValStack K // -------------------------------------------------------- rule label [ TYPES ] { IS } VALSTACK' KCELL => KCELL VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' @@ -1207,8 +1207,9 @@ The `#take` function will return the parameter stack in the reversed order, then rule return ~> (_S:Stmt => .K) ... - rule return ~> (label [_] {_} _ KCELL) ~> _ => (return ~> KCELL) - rule (return => .K) ~> _FR:Frame ... + rule return ~> (label [_] {_} _ KCELL ~> _) => (return ~> KCELL) + rule return ~> _FR:Frame ~> (label [_] {_} _ KCELL) ~> _ => (return ~> KCELL) + rule (return => .K) ~> _FR:Frame ... [owise] ``` ### Function Call