Clippy fixes for upcoming rust toolchain update

cprover_bindings/src/goto_program/expr.rs

@@ -433,9 +433,7 @@ impl Expr {
             assert_eq!(size as usize, elems.len());
             assert!(
                 elems.iter().all(|x| x.typ == *value_typ),
-                "Array type and value types don't match: \n{:?}\n{:?}",
-                typ,
-                elems
+                "Array type and value types don't match: \n{typ:?}\n{elems:?}"
             );
         } else {
             unreachable!("Can't make an array_val with non-array target type {:?}", typ);
@@ -448,9 +446,7 @@ impl Expr {
             assert_eq!(size as usize, elems.len());
             assert!(
                 elems.iter().all(|x| x.typ == *value_typ),
-                "Vector type and value types don't match: \n{:?}\n{:?}",
-                typ,
-                elems
+                "Vector type and value types don't match: \n{typ:?}\n{elems:?}"
             );
         } else {
             unreachable!("Can't make a vector_val with non-vector target type {:?}", typ);
@@ -642,9 +638,7 @@ impl Expr {
     pub fn call(self, arguments: Vec<Expr>) -> Self {
         assert!(
             Expr::typecheck_call(&self, &arguments),
-            "Function call does not type check:\nfunc: {:?}\nargs: {:?}",
-            self,
-            arguments
+            "Function call does not type check:\nfunc: {self:?}\nargs: {arguments:?}"
         );
         let typ = self.typ().return_type().unwrap().clone();
         expr!(FunctionCall { function: self, arguments }, typ)
@@ -658,9 +652,7 @@ impl Expr {
         let field: InternedString = field.into();
         assert!(
             self.typ.is_struct_tag() || self.typ.is_union_tag(),
-            "Can't apply .member operation to\n\t{:?}\n\t{}",
-            self,
-            field,
+            "Can't apply .member operation to\n\t{self:?}\n\t{field}",
         );
         if let Some(ty) = self.typ.lookup_field_type(field, symbol_table) {
             expr!(Member { lhs: self, field }, ty)
@@ -701,10 +693,7 @@ impl Expr {
         // Check that each formal field has an value
         assert!(
             fields.iter().zip(values.iter()).all(|(f, v)| f.typ() == *v.typ()),
-            "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}",
-            typ,
-            fields,
-            values
+            "Error in struct_expr; value type does not match field type.\n\t{typ:?}\n\t{fields:?}\n\t{values:?}"
         );
         expr!(Struct { values }, typ)
     }
@@ -720,18 +709,14 @@ impl Expr {
     ) -> Self {
         assert!(
             typ.is_struct_tag(),
-            "Error in struct_expr; must be given a struct_tag.\n\t{:?}\n\t{:?}",
-            typ,
-            components
+            "Error in struct_expr; must be given a struct_tag.\n\t{typ:?}\n\t{components:?}"
         );
         let fields = typ.lookup_components(symbol_table).unwrap();
         let non_padding_fields: Vec<_> = fields.iter().filter(|x| !x.is_padding()).collect();
         assert_eq!(
             non_padding_fields.len(),
             components.len(),
-            "Error in struct_expr; mismatch in number of fields and components.\n\t{:?}\n\t{:?}",
-            typ,
-            components
+            "Error in struct_expr; mismatch in number of fields and components.\n\t{typ:?}\n\t{components:?}"
         );
 
         // Check that each formal field has an value
@@ -790,28 +775,21 @@ impl Expr {
     ) -> Self {
         assert!(
             typ.is_struct_tag(),
-            "Error in struct_expr; must be given struct_tag.\n\t{:?}\n\t{:?}",
-            typ,
-            non_padding_values
+            "Error in struct_expr; must be given struct_tag.\n\t{typ:?}\n\t{non_padding_values:?}"
         );
         let fields = typ.lookup_components(symbol_table).unwrap();
         let non_padding_fields: Vec<_> = fields.iter().filter(|x| !x.is_padding()).collect();
         assert_eq!(
             non_padding_fields.len(),
             non_padding_values.len(),
-            "Error in struct_expr; mismatch in number of fields and values.\n\t{:?}\n\t{:?}",
-            typ,
-            non_padding_values
+            "Error in struct_expr; mismatch in number of fields and values.\n\t{typ:?}\n\t{non_padding_values:?}"
         );
         assert!(
             non_padding_fields
                 .iter()
                 .zip(non_padding_values.iter())
                 .all(|(f, v)| f.field_typ().unwrap() == v.typ()),
-            "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}",
-            typ,
-            non_padding_fields,
-            non_padding_values
+            "Error in struct_expr; value type does not match field type.\n\t{typ:?}\n\t{non_padding_fields:?}\n\t{non_padding_values:?}"
         );
 
         let values = fields
@@ -834,25 +812,18 @@ impl Expr {
     ) -> Self {
         assert!(
             typ.is_struct_tag() || typ.is_struct(),
-            "Error in struct_expr; must be given struct.\n\t{:?}\n\t{:?}",
-            typ,
-            values
+            "Error in struct_expr; must be given struct.\n\t{typ:?}\n\t{values:?}"
         );
         let typ = typ.aggr_tag().unwrap();
         let fields = typ.lookup_components(symbol_table).unwrap();
         assert_eq!(
             fields.len(),
             values.len(),
-            "Error in struct_expr; mismatch in number of padded fields and padded values.\n\t{:?}\n\t{:?}",
-            typ,
-            values
+            "Error in struct_expr; mismatch in number of padded fields and padded values.\n\t{typ:?}\n\t{values:?}"
         );
         assert!(
             fields.iter().zip(values.iter()).all(|(f, v)| &f.typ() == v.typ()),
-            "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}",
-            typ,
-            fields,
-            values
+            "Error in struct_expr; value type does not match field type.\n\t{typ:?}\n\t{fields:?}\n\t{values:?}"
         );
 
         Expr::struct_expr_with_explicit_padding(typ, fields, values)
@@ -1028,10 +999,7 @@ impl Expr {
     pub fn binop(self, op: BinaryOperator, rhs: Expr) -> Expr {
         assert!(
             Expr::typecheck_binop_args(op, &self, &rhs),
-            "BinaryOperation Expression does not typecheck {:?} {:?} {:?}",
-            op,
-            self,
-            rhs
+            "BinaryOperation Expression does not typecheck {op:?} {self:?} {rhs:?}"
         );
         expr!(BinOp { op, lhs: self, rhs }, Expr::binop_return_type(op, &self, &rhs))
     }
@@ -1041,10 +1009,7 @@ impl Expr {
     pub fn vector_cmp(self, op: BinaryOperator, rhs: Expr, ret_typ: Type) -> Expr {
         assert!(
             Expr::typecheck_vector_cmp_expr(&self, &rhs, &ret_typ),
-            "vector comparison expression does not typecheck {:?} {:?} {:?}",
-            self,
-            rhs,
-            ret_typ,
+            "vector comparison expression does not typecheck {self:?} {rhs:?} {ret_typ:?}",
         );
         expr!(BinOp { op, lhs: self, rhs }, ret_typ)
     }
@@ -1483,9 +1448,7 @@ impl Expr {
     pub fn reinterpret_cast(self, t: Type) -> Expr {
         assert!(
             self.can_take_address_of(),
-            "Can't take address of {:?} when coercing to {:?}",
-            self,
-            t
+            "Can't take address of {self:?} when coercing to {t:?}"
         );
         self.address_of().cast_to(t.to_pointer()).dereference()
     }

cprover_bindings/src/goto_program/stmt.rs

@@ -264,9 +264,7 @@ impl Stmt {
     ) -> Self {
         assert!(
             Expr::typecheck_call(&function, &arguments),
-            "Function call does not type check:\nfunc: {:?}\nargs: {:?}",
-            function,
-            arguments
+            "Function call does not type check:\nfunc: {function:?}\nargs: {arguments:?}"
         );
         if let Some(lhs) = &lhs {
             assert_eq!(lhs.typ(), function.typ().return_type().unwrap())

cprover_bindings/src/goto_program/symbol.rs

@@ -74,9 +74,7 @@ impl Symbol {
         // See https://github.com/model-checking/kani/issues/1361#issuecomment-1181499683
         assert!(
             name.to_string().ends_with(&base_name.map_or(String::new(), |s| s.to_string())),
-            "Symbol's base_name must be the suffix of its name.\nName: {:?}\nBase name: {:?}",
-            name,
-            base_name
+            "Symbol's base_name must be the suffix of its name.\nName: {name:?}\nBase name: {base_name:?}"
         );
         Symbol {
             name,

cprover_bindings/src/goto_program/typ.rs

@@ -191,9 +191,7 @@ impl DatatypeComponent {
         let name = name.into();
         assert!(
             Self::typecheck_datatype_field(&typ),
-            "Illegal field.\n\tName: {}\n\tType: {:?}",
-            name,
-            typ
+            "Illegal field.\n\tName: {name}\n\tType: {typ:?}"
         );
         Field { name, typ }
     }
@@ -942,13 +940,7 @@ impl Type {
         identifier: Option<InternedString>,
         base_name: Option<InternedString>,
     ) -> Parameter {
-        assert!(
-            self.can_be_lvalue(),
-            "Expected lvalue from {:?} {:?} {:?}",
-            self,
-            identifier,
-            base_name
-        );
+        assert!(self.can_be_lvalue(), "Expected lvalue from {self:?} {identifier:?} {base_name:?}");
         Parameter { identifier, base_name, typ: self }
     }
 
@@ -1133,13 +1125,11 @@ impl Type {
     ) -> Self {
         assert!(
             Type::components_are_unique(&components),
-            "Components contain duplicates: {:?}",
-            components
+            "Components contain duplicates: {components:?}"
         );
         assert!(
             Type::components_in_valid_order_for_struct(&components),
-            "Components are not in valid order for struct: {:?}",
-            components
+            "Components are not in valid order for struct: {components:?}"
         );
 
         let tag = tag.into();
@@ -1168,13 +1158,11 @@ impl Type {
         let tag = tag.into();
         assert!(
             Type::components_are_unique(&components),
-            "Components contain duplicates: {:?}",
-            components
+            "Components contain duplicates: {components:?}"
         );
         assert!(
             Type::components_are_not_flexible_array(&components),
-            "Unions cannot contain flexible arrays: {:?}",
-            components
+            "Unions cannot contain flexible arrays: {components:?}"
         );
         Union { tag, components }
     }

kani-compiler/src/codegen_cprover_gotoc/archive.rs

@@ -45,8 +45,7 @@ impl<'a> ArchiveBuilder<'a> {
             BuilderKind::Gnu(ar::GnuBuilder::new(
                 File::create(&output).unwrap_or_else(|err| {
                     sess.fatal(&format!(
-                        "error opening destination during archive building: {}",
-                        err
+                        "error opening destination during archive building: {err}"
                     ));
                 }),
                 self.entries.iter().map(|(name, _)| name.clone()).collect(),

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

@@ -297,8 +297,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "https://github.com/model-checking/kani/issues/new?template=bug_report.md";
 
         let assert_msg = format!(
-            "Kani-internal sanity check: {}. Please report failures:\n{}",
-            message, BUG_REPORT_URL
+            "Kani-internal sanity check: {message}. Please report failures:\n{BUG_REPORT_URL}"
         );
 
         self.codegen_assert_assume(cond, PropertyClass::SanityCheck, &assert_msg, loc)

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

@@ -1499,8 +1499,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if !ret_typ.base_type().unwrap().is_integer() {
             let (_, rust_base_type) = rust_ret_type.simd_size_and_type(self.tcx);
             let err_msg = format!(
-                "expected return type with integer elements, found `{}` with non-integer `{}`",
-                rust_ret_type, rust_base_type,
+                "expected return type with integer elements, found `{rust_ret_type}` with non-integer `{rust_base_type}`",
             );
             self.tcx.sess.span_err(span.unwrap(), err_msg);
         }
@@ -1541,7 +1540,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let check_stmt = self.codegen_assert_assume(
             check.not(),
             PropertyClass::ArithmeticOverflow,
-            format!("attempt to compute {} which would overflow", intrinsic).as_str(),
+            format!("attempt to compute {intrinsic} which would overflow").as_str(),
             loc,
         );
         let res = op_fun(a, b);
@@ -1591,8 +1590,7 @@ impl<'tcx> GotocCtx<'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!(
-                "expected return type of length {}, found `{}` with length {}",
-                n, rust_ret_type, ret_type_len
+                "expected return type of length {n}, found `{rust_ret_type}` with length {ret_type_len}"
             );
             self.tcx.sess.span_err(span.unwrap(), err_msg);
         }

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

@@ -220,7 +220,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         // TODO: Handle cases with other types such as tuples and larger integers.
                         let loc = self.codegen_span_option(span.cloned());
                         let typ = self.codegen_ty(lit_ty);
-                        let operation_name = format!("Constant slice for type {}", slice_ty);
+                        let operation_name = format!("Constant slice for type {slice_ty}");
                         return self.codegen_unimplemented_expr(
                             &operation_name,
                             typ,

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

@@ -173,8 +173,7 @@ impl<'tcx> ProjectedPlace<'tcx> {
             Self::check_expr_typ_mismatch(&goto_expr, &mir_typ_or_variant, ctx)
         {
             let msg = format!(
-                "Unexpected type mismatch in projection:\n{:?}\nExpr type\n{:?}\nType from MIR\n{:?}",
-                goto_expr, expr_ty, ty_from_mir
+                "Unexpected type mismatch in projection:\n{goto_expr:?}\nExpr type\n{expr_ty:?}\nType from MIR\n{ty_from_mir:?}"
             );
             warn!("{}", msg);
             // TODO: there's an expr type mismatch with the rust 2022-11-20 toolchain

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

@@ -940,8 +940,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=0f6eef4f6abeb279031444735e73d2e1
             assert!(
                 matches!(operand_type.kind(), ty::Never),
-                "Expected Never, got: {:?}",
-                operand_type
+                "Expected Never, got: {operand_type:?}"
             );
             Type::size_t().zero()
         } else {

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

@@ -135,8 +135,8 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This method prints the details of a GotoC type, for debugging purposes.
     #[allow(unused)]
     pub(crate) fn debug_print_type_recursively(&self, ty: &Type) -> String {
-        fn debug_write_type<'tcx>(
-            ctx: &GotocCtx<'tcx>,
+        fn debug_write_type(
+            ctx: &GotocCtx,
             ty: &Type,
             out: &mut impl std::fmt::Write,
             indent: usize,
@@ -1782,12 +1782,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         let mut typ = struct_type;
         while let ty::Adt(adt_def, adt_substs) = typ.kind() {
-            assert_eq!(
-                adt_def.variants().len(),
-                1,
-                "Expected a single-variant ADT. Found {:?}",
-                typ
-            );
+            assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}");
             let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
             let last_field = fields.last().expect("Trait should be the last element.");
             typ = last_field.ty(self.tcx, adt_substs);

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -267,8 +267,7 @@ fn check_options(session: &Session) {
         Some(1) => (),
         Some(align) => {
             let err_msg = format!(
-                "Kani requires the target architecture option `min_global_align` to be 1, but it is {}.",
-                align
+                "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}."
             );
             session.err(&err_msg);
         }
@@ -322,7 +321,7 @@ fn check_crate_items(gcx: &GotocCtx) {
 }
 
 /// Prints a report at the end of the compilation.
-fn print_report<'tcx>(ctx: &GotocCtx, tcx: TyCtxt<'tcx>) {
+fn print_report(ctx: &GotocCtx, tcx: TyCtxt) {
     // Print all unsupported constructs.
     if !ctx.unsupported_constructs.is_empty() {
         // Sort alphabetically.

kani-compiler/src/kani_middle/provide.rs

@@ -32,7 +32,7 @@ pub fn provide_extern(providers: &mut ExternProviders) {
 
 /// Returns the optimized code for the function associated with `def_id` by
 /// running rustc's optimization passes followed by Kani-specific passes.
-fn run_mir_passes<'tcx, const EXTERN: bool>(tcx: TyCtxt<'tcx>, def_id: DefId) -> &Body<'tcx> {
+fn run_mir_passes<const EXTERN: bool>(tcx: TyCtxt, def_id: DefId) -> &Body {
     tracing::debug!(?def_id, "Run rustc transformation passes");
     let optimized_mir = if EXTERN {
         rustc_interface::DEFAULT_EXTERN_QUERY_PROVIDERS.optimized_mir