Updates from master (#865)

* `sizeOf` and `alignOf`
* `union` values and their fields
* one more byte simplification

Author: jberthold

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/kmir.md

@@ -100,11 +100,25 @@ will effectively be no-ops at this level).
 ```k
 
   // all memory accesses relegated to another module (to be added)
-  rule [execStmt]: <k> #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN))
+  rule [execStmt]: <k> #execStmt(statement(statementKindAssign(place(local(I), _PROJ) #as PLACE, RVAL), _SPAN))
          =>
             #setLocalValue(PLACE, RVAL)
          ...
        </k>
+       <locals> LOCALS </locals>
+       requires 0 <=Int I andBool I <Int size(LOCALS)
+        andBool notBool #isUnionType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
+       [preserves-definedness]
+
+  rule [execStmt.union]: <k> #execStmt(statement(statementKindAssign(place(local(I), _PROJ) #as PLACE, RVAL), _SPAN))
+         =>
+            #setLocalValue(PLACE, #evalUnion(RVAL))
+         ...
+       </k>
+       <locals> LOCALS </locals>
+       requires 0 <=Int I andBool I <Int size(LOCALS)
+        andBool #isUnionType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
+       [preserves-definedness]
 
   // RVAL evaluation is implemented in rt/data.md
 

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

@@ -208,6 +208,25 @@ This avoids building up large expressions related to overflow checks and vacuous
     [simplification, preserves-definedness, symbolic]
 ```
 
+Another more general simplification relates a `NUMBER` and the bytes from its representation.
+If the number is initially masked at 64 bits (`&Int bitmask64`), it is guaranteed to be positive
+and therefore the masked value equals its bytes taken individually and multiplied.
+Terms like this have been observed as branching conditions in a proof that heavily uses `[u8;8] <--> u64` conversions.
+The simplification eliminates the vacuous branches instantly.
+
+```k
+  rule ((NUMBER &Int bitmask64) &Int bitmask8) +Int 256 *Int (
+         ((NUMBER &Int bitmask64) >>Int 8 &Int bitmask8) +Int 256 *Int (
+           ((NUMBER &Int bitmask64) >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
+             ((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
+               ((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
+                 ((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
+                   ((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8) +Int 256 *Int (
+                     ((NUMBER &Int bitmask64) >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int bitmask8))))))))
+         &Int bitmask64
+         => NUMBER &Int bitmask64
+    [simplification, preserves-definedness, symbolic(NUMBER)]
+```
 
 For the case where the (symbolic) byte values are first converted to a number, the round-trip simplification requires different matching.
 First, the bit-masking with `&Int 255` eliminates `Bytes2Int(Int2Bytes(1, ..) +Bytes ..)` enclosing a byte-valued variable:

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

@@ -312,6 +312,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
 
   // retains information about the value that was deconstructed by a projection
   syntax Context ::= CtxField( VariantIdx, List, Int , Ty )
+                   | CtxFieldUnion( FieldIdx, Value, Ty )
                    | CtxIndex( List , Int ) // array index constant or has been read before
                    | CtxSubslice( List , Int , Int ) // start and end always counted from beginning
                    | CtxPointerOffset( List, Int, Int ) // pointer offset for accessing elements with an offset (Offset, Origin Length)
@@ -329,6 +330,10 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
       => #buildUpdate(Aggregate(IDX, ARGS[I <- VAL]), CTXS)
      [preserves-definedness] // valid list indexing checked upon context construction
 
+  rule #buildUpdate(VAL, CtxFieldUnion(FIELD_IDX, _ARG, _TY) CTXS)
+      => #buildUpdate(Union(FIELD_IDX, VAL), CTXS)
+     [preserves-definedness]
+
   rule #buildUpdate(VAL, CtxIndex(ELEMS, I) CTXS)
       => #buildUpdate(Range(ELEMS[I <- VAL]), CTXS)
      [preserves-definedness] // valid list indexing checked upon context construction
