Deprecate klabel attribute (#666)

* Deprecate klabel

* Set Version: 0.1.74

---------

Co-authored-by: devops <[email protected]>

Author: Baltoli

package/version

@@ -1 +1 @@
-0.1.73
+0.1.74

pykwasm/pyproject.toml

@@ -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. <[email protected]>",

pykwasm/src/pykwasm/kdist/wasm-semantics/data.md

@@ -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
  // --------------------------------
 ```
@@ -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
@@ -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)]
  // -----------------------------------------------
 ```
 
@@ -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
  // ---------------------------
 
@@ -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.
@@ -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
@@ -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)]
  // ------------------------------------------------------------------
 ```
 
@@ -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)
 
@@ -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
@@ -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)
@@ -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
@@ -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
@@ -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)
@@ -730,4 +730,4 @@ module WASM-DATA
    imports WASM-DATA-CONCRETE
    imports WASM-DATA-SYMBOLIC
 endmodule
-```
+```

pykwasm/src/pykwasm/kdist/wasm-semantics/data/int-type.k

@@ -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

pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-ref.k

@@ -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
@@ -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
@@ -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

pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k

@@ -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 )
@@ -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
@@ -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 
@@ -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 
@@ -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)