Upgrade Rust toolchain to nightly-2024-03-29

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

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

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

@@ -570,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // Note: This is not valid C but CBMC seems to be ok with it.
             ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),
             ty::Str => Type::unsigned_int(8).flexible_array_of(),
-            ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t),
+            ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t),
             ty::FnDef(def_id, args) => {
                 let instance =
                     Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
@@ -993,7 +993,7 @@ impl<'tcx> GotocCtx<'tcx> {
             | ty::Foreign(_)
             | ty::Coroutine(..)
             | ty::Int(_)
-            | ty::RawPtr(_)
+            | ty::RawPtr(_, _)
             | ty::Ref(..)
             | ty::Tuple(_)
             | ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),
@@ -1352,10 +1352,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // `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 },
-            ),
+            Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
         }
     }
 
@@ -1659,7 +1656,7 @@ fn common_vtable_fields(drop_in_place: Type) -> Vec<DatatypeComponent> {
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
     match mir_type.kind() {
         ty::Ref(_, pointee_type, _) => Some(*pointee_type),
-        ty::RawPtr(ty::TypeAndMut { ty: pointee_type, .. }) => Some(*pointee_type),
+        ty::RawPtr(pointee_type, _) => Some(*pointee_type),
         _ => None,
     }
 }

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -39,6 +39,7 @@ use stable_mir::mir::mono::Instance;
 use stable_mir::mir::Body;
 use stable_mir::ty::Allocation;
 
+#[allow(dead_code)]
 pub struct GotocCtx<'tcx> {
     /// the typing context
     pub tcx: TyCtxt<'tcx>,

kani-compiler/src/kani_middle/mod.rs

@@ -22,7 +22,6 @@ use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem};
-use stable_mir::mir::pretty::pretty_ty;
 use stable_mir::ty::{BoundVariableKind, FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
 use stable_mir::visitor::{Visitable, Visitor as TypeVisitor};
 use stable_mir::{CrateDef, DefId};
@@ -48,7 +47,7 @@ pub mod transform;
 /// error was found.
 pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
     let krate = tcx.crate_name(LOCAL_CRATE);
-    for item in tcx.hir_crate_items(()).items() {
+    for item in tcx.hir().items() {
         let def_id = item.owner_id.def_id.to_def_id();
         KaniAttributes::for_item(tcx, def_id).check_attributes();
         if tcx.def_kind(def_id) == DefKind::GlobalAsm {
@@ -129,7 +128,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
                 self.tcx.dcx().err(format!(
                     "{} contains a {}pointer ({}). This is prohibited for functions with contracts, \
                     as they cannot yet reason about the pointer behavior.", self.r#where, self.what,
-                    pretty_ty(ty.kind())));
+                    ty));
             }
 
             // Rust's type visitor only recurses into type arguments, (e.g.
@@ -224,6 +223,7 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
 /// Structure that represents the source location of a definition.
 /// TODO: Use `InternedString` once we move it out of the cprover_bindings.
 /// <https://github.com/model-checking/kani/issues/2435>
+#[allow(dead_code)]
 pub struct SourceLocation {
     pub filename: String,
     pub start_line: usize,

kani-compiler/src/kani_middle/reachability.rs

@@ -25,7 +25,6 @@ use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
-use stable_mir::mir::pretty::pretty_ty;
 use stable_mir::mir::{
     visit::Location, Body, CastKind, Constant, MirVisitor, PointerCoercion, Rvalue, Terminator,
     TerminatorKind,
@@ -433,7 +432,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                         `{}`. The function `{}` \
                                         cannot be stubbed by `{}` due to \
                                         generic bounds not being met. Callee: {}",
-                                        pretty_ty(receiver_ty.kind()),
+                                        receiver_ty,
                                         trait_,
                                         caller,
                                         self.tcx.def_path_str(stub),

kani-compiler/src/kani_middle/transform/body.rs

@@ -227,6 +227,7 @@ impl MutableBody {
 }
 
 #[derive(Clone, Debug)]
+#[allow(dead_code)]
 pub enum CheckType {
     /// This is used by default when the `kani` crate is available.
     Assert(Instance),

kani-driver/src/call_cbmc.rs

@@ -40,6 +40,7 @@ pub enum FailedProperties {
 
 /// Our (kani-driver) notions of CBMC results.
 #[derive(Debug)]
+#[allow(dead_code)]
 pub struct VerificationResult {
     /// Whether verification should be considered to have succeeded, or have failed.
     pub status: VerificationStatus,

kani-driver/src/cbmc_output_parser.rs

@@ -286,6 +286,7 @@ fn filepath(file: String) -> String {
 /// documented anywhere. So we ignore the rest for now.
 #[derive(Clone, Debug, Deserialize)]
 #[serde(rename_all = "camelCase")]
+#[allow(dead_code)]
 pub struct TraceItem {
     pub thread: u32,
     pub step_type: String,
@@ -300,6 +301,7 @@ pub struct TraceItem {
 /// Note: this struct can have a lot of different fields depending on the value type.
 /// The fields included right now are relevant to primitive types.
 #[derive(Clone, Debug, Deserialize)]
+#[allow(dead_code)]
 pub struct TraceValue {
     pub name: String,
     pub binary: Option<String>,

rust-toolchain.toml

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