|
The `#[spec]` macro transforms the function body by injecting runtime checks whose behavior is controlled by `runtime-*` feature settings. This process, known as instrumentation, follows a clear pattern. |
|
|
|
Given an original function like this: |
|
|
|
```rust,ignore |
|
#[spec( |
|
requires: <PRECONDITION>, |
|
maintains: <INVARIANT>, |
|
captures: <CAPTURE_EXPR> as <ALIAS>, |
|
ensures: |<PATTERN>| <POSTCONDITION>, |
|
)] |
|
fn my_function(<ARGUMENTS>) -> <RETURN_TYPE> { |
|
<BODY> |
|
} |
|
``` |
|
|
|
The macro rewrites the body to be conceptually equivalent to the following: |
|
|
|
```rust,ignore |
|
fn my_function(<ARGUMENTS>) -> <RETURN_TYPE> { |
|
// 1. Preconditions and invariants are checked |
|
check!((| | <PRECONDITION>)(), "Precondition failed: <PRECONDITION>"); |
|
check!((| | <INVARIANT>)(), "Pre-invariant failed: <INVARIANT>"); |
|
|
|
// 2. Values are captured and the original function body is executed |
|
// Note 1: captures and body execution happen in a single tuple assignment |
|
// to ensure captured values aren't accessible to the function body |
|
// Note 2: the body is evaluated in a closure, so returns inside the body |
|
// do not bypass postcondition checks |
|
let (<ALIAS>, __anodized_output): (_, <RETURN_TYPE>) = ( |
|
<CAPTURE_EXPR>, |
|
(|| { <BODY> })(), |
|
); |
|
|
|
// 3. Invariants and postconditions are checked |
|
// Note 1: Captured values are in scope for postconditions |
|
// Note 2: `__anodized_output` is also in scope for postconditions, |
|
// but referring to it is strongly discouraged |
|
check!((| | <INVARIANT>)(), "Post-invariant failed: <INVARIANT>"); |
|
// Postcondition is checked by invoking the closure with a reference to the return value |
|
check!( |
|
(|<PATTERN>: &<RETURN_TYPE>| <POSTCONDITION>)(&__anodized_output), |
|
"Postcondition failed: | <PATTERN> | <POSTCONDITION>", |
|
); |
|
|
|
// 4. The result is returned |
|
__anodized_output |
|
} |
|
``` |
For details, see #41 and #71.
For reference, the
fninstrumentation is explained here:anodized/crates/anodized-core/README.md
Lines 75 to 123 in 8a9f84f