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

Work around AssertKind::description panicing for BoundsCheck #467

Merged
merged 2 commits into from
Apr 21, 2021

Conversation

dario23
Copy link
Contributor

@dario23 dario23 commented Apr 21, 2021

AssertKind::BoundsCheck panics on calling AssertKind::display, and the
docs say that the caller is supposed to handle those earlier[0]. So we
use fmt_assert_args instead, which can handle BoundsCheck.

[0] https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/mir/enum.AssertKind.html#impl

@Aurel300
Copy link
Member

Oh it's not public… :/

@fpoli
Copy link
Member

fpoli commented Apr 21, 2021

I guess the easiest thing is to create a file in prusti_interface (with an appropriate rustc licence header and link to the rustc source) in which we copy-paste the implementation of fmt_assert_args.

(We could even propose to make that method public with a tiny PR to rustc.)

@dario23
Copy link
Contributor Author

dario23 commented Apr 21, 2021

hm, and the only use seems to be in the mir printing.

i like the idea of doing a rustc PR, but would go with the debug impl (maybe just for the BoundsCheck variant) instead for now, and add a TODO for when/if our rustc-PR is accepted.

AssertKind::BoundsCheck panics on calling AssertKind::display, and the
docs say that the caller is supposed to handle those earlier[0]. So we
use the Debug impl instead, which can handle BoundsCheck.

At some point we want to switch to using `AssertKind::fmt_assert_args`,
but currently that is not public in rustc.

[0] https://doc.rust-lang.org/stable/nightly-rustc/rustc_middle/mir/enum.AssertKind.html#impl
let assert_msg = if let mir::AssertKind::BoundsCheck{ .. } = msg {
// Use the debug impl for BoundsCheck, as it is supposed to be handled before
// calling display() according to the docs
// TODO: use fmt_assert_args once #BUGNR is merged
Copy link
Contributor Author

Choose a reason for hiding this comment

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

will insert the rustc PR number here once i have it.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

alright, i think we could merge this as is for now. alternatively, we could wait ~1 day and hope the rustc side reacts quickly.

Copy link
Member

Choose a reason for hiding this comment

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

Let's merge now

@fpoli fpoli merged commit 850cadd into viperproject:master Apr 21, 2021
@dario23 dario23 deleted the assert-fmt branch April 21, 2021 14:19
dario23 added a commit to dario23/prusti-dev that referenced this pull request May 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants