Update with latest master

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

@@ -23,71 +23,148 @@ This module contains helper functions to operate on this type information.
 
 ## Compatibility of types (high-level representation)
 
-When two types use the same representation for their values, these
-values, and pointers to them, can be converted from one type to the other.
-The `#typesCompatible` function determines this compatibility, and is by default `false`.
+When two types use the same (low-level) representation for their values, pointers to them can be converted from one type to the other.
+
+For compatible pointer types, the `#typeProjection` function computes a projection that can be appended to the pointer's projection
+to return the correct type when the pointer is cast to a different pointee type.
+Most notably, casting between arrays and single elements as well as casting to and from transparent wrappers.
+This projection computation happens _recursively_, for instance casting from `*const [[T]]` to `*const T`.
+
+The interface function is meant for pointer casts to compute pointee projections and returns nothing for other types.
 
 ```k
-  syntax Bool ::= #typesCompatible ( TypeInfo , TypeInfo ) [function, total]
+  syntax MaybeProjectionElems ::= ProjectionElems
+                                | "NoProjectionElems"
 
-  // by default, only identical types are compatible
-  rule #typesCompatible (             T            ,           T              ) => true  [priority(60)] 
-  rule #typesCompatible (             _            ,           _              ) => false [owise] 
+  syntax MaybeProjectionElems ::= #typeProjection ( TypeInfo , TypeInfo )    [function, total]
+  // ---------------------------------------------------------------------------------------
+  rule #typeProjection ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => #pointeeProjection(lookupTy(TY1), lookupTy(TY2))
+  rule #typeProjection ( _, _ ) => NoProjectionElems [owise]
 ```
 
-Arrays and slices are compatible if their element type is (ignoring length)
+Note that certain projections can cancel each other, such as casting from one transparent wrapper to another.
+In case of casting an element pointer to an array pointer, we rely on this cancellation to recover the array length
+(NB ultimately there needs to be an underlying array if there is more than one element in the original allocation).
+
+This can be done in an extended `append` function for projections, and already in the special cons function here. **TODO**
+
+The `#maybeConsProj` function is a "cons" for projection lists with a short-cut case for when the second argument is not a projection list.
+It also implements cancellation of inverse projections (such as casting from one transparent wrapper to another, or between arrays).
+
 ```k
-  rule #typesCompatible ( typeInfoArrayType(TY1, _), typeInfoArrayType(TY2, _)) => #typesCompatible(lookupTy(TY1), lookupTy(TY2))
+  syntax ProjectionElem ::= "projectionElemSingletonArray" // elem -> array. Incomplete information! (relies on cancellation, or caller must consider metadata)
+                          | "projectionElemWrapStruct"     // transparent wrapper (singleton struct)
+                          | "projectionElemToZST"          // cast to ZST (immaterial data)
+                          | "projectionElemFromZST"        // ...and back from ZST to something material (the two cancel out in sequence)
+
+  syntax MaybeProjectionElems ::= maybeConcatProj ( ProjectionElem, MaybeProjectionElems ) [function, total]
+
+  rule maybeConcatProj(PROJ, REST:ProjectionElems) => PROJ REST
+  rule maybeConcatProj(  _ , NoProjectionElems   ) => NoProjectionElems
+
+  // special cancellation rules with higher priority
+  rule maybeConcatProj(projectionElemSingletonArray, projectionElemConstantIndex(0, 0, false) REST:ProjectionElems) => REST [priority(40)]
+  rule maybeConcatProj(projectionElemConstantIndex(0, 0, false), projectionElemSingletonArray REST:ProjectionElems) => REST [priority(40)]
+
+  rule maybeConcatProj(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) REST:ProjectionElems) => REST [priority(40)]
+  // this rule would not be valid if the original pointee had more than one field. In the calling context, this won't occur, though.
+  rule maybeConcatProj(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct REST:ProjectionElems) => REST [priority(40)]
+
+  rule maybeConcatProj(projectionElemToZST, projectionElemFromZST REST:ProjectionElems) => REST [priority(40)]
+  rule maybeConcatProj(projectionElemFromZST, projectionElemToZST REST:ProjectionElems) => REST [priority(40)]
 ```
 
