use syn::visit::Visit;
use crate::prelude::*;
use crate::rewrite_self::*;
pub struct HaxQuantifiers;
impl ToTokens for HaxQuantifiers {
fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) {
quote! {
use ::hax_lib::fstar::prop as fstar;
use ::hax_lib::coq::prop as coq;
use ::hax_lib::legacy_lean::prop as lean;
use ::hax_lib::proverif::prop as proverif;
}
.to_tokens(tokens)
}
}
pub enum FnDecorationKind {
Requires,
Ensures { ret_binder: Pat, by_ref: bool },
Decreases,
SMTPat,
}
impl ToString for FnDecorationKind {
fn to_string(&self) -> String {
match self {
FnDecorationKind::Requires => "requires".to_string(),
FnDecorationKind::Ensures { .. } => "ensures".to_string(),
FnDecorationKind::Decreases { .. } => "decreases".to_string(),
FnDecorationKind::SMTPat { .. } => "SMTPat".to_string(),
}
}
}
impl From<FnDecorationKind> for AssociationRole {
fn from(kind: FnDecorationKind) -> Self {
match &kind {
FnDecorationKind::Requires => AssociationRole::Requires,
FnDecorationKind::Ensures { .. } => AssociationRole::Ensures,
FnDecorationKind::Decreases => AssociationRole::Decreases,
FnDecorationKind::SMTPat => AssociationRole::SMTPat,
}
}
}
pub(crate) fn self_trait_path(item: &ItemTrait) -> Path {
let args: Vec<GenericArgument> = item
.generics
.params
.iter()
.map(|param| match param {
GenericParam::Lifetime(lt) => GenericArgument::Lifetime(lt.lifetime.clone()),
GenericParam::Type(ty) => {
let ident = &ty.ident;
GenericArgument::Type(parse_quote! {#ident})
}
GenericParam::Const(c) => {
let ident = &c.ident;
GenericArgument::Const(parse_quote! {#ident})
}
})
.collect();
let ident = &item.ident;
if args.is_empty() {
parse_quote! {#ident}
} else {
parse_quote! {#ident<#(#args),*>}
}
}
pub(crate) fn impl_fn_decoration_args(
decoration: &Ident,
generics: &Generics,
self_ty: &Type,
as_trait: &Option<TokenStream>,
tokens: &TokenStream,
) -> TokenStream {
let where_clause = &generics.where_clause;
quote! {#decoration, #generics, #where_clause, #self_ty #as_trait, #tokens}
}
pub(crate) fn visit_meta_through_cfg_attr(
meta: &mut Meta,
cfg: Option<Meta>,
f: &mut impl FnMut(&mut Meta, Option<&Meta>),
) {
let is_cfg_attr = matches!(&*meta, Meta::List(ml) if ml.path.is_ident("cfg_attr"));
if !is_cfg_attr {
return f(meta, cfg.as_ref());
}
let Meta::List(ml) = meta else { unreachable!() };
let Ok(args) = ml.parse_args_with(punctuated::Punctuated::<Meta, Token![,]>::parse_terminated)
else {
return;
};
let mut args: Vec<Meta> = args.into_iter().collect();
let Some((pred, nested)) = args.split_first_mut() else {
return;
};
let cfg = match cfg {
Some(outer) => parse_quote! {all(#outer, #pred)},
None => pred.clone(),
};
for meta in nested {
visit_meta_through_cfg_attr(meta, Some(cfg.clone()), f);
}
ml.tokens = quote! {#(#args),*};
}
pub(crate) fn cfg_gate(tokens: TokenStream, pred: &Meta) -> TokenStream {
let Ok(file) = syn::parse2::<File>(tokens.clone()) else {
return quote! {#[cfg(#pred)] const _: () = {#tokens};};
};
file.items
.iter()
.map(|item| quote! {#[cfg(#pred)] #item})
.collect()
}
pub(crate) fn charon_attr(name: TokenStream) -> Option<TokenStream> {
cfg!(charon).then(|| quote! {#[charon::#name]})
}
pub(crate) fn future_args_last() -> bool {
cfg!(hax_backend_lean)
}
pub(crate) fn pad_nullary_sig() -> bool {
!cfg!(hax_backend_lean)
}
pub(crate) fn merge_generics(x: Generics, y: Generics) -> Generics {
Generics {
lt_token: x.lt_token.or(y.lt_token),
gt_token: x.gt_token.or(y.gt_token),
params: {
let lts = x
.lifetimes()
.chain(y.lifetimes())
.cloned()
.map(GenericParam::Lifetime);
let not_lts = x
.params
.clone()
.into_iter()
.filter(|p| !matches!(p, GenericParam::Lifetime(_)))
.chain(
y.params
.clone()
.into_iter()
.filter(|p| !matches!(p, GenericParam::Lifetime(_))),
);
lts.chain(not_lts).collect()
},
where_clause: match (x.where_clause, y.where_clause) {
(Some(wx), Some(wy)) => Some(syn::WhereClause {
where_token: wx.where_token,
predicates: wx.predicates.into_iter().chain(wy.predicates).collect(),
}),
(Some(w), None) | (None, Some(w)) => Some(w),
(None, None) => None,
},
}
}
fn unmut_references_in_inputs(sig: &mut Signature) -> Vec<FnArg> {
let mut mutable_inputs = vec![];
for input in &mut sig.inputs {
if let Some(mutability) = match input {
FnArg::Receiver(syn::Receiver {
reference: Some(_),
mutability,
..
}) => Some(mutability),
FnArg::Typed(syn::PatType { ty, .. }) => {
use std::borrow::BorrowMut;
if let syn::Type::Reference(syn::TypeReference { mutability, .. }) = ty.borrow_mut()
{
Some(mutability)
} else {
None
}
}
_ => None,
} {
if mutability.is_some() {
*mutability = None;
mutable_inputs.push(input.clone());
}
}
}
mutable_inputs
}
fn expect_fn_arg_var_pat(arg: &FnArg) -> Option<(String, syn::Type)> {
match arg {
FnArg::Receiver(recv) => Some(("self".into(), *recv.ty.clone())),
FnArg::Typed(pat_type) => match &*pat_type.pat {
syn::Pat::Wild(_) => Some(("".into(), *pat_type.ty.clone())),
syn::Pat::Ident(pat_ident) => {
Some((format!("{}", pat_ident.ident), *pat_type.ty.clone()))
}
_ => None,
},
}
}
pub(crate) enum NotFutureExpr {
BadNumberOfArgs,
ArgNotIdent,
}
pub(crate) fn expect_future_expr(e: &Expr) -> Option<std::result::Result<Ident, NotFutureExpr>> {
if let Expr::Call(call) = e {
if call.func.is_ident("future") {
return Some(match call.args.iter().collect::<Vec<_>>().as_slice() {
[arg] => arg.expect_ident().ok_or(NotFutureExpr::ArgNotIdent),
_ => Err(NotFutureExpr::BadNumberOfArgs),
});
}
}
None
}
#[derive(Default)]
pub struct IdentCollector {
pub idents: Vec<Ident>,
}
impl<'ast> syn::visit::Visit<'ast> for IdentCollector {
fn visit_ident(&mut self, ident: &'ast Ident) {
self.idents.push(ident.clone());
}
}
impl IdentCollector {
pub fn fresh_ident(&self, prefix: &str) -> Ident {
let idents: HashSet<&Ident> = HashSet::from_iter(self.idents.iter());
let mk = |s| Ident::new(s, Span::call_site());
std::iter::once(mk(prefix))
.chain((0u64..).map(|i| Ident::new(&format!("{}{}", prefix, i), Span::call_site())))
.find(|ident| !idents.contains(ident))
.unwrap()
}
}
struct RewriteFuture(HashSet<String>);
impl VisitMut for RewriteFuture {
fn visit_expr_mut(&mut self, e: &mut Expr) {
syn::visit_mut::visit_expr_mut(self, e);
let error = match expect_future_expr(e) {
Some(Ok(arg)) => {
let arg = format!("{}", arg);
if self.0.contains(&arg) {
let arg = create_future_ident(&arg);
*e = parse_quote! {#arg};
return;
}
Some(format!(
"Cannot find an input `{arg}` of type `&mut _`. In the context, `future` can be called on the following inputs: {:?}.",
self.0
))
}
Some(Err(error_kind)) => {
let message = match error_kind {
NotFutureExpr::BadNumberOfArgs => {
"`future` can only be called with one argument: a `&mut` input name"
}
NotFutureExpr::ArgNotIdent => {
"`future` can only be called with an `&mut` input name"
}
};
let help_message = match self.0.iter().next() {
None => " In the context, there is no `&mut` input.".to_string(),
Some(var) => {
format!(" For example, in the context you can write `future({var})`.")
}
};
Some(format!("{message}.{}", help_message))
}
None => None,
};
if let Some(error) = error {
*e = parse_quote! {::std::compile_error!(#error)};
}
}
}
fn create_future_ident(name: &str) -> syn::Ident {
proc_macro2::Ident::new(&format!("{name}_future"), proc_macro2::Span::call_site())
}
fn add_unit_to_sig_if_needed(signature: &mut Signature) {
if signature.inputs.is_empty() && pad_nullary_sig() {
signature.inputs.push(parse_quote! {_: ()})
}
}
pub fn foreign_self_projection_error(sig: &Signature, assoc: &[String]) -> Option<TokenStream> {
struct Collector<'a> {
assoc: &'a [String],
errors: Vec<Error>,
}
impl<'ast> syn::visit::Visit<'ast> for Collector<'_> {
fn visit_type_path(&mut self, tp: &'ast TypePath) {
syn::visit::visit_type_path(self, tp);
let mut segments = tp.path.segments.iter();
let (Some(first), Some(assoc)) = (segments.next(), segments.next()) else {
return;
};
if tp.qself.is_some() || first.ident != "Self" {
return;
}
let name = assoc.ident.to_string();
if !self.assoc.contains(&name) {
self.errors.push(Error::new(
tp.span(),
format!(
"hax: `Self::{name}` is not defined by this `impl` block, hax cannot \
qualify it. Write `<Type as Trait>::{name}` explicitly. See \
https://github.com/cryspen/hax/issues/2089."
),
));
}
}
}
let mut collector = Collector {
assoc,
errors: Vec::new(),
};
syn::visit::Visit::visit_signature(&mut collector, sig);
let mut errors = collector.errors.into_iter();
let mut error = errors.next()?;
for other in errors {
error.combine(other);
}
Some(error.to_compile_error())
}
pub fn make_fn_decoration(
mut phi: Expr,
mut signature: Signature,
kind: FnDecorationKind,
mut generics: Option<Generics>,
self_type: Option<Type>,
self_projection: SelfProjection,
) -> (TokenStream, AttrPayload) {
let self_ident: Ident = {
let mut idents = IdentCollector::default();
idents.visit_expr(&phi);
idents.visit_signature(&signature);
idents.fresh_ident("self_")
};
let error = {
let mut rewriter = RewriteSelf::new(self_ident, self_type, self_projection);
rewriter.visit_expr_mut(&mut phi);
rewriter.visit_signature_mut(&mut signature);
if let Some(generics) = generics.as_mut() {
rewriter.visit_generics_mut(generics);
}
rewriter.get_error()
};
let uid = ItemUid::fresh();
let mut_ref_inputs = unmut_references_in_inputs(&mut signature);
let decoration = {
let decoration_sig = {
let mut sig = signature.clone();
sig.ident = format_ident!("{}", kind.to_string());
if let FnDecorationKind::Ensures { ret_binder, by_ref } = &kind {
add_unit_to_sig_if_needed(&mut sig);
let output_typ = match sig.output {
syn::ReturnType::Default => parse_quote! {()},
syn::ReturnType::Type(_, t) => t,
};
let output_typ_tokens = if *by_ref {
quote! {&#output_typ}
} else {
quote! {#output_typ}
};
let mut_ref_inputs = mut_ref_inputs
.iter()
.map(|mut_ref_input| {
expect_fn_arg_var_pat(mut_ref_input).expect(
"Every `&mut` input of a function annotated with a `ensures` clause is expected to be a simple variable pattern.",
)
});
let mut rewrite_future =
RewriteFuture(mut_ref_inputs.clone().map(|x| x.0).collect());
rewrite_future.visit_expr_mut(&mut phi);
let (mut pats, mut tys): (Vec<_>, Vec<_>) = mut_ref_inputs
.map(|(name, ty)| {
(
create_future_ident(&name).to_token_stream(),
ty.to_token_stream(),
)
})
.unzip();
let is_output_typ_unit = if let syn::Type::Tuple(tuple) = &*output_typ {
tuple.elems.is_empty()
} else {
false
};
if !is_output_typ_unit || pats.is_empty() {
if future_args_last() {
pats.insert(0, ret_binder.to_token_stream());
tys.insert(0, output_typ_tokens);
} else {
pats.push(ret_binder.to_token_stream());
tys.push(output_typ_tokens);
}
}
sig.inputs
.push(syn::parse_quote! {(#(#pats),*): (#(#tys),*)});
}
if let Some(generics) = generics {
sig.generics = merge_generics(generics, sig.generics);
}
sig.output = match &kind {
FnDecorationKind::Decreases | FnDecorationKind::SMTPat => {
syn::parse_quote! { -> () }
}
_ => syn::parse_quote! { -> impl core::convert::Into<::hax_lib::Prop> },
};
sig
};
let uid_attr = AttrPayload::Uid(uid.clone());
let late_skip = &AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
if let FnDecorationKind::Decreases | FnDecorationKind::SMTPat = &kind {
phi = parse_quote! {::hax_lib::any_to_unit(#phi)};
};
let quantifiers = if let FnDecorationKind::Decreases = &kind {
None
} else {
Some(HaxQuantifiers)
};
let future = if let FnDecorationKind::Ensures { .. } = &kind {
quote! { #late_skip #AttrHaxLang fn future<T>(x: &mut T) -> &T { x } }
} else {
quote! {}
};
use AttrPayload::NeverErased;
quote! {
#[cfg(#DebugOrHaxCfgExpr)]
#late_skip
const _: () = {
#quantifiers
#future
#uid_attr
#late_skip
#[allow(unused)]
#NeverErased
#decoration_sig {
#phi
}
};
}
};
let assoc_attr = AttrPayload::AssociatedItem {
role: kind.into(),
item: uid,
};
let decoration = match error {
Some(error) => error,
None => decoration,
};
(decoration, assoc_attr)
}