From 32ebd3b126614e107795acf631a4d08ba88a75f3 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 12 Dec 2025 18:09:13 +0800 Subject: [PATCH 1/8] test: reproduce unkown function call caused by `.map(function_pointer) --- .../data/prove-rs/option-map-fn-ptr-fail.rs | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/option-map-fn-ptr-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/option-map-fn-ptr-fail.rs b/kmir/src/tests/integration/data/prove-rs/option-map-fn-ptr-fail.rs new file mode 100644 index 000000000..f7299a053 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/option-map-fn-ptr-fail.rs @@ -0,0 +1,26 @@ +// Test case reproducing issues: +// - https://github.com/runtimeverification/mir-semantics/issues/891 +// - https://github.com/runtimeverification/mir-semantics/issues/488 +// - https://github.com/runtimeverification/stable-mir-json/issues/55 +// +// Problem: Option::map with a function pointer (not a closure) causes +// "unknown function -1" error because function pointers passed as arguments +// are not included in the `functions` array in stable-mir-json output. +// +// Original example from issue #891: +// .map(u64::from_le_bytes) // fails - function pointer +// +// Workaround: use a closure instead: +// .map(|bytes| u64::from_le_bytes(bytes)) // works + +fn main() { + let bytes: [u8; 8] = [0x15, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]; + let opt: Option<[u8; 8]> = Some(bytes); + + // This fails: passing function pointer to Option::map + // The MIR desugaring of Option::map invokes the function via a pointer, + // but the function is not present in the `functions` array. + let result = opt.map(u64::from_le_bytes); + + assert_eq!(result, Some(21u64)); +} From 8fa43cd030b1e201cc1c7441907e0a84b90e59ab Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 12 Dec 2025 18:27:39 +0800 Subject: [PATCH 2/8] fix: avoid conflicts between main and unkown function -1 --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 2 +- kmir/src/kmir/smir.py | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 3b117a94c..68cf48c78 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -342,7 +342,7 @@ where the returned result should go. 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 + rule #tyOfCall(_) => ty(-2) [owise] // copy, move, non-zero size: not supported (ty(-1) is reserved for main) ``` 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. diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index e40157e50..6357c87e6 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -130,9 +130,10 @@ def function_symbols(self) -> dict[int, dict]: fnc_symbols[-1] = {'NormalSym': self.main_symbol} # function items not present in the SMIR lookup table are added with negative Ty ID + # Note: -2 is reserved for "unsupported call type" in K semantics missing = [name for name in self.items.keys() if {'NormalSym': name} not in fnc_symbols.values()] - fake_ty = -2 + fake_ty = -3 for name in missing: fnc_symbols[fake_ty] = {'NormalSym': name} fake_ty -= 1 From a77144787b707988858f41e41c15a2884241d30f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 15 Dec 2025 16:18:40 +0800 Subject: [PATCH 3/8] support function call from a function pointer --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 42 ++++++++++++-------- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 2 +- kmir/src/kmir/smir.py | 26 +++++++++--- 3 files changed, 46 insertions(+), 24 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 68cf48c78..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(-2) [owise] // copy, move, non-zero size: not supported (ty(-1) is reserved for main) ``` 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..e76814bae 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -159,7 +159,7 @@ In contrast to regular write operations, the value does not have to be _mutable_ LOCALS requires 0 <=Int I andBool I dict[Ty, set[Ty]]: _LOGGER.debug(f'Skipping call edge extraction for {sym}: missing body') called_tys: set[Ty] = set() else: - called_funs = [ - b['terminator']['kind']['Call']['func'] for b in body['blocks'] if 'Call' in b['terminator']['kind'] - ] - called_tys = {Ty(op['Constant']['const_']['ty']) for op in called_funs if 'Constant' in op} - # TODO also add any constant operands used as arguments whose ty refer to a function - # the semantics currently does not support this, see issue #488 and stable-mir-json issue #55 + called_tys = set() + + def collect_const_fun_tys(obj: object) -> None: + # Recursively collect any Constant operands whose type refers to a function. + if isinstance(obj, dict): + if 'Constant' in obj and isinstance(obj['Constant'], dict): + const = obj['Constant'] + const_inner = const.get('const_') + if isinstance(const_inner, dict): + ty_id = const_inner.get('ty') + if isinstance(ty_id, int) and ty_id in self.function_symbols: + called_tys.add(Ty(ty_id)) + for v in obj.values(): + collect_const_fun_tys(v) + elif isinstance(obj, list): + for v in obj: + collect_const_fun_tys(v) + + # Collect direct calls and function items passed as constants (e.g., fn pointers). + collect_const_fun_tys(body) for ty in self.function_symbols_reverse[sym]: result[Ty(ty)] = called_tys return result From 145b2ccab08e7ff044877ea3fdf69b9e7031ec79 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 15 Dec 2025 16:30:36 +0800 Subject: [PATCH 4/8] fix make check --- kmir/src/kmir/smir.py | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/kmir/src/kmir/smir.py b/kmir/src/kmir/smir.py index 28ea9e8e7..c2c3c436f 100644 --- a/kmir/src/kmir/smir.py +++ b/kmir/src/kmir/smir.py @@ -204,6 +204,23 @@ def reduce_to(self, start_name: str) -> SMIRInfo: def call_edges(self) -> dict[Ty, set[Ty]]: # determines which functions are _called_ from others, by symbol name result = {} + + def collect_const_fun_tys(obj: object, called: set[Ty]) -> None: + # Recursively collect any Constant operands whose type refers to a function. + if isinstance(obj, dict): + if 'Constant' in obj and isinstance(obj['Constant'], dict): + const = obj['Constant'] + const_inner = const.get('const_') + if isinstance(const_inner, dict): + ty_id = const_inner.get('ty') + if isinstance(ty_id, int) and ty_id in self.function_symbols: + called.add(Ty(ty_id)) + for v in obj.values(): + collect_const_fun_tys(v, called) + elif isinstance(obj, list): + for v in obj: + collect_const_fun_tys(v, called) + for sym, item in self.items.items(): if not SMIRInfo._is_func(item): continue @@ -218,24 +235,8 @@ def call_edges(self) -> dict[Ty, set[Ty]]: else: called_tys = set() - def collect_const_fun_tys(obj: object) -> None: - # Recursively collect any Constant operands whose type refers to a function. - if isinstance(obj, dict): - if 'Constant' in obj and isinstance(obj['Constant'], dict): - const = obj['Constant'] - const_inner = const.get('const_') - if isinstance(const_inner, dict): - ty_id = const_inner.get('ty') - if isinstance(ty_id, int) and ty_id in self.function_symbols: - called_tys.add(Ty(ty_id)) - for v in obj.values(): - collect_const_fun_tys(v) - elif isinstance(obj, list): - for v in obj: - collect_const_fun_tys(v) - # Collect direct calls and function items passed as constants (e.g., fn pointers). - collect_const_fun_tys(body) + collect_const_fun_tys(body, called_tys) for ty in self.function_symbols_reverse[sym]: result[Ty(ty)] = called_tys return result From 3dd9a33c5f001b617ca91d9d32ba85f9854a9e8a Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 15 Dec 2025 18:57:05 +0800 Subject: [PATCH 5/8] clear code --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 2 +- kmir/src/kmir/smir.py | 30 +++++-------------- .../488-support-function-pointer-calls.rs | 27 +++++++++++++++++ .../data/prove-rs/option-map-fn-ptr-fail.rs | 26 ---------------- 4 files changed, 35 insertions(+), 50 deletions(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/488-support-function-pointer-calls.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/option-map-fn-ptr-fail.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index e76814bae..f392edda3 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -159,7 +159,7 @@ In contrast to regular write operations, the value does not have to be _mutable_ LOCALS requires 0 <=Int I andBool I dict[int, dict]: fnc_symbols[-1] = {'NormalSym': self.main_symbol} # function items not present in the SMIR lookup table are added with negative Ty ID - # Note: -2 is reserved for "unsupported call type" in K semantics missing = [name for name in self.items.keys() if {'NormalSym': name} not in fnc_symbols.values()] - fake_ty = -3 + fake_ty = -2 for name in missing: fnc_symbols[fake_ty] = {'NormalSym': name} fake_ty -= 1 @@ -204,23 +203,6 @@ def reduce_to(self, start_name: str) -> SMIRInfo: def call_edges(self) -> dict[Ty, set[Ty]]: # determines which functions are _called_ from others, by symbol name result = {} - - def collect_const_fun_tys(obj: object, called: set[Ty]) -> None: - # Recursively collect any Constant operands whose type refers to a function. - if isinstance(obj, dict): - if 'Constant' in obj and isinstance(obj['Constant'], dict): - const = obj['Constant'] - const_inner = const.get('const_') - if isinstance(const_inner, dict): - ty_id = const_inner.get('ty') - if isinstance(ty_id, int) and ty_id in self.function_symbols: - called.add(Ty(ty_id)) - for v in obj.values(): - collect_const_fun_tys(v, called) - elif isinstance(obj, list): - for v in obj: - collect_const_fun_tys(v, called) - for sym, item in self.items.items(): if not SMIRInfo._is_func(item): continue @@ -233,10 +215,12 @@ def collect_const_fun_tys(obj: object, called: set[Ty]) -> None: _LOGGER.debug(f'Skipping call edge extraction for {sym}: missing body') called_tys: set[Ty] = set() else: - called_tys = set() - - # Collect direct calls and function items passed as constants (e.g., fn pointers). - collect_const_fun_tys(body, called_tys) + called_funs = [ + b['terminator']['kind']['Call']['func'] for b in body['blocks'] if 'Call' in b['terminator']['kind'] + ] + called_tys = {Ty(op['Constant']['const_']['ty']) for op in called_funs if 'Constant' in op} + # TODO also add any constant operands used as arguments whose ty refer to a function + # the semantics currently does not support this, see issue #488 and stable-mir-json issue #55 for ty in self.function_symbols_reverse[sym]: result[Ty(ty)] = called_tys return result 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/option-map-fn-ptr-fail.rs b/kmir/src/tests/integration/data/prove-rs/option-map-fn-ptr-fail.rs deleted file mode 100644 index f7299a053..000000000 --- a/kmir/src/tests/integration/data/prove-rs/option-map-fn-ptr-fail.rs +++ /dev/null @@ -1,26 +0,0 @@ -// Test case reproducing issues: -// - https://github.com/runtimeverification/mir-semantics/issues/891 -// - https://github.com/runtimeverification/mir-semantics/issues/488 -// - https://github.com/runtimeverification/stable-mir-json/issues/55 -// -// Problem: Option::map with a function pointer (not a closure) causes -// "unknown function -1" error because function pointers passed as arguments -// are not included in the `functions` array in stable-mir-json output. -// -// Original example from issue #891: -// .map(u64::from_le_bytes) // fails - function pointer -// -// Workaround: use a closure instead: -// .map(|bytes| u64::from_le_bytes(bytes)) // works - -fn main() { - let bytes: [u8; 8] = [0x15, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]; - let opt: Option<[u8; 8]> = Some(bytes); - - // This fails: passing function pointer to Option::map - // The MIR desugaring of Option::map invokes the function via a pointer, - // but the function is not present in the `functions` array. - let result = opt.map(u64::from_le_bytes); - - assert_eq!(result, Some(21u64)); -} From 7c00ab8afd677be11f822ffd62b5328c54cb7fb9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 15 Dec 2025 17:42:22 +1100 Subject: [PATCH 6/8] decode function pointers to a special value type --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 11 +++++++++++ kmir/src/kmir/kdist/mir-semantics/rt/value.md | 2 ++ 2 files changed, 13 insertions(+) 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 From f7de8745f6a69ebedbea18c86bd7c56f62f97c2b Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 15 Dec 2025 23:22:14 +0800 Subject: [PATCH 7/8] update expected output --- .../single-bin/single_exe::a_module::twice.expected | 2 +- .../crate-tests/single-bin/single_exe::main.expected | 2 +- .../single-dylib/small_test_dylib::add.expected | 2 +- ...all_test_lib::testing::test_add_in_range.expected | 6 +++--- .../crate-tests/two-crate-bin/crate2::main.expected | 2 +- .../crate2::test_crate1_with.expected | 2 +- .../exec-smir/call-with-args/main-a-b-with-int.state | 4 ++-- .../tests/integration/data/exec-smir/enum/enum.state | 2 +- .../data/exec-smir/main-a-b-c/main-a-b-c.state | 5 +++-- .../data/exec-smir/pointers/pointer-cast-zst.state | 2 +- .../exec-smir/structs-tuples/structs-tuples.state | 2 +- .../show/assert-inhabited-fail.main.expected | 2 +- .../assert-true.main.cli-custom-printer.expected | 2 +- .../assert-true.main.cli-default-printer.expected | 2 +- .../data/prove-rs/show/assert_eq_exp.main.expected | 2 +- ...code-conflict-fail.check_assume_conflict.expected | 2 +- .../prove-rs/show/bitwise-not-shift.main.expected | 2 +- .../prove-rs/show/interior-mut-fail.main.expected | 2 +- .../prove-rs/show/interior-mut3-fail.main.expected | 2 +- .../prove-rs/show/iter_next_2-fail.main.expected | 2 +- .../prove-rs/show/iterator-simple-fail.main.expected | 2 +- .../data/prove-rs/show/local-raw-fail.main.expected | 2 +- .../data/prove-rs/show/niche-enum.main.expected | 2 +- .../niche-enum.smir.foo.cli-stats-leaves.expected | 10 +++++----- .../data/prove-rs/show/offset-u8-fail.main.expected | 2 +- ...er-cast-length-test-fail.array_cast_test.expected | 8 ++++---- .../prove-rs/show/raw-ptr-cast-fail.main.expected | 2 +- .../show/symbolic-args-fail.eats_all_args.expected | 2 +- ...symbolic-args-fail.main.cli-stats-leaves.expected | 6 +++--- .../prove-rs/show/symbolic-args-fail.main.expected | 2 +- .../symbolic-structs-fail.eats_struct_args.expected | 4 ++-- .../show/test_offset_from-fail.testing.expected | 12 ++++++------ .../show/transmute-maybe-uninit-fail.main.expected | 2 +- ...um-changed-discriminant-signed-fail.main.expected | 2 +- .../show/transmute-u8-to-enum-fail.main.expected | 2 +- .../data/prove-rs/show/unions-fail.main.expected | 2 +- 36 files changed, 56 insertions(+), 55 deletions(-) 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/exec-smir/call-with-args/main-a-b-with-int.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state index 056091d15..8d75f185f 100644 --- a/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state @@ -1,6 +1,6 @@ - #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) ) ~> .K + Integer ( 11 , 16 , true ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #setArgsFromStack ( 3 , .Operands ) ~> #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) ) ~> .K noReturn @@ -27,7 +27,7 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) ) - ListItem ( typedValue ( Integer ( 11 , 16 , true ) , ty ( 28 ) , mutabilityNot ) ) + ListItem ( newLocal ( ty ( 28 ) , mutabilityNot ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/enum/enum.state b/kmir/src/tests/integration/data/exec-smir/enum/enum.state index 16e4c197d..25bf13181 100644 --- a/kmir/src/tests/integration/data/exec-smir/enum/enum.state +++ b/kmir/src/tests/integration/data/exec-smir/enum/enum.state @@ -1,6 +1,6 @@ - #selectBlock ( switchTargets (... branches: branch ( 89 , basicBlockIdx ( 7 ) ) branch ( 90 , basicBlockIdx ( 6 ) ) .Branches , otherwise: basicBlockIdx ( 5 ) ) , operandMove ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ) ) ~> .K + #execTerminator ( terminator (... kind: terminatorKindSwitchInt (... discr: operandMove ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 89 , basicBlockIdx ( 7 ) ) branch ( 90 , basicBlockIdx ( 6 ) ) .Branches , otherwise: basicBlockIdx ( 5 ) ) ) , span: span ( 69 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state index a8b20314b..393984ae0 100644 --- a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) ~> .K + #setUpCalleeData ( monoItemFn (... name: symbol ( "c" ) , id: defId ( 9 ) , body: someBody ( 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 ) ) ) ) , .Operands ) ~> .K noReturn @@ -10,7 +10,8 @@ - ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) ) + ListItem ( 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 ) ) ) ) + ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 62 ) ) ) ) ty ( 26 ) diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state index 059a1ae70..4ca786442 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state @@ -1,6 +1,6 @@ - PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K + PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#cast(_,_,_,_)_RT-DATA_Evaluation_Evaluation_CastKind_MaybeTy_Ty0_ ( castKindPtrToPtr ~> .K , ty ( 26 ) ~> .K , ty ( 25 ) ~> .K ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state index 47b68a635..6e2f97478 100644 --- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state +++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state @@ -1,6 +1,6 @@ - #execStmts ( .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) ) ~> .K + #setArgsFromStack ( 4 , .Operands ) ~> #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) ) ) ~> .K noReturn 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 From 256b8781aa0043625d7946110b568b05eec4ad5a Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 16 Dec 2025 11:42:52 +1100 Subject: [PATCH 8/8] revert exec-smir test expectation changes, adjust step counters instead --- .../exec-smir/call-with-args/main-a-b-with-int.state | 4 ++-- .../tests/integration/data/exec-smir/enum/enum.state | 2 +- .../data/exec-smir/main-a-b-c/main-a-b-c.state | 5 ++--- .../data/exec-smir/pointers/pointer-cast-zst.state | 2 +- .../data/exec-smir/structs-tuples/structs-tuples.state | 2 +- kmir/src/tests/integration/test_integration.py | 10 +++++----- 6 files changed, 12 insertions(+), 13 deletions(-) diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state index 8d75f185f..056091d15 100644 --- a/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/main-a-b-with-int.state @@ -1,6 +1,6 @@ - Integer ( 11 , 16 , true ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #setArgsFromStack ( 3 , .Operands ) ~> #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) ) ~> .K + #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 63 ) ) ) ) ~> .K noReturn @@ -27,7 +27,7 @@ ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( 10 , 64 , false ) , ty ( 26 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 28 ) , mutabilityNot ) ) + ListItem ( typedValue ( Integer ( 11 , 16 , true ) , ty ( 28 ) , mutabilityNot ) ) diff --git a/kmir/src/tests/integration/data/exec-smir/enum/enum.state b/kmir/src/tests/integration/data/exec-smir/enum/enum.state index 25bf13181..16e4c197d 100644 --- a/kmir/src/tests/integration/data/exec-smir/enum/enum.state +++ b/kmir/src/tests/integration/data/exec-smir/enum/enum.state @@ -1,6 +1,6 @@ - #execTerminator ( terminator (... kind: terminatorKindSwitchInt (... discr: operandMove ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 89 , basicBlockIdx ( 7 ) ) branch ( 90 , basicBlockIdx ( 6 ) ) .Branches , otherwise: basicBlockIdx ( 5 ) ) ) , span: span ( 69 ) ) ) ~> .K + #selectBlock ( switchTargets (... branches: branch ( 89 , basicBlockIdx ( 7 ) ) branch ( 90 , basicBlockIdx ( 6 ) ) .Branches , otherwise: basicBlockIdx ( 5 ) ) , operandMove ( place (... local: local ( 11 ) , projection: .ProjectionElems ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state index 393984ae0..a8b20314b 100644 --- a/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state +++ b/kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.state @@ -1,6 +1,6 @@ - #setUpCalleeData ( monoItemFn (... name: symbol ( "c" ) , id: defId ( 9 ) , body: someBody ( 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 ) ) ) ) , .Operands ) ~> .K + #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) ~> .K noReturn @@ -10,8 +10,7 @@ - ListItem ( 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 ) ) ) ) - ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 62 ) ) ) ) + ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 65 ) ) ) ) ty ( 26 ) diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state index 4ca786442..059a1ae70 100644 --- a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state +++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state @@ -1,6 +1,6 @@ - PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#cast(_,_,_,_)_RT-DATA_Evaluation_Evaluation_CastKind_MaybeTy_Ty0_ ( castKindPtrToPtr ~> .K , ty ( 26 ) ~> .K , ty ( 25 ) ~> .K ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K + PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K noReturn diff --git a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state index 6e2f97478..47b68a635 100644 --- a/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state +++ b/kmir/src/tests/integration/data/exec-smir/structs-tuples/structs-tuples.state @@ -1,6 +1,6 @@ - #setArgsFromStack ( 4 , .Operands ) ~> #execBlock ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) ) ) ~> .K + #execStmts ( .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindReturn , span: span ( 73 ) ) ) ~> .K noReturn 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',