Execute drop glue for Drop terminators

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

@@ -219,6 +219,25 @@ 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 indicating the
+  // callee is not expected to return a value (e.g. `main`, top-level framework calls,
+  // or `drop_in_place` functions). 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]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
+         =>
+           #execBlockIdx(TARGET)
+       </k>
+       <currentFunc> _ => CALLER </currentFunc>
+       <currentBody> _ => #getBlocks(CALLER) </currentBody>
+       <caller> CALLER => NEWCALLER </caller>
+       <dest> place(local(-1), .ProjectionElems) => NEWDEST </dest>
+       <target> someBasicBlockIdx(TARGET) => NEWTARGET </target>
+       <unwind> _ => UNWIND </unwind>
+       <locals> _ => NEWLOCALS </locals>
+       <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
+    [priority(40)]
+
   rule [termReturnSome]: <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
          =>
            #setLocalValue(DEST, #decrementRef(VAL)) ~> #execBlockIdx(TARGET)
@@ -349,6 +368,44 @@ 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]:
+       <k> #execTerminatorCall(_, monoItemFn(symbol(""), _, noBody), ARGS, _DEST, TARGET, _UNWIND, _SPAN) ~> _
+        => #consumeNoOpArgs(ARGS, TARGET)
+       </k>
+
+  rule <k> #consumeNoOpArgs(.Operands, TARGET) => #continueAt(TARGET) ... </k>
+
+  rule <k> #consumeNoOpArgs(OP:Operand MORE:Operands, TARGET)
+        => #consumeNoOpArg(OP) ~> #consumeNoOpArgs(MORE, TARGET)
+        ...
+       </k>
+
+  rule <k> #consumeNoOpArg(operandConstant(_)) => .K ... </k>
+
+  rule <k> #consumeNoOpArg(operandCopy(place(local(I), .ProjectionElems))) => .K ... </k>
+       <locals> LOCALS </locals>
+    requires 0 <=Int I
+     andBool I <Int size(LOCALS)
+     andBool isTypedValue(LOCALS[I])
+    [preserves-definedness]
+
+  rule <k> #consumeNoOpArg(operandMove(place(local(I), _))) => .K ... </k>
+       <locals> LOCALS => LOCALS[I <- typedValue(Moved, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)] </locals>
+    requires 0 <=Int I
+     andBool I <Int size(LOCALS)
+     andBool isTypedValue(LOCALS[I])
+    [preserves-definedness]
+
   // Regular function call - full state switching and stack setup
   rule [termCallFunction]:
        <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _
@@ -365,6 +422,7 @@ where the returned result should go.
        </currentFrame>
        <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </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 +441,7 @@ where the returned result should go.
        </currentFrame>
        <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
     requires notBool isIntrinsicFunction(FUNC)
+     andBool notBool isNoOpFunction(FUNC)
      andBool #functionNameMatchesEnv(getFunctionName(FUNC))
 
   syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function]
@@ -442,6 +501,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]: <k> #setUpCalleeData(
@@ -466,6 +526,21 @@ An operand may be a `Reference` (the only way a function could access another fu
        </currentFrame>
   // TODO: Haven't handled "noBody" case
 
+  rule [setupDropGlueData]: <k> #setUpDropGlueData(
+              monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
+              PTR,
+              _SPAN
+              )
+         =>
+           #setLocalValue(place(local(1), .ProjectionElems), #incrementRef(PTR)) ~> #execBlock(FIRST)
+         ...
+       </k>
+       <currentFrame>
+         <currentBody> _ => toKList(BLOCKS) </currentBody>
+         <locals> _ => #reserveFor(NEWLOCALS) </locals>
+         ...
+       </currentFrame>
+
   syntax List ::= #reserveFor( LocalDecls ) [function, total]
 
   rule #reserveFor(.LocalDecls) => .List
@@ -669,12 +744,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]: <k> #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 <Int size(LOCALS)
+     andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness]
+
+  rule #dropPlaceTy(_, _) => TyUnknown [owise]
+
+  syntax KItem ::= #execDropCall ( MaybeTy, Place, BasicBlockIdx, UnwindAction, Span )
+                 | #callDropGlue ( Ty, BasicBlockIdx, UnwindAction, Span )
+
+  rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(PLACE, TARGET, UNWIND), SPAN))
+         =>
+           #execDropCall(#lookupDropFunctionTy(#dropPlaceTy(PLACE, LOCALS)), PLACE, TARGET, UNWIND, SPAN)
+        ...
+       </k>
+       <locals> LOCALS </locals>
+
+  rule <k> #execDropCall(TyUnknown, _PLACE, TARGET, _UNWIND, _SPAN)
          =>
            #execBlockIdx(TARGET)
         ...
        </k>
 
+  rule <k> #execDropCall(FTY:Ty, PLACE, TARGET, UNWIND, SPAN)
+         =>
+           rvalueAddressOf(mutabilityMut, PLACE) ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN)
+        ...
+       </k>
+
+  rule [termCallDropGlue]:
+       <k> PTR:Value ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN) ~> _
+        => #setUpDropGlueData(lookupFunction(FTY), PTR, SPAN)
+       </k>
+       <currentFunc> CALLER => FTY </currentFunc>
+       <currentFrame>
+         <currentBody> _ </currentBody>
+         <caller> OLDCALLER => CALLER </caller>
+         <dest> OLDDEST => place(local(-1), .ProjectionElems) </dest>
+         <target> OLDTARGET => someBasicBlockIdx(TARGET) </target>
+         <unwind> OLDUNWIND => UNWIND </unwind>
+         <locals> LOCALS </locals>
+       </currentFrame>
+       <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
+
   syntax MIRError ::= "ReachedUnreachable"
 
   rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, _SPAN))

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

@@ -508,6 +508,17 @@ The following rule resolves this situation by using the head element.
            )
         => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... </k> // TODO mark context?
     [preserves-definedness, priority(100)]
+
+  // Temporary bridge rule: after PointerOffset lifts a single value to Range(ListItem(...)),
+  // unwrap a Union head element so the existing Union + Field rules below can keep running.
+  rule <k> #traverseProjection(
+             DEST,
+             Range(ListItem(Union(_, _) #as VALUE) _REST:List),
+             projectionElemField(IDX, TY) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... </k> // TODO mark context?
+    [preserves-definedness, priority(100)]
 ```
 
 #### Unions
@@ -649,6 +660,25 @@ 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
 
+  // Temporary bridge rule: PointerOffset is implemented below in terms of Range slicing, so
+  // lift a single non-Range value to Range(ListItem(...)) to reuse that shared path.
+  rule <k> #traverseProjection(
+             DEST,
+             VAL,
+             PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS,
+             CTXTS
+           )
+        => #traverseProjection(
+             DEST,
+             Range(ListItem(VAL)),
+             PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS,
+             CTXTS
+           )
+        ...
+        </k>
+    requires notBool isRange(VAL)
+    [preserves-definedness, priority(100)]
+
   rule <k> #traverseProjection(
              DEST,
              Range(ELEMENTS),

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

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',