anodized_core/
annotate.rs

1use syn::{
2    Attribute, Error, Expr, ExprAssign, FieldValue, Meta,
3    parse::{Parse, ParseStream, Result},
4    parse_quote,
5    spanned::Spanned,
6};
7
8use crate::{
9    Capture, Condition, DataSpec, LoopSpec, LoopVariant, PostCondition, Spec,
10    qualifiers::FnQualifiers,
11};
12
13pub mod syntax;
14use syntax::Keyword;
15
16#[cfg(test)]
17#[path = "annotate_tests.rs"]
18mod annotate_tests;
19
20impl Parse for Spec {
21    fn parse(input: ParseStream) -> Result<Self> {
22        let raw_spec = syntax::SpecFields::parse(input)?;
23
24        let mut errors = MultiError::empty();
25        let mut qualifiers = FnQualifiers::empty();
26        let mut requires: Vec<Condition> = vec![];
27        let mut maintains: Vec<Condition> = vec![];
28        let mut captures: Vec<Capture> = vec![];
29        let mut ensures: Vec<PostCondition> = vec![];
30
31        let is_sorted = raw_spec.is_sorted();
32
33        for field in raw_spec.fields {
34            let keyword = Keyword::from(&field.member);
35            match keyword {
36                Keyword::Unknown(_) => {
37                    // TODO: Check if it seems like a typo of a known keyword.
38                    errors.add(Error::new_spanned(&field.member, "unknown spec field"));
39                }
40                Keyword::Functional => {
41                    if let Err(error) =
42                        parse_fn_qualifier(field, FnQualifiers::FUNCTIONAL, &mut qualifiers)
43                    {
44                        errors.add(error);
45                    }
46                }
47                Keyword::Pure => {
48                    if let Err(error) =
49                        parse_fn_qualifier(field, FnQualifiers::PURE, &mut qualifiers)
50                    {
51                        errors.add(error);
52                    }
53                }
54                Keyword::Total => {
55                    if let Err(error) =
56                        parse_fn_qualifier(field, FnQualifiers::TOTAL, &mut qualifiers)
57                    {
58                        errors.add(error);
59                    }
60                }
61                Keyword::Deterministic => {
62                    if let Err(error) =
63                        parse_fn_qualifier(field, FnQualifiers::DETERMINISTIC, &mut qualifiers)
64                    {
65                        errors.add(error);
66                    }
67                }
68                Keyword::Effectfree => {
69                    if let Err(error) =
70                        parse_fn_qualifier(field, FnQualifiers::EFFECTFREE, &mut qualifiers)
71                    {
72                        errors.add(error);
73                    }
74                }
75                Keyword::Infallible => {
76                    if let Err(error) =
77                        parse_fn_qualifier(field, FnQualifiers::INFALLIBLE, &mut qualifiers)
78                    {
79                        errors.add(error);
80                    }
81                }
82                Keyword::Terminating => {
83                    if let Err(error) =
84                        parse_fn_qualifier(field, FnQualifiers::TERMINATING, &mut qualifiers)
85                    {
86                        errors.add(error);
87                    }
88                }
89                Keyword::Requires => {
90                    if let Err(error) = parse_conditions(field, &mut requires) {
91                        errors.add(error);
92                    }
93                }
94                Keyword::Maintains => {
95                    if let Err(error) = parse_conditions(field, &mut maintains) {
96                        errors.add(error);
97                    }
98                }
99                Keyword::Captures => {
100                    if !captures.is_empty() {
101                        errors.add(Error::new_spanned(
102                            &field.member,
103                            "at most one `captures` field is allowed; to capture multiple values, use a list: `captures: [binding1 = expr1, binding2 = expr2, ...]`",
104                        ));
105                    }
106                    if let Err(error) = parse_captures(field, &mut captures) {
107                        errors.add(error);
108                    }
109                }
110                Keyword::Binds | Keyword::Inspects => {
111                    errors.add(Error::new_spanned(
112                        &field.member,
113                        "no longer supported, use the following form instead: `ensures: |PAT| [EXPR, EXPR, ...]`",
114                    ));
115                }
116                Keyword::Ensures => {
117                    if let Err(error) = parse_postconds(field, &mut ensures) {
118                        errors.add(error);
119                    }
120                }
121                Keyword::Decreases => {
122                    errors.add(Error::new_spanned(&field.member, "not allowed here"));
123                }
124            }
125        }
126
127        if !is_sorted {
128            errors.add(Error::new(
129                input.span(),
130                "fields are out of order: the expected order is: `<QUALIFIERS>`, `requires`, `maintains`, `captures`, `inspects`, `ensures`, where `<QUALIFIERS>` are:\n
131`functional` (`pure` and `total`),\n
132`pure` (`deterministic` and `effectfree`),\n
133`total` (`infallible` and `terminating`)",
134            ));
135        }
136
137        if let Some(combined_error) = errors.get_combined() {
138            return Err(combined_error);
139        }
140
141        Ok(Self {
142            qualifiers,
143            requires,
144            maintains,
145            captures,
146            ensures,
147            span: input.span(),
148        })
149    }
150}
151
152impl Parse for DataSpec {
153    fn parse(input: ParseStream) -> Result<Self> {
154        let raw_spec = syntax::SpecFields::parse(input)?;
155
156        let mut errors = MultiError::empty();
157        let mut maintains: Vec<Condition> = vec![];
158
159        for field in raw_spec.fields {
160            let keyword = Keyword::from(&field.member);
161            match keyword {
162                Keyword::Unknown(_) => {
163                    errors.add(Error::new_spanned(&field.member, "unknown spec field"));
164                }
165                Keyword::Maintains => {
166                    if let Err(error) = parse_conditions(field, &mut maintains) {
167                        errors.add(error);
168                    }
169                }
170                _ => {
171                    errors.add(Error::new_spanned(&field.member, "not allowed here"));
172                }
173            }
174        }
175
176        if let Some(combined_error) = errors.get_combined() {
177            return Err(combined_error);
178        }
179
180        Ok(Self {
181            maintains,
182            span: input.span(),
183        })
184    }
185}
186
187impl Parse for LoopSpec {
188    fn parse(input: ParseStream) -> Result<Self> {
189        let raw_spec = syntax::SpecFields::parse(input)?;
190
191        let is_sorted = raw_spec.is_sorted();
192
193        let mut errors = MultiError::empty();
194        let mut decreases = None;
195        let mut maintains: Vec<Condition> = vec![];
196
197        for field in raw_spec.fields {
198            let keyword = Keyword::from(&field.member);
199            match keyword {
200                Keyword::Unknown(_) => {
201                    errors.add(Error::new_spanned(&field.member, "unknown spec field"));
202                }
203                Keyword::Maintains => {
204                    if let Err(error) = parse_conditions(field, &mut maintains) {
205                        errors.add(error);
206                    }
207                }
208                Keyword::Decreases => {
209                    if decreases.is_some() {
210                        errors.add(Error::new_spanned(
211                            &field.member,
212                            "multiple `decreases` fields are not allowed",
213                        ));
214                    }
215                    if let Err(error) = parse_decreases(field, &mut decreases) {
216                        errors.add(error);
217                    }
218                }
219                _ => {
220                    errors.add(Error::new_spanned(&field.member, "not allowed here"));
221                }
222            }
223        }
224
225        if !is_sorted {
226            errors.add(Error::new(
227                input.span(),
228                "fields are out of order: the expected order is `maintains`, `decreases`",
229            ));
230        }
231
232        if let Some(combined_error) = errors.get_combined() {
233            return Err(combined_error);
234        }
235
236        Ok(Self {
237            maintains,
238            decreases,
239            span: input.span(),
240        })
241    }
242}
243
244fn parse_fn_qualifier(
245    field: FieldValue,
246    value: FnQualifiers,
247    qualifiers: &mut FnQualifiers,
248) -> Result<()> {
249    if let Some(first_attr) = field.attrs.first() {
250        return Err(Error::new_spanned(
251            first_attr,
252            "attributes are not supported here",
253        ));
254    }
255    if field.colon_token.is_some() {
256        return Err(Error::new_spanned(
257            field.member,
258            "qualifier does not take a value",
259        ));
260    }
261    if qualifiers.contains(value) {
262        return Err(Error::new_spanned(
263            field.member,
264            "this qualifier is redundant; remove it",
265        ));
266    }
267    *qualifiers |= value;
268    Ok(())
269}
270
271fn parse_conditions(field: FieldValue, conditions: &mut Vec<Condition>) -> Result<()> {
272    let cfg_attr = find_cfg_attribute(&field.attrs)?;
273    let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
274        Some(attr.parse_args()?)
275    } else {
276        None
277    };
278    if field.colon_token.is_none() {
279        return Err(Error::new_spanned(field.expr, "expected an expression"));
280    };
281    if let Expr::Array(items) = field.expr {
282        for expr in items.elems {
283            conditions.push(Condition {
284                expr,
285                cfg: cfg.clone(),
286            });
287        }
288    } else {
289        conditions.push(Condition {
290            expr: field.expr,
291            cfg,
292        });
293    }
294    Ok(())
295}
296
297fn parse_postconds(field: FieldValue, postconds: &mut Vec<PostCondition>) -> Result<()> {
298    let cfg_attr = find_cfg_attribute(&field.attrs)?;
299    let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
300        Some(attr.parse_args()?)
301    } else {
302        None
303    };
304    if field.colon_token.is_none() {
305        return Err(Error::new_spanned(&field.expr, "expected an expression"));
306    };
307    match field.expr {
308        Expr::Closure(mut closure) => {
309            if closure.inputs.len() != 1 {
310                return Err(Error::new_spanned(
311                    closure,
312                    "postcondition closure must have exactly one input",
313                ));
314            }
315            let (pat, _) = closure.inputs.pop().unwrap().into_tuple();
316            if let Expr::Array(array) = *closure.body {
317                for expr in array.elems {
318                    postconds.push(PostCondition {
319                        pat: Some(pat.clone()),
320                        expr,
321                        cfg: cfg.clone(),
322                    });
323                }
324            } else {
325                postconds.push(PostCondition {
326                    pat: Some(pat),
327                    expr: *closure.body,
328                    cfg: cfg.clone(),
329                });
330            }
331        }
332        Expr::Array(array) => {
333            for expr in array.elems {
334                if let Expr::Closure(mut closure) = expr {
335                    if closure.inputs.len() != 1 {
336                        return Err(Error::new_spanned(
337                            closure,
338                            "postcondition closure must have exactly one input",
339                        ));
340                    }
341                    let (pat, _) = closure.inputs.pop().unwrap().into_tuple();
342                    postconds.push(PostCondition {
343                        pat: Some(pat),
344                        expr: *closure.body,
345                        cfg: cfg.clone(),
346                    });
347                } else {
348                    postconds.push(PostCondition {
349                        pat: None,
350                        expr,
351                        cfg: cfg.clone(),
352                    });
353                }
354            }
355        }
356        _ => {
357            postconds.push(PostCondition {
358                pat: None,
359                expr: field.expr,
360                cfg: cfg.clone(),
361            });
362        }
363    }
364    Ok(())
365}
366
367fn parse_captures(field: FieldValue, captures: &mut Vec<Capture>) -> Result<()> {
368    let cfg_attr = find_cfg_attribute(&field.attrs)?;
369    if cfg_attr.is_some() {
370        return Err(Error::new(
371            cfg_attr.span(),
372            "`cfg` attribute is not supported here",
373        ));
374    }
375    if field.colon_token.is_none() {
376        return Err(Error::new_spanned(field.expr, "expected an expression"));
377    };
378    match field.expr {
379        Expr::Assign(assignment) => {
380            captures.push(interpret_assignment_as_capture(assignment)?);
381        }
382        Expr::Array(array) => {
383            for elem in array.elems {
384                let Expr::Assign(assignment) = elem else {
385                    return Err(Error::new_spanned(elem, "expected an assignment"));
386                };
387                captures.push(interpret_assignment_as_capture(assignment)?);
388            }
389        }
390        _ => {
391            return Err(Error::new_spanned(
392                field.expr,
393                "expected an assignment or block",
394            ));
395        }
396    }
397    Ok(())
398}
399
400fn parse_decreases(field: FieldValue, decreases: &mut Option<LoopVariant>) -> Result<()> {
401    let cfg_attr = find_cfg_attribute(&field.attrs)?;
402    let cfg: Option<Meta> = if let Some(attr) = cfg_attr {
403        Some(attr.parse_args()?)
404    } else {
405        None
406    };
407    if field.colon_token.is_none() {
408        return Err(Error::new_spanned(field.expr, "expected an expression"));
409    };
410    if let Expr::Array(_) = field.expr {
411        return Err(Error::new_spanned(
412            field.expr,
413            "expected a single expression",
414        ));
415    } else {
416        *decreases = Some(LoopVariant {
417            expr: field.expr,
418            cfg,
419        });
420    }
421    Ok(())
422}
423
424/// Try to interpret an ExprAssign as a single Capture.
425fn interpret_assignment_as_capture(assignment: ExprAssign) -> Result<Capture> {
426    let left = assignment.left;
427    Ok(Capture {
428        // TODO: Make this less janky.
429        pat: parse_quote! { #left },
430        expr: *assignment.right,
431    })
432}
433
434fn find_cfg_attribute(attrs: &[Attribute]) -> Result<Option<&Attribute>> {
435    let mut cfg_attr: Option<&Attribute> = None;
436
437    for attr in attrs {
438        if attr.path().is_ident("cfg") {
439            if cfg_attr.is_some() {
440                return Err(Error::new(
441                    attr.span(),
442                    "multiple `cfg` attributes are not supported",
443                ));
444            }
445            cfg_attr = Some(attr);
446        } else {
447            return Err(Error::new(
448                attr.span(),
449                "unsupported attribute; only `cfg` is allowed",
450            ));
451        }
452    }
453
454    Ok(cfg_attr)
455}
456
457struct MultiError(Option<Error>);
458
459impl MultiError {
460    fn empty() -> Self {
461        Self(None)
462    }
463
464    fn get_combined(self) -> Option<Error> {
465        self.0
466    }
467
468    fn add(&mut self, error: Error) {
469        match &mut self.0 {
470            Some(acc) => acc.combine(error),
471            None => self.0 = Some(error),
472        }
473    }
474}
anodized_core/annotate.rs

anodized_core/
annotate.rs
