Adjust reference and pointer offsets within aggregate types and arrays (#636)

Fixes a bug where references and pointers contained within container
types would become invalid when passed between functions as arguments or
read through other references.

Also included: Renaming of `VoidType` to `typeInfoVoidType`

Author: jberthold

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

@@ -51,6 +51,12 @@ If nothing is removed, the list remains the same. If all elements are removed, n
   rule #Ceil(range(L, A, B)) => #Ceil(L) #And #Ceil(A) #And #Ceil(B) #And {true #Equals A +Int B <=Int size(L)} [simplification]
 ```
 
+The `#mapOffset` function maps `#adjustRef` over a lists of `Value`s, leaving the list length unchanged.
+
+```k
+  rule size(#mapOffset(L, _)) => size(L) [simplification, preserves-definedness]
+```
+
 ## Simplifications for Int
 
 These are trivial simplifications driven by syntactic equality, which should be present upstream.

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

@@ -315,16 +315,30 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
      andBool isTypedValue(LOCALS[I])
     [preserves-definedness] // valid list indexing checked
 
-  syntax Value ::= #incrementRef ( Value )  [function, total]
-                 | #decrementRef ( Value )  [function, total]
-                 | #adjustRef (Value, Int ) [function, total]
-
+  syntax Value ::= #adjustRef (Value, Int ) [function, total]
+  // --------------------------------------------------------
   rule #adjustRef(Reference(HEIGHT, PLACE, REFMUT, META), OFFSET)
     => Reference(HEIGHT +Int OFFSET, PLACE, REFMUT, META)
   rule #adjustRef(PtrLocal(HEIGHT, PLACE, REFMUT, EMULATION), OFFSET)
     => PtrLocal(HEIGHT +Int OFFSET, PLACE, REFMUT, EMULATION)
+  rule #adjustRef(Aggregate(IDX, ARGS), OFFSET)
+    => Aggregate(IDX, #mapOffset(ARGS, OFFSET))
+  rule #adjustRef(Range(ELEMS), OFFSET)
+    => Range(#mapOffset(ELEMS, OFFSET))
   rule #adjustRef(TL, _) => TL [owise]
 
+  syntax List ::= #mapOffset ( List, Int ) [function, total]
+  // -------------------------------------------------------
+  rule #mapOffset(.List, _)
+    => .List
+  rule #mapOffset(ListItem(ELEM:Value) REST, OFFSET)
+    => ListItem(#adjustRef(ELEM, OFFSET)) #mapOffset(REST, OFFSET)
+  rule #mapOffset(OTHER, _)
+    => OTHER [owise] // should not happen
+
+  syntax Value ::= #incrementRef ( Value )  [function, total]
+                 | #decrementRef ( Value )  [function, total]
+  // --------------------------------------------------------
   rule #incrementRef(TL) => #adjustRef(TL, 1)
   rule #decrementRef(TL) => #adjustRef(TL, -1)
 ```

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

@@ -265,7 +265,7 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
                     | typeInfoRefType(Ty)                                [symbol(TypeInfo::RefType)      , group(mir-enum---pointee-type)]
                     | typeInfoTupleType(Tys)                             [symbol(TypeInfo::TupleType)    , group(mir-enum---types)]
                     | typeInfoFunType(MIRString)                         [symbol(TypeInfo::FunType)      , group(mir-enum)]
-                    | "VoidType"                                         [symbol(TypeInfo::VoidType)     , group(mir-enum)]
+                    | "typeInfoVoidType"                                 [symbol(TypeInfo::VoidType)     , group(mir-enum)]
 
 
   // discriminant information for enum types

kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state

@@ -82,7 +82,7 @@
     ty ( 18 ) |-> typeInfoRefType ( ty ( 15 ) )
     ty ( 21 ) |-> typeInfoPrimitiveType ( primTypeBool )
     ty ( 24 ) |-> typeInfoRefType ( ty ( 37 ) )
-    ty ( 25 ) |-> VoidType
+    ty ( 25 ) |-> typeInfoVoidType
     ty ( 26 ) |-> typeInfoTupleType ( ty ( 2 )  ty ( 21 )  .Tys )
     ty ( 28 ) |-> typeInfoTupleType ( ty ( 9 )  ty ( 21 )  .Tys )
     ty ( 30 ) |-> typeInfoPtrType ( ty ( 12 ) )

kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic.state

@@ -97,7 +97,7 @@
     ty ( 28 ) |-> typeInfoTupleType ( ty ( 2 )  ty ( 25 )  .Tys )
     ty ( 29 ) |-> typeInfoTupleType ( ty ( 26 )  ty ( 25 )  .Tys )
     ty ( 32 ) |-> typeInfoPtrType ( ty ( 9 ) )
-    ty ( 33 ) |-> VoidType
+    ty ( 33 ) |-> typeInfoVoidType
   </types>
   <adt-to-ty>
     adtDef ( 9 ) |-> ty ( 17 )

kmir/src/tests/integration/data/exec-smir/arithmetic/unary.state

@@ -68,7 +68,7 @@
     ty ( 25 ) |-> typeInfoPrimitiveType ( primTypeBool )
     ty ( 26 ) |-> typeInfoTupleType ( ty ( 9 )  ty ( 25 )  .Tys )
     ty ( 28 ) |-> typeInfoPtrType ( ty ( 9 ) )
-    ty ( 29 ) |-> VoidType
+    ty ( 29 ) |-> typeInfoVoidType
   </types>
   <adt-to-ty>
     adtDef ( 9 ) |-> ty ( 17 )

kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state

@@ -77,7 +77,7 @@
     ty ( 28 ) |-> typeInfoRefType ( ty ( 33 ) )
     ty ( 29 ) |-> typeInfoArrayType ( ty ( 26 ) , someTyConst ( tyConst (... kind: tyConstKindValue ( ty ( 25 ) , allocation (... bytes: b"\x04\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , id: tyConstId ( 0 ) ) ) )
     ty ( 30 ) |-> typeInfoPrimitiveType ( primTypeBool )
-    ty ( 31 ) |-> VoidType
+    ty ( 31 ) |-> typeInfoVoidType
     ty ( 32 ) |-> typeInfoRefType ( ty ( 34 ) )
     ty ( 33 ) |-> typeInfoPrimitiveType ( primTypeStr )
     ty ( 34 ) |-> typeInfoStructType ( "std::panic::Location<'_>" , adtDef ( 8 ) , ty ( 28 )  ty ( 35 )  ty ( 35 )  .Tys )

kmir/src/tests/integration/data/exec-smir/arrays/array_write.state

@@ -87,7 +87,7 @@
     ty ( 29 ) |-> typeInfoArrayType ( ty ( 26 ) , someTyConst ( tyConst (... kind: tyConstKindValue ( ty ( 25 ) , allocation (... bytes: b"\x04\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , id: tyConstId ( 0 ) ) ) )
     ty ( 30 ) |-> typeInfoPrimitiveType ( primTypeBool )
     ty ( 31 ) |-> typeInfoRefType ( ty ( 26 ) )
-    ty ( 32 ) |-> VoidType
+    ty ( 32 ) |-> typeInfoVoidType
     ty ( 34 ) |-> typeInfoPtrType ( ty ( 9 ) )
     ty ( 35 ) |-> typeInfoRefType ( ty ( 37 ) )
     ty ( 36 ) |-> typeInfoPrimitiveType ( primTypeStr )

kmir/src/tests/integration/data/exec-smir/assign-cast/assign-cast.state

@@ -76,7 +76,7 @@
     ty ( 28 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU32 ) )
     ty ( 29 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU64 ) )
     ty ( 31 ) |-> typeInfoPtrType ( ty ( 9 ) )
-    ty ( 32 ) |-> VoidType
+    ty ( 32 ) |-> typeInfoVoidType
   </types>
   <adt-to-ty>
     adtDef ( 13 ) |-> ty ( 10 )

kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state

@@ -64,7 +64,7 @@
     ty ( 26 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyUsize ) )
     ty ( 28 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI16 ) )
     ty ( 30 ) |-> typeInfoPtrType ( ty ( 9 ) )
-    ty ( 31 ) |-> VoidType
+    ty ( 31 ) |-> typeInfoVoidType
   </types>
   <adt-to-ty>
     adtDef ( 14 ) |-> ty ( 10 )