diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 76e3952ae06..1ef23ac02c2 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -26,7 +26,8 @@ use rustc_codegen_ssa::back::archive::{ use rustc_codegen_ssa::back::link::link_binary; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CompiledModules, CrateInfo}; -use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; +use rustc_data_structures::fx::FxHashMap; +use rustc_data_structures::unord::UnordMap; use rustc_errors::ErrorGuaranteed; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; use rustc_metadata::EncodedMetadata; @@ -297,9 +298,8 @@ impl CodegenBackend for LlbcCodegenBackend { _sess: &Session, _filenames: &OutputFilenames, _crate_info: &CrateInfo, - ) -> (CompiledModules, FxIndexMap) { - match ongoing_codegen - .downcast::<(CompiledModules, FxIndexMap)>() + ) -> (CompiledModules, UnordMap) { + match ongoing_codegen.downcast::<(CompiledModules, UnordMap)>() { Ok(val) => *val, Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), @@ -378,7 +378,7 @@ fn contract_metadata_for_harness( /// itself and passes it to `codegen_crate` and `link`, so there is nothing crate-specific to report /// here. fn codegen_results() -> Box { - let work_products = FxIndexMap::::default(); + let work_products = UnordMap::::default(); Box::new((CompiledModules { modules: vec![], allocator_module: None }, work_products)) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 80368d7bdbd..6ca5ffa384f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -6,6 +6,7 @@ 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_public::CrateDefType; use rustc_public::mir::alloc::{AllocId, GlobalAlloc}; use rustc_public::mir::mono::{Instance, StaticDef}; use rustc_public::mir::{Mutability, Operand}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 5130905b13a..3384db9d027 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -246,7 +246,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { current_fn.instance().instantiate_mir_and_normalize_erasing_regions( self.tcx, ty::TypingEnv::fully_monomorphized(), - ty::EarlyBinder::bind(value), + ty::EarlyBinder::bind(self.tcx, value), ) } else { // TODO: confirm with rust team there is no way to monomorphize diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 0b1a138070c..5542f75f74e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -29,7 +29,8 @@ use rustc_codegen_ssa::back::archive::{ use rustc_codegen_ssa::back::link::link_binary; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CompiledModules, CrateInfo, TargetConfig}; -use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; +use rustc_data_structures::fx::FxHashMap; +use rustc_data_structures::unord::UnordMap; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; @@ -526,9 +527,8 @@ impl CodegenBackend for GotocCodegenBackend { _sess: &Session, _filenames: &OutputFilenames, _crate_info: &CrateInfo, - ) -> (CompiledModules, FxIndexMap) { - match ongoing_codegen - .downcast::<(CompiledModules, FxIndexMap)>() + ) -> (CompiledModules, UnordMap) { + match ongoing_codegen.downcast::<(CompiledModules, UnordMap)>() { Ok(val) => *val, Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), @@ -664,7 +664,7 @@ fn check_options(session: &Session) { /// itself and passes it to `codegen_crate` and `link`, so there is nothing crate-specific to report /// here. fn codegen_results() -> Box { - let work_products = FxIndexMap::::default(); + let work_products = UnordMap::::default(); Box::new((CompiledModules { modules: vec![], allocator_module: None }, work_products)) } diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs index 3583055076d..bc620634d36 100644 --- a/kani-compiler/src/kani_middle/abi.rs +++ b/kani-compiler/src/kani_middle/abi.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains code for handling type abi information. +use rustc_public::CrateDefType; use rustc_public::abi::{FieldsShape, LayoutShape}; use rustc_public::ty::{RigidTy, Ty, TyKind, UintTy}; use tracing::debug; diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index fa181272345..3242c1f8147 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -737,9 +737,9 @@ fn resolve_deferred_fn_slots<'tcx>( // ::Val for a choice that does not satisfy the bound); normalize here and // skip the choice on failure, rather than letting Instance::resolve ICE on it. let inputs = - rustc_middle::ty::EarlyBinder::bind(spec.inputs).instantiate(tcx, args_internal); + rustc_middle::ty::EarlyBinder::bind(tcx, spec.inputs).instantiate(tcx, args_internal); let output = - rustc_middle::ty::EarlyBinder::bind(spec.output).instantiate(tcx, args_internal); + rustc_middle::ty::EarlyBinder::bind(tcx, spec.output).instantiate(tcx, args_internal); let typing_env = rustc_middle::ty::TypingEnv::fully_monomorphized(); let Ok(inputs) = tcx.try_normalize_erasing_regions(typing_env, inputs) else { return false; diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 7a9058db7ce..5365a6b4fd6 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -18,6 +18,7 @@ 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_public::CrateDefType; use rustc_public::Symbol; use rustc_public::rustc_internal; use rustc_public::ty::{RigidTy, Ty as TyStable, TyKind}; diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 369a6c1c99f..f3376274697 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -17,7 +17,7 @@ use rustc_public::ty::{ TyKind, }; use rustc_public::visitor::{Visitable, Visitor as TyVisitor}; -use rustc_public::{CrateDef, DefId, local_crate}; +use rustc_public::{CrateDef, CrateDefType, DefId, local_crate}; use std::ops::ControlFlow; use self::attributes::KaniAttributes; diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index fb7ddfed6cb..187c5067aa1 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -184,7 +184,7 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul let old_ret_internal = rustc_internal::internal(tcx, old_ret_ty); let new_ret_internal = rustc_internal::internal(tcx, new_ret_ty); let new_ret_renamed = - EarlyBinder::bind(new_ret_internal).instantiate(tcx, rename_args).skip_normalization(); + EarlyBinder::bind(tcx, new_ret_internal).instantiate(tcx, rename_args).skip_normalization(); let mut diff = vec![]; // Error messages show the user's original types (before renaming) for clarity. @@ -196,8 +196,9 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul { let old_ty_internal = rustc_internal::internal(tcx, old_arg.ty); let new_ty_internal = rustc_internal::internal(tcx, new_arg.ty); - let new_renamed = - EarlyBinder::bind(new_ty_internal).instantiate(tcx, rename_args).skip_normalization(); + let new_renamed = EarlyBinder::bind(tcx, new_ty_internal) + .instantiate(tcx, rename_args) + .skip_normalization(); if old_ty_internal != new_renamed { diff.push(format!( "Expected type `{}` for parameter {}, but found `{}`", @@ -257,7 +258,7 @@ impl<'tcx> StubConstChecker<'tcx> { self.instance.instantiate_mir_and_normalize_erasing_regions( self.tcx, TypingEnv::fully_monomorphized(), - EarlyBinder::bind(value), + EarlyBinder::bind(self.tcx, value), ) } diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 763d3d9d681..83b27d7bf66 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -21,7 +21,6 @@ use crate::kani_middle::{ use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; use rustc_middle::ty::TyCtxt; -use rustc_public::CrateDef; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ AggregateKind, BasicBlock, BasicBlockIdx, BinOp, Body, BorrowKind, CastKind, ConstOperand, @@ -33,6 +32,7 @@ use rustc_public::ty::{ AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, MirConst, Region, RegionKind, RigidTy, Ty, TyConst, TyKind, UintTy, VariantDef, VariantIdx, }; +use rustc_public::{CrateDef, CrateDefType}; use rustc_public_bridge::IndexedVal; use tracing::debug; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index ca2e18f59b6..e4c2c6cf940 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -15,6 +15,7 @@ use crate::{ }, }, }; +use rustc_public::CrateDefType; use rustc_public::{ mir::{ AggregateKind, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index 7dba7cdc9f9..d2dc5217b40 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -5,6 +5,7 @@ use std::fmt::Display; +use rustc_public::CrateDefType; use rustc_public::{ abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape}, target::{MachineInfo, MachineSize}, diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index e4ad256dc53..56baa5e5d55 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -21,6 +21,7 @@ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::{Const, TyCtxt}; use rustc_public::CrateDef; +use rustc_public::CrateDefType; use rustc_public::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange}; use rustc_public::mir::mono::Instance; use rustc_public::mir::visit::{Location, PlaceContext, PlaceRef}; diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 1a798406ab0..f7cf38bcb24 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -561,7 +561,6 @@ impl RustcInternalMir for TerminatorKind { unwind: unwind.internal_mir(tcx), replace: false, drop: None, - async_fut: None, } } TerminatorKind::Call { func, args, destination, target, unwind } => { @@ -600,6 +599,9 @@ impl RustcInternalMir for Terminator { rustc_middle::mir::Terminator { source_info: rustc_middle::mir::SourceInfo::outermost(internal(tcx, self.span)), kind: self.kind.internal_mir(tcx), + // Terminators gained MIR-level attributes; the stable representation has no + // equivalent, and Kani-synthesized terminators carry none. + attributes: Default::default(), } } } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 44e2210371c..49fdeee7bf9 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -22,6 +22,7 @@ use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; +use rustc_public::CrateDefType; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ AggregateKind, BasicBlock, BinOp, Body, ConstOperand, Local, Mutability, Operand, Place, diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index b55d69b6fa8..51ae234d1db 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -60,7 +60,7 @@ fn build_missing_body(tcx: TyCtxt, instance: Instance) -> Body { let mono_body = internal_instance.instantiate_mir_and_normalize_erasing_regions( tcx, TypingEnv::fully_monomorphized(), - EarlyBinder::bind(internal_body), + EarlyBinder::bind(tcx, internal_body), ); rustc_internal::stable(&mono_body) } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index cb6649d4dbb..a2690c311ae 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2026-06-01" +channel = "nightly-2026-07-01" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs index 0e7061afa1d..c90deaf469f 100644 --- a/tools/scanner/src/analysis.rs +++ b/tools/scanner/src/analysis.rs @@ -8,6 +8,7 @@ use csv::WriterBuilder; use graph_cycles::Cycles; use petgraph::graph::Graph; use rustc_middle::ty::TyCtxt; +use rustc_public::CrateDefType; use rustc_public::mir::mono::Instance; use rustc_public::mir::visit::{Location, PlaceContext, PlaceRef}; use rustc_public::mir::{