Update feature/p-token with latest master#965
Merged
dkcumming merged 9 commits intofeature/p-tokenfrom Mar 3, 2026
Merged
Conversation
Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>
### Short Version This PR: - Threads `Span`s 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.
Something I have been noticing when testing pin and push with kup / cachix is we get a failure on 'cachix pin' and it times out after 120 seconds, and then a few minutes later the pin shows up. The workaround here may likely be just wait and keep trying for a few more minutes to determine if it actually did fail or if the error we're getting from cachix is a false failure. -- This very much seems to be the case.
## Cachix Test Pin Workflow Updates
- Addressing an issue when parsing the json blob incorrectly. Store
paths returned by this call returns ALL associated pins to the kmir
project and the associated architectures on that query. We look for
'latest' and compare is our desired artifact there, yes? done, else wait
5 seconds and try again.
- The Cachix Test WF also now properly checks out the correct branch
being modified and tested.
Problem: Before it was checking out the target 'Git ref', if you're
trying to fix / test changes to the script or the test WF it would pull
the wrong code to run.
This combo of script and WF allows now for developers to test / get a
better view of what is on cachix, compare expectations to reality.
- Release workflow should now also find the expected revision it just
prodcued on cachix.
## NOTE
- What remains in question. Is 120 seconds enough or do we need to allow
more time for cachix to update and notify the pin was made. It is slow,
how slow? Maybe longer than 2 minutes. Increase this wait time to 5
minutes if it fails again.
For the most recent release I tested manually with the test workflow
here:
https://github.com/runtimeverification/mir-semantics/actions/runs/22501138031
## Summary Remove the `mutabilityOf(...) ==K mutabilityMut` guard from `#setLocalValue` in `rt/data.md`. MIR's `LocalDecl::mutability` is a source-level annotation, not an assignment constraint — the Rust compiler validates legality before emitting MIR and may reuse immutable locals across loop iterations. - Remove mutability guard from the initialized-local `#setLocalValue` rule - Preserve original mutability on write (`mutabilityOf(...)`) instead of forcing `mutabilityMut` - Add regression test `immutable-local-reassign.rs` (loop variable with `mutability: Not`) Follow-up: #949 (remove mutability tracking entirely) ## Context A `for i in 0..2` loop variable is bound via pattern matching (`Some(i)`) on each iteration, so rustc marks it as `mutability: Not`. However, rustc reuses the same MIR local across iterations, producing repeated assignments to an immutable local. This is valid MIR — confirmed via `rustc -Z unpretty=mir` and the [`LocalDecl` documentation](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.LocalDecl.html). Without this fix, proof execution gets stuck at step 693 on `#setLocalValue(place(local(8), .ProjectionElems), Integer(1, 64, false))` — the loop counter assignment that no rule can handle. ### Proof evidence **Without fix (RED):** ``` APRProof: immutable-local-reassign.main status: ProofStatus.FAILED stuck: 1, failing: 1 Leaf <k>: #setLocalValue(place(local(8), .ProjectionElems), Integer(1, 64, false)) function: repro ``` **With fix (GREEN):** ``` test_prove_rs[immutable-local-reassign] PASSED (53.31s) ``` ## Test plan - [x] `immutable-local-reassign.rs` passes with fix, fails (stuck) without fix - [x] Full integration test suite (`make test-integration`)
Stops error where test runner was reading from a stale release
When I was doing some testing I noticed that if I have a different rust version installed and attempt to rebuild the `stable-mir-json` artefacts that they were error on changed MIR data structures. Adding a `rust-toolchain.toml` means that the correct version will always be active for the repo. ``` daniel@daniel-MS-7E06 mir-semantics$ rustup show active-toolchain -v nightly-2024-11-29-x86_64-unknown-linux-gnu active because: overridden by '/home/daniel/Applications/mir-semantics/rust-toolchain.toml' ``` I also updated the github workflow so that it if `stable-mir-json` is updated it will update the channel to the new one. --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
…on)) (#960) This PR builds upon #931 modifying the approach in response to the comments on that PR. For full context read #931 _first_. The `kmir prove-rs` flag `--break-on-function` is implemented in this PR as a compiled definition with hooked function to retrieve the function names to match on. This is similar to the already existing pattern that compiles the static data of a KMIR configuration into the definition. This allows for functions to be provided both when creating the initial proof, and when reading from disc (triggers a recompile of llvm if different flags are provided). I added a test to demonstrate this working on functions and intrinsics, only matching those provided. I do not have a test from reading a partial proof and adding different function names - I did test it but it seemed a bit overboard for a test just now. I did try the method with [K shell access impure function](https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md#shell-access), however this created branching for every function call since the result was stored in a symbolic value. I couldn't figure out how to get that working concretely (I don't think it is possible but might be wrong).
- [stable-mir-json PR 122](https://github.com/runtimeverification/stable-mir-json/pull/122/changes#diff-f3fb88e143d9d90b06c9086e1c660a3e28674c1c1cebf1870de06d73156e3d54R413-R416) Added `Dyn` which needed corresponding K and python productions added to AST - [stable-mir-json PR 129](runtimeverification/stable-mir-json#129) or [131](runtimeverification/stable-mir-json#131) changes closures which do not have corresponding K updates in this PR, proofs `and_then_closure` and `closure_acces_struct` are regressed to failing for now with semantics for correct usage expected to come after merging --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>
Collaborator
Author
|
I tested locally and after correcting the discrepancies, and pushed the fix to the https://github.com/runtimeverification/mir-semantics/actions/runs/22620571623 |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
showprinting for leaves Improvedshowprinting for leaves #946stable-mir-jsoncommand to build release also Makefilestable-mir-jsoncommand to build release also #963rust-toolchain.tomlAddrust-toolchain.toml#959