From f9f1bc8b11e937e61de17698f2ed7ae61658c4f3 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 11:57:41 +0000 Subject: [PATCH 1/3] 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 3998cb3eb..d81f5cbf0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -183,6 +183,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 c48fef906..620eaecbd 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -487,6 +487,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'),)),) ) @@ -501,7 +512,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 f609a9fe8..252e72018 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 pathlib import Path @@ -172,6 +172,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']} @@ -225,29 +256,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: Ty, edges: dict[Ty, set[Ty]]) -> set[Ty]: work = deque([start]) 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 a0486027b..59918dc76 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 1af72b82734df9969c85935ae8b8ccd2054ba1b9 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 12:00:42 +0000 Subject: [PATCH 2/3] 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 59918dc76..1882cb52e 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 1da7c3486a708b5e8280695942ff3820ff5b8582 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Mar 2026 00:02:54 +0000 Subject: [PATCH 3/3] 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 620eaecbd..dcfd47e76 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -487,7 +487,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 252e72018..60d073e14 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -297,8 +297,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