@@ -400,7 +405,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
   rule originSize(dynamicSize(SIZE)) => SIZE
 ```
 
-#### Aggregates
+#### Aggregates (not Union)
 
 A `Field` access projection operates on `struct`s and tuples, which are represented as `Aggregate` values.
 The field is numbered from zero (in source order), and the field type is provided (not checked here).
@@ -445,6 +450,28 @@ This is done without consideration of the validity of the Downcast[^downcast].
        </k>
 ```
 
+#### Unions
+```k
+  // Case: Union is in same state as field projection
+  rule <k> #traverseProjection(
+             DEST,
+             Union(FIELD_IDX, ARG),
+             projectionElemField(FIELD_IDX, TY) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(
+             DEST,
+             ARG,
+             PROJS,
+             CtxFieldUnion(FIELD_IDX, ARG, TY) CTXTS
+           )
+        ...
+        </k>
+    [preserves-definedness]
+
+  // TODO: Case: Union is in different state as field projection
+```
+
 #### Ranges
 
 An `Index` projection operates on an array or slice (`Range`) value, to access an element of the array.
@@ -934,6 +961,7 @@ Literal arrays are also built using this RValue.
 
   // #mkAggregate produces an aggregate TypedLocal value of given kind from a preceeding list of values
   syntax Value ::= #mkAggregate ( AggregateKind )
+                 | #mkUnion ( FieldIdx )
 
   rule <k> ARGS:List ~> #mkAggregate(aggregateKindAdt(_ADTDEF, VARIDX, _, _, _))
         =>
@@ -977,6 +1005,26 @@ Literal arrays are also built using this RValue.
        </k>
 ```
 
+While Unions are Aggregate in the MIR, we distinguish between them because the semantics
+are different. For example, field accesses to not access different data, but interpret
+that data as a different type.
+```k
+  syntax Rvalue ::= #evalUnion ( Rvalue )
+
+  rule <k> #evalUnion(rvalueAggregate(aggregateKindAdt( _, _, _, _, someFieldIdx ( FIELD )), ARGS))
+        =>
+           #readOperands(ARGS) ~> #mkUnion(FIELD)
+       ...
+      </k>
+
+  rule <k> ListItem(ARG) .List ~> #mkUnion(FIELD)
+        =>
+            Union(FIELD, ARG)
+        ...
+       </k>
+
+```
+
 The `AggregateKind::RawPtr`, somewhat as a special case of a `struct` aggregate, constructs a raw pointer
 from a given data pointer and metadata[^rawPtrAgg]. In case of a _thin_ pointer, the metadata is a unit value,
 for _fat_ pointers it is a `usize` value indicating the data length.
@@ -1063,6 +1111,7 @@ This eliminates any `Deref` projections from the place, and also resolves `Index
   rule #projectionsFor( CtxSubslice(_, I, J) CTXS, PROJS) => #projectionsFor(CTXS,      projectionElemSubslice(I, J, false) PROJS)
   // rule #projectionsFor(CtxPointerOffset(OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSubslice(OFFSET, ORIGIN_LENGTH, false) PROJS)
   rule #projectionsFor(CtxPointerOffset( _, OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS)
+  rule #projectionsFor(CtxFieldUnion(F_IDX, _, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(F_IDX, TY) PROJS)
 
   // Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule.
   rule <k> rvalueRef(REGION, KIND, place(local(I), PROJS))
@@ -2075,12 +2124,18 @@ Since our arithmetic operations signal undefined behaviour on overflow independe
 
 #### "Nullary" operations reifying type information
 
