fix(kompile): map linked NormalSym functions to monoItemFn(noBody) (#953)

## Summary

- Generate `MonoItemKind::MonoItemFn(symbol(...), defId(...), noBody)`
for linked `NormalSym` entries that are present in `function_symbols`
but missing from `items`.
- Keep function resolution on concrete linked symbols instead of falling
back to `"** UNKNOWN FUNCTION **"` for bodyless linked functions.
- Refresh affected integration/show fixtures and normalize panic symbol
hash suffixes in fixture comparison to keep snapshot output stable.
- Preserve readable `kmir show --statistics --leaves` annotations for
`noBody` callees (`>> function`, `>> call span`, `>> message`) even
after replacing `"** UNKNOWN FUNCTION **"` with concrete symbols.

## Context

In multi-crate SMIR, linked external functions can exist in
`function_symbols` but not in local `items` (no local body). Before this
change, that gap could leave `lookupFunction(Ty)` without a generated
`monoItemFn` equation.

### Red vs Green

**RED (actual stuck shape in show fixtures):**
```k
#setUpCalleeData(
  monoItemFn(... name: symbol("** UNKNOWN FUNCTION **"), id: defId(38), body: noBody),
  ...
)
```
This is the unresolved-function path.

**GREEN (after fix):**
```k
#setUpCalleeData(
  monoItemFn(... name: symbol("_ZN4core9panicking5panic17h<hash>E"), id: defId(38), body: noBody),
  ...
)
```
The same path now resolves to a concrete linked symbol instead of `"**
UNKNOWN FUNCTION **"`.

---------

Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>

Author: Stevengre

kmir/src/kmir/kompile.py

@@ -521,13 +521,25 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]:
         for ty in smir_info.function_symbols_reverse[item_name]:
             functions[ty] = parsed_item_kinner.args[1]
 
-    # Add intrinsic functions
+    # Add intrinsic functions and linked normal symbols that have no local body in `items`.
+    # Normal symbols must still map to `monoItemFn(..., noBody)` instead of falling back to UNKNOWN FUNCTION.
     for ty, sym in smir_info.function_symbols.items():
-        if 'IntrinsicSym' in sym and ty not in functions:
+        if ty in functions:
+            continue
+        if 'IntrinsicSym' in sym:
             functions[ty] = KApply(
                 'IntrinsicFunction',
                 [KApply('symbol(_)_LIB_Symbol_String', [stringToken(sym['IntrinsicSym'])])],
             )
+        elif isinstance(sym.get('NormalSym'), str):
+            functions[ty] = KApply(
+                'MonoItemKind::MonoItemFn',
+                (
+                    KApply('symbol(_)_LIB_Symbol_String', (stringToken(sym['NormalSym']),)),
+                    KApply('defId(_)_BODY_DefId_Int', (intToken(ty),)),
+                    KApply('noBody_BODY_MaybeBody', ()),
+                ),
+            )
 
     return functions
 

kmir/src/kmir/testing/fixtures.py

@@ -1,5 +1,7 @@
 from __future__ import annotations
 
+import re
+import sys
 from difflib import unified_diff
 from typing import TYPE_CHECKING
 
@@ -13,24 +15,36 @@
 
     from pytest import FixtureRequest, Parser
 
-import sys
-
 
 def pytest_configure(config) -> None:
     sys.setrecursionlimit(1000000)
 
 
+def _normalize_symbol_hashes(text: str) -> str:
+    """Normalize rustc symbol hash suffixes that drift across builds/environments."""
+    # Normalize mangled symbol hashes, including generic names with `$` and `.`.
+    # Keep trailing `E` when present; truncated variants may omit it.
+    text = re.sub(r'(_ZN[0-9A-Za-z_$.]+17h)[0-9a-fA-F]+E', r'\1<hash>E', text)
+    text = re.sub(r'(_ZN[0-9A-Za-z_$.]+17h)[0-9a-fA-F]+', r'\1<hash>', text)
+    # Normalize demangled hash suffixes (`...::h<hex>`).
+    text = re.sub(r'(::h)[0-9a-fA-F]{8,}', r'\1<hash>', text)
+    return text
+
+
 def assert_or_update_show_output(
     actual_text: str, expected_file: Path, *, update: bool, path_replacements: dict[str, str] | None = None
 ) -> None:
     if path_replacements:
         for old, new in path_replacements.items():
             actual_text = actual_text.replace(old, new)
