diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a3d30ac5d..d588ea32c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1265,15 +1265,78 @@ the `Value` sort. Conversion is especially possible for the case of _Slices_ (of dynamic length) and _Arrays_ (of static length), which have the same representation `Value::Range`. +When the cast crosses transparent wrappers (newtypes that just forward field `0` e.g. `struct Wrapper(T)`), the pointer's +`Place` must be realigned. `#alignTransparentPlace` rewrites the projection list until the source and target +expose the same inner value: +- if the source unwraps more than the target, append an explicit `field(0)` so the target still sees that field; +- if the target unwraps more, strip any redundant tail projections with `#popTransparentTailTo`, leaving the + canonical prefix shared by both sides. + ```k rule #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET) => - PtrLocal(OFFSET, PLACE, MUT, #convertMetadata(META, lookupTy(TY_TARGET))) + PtrLocal( + OFFSET, + #alignTransparentPlace( + PLACE, + #lookupMaybeTy(pointeeTy(lookupTy(TY_SOURCE))), + #lookupMaybeTy(pointeeTy(lookupTy(TY_TARGET))) + ), + MUT, + #convertMetadata(META, lookupTy(TY_TARGET)) + ) ... requires #typesCompatible(lookupTy(TY_SOURCE), lookupTy(TY_TARGET)) [preserves-definedness] // valid map lookups checked + syntax Place ::= #alignTransparentPlace ( Place , TypeInfo , TypeInfo ) [function, total] + syntax ProjectionElems ::= #popTransparentTailTo ( ProjectionElems , TypeInfo ) [function, total] + + rule #alignTransparentPlace(place(LOCAL, PROJS), typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as SOURCE, TARGET) + => #alignTransparentPlace( + place( + LOCAL, + appendP(PROJS, projectionElemField(fieldIdx(0), FIELD_TY) .ProjectionElems) + ), + lookupTy(FIELD_TY), + TARGET + ) + requires #transparentDepth(SOURCE) >Int #transparentDepth(TARGET) + andBool #zeroFieldOffset(LAYOUT) + + rule #alignTransparentPlace( + place(LOCAL, PROJS), + SOURCE, + typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as TARGET + ) + => #alignTransparentPlace( + place(LOCAL, #popTransparentTailTo(PROJS, lookupTy(FIELD_TY))), + SOURCE, + lookupTy(FIELD_TY) + ) + requires #transparentDepth(SOURCE) PLACE [owise] + + rule #popTransparentTailTo( + projectionElemField(fieldIdx(0), FIELD_TY) .ProjectionElems, + TARGET + ) + => .ProjectionElems + requires lookupTy(FIELD_TY) ==K TARGET + + rule #popTransparentTailTo( + X:ProjectionElem REST:ProjectionElems, + TARGET + ) + => X #popTransparentTailTo(REST, TARGET) + requires REST =/=K .ProjectionElems + + rule #popTransparentTailTo(PROJS, _) => PROJS [owise] + syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total] // ------------------------------------------------------------------------------------- ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md index 522df0846..0ac8cff08 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -111,12 +111,6 @@ syntax Int ::= #msBytes ( MachineSize ) [function, total] rule #msBytes(machineSize(mirInt(NBITS))) => NBITS /Int 8 [preserves-definedness] rule #msBytes(machineSize(NBITS)) => NBITS /Int 8 [owise, preserves-definedness] -// Extract field offsets from the struct layout when available (Arbitrary only). -syntax MachineSizes ::= #layoutOffsets ( MaybeLayoutShape ) [function, total] -rule #layoutOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS -rule #layoutOffsets(noLayoutShape) => .MachineSizes -rule #layoutOffsets(_) => .MachineSizes [owise] - // Minimum number of input bytes required to decode all fields by the chosen offsets. // Uses builtin maxInt to compute max(offset + size). The lists of types and // offsets must have the same length; if not, this function returns -1 to signal diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index f0a7c333e..ee42a817c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -61,6 +61,33 @@ Pointers to arrays/slices are compatible with pointers to the element type rule #isArrayOf( _ , _ ) => false [owise] ``` +Pointers to structs with a single zero-offset field are compatible with pointers to that field's type +```k + rule #typesCompatible(SRC, OTHER) => true + requires #zeroSizedType(SRC) orBool #zeroSizedType(OTHER) + + rule #typesCompatible(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER) + => #typesCompatible(lookupTy(FIELD), OTHER) + requires #zeroFieldOffset(LAYOUT) + + rule #typesCompatible(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) + => #typesCompatible(OTHER, lookupTy(FIELD)) + requires #zeroFieldOffset(LAYOUT) + + syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total] + + rule #zeroFieldOffset(LAYOUT) + => #layoutOffsets(LAYOUT) ==K .MachineSizes + orBool #layoutOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes + orBool #layoutOffsets(LAYOUT) ==K machineSize(0) .MachineSizes + + // Extract field offsets from the struct layout when available (Arbitrary only). + syntax MachineSizes ::= #layoutOffsets ( MaybeLayoutShape ) [function, total] + rule #layoutOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS + rule #layoutOffsets(noLayoutShape) => .MachineSizes + rule #layoutOffsets(_) => .MachineSizes [owise] +``` + ## Determining types of places with projection A helper function `getTyOf` traverses type metadata (using the type metadata map `Ty -> TypeInfo`) along the applied projections to determine the `Ty` of the projected place. @@ -70,6 +97,24 @@ To make this function total, an optional `MaybeTy` is used. syntax MaybeTy ::= Ty | "TyUnknown" + syntax MaybeTy ::= #transparentFieldTy ( TypeInfo ) [function, total] + + rule #transparentFieldTy(typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) => FIELD + requires #zeroFieldOffset(LAYOUT) + rule #transparentFieldTy(_) => TyUnknown [owise] + + syntax Int ::= #transparentDepth ( TypeInfo ) [function, total] + + rule #transparentDepth(typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) + => 1 +Int #transparentDepth(lookupTy(FIELD)) + requires #zeroFieldOffset(LAYOUT) + rule #transparentDepth(_) => 0 [owise] + + syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total] + + rule #lookupMaybeTy(TY:Ty) => lookupTy(TY) + rule #lookupMaybeTy(TyUnknown) => typeInfoVoidType + syntax MaybeTy ::= getTyOf( MaybeTy , ProjectionElems ) [function, total] // ----------------------------------------------------------- rule getTyOf(TyUnknown, _ ) => TyUnknown diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs new file mode 100644 index 000000000..dc4688326 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs @@ -0,0 +1,14 @@ +struct Wrapper(u32); + +fn roundtrip(ptr: *const Wrapper) -> u32 { + unsafe { + let erased = ptr as *const (); + let restored = erased as *const Wrapper; + (*restored).0 + } +} + +fn main() { + let value = Wrapper(0xCAFE_BABE); + assert!(roundtrip(&value) == 0xCAFE_BABE); +} diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.smir.json b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.smir.json new file mode 100644 index 000000000..7a7c15d5c --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.smir.json @@ -0,0 +1 @@ +{"name":"pointer_cast_zst","crate_id":18107857841876468948,"allocs":[{"alloc_id":1,"ty":39,"global_alloc":{"Memory":{"bytes":[97,115,115,101,114,116,105,111,110,32,102,97,105,108,101,100,58,32,114,111,117,110,100,116,114,105,112,40,38,118,97,108,117,101,41,32,61,61,32,48,120,67,65,70,69,95,66,65,66,69],"provenance":{"ptrs":[]},"align":1,"mutability":"Not"}}}],"functions":[[0,{"NormalSym":"_ZN3std2rt19lang_start_internal17h035df9ff6960926aE"}],[13,{"NormalSym":"_ZN3std3sys9backtrace28__rust_begin_short_backtrace17hb3c180f61a36ac03E"}],[14,{"NormalSym":"_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h1804589080c497b9E"}],[19,{"NormalSym":"_ZN4core3ops8function6FnOnce9call_once17h9ad1f677a6e2da1bE"}],[20,{"IntrinsicSym":"black_box"}],[21,{"NormalSym":"_ZN4core3ops8function6FnOnce9call_once17h5c8733dc296ff9fbE"}],[23,{"NormalSym":"_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h1ded425107b80709E"}],[31,{"NormalSym":"_ZN16pointer_cast_zst9roundtrip17h43a4d367a192a830E"}],[32,{"NormalSym":"_ZN4core9panicking5panic17h37379bf3ce79a0d7E"}],[41,{"NoOpSym":""}]],"uneval_consts":[],"items":[{"symbol_name":"_ZN16pointer_cast_zst4main17hda02ec75ea4af69bE","mono_item_kind":{"MonoItemFn":{"name":"main","id":7,"body":{"blocks":[{"statements":[{"kind":{"Assign":[{"local":1,"projection":[]},{"Aggregate":[{"Adt":[8,0,[],null,null]},[{"Constant":{"span":61,"user_ty":null,"const_":{"kind":{"Allocated":{"bytes":[190,186,254,202],"provenance":{"ptrs":[]},"align":4,"mutability":"Mut"}},"ty":29,"id":12}}}]]}]},"span":62},{"kind":{"Assign":[{"local":4,"projection":[]},{"Ref":[{"kind":"ReErased"},"Shared",{"local":1,"projection":[]}]}]},"span":63},{"kind":{"Assign":[{"local":3,"projection":[]},{"AddressOf":["Not",{"local":4,"projection":["Deref"]}]}]},"span":63}],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":59,"user_ty":null,"const_":{"kind":"ZeroSized","ty":31,"id":11}}},"args":[{"Move":{"local":3,"projection":[]}}],"destination":{"local":2,"projection":[]},"target":1,"unwind":"Continue"}},"span":60}},{"statements":[],"terminator":{"kind":{"SwitchInt":{"discr":{"Move":{"local":2,"projection":[]}},"targets":{"branches":[[3405691582,2]],"otherwise":3}}},"span":64}},{"statements":[],"terminator":{"kind":"Return","span":65}},{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":66,"user_ty":null,"const_":{"kind":"ZeroSized","ty":32,"id":13}}},"args":[{"Constant":{"span":32,"user_ty":null,"const_":{"kind":{"Allocated":{"bytes":[0,0,0,0,0,0,0,0,50,0,0,0,0,0,0,0],"provenance":{"ptrs":[[0,0]]},"align":8,"mutability":"Mut"}},"ty":33,"id":14}}}],"destination":{"local":5,"projection":[]},"target":null,"unwind":"Continue"}},"span":66}}],"locals":[{"ty":1,"span":67,"mutability":"Mut"},{"ty":28,"span":68,"mutability":"Not"},{"ty":29,"span":60,"mutability":"Mut"},{"ty":26,"span":63,"mutability":"Mut"},{"ty":34,"span":63,"mutability":"Not"},{"ty":35,"span":66,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[{"name":"value","source_info":{"span":68,"scope":1},"composite":null,"value":{"Place":{"local":1,"projection":[]}},"argument_index":null}],"spread_arg":null,"span":69}}},"details":null},{"symbol_name":"_ZN16pointer_cast_zst9roundtrip17h43a4d367a192a830E","mono_item_kind":{"MonoItemFn":{"name":"roundtrip","id":6,"body":{"blocks":[{"statements":[{"kind":{"Assign":[{"local":2,"projection":[]},{"Cast":["PtrToPtr",{"Copy":{"local":1,"projection":[]}},25]}]},"span":51},{"kind":{"Assign":[{"local":3,"projection":[]},{"Cast":["PtrToPtr",{"Copy":{"local":2,"projection":[]}},26]}]},"span":52},{"kind":{"Assign":[{"local":4,"projection":[]},{"Cast":["PtrToPtr",{"Copy":{"local":3,"projection":[]}},25]}]},"span":50},{"kind":{"Assign":[{"local":5,"projection":[]},{"Cast":["Transmute",{"Copy":{"local":4,"projection":[]}},27]}]},"span":50},{"kind":{"Assign":[{"local":6,"projection":[]},{"NullaryOp":["AlignOf",28]}]},"span":50},{"kind":{"Assign":[{"local":7,"projection":[]},{"BinaryOp":["Sub",{"Copy":{"local":6,"projection":[]}},{"Constant":{"span":50,"user_ty":null,"const_":{"kind":{"Allocated":{"bytes":[1,0,0,0,0,0,0,0],"provenance":{"ptrs":[]},"align":8,"mutability":"Mut"}},"ty":27,"id":9}}}]}]},"span":50},{"kind":{"Assign":[{"local":8,"projection":[]},{"BinaryOp":["BitAnd",{"Copy":{"local":5,"projection":[]}},{"Copy":{"local":7,"projection":[]}}]}]},"span":50},{"kind":{"Assign":[{"local":9,"projection":[]},{"BinaryOp":["Eq",{"Copy":{"local":8,"projection":[]}},{"Constant":{"span":50,"user_ty":null,"const_":{"kind":{"Allocated":{"bytes":[0,0,0,0,0,0,0,0],"provenance":{"ptrs":[]},"align":8,"mutability":"Mut"}},"ty":27,"id":10}}}]}]},"span":50}],"terminator":{"kind":{"Assert":{"cond":{"Copy":{"local":9,"projection":[]}},"expected":true,"msg":{"MisalignedPointerDereference":{"required":{"Copy":{"local":6,"projection":[]}},"found":{"Copy":{"local":5,"projection":[]}}}},"target":1,"unwind":"Unreachable"}},"span":50}},{"statements":[{"kind":{"Assign":[{"local":0,"projection":[]},{"Use":{"Copy":{"local":3,"projection":["Deref",{"Field":[0,29]}]}}}]},"span":50}],"terminator":{"kind":"Return","span":53}}],"locals":[{"ty":29,"span":54,"mutability":"Mut"},{"ty":26,"span":55,"mutability":"Not"},{"ty":25,"span":56,"mutability":"Not"},{"ty":26,"span":57,"mutability":"Not"},{"ty":25,"span":50,"mutability":"Mut"},{"ty":27,"span":50,"mutability":"Mut"},{"ty":27,"span":50,"mutability":"Mut"},{"ty":27,"span":50,"mutability":"Mut"},{"ty":27,"span":50,"mutability":"Mut"},{"ty":30,"span":50,"mutability":"Mut"}],"arg_count":1,"var_debug_info":[{"name":"ptr","source_info":{"span":55,"scope":0},"composite":null,"value":{"Place":{"local":1,"projection":[]}},"argument_index":1},{"name":"erased","source_info":{"span":56,"scope":1},"composite":null,"value":{"Place":{"local":2,"projection":[]}},"argument_index":null},{"name":"restored","source_info":{"span":57,"scope":2},"composite":null,"value":{"Place":{"local":3,"projection":[]}},"argument_index":null}],"spread_arg":null,"span":58}}},"details":null},{"symbol_name":"_ZN3std2rt10lang_start17h962317fbad4853bbE","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$17h1ded425107b80709E","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_backtrace17hb3c180f61a36ac03E","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$17h2c2bf18f439a060cE","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_once17h5c8733dc296ff9fbE","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":"_ZN4core3ops8function6FnOnce9call_once17h9ad1f677a6e2da1bE","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":"_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17hdaf6a782b5b32c5bE","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$6report17h1804589080c497b9E","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":8}}}}]},"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}],"types":[[1,{"TupleType":{"types":[],"layout":{"fields":{"Arbitrary":{"offsets":[]}},"variants":{"Single":{"index":0}},"abi":{"Aggregate":{"sized":true}},"abi_align":1,"size":{"num_bits":0}}}}],[5,{"RefType":{"pointee_type":36,"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}}}}],[6,{"PrimitiveType":{"Int":"Isize"}}],[8,{"PtrType":{"pointee_type":37,"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}}}}],[9,{"PrimitiveType":{"Uint":"U8"}}],[10,{"EnumType":{"name":"std::result::Result","adt_def":21,"discriminants":[0,1],"fields":[[6],[35]],"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}}}}],[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}}}}],[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}}}}],[16,{"PrimitiveType":{"Int":"I32"}}],[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}}}}],[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}}}}],[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}}}}],[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}}}}],[25,{"PtrType":{"pointee_type":1,"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}}}}],[26,{"PtrType":{"pointee_type":28,"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}}}}],[27,{"PrimitiveType":{"Uint":"Usize"}}],[28,{"StructType":{"name":"Wrapper","adt_def":8,"fields":[29],"layout":{"fields":{"Arbitrary":{"offsets":[{"num_bits":0}]}},"variants":{"Single":{"index":0}},"abi":{"Scalar":{"Initialized":{"value":{"Int":{"length":"I32","signed":false}},"valid_range":{"start":0,"end":4294967295}}}},"abi_align":4,"size":{"num_bits":32}}}}],[29,{"PrimitiveType":{"Uint":"U32"}}],[30,{"PrimitiveType":"Bool"}],[33,{"RefType":{"pointee_type":39,"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":{"Int":{"length":"I64","signed":false}},"valid_range":{"start":0,"end":18446744073709551615}}}]},"abi_align":8,"size":{"num_bits":128}}}}],[34,{"RefType":{"pointee_type":28,"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}}}}],[35,"VoidType"],[37,{"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}}}}],[38,{"RefType":{"pointee_type":40,"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}}}}],[39,{"PrimitiveType":"Str"}],[40,{"StructType":{"name":"std::panic::Location<'_>","adt_def":25,"fields":[33,29,29],"layout":{"fields":{"Arbitrary":{"offsets":[{"num_bits":0},{"num_bits":128},{"num_bits":160}]}},"variants":{"Single":{"index":0}},"abi":{"Aggregate":{"sized":true}},"abi_align":8,"size":{"num_bits":192}}}}]],"spans":[[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[32,["no-location",0,0,0,0]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[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]],[50,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",7,9,7,22]],[51,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",5,22,5,38]],[52,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",6,24,6,48]],[53,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",9,2,9,2]],[55,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",3,14,3,17]],[56,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",5,13,5,19]],[57,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",6,13,6,21]],[58,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",3,1,9,2]],[59,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",13,13,13,22]],[60,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",13,13,13,30]],[61,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",12,25,12,36]],[62,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",12,17,12,37]],[63,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",13,23,13,29]],[64,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",13,13,13,45]],[65,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",14,2,14,2]],[66,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",13,5,13,46]],[68,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",12,9,12,14]],[69,["/Users/steven/Desktop/projs/kmir/mir5/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs",11,1,14,2]]],"debug":null,"machine":{"endian":"Little","pointer_width":{"num_bits":64}}} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state new file mode 100644 index 000000000..059a1ae70 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state @@ -0,0 +1,50 @@ + + + PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K + + + noReturn + + + ty ( 31 ) + + + + ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 2 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 51 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements , terminator: terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ) + ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 3 ) , projection: projectionElemDeref projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) ) .ProjectionElems ) ) ) ) , span: span ( 50 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 53 ) ) ) ) + + + ty ( -1 ) + + + place (... local: local ( 2 ) , projection: .ProjectionElems ) + + + someBasicBlockIdx ( basicBlockIdx ( 1 ) ) + + + unwindActionContinue + + + ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 25 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 26 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) ) + + + + ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 3405691582 , 32 , false ) ) ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) ) + ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 34 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 35 ) , mutabilityMut ) ) ) ) + ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) ) + + \ No newline at end of file diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut2.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut2.rs 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 index 7cb6831b6..07ddc99a8 100644 --- 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 @@ -3,10 +3,10 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (198 steps) +│ (866 steps) └─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 11 ) , thunk ( #cast ( PtrLocal ( 3 , place ( .. - span: 91 + #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , + span: 32 ┌─ 2 (root, leaf, target, terminal) diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected deleted file mode 100644 index 6ef3112a7..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (185 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 3 , place ( ... - span: 53 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected index d4b0127e7..5d1bd2ecc 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected @@ -26,11 +26,34 @@ │ #execBlockIdx ( basicBlockIdx ( 8 ) ) ~> .K │ function: main │ - │ (8 steps) - └─ 7 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 1 , place ( ... - function: main - span: 80 + │ (111 steps) + ├─ 7 + │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th + │ function: main + ┃ + ┃ (1 step) + ┣━━┓ + ┃ │ + ┃ ├─ 8 + ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC + ┃ │ function: main + ┃ │ + ┃ │ (1 step) + ┃ └─ 10 (stuck, leaf) + ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re + ┃ function: main + ┃ + ┗━━┓ + │ + ├─ 9 + │ #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K + │ function: main + │ + │ (17 steps) + └─ 11 (stuck, leaf) + #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems ) + function: main + span: 79 ┌─ 2 (root, leaf, target, terminal) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 4bdd55b39..ebe847226 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -41,7 +41,6 @@ PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', 'interior-mut-fail', - 'interior-mut2-fail', 'interior-mut3-fail', 'assert_eq_exp', 'bitwise-not-shift', @@ -263,6 +262,12 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo EXEC_DATA_DIR / 'pointers' / 'pointer-cast-length-test-fail.state', 1000, ), + ( + 'pointer-cast-zst', + EXEC_DATA_DIR / 'pointers' / 'pointer-cast-zst.smir.json', + EXEC_DATA_DIR / 'pointers' / 'pointer-cast-zst.state', + 48, + ), ( 'ref-ptr-cases', EXEC_DATA_DIR / 'pointers' / 'ref_ptr_cases.smir.json',