diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 168958fd6..265de567a 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmir" -version = "0.3.69" +version = "0.3.70" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index fa0ad930a..d00e05619 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.69' +VERSION: Final = '0.3.70' diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md b/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md index 7c6737a6b..bf9985a0b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir-ast.md @@ -23,7 +23,7 @@ module KMIR-AST | functionIntrinsic(Symbol) [symbol(FunctionKind::IntrinsicSym), group(mir-enum)] | functionNoop(Symbol) [symbol(FunctionKind::NoOpSym), group(mir-enum)] - syntax FunctionName ::= functionName(MIRInt, FunctionKind) + syntax FunctionName ::= functionName(Ty, FunctionKind) [symbol(functionName), group(mir)] syntax FunctionNames ::= List [group(mir-klist-FunctionName)] diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 194b817b8..8a29a05f9 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -8,7 +8,7 @@ requires "kmir-ast.md" The MIR syntax is largely defined in [KMIR-AST](./kmir-ast.md) and its submodules. The execution is initialised based on a loaded `Pgm` read -from a json format of stable-MIR. +from a json format of stable-MIR, and the name of the function to execute. ```k module KMIR-SYNTAX @@ -16,7 +16,7 @@ module KMIR-SYNTAX imports INT-SYNTAX imports FLOAT-SYNTAX - syntax KItem ::= #init( Pgm ) + syntax KItem ::= #init( Pgm, Symbol ) //////////////////////////////////////////// // FIXME things below related to memory and @@ -64,35 +64,34 @@ module KMIR-CONFIGURATION imports KMIR-SYNTAX imports INT-SYNTAX - syntax RetVal ::= "NoRetVal" - | Int // FIXME is this enough? + syntax RetVal ::= MaybeValue - syntax StackFrame ::= StackFrame(caller:DefId, // index of caller function - dest:Place, // place to store return value - target:BasicBlockIdx, // basic block to return to - UnwindAction, // action to perform on panic - locals:List) // return val, args, local variables + syntax StackFrame ::= StackFrame(caller:Ty, // index of caller function + dest:Place, // place to store return value + target:MaybeBasicBlockIdx, // basic block to return to + UnwindAction, // action to perform on panic + locals:List) // return val, args, local variables configuration - #init($PGM:Pgm) - NoRetVal - defId(-1) // necessary to retrieve caller + #init($PGM:Pgm, symbol("main")) + NoValue + ty(-1) // to retrieve caller // unpacking the top frame to avoid frequent stack read/write operations .List - defId(-1) + ty(-1) place(local(-1), .ProjectionElems) - basicBlockIdx(-1) + noBasicBlockIdx unwindActionUnreachable .List // remaining call stack (without top frame) .List - // FIXME where do we put the "GlobalAllocs"? in the heap, presumably? - // function store, Int -> Body + // function store, Ty -> MonoItemFn .Map // heap .Map // FIXME unclear how to model + // FIXME where do we put the "GlobalAllocs"? in the heap, presumably? endmodule ``` @@ -117,75 +116,121 @@ function map and the initial memory have to be set up. ```k // #init step, assuming a singleton in the K cell - rule #init(_Name:Symbol _Allocs:GlobalAllocs _Functions:FunctionNames Items:MonoItems) + rule #init(_Name:Symbol _Allocs:GlobalAllocs Functions:FunctionNames Items:MonoItems, FuncName) => - #execMain(#findMainItem(Items)) + #execFunction(#findItem(Items, FuncName), Functions) - _ => #mkFunctionMap(Items) + _ => #mkFunctionMap(Functions, Items) ``` -The `Map` of `functions` is keyed on the `DefId` of each `MonoItemFn` -found in the `MonoItems` of the program. The function _names_ are -not relevant for execution and therefore dropped. - -```k - syntax Map ::= #mkFunctionMap ( MonoItems ) [ function, total ] - | #accumFunctions ( Map, MonoItems ) [ function, total ] +The `Map` of `functions` is constructed from the lookup table of `FunctionNames`, +composed with a secondary lookup of `Item`s via `symbolName`. This composed map will +only be populated for `MonoItemFn` items that are indeed _called_ in the code (i.e., +they are callee in a `Call` terminator within an `Item`). - rule #mkFunctionMap(Items) => #accumFunctions(.Map, Items) +The function _names_ and _ids_ are not relevant for calls and therefore dropped. - // accumulate function map discarding duplicate IDs - rule #accumFunctions(Acc, .MonoItems) => Acc - - rule #accumFunctions(Acc, monoItem(_, monoItemFn(_, Id, Body)) Rest:MonoItems) +```k + syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total ] + | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ] + | #accumItems ( Map, MonoItems ) [ function, total ] + + rule #mkFunctionMap(Functions, Items) + => + #accumFunctions(#mainIsMinusOne(Items), #accumItems(.Map, Items), Functions) + //////////////////// ^^^^^^^^^^^^^^^^^^^^^^ HACK Adds "main" as function with ty(-1) + syntax Map ::= #mainIsMinusOne(MonoItems) [function] + rule #mainIsMinusOne(ITEMS) => ty(-1) |-> monoItemKind(#findItem(ITEMS, symbol("main"))) + //////////////////////////////////////////////////////////////// + + // accumulate map of symbol_name -> function (MonoItemFn), discarding duplicate IDs + rule #accumItems(Acc, .MonoItems) => Acc + + rule #accumItems(Acc, monoItem(SymName, monoItemFn(_, _, _) #as Function) Rest:MonoItems) => - #accumFunctions(Acc (Id |-> Body), Rest) - requires notBool (Id in_keys(Acc)) + #accumItems(Acc (SymName |-> Function), Rest) + requires notBool (SymName in_keys(Acc)) [ preserves-definedness ] // key collisions checked - // discard other items and duplicate IDs - rule #accumFunctions(Acc, _:MonoItem Rest:MonoItems) + // discard other items and duplicate symbolNames + rule #accumItems(Acc, _:MonoItem Rest:MonoItems) => - #accumFunctions(Acc, Rest) + #accumItems(Acc, Rest) + [ owise ] + + // accumulate composed map of Ty -> MonoItemFn, using item map from before and function names + rule #accumFunctions(Acc, _, .List) => Acc + + rule #accumFunctions(Acc, ItemMap, ListItem(functionName(TyIdx, functionNormalSym(SymName))) Rest ) + => + #accumFunctions(Acc (TyIdx |-> ItemMap[SymName]), ItemMap, Rest) + requires SymName in_keys(ItemMap) + andBool notBool (TyIdx in_keys(Acc)) + [preserves-definedness] + + // TODO handle NoOpSym and IntrinsicSym cases here + + // discard anything else: + // - duplicate Ty mappings (impossible by construction in stable-mir-json) + // - unknown symbol_name (impossible by construction in stable-mir-json) + rule #accumFunctions(Acc, ItemMap, ListItem(_) Rest) + => + #accumFunctions(Acc, ItemMap, Rest) [ owise ] + ``` -Executing the `main` function means to create the `currentFrame` data +Executing a given named function means to create the `currentFrame` data structure from its function body and then execute the first basic -block of the body. +block of the body. The function's `Ty` index in the `functions` map must +be known to populate the `currentFunc` field. ```k - // `main` is found through its MonoItemFn.name - syntax MonoItemKind ::= #findMainItem ( MonoItems ) [ function ] + // find function through its MonoItemFn.name + syntax MonoItem ::= #findItem ( MonoItems, Symbol ) [ function ] - rule #findMainItem( monoItem(_, monoItemFn(NAME, ID, BODY)) _ ) + rule #findItem( (monoItem(_, monoItemFn(N, _, _)) #as ITEM) _REST, NAME ) => - monoItemFn(NAME, ID, BODY) - requires NAME ==K symbol("main") - rule #findMainItem( _:MonoItem Rest:MonoItems ) + ITEM + requires N ==K NAME + rule #findItem( _:MonoItem REST:MonoItems, NAME ) => - #findMainItem(Rest) + #findItem(REST, NAME) [owise] - // rule #findMainItem( .MonoItems ) => error! + // rule #findItem( .MonoItems, _NAME) => error! - syntax KItem ::= #execMain ( MonoItemKind ) + syntax KItem ::= #execFunction ( MonoItem, FunctionNames ) - // NB differs from arbitrary function execution only by not pushing a stack frame - rule #execMain(monoItemFn(_, ID, body(FIRST:BasicBlock _ #as BLOCKS, LOCALS, _, _, _, _) .Bodies)) + rule #execFunction( + monoItem( + SYMNAME, + monoItemFn(_, _, body(FIRST:BasicBlock _ #as BLOCKS,LOCALS, _, _, _, _) .Bodies) + ), + FUNCTIONNAMES + ) => #execBlock(FIRST) ... - _ => ID + _ => #tyFromName(SYMNAME, FUNCTIONNAMES) _ => toKList(BLOCKS) - _ => defId(-1) + _ => ty(-1) // no caller _ => place(local(-1), .ProjectionElems) - _ => basicBlockIdx(-1) - _ => unwindActionUnreachable // FIXME + _ => noBasicBlockIdx + _ => unwindActionUnreachable _ => #reserveFor(LOCALS) + syntax Ty ::= #tyFromName( Symbol, FunctionNames ) [function] + + rule #tyFromName(NAME, ListItem(functionName(TY, FNAME)) _) => TY + requires NAME ==K FNAME + rule #tyFromName(NAME, ListItem(_) REST:List) => #tyFromName(NAME, REST) + [owise] + + rule #tyFromName(_, .List) => ty(-1) // HACK see #mainIsMinusOne above + syntax List ::= toKList(BasicBlocks) [function, total] rule toKList( .BasicBlocks ) => .List @@ -197,7 +242,7 @@ block of the body. rule #reserveFor(.LocalDecls) => .List - rule #reserveFor(_:LocalDecl REST:LocalDecls) => ListItem(Any) #reserveFor(REST) + rule #reserveFor(_:LocalDecl REST:LocalDecls) => ListItem(NoValue) #reserveFor(REST) ``` Executing a function body consists of repeated calls to `#execBlock` @@ -339,43 +384,52 @@ the stack frame. Execution continues with the context of the enclosing stack frame, at the _target_. ```k - rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) + rule #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ => - #execBlockIdx(TARGET) - ... + #execBlockIdx(TARGET) ~> .K + _ => CALLER // _ => #getBlocks(FUNCS, CALLER) - CALLER => NEWCALLER + CALLER => NEWCALLER DEST => NEWDEST - TARGET => NEWTARGET + someBasicBlockIdx(TARGET) => NEWTARGET _ => UNWIND - ListItem(L0) _ => #setLocal(LOCALS, DEST, L0) + LOCALS => #setLocal(NEWLOCALS, DEST, {LOCALS[0]}:>MaybeValue ) // // remaining call stack (without top frame) - ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, LOCALS)) STACK => STACK + ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK FUNCS requires CALLER in_keys(FUNCS) + andBool 0 #getBlocksAux({FUNCS[ID]}:>Bodies) + rule #getBlocks(FUNCS, ID) => #getBlocksAux({FUNCS[ID]}:>MonoItemKind) requires ID in_keys(FUNCS) - andBool isBodies(FUNCS[ID]) // returns blocks from the _first_ body if there are several - rule #getBlocksAux(.Bodies) => .List - rule #getBlocksAux(body(BLOCKS, _, _, _, _, _) _) => toKList(BLOCKS) + // TODO handle cases with several blocks + rule #getBlocksAux(monoItemFn(_, _, .Bodies)) => .List + rule #getBlocksAux(monoItemFn(_, _, body(BLOCKS, _, _, _, _, _) _)) => toKList(BLOCKS) + // other item kinds are not expected or supported + rule #getBlocksAux(monoItemStatic(_, _, _)) => .List // should not occur in calls at all + rule #getBlocksAux(monoItemGlobalAsm(_)) => .List // not supported. FIXME Should error, maybe during #init // set a local to a new value. Assumes the place is valid - syntax List ::= #setLocal(List, Place, Value) [function] + syntax List ::= #setLocal(List, Place, MaybeValue) [function] - rule #setLocal(LOCALS, place(local(I), .ProjectionElems), VALUE) + rule #setLocal(LOCALS, _, NoValue) => - LOCALS[I <- VALUE] + LOCALS + + rule #setLocal(LOCALS, place(local(I), .ProjectionElems), V:Value) + => + LOCALS[I <- V] requires 0 <=Int I andBool I #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ + => + #EndProgram + + _ => {LOCALS[0]}:>MaybeValue + + noBasicBlockIdx + LOCALS + ... + +``` + + `Call` is calling another function, setting up its stack frame and where the returned result should go. -TODO This rule currently causes a sort error because of a mismatch between parsed data for the `Call` terminator and stack frame data/configuration. -``` +```k rule #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) => - #execBlockIdx(basicBlockIdx(0)) + #setUpCalleeData( {FUNCS[#tyOfCall(FUNC)]}:>MonoItemKind, ARGS) ... - CURRENT + CALLER => #tyOfCall(FUNC) - _ => #getBlocks(FUNCS, FUNC) // FIXME FUNC is an _Operand_! - OLDCALLER => CURRENT + _ + OLDCALLER => CALLER OLDDEST => DEST OLDTARGET => TARGET OLDUNWIND => UNWIND - LOCALS => .List // FIXME + LOCALS STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK FUNCS - requires CALLER in_keys(FUNCS) - // andBool #withinLocals(DEST, LOCALS) - [preserves-definedness] // CALLER lookup defined, DEST within locals TODO + requires #tyOfCall(FUNC) in_keys(FUNCS) + [preserves-definedness] // callee lookup defined + + syntax Ty ::= #tyOfCall( Operand ) [function, total] + + rule #tyOfCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _)))) + => Ty + rule #tyOfCall(_) => ty(-1) [owise] // copy, move, non-zero size: not supported +``` + +The local data has to be set up for the call, which requires information about the local variables of a call. This step is separate from the above call stack setup because it needs to retrieve the locals declaration from the body. Arguments to the call are `Operands` which refer to the old locals (`OLDLOCALS` below), and the data is either _copied_ into the new locals using `#setArgs`, or it needs to be _shared_ via references into the heap, i.e., the reference needs to be copied +(NB: A function won't ever access any other function call's `local` variables). + +```k + syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands) + + // reserve space for local variables and copy arguments from old locals into their place + rule #setUpCalleeData( + monoItemFn(_, _, body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _) _:Bodies), + ARGS + ) + => + #execBlock(FIRST) + ... + + // CALLEE + + _ => toKList(BLOCKS) + // CALLER + // DEST + // TARGET + // UNWIND + OLDLOCALS => #setArgs(OLDLOCALS, 1, ARGS, #reserveFor(NEWLOCALS)) + // assumption: arguments stored as _1 .. _n before actual "local" data + ... + + + syntax List ::= #setArgs ( List, Int, Operands, List) [function] + + rule #setArgs(_, _, .Operands, LOCALS) => LOCALS + rule #setArgs(PRIOR_LOCALS, IDX, ARG:Operand ARGS:Operands, ACC) + => + #setArgs( + PRIOR_LOCALS, + IDX +Int 1, + ARGS, + #setLocal(ACC, place(local(IDX), .ProjectionElems), #readValue(PRIOR_LOCALS, ARG)) + ) + + syntax Value ::= #readValue ( List, Operand ) + + rule #readValue(_, _) => Any // FIXME! Not reading anything ``` diff --git a/kmir/src/tests/integration/data/exec-smir/README.md b/kmir/src/tests/integration/data/exec-smir/README.md new file mode 100644 index 000000000..2ad2cdc02 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/README.md @@ -0,0 +1,19 @@ +Small tests for MIR execution +----------------------------- + +The tests below this directory are intended to be run with `kmir run`, comparing the pretty-printed output to an expectation file. + +# To add a new test + +* Write a Rust test program `NAME.rs` +* Generate stable-mir JSON `NAME.smir.json` for the test program (using `deps/stable-mir-pretty`) +* run the program once to generate the expected output state + ``` + /mir-semantics $ poetry -C kmir run -- kmir run path/to/NAME.smir.json > //.run.state + ``` +* check that the output is as expected +* add test to `EXEC_DATA` array in `kmir/src/tests/integration/test_integration.py` +* Several tests can be run from the same `NAME.smir.json` by varying the `--depth` parameter. + + +Ideally, we should also keep the original `NAME.rs` program so we can later update the tests when/if the JSON format changes. diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.15.state b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.15.state new file mode 100644 index 000000000..1e71b4f21 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.15.state @@ -0,0 +1,51 @@ + + + #execStmts ( .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) ~> .K + + + NoValue + + + ty ( 27 ) + + + + ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) ) + + + ty ( 26 ) + + + place (... local: local ( 0 ) , projection: .ProjectionElems ) + + + someBasicBlockIdx ( basicBlockIdx ( 1 ) ) + + + unwindActionContinue + + + ListItem ( NoValue ) + + + + ListItem ( StackFrame ( ty ( 25 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwindActionContinue , ListItem ( NoValue ) ) ) + ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwindActionContinue , ListItem ( NoValue ) ) ) + ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , ListItem ( NoValue ) ) ) + + + ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::" ) , id: defId ( 2 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) .Bodies ) + ty ( 14 ) |-> monoItemFn (... name: symbol ( "<() as std::process::Termination>::report" ) , id: defId ( 5 ) , body: body (... blocks: basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandConstant ( constOperand (... span: span ( 46 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: someByte ( 0 ) .AllocBytes , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityMut ) ) , ty: ty ( 17 ) , id: mirConstId ( 8 ) ) ) ) ) ) , span: span ( 46 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 45 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 17 ) , span: span ( 47 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 1 ) , span: span ( 48 ) , mut: mutabilityNot ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "self" ) , sourceInfo: sourceInfo (... span: span ( 48 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 49 ) ) .Bodies ) + ty ( 19 ) |-> monoItemFn (... name: symbol ( ">::call_once" ) , id: defId ( 3 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 43 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 43 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 43 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 43 ) , mut: mutabilityNot ) .LocalDecls , argCount: 2 , varDebugInfo: .VarDebugInfos , spreadArg: someLocal ( local ( 2 ) ) , span: span ( 43 ) ) .Bodies ) + ty ( 21 ) |-> monoItemFn (... name: symbol ( "<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once" ) , id: defId ( 3 ) , body: body (... blocks: basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindMut (... kind: mutBorrowKindDefault ) , place (... local: local ( 1 ) , projection: .ProjectionElems ) ) ) , span: span ( 43 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 43 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 23 ) , id: mirConstId ( 7 ) ) ) ) , args: operandMove ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) operandMove ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionCleanup ( basicBlockIdx ( 3 ) ) ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindDrop (... place: place (... local: local ( 1 ) , projection: .ProjectionElems ) , target: basicBlockIdx ( 2 ) , unwind: unwindActionContinue ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindDrop (... place: place (... local: local ( 1 ) , projection: .ProjectionElems ) , target: basicBlockIdx ( 4 ) , unwind: unwindActionTerminate ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindResume , span: span ( 43 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 16 ) , span: span ( 43 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 12 ) , span: span ( 43 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 43 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 24 ) , span: span ( 43 ) , mut: mutabilityNot ) .LocalDecls , argCount: 2 , varDebugInfo: .VarDebugInfos , spreadArg: someLocal ( local ( 2 ) ) , span: span ( 43 ) ) .Bodies ) + ty ( 23 ) |-> monoItemFn (... name: symbol ( "std::rt::lang_start::<()>::{closure#0}" ) , id: defId ( 1 ) , body: body (... blocks: basicBlock (... statements: statement (... kind: statementKindStorageLive ( local ( 2 ) ) , span: span ( 16 ) ) statement (... kind: statementKindStorageLive ( local ( 3 ) ) , span: span ( 15 ) ) statement (... kind: statementKindStorageLive ( local ( 4 ) ) , span: span ( 17 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 1 ) , projection: projectionElemDeref projectionElemField ( fieldIdx ( 0 ) , ty ( 7 ) ) .ProjectionElems ) ) ) ) , span: span ( 17 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 14 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 13 ) , id: mirConstId ( 1 ) ) ) ) , args: operandMove ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 3 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 15 ) ) ) basicBlock (... statements: statement (... kind: statementKindStorageDead ( local ( 4 ) ) , span: span ( 19 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 18 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 14 ) , id: mirConstId ( 2 ) ) ) ) , args: operandMove ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionContinue ) , span: span ( 16 ) ) ) basicBlock (... statements: statement (... kind: statementKindStorageDead ( local ( 3 ) ) , span: span ( 21 ) ) statement (... kind: statementKindStorageLive ( local ( 5 ) ) , span: span ( 22 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 2 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 15 ) ) .ProjectionElems ) ) ) , span: span ( 22 ) ) statement (... kind: statementKindStorageLive ( local ( 6 ) ) , span: span ( 23 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 2 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 15 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 9 ) ) .ProjectionElems ) ) ) ) , span: span ( 23 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindIntToInt , operandMove ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , ty ( 16 ) ) ) , span: span ( 24 ) ) statement (... kind: statementKindStorageDead ( local ( 6 ) ) , span: span ( 25 ) ) statement (... kind: statementKindStorageDead ( local ( 5 ) ) , span: span ( 26 ) ) statement (... kind: statementKindStorageDead ( local ( 2 ) ) , span: span ( 27 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 20 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 16 ) , span: span ( 28 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 11 ) , span: span ( 3 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 17 ) , span: span ( 16 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 1 ) , span: span ( 15 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 17 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 18 ) , span: span ( 22 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 9 ) , span: span ( 23 ) , mut: mutabilityMut ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "main" ) , sourceInfo: sourceInfo (... span: span ( 9 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: projectionElemDeref projectionElemField ( fieldIdx ( 0 ) , ty ( 7 ) ) .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "self" ) , sourceInfo: sourceInfo (... span: span ( 29 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) varDebugInfo (... name: symbol ( "self" ) , sourceInfo: sourceInfo (... span: span ( 30 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 3 ) ) .Bodies ) + ty ( 25 ) |-> monoItemFn (... name: symbol ( "a" ) , id: defId ( 7 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 55 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 26 ) , id: mirConstId ( 10 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 56 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 57 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 58 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 59 ) ) .Bodies ) + ty ( 26 ) |-> monoItemFn (... name: symbol ( "b" ) , id: defId ( 8 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 60 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 27 ) , id: mirConstId ( 11 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 61 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 62 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 63 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 64 ) ) .Bodies ) + ty ( 27 ) |-> monoItemFn (... name: symbol ( "c" ) , id: defId ( 9 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 66 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 67 ) ) .Bodies ) + ty ( -1 ) |-> monoItemFn (... name: symbol ( "main" ) , id: defId ( 6 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 25 ) , id: mirConstId ( 9 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 51 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 52 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 53 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 54 ) ) .Bodies ) + + + .Map + + + diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.rs b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.rs new file mode 100644 index 000000000..8fa612d03 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.rs @@ -0,0 +1,11 @@ +fn main() { + a() +} +fn a() { + b() +} +fn b() { + c() +} +fn c() { +} diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state new file mode 100644 index 000000000..926160ad2 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state @@ -0,0 +1,49 @@ + + + #EndProgram ~> .K + + + NoValue + + + ty ( -1 ) + + + + ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 25 ) , id: mirConstId ( 9 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 51 ) ) ) ) + ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 52 ) ) ) ) + + + ty ( -1 ) + + + place (... local: local ( -1 ) , projection: .ProjectionElems ) + + + noBasicBlockIdx + + + unwindActionUnreachable + + + ListItem ( NoValue ) + + + + .List + + + ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::" ) , id: defId ( 2 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) .Bodies ) + ty ( 14 ) |-> monoItemFn (... name: symbol ( "<() as std::process::Termination>::report" ) , id: defId ( 5 ) , body: body (... blocks: basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandConstant ( constOperand (... span: span ( 46 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: someByte ( 0 ) .AllocBytes , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityMut ) ) , ty: ty ( 17 ) , id: mirConstId ( 8 ) ) ) ) ) ) , span: span ( 46 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 45 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 17 ) , span: span ( 47 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 1 ) , span: span ( 48 ) , mut: mutabilityNot ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "self" ) , sourceInfo: sourceInfo (... span: span ( 48 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 49 ) ) .Bodies ) + ty ( 19 ) |-> monoItemFn (... name: symbol ( ">::call_once" ) , id: defId ( 3 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 43 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 43 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 43 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 43 ) , mut: mutabilityNot ) .LocalDecls , argCount: 2 , varDebugInfo: .VarDebugInfos , spreadArg: someLocal ( local ( 2 ) ) , span: span ( 43 ) ) .Bodies ) + ty ( 21 ) |-> monoItemFn (... name: symbol ( "<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once" ) , id: defId ( 3 ) , body: body (... blocks: basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindMut (... kind: mutBorrowKindDefault ) , place (... local: local ( 1 ) , projection: .ProjectionElems ) ) ) , span: span ( 43 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 43 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 23 ) , id: mirConstId ( 7 ) ) ) ) , args: operandMove ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) operandMove ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionCleanup ( basicBlockIdx ( 3 ) ) ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindDrop (... place: place (... local: local ( 1 ) , projection: .ProjectionElems ) , target: basicBlockIdx ( 2 ) , unwind: unwindActionContinue ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindDrop (... place: place (... local: local ( 1 ) , projection: .ProjectionElems ) , target: basicBlockIdx ( 4 ) , unwind: unwindActionTerminate ) , span: span ( 43 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindResume , span: span ( 43 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 16 ) , span: span ( 43 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 12 ) , span: span ( 43 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 1 ) , span: span ( 43 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 24 ) , span: span ( 43 ) , mut: mutabilityNot ) .LocalDecls , argCount: 2 , varDebugInfo: .VarDebugInfos , spreadArg: someLocal ( local ( 2 ) ) , span: span ( 43 ) ) .Bodies ) + ty ( 23 ) |-> monoItemFn (... name: symbol ( "std::rt::lang_start::<()>::{closure#0}" ) , id: defId ( 1 ) , body: body (... blocks: basicBlock (... statements: statement (... kind: statementKindStorageLive ( local ( 2 ) ) , span: span ( 16 ) ) statement (... kind: statementKindStorageLive ( local ( 3 ) ) , span: span ( 15 ) ) statement (... kind: statementKindStorageLive ( local ( 4 ) ) , span: span ( 17 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 1 ) , projection: projectionElemDeref projectionElemField ( fieldIdx ( 0 ) , ty ( 7 ) ) .ProjectionElems ) ) ) ) , span: span ( 17 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 14 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 13 ) , id: mirConstId ( 1 ) ) ) ) , args: operandMove ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 3 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 15 ) ) ) basicBlock (... statements: statement (... kind: statementKindStorageDead ( local ( 4 ) ) , span: span ( 19 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 18 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 14 ) , id: mirConstId ( 2 ) ) ) ) , args: operandMove ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionContinue ) , span: span ( 16 ) ) ) basicBlock (... statements: statement (... kind: statementKindStorageDead ( local ( 3 ) ) , span: span ( 21 ) ) statement (... kind: statementKindStorageLive ( local ( 5 ) ) , span: span ( 22 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 2 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 15 ) ) .ProjectionElems ) ) ) , span: span ( 22 ) ) statement (... kind: statementKindStorageLive ( local ( 6 ) ) , span: span ( 23 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 2 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 15 ) ) projectionElemField ( fieldIdx ( 0 ) , ty ( 9 ) ) .ProjectionElems ) ) ) ) , span: span ( 23 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindIntToInt , operandMove ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , ty ( 16 ) ) ) , span: span ( 24 ) ) statement (... kind: statementKindStorageDead ( local ( 6 ) ) , span: span ( 25 ) ) statement (... kind: statementKindStorageDead ( local ( 5 ) ) , span: span ( 26 ) ) statement (... kind: statementKindStorageDead ( local ( 2 ) ) , span: span ( 27 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 20 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 16 ) , span: span ( 28 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 11 ) , span: span ( 3 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 17 ) , span: span ( 16 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 1 ) , span: span ( 15 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 7 ) , span: span ( 17 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 18 ) , span: span ( 22 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 9 ) , span: span ( 23 ) , mut: mutabilityMut ) .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "main" ) , sourceInfo: sourceInfo (... span: span ( 9 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: projectionElemDeref projectionElemField ( fieldIdx ( 0 ) , ty ( 7 ) ) .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "self" ) , sourceInfo: sourceInfo (... span: span ( 29 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) varDebugInfo (... name: symbol ( "self" ) , sourceInfo: sourceInfo (... span: span ( 30 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) ) .VarDebugInfos , spreadArg: noLocal , span: span ( 3 ) ) .Bodies ) + ty ( 25 ) |-> monoItemFn (... name: symbol ( "a" ) , id: defId ( 7 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 55 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 26 ) , id: mirConstId ( 10 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 56 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 57 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 58 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 59 ) ) .Bodies ) + ty ( 26 ) |-> monoItemFn (... name: symbol ( "b" ) , id: defId ( 8 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 60 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 27 ) , id: mirConstId ( 11 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 61 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 62 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 63 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 64 ) ) .Bodies ) + ty ( 27 ) |-> monoItemFn (... name: symbol ( "c" ) , id: defId ( 9 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 66 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 67 ) ) .Bodies ) + ty ( -1 ) |-> monoItemFn (... name: symbol ( "main" ) , id: defId ( 6 ) , body: body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 25 ) , id: mirConstId ( 9 ) ) ) ) , args: .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 51 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 52 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 53 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: .VarDebugInfos , spreadArg: noLocal , span: span ( 54 ) ) .Bodies ) + + + .Map + + diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.smir.json b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.smir.json new file mode 100644 index 000000000..5837e58c8 --- /dev/null +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.smir.json @@ -0,0 +1 @@ +{"name":"main_a_b_c","crate_id":2129868149476588123,"allocs":[],"functions":[[14,{"NormalSym":"_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17he57786f330055d2dE"}],[25,{"NormalSym":"_ZN10main_a_b_c1a17hf96e7944faad0bd0E"}],[0,{"NormalSym":"_ZN3std2rt19lang_start_internal17h018b8394ba015d86E"}],[26,{"NormalSym":"_ZN10main_a_b_c1b17hbedf65f2538ce3adE"}],[23,{"NormalSym":"_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h88c62a39fb1b342bE"}],[21,{"NormalSym":"_ZN4core3ops8function6FnOnce9call_once17h5775674bf1184c46E"}],[27,{"NormalSym":"_ZN10main_a_b_c1c17h59101d2318335bbdE"}],[28,{"NoOpSym":""}],[19,{"NormalSym":"_ZN4core3ops8function6FnOnce9call_once17hde47e0bf03682721E"}],[20,{"IntrinsicSym":"black_box"}],[13,{"NormalSym":"_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h98accbb0a20ea4f5E"}]],"uneval_consts":[],"items":[{"symbol_name":"_ZN10main_a_b_c1a17hf96e7944faad0bd0E","mono_item_kind":{"MonoItemFn":{"name":"a","id":7,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":55,"user_ty":null,"const_":{"kind":"ZeroSized","ty":26,"id":10}}},"args":[],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":56}},{"statements":[],"terminator":{"kind":"Return","span":57}}],"locals":[{"ty":1,"span":58,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":59}]}},"details":null},{"symbol_name":"_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17he57786f330055d2dE","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},{"symbol_name":"_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17hba596ab1e21f4dfaE","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":"_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h98accbb0a20ea4f5E","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":"_ZN10main_a_b_c1c17h59101d2318335bbdE","mono_item_kind":{"MonoItemFn":{"name":"c","id":9,"body":[{"blocks":[{"statements":[],"terminator":{"kind":"Return","span":65}}],"locals":[{"ty":1,"span":66,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":67}]}},"details":null},{"symbol_name":"_ZN10main_a_b_c1b17hbedf65f2538ce3adE","mono_item_kind":{"MonoItemFn":{"name":"b","id":8,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":60,"user_ty":null,"const_":{"kind":"ZeroSized","ty":27,"id":11}}},"args":[],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":61}},{"statements":[],"terminator":{"kind":"Return","span":62}}],"locals":[{"ty":1,"span":63,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":64}]}},"details":null},{"symbol_name":"_ZN4core3ops8function6FnOnce9call_once17h5775674bf1184c46E","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_once17hde47e0bf03682721E","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":"_ZN3std2rt10lang_start17he509fe31442a28c4E","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$17h88c62a39fb1b342bE","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":"_ZN10main_a_b_c4main17hcaca459da1b06b9fE","mono_item_kind":{"MonoItemFn":{"name":"main","id":6,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":50,"user_ty":null,"const_":{"kind":"ZeroSized","ty":25,"id":9}}},"args":[],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":51}},{"statements":[],"terminator":{"kind":"Return","span":52}}],"locals":[{"ty":1,"span":53,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":54}]}},"details":null},{"symbol_name":"_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h651e2df3ec0dc2ccE","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}],"debug":null} \ No newline at end of file diff --git a/kmir/src/tests/integration/data/schema-parse/functions/reference.kmir b/kmir/src/tests/integration/data/schema-parse/functions/reference.kmir index 77012364b..57c1399b9 100644 --- a/kmir/src/tests/integration/data/schema-parse/functions/reference.kmir +++ b/kmir/src/tests/integration/data/schema-parse/functions/reference.kmir @@ -1,42 +1,42 @@ ListItem( functionName( - 114, + ty(114), functionNormalSym(symbol("_ZN4core3ptr42drop_in_place$LT$alloc..string..String$GT$17h1018ac0f9e0b0734E")) ) ) ListItem( functionName( - 102, + ty(102), functionNoop(symbol("")) ) ) ListItem( functionName( - 19, + ty(19), functionNormalSym(symbol("_ZN4core3ops8function6FnOnce9call_once17ha726c80bc9e6a2adE")) ) ) ListItem( functionName( - 100, + ty(100), functionNormalSym(symbol("__rust_dealloc")) ) ) ListItem( functionName( - 78, + ty(78), functionIntrinsic(symbol("volatile_load")) ) ) ListItem( functionName( - 27, + ty(27), functionIntrinsic(symbol("ctpop")) ) ) ListItem( functionName( - 109, + ty(109), functionNormalSym(symbol("_ZN10mainfoobar3bar17hc9f701b05bebc012E")) ) ) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 1ea584cdc..107e2e378 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -5,7 +5,7 @@ from typing import TYPE_CHECKING import pytest -from pyk.kast.inner import KApply, KSort, KToken +from pyk.kast.inner import KApply, KSort, KToken, Subst from kmir.convert_from_definition.v2parser import Parser @@ -148,3 +148,53 @@ def test_schema_kapply_parse( json_data, expected_term, expected_sort = test_case assert parser.parse_mir_json(json_data, expected_sort.name) == (expected_term, expected_sort) + + +EXEC_DATA_DIR = (Path(__file__).parent / 'data' / 'exec-smir').resolve(strict=True) +EXEC_DATA = [ + ( + 'main-a-b-c', + EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.smir.json', + EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.run.state', + None, + ), + ( + 'main-a-b-c --depth 15', + EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.smir.json', + EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.15.state', + 15, + ), +] + + +@pytest.mark.parametrize( + 'test_case', + EXEC_DATA, + ids=[name for (name, _, _, _) in EXEC_DATA], +) +def test_exec_smir( + test_case: tuple[str, Path, Path, int], + tools: Tools, +) -> None: + + (_, input_json, output_kast, depth) = test_case + + parser = Parser(tools.definition) + + with input_json.open('r') as f: + json_data = json.load(f) + parsed = parser.parse_mir_json(json_data, 'Pgm') + assert parsed is not None + kmir_kast, _ = parsed + + subst = Subst({'$PGM': kmir_kast}) + init_config = subst.apply(tools.definition.init_config(KSort('GeneratedTopCell'))) + init_kore = tools.krun.kast_to_kore(init_config, KSort('GeneratedTopCell')) + result = tools.krun.run_pattern(init_kore, depth=depth) + + with output_kast.open('r') as f: + expected = f.read().rstrip() + + result_pretty = tools.kprint.kore_to_pretty(result).rstrip() + + assert result_pretty == expected diff --git a/package/version b/package/version index f0e0b7976..bff25c91f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.69 +0.3.70