-`nullOpSizeOf`
-`nullOpAlignOf`
-`nullOpOffsetOf(VariantAndFieldIndices)`
+Operation `nullOpSizeOf` returns the size in bytes of a data structure or primitive type, as a `usize`.
+Operation `nullOpAlignOf` returns the required alignment of a data structure or primitive type, as a `usize`.
+This information is read from the layout in the `TypeInfo` if available, or a fixed constant for primitive types.
 
 ```k
 // FIXME: 64 is hardcoded since usize not supported
+rule <k> rvalueNullaryOp(nullOpSizeOf, TY)
+      =>
+           Integer(#sizeOf(lookupTy(TY)), 64, false)
+         ...
+     </k>
+    requires lookupTy(TY) =/=K typeInfoVoidType
 rule <k> rvalueNullaryOp(nullOpAlignOf, TY)
       =>
            Integer(#alignOf(lookupTy(TY)), 64, false)
@@ -2089,6 +2144,8 @@ rule <k> rvalueNullaryOp(nullOpAlignOf, TY)
     requires lookupTy(TY) =/=K typeInfoVoidType
 ```
 
+`nullOpOffsetOf(VariantAndFieldIndices)`
+
 #### Other operations
 
 The unary operation `unOpPtrMetadata`, when given a reference or pointer to a slice, will return the reference or pointer metadata.

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

@@ -147,31 +147,6 @@ This truncation function is instrumental in the implementation of Integer arithm
     [preserves-definedness]
 ```
 
-## Alignment of Primitives
-
-```k
-// FIXME: Alignment is platform specific
-syntax Int ::= #alignOf( TypeInfo ) [function]
-rule #alignOf( typeInfoPrimitiveType(primTypeBool) )        => 1
-rule #alignOf( typeInfoPrimitiveType(primTypeChar) )        => 4
-rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyIsize)) )  => 8 // FIXME: Hard coded since usize not implemented
-rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI8)) )     => 1
-rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI16)) )    => 2
-rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI32)) )    => 4
-rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI64)) )    => 8
-rule #alignOf( typeInfoPrimitiveType(primTypeInt(intTyI128)) )   => 16
-rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyUsize)) ) => 8 // FIXME: Hard coded since usize not implemented
-rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU8)) )    => 1
-rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU16)) )   => 2
-rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU32)) )   => 4
-rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU64)) )   => 8
-rule #alignOf( typeInfoPrimitiveType(primTypeUint(uintTyU128)) )  => 16
-rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF16)) )  => 2
-rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF32)) )  => 4
-rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF64)) )  => 8
-rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF128)) ) => 16
-```
-
 ```k
 endmodule
 ```

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

@@ -88,6 +88,15 @@ Pointers to structs with a single zero-offset field are compatible with pointers
   rule #layoutOffsets(_) => .MachineSizes [owise]
 ```
 
+Helper function to identify an `union` type, this is needed so `#setLocalValue`
+will not create an `Aggregate` instead of a `Union` `Value`.
+```k
+  syntax Bool ::= #isUnionType ( TypeInfo ) [function, total]
+  // --------------------------------------------------------
+  rule #isUnionType(typeInfoUnionType(_NAME, _ADTDEF, _FIELDS, _LAYOUT) ) => true
+  rule #isUnionType(_)                                                    => false [owise]
+```
+
 ## Determining types of places with projection
 
 A helper function `getTyOf` traverses type metadata (using the type metadata map `Ty -> TypeInfo`) along the applied projections to determine the `Ty` of the projected place.
