diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 3b117a94c..94b101193 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -305,21 +305,33 @@ The call stack is not necessarily empty at this point so it is left untouched. `Call` is calling another function, setting up its stack frame and where the returned result should go. - ```k - // Intrinsic function call - execute directly without state switching - rule [termCallIntrinsic]: #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, _UNWIND), _SPAN)) ~> _ - => - #execIntrinsic(lookupFunction(#tyOfCall(FUNC)), ARGS, DEST) ~> #continueAt(TARGET) + syntax KItem ::= #execTerminatorCall(fty: Ty, func: MonoItemKind, args: Operands, destination: Place, target: MaybeBasicBlockIdx, unwind: UnwindAction) + + rule #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), _SPAN)) + => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND) + ... - requires isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC))) + + rule #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), _SPAN)) + => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND) + ... + + LOCALS + + // Intrinsic function call - execute directly without state switching + rule [termCallIntrinsic]: + #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND) ~> _ + => #execIntrinsic(FUNC, ARGS, DEST) ~> #continueAt(TARGET) + + requires isIntrinsicFunction(FUNC) // Regular function call - full state switching and stack setup - rule [termCallFunction]: #execTerminator(terminator(terminatorKindCall(FUNC, ARGS, DEST, TARGET, UNWIND), _SPAN)) ~> _ - => - #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS) + rule [termCallFunction]: + #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND) ~> _ + => #setUpCalleeData(FUNC, ARGS) - CALLER => #tyOfCall(FUNC) + CALLER => FTY _ OLDCALLER => CALLER @@ -329,7 +341,7 @@ where the returned result should go. LOCALS STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK - requires notBool isIntrinsicFunction(lookupFunction(#tyOfCall(FUNC))) + requires notBool isIntrinsicFunction(FUNC) syntax Bool ::= isIntrinsicFunction(MonoItemKind) [function] rule isIntrinsicFunction(IntrinsicFunction(_)) => true @@ -338,11 +350,6 @@ where the returned result should go. syntax KItem ::= #continueAt(MaybeBasicBlockIdx) rule #continueAt(someBasicBlockIdx(TARGET)) => #execBlockIdx(TARGET) ... rule #continueAt(noBasicBlockIdx) => .K ... - - 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. @@ -412,7 +419,8 @@ 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 - rule #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems))) + // TODO: This is not safe, need to add more checks to this. + rule #setArgFromStack(IDX, operandMove(place(local(I), _))) => #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I))) ... diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index f392edda3..5cb8b44f2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -130,6 +130,17 @@ Constant operands are simply decoded according to their type. requires typeInfoVoidType =/=K lookupTy(TY) ``` +Function pointers are zero-sized constants whose `Ty` is a key in the function table instaed of the type table. + +```k + rule operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, ty(ID) #as TY, _))) + => FunPtr(TY) + ... + + requires typeInfoVoidType ==K lookupTy(TY) // not a valid type info + andBool lookupFunction(TY) =/=K monoItemFn(symbol("** UNKNOWN FUNCTION **"), defId(ID), noBody ) // valid function Ty +``` + ### Copying and Moving When an operand is `Copied` by a read, the original remains valid (see `false` passed to `#readProjection`). diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md index 23accb633..676784869 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md @@ -51,6 +51,8 @@ The special `Moved` value represents values that have been used and should not b [symbol(Value::PtrLocal)] // pointer to a local TypedValue (on the stack) // fields are the same as in Reference + | FunPtr ( Ty ) + // function pointer, created by operandConstant only. Ty is a key in the function table | AllocRef ( AllocId , ProjectionElems , Metadata ) [symbol(Value::AllocRef)] // reference to static allocation, by AllocId, possibly projected, carrying metadata if applicable diff --git a/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected b/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected index 0830f38dd..2609e8676 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected +++ b/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::a_module::twice.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (42 steps) +│ (44 steps) ├─ 3 (split) │ #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 18446744073709 ┃ diff --git a/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected b/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected index 6d3fe2a15..3edeb4f48 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/single-bin/single_exe::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (225 steps) +│ (228 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected b/kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected index 3bc5d0564..76fa2d153 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected +++ b/kmir/src/tests/integration/data/crate-tests/single-dylib/small_test_dylib::add.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (34 steps) +│ (35 steps) ├─ 3 (split) │ #expect ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709 ┃ diff --git a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected b/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected index b46c39ba9..36e7fa6a7 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected +++ b/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (112 steps) +│ (114 steps) ├─ 3 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) ┃ @@ -14,7 +14,7 @@ ┃ ├─ 4 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) ┃ │ -┃ │ (5 steps) +┃ │ (6 steps) ┃ └─ 6 (stuck, leaf) ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , ┃ @@ -25,7 +25,7 @@ ├─ 5 │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) │ - │ (181 steps) + │ (182 steps) ├─ 7 (terminal) │ #EndProgram ~> .K │ 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 edb35463e..9dbc45230 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 │ -│ (727 steps) +│ (736 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected index 9c905f5d3..bd3076868 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (212 steps) +│ (216 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs b/kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs new file mode 100644 index 000000000..39cdce47a --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs @@ -0,0 +1,27 @@ +use std::convert::TryFrom; +use std::array; + +// inspired by solana-pubkey but very simple code +#[allow(dead_code)] +struct EightBytes([u8;8]); + +impl From<[u8;8]> for EightBytes { + fn from(bytes: [u8;8]) -> Self { Self(bytes) } +} + +// causing problems with the extraction +// the `try_from` and `from` from stdlib are not available in the SMIR +impl TryFrom<&[u8]> for EightBytes { + type Error = array::TryFromSliceError; + fn try_from(bytes: &[u8]) -> Result { + <[u8;8]>::try_from(bytes).map(Self::from) + } +} + +fn main() { + let bytes: [u8;8] = [1,2,3,4,5,6,7,8]; + let _unused = EightBytes::from(bytes); + let slice: &[u8] = &bytes; + let thing: Result = EightBytes::try_from(slice); + assert!(thing.is_ok()); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected index f0468d340..cdb5d7e6d 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (8 steps) +│ (10 steps) └─ 3 (stuck, leaf) #ProgramError ( AssertInhabitedFailure ) ~> .K function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected index fb58b9478..bd2fdf0a9 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-custom-printer.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: src/rust/library/std/src/rt.rs:194 │ -│ (6 steps) +│ (7 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected index fb58b9478..bd2fdf0a9 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assert-true.main.cli-default-printer.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: src/rust/library/std/src/rt.rs:194 │ -│ (6 steps) +│ (7 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected index 70f5cb7ce..3fe017dcf 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (147 steps) +│ (148 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected index 6c2435bcb..700446f6e 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (59 steps) +│ (61 steps) └─ 3 (stuck, leaf) #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected b/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected index 1aca3e132..6cf403b84 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (830 steps) +│ (837 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected index 07ddc99a8..44581b4f2 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (866 steps) +│ (877 steps) └─ 3 (stuck, leaf) #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected index 5d1bd2ecc..9ab92745c 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (151 steps) +│ (154 steps) ├─ 3 │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected index dcc3159dd..70f8119ac 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (1990 steps) +│ (2000 steps) └─ 3 (stuck, leaf) #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio span: 146 diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected index bd2f040cd..8ea34ecd8 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (487 steps) +│ (491 steps) └─ 3 (stuck, leaf) #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place ( .. span: 219 diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected index a99c05167..a9a6646e9 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (105 steps) +│ (106 steps) ├─ 3 │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected index 1c1d0972f..586c10ed1 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (731 steps) +│ (740 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected index 18b68c6ca..b9454d080 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: src/rust/library/std/src/rt.rs:194 │ -│ (13 steps) +│ (14 steps) ├─ 3 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 3 ) ) │ function: foo @@ -94,11 +94,11 @@ Node roles (exclusive): Leaf paths from init: total leaves (non-root): 1 reachable leaves : 1 - total steps : 33 + total steps : 34 - leaf 2 (path 1/3): steps 33, path 1 -> 3 -> 5 -> 7 -> 9 -> 11 -> 2 - leaf 2 (path 2/3): steps 46, path 1 -> 3 -> 4 -> 6 -> 2 - leaf 2 (path 3/3): steps 47, path 1 -> 3 -> 5 -> 7 -> 8 -> 10 -> 2 + leaf 2 (path 1/3): steps 34, path 1 -> 3 -> 5 -> 7 -> 9 -> 11 -> 2 + leaf 2 (path 2/3): steps 47, path 1 -> 3 -> 4 -> 6 -> 2 + leaf 2 (path 3/3): steps 48, path 1 -> 3 -> 5 -> 7 -> 8 -> 10 -> 2 LEAF CELLS --------------- diff --git a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected index c827518af..5be59f517 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (31 steps) +│ (34 steps) └─ 3 (stuck, leaf) #traverseProjection ( toLocal ( 1 ) , thunk ( #decodeConstant ( constantKindAllo span: 48 diff --git a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected index 625a74261..1a3c758c5 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (43 steps) +│ (44 steps) ├─ 3 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) ┃ @@ -15,7 +15,7 @@ ┃ ├─ 4 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) ┃ │ -┃ │ (5 steps) +┃ │ (6 steps) ┃ └─ 6 (stuck, leaf) ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , ┃ span: 32 @@ -27,7 +27,7 @@ ├─ 5 │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) │ - │ (209 steps) + │ (211 steps) ├─ 7 │ #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset ( │ span: 87 @@ -51,7 +51,7 @@ ┃ ┃ │ #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( range ( #map ┃ ┃ │ span: 87 ┃ ┃ │ - ┃ ┃ │ (113 steps) + ┃ ┃ │ (114 steps) ┃ ┃ └─ 13 (stuck, leaf) ┃ ┃ #traverseProjection ( toLocal ( 5 ) , Range ( range ( #mapOffset ( ARG_ARRAY1:Li ┃ ┃ span: 97 diff --git a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected index f7d8e97bb..7be3f4dd4 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (119 steps) +│ (120 steps) ├─ 3 │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected index dba616fbf..d75e7ed57 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (51 steps) +│ (52 steps) ├─ 3 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) ┃ diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected index 8dd5ab168..ea8ab05c1 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: src/rust/library/std/src/rt.rs:194 │ -│ (563 steps) +│ (566 steps) └─ 3 (stuck, leaf) #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , span: no-location:0 @@ -25,9 +25,9 @@ Node roles (exclusive): Leaf paths from init: total leaves (non-root): 1 reachable leaves : 1 - total steps : 563 + total steps : 566 - leaf 3: steps 563, path 1 -> 3 + leaf 3: steps 566, path 1 -> 3 LEAF CELLS --------------- diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected index 47fb9f7be..ef7740af7 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (563 steps) +│ (566 steps) └─ 3 (stuck, leaf) #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected index c1d466815..a3abc238d 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (60 steps) +│ (61 steps) ├─ 3 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) ) ┃ @@ -27,7 +27,7 @@ ┃ ┃ ├─ 8 ┃ ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) ) ┃ ┃ │ -┃ ┃ │ (5 steps) +┃ ┃ │ (6 steps) ┃ ┃ └─ 10 (stuck, leaf) ┃ ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , ┃ ┃ span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected index 72b241b12..a0ac24cae 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (296 steps) +│ (297 steps) ├─ 3 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) ) ┃ @@ -15,7 +15,7 @@ ┃ ├─ 4 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) ) ┃ │ -┃ │ (582 steps) +┃ │ (588 steps) ┃ ├─ 6 (terminal) ┃ │ #EndProgram ~> .K ┃ │ @@ -43,7 +43,7 @@ ┃ ├─ 8 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) ) ┃ │ - ┃ │ (99 steps) + ┃ │ (101 steps) ┃ └─ 10 (stuck, leaf) ┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local ┃ @@ -66,7 +66,7 @@ ┃ ├─ 12 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) ) ┃ │ - ┃ │ (99 steps) + ┃ │ (101 steps) ┃ └─ 14 (stuck, leaf) ┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local ┃ @@ -89,7 +89,7 @@ ┃ ├─ 16 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) ) ┃ │ - ┃ │ (16 steps) + ┃ │ (17 steps) ┃ └─ 18 (stuck, leaf) ┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 0 , place ( ... local: local ┃ @@ -112,7 +112,7 @@ ┃ ├─ 20 ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) ) ┃ │ - ┃ │ (68 steps) + ┃ │ (70 steps) ┃ └─ 22 (stuck, leaf) ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , ┃ span: 32 diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected index 2e11278e4..12948003f 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-maybe-uninit-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (15 steps) +│ (16 steps) └─ 3 (stuck, leaf) #ProgramError ( #UBInvalidTransmuteMaybeUninit ) ~> #freezer#setLocalValue(_,_)_ diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected index c9241f5cf..ce7aaeddb 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (100 steps) +│ (102 steps) └─ 3 (stuck, leaf) #traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllo span: 153 diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected index 5b55f313b..4d7658d18 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (14 steps) +│ (15 steps) └─ 3 (stuck, leaf) #ProgramError ( #UBErrorInvalidDiscriminantsInEnumCast ) ~> .K function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected index 8f15113d5..dea9bd948 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/unions-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (75 steps) +│ (76 steps) └─ 3 (stuck, leaf) #traverseProjection ( toLocal ( 1 ) , Union ( fieldIdx ( 0 ) , Integer ( -1 , 8 function: main diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 170b4da54..f3e172edd 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -154,13 +154,13 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo 'main-a-b-c --depth 20', EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.smir.json', EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.state', - 20, + 24, ), ( 'call-with-args', EXEC_DATA_DIR / 'call-with-args' / 'main-a-b-with-int.smir.json', EXEC_DATA_DIR / 'call-with-args' / 'main-a-b-with-int.state', - 30, + 33, ), ( 'closure-call', @@ -178,7 +178,7 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo 'structs-tuples', EXEC_DATA_DIR / 'structs-tuples' / 'structs-tuples.smir.json', EXEC_DATA_DIR / 'structs-tuples' / 'structs-tuples.state', - 99, + 101, ), ( 'struct-field-update', @@ -246,7 +246,7 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo EXEC_DATA_DIR / 'references' / 'weirdRefs.state', None, ), - ('enum-discriminants', EXEC_DATA_DIR / 'enum' / 'enum.smir.json', EXEC_DATA_DIR / 'enum' / 'enum.state', 135), + ('enum-discriminants', EXEC_DATA_DIR / 'enum' / 'enum.smir.json', EXEC_DATA_DIR / 'enum' / 'enum.state', 136), ( 'Array-indexing', EXEC_DATA_DIR / 'arrays' / 'array_indexing.smir.json', @@ -275,7 +275,7 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo 'pointer-cast-zst', EXEC_DATA_DIR / 'pointers' / 'pointer-cast-zst.smir.json', EXEC_DATA_DIR / 'pointers' / 'pointer-cast-zst.state', - 48, + 50, ), ( 'ref-ptr-cases',