Skip to content

Commit

Permalink
Refactor Val: do not overload klabels (#573)
Browse files Browse the repository at this point in the history
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya authored Feb 12, 2024
1 parent 2df0b95 commit 959343e
Show file tree
Hide file tree
Showing 4 changed files with 48 additions and 24 deletions.
29 changes: 23 additions & 6 deletions data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,7 @@ endmodule
```k
module WASM-DATA-INTERNAL-SYNTAX
imports WASM-DATA-COMMON-SYNTAX
imports BOOL
syntax ValStack ::= ".ValStack" [klabel(.ValStack), symbol]
| Val ":" ValStack [klabel(concatValStack), symbol]
Expand All @@ -166,13 +167,29 @@ 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 RefVal ::= "<" RefValType ">" Int [klabel(<_>_)]
| "<" RefValType ">" "null" [klabel(<_>null), symbol]
syntax Val ::= "<" ValType ">" Number [klabel(<_>_)]
| IVal | FVal | RefVal
syntax IVal ::= "<" IValType ">" Int [klabel(IVal), symbol]
syntax FVal ::= "<" FValType ">" Float [klabel(FVal), symbol]
syntax RefVal ::= "<" RefValType ">" Int [klabel(RefVal), symbol]
| "<" RefValType ">" "null" [klabel(RefValNull), symbol]
syntax Val ::= IVal | FVal | RefVal
// ---------------------------
syntax Bool ::= #typeMatches(ValType, Val) [function, total]
// -------------------------------------------------------------
rule #typeMatches(TYP:IValType, <TYP> _:Int) => true
rule #typeMatches(TYP:FValType, <TYP> _:Float) => true
rule #typeMatches(TYP:RefValType, <TYP> _:Int) => true
rule #typeMatches(TYP:RefValType, <TYP> null) => true
rule #typeMatches(_, _) => false [owise]
syntax Bool ::= #sameType(Val, Val) [function, total]
// -------------------------------------------------------
rule #sameType(<T:IValType> _, V) => #typeMatches(T, V)
rule #sameType(<T:FValType> _, V) => #typeMatches(T, V)
rule #sameType(<T:RefValType> _, V) => #typeMatches(T, V)
rule #sameType(<T> null, V) => #typeMatches(T, V)
rule #sameType(undefined, _) => false
```

We also add `undefined` as a value, which makes many partial functions in the semantics total.
Expand Down
4 changes: 2 additions & 2 deletions pykwasm/src/pykwasm/kwasm_ast.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -122,10 +122,10 @@ def ints(iis: Iterable[int]) -> KInner:
def refs(values: Iterable[int | None]) -> KInner:
def idx_to_ref(idx: int | None) -> KInner:
if idx is None:
ref = KApply('<_>null', [funcref])
ref = KApply('RefValNull', [funcref])
else:
# TODO find a readable symbol for RefVals
ref = KApply('<_>__WASM-DATA-INTERNAL-SYNTAX_RefVal_RefValType_Int', [funcref, KInt(idx)])
ref = KApply('RefVal', [funcref, KInt(idx)])
return KApply('ListRefItem', [ref])

return KNamedList(REFS, REFS_NIL, [idx_to_ref(i) for i in values])
Expand Down
13 changes: 12 additions & 1 deletion tests/proofs/locals-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,17 @@ module LOCALS-SPEC

claim <instrs> #local.get(X) ~> #local.set(X) => . ... </instrs>
<locals>
X |-> < _ITYPE > (VAL => VAL)
X |-> _:IVal
</locals>

claim <instrs> #local.get(X) ~> #local.set(X) => . ... </instrs>
<locals>
X |-> _:FVal
</locals>

claim <instrs> #local.get(X) ~> #local.set(X) => . ... </instrs>
<locals>
X |-> _:RefVal
</locals>

endmodule
26 changes: 11 additions & 15 deletions wasm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -449,10 +449,11 @@ The `select` operator picks one of the second or third stack values based on the
<valstack> _ : VALSTACK => VALSTACK </valstack>
rule <instrs> select => . ... </instrs>
<valstack>
< i32 > C : < TYPE > V2:Number : < TYPE > V1:Number : VALSTACK
=> < TYPE > #if C =/=Int 0 #then V1 #else V2 #fi : VALSTACK
<valstack> < i32 > C : V2 : V1 : VALSTACK
=> #if C =/=Int 0 #then V1 #else V2 #fi : VALSTACK
</valstack>
requires #sameType(V1, V2)
```

Structured Control Flow
Expand Down Expand Up @@ -509,16 +510,16 @@ Note that, unlike in the WebAssembly specification document, we do not need the
syntax Instr ::= "#br_if" "(" Int ")" [klabel(aBr_if), symbol]
// --------------------------------------------------------------
rule <instrs> #br_if(IDX) => #br(IDX) ... </instrs>
<valstack> < _TYPE > VAL : VALSTACK => VALSTACK </valstack>
<valstack> <i32> VAL : VALSTACK => VALSTACK </valstack>
requires VAL =/=Int 0
rule <instrs> #br_if(_IDX) => . ... </instrs>
<valstack> < _TYPE > VAL : VALSTACK => VALSTACK </valstack>
<valstack> <i32> VAL : VALSTACK => VALSTACK </valstack>
requires VAL ==Int 0
syntax Instr ::= "#br_table" "(" Ints ")" [klabel(aBr_table), symbol]
// ---------------------------------------------------------------------
rule <instrs> #br_table(ES) => #br(#getInts(ES, minInt(VAL, #lenInts(ES) -Int 1))) ... </instrs>
<valstack> < _TYPE > VAL : VALSTACK => VALSTACK </valstack>
<valstack> <i32> VAL : VALSTACK => VALSTACK </valstack>
```

Finally, we have the conditional and loop instructions.
Expand Down Expand Up @@ -622,12 +623,6 @@ The importing and exporting parts of specifications are dealt with in the respec
...
</globals>
requires #typeMatches(TYP, VAL)
syntax Bool ::= #typeMatches(ValType, Val) [function, total]
// -------------------------------------------------------------
rule #typeMatches(TYP, <TYP> _) => true
rule #typeMatches(TYP, <TYP> null) => true
rule #typeMatches(_, _) => false [owise]
```

Expand Down Expand Up @@ -1805,10 +1800,11 @@ The value of a global gets copied when it is imported.
...
</moduleInst>
<globalInst>
<gAddr> ADDR </gAddr>
<gValue> <TYP> _ </gValue>
<gMut> MUT </gMut>
<gAddr> ADDR </gAddr>
<gValue> GVAL </gValue>
<gMut> MUT </gMut>
</globalInst>
requires #typeMatches(TYP, GVAL)
```

Tables and memories have proper subtyping, unlike globals and functions where a type is only a subtype of itself.
Expand Down

0 comments on commit 959343e

Please sign in to comment.