Skip to content

Commit

Permalink
use List instead of Map for <locals> cell
Browse files Browse the repository at this point in the history
  • Loading branch information
Dwight Guth committed Jun 20, 2024
1 parent d8baa68 commit cce775c
Show file tree
Hide file tree
Showing 5 changed files with 22 additions and 25 deletions.
2 changes: 1 addition & 1 deletion pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module WASM-AUXIL
<instrs> #clearConfig => .K ... </instrs>
<curModIdx> _ => .Int </curModIdx>
<valstack> _ => .ValStack </valstack>
<locals> _ => .Map </locals>
<locals> _ => .List </locals>
<moduleInstances> _ => .Bag </moduleInstances>
<moduleIds> _ => .Map </moduleIds>
<nextModuleIdx> _ => 0 </nextModuleIdx>
Expand Down
3 changes: 2 additions & 1 deletion pykwasm/src/pykwasm/kdist/wasm-semantics/test.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -430,7 +430,8 @@ The operator `#assertLocal`/`#assertGlobal` operators perform a check for a loca

```k
rule <instrs> #assertLocal INDEX VALUE _ => .K ... </instrs>
<locals> ... INDEX |-> VALUE ... </locals>
<locals> LOCALS </locals>
requires LOCALS[INDEX] ==K VALUE
rule <instrs> #assertGlobal TFIDX VALUE _ => .K ... </instrs>
<curModIdx> CUR </curModIdx>
Expand Down
1 change: 0 additions & 1 deletion pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1174,7 +1174,6 @@ They are currently supported in KWasm text files, but may be deprecated.
rule #t2aInstr<C>(#block(VT:VecType, IS:Instrs, BLOCKINFO)) => #block(VT, #t2aInstrs<C>(IS), BLOCKINFO)
rule #t2aInstr<_>(init_local I V) => init_local I V
rule #t2aInstr<_>(init_locals VS) => init_locals VS
```

Expand Down
39 changes: 18 additions & 21 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,10 +164,9 @@ Internal Syntax
module WASM-INTERNAL-SYNTAX
imports WASM-DATA-INTERNAL-SYNTAX
syntax Instr ::= "init_local" Int Val
| "init_locals" ValStack
| "#init_locals" Int ValStack
// --------------------------------------------
syntax Instr ::= "init_locals" ValStack
| "#init_locals" ValStack
// ----------------------------------------
syntax Int ::= #pageSize() [function, total]
syntax Int ::= #maxMemorySize() [function, total]
Expand Down Expand Up @@ -202,8 +201,8 @@ module WASM
<instrs> .K </instrs>
<valstack> .ValStack </valstack>
<curFrame>
<locals> .Map </locals>
<curModIdx> .Int </curModIdx>
<locals> .List </locals>
<curModIdx> .Int </curModIdx>
</curFrame>
<moduleRegistry> .Map </moduleRegistry>
<moduleIds> .Map </moduleIds>
Expand Down Expand Up @@ -549,17 +548,15 @@ Variable Operators
The various `init_local` variants assist in setting up the `locals` cell.

```k
rule <instrs> init_local INDEX VALUE => .K ... </instrs>
<locals> LOCALS => LOCALS [ INDEX <- VALUE ] </locals>
rule <instrs> init_locals VALUES => #init_locals 0 VALUES ... </instrs>
rule <instrs> init_locals VALUES => #init_locals VALUES ... </instrs>
<locals> _ => .List </locals>
rule <instrs> #init_locals _ .ValStack => .K ... </instrs>
rule <instrs> #init_locals N (VALUE : VALSTACK)
=> init_local N VALUE
~> #init_locals (N +Int 1) VALSTACK
rule <instrs> #init_locals .ValStack => .K ... </instrs>
rule <instrs> #init_locals (VALUE : VALSTACK)
=> #init_locals VALSTACK
...
</instrs>
<locals> ... .List => ListItem(VALUE) </locals>
```

The `*_local` instructions are defined here.
Expand All @@ -570,18 +567,18 @@ The `*_local` instructions are defined here.
| "#local.tee" "(" Int ")" [klabel(aLocal.tee), symbol]
// ----------------------------------------------------------------------
rule <instrs> #local.get(I) => .K ... </instrs>
<valstack> VALSTACK => VALUE : VALSTACK </valstack>
<locals> ... I |-> VALUE ... </locals>
<valstack> VALSTACK => {LOCALS [ I ]}:>Val : VALSTACK </valstack>
<locals> LOCALS </locals>
rule <instrs> #local.set(I) => .K ... </instrs>
<valstack> VALUE : VALSTACK => VALSTACK </valstack>
<locals> LOCALS => LOCALS[I <- VALUE] </locals>
requires I in_keys(LOCALS)
requires I >=Int 0 andBool I <Int size(LOCALS)
rule <instrs> #local.tee(I) => .K ... </instrs>
<valstack> VALUE : _VALSTACK </valstack>
<locals> LOCALS => LOCALS[I <- VALUE] </locals>
requires I in_keys(LOCALS)
requires I >=Int 0 andBool I <Int size(LOCALS)
```

### Globals
Expand Down Expand Up @@ -1164,8 +1161,8 @@ Similar to labels, they sit on the instruction stack (the `<instrs>` cell), and
Unlike labels, only one frame can be "broken" through at a time.

```k
syntax Frame ::= "frame" Int ValTypes ValStack Map
// --------------------------------------------------
syntax Frame ::= "frame" Int ValTypes ValStack List
// ---------------------------------------------------
rule <instrs> frame MODIDX' TRANGE VALSTACK' LOCAL' => .K ... </instrs>
<valstack> VALSTACK => #take(lengthValTypes(TRANGE), VALSTACK) ++ VALSTACK' </valstack>
<locals> _ => LOCAL' </locals>
Expand All @@ -1187,7 +1184,7 @@ The `#take` function will return the parameter stack in the reversed order, then
...
</instrs>
<valstack> VALSTACK => .ValStack </valstack>
<locals> LOCAL => .Map </locals>
<locals> LOCAL </locals>
<curModIdx> MODIDX => MODIDX' </curModIdx>
<funcDef>
<fAddr> FADDR </fAddr>
Expand Down
2 changes: 1 addition & 1 deletion tests/success-llvm.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
</valstack>
<curFrame>
<locals>
.Map
.List
</locals>
<curModIdx>
.Int
Expand Down

0 comments on commit cce775c

Please sign in to comment.