@@ -203,6 +212,72 @@ Slices, `str`s  and dynamic types require it, and any `Ty` that `is_sized` does
   rule #zeroSizedType(_) => false [owise]
 ```
 
+## Alignment and Size of Types as per `TypeInfo`
+
+The `alignOf` and `sizeOf` nullary operations return the alignment / size in bytes as a `usize`.
+This information is either hard-wired for primitive types (numbers, first and foremost), or read from the layout in `TypeInfo`.
+
+```k
+  syntax Int ::= #sizeOf ( TypeInfo )  [function, total]
+               | #alignOf ( TypeInfo ) [function, total]
+
+  // primitive int types: use bit width (both for size and alignment)
+  rule #sizeOf(typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
+  rule #alignOf(typeInfoPrimitiveType(primTypeInt(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
+  rule #alignOf(typeInfoPrimitiveType(primTypeUint(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
+  rule #alignOf(typeInfoPrimitiveType(primTypeFloat(NUMTY))) => #bitWidth(NUMTY) /Int 8 [preserves-definedness]
+  // bool and char
+  rule #sizeOf(typeInfoPrimitiveType(primTypeBool))  => 1
+  rule #alignOf(typeInfoPrimitiveType(primTypeBool)) => 1
+  rule #sizeOf(typeInfoPrimitiveType(primTypeChar))  => 4
+  rule #alignOf(typeInfoPrimitiveType(primTypeChar)) => 4
+  // The str primitive has alignment of a Char but size 0 (indicating dynamic size)
+  rule #sizeOf(typeInfoPrimitiveType(primTypeStr))  => 0
+  rule #alignOf(typeInfoPrimitiveType(primTypeStr)) => 4
+  // enums, structs , and tuples provide the values from their layout information
+  rule #sizeOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(   BITS     ))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoEnumType(_, _, _, _, noLayoutShape)) => 0
+  rule #alignOf(typeInfoEnumType(_, _, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
+  rule #alignOf(typeInfoEnumType(_, _, _, _, noLayoutShape)) => 1
+  // struct
+  rule #sizeOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(   BITS     ))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoStructType(_, _, _, noLayoutShape)) => 0
+  rule #alignOf(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
+  rule #alignOf(typeInfoStructType(_, _, _, noLayoutShape)) => 1
+  // tuple
+  rule #sizeOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize(   BITS     ))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, _, machineSize(mirInt(BITS)))))) => BITS /Int 8 [preserves-definedness]
+  rule #sizeOf(typeInfoTupleType(_, noLayoutShape)) => 0
+  rule #alignOf(typeInfoTupleType(_, someLayoutShape(layoutShape(_, _, _, align(BYTES),_)))) => BYTES
+  rule #alignOf(typeInfoTupleType(_, noLayoutShape)) => 1
+  // 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
+  rule #alignOf(typeInfoArrayType(ELEM_TY, _)) => #alignOf(lookupTy(ELEM_TY))
+  // thin ptr and ref types have the size of `usize` and twice that for fat pointers/refs. Alignment is that of `usize`
+  rule #sizeOf(typeInfoPtrType(POINTEE_TY))
+    => #sizeOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
+          *Int (#if #metadataSize(POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi)
+  rule #sizeOf(typeInfoRefType(POINTEE_TY))
+    => #sizeOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
+          *Int (#if #metadataSize(POINTEE_TY) ==K dynamicSize(1) #then 2 #else 1 #fi)
+  rule #alignOf(typeInfoPtrType(_)) => #alignOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
+  rule #alignOf(typeInfoRefType(_)) => #alignOf(typeInfoPrimitiveType(primTypeUint(uintTyUsize)))
+  // other types (fun and void types) have size and alignment 0
+  rule #sizeOf(_)  => 0 [owise]
+  rule #alignOf(_) => 0 [owise]
+```
+
 ```k
 endmodule
 ```

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

@@ -36,7 +36,10 @@ The special `Moved` value represents values that have been used and should not b
                  | StringVal( String )                    [symbol(Value::StringVal)]
                    // UTF-8 encoded Unicode string
                  | Aggregate( VariantIdx , List )         [symbol(Value::Aggregate)]
-                   // heterogenous value list        for tuples and structs (standard, tuple, or anonymous)
+                   // heterogenous value list        for tuples, enum, and structs (standard, tuple, or anonymous)
+                 | Union( FieldIdx, Value )               [symbol(Value::Union)]
+                   // A union is an Aggregate, but we differentiate it from the other Aggregates.
+                   // The Value is the data, and FieldIdx determines the type from the union's fields
                  | Float( Float, Int )                    [symbol(Value::Float)]
                    // value, bit-width               for f16-f128
                  | Reference( Int , Place , Mutability , Metadata )