safety_macro/
lib.rs

1use proc_macro::TokenStream;
2use safety_parser::{
3    configuration::env::config_exists, proc_macro2::TokenStream as TokenStream2, quote::quote,
4    safety::SafetyAttrArgs as AttrArgs, split_attrs::split_attrs_and_rest, syn,
5};
6
7/// This is a shared function to annotate SPs on caller and callee.
8///
9/// When `#[safety]` is removed, this function should be put into `#[requires]`
10/// or renamed `requires_inner`.
11fn tag(attr: TokenStream, item: TokenStream) -> TokenStream {
12    let mut ts = TokenStream2::new();
13
14    // add registered tool attr
15    let tool_attr = {
16        let attr = TokenStream2::from(attr.clone());
17        quote! { #[rapx::proof(#attr)] }
18    };
19    ts.extend(tool_attr);
20
21    let input = split_attrs_and_rest(item.into());
22    if !input.gen_doc {
23        // no need to generate docs on expressions
24        ts.extend(input.attrs);
25        ts.extend(input.rest);
26        return ts.into();
27    }
28
29    // push doc attrs first
30    ts.extend(input.attrs);
31
32    let attr_args: AttrArgs = syn::parse(attr).unwrap();
33    // push generated doc if available
34    if config_exists() {
35        for tag in &attr_args.args {
36            ts.extend(tag.gen_doc());
37        }
38    }
39
40    // push rest tokens
41    ts.extend(input.rest);
42    ts.into()
43}
44
45/// Tag SPs on an unsafe function item, or discharge SPs on an expression.
46///
47/// # Syntax Example
48///
49/// ```
50/// #![feature(stmt_expr_attributes)]
51/// #![feature(proc_macro_hygiene)]
52/// #![feature(register_tool)]
53/// #![register_tool(rapx)]
54/// # use safety_macro::safety;
55///
56/// // Tag SPs:
57/// #[safety { SP1 }] unsafe fn foo() {}
58/// #[safety { SP1, SP2 }] unsafe fn bar() {}
59///
60/// // Discharge SPs:
61/// #[safety { SP1 }] unsafe { foo() };
62/// #[safety { SP1: "reason" }] unsafe { foo() };
63/// #[safety { SP1, SP2: "shared reason" }] unsafe { bar() };
64/// #[safety { SP1: "reason1"; SP2: "reason2" }] unsafe { bar() };
65/// ```
66#[proc_macro_attribute]
67#[deprecated = "Use `#[requires]` instead."]
68pub fn safety(attr: TokenStream, item: TokenStream) -> TokenStream {
69    tag(attr, item)
70}
71
72/// Tag SPs on an unsafe function item.
73///
74/// # Syntax Example
75///
76/// ```
77/// #![feature(stmt_expr_attributes)]
78/// #![feature(proc_macro_hygiene)]
79/// #![feature(register_tool)]
80/// #![register_tool(rapx)]
81/// # use safety_macro::requires;
82///
83/// // Tag SPs:
84/// #[requires { SP1 }] unsafe fn foo() {}
85/// #[requires { SP1, SP2 }] unsafe fn bar() {}
86/// ```
87#[proc_macro_attribute]
88pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
89    tag(attr, item)
90}
91
92/// Discharge SPs.
93///
94/// NOTE: there is no check on whether the annotated is an expression or not.
95///
96/// # Syntax Example
97///
98/// ```
99/// #![feature(stmt_expr_attributes)]
100/// #![feature(proc_macro_hygiene)]
101/// #![feature(register_tool)]
102/// #![register_tool(rapx)]
103/// # use safety_macro::{checked, requires};
104///
105/// // Tag SPs:
106/// #[requires { SP1 }] unsafe fn foo() {}
107/// #[requires { SP1, SP2 }] unsafe fn bar() {}
108///
109/// // Discharge SPs:
110/// #[checked { SP1 }] unsafe { foo() };
111/// #[checked { SP1: "reason" }] unsafe { foo() };
112/// #[checked { SP1, SP2: "shared reason" }] unsafe { bar() };
113/// #[checked { SP1: "reason1"; SP2: "reason2" }] unsafe { bar() };
114/// ```
115#[proc_macro_attribute]
116pub fn checked(attr: TokenStream, item: TokenStream) -> TokenStream {
117    let mut ts = TokenStream::new();
118
119    // Prepend the attribute above all attributes on the expression.
120    let tool_attr: TokenStream = {
121        // attr is all the arguments in #[check(args)]
122        let attr = TokenStream2::from(attr.clone());
123        quote! { #[rapx::checked(#attr)] }.into()
124    };
125    ts.extend(tool_attr);
126
127    ts.extend(item);
128    ts
129}
safety_macro/lib.rs

safety_macro/
lib.rs
