Upgrade Rust toolchain to 2025-07-10 (#4215)

Update the import path for stable-mir's rustc_internal, IndexVal, and
run_with_ctx.
rust-lang/rust@da25619e2a.

Resolves #4214
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: thanhnguyen-aws

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};