contracts 0.6.7

Design-by-contract attributes
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85

/* This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */

use proc_macro2::TokenStream;
use quote::ToTokens;
use syn::{FnArg, ImplItem, ImplItemFn, Item, ItemFn, ItemImpl};

use crate::implementation::{ContractMode, ContractType, FuncWithContracts};

pub(crate) fn invariant(mode: ContractMode, attr: TokenStream, toks: TokenStream) -> TokenStream {
    let item: Item = syn::parse_quote!(#toks);

    let name = mode.name().unwrap().to_string() + "invariant";

    match item {
        Item::Fn(fn_) => invariant_fn(mode, attr, fn_),
        Item::Impl(impl_) => invariant_impl(mode, attr, impl_),
        _ => unimplemented!(
            "The #[{}] attribute only works on functions and impl-blocks.",
            name
        ),
    }
}

fn invariant_fn(mode: ContractMode, attr: TokenStream, func: ItemFn) -> TokenStream {
    let ty = ContractType::Invariant;

    let f = FuncWithContracts::new_with_initial_contract(func, ty, mode, attr);

    f.generate()
}

/// Generate the token-stream for an `impl` block with a "global" invariant.
fn invariant_impl(
    mode: ContractMode,
    invariant: TokenStream,
    mut impl_def: ItemImpl,
) -> TokenStream {
    // all that is done is prefix all the function definitions with
    // the invariant attribute.
    // The following expansion of the attributes will then implement the
    // invariant just like it's done for functions.

    // The mode received is "raw", so it can't be "Disabled" or "LogOnly"
    // but it can't hurt to deal with it anyway.
    let name = match mode.name() {
        Some(n) => n.to_string() + "invariant",
        None => {
            return quote::quote!( #impl_def );
        }
    };

    let invariant_ident = syn::Ident::new(&name, proc_macro2::Span::call_site());

    fn method_uses_self(method: &ImplItemFn) -> bool {
        let inputs = &method.sig.inputs;

        if !inputs.is_empty() {
            matches!(inputs[0], FnArg::Receiver(_))
        } else {
            false
        }
    }

    for item in &mut impl_def.items {
        if let ImplItem::Fn(method) = item {
            // only implement invariants for methods that take `self`
            if !method_uses_self(method) {
                continue;
            }

            let method_toks = quote::quote! {
                #[#invariant_ident(#invariant)]
                #method
            };

            let met: ImplItemFn = syn::parse_quote!(#method_toks);

            *method = met;
        }
    }

    impl_def.into_token_stream()
}