Extend type metadata from stable mir json (#520)

Upgrades the `stable-mir-json` dependency and adjusts parser and
execution to use the new `Basetype` and `TypeInfo` sorts.

Second change to implement `enum` support will follow this one in a
separate PR.

Author: jberthold

deps/stable-mir-json

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.111"
+version = "0.3.112"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/pyproject.toml

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.111'
+VERSION: Final = '0.3.112'

kmir/src/kmir/__init__.py

@@ -17,7 +17,7 @@ module KMIR-AST
   imports TYPES
 
 
-  syntax Pgm ::= Symbol GlobalAllocs FunctionNames MonoItems BaseTypes
+  syntax Pgm ::= Symbol GlobalAllocs FunctionNames MonoItems TypeMappings
                  [symbol(pgm), group(mir---name--allocs--functions--items--types)]
 
   syntax FunctionKind ::= functionNormalSym(Symbol) [symbol(FunctionKind::NormalSym), group(mir-enum)]
@@ -29,9 +29,9 @@ module KMIR-AST
 
   syntax FunctionNames ::= List [group(mir-klist-FunctionName)]
 
-  syntax BaseType ::= baseType( Ty, TyKind ) [group(mir)]
+  syntax TypeMapping ::= TypeMapping( Ty, TypeInfo ) [group(mir)]
 
-  syntax BaseTypes ::= List{BaseType, ""} [group(mir-list), symbol(BaseTypes::append), terminator-symbol(BaseTypes::empty)]
+  syntax TypeMappings ::= List{TypeMapping, ""} [group(mir-list), symbol(TypeMappings::append), terminator-symbol(TypeMappings::empty)]
 
   syntax KItem ::= #init( Pgm )
 

kmir/src/kmir/kdist/mir-semantics/kmir-ast.md

@@ -44,32 +44,32 @@ function map and the initial memory have to be set up.
 
 ```k
   // #init step, assuming a singleton in the K cell
-  rule <k> #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:BaseTypes)
+  rule <k> #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:TypeMappings)
          =>
            #execFunction(#findItem(ITEMS, FUNCNAME), FUNCTIONS)
        </k>
        <functions> _ => #mkFunctionMap(FUNCTIONS, ITEMS) </functions>
        <start-symbol> FUNCNAME </start-symbol>
-       <basetypes> _ => #mkTypeMap(.Map, TYPES) </basetypes>
+       <types> _ => #mkTypeMap(.Map, TYPES) </types>
 ```
 
 The `Map` of types is static information used for decoding constants and allocated data into `Value`s.
 It maps `Ty` IDs to `RigidTy` that can be supplied to decoding functions.
 
 ```k
-  syntax Map ::= #mkTypeMap ( Map, BaseTypes ) [function, total]
+  syntax Map ::= #mkTypeMap ( Map, TypeMappings ) [function, total]
 
-  rule #mkTypeMap(ACC, .BaseTypes) => ACC
+  rule #mkTypeMap(ACC, .TypeMappings) => ACC
 
   // build map of Ty -> RigidTy from suitable pairs
-  rule #mkTypeMap(ACC, baseType(TY, tyKindRigidTy(RIGID)) MORE:BaseTypes)
+  rule #mkTypeMap(ACC, TypeMapping(TY, TYPEINFO) MORE:TypeMappings)
       =>
-       #mkTypeMap(ACC[TY <- RIGID], MORE)
+       #mkTypeMap(ACC[TY <- TYPEINFO], MORE)
     requires notBool TY in_keys(ACC)
     [preserves-definedness] // key collision checked
 
-  // skip anything that is not a RigidTy or causes a key collision
-  rule #mkTypeMap(ACC, baseType(_TY, _OTHERTYKIND) MORE:BaseTypes)
+  // skip anything that causes a key collision
+  rule #mkTypeMap(ACC, _OTHERTYKIND:TypeMapping MORE:TypeMappings)
       =>
        #mkTypeMap(ACC, MORE)
     [owise]

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -53,7 +53,7 @@ module KMIR-CONFIGURATION
                   // FIXME where do we put the "GlobalAllocs"? in the heap, presumably?
                   <start-symbol> symbol($STARTSYM:String) </start-symbol>
                   // static information about the base type interning in the MIR
-                  <basetypes> .Map </basetypes>
+                  <types> .Map </types>
                 </kmir>
 
 endmodule

kmir/src/kmir/kdist/mir-semantics/rt/configuration.md

@@ -67,12 +67,12 @@ Constant operands are simply decoded according to their type.
 ```k
   rule <k> operandConstant(constOperand(_, _, mirConst(KIND, TY, _)))
         =>
-           typedValue(#decodeConstant(KIND, {TYPEMAP[TY]}:>RigidTy), TY, mutabilityNot)
+           typedValue(#decodeConstant(KIND, {TYPEMAP[TY]}:>TypeInfo), TY, mutabilityNot)
         ...
       </k>
-      <basetypes> TYPEMAP </basetypes>
+      <types> TYPEMAP </types>
     requires TY in_keys(TYPEMAP)
-     andBool isRigidTy(TYPEMAP[TY])
+     andBool isTypeInfo(TYPEMAP[TY])
     [preserves-definedness] // valid Map lookup checked
 ```
 
@@ -687,7 +687,7 @@ rewriting `typedLocal(...) ~> #cast(...) ~> REST` to `typedLocal(...) ~> REST`.
   syntax MIRError ::= CastError
 
   syntax CastError ::= UnknownCastTarget ( Ty , Map )
-                     | UnexpectedCastTarget ( CastKind, RigidTy )
+                     | UnexpectedCastTarget ( CastKind, TypeInfo )
                      | UnexpectedCastArgument ( TypedLocal, CastKind )
                      | CastNotimplemented ( CastKind )
 
@@ -703,28 +703,28 @@ bit width, signedness, and possibly truncating or 2s-complementing the value.
   // int casts
   rule <k> #cast(typedValue(Integer(VAL, WIDTH, _SIGNEDNESS), _, MUT), castKindIntToInt, TY)
           =>
-            typedValue(#intAsType(VAL, WIDTH, #numTypeOf({TYPEMAP[TY]}:>RigidTy)), TY, MUT)
+            typedValue(#intAsType(VAL, WIDTH, #numTypeOf({TYPEMAP[TY]}:>TypeInfo)), TY, MUT)
           ...
         </k>
-        <basetypes> TYPEMAP </basetypes>
-      requires #isIntType({TYPEMAP[TY]}:>RigidTy)
+        <types> TYPEMAP </types>
+      requires #isIntType({TYPEMAP[TY]}:>TypeInfo)
       [preserves-definedness] // ensures #numTypeOf is defined
 ```
 
 Error cases for `castKindIntToInt`
-* unknown target type (not in `basetypes`)
+* unknown target type (not in `types`)
 * target type is not an `Int` type
 * value is not a `Integer`
 
 ```k
   rule <k> #cast(_, castKindIntToInt, TY) => UnknownCastTarget(TY, TYPEMAP) ... </k>
-       <basetypes> TYPEMAP </basetypes>
-    requires notBool isRigidTy(TYPEMAP[TY])
+       <types> TYPEMAP </types>
+    requires notBool isTypeInfo(TYPEMAP[TY])
     [preserves-definedness]
 
-  rule <k> #cast(_, castKindIntToInt, TY) => UnexpectedCastTarget(castKindIntToInt, {TYPEMAP[TY]}:>RigidTy) ... </k>
-       <basetypes> TYPEMAP </basetypes>
-    requires notBool (#isIntType({TYPEMAP[TY]}:>RigidTy))
+  rule <k> #cast(_, castKindIntToInt, TY) => UnexpectedCastTarget(castKindIntToInt, {TYPEMAP[TY]}:>TypeInfo) ... </k>
+       <types> TYPEMAP </types>
+    requires notBool (#isIntType({TYPEMAP[TY]}:>TypeInfo))
     [preserves-definedness]
 
   rule <k> #cast(NONINT, castKindIntToInt, _TY) => UnexpectedCastArgument(NONINT, castKindIntToInt) ... </k>
@@ -744,34 +744,31 @@ Other type casts are not implemented yet.
 
 ## Decoding constants from their bytes representation to values
 
-The `Value` sort above operates at a higher level than the bytes representation found in the MIR syntax for constant values. The bytes have to be interpreted according to the given `RigidTy` to produce the higher-level value.
+The `Value` sort above operates at a higher level than the bytes representation found in the MIR syntax for constant values. The bytes have to be interpreted according to the given `TypeInfo` to produce the higher-level value. This is currently only defined for `PrimitiveType`s (primitive types in MIR).
 
 ```k
-  syntax Value ::= #decodeConstant ( ConstantKind, RigidTy ) [function]
+  syntax Value ::= #decodeConstant ( ConstantKind, TypeInfo ) [function]
 
   //////////////////////////////////////////////////////////////////////////////////////
   // decoding the correct amount of bytes depending on base type size
 
   // Boolean: should be one byte with value one or zero
-  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyBool) => BoolVal(false)
+  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool)) => BoolVal(false)
     requires 0 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1
-  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyBool) => BoolVal(true)
+  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool)) => BoolVal(true)
     requires 1 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1
 
   // Integer: handled in separate module for numeric operations
-  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), RIGIDTY)
+  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), TYPEINFO)
       => 
-        #decodeInteger(BYTES, #intTypeOf(RIGIDTY))
-    requires #isIntType(RIGIDTY)
-     andBool lengthBytes(BYTES) ==K #bitWidth(#intTypeOf(RIGIDTY)) /Int 8
+        #decodeInteger(BYTES, #intTypeOf(TYPEINFO))
+    requires #isIntType(TYPEINFO)
+     andBool lengthBytes(BYTES) ==K #bitWidth(#intTypeOf(TYPEINFO)) /Int 8
      [preserves-definedness]
 
   ////////////////////////////////////////////////////////////////////////////////////////////////
-  // FIXME Char and str types
-  // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyChar)
-  //     =>
-  //      Str(...)
-  // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), rigidTyStr)
+  // FIXME Char type
+  // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeChar))
   //     =>
   //      Str(...)
   /////////////////////////////////////////////////////////////////////////////////////////////////

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -22,22 +22,22 @@ module RT-NUMBERS
 
   syntax InTy  ::= IntTy | UintTy
 
-  syntax NumTy ::= #numTypeOf( RigidTy ) [function]
+  syntax NumTy ::= #numTypeOf( TypeInfo ) [function]
   // ----------------------------------------------
-  rule #numTypeOf(rigidTyInt(INTTY)) => INTTY
-  rule #numTypeOf(rigidTyUint(UINTTY)) => UINTTY
-  rule #numTypeOf(rigidTyFloat(FLOATTY)) => FLOATTY
+  rule #numTypeOf(typeInfoPrimitiveType(primTypeInt(INTTY))) => INTTY
+  rule #numTypeOf(typeInfoPrimitiveType(primTypeUint(UINTTY))) => UINTTY
+  rule #numTypeOf(typeInfoPrimitiveType(primTypeFloat(FLOATTY))) => FLOATTY
 
-  syntax InTy ::= #intTypeOf( RigidTy ) [function]
+  syntax InTy ::= #intTypeOf( TypeInfo ) [function]
   // ----------------------------------------------
-  rule #intTypeOf(rigidTyInt(INTTY)) => INTTY
-  rule #intTypeOf(rigidTyUint(UINTTY)) => UINTTY
+  rule #intTypeOf(typeInfoPrimitiveType(primTypeInt(INTTY))) => INTTY
+  rule #intTypeOf(typeInfoPrimitiveType(primTypeUint(UINTTY))) => UINTTY
 
-  syntax Bool ::= #isIntType ( RigidTy ) [function, total]
+  syntax Bool ::= #isIntType ( TypeInfo ) [function, total]
   // -----------------------------------------------------
-  rule #isIntType(rigidTyInt(_))  => true
-  rule #isIntType(rigidTyUint(_)) => true
-  rule #isIntType(_)              => false [owise]
+  rule #isIntType(typeInfoPrimitiveType(primTypeInt(_)))  => true
+  rule #isIntType(typeInfoPrimitiveType(primTypeUint(_))) => true
+  rule #isIntType(_)                                 => false [owise]
 ```
 
 Constants used for overflow-checking and truncation are defined here as macros.

kmir/src/kmir/kdist/mir-semantics/rt/numbers.md

@@ -219,6 +219,17 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
   syntax Movability ::= "movabilityStatic"  [group(mir-enum), symbol(Movability::Static)]
                       | "movabilityMovable" [group(mir-enum), symbol(Movability::Movable)]
 
+```
+
+`PrimitiveType`s are not present as an explicit type in MIR or Stable MIR AST, but are a conceptual sub-sort of  `RigidTy` for types that are "primitive".
+
+```k
+  syntax PrimitiveType ::= "primTypeBool"         [group(mir-enum), symbol(PrimitiveType::Bool)]
+                         | "primTypeChar"         [group(mir-enum), symbol(PrimitiveType::Char)]
+                         | primTypeInt(IntTy)     [group(mir-enum), symbol(PrimitiveType::Int)]
+                         | primTypeUint(UintTy)   [group(mir-enum), symbol(PrimitiveType::Uint)]
+                         | primTypeFloat(FloatTy) [group(mir-enum), symbol(PrimitiveType::Float)]
+
   syntax RigidTy ::= "rigidTyBool"                                                [group(mir-enum), symbol(RigidTy::Bool)]
                    | "rigidTyChar"                                                [group(mir-enum), symbol(RigidTy::Char)]
                    | rigidTyInt(IntTy)                                            [group(mir-enum), symbol(RigidTy::Int)]
@@ -242,6 +253,16 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
                    | rigidTyCoroutineWitness(CoroutineWitnessDef, GenericArgs)    [group(mir-enum), symbol(RigidTy::CoroutineWitness)]
                    | "rigidTyUnimplemented"                                       [group(mir-enum), symbol(RigidTy::Unimplemented), deprecated] // TODO: remove
 
+  // additional sort to provide type information in stable-mir-json
+  syntax TypeInfo ::= typeInfoPrimitiveType(PrimitiveType)       [symbol(TypeInfo::PrimitiveType), group(mir-enum)]
+                    | typeInfoEnumType(MIRString, Discriminants) [symbol(TypeInfo::EnumType)     , group(mir-enum---name--discriminants)]
+                    | typeInfoStructType(MIRString)              [symbol(TypeInfo::StructType)   , group(mir-enum---name)]
+
+  // discriminant information for enum types
+  syntax Discriminant ::= Discriminant ( Ty , MIRInt ) [group(mir)]
+
+  syntax Discriminants ::= List{Discriminant, ""} [group(mir-list), symbol(Discriminants::append), terminator-symbol(Discriminants::empty)]
+
 syntax TyKind ::= tyKindRigidTy(RigidTy)          [group(mir-enum), symbol(TyKind::RigidTy)]
                 | tyKindAlias(AliasKind, AliasTy) [group(mir-enum), symbol(TyKind::Alias)]
                 | tyKindParam(ParamTy)            [group(mir-enum), symbol(TyKind::Param)]