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_field_attribute(attr: &syn::Attribute) -> bool {
113    if let Meta::List(ml) = &attr.meta {
114        !(matches!(expects_refine(&ml.path), Ok(Some(_)))
115            || matches!(expects_order(&ml.path), Ok(Some(_))))
116    } else {
117        true
118    }
119}
120
121#[proc_macro_attribute]
122pub fn attributes(_attr: TokenStream, item: TokenStream) -> TokenStream {
123    let item: Item = parse_macro_input!(item);
124
125    struct AttrVisitor;
126
127    use syn::visit_mut;
128    impl VisitMut for AttrVisitor {
129        fn visit_item_trait_mut(&mut self, item: &mut ItemTrait) {
130            for ti in item.items.iter_mut() {
131                if let TraitItem::Fn(fun) = ti {
132                    fun.attrs.retain(not_hax_attribute)
133                }
134            }
135            visit_mut::visit_item_trait_mut(self, item);
136        }
137        fn visit_type_mut(&mut self, _type: &mut Type) {}
138        fn visit_item_impl_mut(&mut self, item: &mut ItemImpl) {
139            for ii in item.items.iter_mut() {
140                if let ImplItem::Fn(fun) = ii {
141                    fun.attrs.retain(not_hax_attribute)
142                }
143            }
144            visit_mut::visit_item_impl_mut(self, item);
145        }
146        fn visit_item_mut(&mut self, item: &mut Item) {
147            visit_mut::visit_item_mut(self, item);
148
149            match item {
150                Item::Struct(s) => {
151                    for field in s.fields.iter_mut() {
152                        field.attrs.retain(not_field_attribute)
153                    }
154                }
155                _ => (),
156            }
157        }
158    }
159
160    let mut item = item;
161    AttrVisitor.visit_item_mut(&mut item);
162
163    quote! { #item }.into()
164}
165
166#[proc_macro]
167pub fn int(payload: TokenStream) -> TokenStream {
168    let mut tokens = payload.into_iter().peekable();
169    let negative = matches!(tokens.peek(), Some(TokenTree::Punct(p)) if p.as_char() == '-');
170    if negative {
171        tokens.next();
172    }
173    let [lit @ TokenTree::Literal(_)] = &tokens.collect::<Vec<_>>()[..] else {
174        return quote! { ::std::compile_error!("Expected exactly one numeric literal") }.into();
175    };
176    let lit: proc_macro2::TokenStream = TokenStream::from(lit.clone()).into();
177    quote! {::hax_lib::int::Int(#lit)}.into()
178}
179
180#[proc_macro_attribute]
181pub fn impl_fn_decoration(_attr: TokenStream, _item: TokenStream) -> TokenStream {
182    quote! { ::std::compile_error!("`impl_fn_decoration` is an internal macro and should never be used directly.") }.into()
183}
184
185#[proc_macro_attribute]
186pub fn trait_fn_decoration(_attr: TokenStream, _item: TokenStream) -> TokenStream {
187    quote! { ::std::compile_error!("`trait_fn_decoration` is an internal macro and should never be used directly.") }.into()
188}
189
190#[proc_macro]
191pub fn loop_invariant(_predicate: TokenStream) -> TokenStream {
192    quote! {}.into()
193}
194
195#[proc_macro]
196pub fn loop_decreases(_predicate: TokenStream) -> TokenStream {
197    quote! {}.into()
198}
hax_lib_macros/dummy.rs

hax_lib_macros/
dummy.rs
