Update the rust toolchain to nightly-2023-12-03

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -33,14 +33,14 @@ use rustc_data_structures::temp_dir::MaybeTempDir;
 use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_hir::definitions::DefPathHash;
+use rustc_metadata::creader::MetadataLoaderDyn;
 use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
-use rustc_session::cstore::MetadataLoaderDyn;
 use rustc_session::output::out_filename;
 use rustc_session::Session;
 use rustc_smir::rustc_internal;

kani-compiler/src/kani_middle/analysis.rs

@@ -151,7 +151,6 @@ impl From<&Terminator> for Key {
             TerminatorKind::Assert { .. } => Key("Assert"),
             TerminatorKind::Call { .. } => Key("Call"),
             TerminatorKind::Drop { .. } => Key("Drop"),
-            TerminatorKind::CoroutineDrop => Key("CoroutineDrop"),
             TerminatorKind::Goto { .. } => Key("Goto"),
             TerminatorKind::InlineAsm { .. } => Key("InlineAsm"),
             TerminatorKind::Resume { .. } => Key("Resume"),

kani-compiler/src/kani_middle/reachability.rs

@@ -266,7 +266,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
     /// Collect an instance depending on how it is used (invoked directly or via fn_ptr).
     fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) {
         let should_collect = match instance.kind {
-            InstanceKind::Virtual | InstanceKind::Intrinsic => {
+            InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => {
                 // Instance definition has no body.
                 assert!(is_direct_call, "Expected direct call {instance:?}");
                 false
@@ -453,8 +453,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
             TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => {
                 // We generate code for this without invoking any lang item.
             }
-            TerminatorKind::CoroutineDrop { .. }
-            | TerminatorKind::Goto { .. }
+            TerminatorKind::Goto { .. }
             | TerminatorKind::SwitchInt { .. }
             | TerminatorKind::Resume
             | TerminatorKind::Return

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -51,7 +51,7 @@ pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool {
         checker.visit_body(&item.body());
         checker.is_valid()
     } else {
-        true
+        instance.body().is_some()
     }
 }
 

kani-driver/src/concrete_playback/test_generator.rs

@@ -163,7 +163,7 @@ impl KaniSession {
             let mut curr_line_num = 0;
 
             // Use a buffered reader/writer to generate the unit test line by line
-            for line in source_reader.lines().flatten() {
+            for line in source_reader.lines().map_while(Result::ok) {
                 curr_line_num += 1;
                 writeln!(temp_file, "{line}")?;
                 if curr_line_num == proof_harness_end_line {

library/kani/src/models/mod.rs

@@ -69,11 +69,13 @@ mod intrinsics {
     }
 
     #[cfg(target_endian = "little")]
-    unsafe fn simd_bitmask_impl<T, const LANES: usize>(input: &[T; LANES]) -> [u8; mask_len(LANES)]
+    unsafe fn simd_bitmask_impl<T, const LANES: usize, const MASK_LEN: usize>(
+        input: &[T; LANES],
+    ) -> [u8; MASK_LEN]
     where
         T: MaskElement,
     {
-        let mut mask_array = [0; mask_len(LANES)];
+        let mut mask_array = [0; MASK_LEN];
         for lane in (0..input.len()).rev() {
             let byte = lane / 8;
             let mask = &mut mask_array[byte];
@@ -99,14 +101,13 @@ mod intrinsics {
     #[rustc_diagnostic_item = "KaniModelSimdBitmask"]
     pub(super) unsafe fn simd_bitmask<T, U, E, const LANES: usize>(input: T) -> U
     where
-        [u8; mask_len(LANES)]: Sized,
+        [u8; size_of::<U>()]: Sized,
         E: MaskElement,
     {
         // These checks are compiler sanity checks to ensure we are not doing anything invalid.
-        assert_eq!(
-            size_of::<U>(),
-            size_of::<[u8; mask_len(LANES)]>(),
-            "Expected size of return type and mask lanes to match",
+        assert!(
+            size_of::<U>() >= mask_len(LANES),
+            "Expected size of return type to be greater or equal to the mask lanes",
         );
         assert_eq!(
             size_of::<T>(),
@@ -115,8 +116,8 @@ mod intrinsics {
         );
 
         let data = &*(&input as *const T as *const [E; LANES]);
-        let mask = simd_bitmask_impl(data);
-        (&mask as *const [u8; mask_len(LANES)] as *const U).read()
+        let mask = simd_bitmask_impl::<E, LANES, { size_of::<U>() }>(data);
+        (&mask as *const [u8; size_of::<U>()] as *const U).read()
     }
 
     /// Structure used for sanity check our parameters.
@@ -127,7 +128,7 @@ mod intrinsics {
 #[cfg(test)]
 mod test {
     use super::intrinsics as kani_intrinsic;
-    use std::{fmt::Debug, simd::*};
+    use std::{fmt::Debug, mem::size_of, simd::*};
 
     extern "platform-intrinsic" {
         fn simd_bitmask<T, U>(x: T) -> U;
@@ -155,10 +156,12 @@ mod test {
     /// Tests that the model correctly fails if the size parameter of the mask doesn't match the
     /// expected number of bytes in the representation.
     #[test]
-    #[should_panic(expected = "Expected size of return type and mask lanes to match")]
+    #[should_panic(
+        expected = "Expected size of return type to be greater or equal to the mask lanes"
+    )]
     fn test_invalid_generics() {
-        let mask = mask32x16::splat(false);
-        assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u16, i32, 2>(mask) }, u16::MAX);
+        let mask = mask32x32::splat(false);
+        assert_eq!(unsafe { kani_intrinsic::simd_bitmask::<_, u8, i32, 32>(mask) }, u8::MAX);
     }
 
     /// Test that the `simd_bitmask` model is equivalent to the intrinsic for a few random values.
@@ -185,15 +188,14 @@ mod test {
     }
 
     /// Compare the value returned by our model and the portable simd representation.
-    fn check_portable_bitmask<T, E, const LANES: usize>(mask: T)
+    fn check_portable_bitmask<T, E, const LANES: usize>(mask: Mask<T, LANES>)
     where
-        T: ToBitMask + Clone,
-        T::BitMask: Debug + PartialEq,
+        T: std::simd::MaskElement,
+        LaneCount<LANES>: SupportedLaneCount,
         E: kani_intrinsic::MaskElement,
-        [u8; kani_intrinsic::mask_len(LANES)]: Sized,
     {
         assert_eq!(
-            unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) },
+            unsafe { kani_intrinsic::simd_bitmask::<_, u64, E, LANES>(mask.clone()) },
             mask.to_bitmask()
         );
     }
@@ -204,7 +206,7 @@ mod test {
         T: Clone,
         U: PartialEq + Debug,
         E: kani_intrinsic::MaskElement,
-        [u8; kani_intrinsic::mask_len(LANES)]: Sized,
+        [u8; size_of::<U>()]: Sized,
     {
         assert_eq!(
             unsafe { kani_intrinsic::simd_bitmask::<_, U, E, LANES>(mask.clone()) },

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-12-01"
+channel = "nightly-2023-12-03"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/SIMD/portable_simd.rs

@@ -4,7 +4,7 @@
 //! Ensure we have basic support of portable SIMD.
 #![feature(portable_simd)]
 
-use std::simd::{mask32x4, u64x16, ToBitMask};
+use std::simd::{mask32x4, u64x16};
 
 #[kani::proof]
 fn check_sum_any() {