Update the rust toolchain to nightly-2023-12-07 (#2913)

tautschnig · celinval · adpaco-aws · web-flow · commit 63af43d86b00 · 2023-12-08T07:51:10.000Z
Changes required due to: - rust-lang/rust@99ac405b96 Move MetadataLoader{,Dyn} to rustc_metadata. - rust-lang/rust@c997c6d822 Add more information to stable Instance - rust-lang/rust#116915 This also fixes an issue in the `simd_shuffle` implementation that was exposed by the update. Resolves #2911 --------- Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Adrian Palacios <accorell@amazon.com>
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1729,7 +1729,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // [u32; n]: translated wrapped in a struct
         let indexes = fargs.remove(0);
 
-        let (_, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx);
+        let (in_type_len, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx);
         let (ret_type_len, ret_type_subtype) = rust_ret_type.simd_size_and_type(self.tcx);
         if ret_type_len != n {
             let err_msg = format!(
@@ -1749,7 +1749,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // An unsigned type here causes an invariant violation in CBMC.
         // Issue: https://github.com/diffblue/cbmc/issues/6298
         let st_rep = Type::ssize_t();
-        let n_rep = Expr::int_constant(n, st_rep.clone());
+        let n_rep = Expr::int_constant(in_type_len, st_rep.clone());
 
         // P = indexes.expanded_map(v -> if v < N then vec1[v] else vec2[v-N])
         let elems = (0..n)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/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;
diff --git a/kani-compiler/src/kani_middle/analysis.rs b/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"),
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -153,7 +153,11 @@ impl<'tcx> MonoItemsCollector<'tcx> {
     /// instruction looking for the items that should be included in the compilation.
     fn reachable_items(&mut self) {
         while let Some(to_visit) = self.queue.pop() {
-            if !self.collected.contains(&to_visit) {
+            // TODO: This should only check is_foreign_item() or even `has_body()`.
+            // We need https://github.com/rust-lang/rust/pull/118681 to land first.
+            if !self.collected.contains(&to_visit)
+                && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id())
+            {
                 self.collected.insert(to_visit.clone());
                 let next_items = match &to_visit {
                     MonoItem::Fn(instance) => self.visit_fn(*instance),
@@ -266,7 +270,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 +457,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
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -46,6 +46,7 @@ pub fn harness_stub_map(
 pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool {
     let internal_instance = rustc_internal::internal(instance);
     if get_stub(tcx, internal_instance.def_id()).is_some() {
+        debug!(?instance, "validate_instance");
         let item = CrateItem::try_from(instance).unwrap();
         let mut checker = StubConstChecker::new(tcx, internal_instance, item);
         checker.visit_body(&item.body());
diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/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 {
diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs
@@ -137,8 +137,8 @@ mod test {
     /// masks with lanes represented using i16.
     #[test]
     fn test_bitmask_i16() {
-        check_portable_bitmask::<_, i16, 16>(mask16x16::splat(false));
-        check_portable_bitmask::<_, i16, 16>(mask16x16::splat(true));
+        check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(false));
+        check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(true));
     }
 
     /// Tests that the model correctly fails if an invalid value is given.
@@ -165,11 +165,11 @@ mod test {
     /// These values shouldn't be symmetric and ensure that we also handle endianness correctly.
     #[test]
     fn test_bitmask_i32() {
-        check_portable_bitmask::<_, i32, 8>(mask32x8::from([
+        check_portable_bitmask::<_, i32, 8, u8>(mask32x8::from([
             true, true, false, true, false, false, false, true,
         ]));
 
-        check_portable_bitmask::<_, i32, 4>(mask32x4::from([true, false, false, true]));
+        check_portable_bitmask::<_, i32, 4, u8>(mask32x4::from([true, false, false, true]));
     }
 
     #[repr(simd)]
@@ -185,15 +185,16 @@ 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, M>(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,
+        u64: From<M>,
     {
         assert_eq!(
-            unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) },
+            unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) },
             mask.to_bitmask()
         );
     }
@@ -211,4 +212,19 @@ mod test {
             unsafe { simd_bitmask::<T, U>(mask) }
         );
     }
+
+    /// Similar to portable simd_harness.
+    #[test]
+    fn check_mask_harness() {
+        // From array doesn't work either. Manually build [false, true, false, true]
+        let mut mask = mask32x4::splat(false);
+        mask.set(1, true);
+        mask.set(3, true);
+        let bitmask = mask.to_bitmask();
+        assert_eq!(bitmask, 0b1010);
+
+        let kani_mask =
+            unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) };
+        assert_eq!(kani_mask, bitmask);
+    }
 }
diff --git a/rust-toolchain.toml b/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-07"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected
@@ -1,12 +1,12 @@
 Checking harness check_access_length_17...
 
-Failed Checks: dereference failure: pointer outside object bounds\
-in check_access_length_17
+Failed Checks: assumption failed\
+in <usize as std::slice::SliceIndex<[Dummy]>>::get_unchecked
 
 Checking harness check_access_length_zero...
 
-Failed Checks: dereference failure: pointer outside object bounds\
-in check_access_length_zero
+Failed Checks: assumption failed\
+in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_access_length_17
 Verification failed for - check_access_length_zero
diff --git a/tests/expected/any_vec/out_bounds.expected b/tests/expected/any_vec/out_bounds.expected
@@ -1,61 +1,6 @@
-check_always_out_bounds::check_0.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer NULL"\
-function check_always_out_bounds::check_0
-
-check_always_out_bounds::check_0.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_0
-
-check_always_out_bounds::check_0.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: invalid integer address"\
-function check_always_out_bounds::check_0
-
-check_always_out_bounds::check_1.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_1
-
-check_always_out_bounds::check_2.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_2
-
-check_always_out_bounds::check_3.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_3
-
-check_always_out_bounds::check_4.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_4
-
-check_always_out_bounds::check_5.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_5
-
-check_always_out_bounds::check_6.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_6
-
-check_always_out_bounds::check_7.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_7
-
-check_always_out_bounds::check_8.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_8
-
-check_always_out_bounds::check_9.cover\
-Status: UNREACHABLE\
-Description: "cover condition: *val == 0"\
-function check_always_out_bounds::check_9
+Checking harness check_always_out_bounds...
 
+Failed Checks: assumption failed
+in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
+Verification failed for - check_always_out_bounds
diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs
@@ -45,3 +45,13 @@ fn main() {
         assert!(c == i64x4(2, 4, 6, 8));
     }
 }
+
+#[kani::proof]
+fn check_shuffle() {
+    {
+        let y = i64x2(0, 1);
+        let z = i64x2(1, 2);
+        const I: [u32; 4] = [1, 2, 0, 3];
+        let _x: i64x4 = unsafe { simd_shuffle(y, z, I) };
+    }
+}
diff --git a/tests/kani/SIMD/portable_simd.rs b/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, u32x4, u64x16};
 
 #[kani::proof]
 fn check_sum_any() {
@@ -23,3 +23,10 @@ fn check_mask() {
     let bitmask = mask.to_bitmask();
     assert_eq!(bitmask, 0b1010);
 }
+
+#[kani::proof]
+fn check_resize() {
+    let x = u32x4::from_array([0, 1, 2, 3]);
+    assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]);
+    assert_eq!(x.resize::<2>(9).to_array(), [0, 1]);
+}
diff --git a/tests/kani/SIMD/swizzle.rs b/tests/kani/SIMD/swizzle.rs
@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Ensure we can safely swizzle between SIMD types of different sizes.
+#![feature(portable_simd)]
+
+use std::simd::{simd_swizzle, u32x4, u32x8};
+
+#[kani::proof]
+fn harness_from_u32x4_to_u32x4() {
+    let a = u32x4::from_array([0, 1, 2, 3]);
+    let b = u32x4::from_array([4, 5, 6, 7]);
+    let r: u32x4 = simd_swizzle!(a, b, [0, 1, 6, 7]);
+    assert_eq!(r.to_array(), [0, 1, 6, 7]);
+}
+
+#[kani::proof]
+fn harness_from_u32x4_to_u32x8() {
+    let a = u32x4::from_array([0, 1, 2, 3]);
+    let b = u32x4::from_array([4, 5, 6, 7]);
+    let r: u32x8 = simd_swizzle!(a, b, [0, 1, 2, 3, 4, 5, 6, 7]);
+    assert_eq!(r.to_array(), [0, 1, 2, 3, 4, 5, 6, 7]);
+}
+
+#[kani::proof]
+fn harness_from_u32x8_to_u32x4() {
+    let a = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]);
+    let b = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]);
+    let r: u32x4 = simd_swizzle!(a, b, [0, 1, 2, 3]);
+    assert_eq!(r.to_array(), [0, 1, 2, 3]);
+}
