feat: handle empty-body functions in smir.json.

CLAUDE.md

@@ -13,7 +13,7 @@ MIR Semantics provides a K Framework-based formal semantics for Rust's Stable MI
 # Initial setup - install stable-mir-json tool for SMIR generation
 make stable-mir-json
 
-# Build K semantics definitions (required after any K file changes)
+# Build K semantics definitions (required after K file changes)
 make build
 
 # Full build and check

kmir/src/kmir/decoding.py

@@ -6,7 +6,7 @@
 from pyk.kast.inner import KApply
 from pyk.kast.prelude.string import stringToken
 
-from .alloc import Allocation, AllocInfo, Memory, ProvenanceEntry, ProvenanceMap
+from .alloc import Allocation, AllocInfo, Function, Memory, ProvenanceEntry, ProvenanceMap, Static, VTable
 from .ty import (
     ArbitraryFields,
     ArrayT,
@@ -72,6 +72,28 @@ def decode_alloc_or_unable(alloc_info: AllocInfo, types: Mapping[Ty, TypeMetadat
         ):
             data = bytes(n or 0 for n in bytez)
             return _decode_memory_alloc_or_unable(data=data, ptrs=ptrs, ty=ty, types=types)
+        case AllocInfo(
+            ty=_,
+            # `Static` currently only carries `def_id`; we ignore it here.
+            global_alloc=Static(),
+        ):
+            # Static global alloc does not carry raw bytes here; leave as unable-to-decode placeholder
+            return UnableToDecodeValue('Static global allocation not decoded')
+        case AllocInfo(
+            ty=_,
+            global_alloc=Function(
+                instance=_,
+            ),
+        ):
+            # Function alloc currently not decoded to a runtime value
+            return UnableToDecodeValue('Function global allocation not decoded')
+        case AllocInfo(
+            ty=_,
+            # `VTable` carries `ty` and optional `binder`; we ignore both here.
+            global_alloc=VTable(),
+        ):
+            # VTable alloc currently not decoded to a runtime value
+            return UnableToDecodeValue('VTable global allocation not decoded')
         case _:
             raise AssertionError('Unhandled case')
 

kmir/src/kmir/kmir.py

@@ -196,7 +196,18 @@ def prove_rs(opts: ProveRSOpts) -> APRProof:
                     smir_info = SMIRInfo(cargo_get_smir_json(opts.rs_file, save_smir=opts.save_smir))
 
                 smir_info = smir_info.reduce_to(opts.start_symbol)
+                # Report whether the reduced call graph includes any functions without MIR bodies
+                missing_body_syms = [
+                    sym
+                    for sym, item in smir_info.items.items()
+                    if 'MonoItemFn' in item['mono_item_kind']
+                    and item['mono_item_kind']['MonoItemFn'].get('body') is None
+                ]
+                has_missing = len(missing_body_syms) > 0
                 _LOGGER.info(f'Reduced items table size {len(smir_info.items)}')
+                if has_missing:
+                    _LOGGER.info(f'missing-bodies-present={has_missing} count={len(missing_body_syms)}')
+                    _LOGGER.debug(f'Missing-body function symbols (first 5): {missing_body_syms[:5]}')
 
                 kmir = KMIR.from_kompiled_kore(
                     smir_info, symbolic=True, bug_report=opts.bug_report, target_dir=str(target_path)

kmir/src/kmir/linker.py

@@ -208,6 +208,14 @@ def apply_offset(info: SMIRInfo, offset: int) -> None:
         match global_alloc:
             case {'Memory': allocation}:  # global_alloc: Memory, allocation: Allocation
                 apply_offset_provenance(allocation['provenance'], offset)
+            case {'Static': alloc_id}:  # global_alloc: Static
+                alloc['global_alloc']['Static'] = alloc_id + offset
+            case {'Function': _}:  # global_alloc: Function
+                # Quick-compat: leave function instance as-is; not used for offset computations
+                pass
+            case {'VTable': _}:  # global_alloc: VTable
+                # Quick-compat: keep as-is (if present). We do not offset embedded types here.
+                pass
             case _:
                 raise ValueError('Unsupported or invalid GlobalAlloc data: {global_alloc}')
 
@@ -249,17 +257,20 @@ def apply_offset_item(item: dict, offset: int) -> None:
     # * traverses function locals and debug information to add `offset` to all `span` fields
     if 'MonoItemFn' in item and 'body' in item['MonoItemFn']:
         body = item['MonoItemFn']['body']
-        for local in body['locals']:
+        if body is None:
+            _LOGGER.warning(f"MonoItemFn {item['MonoItemFn'].get('name', '<unknown>')!r} has no body; skipping offsets")
+            return
+        for local in body.get('locals', []):
             local['ty'] += offset
             local['span'] += offset
-        for block in body['blocks']:
+        for block in body.get('blocks', []):
             for stmt in block['statements']:
                 apply_offset_stmt(stmt['kind'], offset)
                 stmt['span'] += offset
             apply_offset_terminator(block['terminator']['kind'], offset)
             block['terminator']['span'] += offset
         # adjust span in var_debug_info, each item's source_info.span
-        for thing in body['var_debug_info']:
+        for thing in body.get('var_debug_info', []):
             thing['source_info']['span'] += offset
             if 'Constant' in thing['value']:
                 apply_offset_operand({'Constant': thing['value']}, offset)

kmir/src/kmir/smir.py

@@ -104,8 +104,15 @@ def function_arguments(self) -> dict[str, list[dict]]:
 
             mono_item_fn = item['mono_item_kind']['MonoItemFn']
             name = mono_item_fn['name']
-            arg_count = mono_item_fn['body']['arg_count']
-            local_args = mono_item_fn['body']['locals'][1 : arg_count + 1]
+            body = mono_item_fn.get('body')
+            if body is None:
+                # Functions without a MIR body (e.g., externs/const shims) have no arguments to inspect.
+                # Skip adding entries for them; callers should not rely on args for such symbols.
+                _LOGGER.debug(f'Skipping function_arguments for {name}: missing body')
+                continue
+
+            arg_count = body['arg_count']
+            local_args = body['locals'][1 : arg_count + 1]
             res[name] = local_args
         return res
 
@@ -195,12 +202,16 @@ def call_edges(self) -> dict[Ty, set[Ty]]:
             # skip functions not present in the `function_symbols_reverse` table
             if not sym in self.function_symbols_reverse:
                 continue
-            called_funs = [
-                b['terminator']['kind']['Call']['func']
-                for b in item['mono_item_kind']['MonoItemFn']['body']['blocks']
-                if 'Call' in b['terminator']['kind']
-            ]
-            called_tys = {Ty(op['Constant']['const_']['ty']) for op in called_funs if 'Constant' in op}
+            body = item['mono_item_kind']['MonoItemFn'].get('body')
+            if body is None or 'blocks' not in body:
+                # No MIR body means we cannot extract call edges; treat as having no outgoing edges.
+                _LOGGER.debug(f'Skipping call edge extraction for {sym}: missing body')
+                called_tys: set[Ty] = set()
+            else:
+                called_funs = [
+                    b['terminator']['kind']['Call']['func'] for b in body['blocks'] if 'Call' in b['terminator']['kind']
+                ]
+                called_tys = {Ty(op['Constant']['const_']['ty']) for op in called_funs if 'Constant' in op}
             # TODO also add any constant operands used as arguments whose ty refer to a function
             # the semantics currently does not support this, see issue #488 and stable-mir-json issue #55
             for ty in self.function_symbols_reverse[sym]: