Update Kani to Rust nightly-2022-10-11#1788
Conversation
celinval
left a comment
celinval
left a comment
There was a problem hiding this comment.
Awesome! Just some nits.
| 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
| // 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. :)
| // 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.
| 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
3 participants
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.