Updates from master (#763)

* Python code refactoring
* decoding `struct`s
* handle functions with empty body 
* Fix for statistics (several paths)
* nix overlay fix

---------

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: JianHong Zhao <zhaojianhong96@gmail.com>
Co-authored-by: Julian Kuners <julian.kuners@gmail.com>

Author: 4 people

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

flake.nix

@@ -73,15 +73,22 @@
           final: prev:
           let
             rev = self.rev or null;
+            kmir-pyk-pyproject = final.callPackage ./nix/kmir-pyk-pyproject { inherit uv2nix; };
             kmir-pyk = final.callPackage ./nix/kmir-pyk {
-              inherit pyproject-nix pyproject-build-systems uv2nix;
+              inherit pyproject-nix pyproject-build-systems kmir-pyk-pyproject;
               python = final."python${pythonVer}";
+              pyproject-overlays = [ (k-framework.overlays.pyk-pyproject system) ];
             };
             kmir = final.callPackage ./nix/kmir { inherit kmir-pyk rev; };
             kmir-package-test = final.callPackage ./nix/test/package.nix { inherit rev; };
           in
           {
-            inherit kmir-pyk kmir kmir-package-test;
+            inherit
+              kmir-pyk
+              kmir
+              kmir-package-test
+              kmir-pyk-pyproject
+              ;
           };
         pkgs = import nixpkgs {
           inherit system;
@@ -137,5 +144,12 @@
     )
     // {
       overlays.default = final: prev: { inherit (self.packages.${final.system}) kmir; };
+      pyprojectOverlays = {
+        # this pyproject-nix overlay allows for overriding the python packages that are otherwise locked in `uv.lock`
+        # by using this overlay in dependant nix flakes, you ensure that nix overrides also override the python package     
+        pyk-pyproject = system: final: prev: {
+          inherit (self.packages.${system}.kmir-pyk-pyproject.lockFileOverlay final prev) kmir-pyk;
+        };
+      };
     };
 }

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,
@@ -21,6 +21,7 @@
     RefT,
     Single,
     StrT,
+    StructT,
     UintT,
 )
 from .value import (
@@ -71,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')
 
@@ -149,6 +172,8 @@ def decode_value(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMe
             return _decode_int(data, int_ty)
         case ArrayT(elem_ty, length):
             return _decode_array(data, elem_ty, length, types)
+        case StructT(fields=fields, layout=layout):
+            return _decode_struct(data=data, fields=fields, layout=layout, types=types)
         case EnumT(
             discriminants=discriminants,
             fields=fields,
@@ -219,6 +244,28 @@ def _decode_array(
     return RangeValue(elems)
 
 
+def _decode_struct(
+    *,
+    data: bytes,
+    fields: list[Ty],
+    layout: LayoutShape | None,
+    types: Mapping[Ty, TypeMetadata],
+) -> Value:
+    if not layout:
+        raise ValueError('Struct layout not provided')
+
+    offsets = _extract_offsets(layout.fields)
+
+    match layout.variants:
+        case Single(index=0):
+            pass
+        case _:
+            raise ValueError(f'Unexpected layout variants in struct: {layout.variants}')
+
+    field_values = _decode_fields(data=data, tys=fields, offsets=offsets, types=types)
+    return AggregateValue(0, field_values)
+
+
 def _decode_enum(
     *,
     data: bytes,

kmir/src/kmir/kmir.py

@@ -87,45 +87,61 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
         ) as cts:
             yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
 
-    def make_call_config(
+    def _make_concrete_call_config(self, smir_info: SMIRInfo, *, start_symbol: str = 'main') -> KInner:
+        def init_subst() -> dict[str, KInner]:
+            init_config = self.definition.init_config(KSort('GeneratedTopCell'))
+            _, res = split_config_from(init_config)
+            return res
+
+        if not start_symbol in smir_info.function_tys:
+            raise KeyError(f'{start_symbol} not found in program')
+
+        args_info = smir_info.function_arguments[start_symbol]
+        if args_info:
+            raise ValueError(
+                f'Cannot create concrete call configuration for {start_symbol}: function has parameters: {args_info}'
+            )
+
+        # The configuration is the default initial configuration, with the K cell updated with the call terminator
+        # TODO: see if this can be expressed in more simple terms
+        subst = Subst(
+            {
+                **init_subst(),
+                **{
+                    'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
+                },
+            }
+        )
+        empty_config = self.definition.empty_config(KSort('GeneratedTopCell'))
+        config = subst(empty_config)
+        assert not free_vars(config), f'Config by construction should not have any free variables: {config}'
+        return config
+
+    def _make_symbolic_call_config(
         self,
         smir_info: SMIRInfo,
         *,
         start_symbol: str = 'main',
-        sort: str = 'GeneratedTopCell',
-        init: bool = False,
     ) -> tuple[KInner, list[KInner]]:
         if not start_symbol in smir_info.function_tys:
             raise KeyError(f'{start_symbol} not found in program')
 
         args_info = smir_info.function_arguments[start_symbol]
         locals, constraints = symbolic_locals(smir_info, args_info)
-
-        _subst = {
-            'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
-            'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
-            'LOCALS_CELL': list_of(locals),
-        }
-
-        _init_subst: dict[str, KInner] = {}
-        if init:
-            _subst['LOCALS_CELL'] = list_empty()
-            init_config = self.definition.init_config(KSort(sort))
-            _, _init_subst = split_config_from(init_config)
-
-        for key in _init_subst:
-            if key not in _subst:
-                _subst[key] = _init_subst[key]
-
-        subst = Subst(_subst)
-        config = self.definition.empty_config(KSort(sort))
-        return (subst.apply(config), constraints)
+        subst = Subst(
+            {
+                'K_CELL': mk_call_terminator(smir_info.function_tys[start_symbol], len(args_info)),
+                'STACK_CELL': list_empty(),  # FIXME see #560, problems matching a symbolic stack
+                'LOCALS_CELL': list_of(locals),
+            },
+        )
+        empty_config = self.definition.empty_config(KSort('GeneratedTopCell'))
+        config = subst(empty_config)
+        return config, constraints
 
     def run_smir(self, smir_info: SMIRInfo, start_symbol: str = 'main', depth: int | None = None) -> Pattern:
         smir_info = smir_info.reduce_to(start_symbol)
-        init_config, init_constraints = self.make_call_config(smir_info, start_symbol=start_symbol, init=True)
-        if len(free_vars(init_config)) > 0 or len(init_constraints) > 0:
-            raise ValueError(f'Cannot run function with variables: {start_symbol} - {free_vars(init_config)}')
+        init_config = self._make_concrete_call_config(smir_info, start_symbol=start_symbol)
         init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell'))
         result = self.run_pattern(init_kore, depth=depth)
         return result
@@ -135,10 +151,9 @@ def apr_proof_from_smir(
         id: str,
         smir_info: SMIRInfo,
         start_symbol: str = 'main',
-        sort: str = 'GeneratedTopCell',
         proof_dir: Path | None = None,
     ) -> APRProof:
-        lhs_config, constraints = self.make_call_config(smir_info, start_symbol=start_symbol, sort=sort)
+        lhs_config, constraints = self._make_symbolic_call_config(smir_info, start_symbol=start_symbol)
         lhs = CTerm(lhs_config, constraints)
 
         var_config, var_subst = split_config_from(lhs_config)
@@ -181,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]:

kmir/src/kmir/ty.py

@@ -146,7 +146,7 @@ def from_raw(data: Any) -> EnumT:
                     adt_def=adt_def,
                     discriminants=list(discriminants),
                     fields=[list(tys) for tys in fields],
-                    layout=LayoutShape.from_raw(layout),
+                    layout=LayoutShape.from_raw(layout) if layout is not None else None,
                 )
             case _:
                 raise _cannot_parse_as('EnumT', data)
@@ -467,6 +467,7 @@ class StructT(TypeMetadata):
     name: str
     adt_def: int
     fields: list[Ty]
+    layout: LayoutShape | None
 
     @staticmethod
     def from_raw(data: Any) -> StructT:
@@ -476,16 +477,25 @@ def from_raw(data: Any) -> StructT:
                     'name': name,
                     'adt_def': adt_def,
                     'fields': fields,
+                    'layout': layout,
                 }
             }:
                 return StructT(
                     name=name,
                     adt_def=adt_def,
                     fields=list(fields),
+                    layout=LayoutShape.from_raw(layout) if layout is not None else None,
                 )
             case _:
                 raise _cannot_parse_as('StructT', data)
 
+    def nbytes(self, types: Mapping[Ty, TypeMetadata]) -> int:
+        match self.layout:
+            case None:
+                raise ValueError(f'Cannot determine size, layout is missing for: {self}')
+            case LayoutShape(size=size):
+                return size.in_bytes
+
 
 @dataclass
 class UnionT(TypeMetadata):