Upgrade toolchain to 2024-03-11

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

@@ -474,6 +474,11 @@ impl<'tcx> GotocCtx<'tcx> {
  let binop_stmt = codegen_intrinsic_binop!(sub);
  self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
  }
+ "is_val_statically_known" => {
+ // Returning false is sound according do this intrinsic's documentation:
+ // https://doc.rust-lang.org/nightly/std/intrinsics/fn.is_val_statically_known.html
+ self.codegen_expr_to_place_stable(place, Expr::c_false())
+ }
  "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0)),
  "log10f32" => unstable_codegen!(codegen_simple_intrinsic!(Log10f)),
  "log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)),
@@ -506,6 +511,7 @@ impl<'tcx> GotocCtx<'tcx> {
  "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),
  "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, place, loc),
  "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
+ "retag_box_to_raw" => self.codegen_retag_box_to_raw(fargs, place, loc),
  "rintf32" => codegen_simple_intrinsic!(Rintf),
  "rintf64" => codegen_simple_intrinsic!(Rint),
  "rotate_left" => codegen_intrinsic_binop!(rol),
@@ -1259,6 +1265,19 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_expr_to_place_stable(p, e)
  }
 
+ // This is an operation that is primarily relevant for stacked borrow
+ // checks. For Kani, we simply return the pointer.
+ fn codegen_retag_box_to_raw(
+ &mut self,
+ mut fargs: Vec<Expr>,
+ p: &Place,
+ _loc: Location,
+ ) -> Stmt {
+ assert_eq!(fargs.len(), 1, "raw_box_to_box expected one argument");
+ let arg = fargs.remove(0);
+ self.codegen_expr_to_place_stable(p, arg)
+ }
+
  fn vtable_info(
  &mut self,
  info: VTableInfo,

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

@@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> {
  .bytes(),
  Type::size_t(),
  ),
- NullOp::DebugAssertions => Expr::c_false(),
+ NullOp::UbCheck(_) => Expr::c_false(),
  }
  }
  Rvalue::ShallowInitBox(ref operand, content_ty) => {

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

@@ -542,6 +542,9 @@ impl<'tcx> GotocCtx<'tcx> {
  ty::Float(k) => match k {
  FloatTy::F32 => Type::float(),
  FloatTy::F64 => Type::double(),
+ // `F16` and `F128` are not yet handled.
+ // Tracked here: <https://github.com/model-checking/kani/issues/3069>
+ FloatTy::F16 | FloatTy::F128 => unimplemented!(),
  },
  ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
  ty::Adt(def, subst) => {
@@ -1346,6 +1349,9 @@ impl<'tcx> GotocCtx<'tcx> {
 
  Primitive::F32 => self.tcx.types.f32,
  Primitive::F64 => self.tcx.types.f64,
+ // `F16` and `F128` are not yet handled.
+ // Tracked here: <https://github.com/model-checking/kani/issues/3069>
+ Primitive::F16 | Primitive::F128 => unimplemented!(),
  Primitive::Pointer(_) => Ty::new_ptr(
  self.tcx,
  ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -397,7 +397,7 @@ impl CodegenBackend for GotocCodegenBackend {
  let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps);
  let (metadata, _metadata_position) = create_wrapper_file(
  sess,
- b".rmeta".to_vec(),
+ ".rmeta".to_string(),
  codegen_results.metadata.raw_data(),
  );
  let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME);

kani-compiler/src/kani_middle/attributes.rs

@@ -611,9 +611,8 @@ fn parse_modify_values<'a>(
  let mut iter = t.trees();
  std::iter::from_fn(move || {
  let tree = iter.next()?;
- let wrong_token_err = || {
- tcx.sess.parse_sess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.")
- };
+ let wrong_token_err =
+ || tcx.sess.psess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.");
  let result = match tree {
  TokenTree::Token(token, _) => {
  if let TokenKind::Ident(id, _) = &token.kind {
@@ -640,7 +639,7 @@ fn parse_modify_values<'a>(
  match iter.next() {
  None | Some(comma_tok!()) => (),
  Some(not_comma) => {
- tcx.sess.parse_sess.dcx.span_err(
+ tcx.sess.psess.dcx.span_err(
  not_comma.span(),
  "Unexpected token, expected end of attribute or comma",
  );

kani-compiler/src/kani_middle/intrinsics.rs

@@ -6,7 +6,7 @@ use rustc_index::IndexVec;
 use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, TerminatorKind};
 use rustc_middle::mir::{Local, LocalDecl};
 use rustc_middle::ty::{self, Ty, TyCtxt};
-use rustc_middle::ty::{Const, GenericArgsRef};
+use rustc_middle::ty::{Const, GenericArgsRef, IntrinsicDef};
 use rustc_span::source_map::Spanned;
 use rustc_span::symbol::{sym, Symbol};
 use tracing::{debug, trace};
@@ -33,8 +33,8 @@ impl<'tcx> ModelIntrinsics<'tcx> {
  let terminator = block.terminator_mut();
  if let TerminatorKind::Call { func, args, .. } = &mut terminator.kind {
  let func_ty = func.ty(&self.local_decls, self.tcx);
- if let Some((intrinsic_name, generics)) = resolve_rust_intrinsic(self.tcx, func_ty)
- {
+ if let Some((intrinsic, generics)) = resolve_rust_intrinsic(self.tcx, func_ty) {
+  let intrinsic_name = intrinsic.name;
  trace!(?func, ?intrinsic_name, "run_pass");
  if intrinsic_name == sym::simd_bitmask {
  self.replace_simd_bitmask(func, args, generics)
@@ -99,7 +99,7 @@ fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx>
 fn resolve_rust_intrinsic<'tcx>(
  tcx: TyCtxt<'tcx>,
  func_ty: Ty<'tcx>,
-) -> Option<(Symbol, GenericArgsRef<'tcx>)> {
+) -> Option<(IntrinsicDef, GenericArgsRef<'tcx>)> {
  if let ty::FnDef(def_id, args) = *func_ty.kind() {
  if let Some(symbol) = tcx.intrinsic(def_id) {
  return Some((symbol, args));

kani-compiler/src/kani_middle/reachability.rs

@@ -515,8 +515,8 @@ fn collect_alloc_items(alloc_id: AllocId) -> Vec<MonoItem> {
 }
 
 #[cfg(debug_assertions)]
+#[allow(dead_code)]
 mod debug {
- #![allow(dead_code)]
 
  use std::fmt::{Display, Formatter};
  use std::{

kani-driver/src/assess/mod.rs

@@ -170,7 +170,7 @@ fn reconstruct_metadata_structure(
  }
  if !package_artifacts.is_empty() {
  let mut merged = crate::metadata::merge_kani_metadata(package_artifacts);
- merged.crate_name = package.name.clone();
+ merged.crate_name.clone_from(&package.name);
  package_metas.push(merged);
  }
  }

rust-toolchain.toml

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

tests/coverage/unreachable/variant/expected

@@ -1,4 +1,4 @@
-coverage/unreachable/variant/main.rs, 15, PARTIAL
+coverage/unreachable/variant/main.rs, 15, FULL
 coverage/unreachable/variant/main.rs, 16, NONE
 coverage/unreachable/variant/main.rs, 17, NONE
 coverage/unreachable/variant/main.rs, 18, FULL

tools/bookrunner/librustdoc/html/markdown.rs

@@ -225,7 +225,7 @@ impl LangString {
  let mut data = LangString::default();
  let mut ignores = vec![];
 
- data.original = string.to_owned();
+ string.clone_into(&mut data.original);
 
  for token in Self::tokens(string) {
  match token {