Skip to content

Commit c45c8e8

Browse files
committed
Upgrade Rust toolchain to 2025-07-15
Relevant upstream PR: - rust-lang/rust#143848 (Rename `stable_mir` and `rustc_smir`) The update was done via ``` git grep -l 'stable_mir::' | xargs sed -i 's/stable_mir::/rustc_public::/' git grep -l 'rustc_smir::' | xargs sed -i 's/rustc_smir::/rustc_public_bridge::/' ``` followed by manual touch-ups in `kani-compiler/src/main.rs`, `kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs`, `tools/scanner/src/lib.rs`, and then running `scripts/kani-fmt.sh`. Resolves: #4229
1 parent 4058625 commit c45c8e8

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

65 files changed

+251
-251
lines changed

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -33,12 +33,12 @@ use rustc_metadata::EncodedMetadata;
3333
use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
3434
use rustc_middle::ty::TyCtxt;
3535
use rustc_middle::util::Providers;
36+
use rustc_public::mir::mono::{Instance, MonoItem};
37+
use rustc_public::rustc_internal;
38+
use rustc_public::{CrateDef, DefId};
3639
use rustc_session::Session;
3740
use rustc_session::config::{CrateType, OutputFilenames, OutputType};
3841
use rustc_session::output::out_filename;
39-
use stable_mir::mir::mono::{Instance, MonoItem};
40-
use stable_mir::rustc_internal;
41-
use stable_mir::{CrateDef, DefId};
4242
use std::any::Any;
4343
use std::fs::File;
4444
use std::path::Path;
@@ -253,8 +253,8 @@ impl CodegenBackend for LlbcCodegenBackend {
253253
ReachabilityType::PubFns => {
254254
let unit = CodegenUnit::default();
255255
let transformer = BodyTransformation::new(&queries, tcx, &unit);
256-
let main_instance =
257-
stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap());
256+
let main_instance = rustc_public::entry_fn()
257+
.map(|main_fn| Instance::try_from(main_fn).unwrap());
258258
let local_reachable = filter_crate_items(tcx, |_, instance| {
259259
let def_id = rustc_internal::internal(tcx, instance.def.def_id());
260260
Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id)

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -56,19 +56,19 @@ use charon_lib::{error_assert, error_or_panic};
5656
use core::panic;
5757
use rustc_data_structures::fx::FxHashMap;
5858
use rustc_middle::ty::{TyCtxt, TypingEnv};
59-
use stable_mir::mir::mono::{Instance, InstanceDef};
60-
use stable_mir::mir::{
59+
use rustc_public::mir::mono::{Instance, InstanceDef};
60+
use rustc_public::mir::{
6161
AggregateKind, BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability,
6262
Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator,
6363
TerminatorKind, UnOp, VarDebugInfoContents,
6464
};
65-
use stable_mir::rustc_internal;
66-
use stable_mir::ty::{
65+
use rustc_public::rustc_internal;
66+
use rustc_public::ty::{
6767
AdtDef, AdtKind, Allocation, ConstantKind, FnDef, GenericArgKind, GenericArgs,
6868
GenericParamDefKind, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl, TraitDef,
6969
Ty, TyConst, TyConstKind, TyKind, UintTy,
7070
};
71-
use stable_mir::{CrateDef, CrateDefType, DefId};
71+
use rustc_public::{CrateDef, CrateDefType, DefId};
7272
use std::collections::HashMap;
7373
use std::iter::zip;
7474
use std::path::PathBuf;

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ use super::source_region::SourceRegion;
2222
use crate::codegen_cprover_gotoc::GotocCtx;
2323
use cbmc::InternedString;
2424
use cbmc::goto_program::{Expr, Location, Stmt, Type};
25-
use stable_mir::mir::{Place, ProjectionElem};
26-
use stable_mir::ty::{Span as SpanStable, Ty};
25+
use rustc_public::mir::{Place, ProjectionElem};
26+
use rustc_public::ty::{Span as SpanStable, Ty};
2727
use strum_macros::{AsRefStr, EnumString};
2828
use tracing::debug;
2929

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
use crate::codegen_cprover_gotoc::GotocCtx;
5-
use stable_mir::mir::{BasicBlock, BasicBlockIdx, Body};
5+
use rustc_public::mir::{BasicBlock, BasicBlockIdx, Body};
66
use std::collections::HashSet;
77
use tracing::debug;
88

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,11 @@ use cbmc::goto_program::FunctionContract;
66
use cbmc::goto_program::{Expr, Lambda, Location, Type};
77
use kani_metadata::AssignsContract;
88
use rustc_hir::def_id::DefId as InternalDefId;
9-
use stable_mir::CrateDef;
10-
use stable_mir::mir::mono::{Instance, MonoItem};
11-
use stable_mir::mir::{Local, VarDebugInfoContents};
12-
use stable_mir::rustc_internal;
13-
use stable_mir::ty::{FnDef, RigidTy, TyKind};
9+
use rustc_public::CrateDef;
10+
use rustc_public::mir::mono::{Instance, MonoItem};
11+
use rustc_public::mir::{Local, VarDebugInfoContents};
12+
use rustc_public::rustc_internal;
13+
use rustc_public::ty::{FnDef, RigidTy, TyKind};
1414

1515
impl GotocCtx<'_> {
1616
/// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,11 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
1515
use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
1616
use cbmc::{InternString, InternedString};
1717
use lazy_static::lazy_static;
18-
use stable_mir::CrateDef;
19-
use stable_mir::abi::{CallConvention, PassMode};
20-
use stable_mir::mir::Place;
21-
use stable_mir::mir::mono::Instance;
22-
use stable_mir::ty::{RigidTy, TyKind};
18+
use rustc_public::CrateDef;
19+
use rustc_public::abi::{CallConvention, PassMode};
20+
use rustc_public::mir::Place;
21+
use rustc_public::mir::mono::Instance;
22+
use rustc_public::ty::{RigidTy, TyKind};
2323
use tracing::{debug, trace};
2424

2525
lazy_static! {

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@ use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
88
use cbmc::InternString;
99
use cbmc::InternedString;
1010
use cbmc::goto_program::{Expr, Stmt, Symbol};
11-
use stable_mir::CrateDef;
12-
use stable_mir::mir::mono::Instance;
13-
use stable_mir::mir::{Body, Local};
14-
use stable_mir::ty::{RigidTy, TyKind};
11+
use rustc_public::CrateDef;
12+
use rustc_public::mir::mono::Instance;
13+
use rustc_public::mir::{Body, Local};
14+
use rustc_public::ty::{RigidTy, TyKind};
1515
use std::collections::BTreeMap;
1616
use tracing::{debug, debug_span};
1717

@@ -235,17 +235,17 @@ impl GotocCtx<'_> {
235235
}
236236
}
237237

238-
pub mod rustc_smir {
238+
pub mod rustc_public_bridge {
239239
use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region};
240-
use crate::stable_mir::CrateDef;
240+
use crate::rustc_public::CrateDef;
241241
use rustc_middle::mir::coverage::BasicCoverageBlock;
242242
use rustc_middle::mir::coverage::MappingKind::Code;
243243
use rustc_middle::ty::TyCtxt;
244-
use stable_mir::mir::mono::Instance;
245-
use stable_mir::rustc_internal;
246-
use stable_mir::{Filename, Opaque};
244+
use rustc_public::mir::mono::Instance;
245+
use rustc_public::rustc_internal;
246+
use rustc_public::{Filename, Opaque};
247247

248-
type CoverageOpaque = stable_mir::Opaque;
248+
type CoverageOpaque = rustc_public::Opaque;
249249

250250
/// Retrieves the `SourceRegion` associated with the data in a
251251
/// `CoverageOpaque` object.

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
1010
use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type};
1111
use rustc_middle::ty::TypingEnv;
1212
use rustc_middle::ty::layout::ValidityRequirement;
13-
use stable_mir::mir::mono::Instance;
14-
use stable_mir::mir::{BasicBlockIdx, Operand, Place};
15-
use stable_mir::rustc_internal;
16-
use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
13+
use rustc_public::mir::mono::Instance;
14+
use rustc_public::mir::{BasicBlockIdx, Operand, Place};
15+
use rustc_public::rustc_internal;
16+
use rustc_public::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
1717
use tracing::debug;
1818

1919
pub struct SizeAlign {

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,16 @@ use crate::kani_middle::is_anon_static;
66
use crate::unwrap_or_return_codegen_unimplemented;
77
use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type};
88
use rustc_middle::ty::Const as ConstInternal;
9-
use rustc_span::Span as SpanInternal;
10-
use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
11-
use stable_mir::mir::mono::{Instance, StaticDef};
12-
use stable_mir::mir::{Mutability, Operand};
13-
use stable_mir::rustc_internal;
14-
use stable_mir::ty::{
9+
use rustc_public::mir::alloc::{AllocId, GlobalAlloc};
10+
use rustc_public::mir::mono::{Instance, StaticDef};
11+
use rustc_public::mir::{Mutability, Operand};
12+
use rustc_public::rustc_internal;
13+
use rustc_public::ty::{
1514
Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty,
1615
TyConst, TyConstKind, TyKind, UintTy,
1716
};
18-
use stable_mir::{CrateDef, CrateItem};
17+
use rustc_public::{CrateDef, CrateItem};
18+
use rustc_span::Span as SpanInternal;
1919
use tracing::{debug, trace};
2020

2121
#[derive(Clone, Debug)]

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@ use crate::unwrap_or_return_codegen_unimplemented;
1414
use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type};
1515
use rustc_abi::{TagEncoding, Variants};
1616
use rustc_middle::ty::layout::LayoutOf;
17-
use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
18-
use stable_mir::rustc_internal;
19-
use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
17+
use rustc_public::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
18+
use rustc_public::rustc_internal;
19+
use rustc_public::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
2020
use tracing::{debug, trace, warn};
2121

2222
/// A projection in Kani can either be to a type (the normal case),

0 commit comments

Comments
 (0)