Skip to content

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-EndToEndBenchCI 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.

@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!

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
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-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants