diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 1ef23ac02c22..42f2ef5e4cb3 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -38,9 +38,9 @@ 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::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; +use rustc_session::{IncrCompSession, Session}; use std::any::Any; use std::fs::File; use std::path::Path; @@ -296,6 +296,7 @@ impl CodegenBackend for LlbcCodegenBackend { &self, ongoing_codegen: Box, _sess: &Session, + _incr_comp_session: Option<&IncrCompSession>, _filenames: &OutputFilenames, _crate_info: &CrateInfo, ) -> (CompiledModules, UnordMap) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index c4eeef34d265..07593bd5315b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -813,7 +813,15 @@ impl GotocCtx<'_, '_> { Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => { self.codegen_pointer_cast(k, e, *t, loc) } - Rvalue::Cast(CastKind::Transmute | CastKind::Subtype, operand, ty) => { + // `BoxDerefTransmute` is an elaborated `Box` deref turning the inner pointer into a + // raw one. Its docs describe it as a regular transmute that is additionally UB if the + // input is not valid as a `Box`, and say backends may treat it as a plain + // transmute; Kani checks pointer validity separately at the deref itself. + Rvalue::Cast( + CastKind::Transmute | CastKind::BoxDerefTransmute | CastKind::Subtype, + operand, + ty, + ) => { let src_ty = operand.ty(self.current_fn().locals()).unwrap(); // Transmute requires sized types. let src_sz = LayoutOf::new(src_ty).size_of().unwrap(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index df20cf590cb7..accc2e80c783 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -744,6 +744,22 @@ impl GotocCtx<'_, '_> { ) -> Stmt { debug!(?func, ?args, ?destination, ?span, "codegen_funcall"); let instance_opt = self.get_instance(func); + if let Some(instance) = instance_opt + && matches!(instance.kind, InstanceKind::LlvmIntrinsic) + { + // An LLVM intrinsic -- an `extern "unadjusted"` declaration whose symbol starts with + // `llvm.` -- has no Rust body, and rustc refuses to compute a `FnAbi` for one, so we + // cannot codegen the call or even its arguments. Kani has no model for these either, + // so report the call as unsupported. As of nightly-2026-08-21 these resolve to their + // own `InstanceKind`; before that they were foreign items, and this reports the same + // unsupported-construct check that the FFI shim did, so reaching one still fails + // verification rather than silently succeeding. + return self.codegen_unimplemented_stmt( + &format!("call to LLVM intrinsic `{}`", instance.mangled_name()), + self.codegen_span_stable(span), + "https://github.com/model-checking/kani/issues/4770", + ); + } if let Some(instance) = instance_opt && matches!(instance.kind, InstanceKind::Intrinsic) { @@ -805,10 +821,12 @@ impl GotocCtx<'_, '_> { self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc) } // Normal, non-virtual function calls - InstanceKind::Item - | InstanceKind::Intrinsic - | InstanceKind::LlvmIntrinsic - | InstanceKind::Shim => { + InstanceKind::LlvmIntrinsic => { + unreachable!( + "Kani reports LLVM intrinsic calls as unsupported before codegen" + ) + } + InstanceKind::Item | InstanceKind::Intrinsic | InstanceKind::Shim => { // We need to handle FnDef items in a special way because `codegen_operand` compiles them to dummy structs. // (cf. the function documentation) let func_exp = self.codegen_func_expr(instance, loc); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 3d51c0330870..e3396454fd9c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1637,7 +1637,9 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { let rust_type = self.codegen_prim_typ(prim_type); let cbmc_type = self.codegen_ty(rust_type); - Type::vector(cbmc_type, *size) + // As of nightly-2026-08-21 the lane count is a `BackendLaneCount` (a `NonZero`) + // rather than a bare `u64`. + Type::vector(cbmc_type, size.as_u64()) } /// the function type of the current instance diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 5542f75f74e8..3fd20e0659bd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -30,7 +30,7 @@ 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; -use rustc_data_structures::unord::UnordMap; +use rustc_data_structures::unord::{UnordMap, UnordSet}; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; @@ -40,9 +40,9 @@ use rustc_public::CrateDef; use rustc_public::mir::mono::{Instance, MonoItem}; use rustc_public::rustc_internal; use rustc_public::ty::FnDef; -use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; +use rustc_session::{IncrCompSession, Session}; use rustc_span::{Symbol, sym}; use rustc_target::spec::{Arch, Os, PanicStrategy}; use std::any::Any; @@ -311,15 +311,13 @@ impl CodegenBackend for GotocCodegenBackend { } else { vec![] }; - // FIXME do `unstable_target_features` properly - let unstable_target_features = target_features.clone(); - let has_reliable_f128 = true; let has_reliable_f16 = true; TargetConfig { - target_features, - unstable_target_features, + // As of nightly-2026-08-21 the separate stable/unstable `Vec` feature lists + // are a single `UnordSet`, so there is no longer an unstable list to populate. + internal_target_features: UnordSet::from_iter(target_features), has_reliable_f16, has_reliable_f16_math: has_reliable_f16, has_reliable_f128, @@ -525,6 +523,7 @@ impl CodegenBackend for GotocCodegenBackend { &self, ongoing_codegen: Box, _sess: &Session, + _incr_comp_session: Option<&IncrCompSession>, _filenames: &OutputFilenames, _crate_info: &CrateInfo, ) -> (CompiledModules, UnordMap) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 6e8b39d8706c..0ff1f99b39ef 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -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::LangItem; +use rustc_hir::attrs::lang_items::LangItem; use rustc_middle::ty::TyCtxt; use rustc_public::mir::mono::Instance; use rustc_public::mir::{BasicBlockIdx, Place}; diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 0f8072e35ffb..38b79ddbc223 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -1338,7 +1338,10 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { /// /// This provides a user-friendly interface to manipulate than the internal compiler AST. fn syn_attr(tcx: TyCtxt, attr: &Attribute) -> syn::Attribute { - let attr_str = rustc_hir_pretty::attribute_to_string(&tcx, attr); + // As of nightly-2026-08-21 `TyCtxt` no longer implements `PpAnn` directly; the impl is on + // `&dyn HirTyCtxt`, which `TyCtxt` does implement. + let hir_tcx: &dyn rustc_hir::intravisit::HirTyCtxt<'_> = &tcx; + let attr_str = rustc_hir_pretty::attribute_to_string(&hir_tcx, attr); let parser = syn::Attribute::parse_outer; parser.parse_str(&attr_str).unwrap().pop().unwrap() } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 8e2861d83cc6..551c3a45dfcc 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -547,7 +547,8 @@ fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool predicate.skip_normalization(), )); } - ocx.evaluate_obligations_error_on_ambiguity().is_empty() + // As of nightly-2026-08-21 this returns a `TraitErrors` enum rather than a vector of errors. + ocx.evaluate_obligations_error_on_ambiguity().no_errors() } /// The nondet closure-model FnDefs, keyed by input shape. By-value models fix their diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 5365a6b4fd68..5219243be50a 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -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::lang_items::LangItem; +use rustc_hir::attrs::lang_items::LangItem; use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData}; use rustc_middle::ty::TraitRef; use rustc_middle::ty::adjustment::CustomCoerceUnsized; diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 33ea3f1a4558..6bda959e7712 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -35,8 +35,7 @@ use crate::{ use rustc_middle::{ mir::{ BasicBlock, BinOp, Body, CallReturnPlaces, Location, NonDivergingIntrinsic, Operand, Place, - ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorEdges, - TerminatorKind, + ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }, ty::{Instance, InstanceKind, List, TyCtxt, TyKind, TypingEnv}, }; @@ -182,12 +181,12 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } } - fn apply_primary_terminator_effect<'mir>( + fn apply_primary_terminator_effect( &self, state: &mut Self::Domain, - terminator: &'mir Terminator<'tcx>, + terminator: &Terminator<'tcx>, location: Location, - ) -> TerminatorEdges<'mir, 'tcx> { + ) { if let TerminatorKind::Call { func, args, destination, .. } = &terminator.kind { // Attempt to resolve callee. For now, we panic if the callee cannot be resolved (e.g., // if a function pointer call is used), but we could leverage the call graph to resolve @@ -331,7 +330,6 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } } }; - terminator.edges() } /// We don't care about this and just need to implement this to implement the trait. diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 52aad2cf06a0..6c078dd0bf74 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -629,7 +629,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { }) } } - CastKind::Transmute | CastKind::Subtype => { + CastKind::Transmute | CastKind::BoxDerefTransmute | CastKind::Subtype => { debug!(?dest_ty, "transmute"); // For transmute, we care about the destination type only. // This could be optimized to only add a check if the requirements of the diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index f75d6cf4a795..433968a737c8 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -149,6 +149,7 @@ impl RustcInternalMir for CastKind { CastKind::PtrToPtr => rustc_middle::mir::CastKind::PtrToPtr, CastKind::FnPtrToPtr => rustc_middle::mir::CastKind::FnPtrToPtr, CastKind::Transmute => rustc_middle::mir::CastKind::Transmute, + CastKind::BoxDerefTransmute => rustc_middle::mir::CastKind::BoxDerefTransmute, CastKind::Subtype => rustc_middle::mir::CastKind::Subtype, } } diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 1e4f0c99c833..68d8e2c4569a 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -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::LangItem; +use rustc_hir::attrs::lang_items::LangItem; use rustc_middle::ty::TyCtxt; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 38b9a5467956..c5532974f85d 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-08-01" +channel = "nightly-2026-08-21" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs index a5bb0cbe9561..03f32b604533 100644 --- a/tests/expected/uninit/atomic/atomic.rs +++ b/tests/expected/uninit/atomic/atomic.rs @@ -18,10 +18,12 @@ fn local_atomic_uninit() { unsafe { match kani::any() { 0 => { - atomic_store::<_, { AtomicOrdering::Relaxed }>(ptr, 1); + atomic_store::<_, { AtomicOrdering::Relaxed }, /* VOLATILE */ false>(ptr, 1); } 1 => { - atomic_load::<_, { AtomicOrdering::Relaxed }>(ptr as *const u8); + atomic_load::<_, { AtomicOrdering::Relaxed }, /* VOLATILE */ false>( + ptr as *const u8, + ); } _ => { atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>( diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs index 5f3fc29c0571..9ba1123ba856 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs @@ -18,9 +18,9 @@ fn main() { let ptr_a3: *const u8 = &a3; unsafe { - let x1 = atomic_load::<_, { AtomicOrdering::SeqCst }>(ptr_a1); - let x2 = atomic_load::<_, { AtomicOrdering::Acquire }>(ptr_a2); - let x3 = atomic_load::<_, { AtomicOrdering::Relaxed }>(ptr_a3); + let x1 = atomic_load::<_, { AtomicOrdering::SeqCst }, /* VOLATILE */ false>(ptr_a1); + let x2 = atomic_load::<_, { AtomicOrdering::Acquire }, /* VOLATILE */ false>(ptr_a2); + let x3 = atomic_load::<_, { AtomicOrdering::Relaxed }, /* VOLATILE */ false>(ptr_a3); assert!(x1 == 1); assert!(x2 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs index 8581c6b9698a..af9eb971f9bb 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs @@ -18,9 +18,9 @@ fn main() { let ptr_a3: *mut u8 = &mut a3; unsafe { - atomic_store::<_, { AtomicOrdering::SeqCst }>(ptr_a1, 0); - atomic_store::<_, { AtomicOrdering::Release }>(ptr_a2, 0); - atomic_store::<_, { AtomicOrdering::Relaxed }>(ptr_a3, 0); + atomic_store::<_, { AtomicOrdering::SeqCst }, /* VOLATILE */ false>(ptr_a1, 0); + atomic_store::<_, { AtomicOrdering::Release }, /* VOLATILE */ false>(ptr_a2, 0); + atomic_store::<_, { AtomicOrdering::Relaxed }, /* VOLATILE */ false>(ptr_a3, 0); assert!(*ptr_a1 == 0); assert!(*ptr_a2 == 0); diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index bb8708a14f68..d577a013fa9a 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -148,6 +148,12 @@ fn build_kani_lib( "always-encode-mir", "-Z", "mir-enable-passes=-RemoveStorageMarkers", + // Kani copies these rlibs into its sysroot and later compiles against them on their own, + // so they must carry full metadata. Without this the rlib holds only a metadata stub and + // the full `.rmeta` is left behind in the build directory, which fails as + // "only metadata stub found for `rlib` dependency". + "-Z", + "embed-metadata=yes", ]; rustc_args.extend_from_slice(extra_rustc_args); let mut cmd = Command::new("cargo")