@@ -11,234 +11,7 @@ use syn::{
1111 punctuated:: Punctuated ,
1212} ;
1313
14- struct Contract {
15- pub requires : Vec < Expr > ,
16- pub maintains : Vec < Expr > ,
17- pub ensures : Vec < ExprClosure > ,
18- }
14+ mod macro;
15+ mod syntax;
1916
20- impl TryFrom < ContractArgs > for Contract {
21- type Error = syn:: Error ;
22-
23- fn try_from ( args : ContractArgs ) -> Result < Self > {
24- let mut requires: Vec < Expr > = vec ! [ ] ;
25- let mut maintains: Vec < Expr > = vec ! [ ] ;
26- let mut ensures: Vec < ExprClosure > = vec ! [ ] ;
27-
28- // The default pattern for `ensures` conditions. It must be resolvable at the call site.
29- let default_output_pat = args
30- . binds_pat
31- . clone ( )
32- . map ( |p| p. to_token_stream ( ) )
33- . unwrap_or_else ( || quote ! { output } ) ;
34-
35- for condition in args. conditions {
36- match condition {
37- Condition :: Requires { predicate } => requires. push ( predicate) ,
38- Condition :: Maintains { predicate } => maintains. push ( predicate) ,
39- Condition :: Ensures { predicate } => {
40- // Convert a simple expression into a closure.
41- let closure: ExprClosure = parse_quote ! { |#default_output_pat| #predicate } ;
42- ensures. push ( closure) ;
43- }
44- Condition :: EnsuresClosure { closure } => ensures. push ( closure) ,
45- }
46- }
47-
48- Ok ( Contract {
49- requires,
50- maintains,
51- ensures,
52- } )
53- }
54- }
55-
56- /// The main procedural macro for defining contracts on functions.
57- ///
58- /// This macro parses contract annotations and injects `assert!` statements
59- /// into the function body to perform runtime checks in debug builds.
60- #[ proc_macro_attribute]
61- pub fn contract ( args : TokenStream , input : TokenStream ) -> TokenStream {
62- // Parse the contract arguments from the attribute, e.g., `requires: x > 0, ...`
63- let contract_args = parse_macro_input ! ( args as ContractArgs ) ;
64- // Parse the function to which the attribute is attached.
65- let mut func = parse_macro_input ! ( input as ItemFn ) ;
66-
67- let contract = match Contract :: try_from ( contract_args) {
68- Ok ( contract) => contract,
69- Err ( e) => return e. to_compile_error ( ) . into ( ) ,
70- } ;
71-
72- // Generate the new, instrumented function body.
73- let new_body = match instrument_body ( & func, & contract) {
74- Ok ( body) => body,
75- Err ( e) => return e. to_compile_error ( ) . into ( ) ,
76- } ;
77-
78- // Replace the old function body with the new one.
79- * func. block = syn:: parse2 ( new_body) . expect ( "Failed to parse new function body" ) ;
80-
81- // Return the modified function.
82- func. into_token_stream ( ) . into ( )
83- }
84-
85- /// A container for all parsed arguments from the `#[contract]` attribute.
86- struct ContractArgs {
87- conditions : Vec < Condition > ,
88- binds_pat : Option < Pat > ,
89- }
90-
91- /// Represents a single contract condition, e.g., `requires: x > 0`.
92- enum Condition {
93- Requires { predicate : Expr } ,
94- Ensures { predicate : Expr } ,
95- EnsuresClosure { closure : ExprClosure } ,
96- Maintains { predicate : Expr } ,
97- }
98-
99- impl Parse for ContractArgs {
100- /// Custom parser for the contents of `#[contract(...)]`.
101- fn parse ( input : ParseStream ) -> Result < Self > {
102- let mut conditions = Vec :: new ( ) ;
103- let mut binds_pat = None ;
104-
105- // The arguments are a comma-separated list of conditions or a `binds` setting.
106- let items = Punctuated :: < ContractArgItem , Token ! [ , ] > :: parse_terminated ( input) ?;
107-
108- for item in items {
109- match item {
110- ContractArgItem :: Condition ( condition) => conditions. push ( condition) ,
111- ContractArgItem :: Binds ( pat) => {
112- if binds_pat. is_some ( ) {
113- return Err ( syn:: Error :: new ( pat. span ( ) , "duplicate `binds` setting" ) ) ;
114- }
115- binds_pat = Some ( pat) ;
116- }
117- }
118- }
119-
120- Ok ( ContractArgs {
121- conditions,
122- binds_pat,
123- } )
124- }
125- }
126-
127- /// An intermediate enum to help parse either a condition or a `binds` setting.
128- enum ContractArgItem {
129- Condition ( Condition ) ,
130- Binds ( Pat ) ,
131- }
132-
133- impl Parse for ContractArgItem {
134- fn parse ( input : ParseStream ) -> Result < Self > {
135- let lookahead = input. lookahead1 ( ) ;
136- if lookahead. peek ( kw:: binds) {
137- // Parse `binds: pat`
138- input. parse :: < kw:: binds > ( ) ?;
139- input. parse :: < Token ! [ : ] > ( ) ?;
140- let pat = Pat :: parse_single ( input) ?;
141- Ok ( ContractArgItem :: Binds ( pat) )
142- } else if lookahead. peek ( kw:: requires)
143- || lookahead. peek ( kw:: ensures)
144- || lookahead. peek ( kw:: maintains)
145- {
146- // Parse a condition like `requires: predicate` or `ensures: |val| predicate`
147- Ok ( ContractArgItem :: Condition ( input. parse ( ) ?) )
148- } else {
149- Err ( lookahead. error ( ) )
150- }
151- }
152- }
153-
154- impl Parse for Condition {
155- /// Parses a single condition.
156- fn parse ( input : ParseStream ) -> Result < Self > {
157- let lookahead = input. lookahead1 ( ) ;
158- if lookahead. peek ( kw:: requires) {
159- input. parse :: < kw:: requires > ( ) ?;
160- input. parse :: < Token ! [ : ] > ( ) ?;
161- Ok ( Condition :: Requires {
162- predicate : input. parse ( ) ?,
163- } )
164- } else if lookahead. peek ( kw:: ensures) {
165- input. parse :: < kw:: ensures > ( ) ?;
166- input. parse :: < Token ! [ : ] > ( ) ?;
167- let predicate: Expr = input. parse ( ) ?;
168- if let Expr :: Closure ( closure) = predicate {
169- Ok ( Condition :: EnsuresClosure { closure } )
170- } else {
171- Ok ( Condition :: Ensures { predicate } )
172- }
173- } else if lookahead. peek ( kw:: maintains) {
174- input. parse :: < kw:: maintains > ( ) ?;
175- input. parse :: < Token ! [ : ] > ( ) ?;
176- Ok ( Condition :: Maintains {
177- predicate : input. parse ( ) ?,
178- } )
179- } else {
180- Err ( lookahead. error ( ) )
181- }
182- }
183- }
184-
185- // Custom keywords for parsing. This allows us to use `requires`, `ensures`, etc.,
186- // as if they were built-in Rust keywords during parsing.
187- mod kw {
188- syn:: custom_keyword!( requires) ;
189- syn:: custom_keyword!( ensures) ;
190- syn:: custom_keyword!( maintains) ;
191- syn:: custom_keyword!( binds) ;
192- }
193-
194- /// Takes the original function and contract, and returns a new
195- /// token stream for the instrumented function body.
196- fn instrument_body ( func : & ItemFn , contract : & Contract ) -> Result < proc_macro2:: TokenStream > {
197- let original_body = & func. block ;
198- let is_async = func. sig . asyncness . is_some ( ) ;
199-
200- // The identifier for the return value binding. It's hygienic to prevent collisions.
201- let binding_ident = Ident :: new ( "__anodized_output" , Span :: mixed_site ( ) ) ;
202-
203- // --- Generate Precondition Checks ---
204- let preconditions = contract
205- . requires
206- . iter ( )
207- . map ( |predicate| {
208- let msg = format ! ( "Precondition failed: {}" , predicate. to_token_stream( ) ) ;
209- quote ! { assert!( #predicate, #msg) ; }
210- } )
211- . chain ( contract. maintains . iter ( ) . map ( |predicate| {
212- let msg = format ! ( "Pre-invariant failed: {}" , predicate. to_token_stream( ) ) ;
213- quote ! { assert!( #predicate, #msg) ; }
214- } ) ) ;
215-
216- // --- Generate Postcondition Checks ---
217- let postconditions = contract
218- . maintains
219- . iter ( )
220- . map ( |predicate| {
221- let msg = format ! ( "Post-invariant failed: {}" , predicate. to_token_stream( ) ) ;
222- quote ! { assert!( #predicate, #msg) ; }
223- } )
224- . chain ( contract. ensures . iter ( ) . map ( |closure| {
225- let msg = format ! ( "Postcondition failed: {}" , closure. to_token_stream( ) ) ;
226- quote ! { assert!( ( #closure) ( #binding_ident) , #msg) ; }
227- } ) ) ;
228-
229- // --- Construct the New Body ---
230- let body_expr = if is_async {
231- quote ! { async { #original_body } . await }
232- } else {
233- quote ! { { #original_body } }
234- } ;
235-
236- Ok ( quote ! {
237- {
238- #( #preconditions) *
239- let #binding_ident = #body_expr;
240- #( #postconditions) *
241- #binding_ident
242- }
243- } )
244- }
17+ pub use macro:: contract;
0 commit comments