+    # Normalize rustc symbol hash suffixes that can drift across builds/environments.
+    actual_text = _normalize_symbol_hashes(actual_text)
     if update:
         expected_file.write_text(actual_text)
     else:
         assert expected_file.is_file()
         expected_text = expected_file.read_text()
+        expected_text = _normalize_symbol_hashes(expected_text)
         if actual_text != expected_text:
             diff = '\n'.join(
                 unified_diff(

kmir/src/kmir/utils.py

@@ -288,8 +288,8 @@ def _extract_alloc_id(operands: KInner) -> int | None:
             return None
 
 
-def _annotate_unknown_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]:
-    """If the k cell is `#setUpCalleeData` for `** UNKNOWN FUNCTION **`, return annotation lines with decoded info."""
+def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]:
+    """If the k cell is `#setUpCalleeData` for a `noBody` callee, return annotation lines with decoded info."""
 
     from .alloc import Allocation, AllocId, AllocInfo, Memory
     from .linker import _demangle
@@ -307,16 +307,14 @@ def _annotate_unknown_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]
                     KApply(
                         label=KLabel(name='MonoItemKind::MonoItemFn'),
                         args=[
-                            KApply(args=[KToken(token=symbol_name)]),
+                            KApply(args=[KToken()]),
                             KApply(label=KLabel(name='defId(_)_BODY_DefId_Int'), args=[KToken(token=def_id_str)]),
                             _,
                         ],
                     ),
                     operands,
                     KApply(label=KLabel(name='span'), args=[KToken(token=span_str)]),
-                ] if (
-                    symbol_name == '\"** UNKNOWN FUNCTION **\"'
-                ):
+                ]:
                     def_id = int(def_id_str)
                     span = int(span_str)
                 case _:
