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

Change reachability module to use StableMIR #2894

Merged
merged 12 commits into from
Nov 30, 2023

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Nov 25, 2023

Rewrite the reachability module to use Stable APIs wherever possible. Note that in StableMIR the instance body is already monomorphized and constants are already evaluated, which simplifies the code for most of it, except to handle stubbing issue #2589.

For the stubbing issue, we still use a mix of stable and internal APIs to detect an invalid monomorphization.

Call-outs

  1. This change requires the newest version of the Rust toolchain. Thus, it is upgrading the version as well.
  2. Creating this as a draft until Fix smir's Ty::Ref pretty printing rust-lang/rust#118274 is merged.
  3. I ran s2n-quic manually to assess performance and no significant difference.
  • s2n-quic-core: 36.86 vs 37.19
  • s2n-quic-platform: 16.17 vs 16.19

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

@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Nov 25, 2023
@celinval celinval marked this pull request as ready for review November 27, 2023 21:44
@celinval celinval requested a review from a team as a code owner November 27, 2023 21:44
Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

It's looking really good. I wonder if we could add links to the stable MIR project or its APIs so it's clear what's going on here. But I'm not sure how much you'll use these APIs in other parts of the compiler, maybe it's better to add that elsewhere.

kani-compiler/src/kani_middle/reachability.rs Show resolved Hide resolved
kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/stubbing/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/reachability.rs Outdated Show resolved Hide resolved
Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
@zhassan-aws
Copy link
Contributor

I wonder if we could add links to the stable MIR project or its APIs so it's clear what's going on here.

I second this request. It's a bit difficult for me to understand the changes given my lack of knowledge of how the stable/internal MIR APIs compare.

@celinval
Copy link
Contributor Author

I wonder if we could add links to the stable MIR project or its APIs so it's clear what's going on here.

I second this request. It's a bit difficult for me to understand the changes given my lack of knowledge of how the stable/internal MIR APIs compare.

Sure. Right now stable_mir and rustc_smir are new crates in the rust compiler itself. So there's nothing new, and you can apply the same logic as you currently use to check APIs from rustc_span and rustc_middle.

I will add more information to the code and to main.rs, since this code will start showing up in different parts of our compiler.

@celinval
Copy link
Contributor Author

@zhassan-aws and @adpaco-aws, I added some documentation to our wiki instead. I hope that's what you were looking for. Cheers!

docs/src/stable_mir.md Outdated Show resolved Hide resolved
docs/src/stable_mir.md Outdated Show resolved Hide resolved
docs/src/stable_mir.md Outdated Show resolved Hide resolved
docs/src/stable_mir.md Outdated Show resolved Hide resolved
docs/src/stable_mir.md Show resolved Hide resolved
@celinval celinval enabled auto-merge (squash) November 30, 2023 18:45
@celinval celinval merged commit bd2d8d5 into model-checking:main Nov 30, 2023
20 checks passed
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.

3 participants