use crate::{
common::{HasAttributes, HasSignature},
extract_prusti_attributes, generate_spec_and_assertions,
span_overrider::SpanOverrider,
untyped::AnyFnItem,
ExternSpecKind, RewritableReceiver, SelfTypeRewriter,
};
use itertools::Itertools;
use proc_macro2::TokenStream;
use quote::{format_ident, quote, quote_spanned, ToTokens};
use syn::{
parse_quote_spanned, punctuated::Punctuated, spanned::Spanned, visit::Visit,
visit_mut::VisitMut, Expr, FnArg, GenericArgument, GenericParam, Pat, PatType, Token,
};
struct ElidedLifetimeCounter {
num_elided_lifetimes: u32,
}
impl ElidedLifetimeCounter {
fn new() -> ElidedLifetimeCounter {
ElidedLifetimeCounter {
num_elided_lifetimes: 0,
}
}
}
impl<'ast> syn::visit::Visit<'ast> for ElidedLifetimeCounter {
fn visit_receiver(&mut self, receiver: &syn::Receiver) {
if let Some((_, None)) = receiver.reference {
self.num_elided_lifetimes += 1;
}
}
fn visit_type_reference(&mut self, reference: &syn::TypeReference) {
if reference.lifetime.is_none() {
self.num_elided_lifetimes += 1;
}
}
}
fn has_multiple_elided_lifetimes(inputs: &Punctuated<FnArg, syn::token::Comma>) -> bool {
let mut visitor = ElidedLifetimeCounter::new();
for input in inputs {
visitor.visit_fn_arg(input);
}
visitor.num_elided_lifetimes > 1
}
fn returns_reference_with_elided_lifetime(return_type: &syn::ReturnType) -> bool {
let mut visitor = ElidedLifetimeCounter::new();
visitor.visit_return_type(return_type);
visitor.num_elided_lifetimes >= 1
}
fn with_explicit_lifetimes(sig: &syn::Signature) -> Option<syn::Signature> {
struct SelfLifetimeInserter {}
impl syn::visit_mut::VisitMut for SelfLifetimeInserter {
fn visit_type_reference_mut(&mut self, reference: &mut syn::TypeReference) {
reference.lifetime = parse_quote_spanned! {reference.span() => 'prusti_self_lifetime };
}
fn visit_receiver_mut(&mut self, receiver: &mut syn::Receiver) {
receiver.reference.as_mut().unwrap().1 =
parse_quote_spanned! {receiver.span() => 'prusti_self_lifetime };
}
}
if !returns_reference_with_elided_lifetime(&sig.output)
|| !has_multiple_elided_lifetimes(&sig.inputs)
{
return None;
}
let mut new_sig = sig.clone();
let mut inserter = SelfLifetimeInserter {};
new_sig.generics.params.insert(
0,
parse_quote_spanned! {new_sig.generics.params.span() => 'prusti_self_lifetime },
);
if let Some(syn::FnArg::Receiver(r)) = new_sig.inputs.first_mut() {
inserter.visit_receiver_mut(r)
}
inserter.visit_return_type_mut(&mut new_sig.output);
Some(new_sig)
}
pub(crate) fn generate_extern_spec_method_stub<T: HasSignature + HasAttributes + Spanned>(
method: &T,
self_type: &syn::Type,
self_type_trait: Option<&syn::TypePath>,
extern_spec_kind: ExternSpecKind,
) -> syn::Result<(syn::ImplItemMethod, Vec<syn::ImplItemMethod>)> {
let method_sig = method.sig();
let method_sig_span = method_sig.span();
let method_ident = &method_sig.ident;
let method_path: syn::ExprPath = match self_type_trait {
Some(self_type_as_trait) => parse_quote_spanned! {method_sig_span=>
<#self_type as #self_type_as_trait> :: #method_ident
},
None => parse_quote_spanned! {method_sig_span=>
<#self_type> :: #method_ident
},
};
let stub_method =
generate_extern_spec_function_stub(method, &method_path, extern_spec_kind, false, false);
let stub_method: syn::ImplItemMethod = syn::parse2(stub_method)?;
let mut stub_method = AnyFnItem::ImplMethod(stub_method);
let prusti_attributes = extract_prusti_attributes(&mut stub_method);
let (spec_items, generated_attributes) =
generate_spec_and_assertions(prusti_attributes, &stub_method)?;
let mut stub_method = stub_method.expect_impl_item();
stub_method.attrs.extend(generated_attributes);
stub_method.rewrite_self_type(self_type, self_type_trait);
stub_method.rewrite_receiver(self_type);
syn::visit_mut::visit_impl_item_method_mut(
&mut SpanOverrider::new(method_sig_span),
&mut stub_method,
);
let rewritten_spec_items = spec_items.into_iter().map(|spec_item| {
match spec_item {
syn::Item::Fn(spec_item_fn) => {
let mut spec_item_fn: syn::ImplItemMethod = parse_quote_spanned! {spec_item_fn.span()=>
#spec_item_fn
};
spec_item_fn.rewrite_self_type(self_type, self_type_trait);
spec_item_fn.rewrite_receiver(self_type);
spec_item_fn
}
_ => unreachable!(),
}
}).collect::<Vec<_>>();
Ok((stub_method, rewritten_spec_items))
}
pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttributes + Spanned>(
function: &Input,
fn_path: &syn::ExprPath,
extern_spec_kind: ExternSpecKind,
mangle_name: bool,
is_unsafe: bool,
) -> TokenStream {
let signature = function.sig();
let mut signature = with_explicit_lifetimes(signature).unwrap_or_else(|| signature.clone());
if mangle_name {
signature.ident = format_ident!("prusti_extern_spec_{}", signature.ident);
}
let attrs = function.attrs().clone();
let generic_params = &signature.generic_params_as_call_args();
let args = &signature.params_as_call_args();
let extern_spec_kind_string: String = extern_spec_kind.into();
let fn_call = quote! { #fn_path :: < #generic_params > ( #args ) };
let stub_body = if is_unsafe {
quote! { unsafe { #fn_call } }
} else {
quote! { #fn_call }
};
quote_spanned! {function.span()=>
#[trusted]
#[prusti::extern_spec = #extern_spec_kind_string]
#(#attrs)*
#[allow(unused, dead_code)]
#signature {
#stub_body
}
}
}
pub trait MethodParamsAsCallArguments {
fn params_as_call_args(&self) -> Punctuated<Expr, Token![,]>;
}
impl<H: HasSignature> MethodParamsAsCallArguments for H {
fn params_as_call_args(&self) -> Punctuated<Expr, Token!(,)> {
self.sig().inputs.params_as_call_args()
}
}
impl MethodParamsAsCallArguments for Punctuated<FnArg, Token![,]> {
fn params_as_call_args(&self) -> Punctuated<Expr, Token!(,)> {
Punctuated::from_iter(self.iter().map(|param| -> Expr {
let span = param.span();
match param {
FnArg::Typed(PatType {
pat: box Pat::Ident(ident),
..
}) => parse_quote_spanned! {span=>#ident },
FnArg::Receiver(_) => parse_quote_spanned! {span=>self},
_ => unimplemented!(),
}
}))
}
}
pub trait GenericParamsAsCallArguments {
fn generic_params_as_call_args(&self) -> Punctuated<GenericArgument, Token![,]>;
}
impl<H: HasSignature> GenericParamsAsCallArguments for H {
fn generic_params_as_call_args(&self) -> Punctuated<GenericArgument, Token!(,)> {
self.sig().generics.params.generic_params_as_call_args()
}
}
impl GenericParamsAsCallArguments for Punctuated<GenericParam, Token![,]> {
fn generic_params_as_call_args(&self) -> Punctuated<GenericArgument, Token!(,)> {
use syn::*;
Punctuated::from_iter(self.iter().flat_map(|param| -> Option<GenericArgument> {
let span = param.span();
match param {
GenericParam::Type(TypeParam { ident, .. }) => {
Some(parse_quote_spanned! {span=>#ident })
}
GenericParam::Lifetime(_) => None,
GenericParam::Const(ConstParam { ident, .. }) => {
Some(parse_quote_spanned! {span=>#ident })
}
}
}))
}
}
pub fn add_phantom_data_for_generic_params(item_struct: &mut syn::ItemStruct) {
let fields = item_struct
.generics
.params
.iter()
.flat_map(|param| match param {
syn::GenericParam::Type(tp) => {
let ident = tp.ident.clone();
Some(quote!(::core::marker::PhantomData<#ident>))
}
syn::GenericParam::Lifetime(ld) => {
let ident = ld.lifetime.clone();
Some(quote!(&#ident ::core::marker::PhantomData<()>))
}
syn::GenericParam::Const(_cp) => None,
});
item_struct.fields = syn::Fields::Unnamed(syn::parse_quote! { ( #(#fields),* ) });
}
pub fn rewrite_generics(gens: &syn::Generics) -> syn::AngleBracketedGenericArguments {
let args: Vec<syn::GenericArgument> = gens
.params
.clone()
.into_iter()
.map(|gp| {
let ts = match gp {
syn::GenericParam::Type(syn::TypeParam { ident, .. })
| syn::GenericParam::Const(syn::ConstParam { ident, .. }) => {
ident.into_token_stream()
}
syn::GenericParam::Lifetime(ld) => ld.lifetime.into_token_stream(),
};
syn::parse2::<syn::GenericArgument>(ts).unwrap()
})
.collect();
syn::parse_quote! { < #(#args),* > }
}
pub(super) fn check_is_stub(block: &syn::Block) -> Result<(), syn::Error> {
if is_stub(block) {
Ok(())
} else {
Err(syn::Error::new(
block.span(),
"Unexpected method body. (Extern specs only define specifications.)",
))
}
}
fn is_stub(block: &syn::Block) -> bool {
if let Ok(Some(syn::Stmt::Item(syn::Item::Verbatim(tokens)))) = block.stmts.iter().at_most_one()
{
tokens.to_string() == ";"
} else {
false
}
}