Skip to content

Improved show printing for leaves - #946

Merged
automergerpr-permission-manager[bot] merged 16 commits into
masterfrom
dc/improved-stats
Feb 25, 2026
Merged

Improved show printing for leaves#946
automergerpr-permission-manager[bot] merged 16 commits into
masterfrom
dc/improved-stats

Conversation

@dkcumming

Copy link
Copy Markdown
Collaborator

Short Version

This PR:

  • Threads Spans through to #setUpCalleeData instead of being ignored from the Terminator
  • Modifies the python utility code that prints leaves for kmir show --leaves to print function, call site, and error messages when possible for panic and assert_failed
  • Adds the ability to truncate a path for testing so CI is deterministic

Long Version

In the event that a panic or assert_failed is reached in a proof, a stuck leaf node will be present in the KCFG that calls ** UNKNOWN FUNCTION **. It is not clear exactly which function is being called, where this is being called from, or what the error message is (if there is one) as all the information is represented as interned data (DefId, Span, AllocId).

The print out of the failing nodes is improved for kmir show --leaves from:

Node 3:
  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands) ~> .K

to:

Node 3:
  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands , span ( 117 ) ) ~> .K
  >> function: core::panicking::panic::h941160ead03e2d54
  >> call span: /home/daniel/Applications/mir-semantics/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs:53:5
  >> message: 'assertion failed: false'

This is achieved by taking advantage of the deterministic location of the interned values, retrieving those values, and then consulting the .smir.json to get the un-interned data associated with those interned values.

@automergerpr-permission-manager
automergerpr-permission-manager Bot merged commit 6368cf5 into master Feb 25, 2026
7 checks passed
@automergerpr-permission-manager
automergerpr-permission-manager Bot deleted the dc/improved-stats branch February 25, 2026 19:28
dkcumming added a commit to runtimeverification/solana-token that referenced this pull request Mar 4, 2026
- More `BinOp::Offset` tests
https://github.com/runtimeverification/mir-semantics/pull/#935
- fix: type of offset for applyBinOp(binOpOffset, ...)
https://github.com/runtimeverification/mir-semantics/pull/#936
- Add type-correcting projections on pointer cast and related operations
https://github.com/runtimeverification/mir-semantics/pull/#937
- Fix metadata on `PtrToPtr` cast
https://github.com/runtimeverification/mir-semantics/pull/#941
- Corrections to Multisig cheatcodes
https://github.com/runtimeverification/mir-semantics/pull/#942
- Handled additional Range constructor in `toSigners` side condition.
https://github.com/runtimeverification/mir-semantics/pull/#944
- Update dependency: deps/stable-mir-json_release
runtimeverification/mir-semantics#938
- Improved `show` printing for leaves
runtimeverification/mir-semantics#946
- Fix/cachix pin no response
runtimeverification/mir-semantics#950
- Hotfix/cachix pin checks
runtimeverification/mir-semantics#951
- fix(rt): remove mutability guard on local variable assignment
runtimeverification/mir-semantics#948
- Makefile `stable-mir-json` command to build release also
runtimeverification/mir-semantics#963
- Add `rust-toolchain.toml`
runtimeverification/mir-semantics#959
- Add cut-point rules for specific functions / intrinsics (via
definition)
runtimeverification/mir-semantics#960
- Update dependency: deps/stable-mir-json_release
runtimeverification/mir-semantics#947
- Updated Solana cheatcodes with `Span` in `Call` `Terminator`
(c17566dc)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants