Upgrade Rust toolchain to 2025-07-21

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -33,12 +33,12 @@ use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
+use rustc_public::mir::mono::{Instance, MonoItem};
+use rustc_public::rustc_internal;
+use rustc_public::{CrateDef, DefId};
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
-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;
 use std::path::Path;
@@ -253,8 +253,8 @@ impl CodegenBackend for LlbcCodegenBackend {
                 ReachabilityType::PubFns => {
                     let unit = CodegenUnit::default();
                     let transformer = BodyTransformation::new(&queries, tcx, &unit);
-                    let main_instance =
-                        stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap());
+                    let main_instance = rustc_public::entry_fn()
+                        .map(|main_fn| Instance::try_from(main_fn).unwrap());
                     let local_reachable = filter_crate_items(tcx, |_, instance| {
                         let def_id = rustc_internal::internal(tcx, instance.def.def_id());
                         Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id)

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

@@ -56,19 +56,19 @@ use charon_lib::{error_assert, error_or_panic};
 use core::panic;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::{TyCtxt, TypingEnv};
-use stable_mir::mir::mono::{Instance, InstanceDef};
-use stable_mir::mir::{
+use rustc_public::mir::mono::{Instance, InstanceDef};
+use rustc_public::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::{
+use rustc_public::rustc_internal;
+use rustc_public::ty::{
     AdtDef, AdtKind, Allocation, ConstantKind, FnDef, GenericArgKind, GenericArgs,
     GenericParamDefKind, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl, TraitDef,
     Ty, TyConst, TyConstKind, TyKind, UintTy,
 };
-use stable_mir::{CrateDef, CrateDefType, DefId};
+use rustc_public::{CrateDef, CrateDefType, DefId};
 use std::collections::HashMap;
 use std::iter::zip;
 use std::path::PathBuf;

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

@@ -22,8 +22,8 @@ use super::source_region::SourceRegion;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::InternedString;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
-use stable_mir::mir::{Place, ProjectionElem};
-use stable_mir::ty::{Span as SpanStable, Ty};
+use rustc_public::mir::{Place, ProjectionElem};
+use rustc_public::ty::{Span as SpanStable, Ty};
 use strum_macros::{AsRefStr, EnumString};
 use tracing::debug;
 

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

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use stable_mir::mir::{BasicBlock, BasicBlockIdx, Body};
+use rustc_public::mir::{BasicBlock, BasicBlockIdx, Body};
 use std::collections::HashSet;
 use tracing::debug;
 

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

@@ -6,11 +6,11 @@ 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 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};
+use rustc_public::CrateDef;
+use rustc_public::mir::mono::{Instance, MonoItem};
+use rustc_public::mir::{Local, VarDebugInfoContents};
+use rustc_public::rustc_internal;
+use rustc_public::ty::{FnDef, RigidTy, TyKind};
 
 impl GotocCtx<'_> {
     /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,

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

@@ -15,11 +15,11 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::{InternString, InternedString};
 use lazy_static::lazy_static;
-use stable_mir::CrateDef;
-use stable_mir::abi::{CallConvention, PassMode};
-use stable_mir::mir::Place;
-use stable_mir::mir::mono::Instance;
-use stable_mir::ty::{RigidTy, TyKind};
+use rustc_public::CrateDef;
+use rustc_public::abi::{CallConvention, PassMode};
+use rustc_public::mir::Place;
+use rustc_public::mir::mono::Instance;
+use rustc_public::ty::{RigidTy, TyKind};
 use tracing::{debug, trace};
 
 lazy_static! {

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

@@ -8,10 +8,10 @@ use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
 use cbmc::InternString;
 use cbmc::InternedString;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
-use stable_mir::CrateDef;
-use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Body, Local};
-use stable_mir::ty::{RigidTy, TyKind};
+use rustc_public::CrateDef;
+use rustc_public::mir::mono::Instance;
+use rustc_public::mir::{Body, Local};
+use rustc_public::ty::{RigidTy, TyKind};
 use std::collections::BTreeMap;
 use tracing::{debug, debug_span};
 
@@ -235,17 +235,17 @@ impl GotocCtx<'_> {
     }
 }
 
-pub mod rustc_smir {
+pub mod rustc_public_bridge {
     use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region};
-    use crate::stable_mir::CrateDef;
+    use crate::rustc_public::CrateDef;
     use rustc_middle::mir::coverage::BasicCoverageBlock;
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::ty::TyCtxt;
-    use stable_mir::mir::mono::Instance;
-    use stable_mir::rustc_internal;
-    use stable_mir::{Filename, Opaque};
+    use rustc_public::mir::mono::Instance;
+    use rustc_public::rustc_internal;
+    use rustc_public::{Filename, Opaque};
 
-    type CoverageOpaque = stable_mir::Opaque;
+    type CoverageOpaque = rustc_public::Opaque;
 
     /// Retrieves the `SourceRegion` associated with the data in a
     /// `CoverageOpaque` object.

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

@@ -10,10 +10,10 @@ 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 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 rustc_public::mir::mono::Instance;
+use rustc_public::mir::{BasicBlockIdx, Operand, Place};
+use rustc_public::rustc_internal;
+use rustc_public::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 
 pub struct SizeAlign {

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

@@ -6,16 +6,16 @@ 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_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::{
+use rustc_public::mir::alloc::{AllocId, GlobalAlloc};
+use rustc_public::mir::mono::{Instance, StaticDef};
+use rustc_public::mir::{Mutability, Operand};
+use rustc_public::rustc_internal;
+use rustc_public::ty::{
     Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty,
     TyConst, TyConstKind, TyKind, UintTy,
 };
-use stable_mir::{CrateDef, CrateItem};
+use rustc_public::{CrateDef, CrateItem};
+use rustc_span::Span as SpanInternal;
 use tracing::{debug, trace};
 
 #[derive(Clone, Debug)]

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

@@ -14,9 +14,9 @@ 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 stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
-use stable_mir::rustc_internal;
-use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
+use rustc_public::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
+use rustc_public::rustc_internal;
+use rustc_public::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
 use tracing::{debug, trace, warn};
 
 /// A projection in Kani can either be to a type (the normal case),

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

@@ -20,13 +20,13 @@ 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 stable_mir::abi::{Primitive, Scalar, ValueAbi};
-use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{
+use rustc_public::abi::{Primitive, Scalar, ValueAbi};
+use rustc_public::mir::mono::Instance;
+use rustc_public::mir::{
     AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
 };
-use stable_mir::rustc_internal;
-use stable_mir::ty::{
+use rustc_public::rustc_internal;
+use rustc_public::ty::{
     Binder, ClosureKind, ExistentialPredicate, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy,
     VariantIdx,
 };

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

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

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

@@ -3,7 +3,7 @@
 use super::typ::FN_RETURN_VOID_VAR_NAME;
 use super::typ::TypeExt;
 use super::{PropertyClass, bb_label};
-use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque;
+use crate::codegen_cprover_gotoc::codegen::function::rustc_public_bridge::region_from_coverage_opaque;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::ExprValue;
@@ -12,15 +12,15 @@ use rustc_abi::Size;
 use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{List, TypingEnv};
-use stable_mir::CrateDef;
-use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
-use stable_mir::mir::mono::{Instance, InstanceKind};
-use stable_mir::mir::{
+use rustc_public::CrateDef;
+use rustc_public::abi::{ArgAbi, FnAbi, PassMode};
+use rustc_public::mir::mono::{Instance, InstanceKind};
+use rustc_public::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 rustc_public::rustc_internal;
+use rustc_public::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
 use tracing::{debug, debug_span, trace};
 
 impl GotocCtx<'_> {

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

@@ -5,8 +5,8 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::is_interior_mut;
-use stable_mir::CrateDef;
-use stable_mir::mir::mono::{Instance, StaticDef};
+use rustc_public::CrateDef;
+use rustc_public::mir::mono::{Instance, StaticDef};
 use tracing::debug;
 
 impl GotocCtx<'_> {

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

@@ -10,10 +10,10 @@ 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 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};
+use rustc_public::mir::mono::Instance;
+use rustc_public::mir::{Local, Operand, Place, Rvalue};
+use rustc_public::rustc_internal;
+use rustc_public::ty::{FnSig, RigidTy, Ty, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {
     pub fn place_ty_stable(&self, place: &Place) -> Ty {

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

@@ -20,15 +20,15 @@ use rustc_middle::ty::{
 };
 use rustc_middle::ty::{ExistentialTraitRef, GenericArgsRef};
 use rustc_middle::ty::{List, TypeFoldable};
-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::{
+use rustc_public::abi::{ArgAbi, FnAbi, PassMode};
+use rustc_public::mir::Body;
+use rustc_public::mir::mono::Instance as InstanceStable;
+use rustc_public::rustc_internal;
+use rustc_public::ty::{
     Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
     Ty as StableTy,
 };
+use rustc_span::def_id::DefId;
 use tracing::{debug, trace, warn};
 
 /// Map the unit type to an empty struct
@@ -304,7 +304,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let rigid =
             RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }, DynKind::Dyn);
 
-        stable_mir::ty::Ty::from_rigid_kind(rigid)
+        rustc_public::ty::Ty::from_rigid_kind(rigid)
     }
 
     /// Generates the type for a single field for a dynamic vtable.

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -34,14 +34,14 @@ use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
+use rustc_public::CrateDef;
+use rustc_public::mir::mono::{Instance, MonoItem};
+use rustc_public::rustc_internal;
 use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 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;
@@ -300,8 +300,8 @@ impl CodegenBackend for GotocCodegenBackend {
             if queries.args().reachability_analysis != ReachabilityType::None
                 && queries.kani_functions().is_empty()
             {
-                if stable_mir::find_crates("std").is_empty()
-                    && stable_mir::find_crates("kani").is_empty()
+                if rustc_public::find_crates("std").is_empty()
+                    && rustc_public::find_crates("kani").is_empty()
                 {
                     // Special error for when not importing kani and using #[no_std].
                     // See here for more info: https://github.com/model-checking/kani/issues/3906#issuecomment-2932687768.
@@ -369,8 +369,8 @@ impl CodegenBackend for GotocCodegenBackend {
                 ReachabilityType::PubFns => {
                     let unit = CodegenUnit::default();
                     let transformer = BodyTransformation::new(&queries, tcx, &unit);
-                    let main_instance =
-                        stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap());
+                    let main_instance = rustc_public::entry_fn()
+                        .map(|main_fn| Instance::try_from(main_fn).unwrap());
                     let local_reachable = filter_crate_items(tcx, |_, instance| {
                         let def_id = rustc_internal::internal(tcx, instance.def.def_id());
                         Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id)

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 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 rustc_public::CrateDef;
+use rustc_public::mir::mono::Instance;
+use rustc_public::mir::{Body, Local, LocalDecl, Rvalue, visit::Location, visit::MirVisitor};
+use rustc_public::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/context/goto_ctx.rs

@@ -35,12 +35,12 @@ use rustc_middle::ty::layout::{
     LayoutOfHelpers, TyAndLayout,
 };
 use rustc_middle::ty::{self, Ty, TyCtxt};
+use rustc_public::mir::Body;
+use rustc_public::mir::mono::Instance;
+use rustc_public::ty::Allocation;
 use rustc_span::Span;
 use rustc_span::source_map::respan;
 use rustc_target::callconv::FnAbi;
-use stable_mir::mir::Body;
-use stable_mir::mir::mono::Instance;
-use stable_mir::ty::Allocation;
 use std::collections::{BTreeMap, HashSet};
 use std::fmt::Debug;