Upgrade Rust toolchain to nightly-2026-08-01

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -163,7 +163,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         defid: DefId,
     ) -> (CharonVector<CharonTraitClauseId, CharonTraitRef>, Vec<CharonSpan>) {
         let inter_defid = rustc_internal::internal(self.tcx, defid);
-        let predicates = self.tcx().predicates_of(inter_defid).predicates.to_vec();
+        let predicates = self.tcx().clauses_of(inter_defid).clauses.to_vec();
         let mut c_trait_refs: CharonVector<CharonTraitClauseId, CharonTraitRef> =
             CharonVector::new();
         let mut c_spans = Vec::new();
@@ -207,7 +207,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         defid: DefId,
     ) -> CharonVector<CharonTraitClauseId, CharonTraitClause> {
         let inter_defid = rustc_internal::internal(self.tcx, defid);
-        let predicates = self.tcx().predicates_of(inter_defid).predicates.to_vec();
+        let predicates = self.tcx().clauses_of(inter_defid).clauses.to_vec();
         let mut c_trait_clauses: CharonVector<CharonTraitClauseId, CharonTraitClause> =
             CharonVector::new();
         for (i, (clause, span)) in predicates.iter().enumerate() {
@@ -1531,7 +1531,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             _ => todo!(),
         };
         if let Some(content) = content {
-            let span = self.translate_span(stmt.span);
+            let span = self.translate_span(stmt.source_info.span);
             return Some(CharonStatement { span, content, comments_before: Vec::new() });
         };
         None
@@ -1541,7 +1541,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         &mut self,
         terminator: &Terminator,
     ) -> (Option<CharonStatement>, CharonTerminator) {
-        let span = self.translate_span(terminator.span);
+        let span = self.translate_span(terminator.source_info.span);
         let (statement, terminator) = match &terminator.kind {
             TerminatorKind::Return => (None, CharonRawTerminator::Return),
             TerminatorKind::Goto { target } => {

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

@@ -127,9 +127,9 @@ impl GotocCtx<'_, '_> {
             // closure capture of a contract-clause closure, which is valid by
             // construction (see `CurrentFnCtx::is_capture_ref_local`), so tell
             // CBMC not to generate pointer-validity checks for it.
-            self.codegen_span_stable_with_pragmas(stmt.span, &["disable:pointer-check"])
+            self.codegen_span_stable_with_pragmas(stmt.source_info.span, &["disable:pointer-check"])
         } else {
-            self.codegen_span_stable(stmt.span)
+            self.codegen_span_stable(stmt.source_info.span)
         };
         match &stmt.kind {
             StatementKind::Assign(lhs, rhs) => {
@@ -151,7 +151,8 @@ impl GotocCtx<'_, '_> {
                         let msg = "found `#[kani::loop_decreases]` without \
                                    `-Z loop-contracts`. The decreases clause \
                                    will be ignored.";
-                        let internal_span = rustc_internal::internal(self.tcx, stmt.span);
+                        let internal_span =
+                            rustc_internal::internal(self.tcx, stmt.source_info.span);
                         self.tcx.dcx().span_warn(internal_span, msg);
                         return Stmt::skip(location);
                     }
@@ -293,8 +294,12 @@ impl GotocCtx<'_, '_> {
                 let maybe_source_region =
                     region_from_coverage_opaque(self.tcx, coverage_opaque, instance);
                 if let Some((source_region, file_name)) = maybe_source_region {
-                    let coverage_stmt =
-                        self.codegen_coverage(&counter_data, stmt.span, source_region, &file_name);
+                    let coverage_stmt = self.codegen_coverage(
+                        &counter_data,
+                        stmt.source_info.span,
+                        source_region,
+                        &file_name,
+                    );
                     // TODO: Avoid single-statement blocks when conversion of
                     // standalone statements to the irep format is fixed.
                     // More details in <https://github.com/model-checking/kani/issues/3012>
@@ -318,7 +323,7 @@ impl GotocCtx<'_, '_> {
     ///
     /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s.
     pub fn codegen_terminator(&mut self, term: &Terminator) -> Stmt {
-        let loc = self.codegen_span_stable(term.span);
+        let loc = self.codegen_span_stable(term.source_info.span);
         let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered();
         debug!("handling terminator {:?}", term);
         //TODO: Instead of doing location::none(), and updating, just putit in when we make the stmt.
@@ -369,7 +374,7 @@ impl GotocCtx<'_, '_> {
                 self.codegen_drop(place, target, loc)
             }
             TerminatorKind::Call { func, args, destination, target, .. } => {
-                self.codegen_funcall(func, args, destination, target, term.span)
+                self.codegen_funcall(func, args, destination, target, term.source_info.span)
             }
             TerminatorKind::Assert { cond, expected, msg, target, .. } => {
                 let cond = {
@@ -395,7 +400,8 @@ impl GotocCtx<'_, '_> {
                         PropertyClass::SafetyCheck,
                     ),
                     // For all other assert kind we can get the static message.
-                    AssertMessage::NullPointerDereference => {
+                    AssertMessage::NullPointerDereference
+                    | AssertMessage::NullReferenceConstructed => {
                         (msg.description().unwrap(), PropertyClass::SafetyCheck)
                     }
                     AssertMessage::Overflow { .. }
@@ -410,7 +416,7 @@ impl GotocCtx<'_, '_> {
                 };
 
                 let (msg_str, reach_stmt) =
-                    self.codegen_reachability_check(msg.to_owned(), term.span);
+                    self.codegen_reachability_check(msg.to_owned(), term.source_info.span);
 
                 Stmt::block(
                     vec![
@@ -799,7 +805,10 @@ impl GotocCtx<'_, '_> {
                         self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc)
                     }
                     // Normal, non-virtual function calls
-                    InstanceKind::Item | InstanceKind::Intrinsic | InstanceKind::Shim => {
+                    InstanceKind::Item
+                    | InstanceKind::Intrinsic
+                    | InstanceKind::LlvmIntrinsic
+                    | 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);

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

@@ -640,7 +640,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
                     self.tcx,
                     ty::TypingEnv::fully_monomorphized(),
                     *def_id,
-                    args,
+                    args.skip_binder(),
                 )
                 .unwrap()
                 .unwrap();

kani-compiler/src/kani_middle/codegen_units.rs

@@ -497,9 +497,9 @@ fn impl_derived_candidates(tcx: TyCtxt, def: FnDef) -> FxHashMap<usize, Vec<Ty>>
     // here would leave such a parameter with primitive candidates only.
     let mut next = Some(rustc_internal::internal(tcx, def.def_id()));
     while let Some(def_id) = next {
-        let generic_predicates = tcx.predicates_of(def_id);
-        next = generic_predicates.parent;
-        for (predicate, _span) in generic_predicates.predicates {
+        let generic_clauses = tcx.clauses_of(def_id);
+        next = generic_clauses.parent;
+        for (predicate, _span) in generic_clauses.clauses {
             let Some(trait_pred) = predicate.as_trait_clause() else { continue };
             let trait_pred = trait_pred.skip_binder();
             let ty::Param(param_ty) = trait_pred.self_ty().kind() else { continue };
@@ -538,7 +538,7 @@ fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool
 
     let def_id = rustc_internal::internal(tcx, def.def_id());
     let args_internal = rustc_internal::internal(tcx, args);
-    let predicates = tcx.predicates_of(def_id).instantiate(tcx, args_internal);
+    let predicates = tcx.clauses_of(def_id).instantiate(tcx, args_internal);
     for (predicate, _span) in predicates {
         ocx.register_obligation(Obligation::new(
             tcx,
@@ -623,7 +623,7 @@ fn fn_bound_candidates<'tcx>(
     let fn_tr = tcx.lang_items().fn_trait();
     // Collect Fn-ish trait predicates keyed by the self param index, with tupled inputs.
     let mut sig_inputs: FxHashMap<usize, rustc_middle::ty::Ty> = FxHashMap::default();
-    for (predicate, _span) in tcx.predicates_of(def_id).predicates {
+    for (predicate, _span) in tcx.clauses_of(def_id).clauses {
         let Some(tp) = predicate.as_trait_clause() else { continue };
         // HRTB bounds (e.g. for<'a> FnOnce(&'a Self)) carry late-bound regions; erase them
         // rather than skipping the binder, which would leak escaping bound vars into the
@@ -645,7 +645,7 @@ fn fn_bound_candidates<'tcx>(
     }
     // The return type comes from the FnOnce::Output projection bound.
     let mut sig_output: FxHashMap<usize, rustc_middle::ty::Ty> = FxHashMap::default();
-    for (predicate, _span) in tcx.predicates_of(def_id).predicates {
+    for (predicate, _span) in tcx.clauses_of(def_id).clauses {
         let Some(proj) = predicate.as_projection_clause() else { continue };
         let proj = tcx.instantiate_bound_regions_with_erased(proj);
         let rustc_middle::ty::TyKind::Param(param_ty) = proj.projection_term.self_ty().kind()
@@ -663,7 +663,7 @@ fn fn_bound_candidates<'tcx>(
         if inputs.has_param() || output.has_param() {
             // Signature references other generic parameters: defer construction until a
             // candidate choice for those parameters is made.
-            // SAFETY of the transmute-free 'static: predicates_of types live for the whole
+            // SAFETY of the transmute-free 'static: clauses_of types live for the whole
             // compilation session ('tcx); we only use them within this query's lifetime.
             deferred.insert(idx, DeferredFnSpec { inputs, output });
             continue;

kani-compiler/src/kani_middle/intrinsics.rs

@@ -113,7 +113,7 @@ fn resolve_rust_intrinsic<'tcx>(
     if let ty::FnDef(def_id, args) = *func_ty.kind()
         && let Some(symbol) = tcx.intrinsic(def_id)
     {
-        return Some((symbol, args));
+        return Some((symbol, args.skip_binder()));
     }
     None
 }

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

@@ -359,7 +359,7 @@ fn try_resolve_instance<'tcx>(
                 tcx,
                 TypingEnv::fully_monomorphized(),
                 *def,
-                args,
+                args.skip_binder(),
                 DUMMY_SP,
             ))
         }

kani-compiler/src/kani_middle/reachability.rs

@@ -271,6 +271,11 @@ impl MonoItemsFnCollector<'_, '_> {
                 assert!(is_direct_call, "Expected direct call {instance:?}");
                 false
             }
+            InstanceKind::LlvmIntrinsic => {
+                // LLVM intrinsics have no Rust body to collect.
+                assert!(is_direct_call, "Expected direct call {instance:?}");
+                false
+            }
             InstanceKind::Intrinsic => {
                 // Intrinsics may have a fallback body.
                 assert!(is_direct_call, "Expected direct call {instance:?}");

kani-compiler/src/kani_middle/resolve.rs

@@ -10,7 +10,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, LocalModDefId};
+use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModId};
 use rustc_hir::{ItemKind, UseKind};
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::ty::fast_reject::{self, TreatParams};
@@ -522,7 +522,7 @@ enum RelativeResolution {
 }
 
 /// Resolves a path relative to a local module.
-fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> RelativeResolution {
+fn resolve_relative(tcx: TyCtxt, current_module: LocalModId, name: &str) -> RelativeResolution {
     debug!(?name, ?current_module, "resolve_relative");
 
     let mut glob_imports = vec![];
@@ -590,7 +590,7 @@ fn resolve_in_module<'tcx>(
             ResolveError::MissingItem { tcx, base: current_module, unresolved: name.to_string() }
         }),
         Some(local_id) => {
-            let result = resolve_relative(tcx, LocalModDefId::new_unchecked(local_id), name);
+            let result = resolve_relative(tcx, LocalModId::new_unchecked(local_id), name);
             match result {
                 RelativeResolution::Found(def_id) => Ok(def_id),
                 RelativeResolution::Globs(globs) => {
@@ -644,7 +644,7 @@ fn resolve_in_glob_uses<'tcx>(
 fn resolve_in_glob_use(tcx: TyCtxt, res: &Res, name: &str) -> RelativeResolution {
     if let Res::Def(DefKind::Mod, def_id) = res {
         if let Some(local_id) = def_id.as_local() {
-            resolve_relative(tcx, LocalModDefId::new_unchecked(local_id), name)
+            resolve_relative(tcx, LocalModId::new_unchecked(local_id), name)
         } else {
             resolve_in_foreign_module(tcx, *def_id, name)
                 .map_or(RelativeResolution::Globs(vec![]), RelativeResolution::Found)

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

@@ -12,6 +12,7 @@ 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;