Update toolchain to 2025-02-26

Changes to attribute parsing and representation rust-lang/rust#135726 Map methods moved to `TyCtx` rust-lang/rust#137162 rust-lang/rust#137397 Remove `BackendRepr::Unihabited` rust-lang/rust#136985
model-checking · Feb 26, 2025 · fd6136f · fd6136f
1 parent bc573ef
commit fd6136f
Show file tree

Hide file tree

Showing 9 changed files with 79 additions and 57 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
@@ -63,9 +63,7 @@ impl GotocCtx<'_> {
         // Return item tagged with `#[kanitool::recursion_tracker]`
         let mut recursion_trackers = items.iter().filter_map(|item| {
             let MonoItem::Static(static_item) = item else { return None };
-            if !static_item
-                .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()])
-                .is_empty()
+            if !static_item.tool_attrs(&["kanitool".into(), "recursion_tracker".into()]).is_empty()
             {
                 let span = static_item.span();
                 let loc = self.codegen_span_stable(span);

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -1002,8 +1002,10 @@ impl GotocCtx<'_> {
                     // https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
                     // See also the cranelift backend:
                     // https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116
-                    let offset = match &layout.fields {
-                        FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
+                    let offset: rustc_abi::Size = match &layout.fields {
+                        FieldsShape::Arbitrary { offsets, .. } => {
+                            offsets[rustc_abi::FieldIdx::from_usize(0)]
+                        }
                         _ => unreachable!("niche encoding must have arbitrary fields"),
                     };
 

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -7,6 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_cov
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
+use rustc_abi::Size;
 use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{List, TypingEnv};
@@ -350,8 +351,10 @@ impl GotocCtx<'_> {
                 }
                 TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
                     if *untagged_variant != variant_index_internal {
-                        let offset = match &layout.fields {
-                            FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
+                        let offset: Size = match &layout.fields {
+                            FieldsShape::Arbitrary { offsets, .. } => {
+                                offsets[rustc_abi::FieldIdx::from_usize(0)]
+                            }
                             _ => unreachable!("niche encoding must have arbitrary fields"),
                         };
                         let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal);

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -718,7 +718,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let mut final_fields = Vec::with_capacity(flds.len());
                 let mut offset = initial_offset;
                 for idx in layout.fields.index_by_increasing_offset() {
-                    let fld_offset = offsets[idx.into()];
+                    let fld_offset = offsets[rustc_abi::FieldIdx::from(idx)];
                     let (fld_name, fld_ty) = &flds[idx];
                     if let Some(padding) =
                         self.codegen_struct_padding(offset, fld_offset, final_fields.len())
@@ -1557,9 +1557,9 @@ impl<'tcx> GotocCtx<'tcx> {
                     let components = fields_shape
                         .index_by_increasing_offset()
                         .map(|idx| {
-                            let idx = idx.into();
-                            let name = fields[idx].name.to_string().intern();
-                            let field_ty = fields[idx].ty(ctx.tcx, adt_args);
+                            let fidx = FieldIdx::from(idx);
+                            let name = fields[fidx].name.to_string().intern();
+                            let field_ty = fields[fidx].ty(ctx.tcx, adt_args);
                             let typ = if !ctx.is_zst(field_ty) {
                                 last_type.clone()
                             } else {

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -8,7 +8,7 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
 use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr};
 use rustc_errors::ErrorGuaranteed;
-use rustc_hir::{AttrArgs, AttrKind, Attribute, def::DefKind, def_id::DefId};
+use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId};
 use rustc_middle::ty::{Instance, TyCtxt, TyKind};
 use rustc_session::Session;
 use rustc_smir::rustc_internal;
@@ -214,7 +214,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                     .resolve_from_mod(name.as_str())
                     .map_err(|e| {
                         let mut err = self.tcx.dcx().struct_span_err(
-                            attr.span,
+                            attr.span(),
                             format!(
                                 "Failed to resolve replacement function {}: {e}",
                                 name.as_str()
@@ -229,7 +229,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                         err.emit();
                     })
                     .ok()?;
-                Some((name, def, attr.span))
+                Some((name, def, attr.span()))
             })
             .collect()
     }
@@ -247,10 +247,10 @@ impl<'tcx> KaniAttributes<'tcx> {
         self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| {
             let name = expect_key_string_value(self.tcx.sess, target).ok()?;
             self.resolve_from_mod(name.as_str())
-                .map(|ok| (name, ok, target.span))
+                .map(|ok| (name, ok, target.span()))
                 .map_err(|resolve_err| {
                     let mut err = self.tcx.dcx().struct_span_err(
-                        target.span,
+                        target.span(),
                         format!(
                             "Failed to resolve checking function {} because {resolve_err}",
                             name.as_str()
@@ -336,7 +336,7 @@ impl<'tcx> KaniAttributes<'tcx> {
         // Check that all attributes are correctly used and well formed.
         let is_harness = self.is_proof_harness();
         for (&kind, attrs) in self.map.iter() {
-            let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg);
+            let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span(), msg);
 
             if !is_harness && kind.is_harness_only() {
                 local_error(format!(
@@ -451,7 +451,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                     kind.as_ref()
                 );
                 if let Some(attr) = self.map.get(&kind).unwrap().first() {
-                    self.tcx.dcx().span_err(attr.span, msg);
+                    self.tcx.dcx().span_err(attr.span(), msg);
                 } else {
                     self.tcx.dcx().err(msg);
                 }
@@ -646,7 +646,7 @@ impl<'tcx> KaniAttributes<'tcx> {
 
     /// Check that if this item is tagged with a proof_attribute, it is a valid harness.
     fn check_proof_attribute(&self, kind: KaniAttributeKind, proof_attribute: &Attribute) {
-        let span = proof_attribute.span;
+        let span = proof_attribute.span();
         let tcx = self.tcx;
         if let KaniAttributeKind::Proof = kind {
             expect_no_args(tcx, kind, proof_attribute);
@@ -719,7 +719,7 @@ fn expect_key_string_value(
     sess: &Session,
     attr: &Attribute,
 ) -> Result<rustc_span::Symbol, ErrorGuaranteed> {
-    let span = attr.span;
+    let span = attr.span();
     let AttrArgs::Eq { expr, .. } = &attr.get_normal_item().args else {
         return Err(sess
             .dcx()
@@ -743,7 +743,7 @@ fn expect_single<'a>(
         .expect(&format!("expected at least one attribute {} in {attributes:?}", kind.as_ref()));
     if attributes.len() > 1 {
         tcx.dcx().span_err(
-            attr.span,
+            attr.span(),
             format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()),
         );
     }
@@ -774,7 +774,7 @@ impl UnstableAttrParseError<'_> {
     fn report(&self, tcx: TyCtxt) -> ErrorGuaranteed {
         tcx.dcx()
             .struct_span_err(
-                self.attr.span,
+                self.attr.span(),
                 format!("failed to parse `#[kani::unstable_feature]`: {}", self.reason),
             )
             .with_note(format!(
@@ -817,7 +817,7 @@ impl<'a> TryFrom<&'a Attribute> for UnstableAttribute {
 fn expect_no_args(tcx: TyCtxt, kind: KaniAttributeKind, attr: &Attribute) {
     if !attr.is_word() {
         tcx.dcx()
-            .struct_span_err(attr.span, format!("unexpected argument for `{}`", kind.as_ref()))
+            .struct_span_err(attr.span(), format!("unexpected argument for `{}`", kind.as_ref()))
             .with_help("remove the extra argument")
             .emit();
     }
@@ -830,7 +830,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option<u32> {
         None => {
             // There are no integers or too many arguments given to the attribute
             tcx.dcx().span_err(
-                attr.span,
+                attr.span(),
                 "invalid argument for `unwind` attribute, expected an integer",
             );
             None
@@ -839,7 +839,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option<u32> {
             if let Ok(val) = unwind_integer_value.try_into() {
                 Some(val)
             } else {
-                tcx.dcx().span_err(attr.span, "value above maximum permitted value - u32::MAX");
+                tcx.dcx().span_err(attr.span(), "value above maximum permitted value - u32::MAX");
                 None
             }
         }
@@ -854,13 +854,13 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
             Ok(FnResolution::Fn(_)) => { /* no-op */ }
             Ok(FnResolution::FnImpl { .. }) => {
                 tcx.dcx().span_err(
-                    attr.span,
+                    attr.span(),
                     "Kani currently does not support stubbing trait implementations.",
                 );
             }
             Err(err) => {
                 tcx.dcx().span_err(
-                    attr.span,
+                    attr.span(),
                     format!("failed to resolve `{}`: {err}", pretty_type_path(path)),
                 );
             }
@@ -871,7 +871,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
         .filter_map(|attr| {
             let paths = parse_paths(tcx, attr).unwrap_or_else(|_| {
                 tcx.dcx().span_err(
-                    attr.span,
+                    attr.span(),
                     format!(
                     "attribute `kani::{}` takes two path arguments; found argument that is not a path",
                     KaniAttributeKind::Stub.as_ref())
@@ -893,7 +893,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
                 }
                 _ => {
                     tcx.dcx().span_err(
-                        attr.span,
+                        attr.span(),
                         format!(
                             "attribute `kani::stub` takes two path arguments; found {}",
                             paths.len()
@@ -912,15 +912,15 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
     const ATTRIBUTE: &str = "#[kani::solver]";
     let invalid_arg_err = |attr: &Attribute| {
         tcx.dcx().span_err(
-            attr.span,
+            attr.span(),
             format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"<SAT_SOLVER_BINARY>\"`)"),
         )
     };
 
     let attr_args = attr.meta_item_list().unwrap();
     if attr_args.len() != 1 {
         tcx.dcx().span_err(
-            attr.span,
+            attr.span(),
             format!(
                 "the `{ATTRIBUTE}` attribute expects a single argument. Got {} arguments.",
                 attr_args.len()
@@ -943,7 +943,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
             match solver {
                 Ok(solver) => Some(solver),
                 Err(_) => {
-                    tcx.dcx().span_err(attr.span, format!("unknown solver `{ident_str}`"));
+                    tcx.dcx().span_err(attr.span(), format!("unknown solver `{ident_str}`"));
                     None
                 }
             }
@@ -1016,27 +1016,47 @@ fn parse_str_value(attr: &Attribute) -> Option<String> {
 
 /// If the attribute is named `kanitool::name`, this extracts `name`
 fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
-    match &attr.kind {
-        AttrKind::Normal(normal) => {
-            let segments = &normal.path.segments;
-            if (!segments.is_empty()) && segments[0].as_str() == "kanitool" {
-                let ident_str = segments[1..]
-                    .iter()
-                    .map(|segment| segment.as_str())
-                    .intersperse("::")
-                    .collect::<String>();
-                KaniAttributeKind::try_from(ident_str.as_str())
-                    .inspect_err(|&err| {
-                        debug!(?err, "attr_kind_failed");
-                        tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`"));
-                    })
-                    .ok()
-            } else {
-                None
-            }
+    if let Attribute::Unparsed(normal) = attr {
+        let segments = &normal.path.segments;
+        if (!segments.is_empty()) && segments[0].as_str() == "kanitool" {
+            let ident_str = segments[1..]
+                .iter()
+                .map(|segment| segment.as_str())
+                .intersperse("::")
+                .collect::<String>();
+            KaniAttributeKind::try_from(ident_str.as_str())
+                .inspect_err(|&err| {
+                    debug!(?err, "attr_kind_failed");
+                    tcx.dcx().span_err(attr.span(), format!("unknown attribute `{ident_str}`"));
+                })
+                .ok()
+        } else {
+            None
         }
-        _ => None,
+    } else {
+        None
     }
+    // match &attr.kind {
+    //     AttrKind::Normal(normal) => {
+    //         let segments = &normal.path.segments;
+    //         if (!segments.is_empty()) && segments[0].as_str() == "kanitool" {
+    //             let ident_str = segments[1..]
+    //                 .iter()
+    //                 .map(|segment| segment.as_str())
+    //                 .intersperse("::")
+    //                 .collect::<String>();
+    //             KaniAttributeKind::try_from(ident_str.as_str())
+    //                 .inspect_err(|&err| {
+    //                     debug!(?err, "attr_kind_failed");
+    //                     tcx.dcx().span_err(attr.span(), format!("unknown attribute `{ident_str}`"));
+    //                 })
+    //                 .ok()
+    //         } else {
+    //             None
+    //         }
+    //     }
+    //     _ => None,
+    // }
 }
 
 /// Parse an attribute using `syn`.
@@ -1099,7 +1119,7 @@ fn pretty_type_path(path: &TypePath) -> String {
 /// Retrieve the value of the `fn_marker` attribute for the given definition if it has one.
 pub(crate) fn fn_marker<T: CrateDef>(def: T) -> Option<String> {
     let fn_marker: [SymbolStable; 2] = ["kanitool".into(), "fn_marker".into()];
-    let marker = def.attrs_by_path(&fn_marker).pop()?;
+    let marker = def.tool_attrs(&fn_marker).pop()?;
     let attribute = syn_attr_stable(&marker);
     let meta_name = attribute.meta.require_name_value().unwrap_or_else(|_| {
         panic!("Expected name value attribute for `kanitool::fn_marker`, but found: `{:?}`", marker)

diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs
@@ -93,7 +93,7 @@ fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx>
         ty::Adt(def, args) => {
             assert!(def.repr().simd(), "`simd_size_and_type` called on non-SIMD type");
             let variant = def.non_enum_variant();
-            let f0_ty = variant.fields[0u32.into()].ty(tcx, args);
+            let f0_ty = variant.fields[rustc_abi::FieldIdx::from_usize(0)].ty(tcx, args);
 
             match f0_ty.kind() {
                 ty::Array(elem_ty, len) => (*len, *elem_ty),

diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
@@ -307,7 +307,7 @@ fn resolve_prefix<'tcx>(
         (None, Some(segment)) if segment.ident == CRATE => {
             // Find the module at the root of the crate.
             let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module);
-            let crate_root = match tcx.hir().parent_iter(current_module_hir_id).last() {
+            let crate_root = match tcx.hir_parent_iter(current_module_hir_id).last() {
                 None => current_module,
                 Some((hir_id, _)) => hir_id.owner.def_id,
             };
@@ -366,7 +366,7 @@ where
     I: Iterator<Item = &'a PathSegment>,
 {
     let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module);
-    let mut parents = tcx.hir().parent_iter(current_module_hir_id);
+    let mut parents = tcx.hir_parent_iter(current_module_hir_id);
     let mut base_module = current_module;
     while segments.next_if(|segment| segment.ident == SUPER).is_some() {
         if let Some((parent, _)) = parents.next() {

diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -213,7 +213,6 @@ impl ValidValueReq {
                 }
                 ValueAbi::Scalar(_)
                 | ValueAbi::ScalarPair(_, _)
-                | ValueAbi::Uninhabited
                 | ValueAbi::Vector { .. }
                 | ValueAbi::Aggregate { .. } => None,
             }

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-02-21"
+channel = "nightly-2025-02-26"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]