Upgrade Rust toolchain to 2025-07-10

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -36,8 +36,8 @@ use rustc_middle::util::Providers;
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::rustc_internal;
 use stable_mir::{CrateDef, DefId};
 use std::any::Any;
 use std::fs::File;

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -56,17 +56,17 @@ use charon_lib::{error_assert, error_or_panic};
 use core::panic;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::{TyCtxt, TypingEnv};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::{Instance, InstanceDef};
 use stable_mir::mir::{
     AggregateKind, BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability,
     Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator,
     TerminatorKind, UnOp, VarDebugInfoContents,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     AdtDef, AdtKind, Allocation, ConstantKind, FnDef, GenericArgKind, GenericArgs,
-    GenericParamDefKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl,
-    TraitDef, Ty, TyConst, TyConstKind, TyKind, UintTy,
+    GenericParamDefKind, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl, TraitDef,
+    Ty, TyConst, TyConstKind, TyKind, UintTy,
 };
 use stable_mir::{CrateDef, CrateDefType, DefId};
 use std::collections::HashMap;

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

@@ -6,10 +6,10 @@ use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::mir::{Local, VarDebugInfoContents};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
 
 impl GotocCtx<'_> {

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

@@ -241,8 +241,8 @@ pub mod rustc_smir {
     use rustc_middle::mir::coverage::BasicCoverageBlock;
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::ty::TyCtxt;
-    use rustc_smir::rustc_internal;
     use stable_mir::mir::mono::Instance;
+    use stable_mir::rustc_internal;
     use stable_mir::{Filename, Opaque};
 
     type CoverageOpaque = stable_mir::Opaque;
@@ -285,7 +285,7 @@ pub mod rustc_smir {
         instance: Instance,
     ) -> Option<(SourceRegion, Filename)> {
         // We need to pull the coverage info from the internal MIR instance.
-        let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
+        let instance_def = rustc_internal::internal(tcx, instance.def.def_id());
         let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
         let filename = rustc_internal::stable(body.span).get_filename();
         // Some functions, like `std` ones, may not have coverage info attached

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

@@ -10,9 +10,9 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::ty::TypingEnv;
 use rustc_middle::ty::layout::ValidityRequirement;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Operand, Place};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 

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

@@ -6,11 +6,11 @@ use crate::kani_middle::is_anon_static;
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type};
 use rustc_middle::ty::Const as ConstInternal;
-use rustc_smir::rustc_internal;
 use rustc_span::Span as SpanInternal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, StaticDef};
 use stable_mir::mir::{Mutability, Operand};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty,
     TyConst, TyConstKind, TyKind, UintTy,

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

@@ -14,8 +14,8 @@ use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type};
 use rustc_abi::{TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
 use tracing::{debug, trace, warn};
 

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

@@ -20,12 +20,12 @@ use cbmc::{InternString, InternedString, btree_string_map};
 use num::bigint::BigInt;
 use rustc_abi::{FieldsShape, TagEncoding, Variants};
 use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry};
-use rustc_smir::rustc_internal;
 use stable_mir::abi::{Primitive, Scalar, ValueAbi};
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     Binder, ClosureKind, ExistentialPredicate, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy,
     VariantIdx,

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

@@ -7,8 +7,8 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
 use lazy_static::lazy_static;
 use rustc_hir::Attribute;
-use rustc_smir::rustc_internal;
 use rustc_span::Span;
+use stable_mir::rustc_internal;
 use stable_mir::ty::Span as SpanStable;
 use std::collections::HashMap;
 

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

