diff --git a/Cargo.lock b/Cargo.lock index 483cba85d985..4ee763df221c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1110,8 +1110,8 @@ dependencies = [ name = "kani_macros" version = "0.67.0" dependencies = [ - "proc-macro-error2", "proc-macro2", + "proc-macro2-diagnostics", "quote", "strum", "strum_macros", @@ -1675,34 +1675,24 @@ dependencies = [ ] [[package]] -name = "proc-macro-error-attr2" -version = "2.0.0" +name = "proc-macro2" +version = "1.0.106" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" dependencies = [ - "proc-macro2", - "quote", + "unicode-ident", ] [[package]] -name = "proc-macro-error2" -version = "2.0.1" +name = "proc-macro2-diagnostics" +version = "0.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" +checksum = "af066a9c399a26e020ada66a034357a868728e72cd426f3adcd35f80d88d88c8" dependencies = [ - "proc-macro-error-attr2", "proc-macro2", "quote", "syn", -] - -[[package]] -name = "proc-macro2" -version = "1.0.106" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" -dependencies = [ - "unicode-ident", + "version_check", ] [[package]] diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 1a0516844efc..49800d644ab0 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -13,7 +13,7 @@ proc-macro = true [dependencies] proc-macro2 = "1.0" -proc-macro-error2 = { version = "2.0.0", features = ["nightly"] } +proc-macro2-diagnostics = { version = "0.10", default-features = false } quote = "1.0.20" syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-traits"] } strum = "0.27.1" diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 388dd64057b1..80490a15987a 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -9,8 +9,8 @@ //! struct S; //! //! ``` -use proc_macro_error2::abort; use proc_macro2::{Ident, Span, TokenStream}; +use proc_macro2_diagnostics::{Diagnostic, Level}; use quote::{quote, quote_spanned}; use syn::spanned::Spanned; use syn::{ @@ -45,17 +45,24 @@ pub(crate) fn kani_path_spanned(span: Span) -> TokenStream { /// /// In order to support core, we check the `no_core` feature. pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream { - let trait_name = "Arbitrary"; let derive_item = parse_macro_input!(item as DeriveInput); + match expand_derive_arbitrary_impl(&derive_item) { + Ok(tokens) => tokens.into(), + Err(diagnostic) => diagnostic.emit_as_item_tokens().into(), + } +} + +fn expand_derive_arbitrary_impl(derive_item: &DeriveInput) -> Result { + let trait_name = "Arbitrary"; let item_name = &derive_item.ident; let kani_path = kani_path(); - let body = fn_any_body(item_name, &derive_item.data); + let body = fn_any_body(item_name, &derive_item.data)?; // Get the safety constraints (if any) to produce type-safe values - let safety_conds_opt = safety_conds_opt(item_name, &derive_item, trait_name); + let safety_conds_opt = safety_conds_opt(item_name, derive_item, trait_name)?; // Add a bound `T: Arbitrary` to every type parameter T. - let generics = add_trait_bound_arbitrary(derive_item.generics); + let generics = add_trait_bound_arbitrary(derive_item.generics.clone()); // Generate an expression to sum up the heap size of each field. let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); @@ -82,7 +89,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok } } }; - proc_macro::TokenStream::from(expanded) + Ok(expanded) } /// Add a bound `T: Arbitrary` to every type parameter T. @@ -109,16 +116,19 @@ fn add_trait_bound_arbitrary(mut generics: Generics) -> Generics { /// Self { x: kani::any(), y: kani::any() } /// } /// ``` -fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { +fn fn_any_body(ident: &Ident, data: &Data) -> Result { match data { - Data::Struct(struct_data) => init_symbolic_item(ident, &struct_data.fields), - Data::Enum(enum_data) => fn_any_enum(ident, enum_data), - Data::Union(_) => { - abort!(Span::call_site(), "Cannot derive `Arbitrary` for `{}` union", ident; - note = ident.span() => - "`#[derive(Arbitrary)]` cannot be used for unions such as `{}`", ident - ) - } + Data::Struct(struct_data) => Ok(init_symbolic_item(ident, &struct_data.fields)), + Data::Enum(enum_data) => Ok(fn_any_enum(ident, enum_data)), + Data::Union(_) => Err(Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive `Arbitrary` for `{ident}` union"), + ) + .span_note( + ident.span(), + format!("`#[derive(Arbitrary)]` cannot be used for unions such as `{ident}`"), + )), } } @@ -271,7 +281,7 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { /// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the /// `#[safety_constraint()]` attribute helper associated with a given field. /// Return `None` if the attribute isn't specified. -fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option { +fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Result, Diagnostic> { let name = &field.ident; let mut safety_helper_attr = None; @@ -287,24 +297,35 @@ fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option { let expr_args: Result = attr.parse_args(); // Check if there was an error parsing the arguments - if let Err(err) = expr_args { - abort!(Span::call_site(), "Cannot derive impl for `{}`", ident; - note = attr.span() => - "safety constraint in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err + let safety_expr = expr_args.map_err(|err| { + Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive impl for `{ident}`"), ) - } + .span_note( + attr.span(), + format!( + "safety constraint in field `{}` could not be parsed: {}", + name.as_ref().unwrap(), + err + ), + ) + })?; // Return the expression associated to the safety constraint - let safety_expr = expr_args.unwrap(); - Some(quote_spanned! {field.span()=> + Ok(Some(quote_spanned! {field.span()=> #safety_expr - }) + })) } else { - None + Ok(None) } } -fn parse_safety_expr_input(ident: &Ident, derive_input: &DeriveInput) -> Option { +fn parse_safety_expr_input( + ident: &Ident, + derive_input: &DeriveInput, +) -> Result, Diagnostic> { let name = ident; let mut safety_attr = None; @@ -320,20 +341,24 @@ fn parse_safety_expr_input(ident: &Ident, derive_input: &DeriveInput) -> Option< let expr_args: Result = attr.parse_args(); // Check if there was an error parsing the arguments - if let Err(err) = expr_args { - abort!(Span::call_site(), "Cannot derive impl for `{}`", ident; - note = attr.span() => - "safety constraint in `{}` could not be parsed: {}", name.to_string(), err + let safety_expr = expr_args.map_err(|err| { + Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive impl for `{ident}`"), ) - } + .span_note( + attr.span(), + format!("safety constraint in `{name}` could not be parsed: {err}"), + ) + })?; // Return the expression associated to the safety constraint - let safety_expr = expr_args.unwrap(); - Some(quote_spanned! {derive_input.span()=> + Ok(Some(quote_spanned! {derive_input.span()=> #safety_expr - }) + })) } else { - None + Ok(None) } } /// Generate the body of the function `any()` for enums. The cases are: @@ -398,28 +423,35 @@ fn safe_body_with_calls( item_name: &Ident, derive_input: &DeriveInput, trait_name: &str, -) -> TokenStream { - let safety_conds_opt = safety_conds_opt(item_name, derive_input, trait_name); +) -> Result { + let safety_conds_opt = safety_conds_opt(item_name, derive_input, trait_name)?; let safe_body_default = safe_body_default(item_name, &derive_input.data); if let Some(safety_conds) = safety_conds_opt { - quote! { #safe_body_default && #safety_conds } + Ok(quote! { #safe_body_default && #safety_conds }) } else { - safe_body_default + Ok(safe_body_default) } } pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::TokenStream { - let trait_name = "Invariant"; let derive_item = parse_macro_input!(item as DeriveInput); + match expand_derive_invariant_impl(&derive_item) { + Ok(tokens) => tokens.into(), + Err(diagnostic) => diagnostic.emit_as_item_tokens().into(), + } +} + +fn expand_derive_invariant_impl(derive_item: &DeriveInput) -> Result { + let trait_name = "Invariant"; let item_name = &derive_item.ident; let kani_path = kani_path(); - let safe_body = safe_body_with_calls(item_name, &derive_item, trait_name); + let safe_body = safe_body_with_calls(item_name, derive_item, trait_name)?; let field_refs = field_refs(item_name, &derive_item.data); // Add a bound `T: Invariant` to every type parameter T. - let generics = add_trait_bound_invariant(derive_item.generics); + let generics = add_trait_bound_invariant(derive_item.generics.clone()); // Generate an expression to sum up the heap size of each field. let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); @@ -433,7 +465,7 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok } } }; - proc_macro::TokenStream::from(expanded) + Ok(expanded) } /// Looks for `#[safety_constraint(...)]` attributes used in the struct or its @@ -444,38 +476,53 @@ fn safety_conds_opt( item_name: &Ident, derive_input: &DeriveInput, trait_name: &str, -) -> Option { +) -> Result, Diagnostic> { let has_item_safety_constraint = - has_item_safety_constraint(item_name, derive_input, trait_name); + has_item_safety_constraint(item_name, derive_input, trait_name)?; let has_field_safety_constraints = has_field_safety_constraints(item_name, &derive_input.data); if has_item_safety_constraint && has_field_safety_constraints { - abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, item_name; - note = item_name.span() => - "`#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously" + return Err(Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive `{trait_name}` for `{item_name}`"), ) + .span_note( + item_name.span(), + "`#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously" + .to_string(), + )); } if has_item_safety_constraint { - Some(safe_body_from_struct_attr(item_name, derive_input, trait_name)) + Ok(Some(safe_body_from_struct_attr(item_name, derive_input, trait_name)?)) } else if has_field_safety_constraints { - Some(safe_body_from_fields_attr(item_name, &derive_input.data, trait_name)) + Ok(Some(safe_body_from_fields_attr(item_name, &derive_input.data, trait_name)?)) } else { - None + Ok(None) } } -fn has_item_safety_constraint(ident: &Ident, derive_input: &DeriveInput, trait_name: &str) -> bool { +fn has_item_safety_constraint( + ident: &Ident, + derive_input: &DeriveInput, + trait_name: &str, +) -> Result { let safety_constraints_in_item = derive_input.attrs.iter().filter(|attr| attr.path().is_ident("safety_constraint")).count(); if safety_constraints_in_item > 1 { - abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident; - note = ident.span() => - "`#[safety_constraint(...)]` cannot be used more than once." + return Err(Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive `{trait_name}` for `{ident}`"), ) + .span_note( + ident.span(), + "`#[safety_constraint(...)]` cannot be used more than once.".to_string(), + )); } - safety_constraints_in_item == 1 + Ok(safety_constraints_in_item == 1) } fn has_field_safety_constraints(ident: &Ident, data: &Data) -> bool { @@ -514,14 +561,19 @@ fn safe_body_from_struct_attr( ident: &Ident, derive_input: &DeriveInput, trait_name: &str, -) -> TokenStream { +) -> Result { if !matches!(derive_input.data, Data::Struct(_)) { - abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident; - note = ident.span() => - "`#[safety_constraint(...)]` can only be used in structs" + return Err(Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive `{trait_name}` for `{ident}`"), ) + .span_note( + ident.span(), + "`#[safety_constraint(...)]` can only be used in structs".to_string(), + )); }; - parse_safety_expr_input(ident, derive_input).unwrap() + Ok(parse_safety_expr_input(ident, derive_input)?.unwrap()) } /// Parse the condition expressions in `#[safety_constraint()]` attached to struct @@ -544,48 +596,60 @@ fn safe_body_from_struct_attr( /// ``` /// which can be used by the `Arbitrary` and `Invariant` to generate and check /// type-safe values for the struct, respectively. -fn safe_body_from_fields_attr(ident: &Ident, data: &Data, trait_name: &str) -> TokenStream { +fn safe_body_from_fields_attr( + ident: &Ident, + data: &Data, + trait_name: &str, +) -> Result { match data { Data::Struct(struct_data) => safe_body_from_fields_attr_inner(ident, &struct_data.fields), - Data::Enum(_) => { - abort!(Span::call_site(), "Cannot derive `{}` for `{}` enum", trait_name, ident; - note = ident.span() => - "`#[derive(Invariant)]` cannot be used for enums such as `{}`", ident - ) - } - Data::Union(_) => { - abort!(Span::call_site(), "Cannot derive `{}` for `{}` union", trait_name, ident; - note = ident.span() => - "`#[derive(Invariant)]` cannot be used for unions such as `{}`", ident - ) - } + Data::Enum(_) => Err(Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive `{trait_name}` for `{ident}` enum"), + ) + .span_note( + ident.span(), + format!("`#[derive(Invariant)]` cannot be used for enums such as `{ident}`"), + )), + Data::Union(_) => Err(Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive `{trait_name}` for `{ident}` union"), + ) + .span_note( + ident.span(), + format!("`#[derive(Invariant)]` cannot be used for unions such as `{ident}`"), + )), } } /// Generates an expression resulting from the conjunction of conditions /// specified as safety constraints for each field. /// See `safe_body_from_fields_attr` for more details. -fn safe_body_from_fields_attr_inner(ident: &Ident, fields: &Fields) -> TokenStream { +fn safe_body_from_fields_attr_inner( + ident: &Ident, + fields: &Fields, +) -> Result { match fields { // Expands to the expression // ` && && ..` // where `` is the safety condition specified for the N-th field. Fields::Named(fields) => { - let safety_conds: Vec = - fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect(); - quote! { #(#safety_conds)&&* } - } - Fields::Unnamed(_) => { - quote! { - true - } + let safety_conds: Vec = fields + .named + .iter() + .filter_map(|field| parse_safety_expr(ident, field).transpose()) + .collect::>()?; + Ok(quote! { #(#safety_conds)&&* }) } + Fields::Unnamed(_) => Ok(quote! { + true + }), // Expands to the expression // `true` - Fields::Unit => { - quote! { - true - } - } + Fields::Unit => Ok(quote! { + true + }), } } diff --git a/library/kani_macros/src/derive_bounded.rs b/library/kani_macros/src/derive_bounded.rs index 301021d02b95..0a9cbeed105f 100644 --- a/library/kani_macros/src/derive_bounded.rs +++ b/library/kani_macros/src/derive_bounded.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use proc_macro_error2::abort; use proc_macro2::{Span, TokenStream}; +use proc_macro2_diagnostics::{Diagnostic, Level}; use quote::quote; use crate::derive::kani_path; @@ -43,13 +43,21 @@ pub(crate) fn expand_derive_bounded_arbitrary( item: proc_macro::TokenStream, ) -> proc_macro::TokenStream { let parsed = syn::parse_macro_input!(item as syn::DeriveInput); + match expand_derive_bounded_arbitrary_impl(&parsed) { + Ok(tokens) => tokens.into(), + Err(diagnostic) => diagnostic.emit_as_item_tokens().into(), + } +} +fn expand_derive_bounded_arbitrary_impl( + parsed: &syn::DeriveInput, +) -> Result { let constructor = match &parsed.data { syn::Data::Struct(data_struct) => { generate_type_constructor(quote!(Self), &data_struct.fields) } syn::Data::Enum(data_enum) => enum_constructor(&parsed.ident, data_enum), - syn::Data::Union(data_union) => union_constructor(&parsed.ident, data_union), + syn::Data::Union(data_union) => union_constructor(&parsed.ident, data_union)?, }; // add `T: Arbitrary` bounds for generics @@ -59,7 +67,7 @@ pub(crate) fn expand_derive_bounded_arbitrary( // generate the implementation let kani_path = kani_path(); - quote! { + Ok(quote! { impl #impl_generics #kani_path::BoundedArbitrary for #name #ty_generics #clauses { @@ -67,8 +75,7 @@ pub(crate) fn expand_derive_bounded_arbitrary( #constructor } } - } - .into() + }) } /// Generates the call to construct the given type like so: @@ -130,11 +137,19 @@ fn enum_constructor(ident: &syn::Ident, data_enum: &syn::DataEnum) -> TokenStrea } } -fn union_constructor(ident: &syn::Ident, _data_union: &syn::DataUnion) -> TokenStream { - abort!(Span::call_site(), "Cannot derive `BoundedArbitrary` for `{}` union", ident; - note = ident.span() => - "`#[derive(BoundedArbitrary)]` cannot be used for unions such as `{}`", ident +fn union_constructor( + ident: &syn::Ident, + _data_union: &syn::DataUnion, +) -> Result { + Err(Diagnostic::spanned( + Span::call_site(), + Level::Error, + format!("Cannot derive `BoundedArbitrary` for `{ident}` union"), ) + .span_note( + ident.span(), + format!("`#[derive(BoundedArbitrary)]` cannot be used for unions such as `{ident}`"), + )) } /// Generate the necessary generic parameter declarations and generic bounds for a diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 91fd3ded0cf1..80ae350a056b 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -14,7 +14,6 @@ mod derive_bounded; // proc_macro::quote is nightly-only, so we'll cobble things together instead use proc_macro::TokenStream; -use proc_macro_error2::proc_macro_error; #[cfg(kani_sysroot)] use sysroot as attr_impl; @@ -30,7 +29,6 @@ use regular as attr_impl; /// e.g. `#[kani::proof(schedule = kani::RoundRobin::default())]`. /// /// This will wrap the async function in a call to [`block_on_with_spawn`](https://model-checking.github.io/kani/crates/doc/kani/futures/fn.block_on_with_spawn.html) (see its documentation for more information). -#[proc_macro_error] #[proc_macro_attribute] pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::proof(attr, item) @@ -214,7 +212,6 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// y: i32, /// } /// ``` -#[proc_macro_error] #[proc_macro_derive(Arbitrary, attributes(safety_constraint))] pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) @@ -246,7 +243,6 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// /// Using `BoundedArbitrary` makes proofs incomplete. It is useful for increasing /// confidence that some code is correct, but does not prove that absolutely. -#[proc_macro_error] #[proc_macro_derive(BoundedArbitrary, attributes(bounded))] pub fn derive_bounded_arbitrary(item: TokenStream) -> TokenStream { derive_bounded::expand_derive_bounded_arbitrary(item) @@ -343,7 +339,6 @@ pub fn derive_bounded_arbitrary(item: TokenStream) -> TokenStream { /// y: i32, /// } /// ``` -#[proc_macro_error] #[proc_macro_derive(Invariant, attributes(safety_constraint))] pub fn derive_invariant(item: TokenStream) -> TokenStream { derive::expand_derive_invariant(item) @@ -465,7 +460,7 @@ pub fn loop_decreases(attr: TokenStream, item: TokenStream) -> TokenStream { /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] mod sysroot { - use proc_macro_error2::{abort, abort_call_site}; + use proc_macro2_diagnostics::{Diagnostic, Level}; mod contracts; mod loop_contracts; @@ -478,6 +473,7 @@ mod sysroot { use { quote::{format_ident, quote}, syn::parse::{Parse, ParseStream}, + syn::spanned::Spanned, syn::{ItemFn, parse_macro_input}, }; @@ -511,28 +507,65 @@ mod sysroot { schedule: Option, } - impl Parse for ProofOptions { + /// The syntactic parse of the arguments to `#[kani::proof(...)]`. + /// + /// Parsing is kept separate from validation so that a semantic error (an + /// unrecognized option) can be reported as a rich [`Diagnostic`] -- with + /// structured `help`/`note` sub-diagnostics -- at the proc-macro entry + /// point, rather than being flattened into a `syn::Error`. + enum RawProofOptions { + /// No arguments, e.g. `#[kani::proof]`. + Empty, + /// `#[kani::proof(schedule = )]`. + Schedule(syn::Expr), + /// An unrecognized leading option, e.g. `#[kani::proof(foo)]`. + Unknown(syn::Ident), + } + + impl Parse for RawProofOptions { fn parse(input: ParseStream) -> syn::Result { if input.is_empty() { - Ok(ProofOptions { schedule: None }) - } else { - let ident = input.parse::()?; - if ident != "schedule" { - abort_call_site!("`{}` is not a valid option for `#[kani::proof]`.", ident; - help = "did you mean `schedule`?"; - note = "for now, `schedule` is the only option for `#[kani::proof]`."; - ); - } - let _ = input.parse::()?; - let schedule = Some(input.parse::()?); - Ok(ProofOptions { schedule }) + return Ok(RawProofOptions::Empty); + } + let ident = input.parse::()?; + if ident != "schedule" { + // Consume the remaining tokens so that `syn::parse` does not + // also report trailing input; the unknown option is reported + // by `parse_proof_options`. + input.parse::()?; + return Ok(RawProofOptions::Unknown(ident)); } + input.parse::()?; + Ok(RawProofOptions::Schedule(input.parse::()?)) + } + } + + /// Parse and validate the arguments to `#[kani::proof(...)]`, reporting any + /// problem as a [`Diagnostic`]. + fn parse_proof_options(attr: TokenStream) -> Result { + match syn::parse::(attr).map_err(Diagnostic::from)? { + RawProofOptions::Empty => Ok(ProofOptions { schedule: None }), + RawProofOptions::Schedule(schedule) => Ok(ProofOptions { schedule: Some(schedule) }), + RawProofOptions::Unknown(ident) => Err(Diagnostic::spanned( + ident.span(), + Level::Error, + format!("`{ident}` is not a valid option for `#[kani::proof]`."), + ) + .help("did you mean `schedule`?".to_string()) + .note("for now, `schedule` is the only option for `#[kani::proof]`.".to_string())), } } pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { - let proof_options = parse_macro_input!(attr as ProofOptions); let fn_item = parse_macro_input!(item as ItemFn); + match proof_impl(attr, fn_item) { + Ok(tokens) => tokens, + Err(diagnostic) => diagnostic.emit_as_item_tokens().into(), + } + } + + fn proof_impl(attr: TokenStream, fn_item: ItemFn) -> Result { + let proof_options = parse_proof_options(attr)?; let attrs = fn_item.attrs; let vis = fn_item.vis; let sig = fn_item.sig; @@ -545,18 +578,21 @@ mod sysroot { if sig.asyncness.is_none() { if proof_options.schedule.is_some() { - abort_call_site!( - "`#[kani::proof(schedule = ...)]` can only be used with `async` functions."; - help = "did you mean to make this function `async`?"; - ); + return Err(Diagnostic::spanned( + proc_macro2::Span::call_site(), + Level::Error, + "`#[kani::proof(schedule = ...)]` can only be used with `async` functions." + .to_string(), + ) + .help("did you mean to make this function `async`?".to_string())); } // Adds `#[kanitool::proof]` and other attributes - quote!( + Ok(quote!( #kani_attributes #(#attrs)* #vis #sig #body ) - .into() + .into()) } else { // For async functions, it translates to a synchronous function that calls `kani::block_on`. // Specifically, it translates @@ -578,11 +614,13 @@ mod sysroot { // } // ``` if !sig.inputs.is_empty() { - abort!( - sig.inputs, - "`#[kani::proof]` cannot be applied to async functions that take arguments for now"; - help = "try removing the arguments"; - ); + return Err(Diagnostic::spanned( + sig.inputs.span(), + Level::Error, + "`#[kani::proof]` cannot be applied to async functions that take arguments for now" + .to_string(), + ) + .help("try removing the arguments".to_string())); } let mut modified_sig = sig.clone(); modified_sig.asyncness = None; @@ -593,7 +631,7 @@ mod sysroot { } else { quote!(kani::block_on(#fn_name())) }; - quote!( + Ok(quote!( #kani_attributes #(#attrs)* #vis #modified_sig { @@ -601,7 +639,7 @@ mod sysroot { #block_on_call } ) - .into() + .into()) } } diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs index 794bdd7df55c..f9fde4e4a953 100644 --- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs +++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs @@ -5,7 +5,7 @@ //! use proc_macro::TokenStream; -use proc_macro_error2::abort_call_site; +use proc_macro2_diagnostics::{Diagnostic, Level}; use quote::{format_ident, quote, quote_spanned}; use syn::punctuated::Punctuated; use syn::spanned::Spanned; @@ -566,14 +566,26 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { el.body.stmts = new_stmts.clone(); } _ => { - abort_call_site!("`#[kani::loop_invariant]` is now only supported for while-loops."; - note = "for now, loop contracts is only supported for while-loops."; + return Diagnostic::spanned( + proc_macro2::Span::call_site(), + Level::Error, + "`#[kani::loop_invariant]` is now only supported for while-loops.".to_string(), ) + .note("for now, loop contracts is only supported for while-loops.".to_string()) + .emit_as_item_tokens() + .into(); } }, - _ => abort_call_site!("`#[kani::loop_invariant]` is now only supported for while-loops."; - note = "for now, loop contracts is only supported for while-loops."; - ), + _ => { + return Diagnostic::spanned( + proc_macro2::Span::call_site(), + Level::Error, + "`#[kani::loop_invariant]` is now only supported for while-loops.".to_string(), + ) + .note("for now, loop contracts is only supported for while-loops.".to_string()) + .emit_as_item_tokens() + .into(); + } } let ret: TokenStream = if let Some(ForLoopExtraStmts { init_iter_stmt,