fix(kmir): handle noop drop-glue calls

Author: Stevengre

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

@@ -363,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) ~> _
@@ -379,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
@@ -397,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]

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

@@ -508,6 +508,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
@@ -649,6 +658,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/kompile.py

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

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
   }
 }

kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (798 steps)
+│  (1113 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

kmir/src/tests/unit/test_kompile.py

@@ -1,8 +1,14 @@
 from __future__ import annotations
 
+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
+from kmir.kompile import _add_exists_quantifiers, _collect_evars, _functions
+from kmir.smir import SMIRInfo
 
 
 def test_collect_evars() -> None:
@@ -37,3 +43,31 @@ def test_add_exists_quantifiers() -> None:
     assert result.text.count(r'\exists') == 2
     assert 'VarA' in result.text
     assert 'VarB' in result.text
+
+
+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', ()),
+        ),
+    )