Upgrade toolchain to nightly-2024-12-18

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

@@ -6,7 +6,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
 use lazy_static::lazy_static;
-use rustc_ast::Attribute;
+use rustc_hir::Attribute;
 use rustc_smir::rustc_internal;
 use rustc_span::Span;
 use stable_mir::ty::Span as SpanStable;

kani-compiler/src/kani_middle/attributes.rs

@@ -6,11 +6,9 @@ use std::collections::{BTreeMap, HashSet};
 
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
-use rustc_ast::{
-    AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, attr,
-};
+use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr};
 use rustc_errors::ErrorGuaranteed;
-use rustc_hir::{def::DefKind, def_id::DefId};
+use rustc_hir::{AttrArgs, AttrKind, Attribute, def::DefKind, def_id::DefId};
 use rustc_middle::ty::{Instance, TyCtxt, TyKind};
 use rustc_session::Session;
 use rustc_smir::rustc_internal;
@@ -673,31 +671,12 @@ fn expect_key_string_value(
     attr: &Attribute,
 ) -> Result<rustc_span::Symbol, ErrorGuaranteed> {
     let span = attr.span;
-    let AttrArgs::Eq { eq_span: _, value } = &attr.get_normal_item().args else {
+    let AttrArgs::Eq { expr, .. } = &attr.get_normal_item().args else {
         return Err(sess
             .dcx()
             .span_err(span, "Expected attribute of the form #[attr = \"value\"]"));
     };
-    let maybe_str = match value {
-        AttrArgsEq::Ast(expr) => {
-            if let ExprKind::Lit(tok) = expr.kind {
-                match LitKind::from_token_lit(tok) {
-                    Ok(l) => l.str(),
-                    Err(err) => {
-                        return Err(sess.dcx().span_err(
-                            span,
-                            format!("Invalid string literal on right hand side of `=` {err:?}"),
-                        ));
-                    }
-                }
-            } else {
-                return Err(sess
-                    .dcx()
-                    .span_err(span, "Expected literal string as right hand side of `=`"));
-            }
-        }
-        AttrArgsEq::Hir(lit) => lit.kind.str(),
-    };
+    let maybe_str = expr.kind.str();
     if let Some(str) = maybe_str {
         Ok(str)
     } else {
@@ -841,7 +820,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
     attributes
         .iter()
         .filter_map(|attr| {
-            let paths = parse_paths(attr).unwrap_or_else(|_| {
+            let paths = parse_paths(tcx, attr).unwrap_or_else(|_| {
                 tcx.dcx().span_err(
                     attr.span,
                     format!(
@@ -952,8 +931,8 @@ fn parse_integer(attr: &Attribute) -> Option<u128> {
 /// Extracts a vector with the path arguments of an attribute.
 ///
 /// Emits an error if it couldn't convert any of the arguments and return an empty vector.
-fn parse_paths(attr: &Attribute) -> Result<Vec<TypePath>, syn::Error> {
-    let syn_attr = syn_attr(attr);
+fn parse_paths(tcx: TyCtxt, attr: &Attribute) -> Result<Vec<TypePath>, syn::Error> {
+    let syn_attr = syn_attr(tcx, attr);
     let parser = Punctuated::<TypePath, syn::Token![,]>::parse_terminated;
     let paths = syn_attr.parse_args_with(parser)?;
     Ok(paths.into_iter().collect())
@@ -990,11 +969,11 @@ fn parse_str_value(attr: &Attribute) -> Option<String> {
 fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
     match &attr.kind {
         AttrKind::Normal(normal) => {
-            let segments = &normal.item.path.segments;
-            if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" {
+            let segments = &normal.path.segments;
+            if (!segments.is_empty()) && segments[0].as_str() == "kanitool" {
                 let ident_str = segments[1..]
                     .iter()
-                    .map(|segment| segment.ident.as_str())
+                    .map(|segment| segment.as_str())
                     .intersperse("::")
                     .collect::<String>();
                 KaniAttributeKind::try_from(ident_str.as_str())
@@ -1014,8 +993,8 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
 /// Parse an attribute using `syn`.
 ///
 /// This provides a user-friendly interface to manipulate than the internal compiler AST.
-fn syn_attr(attr: &Attribute) -> syn::Attribute {
-    let attr_str = rustc_ast_pretty::pprust::attribute_to_string(attr);
+fn syn_attr(tcx: TyCtxt, attr: &Attribute) -> syn::Attribute {
+    let attr_str = rustc_hir_pretty::attribute_to_string(&tcx, attr);
     let parser = syn::Attribute::parse_outer;
     parser.parse_str(&attr_str).unwrap().pop().unwrap()
 }

kani-compiler/src/main.rs

@@ -25,6 +25,7 @@ extern crate rustc_data_structures;
 extern crate rustc_driver;
 extern crate rustc_errors;
 extern crate rustc_hir;
+extern crate rustc_hir_pretty;
 extern crate rustc_index;
 extern crate rustc_interface;
 extern crate rustc_metadata;

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-12-15"
+channel = "nightly-2024-12-18"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/uninit/delayed-ub/expected

@@ -1,44 +1,44 @@
-delayed_ub_trigger_copy.assertion.1\
+delayed_ub_trigger_copy.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\
 
-delayed_ub_slices.assertion.4\
+delayed_ub_slices.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`"
 
-delayed_ub_structs.assertion.2\
+delayed_ub_structs.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`"
 
-delayed_ub_double_copy.assertion.1\
+delayed_ub_double_copy.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\
 
-delayed_ub_copy.assertion.1\
+delayed_ub_copy.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_closure_capture_laundered.assertion.2\
+delayed_ub_closure_capture_laundered.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_closure_laundered.assertion.2\
+delayed_ub_closure_laundered.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_laundered.assertion.2\
+delayed_ub_laundered.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_static.assertion.4\
+delayed_ub_static.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub_transmute.assertion.2\
+delayed_ub_transmute.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-delayed_ub.assertion.2\
+delayed_ub.assertion.\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"