hax_lib_macros/
dummy.rs

1mod hax_paths;
2
3use hax_paths::*;
4use proc_macro::{TokenStream, TokenTree};
5use quote::quote;
6use syn::{visit_mut::VisitMut, *};
7
8macro_rules! identity_proc_macro_attribute {
9    ($($name:ident,)*) => {
10        $(
11            #[proc_macro_attribute]
12            pub fn $name(_attr: TokenStream, item: TokenStream) -> TokenStream {
13                item
14            }
15        )*
16    }
17}
18
19identity_proc_macro_attribute!(
20    fstar_options,
21    fstar_verification_status,
22    include,
23    exclude,
24    requires,
25    ensures,
26    decreases,
27    pv_handwritten,
28    pv_constructor,
29    protocol_messages,
30    process_init,
31    process_write,
32    process_read,
33    opaque,
34    opaque_type,
35    transparent,
36    refinement_type,
37    fstar_replace,
38    coq_replace,
39    proverif_replace,
40    fstar_replace_body,
41    coq_replace_body,
42    proverif_replace_body,
43    fstar_before,
44    coq_before,
45    proverif_before,
46    fstar_after,
47    coq_after,
48    proverif_after,
49    fstar_smt_pat,
50    fstar_postprocess_with,
51);
52
53#[proc_macro]
54pub fn fstar_expr(_payload: TokenStream) -> TokenStream {
55    quote! { () }.into()
56}
57#[proc_macro]
58pub fn coq_expr(_payload: TokenStream) -> TokenStream {
59    quote! { () }.into()
60}
61#[proc_macro]
62pub fn proverif_expr(_payload: TokenStream) -> TokenStream {
63    quote! { () }.into()
64}
65
66#[proc_macro_attribute]
67pub fn lemma(_attr: TokenStream, _item: TokenStream) -> TokenStream {
68    quote! {}.into()
69}
70
71fn unsafe_expr() -> TokenStream {
72    // `*_unsafe_expr("<code>")` are macro generating a Rust expression of any type, that will be replaced by `<code>` in the backends.
73    // This should be used solely in hax-only contextes.
74    // If this macro is used, that means the user broke this rule.
75    quote! { ::std::compile_error!("`hax_lib::unsafe_expr` has no meaning outside of hax extraction, please use it solely on hax-only places.") }.into()
76}
77
78#[proc_macro]
79pub fn fstar_unsafe_expr(_payload: TokenStream) -> TokenStream {
80    unsafe_expr()
81}
82#[proc_macro]
83pub fn coq_unsafe_expr(_payload: TokenStream) -> TokenStream {
84    unsafe_expr()
85}
86#[proc_macro]
87pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream {
88    unsafe_expr()
89}
90
91#[proc_macro]
92pub fn fstar_prop_expr(_payload: TokenStream) -> TokenStream {
93    quote! {::hax_lib::Prop::from_bool(true)}.into()
94}
95#[proc_macro]
96pub fn coq_prop_expr(_payload: TokenStream) -> TokenStream {
97    quote! {::hax_lib::Prop::from_bool(true)}.into()
98}
99#[proc_macro]
100pub fn proverif_prop_expr(_payload: TokenStream) -> TokenStream {
101    quote! {::hax_lib::Prop::from_bool(true)}.into()
102}
103
104fn not_hax_attribute(attr: &syn::Attribute) -> bool {
105    if let Meta::List(ml) = &attr.meta {
106        !matches!(expects_path_decoration(&ml.path), Ok(Some(_)))
107    } else {
108        true
109    }
110}
111
112fn not_refine_attribute(attr: &syn::Attribute) -> bool {
113    if let Meta::List(ml) = &attr.meta {
114        !matches!(expects_refine(&ml.path), Ok(Some(_)))
115    } else {
116        true
117    }
118}
119
120#[proc_macro_attribute]
121pub fn attributes(_attr: TokenStream, item: TokenStream) -> TokenStream {
122    let item: Item = parse_macro_input!(item);
123
124    struct AttrVisitor;
125
126    use syn::visit_mut;
127    impl VisitMut for AttrVisitor {
128        fn visit_item_trait_mut(&mut self, item: &mut ItemTrait) {
129            for ti in item.items.iter_mut() {
130                if let TraitItem::Fn(fun) = ti {
131                    fun.attrs.retain(not_hax_attribute)
132                }
133            }
134            visit_mut::visit_item_trait_mut(self, item);
135        }
136        fn visit_type_mut(&mut self, _type: &mut Type) {}
137        fn visit_item_impl_mut(&mut self, item: &mut ItemImpl) {
138            for ii in item.items.iter_mut() {
139                if let ImplItem::Fn(fun) = ii {
140                    fun.attrs.retain(not_hax_attribute)
141                }
142            }
143            visit_mut::visit_item_impl_mut(self, item);
144        }
145        fn visit_item_mut(&mut self, item: &mut Item) {
146            visit_mut::visit_item_mut(self, item);
147
148            match item {
149                Item::Struct(s) => {
150                    for field in s.fields.iter_mut() {
151                        field.attrs.retain(not_refine_attribute)
152                    }
153                }
154                _ => (),
155            }
156        }
157    }
158
159    let mut item = item;
160    AttrVisitor.visit_item_mut(&mut item);
161
162    quote! { #item }.into()
163}
164
165#[proc_macro]
166pub fn int(payload: TokenStream) -> TokenStream {
167    let mut tokens = payload.into_iter().peekable();
168    let negative = matches!(tokens.peek(), Some(TokenTree::Punct(p)) if p.as_char() == '-');
169    if negative {
170        tokens.next();
171    }
172    let [lit @ TokenTree::Literal(_)] = &tokens.collect::<Vec<_>>()[..] else {
173        return quote! { ::std::compile_error!("Expected exactly one numeric literal") }.into();
174    };
175    let lit: proc_macro2::TokenStream = TokenStream::from(lit.clone()).into();
176    quote! {::hax_lib::int::Int(#lit)}.into()
177}
178
179#[proc_macro_attribute]
180pub fn impl_fn_decoration(_attr: TokenStream, _item: TokenStream) -> TokenStream {
181    quote! { ::std::compile_error!("`impl_fn_decoration` is an internal macro and should never be used directly.") }.into()
182}
183
184#[proc_macro_attribute]
185pub fn trait_fn_decoration(_attr: TokenStream, _item: TokenStream) -> TokenStream {
186    quote! { ::std::compile_error!("`trait_fn_decoration` is an internal macro and should never be used directly.") }.into()
187}
188
189#[proc_macro]
190pub fn loop_invariant(_predicate: TokenStream) -> TokenStream {
191    quote! {}.into()
192}
193
194#[proc_macro]
195pub fn loop_decreases(_predicate: TokenStream) -> TokenStream {
196    quote! {}.into()
197}
hax_lib_macros/dummy.rs

hax_lib_macros/
dummy.rs
