Skip to content

Commit

Permalink
Upgrade toolchain to nightly-2024-12-18 (#3794)
Browse files Browse the repository at this point in the history
Relevant upstream PR: rust-lang/rust#131808.
This required replacing `rustc_ast::Attribute` with the new
`rustc_hir::Attribute`.

Resolves #3788 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
zhassan-aws authored Dec 26, 2024
1 parent f212ce5 commit 33b74e0
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 46 deletions.
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
45 changes: 12 additions & 33 deletions kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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!(
Expand Down Expand Up @@ -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())
Expand Down Expand Up @@ -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())
Expand All @@ -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()
}
Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
22 changes: 11 additions & 11 deletions tests/expected/uninit/delayed-ub/expected
Original file line number Diff line number Diff line change
@@ -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`"

Expand Down

0 comments on commit 33b74e0

Please sign in to comment.