Execute drop glue for Drop terminators

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

@@ -219,6 +219,20 @@ 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
+  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 +363,17 @@ 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]
+
+  // 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.
+  rule [termCallNoOp]:
+       <k> #execTerminatorCall(_, monoItemFn(symbol(""), _, noBody), _ARGS, _DEST, TARGET, _UNWIND, _SPAN) ~> _
+        => #continueAt(TARGET)
+       </k>
+
   // Regular function call - full state switching and stack setup
   rule [termCallFunction]:
        <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _
@@ -365,6 +390,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 +409,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]
@@ -474,6 +501,8 @@ An operand may be a `Reference` (the only way a function could access another fu
       =>
        ListItem(newLocal(TY, MUT)) #reserveFor(REST)
 
+  syntax Operand ::= operandValue ( Value )
+
   syntax KItem ::= #setArgsFromStack ( Int, Operands)
                  | #setArgFromStack ( Int, Operand)
                  | #execIntrinsic ( MonoItemKind, Operands, Place, Span )
@@ -493,6 +522,12 @@ An operand may be a `Reference` (the only way a function could access another fu
         ...
        </k>
 
+  rule <k> #setArgFromStack(IDX, operandValue(VAL))
+        =>
+           #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL))
+        ...
+       </k>
+
   rule <k> #setArgFromStack(IDX, operandCopy(place(local(I), .ProjectionElems)))
         =>
            #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I)))
@@ -669,12 +704,52 @@ 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 [termDropGlue]: <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 <k> PTR:Value ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN)
+         =>
+           #execTerminatorCall(
+             FTY,
+             lookupFunction(FTY),
+             operandValue(PTR) .Operands,
+             place(local(-1), .ProjectionElems),
+             someBasicBlockIdx(TARGET),
+             UNWIND,
+             SPAN
+           )
+        ...
+       </k>
+
   syntax MIRError ::= "ReachedUnreachable"
 
   rule [termUnreachable]: <k> #execTerminator(terminator(terminatorKindUnreachable, _SPAN))

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

@@ -517,6 +517,15 @@ 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)]
+
+  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
@@ -658,6 +667,23 @@ 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 <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

@@ -183,6 +183,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

@@ -487,6 +487,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'),)),)
     )
@@ -501,7 +515,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]:
@@ -531,6 +545,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',