From ff019c2d6425f277f76f67f6ade508ff3a9d11e0 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 11:57:41 +0000 Subject: [PATCH 1/6] 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 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 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 a731e4880..13960d47d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -46,7 +46,7 @@ ] PROVE_SHOW_SPECS = [ 'local-raw-fail', - 'interior-mut-fail', + 'interior-mut', 'interior-mut3-fail', 'iter_next_3', 'assert_eq_exp', From 361503043bb458b464e1e0e230081cf405a27540 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Mar 2026 12:00:42 +0000 Subject: [PATCH 2/6] 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 13960d47d..4fb959ccf 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -46,7 +46,6 @@ ] PROVE_SHOW_SPECS = [ 'local-raw-fail', - 'interior-mut', 'interior-mut3-fail', 'iter_next_3', 'assert_eq_exp', From a0621b767e90b00f87a82eff680bb2439959a303 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Mar 2026 00:02:54 +0000 Subject: [PATCH 3/6] 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 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 eb770d6ee1e3ec6f8dbb17834a084b2ba64fb483 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 31 Mar 2026 12:39:36 +0000 Subject: [PATCH 4/6] 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 a363d2676928db358abd60720a1a4e23c453eb22 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 31 Mar 2026 15:27:24 +0000 Subject: [PATCH 5/6] 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 5839521b4..f4b9c45d7 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 dcfd47e76..81642a11e 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -545,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/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 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', ()), + ), + ) From f2ccd0ccfdd6760bb83997e47afca0050257c624 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 1 Apr 2026 09:43:21 +0000 Subject: [PATCH 6/6] 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 ) ) ) ) )