Union Value Sort (#861)

This PR separates a `Value` sort for `Union` out of `Aggregate` as there
are different semantics for the projections (and it also makes the code
clearer). A `Union` has one argument which is data, but it can be
interpreted as different types via field projections - this is
significantly different from other field projections that access
different data via different arguments.

Currently the implementation only supports accessing fields of the same
type as the `Union` construction (no switching between types right now).

Author: dkcumming

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

@@ -97,11 +97,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/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))

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) )  => 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.

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 )

kmir/src/kmir/kmir.py

@@ -74,7 +74,12 @@ def cut_point_rules(
         if break_on_thunk:
             cut_point_rules.append('RT-DATA.thunk')
         if break_every_statement or break_every_step:
-            cut_point_rules.append('KMIR-CONTROL-FLOW.execStmt')
+            cut_point_rules.extend(
+                [
+                    'KMIR-CONTROL-FLOW.execStmt',
+                    'KMIR-CONTROL-FLOW.execStmt.union',
+                ]
+            )
         if break_on_terminator_goto or break_every_terminator or break_every_step:
             cut_point_rules.append('KMIR-CONTROL-FLOW.termGoto')
         if break_on_terminator_switch_int or break_every_terminator or break_every_step:

kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs

@@ -4,4 +4,4 @@ fn main() {
     for elem in arr {
         assert!(elem != 0);
     }
-}
+}

kmir/src/tests/integration/data/prove-rs/maybe-uninit.rs

@@ -0,0 +1,7 @@
+use std::mem::MaybeUninit;
+fn main() {
+    let m_init = MaybeUninit::new(1);
+    let init = unsafe { m_init.assume_init() };
+
+    assert!(init == 1);
+}

kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (75 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 1 ) , Union ( fieldIdx ( 0 ) , Integer ( -1 , 8
+    function: main
+    span: 59
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/data/prove-rs/unions-fail.rs

@@ -0,0 +1,16 @@
+union Union {
+    signed: i8,
+    unsigned: u8,
+}
+
+fn main() {
+    let s = Union { signed: -1 };
+    let u = Union { unsigned: 255 };
+    unsafe {
+        assert!(s.signed == -1);
+        assert!(u.unsigned == 255);
+
+        assert!(s.unsigned == 255);
+        assert!(u.signed == -1);
+    }
+}

kmir/src/tests/integration/test_integration.py

@@ -56,6 +56,7 @@
     'transmute-u8-to-enum-changed-discriminant-signed-fail',
     'assert-inhabited-fail',
     'iterator-simple-fail',
+    'unions-fail',
 ]