449 simplify kmir types

kmir/pyproject.toml

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

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.72'
+VERSION: Final = '0.3.73'

kmir/src/kmir/convert_from_definition/notes.md

@@ -25,6 +25,12 @@ syntax A ::= a(Bool) [group(mir-bool), ...]
 ```
 json: a boolean value, e.g., `true`
 
+#### mir-bytes
+```
+syntax A ::= a(Bytes) [group(mir-bytes), ...]
+```
+json: an array of integer values between 0 and 255
+
 #### mir-list
 ```
 syntax Elems ::= List {Elem, ""} [group(mir-list), ...]
@@ -71,13 +77,13 @@ Any remaining production describing MIR syntax.
 
 
 ### Conventions for productions
-- Syntax productions with more than one non terminals should not include sorts `Int`, `Bool`, `String`, but should instead use the sorts `MIRInt`, `MIRBool`, `MIRString`. These are intended to be semantically equivalent, i.e.
+- Syntax productions with more than one non terminals should not include sorts `Int`, `Bool`, `String`, and `Bytes`, but should instead use the sorts `MIRInt`, `MIRBool`, `MIRString`, and `MIRBytes`. These are intended to be semantically equivalent, i.e.
 ```
 mirInt(I) => I
 mirBool(B) => B
 mirString(S) => S
+mirBytes(B) => B
 ```
-Note: This transformation should have happened already. If a place has been missed, where a `Sort` has not been replaced with `MIRsort`, this should be trasformed. Also, this should happen for any other primitive sorts.
 
 - Similarly, productions should not directly include the List sort. They should instead use a different sort in its place, and then annotate the corresponding production with mir-klist-{ElementSort of the List}, e.g.,
 ```

kmir/src/kmir/convert_from_definition/v2parser.py

@@ -204,6 +204,9 @@ def _parse_mir_json(self, json: JSON, sort: KSort) -> ParseResult:
             case 'mir-bool':
                 assert len(prods) == 1
                 return self._parse_mir_bool_json(json, prod)
+            case 'mir-bytes':
+                assert len(prods) == 1
+                return self._parse_mir_bytes_json(json, prod)
             case _:
                 raise AssertionError()
 
@@ -415,6 +418,31 @@ def _parse_mir_bool_json(self, json: JSON, prod: KProduction) -> ParseResult:
         # Apply the production to the generated bool token
         return KApply(symbol, (KToken(str(json), KSort('Bool')))), sort
 
+    # parse a sequence of ints into a byte array
+    def _parse_mir_bytes_json(self, json: JSON, prod: KProduction) -> ParseResult:
+        assert isinstance(json, Sequence)
+
+        if not json:  # empty sequence, the assertion below would fail
+            bytes = ''
+        else:
+            for i in json:
+                # null values are allowed and taken to mean \x00
+                assert isinstance(i, int) or i is None
+            import string
+
+            if all(chr(int(i)) in string.printable for i in json):
+                # if all elements are ascii printable, use simple characters
+                bytes = ''.join([chr(int(i)) for i in json])
+            else:
+                # otherwise convert to hexadecimal representation \xCA\xFE
+                bytes = ''.join([f'\\x{i:02x}' if i is not None else '\\x00' for i in json])
+        symbol = _get_label(prod)
+        if symbol == 'MIRBytes::Bytes':
+            return KToken('b"' + str(bytes) + '"', KSort('Bytes')), KSort('Bytes')
+        else:
+            sort = prod.sort
+            return KApply(symbol, (KToken('b"' + str(bytes) + '"', KSort('Bytes')))), sort
+
     @cached_property
     def _mir_productions(self) -> tuple[KProduction, ...]:
         return tuple(prod for prod in self.__definition.productions if _is_mir_production(prod))

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

@@ -36,7 +36,7 @@ syntax GlobalAlloc ::= globalAllocEntry(MIRInt, GlobalAllocKind)
 syntax GlobalAllocs ::= List {GlobalAlloc, ""}
          [symbol(GlobalAllocs::append), terminator-symbol(GlobalAllocs::empty), group(mir-list)]
 
-syntax AllocId ::= allocId(Int) [symbol(allocId)]
+syntax AllocId ::= allocId(Int) [group(mir-int), symbol(allocId)]
 
 endmodule
 ```

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

@@ -167,7 +167,6 @@ syntax AggregateKind ::= aggregateKindArray(Ty)
                        | aggregateKindCoroutine(CoroutineDef, GenericArgs, Movability)                                  [group(mir-enum), symbol(AggregateKind::Coroutine)]
                        | aggregateKindRawPtr(Ty, Mutability)                                                            [group(mir-enum), symbol(AggregateKind::RawPtr)]
 
