Update toolchain to nightly-2026-09-22

.cargo/config.toml

@@ -35,3 +35,12 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
     "-Aclippy::needless-borrow",
     "-Aclippy::bool-to-int-with-if",
 ]
+
+# Doctests are compiled by rustdoc, not through Kani's driver, so they miss the
+# `-Znext-solver=coherence` that `base_rustc_flags` passes to every crate Kani compiles.
+# `kani::pointer_generator`'s return type uses `generic_const_exprs`, which the
+# next-generation trait solver (on by default since nightly-2026-09-22) cannot handle, so the
+# doctests that call it need the same setting.
+# Tracked for removal in https://github.com/model-checking/kani/issues/4832.
+[build]
+rustdocflags = ["-Znext-solver=coherence"]

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -38,9 +38,10 @@ use rustc_public::mir::mono::{Instance, MonoItem};
 use rustc_public::rustc_internal;
 use rustc_public::ty::FnDef;
 use rustc_public::{CrateDef, DefId};
-use rustc_session::config::{CrateType, OutputFilenames, OutputType};
+use rustc_session::config::{OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 use rustc_session::{IncrCompSession, Session};
+use rustc_structures::CrateType;
 use std::any::Any;
 use std::fs::File;
 use std::path::Path;

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

@@ -297,7 +297,7 @@ pub mod rustc_public_bridge {
         let filename = rustc_internal::stable(body.span).get_filename();
         // Some functions, like `std` ones, may not have coverage info attached
         // to them because they have been compiled without coverage flags.
-        if let Some(cov_info) = &body.function_coverage_info {
+        if let Some(cov_info) = &body.coverage_mir_info {
             // Iterate over the coverage mappings and match with the coverage term.
             let mut source_regions: Vec<SourceRegion> = Vec::new();
             for mapping in &cov_info.mappings {

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

@@ -10,7 +10,6 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type;
 use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
-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;
@@ -681,8 +680,22 @@ impl GotocCtx<'_, '_> {
     ///   and we need to take it's address and build the fat pointer.
     pub fn codegen_place_ref_stable(&mut self, place: &Place, loc: Location) -> Expr {
         let place_ty = self.place_ty_stable(place);
-        let projection =
-            unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place, loc));
+        let projection = match self.codegen_place_stable(place, loc) {
+            Ok(projection) => projection,
+            Err(err) => {
+                // This function yields a *reference* to the place, so the stub that replaces an
+                // unsupported projection has to have the reference's type (thin or fat), not the
+                // place's own. `unwrap_or_return_codegen_unimplemented!` would return the latter
+                // and the caller would then assign a value to a pointer-typed local.
+                let ref_ty = self.codegen_ty_ref_stable(place_ty);
+                return self.codegen_unimplemented_expr(
+                    err.operation.as_str(),
+                    ref_ty,
+                    err.loc,
+                    err.bug_url.as_str(),
+                );
+            }
+        };
         if self.use_thin_pointer_stable(place_ty) {
             // For ZST objects rustc does not necessarily generate any actual objects.
             let need_not_be_an_object = self.is_zst_object(&projection.goto_expr);

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

@@ -20,7 +20,7 @@ use cbmc::{InternString, InternedString, btree_string_map};
 use num::bigint::BigInt;
 use rustc_abi::{FieldsShape, TagEncoding, Variants};
 use rustc_middle::ty::{TyCtxt, VtblEntry};
-use rustc_public::abi::{Primitive, Scalar, ValueAbi};
+use rustc_public::abi::{Primitive, Scalar, ValueRepr};
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{
     AggregateKind, BinOp, CastKind, Operand, Place, PointerCoercion, Rvalue, UnOp,
@@ -1848,8 +1848,8 @@ impl GotocCtx<'_, '_> {
                 // }
                 // ```
                 let res_typ = self.codegen_ty_stable(res_ty);
-                let ValueAbi::Scalar(Scalar::Initialized { value, valid_range }) =
-                    res_ty.layout().unwrap().shape().abi
+                let ValueRepr::Scalar(Scalar::Initialized { value, valid_range }) =
+                    res_ty.layout().unwrap().shape().value_repr
                 else {
                     unreachable!("Unexpected layout")
                 };

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

@@ -938,7 +938,12 @@ impl GotocCtx<'_, '_> {
         fargs[0] = if self_ty.kind().is_adt() {
             // Generate a temp variable and assign its inner pointer to the fat_ptr.data.
             match fn_ptr.typ() {
-                Type::Pointer { typ: box Type::Code { parameters, .. } } => {
+                // `box` patterns were removed in nightly-2026-09-22, so match the pointer and
+                // then look through it.
+                Type::Pointer { typ } => {
+                    let Type::Code { parameters, .. } = typ.as_ref() else {
+                        unreachable!("Unexpected virtual function type: {:?}", fn_ptr.typ())
+                    };
                     let param_typ = parameters.first().unwrap().typ();
                     let (tmp, decl) = self.decl_temp_variable(param_typ.clone(), None, loc);
                     debug!(?tmp,

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

@@ -1554,6 +1554,10 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
             Float::F32 => self.tcx.types.f32,
             Float::F64 => self.tcx.types.f64,
             Float::F128 => self.tcx.types.f128,
+            // `f16b` (bfloat16) is a library type rather than a primitive, so there is no
+            // `tcx.types` entry for it, and CBMC has no bfloat16 type either. rustc itself
+            // declines to map this primitive back to a Rust type (`rustc_abi::layout::ty`).
+            Float::F16B => unimplemented!("bfloat16 (`f16b`) is not supported by Kani"),
         }
     }
 

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -40,10 +40,11 @@ use rustc_public::CrateDef;
 use rustc_public::mir::mono::{Instance, MonoItem};
 use rustc_public::rustc_internal;
 use rustc_public::ty::FnDef;
-use rustc_session::config::{CrateType, OutputFilenames, OutputType};
+use rustc_session::config::{OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
-use rustc_session::{IncrCompSession, Session};
+use rustc_session::{EarlySession, IncrCompSession, Session};
 use rustc_span::{Symbol, sym};
+use rustc_structures::CrateType;
 use rustc_target::spec::{Arch, Os, PanicStrategy};
 use std::any::Any;
 use std::cmp::min;
@@ -293,7 +294,7 @@ impl CodegenBackend for GotocCodegenBackend {
         "kani-cprover"
     }
 
-    fn target_config(&self, sess: &Session) -> TargetConfig {
+    fn target_config(&self, sess: &EarlySession) -> TargetConfig {
         // This code is adapted from the cranelift backend:
         // https://github.com/rust-lang/rust/blob/a124fb3cb7291d75872934f411d81fe298379ace/compiler/rustc_codegen_cranelift/src/lib.rs#L184
         let target_features = if sess.target.arch == Arch::X86_64 && sess.target.os != Os::None {
@@ -320,6 +321,8 @@ impl CodegenBackend for GotocCodegenBackend {
             internal_target_features: UnordSet::from_iter(target_features),
             has_reliable_f16,
             has_reliable_f16_math: has_reliable_f16,
+            // CBMC has no bfloat16 type, so `f16b` is not supported.
+            has_reliable_f16b: false,
             has_reliable_f128,
             has_reliable_f128_math: has_reliable_f128,
         }

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -29,7 +29,6 @@ use cbmc::utils::aggr_tag;
 use cbmc::{InternedString, MachineModel};
 use rustc_abi::{HasDataLayout, TargetDataLayout};
 use rustc_data_structures::fx::FxHashMap;
-use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
     FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasTyCtxt, HasTypingEnv, LayoutError,
     LayoutOfHelpers, TyAndLayout,
@@ -40,6 +39,7 @@ use rustc_public::mir::mono::Instance;
 use rustc_public::ty::Allocation;
 use rustc_span::Span;
 use rustc_span::respan;
+use rustc_span::span_bug;
 use rustc_target::callconv::FnAbi;
 use std::collections::{BTreeMap, HashMap, HashSet};
 use std::fmt::Debug;

kani-compiler/src/kani_middle/attributes.rs

@@ -518,7 +518,7 @@ impl<'tcx> KaniAttributes<'tcx> {
             )
             .with_note(format!("see issue {} for more information", unstable_attr.issue))
             .with_help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
-            .emit()
+            .emit_err()
     }
 
     /// Is this item a harness? (either `proof` or `proof_for_contract`
@@ -1149,7 +1149,7 @@ impl UnstableAttrParseError<'_> {
                 "expected format: #[kani::unstable_feature({}, {}, {})]",
                 r#"feature="<IDENTIFIER>""#, r#"issue="<ISSUE>""#, r#"reason="<DESCRIPTION>""#
             ))
-            .emit()
+            .emit_err()
     }
 }
 

kani-compiler/src/kani_middle/points_to/points_to_graph.rs

@@ -154,7 +154,11 @@ impl<'tcx> PointsToGraph<'tcx> {
             HashSet::from([MemLoc::new_stack_allocation(instance, place_without_projections)]);
         for projection in place.projection {
             match projection {
-                ProjectionElem::Deref => {
+                // A `PhantomDeref` is the borrow checker's symbolic dereference of a
+                // `Reborrow` type (rust-lang/rust#159103). Treat it as a dereference: it
+                // reaches an indirect place, so following the pointer keeps the aliasing
+                // information conservative.
+                ProjectionElem::Deref | ProjectionElem::PhantomDeref => {
                     node_set = self.successors(&node_set);
                 }
                 ProjectionElem::Field(..)

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -12,7 +12,6 @@ use tracing::{debug, trace};
 use kani_metadata::HarnessMetadata;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Const;
-use rustc_middle::ty::RegionExt;
 use rustc_middle::ty::{self, EarlyBinder, TyCtxt, TypeFoldable, TypingEnv};
 use rustc_public::mir::ConstOperand;
 use rustc_public::mir::mono::Instance;

kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs

@@ -7,7 +7,7 @@ use std::fmt::Display;
 
 use rustc_public::CrateDefType;
 use rustc_public::{
-    abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape},
+    abi::{FieldsShape, Scalar, TagEncoding, ValueRepr, VariantsShape},
     target::{MachineInfo, MachineSize},
     ty::{AdtKind, RigidTy, Ty, TyKind, UintTy, VariantIdx},
 };
@@ -184,11 +184,11 @@ fn data_bytes_for_ty(
     let layout = ty.layout().unwrap().shape();
 
     match layout.fields {
-        FieldsShape::Primitive => Ok(vec![match layout.abi {
-            ValueAbi::Scalar(Scalar::Initialized { value, .. }) => {
+        FieldsShape::Primitive => Ok(vec![match layout.value_repr {
+            ValueRepr::Scalar(Scalar::Initialized { value, .. }) => {
                 DataBytes { offset: current_offset, size: value.size(machine_info) }
             }
-            _ => unreachable!("FieldsShape::Primitive with a different ABI than ValueAbi::Scalar"),
+            _ => unreachable!("FieldsShape::Primitive with a different ABI than ValueRepr::Scalar"),
         }]),
         FieldsShape::Array { stride, count } if count > 0 => {
             let TyKind::RigidTy(RigidTy::Array(elem_ty, _)) = ty.kind() else { unreachable!() };
@@ -358,12 +358,12 @@ fn data_bytes_for_ty(
                 RigidTy::Str | RigidTy::Slice(_) | RigidTy::Array(_, _) => {
                     unreachable!("Expected array layout for {ty:?}")
                 }
-                RigidTy::RawPtr(_, _) | RigidTy::Ref(_, _, _) => Ok(match layout.abi {
-                    ValueAbi::Scalar(Scalar::Initialized { value, .. }) => {
+                RigidTy::RawPtr(_, _) | RigidTy::Ref(_, _, _) => Ok(match layout.value_repr {
+                    ValueRepr::Scalar(Scalar::Initialized { value, .. }) => {
                         // Thin pointer, ABI is a single scalar.
                         vec![DataBytes { offset: current_offset, size: value.size(machine_info) }]
                     }
-                    ValueAbi::ScalarPair {
+                    ValueRepr::ScalarPair {
                         a: Scalar::Initialized { value: value_first, .. },
                         b: Scalar::Initialized { value: value_second, .. },
                         ..

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -22,7 +22,9 @@ 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::abi::{
+    FieldsShape, Scalar, TagEncoding, ValueRepr, VariantsShape, WrappingRange,
+};
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::visit::{Location, PlaceContext, PlaceRef};
 use rustc_public::mir::{
@@ -186,7 +188,7 @@ enum ValidityRange {
 // 3- Ranges intersection is a combination of two new ranges.
 // 4- Intersection is empty.
 impl ValidValueReq {
-    /// Only a type with `ValueAbi::Scalar` and `ValueAbi::ScalarPair` can be directly assigned an
+    /// Only a type with `ValueRepr::Scalar` and `ValueRepr::ScalarPair` can be directly assigned an
     /// invalid value directly.
     ///
     /// It's not possible to define a `rustc_layout_scalar_valid_range_*` to any other structure.
@@ -206,20 +208,20 @@ impl ValidValueReq {
             })
         } else {
             let shape = ty.layout().unwrap().shape();
-            match shape.abi {
-                ValueAbi::Scalar(Scalar::Initialized { value, valid_range })
-                | ValueAbi::ScalarPair { a: Scalar::Initialized { value, valid_range }, .. } => {
+            match shape.value_repr {
+                ValueRepr::Scalar(Scalar::Initialized { value, valid_range })
+                | ValueRepr::ScalarPair { a: Scalar::Initialized { value, valid_range }, .. } => {
                     Some(ValidValueReq {
                         offset: 0,
                         size: value.size(machine_info),
                         valid_range: ValidityRange::Single(valid_range),
                     })
                 }
-                ValueAbi::Scalar(_)
-                | ValueAbi::ScalarPair { .. }
-                | ValueAbi::Vector { .. }
-                | ValueAbi::ScalableVector { .. }
-                | ValueAbi::Aggregate { .. } => None,
+                ValueRepr::Scalar(_)
+                | ValueRepr::ScalarPair { .. }
+                | ValueRepr::Vector { .. }
+                | ValueRepr::ScalableVector { .. }
+                | ValueRepr::Aggregate { .. } => None,
             }
         }
     }
@@ -957,7 +959,7 @@ pub fn ty_validity_per_offset(
             return Err("Unsupported pattern type over `char`".to_string());
         }
         assert!(
-            matches!(layout.abi, ValueAbi::Scalar(..)),
+            matches!(layout.value_repr, ValueRepr::Scalar(..)),
             "expected pattern type to have a scalar ABI: {ty:?}"
         );
         return Ok(ty_req());

kani-compiler/src/main.rs

@@ -8,7 +8,6 @@
 //! rustc_private feature and a specific version of rustc.
 #![feature(extern_types)]
 #![recursion_limit = "256"]
-#![feature(box_patterns)]
 #![feature(rustc_private)]
 #![feature(iter_intersperse)]
 #![feature(f128)]
@@ -39,6 +38,7 @@ extern crate rustc_public;
 extern crate rustc_public_bridge;
 extern crate rustc_session;
 extern crate rustc_span;
+extern crate rustc_structures;
 extern crate rustc_target;
 extern crate rustc_trait_selection;
 // We can't add this directly as a dependency because we need the version to match rustc

kani-driver/src/call_single_file.rs

@@ -273,6 +273,14 @@ pub fn base_rustc_flags(lib_config: LibConfig) -> Vec<RustcArg> {
         "crate-attr=feature(register_tool)",
         "-Z",
         "crate-attr=register_tool(kanitool)",
+        // nightly-2026-09-22 turns the next-generation trait solver on by default
+        // (rust-lang/rust#160619), and that solver cannot handle `generic_const_exprs`
+        // (rust-lang/rust#160895). rustc reverts to this setting automatically for a crate that
+        // enables the feature itself, but Kani's library exposes such a signature
+        // (`kani::pointer_generator`, whose return type computes its buffer length), so every
+        // crate Kani compiles needs the same setting to be able to call it. Tracked for removal in
+        // https://github.com/model-checking/kani/issues/4832.
+        "-Znext-solver=coherence",
         // Kani injects unstable features (`register_tool` above) into every crate it compiles,
         // so crates that `forbid(unstable_features)` (e.g. rustls) would fail to build through
         // no fault of their own. Downgrade that lint to a warning; `--force-warn` overrides

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2026-08-21"
+channel = "nightly-2026-09-22"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]