Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Deprecate klabel attribute #666

Merged
merged 2 commits into from
Jul 2, 2024
Merged

Deprecate klabel attribute #666

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7278351
Deprecate klabel
Baltoli Jul 2, 2024
255e640
Set Version: 0.1.74
Jul 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.73
0.1.74
2 changes: 1 addition & 1 deletion pykwasm/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pykwasm"
version = "0.1.73"
version = "0.1.74"
description = ""
authors = [
"Runtime Verification, Inc. <contact@runtimeverification.com>",
Expand Down
54 changes: 27 additions & 27 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ And we use `OptionalId` to handle the case where an identifier could be omitted.

```k
syntax Identifier ::= IdentifierToken
syntax OptionalId ::= "" [klabel(.Identifier), symbol]
syntax OptionalId ::= "" [symbol(.Identifier)]
| Identifier
// --------------------------------
```
Expand Down Expand Up @@ -88,15 +88,15 @@ WebAssembly has three kinds of [Value types](https://webassembly.github.io/spec/
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 RefValType ::= "funcref" [klabel(funcref), symbol]
| "externref" [klabel(externref), symbol]
syntax IValType ::= "i32" [symbol(i32)] | "i64" [symbol(i64)]
syntax FValType ::= "f32" [symbol(f32)] | "f64" [symbol(f64)]
syntax RefValType ::= "funcref" [symbol(funcref)]
| "externref" [symbol(externref)]
syntax ValType ::= IValType | FValType | RefValType
// ---------------------------------------

syntax HeapType ::= "func" [klabel(func), symbol]
| "extern" [klabel(extern), symbol]
syntax HeapType ::= "func" [symbol(func)]
| "extern" [symbol(extern)]
```

#### Type Constructors
Expand All @@ -120,8 +120,8 @@ For the core language, only regular integers are allowed.
### Type Mutability

```k
syntax Mut ::= "const" [klabel(mutConst), symbol]
| "var" [klabel(mutVar), symbol]
syntax Mut ::= "const" [symbol(mutConst)]
| "var" [symbol(mutVar)]
// -----------------------------------------------
```

Expand Down Expand Up @@ -158,19 +158,19 @@ module WASM-DATA-INTERNAL-SYNTAX
imports WASM-DATA-COMMON-SYNTAX
imports BOOL

syntax ValStack ::= ".ValStack" [klabel(.ValStack), symbol]
| Val ":" ValStack [klabel(concatValStack), symbol]
syntax ValStack ::= ".ValStack" [symbol(.ValStack)]
| Val ":" ValStack [symbol(concatValStack)]
```

### Values

Proper values are numbers annotated with their types.

```k
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 IVal ::= "<" IValType ">" Int [symbol(IVal)]
syntax FVal ::= "<" FValType ">" Float [symbol(FVal)]
syntax RefVal ::= "<" RefValType ">" Int [symbol(RefVal)]
| "<" RefValType ">" "null" [symbol(RefValNull)]
syntax Val ::= IVal | FVal | RefVal
// ---------------------------

Expand Down Expand Up @@ -204,9 +204,9 @@ We also add `undefined` as a value, which makes many partial functions in the se
There are two basic type-constructors: sequencing (`[_]`) and function spaces (`_->_`).

```k
syntax VecType ::= "[" ValTypes "]" [klabel(aVecType), symbol]
syntax VecType ::= "[" ValTypes "]" [symbol(aVecType)]

syntax FuncType ::= VecType "->" VecType [klabel(aFuncType), symbol]
syntax FuncType ::= VecType "->" VecType [symbol(aFuncType)]
```

All told, a `Type` can be a value type, vector of types, or function type.
Expand All @@ -221,7 +221,7 @@ In some cases, an integer is optional, such as when either giving or omitting th
The sort `OptionalInt` provides this potentially "undefined" `Int`.

```k
syntax OptionalInt ::= Int | ".Int" [klabel(.Int), symbol]
syntax OptionalInt ::= Int | ".Int" [symbol(.Int)]
```

### Integer bounds
Expand Down Expand Up @@ -332,8 +332,8 @@ For `Int`, however, a the context is irrelevant and the index always just resolv
Tables and memories have limits, defined as either a single `Int` or two `Int`s, representing min and max bounds.

```k
syntax Limits ::= #limitsMin(Int) [klabel(limitsMin), symbol]
| #limits(Int, Int) [klabel(limitsMinMax), symbol]
syntax Limits ::= #limitsMin(Int) [symbol(limitsMin)]
| #limits(Int, Int) [symbol(limitsMinMax)]
// ------------------------------------------------------------------
```

Expand All @@ -360,7 +360,7 @@ Also we can reverse a `ValTypes` with `#revt`

```k
syntax ValTypes ::= #revt ( ValTypes ) [function, total]
| #revt ( ValTypes , ValTypes ) [function, total, klabel(#revtAux)]
| #revt ( ValTypes , ValTypes ) [function, total, symbol(#revtAux)]
// ------------------------------------------------------------------------------------------
rule #revt(VT) => #revt(VT, .ValTypes)

Expand Down Expand Up @@ -480,7 +480,7 @@ Some operations extend integers from 1, 2, or 4 bytes, so a special function wit
Function `#bool` converts a `Bool` into an `Int`.

```k
syntax Int ::= #bool ( Bool ) [function, total, smtlib(boolToInt), symbol, klabel(boolToInt)]
syntax Int ::= #bool ( Bool ) [function, total, smtlib(boolToInt), symbol(boolToInt)]
// ----------------------------------------------------
rule #bool( B:Bool ) => 1 requires B
rule #bool( B:Bool ) => 0 requires notBool B
Expand Down Expand Up @@ -511,7 +511,7 @@ Each call site _must_ ensure that this is desired behavior before using these fu
| #take ( Int , ValStack ) [function, total]
| #drop ( Int , ValStack ) [function, total]
| #revs ( ValStack ) [function, total]
| #revs ( ValStack , ValStack ) [function, total, klabel(#revsAux)]
| #revs ( ValStack , ValStack ) [function, total, symbol(#revsAux)]
// ------------------------------------------------------------------------------------------
rule #zero(.ValTypes) => .ValStack
rule #zero(ITYPE:IValType VTYPES) => < ITYPE > 0 : #zero(VTYPES)
Expand All @@ -538,7 +538,7 @@ Wasm uses a different character escape rule with K, so we need to define the `un

```k
syntax String ::= unescape(String) [function]
| unescape(String, Int, String) [function, klabel(unescapeAux)]
| unescape(String, Int, String) [function, symbol(unescapeAux)]
// -------------------------------------------------------------------------------
rule unescape(S ) => unescape(S, 1, "")
rule unescape(S, IDX, SB) => SB requires IDX ==Int lengthString(S) -Int 1
Expand Down Expand Up @@ -616,7 +616,7 @@ The strings to connect needs to be unescaped before concatenated, because the `u

```k
syntax String ::= #concatDS ( DataString ) [function]
| #concatDS ( DataString, String ) [function, klabel(#concatDSAux)]
| #concatDS ( DataString, String ) [function, symbol(#concatDSAux)]
// -----------------------------------------------------------------------------------
rule #concatDS ( DS ) => #concatDS ( DS, "" )
rule #concatDS ( .DataString , S ) => S
Expand Down Expand Up @@ -690,7 +690,7 @@ endmodule
module WASM-DATA-SYMBOLIC [symbolic]
imports WASM-DATA-COMMON

syntax Int ::= #signedTotal ( IValType , Int) [function, total, klabel(#signedTotal), symbol, no-evaluators, smtlib(signedTotal)]
syntax Int ::= #signedTotal ( IValType , Int) [function, total, symbol(#signedTotal), no-evaluators, smtlib(signedTotal)]

rule #signedTotal(Arg0:IValType, Arg1:Int)
=> #signed(Arg0, Arg1)
Expand Down Expand Up @@ -730,4 +730,4 @@ module WASM-DATA
imports WASM-DATA-CONCRETE
imports WASM-DATA-SYMBOLIC
endmodule
```
```
4 changes: 2 additions & 2 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/data/int-type.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module INT-TYPE
syntax WrappedInt
syntax Int

syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)]
syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)]
syntax WrappedInt ::= wrap(Int) [symbol(wrapInt)]
syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol(unwrapInt)]
rule unwrap(wrap(A:Int)) => A
endmodule
30 changes: 15 additions & 15 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-ref.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,34 +10,34 @@ module LIST-REF
syntax ListRef [hook(LIST.List)]
syntax ListRef ::= ListRef ListRef
[ left, function, total, hook(LIST.concat),
klabel(_ListRef_), symbol, smtlib(smt_seq_concat),
symbol(_ListRef_), 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)
[ function, total, hook(LIST.unit), symbol(.ListRef),
smtlib(smt_seq_nil)
]
syntax ListRef ::= ListItem(RefVal)
[ function, total, hook(LIST.element), klabel(ListRefItem),
symbol, smtlib(smt_seq_elem)
[ function, total, hook(LIST.element), symbol(ListRefItem),
smtlib(smt_seq_elem)
]
syntax RefVal ::= ListRef "[" Int "]"
[ function, hook(LIST.get), klabel(ListRef:get), symbol ]
[ function, hook(LIST.get), symbol(ListRef:get) ]
syntax ListRef ::= ListRef "[" index: Int "<-" value: RefVal "]"
[function, hook(LIST.update), symbol, klabel(ListRef:set)]
[function, hook(LIST.update), symbol(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]
[function, hook(LIST.range), symbol(ListRef:range)]
syntax Bool ::= RefVal "in" ListRef
[function, total, hook(LIST.in), symbol, klabel(_inListRef_)]
[function, total, hook(LIST.in), symbol(_inListRef_)]
syntax Int ::= size(ListRef)
[function, total, hook(LIST.size), symbol, klabel (sizeListRef), smtlib(smt_seq_len)]
[function, total, hook(LIST.size), symbol(sizeListRef), smtlib(smt_seq_len)]
endmodule

module LIST-REF-EXTENSIONS
Expand All @@ -46,7 +46,7 @@ module LIST-REF-EXTENSIONS
imports INT

syntax RefVal ::= ListRef "[" Int "]" "orDefault" RefVal
[ function, total, klabel(ListRef:getOrDefault), symbol ]
[ function, total, symbol(ListRef:getOrDefault) ]
// ----------------------------------------------------------------
rule ListItem(V:RefVal) _:ListRef [0] orDefault _:RefVal
=> V
Expand All @@ -66,24 +66,24 @@ module LIST-REF-EXTENSIONS
[simplification]

syntax RefVal ::= getRefOrNull(ListRef, Int)
[ function, total, klabel(ListRef:getOrNull), symbol ]
[ function, total, symbol(ListRef:getOrNull) ]
// -------------------------------------------------------------
rule getRefOrNull(L, N) => L [N] orDefault (<funcref> null)

syntax ListRef ::= makeListRefTotal(Int, RefVal)
[function, total, klabel(ListRef:makeTotal), symbol]
[function, total, symbol(ListRef:makeTotal)]
// ----------------------------------------------------
rule makeListRefTotal(N, V) => makeListRef(N, V)
requires N >=Int 0
rule makeListRefTotal(N, _) => .ListRef
requires N <Int 0

syntax ListRef ::= dropListRef(Int, ListRef)
[function, total, klabel(ListRef:drop), symbol]
[function, total, symbol(ListRef:drop)]
// --------------------------------------------------------------
rule dropListRef(N, ListItem(_) L) => dropListRef(N -Int 1, L)
requires N >Int 0
rule dropListRef(_, L) => L
[owise]

endmodule
endmodule
26 changes: 13 additions & 13 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,50 +4,50 @@ module SPARSE-BYTES
imports BYTES
imports INT

syntax SBItem ::= #empty(Int) [symbol, klabel(SBItem:empty)]
| #bytes(Bytes) [symbol, klabel(SBItem:bytes)]
syntax SBItem ::= #empty(Int) [symbol(SBItem:empty)]
| #bytes(Bytes) [symbol(SBItem:bytes)]


syntax SBItemChunk ::= SBChunk(SBItem)

syntax SparseBytes ::= List{SBItemChunk, ""}

syntax Bytes ::= unwrap(SparseBytes)
[function, total, symbol, klabel(SparseBytes:unwrap)]
[function, total, symbol(SparseBytes:unwrap)]
// -----------------------------------------------------------------
rule unwrap(SBChunk(SBI) REST) => unwrap(SBI) +Bytes unwrap(REST)
rule unwrap(.SparseBytes) => .Bytes

syntax SparseBytes ::= fromBytes(Bytes)
[function, total, symbol, klabel(SparseBytes:fromBytes)]
[function, total, symbol(SparseBytes:fromBytes)]
// ---------------------------------------------------------
rule fromBytes(Bs) => SBChunk(#bytes(Bs))

syntax Bytes ::= unwrap(SBItem)
[function, total, symbol, klabel(SBItem:unwrap)]
[function, total, symbol(SBItem:unwrap)]
// -----------------------------------------------
rule unwrap(#bytes(Bs)) => Bs
rule unwrap(#empty(N)) => zeros(N)

syntax Bytes ::= zeros(Int) [function, total, symbol, klabel(zeros)]
syntax Bytes ::= zeros(Int) [function, total, symbol(zeros)]
// -------------------------------------------------------------------
rule zeros(N) => padLeftBytes(.Bytes, size(#empty(N)), 0)

syntax Int ::= size(SparseBytes)
[function, total, klabel(SparseBytes:size), symbol]
[function, total, symbol(SparseBytes:size)]
// ---------------------------------------------------
rule size(SBChunk(SBI) SBS) => size(SBI) +Int size(SBS)
rule size(.SparseBytes) => 0

syntax Int ::= size(SBItem)
[function, total, symbol, klabel(SBItem:size)]
[function, total, symbol(SBItem:size)]
// -----------------------------------------------
rule size(#bytes(Bs)) => lengthBytes(Bs)
rule size(#empty(N)) => maxInt(N,0)


syntax SparseBytes ::= substrSparseBytes(SparseBytes, from: Int, to: Int)
[function, total, klabel(SparseBytes:substr), symbol]
[function, total, symbol(SparseBytes:substr)]
// ------------------------------------------------------------------------
rule substrSparseBytes(_, S, E) => .SparseBytes
requires notBool( 0 <=Int S andBool S <=Int E )
Expand All @@ -66,7 +66,7 @@ module SPARSE-BYTES
andBool size(SBI) >Int S

syntax SparseBytes ::= substrSBItem(SBItem, from: Int, to: Int)
[function, total, klabel(SBItem:substr), symbol]
[function, total, symbol(SBItem:substr)]
// -------------------------------------------------------------
rule substrSBItem(_SBI, S, E) => .SparseBytes
requires S <Int 0 orBool E <Int S
Expand All @@ -90,7 +90,7 @@ module SPARSE-BYTES


syntax SparseBytes ::= replaceAt(SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAt)]
[function, total, symbol(SparseBytes:replaceAt)]
// --------------------------------------------------------
// invalid argument
rule replaceAt(_, S, _) => .SparseBytes
Expand All @@ -115,7 +115,7 @@ module SPARSE-BYTES
requires S <Int lengthBytes(B)

syntax SparseBytes ::= replaceAtZ(Int, SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAtZ)]
[function, total, symbol(SparseBytes:replaceAtZ)]
// ---------------------------------------------------------------
////////////// S < 0
rule replaceAtZ(_, _, S, _) => .SparseBytes
Expand Down Expand Up @@ -156,7 +156,7 @@ module SPARSE-BYTES


syntax SparseBytes ::= replaceAtB(Bytes, SparseBytes, Int, Bytes)
[function, total, symbol, klabel(SparseBytes:replaceAtB)]
[function, total, symbol(SparseBytes:replaceAtB)]
// ---------------------------------------------------------------
////////// S + len(Bs) <= len(MB)
rule replaceAtB(MB, REST, S, Bs)
Expand Down
Loading
Loading