From 244dae6d1035c8dec993e6bdff6d66181586adba Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 7 Nov 2025 17:39:53 +1100 Subject: [PATCH 1/9] implement special calling convention for closures (tuple argument unpacked) --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 63 +++++++++++++++++++- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 24 -------- 2 files changed, 62 insertions(+), 25 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 36ced69cf..5d2412f8c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -367,7 +367,6 @@ An operand may be a `Reference` (the only way a function could access another fu => ListItem(newLocal(TY, MUT)) #reserveFor(REST) - syntax KItem ::= #setArgsFromStack ( Int, Operands) | #setArgFromStack ( Int, Operand) | #execIntrinsic ( MonoItemKind, Operands, Place ) @@ -410,6 +409,68 @@ An operand may be a `Reference` (the only way a function could access another fu andBool isTypedValue(CALLERLOCALS[I]) [preserves-definedness] // valid list indexing checked ``` + +For closures (like `|x,y| { things using x and y }`), a special calling convention is in effect: +The first argument of the closure is its environment. +Its type is currently not extracted (KMIR does not currently support variable-capturing) and it is not initialised. +The second argument is a _tuple_ of all the arguments, however the function body expects these arguments as single locals. + +```k + // reserve space for local variables and copy/move arguments from a tuple inside the old locals into their place + rule [setupCalleeClosure]: #setUpCalleeData( + monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))), + operandMove(place(local(CLOSURE:Int), .ProjectionElems)) + operandMove(place(local(TUPLE), .ProjectionElems)) + .Operands + ) + => + #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST) + ... + + // CALLEE + + _ => toKList(BLOCKS) + // CALLER + // DEST + // TARGET + // UNWIND + LOCALS => #reserveFor(NEWLOCALS) + // assumption: arguments stored as _1 .. _n before actual "local" data + ... + + requires 0 <=Int CLOSURE andBool CLOSURE Ty) ==K typeInfoVoidType // closure types don't get extracted at the moment + [priority(40), preserves-definedness] + + syntax Bool ::= isTupleType ( TypeInfo ) [function, total] + | isRefType ( TypeInfo ) [function, total] + // ------------------------------------------------------- + rule isTupleType(typeInfoTupleType(_)) => true + rule isTupleType( _ ) => false [owise] + rule isRefType(typeInfoRefType(_)) => true + rule isRefType( _ ) => false [owise] + + syntax KItem ::= #setTupleArgs ( Int , Value ) + | #setTupleArgs ( Int , List ) + + // unpack tuple and set arguments individually + rule #setTupleArgs(IDX, Aggregate(variantIdx(0), ARGS)) => #setTupleArgs(IDX, ARGS) ... + + rule #setTupleArgs(_, .List ) => .K ... + + rule #setTupleArgs(IDX, ListItem(VAL) REST:List) + => #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(VAL)) ~> #setTupleArgs(IDX +Int 1, REST) + ... + +``` + + +#### Assert + The `Assert` terminator checks that an operand holding a boolean value (which has previously been computed, e.g., an overflow flag for arithmetic operations) has the expected value (e.g., that this overflow flag is `false` - a very common case). If the condition value is as expected, the program proceeds with the given `target` block. Otherwise the provided message is passed to a `panic!` call, ending the program with an error, modelled as an `AssertError` in the semantics. diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 7adc8dd0f..d1944f033 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -437,30 +437,6 @@ This is done without consideration of the validity of the Downcast[^downcast]. ``` -If an Aggregate contains only one element and #traverseProjection becomes stuck, you can directly access this element. - -Without this rule, the test `closure_access_struct-fail.rs` demonstrates the following behavior: -- The execution gets stuck after 192 steps at `#traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( ... ) ) , ... )` -- The stuck state occurs because there's a Deref projection that needs to be applied to the single element of this Aggregate, but the existing Deref rules only handle pointers and references, not Aggregates - -With this rule enabled: -- The execution progresses further to 277 steps before getting stuck -- It gets stuck at a different location: `#traverseProjection ( toLocal ( 19 ) , thunk ( #decodeConstant ( constantKindAll ... ) ) , ... )` -- The rule automatically unwraps the single-element Aggregate, allowing the field access to proceed - -This rule is essential for handling closures that access struct fields, as MIR represents certain struct accesses through single-element Aggregates that need to be unwrapped. - -```k - rule #traverseProjection( - DEST, - Aggregate(_, ARGS), - PROJS, - CTXTS - ) - => #traverseProjection(DEST, getValue(ARGS, 0), PROJS, CTXTS) ... - requires size(ARGS) ==Int 1 [preserves-definedness, priority(100)] -``` - #### Ranges An `Index` projection operates on an array or slice (`Range`) value, to access an element of the array. From d3da569b7038c5d7defdd9a7e5ee5c113c52c09b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 7 Nov 2025 17:46:35 +1100 Subject: [PATCH 2/9] add new test for closure calling convention --- .../exec-smir/call-with-args/closure-call.rs | 18 + .../call-with-args/closure-call.smir.json | 3881 +++++++++++++++++ .../call-with-args/closure-call.state | 48 + .../src/tests/integration/test_integration.py | 6 + 4 files changed, 3953 insertions(+) create mode 100644 kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.rs create mode 100644 kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.smir.json create mode 100644 kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.rs b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.rs new file mode 100644 index 000000000..431b30f91 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.rs @@ -0,0 +1,18 @@ +fn test_t(x: (u32,)) -> u32 { x.0 } // expects a singleton tuple + +fn main() { + let single: u32 = 32; + let tuple: (u32,) = (single,); + + test_t(tuple); // gets passed a singleton tuple + + let identity = |x| x; // expects a single u32 + + identity(single); // gets passed a &closure and a singleton tuple! + + let twice = (single, single); + let is_equal = |a, b| { assert!(a == b); }; // expects and accesses its arguments as locals _2 and _3 (u32) + + // is_equal(twice); // error + is_equal(single, single); // gets passed a &closure and a singleton tuple !!! +} diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.smir.json b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.smir.json new file mode 100644 index 000000000..abdf57b09 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.smir.json @@ -0,0 +1,3881 @@ +{ + "name": "closure_call", + "crate_id": 6936582464197367803, + "allocs": [ + { + "alloc_id": 1, + "ty": 43, + "global_alloc": { + "Memory": { + "bytes": [ + 97, + 115, + 115, + 101, + 114, + 116, + 105, + 111, + 110, + 32, + 102, + 97, + 105, + 108, + 101, + 100, + 58, + 32, + 97, + 32, + 61, + 61, + 32, + 98 + ], + "provenance": { + "ptrs": [] + }, + "align": 1, + "mutability": "Not" + } + } + } + ], + "functions": [ + [ + 0, + { + "NormalSym": "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E" + } + ], + [ + 13, + { + "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h9b490df76c1d359dE" + } + ], + [ + 14, + { + "NormalSym": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h39fb1d4c166afaffE" + } + ], + [ + 19, + { + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17he927c0ae2717b3ddE" + } + ], + [ + 20, + { + "IntrinsicSym": "black_box" + } + ], + [ + 21, + { + "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17hf20109c62be49566E" + } + ], + [ + 23, + { + "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h88d343d198c60c14E" + } + ], + [ + 27, + { + "NormalSym": "_ZN12closure_call6test_t17h3f9dcc7568e8e6deE" + } + ], + [ + 28, + { + "NormalSym": "_ZN12closure_call4main28_$u7b$$u7b$closure$u7d$$u7d$17h2ce069f3f8e18da6E" + } + ], + [ + 29, + { + "NormalSym": "_ZN12closure_call4main28_$u7b$$u7b$closure$u7d$$u7d$17hd367e620ad7f0d56E" + } + ], + [ + 35, + { + "NormalSym": "_ZN4core9panicking5panic17h941160ead03e2d54E" + } + ], + [ + 41, + { + "NoOpSym": "" + } + ] + ], + "uneval_consts": [], + "items": [ + { + "symbol_name": "_ZN12closure_call4main17hb5e5ffe1c1657f94E", + "mono_item_kind": { + "MonoItemFn": { + "name": "main", + "id": 7, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 1, + "projection": [] + }, + { + "Use": { + "Constant": { + "span": 57, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 32, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [] + }, + "align": 4, + "mutability": "Mut" + } + }, + "ty": 25, + "id": 10 + } + } + } + } + ] + }, + "span": 57 + }, + { + "kind": { + "Assign": [ + { + "local": 2, + "projection": [] + }, + { + "Aggregate": [ + "Tuple", + [ + { + "Copy": { + "local": 1, + "projection": [] + } + } + ] + ] + } + ] + }, + "span": 58 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 55, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 27, + "id": 9 + } + } + }, + "args": [ + { + "Copy": { + "local": 2, + "projection": [] + } + } + ], + "destination": { + "local": 3, + "projection": [] + }, + "target": 1, + "unwind": "Continue" + } + }, + "span": 56 + } + }, + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 6, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + "Shared", + { + "local": 4, + "projection": [] + } + ] + } + ] + }, + "span": 59 + }, + { + "kind": { + "Assign": [ + { + "local": 7, + "projection": [] + }, + { + "Aggregate": [ + "Tuple", + [ + { + "Copy": { + "local": 1, + "projection": [] + } + } + ] + ] + } + ] + }, + "span": 60 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 59, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 28, + "id": 11 + } + } + }, + "args": [ + { + "Move": { + "local": 6, + "projection": [] + } + }, + { + "Move": { + "local": 7, + "projection": [] + } + } + ], + "destination": { + "local": 5, + "projection": [] + }, + "target": 2, + "unwind": "Continue" + } + }, + "span": 60 + } + }, + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 8, + "projection": [] + }, + { + "Aggregate": [ + "Tuple", + [ + { + "Copy": { + "local": 1, + "projection": [] + } + }, + { + "Copy": { + "local": 1, + "projection": [] + } + } + ] + ] + } + ] + }, + "span": 63 + }, + { + "kind": { + "Assign": [ + { + "local": 11, + "projection": [] + }, + { + "Ref": [ + { + "kind": "ReErased" + }, + "Shared", + { + "local": 9, + "projection": [] + } + ] + } + ] + }, + "span": 61 + }, + { + "kind": { + "Assign": [ + { + "local": 12, + "projection": [] + }, + { + "Aggregate": [ + "Tuple", + [ + { + "Copy": { + "local": 1, + "projection": [] + } + }, + { + "Copy": { + "local": 1, + "projection": [] + } + } + ] + ] + } + ] + }, + "span": 62 + } + ], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 61, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 29, + "id": 12 + } + } + }, + "args": [ + { + "Move": { + "local": 11, + "projection": [] + } + }, + { + "Move": { + "local": 12, + "projection": [] + } + } + ], + "destination": { + "local": 10, + "projection": [] + }, + "target": 3, + "unwind": "Continue" + } + }, + "span": 62 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 64 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 65, + "mutability": "Mut" + }, + { + "ty": 25, + "span": 66, + "mutability": "Not" + }, + { + "ty": 26, + "span": 67, + "mutability": "Not" + }, + { + "ty": 25, + "span": 56, + "mutability": "Not" + }, + { + "ty": 30, + "span": 68, + "mutability": "Not" + }, + { + "ty": 25, + "span": 60, + "mutability": "Not" + }, + { + "ty": 31, + "span": 59, + "mutability": "Mut" + }, + { + "ty": 26, + "span": 60, + "mutability": "Mut" + }, + { + "ty": 32, + "span": 69, + "mutability": "Not" + }, + { + "ty": 33, + "span": 70, + "mutability": "Not" + }, + { + "ty": 1, + "span": 62, + "mutability": "Not" + }, + { + "ty": 34, + "span": 61, + "mutability": "Mut" + }, + { + "ty": 32, + "span": 62, + "mutability": "Mut" + } + ], + "arg_count": 0, + "var_debug_info": [ + { + "name": "single", + "source_info": { + "span": 66, + "scope": 1 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": null + }, + { + "name": "tuple", + "source_info": { + "span": 67, + "scope": 2 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": null + }, + { + "name": "identity", + "source_info": { + "span": 68, + "scope": 3 + }, + "composite": null, + "value": { + "Const": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 30, + "id": 13 + } + } + }, + "argument_index": null + }, + { + "name": "twice", + "source_info": { + "span": 69, + "scope": 4 + }, + "composite": null, + "value": { + "Place": { + "local": 8, + "projection": [] + } + }, + "argument_index": null + }, + { + "name": "is_equal", + "source_info": { + "span": 70, + "scope": 5 + }, + "composite": null, + "value": { + "Const": { + "span": 32, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 33, + "id": 14 + } + } + }, + "argument_index": null + } + ], + "spread_arg": null, + "span": 71 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN12closure_call4main28_$u7b$$u7b$closure$u7d$$u7d$17h2ce069f3f8e18da6E", + "mono_item_kind": { + "MonoItemFn": { + "name": "main::{closure#0}", + "id": 8, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 2, + "projection": [] + } + } + } + ] + }, + "span": 73 + } + ], + "terminator": { + "kind": "Return", + "span": 72 + } + } + ], + "locals": [ + { + "ty": 25, + "span": 74, + "mutability": "Mut" + }, + { + "ty": 31, + "span": 75, + "mutability": "Mut" + }, + { + "ty": 25, + "span": 76, + "mutability": "Not" + } + ], + "arg_count": 2, + "var_debug_info": [ + { + "name": "x", + "source_info": { + "span": 76, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": 2 + } + ], + "spread_arg": null, + "span": 75 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN12closure_call4main28_$u7b$$u7b$closure$u7d$$u7d$17hd367e620ad7f0d56E", + "mono_item_kind": { + "MonoItemFn": { + "name": "main::{closure#1}", + "id": 9, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 4, + "projection": [] + }, + { + "BinaryOp": [ + "Eq", + { + "Copy": { + "local": 2, + "projection": [] + } + }, + { + "Copy": { + "local": 3, + "projection": [] + } + } + ] + } + ] + }, + "span": 77 + } + ], + "terminator": { + "kind": { + "SwitchInt": { + "discr": { + "Move": { + "local": 4, + "projection": [] + } + }, + "targets": { + "branches": [ + [ + 0, + 2 + ] + ], + "otherwise": 1 + } + } + }, + "span": 77 + } + }, + { + "statements": [], + "terminator": { + "kind": "Return", + "span": 78 + } + }, + { + "statements": [], + "terminator": { + "kind": { + "Call": { + "func": { + "Constant": { + "span": 79, + "user_ty": null, + "const_": { + "kind": "ZeroSized", + "ty": 35, + "id": 15 + } + } + }, + "args": [ + { + "Constant": { + "span": 32, + "user_ty": null, + "const_": { + "kind": { + "Allocated": { + "bytes": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 24, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "provenance": { + "ptrs": [ + [ + 0, + 0 + ] + ] + }, + "align": 8, + "mutability": "Mut" + } + }, + "ty": 36, + "id": 16 + } + } + } + ], + "destination": { + "local": 5, + "projection": [] + }, + "target": null, + "unwind": "Continue" + } + }, + "span": 79 + } + } + ], + "locals": [ + { + "ty": 1, + "span": 80, + "mutability": "Mut" + }, + { + "ty": 34, + "span": 81, + "mutability": "Mut" + }, + { + "ty": 25, + "span": 82, + "mutability": "Not" + }, + { + "ty": 25, + "span": 83, + "mutability": "Not" + }, + { + "ty": 37, + "span": 77, + "mutability": "Mut" + }, + { + "ty": 38, + "span": 79, + "mutability": "Mut" + } + ], + "arg_count": 3, + "var_debug_info": [ + { + "name": "a", + "source_info": { + "span": 82, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 2, + "projection": [] + } + }, + "argument_index": 2 + }, + { + "name": "b", + "source_info": { + "span": 83, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 3, + "projection": [] + } + }, + "argument_index": 3 + } + ], + "spread_arg": null, + "span": 81 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN12closure_call6test_t17h3f9dcc7568e8e6deE", + "mono_item_kind": { + "MonoItemFn": { + "name": "test_t", + "id": 6, + "body": { + "blocks": [ + { + "statements": [ + { + "kind": { + "Assign": [ + { + "local": 0, + "projection": [] + }, + { + "Use": { + "Copy": { + "local": 1, + "projection": [ + { + "Field": [ + 0, + 25 + ] + } + ] + } + } + } + ] + }, + "span": 51 + } + ], + "terminator": { + "kind": "Return", + "span": 50 + } + } + ], + "locals": [ + { + "ty": 25, + "span": 52, + "mutability": "Mut" + }, + { + "ty": 26, + "span": 53, + "mutability": "Not" + } + ], + "arg_count": 1, + "var_debug_info": [ + { + "name": "x", + "source_info": { + "span": 53, + "scope": 0 + }, + "composite": null, + "value": { + "Place": { + "local": 1, + "projection": [] + } + }, + "argument_index": 1 + } + ], + "spread_arg": null, + "span": 54 + } + } + }, + "details": null + }, + { + "symbol_name": "_ZN3std2rt10lang_start17h3e49324270363008E", + "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$17h88d343d198c60c14E", + "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_backtrace17h9b490df76c1d359dE", + "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$17h9f33329171bf7dccE", + "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_once17he927c0ae2717b3ddE", + "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_once17hf20109c62be49566E", + "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": "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h13f2f296c84e7e84E", + "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$6report17h39fb1d4c166afaffE", + "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": 45, + "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": 46, + "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": 28, + "discriminants": [ + 0, + 1 + ], + "fields": [ + [ + 6 + ], + [ + 38 + ] + ], + "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": 16, + "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": 14, + "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, + { + "PrimitiveType": { + "Uint": "U32" + } + } + ], + [ + 26, + { + "TupleType": { + "types": [ + 25 + ], + "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 + } + } + } + } + ], + [ + 31, + { + "RefType": { + "pointee_type": 30, + "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 + } + } + } + } + ], + [ + 32, + { + "TupleType": { + "types": [ + 25, + 25 + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + }, + { + "num_bits": 32 + } + ] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "ScalarPair": [ + { + "Initialized": { + "value": { + "Int": { + "length": "I32", + "signed": false + } + }, + "valid_range": { + "start": 0, + "end": 4294967295 + } + } + }, + { + "Initialized": { + "value": { + "Int": { + "length": "I32", + "signed": false + } + }, + "valid_range": { + "start": 0, + "end": 4294967295 + } + } + } + ] + }, + "abi_align": 4, + "size": { + "num_bits": 64 + } + } + } + } + ], + [ + 34, + { + "RefType": { + "pointee_type": 33, + "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 + } + } + } + } + ], + [ + 36, + { + "RefType": { + "pointee_type": 43, + "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 + } + } + } + } + ], + [ + 37, + { + "PrimitiveType": "Bool" + } + ], + [ + 38, + "VoidType" + ], + [ + 42, + { + "RefType": { + "pointee_type": 44, + "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 + } + } + } + } + ], + [ + 43, + { + "PrimitiveType": "Str" + } + ], + [ + 44, + { + "StructType": { + "name": "std::panic::Location<'_>", + "adt_def": 19, + "fields": [ + 36, + 25, + 25 + ], + "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 + } + } + } + } + ], + [ + 46, + { + "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 + } + } + } + } + ] + ], + "spans": [ + [ + 0, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 194, + 17, + 194, + 36 + ] + ], + [ + 1, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 194, + 17, + 199, + 6 + ] + ], + [ + 2, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 9, + 195, + 93 + ] + ], + [ + 3, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 10, + 195, + 93 + ] + ], + [ + 4, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 201, + 2, + 201, + 2 + ] + ], + [ + 5, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 199, + 5, + 199, + 6 + ] + ], + [ + 6, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 194, + 12, + 194, + 13 + ] + ], + [ + 7, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 199, + 6, + 199, + 7 + ] + ], + [ + 9, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 189, + 5, + 189, + 9 + ] + ], + [ + 10, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 190, + 5, + 190, + 9 + ] + ], + [ + 11, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 191, + 5, + 191, + 9 + ] + ], + [ + 12, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 192, + 5, + 192, + 12 + ] + ], + [ + 13, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 188, + 1, + 201, + 2 + ] + ], + [ + 14, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 18, + 195, + 69 + ] + ], + [ + 15, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 18, + 195, + 75 + ] + ], + [ + 16, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 18, + 195, + 84 + ] + ], + [ + 17, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 70, + 195, + 74 + ] + ], + [ + 18, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 76, + 195, + 82 + ] + ], + [ + 19, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 74, + 195, + 75 + ] + ], + [ + 20, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 93, + 195, + 93 + ] + ], + [ + 21, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 83, + 195, + 84 + ] + ], + [ + 22, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/process.rs", + 2053, + 9, + 2053, + 15 + ] + ], + [ + 23, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 636, + 9, + 636, + 15 + ] + ], + [ + 24, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 636, + 9, + 636, + 22 + ] + ], + [ + 25, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 636, + 21, + 636, + 22 + ] + ], + [ + 26, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/process.rs", + 2053, + 23, + 2053, + 24 + ] + ], + [ + 27, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/rt.rs", + 195, + 92, + 195, + 93 + ] + ], + [ + 29, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/process.rs", + 2052, + 19, + 2052, + 23 + ] + ], + [ + 30, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/pal/unix/process/process_common.rs", + 635, + 19, + 635, + 24 + ] + ], + [ + 31, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 154, + 18, + 154, + 19 + ] + ], + [ + 32, + [ + "no-location", + 0, + 0, + 0, + 0 + ] + ], + [ + 33, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 154, + 18, + 154, + 21 + ] + ], + [ + 34, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs", + 389, + 5, + 389, + 33 + ] + ], + [ + 35, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs", + 389, + 5, + 389, + 40 + ] + ], + [ + 36, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 160, + 2, + 160, + 2 + ] + ], + [ + 38, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 150, + 43, + 150, + 44 + ] + ], + [ + 40, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 154, + 9, + 154, + 15 + ] + ], + [ + 41, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs", + 388, + 27, + 388, + 32 + ] + ], + [ + 42, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/backtrace.rs", + 150, + 1, + 160, + 2 + ] + ], + [ + 43, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs", + 250, + 5, + 250, + 71 + ] + ], + [ + 44, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs", + 521, + 1, + 521, + 56 + ] + ], + [ + 45, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/process.rs", + 2424, + 6, + 2424, + 6 + ] + ], + [ + 46, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/process.rs", + 2423, + 9, + 2423, + 26 + ] + ], + [ + 48, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/process.rs", + 2422, + 15, + 2422, + 19 + ] + ], + [ + 49, + [ + "/home/jost/.rustup/toolchains/nightly-2024-11-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/process.rs", + 2422, + 5, + 2424, + 6 + ] + ], + [ + 50, + [ + "closure-call.rs", + 1, + 36, + 1, + 36 + ] + ], + [ + 51, + [ + "closure-call.rs", + 1, + 31, + 1, + 34 + ] + ], + [ + 53, + [ + "closure-call.rs", + 1, + 11, + 1, + 12 + ] + ], + [ + 54, + [ + "closure-call.rs", + 1, + 1, + 1, + 36 + ] + ], + [ + 55, + [ + "closure-call.rs", + 7, + 5, + 7, + 11 + ] + ], + [ + 56, + [ + "closure-call.rs", + 7, + 5, + 7, + 18 + ] + ], + [ + 57, + [ + "closure-call.rs", + 4, + 23, + 4, + 25 + ] + ], + [ + 58, + [ + "closure-call.rs", + 5, + 25, + 5, + 34 + ] + ], + [ + 59, + [ + "closure-call.rs", + 11, + 5, + 11, + 13 + ] + ], + [ + 60, + [ + "closure-call.rs", + 11, + 5, + 11, + 21 + ] + ], + [ + 61, + [ + "closure-call.rs", + 17, + 5, + 17, + 13 + ] + ], + [ + 62, + [ + "closure-call.rs", + 17, + 5, + 17, + 29 + ] + ], + [ + 63, + [ + "closure-call.rs", + 13, + 17, + 13, + 33 + ] + ], + [ + 64, + [ + "closure-call.rs", + 18, + 2, + 18, + 2 + ] + ], + [ + 66, + [ + "closure-call.rs", + 4, + 9, + 4, + 15 + ] + ], + [ + 67, + [ + "closure-call.rs", + 5, + 9, + 5, + 14 + ] + ], + [ + 68, + [ + "closure-call.rs", + 9, + 9, + 9, + 17 + ] + ], + [ + 69, + [ + "closure-call.rs", + 13, + 9, + 13, + 14 + ] + ], + [ + 70, + [ + "closure-call.rs", + 14, + 9, + 14, + 17 + ] + ], + [ + 71, + [ + "closure-call.rs", + 3, + 1, + 18, + 2 + ] + ], + [ + 72, + [ + "closure-call.rs", + 9, + 25, + 9, + 25 + ] + ], + [ + 73, + [ + "closure-call.rs", + 9, + 24, + 9, + 25 + ] + ], + [ + 75, + [ + "closure-call.rs", + 9, + 20, + 9, + 25 + ] + ], + [ + 76, + [ + "closure-call.rs", + 9, + 21, + 9, + 22 + ] + ], + [ + 77, + [ + "closure-call.rs", + 14, + 37, + 14, + 43 + ] + ], + [ + 78, + [ + "closure-call.rs", + 14, + 47, + 14, + 47 + ] + ], + [ + 79, + [ + "closure-call.rs", + 14, + 29, + 14, + 44 + ] + ], + [ + 81, + [ + "closure-call.rs", + 14, + 20, + 14, + 47 + ] + ], + [ + 82, + [ + "closure-call.rs", + 14, + 21, + 14, + 22 + ] + ], + [ + 83, + [ + "closure-call.rs", + 14, + 24, + 14, + 25 + ] + ] + ], + "debug": null, + "machine": { + "endian": "Little", + "pointer_width": { + "num_bits": 64 + } + } +} diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state new file mode 100644 index 000000000..49930c0d6 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state @@ -0,0 +1,48 @@ + + + #setLocalValue ( place (... local: local ( 1 ) , projection: .ProjectionElems ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) ) ~> #setArgsFromStack ( 2 , .Operands ) ~> #execBlock ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 25 ) ) .ProjectionElems ) ) ) ) , span: span ( 51 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 50 ) ) ) ) ~> .K + + + noReturn + + + ty ( 27 ) + + + + ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 25 ) ) .ProjectionElems ) ) ) ) , span: span ( 51 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 50 ) ) ) ) + + + ty ( -1 ) + + + place (... local: local ( 3 ) , projection: .ProjectionElems ) + + + someBasicBlockIdx ( basicBlockIdx ( 1 ) ) + + + unwindActionContinue + + + ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 26 ) , mutabilityNot ) ) + + + + ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) + ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 26 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 25 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 30 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 25 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 26 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 32 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 33 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 34 ) , mutabilityMut ) ) + ListItem ( newLocal ( ty ( 32 ) , 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/test_integration.py b/kmir/src/tests/integration/test_integration.py index a42265cc9..d4734dac8 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -153,6 +153,12 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo EXEC_DATA_DIR / 'call-with-args' / 'main-a-b-with-int.state', 30, ), + ( + 'closure-call', + EXEC_DATA_DIR / 'call-with-args' / 'closure-call.smir.json', + EXEC_DATA_DIR / 'call-with-args' / 'closure-call.state', + 30, + ), ( 'assign-cast', EXEC_DATA_DIR / 'assign-cast' / 'assign-cast.smir.json', From a90733ecbf9876f7999dcf090910f223b5bae226 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 7 Nov 2025 17:48:59 +1100 Subject: [PATCH 3/9] adjust test expectation for closure_access_struct test --- .../data/prove-rs/show/closure_access_struct.main.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected index 0459ee731..4777def47 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (315 steps) +│ (311 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main From 1547f684c61c069cea721791b941133ddae3e7f0 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 7 Nov 2025 19:45:46 +1100 Subject: [PATCH 4/9] mark arguments as Moved, execute test to the end (to also prove termination) --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 9 ++-- .../call-with-args/closure-call.state | 43 ++++++++++--------- .../src/tests/integration/test_integration.py | 2 +- 3 files changed, 28 insertions(+), 26 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 5d2412f8c..bfc3e7e92 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -427,14 +427,13 @@ The second argument is a _tuple_ of all the arguments, however the function body #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST) ... - // CALLEE _ => toKList(BLOCKS) - // CALLER - // DEST - // TARGET - // UNWIND LOCALS => #reserveFor(NEWLOCALS) + + (ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved))) + _:List + // assumption: arguments stored as _1 .. _n before actual "local" data ... diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state index 49930c0d6..9c598b715 100644 --- a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state @@ -1,48 +1,51 @@ - #setLocalValue ( place (... local: local ( 1 ) , projection: .ProjectionElems ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) ) ~> #setArgsFromStack ( 2 , .Operands ) ~> #execBlock ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 25 ) ) .ProjectionElems ) ) ) ) , span: span ( 51 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 50 ) ) ) ) ~> .K + #EndProgram ~> .K noReturn - ty ( 27 ) + ty ( -1 ) - ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 25 ) ) .ProjectionElems ) ) ) ) , span: span ( 51 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 50 ) ) ) ) + ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 1 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b" \x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 4 ) , mutability: mutabilityMut ) ) , ty: ty ( 25 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 57 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 2 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindTuple , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 58 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 55 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) , args: operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 3 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 56 ) ) ) ) + ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 4 ) , projection: .ProjectionElems ) ) ) , span: span ( 59 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindTuple , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 60 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 59 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 28 ) , id: mirConstId ( 11 ) ) ) ) , args: operandMove ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) operandMove ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 5 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionContinue ) , span: span ( 60 ) ) ) ) + ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindTuple , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 63 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 11 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 9 ) , projection: .ProjectionElems ) ) ) , span: span ( 61 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 12 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindTuple , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 62 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 61 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 29 ) , id: mirConstId ( 12 ) ) ) ) , args: operandMove ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ) operandMove ( place (... local: local ( 12 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 10 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 3 ) ) , unwind: unwindActionContinue ) , span: span ( 62 ) ) ) ) + ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 64 ) ) ) ) ty ( -1 ) - place (... local: local ( 3 ) , projection: .ProjectionElems ) + place (... local: local ( 0 ) , projection: .ProjectionElems ) - someBasicBlockIdx ( basicBlockIdx ( 1 ) ) + noBasicBlockIdx unwindActionContinue - ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) ) - ListItem ( newLocal ( ty ( 26 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) + ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 26 ) , mutabilityNot ) ) + ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 30 ) , mutabilityNot ) ) + ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) + ListItem ( typedValue ( thunk ( rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 4 ) , projection: .ProjectionElems ) ) ) , ty ( 31 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 26 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) + ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 32 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 33 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) + ListItem ( typedValue ( thunk ( rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 9 ) , projection: .ProjectionElems ) ) ) , ty ( 34 ) , mutabilityMut ) ) + ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) + ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 32 ) , mutabilityMut ) ) - ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) - ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 26 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 25 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 30 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 25 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) ) - ListItem ( newLocal ( ty ( 26 ) , mutabilityMut ) ) - ListItem ( newLocal ( ty ( 32 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 33 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 34 ) , mutabilityMut ) ) - ListItem ( newLocal ( ty ( 32 ) , 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/test_integration.py b/kmir/src/tests/integration/test_integration.py index d4734dac8..4202094c7 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -157,7 +157,7 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo 'closure-call', EXEC_DATA_DIR / 'call-with-args' / 'closure-call.smir.json', EXEC_DATA_DIR / 'call-with-args' / 'closure-call.state', - 30, + None, ), ( 'assign-cast', From 14a9f97f94a0e10640355770eab71680e4c9ccb3 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 7 Nov 2025 23:09:43 +1100 Subject: [PATCH 5/9] Split tuple-args rule in two to avoid undefined terms in side condition --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 39 ++++++++++++++++++++--- 1 file changed, 35 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index bfc3e7e92..c80319cc5 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -415,6 +415,8 @@ The first argument of the closure is its environment. Its type is currently not extracted (KMIR does not currently support variable-capturing) and it is not initialised. The second argument is a _tuple_ of all the arguments, however the function body expects these arguments as single locals. +This should be indicated by the `spread_arg` field in the function body but it isn't more often than not. + ```k // reserve space for local variables and copy/move arguments from a tuple inside the old locals into their place rule [setupCalleeClosure]: #setUpCalleeData( @@ -430,8 +432,8 @@ The second argument is a _tuple_ of all the arguments, however the function body _ => toKList(BLOCKS) LOCALS => #reserveFor(NEWLOCALS) - - (ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved))) + + (ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved))) _:List // assumption: arguments stored as _1 .. _n before actual "local" data @@ -441,10 +443,39 @@ The second argument is a _tuple_ of all the arguments, however the function body andBool 0 <=Int TUPLE andBool TUPLE Ty) ==K typeInfoVoidType // closure types don't get extracted at the moment + andBool typeInfoVoidType ==K lookupTy(tyOfLocal(getLocal(LOCALS, CLOSURE))) + // either the closure ref type is missing from type table [priority(40), preserves-definedness] + rule [setupCalleeClosure2]: #setUpCalleeData( + monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))), + operandMove(place(local(CLOSURE:Int), .ProjectionElems)) + operandMove(place(local(TUPLE), .ProjectionElems)) + .Operands + ) + => + #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST) + ... + + + _ => toKList(BLOCKS) + LOCALS => #reserveFor(NEWLOCALS) + + (ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved))) + _:List + + // assumption: arguments stored as _1 .. _n before actual "local" data + ... + + requires 0 <=Int CLOSURE andBool CLOSURE Ty) ==K typeInfoVoidType + [priority(45), preserves-definedness] + syntax Bool ::= isTupleType ( TypeInfo ) [function, total] | isRefType ( TypeInfo ) [function, total] // ------------------------------------------------------- From c6fb79ac0629d95c9cd3407eeeba645acfab4d37 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 7 Nov 2025 23:16:06 +1100 Subject: [PATCH 6/9] add test for second case (derived from p-token) --- .../integration/data/prove-rs/and_then_closure.rs | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100755 kmir/src/tests/integration/data/prove-rs/and_then_closure.rs diff --git a/kmir/src/tests/integration/data/prove-rs/and_then_closure.rs b/kmir/src/tests/integration/data/prove-rs/and_then_closure.rs new file mode 100755 index 000000000..22f2534ac --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/and_then_closure.rs @@ -0,0 +1,11 @@ +use std::result::Result; + +fn wrap(x: &u32) -> Result<&u32, u8> { Ok(x) } + +fn main() { + let single: u32 = 32; + + let wrapped: Result = wrap(&single).and_then(|x: &u32| if *x <= 42 {Ok(42)} else {Err(43)}); + + assert_eq!(wrapped, Ok(42)); +} From 8860238a51af27b48370c116afbf9d9b7cad41f6 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 8 Nov 2025 10:12:13 +1100 Subject: [PATCH 7/9] adjust step count in two-crate-bin test --- .../data/crate-tests/two-crate-bin/crate2::main.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 224160f42..edb35463e 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 │ -│ (730 steps) +│ (727 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ From 4b9222e43c2279baeb2d3f8e55274d1adfc13990 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Sat, 8 Nov 2025 12:15:44 +1100 Subject: [PATCH 8/9] avoid getLocal function for tuple args rule (problems in p-token) --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index c80319cc5..4041b69aa 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -427,6 +427,7 @@ This should be indicated by the `spread_arg` field in the function body but it i ) => #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST) + // arguments are tuple components, stored as _2 .. _n ... @@ -436,14 +437,14 @@ This should be indicated by the `spread_arg` field in the function body but it i (ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved))) _:List - // assumption: arguments stored as _1 .. _n before actual "local" data ... requires 0 <=Int CLOSURE andBool CLOSURE TypedLocal))) + andBool isTypedLocal(LOCALS[CLOSURE]) + andBool typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)) // either the closure ref type is missing from type table [priority(40), preserves-definedness] @@ -455,6 +456,7 @@ This should be indicated by the `spread_arg` field in the function body but it i ) => #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST) + // arguments are tuple components, stored as _2 .. _n ... @@ -464,16 +466,17 @@ This should be indicated by the `spread_arg` field in the function body but it i (ListItem(CALLERFRAME => #updateStackLocal(#updateStackLocal(CALLERFRAME, TUPLE, Moved), CLOSURE, Moved))) _:List - // assumption: arguments stored as _1 .. _n before actual "local" data ... requires 0 <=Int CLOSURE andBool CLOSURE Ty) ==K typeInfoVoidType + andBool isTypedValue(LOCALS[TUPLE]) + andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal))) + andBool isTypedLocal(LOCALS[CLOSURE]) + // or the closure ref type pointee is missing from the type table + andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) + andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))) + andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType [priority(45), preserves-definedness] syntax Bool ::= isTupleType ( TypeInfo ) [function, total] From 83bf05824450f8bad9ffc92fd2f3c30c919fb1e2 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 10 Nov 2025 10:28:49 +1100 Subject: [PATCH 9/9] add more explanation for what is happening in the closure call convention rules --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 4041b69aa..991777e2d 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -415,7 +415,14 @@ The first argument of the closure is its environment. Its type is currently not extracted (KMIR does not currently support variable-capturing) and it is not initialised. The second argument is a _tuple_ of all the arguments, however the function body expects these arguments as single locals. -This should be indicated by the `spread_arg` field in the function body but it isn't more often than not. +Using this calling convention should be indicated by the `spread_arg` field in the function body.[^spread_arg] +However, this field is usually `None` for _closures_, it is only set for internal functions of the Rust execution mechanism. +Therefore a heuristics is used here: +* The function has two arguments, +* the 1st argument has an unknown type (or refers to one), +* and the 2nd argument is a tuple. + +[^spread_arg]: https://doc.rust-lang.org/beta/nightly-rustc/rustc_public/mir/body/struct.Body.html#structfield.spread_arg ```k // reserve space for local variables and copy/move arguments from a tuple inside the old locals into their place