From 4fb9a32a171d4b0f7e146cfb10d57ca1cdd56172 Mon Sep 17 00:00:00 2001 From: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Date: Fri, 24 Oct 2025 18:28:43 +1000 Subject: [PATCH 1/2] Initial Ptr Offset semantics `binOpOffset` (#746) Support for `binOpOffset` - `binOpOffset` is applied to a `PtrLocal` but must come from a `Range` of some kind (e.g. `[u8; 2]`, `&[u8]`) in which case the offset is applied to a pointer to the element e.g. `*const u8`; - Both `Reference` and `PtrLocal` has the same `Metadata` that tracks and offset; - In order to ensure that pointers are not out of range when the offset is applied, `Metadata` has an `OriginSize` field for `PtrLocal` and `Reference` for the necessary bounds checking in the external `Range`; - After an offset is applied to a `PtrLocal` it can be turned back into a `Reference`, which essentially is an index into the `Range` but it does not return the element type but the `Range` type (with smaller bounds); - The bulk of the change is in `#traverseProjection` that now needs to account for an offset when a `projectionDeref` occurs; - When a non-zero offset is encountered a `ProjectionElem::PointerOffset` is appended to the place projections, later this will be turned into a `CtxPointerOffset` when the contexts are being processed; - `CtxPointerOffset` is essentially the same as a subslice as we must have a `Range` to be offsetting through Test cases for read and write are added --------- Co-authored-by: Jost Berthold --- kmir/src/kmir/decoding.py | 4 +- kmir/src/kmir/kast.py | 36 +- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 334 +++++++++++++----- .../kmir/kdist/mir-semantics/rt/decoding.md | 4 +- kmir/src/kmir/kdist/mir-semantics/rt/types.md | 26 +- kmir/src/kmir/kdist/mir-semantics/rt/value.md | 27 +- kmir/src/kmir/value.py | 19 +- .../allocs/array_const_compare.state | 8 +- .../exec-smir/allocs/array_nest_compare.state | 8 +- .../exec-smir/allocs/enum-two-refs-fail.state | 2 +- .../data/exec-smir/arrays/array_inlined.state | 8 +- .../data/exec-smir/arrays/array_write.state | 2 +- .../data/exec-smir/intrinsic/blackbox.state | 8 +- .../exec-smir/intrinsic/raw_eq_simple.state | 4 +- .../exec-smir/niche-enum/niche-enum.state | 24 +- .../pointer-cast-length-test-fail.state | 14 +- .../exec-smir/references/array_elem_ref.state | 4 +- .../data/exec-smir/references/doubleRef.state | 10 +- .../exec-smir/references/mutableRef.state | 4 +- .../data/exec-smir/references/refAsArg.state | 2 +- .../data/exec-smir/references/refAsArg2.state | 2 +- .../exec-smir/references/refReturned.state | 4 +- .../data/exec-smir/references/simple.state | 2 +- .../data/exec-smir/references/weirdRefs.state | 24 +- .../integration/data/prove-rs/offset_read.rs | 5 + .../data/prove-rs/offset_struct_field_read.rs | 9 + .../prove-rs/offset_struct_field_write.rs | 10 + .../integration/data/prove-rs/offset_write.rs | 6 + .../data/prove-rs/slice-split-at.rs | 27 ++ .../simple-types/final-1.expected | 8 +- .../simple-types/final-4.expected | 8 +- .../simple-types/final-7.expected | 8 +- .../simple-types/final-9.expected | 8 +- 33 files changed, 460 insertions(+), 209 deletions(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/offset_read.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/offset_struct_field_read.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/offset_struct_field_write.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/offset_write.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/slice-split-at.rs diff --git a/kmir/src/kmir/decoding.py b/kmir/src/kmir/decoding.py index 98e77b6ea..e5b114de6 100644 --- a/kmir/src/kmir/decoding.py +++ b/kmir/src/kmir/decoding.py @@ -43,7 +43,7 @@ from pyk.kast import KInner from .ty import FieldsShape, IntegerLength, LayoutShape, MachineSize, Scalar, TagEncoding, Ty, TypeMetadata, UintTy - from .value import Metadata + from .value import MetadataSize @dataclass @@ -145,7 +145,7 @@ def _pointee_ty(type_info: TypeMetadata) -> Ty | None: return None -def _metadata(type_info: TypeMetadata) -> Metadata: +def _metadata(type_info: TypeMetadata) -> MetadataSize: match type_info: case ArrayT(length=None): return DynamicSize(1) # 1 is a placeholder, the actual size is inferred from the slice data diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 7a31b8845..95adbbedb 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -23,7 +23,7 @@ from .smir import SMIRInfo from .ty import TypeMetadata - from .value import Metadata, Value + from .value import MetadataSize, Value _LOGGER: Final = logging.getLogger(__name__) @@ -312,6 +312,14 @@ def _fresh_var(self, prefix: str) -> KVariable: def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInner], KInner | None]: # returns: symbolic value of given type, related constraints, related pointer metadata + + no_metadata = KApply( + 'Metadata', + KApply('noMetadataSize', ()), + token(0), + KApply('noMetadataSize', ()), + ) + match self.types.get(ty): case IntT(info): val, constraints = int_var(self._fresh_var('ARG_INT'), info.value, True) @@ -359,7 +367,14 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne return ( KApply('Value::Range', (elems,)), [mlEqualsTrue(eqInt(KApply('sizeList', (elems,)), l))], - KApply('dynamicSize', (l,)), + KApply( + 'Metadata', + ( + KApply('dynamicSize', (l,)), + token(0), + KApply('dynamicSize', (l,)), + ), + ), ) case ArrayT(element_type, size) if size is not None: @@ -372,7 +387,14 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne return ( KApply('Value::Range', (list_of(elem_vars),)), elem_constraints, - KApply('staticSize', (token(size),)), + KApply( + 'Metadata', + ( + KApply('staticSize', (token(size),)), + token(0), + KApply('staticSize', (token(size),)), + ), + ), ) case TupleT(components): @@ -397,10 +419,10 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne KApply( 'Value::Reference', ( - token(0), + token(0), # Stack OFFSET field KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))), KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()), - metadata if metadata is not None else KApply('noMetadata', ()), + metadata if metadata is not None else no_metadata, ), ), pointee_constraints, @@ -418,7 +440,7 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne token(0), KApply('place', (KApply('local', (token(ref),)), KApply('ProjectionElems::empty', ()))), KApply('Mutability::Mut', ()) if mutable else KApply('Mutability::Not', ()), - KApply('PtrEmulation', (metadata if metadata is not None else KApply('noMetadata', ()),)), + metadata if metadata is not None else no_metadata, ), ), pointee_constraints, @@ -479,7 +501,7 @@ class SimpleRes(NamedTuple): class ArrayRes(NamedTuple): value: TypedValue - metadata: Metadata + metadata: MetadataSize class PointerRes(NamedTuple): diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 27a5857aa..5656f4a63 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -306,6 +306,9 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr syntax Context ::= CtxField( VariantIdx, List, Int , 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) + + syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us syntax Contexts ::= List{Context, ""} @@ -328,6 +331,12 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr requires size(INNER) ==Int END -Int START // ensures updateList is defined [preserves-definedness] // START,END indexes checked before, length check for update here + // Update PointerOffset + rule #buildUpdate(Range(INNER), CtxPointerOffset(ELEMS, START, END) CTXS) + => #buildUpdate( Range(updateList(ELEMS, START, INNER)), CTXS) + requires size(INNER) ==Int END -Int START // ensures updateList is defined + [preserves-definedness] // START,END indexes checked before, length check for update here + syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function] rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL) @@ -353,8 +362,8 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr // -------------------------------------------------------- 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(PtrLocal(HEIGHT, PLACE, REFMUT, META), OFFSET) + => PtrLocal(HEIGHT +Int OFFSET, PLACE, REFMUT, META) rule #adjustRef(Aggregate(IDX, ARGS), OFFSET) => Aggregate(IDX, #mapOffset(ARGS, OFFSET)) rule #adjustRef(Range(ELEMS), OFFSET) @@ -375,6 +384,12 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr // -------------------------------------------------------- rule #incrementRef(TL) => #adjustRef(TL, 1) rule #decrementRef(TL) => #adjustRef(TL, -1) + + syntax Int ::= originSize ( MetadataSize ) [function, total] + // --------------------------------------------------------------------- + rule originSize(noMetadataSize) => 0 // TODO: Is this fair, noMetadataSize does not really mean zero + rule originSize(staticSize(SIZE)) => SIZE + rule originSize(dynamicSize(SIZE)) => SIZE ``` #### Aggregates @@ -404,7 +419,7 @@ This is done without consideration of the validity of the Downcast[^downcast]. requires 0 <=Int I andBool I #traverseProjection( DEST, @@ -562,6 +577,23 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t andBool 0 <=Int END andBool END #traverseProjection( + DEST, + Range(ELEMENTS), + PointerOffset(OFFSET, _ORIGIN_LENGTH) PROJS, // TODO: seems strange to not use the ORIGIN_LENGTH... + CTXTS + ) + => #traverseProjection( + DEST, + Range(range(ELEMENTS, OFFSET, 0)), + PROJS, + CtxPointerOffset(ELEMENTS, OFFSET, size(ELEMENTS)) CTXTS + ) + ... + + requires 0 <=Int OFFSET andBool OFFSET <=Int size(ELEMENTS) + [preserves-definedness] // Offset checked to be in range for ELEMENTS ``` #### References @@ -579,10 +611,10 @@ An attempt to read more elements than the length of the accessed array is undefi ```k // helper rewrite to implement truncating slices to required size - syntax KItem ::= #derefTruncate ( Metadata , ProjectionElems ) + syntax KItem ::= #derefTruncate ( MetadataSize , ProjectionElems ) // ---------------------------------------------------------------------------------------- // no metadata, no change to the value - rule #traverseProjection( DEST, VAL, .ProjectionElems, CTXTS) ~> #derefTruncate(noMetadata, PROJS) + rule #traverseProjection( DEST, VAL, .ProjectionElems, CTXTS) ~> #derefTruncate(noMetadataSize, PROJS) => #traverseProjection(DEST, VAL, PROJS, CTXTS) ... @@ -599,85 +631,184 @@ An attempt to read more elements than the length of the accessed array is undefi requires 0 <=Int SIZE andBool SIZE <=Int size(ELEMS) [preserves-definedness] // range parameters checked + // Ref, 0 < OFFSET, 0 < PTR_OFFSET, ToStack rule #traverseProjection( _DEST, - Reference(OFFSET, place(LOCAL, PLACEPROJ), _MUT, META), + Reference(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, _CTXTS ) => #traverseProjection( toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), - PLACEPROJ, // apply reference projections - .Contexts // previous contexts obsolete + appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset + .Contexts ) - ~> #derefTruncate(META, PROJS) // then truncate, then continue with remaining projections + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... STACK requires 0 #traverseProjection( _DEST, - Reference(OFFSET, place(local(I), PLACEPROJ), _MUT, META), + Reference(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), + projectionElemDeref PROJS, + _CTXTS + ) + => #traverseProjection( + toStack(OFFSET, LOCAL), + #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), + PLACEPROJ, // apply reference projections with pointer offset + .Contexts + ) + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections + ... + + STACK + requires 0 #traverseProjection( + _DEST, + Reference(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, _CTXTS ) => #traverseProjection( toLocal(I), getValue(LOCALS, I), - PLACEPROJ, // apply reference projections - .Contexts // previous contexts obsolete + appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset + .Contexts ) - ~> #derefTruncate(META, PROJS) // then truncate, then continue with remaining projections + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... LOCALS requires OFFSET ==Int 0 andBool 0 <=Int I andBool I #traverseProjection( _DEST, - PtrLocal(OFFSET, place(LOCAL, PLACEPROJ), _MUT, ptrEmulation(META)), + Reference(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), + projectionElemDeref PROJS, + _CTXTS + ) + => #traverseProjection( + toLocal(I), + getValue(LOCALS, I), + PLACEPROJ, + .Contexts + ) + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections + ... + + LOCALS + requires OFFSET ==Int 0 + andBool 0 <=Int I andBool I #traverseProjection( + _DEST, + PtrLocal(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, _CTXTS ) => #traverseProjection( toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), - PLACEPROJ, // apply reference projections + appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset .Contexts // previous contexts obsolete ) - ~> #derefTruncate(META, PROJS) // then truncate, then continue with remaining projections + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... STACK requires 0 #traverseProjection( + _DEST, + PtrLocal(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), + projectionElemDeref PROJS, + _CTXTS + ) + => #traverseProjection( + toStack(OFFSET, LOCAL), + #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), + PLACEPROJ, // apply reference projections + .Contexts // add pointer offset context + ) + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections + ... + + STACK + requires 0 #traverseProjection( _DEST, - PtrLocal(OFFSET, place(local(I), PLACEPROJ), _MUT, ptrEmulation(META)), + PtrLocal(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, _CTXTS ) => #traverseProjection( toLocal(I), getValue(LOCALS, I), - PLACEPROJ, // apply reference projections + appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset .Contexts // previous contexts obsolete ) - ~> #derefTruncate(META, PROJS) // then truncate, then continue with remaining projections + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections + ... + + LOCALS + requires OFFSET ==Int 0 + andBool 0 <=Int I andBool I #traverseProjection( + _DEST, + PtrLocal(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), + projectionElemDeref PROJS, + _CTXTS + ) + => #traverseProjection( + toLocal(I), + getValue(LOCALS, I), + PLACEPROJ, // apply reference projections + .Contexts // add pointer offset context + ) + ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... LOCALS requires OFFSET ==Int 0 andBool 0 <=Int I andBool I #traverseProjection( _DEST, - AllocRef(ALLOC_ID, ALLOC_PROJS, META), + AllocRef(ALLOC_ID, ALLOC_PROJS, metadata(METADATA_SIZE, _PTR_OFFSET, _)), // FIXME can this be offset? projectionElemDeref PROJS, _CTXTS ) @@ -698,7 +829,7 @@ even though this could be supported. ALLOC_PROJS, // alloc projections .Contexts // previous contexts obsolete ) - ~> #derefTruncate(META, PROJS) // then truncate, then continue with remaining projections + ~> #derefTruncate(METADATA_SIZE, PROJS) // then truncate, then continue with remaining projections ... requires isValue(lookupAlloc(ALLOC_ID)) @@ -855,13 +986,13 @@ for _fat_ pointers it is a `usize` value indicating the data length. [^rawPtrAgg]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.AggregateKind.html#variant.RawPtr ```k - rule ListItem(PtrLocal(OFFSET, PLACE, _, _)) ListItem(Integer(LENGTH, 64, false)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT)) - => PtrLocal(OFFSET, PLACE, MUT, ptrEmulation(dynamicSize(LENGTH))) + rule ListItem(PtrLocal(OFFSET, PLACE, _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) ListItem(Integer(LENGTH, 64, false)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT)) + => PtrLocal(OFFSET, PLACE, MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE)) ... - rule ListItem(PtrLocal(OFFSET, PLACE, _, _)) ListItem(Aggregate(_, .List)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT)) - => PtrLocal(OFFSET, PLACE, MUT, ptrEmulation(noMetadata)) + rule ListItem(PtrLocal(OFFSET, PLACE, _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) ListItem(Aggregate(_, .List)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT)) + => PtrLocal(OFFSET, PLACE, MUT, metadata(noMetadataSize, PTR_OFFSET, ORIGIN_SIZE)) ... ``` @@ -932,35 +1063,42 @@ This eliminates any `Deref` projections from the place, and also resolves `Index rule #projectionsFor(CtxField(_, _, I, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(fieldIdx(I), TY) PROJS) rule #projectionsFor( CtxIndex(_, I) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemConstantIndex(I, 0, false) PROJS) 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 rvalueRef(_REGION, KIND, place(local(I), PROJS)) => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts) - ~> #forRef(#mutabilityOf(KIND), #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)) + ~> #forRef(#mutabilityOf(KIND), metadata(#metadataSize(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO: Sus on this rule ... LOCALS requires 0 <=Int I andBool I #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forRef(MUT, META) - => #mkRef(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL)) + rule #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forRef(MUT, metadata(SIZE, OFFSET, ORIGIN_SIZE)) + => #mkRef(DEST, #projectionsFor(CTXTS), MUT, metadata(#maybeDynamicSize(SIZE, VAL), OFFSET, ORIGIN_SIZE) ) ... syntax Evaluation ::= #mkRef( WriteTo , ProjectionElems , Mutability , Metadata ) // [function, total] // ----------------------------------------------------------------------------------------------- + // Create Reference for local variable (stack depth 0, no offset) rule #mkRef( toLocal(I) , PROJS, MUT, META) => Reference( 0 , place(local(I), PROJS), MUT, META) ... + + // Create Reference for stack frame variable (stack depth OFFSET, with pointer offset) rule #mkRef(toStack(OFFSET, LOCAL), PROJS, MUT, META) => Reference(OFFSET, place( LOCAL , PROJS), MUT, META) ... + + // Create AllocRef for heap allocation (assumed zero offset, no offset concept for heap) rule #mkRef(toAlloc(ALLOC_ID) , PROJS, _ , META) => AllocRef(ALLOC_ID, PROJS, META) ... - syntax Metadata ::= #maybeDynamicSize ( Metadata , Value ) [function, total] - // ------------------------------------------------------------------------- + syntax MetadataSize ::= #maybeDynamicSize ( MetadataSize , Value ) [function, total] + // --------------------------------------------------------------------------------- rule #maybeDynamicSize(dynamicSize(_), Range(LIST)) => dynamicSize(size(LIST)) - rule #maybeDynamicSize(dynamicSize(_), _OTHER ) => noMetadata [priority(100)] + rule #maybeDynamicSize(dynamicSize(_), _OTHER ) => noMetadataSize [priority(100)] rule #maybeDynamicSize( OTHER_META , _ ) => OTHER_META [owise] syntax Mutability ::= #mutabilityOf ( BorrowKind ) [function, total] @@ -989,25 +1127,25 @@ The operation typically creates a pointer with empty metadata. rule rvalueAddressOf(MUT, place(local(I), PROJS)) => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts) - ~> #forPtr(MUT, #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)) + ~> #forPtr(MUT, metadata(#metadataSize(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO These initial values might get overwrote // we should use #alignOf to emulate the address ... LOCALS requires 0 <=Int I andBool I #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forPtr(MUT, META) - => #mkPtr(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL)) + rule #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forPtr(MUT, metadata(SIZE, OFFSET, ORIGIN_SIZE)) + => #mkPtr(DEST, #projectionsFor(CTXTS), MUT, metadata(#maybeDynamicSize(SIZE, VAL), OFFSET, ORIGIN_SIZE)) ... syntax Evaluation ::= #mkPtr ( WriteTo, ProjectionElems, Mutability , Metadata ) // [function, total] // ------------------------------------------------------------------------------------------ - rule #mkPtr( toLocal(I) , PROJS, MUT, META) => PtrLocal( 0 , place(local(I), PROJS), MUT, ptrEmulation(META)) ... - rule #mkPtr(toStack(OFFSET, LOCAL), PROJS, MUT, META) => PtrLocal(OFFSET, place( LOCAL , PROJS), MUT, ptrEmulation(META)) ... + rule #mkPtr( toLocal(I) , PROJS, MUT, META) => PtrLocal( 0 , place(local(I), PROJS), MUT, META) ... + rule #mkPtr(toStack(STACK_OFFSET, LOCAL), PROJS, MUT, META) => PtrLocal(STACK_OFFSET, place( LOCAL , PROJS), MUT, META) ... ``` In practice, the `AddressOf` can often be found applied to references that get dereferenced first, @@ -1035,7 +1173,7 @@ a special rule for this case is applied with higher priority. syntax Value ::= refToPtrLocal ( Value , Mutability ) [function] - rule refToPtrLocal(Reference(OFFSET, PLACE, _, META), MUT) => PtrLocal(OFFSET, PLACE, MUT, ptrEmulation(META)) + rule refToPtrLocal(Reference(STACK_OFFSET, PLACE, _, META), MUT) => PtrLocal(STACK_OFFSET, PLACE, MUT, META) ``` ## Type casts @@ -1111,24 +1249,24 @@ Conversion is especially possible for the case of _Slices_ (of dynamic length) a which have the same representation `Value::Range`. ```k - rule #cast(PtrLocal(OFFSET, PLACE, MUT, EMUL), castKindPtrToPtr, TY_SOURCE, TY_TARGET) + rule #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET) => - PtrLocal(OFFSET, PLACE, MUT, #convertPtrEmul(EMUL, lookupTy(TY_TARGET))) + PtrLocal(OFFSET, PLACE, MUT, #convertMetadata(META, lookupTy(TY_TARGET))) ... requires #typesCompatible(lookupTy(TY_SOURCE), lookupTy(TY_TARGET)) [preserves-definedness] // valid map lookups checked - syntax PtrEmulation ::= #convertPtrEmul ( PtrEmulation , TypeInfo ) [function, total] - // ---------------------------------------------------------------------------------- + syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total] + // ------------------------------------------------------------------------------------- ``` Pointers to slices can be converted to pointers to single elements, _losing_ their metadata. ```k - rule #convertPtrEmul( ptrEmulation(_) , typeInfoRefType(POINTEE_TY)) => ptrEmulation(noMetadata) - requires #metadata(POINTEE_TY) ==K noMetadata [priority(60)] - rule #convertPtrEmul( ptrEmulation(_) , typeInfoPtrType(POINTEE_TY)) => ptrEmulation(noMetadata) - requires #metadata(POINTEE_TY) ==K noMetadata [priority(60)] + rule #convertMetadata( metadata(SIZE, OFFSET, _) , typeInfoRefType(POINTEE_TY) ) => metadata(noMetadataSize, OFFSET, SIZE) + requires #metadataSize(POINTEE_TY) ==K noMetadataSize [priority(60)] + rule #convertMetadata( metadata(SIZE, OFFSET, _) , typeInfoPtrType(POINTEE_TY) ) => metadata(noMetadataSize, OFFSET, SIZE) + requires #metadataSize(POINTEE_TY) ==K noMetadataSize [priority(60)] ``` Conversely, when casting a pointer to an element to a pointer to a slice or array, @@ -1138,17 +1276,17 @@ the original allocation size must be checked to be sufficient. ```k // no metadata to begin with, fill it in from target type (NB dynamicSize(1) if dynamic) - rule #convertPtrEmul( ptrEmulation(noMetadata) , typeInfoRefType(POINTEE_TY)) => ptrEmulation(#metadata(POINTEE_TY)) - rule #convertPtrEmul( ptrEmulation(noMetadata) , typeInfoPtrType(POINTEE_TY)) => ptrEmulation(#metadata(POINTEE_TY)) + rule #convertMetadata( metadata(noMetadataSize, OFFSET, _) , typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, noMetadataSize) + rule #convertMetadata( metadata(noMetadataSize, OFFSET, _) , typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, noMetadataSize) ``` Conversion from an array to a slice pointer requires adding metadata (`dynamicSize`) with the previously-static length. ```k // convert static length to dynamic length - rule #convertPtrEmul(ptrEmulation(staticSize(SIZE)), typeInfoRefType(POINTEE_TY)) => ptrEmulation(dynamicSize(SIZE)) - requires #metadata(POINTEE_TY) ==K dynamicSize(1) - rule #convertPtrEmul(ptrEmulation(staticSize(SIZE)), typeInfoPtrType(POINTEE_TY)) => ptrEmulation(dynamicSize(SIZE)) - requires #metadata(POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(metadata(staticSize(SIZE), OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, staticSize(SIZE)) + requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(metadata(staticSize(SIZE), OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, staticSize(SIZE)) + requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) ``` Conversion from a slice to an array pointer, or between different static length array pointers, is allowed in all cases. @@ -1157,29 +1295,29 @@ It may however be illegal to _dereference_ (i.e., access) the created pointer, d **TODO** we can mark cases of insufficient original length as "InvalidCast" in the future, similar to the above future work. ```k - rule #convertPtrEmul(ptrEmulation(staticSize(_)), typeInfoRefType(POINTEE_TY)) => ptrEmulation(#metadata(POINTEE_TY)) - requires #metadata(POINTEE_TY) =/=K dynamicSize(1) - rule #convertPtrEmul(ptrEmulation(staticSize(_)), typeInfoPtrType(POINTEE_TY)) => ptrEmulation(#metadata(POINTEE_TY)) - requires #metadata(POINTEE_TY) =/=K dynamicSize(1) - - rule #convertPtrEmul(ptrEmulation(dynamicSize(_)), typeInfoRefType(POINTEE_TY)) => ptrEmulation(#metadata(POINTEE_TY)) - requires #metadata(POINTEE_TY) =/=K dynamicSize(1) - rule #convertPtrEmul(ptrEmulation(dynamicSize(_)), typeInfoPtrType(POINTEE_TY)) => ptrEmulation(#metadata(POINTEE_TY)) - requires #metadata(POINTEE_TY) =/=K dynamicSize(1) + rule #convertMetadata(metadata(staticSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) + rule #convertMetadata(metadata(staticSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) + + rule #convertMetadata(metadata(dynamicSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) + rule #convertMetadata(metadata(dynamicSize(_) #as ORIGIN_SIZE, OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(#metadataSize(POINTEE_TY), OFFSET, ORIGIN_SIZE) + requires #metadataSize(POINTEE_TY) =/=K dynamicSize(1) ``` For a cast bwetween two pointer types with `dynamicSize` metadata (unlikely to occur), the dynamic size value is retained. ```k - rule #convertPtrEmul(ptrEmulation(dynamicSize(SIZE)), typeInfoRefType(POINTEE_TY)) => ptrEmulation(dynamicSize(SIZE)) - requires #metadata(POINTEE_TY) ==K dynamicSize(1) - rule #convertPtrEmul(ptrEmulation(dynamicSize(SIZE)), typeInfoPtrType(POINTEE_TY)) => ptrEmulation(dynamicSize(SIZE)) - requires #metadata(POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(metadata(dynamicSize(SIZE), OFFSET, _), typeInfoRefType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, dynamicSize(SIZE)) + requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) + rule #convertMetadata(metadata(dynamicSize(SIZE), OFFSET, _), typeInfoPtrType(POINTEE_TY)) => metadata(dynamicSize(SIZE), OFFSET, dynamicSize(SIZE)) + requires #metadataSize(POINTEE_TY) ==K dynamicSize(1) ``` ```k // non-pointer and non-ref target type (should not happen!) - rule #convertPtrEmul( _ , _OTHER_INFO ) => ptrEmulation(noMetadata) [priority(100)] + rule #convertMetadata( metadata(SIZE, OFFSET, _) , _OTHER_INFO ) => metadata(noMetadataSize, OFFSET, SIZE) [priority(100)] ``` `PointerCoercion` may achieve a simmilar effect, or deal with function and closure pointers, depending on the coercion type: @@ -1200,9 +1338,9 @@ Specifically, pointers to arrays of statically-known length are cast to pointers The original metadata is therefore already stored as `staticSize` to avoid having to look it up here. ```k - rule #cast(Reference(OFFSET, PLACE, MUT, staticSize(SIZE)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET) + rule #cast(Reference(OFFSET, PLACE, MUT, metadata(staticSize(SIZE), PTR_OFFSET, ORIGIN_SIZE)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET) => - Reference(OFFSET, PLACE, MUT, dynamicSize(SIZE)) + Reference(OFFSET, PLACE, MUT, metadata(dynamicSize(SIZE), PTR_OFFSET, ORIGIN_SIZE)) ... // TYPEMAP @@ -1212,9 +1350,9 @@ The original metadata is therefore already stored as `staticSize` to avoid havin // andBool notBool hasMetadata(_TY_TARGET, TYPEMAP) // [preserves-definedness] // valid type map indexing and sort coercion - rule #cast(AllocRef(ID, PROJS, staticSize(SIZE)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET) + rule #cast(AllocRef(ID, PROJS, metadata(staticSize(SIZE), OFF, ORIG)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET) => - AllocRef(ID, PROJS, dynamicSize(SIZE)) + AllocRef(ID, PROJS, metadata(dynamicSize(SIZE), OFF, ORIG)) ... ``` @@ -1296,7 +1434,7 @@ into the `` heap where all allocated constants have been decoded at prog _TY, typeInfoRefType(POINTEE_TY) ) - => AllocRef(ALLOC_ID, .ProjectionElems, #metadata(POINTEE_TY)) + => AllocRef(ALLOC_ID, .ProjectionElems, metadata(#metadataSize(POINTEE_TY), 0, #metadataSize(POINTEE_TY))) ... requires isValue(lookupAlloc(ALLOC_ID)) @@ -1312,7 +1450,7 @@ into the `` heap where all allocated constants have been decoded at prog _TY, typeInfoRefType(_) ) - => AllocRef(ALLOC_ID, .ProjectionElems, dynamicSize(Bytes2Int(substrBytes(BYTES, 8, 16), LE, Unsigned)) ) + => AllocRef(ALLOC_ID, .ProjectionElems, metadata(dynamicSize(Bytes2Int(substrBytes(BYTES, 8, 16), LE, Unsigned)), 0, dynamicSize(Bytes2Int(substrBytes(BYTES, 8, 16), LE, Unsigned)) )) // assumes usize == u64 ... @@ -1707,8 +1845,9 @@ The unary operation `unOpPtrMetadata`, when given a reference or pointer to a sl * For values with statically-known size, this operation returns a _unit_ value. However, these calls should not occur in practical programs. ```k - rule #applyUnOp(unOpPtrMetadata, Reference(_, _, _, dynamicSize(SIZE))) => Integer(SIZE, 64, false) ... - rule #applyUnOp(unOpPtrMetadata, PtrLocal(_, _, _, ptrEmulation(dynamicSize(SIZE)))) => Integer(SIZE, 64, false) ... + rule #applyUnOp(unOpPtrMetadata, Reference(_, _, _, metadata(dynamicSize(SIZE), _, _))) => Integer(SIZE, 64, false) ... + rule #applyUnOp(unOpPtrMetadata, PtrLocal(_, _, _, metadata(dynamicSize(SIZE), _, _))) => Integer(SIZE, 64, false) ... + rule #applyUnOp(unOpPtrMetadata, AllocRef( _ , _, metadata(dynamicSize(SIZE), _, _))) => Integer(SIZE, 64, false) ... // could add a rule for cases without metadata ``` @@ -1749,16 +1888,45 @@ Raw pointer comparisons ignore mutability, but require the address and metadata #### Pointer Artithmetic -Currently only supporting a trivial case where `binOpOffset` applies an offset of `0`, returning the same pointer. +Addding an offset is currently restricted to unsigned values of an length, this may be too restrictive TODO Check. +A pointer is offset by adding the magnitude of the `Integer` provided, as along as it is within the bounds of the pointer. +It is valid to offset to the end of the pointer, however I believe it in not valid to read from there TODO: Check. +A trivial case where `binOpOffset` applies an offset of `0` is added with higher priority as it is returning the same pointer. ```k - rule #applyBinOp( - binOpOffset, - PtrLocal( STACK_DEPTH , PLACE , MUT, POINTEE_METADATA ), - Integer(0, _WIDTH, _SIGNED), // Trivial case when adding 0 - _CHECKED) - => - PtrLocal( STACK_DEPTH , PLACE , MUT, POINTEE_METADATA ) + // Trivial case when adding 0 - valid for any pointer + rule #applyBinOp( + binOpOffset, + PtrLocal( STACK_DEPTH , PLACE , MUT, POINTEE_METADATA ), + Integer(VAL, _WIDTH, _SIGNED), // Trivial case when adding 0 + _CHECKED) + => + PtrLocal( STACK_DEPTH , PLACE , MUT, POINTEE_METADATA ) + requires VAL ==Int 0 + [preserves-definedness, priority(40)] + + // Check offset bounds against origin pointer with dynamicSize metadata + rule #applyBinOp( + binOpOffset, + PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET, dynamicSize(ORIGIN_SIZE)) ), + Integer(OFFSET_VAL, _WIDTH, false), // unsigned offset + _CHECKED) + => + PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET +Int OFFSET_VAL, dynamicSize(ORIGIN_SIZE)) ) + requires OFFSET_VAL >=Int 0 + andBool CURRENT_OFFSET +Int OFFSET_VAL <=Int ORIGIN_SIZE + [preserves-definedness] + + // Check offset bounds against origin pointer with staticSize metadata + rule #applyBinOp( + binOpOffset, + PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET, staticSize(ORIGIN_SIZE)) ), + Integer(OFFSET_VAL, _WIDTH, false), // unsigned offset + _CHECKED) + => + PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET +Int OFFSET_VAL, staticSize(ORIGIN_SIZE)) ) + requires OFFSET_VAL >=Int 0 + andBool CURRENT_OFFSET +Int OFFSET_VAL <=Int ORIGIN_SIZE [preserves-definedness] ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md index a37b2c72c..ffef14c2b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -99,11 +99,11 @@ Known element sizes for common types: // thin and fat pointers rule #elemSize(typeInfoRefType(TY)) => #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) - requires dynamicSize(1) ==K #metadata(TY) + requires dynamicSize(1) ==K #metadataSize(TY) rule #elemSize(typeInfoRefType(_)) => 2 *Int #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) [owise] rule #elemSize(typeInfoPtrType(TY)) => #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) - requires dynamicSize(1) ==K #metadata(TY) + requires dynamicSize(1) ==K #metadataSize(TY) rule #elemSize(typeInfoPtrType(_)) => 2 *Int #elemSize(typeInfoPrimitiveType(primTypeUint(uintTyUsize))) [owise] diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index 0a7dd449f..b46ce90ff 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -104,7 +104,7 @@ To make this function total, an optional `MaybeTy` is used. ## Static and Dynamic Metadata for Types References to data on the heap or stack may require metadata, most commonly the size of slices, which is not statically known. -The helper function `#metadata` determines whether or not a given `TypeInfo` requires size information or other metadata (also see `Metadata` sort in `value.md`). +The helper function `#metadataSize` determines whether or not a given `TypeInfo` requires size information or other metadata (also see `MetadataSize` sort in `value.md`). To avoid repeated lookups, static array sizes are also stored as metadata (for `Unsize` casts). NB that the need for metadata is determined for the _pointee_ type, not the pointer type. @@ -113,18 +113,18 @@ A [similar function exists in `rustc`](https://doc.rust-lang.org/nightly/nightly Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does not. ```k - syntax Metadata ::= #metadata ( Ty , ProjectionElems ) [function, total] - | #metadata ( MaybeTy ) [function, total] - | #metadataAux ( TypeInfo ) [function, total] - // ------------------------------------------------------------ - rule #metadata(TY, PROJS) => #metadata(getTyOf(TY, PROJS)) - - rule #metadata(TyUnknown) => noMetadata - rule #metadata(TY) => #metadataAux(lookupTy(TY)) - - rule #metadataAux(typeInfoArrayType(_, noTyConst )) => dynamicSize(1) - rule #metadataAux(typeInfoArrayType(_, someTyConst(tyConst(CONST, _)))) => staticSize(readTyConstInt(CONST)) - rule #metadataAux( _OTHER ) => noMetadata [owise] + syntax MetadataSize ::= #metadataSize ( Ty , ProjectionElems ) [function, total] + | #metadataSize ( MaybeTy ) [function, total] + | #metadataSizeAux ( TypeInfo ) [function, total] + // -------------------------------------------------------------------------------------- + rule #metadataSize(TY, PROJS) => #metadataSize(getTyOf(TY, PROJS)) + + rule #metadataSize(TyUnknown) => noMetadataSize + rule #metadataSize(TY) => #metadataSizeAux(lookupTy(TY)) + + rule #metadataSizeAux(typeInfoArrayType(_, noTyConst )) => dynamicSize(1) + rule #metadataSizeAux(typeInfoArrayType(_, someTyConst(tyConst(CONST, _)))) => staticSize(readTyConstInt(CONST)) + rule #metadataSizeAux( _OTHER ) => noMetadataSize [owise] ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index 22c4e4220..f45ca88b7 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -41,13 +41,13 @@ The special `Moved` value represents values that have been used and should not b // value, bit-width for f16-f128 | Reference( Int , Place , Mutability , Metadata ) [symbol(Value::Reference)] - // stack depth (initially 0), place, borrow kind, dynamic size if applicable + // stack depth (initially 0), place, borrow kind, metadata (size, pointer offset, origin size) | Range( List ) [symbol(Value::Range)] // homogenous values for array/slice - | PtrLocal( Int , Place , Mutability, PtrEmulation ) + | PtrLocal( Int , Place , Mutability, Metadata ) [symbol(Value::PtrLocal)] // pointer to a local TypedValue (on the stack) - // first 3 fields are the same as in Reference, plus pointee metadata + // fields are the same as in Reference | AllocRef ( AllocId , ProjectionElems , Metadata ) [symbol(Value::AllocRef)] // reference to static allocation, by AllocId, possibly projected, carrying metadata if applicable @@ -65,21 +65,18 @@ A _thin pointer_ in Rust is simply an address of data in the heap or on the stac A _fat pointer_ in Rust is a pair of an address and [additional metadata about the pointee](https://doc.rust-lang.org/std/ptr/trait.Pointee.html#associatedtype.Metadata). This is necessary for dynamically-sized pointee types (most prominently slices) and dynamic trait objects. -References to arrays and slices carry `Metadata`. -For array types with statically-known size, the metadata is set to `staticSize` to avoid repeated type lookups. -Other types without metadata use `noMetadata`. +References to arrays and slices carry `Metadata`. In Rust `Metadata` is only a size, but we need more information to detect UB, so we track `(Size, Ptr Offset, Origin Size)` +For array types with statically-known size, the metadata size is set to `staticSize` to avoid repeated type lookups. +Other types without metadata use `noMetadataSize`. ```k - syntax Metadata ::= "noMetadata" [symbol(noMetadata)] - | staticSize ( Int ) [symbol(staticSize)] - | dynamicSize ( Int ) [symbol(dynamicSize)] -``` - -A pointer in Rust carries the same metadata. + // Origin size is since a pointer might not have size iteself but should be in bounds of an aggregate origin + syntax Metadata ::= metadata ( MetadataSize, Int, MetadataSize) [symbol(Metadata)] + // ( Size, Pointer Offset, Origin Size ) - -```k - syntax PtrEmulation ::= ptrEmulation ( Metadata ) [symbol(PtrEmulation)] + syntax MetadataSize ::= "noMetadataSize" [symbol(noMetadataSize)] + | staticSize ( Int ) [symbol(staticSize)] + | dynamicSize ( Int ) [symbol(dynamicSize)] ``` ## Local variables diff --git a/kmir/src/kmir/value.py b/kmir/src/kmir/value.py index ee3275de9..af16795cd 100644 --- a/kmir/src/kmir/value.py +++ b/kmir/src/kmir/value.py @@ -90,24 +90,31 @@ def to_kast(self) -> KInner: class AllocRefValue(Value): alloc_id: AllocId # projection_elems: tuple[ProjectionElem, ...] - metadata: Metadata + metadata: MetadataSize def to_kast(self) -> KInner: return KApply( 'Value::AllocRef', KApply('allocId', intToken(self.alloc_id)), KApply('ProjectionElems::empty'), # TODO - self.metadata.to_kast(), + KApply( + 'Metadata', + ( + self.metadata.to_kast(), + intToken(0), + self.metadata.to_kast(), + ), + ), ) -class Metadata(ABC): +class MetadataSize(ABC): @abstractmethod def to_kast(self) -> KInner: ... @dataclass -class NoMetadata(Metadata): +class NoMetadata(MetadataSize): def to_kast(self) -> KInner: return KApply('noMetadata') @@ -116,7 +123,7 @@ def to_kast(self) -> KInner: @dataclass -class StaticSize(Metadata): +class StaticSize(MetadataSize): size: int def to_kast(self) -> KInner: @@ -124,7 +131,7 @@ def to_kast(self) -> KInner: @dataclass -class DynamicSize(Metadata): +class DynamicSize(MetadataSize): size: int def to_kast(self) -> KInner: diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state index 3e8bde783..5c2707c89 100644 --- a/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state +++ b/kmir/src/tests/integration/data/exec-smir/allocs/array_const_compare.state @@ -32,12 +32,12 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( AllocRef ( allocId ( 0 ) , .ProjectionElems , staticSize ( 3 ) ) ) - ListItem ( AllocRef ( allocId ( 1 ) , .ProjectionElems , staticSize ( 3 ) ) ) ) , ty ( 86 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( AllocRef ( allocId ( 0 ) , .ProjectionElems , metadata ( staticSize ( 3 ) , 0 , staticSize ( 3 ) ) ) ) + ListItem ( AllocRef ( allocId ( 1 ) , .ProjectionElems , metadata ( staticSize ( 3 ) , 0 , staticSize ( 3 ) ) ) ) ) , ty ( 86 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 0 ) , .ProjectionElems , staticSize ( 3 ) ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 1 ) , .ProjectionElems , staticSize ( 3 ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 0 ) , .ProjectionElems , metadata ( staticSize ( 3 ) , 0 , staticSize ( 3 ) ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 1 ) , .ProjectionElems , metadata ( staticSize ( 3 ) , 0 , staticSize ( 3 ) ) ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 69 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 68 ) , mutabilityNot ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state b/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state index a32dddf86..6c3fa5051 100644 --- a/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state +++ b/kmir/src/tests/integration/data/exec-smir/allocs/array_nest_compare.state @@ -36,12 +36,12 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( AllocRef ( allocId ( 0 ) , .ProjectionElems , staticSize ( 2 ) ) ) - ListItem ( AllocRef ( allocId ( 1 ) , .ProjectionElems , staticSize ( 2 ) ) ) ) , ty ( 107 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( AllocRef ( allocId ( 0 ) , .ProjectionElems , metadata ( staticSize ( 2 ) , 0 , staticSize ( 2 ) ) ) ) + ListItem ( AllocRef ( allocId ( 1 ) , .ProjectionElems , metadata ( staticSize ( 2 ) , 0 , staticSize ( 2 ) ) ) ) ) , ty ( 107 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 28 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 28 ) , mutabilityMut ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 0 ) , .ProjectionElems , staticSize ( 2 ) ) , ty ( 28 ) , mutabilityNot ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 1 ) , .ProjectionElems , staticSize ( 2 ) ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 0 ) , .ProjectionElems , metadata ( staticSize ( 2 ) , 0 , staticSize ( 2 ) ) ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 1 ) , .ProjectionElems , metadata ( staticSize ( 2 ) , 0 , staticSize ( 2 ) ) ) , ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 85 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 84 ) , mutabilityNot ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state b/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state index aa870846e..96b5c29ae 100644 --- a/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state +++ b/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state @@ -1,6 +1,6 @@ - #traverseProjection ( toLocal ( 13 ) , thunk ( #decodeConstant ( constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: provenanceMapEntry (... offset: 0 , allocId: allocId ( 1 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty ( 25 ) , typeInfoRefType ( ty ( 99 ) ) ) ) , projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 37 ) ) .ProjectionElems , .Contexts ) ~> #forRef ( mutabilityNot , noMetadata ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 14 ) , projection: .ProjectionElems ) , rvalue: rvalueCopyForDeref ( place (... local: local ( 3 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 25 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 14 ) , projection: projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 1 ) , ty ( 45 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 15 ) , projection: .ProjectionElems ) , rvalue: rvalueCopyForDeref ( place (... local: local ( 3 ) , projection: projectionElemField ( fieldIdx ( 1 ) , ty ( 25 ) ) .ProjectionElems ) ) ) , span: span ( 145 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 15 ) , projection: projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 37 ) ) .ProjectionElems ) ) ) , span: span ( 145 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 16 ) , projection: .ProjectionElems ) , rvalue: rvalueCopyForDeref ( place (... local: local ( 3 ) , projection: projectionElemField ( fieldIdx ( 1 ) , ty ( 25 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 16 ) , projection: projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 1 ) , ty ( 45 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 4 ) , projection: .ProjectionElems ) ) ) , span: span ( 145 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 10 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 6 ) , projection: .ProjectionElems ) ) ) , span: span ( 145 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 145 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 93 ) , id: mirConstId ( 47 ) ) ) ) , args: operandMove ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) operandMove ( place (... local: local ( 10 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 8 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 145 ) ) ) ~> .K + #traverseProjection ( toLocal ( 13 ) , thunk ( #decodeConstant ( constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: provenanceMapEntry (... offset: 0 , allocId: allocId ( 1 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty ( 25 ) , typeInfoRefType ( ty ( 99 ) ) ) ) , projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 37 ) ) .ProjectionElems , .Contexts ) ~> #forRef ( mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 14 ) , projection: .ProjectionElems ) , rvalue: rvalueCopyForDeref ( place (... local: local ( 3 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 25 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 14 ) , projection: projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 1 ) , ty ( 45 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 15 ) , projection: .ProjectionElems ) , rvalue: rvalueCopyForDeref ( place (... local: local ( 3 ) , projection: projectionElemField ( fieldIdx ( 1 ) , ty ( 25 ) ) .ProjectionElems ) ) ) , span: span ( 145 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 15 ) , projection: projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 37 ) ) .ProjectionElems ) ) ) , span: span ( 145 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 16 ) , projection: .ProjectionElems ) , rvalue: rvalueCopyForDeref ( place (... local: local ( 3 ) , projection: projectionElemField ( fieldIdx ( 1 ) , ty ( 25 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 16 ) , projection: projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 1 ) , ty ( 45 ) ) .ProjectionElems ) ) ) , span: span ( 147 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 4 ) , projection: .ProjectionElems ) ) ) , span: span ( 145 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 10 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 6 ) , projection: .ProjectionElems ) ) ) , span: span ( 145 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 145 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 93 ) , id: mirConstId ( 47 ) ) ) ) , args: operandMove ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) operandMove ( place (... local: local ( 10 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 8 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 145 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state index a4e52f93f..7e5876270 100644 --- a/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state +++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_inlined.state @@ -71,16 +71,16 @@ ListItem ( typedValue ( Moved , ty ( 42 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved ) ListItem ( Moved ) ) , ty ( 47 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 27 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) ) , ty ( 48 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 27 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 48 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( -200 , 32 , true ) , ty ( 16 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( -2 , 32 , true ) , ty ( 16 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved ) ListItem ( Moved ) ) , ty ( 47 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 27 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 27 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 42 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 16 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 16 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state index b5fd26e06..861180b8d 100644 --- a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state +++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state @@ -39,7 +39,7 @@ ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 4 , 64 , false ) , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 1 , minLength: 0 , fromEnd: false ) .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 31 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 1 , minLength: 0 , fromEnd: false ) .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 4 , 64 , false ) , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 30 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state index 42d20c987..b05e88c0e 100644 --- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state +++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox.state @@ -33,12 +33,12 @@ ListItem ( typedValue ( Integer ( 11 , 32 , false ) , ty ( 26 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( AllocRef ( allocId ( 0 ) , .ProjectionElems , noMetadata ) ) ) , ty ( 47 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( AllocRef ( allocId ( 0 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 47 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 0 ) , .ProjectionElems , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 0 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 41 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state b/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state index 95201e717..baeb2b64a 100644 --- a/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state +++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state @@ -32,8 +32,8 @@ ListItem ( typedValue ( Integer ( 42 , 32 , true ) , ty ( 16 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 42 , 32 , true ) , ty ( 16 ) , mutabilityNot ) ) ListItem ( typedValue ( BoolVal ( true ) , ty ( 28 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 29 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 29 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 29 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 29 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state b/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state index df69429dc..2f67853c8 100644 --- a/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state +++ b/kmir/src/tests/integration/data/exec-smir/niche-enum/niche-enum.state @@ -38,35 +38,35 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 3 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( AllocRef ( allocId ( 2 ) , .ProjectionElems , noMetadata ) ) ) , ty ( 51 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 3 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( AllocRef ( allocId ( 2 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 51 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , .List ) , ty ( 46 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 3 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 2 ) , .ProjectionElems , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 3 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 2 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 44 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 38 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 37 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 39 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( AllocRef ( allocId ( 3 ) , .ProjectionElems , noMetadata ) ) ) , ty ( 51 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( AllocRef ( allocId ( 3 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 51 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Aggregate ( variantIdx ( 0 ) , .List ) ) ) , ty ( 46 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 3 ) , .ProjectionElems , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 13 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 3 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 44 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 38 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 37 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 39 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 23 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( AllocRef ( allocId ( 4 ) , .ProjectionElems , noMetadata ) ) ) , ty ( 51 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 23 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( AllocRef ( allocId ( 4 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 51 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Aggregate ( variantIdx ( 1 ) , .List ) ) ) , ty ( 46 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 23 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( AllocRef ( allocId ( 4 ) , .ProjectionElems , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 23 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( AllocRef ( allocId ( 4 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 44 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 38 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 37 ) , mutabilityNot ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state index 70178511b..6e2c445d7 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-length-test-fail.state @@ -41,7 +41,7 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , dynamicSize ( 8 ) ) , ty ( 26 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 38 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 29 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 39 ) , mutabilityMut ) ) @@ -49,13 +49,13 @@ ListItem ( Integer ( 42 , 8 , false ) ) ListItem ( Integer ( 42 , 8 , false ) ) ListItem ( Integer ( 42 , 8 , false ) ) ) , ty ( 40 ) , mutabilityNot ) ) - ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , ptrEmulation ( staticSize ( 4 ) ) ) , ty ( 35 ) , mutabilityMut ) ) + ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 4 ) , 0 , noMetadataSize ) ) , ty ( 35 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 29 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 41 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 39 ) , mutabilityMut ) ) - ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , ptrEmulation ( staticSize ( 4 ) ) ) , ty ( 36 ) , mutabilityNot ) ) + ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 4 ) , 0 , noMetadataSize ) ) , ty ( 36 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 29 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 4 , 64 , false ) , ty ( 29 ) , mutabilityMut ) ) @@ -64,10 +64,10 @@ ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 41 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 39 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityNot , dynamicSize ( 4 ) ) , ty ( 26 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityNot , staticSize ( 4 ) ) , ty ( 41 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 4 ) , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 4 ) , 0 , noMetadataSize ) ) , ty ( 41 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 42 ) , mutabilityNot ) ) - ListItem ( typedValue ( PtrLocal ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityNot , ptrEmulation ( staticSize ( 9 ) ) ) , ty ( 37 ) , mutabilityMut ) ) + ListItem ( typedValue ( PtrLocal ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 9 ) , 0 , noMetadataSize ) ) , ty ( 37 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 26 ) , mutabilityMut ) ) @@ -83,7 +83,7 @@ ListItem ( Integer ( 42 , 8 , false ) ) ) , ty ( 30 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , staticSize ( 8 ) ) , ty ( 31 ) , mutabilityNot ) ) ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityNot ) ) ) ) ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state b/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state index 84d76d60d..c90e1b425 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state +++ b/kmir/src/tests/integration/data/exec-smir/references/array_elem_ref.state @@ -33,11 +33,11 @@ ListItem ( Integer ( 0 , 32 , false ) ) ListItem ( Integer ( 0 , 32 , false ) ) ListItem ( Integer ( 0 , 32 , false ) ) ) , ty ( 34 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 3 , minLength: 0 , fromEnd: false ) .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 27 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 3 , minLength: 0 , fromEnd: false ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 27 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 3 , 64 , false ) , ty ( 31 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 4 , 64 , false ) , ty ( 31 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 35 ) , mutabilityMut ) ) - ListItem ( typedValue ( PtrLocal ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 3 , minLength: 0 , fromEnd: false ) .ProjectionElems ) , mutabilityNot , ptrEmulation ( noMetadata ) ) , ty ( 30 ) , mutabilityNot ) ) + ListItem ( typedValue ( PtrLocal ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 3 , minLength: 0 , fromEnd: false ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 30 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state index b0b2b9148..de694867d 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state +++ b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state @@ -32,18 +32,18 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 22 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 22 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 21 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 34 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 21 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 11 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 22 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 11 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 22 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 34 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 22 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 22 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state index bfef72bc6..951a10279 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state +++ b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state @@ -33,10 +33,10 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 22 , 8 , true ) , ty ( 2 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 28 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 28 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state index db3bb356c..043aae9d7 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state +++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state @@ -31,7 +31,7 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 29 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state index db3bb356c..043aae9d7 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state +++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state @@ -31,7 +31,7 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 29 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state index 080d3afa0..7301205f2 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state +++ b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state @@ -30,8 +30,8 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 28 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 28 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 29 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/references/simple.state b/kmir/src/tests/integration/data/exec-smir/references/simple.state index d3c43f58c..86f6e5353 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/simple.state +++ b/kmir/src/tests/integration/data/exec-smir/references/simple.state @@ -29,7 +29,7 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 27 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 27 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 28 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state index f0da321f4..454f37867 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state +++ b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state @@ -39,29 +39,29 @@ ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , true ) ) ListItem ( BoolVal ( true ) ) ListItem ( Integer ( 43 , 64 , false ) ) ) , ty ( 30 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) ) .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 31 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) ) .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) ) .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 31 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 33 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) ) .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 33 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) ) ) , ty ( 34 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 29 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 9 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 35 ) , mutabilityNot ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 34 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 9 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 35 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 43 , 8 , true ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 2 ) , ty ( 26 ) ) .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 36 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 2 ) , ty ( 26 ) ) .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 36 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) ) .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 31 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 29 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 29 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 29 ) , mutabilityMut ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) ) .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 29 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/prove-rs/offset_read.rs b/kmir/src/tests/integration/data/prove-rs/offset_read.rs new file mode 100644 index 000000000..1cf15eb01 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/offset_read.rs @@ -0,0 +1,5 @@ +fn main() { + let arr = [11, 22, 33]; + let subslice = &arr[1..]; + assert!(subslice == [22, 33]); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/offset_struct_field_read.rs b/kmir/src/tests/integration/data/prove-rs/offset_struct_field_read.rs new file mode 100644 index 000000000..f5294fd11 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/offset_struct_field_read.rs @@ -0,0 +1,9 @@ +struct Foo { + arr: [u16; 3], +} + +fn main() { + let foo = Foo { arr: [11, 22, 33] }; + let subslice = &foo.arr[1..]; + assert!(subslice == [22, 33]); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/offset_struct_field_write.rs b/kmir/src/tests/integration/data/prove-rs/offset_struct_field_write.rs new file mode 100644 index 000000000..17aa28581 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/offset_struct_field_write.rs @@ -0,0 +1,10 @@ +struct Foo { + arr: [u16; 3], +} + +fn main() { + let mut foo = Foo { arr: [11, 22, 33] }; + let subslice = &mut foo.arr[1..]; + subslice[0] = 44; + assert!(foo.arr == [11, 44, 33]); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/offset_write.rs b/kmir/src/tests/integration/data/prove-rs/offset_write.rs new file mode 100644 index 000000000..994a51c81 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/offset_write.rs @@ -0,0 +1,6 @@ +fn main() { + let mut arr = [11, 22, 33]; + let subslice = &mut arr[1..]; + subslice[0] = 44; + assert!(arr == [11, 44, 33]); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/slice-split-at.rs b/kmir/src/tests/integration/data/prove-rs/slice-split-at.rs new file mode 100644 index 000000000..bfc1d6394 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/slice-split-at.rs @@ -0,0 +1,27 @@ +fn main() { + let arr: [u8; 2] = [42, 255]; + let slice = arr.as_slice(); + let (left, right) = slice.split_at(1); + assert!(left == [42]); + assert!(right == [255]); + + let arr: [u8; 3] = [42, 255, 66]; + let slice = arr.as_slice(); + let (left, right) = slice.split_at(1); + assert!(left == [42]); + assert!(right == [255, 66]); + + // Empty Case RHS + let arr: [u8; 3] = [42, 255, 66]; + let slice = arr.as_slice(); + let (left, right) = slice.split_at(3); + assert!(left == [42, 255, 66]); + assert!(right == []); + + // Empty Case LHS + let arr: [u8; 3] = [42, 255, 66]; + let slice = arr.as_slice(); + let (left, right) = slice.split_at(0); + assert!(left == []); + assert!(right == [42, 255, 66]); +} diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected index b5d442e5f..d4175ed23 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-1.expected @@ -60,13 +60,13 @@ ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 18 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) ) , ty ( 22 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 22 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( BoolVal ( false ) , ty ( 18 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected index f90e3829c..fe0fc56a4 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-4.expected @@ -60,13 +60,13 @@ ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 18 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) ) , ty ( 22 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 22 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( BoolVal ( false ) , ty ( 18 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected index 34ed3e3e2..f39dc9787 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-7.expected @@ -60,13 +60,13 @@ ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 18 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) ) , ty ( 22 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 22 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( BoolVal ( false ) , ty ( 18 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected index e5c5e76da..3bd535f28 100644 --- a/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/simple-types/final-9.expected @@ -60,13 +60,13 @@ ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 18 ) , mutabilityMut ) ) ListItem ( newLocal ( ty ( 12 ) , mutabilityMut ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) - ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) ) ) , ty ( 22 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) + ListItem ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ) ) , ty ( 22 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) ) ListItem ( typedValue ( BoolVal ( false ) , ty ( 18 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) - ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 22 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 2 ) , mutabilityNot ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) ListItem ( typedValue ( Moved , ty ( 18 ) , mutabilityMut ) ) From 851533dfcff61ee9d44c406a91444d648f49cee1 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 24 Oct 2025 19:31:30 +1100 Subject: [PATCH 2/2] adjust p-token cheatcode module to metadata change --- kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md index c9140c5c6..9761323ac 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md @@ -635,7 +635,7 @@ NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same wa => #setLocalValue( DEST, Aggregate(variantIdx(0), - ListItem(Reference(OFFSET, place(LOCAL, appendP(PROJS, ACCESS_PROJ)), MUT, noMetadata)) + ListItem(Reference(OFFSET, place(LOCAL, appendP(PROJS, ACCESS_PROJ)), MUT, metadata(noMetadataSize, 0, noMetadataSize))) ) ) ... @@ -643,7 +643,7 @@ NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same wa rule #mkPAccountRef(DEST, PAccByteRef(OFFSET, place(LOCAL, PROJS), MUT, _LEN), ACCESS_PROJ, false) => #setLocalValue( DEST, - Reference(OFFSET, place(LOCAL, appendP(PROJS, ACCESS_PROJ)), MUT, noMetadata) + Reference(OFFSET, place(LOCAL, appendP(PROJS, ACCESS_PROJ)), MUT, metadata(noMetadataSize, 0, noMetadataSize)) ) ...