Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

Makefile

@@ -132,6 +132,7 @@ update-exec-smir:
 
 # Update checked-in smir.json files (using stable-mir-json dependency and jq)
 # file paths for spans in the the updated smir are truncated to known infixes
+# Compiles run-smir-random files as libraries, others as binaries
 .PHONY: update-smir-json
 update-smir-json: TARGETS = $(shell git ls-files | grep -e ".*\.smir\.json$$" | grep -v -e pinocchio)
 update-smir-json: SMIR = cargo -q -Z unstable-options -C deps/stable-mir-json run --
@@ -140,7 +141,11 @@ update-smir-json: stable-mir-json
 		dir=$$(realpath $$(dirname $$file)); \
 		rust=$$dir/$$(basename $${file%.smir.json}.rs); \
 		[ -f "$$rust" ] || (echo "Source file $$rust missing."; exit 1); \
-		${SMIR} -Zno-codegen --out-dir $$dir $$rust; \
+		if echo "$$file" | grep -q "run-smir-random"; then \
+			${SMIR} --crate-type=lib --out-dir $$dir $$rust; \
+		else \
+			${SMIR} -Zno-codegen --out-dir $$dir $$rust; \
+		fi; \
 		jq '.spans[].[1].[0] |= sub("/.*lib/rustlib"; "rustlib") | .spans[].[1].[0] |= sub("/.*/integration/data"; "data")' $$file > $$file.tmp; \
 		mv $$file.tmp $$file; \
 	done

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

@@ -93,8 +93,8 @@ will not create an `Aggregate` instead of a `Union` `Value`.
 ```k
   syntax Bool ::= #isUnionType ( TypeInfo ) [function, total]
   // --------------------------------------------------------
-  rule #isUnionType(typeInfoUnionType(_NAME, _ADTDEF) )  => true
-  rule #isUnionType(_)                                   => false [owise]
+  rule #isUnionType(typeInfoUnionType(_NAME, _ADTDEF, _FIELDS, _LAYOUT) ) => true
+  rule #isUnionType(_)                                                    => false [owise]
 ```
 
 ## Determining types of places with projection
@@ -254,9 +254,12 @@ This information is either hard-wired for primitive types (numbers, first and fo
   rule #sizeOf(typeInfoTupleType(_, noLayoutShape)) => 0
   rule #alignOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
   rule #alignOf(typeInfoTupleType(_, noLayoutShape)) => 1
-  // size of union types: FIXME use layout (currently not in K AST)
-  // rule #sizeOf(typeInfoUnionType(_, _)) => FIXME
-  // rule #alignOf(typeInfoUnionType(_, _)) => FIXME
+  // union
+  rule #sizeOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(   BITS     ))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoUnionType(_, _, _, noLayoutShape)) => 0
+  rule #alignOf(typeInfoUnionType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
+  rule #alignOf(typeInfoUnionType(_, _, _, noLayoutShape)) => 1
   // arrays with known length have the alignment of the element type, and a size multiplying element count and element size
   rule #sizeOf(typeInfoArrayType(ELEM_TY, someTyConst(tyConst(KIND, _)))) => #sizeOf(lookupTy(ELEM_TY)) *Int readTyConstInt(KIND)
   rule #sizeOf(typeInfoArrayType(  _    ,    noTyConst                 )) => 0

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

@@ -270,7 +270,11 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
                       , adtDef: AdtDef
                       , fields: Tys
                       , layout: MaybeLayoutShape)             [symbol(TypeInfo::StructType)   , group(mir-enum---name--adt-def--fields--layout)]
-                    | typeInfoUnionType(MIRString, AdtDef)       [symbol(TypeInfo::UnionType)    , group(mir-enum---name--adt-def)]
+                    | typeInfoUnionType(
+                        name: MIRString
+                      , adtDef: AdtDef
+                      , fields: Tys
+                      , layout: MaybeLayoutShape)             [symbol(TypeInfo::UnionType)    , group(mir-enum---name--adt-def--fields--layout)]
                     | typeInfoArrayType(Ty, MaybeTyConst)        [symbol(TypeInfo::ArrayType)    , group(mir-enum---elem-type--size)]
                     | typeInfoPtrType(Ty)                        [symbol(TypeInfo::PtrType)      , group(mir-enum---pointee-type)]
                     | typeInfoRefType(Ty)                        [symbol(TypeInfo::RefType)      , group(mir-enum---pointee-type)]
@@ -299,7 +303,7 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
                             | "noLayoutShape"              [group(mir-option)]
 
   syntax FieldsShape ::= "fieldsShapePrimitive"                     [group(mir-enum), symbol(FieldsShape::Primitive)]
-                       | fieldsShapeUnion(/* TODO */)               [group(mir-enum), symbol(FieldsShape::Union)]
+                       | fieldsShapeUnion(MIRInt)                   [group(mir-enum), symbol(FieldsShape::Union)]
                        | fieldsShapeArray(/* TODO */)               [group(mir-enum), symbol(FieldsShape::Array)]
                        | fieldsShapeArbitrary(FieldsShapeArbitrary) [group(mir-enum), symbol(FieldsShape::Arbitrary)]
 

kmir/src/kmir/linker.py

@@ -235,6 +235,7 @@ def apply_offset_type_info(typeinfo: dict, offset: int) -> dict:
         typeinfo['StructType']['fields'] = [x + offset for x in typeinfo['StructType']['fields']]
         typeinfo['StructType']['adt_def'] += offset
     elif 'UnionType' in typeinfo:
+        typeinfo['UnionType']['fields'] = [x + offset for x in typeinfo['UnionType']['fields']]
         typeinfo['UnionType']['adt_def'] += offset
     elif 'ArrayType' in typeinfo:
         typeinfo['ArrayType']['elem_type'] += offset

kmir/src/kmir/ty.py

@@ -218,6 +218,8 @@ def from_raw(data: Any) -> FieldsShape:
         match data:
             case 'Primitive':
                 return PrimitiveFields()
+            case {'Union': count}:
+                return UnionFields(count=count)
             case {
                 'Arbitrary': {
                     'offsets': offsets,
@@ -234,6 +236,11 @@ def from_raw(data: Any) -> FieldsShape:
 class PrimitiveFields(FieldsShape): ...
 
 
+@dataclass
+class UnionFields(FieldsShape):
+    count: int
+
+
 @dataclass
 class ArbitraryFields(FieldsShape):
     offsets: list[MachineSize]
@@ -525,6 +532,8 @@ def nbytes(self, types: Mapping[Ty, TypeMetadata]) -> int:
 class UnionT(TypeMetadata):
     name: str
     adt_def: int
+    fields: list[Ty]
+    layout: LayoutShape | None
 
     @staticmethod
     def from_raw(data: Any) -> UnionT:
@@ -533,11 +542,15 @@ def from_raw(data: Any) -> UnionT:
                 'UnionType': {
                     'name': name,
                     'adt_def': adt_def,
+                    'fields': fields,
+                    'layout': layout,
                 }
             }:
                 return UnionT(
                     name=name,
                     adt_def=adt_def,
+                    fields=list(fields),
+                    layout=LayoutShape.from_raw(layout) if layout is not None else None,
                 )
             case _:
                 raise _cannot_parse_as('UnionT', data)