diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 82c28b3f0..fff717dfb 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) @@ -349,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) ~> _ @@ -365,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 @@ -383,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] @@ -474,6 +501,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 +522,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 +704,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/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index fffbf7b35..980c0cd40 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -517,6 +517,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 @@ -658,6 +667,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/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..81642a11e 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -487,6 +487,20 @@ def get_int_arg(app: KInner) -> int: type_equations = _make_stratified_rules(kmir, 'lookupTy', 'Ty', 'TypeInfo', 'ty', type_assocs, invalid_type) + 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', + '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 +515,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]: @@ -531,6 +545,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/kmir/smir.py b/kmir/src/kmir/smir.py index f609a9fe8..9aaa207b8 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,104 @@ 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 | 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 + + 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, 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): + 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/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/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/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/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/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a0486027b..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-fail', 'interior-mut3-fail', 'iter_next_3', 'assert_eq_exp', diff --git a/kmir/src/tests/unit/test_kompile.py b/kmir/src/tests/unit/test_kompile.py index acfab2aee..30fa62c8c 100644 --- a/kmir/src/tests/unit/test_kompile.py +++ b/kmir/src/tests/unit/test_kompile.py @@ -1,8 +1,14 @@ from __future__ import annotations +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 +from kmir.kompile import _add_exists_quantifiers, _collect_evars, _functions +from kmir.smir import SMIRInfo def test_collect_evars() -> None: @@ -37,3 +43,31 @@ def test_add_exists_quantifiers() -> None: assert result.text.count(r'\exists') == 2 assert 'VarA' in result.text assert 'VarB' in result.text + + +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', ()), + ), + ) 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()}