feliperodri · Oct 13, 2026 · Oct 7, 2026 · Oct 7, 2026 · Oct 7, 2026 · Oct 11, 2026
@@ -14,6 +14,9 @@ ignore = [
     # `llbc` feature and not part of Kani releases.
     { id = "RUSTSEC-2024-0436", reason = "paste is unmaintained; only reached via charon" },
     { id = "RUSTSEC-2023-0089", reason = "atomic-polyfill is unmaintained; only reached via charon" },
+    # Unmaintained (not vulnerable): `unsafe-libyaml` is only reached through `serde_yaml` in
+    # compiletest, our test runner, which is not part of Kani releases.
+    { id = "RUSTSEC-2024-0449", reason = "unsafe-libyaml is unmaintained; only reached via serde_yaml in compiletest" },
 ]
 
 # This section is considered when running `cargo deny check licenses`

@@ -1447,7 +1447,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 let internal = rustc_internal::internal(self.tcx, def_id);
                 let builtin = self
                     .tcx
-                    .is_lang_item(internal, rustc_hir::attrs::lang_items::LangItem::OwnedBox)
+                    .is_lang_item(internal, rustc_attr_ir::lang_items::LangItem::OwnedBox)
                     .then_some(CharonBuiltinAdt::Box);
                 CharonTy::new(CharonTyKind::Adt(CharonTypeDeclRef {
                     id: c_typedeclid,

@@ -7,7 +7,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::codegen_cprover_gotoc::codegen::cache::{CacheEntry, cache_entry};
 use cbmc::goto_program::Location;
 use lazy_static::lazy_static;
-use rustc_hir::Attribute;
+use rustc_attr_ir::Attribute;
 use rustc_public::rustc_internal;
 use rustc_public::ty::Span as SpanStable;
 use rustc_span::Span;

@@ -1558,6 +1558,11 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
             // `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"),
+            // PowerPC's double-double `long double`, which only exists on PowerPC targets. Kani
+            // supports none of them, and CBMC has no double-double type.
+            Float::PpcF128 => {
+                unimplemented!("PowerPC double-double (`ppcf128`) is not supported by Kani")
+            }
         }
     }
 

@@ -17,7 +17,7 @@ use cbmc::goto_program::CIntType;
 use cbmc::goto_program::Symbol as GotoSymbol;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, StmtBody, SymbolValues, Type};
 use cbmc::{InternedString, goto_program::ExprValue};
-use rustc_hir::attrs::lang_items::LangItem;
+use rustc_attr_ir::lang_items::LangItem;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{BasicBlockIdx, Place};

