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

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)

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

@@ -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

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());

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

@@ -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);
+ }
 }

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"]

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

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

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) };
+ }
+}

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]);
+}

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]);
+}