527 basic support for allocated data (#680)

* Allocated constants are stored in the `<memory>` cell as a map
`AllocId -> Value` (by python code inserting a `#decodeAllocs`
function).
* The allocation decoder (currently) only handles allocations without a
provenance or with a single provenance entry at offset 0 when the
allocation type is a reference. Otherwise, undecoded data is stored in
raw form, in a supersort of `Value`.

* A new value constructor `AllocRef` is added, containing an `AllocId`
and reference metadata.
- This value can be `Deref`erenced like a `PtrLocal` or `Reference` if
the `<memory>` map has a `Value` entry for the given `AllocId` (will get
stuck on undecoded data).
* `AllocRef`s are created by `#decodeConstant` from `operandConstant`
operands with a single provenance map entry at offset 0 when a reference
type is expected (same restrictions as the allocation decoder above).
Otherwise `#decodeConstant` becomes a thunk.
* `AllocRef`s can be `Unsize`d, i.e., dynamic metadata added to replace
known static metadata.
* `AllocRef`s support trivial `Transmute` calls where source and target
type are the same

---------

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

Author: jberthold

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

@@ -30,7 +30,7 @@ syntax GlobalAllocKind ::= globalAllocFunction(Instance)
                          | Memory(Allocation)
                              [group(mir-enum), symbol(GlobalAllocKind::Memory)]
 
-syntax GlobalAlloc ::= globalAllocEntry(MIRInt, Ty, GlobalAllocKind)
+syntax GlobalAlloc ::= globalAllocEntry(AllocId, Ty, GlobalAllocKind)
          [symbol(globalAllocEntry), group(mir---alloc-id--ty--global-alloc)]
 
 syntax GlobalAllocs ::= List {GlobalAlloc, ""}

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

@@ -46,11 +46,11 @@ module KMIR-CONFIGURATION
                   </currentFrame>
                   // remaining call stack (without top frame)
                   <stack> .List </stack>
+                  // static and dynamic allocations: AllocId -> Value
                   <memory> .Map </memory>
                   // ============ static information ============
                   // function store, Ty -> MonoItemFn
                   <functions> .Map </functions>
-                  // heap
                   <start-symbol> symbol($STARTSYM:String) </start-symbol>
                   // static information about the base type interning in the MIR
                   <types> .Map </types>

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

@@ -292,6 +292,14 @@ A `Deref` projection in the projections list changes the target of the write ope
     requires 0 <Int FRAME andBool FRAME <=Int size(STACK)
      andBool isStackFrame(STACK[FRAME -Int 1])
      [preserves-definedness] // valid context ensured upon context construction
+
+  rule <k> #traverseProjection(toAlloc(ALLOC_ID), _ORIGINAL, .ProjectionElems, CONTEXTS)
+        ~> #writeMoved
+        => .K
+        ...
+       </k>
+       <memory> MEMORY => MEMORY[ALLOC_ID <- #buildUpdate(Moved, CONTEXTS)] </memory>
+    [preserves-definedness] // valid ALLOC_ID ensured when destination set
 ```
 
 These helpers mark down, as we traverse the projection, what `Place` we are currently looking up in the traversal.
@@ -301,6 +309,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
   // stores the target of the write operation, which may change when references are dereferenced.
   syntax WriteTo ::= toLocal ( Int )
                    | toStack ( Int , Local )
+                   | toAlloc ( AllocId )
 
   // retains information about the value that was deconstructed by a projection
   syntax Context ::= CtxField( VariantIdx, List, Int , Ty )
@@ -681,6 +690,32 @@ An attempt to read more elements than the length of the accessed array is undefi
     [preserves-definedness]
 ```
 
+References also exist into the `<memory>` heap which is populated with allocated constants.
+A reference to a statically allocated constant is typically never written to,
+even though this could be supported.
+
+```k
+  rule <k> #traverseProjection(
+             _DEST,
+             AllocRef(ALLOC_ID, META),
+             projectionElemDeref PROJS,
+             _CTXTS
+           )
+        => #traverseProjection(
+             toAlloc(ALLOC_ID),
+             {MEMORYMAP[ALLOC_ID]}:>Value,
+             .ProjectionElems, // no place projections
+             .Contexts // previous contexts obsolete
+           )
+          ~> #derefTruncate(META, PROJS) // then truncate, then continue with remaining projections
+        ...
+        </k>
+        <memory> MEMORYMAP </memory>
+    requires ALLOC_ID in_keys(MEMORYMAP)
+     andBool isValue(MEMORYMAP[ALLOC_ID])
+    [preserves-definedness]
+```
+
 ## Evaluation of R-Values (`Rvalue` sort)
 
 The `Rvalue` sort in MIR represents various operations that produce a value which can be assigned to a `Place`.
@@ -1206,6 +1241,12 @@ The original metadata is therefore already stored as `staticSize` to avoid havin
       //  andBool isTypeInfo(TYPEMAP[TY_SOURCE])
       // andBool notBool hasMetadata(_TY_TARGET, TYPEMAP)
       // [preserves-definedness] // valid type map indexing and sort coercion
+
+  rule <k> #cast(AllocRef(ID, staticSize(SIZE)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET)
+          =>
+            AllocRef(ID, dynamicSize(SIZE))
+          ...
+        </k>
 ```
 
 ### `Transmute` casts
@@ -1224,6 +1265,13 @@ What can be supported without additional layout consideration is trivial casts b
        andBool TYPEMAP[TY_SOURCE] ==K TYPEMAP[TY_TARGET]
       [preserves-definedness] // valid map lookups checked
 
+  rule <k> #cast(AllocRef(_, _) #as REF, castKindTransmute, TY_SOURCE, TY_TARGET) => REF ... </k>
+       <types> TYPEMAP </types>
+      requires TY_SOURCE in_keys(TYPEMAP)
+       andBool TY_TARGET in_keys(TYPEMAP)
+       andBool TYPEMAP[TY_SOURCE] ==K TYPEMAP[TY_TARGET]
+      [preserves-definedness] // valid map lookups checked
+
   rule <k> #cast(PtrLocal(_, _, _, _) #as PTR, castKindTransmute, TY_SOURCE, TY_TARGET) => PTR ... </k>
        <types> TYPEMAP </types>
       requires TY_SOURCE in_keys(TYPEMAP)
@@ -1265,8 +1313,6 @@ For allocated constants without provenance, the decoder works directly with the
 
 Zero-sized types can be decoded trivially into their respective representation.
 
-**FIXME test the new cases for tuple and array/slice**
-
 ```k
   // zero-sized struct
   rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoStructType(_, _, _))
@@ -1279,6 +1325,49 @@ Zero-sized types can be decoded trivially into their respective representation.
         => Range(.List) ... </k>
 ```
 
+Allocated constants of reference type with a single provenance map entry are decoded as references
+into the `<memory>` heap where all allocated constants have been decoded at program start.
+
+```k
+  rule <k> #decodeConstant(
+              constantKindAllocated(
+                allocation(
+                  BYTES,
+                  provenanceMap(provenanceMapEntry(0, ALLOC_ID) .ProvenanceMapEntries),
+                  _,
+                  _)),
+              _TY,
+              typeInfoRefType(POINTEE_TY)
+            )
+        => AllocRef(ALLOC_ID, #metadata(POINTEE_TY, TYPEMAP))
+        ...
+       </k>
+       <memory> ALLOCMAP </memory>
+       <types> TYPEMAP </types>
+    requires ALLOC_ID in_keys(ALLOCMAP)
+     andBool lengthBytes(BYTES) ==Int 8 // no dynamic metadata
+
+  rule <k> #decodeConstant(
+              constantKindAllocated(
+                allocation(
+                  BYTES,
+                  provenanceMap(provenanceMapEntry(0, ALLOC_ID) .ProvenanceMapEntries),
+                  _,
+                  _)),
+              _TY,
+              typeInfoRefType(_)
+            )
+        => AllocRef(ALLOC_ID, dynamicSize(Bytes2Int(substrBytes(BYTES, 8, 16), LE, Unsigned)) )
+                                          // assumes usize == u64
+        ...
+       </k>
+       <memory> ALLOCMAP </memory>
+    requires ALLOC_ID in_keys(ALLOCMAP)
+     andBool lengthBytes(BYTES) ==Int 16 // fat pointer (assumes usize == u64)
+    [preserves-definedness] // Byte length checked to be sufficient
+```
+
+
 ## Primitive operations on numeric data
 
 The `RValue:BinaryOp` performs built-in binary operations on two operands.

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

@@ -14,12 +14,14 @@ from raw bytes to typed `Value` objects according to Rust's memory layout rules.
 requires "../ty.md"
 requires "value.md"
 requires "numbers.md"
+requires "../alloc.md"
 
 module RT-DECODING
   imports BOOL
   imports MAP
 
   imports TYPES
+  imports ALLOC
   imports RT-VALUE-SYNTAX
   imports RT-NUMBERS
   imports RT-TYPES
@@ -37,6 +39,7 @@ and arrays (where layout is trivial).
 ```k
   syntax Evaluation ::= #decodeValue ( Bytes , TypeInfo , Map ) [function, total]
                       | UnableToDecode( Bytes , TypeInfo )