@@ -386,7 +386,7 @@ impl Intrinsic {
             }
             // For const eval of nullary intrinsics, see https://github.com/rust-lang/rust/pull/142839
             "needs_drop" => unreachable!(
-                "Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
+                "Expected nullary intrinsic `core::intrinsics::needs_drop` to be const-evaluated before codegen"
             ),
             // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
             "offset" => unreachable!(
@@ -438,7 +438,7 @@ impl Intrinsic {
                 Self::Transmute
             }
             "type_id" => unreachable!(
-                "Expected nullary intrinsic `core::intrinsics::type_id` to be const-evaluated before codegen"
+                "Expected nullary intrinsic `core::intrinsics::reflection::type_id` to be const-evaluated before codegen"
             ),
             "type_name" => unreachable!(
                 "Expected nullary intrinsic `core::intrinsics::type_name` to be const-evaluated before codegen"

@@ -3,7 +3,7 @@
 
 //! This module defines all compiler extensions that form the Kani compiler.
 //!
-//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::run_compiler`]),
+//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::compiler_entrypoint`]),
 //! which is used to implement stubs.
 //!
 //! In the first run, [KaniCompiler::config] will implement the compiler configuration and it will
@@ -26,7 +26,7 @@ use crate::session::init_session;
 use clap::Parser;
 use rustc_ast::{ast, attr};
 use rustc_codegen_ssa::traits::CodegenBackend;
-use rustc_driver::{Callbacks, Compilation, run_compiler};
+use rustc_driver::{Callbacks, Compilation, compiler_entrypoint};
 use rustc_interface::Config;
 use rustc_interface::interface::Compiler;
 use rustc_middle::ty::TyCtxt;
@@ -106,7 +106,7 @@ const KANI_REQUIRED_RUSTC_ARGS: &[&str] = &[
 ];
 
 /// Run the Kani flavour of the compiler.
-/// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler`]).
+/// This may require multiple runs of the rustc driver ([`rustc_driver::compiler_entrypoint`]).
 pub fn run(mut args: Vec<String>) {
     args.extend(KANI_REQUIRED_RUSTC_ARGS.iter().map(|s| s.to_string()));
     let mut kani_compiler = KaniCompiler::new();
@@ -180,7 +180,7 @@ impl KaniCompiler {
     /// actually invoke the rust compiler multiple times.
     pub fn run(&mut self, args: Vec<String>) {
         debug!(?args, "run_compilation_session");
-        run_compiler(&args, self);
+        compiler_entrypoint(&args, self);
     }
 }
 

@@ -7,11 +7,10 @@ use std::collections::{BTreeMap, HashSet};
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
 use rustc_ast::{LitKind, MetaItem, MetaItemKind};
+use rustc_attr_ir::{AttrArgs, Attribute};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{
-    Attribute,
-    attrs::AttrArgs,
     def::DefKind,
     def_id::{DefId, LocalDefId},
 };
@@ -189,7 +188,7 @@ impl<'tcx> KaniAttributes<'tcx> {
     }
 
     pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self {
-        // `get_all_attrs` is deprecated in favor of `rustc_hir::find_attr!`, but that
+        // `get_all_attrs` is deprecated in favor of `rustc_attr_ir::find_attr!`, but that
         // macro only matches parsed built-in attributes. Kani inspects `kanitool::*`
         // tool attributes, which are unparsed, so `get_all_attrs` is the correct API.
         #[allow(deprecated)]

@@ -13,7 +13,7 @@
 //! definition of custom coercions for smart pointers can be found in the
 //! [RFC 982 DST Coercion](https://rust-lang.github.io/rfcs/0982-dst-coercion.html).
 
-use rustc_hir::attrs::lang_items::LangItem;
+use rustc_attr_ir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;

@@ -11,7 +11,7 @@ use crate::kani_middle::stable_fn_def;
 use quote::ToTokens;
 use rustc_hir::def::{DefKind, Res};
 use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModId};
-use rustc_hir::{ItemKind, UseKind};
+use rustc_hir::{ItemKind, UseKind, UseTree};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::ty::fast_reject::{self, TreatParams};
 use rustc_public::CrateDef;
@@ -533,23 +533,31 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModId, name: &str) -> Rela
     // direct module items take precedence over foreign items.
     let result = tcx.hir_module_free_items(current_module).find_map(|item_id| {
         let item = tcx.hir_item(item_id);
+        // A `use` item is one tree of imports (`use a::{b, c::{d, *}}`), so look for `name`, and
+        // collect globs, at every level of it.
+        if let ItemKind::Use(tree) = item.kind {
+            let mut found = None;
+            visit_use_tree(&tree, &mut |tree| match tree.kind {
+                UseKind::Single(ident) if found.is_none() && ident.as_str() == name => {
+                    found =
+                        tree.prefix.res.present_items().filter_map(|res| res.opt_def_id()).next();
+                }
+                // Do not immediately try to resolve the path using this glob,
+                // since paths resolved via non-globs take precedence.
+                UseKind::Glob => glob_imports.extend(tree.prefix.res.present_items()),
+                UseKind::Single(_) | UseKind::Nested { .. } => {}
+            });
+            return found;
+        }
         if item.kind.ident().is_some_and(|ident| ident.as_str() == name) {
             match item.kind {
-                ItemKind::Use(use_path, UseKind::Single(_)) => {
-                    use_path.res.present_items().filter_map(|res| res.opt_def_id()).next()
-                }
                 ItemKind::ExternCrate(orig_name, _) => resolve_external(
                     tcx,
                     orig_name.as_ref().map(|sym| sym.as_str()).unwrap_or(name),
                 ),
                 _ => Some(item.owner_id.def_id.to_def_id()),
             }
         } else {
-            if let ItemKind::Use(use_path, UseKind::Glob) = item.kind {
-                // Do not immediately try to resolve the path using this glob,
-                // since paths resolved via non-globs take precedence.
-                glob_imports.extend(use_path.res.present_items());
-            }
             // Collect foreign items declared inside `extern` blocks so we can
             // search them if the name is not found as a direct module item.
             // This handles `extern "C" { fn foo(); }` where `foo` is a child
@@ -577,6 +585,18 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModId, name: &str) -> Rela
     RelativeResolution::Globs(glob_imports)
 }
 
+/// Call `f` on `tree` and on every tree nested in it. Since nightly-2026-10-06, rustc keeps
+/// `use a::{b, c}` as one HIR item holding a tree of imports, where it used to lower it to one item
+/// per imported name (rust-lang/rust#161349), so every level has to be visited.
+fn visit_use_tree<'hir>(tree: &UseTree<'hir>, f: &mut impl FnMut(&UseTree<'hir>)) {
+    f(tree);
+    if let UseKind::Nested { items } = tree.kind {
+        for (nested, ..) in items {
+            visit_use_tree(nested, f);
+        }
+    }
+}
+
 /// Resolves a path relative to a local or foreign module.
 /// For local modules, if no module item matches the name we also have to traverse the list of glob
 /// imports. For foreign modules, that list should've been flatten already.

@@ -546,6 +546,9 @@ impl RustcInternalMir for TerminatorKind {
         match self {
             TerminatorKind::Goto { target } => rustc_middle::mir::TerminatorKind::Goto {
                 target: rustc_middle::mir::BasicBlock::from_usize(*target),
+                // Loop hint attributes (`#[unroll]`) have no equivalent in the stable
+                // representation, and Kani-synthesized gotos carry none.
+                loop_hint_attrs: Default::default(),
             },
             TerminatorKind::SwitchInt { discr, targets } => {
                 rustc_middle::mir::TerminatorKind::SwitchInt {
@@ -607,9 +610,6 @@ impl RustcInternalMir for Terminator {
                 self.source_info.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(),
         }
     }
 }

@@ -13,7 +13,7 @@ use crate::kani_middle::transform::body::{
 };
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
-use rustc_hir::attrs::lang_items::LangItem;
+use rustc_attr_ir::lang_items::LangItem;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{

@@ -21,6 +21,7 @@
 extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;
+extern crate rustc_attr_ir;
 extern crate rustc_codegen_ssa;
 extern crate rustc_data_structures;
 extern crate rustc_driver;
@@ -55,7 +56,7 @@ mod kani_middle;
 mod kani_queries;
 mod session;
 
-use rustc_driver::{TimePassesCallbacks, run_compiler};
+use rustc_driver::{TimePassesCallbacks, compiler_entrypoint};
 use std::env;
 
 /// Main function. Configure arguments and run the compiler.
@@ -74,7 +75,7 @@ fn main() {
         kani_compiler::run(rustc_args);
     } else {
         let mut callbacks = TimePassesCallbacks::default();
-        run_compiler(&rustc_args, &mut callbacks);
+        compiler_entrypoint(&rustc_args, &mut callbacks);
     }
 }
 

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2026-09-25"
+channel = "nightly-2026-10-11"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Checks that `copy_nonoverlapping` triggers an overflow failure if the `count`
 //! argument can overflow a `usize`
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Check that `copy_nonoverlapping` fails if the `src`/`dst` regions overlap.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_with_overlap() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -3,6 +3,12 @@
 
 //! Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
 
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `copy_nonoverlapping` fails when `src` is not aligned.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Checks that `copy_nonoverlapping` fails when `src` is not valid for reads.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_invalid() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Checks that `copy_nonoverlapping` fails when `dst` is not valid for writes.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_nonoverlapping_invalid() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -3,6 +3,13 @@
 
 // Checks that `copy` triggers an overflow failure if the `count` argument can
 // overflow a `usize`
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `copy` fails when `dst` is not aligned.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];

@@ -2,6 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! Checks that `copy` fails when `src` is not aligned.
+
+// These call the intrinsics themselves, which `core::ptr` wraps with extra debug assertions,
+// so opt in to `core_intrinsics` instead of importing them through the accidentally stabilized
+// `core::intrinsics` path (denied since rust-lang/rust#163160).
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
 #[kani::proof]
 fn test_copy_unaligned() {
     let arr: [i32; 3] = [0, 1, 0];