Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use stable_mir api instead of internal api for analysis #2871

Merged
merged 5 commits into from
Nov 17, 2023

Conversation

ouz-a
Copy link
Contributor

@ouz-a ouz-a commented Nov 11, 2023

This update introduces several stable_mir APIs to Kani. Previously, we relied on internal APIs to accomplish our goals. However, with the recent enhancements to stable_mir, we no longer need these internal APIs. This pull request hopefully marks the beginning of a migration towards stable_mir for Kani.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@ouz-a ouz-a requested a review from a team as a code owner November 11, 2023 14:35
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Nov 11, 2023
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's awesome and quick! Thanks!

I think you'll need to initialize stable mir for this to work. For now, you can wrap the logic of theprint_stats in a closure, and invoke rustc_internal::run. Also, I forgot to mention, and I don't know if you've figured out already, but one way to test this code is to run Kani with --verbose.

kani-compiler/Cargo.toml Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/analysis.rs Outdated Show resolved Hide resolved
@ouz-a
Copy link
Contributor Author

ouz-a commented Nov 14, 2023

Well I tried few things but It wasn't really clear to me which things supposed to fail and which things supposed to not fail, I run cargo kani --verbose from that all I got was reachability report.

@celinval
Copy link
Contributor

@ouz-a No worries. Feel free to ping me offline if you want to know more. The important thing was to see the report when you ran with --verbose. Thanks!

kani-compiler/src/kani_middle/analysis.rs Show resolved Hide resolved
kani-compiler/src/kani_middle/analysis.rs Outdated Show resolved Hide resolved
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks again!

@celinval celinval enabled auto-merge (squash) November 15, 2023 12:06
@ouz-a ouz-a mentioned this pull request Nov 16, 2023
@celinval celinval merged commit 7a35dac into model-checking:main Nov 17, 2023
19 of 20 checks passed
celinval pushed a commit that referenced this pull request Nov 29, 2023
Follow up pr to #2871 as
`stable_mir::ty::Span` have ability to `get_filename` and `get_lineinfo`
we could start adopting it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants