anodized_core/annotate/
mod.rs

1use syn::{
2    Attribute, Error, Expr, Ident, Meta, Pat, PatIdent,
3    parse::{Parse, ParseStream, Result},
4    parse_quote,
5    spanned::Spanned,
6};
7
8use crate::{
9    Capture, DataSpec, LoopSpec, LoopVariant, PostCondition, PreCondition, Spec,
10    annotate::syntax::{CaptureExpr, SpecArg, SpecArgValue},
11    qualifiers::FnQualifiers,
12};
13
14pub mod syntax;
15use syntax::{Captures, Keyword};
16
17#[cfg(test)]
18mod tests;
19
20impl Parse for Spec {
21    fn parse(input: ParseStream) -> Result<Self> {
22        let raw_spec = syntax::SpecArgs::parse(input)?;
23
24        let mut errors = MultiError::empty();
25        let mut qualifiers = FnQualifiers::empty();
26        let mut requires: Vec<PreCondition> = vec![];
27        let mut maintains: Vec<PreCondition> = vec![];
28        let mut captures: Vec<Capture> = vec![];
29        let mut binds_pattern: Option<Pat> = None;
30        let mut ensures: Vec<PostCondition> = vec![];
31
32        let is_sorted = raw_spec.is_sorted();
33
34        for arg in raw_spec.args {
35            match arg.keyword {
36                Keyword::Unknown(ident) => {
37                    errors.add(Error::new(
38                        arg.keyword_span,
39                        format!("unknown spec keyword `{ident}`"),
40                    ));
41                }
42                Keyword::Functional => {
43                    if let Err(error) =
44                        arg.parse_fn_qualifier(FnQualifiers::FUNCTIONAL, &mut qualifiers)
45                    {
46                        errors.add(error);
47                    }
48                }
49                Keyword::Pure => {
50                    if let Err(error) = arg.parse_fn_qualifier(FnQualifiers::PURE, &mut qualifiers)
51                    {
52                        errors.add(error);
53                    }
54                }
55                Keyword::Total => {
56                    if let Err(error) = arg.parse_fn_qualifier(FnQualifiers::TOTAL, &mut qualifiers)
57                    {
58                        errors.add(error);
59                    }
60                }
61                Keyword::Deterministic => {
62                    if let Err(error) =
63                        arg.parse_fn_qualifier(FnQualifiers::DETERMINISTIC, &mut qualifiers)
64                    {
65                        errors.add(error);
66                    }
67                }
68                Keyword::Effectfree => {
69                    if let Err(error) =
70                        arg.parse_fn_qualifier(FnQualifiers::EFFECTFREE, &mut qualifiers)
71                    {
72                        errors.add(error);
73                    }
74                }
75                Keyword::Infallible => {
76                    if let Err(error) =
77                        arg.parse_fn_qualifier(FnQualifiers::INFALLIBLE, &mut qualifiers)
78                    {
79                        errors.add(error);
80                    }
81                }
82                Keyword::Terminating => {
83                    if let Err(error) =
84                        arg.parse_fn_qualifier(FnQualifiers::TERMINATING, &mut qualifiers)
85                    {
86                        errors.add(error);
87                    }
88                }
89                Keyword::Requires => {
90                    if let Err(error) = arg.parse_preconditions(&mut requires) {
91                        errors.add(error);
92                    }
93                }
94                Keyword::Maintains => {
95                    if let Err(error) = arg.parse_preconditions(&mut maintains) {
96                        errors.add(error);
97                    }
98                }
99                Keyword::Captures => {
100                    if !captures.is_empty() {
101                        errors.add(Error::new(
102                            arg.keyword_span,
103                            "at most one `captures` parameter is allowed; to capture multiple values, use a list: `captures: [expr1, expr2, ...]`",
104                        ));
105                    }
106                    if let Err(error) = arg.parse_captures(&mut captures) {
107                        errors.add(error);
108                    }
109                }
110                Keyword::Binds => {
111                    if binds_pattern.is_some() {
112                        errors.add(Error::new(
113                            arg.keyword_span,
114                            "multiple `binds` parameters are not allowed",
115                        ));
116                    }
117                    if let Err(error) = arg.parse_binds(&mut binds_pattern) {
118                        errors.add(error);
119                    }
120                }
121                Keyword::Ensures => {
122                    if let Err(error) = arg.parse_postconditions(&binds_pattern, &mut ensures) {
123                        errors.add(error);
124                    }
125                }
126                Keyword::Decreases => {
127                    errors.add(Error::new(
128                        arg.keyword_span,
129                        format!("`{}` parameter is not supported here", &arg.keyword),
130                    ));
131                }
132            }
133        }
134
135        if !is_sorted {
136            errors.add(Error::new(
137                input.span(),
138                "parameters are out of order: the expected order is: `<QUALIFIERS>`, `requires`, `maintains`, `captures`, `binds`, `ensures`, where `<QUALIFIERS>` are:\n
139`functional` (`pure` and `total`),\n
140`pure` (`deterministic` and `effectfree`),\n
141`total` (`infallible` and `terminating`)",
142            ));
143        }
144
145        if let Some(combined_error) = errors.get_combined() {
146            return Err(combined_error);
147        }
148
149        Ok(Self {
150            qualifiers,
151            requires,
152            maintains,
153            captures,
154            ensures,
155            span: input.span(),
156        })
157    }
158}
159
160impl Parse for DataSpec {
161    fn parse(input: ParseStream) -> Result<Self> {
162        let raw_spec = syntax::SpecArgs::parse(input)?;
163
164        let mut errors = MultiError::empty();
165        let mut maintains: Vec<PreCondition> = vec![];
166
167        for arg in raw_spec.args {
168            match arg.keyword {
169                Keyword::Unknown(ident) => {
170                    errors.add(Error::new(
171                        arg.keyword_span,
172                        format!("unknown spec keyword `{ident}`"),
173                    ));
174                }
175                Keyword::Maintains => {
176                    if let Err(error) = arg.parse_preconditions(&mut maintains) {
177                        errors.add(error);
178                    }
179                }
180                _ => {
181                    errors.add(Error::new(
182                        arg.keyword_span,
183                        format!("`{}` parameter is not supported here", &arg.keyword),
184                    ));
185                }
186            }
187        }
188
189        if let Some(combined_error) = errors.get_combined() {
190            return Err(combined_error);
191        }
192
193        Ok(Self {
194            maintains,
195            span: input.span(),
196        })
197    }
198}
199
200impl Parse for LoopSpec {
201    fn parse(input: ParseStream) -> Result<Self> {
202        let raw_spec = syntax::SpecArgs::parse(input)?;
203
204        let is_sorted = raw_spec.is_sorted();
205
206        let mut errors = MultiError::empty();
207        let mut decreases = None;
208        let mut maintains: Vec<PreCondition> = vec![];
209
210        for arg in raw_spec.args {
211            match arg.keyword {
212                Keyword::Unknown(ident) => {
213                    errors.add(Error::new(
214                        arg.keyword_span,
215                        format!("unknown spec keyword `{ident}`"),
216                    ));
217                }
218                Keyword::Maintains => {
219                    if let Err(error) = arg.parse_preconditions(&mut maintains) {
220                        errors.add(error);
221                    }
222                }
223                Keyword::Decreases => {
224                    if decreases.is_some() {
225                        errors.add(Error::new(
226                            arg.keyword_span,
227                            "multiple `decreases` parameters are not allowed",
228                        ));
229                    }
230                    if let Err(error) = arg.parse_decreases(&mut decreases) {
231                        errors.add(error);
232                    }
233                }
234                _ => {
235                    errors.add(Error::new(
236                        arg.keyword_span,
237                        format!("`{}` parameter is not supported here", &arg.keyword),
238                    ));
239                }
240            }
241        }
242
243        if !is_sorted {
244            errors.add(Error::new(
245                input.span(),
246                "parameters are out of order: the expected order is `maintains`, `decreases`",
247            ));
248        }
249
250        if let Some(combined_error) = errors.get_combined() {
251            return Err(combined_error);
252        }
253
254        Ok(Self {
255            maintains,
256            decreases,
257            span: input.span(),
258        })
259    }
260}
261
262impl SpecArg {
263    fn parse_fn_qualifier(self, value: FnQualifiers, qualifiers: &mut FnQualifiers) -> Result<()> {
264        if let Some(first_attr) = self.attrs.first() {
265            return Err(Error::new_spanned(
266                first_attr,
267                format!("attributes are not supported on `{}`", self.keyword),
268            ));
269        }
270        if !matches!(self.value, SpecArgValue::None) {
271            return Err(Error::new_spanned(
272                self.value,
273                format!("qualifier `{}` does not take a value", self.keyword),
274            ));
275        }
276        if qualifiers.contains(value) {
277            return Err(Error::new(
278                self.keyword_span,
279                "this qualifier is redundant; remove it",
280            ));
281        }
282        *qualifiers |= value;
283        Ok(())
284    }
285
286    fn parse_preconditions(self, preconditions: &mut Vec<PreCondition>) -> Result<()> {
287        let cfg_attr = find_cfg_attribute(&self.attrs)?;
288        let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
289            Some(attr.parse_args()?)
290        } else {
291            None
292        };
293        let expr = self.value.try_into_expr()?;
294        if let Expr::Array(conditions) = expr {
295            for expr in conditions.elems {
296                preconditions.push(PreCondition {
297                    closure: interpret_expr_as_precondition(expr)?,
298                    cfg: cfg.clone(),
299                });
300            }
301        } else {
302            preconditions.push(PreCondition {
303                closure: interpret_expr_as_precondition(expr)?,
304                cfg,
305            });
306        }
307        Ok(())
308    }
309
310    fn parse_captures(self, captures: &mut Vec<Capture>) -> Result<()> {
311        let cfg_attr = find_cfg_attribute(&self.attrs)?;
312        if cfg_attr.is_some() {
313            return Err(Error::new(
314                cfg_attr.span(),
315                "`cfg` attribute is not supported on `captures`",
316            ));
317        }
318        let capture_list = self.value.try_into_captures()?;
319        match capture_list {
320            Captures::One(capture_expr) => {
321                captures.push(interpret_capture_expr_as_capture(*capture_expr.clone())?);
322            }
323            Captures::Many { elems, .. } => {
324                for capture_expr in elems {
325                    captures.push(interpret_capture_expr_as_capture(capture_expr)?);
326                }
327            }
328        }
329        Ok(())
330    }
331
332    fn parse_binds(self, pattern: &mut Option<Pat>) -> Result<()> {
333        let cfg_attr = find_cfg_attribute(&self.attrs)?;
334        if cfg_attr.is_some() {
335            return Err(Error::new(
336                cfg_attr.span(),
337                "`cfg` attribute is not supported on `binds`",
338            ));
339        }
340        let binds_pattern = self.value.try_into_pat()?;
341        *pattern = Some(binds_pattern);
342        Ok(())
343    }
344
345    fn parse_postconditions(
346        self,
347        binds_pattern: &Option<Pat>,
348        postconditions: &mut Vec<PostCondition>,
349    ) -> Result<()> {
350        let cfg_attr = find_cfg_attribute(&self.attrs)?;
351        let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
352            Some(attr.parse_args()?)
353        } else {
354            None
355        };
356        let expr = self.value.try_into_expr()?;
357        let default_pattern = binds_pattern.clone().unwrap_or(parse_quote! { output });
358        if let Expr::Array(conditions) = expr {
359            for expr in conditions.elems {
360                postconditions.push(PostCondition {
361                    closure: interpret_expr_as_postcondition(expr, default_pattern.clone())?,
362                    cfg: cfg.clone(),
363                });
364            }
365        } else {
366            postconditions.push(PostCondition {
367                closure: interpret_expr_as_postcondition(expr, default_pattern)?,
368                cfg,
369            });
370        }
371        Ok(())
372    }
373
374    fn parse_decreases(self, decreases: &mut Option<LoopVariant>) -> Result<()> {
375        let cfg_attr = find_cfg_attribute(&self.attrs)?;
376        let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
377            Some(attr.parse_args()?)
378        } else {
379            None
380        };
381        let expr_span = self.value.span();
382        let expr = self.value.try_into_expr()?;
383        if let Expr::Array(_) = expr {
384            return Err(Error::new(expr_span, "expected a single expression"));
385        } else {
386            *decreases = Some(LoopVariant { expr, cfg });
387        }
388        Ok(())
389    }
390}
391
392/// Try to interpret a CaptureExpr as a single Capture
393fn interpret_capture_expr_as_capture(capture_expr: CaptureExpr) -> Result<Capture> {
394    let span = capture_expr.span();
395    let CaptureExpr { expr, as_, pat } = capture_expr;
396
397    match (expr, as_, pat) {
398        // Complete form: <expression> `as` <pattern>
399        (Some(expr), Some(_), Some(pat)) => Ok(Capture { expr, pat }),
400
401        // Shorthand: <identifier>
402        (Some(ref expr @ Expr::Path(ref path)), None, None)
403            if path.path.segments.len() == 1
404                && path.path.leading_colon.is_none()
405                && path.attrs.is_empty()
406                && path.qself.is_none() =>
407        {
408            // auto-generate binding with `old_` prefix
409            let ident = &path.path.segments[0].ident;
410            let ident_alias = Ident::new(&format!("old_{}", ident), ident.span());
411            let pat = Pat::Ident(PatIdent {
412                ident: ident_alias,
413                attrs: vec![],
414                mutability: None,
415                by_ref: None,
416                subpat: None,
417            });
418            Ok(Capture {
419                expr: expr.clone(),
420                pat,
421            })
422        }
423
424        // Missing <pattern>
425        (Some(_), Some(_), None) => Err(Error::new_spanned(as_, "expected pattern after `as`")),
426
427        // Missing `as` and <pattern>
428        (Some(expr), None, None) => Err(Error::new_spanned(
429            expr,
430            "complex expression must be bound/descructured: <expression> `as` <pattern>",
431        )),
432
433        // Missing `as`
434        (Some(_), None, Some(pat)) => Err(Error::new_spanned(pat, "expected `as` <pattern>")),
435
436        // Missing <expression>
437        (None, _, _) => Err(Error::new(
438            span,
439            "expected capture: <expression> `as` <pattern>",
440        )),
441    }
442}
443
444/// Interpret expression as a zero-parameter closure, wrapping if necessary.
445/// Used for preconditions which don't need access to the return value.
446fn interpret_expr_as_precondition(expr: Expr) -> Result<syn::ExprClosure> {
447    match expr {
448        // Already a closure, validate it has no arguments.
449        Expr::Closure(closure) => {
450            if closure.inputs.is_empty() {
451                Ok(closure)
452            } else {
453                Err(Error::new_spanned(
454                    closure.or1_token,
455                    format!(
456                        "precondition closure must have no arguments, found {}",
457                        closure.inputs.len()
458                    ),
459                ))
460            }
461        }
462        // Naked expression, wrap in an argumentless closure.
463        expr => Ok(syn::ExprClosure {
464            attrs: vec![],
465            lifetimes: None,
466            constness: None,
467            movability: None,
468            asyncness: None,
469            capture: None,
470            or1_token: Default::default(),
471            inputs: syn::punctuated::Punctuated::new(),
472            or2_token: Default::default(),
473            output: syn::ReturnType::Default,
474            body: Box::new(expr),
475        }),
476    }
477}
478
479/// Interpret expression as a closure with a single argument (eg the list of
480/// aliases and function result), wrapping if necessary.
481/// Used for postconditions which take the return value as an argument.
482fn interpret_expr_as_postcondition(expr: Expr, default_binding: Pat) -> Result<syn::ExprClosure> {
483    match expr {
484        // Already a closure, validate it has exactly one argument.
485        Expr::Closure(closure) => {
486            if closure.inputs.len() == 1 {
487                Ok(closure)
488            } else {
489                Err(Error::new_spanned(
490                    closure.or1_token,
491                    format!(
492                        "postcondition closure must have exactly one argument, found {}",
493                        closure.inputs.len()
494                    ),
495                ))
496            }
497        }
498        // Naked expression, wrap in a closure with default binding.
499        expr => Ok(syn::ExprClosure {
500            attrs: vec![],
501            lifetimes: None,
502            constness: None,
503            movability: None,
504            asyncness: None,
505            capture: None,
506            or1_token: Default::default(),
507            inputs: syn::punctuated::Punctuated::from_iter([default_binding]),
508            or2_token: Default::default(),
509            output: syn::ReturnType::Default,
510            body: Box::new(expr),
511        }),
512    }
513}
514
515fn find_cfg_attribute(attrs: &[Attribute]) -> Result<Option<&Attribute>> {
516    let mut cfg_attr: Option<&Attribute> = None;
517
518    for attr in attrs {
519        if attr.path().is_ident("cfg") {
520            if cfg_attr.is_some() {
521                return Err(Error::new(
522                    attr.span(),
523                    "multiple `cfg` attributes are not supported",
524                ));
525            }
526            cfg_attr = Some(attr);
527        } else {
528            return Err(Error::new(
529                attr.span(),
530                "unsupported attribute; only `cfg` is allowed",
531            ));
532        }
533    }
534
535    Ok(cfg_attr)
536}
537
538struct MultiError(Option<Error>);
539
540impl MultiError {
541    fn empty() -> Self {
542        Self(None)
543    }
544
545    fn get_combined(self) -> Option<Error> {
546        self.0
547    }
548
549    fn add(&mut self, error: Error) {
550        match &mut self.0 {
551            Some(acc) => acc.combine(error),
552            None => self.0 = Some(error),
553        }
554    }
555}
anodized_core/annotate/mod.rs

anodized_core/annotate/
mod.rs