@@ -12,14 +12,14 @@ use rustc_abi::Size;
 use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{List, TypingEnv};
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::{
     AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
     RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
 use tracing::{debug, debug_span, trace};
 

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

@@ -10,9 +10,9 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::abi::LayoutOf;
 use cbmc::goto_program::Type;
 use rustc_middle::ty::layout::{LayoutOf as _, TyAndLayout};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Local, Operand, Place, Rvalue};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnSig, RigidTy, Ty, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {

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

@@ -20,11 +20,11 @@ use rustc_middle::ty::{
 };
 use rustc_middle::ty::{ExistentialTraitRef, GenericArgsRef};
 use rustc_middle::ty::{List, TypeFoldable};
-use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::Body;
 use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
     Ty as StableTy,

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -37,11 +37,11 @@ use rustc_middle::util::Providers;
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
-use rustc_smir::rustc_internal;
 use rustc_span::{Symbol, sym};
 use rustc_target::spec::PanicStrategy;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::rustc_internal;
 use std::any::Any;
 use std::collections::BTreeMap;
 use std::fmt::Write;

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

@@ -5,10 +5,10 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::InternedString;
 use cbmc::goto_program::Stmt;
 use rustc_middle::ty::Instance as InstanceInternal;
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, Local, LocalDecl, Rvalue, visit::Location, visit::MirVisitor};
+use stable_mir::rustc_internal;
 use std::collections::{HashMap, HashSet};
 
 /// This structure represents useful data about the function we are currently compiling.

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -17,9 +17,9 @@ use cbmc::goto_program::CIntType;
 use cbmc::goto_program::Symbol as GotoSymbol;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Place};
+use stable_mir::rustc_internal;
 use stable_mir::ty::ClosureKind;
 use stable_mir::ty::RigidTy;
 use stable_mir::{CrateDef, ty::Span};

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -5,7 +5,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type};
 use cbmc::{InternedString, btree_string_map};
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
+use stable_mir::rustc_internal;
 use stable_mir::ty::Span;
 use tracing::debug;
 

kani-compiler/src/kani_compiler.rs

@@ -29,7 +29,7 @@ use rustc_driver::{Callbacks, Compilation, run_compiler};
 use rustc_interface::Config;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::ErrorOutputType;
-use rustc_smir::rustc_internal;
+use stable_mir::rustc_internal;
 use std::sync::{Arc, Mutex};
 use tracing::debug;
 

kani-compiler/src/kani_middle/attributes.rs

@@ -11,10 +11,10 @@ use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId};
 use rustc_middle::ty::{Instance, TyCtxt, TyKind};
 use rustc_session::Session;
-use rustc_smir::rustc_internal;
 use rustc_span::{Span, Symbol};
 use stable_mir::crate_def::Attribute as AttributeStable;
 use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::rustc_internal;
 use stable_mir::{CrateDef, DefId as StableDefId, Symbol as SymbolStable};
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};

kani-compiler/src/kani_middle/codegen_units.rs

@@ -27,9 +27,10 @@ use regex::RegexSet;
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
-use rustc_smir::rustc_internal;
+use rustc_smir::IndexedVal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, Ty, TyKind};
+use stable_mir::rustc_internal;
+use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind};
 use stable_mir::{CrateDef, CrateItem};
 use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fs::File;

kani-compiler/src/kani_middle/coercion.rs

@@ -18,9 +18,9 @@ use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::{PseudoCanonicalInput, Ty, TyCtxt, TypingEnv};
-use rustc_smir::rustc_internal;
 use rustc_span::DUMMY_SP;
 use stable_mir::Symbol;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 use tracing::trace;
 

kani-compiler/src/kani_middle/mod.rs

@@ -9,9 +9,9 @@ use crate::kani_queries::QueryDb;
 use fxhash::FxHashMap;
 use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE};
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::TerminatorKind;
 use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{
     AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind,
 };

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

@@ -41,9 +41,9 @@ use rustc_middle::{
     ty::{Instance, InstanceKind, List, TyCtxt, TyKind, TypingEnv},
 };
 use rustc_mir_dataflow::{Analysis, Forward, JoinSemiLattice};
-use rustc_smir::rustc_internal;
 use rustc_span::{DUMMY_SP, source_map::Spanned};
 use stable_mir::mir::{Body as StableBody, mono::Instance as StableInstance};
+use stable_mir::rustc_internal;
 use std::collections::HashSet;
 
 /// Main points-to analysis object.

kani-compiler/src/kani_middle/points_to/points_to_graph.rs

@@ -9,11 +9,11 @@ use rustc_middle::{
     ty::{Instance, List, TyCtxt},
 };
 use rustc_mir_dataflow::{JoinSemiLattice, fmt::DebugWithContext};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::{
     Place as StablePlace,
     mono::{Instance as StableInstance, StaticDef},
 };
