Update Kani to Rust nightly-2022-10-11 #1788
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
celinval
approved these changes
Oct 14, 2022
| ty: Ty<'tcx>, | ||
| span: Option<&Span>, | ||
| ) -> Expr { | ||
| debug!("The literal was a Unevaluated"); |
There was a problem hiding this comment.
Can you please add the constant?
debug!(?unevaluated, "codegen_const_unevaluated");Nit: I usually add the name of the function to the log so it's easy to find it in the code. But I don't think we have any guidelines on this. So just a suggestion.
| } | ||
| // A `ConstantKind::Ty(ConstKind::Unevaluated)` should no longer show up | ||
| // and should be a `ConstantKind::Unevaluated` instead (and thus handled | ||
| // in `codegen_constant` not here.) |
There was a problem hiding this comment.
in codegen_const_unevaluated
| @@ -2,10 +2,6 @@ | |||
| // | |||
| // Modifications Copyright Kani Contributors | |||
| // See GitHub history for details. | |||
| // | |||
| // NOTE: The initial fix for this has been reverted from rustc. I'm keeping this test here so we | |||
There was a problem hiding this comment.
Hopefully this was useful. :)
adpaco-aws
requested changes
Oct 14, 2022
| // TODO: can be empty now (i.e. `simd_shuffle` instead of `simd_shuffle8`) | ||
| // `parse` fails on empty, so comment that bit of code out. | ||
| // To re-enable this we'll need to investigate how size is computed now. | ||
| // let n: u64 = stripped.parse().unwrap(); |
There was a problem hiding this comment.
Thanks for the heads-up! I'll figure this out as part of the work being done in #1148.
| // intrinsic `assert_uninit_valid` to generate a panic during compilation. | ||
| #[kani::proof] | ||
| fn main() { | ||
| let _var: () = unsafe { | ||
| intrinsics::assert_uninit_valid::<bool>(); | ||
| intrinsics::assert_uninit_valid::<!>(); |
There was a problem hiding this comment.
The problem is that this triggers the same path as tests/kani/Intrinsics/Assert/inhabited_panic.rs. Can you check that you get the message below if you replace bool with &i32?
attempted to leave type `&i32` uninitialized, which is invalid
adpaco-aws
approved these changes
Oct 14, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description of changes:
Updates to newer nightly. Notable impacting changes from upstream:
Remove
mir::CastKind::Miscrust-lang/rust#102675CastKind::MiscbecameCastKind::IntToInt | CastKind::FloatToFloat | CastKind::FloatToInt | CastKind::IntToFloat | CastKind::FnPtrToPtr | CastKind::PtrToPtrUse only ty::Unevaluated<'tcx, ()> in type system rust-lang/rust#98588
ConstantKind::Unevaluatedto replaceContantKind::Tywrapping aConstKind::Unevaluated. Note theANTinConstantdistinguishing these!visit_constwas removed fromMirVisitoras a consequenceInitial implementation of dyn* rust-lang/rust#101212
dyn*might create problems for us in the future but simple change for nowcodegen_unimplementedfor nowAllow destructuring opaque types in their defining scopes rust-lang/rust#98582
ProjectionElem::OpaqueCastpanic-on-uninit: adjust checks to 0x01-filling rust-lang/rust#101061
intrinsics::assert_uninit_valid::<bool>()is ok now? Switch to ! like that pull requestResolved issues:
Resolves #1746
Call-outs:
simd_shuffleis disabled right now, but there's probably a new issue in the way of re-enabling it (it is or can be plainsimd_shufflenow not just e.g.simd_shuffle8) @adpaco-awslet_elseis getting stabilized? Woo hoo!Testing:
How is this change tested? ci
Is this a refactor change? no
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.