-Pointers are compatible if their pointee types are
+The `#pointeeProjection` function computes, for compatible pointee types, how to project from one pointee to the other.
+
 ```k
-  rule #typesCompatible ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => true
-    requires #typesCompatible(lookupTy(TY1), lookupTy(TY2))
-     [priority(59)]
+  syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total]
 ```
 
-Pointers to arrays/slices are compatible with pointers to the element type
+A short-cut rule for identical types takes preference.
+As a default, no projection elements are returned for incompatible types.
 ```k
-  rule #typesCompatible ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => true
-    requires #isArrayOf(lookupTy(TY1), TY2)
-
-  rule #typesCompatible ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => true
-    requires #isArrayOf(lookupTy(TY2), TY1)
+  rule #pointeeProjection(T , T) => .ProjectionElems  [priority(40)]
+  rule #pointeeProjection(_ , _) => NoProjectionElems [owise]
+```
 
-  syntax Bool ::= #isArrayOf ( TypeInfo , Ty ) [function, total]
+Pointers to arrays/slices are compatible with pointers to the element type
+```k
+  rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
+    => maybeConcatProj(
+          projectionElemConstantIndex(0, 0, false),
+          #pointeeProjection(lookupTy(TY1), TY2)
+        )
+  rule #pointeeProjection(TY1, typeInfoArrayType(TY2, _))
+    => maybeConcatProj(
+          projectionElemSingletonArray,
+          #pointeeProjection(TY1, lookupTy(TY2))
+        )
+```
 
-  rule #isArrayOf(typeInfoArrayType(TY, _), TY) => true
-  rule #isArrayOf(      _                 , _ ) => false [owise]
+Pointers to zero-sized types can be converted from and to. No recursion beyond the ZST.
+**TODO** Problem: our ZSTs have different representation: compare empty arrays and empty structs/unit tuples.
+```k
+  rule #pointeeProjection(SRC, OTHER) => projectionElemToZST   .ProjectionElems
+    requires #zeroSizedType(OTHER) andBool notBool #zeroSizedType(SRC)
+    [priority(45)]
+  rule #pointeeProjection(SRC, OTHER) => projectionElemFromZST .ProjectionElems
+    requires #zeroSizedType(SRC) andBool notBool #zeroSizedType(OTHER)
+    [priority(45)]
 ```
 
 Pointers to structs with a single zero-offset field are compatible with pointers to that field's type
 ```k
-  rule #typesCompatible(SRC, OTHER) => true
-    requires #zeroSizedType(SRC) orBool #zeroSizedType(OTHER)
 
-  rule #typesCompatible(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
-    => #typesCompatible(lookupTy(FIELD), OTHER)
+  rule #pointeeProjection(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
+    => maybeConcatProj(
+          projectionElemField(fieldIdx(0), FIELD),
+          #pointeeProjection(lookupTy(FIELD), OTHER)
+        )
     requires #zeroFieldOffset(LAYOUT)
 
-  rule #typesCompatible(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
-    => #typesCompatible(OTHER, lookupTy(FIELD))
+  rule #pointeeProjection(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
+    => maybeConcatProj(
+          projectionElemWrapStruct,
+          #pointeeProjection(OTHER, lookupTy(FIELD))
+        )
     requires #zeroFieldOffset(LAYOUT)
+```
 
-  syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]
+Pointers to `MaybeUninit<X>` can be cast to pointers to `X`.
+This is actually a 2-step compatibility:
+The `MaybeUninit<X>` union contains a `ManuallyDrop<X>` (when filled),
+which is a singleton struct (see above).
 
+```k
+  rule #pointeeProjection(MAYBEUNINIT_TYINFO, ELEM_TYINFO)
+    => maybeConcatProj(
+          projectionElemField(fieldIdx(1), {getFieldTy(MAYBEUNINIT_TYINFO, 1)}:>Ty),
+          maybeConcatProj(
+            projectionElemField(fieldIdx(0), {getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)}:>Ty),
+           .ProjectionElems // TODO recursion?
+          )
+        )
+    requires #typeNameIs(MAYBEUNINIT_TYINFO, "std::mem::MaybeUninit<")
+     andBool #lookupMaybeTy(getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO
+```
+
+```k
+  syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]
+  // --------------------------------------------------------------------
   rule #zeroFieldOffset(LAYOUT)
-    =>      #layoutOffsets(LAYOUT) ==K .MachineSizes
-     orBool #layoutOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes
+    =>      #layoutOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes
      orBool #layoutOffsets(LAYOUT) ==K machineSize(0) .MachineSizes
 
   // Extract field offsets from the struct layout when available (Arbitrary only).
   syntax MachineSizes ::= #layoutOffsets ( MaybeLayoutShape ) [function, total]
+  // --------------------------------------------------------------------------
   rule #layoutOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
   rule #layoutOffsets(noLayoutShape) => .MachineSizes
   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

kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state

@@ -35,12 +35,12 @@
       ListItem ( typedValue ( Range ( ListItem ( Integer ( 11 , 32 , true ) )
       ListItem ( Integer ( 22 , 32 , true ) )
       ListItem ( Integer ( 33 , 32 , true ) ) ) , ty ( 38 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: PointerOffset ( 1 , 3 )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 1 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 39 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 22 , 32 , true ) , ty ( 16 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 35 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: PointerOffset ( 2 , 3 )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 2 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 39 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 16 ) , mutabilityMut ) )

kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state

@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K
+    PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemToZST  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn

kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs

@@ -0,0 +1,19 @@
+struct Wrapper<T>(T);
+
+fn main() {
+    let i = 32_i32;
+
+    unsafe {
+        let p_i = &i as *const i32;
+        assert!(32 == *p_i);
+
+        let p_w = p_i as *const Wrapper<i32>;
+        assert!(32 == (*p_w).0);
+
+        let p_ww = p_w as *const Wrapper<Wrapper<i32>>;
+        assert!(32 == (*p_ww).0.0);
+
+        let p_ii = p_ww as *const i32;
+        assert!(32 == *p_ii);
+    }
+}

kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr-offset.rs

@@ -0,0 +1,11 @@
+fn main() {
+    let arr: [i32; 2] = [42, 84];
+    let r_arr = &arr;
+    let p_arr_wide = r_arr as *const [i32; 2];
+    let p_arr_narrow = p_arr_wide as *const [i32; 1];
+
+    unsafe {
+        let p_arr_narrow_offset = p_arr_narrow.offset(1);
+        assert!(*p_arr_narrow_offset == [84]);
+    }
+}

kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr.rs

@@ -0,0 +1,9 @@
+fn main() {
+    let arr: [i32; 1] = [42];
+    let r_arr = &arr;
+    let p_arr = r_arr as *const [i32; 1];
+
+    unsafe {
+        assert!(*p_arr == [42]);
+    }
+}

kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs

@@ -0,0 +1,9 @@
+fn main() {
+    let arr: [i32; 1] = [42];
+    let r_arr = &arr;
+    let p_arr = r_arr as *const i32;
+
+    unsafe {
+        assert!(*p_arr == 42);
+    }
+}

kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs

@@ -0,0 +1,11 @@
+// ptr-cast-elem-offset-fail.rs
+fn main() {
+    let arr: [i32; 2] = [42, 84];
+    let r_arr = &arr;
+    let p_arr = r_arr as *const i32;
+
+    unsafe {
+        let p_arr_offset = p_arr.offset(1);
+        assert!(*p_arr_offset == 84);
+    }
+}

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

@@ -3,9 +3,9 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (2000 steps)
+│  (2005 steps)
 └─ 3 (stuck, leaf)
-    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio
+    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( ListItem ( Aggregate
     span: 146