@@ -379,7 +377,7 @@ def render_leaf_k_cells(proof: APRProof, cterm_show: CTermShow, smir_info: SMIRI
             lines.extend(f'  {k_line}' for k_line in k_lines)
 
         if smir_info is not None and k_cell is not None:
-            annotations = _annotate_unknown_function(k_cell, smir_info)
+            annotations = _annotate_nobody_function(k_cell, smir_info)
             lines.extend(annotations)
 
         if idx != len(leaves) - 1:

kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected

@@ -16,7 +16,7 @@
 ┃  │
 ┃  │  (6 steps)
 ┃  └─ 6 (stuck, leaf)
-┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN3std7process4exit17h<hash>
 ┃
 ┗━━┓ subst: .Subst
    ┃ constraint:

kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json

@@ -1,69 +1,69 @@
 {
   "-6": {
-    "NormalSym": "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17hb524060ed0e83bbbE"
+    "NormalSym": "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h<hash>E"
   },
   "-5": {
-    "NormalSym": "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hb92e31f0aaa3d322E"
+    "NormalSym": "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17h<hash>E"
   },
   "-4": {
-    "NormalSym": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h526a5c5d4d9d3202E"
+    "NormalSym": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h<hash>E"
   },
   "-3": {
-    "NormalSym": "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h3a8781eea2f9ddb7E"
+    "NormalSym": "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h<hash>E"
   },
   "-2": {
-    "NormalSym": "_ZN3std2rt10lang_start17h17250425291430deE"
+    "NormalSym": "_ZN3std2rt10lang_start17h<hash>E"
   },
   "-1": {
-    "NormalSym": "_ZN8blackbox4main17h56268fefa1135d9eE"
+    "NormalSym": "_ZN8blackbox4main17h<hash>E"
   },
   "0": {
-    "NormalSym": "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E"
+    "NormalSym": "_ZN3std2rt19lang_start_internal17h<hash>E"
   },
   "13": {
-    "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h3ac302c9481e885fE"
+    "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h<hash>E"
   },
   "14": {
-    "NormalSym": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h8eaae5c69aab66e9E"
+    "NormalSym": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h<hash>E"
   },
   "19": {
-    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17haae505bd39892fd2E"
+    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h<hash>E"
   },
   "20": {
     "IntrinsicSym": "black_box"
   },
   "21": {
-    "NormalSym": "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h99c61f0bde9a2afdE"
+    "NormalSym": "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "27": {
-    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8E"
+    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "28": {
-    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h7baa47f3e5cbe44cE"
+    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "29": {
-    "NormalSym": "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17hec74c53b91325b16E"
+    "NormalSym": "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "30": {
-    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h2d8e0aae13049ae8E"
+    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h<hash>E"
   },
   "32": {
-    "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h5c121846c1652782E"
+    "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h<hash>E"
   },
   "35": {
     "IntrinsicSym": "black_box"
   },
   "36": {
-    "NormalSym": "_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E"
+    "NormalSym": "_ZN4core9panicking19assert_failed_inner17h<hash>E"
   },
   "43": {
-    "NormalSym": "_ZN8blackbox7add_one17h19d5f3b41fdf13daE"
+    "NormalSym": "_ZN8blackbox7add_one17h<hash>E"
   },
   "44": {
-    "NormalSym": "_ZN4core4hint9black_box17h0bfc654765aa2ddfE"
+    "NormalSym": "_ZN4core4hint9black_box17h<hash>E"
   },
   "45": {
-    "NormalSym": "_ZN4core9panicking13assert_failed17h9acd0d94a91ca0eaE"
+    "NormalSym": "_ZN4core9panicking13assert_failed17h<hash>E"
   },
   "48": {
     "NoOpSym": ""

kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json

@@ -1,62 +1,62 @@
 {
-  "_ZN3std2rt10lang_start17h17250425291430deE": [
+  "_ZN3std2rt10lang_start17h<hash>E": [
     -2
   ],
-  "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h5c121846c1652782E": [
+  "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h<hash>E": [
     32
   ],
-  "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E": [
+  "_ZN3std2rt19lang_start_internal17h<hash>E": [
     0
   ],
-  "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h3ac302c9481e885fE": [
+  "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h<hash>E": [
     13
   ],
-  "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h3a8781eea2f9ddb7E": [
+  "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h<hash>E": [
     -3
   ],
-  "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17hec74c53b91325b16E": [
+  "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     29
   ],
-  "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h99c61f0bde9a2afdE": [
+  "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     21
   ],
-  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8E": [
+  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     27
   ],
-  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h7baa47f3e5cbe44cE": [
+  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     28
   ],
-  "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h526a5c5d4d9d3202E": [
+  "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h<hash>E": [
     -4
   ],
-  "_ZN4core3ops8function6FnOnce9call_once17h2d8e0aae13049ae8E": [
+  "_ZN4core3ops8function6FnOnce9call_once17h<hash>E": [
     30
   ],
-  "_ZN4core3ops8function6FnOnce9call_once17haae505bd39892fd2E": [
+  "_ZN4core3ops8function6FnOnce9call_once17h<hash>E": [
     19
   ],
-  "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hb92e31f0aaa3d322E": [
+  "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17h<hash>E": [
     -5
   ],
-  "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17hb524060ed0e83bbbE": [
+  "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h<hash>E": [
     -6
   ],
-  "_ZN4core4hint9black_box17h0bfc654765aa2ddfE": [
+  "_ZN4core4hint9black_box17h<hash>E": [
     44
   ],
-  "_ZN4core9panicking13assert_failed17h9acd0d94a91ca0eaE": [
+  "_ZN4core9panicking13assert_failed17h<hash>E": [
     45
   ],
-  "_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E": [
+  "_ZN4core9panicking19assert_failed_inner17h<hash>E": [
     36
   ],
-  "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h8eaae5c69aab66e9E": [
+  "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h<hash>E": [
     14
   ],
-  "_ZN8blackbox4main17h56268fefa1135d9eE": [
+  "_ZN8blackbox4main17h<hash>E": [
     -1
   ],
-  "_ZN8blackbox7add_one17h19d5f3b41fdf13daE": [
+  "_ZN8blackbox7add_one17h<hash>E": [
     43
   ],
   "black_box": [