Add kmir tool description and CI workflow - #310
Conversation
When setting `shell: bash`, the internal command used in the github job is different from when nothing is set, see https://docs.github.com/en/actions/writing-workflows/workflow-syntax-for-github-actions#jobsjob_iddefaultsrunshell
- Focused on fixing read/write permission issues in previous image - New image introduces new env and bash profile for additional exec calls used in CI.
- Still requires some additional steps to fetch the results from the running container but this is a starting point.
…een CI environments
|
@tautschnig Thank you very much for your detailed feedback on the text. Will try to address your points in a revised version coming soon.
Very true, sorry for this. Keeping each paragraph in a single line is sometimes necessary for weak renderers but certainly not a good idea for a PR to be commented on. In a first commit from here, I will just reformat all Markdown to 80-column paragraphs (w/o any non-formatting changes) to get this problem out of the way. |
2 should be fine for a public github runner. I attempted to interleave the proofs that are different so that the expensive `llvm-kompile` calls will happen at different times.
|
Hey @tautschnig, it would be good to get some feedback on this. CI is passing. |
|
@feliperodri hope it is okay to ping unannounced, I wonder if you might be a better candidate to get feedback from |
|
@dkcumming this PR is marked as draft, that's why I didn't review it before. Is it ready for a review? I saw in the GitHub issue associated with this application that the tool application already received the go ahead. Turn this into non-draft if it's ready for a full review. |
|
@dkcumming also resolve any comment that you already addressed. This will facilitate the review and I won't need to double check work that has been already done. |
|
@feliperodri okay sorry I think I got the process misunderstood I will do those things and am in the process of correcting the other PRs you reviewed on Sunday. I intend to correct these things earnestly over the next couple of days. Thank you! |
|
@feliperodri I think I need write access to model-checking/verify-rust-std in order to resolve comments and mark this as ready for review. I added links on all comments to the relevant commits, and if I could resolve them I would. What should be do, is there some step I am missing to have that ability or is someone with write access able to do that for me? The original PR was opened by my colleague who is no longer working at RV, maybe that is related. |
feliperodri
left a comment
There was a problem hiding this comment.
Reviewed the full PR (doc page, workflow, and the Challenge 11 harnesses). This is a clean, additive tool onboarding — no changes to library/ and nothing that touches Kani or any existing tool/CI — and both KMIR jobs are green on the current head, so the Docker-based workflow is demonstrably functional. Approving.
The positive harnesses correctly guard each unchecked_* op behind the matching checked_* precondition, and the negative harnesses (with run-proofs.sh --negative inverting the exit code) are the right shape for asserting UB is detected. LGTM.
A few non-blocking follow-ups:
-
Pin the Docker image tag.
kmir.ymlusesruntimeverificationinc/kmir:ubuntu-jammy-latest, but the docs recommend pinning to a specific version (e.g.ubuntu-jammy-0.4.206). An unpinnedlatestcan silently change and break CI later without a corresponding commit — pinning it keeps the workflow reproducible. -
Tighten the
push:trigger. Thepushtrigger has no branch filter and includeslibrary/**in its paths, so KMIR CI fires on any push touching std (which the KMIR proofs never read) and duplicates thepull_requestrun. Consider droppinglibrary/**from the push paths and/or restricting tomain. -
Doc polish. A few phrasings read a bit stronger than the current tool maturity ("provably complete", "sound assurances"), and there are minor trailing-whitespace / trailing-blank-line nits (e.g. the extra blank lines appended to
doc/src/tools.md). Worth a light editorial pass together with the wording comments already raised in-thread, but not a merge blocker.
I think the problem is because your colleague opened the PR (sorry for taking so long to review it). It looks good to me and I'll get another committee member to give another review and we should be good to go. You can address all remaining comments/suggestions on follow up PRs and you can track these improvements creating GitHub issues. Thanks for this contribution! |
|
@feliperodri I am happy to address those comments immediately. But if that would interfere with the second review I can hold off. Let me know what you prefer. |
|
@dkcumming that would not interfere with the second review. You can go ahead and implement the comments. |
|
@feliperodri I implemented the changes you requested! Thank you for your review. |
Thank you, @dkcumming! @HuStmpHrrr this is ready for a final review. |
e976b65
This PR adds the
kmirtool to the doc.s and sets up a CI workflow that runs the tool on a few examples.The examples are drawn from Challenge 11 (unchecked arithmetic operations).
The tool is described using the text from the related issue #296 , and the example proofs come with a description that explains how they were set up.
The
kmirtool is work in progress, we expect tool usage to change. Specifically the proof setup will be automated in a future version, enabling the tool to work directly with Rust code.kmiris provided as a docker image from Dockerhub for the CI workflow. This image also includesstable-mir-jsonand was assembled for general usage by developers to try the tool in its current state.Resolves #296