+                      | UnableToDecode( Bytes , Ty , ProvenanceMapEntries )
 
   // Boolean: should be one byte with value one or zero
   rule #decodeValue(BYTES, typeInfoPrimitiveType(primTypeBool), _TYPEMAP) => BoolVal(false)
@@ -168,6 +171,100 @@ by the element size, then uses the same element-by-element decoding approach as
     [preserves-definedness]
 ```
 
+# Decoding the allocated constants into a memory map
+
+When the program starts, all allocated constants are stored in the `<memory>` cell in the configuration,
+as a mapping of `AllocId -> Value`, decoding the allocations to values using the above functions.
+
+Besides actual byte allocations, we often find allocations with provenance,
+as slim or fat pointers pointing to other static allocations.
+One example of this is allocated error strings, whose length is stored in a fat pointer that is itself an allocated constant.
+
+
+The basic decoding function is very similar to `#decodeConstant` but returns its result as a singleton `Map` instead of a mere value.
+
+```k
+  syntax Map ::= #decodeAlloc ( AllocId , Ty , Allocation , Map ) [function] // returns AllocId |-> Value
+  // ----------------------------------------------------------
+  rule #decodeAlloc(ID, TY, allocation(BYTES, provenanceMap(.ProvenanceMapEntries), _ALIGN, _MUT), TYPEMAP)
+      => ID |-> #decodeValue(BYTES, {TYPEMAP[TY]}:>TypeInfo, TYPEMAP)
+    requires TY in_keys(TYPEMAP)
+     andBool isTypeInfo(TYPEMAP[TY])
+```
+
+If there are entries in the provenance map, then the decoder must create references to other allocations.
+Each entry replaces a pointer starting at a certain offset in the bytes.
+The pointee of the respective pointer is determined by type _layout_ of the type to decode.
+
+Simple cases of offset 0 and reference types can be implemented here without consideration of layout.
+The reference metadata is either determined statically by type, or filled in from the bytes for fat pointers.
+
+```k
+  // if length(BYTES) ==Int 16 decode BYTES[9..16] as dynamic size.
+  rule #decodeAlloc(
+          ID,
+          TY,
+          allocation(BYTES, provenanceMap(provenanceMapEntry(0, REF_ID) ), _ALIGN, _MUT),
+          TYPEMAP
+        )
+      => ID |-> AllocRef(REF_ID, dynamicSize(Bytes2Int(substrBytes(BYTES, 8, 16), LE, Unsigned)))
+    requires TY in_keys(TYPEMAP)
+     andBool isTypeInfo(TYPEMAP[TY])
+     andBool isTy(pointeeTy({TYPEMAP[TY]}:>TypeInfo)) // ensures this is a reference type
+     andBool lengthBytes(BYTES) ==Int 16 // sufficient data to decode dynamic size (assumes usize == u64)
+     andBool dynamicSize(1) ==K #metadata(pointeeTy({TYPEMAP[TY]}:>TypeInfo), TYPEMAP) // expect fat pointer
+    [preserves-definedness] // valid type lookup ensured
+
+  // Otherwise query type information for static size and insert it.
+  rule #decodeAlloc(
+          ID,
+          TY,
+          allocation(BYTES, provenanceMap(provenanceMapEntry(0, REF_ID) ), _ALIGN, _MUT),
+          TYPEMAP
+        )
+      => ID |-> AllocRef(REF_ID, #metadata(pointeeTy({TYPEMAP[TY]}:>TypeInfo), TYPEMAP))
+    requires TY in_keys(TYPEMAP)
+     andBool isTypeInfo(TYPEMAP[TY])
+     andBool isTy(pointeeTy({TYPEMAP[TY]}:>TypeInfo)) // ensures this is a reference type
+     andBool lengthBytes(BYTES) ==Int 8 // single slim pointer (assumes usize == u64)
+    [owise, preserves-definedness] // valid type lookup ensured
+```
+
+Allocations with more than one provenance map entry or witn non-reference types remain undecoded.
+
+```k
+  rule #decodeAlloc(ID, TY, allocation(BYTES, provenanceMap(ENTRIES), _ALIGN, _MUT), _TYPEMAP)
+      => ID |-> UnableToDecode(BYTES, TY, ENTRIES)
+    [owise]
+```
+
+The entire set of `GlobalAllocs` is decoded by iterating over the list.
+It is assumed that the given `Ty -> TypeInfo` map contains all types required.
+
+```k
+  syntax Map ::= #decodeAllocs ( GlobalAllocs , Map )       [function, total, symbol("decodeAllocs")] // AllocId |-> Thing
+               | #decodeAllocs ( Map , GlobalAllocs , Map ) [function, total] // accumulating version
+  // -----------------------------------------------------------------------------------------------
+  rule #decodeAllocs(ALLOCS, TYPEMAP) => #decodeAllocs(.Map, ALLOCS, TYPEMAP)
+
+  rule #decodeAllocs(ACCUM, .GlobalAllocs, _TYPEMAP) => ACCUM
+  rule #decodeAllocs(ACCUM, globalAllocEntry(ID, TY, Memory(ALLOC)) ALLOCS, TYPEMAP)
+      => #decodeAllocs(ACCUM #decodeAlloc(ID, TY, ALLOC, TYPEMAP), ALLOCS, TYPEMAP)
+    requires TY in_keys(TYPEMAP)
+    [preserves-definedness]
+```
+
+If the type of an alloc cannot be found, or for non-`Memory` allocs, the raw data is stored in a super-sort of `Value`.
+This ensures that the function is total (anyway lookups require constraining the sort).
+
+```k
+  syntax AllocData ::= Value | AllocData ( Ty , GlobalAllocKind )
+
+  rule #decodeAllocs(ACCUM, globalAllocEntry(ID, TY, OTHER) ALLOCS, TYPEMAP)
+      => #decodeAllocs(ACCUM ID |-> AllocData(TY, OTHER), ALLOCS, TYPEMAP)
+    [owise]
+```
+
 ```k
 endmodule
-```
+```

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

@@ -42,6 +42,8 @@ The special `Moved` value represents values that have been used and should not b
                                                           [symbol(Value::PtrLocal)]
                    // pointer to a local TypedValue (on the stack)
                    // first 3 fields are the same as in Reference, plus pointee metadata
+                 | AllocRef ( AllocId , Metadata )
+                   // reference to static allocation, by AllocId, carrying metadata if applicable
                  | "Moved"
                    // The value has been used and is gone now
 ```

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

