fix(kompile): map linked NormalSym functions to monoItemFn(noBody)#953
Conversation
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.
…nd 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
Drop symbol_name capture and dual-path logic; always resolve function name from smir_info.function_symbols via DefId, matching the original code path.
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.
Keep symbol_name capture and wildcard match from master; the only necessary change is removing the UNKNOWN FUNCTION guard.
24a25c7 to
fdbdb3a
Compare
|
I think that it should be good to avoid |
kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected
Show resolved
Hide resolved
|
I know I have gotten to this late, but I want to bring up something related. We are not being consistent between instrinsics and other functions. For
^^^ Notice Ideally I would like use a demangled but qualified name for everything. e.g.:
This would remove ambiguity and stop the need to do regex stuff to strip hashes etc. |
- fix(kompile): map linked NormalSym functions to monoItemFn(noBody) [953](#953) - fix(rt): generalize direct-tag enum decoding to any variant count and discriminant [955](#955) - fix(rt): closure aggregate + #setTupleArgs fallback [952](#952) - fix(rt): bug fix for castKindPtrToPtr [974](#974) - fix(rt): repair closure callee setup for iter-eq repro [957](#957)
- fix(rt): handle fun-type closure env refs in callee setup [956](runtimeverification/mir-semantics#956) - fix(decode): accept signed enum tag scalars in _extract_tag [954](runtimeverification/mir-semantics#954) - Added check for FunType in setupCalleeClosure [969](runtimeverification/mir-semantics#969) - Merge in latest master [973](runtimeverification/mir-semantics#973) - fix(kompile): map linked NormalSym functions to monoItemFn(noBody) [953](runtimeverification/mir-semantics#953) - fix(rt): generalize direct-tag enum decoding to any variant count and discriminant [955](runtimeverification/mir-semantics#955) - fix(spl-token): encode multisig signers as pubkey aggregates [958](runtimeverification/mir-semantics#958) - fix(rt): closure aggregate + #setTupleArgs fallback [952](runtimeverification/mir-semantics#952) - fix(rt): bug fix for castKindPtrToPtr [974](runtimeverification/mir-semantics#974) - fix(rt): repair closure callee setup for iter-eq repro [957](runtimeverification/mir-semantics#957) - Change the number of signers from 11 to 3 [982](runtimeverification/mir-semantics#982) - Merging latest master into feature/p-token [981](runtimeverification/mir-semantics#981)

Summary
MonoItemKind::MonoItemFn(symbol(...), defId(...), noBody)for linkedNormalSymentries that are present infunction_symbolsbut missing fromitems."** UNKNOWN FUNCTION **"for bodyless linked functions.kmir show --statistics --leavesannotations fornoBodycallees (>> function,>> call span,>> message) even after replacing"** UNKNOWN FUNCTION **"with concrete symbols.Context
In multi-crate SMIR, linked external functions can exist in
function_symbolsbut not in localitems(no local body). Before this change, that gap could leavelookupFunction(Ty)without a generatedmonoItemFnequation.Red vs Green
RED (actual stuck shape in show fixtures):
This is the unresolved-function path.
GREEN (after fix):
The same path now resolves to a concrete linked symbol instead of
"** UNKNOWN FUNCTION **".