From 46f2e3be02ce334d2283af381ab5de17f954ec29 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 25 Aug 2026 18:00:10 -0400 Subject: [PATCH 1/2] Upgrade Rust toolchain to nightly-2026-07-01 A much smaller upgrade than the previous two: no verification behaviour changed, and no test needed adjusting. **`FieldDef` moved to the `crate_def_with_ty!` macro.** Its inherent `ty()` and `ty_with_args()` are now provided by the `CrateDefType` trait, so the 17 call sites just need that trait in scope. This is a pure import change -- the semantics are identical (both still resolve to `def_ty`/`def_ty_with_args`). **`EarlyBinder::bind` takes the interner.** `bind(value)` becomes `bind(tcx, value)` at five sites. **`Terminator` gained MIR-level attributes** (`attributes: ThinVec`). The stable representation has no equivalent, and Kani-synthesized terminators carry none, so `internal_mir` passes an empty vector. **`TerminatorKind::Drop` lost `async_fut`**, so that field is dropped from the `internal_mir` conversion. **Work products are an `UnordMap`, not an `FxIndexMap`**, in `CodegenBackend::join_codegen`'s return type (both backends). Full regression run is clean on the first attempt: kani 607/607, cargo-kani 71/71, expected, script-based-pre 68/68, std-checks, cargo-ui, coverage, prusti, smack, kani-docs, json-handler, cargo-coverage, all unit tests, both `-D warnings` clippy gates, the `-D warnings` build, fmt, and the LLBC build. --- .../src/codegen_aeneas_llbc/compiler_interface.rs | 10 +++++----- .../src/codegen_cprover_gotoc/codegen/operand.rs | 1 + kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 2 +- .../src/codegen_cprover_gotoc/compiler_interface.rs | 10 +++++----- kani-compiler/src/kani_middle/abi.rs | 1 + kani-compiler/src/kani_middle/coercion.rs | 1 + kani-compiler/src/kani_middle/mod.rs | 2 +- kani-compiler/src/kani_middle/stubbing/mod.rs | 9 +++++---- kani-compiler/src/kani_middle/transform/automatic.rs | 2 +- .../check_uninit/ptr_uninit/uninit_visitor.rs | 1 + .../kani_middle/transform/check_uninit/ty_layout.rs | 1 + .../src/kani_middle/transform/check_values.rs | 1 + .../src/kani_middle/transform/internal_mir.rs | 4 +++- .../src/kani_middle/transform/kani_intrinsics.rs | 1 + kani-compiler/src/kani_middle/transform/mod.rs | 2 +- rust-toolchain.toml | 2 +- tools/scanner/src/analysis.rs | 1 + 17 files changed, 31 insertions(+), 20 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 76e3952ae06d..1ef23ac02c22 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 80368d7bdbd3..6ca5ffa384f8 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 5130905b13a9..3384db9d0276 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 0b1a138070cc..5542f75f74e8 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 3583055076dc..bc620634d363 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/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 7a9058db7cea..5365a6b4fd68 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 369a6c1c99fd..f33762746971 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 fb7ddfed6cbe..187c5067aa18 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 78f76ca6da60..d0eed1e2b5d0 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 ca2e18f59b61..e4c2c6cf9406 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 7dba7cdc9f9a..d2dc5217b400 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 e4ad256dc530..56baa5e5d55c 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 1a798406ab0d..f7cf38bcb247 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 44e2210371c2..49fdeee7bf96 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 b55d69b6fa86..51ae234d1dbd 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 cb6649d4dbba..a2690c311ae3 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 0e7061afa1da..c90deaf469fb 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::{ From 0d6c59cdfb52433d7be4c216d6e90ba1ea545a70 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 27 Aug 2026 11:40:06 -0400 Subject: [PATCH 2/2] Pass the interner to EarlyBinder::bind in the Fn-bound spec code `EarlyBinder::bind` takes the interner as of nightly-2026-07-01. The Fn-bounded generic instantiation added by #4726 landed on main after this branch was written, so its two `bind` call sites still used the old one-argument form and failed to compile against the new toolchain. --- kani-compiler/src/kani_middle/codegen_units.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index fa181272345b..3242c1f8147e 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;