diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 82c28b3f0..9040d32d9 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -219,6 +219,24 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped. ```k + // `place(local(-1), .ProjectionElems)` is the sentinel destination for calls whose + // return should not be written back. Without this rule, the return path would fall + // through to `#setLocalValue`, which only accepts real local indices and would get + // stuck on `local(-1)`. + rule [termReturnIgnored]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ + => + #execBlockIdx(TARGET) + + _ => CALLER + _ => #getBlocks(CALLER) + CALLER => NEWCALLER + place(local(-1), .ProjectionElems) => NEWDEST + someBasicBlockIdx(TARGET) => NEWTARGET + _ => UNWIND + _ => NEWLOCALS + ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK + [priority(40)] + rule [termReturnSome]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #setLocalValue(DEST, #decrementRef(VAL)) ~> #execBlockIdx(TARGET) @@ -349,6 +367,38 @@ where the returned result should go. requires isIntrinsicFunction(FUNC) andBool #functionNameMatchesEnv(getFunctionName(FUNC)) + syntax Bool ::= isNoOpFunction(MonoItemKind) [function] + rule isNoOpFunction(monoItemFn(symbol(""), _, noBody)) => true + rule isNoOpFunction(_) => false [owise] + + syntax KItem ::= #consumeNoOpArgs(Operands, MaybeBasicBlockIdx) + | #consumeNoOpArg(Operand) + + // SMIR marks some semantically empty shims (e.g. drop glue for trivially droppable slices) + // as NoOpSym. They have no body and should continue immediately without switching frames, + // but `Move` arguments must still invalidate the caller locals that were moved into the call. + rule [termCallNoOp]: + #execTerminatorCall(_, monoItemFn(symbol(""), _, noBody), ARGS, _DEST, TARGET, _UNWIND, _SPAN) ~> _ + => #consumeNoOpArgs(ARGS, TARGET) + + + rule #consumeNoOpArgs(.Operands, TARGET) => #continueAt(TARGET) ... + + rule #consumeNoOpArgs(OP:Operand MORE:Operands, TARGET) + => #consumeNoOpArg(OP) ~> #consumeNoOpArgs(MORE, TARGET) + ... + + + // Constants have no side effects worth preserving. + rule #consumeNoOpArg(operandConstant(_)) => .K ... + + // For Copy/Move operands, delegate to the normal operand evaluation path so that + // projected places are traversed correctly and only the precise subplace is marked + // Moved. The resulting value is discarded since the call is a no-op. + syntax KItem ::= "#discardNoOpResult" + rule #consumeNoOpArg(OP:Operand) => OP ~> #discardNoOpResult ... [owise] + rule _:Value ~> #discardNoOpResult => .K ... + // Regular function call - full state switching and stack setup rule [termCallFunction]: #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _ @@ -365,6 +415,7 @@ where the returned result should go. STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK requires notBool isIntrinsicFunction(FUNC) + andBool notBool isNoOpFunction(FUNC) andBool notBool #functionNameMatchesEnv(getFunctionName(FUNC)) // Function call to a function in the break-on set - same as termCallFunction but separate rule id for cut-point @@ -383,6 +434,7 @@ where the returned result should go. STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK requires notBool isIntrinsicFunction(FUNC) + andBool notBool isNoOpFunction(FUNC) andBool #functionNameMatchesEnv(getFunctionName(FUNC)) syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function] @@ -442,6 +494,7 @@ An operand may be a `Reference` (the only way a function could access another fu ```k syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands, Span) + | #setUpDropGlueData(MonoItemKind, Value, Span) // reserve space for local variables and copy/move arguments from old locals into their place rule [setupCalleeData]: #setUpCalleeData( @@ -466,6 +519,21 @@ An operand may be a `Reference` (the only way a function could access another fu // TODO: Haven't handled "noBody" case + rule [setupDropGlueData]: #setUpDropGlueData( + monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))), + PTR, + _SPAN + ) + => + #setLocalValue(place(local(1), .ProjectionElems), #incrementRef(PTR)) ~> #execBlock(FIRST) + ... + + + _ => toKList(BLOCKS) + _ => #reserveFor(NEWLOCALS) + ... + + syntax List ::= #reserveFor( LocalDecls ) [function, total] rule #reserveFor(.LocalDecls) => .List @@ -669,12 +737,53 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error. ```k - rule [termDrop]: #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN)) + syntax MaybeTy ::= #dropPlaceTy(Place, List) [function, total] + + rule #dropPlaceTy(place(local(I), PROJS), LOCALS) + => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + requires 0 <=Int I andBool I TyUnknown [owise] + + syntax KItem ::= #execDropCall ( MaybeTy, Place, BasicBlockIdx, UnwindAction, Span ) + | #callDropGlue ( Ty, BasicBlockIdx, UnwindAction, Span ) + + rule [termDrop]: #execTerminator(terminator(terminatorKindDrop(PLACE, TARGET, UNWIND), SPAN)) + => + #execDropCall(#lookupDropFunctionTy(#dropPlaceTy(PLACE, LOCALS)), PLACE, TARGET, UNWIND, SPAN) + ... + + LOCALS + + rule #execDropCall(TyUnknown, _PLACE, TARGET, _UNWIND, _SPAN) => #execBlockIdx(TARGET) ... + rule #execDropCall(FTY:Ty, PLACE, TARGET, UNWIND, SPAN) + => + rvalueAddressOf(mutabilityMut, PLACE) ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN) + ... + + + rule [termCallDropGlue]: + PTR:Value ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN) ~> _ + => #setUpDropGlueData(lookupFunction(FTY), PTR, SPAN) + + CALLER => FTY + + _ + OLDCALLER => CALLER + OLDDEST => place(local(-1), .ProjectionElems) + OLDTARGET => someBasicBlockIdx(TARGET) + OLDUNWIND => UNWIND + LOCALS + + STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK + syntax MIRError ::= "ReachedUnreachable" rule [termUnreachable]: #execTerminator(terminator(terminatorKindUnreachable, _SPAN)) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 5839521b4..428acb9c6 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -148,7 +148,7 @@ We ensure that any projections of the copy operation are traversed appropriately ```k rule operandCopy(place(local(I), PROJECTIONS)) - => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJECTIONS, .Contexts) + => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJECTIONS, .Contexts, .ProjectionElems) ~> #readProjection(false) ... @@ -164,7 +164,7 @@ In contrast to regular write operations, the value does not have to be _mutable_ ```k rule operandMove(place(local(I), PROJECTIONS)) - => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJECTIONS, .Contexts) + => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJECTIONS, .Contexts, .ProjectionElems) ~> #readProjection(true) ... @@ -201,7 +201,7 @@ If we are setting a value at a `Place` which has `Projection`s in it, then we mu [preserves-definedness] // valid list indexing checked rule #setLocalValue(place(local(I), PROJ), VAL) - => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJ, .Contexts) + => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJ, .Contexts, .ProjectionElems) ~> #writeProjection(VAL) ... @@ -240,33 +240,37 @@ There are different kinds of `ProjectionElem`s: - Casting values (`OpaqueCast` or `Downcast` - variant narrowing) and `Subtype`ing Read and write operations to places that include (a chain of) projections are handled by a special rewrite symbol `#traverseProjection`. -This helper does the projection lookup and maintains the context chain along the lookup path, then passes control back to `#readProjection` and `#writeProjection`/`#setMoved`. +This helper separates two different concerns that used to be conflated: + +- `Contexts` record only the inverse structural updates needed for write-back (`#buildUpdate`) +- the final `ProjectionElems` argument accumulates the forward surface place path used when rebuilding references and pointers + A `Deref` projection in the projections list changes the target of the write operation, while `Field` updates change the value that is being written (updating just one field of it), recursively. ```k - syntax KItem ::= #traverseProjection ( WriteTo , Value, ProjectionElems, Contexts ) + syntax KItem ::= #traverseProjection ( WriteTo , Value, ProjectionElems, Contexts, ProjectionElems ) | #readProjection ( Bool ) | #writeProjection ( Value ) | "#writeMoved" - rule #traverseProjection(_, VAL, .ProjectionElems, _) ~> #readProjection(false) => VAL ... - rule #traverseProjection(_, VAL, .ProjectionElems, _) ~> (#readProjection(true) => #writeMoved ~> VAL) ... + rule #traverseProjection(_, VAL, .ProjectionElems, _, _) ~> #readProjection(false) => VAL ... + rule #traverseProjection(_, VAL, .ProjectionElems, _, _) ~> (#readProjection(true) => #writeMoved ~> VAL) ... - rule #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS) + rule #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS, _PATH) ~> #writeProjection(NEW) => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) ... [preserves-definedness] // valid context ensured upon context construction - rule #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS) + rule #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS, _PATH) ~> #writeMoved => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(Moved, CONTEXTS)) // TODO retain Ty and Mutability from _ORIGINAL ... [preserves-definedness] // valid context ensured upon context construction - rule #traverseProjection(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, CONTEXTS) + rule #traverseProjection(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, CONTEXTS, _PATH) ~> #writeProjection(NEW) => .K ... @@ -284,7 +288,7 @@ A `Deref` projection in the projections list changes the target of the write ope andBool isStackFrame(STACK[FRAME -Int 1]) [preserves-definedness] // valid context ensured upon context construction - rule #traverseProjection(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, CONTEXTS) + rule #traverseProjection(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, CONTEXTS, _PATH) ~> #writeMoved => .K ... @@ -314,16 +318,25 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr | toStack ( Int , Local ) | toAlloc ( AllocId ) - // retains information about the value that was deconstructed by a projection + // retains information about the value that was deconstructed by a projection. + // These frames are only used for write-back reconstruction. syntax Context ::= CtxField( VariantIdx, List, Int , Ty ) | CtxFieldUnion( FieldIdx, Value, Ty ) | CtxIndex( List , Int ) // array index constant or has been read before + | CtxRangeHead( List ) // inverse frame for the implicit head-element selection on a range | 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) | "CtxWrapStruct" // special context adding a singleton Aggregate(0, _) around a value syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us + // PointerOffset operates on a canonical range view. Bare values are treated as a + // singleton range, and later scalar projections transparently descend into the + // head element through CtxRangeHead instead of materializing a fake index-0 step. + syntax Value ::= #rangeView ( Value ) [function, total] + rule #rangeView(Range(ELEMS)) => Range(ELEMS) + rule #rangeView(VAL) => Range(ListItem(VAL)) requires notBool isRange(VAL) + syntax Contexts ::= List{Context, ""} syntax Value ::= #buildUpdate ( Value , Contexts ) [function] @@ -343,6 +356,12 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr => #buildUpdate(Range(ELEMS[I <- VAL]), CTXS) [preserves-definedness] // valid list indexing checked upon context construction + rule #buildUpdate(VAL, CtxRangeHead(ELEMS) CTXS) + => #buildUpdate(Range(ELEMS[0 <- VAL]), CTXS) + requires 0 #buildUpdate( Range(updateList(ELEMS, START, INNER)), CTXS) @@ -369,12 +388,13 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr andBool isTypedLocal(LOCALS[I]) [preserves-definedness] // valid list indexing and sort checked - syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total] syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total] | consP ( ProjectionElem , ProjectionElems ) [function, total] + | #pushProjection ( ProjectionElems , ProjectionElem ) [function, total] // ---------------------------------------------------------------------------------------- rule appendP(.ProjectionElems, TAIL) => TAIL rule appendP(X:ProjectionElem REST:ProjectionElems, TAIL) => consP(X, appendP(REST, TAIL)) + rule #pushProjection(PROJS, PROJ) => appendP(PROJS, PROJ .ProjectionElems) // default rule consP( PROJ , .ProjectionElems ) => PROJ .ProjectionElems rule consP( PROJ , P:ProjectionElem PS:ProjectionElems) => PROJ (P PS) @@ -384,12 +404,20 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr rule consP(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) PS:ProjectionElems) => PS [priority(40)] // this rule is not valid if the original pointee has more than one field // rule consP(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct PS:ProjectionElems) => PS [priority(40)] - // HACK: special rule which munges together constant-indexing and offset projections + // Canonicalize an appended pointer offset against an already indexed place path. rule consP( projectionElemConstantIndex(I, 0, false), PointerOffset(OFF, _SIZE) PS) => projectionElemConstantIndex(I +Int OFF, 0, false) PS [priority(40)] // requires I +Int OFF < _SIZE // _SIZE is metadataSize, needs a < operation for this to work rule consP(projectionElemToZST, projectionElemFromZST PS:ProjectionElems) => PS [priority(40)] rule consP(projectionElemFromZST, projectionElemToZST PS:ProjectionElems) => PS [priority(40)] + syntax Bool ::= #projectsHead ( ProjectionElem ) [function, total] + // --------------------------------------------------------------- + rule #projectsHead(projectionElemDeref) => true + rule #projectsHead(projectionElemField(_, _)) => true + rule #projectsHead(projectionElemDowncast(_)) => true + rule #projectsHead(projectionElemWrapStruct) => true + rule #projectsHead(_OTHER) => false [owise] + syntax Value ::= #localFromFrame ( StackFrame, Local, Int ) [function] rule #localFromFrame(StackFrame(... locals: LOCALS), local(I:Int), OFFSET) => #adjustRef(getValue(LOCALS, I), OFFSET) @@ -447,13 +475,15 @@ This is done without consideration of the validity of the Downcast[^downcast]. DEST, Aggregate(IDX, ARGS), projectionElemField(fieldIdx(I), TY) PROJS, - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, getValue(ARGS, I), PROJS, - CtxField(IDX, ARGS, I, TY) CTXTS + CtxField(IDX, ARGS, I, TY) CTXTS, + #pushProjection(PATH, projectionElemField(fieldIdx(I), TY)) ) ... @@ -465,13 +495,15 @@ This is done without consideration of the validity of the Downcast[^downcast]. DEST, Aggregate(_, ARGS), projectionElemDowncast(IDX) PROJS, - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, Aggregate(IDX, ARGS), PROJS, - CTXTS + CTXTS, + #pushProjection(PATH, projectionElemDowncast(IDX)) ) ... @@ -488,26 +520,46 @@ The situation typically arises when the stored value is a pointer (`NonNull`) bu DEST, VALUE, projectionElemWrapStruct PROJS, - CTXTS + CTXTS, + PATH ) - => #traverseProjection(DEST, Aggregate(variantIdx(0), ListItem(VALUE)), PROJS, CtxWrapStruct CTXTS) ... + => #traverseProjection( + DEST, + Aggregate(variantIdx(0), ListItem(VALUE)), + PROJS, + CtxWrapStruct CTXTS, + #pushProjection(PATH, projectionElemWrapStruct) + ) ... [preserves-definedness, priority(100)] ``` A somewhat dual case to this rule can occur when a pointer into an array of data elements has been offset and is then dereferenced. The dereferenced pointer may either point to a subslice or to a single element (depending on context). -Therefore, a field projection may be found which has to be applied to the head element of an array. -The following rule resolves this situation by using the head element. +Subsequent scalar projections such as `Field`, `Downcast`, `Deref`, or `WrapStruct` +should act on that single pointed-at element, but the enclosing range still has to be +available for write-back. Instead of re-encoding every scalar projection against +`Range(ListItem(...))`, we first descend into the head element and remember that +implicit step via `CtxRangeHead(...)`, leaving the forward `PATH` unchanged. ```k rule #traverseProjection( DEST, - Range(ListItem(Aggregate(_, _) #as VALUE) _REST:List), - projectionElemField(IDX, TY) PROJS, - CTXTS + Range(ListItem(HEAD) REST:List), + (PROJ:ProjectionElem PROJS), + CTXTS, + PATH ) - => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? - [preserves-definedness, priority(100)] + => #traverseProjection( + DEST, + HEAD, + PROJ PROJS, + CtxRangeHead(ListItem(HEAD) REST) CTXTS, + PATH + ) + ... + + requires #projectsHead(PROJ) + [preserves-definedness] ``` #### Unions @@ -517,13 +569,15 @@ The following rule resolves this situation by using the head element. DEST, Union(FIELD_IDX, ARG), projectionElemField(FIELD_IDX, TY) PROJS, - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, ARG, PROJS, - CtxFieldUnion(FIELD_IDX, ARG, TY) CTXTS + CtxFieldUnion(FIELD_IDX, ARG, TY) CTXTS, + #pushProjection(PATH, projectionElemField(FIELD_IDX, TY)) ) ... @@ -544,13 +598,15 @@ In case of a `ConstantIndex`, the index is provided as an immediate value, toget DEST, Range(ELEMENTS), projectionElemIndex(local(LOCAL)) PROJS, - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, getValue(ELEMENTS, #expectUsize(getValue(LOCALS, LOCAL))), PROJS, - CtxIndex(ELEMENTS, #expectUsize(getValue(LOCALS, LOCAL))) CTXTS + CtxIndex(ELEMENTS, #expectUsize(getValue(LOCALS, LOCAL))) CTXTS, + #pushProjection(PATH, projectionElemConstantIndex(#expectUsize(getValue(LOCALS, LOCAL)), 0, false)) ) ... @@ -566,13 +622,15 @@ In case of a `ConstantIndex`, the index is provided as an immediate value, toget DEST, Range(ELEMENTS), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, getValue(ELEMENTS, OFFSET), PROJS, - CtxIndex(ELEMENTS, OFFSET) CTXTS + CtxIndex(ELEMENTS, OFFSET) CTXTS, + #pushProjection(PATH, projectionElemConstantIndex(OFFSET, 0, false)) ) ... @@ -584,13 +642,15 @@ In case of a `ConstantIndex`, the index is provided as an immediate value, toget DEST, Range(ELEMENTS), projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, // from end - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, - getValue(ELEMENTS, OFFSET), + getValue(ELEMENTS, MINLEN -Int OFFSET), PROJS, - CtxIndex(ELEMENTS, MINLEN -Int OFFSET) CTXTS + CtxIndex(ELEMENTS, MINLEN -Int OFFSET) CTXTS, + #pushProjection(PATH, projectionElemConstantIndex(MINLEN -Int OFFSET, 0, false)) ) ... @@ -615,13 +675,15 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t DEST, Range(ELEMENTS), projectionElemSubslice(START, END, false) PROJS, - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, Range(range(ELEMENTS, START, size(ELEMENTS) -Int END)), PROJS, - CtxSubslice(ELEMENTS, START, END) CTXTS + CtxSubslice(ELEMENTS, START, END) CTXTS, + #pushProjection(PATH, projectionElemSubslice(START, END, false)) ) ... @@ -634,13 +696,15 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t DEST, Range(ELEMENTS), projectionElemSubslice(START, END, true) PROJS, // END from end of ELEMS - CTXTS + CTXTS, + PATH ) => #traverseProjection( DEST, Range(range(ELEMENTS, START, END)), PROJS, - CtxSubslice(ELEMENTS, START, size(ELEMENTS) -Int END) CTXTS + CtxSubslice(ELEMENTS, START, size(ELEMENTS) -Int END) CTXTS, + #pushProjection(PATH, projectionElemSubslice(START, size(ELEMENTS) -Int END, false)) ) ... @@ -649,20 +713,43 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t andBool START <=Int size(ELEMENTS) -Int END [preserves-definedness] // Indexes checked to be in range for ELEMENTS + rule #traverseProjection( + DEST, + VAL, + PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, + CTXTS, + PATH + ) + => #traverseProjection( + DEST, + #rangeView(VAL), + PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, + CTXTS, + PATH + ) + ... + + requires notBool isRange(VAL) + [preserves-definedness, priority(100)] + rule #traverseProjection( DEST, Range(ELEMENTS), - PointerOffset(OFFSET, _ORIGIN_LENGTH) PROJS, // TODO: seems strange to not use the ORIGIN_LENGTH... - CTXTS + PointerOffset(OFFSET, _ORIGIN_LENGTH) PROJS, + CTXTS, + PATH ) => #traverseProjection( DEST, Range(range(ELEMENTS, OFFSET, 0)), PROJS, - CtxPointerOffset(ELEMENTS, OFFSET, size(ELEMENTS)) CTXTS + CtxPointerOffset(ELEMENTS, OFFSET, size(ELEMENTS)) CTXTS, + #pushProjection(PATH, PointerOffset(OFFSET, size(ELEMENTS))) ) ... + // After earlier projections have been applied, the current range is the offset origin + // we want to preserve for both write-back and reference/path reconstruction. requires 0 <=Int OFFSET andBool OFFSET <=Int size(ELEMENTS) [preserves-definedness] // Offset checked to be in range for ELEMENTS ``` @@ -685,8 +772,8 @@ An attempt to read more elements than the length of the accessed array is undefi syntax KItem ::= #derefTruncate ( MetadataSize , ProjectionElems ) // ---------------------------------------------------------------------------------------- // values other than `Range` do not have metadata anyway, they are passed along unchanged - rule #traverseProjection( DEST, VAL , .ProjectionElems, CTXTS) ~> #derefTruncate(noMetadataSize, PROJS) - => #traverseProjection(DEST, VAL, PROJS, CTXTS) + rule #traverseProjection( DEST, VAL , .ProjectionElems, CTXTS, PATH) ~> #derefTruncate(noMetadataSize, PROJS) + => #traverseProjection(DEST, VAL, PROJS, CTXTS, PATH) ... requires notBool isRange(VAL) @@ -698,36 +785,40 @@ An attempt to read more elements than the length of the accessed array is undefi rule isRange( _OTHER ) => false [owise] // staticSize metadata requires an array of suitable length and truncates it - rule #traverseProjection( DEST, Range(ELEMS), .ProjectionElems, CTXTS) ~> #derefTruncate(staticSize(SIZE), PROJS) - => #traverseProjection(DEST, Range(range(ELEMS, 0, size(ELEMS) -Int SIZE)), PROJS, CTXTS) + rule #traverseProjection( DEST, Range(ELEMS), .ProjectionElems, CTXTS, PATH) ~> #derefTruncate(staticSize(SIZE), PROJS) + => #traverseProjection(DEST, Range(range(ELEMS, 0, size(ELEMS) -Int SIZE)), PROJS, CTXTS, PATH) ... requires 0 <=Int SIZE andBool SIZE <=Int size(ELEMS) [preserves-definedness] // range parameters checked // dynamicSize metadata requires an array of suitable length and truncates it - rule #traverseProjection( DEST, Range(ELEMS), .ProjectionElems, CTXTS) ~> #derefTruncate(dynamicSize(SIZE), PROJS) - => #traverseProjection(DEST, Range(range(ELEMS, 0, size(ELEMS) -Int SIZE)), PROJS, CTXTS) + rule #traverseProjection( DEST, Range(ELEMS), .ProjectionElems, CTXTS, PATH) ~> #derefTruncate(dynamicSize(SIZE), PROJS) + => #traverseProjection(DEST, Range(range(ELEMS, 0, size(ELEMS) -Int SIZE)), PROJS, CTXTS, PATH) ... requires 0 <=Int SIZE andBool SIZE <=Int size(ELEMS) [preserves-definedness] // range parameters checked // If an array was projected to but no metadata is available, use the head element - rule #traverseProjection( DEST, Range(ListItem(VAL) _:List), .ProjectionElems, CTXTS) ~> #derefTruncate(noMetadataSize, PROJS) - => #traverseProjection(DEST, VAL, PROJS, CTXTS) + rule #traverseProjection( DEST, Range(ListItem(VAL) _:List), .ProjectionElems, CTXTS, PATH) ~> #derefTruncate(noMetadataSize, PROJS) + => #traverseProjection(DEST, VAL, PROJS, CTXTS, PATH) ... [preserves-definedness] + // Deref restarts traversal from the referred place. The previous update contexts and + // accumulated path belong to the pointer value itself, not to the pointee, so both reset. // Ref, 0 < OFFSET, 0 < PTR_OFFSET, ToStack rule #traverseProjection( _DEST, Reference(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset - .Contexts + .Contexts, + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -743,13 +834,15 @@ An attempt to read more elements than the length of the accessed array is undefi _DEST, Reference(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), PLACEPROJ, // apply reference projections with pointer offset - .Contexts + .Contexts, + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -765,13 +858,15 @@ An attempt to read more elements than the length of the accessed array is undefi _DEST, Reference(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toLocal(I), getValue(LOCALS, I), appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset - .Contexts + .Contexts, + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -788,13 +883,15 @@ An attempt to read more elements than the length of the accessed array is undefi _DEST, Reference(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toLocal(I), getValue(LOCALS, I), PLACEPROJ, - .Contexts + .Contexts, + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -811,13 +908,15 @@ An attempt to read more elements than the length of the accessed array is undefi _DEST, PtrLocal(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset - .Contexts // previous contexts obsolete + .Contexts, // previous contexts obsolete + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -833,13 +932,15 @@ An attempt to read more elements than the length of the accessed array is undefi _DEST, PtrLocal(OFFSET, place(LOCAL, PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), PLACEPROJ, // apply reference projections - .Contexts // add pointer offset context + .Contexts, // add pointer offset context + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -855,13 +956,15 @@ An attempt to read more elements than the length of the accessed array is undefi _DEST, PtrLocal(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toLocal(I), getValue(LOCALS, I), appendP(PLACEPROJ, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))), // apply reference projections with pointer offset - .Contexts // previous contexts obsolete + .Contexts, // previous contexts obsolete + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -878,13 +981,15 @@ An attempt to read more elements than the length of the accessed array is undefi _DEST, PtrLocal(OFFSET, place(local(I), PLACEPROJ), _MUT, metadata(SIZE, PTR_OFFSET, _ORIGIN_SIZE)), projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toLocal(I), getValue(LOCALS, I), PLACEPROJ, // apply reference projections - .Contexts // add pointer offset context + .Contexts, // add pointer offset context + .ProjectionElems ) ~> #derefTruncate(SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -906,13 +1011,15 @@ even though this could be supported. _DEST, AllocRef(ALLOC_ID, ALLOC_PROJS, metadata(METADATA_SIZE, _PTR_OFFSET, _)), // FIXME can this be offset? projectionElemDeref PROJS, - _CTXTS + _CTXTS, + _PATH ) => #traverseProjection( toAlloc(ALLOC_ID), {lookupAlloc(ALLOC_ID)}:>Value, ALLOC_PROJS, // alloc projections - .Contexts // previous contexts obsolete + .Contexts, // previous contexts obsolete + .ProjectionElems ) ~> #derefTruncate(METADATA_SIZE, PROJS) // then truncate, then continue with remaining projections ... @@ -1213,20 +1320,6 @@ As references are sometimes created by dereferencing other references or pointer This eliminates any `Deref` projections from the place, and also resolves `Index` projections to `ConstantIndex` ones. ```k - // reconstructs projections stored as context (used for Rvalues Ref and AddressOf ) - syntax ProjectionElems ::= #projectionsFor( Contexts ) [function, total] - | #projectionsFor( Contexts , ProjectionElems ) [function, total] - // ---------------------------------------------------------------------------------------- - rule #projectionsFor(CTXS) => #projectionsFor(CTXS, .ProjectionElems) - rule #projectionsFor( .Contexts , PROJS) => PROJS - 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 #projectionsFor(CtxFieldUnion(F_IDX, _, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(F_IDX, TY) PROJS) - rule #projectionsFor( CtxWrapStruct CTXS, PROJS) => #projectionsFor(CTXS, projectionElemWrapStruct PROJS) - // Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule. rule rvalueRef(REGION, KIND, place(local(I), PROJS)) => #setLocalValue( @@ -1247,7 +1340,7 @@ This eliminates any `Deref` projections from the place, and also resolves `Index [preserves-definedness] // valid list indexing checked, zero-sized locals materialise trivially rule rvalueRef(_REGION, KIND, place(local(I), PROJS)) - => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts) + => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts, .ProjectionElems) ~> #forRef(#mutabilityOf(KIND), metadata(#metadataSize(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO: Sus on this rule ... @@ -1259,8 +1352,8 @@ This eliminates any `Deref` projections from the place, and also resolves `Index syntax KItem ::= #forRef( Mutability , Metadata ) // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size - 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) ) + rule #traverseProjection(DEST, VAL:Value, .ProjectionElems, _CTXTS, PATH) ~> #forRef(MUT, metadata(SIZE, OFFSET, ORIGIN_SIZE)) + => #mkRef(DEST, PATH, MUT, metadata(#maybeDynamicSize(SIZE, VAL), OFFSET, ORIGIN_SIZE) ) ... @@ -1306,7 +1399,7 @@ The operation typically creates a pointer with empty metadata. rule rvalueAddressOf(MUT, place(local(I), PROJS)) => - #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts) + #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts, .ProjectionElems) ~> #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 ... @@ -1317,8 +1410,8 @@ The operation typically creates a pointer with empty metadata. [preserves-definedness] // valid list indexing checked, #metadataSize should only use static information // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size - 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)) + rule #traverseProjection(DEST, VAL:Value, .ProjectionElems, _CTXTS, PATH) ~> #forPtr(MUT, metadata(SIZE, OFFSET, ORIGIN_SIZE)) + => #mkPtr(DEST, PATH, MUT, metadata(#maybeDynamicSize(SIZE, VAL), OFFSET, ORIGIN_SIZE)) ... diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index aaf854c13..71fa2e773 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -211,6 +211,14 @@ To make this function total, an optional `MaybeTy` is used. syntax MaybeTy ::= Ty | "TyUnknown" + syntax MaybeTy ::= lookupDropFunctionTy ( Ty ) [function, total, symbol(lookupDropFunctionTy)] + | #lookupDropFunctionTy ( MaybeTy ) [function, total] + + rule #lookupDropFunctionTy(TY:Ty) => lookupDropFunctionTy(TY) + rule #lookupDropFunctionTy(TyUnknown) => TyUnknown + + rule lookupDropFunctionTy(_) => TyUnknown [owise] + syntax MaybeTy ::= #transparentFieldTy ( TypeInfo ) [function, total] rule #transparentFieldTy(typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) => FIELD diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 85035d4bd..905af7874 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -513,6 +513,20 @@ def get_int_arg(app: KInner) -> int: type_equations = _make_stratified_rules(kmir, 'lookupTy', 'Ty', 'TypeInfo', 'ty', type_assocs, invalid_type) + drop_function_assocs: list[tuple[int, KInner]] + drop_function_assocs = [ + (int(ty), KApply('ty', (intToken(int(drop_ty)),))) for ty, drop_ty in smir_info.drop_function_tys.items() + ] + drop_function_equations = _make_stratified_rules( + kmir, + 'lookupDropFunctionTy', + 'Ty', + 'MaybeTy', + 'ty', + drop_function_assocs, + KApply('TyUnknown_RT-TYPES_MaybeTy', ()), + ) + invalid_alloc_n = KApply( 'InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KApply('allocId', (KVariable('N'),)),) ) @@ -527,7 +541,7 @@ def get_int_arg(app: KInner) -> int: if break_on_function: break_on_rules.append(_mk_break_on_functions_rule(kmir, break_on_function)) - return [*equations, *type_equations, *alloc_equations, *break_on_rules] + return [*equations, *type_equations, *drop_function_equations, *alloc_equations, *break_on_rules] def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: @@ -557,6 +571,15 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: 'IntrinsicFunction', [KApply('symbol(_)_LIB_Symbol_String', [stringToken(sym['IntrinsicSym'])])], ) + elif 'NoOpSym' in sym: + functions[ty] = KApply( + 'MonoItemKind::MonoItemFn', + ( + KApply('symbol(_)_LIB_Symbol_String', (stringToken(sym['NoOpSym']),)), + KApply('defId(_)_BODY_DefId_Int', (intToken(ty),)), + KApply('noBody_BODY_MaybeBody', ()), + ), + ) elif isinstance(sym.get('NormalSym'), str): functions[ty] = KApply( 'MonoItemKind::MonoItemFn', diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 1ce7b897b..0544fe9e6 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -7,7 +7,7 @@ from typing import TYPE_CHECKING, NewType from .alloc import AllocInfo -from .ty import EnumT, RefT, StructT, Ty, TypeMetadata, UnionT +from .ty import ArrayT, EnumT, PtrT, RefT, StructT, TupleT, Ty, TypeMetadata, UnionT if TYPE_CHECKING: from collections.abc import Sequence @@ -19,6 +19,7 @@ _LOGGER: Final = logging.getLogger(__name__) _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' +_DROP_IN_PLACE_PREFIXES: Final = ('std::ptr::drop_in_place::<', 'core::ptr::drop_in_place::<') AdtDef = NewType('AdtDef', int) @@ -173,6 +174,37 @@ def function_tys(self) -> dict[str, int]: res[name] = fun_syms[sym][0] return res + @cached_property + def drop_function_tys(self) -> dict[Ty, Ty]: + res: dict[Ty, Ty] = {} + + for sym, item in self.items.items(): + if sym not in self.function_symbols_reverse: + continue + + mono_item = item['mono_item_kind'].get('MonoItemFn') + if mono_item is None: + continue + + if not mono_item['name'].startswith(_DROP_IN_PLACE_PREFIXES): + continue + + body = mono_item.get('body') + if body is None or body['arg_count'] < 1: + continue + + arg_ty = Ty(body['locals'][1]['ty']) + arg_type = self.types.get(arg_ty) + if not isinstance(arg_type, (PtrT, RefT)): + _LOGGER.debug(f'Skipping drop glue {sym}: unexpected argument type {arg_type}') + continue + + pointee_ty = Ty(arg_type.pointee_type) + fn_ty = Ty(self.function_symbols_reverse[sym][0]) + res[pointee_ty] = fn_ty + + return res + @cached_property def spans(self) -> dict[int, tuple[Path, int, int, int, int]]: return {id: (p, sr, sc, er, ec) for id, [p, sr, sc, er, ec] in self._smir['spans']} @@ -232,29 +264,107 @@ def call_edges(self) -> dict[Ty, set[Ty]]: else: called_tys = set() for block in body['blocks']: - if 'Call' not in block['terminator']['kind']: - continue - call = block['terminator']['kind']['Call'] - - # 1. Direct call: the function being called - func = call['func'] - if 'Constant' in func: - called_tys.add(Ty(func['Constant']['const_']['ty'])) - - # 2. Indirect call: function pointers passed as arguments - # These are ZeroSized constants whose ty is in the function table - for arg in call.get('args', []): - if 'Constant' in arg: - const_ = arg['Constant'].get('const_', {}) - if const_.get('kind') == 'ZeroSized': - ty = const_.get('ty') - if isinstance(ty, int) and ty in function_tys: - called_tys.add(Ty(ty)) + terminator = block['terminator']['kind'] + + if 'Call' in terminator: + call = terminator['Call'] + + # 1. Direct call: the function being called + func = call['func'] + if 'Constant' in func: + called_tys.add(Ty(func['Constant']['const_']['ty'])) + + # 2. Indirect call: function pointers passed as arguments + # These are ZeroSized constants whose ty is in the function table + for arg in call.get('args', []): + if 'Constant' in arg: + const_ = arg['Constant'].get('const_', {}) + if const_.get('kind') == 'ZeroSized': + ty = const_.get('ty') + if isinstance(ty, int) and ty in function_tys: + called_tys.add(Ty(ty)) + + if 'Drop' in terminator: + drop = terminator['Drop'] + drop_ty = self._place_ty(body, drop['place']) + if drop_ty is None: + continue + drop_fn_ty = self.drop_function_tys.get(drop_ty) + if drop_fn_ty is not None: + called_tys.add(drop_fn_ty) for ty in self.function_symbols_reverse[sym]: result[Ty(ty)] = called_tys return result + def _place_ty(self, body: dict, place: dict) -> Ty | None: + local = place.get('local') + if not isinstance(local, int): + return None + locals_ = body.get('locals', []) + if not (0 <= local < len(locals_)): + return None + + current_ty: Ty | None = Ty(locals_[local]['ty']) + for projection in place.get('projection', []): + assert current_ty is not None + current_ty = self._projected_ty(current_ty, projection) + if current_ty is None: + return None + + return current_ty + + def _projected_ty(self, ty: Ty, projection: object) -> Ty | None: + type_info = self.types.get(ty) + if type_info is None: + return None + + if projection == 'Deref': + if isinstance(type_info, (PtrT, RefT)): + return Ty(type_info.pointee_type) + return None + + if not isinstance(projection, dict): + return None + + if 'Field' in projection: + index, field_ty = projection['Field'] + if isinstance(field_ty, int): + return Ty(field_ty) + + if isinstance(type_info, (StructT, UnionT)): + fields = type_info.fields + elif isinstance(type_info, TupleT): + fields = type_info.components + elif isinstance(type_info, EnumT): + # Field projection into enums is only well-defined after a downcast. + return None + else: + return None + + if 0 <= index < len(fields): + return Ty(fields[index]) + return None + + if 'Index' in projection and isinstance(type_info, ArrayT): + return Ty(type_info.element_type) + + if 'ConstantIndex' in projection and isinstance(type_info, ArrayT): + return Ty(type_info.element_type) + + if 'Subslice' in projection and isinstance(type_info, ArrayT): + return ty + + if 'OpaqueCast' in projection or 'Subtype' in projection: + key = 'OpaqueCast' if 'OpaqueCast' in projection else 'Subtype' + cast_ty = projection[key] + return Ty(cast_ty) if isinstance(cast_ty, int) else None + + if 'Downcast' in projection: + return ty + + return None + def compute_closure(start_nodes: Sequence[Ty], edges: dict[Ty, set[Ty]]) -> set[Ty]: work = deque(start_nodes) diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected index 544958705..60dbf8403 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (737 steps) +│ (740 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected index bd3076868..bdade977c 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (216 steps) +│ (217 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ 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 a1a21b0dc..738dc56da 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 ( 109 ) ) ) ) , 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 + #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 ( 109 ) ) ) ) , projectionElemDeref projectionElemDowncast ( variantIdx ( 0 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 37 ) ) .ProjectionElems , .Contexts , .ProjectionElems ) ~> #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/intrinsic/blackbox_functions.expected.json b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_functions.expected.json index 029619a88..9611bf166 100644 --- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_functions.expected.json +++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_functions.expected.json @@ -33998,5 +33998,68 @@ }, "node": "KApply", "variable": false + }, + "48": { + "args": [ + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "String", + "node": "KSort" + }, + "token": "\"\"" + } + ], + "arity": 1, + "label": { + "name": "symbol(_)_LIB_Symbol_String", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "Int", + "node": "KSort" + }, + "token": "48" + } + ], + "arity": 1, + "label": { + "name": "defId(_)_BODY_DefId_Int", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [], + "arity": 0, + "label": { + "name": "noBody_BODY_MaybeBody", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + } + ], + "arity": 3, + "label": { + "name": "MonoItemKind::MonoItemFn", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false } } \ No newline at end of file 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 133db0c7a..a37f5c9c5 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 @@ -3,7 +3,7 @@ #traverseProjection ( toLocal ( 5 ) , Range ( ListItem ( Integer ( 42 , 8 , false ) ) ListItem ( Integer ( 42 , 8 , false ) ) ListItem ( Integer ( 42 , 8 , false ) ) - ListItem ( Integer ( 42 , 8 , false ) ) ) , .ProjectionElems , .Contexts ) ~> #derefTruncate ( staticSize ( 9 ) , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 23 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 28 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ) , span: span ( 97 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 27 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPointerCoercion ( pointerCoercionUnsize ) , operandMove ( place (... local: local ( 28 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 97 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 26 ) , projection: .ProjectionElems ) , rvalue: rvalueUnaryOp ( unOpPtrMetadata , operandMove ( place (... local: local ( 27 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 98 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindSwitchInt (... discr: operandMove ( place (... local: local ( 26 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 9 , basicBlockIdx ( 11 ) ) .Branches , otherwise: basicBlockIdx ( 12 ) ) ) , span: span ( 94 ) ) ) ~> .K + ListItem ( Integer ( 42 , 8 , false ) ) ) , .ProjectionElems , .Contexts , .ProjectionElems ) ~> #derefTruncate ( staticSize ( 9 ) , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 23 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 28 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ) , span: span ( 97 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 27 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPointerCoercion ( pointerCoercionUnsize ) , operandMove ( place (... local: local ( 28 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 97 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 26 ) , projection: .ProjectionElems ) , rvalue: rvalueUnaryOp ( unOpPtrMetadata , operandMove ( place (... local: local ( 27 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 98 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindSwitchInt (... discr: operandMove ( place (... local: local ( 26 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 9 , basicBlockIdx ( 11 ) ) .Branches , otherwise: basicBlockIdx ( 12 ) ) ) , span: span ( 94 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut.rs similarity index 74% rename from kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut.rs index 4be7fe1e8..db549954b 100644 --- a/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs +++ b/kmir/src/tests/integration/data/prove-rs/interior-mut.rs @@ -20,12 +20,10 @@ impl Counter { fn main() { let counter = Counter::new(0); - // println!("Before: {}", counter.get()); - // We only have &counter, but can still mutate inside + // We only have &counter, but can still mutate inside. counter.increment(); counter.increment(); assert!(2 == counter.get()); - // println!("After: {}", counter.get()); } diff --git a/kmir/src/tests/integration/data/prove-rs/noop-drop-in-place-move.rs b/kmir/src/tests/integration/data/prove-rs/noop-drop-in-place-move.rs new file mode 100644 index 000000000..2d55e8d23 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/noop-drop-in-place-move.rs @@ -0,0 +1,13 @@ +struct Wrap(u8); + +impl Drop for Wrap { + fn drop(&mut self) { + // `drop_in_place::` is compiled as a `NoOpSym`, but moving its pointer + // argument must still invalidate the current frame's local. + unsafe { std::ptr::drop_in_place(&mut self.0) }; + } +} + +fn main() { + let _w = Wrap(1); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected deleted file mode 100644 index 4c165cf72..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (877 steps) -└─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core4cell22panic_already - span: 32 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected deleted file mode 100644 index f1cd9a4d1..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (798 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected deleted file mode 100644 index 586c10ed1..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (740 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected index c8bee9fef..099286793 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 207 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 207 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 244 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 183 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 144 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 71 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected index 50fb59617..e217ff39d 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 32 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 32 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 130 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 60 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 253 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 107 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected index 66dbadacc..35a93bd47 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 46 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 46 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 184 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 86 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 108 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected index d408600a9..fa7459f20 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 66 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 66 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 242 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 33 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 132 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 119 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected index 2b6e8720c..1088d7a69 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 155 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 155 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 52 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 202 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 245 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 34 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 10 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected index 73d82794e..39bece296 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 238 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 238 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 127 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 26 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 80 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected index 3a3a93c89..24ea67198 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 18 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 18 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 0 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 74 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 11 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 139 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected index 056a32057..e2ffb4bca 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 189 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 189 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 192 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 64 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 98 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 70 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected index 92a082106..09b147859 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 95 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 95 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 3 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 173 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 237 , 8 , false ) ) ) ) ) @@ -16,7 +16,7 @@ ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 20 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) ) ) ) ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) ) - ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K + ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) ) .Contexts , projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false ) projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) ) PointerOffset ( 1 , 1 ) .ProjectionElems ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 14b5221c3..fa9c05e49 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -43,7 +43,6 @@ } PROVE_SHOW_SPECS = [ 'local-raw-fail', - 'interior-mut-fail', 'interior-mut3-fail', 'iter_next_3', 'assert_eq_exp', @@ -53,12 +52,10 @@ 'checked_arithmetic-fail', 'offset-u8-fail', 'pointer-cast-length-test-fail', - 'niche-enum', 'assume-cheatcode-conflict-fail', 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', 'assert-inhabited-fail', - 'iterator-simple', 'unions-fail', 'transmute-maybe-uninit-fail', 'ptr-through-wrapper-fail', diff --git a/kmir/src/tests/unit/test_kompile.py b/kmir/src/tests/unit/test_kompile.py index de8366cba..1630a6d99 100644 --- a/kmir/src/tests/unit/test_kompile.py +++ b/kmir/src/tests/unit/test_kompile.py @@ -1,10 +1,15 @@ from __future__ import annotations from typing import TYPE_CHECKING, Any, cast +from unittest.mock import Mock +from pyk.kast.inner import KApply +from pyk.kast.prelude.kint import intToken +from pyk.kast.prelude.string import stringToken from pyk.kore.syntax import And, App, Axiom, EVar, Rewrites, SortApp, Top -from kmir.kompile import _add_exists_quantifiers, _collect_evars, _load_extra_module_rules +from kmir.kompile import _add_exists_quantifiers, _collect_evars, _functions, _load_extra_module_rules +from kmir.smir import SMIRInfo if TYPE_CHECKING: from pathlib import Path @@ -110,3 +115,31 @@ def which(target: str) -> Path: assert captured['file_path'] == module_path assert captured['module_name'] == 'TEST' assert captured['include_dirs'] == ((tmp_path / 'custom-haskell-target'),) + + +def test_functions_preserve_noop_symbols() -> None: + smir_info = SMIRInfo( + { + 'name': 'noop-sym', + 'allocs': [], + 'functions': [[42, {'NoOpSym': ''}]], + 'uneval_consts': [], + 'items': [], + 'types': [], + 'spans': [], + 'debug': None, + 'machine': {}, + } + ) + + kmir = Mock() + kmir.parser = Mock() + + assert _functions(kmir, smir_info)[42] == KApply( + 'MonoItemKind::MonoItemFn', + ( + KApply('symbol(_)_LIB_Symbol_String', (stringToken(''),)), + KApply('defId(_)_BODY_DefId_Int', (intToken(42),)), + KApply('noBody_BODY_MaybeBody', ()), + ), + ) diff --git a/kmir/src/tests/unit/test_smir.py b/kmir/src/tests/unit/test_smir.py index 9be42f87c..32cbf8358 100644 --- a/kmir/src/tests/unit/test_smir.py +++ b/kmir/src/tests/unit/test_smir.py @@ -45,3 +45,216 @@ def test_function_symbols_reverse(smir_file: Path, update_expected_output: bool) def test_function_tys(smir_file: Path, update_expected_output: bool) -> None: """Test function_tys using actual SMIR JSON data.""" _test_smir_property(smir_file, 'function_tys', update_expected_output) + + +def test_call_edges_preserve_drop_glue_for_downcast_field() -> None: + # This SMIR models: + # local 1: Wrapper + # Drop(local 1 . Downcast(0) . Field(0, Inner)) + # so `call_edges` must keep the reachable `std::ptr::drop_in_place::` callee. + smir_info = SMIRInfo( + { + 'name': 'drop-downcast-field', + 'allocs': [], + 'types': [ + [ + 1, + { + 'EnumType': { + 'name': 'Wrapper', + 'adt_def': 1, + 'discriminants': [0], + 'fields': [[2]], + 'layout': None, + } + }, + ], + [ + 2, + { + 'StructType': { + 'name': 'Inner', + 'adt_def': 2, + 'fields': [], + 'layout': None, + } + }, + ], + [3, {'PtrType': {'pointee_type': 2}}], + ], + 'functions': [ + [10, {'NormalSym': 'caller'}], + [12, {'NormalSym': 'drop_inner'}], + ], + 'items': [ + { + 'symbol_name': 'caller', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'caller', + 'body': { + 'arg_count': 0, + 'locals': [{'ty': 0}, {'ty': 1}], + 'blocks': [ + { + 'terminator': { + 'kind': { + 'Drop': { + 'place': { + 'local': 1, + 'projection': [{'Downcast': 0}, {'Field': [0, 2]}], + }, + 'target': 0, + 'unwind': 'Continue', + } + } + } + } + ], + }, + } + }, + }, + { + 'symbol_name': 'drop_inner', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'std::ptr::drop_in_place::', + 'body': { + 'arg_count': 1, + 'locals': [{'ty': 0}, {'ty': 3}], + 'blocks': [], + }, + } + }, + }, + ], + 'spans': [], + } + ) + + assert smir_info.call_edges == {10: {12}, 12: set()} + + +def test_call_edges_preserve_drop_glue_for_index_projection() -> None: + # This SMIR models: + # local 1: [Inner; 2] + # local 2: usize + # Drop(local 1 . Index(local 2)) + # so `call_edges` must keep the reachable `std::ptr::drop_in_place::` callee. + smir_info = SMIRInfo( + { + 'name': 'drop-index-field', + 'allocs': [], + 'types': [ + [1, {'ArrayType': {'elem_type': 2, 'size': None}}], + [ + 2, + { + 'StructType': { + 'name': 'Inner', + 'adt_def': 2, + 'fields': [], + 'layout': None, + } + }, + ], + [3, {'PrimitiveType': {'Uint': 'Usize'}}], + [4, {'PtrType': {'pointee_type': 2}}], + ], + 'functions': [ + [10, {'NormalSym': 'caller'}], + [12, {'NormalSym': 'drop_inner'}], + ], + 'items': [ + { + 'symbol_name': 'caller', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'caller', + 'body': { + 'arg_count': 0, + 'locals': [{'ty': 0}, {'ty': 1}, {'ty': 3}], + 'blocks': [ + { + 'terminator': { + 'kind': { + 'Drop': { + 'place': { + 'local': 1, + 'projection': [{'Index': 2}], + }, + 'target': 0, + 'unwind': 'Continue', + } + } + } + } + ], + }, + } + }, + }, + { + 'symbol_name': 'drop_inner', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'std::ptr::drop_in_place::', + 'body': { + 'arg_count': 1, + 'locals': [{'ty': 0}, {'ty': 4}], + 'blocks': [], + }, + } + }, + }, + ], + 'spans': [], + } + ) + + assert smir_info.call_edges == {10: {12}, 12: set()} + + +def test_drop_function_tys_accept_core_drop_in_place_names() -> None: + smir_info = SMIRInfo( + { + 'name': 'core-drop-glue', + 'allocs': [], + 'types': [ + [ + 2, + { + 'StructType': { + 'name': 'Inner', + 'adt_def': 2, + 'fields': [], + 'layout': None, + } + }, + ], + [3, {'PtrType': {'pointee_type': 2}}], + ], + 'functions': [ + [12, {'NormalSym': 'drop_inner'}], + ], + 'items': [ + { + 'symbol_name': 'drop_inner', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'core::ptr::drop_in_place::', + 'body': { + 'arg_count': 1, + 'locals': [{'ty': 0}, {'ty': 3}], + 'blocks': [], + }, + } + }, + }, + ], + 'spans': [], + } + ) + + assert smir_info.drop_function_tys == {2: 12}