From 4ea60386047f072c584a9d1145a8e4c61d3a3b91 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sat, 28 Feb 2026 10:13:06 +0800 Subject: [PATCH 01/14] fix(kompile): map linked NormalSym functions to monoItemFn(noBody) Linked NormalSym functions (external crate functions present in SMIR but without a local body) had no generated monoItemFn equation, falling back to "** UNKNOWN FUNCTION **". This synthesizes monoItemFn(symbol(...), defId(...), noBody) for all such symbols, ensuring downstream call resolution can find them. --- kmir/src/kmir/kompile.py | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 67878e05e..14ede6a90 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -529,6 +529,20 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: [KApply('symbol(_)_LIB_Symbol_String', [stringToken(sym['IntrinsicSym'])])], ) + # Add linked normal symbols that have no local body in `items`. + # They must still map to `monoItemFn(..., noBody)` instead of falling back to UNKNOWN FUNCTION. + for ty, sym in smir_info.function_symbols.items(): + normal_sym = sym.get('NormalSym') + if isinstance(normal_sym, str) and ty not in functions: + functions[ty] = KApply( + 'MonoItemKind::MonoItemFn', + ( + KApply('symbol(_)_LIB_Symbol_String', (stringToken(normal_sym),)), + KApply('defId(_)_BODY_DefId_Int', (intToken(ty),)), + KApply('noBody_BODY_MaybeBody', ()), + ), + ) + return functions From d4bf1baea92ba17aad367066bf507bf9b1da51e4 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sat, 28 Feb 2026 12:39:25 +0800 Subject: [PATCH 02/14] test(prove-rs): refresh UNKNOWN FUNCTION show fixtures --- ...ssume-cheatcode-conflict-fail.check_assume_conflict.expected | 2 +- .../data/prove-rs/show/interior-mut-fail.main.expected | 2 +- .../show/pointer-cast-length-test-fail.array_cast_test.expected | 2 +- .../data/prove-rs/show/symbolic-args-fail.main.expected | 2 +- .../show/symbolic-structs-fail.eats_struct_args.expected | 2 +- .../data/prove-rs/show/test_offset_from-fail.testing.expected | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected index 700446f6e..95f08c611 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected @@ -5,7 +5,7 @@ │ │ (61 steps) └─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 span: 32 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 index 44581b4f2..4c165cf72 100644 --- 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 @@ -5,7 +5,7 @@ │ │ (877 steps) └─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core4cell22panic_already span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected index 1a3c758c5..bc39714ca 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected @@ -17,7 +17,7 @@ ┃ │ ┃ │ (6 steps) ┃ └─ 6 (stuck, leaf) -┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , +┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 ┃ span: 32 ┃ ┗━━┓ subst: .Subst diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected index ef7740af7..affc081f9 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected @@ -5,7 +5,7 @@ │ │ (566 steps) └─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected index a3abc238d..cdddcdc6c 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected @@ -29,7 +29,7 @@ ┃ ┃ │ ┃ ┃ │ (6 steps) ┃ ┃ └─ 10 (stuck, leaf) -┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , +┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 ┃ ┃ span: 32 ┃ ┃ ┃ ┗━━┓ subst: .Subst diff --git a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected index a0ac24cae..30e9bc3af 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected @@ -114,7 +114,7 @@ ┃ │ ┃ │ (70 steps) ┃ └─ 22 (stuck, leaf) - ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , + ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 ┃ span: 32 ┃ ┗━━┓ subst: .Subst From 7966a3063fdca996e2731a1c98d5ae82f1c665a7 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sat, 28 Feb 2026 20:53:06 +0800 Subject: [PATCH 03/14] Normalize panic symbol hashes in show fixture assertions --- kmir/src/kmir/testing/fixtures.py | 11 +++++++++-- .../symbolic-args-fail.main.cli-stats-leaves.expected | 7 ++----- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/kmir/src/kmir/testing/fixtures.py b/kmir/src/kmir/testing/fixtures.py index 4ade1e06d..245484a92 100644 --- a/kmir/src/kmir/testing/fixtures.py +++ b/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,8 +15,6 @@ from pytest import FixtureRequest, Parser -import sys - def pytest_configure(config) -> None: sys.setrecursionlimit(1000000) @@ -26,11 +26,18 @@ def assert_or_update_show_output( if path_replacements: for old, new in path_replacements.items(): actual_text = actual_text.replace(old, new) + # Normalize rustc panic symbol hash suffixes that can drift across builds/environments. + actual_text = re.sub(r'_ZN4core9panicking5panic17h[0-9a-f]+E', '_ZN4core9panicking5panic17hE', actual_text) + actual_text = re.sub(r'core::panicking::panic::h[0-9a-f]+', 'core::panicking::panic::h', actual_text) if update: expected_file.write_text(actual_text) else: assert expected_file.is_file() expected_text = expected_file.read_text() + expected_text = re.sub( + r'_ZN4core9panicking5panic17h[0-9a-f]+E', '_ZN4core9panicking5panic17hE', expected_text + ) + expected_text = re.sub(r'core::panicking::panic::h[0-9a-f]+', 'core::panicking::panic::h', expected_text) if actual_text != expected_text: diff = '\n'.join( unified_diff( diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected index 84737597a..a705eda16 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected @@ -5,7 +5,7 @@ │ │ (566 steps) └─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 span: no-location:0 @@ -32,7 +32,4 @@ Leaf paths from init: LEAF CELLS --------------- Node 3: - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) ) .Operands , span ( 117 ) ) ~> .K - >> function: core::panicking::panic::h941160ead03e2d54 - >> call span: /kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs:53:5 - >> message: 'assertion failed: false' \ No newline at end of file + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17hE" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) ) .Operands , span ( 117 ) ) ~> .K \ No newline at end of file From 940499057bb059c01be14fceba1fffb7474e3038 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sat, 28 Feb 2026 22:52:46 +0800 Subject: [PATCH 04/14] test(fixtures): normalize truncated panic symbol hashes --- kmir/src/kmir/testing/fixtures.py | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/kmir/src/kmir/testing/fixtures.py b/kmir/src/kmir/testing/fixtures.py index 245484a92..002c5be71 100644 --- a/kmir/src/kmir/testing/fixtures.py +++ b/kmir/src/kmir/testing/fixtures.py @@ -23,21 +23,26 @@ def pytest_configure(config) -> None: def assert_or_update_show_output( actual_text: str, expected_file: Path, *, update: bool, path_replacements: dict[str, str] | None = None ) -> None: + def _normalize_panic_symbol_hashes(text: str) -> str: + # Full panic symbol in mangled form. + text = re.sub(r'_ZN4core9panicking5panic17h[0-9a-f]+E', '_ZN4core9panicking5panic17hE', text) + # Truncated panic symbol shown by `kmir show --statistics --leaves`. + text = re.sub(r'_ZN4core9panicking5panic17h[0-9a-f]+', '_ZN4core9panicking5panic17h', text) + # Demangled panic symbol. + text = re.sub(r'core::panicking::panic::h[0-9a-f]+', 'core::panicking::panic::h', text) + return text + if path_replacements: for old, new in path_replacements.items(): actual_text = actual_text.replace(old, new) # Normalize rustc panic symbol hash suffixes that can drift across builds/environments. - actual_text = re.sub(r'_ZN4core9panicking5panic17h[0-9a-f]+E', '_ZN4core9panicking5panic17hE', actual_text) - actual_text = re.sub(r'core::panicking::panic::h[0-9a-f]+', 'core::panicking::panic::h', actual_text) + actual_text = _normalize_panic_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 = re.sub( - r'_ZN4core9panicking5panic17h[0-9a-f]+E', '_ZN4core9panicking5panic17hE', expected_text - ) - expected_text = re.sub(r'core::panicking::panic::h[0-9a-f]+', 'core::panicking::panic::h', expected_text) + expected_text = _normalize_panic_symbol_hashes(expected_text) if actual_text != expected_text: diff = '\n'.join( unified_diff( From dbdb898206cd2c40b94ecb4432870ecabd5020f2 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sun, 1 Mar 2026 05:22:29 +0800 Subject: [PATCH 05/14] test(integration): refresh snapshots for NormalSym mapping --- ...t_lib::testing::test_add_in_range.expected | 2 +- .../blackbox_functions.expected.json | 315 ++++++++++++++++++ 2 files changed, 316 insertions(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected b/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected index 36e7fa6a7..6c64d5906 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected +++ b/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 ( "_ZN3std7process4exit17hf5473 ┃ ┗━━┓ subst: .Subst ┃ constraint: 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 8c767e34e..f306c611d 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 @@ -13569,6 +13569,69 @@ "node": "KApply", "variable": false }, + "0": { + "args": [ + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "String", + "node": "KSort" + }, + "token": "\"_ZN3std2rt19lang_start_internal17h018b8394ba015d86E\"" + } + ], + "arity": 1, + "label": { + "name": "symbol(_)_LIB_Symbol_String", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "Int", + "node": "KSort" + }, + "token": "0" + } + ], + "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 + }, "13": { "args": [ { @@ -22521,6 +22584,195 @@ "node": "KApply", "variable": false }, + "27": { + "args": [ + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "String", + "node": "KSort" + }, + "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8E\"" + } + ], + "arity": 1, + "label": { + "name": "symbol(_)_LIB_Symbol_String", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "Int", + "node": "KSort" + }, + "token": "27" + } + ], + "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 + }, + "28": { + "args": [ + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "String", + "node": "KSort" + }, + "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h7baa47f3e5cbe44cE\"" + } + ], + "arity": 1, + "label": { + "name": "symbol(_)_LIB_Symbol_String", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "Int", + "node": "KSort" + }, + "token": "28" + } + ], + "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 + }, + "29": { + "args": [ + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "String", + "node": "KSort" + }, + "token": "\"_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17hec74c53b91325b16E\"" + } + ], + "arity": 1, + "label": { + "name": "symbol(_)_LIB_Symbol_String", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "Int", + "node": "KSort" + }, + "token": "29" + } + ], + "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 + }, "30": { "args": [ { @@ -27986,6 +28238,69 @@ "node": "KApply", "variable": false }, + "36": { + "args": [ + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "String", + "node": "KSort" + }, + "token": "\"_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E\"" + } + ], + "arity": 1, + "label": { + "name": "symbol(_)_LIB_Symbol_String", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "Int", + "node": "KSort" + }, + "token": "36" + } + ], + "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 + }, "43": { "args": [ { From 6eee8e14239854d004b23298b2f12604e8f7112f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Sun, 1 Mar 2026 06:38:30 +0800 Subject: [PATCH 06/14] test(fixtures): normalize generic rust symbol hashes --- kmir/src/kmir/testing/fixtures.py | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/kmir/src/kmir/testing/fixtures.py b/kmir/src/kmir/testing/fixtures.py index 002c5be71..2a99ba443 100644 --- a/kmir/src/kmir/testing/fixtures.py +++ b/kmir/src/kmir/testing/fixtures.py @@ -23,26 +23,26 @@ def pytest_configure(config) -> None: def assert_or_update_show_output( actual_text: str, expected_file: Path, *, update: bool, path_replacements: dict[str, str] | None = None ) -> None: - def _normalize_panic_symbol_hashes(text: str) -> str: - # Full panic symbol in mangled form. - text = re.sub(r'_ZN4core9panicking5panic17h[0-9a-f]+E', '_ZN4core9panicking5panic17hE', text) - # Truncated panic symbol shown by `kmir show --statistics --leaves`. - text = re.sub(r'_ZN4core9panicking5panic17h[0-9a-f]+', '_ZN4core9panicking5panic17h', text) - # Demangled panic symbol. - text = re.sub(r'core::panicking::panic::h[0-9a-f]+', 'core::panicking::panic::h', text) + def _normalize_symbol_hashes(text: str) -> str: + # Mangled symbol hash suffixes can drift across rustc versions/builds. + text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+E', r'\1E', text) + # Some show outputs truncate mangled symbols before trailing `E`. + text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+', r'\1', text) + # Normalize demangled hash suffixes (`...::h`). + text = re.sub(r'(::h)[0-9a-f]{8,}', r'\1', text) return text if path_replacements: for old, new in path_replacements.items(): actual_text = actual_text.replace(old, new) - # Normalize rustc panic symbol hash suffixes that can drift across builds/environments. - actual_text = _normalize_panic_symbol_hashes(actual_text) + # 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_panic_symbol_hashes(expected_text) + expected_text = _normalize_symbol_hashes(expected_text) if actual_text != expected_text: diff = '\n'.join( unified_diff( From a261ebc2ea503f4631fdd959cff34b933bce2f0c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 10:42:45 +0800 Subject: [PATCH 07/14] fix(show): annotate noBody callees with demangled details --- kmir/src/kmir/utils.py | 49 +++++++++++++------ ...c-args-fail.main.cli-stats-leaves.expected | 7 ++- 2 files changed, 39 insertions(+), 17 deletions(-) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index 935d37656..afc878273 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -288,20 +288,23 @@ 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 - setup_call_label = '#setUpCalleeData(_,_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands_Span' + setup_call_labels = { + '#setUpCalleeData(_,_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands_Span', + '#setUpCalleeData(_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands', + } annotations: list[str] = [] match k_cell: case KSequence(items=(KApply(label=KLabel(name=label_name), args=args), *_)) | KApply( label=KLabel(name=label_name), args=args - ) if (label_name == setup_call_label): + ) if (label_name in setup_call_labels): match args: case [ KApply( @@ -309,32 +312,48 @@ def _annotate_unknown_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str] args=[ KApply(args=[KToken(token=symbol_name)]), KApply(label=KLabel(name='defId(_)_BODY_DefId_Int'), args=[KToken(token=def_id_str)]), - _, + KApply(label=KLabel(name='noBody_BODY_MaybeBody'), args=[]), ], ), 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 [ + KApply( + label=KLabel(name='MonoItemKind::MonoItemFn'), + args=[ + KApply(args=[KToken(token=symbol_name)]), + KApply(label=KLabel(name='defId(_)_BODY_DefId_Int'), args=[KToken(token=def_id_str)]), + KApply(label=KLabel(name='noBody_BODY_MaybeBody'), args=[]), + ], + ), + operands, + ]: + def_id = int(def_id_str) + span = None case _: return [] case _: return [] - # Use extracted DefId for function name - func_sym = smir_info.function_symbols.get(def_id, {}) - if name := func_sym.get('NormalSym') or func_sym.get('IntrinsicSym'): + # Prefer concrete symbol from the term; for unresolved placeholders, fall back to DefId lookup. + if symbol_name == '\"** UNKNOWN FUNCTION **\"': + func_sym = smir_info.function_symbols.get(def_id, {}) + display_name = func_sym.get('NormalSym') or func_sym.get('IntrinsicSym') + else: + display_name = symbol_name.strip('\"') + + if display_name: try: - name = _demangle(name) + display_name = _demangle(display_name) except Exception: pass - annotations.append(f' >> function: {name}') + annotations.append(f' >> function: {display_name}') # Use extracted Span for call site - if span in smir_info.spans: + if span is not None and span in smir_info.spans: path, start_row, start_col, _, _ = smir_info.spans[span] annotations.append(f' >> call span: {path}:{start_row}:{start_col}') @@ -379,7 +398,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: diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected index a705eda16..e4e10b74c 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected @@ -5,7 +5,7 @@ │ │ (566 steps) └─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h span: no-location:0 @@ -32,4 +32,7 @@ Leaf paths from init: LEAF CELLS --------------- Node 3: - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17hE" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) ) .Operands , span ( 117 ) ) ~> .K \ No newline at end of file + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17hE" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) ) .Operands , span ( 117 ) ) ~> .K + >> function: core::panicking::panic::h + >> call span: /kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs:53:5 + >> message: 'assertion failed: false' \ No newline at end of file From cc40dd625594255dd853bb7f038c2d8dc5b9605f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 10:47:32 +0800 Subject: [PATCH 08/14] fix(show): satisfy mypy for optional span annotation --- kmir/src/kmir/utils.py | 1 + 1 file changed, 1 insertion(+) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index afc878273..86e3003f2 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -300,6 +300,7 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: } annotations: list[str] = [] + span: int | None = None match k_cell: case KSequence(items=(KApply(label=KLabel(name=label_name), args=args), *_)) | KApply( From 33ce1a34a062c03e1cfc3863d91574427323db34 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 11:25:17 +0800 Subject: [PATCH 09/14] refactor: simplify branch code with loop merge, function promotion, and match dedup - Merge two separate function_symbols loops into a single pass in kompile.py - Promote _normalize_symbol_hashes to module-level in fixtures.py - Hoist duplicated def_id assignment out of match arms in utils.py --- kmir/src/kmir/kompile.py | 16 +++++++--------- kmir/src/kmir/testing/fixtures.py | 19 ++++++++++--------- kmir/src/kmir/utils.py | 6 +++--- 3 files changed, 20 insertions(+), 21 deletions(-) diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 14ede6a90..c48fef906 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -521,23 +521,21 @@ 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'])])], ) - - # Add linked normal symbols that have no local body in `items`. - # They must still map to `monoItemFn(..., noBody)` instead of falling back to UNKNOWN FUNCTION. - for ty, sym in smir_info.function_symbols.items(): - normal_sym = sym.get('NormalSym') - if isinstance(normal_sym, str) and ty not in functions: + elif isinstance(sym.get('NormalSym'), str): functions[ty] = KApply( 'MonoItemKind::MonoItemFn', ( - KApply('symbol(_)_LIB_Symbol_String', (stringToken(normal_sym),)), + KApply('symbol(_)_LIB_Symbol_String', (stringToken(sym['NormalSym']),)), KApply('defId(_)_BODY_DefId_Int', (intToken(ty),)), KApply('noBody_BODY_MaybeBody', ()), ), diff --git a/kmir/src/kmir/testing/fixtures.py b/kmir/src/kmir/testing/fixtures.py index 2a99ba443..30772edb0 100644 --- a/kmir/src/kmir/testing/fixtures.py +++ b/kmir/src/kmir/testing/fixtures.py @@ -20,18 +20,19 @@ 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.""" + text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+E', r'\1E', text) + # Some show outputs truncate mangled symbols before trailing `E`. + text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+', r'\1', text) + # Normalize demangled hash suffixes (`...::h`). + text = re.sub(r'(::h)[0-9a-f]{8,}', r'\1', 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: - def _normalize_symbol_hashes(text: str) -> str: - # Mangled symbol hash suffixes can drift across rustc versions/builds. - text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+E', r'\1E', text) - # Some show outputs truncate mangled symbols before trailing `E`. - text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+', r'\1', text) - # Normalize demangled hash suffixes (`...::h`). - text = re.sub(r'(::h)[0-9a-f]{8,}', r'\1', text) - return text - if path_replacements: for old, new in path_replacements.items(): actual_text = actual_text.replace(old, new) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index 86e3003f2..ec53abb73 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -319,7 +319,6 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: operands, KApply(label=KLabel(name='span'), args=[KToken(token=span_str)]), ]: - def_id = int(def_id_str) span = int(span_str) case [ KApply( @@ -332,13 +331,14 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: ), operands, ]: - def_id = int(def_id_str) - span = None + pass case _: return [] case _: return [] + def_id = int(def_id_str) + # Prefer concrete symbol from the term; for unresolved placeholders, fall back to DefId lookup. if symbol_name == '\"** UNKNOWN FUNCTION **\"': func_sym = smir_info.function_symbols.get(def_id, {}) From ffc6a71834a074fa0c4882b2d402cd0538fa35f6 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 11:33:47 +0800 Subject: [PATCH 10/14] refactor(show): simplify noBody annotation to always use DefId lookup Drop symbol_name capture and dual-path logic; always resolve function name from smir_info.function_symbols via DefId, matching the original code path. --- kmir/src/kmir/utils.py | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index ec53abb73..414f38556 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -311,7 +311,7 @@ def _annotate_nobody_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)]), KApply(label=KLabel(name='noBody_BODY_MaybeBody'), args=[]), ], @@ -324,7 +324,7 @@ def _annotate_nobody_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)]), KApply(label=KLabel(name='noBody_BODY_MaybeBody'), args=[]), ], @@ -339,19 +339,14 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: def_id = int(def_id_str) - # Prefer concrete symbol from the term; for unresolved placeholders, fall back to DefId lookup. - if symbol_name == '\"** UNKNOWN FUNCTION **\"': - func_sym = smir_info.function_symbols.get(def_id, {}) - display_name = func_sym.get('NormalSym') or func_sym.get('IntrinsicSym') - else: - display_name = symbol_name.strip('\"') - - if display_name: + # Use extracted DefId for function name + func_sym = smir_info.function_symbols.get(def_id, {}) + if name := func_sym.get('NormalSym') or func_sym.get('IntrinsicSym'): try: - display_name = _demangle(display_name) + name = _demangle(name) except Exception: pass - annotations.append(f' >> function: {display_name}') + annotations.append(f' >> function: {name}') # Use extracted Span for call site if span is not None and span in smir_info.spans: From 74198cafdd44f8b0f369c816cd0055726b659a74 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 11:43:32 +0800 Subject: [PATCH 11/14] refactor(show): remove dead 2-arg setUpCalleeData match arm K semantics only defines the 3-arg variant; the 2-arg label never appears in K terms. Removing it also eliminates the span-None path, setup_call_labels set, and associated scaffolding. --- kmir/src/kmir/utils.py | 25 ++++--------------------- 1 file changed, 4 insertions(+), 21 deletions(-) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index 414f38556..e52329fb6 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -294,18 +294,14 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: from .alloc import Allocation, AllocId, AllocInfo, Memory from .linker import _demangle - setup_call_labels = { - '#setUpCalleeData(_,_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands_Span', - '#setUpCalleeData(_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands', - } + setup_call_label = '#setUpCalleeData(_,_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands_Span' annotations: list[str] = [] - span: int | None = None match k_cell: case KSequence(items=(KApply(label=KLabel(name=label_name), args=args), *_)) | KApply( label=KLabel(name=label_name), args=args - ) if (label_name in setup_call_labels): + ) if (label_name == setup_call_label): match args: case [ KApply( @@ -319,26 +315,13 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: operands, KApply(label=KLabel(name='span'), args=[KToken(token=span_str)]), ]: + def_id = int(def_id_str) span = int(span_str) - case [ - KApply( - label=KLabel(name='MonoItemKind::MonoItemFn'), - args=[ - KApply(args=[KToken()]), - KApply(label=KLabel(name='defId(_)_BODY_DefId_Int'), args=[KToken(token=def_id_str)]), - KApply(label=KLabel(name='noBody_BODY_MaybeBody'), args=[]), - ], - ), - operands, - ]: - pass case _: return [] case _: return [] - def_id = int(def_id_str) - # Use extracted DefId for function name func_sym = smir_info.function_symbols.get(def_id, {}) if name := func_sym.get('NormalSym') or func_sym.get('IntrinsicSym'): @@ -349,7 +332,7 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: annotations.append(f' >> function: {name}') # Use extracted Span for call site - if span is not None and span in smir_info.spans: + if span in smir_info.spans: path, start_row, start_col, _, _ = smir_info.spans[span] annotations.append(f' >> call span: {path}:{start_row}:{start_col}') From e7e8abff9721217a651c97241d932d5bb66536c2 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 11:48:22 +0800 Subject: [PATCH 12/14] refactor(show): restore original match pattern for minimal diff Keep symbol_name capture and wildcard match from master; the only necessary change is removing the UNKNOWN FUNCTION guard. --- kmir/src/kmir/utils.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index e52329fb6..9bca4479c 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -307,9 +307,9 @@ def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]: KApply( label=KLabel(name='MonoItemKind::MonoItemFn'), args=[ - KApply(args=[KToken()]), + KApply(args=[KToken(token=symbol_name)]), KApply(label=KLabel(name='defId(_)_BODY_DefId_Int'), args=[KToken(token=def_id_str)]), - KApply(label=KLabel(name='noBody_BODY_MaybeBody'), args=[]), + _, ], ), operands, From fdbdb3a431e09d3a77608c879e5f855ac32c273d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 11:55:41 +0800 Subject: [PATCH 13/14] fix(show): remove unused noBody symbol binding --- kmir/src/kmir/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py index 9bca4479c..8feb00ca5 100644 --- a/kmir/src/kmir/utils.py +++ b/kmir/src/kmir/utils.py @@ -307,7 +307,7 @@ def _annotate_nobody_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)]), _, ], From 70c0d2de793b3acd0a14cddf0007cea4aec3b740 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 4 Mar 2026 11:49:48 +0800 Subject: [PATCH 14/14] fix(testing): normalize generic symbol hashes in snapshots --- kmir/src/kmir/testing/fixtures.py | 9 +++-- ...t_lib::testing::test_add_in_range.expected | 2 +- .../blackbox_function_symbols.expected.json | 40 +++++++++---------- ...box_function_symbols_reverse.expected.json | 40 +++++++++---------- .../blackbox_functions.expected.json | 10 ++--- ...nflict-fail.check_assume_conflict.expected | 2 +- ...-length-test-fail.array_cast_test.expected | 2 +- .../show/symbolic-args-fail.main.expected | 2 +- ...lic-structs-fail.eats_struct_args.expected | 2 +- .../test_offset_from-fail.testing.expected | 2 +- kmir/src/tests/unit/test_fixtures.py | 27 +++++++++++++ 11 files changed, 83 insertions(+), 55 deletions(-) create mode 100644 kmir/src/tests/unit/test_fixtures.py diff --git a/kmir/src/kmir/testing/fixtures.py b/kmir/src/kmir/testing/fixtures.py index 30772edb0..d42bf606d 100644 --- a/kmir/src/kmir/testing/fixtures.py +++ b/kmir/src/kmir/testing/fixtures.py @@ -22,11 +22,12 @@ def pytest_configure(config) -> None: def _normalize_symbol_hashes(text: str) -> str: """Normalize rustc symbol hash suffixes that drift across builds/environments.""" - text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+E', r'\1E', text) - # Some show outputs truncate mangled symbols before trailing `E`. - text = re.sub(r'(_ZN[0-9A-Za-z_]+17h)[0-9a-f]+', r'\1', text) + # 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'\1E', text) + text = re.sub(r'(_ZN[0-9A-Za-z_$.]+17h)[0-9a-fA-F]+', r'\1', text) # Normalize demangled hash suffixes (`...::h`). - text = re.sub(r'(::h)[0-9a-f]{8,}', r'\1', text) + text = re.sub(r'(::h)[0-9a-fA-F]{8,}', r'\1', text) return text diff --git a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected b/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected index 6c64d5906..3cb67eec2 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected +++ b/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 ( "_ZN3std7process4exit17hf5473 +┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN3std7process4exit17h ┃ ┗━━┓ subst: .Subst ┃ constraint: diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json index 88db28bbd..3058a6679 100644 --- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json +++ b/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$17hE" }, "-5": { - "NormalSym": "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hb92e31f0aaa3d322E" + "NormalSym": "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hE" }, "-4": { - "NormalSym": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h526a5c5d4d9d3202E" + "NormalSym": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17hE" }, "-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$3fmt17hE" }, "-2": { - "NormalSym": "_ZN3std2rt10lang_start17h17250425291430deE" + "NormalSym": "_ZN3std2rt10lang_start17hE" }, "-1": { - "NormalSym": "_ZN8blackbox4main17h56268fefa1135d9eE" + "NormalSym": "_ZN8blackbox4main17hE" }, "0": { - "NormalSym": "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E" + "NormalSym": "_ZN3std2rt19lang_start_internal17hE" }, "13": { - "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h3ac302c9481e885fE" + "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17hE" }, "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$6report17hE" }, "19": { - "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17haae505bd39892fd2E" + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17hE" }, "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$3fmt17hE" }, "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$3fmt17hE" }, "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$3fmt17hE" }, "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$3fmt17hE" }, "30": { - "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h2d8e0aae13049ae8E" + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17hE" }, "32": { - "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h5c121846c1652782E" + "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17hE" }, "35": { "IntrinsicSym": "black_box" }, "36": { - "NormalSym": "_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E" + "NormalSym": "_ZN4core9panicking19assert_failed_inner17hE" }, "43": { - "NormalSym": "_ZN8blackbox7add_one17h19d5f3b41fdf13daE" + "NormalSym": "_ZN8blackbox7add_one17hE" }, "44": { - "NormalSym": "_ZN4core4hint9black_box17h0bfc654765aa2ddfE" + "NormalSym": "_ZN4core4hint9black_box17hE" }, "45": { - "NormalSym": "_ZN4core9panicking13assert_failed17h9acd0d94a91ca0eaE" + "NormalSym": "_ZN4core9panicking13assert_failed17hE" }, "48": { "NoOpSym": "" diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json index 4fcfd0647..05755f54f 100644 --- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json +++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json @@ -1,62 +1,62 @@ { - "_ZN3std2rt10lang_start17h17250425291430deE": [ + "_ZN3std2rt10lang_start17hE": [ -2 ], - "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h5c121846c1652782E": [ + "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17hE": [ 32 ], - "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E": [ + "_ZN3std2rt19lang_start_internal17hE": [ 0 ], - "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h3ac302c9481e885fE": [ + "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17hE": [ 13 ], - "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h3a8781eea2f9ddb7E": [ + "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17hE": [ -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$3fmt17hE": [ 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$3fmt17hE": [ 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$3fmt17hE": [ 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$3fmt17hE": [ 28 ], - "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h526a5c5d4d9d3202E": [ + "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17hE": [ -4 ], - "_ZN4core3ops8function6FnOnce9call_once17h2d8e0aae13049ae8E": [ + "_ZN4core3ops8function6FnOnce9call_once17hE": [ 30 ], - "_ZN4core3ops8function6FnOnce9call_once17haae505bd39892fd2E": [ + "_ZN4core3ops8function6FnOnce9call_once17hE": [ 19 ], - "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hb92e31f0aaa3d322E": [ + "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hE": [ -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$17hE": [ -6 ], - "_ZN4core4hint9black_box17h0bfc654765aa2ddfE": [ + "_ZN4core4hint9black_box17hE": [ 44 ], - "_ZN4core9panicking13assert_failed17h9acd0d94a91ca0eaE": [ + "_ZN4core9panicking13assert_failed17hE": [ 45 ], - "_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E": [ + "_ZN4core9panicking19assert_failed_inner17hE": [ 36 ], - "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h8eaae5c69aab66e9E": [ + "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17hE": [ 14 ], - "_ZN8blackbox4main17h56268fefa1135d9eE": [ + "_ZN8blackbox4main17hE": [ -1 ], - "_ZN8blackbox7add_one17h19d5f3b41fdf13daE": [ + "_ZN8blackbox7add_one17hE": [ 43 ], "black_box": [ 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 f306c611d..029619a88 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 @@ -13579,7 +13579,7 @@ "name": "String", "node": "KSort" }, - "token": "\"_ZN3std2rt19lang_start_internal17h018b8394ba015d86E\"" + "token": "\"_ZN3std2rt19lang_start_internal17hE\"" } ], "arity": 1, @@ -22594,7 +22594,7 @@ "name": "String", "node": "KSort" }, - "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8E\"" + "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hE\"" } ], "arity": 1, @@ -22657,7 +22657,7 @@ "name": "String", "node": "KSort" }, - "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h7baa47f3e5cbe44cE\"" + "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17hE\"" } ], "arity": 1, @@ -22720,7 +22720,7 @@ "name": "String", "node": "KSort" }, - "token": "\"_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17hec74c53b91325b16E\"" + "token": "\"_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17hE\"" } ], "arity": 1, @@ -28248,7 +28248,7 @@ "name": "String", "node": "KSort" }, - "token": "\"_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E\"" + "token": "\"_ZN4core9panicking19assert_failed_inner17hE\"" } ], "arity": 1, diff --git a/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected index 95f08c611..470f41c25 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected @@ -5,7 +5,7 @@ │ │ (61 steps) └─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected index bc39714ca..9198552ba 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected @@ -17,7 +17,7 @@ ┃ │ ┃ │ (6 steps) ┃ └─ 6 (stuck, leaf) -┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 +┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h ┃ span: 32 ┃ ┗━━┓ subst: .Subst diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected index affc081f9..e5b630195 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected @@ -5,7 +5,7 @@ │ │ (566 steps) └─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected index cdddcdc6c..673eb0193 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected @@ -29,7 +29,7 @@ ┃ ┃ │ ┃ ┃ │ (6 steps) ┃ ┃ └─ 10 (stuck, leaf) -┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 +┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h ┃ ┃ span: 32 ┃ ┃ ┃ ┗━━┓ subst: .Subst diff --git a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected index 30e9bc3af..8fd816dd8 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected @@ -114,7 +114,7 @@ ┃ │ ┃ │ (70 steps) ┃ └─ 22 (stuck, leaf) - ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h3 + ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h ┃ span: 32 ┃ ┗━━┓ subst: .Subst diff --git a/kmir/src/tests/unit/test_fixtures.py b/kmir/src/tests/unit/test_fixtures.py new file mode 100644 index 000000000..b9a3de5b5 --- /dev/null +++ b/kmir/src/tests/unit/test_fixtures.py @@ -0,0 +1,27 @@ +from __future__ import annotations + +import pytest + +from kmir.testing.fixtures import _normalize_symbol_hashes + + +@pytest.mark.parametrize( + ('raw', 'expected'), + [ + ( + '_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$3fmt17hE', + ), + ( + '_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8', + '_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h', + ), + ( + 'core::panicking::panic::h941160ead03e2d54', + 'core::panicking::panic::h', + ), + ], + ids=['generic-mangled-full', 'generic-mangled-truncated', 'demangled'], +) +def test_normalize_symbol_hashes(raw: str, expected: str) -> None: + assert _normalize_symbol_hashes(raw) == expected