creusot_contracts_dummy/
lib.rs

1extern crate proc_macro;
2
3mod ghost;
4
5use proc_macro::TokenStream as TS1;
6use quote::ToTokens as _;
7use syn::visit_mut::VisitMut;
8
9#[proc_macro_attribute]
10pub fn requires(_: TS1, tokens: TS1) -> TS1 {
11    let mut item = syn::parse_macro_input!(tokens as syn::ImplItemFn);
12    delete_invariants(&mut item);
13    TS1::from(item.into_token_stream())
14}
15
16#[proc_macro_attribute]
17pub fn ensures(_: TS1, tokens: TS1) -> TS1 {
18    let mut item = syn::parse_macro_input!(tokens as syn::ImplItemFn);
19    delete_invariants(&mut item);
20    TS1::from(item.into_token_stream())
21}
22
23#[proc_macro_attribute]
24pub fn variant(_: TS1, tokens: TS1) -> TS1 {
25    tokens
26}
27
28#[proc_macro_attribute]
29pub fn invariant(_: TS1, tokens: TS1) -> TS1 {
30    tokens
31}
32
33#[proc_macro]
34pub fn proof_assert(_: TS1) -> TS1 {
35    TS1::new()
36}
37
38#[proc_macro]
39pub fn snapshot(_: TS1) -> TS1 {
40    quote::quote! { ::creusot_contracts::snapshot::Snapshot::from_fn(|| std::process::abort()) }
41        .into()
42}
43
44#[proc_macro]
45pub fn ghost(body: TS1) -> TS1 {
46    let body = proc_macro2::TokenStream::from(ghost::ghost_preprocess(body));
47    quote::quote! { ::creusot_contracts::ghost::GhostBox::from_fn(|| { #body }) }.into()
48}
49
50#[proc_macro_attribute]
51pub fn terminates(_: TS1, tokens: TS1) -> TS1 {
52    tokens
53}
54
55#[proc_macro_attribute]
56pub fn pure(_: TS1, tokens: TS1) -> TS1 {
57    tokens
58}
59
60#[proc_macro_attribute]
61pub fn logic(_: TS1, _: TS1) -> TS1 {
62    TS1::new()
63}
64
65#[proc_macro]
66pub fn pearlite(_: TS1) -> TS1 {
67    TS1::new()
68}
69
70#[proc_macro_attribute]
71pub fn predicate(_: TS1, _: TS1) -> TS1 {
72    TS1::new()
73}
74
75#[proc_macro_attribute]
76pub fn law(_: TS1, _: TS1) -> TS1 {
77    TS1::new()
78}
79
80#[proc_macro_attribute]
81pub fn trusted(_: TS1, tokens: TS1) -> TS1 {
82    tokens
83}
84
85#[proc_macro]
86pub fn extern_spec(_: TS1) -> TS1 {
87    TS1::new()
88}
89
90#[proc_macro_attribute]
91pub fn maintains(_: TS1, tokens: TS1) -> TS1 {
92    tokens
93}
94
95#[proc_macro_attribute]
96pub fn open(_: TS1, tokens: TS1) -> TS1 {
97    tokens
98}
99
100#[proc_macro_attribute]
101pub fn open_inv_result(_: TS1, tokens: TS1) -> TS1 {
102    tokens
103}
104
105#[proc_macro_attribute]
106pub fn bitwise_proof(_: TS1, tokens: TS1) -> TS1 {
107    tokens
108}
109
110#[proc_macro_derive(DeepModel, attributes(DeepModelTy))]
111pub fn derive_deep_model(_: TS1) -> TS1 {
112    TS1::new()
113}
114
115#[proc_macro_derive(Resolve)]
116pub fn derive_resolve(_: TS1) -> TS1 {
117    TS1::new()
118}
119
120/// Visitor to delete all `#[invariant]` and `#[creusot_contracts::invariant]`
121/// attributes on loops.
122struct DeleteInvariants;
123
124impl VisitMut for DeleteInvariants {
125    fn visit_expr_for_loop_mut(&mut self, i: &mut syn::ExprForLoop) {
126        delete_invariants_attrs(&mut i.attrs);
127        syn::visit_mut::visit_expr_for_loop_mut(self, i)
128    }
129
130    fn visit_expr_while_mut(&mut self, i: &mut syn::ExprWhile) {
131        delete_invariants_attrs(&mut i.attrs);
132        syn::visit_mut::visit_expr_while_mut(self, i)
133    }
134
135    fn visit_expr_loop_mut(&mut self, i: &mut syn::ExprLoop) {
136        delete_invariants_attrs(&mut i.attrs);
137        syn::visit_mut::visit_expr_loop_mut(self, i)
138    }
139}
140
141// `invariant` or `creusot_contracts::invariant` or `::creusot_contracts::invariant`
142fn is_invariant(path: &syn::Path) -> bool {
143    if path.is_ident("invariant") {
144        return true;
145    }
146    let mut segments = path.segments.iter();
147    if let Some(first) = segments.next() {
148        if let Some(second) = segments.next() {
149            return first.ident == "creusot_contracts" && second.ident == "invariant";
150        }
151    }
152    false
153}
154
155fn delete_invariants_attrs(attrs: &mut Vec<syn::Attribute>) {
156    attrs.retain(|attr| {
157        if let syn::Meta::List(meta) = &attr.meta { !is_invariant(&meta.path) } else { true }
158    });
159}
160
161fn delete_invariants(item: &mut syn::ImplItemFn) {
162    DeleteInvariants.visit_impl_item_fn_mut(item);
163}
creusot_contracts_dummy/lib.rs

creusot_contracts_dummy/
lib.rs