@@ -289,7 +289,7 @@ syntax MaybePromoted ::= promoted(Int) [group(mir-option-int)]
 
 syntax Align ::= align(Int) [group(mir-int), symbol(align)]
 
-syntax ProvenanceMapEntry ::= provenanceMapEntry(provSize: MIRInt, allocId: AllocId)
+syntax ProvenanceMapEntry ::= provenanceMapEntry(offset: MIRInt, allocId: AllocId)
                               [group(mir), symbol(provenanceMapEntry)]
 
 syntax ProvenanceMapEntries ::= List {ProvenanceMapEntry, ""}

kmir/src/kmir/kmir.py

@@ -129,11 +129,23 @@ def make_call_config(
         locals, constraints = symbolic_locals(smir_info, args_info)
         types, adts = self._make_type_and_adt_maps(smir_info)
 
+        parser = Parser(self.definition)
+        allocs: KInner = KApply('GlobalAllocs::empty')
+        allocs_json = smir_info._smir['allocs']
+        assert isinstance(allocs_json, list)
+        allocs_json.reverse()
+        for alloc in allocs_json:
+            parse_result = parser.parse_mir_json(alloc, 'GlobalAlloc')
+            assert parse_result is not None
+            a, _ = parse_result
+            allocs = KApply('GlobalAllocs::append', (a, allocs))
+
         _subst = {
             'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
             'STARTSYMBOL_CELL': KApply('symbol(_)_LIB_Symbol_String', (token(start_symbol),)),
             'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
             'LOCALS_CELL': list_of(locals),
+            'MEMORY_CELL': KApply('decodeAllocs', (allocs, types)),
             'FUNCTIONS_CELL': self._make_function_map(smir_info),
             'TYPES_CELL': types,
             'ADTTOTY_CELL': adts,

kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.rs

@@ -0,0 +1,14 @@
+const I8_ARRAY: [i8; 3] = [1, -2, 3];
+const U16_ARRAY: [u16; 3] = [100, 200, 300];
+
+fn main() {
+    // the array will be allocated twice, even if the same constant is used
+    assert_eq!(I8_ARRAY, I8_ARRAY);
+    // this uses an inlined array constant instead of the global one
+    assert!(compare_to_stored(U16_ARRAY));
+    // println!("All assertions passed!");
+}
+
+fn compare_to_stored(array: [u16;3]) -> bool {
+    U16_ARRAY == array
+}