- // FIXME the arguments for some of these are _heterogenous lists_ in stable-mir-json
 syntax Rvalue ::= rvalueAddressOf(Mutability, Place)                     [group(mir-enum), symbol(Rvalue::AddressOf)]
                 | rvalueAggregate(AggregateKind, Operands)               [group(mir-enum), symbol(Rvalue::Aggregate)]
                 | rvalueBinaryOp(BinOp, Operand, Operand)                [group(mir-enum), symbol(Rvalue::BinaryOp)]

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

@@ -37,6 +37,7 @@ module TYPES
   imports TYPES-SORTS
   imports INT
   imports STRING
+  imports BYTES
   imports LIST
 
 syntax TestSort2 ::= testSort2(MIRInt, MyList)     [group(mir), symbol(testSort2)]
@@ -48,6 +49,8 @@ syntax MIRBool ::= mirBool(Bool)       [group(mir-bool), symbol(MIRBool::Bool)]
                  | Bool
 syntax MIRString ::= mirString(String) [group(mir-string), symbol(MIRString::String)]
                    | String
+syntax MIRBytes ::= mirBytes(Bytes)    [group(mir-bytes), symbol(MIRBytes::Bytes)]
+                  | Bytes
 
 syntax LineInfo ::= lineInfo(startLine: MIRInt, startCol: MIRInt, endLine: MIRInt, endCol: MIRInt)
 syntax InitMaskMaterialized ::= List {MIRInt, ""}
@@ -255,21 +258,16 @@ syntax MaybePromoted ::= promoted(Int) [group(mir-option-int)]
 
 syntax Align ::= align(Int) [group(mir-int), symbol(align)]
 
-// FIXME provSize and allocId are in a _list_ in json
-syntax ProvenanceMapEntry ::= // provenanceMapEntry(provSize: MIRInt, allocId: AllocId) [group(mir), symbol(provenanceMapEntry)]
-                              List [group(mir-klist-MIRInt)]
+syntax ProvenanceMapEntry ::= provenanceMapEntry(provSize: MIRInt, allocId: AllocId)
+                              [group(mir), symbol(provenanceMapEntry)]
 
 syntax ProvenanceMapEntries ::= List {ProvenanceMapEntry, ""}
                                 [group(mir-list), symbol(ProvenanceMapEntries::append), terminator-symbol(ProvenanceMapEntries::empty)]
 
 syntax ProvenanceMap ::= provenanceMap(ptrs: ProvenanceMapEntries) [group(mir---ptrs), symbol(provenanceMap)]
 
-// FIXME why are the bytes optional? What does it mean???
-syntax AllocByte ::= someByte(Int) [group(mir-option-int), symbol(someByte)]
-                   | "noByte"      [group(mir-option), symbol(noByte)]
-syntax AllocBytes ::= List {AllocByte, ""} [group(mir-list), symbol(AllocBytes::append), terminator-symbol(AllocBytes::empty)]
 syntax Allocation ::= allocation(
-                        bytes: AllocBytes,
+                        bytes: MIRBytes,
                         provenance: ProvenanceMap,
                         align: Align,
                         mutability: Mutability)
@@ -363,8 +361,8 @@ syntax ClauseKind ::= clauseKindTrait(TraitPredicate)                   [group(m
                     | clauseKindConstEvaluatable(TyConst)               [group(mir-enum), symbol(ClauseKind::ConstEvaluatable)]
 
 syntax TraitPredicate ::= traitPredicate(traitDef: TraitDef, polarity: PredicatePolarity) [group(mir---traitDef--polarity)]
-syntax RegionOutlivesPredicate ::= regionOutlivesPredicate(Region, Region)                [group(mir)] // FIXME field names??
-syntax TypeOutlivesPredicate ::= typeOutlivesPredicate(Ty, Region)                        [group(mir)] // FIXME field names??
+syntax RegionOutlivesPredicate ::= regionOutlivesPredicate(Region, Region)                [group(mir)]
+syntax TypeOutlivesPredicate ::= typeOutlivesPredicate(Ty, Region)                        [group(mir)]
 syntax ProjectionPredicate ::= projectionPredicate(projectionTy: AliasTy, term: TermKind) [group(mir---projectionTy--term)]
 
 syntax SubtypePredicate ::= subtypePredicate(a: Ty, b: Ty) [group(mir---a--b)]