diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 82c28b3f0..9614bd63e 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -219,6 +219,25 @@ 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 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)) ~> _ + => + #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 +368,44 @@ 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] + + syntax KItem ::= #consumeNoOpArgs(Operands, MaybeBasicBlockIdx) + | #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, + // 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) ~> _ + => #consumeNoOpArgs(ARGS, TARGET) + + + rule #consumeNoOpArgs(.Operands, TARGET) => #continueAt(TARGET) ... + + rule #consumeNoOpArgs(OP:Operand MORE:Operands, TARGET) + => #consumeNoOpArg(OP) ~> #consumeNoOpArgs(MORE, TARGET) + ... + + + rule #consumeNoOpArg(operandConstant(_)) => .K ... + + rule #consumeNoOpArg(operandCopy(place(local(I), .ProjectionElems))) => .K ... + LOCALS + requires 0 <=Int I + andBool I #consumeNoOpArg(operandMove(place(local(I), _))) => .K ... + LOCALS => LOCALS[I <- typedValue(Moved, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)] + requires 0 <=Int I + andBool I #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _ @@ -365,6 +422,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 +441,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] @@ -442,6 +501,7 @@ An operand may be a `Reference` (the only way a function could access another fu ```k syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands, Span) + | #setUpDropGlueData(MonoItemKind, Value, Span) // reserve space for local variables and copy/move arguments from old locals into their place rule [setupCalleeData]: #setUpCalleeData( @@ -466,6 +526,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 @@ -669,12 +744,53 @@ 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 [termDrop]: #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 [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" 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 2cc068084..6437adb66 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -508,6 +508,17 @@ 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 @@ -649,6 +660,25 @@ 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, 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 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..905af7874 100644 --- a/kmir/src/kmir/kompile.py +++ b/kmir/src/kmir/kompile.py @@ -513,6 +513,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'),)),) ) @@ -527,7 +541,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]: @@ -557,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/kmir/smir.py b/kmir/src/kmir/smir.py index 1ce7b897b..11da3cc9f 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 @@ -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) @@ -173,6 +174,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(_DROP_IN_PLACE_PREFIXES): + 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 +264,131 @@ 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 '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) + + 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: + 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/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/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); +} 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 deleted file mode 100644 index f1cd9a4d1..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 -│ -│ (798 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - 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-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/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/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 ) ) ) ) ) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d6e891398..ca787cd56 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', @@ -58,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', @@ -71,6 +69,7 @@ 'ptr-cast-array-to-wrapper-fail', 'ptr-cast-array-to-nested-wrapper-fail', 'ptr-cast-array-to-singleton-wrapped-array-fail', + 'subslice-drop-unsupported-fail', ] diff --git a/kmir/src/tests/unit/test_kompile.py b/kmir/src/tests/unit/test_kompile.py index de8366cba..1630a6d99 100644 --- a/kmir/src/tests/unit/test_kompile.py +++ b/kmir/src/tests/unit/test_kompile.py @@ -1,10 +1,15 @@ 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 +115,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', ()), + ), + ) diff --git a/kmir/src/tests/unit/test_smir.py b/kmir/src/tests/unit/test_smir.py index 9be42f87c..2c30336fd 100644 --- a/kmir/src/tests/unit/test_smir.py +++ b/kmir/src/tests/unit/test_smir.py @@ -45,3 +45,241 @@ 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: + # 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', + '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()} + + +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()} + + +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} + + +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