diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 00160a0db1a0..549fbcf3447d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/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; diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 017266717de7..83893da0707d 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/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 { 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 Option { /// 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, syn::Error> { - let syn_attr = syn_attr(attr); +fn parse_paths(tcx: TyCtxt, attr: &Attribute) -> Result, syn::Error> { + let syn_attr = syn_attr(tcx, attr); let parser = Punctuated::::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 { fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { 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::(); KaniAttributeKind::try_from(ident_str.as_str()) @@ -1014,8 +993,8 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { /// 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() } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 65f1a22852b7..6f108595dbfc 100644 --- a/kani-compiler/src/main.rs +++ b/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; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 62deebf7a7d2..506443c043ca 100644 --- a/rust-toolchain.toml +++ b/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"] diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected index dc0411bdba9c..b7c139c2d101 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/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`"