+use stable_mir::rustc_internal;
 use std::collections::{HashMap, HashSet, VecDeque};
 
 /// A node in the points-to graph, which could be a place on the stack, a heap allocation, or a static.

kani-compiler/src/kani_middle/reachability.rs

@@ -23,14 +23,14 @@ use rustc_data_structures::fx::FxHashSet;
 use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
 use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_session::config::OutputType;
-use rustc_smir::rustc_internal;
 use stable_mir::CrateItem;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
 use stable_mir::mir::{
     Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator, TerminatorKind,
     visit::Location,
 };
+use stable_mir::rustc_internal;
 use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
 use stable_mir::{CrateDef, ItemKind};
 use std::fmt::{Display, Formatter};

kani-compiler/src/kani_middle/resolve.rs

@@ -18,8 +18,8 @@ use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalMo
 use rustc_hir::{ItemKind, UseKind};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::ty::fast_reject::{self, TreatParams};
-use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind};
 use std::collections::HashSet;
 use std::fmt;

kani-compiler/src/kani_middle/resolve/type_resolution.rs

@@ -6,9 +6,9 @@ use crate::kani_middle::resolve::{ResolveError, resolve_path, validate_kind};
 use quote::ToTokens;
 use rustc_hir::def::DefKind;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use rustc_span::def_id::LocalDefId;
 use stable_mir::mir::Mutability;
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FloatTy, IntTy, Region, RegionKind, RigidTy, Ty, UintTy};
 use std::str::FromStr;
 use strum_macros::{EnumString, IntoStaticStr};

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -13,10 +13,10 @@ use kani_metadata::HarnessMetadata;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Const;
 use rustc_middle::ty::{self, EarlyBinder, TyCtxt, TypeFoldable, TypingEnv};
-use rustc_smir::rustc_internal;
 use stable_mir::mir::ConstOperand;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
+use stable_mir::rustc_internal;
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
 use stable_mir::{CrateDef, CrateItem};
 

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

@@ -16,15 +16,15 @@ use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use fxhash::FxHashMap;
 use rustc_middle::ty::TyCtxt;
+use rustc_smir::IndexedVal;
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     AggregateKind, BasicBlockIdx, Body, Local, Mutability, Operand, Place, Rvalue, SwitchTargets,
     Terminator, TerminatorKind,
 };
 use stable_mir::ty::{
-    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, Ty, TyKind, UintTy,
-    VariantDef,
+    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind, UintTy, VariantDef,
 };
 use tracing::debug;
 

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs

@@ -13,7 +13,7 @@ use crate::kani_middle::transform::{
 };
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
+use stable_mir::rustc_internal;
 use stable_mir::{
     CrateDef,
     mir::{Body, Mutability, Place, mono::Instance},

kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs

@@ -5,10 +5,11 @@
 
 use std::fmt::Display;
 
+use rustc_smir::IndexedVal;
 use stable_mir::{
     abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape},
     target::{MachineInfo, MachineSize},
-    ty::{AdtKind, IndexedVal, RigidTy, Ty, TyKind, UintTy, VariantIdx},
+    ty::{AdtKind, RigidTy, Ty, TyKind, UintTy, VariantIdx},
 };
 
 /// Represents a chunk of data bytes in a data structure.

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

@@ -20,7 +20,7 @@ use crate::kani_middle::transform::body::{
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::{Const, TyCtxt};
-use rustc_smir::rustc_internal;
+use rustc_smir::IndexedVal;
 use stable_mir::CrateDef;
 use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange};
 use stable_mir::mir::mono::Instance;
@@ -30,8 +30,9 @@ use stable_mir::mir::{
     Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, Rvalue,
     Statement, StatementKind, Terminator, TerminatorKind,
 };
+use stable_mir::rustc_internal;
 use stable_mir::target::{MachineInfo, MachineSize};
-use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Span, Ty, TyKind, UintTy};
+use stable_mir::ty::{AdtKind, RigidTy, Span, Ty, TyKind, UintTy};
 use std::fmt::Debug;
 use strum_macros::AsRefStr;
 use tracing::{debug, trace};