anodized_core/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use proc_macro2::Span;
4use syn::{Error, Expr, ExprClosure, Meta, Pat};
5
6use crate::qualifiers::FnQualifiers;
7
8pub mod annotate;
9pub mod instrument;
10pub mod qualifiers;
11
12#[cfg(test)]
13mod test_util;
14
15/// Specifies the intended behavior of a function or method: `fn`.
16#[derive(Debug)]
17// TODO: Rename to `FnSpec` to reduce ambiguity.
18pub struct Spec {
19    /// Qualifiers that constrain the behavior of the computation.
20    pub qualifiers: FnQualifiers,
21    /// Preconditions: conditions that must hold when the function is called.
22    pub requires: Vec<PreCondition>,
23    /// Invariants: conditions that must hold both when the function is called and when it returns.
24    pub maintains: Vec<PreCondition>,
25    /// Captures: expressions to snapshot at function entry for use in postconditions.
26    pub captures: Vec<Capture>,
27    /// Postconditions: conditions that must hold when the function returns.
28    pub ensures: Vec<PostCondition>,
29    /// The span in the source code, from which this spec was parsed.
30    span: Span,
31}
32
33impl Spec {
34    /// Empty spec that contains no elements.
35    pub fn empty() -> Self {
36        Self {
37            qualifiers: FnQualifiers::empty(),
38            requires: vec![],
39            maintains: vec![],
40            captures: vec![],
41            ensures: vec![],
42            span: Span::call_site(),
43        }
44    }
45
46    /// Returns `true` if the spec is empty (specifies nothing), otherwise returns `false`.
47    pub fn is_empty(&self) -> bool {
48        self.qualifiers.is_empty()
49            && self.requires.is_empty()
50            && self.maintains.is_empty()
51            && self.ensures.is_empty()
52            && self.captures.is_empty()
53    }
54
55    /// Construct an error from the whole spec.
56    pub fn spec_err(&self, message: &str) -> Error {
57        Error::new::<&str>(self.span, message)
58    }
59}
60
61/// Specifies the intended behavior of a data type: `struct` or `enum`.
62#[derive(Debug)]
63pub struct DataSpec {
64    /// Invariants: conditions that must hold for all instances of the data type.
65    pub maintains: Vec<PreCondition>,
66    /// The span in the source code, from which this spec was parsed.
67    span: Span,
68}
69
70impl DataSpec {
71    /// Empty spec that contains no elements.
72    pub fn empty() -> Self {
73        Self {
74            maintains: vec![],
75            span: Span::call_site(),
76        }
77    }
78
79    /// Returns `true` if the spec is empty (specifies nothing), otherwise returns `false`.
80    pub fn is_empty(&self) -> bool {
81        self.maintains.is_empty()
82    }
83
84    /// Construct an error from the whole spec.
85    pub fn spec_err(&self, message: &str) -> Error {
86        Error::new::<&str>(self.span, message)
87    }
88}
89
90/// Specifies the intended behavior of a loop: `while` or `for`.
91#[derive(Debug)]
92pub struct LoopSpec {
93    /// Loop invariants: conditions that must hold both before and after the loop's body runs.
94    pub maintains: Vec<PreCondition>,
95    /// Loop variant: an expression that decreases with each run of the loop's body.
96    pub decreases: Option<LoopVariant>,
97    /// The span in the source code, from which this spec was parsed.
98    span: Span,
99}
100
101impl LoopSpec {
102    /// Empty spec that contains no elements.
103    pub fn empty() -> Self {
104        Self {
105            maintains: vec![],
106            decreases: None,
107            span: Span::call_site(),
108        }
109    }
110
111    /// Returns `true` if the spec is empty (specifies nothing), otherwise returns `false`.
112    pub fn is_empty(&self) -> bool {
113        self.maintains.is_empty() && self.decreases.is_none()
114    }
115
116    /// Construct an error from the whole spec.
117    pub fn spec_err(&self, message: &str) -> Error {
118        Error::new::<&str>(self.span, message)
119    }
120}
121
122/// A precondition represented by a `bool`-valued expression.
123#[derive(Debug)]
124// TODO: Rename to `Condition` for clarity.
125pub struct PreCondition {
126    /// The closure that validates the precondition,
127    /// takes no input, e.g. `|| input.is_valid()`.
128    pub closure: ExprClosure,
129    /// **Static analyzers can safely ignore this field.**
130    ///
131    /// Build configuration filter to decide whether to add runtime checks.
132    /// Passed to a `cfg!()` guard in the instrumented function.
133    pub cfg: Option<Meta>,
134}
135
136/// A postcondition represented by a closure that takes the return value as a reference.
137#[derive(Debug)]
138pub struct PostCondition {
139    /// The closure that validates the postcondition, taking the function's
140    /// return value by reference, e.g. `|output| *output > 0`.
141    pub closure: ExprClosure,
142    /// **Static analyzers can safely ignore this field.**
143    ///
144    /// Build configuration filter to decide whether to add runtime checks.
145    /// Passed to a `cfg!()` guard in the instrumented function.
146    pub cfg: Option<Meta>,
147}
148
149/// Captures an expression's value at function entry.
150#[derive(Debug)]
151pub struct Capture {
152    /// The expression to capture.
153    pub expr: Expr,
154    /// The pattern to bind/destructure the captured value.
155    pub pat: Pat,
156}
157
158/// Decreases with each run of a loop's body.
159#[derive(Debug)]
160pub struct LoopVariant {
161    /// The expression that defines the variant.
162    pub expr: Expr,
163    /// **Static analyzers can safely ignore this field.**
164    ///
165    /// Build configuration filter to decide whether to add runtime checks.
166    /// Passed to a `cfg!()` guard in the instrumented code.
167    pub cfg: Option<Meta>,
168}
anodized_core/lib.rs

anodized_core/
lib.rs
