safety-macro 0.4.0

A macro for using safety tags defined in tag-std
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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

use proc_macro::TokenStream;
use safety_parser::{
    configuration::env::config_exists, proc_macro2::TokenStream as TokenStream2, quote::quote,
    safety::SafetyAttrArgs as AttrArgs, split_attrs::split_attrs_and_rest, syn,
};

/// This is a shared function to annotate SPs on caller and callee.
///
/// When `#[safety]` is removed, this function should be put into `#[requires]`
/// or renamed `requires_inner`.
fn tag(attr: TokenStream, item: TokenStream) -> TokenStream {
    let mut ts = TokenStream2::new();

    // add registered tool attr
    let tool_attr = {
        let attr = TokenStream2::from(attr.clone());
        quote! { #[rapx::proof(#attr)] }
    };
    ts.extend(tool_attr);

    let input = split_attrs_and_rest(item.into());
    if !input.gen_doc {
        // no need to generate docs on expressions
        ts.extend(input.attrs);
        ts.extend(input.rest);
        return ts.into();
    }

    // push doc attrs first
    ts.extend(input.attrs);

    let attr_args: AttrArgs = syn::parse(attr).unwrap();
    // push generated doc if available
    if config_exists() {
        for tag in &attr_args.args {
            ts.extend(tag.gen_doc());
        }
    }

    // push rest tokens
    ts.extend(input.rest);
    ts.into()
}

/// Tag SPs on an unsafe function item, or discharge SPs on an expression.
///
/// # Syntax Example
///
/// ```
/// #![feature(stmt_expr_attributes)]
/// #![feature(proc_macro_hygiene)]
/// #![feature(register_tool)]
/// #![register_tool(rapx)]
/// # use safety_macro::safety;
///
/// // Tag SPs:
/// #[safety { SP1 }] unsafe fn foo() {}
/// #[safety { SP1, SP2 }] unsafe fn bar() {}
///
/// // Discharge SPs:
/// #[safety { SP1 }] unsafe { foo() };
/// #[safety { SP1: "reason" }] unsafe { foo() };
/// #[safety { SP1, SP2: "shared reason" }] unsafe { bar() };
/// #[safety { SP1: "reason1"; SP2: "reason2" }] unsafe { bar() };
/// ```
#[proc_macro_attribute]
#[deprecated = "Use `#[requires]` instead."]
pub fn safety(attr: TokenStream, item: TokenStream) -> TokenStream {
    tag(attr, item)
}

/// Tag SPs on an unsafe function item.
///
/// # Syntax Example
///
/// ```
/// #![feature(stmt_expr_attributes)]
/// #![feature(proc_macro_hygiene)]
/// #![feature(register_tool)]
/// #![register_tool(rapx)]
/// # use safety_macro::requires;
///
/// // Tag SPs:
/// #[requires { SP1 }] unsafe fn foo() {}
/// #[requires { SP1, SP2 }] unsafe fn bar() {}
/// ```
#[proc_macro_attribute]
pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
    tag(attr, item)
}

/// Discharge SPs.
///
/// NOTE: there is no check on whether the annotated is an expression or not.
///
/// # Syntax Example
///
/// ```
/// #![feature(stmt_expr_attributes)]
/// #![feature(proc_macro_hygiene)]
/// #![feature(register_tool)]
/// #![register_tool(rapx)]
/// # use safety_macro::{checked, requires};
///
/// // Tag SPs:
/// #[requires { SP1 }] unsafe fn foo() {}
/// #[requires { SP1, SP2 }] unsafe fn bar() {}
///
/// // Discharge SPs:
/// #[checked { SP1 }] unsafe { foo() };
/// #[checked { SP1: "reason" }] unsafe { foo() };
/// #[checked { SP1, SP2: "shared reason" }] unsafe { bar() };
/// #[checked { SP1: "reason1"; SP2: "reason2" }] unsafe { bar() };
/// ```
#[proc_macro_attribute]
pub fn checked(attr: TokenStream, item: TokenStream) -> TokenStream {
    let mut ts = TokenStream::new();

    // Prepend the attribute above all attributes on the expression.
    let tool_attr: TokenStream = {
        // attr is all the arguments in #[check(args)]
        let attr = TokenStream2::from(attr.clone());
        quote! { #[rapx::checked(#attr)] }.into()
    };
    ts.extend(tool_attr);

    ts.extend(item);
    ts
}