Merge branch 'main' into dependabot/github_actions/actions/checkout-4

.github/workflows/release.yml

@@ -271,7 +271,7 @@ jobs:
  cargo package -p kani-verifier
 
  - name: 'Login to GitHub Container Registry'
- uses: docker/login-action@v2
+ uses: docker/login-action@v3
  with:
  registry: ghcr.io
  username: ${{ github.repository_owner }}
@@ -284,7 +284,7 @@ jobs:
  OWNER: '${{ github.repository_owner }}'
 
  - name: Build and push
- uses: docker/build-push-action@v3
+ uses: docker/build-push-action@v5
  with:
  context: .
  file: scripts/ci/Dockerfile.bundle-release-20-04

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/codegen/operand.rs

@@ -421,7 +421,8 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  (Scalar::Ptr(ptr, _size), _) => {
  let res_t = self.codegen_ty(ty);
- let (alloc_id, offset) = ptr.into_parts();
+ let (prov, offset) = ptr.into_parts();
+ let alloc_id = prov.alloc_id();
  self.codegen_alloc_pointer(res_t, alloc_id, offset, span)
  }
  _ => unimplemented!(),
@@ -646,7 +647,8 @@ impl<'tcx> GotocCtx<'tcx> {
  Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes());
 
  let mut next_offset = Size::ZERO;
- for &(offset, alloc_id) in alloc.provenance().ptrs().iter() {
+ for &(offset, prov) in alloc.provenance().ptrs().iter() {
+ let alloc_id = prov.alloc_id();
  if offset > next_offset {
  let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
  next_offset.bytes_usize()..offset.bytes_usize(),

kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs

@@ -5,9 +5,10 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
-use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
+use rustc_middle::mir::{Local, VarDebugInfoContents};
 use rustc_smir::rustc_internal;
 use rustc_span::Span;
+use stable_mir::mir::VarDebugInfo;
 
 impl<'tcx> GotocCtx<'tcx> {
  pub fn codegen_span(&self, sp: &Span) -> Location {
@@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> {
  sp.map_or(Location::none(), |x| self.codegen_span(&x))
  }
 
- pub fn find_debug_info(&self, l: &Local) -> Option<&VarDebugInfo<'tcx>> {
- self.current_fn().mir().var_debug_info.iter().find(|info| match info.value {
- VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0,
- VarDebugInfoContents::Const(_) => false,
- })
+ pub fn find_debug_info(&self, l: &Local) -> Option<VarDebugInfo> {
+ rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| {
+ match info.value {
+ VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0,
+ VarDebugInfoContents::Const(_) => false,
+ }
+ }))
  }
 }

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -332,11 +332,11 @@ impl<'tcx> GotocCtx<'tcx> {
  ty: Ty<'tcx>,
  args: ty::GenericArgsRef<'tcx>,
  ) -> ty::PolyFnSig<'tcx> {
- let sig = args.as_coroutine().poly_sig();
+ let sig = args.as_coroutine().sig();
 
- let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
- sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
- );
+ let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once(
+ ty::BoundVariableKind::Region(ty::BrEnv),
+ ));
  let br = ty::BoundRegion {
  var: ty::BoundVar::from_usize(bound_vars.len() - 1),
  kind: ty::BoundRegionKind::BrEnv,
@@ -349,7 +349,6 @@ impl<'tcx> GotocCtx<'tcx> {
  let pin_args = self.tcx.mk_args(&[env_ty.into()]);
  let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args);
 
- let sig = sig.skip_binder();
  // The `FnSig` and the `ret_ty` here is for a coroutines main
  // `coroutine::resume(...) -> CoroutineState` function in case we
  // have an ordinary coroutine, or the `Future::poll(...) -> Poll`

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/codegen_cprover_gotoc/utils/names.rs

@@ -22,7 +22,7 @@ impl<'tcx> GotocCtx<'tcx> {
  pub fn codegen_var_base_name(&self, l: &Local) -> String {
  match self.find_debug_info(l) {
  None => format!("var_{}", l.index()),
- Some(info) => format!("{}", info.name),
+ Some(info) => info.name,
  }
  }
 

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

@@ -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-08"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

scripts/kani-regression.sh

@@ -100,14 +100,6 @@ FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.tom
 cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success
 cargo clean --manifest-path "$FEATURES_MANIFEST_PATH"
 
-# Check that documentation compiles.
-echo "Current disk usage:"
-df -h
-echo "Starting doc tests:"
-cargo doc --workspace --no-deps --exclude std
-echo "Disk usage after documentation build:"
-df -h
-
 echo
 echo "All Kani regression tests completed successfully."
 echo

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