Update to Rust edition 2024 (#4197)

tautschnig · Carolyn Zech · web-flow · commit 173594b7d616 · 2025-07-04T09:11:24.000Z
Upstream change rust-lang/rust#143214 (Remove let_chains unstable feature) requires us to either remove the use of `let` in several places or wholesale update to Rust edition 2024. Doing this edition update seems worthwhile to keep accessing more recent features, but required code changes in several places. This is in preparation of the toolchain upgrade to 2025-07-03, but does not actually do this upgrade for it will require other, unrelated changes. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech <cmzech@amazon.com>
diff --git a/Cargo.toml b/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani-verifier"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
 keywords = ["model-checking", "verification"]
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "cprover_bindings"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
@@ -1131,7 +1131,7 @@ impl Type {
         let concrete = self.unwrap_typedef();
         match concrete {
             CInteger(CIntType::SizeT) => Some(CInteger(CIntType::SSizeT)),
-            Unsignedbv { ref width } => Some(Signedbv { width: *width }),
+            Unsignedbv { width } => Some(Signedbv { width: *width }),
             CInteger(CIntType::SSizeT) | Signedbv { .. } => Some(self.clone()),
             _ => None,
         }
@@ -1144,7 +1144,7 @@ impl Type {
         let concrete = self.unwrap_typedef();
         match concrete {
             CInteger(CIntType::SSizeT) => Some(CInteger(CIntType::SizeT)),
-            Signedbv { ref width } => Some(Unsignedbv { width: *width }),
+            Signedbv { width } => Some(Unsignedbv { width: *width }),
             CInteger(CIntType::SizeT) | Unsignedbv { .. } => Some(self.clone()),
             _ => None,
         }
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani-compiler"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -651,7 +651,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Ensure that the given instance is in the symbol table, returning the symbol.
     fn codegen_func_symbol(&mut self, instance: Instance) -> &Symbol {
-        let sym = if instance.is_foreign_item() && !instance.has_body() {
+        if instance.is_foreign_item() && !instance.has_body() {
             // Get the symbol that represents a foreign instance.
             self.codegen_foreign_fn(instance)
         } else {
@@ -661,8 +661,7 @@ impl<'tcx> GotocCtx<'tcx> {
             self.symbol_table
                 .lookup(&func)
                 .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage"))
-        };
-        sym
+        }
     }
 
     /// Generate a goto expression that references the function identified by `instance`.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -857,7 +857,7 @@ impl GotocCtx<'_> {
                     NullOp::ContractChecks | NullOp::UbChecks => Expr::c_false(),
                 }
             }
-            Rvalue::ShallowInitBox(ref operand, content_ty) => {
+            Rvalue::ShallowInitBox(operand, content_ty) => {
                 // The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box<T>.
                 // See https://github.com/rust-lang/compiler-team/issues/460 for more details.
                 let operand = self.codegen_operand_stable(operand);
@@ -947,7 +947,7 @@ impl GotocCtx<'_> {
                 let pt = self.place_ty_stable(p);
                 self.codegen_get_discriminant(place, pt, res_ty)
             }
-            Rvalue::Aggregate(ref k, operands) => {
+            Rvalue::Aggregate(k, operands) => {
                 self.codegen_rvalue_aggregate(k, operands, res_ty, loc)
             }
             Rvalue::ThreadLocalRef(def_id) => {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -216,7 +216,7 @@ impl GotocCtx<'_> {
             // https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.NonDivergingIntrinsic.html#variant.Assume
             // Informs the optimizer that a condition is always true.
             // If the condition is false, the behavior is undefined.
-            StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(ref op)) => {
+            StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(op)) => {
                 let cond = self.codegen_operand_stable(op).cast_to(Type::bool());
                 self.codegen_assert_assume(
                     cond,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1754,7 +1754,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &self,
         instance: InstanceStable,
         fn_abi: &'a FnAbi,
-    ) -> impl Iterator<Item = (usize, &'a ArgAbi)> {
+    ) -> impl Iterator<Item = (usize, &'a ArgAbi)> + use<'a> {
         let requires_caller_location = self.requires_caller_location(instance);
         let num_args = fn_abi.args.len();
         fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -451,7 +451,7 @@ impl GotocCtx<'_> {
     ) -> Stmt {
         match stmt.body() {
             StmtBody::Return(Some(expr)) => {
-                if let ExprValue::Symbol { ref identifier } = expr.value() {
+                if let ExprValue::Symbol { identifier } = expr.value() {
                     *return_symbol = Some(Expr::symbol_expression(*identifier, expr.typ().clone()));
                     Stmt::goto(*end_label, *stmt.location())
                 } else {
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
@@ -150,7 +150,7 @@ fn resolve_path<'tcx>(
     path.segments.into_iter().try_fold(path.base, |base, segment| {
         let name = segment.ident.to_string();
         let def_kind = tcx.def_kind(base);
-        let next_item = match def_kind {
+        match def_kind {
             DefKind::ForeignMod | DefKind::Mod => resolve_in_module(tcx, base, &name),
             DefKind::Struct | DefKind::Enum | DefKind::Union => {
                 resolve_in_type_def(tcx, base, &path.base_path_args, &name)
@@ -160,8 +160,7 @@ fn resolve_path<'tcx>(
                 debug!(?base, ?kind, "resolve_path: unexpected item");
                 Err(ResolveError::UnexpectedType { tcx, item: base, expected: "module" })
             }
-        };
-        next_item
+        }
     })
 }
 
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -88,9 +88,7 @@ impl AnyModifiesPass {
         let kani_write_any_str = kani_fns.get(&KaniModel::WriteAnyStr.into()).copied();
         let target_fn = if let Some(harness) = unit.harnesses.first() {
             let attributes = KaniAttributes::for_instance(tcx, *harness);
-            let target_fn =
-                attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern());
-            target_fn
+            attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern())
         } else {
             None
         };
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani-driver"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
 homepage = "https://github.com/model-checking/kani"
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani_metadata"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs
@@ -42,7 +42,7 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
 
 /// Iterate over `any_raw_internal` since CBMC produces assignment per element.
 pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
-    [(); N].map(|_| crate::any_raw_internal::<T>())
+    unsafe { [(); N].map(|_| crate::any_raw_internal::<T>()) }
 }
 
 /// Concrete playback implementation of
diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs
@@ -189,9 +189,11 @@ mod intrinsics {
             "Expected size of input and lanes to match",
         );
 
-        let data = &*(&input as *const T as *const [E; LANES]);
-        let mask = simd_bitmask_impl(data);
-        (&mask as *const [u8; mask_len(LANES)] as *const U).read()
+        unsafe {
+            let data = &*(&input as *const T as *const [E; LANES]);
+            let mask = simd_bitmask_impl(data);
+            (&mask as *const [u8; mask_len(LANES)] as *const U).read()
+        }
     }
 
     /// Structure used for sanity check our parameters.
diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani_core"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 description = "Define core constructs to use with Kani"
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
@@ -4,7 +4,7 @@
 [package]
 name = "kani_macros"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
@@ -155,7 +155,7 @@ fn field_refs(ident: &Ident, data: &Data) -> TokenStream {
 /// references to the struct fields. See `field_refs` for more details.
 fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             let field_refs: Vec<TokenStream> = fields
                 .named
                 .iter()
@@ -187,7 +187,7 @@ fn safe_body_default(ident: &Ident, data: &Data) -> TokenStream {
 
 fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             let field_safe_calls: Vec<TokenStream> = fields
                 .named
                 .iter()
@@ -204,7 +204,7 @@ fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
                 quote! { true }
             }
         }
-        Fields::Unnamed(ref fields) => {
+        Fields::Unnamed(fields) => {
             let field_safe_calls: Vec<TokenStream> = fields
                 .unnamed
                 .iter()
@@ -232,7 +232,7 @@ fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
 /// For unit field, generate an empty initialization.
 fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             // Use the span of each `syn::Field`. This way if one of the field types does not
             // implement `Arbitrary` then the compiler's error message underlines which field it
             // is. An example is shown in the readme of the parent directory.
@@ -246,7 +246,7 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
                 #ident {#( #init,)*}
             }
         }
-        Fields::Unnamed(ref fields) => {
+        Fields::Unnamed(fields) => {
             // Expands to an expression like
             // Self(kani::any(), kani::any(), ..., kani::any());
             let init = fields.unnamed.iter().map(|field| {
@@ -490,7 +490,7 @@ fn has_field_safety_constraints(ident: &Ident, data: &Data) -> bool {
 /// field.
 fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool {
     match fields {
-        Fields::Named(ref fields) => fields
+        Fields::Named(fields) => fields
             .named
             .iter()
             .any(|field| field.attrs.iter().any(|attr| attr.path().is_ident("safety_constraint"))),
@@ -570,7 +570,7 @@ fn safe_body_from_fields_attr_inner(ident: &Ident, fields: &Fields) -> TokenStre
         // Expands to the expression
         // `<safety_cond1> && <safety_cond2> && ..`
         // where `<safety_condN>` is the safety condition specified for the N-th field.
-        Fields::Named(ref fields) => {
+        Fields::Named(fields) => {
             let safety_conds: Vec<TokenStream> =
                 fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect();
             quote! { #(#safety_conds)&&* }
diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -128,7 +128,7 @@ impl<'a> ContractConditionsHandler<'a> {
         replace_closure: &TokenStream,
         check_closure: &TokenStream,
     ) -> TokenStream {
-        let ItemFn { ref sig, .. } = self.annotated_fn;
+        let ItemFn { sig, .. } = self.annotated_fn;
         let output = &sig.output;
         let span = Span::call_site();
         let result = Ident::new(INTERNAL_RESULT_IDENT, span);
diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs
@@ -19,10 +19,10 @@ impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState {
     /// Find out if this attribute could be describing a "contract handling"
     /// state and if so return it.
     fn try_from(attribute: &'a syn::Attribute) -> Result<Self, Self::Error> {
-        if let syn::Meta::NameValue(nv) = &attribute.meta {
-            if matches_path(&nv.path, &["kanitool", "checked_with"]) {
-                return Ok(ContractFunctionState::Expanded);
-            }
+        if let syn::Meta::NameValue(nv) = &attribute.meta
+            && matches_path(&nv.path, &["kanitool", "checked_with"])
+        {
+            return Ok(ContractFunctionState::Expanded);
         }
         Err(None)
     }
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -51,14 +51,14 @@ pub fn split_for_remembers(stmts: &[Stmt], contract_mode: ContractMode) -> (&[St
     };
 
     for stmt in stmts {
-        if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt {
-            if let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref() {
-                let first_two_idents =
-                    segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
-
-                if first_two_idents == vec!["kani", check_str] {
-                    pos += 1;
-                }
+        if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt
+            && let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref()
+        {
+            let first_two_idents =
+                segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
+
+            if first_two_idents == vec!["kani", check_str] {
+                pos += 1;
             }
         }
     }
@@ -189,7 +189,7 @@ impl<T: OldTrigger> syn::visit_mut::VisitMut for OldVisitor<'_, T> {
         };
         if trigger {
             let span = ex.span();
-            let new_expr = if let Expr::Call(ExprCall { ref mut args, .. }) = ex {
+            let new_expr = if let Expr::Call(ExprCall { args, .. }) = ex {
                 self.t
                     .trigger(args.iter_mut().next().unwrap(), span, self.remembers_exprs)
                     .then(|| args.pop().unwrap().into_value())
diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs
@@ -137,20 +137,18 @@ impl VisitMut for CallReplacer {
         // Visit nested expressions first
         syn::visit_mut::visit_expr_mut(self, expr);
 
-        if let Expr::Call(call) = expr {
-            if let Expr::Path(expr_path) = &*call.func {
-                if self.should_replace(expr_path) {
-                    let replace_var =
-                        self.replacements.iter().find(|(e, _)| e == expr).map(|(_, v)| v);
-                    if let Some(var) = replace_var {
-                        *expr = syn::parse_quote!(#var);
-                    } else {
-                        let new_var = self.generate_var_name();
-                        self.replacements.push((expr.clone(), new_var.clone()));
-                        *expr = syn::parse_quote!(#new_var);
-                    };
-                }
-            }
+        if let Expr::Call(call) = expr
+            && let Expr::Path(expr_path) = &*call.func
+            && self.should_replace(expr_path)
+        {
+            let replace_var = self.replacements.iter().find(|(e, _)| e == expr).map(|(_, v)| v);
+            if let Some(var) = replace_var {
+                *expr = syn::parse_quote!(#var);
+            } else {
+                let new_var = self.generate_var_name();
+                self.replacements.push((expr.clone(), new_var.clone()));
+                *expr = syn::parse_quote!(#new_var);
+            };
         }
     }
 }
@@ -226,10 +224,10 @@ fn transform_break_continue(block: &mut Block) {
         return (true, None);
     };
     // Add semicolon to the last statement if it's an expression without semicolon
-    if let Some(Stmt::Expr(_, ref mut semi)) = block.stmts.last_mut() {
-        if semi.is_none() {
-            *semi = Some(Default::default());
-        }
+    if let Some(&mut Stmt::Expr(_, ref mut semi)) = block.stmts.last_mut()
+        && semi.is_none()
+    {
+        *semi = Some(Default::default());
     }
     block.stmts.push(return_stmt);
 }
@@ -300,8 +298,8 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
     register_name.push_str(&loop_id);
     let register_ident = format_ident!("{}", register_name);
 
-    match loop_stmt {
-        Stmt::Expr(ref mut e, _) => match e {
+    match &mut loop_stmt {
+        &mut Stmt::Expr(ref mut e, _) => match *e {
             Expr::While(ref mut ew) => {
                 let new_cond: Expr = syn::parse(
                     quote!(
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
@@ -6,7 +6,7 @@
 # standard library symbols are preserved
 name = "std"
 version = "0.64.0"
-edition = "2021"
+edition = "2024"
 license = "MIT OR Apache-2.0"
 publish = false
 
diff --git a/rustfmt.toml b/rustfmt.toml
diff --git a/src/lib.rs b/src/lib.rs
diff --git a/src/setup.rs b/src/setup.rs
diff --git a/tests/kani/Coroutines/issue-1593.rs b/tests/kani/Coroutines/issue-1593.rs
diff --git a/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
diff --git a/tools/compiletest/Cargo.toml b/tools/compiletest/Cargo.toml
diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs
diff --git a/tools/compiletest/src/raise_fd_limit.rs b/tools/compiletest/src/raise_fd_limit.rs
diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml
diff --git a/tools/scanner/Cargo.toml b/tools/scanner/Cargo.toml
diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs

Original file line number	Diff line number	Diff line change
`@@ -857,7 +857,7 @@ impl GotocCtx<'_> {`
`857`	`857`	`NullOp::ContractChecks \| NullOp::UbChecks => Expr::c_false(),`
`858`	`858`	`}`
`859`	`859`	`}`
`860`		`- Rvalue::ShallowInitBox(ref operand, content_ty) => {`
	`860`	`+ Rvalue::ShallowInitBox(operand, content_ty) => {`
`861`	`861`	`// The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box<T>.`
`862`	`862`	`// See https://github.com/rust-lang/compiler-team/issues/460 for more details.`
`863`	`863`	`let operand = self.codegen_operand_stable(operand);`
`@@ -947,7 +947,7 @@ impl GotocCtx<'_> {`
`947`	`947`	`let pt = self.place_ty_stable(p);`
`948`	`948`	`self.codegen_get_discriminant(place, pt, res_ty)`
`949`	`949`	`}`
`950`		`- Rvalue::Aggregate(ref k, operands) => {`
	`950`	`+ Rvalue::Aggregate(k, operands) => {`
`951`	`951`	`self.codegen_rvalue_aggregate(k, operands, res_ty, loc)`
`952`	`952`	`}`
`953`	`953`	`Rvalue::ThreadLocalRef(def_id) => {`