diff --git a/CLAUDE.md b/CLAUDE.md index d9e55afaf..00a0d4de7 100644 --- a/CLAUDE.md +++ b/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 diff --git a/kmir/src/kmir/decoding.py b/kmir/src/kmir/decoding.py index a38e3649d..98e77b6ea 100644 --- a/kmir/src/kmir/decoding.py +++ b/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') diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index b556d874d..cc8af54eb 100644 --- a/kmir/src/kmir/kmir.py +++ b/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) diff --git a/kmir/src/kmir/linker.py b/kmir/src/kmir/linker.py index 4ffc7f714..060d26a9d 100644 --- a/kmir/src/kmir/linker.py +++ b/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', '')!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) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index e72538bf1..fe7795b60 100644 --- a/kmir/src/kmir/smir.py +++ b/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]: