From c6f1b0daa44569e8b506103a504c5cfc6406e66d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 11:57:41 +0000 Subject: [PATCH 01/26] fix(kmir): execute drop glue for drop terminators --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 64 +++++++- kmir/src/kmir/kdist/mir-semantics/rt/types.md | 8 + kmir/src/kmir/kompile.py | 13 +- kmir/src/kmir/smir.py | 140 +++++++++++++++--- .../{interior-mut-fail.rs => interior-mut.rs} | 4 +- .../show/interior-mut-fail.main.expected | 15 -- .../prove-rs/show/interior-mut.main.expected | 17 +++ .../src/tests/integration/test_integration.py | 2 +- 8 files changed, 223 insertions(+), 40 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{interior-mut-fail.rs => interior-mut.rs} (74%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 82c28b3f0..12ab7b757 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -219,6 +219,20 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped. ```k + rule [termReturnIgnored]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ + => + #execBlockIdx(TARGET) + + _ => CALLER + _ => #getBlocks(CALLER) + CALLER => NEWCALLER + place(local(-1), .ProjectionElems) => NEWDEST + someBasicBlockIdx(TARGET) => NEWTARGET + _ => UNWIND + _ => NEWLOCALS + ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK + [priority(40)] + rule [termReturnSome]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #setLocalValue(DEST, #decrementRef(VAL)) ~> #execBlockIdx(TARGET) @@ -474,6 +488,8 @@ An operand may be a `Reference` (the only way a function could access another fu => ListItem(newLocal(TY, MUT)) #reserveFor(REST) + syntax Operand ::= operandValue ( Value ) + syntax KItem ::= #setArgsFromStack ( Int, Operands) | #setArgFromStack ( Int, Operand) | #execIntrinsic ( MonoItemKind, Operands, Place, Span ) @@ -493,6 +509,12 @@ An operand may be a `Reference` (the only way a function could access another fu ... + rule #setArgFromStack(IDX, operandValue(VAL)) + => + #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL)) + ... + + rule #setArgFromStack(IDX, operandCopy(place(local(I), .ProjectionElems))) => #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I))) @@ -669,12 +691,52 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error. ```k - rule [termDrop]: #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN)) + syntax MaybeTy ::= #dropPlaceTy(Place, List) [function, total] + + rule #dropPlaceTy(place(local(I), PROJS), LOCALS) + => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + requires 0 <=Int I andBool I TyUnknown [owise] + + syntax KItem ::= #execDropCall ( MaybeTy, Place, BasicBlockIdx, UnwindAction, Span ) + | #callDropGlue ( Ty, BasicBlockIdx, UnwindAction, Span ) + + rule [termDropGlue]: #execTerminator(terminator(terminatorKindDrop(PLACE, TARGET, UNWIND), SPAN)) + => + #execDropCall(#lookupDropFunctionTy(#dropPlaceTy(PLACE, LOCALS)), PLACE, TARGET, UNWIND, SPAN) + ... + + LOCALS + + rule #execDropCall(TyUnknown, _PLACE, TARGET, _UNWIND, _SPAN) => #execBlockIdx(TARGET) ... + rule #execDropCall(FTY:Ty, PLACE, TARGET, UNWIND, SPAN) + => + rvalueAddressOf(mutabilityMut, PLACE) ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN) + ... + + + rule PTR:Value ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN) + => + #execTerminatorCall( + FTY, + lookupFunction(FTY), + operandValue(PTR) .Operands, + place(local(-1), .ProjectionElems), + someBasicBlockIdx(TARGET), + UNWIND, + SPAN + ) + ... + + syntax MIRError ::= "ReachedUnreachable" rule [termUnreachable]: #execTerminator(terminator(terminatorKindUnreachable, _SPAN)) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index aaf854c13..71fa2e773 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -211,6 +211,14 @@ To make this function total, an optional `MaybeTy` is used. syntax MaybeTy ::= Ty | "TyUnknown" + syntax MaybeTy ::= lookupDropFunctionTy ( Ty ) [function, total, symbol(lookupDropFunctionTy)] + | #lookupDropFunctionTy ( MaybeTy ) [function, total] + + rule #lookupDropFunctionTy(TY:Ty) => lookupDropFunctionTy(TY) + rule #lookupDropFunctionTy(TyUnknown) => TyUnknown + + rule lookupDropFunctionTy(_) => TyUnknown [owise] + syntax MaybeTy ::= #transparentFieldTy ( TypeInfo ) [function, total] rule #transparentFieldTy(typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) => FIELD diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 85035d4bd..32750ac7c 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -513,6 +513,17 @@ def get_int_arg(app: KInner) -> int: type_equations = _make_stratified_rules(kmir, 'lookupTy', 'Ty', 'TypeInfo', 'ty', type_assocs, invalid_type) + drop_function_assocs = [(int(ty), KApply('ty', (intToken(int(drop_ty)),))) for ty, drop_ty in smir_info.drop_function_tys.items()] + drop_function_equations = _make_stratified_rules( + kmir, + 'lookupDropFunctionTy', + 'Ty', + 'MaybeTy', + 'ty', + drop_function_assocs, + KApply('TyUnknown_RT-TYPES_MaybeTy', ()), + ) + invalid_alloc_n = KApply( 'InvalidAlloc(_)_RT-VALUE-SYNTAX_Evaluation_AllocId', (KApply('allocId', (KVariable('N'),)),) ) @@ -527,7 +538,7 @@ def get_int_arg(app: KInner) -> int: if break_on_function: break_on_rules.append(_mk_break_on_functions_rule(kmir, break_on_function)) - return [*equations, *type_equations, *alloc_equations, *break_on_rules] + return [*equations, *type_equations, *drop_function_equations, *alloc_equations, *break_on_rules] def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 1ce7b897b..f236c98f2 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -7,7 +7,7 @@ from typing import TYPE_CHECKING, NewType from .alloc import AllocInfo -from .ty import EnumT, RefT, StructT, Ty, TypeMetadata, UnionT +from .ty import ArrayT, EnumT, PtrT, RefT, StructT, TupleT, Ty, TypeMetadata, UnionT if TYPE_CHECKING: from collections.abc import Sequence @@ -173,6 +173,37 @@ def function_tys(self) -> dict[str, int]: res[name] = fun_syms[sym][0] return res + @cached_property + def drop_function_tys(self) -> dict[Ty, Ty]: + res: dict[Ty, Ty] = {} + + for sym, item in self.items.items(): + if sym not in self.function_symbols_reverse: + continue + + mono_item = item['mono_item_kind'].get('MonoItemFn') + if mono_item is None: + continue + + if not mono_item['name'].startswith('std::ptr::drop_in_place::<'): + continue + + body = mono_item.get('body') + if body is None or body['arg_count'] < 1: + continue + + arg_ty = Ty(body['locals'][1]['ty']) + arg_type = self.types.get(arg_ty) + if not isinstance(arg_type, (PtrT, RefT)): + _LOGGER.debug(f'Skipping drop glue {sym}: unexpected argument type {arg_type}') + continue + + pointee_ty = Ty(arg_type.pointee_type) + fn_ty = Ty(self.function_symbols_reverse[sym][0]) + res[pointee_ty] = fn_ty + + return res + @cached_property def spans(self) -> dict[int, tuple[Path, int, int, int, int]]: return {id: (p, sr, sc, er, ec) for id, [p, sr, sc, er, ec] in self._smir['spans']} @@ -232,29 +263,100 @@ def call_edges(self) -> dict[Ty, set[Ty]]: else: called_tys = set() for block in body['blocks']: - if 'Call' not in block['terminator']['kind']: - continue - call = block['terminator']['kind']['Call'] - - # 1. Direct call: the function being called - func = call['func'] - if 'Constant' in func: - called_tys.add(Ty(func['Constant']['const_']['ty'])) - - # 2. Indirect call: function pointers passed as arguments - # These are ZeroSized constants whose ty is in the function table - for arg in call.get('args', []): - if 'Constant' in arg: - const_ = arg['Constant'].get('const_', {}) - if const_.get('kind') == 'ZeroSized': - ty = const_.get('ty') - if isinstance(ty, int) and ty in function_tys: - called_tys.add(Ty(ty)) + terminator = block['terminator']['kind'] + + if 'Call' in terminator: + call = terminator['Call'] + + # 1. Direct call: the function being called + func = call['func'] + if 'Constant' in func: + called_tys.add(Ty(func['Constant']['const_']['ty'])) + + # 2. Indirect call: function pointers passed as arguments + # These are ZeroSized constants whose ty is in the function table + for arg in call.get('args', []): + if 'Constant' in arg: + const_ = arg['Constant'].get('const_', {}) + if const_.get('kind') == 'ZeroSized': + ty = const_.get('ty') + if isinstance(ty, int) and ty in function_tys: + called_tys.add(Ty(ty)) + + if 'Drop' in terminator: + drop = terminator['Drop'] + drop_ty = self._place_ty(body, drop['place']) + if drop_ty is None: + continue + drop_fn_ty = self.drop_function_tys.get(drop_ty) + if drop_fn_ty is not None: + called_tys.add(drop_fn_ty) for ty in self.function_symbols_reverse[sym]: result[Ty(ty)] = called_tys return result + def _place_ty(self, body: dict, place: dict) -> Ty | None: + local = place.get('local') + if not isinstance(local, int): + return None + locals_ = body.get('locals', []) + if not (0 <= local < len(locals_)): + return None + + current_ty = Ty(locals_[local]['ty']) + for projection in place.get('projection', []): + current_ty = self._projected_ty(current_ty, projection) + if current_ty is None: + return None + + return current_ty + + def _projected_ty(self, ty: Ty, projection: object) -> Ty | None: + type_info = self.types.get(ty) + if type_info is None: + return None + + if projection == 'Deref': + if isinstance(type_info, (PtrT, RefT)): + return Ty(type_info.pointee_type) + return None + + if not isinstance(projection, dict): + return None + + if 'Field' in projection: + index, _ = projection['Field'] + if isinstance(type_info, (StructT, UnionT)): + fields = type_info.fields + elif isinstance(type_info, TupleT): + fields = type_info.components + elif isinstance(type_info, EnumT): + # Field projection into enums is only well-defined after a downcast. + return None + else: + return None + + if 0 <= index < len(fields): + return Ty(fields[index]) + return None + + if 'ConstantIndex' in projection and isinstance(type_info, ArrayT): + return Ty(type_info.element_type) + + if 'Subslice' in projection and isinstance(type_info, ArrayT): + return ty + + if 'OpaqueCast' in projection or 'Subtype' in projection: + key = 'OpaqueCast' if 'OpaqueCast' in projection else 'Subtype' + cast_ty = projection[key] + return Ty(cast_ty) if isinstance(cast_ty, int) else None + + if 'Downcast' in projection: + return ty + + return None + def compute_closure(start_nodes: Sequence[Ty], edges: dict[Ty, set[Ty]]) -> set[Ty]: work = deque(start_nodes) diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut.rs similarity index 74% rename from kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut.rs index 4be7fe1e8..db549954b 100644 --- a/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs +++ b/kmir/src/tests/integration/data/prove-rs/interior-mut.rs @@ -20,12 +20,10 @@ impl Counter { fn main() { let counter = Counter::new(0); - // println!("Before: {}", counter.get()); - // We only have &counter, but can still mutate inside + // We only have &counter, but can still mutate inside. counter.increment(); counter.increment(); assert!(2 == counter.get()); - // println!("After: {}", counter.get()); } 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 deleted file mode 100644 index 4c165cf72..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (877 steps) -└─ 3 (stuck, leaf) - #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core4cell22panic_already - span: 32 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected new file mode 100644 index 000000000..29c87b5b0 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected @@ -0,0 +1,17 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (2626 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d6e891398..90f44ec5c 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -43,7 +43,7 @@ } PROVE_SHOW_SPECS = [ 'local-raw-fail', - 'interior-mut-fail', + 'interior-mut', 'interior-mut3-fail', 'iter_next_3', 'assert_eq_exp', From e9e918df81206595e78bc96a13c52911fa5d1e83 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 12:00:42 +0000 Subject: [PATCH 02/26] test(kmir): drop redundant interior-mut show output --- .../prove-rs/show/interior-mut.main.expected | 17 ----------------- kmir/src/tests/integration/test_integration.py | 1 - 2 files changed, 18 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected deleted file mode 100644 index 29c87b5b0..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (2626 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 90f44ec5c..2303d740b 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -43,7 +43,6 @@ } PROVE_SHOW_SPECS = [ 'local-raw-fail', - 'interior-mut', 'interior-mut3-fail', 'iter_next_3', 'assert_eq_exp', From 5e64648ac44887484fa1895177fc3a1b35aaf811 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Mar 2026 00:02:54 +0000 Subject: [PATCH 03/26] fix(ci): satisfy mypy for drop-glue reachability --- kmir/src/kmir/kompile.py | 5 ++++- kmir/src/kmir/smir.py | 3 ++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index 32750ac7c..dac0c93f0 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -513,7 +513,10 @@ def get_int_arg(app: KInner) -> int: type_equations = _make_stratified_rules(kmir, 'lookupTy', 'Ty', 'TypeInfo', 'ty', type_assocs, invalid_type) - drop_function_assocs = [(int(ty), KApply('ty', (intToken(int(drop_ty)),))) for ty, drop_ty in smir_info.drop_function_tys.items()] + drop_function_assocs: list[tuple[int, KInner]] + drop_function_assocs = [ + (int(ty), KApply('ty', (intToken(int(drop_ty)),))) for ty, drop_ty in smir_info.drop_function_tys.items() + ] drop_function_equations = _make_stratified_rules( kmir, 'lookupDropFunctionTy', diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index f236c98f2..7bca29c72 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -304,8 +304,9 @@ def _place_ty(self, body: dict, place: dict) -> Ty | None: if not (0 <= local < len(locals_)): return None - current_ty = Ty(locals_[local]['ty']) + current_ty: Ty | None = Ty(locals_[local]['ty']) for projection in place.get('projection', []): + assert current_ty is not None current_ty = self._projected_ty(current_ty, projection) if current_ty is None: return None From 83eb9b5db8c8605f0b1b8332fd291db3300b247f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 31 Mar 2026 12:39:36 +0000 Subject: [PATCH 04/26] fix(smir): preserve drop glue edges for downcast fields --- kmir/src/kmir/smir.py | 5 +- .../two-crate-bin/crate2::main.expected | 2 +- .../crate2::test_crate1_with.expected | 2 +- kmir/src/tests/unit/test_smir.py | 85 +++++++++++++++++++ 4 files changed, 91 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 7bca29c72..b4d88f312 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -327,7 +327,10 @@ def _projected_ty(self, ty: Ty, projection: object) -> Ty | None: return None if 'Field' in projection: - index, _ = projection['Field'] + index, field_ty = projection['Field'] + if isinstance(field_ty, int): + return Ty(field_ty) + if isinstance(type_info, (StructT, UnionT)): fields = type_info.fields elif isinstance(type_info, TupleT): diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected index 544958705..60dbf8403 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (737 steps) +│ (740 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected index bd3076868..bdade977c 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (216 steps) +│ (217 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/unit/test_smir.py b/kmir/src/tests/unit/test_smir.py index 9be42f87c..688eedf12 100644 --- a/kmir/src/tests/unit/test_smir.py +++ b/kmir/src/tests/unit/test_smir.py @@ -45,3 +45,88 @@ def test_function_symbols_reverse(smir_file: Path, update_expected_output: bool) def test_function_tys(smir_file: Path, update_expected_output: bool) -> None: """Test function_tys using actual SMIR JSON data.""" _test_smir_property(smir_file, 'function_tys', update_expected_output) + + +def test_call_edges_preserve_drop_glue_for_downcast_field() -> None: + smir_info = SMIRInfo( + { + 'name': 'drop-downcast-field', + 'allocs': [], + 'types': [ + [ + 1, + { + 'EnumType': { + 'name': 'Wrapper', + 'adt_def': 1, + 'discriminants': [0], + 'fields': [[2]], + 'layout': None, + } + }, + ], + [ + 2, + { + 'StructType': { + 'name': 'Inner', + 'adt_def': 2, + 'fields': [], + 'layout': None, + } + }, + ], + [3, {'PtrType': {'pointee_type': 2}}], + ], + 'functions': [ + [10, {'NormalSym': 'caller'}], + [12, {'NormalSym': 'drop_inner'}], + ], + 'items': [ + { + 'symbol_name': 'caller', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'caller', + 'body': { + 'arg_count': 0, + 'locals': [{'ty': 0}, {'ty': 1}], + 'blocks': [ + { + 'terminator': { + 'kind': { + 'Drop': { + 'place': { + 'local': 1, + 'projection': [{'Downcast': 0}, {'Field': [0, 2]}], + }, + 'target': 0, + 'unwind': 'Continue', + } + } + } + } + ], + }, + } + }, + }, + { + 'symbol_name': 'drop_inner', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'std::ptr::drop_in_place::', + 'body': { + 'arg_count': 1, + 'locals': [{'ty': 0}, {'ty': 3}], + 'blocks': [], + }, + } + }, + }, + ], + 'spans': [], + } + ) + + assert smir_info.call_edges == {10: {12}, 12: set()} From e70f00e9783031a27c937101fec1d9db75af8883 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 31 Mar 2026 15:27:24 +0000 Subject: [PATCH 05/26] fix(kmir): handle noop drop-glue calls --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 13 ++++ kmir/src/kmir/kdist/mir-semantics/rt/data.md | 26 ++++++++ kmir/src/kmir/kompile.py | 9 +++ .../blackbox_functions.expected.json | 63 +++++++++++++++++++ .../show/iterator-simple.main.expected | 2 +- kmir/src/tests/unit/test_kompile.py | 36 ++++++++++- 6 files changed, 147 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 12ab7b757..fff717dfb 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -363,6 +363,17 @@ where the returned result should go. requires isIntrinsicFunction(FUNC) andBool #functionNameMatchesEnv(getFunctionName(FUNC)) + syntax Bool ::= isNoOpFunction(MonoItemKind) [function] + rule isNoOpFunction(monoItemFn(symbol(""), _, noBody)) => true + rule isNoOpFunction(_) => false [owise] + + // SMIR marks some semantically empty shims (e.g. drop glue for trivially droppable slices) + // as NoOpSym. They have no body and should continue immediately without switching frames. + rule [termCallNoOp]: + #execTerminatorCall(_, monoItemFn(symbol(""), _, noBody), _ARGS, _DEST, TARGET, _UNWIND, _SPAN) ~> _ + => #continueAt(TARGET) + + // Regular function call - full state switching and stack setup rule [termCallFunction]: #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _ @@ -379,6 +390,7 @@ where the returned result should go. STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK requires notBool isIntrinsicFunction(FUNC) + andBool notBool isNoOpFunction(FUNC) andBool notBool #functionNameMatchesEnv(getFunctionName(FUNC)) // Function call to a function in the break-on set - same as termCallFunction but separate rule id for cut-point @@ -397,6 +409,7 @@ where the returned result should go. STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK requires notBool isIntrinsicFunction(FUNC) + andBool notBool isNoOpFunction(FUNC) andBool #functionNameMatchesEnv(getFunctionName(FUNC)) syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function] diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 2cc068084..c4cf924e5 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -508,6 +508,15 @@ The following rule resolves this situation by using the head element. ) => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? [preserves-definedness, priority(100)] + + rule #traverseProjection( + DEST, + Range(ListItem(Union(_, _) #as VALUE) _REST:List), + projectionElemField(IDX, TY) PROJS, + CTXTS + ) + => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? + [preserves-definedness, priority(100)] ``` #### Unions @@ -649,6 +658,23 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t andBool START <=Int size(ELEMENTS) -Int END [preserves-definedness] // Indexes checked to be in range for ELEMENTS + rule #traverseProjection( + DEST, + VAL, + PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, + CTXTS + ) + => #traverseProjection( + DEST, + Range(ListItem(VAL)), + PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, + CTXTS + ) + ... + + requires notBool isRange(VAL) + [preserves-definedness, priority(100)] + rule #traverseProjection( DEST, Range(ELEMENTS), diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py index dac0c93f0..905af7874 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -571,6 +571,15 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]: 'IntrinsicFunction', [KApply('symbol(_)_LIB_Symbol_String', [stringToken(sym['IntrinsicSym'])])], ) + elif 'NoOpSym' in sym: + functions[ty] = KApply( + 'MonoItemKind::MonoItemFn', + ( + KApply('symbol(_)_LIB_Symbol_String', (stringToken(sym['NoOpSym']),)), + KApply('defId(_)_BODY_DefId_Int', (intToken(ty),)), + KApply('noBody_BODY_MaybeBody', ()), + ), + ) elif isinstance(sym.get('NormalSym'), str): functions[ty] = KApply( 'MonoItemKind::MonoItemFn', 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 029619a88..9611bf166 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 @@ -33998,5 +33998,68 @@ }, "node": "KApply", "variable": false + }, + "48": { + "args": [ + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "String", + "node": "KSort" + }, + "token": "\"\"" + } + ], + "arity": 1, + "label": { + "name": "symbol(_)_LIB_Symbol_String", + "node": "KLabel", + "params": [] + }, + "node": "KApply", + "variable": false + }, + { + "args": [ + { + "node": "KToken", + "sort": { + "name": "Int", + "node": "KSort" + }, + "token": "48" + } + ], + "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 } } \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected index f1cd9a4d1..e650990c0 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (798 steps) +│ (1113 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/unit/test_kompile.py b/kmir/src/tests/unit/test_kompile.py index de8366cba..ca235fa03 100644 --- a/kmir/src/tests/unit/test_kompile.py +++ b/kmir/src/tests/unit/test_kompile.py @@ -1,10 +1,16 @@ from __future__ import annotations from typing import TYPE_CHECKING, Any, cast +from unittest.mock import Mock + +from pyk.kast.inner import KApply +from pyk.kast.prelude.kint import intToken +from pyk.kast.prelude.string import stringToken from pyk.kore.syntax import And, App, Axiom, EVar, Rewrites, SortApp, Top -from kmir.kompile import _add_exists_quantifiers, _collect_evars, _load_extra_module_rules +from kmir.kompile import _add_exists_quantifiers, _collect_evars, _functions, _load_extra_module_rules +from kmir.smir import SMIRInfo if TYPE_CHECKING: from pathlib import Path @@ -110,3 +116,31 @@ def which(target: str) -> Path: assert captured['file_path'] == module_path assert captured['module_name'] == 'TEST' assert captured['include_dirs'] == ((tmp_path / 'custom-haskell-target'),) + + +def test_functions_preserve_noop_symbols() -> None: + smir_info = SMIRInfo( + { + 'name': 'noop-sym', + 'allocs': [], + 'functions': [[42, {'NoOpSym': ''}]], + 'uneval_consts': [], + 'items': [], + 'types': [], + 'spans': [], + 'debug': None, + 'machine': {}, + } + ) + + kmir = Mock() + kmir.parser = Mock() + + assert _functions(kmir, smir_info)[42] == KApply( + 'MonoItemKind::MonoItemFn', + ( + KApply('symbol(_)_LIB_Symbol_String', (stringToken(''),)), + KApply('defId(_)_BODY_DefId_Int', (intToken(42),)), + KApply('noBody_BODY_MaybeBody', ()), + ), + ) From e869bb77c764a4f089d16f267b386b154ee88525 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 1 Apr 2026 09:43:21 +0000 Subject: [PATCH 06/26] test(kmir): refresh complex-types random snapshots --- .../data/run-smir-random/complex-types/final-0.expected | 2 +- .../data/run-smir-random/complex-types/final-1.expected | 2 +- .../data/run-smir-random/complex-types/final-2.expected | 2 +- .../data/run-smir-random/complex-types/final-3.expected | 2 +- .../data/run-smir-random/complex-types/final-4.expected | 2 +- .../data/run-smir-random/complex-types/final-5.expected | 2 +- .../data/run-smir-random/complex-types/final-6.expected | 2 +- .../data/run-smir-random/complex-types/final-8.expected | 2 +- .../data/run-smir-random/complex-types/final-9.expected | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected index c8bee9fef..ed7ed4fc8 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 207 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 207 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 244 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 183 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected index 50fb59617..7dd57ca56 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 32 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 32 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 130 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 60 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 253 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected index 66dbadacc..f5c7a1a1d 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 46 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 46 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 184 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 86 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected index d408600a9..e7278c339 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 66 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 66 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 242 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 33 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected index 2b6e8720c..499281ed4 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 155 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 155 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 52 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 202 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 245 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected index 73d82794e..b94211e09 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 238 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 238 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 127 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 26 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 80 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected index 3a3a93c89..ff8711b9b 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 18 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 18 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 0 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 74 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected index 056a32057..209c3dca4 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 189 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 189 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 192 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 64 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 98 , 8 , false ) ) ) ) ) diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected index 92a082106..726973973 100644 --- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected +++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected @@ -1,6 +1,6 @@ - #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 95 , 8 , false ) , PointerOffset ( 1 , 8 ) .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) ) ) + #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Range ( .List ) , .ProjectionElems , CtxPointerOffset ( ListItem ( Integer ( 95 , 8 , false ) ) , 1 , 1 ) CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) , 0 , ty ( 23 ) ) CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) , ty ( 74 ) ) CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 3 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 173 , 8 , false ) ) ) ) ) ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 237 , 8 , false ) ) ) ) ) From d099d1098613a7e3ee38c035dae795033a01b5e8 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 1 Apr 2026 14:16:41 +0000 Subject: [PATCH 07/26] docs(kmir): mark bridge projection rules as temporary --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index c4cf924e5..9e27f9482 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -509,6 +509,7 @@ The following rule resolves this situation by using the head element. => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? [preserves-definedness, priority(100)] + // Temporary bridge rule for the current mixed bare-value/Range representation. rule #traverseProjection( DEST, Range(ListItem(Union(_, _) #as VALUE) _REST:List), @@ -658,6 +659,7 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t andBool START <=Int size(ELEMENTS) -Int END [preserves-definedness] // Indexes checked to be in range for ELEMENTS + // Temporary bridge rule for the current mixed bare-value/Range representation. rule #traverseProjection( DEST, VAL, From 81ee2568e0546669bc859db44463ed0fb8f1ae87 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 1 Apr 2026 14:17:46 +0000 Subject: [PATCH 08/26] docs(kmir): clarify bridge projection comments --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 9e27f9482..6437adb66 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -509,7 +509,8 @@ The following rule resolves this situation by using the head element. => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? [preserves-definedness, priority(100)] - // Temporary bridge rule for the current mixed bare-value/Range representation. + // Temporary bridge rule: after PointerOffset lifts a single value to Range(ListItem(...)), + // unwrap a Union head element so the existing Union + Field rules below can keep running. rule #traverseProjection( DEST, Range(ListItem(Union(_, _) #as VALUE) _REST:List), @@ -659,7 +660,8 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t andBool START <=Int size(ELEMENTS) -Int END [preserves-definedness] // Indexes checked to be in range for ELEMENTS - // Temporary bridge rule for the current mixed bare-value/Range representation. + // Temporary bridge rule: PointerOffset is implemented below in terms of Range slicing, so + // lift a single non-Range value to Range(ListItem(...)) to reuse that shared path. rule #traverseProjection( DEST, VAL, From da9b1809fbfeb02b772e3db364391f3a3118dd85 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 2 Apr 2026 02:25:49 +0000 Subject: [PATCH 09/26] docs(kmir): explain ignored return sentinel --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index fff717dfb..529d1ec6a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -219,6 +219,9 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped. ```k + // `place(local(-1), .ProjectionElems)` is a sentinel destination meaning that the caller + // ignores the callee's return value. Skip the normal writeback path in that case, because + // `#setLocalValue` only accepts real local indices and would get stuck on `local(-1)`. rule [termReturnIgnored]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #execBlockIdx(TARGET) From 4f4c96bb1c5e1afcfa40e19a762117eae3c1df0c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 2 Apr 2026 02:51:16 +0000 Subject: [PATCH 10/26] docs(test): clarify downcast drop-glue fixture --- kmir/src/tests/unit/test_smir.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kmir/src/tests/unit/test_smir.py b/kmir/src/tests/unit/test_smir.py index 688eedf12..db293a28e 100644 --- a/kmir/src/tests/unit/test_smir.py +++ b/kmir/src/tests/unit/test_smir.py @@ -48,6 +48,10 @@ def test_function_tys(smir_file: Path, update_expected_output: bool) -> None: def test_call_edges_preserve_drop_glue_for_downcast_field() -> None: + # This SMIR models: + # local 1: Wrapper + # Drop(local 1 . Downcast(0) . Field(0, Inner)) + # so `call_edges` must keep the reachable `std::ptr::drop_in_place::` callee. smir_info = SMIRInfo( { 'name': 'drop-downcast-field', From 432a60be399cfe8554c0cbe9f42ecf381dbb1d29 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 2 Apr 2026 03:14:01 +0000 Subject: [PATCH 11/26] fix(smir): preserve drop glue edges for index projections --- kmir/src/kmir/smir.py | 3 ++ kmir/src/tests/unit/test_smir.py | 80 ++++++++++++++++++++++++++++++++ 2 files changed, 83 insertions(+) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index b4d88f312..c6e1e46db 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -345,6 +345,9 @@ def _projected_ty(self, ty: Ty, projection: object) -> Ty | None: return Ty(fields[index]) return None + if 'Index' in projection and isinstance(type_info, ArrayT): + return Ty(type_info.element_type) + if 'ConstantIndex' in projection and isinstance(type_info, ArrayT): return Ty(type_info.element_type) diff --git a/kmir/src/tests/unit/test_smir.py b/kmir/src/tests/unit/test_smir.py index db293a28e..92d226cab 100644 --- a/kmir/src/tests/unit/test_smir.py +++ b/kmir/src/tests/unit/test_smir.py @@ -134,3 +134,83 @@ def test_call_edges_preserve_drop_glue_for_downcast_field() -> None: ) assert smir_info.call_edges == {10: {12}, 12: set()} + + +def test_call_edges_preserve_drop_glue_for_index_projection() -> None: + # This SMIR models: + # local 1: [Inner; 2] + # local 2: usize + # Drop(local 1 . Index(local 2)) + # so `call_edges` must keep the reachable `std::ptr::drop_in_place::` callee. + smir_info = SMIRInfo( + { + 'name': 'drop-index-field', + 'allocs': [], + 'types': [ + [1, {'ArrayType': {'elem_type': 2, 'size': None}}], + [ + 2, + { + 'StructType': { + 'name': 'Inner', + 'adt_def': 2, + 'fields': [], + 'layout': None, + } + }, + ], + [3, {'PrimitiveType': {'Uint': 'Usize'}}], + [4, {'PtrType': {'pointee_type': 2}}], + ], + 'functions': [ + [10, {'NormalSym': 'caller'}], + [12, {'NormalSym': 'drop_inner'}], + ], + 'items': [ + { + 'symbol_name': 'caller', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'caller', + 'body': { + 'arg_count': 0, + 'locals': [{'ty': 0}, {'ty': 1}, {'ty': 3}], + 'blocks': [ + { + 'terminator': { + 'kind': { + 'Drop': { + 'place': { + 'local': 1, + 'projection': [{'Index': 2}], + }, + 'target': 0, + 'unwind': 'Continue', + } + } + } + } + ], + }, + } + }, + }, + { + 'symbol_name': 'drop_inner', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'std::ptr::drop_in_place::', + 'body': { + 'arg_count': 1, + 'locals': [{'ty': 0}, {'ty': 4}], + 'blocks': [], + }, + } + }, + }, + ], + 'spans': [], + } + ) + + assert smir_info.call_edges == {10: {12}, 12: set()} From 77ed24a6619cd3e87a26e935e72618b22ee55335 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 3 Apr 2026 05:42:20 +0000 Subject: [PATCH 12/26] fix(ci): satisfy isort for test_kompile imports --- kmir/src/tests/unit/test_kompile.py | 1 - 1 file changed, 1 deletion(-) diff --git a/kmir/src/tests/unit/test_kompile.py b/kmir/src/tests/unit/test_kompile.py index ca235fa03..1630a6d99 100644 --- a/kmir/src/tests/unit/test_kompile.py +++ b/kmir/src/tests/unit/test_kompile.py @@ -6,7 +6,6 @@ from pyk.kast.inner import KApply from pyk.kast.prelude.kint import intToken from pyk.kast.prelude.string import stringToken - from pyk.kore.syntax import And, App, Axiom, EVar, Rewrites, SortApp, Top from kmir.kompile import _add_exists_quantifiers, _collect_evars, _functions, _load_extra_module_rules From 4f34cdc29986d6b3e41bbb29eced7f8941998664 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 3 Apr 2026 09:17:25 +0000 Subject: [PATCH 13/26] fix(kmir): preserve move effects for noop calls --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 529d1ec6a..f14b1e7bc 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -370,13 +370,26 @@ where the returned result should go. rule isNoOpFunction(monoItemFn(symbol(""), _, noBody)) => true rule isNoOpFunction(_) => false [owise] + syntax KItem ::= #consumeNoOpArgs(Operands, MaybeBasicBlockIdx) + | #consumeNoOpArg(Operand) [strict(1)] + // SMIR marks some semantically empty shims (e.g. drop glue for trivially droppable slices) - // as NoOpSym. They have no body and should continue immediately without switching frames. + // as NoOpSym. They have no body and should continue immediately without switching frames, + // but `Move` arguments must still invalidate the caller locals that were moved into the call. rule [termCallNoOp]: - #execTerminatorCall(_, monoItemFn(symbol(""), _, noBody), _ARGS, _DEST, TARGET, _UNWIND, _SPAN) ~> _ - => #continueAt(TARGET) + #execTerminatorCall(_, monoItemFn(symbol(""), _, noBody), ARGS, _DEST, TARGET, _UNWIND, _SPAN) ~> _ + => #consumeNoOpArgs(ARGS, TARGET) + rule #consumeNoOpArgs(.Operands, TARGET) => #continueAt(TARGET) ... + + rule #consumeNoOpArgs(OP:Operand MORE:Operands, TARGET) + => #consumeNoOpArg(OP) ~> #consumeNoOpArgs(MORE, TARGET) + ... + + + rule #consumeNoOpArg(_:Value) => .K ... + // Regular function call - full state switching and stack setup rule [termCallFunction]: #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _ @@ -506,6 +519,9 @@ An operand may be a `Reference` (the only way a function could access another fu syntax Operand ::= operandValue ( Value ) + // Internal helper operand for already-evaluated runtime values. + rule operandValue(VAL) => VAL ... + syntax KItem ::= #setArgsFromStack ( Int, Operands) | #setArgFromStack ( Int, Operand) | #execIntrinsic ( MonoItemKind, Operands, Place, Span ) From 9802073e4b4facc09ab69c003fcd0f77ccfc8333 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 3 Apr 2026 10:26:53 +0000 Subject: [PATCH 14/26] fix(smir): accept core drop glue names --- kmir/src/kmir/smir.py | 3 ++- kmir/src/tests/unit/test_smir.py | 44 ++++++++++++++++++++++++++++++++ 2 files changed, 46 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index c6e1e46db..0544fe9e6 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -19,6 +19,7 @@ _LOGGER: Final = logging.getLogger(__name__) _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' +_DROP_IN_PLACE_PREFIXES: Final = ('std::ptr::drop_in_place::<', 'core::ptr::drop_in_place::<') AdtDef = NewType('AdtDef', int) @@ -185,7 +186,7 @@ def drop_function_tys(self) -> dict[Ty, Ty]: if mono_item is None: continue - if not mono_item['name'].startswith('std::ptr::drop_in_place::<'): + if not mono_item['name'].startswith(_DROP_IN_PLACE_PREFIXES): continue body = mono_item.get('body') diff --git a/kmir/src/tests/unit/test_smir.py b/kmir/src/tests/unit/test_smir.py index 92d226cab..32cbf8358 100644 --- a/kmir/src/tests/unit/test_smir.py +++ b/kmir/src/tests/unit/test_smir.py @@ -214,3 +214,47 @@ def test_call_edges_preserve_drop_glue_for_index_projection() -> None: ) assert smir_info.call_edges == {10: {12}, 12: set()} + + +def test_drop_function_tys_accept_core_drop_in_place_names() -> None: + smir_info = SMIRInfo( + { + 'name': 'core-drop-glue', + 'allocs': [], + 'types': [ + [ + 2, + { + 'StructType': { + 'name': 'Inner', + 'adt_def': 2, + 'fields': [], + 'layout': None, + } + }, + ], + [3, {'PtrType': {'pointee_type': 2}}], + ], + 'functions': [ + [12, {'NormalSym': 'drop_inner'}], + ], + 'items': [ + { + 'symbol_name': 'drop_inner', + 'mono_item_kind': { + 'MonoItemFn': { + 'name': 'core::ptr::drop_in_place::', + 'body': { + 'arg_count': 1, + 'locals': [{'ty': 0}, {'ty': 3}], + 'blocks': [], + }, + } + }, + }, + ], + 'spans': [], + } + ) + + assert smir_info.drop_function_tys == {2: 12} From 591638b6178531e8bc078165afbbcb5ece464b41 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 3 Apr 2026 13:30:39 +0000 Subject: [PATCH 15/26] fix(kmir): consume noop call operands explicitly --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 21 +++++++++++++++++-- .../show/iterator-simple.main.expected | 2 +- 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index f14b1e7bc..c8ce16cca 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -371,7 +371,7 @@ where the returned result should go. rule isNoOpFunction(_) => false [owise] syntax KItem ::= #consumeNoOpArgs(Operands, MaybeBasicBlockIdx) - | #consumeNoOpArg(Operand) [strict(1)] + | #consumeNoOpArg(Operand) // SMIR marks some semantically empty shims (e.g. drop glue for trivially droppable slices) // as NoOpSym. They have no body and should continue immediately without switching frames, @@ -388,7 +388,24 @@ where the returned result should go. ... - rule #consumeNoOpArg(_:Value) => .K ... + rule #consumeNoOpArg(operandConstant(_)) => .K ... + + rule #consumeNoOpArg(operandValue(_)) => .K ... + + rule #consumeNoOpArg(operandCopy(place(local(I), .ProjectionElems))) => .K ... + ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List + requires 0 <=Int I + andBool I #consumeNoOpArg(operandMove(place(local(I), _))) => .K ... + (ListItem(StackFrame(_, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List + + requires 0 <=Int I + andBool I .K │ function: main From 910ae063f1908ad8ce7abc2d544a564011b97a26 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 8 Apr 2026 08:09:42 +0000 Subject: [PATCH 16/26] Restore termDrop name and drop iterator-simple show snapshot --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 2 +- .../prove-rs/show/iterator-simple.main.expected | 17 ----------------- kmir/src/tests/integration/test_integration.py | 1 - 3 files changed, 1 insertion(+), 19 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index c8ce16cca..aac27ecc5 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -753,7 +753,7 @@ Drops are elaborated to Noops but still define the continuing control flow. Unre syntax KItem ::= #execDropCall ( MaybeTy, Place, BasicBlockIdx, UnwindAction, Span ) | #callDropGlue ( Ty, BasicBlockIdx, UnwindAction, Span ) - rule [termDropGlue]: #execTerminator(terminator(terminatorKindDrop(PLACE, TARGET, UNWIND), SPAN)) + rule [termDrop]: #execTerminator(terminator(terminatorKindDrop(PLACE, TARGET, UNWIND), SPAN)) => #execDropCall(#lookupDropFunctionTy(#dropPlaceTy(PLACE, LOCALS)), PLACE, TARGET, UNWIND, SPAN) ... diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected deleted file mode 100644 index a2a02a391..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (1116 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 2303d740b..d372205c2 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -57,7 +57,6 @@ 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', 'assert-inhabited-fail', - 'iterator-simple', 'unions-fail', 'transmute-maybe-uninit-fail', 'ptr-through-wrapper-fail', From 45f87438dfc6554b1f895c28405d5dfe47a13e10 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 8 Apr 2026 09:27:26 +0000 Subject: [PATCH 17/26] Fix NoOp move handling and drop glue setup --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 74 ++++++++++++----------- 1 file changed, 39 insertions(+), 35 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index aac27ecc5..d8da64f7c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -219,9 +219,10 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped. ```k - // `place(local(-1), .ProjectionElems)` is a sentinel destination meaning that the caller - // ignores the callee's return value. Skip the normal writeback path in that case, because - // `#setLocalValue` only accepts real local indices and would get stuck on `local(-1)`. + // `place(local(-1), .ProjectionElems)` is the sentinel destination for calls whose + // return should not be written back. Without this rule, the return path would fall + // through to `#setLocalValue`, which only accepts real local indices and would get + // stuck on `local(-1)`. rule [termReturnIgnored]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => #execBlockIdx(TARGET) @@ -390,21 +391,18 @@ where the returned result should go. rule #consumeNoOpArg(operandConstant(_)) => .K ... - rule #consumeNoOpArg(operandValue(_)) => .K ... - rule #consumeNoOpArg(operandCopy(place(local(I), .ProjectionElems))) => .K ... - ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List + LOCALS requires 0 <=Int I - andBool I #consumeNoOpArg(operandMove(place(local(I), _))) => .K ... - (ListItem(StackFrame(_, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List - + LOCALS => LOCALS[I <- typedValue(Moved, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)] requires 0 <=Int I - andBool I #setUpCalleeData( @@ -526,6 +525,21 @@ An operand may be a `Reference` (the only way a function could access another fu // TODO: Haven't handled "noBody" case + rule [setupDropGlueData]: #setUpDropGlueData( + monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))), + PTR, + _SPAN + ) + => + #setLocalValue(place(local(1), .ProjectionElems), #incrementRef(PTR)) ~> #execBlock(FIRST) + ... + + + _ => toKList(BLOCKS) + _ => #reserveFor(NEWLOCALS) + ... + + syntax List ::= #reserveFor( LocalDecls ) [function, total] rule #reserveFor(.LocalDecls) => .List @@ -534,11 +548,6 @@ An operand may be a `Reference` (the only way a function could access another fu => ListItem(newLocal(TY, MUT)) #reserveFor(REST) - syntax Operand ::= operandValue ( Value ) - - // Internal helper operand for already-evaluated runtime values. - rule operandValue(VAL) => VAL ... - syntax KItem ::= #setArgsFromStack ( Int, Operands) | #setArgFromStack ( Int, Operand) | #execIntrinsic ( MonoItemKind, Operands, Place, Span ) @@ -558,12 +567,6 @@ An operand may be a `Reference` (the only way a function could access another fu ... - rule #setArgFromStack(IDX, operandValue(VAL)) - => - #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL)) - ... - - rule #setArgFromStack(IDX, operandCopy(place(local(I), .ProjectionElems))) => #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I))) @@ -772,19 +775,20 @@ Drops are elaborated to Noops but still define the continuing control flow. Unre ... - rule PTR:Value ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN) - => - #execTerminatorCall( - FTY, - lookupFunction(FTY), - operandValue(PTR) .Operands, - place(local(-1), .ProjectionElems), - someBasicBlockIdx(TARGET), - UNWIND, - SPAN - ) - ... + rule [termCallDropGlue]: + PTR:Value ~> #callDropGlue(FTY, TARGET, UNWIND, SPAN) ~> _ + => #setUpDropGlueData(lookupFunction(FTY), PTR, SPAN) + CALLER => FTY + + _ + OLDCALLER => CALLER + OLDDEST => place(local(-1), .ProjectionElems) + OLDTARGET => someBasicBlockIdx(TARGET) + OLDUNWIND => UNWIND + LOCALS + + STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK syntax MIRError ::= "ReachedUnreachable" From c6d1d10f570eceffcebd875856e2b78a7ab959ba Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 10 Apr 2026 03:38:51 +0000 Subject: [PATCH 18/26] test(prove-rs): add noop drop_in_place move repro --- .../data/prove-rs/noop-drop-in-place-move.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/noop-drop-in-place-move.rs diff --git a/kmir/src/tests/integration/data/prove-rs/noop-drop-in-place-move.rs b/kmir/src/tests/integration/data/prove-rs/noop-drop-in-place-move.rs new file mode 100644 index 000000000..2d55e8d23 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/noop-drop-in-place-move.rs @@ -0,0 +1,13 @@ +struct Wrap(u8); + +impl Drop for Wrap { + fn drop(&mut self) { + // `drop_in_place::` is compiled as a `NoOpSym`, but moving its pointer + // argument must still invalidate the current frame's local. + unsafe { std::ptr::drop_in_place(&mut self.0) }; + } +} + +fn main() { + let _w = Wrap(1); +} From c7c7548ab62f61e7075ca8511c58b808c602fe7b Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 11:54:53 +0800 Subject: [PATCH 19/26] Fix local(-1) sentinel comment to reflect actual semantics --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index d8da64f7c..9614bd63e 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -219,8 +219,9 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l If the local `_0` does not have a value (i.e., it remained uninitialised), the function returns unit and writing the value is skipped. ```k - // `place(local(-1), .ProjectionElems)` is the sentinel destination for calls whose - // return should not be written back. Without this rule, the return path would fall + // `place(local(-1), .ProjectionElems)` is the sentinel destination indicating the + // callee is not expected to return a value (e.g. `main`, top-level framework calls, + // or `drop_in_place` functions). Without this rule, the return path would fall // through to `#setLocalValue`, which only accepts real local indices and would get // stuck on `local(-1)`. rule [termReturnIgnored]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ From bce52aab9ce9857b375bfd70e7ad58dc31930c5c Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 15:50:39 +0800 Subject: [PATCH 20/26] Remove temporary bridge rules from #traverseProjection The two bridge rules added in bed35038 (Union-unwrap for Field, and bare-value-to-Range for PointerOffset) treated a symptom rather than the root cause. The real issue is in how removeIndexTail and #typeProjection interact during pointer construction and PtrToPtr casts for slice types. Removing these rules exposes the underlying stuck state so the proper fix can be validated against it. See #1011 for the planned structural fix. --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 28 -------------------- 1 file changed, 28 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 6437adb66..f6f105879 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -509,16 +509,6 @@ The following rule resolves this situation by using the head element. => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? [preserves-definedness, priority(100)] - // Temporary bridge rule: after PointerOffset lifts a single value to Range(ListItem(...)), - // unwrap a Union head element so the existing Union + Field rules below can keep running. - rule #traverseProjection( - DEST, - Range(ListItem(Union(_, _) #as VALUE) _REST:List), - projectionElemField(IDX, TY) PROJS, - CTXTS - ) - => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? - [preserves-definedness, priority(100)] ``` #### Unions @@ -660,24 +650,6 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t andBool START <=Int size(ELEMENTS) -Int END [preserves-definedness] // Indexes checked to be in range for ELEMENTS - // Temporary bridge rule: PointerOffset is implemented below in terms of Range slicing, so - // lift a single non-Range value to Range(ListItem(...)) to reuse that shared path. - rule #traverseProjection( - DEST, - VAL, - PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, - CTXTS - ) - => #traverseProjection( - DEST, - Range(ListItem(VAL)), - PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, - CTXTS - ) - ... - - requires notBool isRange(VAL) - [preserves-definedness, priority(100)] rule #traverseProjection( DEST, From 79bd2021739da85dd84094fa027125565c1374eb Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 16:05:42 +0800 Subject: [PATCH 21/26] test(prove-rs): mark iterator-simple as expected-fail The iterator-simple test exposes a stuck state in #traverseProjection caused by the interaction between removeIndexTail and #typeProjection for slice-of-MaybeUninit pointer casts. Mark as -fail with show snapshot until the root cause in pointer projection construction is resolved. See #1011. --- ...iterator-simple.rs => iterator-simple-fail.rs} | 0 .../show/iterator-simple-fail.main.expected | 15 +++++++++++++++ kmir/src/tests/integration/test_integration.py | 1 + 3 files changed, 16 insertions(+) rename kmir/src/tests/integration/data/prove-rs/{iterator-simple.rs => iterator-simple-fail.rs} (100%) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/iterator-simple.rs b/kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/iterator-simple.rs rename to kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected new file mode 100644 index 000000000..969e64ae5 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (1066 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toStack ( 3 , local ( 3 ) ) , Range ( ListItem ( Union ( f + span: 106 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d372205c2..1e16f53e3 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -69,6 +69,7 @@ 'ptr-cast-array-to-wrapper-fail', 'ptr-cast-array-to-nested-wrapper-fail', 'ptr-cast-array-to-singleton-wrapped-array-fail', + 'iterator-simple-fail', ] From 60b5e5a842d3fa2ca1599752d8cc2da699273f7a Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 16:09:13 +0800 Subject: [PATCH 22/26] Remove consP HACK rule and removeIndexTail from RawPtr aggregate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The consP rule that merged ConstantIndex with PointerOffset was a workaround for a deeper issue: removeIndexTail in #mkAggregate(aggregateKindRawPtr) strips the element-extraction CI(0) when constructing fat pointers from thin pointers, but #typeProjection later adds per-element navigation projections (Field for MaybeUninit→ManuallyDrop→T) that assume the element has already been extracted. Removing removeIndexTail preserves the CI(0) through the fat pointer construction, allowing the subsequent #typeProjection projections to correctly navigate into individual array elements. The consP HACK rule is also removed as it is no longer needed and was conceptually unsound (merging projections from different semantic levels). The iterator-simple test now reaches a different stuck state: PointerOffset(1,0) applied to a scalar Integer after successful element navigation, which is closer to the real remaining issue (projection ordering between CI and PointerOffset). See #1011. --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 5 +---- .../data/prove-rs/show/iterator-simple-fail.main.expected | 4 ++-- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index f6f105879..677f917d1 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -384,9 +384,6 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr rule consP(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) PS:ProjectionElems) => PS [priority(40)] // this rule is not valid if the original pointee has more than one field // rule consP(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct PS:ProjectionElems) => PS [priority(40)] - // HACK: special rule which munges together constant-indexing and offset projections - rule consP( projectionElemConstantIndex(I, 0, false), PointerOffset(OFF, _SIZE) PS) => projectionElemConstantIndex(I +Int OFF, 0, false) PS [priority(40)] - // requires I +Int OFF < _SIZE // _SIZE is metadataSize, needs a < operation for this to work rule consP(projectionElemToZST, projectionElemFromZST PS:ProjectionElems) => PS [priority(40)] rule consP(projectionElemFromZST, projectionElemToZST PS:ProjectionElems) => PS [priority(40)] @@ -1113,7 +1110,7 @@ and an array of the indeicated size gets reconstructed if the provided metadata rule ListItem(PtrLocal(OFFSET, place(LOCAL, PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) ListItem(Integer(LENGTH, 64, false)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT)) - => PtrLocal(OFFSET, place(LOCAL, removeIndexTail(PROJS)), MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE)) + => PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE)) ... // requires LENGTH +Int PTR_OFFSET <=Int ORIGIN_SIZE // refuse to create an invalid fat pointer diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected index 969e64ae5..772d0689f 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected @@ -3,9 +3,9 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (1066 steps) +│ (1069 steps) └─ 3 (stuck, leaf) - #traverseProjection ( toStack ( 3 , local ( 3 ) ) , Range ( ListItem ( Union ( f + #traverseProjection ( toStack ( 3 , local ( 3 ) ) , Integer ( 1 , 32 , true ) , span: 106 From 8c27c7e9a68ee14232d86fd0825599722b2476ff Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 16:38:15 +0800 Subject: [PATCH 23/26] test(prove-rs): add subslice-drop-unsupported-fail repro Add integration test for Subslice projection on an owned array of Drop types. The `let [first, rest @ ..]` pattern generates a Subslice that changes the type from [Droppable; 3] to [Droppable; 2], exercising an unsupported code path in _projected_ty() and K semantics. Marked as expected-fail with show snapshot. --- ...bslice-drop-unsupported-fail.main.expected | 56 +++++++++++++++++++ .../subslice-drop-unsupported-fail.rs | 21 +++++++ .../src/tests/integration/test_integration.py | 1 + 3 files changed, 78 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/subslice-drop-unsupported-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/subslice-drop-unsupported-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/subslice-drop-unsupported-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/subslice-drop-unsupported-fail.main.expected new file mode 100644 index 000000000..bdf9bb53a --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/subslice-drop-unsupported-fail.main.expected @@ -0,0 +1,56 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (90 steps) +├─ 3 +│ #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems ) +│ function: main +│ span: 64 +│ +│ (4 steps) +├─ 4 +│ #execStmt ( statement ( ... kind: statementKindAssign ( ... place: place ( ... l +│ function: main +│ span: 64 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 5 +┃ │ #setLocalValue ( place ( ... local: local ( 7 ) , projection: .ProjectionElems ) +┃ │ function: main +┃ │ span: 54 +┃ │ +┃ │ (2 steps) +┃ └─ 8 (vacuous, leaf) +┃ operandCopy ( place ( ... local: local ( 5 ) , projection: projectionElemField ( +┃ function: main +┃ span: 54 +┃ +┣━━┓ +┃ │ +┃ ├─ 6 +┃ │ #setLocalValue ( place ( ... local: local ( 7 ) , projection: .ProjectionElems ) +┃ │ function: main +┃ │ span: 54 +┃ │ +┃ │ (1 step) +┃ └─ 9 (vacuous, leaf) +┃ #evalUnion ( rvalueUse ( operandCopy ( place ( ... local: local ( 5 ) , projecti +┃ function: main +┃ span: 54 +┃ +┗━━┓ + │ + └─ 7 (stuck, leaf) + #execStmt ( statement ( ... kind: statementKindAssign ( ... place: place ( ... l + function: main + span: 64 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/subslice-drop-unsupported-fail.rs b/kmir/src/tests/integration/data/prove-rs/subslice-drop-unsupported-fail.rs new file mode 100644 index 000000000..8fc64049b --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/subslice-drop-unsupported-fail.rs @@ -0,0 +1,21 @@ +// Reproducer: Subslice projection on an array of Drop types. +// +// `let [first, rest @ ..] = arr` generates a Subslice projection that +// changes the type from [Droppable; 3] to [Droppable; 2]. The SMIR +// linker's _projected_ty() currently returns the original array type +// for Subslice, which could cause drop-glue mis-resolution when +// Subslice projections appear in Drop terminator places. + +struct Droppable(u8); + +impl Drop for Droppable { + fn drop(&mut self) {} +} + +fn main() { + let arr = [Droppable(1), Droppable(2), Droppable(3)]; + let [first, rest @ ..] = arr; + assert!(first.0 == 1); + assert!(rest[0].0 == 2); + assert!(rest[1].0 == 3); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 1e16f53e3..3e8f17019 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -70,6 +70,7 @@ 'ptr-cast-array-to-nested-wrapper-fail', 'ptr-cast-array-to-singleton-wrapped-array-fail', 'iterator-simple-fail', + 'subslice-drop-unsupported-fail', ] From 662427fc4e8b5c1713c995782f4c424845ec2fcd Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 17:10:08 +0800 Subject: [PATCH 24/26] Revert data.md changes, restore iterator-simple as passing Revert the experimental removal of bridge rules, consP HACK rule, and removeIndexTail. These are workarounds for a deeper design issue in how #typeProjection interacts with PointerOffset for slice-to-slice PtrToPtr casts (tracked in #1011), and removing them without the proper fix causes regressions. Restore iterator-simple.rs as a passing test. --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 33 ++++++++++++++++++- ...ator-simple-fail.rs => iterator-simple.rs} | 0 .../show/iterator-simple-fail.main.expected | 15 --------- .../src/tests/integration/test_integration.py | 1 - 4 files changed, 32 insertions(+), 17 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{iterator-simple-fail.rs => iterator-simple.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 677f917d1..6437adb66 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -384,6 +384,9 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr rule consP(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) PS:ProjectionElems) => PS [priority(40)] // this rule is not valid if the original pointee has more than one field // rule consP(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct PS:ProjectionElems) => PS [priority(40)] + // HACK: special rule which munges together constant-indexing and offset projections + rule consP( projectionElemConstantIndex(I, 0, false), PointerOffset(OFF, _SIZE) PS) => projectionElemConstantIndex(I +Int OFF, 0, false) PS [priority(40)] + // requires I +Int OFF < _SIZE // _SIZE is metadataSize, needs a < operation for this to work rule consP(projectionElemToZST, projectionElemFromZST PS:ProjectionElems) => PS [priority(40)] rule consP(projectionElemFromZST, projectionElemToZST PS:ProjectionElems) => PS [priority(40)] @@ -506,6 +509,16 @@ The following rule resolves this situation by using the head element. => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? [preserves-definedness, priority(100)] + // Temporary bridge rule: after PointerOffset lifts a single value to Range(ListItem(...)), + // unwrap a Union head element so the existing Union + Field rules below can keep running. + rule #traverseProjection( + DEST, + Range(ListItem(Union(_, _) #as VALUE) _REST:List), + projectionElemField(IDX, TY) PROJS, + CTXTS + ) + => #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... // TODO mark context? + [preserves-definedness, priority(100)] ``` #### Unions @@ -647,6 +660,24 @@ Similar to `ConstantIndex`, the slice _end_ index may count from the _end_ or t andBool START <=Int size(ELEMENTS) -Int END [preserves-definedness] // Indexes checked to be in range for ELEMENTS + // Temporary bridge rule: PointerOffset is implemented below in terms of Range slicing, so + // lift a single non-Range value to Range(ListItem(...)) to reuse that shared path. + rule #traverseProjection( + DEST, + VAL, + PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, + CTXTS + ) + => #traverseProjection( + DEST, + Range(ListItem(VAL)), + PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS, + CTXTS + ) + ... + + requires notBool isRange(VAL) + [preserves-definedness, priority(100)] rule #traverseProjection( DEST, @@ -1110,7 +1141,7 @@ and an array of the indeicated size gets reconstructed if the provided metadata rule ListItem(PtrLocal(OFFSET, place(LOCAL, PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) ListItem(Integer(LENGTH, 64, false)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT)) - => PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE)) + => PtrLocal(OFFSET, place(LOCAL, removeIndexTail(PROJS)), MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE)) ... // requires LENGTH +Int PTR_OFFSET <=Int ORIGIN_SIZE // refuse to create an invalid fat pointer diff --git a/kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs b/kmir/src/tests/integration/data/prove-rs/iterator-simple.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs rename to kmir/src/tests/integration/data/prove-rs/iterator-simple.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected deleted file mode 100644 index 772d0689f..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (1069 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toStack ( 3 , local ( 3 ) ) , Integer ( 1 , 32 , true ) , - span: 106 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 3e8f17019..ca787cd56 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -69,7 +69,6 @@ 'ptr-cast-array-to-wrapper-fail', 'ptr-cast-array-to-nested-wrapper-fail', 'ptr-cast-array-to-singleton-wrapped-array-fail', - 'iterator-simple-fail', 'subslice-drop-unsupported-fail', ] From 8a59eed2738374a16ff8f9850cd34fa525d824de Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 17:11:42 +0800 Subject: [PATCH 25/26] test(smir): reproduce _projected_ty Subslice drop-glue pruning bug MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add unit test demonstrating that _projected_ty() returns the original array type for Subslice projections, causing call_edges to miss the drop_in_place::<[T; M]> edge and reduce_to() to incorrectly prune the required drop glue. Add integration test subslice-drop-partial-move.rs that generates Drop(arr.Subslice(1,3,false)) in the MIR — the exact pattern described in the Codex review comment. --- .../prove-rs/subslice-drop-partial-move.rs | 20 + .../subslice-drop-partial-move.smir.json | 3947 +++++++++++++++++ kmir/src/tests/unit/test_smir.py | 25 + 3 files changed, 3992 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.smir.json diff --git a/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs b/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs new file mode 100644 index 000000000..865280380 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs @@ -0,0 +1,20 @@ +// Subslice projection in a Drop terminator's place. +// +// `let [first, ..] = arr` moves only `first`; the remaining elements +// are dropped in place via Drop(arr.Subslice(1, 3, false)). +// This exercises _projected_ty() resolving the Subslice to the correct +// [Droppable; 2] type so reduce_to() preserves the drop glue. + +struct Droppable(u8); + +impl Drop for Droppable { + fn drop(&mut self) {} +} + +fn consume(_: Droppable) {} + +fn main() { + let arr = [Droppable(1), Droppable(2), Droppable(3)]; + let [first, ..] = arr; + consume(first); +} diff --git a/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.smir.json b/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.smir.json new file mode 100644 index 000000000..331cb5610 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.smir.json @@ -0,0 +1,3947 @@ +{ + "name": "subslice_drop_partial_move", + "crate_id": 1593102877006753471, + "allocs": [], + "functions": [ + [ + 19, + { + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h5429b4bd6d7831c6E" + } + ], + [ + 21, + { + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h951606607a3c270bE" + } + ], + [ + 14, + { + "NormalSym": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17hcac5317c4662e54fE" + } + ], + [ + 20, + { + "IntrinsicSym": "black_box" + } + ], + [ + 32, + { + "NormalSym": "_ZN26subslice_drop_partial_move7consume17hb3fdcddec7d10a15E" + } + ], + [ + 13, + { + "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17hb9b2b1aac1c9eeeaE" + } + ], + [ + 23, + { + "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17ha2d061d484c47fd0E" + } + ], + [ + 0, + { + "NormalSym": "_ZN3std2rt19lang_start_internal17h035df9ff6960926aE" + } + ], + [ + 25, + { + "NormalSym": "_ZN79_$LT$subslice_drop_partial_move..Droppable$u20$as$u20$core..ops..drop..Drop$GT$4drop17hab506f0b70c8ba6eE" + } + ], + [ + 37, + { + "NormalSym": "_ZN4core3ptr58drop_in_place$LT$subslice_drop_partial_move..Droppable$GT$17hfba90f215f9aa0fdE" + } + ], + [ + 36, + { + "NormalSym": "_ZN4core3ptr79drop_in_place$LT$$u5b$subslice_drop_partial_move..Droppable$u3b$$u20$2$u5d$$GT$17haa85988f30869bfeE" + } + ], + [ + 34, + { + "NoOpSym": "" + } + ] + ], + "uneval_consts": [], + "items": [ + { + "symbol_name": "_ZN26subslice_drop_partial_move4main17hdd89e6d07b7fd929E", + "mono_item_kind": { + "MonoItemFn": { + "name": "main", + "id": 8, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 2, + "projection": [] + }, + { + "Aggregate": [ + { + "Adt": [ + 9, + 0, + [], + null, + null + ] + }, + [ + { + "Constant": { + "span": 61, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 1 + ], + "provenance": { + "ptrs": [] + }, + "align": 1, + "mutability": "Mut" + } + }, + "ty": 9, + "id": 14 + } + } + } + ] + ] + } + ] + }, + "span": 62 + }, + { + "kind": { + "Assign": [ + { + "local": 3, + "projection": [] + }, + { + "Aggregate": [ + { + "Adt": [ + 9, + 0, + [], + null, + null + ] + }, + [ + { + "Constant": { + "span": 63, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 2 + ], + "provenance": { + "ptrs": [] + }, + "align": 1, + "mutability": "Mut" + } + }, + "ty": 9, + "id": 15 + } + } + } + ] + ] + } + ] + }, + "span": 64 + }, + { + "kind": { + "Assign": [ + { + "local": 4, + "projection": [] + }, + { + "Aggregate": [ + { + "Adt": [ + 9, + 0, + [], + null, + null + ] + }, + [ + { + "Constant": { + "span": 65, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 3 + ], + "provenance": { + "ptrs": [] + }, + "align": 1, + "mutability": "Mut" + } + }, + "ty": 9, + "id": 16 + } + } + } + ] + ] + } + ] + }, + "span": 66 + }, + { + "kind": { + "Assign": [ + { + "local": 1, + "projection": [] + }, + { + "Aggregate": [ + { + "Array": 31 + }, + [ + { + "Move": { + "local": 2, + "projection": [] + } + }, + { + "Move": { + "local": 3, + "projection": [] + } + }, + { + "Move": { + "local": 4, + "projection": [] + } + } + ] + ] + } + ] + }, + "span": 67 + }, + { + "kind": { + "Assign": [ + { + "local": 5, + "projection": [] + }, + { + "Use": { + "Move": { + "local": 1, + "projection": [ + { + "ConstantIndex": { + "offset": 0, + "min_length": 3, + "from_end": false + } + } + ] + } + } + } + ] + }, + "span": 68 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 59, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 32, + "id": 13 + } + } + }, + "args": [ + { + "Move": { + "local": 5, + "projection": [] + } + } + ], + "destination": { + "local": 6, + "projection": [] + }, + "target": 1, + "unwind": { + "Cleanup": 2 + } + } + }, + "span": 60 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 1, + "projection": [ + { + "Subslice": { + "from": 1, + "to": 3, + "from_end": false + } + } + ] + }, + "target": 4, + "unwind": "Continue" + } + }, + "span": 69 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 1, + "projection": [ + { + "Subslice": { + "from": 1, + "to": 3, + "from_end": false + } + } + ] + }, + "target": 3, + "unwind": "Terminate" + } + }, + "span": 69 + } + }, + { + "statements": [], + "terminator": { + "kind": "Resume", + "span": 70 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 71 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 72, + "mutability": "Mut" + }, + { + "ty": 33, + "span": 73, + "mutability": "Not" + }, + { + "ty": 31, + "span": 62, + "mutability": "Mut" + }, + { + "ty": 31, + "span": 64, + "mutability": "Mut" + }, + { + "ty": 31, + "span": 66, + "mutability": "Mut" + }, + { + "ty": 31, + "span": 68, + "mutability": "Not" + }, + { + "ty": 1, + "span": 60, + "mutability": "Not" + } + ], + "arg_count": 0, + "var_debug_info": [ + { + "name": "arr", + "source_info": { + "span": 73, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": null + }, + { + "name": "first", + "source_info": { + "span": 68, + "scope": 2 + }, + "composite": null, + "value": { + "Place": { + "local": 5, + "projection": [] + } + }, + "argument_index": null + } + ], + "spread_arg": null, + "span": 70 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN26subslice_drop_partial_move7consume17hb3fdcddec7d10a15E", + "mono_item_kind": { + "MonoItemFn": { + "name": "consume", + "id": 7, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 1, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 54 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 55 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 56, + "mutability": "Mut" + }, + { + "ty": 31, + "span": 57, + "mutability": "Mut" + } + ], + "arg_count": 1, + "var_debug_info": [], + "spread_arg": null, + "span": 58 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN3std2rt10lang_start17h0b2bcdf1a162b433E", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::rt::lang_start::<()>", + "id": 0, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "StorageLive": 5 + }, + "span": 1 + }, + { + "kind": { + "StorageLive": 6 + }, + "span": 2 + }, + { + "kind": { + "StorageLive": 8 + }, + "span": 3 + }, + { + "kind": { + "Assign": [ + { + "local": 8, + "projection": [] + }, + { + "Aggregate": [ + { + "Closure": [ + 1, + [ + { + "Type": 1 + }, + { + "Type": 2 + }, + { + "Type": 3 + }, + { + "Type": 4 + } + ] + ] + }, + [ + { + "Copy": { + "local": 1, + "projection": [] + } + } + ] + ] + } + ] + }, + "span": 3 + }, + { + "kind": { + "Assign": [ + { + "local": 7, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + "Shared", + { + "local": 8, + "projection": [] + } + ] + } + ] + }, + "span": 2 + }, + { + "kind": { + "Assign": [ + { + "local": 6, + "projection": [] + }, + { + "Cast": [ + { + "PointerCoercion": "Unsize" + }, + { + "Copy": { + "local": 7, + "projection": [] + } + }, + 5 + ] + } + ] + }, + "span": 2 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 0, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 0, + "id": 0 + } + } + }, + "args": [ + { + "Move": { + "local": 6, + "projection": [] + } + }, + { + "Move": { + "local": 2, + "projection": [] + } + }, + { + "Move": { + "local": 3, + "projection": [] + } + }, + { + "Move": { + "local": 4, + "projection": [] + } + } + ], + "destination": { + "local": 5, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 1 + } + }, + { + "statements": [ + { + "kind": { + "StorageDead": 6 + }, + "span": 5 + }, + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 5, + "projection": [ + { + "Downcast": 0 + }, + { + "Field": [ + 0, + 6 + ] + } + ] + } + } + } + ] + }, + "span": 6 + }, + { + "kind": { + "StorageDead": 8 + }, + "span": 7 + }, + { + "kind": { + "StorageDead": 5 + }, + "span": 7 + } + ], + "terminator": { + "kind": "Return", + "span": 4 + } + } + ], + "locals": [ + { + "ty": 6, + "span": 8, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 9, + "mutability": "Not" + }, + { + "ty": 6, + "span": 10, + "mutability": "Not" + }, + { + "ty": 8, + "span": 11, + "mutability": "Not" + }, + { + "ty": 9, + "span": 12, + "mutability": "Not" + }, + { + "ty": 10, + "span": 1, + "mutability": "Mut" + }, + { + "ty": 5, + "span": 2, + "mutability": "Mut" + }, + { + "ty": 11, + "span": 2, + "mutability": "Not" + }, + { + "ty": 12, + "span": 3, + "mutability": "Not" + } + ], + "arg_count": 4, + "var_debug_info": [ + { + "name": "main", + "source_info": { + "span": 9, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": 1 + }, + { + "name": "argc", + "source_info": { + "span": 10, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": 2 + }, + { + "name": "argv", + "source_info": { + "span": 11, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 3, + "projection": [] + } + }, + "argument_index": 3 + }, + { + "name": "sigpipe", + "source_info": { + "span": 12, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 4, + "projection": [] + } + }, + "argument_index": 4 + }, + { + "name": "v", + "source_info": { + "span": 6, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 0, + "projection": [] + } + }, + "argument_index": null + } + ], + "spread_arg": null, + "span": 13 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17ha2d061d484c47fd0E", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::rt::lang_start::<()>::{closure#0}", + "id": 1, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "StorageLive": 2 + }, + "span": 16 + }, + { + "kind": { + "StorageLive": 3 + }, + "span": 15 + }, + { + "kind": { + "StorageLive": 4 + }, + "span": 17 + }, + { + "kind": { + "Assign": [ + { + "local": 4, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 1, + "projection": [ + "Deref", + { + "Field": [ + 0, + 7 + ] + } + ] + } + } + } + ] + }, + "span": 17 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 14, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 13, + "id": 1 + } + } + }, + "args": [ + { + "Move": { + "local": 4, + "projection": [] + } + } + ], + "destination": { + "local": 3, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 15 + } + }, + { + "statements": [ + { + "kind": { + "StorageDead": 4 + }, + "span": 19 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 18, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 14, + "id": 2 + } + } + }, + "args": [ + { + "Move": { + "local": 3, + "projection": [] + } + } + ], + "destination": { + "local": 2, + "projection": [] + }, + "target": 2, + "unwind": "Continue" + } + }, + "span": 16 + } + }, + { + "statements": [ + { + "kind": { + "StorageDead": 3 + }, + "span": 21 + }, + { + "kind": { + "StorageLive": 5 + }, + "span": 22 + }, + { + "kind": { + "Assign": [ + { + "local": 5, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + "Shared", + { + "local": 2, + "projection": [ + { + "Field": [ + 0, + 15 + ] + } + ] + } + ] + } + ] + }, + "span": 22 + }, + { + "kind": { + "StorageLive": 6 + }, + "span": 23 + }, + { + "kind": { + "Assign": [ + { + "local": 6, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 2, + "projection": [ + { + "Field": [ + 0, + 15 + ] + }, + { + "Field": [ + 0, + 9 + ] + } + ] + } + } + } + ] + }, + "span": 23 + }, + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Cast": [ + "IntToInt", + { + "Move": { + "local": 6, + "projection": [] + } + }, + 16 + ] + } + ] + }, + "span": 24 + }, + { + "kind": { + "StorageDead": 6 + }, + "span": 25 + }, + { + "kind": { + "StorageDead": 5 + }, + "span": 26 + }, + { + "kind": { + "StorageDead": 2 + }, + "span": 27 + } + ], + "terminator": { + "kind": "Return", + "span": 20 + } + } + ], + "locals": [ + { + "ty": 16, + "span": 28, + "mutability": "Mut" + }, + { + "ty": 11, + "span": 3, + "mutability": "Mut" + }, + { + "ty": 17, + "span": 16, + "mutability": "Mut" + }, + { + "ty": 1, + "span": 15, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 17, + "mutability": "Mut" + }, + { + "ty": 18, + "span": 22, + "mutability": "Mut" + }, + { + "ty": 9, + "span": 23, + "mutability": "Mut" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "main", + "source_info": { + "span": 9, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [ + "Deref", + { + "Field": [ + 0, + 7 + ] + } + ] + } + }, + "argument_index": null + }, + { + "name": "self", + "source_info": { + "span": 29, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": 1 + }, + { + "name": "self", + "source_info": { + "span": 30, + "scope": 2 + }, + "composite": null, + "value": { + "Place": { + "local": 5, + "projection": [] + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 3 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17hb9b2b1aac1c9eeeaE", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::sys::backtrace::__rust_begin_short_backtrace::", + "id": 2, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 31, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 19, + "id": 3 + } + } + }, + "args": [ + { + "Move": { + "local": 1, + "projection": [] + } + }, + { + "Constant": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + } + ], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 33 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 34, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 20, + "id": 5 + } + } + }, + "args": [ + { + "Constant": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + } + ], + "destination": { + "local": 2, + "projection": [] + }, + "target": 2, + "unwind": "Unreachable" + } + }, + "span": 35 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 36 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 37, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 38, + "mutability": "Not" + }, + { + "ty": 1, + "span": 39, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "f", + "source_info": { + "span": 38, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": 1 + }, + { + "name": "result", + "source_info": { + "span": 40, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 0, + "projection": [] + } + }, + "argument_index": null + }, + { + "name": "dummy", + "source_info": { + "span": 41, + "scope": 2 + }, + "composite": null, + "value": { + "Const": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 42 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h86839951c2096b4aE", + "mono_item_kind": { + "MonoItemFn": { + "name": "<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once", + "id": 3, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 43, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 21, + "id": 6 + } + } + }, + "args": [ + { + "Move": { + "local": 1, + "projection": [ + "Deref" + ] + } + }, + { + "Move": { + "local": 2, + "projection": [] + } + } + ], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 43 + } + } + ], + "locals": [ + { + "ty": 16, + "span": 43, + "mutability": "Mut" + }, + { + "ty": 22, + "span": 43, + "mutability": "Not" + }, + { + "ty": 1, + "span": 43, + "mutability": "Not" + } + ], + "arg_count": 2, + "var_debug_info": [], + "spread_arg": 2, + "span": 43 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ops8function6FnOnce9call_once17h5429b4bd6d7831c6E", + "mono_item_kind": { + "MonoItemFn": { + "name": ">::call_once", + "id": 3, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Move": { + "local": 1, + "projection": [] + } + }, + "args": [], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 43 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 43, + "mutability": "Mut" + }, + { + "ty": 7, + "span": 43, + "mutability": "Not" + }, + { + "ty": 1, + "span": 43, + "mutability": "Not" + } + ], + "arg_count": 2, + "var_debug_info": [], + "spread_arg": 2, + "span": 43 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ops8function6FnOnce9call_once17h951606607a3c270bE", + "mono_item_kind": { + "MonoItemFn": { + "name": "<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once", + "id": 3, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 3, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + { + "Mut": { + "kind": "Default" + } + }, + { + "local": 1, + "projection": [] + } + ] + } + ] + }, + "span": 43 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 43, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 23, + "id": 7 + } + } + }, + "args": [ + { + "Move": { + "local": 3, + "projection": [] + } + }, + { + "Move": { + "local": 2, + "projection": [] + } + } + ], + "destination": { + "local": 0, + "projection": [] + }, + "target": 1, + "unwind": { + "Cleanup": 3 + } + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 1, + "projection": [] + }, + "target": 2, + "unwind": "Continue" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 1, + "projection": [] + }, + "target": 4, + "unwind": "Terminate" + } + }, + "span": 43 + } + }, + { + "statements": [], + "terminator": { + "kind": "Resume", + "span": 43 + } + } + ], + "locals": [ + { + "ty": 16, + "span": 43, + "mutability": "Mut" + }, + { + "ty": 12, + "span": 43, + "mutability": "Not" + }, + { + "ty": 1, + "span": 43, + "mutability": "Not" + }, + { + "ty": 24, + "span": 43, + "mutability": "Not" + } + ], + "arg_count": 2, + "var_debug_info": [], + "spread_arg": 2, + "span": 43 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ptr58drop_in_place$LT$subslice_drop_partial_move..Droppable$GT$17hfba90f215f9aa0fdE", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::ptr::drop_in_place::", + "id": 4, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 2, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + { + "Mut": { + "kind": "Default" + } + }, + { + "local": 1, + "projection": [ + "Deref" + ] + } + ] + } + ] + }, + "span": 44 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 44, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 25, + "id": 8 + } + } + }, + "args": [ + { + "Move": { + "local": 2, + "projection": [] + } + } + ], + "destination": { + "local": 3, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 44 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 44 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 26, + "span": 44, + "mutability": "Not" + }, + { + "ty": 27, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 1, + "span": 44, + "mutability": "Mut" + } + ], + "arg_count": 1, + "var_debug_info": [], + "spread_arg": null, + "span": 44 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ptr79drop_in_place$LT$$u5b$subslice_drop_partial_move..Droppable$u3b$$u20$2$u5d$$GT$17haa85988f30869bfeE", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::ptr::drop_in_place::<[Droppable; 2]>", + "id": 4, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 2, + "projection": [] + }, + { + "Use": { + "Constant": { + "span": 32, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + }, + "ty": 28, + "id": 9 + } + } + } + } + ] + }, + "span": 44 + }, + { + "kind": { + "Assign": [ + { + "local": 3, + "projection": [] + }, + { + "Use": { + "Constant": { + "span": 44, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + }, + "ty": 28, + "id": 10 + } + } + } + } + ] + }, + "span": 44 + } + ], + "terminator": { + "kind": { + "Goto": { + "target": 6 + } + }, + "span": 44 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 44 + } + }, + { + "statements": [], + "terminator": { + "kind": "Resume", + "span": 44 + } + }, + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 4, + "projection": [] + }, + { + "AddressOf": [ + "Mut", + { + "local": 1, + "projection": [ + "Deref", + { + "Index": 3 + } + ] + } + ] + } + ] + }, + "span": 44 + }, + { + "kind": { + "Assign": [ + { + "local": 3, + "projection": [] + }, + { + "BinaryOp": [ + "Add", + { + "Move": { + "local": 3, + "projection": [] + } + }, + { + "Constant": { + "span": 44, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + }, + "ty": 28, + "id": 11 + } + } + } + ] + } + ] + }, + "span": 44 + } + ], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 4, + "projection": [ + "Deref" + ] + }, + "target": 4, + "unwind": "Terminate" + } + }, + "span": 44 + } + }, + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 5, + "projection": [] + }, + { + "BinaryOp": [ + "Eq", + { + "Copy": { + "local": 3, + "projection": [] + } + }, + { + "Copy": { + "local": 2, + "projection": [] + } + } + ] + } + ] + }, + "span": 44 + } + ], + "terminator": { + "kind": { + "SwitchInt": { + "discr": { + "Move": { + "local": 5, + "projection": [] + } + }, + "targets": { + "branches": [ + [ + 0, + 3 + ] + ], + "otherwise": 2 + } + } + }, + "span": 44 + } + }, + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 6, + "projection": [] + }, + { + "AddressOf": [ + "Mut", + { + "local": 1, + "projection": [ + "Deref", + { + "Index": 3 + } + ] + } + ] + } + ] + }, + "span": 44 + }, + { + "kind": { + "Assign": [ + { + "local": 3, + "projection": [] + }, + { + "BinaryOp": [ + "Add", + { + "Move": { + "local": 3, + "projection": [] + } + }, + { + "Constant": { + "span": 44, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + }, + "ty": 28, + "id": 11 + } + } + } + ] + } + ] + }, + "span": 44 + } + ], + "terminator": { + "kind": { + "Drop": { + "place": { + "local": 6, + "projection": [ + "Deref" + ] + }, + "target": 6, + "unwind": { + "Cleanup": 4 + } + } + }, + "span": 44 + } + }, + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 7, + "projection": [] + }, + { + "BinaryOp": [ + "Eq", + { + "Copy": { + "local": 3, + "projection": [] + } + }, + { + "Copy": { + "local": 2, + "projection": [] + } + } + ] + } + ] + }, + "span": 44 + } + ], + "terminator": { + "kind": { + "SwitchInt": { + "discr": { + "Move": { + "local": 7, + "projection": [] + } + }, + "targets": { + "branches": [ + [ + 0, + 5 + ] + ], + "otherwise": 1 + } + } + }, + "span": 44 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 29, + "span": 44, + "mutability": "Not" + }, + { + "ty": 28, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 28, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 26, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 30, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 26, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 30, + "span": 44, + "mutability": "Mut" + } + ], + "arg_count": 1, + "var_debug_info": [], + "spread_arg": null, + "span": 44 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17hc0001c2b0229352cE", + "mono_item_kind": { + "MonoItemFn": { + "name": "std::ptr::drop_in_place::<{closure@std::rt::lang_start<()>::{closure#0}}>", + "id": 4, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 44 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 44, + "mutability": "Mut" + }, + { + "ty": 22, + "span": 44, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [], + "spread_arg": null, + "span": 44 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17hcac5317c4662e54fE", + "mono_item_kind": { + "MonoItemFn": { + "name": "<() as std::process::Termination>::report", + "id": 5, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Use": { + "Constant": { + "span": 46, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 1, + "mutability": "Mut" + } + }, + "ty": 17, + "id": 12 + } + } + } + } + ] + }, + "span": 46 + } + ], + "terminator": { + "kind": "Return", + "span": 45 + } + } + ], + "locals": [ + { + "ty": 17, + "span": 47, + "mutability": "Mut" + }, + { + "ty": 1, + "span": 48, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "self", + "source_info": { + "span": 48, + "scope": 0 + }, + "composite": null, + "value": { + "Const": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 1, + "id": 4 + } + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 49 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN79_$LT$subslice_drop_partial_move..Droppable$u20$as$u20$core..ops..drop..Drop$GT$4drop17hab506f0b70c8ba6eE", + "mono_item_kind": { + "MonoItemFn": { + "name": "::drop", + "id": 6, + "body": { + "blocks": [ + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 50 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 51, + "mutability": "Mut" + }, + { + "ty": 27, + "span": 52, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "self", + "source_info": { + "span": 52, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 53 + } + } + }, + "details": null + } + ], + "types": [ + [ + 40, + "VoidType" + ], + [ + 5, + { + "RefType": { + "pointee_type": 38, + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + }, + { + "num_bits": 64 + } + ] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "ScalarPair": [ + { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 1, + "end": 18446744073709551615 + } + } + }, + { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 1, + "end": 18446744073709551615 + } + } + } + ] + }, + "abi_align": 8, + "size": { + "num_bits": 128 + } + }, + "mutability": "Not" + } + } + ], + [ + 27, + { + "RefType": { + "pointee_type": 31, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 1, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Mut" + } + } + ], + [ + 24, + { + "RefType": { + "pointee_type": 12, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 1, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Mut" + } + } + ], + [ + 18, + { + "RefType": { + "pointee_type": 15, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 1, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Not" + } + } + ], + [ + 11, + { + "RefType": { + "pointee_type": 12, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 1, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Not" + } + } + ], + [ + 1, + { + "TupleType": { + "types": [], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 0 + } + } + } + } + ], + [ + 8, + { + "PtrType": { + "pointee_type": 39, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 0, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Not" + } + } + ], + [ + 39, + { + "PtrType": { + "pointee_type": 9, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 0, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Not" + } + } + ], + [ + 26, + { + "PtrType": { + "pointee_type": 31, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 0, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Mut" + } + } + ], + [ + 29, + { + "PtrType": { + "pointee_type": 35, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 0, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Mut" + } + } + ], + [ + 22, + { + "PtrType": { + "pointee_type": 12, + "layout": { + "fields": "Primitive", + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Pointer": 0 + }, + "valid_range": { + "start": 0, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + }, + "mutability": "Mut" + } + } + ], + [ + 31, + { + "StructType": { + "name": "Droppable", + "adt_def": 9, + "fields": [ + 9 + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + } + ] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": false + } + }, + "valid_range": { + "start": 0, + "end": 255 + } + } + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + } + } + ], + [ + 35, + { + "ArrayType": { + "elem_type": 31, + "size": { + "kind": { + "Value": [ + 28, + { + "bytes": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + ] + }, + "id": 1 + }, + "layout": { + "fields": { + "Array": { + "stride": { + "num_bits": 8 + }, + "count": 2 + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 16 + } + } + } + } + ], + [ + 33, + { + "ArrayType": { + "elem_type": 31, + "size": { + "kind": { + "Value": [ + 28, + { + "bytes": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 8, + "mutability": "Mut" + } + ] + }, + "id": 0 + }, + "layout": { + "fields": { + "Array": { + "stride": { + "num_bits": 8 + }, + "count": 3 + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 24 + } + } + } + } + ], + [ + 30, + { + "PrimitiveType": "Bool" + } + ], + [ + 38, + { + "DynType": { + "name": "dyn std::ops::Fn() -> i32 + std::marker::Sync + std::panic::RefUnwindSafe", + "layout": { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Aggregate": { + "sized": false + } + }, + "abi_align": 1, + "size": { + "num_bits": 0 + } + } + } + } + ], + [ + 16, + { + "PrimitiveType": { + "Int": "I32" + } + } + ], + [ + 6, + { + "PrimitiveType": { + "Int": "Isize" + } + } + ], + [ + 17, + { + "StructType": { + "name": "std::process::ExitCode", + "adt_def": 12, + "fields": [ + 15 + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + } + ] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": false + } + }, + "valid_range": { + "start": 0, + "end": 255 + } + } + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + } + } + ], + [ + 10, + { + "EnumType": { + "name": "std::result::Result", + "adt_def": 21, + "discriminants": [ + 0, + 1 + ], + "fields": [ + [ + 6 + ], + [ + 40 + ] + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + } + ] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Int": { + "length": "I64", + "signed": true + } + }, + "valid_range": { + "start": 0, + "end": 18446744073709551615 + } + } + } + }, + "abi_align": 8, + "size": { + "num_bits": 64 + } + } + } + } + ], + [ + 15, + { + "StructType": { + "name": "std::sys::pal::unix::process::process_common::ExitCode", + "adt_def": 14, + "fields": [ + 9 + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + } + ] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": false + } + }, + "valid_range": { + "start": 0, + "end": 255 + } + } + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + } + } + ], + [ + 9, + { + "PrimitiveType": { + "Uint": "U8" + } + } + ], + [ + 28, + { + "PrimitiveType": { + "Uint": "Usize" + } + } + ], + [ + 12, + { + "FunType": "{closure@std::rt::lang_start<()>::{closure#0}}" + } + ] + ], + "spans": [ + [ + 41, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/hint.rs", + 388, + 27, + 388, + 32 + ] + ], + [ + 34, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/hint.rs", + 389, + 5, + 389, + 33 + ] + ], + [ + 35, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/hint.rs", + 389, + 5, + 389, + 40 + ] + ], + [ + 43, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ops/function.rs", + 250, + 5, + 250, + 71 + ] + ], + [ + 44, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs", + 521, + 1, + 521, + 56 + ] + ], + [ + 29, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/process.rs", + 2052, + 19, + 2052, + 23 + ] + ], + [ + 22, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/process.rs", + 2053, + 9, + 2053, + 15 + ] + ], + [ + 26, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/process.rs", + 2053, + 23, + 2053, + 24 + ] + ], + [ + 49, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/process.rs", + 2422, + 5, + 2424, + 6 + ] + ], + [ + 48, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/process.rs", + 2422, + 15, + 2422, + 19 + ] + ], + [ + 46, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/process.rs", + 2423, + 9, + 2423, + 26 + ] + ], + [ + 45, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/process.rs", + 2424, + 6, + 2424, + 6 + ] + ], + [ + 13, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 188, + 1, + 201, + 2 + ] + ], + [ + 9, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 189, + 5, + 189, + 9 + ] + ], + [ + 10, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 190, + 5, + 190, + 9 + ] + ], + [ + 11, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 191, + 5, + 191, + 9 + ] + ], + [ + 12, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 192, + 5, + 192, + 12 + ] + ], + [ + 6, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 194, + 12, + 194, + 13 + ] + ], + [ + 0, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 194, + 17, + 194, + 36 + ] + ], + [ + 1, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 194, + 17, + 199, + 6 + ] + ], + [ + 2, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 9, + 195, + 93 + ] + ], + [ + 3, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 10, + 195, + 93 + ] + ], + [ + 14, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 18, + 195, + 69 + ] + ], + [ + 15, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 18, + 195, + 75 + ] + ], + [ + 16, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 18, + 195, + 84 + ] + ], + [ + 17, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 70, + 195, + 74 + ] + ], + [ + 19, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 74, + 195, + 75 + ] + ], + [ + 18, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 76, + 195, + 82 + ] + ], + [ + 21, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 83, + 195, + 84 + ] + ], + [ + 27, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 92, + 195, + 93 + ] + ], + [ + 20, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 93, + 195, + 93 + ] + ], + [ + 5, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 199, + 5, + 199, + 6 + ] + ], + [ + 7, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 199, + 6, + 199, + 7 + ] + ], + [ + 4, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/rt.rs", + 201, + 2, + 201, + 2 + ] + ], + [ + 42, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 150, + 1, + 160, + 2 + ] + ], + [ + 38, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 150, + 43, + 150, + 44 + ] + ], + [ + 40, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 154, + 9, + 154, + 15 + ] + ], + [ + 31, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 154, + 18, + 154, + 19 + ] + ], + [ + 33, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 154, + 18, + 154, + 21 + ] + ], + [ + 36, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 160, + 2, + 160, + 2 + ] + ], + [ + 30, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 635, + 19, + 635, + 24 + ] + ], + [ + 23, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 636, + 9, + 636, + 15 + ] + ], + [ + 24, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 636, + 9, + 636, + 22 + ] + ], + [ + 25, + [ + "/Users/steven/.rustup/toolchains/nightly-2024-11-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 636, + 21, + 636, + 22 + ] + ], + [ + 53, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 11, + 5, + 11, + 26 + ] + ], + [ + 52, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 11, + 13, + 11, + 22 + ] + ], + [ + 50, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 11, + 26, + 11, + 26 + ] + ], + [ + 58, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 14, + 1, + 14, + 28 + ] + ], + [ + 54, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 14, + 27, + 14, + 28 + ] + ], + [ + 55, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 14, + 28, + 14, + 28 + ] + ], + [ + 70, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 16, + 1, + 20, + 2 + ] + ], + [ + 73, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 9, + 17, + 12 + ] + ], + [ + 67, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 15, + 17, + 57 + ] + ], + [ + 62, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 16, + 17, + 28 + ] + ], + [ + 61, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 26, + 17, + 27 + ] + ], + [ + 64, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 30, + 17, + 42 + ] + ], + [ + 63, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 40, + 17, + 41 + ] + ], + [ + 66, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 44, + 17, + 56 + ] + ], + [ + 65, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 17, + 54, + 17, + 55 + ] + ], + [ + 68, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 18, + 10, + 18, + 15 + ] + ], + [ + 59, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 19, + 5, + 19, + 12 + ] + ], + [ + 60, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 19, + 5, + 19, + 19 + ] + ], + [ + 69, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 20, + 1, + 20, + 2 + ] + ], + [ + 71, + [ + "/Users/steven/Desktop/projs/mir-semantics/.claude/worktrees/upstream-pr-999/kmir/src/tests/integration/data/prove-rs/subslice-drop-partial-move.rs", + 20, + 2, + 20, + 2 + ] + ], + [ + 32, + [ + "no-location", + 0, + 0, + 0, + 0 + ] + ] + ], + "debug": null, + "machine": { + "endian": "Little", + "pointer_width": { + "num_bits": 64 + } + } +} diff --git a/kmir/src/tests/unit/test_smir.py b/kmir/src/tests/unit/test_smir.py index 32cbf8358..2c30336fd 100644 --- a/kmir/src/tests/unit/test_smir.py +++ b/kmir/src/tests/unit/test_smir.py @@ -258,3 +258,28 @@ def test_drop_function_tys_accept_core_drop_in_place_names() -> None: ) assert smir_info.drop_function_tys == {2: 12} + + +PROVE_DATA_DIR = Path(__file__).parent.parent / 'integration' / 'data' / 'prove-rs' +SUBSLICE_SMIR_FILE = PROVE_DATA_DIR / 'subslice-drop-partial-move.smir.json' + +DROP_IN_PLACE_DROPPABLE_2 = ( + '_ZN4core3ptr79drop_in_place' + '$LT$$u5b$subslice_drop_partial_move..Droppable$u3b$$u20$2$u5d$$GT$' + '17haa85988f30869bfeE' +) + + +def test_reduce_to_preserves_subslice_drop_glue() -> None: + # Generated from subslice-drop-partial-move.rs: + # let arr = [Droppable(1), Droppable(2), Droppable(3)]; + # let [first, ..] = arr; + # consume(first); + # + # The compiler emits Drop(arr.Subslice(1, 3, false)) to drop the + # remaining [Droppable; 2]. _projected_ty() must resolve the + # Subslice to [Droppable; 2] so reduce_to('main') keeps + # drop_in_place::<[Droppable; 2]>. + smir_info = SMIRInfo.from_file(SUBSLICE_SMIR_FILE) + reduced = smir_info.reduce_to('main') + assert DROP_IN_PLACE_DROPPABLE_2 in reduced.items From 7fb84c93e298c94e6c34091ad2850d527455a7c3 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 16 Apr 2026 17:11:49 +0800 Subject: [PATCH 26/26] fix(smir): resolve Subslice projection to correct array type _projected_ty() returned the original array type for Subslice projections, so call_edges missed drop glue for subslice drops like Drop(local.Subslice(1,3,false)) and reduce_to() pruned the required drop_in_place::<[T; M]> function. Compute the result array length from the Subslice parameters (to - from for from_end=false, len - from - to for from_end=true) and search the type table for a matching ArrayType with the same element type and length. --- kmir/src/kmir/smir.py | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 0544fe9e6..11da3cc9f 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -353,6 +353,30 @@ def _projected_ty(self, ty: Ty, projection: object) -> Ty | None: return Ty(type_info.element_type) if 'Subslice' in projection and isinstance(type_info, ArrayT): + sub = projection['Subslice'] + from_idx = sub.get('from', 0) + to_idx = sub.get('to', 0) + from_end = sub.get('from_end', False) + + if from_end: + # [from .. len-to]: result length depends on runtime size + if type_info.length is not None: + result_len = type_info.length - from_idx - to_idx + else: + result_len = None + else: + # [from .. to]: result length = to - from + result_len = to_idx - from_idx + + # Search for an ArrayType with matching element type and length + if result_len is not None: + for candidate_ty, candidate_info in self.types.items(): + if ( + isinstance(candidate_info, ArrayT) + and candidate_info.element_type == type_info.element_type + and candidate_info.length == result_len + ): + return candidate_ty return ty if 'OpaqueCast' in projection or 'Subtype' in projection: