anodized_core/
lib.rs

1#![doc = include_str!("../README.md")]
2
3use proc_macro2::Span;
4use syn::{Error, Expr, 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<Condition>,
23    /// Invariants: conditions that must hold both when the function is called and when it returns.
24    pub maintains: Vec<Condition>,
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<Condition>,
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<Condition>,
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 condition represented by a `bool`-valued expression.
123#[derive(Debug)]
124pub struct Condition {
125    /// The expression that validates the condition, e.g. `value > 42`.
126    pub expr: Expr,
127    /// **Static analyzers can safely ignore this field.**
128    ///
129    /// Build configuration filter to decide whether to add runtime checks.
130    /// Passed to a `cfg!()` guard in the instrumented function.
131    pub cfg: Option<Meta>,
132}
133
134/// A postcondition represented by a pattern to bind the output and a `bool`-valued expression.
135#[derive(Debug)]
136pub struct PostCondition {
137    /// The pattern to bind/destructure the function's output, e.g. `ref answer`.
138    pub pat: Option<Pat>,
139    /// The expression that validates the postcondition, e.g. `answer == "forty-two"`.
140    pub expr: Expr,
141    /// **Static analyzers can safely ignore this field.**
142    ///
143    /// Build configuration filter to decide whether to add runtime checks.
144    /// Passed to a `cfg!()` guard in the instrumented function.
145    pub cfg: Option<Meta>,
146}
147
148/// Captures an expression's value at function entry.
149#[derive(Debug)]
150pub struct Capture {
151    /// The pattern to bind/destructure the captured value.
152    pub pat: Pat,
153    /// The expression to capture.
154    pub expr: Expr,
155}
156
157/// Decreases with each run of a loop's body.
158#[derive(Debug)]
159pub struct LoopVariant {
160    /// The expression that defines the variant.
161    pub expr: Expr,
162    /// **Static analyzers can safely ignore this field.**
163    ///
164    /// Build configuration filter to decide whether to add runtime checks.
165    /// Passed to a `cfg!()` guard in the instrumented code.
166    pub cfg: Option<Meta>,
167}
anodized_core/lib.rs

anodized_core/
lib.rs
