Updates from master (#869)

* `CastKind::Transmute` for `T -> std::mem::MaybeUninit<T>` (#863) -
single element case

Author: jberthold

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

@@ -1017,6 +1017,12 @@ that data as a different type.
        ...
       </k>
 
+  rule <k> #evalUnion(rvalueCast(_, _, _) #as CAST)
+        =>
+           CAST
+       ...
+      </k>
+
   rule <k> ListItem(ARG) .List ~> #mkUnion(FIELD)
         =>
             Union(FIELD, ARG)
@@ -1628,8 +1634,7 @@ index; if not, return `#UBErrorInvalidDiscriminantsInEnumCast`.
   rule #isEnumWithoutFields(typeInfoEnumType(_, _, _, FIELDSS, _)) => #noFields(FIELDSS)
   rule #isEnumWithoutFields(_OTHER) => false [owise]
 
-  // TODO: Connect this with MirError
-  syntax Evaulation ::= "#UBErrorInvalidDiscriminantsInEnumCast"
+  syntax MIRError ::= "#UBErrorInvalidDiscriminantsInEnumCast"
   rule <k>
            #cast( Integer ( VAL , WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) ~> _REST
         =>
@@ -1664,6 +1669,39 @@ index; if not, return `#UBErrorInvalidDiscriminantsInEnumCast`.
   rule #validDiscriminantAux( _VAL, .Discriminants ) => false
 ```
 
+The type `std::mem::MaybeUninit` is a union that represents a potentially uninitialised location in memory.
+This union has two fields, first `()`, and second `std::mem::ManuallyDrop<T>` which represents the initialised data.
+When [converting an array to an iterator](https://github.com/rust-lang/rust/blob/a2545fd6fc66b4323f555223a860c451885d1d2b/library/core/src/array/iter.rs#L57-L70)
+a `Transmute` cast is invoked for the array element type (`T` from `[T; N]`) into `std::mem::MaybeUninit<T>`. Therefore,
+it is required for iterator use that we handle this transmute. There are details in the safety comment linked above for
+the safety of this cast. The logic of the semantics and saftey of this cast for us is:
+- that there is a `Value` to be cast as we cannot construct a `Value` that is not initialised;
+- that the type being cast from `T` is the same as the type of the unions second field `std::mem::ManuallyDrop<T>`;
+- we can then then create a union that is constructed with the second field, instantiating the `Value` in a struct;
+- otherwise we error so that the cast does not `thunk`.
+```k
+  syntax MIRError ::= "#UBInvalidTransmuteMaybeUninit"
+  rule <k>
+           #cast( _VAL:Value , castKindTransmute , TY_FROM , TY_TO )
+        =>
+           #UBInvalidTransmuteMaybeUninit
+       ...
+      </k>
+      requires #isUnionType(lookupTy(TY_TO))
+        andBool #typeNameIs(lookupTy(TY_TO), "std::mem::MaybeUninit<")
+        andBool TY_FROM =/=K getFieldTy(#lookupMaybeTy(getFieldTy(lookupTy(TY_TO), 1)), 0)
+
+  rule <k>
+           #cast( VAL:Value , castKindTransmute , TY_FROM , TY_TO )
+        =>
+           Union( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem(VAL) .List ))
+       ...
+      </k>
+      requires #isUnionType(lookupTy(TY_TO))
+        andBool #typeNameIs(lookupTy(TY_TO), "std::mem::MaybeUninit<")
+        andBool TY_FROM ==K getFieldTy(#lookupMaybeTy(getFieldTy(lookupTy(TY_TO), 1)), 0)
+```
+
 
 ### Other casts involving pointers
 

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

@@ -119,13 +119,36 @@ To make this function total, an optional `MaybeTy` is used.
     requires #zeroFieldOffset(LAYOUT)
   rule #transparentDepth(_) => 0 [owise]
 
-  syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total]
+  syntax String ::= #typeName ( TypeInfo ) [function, total]
+  // -------------------------------------------------------
+  rule #typeName(typeInfoUnionType(NAME, _, _, _)) => NAME
+  rule #typeName(typeInfoStructType(NAME, _, _, _)) => NAME
+  rule #typeName(typeInfoEnumType(NAME, _, _, _, _)) => NAME
+  rule #typeName(_) => "" [owise]
+
+  syntax Bool ::= #typeNameIs( TypeInfo, String ) [function, total]
+  // --------------------------------------------------------------
+  rule #typeNameIs( TY_TO, STRING) => findString(#typeName(TY_TO), STRING, 0) ==Int 0
+
+  syntax MaybeTy ::= getFieldTy ( TypeInfo , Int ) [function, total]
+  // ---------------------------------------------------------------
+  rule getFieldTy(typeInfoStructType(_, _, FIELDS, _) , IDX) => getFieldTyFromList(FIELDS, IDX)
+  rule getFieldTy(typeInfoUnionType(_, _, FIELDS, _)  , IDX) => getFieldTyFromList(FIELDS, IDX)
+  rule getFieldTy(_, _) => TyUnknown [owise]
+
+  syntax MaybeTy ::= getFieldTyFromList ( Tys , Int ) [function, total]
+  // ------------------------------------------------------------------
+  rule getFieldTyFromList(FIELD _REST, 0) => FIELD
+  rule getFieldTyFromList(_ REST, IDX) => getFieldTyFromList(REST, IDX -Int 1) requires IDX >Int 0
+  rule getFieldTyFromList(_, _) => TyUnknown [owise]
 
+  syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total]
+  // -------------------------------------------------------------
   rule #lookupMaybeTy(TY:Ty) => lookupTy(TY)
   rule #lookupMaybeTy(TyUnknown) => typeInfoVoidType
 
   syntax MaybeTy ::= getTyOf( MaybeTy , ProjectionElems ) [function, total]
-  // -----------------------------------------------------------
+  // ----------------------------------------------------------------------
   rule getTyOf(TyUnknown,             _                      ) => TyUnknown
   rule getTyOf(TY,                    .ProjectionElems       ) => TY
 

kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected

@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (15 steps)
+└─ 3 (stuck, leaf)
+    #ProgramError ( #UBInvalidTransmuteMaybeUninit )
+~> #freezer#setLocalValue(_,_)_
+    function: main
+    span: 60
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected

@@ -3,9 +3,9 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (13 steps)
+│  (14 steps)
 └─ 3 (stuck, leaf)
-    #UBErrorInvalidDiscriminantsInEnumCast ~> .K
+    #ProgramError ( #UBErrorInvalidDiscriminantsInEnumCast ) ~> .K
     function: main
 
 

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

@@ -0,0 +1,10 @@
+#![feature(core_intrinsics)]
+use std::mem::MaybeUninit;
+
+fn main() {
+    unsafe {
+        let maybe_unsigned = std::intrinsics::transmute::<i128, MaybeUninit::<u128>>(9999);
+                                  // Note different types ^^^^                ^^^^
+        assert!(maybe_unsigned.assume_init() == 9999);
+    }
+}

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

@@ -0,0 +1,18 @@
+#![feature(core_intrinsics)]
+use std::mem::MaybeUninit;
+
+struct Something([u8; 3]);
+
+fn main() {
+    unsafe {
+        let maybe_signed = std::intrinsics::transmute_unchecked::<i32, MaybeUninit::<i32>>(42);
+        assert!(maybe_signed.assume_init() == 42);
+
+        let maybe_unsigned = std::intrinsics::transmute::<u128, MaybeUninit::<u128>>(9999);
+        assert!(maybe_unsigned.assume_init() == 9999);
+
+        let something = Something([1, 2, 3]);
+        let maybe_something = std::intrinsics::transmute::<Something, MaybeUninit::<Something>>(something);
+        assert!(maybe_something.assume_init().0 == [1, 2, 3]);
+    }
+}

kmir/src/tests/integration/test_integration.py

@@ -58,6 +58,7 @@
     'assert-inhabited-fail',
     'iterator-simple-fail',
     'unions-fail',
+    'transmute-maybe-uninit-fail',
 ]