Skip to content

Commit 7868f77

Browse files
mkovaxxmkovaxx
authored
[anodized-core] feat: improve spec embedding (#153)
- Embed each predicate as `Fn(*) -> bool` (instead of `Fn(*) -> ()`). - Embed a `fn` spec as only `requires` and `ensures` predicates. - Embed a loop spec in a way that will support multiple `decreases` values if necessary.
1 parent baccc4d commit 7868f77

10 files changed

Lines changed: 203 additions & 145 deletions

File tree

‎.vscode/settings.json‎

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎crates/anodized-core/src/instrument.rs‎

Lines changed: 8 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -39,20 +39,18 @@ impl Config {
3939
let spec_requires_fn = ItemFn {
4040
attrs: attrs.to_vec(),
4141
vis: syn::Visibility::Inherited,
42-
sig: Self::build_spec_fn_sig("__anodized_fn_requires", &item_fn.sig),
43-
block: Box::new(Self::build_precondition_fn_body(&spec.requires)),
44-
};
45-
let spec_maintains_fn = ItemFn {
46-
attrs: attrs.to_vec(),
47-
vis: syn::Visibility::Inherited,
48-
sig: Self::build_spec_fn_sig("__anodized_fn_maintains", &item_fn.sig),
49-
block: Box::new(Self::build_precondition_fn_body(&spec.maintains)),
42+
sig: Self::build_precondition_fn_sig("__anodized_fn_requires", &item_fn.sig),
43+
block: Box::new(Self::build_precondition_fn_body(
44+
&spec.requires,
45+
&spec.maintains,
46+
)),
5047
};
5148
let spec_ensures_fn = ItemFn {
5249
attrs: attrs.to_vec(),
5350
vis: syn::Visibility::Inherited,
54-
sig: Self::build_spec_fn_sig("__anodized_fn_ensures", &item_fn.sig),
55-
block: Box::new(Self::build_poscondition_fn_body(
51+
sig: Self::build_postcondition_fn_sig("__anodized_fn_ensures", &item_fn.sig),
52+
block: Box::new(Self::build_postcondition_fn_body(
53+
&spec.maintains,
5654
&spec.captures,
5755
&spec.ensures,
5856
&item_fn.sig.output,
@@ -61,7 +59,6 @@ impl Config {
6159

6260
spec_qualifiers_const.to_tokens(&mut tokens);
6361
spec_requires_fn.to_tokens(&mut tokens);
64-
spec_maintains_fn.to_tokens(&mut tokens);
6562
spec_ensures_fn.to_tokens(&mut tokens);
6663
}
6764

‎crates/anodized-core/src/instrument/data.rs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ impl Config {
1818

1919
let ident = &item_struct.ident;
2020
let (impl_generics, ty_generics, where_clause) = item_struct.generics.split_for_impl();
21-
let statements = Self::build_precondition_fn_body(&spec.maintains).stmts;
21+
let statements = Self::build_precondition_fn_body(&[], &spec.maintains).stmts;
2222

2323
item_struct.to_tokens(&mut tokens);
2424

@@ -27,7 +27,7 @@ impl Config {
2727
#[doc(hidden)]
2828
#[allow(warnings)]
2929
impl #impl_generics #ident #ty_generics #where_clause {
30-
fn __anodized_data_maintains(&self) {
30+
fn __anodized_data_maintains(&self) -> bool {
3131
#(#statements)*
3232
}
3333
}
@@ -43,7 +43,7 @@ impl Config {
4343

4444
let ident = &item_enum.ident;
4545
let (impl_generics, ty_generics, where_clause) = item_enum.generics.split_for_impl();
46-
let statements = Self::build_precondition_fn_body(&spec.maintains).stmts;
46+
let statements = Self::build_precondition_fn_body(&[], &spec.maintains).stmts;
4747

4848
item_enum.to_tokens(&mut tokens);
4949

@@ -52,7 +52,7 @@ impl Config {
5252
#[doc(hidden)]
5353
#[allow(warnings)]
5454
impl #impl_generics #ident #ty_generics #where_clause {
55-
fn __anodized_data_maintains(&self) {
55+
fn __anodized_data_maintains(&self) -> bool {
5656
// Bring all variants into scope for convenience.
5757
use #ident::*;
5858
#(#statements)*

‎crates/anodized-core/src/instrument/data_tests.rs‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,10 @@ fn embed_spec_item_struct() {
3838
where
3939
'LT_1: 'LT_2,
4040
{
41-
fn __anodized_data_maintains(&self) {
42-
let _ = | | -> bool { COND_1 };
43-
let _ = | | -> bool { COND_2 };
41+
fn __anodized_data_maintains(&self) -> bool {
42+
let __anodized_clause_1 = (| | -> bool { COND_1 })();
43+
let __anodized_clause_2 = (| | -> bool { COND_2 })();
44+
__anodized_clause_1 && __anodized_clause_2
4445
}
4546
}
4647
};
@@ -88,10 +89,11 @@ fn embed_spec_item_enum() {
8889
where
8990
'LT_1: 'LT_2,
9091
{
91-
fn __anodized_data_maintains(&self) {
92+
fn __anodized_data_maintains(&self) -> bool {
9293
use ENUM::*;
93-
let _ = | | -> bool { COND_1 };
94-
let _ = | | -> bool { COND_2 };
94+
let __anodized_clause_1 = (| | -> bool { COND_1 })();
95+
let __anodized_clause_2 = (| | -> bool { COND_2 })();
96+
__anodized_clause_1 && __anodized_clause_2
9597
}
9698
}
9799
};

‎crates/anodized-core/src/instrument/fns.rs‎

Lines changed: 86 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ impl Config {
3535
Ok(())
3636
}
3737

38-
pub fn build_spec_fn_sig(prefix: &str, sig: &Signature) -> Signature {
38+
pub fn build_precondition_fn_sig(prefix: &str, sig: &Signature) -> Signature {
3939
Signature {
4040
constness: sig.constness,
4141
asyncness: sig.asyncness,
@@ -47,7 +47,30 @@ impl Config {
4747
paren_token: sig.paren_token,
4848
inputs: sig.inputs.clone(),
4949
variadic: sig.variadic.clone(),
50-
output: syn::ReturnType::Default,
50+
output: parse_quote!(-> bool),
51+
}
52+
}
53+
54+
pub fn build_postcondition_fn_sig(prefix: &str, sig: &Signature) -> Signature {
55+
let mut inputs = sig.inputs.clone();
56+
let output_binder = match &sig.output {
57+
ReturnType::Type(_, return_type) => parse_quote!(__anodized_output: &#return_type),
58+
ReturnType::Default => parse_quote!(__anodized_output: &()),
59+
};
60+
inputs.push(output_binder);
61+
62+
Signature {
63+
constness: sig.constness,
64+
asyncness: sig.asyncness,
65+
unsafety: sig.unsafety,
66+
abi: sig.abi.clone(),
67+
fn_token: sig.fn_token,
68+
ident: syn::Ident::new(&format!("{prefix}_{}", sig.ident), sig.ident.span()),
69+
generics: sig.generics.clone(),
70+
paren_token: sig.paren_token,
71+
inputs,
72+
variadic: sig.variadic.clone(),
73+
output: parse_quote!(-> bool),
5174
}
5275
}
5376

@@ -96,67 +119,88 @@ impl Config {
96119
}
97120
}
98121

99-
pub fn build_precondition_fn_body(conditions: &[PreCondition]) -> Block {
100-
let statements = conditions.iter().map(|condition| -> Stmt {
122+
pub fn build_precondition_fn_body(
123+
requires: &[PreCondition],
124+
maintains: &[PreCondition],
125+
) -> Block {
126+
let mut statements: Vec<Stmt> = vec![];
127+
let mut clauses: Vec<Expr> = vec![];
128+
129+
for condition in requires.iter().chain(maintains) {
130+
let i = clauses.len();
131+
let name = Ident::new(&format!("__anodized_clause_{}", i + 1), Span::mixed_site());
101132
let closure = &condition.closure;
102-
parse_quote! { let _ = #closure; }
103-
});
133+
statements.push(parse_quote! { let #name = (#closure)(); });
134+
clauses.push(parse_quote! { #name });
135+
}
136+
137+
if clauses.is_empty() {
138+
clauses.push(parse_quote!(true));
139+
}
140+
104141
parse_quote! {
105142
{
106143
#(#statements)*
144+
#(#clauses)&&*
107145
}
108146
}
109147
}
110148

111-
pub fn build_poscondition_fn_body(
149+
pub fn build_postcondition_fn_body(
150+
maintains: &[PreCondition],
112151
captures: &[Capture],
113-
conditions: &[PostCondition],
152+
ensures: &[PostCondition],
114153
return_type: &ReturnType,
115154
) -> Result<Block> {
116-
let aliases = captures.iter().map(|capture| &capture.pat);
117-
let capture_exprs = captures.iter().map(|capture| -> Expr {
118-
let expr = &capture.expr;
119-
// Wrap in closure to guard against `return`.
120-
parse_quote! { (|| #expr)() }
121-
});
155+
let mut statements: Vec<Stmt> = vec![];
156+
let mut clauses: Vec<Expr> = vec![];
122157

123-
let mut statements = vec![];
158+
for condition in maintains {
159+
let i = clauses.len();
160+
let name = Ident::new(&format!("__anodized_clause_{}", i + 1), Span::mixed_site());
161+
let closure = &condition.closure;
162+
statements.push(parse_quote! { let #name = (#closure)(); });
163+
clauses.push(parse_quote! { #name });
164+
}
165+
166+
{
167+
let aliases = captures.iter().map(|capture| &capture.pat);
168+
let capture_exprs = captures.iter().map(|capture| -> Expr {
169+
let expr = &capture.expr;
170+
// Wrap in closure to guard against `return`.
171+
parse_quote! { (|| #expr)() }
172+
});
173+
statements.push(parse_quote! { let (#(#aliases),*) = (#(#capture_exprs),*); });
174+
}
124175

125-
for condition in conditions {
176+
let output_type = match return_type {
177+
ReturnType::Type(_, return_type) => return_type.as_ref().clone(),
178+
ReturnType::Default => parse_quote!(()),
179+
};
180+
for condition in ensures {
181+
let i = clauses.len();
182+
let name = Ident::new(&format!("__anodized_clause_{}", i + 1), Span::mixed_site());
126183
let closure = &condition.closure;
127-
// TODO: This sort of validation should happen during parsing.
128-
let output_binder = match closure.inputs.first() {
129-
Some(output_binder) if closure.inputs.len() == 1 => output_binder,
130-
_ => {
131-
return Err(syn::Error::new_spanned(
132-
&closure.inputs,
133-
"Postcondition closure must have exactly one parameter.",
134-
));
135-
}
136-
};
137-
let statement: Stmt = if let Pat::Type(_) = output_binder {
138-
// If the output binder has a type annotation, use as-is.
139-
parse_quote! { let _ = #closure; }
184+
let input = closure.inputs.first().expect("valid postcondition");
185+
if let Pat::Type(_) = input {
186+
statements.push(parse_quote! { let #name = (#closure)(__anodized_output); });
140187
} else {
141-
// Otherwise add a type annotation.
142188
let body = &closure.body;
143-
let output = &closure.output;
144-
match &return_type {
145-
ReturnType::Default => {
146-
parse_quote! { let _ = |#output_binder: &()| #output { #body }; }
147-
}
148-
ReturnType::Type(_, ty) => {
149-
parse_quote! { let _ = |#output_binder: &#ty| #output { #body }; }
150-
}
151-
}
152-
};
153-
statements.push(statement);
189+
statements.push(parse_quote! {
190+
let #name = (| #input: &#output_type | -> bool { #body })(__anodized_output);
191+
});
192+
}
193+
clauses.push(parse_quote! { #name });
194+
}
195+
196+
if clauses.is_empty() {
197+
clauses.push(parse_quote!(true));
154198
}
155199

156200
Ok(parse_quote! {
157201
{
158-
let (#(#aliases),*) = (#(#capture_exprs),*);
159202
#(#statements)*
203+
#(#clauses)&&*
160204
}
161205
})
162206
}

‎crates/anodized-core/src/instrument/fns_tests.rs‎

Lines changed: 18 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -39,27 +39,29 @@ fn embed_spec_item_fn() {
3939

4040
#[doc(hidden)]
4141
#[allow(warnings)]
42-
fn __anodized_fn_requires_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) {
43-
let _ = | | -> bool { COND_1 };
44-
let _ = | | -> bool { COND_2 };
45-
let _ = | | -> bool { COND_3 };
42+
fn __anodized_fn_requires_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) -> bool {
43+
let __anodized_clause_1 = (| | -> bool { COND_1 })();
44+
let __anodized_clause_2 = (| | -> bool { COND_2 })();
45+
let __anodized_clause_3 = (| | -> bool { COND_3 })();
46+
let __anodized_clause_4 = (| | -> bool { COND_4 })();
47+
let __anodized_clause_5 = (| | -> bool { COND_5 })();
48+
let __anodized_clause_6 = (| | -> bool { COND_6 })();
49+
__anodized_clause_1 && __anodized_clause_2 && __anodized_clause_3
50+
&& __anodized_clause_4 && __anodized_clause_5 && __anodized_clause_6
4651
}
4752

4853
#[doc(hidden)]
4954
#[allow(warnings)]
50-
fn __anodized_fn_maintains_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) {
51-
let _ = | | -> bool { COND_4 };
52-
let _ = | | -> bool { COND_5 };
53-
let _ = | | -> bool { COND_6 };
54-
}
55-
56-
#[doc(hidden)]
57-
#[allow(warnings)]
58-
fn __anodized_fn_ensures_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) {
55+
fn __anodized_fn_ensures_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2, __anodized_output: &RET_TYPE) -> bool {
56+
let __anodized_clause_1 = (| | -> bool { COND_4 })();
57+
let __anodized_clause_2 = (| | -> bool { COND_5 })();
58+
let __anodized_clause_3 = (| | -> bool { COND_6 })();
5959
let (ALIAS_1, (ALIAS_2, ALIAS_3)) = ((| | EXPR_1)(), (| | EXPR_2)());
60-
let _ = |PAT_1: &RET_TYPE| -> bool { COND_7 };
61-
let _ = |PAT_1: &RET_TYPE| -> bool { COND_8 };
62-
let _ = |PAT_2: TYPE| -> bool { COND_9 };
60+
let __anodized_clause_4 = (|PAT_1: &RET_TYPE| -> bool { COND_7 })(__anodized_output);
61+
let __anodized_clause_5 = (|PAT_1: &RET_TYPE| -> bool { COND_8 })(__anodized_output);
62+
let __anodized_clause_6 = (|PAT_2: TYPE| -> bool { COND_9 })(__anodized_output);
63+
__anodized_clause_1 && __anodized_clause_2 && __anodized_clause_3
64+
&& __anodized_clause_4 && __anodized_clause_5 && __anodized_clause_6
6365
}
6466

6567
fn FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) -> RET_TYPE {

‎crates/anodized-core/src/instrument/loops.rs‎

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,10 @@
22
#[path = "loops_tests.rs"]
33
mod loops_tests;
44

5+
use proc_macro2::Span;
56
use syn::{
6-
Block, Error, ExprClosure, ExprForLoop, ExprWhile, ItemFn, Result, Stmt, parse_quote,
7+
Block, Error, Expr, ExprClosure, ExprForLoop, ExprWhile, Ident, ItemFn, Result, Stmt,
8+
parse_quote,
79
visit_mut::{self, VisitMut},
810
};
911

@@ -29,25 +31,35 @@ impl Config {
2931

3032
fn instrument_loop_body(&self, spec: LoopSpec, stmts: &mut Vec<Stmt>) {
3133
if self.embed_spec {
32-
let maintains_block = Self::build_precondition_fn_body(&spec.maintains);
34+
let maintains_block = Self::build_precondition_fn_body(&[], &spec.maintains);
3335
stmts.insert(
3436
0,
3537
parse_quote! {
36-
let __anodized_loop_maintains = #maintains_block;
38+
let __anodized_loop_maintains = || -> bool #maintains_block;
3739
},
3840
);
3941

40-
let let_decreases: Option<Stmt> = spec.decreases.map(|loop_variant| {
41-
let expr = loop_variant.expr;
42-
parse_quote! {
43-
let _ = || #expr;
44-
}
45-
});
42+
let mut variant_stmts: Vec<Stmt> = Vec::new();
43+
let mut variant_names: Vec<Ident> = Vec::new();
44+
if let Some(loop_variant) = &spec.decreases {
45+
let i = variant_names.len();
46+
let name = Ident::new(&format!("__anodized_value_{}", i + 1), Span::mixed_site());
47+
let expr = &loop_variant.expr;
48+
variant_stmts.push(parse_quote! { let #name = (|| #expr)(); });
49+
variant_names.push(name);
50+
}
51+
let variant_expr: Option<Expr> = if !variant_names.is_empty() {
52+
Some(parse_quote! { (#(#variant_names),*) })
53+
} else {
54+
None
55+
};
56+
4657
stmts.insert(
4758
1,
4859
parse_quote! {
49-
let __anodized_loop_decreases = {
50-
#let_decreases
60+
let __anodized_loop_decreases = || {
61+
#(#variant_stmts)*
62+
#variant_expr
5163
};
5264
},
5365
);

0 commit comments

Comments
 (0)