Update feature/proofs with master #791
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
dkcumming
commented
Oct 31, 2025
dkcumming
commented
- Update dependency: deps/k_release #787
- Seed the pseudorandom number generator for random execution #783
- Cut point rules and section edge command in KMIR #780
- More cut point rules #790
Co-authored-by: devops <devops@runtimeverification.com>
This PR adds: - The option `--break-on-calls` to `kmir prove` which will break the proof at the rule `#setUpCalleeData` for easy linking of proof to source code - The command `kmir section-edge` which can be provided an existing proof and an edge (two linked nodes in the kcfg) as a tuple (e.g. `4,5`) and will proof an amount of nodes breaking the edge up. In particular I find this may be useful if we can identify when a thunk is written to `<locals>` and we can section out the edge between the node it appears and the call above it. If the distance between the nodes is `n` steps, then the max sections is `n - 1` which will take 1 step. ### Current Problems - `--break-on-calls` is outputing the node at `#setUpCalleeData` but is also outputting the node afterwards `#setArgsFromStack` which is doubling the amount of output - I did look but can't understand why this is happening currently, however it is also not a deal breaker for me right now - I am still able to see the nodes I want and just some extra. UPDATE: This behaviour is also the same with Kontrol so I think this is a broader thing with K pr pyk --------- Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
Closes #789 In particular adds: - [x] `--break-on-instrinsic-calls` breaks on calling `Intrinsic`s - [x] `--break-on-function-calls` breaks on calling `Function`s - [x] `--break-on-thunks` breaks on `thunk` - [x] `--break-every-statement` breaks every MIR `Statement` - [x] `--break-every-terminator` breaks every MIR `Terminator` - [x] `--break-on-terminator-goto` breaks on calling `TerminatorKind::Goto` - [x] `--break-on-terminator-switch-int` breaks on calling `TerminatorKind::SwitchInt` - [x] `--break-on-terminator-return` breaks on calling `TerminatorKind::Return` - [x] `--break-on-terminator-call` breaks on calling `TerminatorKind::Call` - [x] `--break-on-terminator-assert` breaks on calling `TerminatorKind::Assert` - [x] `--break-on-terminator-drop` breaks on calling `TerminatorKind::Drop` - [x] `--break-on-terminator-unreachable` breaks on calling `TerminatorKind::Unreachable` - [x] `--break-every-step` breaks every MIR `Statement` and `Terminator` And `--break-on-calls` now breaks on instrinics and function calls at the `Terminator` call since it dumps `#setUpCalleeData` node after you can see the name of the intrinsic or function still
Stevengre
approved these changes
Oct 31, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.